Add arrayst::get to return RHS of unbounded arrays

In order to generate a trace value for an unbounded LHS we may need to
look at its RHS as (string) refinement may have constructed values for
the RHS.

Author: tautschnig

jbmc/regression/jbmc-strings/nondet_propagation/Test.class

@@ -0,0 +1,8 @@
+public class Test {
+  public String foo() {
+    final int i = 10;
+    final String retval = Integer.toHexString(i);
+    assert(false);
+    return retval;
+  }
+}

jbmc/regression/jbmc-strings/nondet_propagation/Test.java

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.foo --trace
+^EXIT=10$
+^SIGNAL=0$
+dynamic_object1=\{ 'a' \}
+--
+--
+Nondet propagation would previously cause an output like
+dynamic_object1=dynamic_object1#2, because the mapping between dynamic_object1#2
+and a nondet-symbol, which was otherwise being used by the string solver, was
+not established.

jbmc/regression/jbmc-strings/nondet_propagation/test.desc

@@ -68,9 +68,20 @@ literalt arrayst::record_array_equality(
   collect_arrays(op0);
   collect_arrays(op1);
 
+  lhs_rhs_map.emplace(op0, op1);
+
   return array_equalities.back().l;
 }
 
+exprt arrayst::get(const exprt &expr) const
+{
+  auto it = lhs_rhs_map.find(expr);
+  if(it != lhs_rhs_map.end() && it->first != it->second)
+    return get(it->second);
+  else
+    return SUB::get(expr);
+}
+
 void arrayst::collect_indices()
 {
   for(std::size_t i=0; i<arrays.size(); i++)

src/solvers/flattening/arrays.cpp

@@ -43,6 +43,8 @@ class arrayst:public equalityt
   literalt record_array_equality(const equal_exprt &expr);
   void record_array_index(const index_exprt &expr);
 
+  exprt get(const exprt &expr) const override;
+
 protected:
   const namespacet &ns;
 
@@ -62,6 +64,7 @@ class arrayst:public equalityt
   // elements are added while references are held
   typedef std::list<array_equalityt> array_equalitiest;
   array_equalitiest array_equalities;
+  std::unordered_map<exprt, exprt, irep_hash> lhs_rhs_map;
 
   // this is used to find the clusters of arrays being compared
   union_find<exprt> arrays;

src/solvers/flattening/arrays.h

@@ -964,6 +964,8 @@ static optionalt<exprt> get_array(
   const auto eom = messaget::eom;
   const exprt &size = arr.length();
   exprt arr_val = simplify_expr(adjust_if_recursive(super_get(arr), ns), ns);
+  if(arr_val.id() == ID_array)
+    return std::move(arr_val);
   exprt size_val = super_get(size);
   size_val = simplify_expr(size_val, ns);
   const typet char_type = arr.type().subtype();