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