quebex

  1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
  2--
  3-- SPDX-License-Identifier: GPL-3.0-only
  4{-# OPTIONS_GHC -Wno-x-partial #-}
  5
  6module Symbolic (exprTests) where
  7
  8import Data.Functor ((<&>))
  9import Data.Maybe (fromJust)
 10import Language.QBE.Simulator.Explorer (z3Solver)
 11import Language.QBE.Simulator.Expression qualified as E
 12import Language.QBE.Simulator.Memory qualified as MEM
 13import Language.QBE.Simulator.Symbolic.Expression qualified as SE
 14import Language.QBE.Types qualified as QBE
 15import SimpleSMT qualified as SMT
 16import Test.Tasty
 17import Test.Tasty.HUnit
 18
 19getSolver :: IO SMT.Solver
 20getSolver = do
 21  s <- z3Solver
 22  SMT.check s >> pure s
 23
 24------------------------------------------------------------------------
 25
 26-- TODO: QuickCheck tests against the default interpreter's implementation.
 27storeTests :: TestTree
 28storeTests =
 29  testGroup
 30    "Storage Instance Tests"
 31    [ testCase "Create bitvector and convert it to bytes" $
 32        do
 33          s <- getSolver
 34          let bytes = (MEM.toBytes (E.fromLit QBE.Word 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
 35          values <- mapM (SMT.getExpr s . SE.toSExpr) bytes
 36          values @?= [SMT.Bits 8 0xef, SMT.Bits 8 0xbe, SMT.Bits 8 0xad, SMT.Bits 8 0xde],
 37      testCase "Convert bitvector to bytes and back" $
 38        do
 39          s <- getSolver
 40
 41          let bytes = (MEM.toBytes (E.fromLit QBE.Word 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
 42          length bytes @?= 4
 43
 44          value <- case MEM.fromBytes (QBE.LBase QBE.Word) bytes of
 45            Just x -> SMT.getExpr s (SE.toSExpr x) <&> Just
 46            Nothing -> pure Nothing
 47          value @?= Just (SMT.Bits 32 0xdeadbeef)
 48    ]
 49
 50valueReprTests :: TestTree
 51valueReprTests =
 52  testGroup
 53    "Symbolic ValueRepr Tests"
 54    [ testCase "Create from literal and add" $
 55        do
 56          s <- getSolver
 57
 58          let v1 = E.fromLit QBE.Word 127
 59          let v2 = E.fromLit QBE.Word 128
 60
 61          expr <- SMT.getExpr s (SE.toSExpr $ fromJust $ v1 `E.add` v2)
 62          expr @?= SMT.Bits 32 0xff,
 63      testCase "Add incompatible values" $
 64        do
 65          let v1 = E.fromLit QBE.Word 0xffffffff :: SE.BitVector
 66          let v2 = E.fromLit QBE.Long 0xff :: SE.BitVector
 67
 68          -- Note: E.add doesn't do subtyping if invoked directly
 69          (v1 `E.add` v2) @?= Nothing,
 70      testCase "Subtyping" $
 71        do
 72          s <- getSolver
 73
 74          let v1 = E.fromLit QBE.Word 0xdeadbeef :: SE.BitVector
 75          let v2 = E.fromLit QBE.Long 0xff :: SE.BitVector
 76
 77          let v1sub = fromJust $ E.subType QBE.Word v1
 78          v1sub' <- SMT.getExpr s (SE.toSExpr v1sub)
 79          v1sub' @?= SMT.Bits 32 0xdeadbeef
 80
 81          let v2sub = fromJust $ E.subType QBE.Word v2
 82          v2sub' <- SMT.getExpr s (SE.toSExpr v2sub)
 83          v2sub' @?= SMT.Bits 32 0xff
 84
 85          let subtypedAddExpr = v1sub `E.add` v2sub
 86          expr <- SMT.getExpr s (SE.toSExpr (fromJust subtypedAddExpr))
 87
 88          expr @?= SMT.Bits 32 0xdeadbfee,
 89      testCase "Extend subwords" $
 90        do
 91          s <- getSolver
 92
 93          let value = E.fromLit QBE.Word 0xdeadbeef :: SE.BitVector
 94
 95          -- let sext = fromJust $ E.wordToLong (QBE.SLSubWord QBE.SignedByte) value
 96          -- sextVal <- SMT.getExpr s (SE.toSExpr sext)
 97          -- sextVal @?= SMT.Bits 64 0xffffffffffffffef
 98
 99          let zext = fromJust $ E.wordToLong (QBE.SLSubWord QBE.UnsignedByte) value
100          zextVal <- SMT.getExpr s (SE.toSExpr zext)
101          zextVal @?= SMT.Bits 64 0xef
102    ]
103
104exprTests :: TestTree
105exprTests = testGroup "Expression tests" [storeTests, valueReprTests]