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 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(ID_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 &op,
921  const namespacet &ns)
922 {
923  // op must be a pointer
924  if(op.type().id()!=ID_pointer)
925  throw "free expected to have pointer-type operand";
926 
927  // find out what it points to
928  object_mapt value_set;
929  get_value_set(op, value_set, ns);
930 
931  const object_map_dt &object_map=value_set.read();
932 
933  // find out which *instances* interest us
934  dynamic_object_id_sett to_mark;
935 
936  forall_objects(it, object_map)
937  {
938  const exprt &object=object_numbering[it->first];
939 
940  if(object.id()==ID_dynamic_object)
941  {
943  to_dynamic_object_expr(object);
944 
945  if(dynamic_object.valid().is_true())
946  to_mark.insert(dynamic_object.get_instance());
947  }
948  }
949 
950  // mark these as 'may be invalid'
951  // this, unfortunately, destroys the sharing
952  for(valuest::iterator v_it=values.begin();
953  v_it!=values.end();
954  v_it++)
955  {
956  object_mapt new_object_map;
957 
958  const object_map_dt &old_object_map=
959  v_it->second.object_map.read();
960 
961  bool changed=false;
962 
963  forall_valid_objects(o_it, old_object_map)
964  {
965  const exprt &object=object_numbering[o_it->first];
966 
967  if(object.id()==ID_dynamic_object)
968  {
970  to_dynamic_object_expr(object);
971 
972  if(to_mark.count(dynamic_object.get_instance())==0)
973  set(new_object_map, o_it);
974  else
975  {
976  // adjust
977  offsett o = o_it->second;
978  exprt tmp(object);
979  to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
980  insert_to(new_object_map, tmp, o);
981  changed=true;
982  }
983  }
984  else
985  set(new_object_map, o_it);
986  }
987 
988  if(changed)
989  {
990  entryt &temp_entry = get_temporary_entry(v_it->second.identifier,
991  v_it->second.suffix);
992  temp_entry.object_map=new_object_map;
993  }
994  }
995 }
996 
998  const exprt &lhs,
999  const object_mapt &values_rhs,
1000  const std::string &suffix,
1001  const namespacet &ns,
1002  bool add_to_sets)
1003 {
1004  #if 0
1005  std::cout << "ASSIGN_REC LHS: " << lhs << '\n';
1006  std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1007 
1008  for(object_map_dt::const_iterator it=values_rhs.read().begin();
1009  it!=values_rhs.read().end(); it++)
1010  std::cout << "ASSIGN_REC RHS: " << to_expr(it) << '\n';
1011  #endif
1012 
1013  if(lhs.id()==ID_symbol)
1014  {
1015  const irep_idt &identifier = to_symbol_expr(lhs).get_identifier();
1016 
1017  if(has_prefix(id2string(identifier),
1018  "value_set::dynamic_object") ||
1019  has_prefix(id2string(identifier),
1020  "value_set::return_value") ||
1021  values.find(id2string(identifier)+suffix)!=values.end())
1022  // otherwise we don't track this value
1023  {
1024  entryt &temp_entry = get_temporary_entry(identifier, suffix);
1025 
1026  if(add_to_sets)
1027  {
1028  entryt &state_entry = get_entry(identifier, suffix);
1029  make_valid_union(temp_entry.object_map, state_entry.object_map);
1030  }
1031 
1032  make_union(temp_entry.object_map, values_rhs);
1033  }
1034  }
1035  else if(lhs.id()==ID_dynamic_object)
1036  {
1039 
1040  const std::string name=
1041  "value_set::dynamic_object"+
1042  std::to_string(dynamic_object.get_instance());
1043 
1044  entryt &temp_entry = get_temporary_entry(name, suffix);
1045 
1046  if(add_to_sets)
1047  {
1048  entryt &state_entry = get_entry(name, suffix);
1049  make_valid_union(temp_entry.object_map, state_entry.object_map);
1050  }
1051 
1052  make_union(temp_entry.object_map, values_rhs);
1053  }
1054  else if(lhs.id()==ID_dereference)
1055  {
1056  if(lhs.operands().size()!=1)
1057  throw lhs.id_string()+" expected to have one operand";
1058 
1059  object_mapt reference_set;
1060  get_reference_set(lhs, reference_set, ns);
1061 
1062  forall_objects(it, reference_set.read())
1063  {
1064  const exprt &object=object_numbering[it->first];
1065 
1066  if(object.id()!=ID_unknown)
1067  assign_rec(object, values_rhs, suffix, ns, add_to_sets);
1068  }
1069  }
1070  else if(lhs.id()==ID_index)
1071  {
1072  if(lhs.operands().size()!=2)
1073  throw "index expected to have two operands";
1074 
1075  const typet &type=ns.follow(lhs.op0().type());
1076 
1077  DATA_INVARIANT(type.id()==ID_array || type.id()==ID_incomplete_array,
1078  "operand 0 of index expression must be an array");
1079 
1080  assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, add_to_sets);
1081  }
1082  else if(lhs.id()==ID_member)
1083  {
1084  if(lhs.operands().size()!=1)
1085  throw "member expected to have one operand";
1086 
1087  if(lhs.op0().is_nil())
1088  return;
1089 
1090  const std::string &component_name=lhs.get_string(ID_component_name);
1091 
1092  const typet &type=ns.follow(lhs.op0().type());
1093 
1094  DATA_INVARIANT(type.id()==ID_struct ||
1095  type.id()==ID_union ||
1096  type.id()==ID_incomplete_struct ||
1097  type.id()==ID_incomplete_union,
1098  "operand 0 of member expression must be struct or union");
1099 
1100  assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
1101  ns, add_to_sets);
1102  }
1103  else if(lhs.id()=="valid_object" ||
1104  lhs.id()=="dynamic_size" ||
1105  lhs.id()=="dynamic_type")
1106  {
1107  // we ignore this here
1108  }
1109  else if(lhs.id()==ID_string_constant)
1110  {
1111  // someone writes into a string-constant
1112  // evil guy
1113  }
1114  else if(lhs.id() == ID_null_object)
1115  {
1116  // evil as well
1117  }
1118  else if(lhs.id()==ID_typecast)
1119  {
1120  const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1121 
1122  assign_rec(typecast_expr.op(), values_rhs, suffix,
1123  ns, add_to_sets);
1124  }
1125  else if(lhs.id()=="zero_string" ||
1126  lhs.id()=="is_zero_string" ||
1127  lhs.id()=="zero_string_length")
1128  {
1129  // ignore
1130  }
1131  else if(lhs.id()==ID_byte_extract_little_endian ||
1132  lhs.id()==ID_byte_extract_big_endian)
1133  {
1134  assert(lhs.operands().size()==2);
1135  assign_rec(lhs.op0(), values_rhs, suffix, ns, true);
1136  }
1137  else
1138  throw "assign NYI: `"+lhs.id_string()+"'";
1139 }
1140 
1142  const irep_idt &function,
1143  const exprt::operandst &arguments,
1144  const namespacet &ns)
1145 {
1146  const symbolt &symbol=ns.lookup(function);
1147 
1148  const code_typet &type=to_code_type(symbol.type);
1149  const code_typet::parameterst &parameter_types=type.parameters();
1150 
1151  // these first need to be assigned to dummy, temporary arguments
1152  // and only thereafter to the actuals, in order
1153  // to avoid overwriting actuals that are needed for recursive
1154  // calls
1155 
1156  // the assigned data must be valid on from!
1157  unsigned old_to_function=to_function;
1158  unsigned old_to_target_index=to_target_index;
1159 
1162 
1163  for(std::size_t i=0; i<arguments.size(); i++)
1164  {
1165  const std::string identifier="value_set::" + id2string(function) + "::" +
1166  "argument$"+std::to_string(i);
1167  add_var(identifier, "");
1168  const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1169 
1170  assign(dummy_lhs, arguments[i], ns, true);
1171 
1172  // merge it immediately, the actual assignment needs the data visible!
1173  // does this break the purpose of the dummies?
1174  make_union(values[identifier].object_map,
1175  temporary_values[identifier].object_map);
1176  }
1177 
1178  // restore
1179  to_function=old_to_function;
1180  to_target_index=old_to_target_index;
1181 
1182  // now assign to 'actual actuals'
1183 
1184  std::size_t i=0;
1185 
1186  for(code_typet::parameterst::const_iterator
1187  it=parameter_types.begin();
1188  it!=parameter_types.end();
1189  it++)
1190  {
1191  const irep_idt &identifier=it->get_identifier();
1192  if(identifier=="")
1193  continue;
1194 
1195  add_var(identifier, "");
1196 
1197  const exprt v_expr=
1198  symbol_exprt("value_set::" + id2string(function) + "::" +
1199  "argument$"+std::to_string(i), it->type());
1200 
1201  const symbol_exprt actual_lhs(identifier, it->type());
1202  assign(actual_lhs, v_expr, ns, true);
1203  i++;
1204  }
1205 }
1206 
1208  const exprt &lhs,
1209  const namespacet &ns)
1210 {
1211  if(lhs.is_nil())
1212  return;
1213 
1214  irep_idt rvs = std::string("value_set::return_value") +
1216  add_var(rvs, "");
1217  symbol_exprt rhs(rvs, lhs.type());
1218 
1219  assign(lhs, rhs, ns);
1220 }
1221 
1223  const exprt &code,
1224  const namespacet &ns)
1225 {
1226  const irep_idt &statement=code.get(ID_statement);
1227 
1228  if(statement==ID_block)
1229  {
1230  forall_operands(it, code)
1231  apply_code(*it, ns);
1232  }
1233  else if(statement==ID_function_call)
1234  {
1235  // shouldn't be here
1236  UNREACHABLE;
1237  }
1238  else if(statement==ID_assign ||
1239  statement==ID_init)
1240  {
1241  if(code.operands().size()!=2)
1242  throw "assignment expected to have two operands";
1243 
1244  assign(code.op0(), code.op1(), ns);
1245  }
1246  else if(statement==ID_decl)
1247  {
1248  if(code.operands().size()!=1)
1249  throw "decl expected to have one operand";
1250 
1251  const exprt &lhs=code.op0();
1252 
1253  if(lhs.id()!=ID_symbol)
1254  throw "decl expected to have symbol on lhs";
1255 
1256  assign(lhs, exprt(ID_invalid, lhs.type()), ns);
1257  }
1258  else if(statement==ID_expression)
1259  {
1260  // can be ignored, we don't expect side effects here
1261  }
1262  else if(statement==ID_cpp_delete ||
1263  statement==ID_cpp_delete_array)
1264  {
1265  // does nothing
1266  }
1267  else if(statement==ID_free)
1268  {
1269  // this may kill a valid bit
1270 
1271  if(code.operands().size()!=1)
1272  throw "free expected to have one operand";
1273 
1274  do_free(code.op0(), ns);
1275  }
1276  else if(statement=="lock" || statement=="unlock")
1277  {
1278  // ignore for now
1279  }
1280  else if(statement==ID_asm)
1281  {
1282  // ignore for now, probably not safe
1283  }
1284  else if(statement==ID_nondet)
1285  {
1286  // doesn't do anything
1287  }
1288  else if(statement==ID_printf)
1289  {
1290  // doesn't do anything
1291  }
1292  else if(statement==ID_return)
1293  {
1294  // this is turned into an assignment
1295  if(code.operands().size()==1)
1296  {
1297  irep_idt rvs = std::string("value_set::return_value") +
1299  add_var(rvs, "");
1300  symbol_exprt lhs(rvs, code.op0().type());
1301  assign(lhs, code.op0(), ns);
1302  }
1303  }
1304  else if(statement==ID_input || statement==ID_output)
1305  {
1306  // doesn't do anything
1307  }
1308  else
1309  {
1310  throw
1311  code.pretty()+"\n"+
1312  "value_set_fivrnst: unexpected statement: "+id2string(statement);
1313  }
1314 }
1315 
1317  object_mapt &dest,
1319  const offsett &offset) const
1320 {
1321  object_map_dt &map = dest.write();
1322  if(map.find(n)==map.end())
1323  {
1324  // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1325  // new
1326  map[n] = offset;
1328  return true;
1329  }
1330  else
1331  {
1332  // std::cout << "UPD " << n << '\n';
1333  offsett &old_offset = map[n];
1334 
1335  bool res = map.set_valid_at(n, to_function, to_target_index);
1336 
1337  if(old_offset && offset)
1338  {
1339  if(*old_offset == *offset)
1340  return res;
1341  else
1342  {
1343  old_offset.reset();
1344  return true;
1345  }
1346  }
1347  else if(!old_offset)
1348  return res;
1349  else
1350  {
1351  old_offset.reset();
1352  return true;
1353  }
1354  }
1355 }
1356 
1358  object_mapt &dest,
1360  const offsett &offset) const
1361 {
1362  object_map_dt &map = dest.write();
1363  if(map.find(n)==map.end())
1364  {
1365  // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1366  // new
1367  map[n] = offset;
1369  return true;
1370  }
1371  else
1372  {
1373  // std::cout << "UPD " << n << '\n';
1374  offsett &old_offset = map[n];
1375 
1376  bool res = map.set_valid_at(n, from_function, from_target_index);
1377 
1378  if(old_offset && offset)
1379  {
1380  if(*old_offset == *offset)
1381  return res;
1382  else
1383  {
1384  old_offset.reset();
1385  return true;
1386  }
1387  }
1388  else if(!old_offset)
1389  return res;
1390  else
1391  {
1392  old_offset.reset();
1393  return true;
1394  }
1395  }
1396 }
1397 
1399  unsigned inx,
1400  unsigned f,
1401  unsigned line)
1402 {
1403  if(is_valid_at(inx, f, line))
1404  return false;
1405 
1406  vrange_listt &ranges = validity_ranges[inx];
1407  vrange_listt::iterator it=ranges.begin();
1408 
1409  while(it->function!=f && it!=ranges.end()) it++; // ffw to function block
1410 
1411  for(;
1412  it!=ranges.end() && it->function==f && it->from <= line;
1413  it++)
1414  {
1415  if(it->function==f)
1416  {
1417  if( line == it->to+1)
1418  {
1419  it->to++;
1420 
1421  // by any chance: does the next one connect to this one?
1422  vrange_listt::iterator n_it = it; n_it++;
1423  if(n_it!=ranges.end() &&
1424  it->function == n_it->function &&
1425  it->to+1 == n_it->from)
1426  {
1427  n_it->from = it->from; // connected!
1428  it = ranges.erase(it);
1429  }
1430  return true;
1431  }
1432  }
1433  }
1434 
1435  // it now points to either the end,
1436  // the first of a new function block,or
1437  // the first one that has from > line
1438  if(it!=ranges.end())
1439  {
1440  if(it->function==f)
1441  {
1442  if( line == it->from - 1)
1443  {
1444  it->from--;
1445 
1446  // by any chance: does the previous one connect to this one?
1447  if(it!=ranges.begin())
1448  {
1449  vrange_listt::iterator p_it = it; p_it--;
1450  if(p_it->function == it->function &&
1451  p_it->to+1 == it->from)
1452  {
1453  p_it->to = it->to; // connected!
1454  it = ranges.erase(it);
1455  }
1456  }
1457  return true;
1458  }
1459  }
1460  }
1461 
1462  // none matched
1463  validity_ranget insr(f, line, line);
1464  ranges.insert(it, insr);
1465 
1466  return true;
1467 }
1468 
1470  unsigned inx,
1471  unsigned f,
1472  unsigned line) const
1473 {
1474  #if 0
1475  std::cout << "IS_VALID_AT: " << inx << ", " << f << ", line " << line <<
1476  '\n';
1477  #endif
1478 
1479  validity_rangest::const_iterator vrs = validity_ranges.find(inx);
1480  if(vrs!=validity_ranges.end())
1481  {
1482  const vrange_listt &ranges = vrs->second;
1483 
1484  object_map_dt::vrange_listt::const_iterator it = ranges.begin();
1485 
1486  while(it->function!=f &&
1487  it!=ranges.end())
1488  it++; // ffw to function block
1489 
1490  for( ;
1491  it!=ranges.end() && it->function==f && it->from<=line;
1492  it++)
1493  if(it->contains(f, line))
1494  return true;
1495  }
1496 
1497  return false;
1498 }
1499 
1501 {
1502  bool changed=false;
1503 
1504  for(valuest::iterator it=values.begin();
1505  it!=values.end();
1506  it++)
1507  {
1508  object_mapt &state_map=it->second.object_map;
1509 
1510  irep_idt ident = id2string(it->second.identifier)+it->second.suffix;
1511 
1512  valuest::const_iterator t_it=temporary_values.find(ident);
1513 
1514  if(t_it==temporary_values.end())
1515  {
1516 // std::cout << "OLD VALUES FOR: " << ident << '\n';
1517  Forall_valid_objects(o_it, state_map.write())
1518  {
1519 // std::cout << "STILL VALID: " << to_expr(o_it) << '\n';
1520  if(state_map.write().set_valid_at(o_it->first,
1522  changed = true;
1523  }
1524  }
1525  else
1526  {
1527 // std::cout << "NEW VALUES FOR: " << ident << '\n';
1528  if(make_union(state_map, t_it->second.object_map))
1529  changed = true;
1530  }
1531  }
1532 
1533  temporary_values.clear();
1534 
1535  return changed;
1536 }
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
BigInt mp_integer
Definition: mp_arith.h:22
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
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:106
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
static object_numberingt object_numbering
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
void output(const namespacet &ns, std::ostream &out) const
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
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
const irep_idt & get_identifier() const
Definition: std_expr.h:128
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
Definition: std_types.h:767
void apply_code(const exprt &code, const namespacet &ns)
const_iterator find(object_numberingt::number_type k)
const componentst & components() const
Definition: std_types.h:245
void copy_objects(object_mapt &dest, const object_mapt &src) const
static const object_map_dt blank
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value...
void dereference_rec(const exprt &src, exprt &dest) const
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static const char * alloc_adapter_prefix
Structure type.
Definition: std_types.h:297
Extract member of struct or union.
Definition: std_expr.h:3871
void do_free(const exprt &op, const namespacet &ns)
bool make_union(object_mapt &dest, const object_mapt &src) const
bool offset_is_zero(offsett offset) const
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:4488
#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:75
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:74
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
Value Set (Flow Insensitive, Validity Regions)
#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
exprt to_expr(object_map_dt::const_iterator it) const
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
Author: Diffblue Ltd.
typename Map::mapped_type number_type
Definition: numbering.h:24
objmapt::const_iterator const_iterator
Operator to return the address of an object.
Definition: std_expr.h:3170
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:45
std::list< validity_ranget > vrange_listt
const irep_idt & display_name() const
Definition: symbol.h:57
typet type
Type of symbol.
Definition: symbol.h:34
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:42
const parameterst & parameters() const
Definition: std_types.h:905
std::string to_string(const string_constraintt &expr)
Used for debug printing.
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
#define UNREACHABLE
Definition: invariant.h:250
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
const T & read() const
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:161
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt & op2()
Definition: expr.h:78
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
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:33
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
TO_BE_DOCUMENTED.
Definition: std_expr.h:2035
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void make_typecast(const typet &_type)
Definition: expr.cpp:84
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
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)
array index operator
Definition: std_expr.h:1462
static format_containert< T > format(const T &o)
Definition: format.h:35