cprover
value_set_fivrns.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set (Flow Insensitive, Validity Regions)
4 
5 Author: Daniel Kroening, kroening@kroening.com,
6  CM Wintersteiger
7 
8 \*******************************************************************/
9 
12 
13 #include "value_set_fivrns.h"
14 
15 #include <cassert>
16 #include <ostream>
17 
18 #include <util/symbol_table.h>
19 #include <util/simplify_expr.h>
20 #include <util/base_type.h>
21 #include <util/std_expr.h>
22 #include <util/prefix.h>
23 #include <util/std_code.h>
24 #include <util/arith_tools.h>
25 
26 #include <langapi/language_util.h>
27 #include <util/c_types.h>
28 
32 
33 static const char *alloc_adapter_prefix="alloc_adaptor::";
34 
35 #define forall_objects(it, map) \
36  for(object_map_dt::const_iterator it = (map).begin(); \
37  (it)!=(map).end(); \
38  (it)++)
39 
40 #define forall_valid_objects(it, map) \
41  for(object_map_dt::const_iterator it = (map).begin(); \
42  (it)!=(map).end(); \
43  (it)++) \
44  if((map).is_valid_at((it)->first, from_function, from_target_index))
45 
46 #define Forall_objects(it, map) \
47  for(object_map_dt::iterator it = (map).begin(); \
48  (it)!=(map).end(); \
49  (it)++)
50 
51 #define Forall_valid_objects(it, map) \
52  for(object_map_dt::iterator it = (map).begin(); \
53  (it)!=(map).end(); \
54  (it)++) \
55  if((map).is_valid_at((it)->first, from_function, from_target_index)) /* NOLINT(*) */
56 
58  const namespacet &ns,
59  std::ostream &out) const
60 {
61  for(valuest::const_iterator
62  v_it=values.begin();
63  v_it!=values.end();
64  v_it++)
65  output_entry(v_it->second, ns, out);
66 }
67 
69  const entryt &e,
70  const namespacet &ns,
71  std::ostream &out) const
72 {
73  irep_idt identifier, display_name;
74 // if(has_prefix(id2string(e.identifier), "value_set::dynamic_object"))
75 // {
76 // display_name=id2string(e.identifier)+e.suffix;
77 // identifier="";
78 // }
79 // else if(e.identifier=="value_set::return_value")
80 // {
81 // display_name="RETURN_VALUE"+e.suffix;
82 // identifier="";
83 // }
84 // else
85  {
86  #if 0
87  const symbolt &symbol=ns.lookup(id2string(e.identifier));
88  display_name=symbol.display_name()+e.suffix;
89  identifier=symbol.name;
90  #else
91  display_name=id2string(e.identifier)+e.suffix;
92  #endif
93  }
94 
95  const object_mapt &object_map=e.object_map;
96 
97  out << display_name << " = { ";
98  if(!object_map.read().empty())
99  out << "\n ";
100 
101  std::size_t width=0;
102 
103  forall_valid_objects(o_it, object_map.read())
104  {
105  const exprt &o=object_numbering[o_it->first];
106 
107  std::string result="<"; // +std::to_string(o_it->first) + ",";
108 
109  if(o.id()==ID_invalid)
110  {
111  result+='#';
112  result+=", *, "; // offset unknown
113  if(o.type().id()==ID_unknown)
114  result+='*';
115  else if(o.type().id()==ID_invalid)
116  result+='#';
117  else
118  result+=from_type(ns, identifier, o.type());
119  result+='>';
120  }
121  else if(o.id()==ID_unknown)
122  {
123  result+='*';
124  result+=", *, "; // offset unknown
125  if(o.type().id()==ID_unknown)
126  result+='*';
127  else if(o.type().id()==ID_invalid)
128  result+='#';
129  else
130  result+=from_type(ns, identifier, o.type());
131  result+='>';
132  }
133  else
134  {
135  result+=from_expr(ns, identifier, o)+", ";
136 
137  if(o_it->second)
138  result += integer2string(*o_it->second) + "";
139  else
140  result+='*';
141 
142  result+=", ";
143 
144  if(o.type().id()==ID_unknown)
145  result+='*';
146  else
147  {
148  result+=from_type(ns, identifier, o.type());
149  }
150 
151 
152  result+='>';
153  }
154 
155  out << result << '\n';
156 
157  #if 0
158  object_map_dt::validity_rangest::const_iterator vr =
159  object_map.read().validity_ranges.find(o_it->first);
160 
161  if(vr != object_map.read().validity_ranges.end())
162  {
163  if(vr->second.empty())
164  std::cout << " Empty validity record\n";
165  else
166  {
167  for(object_map_dt::vrange_listt::const_iterator vit =
168  vr->second.begin();
169  vit!=vr->second.end();
170  vit++)
171  {
172  out << " valid at " << function_numbering[vit->function] <<
173  " [" << vit->from << "," << vit->to << "]";
174  if(from_function==vit->function &&
175  from_target_index>=vit->from &&
176  from_target_index<=vit->to)
177  out << " (*)";
178  out << '\n';
179  }
180  }
181  }
182  else
183  {
184  out << " No validity information\n";
185  }
186  #endif
187 
188  width+=result.size();
189 
191  next++;
192 
193  if(next!=object_map.read().end())
194  {
195  out << "\n ";
196  }
197  }
198 
199  out << " } \n";
200 }
201 
203 {
204  const exprt &object=object_numbering[it->first];
205 
206  if(object.id()==ID_invalid ||
207  object.id()==ID_unknown)
208  return object;
209 
211 
212  od.object()=object;
213 
214  if(it->second)
215  od.offset() = from_integer(*it->second, index_type());
216 
217  od.type()=od.object().type();
218 
219  return std::move(od);
220 }
221 
223  object_mapt &dest,
224  const object_mapt &src) const
225 {
226  bool result=false;
227 
228  forall_objects(it, src.read())
229  {
230  if(insert_to(dest, it))
231  result=true;
232  }
233 
234  return result;
235 }
236 
238  object_mapt &dest,
239  const object_mapt &src) const
240 {
241  bool result=false;
242 
243  forall_valid_objects(it, src.read())
244  {
245  if(insert_to(dest, it))
246  result=true;
247  }
248 
249  return result;
250 }
251 
253  object_mapt &dest,
254  const object_mapt &src) const
255 {
256  forall_valid_objects(it, src.read())
257  {
258  dest.write()[it->first] = it->second;
259  dest.write().validity_ranges[it->first].push_back(
263  }
264 }
265 
267  const exprt &expr,
268  std::list<exprt> &value_set,
269  const namespacet &ns) const
270 {
271  object_mapt object_map;
272  get_value_set(expr, object_map, ns);
273 
274  forall_objects(it, object_map.read())
275  value_set.push_back(to_expr(it));
276 
277  #if 0
278  for(std::list<exprt>::const_iterator it=value_set.begin();
279  it!=value_set.end(); it++)
280  std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
281  #endif
282 }
283 
285  const exprt &expr,
286  object_mapt &dest,
287  const namespacet &ns) const
288 {
289  exprt tmp(expr);
290  simplify(tmp, ns);
291 
292  get_value_set_rec(tmp, dest, "", tmp.type(), ns);
293 }
294 
296  const exprt &expr,
297  object_mapt &dest,
298  const std::string &suffix,
299  const typet &original_type,
300  const namespacet &ns) const
301 {
302  #if 0
303  std::cout << "GET_VALUE_SET_REC EXPR: " << expr << '\n';
304  std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
305  std::cout << '\n';
306  #endif
307 
308  if(expr.id()==ID_unknown || expr.id()==ID_invalid)
309  {
310  insert_from(dest, exprt(ID_unknown, original_type));
311  return;
312  }
313  else if(expr.id()==ID_index)
314  {
315  assert(expr.operands().size()==2);
316 
317  const typet &type=ns.follow(expr.op0().type());
318 
319  DATA_INVARIANT(type.id()==ID_array ||
320  type.id()==ID_incomplete_array,
321  "operand 0 of index expression must be an array");
322 
323  get_value_set_rec(expr.op0(), dest, "[]"+suffix, original_type, ns);
324 
325  return;
326  }
327  else if(expr.id()==ID_member)
328  {
329  assert(expr.operands().size()==1);
330 
331  if(expr.op0().is_not_nil())
332  {
333  const typet &type=ns.follow(expr.op0().type());
334 
335  DATA_INVARIANT(type.id()==ID_struct ||
336  type.id()==ID_union ||
337  type.id()==ID_incomplete_struct ||
338  type.id()==ID_incomplete_union,
339  "operand 0 of member expression must be struct or union");
340 
341  const std::string &component_name=
342  expr.get_string(ID_component_name);
343 
344  get_value_set_rec(expr.op0(), dest, "."+component_name+suffix,
345  original_type, ns);
346 
347  return;
348  }
349  }
350  else if(expr.id()==ID_symbol)
351  {
352  // just keep a reference to the ident in the set
353  // (if it exists)
354  irep_idt ident = id2string(to_symbol_expr(expr).get_identifier()) + suffix;
355 
357  {
358  insert_from(dest, expr, 0);
359  return;
360  }
361  else
362  {
363  valuest::const_iterator v_it=values.find(ident);
364 
365  if(v_it!=values.end())
366  {
367  copy_objects(dest, v_it->second.object_map);
368  return;
369  }
370  }
371  }
372  else if(expr.id()==ID_if)
373  {
374  if(expr.operands().size()!=3)
375  throw "if takes three operands";
376 
377  get_value_set_rec(expr.op1(), dest, suffix,
378  original_type, ns);
379  get_value_set_rec(expr.op2(), dest, suffix,
380  original_type, ns);
381 
382  return;
383  }
384  else if(expr.id()==ID_address_of)
385  {
386  if(expr.operands().size()!=1)
387  throw expr.id_string()+" expected to have one operand";
388 
389  get_reference_set(expr.op0(), dest, ns);
390 
391  return;
392  }
393  else if(expr.id()==ID_dereference)
394  {
395  object_mapt reference_set;
396  get_reference_set(expr, reference_set, ns);
397  const object_map_dt &object_map=reference_set.read();
398 
399  if(object_map.begin()!=object_map.end())
400  {
401  forall_objects(it1, object_map)
402  {
403  const exprt &object=object_numbering[it1->first];
404  get_value_set_rec(object, dest, suffix,
405  original_type, ns);
406  }
407 
408  return;
409  }
410  }
411  else if(expr.id()=="reference_to")
412  {
413  object_mapt reference_set;
414 
415  get_reference_set(expr, reference_set, ns);
416 
417  const object_map_dt &object_map=reference_set.read();
418 
419  if(object_map.begin()!=object_map.end())
420  {
421  forall_objects(it, object_map)
422  {
423  const exprt &object=object_numbering[it->first];
424  get_value_set_rec(object, dest, suffix,
425  original_type, ns);
426  }
427 
428  return;
429  }
430  }
431  else if(expr.is_constant())
432  {
433  // check if NULL
434  if(expr.get(ID_value)==ID_NULL &&
435  expr.type().id()==ID_pointer)
436  {
437  insert_from(dest, exprt(ID_null_object, expr.type().subtype()), 0);
438  return;
439  }
440  }
441  else if(expr.id()==ID_typecast)
442  {
443  if(expr.operands().size()!=1)
444  throw "typecast takes one operand";
445 
446  get_value_set_rec(expr.op0(), dest, suffix,
447  original_type, ns);
448 
449  return;
450  }
451  else if(expr.id()==ID_plus || expr.id()==ID_minus)
452  {
453  if(expr.operands().size()<2)
454  throw expr.id_string()+" expected to have at least two operands";
455 
456  if(expr.type().id()==ID_pointer)
457  {
458  // find the pointer operand
459  const exprt *ptr_operand=nullptr;
460 
461  forall_operands(it, expr)
462  if(it->type().id()==ID_pointer)
463  {
464  if(ptr_operand==nullptr)
465  ptr_operand=&(*it);
466  else
467  throw "more than one pointer operand in pointer arithmetic";
468  }
469 
470  if(ptr_operand==nullptr)
471  throw "pointer type sum expected to have pointer operand";
472 
473  object_mapt pointer_expr_set;
474  get_value_set_rec(*ptr_operand, pointer_expr_set, "",
475  ptr_operand->type(), ns);
476 
477  forall_objects(it, pointer_expr_set.read())
478  {
479  offsett offset = it->second;
480 
481  if(offset_is_zero(offset) && expr.operands().size() == 2)
482  {
483  if(expr.op0().type().id()!=ID_pointer)
484  {
485  mp_integer i;
486  if(to_integer(expr.op0(), i))
487  offset.reset();
488  else
489  *offset = (expr.id() == ID_plus) ? i : -i;
490  }
491  else
492  {
493  mp_integer i;
494  if(to_integer(expr.op1(), i))
495  offset.reset();
496  else
497  *offset = (expr.id() == ID_plus) ? i : -i;
498  }
499  }
500  else
501  offset.reset();
502 
503  insert_from(dest, it->first, offset);
504  }
505 
506  return;
507  }
508  }
509  else if(expr.id()==ID_side_effect)
510  {
511  const irep_idt &statement=expr.get(ID_statement);
512 
513  if(statement==ID_function_call)
514  {
515  // these should be gone
516  throw "unexpected function_call sideeffect";
517  }
518  else if(statement==ID_allocate)
519  {
520  if(expr.type().id()!=ID_pointer)
521  throw "malloc expected to return pointer type";
522 
523  assert(suffix=="");
524 
525  const typet &dynamic_type=
526  static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
527 
528  dynamic_object_exprt dynamic_object(dynamic_type);
529  // let's make up a `unique' number for this object...
530  dynamic_object.set_instance(
531  (from_function << 16) | from_target_index);
532  dynamic_object.valid()=true_exprt();
533 
534  insert_from(dest, dynamic_object, 0);
535  return;
536  }
537  else if(statement==ID_cpp_new ||
538  statement==ID_cpp_new_array)
539  {
540  assert(suffix=="");
541  assert(expr.type().id()==ID_pointer);
542 
543  dynamic_object_exprt dynamic_object(expr.type().subtype());
544  // let's make up a unique number for this object...
545  dynamic_object.set_instance(
546  (from_function << 16) | from_target_index);
547  dynamic_object.valid()=true_exprt();
548 
549  insert_from(dest, dynamic_object, 0);
550  return;
551  }
552  }
553  else if(expr.id()==ID_struct)
554  {
555  // this is like a static struct object
556  insert_from(dest, address_of_exprt(expr), 0);
557  return;
558  }
559  else if(expr.id()==ID_with ||
560  expr.id()==ID_array_of ||
561  expr.id()==ID_array)
562  {
563  // these are supposed to be done by assign()
564  throw "unexpected value in get_value_set: "+expr.id_string();
565  }
566  else if(expr.id()==ID_dynamic_object)
567  {
570 
571  const std::string name=
572  "value_set::dynamic_object"+
573  std::to_string(dynamic_object.get_instance())+
574  suffix;
575 
576  // look it up
577  valuest::const_iterator v_it=values.find(name);
578 
579  if(v_it!=values.end())
580  {
581  copy_objects(dest, v_it->second.object_map);
582  return;
583  }
584  }
585 
586  insert_from(dest, exprt(ID_unknown, original_type));
587 }
588 
590  const exprt &src,
591  exprt &dest) const
592 {
593  // remove pointer typecasts
594  if(src.id()==ID_typecast)
595  {
596  assert(src.type().id()==ID_pointer);
597 
598  if(src.operands().size()!=1)
599  throw "typecast expects one operand";
600 
601  dereference_rec(src.op0(), dest);
602  }
603  else
604  dest=src;
605 }
606 
608  const exprt &expr,
609  expr_sett &dest,
610  const namespacet &ns) const
611 {
612  object_mapt object_map;
613  get_reference_set(expr, object_map, ns);
614 
615  forall_objects(it, object_map.read())
616  dest.insert(to_expr(it));
617 }
618 
620  const exprt &expr,
621  object_mapt &dest,
622  const namespacet &ns) const
623 {
624  #if 0
625  std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr) << '\n';
626  #endif
627 
628  if(expr.id()==ID_symbol ||
629  expr.id()==ID_dynamic_object ||
630  expr.id()==ID_string_constant)
631  {
632  if(expr.type().id()==ID_array &&
633  expr.type().subtype().id()==ID_array)
634  insert_from(dest, expr);
635  else
636  insert_from(dest, expr, 0);
637 
638  return;
639  }
640  else if(expr.id()==ID_dereference)
641  {
642  if(expr.operands().size()!=1)
643  throw expr.id_string()+" expected to have one operand";
644 
645  get_value_set_rec(expr.op0(), dest, "", expr.op0().type(), ns);
646 
647  #if 0
648  for(expr_sett::const_iterator it=value_set.begin();
649  it!=value_set.end(); it++)
650  std::cout << "VALUE_SET: " << format(*it) << '\n';
651  #endif
652 
653  return;
654  }
655  else if(expr.id()==ID_index)
656  {
657  if(expr.operands().size()!=2)
658  throw "index expected to have two operands";
659 
660  const exprt &array=expr.op0();
661  const exprt &offset=expr.op1();
662  const typet &array_type=ns.follow(array.type());
663 
664  assert(array_type.id()==ID_array ||
665  array_type.id()==ID_incomplete_array);
666 
667 
668  object_mapt array_references;
669  get_reference_set(array, array_references, ns);
670 
671  const object_map_dt &object_map=array_references.read();
672 
673  forall_objects(a_it, object_map)
674  {
675  const exprt &object=object_numbering[a_it->first];
676 
677  if(object.id()==ID_unknown)
678  insert_from(dest, exprt(ID_unknown, expr.type()));
679  else
680  {
681  index_exprt index_expr(
682  object, from_integer(0, index_type()), expr.type());
683 
684  // adjust type?
685  if(ns.follow(object.type())!=array_type)
686  index_expr.make_typecast(array.type());
687 
688  offsett o = a_it->second;
689  mp_integer i;
690 
691  if(offset.is_zero())
692  {
693  }
694  else if(!to_integer(offset, i) && offset_is_zero(o))
695  *o = i;
696  else
697  o.reset();
698 
699  insert_from(dest, index_expr, o);
700  }
701  }
702 
703  return;
704  }
705  else if(expr.id()==ID_member)
706  {
707  const irep_idt &component_name=expr.get(ID_component_name);
708 
709  if(expr.operands().size()!=1)
710  throw "member expected to have one operand";
711 
712  const exprt &struct_op=expr.op0();
713 
714  object_mapt struct_references;
715  get_reference_set(struct_op, struct_references, ns);
716 
717  const object_map_dt &object_map=struct_references.read();
718 
719  forall_objects(it, object_map)
720  {
721  const exprt &object=object_numbering[it->first];
722  const typet &obj_type=ns.follow(object.type());
723 
724  if(object.id()==ID_unknown)
725  insert_from(dest, exprt(ID_unknown, expr.type()));
726  else if(object.id()==ID_dynamic_object &&
727  obj_type.id()!=ID_struct &&
728  obj_type.id()!=ID_union)
729  {
730  // we catch dynamic objects of the wrong type,
731  // to avoid non-integral typecasts.
732  insert_from(dest, exprt(ID_unknown, expr.type()));
733  }
734  else
735  {
736  offsett o = it->second;
737 
738  member_exprt member_expr(object, component_name, expr.type());
739 
740  // adjust type?
741  if(ns.follow(struct_op.type())!=ns.follow(object.type()))
742  member_expr.op0().make_typecast(struct_op.type());
743 
744  insert_from(dest, member_expr, o);
745  }
746  }
747 
748  return;
749  }
750  else if(expr.id()==ID_if)
751  {
752  if(expr.operands().size()!=3)
753  throw "if takes three operands";
754 
755  get_reference_set_rec(expr.op1(), dest, ns);
756  get_reference_set_rec(expr.op2(), dest, ns);
757  return;
758  }
759 
760  insert_from(dest, exprt(ID_unknown, expr.type()));
761 }
762 
764  const exprt &lhs,
765  const exprt &rhs,
766  const namespacet &ns,
767  bool add_to_sets)
768 {
769  #if 0
770  std::cout << "ASSIGN LHS: " << lhs << '\n';
771  std::cout << "ASSIGN LTYPE: " << format(ns.follow(lhs.type())) << '\n';
772  std::cout << "ASSIGN RHS: " << format(rhs) << '\n';
773  #endif
774 
775  if(rhs.id()==ID_if)
776  {
777  if(rhs.operands().size()!=3)
778  throw "if takes three operands";
779 
780  assign(lhs, rhs.op1(), ns, add_to_sets);
781  assign(lhs, rhs.op2(), ns, true);
782  return;
783  }
784 
785  const typet &type=ns.follow(lhs.type());
786 
787  if(type.id()==ID_struct ||
788  type.id()==ID_union)
789  {
790  const struct_typet &struct_type=to_struct_type(type);
791 
792  std::size_t no=0;
793 
794  for(struct_typet::componentst::const_iterator
795  c_it=struct_type.components().begin();
796  c_it!=struct_type.components().end();
797  c_it++, no++)
798  {
799  const typet &subtype=c_it->type();
800  const irep_idt &name = c_it->get_name();
801 
802  // ignore methods
803  if(subtype.id()==ID_code)
804  continue;
805 
806  member_exprt lhs_member(lhs, name, subtype);
807 
808  exprt rhs_member;
809 
810  if(rhs.id()==ID_unknown ||
811  rhs.id()==ID_invalid)
812  {
813  rhs_member=exprt(rhs.id(), subtype);
814  }
815  else
816  {
817  if(!base_type_eq(rhs.type(), type, ns))
818  throw
819  "type mismatch:\nRHS: "+rhs.type().pretty()+"\n"+
820  "LHS: "+type.pretty();
821 
822  if(rhs.id()==ID_struct ||
823  rhs.id()==ID_constant)
824  {
825  assert(no<rhs.operands().size());
826  rhs_member=rhs.operands()[no];
827  }
828  else if(rhs.id()==ID_with)
829  {
830  assert(rhs.operands().size()==3);
831 
832  // see if op1 is the member we want
833  const exprt &member_operand=rhs.op1();
834 
835  const irep_idt &component_name=
836  member_operand.get(ID_component_name);
837 
838  if(component_name==name)
839  {
840  // yes! just take op2
841  rhs_member=rhs.op2();
842  }
843  else
844  {
845  // no! do op0
846  rhs_member=exprt(ID_member, subtype);
847  rhs_member.copy_to_operands(rhs.op0());
848  rhs_member.set(ID_component_name, name);
849  }
850  }
851  else
852  {
853  rhs_member=exprt(ID_member, subtype);
854  rhs_member.copy_to_operands(rhs);
855  rhs_member.set(ID_component_name, name);
856  }
857 
858  assign(lhs_member, rhs_member, ns, add_to_sets);
859  }
860  }
861  }
862  else if(type.id()==ID_array)
863  {
864  const index_exprt lhs_index(
865  lhs, exprt(ID_unknown, index_type()), type.subtype());
866 
867  if(rhs.id()==ID_unknown ||
868  rhs.id()==ID_invalid)
869  {
870  assign(lhs_index, exprt(rhs.id(), type.subtype()), ns, add_to_sets);
871  }
872  else
873  {
874  assert(base_type_eq(rhs.type(), type, ns));
875 
876  if(rhs.id()==ID_array_of)
877  {
878  assert(rhs.operands().size()==1);
879 // std::cout << "AOF: " << rhs.op0() << '\n';
880  assign(lhs_index, rhs.op0(), ns, add_to_sets);
881  }
882  else if(rhs.id()==ID_array ||
883  rhs.id()==ID_constant)
884  {
885  forall_operands(o_it, rhs)
886  {
887  assign(lhs_index, *o_it, ns, add_to_sets);
888  }
889  }
890  else if(rhs.id()==ID_with)
891  {
892  assert(rhs.operands().size()==3);
893 
894  const index_exprt op0_index(
895  rhs.op0(), exprt(ID_unknown, index_type()), type.subtype());
896 
897  assign(lhs_index, op0_index, ns, add_to_sets);
898  assign(lhs_index, rhs.op2(), ns, true);
899  }
900  else
901  {
902  const index_exprt rhs_index(
903  rhs, exprt(ID_unknown, index_type()), type.subtype());
904  assign(lhs_index, rhs_index, ns, true);
905  }
906  }
907  }
908  else
909  {
910  // basic type
911  object_mapt values_rhs;
912 
913  get_value_set(rhs, values_rhs, ns);
914 
915  assign_rec(lhs, values_rhs, "", ns, add_to_sets);
916  }
917 }
918 
920  const exprt &lhs,
921  const object_mapt &values_rhs,
922  const std::string &suffix,
923  const namespacet &ns,
924  bool add_to_sets)
925 {
926  #if 0
927  std::cout << "ASSIGN_REC LHS: " << lhs << '\n';
928  std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
929 
930  for(object_map_dt::const_iterator it=values_rhs.read().begin();
931  it!=values_rhs.read().end(); it++)
932  std::cout << "ASSIGN_REC RHS: " << to_expr(it) << '\n';
933  #endif
934 
935  if(lhs.id()==ID_symbol)
936  {
937  const irep_idt &identifier = to_symbol_expr(lhs).get_identifier();
938 
939  if(has_prefix(id2string(identifier),
940  "value_set::dynamic_object") ||
941  has_prefix(id2string(identifier),
942  "value_set::return_value") ||
943  values.find(id2string(identifier)+suffix)!=values.end())
944  // otherwise we don't track this value
945  {
946  entryt &temp_entry = get_temporary_entry(identifier, suffix);
947 
948  if(add_to_sets)
949  {
950  entryt &state_entry = get_entry(identifier, suffix);
951  make_valid_union(temp_entry.object_map, state_entry.object_map);
952  }
953 
954  make_union(temp_entry.object_map, values_rhs);
955  }
956  }
957  else if(lhs.id()==ID_dynamic_object)
958  {
961 
962  const std::string name=
963  "value_set::dynamic_object"+
964  std::to_string(dynamic_object.get_instance());
965 
966  entryt &temp_entry = get_temporary_entry(name, suffix);
967 
968  if(add_to_sets)
969  {
970  entryt &state_entry = get_entry(name, suffix);
971  make_valid_union(temp_entry.object_map, state_entry.object_map);
972  }
973 
974  make_union(temp_entry.object_map, values_rhs);
975  }
976  else if(lhs.id()==ID_dereference)
977  {
978  if(lhs.operands().size()!=1)
979  throw lhs.id_string()+" expected to have one operand";
980 
981  object_mapt reference_set;
982  get_reference_set(lhs, reference_set, ns);
983 
984  forall_objects(it, reference_set.read())
985  {
986  const exprt &object=object_numbering[it->first];
987 
988  if(object.id()!=ID_unknown)
989  assign_rec(object, values_rhs, suffix, ns, add_to_sets);
990  }
991  }
992  else if(lhs.id()==ID_index)
993  {
994  if(lhs.operands().size()!=2)
995  throw "index expected to have two operands";
996 
997  const typet &type=ns.follow(lhs.op0().type());
998 
999  DATA_INVARIANT(type.id()==ID_array || type.id()==ID_incomplete_array,
1000  "operand 0 of index expression must be an array");
1001 
1002  assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, add_to_sets);
1003  }
1004  else if(lhs.id()==ID_member)
1005  {
1006  if(lhs.operands().size()!=1)
1007  throw "member expected to have one operand";
1008 
1009  if(lhs.op0().is_nil())
1010  return;
1011 
1012  const std::string &component_name=lhs.get_string(ID_component_name);
1013 
1014  const typet &type=ns.follow(lhs.op0().type());
1015 
1016  DATA_INVARIANT(type.id()==ID_struct ||
1017  type.id()==ID_union ||
1018  type.id()==ID_incomplete_struct ||
1019  type.id()==ID_incomplete_union,
1020  "operand 0 of member expression must be struct or union");
1021 
1022  assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
1023  ns, add_to_sets);
1024  }
1025  else if(lhs.id()=="valid_object" ||
1026  lhs.id()=="dynamic_size" ||
1027  lhs.id()=="dynamic_type")
1028  {
1029  // we ignore this here
1030  }
1031  else if(lhs.id()==ID_string_constant)
1032  {
1033  // someone writes into a string-constant
1034  // evil guy
1035  }
1036  else if(lhs.id() == ID_null_object)
1037  {
1038  // evil as well
1039  }
1040  else if(lhs.id()==ID_typecast)
1041  {
1042  const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1043 
1044  assign_rec(typecast_expr.op(), values_rhs, suffix,
1045  ns, add_to_sets);
1046  }
1047  else if(lhs.id()=="zero_string" ||
1048  lhs.id()=="is_zero_string" ||
1049  lhs.id()=="zero_string_length")
1050  {
1051  // ignore
1052  }
1053  else if(lhs.id()==ID_byte_extract_little_endian ||
1054  lhs.id()==ID_byte_extract_big_endian)
1055  {
1056  assert(lhs.operands().size()==2);
1057  assign_rec(lhs.op0(), values_rhs, suffix, ns, true);
1058  }
1059  else
1060  throw "assign NYI: `"+lhs.id_string()+"'";
1061 }
1062 
1064  const irep_idt &function,
1065  const exprt::operandst &arguments,
1066  const namespacet &ns)
1067 {
1068  const symbolt &symbol=ns.lookup(function);
1069 
1070  const code_typet &type=to_code_type(symbol.type);
1071  const code_typet::parameterst &parameter_types=type.parameters();
1072 
1073  // these first need to be assigned to dummy, temporary arguments
1074  // and only thereafter to the actuals, in order
1075  // to avoid overwriting actuals that are needed for recursive
1076  // calls
1077 
1078  // the assigned data must be valid on from!
1079  unsigned old_to_function=to_function;
1080  unsigned old_to_target_index=to_target_index;
1081 
1084 
1085  for(std::size_t i=0; i<arguments.size(); i++)
1086  {
1087  const std::string identifier="value_set::" + id2string(function) + "::" +
1088  "argument$"+std::to_string(i);
1089  add_var(identifier, "");
1090  const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1091 
1092  assign(dummy_lhs, arguments[i], ns, true);
1093 
1094  // merge it immediately, the actual assignment needs the data visible!
1095  // does this break the purpose of the dummies?
1096  make_union(values[identifier].object_map,
1097  temporary_values[identifier].object_map);
1098  }
1099 
1100  // restore
1101  to_function=old_to_function;
1102  to_target_index=old_to_target_index;
1103 
1104  // now assign to 'actual actuals'
1105 
1106  std::size_t i=0;
1107 
1108  for(code_typet::parameterst::const_iterator
1109  it=parameter_types.begin();
1110  it!=parameter_types.end();
1111  it++)
1112  {
1113  const irep_idt &identifier=it->get_identifier();
1114  if(identifier=="")
1115  continue;
1116 
1117  add_var(identifier, "");
1118 
1119  const exprt v_expr=
1120  symbol_exprt("value_set::" + id2string(function) + "::" +
1121  "argument$"+std::to_string(i), it->type());
1122 
1123  const symbol_exprt actual_lhs(identifier, it->type());
1124  assign(actual_lhs, v_expr, ns, true);
1125  i++;
1126  }
1127 }
1128 
1130  const exprt &lhs,
1131  const namespacet &ns)
1132 {
1133  if(lhs.is_nil())
1134  return;
1135 
1136  irep_idt rvs = std::string("value_set::return_value") +
1138  add_var(rvs, "");
1139  symbol_exprt rhs(rvs, lhs.type());
1140 
1141  assign(lhs, rhs, ns);
1142 }
1143 
1145  const exprt &code,
1146  const namespacet &ns)
1147 {
1148  const irep_idt &statement=code.get(ID_statement);
1149 
1150  if(statement==ID_block)
1151  {
1152  forall_operands(it, code)
1153  apply_code(*it, ns);
1154  }
1155  else if(statement==ID_function_call)
1156  {
1157  // shouldn't be here
1158  UNREACHABLE;
1159  }
1160  else if(statement==ID_assign)
1161  {
1162  if(code.operands().size()!=2)
1163  throw "assignment expected to have two operands";
1164 
1165  assign(code.op0(), code.op1(), ns);
1166  }
1167  else if(statement==ID_decl)
1168  {
1169  if(code.operands().size()!=1)
1170  throw "decl expected to have one operand";
1171 
1172  const exprt &lhs=code.op0();
1173 
1174  if(lhs.id()!=ID_symbol)
1175  throw "decl expected to have symbol on lhs";
1176 
1177  assign(lhs, exprt(ID_invalid, lhs.type()), ns);
1178  }
1179  else if(statement==ID_expression)
1180  {
1181  // can be ignored, we don't expect side effects here
1182  }
1183  else if(statement==ID_cpp_delete ||
1184  statement==ID_cpp_delete_array)
1185  {
1186  // does nothing
1187  }
1188  else if(statement=="lock" || statement=="unlock")
1189  {
1190  // ignore for now
1191  }
1192  else if(statement==ID_asm)
1193  {
1194  // ignore for now, probably not safe
1195  }
1196  else if(statement==ID_nondet)
1197  {
1198  // doesn't do anything
1199  }
1200  else if(statement==ID_printf)
1201  {
1202  // doesn't do anything
1203  }
1204  else if(statement==ID_return)
1205  {
1206  // this is turned into an assignment
1207  if(code.operands().size()==1)
1208  {
1209  irep_idt rvs = std::string("value_set::return_value") +
1211  add_var(rvs, "");
1212  symbol_exprt lhs(rvs, code.op0().type());
1213  assign(lhs, code.op0(), ns);
1214  }
1215  }
1216  else if(statement==ID_input || statement==ID_output)
1217  {
1218  // doesn't do anything
1219  }
1220  else
1221  {
1222  throw
1223  code.pretty()+"\n"+
1224  "value_set_fivrnst: unexpected statement: "+id2string(statement);
1225  }
1226 }
1227 
1229  object_mapt &dest,
1231  const offsett &offset) const
1232 {
1233  object_map_dt &map = dest.write();
1234  if(map.find(n)==map.end())
1235  {
1236  // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1237  // new
1238  map[n] = offset;
1240  return true;
1241  }
1242  else
1243  {
1244  // std::cout << "UPD " << n << '\n';
1245  offsett &old_offset = map[n];
1246 
1247  bool res = map.set_valid_at(n, to_function, to_target_index);
1248 
1249  if(old_offset && offset)
1250  {
1251  if(*old_offset == *offset)
1252  return res;
1253  else
1254  {
1255  old_offset.reset();
1256  return true;
1257  }
1258  }
1259  else if(!old_offset)
1260  return res;
1261  else
1262  {
1263  old_offset.reset();
1264  return true;
1265  }
1266  }
1267 }
1268 
1270  object_mapt &dest,
1272  const offsett &offset) const
1273 {
1274  object_map_dt &map = dest.write();
1275  if(map.find(n)==map.end())
1276  {
1277  // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1278  // new
1279  map[n] = offset;
1281  return true;
1282  }
1283  else
1284  {
1285  // std::cout << "UPD " << n << '\n';
1286  offsett &old_offset = map[n];
1287 
1288  bool res = map.set_valid_at(n, from_function, from_target_index);
1289 
1290  if(old_offset && offset)
1291  {
1292  if(*old_offset == *offset)
1293  return res;
1294  else
1295  {
1296  old_offset.reset();
1297  return true;
1298  }
1299  }
1300  else if(!old_offset)
1301  return res;
1302  else
1303  {
1304  old_offset.reset();
1305  return true;
1306  }
1307  }
1308 }
1309 
1311  unsigned inx,
1312  unsigned f,
1313  unsigned line)
1314 {
1315  if(is_valid_at(inx, f, line))
1316  return false;
1317 
1318  vrange_listt &ranges = validity_ranges[inx];
1319  vrange_listt::iterator it=ranges.begin();
1320 
1321  while(it->function!=f && it!=ranges.end()) it++; // ffw to function block
1322 
1323  for(;
1324  it!=ranges.end() && it->function==f && it->from <= line;
1325  it++)
1326  {
1327  if(it->function==f)
1328  {
1329  if( line == it->to+1)
1330  {
1331  it->to++;
1332 
1333  // by any chance: does the next one connect to this one?
1334  vrange_listt::iterator n_it = it; n_it++;
1335  if(n_it!=ranges.end() &&
1336  it->function == n_it->function &&
1337  it->to+1 == n_it->from)
1338  {
1339  n_it->from = it->from; // connected!
1340  it = ranges.erase(it);
1341  }
1342  return true;
1343  }
1344  }
1345  }
1346 
1347  // it now points to either the end,
1348  // the first of a new function block,or
1349  // the first one that has from > line
1350  if(it!=ranges.end())
1351  {
1352  if(it->function==f)
1353  {
1354  if( line == it->from - 1)
1355  {
1356  it->from--;
1357 
1358  // by any chance: does the previous one connect to this one?
1359  if(it!=ranges.begin())
1360  {
1361  vrange_listt::iterator p_it = it; p_it--;
1362  if(p_it->function == it->function &&
1363  p_it->to+1 == it->from)
1364  {
1365  p_it->to = it->to; // connected!
1366  it = ranges.erase(it);
1367  }
1368  }
1369  return true;
1370  }
1371  }
1372  }
1373 
1374  // none matched
1375  validity_ranget insr(f, line, line);
1376  ranges.insert(it, insr);
1377 
1378  return true;
1379 }
1380 
1382  unsigned inx,
1383  unsigned f,
1384  unsigned line) const
1385 {
1386  #if 0
1387  std::cout << "IS_VALID_AT: " << inx << ", " << f << ", line " << line <<
1388  '\n';
1389  #endif
1390 
1391  validity_rangest::const_iterator vrs = validity_ranges.find(inx);
1392  if(vrs!=validity_ranges.end())
1393  {
1394  const vrange_listt &ranges = vrs->second;
1395 
1396  object_map_dt::vrange_listt::const_iterator it = ranges.begin();
1397 
1398  while(it->function!=f &&
1399  it!=ranges.end())
1400  it++; // ffw to function block
1401 
1402  for( ;
1403  it!=ranges.end() && it->function==f && it->from<=line;
1404  it++)
1405  if(it->contains(f, line))
1406  return true;
1407  }
1408 
1409  return false;
1410 }
1411 
1413 {
1414  bool changed=false;
1415 
1416  for(valuest::iterator it=values.begin();
1417  it!=values.end();
1418  it++)
1419  {
1420  object_mapt &state_map=it->second.object_map;
1421 
1422  irep_idt ident = id2string(it->second.identifier)+it->second.suffix;
1423 
1424  valuest::const_iterator t_it=temporary_values.find(ident);
1425 
1426  if(t_it==temporary_values.end())
1427  {
1428 // std::cout << "OLD VALUES FOR: " << ident << '\n';
1429  Forall_valid_objects(o_it, state_map.write())
1430  {
1431 // std::cout << "STILL VALID: " << to_expr(o_it) << '\n';
1432  if(state_map.write().set_valid_at(o_it->first,
1434  changed = true;
1435  }
1436  }
1437  else
1438  {
1439 // std::cout << "NEW VALUES FOR: " << ident << '\n';
1440  if(make_union(state_map, t_it->second.object_map))
1441  changed = true;
1442  }
1443  }
1444 
1445  temporary_values.clear();
1446 
1447  return changed;
1448 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
exprt::op2
exprt & op2()
Definition: expr.h:90
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
format
static format_containert< T > format(const T &o)
Definition: format.h:35
typet::subtype
const typet & subtype() const
Definition: type.h:38
value_set_fivrnst::assign
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
Definition: value_set_fivrns.cpp:763
value_set_fivrnst::output
void output(const namespacet &ns, std::ostream &out) const
Definition: value_set_fivrns.cpp:57
to_integer
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
value_set_fivrnst::to_expr
exprt to_expr(object_map_dt::const_iterator it) const
Definition: value_set_fivrns.cpp:202
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
value_set_fivrnst::add_var
void add_var(const idt &id, const std::string &suffix)
Definition: value_set_fivrns.h:242
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
value_set_fivrnst::object_map_dt::set_valid_at
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
Definition: value_set_fivrns.cpp:1310
value_set_fivrnst::object_map_dt::begin
iterator begin()
Definition: value_set_fivrns.h:80
value_set_fivrnst::values
valuest values
Definition: value_set_fivrns.h:291
symbolt::display_name
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
typet
The type of an expression, extends irept.
Definition: type.h:27
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
value_set_fivrnst::do_function_call
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Definition: value_set_fivrns.cpp:1063
value_set_fivrnst::get_reference_set_rec
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
Definition: value_set_fivrns.cpp:619
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dynamic_object_exprt
Representation of heap-allocated objects.
Definition: std_expr.h:2208
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
template_numberingt
Definition: numbering.h:21
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2136
value_set_fivrnst::to_target_index
unsigned to_target_index
Definition: value_set_fivrns.h:36
prefix.h
value_set_fivrnst::expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: value_set_fivrns.h:218
value_set_fivrnst::from_target_index
unsigned from_target_index
Definition: value_set_fivrns.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
from_type
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
Definition: language_util.cpp:33
exprt::op0
exprt & op0()
Definition: expr.h:84
value_set_fivrnst::handover
bool handover()
Definition: value_set_fivrns.cpp:1412
value_set_fivrns.h
value_set_fivrnst::apply_code
void apply_code(const exprt &code, const namespacet &ns)
Definition: value_set_fivrns.cpp:1144
value_set_fivrnst::entryt::suffix
std::string suffix
Definition: value_set_fivrns.h:207
value_set_fivrnst::assign_rec
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_fivrns.cpp:919
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
dynamic_object
exprt dynamic_object(const exprt &pointer)
Definition: pointer_predicates.cpp:71
value_set_fivrnst::offsett
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
Definition: value_set_fivrns.h:56
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
reference_counting::read
const T & read() const
Definition: reference_counting.h:67
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
value_set_fivrnst::get_value_set
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
Definition: value_set_fivrns.cpp:266
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
value_set_fivrnst::insert_from
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set_fivrns.h:173
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
alloc_adapter_prefix
static const char * alloc_adapter_prefix
Definition: value_set_fivrns.cpp:33
base_type.h
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
value_set_fivrnst::get_reference_set
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
Definition: value_set_fivrns.cpp:607
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
language_util.h
value_set_fivrnst::object_map_dt::empty
bool empty() const
Definition: value_set_fivrns.h:85
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
value_set_fivrnst::entryt::object_map
object_mapt object_map
Definition: value_set_fivrns.h:205
value_set_fivrnst::object_map_dt::vrange_listt
std::list< validity_ranget > vrange_listt
Definition: value_set_fivrns.h:127
irept::id_string
const std::string & id_string() const
Definition: irep.h:262
value_set_fivrnst::object_map_dt::find
const_iterator find(object_numberingt::number_type k)
Definition: value_set_fivrns.h:76
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2320
exprt::op1
exprt & op1()
Definition: expr.h:87
value_set_fivrnst::make_valid_union
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
Definition: value_set_fivrns.cpp:237
value_set_fivrnst::object_map_dt::validity_ranges
validity_rangest validity_ranges
Definition: value_set_fivrns.h:129
reference_counting::write
T & write()
Definition: reference_counting.h:74
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
code_typet
Base type of functions.
Definition: std_types.h:751
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
value_set_fivrnst::object_map_dt::is_valid_at
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
Definition: value_set_fivrns.cpp:1381
value_set_fivrnst::to_function
unsigned to_function
Definition: value_set_fivrns.h:35
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
to_dynamic_object_expr
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: std_expr.h:2245
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
forall_objects
#define forall_objects(it, map)
Definition: value_set_fivrns.cpp:35
reference_counting< object_map_dt >
std_code.h
value_set_fivrnst::function_numbering
static hash_numbering< irep_idt, irep_id_hash > function_numbering
Definition: value_set_fivrns.h:38
forall_valid_objects
#define forall_valid_objects(it, map)
Definition: value_set_fivrns.cpp:40
value_set_fivrnst::object_map_dt::const_iterator
objmapt::const_iterator const_iterator
Definition: value_set_fivrns.h:72
value_set_fivrnst::object_map_dt::blank
static const object_map_dt blank
Definition: value_set_fivrns.h:66
Forall_valid_objects
#define Forall_valid_objects(it, map)
Definition: value_set_fivrns.cpp:51
simplify_expr.h
value_set_fivrnst::make_union
bool make_union(object_mapt &dest, const object_mapt &src) const
Definition: value_set_fivrns.cpp:222
value_set_fivrnst::insert_to
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set_fivrns.h:144
value_set_fivrnst::object_map_dt
Definition: value_set_fivrns.h:62
value_set_fivrnst::copy_objects
void copy_objects(object_mapt &dest, const object_mapt &src) const
Definition: value_set_fivrns.cpp:252
template_numberingt::number_type
typename Map::mapped_type number_type
Definition: numbering.h:24
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
value_set_fivrnst::dereference_rec
void dereference_rec(const exprt &src, exprt &dest) const
Definition: value_set_fivrns.cpp:589
value_set_fivrnst::do_end_function
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition: value_set_fivrns.cpp:1129
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
value_set_fivrnst::from_function
unsigned from_function
Definition: value_set_fivrns.h:35
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
value_set_fivrnst::object_map_dt::validity_ranget
Definition: value_set_fivrns.h:105
value_set_fivrnst::entryt::identifier
idt identifier
Definition: value_set_fivrns.h:206
value_set_fivrnst::get_value_set_rec
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_fivrns.cpp:295
value_set_fivrnst::get_temporary_entry
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
Definition: value_set_fivrns.h:267
value_set_fivrnst::temporary_values
valuest temporary_values
Definition: value_set_fivrns.h:292
value_set_fivrnst::object_map_dt::end
iterator end()
Definition: value_set_fivrns.h:82
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
value_set_fivrnst::entryt
Definition: value_set_fivrns.h:203
exprt::operands
operandst & operands()
Definition: expr.h:78
value_set_fivrnst::offset_is_zero
bool offset_is_zero(offsett offset) const
Definition: value_set_fivrns.h:57
value_set_fivrnst::object_numbering
static object_numberingt object_numbering
Definition: value_set_fivrns.h:37
index_exprt
Array index operator.
Definition: std_expr.h:1595
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
symbol_table.h
Author: Diffblue Ltd.
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
object_descriptor_exprt::object
exprt & object()
Definition: std_expr.h:2147
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
value_set_fivrnst::output_entry
void output_entry(const entryt &e, const namespacet &ns, std::ostream &out) const
Definition: value_set_fivrns.cpp:68
std_expr.h
value_set_fivrnst::get_entry
entryt & get_entry(const idt &id, const std::string &suffix)
Definition: value_set_fivrns.h:252
c_types.h
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:2159
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106