Handle functions with mangled names in contract replacement

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/assigns_replace_09/main.c

@@ -0,0 +1,19 @@
+#include <stdlib.h>
+
+int x;
+int *z = &x;
+
+void bar() __CPROVER_assigns(*z)
+{
+}
+
+static void foo() __CPROVER_assigns(*z)
+{
+  bar();
+}
+
+int main()
+{
+  foo();
+  return 0;
+}

regression/contracts/assigns_replace_09/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-call-with-contract bar
+^EXIT=0$
+^SIGNAL=0$
+\[\d+\] file main.c line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^Condition: \!not\_found$
+--
+Checks whether CBMC properly evaluates subset relationship on assigns
+during replacement with static functions.

src/goto-instrument/contracts/contracts.cpp

@@ -473,18 +473,19 @@ code_contractst::create_ensures_instruction(
 }
 
 bool code_contractst::apply_function_contract(
-  goto_programt &goto_program,
-  goto_programt::targett target)
+  const irep_idt &function,
+  goto_programt &function_body,
+  goto_programt::targett &target)
 {
   // Return if the function is not named in the call; currently we don't handle
   // function pointers.
-  PRECONDITION(as_const(*target).call_function().id() == ID_symbol);
+  PRECONDITION(as_const(target)->call_function().id() == ID_symbol);
 
   // Retrieve the function type, which is needed to extract the contract
   // components.
-  const irep_idt &function =
-    to_symbol_expr(as_const(*target).call_function()).get_identifier();
-  const symbolt &function_symbol = ns.lookup(function);
+  const irep_idt &target_function =
+    to_symbol_expr(as_const(target)->call_function()).get_identifier();
+  const symbolt &function_symbol = ns.lookup(target_function);
   const auto &type = to_code_with_contract_type(function_symbol.type);
 
   // Isolate each component of the contract.
@@ -499,15 +500,15 @@ bool code_contractst::apply_function_contract(
   if(type.return_type() != empty_typet())
   {
     // Check whether the function's return value is not disregarded.
-    if(as_const(*target).call_lhs().is_not_nil())
+    if(target->call_lhs().is_not_nil())
     {
       // If so, have it replaced appropriately.
       // For example, if foo() ensures that its return value is > 5, then
       // rewrite calls to foo as follows:
       // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
       symbol_exprt ret_val(
-        CPROVER_PREFIX "return_value", as_const(*target).call_lhs().type());
-      common_replace.insert(ret_val, as_const(*target).call_lhs());
+        CPROVER_PREFIX "return_value", as_const(target)->call_lhs().type());
+      common_replace.insert(ret_val, as_const(target)->call_lhs());
     }
     else
     {
@@ -521,10 +522,10 @@ bool code_contractst::apply_function_contract(
         // fresh variable to replace __CPROVER_return_value with.
         const symbolt &fresh = get_fresh_aux_symbol(
           type.return_type(),
-          id2string(function),
+          id2string(target_function),
           "ignored_return_value",
-          target->source_location,
-          symbol_table.lookup_ref(function).mode,
+          as_const(target)->source_location,
+          symbol_table.lookup_ref(target_function).mode,
           ns,
           symbol_table);
         symbol_exprt ret_val(CPROVER_PREFIX "return_value", type.return_type());
@@ -534,7 +535,7 @@ bool code_contractst::apply_function_contract(
   }
 
   // Replace formal parameters
-  const auto &arguments = target->call_arguments();
+  const auto &arguments = as_const(target)->call_arguments();
   auto a_it = arguments.begin();
   for(auto p_it = type.parameters().begin();
       p_it != type.parameters().end() && a_it != arguments.end();
@@ -551,9 +552,9 @@ bool code_contractst::apply_function_contract(
   // and only refer to the common symbols to be replaced.
   common_replace(assigns);
 
-  const auto &mode = symbol_table.lookup_ref(function).mode;
+  const auto &mode = symbol_table.lookup_ref(target_function).mode;
 
-  is_fresh_replacet is_fresh(*this, log, function);
+  is_fresh_replacet is_fresh(*this, log, target_function);
   is_fresh.create_declarations();
 
   // Insert assertion of the precondition immediately before the call site.
@@ -567,14 +568,14 @@ bool code_contractst::apply_function_contract(
     converter.goto_convert(
       code_assertt(requires),
       assertion,
-      symbol_table.lookup_ref(function).mode);
+      symbol_table.lookup_ref(target_function).mode);
     assertion.instructions.back().source_location = requires.source_location();
     assertion.instructions.back().source_location.set_comment(
       "Check requires clause");
     assertion.instructions.back().source_location.set_property_class(
       ID_precondition);
     is_fresh.update_requires(assertion);
-    insert_before_swap_and_advance(goto_program, target, assertion);
+    insert_before_swap_and_advance(function_body, target, assertion);
   }
 
   // Gather all the instructions required to handle history variables
@@ -590,11 +591,11 @@ bool code_contractst::apply_function_contract(
     ensures_pair = create_ensures_instruction(
       assumption,
       ensures.source_location(),
-      symbol_table.lookup_ref(function).mode);
+      symbol_table.lookup_ref(target_function).mode);
 
     // add all the history variable initialization instructions
     // to the goto program
-    insert_before_swap_and_advance(goto_program, target, ensures_pair.second);
+    insert_before_swap_and_advance(function_body, target, ensures_pair.second);
   }
 
   // Create a series of non-deterministic assignments to havoc the variables
@@ -604,9 +605,8 @@ bool code_contractst::apply_function_contract(
     assigns_clauset assigns_clause(assigns, log, ns);
 
     // Retrieve assigns clause of the caller function if exists.
-    const irep_idt &caller_function = target->source_location.get_function();
     auto caller_assigns =
-      to_code_with_contract_type(ns.lookup(caller_function).type).assigns();
+      to_code_with_contract_type(ns.lookup(function).type).assigns();
 
     if(caller_assigns.is_not_nil())
     {
@@ -617,31 +617,32 @@ bool code_contractst::apply_function_contract(
         caller_assigns_clause.generate_subset_check(assigns_clause),
         assigns_clause.location));
       subset_check_assertion.instructions.back().source_location.set_comment(
-        "Check that " + id2string(function) +
-        "'s assigns clause is a subset of " + id2string(caller_function) +
+        "Check that " + id2string(target_function) +
+        "'s assigns clause is a subset of " +
+        id2string(as_const(target)->source_location.get_function()) +
         "'s assigns clause");
       insert_before_swap_and_advance(
-        goto_program, target, subset_check_assertion);
+        function_body, target, subset_check_assertion);
     }
 
     // Havoc all targets in global write set
     auto assigns_havoc = assigns_clause.generate_havoc_code();
 
     // Insert the non-deterministic assignment immediately before the call site.
-    insert_before_swap_and_advance(goto_program, target, assigns_havoc);
+    insert_before_swap_and_advance(function_body, target, assigns_havoc);
   }
 
   // To remove the function call, insert statements related to the assumption.
   // Then, replace the function call with a SKIP statement.
   if(!ensures.is_false())
   {
     is_fresh.update_ensures(ensures_pair.first);
-    insert_before_swap_and_advance(goto_program, target, ensures_pair.first);
+    insert_before_swap_and_advance(function_body, target, ensures_pair.first);
   }
   *target = goto_programt::make_skip();
 
   // Add this function to the set of replaced functions.
-  summarized.insert(function);
+  summarized.insert(target_function);
   return false;
 }
 
@@ -1223,7 +1224,8 @@ bool code_contractst::replace_calls(const std::set<std::string> &functions)
         if(found == functions.end())
           continue;
 
-        fail |= apply_function_contract(goto_function.second.body, ins);
+        fail |= apply_function_contract(
+          goto_function.first, goto_function.second.body, ins);
       }
     }
   }

src/goto-instrument/contracts/contracts.h

@@ -195,8 +195,9 @@ class code_contractst
   /// non-deterministic assignments for the write set, and assumptions
   /// based on ensures clauses.
   bool apply_function_contract(
-    goto_programt &goto_program,
-    goto_programt::targett target);
+    const irep_idt &,
+    goto_programt &,
+    goto_programt::targett &);
 
   /// Instruments `wrapper_function` adding assumptions based on requires
   /// clauses and assertions based on ensures clauses.