Merge pull request diffblue#133 from diffblue/marek/instr_props_PR

Extension of instrumentation props for support of shadow variables.

Author: marek-trtik

security-scanner/presentation.py

@@ -139,7 +139,45 @@ def build_HTML_interface_to_slicer_instrumentation_props(props,fname):
     with open(fname,"w") as ofile:
         ofile.write(get_html_prefix("Instrumentation props"))
 
-        ofile.write("<h2>Definition of states of the instrumentation automaton</h2>\n")
+        ofile.write("<h1>Instrumentation properties</h1>\n")
+
+        ofile.write("<p>\n")
+        ofile.write("These data represent a complete information for instrumentation\n")
+        ofile.write("of shadow variables and related program statements into the GOTO program.\n")
+        ofile.write("</p>\n")
+
+        ofile.write("<h2>Definition of data types for instrumentation</h2>\n")
+
+        ofile.write("<p>\n")
+        ofile.write("This is a list of program types which will be instrumented by shadow variables\n")
+        ofile.write("identified here by the corresponding names of tokens.\n")
+        ofile.write("</p>\n")
+
+        ofile.write("<table>\n")
+        ofile.write("  <tr>\n")
+        ofile.write("    <th>Type name</th>\n")
+        ofile.write("    <th>Shadow variables</th>\n")
+        ofile.write("    <th>Create sub-class?</th>\n")
+        ofile.write("  </tr>\n")
+        for dtype in props["datatypes"]:
+            ofile.write("  <tr>\n")
+            ofile.write("    <td>" + escape_text_to_HTML(dtype["type_name"]) + "</td>\n")
+            ofile.write("    <td>\n")
+            ofile.write("       <ul>\n")
+            for var in dtype["shadow_vars"]:
+                ofile.write("       <li>" + escape_text_to_HTML(var) + "</li>\n")
+            ofile.write("       </ul>\n")
+            ofile.write("    </td>\n")
+            ofile.write("    <td align=\"center\">" + str(dtype["make_subclass"]) + "</td>\n")
+            ofile.write("  </tr>\n")
+        ofile.write("</table>\n")
+
+        ofile.write("<h2>Definition of instrumentation statements</h2>\n")
+
+        ofile.write("<p>\n")
+        ofile.write("This is a list of program locations and descriptions of program statemenets\n")
+        ofile.write("to be instrumented (at those locations).\n")
+        ofile.write("</p>\n")
 
         state_index = 0
         for loc in props["location_props"]:

src/taint-slicer/instrumentation_props.cpp

@@ -22,9 +22,60 @@ instrumentation_props data structure.
 \*******************************************************************/
 
 #include <taint-slicer/instrumentation_props.h>
+#include <goto-programs/remove_returns.h>
+#include <java_bytecode/java_types.h>
+#include <java_bytecode/expr2java.h>
+#include <util/prefix.h>
 #include <util/msgstream.h>
 #include <deque>
 
+bool is_primitive_type(const typet &type)
+{
+  return type==java_boolean_type() ||
+         type==java_byte_type() ||
+         type==java_char_type() ||
+         type==java_short_type() ||
+         type==java_int_type() ||
+         type==java_long_type() ||
+         type==java_float_type() ||
+         type==java_double_type();
+}
+
+std::string unwrap_type_name(const typet &type, const namespacet &ns)
+{
+  if(type.id()==ID_pointer)
+    return unwrap_type_name(to_pointer_type(type).subtype(), ns);
+  if(type.id()==ID_array)
+    return unwrap_type_name(to_array_type(type).subtype(), ns);
+  if(type.id()==ID_symbol)
+    return as_string(to_symbol_type(type).get_identifier());
+  const std::string result=type2java(type, ns);
+  if(!is_primitive_type(type))
+    throw std::logic_error(
+      "ERROR: expecting a primitive data type, but received '" + result + "'.");
+  return result;
+}
+
+bool is_java_array_type_name(const std::string &datatype)
+{
+  return has_prefix(datatype, "java::array[") && *datatype.rbegin()==']';
+}
+
+bool does_instrumentation_of_type_require_subclass(
+  const std::string &datatype, const typet &type)
+{
+  return is_primitive_type(type) ||
+         is_java_array_type_name(datatype) ||
+         datatype=="java::java.lang.Object";
+}
+
+static typet get_return_type_from_function_name(
+  const std::string &fname, const symbol_tablet &symbol_table)
+{
+  assert(symbol_table.has_symbol(fname+RETURN_VALUE_SUFFIX));
+  return symbol_table.lookup(fname+RETURN_VALUE_SUFFIX).type;
+}
+
 /*******************************************************************\
 
 Function: perform_BFS
@@ -72,6 +123,7 @@ static void perform_BFS(
 
 taint_instrumentation_propst::taint_instrumentation_propst(
   const taint_propagation_chainst &chains,
+  const taint_programt &program,
   const taint_function_idt &_root,
   const std::set<taint_function_idt> &in_functions,
   const std::set<taint_function_idt> &in_suppressed)
@@ -107,14 +159,96 @@ taint_instrumentation_propst::taint_instrumentation_propst(
       sinks.insert(location_props.size());
     location_props.push_back(chains.get_nodes().at(nid));
   }
+
+  build_map_from_typenames_to_tokennames(chains, program);
+}
+
+
+/*******************************************************************\
+
+Function: build_map_from_typenames_to_tokennames
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+  The function fills in the member map "datatypes" so that for each
+  data type (identified by its type name, see "unwrap_type_name") to be
+  instrumented by a shadow variable there is computed an instance of
+  "taint_instrumentation_propst::datatype_infot" type holding details
+  about the instrumentation of the shadow variable into that type.
+
+\*******************************************************************/
+void taint_instrumentation_propst::build_map_from_typenames_to_tokennames(
+  const taint_propagation_chainst &chains,
+  const taint_programt &program)
+{
+  for(const auto &loc : get_location_props())
+  {
+    const goto_programt::instructiont &I=*loc.get_instruction_id();
+    assert(I.type==FUNCTION_CALL);
+    const code_function_callt &fn_call = to_code_function_call(I.code);
+    const exprt &callee_expr = fn_call.function();
+    assert(callee_expr.id()==ID_symbol);
+    irep_idt callee_id = to_symbol_expr(callee_expr).get_identifier();
+    const std::string callee_ident = as_string(callee_id);
+    const code_typet &fn_type =
+      program.get_functions().function_map.at(callee_id).type;
+
+    std::set<argidx_and_tokennamet> to_process;
+    for(const auto &elem : loc.get_assumption())
+      to_process.insert(elem);
+    for(const auto &elem : loc.get_turn_on())
+      to_process.insert(elem);
+    for(const auto &elem : loc.get_turn_off())
+      to_process.insert(elem);
+
+    for(const auto& arg_token : to_process)
+    {
+      assert(
+        arg_token.get_argidx()!=
+        taint_tokens_propagation_grapht::get_void_loc());
+      std::string datatype;
+      typet type;
+      if(arg_token.get_argidx()==-1) // Return value?
+        type=get_return_type_from_function_name(
+          callee_ident,
+          program.get_symbol_table());
+      else
+        type=fn_type.parameters().at(arg_token.get_argidx()).type();
+      datatype=unwrap_type_name(type, program.get_namespace());
+      auto it=datatypes.find(datatype);
+      if(it!=datatypes.end())
+      {
+        assert(
+          does_instrumentation_of_type_require_subclass(datatype, type)==
+            it->second.subclass_required() &&
+          is_primitive_type(type)==it->second.is_primitive());
+          it->second.add_token(arg_token.get_token_name());
+      }
+      else
+      {
+        datatypes.insert(
+          {
+            datatype,
+            {
+              datatype,
+              type,
+              does_instrumentation_of_type_require_subclass(datatype, type),
+              is_primitive_type(type),
+              { arg_token.get_token_name() }
+            }
+          });
+      }
+    }
+  }
 }
 
+
 void taint_build_instrumentation_props(
   const taint_propagation_chainst &chains,
-  const taint_tokens_propagation_grapht &tokens_propagation_graph,
-  const goto_functionst &program_functions,
-  const call_grapht &call_graph,
-  const call_grapht &inverted_call_graph,
+  const taint_programt &program,
   std::vector<taint_instrumentation_propst> &output)
 {
   // First we collect all functions mentioned in the graph of chains.
@@ -137,7 +271,8 @@ void taint_build_instrumentation_props(
   //              all of them in the call graph; a nearest common caller has no
   //              callees which are themselves common callers.
   std::set<irep_idt> roots;
-  find_nearest_common_callees(inverted_call_graph, functions, roots);
+  find_nearest_common_callees(
+    program.get_inverted_call_graph(), functions, roots);
 
   for(const auto &root : roots)
   {
@@ -150,7 +285,8 @@ void taint_build_instrumentation_props(
     std::set<taint_function_idt> suppressed;
     {
       // First we called all callees including those which should be suppressed.
-      find_direct_or_indirect_callees_of_function(call_graph, root, callees);
+      find_direct_or_indirect_callees_of_function(
+        program.get_call_graph(), root, callees);
       // Now we compute suppressed functions and erase them from the callees
       // computed above. We do so in 3 steps.
       // Step 1: We collect functions which definitelly should be suppressed.
@@ -165,8 +301,8 @@ void taint_build_instrumentation_props(
           const std::string full_function_name=as_string(to_symbol_expr(
             to_code_function_call(I.code).function()).get_identifier());
           if(callees.count(full_function_name)!=0UL &&
-             program_functions.function_map.at(full_function_name)
-                                           .body_available())
+             program.get_functions().function_map.at(full_function_name)
+                                                 .body_available())
           {
             suppressed.insert(full_function_name);
           }
@@ -178,7 +314,7 @@ void taint_build_instrumentation_props(
       std::unordered_set<irep_idt, dstring_hash> suppressions;
       for(const auto &fn : suppressed)
         find_direct_or_indirect_callees_of_function(
-          call_graph, fn, suppressions);
+          program.get_call_graph(), fn, suppressions);
       // Step 3: We copy from "suppressions" to "suppressed" each function
       //         reachable from the root without passing through any function
       //         collected in the step 1.
@@ -187,7 +323,8 @@ void taint_build_instrumentation_props(
         std::unordered_set<irep_idt, dstring_hash> ignored_functions(
           suppressed.cbegin(), suppressed.cend());
         if(!exists_direct_or_indirect_call(
-             call_graph, root, *suppressions.cbegin(), ignored_functions))
+          program.get_call_graph(), root, *suppressions.cbegin(),
+          ignored_functions))
         {
           suppressed.insert(as_string(*suppressions.cbegin()));
           callees.erase(*suppressions.cbegin());
@@ -202,13 +339,14 @@ void taint_build_instrumentation_props(
     // table.)
     std::set<taint_function_idt> available_functions;
     for(const auto &fn : callees)
-      if(program_functions.function_map.at(fn).body_available())
+      if(program.get_functions().function_map.at(fn).body_available())
         available_functions.insert(as_string(fn));
     // We are ready to create the instrumentation props for the root function.
     // This may fail, if the set of the corresponding chains is empty.
     const taint_instrumentation_propst props
     {
       chains,
+      program,
       as_string(root),
       available_functions,
       suppressed
@@ -220,6 +358,24 @@ void taint_build_instrumentation_props(
 
 void dump_as_json(const taint_instrumentation_propst &props, json_objectt &out)
 {
+  {
+    json_arrayt out_types;
+    for(const auto &elem : props.get_datatypes())
+    {
+      json_arrayt out_tokens;
+      for(const auto &name : elem.second.get_tokens())
+        out_tokens.push_back(json_stringt(msgstream() << name));
+      json_objectt out_type_props;
+      out_type_props["type_name"]=json_stringt(elem.first);
+      out_type_props["shadow_vars"]=out_tokens;
+      out_type_props["make_subclass"]=jsont::json_boolean(
+        elem.second.subclass_required());
+      out_type_props["is_primitive"]=jsont::json_boolean(
+        elem.second.is_primitive());
+      out_types.push_back(out_type_props);
+    }
+    out["datatypes"]=out_types;
+  }
   {
     json_arrayt out_locations;
     for(const auto &loc : props.get_location_props())