29 for(std::size_t i=0; i<dest.size(); ++i)
57 for(
size_t i=0; i<to_read; i++)
71 dest.push_back(value);
97 if(cell.second.initialized==
111 if(ty.
id()==ID_struct)
123 else if(ty.
id()==ID_array)
127 evaluate(at.size(), array_size_vec);
128 if(array_size_vec.size()!=1)
133 result=array_size_vec[0]*subtype_count;
153 const typet &source_type,
157 if(source_type.
id()==ID_struct)
162 for(
const auto &comp : st.components())
168 if(component_byte_size<0)
171 if(comp_offset + component_byte_size > offset)
175 comp.type(), offset - comp_offset, subtype_result);
176 result=previous_member_offsets+subtype_result;
184 previous_member_offsets+=component_count;
190 else if(source_type.
id()==ID_array)
194 evaluate(at.size(), array_size_vec);
195 if(array_size_vec.size()!=1)
199 if(elem_size_bytes<=0)
205 if(this_idx>=array_size_vec[0])
210 offset%elem_size_bytes,
212 result=subtype_result+(elem_size_leaves*this_idx);
230 const typet &source_type,
234 if(source_type.
id()==ID_struct)
239 for(
const auto &comp : st.components())
244 if(component_count>cell_offset)
248 comp.type(), cell_offset, subtype_result);
254 cell_offset-=component_count;
260 else if(source_type.
id()==ID_array)
264 evaluate(at.size(), array_size_vec);
265 if(array_size_vec.size()!=1)
273 mp_integer this_idx=full_cell_offset/elem_count;
274 if(this_idx>=array_size_vec[0])
280 full_cell_offset%elem_count,
282 result=subtype_result+(elem_size*this_idx);
289 return full_cell_offset!=0;
300 if(expr.
id()==ID_constant)
302 if(expr.
type().
id()==ID_struct)
309 if(it->type().id()==ID_code)
319 if(tmp.size()==sub_size)
321 for(std::size_t i=0; i<tmp.size(); ++i)
322 dest.push_back(tmp[i]);
333 else if((expr.
type().
id()==ID_pointer)
334 || (expr.
type().
id()==ID_address_of))
348 else if(expr.
type().
id()==ID_floatbv)
352 dest.push_back(f.
pack());
355 else if(expr.
type().
id()==ID_fixedbv)
362 else if(expr.
type().
id()==ID_c_bool)
368 else if(expr.
type().
id()==ID_bool)
370 dest.push_back(expr.
is_true());
373 else if(expr.
type().
id()==ID_string)
377 warning() <<
"string decoding not fully implemented " 378 << value.size() + 1 <<
eom;
392 else if(expr.
id()==ID_struct)
401 if(it->type().id()==ID_code)
413 for(std::size_t i=0; i<tmp.size(); i++)
414 dest.push_back(tmp[i]);
425 else if(expr.
id()==ID_side_effect)
431 error() <<
"nondet not implemented" <<
eom;
437 error() <<
"heap memory allocation not fully implemented " 440 std::stringstream buffer;
447 dest.push_back(address);
451 error() <<
"side effect not implemented " 455 else if(expr.
id()==ID_bitor)
458 throw id2string(expr.
id())+
" expects at least two operands";
468 dest.push_back(
final);
471 else if(expr.
id()==ID_bitand)
474 throw id2string(expr.
id())+
" expects at least two operands";
484 dest.push_back(
final);
487 else if(expr.
id()==ID_bitxor)
490 throw id2string(expr.
id())+
" expects at least two operands";
500 dest.push_back(
final);
503 else if(expr.
id()==ID_bitnot)
515 else if(expr.
id()==ID_shl)
518 throw id2string(expr.
id())+
" expects two operands";
523 if(tmp0.size()==1 && tmp1.size()==1)
529 dest.push_back(
final);
533 else if((expr.
id()==ID_shr) || (expr.
id()==ID_lshr))
536 throw id2string(expr.
id())+
" expects two operands";
541 if(tmp0.size()==1 && tmp1.size()==1)
547 dest.push_back(
final);
551 else if(expr.
id()==ID_ashr)
554 throw id2string(expr.
id())+
" expects two operands";
559 if(tmp0.size()==1 && tmp1.size()==1)
565 dest.push_back(
final);
569 else if(expr.
id()==ID_ror)
572 throw id2string(expr.
id())+
" expects two operands";
577 if(tmp0.size()==1 && tmp1.size()==1)
582 dest.push_back(
final);
586 else if(expr.
id()==ID_rol)
589 throw id2string(expr.
id())+
" expects two operands";
594 if(tmp0.size()==1 && tmp1.size()==1)
599 dest.push_back(
final);
603 else if(expr.
id()==ID_equal ||
604 expr.
id()==ID_notequal ||
611 throw id2string(expr.
id())+
" expects two operands";
617 if(tmp0.size()==1 && tmp1.size()==1)
622 if(expr.
id()==ID_equal)
623 dest.push_back(op0==op1);
624 else if(expr.
id()==ID_notequal)
625 dest.push_back(op0!=op1);
626 else if(expr.
id()==ID_le)
627 dest.push_back(op0<=op1);
628 else if(expr.
id()==ID_ge)
629 dest.push_back(op0>=op1);
630 else if(expr.
id()==ID_lt)
631 dest.push_back(op0<op1);
632 else if(expr.
id()==ID_gt)
633 dest.push_back(op0>op1);
638 else if(expr.
id()==ID_or)
641 throw id2string(expr.
id())+
" expects at least one operand";
650 if(tmp.size()==1 && tmp.front()!=0)
661 else if(expr.
id()==ID_if)
664 throw "if expects three operands";
678 dest.push_back(tmp1.front());
682 else if(expr.
id()==ID_and)
685 throw id2string(expr.
id())+
" expects at least one operand";
694 if(tmp.size()==1 && tmp.front()==0)
705 else if(expr.
id()==ID_not)
714 dest.push_back(tmp.front()==0);
718 else if(expr.
id()==ID_plus)
733 else if(expr.
id()==ID_mult)
738 if(expr.
type().
id()==ID_fixedbv)
745 else if(expr.
type().
id()==ID_floatbv)
760 if(expr.
type().
id()==ID_fixedbv)
770 else if(expr.
type().
id()==ID_floatbv)
787 else if(expr.
id()==ID_minus)
790 throw "- expects two operands";
796 if(tmp0.size()==1 && tmp1.size()==1)
797 dest.push_back(tmp0.front()-tmp1.front());
800 else if(expr.
id()==ID_div)
803 throw "/ expects two operands";
809 if(tmp0.size()==1 && tmp1.size()==1)
810 dest.push_back(tmp0.front()/tmp1.front());
813 else if(expr.
id()==ID_unary_minus)
816 throw "unary- expects one operand";
822 dest.push_back(-tmp0.front());
825 else if(expr.
id()==ID_address_of)
828 throw "address_of expects one operand";
833 else if(expr.
id()==ID_pointer_offset)
836 throw "pointer_offset expects one operand";
838 throw "pointer_offset expects a pointer operand";
853 dest.push_back(byte_offset);
858 else if(expr.
id()==ID_byte_extract_little_endian ||
859 expr.
id()==ID_byte_extract_big_endian)
862 throw "byte_extract should have two operands";
867 if(extract_offset.size()==1 && extract_from.size()!=0)
880 target_type_leaves>0)
882 dest.insert(dest.end(),
883 extract_from.begin()+memory_offset.to_long(),
884 extract_from.begin()+(memory_offset+target_type_leaves).to_long());
890 else if(expr.
id()==ID_dereference ||
891 expr.
id()==ID_index ||
892 expr.
id()==ID_symbol ||
893 expr.
id()==ID_member)
898 if(address.is_zero())
903 if(expr.
id() == ID_index)
905 exprt evaluated_index = expr;
910 evaluated_index.
op1() =
923 if(simplified.
id() == expr.
id())
931 else if(!address.is_zero())
945 else if(expr.
id()==ID_typecast)
948 throw "typecast expects one operand";
957 if(expr.
type().
id()==ID_pointer)
959 dest.push_back(value);
962 else if(expr.
type().
id()==ID_signedbv)
969 else if(expr.
type().
id()==ID_unsignedbv)
976 else if((expr.
type().
id()==ID_bool) || (expr.
type().
id()==ID_c_bool))
978 dest.push_back(value!=0);
983 else if(expr.
id()==ID_array)
991 else if(expr.
id()==ID_array_of)
994 std::vector<mp_integer> size;
995 if(ty.size().id()==ID_infinity)
1003 for(std::size_t i=0; i<size_int; ++i)
1008 else if(expr.
id()==ID_with)
1012 std::vector<mp_integer> where;
1013 std::vector<mp_integer> new_value;
1015 evaluate(wexpr.new_value(), new_value);
1017 if(!new_value.empty() && where.size()==1 && !
unbounded_size(subtype))
1025 mp_integer need_size=(where_idx+1)*subtype_size;
1027 if(dest.size()<need_size)
1030 for(std::size_t i=0; i<new_value.size(); ++i)
1036 else if(expr.
id()==ID_nil)
1041 else if(expr.
id()==ID_infinity)
1043 if(expr.
type().
id()==ID_signedbv)
1045 warning() <<
"Infinite size arrays not supported" <<
eom;
1049 error() <<
"!! failed to evaluate expression: " 1051 << expr.
id() <<
"[" << expr.
type().
id() <<
"]" 1059 if(expr.
id()==ID_symbol)
1065 interpretert::memory_mapt::const_iterator m_it1=
1069 return m_it1->second;
1073 interpretert::memory_mapt::const_iterator m_it2=
1077 return m_it2->second;
1083 else if(expr.
id()==ID_dereference)
1086 throw "dereference expects one operand";
1092 return tmp0.front();
1094 else if(expr.
id()==ID_index)
1097 throw "index expects two operands";
1106 return base+tmp1.front();
1109 else if(expr.
id()==ID_member)
1112 throw "member expects one operand";
1122 for(
const auto &comp : struct_type.
components())
1124 if(comp.get_name()==component_name)
1134 else if(expr.
id()==ID_byte_extract_little_endian ||
1135 expr.
id()==ID_byte_extract_big_endian)
1138 throw "byte_extract should have two operands";
1143 if(extract_offset.size()==1 && !extract_from.empty())
1147 extract_offset[0], memory_offset))
1151 else if(expr.
id()==ID_if)
1162 else if(expr.
id()==ID_typecast)
1165 throw "typecast expects one operand";
1171 error() <<
"!! failed to evaluate address: " bool byte_offset_to_memory_offset(const typet &source_type, const mp_integer &byte_offset, mp_integer &result)
Supposing the caller has an mp_vector representing a value with type 'source_type', this yields the offset into that vector at which to find a value at byte address 'offset'.
The type of an expression.
typet get_type(const irep_idt &id) const
returns the type object corresponding to id
const std::string & id2string(const irep_idt &d)
mp_integer rotate_left(const mp_integer &a, const mp_integer &b, std::size_t true_size)
rotate left (LSB=MSB) bitwise operations only make sense on native objects, hence the largest object ...
irep_idt address_to_identifier(const mp_integer &address) const
void set_value(const mp_integer &_v)
const std::string integer2string(const mp_integer &n, unsigned base)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
exprt simplify_expr(const exprt &src, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
string_containert & get_string_container()
Get a reference to the global string container.
mp_integer::ullong_t integer2ulong(const mp_integer &n)
void from_expr(const constant_exprt &expr)
std::vector< mp_integer > mp_vectort
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise xor bitwise operations only make sense on native objects, hence the largest object size shoul...
const irep_idt & get_identifier() const
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_value() const
bool memory_offset_to_byte_offset(const typet &source_type, const mp_integer &cell_offset, mp_integer &result)
Similarly to the above, the interpreter's memory objects contain mp_integers that represent variable-...
void from_expr(const constant_exprt &expr)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
const componentst & components() const
The trinary if-then-else operator.
mp_integer arith_left_shift(const mp_integer &a, const mp_integer &b, std::size_t true_size)
arithmetic left shift bitwise operations only make sense on native objects, hence the largest object ...
A constant literal expression.
static mstreamt & eom(mstreamt &m)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
side_effect_exprt & to_side_effect_expr(exprt &expr)
const mp_integer & get_value() const
mstreamt & warning() const
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Interpreter for GOTO Programs.
void unpack(const mp_integer &i)
goto_functionst::function_mapt::const_iterator function
exprt get_value(const typet &type, const mp_integer &offset=0, bool use_non_det=false)
retrives the constant value at memory location offset as an object of type type
void read(const mp_integer &address, mp_vectort &dest) const
Reads a memory address and loads it into the dest variable.
void read_unbounded(const mp_integer &address, mp_vectort &dest) const
void from_integer(const mp_integer &i)
mp_integer logic_right_shift(const mp_integer &a, const mp_integer &b, std::size_t true_size)
logic right shift (loads 0 on MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)
mp_integer bitwise_and(const mp_integer &a, const mp_integer &b)
bitwise and bitwise operations only make sense on native objects, hence the largest object size shoul...
mp_integer arith_right_shift(const mp_integer &a, const mp_integer &b, std::size_t true_size)
arithmetic right shift (loads sign on MSB) bitwise operations only make sense on native objects...
mp_integer address_to_offset(const mp_integer &address) const
mp_integer bitwise_neg(const mp_integer &a)
bitwise negation bitwise operations only make sense on native objects, hence the largest object size ...
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const irep_idt get_original_name() const
mp_integer rotate_right(const mp_integer &a, const mp_integer &b, std::size_t true_size)
rotates right (MSB=LSB) bitwise operations only make sense on native objects, hence the largest objec...
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
mp_integer base_address_to_actual_size(const mp_integer &address) const
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
void allocate(const mp_integer &address, const mp_integer &size)
reserves memory block of size at address
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise or bitwise operations only make sense on native objects, hence the largest object size should...
Operator to return the address of an object.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
bool unbounded_size(const typet &)
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
bool has_operands() const
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
void clear_input_flags()
Clears memoy r/w flag initialization.
mstreamt & result() const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
void build_memory_map()
Creates a memory map of all static symbols in the program.
irep_idt get_component_name() const
const std::string integer2binary(const mp_integer &n, std::size_t width)
bool is_ssa_expr(const exprt &expr)
void from_integer(const mp_integer &i)
bool count_type_leaves(const typet &source_type, mp_integer &result)
Count the number of leaf subtypes of ty, a leaf type is a type that is not an array or a struct...
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
An expression containing a side effect.
const irep_idt & get_statement() const