CONTRACTS: rearchitecture code for loop contracts

- Factor out some methods in dfcc_spec_functionst
- Move the code generation methods from dfcc_contract_functionst
  to dfcc_contract_clauses_codegent.
- Update Makefile with new class.
- Propagate interface changes to top level class

Author: Remi Delmas

src/goto-instrument/Makefile

@@ -26,6 +26,7 @@ SRC = accelerate/accelerate.cpp \
       contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp \
       contracts/dynamic-frames/dfcc_instrument.cpp \
       contracts/dynamic-frames/dfcc_spec_functions.cpp \
+      contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp \
       contracts/dynamic-frames/dfcc_contract_functions.cpp \
       contracts/dynamic-frames/dfcc_wrapper_program.cpp \
       contracts/dynamic-frames/dfcc_contract_handler.cpp \

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

@@ -191,14 +191,21 @@ dfcct::dfcct(
     instrument(goto_model, message_handler, utils, library),
     memory_predicates(goto_model, utils, library, instrument, message_handler),
     spec_functions(goto_model, message_handler, utils, library, instrument),
+    contract_clauses_codegen(
+      goto_model,
+      message_handler,
+      utils,
+      library,
+      spec_functions),
     contract_handler(
       goto_model,
       message_handler,
       utils,
       library,
       instrument,
       memory_predicates,
-      spec_functions),
+      spec_functions,
+      contract_clauses_codegen),
     swap_and_wrap(
       goto_model,
       message_handler,
@@ -483,6 +490,8 @@ void dfcct::instrument_other_functions()
 
   goto_model.goto_functions.update();
 
+  // TODO specialise the library functions for the max size of
+  // loop and function contracts
   if(to_check.has_value())
   {
     log.status() << "Specializing cprover_contracts functions for assigns "

src/goto-instrument/contracts/dynamic-frames/dfcc.h

@@ -33,6 +33,7 @@ Author: Remi Delmas, delmasrd@amazon.com
 #include <util/irep.h>
 #include <util/message.h>
 
+#include "dfcc_contract_clauses_codegen.h"
 #include "dfcc_contract_handler.h"
 #include "dfcc_instrument.h"
 #include "dfcc_library.h"
@@ -208,13 +209,15 @@ class dfcct
   message_handlert &message_handler;
   messaget log;
 
-  // hold the global state of the transformation (caches etc.)
+  // Singletons that hold the global state of the program transformation
+  // (caches etc.)
   dfcc_utilst utils;
   dfcc_libraryt library;
   namespacet ns;
   dfcc_instrumentt instrument;
   dfcc_lift_memory_predicatest memory_predicates;
   dfcc_spec_functionst spec_functions;
+  dfcc_contract_clauses_codegent contract_clauses_codegen;
   dfcc_contract_handlert contract_handler;
   dfcc_swap_and_wrapt swap_and_wrap;
 

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

@@ -0,0 +1,293 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking for function contracts
+
+Author: Remi Delmas, delmasrd@amazon.com
+Date: February 2023
+
+\*******************************************************************/
+#include "dfcc_contract_clauses_codegen.h"
+
+#include <util/expr_util.h>
+#include <util/fresh_symbol.h>
+#include <util/invariant.h>
+#include <util/mathematical_expr.h>
+#include <util/namespace.h>
+#include <util/pointer_offset_size.h>
+#include <util/std_expr.h>
+
+#include <goto-programs/goto_model.h>
+
+#include <ansi-c/c_expr.h>
+#include <goto-instrument/contracts/utils.h>
+#include <langapi/language_util.h>
+
+#include "dfcc_library.h"
+#include "dfcc_spec_functions.h"
+#include "dfcc_utils.h"
+
+dfcc_contract_clauses_codegent::dfcc_contract_clauses_codegent(
+  goto_modelt &goto_model,
+  message_handlert &message_handler,
+  dfcc_utilst &utils,
+  dfcc_libraryt &library,
+  dfcc_spec_functionst &spec_functions)
+  : goto_model(goto_model),
+    message_handler(message_handler),
+    log(message_handler),
+    utils(utils),
+    library(library),
+    spec_functions(spec_functions),
+    ns(goto_model.symbol_table)
+{
+}
+
+void dfcc_contract_clauses_codegent::gen_spec_assigns_instructions(
+  const irep_idt &language_mode,
+  const exprt::operandst &assigns_clause,
+  goto_programt &dest)
+{
+  for(const auto &expr : assigns_clause)
+  {
+    if(can_cast_expr<conditional_target_group_exprt>(expr))
+    {
+      encode_assignable_target_group(
+        language_mode, to_conditional_target_group_expr(expr), dest);
+    }
+    else
+    {
+      encode_assignable_target(language_mode, expr, dest);
+    }
+  }
+
+  // inline resulting program and check for loops
+  inline_and_check_warnings(dest);
+  PRECONDITION_WITH_DIAGNOSTICS(
+    utils.has_no_loops(dest),
+    "loops in assigns clause specification functions must be unwound before "
+    "contracts instrumentation");
+}
+
+void dfcc_contract_clauses_codegent::gen_spec_frees_instructions(
+  const irep_idt &language_mode,
+  const exprt::operandst &frees_clause,
+  goto_programt &dest)
+{
+  for(const auto &expr : frees_clause)
+  {
+    if(can_cast_expr<conditional_target_group_exprt>(expr))
+    {
+      encode_freeable_target_group(
+        language_mode, to_conditional_target_group_expr(expr), dest);
+    }
+    else
+    {
+      encode_freeable_target(language_mode, expr, dest);
+    }
+  }
+
+  // inline resulting program and check for loops
+  inline_and_check_warnings(dest);
+  PRECONDITION_WITH_DIAGNOSTICS(
+    utils.has_no_loops(dest),
+    "loops in assigns clause specification functions must be unwound before "
+    "contracts instrumentation");
+}
+
+void dfcc_contract_clauses_codegent::encode_assignable_target_group(
+  const irep_idt &language_mode,
+  const conditional_target_group_exprt &group,
+  goto_programt &dest)
+{
+  const source_locationt &source_location = group.source_location();
+
+  // clean up side effects from the condition expression if needed
+  cleanert cleaner(goto_model.symbol_table, log.get_message_handler());
+  exprt condition(group.condition());
+  if(has_subexpr(condition, ID_side_effect))
+    cleaner.clean(condition, dest, language_mode);
+
+  // Jump target if condition is false
+  auto goto_instruction = dest.add(
+    goto_programt::make_incomplete_goto(not_exprt{condition}, source_location));
+
+  for(const auto &target : group.targets())
+    encode_assignable_target(language_mode, target, dest);
+
+  auto label_instruction = dest.add(goto_programt::make_skip(source_location));
+  goto_instruction->complete_goto(label_instruction);
+}
+
+void dfcc_contract_clauses_codegent::encode_assignable_target(
+  const irep_idt &language_mode,
+  const exprt &target,
+  goto_programt &dest)
+{
+  const source_locationt &source_location = target.source_location();
+
+  if(can_cast_expr<side_effect_expr_function_callt>(target))
+  {
+    // A function call target `foo(params)` becomes `CALL foo(params);`
+    // ```
+    const auto &funcall = to_side_effect_expr_function_call(target);
+    code_function_callt code_function_call(to_symbol_expr(funcall.function()));
+    auto &arguments = code_function_call.arguments();
+    for(auto &arg : funcall.arguments())
+      arguments.emplace_back(arg);
+    dest.add(
+      goto_programt::make_function_call(code_function_call, source_location));
+  }
+  else if(is_assignable(target))
+  {
+    // An lvalue `target` becomes
+    //` CALL __CPROVER_assignable(&target, sizeof(target), is_ptr_to_ptr);`
+    const auto &size =
+      size_of_expr(target.type(), namespacet(goto_model.symbol_table));
+
+    if(!size.has_value())
+    {
+      throw invalid_source_file_exceptiont{
+        "no definite size for lvalue assigns clause target " +
+          from_expr_using_mode(ns, language_mode, target),
+        target.source_location()};
+    }
+    // we have to build the symbol manually because it might not
+    // be present in the symbol table if the user program does not already
+    // use it.
+    code_function_callt code_function_call(
+      symbol_exprt(CPROVER_PREFIX "assignable", empty_typet()));
+    auto &arguments = code_function_call.arguments();
+
+    // ptr
+    arguments.emplace_back(typecast_exprt::conditional_cast(
+      address_of_exprt{target}, pointer_type(empty_typet())));
+
+    // size
+    arguments.emplace_back(size.value());
+
+    // is_ptr_to_ptr
+    arguments.emplace_back(make_boolean_expr(target.type().id() == ID_pointer));
+
+    dest.add(
+      goto_programt::make_function_call(code_function_call, source_location));
+  }
+  else
+  {
+    // any other type of target is unsupported
+    throw invalid_source_file_exceptiont(
+      "unsupported assigns clause target " +
+        from_expr_using_mode(ns, language_mode, target),
+      target.source_location());
+  }
+}
+
+void dfcc_contract_clauses_codegent::encode_freeable_target_group(
+  const irep_idt &language_mode,
+  const conditional_target_group_exprt &group,
+  goto_programt &dest)
+{
+  const source_locationt &source_location = group.source_location();
+
+  // clean up side effects from the condition expression if needed
+  cleanert cleaner(goto_model.symbol_table, log.get_message_handler());
+  exprt condition(group.condition());
+  if(has_subexpr(condition, ID_side_effect))
+    cleaner.clean(condition, dest, language_mode);
+
+  // Jump target if condition is false
+  auto goto_instruction = dest.add(
+    goto_programt::make_incomplete_goto(not_exprt{condition}, source_location));
+
+  for(const auto &target : group.targets())
+    encode_freeable_target(language_mode, target, dest);
+
+  auto label_instruction = dest.add(goto_programt::make_skip(source_location));
+  goto_instruction->complete_goto(label_instruction);
+}
+
+void dfcc_contract_clauses_codegent::encode_freeable_target(
+  const irep_idt &language_mode,
+  const exprt &target,
+  goto_programt &dest)
+{
+  const source_locationt &source_location = target.source_location();
+
+  if(can_cast_expr<side_effect_expr_function_callt>(target))
+  {
+    const auto &funcall = to_side_effect_expr_function_call(target);
+    if(can_cast_expr<symbol_exprt>(funcall.function()))
+    {
+      // for calls to user-defined functions
+      // `foo(params)`
+      //
+      // ```
+      // CALL foo(params);
+      // ```
+      code_function_callt code_function_call(
+        to_symbol_expr(funcall.function()));
+      auto &arguments = code_function_call.arguments();
+      for(auto &arg : funcall.arguments())
+        arguments.emplace_back(arg);
+      dest.add(
+        goto_programt::make_function_call(code_function_call, source_location));
+    }
+  }
+  else if(can_cast_type<pointer_typet>(target.type()))
+  {
+    // A plain `target` becomes `CALL __CPROVER_freeable(target);`
+    code_function_callt code_function_call(
+      utils.get_function_symbol(CPROVER_PREFIX "freeable").symbol_expr());
+    auto &arguments = code_function_call.arguments();
+    arguments.emplace_back(target);
+
+    dest.add(
+      goto_programt::make_function_call(code_function_call, source_location));
+  }
+  else
+  {
+    // any other type of target is unsupported
+    throw invalid_source_file_exceptiont(
+      "unsupported frees clause target " +
+        from_expr_using_mode(ns, language_mode, target),
+      target.source_location());
+  }
+}
+
+void dfcc_contract_clauses_codegent::inline_and_check_warnings(
+  goto_programt &goto_program)
+{
+  std::set<irep_idt> no_body;
+  std::set<irep_idt> missing_function;
+  std::set<irep_idt> recursive_call;
+  std::set<irep_idt> not_enough_arguments;
+
+  utils.inline_program(
+    goto_program,
+    no_body,
+    recursive_call,
+    missing_function,
+    not_enough_arguments);
+
+  // check that the only no body / missing functions are the cprover builtins
+  for(const auto &id : no_body)
+  {
+    INVARIANT(
+      library.is_front_end_builtin(id),
+      "no body for '" + id2string(id) + "' when inlining goto program");
+  }
+
+  for(auto it : missing_function)
+  {
+    INVARIANT(
+      library.is_front_end_builtin(it),
+      "missing function '" + id2string(it) + "' when inlining goto program");
+  }
+
+  INVARIANT(
+    recursive_call.size() == 0,
+    "recursive calls found when inlining goto program");
+
+  INVARIANT(
+    not_enough_arguments.size() == 0,
+    "not enough arguments when inlining goto program");
+}