From 0b0805cf17aeb6a6cd0a7ed3f47ad8f0b4a3407b Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Fri, 9 Apr 2021 18:10:44 +0200 Subject: scheck: assert_const() 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 --- ident-list.h | 1 + scheck.c | 19 +++++++++++++++++++ validation/scheck/ok.c | 1 + 3 files changed, 21 insertions(+) diff --git a/ident-list.h b/ident-list.h index ab5bc5f5..6264fd06 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 efa5c1c3..f5ea4cf1 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 f4a0daab..8f65013e 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) -- cgit 1.2.3-korg