search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Simplify `IntDomTuple` witness invariants #1517

Open sim642 opened 2 weeks ago

sim642 commented 2 weeks ago

Before this PR, IntDomTuple outputted witness invariants as conjunction of those from each int domain. Except when it was a definite integer, then only the single equality was returned.

This PR extends this logic to avoid obviously redundant and duplicate information in witness invariants, which can make them annoyingly large:

  1. If it is a definite integer, output single equality.
  2. If it is inclusion set, output conjunction of equalities (interval bounds and exclusions are redundant).
  3. Otherwise, output interval bounds based on all integer domains (avoids duplicate bounds from def_exc exclusion bit ranges). Moreover, exclusion set is filtered based on that interval because often def_exc has x != 0 which is pointless if interval has some strictly positive bounds. Congruence and interval set (latter not used in SV-COMP) domains are added unchanged, so all known information should still be there.

TODO

michael-schwarz commented 2 weeks ago

Congruence ... (not used in SV-COMP)

I think congruences are enabled by the autotuner.

sim642 commented 2 weeks ago

I think congruences are enabled by the autotuner.

Sorry, yes. I meant that just about interval sets.

sim642 commented 6 days ago

There's now an option to disable these simplifications. This includes the possibility to even disable the definite integer simplification. These simplifications are the default, to give nicest output out of the box. If this turns out to not be precise enough and the abstract values are better, the option can be changed. Although it would be nicer to improve all simplifications for such cases as well, if possible.