quebex

 1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
 2--
 3-- SPDX-License-Identifier: GPL-3.0-only
 4
 5module BV (bvTests) where
 6
 7import SimpleBV qualified as SMT
 8import Test.Tasty
 9import Test.Tasty.HUnit
10
11foldingTests :: TestTree
12foldingTests =
13  testGroup
14    "foldingTests"
15    [ testCase "Folding of continous concat expressions" $
16        do
17          let val = SMT.const "foo" 32
18
19          let b1 = SMT.extract val 0 8
20          let b2 = SMT.extract val 8 8
21
22          SMT.concat b2 b1 @?= SMT.extract val 0 16,
23      testCase "Folding of ite-based equalities" $
24        do
25          let cond = SMT.const "foo" 32 `SMT.eq` SMT.const "bar" 32
26
27          let ifT = SMT.bvLit 32 0xdeadbeef
28          let ifF = SMT.bvLit 32 0xbeefdead
29          let val = SMT.ite cond ifT ifF
30
31          SMT.eq val ifT @?= cond
32          SMT.eq val ifF @?= SMT.not cond,
33      testCase "Folding of same-width extraction" $
34        do
35          let val = SMT.const "byte" 8
36          SMT.extract val 0 8 @?= val,
37      testCase "Folding of constant extractions" $
38        do
39          let val = SMT.bvLit 32 0xdeadbeef
40          SMT.extract val 16 16 @?= SMT.bvLit 16 0xdead,
41      testCase "Folding of identical nested extracts" $
42        do
43          let val = SMT.const "foobar" 64
44
45          let ex1 = SMT.extract val 0 16
46          let ex2 = SMT.extract ex1 0 16
47
48          ex2 @?= ex1,
49      testCase "Folding of ITE expressions" $
50        do
51          let cond = SMT.const "foo" 32 `SMT.eq` SMT.const "bar" 32
52          let val = SMT.ite cond (SMT.bvLit 32 0xdeadbeef) (SMT.bvLit 32 0xbeefdead)
53
54          SMT.extract val 0 16 @?= SMT.ite cond (SMT.bvLit 16 0xbeef) (SMT.bvLit 16 0xdead),
55      testCase "Extract reduces size" $
56        do
57          let val = SMT.bvLit 32 0xdeadbeef
58          SMT.extract val 8 8 @?= SMT.bvLit 8 0xbe,
59      testCase "Removal of non-extracted zero-extensions" $
60        do
61          let val = SMT.zeroExtend 24 $ SMT.bvLit 8 0xff
62          SMT.extract val 0 8 @?= SMT.bvLit 8 0xff
63          SMT.extract val 4 4 @?= SMT.bvLit 4 0xf,
64      -- TODO: constant fold extractions of zeros.
65      -- SMT.extract val 8 8 @?= SMT.bvLit 8 0x0
66      testCase "Extraction including zero-extended bits" $
67        do
68          let lit = SMT.bvLit 8 0xab
69          let val = SMT.zeroExtend 56 lit
70          SMT.extract val 0 32 @?= SMT.zeroExtend 24 lit
71          SMT.extract val 0 64 @?= val
72    ]
73
74bvTests :: TestTree
75bvTests = testGroup "SimpleBV" [foldingTests]