Merge pull request diffblue#178 from diffblue/feature/SV_to_classes_in_symbol_table

SEC-12: Instrumentation of shadow vars as class members into symbols table.

Author: smowton

src/taint-slicer/instrumenter.cpp

@@ -9,11 +9,12 @@
 ///   on instrumentation of data passed in "instrumentation_propst" instance.
 
 #include <taint-slicer/instrumenter.h>
+#include <taint-slicer/irept_instrument.h>
 #include <util/msgstream.h>
 
 std::string taint_prefix_of_instrumented_variable()
 {
-  return "__CPROVER_TAINT_SLICER_INSTRUMENTED_TOKEN_";
+  return "@__CPROVER_";
 }
 
 static std::string convert_token_id_to_program_identifier(
@@ -38,20 +39,61 @@ static std::string generate_fresh_automaton_variable_for_token(
   return var_name;
 }
 
+static irept add_shadow_variables_to_type(
+  const irept &type,
+  const std::vector<taint_instrumentert::automaton_variable_idt> &vars,
+  const taint_datatype_infot &info)
+{
+  if(type.id()==ID_struct)
+  {
+    const struct_typet &struct_type=
+      to_struct_type(static_cast<const typet &>(type));
+    const auto tag="java::"+as_string(struct_type.get_tag());
+    if(tag==info.get_id())
+    {
+      if(info.subclass_required())
+      {
+        // TODO!
+      }
+      else
+      {
+        struct_typet result=struct_type;
+        struct_typet::componentst &components=result.components();
+        for(const taint_instrumentert::automaton_variable_idt &var : vars)
+        {
+          components.push_back(struct_typet::componentt{
+            var, bool_typet() });
+          components.back().set_pretty_name(var);
+          components.back().set_access(ID_public);
+        }
+        return result;
+      }
+    }
+  }
+  return type;
+}
+
 taint_instrumentert::taint_instrumentert(
-  const taint_instrumentation_propst &props,
+  const taint_instrumentation_propst &in_props,
   const taint_programt *const in_program,
   taint_statisticst *const in_statistics,
   const bool use_data_flow_insensitive_instrumentation)
-  : program(in_program)
+  : props(in_props)
+  , program(in_program)
   , statistics(in_statistics)
   , use_data_flow_insensitive_version(use_data_flow_insensitive_instrumentation)
 {
-  // The next line must be here in order to prevent clang produce the error:
-  //    `error: private field 'use_data_flow_insensitive_version' is not used
-  //     [-Werror,-Wunused-private-field]`
-  (void)use_data_flow_insensitive_version;
+}
 
+/// Builds a new symbol table from the original symbol
+/// table in in_program->get_symbol_table(), by removing of symbols not related
+/// to the set of functions defined in the passed instrumentation properties.
+/// The function also build a new set of functions from those defined in
+/// in_program->get_functions() and which appear in props.get_location_props().
+/// These functions are instrumented by a new code accodring to recipes in
+/// individual elements of props.get_location_props().
+void taint_instrumentert::run()
+{
   assert(program!=nullptr);
   assert(statistics!=nullptr);
 
@@ -129,6 +171,13 @@ taint_instrumentert::taint_instrumentert(
         instr.type=ASSUME;
   }
 
+  if(!use_data_flow_insensitive_version)
+  {
+    // Now we introduce shadow variables as members of (1) existing types
+    // and (2) newly created types (for basic types).
+    instrument_data_types(props);
+  }
+
   // We have to change the way how we identify instrumentation locations.
   // Namely, instead of using iterators for referencing instructions we have to
   // switch to distances from the first instruction. This is because we operate
@@ -182,6 +231,32 @@ taint_instrumentert::taint_instrumentert(
   statistics=nullptr;
 }
 
+void taint_instrumentert::instrument_data_types(
+  const taint_instrumentation_propst &props)
+{
+  std::set<irep_idt> new_type_names;
+  for(const auto &id_info : props.get_datatypes())
+  {
+    std::vector<automaton_variable_idt> vars;
+    for(const auto &token : id_info.second.get_tokens())
+      vars.push_back(from_tokens_to_vars.at(token));
+    if(id_info.second.subclass_required())
+    {
+      // TODO!
+    }
+    else
+    {
+      symbolt &symbol=instrumented_symbol_table.lookup(id_info.first);
+      const irept itype=instrument(symbol.type, std::bind(
+        &add_shadow_variables_to_type,
+        std::placeholders::_1,
+        std::cref(vars),
+        std::cref(id_info.second)));
+      symbol.type=static_cast<const typet&>(itype);
+    }
+  }
+}
+
 std::size_t taint_instrumentert::instrument_location(
   const taint_instrumentation_propst::location_props_idt lid,
   const std::size_t instruction_index,

src/taint-slicer/instrumenter.h

@@ -40,13 +40,7 @@ class taint_instrumentert
 
    Outputs:
 
-   Purpose: The function builds a new symbol table from the original symbol
-   table in _program->get_symbol_table(), by removing of symbols not related
-   to the set of functions defined in the passed instrumentation properties.
-   The function also build a new set of function from those defined in
-   _program->get_functions() and which appear in props.get_location_props().
-   These functions are instrumented by a new code accodring to recipes in
-   individual elements of props.get_location_props().
+   Purpose:
 
   \*******************************************************************/
   taint_instrumentert(
@@ -55,6 +49,8 @@ class taint_instrumentert
     taint_statisticst * const in_statistics,
     const bool use_data_flow_insensitive_instrumentation);
 
+  void run();
+
   const goto_functionst &get_instrumented_functions() const
   { return instrumented_functions; }
 
@@ -66,6 +62,8 @@ class taint_instrumentert
 
 private:
 
+  void instrument_data_types(const taint_instrumentation_propst &props);
+
   /*******************************************************************\
 
   Function: instrument_location
@@ -87,6 +85,7 @@ class taint_instrumentert
     const std::size_t instruction_index,
     const taint_instrumentation_propst &props);
 
+  const taint_instrumentation_propst &props;
   const taint_programt *program;
   taint_statisticst *statistics;
   goto_functionst instrumented_functions;

src/taint-slicer/slicer.cpp

@@ -97,11 +97,14 @@ void taint_slicert::compute_slice(
   std::vector<taint_slicing_taskt> sliced_goto_programs;
   for(std::size_t i=0UL, n=instrumentation_props.size(); i!=n; ++i)
   {
-    const taint_instrumentert instrumenter(
+    taint_instrumentert instrumenter(
       instrumentation_props.at(i),
       program,
       statistics,
       use_data_flow_insensitive_instrumentation);
+
+    instrumenter.run();
+
     const std::pair<taint_slicing_taskt,std::string> task_valid=
       build_slicing_task(
         instrumentation_props.at(i),