Instrumentation of shadow vars as class members into symbols table.

Author: marek-trtik

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,6 +39,40 @@ 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_programt *const in_program,
@@ -129,6 +164,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 +224,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

@@ -41,10 +41,10 @@ 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
+   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 function from those defined in
-   _program->get_functions() and which appear in props.get_location_props().
+   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().
 
@@ -66,6 +66,8 @@ class taint_instrumentert
 
 private:
 
+  void instrument_data_types(const taint_instrumentation_propst &props);
+
   /*******************************************************************\
 
   Function: instrument_location