Added LVSA method for singularity check

Added LVSA method for singularity check
that overrides the one from VSA, considers
the recency of dynamic-objects.

Replaced the old free function with calls to
the above described LVSA method.

The singularity check is now done at the set of expressions
level.

Dropped the taint_algorithm_computing_summary_of_functiont::compute_aliased_numbers_of_lvalue()
method.

Author: mariusmc92

cbmc

@@ -341,6 +341,39 @@ static void get_reachable_objects(
   }
 }
 
+/*******************************************************************\
+
+Function: local_value_set_analysist::is_singular
+
+  Inputs: The set of expressions to check.
+
+ Outputs: true, if the set contains only one element and 
+                that element is either a most-recent-allocation 
+                dynamic-object or a symbol (treated in the call 
+                to the base class). 
+          false, otherwise.
+
+ Purpose: Get whether a set of expressions can have a strong update
+          or not.
+
+\*******************************************************************/
+
+bool local_value_set_analysist::is_singular(const std::set<exprt> &values)
+{
+  if(values.size()!=1)
+    return false;
+
+  const exprt &object=*values.begin();
+  if(object.id()==ID_dynamic_object)
+  {
+    return to_dynamic_object_expr(object).get_recency()==
+      dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION;
+  }
+
+  // Otherwise fall back to base:
+  return baset::is_singular(values);
+}
+
 static void escape_analysis(
   const std::vector<local_value_sett::valuest::const_iterator>& values,
   std::set<unsigned long>& escaped)

src/pointer-analysis/local_value_set_analysis.cpp

@@ -88,6 +88,8 @@ class local_value_set_analysist
 
   void save_summary(const goto_programt&);
 
+  bool is_singular(const std::set<exprt> &);
+
   size_t nstubs;
   size_t nstub_assignments;
 

src/pointer-analysis/local_value_set_analysis.h

@@ -49,31 +49,13 @@ static bool is_pure_local(const exprt &lvalue, const symbol_utilst &nsu)
     !nsu.is_static(lvalue);
 }
 
-// Get whether an expression refers to a unique dynamic lvalue, as
-// opposed to e.g. a dynamic object expression, which refers to the
-// general case of objects allocated (at a particular program point)
-static bool is_expr_singular_object(
-  const object_numberingt &numbering, taint_lvalue_numbert lvalue_num)
-{
-  return get_underlying_object(numbering.at(lvalue_num)).id()==ID_symbol;
-}
-
-
 ////////////////////////////////////////////////////////////////////////////////
 ///
 /// LVSA related stuff : Should be moved to LVSA!
 ///
 ////////////////////////////////////////////////////////////////////////////////
 
 
-static void collect_lvsa_access_paths(
-  exprt const& e,
-  namespacet const& ns,
-  lvalue_numbers_sett& result,
-  local_value_set_analysist& lvsa,
-  instruction_iteratort const& instit,
-  object_numberingt&);
-
 struct parameter_matches_id {
   parameter_matches_id(const irep_idt& _id) : id(_id) {}
   bool operator()(const code_typet::parametert& p) const
@@ -167,11 +149,21 @@ static exprt transform_external_objects(const exprt& e)
 static void collect_lvsa_access_paths(
   exprt const& querye_in,
   namespacet const& ns,
-  lvalue_numbers_sett& result,
   local_value_set_analysist& lvsa,
   instruction_iteratort const& instit,
-  object_numberingt& taint_object_numbering)
+  std::set<exprt> &result)
 {
+  if(querye_in.id()==ID_side_effect)
+  {
+    side_effect_exprt const see=to_side_effect_expr(querye_in);
+    if(see.get_statement()==ID_nondet)
+    {
+      // TODO(marek-trtik): Add computation of a proper points-to set for NONDET
+      //                    in a side-effect expression
+      assert(false);
+    }
+  }
+
   const exprt* querye=&querye_in;
   while(querye->id()==ID_typecast)
     querye=&querye->op0();
@@ -207,7 +199,7 @@ static void collect_lvsa_access_paths(
       else if(get_underlying_object(transformed_object).id()=="NULL-object")
         continue;
 
-      result.insert(taint_object_numbering.number(transformed_object));
+      result.insert(transformed_object);
     }
   }
   else
@@ -216,13 +208,55 @@ static void collect_lvsa_access_paths(
       collect_lvsa_access_paths(
         *it,
         ns,
-        result,
         lvsa,
         instit,
-        taint_object_numbering);
+        result);
   }
 }
 
+static void collect_lvsa_access_paths(
+  exprt const& querye_in,
+  namespacet const& ns,
+  local_value_set_analysist& lvsa,
+  instruction_iteratort const& instit,
+  object_numberingt& taint_object_numbering,
+  lvalue_numbers_sett& result,
+  bool &singular)
+{
+  std::set<exprt> referees;
+  collect_lvsa_access_paths(
+    querye_in,
+    ns,
+    lvsa,
+    instit,
+    referees);
+
+  singular=lvsa.is_singular(referees);
+
+  for(const exprt &object : referees)
+    result.insert(taint_object_numbering.number(object));
+}
+
+static void collect_lvsa_access_paths(
+  exprt const& querye_in,
+  namespacet const& ns,
+  lvalue_numbers_sett &result,
+  local_value_set_analysist& lvsa,
+  instruction_iteratort const& instit,
+  object_numberingt& taint_object_numbering)
+{
+  bool singular=false;
+
+  collect_lvsa_access_paths(
+    querye_in,
+    ns,
+    lvsa,
+    instit,
+    taint_object_numbering,
+    result,
+    singular);
+}
+
 static void populate_formals_to_actuals(
   local_value_set_analysist& lvsa,
   const irep_idt& fname,
@@ -817,49 +851,29 @@ void taint_algorithm_computing_summary_of_functiont::handle_assignment(
   }
 
   lvalue_numbers_sett lhs;
+  bool singular=false;
   collect_lvsa_access_paths(
     asgn.lhs(),
     program->get_namespace(),
-    lhs,
     lvsa,
     Iit,
-    *numbering);
-  for(const auto &path : lhs)
+    *numbering,
+    lhs,
+    singular);
+
+  if(singular)
   {
-    // Get whether an expression refers to a unique dynamic lvalue, as
-    // opposed to e.g. a dynamic object expression, which refers to the
-    // general case of objects allocated [at a particular program point]
-    bool is_singular_object = is_expr_singular_object(*numbering, path);
-    if(lhs.size()>1 || (lhs.size()==1 && !is_singular_object))
-      maybe_assign(result, path, taint);
-    else
-      assign(result, path, taint);
+    // Singular implies that lhs has exactly one element,
+    // so we can access it directly
+    assign(result, *lhs.begin(), taint);
   }
-}
-
-void taint_algorithm_computing_summary_of_functiont::
-  compute_aliased_numbers_of_lvalue(
-    const taint_lvaluet &lvalue,
-    const instruction_iteratort &Iit,
-    local_value_set_analysist &lvsa,
-    lvalue_numbers_sett &numbers_of_aliases)
-{
-  if(lvalue.id() == ID_side_effect)
+  else
   {
-    side_effect_exprt const see=to_side_effect_expr(lvalue);
-    if(see.get_statement()==ID_nondet)
+    for(const auto &path : lhs)
     {
-      // TODO!
-      assert(false);
+      maybe_assign(result, path, taint);
     }
   }
-  collect_lvsa_access_paths(
-    lvalue,
-    program->get_namespace(),
-    numbers_of_aliases,
-    lvsa,
-    Iit,
-    *numbering);
 }
 
 taint_sett taint_algorithm_computing_summary_of_functiont::
@@ -870,11 +884,13 @@ taint_sett taint_algorithm_computing_summary_of_functiont::
     const numbered_lvalue_to_taint_mapt &a)
 {
   lvalue_numbers_sett numbers_of_aliases;
-  compute_aliased_numbers_of_lvalue(
+  collect_lvsa_access_paths(
     lvalue,
-    Iit,
+    program->get_namespace(),
+    numbers_of_aliases,
     lvsa,
-    numbers_of_aliases);
+    Iit,
+    *numbering);
   taint_sett result;
   for(taint_lvalue_numbert lvalue_number : numbers_of_aliases)
   {
@@ -895,19 +911,28 @@ void taint_algorithm_computing_summary_of_functiont::
     numbered_lvalue_to_taint_mapt &result)
 {
   lvalue_numbers_sett numbers_of_aliases;
-  compute_aliased_numbers_of_lvalue(
+  bool singular=false;
+  collect_lvsa_access_paths(
     lvalue,
-    Iit,
+    program->get_namespace(),
     lvsa,
-    numbers_of_aliases);
-  for(taint_lvalue_numbert lvalue_number : numbers_of_aliases)
+    Iit,
+    *numbering,
+    numbers_of_aliases,
+    singular);
+
+  if(singular && is_allowed_pure_assignment)
+  {
+    // Singular implies that lhs has exactly one element,
+    // so we can access it directly
+    assign(result, *numbers_of_aliases.begin(), taint_from_rule);
+  }
+  else
   {
-    bool is_singular_object = is_expr_singular_object(*numbering, lvalue_number);
-    if(!is_allowed_pure_assignment || numbers_of_aliases.size()>1ULL ||
-        (numbers_of_aliases.size()==1ULL && !is_singular_object))
+    for(taint_lvalue_numbert lvalue_number : numbers_of_aliases)
+    {
       maybe_assign(result, lvalue_number, taint_from_rule);
-    else
-      assign(result, lvalue_number, taint_from_rule);
+    }
   }
 }
 
@@ -944,11 +969,13 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
               replace_it->second, Iit, lvsa, a);
 
             lvalue_numbers_sett numbers_of_aliases;
-            compute_aliased_numbers_of_lvalue(
+            collect_lvsa_access_paths(
               replace_it->second,
-              Iit,
+              program->get_namespace(),
+              numbers_of_aliases,
               lvsa,
-              numbers_of_aliases);
+              Iit,
+              *numbering);
             assert(!numbers_of_aliases.empty());
             std::stringstream sstr;
             sstr << "However, instead of applying NONDET as the right-hand-side"

src/taint-analysis/taint_summary.cpp

@@ -266,12 +266,6 @@ class taint_algorithm_computing_summary_of_functiont
     instruction_iteratort const& Iit,
     local_value_set_analysist &lvsa);
 
-  void compute_aliased_numbers_of_lvalue(
-    const taint_lvaluet &lvalue,
-    const instruction_iteratort &Iit,
-    local_value_set_analysist &lvsa,
-    lvalue_numbers_sett &numbers_of_aliases);
-
   taint_sett compute_taint_of_aliased_numbers_of_lvalue(
     const taint_lvaluet &lvalue,
     const instruction_iteratort &Iit,