Merge pull request diffblue#420 from diffblue/owen-jones-diffblue/lvsa-only-track-pointers

LVSA: don't bother tracking non-pointer-typed fields

Author: owen-jones-diffblue

cbmc/src/pointer-analysis/value_set.cpp

@@ -1283,6 +1283,9 @@ void value_sett::assign(
   }
   else
   {
+    if(!should_track_value(lhs))
+      return;
+
     // basic type
     object_mapt values_rhs;
     get_value_set(rhs, values_rhs, ns, is_simplified);

cbmc/src/pointer-analysis/value_set.h

@@ -565,6 +565,13 @@ class value_sett
     const codet &code,
     const namespacet &ns);
 
+  /// Subclass customisation point for limiting which fields are considered
+  /// interesting:
+  virtual bool should_track_value(const exprt &e) const
+  {
+    return true;
+  }
+
  private:
   /// Subclass customisation point to filter or otherwise alter the value-set
   /// returned from get_value_set before it is passed into assign. For example,

regression/LVSA/TestBasic/Test$A.class

@@ -2,6 +2,7 @@
 
 public class Test {
   static A output;
+  static int output_int;
 
   public class A {
     public Object instanceObj;
@@ -25,4 +26,8 @@ public void outputs_dynamic_object_with_allocated_field() {
     output = new A();
     output.instanceObj = new Object();
   }
+
+  public void only_track_pointers() {
+    output_int = 42;
+  }
 }

regression/LVSA/TestBasic/Test.class

@@ -39,3 +39,13 @@ def test_outputs_dynamic_object_with_allocated_field(tmpdir):
 
     value_set_expectation.check_number_of_values(1)
     value_set_expectation.check_contains_dynamic_object()
+
+
+def test_only_track_pointers(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('only_track_pointers')
+    lvsa_expectation = lvsa_driver.run()
+
+    fq_class = lvsa_expectation.fq_class_with_java_prefix
+    fq_variable_name = fq_class + '.output_int'
+    matches = [var_state for var_state in lvsa_expectation.state if var_state['id'] == fq_variable_name]
+    assert(not matches)

regression/LVSA/TestBasic/Test.java

@@ -147,6 +147,12 @@ class local_value_sett : public value_sett
   /// \param loc_number: the location number for the dynamic objects we are
   ///   looking for
   void demote_most_recent_dynamic_objects(const unsigned loc_number);
+
+  /// Suppress tracking any non-pointer-typed values
+  bool should_track_value(const exprt &e) const override
+  {
+    return e.type().id() == ID_pointer;
+  }
 };
 
 /// Soft cast (i.e. using field accesses rather than a typecast) `expr` to its