Function contracts: use call_grapht to detect local static variables,

add INVARIANT for recursive functions and PRECONDITION for function
pointers.

- A symbol is detected as a local static if it is static and declared in
one of the functions called by the function under analysis.
- `code_contractst::check_frame_conditions_function` errors out on
recursive functions
- `call_grapht::forall_callsites` now errors out on function pointers.

Author: Remi Delmas

regression/contracts/assigns_enforce_detect_local_statics/main.c

@@ -0,0 +1,31 @@
+#include <assert.h>
+#include <stdlib.h>
+
+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();
+}

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.

regression/contracts/assigns_enforce_statics/main.c

@@ -1,15 +1,15 @@
-#include <assert.h>
-#include <stdlib.h>
-
-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)++;
 }
 

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.

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.

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.

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).
+Test should fail because a recursive function is found during inlining.

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).
+Test should fail because a recursive function is found during inlining.

regression/contracts/function-calls-recursive-01/main.c

@@ -0,0 +1,23 @@
+#include <stdlib.h>
+
+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;
+}

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.

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

src/goto-instrument/contracts/assigns.cpp

@@ -15,6 +15,8 @@ Date: July 2021
 
 #include <langapi/language_util.h>
 
+#include <analyses/call_graph.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
@@ -192,3 +194,32 @@ 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());
+      }
+    }
+  }
+  return;
+}

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;