Merge pull request diffblue#480 from diffblue/removal_of_nondet_ptr

SEC-517, SEC-509: Removal of 'var = NONDET(SomeType *);' assignments.

Author: marek-trtik

src/driver/sec_driver_parse_options.cpp

@@ -512,29 +512,8 @@ void sec_driver_parse_optionst::process_goto_function(
 
     replace_java_nondet(function);
 
-#if 0 // Enable this when remove handling of NONDET in taint_analysis
-    // Similar removal of java nondet statements:
-    // TODO Should really get this from java_bytecode_language somehow, but we
-    // don't have an instance of that here.
-    object_factory_parameterst factory_params;
-    factory_params.max_nondet_array_length=
-      cmdline.isset("java-max-input-array-length")
-      ? std::stoul(cmdline.get_value("java-max-input-array-length"))
-      : MAX_NONDET_ARRAY_LENGTH_DEFAULT;
-    factory_params.max_nondet_string_length=
-      cmdline.isset("string-max-input-length")
-      ? std::stoul(cmdline.get_value("string-max-input-length"))
-      : MAX_NONDET_STRING_LENGTH;
-    factory_params.max_nondet_tree_depth=
-      cmdline.isset("java-max-input-tree-depth")
-      ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
-      : MAX_NONDET_TREE_DEPTH;
-
     convert_nondet(
-      function,
-      get_message_handler(),
-      factory_params);
-#endif
+      function, get_message_handler(), object_factory_params, ID_java);
 
     adjust_float_expressions(goto_function, namespacet(symbol_table));
 
@@ -657,12 +636,12 @@ bool sec_driver_parse_optionst::generate_function_body(
 {
   // Provide a simple stub implementation for any function we don't have a
   // bytecode implementation for:
-
-  if(body_available)
-    return false;
-
-  if(!can_generate_function_body(function_name))
-    return false;
+  if(body_available || !can_generate_function_body(function_name))
+  {
+    const symbolt *symbol = symbol_table.lookup(function_name);
+    if(symbol == nullptr || !symbol->type.get_bool(ID_C_abstract))
+      return false;
+  }
 
   if(symbol_table.lookup_ref(function_name).mode == ID_java)
   {

src/taint-analysis/taint_program.h

@@ -21,11 +21,6 @@
 
 typedef goto_programt::instructiont::const_targett instruction_iteratort;
 
-typedef std::unordered_map<
-  instruction_iteratort,
-  symbol_exprt,
-  instruction_iterator_hashert> replacements_of_NONDET_retvalst;
-
 class taint_statisticst;
 
 

src/taint-slicer/slicing_tasks_builder.cpp

@@ -326,6 +326,22 @@ std::pair<taint_slicing_taskt,std::string> build_slicing_task(
           I.function=fname_prog.first;
         }
 
+    // Check that the goto program to be saved does not contain any NONDET(T*)
+    // expressions. However, non-pointer NONDET expressions can be present.
+    class nondet_visitort : public const_expr_visitort
+    {
+    public:
+      void operator()(const exprt &expr) override
+      {
+        INVARIANT(
+          expr.id() != ID_nondet || expr.type().id() != ID_pointer,
+          "No pointer-typed NONDET allowed.");
+      }
+    } visitor;
+    for(auto &fname_prog : goto_functions.function_map)
+      for(const auto &I : fname_prog.second.body.instructions)
+        I.code.visit(visitor);
+
     // Finally save the constructed slicing task on the disc as GOTO program
     // binary.
     const bool fail=write_goto_binary(