Fixes local static variables detection. A symbol is detected as a local static

if it is static and declared in one of the subfunctions of the function under analysis.

Author: Remi Delmas

regression/contracts/assigns_enforce_statics/main.c

@@ -1,15 +1,18 @@
 #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/assigns_enforce_statics_subfunctions/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_statics_subfunctions/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-contract bar _ --pointer-primitive-check
+^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.

src/goto-instrument/contracts/contracts.cpp

@@ -15,7 +15,10 @@ Date: February 2016
 
 #include <algorithm>
 #include <map>
+#include <util/find_symbols.h>
+#include <util/std_code.h>
 
+#include <analyses/call_graph.h>
 #include <analyses/local_may_alias.h>
 
 #include <ansi-c/c_expr.h>
@@ -853,18 +856,16 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
     function,
     symbol_table);
 
-  // Adds formal parameters to write set
+  // fetch local statics of all subfunctions in the symbol_table
+  find_static_locals(goto_functions, function, assigns);
+
+  // Full inlining of the function body
+  goto_function_inline(goto_functions, function, ns, log.get_message_handler());
+
+  // Add formal parameters to write set
   for(const auto &param : 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())
   {
@@ -886,8 +887,6 @@ void code_contractst::check_frame_conditions(
   goto_programt::targett &instruction_it,
   assigns_clauset &assigns)
 {
-  goto_function_inline(goto_functions, function, ns, log.get_message_handler());
-
   for(; instruction_it != body.instructions.end(); ++instruction_it)
   {
     if(instruction_it->is_decl())
@@ -1260,3 +1259,34 @@ bool code_contractst::enforce_contracts(const std::set<std::string> &to_enforce)
   }
   return fail;
 }
+
+void code_contractst::find_static_locals(
+  const goto_functionst &functions,
+  const irep_idt &root_function,
+  assigns_clauset &assigns)
+{
+  auto cg =
+    call_grapht::create_from_root_function(functions, root_function, true);
+  auto g = cg.get_directed_graph();
+
+  // 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)
+    {
+      auto fname = sym.location.get_function();
+      if(
+        !fname.empty() &&
+        (fname == root_function || g.get_node_index(fname).has_value()))
+      {
+        // the symbol has
+        // - a static lifetime
+        // - non empty location function
+        // - this function appears in the call graph of the function
+        assigns.add_to_write_set(sym.symbol_expr());
+      }
+    }
+  }
+  return;
+}

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())
-
   {
   }
 
@@ -210,6 +209,23 @@ class code_contractst
     codet &expression,
     source_locationt location,
     const irep_idt &mode);
+
+  /// \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 given `assigns`.
+  ///
+  /// @param functions all functions of the goto_model
+  /// @param root_function the root function under which to search statics
+  /// @param assigns assigns clause where search results are added
+  ///
+  /// 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 find_static_locals(
+    const goto_functionst &functions,
+    const irep_idt &root_function,
+    assigns_clauset &assigns);
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H