From d1ab4c40982ffcfadebf3155f498469aeb1355b0 Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Fri, 9 Apr 2021 18:03:58 +0200 Subject: scheck: assert_eq() 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 --- ident-list.h | 1 + scheck.c | 11 +++++++++++ validation/scheck/ok.c | 5 +++++ 3 files changed, 17 insertions(+) diff --git a/ident-list.h b/ident-list.h index 918f54d7..ab5bc5f5 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 63cbfa2d..c64e8651 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 113912e0..76c04c4f 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 -- cgit 1.2.3-korg