SMT: Refactor overflow checks into generic event checking system

Have assert events for assertions and overflow events for potential
integer overflow. Unclear how these should interact... The order in
which such events are applied to the final assertion is potentially
quite important.

Overflow checks and assertions are now path sensitive, as they should
be.

4 files changed, 42 insertions, 0 deletions

diff --git a/test/smt/add_overflow.sat.sail b/test/smt/add_overflow.sat.sail
new file mode 100644
index 00000000..faf432e8
--- /dev/null
+++ b/test/smt/add_overflow.sat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+
+$counterexample
+function prop(x: int, y: int) -> bool = {
+  if x >= 0  & y >= 0 then {
+    x + y >= 0
+  } else true
+}
diff --git a/test/smt/add_overflow.unsat.sail b/test/smt/add_overflow.unsat.sail
new file mode 100644
index 00000000..3da55b55
--- /dev/null
+++ b/test/smt/add_overflow.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int) -> bool = {
+  if x >= 0  & y >= 0 then {
+    x + y >= 0
+  } else true
+}
diff --git a/test/smt/trivial_assert.sat.sail b/test/smt/trivial_assert.sat.sail
new file mode 100644
index 00000000..5c83f1dc
--- /dev/null
+++ b/test/smt/trivial_assert.sat.sail
@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+
+$counterexample
+function prop(x: bits(5), y: bits(5)) -> bool = {
+  assert(x == y);
+  true
+}
diff --git a/test/smt/trivial_assert_2.unsat.sail b/test/smt/trivial_assert_2.unsat.sail
new file mode 100644
index 00000000..cfc1a5f3
--- /dev/null
+++ b/test/smt/trivial_assert_2.unsat.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int) -> bool = {
+  if x != y then {
+    assert(x != y);
+    true
+  } else true
+}