From 44d533ad7e47daa636ee00a256b09fb3df9433ee Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 29 Apr 2019 20:52:18 +0100
Subject: 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.
---
 test/smt/add_overflow.sat.sail       | 12 ++++++++++++
 test/smt/add_overflow.unsat.sail     | 10 ++++++++++
 test/smt/trivial_assert.sat.sail     |  9 +++++++++
 test/smt/trivial_assert_2.unsat.sail | 11 +++++++++++
 4 files changed, 42 insertions(+)
 create mode 100644 test/smt/add_overflow.sat.sail
 create mode 100644 test/smt/add_overflow.unsat.sail
 create mode 100644 test/smt/trivial_assert.sat.sail
 create mode 100644 test/smt/trivial_assert_2.unsat.sail

(limited to 'test')

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
+}
-- 
cgit v1.2.3