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.Simulator.Concolic.Expression qualified as CE
 11import Language.QBE.Simulator.Default.Expression qualified as DE
 12import Language.QBE.Simulator.Explorer (z3Solver)
 13import Language.QBE.Simulator.Symbolic.Expression qualified as SE
 14import Language.QBE.Simulator.Symbolic.Tracer qualified as ST
 15import Language.QBE.Types qualified as QBE
 16import Test.Tasty
 17import Test.Tasty.HUnit
 18import Util
 19
 20traceTests :: TestTree
 21traceTests =
 22  testGroup
 23    "Tests for the Symbolic Tracer"
 24    [ testCase "Branch tracing with single concrete branch" $
 25        do
 26          t <-
 27            parseAndExec
 28              (QBE.GlobalIdent "main")
 29              []
 30              "function $main() {\n\
 31              \@start.1\n\
 32              \%cond =w add 0, 1\n\
 33              \jnz %cond, @branch.1, @branch.2\n\
 34              \@branch.1\n\
 35              \ret\n\
 36              \@branch.2\n\
 37              \ret\n\
 38              \}"
 39
 40          -- Trace must be empty because it doesn't branch on symbolic values.
 41          length t @?= 0,
 42      testCase "Branch tracing and solving with single symbolic branch" $
 43        do
 44          s <- z3Solver
 45          c <- unconstrained s 0 "input" QBE.Word
 46          assertBool "created value is symbolic" $ CE.hasSymbolic c
 47          let inputs = map (SE.toSExpr . fromJust . CE.symbolic) [c]
 48
 49          t <-
 50            parseAndExec
 51              (QBE.GlobalIdent "branchOnInput")
 52              [c]
 53              "function $branchOnInput(w %cond) {\n\
 54              \@start.1\n\
 55              \jnz %cond, @branch.1, @branch.2\n\
 56              \@branch.1\n\
 57              \ret\n\
 58              \@branch.2\n\
 59              \ret\n\
 60              \}"
 61
 62          t @?= [(False, ST.newBranch (fromJust $ CE.symbolic c))]
 63
 64          let pathSel = trackTrace newPathSel t
 65          (mm, nextPathSel) <- findUnexplored s inputs pathSel
 66
 67          assign <- Model.toList (fromJust mm)
 68          case assign of
 69            [(_, DE.VWord v)] ->
 70              assertBool "condition must be /= 0" (v /= 0)
 71            _ -> assertFailure "unexpected model"
 72
 73          -- There are only two branches: input == 0 and input /= 0
 74          (nxt, _) <- findUnexplored s inputs nextPathSel
 75          nxt @?= Nothing,
 76      testCase "Tracing with multiple branches" $
 77        do
 78          s <- z3Solver
 79          c1 <- unconstrained s 0 "cond1" QBE.Word
 80          c2 <- unconstrained s 0 "cond2" QBE.Word
 81
 82          t <-
 83            parseAndExec
 84              (QBE.GlobalIdent "branchOnInput")
 85              [c1, c2]
 86              "function $branchOnInput(w %cond1, w %cond2) {\n\
 87              \@jump.1\n\
 88              \jnz %cond1, @branch.1, @branch.2\n\
 89              \@branch.1\n\
 90              \jmp @jump.2\n\
 91              \@branch.2\n\
 92              \jmp @jump.2\n\
 93              \@jump.2\n\
 94              \jnz %cond2, @branch.3, @branch.4\n\
 95              \@branch.3\n\
 96              \ret\n\
 97              \@branch.4\n\
 98              \ret\n\
 99              \}"
100
101          length t @?= 2
102    ]
103
104backendTests :: TestTree
105backendTests =
106  testGroup
107    "Tests for the Symbolic Data Structures"
108    [traceTests]