| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
Casts were using the target type for their operands.
Fix this by using the new helper mkivar() for them.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
Most instructions have one associated type, the 'target type'.
Some, like compares, have another one too, the 'input type'.
So, when creating a bitvector from an instruction, we need to specify
the type in some way.
So, create an helper for both cases: mktvar() and mkivar().
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
in sparse, constants (PSEUDO_VALs) are not typed, so the same pseudo
can be used to represent 1-bit 0, 8-bit 0, 16-bit 0, ...
That's incompatible with the bit vectors used here, so we can't associate
a PSEUDO_VAL with its own bitvector like it's done for PSEUDO_REGs.
A fresh one is needed for each occurrence (we could use a small table
but won't bother).
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
Some instructions have no effects and so can just be ignored here.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
When reporting an unsupported instruction, display the instruction
together with the diagnostic message.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
It can be useful to use the same testcase for the symbolic checker
and normal sparse (or test-linearize) processing.
So, there must be a mean to somehow ignore the assertions used
for the symbolic checker when it's not used (since these are otherwise
not known to sparse).
Resolve this by adding a predefine, __SYMBOLIC_CHECKER__, to the
symbolic checker.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
A lot of simplifications are only valid when their variables
satisfy to some conditions (like "is within a given range" or
"is a power of two").
So, allow to add such pre-conditions via new _assume() statements.
Internally, all such preconditions are ANDed together and what is
checked is they imply the assertions:
AND(pre-condition) implies assertion 1
...
Note: IIUC, it seems that boolector has a native mechanism for such
things but I'm not sure if t can be used here.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
Since, the symbolic checker check expressions at the ... symbolic
level, this can be used to check if two expressions are equivalent
but not if this equivalence is effectively used.
So, add a new assertion (this time not at the symbolic level) to
check if an expression which is expected to simplify to a constant
is effectively simplified to this constant.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
With the SMT solver used here, by default, once an expression is
checked it's kinda consumed by the process and can't be reused
anymore for another check.
So, enable the incremental mode: it allows to call boolecter_sat()
several times.
Note: Another would be, of course, to just AND together all assertions
and just check this but then we would lost the finer grained
diagnostic in case of failure.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
Testing the equivalence of two sub-expressions can be done with
with a single assertion like __assert(A == B).
However, in some cases, Sparse can use the equality to simplify
the whole expression although it's unable to simplify one of
the two sub-expressions into the other.
So, add a new assertion, __assert_eq(), testing the equality of
the two expressions given in argument independently of each other.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
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>
|
