Merge pull request diffblue#323 from diffblue/owen-jones-diffblue/precise-evs-loop

SEC-198: Do no export precise EVSs when a loop makes them wrong

Author: owen-jones-diffblue

src/pointer-analysis/local_value_set.cpp

@@ -301,8 +301,9 @@ void local_value_sett::get_value_set_rec(
         bool loop_found=new_ext_set.extend_access_path(
           new_entry, external_value_set_typet::PRECISE);
 
-        // TODO: handle loops properly
-        if(!loop_found)
+        if(loop_found)
+          precise_evs_curtailed_because_of_loop = true;
+        else
         {
           new_ext_set.type()=field_type.subtype();
 
@@ -605,8 +606,9 @@ void local_value_sett::assign_rec(
       bool loop_found=new_ext_set.extend_access_path(
         new_entry, external_value_set_typet::PRECISE);
 
-      // TODO: handle loops properly
-      if(!loop_found)
+      if(loop_found)
+        precise_evs_curtailed_because_of_loop = true;
+      else
       {
         const std::string basename=
           new_ext_set.get_access_path_basename(declared_on_type);
@@ -668,4 +670,6 @@ void local_value_sett::make_union_bookkeeping_data_structures(
     other.num_reads_of_field_of_external_object;
   num_writes_to_field_of_external_object+=
     other.num_writes_to_field_of_external_object;
+  precise_evs_curtailed_because_of_loop &=
+    other.precise_evs_curtailed_because_of_loop;
 }

src/pointer-analysis/local_value_set.h

@@ -20,7 +20,7 @@ class local_value_sett:public value_sett
 
   mutable unsigned int num_reads_of_field_of_external_object=0;
   mutable unsigned int num_writes_to_field_of_external_object=0;
-  mutable bool no_merges=true;
+  mutable bool precise_evs_curtailed_because_of_loop=false;
 
   /// Determines whether we should export precise or per_field external value
   /// sets in function summaries.
@@ -30,8 +30,10 @@ class local_value_sett:public value_sett
 #ifdef DO_NOT_USE_PRECISE_EXTERNAL_VALUE_SETS
     return false;
 #else
-    return no_merges && (num_reads_of_field_of_external_object
-      +num_writes_to_field_of_external_object<=1);
+    return !precise_evs_curtailed_because_of_loop &&
+           (num_reads_of_field_of_external_object +
+              num_writes_to_field_of_external_object <=
+            1);
 #endif
   }