Merge pull request #8412 from tautschnig/library-is-compiled

Library functions: mark them as compiled

Author: tautschnig

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 --sat-solver cadical "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}

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;
 }

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$

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}

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."

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.

src/ansi-c/goto-conversion/link_to_library.cpp

@@ -41,26 +41,36 @@ 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);
+    // this function is now included in goto_functions, no need to re-convert
+    // should the goto binary be reloaded
+    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);
+    // this function is now included in goto_functions, no need to re-convert
+    // should the goto binary be reloaded
+    goto_model.symbol_table.get_writeable_ref(missing_function).set_compiled();
   }
 
   // check whether additional initialization may be required

src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp

@@ -326,6 +326,7 @@ void dfcc_libraryt::load(std::set<irep_idt> &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

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<cext> cegis_verifiert::verify()
@@ -569,10 +565,12 @@ std::optional<cext> 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.