GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-02 01:37:19 +03:00
Code Issues Projects Releases Wiki Activity

symbolic-syntax: Add a test that exercises all the operations

Browse Source
This commit is contained in:
Langston Barrett 2023-11-02 09:11:04 -04:00
parent a2ac7f4300
commit 19f0a578fc
3 changed files with 137 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
symbolic-syntax/test-data/ops.cbl Normal file
View File

@ -0,0 +1,13 @@
; A function that demonstrates the use of all of the operations
(defun @ops ((p Pointer) (q Pointer)) Unit
(start start:
(let b (bv-typed-literal SizeT 42))
(let v (fresh-vec "v" Short 7))
(let n (make-null))
(let d (pointer-diff p q))
(let r (pointer-add p d))
(let s (pointer-sub r d))
(let e (pointer-eq s p))
(let t (pointer-read Int le s))
(pointer-write SizeT le s b)
(return ())))

62
symbolic-syntax/test-data/ops.out Normal file
View File

@ -0,0 +1,62 @@
(defun @ops ((p Pointer) (q Pointer)) Unit
(start start:
(let b (bv-typed-literal SizeT 42))
(let v (fresh-vec "v" Short 7))
(let n (make-null))
(let d (pointer-diff p q))
(let r (pointer-add p d))
(let s (pointer-sub r d))
(let e (pointer-eq s p))
(let t (pointer-read Int le s))
(pointer-write SizeT le s b)
(return ())))
ops
%0
% 4:12
$2 = intLit(42)
% 4:12
$3 = integerToBV(64, $2)
% internal
$4 = fresh BaseBVRepr 16 v_0
% internal
$5 = fresh BaseBVRepr 16 v_1
% internal
$6 = fresh BaseBVRepr 16 v_2
% internal
$7 = fresh BaseBVRepr 16 v_3
% internal
$8 = fresh BaseBVRepr 16 v_4
% internal
$9 = fresh BaseBVRepr 16 v_5
% internal
$10 = fresh BaseBVRepr 16 v_6
% 5:12
$11 = vectorLit(BVRepr 16, [$4, $5, $6, $7, $8, $9, $10])
% 6:12
$12 = extensionApp(null_ptr)
% internal
$13 = (ptr_sub $0 $1)
% 7:12
$14 = extensionApp((ptr_to_bits_64 $13))
% internal
$15 = extensionApp((bits_to_ptr_64 $14))
% 8:12
$16 = (ptr_add $0 $15)
% 9:16
$17 = (ptr_sub $16 $15)
% 10:16
$18 = (ptr_eq $17 $0)
% internal
$19 = (macawReadMem bvle4 $17)
% 11:12
$20 = extensionApp((ptr_to_bits_32 $19))
% internal
$21 = extensionApp((bits_to_ptr_64 $3))
% 12:5
$22 = (macawWriteMem bvle8 $17 $21)
% 13:13
$23 = emptyApp()
% 13:5
return $23
% no postdom

62
symbolic-syntax/test-data/ops.out.good Normal file
View File

@ -0,0 +1,62 @@
(defun @ops ((p Pointer) (q Pointer)) Unit
(start start:
(let b (bv-typed-literal SizeT 42))
(let v (fresh-vec "v" Short 7))
(let n (make-null))
(let d (pointer-diff p q))
(let r (pointer-add p d))
(let s (pointer-sub r d))
(let e (pointer-eq s p))
(let t (pointer-read Int le s))
(pointer-write SizeT le s b)
(return ())))
ops
%0
% 4:12
$2 = intLit(42)
% 4:12
$3 = integerToBV(64, $2)
% internal
$4 = fresh BaseBVRepr 16 v_0
% internal
$5 = fresh BaseBVRepr 16 v_1
% internal
$6 = fresh BaseBVRepr 16 v_2
% internal
$7 = fresh BaseBVRepr 16 v_3
% internal
$8 = fresh BaseBVRepr 16 v_4
% internal
$9 = fresh BaseBVRepr 16 v_5
% internal
$10 = fresh BaseBVRepr 16 v_6
% 5:12
$11 = vectorLit(BVRepr 16, [$4, $5, $6, $7, $8, $9, $10])
% 6:12
$12 = extensionApp(null_ptr)
% internal
$13 = (ptr_sub $0 $1)
% 7:12
$14 = extensionApp((ptr_to_bits_64 $13))
% internal
$15 = extensionApp((bits_to_ptr_64 $14))
% 8:12
$16 = (ptr_add $0 $15)
% 9:16
$17 = (ptr_sub $16 $15)
% 10:16
$18 = (ptr_eq $17 $0)
% internal
$19 = (macawReadMem bvle4 $17)
% 11:12
$20 = extensionApp((ptr_to_bits_32 $19))
% internal
$21 = extensionApp((bits_to_ptr_64 $3))
% 12:5
$22 = (macawWriteMem bvle8 $17 $21)
% 13:13
$23 = emptyApp()
% 13:5
return $23
% no postdom