utils.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Utility functions for code contracts.
 
Author: Saswat Padhi, saspadhi@amazon.com
 
Date: September 2021
 
\*******************************************************************/
 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
 
#include <ansi-c/goto-conversion/goto_convert_class.h>
 
#include <goto-programs/goto_model.h>
#include <goto-programs/loop_ids.h>
 
#include <goto-instrument/havoc_utils.h>
 
#include <vector>
 
#define IN_BASE_CASE "__in_base_case"
#define ENTERED_LOOP "__entered_loop"
#define IN_LOOP_HAVOC_BLOCK "__in_loop_havoc_block"
#define INIT_INVARIANT "__init_invariant"
 
template <class T, typename C>
class loop_templatet;
typedef std::map<loop_idt, exprt> invariant_mapt;
 
class cleanert : public goto_convertt
{
public:
  cleanert(
    symbol_table_baset &_symbol_table,
    message_handlert &_message_handler)
    : goto_convertt(_symbol_table, _message_handler)
  {
  }
 
  void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
  {
    goto_convertt::clean_expr(guard, dest, mode, true);
  }
 
  void do_havoc_slice(
    const symbol_exprt &function,
    const exprt::operandst &arguments,
    goto_programt &dest,
    const irep_idt &mode)
  {
    goto_convertt::do_havoc_slice(nil_exprt{}, function, arguments, dest, mode);
  }
};
 
class havoc_if_validt : public havoc_utilst
{
public:
  havoc_if_validt(const assignst &mod, const namespacet &ns)
    : havoc_utilst(mod, ns), ns(ns)
  {
  }
 
  void append_object_havoc_code_for_expr(
    const source_locationt location,
    const exprt &expr,
    goto_programt &dest) const override;
 
  void append_scalar_havoc_code_for_expr(
    const source_locationt location,
    const exprt &expr,
    goto_programt &dest) const override;
 
protected:
  const namespacet &ns;
};
 
class havoc_assigns_targetst : public havoc_if_validt
{
public:
  havoc_assigns_targetst(
    const assignst &mod,
    symbol_tablet &st,
    message_handlert &message_handler,
    const irep_idt &mode)
    : havoc_if_validt(mod, ns),
      ns(st),
      cleaner(st, message_handler),
      log(message_handler),
      mode(mode)
  {
  }
 
  void append_havoc_pointer_code(
    const source_locationt location,
    const exprt &ptr_to_ptr,
    goto_programt &dest);
 
  void append_havoc_slice_code(
    const source_locationt location,
    const exprt &ptr,
    const exprt &size,
    goto_programt &dest);
 
  void append_havoc_code_for_expr(
    const source_locationt location,
    const exprt &expr,
    goto_programt &dest);
 
  namespacet ns;
  cleanert cleaner;
  messaget log;
  const irep_idt &mode;
};
 
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns);
 
exprt generate_lexicographic_less_than_check(
  const std::vector<symbol_exprt> &lhs,
  const std::vector<symbol_exprt> &rhs);
 
void insert_before_swap_and_advance(
  goto_programt &destination,
  goto_programt::targett &target,
  goto_programt &payload);
 
void insert_before_and_update_jumps(
  goto_programt &destination,
  goto_programt::targett &target,
  const goto_programt::instructiont &i);
 
void simplify_gotos(goto_programt &goto_program, namespacet &ns);
 
bool is_loop_free(
  const goto_programt &goto_program,
  namespacet &ns,
  messaget &log);
 
irep_idt make_assigns_clause_replacement_tracking_comment(
  const exprt &target,
  const irep_idt &function_id,
  const namespacet &ns);
 
bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment);
 
void widen_assigns(assignst &assigns, const namespacet &ns);
 
void add_quantified_variable(
  symbol_table_baset &symbol_table,
  exprt &expression,
  const irep_idt &mode);
 
struct replace_history_parametert
{
  exprt expression_after_replacement;
  std::unordered_map<exprt, symbol_exprt, irep_hash> parameter_to_history;
  goto_programt history_construction;
};
 
replace_history_parametert replace_history_old(
  symbol_table_baset &symbol_table,
  const exprt &expr,
  const source_locationt &location,
  const irep_idt &mode);
 
replace_history_parametert replace_history_loop_entry(
  symbol_table_baset &symbol_table,
  const exprt &expr,
  const source_locationt &location,
  const irep_idt &mode);
 
void generate_history_variables_initialization(
  symbol_table_baset &symbol_table,
  exprt &clause,
  const irep_idt &mode,
  goto_programt &program);
 
bool is_transformed_loop_head(const goto_programt::const_targett &target);
 
bool is_transformed_loop_end(const goto_programt::const_targett &target);
 
bool is_assignment_to_instrumented_variable(
  const goto_programt::const_targett &target,
  std::string var_name);
 
unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix);
 
goto_programt::targett get_loop_end_from_loop_head_and_content_mutable(
  const goto_programt::targett &loop_head,
  const loop_templatet<goto_programt::targett, goto_programt::target_less_than>
    &loop);
 
goto_programt::const_targett get_loop_end_from_loop_head_and_content(
  const goto_programt::const_targett &loop_head,
  const loop_templatet<
    goto_programt::const_targett,
    goto_programt::target_less_than> &loop);
 
goto_programt::targett get_loop_head_or_end(
  const unsigned int loop_number,
  goto_functiont &function,
  bool finding_head);
 
goto_programt::targett
get_loop_end(const unsigned int loop_number, goto_functiont &function);
 
goto_programt::targett
get_loop_head(const unsigned int loop_number, goto_functiont &function);
 
void annotate_invariants(
  const invariant_mapt &invariant_map,
  goto_modelt &goto_model);
 
void annotate_assigns(
  const std::map<loop_idt, std::set<exprt>> &assigns_map,
  goto_modelt &goto_model);
 
void annotate_assigns(
  const std::map<loop_idt, exprt> &assigns_map,
  goto_modelt &goto_model);
 
void annotate_decreases(
  const std::map<loop_idt, std::vector<exprt>> &decreases_map,
  goto_modelt &goto_model);
 
#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H