VSD - to predicate

[jezhiggins]

This is a way that a user of the abstract interpreter to produce a logical expression that is true for any of the possible states represented by a single domain.

For example, if we have three variables in scope and intervals for them:

• x is [0,20]
• y is [-4,3000]
• z is TOP

then to_predicate could generate

(0 <= x <= 20) && (-4 <= y <= 3000)

[codecov]

Codecov Report

Merging #6267 (7af8e92) into develop (9aff751) will increase coverage by 0.07%.
The diff coverage is 99.29%.

@@             Coverage Diff             @@
##           develop    #6267      +/-   ##
===========================================
+ Coverage    75.90%   75.97%   +0.07%     
===========================================
  Files         1492     1503      +11     
  Lines       162711   163165     +454     
===========================================
+ Hits        123508   123967     +459     
+ Misses       39203    39198       -5     

Impacted Files	Coverage Δ
...alyses/variable-sensitivity/abstract_environment.h	100.00% <ø> (ø)
...rc/analyses/variable-sensitivity/abstract_object.h	76.92% <ø> (ø)
...ses/variable-sensitivity/constant_abstract_value.h	100.00% <ø> (ø)
...ble-sensitivity/constant_pointer_abstract_object.h	100.00% <ø> (ø)
...ses/variable-sensitivity/context_abstract_object.h	85.71% <ø> (ø)
.../variable-sensitivity/full_array_abstract_object.h	100.00% <ø> (ø)
...variable-sensitivity/full_struct_abstract_object.h	100.00% <ø> (ø)
...ses/variable-sensitivity/interval_abstract_value.h	100.00% <ø> (ø)
...s/variable-sensitivity/value_set_abstract_object.h	100.00% <ø> (ø)
...le-sensitivity/value_set_pointer_abstract_object.h	100.00% <ø> (ø)
... and 41 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 25ed175...7af8e92. Read the comment docs.

[martin-cs]

Looks good. The only thing missing is pointers, which should be relatively straight-forward.

[martin-cs]

To make this more directly accessible, would it be possible to add to this PR an implementation of this interface:

cbmc/src/analyses/ai_domain.h

Line 157 in d3dc560

virtual exprt to_predicate(void) const

( as variable_sensitivity_domaint::to_predicate ). All it needs to do is to iterate over the environment map, abstract_objectt::to_predicate() each entry and give the conjunct.

Further, would it also be possible to add overloadings of variable_sensitivity_domaint::to_predicate() for:

• a single exprt : it should eval it and then abstract_objectt::to_predicate() the result.
• a vector of exprt : eval each one, abstract_objectt::to_predicate() and conjunct.

[martin-cs]

Thanks for this; looks good.