contracts.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Verify and use annotated invariants and pre/post-conditions
 
Author: Michael Tautschnig
 
Date: February 2016
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
 
#include <goto-programs/goto_convert_class.h>
 
#include <util/message.h>
#include <util/namespace.h>
#include <util/optional.h>
#include <util/pointer_expr.h>
 
#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/instrument_preconditions.h>
 
#include <goto-instrument/loop_utils.h>
 
#include <list>
#include <map>
#include <set>
#include <string>
#include <unordered_set>
 
#define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
#define HELP_LOOP_CONTRACTS                                                    \
  " --apply-loop-contracts\n"                                                  \
  "                              check and use loop contracts when provided\n"
 
#define FLAG_REPLACE_CALL "replace-call-with-contract"
#define HELP_REPLACE_CALL                                                      \
  " --replace-call-with-contract <fun>\n"                                      \
  "                              replace calls to fun with fun's contract\n"
 
#define FLAG_ENFORCE_CONTRACT "enforce-contract"
#define HELP_ENFORCE_CONTRACT                                                  \
  " --enforce-contract <fun>     wrap fun with an assertion of its contract\n"
 
class local_may_aliast;
class instrument_spec_assignst;
class cfg_infot;
class function_pointer_obeys_contract_exprt;
 
class code_contractst
{
public:
  code_contractst(goto_modelt &goto_model, messaget &log)
    : ns(goto_model.symbol_table),
      goto_model(goto_model),
      symbol_table(goto_model.symbol_table),
      goto_functions(goto_model.goto_functions),
      log(log),
      converter(symbol_table, log.get_message_handler())
  {
  }
 
  void check_all_functions_found(const std::set<std::string> &functions) const;
 
  void replace_calls(const std::set<std::string> &to_replace);
 
  void enforce_contracts(
    const std::set<std::string> &to_enforce,
    const std::set<std::string> &to_exclude_from_nondet_init = {});
 
  void apply_loop_contracts(
    const std::set<std::string> &to_exclude_from_nondet_init = {});
 
  void check_apply_loop_contracts(
    const irep_idt &function_name,
    goto_functionst::goto_functiont &goto_function,
    const local_may_aliast &local_may_alias,
    goto_programt::targett loop_head,
    goto_programt::targett loop_end,
    const loopt &loop,
    exprt assigns_clause,
    exprt invariant,
    exprt decreases_clause,
    const irep_idt &mode);
 
  // for "helper" classes to update symbol table.
  symbol_tablet &get_symbol_table();
  goto_functionst &get_goto_functions();
 
  namespacet ns;
 
protected:
  goto_modelt &goto_model;
  symbol_tablet &symbol_table;
  goto_functionst &goto_functions;
 
  messaget &log;
  goto_convertt converter;
 
  std::unordered_set<irep_idt> summarized;
 
public:
  void assert_function_pointer_obeys_contract(
    const function_pointer_obeys_contract_exprt &expr,
    const irep_idt &property_class,
    const irep_idt &mode,
    goto_programt &dest);
 
  void assume_function_pointer_obeys_contract(
    const function_pointer_obeys_contract_exprt &expr,
    const irep_idt &mode,
    goto_programt &dest);
 
  void enforce_contract(const irep_idt &function);
 
  void check_frame_conditions_function(const irep_idt &function);
 
  void apply_loop_contract(
    const irep_idt &function,
    goto_functionst::goto_functiont &goto_function);
 
  void apply_function_contract(
    const irep_idt &function,
    const source_locationt &location,
    goto_programt &function_body,
    goto_programt::targett &target);
 
  void add_contract_check(
    const irep_idt &wrapper_function,
    const irep_idt &mangled_function,
    goto_programt &dest);
 
  void add_quantified_variable(exprt &expression, const irep_idt &mode);
 
  void replace_history_parameter(
    exprt &expr,
    std::map<exprt, exprt> &parameter2history,
    source_locationt location,
    const irep_idt &mode,
    goto_programt &history,
    const irep_idt &id);
 
  std::pair<goto_programt, goto_programt> create_ensures_instruction(
    codet &expression,
    source_locationt location,
    const irep_idt &mode);
};
 
#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H