cprover
value_set.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "value_set.h"
13 
14 #include <cassert>
15 #include <ostream>
16 
17 #include <util/symbol_table.h>
18 #include <util/simplify_expr.h>
19 #include <util/base_type.h>
20 #include <util/std_expr.h>
21 #include <util/prefix.h>
22 #include <util/std_code.h>
23 #include <util/arith_tools.h>
25 #include <util/cprover_prefix.h>
26 
27 #include <util/c_types.h>
28 
29 #ifdef DEBUG
30 #include <langapi/language_util.h>
31 #include <iostream>
32 #endif
33 
34 #include "add_failed_symbols.h"
35 
38 
40  const irep_idt &id,
41  const typet &type,
42  const namespacet &ns)
43 {
44  // we always track fields on these
45  if(has_prefix(id2string(id), "value_set::dynamic_object") ||
46  id=="value_set::return_value" ||
47  id=="value_set::memory")
48  return true;
49 
50  // otherwise it has to be a struct
51  return ns.follow(type).id()==ID_struct;
52 }
53 
55  const entryt &e,
56  const typet &type,
57  const namespacet &ns)
58 {
59  irep_idt index;
60 
61  if(field_sensitive(e.identifier, type, ns))
62  index=id2string(e.identifier)+e.suffix;
63  else
64  index=e.identifier;
65 
66  std::pair<valuest::iterator, bool> r=
67  values.insert(std::pair<idt, entryt>(index, e));
68 
69  return r.first->second;
70 }
71 
73  object_mapt &dest,
74  unsigned n,
75  const objectt &object) const
76 {
77  object_map_dt::const_iterator entry=dest.read().find(n);
78 
79  if(entry==dest.read().end())
80  {
81  // new
82  dest.write()[n]=object;
83  return true;
84  }
85  else if(!entry->second.offset_is_set)
86  return false; // no change
87  else if(object.offset_is_set &&
88  entry->second.offset==object.offset)
89  return false; // no change
90  else
91  {
92  dest.write()[n].offset_is_set=false;
93  return true;
94  }
95 }
96 
98  const namespacet &ns,
99  std::ostream &out) const
100 {
101  for(valuest::const_iterator
102  v_it=values.begin();
103  v_it!=values.end();
104  v_it++)
105  {
106  irep_idt identifier, display_name;
107 
108  const entryt &e=v_it->second;
109 
110  if(has_prefix(id2string(e.identifier), "value_set::dynamic_object"))
111  {
112  display_name=id2string(e.identifier)+e.suffix;
113  identifier="";
114  }
115  else if(e.identifier=="value_set::return_value")
116  {
117  display_name="RETURN_VALUE"+e.suffix;
118  identifier="";
119  }
120  else
121  {
122  #if 0
123  const symbolt &symbol=ns.lookup(e.identifier);
124  display_name=symbol.display_name()+e.suffix;
125  identifier=symbol.name;
126  #else
127  identifier=id2string(e.identifier);
128  display_name=id2string(identifier)+e.suffix;
129  #endif
130  }
131 
132  out << display_name;
133 
134  out << " = { ";
135 
136  const object_map_dt &object_map=e.object_map.read();
137 
138  std::size_t width=0;
139 
140  for(object_map_dt::const_iterator
141  o_it=object_map.begin();
142  o_it!=object_map.end();
143  o_it++)
144  {
145  const exprt &o=object_numbering[o_it->first];
146 
147  std::string result;
148 
149  if(o.id()==ID_invalid || o.id()==ID_unknown)
150  result=from_expr(ns, identifier, o);
151  else
152  {
153  result="<"+from_expr(ns, identifier, o)+", ";
154 
155  if(o_it->second.offset_is_set)
156  result+=integer2string(o_it->second.offset)+"";
157  else
158  result+='*';
159 
160  if(o.type().is_nil())
161  result+=", ?";
162  else
163  result+=", "+from_type(ns, identifier, o.type());
164 
165  result+='>';
166  }
167 
168  out << result;
169 
170  width+=result.size();
171 
172  object_map_dt::const_iterator next(o_it);
173  next++;
174 
175  if(next!=object_map.end())
176  {
177  out << ", ";
178  if(width>=40)
179  out << "\n ";
180  }
181  }
182 
183  out << " } \n";
184  }
185 }
186 
187 exprt value_sett::to_expr(object_map_dt::const_iterator it) const
188 {
189  const exprt &object=object_numbering[it->first];
190 
191  if(object.id()==ID_invalid ||
192  object.id()==ID_unknown)
193  return object;
194 
196 
197  od.object()=object;
198 
199  if(it->second.offset_is_set)
200  od.offset()=from_integer(it->second.offset, index_type());
201 
202  od.type()=od.object().type();
203 
204  return od;
205 }
206 
208 {
209  bool result=false;
210 
211  valuest::iterator v_it=values.begin();
212 
213  for(valuest::const_iterator
214  it=new_values.begin();
215  it!=new_values.end();
216  ) // no it++
217  {
218  if(v_it==values.end() || it->first<v_it->first)
219  {
220  values.insert(v_it, *it);
221  result=true;
222  it++;
223  continue;
224  }
225  else if(v_it->first<it->first)
226  {
227  v_it++;
228  continue;
229  }
230 
231  assert(v_it->first==it->first);
232 
233  entryt &e=v_it->second;
234  const entryt &new_e=it->second;
235 
236  if(make_union(e.object_map, new_e.object_map))
237  result=true;
238 
239  v_it++;
240  it++;
241  }
242 
243  return result;
244 }
245 
246 bool value_sett::make_union(object_mapt &dest, const object_mapt &src) const
247 {
248  bool result=false;
249 
250  for(object_map_dt::const_iterator it=src.read().begin();
251  it!=src.read().end();
252  it++)
253  {
254  if(insert(dest, it))
255  result=true;
256  }
257 
258  return result;
259 }
260 
262  exprt &expr,
263  const namespacet &ns) const
264 {
265  bool mod=false;
266 
267  if(expr.id()==ID_pointer_offset)
268  {
269  assert(expr.operands().size()==1);
270 
271  object_mapt reference_set;
272  get_value_set(expr.op0(), reference_set, ns, true);
273 
274  exprt new_expr;
275  mp_integer previous_offset=0;
276 
277  const object_map_dt &object_map=reference_set.read();
278  for(object_map_dt::const_iterator
279  it=object_map.begin();
280  it!=object_map.end();
281  it++)
282  if(!it->second.offset_is_set)
283  return false;
284  else
285  {
286  const exprt &object=object_numbering[it->first];
287  mp_integer ptr_offset=compute_pointer_offset(object, ns);
288 
289  if(ptr_offset<0)
290  return false;
291 
292  ptr_offset+=it->second.offset;
293 
294  if(mod && ptr_offset!=previous_offset)
295  return false;
296 
297  new_expr=from_integer(ptr_offset, expr.type());
298  previous_offset=ptr_offset;
299  mod=true;
300  }
301 
302  if(mod)
303  expr.swap(new_expr);
304  }
305  else
306  {
307  Forall_operands(it, expr)
308  mod=eval_pointer_offset(*it, ns) || mod;
309  }
310 
311  return mod;
312 }
313 
315  const exprt &expr,
316  value_setst::valuest &dest,
317  const namespacet &ns) const
318 {
319  object_mapt object_map;
320  get_value_set(expr, object_map, ns, false);
321 
322  for(object_map_dt::const_iterator
323  it=object_map.read().begin();
324  it!=object_map.read().end();
325  it++)
326  dest.push_back(to_expr(it));
327 
328  #if 0
329  for(value_setst::valuest::const_iterator it=dest.begin();
330  it!=dest.end(); it++)
331  std::cout << "GET_VALUE_SET: " << from_expr(ns, "", *it) << '\n';
332  #endif
333 }
334 
336  const exprt &expr,
337  object_mapt &dest,
338  const namespacet &ns,
339  bool is_simplified) const
340 {
341  exprt tmp(expr);
342  if(!is_simplified)
343  simplify(tmp, ns);
344 
345  get_value_set_rec(tmp, dest, "", tmp.type(), ns);
346 }
347 
349  const exprt &expr,
350  object_mapt &dest,
351  const std::string &suffix,
352  const typet &original_type,
353  const namespacet &ns) const
354 {
355  #if 0
356  std::cout << "GET_VALUE_SET_REC EXPR: " << from_expr(ns, "", expr) << "\n";
357  std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
358  #endif
359 
360  const typet &expr_type=ns.follow(expr.type());
361 
362  if(expr.id()==ID_unknown || expr.id()==ID_invalid)
363  {
364  insert(dest, exprt(ID_unknown, original_type));
365  }
366  else if(expr.id()==ID_index)
367  {
368  assert(expr.operands().size()==2);
369 
370  const typet &type=ns.follow(expr.op0().type());
371 
372  assert(type.id()==ID_array ||
373  type.id()==ID_incomplete_array);
374 
375  get_value_set_rec(expr.op0(), dest, "[]"+suffix, original_type, ns);
376  }
377  else if(expr.id()==ID_member)
378  {
379  assert(expr.operands().size()==1);
380 
381  const typet &type=ns.follow(expr.op0().type());
382 
383  assert(type.id()==ID_struct ||
384  type.id()==ID_union ||
385  type.id()==ID_incomplete_struct ||
386  type.id()==ID_incomplete_union);
387 
388  const std::string &component_name=
389  expr.get_string(ID_component_name);
390 
391  get_value_set_rec(expr.op0(), dest,
392  "."+component_name+suffix, original_type, ns);
393  }
394  else if(expr.id()==ID_symbol)
395  {
396  irep_idt identifier=to_symbol_expr(expr).get_identifier();
397 
398  // is it a pointer, integer, array or struct?
399  if(expr_type.id()==ID_pointer ||
400  expr_type.id()==ID_signedbv ||
401  expr_type.id()==ID_unsignedbv ||
402  expr_type.id()==ID_struct ||
403  expr_type.id()==ID_union ||
404  expr_type.id()==ID_array)
405  {
406  // look it up
407  valuest::const_iterator v_it=
408  values.find(id2string(identifier)+suffix);
409 
410  // try first component name as suffix if not yet found
411  if(v_it==values.end() &&
412  (expr_type.id()==ID_struct ||
413  expr_type.id()==ID_union))
414  {
415  const struct_union_typet &struct_union_type=
416  to_struct_union_type(expr_type);
417 
418  const std::string first_component_name=
419  struct_union_type.components().front().get_string(ID_name);
420 
421  v_it=values.find(
422  id2string(identifier)+"."+first_component_name+suffix);
423  }
424 
425  // not found? try without suffix
426  if(v_it==values.end())
427  v_it=values.find(identifier);
428 
429  if(v_it!=values.end())
430  make_union(dest, v_it->second.object_map);
431  else
432  insert(dest, exprt(ID_unknown, original_type));
433  }
434  else
435  insert(dest, exprt(ID_unknown, original_type));
436  }
437  else if(expr.id()==ID_if)
438  {
439  if(expr.operands().size()!=3)
440  throw "if takes three operands";
441 
442  get_value_set_rec(expr.op1(), dest, suffix, original_type, ns);
443  get_value_set_rec(expr.op2(), dest, suffix, original_type, ns);
444  }
445  else if(expr.id()==ID_address_of)
446  {
447  if(expr.operands().size()!=1)
448  throw expr.id_string()+" expected to have one operand";
449 
450  get_reference_set(expr.op0(), dest, ns);
451  }
452  else if(expr.id()==ID_dereference)
453  {
454  object_mapt reference_set;
455  get_reference_set(expr, reference_set, ns);
456  const object_map_dt &object_map=reference_set.read();
457 
458  if(object_map.begin()==object_map.end())
459  insert(dest, exprt(ID_unknown, original_type));
460  else
461  {
462  for(object_map_dt::const_iterator
463  it1=object_map.begin();
464  it1!=object_map.end();
465  it1++)
466  {
467  const exprt &object=object_numbering[it1->first];
468  get_value_set_rec(object, dest, suffix, original_type, ns);
469  }
470  }
471  }
472  else if(expr.id()=="reference_to")
473  {
474  // old stuff, will go away
475  object_mapt reference_set;
476 
477  get_reference_set(expr, reference_set, ns);
478 
479  const object_map_dt &object_map=reference_set.read();
480 
481  if(object_map.begin()==object_map.end())
482  insert(dest, exprt(ID_unknown, original_type));
483  else
484  {
485  for(object_map_dt::const_iterator
486  it=object_map.begin();
487  it!=object_map.end();
488  it++)
489  {
490  const exprt &object=object_numbering[it->first];
491  get_value_set_rec(object, dest, suffix, original_type, ns);
492  }
493  }
494  }
495  else if(expr.is_constant())
496  {
497  // check if NULL
498  if(expr.get(ID_value)==ID_NULL &&
499  expr_type.id()==ID_pointer)
500  {
501  insert(dest, exprt("NULL-object", expr_type.subtype()), 0);
502  }
503  else if(expr_type.id()==ID_unsignedbv ||
504  expr_type.id()==ID_signedbv)
505  {
506  // an integer constant got turned into a pointer
507  insert(dest, exprt(ID_integer_address, unsigned_char_type()));
508  }
509  else
510  insert(dest, exprt(ID_unknown, original_type));
511  }
512  else if(expr.id()==ID_typecast)
513  {
514  if(expr.operands().size()!=1)
515  throw "typecast takes one operand";
516 
517  // let's see what gets converted to what
518 
519  const typet &op_type=ns.follow(expr.op0().type());
520 
521  if(op_type.id()==ID_pointer)
522  {
523  // pointer-to-pointer -- we just ignore these
524  get_value_set_rec(expr.op0(), dest, suffix, original_type, ns);
525  }
526  else if(op_type.id()==ID_unsignedbv ||
527  op_type.id()==ID_signedbv)
528  {
529  // integer-to-pointer
530 
531  if(expr.op0().is_zero())
532  insert(dest, exprt("NULL-object", expr_type.subtype()), 0);
533  else
534  {
535  // see if we have something for the integer
536  object_mapt tmp;
537 
538  get_value_set_rec(expr.op0(), tmp, suffix, original_type, ns);
539 
540  if(tmp.read().empty())
541  {
542  // if not, throw in integer
543  insert(dest, exprt(ID_integer_address, unsigned_char_type()));
544  }
545  else if(tmp.read().size()==1 &&
546  object_numbering[tmp.read().begin()->first].id()==ID_unknown)
547  {
548  // if not, throw in integer
549  insert(dest, exprt(ID_integer_address, unsigned_char_type()));
550  }
551  else
552  {
553  // use as is
554  dest.write().insert(tmp.read().begin(), tmp.read().end());
555  }
556  }
557  }
558  else
559  insert(dest, exprt(ID_unknown, original_type));
560  }
561  else if(expr.id()==ID_plus ||
562  expr.id()==ID_minus)
563  {
564  if(expr.operands().size()<2)
565  throw expr.id_string()+" expected to have at least two operands";
566 
567  object_mapt pointer_expr_set;
568  mp_integer i;
569  bool i_is_set=false;
570 
571  // special case for pointer+integer
572 
573  if(expr.operands().size()==2 &&
574  expr_type.id()==ID_pointer)
575  {
576  exprt ptr_operand;
577 
578  if(expr.op0().type().id()!=ID_pointer &&
579  expr.op0().is_constant())
580  {
581  i_is_set=!to_integer(expr.op0(), i);
582  ptr_operand=expr.op1();
583  }
584  else
585  {
586  i_is_set=!to_integer(expr.op1(), i);
587  ptr_operand=expr.op0();
588  }
589 
590  if(i_is_set)
591  {
592  typet pointer_sub_type=ptr_operand.type().subtype();
593  if(pointer_sub_type.id()==ID_empty)
594  pointer_sub_type=char_type();
595 
596  mp_integer size=pointer_offset_size(pointer_sub_type, ns);
597 
598  if(size<=0)
599  {
600  i_is_set=false;
601  }
602  else
603  {
604  i*=size;
605 
606  if(expr.id()==ID_minus)
607  i.negate();
608  }
609  }
610 
612  ptr_operand, pointer_expr_set, "", ptr_operand.type(), ns);
613  }
614  else
615  {
616  // we get the points-to for all operands, even integers
617  forall_operands(it, expr)
618  {
620  *it, pointer_expr_set, "", it->type(), ns);
621  }
622  }
623 
624  for(object_map_dt::const_iterator
625  it=pointer_expr_set.read().begin();
626  it!=pointer_expr_set.read().end();
627  it++)
628  {
629  objectt object=it->second;
630 
631  // adjust by offset
632  if(object.offset_is_zero() && i_is_set)
633  object.offset=i;
634  else
635  object.offset_is_set=false;
636 
637  insert(dest, it->first, object);
638  }
639  }
640  else if(expr.id()==ID_mult)
641  {
642  // this is to do stuff like
643  // (int*)((sel*(ulong)&a)+((sel^0x1)*(ulong)&b))
644 
645  if(expr.operands().size()<2)
646  throw expr.id_string()+" expected to have at least two operands";
647 
648  object_mapt pointer_expr_set;
649 
650  // we get the points-to for all operands, even integers
651  forall_operands(it, expr)
652  {
654  *it, pointer_expr_set, "", it->type(), ns);
655  }
656 
657  for(object_map_dt::const_iterator
658  it=pointer_expr_set.read().begin();
659  it!=pointer_expr_set.read().end();
660  it++)
661  {
662  objectt object=it->second;
663 
664  // kill any offset
665  object.offset_is_set=false;
666 
667  insert(dest, it->first, object);
668  }
669  }
670  else if(expr.id()==ID_side_effect)
671  {
672  const irep_idt &statement=expr.get(ID_statement);
673 
674  if(statement==ID_function_call)
675  {
676  // these should be gone
677  throw "unexpected function_call sideeffect";
678  }
679  else if(statement==ID_malloc)
680  {
681  assert(suffix=="");
682 
683  const typet &dynamic_type=
684  static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
685 
686  dynamic_object_exprt dynamic_object(dynamic_type);
687  dynamic_object.set_instance(location_number);
688  dynamic_object.valid()=true_exprt();
689 
690  insert(dest, dynamic_object, 0);
691  }
692  else if(statement==ID_cpp_new ||
693  statement==ID_cpp_new_array)
694  {
695  assert(suffix=="");
696  assert(expr_type.id()==ID_pointer);
697 
699  dynamic_object.set_instance(location_number);
700  dynamic_object.valid()=true_exprt();
701 
702  insert(dest, dynamic_object, 0);
703  }
704  else
705  insert(dest, exprt(ID_unknown, original_type));
706  }
707  else if(expr.id()==ID_struct)
708  {
709  // a struct constructor, which may contain addresses
710  forall_operands(it, expr)
711  get_value_set_rec(*it, dest, suffix, original_type, ns);
712  }
713  else if(expr.id()==ID_with)
714  {
715  assert(expr.operands().size()==3);
716 
717  // this is the array/struct
718  object_mapt tmp_map0;
719  get_value_set_rec(expr.op0(), tmp_map0, suffix, original_type, ns);
720 
721  // this is the update value -- note NO SUFFIX
722  object_mapt tmp_map2;
723  get_value_set_rec(expr.op2(), tmp_map2, "", original_type, ns);
724 
725  if(expr_type.id()==ID_struct)
726  {
727  #if 0
728  const object_map_dt &object_map0=tmp_map0.read();
729  irep_idt component_name=expr.op1().get(ID_component_name);
730 
731  bool insert=true;
732 
733  for(object_map_dt::const_iterator
734  it=object_map0.begin();
735  it!=object_map0.end();
736  it++)
737  {
738  const exprt &e=to_expr(it);
739 
740  if(e.id()==ID_member &&
741  e.get(ID_component_name)==component_name)
742  {
743  if(insert)
744  {
745  dest.write().insert(tmp_map2.read().begin(), tmp_map2.read().end());
746  insert=false;
747  }
748  }
749  else
750  dest.write().insert(*it);
751  }
752  #else
753  // Should be more precise! We only want "suffix"
754  make_union(dest, tmp_map0);
755  make_union(dest, tmp_map2);
756  #endif
757  }
758  else
759  {
760  make_union(dest, tmp_map0);
761  make_union(dest, tmp_map2);
762  }
763  }
764  else if(expr.id()==ID_array)
765  {
766  // an array constructor, possibly containing addresses
767  forall_operands(it, expr)
768  get_value_set_rec(*it, dest, suffix, original_type, ns);
769  }
770  else if(expr.id()==ID_array_of)
771  {
772  // an array constructor, possibly containing an address
773  assert(expr.operands().size()==1);
774  get_value_set_rec(expr.op0(), dest, suffix, original_type, ns);
775  }
776  else if(expr.id()==ID_dynamic_object)
777  {
780 
781  const std::string prefix=
782  "value_set::dynamic_object"+
783  std::to_string(dynamic_object.get_instance());
784 
785  // first try with suffix
786  const std::string full_name=prefix+suffix;
787 
788  // look it up
789  valuest::const_iterator v_it=values.find(full_name);
790 
791  // not found? try without suffix
792  if(v_it==values.end())
793  v_it=values.find(prefix);
794 
795  if(v_it==values.end())
796  insert(dest, exprt(ID_unknown, original_type));
797  else
798  make_union(dest, v_it->second.object_map);
799  }
800  else if(expr.id()==ID_byte_extract_little_endian ||
801  expr.id()==ID_byte_extract_big_endian)
802  {
803  if(expr.operands().size()!=2)
804  throw "byte_extract takes two operands";
805 
806  bool found=false;
807 
808  exprt op1=expr.op1();
809  if(eval_pointer_offset(op1, ns))
810  simplify(op1, ns);
811 
812  mp_integer op1_offset;
813  const typet &op0_type=ns.follow(expr.op0().type());
814  if(!to_integer(op1, op1_offset) && op0_type.id()==ID_struct)
815  {
816  const struct_typet &struct_type=to_struct_type(op0_type);
817 
818  for(struct_union_typet::componentst::const_iterator
819  c_it=struct_type.components().begin();
820  !found && c_it!=struct_type.components().end();
821  c_it++)
822  {
823  const irep_idt &name=c_it->get_name();
824 
825  mp_integer comp_offset=member_offset(struct_type, name, ns);
826 
827  if(comp_offset>op1_offset)
828  break;
829  else if(comp_offset!=op1_offset)
830  continue;
831 
832  found=true;
833 
834  member_exprt member(expr.op0(), name, c_it->type());
835  get_value_set_rec(member, dest, suffix, original_type, ns);
836  }
837  }
838 
839  if(op0_type.id()==ID_union)
840  {
841  const union_typet &union_type=to_union_type(op0_type);
842 
843  // just collect them all
844  for(union_typet::componentst::const_iterator
845  c_it=union_type.components().begin();
846  c_it!=union_type.components().end(); c_it++)
847  {
848  const irep_idt &name=c_it->get_name();
849  member_exprt member(expr.op0(), name, c_it->type());
850  get_value_set_rec(member, dest, suffix, original_type, ns);
851  }
852  }
853 
854  if(!found)
855  // we just pass through
856  get_value_set_rec(expr.op0(), dest, suffix, original_type, ns);
857  }
858  else if(expr.id()==ID_byte_update_little_endian ||
859  expr.id()==ID_byte_update_big_endian)
860  {
861  if(expr.operands().size()!=3)
862  throw "byte_update takes three operands";
863 
864  // we just pass through
865  get_value_set_rec(expr.op0(), dest, suffix, original_type, ns);
866  get_value_set_rec(expr.op2(), dest, suffix, original_type, ns);
867 
868  // we could have checked object size to be more precise
869  }
870  else
871  {
872  #if 0
873  std::cout << "WARNING: not doing " << expr.id() << '\n';
874  #endif
875  }
876 
877  #if 0
878  std::cout << "GET_VALUE_SET_REC RESULT:\n";
879  for(object_map_dt::const_iterator
880  it=dest.read().begin();
881  it!=dest.read().end();
882  it++)
883  {
884  const exprt &e=to_expr(it);
885  std::cout << " " << from_expr(ns, "", e) << "\n";
886  }
887  std::cout << "\n";
888  #endif
889 }
890 
892  const exprt &src,
893  exprt &dest) const
894 {
895  // remove pointer typecasts
896  if(src.id()==ID_typecast)
897  {
898  assert(src.type().id()==ID_pointer);
899 
900  if(src.operands().size()!=1)
901  throw "typecast expects one operand";
902 
903  dereference_rec(src.op0(), dest);
904  }
905  else
906  dest=src;
907 }
908 
910  const exprt &expr,
911  value_setst::valuest &dest,
912  const namespacet &ns) const
913 {
914  object_mapt object_map;
915  get_reference_set(expr, object_map, ns);
916 
917  for(object_map_dt::const_iterator
918  it=object_map.read().begin();
919  it!=object_map.read().end();
920  it++)
921  dest.push_back(to_expr(it));
922 }
923 
925  const exprt &expr,
926  object_mapt &dest,
927  const namespacet &ns) const
928 {
929  #if 0
930  std::cout << "GET_REFERENCE_SET_REC EXPR: " << from_expr(ns, "", expr)
931  << '\n';
932  #endif
933 
934  if(expr.id()==ID_symbol ||
935  expr.id()==ID_dynamic_object ||
936  expr.id()==ID_string_constant ||
937  expr.id()==ID_array)
938  {
939  if(expr.type().id()==ID_array &&
940  expr.type().subtype().id()==ID_array)
941  insert(dest, expr);
942  else
943  insert(dest, expr, 0);
944 
945  return;
946  }
947  else if(expr.id()==ID_dereference)
948  {
949  if(expr.operands().size()!=1)
950  throw expr.id_string()+" expected to have one operand";
951 
952  get_value_set_rec(expr.op0(), dest, "", expr.op0().type(), ns);
953 
954  #if 0
955  for(expr_sett::const_iterator it=value_set.begin();
956  it!=value_set.end(); it++)
957  std::cout << "VALUE_SET: " << from_expr(ns, "", *it) << '\n';
958  #endif
959 
960  return;
961  }
962  else if(expr.id()==ID_index)
963  {
964  if(expr.operands().size()!=2)
965  throw "index expected to have two operands";
966 
967  const index_exprt &index_expr=to_index_expr(expr);
968  const exprt &array=index_expr.array();
969  const exprt &offset=index_expr.index();
970  const typet &array_type=ns.follow(array.type());
971 
972  assert(array_type.id()==ID_array ||
973  array_type.id()==ID_incomplete_array);
974 
975  object_mapt array_references;
976  get_reference_set(array, array_references, ns);
977 
978  const object_map_dt &object_map=array_references.read();
979 
980  for(object_map_dt::const_iterator
981  a_it=object_map.begin();
982  a_it!=object_map.end();
983  a_it++)
984  {
985  const exprt &object=object_numbering[a_it->first];
986 
987  if(object.id()==ID_unknown)
988  insert(dest, exprt(ID_unknown, expr.type()));
989  else
990  {
991  index_exprt index_expr(expr.type());
992  index_expr.array()=object;
993  index_expr.index()=from_integer(0, index_type());
994 
995  // adjust type?
996  if(ns.follow(object.type())!=array_type)
997  index_expr.make_typecast(array.type());
998 
999  objectt o=a_it->second;
1000  mp_integer i;
1001 
1002  if(offset.is_zero())
1003  {
1004  }
1005  else if(!to_integer(offset, i) &&
1006  o.offset_is_zero())
1007  {
1008  mp_integer size=pointer_offset_size(array_type.subtype(), ns);
1009 
1010  if(size<=0)
1011  o.offset_is_set=false;
1012  else
1013  o.offset=i*size;
1014  }
1015  else
1016  o.offset_is_set=false;
1017 
1018  insert(dest, index_expr, o);
1019  }
1020  }
1021 
1022  return;
1023  }
1024  else if(expr.id()==ID_member)
1025  {
1026  const irep_idt &component_name=expr.get(ID_component_name);
1027 
1028  if(expr.operands().size()!=1)
1029  throw "member expected to have one operand";
1030 
1031  const exprt &struct_op=expr.op0();
1032 
1033  object_mapt struct_references;
1034  get_reference_set(struct_op, struct_references, ns);
1035 
1036  const object_map_dt &object_map=struct_references.read();
1037 
1038  for(object_map_dt::const_iterator
1039  it=object_map.begin();
1040  it!=object_map.end();
1041  it++)
1042  {
1043  const exprt &object=object_numbering[it->first];
1044 
1045  if(object.id()==ID_unknown)
1046  insert(dest, exprt(ID_unknown, expr.type()));
1047  else
1048  {
1049  objectt o=it->second;
1050 
1051  member_exprt member_expr(expr.type());
1052  member_expr.op0()=object;
1053  member_expr.set_component_name(component_name);
1054 
1055  // We cannot introduce a cast from scalar to non-scalar,
1056  // thus, we can only adjust the types of structs and unions.
1057 
1058  const typet &final_object_type = ns.follow(object.type());
1059 
1060  if(final_object_type.id()==ID_struct ||
1061  final_object_type.id()==ID_union)
1062  {
1063  // adjust type?
1064  if(ns.follow(struct_op.type())!=final_object_type)
1065  member_expr.op0().make_typecast(struct_op.type());
1066 
1067  insert(dest, member_expr, o);
1068  }
1069  else
1070  insert(dest, exprt(ID_unknown, expr.type()));
1071  }
1072  }
1073 
1074  return;
1075  }
1076  else if(expr.id()==ID_if)
1077  {
1078  if(expr.operands().size()!=3)
1079  throw "if takes three operands";
1080 
1081  get_reference_set_rec(expr.op1(), dest, ns);
1082  get_reference_set_rec(expr.op2(), dest, ns);
1083  return;
1084  }
1085 
1086  insert(dest, exprt(ID_unknown, expr.type()));
1087 }
1088 
1090  const exprt &lhs,
1091  const exprt &rhs,
1092  const namespacet &ns,
1093  bool is_simplified,
1094  bool add_to_sets)
1095 {
1096  #if 0
1097  std::cout << "ASSIGN LHS: " << from_expr(ns, "", lhs) << '\n';
1098  std::cout << "ASSIGN RHS: " << from_expr(ns, "", rhs) << '\n';
1099  output(ns, std::cout);
1100  #endif
1101 
1102  const typet &type=ns.follow(lhs.type());
1103 
1104  if(type.id()==ID_struct ||
1105  type.id()==ID_union)
1106  {
1107  const struct_union_typet &struct_union_type=
1108  to_struct_union_type(type);
1109 
1110  for(struct_union_typet::componentst::const_iterator
1111  c_it=struct_union_type.components().begin();
1112  c_it!=struct_union_type.components().end();
1113  c_it++)
1114  {
1115  const typet &subtype=c_it->type();
1116  const irep_idt &name=c_it->get(ID_name);
1117 
1118  // ignore methods and padding
1119  if(subtype.id()==ID_code ||
1120  c_it->get_is_padding()) continue;
1121 
1122  member_exprt lhs_member(subtype);
1123  lhs_member.set_component_name(name);
1124  lhs_member.op0()=lhs;
1125 
1126  exprt rhs_member;
1127 
1128  if(rhs.id()==ID_unknown ||
1129  rhs.id()==ID_invalid)
1130  {
1131  rhs_member=exprt(rhs.id(), subtype);
1132  }
1133  else
1134  {
1135  if(!base_type_eq(rhs.type(), type, ns))
1136  throw "value_sett::assign type mismatch: "
1137  "rhs.type():\n"+rhs.type().pretty()+"\n"+
1138  "type:\n"+type.pretty();
1139 
1140  rhs_member=make_member(rhs, name, ns);
1141 
1142  assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
1143  }
1144  }
1145  }
1146  else if(type.id()==ID_array)
1147  {
1148  exprt lhs_index(ID_index, type.subtype());
1149  lhs_index.copy_to_operands(lhs, exprt(ID_unknown, index_type()));
1150 
1151  if(rhs.id()==ID_unknown ||
1152  rhs.id()==ID_invalid)
1153  {
1154  assign(
1155  lhs_index,
1156  exprt(rhs.id(), type.subtype()),
1157  ns,
1158  is_simplified,
1159  add_to_sets);
1160  }
1161  else
1162  {
1163  if(!base_type_eq(rhs.type(), type, ns))
1164  throw "value_sett::assign type mismatch: "
1165  "rhs.type():\n"+rhs.type().pretty()+"\n"+
1166  "type:\n"+type.pretty();
1167 
1168  if(rhs.id()==ID_array_of)
1169  {
1170  assert(rhs.operands().size()==1);
1171  assign(lhs_index, rhs.op0(), ns, is_simplified, add_to_sets);
1172  }
1173  else if(rhs.id()==ID_array ||
1174  rhs.id()==ID_constant)
1175  {
1176  forall_operands(o_it, rhs)
1177  {
1178  assign(lhs_index, *o_it, ns, is_simplified, add_to_sets);
1179  add_to_sets=true;
1180  }
1181  }
1182  else if(rhs.id()==ID_with)
1183  {
1184  assert(rhs.operands().size()==3);
1185 
1186  exprt op0_index(ID_index, type.subtype());
1187  op0_index.copy_to_operands(rhs.op0(), exprt(ID_unknown, index_type()));
1188 
1189  assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
1190  assign(lhs_index, rhs.op2(), ns, is_simplified, true);
1191  }
1192  else
1193  {
1194  exprt rhs_index(ID_index, type.subtype());
1195  rhs_index.copy_to_operands(rhs, exprt(ID_unknown, index_type()));
1196  assign(lhs_index, rhs_index, ns, is_simplified, true);
1197  }
1198  }
1199  }
1200  else
1201  {
1202  // basic type
1203  object_mapt values_rhs;
1204  get_value_set(rhs, values_rhs, ns, is_simplified);
1205 
1206  assign_rec(lhs, values_rhs, "", ns, add_to_sets);
1207  }
1208 }
1209 
1211  const exprt &op,
1212  const namespacet &ns)
1213 {
1214  // op must be a pointer
1215  if(op.type().id()!=ID_pointer)
1216  throw "free expected to have pointer-type operand";
1217 
1218  // find out what it points to
1219  object_mapt value_set;
1220  get_value_set(op, value_set, ns, false);
1221 
1222  const object_map_dt &object_map=value_set.read();
1223 
1224  // find out which *instances* interest us
1225  dynamic_object_id_sett to_mark;
1226 
1227  for(object_map_dt::const_iterator
1228  it=object_map.begin();
1229  it!=object_map.end();
1230  it++)
1231  {
1232  const exprt &object=object_numbering[it->first];
1233 
1234  if(object.id()==ID_dynamic_object)
1235  {
1237  to_dynamic_object_expr(object);
1238 
1239  if(dynamic_object.valid().is_true())
1240  to_mark.insert(dynamic_object.get_instance());
1241  }
1242  }
1243 
1244  // mark these as 'may be invalid'
1245  // this, unfortunately, destroys the sharing
1246  for(valuest::iterator v_it=values.begin();
1247  v_it!=values.end();
1248  v_it++)
1249  {
1250  object_mapt new_object_map;
1251 
1252  const object_map_dt &old_object_map=
1253  v_it->second.object_map.read();
1254 
1255  bool changed=false;
1256 
1257  for(object_map_dt::const_iterator
1258  o_it=old_object_map.begin();
1259  o_it!=old_object_map.end();
1260  o_it++)
1261  {
1262  const exprt &object=object_numbering[o_it->first];
1263 
1264  if(object.id()==ID_dynamic_object)
1265  {
1267  to_dynamic_object_expr(object);
1268 
1269  if(to_mark.count(dynamic_object.get_instance())==0)
1270  set(new_object_map, o_it);
1271  else
1272  {
1273  // adjust
1274  objectt o=o_it->second;
1275  exprt tmp(object);
1276  to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
1277  insert(new_object_map, tmp, o);
1278  changed=true;
1279  }
1280  }
1281  else
1282  set(new_object_map, o_it);
1283  }
1284 
1285  if(changed)
1286  v_it->second.object_map=new_object_map;
1287  }
1288 }
1289 
1291  const exprt &lhs,
1292  const object_mapt &values_rhs,
1293  const std::string &suffix,
1294  const namespacet &ns,
1295  bool add_to_sets)
1296 {
1297  #if 0
1298  std::cout << "ASSIGN_REC LHS: " << from_expr(ns, "", lhs) << '\n';
1299  std::cout << "ASSIGN_REC LHS ID: " << lhs.id() << '\n';
1300  std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1301 
1302  for(object_map_dt::const_iterator it=values_rhs.read().begin();
1303  it!=values_rhs.read().end();
1304  it++)
1305  std::cout << "ASSIGN_REC RHS: " <<
1306  from_expr(ns, "", object_numbering[it->first]) << '\n';
1307  std::cout << '\n';
1308  #endif
1309 
1310  if(lhs.id()==ID_symbol)
1311  {
1312  const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
1313 
1314  entryt &e=get_entry(entryt(identifier, suffix), lhs.type(), ns);
1315 
1316  if(add_to_sets)
1317  make_union(e.object_map, values_rhs);
1318  else
1319  e.object_map=values_rhs;
1320  }
1321  else if(lhs.id()==ID_dynamic_object)
1322  {
1325 
1326  const std::string name=
1327  "value_set::dynamic_object"+
1328  std::to_string(dynamic_object.get_instance());
1329 
1330  entryt &e=get_entry(entryt(name, suffix), lhs.type(), ns);
1331 
1332  make_union(e.object_map, values_rhs);
1333  }
1334  else if(lhs.id()==ID_dereference)
1335  {
1336  if(lhs.operands().size()!=1)
1337  throw lhs.id_string()+" expected to have one operand";
1338 
1339  object_mapt reference_set;
1340  get_reference_set(lhs, reference_set, ns);
1341 
1342  if(reference_set.read().size()!=1)
1343  add_to_sets=true;
1344 
1345  for(object_map_dt::const_iterator
1346  it=reference_set.read().begin();
1347  it!=reference_set.read().end();
1348  it++)
1349  {
1350  const exprt &object=object_numbering[it->first];
1351 
1352  if(object.id()!=ID_unknown)
1353  assign_rec(object, values_rhs, suffix, ns, add_to_sets);
1354  }
1355  }
1356  else if(lhs.id()==ID_index)
1357  {
1358  if(lhs.operands().size()!=2)
1359  throw "index expected to have two operands";
1360 
1361  const typet &type=ns.follow(lhs.op0().type());
1362 
1363  assert(type.id()==ID_array || type.id()==ID_incomplete_array);
1364 
1365  assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, true);
1366  }
1367  else if(lhs.id()==ID_member)
1368  {
1369  if(lhs.operands().size()!=1)
1370  throw "member expected to have one operand";
1371 
1372  const std::string &component_name=lhs.get_string(ID_component_name);
1373 
1374  const typet &type=ns.follow(lhs.op0().type());
1375 
1376  assert(type.id()==ID_struct ||
1377  type.id()==ID_union ||
1378  type.id()==ID_incomplete_struct ||
1379  type.id()==ID_incomplete_union);
1380 
1381  assign_rec(
1382  lhs.op0(), values_rhs, "."+component_name+suffix, ns, add_to_sets);
1383  }
1384  else if(lhs.id()=="valid_object" ||
1385  lhs.id()=="dynamic_size" ||
1386  lhs.id()=="dynamic_type" ||
1387  lhs.id()=="is_zero_string" ||
1388  lhs.id()=="zero_string" ||
1389  lhs.id()=="zero_string_length")
1390  {
1391  // we ignore this here
1392  }
1393  else if(lhs.id()==ID_string_constant)
1394  {
1395  // someone writes into a string-constant
1396  // evil guy
1397  }
1398  else if(lhs.id()=="NULL-object")
1399  {
1400  // evil as well
1401  }
1402  else if(lhs.id()==ID_typecast)
1403  {
1404  const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1405 
1406  assign_rec(typecast_expr.op(), values_rhs, suffix, ns, add_to_sets);
1407  }
1408  else if(lhs.id()==ID_byte_extract_little_endian ||
1409  lhs.id()==ID_byte_extract_big_endian)
1410  {
1411  assert(lhs.operands().size()==2);
1412  assign_rec(lhs.op0(), values_rhs, suffix, ns, true);
1413  }
1414  else if(lhs.id()==ID_integer_address)
1415  {
1416  // that's like assigning into __CPROVER_memory[...],
1417  // which we don't track
1418  }
1419  else
1420  throw "assign NYI: `"+lhs.id_string()+"'";
1421 }
1422 
1424  const irep_idt &function,
1425  const exprt::operandst &arguments,
1426  const namespacet &ns)
1427 {
1428  const symbolt &symbol=ns.lookup(function);
1429 
1430  const code_typet &type=to_code_type(symbol.type);
1431  const code_typet::parameterst &parameter_types=type.parameters();
1432 
1433  // these first need to be assigned to dummy, temporary arguments
1434  // and only thereafter to the actuals, in order
1435  // to avoid overwriting actuals that are needed for recursive
1436  // calls
1437 
1438  for(unsigned i=0; i<arguments.size(); i++)
1439  {
1440  const std::string identifier="value_set::dummy_arg_"+std::to_string(i);
1441  exprt dummy_lhs=symbol_exprt(identifier, arguments[i].type());
1442  assign(dummy_lhs, arguments[i], ns, false, false);
1443  }
1444 
1445  // now assign to 'actual actuals'
1446 
1447  unsigned i=0;
1448 
1449  for(code_typet::parameterst::const_iterator
1450  it=parameter_types.begin();
1451  it!=parameter_types.end();
1452  it++)
1453  {
1454  const irep_idt &identifier=it->get_identifier();
1455  if(identifier=="")
1456  continue;
1457 
1458  const exprt v_expr=
1459  symbol_exprt("value_set::dummy_arg_"+std::to_string(i), it->type());
1460 
1461  exprt actual_lhs=symbol_exprt(identifier, it->type());
1462  assign(actual_lhs, v_expr, ns, true, true);
1463  i++;
1464  }
1465 
1466  // we could delete the dummy_arg_* now.
1467 }
1468 
1470  const exprt &lhs,
1471  const namespacet &ns)
1472 {
1473  if(lhs.is_nil())
1474  return;
1475 
1476  symbol_exprt rhs("value_set::return_value", lhs.type());
1477 
1478  assign(lhs, rhs, ns, false, false);
1479 }
1480 
1482  const codet &code,
1483  const namespacet &ns)
1484 {
1485  const irep_idt &statement=code.get_statement();
1486 
1487  if(statement==ID_block)
1488  {
1489  forall_operands(it, code)
1490  apply_code(to_code(*it), ns);
1491  }
1492  else if(statement==ID_function_call)
1493  {
1494  // shouldn't be here
1495  assert(false);
1496  }
1497  else if(statement==ID_assign ||
1498  statement==ID_init)
1499  {
1500  if(code.operands().size()!=2)
1501  throw "assignment expected to have two operands";
1502 
1503  assign(code.op0(), code.op1(), ns, false, false);
1504  }
1505  else if(statement==ID_decl)
1506  {
1507  if(code.operands().size()!=1)
1508  throw "decl expected to have one operand";
1509 
1510  const exprt &lhs=code.op0();
1511 
1512  if(lhs.id()!=ID_symbol)
1513  throw "decl expected to have symbol on lhs";
1514 
1515  const typet &lhs_type=ns.follow(lhs.type());
1516 
1517  if(lhs_type.id()==ID_pointer ||
1518  (lhs_type.id()==ID_array &&
1519  ns.follow(lhs_type.subtype()).id()==ID_pointer))
1520  {
1521  // assign the address of the failed object
1522  exprt failed=get_failed_symbol(to_symbol_expr(lhs), ns);
1523 
1524  if(failed.is_not_nil())
1525  {
1526  address_of_exprt address_of_expr;
1527  address_of_expr.object()=failed;
1528  address_of_expr.type()=lhs.type();
1529  assign(lhs, address_of_expr, ns, false, false);
1530  }
1531  else
1532  assign(lhs, exprt(ID_invalid), ns, false, false);
1533  }
1534  }
1535  else if(statement=="specc_notify" ||
1536  statement=="specc_wait")
1537  {
1538  // ignore, does not change variables
1539  }
1540  else if(statement==ID_expression)
1541  {
1542  // can be ignored, we don't expect side effects here
1543  }
1544  else if(statement=="cpp_delete" ||
1545  statement=="cpp_delete[]")
1546  {
1547  // does nothing
1548  }
1549  else if(statement==ID_free)
1550  {
1551  // this may kill a valid bit
1552 
1553  if(code.operands().size()!=1)
1554  throw "free expected to have one operand";
1555 
1556  do_free(code.op0(), ns);
1557  }
1558  else if(statement=="lock" || statement=="unlock")
1559  {
1560  // ignore for now
1561  }
1562  else if(statement==ID_asm)
1563  {
1564  // ignore for now, probably not safe
1565  }
1566  else if(statement==ID_nondet)
1567  {
1568  // doesn't do anything
1569  }
1570  else if(statement==ID_printf)
1571  {
1572  // doesn't do anything
1573  }
1574  else if(statement==ID_return)
1575  {
1576  // this is turned into an assignment
1577  if(code.operands().size()==1)
1578  {
1579  symbol_exprt lhs("value_set::return_value", code.op0().type());
1580  assign(lhs, code.op0(), ns, false, false);
1581  }
1582  }
1583  else if(statement==ID_array_set)
1584  {
1585  }
1586  else if(statement==ID_array_copy)
1587  {
1588  }
1589  else if(statement==ID_array_replace)
1590  {
1591  }
1592  else if(statement==ID_assume)
1593  {
1594  guard(to_code_assume(code).op0(), ns);
1595  }
1596  else if(statement==ID_user_specified_predicate ||
1597  statement==ID_user_specified_parameter_predicates ||
1598  statement==ID_user_specified_return_predicates)
1599  {
1600  // doesn't do anything
1601  }
1602  else if(statement==ID_fence)
1603  {
1604  }
1605  else if(statement==ID_input || statement==ID_output)
1606  {
1607  // doesn't do anything
1608  }
1609  else
1610  {
1611  // std::cerr << code.pretty() << '\n';
1612  throw "value_sett: unexpected statement: "+id2string(statement);
1613  }
1614 }
1615 
1617  const exprt &expr,
1618  const namespacet &ns)
1619 {
1620  if(expr.id()==ID_and)
1621  {
1622  forall_operands(it, expr)
1623  guard(*it, ns);
1624  }
1625  else if(expr.id()==ID_equal)
1626  {
1627  }
1628  else if(expr.id()==ID_notequal)
1629  {
1630  }
1631  else if(expr.id()==ID_not)
1632  {
1633  }
1634  else if(expr.id()==ID_dynamic_object)
1635  {
1636  assert(expr.operands().size()==1);
1637 
1639  // dynamic_object.instance()=
1640  // from_integer(location_number, typet(ID_natural));
1641  dynamic_object.valid()=true_exprt();
1642 
1643  address_of_exprt address_of(dynamic_object);
1644  address_of.type()=expr.op0().type();
1645 
1646  assign(expr.op0(), address_of, ns, false, false);
1647  }
1648 }
1649 
1651  const exprt &src,
1652  const irep_idt &component_name,
1653  const namespacet &ns)
1654 {
1655  const struct_union_typet &struct_union_type=
1657 
1658  if(src.id()==ID_struct ||
1659  src.id()==ID_constant)
1660  {
1661  std::size_t no=struct_union_type.component_number(component_name);
1662  assert(no<src.operands().size());
1663  return src.operands()[no];
1664  }
1665  else if(src.id()==ID_with)
1666  {
1667  assert(src.operands().size()==3);
1668 
1669  // see if op1 is the member we want
1670  const exprt &member_operand=src.op1();
1671 
1672  if(component_name==member_operand.get(ID_component_name))
1673  // yes! just take op2
1674  return src.op2();
1675  else
1676  // no! do this recursively
1677  return make_member(src.op0(), component_name, ns);
1678  }
1679  else if(src.id()==ID_typecast)
1680  {
1681  // push through typecast
1682  assert(src.operands().size()==1);
1683  return make_member(src.op0(), component_name, ns);
1684  }
1685 
1686  // give up
1687  typet subtype=struct_union_type.component_type(component_name);
1688  member_exprt member_expr(subtype);
1689  member_expr.op0()=src;
1690  member_expr.set_component_name(component_name);
1691 
1692  return member_expr;
1693 }
const irep_idt & get_statement() const
Definition: std_code.h:37
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
const namespacet & ns
semantic type conversion
Definition: std_expr.h:1725
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
static int8_t r
Definition: irep_hash.h:59
bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set.h:77
BigInt mp_integer
Definition: mp_arith.h:19
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
exprt & object()
Definition: std_expr.h:2608
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
Definition: std_expr.h:1701
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:298
object_mapt object_map
Definition: value_set.h:104
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
const irep_idt & get_identifier() const
Definition: std_expr.h:120
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Definition: value_set.cpp:1089
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool make_union(object_mapt &dest, const object_mapt &src) const
Definition: value_set.cpp:246
std::vector< parametert > parameterst
Definition: std_types.h:829
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
Definition: value_set.cpp:924
bool offset_is_zero() const
Definition: value_set.h:57
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Definition: value_set.cpp:314
const componentst & components() const
Definition: std_types.h:242
Value Set.
static const object_map_dt blank
Definition: value_set.h:65
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
static object_numberingt object_numbering
Definition: value_set.h:38
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void dereference_rec(const exprt &src, exprt &dest) const
Definition: value_set.cpp:891
Pointer Dereferencing.
Structure type.
Definition: std_types.h:296
exprt & op()
Definition: std_expr.h:1739
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
Definition: value_set.cpp:1290
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
mp_integer offset
Definition: value_set.h:55
exprt to_expr(object_map_dt::const_iterator it) const
Definition: value_set.cpp:187
Extract member of struct or union.
Definition: std_expr.h:3214
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3254
static bool field_sensitive(const irep_idt &id, const typet &type, const namespacet &)
Definition: value_set.cpp:39
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:3742
bool eval_pointer_offset(exprt &expr, const namespacet &ns) const
Definition: value_set.cpp:261
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Definition: value_set.cpp:1423
TO_BE_DOCUMENTED.
Definition: namespace.h:62
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1578
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
Definition: value_set.cpp:348
#define forall_operands(it, expr)
Definition: expr.h:17
bitvector_typet index_type()
Definition: c_types.cpp:15
Symbol table.
typet component_type(const irep_idt &component_name) const
Definition: std_types.cpp:68
Operator to return the address of an object.
Definition: std_expr.h:2593
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
bool is_constant() const
Definition: expr.cpp:128
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Pointer Logic.
const irep_idt & display_name() const
Definition: symbol.h:60
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
std::unordered_map< idt, entryt, string_hash > valuest
Definition: value_set.h:126
entryt & get_entry(const entryt &e, const typet &type, const namespacet &)
Definition: value_set.cpp:54
typet type
Type of symbol.
Definition: symbol.h:37
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition: value_set.cpp:1469
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
exprt & index()
Definition: std_expr.h:1208
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Definition: value_set.cpp:909
Base class for all expressions.
Definition: expr.h:46
The union type.
Definition: std_types.h:424
const parameterst & parameters() const
Definition: std_types.h:841
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
std::set< unsigned int > dynamic_object_id_sett
Definition: value_set.h:121
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const T & read() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
bool is_zero() const
Definition: expr.cpp:236
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
void output(const namespacet &ns, std::ostream &out) const
Definition: value_set.cpp:97
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
exprt dynamic_object(const exprt &pointer)
A statement in a programming language.
Definition: std_code.h:19
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:134
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
TO_BE_DOCUMENTED.
Definition: std_expr.h:1658
void guard(const exprt &expr, const namespacet &ns)
Definition: value_set.cpp:1616
operandst & operands()
Definition: expr.h:70
void do_free(const exprt &op, const namespacet &ns)
Definition: value_set.cpp:1210
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::list< exprt > valuest
Definition: value_sets.h:28
std::string suffix
Definition: value_set.h:106
exprt & array()
Definition: std_expr.h:1198
void make_typecast(const typet &_type)
Definition: expr.cpp:90
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
valuest values
Definition: value_set.h:156
bitvector_typet char_type()
Definition: c_types.cpp:113
void apply_code(const codet &code, const namespacet &ns)
Definition: value_set.cpp:1481
bool simplify(exprt &expr, const namespacet &ns)
unsigned location_number
Definition: value_set.h:37
exprt make_member(const exprt &src, const irep_idt &component_name, const namespacet &ns)
Definition: value_set.cpp:1650
array index operator
Definition: std_expr.h:1170