2021-04-17T13:14:26+00:00

* add a symbolic checker

2021-04-13T16:25:43+00:00

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

2021-03-21T12:45:39+00:00

Because laziness is a virtue, add an option '-r' to the 'format' subcommand of the testsuite to quickly create a test template for linearized code which should just return 1. Signed-off-by: Luc Van Oostenryck

2020-12-11T13:13:38+00:00

In testcases' tags, if a value contains 'check-' then this value will be used as the tagname instead of the value. Fix this by adding a bit more context in the regexp used for parsing these. Signed-off-by: Luc Van Oostenryck

2020-10-31T23:55:44+00:00

The current tags check-output-contains/excludes/pattern are quite powerful and the new check-output-match is easy to use but it can be even simpler. Indeed, a lot of IR simplifications/ canonicalizations can be tested by checking that the expression to be tested is equivalent to another one. This is less precise than some more specific tests but: * it's a big advantage because it's less sensitive to 'noise' like the exact number used by the pseudos or to the results of some new simplifications or canonicalizations * very often, this equivalence is what really matters and not the exact transformation. So, add a new utra-simple-to-use tag: just ask that all functions of the tests return the same specified value (usually 1): check-output-returns: Signed-off-by: Luc Van Oostenryck

2020-10-31T23:55:09+00:00

The current tags check-output-contains/excludes/pattern are quite powerful, universal, but they often need 'complex' regular expressions with escaping which make them not so nice to read. For testing IR results, a very common pattern is: this instruction must have this (kind of) operand. So, make a new tag for this. It does nothing than can't be done with done with the previous ones, on the contrary, but is much simpler to use: check-output-match(instruction): operand Signed-off-by: Luc Van Oostenryck

2020-07-04T10:16:59+00:00

This flag facilitates the creation of testcases for preprocessing. Signed-off-by: Luc Van Oostenryck

2020-06-22T23:34:11+00:00

The subcommand 'format help' is broken because the of the way arguments are parsed without validating the number of arguments. Fix this by parsing all arguments (even if there is only one) and validate the number of arguments at the end of the loop. Signed-off-by: Luc Van Oostenryck

2020-06-16T21:10:17+00:00

For some testcases, the testsuite use the command 'timeout' to ensure that the test finish after a reasonable amount of time. This is mainly used for some testcases which, in the past, were stuck in an infinite loop. This the command 'timeout' is used with an extra option (-k 1s) to issue a second kill signal in case the first one would have been ignored. However, this extra option is not supported on all implementations (Alpine) and its use seems a bit paranoid for sparse. So, remove this extra option. Signed-off-by: Luc Van Oostenryck

2019-02-07T20:56:50+00:00

This simplifies finding the offending test when the build ended with KO: out of 584 tests, 527 passed, 57 failed 56 of them are known to fail Signed-off-by: Uwe Kleine-König Signed-off-by: Luc Van Oostenryck