From 5fb8ee5f50060e5b8da31f78c9012f3e634c4da2 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Mon, 8 Nov 2021 18:14:46 +0000 Subject: [PATCH] Function contracts: detect static local variables using the function call graph add INVARIANT for recursive functions and PRECONDITION for function pointers. - Static local variables declared in functions called by the function under analysis are now added the write set (same for loops) - `code_contractst::check_frame_conditions_function` now errors out on recursive functions - `call_grapht::forall_callsites` now errors out on function pointers --- .../main.c | 31 +++++ .../test.desc | 14 ++ .../contracts/assigns_enforce_statics/main.c | 10 +- .../function-calls-03-1/test-enf-f1.desc | 20 +-- .../function-calls-03-1/test-enf-f2.desc | 21 +-- .../function-calls-04-1/test-enf-f1.desc | 21 +-- .../function-calls-04-1/test-enf-f2_in.desc | 22 +-- .../function-calls-04-1/test-enf-f2_out.desc | 22 +-- .../function-calls-recursive-01/main.c | 23 ++++ .../function-calls-recursive-01/test.desc | 12 ++ src/analyses/call_graph.cpp | 10 +- src/goto-instrument/contracts/assigns.cpp | 30 +++++ src/goto-instrument/contracts/assigns.h | 15 +++ src/goto-instrument/contracts/contracts.cpp | 125 ++++++++++++++++-- src/goto-instrument/contracts/contracts.h | 1 - 15 files changed, 278 insertions(+), 99 deletions(-) create mode 100644 regression/contracts/assigns_enforce_detect_local_statics/main.c create mode 100644 regression/contracts/assigns_enforce_detect_local_statics/test.desc create mode 100644 regression/contracts/function-calls-recursive-01/main.c create mode 100644 regression/contracts/function-calls-recursive-01/test.desc diff --git a/regression/contracts/assigns_enforce_detect_local_statics/main.c b/regression/contracts/assigns_enforce_detect_local_statics/main.c new file mode 100644 index 00000000000..3b637dd2f59 --- /dev/null +++ b/regression/contracts/assigns_enforce_detect_local_statics/main.c @@ -0,0 +1,31 @@ +#include +#include + +static int x; +static int xx; + +void foo() +{ + int *y = &x; + int *yy = &xx; + + static int x; + // must pass (modifies local static) + x++; + + // must pass (modifies assignable global static ) + (*y)++; + + // must fail (modifies non-assignable global static) + (*yy)++; +} + +void bar() __CPROVER_assigns(x) +{ + foo(); +} + +int main() +{ + bar(); +} diff --git a/regression/contracts/assigns_enforce_detect_local_statics/test.desc b/regression/contracts/assigns_enforce_detect_local_statics/test.desc new file mode 100644 index 00000000000..9b0ea3f8b69 --- /dev/null +++ b/regression/contracts/assigns_enforce_detect_local_statics/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-contract bar +^EXIT=10$ +^SIGNAL=0$ +^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that \*yy is assignable: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Checks whether static local and global variables are correctly tracked +in assigns clause verification, accross subfunction calls. diff --git a/regression/contracts/assigns_enforce_statics/main.c b/regression/contracts/assigns_enforce_statics/main.c index 92f6f44afab..592d5b41c26 100644 --- a/regression/contracts/assigns_enforce_statics/main.c +++ b/regression/contracts/assigns_enforce_statics/main.c @@ -1,15 +1,15 @@ -#include -#include - -static int x; +static int x = 0; void foo() __CPROVER_assigns(x) { int *y = &x; - static int x; + static int x = 0; + + // should pass (assigns local x) x++; + // should fail (assigns global x) (*y)++; } diff --git a/regression/contracts/function-calls-03-1/test-enf-f1.desc b/regression/contracts/function-calls-03-1/test-enf-f1.desc index e9263c77982..b4074b3fae9 100644 --- a/regression/contracts/function-calls-03-1/test-enf-f1.desc +++ b/regression/contracts/function-calls-03-1/test-enf-f1.desc @@ -1,20 +1,12 @@ CORE main.c --enforce-contract f1 _ --unwind 20 --unwinding-assertions -^EXIT=10$ +^file main\.c line 13 function f2: recursion is ignored on call to 'f2'$ +^Invariant check failed$ +^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$ +^Reason: Recursive functions found during inlining$ +^EXIT=(127|134|137)$ ^SIGNAL=0$ -^file main.c line \d+ function f2: recursion is ignored on call to \'f2\'$ -^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$ -^VERIFICATION FAILED$ -- -- -Verification: - function | pre-cond | post-cond - ---------|----------|---------- - f1 | assumed | asserted - -Test should fail: -The postcondition of f2 is incorrect, considering the recursion particularity. - -Recursion: -The base case for the recursive call to f2 provides different behavior than the common case (given the pre-conditions). +Test should fail because a recursive function is found during inlining. diff --git a/regression/contracts/function-calls-03-1/test-enf-f2.desc b/regression/contracts/function-calls-03-1/test-enf-f2.desc index 040242243ff..8adfa3f0afd 100644 --- a/regression/contracts/function-calls-03-1/test-enf-f2.desc +++ b/regression/contracts/function-calls-03-1/test-enf-f2.desc @@ -1,21 +1,12 @@ CORE main.c --enforce-contract f2 _ --unwind 20 --unwinding-assertions -^EXIT=10$ +^file main\.c line 13 function f2: recursion is ignored on call to 'f2'$ +^Invariant check failed$ +^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$ +^Reason: Recursive functions found during inlining$ +^EXIT=(127|134|137)$ ^SIGNAL=0$ -^file main.c line \d+ function f2: recursion is ignored on call to \'f2\'$ -^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$ -^\[f2.\d+\] line \d+ Check that loc is assignable: SUCCESS$ -^VERIFICATION FAILED$ -- -- -Verification: - function | pre-cond | post-cond - ---------|----------|---------- - f2 | assumed | asserted - -Test should fail: -The postcondition of f2 is incorrect, considering the recursion particularity. - -Recursion: -The base case for the recursive call to f2 provides different behavior than the common case (given the pre-conditions). +Test should fail because a recursive function is found during inlining. diff --git a/regression/contracts/function-calls-04-1/test-enf-f1.desc b/regression/contracts/function-calls-04-1/test-enf-f1.desc index 6749c892087..05550b8a420 100644 --- a/regression/contracts/function-calls-04-1/test-enf-f1.desc +++ b/regression/contracts/function-calls-04-1/test-enf-f1.desc @@ -1,21 +1,12 @@ CORE main.c --enforce-contract f1 _ --unwind 20 --unwinding-assertions -^EXIT=10$ +^file main\.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$ +^Invariant check failed$ +^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$ +^Reason: Recursive functions found during inlining$ +^EXIT=(127|134|137)$ ^SIGNAL=0$ -^file main.c line \d+ function f2\_in: recursion is ignored on call to \'f2\_out\'$ -^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$ -^VERIFICATION FAILED$ -- -- -Verification: - function | pre-cond | post-cond - ---------|----------|---------- - f1 | assumed | asserted - -Test should fail: -The postcondition of f2_out is incorrect, considering the recursion particularity. - -Recursion: -The base case for the recursive call to f2_out provides different behavior -than the general case (given the pre-conditions). +Test should fail because a recursive function is found during inlining. diff --git a/regression/contracts/function-calls-04-1/test-enf-f2_in.desc b/regression/contracts/function-calls-04-1/test-enf-f2_in.desc index c9a40b7b577..21bafb9a4ef 100644 --- a/regression/contracts/function-calls-04-1/test-enf-f2_in.desc +++ b/regression/contracts/function-calls-04-1/test-enf-f2_in.desc @@ -1,22 +1,12 @@ CORE main.c --enforce-contract f2_in _ --unwind 20 --unwinding-assertions -^EXIT=10$ +^file main\.c line 13 function f2_out: recursion is ignored on call to 'f2_in'$ +^Invariant check failed$ +^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$ +^Reason: Recursive functions found during inlining$ +^EXIT=(127|134|137)$ ^SIGNAL=0$ -^file main.c line \d+ function f2\_out: recursion is ignored on call to \'f2\_in\'$ -^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$ -^\[f2\_out.\d+\] line \d+ Check that loc2 is assignable: SUCCESS$ -^VERIFICATION FAILED$ -- -- -Verification: - function | pre-cond | post-cond - ---------|----------|---------- - f2_in | assumed | asserted - -Test should fail: -The postcondition of f2_out is incorrect, considering the recursion particularity. - -Recursion: -The base case for the recursive call to f2_out provides different behavior -than the general case (given the pre-conditions). \ No newline at end of file +Test should fail because a recursive function is found during inlining. diff --git a/regression/contracts/function-calls-04-1/test-enf-f2_out.desc b/regression/contracts/function-calls-04-1/test-enf-f2_out.desc index 87d39ca64d4..2d5c000f3b3 100644 --- a/regression/contracts/function-calls-04-1/test-enf-f2_out.desc +++ b/regression/contracts/function-calls-04-1/test-enf-f2_out.desc @@ -1,22 +1,12 @@ CORE main.c --enforce-contract f2_out _ --unwind 20 --unwinding-assertions -^EXIT=10$ +^file main\.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$ +^Invariant check failed$ +^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$ +^Reason: Recursive functions found during inlining$ +^EXIT=(127|134|137)$ ^SIGNAL=0$ -^file main.c line \d+ function f2\_in: recursion is ignored on call to \'f2\_out\'$ -^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$ -^\[f2\_out.\d+\] line \d+ Check that loc2 is assignable: SUCCESS$ -^VERIFICATION FAILED$ -- -- -Verification: - function | pre-cond | post-cond - ---------|----------|---------- - f2_out | assumed | asserted - -Test should fail: -The postcondition of f2 is incorrect, considering the recursion particularity. - -Recursion: -The base case for the recursive call to f2_out provides different behavior -than the general case (given the pre-conditions). \ No newline at end of file +Test should fail because a recursive function is found during inlining. diff --git a/regression/contracts/function-calls-recursive-01/main.c b/regression/contracts/function-calls-recursive-01/main.c new file mode 100644 index 00000000000..b69a675e874 --- /dev/null +++ b/regression/contracts/function-calls-recursive-01/main.c @@ -0,0 +1,23 @@ +#include + +int sum_rec(int i, int acc) +{ + if(i >= 0) + return sum_rec(i - 1, acc + i); + return acc; +} + +int sum(int i) __CPROVER_requires(0 <= i && i <= 50) + __CPROVER_ensures(__CPROVER_return_value >= 0) __CPROVER_assigns() +{ + int j = i; + int res = sum_rec(j, 0); + return res; +} + +int main() +{ + int result = sum(10); + __CPROVER_assert(result == 55, "result == 55"); + return 0; +} diff --git a/regression/contracts/function-calls-recursive-01/test.desc b/regression/contracts/function-calls-recursive-01/test.desc new file mode 100644 index 00000000000..ef1a4b1df44 --- /dev/null +++ b/regression/contracts/function-calls-recursive-01/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--enforce-contract sum _ --trace +^file main\.c line 6 function sum_rec: recursion is ignored on call to 'sum_rec'$ +^Invariant check failed$ +^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$ +^Reason: Recursive functions found during inlining$ +^EXIT=(127|134|137)$ +^SIGNAL=0$ +-- +-- +Test should fail because a recursive function is found during inlining. diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp index 3194d30349b..93278523c02 100644 --- a/src/analyses/call_graph.cpp +++ b/src/analyses/call_graph.cpp @@ -58,11 +58,11 @@ static void forall_callsites( if(i_it->is_function_call()) { const exprt &function_expr = i_it->call_function(); - if(function_expr.id()==ID_symbol) - { - const irep_idt &callee=to_symbol_expr(function_expr).get_identifier(); - call_task(i_it, callee); - } + PRECONDITION_WITH_DIAGNOSTICS( + function_expr.id() == ID_symbol, + "call graph computation requires function pointer removal"); + const irep_idt &callee = to_symbol_expr(function_expr).get_identifier(); + call_task(i_it, callee); } } } diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index ac87d9c4a35..c4e0ba536f9 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -13,6 +13,8 @@ Date: July 2021 #include "assigns.h" +#include + #include #include @@ -196,3 +198,31 @@ void havoc_assigns_targetst::append_havoc_code_for_expr( 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 index bdc97ead1d9..f076a632feb 100644 --- a/src/goto-instrument/contracts/assigns.h +++ b/src/goto-instrument/contracts/assigns.h @@ -87,6 +87,21 @@ class assigns_clauset 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); + const messaget &log; const namespacet &ns; const irep_idt &function_name; diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 1f1cea11320..1808bce1e96 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -29,6 +29,7 @@ Date: February 2016 #include #include +#include #include #include #include @@ -37,10 +38,98 @@ Date: February 2016 #include #include #include +#include #include "memory_predicates.h" #include "utils.h" +/// Decorator for \ref message_handlert that keeps track of warnings +/// occuring when inlining a function. +/// +/// It counts the number of : +/// - recursive functions warnings +/// - missing functions warnings +/// - missing function body warnings +/// - missing function arguments warnings +class inlining_decoratort : public message_handlert +{ +private: + message_handlert &wrapped; + unsigned int recursive_function_warnings_count = 0; + + void parse_message(const std::string &message) + { + if(message.find("recursion is ignored on call") != std::string::npos) + recursive_function_warnings_count++; + } + +public: + explicit inlining_decoratort(message_handlert &_wrapped) : wrapped(_wrapped) + { + } + + unsigned int get_recursive_function_warnings_count() + { + return recursive_function_warnings_count; + } + + void print(unsigned level, const std::string &message) override + { + parse_message(message); + wrapped.print(level, message); + } + + void print(unsigned level, const xmlt &xml) override + { + wrapped.print(level, xml); + } + + void print(unsigned level, const jsont &json) override + { + wrapped.print(level, json); + } + + void print(unsigned level, const structured_datat &data) override + { + wrapped.print(level, data); + } + + void print( + unsigned level, + const std::string &message, + const source_locationt &location) override + { + parse_message(message); + wrapped.print(level, message, location); + return; + } + + void flush(unsigned i) override + { + return wrapped.flush(i); + } + + void set_verbosity(unsigned _verbosity) + { + wrapped.set_verbosity(_verbosity); + } + + unsigned get_verbosity() const + { + return wrapped.get_verbosity(); + } + + std::size_t get_message_count(unsigned level) const + { + return wrapped.get_message_count(level); + } + + std::string command(unsigned i) const override + { + return wrapped.command(i); + } +}; + void code_contractst::check_apply_loop_contracts( const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, @@ -70,6 +159,8 @@ void code_contractst::check_apply_loop_contracts( assigns_clauset loop_assigns( assigns.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.is_nil()) @@ -688,9 +779,14 @@ void code_contractst::apply_loop_contract( if(!natural_loops.loop_map.size()) return; + inlining_decoratort decorated(log.get_message_handler()); goto_function_inline( goto_functions, function_name, ns, log.get_message_handler()); + INVARIANT( + decorated.get_recursive_function_warnings_count() == 0, + "Recursive functions found during inlining"); + // A graph node type that stores information about a loop. // We create a DAG representing nesting of various loops in goto_function, // sort them topologically, and instrument them in the top-sorted order. @@ -985,18 +1081,13 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) function, symbol_table); - // Adds formal parameters to write set + // detect and add static local variables + assigns.add_static_locals_to_write_set(goto_functions, function); + + // 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()); - // Adds local static declarations to write set - for(const auto &sym_pair : symbol_table) - { - const auto &sym = sym_pair.second; - if(sym.is_static_lifetime && sym.location.get_function() == function) - assigns.add_to_write_set(sym.symbol_expr()); - } - auto instruction_it = function_obj->second.body.instructions.begin(); for(const auto &car : assigns.get_write_set()) { @@ -1005,9 +1096,19 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) function_obj->second.body, instruction_it, snapshot_instructions); }; - // Inline all function calls. - goto_function_inline( - goto_functions, function_obj->first, ns, log.get_message_handler()); + // Full inlining of the function body + // Inlining is performed so that function calls to a same function + // occurring under different write sets get instrumented specifically + // for each write set + inlining_decoratort decorated(log.get_message_handler()); + goto_function_inline(goto_functions, function, ns, decorated); + + INVARIANT( + decorated.get_recursive_function_warnings_count() == 0, + "Recursive functions found during inlining"); + + // restore internal invariants + goto_functions.update(); // Insert write set inclusion checks. check_frame_conditions( diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 08cc0080571..6514aada79e 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -58,7 +58,6 @@ class code_contractst goto_functions(goto_model.goto_functions), log(log), converter(symbol_table, log.get_message_handler()) - { }