Some instruction simplifications can be quite tricky and thus easy to get wrong. Often, they are lso 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. This, combined wth some assertion at the C source level, allows to symbolically check the expressions in these assertions. In other words, it allows to check if these expressions 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". 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 | 52 +++++- builtin.h | 4 + ident-list.h | 6 + scheck.c | 348 +++++++++++++++++++++++++++++++++++++++++ validation/scheck/ko.c | 10 ++ validation/scheck/ok.c | 22 +++ validation/test-suite | 6 + 9 files changed, 472 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
