Go to the documentation of this file.
33 for(std::size_t i=0; i<dest.size(); ++i)
40 memory[numeric_cast_v<std::size_t>(address + i)];
57 std::size_t address_val = numeric_cast_v<std::size_t>(address);
62 for(
size_t i=0; i<to_read; i++)
69 memory[numeric_cast_v<std::size_t>(address + i)];
77 dest.push_back(value);
103 if(cell.second.initialized==
117 if(ty.
id()==ID_struct)
125 result+=subtype_count;
129 else if(ty.
id()==ID_array)
133 evaluate(at.size(), array_size_vec);
134 if(array_size_vec.size()!=1)
139 result=array_size_vec[0]*subtype_count;
159 const typet &source_type,
163 if(source_type.
id()==ID_struct)
168 for(
const auto &comp : st.components())
174 if(!comp_offset.has_value() && !component_byte_size.has_value())
177 if(*comp_offset + *component_byte_size > offset)
181 comp.type(), offset - *comp_offset, subtype_result);
182 result=previous_member_offsets+subtype_result;
190 previous_member_offsets+=component_count;
196 else if(source_type.
id()==ID_array)
201 evaluate(at.size(), array_size_vec);
203 if(array_size_vec.size()!=1)
208 if(!elem_size_bytes.has_value() || *elem_size_bytes == 0)
215 mp_integer this_idx = offset / (*elem_size_bytes);
216 if(this_idx>=array_size_vec[0])
221 at.subtype(), offset % (*elem_size_bytes), subtype_result);
223 result=subtype_result+(elem_size_leaves*this_idx);
241 const typet &source_type,
245 if(source_type.
id()==ID_struct)
250 for(
const auto &comp : st.components())
255 if(component_count>cell_offset)
259 comp.type(), cell_offset, subtype_result);
260 const auto member_offset_result =
263 result = member_offset_result.value() + subtype_result;
268 cell_offset-=component_count;
274 else if(source_type.
id()==ID_array)
279 evaluate(at.size(), array_size_vec);
280 if(array_size_vec.size()!=1)
284 if(!elem_size.has_value())
291 mp_integer this_idx=full_cell_offset/elem_count;
292 if(this_idx>=array_size_vec[0])
299 full_cell_offset%elem_count,
301 result = subtype_result + ((*elem_size) * this_idx);
308 return full_cell_offset!=0;
319 if(expr.
id()==ID_constant)
321 if(expr.
type().
id()==ID_struct)
323 dest.reserve(numeric_cast_v<std::size_t>(
get_size(expr.
type())));
328 if(it->type().id()==ID_code)
338 if(tmp.size()==sub_size)
340 for(std::size_t i=0; i<tmp.size(); ++i)
341 dest.push_back(tmp[i]);
352 else if(expr.
type().
id() == ID_pointer)
357 if(
object.
id() == ID_address_of)
362 else if(
const auto i = numeric_cast<mp_integer>(
object))
371 const auto i = numeric_cast<mp_integer>(expr);
372 if(i && i->is_zero())
379 else if(expr.
type().
id()==ID_floatbv)
383 dest.push_back(f.
pack());
386 else if(expr.
type().
id()==ID_fixedbv)
393 else if(expr.
type().
id()==ID_c_bool)
400 else if(expr.
type().
id()==ID_bool)
402 dest.push_back(expr.
is_true());
405 else if(expr.
type().
id()==ID_string)
416 if(
const auto i = numeric_cast<mp_integer>(expr))
423 else if(expr.
id()==ID_struct)
426 dest.reserve(numeric_cast_v<std::size_t>(
get_size(expr.
type())));
432 if(it->type().id()==ID_code)
444 for(std::size_t i=0; i<tmp.size(); i++)
445 dest.push_back(tmp[i]);
456 else if(expr.
id()==ID_side_effect)
468 output.
error() <<
"heap memory allocation not fully implemented "
470 std::stringstream buffer;
478 dest.push_back(address);
485 else if(expr.
id()==ID_bitor)
488 throw id2string(expr.
id())+
" expects at least two operands";
498 dest.push_back(
final);
501 else if(expr.
id()==ID_bitand)
504 throw id2string(expr.
id())+
" expects at least two operands";
514 dest.push_back(
final);
517 else if(expr.
id()==ID_bitxor)
520 throw id2string(expr.
id())+
" expects at least two operands";
530 dest.push_back(
final);
533 else if(expr.
id()==ID_bitnot)
546 else if(expr.
id()==ID_shl)
551 if(tmp0.size()==1 && tmp1.size()==1)
557 dest.push_back(
final);
561 else if(expr.
id() == ID_shr || expr.
id() == ID_lshr)
566 if(tmp0.size()==1 && tmp1.size()==1)
572 dest.push_back(
final);
576 else if(expr.
id()==ID_ashr)
581 if(tmp0.size()==1 && tmp1.size()==1)
587 dest.push_back(
final);
591 else if(expr.
id()==ID_ror)
596 if(tmp0.size()==1 && tmp1.size()==1)
602 dest.push_back(
final);
606 else if(expr.
id()==ID_rol)
611 if(tmp0.size()==1 && tmp1.size()==1)
617 dest.push_back(
final);
621 else if(expr.
id()==ID_equal ||
622 expr.
id()==ID_notequal ||
632 if(tmp0.size()==1 && tmp1.size()==1)
637 if(expr.
id()==ID_equal)
638 dest.push_back(op0==op1);
639 else if(expr.
id()==ID_notequal)
640 dest.push_back(op0!=op1);
641 else if(expr.
id()==ID_le)
642 dest.push_back(op0<=op1);
643 else if(expr.
id()==ID_ge)
644 dest.push_back(op0>=op1);
645 else if(expr.
id()==ID_lt)
646 dest.push_back(op0<op1);
647 else if(expr.
id()==ID_gt)
648 dest.push_back(op0>op1);
653 else if(expr.
id()==ID_or)
656 throw id2string(expr.
id())+
" expects at least one operand";
665 if(tmp.size()==1 && tmp.front()!=0)
672 dest.push_back(result);
676 else if(expr.
id()==ID_if)
686 evaluate(if_expr.true_case(), tmp1);
688 evaluate(if_expr.false_case(), tmp1);
692 dest.push_back(tmp1.front());
696 else if(expr.
id()==ID_and)
699 throw id2string(expr.
id())+
" expects at least one operand";
708 if(tmp.size()==1 && tmp.front()==0)
715 dest.push_back(result);
719 else if(expr.
id()==ID_not)
725 dest.push_back(tmp.front()==0);
729 else if(expr.
id()==ID_plus)
741 dest.push_back(result);
744 else if(expr.
id()==ID_mult)
749 if(expr.
type().
id()==ID_fixedbv)
756 else if(expr.
type().
id()==ID_floatbv)
771 if(expr.
type().
id()==ID_fixedbv)
781 else if(expr.
type().
id()==ID_floatbv)
795 dest.push_back(result);
798 else if(expr.
id()==ID_minus)
804 if(tmp0.size()==1 && tmp1.size()==1)
805 dest.push_back(tmp0.front()-tmp1.front());
808 else if(expr.
id()==ID_div)
814 if(tmp0.size()==1 && tmp1.size()==1)
815 dest.push_back(tmp0.front()/tmp1.front());
818 else if(expr.
id()==ID_unary_minus)
824 dest.push_back(-tmp0.front());
827 else if(expr.
id()==ID_address_of)
832 else if(expr.
id()==ID_pointer_offset)
835 throw "pointer_offset expects one operand";
838 throw "pointer_offset expects a pointer operand";
855 dest.push_back(byte_offset);
861 expr.
id() == ID_dereference || expr.
id() == ID_index ||
862 expr.
id() == ID_symbol || expr.
id() == ID_member ||
863 expr.
id() == ID_byte_extract_little_endian ||
864 expr.
id() == ID_byte_extract_big_endian)
870 if(address.is_zero())
875 if(expr.
id() == ID_index)
882 evaluated_index.
index() =
895 if(simplified.
id() == expr.
id())
903 else if(!address.is_zero())
906 expr.
id() == ID_byte_extract_little_endian ||
907 expr.
id() == ID_byte_extract_big_endian)
912 evaluate(byte_extract_expr.op(), extract_from);
914 !extract_from.empty(),
915 "evaluate_address should have returned address == 0");
922 target_type_leaves > 0)
926 extract_from.begin() + numeric_cast_v<std::size_t>(memory_offset),
927 extract_from.begin() +
928 numeric_cast_v<std::size_t>(memory_offset + target_type_leaves));
935 dest.resize(numeric_cast_v<std::size_t>(
get_size(expr.
type())));
946 else if(expr.
id()==ID_typecast)
955 if(expr.
type().
id()==ID_pointer)
957 dest.push_back(value);
960 else if(expr.
type().
id()==ID_signedbv)
967 else if(expr.
type().
id()==ID_unsignedbv)
974 else if((expr.
type().
id()==ID_bool) || (expr.
type().
id()==ID_c_bool))
976 dest.push_back(value!=0);
981 else if(expr.
id()==ID_array)
989 else if(expr.
id()==ID_array_of)
992 std::vector<mp_integer> size;
993 if(ty.size().id()==ID_infinity)
1000 std::size_t size_int = numeric_cast_v<std::size_t>(size[0]);
1001 for(std::size_t i=0; i<size_int; ++i)
1006 else if(expr.
id()==ID_with)
1010 std::vector<mp_integer> where;
1011 std::vector<mp_integer> new_value;
1013 evaluate(wexpr.new_value(), new_value);
1015 if(!new_value.empty() && where.size()==1 && !
unbounded_size(subtype))
1023 mp_integer need_size=(where_idx+1)*subtype_size;
1025 if(dest.size()<need_size)
1026 dest.resize(numeric_cast_v<std::size_t>(need_size), 0);
1028 for(std::size_t i=0; i<new_value.size(); ++i)
1029 dest[numeric_cast_v<std::size_t>((where_idx * subtype_size) + i)] =
1035 else if(expr.
id()==ID_nil)
1040 else if(expr.
id()==ID_infinity)
1042 if(expr.
type().
id()==ID_signedbv)
1048 output.
error() <<
"!! failed to evaluate expression: "
1050 << expr.
id() <<
"[" << expr.
type().
id() <<
"]"
1058 if(expr.
id()==ID_symbol)
1064 interpretert::memory_mapt::const_iterator m_it1=
1068 return m_it1->second;
1072 interpretert::memory_mapt::const_iterator m_it2=
1076 return m_it2->second;
1082 else if(expr.
id()==ID_dereference)
1088 return tmp0.front();
1090 else if(expr.
id()==ID_index)
1099 return base+tmp1.front();
1102 else if(expr.
id()==ID_member)
1112 for(
const auto &comp : struct_type.
components())
1114 if(comp.get_name()==component_name)
1124 else if(expr.
id()==ID_byte_extract_little_endian ||
1125 expr.
id()==ID_byte_extract_big_endian)
1129 evaluate(byte_extract_expr.op1(), extract_offset);
1131 evaluate(byte_extract_expr.op0(), extract_from);
1132 if(extract_offset.size()==1 && !extract_from.empty())
1136 byte_extract_expr.op0().type(), extract_offset[0], memory_offset))
1141 else if(expr.
id()==ID_if)
1150 if(result.size()==1)
1153 else if(expr.
id()==ID_typecast)
1160 output.
error() <<
"!! failed to evaluate address: "
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
mp_integer base_address_to_actual_size(const mp_integer &address) const
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
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...
const typet & subtype() const
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const irep_idt get_original_name() const
void from_integer(const mp_integer &i)
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 typet to a struct_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
The trinary if-then-else operator.
void unpack(const mp_integer &i)
symbol_exprt address_to_symbol(const mp_integer &address) const
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
bool unbounded_size(const typet &)
Base class for all expressions.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
bool is_true() const
Return whether the expression is a constant representing true.
side_effect_exprt & to_side_effect_expr(exprt &expr)
Expression to hold a symbol (variable)
mp_integer bitwise_and(const mp_integer &a, const mp_integer &b)
bitwise 'and' of two nonnegative integers
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
void build_memory_map()
Creates a memory map of all static symbols in the program.
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.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
typet & type()
Return the type of the expression.
Interpreter for GOTO Programs.
goto_functionst::function_mapt::const_iterator function
Expression classes for byte-level operators.
bool is_ssa_expr(const exprt &expr)
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
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
bool has_operands() const
Return true if there is at least one operand.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const std::string & id2string(const irep_idt &d)
#define forall_operands(it, expr)
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,...
const irep_idt & get_identifier() const
API to expression classes for Pointers.
exprt simplify_expr(exprt src, const namespacet &ns)
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
void read_unbounded(const mp_integer &address, mp_vectort &dest) const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
std::vector< mp_integer > mp_vectort
void set_value(const mp_integer &_v)
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
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,...
void from_integer(const mp_integer &i)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const irep_idt & get_statement() const
std::size_t get_width() const
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
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 ...
Deprecated expression utility functions.
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
void from_expr(const constant_exprt &expr)
Structure type, corresponds to C style structs.
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
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-...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
void clear_input_flags()
Clears memoy r/w flag initialization.
void read(const mp_integer &address, mp_vectort &dest) const
Reads a memory address and loads it into the dest variable.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
mp_integer address_to_offset(const mp_integer &address) const
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
mstreamt & warning() const
const irep_idt & get_value() const
optionalt< 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)
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',...
const mp_integer & get_value() const
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
An expression containing a side effect.
API to expression classes for bitvectors.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
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 ...
void from_expr(const constant_exprt &expr)
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
string_containert & get_string_container()
Get a reference to the global string container.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.