Merge pull request diffblue#531 from diffblue/smowton/feature/csvsa-constant-propagator-selective-domains

CSVSA constant propagator: use a sparse domain

Author: smowton

cbmc/src/analyses/constant_propagator.h

@@ -175,23 +175,29 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
 
   explicit constant_propagator_ait(
     const goto_functionst &goto_functions,
-    should_track_valuet should_track_value = track_all_values):
+    should_track_valuet should_track_value = track_all_values,
+    std::function<bool(locationt)> retain_domain_predicate = nullptr):
+    ait<constant_propagator_domaint>(retain_domain_predicate),
     dirty(goto_functions),
     should_track_value(should_track_value)
   {
   }
 
   explicit constant_propagator_ait(
     const goto_functiont &goto_function,
-    should_track_valuet should_track_value = track_all_values):
+    should_track_valuet should_track_value = track_all_values,
+    std::function<bool(locationt)> retain_domain_predicate = nullptr):
+    ait<constant_propagator_domaint>(retain_domain_predicate),
     dirty(goto_function),
     should_track_value(should_track_value)
   {
   }
 
   constant_propagator_ait(
     goto_modelt &goto_model,
-    should_track_valuet should_track_value = track_all_values):
+    should_track_valuet should_track_value = track_all_values,
+    std::function<bool(locationt)> retain_domain_predicate = nullptr):
+    ait<constant_propagator_domaint>(retain_domain_predicate),
     dirty(goto_model.goto_functions),
     should_track_value(should_track_value)
   {
@@ -203,7 +209,9 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
   constant_propagator_ait(
     goto_functionst::goto_functiont &goto_function,
     const namespacet &ns,
-    should_track_valuet should_track_value = track_all_values):
+    should_track_valuet should_track_value = track_all_values,
+    std::function<bool(locationt)> retain_domain_predicate = nullptr):
+    ait<constant_propagator_domaint>(retain_domain_predicate),
     dirty(goto_function),
     should_track_value(should_track_value)
   {

src/pointer-analysis/context_sensitive_value_set_analysis.cpp

@@ -118,7 +118,17 @@ void csvsa_function_contextt::csvsa_visit(locationt l)
     return;
   }
 
-  // Constant propagator: visit this instruction
+  // Pointer analysis: visit this instruction
+  working_sett value_set_successors;
+  visit(l, value_set_successors, goto_function.body, empty_goto_functions);
+
+  for(auto &successor : value_set_successors)
+    driver.queue_instruction(context_number, successor.second);
+
+  // Constant propagator: visit this instruction. Note this must come *after*
+  // pointer analysis because pointer analysis consults the constant propagator
+  // state, and the constant propagator's visit routine may clear this
+  // instruction's domain to save memory.
   csvsa_constant_propagatort::working_sett constant_prop_successors;
   constant_propagator.visit(
     l, constant_prop_successors, goto_function.body, empty_goto_functions, ns);
@@ -131,13 +141,6 @@ void csvsa_function_contextt::csvsa_visit(locationt l)
     if(!constant_propagator[successor.second].is_bottom())
       driver.queue_instruction(context_number, successor.second);
   }
-
-  // Pointer analysis: visit this instruction
-  working_sett value_set_successors;
-  visit(l, value_set_successors, goto_function.body, empty_goto_functions);
-
-  for(auto &successor : value_set_successors)
-    driver.queue_instruction(context_number, successor.second);
 }
 
 void csvsa_function_contextt::merge_call_return_state(

src/pointer-analysis/context_sensitive_value_set_analysis.h

@@ -227,8 +227,13 @@ class csvsa_constant_propagatort : public constant_propagator_ait
   }
 
   explicit csvsa_constant_propagatort(
-    const goto_functiont &goto_function, bool is_root_context) :
-    baset(goto_function, constant_propagator_should_track_value)
+    const goto_functiont &goto_function,
+    bool is_root_context,
+    std::function<bool(locationt)> must_retain_state_predicate) :
+    baset(
+      goto_function,
+      constant_propagator_should_track_value,
+      must_retain_state_predicate)
   {
     initialize(goto_function);
     if(is_root_context)
@@ -498,7 +503,8 @@ class csvsa_function_contextt :
       recursive_status(NOT_RECURSIVE),
       driver(driver),
       parent(parent),
-      constant_propagator(goto_function, false)
+      constant_propagator(
+        goto_function, false, get_retain_domain_predicate(driver))
   {
     callers.insert({parent, parent_loc});
   }
@@ -522,7 +528,8 @@ class csvsa_function_contextt :
       recursive_status(NOT_RECURSIVE),
       driver(driver),
       parent(),
-      constant_propagator(goto_function, true)
+      constant_propagator(
+        goto_function, true, get_retain_domain_predicate(driver))
   {
   }