Merge pull request diffblue#254 from diffblue/owen/sec-98/rename-modified-flag

SEC-98 Rename `modified` flag on EVSs

Author: owen-jones-diffblue

regression/LVSA/TestEVS/Test.class

@@ -25,7 +25,7 @@ public void write_new_class_to_static_field() {
     static_node.left = new Object();
   }
 
-  public void modified(Node parameter_node) {
+  public void is_initializer_flag(Node parameter_node) {
     parameter_node.left = new Object();
     parameter_node.right = new Object();
     static_object = parameter_node.left;

regression/LVSA/TestEVS/Test.java

@@ -41,18 +41,18 @@ def test_write_new_class_to_static_field(tmpdir):
     output_value_expectation.check_contains_dynamic_object()
 
 
-def test_modified(tmpdir):
-    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('modified')
+def test_is_initializer_flag(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('is_initializer_flag')
     lvsa_expectation = lvsa_driver.run()
 
     output_value_expectation_1 = lvsa_expectation.check_external_value_set('Node', '.left')
 
     output_value_expectation_1.check_number_of_values(2)
     output_value_expectation_1.check_contains_dynamic_object(is_most_recent_allocation=True)
-    output_value_expectation_1.check_contains_external_value_set(has_been_read=False)
+    output_value_expectation_1.check_contains_external_value_set(is_initializer=True)
 
     output_value_expectation_2 = lvsa_expectation.check_public_static('static_object')
 
     output_value_expectation_2.check_number_of_values(2)
     output_value_expectation_2.check_contains_dynamic_object(is_most_recent_allocation=True)
-    output_value_expectation_2.check_contains_external_value_set(has_been_read=True)
+    output_value_expectation_2.check_contains_external_value_set(is_initializer=False)

regression/LVSA/TestEVS/test_evs.py

@@ -35,7 +35,7 @@ def __init__(self, evs_expr):
         Expr.__init__(self, evs_expr)
         # Expect '0' or '1', corresponding to whether the field has ever been read (and hence values from the field
         # could have been written to the field)
-        self.has_been_read = evs_expr['namedSub']['modified']['id'] == '1'
+        self.is_initializer = evs_expr['namedSub']['is_initializer']['id'] == '1'
         # Expect the parameter name for parameters and 'external_objects' for other things, like static fields
         self.label = evs_expr['sub'][0]['namedSub']['value']['id']
         self.is_external_object = self.label == 'external_objects'
@@ -65,14 +65,14 @@ def check_contains_dynamic_object(self, expected_number=1, is_most_recent_alloca
             matches = [x for x in matches if x.is_most_recent_allocation == is_most_recent_allocation]
         assert expected_number == len(matches)
 
-    def check_contains_external_value_set(self, expected_number=1, is_external_object=None, has_been_read=None):
+    def check_contains_external_value_set(self, expected_number=1, is_external_object=None, is_initializer=None):
         matches = self.external_value_sets
         if is_external_object is not None:
             # Expect True or False
             matches = [x for x in matches if x.is_external_object == is_external_object]
-        if has_been_read is not None:
+        if is_initializer is not None:
             # Expect True or False
-            matches = [x for x in matches if x.has_been_read == has_been_read]
+            matches = [x for x in matches if x.is_initializer == is_initializer]
         assert expected_number == len(matches)
 
     def get_dynamic_object_ids(self):

regression/LVSA/lvsa_driver.py

@@ -21,8 +21,8 @@ std::string evs_pretty_printert::convert(const exprt &src)
       result << top_pretty_printer->convert(*it);
     }
     result << ")";
-    if(src.get_bool("modified"))
-      result << "<maybe-modified>";
+    if(src.get_bool("is_initializer"))
+      result << "<is-initializer>";
     result << " ["
            << top_pretty_printer->convert(src.type())
            << ']';

src/pointer-analysis/evs_pretty_printer.cpp

@@ -89,23 +89,30 @@ class external_value_set_exprt:public exprt
     const typet &type,
     const constant_exprt &_label,
     const local_value_set_analysis_modet mode,
-    bool modified):
+    bool is_initializer):
     exprt(ID_external_value_set, type)
   {
     operands().resize(1);
     operands()[0]=_label;
     set("#lva_mode", std::to_string(static_cast<int>(mode)));
-    set("modified", std::to_string(modified ? 1 : 0));
+    set("is_initializer", std::to_string(is_initializer ? 1 : 0));
   }
 
   local_value_set_analysis_modet analysis_mode() const
   {
     return (local_value_set_analysis_modet)get_int("#lva_mode");
   }
 
-  bool is_modified() const
+  /// At the beginning of a function, the value set for EVS("A.b") is
+  /// { EVS("A.b", is_initializer=true) }. Whenever EVS("A.b") gets put into a
+  /// value set the is_initializer flag is set to false. This includes when
+  /// it is put into the value set for EVS("A.b"), for example because of the
+  /// line `a1.b = a2.b`. This allows us to distinguish the case that nothing
+  /// was written to any A.b and the case that a value was written to an A.b
+  /// from a different A.b.
+  bool is_initializer() const
   {
-    return get_bool("modified");
+    return get_bool("is_initializer");
   }
 
   constant_exprt &label() { return to_constant_expr(op0()); }
@@ -214,14 +221,14 @@ class external_value_set_exprt:public exprt
     }
   }
 
-  external_value_set_exprt as_modified() const
+  external_value_set_exprt as_non_initializer() const
   {
-    if(is_modified())
+    if(!is_initializer())
       return *this;
     else
     {
       external_value_set_exprt copy=*this;
-      copy.set("modified", ID_1);
+      copy.set("is_initializer", ID_0);
       return copy;
     }
   }

src/pointer-analysis/external_value_set_expr.h

@@ -329,8 +329,8 @@ void local_value_sett::assign(
     object_mapt values_rhs;
     get_value_set(rhs, values_rhs, ns, is_simplified);
 
-    // Special case: if an ext-val-set with modified=false is written,
-    // set modified=true before inserting, to represent the fact that
+    // Special case: if an ext-val-set with is_initializer=true is written,
+    // set is_initializer=false before inserting, to represent the fact that
     // <some external>.x = <some external>.x might have a side-effect if
     // the two externals differ, and generally differentiates an
     // initialiser from an external set that has been read from somewhere
@@ -343,7 +343,7 @@ void local_value_sett::assign(
       if(objexpr.id()==ID_external_value_set)
       {
         external_value_set_exprt mod(
-          to_external_value_set(objexpr).as_modified());
+          to_external_value_set(objexpr).as_non_initializer());
         replacements.push_back({obj.first, mod});
       }
     }

src/pointer-analysis/local_value_set.cpp

@@ -84,7 +84,7 @@ void local_value_set_analysist::initialize(const goto_programt &fun)
         extsym.type().subtype(),
         constant_exprt(extsym_name, string_typet()),
         mode,
-        false);
+        true);
       initial_state.insert(extsym_entry.object_map, extsym_var);
     }
   }
@@ -150,7 +150,7 @@ void local_value_set_analysist::transform_function_stub_single_external_set(
       auto &evse=to_external_value_set(assignment.second);
       // Differentiate external-set entries that only contain
       // their initialiser from ones that have been written:
-      if(evse.is_modified())
+      if(!evse.is_initializer())
       {
         lhs_written.insert({
           assignment.first.base_name,
@@ -163,7 +163,7 @@ void local_value_set_analysist::transform_function_stub_single_external_set(
         std::vector<local_value_sett::entryt*> rhs_entries;
         const auto &evse=to_external_value_set(assignment.second);
         const auto &apback=evse.access_path_back();
-        if(evse.is_modified())
+        if(!evse.is_initializer())
         {
           get_all_field_value_sets(
             id2string(apback.label()),