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/fixedbv.h>
15 #include <util/ieee_float.h>
17 #include <util/string_container.h>
18 
19 #include <langapi/language_util.h>
20 
24  const mp_integer &address,
25  mp_vectort &dest) const
26 {
27  // copy memory region
28  for(std::size_t i=0; i<dest.size(); ++i)
29  {
30  mp_integer value;
31 
32  if((address+i)<memory.size())
33  {
34  const memory_cellt &cell=memory[integer2ulong(address+i)];
35  value=cell.value;
38  }
39  else
40  value=0;
41 
42  dest[i]=value;
43  }
44 }
45 
47  const mp_integer &address,
48  mp_vectort &dest) const
49 {
50  // copy memory region
51  std::size_t address_val=integer2size_t(address);
52  const mp_integer offset=address_to_offset(address_val);
53  const mp_integer alloc_size=
54  base_address_to_actual_size(address_val-offset);
55  const mp_integer to_read=alloc_size-offset;
56  for(size_t i=0; i<to_read; i++)
57  {
58  mp_integer value;
59 
60  if((address+i)<memory.size())
61  {
62  const memory_cellt &cell=memory[integer2size_t(address+i)];
63  value=cell.value;
66  }
67  else
68  value=0;
69 
70  dest.push_back(value);
71  }
72 }
73 
76  const mp_integer &address,
77  const mp_integer &size)
78 {
79  // clear memory region
80  for(mp_integer i=0; i<size; ++i)
81  {
82  if((address+i)<memory.size())
83  {
84  memory_cellt &cell=memory[integer2ulong(address+i)];
85  cell.value=0;
87  }
88  }
89 }
90 
93 {
94  for(auto &cell : memory)
95  {
96  if(cell.second.initialized==
98  cell.second.initialized=memory_cellt::initializedt::UNKNOWN;
99  }
100 }
101 
109 {
110  if(ty.id()==ID_struct)
111  {
112  result=0;
113  mp_integer subtype_count;
114  for(const auto &component : to_struct_type(ty).components())
115  {
116  if(count_type_leaves(component.type(), subtype_count))
117  return true;
118  result+=subtype_count;
119  }
120  return false;
121  }
122  else if(ty.id()==ID_array)
123  {
124  const auto &at=to_array_type(ty);
125  mp_vectort array_size_vec;
126  evaluate(at.size(), array_size_vec);
127  if(array_size_vec.size()!=1)
128  return true;
129  mp_integer subtype_count;
130  if(count_type_leaves(at.subtype(), subtype_count))
131  return true;
132  result=array_size_vec[0]*subtype_count;
133  return false;
134  }
135  else
136  {
137  result=1;
138  return false;
139  }
140 }
141 
152  const typet &source_type,
153  const mp_integer &offset,
154  mp_integer &result)
155 {
156  if(source_type.id()==ID_struct)
157  {
158  const auto &st=to_struct_type(source_type);
159  mp_integer previous_member_offsets=0;
160 
161  for(const auto &comp : st.components())
162  {
163  const mp_integer comp_offset = member_offset(st, comp.get_name(), ns);
164 
165  const mp_integer component_byte_size =
166  pointer_offset_size(comp.type(), ns);
167  if(component_byte_size<0)
168  return true;
169 
170  if(comp_offset + component_byte_size > offset)
171  {
172  mp_integer subtype_result;
174  comp.type(), offset - comp_offset, subtype_result);
175  result=previous_member_offsets+subtype_result;
176  return ret;
177  }
178  else
179  {
180  mp_integer component_count;
181  if(count_type_leaves(comp.type(), component_count))
182  return true;
183  previous_member_offsets+=component_count;
184  }
185  }
186  // Ran out of struct members, or struct contained a variable-length field.
187  return true;
188  }
189  else if(source_type.id()==ID_array)
190  {
191  const auto &at=to_array_type(source_type);
192  mp_vectort array_size_vec;
193  evaluate(at.size(), array_size_vec);
194  if(array_size_vec.size()!=1)
195  return true;
196  mp_integer array_size=array_size_vec[0];
197  mp_integer elem_size_bytes=pointer_offset_size(at.subtype(), ns);
198  if(elem_size_bytes<=0)
199  return true;
200  mp_integer elem_size_leaves;
201  if(count_type_leaves(at.subtype(), elem_size_leaves))
202  return true;
203  mp_integer this_idx=offset/elem_size_bytes;
204  if(this_idx>=array_size_vec[0])
205  return true;
206  mp_integer subtype_result;
208  at.subtype(),
209  offset%elem_size_bytes,
210  subtype_result);
211  result=subtype_result+(elem_size_leaves*this_idx);
212  return ret;
213  }
214  else
215  {
216  result=0;
217  // Can't currently subdivide a primitive.
218  return offset!=0;
219  }
220 }
221 
229  const typet &source_type,
230  const mp_integer &full_cell_offset,
231  mp_integer &result)
232 {
233  if(source_type.id()==ID_struct)
234  {
235  const auto &st=to_struct_type(source_type);
236  mp_integer cell_offset=full_cell_offset;
237 
238  for(const auto &comp : st.components())
239  {
240  mp_integer component_count;
241  if(count_type_leaves(comp.type(), component_count))
242  return true;
243  if(component_count>cell_offset)
244  {
245  mp_integer subtype_result;
247  comp.type(), cell_offset, subtype_result);
248  result = member_offset(st, comp.get_name(), ns) + subtype_result;
249  return ret;
250  }
251  else
252  {
253  cell_offset-=component_count;
254  }
255  }
256  // Ran out of members, or member of indefinite size
257  return true;
258  }
259  else if(source_type.id()==ID_array)
260  {
261  const auto &at=to_array_type(source_type);
262  mp_vectort array_size_vec;
263  evaluate(at.size(), array_size_vec);
264  if(array_size_vec.size()!=1)
265  return true;
266  mp_integer elem_size=pointer_offset_size(at.subtype(), ns);
267  if(elem_size==-1)
268  return true;
269  mp_integer elem_count;
270  if(count_type_leaves(at.subtype(), elem_count))
271  return true;
272  mp_integer this_idx=full_cell_offset/elem_count;
273  if(this_idx>=array_size_vec[0])
274  return true;
275  mp_integer subtype_result;
276  bool ret=
278  at.subtype(),
279  full_cell_offset%elem_count,
280  subtype_result);
281  result=subtype_result+(elem_size*this_idx);
282  return ret;
283  }
284  else
285  {
286  // Primitive type.
287  result=0;
288  return full_cell_offset!=0;
289  }
290 }
291 
296  const exprt &expr,
297  mp_vectort &dest)
298 {
299  if(expr.id()==ID_constant)
300  {
301  if(expr.type().id()==ID_struct)
302  {
303  dest.reserve(integer2size_t(get_size(expr.type())));
304  bool error=false;
305 
306  forall_operands(it, expr)
307  {
308  if(it->type().id()==ID_code)
309  continue;
310 
311  mp_integer sub_size=get_size(it->type());
312  if(sub_size==0)
313  continue;
314 
315  mp_vectort tmp;
316  evaluate(*it, tmp);
317 
318  if(tmp.size()==sub_size)
319  {
320  for(std::size_t i=0; i<tmp.size(); ++i)
321  dest.push_back(tmp[i]);
322  }
323  else
324  error=true;
325  }
326 
327  if(!error)
328  return;
329 
330  dest.clear();
331  }
332  else if((expr.type().id()==ID_pointer)
333  || (expr.type().id()==ID_address_of))
334  {
335  mp_integer i=0;
336  if(expr.has_operands() && expr.op0().id()==ID_address_of)
337  {
338  evaluate(expr.op0(), dest);
339  return;
340  }
341  if(expr.has_operands() && !to_integer(expr.op0(), i))
342  {
343  dest.push_back(i);
344  return;
345  }
346  }
347  else if(expr.type().id()==ID_floatbv)
348  {
349  ieee_floatt f;
350  f.from_expr(to_constant_expr(expr));
351  dest.push_back(f.pack());
352  return;
353  }
354  else if(expr.type().id()==ID_fixedbv)
355  {
356  fixedbvt f;
357  f.from_expr(to_constant_expr(expr));
358  dest.push_back(f.get_value());
359  return;
360  }
361  else if(expr.type().id()==ID_c_bool)
362  {
363  const irep_idt &value=to_constant_expr(expr).get_value();
364  dest.push_back(binary2integer(id2string(value), false));
365  return;
366  }
367  else if(expr.type().id()==ID_bool)
368  {
369  dest.push_back(expr.is_true());
370  return;
371  }
372  else if(expr.type().id()==ID_string)
373  {
374  const std::string &value = id2string(to_constant_expr(expr).get_value());
375  if(show)
376  warning() << "string decoding not fully implemented "
377  << value.size() + 1 << eom;
378  dest.push_back(get_string_container()[value]);
379  return;
380  }
381  else
382  {
383  mp_integer i;
384  if(!to_integer(expr, i))
385  {
386  dest.push_back(i);
387  return;
388  }
389  }
390  }
391  else if(expr.id()==ID_struct)
392  {
393  if(!unbounded_size(expr.type()))
394  dest.reserve(integer2size_t(get_size(expr.type())));
395 
396  bool error=false;
397 
398  forall_operands(it, expr)
399  {
400  if(it->type().id()==ID_code)
401  continue;
402 
403  mp_integer sub_size=get_size(it->type());
404  if(sub_size==0)
405  continue;
406 
407  mp_vectort tmp;
408  evaluate(*it, tmp);
409 
410  if(unbounded_size(it->type()) || tmp.size()==sub_size)
411  {
412  for(std::size_t i=0; i<tmp.size(); i++)
413  dest.push_back(tmp[i]);
414  }
415  else
416  error=true;
417  }
418 
419  if(!error)
420  return;
421 
422  dest.clear();
423  }
424  else if(expr.id()==ID_side_effect)
425  {
426  side_effect_exprt side_effect=to_side_effect_expr(expr);
427  if(side_effect.get_statement()==ID_nondet)
428  {
429  if(show)
430  error() << "nondet not implemented" << eom;
431  return;
432  }
433  else if(side_effect.get_statement()==ID_allocate)
434  {
435  if(show)
436  error() << "heap memory allocation not fully implemented "
437  << expr.type().subtype().pretty()
438  << eom;
439  std::stringstream buffer;
441  buffer << "interpreter::dynamic_object" << num_dynamic_objects;
442  irep_idt id(buffer.str().c_str());
443  mp_integer address=build_memory_map(id, expr.type().subtype());
444  // TODO: check array of type
445  // TODO: interpret zero-initialization argument
446  dest.push_back(address);
447  return;
448  }
449  if(show)
450  error() << "side effect not implemented "
451  << side_effect.get_statement()
452  << eom;
453  }
454  else if(expr.id()==ID_bitor)
455  {
456  if(expr.operands().size()<2)
457  throw id2string(expr.id())+" expects at least two operands";
458 
459  mp_integer final=0;
460  forall_operands(it, expr)
461  {
462  mp_vectort tmp;
463  evaluate(*it, tmp);
464  if(tmp.size()==1)
465  final=bitwise_or(final, tmp.front());
466  }
467  dest.push_back(final);
468  return;
469  }
470  else if(expr.id()==ID_bitand)
471  {
472  if(expr.operands().size()<2)
473  throw id2string(expr.id())+" expects at least two operands";
474 
475  mp_integer final=-1;
476  forall_operands(it, expr)
477  {
478  mp_vectort tmp;
479  evaluate(*it, tmp);
480  if(tmp.size()==1)
481  final=bitwise_and(final, tmp.front());
482  }
483  dest.push_back(final);
484  return;
485  }
486  else if(expr.id()==ID_bitxor)
487  {
488  if(expr.operands().size()<2)
489  throw id2string(expr.id())+" expects at least two operands";
490 
491  mp_integer final=0;
492  forall_operands(it, expr)
493  {
494  mp_vectort tmp;
495  evaluate(*it, tmp);
496  if(tmp.size()==1)
497  final=bitwise_xor(final, tmp.front());
498  }
499  dest.push_back(final);
500  return;
501  }
502  else if(expr.id()==ID_bitnot)
503  {
504  if(expr.operands().size()!=1)
505  throw id2string(expr.id())+" expects one operand";
506  mp_vectort tmp;
507  evaluate(expr.op0(), tmp);
508  if(tmp.size()==1)
509  {
510  dest.push_back(bitwise_neg(tmp.front()));
511  return;
512  }
513  }
514  else if(expr.id()==ID_shl)
515  {
516  if(expr.operands().size()!=2)
517  throw id2string(expr.id())+" expects two operands";
518 
519  mp_vectort tmp0, tmp1;
520  evaluate(expr.op0(), tmp0);
521  evaluate(expr.op1(), tmp1);
522  if(tmp0.size()==1 && tmp1.size()==1)
523  {
525  tmp0.front(),
526  tmp1.front(),
527  to_bitvector_type(expr.op0().type()).get_width());
528  dest.push_back(final);
529  return;
530  }
531  }
532  else if((expr.id()==ID_shr) || (expr.id()==ID_lshr))
533  {
534  if(expr.operands().size()!=2)
535  throw id2string(expr.id())+" expects two operands";
536 
537  mp_vectort tmp0, tmp1;
538  evaluate(expr.op0(), tmp0);
539  evaluate(expr.op1(), tmp1);
540  if(tmp0.size()==1 && tmp1.size()==1)
541  {
543  tmp0.front(),
544  tmp1.front(),
545  to_bitvector_type(expr.op0().type()).get_width());
546  dest.push_back(final);
547  return;
548  }
549  }
550  else if(expr.id()==ID_ashr)
551  {
552  if(expr.operands().size()!=2)
553  throw id2string(expr.id())+" expects two operands";
554 
555  mp_vectort tmp0, tmp1;
556  evaluate(expr.op0(), tmp0);
557  evaluate(expr.op1(), tmp1);
558  if(tmp0.size()==1 && tmp1.size()==1)
559  {
561  tmp0.front(),
562  tmp1.front(),
563  to_bitvector_type(expr.op0().type()).get_width());
564  dest.push_back(final);
565  return;
566  }
567  }
568  else if(expr.id()==ID_ror)
569  {
570  if(expr.operands().size()!=2)
571  throw id2string(expr.id())+" expects two operands";
572 
573  mp_vectort tmp0, tmp1;
574  evaluate(expr.op0(), tmp0);
575  evaluate(expr.op1(), tmp1);
576  if(tmp0.size()==1 && tmp1.size()==1)
577  {
578  mp_integer final=rotate_right(tmp0.front(),
579  tmp1.front(),
580  to_bitvector_type(expr.op0().type()).get_width());
581  dest.push_back(final);
582  return;
583  }
584  }
585  else if(expr.id()==ID_rol)
586  {
587  if(expr.operands().size()!=2)
588  throw id2string(expr.id())+" expects two operands";
589 
590  mp_vectort tmp0, tmp1;
591  evaluate(expr.op0(), tmp0);
592  evaluate(expr.op1(), tmp1);
593  if(tmp0.size()==1 && tmp1.size()==1)
594  {
595  mp_integer final=rotate_left(tmp0.front(),
596  tmp1.front(),
597  to_bitvector_type(expr.op0().type()).get_width());
598  dest.push_back(final);
599  return;
600  }
601  }
602  else if(expr.id()==ID_equal ||
603  expr.id()==ID_notequal ||
604  expr.id()==ID_le ||
605  expr.id()==ID_ge ||
606  expr.id()==ID_lt ||
607  expr.id()==ID_gt)
608  {
609  if(expr.operands().size()!=2)
610  throw id2string(expr.id())+" expects two operands";
611 
612  mp_vectort tmp0, tmp1;
613  evaluate(expr.op0(), tmp0);
614  evaluate(expr.op1(), tmp1);
615 
616  if(tmp0.size()==1 && tmp1.size()==1)
617  {
618  const mp_integer &op0=tmp0.front();
619  const mp_integer &op1=tmp1.front();
620 
621  if(expr.id()==ID_equal)
622  dest.push_back(op0==op1);
623  else if(expr.id()==ID_notequal)
624  dest.push_back(op0!=op1);
625  else if(expr.id()==ID_le)
626  dest.push_back(op0<=op1);
627  else if(expr.id()==ID_ge)
628  dest.push_back(op0>=op1);
629  else if(expr.id()==ID_lt)
630  dest.push_back(op0<op1);
631  else if(expr.id()==ID_gt)
632  dest.push_back(op0>op1);
633  }
634 
635  return;
636  }
637  else if(expr.id()==ID_or)
638  {
639  if(expr.operands().empty())
640  throw id2string(expr.id())+" expects at least one operand";
641 
642  bool result=false;
643 
644  forall_operands(it, expr)
645  {
646  mp_vectort tmp;
647  evaluate(*it, tmp);
648 
649  if(tmp.size()==1 && tmp.front()!=0)
650  {
651  result=true;
652  break;
653  }
654  }
655 
656  dest.push_back(result);
657 
658  return;
659  }
660  else if(expr.id()==ID_if)
661  {
662  if(expr.operands().size()!=3)
663  throw "if expects three operands";
664 
665  mp_vectort tmp0, tmp1;
666  evaluate(expr.op0(), tmp0);
667 
668  if(tmp0.size()==1)
669  {
670  if(tmp0.front()!=0)
671  evaluate(expr.op1(), tmp1);
672  else
673  evaluate(expr.op2(), tmp1);
674  }
675 
676  if(tmp1.size()==1)
677  dest.push_back(tmp1.front());
678 
679  return;
680  }
681  else if(expr.id()==ID_and)
682  {
683  if(expr.operands().empty())
684  throw id2string(expr.id())+" expects at least one operand";
685 
686  bool result=true;
687 
688  forall_operands(it, expr)
689  {
690  mp_vectort tmp;
691  evaluate(*it, tmp);
692 
693  if(tmp.size()==1 && tmp.front()==0)
694  {
695  result=false;
696  break;
697  }
698  }
699 
700  dest.push_back(result);
701 
702  return;
703  }
704  else if(expr.id()==ID_not)
705  {
706  if(expr.operands().size()!=1)
707  throw id2string(expr.id())+" expects one operand";
708 
709  mp_vectort tmp;
710  evaluate(expr.op0(), tmp);
711 
712  if(tmp.size()==1)
713  dest.push_back(tmp.front()==0);
714 
715  return;
716  }
717  else if(expr.id()==ID_plus)
718  {
719  mp_integer result=0;
720 
721  forall_operands(it, expr)
722  {
723  mp_vectort tmp;
724  evaluate(*it, tmp);
725  if(tmp.size()==1)
726  result+=tmp.front();
727  }
728 
729  dest.push_back(result);
730  return;
731  }
732  else if(expr.id()==ID_mult)
733  {
734  // type-dependent!
736 
737  if(expr.type().id()==ID_fixedbv)
738  {
739  fixedbvt f;
741  f.from_integer(1);
742  result=f.get_value();
743  }
744  else if(expr.type().id()==ID_floatbv)
745  {
746  ieee_floatt f(to_floatbv_type(expr.type()));
747  f.from_integer(1);
748  result=f.pack();
749  }
750  else
751  result=1;
752 
753  forall_operands(it, expr)
754  {
755  mp_vectort tmp;
756  evaluate(*it, tmp);
757  if(tmp.size()==1)
758  {
759  if(expr.type().id()==ID_fixedbv)
760  {
761  fixedbvt f1, f2;
763  f2.spec=fixedbv_spect(to_fixedbv_type(it->type()));
764  f1.set_value(result);
765  f2.set_value(tmp.front());
766  f1*=f2;
767  result=f1.get_value();
768  }
769  else if(expr.type().id()==ID_floatbv)
770  {
771  ieee_floatt f1(to_floatbv_type(expr.type()));
772  ieee_floatt f2(to_floatbv_type(it->type()));
773  f1.unpack(result);
774  f2.unpack(tmp.front());
775  f1*=f2;
776  result=f2.pack();
777  }
778  else
779  result*=tmp.front();
780  }
781  }
782 
783  dest.push_back(result);
784  return;
785  }
786  else if(expr.id()==ID_minus)
787  {
788  if(expr.operands().size()!=2)
789  throw "- expects two operands";
790 
791  mp_vectort tmp0, tmp1;
792  evaluate(expr.op0(), tmp0);
793  evaluate(expr.op1(), tmp1);
794 
795  if(tmp0.size()==1 && tmp1.size()==1)
796  dest.push_back(tmp0.front()-tmp1.front());
797  return;
798  }
799  else if(expr.id()==ID_div)
800  {
801  if(expr.operands().size()!=2)
802  throw "/ expects two operands";
803 
804  mp_vectort tmp0, tmp1;
805  evaluate(expr.op0(), tmp0);
806  evaluate(expr.op1(), tmp1);
807 
808  if(tmp0.size()==1 && tmp1.size()==1)
809  dest.push_back(tmp0.front()/tmp1.front());
810  return;
811  }
812  else if(expr.id()==ID_unary_minus)
813  {
814  if(expr.operands().size()!=1)
815  throw "unary- expects one operand";
816 
817  mp_vectort tmp0;
818  evaluate(expr.op0(), tmp0);
819 
820  if(tmp0.size()==1)
821  dest.push_back(-tmp0.front());
822  return;
823  }
824  else if(expr.id()==ID_address_of)
825  {
826  if(expr.operands().size()!=1)
827  throw "address_of expects one operand";
828 
829  dest.push_back(evaluate_address(expr.op0()));
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  if(expr.op0().type().id()!=ID_pointer)
837  throw "pointer_offset expects a pointer operand";
839  evaluate(expr.op0(), result);
840  if(result.size()==1)
841  {
842  // Return the distance, in bytes, between the address returned
843  // and the beginning of the underlying object.
844  mp_integer address=result[0];
845  if(address>0 && address<memory.size())
846  {
847  auto obj_type=get_type(address_to_identifier(address));
848 
849  mp_integer offset=address_to_offset(address);
850  mp_integer byte_offset;
851  if(!memory_offset_to_byte_offset(obj_type, offset, byte_offset))
852  dest.push_back(byte_offset);
853  }
854  }
855  return;
856  }
857  else if(expr.id()==ID_byte_extract_little_endian ||
858  expr.id()==ID_byte_extract_big_endian)
859  {
860  if(expr.operands().size()!=2)
861  throw "byte_extract should have two operands";
862  mp_vectort extract_offset;
863  evaluate(expr.op1(), extract_offset);
864  mp_vectort extract_from;
865  evaluate(expr.op0(), extract_from);
866  if(extract_offset.size()==1 && extract_from.size()!=0)
867  {
868  const typet &target_type=expr.type();
869  mp_integer memory_offset;
870  // If memory offset is found (which should normally be the case)
871  // extract the corresponding data from the appropriate memory location
873  expr.op0().type(),
874  extract_offset[0],
875  memory_offset))
876  {
877  mp_integer target_type_leaves;
878  if(!count_type_leaves(target_type, target_type_leaves) &&
879  target_type_leaves>0)
880  {
881  dest.insert(dest.end(),
882  extract_from.begin()+memory_offset.to_long(),
883  extract_from.begin()+(memory_offset+target_type_leaves).to_long());
884  return;
885  }
886  }
887  }
888  }
889  else if(expr.id()==ID_dereference ||
890  expr.id()==ID_index ||
891  expr.id()==ID_symbol ||
892  expr.id()==ID_member)
893  {
895  expr,
896  true); // fail quietly
897  if(address.is_zero() && expr.id()==ID_index)
898  {
899  // Try reading from a constant array:
900  mp_vectort idx;
901  evaluate(expr.op1(), idx);
902  if(idx.size()==1)
903  {
904  mp_integer read_from_index=idx[0];
905  if(expr.op0().id()==ID_array)
906  {
907  const auto &ops=expr.op0().operands();
908  DATA_INVARIANT(read_from_index.is_long(), "index is too large");
909  if(read_from_index>=0 && read_from_index<ops.size())
910  {
911  evaluate(ops[read_from_index.to_long()], dest);
912  if(dest.size()!=0)
913  return;
914  }
915  }
916  else if(expr.op0().id() == ID_array_list)
917  {
918  // This sort of construct comes from boolbv_get, but doesn't seem
919  // to have an exprt yet. Its operands are a list of key-value pairs.
920  const auto &ops=expr.op0().operands();
922  ops.size()%2==0,
923  "array-list has odd number of operands");
924  for(size_t listidx=0; listidx!=ops.size(); listidx+=2)
925  {
926  mp_vectort elem_idx;
927  evaluate(ops[listidx], elem_idx);
928  CHECK_RETURN(elem_idx.size()==1);
929  if(elem_idx[0]==read_from_index)
930  {
931  evaluate(ops[listidx+1], dest);
932  if(dest.size()!=0)
933  return;
934  else
935  break;
936  }
937  }
938  // If we fall out the end of this loop then the constant array-list
939  // didn't define an element matching the index we're looking for.
940  }
941  }
942  evaluate_address(expr); // Evaluate again to print error message.
943  }
944  else if(!address.is_zero())
945  {
946  if(!unbounded_size(expr.type()))
947  {
948  dest.resize(integer2size_t(get_size(expr.type())));
949  read(address, dest);
950  }
951  else
952  {
953  read_unbounded(address, dest);
954  }
955  return;
956  }
957  }
958  else if(expr.id()==ID_typecast)
959  {
960  if(expr.operands().size()!=1)
961  throw "typecast expects one operand";
962 
963  mp_vectort tmp;
964  evaluate(expr.op0(), tmp);
965 
966  if(tmp.size()==1)
967  {
968  const mp_integer &value=tmp.front();
969 
970  if(expr.type().id()==ID_pointer)
971  {
972  dest.push_back(value);
973  return;
974  }
975  else if(expr.type().id()==ID_signedbv)
976  {
977  const std::string s=
978  integer2binary(value, to_signedbv_type(expr.type()).get_width());
979  dest.push_back(binary2integer(s, true));
980  return;
981  }
982  else if(expr.type().id()==ID_unsignedbv)
983  {
984  const std::string s=
985  integer2binary(value, to_unsignedbv_type(expr.type()).get_width());
986  dest.push_back(binary2integer(s, false));
987  return;
988  }
989  else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))
990  {
991  dest.push_back(value!=0);
992  return;
993  }
994  }
995  }
996  else if(expr.id()==ID_array)
997  {
998  forall_operands(it, expr)
999  {
1000  evaluate(*it, dest);
1001  }
1002  return;
1003  }
1004  else if(expr.id()==ID_array_of)
1005  {
1006  const auto &ty=to_array_type(expr.type());
1007  std::vector<mp_integer> size;
1008  if(ty.size().id()==ID_infinity)
1009  size.push_back(0);
1010  else
1011  evaluate(ty.size(), size);
1012 
1013  if(size.size()==1)
1014  {
1015  std::size_t size_int=integer2size_t(size[0]);
1016  for(std::size_t i=0; i<size_int; ++i)
1017  evaluate(expr.op0(), dest);
1018  return;
1019  }
1020  }
1021  else if(expr.id()==ID_with)
1022  {
1023  const auto &wexpr=to_with_expr(expr);
1024  evaluate(wexpr.old(), dest);
1025  std::vector<mp_integer> where;
1026  std::vector<mp_integer> new_value;
1027  evaluate(wexpr.where(), where);
1028  evaluate(wexpr.new_value(), new_value);
1029  const auto &subtype=expr.type().subtype();
1030  if(!new_value.empty() && where.size()==1 && !unbounded_size(subtype))
1031  {
1032  // Ignore indices < 0, which the string solver sometimes produces
1033  if(where[0]<0)
1034  return;
1035 
1036  mp_integer where_idx=where[0];
1037  mp_integer subtype_size=get_size(subtype);
1038  mp_integer need_size=(where_idx+1)*subtype_size;
1039 
1040  if(dest.size()<need_size)
1041  dest.resize(integer2size_t(need_size), 0);
1042 
1043  for(std::size_t i=0; i<new_value.size(); ++i)
1044  dest[integer2size_t((where_idx*subtype_size)+i)]=new_value[i];
1045 
1046  return;
1047  }
1048  }
1049  else if(expr.id()==ID_nil)
1050  {
1051  dest.push_back(0);
1052  return;
1053  }
1054  else if(expr.id()==ID_infinity)
1055  {
1056  if(expr.type().id()==ID_signedbv)
1057  {
1058  warning() << "Infinite size arrays not supported" << eom;
1059  return;
1060  }
1061  }
1062  error() << "!! failed to evaluate expression: "
1063  << from_expr(ns, function->first, expr) << "\n"
1064  << expr.id() << "[" << expr.type().id() << "]"
1065  << eom;
1066 }
1067 
1069  const exprt &expr,
1070  bool fail_quietly)
1071 {
1072  if(expr.id()==ID_symbol)
1073  {
1074  const irep_idt &identifier = is_ssa_expr(expr)
1075  ? to_ssa_expr(expr).get_original_name()
1076  : to_symbol_expr(expr).get_identifier();
1077 
1078  interpretert::memory_mapt::const_iterator m_it1=
1079  memory_map.find(identifier);
1080 
1081  if(m_it1!=memory_map.end())
1082  return m_it1->second;
1083 
1084  if(!call_stack.empty())
1085  {
1086  interpretert::memory_mapt::const_iterator m_it2=
1087  call_stack.top().local_map.find(identifier);
1088 
1089  if(m_it2!=call_stack.top().local_map.end())
1090  return m_it2->second;
1091  }
1092  mp_integer address=memory.size();
1093  build_memory_map(to_symbol_expr(expr).get_identifier(), expr.type());
1094  return address;
1095  }
1096  else if(expr.id()==ID_dereference)
1097  {
1098  if(expr.operands().size()!=1)
1099  throw "dereference expects one operand";
1100 
1101  mp_vectort tmp0;
1102  evaluate(expr.op0(), tmp0);
1103 
1104  if(tmp0.size()==1)
1105  return tmp0.front();
1106  }
1107  else if(expr.id()==ID_index)
1108  {
1109  if(expr.operands().size()!=2)
1110  throw "index expects two operands";
1111 
1112  mp_vectort tmp1;
1113  evaluate(expr.op1(), tmp1);
1114 
1115  if(tmp1.size()==1)
1116  {
1117  auto base=evaluate_address(expr.op0(), fail_quietly);
1118  if(!base.is_zero())
1119  return base+tmp1.front();
1120  }
1121  }
1122  else if(expr.id()==ID_member)
1123  {
1124  if(expr.operands().size()!=1)
1125  throw "member expects one operand";
1126 
1127  const struct_typet &struct_type=
1128  to_struct_type(ns.follow(expr.op0().type()));
1129 
1130  const irep_idt &component_name=
1132 
1133  mp_integer offset=0;
1134 
1135  for(const auto &comp : struct_type.components())
1136  {
1137  if(comp.get_name()==component_name)
1138  break;
1139 
1140  offset+=get_size(comp.type());
1141  }
1142 
1143  auto base=evaluate_address(expr.op0(), fail_quietly);
1144  if(!base.is_zero())
1145  return base+offset;
1146  }
1147  else if(expr.id()==ID_byte_extract_little_endian ||
1148  expr.id()==ID_byte_extract_big_endian)
1149  {
1150  if(expr.operands().size()!=2)
1151  throw "byte_extract should have two operands";
1152  mp_vectort extract_offset;
1153  evaluate(expr.op1(), extract_offset);
1154  mp_vectort extract_from;
1155  evaluate(expr.op0(), extract_from);
1156  if(extract_offset.size()==1 && !extract_from.empty())
1157  {
1158  mp_integer memory_offset;
1159  if(!byte_offset_to_memory_offset(expr.op0().type(),
1160  extract_offset[0], memory_offset))
1161  return evaluate_address(expr.op0(), fail_quietly)+memory_offset;
1162  }
1163  }
1164  else if(expr.id()==ID_if)
1165  {
1167  if_exprt address_cond(
1168  expr.op0(),
1169  address_of_exprt(expr.op1()),
1170  address_of_exprt(expr.op2()));
1171  evaluate(address_cond, result);
1172  if(result.size()==1)
1173  return result[0];
1174  }
1175  else if(expr.id()==ID_typecast)
1176  {
1177  if(expr.operands().size()!=1)
1178  throw "typecast expects one operand";
1179 
1180  return evaluate_address(expr.op0(), fail_quietly);
1181  }
1182  if(!fail_quietly)
1183  {
1184  error() << "!! failed to evaluate address: "
1185  << from_expr(ns, function->first, expr)
1186  << eom;
1187  }
1188 
1189  return 0;
1190 }
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 &#39;source_type&#39;, this yields the offset into that vector at which to find a value at byte address &#39;offset&#39;.
The type of an expression.
Definition: type.h:22
BigInt mp_integer
Definition: mp_arith.h:22
typet get_type(const irep_idt &id) const
returns the type object corresponding to id
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
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:356
irep_idt address_to_identifier(const mp_integer &address) const
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1287
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1150
string_containert & get_string_container()
Get a reference to the global string container.
mp_integer::ullong_t integer2ulong(const mp_integer &n)
Definition: mp_arith.cpp:189
void from_expr(const constant_exprt &expr)
std::vector< mp_integer > mp_vectort
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise xor bitwise operations only make sense on native objects, hence the largest object size shoul...
Definition: mp_arith.cpp:232
const irep_idt & get_identifier() const
Definition: std_expr.h:128
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_value() const
Definition: std_expr.h:4441
bool memory_offset_to_byte_offset(const typet &source_type, const mp_integer &cell_offset, mp_integer &result)
Similarly to the above, the interpreter&#39;s memory objects contain mp_integers that represent variable-...
void from_expr(const constant_exprt &expr)
Definition: fixedbv.cpp:26
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
const componentst & components() const
Definition: std_types.h:245
The trinary if-then-else operator.
Definition: std_expr.h:3361
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
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:252
Container for C-Strings.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1287
const mp_integer & get_value() const
Definition: fixedbv.h:95
mstreamt & warning() const
Definition: message.h:307
const irep_idt & id() const
Definition: irep.h:189
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
Interpreter for GOTO Programs.
fixedbv_spect spec
Definition: fixedbv.h:44
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:312
goto_functionst::function_mapt::const_iterator function
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
void read(const mp_integer &address, mp_vectort &dest) const
Reads a memory address and loads it into the dest variable.
void read_unbounded(const mp_integer &address, mp_vectort &dest) const
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
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, hence the largest object size should be the largest available c++ integer size (currently long long)
Definition: mp_arith.cpp:319
mp_integer bitwise_and(const mp_integer &a, const mp_integer &b)
bitwise and bitwise operations only make sense on native objects, hence the largest object size shoul...
Definition: mp_arith.cpp:222
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:273
mp_integer address_to_offset(const mp_integer &address) const
exprt & op1()
Definition: expr.h:75
mstreamt & error() const
Definition: message.h:302
mp_integer bitwise_neg(const mp_integer &a)
bitwise negation bitwise operations only make sense on native objects, hence the largest object size ...
Definition: mp_arith.cpp:242
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
const irep_idt get_original_name() const
Definition: ssa_expr.h:77
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:336
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
mp_integer base_address_to_actual_size(const mp_integer &address) const
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
const typet & follow(const typet &) const
Definition: namespace.cpp:55
void allocate(const mp_integer &address, const mp_integer &size)
reserves memory block of size at address
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise or bitwise operations only make sense on native objects, hence the largest object size should...
Definition: mp_arith.cpp:212
Operator to return the address of an object.
Definition: std_expr.h:3170
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
bool unbounded_size(const typet &)
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
bool has_operands() const
Definition: expr.h:63
Pointer Logic.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1245
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
Definition: std_expr.h:3519
void clear_input_flags()
Clears memoy r/w flag initialization.
const namespacet ns
mstreamt & result() const
Definition: message.h:312
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1373
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1334
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
mp_integer pack() const
Definition: ieee_float.cpp:367
void build_memory_map()
Creates a memory map of all static symbols in the program.
irep_idt get_component_name() const
Definition: std_expr.h:3895
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
memory_mapt memory_map
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:173
call_stackt call_stack
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:508
uint64_t size() const
Definition: sparse_vector.h:43
exprt & op2()
Definition: expr.h:78
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
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...
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
An expression containing a side effect.
Definition: std_code.h:1238
operandst & operands()
Definition: expr.h:66
const irep_idt & get_statement() const
Definition: std_code.h:1253