CSVSA: retain state at top and bottom of functions

This prevents the fixpoint algorithm from ending up in a loop when working over recursive functions --
the top of a function is a control-flow merge point in this case, so it must obviously be retained to
determine when the loop should terminate, and the end-of-function state must be retained to prevent
a directly recursive function from infinitely analysing the path between a recursive call and its own end.

The final state must be set "seen" when it is analysed, as static_analysist does when visiting "normal"
states, for this check to take effect.

Author: smowton

src/pointer-analysis/context_sensitive_value_set_analysis.cpp

@@ -62,7 +62,9 @@ void csvsa_function_contextt::csvsa_visit(locationt l)
   {
     // Function returns are special-- if anything changed,
     // queue all of this context's callsites' successors:
-    const auto &end_state = (*this)[l];
+    auto &end_state = (*this)[l];
+    end_state.set_seen();
+
     std::unique_ptr<const domaint> end_state_without_locals;
     for(const auto &caller : callers)
     {

src/pointer-analysis/context_sensitive_value_set_analysis.h

@@ -381,8 +381,19 @@ class csvsa_function_contextt :
     callers.insert({caller, callsite});
   }
 
-  static bool is_virtual_callsite(locationt instruction)
+  static bool csvsa_must_retain_domain(locationt instruction)
   {
+    // Retain start of function, in case of a recursive edge:
+    if(instruction->incoming_edges.size() == 0)
+      return true;
+
+    // Retain the END_FUNCTION instruction, to provide a stopping point for
+    // the otherwise apparently infinite loop of a recursive function whose
+    // return values propagate to a callsite within its own body.
+    if(instruction->is_end_function())
+      return true;
+
+    // Retain virtual callsites, for the specialiser to consult later.
     return instruction->type == FUNCTION_CALL &&
            to_code_function_call(instruction->code).function().id() ==
              ID_virtual_function;
@@ -408,7 +419,7 @@ class csvsa_function_contextt :
     context_sensitive_value_set_analysis_drivert &driver,
     context_indext parent,
     const locationt &parent_loc)
-    : csvsa_value_set_analysist(ns, is_virtual_callsite),
+    : csvsa_value_set_analysist(ns, csvsa_must_retain_domain),
       get_goto_program(get_goto_program),
       function_name(function_name),
       goto_program(get_goto_program(function_name)),
@@ -431,7 +442,7 @@ class csvsa_function_contextt :
     get_goto_programt get_goto_program,
     const irep_idt &function_name,
     context_sensitive_value_set_analysis_drivert &driver)
-    : csvsa_value_set_analysist(ns, is_virtual_callsite),
+    : csvsa_value_set_analysist(ns, csvsa_must_retain_domain),
       get_goto_program(get_goto_program),
       function_name(function_name),
       goto_program(get_goto_program(function_name)),