diff --git a/regression/cbmc/array_of_bool_as_bitvec/main.c b/regression/cbmc/array_of_bool_as_bitvec/main.c new file mode 100644 index 00000000000..19888bb1a45 --- /dev/null +++ b/regression/cbmc/array_of_bool_as_bitvec/main.c @@ -0,0 +1,19 @@ +#include +#include +#include + +__CPROVER_bool w[8]; + +void main() +{ + _Bool x[8] = {false}; + __CPROVER_bool y[8] = {false}; + bool *z = calloc(8, sizeof(bool)); + + unsigned idx; + __CPROVER_assume(0 <= idx && idx < 8); + + assert(w[idx] == x[idx]); + assert(x[idx] == y[idx]); + assert(y[idx] == z[idx]); +} diff --git a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc new file mode 100644 index 00000000000..ae228a04e44 --- /dev/null +++ b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc @@ -0,0 +1,31 @@ +CORE broken-smt-backend +main.c +--smt2 --outfile - +\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\) +\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\) +\(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\) +^EXIT=0$ +^SIGNAL=0$ +-- +\(= \(select array_of\.2 i\) false\) +\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\) +\(= \(select array\.3 \(_ bv\d+ 64\)\) false\) +-- +This test checks for correctness of BitVec-array encoding of Boolean arrays. + +Ideally, we shouldn't have to check the SMT output, but should run with backend +SMT solvers. However, we currently cannot because of #5977 (also see #6005). + +For now, we tag this test as `broken-smt-backend` to avoid running main.c +with `--z3` or `--cprover-smt2`, both of which encode Boolean arrays directly. +Instead, we generate a generic SMT encoding with `--smt2` and check the output. + +Explanation of regexes: +line 4,10: array.2 elements should be BitVec not Bool +line 5,11: equality operator (=) should have 2 arguments not 3 +line 6,12: array.3 elements should be BitVec not Bool + +Once #5977 and #6005 are resolved, we should: +- remove `broken-smt-backend` tag +- run with `--smt2 --cprover-smt2` and `--smt2 --z3` +- check for successful verification diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index dde6bb833bc..0b153f61854 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -12,6 +12,8 @@ # some tests in the cbmc suite don't work for the trace checks for one reason or another ExcludedTests = list(map(lambda s: os.path.join(test_base_dir, s[0], s[1]), [ + # these tests dump the raw SMT2 output (using --outfile) + ['array_of_bool_as_bitvec', 'test-smt2-outfile.desc'], # these tests expect input from stdin ['json-interface1', 'test_wrong_option.desc'], ['json-interface1', 'test.desc'], diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index f864f95054e..0d2b5af1f32 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -3871,7 +3871,7 @@ void smt2_convt::convert_index(const index_exprt &expr) out << " "; convert_expr(typecast_exprt(expr.index(), array_type.size().type())); out << ")"; - out << " #b1 #b0)"; + out << " #b1)"; } else { @@ -4405,19 +4405,29 @@ void smt2_convt::find_symbols(const exprt &expr) if(defined_expressions.find(expr) == defined_expressions.end()) { const auto &array_of = to_array_of_expr(expr); + const auto &array_type = array_of.type(); const irep_idt id = "array_of." + std::to_string(defined_expressions.size()); out << "; the following is a substitute for lambda i. x\n"; out << "(declare-fun " << id << " () "; - convert_type(array_of.type()); + convert_type(array_type); out << ")\n"; // use a quantifier-based initialization instead of lambda out << "(assert (forall ((i "; - convert_type(array_of.type().size().type()); + convert_type(array_type.size().type()); out << ")) (= (select " << id << " i) "; - convert_expr(array_of.what()); + if(array_type.subtype().id() == ID_bool && !use_array_of_bool) + { + out << "(ite "; + convert_expr(array_of.what()); + out << " #b1 #b0)"; + } + else + { + convert_expr(array_of.what()); + } out << ")))\n"; defined_expressions[expr] = id; @@ -4431,12 +4441,13 @@ void smt2_convt::find_symbols(const exprt &expr) if(defined_expressions.find(expr) == defined_expressions.end()) { const auto &array_comprehension = to_array_comprehension_expr(expr); - const auto &array_size = array_comprehension.type().size(); + const auto &array_type = array_comprehension.type(); + const auto &array_size = array_type.size(); const irep_idt id = "array_comprehension." + std::to_string(defined_expressions.size()); out << "(declare-fun " << id << " () "; - convert_type(array_comprehension.type()); + convert_type(array_type); out << ")\n"; out << "; the following is a substitute for lambda i . x(i)\n"; @@ -4455,7 +4466,16 @@ void smt2_convt::find_symbols(const exprt &expr) out << ")) (= (select " << id << " "; convert_expr(array_comprehension.arg()); out << ") "; - convert_expr(array_comprehension.body()); + if(array_type.subtype().id() == ID_bool && !use_array_of_bool) + { + out << "(ite "; + convert_expr(array_comprehension.body()); + out << " #b1 #b0)"; + } + else + { + convert_expr(array_comprehension.body()); + } out << "))))\n"; defined_expressions[expr] = id; @@ -4479,7 +4499,16 @@ void smt2_convt::find_symbols(const exprt &expr) out << "(assert (= (select " << id << " "; convert_expr(from_integer(i, array_type.size().type())); out << ") "; // select - convert_expr(expr.operands()[i]); + if(array_type.subtype().id() == ID_bool && !use_array_of_bool) + { + out << "(ite "; + convert_expr(expr.operands()[i]); + out << " #b1 #b0)"; + } + else + { + convert_expr(expr.operands()[i]); + } out << "))" << "\n"; // =, assert }