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.Symbolic.Expression qualified as SE
 13import Language.QBE.Types qualified as QBE
 14import SimpleSMT qualified as SMT
 15import Test.Tasty
 16import Test.Tasty.HUnit
 17
 18getSolver :: IO SMT.Solver
 19getSolver = do
 20  s <- z3Solver
 21  SMT.check s >> pure s
 22
 23------------------------------------------------------------------------
 24
 25-- TODO: QuickCheck tests against the default interpreter's implementation.
 26storeTests :: TestTree
 27storeTests =
 28  testGroup
 29    "Storage Instance Tests"
 30    [ testCase "Create bitvector and convert it to bytes" $
 31        do
 32          s <- getSolver
 33          let bytes = (E.toBytes (E.fromLit QBE.Word 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
 34          values <- mapM (SMT.getExpr s . SE.toSExpr) bytes
 35          values @?= [SMT.Bits 8 0xef, SMT.Bits 8 0xbe, SMT.Bits 8 0xad, SMT.Bits 8 0xde],
 36      testCase "Convert bitvector to bytes and back" $
 37        do
 38          s <- getSolver
 39
 40          let bytes = (E.toBytes (E.fromLit QBE.Word 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])
 41          length bytes @?= 4
 42
 43          value <- case E.fromBytes (QBE.Base QBE.Word) bytes of
 44            Just x -> SMT.getExpr s (SE.toSExpr x) <&> Just
 45            Nothing -> pure Nothing
 46          value @?= Just (SMT.Bits 32 0xdeadbeef)
 47    ]
 48
 49valueReprTests :: TestTree
 50valueReprTests =
 51  testGroup
 52    "Symbolic ValueRepr Tests"
 53    [ testCase "Create from literal and add" $
 54        do
 55          s <- getSolver
 56
 57          let v1 = E.fromLit QBE.Word 127
 58          let v2 = E.fromLit QBE.Word 128
 59
 60          expr <- SMT.getExpr s (SE.toSExpr $ fromJust $ v1 `E.add` v2)
 61          expr @?= SMT.Bits 32 0xff,
 62      testCase "Add incompatible values" $
 63        do
 64          let v1 = E.fromLit QBE.Word 0xffffffff :: SE.BitVector
 65          let v2 = E.fromLit QBE.Long 0xff :: SE.BitVector
 66
 67          -- Note: E.add doesn't do subtyping if invoked directly
 68          (v1 `E.add` v2) @?= Nothing,
 69      testCase "Subtyping" $
 70        do
 71          s <- getSolver
 72
 73          let v1 = E.fromLit QBE.Word 0xdeadbeef :: SE.BitVector
 74          let v2 = E.fromLit QBE.Long 0xff :: SE.BitVector
 75
 76          let v1sub = fromJust $ E.subType QBE.Word v1
 77          v1sub' <- SMT.getExpr s (SE.toSExpr v1sub)
 78          v1sub' @?= SMT.Bits 32 0xdeadbeef
 79
 80          let v2sub = fromJust $ E.subType QBE.Word v2
 81          v2sub' <- SMT.getExpr s (SE.toSExpr v2sub)
 82          v2sub' @?= SMT.Bits 32 0xff
 83
 84          let subtypedAddExpr = v1sub `E.add` v2sub
 85          expr <- SMT.getExpr s (SE.toSExpr (fromJust subtypedAddExpr))
 86
 87          expr @?= SMT.Bits 32 0xdeadbfee,
 88      testCase "Extend subwords" $
 89        do
 90          s <- getSolver
 91
 92          let bytes = (E.toBytes (E.fromLit QBE.Word 0xacacacac :: SE.BitVector) :: [SE.BitVector])
 93          let byte = head bytes
 94
 95          let sext = fromJust $ E.extend QBE.SignedByte byte
 96          sextVal <- SMT.getExpr s (SE.toSExpr sext)
 97          sextVal @?= SMT.Bits 64 0xffffffffffffffac
 98
 99          let zext = fromJust $ E.extend QBE.UnsignedByte byte
100          zextVal <- SMT.getExpr s (SE.toSExpr zext)
101          zextVal @?= SMT.Bits 64 0xac
102    ]
103
104exprTests :: TestTree
105exprTests = testGroup "Expression tests" [storeTests, valueReprTests]