CBMC
interpreter_evaluate.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interpreter for GOTO Programs
4 
5 Author: 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>
24 #include <util/string_container.h>
25 
26 #include <langapi/language_util.h>
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;
182  bool ret = byte_offset_to_memory_offset(
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;
221  bool ret = byte_offset_to_memory_offset(
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;
296  bool ret = memory_offset_to_byte_offset(
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.is_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  for(const auto &op : expr.operands())
323  {
324  if(op.type().id() == ID_code)
325  continue;
326 
327  mp_integer sub_size = get_size(op.type());
328  if(sub_size==0)
329  continue;
330 
331  mp_vectort tmp = evaluate(op);
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;
368  f.from_expr(to_constant_expr(expr));
369  return {f.pack()};
370  }
371  else if(expr.type().id()==ID_fixedbv)
372  {
373  fixedbvt f;
374  f.from_expr(to_constant_expr(expr));
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.is_boolean())
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  for(const auto &op : expr.operands())
411  {
412  if(op.type().id() == ID_code)
413  continue;
414 
415  mp_integer sub_size = get_size(op.type());
416  if(sub_size==0)
417  continue;
418 
419  mp_vectort tmp = evaluate(op);
420 
421  if(unbounded_size(op.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());
454  mp_integer address = build_memory_map(
455  symbol_exprt{id, to_pointer_type(expr.type()).base_type()});
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  for(const auto &op : expr.operands())
471  {
472  mp_vectort tmp = evaluate(op);
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  for(const auto &op : expr.operands())
485  {
486  mp_vectort tmp = evaluate(op);
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  for(const auto &op : expr.operands())
500  {
501  mp_vectort tmp = evaluate(op);
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  for(const auto &op : expr.operands())
624  {
625  mp_vectort tmp = evaluate(op);
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  for(const auto &op : expr.operands())
664  {
665  mp_vectort tmp = evaluate(op);
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  for(const auto &op : expr.operands())
690  {
691  mp_vectort tmp = evaluate(op);
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  {
712  ieee_floatt f(to_floatbv_type(expr.type()));
713  f.from_integer(1);
714  result=f.pack();
715  }
716  else
717  result=1;
718 
719  for(const auto &op : expr.operands())
720  {
721  mp_vectort tmp = evaluate(op);
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(op.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(op.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(to_pointer_offset_expr(expr).op().type().id() != ID_pointer)
783  throw "pointer_offset expects a pointer operand";
784 
785  mp_vectort result = evaluate(to_pointer_offset_expr(expr).op());
786 
787  if(result.size()==1)
788  {
789  // Return the distance, in bytes, between the address returned
790  // and the beginning of the underlying object.
791  mp_integer address=result[0];
792  if(address>0 && address<memory.size())
793  {
794  auto obj_type = address_to_symbol(address).type();
795 
796  mp_integer offset=address_to_offset(address);
797  mp_integer byte_offset;
798  if(!memory_offset_to_byte_offset(obj_type, offset, byte_offset))
799  return {byte_offset};
800  }
801  }
802  return {};
803  }
804  else if(
805  expr.id() == ID_dereference || expr.id() == ID_index ||
806  expr.id() == ID_symbol || expr.id() == ID_member ||
807  expr.id() == ID_byte_extract_little_endian ||
808  expr.id() == ID_byte_extract_big_endian)
809  {
811  expr,
812  true); // fail quietly
813 
814  if(address.is_zero())
815  {
816  exprt simplified;
817  // In case of being an indexed access, try to evaluate the index, then
818  // simplify.
819  if(expr.id() == ID_index)
820  {
821  index_exprt evaluated_index = to_index_expr(expr);
822  mp_vectort idx = evaluate(to_index_expr(expr).index());
823  if(idx.size() == 1)
824  {
825  evaluated_index.index() =
826  from_integer(idx[0], to_index_expr(expr).index().type());
827  }
828  simplified = simplify_expr(evaluated_index, ns);
829  }
830  else
831  {
832  // Try reading from a constant -- simplify_expr has all the relevant
833  // cases (index-of-constant-array, member-of-constant-struct and so on)
834  // Note we complain of a problem even if simplify did *something* but
835  // still left us with an unresolved index, member, etc.
836  simplified = simplify_expr(expr, ns);
837  }
838 
839  if(simplified.id() == expr.id())
840  evaluate_address(expr); // Evaluate again to print error message.
841  else
842  return evaluate(simplified);
843  }
844  else if(!address.is_zero())
845  {
846  if(
847  expr.id() == ID_byte_extract_little_endian ||
848  expr.id() == ID_byte_extract_big_endian)
849  {
850  const auto &byte_extract_expr = to_byte_extract_expr(expr);
851 
852  mp_vectort extract_from = evaluate(byte_extract_expr.op());
853  INVARIANT(
854  !extract_from.empty(),
855  "evaluate_address should have returned address == 0");
856  const mp_integer memory_offset =
857  address - evaluate_address(byte_extract_expr.op(), true);
858  const typet &target_type = expr.type();
859  mp_integer target_type_leaves;
860  if(
861  !count_type_leaves(target_type, target_type_leaves) &&
862  target_type_leaves > 0)
863  {
864  mp_vectort dest;
865  dest.insert(
866  dest.end(),
867  extract_from.begin() + numeric_cast_v<std::size_t>(memory_offset),
868  extract_from.begin() +
869  numeric_cast_v<std::size_t>(memory_offset + target_type_leaves));
870  return dest;
871  }
872  // we fail
873  }
874  else if(!unbounded_size(expr.type()))
875  {
876  mp_vectort dest;
877  dest.resize(numeric_cast_v<std::size_t>(get_size(expr.type())));
878  read(address, dest);
879  return dest;
880  }
881  else
882  {
883  mp_vectort dest;
884  read_unbounded(address, dest);
885  return dest;
886  }
887  }
888  }
889  else if(expr.id()==ID_typecast)
890  {
891  mp_vectort tmp = evaluate(to_typecast_expr(expr).op());
892 
893  if(tmp.size()==1)
894  {
895  const mp_integer &value=tmp.front();
896 
897  if(expr.type().id()==ID_pointer)
898  {
899  return {value};
900  }
901  else if(expr.type().id()==ID_signedbv)
902  {
903  const auto width = to_signedbv_type(expr.type()).get_width();
904  const auto s = integer2bvrep(value, width);
905  return {bvrep2integer(s, width, true)};
906  }
907  else if(expr.type().id()==ID_unsignedbv)
908  {
909  const auto width = to_unsignedbv_type(expr.type()).get_width();
910  const auto s = integer2bvrep(value, width);
911  return {bvrep2integer(s, width, false)};
912  }
913  else if(expr.is_boolean() || expr.type().id() == ID_c_bool)
914  return {value != 0};
915  }
916  }
917  else if(expr.id()==ID_array)
918  {
919  mp_vectort dest;
920  for(const auto &op : expr.operands())
921  {
922  mp_vectort tmp = evaluate(op);
923  dest.insert(dest.end(), tmp.begin(), tmp.end());
924  }
925  return dest;
926  }
927  else if(expr.id()==ID_array_of)
928  {
929  const auto &ty=to_array_type(expr.type());
930 
931  mp_vectort size;
932  if(ty.size().id()==ID_infinity)
933  size.push_back(0);
934  else
935  size = evaluate(ty.size());
936 
937  if(size.size()==1)
938  {
939  std::size_t size_int = numeric_cast_v<std::size_t>(size[0]);
940  mp_vectort tmp = evaluate(to_array_of_expr(expr).op());
941  mp_vectort dest;
942  for(std::size_t i=0; i<size_int; ++i)
943  dest.insert(dest.end(), tmp.begin(), tmp.end());
944  return dest;
945  }
946  }
947  else if(expr.id()==ID_with)
948  {
949  const auto &wexpr=to_with_expr(expr);
950 
951  mp_vectort dest = evaluate(wexpr.old());
952  mp_vectort where = evaluate(wexpr.where());
953  mp_vectort new_value = evaluate(wexpr.new_value());
954 
955  const auto &subtype = to_array_type(expr.type()).element_type();
956 
957  if(!new_value.empty() && where.size()==1 && !unbounded_size(subtype))
958  {
959  // Ignore indices < 0, which the string solver sometimes produces
960  if(where[0]<0)
961  return {};
962 
963  mp_integer where_idx=where[0];
964  mp_integer subtype_size=get_size(subtype);
965  mp_integer need_size=(where_idx+1)*subtype_size;
966 
967  if(dest.size()<need_size)
968  dest.resize(numeric_cast_v<std::size_t>(need_size), 0);
969 
970  for(std::size_t i=0; i<new_value.size(); ++i)
971  dest[numeric_cast_v<std::size_t>((where_idx * subtype_size) + i)] =
972  new_value[i];
973 
974  return {};
975  }
976  }
977  else if(expr.id()==ID_nil)
978  {
979  return {0};
980  }
981  else if(expr.id()==ID_infinity)
982  {
983  if(expr.type().id()==ID_signedbv)
984  {
985  output.warning() << "Infinite size arrays not supported" << messaget::eom;
986  return {};
987  }
988  }
989  output.error() << "!! failed to evaluate expression: "
990  << from_expr(ns, function->first, expr) << "\n"
991  << expr.id() << "[" << expr.type().id() << "]"
992  << messaget::eom;
993  return {};
994 }
995 
997  const exprt &expr,
998  bool fail_quietly)
999 {
1000  if(expr.id()==ID_symbol)
1001  {
1002  const irep_idt &identifier = is_ssa_expr(expr)
1003  ? to_ssa_expr(expr).get_original_name()
1004  : to_symbol_expr(expr).get_identifier();
1005 
1006  interpretert::memory_mapt::const_iterator m_it1=
1007  memory_map.find(identifier);
1008 
1009  if(m_it1!=memory_map.end())
1010  return m_it1->second;
1011 
1012  if(!call_stack.empty())
1013  {
1014  interpretert::memory_mapt::const_iterator m_it2=
1015  call_stack.top().local_map.find(identifier);
1016 
1017  if(m_it2!=call_stack.top().local_map.end())
1018  return m_it2->second;
1019  }
1020  mp_integer address=memory.size();
1022  return address;
1023  }
1024  else if(expr.id()==ID_dereference)
1025  {
1026  mp_vectort tmp0 = evaluate(to_dereference_expr(expr).op());
1027 
1028  if(tmp0.size()==1)
1029  return tmp0.front();
1030  }
1031  else if(expr.id()==ID_index)
1032  {
1033  mp_vectort tmp1 = evaluate(to_index_expr(expr).index());
1034 
1035  if(tmp1.size()==1)
1036  {
1037  auto base = evaluate_address(to_index_expr(expr).array(), fail_quietly);
1038  if(!base.is_zero())
1039  return base+tmp1.front();
1040  }
1041  }
1042  else if(expr.id()==ID_member)
1043  {
1044  const struct_typet &struct_type =
1045  to_struct_type(ns.follow(to_member_expr(expr).compound().type()));
1046 
1047  const irep_idt &component_name=
1049 
1050  mp_integer offset=0;
1051 
1052  for(const auto &comp : struct_type.components())
1053  {
1054  if(comp.get_name()==component_name)
1055  break;
1056 
1057  offset+=get_size(comp.type());
1058  }
1059 
1060  auto base = evaluate_address(to_member_expr(expr).compound(), fail_quietly);
1061  if(!base.is_zero())
1062  return base+offset;
1063  }
1064  else if(expr.id()==ID_byte_extract_little_endian ||
1065  expr.id()==ID_byte_extract_big_endian)
1066  {
1067  const auto &byte_extract_expr = to_byte_extract_expr(expr);
1068  mp_vectort extract_offset = evaluate(byte_extract_expr.op1());
1069  mp_vectort extract_from = evaluate(byte_extract_expr.op0());
1070  if(extract_offset.size()==1 && !extract_from.empty())
1071  {
1072  mp_integer memory_offset;
1074  byte_extract_expr.op0().type(), extract_offset[0], memory_offset))
1075  return evaluate_address(byte_extract_expr.op0(), fail_quietly) +
1076  memory_offset;
1077  }
1078  }
1079  else if(expr.id()==ID_if)
1080  {
1081  const auto &if_expr = to_if_expr(expr);
1082  if_exprt address_cond(
1083  if_expr.cond(),
1084  address_of_exprt(if_expr.true_case()),
1085  address_of_exprt(if_expr.false_case()));
1086  mp_vectort result = evaluate(address_cond);
1087  if(result.size()==1)
1088  return {result[0]};
1089  }
1090  else if(expr.id()==ID_typecast)
1091  {
1092  return evaluate_address(to_typecast_expr(expr).op(), fail_quietly);
1093  }
1094 
1095  if(!fail_quietly)
1096  {
1097  output.error() << "!! failed to evaluate address: "
1098  << from_expr(ns, function->first, expr) << messaget::eom;
1099  }
1100 
1101  return 0;
1102 }
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)
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 bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
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.
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:128
Operator to return the address of an object.
Definition: pointer_expr.h:540
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
std::size_t get_width() const
Definition: std_types.h:920
const irep_idt & get_value() const
Definition: std_expr.h:2995
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:91
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.h:224
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
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
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
const mp_integer & get_value() const
Definition: fixedbv.h:95
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:2370
Array index operator.
Definition: std_expr.h:1465
exprt & index()
Definition: std_expr.h:1505
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:482
const irep_idt & id() const
Definition: irep.h:384
irep_idt get_component_name() const
Definition: std_expr.h:2863
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:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
The type of an expression, extends irept.
Definition: type.h:29
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:219
Deprecated expression utility functions.
Interpreter for GOTO Programs.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
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 pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< 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:17
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
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:80
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3037
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2102
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2352
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:514
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1201
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1086
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2533
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:715
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1598
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2933
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:426
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
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:888
Container for C-Strings.
string_containert & get_string_container()
Get a reference to the global string container.