quebex - Concolic.hs

 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 Data.Word (Word8)
 9import Language.QBE.Simulator.Concolic.Expression qualified as C
10import Language.QBE.Simulator.Default.Expression qualified as D
11import Language.QBE.Simulator.Expression qualified as E
12import Language.QBE.Simulator.Memory qualified as MEM
13import Language.QBE.Types qualified as QBE
14import Test.Tasty
15import Test.Tasty.HUnit
16
17-- TODO: QuickCheck tests against the default interpreter's implementation.
18storeTests :: TestTree
19storeTests =
20  testGroup
21    "Storage Instance Tests"
22    -- TODO: Test case for partial concoilc bytes
23    [ testCase "Convert concrete concolic value to bytes and back" $
24        do
25          let value = E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: C.Concolic D.RegVal
26
27          let bytes = MEM.toBytes value :: [C.Concolic Word8]
28          length bytes @?= 4
29
30          let valueFromBytes = fromJust $ MEM.fromBytes (QBE.LBase QBE.Word) bytes
31          C.concrete value @?= C.concrete valueFromBytes
32    ]
33
34exprTests :: TestTree
35exprTests = testGroup "Expression tests" [storeTests]