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 {