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