goto_convert_class.h

Go to the documentation of this file.

#ifndef CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
#define CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_CLASS_H
 
#include <goto-programs/goto_program.h>
#include <list>
#include <optional>
#include <queue>
#include <set>
#include <stack>
#include <util/expr/expr_util.h>
#include <irep2/irep2_guard.h>
#include <util/symtab/namespace.h>
#include <util/config/options.h>
#include <util/symtab/symbol_generator.h>
#include <util/irep/std_code.h>
 
class goto_convertt
{
public:
  void goto_convert(const codet &code, goto_programt &dest);

  static bool is_atomic_symbol(const exprt &expr, const namespacet &ns);

  static bool has_atomic_read(const exprt &expr, const namespacet &ns);
 
  goto_convertt(contextt &_context, optionst &_options)
    : context(_context),
      options(_options),
      ns(_context),
      tmp_symbol("goto_convertt::")
  {
  }
 
protected:
  contextt &context;
  optionst &options;
  namespacet ns;
  symbol_generator tmp_symbol;
 
  void goto_convert_rec(const codet &code, goto_programt &dest);
 
  //
  // tools for symbols
  //
  void new_name(symbolt &symbol);
 
  symbolt &new_tmp_symbol(const typet &type);
  symbolt &new_cftest_symbol(const typet &type);
 
  //
  // side effect removal
  //
  void make_temp_symbol(exprt &expr, goto_programt &dest);
 
  // this produces if(guard) dest;
  void guard_program(const guard2tc &guard, goto_programt &dest);
 
  void remove_sideeffects(
    exprt &expr,
    goto_programt &dest,
    bool result_is_used = true);
 
  // IREP2 dual-API seam (W1, esbmc/esbmc#4715): delegates to the legacy
  // exprt overload above; behaviour-identical by construction.
  void remove_sideeffects(
    expr2tc &expr,
    goto_programt &dest,
    bool result_is_used = true);

  void remove_condition_sideeffects(exprt &cond, goto_programt &dest);
  bool in_short_circuit = false;
 
  // Recursively flatten a (possibly nested) &&/|| contract clause
  // (__ESBMC_requires / __ESBMC_ensures), hoisting side effects (e.g.
  // __ESBMC_old()) only at the leaves so no conjunct is dropped (#6298).
  void flatten_contract_clause(exprt &clause, goto_programt &dest);
 
  void address_of_replace_objects(exprt &expr, goto_programt &dest);
 
  bool rewrite_vla_decl(typet &var_type, goto_programt &dest);
  bool rewrite_vla_decl_size(exprt &size, goto_programt &dest);
  void generate_dynamic_size_vla(
    exprt &var,
    const locationt &loc,
    goto_programt &dest,
    bool allow_zero_size = false);
 
  bool has_sideeffect(const exprt &expr);
  // IREP2 overload (W1, esbmc/esbmc#4715): native recursive scan for a
  // sideeffect2t node, mirroring the legacy exprt overload above.
  bool has_sideeffect(const expr2tc &expr);
  bool has_destructible_sideeffect(const exprt &expr);
  bool splits_and_condition(const exprt &cond);
 
  // Used by remove_sideeffects() to process a quantifier body expression.
  // Recursively walks || and && sub-expressions without converting them to
  // short-circuit ITE chains, so that bound variables remain reachable by
  // replace_name_in_body() in smt_solver.cpp.  @p bound_vars holds the
  // identifiers bound by the enclosing quantifiers.
  void remove_sideeffects_for_quantifier_body(
    exprt &body,
    const std::set<irep_idt> &bound_vars,
    goto_programt &dest);
  void inline_calls_in_quantifier_body(exprt &expr, unsigned depth);
  bool try_inline_pure_call(const symbolt &fsym, const exprt &call, exprt &out);
  // Summarize a callee with straight-line assignments, if/else, and
  // constant-trip-count loops into a single side-effect-free expression so it
  // can appear in a quantifier body.  Returns false (leaving @p out untouched)
  // for any shape it cannot soundly turn into a pure expression.
  bool summarize_pure_call(const symbolt &fsym, const exprt &call, exprt &out);
  // Why summarize_pure_call() gave up, keyed by callsite location, so that
  // the rejection reported for a quantifier body can name the cause.
  std::map<std::string, std::string> summary_reject_reasons;
  const exprt *find_sideeffect_on_bound_var(
    const exprt &expr,
    const std::set<irep_idt> &bound_vars);
  void skolemize_asserted_foralls(exprt &expr, goto_programt &dest);
  // Rewrite __ESBMC_forall/__ESBMC_exists intrinsic calls into forall/exists
  // expressions, summarizing calls in the body first, before any hoisting can
  // freeze the bound variable.  Bodies that cannot be made side-effect-free are
  // left as calls for the skolemization / quantifier-body fallbacks.
  void convert_quantifier_calls(exprt &expr);
 
  void remove_assignment(exprt &expr, goto_programt &dest, bool result_is_used);
  void remove_post(exprt &expr, goto_programt &dest, bool result_is_used);
  void remove_pre(exprt &expr, goto_programt &dest, bool result_is_used);
  void
  remove_function_call(exprt &expr, goto_programt &dest, bool result_is_used);
  void remove_cpp_new(exprt &expr, goto_programt &dest, bool result_is_used);
  void remove_cpp_delete(exprt &expr, goto_programt &dest);
  void remove_operand_sideeffects(exprt &expr, goto_programt &dest);
  void drop_destructor(const symbol_exprt &object, std::size_t from);
  void remove_temporary_object(exprt &expr, goto_programt &dest);
  void remove_statement_expression(
    exprt &expr,
    goto_programt &dest,
    bool result_is_used);
  void remove_gcc_conditional_expression(exprt &expr, goto_programt &dest);
 
  virtual void
  do_cpp_new(const exprt &lhs, const exprt &rhs, goto_programt &dest);
 
  static void replace_new_object(const exprt &object, exprt &dest);
 
  void cpp_new_at(
    const exprt &lhs,
    const exprt &placement,
    const locationt &location,
    goto_programt &dest);
 
  void cpp_new_initializer(
    const exprt &lhs,
    const exprt &rhs,
    const exprt &elem_count,
    goto_programt &dest);
 
  void cpp_new_zero_fill(
    const exprt &lhs,
    const exprt &rhs,
    const exprt &elem_count,
    goto_programt &dest);
 
  void cpp_new_store_element(
    const exprt &base,
    const exprt &offset,
    const exprt &init,
    const locationt &location,
    const exprt &built,
    code_blockt &out);
 
  bool cpp_new_init_list(
    const exprt &lhs,
    const exprt &rhs,
    const exprt &init,
    const exprt &elem_count,
    const exprt &built,
    code_blockt &out);
 
  void convert_cpp_new_elements(
    const exprt &base,
    const exprt &built,
    const codet &construction,
    goto_programt &dest);
 
  bool user_code_throws();
  std::optional<bool> user_code_throws_cache;
 
  //
  // function calls
  //
 
  virtual void do_function_call(
    const exprt &lhs,
    const exprt &function,
    const exprt::operandst &arguments,
    const locationt &location,
    goto_programt &dest);
 
  virtual void do_function_call_if(
    const exprt &lhs,
    const exprt &function,
    const exprt::operandst &arguments,
    goto_programt &dest);

  bool drop_inactive_contract_clause(bool is_clause) const;
 
  virtual void do_function_call_symbol(
    const exprt &lhs,
    const exprt &function,
    const exprt::operandst &arguments,
    goto_programt &dest);
 
  virtual void do_function_call_dereference(
    const exprt &lhs,
    const exprt &function,
    const exprt::operandst &arguments,
    goto_programt &dest);
 
  //
  // conversion
  //
  void convert_block(const codet &code, goto_programt &dest);
  void convert_controlled(const codet &code, goto_programt &dest);
  void convert_decl(const codet &code, goto_programt &dest);
  void discard_comma_operands(exprt &initializer, goto_programt &dest);
  void remove_comma_operand(exprt &operand, goto_programt &dest);
  void destroy_comma_operand_temporaries(
    std::size_t stack_size,
    const locationt &location,
    goto_programt &dest);
  std::set<irep_idt> comma_operand_temporaries;
  void convert_decl_initializer(
    const exprt &var,
    exprt &initializer,
    const codet &new_code,
    const symbolt &s,
    goto_programt &dest);
  bool construct_in_place(
    const exprt &object,
    const exprt &initializer,
    goto_programt &dest);
  void remove_initializer_sideeffects(
    const exprt &object,
    exprt &initializer,
    goto_programt &dest);
  void convert_dynamic_static_init(
    const codet &decl,
    const symbolt &s,
    const symbolt &guard,
    goto_programt &dest);
  void construct_array_elements(
    const exprt &base,
    const typet &type,
    const side_effect_expr_function_callt &ctor,
    goto_programt &dest);
  void schedule_array_element_destructors(const exprt &base, const typet &type);
 
  void convert_decl_block(const codet &code, goto_programt &dest);
  void convert_expression(const codet &code, goto_programt &dest);
  void convert_assign(const code_assignt &code, goto_programt &dest);
  void convert_assign_atomic(
    const exprt &lhs,
    const exprt &rhs,
    const locationt &location,
    goto_programt &dest);
  void convert_assign_rmw_atomic(
    const exprt &lhs,
    const exprt &rhs,
    const locationt &location,
    goto_programt &dest);
  void convert_cpp_delete(const codet &code, goto_programt &dest);
  void convert_for(const codet &code, goto_programt &dest);
  void convert_while(const codet &code, goto_programt &dest);
  void convert_dowhile(const codet &code, goto_programt &dest);
  void convert_assume(const codet &code, goto_programt &dest);
  void convert_assert(const codet &code, goto_programt &dest);
  bool emits_assert(const locationt &location) const;
  void assume_if_ends_path(
    const expr2tc &guard,
    const locationt &location,
    goto_programt &dest);
  void convert_switch(const codet &code, goto_programt &dest);
  void convert_break(const code_breakt &code, goto_programt &dest);
  void convert_return(const code_returnt &code, goto_programt &dest);
  void remove_return_value_sideeffects(exprt &value, goto_programt &dest);
  void convert_continue(const code_continuet &code, goto_programt &dest);
  void convert_ifthenelse(const codet &code, goto_programt &dest);
  void convert_init(const codet &code, goto_programt &dest);
  void convert_goto(const codet &code, goto_programt &dest);
  void convert_skip(const codet &code, goto_programt &dest);
  void convert_non_deterministic_goto(const codet &code, goto_programt &dest);
  void convert_label(const code_labelt &code, goto_programt &dest);
  void convert_switch_case(const code_switch_caset &code, goto_programt &dest);
  void
  convert_function_call(const code_function_callt &code, goto_programt &dest);
  void convert_atomic_begin(const codet &code, goto_programt &dest);
  void convert_atomic_end(const codet &code, goto_programt &dest);
  void convert(const codet &code, goto_programt &dest);
  void copy(
    const codet &code,
    goto_program_instruction_typet type,
    goto_programt &dest);
 
  typedef std::vector<codet> destructor_stackt;

  void convert_full_expression(const codet &code, goto_programt &dest);
  bool destroy_full_expression_temporaries(
    std::size_t stack_size,
    const locationt &,
    goto_programt &dest);
  std::size_t keep_reference_member_temporaries(
    const exprt &initializer,
    std::size_t stack_size);
  void unwind_destructor_stack(
    const locationt &,
    std::size_t stack_size,
    goto_programt &dest);
  void unwind_destructor_stack(
    const locationt &,
    std::size_t stack_size,
    goto_programt &dest,
    destructor_stackt &stack);
  void declare_skipped_locals(
    const destructor_stackt &stack,
    std::size_t from,
    const locationt &location,
    goto_programt &dest);
  goto_programt::targett case_entry(
    goto_programt::targett target,
    std::size_t switch_stack_size,
    const locationt &location,
    goto_programt &stubs);
  static bool is_destructor_entry(const codet &entry);
  void kill_condition_temporaries(
    std::size_t stack_size,
    const locationt &location,
    goto_programt &branch,
    goto_programt &exit);
  void guard_arm_destructors(
    exprt &cond,
    std::size_t true_size,
    std::size_t false_size,
    const locationt &location,
    goto_programt &dest);
  void record_exception_unwind(goto_programt::instructiont &call);
 
  //
  // Try-catch conversion
  //
 
  void convert_catch(const codet &code, goto_programt &dest);
  void convert_throw(const exprt &expr, goto_programt &dest);
 
  //
  // gotos
  //
 
  void finish_gotos(goto_programt &dest);
  void optimize_guarded_gotos(goto_programt &dest);
 
  typedef std::
    map<irep_idt, std::pair<goto_programt::targett, destructor_stackt>>
      labelst;
  typedef std::list<std::pair<goto_programt::targett, destructor_stackt>>
    gotost;
  typedef std::list<goto_programt::targett> computed_gotost;
  typedef exprt::operandst caset;
  typedef std::list<std::pair<goto_programt::targett, caset>> casest;
  typedef std::map<goto_programt::targett, casest::iterator> cases_mapt;
  typedef std::map<goto_programt::targett, destructor_stackt> case_stackst;
 
  struct targetst
  {
    bool return_set, has_return_value, break_set, continue_set, default_set,
      throw_set, leave_set;
 
    labelst labels;
    gotost gotos;
    computed_gotost computed_gotos;
    destructor_stackt destructor_stack;
 
    casest cases;
    cases_mapt cases_map;
    case_stackst case_stacks;
 
    goto_programt::targett return_target, break_target, continue_target,
      default_target, throw_target, leave_target;
 
    std::size_t break_stack_size, continue_stack_size, throw_stack_size,
      leave_stack_size;
 
    targetst()
      : return_set(false),
        has_return_value(false),
        break_set(false),
        continue_set(false),
        default_set(false),
        throw_set(false),
        leave_set(false),
        break_stack_size(0),
        continue_stack_size(0),
        throw_stack_size(0),
        leave_stack_size(0)
    {
    }
 
    void set_break(goto_programt::targett _break_target)
    {
      break_set = true;
      break_target = _break_target;
      break_stack_size = destructor_stack.size();
    }
 
    void set_continue(goto_programt::targett _continue_target)
    {
      continue_set = true;
      continue_target = _continue_target;
      continue_stack_size = destructor_stack.size();
    }
 
    void set_default(goto_programt::targett _default_target)
    {
      default_set = true;
      default_target = _default_target;
    }
 
    void set_return(goto_programt::targett _return_target)
    {
      return_set = true;
      return_target = _return_target;
    }
 
    void set_throw(goto_programt::targett _throw_target)
    {
      throw_set = true;
      throw_target = _throw_target;
      throw_stack_size = destructor_stack.size();
    }
 
    void set_leave(goto_programt::targett _leave_target)
    {
      leave_set = true;
      leave_target = _leave_target;
      leave_stack_size = destructor_stack.size();
    }
  } targets;
 
  struct break_continue_targetst
  {
    // for 'while', 'for', 'dowhile'
 
    explicit break_continue_targetst(const targetst &targets)
    {
      break_set = targets.break_set;
      continue_set = targets.continue_set;
      break_target = targets.break_target;
      continue_target = targets.continue_target;
      break_stack_size = targets.break_stack_size;
      continue_stack_size = targets.continue_stack_size;
    }
 
    // An outer break or continue after this construct must unwind to the
    // outer depth, not to this one's.
    void restore(targetst &targets)
    {
      targets.break_set = break_set;
      targets.continue_set = continue_set;
      targets.break_target = break_target;
      targets.continue_target = continue_target;
      targets.break_stack_size = break_stack_size;
      targets.continue_stack_size = continue_stack_size;
    }
 
    goto_programt::targett break_target;
    goto_programt::targett continue_target;
    bool break_set, continue_set;
    std::size_t break_stack_size, continue_stack_size;
  };
 
  struct break_switch_targetst
  {
    // for 'switch'
 
    explicit break_switch_targetst(const targetst &targets)
    {
      break_set = targets.break_set;
      default_set = targets.default_set;
      break_target = targets.break_target;
      default_target = targets.default_target;
      break_stack_size = targets.break_stack_size;
      cases = targets.cases;
      cases_map = targets.cases_map;
      case_stacks = targets.case_stacks;
    }
 
    void restore(targetst &targets)
    {
      targets.break_set = break_set;
      targets.default_set = default_set;
      targets.break_target = break_target;
      targets.default_target = default_target;
      targets.break_stack_size = break_stack_size;
      targets.cases = cases;
      targets.cases_map = cases_map;
      targets.case_stacks = case_stacks;
    }
 
    goto_programt::targett break_target;
    goto_programt::targett default_target;
    bool break_set, default_set;
    std::size_t break_stack_size;
 
    casest cases;
    cases_mapt cases_map;
    case_stackst case_stacks;
  };
 
  struct throw_targett
  {
    // for 'try...catch' and the like
 
    explicit throw_targett(const targetst &targets)
    {
      throw_set = targets.throw_set;
      throw_target = targets.throw_target;
      throw_stack_size = targets.destructor_stack.size();
    }
 
    void restore(targetst &targets)
    {
      targets.throw_set = throw_set;
      targets.throw_target = throw_target;
    }
 
    goto_programt::targett throw_target;
    bool throw_set;
    std::size_t throw_stack_size;
  };
 
  void case_guard(const exprt &value, const caset &case_op, exprt &dest);
  static exprt case_label(const exprt &lo, const exprt &hi);
 
  // if(cond) { true_case } else { false_case }
  void generate_ifthenelse(
    const exprt &cond,
    goto_programt &true_case,
    goto_programt &false_case,
    const locationt &location,
    goto_programt &dest);
 
  // if(guard) goto target_true; else goto target_false;
  void generate_conditional_branch(
    const exprt &guard,
    goto_programt::targett target_true,
    goto_programt::targett target_false,
    const locationt &location,
    goto_programt &dest);
 
  // if(guard) goto target;
  void generate_conditional_branch(
    const exprt &guard,
    goto_programt::targett target_true,
    const locationt &location,
    goto_programt &dest);
 
  // turn a OP b OP c into a list a, b, c
  static void collect_operands(
    const exprt &expr,
    const irep_idt &id,
    std::list<exprt> &dest);
 
  // Emit the post-noreturn truncation for __assert_fail-family calls
  // (__assert_fail / __assert_rtn / FreeBSD __assert / _wassert) under
  // --no-assertions.  Fires only when --memory-leak-check is enabled
  // (i.e. valid-memsafety / valid-memcleanup): the leak walker is
  // invoked --- mirroring abort()'s body in
  // src/c2goto/library/stdlib.c --- and then ASSUME false truncates
  // the path.  Otherwise the call is a no-op so user assert(cond)
  // does not silently become assume(cond) under property modes that
  // intentionally suppress assertions (no-data-race, plain
  // --no-assertions).  See PR #4442 review for the no-data-race
  // regression that motivated the gate.
  void
  emit_assert_fail_noreturn(const locationt &location, goto_programt &dest);
 
  // Lower a value-discarding `&&` / `||` as a statement; false when the caller
  // should fall back to rewrite_short_circuit_as_ternary.
  bool lower_discarded_short_circuit(
    exprt &expr,
    goto_programt &dest,
    bool result_is_used);
 
  void rewrite_short_circuit_as_ternary(exprt &expr);
 
  // The same four hooks differ only in arity and in which argument carries the
  // failing expression; `expr_arg` names the latter.
  void do_assert_fail(
    const exprt &function,
    const exprt::operandst &arguments,
    goto_programt &dest,
    const irep_idt &base_name,
    std::size_t arity,
    std::size_t expr_arg);
 
  // some built-in functions
  void do_abort(
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void do_atomic_begin(
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void do_atomic_end(
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void do_create_thread(
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void do_malloc(
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void do_realloc(
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void do_alloca(
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void do_free(
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void do_sync(
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void do_exit(
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void do_printf(
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest,
    const std::string &bs_name);
  void do_operator_new(
    const exprt &lhs,
    const exprt &function,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void do_mem(
    bool is_malloc,
    const exprt &lhs,
    const exprt &rhs,
    const exprt::operandst &arguments,
    goto_programt &dest);
  void get_alloc_size(typet &alloc_type, exprt &alloc_size);
};
 
#endif