Merge pull request #6004 from padhi-aws-forks/use_array_of_bool_fix

[smt_convt] Fix usage of `use_array_of_bool`

Author: SaswatPadhi

regression/cbmc/array_of_bool_as_bitvec/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+__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]);
+}

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

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'],

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
       }