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.offset_is_set)
138  result+=integer2string(o_it->second.offset)+"";
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.offset_is_set)
215  od.offset()=from_integer(it->second.offset, index_type());
216 
217  od.type()=od.object().type();
218 
219  return 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: " << from_expr(ns, "", *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  assert(type.id()==ID_array ||
320  type.id()==ID_incomplete_array);
321 
322  get_value_set_rec(expr.op0(), dest, "[]"+suffix, original_type, ns);
323 
324  return;
325  }
326  else if(expr.id()==ID_member)
327  {
328  assert(expr.operands().size()==1);
329 
330  if(expr.op0().is_not_nil())
331  {
332  const typet &type=ns.follow(expr.op0().type());
333 
334  assert(type.id()==ID_struct ||
335  type.id()==ID_union ||
336  type.id()==ID_incomplete_struct ||
337  type.id()==ID_incomplete_union);
338 
339  const std::string &component_name=
340  expr.get_string(ID_component_name);
341 
342  get_value_set_rec(expr.op0(), dest, "."+component_name+suffix,
343  original_type, ns);
344 
345  return;
346  }
347  }
348  else if(expr.id()==ID_symbol)
349  {
350  // just keep a reference to the ident in the set
351  // (if it exists)
352  irep_idt ident = expr.get_string(ID_identifier)+suffix;
353 
355  {
356  insert_from(dest, expr, 0);
357  return;
358  }
359  else
360  {
361  valuest::const_iterator v_it=values.find(ident);
362 
363  if(v_it!=values.end())
364  {
365  copy_objects(dest, v_it->second.object_map);
366  return;
367  }
368  }
369  }
370  else if(expr.id()==ID_if)
371  {
372  if(expr.operands().size()!=3)
373  throw "if takes three operands";
374 
375  get_value_set_rec(expr.op1(), dest, suffix,
376  original_type, ns);
377  get_value_set_rec(expr.op2(), dest, suffix,
378  original_type, ns);
379 
380  return;
381  }
382  else if(expr.id()==ID_address_of)
383  {
384  if(expr.operands().size()!=1)
385  throw expr.id_string()+" expected to have one operand";
386 
387  get_reference_set(expr.op0(), dest, ns);
388 
389  return;
390  }
391  else if(expr.id()==ID_dereference)
392  {
393  object_mapt reference_set;
394  get_reference_set(expr, reference_set, ns);
395  const object_map_dt &object_map=reference_set.read();
396 
397  if(object_map.begin()!=object_map.end())
398  {
399  forall_objects(it1, object_map)
400  {
401  const exprt &object=object_numbering[it1->first];
402  get_value_set_rec(object, dest, suffix,
403  original_type, ns);
404  }
405 
406  return;
407  }
408  }
409  else if(expr.id()=="reference_to")
410  {
411  object_mapt reference_set;
412 
413  get_reference_set(expr, reference_set, ns);
414 
415  const object_map_dt &object_map=reference_set.read();
416 
417  if(object_map.begin()!=object_map.end())
418  {
419  forall_objects(it, object_map)
420  {
421  const exprt &object=object_numbering[it->first];
422  get_value_set_rec(object, dest, suffix,
423  original_type, ns);
424  }
425 
426  return;
427  }
428  }
429  else if(expr.is_constant())
430  {
431  // check if NULL
432  if(expr.get(ID_value)==ID_NULL &&
433  expr.type().id()==ID_pointer)
434  {
435  insert_from(dest, exprt("NULL-object", expr.type().subtype()), 0);
436  return;
437  }
438  }
439  else if(expr.id()==ID_typecast)
440  {
441  if(expr.operands().size()!=1)
442  throw "typecast takes one operand";
443 
444  get_value_set_rec(expr.op0(), dest, suffix,
445  original_type, ns);
446 
447  return;
448  }
449  else if(expr.id()==ID_plus || expr.id()==ID_minus)
450  {
451  if(expr.operands().size()<2)
452  throw expr.id_string()+" expected to have at least two operands";
453 
454  if(expr.type().id()==ID_pointer)
455  {
456  // find the pointer operand
457  const exprt *ptr_operand=nullptr;
458 
459  forall_operands(it, expr)
460  if(it->type().id()==ID_pointer)
461  {
462  if(ptr_operand==nullptr)
463  ptr_operand=&(*it);
464  else
465  throw "more than one pointer operand in pointer arithmetic";
466  }
467 
468  if(ptr_operand==nullptr)
469  throw "pointer type sum expected to have pointer operand";
470 
471  object_mapt pointer_expr_set;
472  get_value_set_rec(*ptr_operand, pointer_expr_set, "",
473  ptr_operand->type(), ns);
474 
475  forall_objects(it, pointer_expr_set.read())
476  {
477  objectt object=it->second;
478 
479  if(object.offset_is_zero() &&
480  expr.operands().size()==2)
481  {
482  if(expr.op0().type().id()!=ID_pointer)
483  {
484  mp_integer i;
485  if(to_integer(expr.op0(), i))
486  object.offset_is_set=false;
487  else
488  object.offset=(expr.id()==ID_plus)? i : -i;
489  }
490  else
491  {
492  mp_integer i;
493  if(to_integer(expr.op1(), i))
494  object.offset_is_set=false;
495  else
496  object.offset=(expr.id()==ID_plus)? i : -i;
497  }
498  }
499  else
500  object.offset_is_set=false;
501 
502  insert_from(dest, it->first, object);
503  }
504 
505  return;
506  }
507  }
508  else if(expr.id()==ID_side_effect)
509  {
510  const irep_idt &statement=expr.get(ID_statement);
511 
512  if(statement==ID_function_call)
513  {
514  // these should be gone
515  throw "unexpected function_call sideeffect";
516  }
517  else if(statement==ID_malloc)
518  {
519  if(expr.type().id()!=ID_pointer)
520  throw "malloc expected to return pointer type";
521 
522  assert(suffix=="");
523 
524  const typet &dynamic_type=
525  static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
526 
527  dynamic_object_exprt dynamic_object(dynamic_type);
528  // let's make up a `unique' number for this object...
529  dynamic_object.set_instance(
530  (from_function << 16) | from_target_index);
531  dynamic_object.valid()=true_exprt();
532 
533  insert_from(dest, dynamic_object, 0);
534  return;
535  }
536  else if(statement==ID_cpp_new ||
537  statement==ID_cpp_new_array)
538  {
539  assert(suffix=="");
540  assert(expr.type().id()==ID_pointer);
541 
542  dynamic_object_exprt dynamic_object(expr.type().subtype());
543  // let's make up a unique number for this object...
544  dynamic_object.set_instance(
545  (from_function << 16) | from_target_index);
546  dynamic_object.valid()=true_exprt();
547 
548  insert_from(dest, dynamic_object, 0);
549  return;
550  }
551  }
552  else if(expr.id()==ID_struct)
553  {
554  // this is like a static struct object
555  insert_from(dest, address_of_exprt(expr), 0);
556  return;
557  }
558  else if(expr.id()==ID_with ||
559  expr.id()==ID_array_of ||
560  expr.id()==ID_array)
561  {
562  // these are supposed to be done by assign()
563  throw "unexpected value in get_value_set: "+expr.id_string();
564  }
565  else if(expr.id()==ID_dynamic_object)
566  {
569 
570  const std::string name=
571  "value_set::dynamic_object"+
572  std::to_string(dynamic_object.get_instance())+
573  suffix;
574 
575  // look it up
576  valuest::const_iterator v_it=values.find(name);
577 
578  if(v_it!=values.end())
579  {
580  copy_objects(dest, v_it->second.object_map);
581  return;
582  }
583  }
584 
585  insert_from(dest, exprt(ID_unknown, original_type));
586 }
587 
589  const exprt &src,
590  exprt &dest) const
591 {
592  // remove pointer typecasts
593  if(src.id()==ID_typecast)
594  {
595  assert(src.type().id()==ID_pointer);
596 
597  if(src.operands().size()!=1)
598  throw "typecast expects one operand";
599 
600  dereference_rec(src.op0(), dest);
601  }
602  else
603  dest=src;
604 }
605 
607  const exprt &expr,
608  expr_sett &dest,
609  const namespacet &ns) const
610 {
611  object_mapt object_map;
612  get_reference_set(expr, object_map, ns);
613 
614  forall_objects(it, object_map.read())
615  dest.insert(to_expr(it));
616 }
617 
619  const exprt &expr,
620  object_mapt &dest,
621  const namespacet &ns) const
622 {
623  #if 0
624  std::cout << "GET_REFERENCE_SET_REC EXPR: " << from_expr(ns, "", expr)
625  << '\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: " << from_expr(ns, "", *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  exprt index_expr(ID_index, expr.type());
682  index_expr.operands().resize(2);
683  index_expr.op0()=object;
684  index_expr.op1()=from_integer(0, index_type());
685 
686  // adjust type?
687  if(ns.follow(object.type())!=array_type)
688  index_expr.make_typecast(array.type());
689 
690  objectt o=a_it->second;
691  mp_integer i;
692 
693  if(offset.is_zero())
694  {
695  }
696  else if(!to_integer(offset, i) &&
697  o.offset_is_zero())
698  o.offset=i;
699  else
700  o.offset_is_set=false;
701 
702  insert_from(dest, index_expr, o);
703  }
704  }
705 
706  return;
707  }
708  else if(expr.id()==ID_member)
709  {
710  const irep_idt &component_name=expr.get(ID_component_name);
711 
712  if(expr.operands().size()!=1)
713  throw "member expected to have one operand";
714 
715  const exprt &struct_op=expr.op0();
716 
717  object_mapt struct_references;
718  get_reference_set(struct_op, struct_references, ns);
719 
720  const object_map_dt &object_map=struct_references.read();
721 
722  forall_objects(it, object_map)
723  {
724  const exprt &object=object_numbering[it->first];
725  const typet &obj_type=ns.follow(object.type());
726 
727  if(object.id()==ID_unknown)
728  insert_from(dest, exprt(ID_unknown, expr.type()));
729  else if(object.id()==ID_dynamic_object &&
730  obj_type.id()!=ID_struct &&
731  obj_type.id()!=ID_union)
732  {
733  // we catch dynamic objects of the wrong type,
734  // to avoid non-integral typecasts.
735  insert_from(dest, exprt(ID_unknown, expr.type()));
736  }
737  else
738  {
739  objectt o=it->second;
740 
741  exprt member_expr(ID_member, expr.type());
742  member_expr.copy_to_operands(object);
743  member_expr.set(ID_component_name, component_name);
744 
745  // adjust type?
746  if(ns.follow(struct_op.type())!=ns.follow(object.type()))
747  member_expr.op0().make_typecast(struct_op.type());
748 
749  insert_from(dest, member_expr, o);
750  }
751  }
752 
753  return;
754  }
755  else if(expr.id()==ID_if)
756  {
757  if(expr.operands().size()!=3)
758  throw "if takes three operands";
759 
760  get_reference_set_rec(expr.op1(), dest, ns);
761  get_reference_set_rec(expr.op2(), dest, ns);
762  return;
763  }
764 
765  insert_from(dest, exprt(ID_unknown, expr.type()));
766 }
767 
769  const exprt &lhs,
770  const exprt &rhs,
771  const namespacet &ns,
772  bool add_to_sets)
773 {
774  #if 0
775  std::cout << "ASSIGN LHS: " << lhs << '\n';
776  std::cout << "ASSIGN LTYPE: " << ns.follow(lhs.type()) << '\n';
777  std::cout << "ASSIGN RHS: " << from_expr(ns, "", rhs) << '\n';
778  #endif
779 
780  if(rhs.id()==ID_if)
781  {
782  if(rhs.operands().size()!=3)
783  throw "if takes three operands";
784 
785  assign(lhs, rhs.op1(), ns, add_to_sets);
786  assign(lhs, rhs.op2(), ns, true);
787  return;
788  }
789 
790  const typet &type=ns.follow(lhs.type());
791 
792  if(type.id()==ID_struct ||
793  type.id()==ID_union)
794  {
795  const struct_typet &struct_type=to_struct_type(type);
796 
797  unsigned no=0;
798 
799  for(struct_typet::componentst::const_iterator
800  c_it=struct_type.components().begin();
801  c_it!=struct_type.components().end();
802  c_it++, no++)
803  {
804  const typet &subtype=c_it->type();
805  const irep_idt &name=c_it->get(ID_name);
806 
807  // ignore methods
808  if(subtype.id()==ID_code)
809  continue;
810 
811  exprt lhs_member(ID_member, subtype);
812  lhs_member.set(ID_component_name, name);
813  lhs_member.copy_to_operands(lhs);
814 
815  exprt rhs_member;
816 
817  if(rhs.id()==ID_unknown ||
818  rhs.id()==ID_invalid)
819  {
820  rhs_member=exprt(rhs.id(), subtype);
821  }
822  else
823  {
824  if(!base_type_eq(rhs.type(), type, ns))
825  throw
826  "type mismatch:\nRHS: "+rhs.type().pretty()+"\n"+
827  "LHS: "+type.pretty();
828 
829  if(rhs.id()==ID_struct ||
830  rhs.id()==ID_constant)
831  {
832  assert(no<rhs.operands().size());
833  rhs_member=rhs.operands()[no];
834  }
835  else if(rhs.id()==ID_with)
836  {
837  assert(rhs.operands().size()==3);
838 
839  // see if op1 is the member we want
840  const exprt &member_operand=rhs.op1();
841 
842  const irep_idt &component_name=
843  member_operand.get(ID_component_name);
844 
845  if(component_name==name)
846  {
847  // yes! just take op2
848  rhs_member=rhs.op2();
849  }
850  else
851  {
852  // no! do op0
853  rhs_member=exprt(ID_member, subtype);
854  rhs_member.copy_to_operands(rhs.op0());
855  rhs_member.set(ID_component_name, name);
856  }
857  }
858  else
859  {
860  rhs_member=exprt(ID_member, subtype);
861  rhs_member.copy_to_operands(rhs);
862  rhs_member.set(ID_component_name, name);
863  }
864 
865  assign(lhs_member, rhs_member, ns, add_to_sets);
866  }
867  }
868  }
869  else if(type.id()==ID_array)
870  {
871  exprt lhs_index(ID_index, type.subtype());
872  lhs_index.copy_to_operands(lhs, exprt(ID_unknown, index_type()));
873 
874  if(rhs.id()==ID_unknown ||
875  rhs.id()==ID_invalid)
876  {
877  assign(lhs_index, exprt(rhs.id(), type.subtype()), ns, add_to_sets);
878  }
879  else
880  {
881  assert(base_type_eq(rhs.type(), type, ns));
882 
883  if(rhs.id()==ID_array_of)
884  {
885  assert(rhs.operands().size()==1);
886 // std::cout << "AOF: " << rhs.op0() << '\n';
887  assign(lhs_index, rhs.op0(), ns, add_to_sets);
888  }
889  else if(rhs.id()==ID_array ||
890  rhs.id()==ID_constant)
891  {
892  forall_operands(o_it, rhs)
893  {
894  assign(lhs_index, *o_it, ns, add_to_sets);
895  }
896  }
897  else if(rhs.id()==ID_with)
898  {
899  assert(rhs.operands().size()==3);
900 
901  exprt op0_index(ID_index, type.subtype());
902  op0_index.copy_to_operands(rhs.op0(), exprt(ID_unknown, index_type()));
903 
904  assign(lhs_index, op0_index, ns, add_to_sets);
905  assign(lhs_index, rhs.op2(), ns, true);
906  }
907  else
908  {
909  exprt rhs_index(ID_index, type.subtype());
910  rhs_index.copy_to_operands(rhs, exprt(ID_unknown, index_type()));
911  assign(lhs_index, rhs_index, ns, true);
912  }
913  }
914  }
915  else
916  {
917  // basic type
918  object_mapt values_rhs;
919 
920  get_value_set(rhs, values_rhs, ns);
921 
922  assign_rec(lhs, values_rhs, "", ns, add_to_sets);
923  }
924 }
925 
927  const exprt &op,
928  const namespacet &ns)
929 {
930  // op must be a pointer
931  if(op.type().id()!=ID_pointer)
932  throw "free expected to have pointer-type operand";
933 
934  // find out what it points to
935  object_mapt value_set;
936  get_value_set(op, value_set, ns);
937 
938  const object_map_dt &object_map=value_set.read();
939 
940  // find out which *instances* interest us
941  dynamic_object_id_sett to_mark;
942 
943  forall_objects(it, object_map)
944  {
945  const exprt &object=object_numbering[it->first];
946 
947  if(object.id()==ID_dynamic_object)
948  {
950  to_dynamic_object_expr(object);
951 
952  if(dynamic_object.valid().is_true())
953  to_mark.insert(dynamic_object.get_instance());
954  }
955  }
956 
957  // mark these as 'may be invalid'
958  // this, unfortunately, destroys the sharing
959  for(valuest::iterator v_it=values.begin();
960  v_it!=values.end();
961  v_it++)
962  {
963  object_mapt new_object_map;
964 
965  const object_map_dt &old_object_map=
966  v_it->second.object_map.read();
967 
968  bool changed=false;
969 
970  forall_valid_objects(o_it, old_object_map)
971  {
972  const exprt &object=object_numbering[o_it->first];
973 
974  if(object.id()==ID_dynamic_object)
975  {
977  to_dynamic_object_expr(object);
978 
979  if(to_mark.count(dynamic_object.get_instance())==0)
980  set(new_object_map, o_it);
981  else
982  {
983  // adjust
984  objectt o=o_it->second;
985  exprt tmp(object);
986  to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
987  insert_to(new_object_map, tmp, o);
988  changed=true;
989  }
990  }
991  else
992  set(new_object_map, o_it);
993  }
994 
995  if(changed)
996  {
997  entryt &temp_entry = get_temporary_entry(v_it->second.identifier,
998  v_it->second.suffix);
999  temp_entry.object_map=new_object_map;
1000  }
1001  }
1002 }
1003 
1005  const exprt &lhs,
1006  const object_mapt &values_rhs,
1007  const std::string &suffix,
1008  const namespacet &ns,
1009  bool add_to_sets)
1010 {
1011  #if 0
1012  std::cout << "ASSIGN_REC LHS: " << lhs << '\n';
1013  std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1014 
1015  for(object_map_dt::const_iterator it=values_rhs.read().begin();
1016  it!=values_rhs.read().end(); it++)
1017  std::cout << "ASSIGN_REC RHS: " << to_expr(it) << '\n';
1018  #endif
1019 
1020  if(lhs.id()==ID_symbol)
1021  {
1022  const irep_idt &identifier=lhs.get(ID_identifier);
1023 
1024  if(has_prefix(id2string(identifier),
1025  "value_set::dynamic_object") ||
1026  has_prefix(id2string(identifier),
1027  "value_set::return_value") ||
1028  values.find(id2string(identifier)+suffix)!=values.end())
1029  // otherwise we don't track this value
1030  {
1031  entryt &temp_entry = get_temporary_entry(identifier, suffix);
1032 
1033  if(add_to_sets)
1034  {
1035  entryt &state_entry = get_entry(identifier, suffix);
1036  make_valid_union(temp_entry.object_map, state_entry.object_map);
1037  }
1038 
1039  make_union(temp_entry.object_map, values_rhs);
1040  }
1041  }
1042  else if(lhs.id()==ID_dynamic_object)
1043  {
1046 
1047  const std::string name=
1048  "value_set::dynamic_object"+
1049  std::to_string(dynamic_object.get_instance());
1050 
1051  entryt &temp_entry = get_temporary_entry(name, suffix);
1052 
1053  if(add_to_sets)
1054  {
1055  entryt &state_entry = get_entry(name, suffix);
1056  make_valid_union(temp_entry.object_map, state_entry.object_map);
1057  }
1058 
1059  make_union(temp_entry.object_map, values_rhs);
1060  }
1061  else if(lhs.id()==ID_dereference)
1062  {
1063  if(lhs.operands().size()!=1)
1064  throw lhs.id_string()+" expected to have one operand";
1065 
1066  object_mapt reference_set;
1067  get_reference_set(lhs, reference_set, ns);
1068 
1069  forall_objects(it, reference_set.read())
1070  {
1071  const exprt &object=object_numbering[it->first];
1072 
1073  if(object.id()!=ID_unknown)
1074  assign_rec(object, values_rhs, suffix, ns, add_to_sets);
1075  }
1076  }
1077  else if(lhs.id()==ID_index)
1078  {
1079  if(lhs.operands().size()!=2)
1080  throw "index expected to have two operands";
1081 
1082  const typet &type=ns.follow(lhs.op0().type());
1083 
1084  assert(type.id()==ID_array || type.id()==ID_incomplete_array);
1085 
1086  assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, add_to_sets);
1087  }
1088  else if(lhs.id()==ID_member)
1089  {
1090  if(lhs.operands().size()!=1)
1091  throw "member expected to have one operand";
1092 
1093  if(lhs.op0().is_nil())
1094  return;
1095 
1096  const std::string &component_name=lhs.get_string(ID_component_name);
1097 
1098  const typet &type=ns.follow(lhs.op0().type());
1099 
1100  assert(type.id()==ID_struct ||
1101  type.id()==ID_union ||
1102  type.id()==ID_incomplete_struct ||
1103  type.id()==ID_incomplete_union);
1104 
1105  assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
1106  ns, add_to_sets);
1107  }
1108  else if(lhs.id()=="valid_object" ||
1109  lhs.id()=="dynamic_size" ||
1110  lhs.id()=="dynamic_type")
1111  {
1112  // we ignore this here
1113  }
1114  else if(lhs.id()==ID_string_constant)
1115  {
1116  // someone writes into a string-constant
1117  // evil guy
1118  }
1119  else if(lhs.id()=="NULL-object")
1120  {
1121  // evil as well
1122  }
1123  else if(lhs.id()==ID_typecast)
1124  {
1125  const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1126 
1127  assign_rec(typecast_expr.op(), values_rhs, suffix,
1128  ns, add_to_sets);
1129  }
1130  else if(lhs.id()=="zero_string" ||
1131  lhs.id()=="is_zero_string" ||
1132  lhs.id()=="zero_string_length")
1133  {
1134  // ignore
1135  }
1136  else if(lhs.id()==ID_byte_extract_little_endian ||
1137  lhs.id()==ID_byte_extract_big_endian)
1138  {
1139  assert(lhs.operands().size()==2);
1140  assign_rec(lhs.op0(), values_rhs, suffix, ns, true);
1141  }
1142  else
1143  throw "assign NYI: `"+lhs.id_string()+"'";
1144 }
1145 
1147  const irep_idt &function,
1148  const exprt::operandst &arguments,
1149  const namespacet &ns)
1150 {
1151  const symbolt &symbol=ns.lookup(function);
1152 
1153  const code_typet &type=to_code_type(symbol.type);
1154  const code_typet::parameterst &parameter_types=type.parameters();
1155 
1156  // these first need to be assigned to dummy, temporary arguments
1157  // and only thereafter to the actuals, in order
1158  // to avoid overwriting actuals that are needed for recursive
1159  // calls
1160 
1161  // the assigned data must be valid on from!
1162  unsigned old_to_function=to_function;
1163  unsigned old_to_target_index=to_target_index;
1164 
1167 
1168  for(unsigned i=0; i<arguments.size(); i++)
1169  {
1170  const std::string identifier="value_set::" + id2string(function) + "::" +
1171  "argument$"+std::to_string(i);
1172  add_var(identifier, "");
1173  exprt dummy_lhs=symbol_exprt(identifier, arguments[i].type());
1174 // std::cout << arguments[i] << '\n';
1175 
1176  assign(dummy_lhs, arguments[i], ns, true);
1177 
1178  // merge it immediately, the actual assignment needs the data visible!
1179  // does this break the purpose of the dummies?
1180  make_union(values[identifier].object_map,
1181  temporary_values[identifier].object_map);
1182  }
1183 
1184  // restore
1185  to_function=old_to_function;
1186  to_target_index=old_to_target_index;
1187 
1188  // now assign to 'actual actuals'
1189 
1190  unsigned i=0;
1191 
1192  for(code_typet::parameterst::const_iterator
1193  it=parameter_types.begin();
1194  it!=parameter_types.end();
1195  it++)
1196  {
1197  const irep_idt &identifier=it->get_identifier();
1198  if(identifier=="")
1199  continue;
1200 
1201  add_var(identifier, "");
1202 
1203  const exprt v_expr=
1204  symbol_exprt("value_set::" + id2string(function) + "::" +
1205  "argument$"+std::to_string(i), it->type());
1206 
1207  exprt actual_lhs=symbol_exprt(identifier, it->type());
1208  assign(actual_lhs, v_expr, ns, true);
1209  i++;
1210  }
1211 }
1212 
1214  const exprt &lhs,
1215  const namespacet &ns)
1216 {
1217  if(lhs.is_nil())
1218  return;
1219 
1220  irep_idt rvs = std::string("value_set::return_value") +
1221  std::to_string(from_function);
1222  add_var(rvs, "");
1223  symbol_exprt rhs(rvs, lhs.type());
1224 
1225  assign(lhs, rhs, ns);
1226 }
1227 
1229  const exprt &code,
1230  const namespacet &ns)
1231 {
1232  const irep_idt &statement=code.get(ID_statement);
1233 
1234  if(statement==ID_block)
1235  {
1236  forall_operands(it, code)
1237  apply_code(*it, ns);
1238  }
1239  else if(statement==ID_function_call)
1240  {
1241  // shouldn't be here
1242  assert(false);
1243  }
1244  else if(statement==ID_assign ||
1245  statement==ID_init)
1246  {
1247  if(code.operands().size()!=2)
1248  throw "assignment expected to have two operands";
1249 
1250  assign(code.op0(), code.op1(), ns);
1251  }
1252  else if(statement==ID_decl)
1253  {
1254  if(code.operands().size()!=1)
1255  throw "decl expected to have one operand";
1256 
1257  const exprt &lhs=code.op0();
1258 
1259  if(lhs.id()!=ID_symbol)
1260  throw "decl expected to have symbol on lhs";
1261 
1262  assign(lhs, exprt(ID_invalid, lhs.type()), ns);
1263  }
1264  else if(statement==ID_specc_notify ||
1265  statement==ID_specc_wait)
1266  {
1267  // ignore, does not change variables
1268  }
1269  else if(statement==ID_expression)
1270  {
1271  // can be ignored, we don't expect side effects here
1272  }
1273  else if(statement==ID_cpp_delete ||
1274  statement==ID_cpp_delete_array)
1275  {
1276  // does nothing
1277  }
1278  else if(statement==ID_free)
1279  {
1280  // this may kill a valid bit
1281 
1282  if(code.operands().size()!=1)
1283  throw "free expected to have one operand";
1284 
1285  do_free(code.op0(), ns);
1286  }
1287  else if(statement=="lock" || statement=="unlock")
1288  {
1289  // ignore for now
1290  }
1291  else if(statement==ID_asm)
1292  {
1293  // ignore for now, probably not safe
1294  }
1295  else if(statement==ID_nondet)
1296  {
1297  // doesn't do anything
1298  }
1299  else if(statement==ID_printf)
1300  {
1301  // doesn't do anything
1302  }
1303  else if(statement==ID_return)
1304  {
1305  // this is turned into an assignment
1306  if(code.operands().size()==1)
1307  {
1308  irep_idt rvs = std::string("value_set::return_value") +
1309  std::to_string(from_function);
1310  add_var(rvs, "");
1311  symbol_exprt lhs(rvs, code.op0().type());
1312  assign(lhs, code.op0(), ns);
1313  }
1314  }
1315  else if(statement==ID_input || statement==ID_output)
1316  {
1317  // doesn't do anything
1318  }
1319  else
1320  {
1321  throw
1322  code.pretty()+"\n"+
1323  "value_set_fivrnst: unexpected statement: "+id2string(statement);
1324  }
1325 }
1326 
1328  object_mapt &dest,
1329  unsigned n,
1330  const objectt &object) const
1331 {
1332  object_map_dt &map = dest.write();
1333  if(map.find(n)==map.end())
1334  {
1335 // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1336  // new
1337  map[n]=object;
1339  return true;
1340  }
1341  else
1342  {
1343 // std::cout << "UPD " << n << '\n';
1344  objectt &old=map[n];
1345 
1346  bool res = map.set_valid_at(n, to_function, to_target_index);
1347 
1348  if(old.offset_is_set && object.offset_is_set)
1349  {
1350  if(old.offset==object.offset)
1351  return res;
1352  else
1353  {
1354  old.offset_is_set=false;
1355  return true;
1356  }
1357  }
1358  else if(!old.offset_is_set)
1359  return res;
1360  else
1361  {
1362  old.offset_is_set=false;
1363  return true;
1364  }
1365  }
1366 }
1367 
1369  object_mapt &dest,
1370  unsigned n,
1371  const objectt &object) const
1372 {
1373  object_map_dt &map = dest.write();
1374  if(map.find(n)==map.end())
1375  {
1376 // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1377  // new
1378  map[n]=object;
1380  return true;
1381  }
1382  else
1383  {
1384 // std::cout << "UPD " << n << '\n';
1385  objectt &old=map[n];
1386 
1387  bool res = map.set_valid_at(n, from_function, from_target_index);
1388 
1389  if(old.offset_is_set && object.offset_is_set)
1390  {
1391  if(old.offset==object.offset)
1392  return res;
1393  else
1394  {
1395  old.offset_is_set=false;
1396  return true;
1397  }
1398  }
1399  else if(!old.offset_is_set)
1400  return res;
1401  else
1402  {
1403  old.offset_is_set=false;
1404  return true;
1405  }
1406  }
1407 }
1408 
1410  unsigned inx,
1411  unsigned f,
1412  unsigned line)
1413 {
1414  if(is_valid_at(inx, f, line))
1415  return false;
1416 
1417  vrange_listt &ranges = validity_ranges[inx];
1418  vrange_listt::iterator it=ranges.begin();
1419 
1420  while(it->function!=f && it!=ranges.end()) it++; // ffw to function block
1421 
1422  for(;
1423  it!=ranges.end() && it->function==f && it->from <= line;
1424  it++)
1425  {
1426  if(it->function==f)
1427  {
1428  if( line == it->to+1)
1429  {
1430  it->to++;
1431 
1432  // by any chance: does the next one connect to this one?
1433  vrange_listt::iterator n_it = it; n_it++;
1434  if(n_it!=ranges.end() &&
1435  it->function == n_it->function &&
1436  it->to+1 == n_it->from)
1437  {
1438  n_it->from = it->from; // connected!
1439  it = ranges.erase(it);
1440  }
1441  return true;
1442  }
1443  }
1444  }
1445 
1446  // it now points to either the end,
1447  // the first of a new function block,or
1448  // the first one that has from > line
1449  if(it!=ranges.end())
1450  {
1451  if(it->function==f)
1452  {
1453  if( line == it->from - 1)
1454  {
1455  it->from--;
1456 
1457  // by any chance: does the previous one connect to this one?
1458  if(it!=ranges.begin())
1459  {
1460  vrange_listt::iterator p_it = it; p_it--;
1461  if(p_it->function == it->function &&
1462  p_it->to+1 == it->from)
1463  {
1464  p_it->to = it->to; // connected!
1465  it = ranges.erase(it);
1466  }
1467  }
1468  return true;
1469  }
1470  }
1471  }
1472 
1473  // none matched
1474  validity_ranget insr(f, line, line);
1475  ranges.insert(it, insr);
1476 
1477  return true;
1478 }
1479 
1481  unsigned inx,
1482  unsigned f,
1483  unsigned line) const
1484 {
1485  #if 0
1486  std::cout << "IS_VALID_AT: " << inx << ", " << f << ", line " << line <<
1487  '\n';
1488  #endif
1489 
1490  validity_rangest::const_iterator vrs = validity_ranges.find(inx);
1491  if(vrs!=validity_ranges.end())
1492  {
1493  const vrange_listt &ranges = vrs->second;
1494 
1495  object_map_dt::vrange_listt::const_iterator it = ranges.begin();
1496 
1497  while(it->function!=f &&
1498  it!=ranges.end())
1499  it++; // ffw to function block
1500 
1501  for( ;
1502  it!=ranges.end() && it->function==f && it->from<=line;
1503  it++)
1504  if(it->contains(f, line))
1505  return true;
1506  }
1507 
1508  return false;
1509 }
1510 
1512 {
1513  bool changed=false;
1514 
1515  for(valuest::iterator it=values.begin();
1516  it!=values.end();
1517  it++)
1518  {
1519  object_mapt &state_map=it->second.object_map;
1520 
1521  irep_idt ident = id2string(it->second.identifier)+it->second.suffix;
1522 
1523  valuest::const_iterator t_it=temporary_values.find(ident);
1524 
1525  if(t_it==temporary_values.end())
1526  {
1527 // std::cout << "OLD VALUES FOR: " << ident << '\n';
1528  Forall_valid_objects(o_it, state_map.write())
1529  {
1530 // std::cout << "STILL VALID: " << to_expr(o_it) << '\n';
1531  if(state_map.write().set_valid_at(o_it->first,
1533  changed = true;
1534  }
1535  }
1536  else
1537  {
1538 // std::cout << "NEW VALUES FOR: " << ident << '\n';
1539  if(make_union(state_map, t_it->second.object_map))
1540  changed = true;
1541  }
1542  }
1543 
1544  temporary_values.clear();
1545 
1546  return changed;
1547 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
semantic type conversion
Definition: std_expr.h:1725
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
BigInt mp_integer
Definition: mp_arith.h:19
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
Definition: std_expr.h:1701
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
static object_numberingt object_numbering
void output(const namespacet &ns, std::ostream &out) const
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
unsigned int get_instance() const
Definition: std_expr.cpp:45
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
Definition: std_types.h:829
void apply_code(const exprt &code, const namespacet &ns)
const componentst & components() const
Definition: std_types.h:242
void copy_objects(object_mapt &dest, const object_mapt &src) const
static const object_map_dt blank
void dereference_rec(const exprt &src, exprt &dest) const
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static const char * alloc_adapter_prefix
Structure type.
Definition: std_types.h:296
exprt & op()
Definition: std_expr.h:1739
void do_free(const exprt &op, const namespacet &ns)
bool make_union(object_mapt &dest, const object_mapt &src) const
void set_instance(unsigned int instance)
Definition: std_expr.cpp:40
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
const irep_idt & id() const
Definition: irep.h:189
void output_entry(const entryt &e, const namespacet &ns, std::ostream &out) const
The boolean constant true.
Definition: std_expr.h:3742
#define forall_valid_objects(it, map)
void do_end_function(const exprt &lhs, const namespacet &ns)
entryt & get_entry(const idt &id, const std::string &suffix)
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1578
Value Set (Flow Insensitive, Validity Regions)
#define forall_operands(it, expr)
Definition: expr.h:17
exprt to_expr(object_map_dt::const_iterator it) const
bitvector_typet index_type()
Definition: c_types.cpp:15
Symbol table.
objmapt::const_iterator const_iterator
Operator to return the address of an object.
Definition: std_expr.h:2593
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
#define forall_objects(it, map)
void add_var(const idt &id, const std::string &suffix)
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
std::list< validity_ranget > vrange_listt
const irep_idt & display_name() const
Definition: symbol.h:60
typet type
Type of symbol.
Definition: symbol.h:37
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
static hash_numbering< irep_idt, irep_id_hash > function_numbering
std::unordered_set< exprt, irep_hash > expr_sett
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const T & read() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
const std::string & id_string() const
Definition: irep.h:192
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
std::unordered_set< unsigned int > dynamic_object_id_sett
bool is_zero() const
Definition: expr.cpp:236
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
exprt dynamic_object(const exprt &pointer)
Base Type Computation.
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
const typet & subtype() const
Definition: type.h:31
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
const_iterator find(unsigned k)
TO_BE_DOCUMENTED.
Definition: std_expr.h:1658
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
unsigned from_target_index
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
#define Forall_valid_objects(it, map)
bool simplify(exprt &expr, const namespacet &ns)