added generation of havoc functions from assigns clauses

Author: Remi Delmas

src/goto-instrument/contracts/dfcc.cpp

@@ -348,7 +348,7 @@ void dfcct::transform_goto_model(
   }
 
   goto_model.goto_functions.update();
-  library.specialize_functions(max_assigns_clause_size);
+  library.specialize(max_assigns_clause_size);
   utils.create_initialize_function();
 }
 

src/goto-instrument/contracts/dfcc_contract_handler.h

@@ -19,14 +19,25 @@ class goto_programt;
 class dfcc_contract_handlert
 {
 public:
-  /// Adds instruction modeling contract checking to dest
+  /// Adds instruction modeling contract checking to dest.
+  /// \param wrapped_id name of the wrapped function that is being checked
+  /// \param wrapper_id name of the wrapper function for which the instructions
+  /// are generated
+  /// \param contract_id name of the contract to check
+  /// \param dest destination program where instructions are added
   virtual void add_contract_checking_instructions(
     const irep_idt &wrapped_id,
     const irep_idt &wrapper_id,
     const irep_idt &contract_id,
     goto_programt &dest) = 0;
 
-  /// Adds instruction modeling contract replacement to dest
+  /// Adds instruction modeling contract replacement to dest.
+  /// \param wrapper_id name of the wrapper function for which the instructions
+  /// are generated
+  /// \param contract_id name of the contract to check
+  /// \param wrapper_write_set_symbol symbol of the write set against which
+  /// to check the contract's write set for inclusion
+  /// \param dest destination program where instructions are added
   virtual void add_contract_replacement_instructions(
     const irep_idt &wrapper_id,
     const irep_idt &contract_id,

src/goto-instrument/contracts/dfcc_library.cpp

@@ -33,7 +33,7 @@ dfcc_libraryt::dfcc_libraryt(
 {
 }
 
-/// Enum to type name mapping
+/// enum to type name mapping
 static const std::map<dfcc_typet, irep_idt> dfcc_type_name = {
   {dfcc_typet::FREEABLE, CPROVER_PREFIX "freeable_t"},
   {dfcc_typet::ASSIGNABLE, CPROVER_PREFIX "assignable_t"},
@@ -45,7 +45,7 @@ static const std::map<dfcc_typet, irep_idt> dfcc_type_name = {
   {dfcc_typet::SET, CPROVER_PREFIX "assignable_set_t"},
   {dfcc_typet::SET_PTR, CPROVER_PREFIX "assignable_set_ptr_t"}};
 
-/// Enum to function name mapping
+/// enum to function name mapping
 static const std::map<dfcc_funt, irep_idt> dfcc_fun_name = {
   {dfcc_funt::CAR_CREATE, CPROVER_PREFIX "assignable_car_create"},
   {dfcc_funt::CAR_SET_CREATE, CPROVER_PREFIX "assignable_car_set_create"},
@@ -92,9 +92,17 @@ static const std::map<dfcc_funt, irep_idt> dfcc_fun_name = {
   {dfcc_funt::SET_CHECK_FREES_CLAUSE_INCLUSION,
    CPROVER_PREFIX "assignable_set_check_frees_clause_inclusion"},
   {dfcc_funt::SET_DEALLOCATE_FREEABLE,
-   CPROVER_PREFIX "assignable_set_deallocate_freeable"}};
-
-/// Built-in function name to enum to use for instrumentation
+   CPROVER_PREFIX "assignable_set_deallocate_freeable"},
+  {dfcc_funt::SET_HAVOC_GET_ASSIGNABLE_TARGET,
+   CPROVER_PREFIX "assignable_set_havoc_get_assignable_target"},
+  {dfcc_funt::SET_HAVOC_WHOLE_OBJECT,
+   CPROVER_PREFIX "assignable_set_havoc_whole_object"},
+  {dfcc_funt::SET_HAVOC_OBJECT_FROM,
+   CPROVER_PREFIX "assignable_set_havoc_object_from"},
+  {dfcc_funt::SET_HAVOC_OBJECT_UPTO,
+   CPROVER_PREFIX "assignable_set_havoc_object_upto"}};
+
+/// built-in function name to enum to use for instrumentation
 static const std::map<irep_idt, dfcc_funt> dfcc_hook = {
   {CPROVER_PREFIX "assignable", dfcc_funt::SET_INSERT_ASSIGNABLE},
   {CPROVER_PREFIX "whole_object", dfcc_funt::SET_INSERT_WHOLE_OBJECT},
@@ -111,7 +119,23 @@ optionalt<dfcc_funt> dfcc_libraryt::get_hook(const irep_idt &function_id) const
     return {};
 }
 
-/// Built-in function names (front-end and instrumentation hooks)
+static const std::map<irep_idt, dfcc_funt> havoc_hook = {
+  {CPROVER_PREFIX "assignable", dfcc_funt::SET_HAVOC_GET_ASSIGNABLE_TARGET},
+  {CPROVER_PREFIX "whole_object", dfcc_funt::SET_HAVOC_WHOLE_OBJECT},
+  {CPROVER_PREFIX "object_from", dfcc_funt::SET_HAVOC_OBJECT_FROM},
+  {CPROVER_PREFIX "object_upto", dfcc_funt::SET_HAVOC_OBJECT_UPTO}};
+
+optionalt<dfcc_funt>
+dfcc_libraryt::get_havoc_hook(const irep_idt &function_id) const
+{
+  auto found = havoc_hook.find(function_id);
+  if(found != havoc_hook.end())
+    return {found->second};
+  else
+    return {};
+}
+
+/// built-in function names (front-end and instrumentation hooks)
 static const std::set<irep_idt> assignable_builtin_names = {
   CPROVER_PREFIX "assignable",
   CPROVER_PREFIX "assignable_set_insert_assignable",
@@ -144,7 +168,7 @@ void dfcc_libraryt::get_missing_funs(std::set<irep_idt> &missing)
   }
 }
 
-// true iff library symbols have been loaded
+// true iff library symbols have already been loaded
 static bool loaded = false;
 
 void dfcc_libraryt::load()
@@ -198,7 +222,6 @@ void dfcc_libraryt::load()
       throw 0;
     }
     dfcc_fun_symbol[pair.first] = ns.lookup(pair.second);
-    //dfcc_fun_symbol_expr[pair.first] = ns.lookup(pair.second).symbol_expr();
   }
 
   // populate symbol maps for easy access to symbols during translation
@@ -221,7 +244,7 @@ bool dfcc_libraryt::is_special_builtin(const irep_idt &id) const
   return special_builtins.find(id) != special_builtins.end();
 }
 
-/// Set of functions that need to be inlined for specialisation
+/// set of functions that need to be inlined for specialisation
 static const std::set<dfcc_funt> to_inline = {
   dfcc_funt::SET_CREATE,
   dfcc_funt::SET_INSERT_ASSIGNABLE,
@@ -242,7 +265,9 @@ static const std::set<dfcc_funt> to_inline = {
   dfcc_funt::SET_CHECK_FREES_CLAUSE_INCLUSION,
   dfcc_funt::SET_DEALLOCATE_FREEABLE};
 
+/// true iff the library functions have already been inlined
 static bool inlined = false;
+
 void dfcc_libraryt::inline_functions()
 {
   INVARIANT(!inlined, "inlined_functions can only be called once");
@@ -253,7 +278,7 @@ void dfcc_libraryt::inline_functions()
   }
 }
 
-/// Set of functions that need to be unwound to assigns clause size with
+/// set of functions that need to be unwound to assigns clause size with
 /// corresponding loop labels.
 static const std::map<dfcc_funt, irep_idt> to_unwind = {
   {dfcc_funt::SET_REMOVE_DEALLOCATED, "CAR_SET_REMOVE_LOOP"},
@@ -266,7 +291,7 @@ static const std::map<dfcc_funt, irep_idt> to_unwind = {
 /// true iff the library functions have already been specialized
 static bool specialized = false;
 
-void dfcc_libraryt::specialize_functions(const int contract_assigns_size_hint)
+void dfcc_libraryt::specialize(const int contract_assigns_size_hint)
 {
   INVARIANT(
     !specialized,

src/goto-instrument/contracts/dfcc_library.h

@@ -12,9 +12,13 @@ Author: Remi Delmas, delmasrd@amazon.com
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DFCC_LIBRARY_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DFCC_LIBRARY_H
 
+#include <util/irep.h>
 #include <util/optional.h>
 
-/// Library types used in the instrumentation
+#include <map>
+#include <set>
+
+/// One enum value per type defined by the `cprover_dfcc.c` library file.
 enum class dfcc_typet
 {
   FREEABLE,
@@ -28,7 +32,7 @@ enum class dfcc_typet
   SET_PTR
 };
 
-/// Library functions used in the instrumentation
+/// One enum value per function defined by the `cprover_dfcc.c` library file.
 enum class dfcc_funt
 {
   CAR_CREATE,
@@ -60,7 +64,11 @@ enum class dfcc_funt
   SET_CHECK_DEALLOCATE,
   SET_CHECK_ASSIGNS_CLAUSE_INCLUSION,
   SET_CHECK_FREES_CLAUSE_INCLUSION,
-  SET_DEALLOCATE_FREEABLE
+  SET_DEALLOCATE_FREEABLE,
+  SET_HAVOC_GET_ASSIGNABLE_TARGET,
+  SET_HAVOC_WHOLE_OBJECT,
+  SET_HAVOC_OBJECT_FROM,
+  SET_HAVOC_OBJECT_UPTO
 };
 
 class goto_modelt;
@@ -72,13 +80,8 @@ class symbol_exprt;
 class typet;
 class dfcc_utilst;
 
-#include <util/irep.h>
-
-#include <map>
-#include <set>
-
-/// A programmatic interface to library types and functions
-/// defined in `src/ansi-c/library/cprover_dfcc.c`.
+/// Programmatic interface to library types and functions defined in
+/// `cprover_dfcc.c`.
 class dfcc_libraryt
 {
 public:
@@ -90,52 +93,45 @@ class dfcc_libraryt
   messaget &log;
   message_handlert &message_handler;
 
-  /// Collects the names of all currently missing dfcc functions
-  /// in the goto_model
+  /// Collects the names of all library functions currently missing from the
+  /// goto_model into missing.
   void get_missing_funs(std::set<irep_idt> &missing);
 
+  /// Inlines library functions that need to be inlined before use
+  void inline_functions();
+
 public:
-  /// enum-to-typet mapping (dynamically loaded)
+  /// Maps enum values to the actual types (dynamically loaded)
   std::map<dfcc_typet, typet> dfcc_type;
 
-  /// enum-to-symbol mapping (dynamically loaded)
+  /// Maps enum values to the actual function symbols (dynamically loaded)
   std::map<dfcc_funt, symbolt> dfcc_fun_symbol;
 
-  /// enum-to-symbol_exprt mapping (dynamically loaded)
-  std::map<dfcc_funt, symbol_exprt> dfcc_fun_symbol_expr;
-
-  /// Adds all the `cprover_dfcc.c` library types and functions to the model
+  /// After calling this function, all library types and functions are present
+  /// in the the goto_model.
   void load();
 
   /// True iff the id starts with CPROVER_PREFIX
-  /// that we do not want to instrument
   bool is_cprover_symbol(const irep_idt &id) const;
 
-  /// True iff the id is one of the special builtins
-  /// that we do not want to instrument
+  /// True iff the id is one of the special builtins that musnt be instrumented
   bool is_special_builtin(const irep_idt &id) const;
 
-  /// Inlines library functions as specified in the `inline_and_unwind` map.
-  void inline_functions();
+  /// Specializes the library by unwinding loops in library functions
+  /// to the given assigns clause size.
+  /// \param contract_assigns_size_hint size of the assigns clause being checked
+  void specialize(const int contract_assigns_size_hint);
 
-  /// Specialises the library function code to a specific contract
-  /// by inlining and unwinding loops in library functions that require it,
-  /// based on the given size hints for the assigns clause and the frees clause
-  /// of the checked contract.
-  void unwind_functions(const int assigns_size_hint, const int frees_size_hint);
-
-  /// Specialises the library function code to a specific contract unwinding
-  /// loops in library functions using the given hint for assigns clause size.
-  /// \param contract_assigns_size_hint assigns clause size to unwind to
-  /// \param continue_as_loops value of the goto-instrument command line switch
-  /// (to detect incompatibility with unwind assertions)
-  void specialize_functions(const int contract_assigns_size_hint);
-
-  /// returns the library instrumentation hook for the given built-in
-  /// function_id must be one of
-  /// {__CPROVER_assignable, __CPROVER_whole_object, __CPROVER_object_from,
-  /// __CPROVER_object_upto, __CPROVER_freeable }
+  /// Returns the library instrumentation hook for the given built-in.
+  /// function_id must be one of `__CPROVER_assignable`,
+  /// `__CPROVER_whole_object`, `__CPROVER_object_from`,
+  /// `__CPROVER_object_upto`, `__CPROVER_freeable`
   optionalt<dfcc_funt> get_hook(const irep_idt &function_id) const;
+
+  /// Returns the library instrumentation hook for the given built-in.
+  /// function_id must be one of `__CPROVER_assignable`,
+  /// `__CPROVER_whole_object`, `__CPROVER_object_from`, `__CPROVER_object_upto`
+  optionalt<dfcc_funt> get_havoc_hook(const irep_idt &function_id) const;
 };
 
 #endif