quebex

  1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
  2--
  3-- SPDX-License-Identifier: GPL-3.0-only
  4
  5module Explorer (exploreTests) where
  6
  7import Data.List (sort)
  8import Data.Map qualified as Map
  9import Data.Maybe (fromJust)
 10import Language.QBE.Backend.Store qualified as ST
 11import Language.QBE.Simulator.Default.Expression qualified as DE
 12import Language.QBE.Simulator.Explorer (explore)
 13import Language.QBE.Simulator.Symbolic.Tracer qualified as T
 14import Language.QBE.Types qualified as QBE
 15import Test.Tasty
 16import Test.Tasty.HUnit
 17import Util
 18
 19branchPoints :: [(ST.Assign, T.ExecTrace)] -> [[Bool]]
 20branchPoints lst = sort $ map (\(_, t) -> map fst t) lst
 21
 22findAssign :: [(ST.Assign, T.ExecTrace)] -> [Bool] -> Maybe ST.Assign
 23findAssign [] _ = Nothing
 24findAssign ((a, eTrace) : xs) toFind
 25  | map fst eTrace == toFind = Just a
 26  | otherwise = findAssign xs toFind
 27
 28------------------------------------------------------------------------
 29
 30exploreTests :: TestTree
 31exploreTests =
 32  testGroup
 33    "Tests for Symbolic Program Exploration"
 34    [ testCase "Explore program with four execution paths" $
 35        do
 36          prog <-
 37            parseProg
 38              "function $branchOnInput(w %cond1, w %cond2) {\n\
 39              \@jump.1\n\
 40              \jnz %cond1, @branch.1, @branch.2\n\
 41              \@branch.1\n\
 42              \jmp @jump.2\n\
 43              \@branch.2\n\
 44              \jmp @jump.2\n\
 45              \@jump.2\n\
 46              \jnz %cond2, @branch.3, @branch.4\n\
 47              \@branch.3\n\
 48              \ret\n\
 49              \@branch.4\n\
 50              \ret\n\
 51              \}"
 52
 53          let funcDef = findFunc prog (QBE.GlobalIdent "branchOnInput")
 54          eTraces <- explore prog funcDef [("cond1", QBE.Word), ("cond2", QBE.Word)]
 55
 56          let branches = branchPoints eTraces
 57          branches @?= [[False, False], [False, True], [True, False], [True, True]],
 58      testCase "Unsatisfiable branches" $
 59        do
 60          prog <-
 61            parseProg
 62              "function $branchOnInput(w %cond1) {\n\
 63              \@jump.1\n\
 64              \jnz %cond1, @branch.1, @branch.2\n\
 65              \@branch.1\n\
 66              \jmp @jump.2\n\
 67              \@branch.2\n\
 68              \jmp @jump.2\n\
 69              \@jump.2\n\
 70              \jnz %cond1, @branch.3, @branch.4\n\
 71              \@branch.3\n\
 72              \ret\n\
 73              \@branch.4\n\
 74              \ret\n\
 75              \}"
 76
 77          let funcDef = findFunc prog (QBE.GlobalIdent "branchOnInput")
 78          eTraces <- explore prog funcDef [("cond1", QBE.Word)]
 79
 80          let branches = branchPoints eTraces
 81          branches @?= [[False, False], [True, True]],
 82      testCase "Branch with overflow arithmetics" $
 83        do
 84          prog <-
 85            parseProg
 86              "function $branchArithmetics(w %input) {\n\
 87              \@start\n\
 88              \%cond =w add %input, 1\n\
 89              \jnz %input, @branch.1, @branch.2\n\
 90              \@branch.1\n\
 91              \ret\n\
 92              \@branch.2\n\
 93              \ret\n\
 94              \}"
 95
 96          let funcDef = findFunc prog (QBE.GlobalIdent "branchArithmetics")
 97          eTraces <- explore prog funcDef [("input", QBE.Word)]
 98
 99          let branches = branchPoints eTraces
100          branches @?= [[False], [True]]
101
102          let assign = fromJust $ findAssign eTraces [False]
103          Map.lookup "input" assign @?= (Just $ DE.VWord 0),
104      testCase "Store symbolic value and memory, load it and pass it to function" $
105        do
106          prog <-
107            parseProg
108              "function $branchOnInput(w %cond1) {\n\
109              \@jump.1\n\
110              \jnz %cond1, @branch.1, @branch.2\n\
111              \@branch.1\n\
112              \jmp @jump.2\n\
113              \@branch.2\n\
114              \jmp @jump.2\n\
115              \@jump.2\n\
116              \jnz %cond1, @branch.3, @branch.4\n\
117              \@branch.3\n\
118              \ret\n\
119              \@branch.4\n\
120              \ret\n\
121              \}\n\
122              \function $entry(w %in) {\n\
123              \@start\n\
124              \%a =l alloc4 4\n\
125              \storew %in, %a\n\
126              \%l =w loadw %a\n\
127              \call $branchOnInput(w %l)\n\
128              \ret\n\
129              \}"
130
131          let funcDef = findFunc prog (QBE.GlobalIdent "entry")
132          eTraces <- explore prog funcDef [("x", QBE.Word)]
133
134          let branches = branchPoints eTraces
135          branches @?= [[False, False], [True, True]],
136      testCase "Branch on a specific concrete 64-bit value" $
137        do
138          prog <-
139            parseProg
140              "function $f(l %input.0) {\n\
141              \@start\n\
142              \%input.1 =l sub %input.0, 42\n\
143              \jnz %input.1, @not42, @is42\n\
144              \@not42\n\
145              \ret\n\
146              \@is42\n\
147              \ret\n\
148              \}"
149
150          let funcDef = findFunc prog (QBE.GlobalIdent "f")
151          eTraces <- explore prog funcDef [("y", QBE.Long)]
152
153          branchPoints eTraces @?= [[False], [True]]
154          let assign = fromJust $ findAssign eTraces [False]
155          Map.lookup "y" assign @?= (Just $ DE.VLong 42),
156      testCase "Branching with subtyping" $
157        do
158          prog <-
159            parseProg
160              "function $f(l %input.0, w %input.1) {\n\
161              \@start\n\
162              \%added =w add %input.1, 1\n\
163              \%subed =w sub %added, %input.1\n\
164              \%result =w add %added, %subed\n\
165              \jnz %result, @b1, @b2\n\
166              \@b1\n\
167              \jnz %input.0, @b2, @b2\n\
168              \@b2\n\
169              \ret\n\
170              \}"
171
172          let funcDef = findFunc prog (QBE.GlobalIdent "f")
173          eTraces <- explore prog funcDef [("y", QBE.Long), ("x", QBE.Word)]
174
175          branchPoints eTraces @?= [[False], [True, False], [True, True]]
176    ]