Merge pull request diffblue#331 from diffblue/bugfix/non_replaced_occurrences_of_NONDET

SEC-224: Added replacement of missed NONDET calls.

Author: owen-jones-diffblue

src/taint-analysis/taint_program.cpp

@@ -32,8 +32,66 @@ static void build_NONDET_retvals_replacements(
       next_instr_it!=instructions.end();
       instr_it = next_instr_it, ++next_instr_it)
     {
-      if(instr_it->type!=FUNCTION_CALL || next_instr_it->type!=ASSIGN)
+      if(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 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;
+      }
       const code_function_callt &fn_call=to_code_function_call(instr_it->code);
       if(fn_call.function().id()!=ID_symbol)
         continue;