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 "Concat with zeros" $
24        do
25          let lhs = SMT.bvLit 8 0x0
26          let rhs = SMT.const "foo" 8
27
28          SMT.concat lhs rhs @?= SMT.zeroExtend 8 rhs,
29      testCase "Folding of ite-based equalities" $
30        do
31          let cond = SMT.const "foo" 32 `SMT.eq` SMT.const "bar" 32
32
33          let ifT = SMT.bvLit 32 0xdeadbeef
34          let ifF = SMT.bvLit 32 0xbeefdead
35          let val = SMT.ite cond ifT ifF
36
37          SMT.eq val ifT @?= cond
38          SMT.eq val ifF @?= SMT.not cond,
39      testCase "Folding of same-width extraction" $
40        do
41          let val = SMT.const "byte" 8
42          SMT.extract val 0 8 @?= val,
43      testCase "Folding of constant extractions" $
44        do
45          let val = SMT.bvLit 32 0xdeadbeef
46          SMT.extract val 16 16 @?= SMT.bvLit 16 0xdead,
47      testCase "Folding of identical nested extracts" $
48        do
49          let val = SMT.const "foobar" 64
50
51          let ex1 = SMT.extract val 0 16
52          let ex2 = SMT.extract ex1 0 16
53
54          ex2 @?= ex1,
55      testCase "Folding of ITE expressions" $
56        do
57          let cond = SMT.const "foo" 32 `SMT.eq` SMT.const "bar" 32
58          let val = SMT.ite cond (SMT.bvLit 32 0xdeadbeef) (SMT.bvLit 32 0xbeefdead)
59
60          SMT.extract val 0 16 @?= SMT.ite cond (SMT.bvLit 16 0xbeef) (SMT.bvLit 16 0xdead),
61      testCase "Extract reduces size" $
62        do
63          let val = SMT.bvLit 32 0xdeadbeef
64          SMT.extract val 8 8 @?= SMT.bvLit 8 0xbe,
65      testCase "Removal of non-extracted zero-extensions" $
66        do
67          let val = SMT.zeroExtend 24 $ SMT.bvLit 8 0xff
68          SMT.extract val 0 8 @?= SMT.bvLit 8 0xff
69          SMT.extract val 4 4 @?= SMT.bvLit 4 0xf,
70      testCase "Extraction of zero bits" $
71        do
72          let val = SMT.zeroExtend 24 $ SMT.bvLit 8 0xff
73          SMT.extract val 8 24 @?= SMT.bvLit 24 0x0
74          SMT.extract val 0 8 @?= SMT.bvLit 8 0xff
75          SMT.extract val 24 8 @?= SMT.bvLit 8 0x0,
76      -- TODO: constant fold extractions of zeros.
77      -- SMT.extract val 8 8 @?= SMT.bvLit 8 0x0
78      testCase "Extraction including zero-extended bits" $
79        do
80          let lit = SMT.bvLit 8 0xab
81          let val = SMT.zeroExtend 56 lit
82          SMT.extract val 0 32 @?= SMT.zeroExtend 24 lit
83          SMT.extract val 0 64 @?= val
84    ]
85
86bvTests :: TestTree
87bvTests = testGroup "SimpleBV" [foldingTests]