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

GaloisInc · Nov 2, 2023 · 19f0a57 · 19f0a57
1 parent a2ac7f4
commit 19f0a57
Show file tree

Hide file tree

Showing 3 changed files with 137 additions and 0 deletions.
diff --git a/symbolic-syntax/test-data/ops.cbl b/symbolic-syntax/test-data/ops.cbl
@@ -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 ())))
diff --git a/symbolic-syntax/test-data/ops.out b/symbolic-syntax/test-data/ops.out
@@ -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
diff --git a/symbolic-syntax/test-data/ops.out.good b/symbolic-syntax/test-data/ops.out.good
@@ -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