From 1e687f6a11b1dff46237b8e683a4595fdc7998b1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Aug 2024 15:16:17 +0000 Subject: [PATCH] Library functions: mark them as compiled When adding library functions to the goto model we no longer need their function bodies as values in the symbol table. Marking them as "compiled" will make sure we don't re-convert them in any subsequent run (e.g., running cbmc after goto-instrument). Doing so would undo any application of "drop-unused-functions." This was most notable with contracts/dynamic frames, where we ended up reporting thousands of properties as "SUCCESS" in library functions that were never actually called. For some contracts examples this now reduces the number of properties reported from over a thousand to tens of properties, and in other cases this made apparent that we were spuriously reporting "SUCCESS" when we never actually invoked those functions in the first place. --- regression/contracts-dfcc/chain.sh | 3 ++ .../contracts/assigns_enforce_03/main.c | 5 ++++ .../contracts/assigns_enforce_03/test.desc | 24 ++++++++-------- regression/contracts/chain.sh | 3 ++ .../loop.desc | 27 ++++++++++++++++++ .../test.desc | 28 +++---------------- .../goto-conversion/link_to_library.cpp | 10 +++++-- .../contracts/dynamic-frames/dfcc_library.cpp | 1 + src/goto-synthesizer/cegis_verifier.cpp | 14 ++++------ 9 files changed, 69 insertions(+), 46 deletions(-) create mode 100644 regression/contracts/variant_multidimensional_ackermann/loop.desc diff --git a/regression/contracts-dfcc/chain.sh b/regression/contracts-dfcc/chain.sh index c388dc26c914..54829580e44f 100755 --- a/regression/contracts-dfcc/chain.sh +++ b/regression/contracts-dfcc/chain.sh @@ -58,5 +58,8 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then rm "${name}${dfcc_suffix}-mod.c" fi +if ! echo "${args_cbmc}" | grep -q -- --function ; then + $goto_instrument --drop-unused-functions "${name}${dfcc_suffix}-mod.gb" "${name}${dfcc_suffix}-mod.gb" +fi $goto_instrument --show-goto-functions "${name}${dfcc_suffix}-mod.gb" $cbmc "${name}${dfcc_suffix}-mod.gb" ${args_cbmc} diff --git a/regression/contracts/assigns_enforce_03/main.c b/regression/contracts/assigns_enforce_03/main.c index 433eab010498..295b23fbd5fa 100644 --- a/regression/contracts/assigns_enforce_03/main.c +++ b/regression/contracts/assigns_enforce_03/main.c @@ -1,3 +1,6 @@ +void f2(int *, int *, int *); +void f3(int *, int *, int *); + void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1) { f2(x1, y1, z1); @@ -22,6 +25,8 @@ int main() int q = 2; int r = 3; f1(&p, &q, &r); + f2(&p, &q, &r); + f3(&p, &q, &r); return 0; } diff --git a/regression/contracts/assigns_enforce_03/test.desc b/regression/contracts/assigns_enforce_03/test.desc index 4b342024cc93..1a2be3f0e630 100644 --- a/regression/contracts/assigns_enforce_03/test.desc +++ b/regression/contracts/assigns_enforce_03/test.desc @@ -1,18 +1,18 @@ 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$ +^\[f1.assigns.\d+\] line 4 Check that \*x1 is valid: SUCCESS$ +^\[f1.assigns.\d+\] line 4 Check that \*y1 is valid: SUCCESS$ +^\[f1.assigns.\d+\] line 4 Check that \*z1 is valid: SUCCESS$ +^\[f2.assigns.\d+\] line 9 Check that \*x2 is valid: SUCCESS$ +^\[f2.assigns.\d+\] line 9 Check that \*y2 is valid: SUCCESS$ +^\[f2.assigns.\d+\] line 9 Check that \*z2 is valid: SUCCESS$ +^\[f3.assigns.\d+\] line 14 Check that \*x3 is valid: SUCCESS$ +^\[f3.assigns.\d+\] line 14 Check that \*y3 is valid: SUCCESS$ +^\[f3.assigns.\d+\] line 15 Check that \*z3 is valid: SUCCESS$ +^\[f3.assigns.\d+\] line 17 Check that \*x3 is assignable: SUCCESS$ +^\[f3.assigns.\d+\] line 18 Check that \*y3 is assignable: SUCCESS$ +^\[f3.assigns.\d+\] line 19 Check that \*z3 is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts/chain.sh b/regression/contracts/chain.sh index 37aa18a35b53..0cfcbb3fe20d 100755 --- a/regression/contracts/chain.sh +++ b/regression/contracts/chain.sh @@ -41,5 +41,8 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then rm "${name}-mod.c" fi +if ! echo "${args_cbmc}" | grep -q -- --function ; then + $goto_instrument --drop-unused-functions "${name}-mod.gb" "${name}-mod.gb" +fi $goto_instrument --show-goto-functions "${name}-mod.gb" $cbmc "${name}-mod.gb" ${args_cbmc} diff --git a/regression/contracts/variant_multidimensional_ackermann/loop.desc b/regression/contracts/variant_multidimensional_ackermann/loop.desc new file mode 100644 index 000000000000..82af4451f1af --- /dev/null +++ b/regression/contracts/variant_multidimensional_ackermann/loop.desc @@ -0,0 +1,27 @@ +CORE +main.c +--apply-loop-contracts +^\[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.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 35 Check that m is assignable: SUCCESS$ +^\[ackermann.overflow.\d+] line 39 arithmetic overflow on signed \+ in n \+ 1: FAILURE$ +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +It tests whether we can prove (only partially) the termination of the Ackermann +function using a multidimensional decreases clause. + +Note that this particular implementation of the Ackermann function contains +both a while-loop and recursion. Therefore, to fully prove the termination of +the Ackermann function, we must prove both +(i) the termination of the while-loop and +(ii) the termination of the recursion. +Because CBMC does not support termination proofs of recursions (yet), we cannot +prove the latter, but the former. Hence, the termination proof in the code is +only "partial." diff --git a/regression/contracts/variant_multidimensional_ackermann/test.desc b/regression/contracts/variant_multidimensional_ackermann/test.desc index 213f347ed885..aa9cf7ddedca 100644 --- a/regression/contracts/variant_multidimensional_ackermann/test.desc +++ b/regression/contracts/variant_multidimensional_ackermann/test.desc @@ -1,38 +1,18 @@ CORE main.c ---apply-loop-contracts --replace-call-with-contract ackermann +--replace-call-with-contract ackermann ^\[ackermann.precondition\.\d+\] line \d+ Check requires clause of ackermann in main: SUCCESS$ -^\[ackermann.precondition\.\d+\] line \d+ Check requires clause of ackermann in ackermann: SUCCESS$ -^\[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.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$ -- -- -It tests whether we can prove (only partially) the termination of the Ackermann -function using a multidimensional decreases clause. - -Note that this particular implementation of the Ackermann function contains -both a while-loop and recursion. Therefore, to fully prove the termination of -the Ackermann function, we must prove both -(i) the termination of the while-loop and -(ii) the termination of the recursion. -Because CBMC does not support termination proofs of recursions (yet), we cannot -prove the latter, but the former. Hence, the termination proof in the code is -only "partial." - -Furthermore, the Ackermann function has a function contract that the result +The Ackermann function has a function contract that the result is always non-negative. This post-condition is necessary for establishing the loop invariant. However, in this test, we do not enforce the function contract. Instead, we assume that the function contract is correct and use it -(i.e. replace a recursive call of the Ackermann function with its contract). +(i.e. replace a recursive call of the Ackermann function with its contract). We cannot verify/enforce the function contract of the Ackermann function, since CBMC does not support function contracts for recursively defined functions. -As of now, CBMC only supports function contracts for non-recursive functions. +As of now, CBMC only supports function contracts for non-recursive functions. diff --git a/src/ansi-c/goto-conversion/link_to_library.cpp b/src/ansi-c/goto-conversion/link_to_library.cpp index cc814e1965ad..8cdd5dcfd36e 100644 --- a/src/ansi-c/goto-conversion/link_to_library.cpp +++ b/src/ansi-c/goto-conversion/link_to_library.cpp @@ -41,26 +41,32 @@ add_one_function( // convert to CFG if( library_model.symbol_table.symbols.find(missing_function) != - library_model.symbol_table.symbols.end()) + library_model.symbol_table.symbols.end() && + library_model.symbol_table.lookup_ref(missing_function).value.is_not_nil()) { goto_convert( missing_function, library_model.symbol_table, library_model.goto_functions, message_handler); + library_model.symbol_table.get_writeable_ref(missing_function) + .set_compiled(); } // We might need a function that's outside our own library, but brought in via // some header file included by the library. Those functions already exist in // goto_model.symbol_table, but haven't been converted just yet. else if( goto_model.symbol_table.symbols.find(missing_function) != - goto_model.symbol_table.symbols.end()) + goto_model.symbol_table.symbols.end() && + goto_model.symbol_table.lookup_ref(missing_function).value.is_not_nil() && + !goto_model.symbol_table.lookup_ref(missing_function).is_compiled()) { goto_convert( missing_function, goto_model.symbol_table, library_model.goto_functions, message_handler); + goto_model.symbol_table.get_writeable_ref(missing_function).set_compiled(); } // check whether additional initialization may be required diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index 63c4d8046008..242b330b4d30 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -326,6 +326,7 @@ void dfcc_libraryt::load(std::set &to_instrument) { goto_convert( id, goto_model.symbol_table, goto_model.goto_functions, message_handler); + goto_model.symbol_table.get_writeable_ref(id).set_compiled(); } // check that all symbols have a goto_implementation diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 8d5a8ef282c9..dd32b5eec57d 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -546,12 +546,8 @@ cext cegis_verifiert::build_cex( void cegis_verifiert::restore_functions() { - for(const auto &fun_entry : goto_model.goto_functions.function_map) - { - irep_idt fun_name = fun_entry.first; - goto_model.goto_functions.function_map[fun_name].body.swap( - original_functions[fun_name]); - } + for(auto &[fun_name, orig_fun_body] : original_functions) + goto_model.goto_functions.function_map[fun_name].body.swap(orig_fun_body); } std::optional cegis_verifiert::verify() @@ -569,10 +565,12 @@ std::optional cegis_verifiert::verify() // 3. construct the formatted counterexample from the violated property and // its trace. - // Store the original functions. We will restore them after the verification. + // Store the original functions when they have a body (library functions might + // not yet have one). We will restore them after the verification. for(const auto &fun_entry : goto_model.goto_functions.function_map) { - original_functions[fun_entry.first].copy_from(fun_entry.second.body); + if(fun_entry.second.body_available()) + original_functions[fun_entry.first].copy_from(fun_entry.second.body); } // Annotate the candidates to the goto_model for checking.