quebex

  1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
  2--
  3-- SPDX-License-Identifier: GPL-3.0-only
  4
  5module Symbolic (exprTests) where
  6
  7import Data.Functor ((<&>))
  8import Data.Int (Int64)
  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
 29getSolver :: IO SMT.Solver
 30getSolver = do
 31  s <- defSolver
 32  SMT.check s >> pure s
 33
 34eqConcrete :: Maybe SE.BitVector -> Maybe DE.RegVal -> IO Bool
 35eqConcrete (Just sym) (Just con) = do
 36  s <- getSolver
 37  symVal <- SMT.getValue 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
 42eqConcrete Nothing Nothing = pure True
 43eqConcrete _ _ = pure False
 44
 45------------------------------------------------------------------------
 46
 47data UnaryInput = UnaryInput QBE.BaseType Word64
 48  deriving (Show)
 49
 50instance Arbitrary UnaryInput where
 51  arbitrary = do
 52    t <- elements [QBE.Word, QBE.Long]
 53    UnaryInput t <$> arbitrary
 54
 55unaryProp ::
 56  (SE.BitVector -> Maybe SE.BitVector) ->
 57  (DE.RegVal -> Maybe DE.RegVal) ->
 58  UnaryInput ->
 59  Property
 60unaryProp opSym opCon (UnaryInput ty val) = ioProperty $ do
 61  eqConcrete (opSym $ E.fromLit (QBE.Base ty) val) (opCon $ E.fromLit (QBE.Base ty) val)
 62
 63negEquiv :: TestTree
 64negEquiv = testProperty "neg" (unaryProp E.neg E.neg)
 65
 66------------------------------------------------------------------------
 67
 68data BinaryInput = BinaryInput QBE.BaseType Word64 Word64
 69  deriving (Show)
 70
 71instance Arbitrary BinaryInput where
 72  arbitrary = do
 73    ty <- elements [QBE.Word, QBE.Long]
 74    lhs <- arbitrary
 75    BinaryInput ty lhs <$> arbitrary
 76
 77binaryEq ::
 78  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->
 79  (DE.RegVal -> DE.RegVal -> Maybe DE.RegVal) ->
 80  BinaryInput ->
 81  IO Bool
 82binaryEq opSym opCon (BinaryInput ty lhs rhs) =
 83  eqConcrete (opSym (mkS lhs) (mkS rhs)) (opCon (mkC lhs) (mkC rhs))
 84  where
 85    mkS :: Word64 -> SE.BitVector
 86    mkS = E.fromLit (QBE.Base ty)
 87
 88    mkC :: Word64 -> DE.RegVal
 89    mkC = E.fromLit (QBE.Base ty)
 90
 91binaryProp ::
 92  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->
 93  (DE.RegVal -> DE.RegVal -> Maybe DE.RegVal) ->
 94  BinaryInput ->
 95  Property
 96binaryProp opSym opCon input = ioProperty $ binaryEq opSym opCon input
 97
 98opEquiv :: TestTree
 99opEquiv =
100  testGroup
101    "Operation equivalence"
102    [ testProperty "add" (binaryProp E.add E.add),
103      testProperty "sub" (binaryProp E.sub E.sub),
104      testProperty "mul" (binaryProp E.mul E.mul),
105      testProperty "div" (binaryProp E.div E.div),
106      testProperty "or" (binaryProp E.or E.or),
107      testProperty "xor" (binaryProp E.xor E.xor),
108      testProperty "and" (binaryProp E.and E.and),
109      testProperty "urem" (binaryProp E.urem E.urem),
110      testProperty "srem" (binaryProp E.srem E.srem),
111      testProperty "udiv" (binaryProp E.udiv E.udiv),
112      testProperty "eq" (binaryProp E.eq E.eq),
113      testProperty "ne" (binaryProp E.ne E.ne),
114      testProperty "sle" (binaryProp E.sle E.sle),
115      testProperty "slt" (binaryProp E.slt E.slt),
116      testProperty "sge" (binaryProp E.sge E.sge),
117      testProperty "sgt" (binaryProp E.sgt E.sgt),
118      testProperty "ule" (binaryProp E.ule E.ule),
119      testProperty "ult" (binaryProp E.ult E.ult),
120      testProperty "uge" (binaryProp E.uge E.uge),
121      testProperty "ugt" (binaryProp E.ugt E.ugt)
122    ]
123
124------------------------------------------------------------------------
125
126data ShiftInput = ShiftInput QBE.BaseType Word64 Word32
127  deriving (Show)
128
129instance Arbitrary ShiftInput where
130  arbitrary = do
131    t <- elements [QBE.Word, QBE.Long]
132    v <- arbitrary
133    ShiftInput t v <$> arbitrary
134
135shiftProp ::
136  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->
137  (DE.RegVal -> DE.RegVal -> Maybe DE.RegVal) ->
138  ShiftInput ->
139  Property
140shiftProp opSym opCon (ShiftInput ty val amount) = ioProperty $ do
141  let symValue = E.fromLit (QBE.Base ty) val :: SE.BitVector
142  let conValue = E.fromLit (QBE.Base ty) val :: DE.RegVal
143
144  let symResult = symValue `opSym` E.fromLit (QBE.Base QBE.Word) (fromIntegral amount)
145  let conResult = conValue `opCon` E.fromLit (QBE.Base QBE.Word) (fromIntegral amount)
146
147  eqConcrete symResult conResult
148
149shiftEquiv :: TestTree
150shiftEquiv =
151  testGroup
152    "Concrete and symbolic shifts are equivalent"
153    [ testProperty "sar" (shiftProp E.sar E.sar),
154      testProperty "shr" (shiftProp E.shr E.shr),
155      testProperty "shl" (shiftProp E.shl E.shl)
156    ]
157
158------------------------------------------------------------------------
159
160equivTests :: TestTree
161equivTests =
162  testGroup
163    "Equivalence tests for symbolic and default expression interpreter"
164    [ shiftEquiv,
165      negEquiv,
166      opEquiv,
167      -- Occurs when the most-negative integer is divided by -1.
168      testCase "Signed division overflow on div" $
169        do
170          let input =
171                BinaryInput QBE.Long 0x8000000000000000 $
172                  fromIntegral (-1 :: Int64)
173          binaryEq E.div E.div input >>= assertBool "signed-div-overflow",
174      testCase "Signed division overflow on srem" $
175        do
176          let input =
177                BinaryInput QBE.Long 0x8000000000000000 $
178                  fromIntegral (-1 :: Int64)
179          binaryEq E.srem E.srem input >>= assertBool "signed-srem-overflow"
180    ]
181
182storeTests :: TestTree
183storeTests =
184  testGroup
185    "Storage Instance Tests"
186    [ testCase "Create bitvector and convert it to bytes" $
187        do
188          s <- getSolver
189          let bytes = (MEM.toBytes (E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
190          values <- mapM (SMT.getValue s . SE.toSExpr) bytes
191          values @?= [SMT.Bits 8 0xef, SMT.Bits 8 0xbe, SMT.Bits 8 0xad, SMT.Bits 8 0xde],
192      testCase "Convert bitvector to bytes and back" $
193        do
194          s <- getSolver
195
196          let bytes = (MEM.toBytes (E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
197          length bytes @?= 4
198
199          value <- case MEM.fromBytes (QBE.LBase QBE.Word) bytes of
200            Just x -> SMT.getValue s (SE.toSExpr x) <&> Just
201            Nothing -> pure Nothing
202          value @?= Just (SMT.Bits 32 0xdeadbeef)
203    ]
204
205valueReprTests :: TestTree
206valueReprTests =
207  testGroup
208    "Symbolic ValueRepr Tests"
209    [ testCase "create from literal and add" $
210        do
211          s <- getSolver
212
213          let v1 = E.fromLit (QBE.Base QBE.Word) 127
214          let v2 = E.fromLit (QBE.Base QBE.Word) 128
215
216          expr <- SMT.getValue s (SE.toSExpr $ fromJust $ v1 `E.add` v2)
217          expr @?= SMT.Bits 32 0xff,
218      testCase "add incompatible values" $
219        do
220          let v1 = E.fromLit (QBE.Base QBE.Word) 0xffffffff :: SE.BitVector
221          let v2 = E.fromLit (QBE.Base QBE.Long) 0xff :: SE.BitVector
222
223          -- Note: E.add doesn't do subtyping if invoked directly
224          (v1 `E.add` v2) @?= Nothing,
225      testCase "extend" $
226        do
227          s <- getSolver
228
229          let v1 = E.fromLit QBE.Byte 0xff :: SE.BitVector
230              ext1 = fromJust $ E.extend QBE.HalfWord False v1
231          ext1Val <- SMT.getValue s (SE.toSExpr ext1)
232          ext1Val @?= SMT.Bits 16 0x00ff
233
234          let v2 = E.fromLit QBE.Byte 0xab :: SE.BitVector
235              ext2 = fromJust $ E.extend (QBE.Base QBE.Word) True v2
236          ext2Val <- SMT.getValue s (SE.toSExpr ext2)
237          ext2Val @?= SMT.Bits 32 0xffffffab
238
239          let v3 = E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector
240          E.extend (QBE.Base QBE.Word) True v3 @?= Nothing
241          E.extend QBE.Byte True v3 @?= Nothing,
242      testCase "extract" $
243        do
244          s <- getSolver
245
246          let value = E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector
247
248          let ex1 = fromJust $ E.extract QBE.Byte value
249          ex1Val <- SMT.getValue s (SE.toSExpr ex1)
250          ex1Val @?= SMT.Bits 8 0xef
251
252          let ex2 = fromJust $ E.extract QBE.HalfWord value
253          ex2Val <- SMT.getValue s (SE.toSExpr ex2)
254          ex2Val @?= SMT.Bits 16 0xbeef
255
256          E.extract (QBE.Base QBE.Word) value @?= Just value
257          E.extract (QBE.Base QBE.Long) value @?= Nothing
258    ]
259
260exprTests :: TestTree
261exprTests = testGroup "Expression tests" [storeTests, valueReprTests, equivTests]