Merge pull request #2625 from smowton/smowton/feature/value-set-accuracy

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

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,13 @@
+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:.*bytecode-index 8.*: FAILED
+dec_solve: current index set is empty, this should not happen
+--
+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)
   {