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