28 for(std::size_t i=0; i<dest.size(); ++i)
56 for(
size_t i=0; i<to_read; i++)
70 dest.push_back(value);
96 if(cell.second.initialized==
110 if(ty.
id()==ID_struct)
122 else if(ty.
id()==ID_array)
126 evaluate(at.size(), array_size_vec);
127 if(array_size_vec.size()!=1)
132 result=array_size_vec[0]*subtype_count;
152 const typet &source_type,
156 if(source_type.
id()==ID_struct)
161 for(
const auto &comp : st.components())
167 if(component_byte_size<0)
170 if(comp_offset + component_byte_size > offset)
174 comp.type(), offset - comp_offset, subtype_result);
175 result=previous_member_offsets+subtype_result;
183 previous_member_offsets+=component_count;
189 else if(source_type.
id()==ID_array)
193 evaluate(at.size(), array_size_vec);
194 if(array_size_vec.size()!=1)
198 if(elem_size_bytes<=0)
204 if(this_idx>=array_size_vec[0])
209 offset%elem_size_bytes,
211 result=subtype_result+(elem_size_leaves*this_idx);
229 const typet &source_type,
233 if(source_type.
id()==ID_struct)
238 for(
const auto &comp : st.components())
243 if(component_count>cell_offset)
247 comp.type(), cell_offset, subtype_result);
253 cell_offset-=component_count;
259 else if(source_type.
id()==ID_array)
263 evaluate(at.size(), array_size_vec);
264 if(array_size_vec.size()!=1)
272 mp_integer this_idx=full_cell_offset/elem_count;
273 if(this_idx>=array_size_vec[0])
279 full_cell_offset%elem_count,
281 result=subtype_result+(elem_size*this_idx);
288 return full_cell_offset!=0;
299 if(expr.
id()==ID_constant)
301 if(expr.
type().
id()==ID_struct)
308 if(it->type().id()==ID_code)
318 if(tmp.size()==sub_size)
320 for(std::size_t i=0; i<tmp.size(); ++i)
321 dest.push_back(tmp[i]);
332 else if((expr.
type().
id()==ID_pointer)
333 || (expr.
type().
id()==ID_address_of))
347 else if(expr.
type().
id()==ID_floatbv)
351 dest.push_back(f.
pack());
354 else if(expr.
type().
id()==ID_fixedbv)
361 else if(expr.
type().
id()==ID_c_bool)
367 else if(expr.
type().
id()==ID_bool)
369 dest.push_back(expr.
is_true());
372 else if(expr.
type().
id()==ID_string)
376 warning() <<
"string decoding not fully implemented " 377 << value.size() + 1 <<
eom;
391 else if(expr.
id()==ID_struct)
400 if(it->type().id()==ID_code)
412 for(std::size_t i=0; i<tmp.size(); i++)
413 dest.push_back(tmp[i]);
424 else if(expr.
id()==ID_side_effect)
430 error() <<
"nondet not implemented" <<
eom;
436 error() <<
"heap memory allocation not fully implemented " 439 std::stringstream buffer;
446 dest.push_back(address);
450 error() <<
"side effect not implemented " 454 else if(expr.
id()==ID_bitor)
457 throw id2string(expr.
id())+
" expects at least two operands";
467 dest.push_back(
final);
470 else if(expr.
id()==ID_bitand)
473 throw id2string(expr.
id())+
" expects at least two operands";
483 dest.push_back(
final);
486 else if(expr.
id()==ID_bitxor)
489 throw id2string(expr.
id())+
" expects at least two operands";
499 dest.push_back(
final);
502 else if(expr.
id()==ID_bitnot)
514 else if(expr.
id()==ID_shl)
517 throw id2string(expr.
id())+
" expects two operands";
522 if(tmp0.size()==1 && tmp1.size()==1)
528 dest.push_back(
final);
532 else if((expr.
id()==ID_shr) || (expr.
id()==ID_lshr))
535 throw id2string(expr.
id())+
" expects two operands";
540 if(tmp0.size()==1 && tmp1.size()==1)
546 dest.push_back(
final);
550 else if(expr.
id()==ID_ashr)
553 throw id2string(expr.
id())+
" expects two operands";
558 if(tmp0.size()==1 && tmp1.size()==1)
564 dest.push_back(
final);
568 else if(expr.
id()==ID_ror)
571 throw id2string(expr.
id())+
" expects two operands";
576 if(tmp0.size()==1 && tmp1.size()==1)
581 dest.push_back(
final);
585 else if(expr.
id()==ID_rol)
588 throw id2string(expr.
id())+
" expects two operands";
593 if(tmp0.size()==1 && tmp1.size()==1)
598 dest.push_back(
final);
602 else if(expr.
id()==ID_equal ||
603 expr.
id()==ID_notequal ||
610 throw id2string(expr.
id())+
" expects two operands";
616 if(tmp0.size()==1 && tmp1.size()==1)
621 if(expr.
id()==ID_equal)
622 dest.push_back(op0==op1);
623 else if(expr.
id()==ID_notequal)
624 dest.push_back(op0!=op1);
625 else if(expr.
id()==ID_le)
626 dest.push_back(op0<=op1);
627 else if(expr.
id()==ID_ge)
628 dest.push_back(op0>=op1);
629 else if(expr.
id()==ID_lt)
630 dest.push_back(op0<op1);
631 else if(expr.
id()==ID_gt)
632 dest.push_back(op0>op1);
637 else if(expr.
id()==ID_or)
640 throw id2string(expr.
id())+
" expects at least one operand";
649 if(tmp.size()==1 && tmp.front()!=0)
660 else if(expr.
id()==ID_if)
663 throw "if expects three operands";
677 dest.push_back(tmp1.front());
681 else if(expr.
id()==ID_and)
684 throw id2string(expr.
id())+
" expects at least one operand";
693 if(tmp.size()==1 && tmp.front()==0)
704 else if(expr.
id()==ID_not)
713 dest.push_back(tmp.front()==0);
717 else if(expr.
id()==ID_plus)
732 else if(expr.
id()==ID_mult)
737 if(expr.
type().
id()==ID_fixedbv)
744 else if(expr.
type().
id()==ID_floatbv)
759 if(expr.
type().
id()==ID_fixedbv)
769 else if(expr.
type().
id()==ID_floatbv)
786 else if(expr.
id()==ID_minus)
789 throw "- expects two operands";
795 if(tmp0.size()==1 && tmp1.size()==1)
796 dest.push_back(tmp0.front()-tmp1.front());
799 else if(expr.
id()==ID_div)
802 throw "/ expects two operands";
808 if(tmp0.size()==1 && tmp1.size()==1)
809 dest.push_back(tmp0.front()/tmp1.front());
812 else if(expr.
id()==ID_unary_minus)
815 throw "unary- expects one operand";
821 dest.push_back(-tmp0.front());
824 else if(expr.
id()==ID_address_of)
827 throw "address_of expects one operand";
832 else if(expr.
id()==ID_pointer_offset)
835 throw "pointer_offset expects one operand";
837 throw "pointer_offset expects a pointer operand";
852 dest.push_back(byte_offset);
857 else if(expr.
id()==ID_byte_extract_little_endian ||
858 expr.
id()==ID_byte_extract_big_endian)
861 throw "byte_extract should have two operands";
866 if(extract_offset.size()==1 && extract_from.size()!=0)
879 target_type_leaves>0)
881 dest.insert(dest.end(),
882 extract_from.begin()+memory_offset.to_long(),
883 extract_from.begin()+(memory_offset+target_type_leaves).to_long());
889 else if(expr.
id()==ID_dereference ||
890 expr.
id()==ID_index ||
891 expr.
id()==ID_symbol ||
892 expr.
id()==ID_member)
897 if(address.is_zero() && expr.
id()==ID_index)
905 if(expr.
op0().
id()==ID_array)
909 if(read_from_index>=0 && read_from_index<ops.size())
911 evaluate(ops[read_from_index.to_long()], dest);
916 else if(expr.
op0().
id() == ID_array_list)
923 "array-list has odd number of operands");
924 for(
size_t listidx=0; listidx!=ops.size(); listidx+=2)
929 if(elem_idx[0]==read_from_index)
944 else if(!address.is_zero())
958 else if(expr.
id()==ID_typecast)
961 throw "typecast expects one operand";
970 if(expr.
type().
id()==ID_pointer)
972 dest.push_back(value);
975 else if(expr.
type().
id()==ID_signedbv)
982 else if(expr.
type().
id()==ID_unsignedbv)
989 else if((expr.
type().
id()==ID_bool) || (expr.
type().
id()==ID_c_bool))
991 dest.push_back(value!=0);
996 else if(expr.
id()==ID_array)
1004 else if(expr.
id()==ID_array_of)
1007 std::vector<mp_integer> size;
1008 if(ty.size().id()==ID_infinity)
1016 for(std::size_t i=0; i<size_int; ++i)
1021 else if(expr.
id()==ID_with)
1025 std::vector<mp_integer> where;
1026 std::vector<mp_integer> new_value;
1028 evaluate(wexpr.new_value(), new_value);
1030 if(!new_value.empty() && where.size()==1 && !
unbounded_size(subtype))
1038 mp_integer need_size=(where_idx+1)*subtype_size;
1040 if(dest.size()<need_size)
1043 for(std::size_t i=0; i<new_value.size(); ++i)
1049 else if(expr.
id()==ID_nil)
1054 else if(expr.
id()==ID_infinity)
1056 if(expr.
type().
id()==ID_signedbv)
1058 warning() <<
"Infinite size arrays not supported" <<
eom;
1062 error() <<
"!! failed to evaluate expression: " 1064 << expr.
id() <<
"[" << expr.
type().
id() <<
"]" 1072 if(expr.
id()==ID_symbol)
1078 interpretert::memory_mapt::const_iterator m_it1=
1082 return m_it1->second;
1086 interpretert::memory_mapt::const_iterator m_it2=
1090 return m_it2->second;
1096 else if(expr.
id()==ID_dereference)
1099 throw "dereference expects one operand";
1105 return tmp0.front();
1107 else if(expr.
id()==ID_index)
1110 throw "index expects two operands";
1119 return base+tmp1.front();
1122 else if(expr.
id()==ID_member)
1125 throw "member expects one operand";
1135 for(
const auto &comp : struct_type.
components())
1137 if(comp.get_name()==component_name)
1147 else if(expr.
id()==ID_byte_extract_little_endian ||
1148 expr.
id()==ID_byte_extract_big_endian)
1151 throw "byte_extract should have two operands";
1156 if(extract_offset.size()==1 && !extract_from.empty())
1160 extract_offset[0], memory_offset))
1164 else if(expr.
id()==ID_if)
1175 else if(expr.
id()==ID_typecast)
1178 throw "typecast expects one operand";
1184 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 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
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 ...
#define CHECK_RETURN(CONDITION)
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.
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
#define DATA_INVARIANT(CONDITION, REASON)
An expression containing a side effect.
const irep_idt & get_statement() const