[v2,7/8] scheck: assert_const()

Commit Message

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

Since, the symbolic checker check expressions at the ... symbolic
level, this can be used to check if two expressions are equivalent
but not if this equivalence is effectively used.

So, add a new assertion (this time not at the symbolic level) to
check if an expression which is expected to simplify to a constant
is effectively simplified to this constant.

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

Patch

diff --git a/ident-list.h b/ident-list.h
index ab5bc5f52e01..6264fd062534 100644
--- a/ident-list.h
+++ b/ident-list.h
@@ -81,6 +81,7 @@  IDENT(main);
 /* used by the symbolic checker */
 IDENT(__assert);
 IDENT(__assert_eq);
+IDENT(__assert_const);
 
 #undef __IDENT
 #undef IDENT
diff --git a/scheck.c b/scheck.c
index efa5c1c3247b..f5ea4cf11902 100644
--- a/scheck.c
+++ b/scheck.c
@@ -33,6 +33,7 @@ 
 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 },
+	{ "__assert_const", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
 	{}
 };
 
@@ -233,6 +234,22 @@  static bool check_equal(Btor *btor, struct instruction *insn)
 	return check_btor(btor, n, insn);
 }
 
+static bool check_const(Btor *ctxt, struct instruction *insn)
+{
+	pseudo_t src1 = ptr_list_nth(insn->arguments, 0);
+	pseudo_t src2 = ptr_list_nth(insn->arguments, 1);
+
+	if (src2->type != PSEUDO_VAL)
+		sparse_error(insn->pos, "should be a constant: %s", show_pseudo(src2));
+	if (src1 == src2)
+		return 1;
+	if (src1->type != PSEUDO_VAL)
+		sparse_error(insn->pos, "not a constant: %s", show_pseudo(src1));
+	else
+		sparse_error(insn->pos, "invalid value: %s != %s", show_pseudo(src1), show_pseudo(src2));
+	return 0;
+}
+
 static bool check_call(Btor *btor, struct instruction *insn)
 {
 	pseudo_t func = insn->func;
@@ -242,6 +259,8 @@  static bool check_call(Btor *btor, struct instruction *insn)
 		return check_assert(btor, insn);
 	if (ident == &__assert_eq_ident)
 		return check_equal(btor, insn);
+	if (ident == &__assert_const_ident)
+		return check_const(btor, insn);
 	return 0;
 }
 
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c
index f4a0daabfe9a..8f65013e1618 100644
--- a/validation/scheck/ok.c
+++ b/validation/scheck/ok.c
@@ -2,6 +2,7 @@  static void ok(int x)
 {
 	__assert((~x) == (~0 - x));	// true but not simplified yet
 	__assert_eq(~x, ~0 - x);
+	__assert_const(x & 0, 0);
 }
 
 static void always(int x)