quebex

 1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
 2--
 3-- SPDX-License-Identifier: GPL-3.0-only
 4
 5module Concolic (exprTests) where
 6
 7import Data.Maybe (fromJust)
 8import Language.QBE.Simulator.Concolic.Expression qualified as C
 9import Language.QBE.Simulator.Expression qualified as E
10import Language.QBE.Types qualified as QBE
11import Test.Tasty
12import Test.Tasty.HUnit
13
14-- TODO: QuickCheck tests against the default interpreter's implementation.
15storeTests :: TestTree
16storeTests =
17  testGroup
18    "Storage Instance Tests"
19    -- TODO: Test case for partial concoilc bytes
20    [ testCase "Convert concrete concolic value to bytes and back" $
21        do
22          let value = E.fromLit QBE.Word 0xdeadbeef :: C.Concolic
23
24          let bytes = E.toBytes value
25          length bytes @?= 4
26
27          let valueFromBytes = fromJust $ E.fromBytes (QBE.Base QBE.Word) bytes
28          C.concrete value @?= C.concrete valueFromBytes
29    ]
30
31exprTests :: TestTree
32exprTests = testGroup "Expression tests" [storeTests]