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