From 2e3c2464ca3522fe0a6dfc93ea36c88cbe7bf117 Mon Sep 17 00:00:00 2001
From: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
Date: Fri, 9 Apr 2021 23:36:32 +0200
Subject: scheck: support pre-conditions via __assume()

A lot of simplifications are only valid when their variables
satisfy to some conditions (like "is within a given range" or
"is a power of two").

So, allow to add such pre-conditions via new _assume() statements.
Internally, all such preconditions are ANDed together and what is
checked is they imply the assertions:
	AND(pre-condition) implies assertion 1
	...

Note: IIUC, it seems that boolector has a native mechanism for such
      things but I'm not sure if t can be used here.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 ident-list.h           |  1 +
 scheck.c               | 33 ++++++++++++++++++++++++---------
 validation/scheck/ok.c |  6 ++++++
 3 files changed, 31 insertions(+), 9 deletions(-)

diff --git a/ident-list.h b/ident-list.h
index 6264fd06..3c08e8ca 100644
--- a/ident-list.h
+++ b/ident-list.h
@@ -79,6 +79,7 @@ IDENT(copy_to_user); IDENT(copy_from_user);
 IDENT(main);
 
 /* used by the symbolic checker */
+IDENT(__assume);
 IDENT(__assert);
 IDENT(__assert_eq);
 IDENT(__assert_const);
diff --git a/scheck.c b/scheck.c
index f5ea4cf1..6752b9d9 100644
--- a/scheck.c
+++ b/scheck.c
@@ -31,6 +31,7 @@
 
 #define dyntype incomplete_ctype
 static const struct builtin_fn builtins_scheck[] = {
+	{ "__assume", &void_ctype, 0, { &dyntype }, .op = &generic_int_op },
 	{ "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op },
 	{ "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
 	{ "__assert_const", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
@@ -195,11 +196,22 @@ static void ternop(Btor *btor, struct instruction *insn)
 	insn->target->priv = t;
 }
 
-static bool check_btor(Btor *btor, BoolectorNode *n, struct instruction *insn)
+static bool add_precondition(Btor *btor, BoolectorNode **pre, struct instruction *insn)
+{
+	BoolectorNode *a = get_arg(btor, insn, 0);
+	BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
+	BoolectorNode *n = boolector_ne(btor, a, z);
+	BoolectorNode *p = boolector_and(btor, *pre, n);
+	*pre = p;
+	return true;
+}
+
+static bool check_btor(Btor *btor, BoolectorNode *p, BoolectorNode *n, struct instruction *insn)
 {
 	char model_format[] = "btor";
 	int res;
 
+	n = boolector_implies(btor, p, n);
 	boolector_assert(btor, boolector_not(btor, n));
 	res = boolector_sat(btor);
 	switch (res) {
@@ -218,20 +230,20 @@ static bool check_btor(Btor *btor, BoolectorNode *n, struct instruction *insn)
 	return 0;
 }
 
-static bool check_assert(Btor *btor, struct instruction *insn)
+static bool check_assert(Btor *btor, BoolectorNode *pre, struct instruction *insn)
 {
 	BoolectorNode *a = get_arg(btor, insn, 0);
 	BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
 	BoolectorNode *n = boolector_ne(btor, a, z);
-	return check_btor(btor, n, insn);
+	return check_btor(btor, pre, n, insn);
 }
 
-static bool check_equal(Btor *btor, struct instruction *insn)
+static bool check_equal(Btor *btor, BoolectorNode *pre, struct instruction *insn)
 {
 	BoolectorNode *a = get_arg(btor, insn, 0);
 	BoolectorNode *b = get_arg(btor, insn, 1);
 	BoolectorNode *n = boolector_eq(btor, a, b);
-	return check_btor(btor, n, insn);
+	return check_btor(btor, pre, n, insn);
 }
 
 static bool check_const(Btor *ctxt, struct instruction *insn)
@@ -250,15 +262,17 @@ static bool check_const(Btor *ctxt, struct instruction *insn)
 	return 0;
 }
 
-static bool check_call(Btor *btor, struct instruction *insn)
+static bool check_call(Btor *btor, BoolectorNode **pre, struct instruction *insn)
 {
 	pseudo_t func = insn->func;
 	struct ident *ident = func->ident;
 
+	if (ident == &__assume_ident)
+		return add_precondition(btor, pre, insn);
 	if (ident == &__assert_ident)
-		return check_assert(btor, insn);
+		return check_assert(btor, *pre, insn);
 	if (ident == &__assert_eq_ident)
-		return check_equal(btor, insn);
+		return check_equal(btor, *pre, insn);
 	if (ident == &__assert_const_ident)
 		return check_const(btor, insn);
 	return 0;
@@ -267,6 +281,7 @@ static bool check_call(Btor *btor, struct instruction *insn)
 static bool check_function(struct entrypoint *ep)
 {
 	Btor *btor = boolector_new();
+	BoolectorNode *pre = boolector_true(btor);
 	struct basic_block *bb;
 	int rc = 0;
 
@@ -294,7 +309,7 @@ static bool check_function(struct entrypoint *ep)
 				ternop(btor, insn);
 				break;
 			case OP_CALL:
-				rc &= check_call(btor, insn);
+				rc &= check_call(btor, &pre, insn);
 				break;
 			case OP_RET:
 				goto out;
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c
index 8f65013e..1e5314f2 100644
--- a/validation/scheck/ok.c
+++ b/validation/scheck/ok.c
@@ -10,6 +10,12 @@ static void always(int x)
 	__assert((x - x) == 0);		// true and simplified
 }
 
+static void assumed(int x, int a, int b)
+{
+	__assume((a & ~b) == 0);
+	__assert_eq((x ^ a) | b, x | b);
+}
+
 /*
  * check-name: scheck-ok
  * check-command: scheck $file
-- 
cgit 1.2.3-korg