quebex

  1-- SPDX-FileCopyrightText: 2025-2026 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.Bifunctor (second)
  8import Data.List (partition, sort, uncons)
  9import Data.Map qualified as Map
 10import Data.Maybe (fromJust, isJust)
 11import Language.QBE (Program, parseAndFind)
 12import Language.QBE.Backend.Store qualified as ST
 13import Language.QBE.Simulator.Concolic.State (mkEnv)
 14import Language.QBE.Simulator.Default.Expression qualified as DE
 15import Language.QBE.Simulator.Explorer
 16  ( PathResult (..),
 17    defSolver,
 18    exploreFunc,
 19    newEngine,
 20  )
 21import Language.QBE.Types qualified as QBE
 22import System.FilePath ((</>))
 23import Test.Tasty
 24import Test.Tasty.HUnit
 25
 26branchPoints :: [PathResult] -> [[Bool]]
 27branchPoints lst = sort $ map (\(PathResult _ t _) -> map fst t) lst
 28
 29findAssign :: [PathResult] -> [Bool] -> Maybe ST.Assign
 30findAssign [] _ = Nothing
 31findAssign ((PathResult _ eTrace a) : xs) toFind
 32  | map fst eTrace == toFind = Just a
 33  | otherwise = findAssign xs toFind
 34
 35explore' :: Program -> QBE.FuncDef -> [(String, QBE.BaseType)] -> IO [PathResult]
 36explore' prog entry params = do
 37  defEnv <- mkEnv prog 0 128 Nothing
 38  engine <- newEngine defEnv <$> defSolver
 39
 40  exploreFunc engine entry $ map (second QBE.Base) params
 41
 42getFuncAndProg :: FilePath -> QBE.GlobalIdent -> IO (Program, QBE.FuncDef)
 43getFuncAndProg fileName funcName =
 44  let filePath = "test" </> "testdata" </> fileName
 45   in readFile filePath >>= parseAndFind funcName
 46
 47------------------------------------------------------------------------
 48
 49exploreTests :: TestTree
 50exploreTests =
 51  testGroup
 52    "Tests for Symbolic Program Exploration"
 53    [ testCase "Explore' program with four execution paths" $
 54        do
 55          let qbe =
 56                "function $branchOnInput(w %cond1, w %cond2) {\n\
 57                \@jump.1\n\
 58                \jnz %cond1, @branch.1, @branch.2\n\
 59                \@branch.1\n\
 60                \jmp @jump.2\n\
 61                \@branch.2\n\
 62                \jmp @jump.2\n\
 63                \@jump.2\n\
 64                \jnz %cond2, @branch.3, @branch.4\n\
 65                \@branch.3\n\
 66                \ret\n\
 67                \@branch.4\n\
 68                \ret\n\
 69                \}"
 70
 71          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchOnInput") qbe
 72          eTraces <- explore' prog funcDef [("cond1", QBE.Word), ("cond2", QBE.Word)]
 73
 74          let branches = branchPoints eTraces
 75          branches @?= [[False, False], [False, True], [True, False], [True, True]],
 76      testCase "Unsatisfiable branches" $
 77        do
 78          let qbe =
 79                "function $branchOnInput(w %cond1) {\n\
 80                \@jump.1\n\
 81                \jnz %cond1, @branch.1, @branch.2\n\
 82                \@branch.1\n\
 83                \jmp @jump.2\n\
 84                \@branch.2\n\
 85                \jmp @jump.2\n\
 86                \@jump.2\n\
 87                \jnz %cond1, @branch.3, @branch.4\n\
 88                \@branch.3\n\
 89                \ret\n\
 90                \@branch.4\n\
 91                \ret\n\
 92                \}"
 93
 94          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchOnInput") qbe
 95          eTraces <- explore' prog funcDef [("cond1", QBE.Word)]
 96
 97          let branches = branchPoints eTraces
 98          branches @?= [[False, False], [True, True]],
 99      testCase "Branch with overflow arithmetics" $
100        do
101          let qbe =
102                "function $branchArithmetics(w %input) {\n\
103                \@start\n\
104                \%cond =w add %input, 1\n\
105                \jnz %input, @branch.1, @branch.2\n\
106                \@branch.1\n\
107                \ret\n\
108                \@branch.2\n\
109                \ret\n\
110                \}"
111
112          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchArithmetics") qbe
113          eTraces <- explore' prog funcDef [("input", QBE.Word)]
114
115          let branches = branchPoints eTraces
116          branches @?= [[False], [True]]
117
118          let assign = fromJust $ findAssign eTraces [False]
119          Map.lookup "input" assign @?= Just (DE.VWord 0),
120      testCase "Store symbolic value and memory, load it and pass it to function" $
121        do
122          let qbe =
123                "function $branchOnInput(w %cond1) {\n\
124                \@jump.1\n\
125                \jnz %cond1, @branch.1, @branch.2\n\
126                \@branch.1\n\
127                \jmp @jump.2\n\
128                \@branch.2\n\
129                \jmp @jump.2\n\
130                \@jump.2\n\
131                \jnz %cond1, @branch.3, @branch.4\n\
132                \@branch.3\n\
133                \ret\n\
134                \@branch.4\n\
135                \ret\n\
136                \}\n\
137                \function $entry(w %in) {\n\
138                \@start\n\
139                \%a =l alloc4 4\n\
140                \storew %in, %a\n\
141                \%l =w loadw %a\n\
142                \call $branchOnInput(w %l)\n\
143                \ret\n\
144                \}"
145
146          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "entry") qbe
147          eTraces <- explore' prog funcDef [("x", QBE.Word)]
148
149          let branches = branchPoints eTraces
150          branches @?= [[False, False], [True, True]],
151      testCase "Branch on a specific concrete 64-bit value" $
152        do
153          let qbe =
154                "function $f(l %input.0) {\n\
155                \@start\n\
156                \%input.1 =l sub %input.0, 42\n\
157                \jnz %input.1, @not42, @is42\n\
158                \@not42\n\
159                \ret\n\
160                \@is42\n\
161                \ret\n\
162                \}"
163
164          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "f") qbe
165          eTraces <- explore' prog funcDef [("y", QBE.Long)]
166
167          branchPoints eTraces @?= [[False], [True]]
168          let assign = fromJust $ findAssign eTraces [False]
169          Map.lookup "y" assign @?= Just (DE.VLong 42),
170      testCase "Branching with subtyping" $
171        do
172          let qbe =
173                "function $f(l %input.0, w %input.1) {\n\
174                \@start\n\
175                \%added =w add %input.1, 1\n\
176                \%subed =w sub %added, %input.1\n\
177                \%result =w add %added, %subed\n\
178                \jnz %result, @b1, @b2\n\
179                \@b1\n\
180                \jnz %input.0, @b2, @b2\n\
181                \@b2\n\
182                \ret\n\
183                \}"
184
185          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "f") qbe
186          eTraces <- explore' prog funcDef [("y", QBE.Long), ("x", QBE.Word)]
187
188          branchPoints eTraces @?= [[False], [True, False], [True, True]],
189      testCase "make a single word symbolic" $
190        do
191          let qbe =
192                "data $name = align 1 {  b \"abcd\", b 0 }\n\
193                \function w $main() {\n\
194                \@start\n\
195                \%ptr =l alloc4 4\n\
196                \call $quebex_make_symbolic(l %ptr, l 1, l 4, l $name)\n\
197                \%word =w loadw %ptr\n\
198                \jnz %word, @b1, @b2\n\
199                \@b1\n\
200                \ret 0\n\
201                \@b2\n\
202                \ret 1\n\
203                \}"
204
205          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "main") qbe
206          eTraces <- explore' prog funcDef []
207
208          length eTraces @?= 2,
209      testCase "make a range of memory symbolic" $
210        do
211          let qbe =
212                "data $name = align 1 {  b \"array\", b 0 }\n\
213                \function w $main() {\n\
214                \@start\n\
215                \%ptr =l alloc4 32\n\
216                \call $quebex_make_symbolic(l %ptr, l 8, l 4, l $name)\n\
217                \%word =w loadw %ptr\n\
218                \jnz %word, @b1, @b2\n\
219                \@b1\n\
220                \%ptr =l add %ptr, 4\n\
221                \%word =w loadw %ptr\n\
222                \jnz %word, @b3, @b4\n\
223                \@b2\n\
224                \ret 1\n\
225                \@b3\n\
226                \ret 0\n\
227                \@b4\n\
228                \ret 1\n\
229                \}"
230
231          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "main") qbe
232          eTraces <- explore' prog funcDef []
233
234          length eTraces @?= 3,
235      testCase "explore a path with an error case" $
236        do
237          let qbe =
238                "data $.Lstring.1 = align 1 { b \"a\", b 0 }\n\
239                \export\n\
240                \function w $main() {\n\
241                \@body\n\
242                \%.1 =l alloc4 4\n\
243                \call $quebex_make_symbolic(l %.1, l 1, l 4, l $.Lstring.1)\n\
244                \%.2 =w loadw %.1\n\
245                \%.3 =w ceqw %.2, 42\n\
246                \jnz %.3, @error, @okay\n\
247                \@error\n\
248                \hlt\n\
249                \@okay\n\
250                \ret 0\n\
251                \}"
252
253          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "main") qbe
254          (wErr, woErr) <-
255            partition (isJust . pathErr)
256              <$> explore' prog funcDef []
257
258          length wErr @?= 1
259          length woErr @?= 1
260
261          let errorVars = pathVars $ fst $ fromJust $ uncons wErr
262              errorVal = Map.lookup "a1" errorVars
263          errorVal @?= Just (DE.VWord 42),
264      testCase "explore program with multiple paths to error" $
265        do
266          (prog, funcDef) <-
267            getFuncAndProg
268              "insertion-sort-error-on-42.qbe"
269              (QBE.GlobalIdent "main")
270          (wErr, woErr) <-
271            partition (isJust . pathErr)
272              <$> explore' prog funcDef []
273
274          length wErr @?= 8
275          length woErr @?= 6
276
277          -- every path on the error case must contain 42 in its input.
278          let vals = map (Map.elems . pathVars) wErr
279          let has42 = elem (DE.VWord 42)
280          length (filter has42 vals) @?= length wErr,
281      testCase "continue exploration after single path to error" $
282        do
283          (prog, funcDef) <-
284            getFuncAndProg
285              "single-error-case.qbe"
286              (QBE.GlobalIdent "main")
287          (wErr, woErr) <-
288            partition (isJust . pathErr)
289              <$> explore' prog funcDef []
290
291          length wErr @?= 1
292          length woErr @?= 20
293
294          let errorVars = pathVars $ fst $ fromJust $ uncons wErr
295              errorVal = Map.lookup "prime1" errorVars
296          errorVal @?= Just (DE.VWord 43),
297      testCase "exploration with memory error" $
298        do
299          (prog, funcDef) <-
300            getFuncAndProg
301              "out-of-bounds-error.qbe"
302              (QBE.GlobalIdent "main")
303          (wErr, woErr) <-
304            partition (isJust . pathErr)
305              <$> explore' prog funcDef []
306
307          length wErr @?= 1
308          length woErr @?= 3
309
310          let errorVars = pathVars $ fst $ fromJust $ uncons wErr
311              errorVal = Map.lookup "a1" errorVars
312          errorVal @?= Just (DE.VWord 0x23523929)
313    ]