CBMC
Loading...
Searching...
No Matches
value_set_fi.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set (Flow Insensitive, Sharing)
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "value_set_fi.h"
13
14#include <util/arith_tools.h>
15#include <util/byte_operators.h>
16#include <util/c_types.h>
17#include <util/namespace.h>
18#include <util/pointer_expr.h>
19#include <util/simplify_expr.h>
20#include <util/std_code.h>
21#include <util/symbol.h>
22
24
26
27#include <ostream>
28
30
33
34static const char *alloc_adapter_prefix="alloc_adaptor::";
35
37 const namespacet &ns,
38 std::ostream &out) const
39{
40 for(valuest::const_iterator
41 v_it=values.begin();
42 v_it!=values.end();
43 v_it++)
44 {
45 irep_idt identifier, display_name;
46
47 const entryt &e=v_it->second;
48
49 if(e.identifier.starts_with("value_set::dynamic_object"))
50 {
51 display_name=id2string(e.identifier)+e.suffix;
52 identifier.clear();
53 }
54 else
55 {
56 #if 0
57 const symbolt &symbol=ns.lookup(id2string(e.identifier));
58 display_name=symbol.display_name()+e.suffix;
59 identifier=symbol.name;
60 #else
61 identifier=id2string(e.identifier);
62 display_name=id2string(identifier)+e.suffix;
63 #endif
64 }
65
66 out << display_name;
67
68 out << " = { ";
69
70 object_mapt object_map;
71 flatten(e, object_map);
72
73 std::size_t width=0;
74
75 const auto &entries = object_map.read();
76 for(object_map_dt::const_iterator o_it = entries.begin();
77 o_it != entries.end();
78 ++o_it)
79 {
80 const exprt &o=object_numbering[o_it->first];
81
82 std::string result;
83
84 if(o.id()==ID_invalid || o.id()==ID_unknown)
85 {
86 result="<";
87 result+=from_expr(ns, identifier, o);
88 result+=", *, "; // offset unknown
89 if(o.type().id()==ID_unknown)
90 result+='*';
91 else
92 result+=from_type(ns, identifier, o.type());
93 result+='>';
94 }
95 else
96 {
97 result="<"+from_expr(ns, identifier, o)+", ";
98
99 if(o_it->second)
100 result += integer2string(*o_it->second);
101 else
102 result+='*';
103
104 result+=", ";
105
106 if(o.type().id()==ID_unknown)
107 result+='*';
108 else
109 result+=from_type(ns, identifier, o.type());
110
111 result+='>';
112 }
113
114 out << result;
115
116 width+=result.size();
117
119 next++;
120
121 if(next != entries.end())
122 {
123 out << ", ";
124 if(width>=40)
125 out << "\n ";
126 }
127 }
128
129 out << " } \n";
130 }
131}
132
134 const entryt &e,
135 object_mapt &dest) const
136{
137 #if 0
138 std::cout << "FLATTEN: " << e.identifier << e.suffix << '\n';
139 #endif
140
141 flatten_seent seen;
142 flatten_rec(e, dest, seen);
143
144 #if 0
145 std::cout << "FLATTEN: Done.\n";
146 #endif
147}
148
150 const entryt &e,
151 object_mapt &dest,
152 flatten_seent &seen) const
153{
154 #if 0
155 std::cout << "FLATTEN_REC: " << e.identifier << e.suffix << '\n';
156 #endif
157
158 std::string identifier = id2string(e.identifier);
159 CHECK_RETURN(seen.find(identifier + e.suffix) == seen.end());
160
161 bool generalize_index = false;
162
163 seen.insert(identifier + e.suffix);
164
165 for(const auto &object_entry : e.object_map.read())
166 {
167 const exprt &o = object_numbering[object_entry.first];
168
169 if(o.type().id()=="#REF#")
170 {
171 if(seen.find(o.get(ID_identifier))!=seen.end())
172 {
173 generalize_index = true;
174 continue;
175 }
176
177 valuest::const_iterator fi = values.find(o.get(ID_identifier));
178 if(fi==values.end())
179 {
180 // this is some static object, keep it in.
181 const symbol_exprt se(
182 o.get(ID_identifier), to_type_with_subtype(o.type()).subtype());
183 insert(dest, se, mp_integer{0});
184 }
185 else
186 {
188 flatten_rec(fi->second, temp, seen);
189
190 for(object_map_dt::iterator t_it=temp.write().begin();
191 t_it!=temp.write().end();
192 t_it++)
193 {
194 if(t_it->second && object_entry.second)
195 {
196 *t_it->second += *object_entry.second;
197 }
198 else
199 t_it->second.reset();
200 }
201
202 for(const auto &object_entry : temp.read())
203 insert(dest, object_entry);
204 }
205 }
206 else
207 insert(dest, object_entry);
208 }
209
210 if(generalize_index) // this means we had recursive symbols in there
211 {
212 for(auto &object_entry : dest.write())
213 object_entry.second.reset();
214 }
215
216 seen.erase(identifier + e.suffix);
217}
218
220{
221 const exprt &object=object_numbering[it.first];
222
223 if(object.id()==ID_invalid ||
224 object.id()==ID_unknown)
225 return object;
226
228
229 od.object()=object;
230
231 if(it.second)
232 od.offset() = from_integer(*it.second, c_index_type());
233
234 od.type()=od.object().type();
235
236 return std::move(od);
237}
238
240{
242 bool result=false;
243
244 for(valuest::const_iterator
245 it=new_values.begin();
246 it!=new_values.end();
247 it++)
248 {
249 valuest::iterator it2=values.find(it->first);
250
251 if(it2==values.end())
252 {
253 // we always track these
254 if(
255 it->second.identifier.starts_with("value_set::dynamic_object") ||
256 it->second.identifier.starts_with("value_set::return_value"))
257 {
258 values.insert(*it);
259 result=true;
260 }
261
262 continue;
263 }
264
265 entryt &e=it2->second;
266 const entryt &new_e=it->second;
267
268 if(make_union(e.object_map, new_e.object_map))
269 result=true;
270 }
271
272 changed = result;
273
274 return result;
275}
276
278{
279 bool result=false;
280
281 for(const auto &object_entry : src.read())
282 {
283 if(insert(dest, object_entry))
284 result=true;
285 }
286
287 return result;
288}
289
290std::vector<exprt>
291value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
292{
293 object_mapt object_map;
294 get_value_set(expr, object_map, ns);
295
297
298 for(const auto &object_entry : object_map.read())
299 {
300 const exprt &object = object_numbering[object_entry.first];
301 if(object.type().id()=="#REF#")
302 {
303 DATA_INVARIANT(object.id() == ID_symbol, "reference to symbol required");
304
305 const irep_idt &ident = object.get(ID_identifier);
306 valuest::const_iterator v_it = values.find(ident);
307
308 if(v_it!=values.end())
309 {
311 flatten(v_it->second, temp);
312
313 for(object_map_dt::iterator t_it=temp.write().begin();
314 t_it!=temp.write().end();
315 t_it++)
316 {
317 if(t_it->second && object_entry.second)
318 {
319 *t_it->second += *object_entry.second;
320 }
321 else
322 t_it->second.reset();
323
324 flat_map.write()[t_it->first]=t_it->second;
325 }
326 }
327 }
328 else
329 flat_map.write()[object_entry.first] = object_entry.second;
330 }
331
332 std::vector<exprt> result;
333 for(const auto &object_entry : flat_map.read())
334 result.push_back(to_expr(object_entry));
335
336#if 0
337 // Sanity check!
338 for(std::list<exprt>::const_iterator it=value_set.begin();
339 it!=value_set.end();
340 it++)
341 assert(it->type().id()!="#REF");
342#endif
343
344#if 0
345 for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
346 std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
347#endif
348
349 return result;
350}
351
353 const exprt &expr,
354 object_mapt &dest,
355 const namespacet &ns) const
356{
357 exprt tmp(expr);
358 simplify(tmp, ns);
359
361 bool includes_nondet_pointer = false;
363 tmp, dest, includes_nondet_pointer, "", tmp.type(), ns, recset);
364}
365
367 const exprt &expr,
368 object_mapt &dest,
370 const std::string &suffix,
371 const typet &original_type,
372 const namespacet &ns,
373 gvs_recursion_sett &recursion_set) const
374{
375 #if 0
376 std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr)
377 << '\n';
378 std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
379 std::cout << '\n';
380 #endif
381
382 if(expr.type().id()=="#REF#")
383 {
384 valuest::const_iterator fi = values.find(expr.get(ID_identifier));
385
386 if(fi!=values.end())
387 {
388 for(const auto &object_entry : fi->second.object_map.read())
389 {
392 dest,
394 suffix,
396 ns,
397 recursion_set);
398 }
399 return;
400 }
401 else
402 {
404 return;
405 }
406 }
407 else if(expr.id()==ID_unknown || expr.id()==ID_invalid)
408 {
410 return;
411 }
412 else if(expr.id()==ID_index)
413 {
414 const typet &type = to_index_expr(expr).array().type();
415
416 if(type.id() == ID_array)
417 {
419 to_index_expr(expr).array(),
420 dest,
422 "[]" + suffix,
424 ns,
425 recursion_set);
426 }
427 else
429
430 return;
431 }
432 else if(expr.id()==ID_member)
433 {
434 const auto &compound = to_member_expr(expr).compound();
435
436 if(compound.is_not_nil())
437 {
439 compound.type().id() == ID_struct ||
440 compound.type().id() == ID_struct_tag ||
441 compound.type().id() == ID_union ||
442 compound.type().id() == ID_union_tag,
443 "operand 0 of member expression must be struct or union");
444
445 const std::string &component_name =
446 id2string(to_member_expr(expr).get_component_name());
447
449 compound,
450 dest,
452 "." + component_name + suffix,
454 ns,
455 recursion_set);
456
457 return;
458 }
459 }
460 else if(expr.id()==ID_symbol)
461 {
462 // just keep a reference to the ident in the set
463 // (if it exists)
464 irep_idt ident = id2string(to_symbol_expr(expr).get_identifier()) + suffix;
465 valuest::const_iterator v_it=values.find(ident);
466
467 if(ident.starts_with(alloc_adapter_prefix))
468 {
469 insert(dest, expr, mp_integer{0});
470 return;
471 }
472 else if(v_it!=values.end())
473 {
474 type_with_subtypet t("#REF#", expr.type());
476 insert(dest, sym, mp_integer{0});
477 return;
478 }
479 }
480 else if(expr.id()==ID_if)
481 {
483 to_if_expr(expr).true_case(),
484 dest,
486 suffix,
488 ns,
489 recursion_set);
491 to_if_expr(expr).false_case(),
492 dest,
494 suffix,
496 ns,
497 recursion_set);
498
499 return;
500 }
501 else if(expr.id()==ID_address_of)
502 {
503 get_reference_set_sharing(to_address_of_expr(expr).object(), dest, ns);
504
505 return;
506 }
507 else if(expr.id()==ID_dereference)
508 {
511 const object_map_dt &object_map=reference_set.read();
512
513 if(object_map.begin()!=object_map.end())
514 {
515 for(const auto &object_entry : object_map)
516 {
517 const exprt &object = object_numbering[object_entry.first];
519 object,
520 dest,
522 suffix,
524 ns,
525 recursion_set);
526 }
527
528 return;
529 }
530 }
531 else if(expr.is_constant())
532 {
533 // check if NULL
534 if(to_constant_expr(expr).is_null_pointer())
535 {
536 insert(
537 dest,
538 exprt(ID_null_object, to_pointer_type(expr.type()).base_type()),
539 mp_integer{0});
540 return;
541 }
542 }
543 else if(expr.id()==ID_typecast)
544 {
546 to_typecast_expr(expr).op(),
547 dest,
549 suffix,
551 ns,
552 recursion_set);
553
554 return;
555 }
556 else if(expr.id()==ID_plus || expr.id()==ID_minus)
557 {
558 if(expr.operands().size()<2)
559 throw expr.id_string()+" expected to have at least two operands";
560
561 if(expr.type().id()==ID_pointer)
562 {
563 // find the pointer operand
564 const exprt *ptr_operand=nullptr;
565
566 for(const auto &op : expr.operands())
567 {
568 if(op.type().id() == ID_pointer)
569 {
570 if(ptr_operand==nullptr)
571 ptr_operand = &op;
572 else
573 throw "more than one pointer operand in pointer arithmetic";
574 }
575 }
576
577 if(ptr_operand==nullptr)
578 throw "pointer type sum expected to have pointer operand";
579
585 "",
586 ptr_operand->type(),
587 ns,
588 recursion_set);
589
590 for(const auto &object_entry : pointer_expr_set.read())
591 {
592 offsett offset = object_entry.second;
593
594 if(offset_is_zero(offset) && expr.operands().size() == 2)
595 {
596 if(to_binary_expr(expr).op0().type().id() != ID_pointer)
597 {
598 const auto i = numeric_cast<mp_integer>(to_binary_expr(expr).op0());
599 if(!i.has_value())
600 offset.reset();
601 else
602 *offset = (expr.id() == ID_plus) ? *i : -*i;
603 }
604 else
605 {
606 const auto i = numeric_cast<mp_integer>(to_binary_expr(expr).op1());
607 if(!i.has_value())
608 offset.reset();
609 else
610 *offset = (expr.id() == ID_plus) ? *i : -*i;
611 }
612 }
613 else
614 offset.reset();
615
616 insert(dest, object_entry.first, offset);
617 }
618
619 return;
620 }
621 }
622 else if(expr.id()==ID_side_effect)
623 {
624 const irep_idt &statement = to_side_effect_expr(expr).get_statement();
625
626 if(statement==ID_function_call)
627 {
628 // these should be gone
629 throw "unexpected function_call sideeffect";
630 }
631 else if(statement==ID_allocate)
632 {
633 if(expr.type().id()!=ID_pointer)
634 throw "malloc expected to return pointer type";
635
636 PRECONDITION(suffix.empty());
637
638 const typet &dynamic_type=
639 static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
640
642 // let's make up a `unique' number for this object...
643 dynamic_object.set_instance(
645 dynamic_object.valid()=true_exprt();
646
648 return;
649 }
650 else if(statement==ID_cpp_new ||
651 statement==ID_cpp_new_array)
652 {
653 PRECONDITION(suffix.empty());
654 PRECONDITION(expr.type().id() == ID_pointer);
655
657 to_pointer_type(expr.type()).base_type());
658 dynamic_object.set_instance(
660 dynamic_object.valid()=true_exprt();
661
663 return;
664 }
665 }
666 else if(expr.id()==ID_struct)
667 {
668 // this is like a static struct object
669 insert(dest, address_of_exprt(expr), mp_integer{0});
670 return;
671 }
672 else if(expr.id()==ID_with)
673 {
674 // these are supposed to be done by assign()
675 throw "unexpected value in get_value_set: "+expr.id_string();
676 }
677 else if(expr.id()==ID_array_of ||
678 expr.id()==ID_array)
679 {
680 // an array constructor, possibly containing addresses
681 for(const auto &op : expr.operands())
682 {
684 op,
685 dest,
687 suffix,
689 ns,
690 recursion_set);
691 }
692 }
693 else if(expr.id()==ID_dynamic_object)
694 {
697
698 const std::string name=
699 "value_set::dynamic_object"+
700 std::to_string(dynamic_object.get_instance())+
701 suffix;
702
703 // look it up
704 valuest::const_iterator v_it=values.find(name);
705
706 if(v_it!=values.end())
707 {
708 make_union(dest, v_it->second.object_map);
709 return;
710 }
711 }
712
714}
715
717 const exprt &src,
718 exprt &dest) const
719{
720 // remove pointer typecasts
721 if(src.id()==ID_typecast)
722 {
723 PRECONDITION(src.type().id() == ID_pointer);
724
725 dereference_rec(to_typecast_expr(src).op(), dest);
726 }
727 else
728 dest=src;
729}
730
732 const exprt &expr,
733 expr_sett &dest,
734 const namespacet &ns) const
735{
736 object_mapt object_map;
737 get_reference_set_sharing(expr, object_map, ns);
738
739 for(const auto &object_entry : object_map.read())
740 {
741 const exprt &object = object_numbering[object_entry.first];
742
743 if(object.type().id() == "#REF#")
744 {
745 const irep_idt &ident = object.get(ID_identifier);
746 valuest::const_iterator vit = values.find(ident);
747 if(vit==values.end())
748 {
749 // Assume the variable never was assigned,
750 // so assume it's reference set is unknown.
751 dest.insert(exprt(ID_unknown, object.type()));
752 }
753 else
754 {
756 flatten(vit->second, omt);
757
758 for(object_map_dt::iterator t_it=omt.write().begin();
759 t_it!=omt.write().end();
760 t_it++)
761 {
762 if(t_it->second && object_entry.second)
763 {
764 *t_it->second += *object_entry.second;
765 }
766 else
767 t_it->second.reset();
768 }
769
770 for(const auto &o : omt.read())
771 dest.insert(to_expr(o));
772 }
773 }
774 else
775 dest.insert(to_expr(object_entry));
776 }
777}
778
780 const exprt &expr,
781 expr_sett &dest,
782 const namespacet &ns) const
783{
784 object_mapt object_map;
785 get_reference_set_sharing(expr, object_map, ns);
786
787 for(const auto &object_entry : object_map.read())
788 dest.insert(to_expr(object_entry));
789}
790
792 const exprt &expr,
793 object_mapt &dest,
794 const namespacet &ns) const
795{
796 #if 0
797 std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)
798 << '\n';
799 #endif
800
801 if(expr.type().id()=="#REF#")
802 {
803 valuest::const_iterator fi = values.find(expr.get(ID_identifier));
804 if(fi!=values.end())
805 {
806 for(const auto &object_entry : fi->second.object_map.read())
807 {
809 object_numbering[object_entry.first], dest, ns);
810 }
811 return;
812 }
813 }
814 else if(expr.id()==ID_symbol ||
815 expr.id()==ID_dynamic_object ||
816 expr.id()==ID_string_constant)
817 {
818 if(
819 expr.type().id() == ID_array &&
820 to_array_type(expr.type()).element_type().id() == ID_array)
821 {
822 insert(dest, expr);
823 }
824 else
825 insert(dest, expr, mp_integer{0});
826
827 return;
828 }
829 else if(expr.id()==ID_dereference)
830 {
833 bool includes_nondet_pointer = false;
835 to_dereference_expr(expr).pointer(),
836 temp,
838 "",
839 to_dereference_expr(expr).pointer().type(),
840 ns,
841 recset);
842
843 // REF's need to be dereferenced manually!
844 for(const auto &object_entry : temp.read())
845 {
846 const exprt &obj = object_numbering[object_entry.first];
847 if(obj.type().id()=="#REF#")
848 {
849 const irep_idt &ident = obj.get(ID_identifier);
850 valuest::const_iterator v_it = values.find(ident);
851
852 if(v_it!=values.end())
853 {
855 flatten(v_it->second, t2);
856
857 for(object_map_dt::iterator t_it=t2.write().begin();
858 t_it!=t2.write().end();
859 t_it++)
860 {
861 if(t_it->second && object_entry.second)
862 {
863 *t_it->second += *object_entry.second;
864 }
865 else
866 t_it->second.reset();
867 }
868
869 for(const auto &t2_object_entry : t2.read())
870 insert(dest, t2_object_entry);
871 }
872 else
873 insert(
874 dest,
875 exprt(ID_unknown, to_type_with_subtype(obj.type()).subtype()));
876 }
877 else
878 insert(dest, object_entry);
879 }
880
881 #if 0
882 for(expr_sett::const_iterator it=value_set.begin();
883 it!=value_set.end();
884 it++)
885 std::cout << "VALUE_SET: " << format(*it) << '\n';
886 #endif
887
888 return;
889 }
890 else if(expr.id()==ID_index)
891 {
892 const exprt &array = to_index_expr(expr).array();
893 const exprt &offset = to_index_expr(expr).index();
894 const typet &array_type = array.type();
895
897 array_type.id() == ID_array, "index takes array-typed operand");
898
901
902 const object_map_dt &object_map=array_references.read();
903
904 for(const auto &object_entry : object_map)
905 {
906 const exprt &object = object_numbering[object_entry.first];
907
908 if(
909 object.id() == ID_unknown ||
910 (object.type().id() != ID_array && object.type().id() != ID_vector))
911 {
912 insert(dest, exprt(ID_unknown, expr.type()));
913 }
914 else
915 {
917 object, from_integer(0, c_index_type()), expr.type());
918
920
921 // adjust type?
922 if(object.type().id() != "#REF#" && object.type() != array_type)
924 else
926
927 offsett o = object_entry.second;
928 const auto i = numeric_cast<mp_integer>(offset);
929
930 if(offset.is_zero())
931 {
932 }
933 else if(i.has_value() && offset_is_zero(o))
934 *o = *i;
935 else
936 o.reset();
937
938 insert(dest, casted_index, o);
939 }
940 }
941
942 return;
943 }
944 else if(expr.id()==ID_member)
945 {
946 const irep_idt &component_name=expr.get(ID_component_name);
947
948 const exprt &struct_op = to_member_expr(expr).compound();
949
952
953 for(const auto &object_entry : struct_references.read())
954 {
955 const exprt &object = object_numbering[object_entry.first];
956 const typet &obj_type = object.type();
957
958 if(object.id()==ID_unknown)
959 insert(dest, exprt(ID_unknown, expr.type()));
960 else if(
961 obj_type.id() != ID_struct && obj_type.id() != ID_union &&
962 obj_type.id() != ID_struct_tag && obj_type.id() != ID_union_tag)
963 {
964 // we catch objects of the wrong type,
965 // to avoid non-integral typecasts.
966 insert(dest, exprt(ID_unknown, expr.type()));
967 }
968 else
969 {
970 offsett o = object_entry.second;
971
972 member_exprt member_expr(object, component_name, expr.type());
973
974 // adjust type?
975 if(struct_op.type() != object.type())
976 {
977 member_expr.compound() =
978 typecast_exprt(member_expr.compound(), struct_op.type());
979 }
980
981 insert(dest, member_expr, o);
982 }
983 }
984
985 return;
986 }
987 else if(expr.id()==ID_if)
988 {
989 get_reference_set_sharing_rec(to_if_expr(expr).true_case(), dest, ns);
990 get_reference_set_sharing_rec(to_if_expr(expr).false_case(), dest, ns);
991 return;
992 }
993
994 insert(dest, exprt(ID_unknown, expr.type()));
995}
996
998 const exprt &lhs,
999 const exprt &rhs,
1000 const namespacet &ns)
1001{
1002 #if 0
1003 std::cout << "ASSIGN LHS: " << format(lhs) << '\n';
1004 std::cout << "ASSIGN RHS: " << format(rhs) << '\n';
1005 #endif
1006
1007 if(rhs.id()==ID_if)
1008 {
1009 assign(lhs, to_if_expr(rhs).true_case(), ns);
1010 assign(lhs, to_if_expr(rhs).false_case(), ns);
1011 return;
1012 }
1013
1014 if(
1015 lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag ||
1016 lhs.type().id() == ID_union || lhs.type().id() == ID_union_tag)
1017 {
1018 const auto &components =
1019 (lhs.type().id() == ID_struct_tag || lhs.type().id() == ID_union_tag)
1020 ? ns.follow_tag(to_struct_or_union_tag_type(lhs.type())).components()
1021 : to_struct_union_type(lhs.type()).components();
1022
1023 std::size_t no=0;
1024
1025 for(struct_typet::componentst::const_iterator c_it = components.begin();
1026 c_it != components.end();
1027 c_it++, no++)
1028 {
1029 const typet &subtype=c_it->type();
1030 const irep_idt &name = c_it->get_name();
1031
1032 // ignore padding
1034 subtype.id() != ID_code,
1035 "struct/union member must not be of code type");
1036 if(c_it->get_is_padding())
1037 continue;
1038
1039 member_exprt lhs_member(lhs, name, subtype);
1040
1042
1043 if(rhs.id()==ID_unknown ||
1044 rhs.id()==ID_invalid)
1045 {
1046 rhs_member=exprt(rhs.id(), subtype);
1047 }
1048 else
1049 {
1050 if(rhs.type() != lhs.type())
1051 throw "value_set_fit::assign type mismatch: "
1052 "rhs.type():\n"+rhs.type().pretty()+"\n"+
1053 "type:\n"+lhs.type().pretty();
1054
1055 if(rhs.id() == ID_struct || rhs.is_constant())
1056 {
1058 no < rhs.operands().size(), "component index must be in bounds");
1059 rhs_member=rhs.operands()[no];
1060 }
1061 else if(rhs.id()==ID_with)
1062 {
1063 // see if this is the member we want
1064 const auto &rhs_with = to_with_expr(rhs);
1065 const exprt &member_operand = rhs_with.where();
1066
1067 const irep_idt &component_name=
1069
1070 if(component_name==name)
1071 {
1072 // yes! just take op2
1073 rhs_member = rhs_with.new_value();
1074 }
1075 else
1076 {
1077 // no! do op0
1078 rhs_member=exprt(ID_member, subtype);
1079 rhs_member.copy_to_operands(rhs_with.old());
1080 rhs_member.set(ID_component_name, name);
1081 }
1082 }
1083 else
1084 {
1085 rhs_member=exprt(ID_member, subtype);
1086 rhs_member.copy_to_operands(rhs);
1087 rhs_member.set(ID_component_name, name);
1088 }
1089
1091 }
1092 }
1093 }
1094 else if(lhs.type().id() == ID_array)
1095 {
1096 const index_exprt lhs_index(
1097 lhs,
1099 to_array_type(lhs.type()).element_type());
1100
1101 if(rhs.id()==ID_unknown ||
1102 rhs.id()==ID_invalid)
1103 {
1104 assign(
1105 lhs_index,
1106 exprt(rhs.id(), to_array_type(lhs.type()).element_type()),
1107 ns);
1108 }
1109 else if(rhs.is_nil())
1110 {
1111 // do nothing
1112 }
1113 else
1114 {
1115 if(rhs.type() != lhs.type())
1116 throw "value_set_fit::assign type mismatch: "
1117 "rhs.type():\n"+rhs.type().pretty()+"\n"+
1118 "type:\n"+lhs.type().pretty();
1119
1120 if(rhs.id()==ID_array_of)
1121 {
1122 assign(lhs_index, to_array_of_expr(rhs).what(), ns);
1123 }
1124 else if(rhs.id() == ID_array || rhs.is_constant())
1125 {
1126 for(const auto &op : rhs.operands())
1127 {
1128 assign(lhs_index, op, ns);
1129 }
1130 }
1131 else if(rhs.id()==ID_with)
1132 {
1133 const index_exprt op0_index(
1134 to_with_expr(rhs).old(),
1136 to_array_type(lhs.type()).element_type());
1137
1139 assign(lhs_index, to_with_expr(rhs).new_value(), ns);
1140 }
1141 else
1142 {
1143 const index_exprt rhs_index(
1144 rhs,
1146 to_array_type(lhs.type()).element_type());
1148 }
1149 }
1150 }
1151 else
1152 {
1153 // basic type
1155
1156 get_value_set(rhs, values_rhs, ns);
1157
1159 assign_rec(lhs, values_rhs, "", ns, recset);
1160 }
1161}
1162
1164 const exprt &lhs,
1165 const object_mapt &values_rhs,
1166 const std::string &suffix,
1167 const namespacet &ns,
1168 assign_recursion_sett &recursion_set)
1169{
1170 #if 0
1171 std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n';
1172 std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1173
1174 for(object_map_dt::const_iterator it=values_rhs.read().begin();
1175 it!=values_rhs.read().end(); it++)
1176 std::cout << "ASSIGN_REC RHS: " << to_expr(it) << '\n';
1177 #endif
1178
1179 if(lhs.type().id()=="#REF#")
1180 {
1181 const irep_idt &ident = lhs.get(ID_identifier);
1184 bool includes_nondet_pointer = false;
1186 lhs,
1187 temp,
1189 "",
1190 to_type_with_subtype(lhs.type()).subtype(),
1191 ns,
1192 recset);
1193
1194 if(recursion_set.find(ident)!=recursion_set.end())
1195 {
1196 recursion_set.insert(ident);
1197
1198 for(const auto &object_entry : temp.read())
1199 {
1200 const exprt &object = object_numbering[object_entry.first];
1201
1202 if(object.id() != ID_unknown)
1203 assign_rec(object, values_rhs, suffix, ns, recursion_set);
1204 }
1205
1206 recursion_set.erase(ident);
1207 }
1208 }
1209 else if(lhs.id()==ID_symbol)
1210 {
1211 const irep_idt &identifier = to_symbol_expr(lhs).get_identifier();
1212
1213 if(
1214 identifier.starts_with("value_set::dynamic_object") ||
1215 identifier.starts_with("value_set::return_value") ||
1216 values.find(id2string(identifier) + suffix) != values.end())
1217 // otherwise we don't track this value
1218 {
1219 entryt &entry = get_entry(identifier, suffix);
1220
1221 if(make_union(entry.object_map, values_rhs))
1222 changed = true;
1223 }
1224 }
1225 else if(lhs.id()==ID_dynamic_object)
1226 {
1229
1230 const std::string name=
1231 "value_set::dynamic_object"+
1232 std::to_string(dynamic_object.get_instance());
1233
1234 if(make_union(get_entry(name, suffix).object_map, values_rhs))
1235 changed = true;
1236 }
1237 else if(lhs.id()==ID_dereference)
1238 {
1239 if(lhs.operands().size()!=1)
1240 throw lhs.id_string()+" expected to have one operand";
1241
1244
1245 for(const auto &object_entry : reference_set.read())
1246 {
1247 const exprt &object = object_numbering[object_entry.first];
1248
1249 if(object.id()!=ID_unknown)
1250 assign_rec(object, values_rhs, suffix, ns, recursion_set);
1251 }
1252 }
1253 else if(lhs.id()==ID_index)
1254 {
1255 const typet &type = to_index_expr(lhs).array().type();
1256
1257 if(type.id() == ID_array)
1258 {
1259 assign_rec(
1260 to_index_expr(lhs).array(),
1261 values_rhs,
1262 "[]" + suffix,
1263 ns,
1264 recursion_set);
1265 }
1266 }
1267 else if(lhs.id()==ID_member)
1268 {
1269 if(to_member_expr(lhs).compound().is_nil())
1270 return;
1271
1272 const std::string &component_name=lhs.get_string(ID_component_name);
1273 const exprt &compound = to_member_expr(lhs).compound();
1274
1276 compound.type().id() == ID_struct ||
1277 compound.type().id() == ID_struct_tag ||
1278 compound.type().id() == ID_union ||
1279 compound.type().id() == ID_union_tag,
1280 "operand 0 of member expression must be struct or union");
1281
1282 assign_rec(
1283 compound, values_rhs, "." + component_name + suffix, ns, recursion_set);
1284 }
1285 else if(lhs.id()=="valid_object" ||
1286 lhs.id()=="dynamic_type")
1287 {
1288 // we ignore this here
1289 }
1290 else if(lhs.id()==ID_string_constant)
1291 {
1292 // someone writes into a string-constant
1293 // evil guy
1294 }
1295 else if(lhs.id() == ID_null_object)
1296 {
1297 // evil as well
1298 }
1299 else if(lhs.id()==ID_typecast)
1300 {
1302
1303 assign_rec(typecast_expr.op(), values_rhs, suffix, ns, recursion_set);
1304 }
1305 else if(
1306 lhs.id() == "zero_string" || lhs.id() == "is_zero_string" ||
1307 lhs.id() == "zero_string_length" || lhs.id() == ID_address_of)
1308 {
1309 // ignore
1310 }
1311 else if(lhs.id()==ID_byte_extract_little_endian ||
1313 {
1314 assign_rec(
1315 to_byte_extract_expr(lhs).op(), values_rhs, suffix, ns, recursion_set);
1316 }
1317 else
1318 throw "assign NYI: '" + lhs.id_string() + "'";
1319}
1320
1322 const irep_idt &function,
1323 const exprt::operandst &arguments,
1324 const namespacet &ns)
1325{
1326 const symbolt &symbol=ns.lookup(function);
1327
1328 const code_typet &type=to_code_type(symbol.type);
1330
1331 // these first need to be assigned to dummy, temporary arguments
1332 // and only thereafter to the actuals, in order
1333 // to avoid overwriting actuals that are needed for recursive
1334 // calls
1335
1336 for(std::size_t i=0; i<arguments.size(); i++)
1337 {
1338 const std::string identifier="value_set::" + id2string(function) + "::" +
1339 "argument$"+std::to_string(i);
1340 add_var(identifier);
1341 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1342 assign(dummy_lhs, arguments[i], ns);
1343 }
1344
1345 // now assign to 'actual actuals'
1346
1347 std::size_t i=0;
1348
1349 for(code_typet::parameterst::const_iterator
1350 it=parameter_types.begin();
1351 it!=parameter_types.end();
1352 it++)
1353 {
1354 const irep_idt &identifier=it->get_identifier();
1355 if(identifier.empty())
1356 continue;
1357
1358 add_var(identifier);
1359
1360 const exprt v_expr=
1361 symbol_exprt("value_set::" + id2string(function) + "::" +
1362 "argument$"+std::to_string(i), it->type());
1363
1364 const symbol_exprt actual_lhs(identifier, it->type());
1365 assign(actual_lhs, v_expr, ns);
1366 i++;
1367 }
1368}
1369
1371 const exprt &lhs,
1372 const namespacet &ns)
1373{
1374 if(lhs.is_nil())
1375 return;
1376
1377 std::string rvs = "value_set::return_value" + std::to_string(from_function);
1378 symbol_exprt rhs(rvs, lhs.type());
1379
1380 assign(lhs, rhs, ns);
1381}
1382
1383void value_set_fit::apply_code(const codet &code, const namespacet &ns)
1384{
1385 const irep_idt &statement=code.get(ID_statement);
1386
1387 if(statement==ID_block)
1388 {
1389 for(const auto &stmt : to_code_block(code).statements())
1390 apply_code(stmt, ns);
1391 }
1392 else if(statement==ID_function_call)
1393 {
1394 // shouldn't be here
1396 }
1397 else if(statement==ID_assign)
1398 {
1399 if(code.operands().size()!=2)
1400 throw "assignment expected to have two operands";
1401
1402 assign(code.op0(), code.op1(), ns);
1403 }
1404 else if(statement==ID_decl)
1405 {
1406 if(code.operands().size()!=1)
1407 throw "decl expected to have one operand";
1408
1409 const exprt &lhs=code.op0();
1410
1411 if(lhs.id()!=ID_symbol)
1412 throw "decl expected to have symbol on lhs";
1413
1414 assign(lhs, exprt(ID_invalid, lhs.type()), ns);
1415 }
1416 else if(statement==ID_expression)
1417 {
1418 // can be ignored, we don't expect side effects here
1419 }
1420 else if(statement==ID_cpp_delete ||
1421 statement==ID_cpp_delete_array)
1422 {
1423 // does nothing
1424 }
1425 else if(statement=="lock" || statement=="unlock")
1426 {
1427 // ignore for now
1428 }
1429 else if(statement==ID_asm)
1430 {
1431 // ignore for now, probably not safe
1432 }
1433 else if(statement==ID_nondet)
1434 {
1435 // doesn't do anything
1436 }
1437 else if(statement==ID_printf)
1438 {
1439 // doesn't do anything
1440 }
1441 else if(statement==ID_return)
1442 {
1444 // this is turned into an assignment
1445 std::string rvs = "value_set::return_value" + std::to_string(from_function);
1446 symbol_exprt lhs(rvs, code_return.return_value().type());
1447 assign(lhs, code_return.return_value(), ns);
1448 }
1449 else if(statement==ID_fence)
1450 {
1451 }
1452 else if(
1453 statement == ID_array_copy || statement == ID_array_replace ||
1454 statement == ID_array_set || statement == ID_array_equal)
1455 {
1456 }
1458 {
1459 // doesn't do anything
1460 }
1461 else if(statement == ID_havoc_object)
1462 {
1463 }
1464 else
1465 throw
1466 code.pretty()+"\n"+
1467 "value_set_fit: unexpected statement: "+id2string(statement);
1468}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
goto_instruction_codet representation of a "return from a function" statement.
Base type of functions.
Definition std_types.h:583
std::vector< parametert > parameterst
Definition std_types.h:586
const parameterst & parameters() const
Definition std_types.h:699
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
bool empty() const
Definition dstring.h:89
void clear()
Definition dstring.h:159
Representation of heap-allocated objects.
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
Array index operator.
Definition std_expr.h:1470
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
const std::string & get_string(const irep_idt &name) const
Definition irep.h:401
Extract member of struct or union.
Definition std_expr.h:2972
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Split an expression into a base object and a (byte) offset.
const T & read() const
const irep_idt & get_statement() const
Definition std_code.h:1472
Expression to hold a symbol (variable)
Definition std_expr.h:131
Symbol table entry.
Definition symbol.h:28
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
The Boolean constant true.
Definition std_expr.h:3191
Type with a single subtype.
Definition type.h:180
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
data_typet::value_type value_type
data_typet::const_iterator const_iterator
static const object_map_dt blank
data_typet::iterator iterator
std::optional< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
static object_numberingt object_numbering
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
static numberingt< irep_idt > function_numbering
void add_var(const idt &id)
std::unordered_set< idt > assign_recursion_sett
bool make_union(object_mapt &dest, const object_mapt &src) const
std::vector< exprt > get_value_set(const exprt &expr, const namespacet &ns) const
unsigned from_function
void apply_code(const codet &code, const namespacet &ns)
void get_value_set_rec(const exprt &expr, object_mapt &dest, bool &includes_nondet_pointer, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
void dereference_rec(const exprt &src, exprt &dest) const
void output(const namespacet &ns, std::ostream &out) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
std::unordered_set< exprt, irep_hash > expr_sett
void do_end_function(const exprt &lhs, const namespacet &ns)
std::set< idt > flatten_seent
void flatten(const entryt &e, object_mapt &dest) const
bool offset_is_zero(const offsett &offset) const
entryt & get_entry(const idt &id, const std::string &suffix)
unsigned from_target_index
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
std::unordered_set< idt > gvs_recursion_sett
std::map< idt, entryt > valuest
exprt to_expr(const object_map_dt::value_type &it) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
static format_containert< T > format(const T &o)
Definition format.h:37
const code_returnt & to_code_return(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
bool simplify(exprt &expr, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1603
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2582
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3173
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2661
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
Definition std_types.h:478
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
Symbol table entry.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208
static const char * alloc_adapter_prefix
Value Set (Flow Insensitive, Sharing)