From 7dc18d54da0804c9a99bd91eda2bc17b419d426e Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 19 Apr 2019 19:57:17 +0100
Subject: SMT: Support writing to register references

Add a new AE_write_ref constructor in the ANF representation to
make writes to register references explicit in Jib_compile
---
 test/smt/write_ref.sat.sail   | 28 ++++++++++++++++++++++++++++
 test/smt/write_ref.unsat.sail | 28 ++++++++++++++++++++++++++++
 2 files changed, 56 insertions(+)
 create mode 100644 test/smt/write_ref.sat.sail
 create mode 100644 test/smt/write_ref.unsat.sail

(limited to 'test')

diff --git a/test/smt/write_ref.sat.sail b/test/smt/write_ref.sat.sail
new file mode 100644
index 00000000..637f5808
--- /dev/null
+++ b/test/smt/write_ref.sat.sail
@@ -0,0 +1,28 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R0 : bits(32)
+register R1 : bits(32)
+register R2 : bits(32)
+register R3 : bits(32)
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+let GPRs = [ref R3, ref R2, ref R1, ref R0]
+
+function wGPR(n: range(0, 3), v: bits(32)) -> unit = {
+  (*GPRs[n]) = v
+}
+
+function rGPR(n: range(0, 3)) -> bits(32) = {
+  reg_deref(GPRs[n])
+}
+
+overload R = {wGPR, rGPR}
+
+$property
+function prop() -> bool = {
+  R(0) = 0x1234_5679;
+  R(0) == 0x1234_5678
+}
diff --git a/test/smt/write_ref.unsat.sail b/test/smt/write_ref.unsat.sail
new file mode 100644
index 00000000..4f786907
--- /dev/null
+++ b/test/smt/write_ref.unsat.sail
@@ -0,0 +1,28 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R0 : bits(32)
+register R1 : bits(32)
+register R2 : bits(32)
+register R3 : bits(32)
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+let GPRs = [ref R3, ref R2, ref R1, ref R0]
+
+function wGPR(n: range(0, 3), v: bits(32)) -> unit = {
+  (*GPRs[n]) = v
+}
+
+function rGPR(n: range(0, 3)) -> bits(32) = {
+  reg_deref(GPRs[n])
+}
+
+overload R = {wGPR, rGPR}
+
+$property
+function prop() -> bool = {
+  R(0) = 0x1234_5678;
+  R(0) == 0x1234_5678
+}
-- 
cgit v1.2.3