Allow simplification of singleton interval. #7761

NlightNFotis · 2023-06-12T08:37:30Z

Before this change, an expression like value >= 255 && value <= 255 would fail to be simplified to value == 255 by the expression simplifier.

While the simplification itself is useful, the lack of it was causing some misbehaviour in one of our backends (the old SMT one under src/solvers/smt2) because the lack of simplification resulted in less constraints being propagated to the solver, missing some assertions around the expression that was using value as the size of an array.

This was originally presented as a fix for #7690 , but #7768 is a more robust fix for that, so I'm changing the presentation of this as improvement to the expression simplifier instead of a workaround for an issue with the old SMT backend.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig · 2023-06-12T20:47:06Z

While the simplification itself is useful, the lack of it was causing some misbehaviour in one of our backends (the old SMT one under src/solvers/smt2) because the lack of simplification resulted in less constraints being propagated to the solver, missing some assertions around the expression that was using value as the size of an array.

While the simplification is nice to have we must not rely on it in our back-ends. So we also need a back-end fix here plus a test that uses —no-simplify.

codecov · 2023-06-13T17:13:41Z

Codecov Report

Patch coverage: 96.00% and project coverage change: +0.51 🎉

Comparison is base (b1d78e2) 78.06% compared to head (de8b169) 78.57%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7761      +/-   ##
===========================================
+ Coverage    78.06%   78.57%   +0.51%     
===========================================
  Files         1693     1693              
  Lines       193308   193346      +38     
===========================================
+ Hits        150899   151928    +1029     
+ Misses       42409    41418     -991

Impacted Files	Coverage Δ
src/solvers/flattening/boolbv_quantifier.cpp	`89.07% <93.75%> (-0.49%)`	⬇️
src/util/simplify_expr_boolean.cpp	`92.13% <97.05%> (+17.13%)`	⬆️

... and 53 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

NlightNFotis · 2023-06-14T10:13:55Z

@tautschnig Hi Michael, agree that this is a workaround for the issue, but also believe that the simplification has value itself.

I believe that this should go in on the basis that it sidesteps an important bug #7690, and I have also noted that we may need to do a deeper dive to fix the underlying issue at the root level, but it's also worth noting that this issue was only observed on the old SMT backend (the new SMT backend and the SAT backend both worked before).

Given that the issue is not observable on the new SMT backend however, and that it's scheduled to (eventually?) take over, it might not be worth to have deeper dive unless the issue comes up again.

thomasspriggs · 2023-06-14T16:46:48Z

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c

+
+void *smap_get(smap_t *smap, void *ptr) {
+  size_t id = __CPROVER_POINTER_OBJECT(ptr);
+  void *sptr = smap->ptrs[id];


I think this test will pass on the VS2019 job if you change this line to char *sptr = smap->ptrs[id];

Yeah that seems to work.

peterschrammel

causing some misbehaviour

What precisely does "misbehaviour" mean here?

If it returns incorrect results then I agree with @tautschnig that we need to fix our code so that we get correct results even with --no-simplify.

If it results just in a performance issue of the SMT backend then I'm fine with this PR as is.

esteffin

Few simplification can be done

esteffin · 2023-06-15T14:23:40Z

src/util/simplify_expr_boolean.cpp

+      };
+
+      // We need to match both operands, at the particular sequence we expect.
+      structure_matched |= match_first_operand(new_operands[0]);


⛏️ The variable structure_matched is set roughly 50 lines above and never used, so I suggest defining it here and assigning to match_first_operand(new_operands[0]).

bool structure_matched = match_first_operand(new_operands[0]);

Or even better
bool structure_matched = match_first_operand(new_operands[0]) && match_second_operand(new_operands[1]).

This will also be faster as the && will short-circuit if the former condition is false.

esteffin · 2023-06-15T14:30:59Z

src/util/simplify_expr_boolean.cpp

+        for(const auto &op : new_operands)
+        {
+          if(
+            const auto ge_expr =
+              expr_try_dynamic_cast<greater_than_or_equal_exprt>(op))


This loop and check are redundant.

We already know that new_operands.size() == 2 ( line 148) and that they are both greater_than_or_equal_exprt (lines 170 and 191), so I suggest to check only structure_matched && bounds.lower == bounds.higher and return new_expr{ge_expr->lhs(), ge_expr->rhs()}.

Yeah, you're right, I've changed to just handle take the info from new_operands[0] without any further processing.

esteffin · 2023-06-15T14:39:13Z

src/solvers/flattening/boolbv_quantifier.cpp

+        // If we are here, we came across a (simplified?) expression that was
+        // not anticipated - normally this would be a bug, but if you made
+        // changes to the simplifier (as an example), you would need to add an
+        // else-if branch that handles that type above.


Isn't this shouting INVARIANT loud?

No, then the comment should be changed to specify that if we are here we may have a non-simplified expression

Clarified the comment.

esteffin · 2023-06-15T14:39:59Z

regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.c

@@ -8,7 +8,7 @@ int main(int argc, char **argv)

    __CPROVER_assert(
        __CPROVER_exists { int z; (0 < z && z < 2) &&
-            __CPROVER_forall { int o; (10 < o && o < 20) ==> o > z && z == * i }},


⛏️ The commit message looks split between title and body...

NlightNFotis · 2023-06-15T16:51:17Z

@peterschrammel

Misbehaviour in this context is an assertion failing when it wouldn't fail for the SAT or the new SMT backend.

I played around with the code and there does remain an issue with the old SMT2 backend and this particular assertion if the interval is not the singleton interval (as in, the interval is wider than 1 element), so there will probably need to be a fix for that issue, but outside of that, this PR allows for improving performance, at least in the context of the SAT backend, with the following numbers coming out of the runs on the regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c test:

without optimisation:

Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.0659747s
size of program expression: 291 steps
simple slicing removed 14 assignments
Generated 157 VCC(s), 49 remaining after simplification
Runtime Postprocess Equation: 3.0125e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0392838s
Running propositional reduction
Post-processing
Runtime Post-process: 0.0141315s
Solving with MiniSAT 2.2.1 with simplifier
8868 variables, 5507 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.0464093s
Runtime decision procedure: 0.0861215s

With optimisation:

Starting Bounded Model Checking
Runtime Symex: 0.118682s
size of program expression: 288 steps
simple slicing removed 14 assignments
Generated 157 VCC(s), 48 remaining after simplification
Runtime Postprocess Equation: 2.8459e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.110274s
Running propositional reduction
Post-processing
Runtime Post-process: 0.00303258s
Solving with MiniSAT 2.2.1 with simplifier
7063 variables, 2018 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 0.003055s
Runtime decision procedure: 0.113702s

peterschrammel · 2023-06-15T17:04:59Z

Is this a general bug in the old SMT backend that non-constant dynamic object sizes lead to incorrect results?

thomasspriggs · 2023-06-15T17:29:40Z

Is this a general bug in the old SMT backend that non-constant dynamic object sizes lead to incorrect results?

The old SMT2 backend does just skip defining the object_size if it is non-constant -

cbmc/src/solvers/smt2/smt2_conv.cpp

Lines 301 to 314 in ce831a0

    
           if( 
        
             (o.id() != ID_symbol && o.id() != ID_string_constant) || 
        
             !size_expr.has_value() || !object_size.has_value()) 
        
           { 
        
             ++number; 
        
             continue; 
        
           } 
        
           out << "(assert (=> (= " 
        
               << "((_ extract " << h << " " << l << ") "; 
        
           convert_expr(ptr); 
        
           out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))" 
        
               << "(= " << id << " (_ bv" << *object_size << " " << size_width 
        
               << "))))\n";

It does this because the size term is solely implemented as a bit vector constant.

The new back end just converts the size expression into an SMT term. As such, it works for more complex expressions -

cbmc/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines 590 to 591 in ce831a0

    
           solver_process->send(object_size_function.make_definition( 
        
             object.unique_id, convert_expr_to_smt(object.size)));

For the example given in #7690 the new SMT back end produces the same verification results as the SAT backend. As in the issue is not reproducible. So this difference between the new and old SMT backends could be the source of the bug.

peterschrammel · 2023-06-15T18:15:34Z

If I understand correctly this means that the old SMT backend is simply broken (and probably has always been) and the simplification hides the bug in some specific cases.
So, in this sense this PR makes the old SMT backend practically useable in more cases, but it remains broken. I'd say this is an improvement.
Still, it would be great to fix the bug in the old backend if effort allows.

Before this change, an expression like `value >= 255 && value <= 255` would fail to be simplified to `value == 255` by the expression simplifier. While the simplification itself is useful, the *lack* of it was causing some misbehaviour in one of our backends (the old SMT one under `src/solvers/smt2`) because the lack of simplification resulted in less constraints being propagated to the solver, missing some assertions around the expression that was using `value` as the size of an array.

…on of singleton interval

…branch

remi-delmas-3000 · 2023-06-22T17:49:55Z

@NlightNFotis I ran more tests with this fix and did not observe negative effects, approving

NlightNFotis · 2023-06-22T21:16:35Z

Cheers @remi-delmas-3000 , thanks for having a look.

NlightNFotis self-assigned this Jun 12, 2023

NlightNFotis force-pushed the simplify_interval_domain branch 2 times, most recently from a00ea8e to eeff129 Compare June 12, 2023 16:10

NlightNFotis force-pushed the simplify_interval_domain branch from 54e46cd to 7714d51 Compare June 13, 2023 16:08

NlightNFotis force-pushed the simplify_interval_domain branch from 7714d51 to c9cb4c1 Compare June 14, 2023 10:08

NlightNFotis force-pushed the simplify_interval_domain branch from c9cb4c1 to d8b98b6 Compare June 14, 2023 10:14

NlightNFotis marked this pull request as ready for review June 14, 2023 10:14

NlightNFotis requested review from kroening, tautschnig, peterschrammel and martin-cs as code owners June 14, 2023 10:14

NlightNFotis force-pushed the simplify_interval_domain branch 4 times, most recently from 102f758 to 1cc4a4b Compare June 14, 2023 14:25

thomasspriggs reviewed Jun 14, 2023

View reviewed changes

NlightNFotis force-pushed the simplify_interval_domain branch 2 times, most recently from 8b29c93 to 614eaef Compare June 15, 2023 13:10

peterschrammel reviewed Jun 15, 2023

View reviewed changes

esteffin reviewed Jun 15, 2023

View reviewed changes

NlightNFotis mentioned this pull request Jun 15, 2023

Spurious pointer check violation with smt2 backend and z3 4.12.1 #7690

Closed

peterschrammel approved these changes Jun 15, 2023

View reviewed changes

esteffin approved these changes Jun 16, 2023

View reviewed changes

NlightNFotis added 4 commits June 16, 2023 11:55

Fix recognition of quantifier bounds in case of previous simplificati…

8e82b4d

…on of singleton interval

Add regression tests for simplification of singleton intervals

c5c8e62

Simplify handling of expression matching and clarify comment in else …

de8b169

…branch

NlightNFotis force-pushed the simplify_interval_domain branch from ea48112 to de8b169 Compare June 16, 2023 10:58

NlightNFotis merged commit 14fce73 into diffblue:develop Jun 22, 2023

NlightNFotis deleted the simplify_interval_domain branch June 22, 2023 20:13

NlightNFotis mentioned this pull request Oct 12, 2023

Simplification towards singleton intervals requires single variable #7954

Merged

3 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Allow simplification of singleton interval. #7761

Allow simplification of singleton interval. #7761

NlightNFotis commented Jun 12, 2023 •

edited

Loading

tautschnig commented Jun 12, 2023

codecov bot commented Jun 13, 2023 •

edited

Loading

NlightNFotis commented Jun 14, 2023

thomasspriggs Jun 14, 2023

NlightNFotis Jun 15, 2023

peterschrammel left a comment

esteffin left a comment

esteffin Jun 15, 2023

NlightNFotis Jun 16, 2023

esteffin Jun 15, 2023

NlightNFotis Jun 16, 2023

esteffin Jun 15, 2023 •

edited

Loading

NlightNFotis Jun 16, 2023

esteffin Jun 15, 2023

NlightNFotis commented Jun 15, 2023

peterschrammel commented Jun 15, 2023

thomasspriggs commented Jun 15, 2023 •

edited

Loading

peterschrammel commented Jun 15, 2023

remi-delmas-3000 commented Jun 22, 2023

NlightNFotis commented Jun 22, 2023

Allow simplification of singleton interval. #7761

Allow simplification of singleton interval. #7761

Conversation

NlightNFotis commented Jun 12, 2023 • edited Loading

tautschnig commented Jun 12, 2023

codecov bot commented Jun 13, 2023 • edited Loading

Codecov Report

NlightNFotis commented Jun 14, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel left a comment

Choose a reason for hiding this comment

esteffin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

esteffin Jun 15, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis commented Jun 15, 2023

peterschrammel commented Jun 15, 2023

thomasspriggs commented Jun 15, 2023 • edited Loading

peterschrammel commented Jun 15, 2023

remi-delmas-3000 commented Jun 22, 2023

NlightNFotis commented Jun 22, 2023

NlightNFotis commented Jun 12, 2023 •

edited

Loading

codecov bot commented Jun 13, 2023 •

edited

Loading

esteffin Jun 15, 2023 •

edited

Loading

thomasspriggs commented Jun 15, 2023 •

edited

Loading