Improved comments and made symbol static

Author: Owen Jones

src/taint-analysis/taint_program.cpp

@@ -43,6 +43,13 @@ static void build_NONDET_retvals_replacements(
               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();
@@ -58,6 +65,12 @@ static void build_NONDET_retvals_replacements(
               }
               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;
@@ -70,10 +83,8 @@ static void build_NONDET_retvals_replacements(
                 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);
-                // NOTE: This is not a sound solution. However, handling of
-                //       NONDETs is just a temporary solution, until we
-                //       get rid of them completely.
                 replacements.insert({instr_it, symbol.symbol_expr()});
               }
             }