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