dfcc_instrument_loop.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Dynamic frame condition checking for loop contracts
 
Author: Qinheping Hu, qinhh@amazon.com
 
Author: Remi Delmas, delmasrd@amazon.com
 
Date: April 2023
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INSTRUMENT_LOOP_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INSTRUMENT_LOOP_H
 
#include <util/message.h>
 
#include <goto-programs/goto_model.h>
 
#include <analyses/local_may_alias.h>
 
class dfcc_spec_functionst;
class dfcc_libraryt;
class dfcc_instrumentt;
class dfcc_spec_functionst;
class dfcc_contract_clauses_codegent;
class dfcc_cfg_infot;
 
class dfcc_instrument_loopt
{
public:
  dfcc_instrument_loopt(
    goto_modelt &goto_model,
    message_handlert &message_handler,
    dfcc_libraryt &library,
    dfcc_spec_functionst &spec_functions,
    dfcc_contract_clauses_codegent &contract_clauses_codegen);
 
  //    new_variant = loop_decreases;
  void operator()(
    const std::size_t loop_id,
    const irep_idt &function_id,
    goto_functiont &goto_function,
    dfcc_cfg_infot &cfg_info,
    const std::set<symbol_exprt> &local_statics,
    std::set<irep_idt> &function_pointer_contracts);
 
  std::size_t get_max_assigns_clause_size() const
  {
    return max_assigns_clause_size;
  }
 
protected:
  // keeps track of the maximum number of assigns clause targets
  std::size_t max_assigns_clause_size = 0;
  goto_modelt &goto_model;
  messaget log;
  dfcc_libraryt &library;
  dfcc_spec_functionst &spec_functions;
  dfcc_contract_clauses_codegent &contract_clauses_codegen;
  namespacet ns;
 
  std::unordered_map<exprt, symbol_exprt, irep_hash> add_prehead_instructions(
    const std::size_t loop_id,
    goto_functionst::goto_functiont &goto_function,
    symbol_table_baset &symbol_table,
    goto_programt::targett loop_head,
    goto_programt::targett loop_latch,
    goto_programt &assigns_instrs,
    exprt &invariant,
    const exprt::operandst &assigns,
    const symbol_exprt &loop_write_set,
    const symbol_exprt &addr_of_loop_write_set,
    const symbol_exprt &entered_loop,
    const symbol_exprt &initial_invariant,
    const symbol_exprt &in_base_case,
    const irep_idt &symbol_mode);
 
  goto_programt::instructiont::targett add_step_instructions(
    const std::size_t loop_id,
    const std::size_t cbmc_loop_id,
    const irep_idt &function_id,
    goto_functionst::goto_functiont &goto_function,
    symbol_table_baset &symbol_table,
    goto_programt::targett loop_head,
    goto_programt::targett loop_latch,
    goto_programt &havoc_instrs,
    exprt &invariant,
    const exprt::operandst &decreases_clauses,
    const symbol_exprt &loop_write_set,
    const exprt &outer_write_set,
    const symbol_exprt &initial_invariant,
    const symbol_exprt &in_base_case,
    const std::vector<symbol_exprt> &old_decreases_vars);
 
  void add_body_instructions(
    const std::size_t loop_id,
    const std::size_t cbmc_loop_id,
    goto_functionst::goto_functiont &goto_function,
    symbol_table_baset &symbol_table,
    goto_programt::targett loop_head,
    goto_programt::targett loop_latch,
    exprt &invariant,
    const exprt::operandst &decreases_clauses,
    const symbol_exprt &entered_loop,
    const symbol_exprt &in_base_case,
    const std::vector<symbol_exprt> &old_decreases_vars,
    const std::vector<symbol_exprt> &new_decreases_vars,
    const goto_programt::instructiont::targett &step_case_target,
    const irep_idt &symbol_mode);
 
  void add_exit_instructions(
    const std::size_t loop_id,
    const std::size_t cbmc_loop_id,
    goto_functionst::goto_functiont &goto_function,
    goto_programt::targett loop_head,
    const symbol_exprt &loop_write_set,
    const symbol_exprt &addr_of_loop_write_set,
    const std::unordered_map<exprt, symbol_exprt, irep_hash> &history_var_map,
    const symbol_exprt &entered_loop,
    const symbol_exprt &initial_invariant,
    const symbol_exprt &in_base_case,
    const std::vector<symbol_exprt> &old_decreases_vars,
    const std::vector<symbol_exprt> &new_decreases_vars);
};
 
#endif