Merge pull request diffblue#388 from diffblue/owen-jones-diffblue/bugfix/add-precise-evs-initializers

SEC-366: LVSA: fix bug in add_precise_evs_initializers()

Author: owen-jones-diffblue

cbmc/src/analyses/static_analysis.cpp

@@ -221,6 +221,28 @@ bool static_analysis_baset::fixedpoint(
   return new_data;
 }
 
+bool static_analysis_baset::fixedpoint(
+  const goto_programt &goto_program,
+  const goto_functionst &goto_functions,
+  working_sett &working_set)
+{
+  if(goto_program.instructions.empty())
+    return false;
+
+  bool new_data = false;
+
+  while(!working_set.empty())
+  {
+    ++nsteps;
+    locationt l = get_next(working_set);
+
+    if(visit(l, working_set, goto_program, goto_functions))
+      new_data = true;
+  }
+
+  return new_data;
+}
+
 bool static_analysis_baset::visit(
   locationt l,
   working_sett &working_set,
@@ -243,21 +265,7 @@ bool static_analysis_baset::visit(
 
     statet &new_values=*tmp_state;
 
-    if(l->is_function_call())
-    {
-      // this is a big special case
-      const code_function_callt &code=
-        to_code_function_call(l->code);
-
-      do_function_call_rec(
-        l, to_l,
-        code.function(),
-        code.arguments(),
-        new_values,
-        goto_functions);
-    }
-    else
-      new_values.transform(ns, l, to_l);
+    transform_or_apply_function_call(l, to_l, goto_functions, new_values);
 
     statet &other=get_state(to_l);
 
@@ -547,3 +555,21 @@ void static_analysis_baset::concurrent_fixedpoint(
     }
   }
 }
+
+void static_analysis_baset::transform_or_apply_function_call(
+  locationt l,
+  locationt to_l,
+  const goto_functionst &goto_functions,
+  statet &new_values)
+{
+  if(l->is_function_call())
+  {
+    // this is a big special case
+    const code_function_callt &code = to_code_function_call(l->code);
+
+    do_function_call_rec(
+      l, to_l, code.function(), code.arguments(), new_values, goto_functions);
+  }
+  else
+    new_values.transform(ns, l, to_l);
+}

cbmc/src/analyses/static_analysis.h

@@ -217,6 +217,10 @@ class static_analysis_baset
   bool fixedpoint(
     const goto_programt &goto_program,
     const goto_functionst &goto_functions);
+  bool fixedpoint(
+    const goto_programt &goto_program,
+    const goto_functionst &goto_functions,
+    working_sett &working_set);
 
   virtual void fixedpoint(
     const goto_functionst &goto_functions)=0;
@@ -226,6 +230,12 @@ class static_analysis_baset
   void concurrent_fixedpoint(
     const goto_functionst &goto_functions);
 
+  void transform_or_apply_function_call(
+    locationt l,
+    locationt to_l,
+    const goto_functionst &goto_functions,
+    statet &new_values);
+
   // true = found something new
   bool visit(
     locationt l,

regression/LVSA/TestPreciseAccessPaths/test_precise_access_paths.py

@@ -73,7 +73,6 @@ def test_apply_set_field_of_external_object(tmpdir):
                                                      is_initializer=True)
 
 
-@pytest.mark.xfail(strict=True)  # SEC-202
 def test_conditionally_set_field_of_external_object(tmpdir):
     lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('conditionally_set_field_of_external_object')
     lvsa_expectation = lvsa_driver.run()
@@ -94,7 +93,12 @@ def test_apply_conditionally_set_field_of_external_object(tmpdir):
     value_set_expectation = lvsa_expectation.get_value_set_for_precise_evs(
         parameter_name='parameter_a', suffix='.object')
 
-    value_set_expectation.check_number_of_values(2)
+    value_set_expectation.check_number_of_values(4)
+    # Two values that existed before the function call
+    value_set_expectation.check_contains_per_field_evs(access_path=['.object'])
+    value_set_expectation.check_contains_precise_evs(label_suffix='parameter_a', access_path=['.object'],
+                                                     is_initializer=False)
+    # Two values that came from the function call
     value_set_expectation.check_contains_root_object_evs(label_suffix='parameter_object')
     value_set_expectation.check_contains_precise_evs(label_suffix='parameter_a', access_path=['.object'],
                                                      is_initializer=True)

src/pointer-analysis/local_value_set.cpp

@@ -717,6 +717,7 @@ void local_value_sett::assign_rec(
 
       external_value_set_exprt new_ext_set = evsi;
       new_ext_set.set_per_field_access_path(new_entry);
+      new_ext_set.type() = field_type.subtype();
 
       const std::string basename =
         new_ext_set.get_access_path_basename(declared_on_type);
@@ -730,10 +731,7 @@ void local_value_sett::assign_rec(
       auto &lhs_entry = insert_result.first->second;
 
       if(insert_result.second && field_type.id() == ID_pointer)
-      {
-        new_ext_set.type() = field_type.subtype();
         insert(lhs_entry.object_map, new_ext_set.as_initializer());
-      }
 
       make_union(lhs_entry.object_map, values_rhs);
     }
@@ -747,6 +745,7 @@ void local_value_sett::assign_rec(
         declared_on_type);
       external_value_set_exprt new_ext_set = evsi;
       bool loop_found = new_ext_set.extend_precise_access_path(new_entry);
+      new_ext_set.type() = field_type.subtype();
 
       if(loop_found)
         precise_evs_curtailed_because_of_loop = true;

src/pointer-analysis/local_value_set_analysis.cpp

@@ -17,6 +17,7 @@
 #include <algorithm>
 
 #include <pointer-analysis/dynamic_object_name.h>
+#include <analyses/static_analysis.h>
 #include <util/infix.h>
 #include <java_bytecode/java_types.h>
 
@@ -604,28 +605,31 @@ void local_value_set_analysist::operator()(const goto_programt &goto_program)
   /// This is a dummy variable that will always be empty because we handle
   /// function calls specially
   goto_functionst goto_functions;
+  working_sett working_set;
+  put_in_working_set(working_set, goto_program.instructions.begin());
 
   while(true)
   {
-    bool fixedpoint_changed_valuesets =
-      static_analysis_baset::fixedpoint(goto_program, goto_functions);
+    bool fixedpoint_changed_valuesets = static_analysis_baset::fixedpoint(
+      goto_program, goto_functions, working_set);
 
     if(!fixedpoint_changed_valuesets)
       break;
 
-    bool initializer_precise_evs_added =
-      add_precise_evs_initializers(goto_program);
+    working_set = add_precise_evs_initializers(goto_program, goto_functions);
 
-    if(!initializer_precise_evs_added)
+    if(working_set.empty())
       break;
   }
 }
 
-bool local_value_set_analysist::add_precise_evs_initializers(
-  const goto_programt &goto_program)
+static_analysis_baset::working_sett
+local_value_set_analysist::add_precise_evs_initializers(
+  const goto_programt &goto_program,
+  const goto_functionst &goto_functions)
 {
   const std::string precise_evs_prefix = PRECISE_EVS_PREFIX;
-  bool any_changes = false;
+  static_analysis_baset::working_sett working_set;
 
   for(locationt loc = goto_program.instructions.begin();
       loc != goto_program.instructions.end();
@@ -642,7 +646,14 @@ bool local_value_set_analysist::add_precise_evs_initializers(
     for(goto_programt::instructionst::const_iterator predecessor :
         loc->incoming_edges)
     {
-      for(const auto &value : (*this)[predecessor].value_set.values)
+      std::unique_ptr<local_value_set_domaint> tmp_state =
+        util_make_unique<local_value_set_domaint>((*this)[predecessor]);
+      local_value_set_domaint &incoming_state = *tmp_state;
+
+      transform_or_apply_function_call(
+        predecessor, loc, goto_functions, incoming_state);
+
+      for(const auto &value : incoming_state.value_set.values)
       {
         const exprt &lhs = value.second.structured_lhs;
 
@@ -673,11 +684,11 @@ bool local_value_set_analysist::add_precise_evs_initializers(
         bool object_map_changed = value_set.insert(entry.object_map, init_evs);
 
         if(object_map_changed)
-          any_changes = true;
+          put_in_working_set(working_set, loc);
       }
     }
   }
-  return any_changes;
+  return working_set;
 }
 
 void local_value_set_analysist::generate_state(locationt l)

src/pointer-analysis/local_value_set_analysis.h

@@ -242,7 +242,9 @@ class local_value_set_analysist
   /// for precise external value sets to their value-sets if needed.
   /// \param goto_program: the program under analysis
   /// \return true if any value-sets were changed
-  bool add_precise_evs_initializers(const goto_programt &goto_program);
+  static_analysis_baset::working_sett add_precise_evs_initializers(
+    const goto_programt &goto_program,
+    const goto_functionst &goto_functions);
   virtual void generate_state(locationt l) override;
 };