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.Backend.Tracer qualified as T
 12import Language.QBE.Simulator.Default.Expression qualified as DE
 13import Language.QBE.Types qualified as QBE
 14import Test.Tasty
 15import Test.Tasty.HUnit
 16import Util
 17
 18branchPoints :: [(ST.Assign, T.ExecTrace)] -> [[Bool]]
 19branchPoints lst = sort $ map (\(_, t) -> map fst t) lst
 20
 21findAssign :: [(ST.Assign, T.ExecTrace)] -> [Bool] -> Maybe ST.Assign
 22findAssign [] _ = Nothing
 23findAssign ((a, eTrace) : xs) toFind
 24  | map fst eTrace == toFind = Just a
 25  | otherwise = findAssign xs toFind
 26
 27------------------------------------------------------------------------
 28
 29exploreTests :: TestTree
 30exploreTests =
 31  testGroup
 32    "Tests for Symbolic Program Exploration"
 33    [ testCase "Explore' program with four execution paths" $
 34        do
 35          prog <-
 36            parseProg
 37              "function $branchOnInput(w %cond1, w %cond2) {\n\
 38              \@jump.1\n\
 39              \jnz %cond1, @branch.1, @branch.2\n\
 40              \@branch.1\n\
 41              \jmp @jump.2\n\
 42              \@branch.2\n\
 43              \jmp @jump.2\n\
 44              \@jump.2\n\
 45              \jnz %cond2, @branch.3, @branch.4\n\
 46              \@branch.3\n\
 47              \ret\n\
 48              \@branch.4\n\
 49              \ret\n\
 50              \}"
 51
 52          let funcDef = findFunc prog (QBE.GlobalIdent "branchOnInput")
 53          eTraces <- explore' prog funcDef [("cond1", QBE.Word), ("cond2", QBE.Word)]
 54
 55          let branches = branchPoints eTraces
 56          branches @?= [[False, False], [False, True], [True, False], [True, True]],
 57      testCase "Unsatisfiable branches" $
 58        do
 59          prog <-
 60            parseProg
 61              "function $branchOnInput(w %cond1) {\n\
 62              \@jump.1\n\
 63              \jnz %cond1, @branch.1, @branch.2\n\
 64              \@branch.1\n\
 65              \jmp @jump.2\n\
 66              \@branch.2\n\
 67              \jmp @jump.2\n\
 68              \@jump.2\n\
 69              \jnz %cond1, @branch.3, @branch.4\n\
 70              \@branch.3\n\
 71              \ret\n\
 72              \@branch.4\n\
 73              \ret\n\
 74              \}"
 75
 76          let funcDef = findFunc prog (QBE.GlobalIdent "branchOnInput")
 77          eTraces <- explore' prog funcDef [("cond1", QBE.Word)]
 78
 79          let branches = branchPoints eTraces
 80          branches @?= [[False, False], [True, True]],
 81      testCase "Branch with overflow arithmetics" $
 82        do
 83          prog <-
 84            parseProg
 85              "function $branchArithmetics(w %input) {\n\
 86              \@start\n\
 87              \%cond =w add %input, 1\n\
 88              \jnz %input, @branch.1, @branch.2\n\
 89              \@branch.1\n\
 90              \ret\n\
 91              \@branch.2\n\
 92              \ret\n\
 93              \}"
 94
 95          let funcDef = findFunc prog (QBE.GlobalIdent "branchArithmetics")
 96          eTraces <- explore' prog funcDef [("input", QBE.Word)]
 97
 98          let branches = branchPoints eTraces
 99          branches @?= [[False], [True]]
100
101          let assign = fromJust $ findAssign eTraces [False]
102          Map.lookup "input" assign @?= Just (DE.VWord 0),
103      testCase "Store symbolic value and memory, load it and pass it to function" $
104        do
105          prog <-
106            parseProg
107              "function $branchOnInput(w %cond1) {\n\
108              \@jump.1\n\
109              \jnz %cond1, @branch.1, @branch.2\n\
110              \@branch.1\n\
111              \jmp @jump.2\n\
112              \@branch.2\n\
113              \jmp @jump.2\n\
114              \@jump.2\n\
115              \jnz %cond1, @branch.3, @branch.4\n\
116              \@branch.3\n\
117              \ret\n\
118              \@branch.4\n\
119              \ret\n\
120              \}\n\
121              \function $entry(w %in) {\n\
122              \@start\n\
123              \%a =l alloc4 4\n\
124              \storew %in, %a\n\
125              \%l =w loadw %a\n\
126              \call $branchOnInput(w %l)\n\
127              \ret\n\
128              \}"
129
130          let funcDef = findFunc prog (QBE.GlobalIdent "entry")
131          eTraces <- explore' prog funcDef [("x", QBE.Word)]
132
133          let branches = branchPoints eTraces
134          branches @?= [[False, False], [True, True]],
135      testCase "Branch on a specific concrete 64-bit value" $
136        do
137          prog <-
138            parseProg
139              "function $f(l %input.0) {\n\
140              \@start\n\
141              \%input.1 =l sub %input.0, 42\n\
142              \jnz %input.1, @not42, @is42\n\
143              \@not42\n\
144              \ret\n\
145              \@is42\n\
146              \ret\n\
147              \}"
148
149          let funcDef = findFunc prog (QBE.GlobalIdent "f")
150          eTraces <- explore' prog funcDef [("y", QBE.Long)]
151
152          branchPoints eTraces @?= [[False], [True]]
153          let assign = fromJust $ findAssign eTraces [False]
154          Map.lookup "y" assign @?= Just (DE.VLong 42),
155      testCase "Branching with subtyping" $
156        do
157          prog <-
158            parseProg
159              "function $f(l %input.0, w %input.1) {\n\
160              \@start\n\
161              \%added =w add %input.1, 1\n\
162              \%subed =w sub %added, %input.1\n\
163              \%result =w add %added, %subed\n\
164              \jnz %result, @b1, @b2\n\
165              \@b1\n\
166              \jnz %input.0, @b2, @b2\n\
167              \@b2\n\
168              \ret\n\
169              \}"
170
171          let funcDef = findFunc prog (QBE.GlobalIdent "f")
172          eTraces <- explore' prog funcDef [("y", QBE.Long), ("x", QBE.Word)]
173
174          branchPoints eTraces @?= [[False], [True, False], [True, True]],
175      testCase "make a single word symbolic" $
176        do
177          prog <-
178            parseProg
179              "data $name = align 1 {  b \"abcd\", b 0 }\n\
180              \function w $main() {\n\
181              \@start\n\
182              \%ptr =l alloc4 4\n\
183              \call $quebex_symbolic_array(l %ptr, l 1, l 4, l $name)\n\
184              \%word =w loadw %ptr\n\
185              \jnz %word, @b1, @b2\n\
186              \@b1\n\
187              \ret 0\n\
188              \@b2\n\
189              \ret 1\n\
190              \}"
191
192          let funcDef = findFunc prog (QBE.GlobalIdent "main")
193          eTraces <- explore' prog funcDef []
194
195          length eTraces @?= 2,
196      testCase "make a range of memory symbolic" $
197        do
198          prog <-
199            parseProg
200              "data $name = align 1 {  b \"array\", b 0 }\n\
201              \function w $main() {\n\
202              \@start\n\
203              \%ptr =l alloc4 32\n\
204              \call $quebex_symbolic_array(l %ptr, l 8, l 4, l $name)\n\
205              \%word =w loadw %ptr\n\
206              \jnz %word, @b1, @b2\n\
207              \@b1\n\
208              \%ptr =l add %ptr, 4\n\
209              \%word =w loadw %ptr\n\
210              \jnz %word, @b3, @b4\n\
211              \@b2\n\
212              \ret 1\n\
213              \@b3\n\
214              \ret 0\n\
215              \@b4\n\
216              \ret 1\n\
217              \}"
218
219          let funcDef = findFunc prog (QBE.GlobalIdent "main")
220          eTraces <- explore' prog funcDef []
221
222          length eTraces @?= 3
223    ]