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 <util/message.h>
#include <util/namespace.h>
 
#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_model.h>
 
#include <goto-instrument/loop_utils.h>
 
#include "loop_contract_config.h"
 
#include <map>
#include <set>
#include <string>
#include <unordered_set>
 
#define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
#define HELP_LOOP_CONTRACTS                                                    \
  " {y--apply-loop-contracts} \t check and use loop contracts when provided\n"
#define HELP_LOOP_CONTRACTS                                                    \ …
 
#define FLAG_DISABLE_SIDE_EFFECT_CHECK                                         \
  "disable-loop-contracts-side-effect-check"
#define FLAG_DISABLE_SIDE_EFFECT_CHECK                                         \ …
#define HELP_DISABLE_SIDE_EFFECT_CHECK                                         \
  " {y--disable-loop-contracts-side-effect-check} \t UNSOUND OPTION.\t "       \
  " disable the check of side-effect of loop contracts\n"
#define HELP_DISABLE_SIDE_EFFECT_CHECK                                         \ …
#define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind"
#define HELP_LOOP_CONTRACTS_NO_UNWIND                                          \
  " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n"
#define HELP_LOOP_CONTRACTS_NO_UNWIND                                          \ …
 
#define FLAG_LOOP_CONTRACTS_FILE "loop-contracts-file"
#define HELP_LOOP_CONTRACTS_FILE                                               \
  " {y--loop-contracts-file} {ufile} \t "                                      \
  "parse and annotate loop contracts from files\n"
#define HELP_LOOP_CONTRACTS_FILE                                               \ …
 
#define FLAG_REPLACE_CALL "replace-call-with-contract"
#define HELP_REPLACE_CALL                                                      \
  " {y--replace-call-with-contract} {ufunction}[/{ucontract}] \t "             \
  "replace calls to {ufunction} with {ucontract}\n"
#define HELP_REPLACE_CALL                                                      \ …
 
#define FLAG_ENFORCE_CONTRACT "enforce-contract"
#define HELP_ENFORCE_CONTRACT                                                  \
  " {y--enforce-contract} {ufunction}[/{ucontract}] \t "                       \
  "wrap function with an assertion of contract\n"
#define HELP_ENFORCE_CONTRACT                                                  \ …
 
class local_may_aliast;
 
class code_contractst
{
public:
  code_contractst(
    goto_modelt &goto_model,
    messaget &log,
    const loop_contract_configt &loop_contract_config)
    : ns(goto_model.symbol_table),
      goto_model(goto_model),
      symbol_table(goto_model.symbol_table),
      goto_functions(goto_model.goto_functions),
      log(log),
      loop_contract_config(loop_contract_config)
  {
  }
  code_contractst( {…}
 
  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);
 
  std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
  get_original_loop_number_map() const
  {
    return original_loop_number_map;
  }
  get_original_loop_number_map() const {…}
 
  std::unordered_set<goto_programt::const_targett, const_target_hash>
  get_loop_havoc_set() const
  {
    return loop_havoc_set;
  }
  get_loop_havoc_set() const {…}
 
  const namespacet ns;
 
protected:
  goto_modelt &goto_model;
  symbol_tablet &symbol_table;
  goto_functionst &goto_functions;
 
  messaget &log;
 
  std::unordered_set<irep_idt> summarized;
 
  std::list<std::string> loop_names;
 
  std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
    original_loop_number_map;
 
  std::unordered_set<goto_programt::const_targett, const_target_hash>
    loop_havoc_set;
 
  // Loop contract configuration
  loop_contract_configt loop_contract_config;
 
public:
  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);
};
class code_contractst {…};
 
#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H