Add "make invalid pointer" utility function and havoc mode

Operates in two sub-modes, controlled by
CLI switch `--dfcc-simple-invalid-pointer-model`

Author: Remi Delmas

Diff for: doc/man/cbmc.1

@@ -337,6 +337,10 @@ track C string lengths and zero\-termination
 \fB\-\-dfcc\-debug\-lib\fR
 enable debug assertions in the cprover contracts library
 .TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
+.TP
 \fB\-\-reachability\-slice\fR
 remove instructions that cannot appear on a trace
 from entry point to a property

Diff for: doc/man/goto-analyzer.1

@@ -588,6 +588,10 @@ track C string lengths and zero\-termination
 .TP
 \fB\-\-dfcc\-debug\-lib\fR
 enable debug assertions in the cprover contracts library
+.TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
 .SS "Standard Checks"
 From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
 apply some checks to the program by default (called the "standard checks"), with the

Diff for: doc/man/goto-instrument.1

@@ -709,6 +709,10 @@ track C string lengths and zero\-termination
 \fB\-\-dfcc\-debug\-lib\fR
 enable debug assertions in the cprover contracts library
 .TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
+.TP
 \fB\-\-model\-argc\-argv\fR \fIn\fR
 Create up to \fIn\fR non-deterministic C strings as entries to \fIargv\fR and
 set \fIargc\fR accordingly. In absence of such modelling, \fIargv\fR is left

Diff for: src/ansi-c/cprover_library.cpp

@@ -48,6 +48,10 @@ static std::string get_cprover_library_text(
   if(config.ansi_c.dfcc_debug_lib)
     library_text << "#define " CPROVER_PREFIX "DFCC_DEBUG_LIB\n";
 
+  if(config.ansi_c.simple_invalid_pointer_model)
+    library_text << "#define " CPROVER_PREFIX
+                    "DFCC_SIMPLE_INVALID_POINTER_MODEL\n";
+
   // cprover_library.inc may not have been generated when running Doxygen, thus
   // make Doxygen skip this part
   /// \cond

Diff for: src/ansi-c/library/cprover_contracts.c

@@ -1136,6 +1136,33 @@ void *__CPROVER_contracts_malloc(
   __CPROVER_size_t,
   __CPROVER_contracts_write_set_ptr_t);
 
+/// \brief Makes the given pointer invalid.
+///
+/// Used to craft invalid pointers when pointer predicates return false
+/// in "assume" mode.
+/// We have two models for invalid pointers:
+/// - default: pointer is uninitialized (empty value set, nondet bit pattern).
+/// - simple: pointer is either null or pointing to a dead object of size zero.
+/// The simple model is activated by a CLI switch in goto-instrument.
+void __CPROVER_contracts_make_invalid_pointer(void **ptr)
+{
+#ifdef __CPROVER_DFCC_SIMPLE_INVALID_POINTER_MODEL
+  void *dummy = __CPROVER_allocate(0, 0);
+  __CPROVER_deallocated =
+    __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated;
+  *ptr = __VERIFIER_nondet___CPROVER_bool() ? dummy : (void *)0;
+#else
+#  pragma GCC diagnostic push
+#  pragma GCC diagnostic ignored "-Wuninitialized"
+  // We have to silence this warning to be able to generate and use an
+  // invalid pointer.
+  void *invalid;
+  *ptr = invalid;
+#  pragma GCC diagnostic pop
+#endif
+}
+
+
 /// \brief Implementation of the `is_fresh` front-end predicate.
 ///
 /// The behaviour depends on the boolean flags carried by \p set

Diff for: src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

@@ -121,6 +121,7 @@ void dfcc_instrument_loopt::operator()(
     function_id,
     write_set_populate_instrs,
     loop.addr_of_write_set_var,
+    dfcc_ptr_havoc_modet::NONDET,
     havoc_instrs,
     nof_targets);
   spec_functions.to_spec_assigns_instructions(

Diff for: src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp

@@ -103,6 +103,7 @@ void dfcc_spec_functionst::generate_havoc_function(
     havoc_function_id,
     original_program,
     write_set_symbol.symbol_expr(),
+    dfcc_ptr_havoc_modet::INVALID,
     havoc_program,
     nof_targets);
 
@@ -144,6 +145,7 @@ void dfcc_spec_functionst::generate_havoc_instructions(
   const irep_idt &function_id,
   const goto_programt &original_program,
   const exprt &write_set_to_havoc,
+  dfcc_ptr_havoc_modet ptr_havoc_mode,
   goto_programt &havoc_program,
   std::size_t &nof_targets)
 {
@@ -191,8 +193,9 @@ void dfcc_spec_functionst::generate_havoc_instructions(
         // DECL __havoc_target;
         // CALL __havoc_target = havoc_hook(set, next_idx);
         // IF !__havoc_target GOTO label;
-        // ASSIGN *__havoc_target = nondet(target_type);
-        // label: DEAD __havoc_target;
+        // .... add code for scalar or pointer targets ...
+        // label:
+        //   DEAD __havoc_target;
         // ```
         // declare a local var to store targets havoced via nondet assignment
         auto &target_type = get_target_type(ins_it->call_arguments().at(0));
@@ -213,13 +216,42 @@ void dfcc_spec_functionst::generate_havoc_instructions(
           havoc_program.add(goto_programt::make_incomplete_goto(
             dfcc_utilst::make_null_check_expr(target_expr), location));
 
-        // create nondet assignment to the target
-        side_effect_expr_nondett nondet(target_type, location);
-        havoc_program.add(goto_programt::make_assignment(
-          dereference_exprt{typecast_exprt::conditional_cast(
-            target_expr, pointer_type(target_type))},
-          nondet,
-          location));
+        if(
+          ptr_havoc_mode == dfcc_ptr_havoc_modet::INVALID &&
+          target_type.id() == ID_pointer)
+        {
+          // ```
+          // DECL *__invalid_ptr;
+          // ASSIGN *__havoc_target = __invalid_ptr;
+          // DEAD __invalid_ptr;
+          // ```
+          const auto invalid_ptr_expr = dfcc_utilst::create_symbol(
+            goto_model.symbol_table,
+            target_type,
+            function_id,
+            "__invalid_ptr",
+            location);
+
+          havoc_program.add(goto_programt::make_assignment(
+            dereference_exprt{typecast_exprt::conditional_cast(
+              target_expr, pointer_type(target_type))},
+            invalid_ptr_expr,
+            location));
+          havoc_program.add(
+            goto_programt::make_dead(invalid_ptr_expr, location));
+        }
+        else
+        {
+          // ```
+          // ASSIGN *__havoc_target = nondet(target_type);
+          // ```
+          side_effect_expr_nondett nondet(target_type, location);
+          havoc_program.add(goto_programt::make_assignment(
+            dereference_exprt{typecast_exprt::conditional_cast(
+              target_expr, pointer_type(target_type))},
+            nondet,
+            location));
+        }
         auto label =
           havoc_program.add(goto_programt::make_dead(target_expr, location));
         goto_instruction->complete_goto(label);

Diff for: src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h

@@ -32,6 +32,19 @@ class message_handlert;
 class symbolt;
 class conditional_target_group_exprt;
 
+/// \brief Represents the different ways to havoc pointers.
+///
+/// Remark:
+/// - Function contracts use invalid
+/// - Loop contracts use nondet
+enum class dfcc_ptr_havoc_modet
+{
+  /// havocs the pointer to an invalid pointer
+  INVALID,
+  /// havocs the pointer to an nondet pointer
+  NONDET
+};
+
 /// This class rewrites GOTO functions that use the built-ins:
 /// - `__CPROVER_assignable`,
 /// - `__CPROVER_object_whole`,
@@ -48,6 +61,9 @@ class dfcc_spec_functionst
     message_handlert &message_handler,
     dfcc_libraryt &library);
 
+  /// Generates the havoc function for a function contract.
+  /// Pointer-typed targets are turned into invalid pointers by the havoc.
+  ///
   /// From a function:
   ///
   /// ```
@@ -62,10 +78,9 @@ class dfcc_spec_functionst
   ///
   /// Which havocs the targets specified by `function_id`, passed
   ///
-  /// \param function_id function to generate instructions from
-  /// \param havoc_function_id write set variable to havoc
-  /// \param nof_targets maximum number of targets to havoc
-  ///
+  /// \param[in] function_id function to generate instructions from
+  /// \param[in] havoc_function_id write set variable to havoc
+  /// \param[out] nof_targets maximum number of targets to havoc
   void generate_havoc_function(
     const irep_idt &function_id,
     const irep_idt &havoc_function_id,
@@ -89,13 +104,14 @@ class dfcc_spec_functionst
   /// \param[in] function_id function id to use for prefixing fresh variables
   /// \param[in] original_program program from which to derive the havoc program
   /// \param[in] write_set_to_havoc write set symbol to havoc
+  /// \param[in] ptr_havoc_mode havocing mode for pointers
   /// \param[out] havoc_program destination program for havoc instructions
   /// \param[out] nof_targets max number of havoc targets discovered
-  ///
   void generate_havoc_instructions(
     const irep_idt &function_id,
     const goto_programt &original_program,
     const exprt &write_set_to_havoc,
+    dfcc_ptr_havoc_modet ptr_havoc_mode,
     goto_programt &havoc_program,
     std::size_t &nof_targets);
 

Diff for: src/util/config.cpp

@@ -1169,6 +1169,11 @@ bool configt::set(const cmdlinet &cmdline)
   else
     ansi_c.dfcc_debug_lib = false;
 
+  if(cmdline.isset("dfcc-simple-invalid-pointer-model"))
+    ansi_c.simple_invalid_pointer_model = true;
+  else
+    ansi_c.simple_invalid_pointer_model = false;
+
   if(cmdline.isset("no-library"))
     ansi_c.lib=configt::ansi_ct::libt::LIB_NONE;
 

Diff for: src/util/config.h

@@ -73,7 +73,8 @@ class symbol_table_baset;
   "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)"                    \
   "(no-malloc-may-fail)"                                                       \
   "(string-abstraction)"                                                       \
-  "(dfcc-debug-lib)"
+  "(dfcc-debug-lib)"                                                           \
+  "(dfcc-simple-invalid-pointer-model)"
 
 #define HELP_CONFIG_LIBRARY                                                    \
   " {y--malloc-may-fail} \t allow malloc calls to return a null pointer\n"     \
@@ -83,7 +84,9 @@ class symbol_table_baset;
   " {y--malloc-fail-null} \t set malloc failure mode to return null\n"         \
   " {y--string-abstraction} \t track C string lengths and zero-termination\n"  \
   " {y--dfcc-debug-lib} \t enable debug assertions in the cprover contracts "  \
-  "library\n"
+  "library\n"                                                                  \
+  " {y--dfcc-simple-invalid-pointer-model} \t use simplified invalid pointer " \
+  "model in the cprover contracts library (faster, unsound)\n"
 
 #define OPT_CONFIG_JAVA "(classpath)(cp)(main-class)"
 
@@ -288,6 +291,8 @@ class configt
     /// enable debug code in cprover_contracts library
     bool dfcc_debug_lib = false;
 
+    /// use simplified invalid pointer model in cprover_contracts library
+    bool simple_invalid_pointer_model = false;
 
     enum malloc_failure_modet
     {