cprover
Loading...
Searching...
No Matches
interpreter_evaluate.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Interpreter for GOTO Programs
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "interpreter_class.h"
13
14#include <util/bitvector_expr.h>
15#include <util/byte_operators.h>
16#include <util/c_types.h>
17#include <util/fixedbv.h>
18#include <util/ieee_float.h>
19#include <util/pointer_expr.h>
21#include <util/simplify_expr.h>
22#include <util/ssa_expr.h>
23#include <util/std_code.h>
25
27#include <util/expr_util.h>
28
32 const mp_integer &address,
33 mp_vectort &dest) const
34{
35 // copy memory region
36 for(std::size_t i=0; i<dest.size(); ++i)
37 {
38 mp_integer value;
39
40 if((address+i)<memory.size())
41 {
42 const memory_cellt &cell =
43 memory[numeric_cast_v<std::size_t>(address + i)];
44 value=cell.value;
47 }
48 else
49 value=0;
50
51 dest[i]=value;
52 }
53}
54
56 const mp_integer &address,
57 mp_vectort &dest) const
58{
59 // copy memory region
60 std::size_t address_val = numeric_cast_v<std::size_t>(address);
61 const mp_integer offset=address_to_offset(address_val);
62 const mp_integer alloc_size=
63 base_address_to_actual_size(address_val-offset);
64 const mp_integer to_read=alloc_size-offset;
65 for(size_t i=0; i<to_read; i++)
66 {
67 mp_integer value;
68
69 if((address+i)<memory.size())
70 {
71 const memory_cellt &cell =
72 memory[numeric_cast_v<std::size_t>(address + i)];
73 value=cell.value;
76 }
77 else
78 value=0;
79
80 dest.push_back(value);
81 }
82}
83
86 const mp_integer &address,
87 const mp_integer &size)
88{
89 // clear memory region
90 for(mp_integer i=0; i<size; ++i)
91 {
92 if((address+i)<memory.size())
93 {
94 memory_cellt &cell = memory[numeric_cast_v<std::size_t>(address + i)];
95 cell.value=0;
97 }
98 }
99}
100
103{
104 for(auto &cell : memory)
105 {
106 if(cell.second.initialized==
108 cell.second.initialized=memory_cellt::initializedt::UNKNOWN;
109 }
110}
111
119{
120 if(ty.id()==ID_struct)
121 {
122 result=0;
123 mp_integer subtype_count;
124 for(const auto &component : to_struct_type(ty).components())
125 {
126 if(count_type_leaves(component.type(), subtype_count))
127 return true;
128 result+=subtype_count;
129 }
130 return false;
131 }
132 else if(ty.id()==ID_array)
133 {
134 const auto &at=to_array_type(ty);
135 mp_vectort array_size_vec = evaluate(at.size());
136 if(array_size_vec.size()!=1)
137 return true;
138 mp_integer subtype_count;
139 if(count_type_leaves(at.element_type(), subtype_count))
140 return true;
141 result=array_size_vec[0]*subtype_count;
142 return false;
143 }
144 else
145 {
146 result=1;
147 return false;
148 }
149}
150
161 const typet &source_type,
162 const mp_integer &offset,
163 mp_integer &result)
164{
165 if(source_type.id()==ID_struct)
166 {
167 const auto &st=to_struct_type(source_type);
168 mp_integer previous_member_offsets=0;
169
170 for(const auto &comp : st.components())
171 {
172 const auto comp_offset = member_offset(st, comp.get_name(), ns);
173
174 const auto component_byte_size = pointer_offset_size(comp.type(), ns);
175
176 if(!comp_offset.has_value() && !component_byte_size.has_value())
177 return true;
178
179 if(*comp_offset + *component_byte_size > offset)
180 {
181 mp_integer subtype_result;
183 comp.type(), offset - *comp_offset, subtype_result);
184 result=previous_member_offsets+subtype_result;
185 return ret;
186 }
187 else
188 {
189 mp_integer component_count;
190 if(count_type_leaves(comp.type(), component_count))
191 return true;
192 previous_member_offsets+=component_count;
193 }
194 }
195 // Ran out of struct members, or struct contained a variable-length field.
196 return true;
197 }
198 else if(source_type.id()==ID_array)
199 {
200 const auto &at=to_array_type(source_type);
201
202 mp_vectort array_size_vec = evaluate(at.size());
203
204 if(array_size_vec.size()!=1)
205 return true;
206
207 mp_integer array_size=array_size_vec[0];
208 auto elem_size_bytes = pointer_offset_size(at.element_type(), ns);
209 if(!elem_size_bytes.has_value() || *elem_size_bytes == 0)
210 return true;
211
212 mp_integer elem_size_leaves;
213 if(count_type_leaves(at.element_type(), elem_size_leaves))
214 return true;
215
216 mp_integer this_idx = offset / (*elem_size_bytes);
217 if(this_idx>=array_size_vec[0])
218 return true;
219
220 mp_integer subtype_result;
222 at.element_type(), offset % (*elem_size_bytes), subtype_result);
223
224 result=subtype_result+(elem_size_leaves*this_idx);
225 return ret;
226 }
227 else
228 {
229 result=0;
230 // Can't currently subdivide a primitive.
231 return offset!=0;
232 }
233}
234
242 const typet &source_type,
243 const mp_integer &full_cell_offset,
244 mp_integer &result)
245{
246 if(source_type.id()==ID_struct)
247 {
248 const auto &st=to_struct_type(source_type);
249 mp_integer cell_offset=full_cell_offset;
250
251 for(const auto &comp : st.components())
252 {
253 mp_integer component_count;
254 if(count_type_leaves(comp.type(), component_count))
255 return true;
256 if(component_count>cell_offset)
257 {
258 mp_integer subtype_result;
260 comp.type(), cell_offset, subtype_result);
261 const auto member_offset_result =
262 member_offset(st, comp.get_name(), ns);
263 CHECK_RETURN(member_offset_result.has_value());
264 result = member_offset_result.value() + subtype_result;
265 return ret;
266 }
267 else
268 {
269 cell_offset-=component_count;
270 }
271 }
272 // Ran out of members, or member of indefinite size
273 return true;
274 }
275 else if(source_type.id()==ID_array)
276 {
277 const auto &at=to_array_type(source_type);
278
279 mp_vectort array_size_vec = evaluate(at.size());
280 if(array_size_vec.size()!=1)
281 return true;
282
283 auto elem_size = pointer_offset_size(at.element_type(), ns);
284 if(!elem_size.has_value())
285 return true;
286
287 mp_integer elem_count;
288 if(count_type_leaves(at.element_type(), elem_count))
289 return true;
290
291 mp_integer this_idx=full_cell_offset/elem_count;
292 if(this_idx>=array_size_vec[0])
293 return true;
294
295 mp_integer subtype_result;
297 at.element_type(), full_cell_offset % elem_count, subtype_result);
298 result = subtype_result + ((*elem_size) * this_idx);
299 return ret;
300 }
301 else
302 {
303 // Primitive type.
304 result=0;
305 return full_cell_offset!=0;
306 }
307}
308
313{
314 if(expr.id()==ID_constant)
315 {
316 if(expr.type().id()==ID_struct)
317 {
318 mp_vectort dest;
319 dest.reserve(numeric_cast_v<std::size_t>(get_size(expr.type())));
320 bool error=false;
321
322 forall_operands(it, expr)
323 {
324 if(it->type().id()==ID_code)
325 continue;
326
327 mp_integer sub_size=get_size(it->type());
328 if(sub_size==0)
329 continue;
330
331 mp_vectort tmp = evaluate(*it);
332
333 if(tmp.size()==sub_size)
334 {
335 for(std::size_t i=0; i<tmp.size(); ++i)
336 dest.push_back(tmp[i]);
337 }
338 else
339 error=true;
340 }
341
342 if(!error)
343 return dest;
344
345 dest.clear();
346 }
347 else if(expr.type().id() == ID_pointer)
348 {
349 if(expr.has_operands())
350 {
351 const exprt &object = skip_typecast(to_unary_expr(expr).op());
352 if(object.id() == ID_address_of)
353 return evaluate(object);
354 else if(const auto i = numeric_cast<mp_integer>(object))
355 return {*i};
356 }
357 // check if expression is constant null pointer without operands
358 else
359 {
360 const auto i = numeric_cast<mp_integer>(expr);
361 if(i && i->is_zero())
362 return {*i};
363 }
364 }
365 else if(expr.type().id()==ID_floatbv)
366 {
367 ieee_floatt f;
369 return {f.pack()};
370 }
371 else if(expr.type().id()==ID_fixedbv)
372 {
373 fixedbvt f;
375 return {f.get_value()};
376 }
377 else if(expr.type().id()==ID_c_bool)
378 {
379 const irep_idt &value=to_constant_expr(expr).get_value();
380 const auto width = to_c_bool_type(expr.type()).get_width();
381 return {bvrep2integer(value, width, false)};
382 }
383 else if(expr.type().id()==ID_bool)
384 {
385 return {expr.is_true()};
386 }
387 else if(expr.type().id()==ID_string)
388 {
389 const std::string &value = id2string(to_constant_expr(expr).get_value());
390 if(show)
391 output.warning() << "string decoding not fully implemented "
392 << value.size() + 1 << messaget::eom;
393 return {get_string_container()[value]};
394 }
395 else
396 {
397 if(const auto i = numeric_cast<mp_integer>(expr))
398 return {*i};
399 }
400 }
401 else if(expr.id()==ID_struct)
402 {
403 mp_vectort dest;
404
405 if(!unbounded_size(expr.type()))
406 dest.reserve(numeric_cast_v<std::size_t>(get_size(expr.type())));
407
408 bool error=false;
409
410 forall_operands(it, expr)
411 {
412 if(it->type().id()==ID_code)
413 continue;
414
415 mp_integer sub_size=get_size(it->type());
416 if(sub_size==0)
417 continue;
418
419 mp_vectort tmp = evaluate(*it);
420
421 if(unbounded_size(it->type()) || tmp.size()==sub_size)
422 {
423 for(std::size_t i=0; i<tmp.size(); i++)
424 dest.push_back(tmp[i]);
425 }
426 else
427 error=true;
428 }
429
430 if(!error)
431 return dest;
432
433 dest.clear();
434 }
435 else if(expr.id()==ID_side_effect)
436 {
437 side_effect_exprt side_effect=to_side_effect_expr(expr);
438 if(side_effect.get_statement()==ID_nondet)
439 {
440 if(show)
441 output.error() << "nondet not implemented" << messaget::eom;
442 return {};
443 }
444 else if(side_effect.get_statement()==ID_allocate)
445 {
446 if(show)
447 output.error() << "heap memory allocation not fully implemented "
448 << to_pointer_type(expr.type()).base_type().pretty()
449 << messaget::eom;
450 std::stringstream buffer;
452 buffer << "interpreter::dynamic_object" << num_dynamic_objects;
453 irep_idt id(buffer.str().c_str());
456 // TODO: check array of type
457 // TODO: interpret zero-initialization argument
458 return {address};
459 }
460 if(show)
461 output.error() << "side effect not implemented "
462 << side_effect.get_statement() << messaget::eom;
463 }
464 else if(expr.id()==ID_bitor)
465 {
466 if(expr.operands().size()<2)
467 throw id2string(expr.id())+" expects at least two operands";
468
469 mp_integer final=0;
470 forall_operands(it, expr)
471 {
472 mp_vectort tmp = evaluate(*it);
473 if(tmp.size()==1)
474 final=bitwise_or(final, tmp.front());
475 }
476 return {final};
477 }
478 else if(expr.id()==ID_bitand)
479 {
480 if(expr.operands().size()<2)
481 throw id2string(expr.id())+" expects at least two operands";
482
483 mp_integer final=-1;
484 forall_operands(it, expr)
485 {
486 mp_vectort tmp = evaluate(*it);
487 if(tmp.size()==1)
488 final=bitwise_and(final, tmp.front());
489 }
490
491 return {final};
492 }
493 else if(expr.id()==ID_bitxor)
494 {
495 if(expr.operands().size()<2)
496 throw id2string(expr.id())+" expects at least two operands";
497
498 mp_integer final=0;
499 forall_operands(it, expr)
500 {
501 mp_vectort tmp = evaluate(*it);
502 if(tmp.size()==1)
503 final=bitwise_xor(final, tmp.front());
504 }
505
506 return {final};
507 }
508 else if(expr.id()==ID_bitnot)
509 {
510 mp_vectort tmp = evaluate(to_bitnot_expr(expr).op());
511 if(tmp.size()==1)
512 {
513 const auto width =
514 to_bitvector_type(to_bitnot_expr(expr).op().type()).get_width();
515 const mp_integer mask = power(2, width) - 1;
516
517 return {bitwise_xor(tmp.front(), mask)};
518 }
519 }
520 else if(expr.id()==ID_shl)
521 {
522 mp_vectort tmp0 = evaluate(to_shl_expr(expr).op0());
523 mp_vectort tmp1 = evaluate(to_shl_expr(expr).op1());
524 if(tmp0.size()==1 && tmp1.size()==1)
525 {
527 tmp0.front(),
528 tmp1.front(),
529 to_bitvector_type(to_shl_expr(expr).op0().type()).get_width());
530 return {final};
531 }
532 }
533 else if(expr.id() == ID_shr || expr.id() == ID_lshr)
534 {
535 mp_vectort tmp0 = evaluate(to_shift_expr(expr).op0());
536 mp_vectort tmp1 = evaluate(to_shift_expr(expr).op1());
537 if(tmp0.size()==1 && tmp1.size()==1)
538 {
540 tmp0.front(),
541 tmp1.front(),
542 to_bitvector_type(to_shift_expr(expr).op0().type()).get_width());
543 return {final};
544 }
545 }
546 else if(expr.id()==ID_ashr)
547 {
548 mp_vectort tmp0 = evaluate(to_shift_expr(expr).op0());
549 mp_vectort tmp1 = evaluate(to_shift_expr(expr).op1());
550 if(tmp0.size()==1 && tmp1.size()==1)
551 {
553 tmp0.front(),
554 tmp1.front(),
555 to_bitvector_type(to_shift_expr(expr).op0().type()).get_width());
556 return {final};
557 }
558 }
559 else if(expr.id()==ID_ror)
560 {
561 mp_vectort tmp0 = evaluate(to_binary_expr(expr).op0());
562 mp_vectort tmp1 = evaluate(to_binary_expr(expr).op1());
563 if(tmp0.size()==1 && tmp1.size()==1)
564 {
565 mp_integer final = rotate_right(
566 tmp0.front(),
567 tmp1.front(),
568 to_bitvector_type(to_binary_expr(expr).op0().type()).get_width());
569 return {final};
570 }
571 }
572 else if(expr.id()==ID_rol)
573 {
574 mp_vectort tmp0 = evaluate(to_binary_expr(expr).op0());
575 mp_vectort tmp1 = evaluate(to_binary_expr(expr).op1());
576 if(tmp0.size()==1 && tmp1.size()==1)
577 {
578 mp_integer final = rotate_left(
579 tmp0.front(),
580 tmp1.front(),
581 to_bitvector_type(to_binary_expr(expr).op0().type()).get_width());
582 return {final};
583 }
584 }
585 else if(expr.id()==ID_equal ||
586 expr.id()==ID_notequal ||
587 expr.id()==ID_le ||
588 expr.id()==ID_ge ||
589 expr.id()==ID_lt ||
590 expr.id()==ID_gt)
591 {
592 mp_vectort tmp0 = evaluate(to_binary_expr(expr).op0());
593 mp_vectort tmp1 = evaluate(to_binary_expr(expr).op1());
594
595 if(tmp0.size()==1 && tmp1.size()==1)
596 {
597 const mp_integer &op0=tmp0.front();
598 const mp_integer &op1=tmp1.front();
599
600 if(expr.id()==ID_equal)
601 return {op0 == op1};
602 else if(expr.id()==ID_notequal)
603 return {op0 != op1};
604 else if(expr.id()==ID_le)
605 return {op0 <= op1};
606 else if(expr.id()==ID_ge)
607 return {op0 >= op1};
608 else if(expr.id()==ID_lt)
609 return {op0 < op1};
610 else if(expr.id()==ID_gt)
611 return {op0 > op1};
612 }
613
614 return {};
615 }
616 else if(expr.id()==ID_or)
617 {
618 if(expr.operands().empty())
619 throw id2string(expr.id())+" expects at least one operand";
620
621 bool result=false;
622
623 forall_operands(it, expr)
624 {
625 mp_vectort tmp = evaluate(*it);
626
627 if(tmp.size()==1 && tmp.front()!=0)
628 {
629 result=true;
630 break;
631 }
632 }
633
634 return {result};
635 }
636 else if(expr.id()==ID_if)
637 {
638 const auto &if_expr = to_if_expr(expr);
639
640 mp_vectort tmp0 = evaluate(if_expr.cond());
641 mp_vectort tmp1;
642
643 if(tmp0.size()==1)
644 {
645 if(tmp0.front()!=0)
646 tmp1 = evaluate(if_expr.true_case());
647 else
648 tmp1 = evaluate(if_expr.false_case());
649 }
650
651 if(tmp1.size()==1)
652 return {tmp1.front()};
653
654 return {};
655 }
656 else if(expr.id()==ID_and)
657 {
658 if(expr.operands().empty())
659 throw id2string(expr.id())+" expects at least one operand";
660
661 bool result=true;
662
663 forall_operands(it, expr)
664 {
665 mp_vectort tmp = evaluate(*it);
666
667 if(tmp.size()==1 && tmp.front()==0)
668 {
669 result=false;
670 break;
671 }
672 }
673
674 return {result};
675 }
676 else if(expr.id()==ID_not)
677 {
678 mp_vectort tmp = evaluate(to_not_expr(expr).op());
679
680 if(tmp.size()==1)
681 return {tmp.front() == 0};
682
683 return {};
684 }
685 else if(expr.id()==ID_plus)
686 {
687 mp_integer result=0;
688
689 forall_operands(it, expr)
690 {
691 mp_vectort tmp = evaluate(*it);
692 if(tmp.size()==1)
693 result+=tmp.front();
694 }
695
696 return {result};
697 }
698 else if(expr.id()==ID_mult)
699 {
700 // type-dependent!
701 mp_integer result;
702
703 if(expr.type().id()==ID_fixedbv)
704 {
705 fixedbvt f;
707 f.from_integer(1);
708 result=f.get_value();
709 }
710 else if(expr.type().id()==ID_floatbv)
711 {
713 f.from_integer(1);
714 result=f.pack();
715 }
716 else
717 result=1;
718
719 forall_operands(it, expr)
720 {
721 mp_vectort tmp = evaluate(*it);
722 if(tmp.size()==1)
723 {
724 if(expr.type().id()==ID_fixedbv)
725 {
726 fixedbvt f1, f2;
728 f2.spec=fixedbv_spect(to_fixedbv_type(it->type()));
729 f1.set_value(result);
730 f2.set_value(tmp.front());
731 f1*=f2;
732 result=f1.get_value();
733 }
734 else if(expr.type().id()==ID_floatbv)
735 {
736 ieee_floatt f1(to_floatbv_type(expr.type()));
737 ieee_floatt f2(to_floatbv_type(it->type()));
738 f1.unpack(result);
739 f2.unpack(tmp.front());
740 f1*=f2;
741 result=f2.pack();
742 }
743 else
744 result*=tmp.front();
745 }
746 }
747
748 return {result};
749 }
750 else if(expr.id()==ID_minus)
751 {
752 mp_vectort tmp0 = evaluate(to_minus_expr(expr).op0());
753 mp_vectort tmp1 = evaluate(to_minus_expr(expr).op1());
754
755 if(tmp0.size()==1 && tmp1.size()==1)
756 return {tmp0.front() - tmp1.front()};
757 return {};
758 }
759 else if(expr.id()==ID_div)
760 {
761 mp_vectort tmp0 = evaluate(to_div_expr(expr).op0());
762 mp_vectort tmp1 = evaluate(to_div_expr(expr).op1());
763
764 if(tmp0.size()==1 && tmp1.size()==1)
765 return {tmp0.front() / tmp1.front()};
766 return {};
767 }
768 else if(expr.id()==ID_unary_minus)
769 {
770 mp_vectort tmp0 = evaluate(to_unary_minus_expr(expr).op());
771
772 if(tmp0.size()==1)
773 return {-tmp0.front()};
774 return {};
775 }
776 else if(expr.id()==ID_address_of)
777 {
778 return {evaluate_address(to_address_of_expr(expr).op())};
779 }
780 else if(expr.id()==ID_pointer_offset)
781 {
782 if(expr.operands().size()!=1)
783 throw "pointer_offset expects one operand";
784
785 if(to_unary_expr(expr).op().type().id() != ID_pointer)
786 throw "pointer_offset expects a pointer operand";
787
788 mp_vectort result = evaluate(to_unary_expr(expr).op());
789
790 if(result.size()==1)
791 {
792 // Return the distance, in bytes, between the address returned
793 // and the beginning of the underlying object.
794 mp_integer address=result[0];
795 if(address>0 && address<memory.size())
796 {
797 auto obj_type = address_to_symbol(address).type();
798
799 mp_integer offset=address_to_offset(address);
800 mp_integer byte_offset;
801 if(!memory_offset_to_byte_offset(obj_type, offset, byte_offset))
802 return {byte_offset};
803 }
804 }
805 return {};
806 }
807 else if(
808 expr.id() == ID_dereference || expr.id() == ID_index ||
809 expr.id() == ID_symbol || expr.id() == ID_member ||
810 expr.id() == ID_byte_extract_little_endian ||
811 expr.id() == ID_byte_extract_big_endian)
812 {
814 expr,
815 true); // fail quietly
816
817 if(address.is_zero())
818 {
819 exprt simplified;
820 // In case of being an indexed access, try to evaluate the index, then
821 // simplify.
822 if(expr.id() == ID_index)
823 {
824 index_exprt evaluated_index = to_index_expr(expr);
825 mp_vectort idx = evaluate(to_index_expr(expr).index());
826 if(idx.size() == 1)
827 {
828 evaluated_index.index() =
829 from_integer(idx[0], to_index_expr(expr).index().type());
830 }
831 simplified = simplify_expr(evaluated_index, ns);
832 }
833 else
834 {
835 // Try reading from a constant -- simplify_expr has all the relevant
836 // cases (index-of-constant-array, member-of-constant-struct and so on)
837 // Note we complain of a problem even if simplify did *something* but
838 // still left us with an unresolved index, member, etc.
839 simplified = simplify_expr(expr, ns);
840 }
841
842 if(simplified.id() == expr.id())
843 evaluate_address(expr); // Evaluate again to print error message.
844 else
845 return evaluate(simplified);
846 }
847 else if(!address.is_zero())
848 {
849 if(
850 expr.id() == ID_byte_extract_little_endian ||
851 expr.id() == ID_byte_extract_big_endian)
852 {
853 const auto &byte_extract_expr = to_byte_extract_expr(expr);
854
855 mp_vectort extract_from = evaluate(byte_extract_expr.op());
856 INVARIANT(
857 !extract_from.empty(),
858 "evaluate_address should have returned address == 0");
859 const mp_integer memory_offset =
860 address - evaluate_address(byte_extract_expr.op(), true);
861 const typet &target_type = expr.type();
862 mp_integer target_type_leaves;
863 if(
864 !count_type_leaves(target_type, target_type_leaves) &&
865 target_type_leaves > 0)
866 {
867 mp_vectort dest;
868 dest.insert(
869 dest.end(),
870 extract_from.begin() + numeric_cast_v<std::size_t>(memory_offset),
871 extract_from.begin() +
872 numeric_cast_v<std::size_t>(memory_offset + target_type_leaves));
873 return dest;
874 }
875 // we fail
876 }
877 else if(!unbounded_size(expr.type()))
878 {
879 mp_vectort dest;
880 dest.resize(numeric_cast_v<std::size_t>(get_size(expr.type())));
881 read(address, dest);
882 return dest;
883 }
884 else
885 {
886 mp_vectort dest;
887 read_unbounded(address, dest);
888 return dest;
889 }
890 }
891 }
892 else if(expr.id()==ID_typecast)
893 {
894 mp_vectort tmp = evaluate(to_typecast_expr(expr).op());
895
896 if(tmp.size()==1)
897 {
898 const mp_integer &value=tmp.front();
899
900 if(expr.type().id()==ID_pointer)
901 {
902 return {value};
903 }
904 else if(expr.type().id()==ID_signedbv)
905 {
906 const auto width = to_signedbv_type(expr.type()).get_width();
907 const auto s = integer2bvrep(value, width);
908 return {bvrep2integer(s, width, true)};
909 }
910 else if(expr.type().id()==ID_unsignedbv)
911 {
912 const auto width = to_unsignedbv_type(expr.type()).get_width();
913 const auto s = integer2bvrep(value, width);
914 return {bvrep2integer(s, width, false)};
915 }
916 else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))
917 return {value != 0};
918 }
919 }
920 else if(expr.id()==ID_array)
921 {
922 mp_vectort dest;
923 forall_operands(it, expr)
924 {
925 mp_vectort tmp = evaluate(*it);
926 dest.insert(dest.end(), tmp.begin(), tmp.end());
927 }
928 return dest;
929 }
930 else if(expr.id()==ID_array_of)
931 {
932 const auto &ty=to_array_type(expr.type());
933
934 mp_vectort size;
935 if(ty.size().id()==ID_infinity)
936 size.push_back(0);
937 else
938 size = evaluate(ty.size());
939
940 if(size.size()==1)
941 {
942 std::size_t size_int = numeric_cast_v<std::size_t>(size[0]);
943 mp_vectort tmp = evaluate(to_array_of_expr(expr).op());
944 mp_vectort dest;
945 for(std::size_t i=0; i<size_int; ++i)
946 dest.insert(dest.end(), tmp.begin(), tmp.end());
947 return dest;
948 }
949 }
950 else if(expr.id()==ID_with)
951 {
952 const auto &wexpr=to_with_expr(expr);
953
954 mp_vectort dest = evaluate(wexpr.old());
955 mp_vectort where = evaluate(wexpr.where());
956 mp_vectort new_value = evaluate(wexpr.new_value());
957
958 const auto &subtype = to_array_type(expr.type()).element_type();
959
960 if(!new_value.empty() && where.size()==1 && !unbounded_size(subtype))
961 {
962 // Ignore indices < 0, which the string solver sometimes produces
963 if(where[0]<0)
964 return {};
965
966 mp_integer where_idx=where[0];
967 mp_integer subtype_size=get_size(subtype);
968 mp_integer need_size=(where_idx+1)*subtype_size;
969
970 if(dest.size()<need_size)
971 dest.resize(numeric_cast_v<std::size_t>(need_size), 0);
972
973 for(std::size_t i=0; i<new_value.size(); ++i)
974 dest[numeric_cast_v<std::size_t>((where_idx * subtype_size) + i)] =
975 new_value[i];
976
977 return {};
978 }
979 }
980 else if(expr.id()==ID_nil)
981 {
982 return {0};
983 }
984 else if(expr.id()==ID_infinity)
985 {
986 if(expr.type().id()==ID_signedbv)
987 {
988 output.warning() << "Infinite size arrays not supported" << messaget::eom;
989 return {};
990 }
991 }
992 output.error() << "!! failed to evaluate expression: "
993 << from_expr(ns, function->first, expr) << "\n"
994 << expr.id() << "[" << expr.type().id() << "]"
995 << messaget::eom;
996 return {};
997}
998
1000 const exprt &expr,
1001 bool fail_quietly)
1002{
1003 if(expr.id()==ID_symbol)
1004 {
1005 const irep_idt &identifier = is_ssa_expr(expr)
1008
1009 interpretert::memory_mapt::const_iterator m_it1=
1010 memory_map.find(identifier);
1011
1012 if(m_it1!=memory_map.end())
1013 return m_it1->second;
1014
1015 if(!call_stack.empty())
1016 {
1017 interpretert::memory_mapt::const_iterator m_it2=
1018 call_stack.top().local_map.find(identifier);
1019
1020 if(m_it2!=call_stack.top().local_map.end())
1021 return m_it2->second;
1022 }
1023 mp_integer address=memory.size();
1025 return address;
1026 }
1027 else if(expr.id()==ID_dereference)
1028 {
1029 mp_vectort tmp0 = evaluate(to_dereference_expr(expr).op());
1030
1031 if(tmp0.size()==1)
1032 return tmp0.front();
1033 }
1034 else if(expr.id()==ID_index)
1035 {
1036 mp_vectort tmp1 = evaluate(to_index_expr(expr).index());
1037
1038 if(tmp1.size()==1)
1039 {
1040 auto base = evaluate_address(to_index_expr(expr).array(), fail_quietly);
1041 if(!base.is_zero())
1042 return base+tmp1.front();
1043 }
1044 }
1045 else if(expr.id()==ID_member)
1046 {
1047 const struct_typet &struct_type =
1048 to_struct_type(ns.follow(to_member_expr(expr).compound().type()));
1049
1050 const irep_idt &component_name=
1052
1053 mp_integer offset=0;
1054
1055 for(const auto &comp : struct_type.components())
1056 {
1057 if(comp.get_name()==component_name)
1058 break;
1059
1060 offset+=get_size(comp.type());
1061 }
1062
1063 auto base = evaluate_address(to_member_expr(expr).compound(), fail_quietly);
1064 if(!base.is_zero())
1065 return base+offset;
1066 }
1067 else if(expr.id()==ID_byte_extract_little_endian ||
1068 expr.id()==ID_byte_extract_big_endian)
1069 {
1070 const auto &byte_extract_expr = to_byte_extract_expr(expr);
1071 mp_vectort extract_offset = evaluate(byte_extract_expr.op1());
1072 mp_vectort extract_from = evaluate(byte_extract_expr.op0());
1073 if(extract_offset.size()==1 && !extract_from.empty())
1074 {
1075 mp_integer memory_offset;
1077 byte_extract_expr.op0().type(), extract_offset[0], memory_offset))
1078 return evaluate_address(byte_extract_expr.op0(), fail_quietly) +
1079 memory_offset;
1080 }
1081 }
1082 else if(expr.id()==ID_if)
1083 {
1084 const auto &if_expr = to_if_expr(expr);
1085 if_exprt address_cond(
1086 if_expr.cond(),
1087 address_of_exprt(if_expr.true_case()),
1088 address_of_exprt(if_expr.false_case()));
1089 mp_vectort result = evaluate(address_cond);
1090 if(result.size()==1)
1091 return {result[0]};
1092 }
1093 else if(expr.id()==ID_typecast)
1094 {
1095 return evaluate_address(to_typecast_expr(expr).op(), fail_quietly);
1096 }
1097
1098 if(!fail_quietly)
1099 {
1100 output.error() << "!! failed to evaluate address: "
1101 << from_expr(ns, function->first, expr) << messaget::eom;
1102 }
1103
1104 return 0;
1105}
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:106
Operator to return the address of an object.
Definition: pointer_expr.h:361
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
std::size_t get_width() const
Definition: std_types.h:864
const irep_idt & get_value() const
Definition: std_expr.h:2815
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
fixedbv_spect spec
Definition: fixedbv.h:44
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
void from_expr(const constant_exprt &expr)
Definition: fixedbv.cpp:26
const mp_integer & get_value() const
Definition: fixedbv.h:95
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:320
void from_expr(const constant_exprt &expr)
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:516
mp_integer pack() const
Definition: ieee_float.cpp:375
The trinary if-then-else operator.
Definition: std_expr.h:2226
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
void clear_input_flags()
Clears memoy r/w flag initialization.
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
mp_integer base_address_to_actual_size(const mp_integer &address) const
memory_mapt memory_map
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
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',...
goto_functionst::function_mapt::const_iterator function
symbol_exprt address_to_symbol(const mp_integer &address) const
call_stackt call_stack
void build_memory_map()
Creates a memory map of all static symbols in the program.
std::vector< mp_integer > mp_vectort
mp_vectort evaluate(const exprt &)
Evaluate an expression.
void allocate(const mp_integer &address, const mp_integer &size)
reserves memory block of size at address
void read(const mp_integer &address, mp_vectort &dest) const
Reads a memory address and loads it into the dest variable.
mp_integer address_to_offset(const mp_integer &address) const
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 namespacet ns
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
bool unbounded_size(const typet &)
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 read_unbounded(const mp_integer &address, mp_vectort &dest) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & id() const
Definition: irep.h:396
irep_idt get_component_name() const
Definition: std_expr.h:2681
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
An expression containing a side effect.
Definition: std_code.h:1450
const irep_idt & get_statement() const
Definition: std_code.h:1472
uint64_t size() const
Definition: sparse_vector.h:43
const irep_idt get_original_name() const
Definition: ssa_expr.h:49
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The type of an expression, extends irept.
Definition: type.h:29
#define forall_operands(it, expr)
Definition: expr.h:18
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
Deprecated expression utility functions.
Interpreter for GOTO Programs.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &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,...
Definition: mp_arith.cpp:317
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 ...
Definition: mp_arith.cpp:253
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,...
Definition: mp_arith.cpp:272
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...
Definition: mp_arith.cpp:333
mp_integer bitwise_and(const mp_integer &a, const mp_integer &b)
bitwise 'and' of two nonnegative integers
Definition: mp_arith.cpp:227
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
Definition: mp_arith.cpp:215
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
Definition: mp_arith.cpp:239
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 ...
Definition: mp_arith.cpp:353
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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.
Pointer Logic.
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1456
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1113
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2374
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
Container for C-Strings.
string_containert & get_string_container()
Get a reference to the global string container.