quebex

  1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
  2--
  3-- SPDX-License-Identifier: GPL-3.0-only
  4
  5module Backend (backendTests) where
  6
  7import Data.Maybe (fromJust)
  8import Language.QBE.Backend.DFS (findUnexplored, newPathSel, trackTrace)
  9import Language.QBE.Backend.Model qualified as Model
 10import Language.QBE.Backend.Store qualified as ST
 11import Language.QBE.Backend.Tracer qualified as T
 12import Language.QBE.Simulator.Concolic.Expression qualified as CE
 13import Language.QBE.Simulator.Default.Expression qualified as DE
 14import Language.QBE.Simulator.Explorer (defSolver)
 15import Language.QBE.Simulator.Symbolic.Expression qualified as SE
 16import Language.QBE.Types qualified as QBE
 17import System.Random (initStdGen)
 18import Test.Tasty
 19import Test.Tasty.HUnit
 20import Util
 21
 22storeTests :: TestTree
 23storeTests =
 24  testGroup
 25    "Tests for the Variable Store"
 26    [ testCase "finalize never forgets defined variables" $
 27        do
 28          s0 <- ST.empty <$> initStdGen
 29          solver <- defSolver
 30
 31          let s1 = fst $ ST.getConcolic s0 "a" (QBE.Base QBE.Word)
 32          s2 <- ST.finalize solver s1
 33
 34          let s3 = fst $ ST.getConcolic s2 "b" (QBE.Base QBE.Word)
 35          s4 <- ST.finalize solver s3
 36
 37          -- The 'a' variable returns, but should still be known.
 38          -- There used to be a bug where this caused an exception.
 39          let s5 = fst $ ST.getConcolic s4 "a" (QBE.Base QBE.Word)
 40          _ <- ST.finalize solver s5
 41
 42          assertBool "finalize does not throw an exception" True
 43    ]
 44
 45traceTests :: TestTree
 46traceTests =
 47  testGroup
 48    "Tests for the Symbolic Tracer"
 49    [ testCase "Branch tracing with single concrete branch" $
 50        do
 51          t <-
 52            parseAndExec
 53              (QBE.GlobalIdent "main")
 54              []
 55              "function $main() {\n\
 56              \@start.1\n\
 57              \%cond =w add 0, 1\n\
 58              \jnz %cond, @branch.1, @branch.2\n\
 59              \@branch.1\n\
 60              \ret\n\
 61              \@branch.2\n\
 62              \ret\n\
 63              \}"
 64
 65          -- Trace must be empty because it doesn't branch on symbolic values.
 66          length t @?= 0,
 67      testCase "Branch tracing and solving with single symbolic branch" $
 68        do
 69          s <- defSolver
 70          c <- unconstrained s 0 "input" QBE.Word
 71          assertBool "created value is symbolic" $ CE.hasSymbolic c
 72          let inputs = [(SE.toSExpr . fromJust . CE.symbolic) c]
 73
 74          t <-
 75            parseAndExec
 76              (QBE.GlobalIdent "branchOnInput")
 77              [c]
 78              "function $branchOnInput(w %cond) {\n\
 79              \@start.1\n\
 80              \jnz %cond, @branch.1, @branch.2\n\
 81              \@branch.1\n\
 82              \ret\n\
 83              \@branch.2\n\
 84              \ret\n\
 85              \}"
 86
 87          t @?= [(False, T.newBranch (fromJust $ CE.symbolic c))]
 88
 89          let pathSel = trackTrace newPathSel t
 90          (mm, nextPathSel) <- findUnexplored s inputs pathSel
 91
 92          let assign = Model.toList (fromJust mm)
 93          case assign of
 94            [(_, DE.VWord v)] ->
 95              assertBool "condition must be /= 0" (v /= 0)
 96            _ -> assertFailure "unexpected model"
 97
 98          -- There are only two branches: input == 0 and input /= 0
 99          (nxt, _) <- findUnexplored s inputs nextPathSel
100          nxt @?= Nothing,
101      testCase "Tracing with multiple branches" $
102        do
103          s <- defSolver
104          c1 <- unconstrained s 0 "cond1" QBE.Word
105          c2 <- unconstrained s 0 "cond2" QBE.Word
106
107          t <-
108            parseAndExec
109              (QBE.GlobalIdent "branchOnInput")
110              [c1, c2]
111              "function $branchOnInput(w %cond1, w %cond2) {\n\
112              \@jump.1\n\
113              \jnz %cond1, @branch.1, @branch.2\n\
114              \@branch.1\n\
115              \jmp @jump.2\n\
116              \@branch.2\n\
117              \jmp @jump.2\n\
118              \@jump.2\n\
119              \jnz %cond2, @branch.3, @branch.4\n\
120              \@branch.3\n\
121              \ret\n\
122              \@branch.4\n\
123              \ret\n\
124              \}"
125
126          length t @?= 2
127    ]
128
129backendTests :: TestTree
130backendTests =
131  testGroup
132    "Tests for the Symbolic Data Structures"
133    [storeTests, traceTests]