From 260b0bf86e3376475a97d373326825303dae7ec4 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 16 Jul 2021 16:57:29 +0000 Subject: [PATCH 1/6] Adds a memory predicate moddule in contracts Signed-off-by: Felipe R. Monteiro --- .../contracts/assigns_replace_06/test.desc | 4 +- src/goto-instrument/Makefile | 1 + src/goto-instrument/code_contracts.cpp | 385 +----------------- src/goto-instrument/code_contracts.h | 186 ++------- .../contracts_memory_predicates.cpp | 360 ++++++++++++++++ .../contracts_memory_predicates.h | 159 ++++++++ 6 files changed, 560 insertions(+), 535 deletions(-) create mode 100644 src/goto-instrument/contracts_memory_predicates.cpp create mode 100644 src/goto-instrument/contracts_memory_predicates.h diff --git a/regression/contracts/assigns_replace_06/test.desc b/regression/contracts/assigns_replace_06/test.desc index 13d942ed25e..e34e91e28f0 100644 --- a/regression/contracts/assigns_replace_06/test.desc +++ b/regression/contracts/assigns_replace_06/test.desc @@ -1,9 +1,9 @@ CORE main.c --replace-all-calls-with-contracts -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ -- -- Checks whether the values outside the array range specified by the assigns diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 8cd5b3936b9..e5edc810bbe 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -17,6 +17,7 @@ SRC = accelerate/accelerate.cpp \ branch.cpp \ call_sequences.cpp \ code_contracts.cpp \ + contracts_memory_predicates.cpp \ concurrency.cpp \ count_eloc.cpp \ cover.cpp \ diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 16fa9ffad95..91738a42d9b 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -11,24 +11,21 @@ Date: February 2016 /// \file /// Verify and use annotated invariants and pre/post-conditions -#include "code_contracts.h" +#include "contracts_memory_predicates.h" #include #include #include -#include #include -#include -#include +#include -#include +#include #include #include -#include #include #include #include @@ -36,73 +33,8 @@ Date: February 2016 #include #include #include -#include #include -bool return_value_visitort::found_return_value() -{ - return found; -} - -void return_value_visitort::operator()(const exprt &exp) -{ - if(exp.id() != ID_symbol) - return; - const symbol_exprt &sym = to_symbol_expr(exp); - found |= sym.get_identifier() == CPROVER_PREFIX "return_value"; -} - -std::set &functions_in_scope_visitort::function_calls() -{ - return function_set; -} - -void functions_in_scope_visitort::operator()(const goto_programt &prog) -{ - forall_goto_program_instructions(ins, prog) - { - if(ins->is_function_call()) - { - const code_function_callt &call = ins->get_function_call(); - - if(call.function().id() != ID_symbol) - { - log.error().source_location = call.find_source_location(); - log.error() << "Function pointer used in function invoked by " - "function contract: " - << messaget::eom; - throw 0; - } - else - { - const irep_idt &fun_name = - to_symbol_expr(call.function()).get_identifier(); - if(function_set.find(fun_name) == function_set.end()) - { - function_set.insert(fun_name); - auto called_fun = goto_functions.function_map.find(fun_name); - if(called_fun == goto_functions.function_map.end()) - { - log.warning() << "Could not find function '" << fun_name - << "' in goto-program." << messaget::eom; - throw 0; - } - if(called_fun->second.body_available()) - { - const goto_programt &program = called_fun->second.body; - (*this)(program); - } - else - { - log.warning() << "No body for function: " << fun_name - << "invoked from function contract." << messaget::eom; - } - } - } - } - } -} - exprt get_size(const typet &type, const namespacet &ns, messaget &log) { auto size_of_opt = size_of_expr(type, ns); @@ -1763,30 +1695,16 @@ assigns_clauset::~assigns_clauset() assigns_clause_targett *assigns_clauset::add_target(exprt current_operation) { - if(current_operation.id() == ID_address_of) - { - assigns_clause_array_targett *array_target = - new assigns_clause_array_targett( - current_operation, parent, log, function_id); - targets.push_back(array_target); - return array_target; - } - else if(current_operation.type().id() == ID_struct_tag) - { - assigns_clause_struct_targett *struct_target = - new assigns_clause_struct_targett( - current_operation, parent, log, function_id); - targets.push_back(struct_target); - return struct_target; - } - else - { - assigns_clause_scalar_targett *scalar_target = - new assigns_clause_scalar_targett( - current_operation, parent, log, function_id); - targets.push_back(scalar_target); - return scalar_target; - } + assigns_clause_scalar_targett *scalar_target = + new assigns_clause_scalar_targett( + (current_operation.id() == ID_address_of) + ? to_index_expr(to_address_of_expr(current_operation).object()).array() + : current_operation, + parent, + log, + function_id); + targets.push_back(scalar_target); + return scalar_target; } assigns_clause_targett * @@ -1867,6 +1785,7 @@ goto_programt assigns_clauset::havoc_code( goto_programt::targett z = tmp_z.add(goto_programt::make_skip(location)); const auto &target_ptr = target->get_direct_pointer(); + if(to_address_of_expr(target_ptr).object().id() == ID_dereference) { // create the condition @@ -1981,278 +1900,4 @@ exprt assigns_clauset::compatible_expression( } return result; -} - -std::set &find_is_fresh_calls_visitort::is_fresh_calls() -{ - return function_set; -} - -void find_is_fresh_calls_visitort::clear_set() -{ - function_set.clear(); -} - -void find_is_fresh_calls_visitort::operator()(goto_programt &prog) -{ - Forall_goto_program_instructions(ins, prog) - { - if(ins->is_function_call()) - { - const code_function_callt &call = ins->get_function_call(); - - if(call.function().id() == ID_symbol) - { - const irep_idt &fun_name = - to_symbol_expr(call.function()).get_identifier(); - - if(fun_name == (CPROVER_PREFIX + std::string("is_fresh"))) - { - function_set.insert(ins); - } - } - } - } -} - -void is_fresh_baset::update_requires(goto_programt &requires) -{ - find_is_fresh_calls_visitort requires_visitor; - requires_visitor(requires); - for(auto it : requires_visitor.is_fresh_calls()) - { - create_requires_fn_call(it); - } -} - -void is_fresh_baset::update_ensures(goto_programt &ensures) -{ - find_is_fresh_calls_visitort ensures_visitor; - ensures_visitor(ensures); - for(auto it : ensures_visitor.is_fresh_calls()) - { - create_ensures_fn_call(it); - } -} - -// -// -// Code largely copied from model_argc_argv.cpp -// -// - -void is_fresh_baset::add_declarations(const std::string &decl_string) -{ - log.debug() << "Creating declarations: \n" << decl_string << "\n"; - - std::istringstream iss(decl_string); - - ansi_c_languaget ansi_c_language; - ansi_c_language.set_message_handler(log.get_message_handler()); - configt::ansi_ct::preprocessort pp = config.ansi_c.preprocessor; - config.ansi_c.preprocessor = configt::ansi_ct::preprocessort::NONE; - ansi_c_language.parse(iss, ""); - config.ansi_c.preprocessor = pp; - - symbol_tablet tmp_symbol_table; - ansi_c_language.typecheck(tmp_symbol_table, ""); - exprt value = nil_exprt(); - - goto_functionst tmp_functions; - - // Add the new functions into the goto functions table. - parent.get_goto_functions().function_map[ensures_fn_name].copy_from( - tmp_functions.function_map[ensures_fn_name]); - - parent.get_goto_functions().function_map[requires_fn_name].copy_from( - tmp_functions.function_map[requires_fn_name]); - - for(const auto &symbol_pair : tmp_symbol_table.symbols) - { - if( - symbol_pair.first == memmap_name || - symbol_pair.first == ensures_fn_name || - symbol_pair.first == requires_fn_name || symbol_pair.first == "malloc") - { - this->parent.get_symbol_table().insert(symbol_pair.second); - } - // Parameters are stored as scoped names in the symbol table. - else if( - (has_prefix( - id2string(symbol_pair.first), id2string(ensures_fn_name) + "::") || - has_prefix( - id2string(symbol_pair.first), id2string(requires_fn_name) + "::")) && - parent.get_symbol_table().add(symbol_pair.second)) - { - UNREACHABLE; - } - } - - // We have to set the global memory map array to - // all zeros for this to work properly - const array_typet ty = - to_array_type(tmp_symbol_table.lookup_ref(memmap_name).type); - constant_exprt initial_value(irep_idt(dstringt("0")), ty.subtype()); - array_of_exprt memmap_init(initial_value, ty); - goto_programt::instructiont a = - goto_programt::make_assignment(symbol_exprt(memmap_name, ty), memmap_init); - - // insert the assignment into the initialize function. - auto called_func = - parent.get_goto_functions().function_map.find(INITIALIZE_FUNCTION); - goto_programt &body = called_func->second.body; - auto target = body.get_end_function(); - body.insert_before(target, a); -} - -void is_fresh_baset::update_fn_call( - goto_programt::targett &ins, - const std::string &fn_name, - bool add_address_of) -{ - const code_function_callt &const_call = ins->get_function_call(); - code_function_callt call( - exprt(const_call.lhs()), - exprt(const_call.function()), - code_function_callt::argumentst(const_call.arguments())); - - // adjusting the expression for the first argument, if required - if(add_address_of) - { - INVARIANT(call.arguments().size() > 0, "Function must have arguments"); - call.arguments()[0] = address_of_exprt(call.arguments()[0]); - } - - // fixing the function name. - to_symbol_expr(call.function()).set_identifier(fn_name); - log.debug() << "printing updated call expression: " - << expr2c(call, parent.get_namespace()) << "\n"; - - ins->set_function_call(call); -} - -/* Declarations for contract enforcement */ - -is_fresh_enforcet::is_fresh_enforcet( - code_contractst &_parent, - messaget _log, - irep_idt _fun_id) - : is_fresh_baset(_parent, _log, _fun_id) -{ - std::stringstream ssreq, ssensure, ssmemmap; - ssreq << CPROVER_PREFIX << fun_id << "_requires_is_fresh"; - this->requires_fn_name = ssreq.str(); - - ssensure << CPROVER_PREFIX << fun_id << "_ensures_is_fresh"; - this->ensures_fn_name = ssensure.str(); - - ssmemmap << CPROVER_PREFIX << fun_id << "_memory_map"; - this->memmap_name = ssmemmap.str(); -} - -void is_fresh_enforcet::create_declarations() -{ - std::ostringstream oss; - std::string cprover_prefix(CPROVER_PREFIX); - oss << "static _Bool " << memmap_name - << "[" + cprover_prefix + "constant_infinity_uint]; \n" - << "\n" - << "_Bool " << requires_fn_name - << "(void **elem, " + cprover_prefix + "size_t size) { \n" - << " *elem = malloc(size); \n" - << " if (!*elem || " << memmap_name - << "[" + cprover_prefix + "POINTER_OBJECT(*elem)]) return 0; \n" - << " " << memmap_name << "[" + cprover_prefix - << "POINTER_OBJECT(*elem)] = 1; \n" - << " return 1; \n" - << "} \n" - << "\n" - << "_Bool " << ensures_fn_name - << "(void *elem, " + cprover_prefix + "size_t size) { \n" - << " _Bool ok = (!" << memmap_name - << "[" + cprover_prefix + "POINTER_OBJECT(elem)] && " - << cprover_prefix + "r_ok(elem, size)); \n" - << " " << memmap_name << "[" + cprover_prefix - << "POINTER_OBJECT(elem)] = 1; \n" - << " return ok; \n" - << "}"; - - add_declarations(oss.str()); -} - -void is_fresh_enforcet::create_requires_fn_call(goto_programt::targett &ins) -{ - update_fn_call(ins, requires_fn_name, true); -} - -void is_fresh_enforcet::create_ensures_fn_call(goto_programt::targett &ins) -{ - update_fn_call(ins, ensures_fn_name, false); -} - -/* Declarations for contract replacement: note that there may be several - instances of the same function called in a particular context, so care must be taken - that the 'call' functions and global data structure are unique for each instance. - This is why we check that the symbols are unique for each such declaration. */ - -std::string unique_symbol(const symbol_tablet &tbl, const std::string &original) -{ - auto size = tbl.next_unused_suffix(original); - return original + std::to_string(size); -} - -is_fresh_replacet::is_fresh_replacet( - code_contractst &_parent, - messaget _log, - irep_idt _fun_id) - : is_fresh_baset(_parent, _log, _fun_id) -{ - std::stringstream ssreq, ssensure, ssmemmap; - ssreq /* << CPROVER_PREFIX */ << fun_id << "_call_requires_is_fresh"; - this->requires_fn_name = - unique_symbol(parent.get_symbol_table(), ssreq.str()); - - ssensure /* << CPROVER_PREFIX */ << fun_id << "_call_ensures_is_fresh"; - this->ensures_fn_name = - unique_symbol(parent.get_symbol_table(), ssensure.str()); - - ssmemmap /* << CPROVER_PREFIX */ << fun_id << "_memory_map"; - this->memmap_name = unique_symbol(parent.get_symbol_table(), ssmemmap.str()); -} - -void is_fresh_replacet::create_declarations() -{ - std::ostringstream oss; - std::string cprover_prefix(CPROVER_PREFIX); - oss << "static _Bool " << memmap_name - << "[" + cprover_prefix + "constant_infinity_uint]; \n" - << "\n" - << "static _Bool " << requires_fn_name - << "(void *elem, " + cprover_prefix + "size_t size) { \n" - << " _Bool r_ok = " + cprover_prefix + "r_ok(elem, size); \n" - << " if (" << memmap_name - << "[" + cprover_prefix + "POINTER_OBJECT(elem)]" - << " != 0 || !r_ok) return 0; \n" - << " " << memmap_name << "[" - << cprover_prefix + "POINTER_OBJECT(elem)] = 1; \n" - << " return 1; \n" - << "} \n" - << " \n" - << "_Bool " << ensures_fn_name - << "(void **elem, " + cprover_prefix + "size_t size) { \n" - << " *elem = malloc(size); \n" - << " return (*elem != 0); \n" - << "} \n"; - - add_declarations(oss.str()); -} - -void is_fresh_replacet::create_requires_fn_call(goto_programt::targett &ins) -{ - update_fn_call(ins, requires_fn_name, false); -} - -void is_fresh_replacet::create_ensures_fn_call(goto_programt::targett &ins) -{ - update_fn_call(ins, ensures_fn_name, true); -} +} \ No newline at end of file diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 0137613a0d4..4687ad469fb 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -31,6 +31,29 @@ Date: February 2016 #include "loop_utils.h" +#define FLAG_LOOP_CONTRACTS "apply-loop-contracts" +#define HELP_LOOP_CONTRACTS \ + " --apply-loop-contracts\n" \ + " check and use loop contracts when provided\n" + +#define FLAG_REPLACE_CALL "replace-call-with-contract" +#define HELP_REPLACE_CALL \ + " --replace-call-with-contract \n" \ + " replace calls to fun with fun's contract\n" + +#define FLAG_REPLACE_ALL_CALLS "replace-all-calls-with-contracts" +#define HELP_REPLACE_ALL_CALLS \ + " --replace-all-calls-with-contracts\n" \ + " as above for all functions with a contract\n" + +#define FLAG_ENFORCE_CONTRACT "enforce-contract" +#define HELP_ENFORCE_CONTRACT \ + " --enforce-contract wrap fun with an assertion of its contract\n" + +#define FLAG_ENFORCE_ALL_CONTRACTS "enforce-all-contracts" +#define HELP_ENFORCE_ALL_CONTRACTS \ + " --enforce-all-contracts as above for all functions with a contract\n" + class assigns_clauset; class local_may_aliast; class replace_symbolt; @@ -220,29 +243,6 @@ class code_contractst const irep_idt &mode); }; -#define FLAG_LOOP_CONTRACTS "apply-loop-contracts" -#define HELP_LOOP_CONTRACTS \ - " --apply-loop-contracts\n" \ - " check and use loop contracts when provided\n" - -#define FLAG_REPLACE_CALL "replace-call-with-contract" -#define HELP_REPLACE_CALL \ - " --replace-call-with-contract \n" \ - " replace calls to fun with fun's contract\n" - -#define FLAG_REPLACE_ALL_CALLS "replace-all-calls-with-contracts" -#define HELP_REPLACE_ALL_CALLS \ - " --replace-all-calls-with-contracts\n" \ - " as above for all functions with a contract\n" - -#define FLAG_ENFORCE_CONTRACT "enforce-contract" -#define HELP_ENFORCE_CONTRACT \ - " --enforce-contract wrap fun with an assertion of its contract\n" - -#define FLAG_ENFORCE_ALL_CONTRACTS "enforce-all-contracts" -#define HELP_ENFORCE_ALL_CONTRACTS \ - " --enforce-all-contracts as above for all functions with a contract\n" - /// \brief A base class for assigns clause targets class assigns_clause_targett { @@ -407,144 +407,4 @@ class assigns_clauset messaget log; }; -class is_fresh_baset -{ -public: - is_fresh_baset( - code_contractst &_parent, - messaget _log, - const irep_idt _fun_id) - : parent(_parent), log(_log), fun_id(_fun_id) - { - } - - void update_requires(goto_programt &requires); - void update_ensures(goto_programt &ensures); - - virtual void create_declarations() = 0; - -protected: - void add_declarations(const std::string &decl_string); - void update_fn_call( - goto_programt::targett &target, - const std::string &name, - bool add_address_of); - - virtual void create_requires_fn_call(goto_programt::targett &target) = 0; - virtual void create_ensures_fn_call(goto_programt::targett &target) = 0; - - code_contractst &parent; - messaget log; - irep_idt fun_id; - - // written by the child classes. - std::string memmap_name; - std::string requires_fn_name; - std::string ensures_fn_name; -}; - -class is_fresh_enforcet : public is_fresh_baset -{ -public: - is_fresh_enforcet( - code_contractst &_parent, - messaget _log, - const irep_idt _fun_id); - - virtual void create_declarations(); - -protected: - virtual void create_requires_fn_call(goto_programt::targett &target); - virtual void create_ensures_fn_call(goto_programt::targett &target); -}; - -class is_fresh_replacet : public is_fresh_baset -{ -public: - is_fresh_replacet( - code_contractst &_parent, - messaget _log, - const irep_idt _fun_id); - - virtual void create_declarations(); - -protected: - virtual void create_requires_fn_call(goto_programt::targett &target); - virtual void create_ensures_fn_call(goto_programt::targett &target); -}; - -/// Predicate to be used with the exprt::visit() function. It -/// will return the set of function calls within a goto program. -class find_is_fresh_calls_visitort -{ -public: - find_is_fresh_calls_visitort() - { - } - - // \brief return the set of functions invoked by - // the call graph of this program. - std::set &is_fresh_calls(); - void clear_set(); - void operator()(goto_programt &prog); - -protected: - std::set function_set; -}; - -/// Predicate to be used with the exprt::visit() function. The function -/// found_return_value() will return `true` iff this predicate is called on an -/// expr that contains `__CPROVER_return_value`. -class return_value_visitort : public const_expr_visitort -{ -public: - return_value_visitort() : const_expr_visitort(), found(false) - { - } - - // \brief Has this object been passed to exprt::visit() on an exprt whose - // descendants contain __CPROVER_return_value? - bool found_return_value(); - void operator()(const exprt &exp) override; - -protected: - bool found; -}; - -/// Predicate to be used with the exprt::visit() function. The function -/// found_return_value() will return `true` iff this predicate is called on an -/// expr that contains `__CPROVER_return_value`. -class functions_in_scope_visitort -{ -public: - functions_in_scope_visitort( - const goto_functionst &goto_functions, - messaget &log) - : goto_functions(goto_functions), log(log) - { - } - - // \brief return the set of functions invoked by - // the call graph of this program. - std::set &function_calls(); - void operator()(const goto_programt &prog); - -protected: - const goto_functionst &goto_functions; - messaget &log; - std::set function_set; -}; - -class function_binding_visitort : const_expr_visitort -{ -public: - function_binding_visitort() : const_expr_visitort() - { - } - - void operator()(const exprt &exp) override - { - } -}; - #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H diff --git a/src/goto-instrument/contracts_memory_predicates.cpp b/src/goto-instrument/contracts_memory_predicates.cpp new file mode 100644 index 00000000000..e437f188686 --- /dev/null +++ b/src/goto-instrument/contracts_memory_predicates.cpp @@ -0,0 +1,360 @@ +/*******************************************************************\ + +Module: Predicates to specify memory footprint in function contracts. + +Author: Felipe R. Monteiro + +Date: July 2021 + +\*******************************************************************/ + +/// \file +/// Predicates to specify memory footprint in function contracts + +#include "contracts_memory_predicates.h" + +#include +#include + +#include + +#include +#include + +bool return_value_visitort::found_return_value() +{ + return found; +} + +void return_value_visitort::operator()(const exprt &exp) +{ + if(exp.id() != ID_symbol) + return; + const symbol_exprt &sym = to_symbol_expr(exp); + found |= sym.get_identifier() == CPROVER_PREFIX "return_value"; +} + +std::set &functions_in_scope_visitort::function_calls() +{ + return function_set; +} + +void functions_in_scope_visitort::operator()(const goto_programt &prog) +{ + forall_goto_program_instructions(ins, prog) + { + if(ins->is_function_call()) + { + const code_function_callt &call = ins->get_function_call(); + + if(call.function().id() != ID_symbol) + { + log.error().source_location = call.find_source_location(); + log.error() << "Function pointer used in function invoked by " + "function contract: " + << messaget::eom; + throw 0; + } + else + { + const irep_idt &fun_name = + to_symbol_expr(call.function()).get_identifier(); + if(function_set.find(fun_name) == function_set.end()) + { + function_set.insert(fun_name); + auto called_fun = goto_functions.function_map.find(fun_name); + if(called_fun == goto_functions.function_map.end()) + { + log.warning() << "Could not find function '" << fun_name + << "' in goto-program." << messaget::eom; + throw 0; + } + if(called_fun->second.body_available()) + { + const goto_programt &program = called_fun->second.body; + (*this)(program); + } + else + { + log.warning() << "No body for function: " << fun_name + << "invoked from function contract." << messaget::eom; + } + } + } + } + } +} + +std::set &find_is_fresh_calls_visitort::is_fresh_calls() +{ + return function_set; +} + +void find_is_fresh_calls_visitort::clear_set() +{ + function_set.clear(); +} + +void find_is_fresh_calls_visitort::operator()(goto_programt &prog) +{ + Forall_goto_program_instructions(ins, prog) + { + if(ins->is_function_call()) + { + const code_function_callt &call = ins->get_function_call(); + + if(call.function().id() == ID_symbol) + { + const irep_idt &fun_name = + to_symbol_expr(call.function()).get_identifier(); + + if(fun_name == (CPROVER_PREFIX + std::string("is_fresh"))) + { + function_set.insert(ins); + } + } + } + } +} + +void is_fresh_baset::update_requires(goto_programt &requires) +{ + find_is_fresh_calls_visitort requires_visitor; + requires_visitor(requires); + for(auto it : requires_visitor.is_fresh_calls()) + { + create_requires_fn_call(it); + } +} + +void is_fresh_baset::update_ensures(goto_programt &ensures) +{ + find_is_fresh_calls_visitort ensures_visitor; + ensures_visitor(ensures); + for(auto it : ensures_visitor.is_fresh_calls()) + { + create_ensures_fn_call(it); + } +} + +// +// +// Code largely copied from model_argc_argv.cpp +// +// + +void is_fresh_baset::add_declarations(const std::string &decl_string) +{ + log.debug() << "Creating declarations: \n" << decl_string << "\n"; + + std::istringstream iss(decl_string); + + ansi_c_languaget ansi_c_language; + ansi_c_language.set_message_handler(log.get_message_handler()); + configt::ansi_ct::preprocessort pp = config.ansi_c.preprocessor; + config.ansi_c.preprocessor = configt::ansi_ct::preprocessort::NONE; + ansi_c_language.parse(iss, ""); + config.ansi_c.preprocessor = pp; + + symbol_tablet tmp_symbol_table; + ansi_c_language.typecheck(tmp_symbol_table, ""); + exprt value = nil_exprt(); + + goto_functionst tmp_functions; + + // Add the new functions into the goto functions table. + parent.get_goto_functions().function_map[ensures_fn_name].copy_from( + tmp_functions.function_map[ensures_fn_name]); + + parent.get_goto_functions().function_map[requires_fn_name].copy_from( + tmp_functions.function_map[requires_fn_name]); + + for(const auto &symbol_pair : tmp_symbol_table.symbols) + { + if( + symbol_pair.first == memmap_name || + symbol_pair.first == ensures_fn_name || + symbol_pair.first == requires_fn_name || symbol_pair.first == "malloc") + { + this->parent.get_symbol_table().insert(symbol_pair.second); + } + // Parameters are stored as scoped names in the symbol table. + else if( + (has_prefix( + id2string(symbol_pair.first), id2string(ensures_fn_name) + "::") || + has_prefix( + id2string(symbol_pair.first), id2string(requires_fn_name) + "::")) && + parent.get_symbol_table().add(symbol_pair.second)) + { + UNREACHABLE; + } + } + + // We have to set the global memory map array to + // all zeros for this to work properly + const array_typet ty = + to_array_type(tmp_symbol_table.lookup_ref(memmap_name).type); + constant_exprt initial_value(irep_idt(dstringt("0")), ty.subtype()); + array_of_exprt memmap_init(initial_value, ty); + goto_programt::instructiont a = + goto_programt::make_assignment(symbol_exprt(memmap_name, ty), memmap_init); + + // insert the assignment into the initialize function. + auto called_func = + parent.get_goto_functions().function_map.find(INITIALIZE_FUNCTION); + goto_programt &body = called_func->second.body; + auto target = body.get_end_function(); + body.insert_before(target, a); +} + +void is_fresh_baset::update_fn_call( + goto_programt::targett &ins, + const std::string &fn_name, + bool add_address_of) +{ + const code_function_callt &const_call = ins->get_function_call(); + code_function_callt call( + exprt(const_call.lhs()), + exprt(const_call.function()), + code_function_callt::argumentst(const_call.arguments())); + + // adjusting the expression for the first argument, if required + if(add_address_of) + { + INVARIANT(call.arguments().size() > 0, "Function must have arguments"); + call.arguments()[0] = address_of_exprt(call.arguments()[0]); + } + + // fixing the function name. + to_symbol_expr(call.function()).set_identifier(fn_name); + log.debug() << "printing updated call expression: " + << expr2c(call, parent.get_namespace()) << "\n"; + + ins->set_function_call(call); +} + +/* Declarations for contract enforcement */ + +is_fresh_enforcet::is_fresh_enforcet( + code_contractst &_parent, + messaget _log, + irep_idt _fun_id) + : is_fresh_baset(_parent, _log, _fun_id) +{ + std::stringstream ssreq, ssensure, ssmemmap; + ssreq << CPROVER_PREFIX << fun_id << "_requires_is_fresh"; + this->requires_fn_name = ssreq.str(); + + ssensure << CPROVER_PREFIX << fun_id << "_ensures_is_fresh"; + this->ensures_fn_name = ssensure.str(); + + ssmemmap << CPROVER_PREFIX << fun_id << "_memory_map"; + this->memmap_name = ssmemmap.str(); +} + +void is_fresh_enforcet::create_declarations() +{ + std::ostringstream oss; + std::string cprover_prefix(CPROVER_PREFIX); + oss << "static _Bool " << memmap_name + << "[" + cprover_prefix + "constant_infinity_uint]; \n" + << "\n" + << "_Bool " << requires_fn_name + << "(void **elem, " + cprover_prefix + "size_t size) { \n" + << " *elem = malloc(size); \n" + << " if (!*elem || " << memmap_name + << "[" + cprover_prefix + "POINTER_OBJECT(*elem)]) return 0; \n" + << " " << memmap_name << "[" + cprover_prefix + << "POINTER_OBJECT(*elem)] = 1; \n" + << " return 1; \n" + << "} \n" + << "\n" + << "_Bool " << ensures_fn_name + << "(void *elem, " + cprover_prefix + "size_t size) { \n" + << " _Bool ok = (!" << memmap_name + << "[" + cprover_prefix + "POINTER_OBJECT(elem)] && " + << cprover_prefix + "r_ok(elem, size)); \n" + << " " << memmap_name << "[" + cprover_prefix + << "POINTER_OBJECT(elem)] = 1; \n" + << " return ok; \n" + << "}"; + + add_declarations(oss.str()); +} + +void is_fresh_enforcet::create_requires_fn_call(goto_programt::targett &ins) +{ + update_fn_call(ins, requires_fn_name, true); +} + +void is_fresh_enforcet::create_ensures_fn_call(goto_programt::targett &ins) +{ + update_fn_call(ins, ensures_fn_name, false); +} + +/* Declarations for contract replacement: note that there may be several + instances of the same function called in a particular context, so care must be taken + that the 'call' functions and global data structure are unique for each instance. + This is why we check that the symbols are unique for each such declaration. */ + +std::string unique_symbol(const symbol_tablet &tbl, const std::string &original) +{ + auto size = tbl.next_unused_suffix(original); + return original + std::to_string(size); +} + +is_fresh_replacet::is_fresh_replacet( + code_contractst &_parent, + messaget _log, + irep_idt _fun_id) + : is_fresh_baset(_parent, _log, _fun_id) +{ + std::stringstream ssreq, ssensure, ssmemmap; + ssreq /* << CPROVER_PREFIX */ << fun_id << "_call_requires_is_fresh"; + this->requires_fn_name = + unique_symbol(parent.get_symbol_table(), ssreq.str()); + + ssensure /* << CPROVER_PREFIX */ << fun_id << "_call_ensures_is_fresh"; + this->ensures_fn_name = + unique_symbol(parent.get_symbol_table(), ssensure.str()); + + ssmemmap /* << CPROVER_PREFIX */ << fun_id << "_memory_map"; + this->memmap_name = unique_symbol(parent.get_symbol_table(), ssmemmap.str()); +} + +void is_fresh_replacet::create_declarations() +{ + std::ostringstream oss; + std::string cprover_prefix(CPROVER_PREFIX); + oss << "static _Bool " << memmap_name + << "[" + cprover_prefix + "constant_infinity_uint]; \n" + << "\n" + << "static _Bool " << requires_fn_name + << "(void *elem, " + cprover_prefix + "size_t size) { \n" + << " _Bool r_ok = " + cprover_prefix + "r_ok(elem, size); \n" + << " if (" << memmap_name + << "[" + cprover_prefix + "POINTER_OBJECT(elem)]" + << " != 0 || !r_ok) return 0; \n" + << " " << memmap_name << "[" + << cprover_prefix + "POINTER_OBJECT(elem)] = 1; \n" + << " return 1; \n" + << "} \n" + << " \n" + << "_Bool " << ensures_fn_name + << "(void **elem, " + cprover_prefix + "size_t size) { \n" + << " *elem = malloc(size); \n" + << " return (*elem != 0); \n" + << "} \n"; + + add_declarations(oss.str()); +} + +void is_fresh_replacet::create_requires_fn_call(goto_programt::targett &ins) +{ + update_fn_call(ins, requires_fn_name, false); +} + +void is_fresh_replacet::create_ensures_fn_call(goto_programt::targett &ins) +{ + update_fn_call(ins, ensures_fn_name, true); +} diff --git a/src/goto-instrument/contracts_memory_predicates.h b/src/goto-instrument/contracts_memory_predicates.h new file mode 100644 index 00000000000..d6a0d8e92b7 --- /dev/null +++ b/src/goto-instrument/contracts_memory_predicates.h @@ -0,0 +1,159 @@ +/*******************************************************************\ + +Module: Predicates to specify memory footprint in function contracts. + +Author: Felipe R. Monteiro + +Date: July 2021 + +\*******************************************************************/ + +/// \file +/// Predicates to specify memory footprint in function contracts + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H + +#include "code_contracts.h" + +class is_fresh_baset +{ +public: + is_fresh_baset( + code_contractst &_parent, + messaget _log, + const irep_idt _fun_id) + : parent(_parent), log(_log), fun_id(_fun_id) + { + } + + void update_requires(goto_programt &requires); + void update_ensures(goto_programt &ensures); + + virtual void create_declarations() = 0; + +protected: + void add_declarations(const std::string &decl_string); + void update_fn_call( + goto_programt::targett &target, + const std::string &name, + bool add_address_of); + + virtual void create_requires_fn_call(goto_programt::targett &target) = 0; + virtual void create_ensures_fn_call(goto_programt::targett &target) = 0; + + code_contractst &parent; + messaget log; + irep_idt fun_id; + + // written by the child classes. + std::string memmap_name; + std::string requires_fn_name; + std::string ensures_fn_name; +}; + +class is_fresh_enforcet : public is_fresh_baset +{ +public: + is_fresh_enforcet( + code_contractst &_parent, + messaget _log, + const irep_idt _fun_id); + + virtual void create_declarations(); + +protected: + virtual void create_requires_fn_call(goto_programt::targett &target); + virtual void create_ensures_fn_call(goto_programt::targett &target); +}; + +class is_fresh_replacet : public is_fresh_baset +{ +public: + is_fresh_replacet( + code_contractst &_parent, + messaget _log, + const irep_idt _fun_id); + + virtual void create_declarations(); + +protected: + virtual void create_requires_fn_call(goto_programt::targett &target); + virtual void create_ensures_fn_call(goto_programt::targett &target); +}; + +/// Predicate to be used with the exprt::visit() function. It +/// will return the set of function calls within a goto program. +class find_is_fresh_calls_visitort +{ +public: + find_is_fresh_calls_visitort() + { + } + + // \brief return the set of functions invoked by + // the call graph of this program. + std::set &is_fresh_calls(); + void clear_set(); + void operator()(goto_programt &prog); + +protected: + std::set function_set; +}; + +/// Predicate to be used with the exprt::visit() function. The function +/// found_return_value() will return `true` iff this predicate is called on an +/// expr that contains `__CPROVER_return_value`. +class return_value_visitort : public const_expr_visitort +{ +public: + return_value_visitort() : const_expr_visitort(), found(false) + { + } + + // \brief Has this object been passed to exprt::visit() on an exprt whose + // descendants contain __CPROVER_return_value? + bool found_return_value(); + void operator()(const exprt &exp) override; + +protected: + bool found; +}; + +/// Predicate to be used with the exprt::visit() function. The function +/// found_return_value() will return `true` iff this predicate is called on an +/// expr that contains `__CPROVER_return_value`. +class functions_in_scope_visitort +{ +public: + functions_in_scope_visitort( + const goto_functionst &goto_functions, + messaget &log) + : goto_functions(goto_functions), log(log) + { + } + + // \brief return the set of functions invoked by + // the call graph of this program. + std::set &function_calls(); + void operator()(const goto_programt &prog); + +protected: + const goto_functionst &goto_functions; + messaget &log; + std::set function_set; +}; + +class function_binding_visitort : const_expr_visitort +{ +public: + function_binding_visitort() : const_expr_visitort() + { + } + + void operator()(const exprt &exp) override + { + } +}; + +#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H \ No newline at end of file From cc604be9e9453511a196a30ed6a9721a90a406b7 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 16 Jul 2021 17:09:57 +0000 Subject: [PATCH 2/6] Adds missing case to assigns clause type checking Signed-off-by: Felipe R. Monteiro --- .../contracts/assigns_type_checking_valid_cases/main.c | 8 +++++++- src/ansi-c/ansi_c_convert_type.cpp | 2 +- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/regression/contracts/assigns_type_checking_valid_cases/main.c b/regression/contracts/assigns_type_checking_valid_cases/main.c index e4b1c778aa7..cf20e9baa11 100644 --- a/regression/contracts/assigns_type_checking_valid_cases/main.c +++ b/regression/contracts/assigns_type_checking_valid_cases/main.c @@ -3,10 +3,15 @@ int *x; int y; +struct blob +{ + int allocated; +}; struct buf { int *data; size_t len; + struct blob aux; }; void foo1(int a) __CPROVER_assigns(a) @@ -76,9 +81,10 @@ void foo9(int array[]) __CPROVER_assigns(array) } void foo10(struct buf *buffer) __CPROVER_requires(buffer != NULL) - __CPROVER_assigns(*buffer) + __CPROVER_assigns(buffer->len, buffer->aux.allocated) { buffer->len = 0; + buffer->aux.allocated = 0; } int main() diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 0ac0a11204a..6223257e259 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -257,7 +257,7 @@ void ansi_c_convert_typet::read_rec(const typet &type) { if( operand.id() != ID_symbol && operand.id() != ID_ptrmember && - operand.id() != ID_dereference) + operand.id() != ID_member && operand.id() != ID_dereference) { error().source_location = source_location; error() << "illegal target in assigns clause" << eom; From e8777aa81ffa819ca4119bd44a53c5318f59c856 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 16 Jul 2021 17:57:21 +0000 Subject: [PATCH 3/6] Removes dead code from assigns clause implementation Signed-off-by: Felipe R. Monteiro --- src/goto-instrument/code_contracts.cpp | 401 +++---------------------- src/goto-instrument/code_contracts.h | 117 +------- 2 files changed, 48 insertions(+), 470 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 91738a42d9b..c1b0f57278c 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -1260,18 +1260,21 @@ bool code_contractst::enforce_contracts( return fail; } -assigns_clause_scalar_targett::assigns_clause_scalar_targett( +assigns_clause_targett::assigns_clause_targett( const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id) - : assigns_clause_targett( - Scalar, - pointer_for(object_ptr), - contract, - log_parameter), - local_standin_variable(typet()) + : pointer_object(pointer_for(object_ptr)), + contract(contract), + init_block(), + log(log_parameter), + local_target(typet()) { + INVARIANT( + pointer_object.type().id() == ID_pointer, + "Assigns clause targets should be stored as pointer expressions."); + const symbolt &function_symbol = contract.ns.lookup(function_id); // Declare a new symbol to stand in for the reference @@ -1281,214 +1284,39 @@ assigns_clause_scalar_targett::assigns_clause_scalar_targett( function_id, function_symbol.mode); - local_standin_variable = standin_symbol.symbol_expr(); + local_target = standin_symbol.symbol_expr(); // Build standin variable initialization block init_block.add( - goto_programt::make_decl(local_standin_variable, function_symbol.location)); + goto_programt::make_decl(local_target, function_symbol.location)); init_block.add(goto_programt::make_assignment( - code_assignt(local_standin_variable, pointer_object), - function_symbol.location)); + code_assignt(local_target, pointer_object), function_symbol.location)); } -std::vector -assigns_clause_scalar_targett::temporary_declarations() const +assigns_clause_targett::~assigns_clause_targett() { - std::vector result; - result.push_back(local_standin_variable); - return result; } -exprt assigns_clause_scalar_targett::alias_expression(const exprt &ptr) +std::vector assigns_clause_targett::temporary_declarations() const { - return same_object(ptr, local_standin_variable); -} - -exprt assigns_clause_scalar_targett::compatible_expression( - const assigns_clause_targett &called_target) -{ - if(called_target.target_type == Scalar) - { - return alias_expression(called_target.get_direct_pointer()); - } - else // Struct or Array - { - return false_exprt(); - } -} - -goto_programt -assigns_clause_scalar_targett::havoc_code(source_locationt location) const -{ - goto_programt assigns_havoc; - - exprt lhs = dereference_exprt(pointer_object); - side_effect_expr_nondett rhs(lhs.type(), location); - - goto_programt::targett target = - assigns_havoc.add(goto_programt::make_assignment( - code_assignt(std::move(lhs), std::move(rhs)), location)); - target->code_nonconst().add_source_location() = location; - - return assigns_havoc; -} - -assigns_clause_struct_targett::assigns_clause_struct_targett( - const exprt &object_ptr, - code_contractst &contract, - messaget &log_parameter, - const irep_idt &function_id) - : assigns_clause_targett( - Struct, - pointer_for(object_ptr), - contract, - log_parameter), - main_struct_standin(typet()) -{ - const symbolt &struct_symbol = - contract.ns.lookup(to_tag_type(object_ptr.type())); - const symbolt &function_symbol = contract.ns.lookup(function_id); - - // Declare a new symbol to stand in for the reference - symbolt struct_temp_symbol = contract.new_tmp_symbol( - pointer_object.type(), - function_symbol.location, - function_id, - function_symbol.mode); - main_struct_standin = struct_temp_symbol.symbol_expr(); - local_standin_variables.push_back(main_struct_standin); - - // Build standin variable initialization block - init_block.add( - goto_programt::make_decl(main_struct_standin, function_symbol.location)); - init_block.add(goto_programt::make_assignment( - code_assignt(main_struct_standin, pointer_object), - function_symbol.location)); - - // Handle component members - std::vector component_members; - const struct_typet &struct_type = to_struct_type(struct_symbol.type); - for(struct_union_typet::componentt component : struct_type.components()) - { - exprt current_member = member_exprt(object_ptr, component); - component_members.push_back(current_member); - } - - while(!component_members.empty()) - { - exprt current_operation = component_members.front(); - exprt operation_address = pointer_for(current_operation); - - // Declare a new symbol to stand in for the reference - symbolt standin_symbol = contract.new_tmp_symbol( - operation_address.type(), - function_symbol.location, - function_id, - function_symbol.mode); - - symbol_exprt current_standin = standin_symbol.symbol_expr(); - local_standin_variables.push_back(current_standin); - - // Add to standin variable initialization block - init_block.add( - goto_programt::make_decl(current_standin, function_symbol.location)); - init_block.add(goto_programt::make_assignment( - code_assignt(current_standin, operation_address), - function_symbol.location)); - - if(current_operation.type().id() == ID_struct_tag) - { - const symbolt ¤t_struct_symbol = - contract.ns.lookup(to_tag_type(current_operation.type())); - - const struct_typet &curr_struct_t = - to_struct_type(current_struct_symbol.type); - for(struct_union_typet::componentt component : curr_struct_t.components()) - { - exprt current_member = member_exprt(current_operation, component); - component_members.push_back(current_member); - } - } - component_members.erase(component_members.begin()); - } -} - -std::vector -assigns_clause_struct_targett::temporary_declarations() const -{ - return local_standin_variables; + std::vector result; + result.push_back(local_target); + return result; } -exprt assigns_clause_struct_targett::alias_expression(const exprt &ptr) +exprt assigns_clause_targett::alias_expression(const exprt &ptr) { - exprt::operandst disjuncts; - disjuncts.reserve(local_standin_variables.size()); - for(symbol_exprt symbol : local_standin_variables) - { - const typet &ptr_concrete_type = to_pointer_type(ptr.type()).subtype(); - auto left_size = size_of_expr(ptr_concrete_type, contract.ns); - const typet &standin_concrete_type = - to_pointer_type(symbol.type()).subtype(); - auto right_size = size_of_expr(standin_concrete_type, contract.ns); - INVARIANT(left_size.has_value(), "Unable to determine size of type (lhs)."); - INVARIANT( - right_size.has_value(), "Unable to determine size of type (rhs)."); - if(*left_size == *right_size) - { - exprt same_obj = same_object(ptr, symbol); - exprt same_offset = - equal_exprt(pointer_offset(ptr), pointer_offset(symbol)); - - disjuncts.push_back(and_exprt{same_obj, same_offset}); - } - } - - return disjunction(disjuncts); + return same_object(ptr, local_target); } -exprt assigns_clause_struct_targett::compatible_expression( +exprt assigns_clause_targett::compatible_expression( const assigns_clause_targett &called_target) { - if(called_target.target_type == Scalar) - { return alias_expression(called_target.get_direct_pointer()); - } - else if(called_target.target_type == Struct) - { - const assigns_clause_struct_targett &struct_target = - static_cast(called_target); - - exprt same_obj = - same_object(this->main_struct_standin, struct_target.pointer_object); - // the size of the called struct should be less than or - // equal to that of the assignable target struct. - exprt current_size = - get_size(this->pointer_object.type(), contract.ns, log); - exprt curr_upper_offset = - pointer_offset(plus_exprt(this->main_struct_standin, current_size)); - exprt called_size = - get_size(struct_target.pointer_object.type(), contract.ns, log); - exprt called_upper_offset = - pointer_offset(plus_exprt(struct_target.pointer_object, called_size)); - - exprt in_range_lower = binary_predicate_exprt( - pointer_offset(struct_target.pointer_object), - ID_ge, - pointer_offset(this->main_struct_standin)); - exprt in_range_upper = - binary_predicate_exprt(curr_upper_offset, ID_ge, called_upper_offset); - - exprt in_range = and_exprt(in_range_lower, in_range_upper); - return and_exprt(same_obj, in_range); - } - else // Array - { - return false_exprt(); - } } goto_programt -assigns_clause_struct_targett::havoc_code(source_locationt location) const +assigns_clause_targett::havoc_code(source_locationt location) const { goto_programt assigns_havoc; @@ -1503,171 +1331,14 @@ assigns_clause_struct_targett::havoc_code(source_locationt location) const return assigns_havoc; } -assigns_clause_array_targett::assigns_clause_array_targett( - const exprt &object_ptr, - code_contractst &contract, - messaget &log_parameter, - const irep_idt &function_id) - : assigns_clause_targett(Array, object_ptr, contract, log_parameter), - lower_offset_object(), - upper_offset_object(), - array_standin_variable(typet()), - lower_offset_variable(typet()), - upper_offset_variable(typet()) +const exprt &assigns_clause_targett::get_direct_pointer() const { - const symbolt &function_symbol = contract.ns.lookup(function_id); - - // Declare a new symbol to stand in for the reference - symbolt standin_symbol = contract.new_tmp_symbol( - pointer_object.type(), - function_symbol.location, - function_id, - function_symbol.mode); - - array_standin_variable = standin_symbol.symbol_expr(); - - // Add array temp to variable initialization block - init_block.add( - goto_programt::make_decl(array_standin_variable, function_symbol.location)); - init_block.add(goto_programt::make_assignment( - code_assignt(array_standin_variable, pointer_object), - function_symbol.location)); - - if(object_ptr.id() == ID_address_of) - { - exprt constant_size = - get_size(object_ptr.type().subtype(), contract.ns, log); - lower_offset_object = typecast_exprt( - mult_exprt( - typecast_exprt(object_ptr, unsigned_long_int_type()), constant_size), - signed_int_type()); - - // Declare a new symbol to stand in for the reference - symbolt lower_standin_symbol = contract.new_tmp_symbol( - lower_offset_object.type(), - function_symbol.location, - function_id, - function_symbol.mode); - - lower_offset_variable = lower_standin_symbol.symbol_expr(); - - // Add array temp to variable initialization block - init_block.add(goto_programt::make_decl( - lower_offset_variable, function_symbol.location)); - init_block.add(goto_programt::make_assignment( - code_assignt(lower_offset_variable, lower_offset_object), - function_symbol.location)); - - upper_offset_object = typecast_exprt( - mult_exprt( - typecast_exprt(object_ptr, unsigned_long_int_type()), constant_size), - signed_int_type()); - - // Declare a new symbol to stand in for the reference - symbolt upper_standin_symbol = contract.new_tmp_symbol( - upper_offset_object.type(), - function_symbol.location, - function_id, - function_symbol.mode); - - upper_offset_variable = upper_standin_symbol.symbol_expr(); - - // Add array temp to variable initialization block - init_block.add(goto_programt::make_decl( - upper_offset_variable, function_symbol.location)); - init_block.add(goto_programt::make_assignment( - code_assignt(upper_offset_variable, upper_offset_object), - function_symbol.location)); - } + return pointer_object; } -std::vector -assigns_clause_array_targett::temporary_declarations() const +goto_programt &assigns_clause_targett::get_init_block() { - std::vector result; - result.push_back(array_standin_variable); - result.push_back(lower_offset_variable); - result.push_back(upper_offset_variable); - - return result; -} - -goto_programt -assigns_clause_array_targett::havoc_code(source_locationt location) const -{ - goto_programt assigns_havoc; - - modifiest assigns_tgts; - typet lower_type = lower_offset_variable.type(); - exprt array_type_size = - get_size(pointer_object.type().subtype(), contract.ns, log); - - for(mp_integer i = lower_bound; i < upper_bound; ++i) - { - irep_idt offset_string(from_integer(i, integer_typet()).get_value()); - irep_idt offset_irep(offset_string); - constant_exprt val_const(offset_irep, lower_type); - dereference_exprt array_deref(plus_exprt( - pointer_object, typecast_exprt(val_const, signed_long_int_type()))); - - assigns_tgts.insert(array_deref); - } - - for(auto lhs : assigns_tgts) - { - side_effect_expr_nondett rhs(lhs.type(), location); - - goto_programt::targett target = - assigns_havoc.add(goto_programt::make_assignment( - code_assignt(std::move(lhs), std::move(rhs)), location)); - target->code_nonconst().add_source_location() = location; - } - - return assigns_havoc; -} - -exprt assigns_clause_array_targett::alias_expression(const exprt &ptr) -{ - exprt ptr_offset = pointer_offset(ptr); - exprt::operandst conjuncts; - - conjuncts.push_back(same_object(ptr, array_standin_variable)); - conjuncts.push_back(binary_predicate_exprt( - ptr_offset, - ID_ge, - typecast_exprt(lower_offset_variable, ptr_offset.type()))); - conjuncts.push_back(binary_predicate_exprt( - typecast_exprt(upper_offset_variable, ptr_offset.type()), - ID_ge, - ptr_offset)); - - return conjunction(conjuncts); -} - -exprt assigns_clause_array_targett::compatible_expression( - const assigns_clause_targett &called_target) -{ - if(called_target.target_type == Scalar) - { - return alias_expression(called_target.get_direct_pointer()); - } - else if(called_target.target_type == Array) - { - const assigns_clause_array_targett &array_target = - static_cast(called_target); - exprt same_obj = - same_object(this->array_standin_variable, array_target.pointer_object); - exprt in_range_lower = binary_predicate_exprt( - array_target.lower_offset_object, ID_ge, this->lower_offset_variable); - exprt in_range_upper = binary_predicate_exprt( - this->upper_offset_variable, ID_ge, array_target.upper_offset_object); - exprt in_range = and_exprt(in_range_lower, in_range_upper); - return and_exprt(same_obj, in_range); - } - else // Struct - { - return false_exprt(); - } + return init_block; } assigns_clauset::assigns_clauset( @@ -1685,6 +1356,7 @@ assigns_clauset::assigns_clauset( add_target(current_operation); } } + assigns_clauset::~assigns_clauset() { for(assigns_clause_targett *target : targets) @@ -1695,16 +1367,15 @@ assigns_clauset::~assigns_clauset() assigns_clause_targett *assigns_clauset::add_target(exprt current_operation) { - assigns_clause_scalar_targett *scalar_target = - new assigns_clause_scalar_targett( - (current_operation.id() == ID_address_of) - ? to_index_expr(to_address_of_expr(current_operation).object()).array() - : current_operation, - parent, - log, - function_id); - targets.push_back(scalar_target); - return scalar_target; + assigns_clause_targett *target = new assigns_clause_targett( + (current_operation.id() == ID_address_of) + ? to_index_expr(to_address_of_expr(current_operation).object()).array() + : current_operation, + parent, + log, + function_id); + targets.push_back(target); + return target; } assigns_clause_targett * diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 4687ad469fb..8aa56f62dc1 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -247,124 +247,31 @@ class code_contractst class assigns_clause_targett { public: - enum target_type - { - Scalar, - Struct, - Array - }; - assigns_clause_targett( - target_type type, - const exprt object_ptr, - const code_contractst &contract, - messaget &log_parameter) - : target_type(type), - pointer_object(object_ptr), - contract(contract), - init_block(), - log(log_parameter) - { - INVARIANT( - pointer_object.type().id() == ID_pointer, - "Assigns clause targets should be stored as pointer expressions."); - } - - virtual ~assigns_clause_targett() - { - } - - virtual std::vector temporary_declarations() const = 0; - virtual exprt alias_expression(const exprt &lhs) = 0; - virtual exprt - compatible_expression(const assigns_clause_targett &called_target) = 0; - virtual goto_programt havoc_code(source_locationt location) const = 0; - - const exprt &get_direct_pointer() const - { - return pointer_object; - } - - goto_programt &get_init_block() - { - return init_block; - } - - static exprt pointer_for(const exprt &exp) - { - return address_of_exprt(exp); - } - - const target_type target_type; - -protected: - const exprt pointer_object; - const code_contractst &contract; - goto_programt init_block; - messaget &log; -}; - -class assigns_clause_scalar_targett : public assigns_clause_targett -{ -public: - assigns_clause_scalar_targett( const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id); + ~assigns_clause_targett(); std::vector temporary_declarations() const; exprt alias_expression(const exprt &lhs); exprt compatible_expression(const assigns_clause_targett &called_target); goto_programt havoc_code(source_locationt location) const; + const exprt &get_direct_pointer() const; + goto_programt &get_init_block(); -protected: - symbol_exprt local_standin_variable; -}; - -class assigns_clause_struct_targett : public assigns_clause_targett -{ -public: - assigns_clause_struct_targett( - const exprt &object_ptr, - code_contractst &contract, - messaget &log_parameter, - const irep_idt &function_id); - - std::vector temporary_declarations() const; - exprt alias_expression(const exprt &lhs); - exprt compatible_expression(const assigns_clause_targett &called_target); - goto_programt havoc_code(source_locationt location) const; - -protected: - symbol_exprt main_struct_standin; - std::vector local_standin_variables; -}; - -class assigns_clause_array_targett : public assigns_clause_targett -{ -public: - assigns_clause_array_targett( - const exprt &object_ptr, - code_contractst &contract, - messaget &log_parameter, - const irep_idt &function_id); - - std::vector temporary_declarations() const; - exprt alias_expression(const exprt &lhs); - exprt compatible_expression(const assigns_clause_targett &called_target); - goto_programt havoc_code(source_locationt location) const; + static exprt pointer_for(const exprt &exp) + { + return address_of_exprt(exp); + } protected: - mp_integer lower_bound; - mp_integer upper_bound; - - exprt lower_offset_object; - exprt upper_offset_object; - - symbol_exprt array_standin_variable; - symbol_exprt lower_offset_variable; - symbol_exprt upper_offset_variable; + const exprt pointer_object; + const code_contractst &contract; + goto_programt init_block; + messaget &log; + symbol_exprt local_target; }; class assigns_clauset From c2a5d79eb709848d9309a28cb0c9c26e34050d57 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 16 Jul 2021 18:39:27 +0000 Subject: [PATCH 4/6] Adds a assigns clause module in contracts Signed-off-by: Felipe R. Monteiro --- src/goto-instrument/Makefile | 3 +- .../{code_contracts.cpp => contracts.cpp} | 324 +---------------- .../{code_contracts.h => contracts.h} | 71 ---- src/goto-instrument/contracts_assigns.cpp | 331 ++++++++++++++++++ src/goto-instrument/contracts_assigns.h | 90 +++++ .../contracts_memory_predicates.h | 2 +- .../goto_instrument_parse_options.h | 2 +- 7 files changed, 430 insertions(+), 393 deletions(-) rename src/goto-instrument/{code_contracts.cpp => contracts.cpp} (83%) rename src/goto-instrument/{code_contracts.h => contracts.h} (82%) create mode 100644 src/goto-instrument/contracts_assigns.cpp create mode 100644 src/goto-instrument/contracts_assigns.h diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index e5edc810bbe..99e17cd2d5b 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -16,8 +16,9 @@ SRC = accelerate/accelerate.cpp \ alignment_checks.cpp \ branch.cpp \ call_sequences.cpp \ - code_contracts.cpp \ + contracts_assigns.cpp \ contracts_memory_predicates.cpp \ + contracts.cpp \ concurrency.cpp \ count_eloc.cpp \ cover.cpp \ diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/contracts.cpp similarity index 83% rename from src/goto-instrument/code_contracts.cpp rename to src/goto-instrument/contracts.cpp index c1b0f57278c..645f3400f7b 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/contracts.cpp @@ -11,6 +11,7 @@ Date: February 2016 /// \file /// Verify and use annotated invariants and pre/post-conditions +#include "contracts_assigns.h" #include "contracts_memory_predicates.h" #include @@ -24,7 +25,6 @@ Date: February 2016 #include -#include #include #include #include @@ -32,7 +32,6 @@ Date: February 2016 #include #include #include -#include #include exprt get_size(const typet &type, const namespacet &ns, messaget &log) @@ -163,8 +162,8 @@ void code_contractst::check_apply_loop_contracts( // Generate: an assignment to store the decreases clause's value before the // loop - code_assignt old_decreases_assignment{old_decreases_symbol, - decreases_clause}; + code_assignt old_decreases_assignment{ + old_decreases_symbol, decreases_clause}; old_decreases_assignment.add_source_location() = loop_head->source_location; converter.goto_convert(old_decreases_assignment, havoc_code, mode); } @@ -201,8 +200,8 @@ void code_contractst::check_apply_loop_contracts( // Generate: an assignment to store the decreases clause's value after one // iteration of the loop - code_assignt new_decreases_assignment{new_decreases_symbol, - decreases_clause}; + code_assignt new_decreases_assignment{ + new_decreases_symbol, decreases_clause}; new_decreases_assignment.add_source_location() = loop_head->source_location; converter.goto_convert(new_decreases_assignment, havoc_code, mode); @@ -1258,317 +1257,4 @@ bool code_contractst::enforce_contracts( fail = enforce_contract(fun); } return fail; -} - -assigns_clause_targett::assigns_clause_targett( - const exprt &object_ptr, - code_contractst &contract, - messaget &log_parameter, - const irep_idt &function_id) - : pointer_object(pointer_for(object_ptr)), - contract(contract), - init_block(), - log(log_parameter), - local_target(typet()) -{ - INVARIANT( - pointer_object.type().id() == ID_pointer, - "Assigns clause targets should be stored as pointer expressions."); - - const symbolt &function_symbol = contract.ns.lookup(function_id); - - // Declare a new symbol to stand in for the reference - symbolt standin_symbol = contract.new_tmp_symbol( - pointer_object.type(), - function_symbol.location, - function_id, - function_symbol.mode); - - local_target = standin_symbol.symbol_expr(); - - // Build standin variable initialization block - init_block.add( - goto_programt::make_decl(local_target, function_symbol.location)); - init_block.add(goto_programt::make_assignment( - code_assignt(local_target, pointer_object), function_symbol.location)); -} - -assigns_clause_targett::~assigns_clause_targett() -{ -} - -std::vector assigns_clause_targett::temporary_declarations() const -{ - std::vector result; - result.push_back(local_target); - return result; -} - -exprt assigns_clause_targett::alias_expression(const exprt &ptr) -{ - return same_object(ptr, local_target); -} - -exprt assigns_clause_targett::compatible_expression( - const assigns_clause_targett &called_target) -{ - return alias_expression(called_target.get_direct_pointer()); -} - -goto_programt -assigns_clause_targett::havoc_code(source_locationt location) const -{ - goto_programt assigns_havoc; - - exprt lhs = dereference_exprt(pointer_object); - side_effect_expr_nondett rhs(lhs.type(), location); - - goto_programt::targett target = - assigns_havoc.add(goto_programt::make_assignment( - code_assignt(std::move(lhs), std::move(rhs)), location)); - target->code_nonconst().add_source_location() = location; - - return assigns_havoc; -} - -const exprt &assigns_clause_targett::get_direct_pointer() const -{ - return pointer_object; -} - -goto_programt &assigns_clause_targett::get_init_block() -{ - return init_block; -} - -assigns_clauset::assigns_clauset( - const exprt &assigns, - code_contractst &contract, - const irep_idt function_id, - messaget log_parameter) - : assigns_expr(assigns), - parent(contract), - function_id(function_id), - log(log_parameter) -{ - for(exprt current_operation : assigns_expr.operands()) - { - add_target(current_operation); - } -} - -assigns_clauset::~assigns_clauset() -{ - for(assigns_clause_targett *target : targets) - { - delete target; - } -} - -assigns_clause_targett *assigns_clauset::add_target(exprt current_operation) -{ - assigns_clause_targett *target = new assigns_clause_targett( - (current_operation.id() == ID_address_of) - ? to_index_expr(to_address_of_expr(current_operation).object()).array() - : current_operation, - parent, - log, - function_id); - targets.push_back(target); - return target; -} - -assigns_clause_targett * -assigns_clauset::add_pointer_target(exprt current_operation) -{ - return add_target(dereference_exprt(current_operation)); -} - -goto_programt assigns_clauset::init_block(source_locationt location) -{ - goto_programt result; - for(assigns_clause_targett *target : targets) - { - for(goto_programt::instructiont inst : - target->get_init_block().instructions) - { - result.add(goto_programt::instructiont(inst)); - } - } - return result; -} - -goto_programt &assigns_clauset::temporary_declarations( - source_locationt location, - irep_idt function_name, - irep_idt language_mode) -{ - if(standin_declarations.empty()) - { - for(assigns_clause_targett *target : targets) - { - for(symbol_exprt symbol : target->temporary_declarations()) - { - standin_declarations.add( - goto_programt::make_decl(symbol, symbol.source_location())); - } - } - } - return standin_declarations; -} - -goto_programt assigns_clauset::dead_stmts( - source_locationt location, - irep_idt function_name, - irep_idt language_mode) -{ - goto_programt dead_statements; - for(assigns_clause_targett *target : targets) - { - for(symbol_exprt symbol : target->temporary_declarations()) - { - dead_statements.add( - goto_programt::make_dead(symbol, symbol.source_location())); - } - } - return dead_statements; -} - -goto_programt assigns_clauset::havoc_code( - source_locationt location, - irep_idt function_name, - irep_idt language_mode) -{ - goto_programt havoc_statements; - for(assigns_clause_targett *target : targets) - { - // (1) If the assigned target is not a dereference, - // only include the havoc_statement - - // (2) If the assigned target is a dereference, do the following: - - // if(!__CPROVER_w_ok(target, 0)) goto z; - // havoc_statements - // z: skip - - // create the z label - goto_programt tmp_z; - goto_programt::targett z = tmp_z.add(goto_programt::make_skip(location)); - - const auto &target_ptr = target->get_direct_pointer(); - - if(to_address_of_expr(target_ptr).object().id() == ID_dereference) - { - // create the condition - exprt condition = - not_exprt(w_ok_exprt(target_ptr, from_integer(0, unsigned_int_type()))); - havoc_statements.add(goto_programt::make_goto(z, condition, location)); - } - - // create havoc_statements - for(goto_programt::instructiont instruction : - target->havoc_code(location).instructions) - { - havoc_statements.add(std::move(instruction)); - } - - if(to_address_of_expr(target_ptr).object().id() == ID_dereference) - { - // add the z label instruction - havoc_statements.destructive_append(tmp_z); - } - } - return havoc_statements; -} - -exprt assigns_clauset::alias_expression(const exprt &lhs) -{ - if(targets.empty()) - { - return false_exprt(); - } - - exprt left_ptr = assigns_clause_targett::pointer_for(lhs); - - bool first_iter = true; - exprt result = false_exprt(); - for(assigns_clause_targett *target : targets) - { - if(first_iter) - { - result = target->alias_expression(left_ptr); - first_iter = false; - } - else - { - result = or_exprt(result, target->alias_expression(left_ptr)); - } - } - return result; -} - -exprt assigns_clauset::compatible_expression( - const assigns_clauset &called_assigns) -{ - if(called_assigns.targets.empty()) - { - return true_exprt(); - } - - bool first_clause = true; - exprt result = true_exprt(); - for(assigns_clause_targett *called_target : called_assigns.targets) - { - bool first_iter = true; - exprt current_target_compatible = false_exprt(); - for(assigns_clause_targett *target : targets) - { - if(first_iter) - { - // TODO: Optimize the validation below and remove code duplication - // See GitHub issue #6105 for further details - - // Validating the called target through __CPROVER_w_ok() is - // only useful when the called target is a dereference - const auto &called_target_ptr = called_target->get_direct_pointer(); - if( - to_address_of_expr(called_target_ptr).object().id() == ID_dereference) - { - // or_exprt is short-circuited, therefore - // target->compatible_expression(*called_target) would not be - // checked on invalid called_targets. - current_target_compatible = or_exprt( - not_exprt(w_ok_exprt( - called_target_ptr, from_integer(0, unsigned_int_type()))), - target->compatible_expression(*called_target)); - } - else - { - current_target_compatible = - target->compatible_expression(*called_target); - } - first_iter = false; - } - else - { - current_target_compatible = or_exprt( - current_target_compatible, - target->compatible_expression(*called_target)); - } - } - if(first_clause) - { - result = current_target_compatible; - first_clause = false; - } - else - { - exprt::operandst conjuncts; - conjuncts.push_back(result); - conjuncts.push_back(current_target_compatible); - result = conjunction(conjuncts); - } - } - - return result; } \ No newline at end of file diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/contracts.h similarity index 82% rename from src/goto-instrument/code_contracts.h rename to src/goto-instrument/contracts.h index 8aa56f62dc1..c063d3b1490 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/contracts.h @@ -243,75 +243,4 @@ class code_contractst const irep_idt &mode); }; -/// \brief A base class for assigns clause targets -class assigns_clause_targett -{ -public: - assigns_clause_targett( - const exprt &object_ptr, - code_contractst &contract, - messaget &log_parameter, - const irep_idt &function_id); - ~assigns_clause_targett(); - - std::vector temporary_declarations() const; - exprt alias_expression(const exprt &lhs); - exprt compatible_expression(const assigns_clause_targett &called_target); - goto_programt havoc_code(source_locationt location) const; - const exprt &get_direct_pointer() const; - goto_programt &get_init_block(); - - static exprt pointer_for(const exprt &exp) - { - return address_of_exprt(exp); - } - -protected: - const exprt pointer_object; - const code_contractst &contract; - goto_programt init_block; - messaget &log; - symbol_exprt local_target; -}; - -class assigns_clauset -{ -public: - assigns_clauset( - const exprt &assigns, - code_contractst &contract, - const irep_idt function_id, - messaget log_parameter); - ~assigns_clauset(); - - assigns_clause_targett *add_target(exprt current_operation); - assigns_clause_targett *add_pointer_target(exprt current_operation); - goto_programt init_block(source_locationt location); - goto_programt &temporary_declarations( - source_locationt location, - irep_idt function_name, - irep_idt language_mode); - goto_programt dead_stmts( - source_locationt location, - irep_idt function_name, - irep_idt language_mode); - goto_programt havoc_code( - source_locationt location, - irep_idt function_name, - irep_idt language_mode); - exprt alias_expression(const exprt &lhs); - - exprt compatible_expression(const assigns_clauset &called_assigns); - -protected: - const exprt &assigns_expr; - - std::vector targets; - goto_programt standin_declarations; - - code_contractst &parent; - const irep_idt function_id; - messaget log; -}; - #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H diff --git a/src/goto-instrument/contracts_assigns.cpp b/src/goto-instrument/contracts_assigns.cpp new file mode 100644 index 00000000000..c0b97680e26 --- /dev/null +++ b/src/goto-instrument/contracts_assigns.cpp @@ -0,0 +1,331 @@ +/*******************************************************************\ + +Module: Specify write set in function contracts. + +Author: Felipe R. Monteiro + +Date: July 2021 + +\*******************************************************************/ + +/// \file +/// Specify write set in function contracts + +#include "contracts_assigns.h" + +#include +#include +#include + +assigns_clause_targett::assigns_clause_targett( + const exprt &object_ptr, + code_contractst &contract, + messaget &log_parameter, + const irep_idt &function_id) + : pointer_object(pointer_for(object_ptr)), + contract(contract), + init_block(), + log(log_parameter), + local_target(typet()) +{ + INVARIANT( + pointer_object.type().id() == ID_pointer, + "Assigns clause targets should be stored as pointer expressions."); + + const symbolt &function_symbol = contract.ns.lookup(function_id); + + // Declare a new symbol to stand in for the reference + symbolt standin_symbol = contract.new_tmp_symbol( + pointer_object.type(), + function_symbol.location, + function_id, + function_symbol.mode); + + local_target = standin_symbol.symbol_expr(); + + // Build standin variable initialization block + init_block.add( + goto_programt::make_decl(local_target, function_symbol.location)); + init_block.add(goto_programt::make_assignment( + code_assignt(local_target, pointer_object), function_symbol.location)); +} + +assigns_clause_targett::~assigns_clause_targett() +{ +} + +std::vector assigns_clause_targett::temporary_declarations() const +{ + std::vector result; + result.push_back(local_target); + return result; +} + +exprt assigns_clause_targett::alias_expression(const exprt &ptr) +{ + return same_object(ptr, local_target); +} + +exprt assigns_clause_targett::compatible_expression( + const assigns_clause_targett &called_target) +{ + return alias_expression(called_target.get_direct_pointer()); +} + +goto_programt +assigns_clause_targett::havoc_code(source_locationt location) const +{ + goto_programt assigns_havoc; + + exprt lhs = dereference_exprt(pointer_object); + side_effect_expr_nondett rhs(lhs.type(), location); + + goto_programt::targett target = + assigns_havoc.add(goto_programt::make_assignment( + code_assignt(std::move(lhs), std::move(rhs)), location)); + target->code_nonconst().add_source_location() = location; + + return assigns_havoc; +} + +const exprt &assigns_clause_targett::get_direct_pointer() const +{ + return pointer_object; +} + +goto_programt &assigns_clause_targett::get_init_block() +{ + return init_block; +} + +assigns_clauset::assigns_clauset( + const exprt &assigns, + code_contractst &contract, + const irep_idt function_id, + messaget log_parameter) + : assigns_expr(assigns), + parent(contract), + function_id(function_id), + log(log_parameter) +{ + for(exprt current_operation : assigns_expr.operands()) + { + add_target(current_operation); + } +} + +assigns_clauset::~assigns_clauset() +{ + for(assigns_clause_targett *target : targets) + { + delete target; + } +} + +assigns_clause_targett *assigns_clauset::add_target(exprt current_operation) +{ + assigns_clause_targett *target = new assigns_clause_targett( + (current_operation.id() == ID_address_of) + ? to_index_expr(to_address_of_expr(current_operation).object()).array() + : current_operation, + parent, + log, + function_id); + targets.push_back(target); + return target; +} + +assigns_clause_targett * +assigns_clauset::add_pointer_target(exprt current_operation) +{ + return add_target(dereference_exprt(current_operation)); +} + +goto_programt assigns_clauset::init_block(source_locationt location) +{ + goto_programt result; + for(assigns_clause_targett *target : targets) + { + for(goto_programt::instructiont inst : + target->get_init_block().instructions) + { + result.add(goto_programt::instructiont(inst)); + } + } + return result; +} + +goto_programt &assigns_clauset::temporary_declarations( + source_locationt location, + irep_idt function_name, + irep_idt language_mode) +{ + if(standin_declarations.empty()) + { + for(assigns_clause_targett *target : targets) + { + for(symbol_exprt symbol : target->temporary_declarations()) + { + standin_declarations.add( + goto_programt::make_decl(symbol, symbol.source_location())); + } + } + } + return standin_declarations; +} + +goto_programt assigns_clauset::dead_stmts( + source_locationt location, + irep_idt function_name, + irep_idt language_mode) +{ + goto_programt dead_statements; + for(assigns_clause_targett *target : targets) + { + for(symbol_exprt symbol : target->temporary_declarations()) + { + dead_statements.add( + goto_programt::make_dead(symbol, symbol.source_location())); + } + } + return dead_statements; +} + +goto_programt assigns_clauset::havoc_code( + source_locationt location, + irep_idt function_name, + irep_idt language_mode) +{ + goto_programt havoc_statements; + for(assigns_clause_targett *target : targets) + { + // (1) If the assigned target is not a dereference, + // only include the havoc_statement + + // (2) If the assigned target is a dereference, do the following: + + // if(!__CPROVER_w_ok(target, 0)) goto z; + // havoc_statements + // z: skip + + // create the z label + goto_programt tmp_z; + goto_programt::targett z = tmp_z.add(goto_programt::make_skip(location)); + + const auto &target_ptr = target->get_direct_pointer(); + + if(to_address_of_expr(target_ptr).object().id() == ID_dereference) + { + // create the condition + exprt condition = + not_exprt(w_ok_exprt(target_ptr, from_integer(0, unsigned_int_type()))); + havoc_statements.add(goto_programt::make_goto(z, condition, location)); + } + + // create havoc_statements + for(goto_programt::instructiont instruction : + target->havoc_code(location).instructions) + { + havoc_statements.add(std::move(instruction)); + } + + if(to_address_of_expr(target_ptr).object().id() == ID_dereference) + { + // add the z label instruction + havoc_statements.destructive_append(tmp_z); + } + } + return havoc_statements; +} + +exprt assigns_clauset::alias_expression(const exprt &lhs) +{ + if(targets.empty()) + { + return false_exprt(); + } + + exprt left_ptr = assigns_clause_targett::pointer_for(lhs); + + bool first_iter = true; + exprt result = false_exprt(); + for(assigns_clause_targett *target : targets) + { + if(first_iter) + { + result = target->alias_expression(left_ptr); + first_iter = false; + } + else + { + result = or_exprt(result, target->alias_expression(left_ptr)); + } + } + return result; +} + +exprt assigns_clauset::compatible_expression( + const assigns_clauset &called_assigns) +{ + if(called_assigns.targets.empty()) + { + return true_exprt(); + } + + bool first_clause = true; + exprt result = true_exprt(); + for(assigns_clause_targett *called_target : called_assigns.targets) + { + bool first_iter = true; + exprt current_target_compatible = false_exprt(); + for(assigns_clause_targett *target : targets) + { + if(first_iter) + { + // TODO: Optimize the validation below and remove code duplication + // See GitHub issue #6105 for further details + + // Validating the called target through __CPROVER_w_ok() is + // only useful when the called target is a dereference + const auto &called_target_ptr = called_target->get_direct_pointer(); + if( + to_address_of_expr(called_target_ptr).object().id() == ID_dereference) + { + // or_exprt is short-circuited, therefore + // target->compatible_expression(*called_target) would not be + // checked on invalid called_targets. + current_target_compatible = or_exprt( + not_exprt(w_ok_exprt( + called_target_ptr, from_integer(0, unsigned_int_type()))), + target->compatible_expression(*called_target)); + } + else + { + current_target_compatible = + target->compatible_expression(*called_target); + } + first_iter = false; + } + else + { + current_target_compatible = or_exprt( + current_target_compatible, + target->compatible_expression(*called_target)); + } + } + if(first_clause) + { + result = current_target_compatible; + first_clause = false; + } + else + { + exprt::operandst conjuncts; + conjuncts.push_back(result); + conjuncts.push_back(current_target_compatible); + result = conjunction(conjuncts); + } + } + + return result; +} \ No newline at end of file diff --git a/src/goto-instrument/contracts_assigns.h b/src/goto-instrument/contracts_assigns.h new file mode 100644 index 00000000000..7d48fccda48 --- /dev/null +++ b/src/goto-instrument/contracts_assigns.h @@ -0,0 +1,90 @@ +/*******************************************************************\ + +Module: Specify write set in function contracts. + +Author: Felipe R. Monteiro + +Date: July 2021 + +\*******************************************************************/ + +/// \file +/// Specify write set in function contracts + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H + +#include "contracts.h" + +/// \brief A base class for assigns clause targets +class assigns_clause_targett +{ +public: + assigns_clause_targett( + const exprt &object_ptr, + code_contractst &contract, + messaget &log_parameter, + const irep_idt &function_id); + ~assigns_clause_targett(); + + std::vector temporary_declarations() const; + exprt alias_expression(const exprt &lhs); + exprt compatible_expression(const assigns_clause_targett &called_target); + goto_programt havoc_code(source_locationt location) const; + const exprt &get_direct_pointer() const; + goto_programt &get_init_block(); + + static exprt pointer_for(const exprt &exp) + { + return address_of_exprt(exp); + } + +protected: + const exprt pointer_object; + const code_contractst &contract; + goto_programt init_block; + messaget &log; + symbol_exprt local_target; +}; + +class assigns_clauset +{ +public: + assigns_clauset( + const exprt &assigns, + code_contractst &contract, + const irep_idt function_id, + messaget log_parameter); + ~assigns_clauset(); + + assigns_clause_targett *add_target(exprt current_operation); + assigns_clause_targett *add_pointer_target(exprt current_operation); + goto_programt init_block(source_locationt location); + goto_programt &temporary_declarations( + source_locationt location, + irep_idt function_name, + irep_idt language_mode); + goto_programt dead_stmts( + source_locationt location, + irep_idt function_name, + irep_idt language_mode); + goto_programt havoc_code( + source_locationt location, + irep_idt function_name, + irep_idt language_mode); + exprt alias_expression(const exprt &lhs); + + exprt compatible_expression(const assigns_clauset &called_assigns); + +protected: + const exprt &assigns_expr; + + std::vector targets; + goto_programt standin_declarations; + + code_contractst &parent; + const irep_idt function_id; + messaget log; +}; + +#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H \ No newline at end of file diff --git a/src/goto-instrument/contracts_memory_predicates.h b/src/goto-instrument/contracts_memory_predicates.h index d6a0d8e92b7..28974ecf4de 100644 --- a/src/goto-instrument/contracts_memory_predicates.h +++ b/src/goto-instrument/contracts_memory_predicates.h @@ -14,7 +14,7 @@ Date: July 2021 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H -#include "code_contracts.h" +#include "contracts.h" class is_fresh_baset { diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 0002b11e5ce..778d043885f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "aggressive_slicer.h" -#include "code_contracts.h" +#include "contracts.h" #include "generate_function_bodies.h" #include "insert_final_assert_false.h" #include "nondet_volatile.h" From 58612c4da678afe708a12a9a2764c554869d84d2 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 16 Jul 2021 20:32:44 +0000 Subject: [PATCH 5/6] Refactoring frame-condition checks Signed-off-by: Felipe R. Monteiro --- src/goto-instrument/contracts.cpp | 64 ++++++++++++++++--------------- src/goto-instrument/contracts.h | 7 +++- 2 files changed, 39 insertions(+), 32 deletions(-) diff --git a/src/goto-instrument/contracts.cpp b/src/goto-instrument/contracts.cpp index 645f3400f7b..0aaaff8baaa 100644 --- a/src/goto-instrument/contracts.cpp +++ b/src/goto-instrument/contracts.cpp @@ -825,13 +825,13 @@ bool code_contractst::check_for_looped_mallocs(const goto_programt &program) return false; } -bool code_contractst::add_pointer_checks(const std::string &function_name) +bool code_contractst::check_frame_conditions_function(const irep_idt &function) { // Get the function object before instrumentation. - auto old_function = goto_functions.function_map.find(function_name); + auto old_function = goto_functions.function_map.find(function); if(old_function == goto_functions.function_map.end()) { - log.error() << "Could not find function '" << function_name + log.error() << "Could not find function '" << function << "' in goto-program; not enforcing contracts." << messaget::eom; return true; @@ -842,22 +842,25 @@ bool code_contractst::add_pointer_checks(const std::string &function_name) return false; } - const irep_idt function_id(function_name); - const symbolt &function_symbol = ns.lookup(function_id); - const auto &type = to_code_with_contract_type(function_symbol.type); + if(check_for_looped_mallocs(program)) + { + return true; + } - exprt assigns_expr = type.assigns(); + // Insert aliasing assertions + check_frame_conditions(program, ns.lookup(function)); - assigns_clauset assigns(assigns_expr, *this, function_id, log); + return false; +} - goto_programt::instructionst::iterator instruction_it = - program.instructions.begin(); +void code_contractst::check_frame_conditions( + goto_programt &program, + const symbolt &target) +{ + const auto &type = to_code_with_contract_type(target.type); + exprt assigns_expr = type.assigns(); - // Create temporary variables to hold the assigns - // clause targets before they can be modified. - goto_programt standin_decls = assigns.init_block(function_symbol.location); - goto_programt mark_dead = assigns.dead_stmts( - function_symbol.location, function_name, function_symbol.mode); + assigns_clauset assigns(assigns_expr, *this, target.name, log); // Create a list of variables that are okay to assign. std::set freely_assignable_symbols; @@ -866,16 +869,19 @@ bool code_contractst::add_pointer_checks(const std::string &function_name) freely_assignable_symbols.insert(param.get_identifier()); } + goto_programt::instructionst::iterator instruction_it = + program.instructions.begin(); + + // Create temporary variables to hold the assigns + // clause targets before they can be modified. + goto_programt standin_decls = assigns.init_block(target.location); + goto_programt mark_dead = + assigns.dead_stmts(target.location, target.name, target.mode); + int lines_to_iterate = standin_decls.instructions.size(); program.insert_before_swap(instruction_it, standin_decls); std::advance(instruction_it, lines_to_iterate); - if(check_for_looped_mallocs(program)) - { - return true; - } - - // Insert aliasing assertions for(; instruction_it != program.instructions.end(); ++instruction_it) { if(instruction_it->is_decl()) @@ -909,7 +915,7 @@ bool code_contractst::add_pointer_checks(const std::string &function_name) instruction_it, program, assigns_expr, - function_id, + target.name, freely_assignable_symbols, assigns); } @@ -924,26 +930,24 @@ bool code_contractst::add_pointer_checks(const std::string &function_name) // Make sure the temporary symbols are marked dead lines_to_iterate = mark_dead.instructions.size(); program.insert_before_swap(instruction_it, mark_dead); - - return false; } -bool code_contractst::enforce_contract(const std::string &fun_to_enforce) +bool code_contractst::enforce_contract(const irep_idt &function) { // Add statements to the source function // to ensure assigns clause is respected. - add_pointer_checks(fun_to_enforce); + check_frame_conditions_function(function); // Rename source function std::stringstream ss; - ss << CPROVER_PREFIX << "contracts_original_" << fun_to_enforce; + ss << CPROVER_PREFIX << "contracts_original_" << function; const irep_idt mangled(ss.str()); - const irep_idt original(fun_to_enforce); + const irep_idt original(function); auto old_function = goto_functions.function_map.find(original); if(old_function == goto_functions.function_map.end()) { - log.error() << "Could not find function '" << fun_to_enforce + log.error() << "Could not find function '" << function << "' in goto-program; not enforcing contracts." << messaget::eom; return true; @@ -972,7 +976,7 @@ bool code_contractst::enforce_contract(const std::string &fun_to_enforce) auto nexist_old_function = goto_functions.function_map.find(original); INVARIANT( nexist_old_function == goto_functions.function_map.end(), - "There should be no function called " + fun_to_enforce + + "There should be no function called " + id2string(function) + " in the function map because that function should have had its" " name mangled"); diff --git a/src/goto-instrument/contracts.h b/src/goto-instrument/contracts.h index c063d3b1490..68da19e8353 100644 --- a/src/goto-instrument/contracts.h +++ b/src/goto-instrument/contracts.h @@ -147,11 +147,14 @@ class code_contractst std::unordered_set summarized; /// \brief Enforce contract of a single function - bool enforce_contract(const std::string &); + bool enforce_contract(const irep_idt &function); + + /// Instrument functions to check frame conditions. + bool check_frame_conditions_function(const irep_idt &function); /// Insert assertion statements into the goto program to ensure that /// assigned memory is within the assignable memory frame. - bool add_pointer_checks(const std::string &); + void check_frame_conditions(goto_programt &program, const symbolt &target); /// Check if there are any malloc statements which may be repeated because of /// a goto statement that jumps back. From 5d0ffe0c14822d5c0d1ed495c7e164ae9010a483 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 16 Jul 2021 20:48:48 +0000 Subject: [PATCH 6/6] Adds a code contract module to goto-instrument Signed-off-by: Felipe R. Monteiro --- CODEOWNERS | 4 ++-- src/goto-instrument/Makefile | 6 +++--- .../assigns.cpp} | 4 ++-- .../assigns.h} | 2 +- .../{ => contracts}/contracts.cpp | 18 +++++++++--------- .../{ => contracts}/contracts.h | 10 +++++----- .../memory_predicates.cpp} | 2 +- .../memory_predicates.h} | 2 +- .../contracts/module_dependencies.txt | 8 ++++++++ .../goto_instrument_parse_options.h | 2 +- src/goto-instrument/module_dependencies.txt | 1 + 11 files changed, 34 insertions(+), 25 deletions(-) rename src/goto-instrument/{contracts_assigns.cpp => contracts/assigns.cpp} (99%) rename src/goto-instrument/{contracts_assigns.h => contracts/assigns.h} (97%) rename src/goto-instrument/{ => contracts}/contracts.cpp (99%) rename src/goto-instrument/{ => contracts}/contracts.h (97%) rename src/goto-instrument/{contracts_memory_predicates.cpp => contracts/memory_predicates.cpp} (99%) rename src/goto-instrument/{contracts_memory_predicates.h => contracts/memory_predicates.h} (98%) create mode 100644 src/goto-instrument/contracts/module_dependencies.txt diff --git a/CODEOWNERS b/CODEOWNERS index 93afa74e9a1..9513faf65e6 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -45,8 +45,8 @@ /src/goto-analyzer/ @martin-cs @chrisr-diffblue @peterschrammel /src/goto-harness/ @martin-cs @chrisr-diffblue @peterschrammel /src/goto-instrument/ @martin-cs @chrisr-diffblue @peterschrammel -/src/goto-instrument/code_contracts.* @tautschnig @feliperodri @SaswatPadhi -doc/cprover-manual/contracts* @tautschnig @feliperodri @SaswatPadhi +/src/goto-instrument/contracts/ @tautschnig @feliperodri @SaswatPadhi +/doc/cprover-manual/contracts* @tautschnig @feliperodri @SaswatPadhi /src/goto-diff/ @tautschnig @peterschrammel /src/jsil/ @kroening @tautschnig /src/memory-analyzer/ @tautschnig @chrisr-diffblue diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 99e17cd2d5b..2da96334d52 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -16,9 +16,9 @@ SRC = accelerate/accelerate.cpp \ alignment_checks.cpp \ branch.cpp \ call_sequences.cpp \ - contracts_assigns.cpp \ - contracts_memory_predicates.cpp \ - contracts.cpp \ + contracts/assigns.cpp \ + contracts/memory_predicates.cpp \ + contracts/contracts.cpp \ concurrency.cpp \ count_eloc.cpp \ cover.cpp \ diff --git a/src/goto-instrument/contracts_assigns.cpp b/src/goto-instrument/contracts/assigns.cpp similarity index 99% rename from src/goto-instrument/contracts_assigns.cpp rename to src/goto-instrument/contracts/assigns.cpp index c0b97680e26..e41f9ebf8e0 100644 --- a/src/goto-instrument/contracts_assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -11,7 +11,7 @@ Date: July 2021 /// \file /// Specify write set in function contracts -#include "contracts_assigns.h" +#include "assigns.h" #include #include @@ -328,4 +328,4 @@ exprt assigns_clauset::compatible_expression( } return result; -} \ No newline at end of file +} diff --git a/src/goto-instrument/contracts_assigns.h b/src/goto-instrument/contracts/assigns.h similarity index 97% rename from src/goto-instrument/contracts_assigns.h rename to src/goto-instrument/contracts/assigns.h index 7d48fccda48..4be813baa0d 100644 --- a/src/goto-instrument/contracts_assigns.h +++ b/src/goto-instrument/contracts/assigns.h @@ -87,4 +87,4 @@ class assigns_clauset messaget log; }; -#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H \ No newline at end of file +#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H diff --git a/src/goto-instrument/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp similarity index 99% rename from src/goto-instrument/contracts.cpp rename to src/goto-instrument/contracts/contracts.cpp index 0aaaff8baaa..596b32c9520 100644 --- a/src/goto-instrument/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -11,8 +11,10 @@ Date: February 2016 /// \file /// Verify and use annotated invariants and pre/post-conditions -#include "contracts_assigns.h" -#include "contracts_memory_predicates.h" +#include "contracts.h" + +#include "assigns.h" +#include "memory_predicates.h" #include #include @@ -21,8 +23,6 @@ Date: February 2016 #include -#include - #include #include @@ -162,8 +162,8 @@ void code_contractst::check_apply_loop_contracts( // Generate: an assignment to store the decreases clause's value before the // loop - code_assignt old_decreases_assignment{ - old_decreases_symbol, decreases_clause}; + code_assignt old_decreases_assignment{old_decreases_symbol, + decreases_clause}; old_decreases_assignment.add_source_location() = loop_head->source_location; converter.goto_convert(old_decreases_assignment, havoc_code, mode); } @@ -200,8 +200,8 @@ void code_contractst::check_apply_loop_contracts( // Generate: an assignment to store the decreases clause's value after one // iteration of the loop - code_assignt new_decreases_assignment{ - new_decreases_symbol, decreases_clause}; + code_assignt new_decreases_assignment{new_decreases_symbol, + decreases_clause}; new_decreases_assignment.add_source_location() = loop_head->source_location; converter.goto_convert(new_decreases_assignment, havoc_code, mode); @@ -1261,4 +1261,4 @@ bool code_contractst::enforce_contracts( fail = enforce_contract(fun); } return fail; -} \ No newline at end of file +} diff --git a/src/goto-instrument/contracts.h b/src/goto-instrument/contracts/contracts.h similarity index 97% rename from src/goto-instrument/contracts.h rename to src/goto-instrument/contracts/contracts.h index 68da19e8353..6afd15a8f6a 100644 --- a/src/goto-instrument/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -11,14 +11,16 @@ Date: February 2016 /// \file /// Verify and use annotated invariants and pre/post-conditions -#ifndef CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H -#define CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H #include #include #include #include +#include + #include #include #include @@ -29,8 +31,6 @@ Date: February 2016 #include #include -#include "loop_utils.h" - #define FLAG_LOOP_CONTRACTS "apply-loop-contracts" #define HELP_LOOP_CONTRACTS \ " --apply-loop-contracts\n" \ @@ -246,4 +246,4 @@ class code_contractst const irep_idt &mode); }; -#endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H +#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H diff --git a/src/goto-instrument/contracts_memory_predicates.cpp b/src/goto-instrument/contracts/memory_predicates.cpp similarity index 99% rename from src/goto-instrument/contracts_memory_predicates.cpp rename to src/goto-instrument/contracts/memory_predicates.cpp index e437f188686..2c98e0a24c6 100644 --- a/src/goto-instrument/contracts_memory_predicates.cpp +++ b/src/goto-instrument/contracts/memory_predicates.cpp @@ -11,7 +11,7 @@ Date: July 2021 /// \file /// Predicates to specify memory footprint in function contracts -#include "contracts_memory_predicates.h" +#include "memory_predicates.h" #include #include diff --git a/src/goto-instrument/contracts_memory_predicates.h b/src/goto-instrument/contracts/memory_predicates.h similarity index 98% rename from src/goto-instrument/contracts_memory_predicates.h rename to src/goto-instrument/contracts/memory_predicates.h index 28974ecf4de..98820cbc955 100644 --- a/src/goto-instrument/contracts_memory_predicates.h +++ b/src/goto-instrument/contracts/memory_predicates.h @@ -156,4 +156,4 @@ class function_binding_visitort : const_expr_visitort } }; -#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H \ No newline at end of file +#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H diff --git a/src/goto-instrument/contracts/module_dependencies.txt b/src/goto-instrument/contracts/module_dependencies.txt new file mode 100644 index 00000000000..a797c099df6 --- /dev/null +++ b/src/goto-instrument/contracts/module_dependencies.txt @@ -0,0 +1,8 @@ +analyses +ansi-c +goto-instrument/contracts +goto-instrument +goto-programs +langapi +linking +util diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 778d043885f..5ce7b72d273 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "aggressive_slicer.h" -#include "contracts.h" +#include "contracts/contracts.h" #include "generate_function_bodies.h" #include "insert_final_assert_false.h" #include "nondet_volatile.h" diff --git a/src/goto-instrument/module_dependencies.txt b/src/goto-instrument/module_dependencies.txt index 5d9e0a710aa..68812d59375 100644 --- a/src/goto-instrument/module_dependencies.txt +++ b/src/goto-instrument/module_dependencies.txt @@ -2,6 +2,7 @@ accelerate analyses ansi-c assembler +contracts cpp goto-instrument goto-programs