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
 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 InstrInput = InstrInput QBE.BaseType Word64
 48  deriving (Show)
 49
 50instance Arbitrary InstrInput where
 51  arbitrary = do
 52    t <- elements [QBE.Word, QBE.Long]
 53    InstrInput t <$> arbitrary
 54
 55unaryProp ::
 56  (SE.BitVector -> Maybe SE.BitVector) ->
 57  (DE.RegVal -> Maybe DE.RegVal) ->
 58  InstrInput ->
 59  Property
 60unaryProp opSym opCon (InstrInput 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 ShiftInput = ShiftInput QBE.BaseType Word64 Word32
 69  deriving (Show)
 70
 71instance Arbitrary ShiftInput where
 72  arbitrary = do
 73    t <- elements [QBE.Word, QBE.Long]
 74    v <- arbitrary
 75    ShiftInput t v <$> arbitrary
 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 (QBE.Base ty) val :: SE.BitVector
 84  let conValue = E.fromLit (QBE.Base ty) val :: DE.RegVal
 85
 86  let symResult = symValue `opSym` E.fromLit (QBE.Base QBE.Word) (fromIntegral amount)
 87  let conResult = conValue `opCon` E.fromLit (QBE.Base QBE.Word) (fromIntegral amount)
 88
 89  eqConcrete symResult conResult
 90
 91shiftEquiv :: TestTree
 92shiftEquiv =
 93  testGroup
 94    "Concrete and symbolic shifts are equivalent"
 95    [ testProperty "sar" (shiftProp E.sar E.sar),
 96      testProperty "shr" (shiftProp E.shr E.shr),
 97      testProperty "shl" (shiftProp E.shl E.shl)
 98    ]
 99
100------------------------------------------------------------------------
101
102equivTests :: TestTree
103equivTests =
104  testGroup
105    "QuickCheck-based equivalence tests"
106    [shiftEquiv, negEquiv]
107
108storeTests :: TestTree
109storeTests =
110  testGroup
111    "Storage Instance Tests"
112    [ testCase "Create bitvector and convert it to bytes" $
113        do
114          s <- getSolver
115          let bytes = (MEM.toBytes (E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
116          values <- mapM (SMT.getValue s . SE.toSExpr) bytes
117          values @?= [SMT.Bits 8 0xef, SMT.Bits 8 0xbe, SMT.Bits 8 0xad, SMT.Bits 8 0xde],
118      testCase "Convert bitvector to bytes and back" $
119        do
120          s <- getSolver
121
122          let bytes = (MEM.toBytes (E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
123          length bytes @?= 4
124
125          value <- case MEM.fromBytes (QBE.LBase QBE.Word) bytes of
126            Just x -> SMT.getValue s (SE.toSExpr x) <&> Just
127            Nothing -> pure Nothing
128          value @?= Just (SMT.Bits 32 0xdeadbeef)
129    ]
130
131valueReprTests :: TestTree
132valueReprTests =
133  testGroup
134    "Symbolic ValueRepr Tests"
135    [ testCase "Create from literal and add" $
136        do
137          s <- getSolver
138
139          let v1 = E.fromLit (QBE.Base QBE.Word) 127
140          let v2 = E.fromLit (QBE.Base QBE.Word) 128
141
142          expr <- SMT.getValue s (SE.toSExpr $ fromJust $ v1 `E.add` v2)
143          expr @?= SMT.Bits 32 0xff,
144      testCase "Add incompatible values" $
145        do
146          let v1 = E.fromLit (QBE.Base QBE.Word) 0xffffffff :: SE.BitVector
147          let v2 = E.fromLit (QBE.Base QBE.Long) 0xff :: SE.BitVector
148
149          -- Note: E.add doesn't do subtyping if invoked directly
150          (v1 `E.add` v2) @?= Nothing,
151      testCase "Subtyping" $
152        do
153          s <- getSolver
154
155          let v1 = E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector
156          let v2 = E.fromLit (QBE.Base QBE.Long) 0xff :: SE.BitVector
157
158          let v1sub = fromJust $ E.subType QBE.Word v1
159          v1sub' <- SMT.getValue s (SE.toSExpr v1sub)
160          v1sub' @?= SMT.Bits 32 0xdeadbeef
161
162          let v2sub = fromJust $ E.subType QBE.Word v2
163          v2sub' <- SMT.getValue s (SE.toSExpr v2sub)
164          v2sub' @?= SMT.Bits 32 0xff
165
166          let subtypedAddExpr = v1sub `E.add` v2sub
167          expr <- SMT.getValue s (SE.toSExpr (fromJust subtypedAddExpr))
168
169          expr @?= SMT.Bits 32 0xdeadbfee,
170      testCase "Extend subwords" $
171        do
172          s <- getSolver
173
174          let value = E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector
175
176          -- let sext = fromJust $ E.wordToLong (QBE.SLSubWord QBE.SignedByte) value
177          -- sextVal <- SMT.getValue s (SE.toSExpr sext)
178          -- sextVal @?= SMT.Bits 64 0xffffffffffffffef
179
180          let zext = fromJust $ E.wordToLong (QBE.SLSubWord QBE.UnsignedByte) value
181          zextVal <- SMT.getValue s (SE.toSExpr zext)
182          zextVal @?= SMT.Bits 64 0xef
183    ]
184
185exprTests :: TestTree
186exprTests = testGroup "Expression tests" [storeTests, valueReprTests, equivTests]