Merge pull request diffblue#330 from diffblue/bugfix/downcast_issue_solved_by_moving_shadow_vars_to_Object

SEC-218: Bugfix: Downcast issue resolved by moving shadow vars to java.lang.Object.

Author: marek-trtik

regression/end_to_end/taint_over_downcast/test_taint_over_downcast.py

@@ -1,24 +1,10 @@
 import regression.end_to_end.driver as pipeline_executor
 import os
 import subprocess
-import pytest
 import regression.utils as utils
 
 
-@pytest.mark.xfail(strict=True)
 def test_taint_over_downcast():
-    """
-    Wrong handling of down-casting. Here are related lines of the goto program:
-            new_tmp0 = ALLOCATE(struct Derived, 5ul, false);
-            a = (struct Base *)&new_tmp0->@Base;
-            a->@__CPROVER_com_diffblue_security_Tainted_data = true;
-            IF !((struct Derived *)a)->@__CPROVER_com_diffblue_security_Tainted_data THEN GOTO 2
-            ASSERT false
-        2:  ...
-    So, the access path to @__CPROVER_com_diffblue_security_Tainted in the IF
-    statement should rather be
-            (&(((struct Derived *)a)->@Base))->@__CPROVER_com_diffblue_security_Tainted
-    """
     with utils.working_dir(os.path.abspath(os.path.dirname(__file__))):
         subprocess.call("ant")
     traces = pipeline_executor.run_security_analyser_pipeline(

regression/end_to_end/tainted-user-class/test_tainted_user_class.py

@@ -5,6 +5,7 @@
 import os.path
 import pytest
 
+@pytest.mark.user_class
 def test_user_class():
     traces = run_security_analyser_pipeline(
         "test.class",
@@ -13,7 +14,7 @@ def test_user_class():
     assert traces.count_traces() > 0
     assert traces.trace_exists("java::test.main:(I)V", 16)
 
-@pytest.mark.xfail(strict=True)
+@pytest.mark.user_subclass
 def test_user_subclass():
     """
     The issue is the instrumentation; Although the taint var is here
@@ -22,7 +23,7 @@ def test_user_subclass():
         IF !((struct test *)anonlocal::3a)->@__CPROVER_XXX THEN GOTO 5
     """
     traces = run_security_analyser_pipeline(
-        "subclass.class",
+        "./",
         "subclass_rules.json",
         os.path.realpath(os.path.dirname(__file__)))
     assert traces.count_traces() == 1

src/taint-slicer/instrumentation_props.cpp

@@ -55,9 +55,7 @@ bool is_java_array_type_name(const std::string &datatype)
 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";
+  return is_primitive_type(type) || is_java_array_type_name(datatype);
 }
 
 static typet get_return_type_from_function_name(

src/taint-slicer/instrumenter.cpp

@@ -606,42 +606,6 @@ void taint_instrumentert::instrument_instructions_with_shadow_variables(
   }
 }
 
-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())
-      {
-        // Nothing to do here, because we handle subclassed data types
-        // differently. See calls to 'substitute_subclassed_types' from
-        // 'taint_instrumentert::instrument_data_types' for details.
-      }
-      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 &in_props,
   const taint_programt *const in_program,
@@ -870,13 +834,37 @@ void taint_instrumentert::instrument_data_types(
     }
     else
     {
-      symbolt &symbol=*instrumented_symbol_table.get_writeable(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);
+      namespacet ns(instrumented_symbol_table);
+      const symbolt *symbol_ptr = &ns.lookup(id_info.first);
+      while(true)
+      {
+        INVARIANT(
+          symbol_ptr->type.id() == ID_struct,
+          "In this branch the instrumented type must always be a struct type.");
+        const struct_typet &struct_type = to_struct_type(symbol_ptr->type);
+        const struct_typet::componentst &components = struct_type.components();
+        INVARIANT(
+          !components.empty(),
+          "The class has either a parent or class identifier.");
+        auto type = namespacet(instrumented_symbol_table)
+                      .follow(components.front().type());
+        if(type.id() != ID_struct)
+          break;
+        symbol_ptr =
+          &ns.lookup("java::" + as_string(to_struct_type(type).get_tag()));
+      }
+      struct_typet &struct_type = to_struct_type(
+        instrumented_symbol_table.get_writeable(symbol_ptr->name)->type);
+      struct_typet::componentst &components = struct_type.components();
+      for(const taint_instrumentert::automaton_variable_idt &var : vars)
+      {
+        if(!struct_type.has_component(var))
+        {
+          components.push_back(struct_typet::componentt{var, bool_typet()});
+          components.back().set_pretty_name(var);
+          components.back().set_access(ID_public);
+        }
+      }
     }
   }
 
@@ -927,18 +915,45 @@ static exprt get_accessor_expression_to_shadow_variable_from_call_expression(
 }
 
 static exprt make_accessor_expression_to_shadow_variable(
-  const exprt &argument, const std::string &shadow_variable_name)
+  const exprt &argument,
+  const std::string &shadow_variable_name,
+  const symbol_tablet &symbol_table)
 {
-  if(argument.type().id()==ID_pointer)
+  namespacet ns(symbol_table);
+  const typet &arg_type = ns.follow(argument.type());
+  if(arg_type.id() == ID_pointer)
   {
-    const pointer_typet pt=to_pointer_type(argument.type());
-    return member_exprt(
+    const pointer_typet pt = to_pointer_type(arg_type);
+    return make_accessor_expression_to_shadow_variable(
       dereference_exprt(argument, pt.subtype()),
       shadow_variable_name,
-      bool_typet());
+      symbol_table);
   }
-  else
-    return member_exprt(argument, shadow_variable_name, bool_typet());
+  INVARIANT(
+    arg_type.id() == ID_struct,
+    "The remaining possible case is that the arg_type is of a class type.");
+  exprt access_path = argument;
+  typet type = arg_type;
+  while(true)
+  {
+    const struct_typet &struct_type = to_struct_type(type);
+    if(struct_type.has_component(shadow_variable_name))
+    {
+      access_path =
+        member_exprt(access_path, shadow_variable_name, bool_typet());
+      break;
+    }
+    const struct_typet::componentst &components = struct_type.components();
+    INVARIANT(
+      !components.empty(), "The class has either the shadow var of a parent.");
+    access_path = member_exprt(
+      access_path, components.front().get_name(), components.front().type());
+    type = ns.follow(components.front().type());
+    INVARIANT(
+      type.id() == ID_struct,
+      "The base class instance is stored by value and must be available.");
+  }
+  return access_path;
 }
 
 void taint_instrumentert::instrument_location(
@@ -989,9 +1004,10 @@ void taint_instrumentert::instrument_location(
           fn_call,
           assumption.get_argidx(),
           instrumented_symbol_table);
-      const exprt proposition=make_accessor_expression_to_shadow_variable(
+      const exprt proposition = make_accessor_expression_to_shadow_variable(
         acc_path,
-        from_tokens_to_vars.at(assumption.get_token_name()));
+        from_tokens_to_vars.at(assumption.get_token_name()),
+        instrumented_symbol_table);
       conjuncts.push_back(proposition);
     }
     auto iit=instrumentation_code.add_instruction();
@@ -1019,10 +1035,11 @@ void taint_instrumentert::instrument_location(
           get_accessor_expression_to_shadow_variable_from_call_expression(
             fn_call, arg_token.get_argidx(), symbol_table);
         auto iit=instrumentation_code.add_instruction(ASSIGN);
-        iit->code=code_assignt(
+        iit->code = code_assignt(
           make_accessor_expression_to_shadow_variable(
             acc_path,
-            from_tokens_to_vars.at(arg_token.get_token_name())),
+            from_tokens_to_vars.at(arg_token.get_token_name()),
+            symbol_table),
           constant_exprt(bool_state_name, typet(ID_bool)));
         iit->function=function_id;
       }