Value set: handle with, array and struct expressions more accurately

We may have a suffix indicating that the result of a get_value_set_rec query
would effectively be projected down to particular struct member or array indices
on completion (and so we in fact do this eagerly at the bottom of the recursion,
rather than at the top as one might expect). However, the ID_array, ID_struct and
ID_with expressions are widening -- one or more of their operands is integrated
into a larger type -- so we should consume suffix entries introduced by ID_member
expressions if available.

Author: smowton

jbmc/regression/jbmc/string_field_aliasing/Cart$Category.class

@@ -0,0 +1,16 @@
+public class Cart {
+
+    class Product {
+        public String size;
+        public Category cat;
+    }
+
+    class Category {
+        public String name;
+    }
+
+    public boolean checkTax4(Product product, String s) {
+        product.size="abc";
+        return s.startsWith(product.cat.name);
+    }
+}

jbmc/regression/jbmc/string_field_aliasing/Cart$Product.class

@@ -0,0 +1,14 @@
+CORE
+Cart.class
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --trace --cover location --java-max-vla-length 96 --refine-strings --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 Cart.class --function Cart.checkTax4 --string-printable
+^EXIT=0$
+^SIGNAL=0$
+checkTax4:.*: SATISFIED
+--
+checkTax4:.*: FAILED
+dec_solve: current index set is empty, this should not happen
+^warning: ignoring
+--
+This checks that assigning to a field of an object (which generates a WITH expression in this case) doesn't result
+in conflating the String-typed and non-String-typed fields of the Cart class. When they are conflated we get
+warnings from the string solver and missing coverage.

jbmc/regression/jbmc/string_field_aliasing/Cart.class

@@ -344,6 +344,30 @@ void value_sett::get_value_set(
   get_value_set_rec(tmp, dest, "", tmp.type(), ns);
 }
 
+/// Check if 'suffix' starts with 'field'.
+/// Suffix is delimited by periods and '[]' (array access) tokens, so we're
+/// looking for ".field($|[]|.)"
+static bool suffix_starts_with_field(
+  const std::string &suffix, const std::string &field)
+{
+  return
+    !suffix.empty() &&
+    suffix[0] == '.' &&
+    suffix.compare(1, field.length(), field) == 0 &&
+    (suffix.length() == field.length() + 1 ||
+     suffix[field.length() + 1] == '.' ||
+     suffix[field.length() + 1] == '[');
+}
+
+static std::string strip_first_field_from_suffix(
+  const std::string &suffix, const std::string &field)
+{
+  INVARIANT(
+    suffix_starts_with_field(suffix, field),
+    "suffix should start with " + field);
+  return suffix.substr(field.length() + 1);
+}
+
 void value_sett::get_value_set_rec(
   const exprt &expr,
   object_mapt &dest,
@@ -711,72 +735,113 @@ void value_sett::get_value_set_rec(
   }
   else if(expr.id()==ID_struct)
   {
+    const auto &struct_components = to_struct_type(expr_type).components();
+    INVARIANT(
+      struct_components.size() == expr.operands().size(),
+      "struct expression should have an operand per component");
+    auto component_iter = struct_components.begin();
+    bool found_component = false;
+
     // a struct constructor, which may contain addresses
+
     forall_operands(it, expr)
-      get_value_set_rec(*it, dest, suffix, original_type, ns);
+    {
+      const std::string &component_name =
+        id2string(component_iter->get_name());
+      if(suffix_starts_with_field(suffix, component_name))
+      {
+        std::string remaining_suffix =
+          strip_first_field_from_suffix(suffix, component_name);
+        get_value_set_rec(*it, dest, remaining_suffix, original_type, ns);
+        found_component = true;
+      }
+      ++component_iter;
+    }
+
+    if(!found_component)
+    {
+      // Struct field doesn't appear as expected -- this has probably been
+      // cast from an incompatible type. Conservatively assume all fields may
+      // be of interest.
+      forall_operands(it, expr)
+        get_value_set_rec(*it, dest, suffix, original_type, ns);
+    }
   }
   else if(expr.id()==ID_with)
   {
-    assert(expr.operands().size()==3);
-
-    // this is the array/struct
-    object_mapt tmp_map0;
-    get_value_set_rec(expr.op0(), tmp_map0, suffix, original_type, ns);
+    const with_exprt &with_expr = to_with_expr(expr);
 
-    // this is the update value -- note NO SUFFIX
-    object_mapt tmp_map2;
-    get_value_set_rec(expr.op2(), tmp_map2, "", original_type, ns);
-
-    if(expr_type.id()==ID_struct)
+    // If the suffix is empty we're looking for the whole struct:
+    // default to combining both options as below.
+    if(expr_type.id() == ID_struct && !suffix.empty())
     {
-      #if 0
-      const object_map_dt &object_map0=tmp_map0.read();
-      irep_idt component_name=expr.op1().get(ID_component_name);
-
-      bool insert=true;
-
-      for(object_map_dt::const_iterator
-          it=object_map0.begin();
-          it!=object_map0.end();
-          it++)
+      irep_idt component_name = with_expr.where().get(ID_component_name);
+      if(suffix_starts_with_field(suffix, id2string(component_name)))
       {
-        const exprt &e=to_expr(it);
-
-        if(e.id()==ID_member &&
-           e.get(ID_component_name)==component_name)
-        {
-          if(insert)
-          {
-            dest.write().insert(tmp_map2.read().begin(), tmp_map2.read().end());
-            insert=false;
-          }
-        }
-        else
-          dest.write().insert(*it);
+        // Looking for the member overwritten by this WITH expression
+        std::string remaining_suffix =
+          strip_first_field_from_suffix(suffix, id2string(component_name));
+        get_value_set_rec(
+          with_expr.new_value(), dest, remaining_suffix, original_type, ns);
+      }
+      else if(to_struct_type(expr_type).has_component(component_name))
+      {
+        // Looking for a non-overwritten member, look through this expression
+        get_value_set_rec(with_expr.old(), dest, suffix, original_type, ns);
+      }
+      else
+      {
+        // Member we're looking for is not defined in this struct -- this
+        // must be a reinterpret cast of some sort. Default to conservatively
+        // assuming either operand might be involved.
+        get_value_set_rec(expr.op0(), dest, suffix, original_type, ns);
+        get_value_set_rec(expr.op2(), dest, "", original_type, ns);
       }
-      #else
-      // Should be more precise! We only want "suffix"
-      make_union(dest, tmp_map0);
-      make_union(dest, tmp_map2);
-      #endif
+    }
+    else if(expr_type.id() == ID_array && !suffix.empty())
+    {
+      std::string new_value_suffix;
+      if(has_prefix(suffix, "[]"))
+        new_value_suffix = suffix.substr(2);
+
+      // Otherwise use a blank suffix on the assumption anything involved with
+      // the new value might be interesting.
+
+      get_value_set_rec(with_expr.old(), dest, suffix, original_type, ns);
+      get_value_set_rec(
+        with_expr.new_value(), dest, new_value_suffix, original_type, ns);
     }
     else
     {
-      make_union(dest, tmp_map0);
-      make_union(dest, tmp_map2);
+      // Something else-- the suffixes used here are a rough guess at best,
+      // so this is imprecise.
+      get_value_set_rec(expr.op0(), dest, suffix, original_type, ns);
+      get_value_set_rec(expr.op2(), dest, "", original_type, ns);
     }
   }
   else if(expr.id()==ID_array)
   {
     // an array constructor, possibly containing addresses
+    std::string new_suffix = suffix;
+    if(has_prefix(suffix, "[]"))
+      new_suffix = suffix.substr(2);
+    // Otherwise we're probably reinterpreting some other type -- try persisting
+    // with the current suffix for want of a better idea.
+
     forall_operands(it, expr)
-      get_value_set_rec(*it, dest, suffix, original_type, ns);
+      get_value_set_rec(*it, dest, new_suffix, original_type, ns);
   }
   else if(expr.id()==ID_array_of)
   {
     // an array constructor, possibly containing an address
+    std::string new_suffix = suffix;
+    if(has_prefix(suffix, "[]"))
+      new_suffix = suffix.substr(2);
+    // Otherwise we're probably reinterpreting some other type -- try persisting
+    // with the current suffix for want of a better idea.
+
     assert(expr.operands().size()==1);
-    get_value_set_rec(expr.op0(), dest, suffix, original_type, ns);
+    get_value_set_rec(expr.op0(), dest, new_suffix, original_type, ns);
   }
   else if(expr.id()==ID_dynamic_object)
   {