diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 2a420f75d50..f81b03278e4 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -321,14 +321,11 @@ void code_contractst::check_apply_loop_contracts( optionalt cfg_empty_info; // Perform write set instrumentation on the entire loop. - check_frame_conditions( - function_name, + instrument_spec_assigns.instrument_instructions( goto_function.body, loop_head, loop_end, - instrument_spec_assigns, - // do not skip checks on function parameter assignments - skipt::DontSkip, + skip_function_paramst::NO, // do not use CFG info for now cfg_empty_info); @@ -960,68 +957,6 @@ goto_functionst &code_contractst::get_goto_functions() return goto_functions; } -void code_contractst::instrument_assign_statement( - goto_programt::targett &instruction_it, - goto_programt &program, - instrument_spec_assignst &instrument_spec_assigns, - optionalt &cfg_info_opt) -{ - auto lhs = instruction_it->assign_lhs(); - lhs.add_source_location() = instruction_it->source_location(); - goto_programt payload; - instrument_spec_assigns.check_inclusion_assignment( - lhs, cfg_info_opt, payload); - insert_before_swap_and_advance(program, instruction_it, payload); -} - -void code_contractst::instrument_call_statement( - goto_programt::targett &instruction_it, - const irep_idt &function, - goto_programt &body, - instrument_spec_assignst &instrument_spec_assigns, - optionalt &cfg_info_opt) -{ - INVARIANT( - instruction_it->is_function_call(), - "The first argument of instrument_call_statement should always be " - "a function call"); - - const auto &callee_name = - to_symbol_expr(instruction_it->call_function()).get_identifier(); - - if(callee_name == "malloc") - { - const auto &function_call = - to_code_function_call(instruction_it->get_code()); - if(function_call.lhs().is_not_nil()) - { - // grab the returned pointer from malloc - auto object = pointer_object(function_call.lhs()); - object.add_source_location() = function_call.source_location(); - // move past the call and then insert the CAR - instruction_it++; - goto_programt payload; - instrument_spec_assigns.track_heap_allocated(object, payload); - insert_before_swap_and_advance(body, instruction_it, payload); - // since CAR was inserted *after* the malloc call, - // move the instruction pointer backward, - // because the caller increments it in a `for` loop - instruction_it--; - } - } - else if(callee_name == "free") - { - const auto &ptr = instruction_it->call_arguments().front(); - auto object = pointer_object(ptr); - object.add_source_location() = instruction_it->source_location(); - goto_programt payload; - instrument_spec_assigns - .check_inclusion_heap_allocated_and_invalidate_aliases( - object, cfg_info_opt, payload); - insert_before_swap_and_advance(body, instruction_it, payload); - } -} - bool code_contractst::check_for_looped_mallocs(const goto_programt &program) { // Collect all GOTOs and mallocs @@ -1101,9 +1036,9 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) auto &function_body = function_obj->second.body; // Get assigns clause for function - const symbolt &function_sybmol = ns.lookup(function); + const symbolt &function_symbol = ns.lookup(function); const auto &function_with_contract = - to_code_with_contract_type(function_sybmol.type); + to_code_with_contract_type(function_symbol.type); instrument_spec_assignst instrument_spec_assigns( function, goto_functions, symbol_table, log.get_message_handler()); @@ -1158,7 +1093,7 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) // Track formal parameters goto_programt snapshot_function_parameters; - for(const auto ¶m : to_code_type(function_sybmol.type).parameters()) + for(const auto ¶m : to_code_type(function_symbol.type).parameters()) { goto_programt payload; instrument_spec_assigns.track_stack_allocated( @@ -1170,184 +1105,16 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) goto_functions.update(); // Insert write set inclusion checks. - check_frame_conditions( - function, + instrument_spec_assigns.instrument_instructions( function_body, instruction_it, function_body.instructions.end(), - instrument_spec_assigns, - // skip checks on function parameter assignments - skipt::Skip, + skip_function_paramst::YES, cfg_info_opt); return false; } -/// Returns true iff the target instruction is tagged with a -/// 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' pragma. -bool has_disable_assigns_check_pragma( - const goto_programt::const_targett &target) -{ - const auto &pragmas = target->source_location().get_pragmas(); - return pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end(); -} - -/// Returns true iff an `ASSIGN lhs := rhs` instruction must be instrumented. -bool must_check_assign( - const goto_programt::const_targett &target, - code_contractst::skipt skip_parameter_assigns, - const namespacet ns, - const optionalt cfg_info_opt) -{ - if( - const auto &symbol_expr = - expr_try_dynamic_cast(target->assign_lhs())) - { - if( - skip_parameter_assigns == code_contractst::skipt::DontSkip && - ns.lookup(symbol_expr->get_identifier()).is_parameter) - return true; - - if(cfg_info_opt.has_value()) - return !cfg_info_opt.value().is_local(symbol_expr->get_identifier()); - } - - return true; -} - -/// Returns true iff a `DECL x` must be added to the local write set. -/// -/// A variable is called 'dirty' if its address gets taken at some point in -/// the program. -/// -/// Assuming the goto program is obtained from a structured C program that -/// passed C compiler checks, non-dirty variables can only be assigned to -/// directly by name, cannot escape their lexical scope, and are always safe -/// to assign. Hence, we only track dirty variables in the write set. -bool must_track_decl( - const goto_programt::const_targett &target, - const optionalt &cfg_info_opt) -{ - if(cfg_info_opt.has_value()) - return cfg_info_opt.value().is_not_local_or_dirty_local( - target->decl_symbol().get_identifier()); - - // Unless proved non-dirty by the CFG analysis we assume it is dirty. - return true; -} - -/// 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 must_track_dead( - const goto_programt::const_targett &target, - const optionalt &cfg_info_opt) -{ - // Unless proved non-dirty by the CFG analysis we assume it is dirty. - if(!cfg_info_opt.has_value()) - return true; - - return cfg_info_opt.value().is_not_local_or_dirty_local( - target->dead_symbol().get_identifier()); -} - -void code_contractst::check_frame_conditions( - const irep_idt &function, - goto_programt &body, - goto_programt::targett instruction_it, - const goto_programt::targett &instruction_end, - instrument_spec_assignst &instrument_spec_assigns, - skipt skip_parameter_assigns, - optionalt &cfg_info_opt) -{ - while(instruction_it != instruction_end) - { - // Skip instructions marked as disabled for assigns clause checking - if(has_disable_assigns_check_pragma(instruction_it)) - { - instruction_it++; - if(cfg_info_opt.has_value()) - cfg_info_opt.value().step(); - continue; - } - - // Do not instrument this instruction again in the future, - // 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)) - { - // grab the declared symbol - const auto &decl_symbol = instruction_it->decl_symbol(); - // move past the call and then insert the CAR - instruction_it++; - goto_programt payload; - instrument_spec_assigns.track_stack_allocated(decl_symbol, payload); - insert_before_swap_and_advance(body, instruction_it, payload); - // since CAR was inserted *after* the DECL instruction, - // move the instruction pointer backward, - // because the loop step takes care of the increment - instruction_it--; - } - else if( - instruction_it->is_assign() && - must_check_assign( - instruction_it, skip_parameter_assigns, ns, cfg_info_opt)) - { - instrument_assign_statement( - instruction_it, body, instrument_spec_assigns, cfg_info_opt); - } - else if(instruction_it->is_function_call()) - { - instrument_call_statement( - instruction_it, function, body, instrument_spec_assigns, cfg_info_opt); - } - else if( - instruction_it->is_dead() && - must_track_dead(instruction_it, cfg_info_opt)) - { - const auto &symbol = instruction_it->dead_symbol(); - if(instrument_spec_assigns.stack_allocated_is_tracked(symbol)) - { - goto_programt payload; - instrument_spec_assigns.invalidate_stack_allocated(symbol, payload); - insert_before_swap_and_advance(body, instruction_it, payload); - } - else - { - // For loops, the loop_head appears after the DECL of counters, - // and any other temporaries introduced during "initialization". - // However, they go `DEAD` (possible conditionally) inside the loop, - // in presence of return statements. - // Notice that for them those variables be writable, - // they must appear as assigns targets anyway, - // but their DECL statements are outside of the loop. - log.warning() << "Found a `DEAD` variable " << symbol.get_identifier() - << " without corresponding `DECL`, at: " - << instruction_it->source_location() << messaget::eom; - } - } - else if( - instruction_it->is_other() && - instruction_it->get_other().get_statement() == ID_havoc_object) - { - auto havoc_argument = instruction_it->get_other().operands().front(); - auto havoc_object = pointer_object(havoc_argument); - havoc_object.add_source_location() = instruction_it->source_location(); - goto_programt payload; - instrument_spec_assigns.check_inclusion_assignment( - havoc_object, cfg_info_opt, 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(); - } -} - bool code_contractst::enforce_contract(const irep_idt &function) { // Add statements to the source function diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 5760c6392ba..611a87daeab 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -111,13 +111,6 @@ class code_contractst namespacet ns; - /// Tells wether to skip or not skip an action - enum class skipt - { - DontSkip, - Skip - }; - protected: symbol_tablet &symbol_table; goto_functionst &goto_functions; @@ -133,52 +126,10 @@ class code_contractst /// Instrument functions to check frame conditions. bool check_frame_conditions_function(const irep_idt &function); - /// \brief Insert assertion statements into the goto program to ensure that - /// assigned memory is within the assignable memory frame. - /// - /// \param function Name of the function getting instrumented. - /// \param body Body of the function getting instrumented. - /// \param instruction_it Iterator to the instruction from which to start - /// instrumentation (inclusive). - /// \param instruction_end Iterator to the instruction at which to stop - /// instrumentation (exclusive). - /// \param instrument_spec_assigns Assigns clause instrumenter of the function - /// \param skip_parameter_assigns If true, will cause assignments to symbol - /// marked as is_parameter to not be instrumented. - /// \param cfg_info_opt Control flow graph information can will be used - /// for write set optimisation if available. - void check_frame_conditions( - const irep_idt &function, - goto_programt &body, - goto_programt::targett instruction_it, - const goto_programt::targett &instruction_end, - instrument_spec_assignst &instrument_spec_assigns, - skipt skip_parameter_assigns, - optionalt &cfg_info_opt); - /// Check if there are any malloc statements which may be repeated because of /// a goto statement that jumps back. bool check_for_looped_mallocs(const goto_programt &program); - /// Inserts an assertion into program immediately before the assignment - /// instruction_it, to ensure that the left-hand-side of the assignment - /// is "included" in the (conditional address ranges in the) write set. - void instrument_assign_statement( - goto_programt::targett &instruction_it, - goto_programt &program, - instrument_spec_assignst &instrument_spec_assigns, - optionalt &cfg_info_opt); - - /// Inserts an assertion into program immediately before the function call at - /// instruction_it, to ensure that all memory locations written to by the - // callee are "included" in the (conditional address ranges in the) write set. - void instrument_call_statement( - goto_programt::targett &instruction_it, - const irep_idt &function, - goto_programt &body, - instrument_spec_assignst &instrument_spec_assigns, - optionalt &cfg_info_opt); - /// Apply loop contracts, whenever available, to all loops in `function`. /// Loop invariants, loop variants, and loop assigns clauses. void apply_loop_contract( diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index 71e769e37f9..fcca7a03fa6 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -27,7 +27,47 @@ Date: January 2022 #include "utils.h" -///// PUBLIC METHODS ///// +/// a local pragma used to keep track and skip already instrumented instructions +const char CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK[] = + "contracts:disable:assigns-check"; + +void add_pragma_disable_pointer_checks(source_locationt &location) +{ + location.add_pragma("disable:pointer-check"); + location.add_pragma("disable:pointer-primitive-check"); + location.add_pragma("disable:pointer-overflow-check"); + location.add_pragma("disable:signed-overflow-check"); + location.add_pragma("disable:unsigned-overflow-check"); + location.add_pragma("disable:conversion-check"); +} + +/// Returns true iff the target instruction is tagged with a +/// 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' pragma. +bool has_disable_assigns_check_pragma( + const goto_programt::const_targett &target) +{ + const auto &pragmas = target->source_location().get_pragmas(); + return pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end(); +} + +void add_pragma_disable_assigns_check(source_locationt &location) +{ + location.add_pragma(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK); +} + +goto_programt::instructiont & +add_pragma_disable_assigns_check(goto_programt::instructiont &instr) +{ + add_pragma_disable_assigns_check(instr.source_location_nonconst()); + return instr; +} + +goto_programt &add_pragma_disable_assigns_check(goto_programt &prog) +{ + Forall_goto_program_instructions(it, prog) + add_pragma_disable_assigns_check(*it); + return prog; +} void instrument_spec_assignst::track_spec_target( const exprt &expr, @@ -81,7 +121,7 @@ void instrument_spec_assignst::track_heap_allocated( void instrument_spec_assignst::check_inclusion_assignment( const exprt &lhs, optionalt &cfg_info_opt, - goto_programt &dest) + goto_programt &dest) const { // create temporary car but do not track const auto car = create_car_expr(true_exprt{}, lhs); @@ -137,7 +177,98 @@ void instrument_spec_assignst:: invalidate_heap_and_spec_aliases(car, dest); } -///// PRIVATE METHODS ///// +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) +{ + while(instruction_it != instruction_end) + { + // Skip instructions marked as disabled for assigns clause checking + if(has_disable_assigns_check_pragma(instruction_it)) + { + instruction_it++; + if(cfg_info_opt.has_value()) + cfg_info_opt.value().step(); + continue; + } + + // Do not instrument this instruction again in the future, + // 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)) + { + // grab the declared symbol + const auto &decl_symbol = instruction_it->decl_symbol(); + // move past the call and then insert the CAR + instruction_it++; + goto_programt payload; + track_stack_allocated(decl_symbol, payload); + insert_before_swap_and_advance(body, instruction_it, payload); + // since CAR was inserted *after* the DECL instruction, + // move the instruction pointer backward, + // because the enclosing while loop step takes + // care of the increment + instruction_it--; + } + else if( + instruction_it->is_assign() && + must_check_assign(instruction_it, skip_function_params, cfg_info_opt)) + { + instrument_assign_statement(instruction_it, body, cfg_info_opt); + } + else if(instruction_it->is_function_call()) + { + instrument_call_statement(instruction_it, body, cfg_info_opt); + } + else if( + instruction_it->is_dead() && + must_track_dead(instruction_it, cfg_info_opt)) + { + const auto &symbol = instruction_it->dead_symbol(); + if(stack_allocated_is_tracked(symbol)) + { + goto_programt payload; + invalidate_stack_allocated(symbol, payload); + insert_before_swap_and_advance(body, instruction_it, payload); + } + else + { + // Some variables declared outside of the loop + // can go `DEAD` (possible conditionally) when return + // statements exist inside the loop body. + // Since they are not DECL'd inside the loop, these locations + // are not automatically tracked in the stack_allocated map, + // so to be writable these variables must be listed in the assigns + // clause. + log.warning() << "Found a `DEAD` variable " << symbol.get_identifier() + << " without corresponding `DECL`, at: " + << instruction_it->source_location() << messaget::eom; + } + } + else if( + instruction_it->is_other() && + instruction_it->get_other().get_statement() == ID_havoc_object) + { + auto havoc_argument = instruction_it->get_other().operands().front(); + 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); + 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(); + } +} void instrument_spec_assignst::track_spec_target_group( const conditional_target_group_exprt &group, @@ -513,3 +644,120 @@ void instrument_spec_assignst::invalidate_heap_and_spec_aliases( for(const auto &pair : from_heap_alloc) invalidate_car(pair.second, freed_car, dest); } + +/// 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) +{ + if( + const auto &symbol_expr = + expr_try_dynamic_cast(target->assign_lhs())) + { + if( + skip_function_params == skip_function_paramst::NO && + ns.lookup(symbol_expr->get_identifier()).is_parameter) + { + return true; + } + + if(cfg_info_opt.has_value()) + return !cfg_info_opt.value().is_local(symbol_expr->get_identifier()); + } + + return true; +} + +/// Returns true iff a `DECL x` must be added to the local write set. +/// +/// A variable is called 'dirty' if its address gets taken at some point in +/// the program. +/// +/// Assuming the goto program is obtained from a structured C program that +/// passed C compiler checks, non-dirty variables can only be assigned to +/// directly by name, cannot escape their lexical scope, and are always safe +/// to assign. Hence, we only track dirty variables in the write set. +bool instrument_spec_assignst::must_track_decl( + const goto_programt::const_targett &target, + const optionalt &cfg_info_opt) const +{ + if(cfg_info_opt.has_value()) + { + return cfg_info_opt.value().is_not_local_or_dirty_local( + target->decl_symbol().get_identifier()); + } + // Unless proved non-dirty by the CFG analysis we assume it is dirty. + return true; +} + +/// 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 +{ + // Unless proved non-dirty by the CFG analysis we assume it is dirty. + if(!cfg_info_opt.has_value()) + return true; + + return cfg_info_opt.value().is_not_local_or_dirty_local( + 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 +{ + 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); + 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) +{ + PRECONDITION_WITH_DIAGNOSTICS( + instruction_it->is_function_call(), + "The first argument of instrument_call_statement should always be " + "a function call"); + + const auto &callee_name = + to_symbol_expr(instruction_it->call_function()).get_identifier(); + + if(callee_name == "malloc") + { + const auto &function_call = + to_code_function_call(instruction_it->get_code()); + if(function_call.lhs().is_not_nil()) + { + // grab the returned pointer from malloc + auto object = pointer_object(function_call.lhs()); + object.add_source_location() = function_call.source_location(); + // move past the call and then insert the CAR + instruction_it++; + goto_programt payload; + track_heap_allocated(object, payload); + insert_before_swap_and_advance(body, instruction_it, payload); + // since CAR was inserted *after* the malloc call, + // move the instruction pointer backward, + // because the caller increments it in a `for` loop + instruction_it--; + } + } + else if(callee_name == "free") + { + const auto &ptr = instruction_it->call_arguments().front(); + 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); + 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 1af2e3c0619..3df9a412391 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.h +++ b/src/goto-instrument/contracts/instrument_spec_assigns.h @@ -131,6 +131,37 @@ class car_exprt : public exprt } }; +/// \brief Adds a pragma on a source location disable all pointer checks. +/// +/// The disabled checks are: "pointer-check", "pointer-primitive-check", +/// "pointer-overflow-check", "signed-overflow-check", +// "unsigned-overflow-check", "conversion-check". +void add_pragma_disable_pointer_checks(source_locationt &source_location); + +/// \brief Adds a pragma on a source_locationt to disable inclusion checking. +void add_pragma_disable_assigns_check(source_locationt &source_location); + +/// \brief Adds a pragma on a GOTO instruction to disable inclusion checking. +/// +/// \param instr: A mutable reference to the GOTO instruction. +/// \return The same reference after mutation (i.e., adding the pragma). +goto_programt::instructiont & +add_pragma_disable_assigns_check(goto_programt::instructiont &instr); + +/// \brief Adds pragmas on all instructions in a GOTO program +/// to disable inclusion checking on them. +/// +/// \param prog: A mutable reference to the GOTO program. +/// \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 @@ -182,13 +213,37 @@ class instrument_spec_assignst /// in dest. void track_heap_allocated(const exprt &expr, goto_programt &dest); - /// Search the call graph reachable from the instrumented function to identify - /// local static variables used directly or indirectly, add them to the - /// `stack-allocated` tracked locations, and generate corresponding snapshot - /// instructions in dest. - /// \param dest a snaphot program for the identified static locals. +protected: + /// Collects (from the symbol table) symbols that have a static lifetime + /// and have a source location where the funciton name appears in the call + /// graph built from the given function identifier. + /// \param root_function_id the function to build the call graph from + /// \param dest the program where snapshots of the collected static locals + void collect_static_locals_from_root_function( + const irep_idt &root_function_id, + goto_programt &dest); + +public: + /// Searches the call graph reachable from the instrumented function to + /// collect local static variables used directly or indirectly, add them to + /// the `stack-allocated` tracked locations, and generate corresponding + /// snapshot instructions in dest. + /// \param dest pogram where snaphots instructions for the collected static + /// locals are added. void track_static_locals(goto_programt &dest); + /// Searches for function calls occurring between the start and stop + /// targets (inclusive) instructions, and collects the static locals declared + /// by these functions. + /// \param begin instruction to start the search from. + /// \param end instruction to stop the search at. + /// \param dest pogram where snaphots instructions for the collected static + /// locals are added. + void track_static_locals_from_calls( + const goto_programt::targett &begin, + const goto_programt::targett &end, + goto_programt &dest); + /// Generates inclusion check instructions for an assignment, havoc or /// havoc_object instruction /// \param lhs the assignment lhs or argument to havoc/havoc_object @@ -201,7 +256,7 @@ class instrument_spec_assignst void check_inclusion_assignment( const exprt &lhs, optionalt &cfg_info_opt, - goto_programt &dest); + goto_programt &dest) const; /// Generates inclusion check instructions for an argument passed to free /// \param expr the argument to the free operator @@ -216,6 +271,13 @@ class instrument_spec_assignst optionalt &cfg_info_opt, goto_programt &dest); + 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); + protected: /// Name of the instrumented function const irep_idt &function_id; @@ -312,6 +374,47 @@ class instrument_spec_assignst const car_exprt &freed_car, goto_programt &dest) const; + /// Returns true iff a `DECL x` must be added to the local write set. + /// + /// A variable is called 'dirty' if its address gets taken at some point in + /// the program. + /// + /// Assuming the goto program is obtained from a structured C program that + /// passed C compiler checks, non-dirty variables can only be assigned to + /// directly by name, cannot escape their lexical scope, and are always safe + /// to assign. Hence, we only track dirty variables in the write set. + bool must_track_decl( + const goto_programt::const_targett &target, + const optionalt &cfg_info_opt) const; + + /// Returns true iff a `DEAD x` must be processed to update the local write + /// set. The conditions are the same than for tracking a `DECL x` instruction. + bool must_track_dead( + const goto_programt::const_targett &target, + const optionalt &cfg_info_opt) 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); + + /// 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; + + /// 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); + using cond_target_exprt_to_car_mapt = std:: unordered_map; diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index a6e40f785d6..a945600b614 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -76,49 +76,6 @@ void havoc_assigns_targetst::append_havoc_code_for_expr( havoc_utilst::append_havoc_code_for_expr(location, expr, dest); } -void add_pragma_disable_pointer_checks(source_locationt &location) -{ - location.add_pragma("disable:pointer-check"); - location.add_pragma("disable:pointer-primitive-check"); - location.add_pragma("disable:pointer-overflow-check"); - location.add_pragma("disable:signed-overflow-check"); - location.add_pragma("disable:unsigned-overflow-check"); - location.add_pragma("disable:conversion-check"); -} - -goto_programt::instructiont & -add_pragma_disable_pointer_checks(goto_programt::instructiont &instr) -{ - add_pragma_disable_pointer_checks(instr.source_location_nonconst()); - return instr; -} - -goto_programt &add_pragma_disable_pointer_checks(goto_programt &prog) -{ - Forall_goto_program_instructions(it, prog) - add_pragma_disable_pointer_checks(*it); - return prog; -} - -void add_pragma_disable_assigns_check(source_locationt &location) -{ - location.add_pragma(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK); -} - -goto_programt::instructiont & -add_pragma_disable_assigns_check(goto_programt::instructiont &instr) -{ - add_pragma_disable_assigns_check(instr.source_location_nonconst()); - return instr; -} - -goto_programt &add_pragma_disable_assigns_check(goto_programt &prog) -{ - Forall_goto_program_instructions(it, prog) - add_pragma_disable_assigns_check(*it); - return prog; -} - exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns) { exprt::operandst validity_checks; diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 6fe53c46c24..9487ddb9475 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -24,8 +24,6 @@ Date: September 2021 #include #include -#define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check" - /// \brief A class that overrides the low-level havocing functions in the base /// utility class, to havoc only when expressions point to valid memory, /// i.e. if all dereferences within an expression are valid @@ -67,44 +65,6 @@ class havoc_assigns_targetst : public havoc_if_validt goto_programt &dest) const override; }; -/// \brief Adds a pragma on a source location disable all pointer checks. -/// -/// The disabled checks are: "pointer-check", "pointer-primitive-check", -/// "pointer-overflow-check", "signed-overflow-check", -// "unsigned-overflow-check", "conversion-check". -void add_pragma_disable_pointer_checks(source_locationt &source_location); - -/// \brief Adds pragmas on a GOTO instruction to disable all pointer checks. -/// -/// \param instr: A mutable reference to the GOTO instruction. -/// \return The same reference after mutation (i.e., adding the pragma). -goto_programt::instructiont & -add_pragma_disable_pointer_checks(goto_programt::instructiont &instr); - -/// \brief Adds pragmas on all instructions in a GOTO program -/// to disable all pointer checks. -/// -/// \param prog: A mutable reference to the GOTO program. -/// \return The same reference after mutation (i.e., adding the pragmas). -goto_programt &add_pragma_disable_pointer_checks(goto_programt &prog); - -/// \brief Adds a pragma on a source_locationt to disable inclusion checking. -void add_pragma_disable_assigns_check(source_locationt &source_location); - -/// \brief Adds a pragma on a GOTO instruction to disable inclusion checking. -/// -/// \param instr: A mutable reference to the GOTO instruction. -/// \return The same reference after mutation (i.e., adding the pragma). -goto_programt::instructiont & -add_pragma_disable_assigns_check(goto_programt::instructiont &instr); - -/// \brief Adds pragmas on all instructions in a GOTO program -/// to disable inclusion checking on them. -/// -/// \param prog: A mutable reference to the GOTO program. -/// \return The same reference after mutation (i.e., adding the pragmas). -goto_programt &add_pragma_disable_assigns_check(goto_programt &prog); - /// \brief Generate a validity check over all dereferences in an expression /// /// This function generates a formula: