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 Data.Word (Word32, Word64)
 11import Language.QBE.Simulator.Default.Expression qualified as DE
 12import Language.QBE.Simulator.Explorer (defSolver)
 13import Language.QBE.Simulator.Expression qualified as E
 14import Language.QBE.Simulator.Memory qualified as MEM
 15import Language.QBE.Simulator.Symbolic.Expression qualified as SE
 16import Language.QBE.Types qualified as QBE
 17import SimpleSMT qualified as SMT
 18import Test.Tasty
 19import Test.Tasty.HUnit
 20import Test.Tasty.QuickCheck
 21  ( Arbitrary,
 22    Property,
 23    arbitrary,
 24    elements,
 25    ioProperty,
 26    testProperty,
 27  )
 28
 29getSolver :: IO SMT.Solver
 30getSolver = do
 31  s <- defSolver
 32  SMT.check s >> pure s
 33
 34eqConcrete :: SE.BitVector -> DE.RegVal -> IO Bool
 35eqConcrete sym con = do
 36  s <- getSolver
 37  symVal <- SMT.getExpr s (SE.toSExpr sym)
 38  case (symVal, con) of
 39    (SMT.Bits 32 sv, DE.VWord cv) -> pure $ sv == (fromIntegral cv)
 40    (SMT.Bits 64 sv, DE.VLong cv) -> pure $ sv == (fromIntegral cv)
 41    _ -> pure False
 42
 43------------------------------------------------------------------------
 44
 45data InstrInput = InstrInput QBE.BaseType Word64
 46  deriving (Show)
 47
 48instance Arbitrary InstrInput where
 49  arbitrary = do
 50    t <- elements [QBE.Word, QBE.Long]
 51    v <- arbitrary
 52    pure $ InstrInput t v
 53
 54unaryProp ::
 55  (SE.BitVector -> SE.BitVector) ->
 56  (DE.RegVal -> DE.RegVal) ->
 57  InstrInput ->
 58  Property
 59unaryProp opSym opCon (InstrInput ty val) = ioProperty $ do
 60  eqConcrete (opSym $ E.fromLit ty val) (opCon $ E.fromLit ty val)
 61
 62negEquiv :: TestTree
 63negEquiv = testProperty "neg" (unaryProp E.neg E.neg)
 64
 65------------------------------------------------------------------------
 66
 67data ShiftInput = ShiftInput QBE.BaseType Word64 Word32
 68  deriving (Show)
 69
 70instance Arbitrary ShiftInput where
 71  arbitrary = do
 72    t <- elements [QBE.Word, QBE.Long]
 73    v <- arbitrary
 74    s <- arbitrary
 75    pure $ ShiftInput t v s
 76
 77shiftProp ::
 78  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->
 79  (DE.RegVal -> DE.RegVal -> Maybe DE.RegVal) ->
 80  ShiftInput ->
 81  Property
 82shiftProp opSym opCon (ShiftInput ty val amount) = ioProperty $ do
 83  let symValue = E.fromLit ty val :: SE.BitVector
 84  let conValue = E.fromLit ty val :: DE.RegVal
 85
 86  let symResult = symValue `opSym` (E.fromLit QBE.Word $ fromIntegral amount)
 87  let conResult = conValue `opCon` (E.fromLit QBE.Word $ fromIntegral amount)
 88
 89  case (symResult, conResult) of
 90    (Just s, Just c) -> eqConcrete s c
 91    (Nothing, Nothing) -> pure True
 92    _ -> pure False
 93
 94shiftEquiv :: TestTree
 95shiftEquiv =
 96  testGroup
 97    "Concrete and symbolic shifts are equivalent"
 98    [ testProperty "sar" (shiftProp E.sar E.sar),
 99      testProperty "shr" (shiftProp E.shr E.shr),
100      testProperty "shl" (shiftProp E.shl E.shl)
101    ]
102
103------------------------------------------------------------------------
104
105equivTests :: TestTree
106equivTests =
107  testGroup
108    "QuickCheck-based equivalence tests"
109    [shiftEquiv, negEquiv]
110
111storeTests :: TestTree
112storeTests =
113  testGroup
114    "Storage Instance Tests"
115    [ testCase "Create bitvector and convert it to bytes" $
116        do
117          s <- getSolver
118          let bytes = (MEM.toBytes (E.fromLit QBE.Word 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
119          values <- mapM (SMT.getExpr s . SE.toSExpr) bytes
120          values @?= [SMT.Bits 8 0xef, SMT.Bits 8 0xbe, SMT.Bits 8 0xad, SMT.Bits 8 0xde],
121      testCase "Convert bitvector to bytes and back" $
122        do
123          s <- getSolver
124
125          let bytes = (MEM.toBytes (E.fromLit QBE.Word 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
126          length bytes @?= 4
127
128          value <- case MEM.fromBytes (QBE.LBase QBE.Word) bytes of
129            Just x -> SMT.getExpr s (SE.toSExpr x) <&> Just
130            Nothing -> pure Nothing
131          value @?= Just (SMT.Bits 32 0xdeadbeef)
132    ]
133
134valueReprTests :: TestTree
135valueReprTests =
136  testGroup
137    "Symbolic ValueRepr Tests"
138    [ testCase "Create from literal and add" $
139        do
140          s <- getSolver
141
142          let v1 = E.fromLit QBE.Word 127
143          let v2 = E.fromLit QBE.Word 128
144
145          expr <- SMT.getExpr s (SE.toSExpr $ fromJust $ v1 `E.add` v2)
146          expr @?= SMT.Bits 32 0xff,
147      testCase "Add incompatible values" $
148        do
149          let v1 = E.fromLit QBE.Word 0xffffffff :: SE.BitVector
150          let v2 = E.fromLit QBE.Long 0xff :: SE.BitVector
151
152          -- Note: E.add doesn't do subtyping if invoked directly
153          (v1 `E.add` v2) @?= Nothing,
154      testCase "Subtyping" $
155        do
156          s <- getSolver
157
158          let v1 = E.fromLit QBE.Word 0xdeadbeef :: SE.BitVector
159          let v2 = E.fromLit QBE.Long 0xff :: SE.BitVector
160
161          let v1sub = fromJust $ E.subType QBE.Word v1
162          v1sub' <- SMT.getExpr s (SE.toSExpr v1sub)
163          v1sub' @?= SMT.Bits 32 0xdeadbeef
164
165          let v2sub = fromJust $ E.subType QBE.Word v2
166          v2sub' <- SMT.getExpr s (SE.toSExpr v2sub)
167          v2sub' @?= SMT.Bits 32 0xff
168
169          let subtypedAddExpr = v1sub `E.add` v2sub
170          expr <- SMT.getExpr s (SE.toSExpr (fromJust subtypedAddExpr))
171
172          expr @?= SMT.Bits 32 0xdeadbfee,
173      testCase "Extend subwords" $
174        do
175          s <- getSolver
176
177          let value = E.fromLit QBE.Word 0xdeadbeef :: SE.BitVector
178
179          -- let sext = fromJust $ E.wordToLong (QBE.SLSubWord QBE.SignedByte) value
180          -- sextVal <- SMT.getExpr s (SE.toSExpr sext)
181          -- sextVal @?= SMT.Bits 64 0xffffffffffffffef
182
183          let zext = fromJust $ E.wordToLong (QBE.SLSubWord QBE.UnsignedByte) value
184          zextVal <- SMT.getExpr s (SE.toSExpr zext)
185          zextVal @?= SMT.Bits 64 0xef
186    ]
187
188exprTests :: TestTree
189exprTests = testGroup "Expression tests" [storeTests, valueReprTests, equivTests]