Fix quantifiers for arrays only works with Z3 and CVC4 #6270

TGWDB · 2021-08-04T13:27:37Z

This commit fixes an error introduced in #5974 where quantifiers
were produced for all SMT2 solvers despite only being supported by
Z3 and CVC4. The fix here reverts to the older behaviour for other
solvers.

Fixes #6263

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.

kroening · 2021-08-04T14:40:58Z

MathSAT does not support forall either.

TGWDB · 2021-08-04T14:50:52Z

MathSAT does not support forall either.

Now we only produce the forall in the array code block for Z3 and CVC4, all other solvers will have the old code.

SaswatPadhi · 2021-08-04T15:26:19Z

src/solvers/smt2/smt2_conv.cpp

+        // The code below only works in Z3 and CVC4, it was added (and
+        // approved/merged) despite breaking other solvers.
+        // This conditional removes this for other solvers
+        if(solver == solvert::CVC4 || solver == solvert::Z3)


Thanks for fixing this. In my original commit, I didn't realize that we also support solvers that do not have quantifier support.

Instead of checking for specific solvers, should we introduce use_quantified_array_init? This can be set to true for Z3 and CVC4in the case split we have in the constructor, and we wouldn't need the solver-specific checks or the comments above and below. We use the same pattern for other solver-specific features, e.g. array of Bools support, as const support etc.

Actually, may be we should have a use_quantifier flag instead to track solvers that support quantifiers. The issue here is with the use of quantifiers, not really specific to array initialization. May be we should also go over other uses of quantifiers in this file and guard them with use_quantifier.

Agree that a flag for quantifiers is probably the better approach, the PR above is a bit limited and incomplete (also we should have a flag and not solver specific code in random places).

I've gone with a very lightweight (minimum) fix and rebase for now. Is this still blocking?

Thank you! No this isn't a blocker currently.

This commit fixes an error introduced in diffblue#5974 where quantifiers were produced for all SMT2 solvers despite only being supported by Z3 and CVC4. The fix here reverts to the older behaviour for other solvers. Fixes diffblue#6263

codecov · 2022-05-18T15:06:25Z

Codecov Report

Merging #6270 (52829ee) into develop (6baffa3) will decrease coverage by 0.02%.
The diff coverage is 18.75%.

@@             Coverage Diff             @@
##           develop    #6270      +/-   ##
===========================================
- Coverage    77.79%   77.76%   -0.03%     
===========================================
  Files         1567     1567              
  Lines       179707   179780      +73     
===========================================
+ Hits        139797   139807      +10     
- Misses       39910    39973      +63

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_conv.cpp	`65.92% <18.75%> (-1.57%)`	⬇️
src/util/find_symbols.cpp	`65.71% <0.00%> (-18.45%)`	⬇️
src/ansi-c/cprover_library.cpp	`87.50% <0.00%> (-10.12%)`	⬇️
src/goto-checker/solver_factory.cpp	`69.31% <0.00%> (-7.25%)`	⬇️
src/goto-instrument/accelerate/scratch_program.cpp	`50.51% <0.00%> (-1.00%)`	⬇️
src/pointer-analysis/goto_program_dereference.cpp	`56.80% <0.00%> (-0.69%)`	⬇️
src/analyses/goto_rw.h	`74.50% <0.00%> (-0.50%)`	⬇️
src/util/std_expr.h	`92.94% <0.00%> (-0.43%)`	⬇️
src/cpp/cpp_convert_type.cpp	`73.41% <0.00%> (-0.16%)`	⬇️
... and 53 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 5c974cc...52829ee. Read the comment docs.

tautschnig · 2022-05-19T09:20:09Z

src/solvers/smt2/smt2_conv.cpp

+        // else
+        // {
+        //   // This is where an alternate for other solvers that does not use
+        //   // quantifiers should go.
+        // }


We should not silently do this. It's ok to fail an invariant, but let's please not generate incomplete formulae without telling the user.

tautschnig · 2022-05-23T12:14:12Z

@TGWDB Thank you for adding the invariant. This is now, not unexpectedly, failing in some tests. I'd suggest to reinstate the regex pattern in the test, and mark the test as known-broken.

This adds an invariant failure when correct SMT output would not be produced.

This marks two tests as KNOWNBUG due to them failing here.

kroening

This needs more work -- the array_of expression is an array constructor for an array that maps all indices to one value. Various solvers do support SMT2-LIB array constructor expressions, which should be used here.

kroening · 2022-05-23T13:40:02Z

Perhaps a bit more controversial, we could consider dropping support for solvers that support neither as const nor the alternative that uses quantifiers. You won't get anything through CBMC without at least one of these.

TGWDB · 2022-06-06T08:29:23Z

@kroening I agree that this PR does not correctly solve all the issues with various solvers. This was intended to be a sport fix for an issue introduced in a prior PR that allowed us to crash some solvers. Instead now this produces an error from CBMC (where we should be building something better). With that in mind, would you be willing to accept this spot fix since in practice this is a fix to the output/failure behaviour? (Also in the context where a new SMT backend is being developer, which may deprecate this code path or enable a better solution in future.)

TGWDB requested review from allredj, kroening, martin-cs, peterschrammel, romainbrenguier and tautschnig as code owners August 4, 2021 13:27

TGWDB added bugfix SMT Backend Interface labels Aug 4, 2021

SaswatPadhi suggested changes Aug 4, 2021

View reviewed changes

tautschnig assigned TGWDB Aug 11, 2021

TGWDB mentioned this pull request Sep 2, 2021

Incorrect (hard-coded) logic for SMT backend #5977

Closed

TGWDB force-pushed the array_quantifier_safety_z3_cvc4 branch from 4a1fab6 to 650d458 Compare May 12, 2022 14:51

TGWDB requested review from thomasspriggs and NlightNFotis as code owners May 12, 2022 14:51

TGWDB marked this pull request as draft May 12, 2022 14:52

TGWDB added work in progress and removed work in progress labels May 12, 2022

TGWDB marked this pull request as ready for review May 18, 2022 15:03

SaswatPadhi approved these changes May 18, 2022

View reviewed changes

tautschnig assigned kroening, NlightNFotis, martin-cs, thomasspriggs and peterschrammel and unassigned TGWDB May 19, 2022

NlightNFotis approved these changes May 19, 2022

View reviewed changes

tautschnig requested changes May 19, 2022

View reviewed changes

tautschnig assigned TGWDB and tautschnig and unassigned kroening, NlightNFotis, peterschrammel, martin-cs and thomasspriggs May 19, 2022

tautschnig approved these changes May 23, 2022

View reviewed changes

tautschnig removed their assignment May 23, 2022

TGWDB added 2 commits May 23, 2022 14:00

Add invariant failure on case where correct SMT is not produced

00ec951

This adds an invariant failure when correct SMT output would not be produced.

Mark known failing tests as KNOWNBUG

52829ee

This marks two tests as KNOWNBUG due to them failing here.

TGWDB force-pushed the array_quantifier_safety_z3_cvc4 branch from b342ddc to 52829ee Compare May 23, 2022 13:12

kroening requested changes May 23, 2022

View reviewed changes

TGWDB closed this Oct 11, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Fix quantifiers for arrays only works with Z3 and CVC4 #6270

Fix quantifiers for arrays only works with Z3 and CVC4 #6270

Uh oh!

TGWDB commented Aug 4, 2021

Uh oh!

kroening commented Aug 4, 2021

Uh oh!

TGWDB commented Aug 4, 2021

Uh oh!

SaswatPadhi Aug 4, 2021 •

edited

Loading

Uh oh!

TGWDB Aug 9, 2021

Uh oh!

TGWDB May 18, 2022

Uh oh!

SaswatPadhi May 18, 2022

Uh oh!

codecov bot commented May 18, 2022 •

edited

Loading

Uh oh!

tautschnig May 19, 2022

Uh oh!

tautschnig commented May 23, 2022

Uh oh!

kroening left a comment

Uh oh!

kroening commented May 23, 2022

Uh oh!

TGWDB commented Jun 6, 2022

Uh oh!

Uh oh!

Fix quantifiers for arrays only works with Z3 and CVC4 #6270

Fix quantifiers for arrays only works with Z3 and CVC4 #6270

Uh oh!

Conversation

TGWDB commented Aug 4, 2021

Uh oh!

kroening commented Aug 4, 2021

Uh oh!

TGWDB commented Aug 4, 2021

Uh oh!

SaswatPadhi Aug 4, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

TGWDB Aug 9, 2021

Choose a reason for hiding this comment

Uh oh!

TGWDB May 18, 2022

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi May 18, 2022

Choose a reason for hiding this comment

Uh oh!

codecov bot commented May 18, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

tautschnig May 19, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig commented May 23, 2022

Uh oh!

kroening left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented May 23, 2022

Uh oh!

TGWDB commented Jun 6, 2022

Uh oh!

Uh oh!

SaswatPadhi Aug 4, 2021 •

edited

Loading

codecov bot commented May 18, 2022 •

edited

Loading