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