diff options
| author | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2021-04-09 00:07:40 +0200 |
|---|---|---|
| committer | Luc Van Oostenryck <luc.vanoostenryck@gmail.com> | 2021-04-13 18:25:43 +0200 |
| commit | 7a9fab6984f7bce3fd52809ecf6e21b79f115be3 (patch) | |
| tree | f2f9d729884c61e186ac2ad82751b4e354430646 /validation | |
| parent | 4806f30a473ca70ffee3b10136f7ee8ea2b36f6f (diff) | |
| download | sparse-dev-7a9fab6984f7bce3fd52809ecf6e21b79f115be3.tar.gz | |
scheck: add a symbolic checker
Some instruction simplifications can be quite tricky and thus easy to
get wrong. Often, they also are hard to test (for example, you can
test it with a few input values but of course not all combinations).
I'm used to validate some of these with an independent tool
(Alive cfr. [1], [2]) which is quite neat but has some issues:
1) This tool doesn't work with Sparse's IR or C source but it needs to
have the tests written in its own language (very close to LLVM's IR).
So it can be used to test if the logic of a simplification but
not if implemented correctly.
2) This tool isn't maintained anymore (has some bugs too) and it's
successor (Alive2 [3]) is not quite as handy to me (I miss the
pre-conditions a lot).
So, this patch implement the same idea but fully integrated with
Sparse. This mean that you can write a test in C, let Sparse process
and simplify it and then directly validate it and not only for
a few values but symbolically, for all possible values.
Note: Of course, this is not totally stand-alone and depends on
an external library for the solver (Boolector, see [4], [5]).
Note: Currently, it's just a proof of concept and, except the
included tests, it's only very slightly tested (and untested
with anything more complex than a few instructions).
[1] https://blog.regehr.org/archives/1170
[2] https://www.cs.utah.edu/~regehr/papers/pldi15.pdf
[3] https://blog.regehr.org/archives/1722
[4] https://boolector.github.io/
[5] https://boolector.github.io/papers/BrummayerBiere-TACAS09.pdf
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
Diffstat (limited to 'validation')
| -rw-r--r-- | validation/scheck/ko.c | 10 | ||||
| -rw-r--r-- | validation/scheck/ok.c | 14 | ||||
| -rwxr-xr-x | validation/test-suite | 6 |
3 files changed, 30 insertions, 0 deletions
diff --git a/validation/scheck/ko.c b/validation/scheck/ko.c new file mode 100644 index 00000000..dbd861ea --- /dev/null +++ b/validation/scheck/ko.c @@ -0,0 +1,10 @@ +static void ko(int x) +{ + __assert((~x) == (~0 + x)); +} + +/* + * check-name: scheck-ko + * check-command: scheck $file + * check-known-to-fail + */ diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c new file mode 100644 index 00000000..113912e0 --- /dev/null +++ b/validation/scheck/ok.c @@ -0,0 +1,14 @@ +static void ok(int x) +{ + __assert((~x) == (~0 - x)); // true but not simplified yet +} + +static void always(int x) +{ + __assert((x - x) == 0); // true and simplified +} + +/* + * check-name: scheck-ok + * check-command: scheck $file + */ diff --git a/validation/test-suite b/validation/test-suite index 1b05c75e..2f7950ef 100755 --- a/validation/test-suite +++ b/validation/test-suite @@ -13,6 +13,9 @@ prog_name=`basename $0` if [ ! -x "$default_path/sparse-llvm" ]; then disabled_cmds="sparsec sparsei sparse-llvm sparse-llvm-dis" fi +if [ ! -x "$default_path/scheck" ]; then + disabled_cmds="$disabled_cmds scheck" +fi # flags: # - some tests gave an unexpected result @@ -513,6 +516,7 @@ echo " -a append the created test to the input file" echo " -f write a test known to fail" echo " -l write a test for linearized code" echo " -p write a test for pre-processing" +echo " -s write a test for symbolic checking" echo echo "argument(s):" echo " file file containing the test case(s)" @@ -540,6 +544,8 @@ do_format() linear=1 ;; -p) def_cmd='sparse -E $file' ;; + -s) + def_cmd='scheck $file' ;; help|-*) do_format_help |