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 SimpleBV 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  )
 29
 30getSolver :: IO SMT.Solver
 31getSolver = do
 32  s <- defSolver
 33  SMT.check s >> pure s
 34
 35eqConcrete :: Maybe SE.BitVector -> Maybe DE.RegVal -> IO Bool
 36eqConcrete (Just sym) (Just con) = do
 37  s <- getSolver
 38  symVal <- SMT.getValue s (SE.toSExpr sym)
 39  case (symVal, con) of
 40    (SMT.Bits 32 sv, DE.VWord cv) -> pure $ sv == fromIntegral cv
 41    (SMT.Bits 64 sv, DE.VLong cv) -> pure $ sv == fromIntegral cv
 42    _ -> pure False
 43eqConcrete Nothing Nothing = pure True
 44eqConcrete _ _ = pure False
 45
 46------------------------------------------------------------------------
 47
 48data UnaryInput = UnaryInput QBE.BaseType Word64
 49  deriving (Show)
 50
 51instance Arbitrary UnaryInput where
 52  arbitrary = do
 53    t <- elements [QBE.Word, QBE.Long]
 54    UnaryInput t <$> arbitrary
 55
 56unaryProp ::
 57  (SE.BitVector -> Maybe SE.BitVector) ->
 58  (DE.RegVal -> Maybe DE.RegVal) ->
 59  UnaryInput ->
 60  Property
 61unaryProp opSym opCon (UnaryInput ty val) = ioProperty $ do
 62  eqConcrete (opSym $ E.fromLit (QBE.Base ty) val) (opCon $ E.fromLit (QBE.Base ty) val)
 63
 64negEquiv :: TestTree
 65negEquiv = testProperty "neg" (unaryProp E.neg E.neg)
 66
 67------------------------------------------------------------------------
 68
 69data BinaryInput = BinaryInput QBE.BaseType Word64 Word64
 70  deriving (Show)
 71
 72instance Arbitrary BinaryInput where
 73  arbitrary = do
 74    ty <- elements [QBE.Word, QBE.Long]
 75    lhs <- arbitrary
 76    BinaryInput ty lhs <$> arbitrary
 77
 78binaryProp ::
 79  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->
 80  (DE.RegVal -> DE.RegVal -> Maybe DE.RegVal) ->
 81  BinaryInput ->
 82  Property
 83binaryProp opSym opCon (BinaryInput ty lhs rhs) =
 84  ioProperty $
 85    eqConcrete (opSym (mkS lhs) (mkS rhs)) (opCon (mkC lhs) (mkC rhs))
 86  where
 87    mkS :: Word64 -> SE.BitVector
 88    mkS = E.fromLit (QBE.Base ty)
 89
 90    mkC :: Word64 -> DE.RegVal
 91    mkC = E.fromLit (QBE.Base ty)
 92
 93divProp ::
 94  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->
 95  (DE.RegVal -> DE.RegVal -> Maybe DE.RegVal) ->
 96  BinaryInput ->
 97  Property
 98divProp opSym opCon input@(BinaryInput _ _ rhs) =
 99  (rhs /= 0) ==> binaryProp opSym opCon input
100
101opEquiv :: TestTree
102opEquiv =
103  testGroup
104    "Operation equivalence"
105    [ testProperty "add" (binaryProp E.add E.add),
106      testProperty "sub" (binaryProp E.sub E.sub),
107      testProperty "mul" (binaryProp E.mul E.mul),
108      testProperty "div" (divProp E.div E.div),
109      testProperty "or" (binaryProp E.or E.or),
110      testProperty "xor" (binaryProp E.xor E.xor),
111      testProperty "and" (binaryProp E.and E.and),
112      testProperty "urem" (divProp E.urem E.urem),
113      testProperty "srem" (divProp E.srem E.srem),
114      testProperty "udiv" (divProp E.udiv E.udiv),
115      testProperty "eq" (binaryProp E.eq E.eq),
116      testProperty "ne" (binaryProp E.ne E.ne),
117      testProperty "sle" (binaryProp E.sle E.sle),
118      testProperty "slt" (binaryProp E.slt E.slt),
119      testProperty "sge" (binaryProp E.sge E.sge),
120      testProperty "sgt" (binaryProp E.sgt E.sgt),
121      testProperty "ule" (binaryProp E.ule E.ule),
122      testProperty "ult" (binaryProp E.ult E.ult),
123      testProperty "uge" (binaryProp E.uge E.uge),
124      testProperty "ugt" (binaryProp E.ugt E.ugt)
125    ]
126
127------------------------------------------------------------------------
128
129data ShiftInput = ShiftInput QBE.BaseType Word64 Word32
130  deriving (Show)
131
132instance Arbitrary ShiftInput where
133  arbitrary = do
134    t <- elements [QBE.Word, QBE.Long]
135    v <- arbitrary
136    ShiftInput t v <$> arbitrary
137
138shiftProp ::
139  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->
140  (DE.RegVal -> DE.RegVal -> Maybe DE.RegVal) ->
141  ShiftInput ->
142  Property
143shiftProp opSym opCon (ShiftInput ty val amount) = ioProperty $ do
144  let symValue = E.fromLit (QBE.Base ty) val :: SE.BitVector
145  let conValue = E.fromLit (QBE.Base ty) val :: DE.RegVal
146
147  let symResult = symValue `opSym` E.fromLit (QBE.Base QBE.Word) (fromIntegral amount)
148  let conResult = conValue `opCon` E.fromLit (QBE.Base QBE.Word) (fromIntegral amount)
149
150  eqConcrete symResult conResult
151
152shiftEquiv :: TestTree
153shiftEquiv =
154  testGroup
155    "Concrete and symbolic shifts are equivalent"
156    [ testProperty "sar" (shiftProp E.sar E.sar),
157      testProperty "shr" (shiftProp E.shr E.shr),
158      testProperty "shl" (shiftProp E.shl E.shl)
159    ]
160
161------------------------------------------------------------------------
162
163equivTests :: TestTree
164equivTests =
165  testGroup
166    "QuickCheck-based equivalence tests"
167    [shiftEquiv, negEquiv, opEquiv]
168
169storeTests :: TestTree
170storeTests =
171  testGroup
172    "Storage Instance Tests"
173    [ testCase "Create bitvector and convert it to bytes" $
174        do
175          s <- getSolver
176          let bytes = (MEM.toBytes (E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
177          values <- mapM (SMT.getValue s . SE.toSExpr) bytes
178          values @?= [SMT.Bits 8 0xef, SMT.Bits 8 0xbe, SMT.Bits 8 0xad, SMT.Bits 8 0xde],
179      testCase "Convert bitvector to bytes and back" $
180        do
181          s <- getSolver
182
183          let bytes = (MEM.toBytes (E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
184          length bytes @?= 4
185
186          value <- case MEM.fromBytes (QBE.LBase QBE.Word) bytes of
187            Just x -> SMT.getValue s (SE.toSExpr x) <&> Just
188            Nothing -> pure Nothing
189          value @?= Just (SMT.Bits 32 0xdeadbeef)
190    ]
191
192valueReprTests :: TestTree
193valueReprTests =
194  testGroup
195    "Symbolic ValueRepr Tests"
196    [ testCase "Create from literal and add" $
197        do
198          s <- getSolver
199
200          let v1 = E.fromLit (QBE.Base QBE.Word) 127
201          let v2 = E.fromLit (QBE.Base QBE.Word) 128
202
203          expr <- SMT.getValue s (SE.toSExpr $ fromJust $ v1 `E.add` v2)
204          expr @?= SMT.Bits 32 0xff,
205      testCase "Add incompatible values" $
206        do
207          let v1 = E.fromLit (QBE.Base QBE.Word) 0xffffffff :: SE.BitVector
208          let v2 = E.fromLit (QBE.Base QBE.Long) 0xff :: SE.BitVector
209
210          -- Note: E.add doesn't do subtyping if invoked directly
211          (v1 `E.add` v2) @?= Nothing,
212      testCase "Subtyping" $
213        do
214          s <- getSolver
215
216          let v1 = E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector
217          let v2 = E.fromLit (QBE.Base QBE.Long) 0xff :: SE.BitVector
218
219          let v1sub = fromJust $ E.subType QBE.Word v1
220          v1sub' <- SMT.getValue s (SE.toSExpr v1sub)
221          v1sub' @?= SMT.Bits 32 0xdeadbeef
222
223          let v2sub = fromJust $ E.subType QBE.Word v2
224          v2sub' <- SMT.getValue s (SE.toSExpr v2sub)
225          v2sub' @?= SMT.Bits 32 0xff
226
227          let subtypedAddExpr = v1sub `E.add` v2sub
228          expr <- SMT.getValue s (SE.toSExpr (fromJust subtypedAddExpr))
229
230          expr @?= SMT.Bits 32 0xdeadbfee,
231      testCase "Extend subwords" $
232        do
233          s <- getSolver
234
235          let value = E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector
236
237          -- let sext = fromJust $ E.wordToLong (QBE.SLSubWord QBE.SignedByte) value
238          -- sextVal <- SMT.getValue s (SE.toSExpr sext)
239          -- sextVal @?= SMT.Bits 64 0xffffffffffffffef
240
241          let zext = fromJust $ E.wordToLong (QBE.SLSubWord QBE.UnsignedByte) value
242          zextVal <- SMT.getValue s (SE.toSExpr zext)
243          zextVal @?= SMT.Bits 64 0xef
244    ]
245
246exprTests :: TestTree
247exprTests = testGroup "Expression tests" [storeTests, valueReprTests, equivTests]