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