From a7afbe2460f4ea4e877faf47b1cd879e800c52f7 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Sat, 22 Jun 2024 02:00:33 -0500 Subject: [PATCH] Use unified loop contract config --- src/goto-instrument/Makefile | 1 - src/goto-instrument/contracts/contracts.cpp | 2 +- src/goto-instrument/contracts/contracts.h | 16 ++++-- .../contracts/dynamic-frames/dfcc.cpp | 45 +++------------ .../contracts/dynamic-frames/dfcc.h | 47 ++-------------- .../dynamic-frames/dfcc_cfg_info.cpp | 4 +- .../contracts/dynamic-frames/dfcc_cfg_info.h | 4 +- .../dfcc_contract_functions.cpp | 4 +- .../dynamic-frames/dfcc_instrument.cpp | 28 +++++----- .../dynamic-frames/dfcc_instrument.h | 19 ++++--- .../dfcc_lift_memory_predicates.cpp | 2 +- .../dfcc_loop_contract_mode.cpp | 55 ------------------- .../dynamic-frames/dfcc_loop_contract_mode.h | 37 ------------- .../dynamic-frames/dfcc_spec_functions.cpp | 1 - .../dynamic-frames/dfcc_swap_and_wrap.cpp | 21 ++++--- .../dynamic-frames/dfcc_swap_and_wrap.h | 13 ++--- .../contracts/loop_contract_config.h | 55 +++++++++++++++++++ .../goto_instrument_parse_options.cpp | 55 ++++++++----------- src/goto-synthesizer/cegis_verifier.cpp | 4 +- .../goto_synthesizer_parse_options.cpp | 9 ++- 20 files changed, 157 insertions(+), 265 deletions(-) delete mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_loop_contract_mode.cpp delete mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_loop_contract_mode.h create mode 100644 src/goto-instrument/contracts/loop_contract_config.h diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 300e8f74047..dfacdd636ee 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -21,7 +21,6 @@ SRC = accelerate/accelerate.cpp \ contracts/dynamic-frames/dfcc_utils.cpp \ contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp \ contracts/dynamic-frames/dfcc_contract_mode.cpp \ - contracts/dynamic-frames/dfcc_loop_contract_mode.cpp \ contracts/dynamic-frames/dfcc_loop_tags.cpp \ contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp \ contracts/dynamic-frames/dfcc_root_object.cpp \ diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index f637527cebb..36eff629528 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -1500,7 +1500,7 @@ void code_contractst::apply_loop_contracts( nondet_static(goto_model, to_exclude_from_nondet_init); // unwind all transformed loops twice. - if(unwind_transformed_loops) + if(loop_contract_config.unwind_transformed_loops) { unwindsett unwindset{goto_model}; unwindset.parse_unwindset(loop_names, log.get_message_handler()); diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index aa2fb905d45..8e6fe670dd3 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -22,6 +22,8 @@ Date: February 2016 #include +#include "loop_contract_config.h" + #include #include #include @@ -55,12 +57,16 @@ class local_may_aliast; class code_contractst { public: - code_contractst(goto_modelt &goto_model, messaget &log) + code_contractst( + goto_modelt &goto_model, + messaget &log, + const loop_contract_configt &loop_contract_config) : ns(goto_model.symbol_table), goto_model(goto_model), symbol_table(goto_model.symbol_table), goto_functions(goto_model.goto_functions), - log(log) + log(log), + loop_contract_config(loop_contract_config) { } @@ -138,9 +144,6 @@ class code_contractst namespacet ns; - // Unwind transformed loops after applying loop contracts or not. - bool unwind_transformed_loops = true; - protected: goto_modelt &goto_model; symbol_tablet &symbol_table; @@ -164,6 +167,9 @@ class code_contractst std::unordered_set loop_havoc_set; + // Loop contract configuration + loop_contract_configt loop_contract_config; + public: /// \brief Enforce contract of a single function void enforce_contract(const irep_idt &function); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index 0e420e372c7..e921eb88dc7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -119,8 +119,7 @@ void dfcc( const std::optional &to_check, const bool allow_recursive_calls, const std::set &to_replace, - const bool apply_loop_contracts, - const bool unwind_transformed_loops, + const loop_contract_configt loop_contract_config, const std::set &to_exclude_from_nondet_static, message_handlert &message_handler) { @@ -128,7 +127,7 @@ void dfcc( for(const auto &cli_flag : to_replace) to_replace_map.insert(parse_function_contract_pair(cli_flag)); - dfcc( + dfcct( options, goto_model, harness_id, @@ -136,35 +135,9 @@ void dfcc( : std::optional>{}, allow_recursive_calls, to_replace_map, - apply_loop_contracts, - unwind_transformed_loops, - to_exclude_from_nondet_static, - message_handler); -} - -void dfcc( - const optionst &options, - goto_modelt &goto_model, - const irep_idt &harness_id, - const std::optional> &to_check, - const bool allow_recursive_calls, - const std::map &to_replace, - const bool apply_loop_contracts, - const bool unwind_transformed_loops, - const std::set &to_exclude_from_nondet_static, - message_handlert &message_handler) -{ - dfcct{ - options, - goto_model, - harness_id, - to_check, - allow_recursive_calls, - to_replace, - dfcc_loop_contract_mode_from_bools( - apply_loop_contracts, unwind_transformed_loops), + loop_contract_config, message_handler, - to_exclude_from_nondet_static}; + to_exclude_from_nondet_static); } dfcct::dfcct( @@ -174,7 +147,7 @@ dfcct::dfcct( const std::optional> &to_check, const bool allow_recursive_calls, const std::map &to_replace, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt loop_contract_config, message_handlert &message_handler, const std::set &to_exclude_from_nondet_static) : options(options), @@ -183,7 +156,7 @@ dfcct::dfcct( to_check(to_check), allow_recursive_calls(allow_recursive_calls), to_replace(to_replace), - loop_contract_mode(loop_contract_mode), + loop_contract_config(loop_contract_config), to_exclude_from_nondet_static(to_exclude_from_nondet_static), message_handler(message_handler), log(message_handler), @@ -339,7 +312,7 @@ void dfcct::instrument_harness_function() << messaget::eom; instrument.instrument_harness_function( - harness_id, loop_contract_mode, function_pointer_contracts); + harness_id, loop_contract_config, function_pointer_contracts); other_symbols.erase(harness_id); } @@ -368,7 +341,7 @@ void dfcct::wrap_checked_function() << contract_id << "' in CHECK mode" << messaget::eom; swap_and_wrap.swap_and_wrap_check( - loop_contract_mode, + loop_contract_config, wrapper_id, contract_id, function_pointer_contracts, @@ -486,7 +459,7 @@ void dfcct::instrument_other_functions() log.status() << "Instrumenting '" << function_id << "'" << messaget::eom; instrument.instrument_function( - function_id, loop_contract_mode, function_pointer_contracts); + function_id, loop_contract_config, function_pointer_contracts); } goto_model.goto_functions.update(); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.h b/src/goto-instrument/contracts/dynamic-frames/dfcc.h index 247c70cf127..b385f9e0233 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.h @@ -38,7 +38,6 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_instrument.h" #include "dfcc_library.h" #include "dfcc_lift_memory_predicates.h" -#include "dfcc_loop_contract_mode.h" #include "dfcc_spec_functions.h" #include "dfcc_swap_and_wrap.h" @@ -96,9 +95,7 @@ class invalid_function_contract_pair_exceptiont : public cprover_exception_baset /// \param to_check function to check against its contract /// \param allow_recursive_calls Allow the checked function to be recursive /// \param to_replace set of functions to replace with their contract -/// \param apply_loop_contracts apply loop contract transformations iff true -/// \param unwind_transformed_loops unwind transformed loops after applying loop -/// contracts. +/// \param loop_contract_config configuration for applying loop contracts /// \param to_exclude_from_nondet_static set of symbols to exclude when havocing /// static program symbols. /// \param message_handler used for debug/warning/error messages @@ -109,41 +106,7 @@ void dfcc( const std::optional &to_check, const bool allow_recursive_calls, const std::set &to_replace, - const bool apply_loop_contracts, - const bool unwind_transformed_loops, - const std::set &to_exclude_from_nondet_static, - message_handlert &message_handler); - -/// \ingroup dfcc-module -/// \brief Applies function contracts and loop contracts transformation to GOTO -/// model, using the dynamic frame condition checking approach. -/// -/// Functions to check/replace are explicitly mapped to contracts. -/// When checking function `foo` against contract `bar`, we require the -/// actual contract symbol to exist as `contract::bar` in the symbol table. -/// -/// \param options CLI options (used to lookup options for language config when -/// re-defining the model's entry point) -/// \param goto_model GOTO model to transform -/// \param harness_id Proof harness name, must be the entry point of the model -/// \param to_check (function,contract) pair for contract checking -/// \param allow_recursive_calls Allow the checked function to be recursive -/// \param to_replace Functions-to-contract mapping for replacement -/// \param apply_loop_contracts Apply loop contract transformations iff true -/// \param unwind_transformed_loops unwind transformed loops after applying loop -/// contracts. -/// \param to_exclude_from_nondet_static Set of symbols to exclude when havocing -/// static program symbols. -/// \param message_handler used for debug/warning/error messages -void dfcc( - const optionst &options, - goto_modelt &goto_model, - const irep_idt &harness_id, - const std::optional> &to_check, - const bool allow_recursive_calls, - const std::map &to_replace, - const bool apply_loop_contracts, - const bool unwind_transformed_loops, + const loop_contract_configt loop_contract_config, const std::set &to_exclude_from_nondet_static, message_handlert &message_handler); @@ -160,7 +123,7 @@ class dfcct /// \param to_check (function,contract) pair for contract checking /// \param allow_recursive_calls Allow the checked function to be recursive /// \param to_replace functions-to-contract mapping for replacement - /// \param loop_contract_mode mode to use for loop contracts + /// \param loop_contract_config configuration for applying loop contracts /// \param message_handler used for debug/warning/error messages /// \param to_exclude_from_nondet_static set of symbols to exclude when dfcct( @@ -170,7 +133,7 @@ class dfcct const std::optional> &to_check, const bool allow_recursive_calls, const std::map &to_replace, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt loop_contract_config, message_handlert &message_handler, const std::set &to_exclude_from_nondet_static); @@ -207,7 +170,7 @@ class dfcct const std::optional> &to_check; const bool allow_recursive_calls; const std::map &to_replace; - const dfcc_loop_contract_modet loop_contract_mode; + const loop_contract_configt loop_contract_config; const std::set &to_exclude_from_nondet_static; message_handlert &message_handler; messaget log; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp index 69073bbc192..2aa5953ef38 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -506,7 +506,7 @@ dfcc_cfg_infot::dfcc_cfg_infot( const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, symbol_table_baset &symbol_table, message_handlert &message_handler, dfcc_libraryt &library) @@ -517,7 +517,7 @@ dfcc_cfg_infot::dfcc_cfg_infot( { dfcc_loop_nesting_grapht loop_nesting_graph; goto_programt &goto_program = goto_function.body; - if(loop_contract_mode != dfcc_loop_contract_modet::NONE) + if(loop_contract_config.apply_loop_contracts) { messaget log(message_handler); dfcc_check_loop_normal_form(goto_program, log); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h index 3cbd23551a6..ea4e819a5d2 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h @@ -23,7 +23,7 @@ Date: March 2023 #include -#include "dfcc_loop_contract_mode.h" +#include #include #include @@ -238,7 +238,7 @@ class dfcc_cfg_infot const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, symbol_table_baset &symbol_table, message_handlert &message_handler, dfcc_libraryt &library); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp index 33b4cec65db..d8bb7834432 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp @@ -80,9 +80,7 @@ void dfcc_contract_functionst:: { std::set function_pointer_contracts; instrument.instrument_function( - spec_function_id, - dfcc_loop_contract_modet::NONE, - function_pointer_contracts); + spec_function_id, loop_contract_configt{false}, function_pointer_contracts); INVARIANT( function_pointer_contracts.empty(), diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index 34e3f44a2b7..167961f4d76 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -237,7 +237,7 @@ bool dfcc_instrumentt::do_not_instrument(const irep_idt &id) const void dfcc_instrumentt::instrument_harness_function( const irep_idt &function_id, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, std::set &function_pointer_contracts) { // never instrument a function twice @@ -272,7 +272,7 @@ void dfcc_instrumentt::instrument_harness_function( goto_function, write_set, local_statics, - loop_contract_mode, + loop_contract_config, function_pointer_contracts); auto &body = goto_function.body; @@ -316,7 +316,7 @@ dfcc_instrumentt::get_local_statics(const irep_idt &function_id) void dfcc_instrumentt::instrument_function( const irep_idt &function_id, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, std::set &function_pointer_contracts) { // never instrument a function twice @@ -345,14 +345,14 @@ void dfcc_instrumentt::instrument_function( goto_function, write_set, local_statics, - loop_contract_mode, + loop_contract_config, function_pointer_contracts); } void dfcc_instrumentt::instrument_wrapped_function( const irep_idt &wrapped_function_id, const irep_idt &initial_function_id, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, std::set &function_pointer_contracts) { // never instrument a function twice @@ -383,7 +383,7 @@ void dfcc_instrumentt::instrument_wrapped_function( goto_function, write_set, local_statics, - loop_contract_mode, + loop_contract_config, function_pointer_contracts); } @@ -402,7 +402,7 @@ void dfcc_instrumentt::instrument_goto_program( function_id, goto_function, write_set, - dfcc_loop_contract_modet::NONE, + loop_contract_configt{false}, goto_model.symbol_table, message_handler, library); @@ -429,7 +429,7 @@ void dfcc_instrumentt::instrument_goto_function( goto_functiont &goto_function, const exprt &write_set, const std::set &local_statics, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, std::set &function_pointer_contracts) { if(!goto_function.body_available()) @@ -451,7 +451,7 @@ void dfcc_instrumentt::instrument_goto_function( function_id, goto_function, write_set, - loop_contract_mode, + loop_contract_config, goto_model.symbol_table, message_handler, library); @@ -468,13 +468,13 @@ void dfcc_instrumentt::instrument_goto_function( // recalculate numbers, etc. goto_model.goto_functions.update(); - if(loop_contract_mode != dfcc_loop_contract_modet::NONE) + if(loop_contract_config.apply_loop_contracts) { apply_loop_contracts( function_id, goto_function, cfg_info, - loop_contract_mode, + loop_contract_config, local_statics, function_pointer_contracts); } @@ -1241,11 +1241,11 @@ void dfcc_instrumentt::apply_loop_contracts( const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, const std::set &local_statics, std::set &function_pointer_contracts) { - PRECONDITION(loop_contract_mode != dfcc_loop_contract_modet::NONE); + PRECONDITION(loop_contract_config.apply_loop_contracts); cfg_info.get_loops_toposorted(); std::list to_unwind; @@ -1275,7 +1275,7 @@ void dfcc_instrumentt::apply_loop_contracts( } // If required, unwind all transformed loops to yield base and step cases - if(loop_contract_mode == dfcc_loop_contract_modet::APPLY_UNWIND) + if(loop_contract_config.unwind_transformed_loops) { unwindsett unwindset{goto_model}; unwindset.parse_unwindset(to_unwind, log.get_message_handler()); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h index 4dd9aeec881..1d3494de226 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h @@ -21,9 +21,10 @@ Author: Remi Delmas, delmasrd@amazon.com #include +#include + #include "dfcc_contract_mode.h" #include "dfcc_instrument_loop.h" -#include "dfcc_loop_contract_mode.h" #include #include @@ -75,12 +76,12 @@ class dfcc_instrumentt /// called from the loop. /// /// \param function_id Function to instrument - /// \param loop_contract_mode Mode to use for loop contracts + /// \param loop_contract_config Config to use for loop contracts /// \param function_pointer_contracts Contract names discovered in calls to /// the `obeys_contract` predicate are added to this set. void instrument_harness_function( const irep_idt &function_id, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, std::set &function_pointer_contracts); /// \brief Instruments a GOTO function by adding an extra write set parameter @@ -96,12 +97,12 @@ class dfcc_instrumentt /// \param function_id The name of the function, used to retrieve the function /// to instrument and used as prefix when generating new symbols during /// instrumentation. - /// \param loop_contract_mode Mode to use for loop contracts + /// \param loop_contract_config Config to use for loop contracts /// \param function_pointer_contracts Contracts discovered in calls to /// the obeys_contract predicate are added to this set. void instrument_function( const irep_idt &function_id, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, std::set &function_pointer_contracts); /// \brief Instruments a GOTO function by adding an extra write set parameter @@ -121,13 +122,13 @@ class dfcc_instrumentt /// \param initial_function_id The initial name of the function, /// before mangling. This is the name used to identify statics symbols in the /// symbol table that were locally declared in the function. - /// \param loop_contract_mode Mode to use for loop contracts + /// \param loop_contract_config Config to use for loop contracts /// \param function_pointer_contracts contracts discovered in calls to /// the obeys_contract predicate are added to this set. void instrument_wrapped_function( const irep_idt &wrapped_function_id, const irep_idt &initial_function_id, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, std::set &function_pointer_contracts); /// \brief Instruments a GOTO program against a given write set variable. @@ -234,7 +235,7 @@ class dfcc_instrumentt goto_functiont &goto_function, const exprt &write_set, const std::set &local_statics, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, std::set &function_pointer_contracts); /// \brief Instruments the instructions found between \p first_instruction and @@ -361,7 +362,7 @@ class dfcc_instrumentt const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, const std::set &local_statics, std::set &function_pointer_contracts); }; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp index 2a1429234c3..ef8300f1182 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp @@ -387,7 +387,7 @@ void dfcc_lift_memory_predicatest::lift_predicate( // adds checks for side effects, maps core predicates to their implementation. instrument.instrument_function( function_id, - dfcc_loop_contract_modet::NONE, + loop_contract_configt{false}, discovered_function_pointer_contracts); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_contract_mode.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_contract_mode.cpp deleted file mode 100644 index 36850003117..00000000000 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_contract_mode.cpp +++ /dev/null @@ -1,55 +0,0 @@ -/*******************************************************************\ - -Module: Dynamic frame condition checking for function contracts - -Author: Remi Delmas, delmasrd@amazon.com - -Date: March 2023 - -\*******************************************************************/ - -#include "dfcc_loop_contract_mode.h" - -#include - -dfcc_loop_contract_modet dfcc_loop_contract_mode_from_bools( - bool apply_loop_contracts, - bool unwind_transformed_loops) -{ - if(apply_loop_contracts) - { - if(unwind_transformed_loops) - { - return dfcc_loop_contract_modet::APPLY_UNWIND; - } - else - { - return dfcc_loop_contract_modet::APPLY; - } - } - else - { - return dfcc_loop_contract_modet::NONE; - } -} - -std::string -dfcc_loop_contract_mode_to_string(const dfcc_loop_contract_modet mode) -{ - switch(mode) - { - case dfcc_loop_contract_modet::NONE: - return "dfcc_loop_contract_modet::NONE"; - case dfcc_loop_contract_modet::APPLY: - return "dfcc_loop_contract_modet::APPLY"; - case dfcc_loop_contract_modet::APPLY_UNWIND: - return "dfcc_loop_contract_modet::APPLY_UNWIND"; - } - UNREACHABLE; -} - -std::ostream &operator<<(std::ostream &os, const dfcc_loop_contract_modet mode) -{ - os << dfcc_loop_contract_mode_to_string(mode); - return os; -} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_contract_mode.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_contract_mode.h deleted file mode 100644 index 63998abc799..00000000000 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_contract_mode.h +++ /dev/null @@ -1,37 +0,0 @@ -/*******************************************************************\ - -Module: Dynamic frame condition checking for function contracts - -Author: Remi Delmas, delmasrd@amazon.com - -\*******************************************************************/ - -/// \file -/// Enumeration representing the instrumentation mode for loop contracts. - -#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_CONTRACT_MODE_H -#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_CONTRACT_MODE_H - -#include - -/// Enumeration representing the instrumentation mode for loop contracts. -enum class dfcc_loop_contract_modet -{ - /// Do not apply loop contracts - NONE, - /// Apply loop contracts - APPLY, - /// Apply loop contracts and unwind the resulting base + step encoding - APPLY_UNWIND -}; - -/// Generates an enum value from boolean flags for application and unwinding. -dfcc_loop_contract_modet dfcc_loop_contract_mode_from_bools( - bool apply_loop_contracts, - bool unwind_transformed_loops); - -std::string dfcc_loop_contract_mode_to_string(dfcc_loop_contract_modet mode); - -std::ostream &operator<<(std::ostream &os, const dfcc_loop_contract_modet mode); - -#endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp index 3bfa11b4ffc..1772647fc94 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -17,7 +17,6 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include "dfcc_library.h" -#include "dfcc_loop_contract_mode.h" dfcc_spec_functionst::dfcc_spec_functionst( goto_modelt &goto_model, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp index 21c886befe0..f74490d3c11 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp @@ -55,43 +55,42 @@ dfcc_swap_and_wrapt::dfcc_swap_and_wrapt( // static map std::map< irep_idt, - std::pair>> + std::pair>> dfcc_swap_and_wrapt::cache; void dfcc_swap_and_wrapt::swap_and_wrap( const dfcc_contract_modet contract_mode, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set &function_pointer_contracts, bool allow_recursive_calls) { auto pair = cache.insert( - {function_id, {contract_id, {contract_mode, loop_contract_mode}}}); + {function_id, {contract_id, {contract_mode, loop_contract_config}}}); auto inserted = pair.second; if(!inserted) { irep_idt old_contract_id = pair.first->second.first; dfcc_contract_modet old_contract_mode = pair.first->second.second.first; - dfcc_loop_contract_modet old_loop_contract_mode = + loop_contract_configt old_loop_contract_config = pair.first->second.second.second; // different swap already performed, abort (should be unreachable) if( old_contract_id != contract_id || old_contract_mode != contract_mode || - old_loop_contract_mode != loop_contract_mode) + old_loop_contract_config != loop_contract_config) { std::ostringstream err_msg; err_msg << "DFCC: multiple attempts to swap and wrap function '" << function_id << "':\n"; err_msg << "- with '" << old_contract_id << "' in " << dfcc_contract_mode_to_string(old_contract_mode) << " " - << dfcc_loop_contract_mode_to_string(old_loop_contract_mode) - << "\n"; + << old_loop_contract_config.to_string() << "\n"; err_msg << "- with '" << contract_id << "' in " << dfcc_contract_mode_to_string(contract_mode) << " " - << dfcc_loop_contract_mode_to_string(loop_contract_mode) << "\n"; + << loop_contract_config.to_string() << "\n"; throw invalid_input_exceptiont(err_msg.str()); } // same swap already performed @@ -104,7 +103,7 @@ void dfcc_swap_and_wrapt::swap_and_wrap( case dfcc_contract_modet::CHECK: { check_contract( - loop_contract_mode, + loop_contract_config, function_id, contract_id, function_pointer_contracts, @@ -152,7 +151,7 @@ void dfcc_swap_and_wrapt::get_swapped_functions(std::set &dest) const /// END_FUNCTION; /// ``` void dfcc_swap_and_wrapt::check_contract( - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set &function_pointer_contracts, @@ -278,7 +277,7 @@ void dfcc_swap_and_wrapt::check_contract( // instrument the wrapped function instrument.instrument_wrapped_function( - wrapped_id, wrapper_id, loop_contract_mode, function_pointer_contracts); + wrapped_id, wrapper_id, loop_contract_config, function_pointer_contracts); goto_model.goto_functions.update(); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h index 737bd3392c8..9fb11f4c171 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h @@ -50,7 +50,7 @@ class dfcc_swap_and_wrapt dfcc_contract_handlert &contract_handler); void swap_and_wrap_check( - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set &function_pointer_contracts, @@ -58,7 +58,7 @@ class dfcc_swap_and_wrapt { swap_and_wrap( dfcc_contract_modet::CHECK, - loop_contract_mode, + loop_contract_config, function_id, contract_id, function_pointer_contracts, @@ -72,7 +72,7 @@ class dfcc_swap_and_wrapt { swap_and_wrap( dfcc_contract_modet::REPLACE, - dfcc_loop_contract_modet::NONE, + loop_contract_configt{false}, function_id, contract_id, function_pointer_contracts, @@ -95,13 +95,12 @@ class dfcc_swap_and_wrapt /// remember all functions that were swapped/wrapped and in which mode static std::map< irep_idt, - std:: - pair>> + std::pair>> cache; void swap_and_wrap( const dfcc_contract_modet contract_mode, - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set &function_pointer_contracts, @@ -110,7 +109,7 @@ class dfcc_swap_and_wrapt /// Swaps-and-wraps the given `function_id` in a wrapper function that /// checks the given `contract_id`. void check_contract( - const dfcc_loop_contract_modet loop_contract_mode, + const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set &function_pointer_contracts, diff --git a/src/goto-instrument/contracts/loop_contract_config.h b/src/goto-instrument/contracts/loop_contract_config.h new file mode 100644 index 00000000000..35f790fa2c1 --- /dev/null +++ b/src/goto-instrument/contracts/loop_contract_config.h @@ -0,0 +1,55 @@ +/*******************************************************************\ + +Module: Config for loop contract + +Author: Qinheping Hu + +Date: June 2024 + +\*******************************************************************/ + +/// \file +/// Config for loop contract + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_LOOP_CONTRACT_CONFIG_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_LOOP_CONTRACT_CONFIG_H + +/// Loop contract configurations +struct loop_contract_configt +{ +public: + // Apply loop contracts. + bool apply_loop_contracts = false; + + // Unwind transformed loops after applying loop contracts or not. + bool unwind_transformed_loops = true; + + // Check if loop contracts are all side-effect free. + bool check_side_effect = true; + + std::string to_string() const + { + std::string result; + result += "Apply loop contracts: "; + result += (apply_loop_contracts ? "yes\n" : "no\n"); + result += "Unwind transformed loops: "; + result += (unwind_transformed_loops ? "yes\n" : "no\n"); + result += "Check side effect of loop contracts: "; + result += (check_side_effect ? "yes\n" : "no\n"); + return result; + } + + bool operator==(const loop_contract_configt &rhs) const + { + return apply_loop_contracts == rhs.apply_loop_contracts && + unwind_transformed_loops == rhs.unwind_transformed_loops && + check_side_effect == rhs.check_side_effect; + } + + bool operator!=(const loop_contract_configt &rhs) const + { + return !(this == &rhs); + } +}; + +#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_LOOP_CONTRACT_CONFIG_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 868d2027a16..dc613b102f4 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1166,6 +1166,26 @@ void goto_instrument_parse_optionst::instrument_goto_program() goto_model, file_name, ui_message_handler); } + // Initialize loop contract config from cmdline. + loop_contract_configt loop_contract_config = { + cmdline.isset(FLAG_LOOP_CONTRACTS), + !cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND)}; + + if( + cmdline.isset(FLAG_LOOP_CONTRACTS) && + cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND)) + { + // After instrumentation, all annotated loops will be transformed to + // loops execute exactly once. CBMC by default unwinds transformed loops + // by twice. + // Users may want to disable the default unwinding to avoid duplicate + // assertions. + log.warning() << "**** WARNING: transformed loops will not be unwound " + << "after applying loop contracts. Note that transformed " + << "loops require at least unwinding bounds 2 to pass " + << "the unwinding assertions." << messaget::eom; + } + bool use_dfcc = cmdline.isset(FLAG_DFCC); if(use_dfcc) { @@ -1209,22 +1229,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() cmdline.get_values("nondet-static-exclude").begin(), cmdline.get_values("nondet-static-exclude").end()); - if( - cmdline.isset(FLAG_LOOP_CONTRACTS) && - cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND)) - { - // When the model is produced by Kani, we must not automatically unwind - // the backjump introduced by the loop transformation. - // Automatic unwinding duplicates assertions found in the loop body, and - // since Kani expects property identifiers to remain unique. Having - // duplicate instances of the assertions makes Kani fail to handle the - // analysis results. - log.warning() << "**** WARNING: transformed loops will not be unwound " - << "after applying loop contracts. Remember to unwind " - << "them at least twice to pass unwinding-assertions." - << messaget::eom; - } - dfcc( options, goto_model, @@ -1233,8 +1237,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() : std::optional{to_enforce.front()}, allow_recursive_calls, to_replace, - cmdline.isset(FLAG_LOOP_CONTRACTS), - !cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND), + loop_contract_config, to_exclude_from_nondet_static, log.get_message_handler()); } @@ -1245,7 +1248,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_indirect_call_and_rtti_removal(); log.status() << "Trying to force one backedge per target" << messaget::eom; ensure_one_backedge_per_target(goto_model); - code_contractst contracts(goto_model, log); + code_contractst contracts(goto_model, log, loop_contract_config); std::set to_replace( cmdline.get_values(FLAG_REPLACE_CALL).begin(), @@ -1268,20 +1271,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset(FLAG_LOOP_CONTRACTS)) { - if(cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND)) - { - contracts.unwind_transformed_loops = false; - // When the model is produced by Kani, we must not automatically unwind - // the backjump introduced by the loop transformation. - // Automatic unwinding duplicates assertions found in the loop body, and - // since Kani expects property identifiers to remain unique. Having - // duplicate instances of the assertions makes Kani fail to handle the - // analysis results. - log.warning() << "**** WARNING: transformed loops will not be unwound " - << "after applying loop contracts. Remember to unwind " - << "them at least twice to pass unwinding-assertions." - << messaget::eom; - } contracts.apply_loop_contracts(to_exclude_from_nondet_static); } } diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index f959361f41e..8d5a8ef282c 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -588,8 +588,8 @@ std::optional cegis_verifiert::verify() log.get_message_handler().set_verbosity(messaget::M_ERROR); // Apply loop contracts we annotated. - code_contractst cont(goto_model, log); - cont.unwind_transformed_loops = false; + code_contractst cont( + goto_model, log, loop_contract_configt{true, false, true}); cont.apply_loop_contracts(); original_loop_number_map = cont.get_original_loop_number_map(); loop_havoc_set = cont.get_loop_havoc_set(); diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp index 93f264fd24e..6cd7628010a 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp @@ -133,9 +133,12 @@ int goto_synthesizer_parse_optionst::doit() std::set to_exclude_from_nondet_static( cmdline.get_values("nondet-static-exclude").begin(), cmdline.get_values("nondet-static-exclude").end()); - code_contractst contracts(goto_model, log); - contracts.unwind_transformed_loops = - !cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND); + code_contractst contracts( + goto_model, + log, + loop_contract_configt{ + true, !cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND), true}); + contracts.apply_loop_contracts(to_exclude_from_nondet_static); // recalculate numbers, etc.