diff --git a/regression/cbmc/Float-div3/test.desc b/regression/cbmc/Float-div3/test.desc index b7d95a28215..e40801d9f85 100644 --- a/regression/cbmc/Float-div3/test.desc +++ b/regression/cbmc/Float-div3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc index 46ce7f990fa..b1a5226b9b1 100644 --- a/regression/cbmc/Quantifiers-assertion/test.desc +++ b/regression/cbmc/Quantifiers-assertion/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc index a584f718857..91fdb54f4e1 100644 --- a/regression/cbmc/Quantifiers-assignment/test.desc +++ b/regression/cbmc/Quantifiers-assignment/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc index 0797ac525b4..0269bf6e9a7 100644 --- a/regression/cbmc/Quantifiers-if/test.desc +++ b/regression/cbmc/Quantifiers-if/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc index ab42e172aea..e841114af5f 100644 --- a/regression/cbmc/Quantifiers-initialisation2/test.desc +++ b/regression/cbmc/Quantifiers-initialisation2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-not-exists/fixed.desc b/regression/cbmc/Quantifiers-not-exists/fixed.desc index 6d41315fd94..4e784a1b684 100644 --- a/regression/cbmc/Quantifiers-not-exists/fixed.desc +++ b/regression/cbmc/Quantifiers-not-exists/fixed.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend fixed.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc index 815e388b2d0..50b7285586e 100644 --- a/regression/cbmc/Quantifiers-not/test.desc +++ b/regression/cbmc/Quantifiers-not/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc index f12ffbd5519..802c82dac74 100644 --- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc +++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/enum-trace1/test_json.desc b/regression/cbmc/enum-trace1/test_json.desc index 255c95b8c1c..6619fc73eea 100644 --- a/regression/cbmc/enum-trace1/test_json.desc +++ b/regression/cbmc/enum-trace1/test_json.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --json-ui --function test --trace activate-multi-line-match diff --git a/regression/cbmc/json-interface1/test.desc b/regression/cbmc/json-interface1/test.desc index 5ea8fe3d74c..a15a7b20943 100644 --- a/regression/cbmc/json-interface1/test.desc +++ b/regression/cbmc/json-interface1/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE --json-interface < test.json activate-multi-line-match diff --git a/regression/cbmc/json1/test.desc b/regression/cbmc/json1/test.desc index bf66d83d928..b9eb6a30118 100644 --- a/regression/cbmc/json1/test.desc +++ b/regression/cbmc/json1/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --json-ui --stop-on-fail activate-multi-line-match diff --git a/regression/cbmc/union10/union_list2.desc b/regression/cbmc/union10/union_list2.desc index 613581a5fc8..88bd7d7090e 100644 --- a/regression/cbmc/union10/union_list2.desc +++ b/regression/cbmc/union10/union_list2.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend union_list2.c ^EXIT=0$ diff --git a/regression/cbmc/union11/union_list.desc b/regression/cbmc/union11/union_list.desc index e4d3a427794..4d4566283f4 100644 --- a/regression/cbmc/union11/union_list.desc +++ b/regression/cbmc/union11/union_list.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend union_list.c ^EXIT=0$ diff --git a/regression/cbmc/z3/Issue5970.c b/regression/cbmc/z3/Issue5970.c new file mode 100644 index 00000000000..9831e79672e --- /dev/null +++ b/regression/cbmc/z3/Issue5970.c @@ -0,0 +1,11 @@ +#include + +void main() +{ + unsigned A, x[64]; + // clang-format off + __CPROVER_assume(0 <= A && A < 64); + __CPROVER_assume(__CPROVER_forall { int i ; (0 <= i && i < A) ==> x[i] >= 1 }); + // clang-format on + assert(x[0] > 0); +} diff --git a/regression/cbmc/z3/Issue5970.desc b/regression/cbmc/z3/Issue5970.desc new file mode 100644 index 00000000000..5c85d8d81d7 --- /dev/null +++ b/regression/cbmc/z3/Issue5970.desc @@ -0,0 +1,12 @@ +CORE smt-backend broken-cprover-smt-backend +Issue5970.c +--z3 +^EXIT=10$ +^SIGNAL=0$ +^\[main\.assertion\.1\] line [0-9]+ assertion x\[0\] > 0: FAILURE$ +-- +invalid get-value term, term must be ground and must not contain quantifiers +^\[main\.assertion\.1\] line [0-9]+ assertion x\[0\] > 0: ERROR$ +-- +This tests that attempts to "(get-value |XXX|)" from z3 sat results +are handled and do not cause an error message or ERROR result. diff --git a/regression/cbmc/z3/trace-char.c b/regression/cbmc/z3/trace-char.c new file mode 100644 index 00000000000..18308105a75 --- /dev/null +++ b/regression/cbmc/z3/trace-char.c @@ -0,0 +1,5 @@ +void main(int argc, char **argv) +{ + char arr[] = {'0', '1', '2', '3', '4', '5', '6', '7'}; + assert(arr[0] == '2'); +} diff --git a/regression/cbmc/z3/trace-char.desc b/regression/cbmc/z3/trace-char.desc new file mode 100644 index 00000000000..ee19e04f73b --- /dev/null +++ b/regression/cbmc/z3/trace-char.desc @@ -0,0 +1,13 @@ +CORE smt-backend broken-cprover-smt-backend +trace-char.c +--trace --smt2 --z3 +^EXIT=10$ +^SIGNAL=0$ +arr=\{ arr +arr=\{ '0', '1', '2', '3', '4', '5', '6', '7' \} +-- +arr=(assignment removed) +error running SMT2 solver +-- +Run cbmc with the --z3 and --trace options with arrays to confirm that +char arrays are displayed in traces. diff --git a/regression/cbmc/z3/trace.c b/regression/cbmc/z3/trace.c new file mode 100644 index 00000000000..7e842774d2c --- /dev/null +++ b/regression/cbmc/z3/trace.c @@ -0,0 +1,5 @@ +void main(int argc, char **argv) +{ + int arr[] = {0, 1, 2, 3, 4, 5, 6, 17}; + assert(arr[0] == 2); +} diff --git a/regression/cbmc/z3/trace.desc b/regression/cbmc/z3/trace.desc new file mode 100644 index 00000000000..3900217e56b --- /dev/null +++ b/regression/cbmc/z3/trace.desc @@ -0,0 +1,13 @@ +CORE smt-backend broken-cprover-smt-backend +trace.c +--trace --smt2 --z3 +^EXIT=10$ +^SIGNAL=0$ +arr=\{ arr +arr=\{ 0, 1, 2, 3, 4, 5, 6, 17 \} +-- +arr=(assignment removed) +error running SMT2 solver +-- +Run cbmc with the --z3 and --trace options with arrays to confirm that +int arrays are displayed in traces. diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 3b4fa14e4f0..21322120357 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/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; } else if(expr.id()==ID_nondet_symbol) { @@ -319,6 +320,15 @@ exprt smt2_convt::get(const exprt &expr) const } else if(expr.is_constant()) return expr; + else if(const auto &array = expr_try_dynamic_cast(expr)) + { + exprt array_copy = *array; + for(auto &element : array_copy.operands()) + { + element = get(element); + } + return array_copy; + } return nil_exprt(); } @@ -464,31 +474,85 @@ constant_exprt smt2_convt::parse_literal( exprt smt2_convt::parse_array( const irept &src, const array_typet &type) +{ + std::unordered_map operands_map; + walk_array_tree(&operands_map, src, type); + exprt::operandst operands; + // Try to find the default value, if there is none then set it + auto maybe_default_op = operands_map.find(-1); + exprt default_op; + if(maybe_default_op == operands_map.end()) + default_op = nil_exprt(); + else + default_op = maybe_default_op->second; + int64_t i = 0; + auto maybe_size = numeric_cast(type.size()); + if(maybe_size.has_value()) + { + while(i < maybe_size.value()) + { + auto found_op = operands_map.find(i); + if(found_op != operands_map.end()) + operands.emplace_back(found_op->second); + else + operands.emplace_back(default_op); + i++; + } + } + else + { + // Array size is unknown, keep adding with known indexes in order + // until we fail to find one. + auto found_op = operands_map.find(i); + while(found_op != operands_map.end()) + { + operands.emplace_back(found_op->second); + i++; + found_op = operands_map.find(i); + } + operands.emplace_back(default_op); + } + return array_exprt(operands, type); +} + +void smt2_convt::walk_array_tree( + std::unordered_map *operands_map, + const irept &src, + const array_typet &type) { if(src.get_sub().size()==4 && src.get_sub()[0].id()=="store") { + // This is the SMT syntax being parsed here // (store array index value) - if(src.get_sub().size()!=4) - return nil_exprt(); - - exprt array=parse_array(src.get_sub()[1], type); - exprt index=parse_rec(src.get_sub()[2], type.size().type()); - exprt value=parse_rec(src.get_sub()[3], type.subtype()); - - return with_exprt(array, index, value); + // Recurse + walk_array_tree(operands_map, src.get_sub()[1], type); + const auto index_expr = parse_rec(src.get_sub()[2], type.size().type()); + const constant_exprt index_constant = to_constant_expr(index_expr); + mp_integer tempint; + bool failure = to_integer(index_constant, tempint); + if(failure) + return; + long index = tempint.to_long(); + exprt value = parse_rec(src.get_sub()[3], type.subtype()); + operands_map->emplace(index, value); + } + else if(src.get_sub().size() == 3 && src.get_sub()[0].id() == "let") + { + // This is produced by Z3 + // (let (....) (....)) + walk_array_tree( + operands_map, src.get_sub()[1].get_sub()[0].get_sub()[1], type); + walk_array_tree(operands_map, src.get_sub()[2], type); } else if(src.get_sub().size()==2 && src.get_sub()[0].get_sub().size()==3 && src.get_sub()[0].get_sub()[0].id()=="as" && src.get_sub()[0].get_sub()[1].id()=="const") { - // This is produced by Z3. - // ((as const (Array (_ BitVec 64) (_ BitVec 8))) #x00))) - exprt value=parse_rec(src.get_sub()[1], type.subtype()); - return array_of_exprt(value, type); + // (as const type_info default_value) + exprt default_value = parse_rec(src.get_sub()[1], type.subtype()); + operands_map->emplace(-1, default_value); } - else - return nil_exprt(); } exprt smt2_convt::parse_union( @@ -4351,6 +4415,7 @@ void smt2_convt::set_to(const exprt &expr, bool value) // This is a converted expression, we can just assert the literal name // since the expression is already defined out << found_literal->second; + set_values[found_literal->second] = value; } else { diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index e1a65ff2fb5..d233575d96d 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -159,8 +159,23 @@ class smt2_convt : public stack_decision_proceduret constant_exprt parse_literal(const irept &, const typet &type); struct_exprt parse_struct(const irept &s, const struct_typet &type); exprt parse_union(const irept &s, const union_typet &type); + /// This function is for parsing array output from SMT solvers + /// when "(get-value |???|)" returns an array object. + /// \param s: is the irept parsed from the SMT output + /// \param type: is the expected type + /// \returns an exprt that represents the array exprt parse_array(const irept &s, const array_typet &type); exprt parse_rec(const irept &s, const typet &type); + /// This function walks the SMT output and populates a + /// map with index/value pairs for the array + /// \param operands_map: is a map of the operands to the array + /// being constructed indexed by their index. + /// \param src: is the irept source for the SMT output + /// \param type: is the type of the array + void walk_array_tree( + std::unordered_map *operands_map, + const irept &src, + const array_typet &type); // we use this to build a bit-vector encoding of the FPA theory void convert_floatbv(const exprt &expr); @@ -235,6 +250,10 @@ class smt2_convt : public stack_decision_proceduret typedef std::map defined_expressionst; defined_expressionst defined_expressions; + /// The values which boolean identifiers have been `smt2_convt::set_to` or + /// in other words those which are asserted as true / false in the output + /// smt2 formula. + std::unordered_map set_values; defined_expressionst object_sizes; diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 5a2979707fb..7f66b5cd870 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -139,7 +139,7 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) boolean_assignment.resize(no_boolean_variables, false); typedef std::unordered_map valuest; - valuest values; + valuest parsed_values; while(in) { @@ -167,7 +167,7 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) // ( (|some_integer| 0) ) // ( (|some_integer| (- 10)) ) - values[s0.id()]=s1; + parsed_values[s0.id()] = s1; } else if( parsed.id().empty() && parsed.get_sub().size() == 2 && @@ -175,29 +175,61 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) { // We ignore errors after UNSAT because get-value after check-sat // returns unsat will give an error. - if(res!=resultt::D_UNSATISFIABLE) + if(res != resultt::D_UNSATISFIABLE) { - messaget log{message_handler}; - log.error() << "SMT2 solver returned error message:\n" - << "\t\"" << parsed.get_sub()[1].id() << "\"" - << messaget::eom; - return decision_proceduret::resultt::D_ERROR; + const auto &message = id2string(parsed.get_sub()[1].id()); + // Special case error handling + if( + solver == solvert::Z3 && + message.find("must not contain quantifiers") != std::string::npos) + { + // We tried to "(get-value |XXXX|)" where |XXXX| is determined to + // include a quantified expression + // Nothing to do, this should be caught and value assigned by the + // set_to defaults later. + } + // Unhandled error, log the error and report it back up to caller + else + { + messaget log{message_handler}; + log.error() << "SMT2 solver returned error message:\n" + << "\t\"" << message << "\"" << messaget::eom; + return decision_proceduret::resultt::D_ERROR; + } } } } + // If the result is not satisfiable don't bother updating the assignments and + // values (since we didn't get any), just return. + if(res != resultt::D_SATISFIABLE) + return res; + for(auto &assignment : identifier_map) { - std::string conv_id=convert_identifier(assignment.first); - const irept &value=values[conv_id]; - assignment.second.value=parse_rec(value, assignment.second.type); + std::string conv_id = convert_identifier(assignment.first); + const irept &value = parsed_values[conv_id]; + assignment.second.value = parse_rec(value, assignment.second.type); } // Booleans for(unsigned v=0; vsecond.id() == ID_true; + // Work out the value based on what set_to was called with. + const auto found_set_value = + set_values.find('|' + boolean_identifier + '|'); + if(found_set_value != set_values.end()) + return found_set_value->second; + // Old code used the computation + // const irept &value=values["B"+std::to_string(v)]; + // boolean_assignment[v]=(value.id()==ID_true); + return parsed_values[boolean_identifier].id() == ID_true; + }(); } return res;