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/byte_operators.h>
15 #include <util/fixedbv.h>
16 #include <util/ieee_float.h>
18 #include <util/simplify_expr.h>
19 #include <util/string_container.h>
20 
21 #include <langapi/language_util.h>
22 #include <util/expr_util.h>
23 
27  const mp_integer &address,
28  mp_vectort &dest) const
29 {
30  // copy memory region
31  for(std::size_t i=0; i<dest.size(); ++i)
32  {
33  mp_integer value;
34 
35  if((address+i)<memory.size())
36  {
37  const memory_cellt &cell =
38  memory[numeric_cast_v<std::size_t>(address + i)];
39  value=cell.value;
42  }
43  else
44  value=0;
45 
46  dest[i]=value;
47  }
48 }
49 
51  const mp_integer &address,
52  mp_vectort &dest) const
53 {
54  // copy memory region
55  std::size_t address_val = numeric_cast_v<std::size_t>(address);
56  const mp_integer offset=address_to_offset(address_val);
57  const mp_integer alloc_size=
58  base_address_to_actual_size(address_val-offset);
59  const mp_integer to_read=alloc_size-offset;
60  for(size_t i=0; i<to_read; i++)
61  {
62  mp_integer value;
63 
64  if((address+i)<memory.size())
65  {
66  const memory_cellt &cell =
67  memory[numeric_cast_v<std::size_t>(address + i)];
68  value=cell.value;
71  }
72  else
73  value=0;
74 
75  dest.push_back(value);
76  }
77 }
78 
81  const mp_integer &address,
82  const mp_integer &size)
83 {
84  // clear memory region
85  for(mp_integer i=0; i<size; ++i)
86  {
87  if((address+i)<memory.size())
88  {
89  memory_cellt &cell = memory[numeric_cast_v<std::size_t>(address + i)];
90  cell.value=0;
92  }
93  }
94 }
95 
98 {
99  for(auto &cell : memory)
100  {
101  if(cell.second.initialized==
103  cell.second.initialized=memory_cellt::initializedt::UNKNOWN;
104  }
105 }
106 
114 {
115  if(ty.id()==ID_struct)
116  {
117  result=0;
118  mp_integer subtype_count;
119  for(const auto &component : to_struct_type(ty).components())
120  {
121  if(count_type_leaves(component.type(), subtype_count))
122  return true;
123  result+=subtype_count;
124  }
125  return false;
126  }
127  else if(ty.id()==ID_array)
128  {
129  const auto &at=to_array_type(ty);
130  mp_vectort array_size_vec;
131  evaluate(at.size(), array_size_vec);
132  if(array_size_vec.size()!=1)
133  return true;
134  mp_integer subtype_count;
135  if(count_type_leaves(at.subtype(), subtype_count))
136  return true;
137  result=array_size_vec[0]*subtype_count;
138  return false;
139  }
140  else
141  {
142  result=1;
143  return false;
144  }
145 }
146 
157  const typet &source_type,
158  const mp_integer &offset,
159  mp_integer &result)
160 {
161  if(source_type.id()==ID_struct)
162  {
163  const auto &st=to_struct_type(source_type);
164  mp_integer previous_member_offsets=0;
165 
166  for(const auto &comp : st.components())
167  {
168  const auto comp_offset = member_offset(st, comp.get_name(), ns);
169 
170  const auto component_byte_size = pointer_offset_size(comp.type(), ns);
171 
172  if(!comp_offset.has_value() && !component_byte_size.has_value())
173  return true;
174 
175  if(*comp_offset + *component_byte_size > offset)
176  {
177  mp_integer subtype_result;
178  bool ret = byte_offset_to_memory_offset(
179  comp.type(), offset - *comp_offset, subtype_result);
180  result=previous_member_offsets+subtype_result;
181  return ret;
182  }
183  else
184  {
185  mp_integer component_count;
186  if(count_type_leaves(comp.type(), component_count))
187  return true;
188  previous_member_offsets+=component_count;
189  }
190  }
191  // Ran out of struct members, or struct contained a variable-length field.
192  return true;
193  }
194  else if(source_type.id()==ID_array)
195  {
196  const auto &at=to_array_type(source_type);
197 
198  mp_vectort array_size_vec;
199  evaluate(at.size(), array_size_vec);
200 
201  if(array_size_vec.size()!=1)
202  return true;
203 
204  mp_integer array_size=array_size_vec[0];
205  auto elem_size_bytes = pointer_offset_size(at.subtype(), ns);
206  if(!elem_size_bytes.has_value() || *elem_size_bytes == 0)
207  return true;
208 
209  mp_integer elem_size_leaves;
210  if(count_type_leaves(at.subtype(), elem_size_leaves))
211  return true;
212 
213  mp_integer this_idx = offset / (*elem_size_bytes);
214  if(this_idx>=array_size_vec[0])
215  return true;
216 
217  mp_integer subtype_result;
218  bool ret = byte_offset_to_memory_offset(
219  at.subtype(), offset % (*elem_size_bytes), subtype_result);
220 
221  result=subtype_result+(elem_size_leaves*this_idx);
222  return ret;
223  }
224  else
225  {
226  result=0;
227  // Can't currently subdivide a primitive.
228  return offset!=0;
229  }
230 }
231 
239  const typet &source_type,
240  const mp_integer &full_cell_offset,
241  mp_integer &result)
242 {
243  if(source_type.id()==ID_struct)
244  {
245  const auto &st=to_struct_type(source_type);
246  mp_integer cell_offset=full_cell_offset;
247 
248  for(const auto &comp : st.components())
249  {
250  mp_integer component_count;
251  if(count_type_leaves(comp.type(), component_count))
252  return true;
253  if(component_count>cell_offset)
254  {
255  mp_integer subtype_result;
257  comp.type(), cell_offset, subtype_result);
258  const auto member_offset_result =
259  member_offset(st, comp.get_name(), ns);
260  CHECK_RETURN(member_offset_result.has_value());
261  result = member_offset_result.value() + subtype_result;
262  return ret;
263  }
264  else
265  {
266  cell_offset-=component_count;
267  }
268  }
269  // Ran out of members, or member of indefinite size
270  return true;
271  }
272  else if(source_type.id()==ID_array)
273  {
274  const auto &at=to_array_type(source_type);
275 
276  mp_vectort array_size_vec;
277  evaluate(at.size(), array_size_vec);
278  if(array_size_vec.size()!=1)
279  return true;
280 
281  auto elem_size = pointer_offset_size(at.subtype(), ns);
282  if(!elem_size.has_value())
283  return true;
284 
285  mp_integer elem_count;
286  if(count_type_leaves(at.subtype(), elem_count))
287  return true;
288 
289  mp_integer this_idx=full_cell_offset/elem_count;
290  if(this_idx>=array_size_vec[0])
291  return true;
292 
293  mp_integer subtype_result;
294  bool ret=
296  at.subtype(),
297  full_cell_offset%elem_count,
298  subtype_result);
299  result = subtype_result + ((*elem_size) * this_idx);
300  return ret;
301  }
302  else
303  {
304  // Primitive type.
305  result=0;
306  return full_cell_offset!=0;
307  }
308 }
309 
314  const exprt &expr,
315  mp_vectort &dest)
316 {
317  if(expr.id()==ID_constant)
318  {
319  if(expr.type().id()==ID_struct)
320  {
321  dest.reserve(numeric_cast_v<std::size_t>(get_size(expr.type())));
322  bool error=false;
323 
324  forall_operands(it, expr)
325  {
326  if(it->type().id()==ID_code)
327  continue;
328 
329  mp_integer sub_size=get_size(it->type());
330  if(sub_size==0)
331  continue;
332 
333  mp_vectort tmp;
334  evaluate(*it, tmp);
335 
336  if(tmp.size()==sub_size)
337  {
338  for(std::size_t i=0; i<tmp.size(); ++i)
339  dest.push_back(tmp[i]);
340  }
341  else
342  error=true;
343  }
344 
345  if(!error)
346  return;
347 
348  dest.clear();
349  }
350  else if(expr.type().id() == ID_pointer)
351  {
352  if(expr.has_operands())
353  {
354  const exprt &object = skip_typecast(to_unary_expr(expr).op());
355  if(object.id() == ID_address_of)
356  {
357  evaluate(object, dest);
358  return;
359  }
360  else if(const auto i = numeric_cast<mp_integer>(object))
361  {
362  dest.push_back(*i);
363  return;
364  }
365  }
366  // check if expression is constant null pointer without operands
367  else
368  {
369  const auto i = numeric_cast<mp_integer>(expr);
370  if(i && i->is_zero())
371  {
372  dest.push_back(*i);
373  return;
374  }
375  }
376  }
377  else if(expr.type().id()==ID_floatbv)
378  {
379  ieee_floatt f;
380  f.from_expr(to_constant_expr(expr));
381  dest.push_back(f.pack());
382  return;
383  }
384  else if(expr.type().id()==ID_fixedbv)
385  {
386  fixedbvt f;
387  f.from_expr(to_constant_expr(expr));
388  dest.push_back(f.get_value());
389  return;
390  }
391  else if(expr.type().id()==ID_c_bool)
392  {
393  const irep_idt &value=to_constant_expr(expr).get_value();
394  const auto width = to_c_bool_type(expr.type()).get_width();
395  dest.push_back(bvrep2integer(value, width, false));
396  return;
397  }
398  else if(expr.type().id()==ID_bool)
399  {
400  dest.push_back(expr.is_true());
401  return;
402  }
403  else if(expr.type().id()==ID_string)
404  {
405  const std::string &value = id2string(to_constant_expr(expr).get_value());
406  if(show)
407  warning() << "string decoding not fully implemented "
408  << value.size() + 1 << eom;
409  dest.push_back(get_string_container()[value]);
410  return;
411  }
412  else
413  {
414  if(const auto i = numeric_cast<mp_integer>(expr))
415  {
416  dest.push_back(*i);
417  return;
418  }
419  }
420  }
421  else if(expr.id()==ID_struct)
422  {
423  if(!unbounded_size(expr.type()))
424  dest.reserve(numeric_cast_v<std::size_t>(get_size(expr.type())));
425 
426  bool error=false;
427 
428  forall_operands(it, expr)
429  {
430  if(it->type().id()==ID_code)
431  continue;
432 
433  mp_integer sub_size=get_size(it->type());
434  if(sub_size==0)
435  continue;
436 
437  mp_vectort tmp;
438  evaluate(*it, tmp);
439 
440  if(unbounded_size(it->type()) || tmp.size()==sub_size)
441  {
442  for(std::size_t i=0; i<tmp.size(); i++)
443  dest.push_back(tmp[i]);
444  }
445  else
446  error=true;
447  }
448 
449  if(!error)
450  return;
451 
452  dest.clear();
453  }
454  else if(expr.id()==ID_side_effect)
455  {
456  side_effect_exprt side_effect=to_side_effect_expr(expr);
457  if(side_effect.get_statement()==ID_nondet)
458  {
459  if(show)
460  error() << "nondet not implemented" << eom;
461  return;
462  }
463  else if(side_effect.get_statement()==ID_allocate)
464  {
465  if(show)
466  error() << "heap memory allocation not fully implemented "
467  << expr.type().subtype().pretty()
468  << eom;
469  std::stringstream buffer;
471  buffer << "interpreter::dynamic_object" << num_dynamic_objects;
472  irep_idt id(buffer.str().c_str());
473  mp_integer address =
474  build_memory_map(symbol_exprt{id, expr.type().subtype()});
475  // TODO: check array of type
476  // TODO: interpret zero-initialization argument
477  dest.push_back(address);
478  return;
479  }
480  if(show)
481  error() << "side effect not implemented "
482  << side_effect.get_statement()
483  << 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!
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 
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(expr.id()==ID_byte_extract_little_endian ||
861  expr.id()==ID_byte_extract_big_endian)
862  {
863  const auto &byte_extract_expr = to_byte_extract_expr(expr);
864 
865  mp_vectort extract_offset;
866  evaluate(byte_extract_expr.op1(), extract_offset);
867  mp_vectort extract_from;
868  evaluate(byte_extract_expr.op0(), extract_from);
869 
870  if(extract_offset.size()==1 && extract_from.size()!=0)
871  {
872  const typet &target_type=expr.type();
873  mp_integer memory_offset;
874  // If memory offset is found (which should normally be the case)
875  // extract the corresponding data from the appropriate memory location
877  byte_extract_expr.op0().type(), extract_offset[0], memory_offset))
878  {
879  mp_integer target_type_leaves;
880  if(!count_type_leaves(target_type, target_type_leaves) &&
881  target_type_leaves>0)
882  {
883  dest.insert(dest.end(),
884  extract_from.begin()+memory_offset.to_long(),
885  extract_from.begin()+(memory_offset+target_type_leaves).to_long());
886  return;
887  }
888  }
889  }
890  }
891  else if(expr.id()==ID_dereference ||
892  expr.id()==ID_index ||
893  expr.id()==ID_symbol ||
894  expr.id()==ID_member)
895  {
897  expr,
898  true); // fail quietly
899 
900  if(address.is_zero())
901  {
902  exprt simplified;
903  // In case of being an indexed access, try to evaluate the index, then
904  // simplify.
905  if(expr.id() == ID_index)
906  {
907  index_exprt evaluated_index = to_index_expr(expr);
908  mp_vectort idx;
909  evaluate(to_index_expr(expr).index(), idx);
910  if(idx.size() == 1)
911  {
912  evaluated_index.index() =
913  from_integer(idx[0], to_index_expr(expr).index().type());
914  }
915  simplified = simplify_expr(evaluated_index, ns);
916  }
917  else
918  {
919  // Try reading from a constant -- simplify_expr has all the relevant
920  // cases (index-of-constant-array, member-of-constant-struct and so on)
921  // Note we complain of a problem even if simplify did *something* but
922  // still left us with an unresolved index, member, etc.
923  simplified = simplify_expr(expr, ns);
924  }
925  if(simplified.id() == expr.id())
926  evaluate_address(expr); // Evaluate again to print error message.
927  else
928  {
929  evaluate(simplified, dest);
930  return;
931  }
932  }
933  else if(!address.is_zero())
934  {
935  if(!unbounded_size(expr.type()))
936  {
937  dest.resize(numeric_cast_v<std::size_t>(get_size(expr.type())));
938  read(address, dest);
939  }
940  else
941  {
942  read_unbounded(address, dest);
943  }
944  return;
945  }
946  }
947  else if(expr.id()==ID_typecast)
948  {
949  mp_vectort tmp;
950  evaluate(to_typecast_expr(expr).op(), tmp);
951 
952  if(tmp.size()==1)
953  {
954  const mp_integer &value=tmp.front();
955 
956  if(expr.type().id()==ID_pointer)
957  {
958  dest.push_back(value);
959  return;
960  }
961  else if(expr.type().id()==ID_signedbv)
962  {
963  const auto width = to_signedbv_type(expr.type()).get_width();
964  const auto s = integer2bvrep(value, width);
965  dest.push_back(bvrep2integer(s, width, true));
966  return;
967  }
968  else if(expr.type().id()==ID_unsignedbv)
969  {
970  const auto width = to_unsignedbv_type(expr.type()).get_width();
971  const auto s = integer2bvrep(value, width);
972  dest.push_back(bvrep2integer(s, width, false));
973  return;
974  }
975  else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))
976  {
977  dest.push_back(value!=0);
978  return;
979  }
980  }
981  }
982  else if(expr.id()==ID_array)
983  {
984  forall_operands(it, expr)
985  {
986  evaluate(*it, dest);
987  }
988  return;
989  }
990  else if(expr.id()==ID_array_of)
991  {
992  const auto &ty=to_array_type(expr.type());
993  std::vector<mp_integer> size;
994  if(ty.size().id()==ID_infinity)
995  size.push_back(0);
996  else
997  evaluate(ty.size(), size);
998 
999  if(size.size()==1)
1000  {
1001  std::size_t size_int = numeric_cast_v<std::size_t>(size[0]);
1002  for(std::size_t i=0; i<size_int; ++i)
1003  evaluate(to_array_of_expr(expr).op(), dest);
1004  return;
1005  }
1006  }
1007  else if(expr.id()==ID_with)
1008  {
1009  const auto &wexpr=to_with_expr(expr);
1010  evaluate(wexpr.old(), dest);
1011  std::vector<mp_integer> where;
1012  std::vector<mp_integer> new_value;
1013  evaluate(wexpr.where(), where);
1014  evaluate(wexpr.new_value(), new_value);
1015  const auto &subtype=expr.type().subtype();
1016  if(!new_value.empty() && where.size()==1 && !unbounded_size(subtype))
1017  {
1018  // Ignore indices < 0, which the string solver sometimes produces
1019  if(where[0]<0)
1020  return;
1021 
1022  mp_integer where_idx=where[0];
1023  mp_integer subtype_size=get_size(subtype);
1024  mp_integer need_size=(where_idx+1)*subtype_size;
1025 
1026  if(dest.size()<need_size)
1027  dest.resize(numeric_cast_v<std::size_t>(need_size), 0);
1028 
1029  for(std::size_t i=0; i<new_value.size(); ++i)
1030  dest[numeric_cast_v<std::size_t>((where_idx * subtype_size) + i)] =
1031  new_value[i];
1032 
1033  return;
1034  }
1035  }
1036  else if(expr.id()==ID_nil)
1037  {
1038  dest.push_back(0);
1039  return;
1040  }
1041  else if(expr.id()==ID_infinity)
1042  {
1043  if(expr.type().id()==ID_signedbv)
1044  {
1045  warning() << "Infinite size arrays not supported" << eom;
1046  return;
1047  }
1048  }
1049  error() << "!! failed to evaluate expression: "
1050  << from_expr(ns, function->first, expr) << "\n"
1051  << expr.id() << "[" << expr.type().id() << "]"
1052  << eom;
1053 }
1054 
1056  const exprt &expr,
1057  bool fail_quietly)
1058 {
1059  if(expr.id()==ID_symbol)
1060  {
1061  const irep_idt &identifier = is_ssa_expr(expr)
1062  ? to_ssa_expr(expr).get_original_name()
1063  : to_symbol_expr(expr).get_identifier();
1064 
1065  interpretert::memory_mapt::const_iterator m_it1=
1066  memory_map.find(identifier);
1067 
1068  if(m_it1!=memory_map.end())
1069  return m_it1->second;
1070 
1071  if(!call_stack.empty())
1072  {
1073  interpretert::memory_mapt::const_iterator m_it2=
1074  call_stack.top().local_map.find(identifier);
1075 
1076  if(m_it2!=call_stack.top().local_map.end())
1077  return m_it2->second;
1078  }
1079  mp_integer address=memory.size();
1081  return address;
1082  }
1083  else if(expr.id()==ID_dereference)
1084  {
1085  mp_vectort tmp0;
1086  evaluate(to_dereference_expr(expr).op(), tmp0);
1087 
1088  if(tmp0.size()==1)
1089  return tmp0.front();
1090  }
1091  else if(expr.id()==ID_index)
1092  {
1093  mp_vectort tmp1;
1094  evaluate(to_index_expr(expr).index(), tmp1);
1095 
1096  if(tmp1.size()==1)
1097  {
1098  auto base = evaluate_address(to_index_expr(expr).array(), fail_quietly);
1099  if(!base.is_zero())
1100  return base+tmp1.front();
1101  }
1102  }
1103  else if(expr.id()==ID_member)
1104  {
1105  const struct_typet &struct_type =
1106  to_struct_type(ns.follow(to_member_expr(expr).compound().type()));
1107 
1108  const irep_idt &component_name=
1110 
1111  mp_integer offset=0;
1112 
1113  for(const auto &comp : struct_type.components())
1114  {
1115  if(comp.get_name()==component_name)
1116  break;
1117 
1118  offset+=get_size(comp.type());
1119  }
1120 
1121  auto base = evaluate_address(to_member_expr(expr).compound(), fail_quietly);
1122  if(!base.is_zero())
1123  return base+offset;
1124  }
1125  else if(expr.id()==ID_byte_extract_little_endian ||
1126  expr.id()==ID_byte_extract_big_endian)
1127  {
1128  const auto &byte_extract_expr = to_byte_extract_expr(expr);
1129  mp_vectort extract_offset;
1130  evaluate(byte_extract_expr.op1(), extract_offset);
1131  mp_vectort extract_from;
1132  evaluate(byte_extract_expr.op0(), extract_from);
1133  if(extract_offset.size()==1 && !extract_from.empty())
1134  {
1135  mp_integer memory_offset;
1137  byte_extract_expr.op0().type(), extract_offset[0], memory_offset))
1138  return evaluate_address(byte_extract_expr.op0(), fail_quietly) +
1139  memory_offset;
1140  }
1141  }
1142  else if(expr.id()==ID_if)
1143  {
1145  const auto &if_expr = to_if_expr(expr);
1146  if_exprt address_cond(
1147  if_expr.cond(),
1148  address_of_exprt(if_expr.true_case()),
1149  address_of_exprt(if_expr.false_case()));
1150  evaluate(address_cond, result);
1151  if(result.size()==1)
1152  return result[0];
1153  }
1154  else if(expr.id()==ID_typecast)
1155  {
1156  return evaluate_address(to_typecast_expr(expr).op(), fail_quietly);
1157  }
1158 
1159  if(!fail_quietly)
1160  {
1161  error() << "!! failed to evaluate address: "
1162  << from_expr(ns, function->first, expr)
1163  << eom;
1164  }
1165 
1166  return 0;
1167 }
to_c_bool_type
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: std_types.h:1636
interpretert::base_address_to_actual_size
mp_integer base_address_to_actual_size(const mp_integer &address) const
Definition: interpreter_class.h:146
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
ieee_floatt
Definition: ieee_float.h:120
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
rotate_right
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
typet::subtype
const typet & subtype() const
Definition: type.h:47
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:217
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1080
ssa_exprt::get_original_name
const irep_idt get_original_name() const
Definition: ssa_expr.h:49
fixedbvt::from_integer
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
interpretert::allocate
void allocate(const mp_integer &address, const mp_integer &size)
reserves memory block of size at address
Definition: interpreter_evaluate.cpp:80
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
interpretert::memory
memoryt memory
Definition: interpreter_class.h:189
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
sparse_vectort::size
uint64_t size() const
Definition: sparse_vector.h:43
ieee_floatt::unpack
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:315
fixedbv.h
interpretert::address_to_symbol
symbol_exprt address_to_symbol(const mp_integer &address) const
Definition: interpreter_class.h:125
string_container.h
Container for C-Strings.
interpretert::memory_cellt::initializedt::READ_BEFORE_WRITTEN
@ READ_BEFORE_WRITTEN
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1412
interpretert::unbounded_size
bool unbounded_size(const typet &)
Definition: interpreter.cpp:958
interpretert::memory_cellt::value
mp_integer value
Definition: interpreter_class.h:168
exprt
Base class for all expressions.
Definition: expr.h:53
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
messaget::eom
static eomt eom
Definition: message.h:297
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
interpretert::call_stack
call_stackt call_stack
Definition: interpreter_class.h:263
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1931
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bitwise_and
mp_integer bitwise_and(const mp_integer &a, const mp_integer &b)
bitwise 'and' of two nonnegative integers
Definition: mp_arith.cpp:230
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:965
interpretert::build_memory_map
void build_memory_map()
Creates a memory map of all static symbols in the program.
Definition: interpreter.cpp:860
interpretert::count_type_leaves
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.
Definition: interpreter_evaluate.cpp:113
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2543
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
interpreter_class.h
Interpreter for GOTO Programs.
interpretert::memory_cellt
Definition: interpreter_class.h:162
interpretert::function
goto_functionst::function_mapt::const_iterator function
Definition: interpreter_class.h:267
byte_operators.h
Expression classes for byte-level operators.
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:128
messaget::result
mstreamt & result() const
Definition: message.h:409
messaget::error
mstreamt & error() const
Definition: message.h:399
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1362
integer2bvrep
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...
Definition: arith_tools.cpp:379
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1248
interpretert::get_size
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
Definition: interpreter.cpp:981
interpretert::get_value
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
Definition: interpreter.cpp:469
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
language_util.h
logic_right_shift
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
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
interpretert::num_dynamic_objects
int num_dynamic_objects
Definition: interpreter_class.h:278
interpretert::memory_cellt::initialized
initializedt initialized
Definition: interpreter_class.h:177
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:408
interpretert::read_unbounded
void read_unbounded(const mp_integer &address, mp_vectort &dest) const
Definition: interpreter_evaluate.cpp:50
ieee_floatt::pack
mp_integer pack() const
Definition: ieee_float.cpp:370
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
interpretert::mp_vectort
std::vector< mp_integer > mp_vectort
Definition: interpreter_class.h:59
fixedbvt::set_value
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
arith_right_shift
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
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:511
fixedbv_spect
Definition: fixedbv.h:20
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3112
interpretert::show
bool show
Definition: interpreter_class.h:271
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1897
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
interpretert::evaluate
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
Definition: interpreter_evaluate.cpp:313
interpretert::ns
const namespacet ns
Definition: interpreter_class.h:104
arith_left_shift
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
expr_util.h
Deprecated expression utility functions.
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
bitwise_xor
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
Definition: mp_arith.cpp:242
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
fixedbvt::from_expr
void from_expr(const constant_exprt &expr)
Definition: fixedbv.cpp:26
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
pointer_offset_size
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.
Definition: pointer_offset_size.cpp:89
interpretert::memory_offset_to_byte_offset
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-...
Definition: interpreter_evaluate.cpp:238
interpretert::memory_cellt::initializedt::UNKNOWN
@ UNKNOWN
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2868
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
ieee_float.h
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1298
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
interpretert::clear_input_flags
void clear_input_flags()
Clears memoy r/w flag initialization.
Definition: interpreter_evaluate.cpp:97
fixedbvt::spec
fixedbv_spect spec
Definition: fixedbv.h:44
interpretert::read
void read(const mp_integer &address, mp_vectort &dest) const
Reads a memory address and loads it into the dest variable.
Definition: interpreter_evaluate.cpp:26
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
interpretert::memory_cellt::initializedt::WRITTEN_BEFORE_READ
@ WRITTEN_BEFORE_READ
to_bitnot_expr
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: std_expr.h:2368
fixedbvt
Definition: fixedbv.h:42
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
interpretert::address_to_offset
mp_integer address_to_offset(const mp_integer &address) const
Definition: interpreter_class.h:130
exprt::operands
operandst & operands()
Definition: expr.h:95
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
messaget::warning
mstreamt & warning() const
Definition: message.h:404
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:23
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
interpretert::byte_offset_to_memory_offset
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',...
Definition: interpreter_evaluate.cpp:156
fixedbvt::get_value
const mp_integer & get_value() const
Definition: fixedbv.h:95
to_shl_expr
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: std_expr.h:2580
interpretert::memory_map
memory_mapt memory_map
Definition: interpreter_class.h:110
bitwise_or
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
Definition: mp_arith.cpp:218
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
rotate_left
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
ieee_floatt::from_expr
void from_expr(const constant_exprt &expr)
Definition: ieee_float.cpp:1063
interpretert::evaluate_address
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
Definition: interpreter_evaluate.cpp:1055
get_string_container
string_containert & get_string_container()
Get a reference to the global string container.
Definition: string_container.h:93
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939