From cc59ac12620eeb7e68f03b52864cb49bc24aba1e Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Mon, 9 Oct 2023 19:15:23 +0100 Subject: [PATCH 1/2] Refactor ai_domaint::to_predicate() to restrict the variables used An abstract domain may contain information about variables from a calling context which are not valid in an assertion in a different function. This commit changes the interface to give a limiting scope. This is particularly fiddly in the case of pointers to things that are out of scope. --- src/analyses/ai_domain.h | 30 ++++++++- .../abstract_environment.cpp | 62 +++++++++++++++++-- .../abstract_environment.h | 2 +- .../variable-sensitivity/abstract_object.cpp | 10 ++- .../variable-sensitivity/abstract_object.h | 9 ++- .../constant_abstract_value.cpp | 4 +- .../constant_abstract_value.h | 3 +- .../constant_pointer_abstract_object.cpp | 47 +++++++++++++- .../constant_pointer_abstract_object.h | 3 +- .../context_abstract_object.cpp | 6 +- .../context_abstract_object.h | 3 +- .../full_array_abstract_object.cpp | 5 +- .../full_array_abstract_object.h | 3 +- .../full_struct_abstract_object.cpp | 5 +- .../full_struct_abstract_object.h | 3 +- .../interval_abstract_value.cpp | 4 +- .../interval_abstract_value.h | 3 +- .../value_set_abstract_object.cpp | 17 +++-- .../value_set_abstract_object.h | 3 +- .../value_set_pointer_abstract_object.cpp | 16 +++-- .../value_set_pointer_abstract_object.h | 3 +- .../variable_sensitivity_domain.cpp | 28 +-------- .../variable_sensitivity_domain.h | 11 +--- 23 files changed, 194 insertions(+), 86 deletions(-) diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h index 85d6dcb1dfb..0bfd0d32686 100644 --- a/src/analyses/ai_domain.h +++ b/src/analyses/ai_domain.h @@ -45,6 +45,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "ai_history.h" +#include + // forward reference the abstract interpreter interface class ai_baset; @@ -155,15 +157,37 @@ class ai_domain_baset /// Simplifies the expression but keeps it as an l-value virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const; - /// Gives a Boolean condition that is true for all values represented by the - /// domain. This allows domains to be converted into program invariants. - virtual exprt to_predicate(void) const + /// Gives a Boolean condition involving expression from the set that + /// is true for all of the states represented by the domain. If the + /// set is empty then the domain can use any expressions in building + /// the condition. This allows domains to be converted into program + /// invariants. + virtual exprt + to_predicate(const std::set &, const namespacet &ns) const { + // Without knowing what the domain records this is the best that + // can be done. if(is_bottom()) return false_exprt(); else return true_exprt(); } + + /// A utility function to convert to generate a predicate without + /// grammar restrictions. + virtual exprt to_predicate(const namespacet &ns) const + { + std::set empty; + return to_predicate(empty, ns); + } + + /// to_predicate for a single expression. + virtual exprt to_predicate(const exprt &e, const namespacet &ns) const + { + std::set single; + single.insert(e); + return to_predicate(single, ns); + } }; // No virtual interface is complete without a factory! diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index d1a9cdad5dd..0e9d59fbae1 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -424,7 +424,9 @@ void abstract_environmentt::output( out << "}\n"; } -exprt abstract_environmentt::to_predicate() const +exprt abstract_environmentt::to_predicate( + const std::set &scope, + const namespacet &ns) const { if(is_bottom()) return false_exprt(); @@ -432,13 +434,61 @@ exprt abstract_environmentt::to_predicate() const return true_exprt(); exprt::operandst predicates; - for(const auto &entry : map.get_view()) + + if(scope.size() == 0) + { + for(const auto &entry : map.get_view()) + { + auto sym = entry.first; + auto val = entry.second; + + INVARIANT( + !val->is_bottom(), + "If one variable is bottom, the whole domain should be"); + if(val->is_top()) + { + continue; + } + else + { + auto pred = val->to_predicate(symbol_exprt(sym, val->type()), scope); + + // It is possible that the abstract object is not top but the + // information it contains is not expressible as a predicate. + // For example if it just has write locations. + INVARIANT(!pred.is_false(), "Only bottom should give false"); + if(!pred.is_true()) + { + predicates.push_back(pred); + } + } + } + } + else { - auto sym = entry.first; - auto val = entry.second; - auto pred = val->to_predicate(symbol_exprt(sym, val->type())); + for(const auto &expr : scope) + { + auto val = eval(expr, ns); - predicates.push_back(pred); + if(val->is_top()) + { + continue; + } + else if(val->is_bottom()) + { + // Unlike the previous case, this is possible if the user + // passes an expression like 'x == 1' which can be evaluated + // to false + return false_exprt(); + } + + auto pred = val->to_predicate(expr, scope); + INVARIANT(!pred.is_false(), "Only bottom should give false"); + if(!pred.is_true()) + { + predicates.push_back(pred); + } + } } if(predicates.size() == 1) diff --git a/src/analyses/variable-sensitivity/abstract_environment.h b/src/analyses/variable-sensitivity/abstract_environment.h index f1785e917df..64a69949636 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.h +++ b/src/analyses/variable-sensitivity/abstract_environment.h @@ -222,7 +222,7 @@ class abstract_environmentt /// environment. /// /// \return An exprt describing the environment - exprt to_predicate() const; + exprt to_predicate(const std::set &scope, const namespacet &ns) const; /// Check the structural invariants are maintained. /// In this case this is checking there aren't any null pointer mapped values diff --git a/src/analyses/variable-sensitivity/abstract_object.cpp b/src/analyses/variable-sensitivity/abstract_object.cpp index 86c42d56be7..5f20500fbf0 100644 --- a/src/analyses/variable-sensitivity/abstract_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_object.cpp @@ -158,16 +158,20 @@ exprt abstract_objectt::to_constant() const return nil_exprt(); } -exprt abstract_objectt::to_predicate(const exprt &name) const +exprt abstract_objectt::to_predicate( + const exprt &name, + const std::set &scope) const { if(is_top()) return true_exprt(); if(is_bottom()) return false_exprt(); - return to_predicate_internal(name); + return to_predicate_internal(name, scope); } -exprt abstract_objectt::to_predicate_internal(const exprt &name) const +exprt abstract_objectt::to_predicate_internal( + const exprt &name, + const std::set &) const { UNREACHABLE; return nil_exprt(); diff --git a/src/analyses/variable-sensitivity/abstract_object.h b/src/analyses/variable-sensitivity/abstract_object.h index 914f291ff13..2c71fa0f6a7 100644 --- a/src/analyses/variable-sensitivity/abstract_object.h +++ b/src/analyses/variable-sensitivity/abstract_object.h @@ -158,13 +158,14 @@ class abstract_objectt : public std::enable_shared_from_this /// Converts to an invariant expression /// /// \param name - the variable name to substitute into the expression + /// \param scope - the set of exprt which can be used to build the predicate /// \return Returns an exprt representing the object as an invariant. /// - /// The the abstract element represents a single value the expression will + /// If the abstract element represents a single value the expression will /// have the form _name = value_, if the value is an interval it will have the /// the form _lower <= name <= upper_, etc. /// If the value is bottom returns false, if top returns true. - exprt to_predicate(const exprt &name) const; + exprt to_predicate(const exprt &name, const std::set &scope) const; /** * A helper function to evaluate writing to a component of an @@ -361,8 +362,10 @@ class abstract_objectt : public std::enable_shared_from_this /// to_predicate implementation - derived classes will override /// \param name - the variable name to substitute into the expression + /// \param scope - the set of expressions that can be used /// \return Returns an exprt representing the object as an invariant. - virtual exprt to_predicate_internal(const exprt &name) const; + virtual exprt + to_predicate_internal(const exprt &name, const std::set &scope) const; private: /// To enforce copy-on-write these are private and have read-only accessors diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.cpp b/src/analyses/variable-sensitivity/constant_abstract_value.cpp index 32d46f06f6f..6985e90b3ba 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/constant_abstract_value.cpp @@ -139,7 +139,9 @@ abstract_value_pointert constant_abstract_valuet::constrain( return as_value(mutable_clone()); } -exprt constant_abstract_valuet::to_predicate_internal(const exprt &name) const +exprt constant_abstract_valuet::to_predicate_internal( + const exprt &name, + const std::set &) const { return equal_exprt(name, value); } diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.h b/src/analyses/variable-sensitivity/constant_abstract_value.h index 4f9e4561644..cc8d50389ee 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.h +++ b/src/analyses/variable-sensitivity/constant_abstract_value.h @@ -80,7 +80,8 @@ class constant_abstract_valuet : public abstract_value_objectt abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override; - exprt to_predicate_internal(const exprt &name) const override; + exprt to_predicate_internal(const exprt &name, const std::set &scope) + const override; private: exprt value; diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp index b4bf1a6312b..ba7075704c2 100644 --- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp @@ -387,7 +387,50 @@ exprt constant_pointer_abstract_objectt::ptr_comparison_expr( } exprt constant_pointer_abstract_objectt::to_predicate_internal( - const exprt &name) const + const exprt &name, + const std::set &scope) const { - return equal_exprt(name, value_stack.to_expression()); + exprt target = value_stack.to_expression(); + + // This is simple if there are no restrictions: + if(scope.size() == 0) + { + return equal_exprt(name, target); + } + else + { + // However handling the scope requires some care. + // Because if you have a pointer to a[i]->field then you need to + // check if a[i]->field, a[i] or a is in the scope. + exprt working = target; + do + { + if(scope.find(working) != scope.end()) + { + return equal_exprt(name, target); + } + + if(working.id() == ID_index) + { + working = to_index_expr(working).array(); + } + else if(working.id() == ID_member) + { + working = to_member_expr(working).compound(); + } + else if(working.id() == ID_symbol || working.id() == ID_dynamic_object) + { + // If this has not been found then the object that the + // (abstract) pointer points to is not in scope and so can't + // be directly expressed, so true is the best we can do + return true_exprt(); + } + else + { + // These should be the only things generated from a write stack + UNREACHABLE; + } + } while(1); + } + UNREACHABLE; } diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h index 2a7a053451b..4369ba62ca8 100644 --- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h @@ -142,7 +142,8 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt CLONE - exprt to_predicate_internal(const exprt &name) const override; + exprt to_predicate_internal(const exprt &name, const std::set &scope) + const override; private: bool same_target(abstract_object_pointert other) const; diff --git a/src/analyses/variable-sensitivity/context_abstract_object.cpp b/src/analyses/variable-sensitivity/context_abstract_object.cpp index 97488c06043..967ebaca7e3 100644 --- a/src/analyses/variable-sensitivity/context_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/context_abstract_object.cpp @@ -171,9 +171,11 @@ abstract_object_pointert context_abstract_objectt::unwrap_context() const return child_abstract_object->unwrap_context(); } -exprt context_abstract_objectt::to_predicate_internal(const exprt &name) const +exprt context_abstract_objectt::to_predicate_internal( + const exprt &name, + const std::set &scope) const { - return child_abstract_object->to_predicate(name); + return child_abstract_object->to_predicate(name, scope); } void context_abstract_objectt::get_statistics( diff --git a/src/analyses/variable-sensitivity/context_abstract_object.h b/src/analyses/variable-sensitivity/context_abstract_object.h index c0b067e696a..14d0c7d3b6f 100644 --- a/src/analyses/variable-sensitivity/context_abstract_object.h +++ b/src/analyses/variable-sensitivity/context_abstract_object.h @@ -122,7 +122,8 @@ class context_abstract_objectt : public abstract_objectt bool has_been_modified(const abstract_object_pointert &before) const override; - exprt to_predicate_internal(const exprt &name) const override; + exprt to_predicate_internal(const exprt &name, const std::set &scope) + const override; typedef std::set locationst; diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp index 1d766adf82a..99c4ea127d6 100644 --- a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp @@ -416,7 +416,8 @@ abstract_object_pointert full_array_abstract_objectt::visit_sub_elements( } exprt full_array_abstract_objectt::to_predicate_internal( - const exprt &name) const + const exprt &name, + const std::set &scope) const { auto all_predicates = exprt::operandst{}; @@ -424,7 +425,7 @@ exprt full_array_abstract_objectt::to_predicate_internal( { auto ii = from_integer(field.first.to_long(), integer_typet()); auto index = index_exprt(name, ii); - auto field_expr = field.second->to_predicate(index); + auto field_expr = field.second->to_predicate(index, scope); if(!field_expr.is_true()) all_predicates.push_back(field_expr); diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.h b/src/analyses/variable-sensitivity/full_array_abstract_object.h index c2e0a74ffa4..5052df9aced 100644 --- a/src/analyses/variable-sensitivity/full_array_abstract_object.h +++ b/src/analyses/variable-sensitivity/full_array_abstract_object.h @@ -232,7 +232,8 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt< const full_array_pointert &other, const widen_modet &widen_mode) const; - exprt to_predicate_internal(const exprt &name) const override; + exprt to_predicate_internal(const exprt &name, const std::set &scope) + const override; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp index a2b2a6f9cbc..55e0ae269b2 100644 --- a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp @@ -296,7 +296,8 @@ abstract_object_pointert full_struct_abstract_objectt::visit_sub_elements( } exprt full_struct_abstract_objectt::to_predicate_internal( - const exprt &name) const + const exprt &name, + const std::set &scope) const { const auto &compound_type = to_struct_union_type(name.type()); auto all_predicates = exprt::operandst{}; @@ -305,7 +306,7 @@ exprt full_struct_abstract_objectt::to_predicate_internal( { auto field_name = member_exprt(name, compound_type.get_component(field.first)); - auto field_expr = field.second->to_predicate(field_name); + auto field_expr = field.second->to_predicate(field_name, scope); if(!field_expr.is_true()) all_predicates.push_back(field_expr); diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.h b/src/analyses/variable-sensitivity/full_struct_abstract_object.h index c3f08bcba32..c152a872efc 100644 --- a/src/analyses/variable-sensitivity/full_struct_abstract_object.h +++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.h @@ -180,7 +180,8 @@ class full_struct_abstract_objectt : public abstract_aggregate_objectt< const abstract_object_pointert &other, const widen_modet &widen_mode) const override; - exprt to_predicate_internal(const exprt &name) const override; + exprt to_predicate_internal(const exprt &name, const std::set &scope) + const override; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_H diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 51f738c5109..eaeb500f039 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -455,7 +455,9 @@ abstract_value_pointert interval_abstract_valuet::constrain( make_interval(constant_interval_exprt(lower_bound, upper_bound))); } -exprt interval_abstract_valuet::to_predicate_internal(const exprt &name) const +exprt interval_abstract_valuet::to_predicate_internal( + const exprt &name, + const std::set &) const { if(interval.is_single_value_interval()) return equal_exprt(name, interval.get_lower()); diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 9985d872448..f5fb3550394 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -93,7 +93,8 @@ class interval_abstract_valuet : public abstract_value_objectt abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override; - exprt to_predicate_internal(const exprt &name) const override; + exprt to_predicate_internal(const exprt &name, const std::set &scope) + const override; private: constant_interval_exprt interval; diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 5357fc3046a..2b1134de3ed 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -330,20 +330,19 @@ abstract_value_pointert value_set_abstract_objectt::constrain( return as_value(resolve_values(constrained_values)); } -exprt value_set_abstract_objectt::to_predicate_internal(const exprt &name) const +exprt value_set_abstract_objectt::to_predicate_internal( + const exprt &name, + const std::set &scope) const { auto compacted = non_destructive_compact(values); if(compacted.size() == 1) - return compacted.first()->to_predicate(name); + return compacted.first()->to_predicate(name, scope); auto all_predicates = exprt::operandst{}; - std::transform( - compacted.begin(), - compacted.end(), - std::back_inserter(all_predicates), - [&name](const abstract_object_pointert &value) { - return value->to_predicate(name); - }); + for(const auto &c : compacted) + { + all_predicates.push_back(c->to_predicate(name, scope)); + } std::sort(all_predicates.begin(), all_predicates.end()); return or_exprt(all_predicates); diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 19be166ec5d..3119b421fe9 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -66,7 +66,8 @@ class value_set_abstract_objectt : public abstract_value_objectt, abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override; - exprt to_predicate_internal(const exprt &name) const override; + exprt to_predicate_internal(const exprt &name, const std::set &scope) + const override; private: /// Setter for updating the stored values diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp index 97a01342093..4e38d17e975 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp @@ -226,19 +226,17 @@ abstract_object_pointert value_set_pointer_abstract_objectt::merge( } exprt value_set_pointer_abstract_objectt::to_predicate_internal( - const exprt &name) const + const exprt &name, + const std::set &scope) const { if(values.size() == 1) - return values.first()->to_predicate(name); + return values.first()->to_predicate(name, scope); auto all_predicates = exprt::operandst{}; - std::transform( - values.begin(), - values.end(), - std::back_inserter(all_predicates), - [&name](const abstract_object_pointert &value) { - return value->to_predicate(name); - }); + for(const auto &v : values) + { + all_predicates.push_back(v->to_predicate(name, scope)); + } std::sort(all_predicates.begin(), all_predicates.end()); return or_exprt(all_predicates); diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h index 56de6a00219..2ed2b1acacc 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h @@ -95,7 +95,8 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt, const abstract_object_pointert &other, const widen_modet &widen_mode) const override; - exprt to_predicate_internal(const exprt &name) const override; + exprt to_predicate_internal(const exprt &name, const std::set &scope) + const override; private: /// Update the set of stored values to \p new_values. Build a new abstract diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index b348096522c..801410c6697 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -176,35 +176,11 @@ void variable_sensitivity_domaint::output( abstract_state.output(out, ai, ns); } -exprt variable_sensitivity_domaint::to_predicate() const -{ - return abstract_state.to_predicate(); -} - -exprt variable_sensitivity_domaint::to_predicate( - const exprt &expr, - const namespacet &ns) const -{ - auto result = abstract_state.eval(expr, ns); - return result->to_predicate(expr); -} - exprt variable_sensitivity_domaint::to_predicate( - const exprt::operandst &exprs, + const std::set &scope, const namespacet &ns) const { - if(exprs.empty()) - return false_exprt(); - if(exprs.size() == 1) - return to_predicate(exprs.front(), ns); - - auto predicates = std::vector{}; - std::transform( - exprs.cbegin(), - exprs.cend(), - std::back_inserter(predicates), - [this, &ns](const exprt &expr) { return to_predicate(expr, ns); }); - return and_exprt(predicates); + return abstract_state.to_predicate(scope, ns); } void variable_sensitivity_domaint::make_bottom() diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h index 707de155078..67ac336990b 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h @@ -153,14 +153,9 @@ class variable_sensitivity_domaint : public ai_domain_baset void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override; - /// Gives a Boolean condition that is true for all values represented by the - /// domain. This allows domains to be converted into program invariants. - /// - /// \return exprt describing the domain - exprt to_predicate() const override; - - exprt to_predicate(const exprt &expr, const namespacet &ns) const; - exprt to_predicate(const exprt::operandst &exprs, const namespacet &ns) const; + /// \copydoc ai_domaint::to_predicate + virtual exprt to_predicate(const std::set &scope, const namespacet &ns) + const override; /// Computes the join between "this" and "b". /// From c0dc3a67047dddf98112764958507c98849c45e8 Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 11 Aug 2022 18:02:20 +0100 Subject: [PATCH 2/2] Add a task to goto-analyzer to instrument the program with invariants --- doc/cprover-manual/goto-analyzer.md | 48 +- doc/man/goto-analyzer.1 | 22 + .../after_goto_not_taken.desc | 14 + .../instrument-basic/any_goto_target.desc | 13 + .../instrument-basic/assertions.desc | 14 + .../backwards_goto_target.desc | 13 + .../instrument-basic/default.desc | 13 + .../instrument-basic/ensures.desc | 12 + .../instrument-basic/function_call.desc | 13 + .../instrument-basic/function_end.desc | 14 + .../instrument-basic/function_return.desc | 13 + .../instrument-basic/function_start.desc | 14 + .../goto-analyzer/instrument-basic/main.c | 29 ++ .../instrument-basic/requires.desc | 14 + src/goto-analyzer/Makefile | 1 + .../goto_analyzer_parse_options.cpp | 43 ++ .../goto_analyzer_parse_options.h | 7 +- src/goto-analyzer/static_instrument.cpp | 461 ++++++++++++++++++ src/goto-analyzer/static_instrument.h | 73 +++ 19 files changed, 828 insertions(+), 3 deletions(-) create mode 100644 regression/goto-analyzer/instrument-basic/after_goto_not_taken.desc create mode 100644 regression/goto-analyzer/instrument-basic/any_goto_target.desc create mode 100644 regression/goto-analyzer/instrument-basic/assertions.desc create mode 100644 regression/goto-analyzer/instrument-basic/backwards_goto_target.desc create mode 100644 regression/goto-analyzer/instrument-basic/default.desc create mode 100644 regression/goto-analyzer/instrument-basic/ensures.desc create mode 100644 regression/goto-analyzer/instrument-basic/function_call.desc create mode 100644 regression/goto-analyzer/instrument-basic/function_end.desc create mode 100644 regression/goto-analyzer/instrument-basic/function_return.desc create mode 100644 regression/goto-analyzer/instrument-basic/function_start.desc create mode 100644 regression/goto-analyzer/instrument-basic/main.c create mode 100644 regression/goto-analyzer/instrument-basic/requires.desc create mode 100644 src/goto-analyzer/static_instrument.cpp create mode 100644 src/goto-analyzer/static_instrument.h diff --git a/doc/cprover-manual/goto-analyzer.md b/doc/cprover-manual/goto-analyzer.md index f5a84207e76..c3fadcb1ffd 100644 --- a/doc/cprover-manual/goto-analyzer.md +++ b/doc/cprover-manual/goto-analyzer.md @@ -49,16 +49,21 @@ goto-analyzer --verify --three-way-merge --vsd --vsd-values set-of-constants -- I want to discharge obvious conditions and remove unreachable code: ``` -goto-analyzer --simplify out.gb --three-way-merge --vsd +goto-analyzer --simplify out.gb --three-way-merge --vsd program.c ``` I want to build a dependency graph: ``` -goto-analyzer --show --dot depgraph.dot --dependence-graph-vs +goto-analyzer --show --dot depgraph.dot --dependence-graph-vs program.c ``` +I want to generate code contracts: +``` +goto-analyzer --instrument out.gb --instrument-targets requires,ensures,function_start,function_end,backwards_goto_target --vsd --verbosity 9 program.c +``` + ## Task @@ -106,6 +111,45 @@ domain which can result in a second (or more) runs giving simplification. Submitting bug reports for these is helpful but they may not be viable to fix. +`--instrument output_file.gb` +: Produces a new version of the GOTO binary in which +the abstract domains have been used to insert annotations, such as assertios +or assumptions. If everything is working correctly these should always +be true because they are implied by the program and are an overapproximation. +However they can be useful for a number of reasons. Assertions can be +used to test the results of goto-analyze against another tool. +Assumptions can be useful as auxilliary constraints to help other +tools or to provide better approximations of parts of the program. +The exact instrumentation depends on the domain. + +`--instrument-targets` +: A comma separated list of where in the program instrumentation should +be added and what kind of instrumentation should be inserted. +Available locations are `function_start`, `function_end`, `function_call` +(before function calls), `function_return` (after function calls), +`any_goto_target`, `backwards_goto_target`, `after_goto_not_taken`, +`requires` and `ensures`. If just the locations is used, assumptions +will be inserted apart from requires and assumes which add the +corresponding code contracts. If the location is given followed by +`=assume`, `=assert` or `=nothing` then assumptions, assertions or +nothing is inserted. A little care is necessary when using contracts +generated by `goto-analyzer`. The `requires` contract is an +over-approximations of the calling context in the analyzed program. +So if the function has flags (read, write, append, etc.) but only one +set is used in the program then the `requires` contract may well +include that specific set of flags. In that sense what is generated +is an over-approximation (i.e. a weakening or less restrictive +version) of the strongest pre-condition that would work for the +program you have analysed. In practice you may want to weaken it +further so your verification results are more general. Likewise the +`ensures` contract is an over-approximation of what the function does +in the analyzed program. If part of the functionality of the function +is not used then it may not be in the generated contract. In the +example of flags above, if the program only uses one set of flags, the +`ensures` contract may not include changes that are possible using +other sets of flags. Again, it may be desirable to weaken the +generated contract so it can be used more generally. + `--unreachable-instructions` : Lists which instructions have a domain which is bottom (i.e. unreachable). If `--function` has been used to set the program diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1 index 9517eef3072..8f4155174dc 100644 --- a/doc/man/goto-analyzer.1 +++ b/doc/man/goto-analyzer.1 @@ -109,6 +109,28 @@ may not be viable to fix. Do not remove instructions from which no property can be reached (use with \fB\-\-simplify\fR). .TP +\fB\-\-instrument\fR \fIfile_name\fR +Writes a new version of the input program to \fIfile_name\fR in which +the abstract domains have been used to insert annotations, such as assertios +or assumptions. If everything is working correctly these should always +be true because they are implied by the program and are an overapproximation. +However they can be useful for a number of reasons. Assertions can be +used to test the results of goto-analyze against another tool. +Assumptions can be useful as auxilliary constraints to help other +tools or to provide better approximations of parts of the program. +The exact instrumentation depends on the domain. +.TP +\fB\-\-instrument\-targets\fR +A comma separated list of where in the program instrumentation should +be added and what kind of instrumentation should be inserted. +Available locations are function_start, function_end, function_call +(before function calls), function_return (after function calls), +any_goto_target, backwards_goto_target, after_goto_not_taken, requires +and ensures. If just the locations is used, assumptions will be +inserted apart from requires and assumes which add the corresponding +code contracts. If the location is given followed by =assume, =assert or +=nothing then assumptions, assertions or nothing is inserted. +.TP \fB\-\-unreachable\-instructions\fR Lists which instructions have a domain which is bottom (i.e. unreachable). If \fB\-\-function\fR has been used to set the program diff --git a/regression/goto-analyzer/instrument-basic/after_goto_not_taken.desc b/regression/goto-analyzer/instrument-basic/after_goto_not_taken.desc new file mode 100644 index 00000000000..47a91d5c510 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/after_goto_not_taken.desc @@ -0,0 +1,14 @@ +CORE +main.c +--instrument out.gb --instrument-targets after_goto_not_taken --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting example_function\nInstruction \d+ because after_goto_not_taken... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at after gotos that are not taken (i.e. the "other" branch that is not a goto_target) + + + diff --git a/regression/goto-analyzer/instrument-basic/any_goto_target.desc b/regression/goto-analyzer/instrument-basic/any_goto_target.desc new file mode 100644 index 00000000000..4764d6ff748 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/any_goto_target.desc @@ -0,0 +1,13 @@ +CORE +main.c +--instrument out.gb --instrument-targets any_goto_target --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting example_function\nInstruction \d+ because any_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption\nInstruction \d+ because any_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1 ∧ \(10 ≤ example_function::1::1::i ∧ example_function::1::1::i ≤ max_value\)... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at goto targets + + diff --git a/regression/goto-analyzer/instrument-basic/assertions.desc b/regression/goto-analyzer/instrument-basic/assertions.desc new file mode 100644 index 00000000000..aceef5b2639 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/assertions.desc @@ -0,0 +1,14 @@ +CORE +main.c +--instrument out.gb --instrument-targets function_call=assert,function_start=assume,function_end=assert,function_return=assume --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_return... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption\nInstruction \d+ because function_end... single history... condition is main#return_value = 0 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assertion\nInstruction \d+ because function_start... single history... condition is true_from_calling_context = 0 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption\nInstruction \d+ because function_call... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assertion$ +^Instrumenting example_function\nInstruction \d+ because function_end... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assertion\nInstruction \d+ because function_start... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing the addition of assertions in a way that mimics the use of contracts + + diff --git a/regression/goto-analyzer/instrument-basic/backwards_goto_target.desc b/regression/goto-analyzer/instrument-basic/backwards_goto_target.desc new file mode 100644 index 00000000000..fe8004ec2a5 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/backwards_goto_target.desc @@ -0,0 +1,13 @@ +CORE +main.c +--instrument out.gb --instrument-targets backwards_goto_target --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting example_function\nInstruction \d+ because backwards_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at backwards goto targets + + diff --git a/regression/goto-analyzer/instrument-basic/default.desc b/regression/goto-analyzer/instrument-basic/default.desc new file mode 100644 index 00000000000..425935f3aaa --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/default.desc @@ -0,0 +1,13 @@ +CORE +main.c +--instrument out.gb --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_start... single history... condition is true_from_calling_context = 0 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption\nInstruction \d+ because function_return... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$ +^Instrumenting example_function\nInstruction \d+ because function_start... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption\nInstruction \d+ because backwards_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing the default options of instrumentation with goto-analyze + diff --git a/regression/goto-analyzer/instrument-basic/ensures.desc b/regression/goto-analyzer/instrument-basic/ensures.desc new file mode 100644 index 00000000000..a97588ecfc2 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/ensures.desc @@ -0,0 +1,12 @@ +CORE +main.c +--instrument out.gb --instrument-targets ensures --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting example_function\nAdd ensures contract... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as contract$ +-- +^warning: ignoring +-- +Testing instrumenting add ensures contract + diff --git a/regression/goto-analyzer/instrument-basic/function_call.desc b/regression/goto-analyzer/instrument-basic/function_call.desc new file mode 100644 index 00000000000..a8e0b60c51e --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/function_call.desc @@ -0,0 +1,13 @@ +CORE +main.c +--instrument out.gb --instrument-targets function_call --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_call... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at function call + + diff --git a/regression/goto-analyzer/instrument-basic/function_end.desc b/regression/goto-analyzer/instrument-basic/function_end.desc new file mode 100644 index 00000000000..13c82059cbd --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/function_end.desc @@ -0,0 +1,14 @@ +CORE +main.c +--instrument out.gb --instrument-targets function_end --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_end... single history... condition is main#return_value = 0 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$ +^Instrumenting example_function\nInstruction \d+ because function_end... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at the function end + + diff --git a/regression/goto-analyzer/instrument-basic/function_return.desc b/regression/goto-analyzer/instrument-basic/function_return.desc new file mode 100644 index 00000000000..c82548fd455 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/function_return.desc @@ -0,0 +1,13 @@ +CORE +main.c +--instrument out.gb --instrument-targets function_return --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_return... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at function return + + diff --git a/regression/goto-analyzer/instrument-basic/function_start.desc b/regression/goto-analyzer/instrument-basic/function_start.desc new file mode 100644 index 00000000000..3e7bacc4ffb --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/function_start.desc @@ -0,0 +1,14 @@ +CORE +main.c +--instrument out.gb --instrument-targets function_start --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting main\nInstruction \d+ because function_start... single history... condition is true_from_calling_context = 0 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$ +^Instrumenting example_function\nInstruction \d+ because function_start... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$ +-- +^warning: ignoring +-- +Testing instrumenting at the function start + + diff --git a/regression/goto-analyzer/instrument-basic/main.c b/regression/goto-analyzer/instrument-basic/main.c new file mode 100644 index 00000000000..b4a5655f29c --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/main.c @@ -0,0 +1,29 @@ +int true_from_calling_context = 0; + +int example_function(int argument) +{ + int local = argument + 1; + int location = 1; + + for(int i = 0; i < 10; ++i) + { + location = 2; + ++local; + } + + location = 3; + ++local; + + return location + local; +} + +int main(int argc, char **argv) +{ + true_from_calling_context = 1; + + int argument_input = 1; + + int ret = example_function(argument_input); + + return 0; +} diff --git a/regression/goto-analyzer/instrument-basic/requires.desc b/regression/goto-analyzer/instrument-basic/requires.desc new file mode 100644 index 00000000000..9af91e22a72 --- /dev/null +++ b/regression/goto-analyzer/instrument-basic/requires.desc @@ -0,0 +1,14 @@ +CORE +main.c +--instrument out.gb --instrument-targets requires --verbosity 9 --vsd +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^Instrumenting example_function\nAdd requires contract... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as contract$ +-- +^warning: ignoring +-- +Testing instrumenting add requires contract + + + diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index d3cc012ca02..a2fd3d9a74d 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -5,6 +5,7 @@ SRC = goto_analyzer_languages.cpp \ taint_parser.cpp \ unreachable_instructions.cpp \ show_on_source.cpp \ + static_instrument.cpp \ static_show_domain.cpp \ static_simplifier.cpp \ static_verifier.cpp \ diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index f6463eca656..bc72ad823df 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "build_analyzer.h" #include "show_on_source.h" +#include "static_instrument.h" #include "static_show_domain.h" #include "static_simplifier.h" #include "static_verifier.h" @@ -193,6 +194,18 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) "simplify-slicing", !(cmdline.isset("no-simplify-slicing"))); } + else if(cmdline.isset("instrument")) + { + if(cmdline.get_value("instrument") == "-") + throw invalid_command_line_argument_exceptiont( + "cannot output goto binary to stdout", "--instrument"); + + options.set_option("instrument", true); + options.set_option("outfile", cmdline.get_value("instrument")); + options.set_option("general-analysis", true); + options.set_option( + "instrument-targets", cmdline.get_value("instrument-targets")); + } else if(cmdline.isset("show-intervals")) { // For backwards compatibility @@ -656,6 +669,34 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) result = static_simplifier( goto_model, *analyzer, options, ui_message_handler, out); } + else if(options.get_bool_option("instrument")) + { + PRECONDITION(!outfile.empty() && outfile != "-"); + output_stream.close(); + output_stream.open(outfile, std::ios::binary); + if( + options.is_set("instrument-targets") && + options.get_option("instrument-targets") != "") + { + result = static_instrument( + goto_model, + *analyzer, + options.get_option("instrument-targets"), + ui_message_handler, + out); + } + else + { + // A reasonably sane set of defaults + result = static_instrument( + goto_model, + *analyzer, + "function_start=assume,function_return=assume,backwards_goto_target=" + "assume", + ui_message_handler, + out); + } + } else if(options.get_bool_option("unreachable-instructions")) { result = static_unreachable_instructions(goto_model, @@ -746,6 +787,8 @@ void goto_analyzer_parse_optionst::help() " program\n" " {y--no-simplify-slicing} \t do not remove instructions from which no" " property can be reached (use with {y--simplify})\n" + " {y--instrument} {ufile_name} \t use the abstract domains to generate annotations\n" + " {y--instrument-targets} {ulist} \t where to annotate and what annotations to use\n" " {y--unreachable-instructions} \t list dead code\n" " {y--unreachable-functions} \t list functions unreachable from the entry" " point\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index a78643b12d7..0ec96eb068f 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -109,10 +109,15 @@ class optionst; #define GOTO_ANALYSER_OPTIONS_TASKS \ "(show)(verify)(simplify):" \ "(show-on-source)" \ + "(instrument):" \ "(unreachable-instructions)(unreachable-functions)" \ "(reachable-functions)" \ "(no-standard-checks)" +#define GOTO_ANALYZER_OPTIONS_TASKS_CONFIG \ + "(no-simplify-slicing)" \ + "(instrument-targets):" \ + #define GOTO_ANALYSER_OPTIONS_AI \ "(recursive-interprocedural)" \ "(three-way-merge)" \ @@ -161,7 +166,7 @@ class optionst; OPT_TIMESTAMP \ OPT_VALIDATE \ GOTO_ANALYSER_OPTIONS_TASKS \ - "(no-simplify-slicing)" \ + GOTO_ANALYZER_OPTIONS_TASKS_CONFIG \ "(show-intervals)(show-non-null)" \ GOTO_ANALYSER_OPTIONS_AI \ "(location-sensitive)(concurrent)" \ diff --git a/src/goto-analyzer/static_instrument.cpp b/src/goto-analyzer/static_instrument.cpp new file mode 100644 index 00000000000..5c47a259904 --- /dev/null +++ b/src/goto-analyzer/static_instrument.cpp @@ -0,0 +1,461 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#include "static_instrument.h" + +#include +#include +#include +#include +#include +#include +#include + +#include +#include +#include +#include + +#include + +#include + +static std::string s_function_start = "function_start"; +static std::string s_function_end = "function_end"; +static std::string s_function_call = "function_call"; +static std::string s_function_return = "function_return"; +static std::string s_any_goto_target = "any_goto_target"; +static std::string s_backwards_goto_target = "backwards_goto_target"; +static std::string s_after_goto_not_taken = "after_goto_not_taken"; + +// Build a configuration from user strings +instrument_configt::instrument_configt(const std::string &opts) +{ + // Initialise everything to the defaults + function_start = instrument_actiont::NOTHING; + function_end = instrument_actiont::NOTHING; + function_call = instrument_actiont::NOTHING; + function_return = instrument_actiont::NOTHING; + any_goto_target = instrument_actiont::NOTHING; + backwards_goto_target = instrument_actiont::NOTHING; + after_goto_not_taken = instrument_actiont::NOTHING; + requires = false; + ensures = false; + + if(opts == "") + { + return; + } + + // A helper struct + struct config_targett + { + const std::string &name; + instrument_actiont *target; + + config_targett(const std::string &n, instrument_actiont *t) + : name(n), target(t) + { + } + }; + + std::vector options; + options.push_back(config_targett(s_function_start, &(this->function_start))); + options.push_back(config_targett(s_function_end, &(this->function_end))); + options.push_back(config_targett(s_function_call, &(this->function_call))); + options.push_back( + config_targett(s_function_return, &(this->function_return))); + options.push_back( + config_targett(s_any_goto_target, &(this->any_goto_target))); + options.push_back( + config_targett(s_backwards_goto_target, &(this->backwards_goto_target))); + options.push_back( + config_targett(s_after_goto_not_taken, &(this->after_goto_not_taken))); + + auto const config_strings = split_string(opts, ','); + for(auto const &config_string : config_strings) + { + instrument_actiont *target = NULL; + std::string remainder = ""; + + for(auto const &option : options) + { + if(config_string.substr(0, option.name.length()) == option.name) + { + target = option.target; + remainder = config_string.substr(option.name.length()); + break; + } + } + + if(target == NULL) + { + if(config_string == "requires") + { + requires = true; + } + else if(config_string == "ensures") + { + ensures = true; + } + else + { + throw invalid_command_line_argument_exceptiont( + "Unrecognised instrument option: " + config_string, opts); + } + } + else + { + if((remainder == "") || (remainder == "=assume")) + *target = instrument_actiont::ASSUME; + else if(remainder == "=assert") + *target = instrument_actiont::ASSERT; + else if(remainder == "=nothing") + *target = instrument_actiont::NOTHING; + else + { + throw invalid_command_line_argument_exceptiont( + "Unrecognised instrument action: " + remainder, opts); + } + } + } +} + +typedef std::map< + goto_programt::targett, + std::pair, + goto_programt::target_less_than> + instrument_locationst; + +static instrument_locationst get_instrumentation_locations( + goto_programt &gp, + const instrument_configt &config) +{ + instrument_locationst targets; + + goto_programt::targett prev_it = gp.instructions.begin(); + Forall_goto_program_instructions(i_it, gp) + { + instrument_actiont action = instrument_actiont::NOTHING; + std::string *reason; + + if(i_it == gp.instructions.begin()) + { + action = config.function_start; + reason = &s_function_start; + } + else if(i_it->is_end_function()) + { + action = config.function_end; + reason = &s_function_end; + } + else if(i_it->is_function_call()) + { + action = config.function_call; + reason = &s_function_call; + } + else if(prev_it->is_function_call()) + { + action = config.function_return; + reason = &s_function_return; + } + else if(i_it->is_target()) + { + action = config.any_goto_target; + reason = &s_any_goto_target; + + // Choices for backwards_goto override any_goto if present + if(config.backwards_goto_target != instrument_actiont::NOTHING) + { + for(auto const incoming_it : i_it->incoming_edges) + { + if(incoming_it->is_backwards_goto()) + { + action = config.backwards_goto_target; + reason = &s_backwards_goto_target; + break; // inner! + } + } + } + } + else if(prev_it->is_goto() && !prev_it->condition().is_true()) + { + action = config.after_goto_not_taken; + reason = &s_after_goto_not_taken; + } + + if(action != instrument_actiont::NOTHING) + { + targets.emplace(i_it, std::make_pair(action, reason)); + } + + // This bit is vital! + prev_it = i_it; + } + + return targets; +} + +static exprt compute_instrumentation_expression( + goto_programt::targett i_it, + const ai_baset &ai, + const namespacet &ns, + const std::set &relevant_expressions, + messaget &m) +{ + // Multiple histories are handled as disjunctions + exprt::operandst inst; + + const auto trace_set_pointer = + ai.abstract_traces_before(i_it); // Keep a pointer so refcount > 0 + const auto &trace_set = *trace_set_pointer; + + if(trace_set.size() == 0) // i.e. unreachable + { + m.progress() << "unreachable... "; // No EOM yet + + inst.push_back(false_exprt{}); + } + else if(trace_set.size() == 1) + { + auto dp = ai.abstract_state_before(i_it); + + m.progress() << "single history... "; // No EOM yet + + inst.push_back(dp->to_predicate(relevant_expressions, ns)); + } + else + { + m.progress() << "multiple histories... "; // No EOM yet + + for(const auto &trace_ptr : trace_set) + { + auto dp = ai.abstract_state_before(trace_ptr); + inst.push_back(dp->to_predicate(relevant_expressions, ns)); + } + } + + return disjunction(inst); +} + +static void +get_globals(std::set &relevant_expressions, const namespacet &ns) +{ + system_library_symbolst lib; + std::set out; // Unused + + for(const auto &symbol_pair : ns.get_symbol_table().symbols) + { + const symbolt &symbol = symbol_pair.second; + auto name_string = id2string(symbol.name); + if( + symbol.is_lvalue && symbol.is_static_lifetime && + !lib.is_symbol_internal_symbol(symbol, out)) + { + relevant_expressions.insert(symbol_exprt(symbol.name, symbol.type)); + } + } + return; +} + +static void get_locals( + std::set &relevant_expressions, + const goto_programt &goto_program, + const namespacet &ns) +{ + goto_programt::decl_identifierst locals; + goto_program.get_decl_identifiers(locals); + for(const auto &identifier : locals) + { + const symbolt &symbol = ns.lookup(identifier); + relevant_expressions.insert(symbol_exprt(identifier, symbol.type)); + } + return; +} + +static void get_arguments( + std::set &relevant_expressions, + const irep_idt function_name, + const namespacet &ns) +{ + const symbolt &symbol = ns.lookup(function_name); + const code_typet &type = to_code_type(symbol.type); + + for(const auto ¶m : type.parameters()) + { + relevant_expressions.insert( + symbol_exprt(param.get_identifier(), param.type())); + } + return; +} + +static void static_instrument_goto_program( + const irep_idt function_name, + goto_programt &goto_program, + symbol_tablet &symbol_table, + const namespacet &ns, + const ai_baset &ai, + const instrument_configt &config, + message_handlert &message_handler) +{ + // Get the locations to instrument + auto targets = get_instrumentation_locations(goto_program, config); + + // The state may contain information about variables from other + // scopes, such as the caller which are true but putting them into + // instrumentation can cause problems. So gather the local + // variables. + std::set relevant_expressions; + get_globals(relevant_expressions, ns); + get_locals(relevant_expressions, goto_program, ns); + get_arguments(relevant_expressions, function_name, ns); + // TODO : for pointer variables p, add *p? + // TODO : rename whatever#return to __CPROVER_return_value + + // For each of them + for(const auto &t : targets) + { + goto_programt::targett i_it = t.first; + instrument_actiont action = t.second.first; + const std::string &reason = *(t.second.second); + + messaget m(message_handler); + m.status() << "Instruction " << i_it->location_number << " because " + << reason << "... "; // No EOM + + // Generate the expression + exprt instrument_expression = + compute_instrumentation_expression(i_it, ai, ns, relevant_expressions, m); + m.status() << "condition is " << format(instrument_expression) + << "... "; // No EOM + + // Insert it! + goto_programt::targett current = i_it; + goto_program.insert_before_swap(i_it); + + if(action == instrument_actiont::ASSUME) + { + *current = goto_programt::make_assumption(instrument_expression); + m.progress() << "added as assumption" << messaget::eom; + } + else if(action == instrument_actiont::ASSERT) + { + *current = goto_programt::make_assertion(instrument_expression); + m.progress() << "added as assertion" << messaget::eom; + } + else + { + UNREACHABLE; + } + current->source_location_nonconst() = i_it->source_location(); + } + + if(config.requires || config.ensures) + { + messaget m(message_handler); + + symbolt *symbol = symbol_table.get_writeable(function_name); + auto code = to_code_with_contract_type(symbol->type); + + if(config.requires) + { + m.status() << "Add requires contract... "; + exprt instrument_expression = compute_instrumentation_expression( + goto_program.instructions.begin(), ai, ns, relevant_expressions, m); + m.status() << "condition is " << format(instrument_expression) + << "... "; // No EOM + + code.c_requires().push_back(instrument_expression); + m.progress() << "added as contract" << messaget::eom; + } + if(config.ensures) + { + m.status() << "Add ensures contract... "; + auto i_it = goto_program.instructions.end(); + --i_it; + exprt instrument_expression = compute_instrumentation_expression( + i_it, ai, ns, relevant_expressions, m); + m.status() << "condition is " << format(instrument_expression) + << "... "; // No EOM + + code.c_requires().push_back(instrument_expression); + m.progress() << "added as contract" << messaget::eom; + } + + // Write back the annotated type + symbol->type = code; + } + + goto_program.update(); // Make sure the references are correct. + return; +} + +void static_instrument_goto_model( + goto_modelt &goto_model, + const ai_baset &ai, + const instrument_configt &config, + message_handlert &message_handler) +{ + messaget m(message_handler); + m.status() << "Instrumenting goto_model" << messaget::eom; + + const namespacet ns(goto_model.symbol_table); + + for(auto &gf_entry : goto_model.goto_functions.function_map) + { + if(!gf_entry.second.body_available()) + { + m.progress() << "Not instrumenting " << gf_entry.first + << " because it has no body" << messaget::eom; + } + else + { + m.progress() << "Instrumenting " << gf_entry.first << messaget::eom; + + static_instrument_goto_program( + gf_entry.first, + gf_entry.second.body, + goto_model.symbol_table, + ns, + ai, + config, + message_handler); + } + } + + return; +} + +/// Uses the domain to_predicate method to generate ASSUMEs or ASSERTs. +/// \param goto_model: the program analyzed +/// \param ai: the abstract interpreter after it has been run to fix point +/// \param options: the parsed user options +/// \param message_handler: the system message handler +/// \param out: output stream for the instrumented program +/// \return false on success with the instrumented program to out +bool static_instrument( + goto_modelt &goto_model, + const ai_baset &ai, + const std::string &configuration_string, + message_handlert &message_handler, + std::ostream &out) +{ + instrument_configt config(configuration_string); + + static_instrument_goto_model(goto_model, ai, config, message_handler); + + messaget m(message_handler); + m.status() << "Writing goto binary" << messaget::eom; + + restore_returns(goto_model); // restore return types before writing the binary + goto_model.goto_functions.update(); // Make sure the references are correct. + + namespacet ns(goto_model.symbol_table); + return write_goto_binary( + out, ns.get_symbol_table(), goto_model.goto_functions); +} diff --git a/src/goto-analyzer/static_instrument.h b/src/goto-analyzer/static_instrument.h new file mode 100644 index 00000000000..86a918ec754 --- /dev/null +++ b/src/goto-analyzer/static_instrument.h @@ -0,0 +1,73 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_ANALYZER_STATIC_INSTRUMENT_H +#define CPROVER_GOTO_ANALYZER_STATIC_INSTRUMENT_H + +#include + +// What kind of instrumentation to add +enum class instrument_actiont +{ + NOTHING, + ASSERT, + ASSUME +}; + +// What kind of instrumentation to add at each location +struct instrument_configt +{ +public: + instrument_actiont function_start; + instrument_actiont function_end; + instrument_actiont function_call; + instrument_actiont function_return; + instrument_actiont any_goto_target; + instrument_actiont backwards_goto_target; + instrument_actiont after_goto_not_taken; + bool requires; + bool ensures; + + instrument_configt() + : function_start(instrument_actiont::NOTHING), + function_end(instrument_actiont::NOTHING), + function_call(instrument_actiont::NOTHING), + function_return(instrument_actiont::NOTHING), + any_goto_target(instrument_actiont::NOTHING), + backwards_goto_target(instrument_actiont::NOTHING), + after_goto_not_taken(instrument_actiont::NOTHING), + requires(false), + ensures(false) + { + } + + // Parse from an option string + explicit instrument_configt(const std::string &opts); +}; + +class ai_baset; +class goto_modelt; +class message_handlert; +class optionst; + +// For using this functionality in other tools +void static_instrument_goto_model( + goto_modelt &, + const ai_baset &, + const instrument_configt &, + message_handlert &); + +// As used in goto-analyze +bool static_instrument( + goto_modelt &, + const ai_baset &, + const std::string &configuration_string, + message_handlert &, + std::ostream &); + +#endif // CPROVER_GOTO_ANALYZER_STATIC_INSTRUMENT_H