From db9131af88a76525cf69d54771d2430b50cbe681 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 25 Jan 2022 02:35:19 +0000 Subject: [PATCH 1/7] CONTRACTS: Do not distribute conditions on assigns clause targets in the front-end (defer to actual instrumentation). --- src/ansi-c/c_typecheck_code.cpp | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index bc7a12754f3..dc42dacfe7b 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -984,19 +984,12 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) } else { - // if the condition is not trivially true, - // place each single target in its own conditional target expr, - // distributing the condition + // if the condition is not trivially true, typecheck in place for(auto &actual_target : conditional_target_group.targets()) { typecheck_spec_assigns_target(actual_target); - exprt ops{ID_expression_list}; - ops.add_to_operands(actual_target); - conditional_target_group_exprt result{condition, ops}; - result.add_source_location() = - conditional_target_group.source_location(); - tmp.push_back(std::move(result)); } + tmp.push_back(std::move(target)); } } @@ -1004,8 +997,9 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) if(must_throw) throw 0; - // now each target is either a simple side-effect-free lvalue expression - // or a conditional target expression with a single target + // now each target is either: + // - a simple side-effect-free unconditional lvalue expression or + // - a conditional target group expression with a non-trivial condition // update original vector in-place std::swap(targets, tmp); From 83e9cadcf5f7416dc534091f5ffbf364d1b56fc3 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 25 Jan 2022 02:36:40 +0000 Subject: [PATCH 2/7] CONTRACTS: New classes encapsulating assigns clause checking logic. - new class conditional_target_exprt derived from exprt representing conditional targets - new class car_exprt derived from exprt representing normalised conditional targets extended with their conditional address ranges and snapshot variables - new class instrument_assigns_clauset encapsulating assigns clause checking logic - simplified interface with 5 main methods to generate CARs snapshots for different types of targets, generate inclusion checks, invalidate CARs - Add the new intrument_spec_assigns.cpp to the Makefile --- src/goto-instrument/Makefile | 1 + .../contracts/instrument_spec_assigns.cpp | 515 ++++++++++++++++++ .../contracts/instrument_spec_assigns.h | 346 ++++++++++++ 3 files changed, 862 insertions(+) create mode 100644 src/goto-instrument/contracts/instrument_spec_assigns.cpp create mode 100644 src/goto-instrument/contracts/instrument_spec_assigns.h diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index c7cd8e63aa8..d8c6fdd02c8 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -19,6 +19,7 @@ SRC = accelerate/accelerate.cpp \ contracts/assigns.cpp \ contracts/contracts.cpp \ contracts/havoc_assigns_clause_targets.cpp \ + contracts/instrument_spec_assigns.cpp \ contracts/memory_predicates.cpp \ contracts/utils.cpp \ concurrency.cpp \ diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp new file mode 100644 index 00000000000..71e769e37f9 --- /dev/null +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -0,0 +1,515 @@ +/*******************************************************************\ + +Module: Instrument assigns clauses in code contracts. + +Author: Remi Delmas + +Date: January 2022 + +\*******************************************************************/ + +/// \file +/// Specify write set in code contracts + +#include "instrument_spec_assigns.h" + +#include +#include +#include +#include +#include +#include +#include + +#include + +#include + +#include "utils.h" + +///// PUBLIC METHODS ///// + +void instrument_spec_assignst::track_spec_target( + const exprt &expr, + goto_programt &dest) +{ + if(auto target = expr_try_dynamic_cast(expr)) + track_spec_target_group(*target, dest); + else + track_plain_spec_target(expr, dest); +} + +void instrument_spec_assignst::track_stack_allocated( + const symbol_exprt &symbol_expr, + goto_programt &dest) +{ + create_snapshot(create_car_from_stack_alloc(symbol_expr), dest); +} + +bool instrument_spec_assignst::stack_allocated_is_tracked( + const symbol_exprt &symbol_expr) const +{ + return from_stack_alloc.find(symbol_expr) != from_stack_alloc.end(); +} + +void instrument_spec_assignst::invalidate_stack_allocated( + const symbol_exprt &symbol_expr, + goto_programt &dest) +{ + // ensure it is tracked + PRECONDITION_WITH_DIAGNOSTICS( + stack_allocated_is_tracked(symbol_expr), + "symbol is not tracked :" + from_expr(ns, "", symbol_expr)); + + const auto &car = from_stack_alloc.find(symbol_expr)->second; + + source_locationt source_location(symbol_expr.source_location()); + add_pragma_disable_pointer_checks(source_location); + add_pragma_disable_assigns_check(source_location); + + dest.add(goto_programt::make_assignment( + car.valid_var(), false_exprt{}, source_location)); +} + +void instrument_spec_assignst::track_heap_allocated( + const exprt &expr, + goto_programt &dest) +{ + create_snapshot(create_car_from_heap_alloc(expr), dest); +} + +void instrument_spec_assignst::check_inclusion_assignment( + const exprt &lhs, + optionalt &cfg_info_opt, + goto_programt &dest) +{ + // 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); +} + +void instrument_spec_assignst::track_static_locals(goto_programt &dest) +{ + auto call_graph = + call_grapht::create_from_root_function(functions, function_id, true) + .get_directed_graph(); + + for(const auto &sym_pair : st) + { + const auto &sym = sym_pair.second; + if(sym.is_static_lifetime) + { + auto fname = sym.location.get_function(); + if( + !fname.empty() && + (fname == function_id || call_graph.get_node_index(fname).has_value())) + { + // We found a symbol with + // - a static lifetime + // - non empty location function + // - this function appears in the call graph of the function + + // insert in tracking set and generate snapshot instructions + // for this target. + create_snapshot(create_car_from_stack_alloc(sym.symbol_expr()), dest); + } + } + } +} + +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 + const auto car = create_car_expr(true_exprt{}, expr); + + // generate snapshot instructions for this target. + create_snapshot(car, dest); + + // check inclusion, allowing null and not allowing stack allocated locals + inclusion_check_assertion(car, true, false, cfg_info_opt, dest); + + // invalidate aliases of the freed object + invalidate_heap_and_spec_aliases(car, dest); +} + +///// PRIVATE METHODS ///// + +void instrument_spec_assignst::track_spec_target_group( + const conditional_target_group_exprt &group, + goto_programt &dest) +{ + // clean up side effects from the guard expression if needed + cleanert cleaner(st, log.get_message_handler()); + exprt condition(group.condition()); + if(has_subexpr(condition, ID_side_effect)) + cleaner.clean(condition, dest, st.lookup_ref(function_id).mode); + + // create conditional address ranges by distributing the condition + for(const auto &target : group.targets()) + { + // insert in tracking set + const auto &car = create_car_from_spec_assigns(condition, target); + + // generate target validity check for this target. + target_validity_assertion(car, true, dest); + + // generate snapshot instructions for this target. + create_snapshot(car, dest); + } +} + +void instrument_spec_assignst::track_plain_spec_target( + const exprt &expr, + goto_programt &dest) +{ + // insert in tracking set + const auto &car = create_car_from_spec_assigns(true_exprt{}, expr); + + // generate target validity check for this target. + target_validity_assertion(car, true, dest); + + // generate snapshot instructions for this target. + create_snapshot(car, dest); +} + +const symbolt instrument_spec_assignst::create_fresh_symbol( + const std::string &suffix, + const typet &type, + const source_locationt &location) const +{ + return new_tmp_symbol( + type, location, st.lookup_ref(function_id).mode, st, suffix); +} + +car_exprt instrument_spec_assignst::create_car_expr( + const exprt &condition, + const exprt &target) const +{ + const source_locationt &source_location = target.source_location(); + const auto &valid_var = + create_fresh_symbol("__car_valid", bool_typet(), source_location) + .symbol_expr(); + + const auto &lower_bound_var = + create_fresh_symbol("__car_lb", pointer_type(char_type()), source_location) + .symbol_expr(); + + const auto &upper_bound_var = + create_fresh_symbol("__car_ub", pointer_type(char_type()), source_location) + .symbol_expr(); + + if(target.id() == ID_pointer_object) + { + const auto &arg = to_unary_expr(target).op(); + return { + condition, + target, + minus_exprt( + typecast_exprt::conditional_cast(arg, pointer_type(char_type())), + pointer_offset(arg)), + typecast_exprt::conditional_cast(object_size(arg), signed_size_type()), + valid_var, + lower_bound_var, + upper_bound_var}; + } + else if(is_assignable(target)) + { + const auto &size = size_of_expr(target.type(), ns); + + INVARIANT( + size.has_value(), + "no definite size for lvalue target:\n" + target.pretty()); + + return {condition, + target, + typecast_exprt::conditional_cast( + address_of_exprt{target}, pointer_type(char_type())), + typecast_exprt::conditional_cast(size.value(), signed_size_type()), + valid_var, + lower_bound_var, + upper_bound_var}; + }; + + UNREACHABLE; +} + +void instrument_spec_assignst::create_snapshot( + const car_exprt &car, + goto_programt &dest) const +{ + source_locationt source_location(car.source_location()); + add_pragma_disable_pointer_checks(source_location); + add_pragma_disable_assigns_check(source_location); + + dest.add(goto_programt::make_decl(car.valid_var(), source_location)); + + dest.add(goto_programt::make_assignment( + car.valid_var(), + simplify_expr( + and_exprt{car.condition(), + not_exprt{null_pointer(car.target_start_address())}}, + ns), + source_location)); + + dest.add(goto_programt::make_decl(car.lower_bound_var(), source_location)); + + dest.add(goto_programt::make_assignment( + car.lower_bound_var(), car.target_start_address(), source_location)); + + dest.add(goto_programt::make_decl(car.upper_bound_var(), source_location)); + + dest.add(goto_programt::make_assignment( + car.upper_bound_var(), + simplify_expr( + plus_exprt{car.target_start_address(), car.target_size()}, ns), + source_location)); +} + +exprt instrument_spec_assignst::target_validity_expr( + const car_exprt &car, + bool allow_null_target) const +{ + // If requested, we check that when guard condition is true, + // the target's `start_address` pointer satisfies w_ok with the expected size + // (or is NULL if we allow it explicitly). + // This assertion will be falsified whenever `start_address` is invalid or + // not of the right size (or is NULL if we dot not allow it expliclitly). + auto result = + or_exprt{not_exprt{car.condition()}, + w_ok_exprt{car.target_start_address(), car.target_size()}}; + + if(allow_null_target) + result.add_to_operands(null_pointer(car.target_start_address())); + + return simplify_expr(result, ns); +} + +void instrument_spec_assignst::target_validity_assertion( + const car_exprt &car, + bool allow_null_target, + goto_programt &dest) const +{ + // since assigns clauses are declared outside of their function body + // their source location might not have a function attribute + source_locationt source_location(car.source_location()); + if(source_location.get_function().empty()) + source_location.set_function(function_id); + + source_location.set_property_class("assigns"); + + add_pragma_disable_pointer_checks(source_location); + add_pragma_disable_assigns_check(source_location); + + std::string comment = "Check that "; + comment += from_expr(ns, "", car.target()); + comment += " is valid"; + if(!car.condition().is_true()) + { + comment += " when "; + comment += from_expr(ns, "", car.condition()); + } + + source_location.set_comment(comment); + + dest.add(goto_programt::make_assertion( + target_validity_expr(car, allow_null_target), source_location)); +} + +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()); + + // since assigns clauses are declared outside of their function body + // their source location might not have a function attribute + if(source_location.get_function().empty()) + source_location.set_function(function_id); + + add_pragma_disable_pointer_checks(source_location); + add_pragma_disable_assigns_check(source_location); + + source_location.set_property_class("assigns"); + + const auto &orig_comment = source_location.get_comment(); + std::string comment = "Check that "; + if(!is_assigns_clause_replacement_tracking_comment(orig_comment)) + { + if(!car.condition().is_true()) + comment += from_expr(ns, "", car.condition()) + ": "; + comment += from_expr(ns, "", car.target()); + } + else + comment += id2string(orig_comment); + + comment += " is assignable"; + source_location.set_comment(comment); + + dest.add(goto_programt::make_assertion( + inclusion_check_full( + car, allow_null_lhs, include_stack_allocated, cfg_info_opt), + source_location)); +} + +exprt instrument_spec_assignst::inclusion_check_single( + const car_exprt &car, + const car_exprt &candidate_car) const +{ + // remark: both lb and ub are derived from the same object so checking + // same_object(upper_bound_address_var, lhs.upper_bound_address_var) + // is redundant + return simplify_expr( + and_exprt{ + {candidate_car.valid_var(), + same_object(candidate_car.lower_bound_var(), car.lower_bound_var()), + less_than_or_equal_exprt{pointer_offset(candidate_car.lower_bound_var()), + pointer_offset(car.lower_bound_var())}, + less_than_or_equal_exprt{ + pointer_offset(car.upper_bound_var()), + pointer_offset(candidate_car.upper_bound_var())}}}, + ns); +} + +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 no_targets = from_spec_assigns.empty() && from_heap_alloc.empty() && + (!include_stack_allocated || from_stack_alloc.empty()); + + // inclusion check expression + if(no_targets) + { + // if null lhs are allowed then we should have a null lhs when + // we reach this program point, otherwise we should never reach + // this program point + if(allow_null_lhs) + return null_pointer(car.target_start_address()); + else + return false_exprt{}; + } + + // Build a disjunction over all tracked locations + exprt::operandst disjuncts; + + for(const auto &pair : from_spec_assigns) + disjuncts.push_back(inclusion_check_single(car, pair.second)); + + for(const auto &pair : from_heap_alloc) + disjuncts.push_back(inclusion_check_single(car, pair.second)); + + if(include_stack_allocated) + { + 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)); + } + } + + if(allow_null_lhs) + return or_exprt{null_pointer(car.target_start_address()), + and_exprt{car.valid_var(), disjunction(disjuncts)}}; + else + return and_exprt{car.valid_var(), disjunction(disjuncts)}; +} + +const car_exprt &instrument_spec_assignst::create_car_from_spec_assigns( + const exprt &condition, + const exprt &target) +{ + conditional_target_exprt key{condition, target}; + const auto &found = from_spec_assigns.find(key); + if(found != from_spec_assigns.end()) + { + log.warning() << "Ignored duplicate expression '" + << from_expr(ns, target.id(), target) + << "' in assigns clause spec at " + << target.source_location().as_string() << messaget::eom; + return found->second; + } + else + { + from_spec_assigns.insert({key, create_car_expr(condition, target)}); + return from_spec_assigns.find(key)->second; + } +} + +const car_exprt &instrument_spec_assignst::create_car_from_stack_alloc( + const symbol_exprt &target) +{ + const auto &found = from_stack_alloc.find(target); + if(found != from_stack_alloc.end()) + { + log.warning() << "Ignored duplicate stack-allocated target '" + << from_expr(ns, target.id(), target) << "' at " + << target.source_location().as_string() << messaget::eom; + return found->second; + } + else + { + from_stack_alloc.insert({target, create_car_expr(true_exprt{}, target)}); + return from_stack_alloc.find(target)->second; + } +} + +const car_exprt & +instrument_spec_assignst::create_car_from_heap_alloc(const exprt &target) +{ + const auto &found = from_heap_alloc.find(target); + if(found != from_heap_alloc.end()) + { + log.warning() << "Ignored duplicate heap-allocated target '" + << from_expr(ns, target.id(), target) << "' at " + << target.source_location().as_string() << messaget::eom; + return found->second; + } + else + { + from_heap_alloc.insert({target, create_car_expr(true_exprt{}, target)}); + return from_heap_alloc.find(target)->second; + } +} + +void instrument_spec_assignst::invalidate_car( + const car_exprt &tracked_car, + const car_exprt &freed_car, + goto_programt &result) const +{ + source_locationt source_location(freed_car.source_location()); + add_pragma_disable_pointer_checks(source_location); + add_pragma_disable_assigns_check(source_location); + + result.add(goto_programt::make_assignment( + tracked_car.valid_var(), + and_exprt{tracked_car.valid_var(), + not_exprt{same_object( + tracked_car.lower_bound_var(), freed_car.lower_bound_var())}}, + source_location)); +} + +void instrument_spec_assignst::invalidate_heap_and_spec_aliases( + const car_exprt &freed_car, + goto_programt &dest) const +{ + for(const auto &pair : from_spec_assigns) + invalidate_car(pair.second, freed_car, dest); + + for(const auto &pair : from_heap_alloc) + invalidate_car(pair.second, freed_car, dest); +} diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.h b/src/goto-instrument/contracts/instrument_spec_assigns.h new file mode 100644 index 00000000000..1af2e3c0619 --- /dev/null +++ b/src/goto-instrument/contracts/instrument_spec_assigns.h @@ -0,0 +1,346 @@ +/*******************************************************************\ + +Module: Instrument assigns clauses in code contracts. + +Author: Remi Delmas + +Date: January 2022 + +\*******************************************************************/ + +/// \file +/// Specify write set in function contracts + +#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 "utils.h" + +// forward declarations +class conditional_target_group_exprt; +class namespacet; +class symbol_tablet; +class symbolt; + +/// Class that represents a single conditional target. +class conditional_target_exprt : public exprt +{ +public: + conditional_target_exprt(const exprt &_condition, const exprt &_target) + : exprt(irep_idt{}, typet{}, {_condition, _target}) + { + INVARIANT( + !has_subexpr(_condition, ID_side_effect), + "condition must have no side_effect sub-expression"); + add_source_location() = _target.source_location(); + } + + /// Condition expression + const exprt &condition() const + { + return operands()[0]; + } + + /// Target expression + const exprt &target() const + { + return operands()[1]; + } +}; + +/// Class that represents a normalized conditional address range, with: +/// - condition expression +/// - target expression +/// - normalised start address expression +/// - normalised size expression +/// - snapshot variable symbols +class car_exprt : public exprt +{ +public: + car_exprt( + const exprt &_condition, + const exprt &_target, + const exprt &_target_start_address, + const exprt &_target_size, + const symbol_exprt &_validity_var, + const symbol_exprt &_lower_bound_var, + const symbol_exprt &_upper_bound_var) + : exprt( + irep_idt{}, + typet{}, + {_condition, + _target, + _target_start_address, + _target_size, + _validity_var, + _lower_bound_var, + _upper_bound_var}) + { + add_source_location() = _target.source_location(); + } + + /// Condition expression. When this condition holds the target is allowed + const exprt &condition() const + { + return operands()[0]; + } + + /// The target expression + const exprt &target() const + { + return operands()[1]; + } + + /// Start address of the target + const exprt &target_start_address() const + { + return operands()[2]; + } + + /// Size of the target in bytes + const exprt &target_size() const + { + return operands()[3]; + } + + /// Identifier of the validity snapshot variable + const symbol_exprt &valid_var() const + { + return to_symbol_expr(operands()[4]); + } + + /// Identifier of the lower address bound snapshot variable + const symbol_exprt &lower_bound_var() const + { + return to_symbol_expr(operands()[5]); + } + + /// Identifier of the upper address bound snapshot variable + const symbol_exprt &upper_bound_var() const + { + return to_symbol_expr(operands()[6]); + } +}; + +/// \brief A class that generates instrumentation for assigns clause checking. +/// +/// The `track_*` methods add targets to the sets of tracked targets and append +/// instructions to the given destination program. +/// +/// The `check_inclusion_*` methods generate assertions checking for inclusion +/// of a designated target in one of the tracked targets, +/// and append instructions to the given destination. +class instrument_spec_assignst +{ +public: + /// \brief Class constructor. + /// + /// \param _function_id name of the instrumented function + /// \param _functions other functions of the model + /// \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, + symbol_tablet &_st, + message_handlert &_message_handler) + : function_id(_function_id), + functions(_functions), + st(_st), + ns(_st), + log(_message_handler) + { + } + + /// Track an assigns clause target and generate snaphsot instructions + /// and well-definedness assertions in dest. + void track_spec_target(const exprt &expr, goto_programt &dest); + + /// Track a stack-allocated object and generate snaphsot instructions in dest. + void + track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest); + + /// Returns true if the expression is tracked. + bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const; + + /// Generate instructions to invalidate a + /// stack-allocated object that goes DEAD in dest. + void invalidate_stack_allocated( + const symbol_exprt &symbol_expr, + goto_programt &dest); + + /// Track a whole heap-alloc object and generate snaphsot instructions + /// 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. + void track_static_locals(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 + /// \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); + + /// 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); + +protected: + /// Name of the instrumented function + const irep_idt &function_id; + + /// Other functions of the model + const goto_functionst &functions; + + /// Program symbol table + symbol_tablet &st; + + /// Program namespace + const namespacet ns; + + /// Logger + messaget log; + + /// Track and generate snaphsot instructions and target validity + /// checking assertions for a conditional target group from an assigns clause + void track_spec_target_group( + const conditional_target_group_exprt &group, + goto_programt &dest); + + /// Track and generate snaphsot instructions and target validity + /// checking assertions for a conditional target group from an assigns clause + void track_plain_spec_target(const exprt &expr, goto_programt &dest); + + /// Creates a fresh symbolt with given suffix, + /// scoped to \ref function_id. + const symbolt create_fresh_symbol( + const std::string &suffix, + const typet &type, + const source_locationt &location) const; + + /// Returns snapshot instructions for a car_exprt + void create_snapshot(const car_exprt &car, goto_programt &dest) const; + + /// Returns the target validity expression for a car_exprt + exprt + target_validity_expr(const car_exprt &car, bool allow_null_target) const; + + /// Generates the target validity assertion for the given `car` and adds + /// it to `dest`. + /// The assertion checks that if the car's condition holds then + /// the target is `r_ok` (or `NULL` if `allow_null_targets` is true). + void target_validity_assertion( + const car_exprt &car, + bool allow_null_target, + goto_programt &dest) const; + + /// Returns inclusion check expression for a single candidate location + exprt inclusion_check_single( + const car_exprt &lhs, + const car_exprt &candidate_car) const; + + /// Returns an inclusion check expression 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 + /// \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; + + /// 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 + /// was valid before and was pointing to the same object as the freed car. + void invalidate_car( + const car_exprt &tracked_car, + const car_exprt &freed_car, + goto_programt &result) const; + + /// Generates instructions to invalidate all targets aliased with a + /// car that was passed to `free`, assuming the inclusion check passes, + /// ie. that the freed_car is fully included in one of the tracked targets. + void invalidate_heap_and_spec_aliases( + const car_exprt &freed_car, + goto_programt &dest) const; + + using cond_target_exprt_to_car_mapt = std:: + unordered_map; + + /// Map to from conditional target expressions of assigns clauses + /// to corresponding conditional address ranges. + cond_target_exprt_to_car_mapt from_spec_assigns; + + const car_exprt & + create_car_from_spec_assigns(const exprt &condition, const exprt &target); + + using symbol_exprt_to_car_mapt = + std::unordered_map; + + /// Map to from DECL symbols to corresponding conditional address ranges. + symbol_exprt_to_car_mapt from_stack_alloc; + + const car_exprt &create_car_from_stack_alloc(const symbol_exprt &target); + + using exprt_to_car_mapt = + std::unordered_map; + + /// Map to from malloc'd symbols to corresponding conditional address ranges. + exprt_to_car_mapt from_heap_alloc; + + const car_exprt &create_car_from_heap_alloc(const exprt &target); + + /// Creates a conditional address range expression from a cleaned-up condition + /// and target expression. + car_exprt create_car_expr(const exprt &condition, const exprt &target) const; +}; + +#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H From a61b669c875f5c409fd42a2fc1ddd3f423fc63ce Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 25 Jan 2022 02:42:42 +0000 Subject: [PATCH 3/7] CONTRACTS: Make havoc_assigns_clause_targets a class that inherits from instrument_assigns_clauset. Eliminate code duplication for CAR calculation, target validity assertions properly handle condition cleaning, local statics when havocking assigns clauses. --- .../havoc_assigns_clause_targets.cpp | 269 +++--------------- .../contracts/havoc_assigns_clause_targets.h | 70 ++++- 2 files changed, 97 insertions(+), 242 deletions(-) diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp index a5d02adf564..f0e1d51bf7a 100644 --- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp @@ -26,6 +26,7 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include +#include "instrument_spec_assigns.h" #include "utils.h" static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[] = @@ -46,268 +47,80 @@ bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment) std::string::npos; } -/// Returns a pointer expression to the start address of the target -/// -/// - If the target is a `pointer_object(p)` expression, -/// return a pointer to the same object with offset zero -/// - else, if the target is a sized and assignable expression, -/// return its address -/// - else trigger an error. -/// -static exprt build_address_of( - const exprt &target, - // context parameters - const namespacet &ns) +void havoc_assigns_clause_targetst::get_instructions(goto_programt &dest) { - if(target.id() == ID_pointer_object) - { - const auto &ptr = target.operands().front(); - // bring the offset back to zero - return minus_exprt{ptr, pointer_offset(ptr)}; - } - else if(is_assignable(target)) - { - INVARIANT( - size_of_expr(target.type(), ns).has_value(), - "`sizeof` must always be computable on assignable assigns clause " - "targets."); - - return address_of_exprt{target}; - } - - UNREACHABLE; -} - -/// \brief Generates instructions to conditionally snapshot the value -/// of `target_pointer` into `target_snapshot_var`. -/// -/// ``` -/// DECL target_valid_var : bool; -/// DECL target_snapshot_var : ; -/// ASSIGN target_valid_var := & -/// ; -/// ASSIGN target_snapshot_var := NULL; -/// IF !target_valid_var GOTO skip_target; -/// ASSIGN target_snapshot_var := target_pointer; -/// skip_target: SKIP; -/// ``` -/// -static void snapshot_if_valid( - const symbol_exprt &target_valid_var, - const symbol_exprt &target_snapshot_var, - const exprt &condition, - const exprt &target_pointer, - goto_programt &dest, - // context parameters - const source_locationt &source_location, - const namespacet &ns) -{ - source_locationt source_location_no_checks(source_location); - disable_pointer_checks(source_location_no_checks); - - dest.add(goto_programt::make_decl(target_valid_var)); - - dest.add(goto_programt::make_decl(target_snapshot_var)); - - const not_exprt not_null(null_pointer(target_pointer)); - const not_exprt not_invalid{is_invalid_pointer_exprt{target_pointer}}; + // snapshotting instructions and well-definedness checks + goto_programt snapshot_program; - dest.add(goto_programt::make_assignment( - target_valid_var, - and_exprt{condition, not_null, not_invalid}, - source_location_no_checks)); + // add spec targets + for(const auto &target : targets) + track_spec_target(target, snapshot_program); - dest.add(goto_programt::make_assignment( - target_snapshot_var, - null_pointer_exprt{to_pointer_type(target_pointer.type())}, - source_location_no_checks)); + // add static locals called touched by the replaced function + track_static_locals(snapshot_program); - goto_programt skip_program; - const auto skip_target = - skip_program.add(goto_programt::make_skip(source_location_no_checks)); + // generate havocking instructions for all tracked CARs + goto_programt havoc_program; + for(const auto &pair : from_spec_assigns) + havoc_if_valid(pair.second, havoc_program); - dest.add(goto_programt::make_goto( - skip_target, not_exprt{target_valid_var}, source_location_no_checks)); + for(const auto &pair : from_stack_alloc) + havoc_if_valid(pair.second, havoc_program); - dest.add(goto_programt::make_assignment( - target_snapshot_var, target_pointer, source_location_no_checks)); + for(const auto &pair : from_heap_alloc) + havoc_if_valid(pair.second, havoc_program); - dest.destructive_append(skip_program); + // append to dest + dest.destructive_append(snapshot_program); + dest.destructive_append(havoc_program); } -/// \brief Generates instructions to conditionally havoc -/// the given `target_snapshot_var`. -/// -/// Generates these instructions if target is a `__CPROVER_POINTER_OBJECT(...)`: -/// -/// ``` -/// IF !target_valid_var GOTO skip_target -/// OTHER havoc_object(target_snapshot_var) -/// skip_target: SKIP -/// DEAD target_valid_var -/// DEAD target_snapshot_var -/// ``` -/// -/// And generate these instructions otherwise: -/// -/// ``` -/// IF !target_valid_var GOTO skip_target -/// ASSIGN *target_snapshot_var = nondet() -/// skip_target: SKIP -/// DEAD target_valid_var -/// DEAD target_snapshot_var -/// ``` -/// Adds a special comment on the havoc instructions in order to trace back -/// the havoc to the replaced function. -static void havoc_if_valid( - const symbol_exprt &target_valid_var, - const symbol_exprt &target_snapshot_var, - const exprt &target, - const irep_idt &tracking_comment, - goto_programt &dest, - // context parameters - const source_locationt &source_location, - const namespacet &ns) +void havoc_assigns_clause_targetst::havoc_if_valid( + car_exprt car, + goto_programt &dest) { + const irep_idt &tracking_comment = + make_tracking_comment(car.target(), function_id, ns); + source_locationt source_location_no_checks(source_location); - disable_pointer_checks(source_location_no_checks); + add_pragma_disable_pointer_checks(source_location_no_checks); goto_programt skip_program; const auto skip_target = skip_program.add(goto_programt::make_skip(source_location_no_checks)); dest.add(goto_programt::make_goto( - skip_target, not_exprt{target_valid_var}, source_location_no_checks)); + skip_target, not_exprt{car.valid_var()}, source_location_no_checks)); - if(target.id() == ID_pointer_object) + if(car.target().id() == ID_pointer_object) { // OTHER __CPROVER_havoc_object(target_snapshot_var) - codet code(ID_havoc_object, {target_snapshot_var}); + codet code(ID_havoc_object, {car.lower_bound_var()}); const auto &inst = dest.add(goto_programt::make_other(code, source_location)); inst->source_location_nonconst().set_comment(tracking_comment); } else { - // ASSIGN *target_snapshot_var = nondet() - side_effect_expr_nondett nondet(target.type(), source_location); + // ASSIGN *(target.type() *)__car_lb = nondet(car.target().type()) + const auto &target_type = car.target().type(); + side_effect_expr_nondett nondet(target_type, source_location); const auto &inst = dest.add(goto_programt::make_assignment( - dereference_exprt{target_snapshot_var}, nondet, source_location)); + dereference_exprt{typecast_exprt::conditional_cast( + car.lower_bound_var(), pointer_type(target_type))}, + nondet, + source_location)); inst->source_location_nonconst().set_comment(tracking_comment); } dest.destructive_append(skip_program); dest.add( - goto_programt::make_dead(target_valid_var, source_location_no_checks)); + goto_programt::make_dead(car.valid_var(), source_location_no_checks)); dest.add( - goto_programt::make_dead(target_snapshot_var, source_location_no_checks)); -} + goto_programt::make_dead(car.lower_bound_var(), source_location_no_checks)); -void havoc_single_target( - const exprt &condition, - const exprt &target, - const source_locationt &source_location, - const irep_idt &replaced_function_id, - goto_programt &snapshot_program, - goto_programt &havoc_program, - const namespacet &ns, - symbol_tablet &st, - irep_idt mode) -{ - const auto target_pointer = build_address_of(target, ns); - const auto target_snapshot_var = new_tmp_symbol( - target_pointer.type(), - source_location, - mode, - st, - "__target_snapshot_var", - true) - .symbol_expr(); - const auto target_valid_var = - new_tmp_symbol( - bool_typet(), source_location, mode, st, "__target_valid_var", true) - .symbol_expr(); - - snapshot_if_valid( - target_valid_var, - target_snapshot_var, - condition, - target_pointer, - snapshot_program, - source_location, - ns); - - const auto &tracking_comment = - make_tracking_comment(target, replaced_function_id, ns); - - havoc_if_valid( - target_valid_var, - target_snapshot_var, - target, - tracking_comment, - havoc_program, - source_location, - ns); -} - -void havoc_assigns_clause_targets( - const irep_idt &replaced_function_id, - const std::vector &targets, - goto_programt &dest, - // context parameters - const source_locationt &source_location, - const irep_idt &mode, - namespacet &ns, - symbol_tablet &st, - message_handlert &message_handler) -{ - goto_programt snapshot_program; - goto_programt havoc_program; - - for(const auto &target : targets) - { - if(can_cast_expr(target)) - { - const auto &cond_target = to_conditional_target_group_expr(target); - - // clean the condition if needed - cleanert cleaner(st, message_handler); - exprt condition(cond_target.condition()); - if(has_subexpr(condition, ID_side_effect)) - cleaner.clean(condition, snapshot_program, mode); - - for(const auto &actual_target : cond_target.targets()) - { - havoc_single_target( - condition, - actual_target, - source_location, - replaced_function_id, - snapshot_program, - havoc_program, - ns, - st, - mode); - } - } - else - { - // nonconditional target - havoc_single_target( - true_exprt{}, - target, - source_location, - replaced_function_id, - snapshot_program, - havoc_program, - ns, - st, - mode); - } - } - - dest.destructive_append(snapshot_program); - dest.destructive_append(havoc_program); + dest.add( + goto_programt::make_dead(car.upper_bound_var(), source_location_no_checks)); } diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h index 24fa1daa07f..156817d5f87 100644 --- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h @@ -12,19 +12,23 @@ Author: Remi Delmas, delmasrd@amazon.com #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H +#include "instrument_spec_assigns.h" #include class namespacet; class symbol_tablet; class goto_programt; +class goto_functionst; class message_handlert; -/// Generates havocking instructions for target expressions of a +bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment); + +/// Class to generate havocking instructions for target expressions of a /// function contract's assign clause (replacement). /// /// \param replaced_function_id Name of the replaced function -/// \param targets Assigns clause targets -/// \param dest Destination program where the instructions are generated +/// \param goto_functions Other functions forming the GOTO model +/// \param targets Assigns clause targets for the replaced function /// \param source_location Source location of the replaced function call /// (added to all generated instructions) /// \param mode Language mode to use for newly generated symbols @@ -49,17 +53,55 @@ class message_handlert; /// of their addresses, and havoc them in a second time. /// Snapshotting and havocking are both guarded by the validity of the target. /// -void havoc_assigns_clause_targets( - const irep_idt &replaced_function_id, - const std::vector &targets, - goto_programt &dest, - // context parameters - const source_locationt &source_location, - const irep_idt &mode, - namespacet &ns, - symbol_tablet &st, - message_handlert &message_handler); +class havoc_assigns_clause_targetst : public instrument_spec_assignst +{ +public: + havoc_assigns_clause_targetst( + const irep_idt &_function_id, + const std::vector &_targets, + const goto_functionst &_functions, + const source_locationt &_source_location, + symbol_tablet &_st, + message_handlert &_message_handler) + : instrument_spec_assignst(_function_id, _functions, _st, _message_handler), + targets(_targets), + source_location(_source_location) + { + } -bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment); + /// Generates the assigns clause replacement instructions in dest. + void get_instructions(goto_programt &dest); + +private: + /// \brief Generates instructions to conditionally havoc + /// the given `car_exprt`. + /// + /// Generates these instructions for a `__CPROVER_POINTER_OBJECT(...)` target: + /// + /// ``` + /// IF !__car_writable GOTO skip_target + /// OTHER havoc_object(_car_lb) + /// skip_target: SKIP + /// DEAD __car_writable + /// DEAD __car_lb + /// DEAD __car_ub + /// ``` + /// + /// And generate these instructions otherwise: + /// + /// ``` + /// IF !__car_writable GOTO skip_target + /// ASSIGN * (( *)_car_lb) = nondet_; + /// skip_target: SKIP + /// DEAD __car_writable + /// DEAD __car_lb + /// DEAD __car_ub + /// ``` + /// Adds a special comment on the havoc instructions in order to trace back + /// the havoc to the replaced function. + void havoc_if_valid(car_exprt car, goto_programt &dest); + const std::vector &targets; + const source_locationt &source_location; +}; #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H From f28f7bad8cc6f543f23e66a0b818ffd5c8778dc1 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 25 Jan 2022 02:47:44 +0000 Subject: [PATCH 4/7] CONTRACTS: Move code to utils - Move havoc_assigns_clauset from contract/assigns to utils - Moving functions for tracking assigns clause replacement to utils to break circular dependency - Unified interface for adding "disable:check" pragmas on locations, instructions and programs --- .../havoc_assigns_clause_targets.cpp | 28 +---- .../contracts/havoc_assigns_clause_targets.h | 14 +-- src/goto-instrument/contracts/utils.cpp | 102 +++++++++++++----- src/goto-instrument/contracts/utils.h | 54 +++++++++- 4 files changed, 141 insertions(+), 57 deletions(-) diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp index f0e1d51bf7a..b03b626718f 100644 --- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp @@ -13,10 +13,6 @@ Author: Remi Delmas, delmasrd@amazon.com #include -#include - -#include - #include #include #include @@ -26,27 +22,12 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include +#include +#include + #include "instrument_spec_assigns.h" #include "utils.h" -static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[] = - " (assigned by the contract of "; - -static irep_idt make_tracking_comment( - const exprt &target, - const irep_idt &function_id, - const namespacet &ns) -{ - return from_expr(ns, target.id(), target) + - ASSIGNS_CLAUSE_REPLACEMENT_TRACKING + id2string(function_id) + ")"; -} - -bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment) -{ - return id2string(comment).find(ASSIGNS_CLAUSE_REPLACEMENT_TRACKING) != - std::string::npos; -} - void havoc_assigns_clause_targetst::get_instructions(goto_programt &dest) { // snapshotting instructions and well-definedness checks @@ -80,7 +61,8 @@ void havoc_assigns_clause_targetst::havoc_if_valid( goto_programt &dest) { const irep_idt &tracking_comment = - make_tracking_comment(car.target(), function_id, ns); + make_assigns_clause_replacement_tracking_comment( + car.target(), function_id, ns); source_locationt source_location_no_checks(source_location); add_pragma_disable_pointer_checks(source_location_no_checks); diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h index 156817d5f87..83ed3dfd5a8 100644 --- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h @@ -21,8 +21,6 @@ class goto_programt; class goto_functionst; class message_handlert; -bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment); - /// Class to generate havocking instructions for target expressions of a /// function contract's assign clause (replacement). /// @@ -73,8 +71,11 @@ class havoc_assigns_clause_targetst : public instrument_spec_assignst void get_instructions(goto_programt &dest); private: - /// \brief Generates instructions to conditionally havoc - /// the given `car_exprt`. + /// \brief Generates instructions to conditionally havoc the given conditional + /// address range expression `car`, adding results to `dest`. + /// + /// Adds a special comment on the havoc instructions in order to trace back + /// the origin of the havoc expressions to the function being replaced. /// /// Generates these instructions for a `__CPROVER_POINTER_OBJECT(...)` target: /// @@ -91,14 +92,13 @@ class havoc_assigns_clause_targetst : public instrument_spec_assignst /// /// ``` /// IF !__car_writable GOTO skip_target - /// ASSIGN * (( *)_car_lb) = nondet_; + /// ASSIGN *((target_type *) _car_lb) = nondet(target_type); /// skip_target: SKIP /// DEAD __car_writable /// DEAD __car_lb /// DEAD __car_ub /// ``` - /// Adds a special comment on the havoc instructions in order to trace back - /// the havoc to the replaced function. + /// Where `target_type` is the type of the target expression. void havoc_if_valid(car_exprt car, goto_programt &dest); const std::vector &targets; diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 31902f60d25..a6e40f785d6 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -11,6 +11,7 @@ Date: September 2021 #include "utils.h" #include + #include #include #include @@ -18,20 +19,7 @@ Date: September 2021 #include #include -goto_programt::instructiont & -add_pragma_disable_assigns_check(goto_programt::instructiont &instr) -{ - instr.source_location_nonconst().add_pragma( - CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK); - 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; -} +#include static void append_safe_havoc_code_for_expr( const source_locationt location, @@ -74,6 +62,63 @@ void havoc_if_validt::append_scalar_havoc_code_for_expr( }); } +void havoc_assigns_targetst::append_havoc_code_for_expr( + const source_locationt location, + const exprt &expr, + goto_programt &dest) const +{ + if(expr.id() == ID_pointer_object) + { + append_object_havoc_code_for_expr(location, expr.operands().front(), dest); + return; + } + + 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; @@ -156,16 +201,6 @@ const symbolt &new_tmp_symbol( return new_symbol; } -void disable_pointer_checks(source_locationt &source_location) -{ - source_location.add_pragma("disable:pointer-check"); - source_location.add_pragma("disable:pointer-primitive-check"); - source_location.add_pragma("disable:pointer-overflow-check"); - source_location.add_pragma("disable:signed-overflow-check"); - source_location.add_pragma("disable:unsigned-overflow-check"); - source_location.add_pragma("disable:conversion-check"); -} - void simplify_gotos(goto_programt &goto_program, namespacet &ns) { for(auto &instruction : goto_program.instructions) @@ -226,3 +261,22 @@ bool is_loop_free( } return true; } + +/// Prefix for comments added to track assigns clause replacement. +static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[] = + " (assigned by the contract of "; + +irep_idt make_assigns_clause_replacement_tracking_comment( + const exprt &target, + const irep_idt &function_id, + const namespacet &ns) +{ + return from_expr(ns, target.id(), target) + + ASSIGNS_CLAUSE_REPLACEMENT_TRACKING + id2string(function_id) + ")"; +} + +bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment) +{ + return id2string(comment).find(ASSIGNS_CLAUSE_REPLACEMENT_TRACKING) != + std::string::npos; +} diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 04a4d917426..6fe53c46c24 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -51,6 +51,46 @@ class havoc_if_validt : public havoc_utilst const namespacet &ns; }; +/// \brief A class that further overrides the "safe" havoc utilities, +/// and adds support for havocing pointer_object expressions. +class havoc_assigns_targetst : public havoc_if_validt +{ +public: + havoc_assigns_targetst(const assignst &mod, const namespacet &ns) + : havoc_if_validt(mod, ns) + { + } + + void append_havoc_code_for_expr( + const source_locationt location, + const exprt &expr, + 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. @@ -129,9 +169,6 @@ const symbolt &new_tmp_symbol( std::string suffix = "tmp_cc", bool is_auxiliary = true); -/// Add disable pragmas for all pointer checks on the given location -void disable_pointer_checks(source_locationt &source_location); - /// Turns goto instructions `IF cond GOTO label` where the condition /// statically simplifies to `false` into SKIP instructions. void simplify_gotos(goto_programt &goto_program, namespacet &ns); @@ -224,4 +261,15 @@ class cleanert : public goto_convertt } }; +/// Returns an \ref irep_idt that essentially says that +/// `target` was assigned by the contract of `function_id`. +irep_idt make_assigns_clause_replacement_tracking_comment( + const exprt &target, + const irep_idt &function_id, + const namespacet &ns); + +/// Returns true if the given comment matches the type of comments created by +/// \ref make_assigns_clause_replacement_tracking_comment. +bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment); + #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H From cc143a0c17dd745d83a17d3370c50b86fcef2809 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 25 Jan 2022 02:48:33 +0000 Subject: [PATCH 5/7] CONTRACTS: Remove assigns.cpp - Remove the old assigns clause checking implementation - Remove assigns.cpp from the Makefile. --- src/goto-instrument/Makefile | 1 - src/goto-instrument/contracts/assigns.cpp | 346 ---------------------- src/goto-instrument/contracts/assigns.h | 184 ------------ 3 files changed, 531 deletions(-) delete mode 100644 src/goto-instrument/contracts/assigns.cpp delete mode 100644 src/goto-instrument/contracts/assigns.h diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index d8c6fdd02c8..707d3780677 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -16,7 +16,6 @@ SRC = accelerate/accelerate.cpp \ alignment_checks.cpp \ branch.cpp \ call_sequences.cpp \ - contracts/assigns.cpp \ contracts/contracts.cpp \ contracts/havoc_assigns_clause_targets.cpp \ contracts/instrument_spec_assigns.cpp \ diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp deleted file mode 100644 index 32df3041401..00000000000 --- a/src/goto-instrument/contracts/assigns.cpp +++ /dev/null @@ -1,346 +0,0 @@ -/*******************************************************************\ - -Module: Specify write set in code contracts. - -Author: Felipe R. Monteiro - -Date: July 2021 - -\*******************************************************************/ - -/// \file -/// Specify write set in code contracts - -#include "assigns.h" -#include "utils.h" - -#include - -#include - -#include - -#include -#include -#include -#include -#include -#include - -static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns) -{ - // FIXME: Refactor these checks out to a common function that can be - // used both in compilation and instrumentation stages - if(expr.id() == ID_pointer_object) - { - const auto &arg = expr.operands().front(); - return { - minus_exprt{ - typecast_exprt::conditional_cast(arg, pointer_type(char_type())), - pointer_offset(arg)}, - typecast_exprt::conditional_cast(object_size(arg), signed_size_type())}; - } - else if(is_assignable(expr)) - { - const auto &size = size_of_expr(expr.type(), ns); - - INVARIANT( - size.has_value(), - "no definite size for lvalue target: \n" + expr.pretty()); - - return {typecast_exprt::conditional_cast( - address_of_exprt{expr}, pointer_type(char_type())), - typecast_exprt::conditional_cast(size.value(), signed_size_type())}; - } - - UNREACHABLE; -} - -/// Normalises a assigns target expression to a guarded slice struct. -/// -/// ``` -/// case expr of -/// | guard ? target -> -/// {guard -/// target, -/// normalize_to_slice(target)} -/// | target -> -/// {true, -/// target, -/// normalize_to_slice(target)} -/// ``` -static const guarded_slicet -normalize_to_guarded_slice(const exprt &expr, const namespacet &ns) -{ - if(can_cast_expr(expr)) - { - const auto &conditional_target_group = - to_conditional_target_group_expr(expr); - INVARIANT( - conditional_target_group.targets().size() == 1, - "expecting only a single target"); - const auto &target = conditional_target_group.targets().front(); - const auto slice = normalize_to_slice(target, ns); - return { - conditional_target_group.condition(), target, slice.first, slice.second}; - } - else - { - const auto slice = normalize_to_slice(expr, ns); - return {true_exprt{}, expr, slice.first, slice.second}; - } -} - -const symbolt assigns_clauset::conditional_address_ranget::generate_new_symbol( - const std::string &prefix, - const typet &type, - const source_locationt &location) const -{ - return new_tmp_symbol( - type, - location, - parent.symbol_table.lookup_ref(parent.function_name).mode, - parent.symbol_table, - prefix); -} - -assigns_clauset::conditional_address_ranget::conditional_address_ranget( - const assigns_clauset &parent, - const exprt &expr) - : source_expr(expr), - location(expr.source_location()), - parent(parent), - guarded_slice(normalize_to_guarded_slice(expr, parent.ns)), - validity_condition_var( - generate_new_symbol("__car_valid", bool_typet(), location).symbol_expr()), - lower_bound_address_var(generate_new_symbol( - "__car_lb", - guarded_slice.start_address.type(), - location) - .symbol_expr()), - upper_bound_address_var(generate_new_symbol( - "__car_ub", - guarded_slice.start_address.type(), - location) - .symbol_expr()) -{ -} - -goto_programt -assigns_clauset::conditional_address_ranget::generate_snapshot_instructions( - check_target_validityt check_target_validity) const -{ - goto_programt instructions; - - // clean up side effects from the guard expression if needed - cleanert cleaner(parent.symbol_table, parent.log.get_message_handler()); - exprt clean_guard(guarded_slice.guard); - - if(has_subexpr(clean_guard, ID_side_effect)) - cleaner.clean( - clean_guard, - instructions, - parent.symbol_table.lookup_ref(parent.function_name).mode); - - // we want checks on the guard because it is user code - clean_guard.add_source_location() = location; - - // adding pragmas to the location to selectively disable checks - // where it is sound to do so - source_locationt location_no_checks(location); - disable_pointer_checks(location_no_checks); - - // If requested, we check that when guard condition is true, - // the target's `start_address` pointer satisfies w_ok with the expected size - // (or is NULL if we allow it explicitly). - // This assertion will be falsified whenever `start_address` is invalid or - // not of the right size (or is NULL if we dot not allow it expliclitly). - auto validity_check_expr = - check_target_validity == check_target_validityt::YES_ALLOW_NULL - ? or_exprt{not_exprt{clean_guard}, - null_pointer(guarded_slice.start_address), - w_ok_exprt{guarded_slice.start_address, guarded_slice.size}} - : or_exprt{not_exprt{clean_guard}, - w_ok_exprt{guarded_slice.start_address, guarded_slice.size}}; - - if(check_target_validity != check_target_validityt::NO) - { - auto target_validity_assert = - instructions.add(goto_programt::make_assertion( - simplify_expr(validity_check_expr, parent.ns), location_no_checks)); - - target_validity_assert->source_location_nonconst().set_comment( - "Check assigns target validity '" + - from_expr(parent.ns, "", guarded_slice.guard) + ": " + - from_expr(parent.ns, "", guarded_slice.expr) + "'"); - } - - // ~~~ From then on we implicitly assume that the assertion holds ~~~ // - - // We snapshot the validity condition, lower bound and upper bound addresses - instructions.add( - goto_programt::make_decl(validity_condition_var, location_no_checks)); - - instructions.add(goto_programt::make_assignment( - validity_condition_var, - simplify_expr( - and_exprt{clean_guard, - not_exprt{null_pointer(guarded_slice.start_address)}}, - parent.ns), - location_no_checks)); - - instructions.add( - goto_programt::make_decl(lower_bound_address_var, location_no_checks)); - - instructions.add(goto_programt::make_assignment( - lower_bound_address_var, guarded_slice.start_address, location_no_checks)); - - instructions.add( - goto_programt::make_decl(upper_bound_address_var, location_no_checks)); - - instructions.add(goto_programt::make_assignment( - upper_bound_address_var, - simplify_expr( - plus_exprt{guarded_slice.start_address, guarded_slice.size}, parent.ns), - location_no_checks)); - - // The snapshot assignments involve only instrumentation variables - // need not be checked against the surrounding assigns clause. - add_pragma_disable_assigns_check(instructions); - return instructions; -} - -const exprt -assigns_clauset::conditional_address_ranget::generate_unsafe_inclusion_check( - const conditional_address_ranget &lhs) const -{ - // remark: both lb and ub are derived from the same object so checking - // same_object(upper_bound_address_var, lhs.upper_bound_address_var) - // is redundant - return conjunction( - {validity_condition_var, - same_object(lower_bound_address_var, lhs.lower_bound_address_var), - less_than_or_equal_exprt{pointer_offset(lower_bound_address_var), - pointer_offset(lhs.lower_bound_address_var)}, - less_than_or_equal_exprt{pointer_offset(lhs.upper_bound_address_var), - pointer_offset(upper_bound_address_var)}}); -} - -bool assigns_clauset::conditional_address_ranget::maybe_alive( - cfg_infot &cfg_info) const -{ - if(can_cast_expr(source_expr)) - return cfg_info.is_maybe_alive(to_symbol_expr(source_expr)); - - return true; -} - -assigns_clauset::assigns_clauset( - const exprt::operandst &assigns, - messaget &log, - const namespacet &ns, - const irep_idt &function_name, - symbol_tablet &symbol_table) - : log(log), ns(ns), function_name(function_name), symbol_table(symbol_table) -{ - for(const auto &target_expr : assigns) - add_to_write_set(target_expr); -} - -assigns_clauset::write_sett::const_iterator -assigns_clauset::add_to_write_set(const exprt &target_expr) -{ - auto result = write_set.emplace(*this, target_expr); - - if(!result.second) - { - log.warning() << "Ignored duplicate expression '" - << from_expr(ns, target_expr.id(), target_expr) - << "' in assigns clause at " - << target_expr.source_location().as_string() << messaget::eom; - } - return result.first; -} - -void assigns_clauset::remove_from_write_set(const exprt &target_expr) -{ - write_set.erase(conditional_address_ranget(*this, target_expr)); -} - -exprt assigns_clauset::generate_inclusion_check( - const conditional_address_ranget &lhs, - check_target_validityt allow_null_target, - optionalt &cfg_info_opt) const -{ - if(write_set.empty()) - { - if(allow_null_target == check_target_validityt::YES_ALLOW_NULL) - return false_exprt{}; - else - return null_pointer(lhs.guarded_slice.start_address); - } - - exprt::operandst conditions; - - if(cfg_info_opt.has_value()) - { - auto &cfg_info = cfg_info_opt.value(); - for(const auto &target : write_set) - if(target.maybe_alive(cfg_info)) - conditions.push_back(target.generate_unsafe_inclusion_check(lhs)); - } - else - { - for(const auto &target : write_set) - conditions.push_back(target.generate_unsafe_inclusion_check(lhs)); - } - - if(allow_null_target == check_target_validityt::YES_ALLOW_NULL) - return or_exprt{ - null_pointer(lhs.guarded_slice.start_address), - and_exprt{lhs.validity_condition_var, disjunction(conditions)}}; - else - return and_exprt{lhs.validity_condition_var, disjunction(conditions)}; -} - -void havoc_assigns_targetst::append_havoc_code_for_expr( - const source_locationt location, - const exprt &expr, - goto_programt &dest) const -{ - if(expr.id() == ID_pointer_object) - { - append_object_havoc_code_for_expr(location, expr.operands().front(), dest); - return; - } - - havoc_utilst::append_havoc_code_for_expr(location, expr, dest); -} - -void assigns_clauset::add_static_locals_to_write_set( - const goto_functionst &functions, - const irep_idt &root_function) -{ - auto call_graph = - call_grapht::create_from_root_function(functions, root_function, true) - .get_directed_graph(); - - for(const auto &sym_pair : symbol_table) - { - const auto &sym = sym_pair.second; - if(sym.is_static_lifetime) - { - auto fname = sym.location.get_function(); - if( - !fname.empty() && (fname == root_function || - call_graph.get_node_index(fname).has_value())) - { - // We found a symbol with - // - a static lifetime - // - non empty location function - // - this function appears in the call graph of the function - add_to_write_set(sym.symbol_expr()); - } - } - } -} diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h deleted file mode 100644 index 6a17a1a2a74..00000000000 --- a/src/goto-instrument/contracts/assigns.h +++ /dev/null @@ -1,184 +0,0 @@ -/*******************************************************************\ - -Module: Specify write set in code contracts. - -Author: Felipe R. Monteiro - -Date: July 2021 - -\*******************************************************************/ - -/// \file -/// Specify write set in function contracts - -#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H -#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H - -#include - -#include - -#include "utils.h" - -typedef std::pair slicet; - -/// A guarded slice of memory -typedef struct guarded_slicet -{ - guarded_slicet(exprt _guard, exprt _expr, exprt _start_address, exprt _size) - : guard(_guard), expr(_expr), start_address(_start_address), size(_size) - { - } - - /// Guard expression (may contain side_effect_exprt expressions) - const exprt guard; - - /// Target expression - const exprt expr; - - /// Start address of the target - const exprt start_address; - - /// Size of the target - const exprt size; -} guarded_slicet; - -/// \brief A class for representing assigns clauses in code contracts -class assigns_clauset -{ -public: - enum class check_target_validityt - { - YES, - YES_ALLOW_NULL, - NO - }; - - /// \brief A class for representing Conditional Address Ranges - class conditional_address_ranget - { - public: - conditional_address_ranget(const assigns_clauset &, const exprt &); - - /// \brief Returns a program that computes a snapshot of the CAR. - /// - /// In addition, if check_target_validity is Yes, generates: - /// ``` - /// ASSERT - /// condition ==> w_ok(target_start_address, target_size) - /// ``` - // - /// else if check_target_validity is YesAlloNull, generates: - /// ``` - /// ASSERT - /// condition ==> - /// (target_start_address==NULL || - /// w_ok(target_start_address, target_size)) - /// ``` - goto_programt generate_snapshot_instructions( - check_target_validityt check_target_validity) const; - - bool operator==(const conditional_address_ranget &other) const - { - return source_expr == other.source_expr; - } - - struct hasht - { - std::size_t operator()(const conditional_address_ranget &target) const - { - return irep_hash{}(target.source_expr); - } - }; - - /// Returns true whenever this CAR's `source_expr` and associated address - /// range may be alive at the instruction currently pointed to by - /// `cfg_info.target`. - bool maybe_alive(cfg_infot &cfg_info) const; - - const exprt source_expr; - const source_locationt &location; - const assigns_clauset &parent; - - const guarded_slicet guarded_slice; - const symbol_exprt validity_condition_var; - const symbol_exprt lower_bound_address_var; - const symbol_exprt upper_bound_address_var; - - protected: - const exprt - generate_unsafe_inclusion_check(const conditional_address_ranget &) const; - - const symbolt generate_new_symbol( - const std::string &prefix, - const typet &, - const source_locationt &) const; - - friend class assigns_clauset; - }; - - typedef std:: - unordered_set - write_sett; - - assigns_clauset( - const exprt::operandst &assigns, - messaget &log, - const namespacet &ns, - const irep_idt &function_name, - symbol_tablet &symbol_table); - - write_sett::const_iterator add_to_write_set(const exprt &); - void remove_from_write_set(const exprt &); - - exprt generate_inclusion_check( - const conditional_address_ranget &lhs, - check_target_validityt allow_null_target, - optionalt &cfg_info_opt) const; - - const write_sett &get_write_set() const - { - return write_set; - } - - /// \brief Finds symbols declared with a static lifetime in the given - /// `root_function` or one of the functions it calls, - /// and adds them to the write set of this assigns clause. - /// - /// @param functions all functions of the goto_model - /// @param root_function the root function under which to search statics - /// - /// A symbol is considered a static local symbol iff: - /// - it has a static lifetime annotation - /// - its source location has a non-empty function attribute - /// - this function attribute is found in the call graph of the root_function - void add_static_locals_to_write_set( - const goto_functionst &functions, - const irep_idt &root_function); - - messaget &log; - const namespacet &ns; - const irep_idt &function_name; - -protected: - symbol_tablet &symbol_table; - write_sett write_set; -}; - -/// \brief A class that further overrides the "safe" havoc utilities, -/// and adds support for havocing pointer_object expressions. -class havoc_assigns_targetst : public havoc_if_validt -{ -public: - havoc_assigns_targetst(const assignst &mod, const namespacet &ns) - : havoc_if_validt(mod, ns) - { - } - - void append_havoc_code_for_expr( - const source_locationt location, - const exprt &expr, - goto_programt &dest) const override; -}; - -#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H From b18fb5015d09b13ed42856db351aa5b469981fc1 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 25 Jan 2022 02:49:13 +0000 Subject: [PATCH 6/7] CONTRACTS: Remove assigns clause checking logic that is now in instrument_assigns_clauset. --- src/goto-instrument/contracts/contracts.cpp | 348 +++++++------------- src/goto-instrument/contracts/contracts.h | 30 +- 2 files changed, 118 insertions(+), 260 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 1eb98ce57a4..2a420f75d50 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -44,6 +44,7 @@ Date: February 2016 #include #include "havoc_assigns_clause_targets.h" +#include "instrument_spec_assigns.h" #include "memory_predicates.h" #include "utils.h" @@ -160,11 +161,6 @@ void code_contractst::check_apply_loop_contracts( auto decreases_clause = static_cast( loop_end->get_condition().find(ID_C_spec_decreases)); - assigns_clauset loop_assigns( - assigns_clause.operands(), log, ns, function_name, symbol_table); - - loop_assigns.add_static_locals_to_write_set(goto_functions, function_name); - if(invariant.is_nil()) { if(decreases_clause.is_nil() && assigns_clause.is_nil()) @@ -255,6 +251,19 @@ void code_contractst::check_apply_loop_contracts( loop_head, add_pragma_disable_assigns_check(generated_code)); + instrument_spec_assignst instrument_spec_assigns( + function_name, goto_functions, symbol_table, log.get_message_handler()); + + // assigns clause snapshots + goto_programt snapshot_instructions; + + instrument_spec_assigns.track_static_locals(snapshot_instructions); + + // ^^^ FIXME ^^^ we should only allow assignments to static locals + // declared in functions that are called in the loop body, not from the whole + // function... + + // set of targets to havoc assignst to_havoc; if(assigns_clause.is_nil()) @@ -265,6 +274,8 @@ void code_contractst::check_apply_loop_contracts( try { get_assigns(local_may_alias, loop, to_havoc); + // TODO: if the set contains pairs (i, a[i]), + // we must at least widen them to (i, pointer_object(a)) log.debug() << "No loop assigns clause provided. Inferred targets {"; // Add inferred targets to the loop assigns clause. bool ran_once = false; @@ -274,7 +285,8 @@ void code_contractst::check_apply_loop_contracts( log.debug() << ", "; ran_once = true; log.debug() << format(target); - loop_assigns.add_to_write_set(target); + instrument_spec_assigns.track_spec_target( + target, snapshot_instructions); } log.debug() << "}. Please specify an assigns clause if verification fails." @@ -293,22 +305,18 @@ void code_contractst::check_apply_loop_contracts( { // An assigns clause was specified for this loop. // Add the targets to the set of expressions to havoc. - // TODO: Should we add the automatically detected local static variables - // too ? (they are present in loop_assigns but not in assigns_clause, and - // they are not necessarily touched by the loop). - to_havoc.insert( - assigns_clause.operands().cbegin(), assigns_clause.operands().cend()); + for(const auto &target : assigns_clause.operands()) + { + to_havoc.insert(target); + instrument_spec_assigns.track_spec_target(target, snapshot_instructions); + } } - // Create snapshots of write set CARs. + // Insert instrumentation // This must be done before havocing the write set. - for(const auto &car : loop_assigns.get_write_set()) - { - auto snapshot_instructions = car.generate_snapshot_instructions( - assigns_clauset::check_target_validityt::YES_ALLOW_NULL); - insert_before_swap_and_advance( - goto_function.body, loop_head, snapshot_instructions); - }; + // ^^^ FIXME this is not true ^^^ + insert_before_swap_and_advance( + goto_function.body, loop_head, snapshot_instructions); optionalt cfg_empty_info; @@ -318,12 +326,13 @@ void code_contractst::check_apply_loop_contracts( goto_function.body, loop_head, loop_end, - loop_assigns, + instrument_spec_assigns, // do not skip checks on function parameter assignments skipt::DontSkip, // do not use CFG info for now cfg_empty_info); + // insert havocing code havoc_assigns_targetst havoc_gen(to_havoc, ns); havoc_gen.append_full_havoc_code( loop_head->source_location(), generated_code); @@ -339,6 +348,13 @@ void code_contractst::check_apply_loop_contracts( insert_before_swap_and_advance( goto_function.body, loop_head, generated_code); + // ^^^ FIXME ^^^ + // comment by delmasrd: I did not reactivate this behaviour + // because I think we always want to check the loop assignments against + // the surrounding clause + + insert_before_swap_and_advance(goto_function.body, loop_head, generated_code); + // Generate: assume(invariant) just after havocing // We use a block scope to create a temporary assumption, // and immediately convert it to goto instructions. @@ -794,16 +810,14 @@ bool code_contractst::apply_function_contract( { // Havoc all targets in the assigns clause // TODO: handle local statics possibly touched by this function - havoc_assigns_clause_targets( + havoc_assigns_clause_targetst havocker( target_function, targets.operands(), - havoc_instructions, - // context parameters + goto_functions, location, - mode, - ns, symbol_table, log.get_message_handler()); + havocker.get_instructions(havoc_instructions); } // ...for the return value @@ -949,23 +963,22 @@ goto_functionst &code_contractst::get_goto_functions() void code_contractst::instrument_assign_statement( goto_programt::targett &instruction_it, goto_programt &program, - assigns_clauset &assigns_clause, + instrument_spec_assignst &instrument_spec_assigns, optionalt &cfg_info_opt) { - add_inclusion_check( - program, - assigns_clause, - instruction_it, - instruction_it->assign_lhs(), - allow_null_lhst::NO, - 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, - assigns_clauset &assigns, + instrument_spec_assignst &instrument_spec_assigns, optionalt &cfg_info_opt) { INVARIANT( @@ -983,15 +996,13 @@ void code_contractst::instrument_call_statement( if(function_call.lhs().is_not_nil()) { // grab the returned pointer from malloc - const auto &object = function_call.lhs(); + 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++; - const auto car = assigns.add_to_write_set(pointer_object(object)); - auto snapshot_instructions = car->generate_snapshot_instructions( - // no check because malloc always returns a null or valid pointer - assigns_clauset::check_target_validityt::NO); - insert_before_swap_and_advance( - body, instruction_it, snapshot_instructions); + 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 @@ -1000,97 +1011,14 @@ void code_contractst::instrument_call_statement( } else if(callee_name == "free") { - source_locationt location_no_checks = instruction_it->source_location(); - disable_pointer_checks(location_no_checks); - const auto free_car = add_inclusion_check( - body, - assigns, - instruction_it, - pointer_object(instruction_it->call_arguments().front()), - // NULL pointers are a allowed and a no-op with free - allow_null_lhst::YES, - cfg_info_opt); - - // skip all invalidation business if we're freeing invalid memory - goto_programt alias_checking_instructions, skip_program; - alias_checking_instructions.add(goto_programt::make_goto( - skip_program.add(goto_programt::make_skip(location_no_checks)), - not_exprt{free_car.validity_condition_var}, - location_no_checks)); - - // Since the argument to free may be an "alias" (but not identical) - // to existing CARs' source_expr, structural equality wouldn't work. - // Moreover, multiple CARs in the writeset might be aliased to the - // same underlying object. - // So, we first find the corresponding CAR using `same_object` checks. - std::unordered_set write_set_validity_addrs; - for(const auto &w_car : assigns.get_write_set()) - { - const auto object_validity_var_addr = - new_tmp_symbol( - pointer_type(bool_typet{}), - location_no_checks, - symbol_table.lookup_ref(function).mode, - symbol_table, - "__car_valid") - .symbol_expr(); - write_set_validity_addrs.insert(object_validity_var_addr); - - alias_checking_instructions.add( - goto_programt::make_decl(object_validity_var_addr, location_no_checks)); - // if the CAR was defined on the same_object as the one being `free`d, - // record its validity variable's address, otherwise record NULL - alias_checking_instructions.add(goto_programt::make_assignment( - object_validity_var_addr, - if_exprt{ - and_exprt{ - w_car.validity_condition_var, - same_object( - free_car.lower_bound_address_var, w_car.lower_bound_address_var)}, - address_of_exprt{w_car.validity_condition_var}, - null_pointer_exprt{to_pointer_type(object_validity_var_addr.type())}}, - location_no_checks)); - } - - alias_checking_instructions.destructive_append(skip_program); - insert_before_swap_and_advance( - body, - instruction_it, - add_pragma_disable_assigns_check(alias_checking_instructions)); - - // move past the call and then insert the invalidation instructions - instruction_it++; - - // skip all invalidation business if we're freeing invalid memory - goto_programt invalidation_instructions; - skip_program.clear(); - invalidation_instructions.add(goto_programt::make_goto( - skip_program.add(goto_programt::make_skip(location_no_checks)), - not_exprt{free_car.validity_condition_var}, - location_no_checks)); - - // invalidate all recorded CAR validity variables - for(const auto &w_car_validity_addr : write_set_validity_addrs) - { - goto_programt w_car_skip_program; - invalidation_instructions.add(goto_programt::make_goto( - w_car_skip_program.add(goto_programt::make_skip(location_no_checks)), - null_pointer(w_car_validity_addr), - location_no_checks)); - invalidation_instructions.add(goto_programt::make_assignment( - dereference_exprt{w_car_validity_addr}, - false_exprt{}, - location_no_checks)); - invalidation_instructions.destructive_append(w_car_skip_program); - } - - invalidation_instructions.destructive_append(skip_program); - insert_before_swap_and_advance( - body, - instruction_it, - add_pragma_disable_assigns_check(invalidation_instructions)); - - instruction_it--; + 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); } } @@ -1173,16 +1101,16 @@ 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 &target = ns.lookup(function); - assigns_clauset assigns( - to_code_with_contract_type(target.type).assigns(), - log, - ns, - function, - symbol_table); + const symbolt &function_sybmol = ns.lookup(function); + const auto &function_with_contract = + to_code_with_contract_type(function_sybmol.type); - // Detect and add static local variables - assigns.add_static_locals_to_write_set(goto_functions, function); + instrument_spec_assignst instrument_spec_assigns( + function, goto_functions, symbol_table, log.get_message_handler()); + + // Detect and track static local variables before inlining + goto_programt snapshot_static_locals; + instrument_spec_assigns.track_static_locals(snapshot_static_locals); // Full inlining of the function body // Inlining is performed so that function calls to a same function @@ -1206,25 +1134,37 @@ bool 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 original goto_function object - // and compute static control flow graph information on it + // 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}; - // Add formal parameters to write set - for(const auto ¶m : to_code_type(target.type).parameters()) - assigns.add_to_write_set(ns.lookup(param.get_identifier()).symbol_expr()); - + // Start instrumentation auto instruction_it = function_body.instructions.begin(); - for(const auto &car : assigns.get_write_set()) + + // Inject local static snapshots + insert_before_swap_and_advance( + function_body, instruction_it, snapshot_static_locals); + + // Track targets mentionned in the specification + for(auto &target : function_with_contract.assigns()) { - auto snapshot_instructions = car.generate_snapshot_instructions( - assigns_clauset::check_target_validityt::YES_ALLOW_NULL); - insert_before_swap_and_advance( - function_body, instruction_it, snapshot_instructions); - }; + goto_programt payload; + instrument_spec_assigns.track_spec_target(target, payload); + insert_before_swap_and_advance(function_body, instruction_it, payload); + } + + // Track formal parameters + goto_programt snapshot_function_parameters; + for(const auto ¶m : to_code_type(function_sybmol.type).parameters()) + { + goto_programt payload; + instrument_spec_assigns.track_stack_allocated( + ns.lookup(param.get_identifier()).symbol_expr(), payload); + insert_before_swap_and_advance(function_body, instruction_it, payload); + } // Restore internal coherence in the programs goto_functions.update(); @@ -1235,7 +1175,7 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) function_body, instruction_it, function_body.instructions.end(), - assigns, + instrument_spec_assigns, // skip checks on function parameter assignments skipt::Skip, cfg_info_opt); @@ -1315,7 +1255,7 @@ void code_contractst::check_frame_conditions( goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, - assigns_clauset &assigns, + instrument_spec_assignst &instrument_spec_assigns, skipt skip_parameter_assigns, optionalt &cfg_info_opt) { @@ -1342,13 +1282,9 @@ void code_contractst::check_frame_conditions( const auto &decl_symbol = instruction_it->decl_symbol(); // move past the call and then insert the CAR instruction_it++; - const auto car = assigns.add_to_write_set(decl_symbol); - // we do not need to check target validity because DECL - // are always backed by adequately sized objects - auto snapshot_instructions = car->generate_snapshot_instructions( - assigns_clauset::check_target_validityt::NO); - insert_before_swap_and_advance( - body, instruction_it, snapshot_instructions); + 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 @@ -1359,35 +1295,24 @@ void code_contractst::check_frame_conditions( must_check_assign( instruction_it, skip_parameter_assigns, ns, cfg_info_opt)) { - instrument_assign_statement(instruction_it, body, assigns, 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, assigns, cfg_info_opt); + 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(); - source_locationt location_no_checks = instruction_it->source_location(); - disable_pointer_checks(location_no_checks); - - // CAR equality and hash are defined on source_expr alone, - // therefore this temporary CAR should be "found" - const auto &symbol_car = assigns.get_write_set().find( - assigns_clauset::conditional_address_ranget{assigns, symbol}); - if(symbol_car != assigns.get_write_set().end()) + if(instrument_spec_assigns.stack_allocated_is_tracked(symbol)) { - auto invalidation_assignment = goto_programt::make_assignment( - symbol_car->validity_condition_var, - false_exprt{}, - instruction_it->source_location()); - body.insert_before_swap( - instruction_it, - add_pragma_disable_assigns_check(invalidation_assignment)); - instruction_it++; + goto_programt payload; + instrument_spec_assigns.invalidate_stack_allocated(symbol, payload); + insert_before_swap_and_advance(body, instruction_it, payload); } else { @@ -1407,15 +1332,13 @@ void code_contractst::check_frame_conditions( instruction_it->is_other() && instruction_it->get_other().get_statement() == ID_havoc_object) { - const auto havoc_argument = - pointer_object(instruction_it->get_other().operands().front()); - add_inclusion_check( - body, - assigns, - instruction_it, - havoc_argument, - allow_null_lhst::NO, - cfg_info_opt); + 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 @@ -1425,53 +1348,6 @@ void code_contractst::check_frame_conditions( } } -const assigns_clauset::conditional_address_ranget -code_contractst::add_inclusion_check( - goto_programt &program, - const assigns_clauset &assigns, - goto_programt::targett &instruction_it, - const exprt &lhs, - allow_null_lhst allow_null_lhs, - optionalt &cfg_info_opt) -{ - const assigns_clauset::conditional_address_ranget car{assigns, lhs}; - - auto check_target_validity = - allow_null_lhs == allow_null_lhst::YES - ? assigns_clauset::check_target_validityt::YES_ALLOW_NULL - : assigns_clauset::check_target_validityt::YES; - - auto snapshot_instructions = - car.generate_snapshot_instructions(check_target_validity); - insert_before_swap_and_advance( - program, instruction_it, snapshot_instructions); - - goto_programt assertion; - source_locationt location_no_checks = - instruction_it->source_location_nonconst(); - disable_pointer_checks(location_no_checks); - - // does this assignment come from some contract replacement ? - const auto &comment = location_no_checks.get_comment(); - if(is_assigns_clause_replacement_tracking_comment(comment)) - { - location_no_checks.set_comment( - "Check that " + id2string(comment) + " is assignable"); - } - else - { - location_no_checks.set_comment( - "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable"); - } - - assertion.add(goto_programt::make_assertion( - assigns.generate_inclusion_check(car, check_target_validity, cfg_info_opt), - location_no_checks)); - insert_before_swap_and_advance(program, instruction_it, assertion); - - return car; -} - 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 67f5c7b7f9b..5760c6392ba 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -31,8 +31,6 @@ Date: February 2016 #include #include -#include "assigns.h" - #define FLAG_LOOP_CONTRACTS "apply-loop-contracts" #define HELP_LOOP_CONTRACTS \ " --apply-loop-contracts\n" \ @@ -49,6 +47,8 @@ Date: February 2016 class local_may_aliast; class replace_symbolt; +class instrument_spec_assignst; +class cfg_infot; class code_contractst { @@ -142,8 +142,7 @@ class code_contractst /// instrumentation (inclusive). /// \param instruction_end Iterator to the instruction at which to stop /// instrumentation (exclusive). - /// \param assigns Assigns clause of the function (its write set attribute - /// gets extended during the instrumentation). + /// \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 @@ -153,27 +152,10 @@ class code_contractst goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, - assigns_clauset &assigns, + instrument_spec_assignst &instrument_spec_assigns, skipt skip_parameter_assigns, optionalt &cfg_info_opt); - /// Allow or do not allow NULL targets in inclusion checks - enum class allow_null_lhst - { - YES, - NO - }; - - /// Inserts an assertion into the goto program to ensure that - /// an expression is within the assignable memory frame. - const assigns_clauset::conditional_address_ranget add_inclusion_check( - goto_programt &program, - const assigns_clauset &assigns, - goto_programt::targett &instruction_it, - const exprt &lhs, - allow_null_lhst allow_null_lhs, - 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); @@ -184,7 +166,7 @@ class code_contractst void instrument_assign_statement( goto_programt::targett &instruction_it, goto_programt &program, - assigns_clauset &assigns_clause, + instrument_spec_assignst &instrument_spec_assigns, optionalt &cfg_info_opt); /// Inserts an assertion into program immediately before the function call at @@ -194,7 +176,7 @@ class code_contractst goto_programt::targett &instruction_it, const irep_idt &function, goto_programt &body, - assigns_clauset &assigns, + instrument_spec_assignst &instrument_spec_assigns, optionalt &cfg_info_opt); /// Apply loop contracts, whenever available, to all loops in `function`. From 63d03bc5a4016233eeff1a17f11b863a6071427a Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 25 Jan 2022 02:50:54 +0000 Subject: [PATCH 7/7] CONTRACS: Update test descriptions following assigns clause refactoring --- .../assigns-enforce-malloc-zero/test.desc | 3 +- .../test.desc | 2 +- .../contracts/assigns_enforce_02/test.desc | 2 + .../contracts/assigns_enforce_03/test.desc | 14 ++++++- .../contracts/assigns_enforce_04/test.desc | 11 +++-- .../contracts/assigns_enforce_15/test.desc | 7 ++-- .../contracts/assigns_enforce_18/test.desc | 20 +++++---- .../contracts/assigns_enforce_19/test.desc | 13 +++--- .../contracts/assigns_enforce_20/test.desc | 4 +- .../contracts/assigns_enforce_21/test.desc | 8 ++-- .../assigns_enforce_arrays_02/test.desc | 12 +++--- .../assigns_enforce_arrays_05/test.desc | 5 ++- .../test.desc | 5 ++- .../test.desc | 14 ++++--- .../test.desc | 14 ++++--- .../test.desc | 14 ++++--- .../test.desc | 17 ++++---- .../test.desc | 28 +++++++------ .../test.desc | 6 +-- .../assigns_enforce_free_dead/test.desc | 27 ++++++------ .../assigns_enforce_havoc_object/test.desc | 5 ++- .../assigns_enforce_malloc_01/test.desc | 2 +- .../assigns_enforce_multi_file_02/test.desc | 3 +- .../assigns_enforce_offsets_2/test.desc | 6 +-- .../assigns_enforce_offsets_4/test.desc | 2 +- .../assigns_enforce_scoping_01/test.desc | 4 +- .../assigns_enforce_scoping_02/test.desc | 4 +- .../assigns_enforce_statics/test.desc | 6 ++- .../assigns_enforce_structs_01/test.desc | 3 +- .../assigns_enforce_structs_02/test.desc | 3 +- .../assigns_enforce_structs_04/test.desc | 6 +-- .../assigns_enforce_structs_05/test.desc | 8 ++-- .../assigns_enforce_structs_06/test.desc | 16 +++---- .../assigns_enforce_structs_07/test.desc | 6 ++- .../assigns_enforce_structs_08/test.desc | 11 ++--- .../test.desc | 4 +- .../assigns_function_pointer/test.desc | 4 +- .../assigns_repeated_ignored/test.desc | 3 +- .../contracts/assigns_replace_04/test.desc | 2 +- .../contracts/assigns_replace_08/test.desc | 2 +- .../contracts/assigns_replace_09/test.desc | 3 +- .../test.desc | 42 +++++++++---------- .../assigns_validity_pointer_02/test.desc | 8 ++-- .../assigns_validity_pointer_04/test.desc | 2 +- .../test.desc | 4 +- .../history-pointer-enforce-09/test.desc | 2 +- .../history-pointer-enforce-10/test.desc | 6 +-- .../contracts/invar_assigns_opt/test.desc | 4 +- .../invar_check_break_fail/test.desc | 2 +- .../invar_check_break_pass/test.desc | 2 +- .../contracts/invar_check_continue/test.desc | 2 +- .../invar_check_multiple_loops/test.desc | 8 ++-- .../invar_check_nested_loops/test.desc | 6 +-- .../invar_check_pointer_modifies-01/test.desc | 4 +- .../invar_check_pointer_modifies-02/test.desc | 4 +- .../invar_check_sufficiency/test.desc | 2 +- .../invar_dynamic_struct_member/test.desc | 6 +-- .../invar_havoc_dynamic_array/test.desc | 4 +- .../test.desc | 4 +- .../test.desc | 4 +- .../invar_havoc_static_array/test.desc | 4 +- .../test.desc | 4 +- .../test.desc | 2 +- .../test.desc | 4 +- .../invar_loop-entry_check/test.desc | 18 ++++---- .../contracts/invar_loop-entry_fail/test.desc | 6 +-- .../invar_loop_constant_fail/test.desc | 4 +- .../invar_loop_constant_no_modify/test.desc | 2 +- .../invar_loop_constant_pass/test.desc | 4 +- .../contracts/invar_struct_member/test.desc | 5 ++- .../invariant_side_effects/test.desc | 2 +- .../contracts/loop_assigns-01/test.desc | 4 +- .../contracts/loop_assigns-02/test.desc | 4 +- .../contracts/loop_assigns-03/test.desc | 6 +-- .../contracts/loop_assigns-04/test.desc | 10 ++--- .../contracts/loop_assigns-05/test.desc | 10 ++--- .../loop_contracts_binary_search/test.desc | 6 +-- .../test.desc | 4 +- .../contracts/quantifiers-loop-01/test.desc | 4 +- .../contracts/quantifiers-loop-02/test.desc | 4 +- .../contracts/quantifiers-loop-03/test.desc | 4 +- .../contracts/test_aliasing_enforce/test.desc | 6 +-- .../contracts/test_aliasing_ensure/test.desc | 6 +-- .../test_aliasing_ensure_indirect/test.desc | 2 +- .../test_array_memory_enforce/test.desc | 6 +-- .../test_scalar_memory_enforce/test.desc | 2 +- .../contracts/test_struct_enforce/test.desc | 4 +- .../test_struct_member_enforce/test.desc | 2 +- .../variant_init_inside_loop/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 8 ++-- .../test.desc | 6 +-- .../test.desc | 6 +-- .../test.desc | 6 +-- .../variant_not_decreasing_fail/test.desc | 2 +- .../variant_weak_invariant_fail/test.desc | 2 +- .../variant_while_true_pass/test.desc | 2 +- 97 files changed, 336 insertions(+), 284 deletions(-) diff --git a/regression/contracts/assigns-enforce-malloc-zero/test.desc b/regression/contracts/assigns-enforce-malloc-zero/test.desc index ef0d72b3c11..eefba72ce5b 100644 --- a/regression/contracts/assigns-enforce-malloc-zero/test.desc +++ b/regression/contracts/assigns-enforce-malloc-zero/test.desc @@ -1,9 +1,10 @@ CORE main.c --enforce-contract foo _ --malloc-may-fail --malloc-fail-null +^\[foo.assigns.\d+\] line 9 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid when a != \(\(char \*\)NULL\): SUCCESS$ +^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ -^\[foo\.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS ^VERIFICATION SUCCESSFUL$ -- This test checks that objects of size zero or __CPROVER_max_malloc_size diff --git a/regression/contracts/assigns-replace-ignored-return-value/test.desc b/regression/contracts/assigns-replace-ignored-return-value/test.desc index c08d1bf63dc..c362aba98fd 100644 --- a/regression/contracts/assigns-replace-ignored-return-value/test.desc +++ b/regression/contracts/assigns-replace-ignored-return-value/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -^[.*] Check that .*ignored_return_value.* is assignable: FAILURE +^\[.*assigns.*\].*ignored_return_value.*FAILURE -- This test checks that when replacing a call by a contract for a call that ignores the return value of the function, the temporary introduced to diff --git a/regression/contracts/assigns_enforce_02/test.desc b/regression/contracts/assigns_enforce_02/test.desc index 14e03da3174..2abca0b8bd1 100644 --- a/regression/contracts/assigns_enforce_02/test.desc +++ b/regression/contracts/assigns_enforce_02/test.desc @@ -1,6 +1,8 @@ CORE main.c --enforce-contract foo +^\[foo.assigns.\d+\] line 3 Check that z is valid: SUCCESS$ +^\[foo.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_03/test.desc b/regression/contracts/assigns_enforce_03/test.desc index 6d528891df0..4b342024cc9 100644 --- a/regression/contracts/assigns_enforce_03/test.desc +++ b/regression/contracts/assigns_enforce_03/test.desc @@ -1,9 +1,21 @@ CORE main.c --enforce-contract f1 --enforce-contract f2 --enforce-contract f3 +^\[f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$ +^\[f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$ +^\[f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$ +^\[f2.assigns.\d+\] line 6 Check that \*x2 is valid: SUCCESS$ +^\[f2.assigns.\d+\] line 6 Check that \*y2 is valid: SUCCESS$ +^\[f2.assigns.\d+\] line 6 Check that \*z2 is valid: SUCCESS$ +^\[f3.assigns.\d+\] line 11 Check that \*x3 is valid: SUCCESS$ +^\[f3.assigns.\d+\] line 11 Check that \*y3 is valid: SUCCESS$ +^\[f3.assigns.\d+\] line 12 Check that \*z3 is valid: SUCCESS$ +^\[f3.assigns.\d+\] line 14 Check that \*x3 is assignable: SUCCESS$ +^\[f3.assigns.\d+\] line 15 Check that \*y3 is assignable: SUCCESS$ +^\[f3.assigns.\d+\] line 16 Check that \*z3 is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ -- -- This test checks that verification succeeds when assigns clauses are respected through multiple function calls. diff --git a/regression/contracts/assigns_enforce_04/test.desc b/regression/contracts/assigns_enforce_04/test.desc index 2e1caa26893..35a898dd382 100644 --- a/regression/contracts/assigns_enforce_04/test.desc +++ b/regression/contracts/assigns_enforce_04/test.desc @@ -1,12 +1,15 @@ CORE main.c --enforce-contract f1 +^\[f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$ +^\[f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$ +^\[f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$ +^\[f3.assigns.\d+\] line 13 Check that \*x3 is assignable: SUCCESS$ +^\[f3.assigns.\d+\] line 14 Check that \*y3 is assignable: SUCCESS$ +^\[f3.assigns.\d+\] line 15 Check that \*z3 is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -^\[f3.\d+\] line \d+ Check that \*x3 is assignable: SUCCESS$ -^\[f3.\d+\] line \d+ Check that \*y3 is assignable: SUCCESS$ -^\[f3.\d+\] line \d+ Check that \*z3 is assignable: SUCCESS$ -^VERIFICATION SUCCESSFUL$ -- -- This test checks that verification only considers assigns clause from enforced function. diff --git a/regression/contracts/assigns_enforce_15/test.desc b/regression/contracts/assigns_enforce_15/test.desc index ae036394aaf..82ce16cb582 100644 --- a/regression/contracts/assigns_enforce_15/test.desc +++ b/regression/contracts/assigns_enforce_15/test.desc @@ -1,11 +1,12 @@ CORE main.c --enforce-contract foo --enforce-contract baz --enforce-contract qux +^\[foo.assigns.\d+\] line \d+ Check that \*x is valid: SUCCESS$ +^\[baz.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$ +^\[qux.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$ +^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -^\[baz.\d+\] line \d+ Check that global is assignable: FAILURE$ -^\[qux.\d+\] line \d+ Check that global is assignable: FAILURE$ -^VERIFICATION FAILED$ -- -- Checks whether verification fails when enforcing a contract diff --git a/regression/contracts/assigns_enforce_18/test.desc b/regression/contracts/assigns_enforce_18/test.desc index 74c8ac7a49b..f1fc63f61ec 100644 --- a/regression/contracts/assigns_enforce_18/test.desc +++ b/regression/contracts/assigns_enforce_18/test.desc @@ -1,16 +1,20 @@ CORE main.c --enforce-contract foo --enforce-contract bar --enforce-contract baz _ --pointer-primitive-check +^\[foo.assigns.\d+\] line 7 Check that \*xp is valid: SUCCESS$ +^\[foo.assigns.\d+\] line 11 Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 14 Check that y is assignable: FAILURE$ +^\[bar.assigns.\d+\] line 17 Check that \*a is valid: SUCCESS$ +^\[bar.assigns.\d+\] line 17 Check that \*b is valid: SUCCESS$ +^\[bar.assigns.\d+\] line 19 Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$ +^\[bar.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$ +^\[baz.assigns.\d+\] line 23 Check that \*a is valid: SUCCESS$ +^\[baz.assigns.\d+\] line 25 Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$ +^\[baz.assigns.\d+\] line 26 Check that \*a is assignable: SUCCESS$ +^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -^\[bar.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$ -^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$ -^\[baz.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$ -^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$ -^VERIFICATION FAILED$ -- -- Checks whether contract enforcement works with functions that deallocate memory. diff --git a/regression/contracts/assigns_enforce_19/test.desc b/regression/contracts/assigns_enforce_19/test.desc index 2f9f2695843..8a2a9086a7e 100644 --- a/regression/contracts/assigns_enforce_19/test.desc +++ b/regression/contracts/assigns_enforce_19/test.desc @@ -1,14 +1,15 @@ CORE main.c --enforce-contract f --enforce-contract g +^\[f.assigns.\d+\] line 9 Check that a is assignable: SUCCESS$ +^\[g.assigns.\d+\] line 14 Check that b is valid: SUCCESS$ +^\[g.assigns.\d+\] line 16 Check that b is assignable: SUCCESS$ +^\[g.assigns.\d+\] line 17 Check that c is assignable: FAILURE$ +^\[g.assigns.\d+\] line 18 Check that \*points_to_b is assignable: SUCCESS$ +^\[g.assigns.\d+\] line 19 Check that \*points_to_c is assignable: FAILURE$ +^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -^\[f.\d+\] line \d+ Check that a is assignable: SUCCESS$ -^\[g.\d+\] line \d+ Check that b is assignable: SUCCESS$ -^\[g.\d+\] line \d+ Check that c is assignable: FAILURE$ -^\[g.\d+\] line \d+ Check that \*points\_to\_b is assignable: SUCCESS$ -^\[g.\d+\] line \d+ Check that \*points\_to\_c is assignable: FAILURE$ -^VERIFICATION FAILED$ -- -- Checks whether contract enforcement works with (local and global) static variables. diff --git a/regression/contracts/assigns_enforce_20/test.desc b/regression/contracts/assigns_enforce_20/test.desc index 1cca96c1c7f..f7d805e7c2a 100644 --- a/regression/contracts/assigns_enforce_20/test.desc +++ b/regression/contracts/assigns_enforce_20/test.desc @@ -3,8 +3,8 @@ main.c --enforce-contract foo ^EXIT=10$ ^SIGNAL=0$ -^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that x is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_21/test.desc b/regression/contracts/assigns_enforce_21/test.desc index a75ef140a6c..f27b7f42c59 100644 --- a/regression/contracts/assigns_enforce_21/test.desc +++ b/regression/contracts/assigns_enforce_21/test.desc @@ -1,12 +1,12 @@ CORE main.c --enforce-contract foo --replace-call-with-contract quz +^\[foo.assigns.\d+\] line \d+ Check that \*y is valid: SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE$ +^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -main.c function bar -^\[bar\.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ -^\[bar\.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE -^VERIFICATION FAILED$ -- -- Checks whether checks write set for sub-function calls. diff --git a/regression/contracts/assigns_enforce_arrays_02/test.desc b/regression/contracts/assigns_enforce_arrays_02/test.desc index abb9e92a686..d4bd5df0a94 100644 --- a/regression/contracts/assigns_enforce_arrays_02/test.desc +++ b/regression/contracts/assigns_enforce_arrays_02/test.desc @@ -1,11 +1,13 @@ CORE main.c --enforce-contract f1 --enforce-contract f2 -^\[f1.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that a\[.*5\] is assignable: FAILURE$ -^\[f2.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$ -^\[f2.\d+\] line \d+ Check that a\[.*5\] is assignable: SUCCESS$ -^\[f2.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line 6 Check that \*a is valid: SUCCESS$ +^\[f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$ +^\[f2.assigns.\d+\] line 12 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid: SUCCESS$ +^\[f2.assigns.\d+\] line 14 Check that a\[.*0\] is assignable: SUCCESS$ +^\[f2.assigns.\d+\] line 15 Check that a\[.*5\] is assignable: SUCCESS$ +^\[f2.assigns.\d+\] line 16 Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/regression/contracts/assigns_enforce_arrays_05/test.desc index 019d4770188..54d643ef138 100644 --- a/regression/contracts/assigns_enforce_arrays_05/test.desc +++ b/regression/contracts/assigns_enforce_arrays_05/test.desc @@ -1,10 +1,11 @@ CORE main.c --enforce-contract uses_assigns +^\[uses_assigns.assigns.\d+\] line \d+ Check that \*\(&a\[\(.*int\)i\]\) is valid: SUCCESS$ +^\[assigns_ptr.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -^\[assigns_ptr\.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ -^VERIFICATION SUCCESSFUL$ -- -- Checks whether verification succeeds for array elements at a symbolic index. diff --git a/regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc b/regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc index daca51d2cfd..2106dd933e3 100644 --- a/regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc +++ b/regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc @@ -2,8 +2,9 @@ CORE main.c --enforce-contract foo ^main.c function foo$ -^\[foo\.\d+\] line 16 Check that \*x is assignable: SUCCESS$ -^\[foo\.\d+\] line 20 Check that \*x is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 10 Check that \*x is valid when .*: SUCCESS$ +^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 20 Check that \*x is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_lvalue/test.desc b/regression/contracts/assigns_enforce_conditional_lvalue/test.desc index 68f9ac72d9b..999be3227c8 100644 --- a/regression/contracts/assigns_enforce_conditional_lvalue/test.desc +++ b/regression/contracts/assigns_enforce_conditional_lvalue/test.desc @@ -2,12 +2,14 @@ CORE main.c --enforce-contract foo main.c function foo -^\[foo\.\d+\] line 7 Check that \*x is assignable: SUCCESS$ -^\[foo\.\d+\] line 8 Check that \*y is assignable: FAILURE$ -^\[foo\.\d+\] line 12 Check that \*x is assignable: FAILURE$ -^\[foo\.\d+\] line 13 Check that \*y is assignable: SUCCESS$ -^\[foo\.\d+\] line 16 Check that \*x is assignable: FAILURE$ -^\[foo\.\d+\] line 17 Check that \*y is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 3 Check that \*x is valid when a != FALSE: SUCCESS$ +^\[foo.assigns.\d+\] line 3 Check that \*y is valid when !\(a != FALSE\): SUCCESS$ +^\[foo.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 13 Check that \*y is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc b/regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc index 4e13aecc929..9e01d79ca12 100644 --- a/regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc +++ b/regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc @@ -2,12 +2,14 @@ CORE main.c --enforce-contract foo main.c function foo -^\[foo\.\d+\] line 7 Check that \*x is assignable: SUCCESS$ -^\[foo\.\d+\] line 8 Check that \*y is assignable: SUCCESS$ -^\[foo\.\d+\] line 12 Check that \*x is assignable: FAILURE$ -^\[foo\.\d+\] line 13 Check that \*y is assignable: FAILURE$ -^\[foo\.\d+\] line 16 Check that \*x is assignable: FAILURE$ -^\[foo\.\d+\] line 17 Check that \*y is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 3 Check that \*x is valid when a != FALSE: SUCCESS$ +^\[foo.assigns.\d+\] line 3 Check that \*y is valid when a != FALSE: SUCCESS$ +^\[foo.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 13 Check that \*y is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc b/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc index cb7a980d68f..c46143c5847 100644 --- a/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc +++ b/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc @@ -2,12 +2,14 @@ CORE main.c --enforce-contract foo main.c function foo -^\[foo\.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo\.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo\.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo\.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo\.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo\.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)x\) is valid when a != FALSE: SUCCESS$ +^\[foo.assigns.\d+\] line 7 Check that POINTER_OBJECT\(\(const void \*\)y\) is valid when !\(a != FALSE\): SUCCESS$ +^\[foo.assigns.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc b/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc index 7bb88a83c08..96fe0be031c 100644 --- a/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc +++ b/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc @@ -2,16 +2,17 @@ CORE main.c --enforce-contract foo main.c function foo -^\[foo\.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo\.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo\.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo\.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo\.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo\.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)x\) is valid when a != FALSE: SUCCESS$ +^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)y\) is valid when a != FALSE: SUCCESS$ +^\[foo.assigns.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -- -- -Check that conditional assigns clause `c ? {__CPROVER_POINTER_OBJECT((p), .. }` -match with control flow path conditions. +Check that conditional target groups match with control flow path conditions. diff --git a/regression/contracts/assigns_enforce_conditional_unions/test.desc b/regression/contracts/assigns_enforce_conditional_unions/test.desc index f9b7044d64e..13bc223c0b6 100644 --- a/regression/contracts/assigns_enforce_conditional_unions/test.desc +++ b/regression/contracts/assigns_enforce_conditional_unions/test.desc @@ -1,18 +1,22 @@ CORE main.c --enforce-contract update _ --pointer-check --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check --conversion-check -^\[is_high_level.\d+\] line 50 Check that latch is assignable: SUCCESS$ -^\[is_high_level.\d+\] line 51 Check that once is assignable: SUCCESS$ -^\[update.\d+\] line 84 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS$ -^\[update.\d+\] line 85 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$ -^\[update.\d+\] line 90 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$ -^\[update.\d+\] line 91 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$ -^\[update.\d+\] line 95 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$ -^\[update.\d+\] line 96 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ -^\[update.\d+\] line 100 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$ -^\[update.\d+\] line 101 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$ -^\[update.\d+\] line 104 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$ -^\[update.\d+\] line 105 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ +^\[update.assigns.\d+] line 73 Check that POINTER_OBJECT\(\(const void \*\)state->digest.high_level.first.ctx->digest\) is valid when .*: SUCCESS +^\[update.assigns.\d+] line 74 Check that state->digest.high_level.first.ctx->flags is valid when .*: SUCCESS +^\[update.assigns.\d+] line 76 Check that POINTER_OBJECT\(\(const void \*\)state->digest.high_level.second.ctx->digest\) is valid when .*: SUCCESS +^\[update.assigns.\d+] line 77 Check that state->digest.high_level.second.ctx->flags is valid when .*: SUCCESS +^\[is_high_level.assigns.\d+\] line 50 Check that latch is assignable: SUCCESS$ +^\[is_high_level.assigns.\d+\] line 51 Check that once is assignable: SUCCESS$ +^\[update.assigns.\d+\] line 84 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS$ +^\[update.assigns.\d+\] line 85 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$ +^\[update.assigns.\d+\] line 90 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$ +^\[update.assigns.\d+\] line 91 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$ +^\[update.assigns.\d+\] line 95 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$ +^\[update.assigns.\d+\] line 96 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ +^\[update.assigns.\d+\] line 100 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$ +^\[update.assigns.\d+\] line 101 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$ +^\[update.assigns.\d+\] line 104 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$ +^\[update.assigns.\d+\] line 105 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_detect_local_statics/test.desc b/regression/contracts/assigns_enforce_detect_local_statics/test.desc index e0309d9fc9d..363b231dc52 100644 --- a/regression/contracts/assigns_enforce_detect_local_statics/test.desc +++ b/regression/contracts/assigns_enforce_detect_local_statics/test.desc @@ -1,9 +1,9 @@ CORE main.c --enforce-contract bar -^\[foo.\d+\] line 14 Check that foo\$\$1\$\$x is assignable: SUCCESS -^\[foo.\d+\] line 17 Check that \*y is assignable: SUCCESS -^\[foo.\d+\] line 20 Check that \*yy is assignable: FAILURE +^\[foo.assigns.\d+\] line 14 Check that foo\$\$1\$\$x is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 20 Check that \*yy is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc index 9c6a1f0066c..6331637168a 100644 --- a/regression/contracts/assigns_enforce_free_dead/test.desc +++ b/regression/contracts/assigns_enforce_free_dead/test.desc @@ -1,22 +1,25 @@ CORE main.c --enforce-contract foo _ --malloc-may-fail --malloc-fail-null --pointer-primitive-check -^\[foo.\d+\] line 7 Check that \*\(\*p\) is assignable: SUCCESS$ -^\[foo.\d+\] line 24 Check that \*\(\*p\) is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that \*p is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*q is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*w is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$ +\[foo.assigns.\d+\] line 4 Check that \*x is valid: SUCCESS$ +\[foo.assigns.\d+\] line 4 Check that \*p is valid when .*: SUCCESS$ +\[foo.assigns.\d+\] line 4 Check that \*\(\*p\) is valid when .*: SUCCESS$ +^\[foo.assigns.\d+\] line 7 Check that \*\(\*p\) is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 24 Check that \*\(\*p\) is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that \*p is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*q is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*w is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- -^\[foo.\d+\] line \d+ Check that \*p is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that \*q is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that \*w is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that \*x is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that \*p is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that \*q is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that \*w is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$ -- Checks that invalidated CARs are correctly tracked on `free` and `DEAD`. diff --git a/regression/contracts/assigns_enforce_havoc_object/test.desc b/regression/contracts/assigns_enforce_havoc_object/test.desc index 80977f7f202..308b22c1da3 100644 --- a/regression/contracts/assigns_enforce_havoc_object/test.desc +++ b/regression/contracts/assigns_enforce_havoc_object/test.desc @@ -3,8 +3,9 @@ main.c --enforce-contract foo ^EXIT=10$ ^SIGNAL=0$ -^\[bar.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: SUCCESS$ -^\[bar.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(const void \*\)a1->u.b->c\) is valid: SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_malloc_01/test.desc b/regression/contracts/assigns_enforce_malloc_01/test.desc index 0ee889a7b2b..ae3a0536bf1 100644 --- a/regression/contracts/assigns_enforce_malloc_01/test.desc +++ b/regression/contracts/assigns_enforce_malloc_01/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract f ^EXIT=0$ ^SIGNAL=0$ -^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS +^\[f\.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/assigns_enforce_multi_file_02/test.desc b/regression/contracts/assigns_enforce_multi_file_02/test.desc index dd02559f652..c9f45d47c58 100644 --- a/regression/contracts/assigns_enforce_multi_file_02/test.desc +++ b/regression/contracts/assigns_enforce_multi_file_02/test.desc @@ -3,7 +3,8 @@ main.c --enforce-contract f1 ^EXIT=0$ ^SIGNAL=0$ -^\[f1\.\d+\] line \d+ Check that b->y is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that \*a is valid: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that b->y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/assigns_enforce_offsets_2/test.desc b/regression/contracts/assigns_enforce_offsets_2/test.desc index 9edeb40efd6..dbf3b1e0810 100644 --- a/regression/contracts/assigns_enforce_offsets_2/test.desc +++ b/regression/contracts/assigns_enforce_offsets_2/test.desc @@ -1,9 +1,9 @@ CORE main.c --enforce-contract foo _ --pointer-check -^\[.*\d+\].* line 5 Check assigns target validity 'TRUE: \*x': SUCCESS$ -^\[.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: (SUCCESS|FAILURE)$ -^\[.*\d+\].* line 8 Check assigns target validity 'TRUE: x\[\(.*\)1\]': FAILURE$ +^\[foo.assigns.*\d+\].* line 5 Check that \*x is valid: SUCCESS$ +^\[foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: (SUCCESS|FAILURE)$ +^\[foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_offsets_4/test.desc b/regression/contracts/assigns_enforce_offsets_4/test.desc index c7795c03c7c..a9144122d51 100644 --- a/regression/contracts/assigns_enforce_offsets_4/test.desc +++ b/regression/contracts/assigns_enforce_offsets_4/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo _ --pointer-check -^\[.*\d+\].* line 8 Check assigns target validity 'TRUE: x\[\(.*\)10\]': FAILURE$ +^\[foo.assigns.*\d+\].* line 5 Check that x\[\(.*\)10\] is valid: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_scoping_01/test.desc b/regression/contracts/assigns_enforce_scoping_01/test.desc index 8262484576f..d95afefade3 100644 --- a/regression/contracts/assigns_enforce_scoping_01/test.desc +++ b/regression/contracts/assigns_enforce_scoping_01/test.desc @@ -3,8 +3,8 @@ main.c --enforce-contract f1 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that \*b is assignable: FAILURE$ +^\[f1.assigns.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that \*b is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_scoping_02/test.desc b/regression/contracts/assigns_enforce_scoping_02/test.desc index 791cbf3c6c3..a5d07aa04d5 100644 --- a/regression/contracts/assigns_enforce_scoping_02/test.desc +++ b/regression/contracts/assigns_enforce_scoping_02/test.desc @@ -3,8 +3,8 @@ main.c --enforce-contract f1 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that \*b is assignable: FAILURE$ +^\[f1.assigns.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that \*b is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_statics/test.desc b/regression/contracts/assigns_enforce_statics/test.desc index fee67eaefaa..87f417d025f 100644 --- a/regression/contracts/assigns_enforce_statics/test.desc +++ b/regression/contracts/assigns_enforce_statics/test.desc @@ -3,10 +3,12 @@ main.c --enforce-contract foo _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that x is valid: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- +^\[.*assigns.*\].*: FAILURE$ -- Checks whether static local and global variables are correctly tracked in assigns clause verification. diff --git a/regression/contracts/assigns_enforce_structs_01/test.desc b/regression/contracts/assigns_enforce_structs_01/test.desc index 0d77a423c99..a2e87391c9c 100644 --- a/regression/contracts/assigns_enforce_structs_01/test.desc +++ b/regression/contracts/assigns_enforce_structs_01/test.desc @@ -3,9 +3,10 @@ main.c --enforce-contract f ^EXIT=0$ ^SIGNAL=0$ -^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ +^\[f.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- +^\[.*assigns.*\].*: FAILURE$ -- Checks whether verification succeeds when a pointer deref that is not specified in the assigns clause is first pointed at a member of a diff --git a/regression/contracts/assigns_enforce_structs_02/test.desc b/regression/contracts/assigns_enforce_structs_02/test.desc index fc0948b1676..2efece83723 100644 --- a/regression/contracts/assigns_enforce_structs_02/test.desc +++ b/regression/contracts/assigns_enforce_structs_02/test.desc @@ -3,9 +3,10 @@ main.c --enforce-contract f ^EXIT=0$ ^SIGNAL=0$ -^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ +^\[f.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- +^\[.*assigns.*\].*: FAILURE$ -- Checks whether verification succeeds when a pointer deref that is not specified in the assigns clause is first pointed at a member of a locally diff --git a/regression/contracts/assigns_enforce_structs_04/test.desc b/regression/contracts/assigns_enforce_structs_04/test.desc index 3de0bffb9ca..003a6fd2f4a 100644 --- a/regression/contracts/assigns_enforce_structs_04/test.desc +++ b/regression/contracts/assigns_enforce_structs_04/test.desc @@ -3,9 +3,9 @@ main.c --enforce-contract f1 --enforce-contract f2 --enforce-contract f3 --enforce-contract f4 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$ -^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$ -^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->y is assignable: FAILURE$ +^\[f2.assigns.\d+\] line \d+ Check that p->x is assignable: FAILURE$ +^\[f3.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_05/test.desc b/regression/contracts/assigns_enforce_structs_05/test.desc index 664fd950149..0220675ec2a 100644 --- a/regression/contracts/assigns_enforce_structs_05/test.desc +++ b/regression/contracts/assigns_enforce_structs_05/test.desc @@ -3,10 +3,10 @@ main.c --enforce-contract f1 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$ -^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)0\] is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)1\] is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)2\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->y is assignable: FAILURE$ +^\[f1.assigns.\d+\] line \d+ Check that p->x\[\(.*\)0\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->x\[\(.*\)1\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->x\[\(.*\)2\] is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_06/test.desc b/regression/contracts/assigns_enforce_structs_06/test.desc index 60310ca0380..2a56bf89725 100644 --- a/regression/contracts/assigns_enforce_structs_06/test.desc +++ b/regression/contracts/assigns_enforce_structs_06/test.desc @@ -3,14 +3,14 @@ main.c --enforce-contract f1 --enforce-contract f2 --enforce-contract f3 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)1\] is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)2\] is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that p->size is assignable: FAILURE$ -^\[f2.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ -^\[f2.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ -^\[f3.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$ -^\[f3.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)1\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)2\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->size is assignable: FAILURE$ +^\[f2.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f2.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ +^\[f3.assigns.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$ +^\[f3.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_07/test.desc b/regression/contracts/assigns_enforce_structs_07/test.desc index 7a0d41839e0..c7337935f6b 100644 --- a/regression/contracts/assigns_enforce_structs_07/test.desc +++ b/regression/contracts/assigns_enforce_structs_07/test.desc @@ -3,8 +3,10 @@ main.c --enforce-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check ^EXIT=10$ ^SIGNAL=0$ -^\[f1.*\d+\].*line 18 Check assigns target validity 'TRUE: p->buf\[\(.*\)0\]': FAILURE$ -^\[f2.*\d+\].*line 23 Check assigns target validity 'TRUE: pp->p->buf\[\(.*\)0\]': FAILURE$ +^\[f1.assigns.\d+\].*line 16 Check that \*p->buf is valid: FAILURE$ +^\[f1.assigns.\d+\].*line 18 Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f2.assigns.\d+\].*line 21 Check that \*pp->p->buf is valid: FAILURE$ +^\[f2.assigns.\d+\].*line 23 Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_08/test.desc b/regression/contracts/assigns_enforce_structs_08/test.desc index 0272e14736a..054a165460b 100644 --- a/regression/contracts/assigns_enforce_structs_08/test.desc +++ b/regression/contracts/assigns_enforce_structs_08/test.desc @@ -1,19 +1,16 @@ CORE main.c --enforce-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check -^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ -^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[f2.assigns.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -- -^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in p->buf: FAILURE$ -^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in p->buf\[\(.*\)0\]: FAILURE$ -^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in pp->p->buf\[\(.*\)0\]: FAILURE$ -^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in pp->p->buf\[\(.*\)0\]: FAILURE$ +^\[.*assigns.*\].*: FAILURE$ -- In f1, the assigns clause specifies `*(p->buf)` as target (which can be invalid) -and assigns `p->buf[0]` unconditionally. When both target and lhs are invalid, +and assigns `p->buf[0]` unconditionally. When both target and lhs are invalid, its inclusion check can be trivially satisfied or not but we expect in all cases a null pointer failure and an invalid pointer error to occur on the assignment. diff --git a/regression/contracts/assigns_enforce_subfunction_calls/test.desc b/regression/contracts/assigns_enforce_subfunction_calls/test.desc index f1668d7397c..ed4c35002f3 100644 --- a/regression/contracts/assigns_enforce_subfunction_calls/test.desc +++ b/regression/contracts/assigns_enforce_subfunction_calls/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^main.c function baz$ -^\[baz.\d+\] line 6 Check that \*x is assignable: SUCCESS$ -^\[baz.\d+\] line 6 Check that \*x is assignable: FAILURE$ +^\[baz.assigns.\d+\] line 6 Check that \*x is assignable: SUCCESS$ +^\[baz.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$ ^main.c function foo$ ^\[foo.assertion.\d+\] line 20 foo.x.set: SUCCESS$ ^\[foo.assertion.\d+\] line 25 foo.local.set: SUCCESS$ diff --git a/regression/contracts/assigns_function_pointer/test.desc b/regression/contracts/assigns_function_pointer/test.desc index f5d4a7d36b8..8d88ab790f5 100644 --- a/regression/contracts/assigns_function_pointer/test.desc +++ b/regression/contracts/assigns_function_pointer/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$ -^\[bar\.\d+\] line \d+ Check that s->f is assignable: SUCCESS$ -^\[bar\.\d+\] line \d+ Check that \*f is assignable: SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that s->f is assignable: SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that \*f is assignable: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion x \=\= 1: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion x \=\= 2: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/assigns_repeated_ignored/test.desc b/regression/contracts/assigns_repeated_ignored/test.desc index 419432073d4..7e8ecdffd98 100644 --- a/regression/contracts/assigns_repeated_ignored/test.desc +++ b/regression/contracts/assigns_repeated_ignored/test.desc @@ -1,11 +1,12 @@ CORE main.c --enforce-contract foo -^Ignored duplicate expression '\*x' in assigns clause at file main\.c line \d+$ +^Ignored duplicate expression '\*x' in assigns clause spec at file main.c line \d+$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +^\[.*assigns.*].*: FAILURE$ -- This test checks that repeated expressions in assigns clauses are correctly detected and ignored. diff --git a/regression/contracts/assigns_replace_04/test.desc b/regression/contracts/assigns_replace_04/test.desc index b284bf324ef..99b62a36707 100644 --- a/regression/contracts/assigns_replace_04/test.desc +++ b/regression/contracts/assigns_replace_04/test.desc @@ -5,7 +5,7 @@ main.c function main ^\[.*\d+\] line 29 assertion p > 100: SUCCESS$ ^\[.*\d+\] line 30 assertion q == 2: SUCCESS$ ^\[.*\d+\] line 31 reachability test: FAILURE$ -^\*\* 1 of 3 failed +^\*\* 1 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_replace_08/test.desc b/regression/contracts/assigns_replace_08/test.desc index 16b3fc738fa..d5899cf297d 100644 --- a/regression/contracts/assigns_replace_08/test.desc +++ b/regression/contracts/assigns_replace_08/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check ^EXIT=10$ ^SIGNAL=0$ -\[foo.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: FAILURE$ +\[foo.assigns.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: FAILURE$ ^.* 1 of \d+ failed \(\d+ iteration.*\)$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/assigns_replace_09/test.desc b/regression/contracts/assigns_replace_09/test.desc index 4d16659c1c8..f918151a1b8 100644 --- a/regression/contracts/assigns_replace_09/test.desc +++ b/regression/contracts/assigns_replace_09/test.desc @@ -3,7 +3,8 @@ main.c --replace-call-with-contract bar --enforce-contract foo ^EXIT=0$ ^SIGNAL=0$ -\[foo.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*z is valid: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^Condition: \!not\_found$ diff --git a/regression/contracts/assigns_type_checking_valid_cases/test.desc b/regression/contracts/assigns_type_checking_valid_cases/test.desc index 1592a4973c2..2e6ca5c2349 100644 --- a/regression/contracts/assigns_type_checking_valid_cases/test.desc +++ b/regression/contracts/assigns_type_checking_valid_cases/test.desc @@ -3,27 +3,27 @@ main.c --enforce-contract foo1 --enforce-contract foo2 --enforce-contract foo3 --enforce-contract foo4 --enforce-contract foo5 --enforce-contract foo6 --enforce-contract foo7 --enforce-contract foo8 --enforce-contract foo9 --enforce-contract foo10 _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo10.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ -^\[foo10.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$ -^\[foo3.\d+\] line \d+ Check that y is assignable: SUCCESS$ -^\[foo4.\d+\] line \d+ Check that \*c is assignable: SUCCESS$ -^\[foo4.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ -^\[foo5.\d+\] line \d+ Check that buffer.data is assignable: SUCCESS$ -^\[foo5.\d+\] line \d+ Check that buffer.len is assignable: SUCCESS$ -^\[foo6.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ -^\[foo6.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ -^\[foo7.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ -^\[foo7.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ -^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$ -^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$ -^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$ -^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)3\] is assignable: SUCCESS$ -^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)4\] is assignable: SUCCESS$ -^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)5\] is assignable: SUCCESS$ -^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)6\] is assignable: SUCCESS$ -^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$ -^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$ -^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$ +^\[foo10.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ +^\[foo10.assigns.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$ +^\[foo3.assigns.\d+\] line \d+ Check that y is assignable: SUCCESS$ +^\[foo4.assigns.\d+\] line \d+ Check that \*c is assignable: SUCCESS$ +^\[foo4.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[foo5.assigns.\d+\] line \d+ Check that buffer.data is assignable: SUCCESS$ +^\[foo5.assigns.\d+\] line \d+ Check that buffer.len is assignable: SUCCESS$ +^\[foo6.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ +^\[foo6.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ +^\[foo7.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ +^\[foo7.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)3\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)4\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)5\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)6\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts/assigns_validity_pointer_02/test.desc b/regression/contracts/assigns_validity_pointer_02/test.desc index 4035fc12118..848aeb0958f 100644 --- a/regression/contracts/assigns_validity_pointer_02/test.desc +++ b/regression/contracts/assigns_validity_pointer_02/test.desc @@ -4,10 +4,10 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ -^\[bar.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ -^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ -^\[baz.\d+\] line \d+ Check that \*z is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[baz.assigns.\d+\] line \d+ Check that \*z is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$ diff --git a/regression/contracts/assigns_validity_pointer_04/test.desc b/regression/contracts/assigns_validity_pointer_04/test.desc index 0d3a03e4367..b3fe4dbb3b1 100644 --- a/regression/contracts/assigns_validity_pointer_04/test.desc +++ b/regression/contracts/assigns_validity_pointer_04/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-primitive-check ^EXIT=10$ ^SIGNAL=0$ -^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that z is assignable: FAILURE$ ^.* 1 of \d+ failed \(\d+ iteration.*\)$ ^VERIFICATION FAILED$ // bar diff --git a/regression/contracts/contracts_with_function_pointers/test.desc b/regression/contracts/contracts_with_function_pointers/test.desc index a955e31cd09..480b8532f47 100644 --- a/regression/contracts/contracts_with_function_pointers/test.desc +++ b/regression/contracts/contracts_with_function_pointers/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ -^\[bar.\d+\] line \d+ Check that \*return\_value\_baz is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that \*return\_value\_baz is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC properly instrument functions with function pointers diff --git a/regression/contracts/history-pointer-enforce-09/test.desc b/regression/contracts/history-pointer-enforce-09/test.desc index 0da48356559..226c63e735e 100644 --- a/regression/contracts/history-pointer-enforce-09/test.desc +++ b/regression/contracts/history-pointer-enforce-09/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ -^\[foo.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/history-pointer-enforce-10/test.desc b/regression/contracts/history-pointer-enforce-10/test.desc index e8359a34c9e..afbbf3e463c 100644 --- a/regression/contracts/history-pointer-enforce-10/test.desc +++ b/regression/contracts/history-pointer-enforce-10/test.desc @@ -6,9 +6,9 @@ main.c ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ -^\[bar.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == 7: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == -1: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/invar_assigns_opt/test.desc b/regression/contracts/invar_assigns_opt/test.desc index da69d71761f..16e5e040543 100644 --- a/regression/contracts/invar_assigns_opt/test.desc +++ b/regression/contracts/invar_assigns_opt/test.desc @@ -8,8 +8,8 @@ main.c ^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$ ^\[main.assertion.\d+\] .* assertion r1 == 0: SUCCESS$ ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ -^\[main.\d+\] .* Check that s2 is assignable: SUCCESS$ -^\[main.\d+\] .* Check that r2 is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that s2 is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r2 is assignable: SUCCESS$ ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$ ^\[main.assertion.\d+\] .* assertion r2 == 0: SUCCESS$ diff --git a/regression/contracts/invar_check_break_fail/test.desc b/regression/contracts/invar_check_break_fail/test.desc index b473182ddc8..43ace0d05ad 100644 --- a/regression/contracts/invar_check_break_fail/test.desc +++ b/regression/contracts/invar_check_break_fail/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion r == 0: FAILURE$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/invar_check_break_pass/test.desc b/regression/contracts/invar_check_break_pass/test.desc index afdd776fe65..c31ecb10767 100644 --- a/regression/contracts/invar_check_break_pass/test.desc +++ b/regression/contracts/invar_check_break_pass/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion r == 0 || r == 1: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/invar_check_continue/test.desc b/regression/contracts/invar_check_continue/test.desc index a3b77498072..baa936a14f3 100644 --- a/regression/contracts/invar_check_continue/test.desc +++ b/regression/contracts/invar_check_continue/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/invar_check_multiple_loops/test.desc b/regression/contracts/invar_check_multiple_loops/test.desc index 625c7889df7..86b4399b890 100644 --- a/regression/contracts/invar_check_multiple_loops/test.desc +++ b/regression/contracts/invar_check_multiple_loops/test.desc @@ -10,10 +10,10 @@ main.c ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion x == y \+ 2 \* n: SUCCESS$ -^\[main\.\d+\] line 8 Check that r is assignable: SUCCESS$ -^\[main\.\d+\] line 15 Check that x is assignable: SUCCESS$ -^\[main\.\d+\] line 23 Check that y is assignable: SUCCESS$ -^\[main\.\d+\] line 24 Check that r is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 8 Check that r is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 15 Check that x is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 23 Check that y is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 24 Check that r is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- This test checks that multiple loops and `for` loops are correctly handled. diff --git a/regression/contracts/invar_check_nested_loops/test.desc b/regression/contracts/invar_check_nested_loops/test.desc index 93b26c1ce39..47c33e05abe 100644 --- a/regression/contracts/invar_check_nested_loops/test.desc +++ b/regression/contracts/invar_check_nested_loops/test.desc @@ -9,9 +9,9 @@ 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\.\d+] line 23 Check that s is assignable: SUCCESS$ -^\[main\.\d+] line 24 Check that a is assignable: SUCCESS$ -^\[main\.\d+] line 27 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/invar_check_pointer_modifies-01/test.desc b/regression/contracts/invar_check_pointer_modifies-01/test.desc index 3a97638f638..deb947163f4 100644 --- a/regression/contracts/invar_check_pointer_modifies-01/test.desc +++ b/regression/contracts/invar_check_pointer_modifies-01/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+] .* Check that \*data is assignable: SUCCESS$ -^\[main\.\d+] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+] .* Check that \*data is assignable: SUCCESS$ +^\[main.assigns.\d+] .* Check that i is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion \*data = 42: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/invar_check_pointer_modifies-02/test.desc b/regression/contracts/invar_check_pointer_modifies-02/test.desc index 6dee673c6f9..95a9eb36ea7 100644 --- a/regression/contracts/invar_check_pointer_modifies-02/test.desc +++ b/regression/contracts/invar_check_pointer_modifies-02/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that \*data is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*data is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data == copy: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion \*copy = 42: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/invar_check_sufficiency/test.desc b/regression/contracts/invar_check_sufficiency/test.desc index 3381482ec83..ef73ea2fc76 100644 --- a/regression/contracts/invar_check_sufficiency/test.desc +++ b/regression/contracts/invar_check_sufficiency/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ ^\[main\.assertion\.1\] .* assertion r == 0: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/invar_dynamic_struct_member/test.desc b/regression/contracts/invar_dynamic_struct_member/test.desc index 763072ccff7..d6653a12b0c 100644 --- a/regression/contracts/invar_dynamic_struct_member/test.desc +++ b/regression/contracts/invar_dynamic_struct_member/test.desc @@ -5,9 +5,9 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main\.\d+\] line 22 Check that t->x is assignable: SUCCESS$ -^\[main\.\d+\] line 25 Check that t->x is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 22 Check that t->x is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 25 Check that t->x is assignable: SUCCESS$ ^\[main.assertion.1\] .* assertion .*: FAILURE$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/invar_havoc_dynamic_array/test.desc b/regression/contracts/invar_havoc_dynamic_array/test.desc index 0676aa4b6da..11bf3202c59 100644 --- a/regression/contracts/invar_havoc_dynamic_array/test.desc +++ b/regression/contracts/invar_havoc_dynamic_array/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc index 27ca897e8bb..6bf09ab0360 100644 --- a/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc +++ b/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc index 441b05eea40..ff6b7e8e980 100644 --- a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc +++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ -^\[main.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.\d+\] .* Check that data\[(.*)4\]\[(.*)5\]\[(.*)6\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(.*)4\]\[(.*)5\]\[(.*)6\] is assignable: SUCCESS$ ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assertion.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ ^\[main.assertion.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$ diff --git a/regression/contracts/invar_havoc_static_array/test.desc b/regression/contracts/invar_havoc_static_array/test.desc index efc72383f7d..ced29fb215b 100644 --- a/regression/contracts/invar_havoc_static_array/test.desc +++ b/regression/contracts/invar_havoc_static_array/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_havoc_static_array_const_idx/test.desc b/regression/contracts/invar_havoc_static_array_const_idx/test.desc index 3ca63dfe501..45adf3e6982 100644 --- a/regression/contracts/invar_havoc_static_array_const_idx/test.desc +++ b/regression/contracts/invar_havoc_static_array_const_idx/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc index 052762e9b2f..052fe5af389 100644 --- a/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc +++ b/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)5\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)5\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc index 910c438d54f..6ec32feb580 100644 --- a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc +++ b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)i\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)i\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_loop-entry_check/test.desc b/regression/contracts/invar_loop-entry_check/test.desc index 37f389403dd..554a504ef23 100644 --- a/regression/contracts/invar_loop-entry_check/test.desc +++ b/regression/contracts/invar_loop-entry_check/test.desc @@ -11,15 +11,15 @@ main.c ^\[main\.assertion\.\d+\] .* assertion x2 == z2: SUCCESS$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that y1 is assignable: SUCCESS$ -^\[main\.\d+\] line 18 Check that \*x1 is assignable: SUCCESS$ -^\[main\.\d+\] line 19 Check that \*x1 is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that y2 is assignable: SUCCESS$ -^\[main\.\d+\] line 30 Check that x2 is assignable: SUCCESS$ -^\[main\.\d+\] line 31 Check that x2 is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that y3 is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that s0\.n is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that s2->n is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that y1 is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 18 Check that \*x1 is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 19 Check that \*x1 is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that y2 is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 30 Check that x2 is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 31 Check that x2 is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that y3 is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that s0\.n is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that s2->n is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion \*\(s1\.n\) == \*\(s2->n\): SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/invar_loop-entry_fail/test.desc b/regression/contracts/invar_loop-entry_fail/test.desc index c5a1d71b0b4..fb736fa7817 100644 --- a/regression/contracts/invar_loop-entry_fail/test.desc +++ b/regression/contracts/invar_loop-entry_fail/test.desc @@ -5,9 +5,9 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: FAILURE$ -^\[main\.\d+\] line 11 Check that y is assignable: SUCCESS$ -^\[main\.\d+\] line 12 Check that x is assignable: SUCCESS$ -^\[main\.\d+\] line 13 Check that x is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 11 Check that y is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 12 Check that x is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 13 Check that x is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/invar_loop_constant_fail/test.desc b/regression/contracts/invar_loop_constant_fail/test.desc index 5ffac813b1d..261e2c27726 100644 --- a/regression/contracts/invar_loop_constant_fail/test.desc +++ b/regression/contracts/invar_loop_constant_fail/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that s is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that s is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion s == 1: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_loop_constant_no_modify/test.desc b/regression/contracts/invar_loop_constant_no_modify/test.desc index 2cd7e168998..ccb12ed94d2 100644 --- a/regression/contracts/invar_loop_constant_no_modify/test.desc +++ b/regression/contracts/invar_loop_constant_no_modify/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion s == 1: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/invar_loop_constant_pass/test.desc b/regression/contracts/invar_loop_constant_pass/test.desc index 56cefb66d88..a33b725b669 100644 --- a/regression/contracts/invar_loop_constant_pass/test.desc +++ b/regression/contracts/invar_loop_constant_pass/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that s is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that s is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion s == 1: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/invar_struct_member/test.desc b/regression/contracts/invar_struct_member/test.desc index 1c93bf225d8..111e8f9c944 100644 --- a/regression/contracts/invar_struct_member/test.desc +++ b/regression/contracts/invar_struct_member/test.desc @@ -5,7 +5,10 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that t\.x is assignable: SUCCESS$ +^\[main.assigns.\d+\].* Check that i is valid: SUCCESS$ +^\[main.assigns.\d+\].* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\].* Check that t\.x is valid: SUCCESS$ +^\[main.assigns.\d+\].* Check that t\.x is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion t.x == 0 || t.x == 2: FAILURE$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/invariant_side_effects/test.desc b/regression/contracts/invariant_side_effects/test.desc index dcc839d15e2..8268af383e0 100644 --- a/regression/contracts/invariant_side_effects/test.desc +++ b/regression/contracts/invariant_side_effects/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that \*a is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*a is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion \*a == N: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/loop_assigns-01/test.desc b/regression/contracts/loop_assigns-01/test.desc index 8e242fd5b3d..dfdb76bc45b 100644 --- a/regression/contracts/loop_assigns-01/test.desc +++ b/regression/contracts/loop_assigns-01/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ -^\[main.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/loop_assigns-02/test.desc b/regression/contracts/loop_assigns-02/test.desc index e1ecdc4b04b..205356864ef 100644 --- a/regression/contracts/loop_assigns-02/test.desc +++ b/regression/contracts/loop_assigns-02/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ -^\[main.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$ ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/loop_assigns-03/test.desc b/regression/contracts/loop_assigns-03/test.desc index 632e889b1b4..15963cb9c00 100644 --- a/regression/contracts/loop_assigns-03/test.desc +++ b/regression/contracts/loop_assigns-03/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ -^\[main.\d+\] .* Check that i is assignable: FAILURE$ -^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: FAILURE$ +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- @@ -14,4 +14,4 @@ The alias analysis in this case returns `unknown`, and so we must manually annotate an assigns clause on the loop. Note that the annotated assigns clause in this case is an underapproximation, -because `i` is also assigned in the loop and should be marked as assignable. +because `i`assigns. is also assigned in the loop and should be marked as assignable. diff --git a/regression/contracts/loop_assigns-04/test.desc b/regression/contracts/loop_assigns-04/test.desc index fef5d6e0572..75c60d625bd 100644 --- a/regression/contracts/loop_assigns-04/test.desc +++ b/regression/contracts/loop_assigns-04/test.desc @@ -3,10 +3,10 @@ main.c --apply-loop-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.\d+\] .* Check that j is assignable: SUCCESS$ -^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ -^\[main.\d+\] .* Check that y is assignable: FAILURE$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that y is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- @@ -15,4 +15,4 @@ The alias analysis in this case returns `unknown`, and so we must manually annotate an assigns clause on the loop. Note that the annotated assigns clause in this case is an underapproximation, -because `i` is also assigned in the loop and should be marked as assignable. +because `i`assigns. is also assigned in the loop and should be marked as assignable. diff --git a/regression/contracts/loop_assigns-05/test.desc b/regression/contracts/loop_assigns-05/test.desc index 78091d38b81..57bf54b90a8 100644 --- a/regression/contracts/loop_assigns-05/test.desc +++ b/regression/contracts/loop_assigns-05/test.desc @@ -3,11 +3,11 @@ main.c --apply-loop-contracts ^EXIT=0$ ^SIGNAL=0$ -^\[body_1.\d+\] .* Check that j is assignable: SUCCESS$ -^\[body_2.\d+\] .* Check that \*i is assignable: SUCCESS$ -^\[body_3.\d+\] .* Check that \*i is assignable: SUCCESS$ -^\[incr.\d+\] .* Check that \*i is assignable: SUCCESS$ -^\[main.\d+\] .* Check that i is assignable: SUCCESS$ +^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$ +^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$ diff --git a/regression/contracts/loop_contracts_binary_search/test.desc b/regression/contracts/loop_contracts_binary_search/test.desc index f727ec04174..e2104872550 100644 --- a/regression/contracts/loop_contracts_binary_search/test.desc +++ b/regression/contracts/loop_contracts_binary_search/test.desc @@ -6,9 +6,9 @@ main.c ^\[binary_search\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[binary_search\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[binary_search\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$ -^\[binary_search\.\d+\] .* Check that lb is assignable: SUCCESS$ -^\[binary_search\.\d+\] .* Check that ub is assignable: SUCCESS$ -^\[binary_search\.\d+\] .* Check that mid is assignable: SUCCESS$ +^\[binary_search.assigns.\d+\] .* Check that lb is assignable: SUCCESS$ +^\[binary_search.assigns.\d+\] .* Check that ub is assignable: SUCCESS$ +^\[binary_search.assigns.\d+\] .* Check that mid is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion buf\[idx\] == val: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc index b5a17935c58..43d5442d71d 100644 --- a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc +++ b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc @@ -4,11 +4,11 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ -^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring -^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: FAILURE$ +^\[f1.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: FAILURE$ -- The purpose of this test is to ensure that we can safely use __CPROVER_forall within positive contexts (enforced ENSURES clauses). diff --git a/regression/contracts/quantifiers-loop-01/test.desc b/regression/contracts/quantifiers-loop-01/test.desc index 36add00c985..2b61263b997 100644 --- a/regression/contracts/quantifiers-loop-01/test.desc +++ b/regression/contracts/quantifiers-loop-01/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] line .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] line .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] line .* Check that i is assignable: SUCCESS$ -^\[main\.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] line .* assertion a\[10\] == 1: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/quantifiers-loop-02/test.desc b/regression/contracts/quantifiers-loop-02/test.desc index c84fbd9fe58..6d2b3c39772 100644 --- a/regression/contracts/quantifiers-loop-02/test.desc +++ b/regression/contracts/quantifiers-loop-02/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS$ ^\[main.\d+\] line .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] line .* Check that i is assignable: SUCCESS$ -^\[main\.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ ^\[main.assertion.\d+\] line .* assertion .*: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/quantifiers-loop-03/test.desc b/regression/contracts/quantifiers-loop-03/test.desc index 8acc26e8542..faeedaec836 100644 --- a/regression/contracts/quantifiers-loop-03/test.desc +++ b/regression/contracts/quantifiers-loop-03/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main\.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main\.\d+\] .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] line .* assertion .*: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/test_aliasing_enforce/test.desc b/regression/contracts/test_aliasing_enforce/test.desc index f06c2f48655..93495129f1b 100644 --- a/regression/contracts/test_aliasing_enforce/test.desc +++ b/regression/contracts/test_aliasing_enforce/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS -\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS -\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS -\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/test_aliasing_ensure/test.desc b/regression/contracts/test_aliasing_ensure/test.desc index 61ee5c97f78..c7fcc2e0264 100644 --- a/regression/contracts/test_aliasing_ensure/test.desc +++ b/regression/contracts/test_aliasing_ensure/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS -\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS -\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS -\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/test_aliasing_ensure_indirect/test.desc b/regression/contracts/test_aliasing_ensure_indirect/test.desc index 4c9575dddb9..95b62b742fe 100644 --- a/regression/contracts/test_aliasing_ensure_indirect/test.desc +++ b/regression/contracts/test_aliasing_ensure_indirect/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS -\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/test_array_memory_enforce/test.desc b/regression/contracts/test_array_memory_enforce/test.desc index e338aa07342..169bc8f4b86 100644 --- a/regression/contracts/test_array_memory_enforce/test.desc +++ b/regression/contracts/test_array_memory_enforce/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS -\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS -\[foo.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS -\[foo.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/test_scalar_memory_enforce/test.desc b/regression/contracts/test_scalar_memory_enforce/test.desc index 41d80653ccb..3a8aa7f3a99 100644 --- a/regression/contracts/test_scalar_memory_enforce/test.desc +++ b/regression/contracts/test_scalar_memory_enforce/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS -\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/test_struct_enforce/test.desc b/regression/contracts/test_struct_enforce/test.desc index 529b72a22a8..74700a3258c 100644 --- a/regression/contracts/test_struct_enforce/test.desc +++ b/regression/contracts/test_struct_enforce/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS -\[foo.\d+\] line \d+ Check that x->baz is assignable: SUCCESS -\[foo.\d+\] line \d+ Check that x->qux is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that x->baz is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that x->qux is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion rval \=\= 10: SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/test_struct_member_enforce/test.desc b/regression/contracts/test_struct_member_enforce/test.desc index 560b7fc339c..7f7a8adf160 100644 --- a/regression/contracts/test_struct_member_enforce/test.desc +++ b/regression/contracts/test_struct_member_enforce/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS -\[foo.\d+\] line \d+ Check that x->str\[\(.*\)\(x->len - 1\)\] is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that x->str\[\(.*\)\(x->len - 1\)\] is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion rval \=\= 128: SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/variant_init_inside_loop/test.desc b/regression/contracts/variant_init_inside_loop/test.desc index 78465a6cf95..b67e30c23df 100644 --- a/regression/contracts/variant_init_inside_loop/test.desc +++ b/regression/contracts/variant_init_inside_loop/test.desc @@ -4,7 +4,7 @@ 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\.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ ^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$ ^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$ ^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS$ diff --git a/regression/contracts/variant_missing_invariant_warning/test.desc b/regression/contracts/variant_missing_invariant_warning/test.desc index 80ca306f3c4..341b1e7c028 100644 --- a/regression/contracts/variant_missing_invariant_warning/test.desc +++ b/regression/contracts/variant_missing_invariant_warning/test.desc @@ -6,7 +6,7 @@ activate-multi-line-match ^\[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\.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts/variant_multidimensional_ackermann/test.desc b/regression/contracts/variant_multidimensional_ackermann/test.desc index a8e8dd2a786..ae2ba7900c4 100644 --- a/regression/contracts/variant_multidimensional_ackermann/test.desc +++ b/regression/contracts/variant_multidimensional_ackermann/test.desc @@ -6,10 +6,10 @@ main.c ^\[ackermann\.\d+\] line 21 Check loop invariant before entry: SUCCESS$ ^\[ackermann\.\d+\] line 21 Check that loop invariant is preserved: SUCCESS$ ^\[ackermann\.\d+\] line 21 Check decreases clause on loop iteration: SUCCESS$ -^\[ackermann\.\d+\] line 29 Check that m is assignable: SUCCESS$ -^\[ackermann\.\d+\] line 30 Check that n is assignable: SUCCESS$ -^\[ackermann\.\d+\] line 34 Check that n is assignable: SUCCESS$ -^\[ackermann\.\d+\] line 35 Check that m is assignable: SUCCESS$ +^\[ackermann.assigns.\d+\] line 29 Check that m is assignable: SUCCESS$ +^\[ackermann.assigns.\d+\] line 30 Check that n is assignable: SUCCESS$ +^\[ackermann.assigns.\d+\] line 34 Check that n is assignable: SUCCESS$ +^\[ackermann.assigns.\d+\] line 35 Check that m is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc b/regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc index 22c4a7531d4..68d91776ba5 100644 --- a/regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc +++ b/regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc @@ -4,9 +4,9 @@ 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: FAILURE$ -^\[main\.\d+\] line 14 Check that j is assignable: SUCCESS$ -^\[main\.\d+\] line 18 Check that i is assignable: SUCCESS$ -^\[main\.\d+\] line 19 Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 14 Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 18 Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 19 Check that j is assignable: SUCCESS$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc b/regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc index fb7d3607739..ef8dcbd7370 100644 --- a/regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc +++ b/regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc @@ -4,9 +4,9 @@ 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: FAILURE$ -^\[main\.\d+\] line 14 Check that j is assignable: SUCCESS$ -^\[main\.\d+\] line 18 Check that i is assignable: SUCCESS$ -^\[main\.\d+\] line 19 Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 14 Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 18 Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 19 Check that j is assignable: SUCCESS$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/variant_multidimensional_two_index_variables/test.desc b/regression/contracts/variant_multidimensional_two_index_variables/test.desc index 8a88e25eb86..47e373b1083 100644 --- a/regression/contracts/variant_multidimensional_two_index_variables/test.desc +++ b/regression/contracts/variant_multidimensional_two_index_variables/test.desc @@ -4,9 +4,9 @@ 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\.\d+\] line 14 Check that j is assignable: SUCCESS$ -^\[main\.\d+\] line 18 Check that i is assignable: SUCCESS$ -^\[main\.\d+\] line 19 Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 14 Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 18 Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 19 Check that j is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts/variant_not_decreasing_fail/test.desc b/regression/contracts/variant_not_decreasing_fail/test.desc index 1d3207e55f8..0f5940654f3 100644 --- a/regression/contracts/variant_not_decreasing_fail/test.desc +++ b/regression/contracts/variant_not_decreasing_fail/test.desc @@ -4,7 +4,7 @@ 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: FAILURE$ -^\[main\.\d+] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+] .* Check that i is assignable: SUCCESS$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/variant_weak_invariant_fail/test.desc b/regression/contracts/variant_weak_invariant_fail/test.desc index cbb416b5bb5..31061fa9168 100644 --- a/regression/contracts/variant_weak_invariant_fail/test.desc +++ b/regression/contracts/variant_weak_invariant_fail/test.desc @@ -4,7 +4,7 @@ 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: FAILURE$ -^\[main\.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/variant_while_true_pass/test.desc b/regression/contracts/variant_while_true_pass/test.desc index 14c961f051b..ec4727a67b7 100644 --- a/regression/contracts/variant_while_true_pass/test.desc +++ b/regression/contracts/variant_while_true_pass/test.desc @@ -4,7 +4,7 @@ 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\.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$