From 00959cc79de5ab469bf544e755dbbd7bb1e6829d Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 17 Jun 2022 20:44:23 +0000 Subject: [PATCH] CONTRACTS: detect and handle locals in assigns clause checking for loops When no assigns clause was provided, we were trying to infer variables touched by the loop and generate an assigns clause from that. Some of these variables could be locals, which have no meaning outside the loop, and we were trying to snapshot these variables outside of the loop. We now detect loop locals and remove them from the inferred frame condition the loop. --- .../contracts/detect_loop_locals/main.c | 12 ++ .../contracts/detect_loop_locals/test.desc | 10 + .../contracts/detect_loop_locals2/main.c | 28 +++ .../contracts/detect_loop_locals2/test.desc | 11 + .../invar_check_nested_loops/test.desc | 7 +- .../loop_guard_with_side_effects/test.desc | 2 +- .../test.desc | 1 - src/goto-instrument/contracts/cfg_info.h | 197 ++++++++++++++++++ src/goto-instrument/contracts/contracts.cpp | 42 ++-- .../contracts/havoc_assigns_clause_targets.h | 9 +- .../contracts/instrument_spec_assigns.cpp | 116 ++++------- .../contracts/instrument_spec_assigns.h | 78 ++----- src/goto-instrument/contracts/utils.h | 123 ----------- 13 files changed, 350 insertions(+), 286 deletions(-) create mode 100644 regression/contracts/detect_loop_locals/main.c create mode 100644 regression/contracts/detect_loop_locals/test.desc create mode 100644 regression/contracts/detect_loop_locals2/main.c create mode 100644 regression/contracts/detect_loop_locals2/test.desc create mode 100644 src/goto-instrument/contracts/cfg_info.h diff --git a/regression/contracts/detect_loop_locals/main.c b/regression/contracts/detect_loop_locals/main.c new file mode 100644 index 00000000000..602df7f5db9 --- /dev/null +++ b/regression/contracts/detect_loop_locals/main.c @@ -0,0 +1,12 @@ +#include + +int main() +{ + unsigned char *i = malloc(5); + + while(i != i + 5) + __CPROVER_loop_invariant(1 == 1) + { + const char lower = *i++; + } +} diff --git a/regression/contracts/detect_loop_locals/test.desc b/regression/contracts/detect_loop_locals/test.desc new file mode 100644 index 00000000000..c116642ea92 --- /dev/null +++ b/regression/contracts/detect_loop_locals/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--apply-loop-contracts +^\[main.assigns.\d+\].*line 10 Check that i is assignable: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks that loop local variables do not cause explicit checks diff --git a/regression/contracts/detect_loop_locals2/main.c b/regression/contracts/detect_loop_locals2/main.c new file mode 100644 index 00000000000..fb37cf3442a --- /dev/null +++ b/regression/contracts/detect_loop_locals2/main.c @@ -0,0 +1,28 @@ +static void foo() +{ + unsigned i; + + for(i = 0; i < 16; i++) + __CPROVER_loop_invariant(1 == 1) + { + int v = 1; + } +} + +static void bar() +{ + unsigned i; + + for(i = 0; i < 16; i++) + __CPROVER_loop_invariant(1 == 1) + { + int v = 1; + } +} + +int main() +{ + bar(); + foo(); + foo(); +} diff --git a/regression/contracts/detect_loop_locals2/test.desc b/regression/contracts/detect_loop_locals2/test.desc new file mode 100644 index 00000000000..825d79b8bca --- /dev/null +++ b/regression/contracts/detect_loop_locals2/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--apply-loop-contracts +^\[bar.assigns.\d+\].*Check that i is assignable: SUCCESS$ +^\[foo.assigns.\d+\].*Check that i is assignable: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks that loop local variables do not cause explicit checks diff --git a/regression/contracts/invar_check_nested_loops/test.desc b/regression/contracts/invar_check_nested_loops/test.desc index 2ef3cb314e6..d7360332c84 100644 --- a/regression/contracts/invar_check_nested_loops/test.desc +++ b/regression/contracts/invar_check_nested_loops/test.desc @@ -9,9 +9,10 @@ main.c ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$ -^\[main.assigns.\d+] .* line 23 Check that s is assignable: SUCCESS$ -^\[main.assigns.\d+] .* line 24 Check that a is assignable: SUCCESS$ -^\[main.assigns.\d+] .* line 27 Check that s is assignable: SUCCESS$ +^\[main\.assigns\.\d+\].*line 17 Check that s is assignable: SUCCESS$ +^\[main\.assigns\.\d+\].*line 23 Check that s is assignable: SUCCESS$ +^\[main\.assigns\.\d+\].*line 24 Check that a is assignable: SUCCESS$ +^\[main\.assigns\.\d+\].*line 27 Check that s is assignable: SUCCESS$ ^\[main\.assertion.\d+\] .* assertion s == n: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/loop_guard_with_side_effects/test.desc b/regression/contracts/loop_guard_with_side_effects/test.desc index 78a7f3b9dba..e1c9d00edb1 100644 --- a/regression/contracts/loop_guard_with_side_effects/test.desc +++ b/regression/contracts/loop_guard_with_side_effects/test.desc @@ -4,7 +4,6 @@ main.c \[check.assigns\.\d+\] line \d+ Check that \*j is assignable: SUCCESS$ \[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS \[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS -\[check.assigns\.\d+\] line \d+ Check that return_value_check is assignable: SUCCESS$ \[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$ \[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$ \[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$ @@ -16,6 +15,7 @@ main.c \[main.assertion\.\d+\] line \d+ assertion j == k \+ 1: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ -- -- This test demonstrates a case where the loop guard has side effects. diff --git a/regression/contracts/loop_guard_with_side_effects_fail/test.desc b/regression/contracts/loop_guard_with_side_effects_fail/test.desc index aac46db3c6b..0d753f4ad57 100644 --- a/regression/contracts/loop_guard_with_side_effects_fail/test.desc +++ b/regression/contracts/loop_guard_with_side_effects_fail/test.desc @@ -2,7 +2,6 @@ CORE main.c --apply-loop-contracts _ --unsigned-overflow-check \[check.assigns\.\d+\] line \d+ Check that \*j is assignable: FAILURE$ -\[check.assigns\.\d+\] line \d+ Check that return_value_check is assignable: SUCCESS$ \[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$ \[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$ \[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$ diff --git a/src/goto-instrument/contracts/cfg_info.h b/src/goto-instrument/contracts/cfg_info.h new file mode 100644 index 00000000000..89c22036ad7 --- /dev/null +++ b/src/goto-instrument/contracts/cfg_info.h @@ -0,0 +1,197 @@ +/*******************************************************************\ + +Module: CFG-based information for assigns clause checking simplification + +Author: Remi Delmas + +Date: June 2022 + +\*******************************************************************/ + +/// \file +/// Classes providing CFG-based information about symbols to guide +/// simplifications in function and loop assigns clause checking + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CFG_INFO_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CFG_INFO_H + +#include + +#include +#include +#include + +#include + +#include +#include +#include +#include + +#include +#include + +/// Stores information about a goto function computed from its CFG. +/// +/// The methods of this class provide information about identifiers +/// to allow simplifying assigns clause checking assertions. +class cfg_infot +{ +public: + /// Returns true iff `ident` is locally declared. + virtual bool is_local(const irep_idt &ident) const = 0; + + /// Returns true iff the given `ident` is either non-locally declared + /// or is locally-declared but dirty. + virtual bool is_not_local_or_dirty_local(const irep_idt &ident) const = 0; + + /// Returns true iff `expr` is an access to a locally declared symbol + /// and does not contain `dereference` or `address_of` operations. + bool is_local_composite_access(const exprt &expr) const + { + // case-splitting on the lhs structure copied from symex_assignt::assign_rec + if(expr.id() == ID_symbol) + { + return is_local(to_symbol_expr(expr).get_identifier()); + } + else if(expr.id() == ID_index) + { + return is_local_composite_access(to_index_expr(expr).array()); + } + else if(expr.id() == ID_member) + { + const typet &type = to_member_expr(expr).struct_op().type(); + if( + type.id() == ID_struct || type.id() == ID_struct_tag || + type.id() == ID_union || type.id() == ID_union_tag) + { + return is_local_composite_access(to_member_expr(expr).compound()); + } + else + { + throw unsupported_operation_exceptiont( + "is_local_composite_access: unexpected assignment to member of '" + + type.id_string() + "'"); + } + } + else if(expr.id() == ID_if) + { + return is_local_composite_access(to_if_expr(expr).true_case()) && + is_local_composite_access(to_if_expr(expr).false_case()); + } + else if(expr.id() == ID_typecast) + { + return is_local_composite_access(to_typecast_expr(expr).op()); + } + else if( + expr.id() == ID_byte_extract_little_endian || + expr.id() == ID_byte_extract_big_endian) + { + return is_local_composite_access(to_byte_extract_expr(expr).op()); + } + else if(expr.id() == ID_complex_real) + { + return is_local_composite_access(to_complex_real_expr(expr).op()); + } + else if(expr.id() == ID_complex_imag) + { + return is_local_composite_access(to_complex_imag_expr(expr).op()); + } + else + { + // matches ID_address_of, ID_dereference, etc. + return false; + } + } +}; + +// For goto_functions +class function_cfg_infot : public cfg_infot +{ +public: + explicit function_cfg_infot(const goto_functiont &_goto_function) + : dirty_analysis(_goto_function), locals(_goto_function) + { + parameters.insert( + _goto_function.parameter_identifiers.begin(), + _goto_function.parameter_identifiers.end()); + } + + /// Returns true iff `ident` is a local or parameter of the goto_function. + bool is_local(const irep_idt &ident) const override + { + return locals.is_local(ident) || + (parameters.find(ident) != parameters.end()); + } + + /// Returns true iff the given `ident` is either not a goto_function local + /// or is a local that is dirty. + bool is_not_local_or_dirty_local(const irep_idt &ident) const override + { + if(is_local(ident)) + return dirty_analysis.get_dirty_ids().find(ident) != + dirty_analysis.get_dirty_ids().end(); + else + return true; + } + +private: + const dirtyt dirty_analysis; + const localst locals; + std::unordered_set parameters; +}; + +// For a loop in a goto_function +class loop_cfg_infot : public cfg_infot +{ +public: + loop_cfg_infot(goto_functiont &_goto_function, const loopt &loop) + : dirty_analysis(_goto_function) + { + for(const auto &t : loop) + { + if(t->is_decl()) + locals.insert(t->decl_symbol().get_identifier()); + } + } + + /// Returns true iff `ident` is a loop local. + bool is_local(const irep_idt &ident) const override + { + return locals.find(ident) != locals.end(); + } + + /// Returns true iff the given `ident` is either not a loop local + /// or is a loop local that is dirty. + bool is_not_local_or_dirty_local(const irep_idt &ident) const override + { + if(is_local(ident)) + return dirty_analysis.get_dirty_ids().find(ident) != + dirty_analysis.get_dirty_ids().end(); + else + return true; + } + + void erase_locals(std::set &exprs) + { + auto it = exprs.begin(); + while(it != exprs.end()) + { + if( + it->id() == ID_symbol && is_local(to_symbol_expr(*it).get_identifier())) + { + it = exprs.erase(it); + } + else + { + it++; + } + } + } + +private: + const dirtyt dirty_analysis; + std::unordered_set locals; +}; + +#endif diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 7698d2b94d9..108a902d1d4 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -39,6 +39,7 @@ Date: February 2016 #include #include +#include "cfg_info.h" #include "havoc_assigns_clause_targets.h" #include "instrument_spec_assigns.h" #include "memory_predicates.h" @@ -270,9 +271,16 @@ void code_contractst::check_apply_loop_contracts( // CAR snapshot instructions for checking assigns clause goto_programt snapshot_instructions; + loop_cfg_infot cfg_info(goto_function, loop); + // track static local symbols instrument_spec_assignst instrument_spec_assigns( - function_name, goto_functions, symbol_table, log.get_message_handler()); + function_name, + goto_functions, + cfg_info, + symbol_table, + log.get_message_handler()); + instrument_spec_assigns.track_static_locals_between( loop_head, loop_end, snapshot_instructions); @@ -290,6 +298,9 @@ void code_contractst::check_apply_loop_contracts( // TODO: if the set contains pairs (i, a[i]), // we must at least widen them to (i, pointer_object(a)) + // remove loop-local symbols from the inferred set + cfg_info.erase_locals(to_havoc); + log.debug() << "No loop assigns clause provided. Inferred targets: {"; // Add inferred targets to the loop assigns clause. bool ran_once = false; @@ -441,16 +452,11 @@ void code_contractst::check_apply_loop_contracts( goto_function.body.destructive_insert( loop_head, add_pragma_disable_assigns_check(pre_loop_head_instrs)); - optionalt cfg_empty_info; - // Perform write set instrumentation on the entire loop. instrument_spec_assigns.instrument_instructions( goto_function.body, loop_head, loop_end, - skip_function_paramst::NO, - // do not use CFG info for now - cfg_empty_info, [&loop](const goto_programt::targett &t) { return loop.contains(t); }); // Now we begin instrumenting at the loop_end. @@ -894,11 +900,12 @@ void code_contractst::apply_function_contract( // ... for the assigns clause targets and static locals goto_programt havoc_instructions; - + function_cfg_infot cfg_info({}); havoc_assigns_clause_targetst havocker( target_function, targets.operands(), goto_functions, + cfg_info, location, symbol_table, log.get_message_handler()); @@ -1247,8 +1254,14 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function) const auto &function_with_contract = to_code_with_contract_type(function_symbol.type); + function_cfg_infot cfg_info(goto_function); + instrument_spec_assignst instrument_spec_assigns( - function, goto_functions, symbol_table, log.get_message_handler()); + function, + goto_functions, + cfg_info, + symbol_table, + log.get_message_handler()); // Detect and track static local variables before inlining goto_programt snapshot_static_locals; @@ -1276,13 +1289,6 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function) "Loops remain in function '" + id2string(function) + "', assigns clause checking instrumentation cannot be applied."); - // Create a deep copy of the inlined body before any instrumentation is added - // and compute static control flow graph information - goto_functiont goto_function_orig; - goto_function_orig.copy_from(goto_function); - cfg_infot cfg_info(ns, goto_function_orig); - optionalt cfg_info_opt{cfg_info}; - // Start instrumentation auto instruction_it = function_body.instructions.begin(); @@ -1313,11 +1319,7 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function) // Insert write set inclusion checks. instrument_spec_assigns.instrument_instructions( - function_body, - instruction_it, - function_body.instructions.end(), - skip_function_paramst::YES, - cfg_info_opt); + function_body, instruction_it, function_body.instructions.end()); } void code_contractst::enforce_contract(const irep_idt &function) diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h index d41f11d3735..5028b3c315b 100644 --- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h @@ -47,6 +47,7 @@ class havoc_assigns_clause_targetst : public instrument_spec_assignst /// \param _function_id Name of the replaced function /// \param _targets Assigns clause targets of the replaced function /// \param _functions Other functions forming the GOTO model + /// \param _cfg_info CFG-based information on function symbols (not used) /// \param _source_location Source location of the replaced function call /// (added to all generated instructions) /// \param _st Symbol table of the model (new symbols will be added) @@ -56,10 +57,16 @@ class havoc_assigns_clause_targetst : public instrument_spec_assignst const irep_idt &_function_id, const std::vector &_targets, const goto_functionst &_functions, + cfg_infot &_cfg_info, const source_locationt &_source_location, symbol_tablet &_st, message_handlert &_message_handler) - : instrument_spec_assignst(_function_id, _functions, _st, _message_handler), + : instrument_spec_assignst( + _function_id, + _functions, + _cfg_info, + _st, + _message_handler), targets(_targets), source_location(_source_location) { diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index 26e93618a67..f56f4a47d27 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -23,6 +23,7 @@ Date: January 2022 #include +#include "cfg_info.h" #include "utils.h" /// header for log messages @@ -143,13 +144,12 @@ void instrument_spec_assignst::track_heap_allocated( void instrument_spec_assignst::check_inclusion_assignment( const exprt &lhs, - optionalt &cfg_info_opt, goto_programt &dest) const { // create temporary car but do not track const auto car = create_car_expr(true_exprt{}, lhs); create_snapshot(car, dest); - inclusion_check_assertion(car, false, true, cfg_info_opt, dest); + inclusion_check_assertion(car, false, true, dest); } void instrument_spec_assignst::track_static_locals(goto_programt &dest) @@ -303,7 +303,7 @@ void instrument_spec_assignst::collect_static_symbols( void instrument_spec_assignst:: check_inclusion_heap_allocated_and_invalidate_aliases( const exprt &expr, - optionalt &cfg_info_opt, + goto_programt &dest) { // create temporary car but do not track @@ -313,7 +313,7 @@ void instrument_spec_assignst:: create_snapshot(car, dest); // check inclusion, allowing null and not allowing stack allocated locals - inclusion_check_assertion(car, true, false, cfg_info_opt, dest); + inclusion_check_assertion(car, true, false, dest); // invalidate aliases of the freed object invalidate_heap_and_spec_aliases(car, dest); @@ -323,8 +323,6 @@ void instrument_spec_assignst::instrument_instructions( goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, - skip_function_paramst skip_function_params, - optionalt &cfg_info_opt, const std::function &pred) { while(instruction_it != instruction_end) @@ -335,8 +333,6 @@ void instrument_spec_assignst::instrument_instructions( (pred && !pred(instruction_it))) { instruction_it++; - if(cfg_info_opt.has_value()) - cfg_info_opt.value().step(); continue; } @@ -344,9 +340,7 @@ void instrument_spec_assignst::instrument_instructions( // since we are going to instrument it now below. add_pragma_disable_assigns_check(*instruction_it); - if( - instruction_it->is_decl() && - must_track_decl(instruction_it, cfg_info_opt)) + if(instruction_it->is_decl() && must_track_decl(instruction_it)) { // grab the declared symbol const auto &decl_symbol = instruction_it->decl_symbol(); @@ -361,19 +355,15 @@ void instrument_spec_assignst::instrument_instructions( // care of the increment instruction_it--; } - else if( - instruction_it->is_assign() && - must_check_assign(instruction_it, skip_function_params, cfg_info_opt)) + else if(instruction_it->is_assign() && must_check_assign(instruction_it)) { - instrument_assign_statement(instruction_it, body, cfg_info_opt); + instrument_assign_statement(instruction_it, body); } else if(instruction_it->is_function_call()) { - instrument_call_statement(instruction_it, body, cfg_info_opt); + instrument_call_statement(instruction_it, body); } - else if( - instruction_it->is_dead() && - must_track_dead(instruction_it, cfg_info_opt)) + else if(instruction_it->is_dead() && must_track_dead(instruction_it)) { const auto &symbol = instruction_it->dead_symbol(); if(stack_allocated_is_tracked(symbol)) @@ -404,14 +394,12 @@ void instrument_spec_assignst::instrument_instructions( auto havoc_object = pointer_object(havoc_argument); havoc_object.add_source_location() = instruction_it->source_location(); goto_programt payload; - check_inclusion_assignment(havoc_object, cfg_info_opt, payload); + check_inclusion_assignment(havoc_object, payload); insert_before_swap_and_advance(body, instruction_it, payload); } // Move to the next instruction instruction_it++; - if(cfg_info_opt.has_value()) - cfg_info_opt.value().step(); } } @@ -642,7 +630,6 @@ void instrument_spec_assignst::inclusion_check_assertion( const car_exprt &car, bool allow_null_lhs, bool include_stack_allocated, - optionalt &cfg_info_opt, goto_programt &dest) const { source_locationt source_location(car.source_location()); @@ -672,8 +659,7 @@ void instrument_spec_assignst::inclusion_check_assertion( source_location.set_comment(comment); dest.add(goto_programt::make_assertion( - inclusion_check_full( - car, allow_null_lhs, include_stack_allocated, cfg_info_opt), + inclusion_check_full(car, allow_null_lhs, include_stack_allocated), source_location)); } @@ -699,8 +685,7 @@ exprt instrument_spec_assignst::inclusion_check_single( exprt instrument_spec_assignst::inclusion_check_full( const car_exprt &car, bool allow_null_lhs, - bool include_stack_allocated, - optionalt &cfg_info_opt) const + bool include_stack_allocated) const { bool no_targets = from_spec_assigns.empty() && from_heap_alloc.empty() && (!include_stack_allocated || @@ -744,12 +729,6 @@ exprt instrument_spec_assignst::inclusion_check_full( { for(const auto &pair : from_stack_alloc) { - // skip dead targets - if( - cfg_info_opt.has_value() && - !cfg_info_opt.value().is_maybe_alive(pair.first)) - continue; - disjuncts.push_back(inclusion_check_single(car, pair.second)); log.debug() << "\t(stack) " << from_expr_using_mode(ns, mode, pair.second.target()) @@ -877,40 +856,28 @@ void instrument_spec_assignst::invalidate_heap_and_spec_aliases( /// Returns true iff an `ASSIGN lhs := rhs` instruction must be instrumented. bool instrument_spec_assignst::must_check_assign( - const goto_programt::const_targett &target, - skip_function_paramst skip_function_params, - const optionalt cfg_info_opt) + const goto_programt::const_targett &target) { log.debug().source_location = target->source_location(); if(can_cast_expr(target->assign_lhs())) { const auto &symbol_expr = to_symbol_expr(target->assign_lhs()); - if( - skip_function_params == skip_function_paramst::NO && - ns.lookup(symbol_expr.get_identifier()).is_parameter) + + if(cfg_info.is_local(symbol_expr.get_identifier())) { - log.debug() << LOG_HEADER << "checking assignment to function parameter " + log.debug() << LOG_HEADER + << "skipping checking on assignment to local symbol " << format(symbol_expr) << messaget::eom; - return true; + return false; } - - if(cfg_info_opt.has_value()) + else { - if(cfg_info_opt.value().is_local(symbol_expr.get_identifier())) - { - log.debug() << LOG_HEADER - << "skipping checking on assignment to local symbol " - << format(symbol_expr) << messaget::eom; - return false; - } - else - { - log.debug() << LOG_HEADER << "checking assignment to non-local symbol " - << format(symbol_expr) << messaget::eom; - return true; - } + log.debug() << LOG_HEADER << "checking assignment to non-local symbol " + << format(symbol_expr) << messaget::eom; + return true; } + log.debug() << LOG_HEADER << "checking assignment to symbol " << format(symbol_expr) << messaget::eom; return true; @@ -934,9 +901,7 @@ bool instrument_spec_assignst::must_check_assign( // In all other cases (address of a non-local object, or dereference of // a non-locally computed address) the location must be given explicitly // in the assigns clause to be tracked and we must check the assignment. - if( - cfg_info_opt.has_value() && - cfg_info_opt.value().is_local_composite_access(target->assign_lhs())) + if(cfg_info.is_local_composite_access(target->assign_lhs())) { log.debug() << LOG_HEADER @@ -950,25 +915,19 @@ bool instrument_spec_assignst::must_check_assign( } } -/// Track the symbol iff we have no cfg_infot, or we have a cfg_infot and the -/// symbol is not a local or is a dirty local. +/// Track the symbol is not a local or is a dirty local. bool instrument_spec_assignst::must_track_decl_or_dead( - const irep_idt &ident, - const optionalt &cfg_info_opt) const + const irep_idt &ident) const { - return !cfg_info_opt.has_value() || - (cfg_info_opt.has_value() && - cfg_info_opt.value().is_not_local_or_dirty_local(ident)); + return cfg_info.is_not_local_or_dirty_local(ident); } /// Returns true iff a `DECL x` must be explicitly tracked in the write set. bool instrument_spec_assignst::must_track_decl( - const goto_programt::const_targett &target, - const optionalt &cfg_info_opt) const + const goto_programt::const_targett &target) const { log.debug().source_location = target->source_location(); - if(must_track_decl_or_dead( - target->decl_symbol().get_identifier(), cfg_info_opt)) + if(must_track_decl_or_dead(target->decl_symbol().get_identifier())) { log.debug() << LOG_HEADER << "explicitly tracking " << format(target->decl_symbol()) << " as assignable" @@ -987,29 +946,25 @@ bool instrument_spec_assignst::must_track_decl( /// Returns true iff a `DEAD x` must be processed to upate the local write set. /// The conditions are the same than for tracking a `DECL x` instruction. bool instrument_spec_assignst::must_track_dead( - const goto_programt::const_targett &target, - const optionalt &cfg_info_opt) const + const goto_programt::const_targett &target) const { - return must_track_decl_or_dead( - target->dead_symbol().get_identifier(), cfg_info_opt); + return must_track_decl_or_dead(target->dead_symbol().get_identifier()); } void instrument_spec_assignst::instrument_assign_statement( goto_programt::targett &instruction_it, - goto_programt &program, - optionalt &cfg_info_opt) const + goto_programt &program) const { auto lhs = instruction_it->assign_lhs(); lhs.add_source_location() = instruction_it->source_location(); goto_programt payload; - check_inclusion_assignment(lhs, cfg_info_opt, payload); + check_inclusion_assignment(lhs, payload); insert_before_swap_and_advance(program, instruction_it, payload); } void instrument_spec_assignst::instrument_call_statement( goto_programt::targett &instruction_it, - goto_programt &body, - optionalt &cfg_info_opt) + goto_programt &body) { PRECONDITION_WITH_DIAGNOSTICS( instruction_it->is_function_call(), @@ -1044,8 +999,7 @@ void instrument_spec_assignst::instrument_call_statement( auto object = pointer_object(ptr); object.add_source_location() = instruction_it->source_location(); goto_programt payload; - check_inclusion_heap_allocated_and_invalidate_aliases( - object, cfg_info_opt, payload); + check_inclusion_heap_allocated_and_invalidate_aliases(object, payload); insert_before_swap_and_advance(body, instruction_it, payload); } } diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.h b/src/goto-instrument/contracts/instrument_spec_assigns.h index 60cf2de0c6e..ea91cd0ce99 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.h +++ b/src/goto-instrument/contracts/instrument_spec_assigns.h @@ -14,22 +14,24 @@ Date: January 2022 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H -#include -#include -#include - -#include +#include #include -#include + +#include #include "utils.h" +#include +#include +#include + // forward declarations class conditional_target_group_exprt; class namespacet; class symbol_tablet; class symbolt; +class cfg_infot; /// Class that represents a single conditional target. class conditional_target_exprt : public exprt @@ -176,13 +178,6 @@ add_pragma_disable_assigns_check(goto_programt::instructiont &instr); /// \return The same reference after mutation (i.e., adding the pragmas). goto_programt &add_pragma_disable_assigns_check(goto_programt &prog); -/// Skip or do not skip assignments to function parameters -enum class skip_function_paramst -{ - YES, - NO -}; - /// \brief A class that generates instrumentation for assigns clause checking. /// /// The `track_*` methods add targets to the sets of tracked targets and append @@ -198,15 +193,18 @@ class instrument_spec_assignst /// /// \param _function_id name of the instrumented function /// \param _functions other functions of the model + /// \param _cfg_info control flow graph info about the function /// \param _st symbol table of the goto_model /// \param _message_handler used to output warning/error messages instrument_spec_assignst( const irep_idt &_function_id, const goto_functionst &_functions, + cfg_infot &_cfg_info, symbol_tablet &_st, message_handlert &_message_handler) : function_id(_function_id), functions(_functions), + cfg_info(_cfg_info), st(_st), ns(_st), log(_message_handler), @@ -434,28 +432,14 @@ class instrument_spec_assignst /// Generates inclusion check instructions for an assignment, havoc or /// havoc_object instruction /// \param lhs the assignment lhs or argument to havoc/havoc_object - /// \param cfg_info_opt allows target set pruning if available /// \param dest destination program to append instructions to - /// - /// \remark if provided, the internal instruction pointer of - /// `cfg_info_opt::target()` must point to the instruction containing the lhs - /// in question. - void check_inclusion_assignment( - const exprt &lhs, - optionalt &cfg_info_opt, - goto_programt &dest) const; + void check_inclusion_assignment(const exprt &lhs, goto_programt &dest) const; /// Generates inclusion check instructions for an argument passed to free /// \param expr the argument to the free operator - /// \param cfg_info_opt allows target set pruning if available /// \param dest destination program to append instructions to - /// - /// \remark If provided, the internal instruction pointer of - /// `cfg_info_opt::target()` must point to the instruction containing the lhs - /// in question. void check_inclusion_heap_allocated_and_invalidate_aliases( const exprt &expr, - optionalt &cfg_info_opt, goto_programt &dest); /// Instruments a sequence of instructions with inclusion checks. @@ -467,15 +451,11 @@ class instrument_spec_assignst /// \param body goto program containing the instructions /// \param instruction_it target to the first instruction of the sequence /// \param instruction_end target to the last instruction of the sequence - /// \param skip_function_params the argument to the free operator - /// \param cfg_info_opt allows target set pruning if available /// \param pred a predicate on targets to check if they should be instrumented void instrument_instructions( goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, - skip_function_paramst skip_function_params, - optionalt &cfg_info_opt, const std::function &pred = {}); /// Inserts the detected static local symbols into a target container. @@ -499,6 +479,9 @@ class instrument_spec_assignst /// Other functions of the model const goto_functionst &functions; + /// CFG information for simplification + cfg_infot &cfg_info; + /// Program symbol table symbol_tablet &st; @@ -554,27 +537,21 @@ class instrument_spec_assignst /// \param allow_null_lhs if true, allow the lhs to be NULL /// \param include_stack_allocated if true, include stack allocated targets /// in the inclusion check. - /// \param cfg_info_opt allows target set pruning if available - /// \remark If available, `cfg_info_opt` must point to the `lhs` in question. exprt inclusion_check_full( const car_exprt &lhs, bool allow_null_lhs, - bool include_stack_allocated, - optionalt &cfg_info_opt) const; + bool include_stack_allocated) const; /// Returns an inclusion check assertion of lhs over all tracked cars. /// \param lhs the lhs expression to check for inclusion /// \param allow_null_lhs if true, allow the lhs to be NULL /// \param include_stack_allocated if true, include stack allocated targets /// in the inclusion check. - /// \param cfg_info_opt allows target set pruning if available /// \param dest destination program to append instructions to - /// \remark If available, `cfg_info_opt` must point to the `lhs` in question. void inclusion_check_assertion( const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, - optionalt &cfg_info_opt, goto_programt &dest) const; /// \brief Adds an assignment in dest to invalidate the tracked car if @@ -593,15 +570,11 @@ class instrument_spec_assignst /// Returns true iff a `DECL x` must be explicitly added to the write set. /// @see must_track_decl_or_dead. - bool must_track_decl( - const goto_programt::const_targett &target, - const optionalt &cfg_info_opt) const; + bool must_track_decl(const goto_programt::const_targett &target) const; /// Returns true iff a `DEAD x` must be processed to update the write set. /// @see must_track_decl_or_dead. - bool must_track_dead( - const goto_programt::const_targett &target, - const optionalt &cfg_info_opt) const; + bool must_track_dead(const goto_programt::const_targett &target) const; /// \brief Returns true iff a function-local symbol must be tracked. /// @@ -612,31 +585,24 @@ class instrument_spec_assignst /// passed C compiler checks, non-dirty locals can only be assigned to /// directly by name, cannot escape their lexical scope, and are always safe /// to assign. Hence, we only track dirty locals in the write set. - bool must_track_decl_or_dead( - const irep_idt &ident, - const optionalt &cfg_info_opt) const; + bool must_track_decl_or_dead(const irep_idt &ident) const; /// Returns true iff an `ASSIGN lhs := rhs` instruction must be instrumented. - bool must_check_assign( - const goto_programt::const_targett &target, - skip_function_paramst skip_function_params, - const optionalt cfg_info_opt); + bool must_check_assign(const goto_programt::const_targett &target); /// Inserts an assertion in `body` immediately before the assignment /// at `instruction_it`, to ensure that the LHS of the assignment /// is included in the set of currently tracked CARs. void instrument_assign_statement( goto_programt::targett &instruction_it, - goto_programt &body, - optionalt &cfg_info_opt) const; + goto_programt &body) const; /// Inserts an assertion in `body` immediately before the function call at /// `instruction_it`, to ensure that all memory locations written to by the /// called function are included in the set of currently tracked CARs. void instrument_call_statement( goto_programt::targett &instruction_it, - goto_programt &body, - optionalt &cfg_info_opt); + goto_programt &body); using cond_target_exprt_to_car_mapt = std:: unordered_map; diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index ac43561e08f..71f6682fcbc 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -143,129 +143,6 @@ bool is_loop_free( namespacet &ns, messaget &log); -/// Stores information about a goto function computed from its CFG, -/// together with a `target` iterator into the instructions of the function. -/// -/// The methods of this class provide information about identifiers at -/// the current `target` instruction to allow simplifying assigns -/// clause checking assertions. -class cfg_infot -{ -public: - cfg_infot(const namespacet &_ns, goto_functiont &_goto_function) - : ns(_ns), - goto_function(_goto_function), - target(goto_function.body.instructions.begin()), - dirty_analysis(goto_function), - locals(goto_function) - { - } - - /// Steps the `target` iterator forward. - void step() - { - target++; - } - - /// Returns true iff the given `ident` is either not a `goto_function` local - /// or is a local that is dirty. - bool is_not_local_or_dirty_local(irep_idt ident) const - { - if(is_local(ident)) - return dirty_analysis.get_dirty_ids().find(ident) != - dirty_analysis.get_dirty_ids().end(); - else - return true; - } - - /// Returns true whenever the given `symbol_expr` might be alive - /// at the current `target` instruction. - bool is_maybe_alive(const symbol_exprt &symbol_expr) - { - // TODO query the static analysis when available - return true; - } - - /// Returns true iff `ident` is a local (or parameter) of `goto_function`. - bool is_local(irep_idt ident) const - { - const auto &symbol = ns.lookup(ident); - return locals.is_local(ident) || symbol.is_parameter; - } - - /// Returns true iff `expr` is an access to a locally declared symbol - /// or parameter symbol, without any dereference/address_of operations. - bool is_local_composite_access(const exprt &expr) const - { - // case-splitting on the lhs structure copied from symex_assignt::assign_rec - if(expr.id() == ID_symbol) - { - return is_local(to_symbol_expr(expr).get_identifier()); - } - else if(expr.id() == ID_index) - { - return is_local_composite_access(to_index_expr(expr).array()); - } - else if(expr.id() == ID_member) - { - const typet &type = to_member_expr(expr).struct_op().type(); - if( - type.id() == ID_struct || type.id() == ID_struct_tag || - type.id() == ID_union || type.id() == ID_union_tag) - { - return is_local_composite_access(to_member_expr(expr).compound()); - } - else - { - throw unsupported_operation_exceptiont( - "is_local_composite_access: unexpected assignment to member of '" + - type.id_string() + "'"); - } - } - else if(expr.id() == ID_if) - { - return is_local_composite_access(to_if_expr(expr).true_case()) && - is_local_composite_access(to_if_expr(expr).false_case()); - } - else if(expr.id() == ID_typecast) - { - return is_local_composite_access(to_typecast_expr(expr).op()); - } - else if( - expr.id() == ID_byte_extract_little_endian || - expr.id() == ID_byte_extract_big_endian) - { - return is_local_composite_access(to_byte_extract_expr(expr).op()); - } - else if(expr.id() == ID_complex_real) - { - return is_local_composite_access(to_complex_real_expr(expr).op()); - } - else if(expr.id() == ID_complex_imag) - { - return is_local_composite_access(to_complex_imag_expr(expr).op()); - } - else - { - // matches ID_address_of, ID_dereference, etc. - return false; - } - } - - /// returns the current target instruction - const goto_programt::targett &get_current_target() const - { - return target; - } - -private: - const namespacet &ns; - goto_functiont &goto_function; - goto_programt::targett target; - const dirtyt dirty_analysis; - const localst locals; -}; - /// Allows to clean expressions of side effects. class cleanert : public goto_convertt {