Merge pull request diffblue#492 from diffblue/smowton/cleanup/remove-…

…nondet-handlers

Remove nondet expression handlers

src/taint-analysis/taint_program.cpp

@@ -12,95 +12,13 @@
 #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 goto_programt::instructionst &instructions =
-      elem.second.body.instructions;
-    for(auto instr_it = instructions.begin(); instr_it != instructions.end();
-        ++instr_it)
-    {
-      auto next_instr_it = std::next(instr_it);
-      if(
-        next_instr_it != instructions.end() &&
-        instr_it->type == FUNCTION_CALL && next_instr_it->type == ASSIGN)
-      {
-        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(
-          {
-            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() });
-      }
-    }
-  }
-}
-
 taint_programt::taint_programt(
     const goto_modelt &model,
     taint_statisticst &statistics)
   : model(model), ns(model.symbol_table)
 {
   statistics.begin_goto_program_building();
 
-  build_NONDET_retvals_replacements(model, ns, NONDET_retvals_replacements);
-
   class_hierarchy(model.symbol_table);
 
   call_graph = call_grapht(model.goto_functions);

src/taint-analysis/taint_program.h

@@ -79,12 +79,6 @@ class taint_programt
     return inverted_topological_order;
   }
 
-  const replacements_of_NONDET_retvalst& get_NONDET_retvals_replacements()
-    const noexcept
-  {
-    return NONDET_retvals_replacements;
-  }
-
 private:
   taint_programt() = delete;
   taint_programt(const taint_programt &) = delete;
@@ -97,7 +91,6 @@ class taint_programt
   call_grapht inv_call_graph;
   call_grapht::directed_grapht directed_call_graph;
   std::vector<irep_idt> inverted_topological_order;
-  replacements_of_NONDET_retvalst NONDET_retvals_replacements;
 };
 
 

src/taint-analysis/taint_statistics.cpp

@@ -77,21 +77,6 @@ static bool  is_instruction_GOTO(goto_programt::instructiont const&  I)
   return I.type == GOTO && I.guard.id() == ID_constant;
 }
 
-static bool  is_instruction_call_NONDET(goto_programt::instructiont const&  I)
-{
-  if (I.type == ASSIGN)
-  {
-    code_assignt const&  asgn = to_code_assign(I.code);
-    if (asgn.rhs().id() == ID_side_effect)
-    {
-      side_effect_exprt const  see = to_side_effect_expr(asgn.rhs());
-      if(see.get_statement() == ID_nondet)
-        return true;
-    }
-  }
-  return false;
-}
-
 static bool  is_instruction_StringBuilder_call(
     goto_programt::instructiont const&  I,
     const namespacet &ns)
@@ -153,7 +138,6 @@ taint_function_statisticst::taint_function_statisticst(
     num_temporaries(0UL),
     num_assignments_to_temporaries(0UL),
     num_dead_statements(0UL),
-    num_NONDET_calls(0UL),
     num_SKIPs(0UL),
     num_GOTOs(0UL),
     num_string_builder_lines(0UL),
@@ -424,11 +408,6 @@ void  taint_statisticst::end_goto_program_building(
           fn_stats.on_dead_statement();
           is_auxiliaty = true;
         }
-        if(is_instruction_call_NONDET(I))
-        {
-          fn_stats.on_NONDET_call();
-          is_auxiliaty = true;
-        }
         if(is_instruction_SKIP(I))
         {
           fn_stats.on_SKIP();

src/taint-analysis/taint_statistics.h

@@ -41,7 +41,6 @@ class taint_function_statisticst
   void on_temporary() { ++num_temporaries; }
   void on_assignment_to_temporary() { ++num_assignments_to_temporaries; }
   void on_dead_statement() { ++num_dead_statements; }
-  void on_NONDET_call() { ++num_NONDET_calls; }
   void on_SKIP() { ++num_SKIPs; }
   void on_GOTO() { ++num_GOTOs; }
   void on_string_builder_line() { ++num_string_builder_lines; }
@@ -84,8 +83,6 @@ class taint_function_statisticst
   { return num_assignments_to_temporaries; }
   std::size_t get_num_dead_statements() const noexcept
   { return num_dead_statements; }
-  std::size_t get_num_NONDET_calls() const noexcept
-  { return num_NONDET_calls; }
   std::size_t get_num_SKIPs() const noexcept
   { return num_SKIPs; }
   std::size_t get_num_GOTOs() const noexcept
@@ -157,7 +154,6 @@ class taint_function_statisticst
   std::size_t num_temporaries;
   std::size_t num_assignments_to_temporaries;
   std::size_t num_dead_statements;
-  std::size_t num_NONDET_calls;
   std::size_t num_SKIPs;
   std::size_t num_GOTOs;
   std::size_t num_string_builder_lines;

src/taint-analysis/taint_statistics_dump_html.cpp

@@ -202,7 +202,6 @@ static void  taint_global_program_stats_table(
   std::size_t  num_temporaries = 0UL;
   std::size_t  num_assgns_to_temporaries = 0UL;
   std::size_t  num_dead_statements = 0UL;
-  std::size_t  num_NONDET_calls = 0UL;
   std::size_t  num_SKIPs = 0UL;
   std::size_t  num_GOTOs = 0UL;
   std::size_t  num_string_builders = 0UL;
@@ -219,7 +218,6 @@ static void  taint_global_program_stats_table(
       num_temporaries += fS.get_num_temporaries();
       num_assgns_to_temporaries += fS.get_num_assignments_to_temporaries();
       num_dead_statements += fS.get_num_dead_statements();
-      num_NONDET_calls += fS.get_num_NONDET_calls();
       num_SKIPs += fS.get_num_SKIPs();
       num_GOTOs += fS.get_num_GOTOs();
       num_string_builders += fS.get_num_string_builder_lines();
@@ -266,12 +264,6 @@ static void  taint_global_program_stats_table(
           "  </tr>\n"
           ;
 
-  ostr << "  <tr>\n"
-          "    <td>Number of locations performing calls to NONDET()</td>\n"
-          "    <td align=\"right\">" << num_NONDET_calls << "</td>\n"
-          "  </tr>\n"
-          ;
-
   ostr << "  <tr>\n"
           "    <td>Number of SKIP statement locations</td>\n"
           "    <td align=\"right\">" << num_SKIPs << "</td>\n"
@@ -365,12 +357,6 @@ static void  taint_function_stats_table(
           "  </tr>\n"
           ;
 
-  ostr << "  <tr>\n"
-          "    <td>Number of calls to NONDET() function</td>\n"
-          "    <td align=\"right\">" << fS.get_num_NONDET_calls() << "</td>\n"
-          "  </tr>\n"
-          ;
-
   ostr << "  <tr>\n"
           "    <td>Number of SKIP statements</td>\n"
           "    <td align=\"right\">" << fS.get_num_SKIPs() << "</td>\n"

src/taint-analysis/taint_statistics_dump_json.cpp

@@ -97,8 +97,6 @@ static void  taint_dump_files_table(
                 );
         fn_table["num-DEAD-statements"] =
             json_numbert(msgstream() << fS.get_num_dead_statements());
-        fn_table["num-NONDET-calls"] =
-            json_numbert(msgstream() << fS.get_num_NONDET_calls());
         fn_table["num-SKIP-statements"] =
             json_numbert(msgstream() << fS.get_num_SKIPs());
         fn_table["num-GOTO-unconditional-statements"] =
@@ -191,4 +189,4 @@ void taint_dump_statistics_in_JSON(
     boost::filesystem::create_directory(out_file_pathname.parent_path());
   std::ofstream ostr(out_file_pathname.native());
   taint_dump_statistics_in_JSON(stats, ostr);
-}
+}

src/taint-analysis/taint_summary.cpp

@@ -179,16 +179,6 @@ static void collect_lvsa_access_paths(
 {
   TMPROF_BLOCK();
 
-  if(query.id() == ID_side_effect)
-  {
-    const side_effect_exprt &see = to_side_effect_expr(query);
-    if(see.get_statement()==ID_nondet)
-    {
-      // TODO(marek-trtik): Add computation of a proper points-to set for NONDET
-      //                    in a side-effect expression
-    }
-  }
-
   if(
     query.id() == ID_symbol || query.id() == ID_index ||
     query.id() == ID_member || query.id() == ID_dereference)
@@ -984,64 +974,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
 
       transition_properties[Iit].push_back(
         {taint_transition_property_typet::ASSIGNMENT, taint_rule_idt{}, ""});
-      const code_assignt &asgn=to_code_assign(I.code);
-      if(asgn.rhs().id()==ID_side_effect)
-      {
-        const side_effect_exprt see=to_side_effect_expr(asgn.rhs());
-        if(see.get_statement()==ID_nondet)
-        {
-          const auto replace_it=
-            program->get_NONDET_retvals_replacements().find(Iit);
-          if(replace_it!=program->get_NONDET_retvals_replacements().cend())
-          {
-            taint_sett taint =
-              compute_taint_of_aliased_numbers_of_lvalue(
-                replace_it->second, Iit, lvsa, input, a);
-
-            lvalue_numbers_sett numbers_of_aliases;
-            collect_lvsa_access_paths_extended(
-              replace_it->second, Iit, lvsa, numbers_of_aliases);
-            assert(!numbers_of_aliases.empty());
-            std::stringstream sstr;
-            sstr << "However, instead of applying NONDET as the right-hand-side"
-                    " expression of the assignment, join of values of these "
-                    "expressions was taken:";
-            bool first = true;
-            for(const auto num : numbers_of_aliases)
-            {
-              assert(num < numbering->size());
-              if(!first)
-                sstr << ", ";
-              sstr << from_expr(program->get_namespace(), "", numbering->at(num));
-              first = false;
-            }
-            sstr << ".";
-            transition_properties[Iit].push_back(
-              {taint_transition_property_typet::ASSIGNMENT,
-               taint_rule_idt{},
-               sstr.str()});
-
-            lvalue_numbers_sett lhs;
-            collect_lvsa_access_paths_extended(asgn.lhs(), Iit, lvsa, lhs);
-            for(const auto& path : lhs)
-            {
-              if(lhs.size() > 1UL)
-                maybe_assign(result, path, taint);
-              else
-                assign(result, path, taint);
-            }
-            return result;
-          }
-          else
-          {
-            // If this is not listed in get_NONDET_retvals, then it must be
-            // unrelated to a stub function call and does not need this special
-            // treatment.
-            break;
-          }
-        }
-      }
-      handle_assignment(asgn, a, input, result, Iit, lvsa);
+      handle_assignment(to_code_assign(I.code), a, input, result, Iit, lvsa);
     }
     break;
   case FUNCTION_CALL:

src/taint-slicer/instrumenter.cpp

@@ -109,9 +109,7 @@ exprt make_or_update_initialiser(
   const std::set<taint_instrumentert::automaton_variable_idt> &
     names_of_shadow_variables)
 {
-  if(new_type.id()!=ID_struct ||
-    (initialiser.id() == ID_side_effect &&
-      to_side_effect_expr(initialiser).get_statement() == ID_nondet))
+  if(new_type.id() != ID_struct)
   {
     // Rewrite type regardless, for example to turn (array*)null into
     // (wrapped_array*)null