[v2,5/8] scheck: assert_eq()

Commit Message

Luc Van Oostenryck April 12, 2021, 9:21 p.m. UTC

Testing the equivalence of two sub-expressions can be done with
with a single assertion like __assert(A == B).

However, in some cases, Sparse can use the equality to simplify
the whole expression although it's unable to simplify one of
the two sub-expressions into the other.

So, add a new assertion, __assert_eq(), testing the equality of
the two expressions given in argument independently of each other.

Signed-off-by: Luc Van Oostenryck <[e-mail]>
---
 ident-list.h           |  1 +
 scheck.c               | 11 +++++++++++
 validation/scheck/ok.c |  5 +++++
 3 files changed, 17 insertions(+)

Patch

diff --git a/ident-list.h b/ident-list.h
index 918f54d75fc4..ab5bc5f52e01 100644
--- a/ident-list.h
+++ b/ident-list.h
@@ -80,6 +80,7 @@  IDENT(main);
 
 /* used by the symbolic checker */
 IDENT(__assert);
+IDENT(__assert_eq);
 
 #undef __IDENT
 #undef IDENT
diff --git a/scheck.c b/scheck.c
index 63cbfa2d3404..c64e865136c5 100644
--- a/scheck.c
+++ b/scheck.c
@@ -32,6 +32,7 @@ 
 #define dyntype incomplete_ctype
 static const struct builtin_fn builtins_scheck[] = {
 	{ "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op },
+	{ "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
 	{}
 };
 
@@ -224,6 +225,14 @@  static bool check_assert(Btor *btor, struct instruction *insn)
 	return check_btor(btor, n, insn);
 }
 
+static bool check_equal(Btor *btor, 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);
+}
+
 static bool check_call(Btor *btor, struct instruction *insn)
 {
 	pseudo_t func = insn->func;
@@ -231,6 +240,8 @@  static bool check_call(Btor *btor, struct instruction *insn)
 
 	if (ident == &__assert_ident)
 		return check_assert(btor, insn);
+	if (ident == &__assert_eq_ident)
+		return check_equal(btor, insn);
 	return 0;
 }
 
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c
index 113912e01aad..76c04c4f6870 100644
--- a/validation/scheck/ok.c
+++ b/validation/scheck/ok.c
@@ -3,6 +3,11 @@  static void ok(int x)
 	__assert((~x) == (~0 - x));	// true but not simplified yet
 }
 
+static void also_ok(int x)
+{
+	__assert_eq(~x, ~0 - x);
+}
+
 static void always(int x)
 {
 	__assert((x - x) == 0);		// true and simplified