Merge pull request #8942 from tautschnig/let-bound-arrays

Connect let-bound arrays to originals in array theory

Author: tautschnig

regression/smt2_solver/let-array/let-array.desc

@@ -0,0 +1,11 @@
+CORE
+let-array.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+^sat$
+--
+Let-bound arrays must be connected to the original array in the
+array theory so that element-wise constraints propagate correctly.

regression/smt2_solver/let-array/let-array.smt2

@@ -0,0 +1,11 @@
+; Test that let-bound arrays are properly connected to the original
+; array in the array theory. A let binding creates a fresh symbol
+; internally; without proper connection, the element-wise constraints
+; on the original array don't propagate to the let-bound copy.
+(set-option :produce-models true)
+(declare-fun arr () (Array (_ BitVec 32) (_ BitVec 32)))
+(assert (= (select arr (_ bv0 32)) (_ bv42 32)))
+(assert (= (select arr (_ bv1 32)) (_ bv99 32)))
+(assert (not (= (let ((?a arr)) (select ?a (_ bv1 32))) (_ bv99 32))))
+(check-sat)
+(exit)

src/solvers/flattening/arrays.cpp

@@ -80,6 +80,19 @@ literalt arrayst::record_array_equality(
   return array_equalities.back().l;
 }
 
+void arrayst::record_array_let_binding(
+  const symbol_exprt &symbol,
+  const exprt &value)
+{
+  DATA_INVARIANT(
+    symbol.type().id() == ID_array,
+    "record_array_let_binding parameter should be array-typed");
+
+  const equal_exprt eq{symbol, value};
+  const literalt eq_lit = record_array_equality(eq);
+  prop.l_set_to_true(eq_lit);
+}
+
 void arrayst::collect_indices()
 {
   for(std::size_t i=0; i<arrays.size(); i++)

src/solvers/flattening/arrays.h

@@ -26,6 +26,7 @@ class array_of_exprt;
 class equal_exprt;
 class if_exprt;
 class index_exprt;
+class symbol_exprt;
 class with_exprt;
 class update_exprt;
 
@@ -52,6 +53,12 @@ class arrayst:public equalityt
   literalt record_array_equality(const equal_exprt &expr);
   void record_array_index(const index_exprt &expr);
 
+  /// Record that \p symbol is equal to \p value for the purposes of the
+  /// array theory. For unbounded-array-typed bindings this connects the
+  /// two expressions in the union-find so that element-wise constraints
+  /// propagate correctly.
+  void record_array_let_binding(const symbol_exprt &symbol, const exprt &value);
+
 protected:
   const namespacet &ns;
   messaget log;

src/solvers/flattening/boolbv_let.cpp

@@ -6,12 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include "boolbv.h"
-
+#include <util/byte_operators.h>
 #include <util/range.h>
 #include <util/replace_symbol.h>
 #include <util/std_expr.h>
 
+#include "boolbv.h"
+
 bvt boolbvt::convert_let(const let_exprt &expr)
 {
   const auto &variables = expr.variables();
@@ -69,6 +70,20 @@ bvt boolbvt::convert_let(const let_exprt &expr)
   for(const auto &pair : make_range(variables).zip(fresh_variables))
     replace_symbol.insert(pair.first, pair.second);
 
+  // Connect fresh let-bound symbols to their values in the array theory.
+  for(const auto &pair : make_range(fresh_variables).zip(values))
+  {
+    if(
+      pair.first.type().id() == ID_array &&
+      is_unbounded_array(to_array_type(pair.first.type())))
+    {
+      const exprt lowered_value = has_byte_operator(pair.second)
+                                    ? lower_byte_operators(pair.second, ns)
+                                    : pair.second;
+      record_array_let_binding(pair.first, pair.second);
+    }
+  }
+
   // rename the bound symbols in 'where'
   exprt where_renamed = expr.where();
   replace_symbol(where_renamed);