Merge pull request diffblue#407 from diffblue/bugfix/build_NONDET_retvals_replacements

SEC-387: Check assignment lhs matches function call return value

Author: NathanJPhillips

src/taint-analysis/taint_program.cpp

@@ -12,98 +12,82 @@
 #include <analyses/call_graph_helpers.h>
 #include <unordered_set>
 
+/// Remove assignment of non-dets to values if they can't be reached
+/// Mark instances of function call followed by assignment of non-det to
+/// function's return value
 static void build_NONDET_retvals_replacements(
   const goto_modelt &model,
   const namespacet &ns,
   replacements_of_NONDET_retvalst &replacements)
 {
   for(const auto &elem : model.goto_functions.function_map)
   {
-    const auto & instructions=elem.second.body.instructions;
-    auto instr_it=instructions.begin();
-    if(instr_it==instructions.end())
-      continue;
-    for(auto next_instr_it=std::next(instr_it);
-      next_instr_it!=instructions.end();
-      instr_it = next_instr_it, ++next_instr_it)
+    const goto_programt::instructionst &instructions =
+      elem.second.body.instructions;
+    for(auto instr_it = instructions.begin(); instr_it != instructions.end();
+        ++instr_it)
     {
-      if(instr_it->type != FUNCTION_CALL || next_instr_it->type != ASSIGN)
+      auto next_instr_it = std::next(instr_it);
+      if(
+        next_instr_it != instructions.end() &&
+        instr_it->type == FUNCTION_CALL && next_instr_it->type == ASSIGN)
       {
-        if(instr_it->type == ASSIGN)
-        {
-          const code_assignt &assign = to_code_assign(instr_it->code);
-          if(assign.rhs().id() == ID_side_effect)
+        const code_assignt &asgn = to_code_assign(next_instr_it->code);
+        if(asgn.rhs().id() != ID_side_effect)
+          continue;
+        const side_effect_exprt see = to_side_effect_expr(asgn.rhs());
+        if(see.get_statement() != ID_nondet)
+          continue;
+
+        const code_function_callt &fn_call =
+          to_code_function_call(instr_it->code);
+        if(fn_call.function().id() != ID_symbol)
+          continue;
+        const irep_idt &callee_ident =
+          to_symbol_expr(fn_call.function()).get_identifier();
+
+        std::string callee_return_value_symbol =
+          id2string(callee_ident) + RETURN_VALUE_SUFFIX;
+        if(!ns.get_symbol_table().has_symbol(callee_return_value_symbol))
+          continue;
+
+        replacements.insert(
           {
-            const side_effect_exprt side_effect =
-              to_side_effect_expr(assign.rhs());
-            if(side_effect.get_statement() == ID_nondet)
-            {
-              // See if we can see that this instruction is definitely
-              // dead. Iterate backwards through the program from the current
-              // instruction, looking for an unconditional GOTO or a target.
-              // If we find an unconditional GOTO first then the instruction
-              // is dead. If we find a target first then we must assume that
-              // it can be reached. If we reach the beginning before finding
-              // either then the instruction is reachable.
-              bool is_dead = true;
-              for(auto sit = instr_it;
-                  sit != instructions.begin();
-                  sit=std::prev(sit))
-              {
-                if(sit->is_target())
-                {
-                  is_dead = false;
-                  break;
-                }
-                if(sit->type == GOTO && sit->guard.is_true())
-                  break;
-              }
-              if(is_dead || side_effect.type().id() == ID_pointer)
-              {
-                // Create a new static variable to put on the rhs of this
-                // assignment. When the instruction is dead then this is
-                // sound. Otherwise this is not sound, but it is
-                // preferable to having a pointer that could point to
-                // anything. A better solution would be to use the
-                // replace_java_nondet pass or similar.
-                static unsigned long counter = 0UL;
-                std::stringstream sstr;
-                sstr << "@__CPROVER_NONDET_dead_replace_" << ++counter;
-                symbolt symbol;
-                symbol.type =
-                  side_effect.type().id() == ID_pointer ?
-                    to_pointer_type(side_effect.type()).subtype() :
-                    side_effect.type();
-                symbol.name = sstr.str();
-                symbol.base_name = symbol.name;
-                symbol.mode = ID_java;
-                symbol.pretty_name = symbol.name;
-                symbol.is_static_lifetime = true;
-                const_cast<symbol_tablet&>(model.symbol_table).insert(symbol);
-                replacements.insert({instr_it, symbol.symbol_expr()});
-              }
-            }
-          }
-        }
-        continue;
+            next_instr_it,
+            ns.lookup(callee_return_value_symbol).symbol_expr()
+          });
+      }
+      else if(instr_it->type == ASSIGN)
+      {
+        const code_assignt &assign = to_code_assign(instr_it->code);
+        if(assign.rhs().id() != ID_side_effect)
+          continue;
+        const side_effect_exprt side_effect = to_side_effect_expr(assign.rhs());
+        if(side_effect.get_statement() != ID_nondet)
+          continue;
+        if(side_effect.type().id() != ID_pointer)
+          continue;
+        // Create a new static variable to put on the rhs of this
+        // assignment. When the instruction is dead then this is sound.
+        // Otherwise this is not sound, but it is preferable to having a
+        // pointer that could point to anything. A better solution would be
+        // to use the convert_nondet pass or similar.
+        static unsigned long counter = 0UL;
+        std::stringstream sstr;
+        sstr << "@__CPROVER_NONDET_dead_replace_" << ++counter;
+        symbolt symbol;
+        symbol.type =
+          side_effect.type().id() == ID_pointer
+            ? to_pointer_type(side_effect.type()).subtype()
+            : side_effect.type();
+        symbol.name = sstr.str();
+        symbol.base_name = symbol.name;
+        symbol.mode = ID_java;
+        symbol.pretty_name = symbol.name;
+        symbol.is_static_lifetime = true;
+        const_cast<symbol_tablet &>(model.symbol_table).insert(symbol);
+        replacements.insert({ instr_it, symbol.symbol_expr() });
       }
-      const code_function_callt &fn_call=to_code_function_call(instr_it->code);
-      if(fn_call.function().id()!=ID_symbol)
-        continue;
-      const irep_idt &callee_ident=
-        to_symbol_expr(fn_call.function()).get_identifier();
-
-      const code_assignt &asgn=to_code_assign(next_instr_it->code);
-      if(asgn.rhs().id()!=ID_side_effect)
-        continue;
-      const side_effect_exprt see=to_side_effect_expr(asgn.rhs());
-      if(see.get_statement()!=ID_nondet)
-        continue;
-      replacements.insert(
-        {
-          next_instr_it,
-          ns.lookup(id2string(callee_ident) + RETURN_VALUE_SUFFIX).symbol_expr()
-        });
     }
   }
 }