From 1ad6ecc416b0bed3e857221198a6eb7c67739a67 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 16 Feb 2023 20:59:13 +0000 Subject: [PATCH 1/5] CONTRACTS: new inlining and loop detection methods Allows to to inlining and loop detection directly on a goto program instead of a goto function --- .../contracts/dynamic-frames/dfcc_utils.cpp | 51 ++++++++++++++++--- .../contracts/dynamic-frames/dfcc_utils.h | 17 +++++++ 2 files changed, 62 insertions(+), 6 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp index 4366c0e8a4a..acda92165d1 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp @@ -476,8 +476,7 @@ void dfcc_utilst::inline_function(const irep_idt &function_id) inlining_decoratort decorated(log.get_message_handler()); namespacet ns{goto_model.symbol_table}; - goto_function_inline( - goto_model.goto_functions, function_id, ns, log.get_message_handler()); + goto_function_inline(goto_model.goto_functions, function_id, ns, decorated); decorated.throw_on_recursive_calls(log, 0); decorated.throw_on_no_body(log, 0); @@ -503,8 +502,7 @@ void dfcc_utilst::inline_function( inlining_decoratort decorated(log.get_message_handler()); namespacet ns{goto_model.symbol_table}; - goto_function_inline( - goto_model.goto_functions, function_id, ns, log.get_message_handler()); + goto_function_inline(goto_model.goto_functions, function_id, ns, decorated); no_body.insert( decorated.get_no_body_set().begin(), decorated.get_no_body_set().end()); recursive_call.insert( @@ -519,10 +517,51 @@ void dfcc_utilst::inline_function( goto_model.goto_functions.update(); } +void dfcc_utilst::inline_program(goto_programt &program) +{ + inlining_decoratort decorated(log.get_message_handler()); + namespacet ns{goto_model.symbol_table}; + goto_program_inline(goto_model.goto_functions, program, ns, decorated); + + decorated.throw_on_recursive_calls(log, 0); + decorated.throw_on_no_body(log, 0); + decorated.throw_on_missing_function(log, 0); + decorated.throw_on_not_enough_arguments(log, 0); +} + +void dfcc_utilst::inline_program( + goto_programt &goto_program, + std::set &no_body, + std::set &recursive_call, + std::set &missing_function, + std::set ¬_enough_arguments) +{ + inlining_decoratort decorated(log.get_message_handler()); + namespacet ns{goto_model.symbol_table}; + goto_program_inline(goto_model.goto_functions, goto_program, ns, decorated); + no_body.insert( + decorated.get_no_body_set().begin(), decorated.get_no_body_set().end()); + recursive_call.insert( + decorated.get_recursive_call_set().begin(), + decorated.get_recursive_call_set().end()); + missing_function.insert( + decorated.get_missing_function_set().begin(), + decorated.get_missing_function_set().end()); + not_enough_arguments.insert( + decorated.get_not_enough_arguments_set().begin(), + decorated.get_not_enough_arguments_set().end()); + goto_model.goto_functions.update(); +} + +bool dfcc_utilst::has_no_loops(const goto_programt &goto_program) +{ + return is_loop_free(goto_program, ns, log); +} + bool dfcc_utilst::has_no_loops(const irep_idt &function_id) { - auto &goto_function = goto_model.goto_functions.function_map.at(function_id); - return is_loop_free(goto_function.body, ns, log); + return has_no_loops( + goto_model.goto_functions.function_map.at(function_id).body); } void dfcc_utilst::set_hide(const irep_idt &function_id, bool hide) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h index 0c2c42a2c1d..0a9dff03f19 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h @@ -20,6 +20,7 @@ Date: August 2022 #include class goto_modelt; +class goto_programt; class message_handlert; class symbolt; @@ -213,6 +214,22 @@ class dfcc_utilst /// \returns True iff \p function_id is loop free. bool has_no_loops(const irep_idt &function_id); + /// \brief Inlines the given program, aborts on recursive calls during + /// inlining. + void inline_program(goto_programt &program); + + /// \brief Inlines the given program, and returns function symbols that + /// caused warnings. + void inline_program( + goto_programt &goto_program, + std::set &no_body, + std::set &recursive_call, + std::set &missing_function, + std::set ¬_enough_arguments); + + /// \returns True iff \p goto_program is loop free. + bool has_no_loops(const goto_programt &goto_program); + /// \brief Sets the given hide flag on all instructions of the function if it /// exists. void set_hide(const irep_idt &function_id, bool hide); From 8427b1f8f650fd6b5ecf7a8fa0d63c2d9bb15481 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 16 Feb 2023 20:57:51 +0000 Subject: [PATCH 2/5] CONTRACTS: rearchitecture code for loop contracts - Factor out some methods in dfcc_spec_functionst - Move the code generation methods from dfcc_contract_functionst to dfcc_contract_clauses_codegent. - Update Makefile with new class. - Propagate interface changes to top level class --- src/goto-instrument/Makefile | 1 + .../contracts/dynamic-frames/dfcc.cpp | 11 +- .../contracts/dynamic-frames/dfcc.h | 5 +- .../dfcc_contract_clauses_codegen.cpp | 288 ++++++++++++++++++ .../dfcc_contract_clauses_codegen.h | 125 ++++++++ .../dfcc_contract_functions.cpp | 263 ++-------------- .../dynamic-frames/dfcc_contract_functions.h | 34 +-- .../dynamic-frames/dfcc_contract_handler.cpp | 7 +- .../dynamic-frames/dfcc_contract_handler.h | 5 +- .../dynamic-frames/dfcc_spec_functions.cpp | 224 ++++++++------ .../dynamic-frames/dfcc_spec_functions.h | 76 +++++ 11 files changed, 677 insertions(+), 362 deletions(-) create mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp create mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 67deed54d59..f1befc993b3 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -26,6 +26,7 @@ SRC = accelerate/accelerate.cpp \ contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp \ contracts/dynamic-frames/dfcc_instrument.cpp \ contracts/dynamic-frames/dfcc_spec_functions.cpp \ + contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp \ contracts/dynamic-frames/dfcc_contract_functions.cpp \ contracts/dynamic-frames/dfcc_wrapper_program.cpp \ contracts/dynamic-frames/dfcc_contract_handler.cpp \ diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index a523067d19e..68a6b3e10f2 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -191,6 +191,12 @@ dfcct::dfcct( instrument(goto_model, message_handler, utils, library), memory_predicates(goto_model, utils, library, instrument, message_handler), spec_functions(goto_model, message_handler, utils, library, instrument), + contract_clauses_codegen( + goto_model, + message_handler, + utils, + library, + spec_functions), contract_handler( goto_model, message_handler, @@ -198,7 +204,8 @@ dfcct::dfcct( library, instrument, memory_predicates, - spec_functions), + spec_functions, + contract_clauses_codegen), swap_and_wrap( goto_model, message_handler, @@ -483,6 +490,8 @@ void dfcct::instrument_other_functions() goto_model.goto_functions.update(); + // TODO specialise the library functions for the max size of + // loop and function contracts if(to_check.has_value()) { log.status() << "Specializing cprover_contracts functions for assigns " diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.h b/src/goto-instrument/contracts/dynamic-frames/dfcc.h index 400439c5c0b..7ef25c5b287 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.h @@ -33,6 +33,7 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include +#include "dfcc_contract_clauses_codegen.h" #include "dfcc_contract_handler.h" #include "dfcc_instrument.h" #include "dfcc_library.h" @@ -208,13 +209,15 @@ class dfcct message_handlert &message_handler; messaget log; - // hold the global state of the transformation (caches etc.) + // Singletons that hold the global state of the program transformation + // (caches etc.) dfcc_utilst utils; dfcc_libraryt library; namespacet ns; dfcc_instrumentt instrument; dfcc_lift_memory_predicatest memory_predicates; dfcc_spec_functionst spec_functions; + dfcc_contract_clauses_codegent contract_clauses_codegen; dfcc_contract_handlert contract_handler; dfcc_swap_and_wrapt swap_and_wrap; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp new file mode 100644 index 00000000000..99f4bf888d5 --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp @@ -0,0 +1,288 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: February 2023 + +\*******************************************************************/ +#include "dfcc_contract_clauses_codegen.h" + +#include +#include +#include +#include +#include +#include +#include + +#include + +#include +#include +#include + +#include "dfcc_library.h" +#include "dfcc_spec_functions.h" +#include "dfcc_utils.h" + +dfcc_contract_clauses_codegent::dfcc_contract_clauses_codegent( + goto_modelt &goto_model, + message_handlert &message_handler, + dfcc_utilst &utils, + dfcc_libraryt &library, + dfcc_spec_functionst &spec_functions) + : goto_model(goto_model), + message_handler(message_handler), + log(message_handler), + utils(utils), + library(library), + spec_functions(spec_functions), + ns(goto_model.symbol_table) +{ +} + +void dfcc_contract_clauses_codegent::gen_spec_assigns_instructions( + const irep_idt &language_mode, + const exprt::operandst &assigns_clause, + goto_programt &dest) +{ + for(const auto &expr : assigns_clause) + { + if(can_cast_expr(expr)) + { + encode_assignable_target_group( + language_mode, to_conditional_target_group_expr(expr), dest); + } + else + { + encode_assignable_target(language_mode, expr, dest); + } + } + + // inline resulting program and check for loops + inline_and_check_warnings(dest); + PRECONDITION_WITH_DIAGNOSTICS( + utils.has_no_loops(dest), + "loops in assigns clause specification functions must be unwound before " + "contracts instrumentation"); +} + +void dfcc_contract_clauses_codegent::gen_spec_frees_instructions( + const irep_idt &language_mode, + const exprt::operandst &frees_clause, + goto_programt &dest) +{ + for(const auto &expr : frees_clause) + { + if(can_cast_expr(expr)) + { + encode_freeable_target_group( + language_mode, to_conditional_target_group_expr(expr), dest); + } + else + { + encode_freeable_target(language_mode, expr, dest); + } + } + + // inline resulting program and check for loops + inline_and_check_warnings(dest); + PRECONDITION_WITH_DIAGNOSTICS( + utils.has_no_loops(dest), + "loops in assigns clause specification functions must be unwound before " + "contracts instrumentation"); +} + +void dfcc_contract_clauses_codegent::encode_assignable_target_group( + const irep_idt &language_mode, + const conditional_target_group_exprt &group, + goto_programt &dest) +{ + const source_locationt &source_location = group.source_location(); + + // clean up side effects from the condition expression if needed + cleanert cleaner(goto_model.symbol_table, log.get_message_handler()); + exprt condition(group.condition()); + if(has_subexpr(condition, ID_side_effect)) + cleaner.clean(condition, dest, language_mode); + + // Jump target if condition is false + auto goto_instruction = dest.add( + goto_programt::make_incomplete_goto(not_exprt{condition}, source_location)); + + for(const auto &target : group.targets()) + encode_assignable_target(language_mode, target, dest); + + auto label_instruction = dest.add(goto_programt::make_skip(source_location)); + goto_instruction->complete_goto(label_instruction); +} + +void dfcc_contract_clauses_codegent::encode_assignable_target( + const irep_idt &language_mode, + const exprt &target, + goto_programt &dest) +{ + const source_locationt &source_location = target.source_location(); + + if(can_cast_expr(target)) + { + // A function call target `foo(params)` becomes `CALL foo(params);` + const auto &funcall = to_side_effect_expr_function_call(target); + code_function_callt code_function_call(to_symbol_expr(funcall.function())); + auto &arguments = code_function_call.arguments(); + for(auto &arg : funcall.arguments()) + arguments.emplace_back(arg); + dest.add( + goto_programt::make_function_call(code_function_call, source_location)); + } + else if(is_assignable(target)) + { + // An lvalue `target` becomes + //` CALL __CPROVER_assignable(&target, sizeof(target), is_ptr_to_ptr);` + const auto &size = + size_of_expr(target.type(), namespacet(goto_model.symbol_table)); + + if(!size.has_value()) + { + throw invalid_source_file_exceptiont{ + "no definite size for lvalue assigns clause target " + + from_expr_using_mode(ns, language_mode, target), + target.source_location()}; + } + // we have to build the symbol manually because it might not + // be present in the symbol table if the user program does not already + // use it. + code_function_callt code_function_call( + symbol_exprt(CPROVER_PREFIX "assignable", empty_typet())); + auto &arguments = code_function_call.arguments(); + + // ptr + arguments.emplace_back(typecast_exprt::conditional_cast( + address_of_exprt{target}, pointer_type(empty_typet()))); + + // size + arguments.emplace_back(size.value()); + + // is_ptr_to_ptr + arguments.emplace_back(make_boolean_expr(target.type().id() == ID_pointer)); + + dest.add( + goto_programt::make_function_call(code_function_call, source_location)); + } + else + { + // any other type of target is unsupported + throw invalid_source_file_exceptiont( + "unsupported assigns clause target " + + from_expr_using_mode(ns, language_mode, target), + target.source_location()); + } +} + +void dfcc_contract_clauses_codegent::encode_freeable_target_group( + const irep_idt &language_mode, + const conditional_target_group_exprt &group, + goto_programt &dest) +{ + const source_locationt &source_location = group.source_location(); + + // clean up side effects from the condition expression if needed + cleanert cleaner(goto_model.symbol_table, log.get_message_handler()); + exprt condition(group.condition()); + if(has_subexpr(condition, ID_side_effect)) + cleaner.clean(condition, dest, language_mode); + + // Jump target if condition is false + auto goto_instruction = dest.add( + goto_programt::make_incomplete_goto(not_exprt{condition}, source_location)); + + for(const auto &target : group.targets()) + encode_freeable_target(language_mode, target, dest); + + auto label_instruction = dest.add(goto_programt::make_skip(source_location)); + goto_instruction->complete_goto(label_instruction); +} + +void dfcc_contract_clauses_codegent::encode_freeable_target( + const irep_idt &language_mode, + const exprt &target, + goto_programt &dest) +{ + const source_locationt &source_location = target.source_location(); + + if(can_cast_expr(target)) + { + const auto &funcall = to_side_effect_expr_function_call(target); + if(can_cast_expr(funcall.function())) + { + // for calls to user-defined functions a call expression `foo(params)` + // becomes an instruction `CALL foo(params);` + code_function_callt code_function_call( + to_symbol_expr(funcall.function())); + auto &arguments = code_function_call.arguments(); + for(auto &arg : funcall.arguments()) + arguments.emplace_back(arg); + dest.add( + goto_programt::make_function_call(code_function_call, source_location)); + } + } + else if(can_cast_type(target.type())) + { + // A plain `target` becomes `CALL __CPROVER_freeable(target);` + code_function_callt code_function_call( + utils.get_function_symbol(CPROVER_PREFIX "freeable").symbol_expr()); + auto &arguments = code_function_call.arguments(); + arguments.emplace_back(target); + + dest.add( + goto_programt::make_function_call(code_function_call, source_location)); + } + else + { + // any other type of target is unsupported + throw invalid_source_file_exceptiont( + "unsupported frees clause target " + + from_expr_using_mode(ns, language_mode, target), + target.source_location()); + } +} + +void dfcc_contract_clauses_codegent::inline_and_check_warnings( + goto_programt &goto_program) +{ + std::set no_body; + std::set missing_function; + std::set recursive_call; + std::set not_enough_arguments; + + utils.inline_program( + goto_program, + no_body, + recursive_call, + missing_function, + not_enough_arguments); + + // check that the only no body / missing functions are the cprover builtins + for(const auto &id : no_body) + { + INVARIANT( + library.is_front_end_builtin(id), + "no body for '" + id2string(id) + "' when inlining goto program"); + } + + for(auto it : missing_function) + { + INVARIANT( + library.is_front_end_builtin(it), + "missing function '" + id2string(it) + "' when inlining goto program"); + } + + INVARIANT( + recursive_call.size() == 0, + "recursive calls found when inlining goto program"); + + INVARIANT( + not_enough_arguments.size() == 0, + "not enough arguments when inlining goto program"); +} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h new file mode 100644 index 00000000000..c3a8b2709dd --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h @@ -0,0 +1,125 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: February 2023 + +\*******************************************************************/ + +/// \file +/// Translates assigns and frees clauses of a function contract or +/// loop contract into goto programs that build write sets or havoc write sets. + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H + +#include + +#include +#include +#include +#include + +#include "dfcc_contract_mode.h" + +#include + +class goto_modelt; +class message_handlert; +class dfcc_libraryt; +class dfcc_utilst; +class dfcc_spec_functionst; +class code_with_contract_typet; +class conditional_target_group_exprt; + +class dfcc_contract_clauses_codegent +{ +public: + /// \param goto_model goto model being transformed + /// \param message_handler used debug/warning/error messages + /// \param utils utility class for dynamic frames + /// \param library the contracts instrumentation library + /// \param spec_functions provides translation methods for assignable set + /// or freeable set specification functions. + dfcc_contract_clauses_codegent( + goto_modelt &goto_model, + message_handlert &message_handler, + dfcc_utilst &utils, + dfcc_libraryt &library, + dfcc_spec_functionst &spec_functions); + + /// \brief Generates instructions encoding the \p assigns_clause targets and + /// adds them to \p dest. + /// + /// \details Assumes that all targets in the clause are represented as plain + /// expressions (i.e. an lambdas expressions introduced for function contract + /// targets may are already instanciated). + /// + /// \param language_mode Mode to use for fresh symbols + /// \param assigns_clause Sequence of targets to encode + /// \param dest Destination program + void gen_spec_assigns_instructions( + const irep_idt &language_mode, + const exprt::operandst &assigns_clause, + goto_programt &dest); + + /// \brief Generates instructions encoding the \p frees_clause targets and + /// adds them to \p dest. + /// + /// \details Assumes that all targets in the clause are represented as plain + /// expressions (i.e. an lambdas expressions introduced for function contract + /// targets may are already instanciated). + /// + /// \param language_mode Mode to use for fresh symbols + /// \param frees_clause Sequence of targets to encode + /// \param dest Destination program + void gen_spec_frees_instructions( + const irep_idt &language_mode, + const exprt::operandst &frees_clause, + goto_programt &dest); + +protected: + goto_modelt &goto_model; + message_handlert &message_handler; + messaget log; + dfcc_utilst &utils; + dfcc_libraryt &library; + dfcc_spec_functionst &spec_functions; + namespacet ns; + + /// Generates GOTO instructions to build the representation of the given + /// conditional target group. + void encode_assignable_target_group( + const irep_idt &language_mode, + const conditional_target_group_exprt &group, + goto_programt &dest); + + /// Generates GOTO instructions to build the representation of the given + /// assignable target. + void encode_assignable_target( + const irep_idt &language_mode, + const exprt &target, + goto_programt &dest); + + /// Generates GOTO instructions to build the representation of the given + /// conditional target group. + void encode_freeable_target_group( + const irep_idt &language_mode, + const conditional_target_group_exprt &group, + goto_programt &dest); + + /// Generates GOTO instructions to build the representation of the given + /// freeable target. + void encode_freeable_target( + const irep_idt &language_mode, + const exprt &target, + goto_programt &dest); + + /// Inlines all calls in the given program and checks that the only missing + /// functions or functions without bodies are built-in functions, + /// and that no other warnings happened. + void inline_and_check_warnings(goto_programt &goto_program); +}; + +#endif 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 9fdfac71676..33fcbe59b64 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp @@ -22,6 +22,7 @@ Date: August 2022 #include #include +#include "dfcc_contract_clauses_codegen.h" #include "dfcc_library.h" #include "dfcc_spec_functions.h" #include "dfcc_utils.h" @@ -32,7 +33,8 @@ dfcc_contract_functionst::dfcc_contract_functionst( message_handlert &message_handler, dfcc_utilst &utils, dfcc_libraryt &library, - dfcc_spec_functionst &spec_functions) + dfcc_spec_functionst &spec_functions, + dfcc_contract_clauses_codegent &contract_clauses_codegen) : pure_contract_symbol(pure_contract_symbol), code_with_contract(to_code_with_contract_type(pure_contract_symbol.type)), spec_assigns_function_id( @@ -47,6 +49,7 @@ dfcc_contract_functionst::dfcc_contract_functionst( utils(utils), library(library), spec_functions(spec_functions), + contract_clauses_codegen(contract_clauses_codegen), ns(goto_model.symbol_table) { gen_spec_assigns_function(); @@ -119,120 +122,22 @@ void dfcc_contract_functionst::gen_spec_assigns_function() // fetch the goto_function to add instructions to goto_functiont &goto_function = goto_model.goto_functions.function_map.at(spec_function_id); - goto_programt &body = goto_function.body; - for(const auto &assigns_expr : code_with_contract.assigns()) + exprt::operandst targets; + + for(const exprt &target : code_with_contract.assigns()) { - auto expr = to_lambda_expr(assigns_expr).application(lambda_parameters); - expr.add_source_location() = assigns_expr.source_location(); - if(can_cast_expr(expr)) - { - encode_assignable_target_group( - to_conditional_target_group_expr(expr), body); - } - else - { - encode_assignable_target(expr, body); - } + auto new_target = to_lambda_expr(target).application(lambda_parameters); + new_target.add_source_location() = target.source_location(); + targets.push_back(new_target); } + goto_programt &body = goto_function.body; + contract_clauses_codegen.gen_spec_assigns_instructions( + spec_function_symbol.mode, targets, body); body.add(goto_programt::make_end_function(spec_function_symbol.location)); goto_model.goto_functions.update(); - - inline_and_check_warnings(spec_function_id); - - PRECONDITION_WITH_DIAGNOSTICS( - utils.has_no_loops(spec_function_id), - "loops in assigns clause specification functions must be unwound before " - "model instrumentation"); - - goto_model.goto_functions.update(); -} - -void dfcc_contract_functionst::encode_assignable_target_group( - const conditional_target_group_exprt &group, - goto_programt &dest) -{ - const source_locationt &source_location = group.source_location(); - - // clean up side effects from the condition expression if needed - cleanert cleaner(goto_model.symbol_table, log.get_message_handler()); - exprt condition(group.condition()); - if(has_subexpr(condition, ID_side_effect)) - cleaner.clean(condition, dest, language_mode); - - // Jump target if condition is false - auto goto_instruction = dest.add( - goto_programt::make_incomplete_goto(not_exprt{condition}, source_location)); - - for(const auto &target : group.targets()) - encode_assignable_target(target, dest); - - auto label_instruction = dest.add(goto_programt::make_skip(source_location)); - goto_instruction->complete_goto(label_instruction); -} - -void dfcc_contract_functionst::encode_assignable_target( - const exprt &target, - goto_programt &dest) -{ - const source_locationt &source_location = target.source_location(); - - if(can_cast_expr(target)) - { - // A function call target `foo(params)` becomes `CALL foo(params);` - // ``` - const auto &funcall = to_side_effect_expr_function_call(target); - code_function_callt code_function_call(to_symbol_expr(funcall.function())); - auto &arguments = code_function_call.arguments(); - for(auto &arg : funcall.arguments()) - arguments.emplace_back(arg); - dest.add( - goto_programt::make_function_call(code_function_call, source_location)); - } - else if(is_assignable(target)) - { - // An lvalue `target` becomes - //` CALL __CPROVER_assignable(&target, sizeof(target), is_ptr_to_ptr);` - const auto &size = - size_of_expr(target.type(), namespacet(goto_model.symbol_table)); - - if(!size.has_value()) - { - throw invalid_source_file_exceptiont{ - "no definite size for lvalue assigns clause target " + - from_expr_using_mode(ns, language_mode, target), - target.source_location()}; - } - // we have to build the symbol manually because it might not - // be present in the symbol table if the user program does not already - // use it. - code_function_callt code_function_call( - symbol_exprt(CPROVER_PREFIX "assignable", empty_typet())); - auto &arguments = code_function_call.arguments(); - - // ptr - arguments.emplace_back(typecast_exprt::conditional_cast( - address_of_exprt{target}, pointer_type(empty_typet()))); - - // size - arguments.emplace_back(size.value()); - - // is_ptr_to_ptr - arguments.emplace_back(make_boolean_expr(target.type().id() == ID_pointer)); - - dest.add( - goto_programt::make_function_call(code_function_call, source_location)); - } - else - { - // any other type of target is unsupported - throw invalid_source_file_exceptiont( - "unsupported assigns clause target " + - from_expr_using_mode(ns, language_mode, target), - target.source_location()); - } } void dfcc_contract_functionst::gen_spec_frees_function() @@ -268,144 +173,20 @@ void dfcc_contract_functionst::gen_spec_frees_function() // fetch the goto_function to add instructions to goto_functiont &goto_function = goto_model.goto_functions.function_map.at(spec_function_id); - goto_programt &body = goto_function.body; - for(const auto &frees_expr : code_with_contract.frees()) + exprt::operandst targets; + + for(const exprt &target : code_with_contract.frees()) { - auto expr = to_lambda_expr(frees_expr).application(lambda_parameters); - expr.add_source_location() = frees_expr.source_location(); - if(can_cast_expr(expr)) - { - encode_freeable_target_group( - to_conditional_target_group_expr(expr), body); - } - else - { - encode_freeable_target(expr, body); - } + auto new_target = to_lambda_expr(target).application(lambda_parameters); + new_target.add_source_location() = target.source_location(); + targets.push_back(new_target); } + goto_programt &body = goto_function.body; + contract_clauses_codegen.gen_spec_frees_instructions( + spec_function_symbol.mode, targets, body); body.add(goto_programt::make_end_function(spec_function_symbol.location)); goto_model.goto_functions.update(); - - inline_and_check_warnings(spec_function_id); - - PRECONDITION_WITH_DIAGNOSTICS( - utils.has_no_loops(spec_function_id), - "loops in frees clause specification functions must be unwound before " - "model instrumentation"); - - goto_model.goto_functions.update(); -} - -void dfcc_contract_functionst::inline_and_check_warnings( - const irep_idt &function_id) -{ - std::set no_body; - std::set missing_function; - std::set recursive_call; - std::set not_enough_arguments; - - utils.inline_function( - function_id, - no_body, - recursive_call, - missing_function, - not_enough_arguments); - - // check that the only no body / missing functions are the cprover builtins - for(const auto &id : no_body) - { - INVARIANT( - library.is_front_end_builtin(id), - "no body for '" + id2string(id) + "' when inlining '" + - id2string(function_id) + "'"); - } - - for(auto it : missing_function) - { - INVARIANT( - library.is_front_end_builtin(it), - "missing function '" + id2string(it) + "' when inlining '" + - id2string(function_id) + "'"); - } - - INVARIANT( - recursive_call.size() == 0, - "recursive calls when inlining '" + id2string(function_id) + "'"); - - INVARIANT( - not_enough_arguments.size() == 0, - "not enough arguments when inlining '" + id2string(function_id) + "'"); -} - -void dfcc_contract_functionst::encode_freeable_target_group( - const conditional_target_group_exprt &group, - goto_programt &dest) -{ - const source_locationt &source_location = group.source_location(); - - // clean up side effects from the condition expression if needed - cleanert cleaner(goto_model.symbol_table, log.get_message_handler()); - exprt condition(group.condition()); - if(has_subexpr(condition, ID_side_effect)) - cleaner.clean(condition, dest, language_mode); - - // Jump target if condition is false - auto goto_instruction = dest.add( - goto_programt::make_incomplete_goto(not_exprt{condition}, source_location)); - - for(const auto &target : group.targets()) - encode_freeable_target(target, dest); - - auto label_instruction = dest.add(goto_programt::make_skip(source_location)); - goto_instruction->complete_goto(label_instruction); -} - -void dfcc_contract_functionst::encode_freeable_target( - const exprt &target, - goto_programt &dest) -{ - const source_locationt &source_location = target.source_location(); - - if(can_cast_expr(target)) - { - const auto &funcall = to_side_effect_expr_function_call(target); - if(can_cast_expr(funcall.function())) - { - // for calls to user-defined functions - // `foo(params)` - // - // ``` - // CALL foo(params); - // ``` - code_function_callt code_function_call( - to_symbol_expr(funcall.function())); - auto &arguments = code_function_call.arguments(); - for(auto &arg : funcall.arguments()) - arguments.emplace_back(arg); - dest.add( - goto_programt::make_function_call(code_function_call, source_location)); - } - } - else if(can_cast_type(target.type())) - { - // A plain `target` becomes `CALL __CPROVER_freeable(target);` - code_function_callt code_function_call( - utils.get_function_symbol(CPROVER_PREFIX "freeable").symbol_expr()); - auto &arguments = code_function_call.arguments(); - arguments.emplace_back(target); - - dest.add( - goto_programt::make_function_call(code_function_call, source_location)); - } - else - { - // any other type of target is unsupported - throw invalid_source_file_exceptiont( - "unsupported frees clause target " + - from_expr_using_mode(ns, language_mode, target), - target.source_location()); - } } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h index 95d9721de98..32e27a9742f 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h @@ -30,6 +30,7 @@ class message_handlert; class dfcc_libraryt; class dfcc_utilst; class dfcc_spec_functionst; +class dfcc_contract_clauses_codegent; class code_with_contract_typet; class conditional_target_group_exprt; @@ -67,14 +68,16 @@ class dfcc_contract_functionst /// \param utils utility class for dynamic frames /// \param library the contracts instrumentation library /// \param spec_functions provides translation methods for assignable set - /// or freeable set specification functions. + /// \param contract_clauses_codegen provides GOTO code generation methods + /// for assigns and free clauses. dfcc_contract_functionst( const symbolt &pure_contract_symbol, goto_modelt &goto_model, message_handlert &message_handler, dfcc_utilst &utils, dfcc_libraryt &library, - dfcc_spec_functionst &spec_functions); + dfcc_spec_functionst &spec_functions, + dfcc_contract_clauses_codegent &contract_clauses_codegen); /// Returns the contract::assigns function symbol const symbolt &get_spec_assigns_function_symbol() const; @@ -116,6 +119,7 @@ class dfcc_contract_functionst dfcc_utilst &utils; dfcc_libraryt &library; dfcc_spec_functionst &spec_functions; + dfcc_contract_clauses_codegent &contract_clauses_codegen; namespacet ns; std::size_t nof_assigns_targets; std::size_t nof_frees_targets; @@ -128,32 +132,6 @@ class dfcc_contract_functionst /// Translates the contract's frees clause to a GOTO function that uses the /// `freeable` built-in to express targets. void gen_spec_frees_function(); - - /// Generates GOTO instructions to build the representation of the given - /// conditional target group. - void encode_assignable_target_group( - const conditional_target_group_exprt &group, - goto_programt &dest); - - /// Generates GOTO instructions to build the representation of the given - /// assignable target. - void encode_assignable_target(const exprt &target, goto_programt &dest); - - /// Generates GOTO instructions to build the representation of the given - /// conditional target group. - void encode_freeable_target_group( - const conditional_target_group_exprt &group, - goto_programt &dest); - - /// Generates GOTO instructions to build the representation of the given - /// freeable target. - void encode_freeable_target(const exprt &target, goto_programt &dest); - - /// Inlines the given function and checks that the only missign functions - /// or no body functions are front-end - // void or __CPROVER_freeable_t functions, - /// and that no other warnings happened. - void inline_and_check_warnings(const irep_idt &function_id); }; #endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp index b638692a73e..be6ca1db972 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp @@ -44,7 +44,8 @@ dfcc_contract_handlert::dfcc_contract_handlert( dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates, - dfcc_spec_functionst &spec_functions) + dfcc_spec_functionst &spec_functions, + dfcc_contract_clauses_codegent &contract_clauses_codegen) : goto_model(goto_model), message_handler(message_handler), log(message_handler), @@ -53,6 +54,7 @@ dfcc_contract_handlert::dfcc_contract_handlert( instrument(instrument), memory_predicates(memory_predicates), spec_functions(spec_functions), + contract_clauses_codegen(contract_clauses_codegen), ns(goto_model.symbol_table) { } @@ -76,7 +78,8 @@ dfcc_contract_handlert::get_contract_functions(const irep_idt &contract_id) message_handler, utils, library, - spec_functions)}) + spec_functions, + contract_clauses_codegen)}) .first->second; } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h index e8c55660908..4535f00c4f4 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h @@ -31,6 +31,7 @@ class dfcc_utilst; class dfcc_instrumentt; class dfcc_lift_memory_predicatest; class dfcc_spec_functionst; +class dfcc_contract_clauses_codegent; class code_with_contract_typet; class conditional_target_group_exprt; @@ -72,7 +73,8 @@ class dfcc_contract_handlert dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates, - dfcc_spec_functionst &spec_functions); + dfcc_spec_functionst &spec_functions, + dfcc_contract_clauses_codegent &contract_clauses_codegen); /// Adds instructions in `dest` modeling contract checking, assuming /// that `ret_t wrapper_id(params)` is the function receiving @@ -122,6 +124,7 @@ class dfcc_contract_handlert dfcc_instrumentt &instrument; dfcc_lift_memory_predicatest &memory_predicates; dfcc_spec_functionst &spec_functions; + dfcc_contract_clauses_codegent &contract_clauses_codegen; namespacet ns; // Caches the functions generated from contracts 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 ea6288a162a..4a3589dba4b 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -96,16 +96,66 @@ void dfcc_spec_functionst::generate_havoc_function( dummy_havoc_function); // body will be filled with instructions - auto &body = + auto &havoc_program = goto_model.goto_functions.function_map.at(havoc_function_id).body; + const goto_programt &original_program = + goto_model.goto_functions.function_map.at(function_id).body; + + generate_havoc_instructions( + havoc_function_id, + havoc_function_symbol.mode, + havoc_function_symbol.module, + original_program, + write_set_symbol.symbol_expr(), + havoc_program, + nof_targets); + + goto_model.goto_functions.update(); + + std::set no_body; + std::set missing_function; + std::set recursive_call; + std::set not_enough_arguments; + utils.inline_function( + havoc_function_id, + no_body, + recursive_call, + missing_function, + not_enough_arguments); + INVARIANT( + no_body.empty(), + "no body warnings when inlining " + id2string(havoc_function_id)); + INVARIANT( + missing_function.empty(), + "missing function warnings when inlining " + id2string(havoc_function_id)); + INVARIANT( + recursive_call.empty(), + "recursive calls when inlining " + id2string(havoc_function_id)); + INVARIANT( + not_enough_arguments.empty(), + "not enough arguments when inlining " + id2string(havoc_function_id)); + + utils.set_hide(havoc_function_id, true); + + goto_model.goto_functions.update(); +} + +void dfcc_spec_functionst::generate_havoc_instructions( + const irep_idt &function_id, + const irep_idt &mode, + const irep_idt &module, + const goto_programt &original_program, + const exprt &write_set_to_havoc, + goto_programt &havoc_program, + std::size_t &nof_targets) +{ // index of the CAR to havoc in the write set std::size_t next_idx = 0; // iterate on the body of the original function and emit one havoc instruction // per target - Forall_goto_program_instructions( - ins_it, goto_model.goto_functions.function_map.at(function_id).body) + forall_goto_program_instructions(ins_it, original_program) { if(ins_it->is_function_call()) { @@ -121,21 +171,22 @@ void dfcc_spec_functionst::generate_havoc_function( const irep_idt &callee_id = to_symbol_expr(ins_it->call_function()).get_identifier(); - // only process built-in functions that return assignable_t, - // error out on any other function call - // find the corresponding instrumentation hook + // Only process built-in functions that represent assigns clause targets, + // and error-out on any other function call + + // Find the corresponding instrumentation hook auto hook_opt = library.get_havoc_hook(callee_id); INVARIANT( hook_opt.has_value(), - "dfcc_spec_functionst::generate_havoc_function: function calls must " - "be inlined before calling this function"); + "dfcc_spec_functionst::generate_havoc_instructions: function calls " + "must be inlined before calling this function"); // Use same source location as original call source_locationt location(ins_it->source_location()); auto hook = hook_opt.value(); code_function_callt call( library.dfcc_fun_symbol.at(hook).symbol_expr(), - {write_set_symbol.symbol_expr(), from_integer(next_idx, size_type())}); + {write_set_to_havoc, from_integer(next_idx, size_type())}); if(hook == dfcc_funt::WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET) { @@ -151,30 +202,31 @@ void dfcc_spec_functionst::generate_havoc_function( const auto &target_symbol = utils.create_symbol( pointer_type(target_type), - id2string(havoc_function_id), + id2string(function_id), "__havoc_target", location, - function_symbol.mode, - function_symbol.module, + mode, + module, false); auto target_expr = target_symbol.symbol_expr(); - body.add(goto_programt::make_decl(target_expr)); + havoc_program.add(goto_programt::make_decl(target_expr)); call.lhs() = target_expr; - body.add(goto_programt::make_function_call(call, location)); + havoc_program.add(goto_programt::make_function_call(call, location)); - auto goto_instruction = body.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(target_expr), location)); + auto goto_instruction = + havoc_program.add(goto_programt::make_incomplete_goto( + utils.make_null_check_expr(target_expr), location)); // create nondet assignment to the target side_effect_expr_nondett nondet(target_type, location); - body.add(goto_programt::make_assignment( + havoc_program.add(goto_programt::make_assignment( dereference_exprt{typecast_exprt::conditional_cast( target_expr, pointer_type(target_type))}, nondet, location)); - auto label = body.add(goto_programt::make_dead(target_expr)); + auto label = havoc_program.add(goto_programt::make_dead(target_expr)); goto_instruction->complete_goto(label); } else if( @@ -184,7 +236,7 @@ void dfcc_spec_functionst::generate_havoc_function( // ``` // CALL havoc_hook(set, next_idx); // ``` - body.add(goto_programt::make_function_call(call, location)); + havoc_program.add(goto_programt::make_function_call(call, location)); } else { @@ -192,59 +244,51 @@ void dfcc_spec_functionst::generate_havoc_function( } ++next_idx; } - nof_targets = next_idx; } + nof_targets = next_idx; + havoc_program.add(goto_programt::make_end_function()); +} - body.add(goto_programt::make_end_function()); - - goto_model.goto_functions.update(); +void dfcc_spec_functionst::to_spec_assigns_function( + const irep_idt &function_id, + std::size_t &nof_targets) +{ + auto &goto_function = goto_model.goto_functions.function_map.at(function_id); - std::set no_body; - std::set missing_function; - std::set recursive_call; - std::set not_enough_arguments; - utils.inline_function( - havoc_function_id, - no_body, - recursive_call, - missing_function, - not_enough_arguments); - INVARIANT( - no_body.empty(), - "no body warnings when inlining " + id2string(havoc_function_id)); - INVARIANT( - missing_function.empty(), - "missing function warnings when inlining " + id2string(havoc_function_id)); - INVARIANT( - recursive_call.empty(), - "recursive calls when inlining " + id2string(havoc_function_id)); - INVARIANT( - not_enough_arguments.empty(), - "not enough arguments when inlining " + id2string(havoc_function_id)); + // add write_set parameter + const exprt write_set_to_fill = + utils + .add_parameter( + function_id, + "__write_set_to_fill", + library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) + .symbol_expr(); - utils.set_hide(havoc_function_id, true); + to_spec_assigns_instructions( + write_set_to_fill, goto_function.body, nof_targets); goto_model.goto_functions.update(); + + // instrument for side-effects checking + std::set function_pointer_contracts; + instrument.instrument_function(function_id, function_pointer_contracts); + INVARIANT( + function_pointer_contracts.size() == 0, + "discovered function pointer contracts unexpectedly"); + utils.set_hide(function_id, true); } -void dfcc_spec_functionst::to_spec_assigns_function( - const irep_idt &function_id, +void dfcc_spec_functionst::to_spec_assigns_instructions( + const exprt &write_set_to_fill, + goto_programt &program, std::size_t &nof_targets) { // counts the number of calls to built-ins to get an over approximation // of the size of the set std::size_t next_idx = 0; - auto &goto_function = goto_model.goto_functions.function_map.at(function_id); - - // add write_set parameter - auto &set_symbol = utils.add_parameter( - function_id, - "__write_set_to_fill", - library.dfcc_type[dfcc_typet::WRITE_SET_PTR]); - // rewrite calls - Forall_goto_program_instructions(ins_it, goto_function.body) + Forall_goto_program_instructions(ins_it, program) { if(ins_it->is_function_call()) { @@ -252,17 +296,18 @@ void dfcc_spec_functionst::to_spec_assigns_function( { throw invalid_source_file_exceptiont( "Function pointer call '" + - from_expr(ns, function_id, ins_it->call_function()) + - "' in function '" + id2string(function_id) + "' is not supported", + from_expr(ns, "", ins_it->call_function()) + + "' are supported in assigns clauses", ins_it->source_location()); } const irep_idt &callee_id = to_symbol_expr(ins_it->call_function()).get_identifier(); - // only process built-in functions that return assignable_t, - // error out on any other function call - // find the corresponding instrumentation hook + // Only process built-in functions that specify assignable targets + // and error-out on any other function call + + // Find the corresponding instrumentation hook INVARIANT( library.is_front_end_builtin(callee_id), "dfcc_spec_functionst::to_spec_assigns_function: function calls must " @@ -276,7 +321,7 @@ void dfcc_spec_functionst::to_spec_assigns_function( ins_it->call_arguments().begin(), from_integer(next_idx, size_type())); // insert write set argument ins_it->call_arguments().insert( - ins_it->call_arguments().begin(), set_symbol.symbol_expr()); + ins_it->call_arguments().begin(), write_set_to_fill); // remove the is_pointer_to_pointer argument which is not used in the // hook for insert assignable @@ -286,8 +331,27 @@ void dfcc_spec_functionst::to_spec_assigns_function( ++next_idx; } } - nof_targets = next_idx; +} + +void dfcc_spec_functionst::to_spec_frees_function( + const irep_idt &function_id, + std::size_t &nof_targets) +{ + auto &goto_function = goto_model.goto_functions.function_map.at(function_id); + + // add __dfcc_set parameter + const exprt &write_set_to_fill = + utils + .add_parameter( + function_id, + "__write_set_to_fill", + library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) + .symbol_expr(); + + to_spec_frees_instructions( + write_set_to_fill, goto_function.body, nof_targets); + goto_model.goto_functions.update(); // instrument for side-effects checking @@ -296,24 +360,18 @@ void dfcc_spec_functionst::to_spec_assigns_function( INVARIANT( function_pointer_contracts.size() == 0, "discovered function pointer contracts unexpectedly"); + utils.set_hide(function_id, true); } -void dfcc_spec_functionst::to_spec_frees_function( - const irep_idt &function_id, +void dfcc_spec_functionst::to_spec_frees_instructions( + const exprt &write_set_to_fill, + goto_programt &program, std::size_t &nof_targets) { // counts the number of calls to the `freeable` builtin std::size_t next_idx = 0; - auto &goto_function = goto_model.goto_functions.function_map.at(function_id); - - // add __dfcc_set parameter - auto &set_symbol = utils.add_parameter( - function_id, - "__write_set_to_fill", - library.dfcc_type[dfcc_typet::WRITE_SET_PTR]); - - Forall_goto_program_instructions(ins_it, goto_function.body) + Forall_goto_program_instructions(ins_it, program) { if(ins_it->is_function_call()) { @@ -321,8 +379,8 @@ void dfcc_spec_functionst::to_spec_frees_function( { throw invalid_source_file_exceptiont( "Function pointer call '" + - from_expr(ns, function_id, ins_it->call_function()) + - "' in function '" + id2string(function_id) + "' is not supported", + from_expr(ns, "", ins_it->call_function()) + + "' are not supported in frees clauses", ins_it->source_location()); } @@ -340,20 +398,10 @@ void dfcc_spec_functionst::to_spec_frees_function( library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_FREEABLE] .symbol_expr(); ins_it->call_arguments().insert( - ins_it->call_arguments().begin(), set_symbol.symbol_expr()); + ins_it->call_arguments().begin(), write_set_to_fill); ++next_idx; } } nof_targets = next_idx; - goto_model.goto_functions.update(); - - // instrument for side-effects checking - std::set function_pointer_contracts; - instrument.instrument_function(function_id, function_pointer_contracts); - INVARIANT( - function_pointer_contracts.size() == 0, - "discovered function pointer contracts unexpectedly"); - - utils.set_hide(function_id, true); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h index 3bb843859cb..d567fb21d71 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h @@ -78,6 +78,38 @@ class dfcc_spec_functionst const irep_idt &havoc_function_id, std::size_t &nof_targets); + /// Translates \p original_program that specifies assignable targets + /// into a program that havocs the targets. + /// + /// \pre The \p original_program must be already fully inlined, and the only + /// function calls allowed are to the built-ins that specify + /// assignable targets: `__CPROVER_assignable`, `__CPROVER_object_whole`, + /// `__CPROVER_object_from`, `__CPROVER_object_upto`. + /// + /// \details The \p original_program is assumed to encode an assigns clause + /// using the built-ins `__CPROVER_assignable`, `__CPROVER_object_whole`, + /// `__CPROVER_object_from`, `__CPROVER_object_upto`. + /// The method traverses \p original_program and emits a sequence of GOTO + /// instructions in \p havoc_program that encode the havocing of the target + /// write set \p write_set_to_havoc. + /// + /// \param[in] function_id function id to use for prefixing fresh variables + /// \param[in] mode function id to use for prefixing fresh variables + /// \param[in] module 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[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 irep_idt &mode, + const irep_idt &module, + const goto_programt &original_program, + const exprt &write_set_to_havoc, + goto_programt &havoc_program, + std::size_t &nof_targets); + /// Transforms (in place) a function /// /// ``` @@ -105,6 +137,29 @@ class dfcc_spec_functionst const irep_idt &function_id, std::size_t &nof_targets); + /// Rewrites in place \p program expressed in terms of built-ins specifying + /// assignable targets declaratively using `__CPROVER_assignable`, + /// `__CPROVER_object_whole`, `__CPROVER_object_from`, + /// `__CPROVER_object_upto` into a program populating \p write_set_to_fill. + /// + /// It is the responsibility of the caller of this method to instrument the + /// resulting program against another write set instance to check them for + /// unwanted side effects. + /// + /// \pre The \p program must be already fully inlined, and the only + /// function calls allowed are to the built-ins that specify + /// assignable targets: `__CPROVER_assignable`, `__CPROVER_object_whole`, + /// `__CPROVER_object_from`, `__CPROVER_object_upto`. + /// + /// \param[in] write_set_to_fill write set to populate. + /// \param[inout] program function to transform in place + /// \param[out] nof_targets receives the estimated size of the write set + /// + void to_spec_assigns_instructions( + const exprt &write_set_to_fill, + goto_programt &program, + std::size_t &nof_targets); + /// Transforms (in place) a function /// /// ``` @@ -133,6 +188,27 @@ class dfcc_spec_functionst void to_spec_frees_function(const irep_idt &function_id, std::size_t &nof_targets); + /// Rewrites in place \p program expressed in terms of built-ins specifying + /// freeable targets declaratively using `__CPROVER_freeable` into a program + /// populating \p write_set_to_fill. + /// + /// It is the responsibility of the caller of this method to instrument the + /// resulting program against another write set instance to check them for + /// unwanted side effects. + /// + /// \pre The \p program must be already fully inlined, and the only + /// function calls allowed are to the built-ins that specify + /// freeable targets: `__CPROVER_freeable`. + /// + /// \param[in] write_set_to_fill write set to populate. + /// \param[inout] program function to transform in place + /// \param[out] nof_targets receives the estimated size of the write set + /// + void to_spec_frees_instructions( + const exprt &write_set_to_fill, + goto_programt &program, + std::size_t &nof_targets); + protected: goto_modelt &goto_model; message_handlert &message_handler; From 6c5b2a6cb8b3658181f07eac23d13a39471f9190 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 17 Feb 2023 15:26:15 +0000 Subject: [PATCH 3/5] CONTRACTS: new context tracking flags in write set Enable checking for the presence of dynamic allocations or deallocations in loop bodies and transitively in the functions called from loop bodies. - Adds `allow_allocate` and `allow_deallocate` flags in the write set struct - Modify `add_allocated` to fail an assertion when called on a write set with `allow_allocate` set to false. - Modify `check_deallocate` to return false when called on a write set with `allow_deallocate` set to false. - Don't treat replacement mode specially anymore, always store freeable targets in both the object map (for lookups) and in the append list (for inclusion checks). --- src/ansi-c/library/cprover_contracts.c | 132 ++++++++---------- .../dynamic-frames/dfcc_instrument.cpp | 11 +- .../dynamic-frames/dfcc_instrument.h | 4 +- .../contracts/dynamic-frames/dfcc_library.cpp | 1 + .../contracts/dynamic-frames/dfcc_library.h | 2 + 5 files changed, 69 insertions(+), 81 deletions(-) diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 619b3744c03..576b983fee9 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -72,7 +72,7 @@ typedef struct /// \brief Set of freeable pointers derived from the contract (indexed mode) __CPROVER_contracts_obj_set_t contract_frees; /// \brief Set of freeable pointers derived from the contract (append mode) - __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t contract_frees_append; /// \brief Set of objects allocated by the function under analysis /// (indexed mode) __CPROVER_contracts_obj_set_t allocated; @@ -83,12 +83,9 @@ typedef struct /// (indexed mode) __CPROVER_contracts_obj_set_ptr_t linked_is_fresh; /// \brief Object set recording the is_fresh allocations in post conditions - /// (replacement mode only) __CPROVER_contracts_obj_set_ptr_t linked_allocated; /// \brief Object set recording the deallocations (used by was_freed) __CPROVER_contracts_obj_set_ptr_t linked_deallocated; - /// \brief True iff this write set is used for contract replacement - __CPROVER_bool replacement; /// \brief True iff the write set checks requires clauses in an assumption ctx __CPROVER_bool assume_requires_ctx; /// \brief True iff the write set checks requires clauses in an assertion ctx @@ -97,6 +94,10 @@ typedef struct __CPROVER_bool assume_ensures_ctx; /// \brief True iff this write set checks ensures clauses in an assertion ctx __CPROVER_bool assert_ensures_ctx; + /// \brief True iff dynamic allocation is allowed (default: true) + __CPROVER_bool allow_allocate; + /// \brief True iff dynamic deallocation is allowed (default: true) + __CPROVER_bool allow_deallocate; } __CPROVER_contracts_write_set_t; /// \brief Type of pointers to \ref __CPROVER_contracts_write_set_t. @@ -388,7 +389,6 @@ __CPROVER_HIDE:; /// \param[inout] set Pointer to the object to initialise /// \param[in] contract_assigns_size Max size of the assigns clause /// \param[in] contract_frees_size Max size of the frees clause -/// \param[in] replacement True iff this write set is used to replace a contract /// \param[in] assume_requires_ctx True iff this write set is used to check side /// effects in a requires clause in contract checking mode /// \param[in] assert_requires_ctx True iff this write set is used to check side @@ -397,15 +397,20 @@ __CPROVER_HIDE:; /// side effects in an ensures clause in contract replacement mode /// \param[in] assert_ensures_ctx True iff this write set is used to check for /// side effects in an ensures clause in contract checking mode +/// \param[in] allow_allocate True iff the context gobally allows dynamic +/// allocation. +/// \param[in] allow_deallocate True iff the context gobally allows dynamic +/// deallocation. void __CPROVER_contracts_write_set_create( __CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t contract_assigns_size, __CPROVER_size_t contract_frees_size, - __CPROVER_bool replacement, __CPROVER_bool assume_requires_ctx, __CPROVER_bool assert_requires_ctx, __CPROVER_bool assume_ensures_ctx, - __CPROVER_bool assert_ensures_ctx) + __CPROVER_bool assert_ensures_ctx, + __CPROVER_bool allow_allocate, + __CPROVER_bool allow_deallocate) { __CPROVER_HIDE:; #ifdef DFCC_DEBUG @@ -417,16 +422,8 @@ __CPROVER_HIDE:; &(set->contract_assigns), contract_assigns_size); __CPROVER_contracts_obj_set_create_indexed_by_object_id( &(set->contract_frees)); - set->replacement = replacement; - if(replacement) - { - __CPROVER_contracts_obj_set_create_append( - &(set->contract_frees_replacement), contract_frees_size); - } - else - { - set->contract_frees_replacement.elems = 0; - } + __CPROVER_contracts_obj_set_create_append( + &(set->contract_frees_append), contract_frees_size); __CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->allocated)); __CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->deallocated)); set->linked_is_fresh = 0; @@ -436,6 +433,8 @@ __CPROVER_HIDE:; set->assert_requires_ctx = assert_requires_ctx; set->assume_ensures_ctx = assume_ensures_ctx; set->assert_ensures_ctx = assert_ensures_ctx; + set->allow_allocate = allow_allocate; + set->allow_deallocate = allow_deallocate; } /// \brief Releases resources used by \p set. @@ -454,9 +453,8 @@ __CPROVER_HIDE:; __CPROVER_rw_ok(&(set->contract_frees.elems), 0), "contract_frees writable"); __CPROVER_assert( - (set->replacement == 0) || - __CPROVER_rw_ok(&(set->contract_frees_replacement.elems), 0), - "contract_frees_replacement writable"); + __CPROVER_rw_ok(&(set->contract_frees_append.elems), 0), + "contract_frees_append writable"); __CPROVER_assert( __CPROVER_rw_ok(&(set->allocated.elems), 0), "allocated writable"); __CPROVER_assert( @@ -464,10 +462,7 @@ __CPROVER_HIDE:; #endif __CPROVER_deallocate(set->contract_assigns.elems); __CPROVER_deallocate(set->contract_frees.elems); - if(set->replacement != 0) - { - __CPROVER_deallocate(set->contract_frees_replacement.elems); - } + __CPROVER_deallocate(set->contract_frees_append.elems); __CPROVER_deallocate(set->allocated.elems); __CPROVER_deallocate(set->deallocated.elems); // do not free set->linked_is_fresh->elems or set->deallocated_linked->elems @@ -585,29 +580,44 @@ __CPROVER_HIDE:; // append pointer if available #ifdef DFCC_DEBUG - if(set->replacement) - __CPROVER_contracts_obj_set_append(&(set->contract_frees_replacement), ptr); + __CPROVER_contracts_obj_set_append(&(set->contract_frees_append), ptr); #else - if(set->replacement) - { - set->contract_frees_replacement.nof_elems = - set->contract_frees_replacement.watermark; - set->contract_frees_replacement - .elems[set->contract_frees_replacement.watermark] = ptr; - set->contract_frees_replacement.watermark += 1; - set->contract_frees_replacement.is_empty = 0; - } + set->contract_frees_append.nof_elems = set->contract_frees_append.watermark; + set->contract_frees_append.elems[set->contract_frees_append.watermark] = ptr; + set->contract_frees_append.watermark += 1; + set->contract_frees_append.is_empty = 0; #endif } -/// \brief Adds the pointer \p ptr to \p set->allocated. +/// \brief Adds the dynamically allocated pointer \p ptr to \p set->allocated. /// \param[inout] set The set to update -/// \param[in] ptr Pointer to an object declared using a `DECL x` or -/// `x = __CPROVER_allocate(...)` GOTO instruction. +/// \param[in] ptr Pointer to a dynamic object `x = __CPROVER_allocate(...)`. void __CPROVER_contracts_write_set_add_allocated( __CPROVER_contracts_write_set_ptr_t set, void *ptr) { +__CPROVER_HIDE:; + __CPROVER_assert(set->allow_allocate, "dynamic allocation is allowed"); +#if DFCC_DEBUG + // call inlined below + __CPROVER_contracts_obj_set_add(&(set->allocated), ptr); +#else + __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); + set->allocated.nof_elems = (set->allocated.elems[object_id] != 0) + ? set->allocated.nof_elems + : set->allocated.nof_elems + 1; + set->allocated.elems[object_id] = ptr; + set->allocated.is_empty = 0; +#endif +} + +/// \brief Adds the pointer \p ptr to \p set->allocated. +/// \param[inout] set The set to update +/// \param[in] ptr Pointer to an object declared using `DECL x`. +void __CPROVER_contracts_write_set_add_decl( + __CPROVER_contracts_write_set_ptr_t set, + void *ptr) +{ __CPROVER_HIDE:; #if DFCC_DEBUG // call inlined below @@ -659,10 +669,6 @@ void __CPROVER_contracts_write_set_record_deallocated( void *ptr) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG - __CPROVER_assert(set->replacement == 0, "!replacement"); -#endif - #if DFCC_DEBUG // we record the deallocation to be able to evaluate was_freed post conditions __CPROVER_contracts_obj_set_add(&(set->deallocated), ptr); @@ -735,7 +741,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_assignment( // manually inlined below { __CPROVER_HIDE:; - __CPROVER_assert(set->replacement == 0, "!replacement"); __CPROVER_assert( ((ptr == 0) | __CPROVER_rw_ok(ptr, size)), "ptr NULL or writable up to size"); @@ -904,16 +909,13 @@ __CPROVER_HIDE:; /// \param[in] set Write set to check the deallocation against /// \param[in] ptr Deallocated pointer to check set to check the deallocation /// against -/// \return True iff \p ptr is contained in \p set->contract_frees or -/// \p set->allocated. +/// \return True iff deallocation is allowed and \p ptr is contained in +/// \p set->contract_frees or \p set->allocated. __CPROVER_bool __CPROVER_contracts_write_set_check_deallocate( __CPROVER_contracts_write_set_ptr_t set, void *ptr) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG - __CPROVER_assert(set->replacement == 0, "!replacement"); -#endif __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); #ifdef DFCC_DEBUG @@ -924,16 +926,15 @@ __CPROVER_HIDE:; set->allocated.indexed_by_object_id, "set->allocated is indexed by object id"); #endif - return (ptr == 0) | (set->contract_frees.elems[object_id] == ptr) | - (set->allocated.elems[object_id] == ptr); + return (set->allow_deallocate) & + ((ptr == 0) | (set->contract_frees.elems[object_id] == ptr) | + (set->allocated.elems[object_id] == ptr)); } /// \brief Checks the inclusion of the \p candidate->contract_assigns elements /// in \p reference->contract_assigns or \p reference->allocated. /// -/// \pre \p reference must not be in replacement mode. -/// \pre \p candidate must be in replacement mode and \p candidate->allocated -/// must be empty. +/// \pre \p candidate->allocated must be empty. /// /// \param[in] reference Reference write set from a caller /// \param[in] candidate Candidate write set from a contract being replaced @@ -944,11 +945,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_assigns_clause_inclusion( __CPROVER_contracts_write_set_ptr_t candidate) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG - __CPROVER_assert( - reference->replacement == 0, "reference set in !replacement"); - __CPROVER_assert(candidate->replacement != 0, "candidate set in replacement"); -#endif __CPROVER_bool incl = 1; __CPROVER_contracts_car_t *current = candidate->contract_assigns.elems; __CPROVER_size_t idx = candidate->contract_assigns.max_elems; @@ -969,9 +965,7 @@ __CPROVER_HIDE:; /// \brief Checks the inclusion of the \p candidate->contract_frees elements /// in \p reference->contract_frees or \p reference->allocated. /// -/// \pre \p reference must not be in replacement mode. -/// \pre \p candidate must be in replacement mode and \p candidate->allocated -/// must be empty. +/// \pre \p candidate->allocated must be empty. /// /// \param[in] reference Reference write set from a caller /// \param[in] candidate Candidate write set from a contract being replaced @@ -983,9 +977,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_frees_clause_inclusion( { __CPROVER_HIDE:; #ifdef DFCC_DEBUG - __CPROVER_assert( - reference->replacement == 0, "reference set in !replacement"); - __CPROVER_assert(candidate->replacement != 0, "candidate set in replacement"); __CPROVER_assert( reference->contract_frees.indexed_by_object_id, "reference->contract_frees is indexed by object id"); @@ -994,8 +985,8 @@ __CPROVER_HIDE:; "reference->allocated is indexed by object id"); #endif __CPROVER_bool all_incl = 1; - void **current = candidate->contract_frees_replacement.elems; - __CPROVER_size_t idx = candidate->contract_frees_replacement.max_elems; + void **current = candidate->contract_frees_append.elems; + __CPROVER_size_t idx = candidate->contract_frees_append.max_elems; SET_CHECK_FREES_CLAUSE_INCLUSION_LOOP: while(idx != 0) @@ -1030,13 +1021,8 @@ void __CPROVER_contracts_write_set_deallocate_freeable( __CPROVER_contracts_write_set_ptr_t target) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG - __CPROVER_assert(set->replacement == 1, "set is in replacement"); - __CPROVER_assert( - (target == 0) | (target->replacement == 0), "target is in !replacement"); -#endif - void **current = set->contract_frees_replacement.elems; - __CPROVER_size_t idx = set->contract_frees_replacement.max_elems; + void **current = set->contract_frees_append.elems; + __CPROVER_size_t idx = set->contract_frees_append.max_elems; SET_DEALLOCATE_FREEABLE_LOOP: while(idx != 0) { diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index 762ed33df88..973a9c42c57 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -380,8 +380,7 @@ void dfcc_instrumentt::instrument_function_body( for(const auto &local_static : local_statics) { // automatically add local statics to the write set - insert_add_allocated_call( - function_id, write_set, local_static, begin, body); + insert_add_decl_call(function_id, write_set, local_static, begin, body); // automatically remove local statics to the write set insert_record_dead_call(function_id, write_set, local_static, end, body); @@ -510,7 +509,7 @@ bool dfcc_instrumentt::must_track_decl_or_dead( return retval; } -void dfcc_instrumentt::insert_add_allocated_call( +void dfcc_instrumentt::insert_add_decl_call( const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, @@ -523,7 +522,7 @@ void dfcc_instrumentt::insert_add_allocated_call( payload.add(goto_programt::make_function_call( code_function_callt{ - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_ALLOCATED].symbol_expr(), + library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_DECL].symbol_expr(), {write_set, address_of_exprt(symbol_expr)}}, target->source_location())); @@ -538,7 +537,7 @@ void dfcc_instrumentt::insert_add_allocated_call( /// ```c /// DECL x; /// ---- -/// insert_add_allocated_call(...); +/// insert_add_decl_call(...); /// ``` void dfcc_instrumentt::instrument_decl( const irep_idt &function_id, @@ -552,7 +551,7 @@ void dfcc_instrumentt::instrument_decl( const auto &decl_symbol = target->decl_symbol(); target++; - insert_add_allocated_call( + insert_add_decl_call( function_id, write_set, decl_symbol, target, goto_program); target--; } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h index b27af5b7e0f..0c7ec972d1a 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h @@ -175,7 +175,7 @@ class dfcc_instrumentt /// forward. /// ``` /// IF !write_set GOTO skip_target; - /// CALL __CPROVER_contracts_write_set_add_allocated(write_set, &x); + /// CALL __CPROVER_contracts_write_set_add_decl(write_set, &x); /// skip_target: SKIP; /// ``` /// \param function_id Name of the function in which the instructions is added @@ -183,7 +183,7 @@ class dfcc_instrumentt /// \param symbol_expr The symbol to add to the write set /// \param target The instruction pointer to insert at /// \param goto_program the goto_program being instrumented - void insert_add_allocated_call( + void insert_add_decl_call( const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index bc30d1ef9ff..26f295de595 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -91,6 +91,7 @@ const std::map create_dfcc_fun_to_name() CONTRACTS_PREFIX "write_set_add_freeable"}, {dfcc_funt::WRITE_SET_ADD_ALLOCATED, CONTRACTS_PREFIX "write_set_add_allocated"}, + {dfcc_funt::WRITE_SET_ADD_DECL, CONTRACTS_PREFIX "write_set_add_decl"}, {dfcc_funt::WRITE_SET_RECORD_DEAD, CONTRACTS_PREFIX "write_set_record_dead"}, {dfcc_funt::WRITE_SET_RECORD_DEALLOCATED, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h index b8ff5e5b361..23858063579 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h @@ -87,6 +87,8 @@ enum class dfcc_funt WRITE_SET_ADD_FREEABLE, /// \see __CPROVER_contracts_write_set_add_allocated WRITE_SET_ADD_ALLOCATED, + /// \see __CPROVER_contracts_write_set_add_decl + WRITE_SET_ADD_DECL, /// \see __CPROVER_contracts_write_set_record_dead WRITE_SET_RECORD_DEAD, /// \see __CPROVER_contracts_write_set_record_deallocated From da85771a49600714f7066ba81ccc775ef15a7a8b Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 17 Feb 2023 20:48:06 +0000 Subject: [PATCH 4/5] CONTRACTS: new c++ methods to build calls to cprover_contracts library --- .../dynamic-frames/dfcc_instrument.cpp | 70 ++-- .../dynamic-frames/dfcc_is_freeable.cpp | 10 +- .../contracts/dynamic-frames/dfcc_library.cpp | 309 ++++++++++++++++++ .../contracts/dynamic-frames/dfcc_library.h | 165 ++++++++++ .../dynamic-frames/dfcc_wrapper_program.cpp | 282 +++++----------- 5 files changed, 587 insertions(+), 249 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index 973a9c42c57..e9d2e03685b 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -521,9 +521,8 @@ void dfcc_instrumentt::insert_add_decl_call( utils.make_null_check_expr(write_set), target->source_location())); payload.add(goto_programt::make_function_call( - code_function_callt{ - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_DECL].symbol_expr(), - {write_set, address_of_exprt(symbol_expr)}}, + library.write_set_add_decl_call( + write_set, address_of_exprt(symbol_expr), target->source_location()), target->source_location())); auto label_instruction = @@ -569,9 +568,8 @@ void dfcc_instrumentt::insert_record_dead_call( utils.make_null_check_expr(write_set), target->source_location())); payload.add(goto_programt::make_function_call( - code_function_callt{ - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_RECORD_DEAD].symbol_expr(), - {write_set, address_of_exprt(symbol_expr)}}, + library.write_set_record_dead_call( + write_set, address_of_exprt(symbol_expr), target->source_location()), target->source_location())); auto label_instruction = @@ -716,14 +714,13 @@ void dfcc_instrumentt::instrument_lhs( payload.add(goto_programt::make_decl(check_var, lhs_source_location)); payload.add(goto_programt::make_function_call( - code_function_callt{ + library.write_set_check_assignment_call( check_var, - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_ASSIGNMENT] - .symbol_expr(), - {write_set, - typecast_exprt::conditional_cast( - address_of_exprt(lhs), pointer_type(empty_typet{})), - utils.make_sizeof_expr(lhs)}}, + write_set, + typecast_exprt::conditional_cast( + address_of_exprt(lhs), pointer_type(empty_typet{})), + utils.make_sizeof_expr(lhs), + lhs_source_location), lhs_source_location)); payload.add( @@ -810,10 +807,8 @@ void dfcc_instrumentt::instrument_assign( utils.make_null_check_expr(write_set), target_location)); payload.add(goto_programt::make_function_call( - code_function_callt{ - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_RECORD_DEALLOCATED] - .symbol_expr(), - {write_set, dead_ptr.value()}}, + library.write_set_record_dead_call( + write_set, dead_ptr.value(), target_location), target_location)); auto label_instruction = @@ -846,10 +841,7 @@ void dfcc_instrumentt::instrument_assign( utils.make_null_check_expr(write_set), target_location)); payload.add(goto_programt::make_function_call( - code_function_callt{ - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_ALLOCATED] - .symbol_expr(), - {write_set, lhs}}, + library.write_set_add_allocated_call(write_set, lhs, target_location), target_location)); auto label_instruction = @@ -987,11 +979,8 @@ void dfcc_instrumentt::instrument_deallocate_call( const auto &ptr = target->call_arguments().at(0); payload.add(goto_programt::make_function_call( - code_function_callt{ - check_var, - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_DEALLOCATE] - .symbol_expr(), - {write_set, ptr}}, + library.write_set_check_deallocate_call( + check_var, write_set, ptr, target_location), target_location)); // add property class on assertion source_location @@ -1005,10 +994,7 @@ void dfcc_instrumentt::instrument_deallocate_call( payload.add(goto_programt::make_dead(check_var, target_location)); payload.add(goto_programt::make_function_call( - code_function_callt{ - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_RECORD_DEALLOCATED] - .symbol_expr(), - {write_set, ptr}}, + library.write_set_record_deallocated_call(write_set, ptr, target_location), target_location)); auto label_instruction = @@ -1099,13 +1085,11 @@ void dfcc_instrumentt::instrument_other( const auto &dest = target->get_other().operands().at(0); - symbolt &check_fun = - library.dfcc_fun_symbol - [is_array_set ? dfcc_funt::WRITE_SET_CHECK_ARRAY_SET - : dfcc_funt::WRITE_SET_CHECK_ARRAY_COPY]; payload.add(goto_programt::make_function_call( - code_function_callt{ - check_var, check_fun.symbol_expr(), {write_set, dest}}, + is_array_set ? library.write_set_check_array_set_call( + check_var, write_set, dest, target_location) + : library.write_set_check_array_copy_call( + check_var, write_set, dest, target_location), target_location)); // add property class on assertion source_location @@ -1162,11 +1146,8 @@ void dfcc_instrumentt::instrument_other( const auto &src = target->get_other().operands().at(1); payload.add(goto_programt::make_function_call( - code_function_callt{ - check_var, - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_ARRAY_REPLACE] - .symbol_expr(), - {write_set, dest, src}}, + library.write_set_check_array_replace_call( + check_var, write_set, dest, src, target_location), target_location)); // add property class on assertion source_location @@ -1217,11 +1198,8 @@ void dfcc_instrumentt::instrument_other( const auto &ptr = target->get_other().operands().at(0); payload.add(goto_programt::make_function_call( - code_function_callt{ - check_var, - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_HAVOC_OBJECT] - .symbol_expr(), - {write_set, ptr}}, + library.write_set_check_havoc_object_call( + check_var, write_set, ptr, target_location), target_location)); // add property class on assertion source_location diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp index 099935ab0f7..b4500cf4d13 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp @@ -60,12 +60,10 @@ void dfcc_is_freeablet::rewrite_calls( { // insert call to precondition for vacuity checking auto inst = goto_programt::make_function_call( - code_function_callt{ - library - .dfcc_fun_symbol - [dfcc_funt::REPLACE_ENSURES_WAS_FREED_PRECONDITIONS] - .symbol_expr(), - {target->call_arguments().at(0), write_set}}, + library.check_replace_ensures_was_freed_preconditions_call( + target->call_arguments().at(0), + write_set, + target->source_location()), target->source_location()); program.insert_before_swap(target, inst); target++; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index 26f295de595..e57b1b5bc42 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -559,3 +559,312 @@ void dfcc_libraryt::add_instrumented_functions_map_init_instructions( } goto_model.goto_functions.update(); } + +const code_function_callt dfcc_libraryt::write_set_create_call( + const exprt &address_of_write_set, + const exprt &max_assigns_clause_size, + const exprt &max_frees_clause_size, + const exprt &assume_requires_ctx, + const exprt &assert_requires_ctx, + const exprt &assume_ensures_ctx, + const exprt &assert_ensures_ctx, + const exprt &allow_allocate, + const exprt &allow_deallocate, + const source_locationt &source_location) +{ + auto function_symbol = + dfcc_fun_symbol[dfcc_funt::WRITE_SET_CREATE].symbol_expr(); + code_function_callt call(function_symbol); + auto &arguments = call.arguments(); + // check that address_of_write_set.type() is dfcc_typet::WRITE_SET_PTR + arguments.emplace_back(address_of_write_set); + PRECONDITION(max_assigns_clause_size.type() == size_type()); + arguments.emplace_back(max_assigns_clause_size); + PRECONDITION(max_frees_clause_size.type() == size_type()); + arguments.emplace_back(max_frees_clause_size); + arguments.push_back(assume_requires_ctx); + arguments.push_back(assert_requires_ctx); + arguments.push_back(assume_ensures_ctx); + arguments.push_back(assert_ensures_ctx); + arguments.push_back(allow_allocate); + arguments.push_back(allow_deallocate); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_release_call( + const exprt &write_set_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::WRITE_SET_RELEASE].symbol_expr(), + {write_set_ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_add_allocated_call( + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_ALLOCATED].symbol_expr(), + {write_set_ptr, ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_add_decl_call( + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_DECL].symbol_expr(), + {write_set_ptr, ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_record_dead_call( + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::WRITE_SET_RECORD_DEAD].symbol_expr(), + {write_set_ptr, ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_record_deallocated_call( + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::WRITE_SET_RECORD_DEALLOCATED].symbol_expr(), + {write_set_ptr, ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt +dfcc_libraryt::write_set_check_allocated_deallocated_is_empty_call( + const exprt &check_var, + const exprt &write_set_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + check_var, + dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_ALLOCATED_DEALLOCATED_IS_EMPTY] + .symbol_expr(), + {write_set_ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_check_assignment_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &ptr, + const exprt &size, + const source_locationt &source_location) +{ + code_function_callt call( + check_var, + dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_ASSIGNMENT].symbol_expr(), + {write_set_ptr, ptr, size}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_check_array_set_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &dest, + const source_locationt &source_location) +{ + code_function_callt call( + check_var, + dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_ARRAY_SET].symbol_expr(), + {write_set_ptr, dest}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_check_array_copy_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &dest, + const source_locationt &source_location) +{ + code_function_callt call( + check_var, + dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_ARRAY_COPY].symbol_expr(), + {write_set_ptr, dest}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_check_array_replace_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &dest, + const exprt &src, + const source_locationt &source_location) +{ + code_function_callt call( + check_var, + dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_ARRAY_REPLACE].symbol_expr(), + {write_set_ptr, dest, src}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_check_havoc_object_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location) +{ + code_function_callt call( + check_var, + dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_HAVOC_OBJECT].symbol_expr(), + {write_set_ptr, ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_check_deallocate_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location) +{ + code_function_callt call( + check_var, + dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_DEALLOCATE].symbol_expr(), + {write_set_ptr, ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt +dfcc_libraryt::write_set_check_assigns_clause_inclusion_call( + const exprt &check_var, + const exprt &reference_write_set_ptr, + const exprt &candidate_write_set_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + check_var, + dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_ASSIGNS_CLAUSE_INCLUSION] + .symbol_expr(), + {reference_write_set_ptr, candidate_write_set_ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt +dfcc_libraryt::write_set_check_frees_clause_inclusion_call( + const exprt &check_var, + const exprt &reference_write_set_ptr, + const exprt &candidate_write_set_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + check_var, + dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_FREES_CLAUSE_INCLUSION] + .symbol_expr(), + {reference_write_set_ptr, candidate_write_set_ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::write_set_deallocate_freeable_call( + const exprt &write_set_ptr, + const exprt &target_write_set_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::WRITE_SET_DEALLOCATE_FREEABLE].symbol_expr(), + {write_set_ptr, target_write_set_ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::link_is_fresh_call( + const exprt &write_set_ptr, + const exprt &is_fresh_obj_set_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::LINK_IS_FRESH].symbol_expr(), + {write_set_ptr, is_fresh_obj_set_ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::link_allocated_call( + const exprt &write_set_postconditions_ptr, + const exprt &write_set_to_link_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::LINK_ALLOCATED].symbol_expr(), + {write_set_postconditions_ptr, write_set_to_link_ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::link_deallocated_call( + const exprt &write_set_postconditions_ptr, + const exprt &write_set_to_link_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::LINK_DEALLOCATED].symbol_expr(), + {write_set_postconditions_ptr, write_set_to_link_ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt +dfcc_libraryt::check_replace_ensures_was_freed_preconditions_call( + const exprt &ptr, + const exprt &write_set_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::REPLACE_ENSURES_WAS_FREED_PRECONDITIONS] + .symbol_expr(), + {ptr, write_set_ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt +dfcc_libraryt::obj_set_create_indexed_by_object_id_call( + const exprt &obj_set_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::OBJ_SET_CREATE_INDEXED_BY_OBJECT_ID] + .symbol_expr(), + {obj_set_ptr}); + call.add_source_location() = source_location; + return call; +} + +const code_function_callt dfcc_libraryt::obj_set_release_call( + const exprt &obj_set_ptr, + const source_locationt &source_location) +{ + code_function_callt call( + dfcc_fun_symbol[dfcc_funt::OBJ_SET_RELEASE].symbol_expr(), {obj_set_ptr}); + call.add_source_location() = source_location; + return call; +} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h index 23858063579..c008a54c47a 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h @@ -16,6 +16,8 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include +#include + #include #include @@ -285,6 +287,169 @@ class dfcc_libraryt const std::set &instrumented_functions, const source_locationt &source_location, goto_programt &dest); + + /// \brief Builds call to \ref __CPROVER_contracts_write_set_create + const code_function_callt write_set_create_call( + const exprt &write_set_ptr, + const exprt &contract_assigns_size, + const exprt &contract_frees_size, + const exprt &assume_requires_ctx, + const exprt &assert_requires_ctx, + const exprt &assume_ensures_ctx, + const exprt &assert_ensures_ctx, + const exprt &allow_allocate, + const exprt &allow_deallocate, + const source_locationt &source_location); + + /// \brief Builds call to \ref __CPROVER_contracts_write_set_release + const code_function_callt write_set_release_call( + const exprt &write_set_ptr, + const source_locationt &source_location); + + /// \brief Builds call to \ref __CPROVER_contracts_write_set_add_allocated + const code_function_callt write_set_add_allocated_call( + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location); + + /// \brief Builds call to \ref __CPROVER_contracts_write_set_add_decl + const code_function_callt write_set_add_decl_call( + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location); + + /// \brief Builds call to \ref __CPROVER_contracts_write_set_record_dead + const code_function_callt write_set_record_dead_call( + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_write_set_record_deallocated + const code_function_callt write_set_record_deallocated_call( + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty + const code_function_callt write_set_check_allocated_deallocated_is_empty_call( + const exprt &check_var, + const exprt &write_set_ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_write_set_check_assignment + const code_function_callt write_set_check_assignment_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &ptr, + const exprt &size, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_write_set_check_array_set + const code_function_callt write_set_check_array_set_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &dest, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_write_set_check_array_copy + const code_function_callt write_set_check_array_copy_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &dest, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_write_set_check_array_replace + const code_function_callt write_set_check_array_replace_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &dest, + const exprt &src, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_write_set_check_havoc_object + const code_function_callt write_set_check_havoc_object_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_write_set_check_deallocate + const code_function_callt write_set_check_deallocate_call( + const exprt &check_var, + const exprt &write_set_ptr, + const exprt &ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_write_set_check_assigns_clause_inclusion + const code_function_callt write_set_check_assigns_clause_inclusion_call( + const exprt &check_var, + const exprt &reference_write_set_ptr, + const exprt &candidate_write_set_ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_write_set_check_frees_clause_inclusion + const code_function_callt write_set_check_frees_clause_inclusion_call( + const exprt &check_var, + const exprt &reference_write_set_ptr, + const exprt &candidate_write_set_ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_write_set_deallocate_freeable + const code_function_callt write_set_deallocate_freeable_call( + const exprt &write_set_ptr, + const exprt &target_write_set_ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_link_is_fresh + const code_function_callt link_is_fresh_call( + const exprt &write_set_ptr, + const exprt &is_fresh_obj_set_ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_link_allocated + const code_function_callt link_allocated_call( + const exprt &write_set_postconditions_ptr, + const exprt &write_set_to_link_ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_link_deallocated + const code_function_callt link_deallocated_call( + const exprt &write_set_postconditions_ptr, + const exprt &write_set_to_link_ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_check_replace_ensures_was_freed_preconditions + const code_function_callt check_replace_ensures_was_freed_preconditions_call( + const exprt &ptr, + const exprt &write_set_ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_obj_set_create_indexed_by_object_id + const code_function_callt obj_set_create_indexed_by_object_id_call( + const exprt &obj_set_ptr, + const source_locationt &source_location); + + /// \brief Builds call to + /// \ref __CPROVER_contracts_obj_set_release + const code_function_callt obj_set_release_call( + const exprt &obj_set_ptr, + const source_locationt &source_location); }; #endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index ef258745758..8d03762e3cd 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -30,6 +30,14 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_lift_memory_predicates.h" #include "dfcc_utils.h" +/// Lift a c++ bool to an exprt +static exprt to_bool_expr(bool v) +{ + if(v) + return true_exprt(); + return false_exprt(); +} + /// Generate the contract write set const symbol_exprt create_contract_write_set( dfcc_utilst &utils, @@ -299,45 +307,18 @@ void dfcc_wrapper_programt::encode_requires_write_set() preamble.add(goto_programt::make_assignment( address_of_write_set, address_of_exprt(write_set), wrapper_sl)); - auto function_symbol = - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CREATE].symbol_expr(); - code_function_callt call(function_symbol); - auto &arguments = call.arguments(); - - // write set - arguments.emplace_back(address_of_write_set); - - // max assigns clause size - arguments.emplace_back(from_integer(0, size_type())); - - // max frees clause size - arguments.emplace_back(from_integer(0, size_type())); - - // replacement mode - arguments.push_back(false_exprt()); - - if(contract_mode == dfcc_contract_modet::CHECK) - { - // assume_requires_ctx - arguments.push_back(true_exprt()); - - // assert_requires_ctx - arguments.push_back(false_exprt()); - } - else - { - // assume_requires_ctx - arguments.push_back(false_exprt()); - - // assert_requires_ctx mode - arguments.push_back(true_exprt()); - } - - // assume_ensures_ctx mode - arguments.push_back(false_exprt()); - - // assert_ensures_ctx mode - arguments.push_back(false_exprt()); + bool check_mode = contract_mode == dfcc_contract_modet::CHECK; + code_function_callt call = library.write_set_create_call( + address_of_write_set, + from_integer(0, size_type()), + from_integer(0, size_type()), + to_bool_expr(check_mode), + to_bool_expr(!check_mode), + false_exprt(), + false_exprt(), + true_exprt(), + true_exprt(), + wrapper_sl); preamble.add(goto_programt::make_function_call(call, wrapper_sl)); @@ -360,13 +341,8 @@ void dfcc_wrapper_programt::encode_requires_write_set() postamble.add(goto_programt::make_decl(check_var, wrapper_sl)); postamble.add(goto_programt::make_function_call( - code_function_callt{ - check_var, - library - .dfcc_fun_symbol - [dfcc_funt::WRITE_SET_CHECK_ALLOCATED_DEALLOCATED_IS_EMPTY] - .symbol_expr(), - {address_of_write_set}}, + library.write_set_check_allocated_deallocated_is_empty_call( + check_var, address_of_write_set, wrapper_sl), wrapper_sl)); source_locationt check_sl(wrapper_sl); @@ -378,13 +354,10 @@ void dfcc_wrapper_programt::encode_requires_write_set() postamble.add(goto_programt::make_dead(check_var, wrapper_sl)); // generate write set release and DEAD instructions - { - code_function_callt call( - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_RELEASE].symbol_expr(), - {address_of_write_set}); - postamble.add(goto_programt::make_function_call(call, wrapper_sl)); - postamble.add(goto_programt::make_dead(write_set, wrapper_sl)); - } + postamble.add(goto_programt::make_function_call( + library.write_set_release_call(address_of_write_set, wrapper_sl), + wrapper_sl)); + postamble.add(goto_programt::make_dead(write_set, wrapper_sl)); } void dfcc_wrapper_programt::encode_ensures_write_set() @@ -393,7 +366,6 @@ void dfcc_wrapper_programt::encode_ensures_write_set() // ensures_write_set, // assigns_size = 0, // frees_size = 0, - // replacement_mode = false, // assume_requires_ctx = false, // assert_requires_ctx = false, // assume_ensures_ctx = contract_mode != check, @@ -407,59 +379,29 @@ void dfcc_wrapper_programt::encode_ensures_write_set() preamble.add(goto_programt::make_assignment( address_of_write_set, address_of_exprt(write_set), wrapper_sl)); - auto function_symbol = - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CREATE].symbol_expr(); - code_function_callt call(function_symbol); - auto &arguments = call.arguments(); - - // write set - arguments.emplace_back(address_of_write_set); + bool check_mode = contract_mode == dfcc_contract_modet::CHECK; - // max assigns clause size - arguments.emplace_back(from_integer(0, size_type())); + code_function_callt call = library.write_set_create_call( + address_of_write_set, + from_integer(0, size_type()), + from_integer(0, size_type()), + false_exprt(), + false_exprt(), + to_bool_expr(!check_mode), + to_bool_expr(check_mode), + true_exprt(), + true_exprt(), + wrapper_sl); - // max frees clause size - arguments.emplace_back(from_integer(0, size_type())); - - // replacement mode - arguments.push_back(false_exprt()); - - // assume_requires_ctx - arguments.push_back(false_exprt()); - - // assume_requires_ctx - arguments.push_back(false_exprt()); - - if(contract_mode == dfcc_contract_modet::CHECK) - { - // assume_ensures_ctx - arguments.push_back(false_exprt()); - - // assert_ensures_ctx - arguments.push_back(true_exprt()); - } - else - { - // assume_ensures_ctx - arguments.push_back(true_exprt()); - - // assert_ensures_ctx - arguments.push_back(false_exprt()); - } - - preamble.add(goto_programt::make_function_call(call)); + preamble.add(goto_programt::make_function_call(call, wrapper_sl)); // call link_allocated(pre_post, caller) if in REPLACE MODE if(contract_mode == dfcc_contract_modet::REPLACE) { - auto function_symbol = - library.dfcc_fun_symbol[dfcc_funt::LINK_ALLOCATED].symbol_expr(); - code_function_callt call(function_symbol); - auto &arguments = call.arguments(); - arguments.emplace_back(address_of_write_set); - arguments.emplace_back(caller_write_set); - link_allocated_caller.add( - goto_programt::make_function_call(call, wrapper_sl)); + link_allocated_caller.add(goto_programt::make_function_call( + library.link_allocated_call( + address_of_write_set, caller_write_set, wrapper_sl), + wrapper_sl)); } // check for absence of allocation/deallocation in contract clauses @@ -481,13 +423,8 @@ void dfcc_wrapper_programt::encode_ensures_write_set() postamble.add(goto_programt::make_decl(check_var, wrapper_sl)); postamble.add(goto_programt::make_function_call( - code_function_callt{ - check_var, - library - .dfcc_fun_symbol - [dfcc_funt::WRITE_SET_CHECK_ALLOCATED_DEALLOCATED_IS_EMPTY] - .symbol_expr(), - {address_of_write_set}}, + library.write_set_check_allocated_deallocated_is_empty_call( + check_var, address_of_write_set, wrapper_sl), wrapper_sl)); source_locationt check_sl(wrapper_sl); @@ -501,9 +438,7 @@ void dfcc_wrapper_programt::encode_ensures_write_set() // generate write set release postamble.add(goto_programt::make_function_call( - code_function_callt{ - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_RELEASE].symbol_expr(), - {address_of_write_set}}, + library.write_set_release_call(address_of_write_set, wrapper_sl), wrapper_sl)); // declare write set DEAD @@ -527,43 +462,18 @@ void dfcc_wrapper_programt::encode_contract_write_set() // call write_set_create { - auto function_symbol = - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CREATE].symbol_expr(); - - code_function_callt call(function_symbol); - auto &arguments = call.arguments(); - - // write set - arguments.emplace_back(address_of_contract_write_set); - - // max assigns clause size - arguments.emplace_back( - from_integer(contract_functions.get_nof_assigns_targets(), size_type())); - - // max frees clause size - arguments.emplace_back( - from_integer(contract_functions.get_nof_frees_targets(), size_type())); - - // activate replace mode - const bool replace = contract_mode == dfcc_contract_modet::REPLACE; - arguments.emplace_back( - (replace ? (exprt)true_exprt() : (exprt)false_exprt())); - - // not analysing ensures or requires clauses, set all context flags to false - - // assume_requires_ctx - arguments.push_back(false_exprt()); - - // assert_requires_ctx - arguments.push_back(false_exprt()); - - // assume_ensures_ctx - arguments.push_back(false_exprt()); - - // assert_ensures_ctx - arguments.push_back(false_exprt()); - - write_set_checks.add(goto_programt::make_function_call(call)); + code_function_callt call = library.write_set_create_call( + address_of_contract_write_set, + from_integer(contract_functions.get_nof_assigns_targets(), size_type()), + from_integer(contract_functions.get_nof_frees_targets(), size_type()), + false_exprt(), + false_exprt(), + false_exprt(), + false_exprt(), + true_exprt(), + true_exprt(), + wrapper_sl); + write_set_checks.add(goto_programt::make_function_call(call, wrapper_sl)); } // build arguments for assigns and frees clauses functions @@ -615,13 +525,10 @@ void dfcc_wrapper_programt::encode_contract_write_set() } // generate write set release and DEAD instructions - { - code_function_callt call( - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_RELEASE].symbol_expr(), - {address_of_contract_write_set}); - postamble.add(goto_programt::make_function_call(call, wrapper_sl)); - postamble.add(goto_programt::make_dead(write_set, wrapper_sl)); - } + postamble.add(goto_programt::make_function_call( + library.write_set_release_call(address_of_contract_write_set, wrapper_sl), + wrapper_sl)); + postamble.add(goto_programt::make_dead(write_set, wrapper_sl)); } void dfcc_wrapper_programt::encode_is_fresh_set() @@ -636,31 +543,25 @@ void dfcc_wrapper_programt::encode_is_fresh_set() // CALL obj_set_create_indexed_by_object_id(is_fresh_set) in preamble preamble.add(goto_programt::make_function_call( - code_function_callt{ - library.dfcc_fun_symbol[dfcc_funt::OBJ_SET_CREATE_INDEXED_BY_OBJECT_ID] - .symbol_expr(), - {address_of_object_set}}, + library.obj_set_create_indexed_by_object_id_call( + address_of_object_set, wrapper_sl), wrapper_sl)); // link to requires write set link_is_fresh.add(goto_programt::make_function_call( - code_function_callt( - library.dfcc_fun_symbol[dfcc_funt::LINK_IS_FRESH].symbol_expr(), - {addr_of_requires_write_set, address_of_object_set}), + library.link_is_fresh_call( + addr_of_requires_write_set, address_of_object_set, wrapper_sl), wrapper_sl)); // link to ensures write set link_is_fresh.add(goto_programt::make_function_call( - code_function_callt( - library.dfcc_fun_symbol[dfcc_funt::LINK_IS_FRESH].symbol_expr(), - {addr_of_ensures_write_set, address_of_object_set}), + library.link_is_fresh_call( + addr_of_ensures_write_set, address_of_object_set, wrapper_sl), wrapper_sl)); // release call in postamble postamble.add(goto_programt::make_function_call( - code_function_callt( - library.dfcc_fun_symbol[dfcc_funt::OBJ_SET_RELEASE].symbol_expr(), - {address_of_object_set}), + library.obj_set_release_call(address_of_object_set, wrapper_sl), wrapper_sl)); // DEAD instructions in postamble @@ -764,13 +665,10 @@ void dfcc_wrapper_programt::encode_ensures_clauses() // When checking an ensures clause we link the contract write set to the // ensures write set to know what was deallocated by the function so that // the was_freed predicate can perform its checks - code_function_callt call( - library.dfcc_fun_symbol[dfcc_funt::LINK_DEALLOCATED].symbol_expr()); - auto &arguments = call.arguments(); - arguments.emplace_back(address_of_ensures_write_set); - arguments.emplace_back(addr_of_contract_write_set); - link_deallocated_contract.add( - goto_programt::make_function_call(call, wrapper_sl)); + link_deallocated_contract.add(goto_programt::make_function_call( + library.link_deallocated_call( + address_of_ensures_write_set, addr_of_contract_write_set, wrapper_sl), + wrapper_sl)); // fix calls to user-defined user-defined memory predicates memory_predicates.fix_calls(ensures_program); @@ -876,15 +774,11 @@ void dfcc_wrapper_programt::encode_havoced_function_call() write_set_checks.add(goto_programt::make_decl(check_var, wrapper_sl)); - code_function_callt check_incl_call( - check_var, - library - .dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_ASSIGNS_CLAUSE_INCLUSION] - .symbol_expr(), - {caller_write_set, address_of_contract_write_set}); + write_set_checks.add(goto_programt::make_function_call( + library.write_set_check_assigns_clause_inclusion_call( + check_var, caller_write_set, address_of_contract_write_set, wrapper_sl), + wrapper_sl)); - write_set_checks.add( - goto_programt::make_function_call(check_incl_call, wrapper_sl)); source_locationt check_sl(wrapper_sl); check_sl.set_function(wrapper_symbol.name); check_sl.set_property_class("assigns"); @@ -908,14 +802,10 @@ void dfcc_wrapper_programt::encode_havoced_function_call() write_set_checks.add(goto_programt::make_decl(check_var, wrapper_sl)); - code_function_callt check_incl_call( - check_var, - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_CHECK_FREES_CLAUSE_INCLUSION] - .symbol_expr(), - {caller_write_set, address_of_contract_write_set}); - - write_set_checks.add( - goto_programt::make_function_call(check_incl_call, wrapper_sl)); + write_set_checks.add(goto_programt::make_function_call( + library.write_set_check_frees_clause_inclusion_call( + check_var, caller_write_set, address_of_contract_write_set, wrapper_sl), + wrapper_sl)); source_locationt check_sl(wrapper_sl); check_sl.set_function(wrapper_symbol.name); @@ -960,10 +850,8 @@ void dfcc_wrapper_programt::encode_havoced_function_call() // nondet free the freeable set, record effects in both the contract write // set and the caller write set - code_function_callt deallocate_call( - library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_DEALLOCATE_FREEABLE] - .symbol_expr(), - {address_of_contract_write_set, caller_write_set}); - function_call.add( - goto_programt::make_function_call(deallocate_call, wrapper_sl)); + function_call.add(goto_programt::make_function_call( + library.write_set_deallocate_freeable_call( + address_of_contract_write_set, caller_write_set, wrapper_sl), + wrapper_sl)); } From fb35a173984d1cf25de3ecb37890e73c82593c01 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 22 Feb 2023 16:23:28 +0000 Subject: [PATCH 5/5] address review comments --- .../contracts/dynamic-frames/dfcc.cpp | 4 +-- .../dfcc_contract_clauses_codegen.cpp | 19 +++++------ .../dynamic-frames/dfcc_spec_functions.cpp | 32 ++++++++++++------- .../dynamic-frames/dfcc_spec_functions.h | 4 +++ .../dynamic-frames/dfcc_wrapper_program.cpp | 16 +++------- 5 files changed, 40 insertions(+), 35 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index 68a6b3e10f2..e6bdc72b1e8 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -92,14 +92,14 @@ parse_function_contract_pair(const irep_idt &cli_flag) else if(split.size() == 2) { auto function_name = split[0]; - if(function_name.size() == 0) + if(function_name.empty()) { throw invalid_function_contract_pair_exceptiont{ "couldn't find function name before '/' in '" + cli_flag_str + "'", correct_format_message}; } auto contract_name = split[1]; - if(contract_name.size() == 0) + if(contract_name.empty()) { throw invalid_function_contract_pair_exceptiont{ "couldn't find contract name after '/' in '" + cli_flag_str + "'", diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp index 99f4bf888d5..27f8d96977e 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp @@ -49,10 +49,11 @@ void dfcc_contract_clauses_codegent::gen_spec_assigns_instructions( { for(const auto &expr : assigns_clause) { - if(can_cast_expr(expr)) + if( + auto target_group = + expr_try_dynamic_cast(expr)) { - encode_assignable_target_group( - language_mode, to_conditional_target_group_expr(expr), dest); + encode_assignable_target_group(language_mode, *target_group, dest); } else { @@ -75,10 +76,11 @@ void dfcc_contract_clauses_codegent::gen_spec_frees_instructions( { for(const auto &expr : frees_clause) { - if(can_cast_expr(expr)) + if( + auto target_group = + expr_try_dynamic_cast(expr)) { - encode_freeable_target_group( - language_mode, to_conditional_target_group_expr(expr), dest); + encode_freeable_target_group(language_mode, *target_group, dest); } else { @@ -279,10 +281,9 @@ void dfcc_contract_clauses_codegent::inline_and_check_warnings( } INVARIANT( - recursive_call.size() == 0, - "recursive calls found when inlining goto program"); + recursive_call.empty(), "recursive calls found when inlining goto program"); INVARIANT( - not_enough_arguments.size() == 0, + not_enough_arguments.empty(), "not enough arguments when inlining goto program"); } 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 4a3589dba4b..d24f568a682 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -162,9 +162,9 @@ void dfcc_spec_functionst::generate_havoc_instructions( if(ins_it->call_function().id() != ID_symbol) { throw invalid_source_file_exceptiont( - "Function pointer call '" + + "Function pointer calls are not supported in assigns clauses: '" + from_expr(ns, function_id, ins_it->call_function()) + - "' in function '" + id2string(function_id) + "' is not supported", + "' called in function '" + id2string(function_id) + "'", ins_it->source_location()); } @@ -265,7 +265,10 @@ void dfcc_spec_functionst::to_spec_assigns_function( .symbol_expr(); to_spec_assigns_instructions( - write_set_to_fill, goto_function.body, nof_targets); + write_set_to_fill, + utils.get_function_symbol(function_id).mode, + goto_function.body, + nof_targets); goto_model.goto_functions.update(); @@ -273,13 +276,14 @@ void dfcc_spec_functionst::to_spec_assigns_function( std::set function_pointer_contracts; instrument.instrument_function(function_id, function_pointer_contracts); INVARIANT( - function_pointer_contracts.size() == 0, + function_pointer_contracts.empty(), "discovered function pointer contracts unexpectedly"); utils.set_hide(function_id, true); } void dfcc_spec_functionst::to_spec_assigns_instructions( const exprt &write_set_to_fill, + const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets) { @@ -295,9 +299,9 @@ void dfcc_spec_functionst::to_spec_assigns_instructions( if(ins_it->call_function().id() != ID_symbol) { throw invalid_source_file_exceptiont( - "Function pointer call '" + - from_expr(ns, "", ins_it->call_function()) + - "' are supported in assigns clauses", + "Function pointer calls are not supported in assigns clauses '" + + from_expr_using_mode(ns, language_mode, ins_it->call_function()) + + "'", ins_it->source_location()); } @@ -350,7 +354,10 @@ void dfcc_spec_functionst::to_spec_frees_function( .symbol_expr(); to_spec_frees_instructions( - write_set_to_fill, goto_function.body, nof_targets); + write_set_to_fill, + utils.get_function_symbol(function_id).mode, + goto_function.body, + nof_targets); goto_model.goto_functions.update(); @@ -358,7 +365,7 @@ void dfcc_spec_functionst::to_spec_frees_function( std::set function_pointer_contracts; instrument.instrument_function(function_id, function_pointer_contracts); INVARIANT( - function_pointer_contracts.size() == 0, + function_pointer_contracts.empty(), "discovered function pointer contracts unexpectedly"); utils.set_hide(function_id, true); @@ -366,6 +373,7 @@ void dfcc_spec_functionst::to_spec_frees_function( void dfcc_spec_functionst::to_spec_frees_instructions( const exprt &write_set_to_fill, + const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets) { @@ -378,9 +386,9 @@ void dfcc_spec_functionst::to_spec_frees_instructions( if(ins_it->call_function().id() != ID_symbol) { throw invalid_source_file_exceptiont( - "Function pointer call '" + - from_expr(ns, "", ins_it->call_function()) + - "' are not supported in frees clauses", + "Function pointer calls are not supported in frees clauses: '" + + from_expr_using_mode(ns, language_mode, ins_it->call_function()) + + "'", ins_it->source_location()); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h index d567fb21d71..6e12be814d0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h @@ -152,11 +152,13 @@ class dfcc_spec_functionst /// `__CPROVER_object_from`, `__CPROVER_object_upto`. /// /// \param[in] write_set_to_fill write set to populate. + /// \param[in] language_mode used to format expressions. /// \param[inout] program function to transform in place /// \param[out] nof_targets receives the estimated size of the write set /// void to_spec_assigns_instructions( const exprt &write_set_to_fill, + const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets); @@ -201,11 +203,13 @@ class dfcc_spec_functionst /// freeable targets: `__CPROVER_freeable`. /// /// \param[in] write_set_to_fill write set to populate. + /// \param[in] language_mode used to format expressions. /// \param[inout] program function to transform in place /// \param[out] nof_targets receives the estimated size of the write set /// void to_spec_frees_instructions( const exprt &write_set_to_fill, + const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index 8d03762e3cd..a44bdbfa23f 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -30,14 +30,6 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_lift_memory_predicates.h" #include "dfcc_utils.h" -/// Lift a c++ bool to an exprt -static exprt to_bool_expr(bool v) -{ - if(v) - return true_exprt(); - return false_exprt(); -} - /// Generate the contract write set const symbol_exprt create_contract_write_set( dfcc_utilst &utils, @@ -312,8 +304,8 @@ void dfcc_wrapper_programt::encode_requires_write_set() address_of_write_set, from_integer(0, size_type()), from_integer(0, size_type()), - to_bool_expr(check_mode), - to_bool_expr(!check_mode), + make_boolean_expr(check_mode), + make_boolean_expr(!check_mode), false_exprt(), false_exprt(), true_exprt(), @@ -387,8 +379,8 @@ void dfcc_wrapper_programt::encode_ensures_write_set() from_integer(0, size_type()), false_exprt(), false_exprt(), - to_bool_expr(!check_mode), - to_bool_expr(check_mode), + make_boolean_expr(!check_mode), + make_boolean_expr(check_mode), true_exprt(), true_exprt(), wrapper_sl);