Add visitor for simplifying Boolean and bitvector expressions

[jeroenk]

When a loop has a manually specified invariant, we speculate additional invariants irrespective of whether array access checks occur in the loop. Under normal circumstances this should be rare, and speculating invariants might still help to prove the user provided ones.

When race checking is disabled for some arrays, the above situation might might have a negative impact on verification performance: Invariants might be speculated for loops that have manually supplied invariants referring only to arrays for which race checking has been disabled. These speculated invariants need to be considered by Houdini, and since some speculated invariants state facts not related to array accesses substantial effort might be involved.

To mitigate the above situation we simplify Boolean and bitvector expressions that commonly occur in manually provided invariants. The hope is that the invariants are reduced to just "true", which stops additional invariants from being speculated.

@afd This has been in my tree for a long while. I recall that you may have had some different ideas of addressing what is described above.

[jeroenk]

Forgot to say: it's not completely clear to me how to write tests for this. It sort of requires looking at bpl files, which we could do in out testing framework, but which is a bit awkward.

[afd]

I understand the problem, and I think your solution sounds fine.

Regarding how to test it: do we have a way of looking for expected output from GPUVerify? If so then we could run GPUVerify with --verbose and --infer-info. We could then write an example that should have no associated generated invariants after your fix, and check that the Houdini assignment axiom is trivial. Makes sense?

[afd]

I looked at the patch, and it looks good. I am happy for you to merge.

[jeroenk]

--verbose and --infer-info might work. What I will do is at least add some tests that exercise the code in this merge request, and then look further in to this.

[jeroenk]

--infer-info works quite nicely:

• write an invariant that should fails when race checking for the array is enabled
• add an __assert(false) to the end of the kernel
• run with --infer_info
• check for "Houdini assignment axiom: true" and "this assertion might not hold"