[0/8] scheck: add a symbolic checker for sparse

Message

Luc Van Oostenryck April 10, 2021, 1:30 p.m. UTC

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