Some instruction simplifications can be quite tricky and thus
easy to get wrong. Often, they are also hard to test (for example,
you can test them with a few input values but of course not all
combinations, it's not clear what are the conditions for which
they're valid, ...).
This series add a tool, scheck, which feeds Sparse's IR into a
bitvector SMT solver (Boolector). This, together with assertions
added at C level, allows to symbolically check the validity of these
assertions. In other words, it allows to check if these assertions
are valid for all possible values (but these expressions are limited
to pure integer expressions, so no floats, no branches, no memory
accesses, no functions calls).
Now, you may ask yourself "Nice, but how can I be sure that this
checker is working correctly?". And the answer to this question
is obviously "You should write another checker, of course. And
then another one, all the way down!".
Notes: This needs to have the SMT solver's librarie installed
and having 'BOOLECTORDIR' and 'HAVE_BOOLECTOR' configured.
Changes since v1:
* Rewrite evaluate_generic_int_op() which was very broken
(thanks to Ramsay Jones for noticing it).
* When translating compare instructions, the input bitvectors
must use the instructions' input type, not the target type).
Luc Van Oostenryck (8):
export declare_builtins()
builtin: define a symbol_op for a generic op acting on integer
.gitignore is a bit too greedy
scheck: add a symbolic checker
scheck: assert_eq()
scheck: allow multiple assertions
scheck: assert_const()
scheck: support pre-conditions via __assume()
.gitignore | 35 ++--
Makefile | 7 +
builtin.c | 63 ++++++-
builtin.h | 4 +
ident-list.h | 6 +
scheck.c | 361 +++++++++++++++++++++++++++++++++++++++++
validation/scheck/ko.c | 10 ++
validation/scheck/ok.c | 22 +++
validation/test-suite | 6 +
9 files changed, 496 insertions(+), 18 deletions(-)
create mode 100644 scheck.c
create mode 100644 validation/scheck/ko.c
create mode 100644 validation/scheck/ok.c
--
2.31.1
