1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>2--3-- SPDX-License-Identifier: GPL-3.0-only45module Explorer (exploreTests) where67import Data.Bifunctor (second)8import Data.List (sort)9import Data.Map qualified as Map10import Data.Maybe (fromJust)11import Language.QBE (Program, parseAndFind)12import Language.QBE.Backend.Store qualified as ST13import Language.QBE.Backend.Tracer qualified as T14import Language.QBE.Simulator.Concolic.State (mkEnv)15import Language.QBE.Simulator.Default.Expression qualified as DE16import Language.QBE.Simulator.Explorer (defSolver, explore, newEngine)17import Language.QBE.Types qualified as QBE18import Test.Tasty19import Test.Tasty.HUnit2021branchPoints :: [(ST.Assign, T.ExecTrace)] -> [[Bool]]22branchPoints lst = sort $ map (\(_, t) -> map fst t) lst2324findAssign :: [(ST.Assign, T.ExecTrace)] -> [Bool] -> Maybe ST.Assign25findAssign [] _ = Nothing26findAssign ((a, eTrace) : xs) toFind27 | map fst eTrace == toFind = Just a28 | otherwise = findAssign xs toFind2930explore' :: Program -> QBE.FuncDef -> [(String, QBE.BaseType)] -> IO [(ST.Assign, T.ExecTrace)]31explore' prog entry params = do32 engine <- newEngine <$> defSolver33 defEnv <- mkEnv prog 0 128 Nothing3435 explore engine defEnv entry $36 map (second QBE.Base) params3738------------------------------------------------------------------------3940exploreTests :: TestTree41exploreTests =42 testGroup43 "Tests for Symbolic Program Exploration"44 [ testCase "Explore' program with four execution paths" $45 do46 let qbe =47 "function $branchOnInput(w %cond1, w %cond2) {\n\48 \@jump.1\n\49 \jnz %cond1, @branch.1, @branch.2\n\50 \@branch.1\n\51 \jmp @jump.2\n\52 \@branch.2\n\53 \jmp @jump.2\n\54 \@jump.2\n\55 \jnz %cond2, @branch.3, @branch.4\n\56 \@branch.3\n\57 \ret\n\58 \@branch.4\n\59 \ret\n\60 \}"6162 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchOnInput") qbe63 eTraces <- explore' prog funcDef [("cond1", QBE.Word), ("cond2", QBE.Word)]6465 let branches = branchPoints eTraces66 branches @?= [[False, False], [False, True], [True, False], [True, True]],67 testCase "Unsatisfiable branches" $68 do69 let qbe =70 "function $branchOnInput(w %cond1) {\n\71 \@jump.1\n\72 \jnz %cond1, @branch.1, @branch.2\n\73 \@branch.1\n\74 \jmp @jump.2\n\75 \@branch.2\n\76 \jmp @jump.2\n\77 \@jump.2\n\78 \jnz %cond1, @branch.3, @branch.4\n\79 \@branch.3\n\80 \ret\n\81 \@branch.4\n\82 \ret\n\83 \}"8485 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchOnInput") qbe86 eTraces <- explore' prog funcDef [("cond1", QBE.Word)]8788 let branches = branchPoints eTraces89 branches @?= [[False, False], [True, True]],90 testCase "Branch with overflow arithmetics" $91 do92 let qbe =93 "function $branchArithmetics(w %input) {\n\94 \@start\n\95 \%cond =w add %input, 1\n\96 \jnz %input, @branch.1, @branch.2\n\97 \@branch.1\n\98 \ret\n\99 \@branch.2\n\100 \ret\n\101 \}"102103 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchArithmetics") qbe104 eTraces <- explore' prog funcDef [("input", QBE.Word)]105106 let branches = branchPoints eTraces107 branches @?= [[False], [True]]108109 let assign = fromJust $ findAssign eTraces [False]110 Map.lookup "input" assign @?= Just (DE.VWord 0),111 testCase "Store symbolic value and memory, load it and pass it to function" $112 do113 let qbe =114 "function $branchOnInput(w %cond1) {\n\115 \@jump.1\n\116 \jnz %cond1, @branch.1, @branch.2\n\117 \@branch.1\n\118 \jmp @jump.2\n\119 \@branch.2\n\120 \jmp @jump.2\n\121 \@jump.2\n\122 \jnz %cond1, @branch.3, @branch.4\n\123 \@branch.3\n\124 \ret\n\125 \@branch.4\n\126 \ret\n\127 \}\n\128 \function $entry(w %in) {\n\129 \@start\n\130 \%a =l alloc4 4\n\131 \storew %in, %a\n\132 \%l =w loadw %a\n\133 \call $branchOnInput(w %l)\n\134 \ret\n\135 \}"136137 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "entry") qbe138 eTraces <- explore' prog funcDef [("x", QBE.Word)]139140 let branches = branchPoints eTraces141 branches @?= [[False, False], [True, True]],142 testCase "Branch on a specific concrete 64-bit value" $143 do144 let qbe =145 "function $f(l %input.0) {\n\146 \@start\n\147 \%input.1 =l sub %input.0, 42\n\148 \jnz %input.1, @not42, @is42\n\149 \@not42\n\150 \ret\n\151 \@is42\n\152 \ret\n\153 \}"154155 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "f") qbe156 eTraces <- explore' prog funcDef [("y", QBE.Long)]157158 branchPoints eTraces @?= [[False], [True]]159 let assign = fromJust $ findAssign eTraces [False]160 Map.lookup "y" assign @?= Just (DE.VLong 42),161 testCase "Branching with subtyping" $162 do163 let qbe =164 "function $f(l %input.0, w %input.1) {\n\165 \@start\n\166 \%added =w add %input.1, 1\n\167 \%subed =w sub %added, %input.1\n\168 \%result =w add %added, %subed\n\169 \jnz %result, @b1, @b2\n\170 \@b1\n\171 \jnz %input.0, @b2, @b2\n\172 \@b2\n\173 \ret\n\174 \}"175176 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "f") qbe177 eTraces <- explore' prog funcDef [("y", QBE.Long), ("x", QBE.Word)]178179 branchPoints eTraces @?= [[False], [True, False], [True, True]],180 testCase "make a single word symbolic" $181 do182 let qbe =183 "data $name = align 1 { b \"abcd\", b 0 }\n\184 \function w $main() {\n\185 \@start\n\186 \%ptr =l alloc4 4\n\187 \call $quebex_symbolic_array(l %ptr, l 1, l 4, l $name)\n\188 \%word =w loadw %ptr\n\189 \jnz %word, @b1, @b2\n\190 \@b1\n\191 \ret 0\n\192 \@b2\n\193 \ret 1\n\194 \}"195196 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "main") qbe197 eTraces <- explore' prog funcDef []198199 length eTraces @?= 2,200 testCase "make a range of memory symbolic" $201 do202 let qbe =203 "data $name = align 1 { b \"array\", b 0 }\n\204 \function w $main() {\n\205 \@start\n\206 \%ptr =l alloc4 32\n\207 \call $quebex_symbolic_array(l %ptr, l 8, l 4, l $name)\n\208 \%word =w loadw %ptr\n\209 \jnz %word, @b1, @b2\n\210 \@b1\n\211 \%ptr =l add %ptr, 4\n\212 \%word =w loadw %ptr\n\213 \jnz %word, @b3, @b4\n\214 \@b2\n\215 \ret 1\n\216 \@b3\n\217 \ret 0\n\218 \@b4\n\219 \ret 1\n\220 \}"221222 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "main") qbe223 eTraces <- explore' prog funcDef []224225 length eTraces @?= 3226 ]