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, exploreFunc, 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 defEnv <- mkEnv prog 0 128 Nothing33 engine <- newEngine defEnv <$> defSolver3435 exploreFunc engine entry $ map (second QBE.Base) params3637------------------------------------------------------------------------3839exploreTests :: TestTree40exploreTests =41 testGroup42 "Tests for Symbolic Program Exploration"43 [ testCase "Explore' program with four execution paths" $44 do45 let qbe =46 "function $branchOnInput(w %cond1, w %cond2) {\n\47 \@jump.1\n\48 \jnz %cond1, @branch.1, @branch.2\n\49 \@branch.1\n\50 \jmp @jump.2\n\51 \@branch.2\n\52 \jmp @jump.2\n\53 \@jump.2\n\54 \jnz %cond2, @branch.3, @branch.4\n\55 \@branch.3\n\56 \ret\n\57 \@branch.4\n\58 \ret\n\59 \}"6061 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchOnInput") qbe62 eTraces <- explore' prog funcDef [("cond1", QBE.Word), ("cond2", QBE.Word)]6364 let branches = branchPoints eTraces65 branches @?= [[False, False], [False, True], [True, False], [True, True]],66 testCase "Unsatisfiable branches" $67 do68 let qbe =69 "function $branchOnInput(w %cond1) {\n\70 \@jump.1\n\71 \jnz %cond1, @branch.1, @branch.2\n\72 \@branch.1\n\73 \jmp @jump.2\n\74 \@branch.2\n\75 \jmp @jump.2\n\76 \@jump.2\n\77 \jnz %cond1, @branch.3, @branch.4\n\78 \@branch.3\n\79 \ret\n\80 \@branch.4\n\81 \ret\n\82 \}"8384 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchOnInput") qbe85 eTraces <- explore' prog funcDef [("cond1", QBE.Word)]8687 let branches = branchPoints eTraces88 branches @?= [[False, False], [True, True]],89 testCase "Branch with overflow arithmetics" $90 do91 let qbe =92 "function $branchArithmetics(w %input) {\n\93 \@start\n\94 \%cond =w add %input, 1\n\95 \jnz %input, @branch.1, @branch.2\n\96 \@branch.1\n\97 \ret\n\98 \@branch.2\n\99 \ret\n\100 \}"101102 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchArithmetics") qbe103 eTraces <- explore' prog funcDef [("input", QBE.Word)]104105 let branches = branchPoints eTraces106 branches @?= [[False], [True]]107108 let assign = fromJust $ findAssign eTraces [False]109 Map.lookup "input" assign @?= Just (DE.VWord 0),110 testCase "Store symbolic value and memory, load it and pass it to function" $111 do112 let qbe =113 "function $branchOnInput(w %cond1) {\n\114 \@jump.1\n\115 \jnz %cond1, @branch.1, @branch.2\n\116 \@branch.1\n\117 \jmp @jump.2\n\118 \@branch.2\n\119 \jmp @jump.2\n\120 \@jump.2\n\121 \jnz %cond1, @branch.3, @branch.4\n\122 \@branch.3\n\123 \ret\n\124 \@branch.4\n\125 \ret\n\126 \}\n\127 \function $entry(w %in) {\n\128 \@start\n\129 \%a =l alloc4 4\n\130 \storew %in, %a\n\131 \%l =w loadw %a\n\132 \call $branchOnInput(w %l)\n\133 \ret\n\134 \}"135136 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "entry") qbe137 eTraces <- explore' prog funcDef [("x", QBE.Word)]138139 let branches = branchPoints eTraces140 branches @?= [[False, False], [True, True]],141 testCase "Branch on a specific concrete 64-bit value" $142 do143 let qbe =144 "function $f(l %input.0) {\n\145 \@start\n\146 \%input.1 =l sub %input.0, 42\n\147 \jnz %input.1, @not42, @is42\n\148 \@not42\n\149 \ret\n\150 \@is42\n\151 \ret\n\152 \}"153154 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "f") qbe155 eTraces <- explore' prog funcDef [("y", QBE.Long)]156157 branchPoints eTraces @?= [[False], [True]]158 let assign = fromJust $ findAssign eTraces [False]159 Map.lookup "y" assign @?= Just (DE.VLong 42),160 testCase "Branching with subtyping" $161 do162 let qbe =163 "function $f(l %input.0, w %input.1) {\n\164 \@start\n\165 \%added =w add %input.1, 1\n\166 \%subed =w sub %added, %input.1\n\167 \%result =w add %added, %subed\n\168 \jnz %result, @b1, @b2\n\169 \@b1\n\170 \jnz %input.0, @b2, @b2\n\171 \@b2\n\172 \ret\n\173 \}"174175 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "f") qbe176 eTraces <- explore' prog funcDef [("y", QBE.Long), ("x", QBE.Word)]177178 branchPoints eTraces @?= [[False], [True, False], [True, True]],179 testCase "make a single word symbolic" $180 do181 let qbe =182 "data $name = align 1 { b \"abcd\", b 0 }\n\183 \function w $main() {\n\184 \@start\n\185 \%ptr =l alloc4 4\n\186 \call $quebex_make_symbolic(l %ptr, l 1, l 4, l $name)\n\187 \%word =w loadw %ptr\n\188 \jnz %word, @b1, @b2\n\189 \@b1\n\190 \ret 0\n\191 \@b2\n\192 \ret 1\n\193 \}"194195 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "main") qbe196 eTraces <- explore' prog funcDef []197198 length eTraces @?= 2,199 testCase "make a range of memory symbolic" $200 do201 let qbe =202 "data $name = align 1 { b \"array\", b 0 }\n\203 \function w $main() {\n\204 \@start\n\205 \%ptr =l alloc4 32\n\206 \call $quebex_make_symbolic(l %ptr, l 8, l 4, l $name)\n\207 \%word =w loadw %ptr\n\208 \jnz %word, @b1, @b2\n\209 \@b1\n\210 \%ptr =l add %ptr, 4\n\211 \%word =w loadw %ptr\n\212 \jnz %word, @b3, @b4\n\213 \@b2\n\214 \ret 1\n\215 \@b3\n\216 \ret 0\n\217 \@b4\n\218 \ret 1\n\219 \}"220221 (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "main") qbe222 eTraces <- explore' prog funcDef []223224 length eTraces @?= 3225 ]