Merge pull request #5411 from polgreen/havoc_undefined_functions

Havoc undefined functions during symbolic execution

Author: kroening

regression/cbmc/havoc_undefined_functions/main.c

@@ -0,0 +1,9 @@
+void function(int *a);
+
+int main()
+{
+  int a = 0;
+  function(&a);
+  __CPROVER_assert(a == 0, "");
+  return 0;
+}

regression/cbmc/havoc_undefined_functions/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--havoc-undefined-functions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

src/cbmc/cbmc_parse_options.cpp

@@ -240,6 +240,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("drop-unused-functions"))
     options.set_option("drop-unused-functions", true);
 
+  if(cmdline.isset("havoc-undefined-functions"))
+    options.set_option("havoc-undefined-functions", true);
+
   if(cmdline.isset("string-abstraction"))
     options.set_option("string-abstraction", true);
 
@@ -1082,6 +1085,9 @@ void cbmc_parse_optionst::help()
     HELP_REACHABILITY_SLICER_FB
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
+    " --havoc-undefined-functions\n"
+    "                              for any function that has no body, assign non-deterministic values to\n" // NOLINT(*)
+    "                              any parameters passed as non-const pointers and the return value\n" // NOLINT(*)
     "\n"
     "Semantic transformations:\n"
     // NOLINTNEXTLINE(whitespace/line_length)

src/cbmc/cbmc_parse_options.h

@@ -67,6 +67,7 @@ class optionst;
   OPT_SHOW_PROPERTIES \
   "(show-symbol-table)(show-parse-tree)" \
   "(drop-unused-functions)" \
+  "(havoc-undefined-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \

src/goto-checker/symex_bmc.cpp

@@ -33,6 +33,8 @@ symex_bmct::symex_bmct(
       path_storage,
       guard_manager),
     record_coverage(!options.get_option("symex-coverage-report").empty()),
+    havoc_bodyless_functions(
+      options.get_bool_option("havoc-undefined-functions")),
     symex_coverage(ns)
 {
 }
@@ -210,7 +212,13 @@ void symex_bmct::no_body(const irep_idt &identifier)
 {
   if(body_warnings.insert(identifier).second)
   {
-    log.warning() << "**** WARNING: no body for function " << identifier
-                  << log.eom;
+    log.warning() << "**** WARNING: no body for function " << identifier;
+
+    if(havoc_bodyless_functions)
+    {
+      log.warning()
+        << "; assigning non-deterministic values to any pointer arguments";
+    }
+    log.warning() << log.eom;
   }
 }

src/goto-checker/symex_bmc.h

@@ -81,6 +81,7 @@ class symex_bmct : public goto_symext
   }
 
   const bool record_coverage;
+  const bool havoc_bodyless_functions;
 
   unwindsett unwindset;
 

src/goto-symex/symex_config.h

@@ -34,6 +34,8 @@ struct symex_configt final
 
   bool partial_loops;
 
+  bool havoc_undefined_functions;
+
   mp_integer debug_level;
 
   /// \brief Should the additional validation checks be run?

src/goto-symex/symex_function_call.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
+#include <analyses/guard_expr.h>
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
@@ -293,6 +294,25 @@ void goto_symext::symex_function_call_code(
       symex_assign(state, code);
     }
 
+    if(symex_config.havoc_undefined_functions)
+    {
+      // assign non det to function arguments if pointers
+      // are not const
+      for(const auto &arg : call.arguments())
+      {
+        if(
+          arg.type().id() == ID_pointer &&
+          !arg.type().subtype().get_bool(ID_C_constant) &&
+          arg.type().subtype().id() != ID_code)
+        {
+          exprt object = dereference_exprt(arg, arg.type().subtype());
+          exprt cleaned_object = clean_expr(object, state, true);
+          const guardt guard(true_exprt(), state.guard_manager);
+          havoc_rec(state, guard, cleaned_object);
+        }
+      }
+    }
+
     symex_transition(state);
     return;
   }

src/goto-symex/symex_main.cpp

@@ -42,6 +42,8 @@ symex_configt::symex_configt(const optionst &options)
     simplify_opt(options.get_bool_option("simplify")),
     unwinding_assertions(options.get_bool_option("unwinding-assertions")),
     partial_loops(options.get_bool_option("partial-loops")),
+    havoc_undefined_functions(
+      options.get_bool_option("havoc-undefined-functions")),
     debug_level(unsafe_string2int(options.get_option("debug-level"))),
     run_validation_checks(options.get_bool_option("validate-ssa-equation")),
     show_symex_steps(options.get_bool_option("show-goto-symex-steps")),