Consistent order of parameters across contracts functions

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

src/goto-instrument/contracts/assigns.cpp

@@ -38,7 +38,6 @@ assigns_clause_targett::assigns_clause_targett(
   symbolt standin_symbol = contract.new_tmp_symbol(
     pointer_object.type(),
     function_symbol.location,
-    function_id,
     function_symbol.mode);
 
   local_target = standin_symbol.symbol_expr();

src/goto-instrument/contracts/contracts.cpp

@@ -51,7 +51,6 @@ exprt get_size(const typet &type, const namespacet &ns, messaget &log)
 
 void code_contractst::check_apply_loop_contracts(
   goto_functionst::goto_functiont &goto_function,
-  const irep_idt &function_name,
   const local_may_aliast &local_may_alias,
   const goto_programt::targett loop_head,
   const loopt &loop,
@@ -161,12 +160,10 @@ void code_contractst::check_apply_loop_contracts(
   for(const auto &clause : decreases_clause.operands())
   {
     old_temporary_variables.push_back(
-      new_tmp_symbol(
-        clause.type(), loop_head->source_location, function_name, mode)
+      new_tmp_symbol(clause.type(), loop_head->source_location, mode)
         .symbol_expr());
     new_temporary_variables.push_back(
-      new_tmp_symbol(
-        clause.type(), loop_head->source_location, function_name, mode)
+      new_tmp_symbol(clause.type(), loop_head->source_location, mode)
         .symbol_expr());
   }
 
@@ -396,14 +393,12 @@ void code_contractst::replace_old_parameter(
   exprt &expr,
   std::map<exprt, exprt> &parameter2history,
   source_locationt location,
-  const irep_idt &function,
   const irep_idt &mode,
   goto_programt &history)
 {
   for(auto &op : expr.operands())
   {
-    replace_old_parameter(
-      op, parameter2history, location, function, mode, history);
+    replace_old_parameter(op, parameter2history, location, mode, history);
   }
 
   if(expr.id() == ID_old)
@@ -425,8 +420,7 @@ void code_contractst::replace_old_parameter(
         // 1. Create a temporary symbol expression that represents the
         // history variable
         symbol_exprt tmp_symbol =
-          new_tmp_symbol(dereference_expr.type(), location, function, mode)
-            .symbol_expr();
+          new_tmp_symbol(dereference_expr.type(), location, mode).symbol_expr();
 
         // 2. Associate the above temporary variable to it's corresponding
         // expression
@@ -458,15 +452,13 @@ std::pair<goto_programt, goto_programt>
 code_contractst::create_ensures_instruction(
   codet &expression,
   source_locationt location,
-  const irep_idt &function,
   const irep_idt &mode)
 {
   std::map<exprt, exprt> parameter2history;
   goto_programt history;
 
   // Find and replace "old" expression in the "expression" variable
-  replace_old_parameter(
-    expression, parameter2history, location, function, mode, history);
+  replace_old_parameter(expression, parameter2history, location, mode, history);
 
   // Create instructions corresponding to the ensures clause
   goto_programt ensures_program;
@@ -479,7 +471,6 @@ code_contractst::create_ensures_instruction(
 }
 
 bool code_contractst::apply_function_contract(
-  const irep_idt &function_id,
   goto_programt &goto_program,
   goto_programt::targett target)
 {
@@ -603,7 +594,6 @@ bool code_contractst::apply_function_contract(
     ensures_pair = create_ensures_instruction(
       assumption,
       ensures.source_location(),
-      function,
       symbol_table.lookup_ref(function).mode);
 
     // add all the history variable initialization instructions
@@ -617,9 +607,9 @@ bool code_contractst::apply_function_contract(
   // in the assigns clause.
   if(assigns.is_not_nil())
   {
-    assigns_clauset assigns_cause(assigns, *this, function_id, log);
+    assigns_clauset assigns_cause(assigns, *this, function, log);
     goto_programt assigns_havoc = assigns_cause.havoc_code(
-      function_symbol.location, function_id, function_symbol.mode);
+      function_symbol.location, function, function_symbol.mode);
 
     // Insert the non-deterministic assignment immediately before the call site.
     std::size_t lines_to_iterate = assigns_havoc.instructions.size();
@@ -644,7 +634,7 @@ bool code_contractst::apply_function_contract(
 }
 
 void code_contractst::apply_loop_contract(
-  const irep_idt &function_name,
+  const irep_idt &function,
   goto_functionst::goto_functiont &goto_function)
 {
   local_may_aliast local_may_alias(goto_function);
@@ -656,23 +646,21 @@ void code_contractst::apply_loop_contract(
   {
     check_apply_loop_contracts(
       goto_function,
-      function_name,
       local_may_alias,
       loop.first,
       loop.second,
-      symbol_table.lookup_ref(function_name).mode);
+      symbol_table.lookup_ref(function).mode);
   }
 }
 
 const symbolt &code_contractst::new_tmp_symbol(
   const typet &type,
   const source_locationt &source_location,
-  const irep_idt &function_id,
   const irep_idt &mode)
 {
   return get_fresh_aux_symbol(
     type,
-    id2string(function_id) + "::tmp_cc",
+    id2string(source_location.get_function()) + "::tmp_cc",
     "tmp_cc",
     source_location,
     mode,
@@ -731,7 +719,6 @@ void code_contractst::instrument_call_statement(
   goto_programt::instructionst::iterator &instruction_iterator,
   goto_programt &program,
   exprt &assigns,
-  const irep_idt &function_id,
   std::set<irep_idt> &freely_assignable_symbols,
   assigns_clauset &assigns_clause)
 {
@@ -827,7 +814,7 @@ void code_contractst::instrument_call_statement(
 
     // check compatibility of assigns clause with the called function
     assigns_clauset called_assigns_clause(
-      called_assigns, *this, function_id, log);
+      called_assigns, *this, called_name, log);
     exprt compatible =
       assigns_clause.compatible_expression(called_assigns_clause);
     goto_programt alias_assertion;
@@ -992,7 +979,6 @@ void code_contractst::check_frame_conditions(
         instruction_it,
         program,
         assigns_expr,
-        target.name,
         freely_assignable_symbols,
         assigns);
     }
@@ -1073,13 +1059,13 @@ bool code_contractst::enforce_contract(const irep_idt &function)
 }
 
 void code_contractst::add_contract_check(
-  const irep_idt &wrapper_fun,
-  const irep_idt &mangled_fun,
+  const irep_idt &wrapper_function,
+  const irep_idt &mangled_function,
   goto_programt &dest)
 {
   PRECONDITION(!dest.instructions.empty());
 
-  const symbolt &function_symbol = ns.lookup(mangled_fun);
+  const symbolt &function_symbol = ns.lookup(mangled_function);
   const auto &code_type = to_code_with_contract_type(function_symbol.type);
 
   exprt assigns = code_type.assigns();
@@ -1123,7 +1109,6 @@ void code_contractst::add_contract_check(
     symbol_exprt r = new_tmp_symbol(
                        code_type.return_type(),
                        skip->source_location,
-                       wrapper_fun,
                        function_symbol.mode)
                        .symbol_expr();
     check.add(goto_programt::make_decl(r, skip->source_location));
@@ -1137,7 +1122,7 @@ void code_contractst::add_contract_check(
 
   // decl parameter1 ...
   goto_functionst::function_mapt::iterator f_it =
-    goto_functions.function_map.find(mangled_fun);
+    goto_functions.function_map.find(mangled_function);
   PRECONDITION(f_it != goto_functions.function_map.end());
 
   const goto_functionst::goto_functiont &gf = f_it->second;
@@ -1148,7 +1133,6 @@ void code_contractst::add_contract_check(
     symbol_exprt p = new_tmp_symbol(
                        parameter_symbol.type,
                        skip->source_location,
-                       wrapper_fun,
                        parameter_symbol.mode)
                        .symbol_expr();
     check.add(goto_programt::make_decl(p, skip->source_location));
@@ -1160,7 +1144,7 @@ void code_contractst::add_contract_check(
     common_replace.insert(parameter_symbol.symbol_expr(), p);
   }
 
-  is_fresh_enforcet visitor(*this, log, wrapper_fun);
+  is_fresh_enforcet visitor(*this, log, wrapper_function);
   visitor.create_declarations();
 
   // Generate: assume(requires)
@@ -1197,7 +1181,7 @@ void code_contractst::add_contract_check(
     auto assertion = code_assertt(ensures);
     assertion.add_source_location() = ensures.source_location();
     ensures_pair = create_ensures_instruction(
-      assertion, ensures.source_location(), wrapper_fun, function_symbol.mode);
+      assertion, ensures.source_location(), function_symbol.mode);
     ensures_pair.first.instructions.back().source_location.set_comment(
       "Check ensures clause");
     ensures_pair.first.instructions.back().source_location.set_property_class(
@@ -1208,7 +1192,7 @@ void code_contractst::add_contract_check(
     check.destructive_append(ensures_pair.second);
   }
 
-  // ret=mangled_fun(parameter1, ...)
+  // ret=mangled_function(parameter1, ...)
   check.add(goto_programt::make_function_call(call, skip->source_location));
 
   // Generate: assert(ensures)
@@ -1227,15 +1211,14 @@ void code_contractst::add_contract_check(
   dest.destructive_insert(dest.instructions.begin(), check);
 }
 
-bool code_contractst::replace_calls(
-  const std::set<std::string> &funs_to_replace)
+bool code_contractst::replace_calls(const std::set<std::string> &functions)
 {
   bool fail = false;
-  for(const auto &fun : funs_to_replace)
+  for(const auto &function : functions)
   {
-    if(!has_contract(fun))
+    if(!has_contract(function))
     {
-      log.error() << "Function '" << fun
+      log.error() << "Function '" << function
                   << "' does not have a contract; "
                      "not replacing calls with contract."
                   << messaget::eom;
@@ -1256,17 +1239,14 @@ bool code_contractst::replace_calls(
         if(call.function().id() != ID_symbol)
           continue;
 
-        const irep_idt &function_name =
+        const irep_idt &called_function =
           to_symbol_expr(call.function()).get_identifier();
         auto found = std::find(
-          funs_to_replace.begin(),
-          funs_to_replace.end(),
-          id2string(function_name));
-        if(found == funs_to_replace.end())
+          functions.begin(), functions.end(), id2string(called_function));
+        if(found == functions.end())
           continue;
 
-        fail |= apply_function_contract(
-          function_name, goto_function.second.body, ins);
+        fail |= apply_function_contract(goto_function.second.body, ins);
       }
     }
   }
@@ -1290,52 +1270,51 @@ void code_contractst::apply_loop_contracts()
 
 bool code_contractst::replace_calls()
 {
-  std::set<std::string> funs_to_replace;
+  std::set<std::string> functions;
   for(auto &goto_function : goto_functions.function_map)
   {
     if(has_contract(goto_function.first))
-      funs_to_replace.insert(id2string(goto_function.first));
+      functions.insert(id2string(goto_function.first));
   }
-  return replace_calls(funs_to_replace);
+  return replace_calls(functions);
 }
 
 bool code_contractst::enforce_contracts()
 {
-  std::set<std::string> funs_to_enforce;
+  std::set<std::string> functions;
   for(auto &goto_function : goto_functions.function_map)
   {
     if(has_contract(goto_function.first))
-      funs_to_enforce.insert(id2string(goto_function.first));
+      functions.insert(id2string(goto_function.first));
   }
-  return enforce_contracts(funs_to_enforce);
+  return enforce_contracts(functions);
 }
 
-bool code_contractst::enforce_contracts(
-  const std::set<std::string> &funs_to_enforce)
+bool code_contractst::enforce_contracts(const std::set<std::string> &functions)
 {
   bool fail = false;
-  for(const auto &fun : funs_to_enforce)
+  for(const auto &function : functions)
   {
-    auto goto_function = goto_functions.function_map.find(fun);
+    auto goto_function = goto_functions.function_map.find(function);
     if(goto_function == goto_functions.function_map.end())
     {
       fail = true;
-      log.error() << "Could not find function '" << fun
+      log.error() << "Could not find function '" << function
                   << "' in goto-program; not enforcing contracts."
                   << messaget::eom;
       continue;
     }
 
-    if(!has_contract(fun))
+    if(!has_contract(function))
     {
       fail = true;
-      log.error() << "Could not find any contracts within function '" << fun
-                  << "'; nothing to enforce." << messaget::eom;
+      log.error() << "Could not find any contracts within function '"
+                  << function << "'; nothing to enforce." << messaget::eom;
       continue;
     }
 
     if(!fail)
-      fail = enforce_contract(fun);
+      fail = enforce_contract(function);
   }
   return fail;
 }