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
 
// clang-format off
#include <vector>
 
#include <analyses/dirty.h>
#include <analyses/locals.h>
 
#include <goto-instrument/havoc_utils.h>
 
#include <goto-programs/goto_convert_class.h>
#include <goto-programs/goto_model.h>
 
#include <util/expr_cast.h>
#include <util/byte_operators.h>
#include <util/message.h>
// clang-format on
 
class havoc_if_validt : public havoc_utilst
{
public:
  havoc_if_validt(const assignst &mod, const namespacet &ns)
    : havoc_utilst(mod), 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, const namespacet &ns)
    : havoc_if_validt(mod, ns)
  {
  }
 
  void append_havoc_code_for_expr(
    const source_locationt location,
    const exprt &expr,
    goto_programt &dest) const override;
};
 
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);
 
const symbolt &new_tmp_symbol(
  const typet &type,
  const source_locationt &location,
  const irep_idt &mode,
  symbol_table_baset &symtab,
  std::string suffix = "tmp_cc",
  bool is_auxiliary = true);
 
void simplify_gotos(goto_programt &goto_program, namespacet &ns);
 
bool is_loop_free(
  const goto_programt &goto_program,
  namespacet &ns,
  messaget &log);
 
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);
  }
};
 
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);
 
#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H