Simplify IntDomTuple witness invariants
#1517
Conversation
I think congruences are enabled by the autotuner. |
Sorry, yes. I meant that just about interval sets. |
sim642
force-pushed
the
witness-invariant-int
branch
from
0afc2c8 to
02ef2f9
Compare
|
There's now an option to disable these simplifications. This includes the possibility to even disable the definite integer simplification. |
| | None -> | ||
| let is = to_list (mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.invariant_ikind e ik } x) | ||
| in List.fold_left (fun a i -> | ||
| let invariant_ikind e ik ((_, _, _, x_cong, x_intset) as x) = |
There was a problem hiding this comment.
What do you think of doing a single refine call before generating invariant? This would ensure things such as inclusion sets being more precise than intervals etc.
There was a problem hiding this comment.
I looked at it now and the refinement wouldn't actually ensure that because we're missing a number of refinement directions at least. I added some TODOs about them.
CHANGES: Functionally equivalent to Goblint in SV-COMP 2025. * Add 32bit vs 64bit architecture support (goblint/analyzer#54, goblint/analyzer#1574). * Add per-function context gas analysis (goblint/analyzer#1569, goblint/analyzer#1570, goblint/analyzer#1598). * Adapt automatic static loop unrolling (goblint/analyzer#1516, goblint/analyzer#1582, goblint/analyzer#1583, goblint/analyzer#1584, goblint/analyzer#1590, goblint/analyzer#1595, goblint/analyzer#1599). * Adapt automatic configuration tuning (goblint/analyzer#1450, goblint/analyzer#1612, goblint/analyzer#1181, goblint/analyzer#1604). * Simplify non-relational integer invariants in witnesses (goblint/analyzer#1517). * Fix excessive hash collisions (goblint/analyzer#1594, goblint/analyzer#1602). * Clean up various code (goblint/analyzer#1095, goblint/analyzer#1523, goblint/analyzer#1554, goblint/analyzer#1575, goblint/analyzer#1588, goblint/analyzer#1597, goblint/analyzer#1614).
Before this PR,
IntDomTupleoutputted 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:
x != 0which 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
ana.base.invariant.int.simplify.