SMT cache values and handle z3 errors #6215

TGWDB · 2021-07-07T13:53:55Z

This PR contains a fix for problems due to cbmc being able to send expressions with quantifiers to z3. This creates a problem where a sat result can be followed by an attempt to (get-value |XXX|) for various identifiers XXX. However, when z3 has a quantifier in one of these identifiers this raises an error.

This PR addresses this problem by doing three things:

When we pass the solver input of the form (assert |XXX|) via the set_to function that is in turn referring to something in defined_expressions, then we also store what value we set this identifier to in set_values. (This covers various expressions, but most importantly here quantifier questions which z3 will fail to handle with (get-value |XXX|).)
When we parse output from the SMT solver if we hit an error relating to quantifiers after z3 has determined the result is sat, then we ignore this error. This would lead to us missing results from the (get-value ...) expressions except for
When parsing results, if we already know the correct response for sat because we stored it in the set_values in 1 (above), then use this instead of parsing and checking the result from the solver. This also solves the problem with z3 not being able to return the result and it being skipped in 2 (above).

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.

codecov · 2021-07-07T15:20:59Z

Codecov Report

Merging #6215 (e66aa29) into develop (d125b1a) will increase coverage by 0.07%.
The diff coverage is 89.41%.

@@             Coverage Diff             @@
##           develop    #6215      +/-   ##
===========================================
+ Coverage    75.12%   75.20%   +0.07%     
===========================================
  Files         1458     1458              
  Lines       161402   161431      +29     
===========================================
+ Hits        121261   121408     +147     
+ Misses       40141    40023     -118

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_conv.h	`100.00% <ø> (ø)`
src/solvers/smt2/smt2_dec.cpp	`74.77% <80.76%> (+3.34%)`	⬆️
src/solvers/smt2/smt2_conv.cpp	`67.16% <93.22%> (-0.03%)`	⬇️
src/goto-programs/link_goto_model.cpp	`0.00% <0.00%> (-77.97%)`	⬇️
src/ansi-c/c_typecheck_typecast.cpp	`55.00% <0.00%> (-15.00%)`	⬇️
src/ansi-c/literals/parse_float.cpp	`83.65% <0.00%> (-12.50%)`	⬇️
src/ansi-c/c_typecheck_code.cpp	`72.44% <0.00%> (-5.89%)`	⬇️
src/goto-instrument/code_contracts.cpp	`86.57% <0.00%> (+0.01%)`	⬆️
... and 11 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 54c385e...e66aa29. Read the comment docs.

TGWDB · 2021-07-08T11:01:54Z

@peterschrammel @tautschnig I would appreciate codeowner review (and ideally approved) here. I've tried to explain in the PR why this is done this way and what problem it solves. I'm also aware of critique regarding handling specific z3 errors and special cases, but since we already give this input to z3 (including in regression tests) I would argue that handling it in some form is better than simply reporting errors due to what cbmc creates internally. Also this is part of a series of fixes that AWS has found useful on a branch (https://github.com/NlightNFotis/cbmc/tree/smt_fast_response), so there is also argument from usage that this is valuable.

peterschrammel · 2021-07-09T08:30:18Z

src/solvers/smt2/smt2_dec.cpp

      }
    }
  }

+  // If the result is satisfiable don't bother updating the assignments and


Should be is NOT satisfiable ?

This was previously unimplemented, which put null expressions into the trace steps and resulted in the elements of arrays not being printed when the trace is printed.

This is a fix for how we parse Z3 array output to reconstruct values in traces. This is specific bug fix for Z3 array output.

This removes the labels on some tests that used to have the broken-smt-backend flag but now pass.

Add two regression tests to check for array output in traces.

Due to how we call z3 it is possible to have values that contain quantifiers appear in the results. However, z3 cannot give a real value in response to a "(get-value |XXX|)" request. This catches these any simply ignores them, allowing the rest of the code to continue. Note that this becomes necessary to handle since cbmc now produces quantifiers in expressions sent to z3.

This fixes some of the cases where `z3` returns an error instead of a value for some of the values cbmc is attempting to get.

Add a new regression test for error handling for z3 output that came from a Issue diffblue#5970

These various tests are either broken with error or timeout on SMT backends, in particular cprover-smt or z3. # Please enter the commit message for your changes. Lines starting

kroening · 2021-07-09T09:45:56Z

src/solvers/smt2/smt2_conv.cpp

@@ -283,6 +283,7 @@ exprt smt2_convt::get(const exprt &expr) const

    if(it!=identifier_map.end())
      return it->second.value;
+    return expr;
  }


It's wrong for get to return the symbol that it's asked to provide a model for.
The API is meant to return nil when no value is available.

This appears to have been caught from another PR/merging problem with git (and is already merged in #6210 ). That said, this fixes missing symbols in arrays when printing traces from SMT solvers.

kroening · 2021-07-09T09:48:30Z

This is a horrible hack to work around a bug in Z3.
I would much prefer to raise this with the developers of Z3.

martin-cs

I appreciate that "maybe do something else" is not a particularly helpful review comment but some general thoughts:

In SMT-LIB 2.* there is little standarization of the representation of models and values. For simple variables it is simple but for things like arrays and quantifiers it rapidly gets less obvious.
This may change in SMT-LIB 3.0. One of the reasons for adding things like lambdas to the language is to help create a way of outputting arrays and quantifiers.
As such the output is quite solver-specific.
(get-model) is a generally preferred interface than (get-value).

So, maybe the correct way to handle this is to call (get-model) and then do a solver-specific parsing of what you get?

martin-cs · 2021-07-09T10:48:47Z

regression/cbmc/union10/union_list2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend


Why does this break?

These appear to have been broken before, previous version of cbmc have errors here.

TGWDB · 2021-07-09T11:10:31Z

Broadly I agree on the points raised by both @kroening and @martin-cs , the ideal would be to do something better and not have this hack. However, the main concern here (and hence my raising this PR with the above comments/discussion) is that we are already sending "bad" input to z3 (and other solvers). The goal here is to (better) handle where we send bad input to z3 and in particular do this without major changes to how to invoke solvers. That said, feedback and commentary on how to do this right are welcome as the larger project (overview here #6134 ) can benefit from this.

TGWDB added SMT Backend Interface bugfix labels Jul 7, 2021

TGWDB requested review from allredj, kroening, martin-cs, peterschrammel, romainbrenguier and tautschnig as code owners July 7, 2021 13:53

TGWDB force-pushed the SMT-cache-values-and-handle-z3-errors branch from b51b88d to b34eb03 Compare July 7, 2021 14:11

TGWDB force-pushed the SMT-cache-values-and-handle-z3-errors branch from b34eb03 to 96898d4 Compare July 8, 2021 09:30

peterschrammel approved these changes Jul 9, 2021

View reviewed changes

Implement getting arrays from the SMT2 backend

1fc8aa5

This was previously unimplemented, which put null expressions into the trace steps and resulted in the elements of arrays not being printed when the trace is printed.

TGWDB force-pushed the SMT-cache-values-and-handle-z3-errors branch from 96898d4 to 76c8183 Compare July 9, 2021 08:49

TGWDB and others added 5 commits July 9, 2021 09:49

Fixes array value in traces for Z3 SMT

a865ede

This is a fix for how we parse Z3 array output to reconstruct values in traces. This is specific bug fix for Z3 array output.

Fix tests previously broken

94fa314

This removes the labels on some tests that used to have the broken-smt-backend flag but now pass.

Add regression tests for array output with z3

50354d6

Add two regression tests to check for array output in traces.

Use set_to to infer missing boolean identifier values

393d47a

This fixes some of the cases where `z3` returns an error instead of a value for some of the values cbmc is attempting to get.

TGWDB force-pushed the SMT-cache-values-and-handle-z3-errors branch from 76c8183 to e66aa29 Compare July 9, 2021 09:22

TGWDB added 2 commits July 9, 2021 10:23

Add regression test for new error handling

1b9bdb5

Add a new regression test for error handling for z3 output that came from a Issue diffblue#5970

Fix tags on broken SMT backend test

e66aa29

These various tests are either broken with error or timeout on SMT backends, in particular cprover-smt or z3. # Please enter the commit message for your changes. Lines starting

kroening reviewed Jul 9, 2021

View reviewed changes

martin-cs reviewed Jul 9, 2021

View reviewed changes

TGWDB merged commit 00c32e3 into diffblue:develop Jul 9, 2021

This was referenced Jul 9, 2021

SMT solver errors in counterexample extraction over quantified expressions #5970

Closed

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

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

SMT cache values and handle z3 errors #6215

SMT cache values and handle z3 errors #6215

TGWDB commented Jul 7, 2021 •

edited

Loading

codecov bot commented Jul 7, 2021 •

edited

Loading

TGWDB commented Jul 8, 2021

peterschrammel Jul 9, 2021

kroening Jul 9, 2021

TGWDB Jul 9, 2021

kroening commented Jul 9, 2021

martin-cs left a comment

martin-cs Jul 9, 2021

TGWDB Jul 9, 2021

TGWDB commented Jul 9, 2021 •

edited

Loading

SMT cache values and handle z3 errors #6215

SMT cache values and handle z3 errors #6215

Conversation

TGWDB commented Jul 7, 2021 • edited Loading

codecov bot commented Jul 7, 2021 • edited Loading

Codecov Report

TGWDB commented Jul 8, 2021

peterschrammel Jul 9, 2021

Choose a reason for hiding this comment

kroening Jul 9, 2021

Choose a reason for hiding this comment

TGWDB Jul 9, 2021

Choose a reason for hiding this comment

kroening commented Jul 9, 2021

martin-cs left a comment

Choose a reason for hiding this comment

martin-cs Jul 9, 2021

Choose a reason for hiding this comment

TGWDB Jul 9, 2021

Choose a reason for hiding this comment

TGWDB commented Jul 9, 2021 • edited Loading

TGWDB commented Jul 7, 2021 •

edited

Loading

codecov bot commented Jul 7, 2021 •

edited

Loading

TGWDB commented Jul 9, 2021 •

edited

Loading