Computation of taint summaries for all functions (including those in rules).

Author: marek-trtik

src/summaries/summary_dump.cpp

@@ -1025,29 +1025,6 @@ void dump_irept(const irept &irep, std::ostream &ostr, const std::string &shift)
 }
 
 
-bool skip_fn_summary(const std::string &fname)
-{
-  if (fname.find("java::sun.") == 0UL
-      || fname.find("java::com.oracle.") == 0UL
-      || fname.find("java::com.sun.") == 0UL
-      || fname.find("java::java.") == 0UL
-      || fname.find("java::javax.") == 0UL
-      || fname.find("java::org.ietf.") == 0UL
-      || fname.find("java::org.jpc.") == 0UL
-      || fname.find("java::org.omg.") == 0UL
-      || fname.find("java::org.w3c.") == 0UL
-      || fname.find("java::org.xml.") == 0UL
-      || fname.find("java::jdk.") == 0UL
-      || fname.find("java::org.apache.") == 0UL
-      || fname.find("java::org.springframework.") == 0UL
-      || fname.find("java::org.json.") == 0UL
-      || fname.find("java::junit.") == 0UL
-      )
-    return true;
-  return false;
-}
-
-
 std::string to_file_name(std::string file_name, std::size_t suffix_length)
 {
   // The maximum file name length is 255 on most Linux file systems

src/summaries/summary_dump.h

@@ -101,7 +101,6 @@ void dump_instruction_code_in_html(
     );
 
 std::string to_file_name(std::string file_name, std::size_t suffix_length=15);
-bool skip_fn_summary(const std::string &fname);
 
 
 /// Functions to dump summaries to HTML.
@@ -152,8 +151,6 @@ class summary_dumpt:public messaget
     for(const std::pair<irep_idt, std::shared_ptr<summary_typet>> &summary
       : computed_summaries)
     {
-      if(skip_fn_summary(id2string(summary.first)))
-        continue;
       dump_in_html(
         summary.first,
         *summary.second,
@@ -182,8 +179,6 @@ class summary_dumpt:public messaget
       "  </tr>\n";
     for(const irep_idt &id : computed_summaries.keys())
     {
-      if(skip_fn_summary(id2string(id)))
-        continue;
       ostr
         << "  <tr>\n"
           "    <td>" << to_html_text(id2string(id)) << "</td>\n"

src/taint-analysis/taint_summary.cpp

@@ -702,23 +702,20 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
       const auto &fn_type=
         program->get_functions().function_map.at(callee_id).type;
 
-      if(!database.contains(callee_id))
+      for(const auto &arg : fn_call.arguments())
       {
-        // Normally should have already processed called functions as we
-        //  follow an inverted topological ordering
-        // This callee must recursively call us
-        for(const auto &arg : fn_call.arguments())
-        {
-          collect_lvsa_access_paths(
-            arg,
-            program->get_namespace(),
-            environment,
-            lvsa,
-            it,
-            *numbering);
-        }
-        continue;
+        collect_lvsa_access_paths(
+          arg,
+          program->get_namespace(),
+          environment,
+          lvsa,
+          it,
+          *numbering);
       }
+
+      if(!database.contains(callee_id))
+        continue;
+
       const std::shared_ptr<taint_summaryt> summary = database.at(callee_id);
       for(const std::pair<taint_lvalue_numbert, taint_variablet>& input
         : summary->input)
@@ -1499,7 +1496,6 @@ void taint_algorithm_computing_summary_of_functiont::
 void taint_algorithm_computing_summary_of_functiont::
   taint_summarise_function(
     const irep_idt &function_id,
-    bool function_has_taint_rule,
     taint_summaryt::dbt &database,
     local_value_set_analysist::dbt &lvsa_db)
 {
@@ -1539,11 +1535,6 @@ void taint_algorithm_computing_summary_of_functiont::
     lvsa.nstubs,
     lvsa.nstub_assignments);
 
-  // No need to analyse the internal taint flow of functions that have
-  // a taint axiom (source, sink or sanitizer) associated with them:
-  if(function_has_taint_rule)
-    return;
-
   if(database.contains(function_id))
     // Already been pre-computed
     return;
@@ -1700,7 +1691,6 @@ void taint_summarise_all_functions(
     const goto_functionst::function_mapt &functions_map =
         program->get_functions().function_map;
     const auto fn_it = functions_map.find(fn_name);
-    bool has_rule = transition_rules->has_rule(fn_name);
     if(fn_it!=functions_map.cend() && fn_it->second.body_available()
       && fn_name!="_start")
     {
@@ -1723,7 +1713,6 @@ void taint_summarise_all_functions(
         log);
       summariser.taint_summarise_function(
         fn_name,
-        has_rule,
         summaries_to_compute,
         lvsa_db);
       ++processed;
@@ -1738,8 +1727,7 @@ void taint_summarise_all_functions(
                     (double)topological_order_size)
         << "%] Skipping"
         << (fn_it!=functions_map.cend() && !fn_it->second.body_available()
-          ? " [function without a body]"
-          : has_rule ? " [function call representing a transition rule]" : "")
+          ? " [function without a body]" : "")
         << ": "
         << fn_name
         << messaget::eom;

src/taint-analysis/taint_summary.h

@@ -189,7 +189,6 @@ class taint_algorithm_computing_summary_of_functiont
 
   void taint_summarise_function(
     const irep_idt &function_id,
-    bool function_has_taint_rule,
     taint_summaryt::dbt &database,
     local_value_set_analysist::dbt &lvsa_db);