expr2c_class.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANSI_C_EXPR2C_CLASS_H
#define CPROVER_ANSI_C_EXPR2C_CLASS_H
 
#include "expr2c.h"
 
#include <string>
#include <unordered_map>
#include <unordered_set>
 
#include <goto-programs/goto_instruction_code.h>
 
#include <util/bitvector_expr.h>
#include <util/byte_operators.h>
#include <util/mathematical_expr.h>
#include <util/std_code.h>
 
class annotated_pointer_constant_exprt;
class c_qualifierst;
class namespacet;
class r_or_w_ok_exprt;
class pointer_in_range_exprt;
class prophecy_r_or_w_ok_exprt;
class prophecy_pointer_in_range_exprt;
 
class expr2ct
{
public:
  explicit expr2ct(
    const namespacet &_ns,
    const expr2c_configurationt &configuration =
      expr2c_configurationt::default_configuration)
    : ns(_ns), configuration(configuration), sizeof_nesting(0)
  {
  }
  explicit expr2ct( {…}
  virtual ~expr2ct() { }
 
  virtual std::string convert(const typet &src);
  virtual std::string convert(const exprt &src);
 
  void get_shorthands(const exprt &expr);
 
  std::string
  convert_with_identifier(const typet &src, const std::string &identifier);
 
protected:
  const namespacet &ns;
  const expr2c_configurationt &configuration;
 
  virtual std::string convert_rec(
    const typet &src,
    const c_qualifierst &qualifiers,
    const std::string &declarator);
 
  virtual std::string convert_struct_type(
    const typet &src,
    const std::string &qualifiers_str,
    const std::string &declarator_str);
 
  std::string convert_struct_type(
    const typet &src,
    const std::string &qualifer_str,
    const std::string &declarator_str,
    bool inc_struct_body,
    bool inc_padding_components);
 
  virtual std::string convert_array_type(
    const typet &src,
    const c_qualifierst &qualifiers,
    const std::string &declarator_str);
 
  std::string convert_array_type(
    const typet &src,
    const c_qualifierst &qualifiers,
    const std::string &declarator_str,
    bool inc_size_if_possible);
 
  static std::string indent_str(unsigned indent);
 
  std::unordered_map<irep_idt, std::unordered_set<irep_idt>> ns_collision;
  std::unordered_map<irep_idt, irep_idt> shorthands;
 
  unsigned sizeof_nesting;
 
  irep_idt id_shorthand(const irep_idt &identifier) const;
 
  std::string convert_typecast(
    const typecast_exprt &src, unsigned &precedence);
 
  std::string convert_pointer_arithmetic(
    const exprt &src,
    unsigned &precedence);
 
  std::string convert_pointer_difference(
    const exprt &src,
    unsigned &precedence);
 
  std::string convert_binary(
    const binary_exprt &,
    const std::string &symbol,
    unsigned precedence,
    bool full_parentheses);
 
  std::string convert_multi_ary(
    const exprt &src, const std::string &symbol,
    unsigned precedence, bool full_parentheses);
 
  std::string convert_cond(
    const exprt &src, unsigned precedence);
 
  std::string convert_struct_member_value(
    const exprt &src, unsigned precedence);
 
  std::string convert_array_member_value(
    const exprt &src, unsigned precedence);
 
  std::string convert_member(
    const member_exprt &src, unsigned precedence);
 
  std::string convert_array_of(const exprt &src, unsigned precedence);
 
  std::string convert_trinary(
    const ternary_exprt &src,
    const std::string &symbol1,
    const std::string &symbol2,
    unsigned precedence);
 
  std::string convert_rox(const shift_exprt &src, unsigned precedence);
 
  std::string convert_overflow(
    const exprt &src, unsigned &precedence);
 
  std::string convert_binding(
    const binding_exprt &,
    const std::string &symbol,
    unsigned precedence);
 
  std::string convert_with(
    const exprt &src, unsigned precedence);
 
  std::string convert_update(const update_exprt &, unsigned precedence);
 
  std::string convert_member_designator(
    const exprt &src);
 
  std::string convert_index_designator(
    const exprt &src);
 
  std::string convert_index(const binary_exprt &, unsigned precedence);
 
  std::string
  convert_byte_extract(const byte_extract_exprt &, unsigned precedence);
 
  std::string
  convert_byte_update(const byte_update_exprt &, unsigned precedence);
 
  std::string convert_extractbit(const extractbit_exprt &, unsigned precedence);
 
  std::string
  convert_extractbits(const extractbits_exprt &src, unsigned precedence);
 
  std::string convert_unary(
    const unary_exprt &,
    const std::string &symbol,
    unsigned precedence);
 
  std::string convert_unary_post(
    const exprt &src, const std::string &symbol,
    unsigned precedence);
 
  std::optional<std::string> convert_function(const exprt &src);
  std::string convert_function(const exprt &src, const std::string &symbol);
 
  std::string convert_complex(
    const exprt &src,
    unsigned precedence);
 
  std::string convert_comma(
    const exprt &src,
    unsigned precedence);
 
  std::string convert_Hoare(const exprt &src);
 
  std::string convert_code(const codet &src);
  virtual std::string convert_code(const codet &src, unsigned indent);
  std::string convert_code_label(const code_labelt &src, unsigned indent);
  // NOLINTNEXTLINE(whitespace/line_length)
  std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent);
  std::string convert_code_asm(const code_asmt &src, unsigned indent);
  std::string
  convert_code_frontend_assign(const code_frontend_assignt &, unsigned indent);
  // NOLINTNEXTLINE(whitespace/line_length)
  std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent);
  std::string convert_code_for(const code_fort &src, unsigned indent);
  std::string convert_code_while(const code_whilet &src, unsigned indent);
  std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent);
  std::string convert_code_block(const code_blockt &src, unsigned indent);
  std::string convert_code_expression(const codet &src, unsigned indent);
  std::string convert_code_return(const codet &src, unsigned indent);
  std::string convert_code_goto(const codet &src, unsigned indent);
  std::string convert_code_assume(const codet &src, unsigned indent);
  std::string convert_code_assert(const codet &src, unsigned indent);
  std::string convert_code_break(unsigned indent);
  std::string convert_code_switch(const codet &src, unsigned indent);
  std::string convert_code_continue(unsigned indent);
  std::string convert_code_frontend_decl(const codet &, unsigned indent);
  std::string convert_code_decl_block(const codet &src, unsigned indent);
  std::string convert_code_dead(const codet &src, unsigned indent);
  // NOLINTNEXTLINE(whitespace/line_length)
  std::string convert_code_function_call(const code_function_callt &src, unsigned indent);
  std::string convert_code_lock(const codet &src, unsigned indent);
  std::string convert_code_unlock(const codet &src, unsigned indent);
  std::string convert_code_printf(const codet &src, unsigned indent);
  std::string convert_code_fence(const codet &src, unsigned indent);
  std::string convert_code_input(const codet &src, unsigned indent);
  std::string convert_code_output(const codet &src, unsigned indent);
  std::string convert_code_array_set(const codet &src, unsigned indent);
  std::string convert_code_array_copy(const codet &src, unsigned indent);
  std::string convert_code_array_replace(const codet &src, unsigned indent);
 
  virtual std::string convert_with_precedence(
    const exprt &src, unsigned &precedence);
 
  std::string
  convert_function_application(const function_application_exprt &src);
  std::string convert_side_effect_expr_function_call(
    const side_effect_expr_function_callt &src);
  std::string convert_allocate(const exprt &src, unsigned &precedence);
  std::string convert_nondet(const exprt &src, unsigned &precedence);
  std::string convert_prob_coin(const exprt &src, unsigned &precedence);
  std::string convert_prob_uniform(const exprt &src, unsigned &precedence);
  // NOLINTNEXTLINE(whitespace/line_length)
  std::string convert_statement_expression(const exprt &src, unsigned &precendence);
 
  virtual std::string convert_symbol(const exprt &src);
  std::string convert_predicate_symbol(const exprt &src);
  std::string convert_predicate_next_symbol(const exprt &src);
  std::string convert_predicate_passive_symbol(const exprt &src);
  std::string convert_nondet_symbol(const nondet_symbol_exprt &);
  std::string convert_quantified_symbol(const exprt &src);
  std::string convert_nondet_bool();
  std::string convert_object_descriptor(const exprt &src, unsigned &precedence);
  std::string convert_literal(const exprt &src);
  // NOLINTNEXTLINE(whitespace/line_length)
  virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence);
  virtual std::string convert_constant_bool(bool boolean_value);
  virtual std::string convert_annotated_pointer_constant(
    const annotated_pointer_constant_exprt &src,
    unsigned &precedence);
 
  std::string convert_norep(const exprt &src, unsigned &precedence);
 
  virtual std::string convert_struct(const exprt &src, unsigned &precedence);
  std::string convert_union(const exprt &src, unsigned &precedence);
  std::string convert_vector(const exprt &src, unsigned &precedence);
  std::string convert_array(const exprt &src);
  std::string convert_array_list(const exprt &src, unsigned &precedence);
  std::string convert_initializer_list(const exprt &src);
  std::string convert_designated_initializer(const exprt &src);
  std::string convert_concatenation(const exprt &src, unsigned &precedence);
  std::string convert_sizeof(const exprt &src, unsigned &precedence);
  std::string convert_let(const let_exprt &, unsigned precedence);
 
  std::string convert_struct(
    const exprt &src,
    unsigned &precedence,
    bool include_padding_components);
 
  std::string convert_conditional_target_group(const exprt &src);
  std::string convert_bitreverse(const bitreverse_exprt &src);
 
  std::string convert_r_or_w_ok(const r_or_w_ok_exprt &src);
  std::string convert_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &src);
  std::string convert_pointer_in_range(const pointer_in_range_exprt &src);
  std::string
  convert_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &src);
};
class expr2ct {…};
 
#endif // CPROVER_ANSI_C_EXPR2C_CLASS_H