38 else if(src.
id()==ID_member)
40 else if(src.
id()==ID_index)
42 else if(src.
id()==ID_typecast)
44 else if(src.
id()==ID_symbol)
46 else if(src.
id()==ID_address_of)
48 else if(src.
id()==ID_plus)
55 else if(src.
id()==ID_array)
62 else if(src.
id()==ID_vector)
69 else if(src.
id()==ID_if)
78 else if(src.
id()==ID_array_of)
82 else if(src.
id()==ID_union)
97 if(rhs.
id()==ID_side_effect)
102 if(statement==ID_malloc)
107 else if(statement==ID_nondet)
111 else if(statement==ID_gcc_builtin_va_arg_next)
117 throw "unexpected side-effect on rhs: "+
id2string(statement);
137 const irept &sizeof_type=expr.
find(ID_C_c_sizeof_type);
141 return static_cast<const typet &
>(sizeof_type);
143 else if(expr.
id()==ID_mult)
162 throw "malloc expected to have one operand";
174 if(tmp_size.
id()==ID_mult &&
191 if(elem_size<0 ||
to_integer(tmp_size, alloc_size))
196 if(alloc_size==elem_size)
197 object_type=tmp_type;
202 if(elements*elem_size==alloc_size)
216 if(object_type.
id()==ID_array &&
223 size_symbol.
base_name=
"dynamic_object_size"+std::to_string(dynamic_count);
227 size_symbol.
mode=ID_C;
244 value_symbol.
type=object_type;
245 value_symbol.
type.
set(
"#dynamic",
true);
246 value_symbol.
mode=ID_C;
250 if(object_type.
id()==ID_array)
256 rhs.
op0()=index_expr;
275 if(src.
id()==ID_typecast)
277 else if(src.
id()==ID_address_of)
281 if(op.
id()==ID_symbol)
294 throw "va_arg_next expected to have one operand";
313 if(pos!=std::string::npos)
316 std::string base=
id2string(function_identifier)+
"::va_arg";
326 std::string(
id2string(
id), base.size(), std::string::npos))
350 const exprt &ssa_lhs,
351 const exprt &ssa_rhs)
356 std::cout <<
"assign_rec: " << ssa_lhs.
pretty() <<
'\n';
360 if(ssa_lhs.
id()==ID_symbol)
363 assert(ssa_lhs.
get_bool(ID_C_SSA_symbol));
366 const irep_idt &full_identifier=symbol_expr.get(ID_C_full_identifier);
369 const irep_idt &ssa_identifier=symbol_expr.get_identifier();
370 std::cout <<
"SSA symbol identifier: " << ssa_identifier <<
'\n';
371 std::cout <<
"full identifier: " << full_identifier <<
'\n';
404 std::cout <<
"ssa_rhs: " << ssa_rhs.
pretty() <<
'\n';
405 std::cout <<
"new_lhs: " << new_lhs.
pretty() <<
'\n';
407 throw "assign_rec got different types";
425 else if(ssa_lhs.
id()==ID_typecast)
433 else if(ssa_lhs.
id()==ID_member)
436 std::cout <<
"assign_rec ID_member\n";
442 const typet &compound_type=
445 if(compound_type.
id()==ID_struct)
450 exprt member_name(ID_member_name);
455 with_exprt new_rhs(struct_op, member_name, ssa_rhs);
459 else if(compound_type.
id()==ID_union)
470 throw "assign_rec: member expects struct or union type";
472 else if(ssa_lhs.
id()==ID_index)
475 std::cout <<
"assign_rec ID_index\n";
478 throw "unexpected array index on lhs";
480 else if(ssa_lhs.
id()==ID_dereference)
483 std::cout <<
"assign_rec ID_dereference\n";
486 throw "unexpected dereference on lhs";
488 else if(ssa_lhs.
id()==ID_if)
491 std::cout <<
"assign_rec ID_if\n";
498 guard.push_back(cond);
507 else if(ssa_lhs.
id()==ID_byte_extract_little_endian ||
508 ssa_lhs.
id()==ID_byte_extract_big_endian)
511 std::cout <<
"assign_rec ID_byte_extract\n";
522 if(ssa_lhs.
id()==ID_byte_extract_little_endian)
523 new_id=ID_byte_update_little_endian;
524 else if(ssa_lhs.
id()==ID_byte_extract_big_endian)
525 new_id=ID_byte_update_big_endian;
532 new_rhs.
op()=byte_extract_expr.
op();
534 new_rhs.
value()=ssa_rhs;
536 const exprt new_lhs=byte_extract_expr.
op();
540 else if(ssa_lhs.
id()==ID_struct)
550 assert(operands.size()==components.size());
552 if(ssa_rhs.
id()==ID_struct &&
553 ssa_rhs.
operands().size()==components.size())
555 exprt::operandst::const_iterator lhs_it=operands.begin();
564 for(std::size_t i=0; i<components.size(); i++)
571 components[i].get_name(),
572 components[i].type()),
574 assign_rec(state, guard, operands[i], new_rhs);
578 else if(ssa_lhs.
id()==ID_array)
582 if(ssa_lhs_type.
id()!=ID_array)
583 throw "array constructor must have array type";
591 if(ssa_rhs.
id()==ID_array &&
592 ssa_rhs.
operands().size()==operands.size())
594 exprt::operandst::const_iterator lhs_it=operands.begin();
603 for(std::size_t i=0; i<operands.size(); i++)
613 assign_rec(state, guard, operands[i], new_rhs);
617 else if(ssa_lhs.
id()==ID_string_constant ||
618 ssa_lhs.
id()==
"NULL-object" ||
619 ssa_lhs.
id()==
"zero_string" ||
620 ssa_lhs.
id()==
"is_zero_string" ||
621 ssa_lhs.
id()==
"zero_string_length")
628 throw "path_symext::assign_rec(): unexpected lhs: "+ssa_lhs.
id_string();
635 const exprt &
function,
636 std::list<path_symex_statet> &further_states)
639 std::cout <<
"function_call_rec: " <<
function.pretty() <<
'\n';
642 if(
function.
id()==ID_symbol)
644 const irep_idt &function_identifier=
648 locst::function_mapt::const_iterator f_it=
653 "failed to find `"+
id2string(function_identifier)+
"' in function_map";
660 if(function_entry_point==
loc_reft())
676 thread.
call_stack.back().current_function=function_identifier;
682 for(
loc_reft l=function_entry_point; ; ++l)
684 if(locs[l].target->is_end_function())
686 if(locs[l].target->is_decl())
694 for(locst::local_variablest::const_iterator
695 it=function_entry.local_variables.begin();
696 it!=function_entry.local_variables.end();
699 unsigned nr=state.
var_map[*it].number;
711 std::size_t va_args_start_index=0;
714 for(std::size_t i=0; i<call_arguments.size(); i++)
716 if(i<function_parameters.size())
721 if(identifier.
empty())
722 throw "function_call " +
id2string(function_identifier)
723 +
" no identifier for function parameter";
726 exprt rhs=call_arguments[i];
729 if(lhs.type()!=rhs.type())
734 else if(va_args_start_index==0)
735 va_args_start_index=i;
740 std::size_t va_count=0;
742 auto call_arguments_it = std::begin(call_arguments);
743 std::advance(call_arguments_it, va_args_start_index);
744 auto call_arguments_end = std::end(call_arguments);
746 for(; call_arguments_it!=call_arguments_end; ++call_arguments_it)
748 exprt rhs=*call_arguments_it;
751 +std::to_string(va_count);
755 symbol.
base_name=
"va_arg"+std::to_string(va_count);
774 thread.
pc=function_entry_point;
776 else if(
function.
id()==ID_dereference)
779 throw "function_call_rec got dereference";
781 else if(
function.
id()==ID_if)
789 further_states.push_back(state);
794 further_states.back(), call, if_expr.
false_case(), further_states);
804 else if(
function.
id()==ID_typecast)
812 throw "TODO: function_call "+
function.id_string();
833 if(thread.
call_stack.back().return_rhs.is_not_nil() &&
834 thread.
call_stack.back().return_lhs.is_not_nil())
839 for(path_symex_statet::var_state_mapt::const_iterator
840 it=thread.
call_stack.back().saved_local_vars.begin();
841 it!=thread.
call_stack.back().saved_local_vars.end();
864 std::list<path_symex_statet> &further_states)
866 const goto_programt::instructiont &instruction=
869 if(instruction.is_backwards_goto())
878 exprt guard=state.
read(instruction.guard);
888 if(!guard.is_false())
892 further_states.push_back(state);
893 further_states.back().record_step();
896 further_states.back().history->guard=guard;
913 const goto_programt::instructiont &instruction=
916 if(instruction.is_backwards_goto())
922 exprt guard=state.
read(instruction.guard);
945 std::list<path_symex_statet> &further_states)
947 const goto_programt::instructiont &instruction=
951 std::cout <<
"path_symext::operator(): " 957 switch(instruction.type)
970 if(instruction.code.operands().size()==1)
998 do_goto(state, further_states);
1009 throw "THROW not yet implemented";
1014 if(instruction.guard.is_false())
1018 exprt guard=state.
read(instruction.guard);
1039 throw "nested ATOMIC_BEGIN";
1048 throw "ATOMIC_END unmatched";
1070 const codet &code=instruction.code;
1073 if(statement==ID_expression)
1077 else if(statement==ID_printf)
1081 else if(statement==ID_asm)
1085 else if(statement==ID_fence)
1089 else if(statement==ID_input)
1094 throw "unexpected OTHER statement: "+
id2string(statement);
1101 throw "path_symext: unexpected instruction";
1107 std::list<path_symex_statet> further_states;
1109 if(!further_states.empty())
1110 throw "path_symext got unexpected further states";
1115 std::list<path_symex_statet> &further_states)
1132 path_symex.
do_goto(state, taken);
const irep_idt & get_statement() const
virtual void operator()(path_symex_statet &state, std::list< path_symex_statet > &furter_states)
The type of an expression.
irep_idt name
The unique identifier.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const typet & follow(const typet &src) const
const code_declt & to_code_decl(const codet &code)
Linking: Zero Initialization.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
exprt simplify_expr(const exprt &src, const namespacet &ns)
irep_idt mode
Language mode.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
bool inside_atomic_section
bool has_ellipsis() const
void assign_rec(path_symex_statet &state, exprt::operandst &guard, const exprt &ssa_lhs, const exprt &ssa_rhs)
void symex_malloc(path_symex_statet &state, const exprt &lhs, const side_effect_exprt &code)
const irep_idt & get_identifier() const
void disable_current_thread()
std::vector< componentt > componentst
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
std::vector< parametert > parameterst
const componentst & components() const
exprt read_no_propagate(const exprt &src)
The trinary if-then-else operator.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void path_symex_assert_fail(path_symex_statet &state)
bool get_bool(const irep_namet &name) const
unwinding_mapt unwinding_map
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
void function_call(path_symex_statet &state, const code_function_callt &call, std::list< path_symex_statet > &further_states)
void do_goto(path_symex_statet &state, bool taken)
virtual void do_assert_fail(path_symex_statet &state)
symbol_exprt ssa_symbol() const
side_effect_exprt & to_side_effect_expr(exprt &expr)
Extract member of struct or union.
exprt conjunction(const exprt::operandst &op)
const code_assignt & to_code_assign(const codet &code)
enum path_symex_stept::kindt branch
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Concrete Symbolic Transformer.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
Expression classes for byte-level operators.
exprt read(const exprt &src)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
void path_symex(path_symex_statet &state, std::list< path_symex_statet > &further_states)
Operator to dereference a pointer.
void symex_va_arg_next(path_symex_statet &state, const exprt &lhs, const side_effect_exprt &code)
void assign(path_symex_statet &state, const exprt &lhs, const exprt &rhs)
const exprt & size() const
Base class for tree-like data structures with sharing.
#define forall_operands(it, expr)
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
var_statet & get_var_state(const var_mapt::var_infot &var_info)
bitvector_typet index_type()
unsigned get_current_thread() const
void return_from_function(path_symex_statet &state)
Operator to return the address of an object.
loc_reft next_loc() const
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
unsigned safe_string2unsigned(const std::string &str, int base)
typet type
Type of symbol.
recursion_mapt recursion_map
static bool propagate(const exprt &src)
goto_programt::const_targett get_instruction() const
void increment_ssa_counter()
Base class for all expressions.
const exprt & struct_op() const
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
irep_idt base_name
Base (non-scoped) name.
Operator to update elements in structs and arrays.
const source_locationt & source_location() const
irep_idt get_component_name() const
void set_pc(loc_reft new_pc)
function_mapt function_map
Concrete Symbolic Transformer.
void path_symex_goto(path_symex_statet &state, bool taken)
const std::string & id_string() const
void function_call_rec(path_symex_statet &state, const code_function_callt &function_call, const exprt &function, std::list< path_symex_statet > &further_states)
void set_return_value(path_symex_statet &, const exprt &)
static irep_idt get_old_va_symbol(const path_symex_statet &state, const exprt &src)
Expression to hold a symbol (variable)
A statement in a programming language.
unsignedbv_typet unsigned_char_type()
const typet & subtype() const
An expression containing a side effect.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const irep_idt & get_identifier() const
void make_typecast(const typet &_type)
const irept & find(const irep_namet &name) const
static typet c_sizeof_type_rec(const exprt &expr)
path_symex_step_reft history
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & get_statement() const
const code_function_callt & to_code_function_call(const codet &code)
irep_idt byte_update_id()