From b8f0a4e79749278f18e2e98f87a817e27a15c9ef Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 17 Apr 2019 15:54:52 +0100
Subject: SMT: Support generic vectors and handle lets between specs and
 functions

If we have e.g.

$property
val prop : ...

let X = 0

function prop(...) = X == ...

then we need to ensure that let X is included when we generate the
property.
---
 test/smt/foreach_simple_2.unsat.sail | 15 +++++++++++++++
 test/smt/gvector.unsat.sail          | 15 +++++++++++++++
 test/smt/gvector_trivial.unsat.sail  | 11 +++++++++++
 test/smt/let_intervene.unsat.sail    | 18 ++++++++++++++++++
 4 files changed, 59 insertions(+)
 create mode 100644 test/smt/foreach_simple_2.unsat.sail
 create mode 100644 test/smt/gvector.unsat.sail
 create mode 100644 test/smt/gvector_trivial.unsat.sail
 create mode 100644 test/smt/let_intervene.unsat.sail

(limited to 'test')

diff --git a/test/smt/foreach_simple_2.unsat.sail b/test/smt/foreach_simple_2.unsat.sail
new file mode 100644
index 00000000..ce466044
--- /dev/null
+++ b/test/smt/foreach_simple_2.unsat.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+let C = 0
+
+$property
+function prop() -> bool = {
+  let n = 3;
+  bv = 0x0;
+  foreach (i from C to n) {
+    bv[i] = bitone
+  };
+  bv == 0xF
+}
diff --git a/test/smt/gvector.unsat.sail b/test/smt/gvector.unsat.sail
new file mode 100644
index 00000000..23054765
--- /dev/null
+++ b/test/smt/gvector.unsat.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : vector(32, dec, vector(32, dec, bit))
+
+type is_reg('n: Int) -> Bool = 0 <= 'n <= 31
+
+$property
+function prop forall 'n, is_reg('n). (n: int('n)) -> bool = {
+  foreach (i from 0 to 31) {
+    R[i] = 0xDEAD_BEEF;
+  };
+  R[n] == 0xDEAD_BEEF
+}
\ No newline at end of file
diff --git a/test/smt/gvector_trivial.unsat.sail b/test/smt/gvector_trivial.unsat.sail
new file mode 100644
index 00000000..37a4fbed
--- /dev/null
+++ b/test/smt/gvector_trivial.unsat.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : vector(32, dec, vector(32, dec, bit))
+
+$property
+function prop() -> bool = {
+  R[0] = 0xDEAD_BEEF;
+  R[0] == 0xDEAD_BEEF
+}
\ No newline at end of file
diff --git a/test/smt/let_intervene.unsat.sail b/test/smt/let_intervene.unsat.sail
new file mode 100644
index 00000000..5494848b
--- /dev/null
+++ b/test/smt/let_intervene.unsat.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+val prop : unit -> bool
+
+let C = 0
+let x = bitone
+
+function prop() = {
+  let n = 3;
+  bv = 0x0;
+  foreach (i from C to n) {
+    bv[i] = x
+  };
+  bv == 0xF
+}
-- 
cgit v1.2.3