ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
solidity_convertert Class Reference

#include <solidity_convert.h>

Classes

struct  func_sig

Public Member Functions

 solidity_convertert (contextt &_context, nlohmann::json &_ast_json, const std::string &_sol_cnts, const std::string &_sol_func, const std::string &_contract_path, const std::string &_focus_func=std::string())
virtual ~solidity_convertert ()=default
bool convert ()
const nlohmann::json & find_decl_ref (int ref_id)
std::string get_sol_contract (const typet &t) const
 Derived rather than read back from #sol_contract: a contract type is a pointer to the contract's own tag-<name> symbol type, and the converter already knows every contract's name, so the name need not ride on the type – which matters because IREP2 has no field for it (docs/roadmap/scope-solidity-irep2.md §8).
bool has_sol_contract (const typet &t) const
void set_sol_state_var (const irep_idt &symbol_id, bool v)
bool get_sol_state_var (const irep_idt &symbol_id) const

Static Public Member Functions

static bool is_low_level_call (const std::string &name)
static bool is_low_level_property (const std::string &name)
static const nlohmann::json & find_last_parent (const nlohmann::json &json, const nlohmann::json &target)
static const nlohmann::json & find_parent_contract (const nlohmann::json &json, const nlohmann::json &target)
static const nlohmann::json & find_node_by_id (const nlohmann::json &subtree, int ref_id)
static const nlohmann::json & find_constructor_ref (int ref_decl_id)
static const nlohmann::json & find_constructor_ref (const std::string &contract_name)
static void set_sol_type (typet &t, SolidityGrammar::SolType st)
static SolidityGrammar::SolType get_sol_type (const typet &t)
static void set_sol_array_size (typet &t, const std::string &size)
static std::string get_sol_array_size (const typet &t)
static bool has_sol_array_size (const typet &t)
static void set_sol_bytesn_size (typet &t, long size)
static void set_sol_bytesn_size (typet &t, const irep_idt &size)
static std::string get_sol_bytesn_size (const typet &t)
static bool has_sol_bytesn_size (const typet &t)
static void set_sol_mapping_array (typet &t, bool v)
static bool get_sol_mapping_array (const typet &t)
static void set_sol_dynarray_state (typet &t, bool v)
static bool get_sol_dynarray_state (const typet &t)

Public Attributes

std::unordered_set< irep_idt > sol_state_vars
 Whether a declared variable is a contract state variable.

Static Public Attributes

static const nlohmann::json empty_json = nlohmann::json::object()
static std::string current_baseContractName = ""
static nlohmann::json src_ast_json = empty_json
static std::unordered_map< std::string, typet > UserDefinedVarMap

Protected Types

typedef struct solidity_convertert::func_sig func_sig

Protected Member Functions

void merge_multi_files ()
void topological_sort (std::unordered_map< std::string, std::unordered_set< std::string > > &graph, std::unordered_map< std::string, nlohmann::json > &path_to_json, nlohmann::json &sorted_files)
bool contract_precheck ()
bool check_sol_ver ()
bool populate_auxiliary_vars ()
bool populate_function_signature (nlohmann::json &json, const std::string &cname)
 initialize the function signature set.
bool populate_low_level_functions (const std::string &cname)
bool convert_ast_nodes (const nlohmann::json &contract_def, const std::string &cname)
void get_cname_expr (const std::string &cname, exprt &new_expr)
bool get_contract_definition (const std::string &c_name)
bool get_non_function_decl (const nlohmann::json &ast_node, exprt &new_expr)
bool get_function_decl (const nlohmann::json &ast_node)
bool get_var_decl (const nlohmann::json &ast_node, const nlohmann::json &initialValue, exprt &new_expr)
bool get_var_decl (const nlohmann::json &ast_node, exprt &new_expr)
bool get_function_definition (const nlohmann::json &ast_node)
bool add_reentry_check (const std::string &c_name, const locationt &loc, exprt &body_exprt)
bool get_func_modifier (const nlohmann::json &ast_node, const std::string &c_name, const std::string &f_name, const std::string &f_id, const bool add_reentry, exprt &body_exprt)
bool has_modifier_invocation (const nlohmann::json &ast_node)
bool insert_modifier_json (const nlohmann::json &ast_node, const std::string &cname, const std::string &fname, nlohmann::json *&modifier_def)
bool delete_modifier_json (const std::string &cname, const std::string &fname, nlohmann::json *&modifier_def)
void get_modifier_function_name (const std::string &cname, const std::string &mod_name, const std::string &func_name, std::string &name, std::string &id)
bool get_function_params (const nlohmann::json &pd, const std::string &cname, exprt &param)
void get_function_this_pointer_param (const std::string &contract_name, const std::string &ctor_id, const std::string &debug_modulename, const locationt &location_begin, code_typet &type)
bool get_unbound_funccall (const std::string contractName, code_function_callt &call)
void get_static_contract_instance_name (const std::string c_name, std::string &name, std::string &id)
void add_static_contract_instance (const std::string c_name)
void get_static_contract_instance_ref (const std::string &c_name, exprt &new_expr)
void get_inherit_static_contract_instance_name (const std::string bs_c_name, const std::string c_name, std::string &name, std::string &id)
void get_inherit_static_contract_instance (const std::string bs_c_name, const std::string c_name, const nlohmann::json &args_list, symbolt &sym)
void get_inherit_ctor_definition (const std::string c_name, exprt &new_expr)
void get_inherit_ctor_definition_name (const std::string c_name, std::string &name, std::string &id)
void get_contract_mutex_name (const std::string c_name, std::string &name, std::string &id)
void get_contract_mutex_expr (const std::string c_name, const exprt &this_expr, exprt &expr)
bool get_high_level_call_wrapper (const std::string c_name, const exprt &this_expr, exprt &front_block, exprt &back_block)
bool is_sol_builin_symbol (const std::string &cname, const std::string &name)
nlohmann::json reorder_arguments (const nlohmann::json &expr, const nlohmann::json &callee_expr_json)
bool get_noncontract_defition (nlohmann::json &ast_node)
bool get_noncontract_decl_ref (const nlohmann::json &ast_node, exprt &new_expr)
bool get_struct_class (const nlohmann::json &ast_node)
void add_enum_member_val (nlohmann::json &ast_node)
bool get_error_definition (const nlohmann::json &ast_node)
void add_empty_body_node (nlohmann::json &ast_node)
void merge_inheritance_ast (const std::string &c_name, nlohmann::json &c_node, std::set< std::string > &merged_list)
void add_inherit_label (nlohmann::json &node, const std::string &cname)
bool get_constructor (const nlohmann::json &ast_node, const std::string &contract_name)
bool add_implicit_constructor (const std::string &contract_name)
bool get_implicit_ctor_ref (const std::string &contract_name, const bool is_object, exprt &new_expr)
bool get_instantiation_ctor_call (const std::string &contract_name, exprt &new_expr)
void move_to_initializer (const exprt &expr)
bool move_initializer_to_ctor (const nlohmann::json *based_contracts, const nlohmann::json &current_contract, const std::string contract_name)
bool move_initializer_to_ctor (const nlohmann::json *based_contracts, const nlohmann::json &current_contract, const std::string contract_name, bool is_aux_ctor)
bool move_initializer_to_main (codet &func_body)
bool move_inheritance_to_ctor (const nlohmann::json *based_contracts, const std::string contract_name, std::string ctor_id, symbolt &sym)
void move_to_front_block (const exprt &expr)
void move_to_back_block (const exprt &expr)
bool get_struct_class_fields (const nlohmann::json &ast_node, struct_typet &type)
bool get_struct_class_method (const nlohmann::json &ast_node, struct_typet &type)
bool get_access_from_decl (const nlohmann::json &ast_node, struct_typet::componentt &comp)
bool get_block (const nlohmann::json &expr, exprt &new_expr)
bool get_statement (const nlohmann::json &block, exprt &new_expr)
bool get_expr (const nlohmann::json &expr, exprt &new_expr)
bool get_expr (const nlohmann::json &expr, const nlohmann::json &expr_common_type, exprt &new_expr)
 Populate the out parameter with the expression based on the solidity expression grammar.
bool get_init_expr (const nlohmann::json &init_value, const nlohmann::json &literal_type, const typet &dest_type, exprt &new_expr)
bool get_decl_ref_expr (const nlohmann::json &expr, exprt &new_expr)
bool get_literal_expr (const nlohmann::json &expr, const nlohmann::json &literal_type, exprt &new_expr)
bool get_tuple_expr (const nlohmann::json &expr, const nlohmann::json &literal_type, exprt &new_expr)
bool get_call_expr (const nlohmann::json &expr, const nlohmann::json &literal_type, exprt &new_expr)
bool get_contract_member_call_expr (const nlohmann::json &expr, const nlohmann::json &literal_type, exprt &new_expr)
bool get_index_access_expr (const nlohmann::json &expr, const nlohmann::json &literal_type, exprt &new_expr)
bool get_index_range_access_expr (const nlohmann::json &expr, const nlohmann::json &literal_type, exprt &new_expr)
bool get_new_object_expr (const nlohmann::json &expr, const nlohmann::json &literal_type, exprt &new_expr)
bool get_binary_operator_expr (const nlohmann::json &expr, exprt &new_expr)
void convert_operand_types (exprt &lhs, exprt &rhs, const typet &common_type, bool is_shift, const nlohmann::json &expr)
bool get_compound_assign_expr (const nlohmann::json &expr, exprt &lhs, exprt &rhs, typet &common_type, exprt &new_expr)
bool get_unary_operator_expr (const nlohmann::json &expr, const nlohmann::json &literal_type, exprt &new_expr)
bool get_conditional_operator_expr (const nlohmann::json &expr, exprt &new_expr)
bool get_cast_expr (const nlohmann::json &cast_expr, exprt &new_expr, const nlohmann::json literal_type=nullptr)
bool get_var_decl_ref (const nlohmann::json &decl, const bool is_this_ptr, exprt &new_expr)
 This function can return expr with either id::symbol or id::member id::memebr can only be the case where this.xx @decl: declaration json node @is_this_ptr: whether we need to convert x => this.x @cname: based contract name.
void get_symbol_decl_ref (const std::string &sym_name, const std::string &sym_id, const typet &t, exprt &new_expr)
bool get_func_decl_ref (const nlohmann::json &decl, exprt &new_expr)
bool get_func_decl_this_ref (const nlohmann::json &decl, exprt &new_expr)
bool get_func_decl_this_ref (const std::string contract_name, const std::string &func_id, exprt &new_expr)
bool get_ctor_decl_this_ref (const nlohmann::json &caller, exprt &this_object)
bool get_ctor_decl_this_ref (const std::string &c_name, exprt &this_object)
bool get_enum_member_ref (const nlohmann::json &decl, exprt &new_expr)
bool get_esbmc_builtin_ref (const nlohmann::json &decl, exprt &new_expr)
bool get_type_description (const nlohmann::json &type_name, typet &new_type)
bool get_type_description (const nlohmann::json &decl, const nlohmann::json &type_name, typet &new_type)
bool get_func_decl_ref_type (const nlohmann::json &decl, typet &new_type)
bool get_array_to_pointer_type (const nlohmann::json &decl, typet &new_type)
bool get_elementary_type_name (const nlohmann::json &type_name, typet &new_type)
bool get_parameter_list (const nlohmann::json &type_name, typet &new_type)
void get_state_var_decl_name (const nlohmann::json &ast_node, const std::string &cname, std::string &name, std::string &id)
void get_local_var_decl_name (const nlohmann::json &ast_node, const std::string &cname, std::string &name, std::string &id)
void get_function_definition_name (const nlohmann::json &ast_node, std::string &name, std::string &id)
void get_error_definition_name (const nlohmann::json &ast_node, std::string &name, std::string &id)
bool get_var_decl_name (const nlohmann::json &decl, std::string &name, std::string &id)
bool get_non_library_function_call (const nlohmann::json &decl_ref, const nlohmann::json &caller, side_effect_expr_function_callt &call)
 call to a non-library function: this.func(); // func(&this)
bool get_super_function_call (const nlohmann::json &member_access, const nlohmann::json &call_expr, exprt &new_expr)
std::string find_contract_name_for_id (int func_id)
bool get_ctor_call (const nlohmann::json &decl_ref, const nlohmann::json &epxr, side_effect_expr_function_callt &call)
bool get_new_object_ctor_call (const nlohmann::json &ast_node, const bool is_object, exprt &new_expr)
bool get_new_object_ctor_call (const std::string &contract_name, const nlohmann::json param_list, const bool is_object, exprt &new_expr)
void get_current_contract_name (const nlohmann::json &ast_node, std::string &contract_name)
bool get_library_function_call (const nlohmann::json &decl_ref, const nlohmann::json &caller, side_effect_expr_function_callt &call, bool skip_first_param=false)
bool get_library_function_call (const exprt &func, const typet &t, const nlohmann::json &decl_ref, const nlohmann::json &caller, side_effect_expr_function_callt &call, bool skip_first_param=false)
void get_library_function_call_no_args (const std::string &func_name, const std::string &func_id, const typet &t, const locationt &l, exprt &new_expr)
void get_malloc_function_call (const locationt &loc, side_effect_expr_function_callt &_call)
void get_calloc_function_call (const locationt &loc, side_effect_expr_function_callt &_call)
void get_arrcpy_function_call (const locationt &loc, side_effect_expr_function_callt &calc_call)
void get_str_assign_function_call (const locationt &loc, side_effect_expr_function_callt &_call)
void get_memcpy_function_call (const locationt &loc, side_effect_expr_function_callt &_call)
bool is_esbmc_library_function (const std::string &id)
bool get_empty_array_ref (const nlohmann::json &ast_node, exprt &new_expr)
void get_unique_name (const std::string &name_prefix, const std::string &id_prefix, std::string &aux_name, std::string &aux_id)
void get_aux_array_name (std::string &aux_name, std::string &aux_id)
void get_aux_array (const exprt &src_expr, const typet &sub_t, exprt &new_expr)
void get_aux_var (std::string &aux_name, std::string &aux_id)
void get_size_expr (const exprt &rhs, exprt &size_expr)
void store_update_dyn_array (const exprt &dyn_arr, const exprt &size_expr, exprt &store_call)
bool check_array_push_pop_length (const nlohmann::json &node)
 Recursively checks whether a Solidity AST node contains any usage of array-specific operations: push, pop, or length, excluding operations on the bytes type.
bool get_tuple_definition (const nlohmann::json &ast_node)
bool get_tuple_instance (const nlohmann::json &ast_node, exprt &new_expr)
void get_tuple_name (const nlohmann::json &ast_node, std::string &name, std::string &id)
bool get_tuple_instance_name (const nlohmann::json &ast_node, std::string &name, std::string &id)
bool get_tuple_function_ref (const nlohmann::json &ast_node, exprt &new_expr)
bool get_tuple_member_call (const irep_idt instance_id, const exprt &comp, exprt &new_expr)
bool construct_tuple_assigments (const nlohmann::json &ast_node, const exprt &lhs, const exprt &rhs)
bool flatten_nested_tuple_assignment (const nlohmann::json &expr, const nlohmann::json &lhs_json, const nlohmann::json &rhs_json)
void get_tuple_assignment (const nlohmann::json &expr, const exprt &lop, exprt rop)
void get_tuple_function_call (const exprt &op)
void get_llc_ret_tuple (symbolt &sym)
void get_string_assignment (const exprt &lhs, const exprt &rhs, exprt &new_expr)
void get_mapping_inf_arr_name (const std::string &cname, const std::string &name, std::string &arr_name, std::string &arr_id)
bool is_mapping_set_lvalue (const nlohmann::json &json)
 @target: target index access child json return true if it's a mapping_set, including assign, assign+, tuple assign... otherwise return false, representing mapping_get
bool get_mapping_key_value_type (const nlohmann::json &map_node, typet &key_t, typet &value_t, SolidityGrammar::SolType &key_sol_type, SolidityGrammar::SolType &val_sol_type)
void gen_mapping_key_typecast (const std::string &c_name, exprt &pos, const locationt &l, const typet &key_type)
void xor_fold_key_to_64bit (exprt &key)
bool get_new_mapping_index_access (const typet &value_t, SolidityGrammar::SolType val_sol_type, bool is_mapping_set, const exprt &array, const exprt &pos, const locationt &location, exprt &new_expr)
 index accesss could either be set or get: x[1] => map_uint_get(&m, 1) x[1] = 2 => map_uint_set(&x, 1, 2) @array: x @pos: 1 @is_mapping_set: true if it's a setValue, otherwise getValue
void get_mapping_struct_function (const typet &struct_t, std::string &struct_contract_name, const side_effect_expr_function_callt &gen_call, exprt &new_expr)
void extract_new_contracts ()
void get_location_from_node (const nlohmann::json &ast_node, locationt &location)
void get_start_location_from_stmt (const nlohmann::json &ast_node, locationt &location)
void get_final_location_from_stmt (const nlohmann::json &ast_node, locationt &location)
unsigned int get_line_number (const nlohmann::json &ast_node, bool final_position=false)
size_t add_offset (const std::string &src, size_t start_position)
std::string get_src_from_json (const nlohmann::json &ast_node)
symbolt * move_symbol_to_context (symbolt &symbol)
bool multi_transaction_verification (const std::string &contractName)
bool multi_contract_verification_bound (std::set< std::string > &tgt_set)
bool multi_contract_verification_unbound (std::set< std::string > &tgt_set)
bool prepare_harness_entry_functions (const std::set< std::string > &cname_set, std::vector< const symbolt * > &entry_syms)
bool register_harness_main (const std::string &sol_id, const codet &func_body)
void reset_auxiliary_vars ()
std::string get_modulename_from_path (std::string path)
std::string get_filename_from_path (std::string path)
void convert_expression_to_code (exprt &expr)
bool check_intrinsic_function (const nlohmann::json &ast_node)
nlohmann::json make_implicit_cast_expr (const nlohmann::json &sub_expr, std::string cast_type)
nlohmann::json make_return_type_from_typet (typet type)
nlohmann::json make_pointee_type (const nlohmann::json &sub_expr)
nlohmann::json make_array_elementary_type (const nlohmann::json &type_descrpt)
nlohmann::json make_array_to_pointer_type (const nlohmann::json &type_descrpt)
std::string get_array_size (const nlohmann::json &type_descrpt)
void get_size_of_expr (const typet &elem_type, exprt &size_of_expr)
bool is_dyn_array (const nlohmann::json &json_in)
bool is_func_sig_cover (const std::string &derived, const std::string &base)
bool is_var_getter_matched (const std::string &cname, const std::string &tname, const typet &ttype)
void get_default_symbol (symbolt &symbol, std::string module_name, typet type, std::string name, std::string id, locationt location)
bool get_constant_value (const int ref_id, std::string &value)
bool get_array_pointer_type (const nlohmann::json &decl, const typet &base_type, typet &new_type)
bool get_ctor_call_id (const std::string &contract_name, std::string &ctor_id)
std::string get_explicit_ctor_call_id (const std::string &contract_name)
std::string get_implict_ctor_call_id (const std::string &contract_name)
bool get_sol_builtin_ref (const nlohmann::json expr, exprt &new_expr)
void get_temporary_object (exprt &call, exprt &new_expr)
bool get_unbound_function (const std::string &c_name, symbolt &sym)
bool get_unbound_expr (const nlohmann::json expr, const std::string &cname, exprt &new_expr)
void convert_unboundcall_nondet (exprt &new_expr, const typet common_type, const locationt &l)
bool add_auxiliary_members (const nlohmann::json &json, const std::string contract_name)
void get_builtin_symbol (const std::string name, const std::string id, const typet t, const locationt &l, const exprt &val, const std::string c_name)
void move_builtin_to_contract (const std::string cname, const exprt &sym, bool is_method)
void move_builtin_to_contract (const std::string cname, const exprt &sym, const std::string &access, bool is_method)
const nlohmann::json & get_func_decl_ref (const std::string &c_name, const std::string &f_name)
void get_builtin_property_expr (const std::string &cname, const std::string &name, const exprt &base, const locationt &loc, exprt &new_expr)
void get_aux_property_function (const std::string &cname, const exprt &addr, const typet &return_t, const locationt &loc, const std::string &property_name, exprt &new_expr)
void get_addr_expr (const std::string &cname, const exprt &base, exprt &new_expr)
void get_new_object (const typet &t, exprt &this_object)
 symbol
bool get_high_level_member_access (const nlohmann::json &expr, const nlohmann::json &literal_type, const exprt &base, const exprt &member, const exprt &_mem_call, const bool is_func_call, exprt &new_expr)
 Conversion: constructor() { this->_ESBMC_bind_cname = get_nondet_cname(); // unless we have a new Base(), then = Base; }.
bool get_high_level_member_access (const nlohmann::json &expr, const exprt &base, const exprt &member, const exprt &_mem_call, const bool is_func_call, exprt &new_expr)
bool get_bound_low_level_call (const nlohmann::json &expr, const nlohmann::json &literal_type, const std::string &mem_name, const exprt &base, exprt &new_expr)
 Resolve a low-level call (.call/.send/.transfer/.delegatecall/.staticcall) in bound mode by finding the enclosing FunctionCall AST node, extracting arguments, and dispatching to get_low_level_member_accsss.
bool get_low_level_member_accsss (const nlohmann::json &expr, const nlohmann::json &options, const std::string mem_name, const exprt &base, const exprt &arg, exprt &new_expr)
 @options: val
bool has_callable_func (const std::string &cname)
bool has_target_function (const std::string &cname, const std::string func_name)
func_sig get_target_function (const std::string &cname, const std::string &func_name)
bool get_call_definition (const std::string &cname, exprt &new_expr)
bool get_call_value_definition (const std::string &cname, exprt &new_expr)
bool try_get_signature_dispatched_call (const nlohmann::json &expr, const nlohmann::json &func_call, const exprt &base, exprt &new_expr)
bool try_get_delegate_shadow_call (const nlohmann::json &expr, const nlohmann::json &func_call, const exprt &base, exprt &new_expr)
bool validate_delegate_shadow_compatible (const std::string &caller_cname, const nlohmann::json &target_body)
void rewrite_returns_for_delegate_shadow (exprt &node, const exprt &ret_lvalue, const std::string &end_label)
bool try_inline_delegate_shadow_helper_call (const nlohmann::json &call_expr, const nlohmann::json &fdecl, exprt &new_expr)
bool extract_abi_encode_signature (const nlohmann::json &payload, std::string &sig_literal, std::vector< const nlohmann::json * > &args_out)
std::string build_canonical_signature (const nlohmann::json &func_def)
const nlohmann::json & find_function_by_signature (const std::string &cname, const std::string &target_sig)
bool get_typed_call_definition (const std::string &caller_cname, const std::string &target_sig, const std::vector< exprt > &arg_exprs, symbolt *&out_sym)
bool get_transfer_definition (const std::string &cname, exprt &new_expr)
bool get_send_definition (const std::string &cname, exprt &new_expr)
bool get_staticcall_definition (const std::string &cname, exprt &new_expr)
bool get_delegatecall_definition (const std::string &cname, exprt &new_expr)
bool model_transaction (const nlohmann::json &expr, const exprt &this_expr, const exprt &base, const exprt &value, const locationt &loc, exprt &front_block, exprt &back_block)
 e.g.
bool get_bind_cname_expr (const nlohmann::json &json, exprt &bind_cname_expr)
void get_bind_cname_func_name (const std::string &cname, std::string &fname, std::string &fid)
void get_nondet_expr (const typet &t, exprt &new_expr)
bool assign_nondet_contract_name (const std::string &_cname, exprt &new_expr)
bool assign_param_nondet (const nlohmann::json &decl_ref, side_effect_expr_function_callt &call)
bool get_base_contract_name (const exprt &base, std::string &cname)
bool convert_integer_literal (const nlohmann::json &integer_literal, std::string the_value, exprt &dest)
bool convert_bool_literal (const nlohmann::json &bool_literal, std::string the_value, exprt &dest)
bool convert_string_literal (std::string the_value, exprt &dest)
 Converts the string literal to a string_constt.
void convert_type_expr (const namespacet &ns, exprt &src_expr, const typet &dest_type, const nlohmann::json &expr)
void convert_type_expr (const namespacet &ns, exprt &src_expr, const exprt &dest_expr, const nlohmann::json &expr)
bool convert_hex_literal (std::string the_value, exprt &dest, const int n=256)
 convert hex-string to uint constant
: the bit width, default 256 (unsignedbv_typet(256))
bool is_byte_type (const typet &t)
bool is_bytes_type (const typet &t)
bool is_bytesN_type (const typet &t)
exprt make_aux_var (exprt &val, const locationt &location)
void get_bytesN_size (const exprt &src_expr, exprt &len_expr)
bool has_contract_bytes (const nlohmann::json &json)
bool get_dynamic_pool (const std::string &c_name, exprt &pool)
bool get_dynamic_pool (const nlohmann::json &expr, exprt &pool)
bool should_treat_as_new (const std::string &contract_name) const

Static Protected Member Functions

static std::string get_library_param_id (const std::string &lib_cname, const std::string &func_name, const std::string &param_name, int param_ast_id)

Protected Attributes

contextt & context
namespacet ns
nlohmann::json src_ast_json_array = nlohmann::json::array()
const std::string & tgt_cnts
std::set< std::string > tgt_cnt_set
const std::string & tgt_func
std::string focus_func
const std::string & contract_path
std::string absolute_path
std::string contract_contents = ""
const nlohmann::json * current_functionDecl
const nlohmann::json * current_forStmt
code_blockt expr_frontBlockDecl
code_blockt expr_backBlockDecl
code_blockt ctor_frontBlockDecl
code_blockt ctor_backBlockDecl
bool current_lhsDecl
bool current_rhsDecl
std::stack< const nlohmann::json * > current_BinOp_type
std::string current_functionName
bool in_unchecked_block = false
std::unordered_map< std::string, std::vector< int > > linearizedBaseList
std::unordered_map< std::string, std::unordered_set< std::string > > inheritanceMap
std::unordered_map< std::string, std::unordered_set< std::string > > structureTypingMap
std::unordered_map< std::string, std::unordered_map< int, int > > overrideMap
std::unordered_map< int, int > storage_ref_aliases
std::unordered_map< int, std::string > delegate_shadow_param_remap
const nlohmann::json * delegate_shadow_target_return_params = nullptr
std::string delegate_shadow_target_cname
std::unordered_map< int, std::string > contractNamesMap
std::vector< std::string > contractNamesList
std::set< std::string > nonContractNamesList
std::set< std::string > newContractSet
std::unordered_map< int, std::string > member_entity_scope
code_blockt initializers
std::unordered_map< std::string, std::vector< func_sig > > funcSignatures
std::string prefix = "tag-"
std::string lib_prefix = "tag-struct "
int aux_counter
bool is_bound
bool is_reentry_check
bool is_pointer_check
side_effect_expr_function_callt nondet_bool_expr
side_effect_expr_function_callt nondet_uint_expr
side_effect_expr_function_callt nondet_bytes_dynamic_expr
typet addr_t
typet addrp_t
typet string_t
typet bool_t
typet byte_dynamic_t
typet byte_static_t

Static Protected Attributes

static constexpr const char * mode = "C++"

Member Typedef Documentation

◆ func_sig

typedef struct solidity_convertert::func_sig solidity_convertert::func_sig
protected

Constructor & Destructor Documentation

◆ solidity_convertert()

solidity_convertert::solidity_convertert ( contextt & _context,
nlohmann::json & _ast_json,
const std::string & _sol_cnts,
const std::string & _sol_func,
const std::string & _contract_path,
const std::string & _focus_func = std::string() )

◆ ~solidity_convertert()

virtual solidity_convertert::~solidity_convertert ( )
virtualdefault

Member Function Documentation

◆ add_auxiliary_members()

bool solidity_convertert::add_auxiliary_members ( const nlohmann::json & json,
const std::string contract_name )
protected

◆ add_empty_body_node()

void solidity_convertert::add_empty_body_node ( nlohmann::json & ast_node)
protected

◆ add_enum_member_val()

void solidity_convertert::add_enum_member_val ( nlohmann::json & ast_node)
protected

◆ add_implicit_constructor()

bool solidity_convertert::add_implicit_constructor ( const std::string & contract_name)
protected

◆ add_inherit_label()

void solidity_convertert::add_inherit_label ( nlohmann::json & node,
const std::string & cname )
protected

◆ add_offset()

size_t solidity_convertert::add_offset ( const std::string & src,
size_t start_position )
protected

◆ add_reentry_check()

bool solidity_convertert::add_reentry_check ( const std::string & c_name,
const locationt & loc,
exprt & body_exprt )
protected

◆ add_static_contract_instance()

void solidity_convertert::add_static_contract_instance ( const std::string c_name)
protected

◆ assign_nondet_contract_name()

bool solidity_convertert::assign_nondet_contract_name ( const std::string & _cname,
exprt & new_expr )
protected

◆ assign_param_nondet()

bool solidity_convertert::assign_param_nondet ( const nlohmann::json & decl_ref,
side_effect_expr_function_callt & call )
protected

specific for string, we need to explicitly assign it as nondet_string()

◆ build_canonical_signature()

std::string solidity_convertert::build_canonical_signature ( const nlohmann::json & func_def)
protected

◆ check_array_push_pop_length()

bool solidity_convertert::check_array_push_pop_length ( const nlohmann::json & node)
protected

Recursively checks whether a Solidity AST node contains any usage of array-specific operations: push, pop, or length, excluding operations on the bytes type.

This function traverses the AST (produced by solc in JSON format) and looks for MemberAccess nodes with member names "push", "pop", or "length". It ensures that these accesses are on array types (e.g., int[], uint256[]) and not on the dynamic bytes type.

Parameters
nodeA JSON node from the Solidity AST.
Returns
true if any array push/pop/length usage is found (excluding bytes).
false otherwise.

◆ check_intrinsic_function()

bool solidity_convertert::check_intrinsic_function ( const nlohmann::json & ast_node)
protected

◆ check_sol_ver()

bool solidity_convertert::check_sol_ver ( )
protected

◆ construct_tuple_assigments()

bool solidity_convertert::construct_tuple_assigments ( const nlohmann::json & ast_node,
const exprt & lhs,
const exprt & rhs )
protected

◆ contract_precheck()

bool solidity_convertert::contract_precheck ( )
protected

◆ convert()

bool solidity_convertert::convert ( )

◆ convert_ast_nodes()

bool solidity_convertert::convert_ast_nodes ( const nlohmann::json & contract_def,
const std::string & cname )
protected

◆ convert_bool_literal()

bool solidity_convertert::convert_bool_literal ( const nlohmann::json & bool_literal,
std::string the_value,
exprt & dest )
protected

◆ convert_expression_to_code()

void solidity_convertert::convert_expression_to_code ( exprt & expr)
protected

◆ convert_hex_literal()

bool solidity_convertert::convert_hex_literal ( std::string the_value,
exprt & dest,
const int n = 256 )
protected

convert hex-string to uint constant
: the bit width, default 256 (unsignedbv_typet(256))

◆ convert_integer_literal()

bool solidity_convertert::convert_integer_literal ( const nlohmann::json & integer_literal,
std::string the_value,
exprt & dest )
protected

◆ convert_operand_types()

void solidity_convertert::convert_operand_types ( exprt & lhs,
exprt & rhs,
const typet & common_type,
bool is_shift,
const nlohmann::json & expr )
protected

◆ convert_string_literal()

bool solidity_convertert::convert_string_literal ( std::string the_value,
exprt & dest )
protected

Converts the string literal to a string_constt.

Parameters
the_valuethe value of the literal
destreturn reference
Returns
true Only if the function fails
false Only if the function successfully converts the literal

◆ convert_type_expr() [1/2]

void solidity_convertert::convert_type_expr ( const namespacet & ns,
exprt & src_expr,
const exprt & dest_expr,
const nlohmann::json & expr )
protected

◆ convert_type_expr() [2/2]

void solidity_convertert::convert_type_expr ( const namespacet & ns,
exprt & src_expr,
const typet & dest_type,
const nlohmann::json & expr )
protected

◆ convert_unboundcall_nondet()

void solidity_convertert::convert_unboundcall_nondet ( exprt & new_expr,
const typet common_type,
const locationt & l )
protected

◆ delete_modifier_json()

bool solidity_convertert::delete_modifier_json ( const std::string & cname,
const std::string & fname,
nlohmann::json *& modifier_def )
protected

◆ extract_abi_encode_signature()

bool solidity_convertert::extract_abi_encode_signature ( const nlohmann::json & payload,
std::string & sig_literal,
std::vector< const nlohmann::json * > & args_out )
protected

◆ extract_new_contracts()

void solidity_convertert::extract_new_contracts ( )
protected

◆ find_constructor_ref() [1/2]

const nlohmann::json & solidity_convertert::find_constructor_ref ( const std::string & contract_name)
static

◆ find_constructor_ref() [2/2]

const nlohmann::json & solidity_convertert::find_constructor_ref ( int ref_decl_id)
static

◆ find_contract_name_for_id()

std::string solidity_convertert::find_contract_name_for_id ( int func_id)
protected

◆ find_decl_ref()

const nlohmann::json & solidity_convertert::find_decl_ref ( int ref_id)

◆ find_function_by_signature()

const nlohmann::json & solidity_convertert::find_function_by_signature ( const std::string & cname,
const std::string & target_sig )
protected

◆ find_last_parent()

const nlohmann::json & solidity_convertert::find_last_parent ( const nlohmann::json & json,
const nlohmann::json & target )
static

◆ find_node_by_id()

const nlohmann::json & solidity_convertert::find_node_by_id ( const nlohmann::json & subtree,
int ref_id )
static

◆ find_parent_contract()

const nlohmann::json & solidity_convertert::find_parent_contract ( const nlohmann::json & json,
const nlohmann::json & target )
static

◆ flatten_nested_tuple_assignment()

bool solidity_convertert::flatten_nested_tuple_assignment ( const nlohmann::json & expr,
const nlohmann::json & lhs_json,
const nlohmann::json & rhs_json )
protected

◆ gen_mapping_key_typecast()

void solidity_convertert::gen_mapping_key_typecast ( const std::string & c_name,
exprt & pos,
const locationt & l,
const typet & key_type )
protected

◆ get_access_from_decl()

bool solidity_convertert::get_access_from_decl ( const nlohmann::json & ast_node,
struct_typet::componentt & comp )
protected

◆ get_addr_expr()

void solidity_convertert::get_addr_expr ( const std::string & cname,
const exprt & base,
exprt & new_expr )
protected

◆ get_array_pointer_type()

bool solidity_convertert::get_array_pointer_type ( const nlohmann::json & decl,
const typet & base_type,
typet & new_type )
protected

◆ get_array_size()

std::string solidity_convertert::get_array_size ( const nlohmann::json & type_descrpt)
protected

◆ get_array_to_pointer_type()

bool solidity_convertert::get_array_to_pointer_type ( const nlohmann::json & decl,
typet & new_type )
protected

◆ get_arrcpy_function_call()

void solidity_convertert::get_arrcpy_function_call ( const locationt & loc,
side_effect_expr_function_callt & calc_call )
protected

◆ get_aux_array()

void solidity_convertert::get_aux_array ( const exprt & src_expr,
const typet & sub_t,
exprt & new_expr )
protected

◆ get_aux_array_name()

void solidity_convertert::get_aux_array_name ( std::string & aux_name,
std::string & aux_id )
protected

◆ get_aux_property_function()

void solidity_convertert::get_aux_property_function ( const std::string & cname,
const exprt & addr,
const typet & return_t,
const locationt & loc,
const std::string & property_name,
exprt & new_expr )
protected

◆ get_aux_var()

void solidity_convertert::get_aux_var ( std::string & aux_name,
std::string & aux_id )
protected

◆ get_base_contract_name()

bool solidity_convertert::get_base_contract_name ( const exprt & base,
std::string & cname )
protected

◆ get_binary_operator_expr()

bool solidity_convertert::get_binary_operator_expr ( const nlohmann::json & expr,
exprt & new_expr )
protected

◆ get_bind_cname_expr()

bool solidity_convertert::get_bind_cname_expr ( const nlohmann::json & json,
exprt & bind_cname_expr )
protected

◆ get_bind_cname_func_name()

void solidity_convertert::get_bind_cname_func_name ( const std::string & cname,
std::string & fname,
std::string & fid )
protected

◆ get_block()

bool solidity_convertert::get_block ( const nlohmann::json & expr,
exprt & new_expr )
protected

◆ get_bound_low_level_call()

bool solidity_convertert::get_bound_low_level_call ( const nlohmann::json & expr,
const nlohmann::json & literal_type,
const std::string & mem_name,
const exprt & base,
exprt & new_expr )
protected

Resolve a low-level call (.call/.send/.transfer/.delegatecall/.staticcall) in bound mode by finding the enclosing FunctionCall AST node, extracting arguments, and dispatching to get_low_level_member_accsss.

e.g. x.call{value: val}("") @base: (this->)x @mem_name: call

◆ get_builtin_property_expr()

void solidity_convertert::get_builtin_property_expr ( const std::string & cname,
const std::string & name,
const exprt & base,
const locationt & loc,
exprt & new_expr )
protected

◆ get_builtin_symbol()

void solidity_convertert::get_builtin_symbol ( const std::string name,
const std::string id,
const typet t,
const locationt & l,
const exprt & val,
const std::string c_name )
protected

◆ get_bytesN_size()

void solidity_convertert::get_bytesN_size ( const exprt & src_expr,
exprt & len_expr )
protected

◆ get_call_definition()

bool solidity_convertert::get_call_definition ( const std::string & cname,
exprt & new_expr )
protected

◆ get_call_expr()

bool solidity_convertert::get_call_expr ( const nlohmann::json & expr,
const nlohmann::json & literal_type,
exprt & new_expr )
protected

◆ get_call_value_definition()

bool solidity_convertert::get_call_value_definition ( const std::string & cname,
exprt & new_expr )
protected

◆ get_calloc_function_call()

void solidity_convertert::get_calloc_function_call ( const locationt & loc,
side_effect_expr_function_callt & _call )
protected

◆ get_cast_expr()

bool solidity_convertert::get_cast_expr ( const nlohmann::json & cast_expr,
exprt & new_expr,
const nlohmann::json literal_type = nullptr )
protected

◆ get_cname_expr()

void solidity_convertert::get_cname_expr ( const std::string & cname,
exprt & new_expr )
protected

◆ get_compound_assign_expr()

bool solidity_convertert::get_compound_assign_expr ( const nlohmann::json & expr,
exprt & lhs,
exprt & rhs,
typet & common_type,
exprt & new_expr )
protected

◆ get_conditional_operator_expr()

bool solidity_convertert::get_conditional_operator_expr ( const nlohmann::json & expr,
exprt & new_expr )
protected

◆ get_constant_value()

bool solidity_convertert::get_constant_value ( const int ref_id,
std::string & value )
protected

◆ get_constructor()

bool solidity_convertert::get_constructor ( const nlohmann::json & ast_node,
const std::string & contract_name )
protected

◆ get_contract_definition()

bool solidity_convertert::get_contract_definition ( const std::string & c_name)
protected

◆ get_contract_member_call_expr()

bool solidity_convertert::get_contract_member_call_expr ( const nlohmann::json & expr,
const nlohmann::json & literal_type,
exprt & new_expr )
protected

◆ get_contract_mutex_expr()

void solidity_convertert::get_contract_mutex_expr ( const std::string c_name,
const exprt & this_expr,
exprt & expr )
protected

◆ get_contract_mutex_name()

void solidity_convertert::get_contract_mutex_name ( const std::string c_name,
std::string & name,
std::string & id )
protected

◆ get_ctor_call()

bool solidity_convertert::get_ctor_call ( const nlohmann::json & decl_ref,
const nlohmann::json & caller,
side_effect_expr_function_callt & call )
protected
Parameters
decl_refthe declaration of the ctor. Can be empty for implicit ctor. @caller: the caller node that might contain the arguments

◆ get_ctor_call_id()

bool solidity_convertert::get_ctor_call_id ( const std::string & contract_name,
std::string & ctor_id )
protected

◆ get_ctor_decl_this_ref() [1/2]

bool solidity_convertert::get_ctor_decl_this_ref ( const nlohmann::json & caller,
exprt & this_object )
protected

◆ get_ctor_decl_this_ref() [2/2]

bool solidity_convertert::get_ctor_decl_this_ref ( const std::string & c_name,
exprt & this_object )
protected

◆ get_current_contract_name()

void solidity_convertert::get_current_contract_name ( const nlohmann::json & ast_node,
std::string & contract_name )
protected

◆ get_decl_ref_expr()

bool solidity_convertert::get_decl_ref_expr ( const nlohmann::json & expr,
exprt & new_expr )
protected

◆ get_default_symbol()

void solidity_convertert::get_default_symbol ( symbolt & symbol,
std::string module_name,
typet type,
std::string name,
std::string id,
locationt location )
protected

◆ get_delegatecall_definition()

bool solidity_convertert::get_delegatecall_definition ( const std::string & cname,
exprt & new_expr )
protected

◆ get_dynamic_pool() [1/2]

bool solidity_convertert::get_dynamic_pool ( const nlohmann::json & expr,
exprt & pool )
protected

◆ get_dynamic_pool() [2/2]

bool solidity_convertert::get_dynamic_pool ( const std::string & c_name,
exprt & pool )
protected

◆ get_elementary_type_name()

bool solidity_convertert::get_elementary_type_name ( const nlohmann::json & type_name,
typet & new_type )
protected

◆ get_empty_array_ref()

bool solidity_convertert::get_empty_array_ref ( const nlohmann::json & ast_node,
exprt & new_expr )
protected

◆ get_enum_member_ref()

bool solidity_convertert::get_enum_member_ref ( const nlohmann::json & decl,
exprt & new_expr )
protected

◆ get_error_definition()

bool solidity_convertert::get_error_definition ( const nlohmann::json & ast_node)
protected

◆ get_error_definition_name()

void solidity_convertert::get_error_definition_name ( const nlohmann::json & ast_node,
std::string & name,
std::string & id )
protected

◆ get_esbmc_builtin_ref()

bool solidity_convertert::get_esbmc_builtin_ref ( const nlohmann::json & decl,
exprt & new_expr )
protected

assume it's a solidity built-in func

◆ get_explicit_ctor_call_id()

std::string solidity_convertert::get_explicit_ctor_call_id ( const std::string & contract_name)
protected

◆ get_expr() [1/2]

bool solidity_convertert::get_expr ( const nlohmann::json & expr,
const nlohmann::json & literal_type,
exprt & new_expr )
protected

Populate the out parameter with the expression based on the solidity expression grammar.

More specifically, parse each expression in the AST json and convert it to a exprt ("new_expr"). The expression may have sub-expression

!Always check if the expression is a Literal before calling get_expr !Unless you are 100% sure it will not be a constant

This function is called through two paths:

  1. get_non_function_decl => get_var_decl => get_expr
  2. get_non_function_decl => get_function_definition => get_statement => get_expr
Parameters
exprThe expression that is to be converted to the IR
literal_typeType information ast to create the the literal type in the IR (only needed for when the expression is a literal). A literal_type is a "typeDescriptions" ast_node. we need this due to some info is missing in the child node.
new_exprOut parameter to hold the conversion
Returns
true iff the conversion has failed
false iff the conversion was successful

note that this will leads to "failed to get current contract name" error

Note that member call like msg.sender will not be handled here

assume: only one argument

◆ get_expr() [2/2]

bool solidity_convertert::get_expr ( const nlohmann::json & expr,
exprt & new_expr )
protected

◆ get_filename_from_path()

std::string solidity_convertert::get_filename_from_path ( std::string path)
protected

◆ get_final_location_from_stmt()

void solidity_convertert::get_final_location_from_stmt ( const nlohmann::json & ast_node,
locationt & location )
protected

◆ get_func_decl_ref() [1/2]

bool solidity_convertert::get_func_decl_ref ( const nlohmann::json & decl,
exprt & new_expr )
protected

function with no value i.e function body

◆ get_func_decl_ref() [2/2]

const nlohmann::json & solidity_convertert::get_func_decl_ref ( const std::string & c_name,
const std::string & f_name )
protected

◆ get_func_decl_ref_type()

bool solidity_convertert::get_func_decl_ref_type ( const nlohmann::json & decl,
typet & new_type )
protected

◆ get_func_decl_this_ref() [1/2]

bool solidity_convertert::get_func_decl_this_ref ( const nlohmann::json & decl,
exprt & new_expr )
protected

◆ get_func_decl_this_ref() [2/2]

bool solidity_convertert::get_func_decl_this_ref ( const std::string contract_name,
const std::string & func_id,
exprt & new_expr )
protected

◆ get_func_modifier()

bool solidity_convertert::get_func_modifier ( const nlohmann::json & ast_node,
const std::string & c_name,
const std::string & f_name,
const std::string & f_id,
const bool add_reentry,
exprt & body_exprt )
protected

◆ get_function_decl()

bool solidity_convertert::get_function_decl ( const nlohmann::json & ast_node)
protected

◆ get_function_definition()

bool solidity_convertert::get_function_definition ( const nlohmann::json & ast_node)
protected

◆ get_function_definition_name()

void solidity_convertert::get_function_definition_name ( const nlohmann::json & ast_node,
std::string & name,
std::string & id )
protected

for event/... who have added an body node. It seems that a ["kind"] is automatically added.?

◆ get_function_params()

bool solidity_convertert::get_function_params ( const nlohmann::json & pd,
const std::string & cname,
exprt & param )
protected

◆ get_function_this_pointer_param()

void solidity_convertert::get_function_this_pointer_param ( const std::string & contract_name,
const std::string & ctor_id,
const std::string & debug_modulename,
const locationt & location_begin,
code_typet & type )
protected

◆ get_high_level_call_wrapper()

bool solidity_convertert::get_high_level_call_wrapper ( const std::string c_name,
const exprt & this_expr,
exprt & front_block,
exprt & back_block )
protected

◆ get_high_level_member_access() [1/2]

bool solidity_convertert::get_high_level_member_access ( const nlohmann::json & expr,
const exprt & base,
const exprt & member,
const exprt & _mem_call,
const bool is_func_call,
exprt & new_expr )
protected

◆ get_high_level_member_access() [2/2]

bool solidity_convertert::get_high_level_member_access ( const nlohmann::json & expr,
const nlohmann::json & options,
const exprt & base,
const exprt & member,
const exprt & _mem_call,
const bool is_func_call,
exprt & new_expr )
protected

Conversion: constructor() { this->_ESBMC_bind_cname = get_nondet_cname(); // unless we have a new Base(), then = Base; }.

function test1(Base x, address _addr) public { x = new Base(); // x._ESBMC_bind_cname = Base; x.test(); // if x._ESBMC_bind_cname == base _ESBMC_Object_base.test(); x = Base(_addr); // x = ESBMC_Object_base if _addr == _ESBMC_Object_base.$address x._ESBMC_bind_cname = base if _addr == _ESBMC_Object_y.$address x._ESBMC_bind_cname = y; }

the auxilidary tmp var will not be created if the member_type is void @expr: the whole member access expression json @options: call with options @is_func_call: true if it's a function member access; false state variable access @_mem_call: function call statement, with arguments populated return true: we fail to generate the high_level_member_access bound harness however, this should not be treated as an erorr. E.g. x.access() where x is a state variable

we need to move it to the struct symbol

◆ get_implicit_ctor_ref()

bool solidity_convertert::get_implicit_ctor_ref ( const std::string & contract_name,
const bool is_object,
exprt & new_expr )
protected

◆ get_implict_ctor_call_id()

std::string solidity_convertert::get_implict_ctor_call_id ( const std::string & contract_name)
protected

◆ get_index_access_expr()

bool solidity_convertert::get_index_access_expr ( const nlohmann::json & expr,
const nlohmann::json & literal_type,
exprt & new_expr )
protected

◆ get_index_range_access_expr()

bool solidity_convertert::get_index_range_access_expr ( const nlohmann::json & expr,
const nlohmann::json & literal_type,
exprt & new_expr )
protected

◆ get_inherit_ctor_definition()

void solidity_convertert::get_inherit_ctor_definition ( const std::string c_name,
exprt & new_expr )
protected

◆ get_inherit_ctor_definition_name()

void solidity_convertert::get_inherit_ctor_definition_name ( const std::string c_name,
std::string & name,
std::string & id )
protected

◆ get_inherit_static_contract_instance()

void solidity_convertert::get_inherit_static_contract_instance ( const std::string bs_c_name,
const std::string c_name,
const nlohmann::json & args_list,
symbolt & sym )
protected

◆ get_inherit_static_contract_instance_name()

void solidity_convertert::get_inherit_static_contract_instance_name ( const std::string bs_c_name,
const std::string c_name,
std::string & name,
std::string & id )
protected

◆ get_init_expr()

bool solidity_convertert::get_init_expr ( const nlohmann::json & init_value,
const nlohmann::json & literal_type,
const typet & dest_type,
exprt & new_expr )
protected

◆ get_instantiation_ctor_call()

bool solidity_convertert::get_instantiation_ctor_call ( const std::string & contract_name,
exprt & new_expr )
protected

◆ get_library_function_call() [1/2]

bool solidity_convertert::get_library_function_call ( const exprt & func,
const typet & t,
const nlohmann::json & decl_ref,
const nlohmann::json & caller,
side_effect_expr_function_callt & call,
bool skip_first_param = false )
protected

◆ get_library_function_call() [2/2]

bool solidity_convertert::get_library_function_call ( const nlohmann::json & decl_ref,
const nlohmann::json & caller,
side_effect_expr_function_callt & call,
bool skip_first_param = false )
protected

◆ get_library_function_call_no_args()

void solidity_convertert::get_library_function_call_no_args ( const std::string & func_name,
const std::string & func_id,
const typet & t,
const locationt & l,
exprt & new_expr )
protected

◆ get_library_param_id()

std::string solidity_convertert::get_library_param_id ( const std::string & lib_cname,
const std::string & func_name,
const std::string & param_name,
int param_ast_id )
staticprotected

◆ get_line_number()

unsigned int solidity_convertert::get_line_number ( const nlohmann::json & ast_node,
bool final_position = false )
protected

◆ get_literal_expr()

bool solidity_convertert::get_literal_expr ( const nlohmann::json & expr,
const nlohmann::json & literal_type,
exprt & new_expr )
protected

◆ get_llc_ret_tuple()

void solidity_convertert::get_llc_ret_tuple ( symbolt & sym)
protected

◆ get_local_var_decl_name()

void solidity_convertert::get_local_var_decl_name ( const nlohmann::json & ast_node,
const std::string & cname,
std::string & name,
std::string & id )
protected

Assume it is a variable inside struct/error which can be declared outside the contract

◆ get_location_from_node()

void solidity_convertert::get_location_from_node ( const nlohmann::json & ast_node,
locationt & location )
protected

◆ get_low_level_member_accsss()

bool solidity_convertert::get_low_level_member_accsss ( const nlohmann::json & expr,
const nlohmann::json & options,
const std::string mem_name,
const exprt & base,
const exprt & arg,
exprt & new_expr )
protected

@options: val

  • : ""

◆ get_malloc_function_call()

void solidity_convertert::get_malloc_function_call ( const locationt & loc,
side_effect_expr_function_callt & _call )
protected

◆ get_mapping_inf_arr_name()

void solidity_convertert::get_mapping_inf_arr_name ( const std::string & cname,
const std::string & name,
std::string & arr_name,
std::string & arr_id )
protected

◆ get_mapping_key_value_type()

bool solidity_convertert::get_mapping_key_value_type ( const nlohmann::json & map_node,
typet & key_t,
typet & value_t,
SolidityGrammar::SolType & key_sol_type,
SolidityGrammar::SolType & val_sol_type )
protected

◆ get_mapping_struct_function()

void solidity_convertert::get_mapping_struct_function ( const typet & struct_t,
std::string & struct_contract_name,
const side_effect_expr_function_callt & gen_call,
exprt & new_expr )
protected

◆ get_memcpy_function_call()

void solidity_convertert::get_memcpy_function_call ( const locationt & loc,
side_effect_expr_function_callt & _call )
protected

◆ get_modifier_function_name()

void solidity_convertert::get_modifier_function_name ( const std::string & cname,
const std::string & mod_name,
const std::string & func_name,
std::string & name,
std::string & id )
protected

◆ get_modulename_from_path()

std::string solidity_convertert::get_modulename_from_path ( std::string path)
protected

◆ get_new_mapping_index_access()

bool solidity_convertert::get_new_mapping_index_access ( const typet & value_t,
SolidityGrammar::SolType val_sol_type,
bool is_mapping_set,
const exprt & array,
const exprt & pos,
const locationt & location,
exprt & new_expr )
protected

index accesss could either be set or get: x[1] => map_uint_get(&m, 1) x[1] = 2 => map_uint_set(&x, 1, 2) @array: x @pos: 1 @is_mapping_set: true if it's a setValue, otherwise getValue

◆ get_new_object()

void solidity_convertert::get_new_object ( const typet & t,
exprt & this_object )
protected

symbol

  • identifier: tag-Bank

◆ get_new_object_ctor_call() [1/2]

bool solidity_convertert::get_new_object_ctor_call ( const nlohmann::json & ast_node,
const bool is_object,
exprt & new_expr )
protected

◆ get_new_object_ctor_call() [2/2]

bool solidity_convertert::get_new_object_ctor_call ( const std::string & contract_name,
const nlohmann::json param_list,
const bool is_object,
exprt & new_expr )
protected

◆ get_new_object_expr()

bool solidity_convertert::get_new_object_expr ( const nlohmann::json & expr,
const nlohmann::json & literal_type,
exprt & new_expr )
protected

◆ get_non_function_decl()

bool solidity_convertert::get_non_function_decl ( const nlohmann::json & ast_node,
exprt & new_expr )
protected

◆ get_non_library_function_call()

bool solidity_convertert::get_non_library_function_call ( const nlohmann::json & decl_ref,
const nlohmann::json & caller,
side_effect_expr_function_callt & call )
protected

call to a non-library function: this.func(); // func(&this)

Parameters
decl_refthe function declaration node
callerthe function caller node which contains the arguments TODO: if the paramenter is a 'memory' type, we need to create a copy. E.g. string memory x => char *x => char * x_cpy this could be done by memcpy. However, for dyn_array, we do not have the size info. Thus in the future we need to convert the dyn array to a struct which record both array and size. This will also help us to support array.length, .push and .pop

◆ get_noncontract_decl_ref()

bool solidity_convertert::get_noncontract_decl_ref ( const nlohmann::json & ast_node,
exprt & new_expr )
protected

◆ get_noncontract_defition()

bool solidity_convertert::get_noncontract_defition ( nlohmann::json & ast_node)
protected

◆ get_nondet_expr()

void solidity_convertert::get_nondet_expr ( const typet & t,
exprt & new_expr )
protected

◆ get_parameter_list()

bool solidity_convertert::get_parameter_list ( const nlohmann::json & type_name,
typet & new_type )
protected

◆ get_send_definition()

bool solidity_convertert::get_send_definition ( const std::string & cname,
exprt & new_expr )
protected

"ifthenelse" has to be declared as codet, not exprt and use convert_expr_to_code

◆ get_size_expr()

void solidity_convertert::get_size_expr ( const exprt & rhs,
exprt & size_expr )
protected

◆ get_size_of_expr()

void solidity_convertert::get_size_of_expr ( const typet & elem_type,
exprt & size_of_expr )
protected

◆ get_sol_array_size()

std::string solidity_convertert::get_sol_array_size ( const typet & t)
inlinestatic

◆ get_sol_builtin_ref()

bool solidity_convertert::get_sol_builtin_ref ( const nlohmann::json expr,
exprt & new_expr )
protected

◆ get_sol_bytesn_size()

std::string solidity_convertert::get_sol_bytesn_size ( const typet & t)
inlinestatic

◆ get_sol_contract()

std::string solidity_convertert::get_sol_contract ( const typet & t) const
inline

Derived rather than read back from #sol_contract: a contract type is a pointer to the contract's own tag-<name> symbol type, and the converter already knows every contract's name, so the name need not ride on the type – which matters because IREP2 has no field for it (docs/roadmap/scope-solidity-irep2.md §8).

◆ get_sol_dynarray_state()

bool solidity_convertert::get_sol_dynarray_state ( const typet & t)
inlinestatic

◆ get_sol_mapping_array()

bool solidity_convertert::get_sol_mapping_array ( const typet & t)
inlinestatic

◆ get_sol_state_var()

bool solidity_convertert::get_sol_state_var ( const irep_idt & symbol_id) const
inline

◆ get_sol_type()

SolidityGrammar::SolType solidity_convertert::get_sol_type ( const typet & t)
inlinestatic

◆ get_src_from_json()

std::string solidity_convertert::get_src_from_json ( const nlohmann::json & ast_node)
protected

◆ get_start_location_from_stmt()

void solidity_convertert::get_start_location_from_stmt ( const nlohmann::json & ast_node,
locationt & location )
protected

◆ get_state_var_decl_name()

void solidity_convertert::get_state_var_decl_name ( const nlohmann::json & ast_node,
const std::string & cname,
std::string & name,
std::string & id )
protected

◆ get_statement()

bool solidity_convertert::get_statement ( const nlohmann::json & block,
exprt & new_expr )
protected

◆ get_static_contract_instance_name()

void solidity_convertert::get_static_contract_instance_name ( const std::string c_name,
std::string & name,
std::string & id )
protected

◆ get_static_contract_instance_ref()

void solidity_convertert::get_static_contract_instance_ref ( const std::string & c_name,
exprt & new_expr )
protected

◆ get_staticcall_definition()

bool solidity_convertert::get_staticcall_definition ( const std::string & cname,
exprt & new_expr )
protected

◆ get_str_assign_function_call()

void solidity_convertert::get_str_assign_function_call ( const locationt & loc,
side_effect_expr_function_callt & _call )
protected

◆ get_string_assignment()

void solidity_convertert::get_string_assignment ( const exprt & lhs,
const exprt & rhs,
exprt & new_expr )
protected

◆ get_struct_class()

bool solidity_convertert::get_struct_class ( const nlohmann::json & ast_node)
protected

◆ get_struct_class_fields()

bool solidity_convertert::get_struct_class_fields ( const nlohmann::json & ast_node,
struct_typet & type )
protected

◆ get_struct_class_method()

bool solidity_convertert::get_struct_class_method ( const nlohmann::json & ast_node,
struct_typet & type )
protected

◆ get_super_function_call()

bool solidity_convertert::get_super_function_call ( const nlohmann::json & member_access,
const nlohmann::json & call_expr,
exprt & new_expr )
protected

◆ get_symbol_decl_ref()

void solidity_convertert::get_symbol_decl_ref ( const std::string & sym_name,
const std::string & sym_id,
const typet & t,
exprt & new_expr )
protected

◆ get_target_function()

solidity_convertert::func_sig solidity_convertert::get_target_function ( const std::string & cname,
const std::string & func_name )
protected

◆ get_temporary_object()

void solidity_convertert::get_temporary_object ( exprt & call,
exprt & new_expr )
protected

◆ get_transfer_definition()

bool solidity_convertert::get_transfer_definition ( const std::string & cname,
exprt & new_expr )
protected

Do not use gen_one(bool_type()) to replace true_exprt() it will make the verification process stuck somehow

◆ get_tuple_assignment()

void solidity_convertert::get_tuple_assignment ( const nlohmann::json & expr,
const exprt & lop,
exprt rop )
protected

◆ get_tuple_definition()

bool solidity_convertert::get_tuple_definition ( const nlohmann::json & ast_node)
protected

◆ get_tuple_expr()

bool solidity_convertert::get_tuple_expr ( const nlohmann::json & expr,
const nlohmann::json & literal_type,
exprt & new_expr )
protected

◆ get_tuple_function_call()

void solidity_convertert::get_tuple_function_call ( const exprt & op)
protected

◆ get_tuple_function_ref()

bool solidity_convertert::get_tuple_function_ref ( const nlohmann::json & ast_node,
exprt & new_expr )
protected

◆ get_tuple_instance()

bool solidity_convertert::get_tuple_instance ( const nlohmann::json & ast_node,
exprt & new_expr )
protected

◆ get_tuple_instance_name()

bool solidity_convertert::get_tuple_instance_name ( const nlohmann::json & ast_node,
std::string & name,
std::string & id )
protected

◆ get_tuple_member_call()

bool solidity_convertert::get_tuple_member_call ( const irep_idt instance_id,
const exprt & comp,
exprt & new_expr )
protected

◆ get_tuple_name()

void solidity_convertert::get_tuple_name ( const nlohmann::json & ast_node,
std::string & name,
std::string & id )
protected

◆ get_type_description() [1/2]

bool solidity_convertert::get_type_description ( const nlohmann::json & decl,
const nlohmann::json & type_name,
typet & new_type )
protected

◆ get_type_description() [2/2]

bool solidity_convertert::get_type_description ( const nlohmann::json & type_name,
typet & new_type )
protected

◆ get_typed_call_definition()

bool solidity_convertert::get_typed_call_definition ( const std::string & caller_cname,
const std::string & target_sig,
const std::vector< exprt > & arg_exprs,
symbolt *& out_sym )
protected

◆ get_unary_operator_expr()

bool solidity_convertert::get_unary_operator_expr ( const nlohmann::json & expr,
const nlohmann::json & literal_type,
exprt & new_expr )
protected

◆ get_unbound_expr()

bool solidity_convertert::get_unbound_expr ( const nlohmann::json expr,
const std::string & cname,
exprt & new_expr )
protected

◆ get_unbound_funccall()

bool solidity_convertert::get_unbound_funccall ( const std::string contractName,
code_function_callt & call )
protected

◆ get_unbound_function()

bool solidity_convertert::get_unbound_function ( const std::string & c_name,
symbolt & sym )
protected

◆ get_unique_name()

void solidity_convertert::get_unique_name ( const std::string & name_prefix,
const std::string & id_prefix,
std::string & aux_name,
std::string & aux_id )
protected

◆ get_var_decl() [1/2]

bool solidity_convertert::get_var_decl ( const nlohmann::json & ast_node,
const nlohmann::json & initialValue,
exprt & new_expr )
protected 
  uint[2] z;            // uint *z = (uint *)calloc(2, sizeof(uint));

uint tmp1[2] = {1,2}; // populated into sym tab, not a real statement uint[2] zz = [1,2]; // uint *zz = (uint )_ESBMC_arrcpy(tmp1, 2, 2, sizeof(uint));

uint[2] y = x; // uint *zz = (uint *)_ESBMC_arrcpy(x, 2, 2, sizeof(uint));

TODO: suport disorder: uint[2] y = x; uint[2] x = [1,2];

  uint[] zzz;           // uint* zzz; // will not reach here actually

  uint[] zzzz = [1,2];  // memcpy(zzzz, tmp2, 2*sizeof(uint));

uint* zzzzz = 0; uint[] zzzzzz = zzz; // memcpy(zzzzzz, zzz, zzz.size * sizeof(uint));

Theoretically we can convert it to something like int *z = new int[2]{0,1}; However, this feature seems to be not fully supported in current esbmc-cpp (v7.6.1)

◆ get_var_decl() [2/2]

bool solidity_convertert::get_var_decl ( const nlohmann::json & ast_node,
exprt & new_expr )
protected

◆ get_var_decl_name()

bool solidity_convertert::get_var_decl_name ( const nlohmann::json & decl,
std::string & name,
std::string & id )
protected

◆ get_var_decl_ref()

bool solidity_convertert::get_var_decl_ref ( const nlohmann::json & decl,
const bool is_this_ptr,
exprt & new_expr )
protected

This function can return expr with either id::symbol or id::member id::memebr can only be the case where this.xx @decl: declaration json node @is_this_ptr: whether we need to convert x => this.x @cname: based contract name.

◆ has_callable_func()

bool solidity_convertert::has_callable_func ( const std::string & cname)
protected

◆ has_contract_bytes()

bool solidity_convertert::has_contract_bytes ( const nlohmann::json & json)
protected

◆ has_modifier_invocation()

bool solidity_convertert::has_modifier_invocation ( const nlohmann::json & ast_node)
protected

◆ has_sol_array_size()

bool solidity_convertert::has_sol_array_size ( const typet & t)
inlinestatic

◆ has_sol_bytesn_size()

bool solidity_convertert::has_sol_bytesn_size ( const typet & t)
inlinestatic

◆ has_sol_contract()

bool solidity_convertert::has_sol_contract ( const typet & t) const
inline

◆ has_target_function()

bool solidity_convertert::has_target_function ( const std::string & cname,
const std::string func_name )
protected

◆ insert_modifier_json()

bool solidity_convertert::insert_modifier_json ( const nlohmann::json & ast_node,
const std::string & cname,
const std::string & fname,
nlohmann::json *& modifier_def )
protected

◆ is_byte_type()

bool solidity_convertert::is_byte_type ( const typet & t)
protected

◆ is_bytes_type()

bool solidity_convertert::is_bytes_type ( const typet & t)
protected

◆ is_bytesN_type()

bool solidity_convertert::is_bytesN_type ( const typet & t)
protected

◆ is_dyn_array()

bool solidity_convertert::is_dyn_array ( const nlohmann::json & json_in)
protected

◆ is_esbmc_library_function()

bool solidity_convertert::is_esbmc_library_function ( const std::string & id)
protected

◆ is_func_sig_cover()

bool solidity_convertert::is_func_sig_cover ( const std::string & derived,
const std::string & base )
protected

◆ is_low_level_call()

bool solidity_convertert::is_low_level_call ( const std::string & name)
static

◆ is_low_level_property()

bool solidity_convertert::is_low_level_property ( const std::string & name)
static

◆ is_mapping_set_lvalue()

bool solidity_convertert::is_mapping_set_lvalue ( const nlohmann::json & json)
protected

@target: target index access child json return true if it's a mapping_set, including assign, assign+, tuple assign... otherwise return false, representing mapping_get

◆ is_sol_builin_symbol()

bool solidity_convertert::is_sol_builin_symbol ( const std::string & cname,
const std::string & name )
protected

◆ is_var_getter_matched()

bool solidity_convertert::is_var_getter_matched ( const std::string & cname,
const std::string & tname,
const typet & ttype )
protected

◆ make_array_elementary_type()

nlohmann::json solidity_convertert::make_array_elementary_type ( const nlohmann::json & type_descrpt)
protected

current implement does not consider Multi-Dimensional Arrays

◆ make_array_to_pointer_type()

nlohmann::json solidity_convertert::make_array_to_pointer_type ( const nlohmann::json & type_descrpt)
protected

◆ make_aux_var()

exprt solidity_convertert::make_aux_var ( exprt & val,
const locationt & location )
protected

◆ make_implicit_cast_expr()

nlohmann::json solidity_convertert::make_implicit_cast_expr ( const nlohmann::json & sub_expr,
std::string cast_type )
protected

◆ make_pointee_type()

nlohmann::json solidity_convertert::make_pointee_type ( const nlohmann::json & sub_expr)
protected

◆ make_return_type_from_typet()

nlohmann::json solidity_convertert::make_return_type_from_typet ( typet type)
protected

◆ merge_inheritance_ast()

void solidity_convertert::merge_inheritance_ast ( const std::string & c_name,
nlohmann::json & c_node,
std::set< std::string > & merged_list )
protected

receive/fallback can be inherited but cannot be override.

◆ merge_multi_files()

void solidity_convertert::merge_multi_files ( )
protected

◆ model_transaction()

bool solidity_convertert::model_transaction ( const nlohmann::json & expr,
const exprt & this_expr,
const exprt & base,
const exprt & value,
const locationt & loc,
exprt & front_block,
exprt & back_block )
protected

e.g.

x = target.deposit{value: msg.value}() @expr: member_call json @this_expr: this->(target) @base: target @value: msg.value @block: returns

◆ move_builtin_to_contract() [1/2]

void solidity_convertert::move_builtin_to_contract ( const std::string cname,
const exprt & sym,
bool is_method )
protected

◆ move_builtin_to_contract() [2/2]

void solidity_convertert::move_builtin_to_contract ( const std::string cname,
const exprt & sym,
const std::string & access,
bool is_method )
protected

◆ move_inheritance_to_ctor()

bool solidity_convertert::move_inheritance_to_ctor ( const nlohmann::json * based_contracts,
const std::string contract_name,
std::string ctor_id,
symbolt & sym )
protected

◆ move_initializer_to_ctor() [1/2]

bool solidity_convertert::move_initializer_to_ctor ( const nlohmann::json * based_contracts,
const nlohmann::json & current_contract,
const std::string contract_name )
protected

◆ move_initializer_to_ctor() [2/2]

bool solidity_convertert::move_initializer_to_ctor ( const nlohmann::json * based_contracts,
const nlohmann::json & current_contract,
const std::string contract_name,
bool is_aux_ctor )
protected

◆ move_initializer_to_main()

bool solidity_convertert::move_initializer_to_main ( codet & func_body)
protected

◆ move_symbol_to_context()

symbolt * solidity_convertert::move_symbol_to_context ( symbolt & symbol)
protected

◆ move_to_back_block()

void solidity_convertert::move_to_back_block ( const exprt & expr)
protected

◆ move_to_front_block()

void solidity_convertert::move_to_front_block ( const exprt & expr)
protected

◆ move_to_initializer()

void solidity_convertert::move_to_initializer ( const exprt & expr)
protected

◆ multi_contract_verification_bound()

bool solidity_convertert::multi_contract_verification_bound ( std::set< std::string > & tgt_set)
protected

◆ multi_contract_verification_unbound()

bool solidity_convertert::multi_contract_verification_unbound ( std::set< std::string > & tgt_set)
protected

◆ multi_transaction_verification()

bool solidity_convertert::multi_transaction_verification ( const std::string & contractName)
protected

◆ populate_auxiliary_vars()

bool solidity_convertert::populate_auxiliary_vars ( )
protected

◆ populate_function_signature()

bool solidity_convertert::populate_function_signature ( nlohmann::json & json,
const std::string & cname )
protected

initialize the function signature set.

Additionally, we merge inherited nodes. @json: parsing contract json @cname: parsing contract name

◆ populate_low_level_functions()

bool solidity_convertert::populate_low_level_functions ( const std::string & cname)
protected

◆ prepare_harness_entry_functions()

bool solidity_convertert::prepare_harness_entry_functions ( const std::set< std::string > & cname_set,
std::vector< const symbolt * > & entry_syms )
protected

◆ register_harness_main()

bool solidity_convertert::register_harness_main ( const std::string & sol_id,
const codet & func_body )
protected

◆ reorder_arguments()

nlohmann::json solidity_convertert::reorder_arguments ( const nlohmann::json & expr,
const nlohmann::json & callee_expr_json )
protected

◆ reset_auxiliary_vars()

void solidity_convertert::reset_auxiliary_vars ( )
protected

◆ rewrite_returns_for_delegate_shadow()

void solidity_convertert::rewrite_returns_for_delegate_shadow ( exprt & node,
const exprt & ret_lvalue,
const std::string & end_label )
protected

◆ set_sol_array_size()

void solidity_convertert::set_sol_array_size ( typet & t,
const std::string & size )
inlinestatic

◆ set_sol_bytesn_size() [1/2]

void solidity_convertert::set_sol_bytesn_size ( typet & t,
const irep_idt & size )
inlinestatic

◆ set_sol_bytesn_size() [2/2]

void solidity_convertert::set_sol_bytesn_size ( typet & t,
long size )
inlinestatic

◆ set_sol_dynarray_state()

void solidity_convertert::set_sol_dynarray_state ( typet & t,
bool v )
inlinestatic

◆ set_sol_mapping_array()

void solidity_convertert::set_sol_mapping_array ( typet & t,
bool v )
inlinestatic

◆ set_sol_state_var()

void solidity_convertert::set_sol_state_var ( const irep_idt & symbol_id,
bool v )
inline

◆ set_sol_type()

void solidity_convertert::set_sol_type ( typet & t,
SolidityGrammar::SolType st )
inlinestatic

◆ should_treat_as_new()

bool solidity_convertert::should_treat_as_new ( const std::string & contract_name) const
inlineprotected

◆ store_update_dyn_array()

void solidity_convertert::store_update_dyn_array ( const exprt & dyn_arr,
const exprt & size_expr,
exprt & store_call )
protected

◆ topological_sort()

void solidity_convertert::topological_sort ( std::unordered_map< std::string, std::unordered_set< std::string > > & graph,
std::unordered_map< std::string, nlohmann::json > & path_to_json,
nlohmann::json & sorted_files )
protected

◆ try_get_delegate_shadow_call()

bool solidity_convertert::try_get_delegate_shadow_call ( const nlohmann::json & expr,
const nlohmann::json & func_call,
const exprt & base,
exprt & new_expr )
protected

◆ try_get_signature_dispatched_call()

bool solidity_convertert::try_get_signature_dispatched_call ( const nlohmann::json & expr,
const nlohmann::json & func_call,
const exprt & base,
exprt & new_expr )
protected

◆ try_inline_delegate_shadow_helper_call()

bool solidity_convertert::try_inline_delegate_shadow_helper_call ( const nlohmann::json & call_expr,
const nlohmann::json & fdecl,
exprt & new_expr )
protected

◆ validate_delegate_shadow_compatible()

bool solidity_convertert::validate_delegate_shadow_compatible ( const std::string & caller_cname,
const nlohmann::json & target_body )
protected

◆ xor_fold_key_to_64bit()

void solidity_convertert::xor_fold_key_to_64bit ( exprt & key)
protected

Member Data Documentation

◆ absolute_path

std::string solidity_convertert::absolute_path
protected

◆ addr_t

typet solidity_convertert::addr_t
protected

◆ addrp_t

typet solidity_convertert::addrp_t
protected

◆ aux_counter

int solidity_convertert::aux_counter
protected

◆ bool_t

typet solidity_convertert::bool_t
protected

◆ byte_dynamic_t

typet solidity_convertert::byte_dynamic_t
protected

◆ byte_static_t

typet solidity_convertert::byte_static_t
protected

◆ context

contextt& solidity_convertert::context
protected

◆ contract_contents

std::string solidity_convertert::contract_contents = ""
protected

◆ contract_path

const std::string& solidity_convertert::contract_path
protected

◆ contractNamesList

std::vector<std::string> solidity_convertert::contractNamesList
protected

◆ contractNamesMap

std::unordered_map<int, std::string> solidity_convertert::contractNamesMap
protected

◆ ctor_backBlockDecl

code_blockt solidity_convertert::ctor_backBlockDecl
protected

◆ ctor_frontBlockDecl

code_blockt solidity_convertert::ctor_frontBlockDecl
protected

◆ current_baseContractName

std::string solidity_convertert::current_baseContractName = ""
static

Be careful of using 'current_contractName'. This might lead to trouble in inheritance. If you are not sure, use 'get_current_contract_name' instead.

◆ current_BinOp_type

std::stack<const nlohmann::json *> solidity_convertert::current_BinOp_type
protected

◆ current_forStmt

const nlohmann::json* solidity_convertert::current_forStmt
protected

◆ current_functionDecl

const nlohmann::json* solidity_convertert::current_functionDecl
protected

◆ current_functionName

std::string solidity_convertert::current_functionName
protected

◆ current_lhsDecl

bool solidity_convertert::current_lhsDecl
protected

◆ current_rhsDecl

bool solidity_convertert::current_rhsDecl
protected

◆ delegate_shadow_param_remap

std::unordered_map<int, std::string> solidity_convertert::delegate_shadow_param_remap
protected

◆ delegate_shadow_target_cname

std::string solidity_convertert::delegate_shadow_target_cname
protected

◆ delegate_shadow_target_return_params

const nlohmann::json* solidity_convertert::delegate_shadow_target_return_params = nullptr
protected

◆ empty_json

const nlohmann::json solidity_convertert::empty_json = nlohmann::json::object()
static

◆ expr_backBlockDecl

code_blockt solidity_convertert::expr_backBlockDecl
protected

◆ expr_frontBlockDecl

code_blockt solidity_convertert::expr_frontBlockDecl
protected

◆ focus_func

std::string solidity_convertert::focus_func
protected

◆ funcSignatures

std::unordered_map<std::string, std::vector<func_sig> > solidity_convertert::funcSignatures
protected

◆ in_unchecked_block

bool solidity_convertert::in_unchecked_block = false
protected

◆ inheritanceMap

std::unordered_map<std::string, std::unordered_set<std::string> > solidity_convertert::inheritanceMap
protected

◆ initializers

code_blockt solidity_convertert::initializers
protected

◆ is_bound

bool solidity_convertert::is_bound
protected

◆ is_pointer_check

bool solidity_convertert::is_pointer_check
protected

◆ is_reentry_check

bool solidity_convertert::is_reentry_check
protected

◆ lib_prefix

std::string solidity_convertert::lib_prefix = "tag-struct "
protected

◆ linearizedBaseList

std::unordered_map<std::string, std::vector<int> > solidity_convertert::linearizedBaseList
protected

◆ member_entity_scope

std::unordered_map<int, std::string> solidity_convertert::member_entity_scope
protected

◆ mode

const char* solidity_convertert::mode = "C++"
staticconstexprprotected

◆ newContractSet

std::set<std::string> solidity_convertert::newContractSet
protected

◆ nonContractNamesList

std::set<std::string> solidity_convertert::nonContractNamesList
protected

◆ nondet_bool_expr

side_effect_expr_function_callt solidity_convertert::nondet_bool_expr
protected

◆ nondet_bytes_dynamic_expr

side_effect_expr_function_callt solidity_convertert::nondet_bytes_dynamic_expr
protected

◆ nondet_uint_expr

side_effect_expr_function_callt solidity_convertert::nondet_uint_expr
protected

◆ ns

namespacet solidity_convertert::ns
protected

◆ overrideMap

std::unordered_map<std::string, std::unordered_map<int, int> > solidity_convertert::overrideMap
protected

◆ prefix

std::string solidity_convertert::prefix = "tag-"
protected

◆ sol_state_vars

std::unordered_set<irep_idt> solidity_convertert::sol_state_vars

Whether a declared variable is a contract state variable.

Held here, keyed by the variable's symbol id, rather than on its typet: IREP2 has no field for it, and a symbol's id survives every migration by construction, so the frontend keeps what is Solidity-level and the shared representation stays closed (docs/roadmap/scope-solidity-irep2.md §10).

◆ src_ast_json

nlohmann::json solidity_convertert::src_ast_json = empty_json
static

◆ src_ast_json_array

nlohmann::json solidity_convertert::src_ast_json_array = nlohmann::json::array()
protected

◆ storage_ref_aliases

std::unordered_map<int, int> solidity_convertert::storage_ref_aliases
protected

◆ string_t

typet solidity_convertert::string_t
protected

◆ structureTypingMap

std::unordered_map<std::string, std::unordered_set<std::string> > solidity_convertert::structureTypingMap
protected

◆ tgt_cnt_set

std::set<std::string> solidity_convertert::tgt_cnt_set
protected

◆ tgt_cnts

const std::string& solidity_convertert::tgt_cnts
protected

◆ tgt_func

const std::string& solidity_convertert::tgt_func
protected

◆ UserDefinedVarMap

std::unordered_map< std::string, typet > solidity_convertert::UserDefinedVarMap
static
The documentation for this class was generated from the following files: