cprover
Loading...
Searching...
No Matches
goto_program.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_program.h"
13
14#include "validate_code.h"
15
16#include <iomanip>
17
18#include <util/base_type.h>
19#include <util/expr_iterator.h>
20#include <util/find_symbols.h>
21#include <util/format_expr.h>
22#include <util/format_type.h>
23#include <util/invariant.h>
24#include <util/pointer_expr.h>
25#include <util/std_code.h>
26#include <util/std_expr.h>
27#include <util/symbol_table.h>
28#include <util/validate.h>
29
31
32std::ostream &goto_programt::output(std::ostream &out) const
33{
34 return output(namespacet(symbol_tablet()), irep_idt(), out);
35}
36
43
58 const namespacet &ns,
59 const irep_idt &identifier,
60 std::ostream &out,
61 const instructiont &instruction) const
62{
63 out << " // " << instruction.location_number << " ";
64
65 if(!instruction.source_location().is_nil())
66 out << instruction.source_location().as_string();
67 else
68 out << "no location";
69
70 out << "\n";
71
72 if(!instruction.labels.empty())
73 {
74 out << " // Labels:";
75 for(const auto &label : instruction.labels)
76 out << " " << label;
77
78 out << '\n';
79 }
80
81 if(instruction.is_target())
82 out << std::setw(6) << instruction.target_number << ": ";
83 else
84 out << " ";
85
86 switch(instruction.type())
87 {
89 out << "NO INSTRUCTION TYPE SET" << '\n';
90 break;
91
92 case GOTO:
93 case INCOMPLETE_GOTO:
94 if(!instruction.get_condition().is_true())
95 {
96 out << "IF " << format(instruction.get_condition()) << " THEN ";
97 }
98
99 out << "GOTO ";
100
101 if(instruction.is_incomplete_goto())
102 {
103 out << "(incomplete)";
104 }
105 else
106 {
107 for(auto gt_it = instruction.targets.begin();
108 gt_it != instruction.targets.end();
109 gt_it++)
110 {
111 if(gt_it != instruction.targets.begin())
112 out << ", ";
113 out << (*gt_it)->target_number;
114 }
115 }
116
117 out << '\n';
118 break;
119
120 case OTHER:
121 if(instruction.get_other().id() == ID_code)
122 {
123 const auto &code = instruction.get_other();
124 if(code.get_statement() == ID_havoc_object)
125 {
126 out << "HAVOC_OBJECT " << format(code.op0()) << '\n';
127 break;
128 }
129 // fallthrough
130 }
131
132 out << "OTHER " << format(instruction.get_other()) << '\n';
133 break;
134
135 case SET_RETURN_VALUE:
136 out << "SET RETURN VALUE " << format(instruction.return_value()) << '\n';
137 break;
138
139 case DECL:
140 out << "DECL " << format(instruction.decl_symbol()) << " : "
141 << format(instruction.decl_symbol().type()) << '\n';
142 break;
143
144 case DEAD:
145 out << "DEAD " << format(instruction.dead_symbol()) << '\n';
146 break;
147
148 case FUNCTION_CALL:
149 out << "CALL ";
150 {
151 if(instruction.call_lhs().is_not_nil())
152 out << format(instruction.call_lhs()) << " := ";
153 out << format(instruction.call_function());
154 out << '(';
155 bool first = true;
156 for(const auto &argument : instruction.call_arguments())
157 {
158 if(first)
159 first = false;
160 else
161 out << ", ";
162 out << format(argument);
163 }
164 out << ')';
165 out << '\n';
166 }
167 break;
168
169 case ASSIGN:
170 out << "ASSIGN " << format(instruction.assign_lhs())
171 << " := " << format(instruction.assign_rhs()) << '\n';
172 break;
173
174 case ASSUME:
175 case ASSERT:
176 if(instruction.is_assume())
177 out << "ASSUME ";
178 else
179 out << "ASSERT ";
180
181 {
182 out << format(instruction.get_condition());
183
184 const irep_idt &comment = instruction.source_location().get_comment();
185 if(!comment.empty())
186 out << " // " << comment;
187 }
188
189 out << '\n';
190 break;
191
192 case SKIP:
193 out << "SKIP" << '\n';
194 break;
195
196 case END_FUNCTION:
197 out << "END_FUNCTION" << '\n';
198 break;
199
200 case LOCATION:
201 out << "LOCATION" << '\n';
202 break;
203
204 case THROW:
205 out << "THROW";
206
207 {
208 const irept::subt &exception_list =
209 instruction.get_code().find(ID_exception_list).get_sub();
210
211 for(const auto &ex : exception_list)
212 out << " " << ex.id();
213 }
214
215 if(instruction.get_code().operands().size() == 1)
216 out << ": " << format(instruction.get_code().op0());
217
218 out << '\n';
219 break;
220
221 case CATCH:
222 {
223 if(instruction.get_code().get_statement() == ID_exception_landingpad)
224 {
225 const auto &landingpad = to_code_landingpad(instruction.get_code());
226 out << "EXCEPTION LANDING PAD (" << format(landingpad.catch_expr().type())
227 << ' ' << format(landingpad.catch_expr()) << ")";
228 }
229 else if(instruction.get_code().get_statement() == ID_push_catch)
230 {
231 out << "CATCH-PUSH ";
232
233 unsigned i=0;
234 const irept::subt &exception_list =
235 instruction.get_code().find(ID_exception_list).get_sub();
237 instruction.targets.size() == exception_list.size(),
238 "unexpected discrepancy between sizes of instruction"
239 "targets and exception list");
240 for(instructiont::targetst::const_iterator
241 gt_it=instruction.targets.begin();
242 gt_it!=instruction.targets.end();
243 gt_it++, i++)
244 {
245 if(gt_it!=instruction.targets.begin())
246 out << ", ";
247 out << exception_list[i].id() << "->"
248 << (*gt_it)->target_number;
249 }
250 }
251 else if(instruction.get_code().get_statement() == ID_pop_catch)
252 {
253 out << "CATCH-POP";
254 }
255 else
256 {
258 }
259
260 out << '\n';
261 break;
262 }
263
264 case ATOMIC_BEGIN:
265 out << "ATOMIC_BEGIN" << '\n';
266 break;
267
268 case ATOMIC_END:
269 out << "ATOMIC_END" << '\n';
270 break;
271
272 case START_THREAD:
273 out << "START THREAD "
274 << instruction.get_target()->target_number
275 << '\n';
276 break;
277
278 case END_THREAD:
279 out << "END THREAD" << '\n';
280 break;
281 }
282
283 return out;
284}
285
288{
289 for(const auto &instruction : instructions)
290 {
291 if(instruction.is_decl())
292 {
294 instruction.get_code().get_statement() == ID_decl,
295 "expected statement to be declaration statement");
297 instruction.get_code().operands().size() == 1,
298 "declaration statement expects one operand");
299 decl_identifiers.insert(instruction.decl_symbol().get_identifier());
300 }
301 }
302}
303
304void parse_lhs_read(const exprt &src, std::list<exprt> &dest)
305{
306 if(src.id()==ID_dereference)
307 {
308 dest.push_back(to_dereference_expr(src).pointer());
309 }
310 else if(src.id()==ID_index)
311 {
312 auto &index_expr = to_index_expr(src);
313 dest.push_back(index_expr.index());
315 }
316 else if(src.id()==ID_member)
317 {
318 parse_lhs_read(to_member_expr(src).compound(), dest);
319 }
320 else if(src.id()==ID_if)
321 {
322 auto &if_expr = to_if_expr(src);
323 dest.push_back(if_expr.cond());
324 parse_lhs_read(if_expr.true_case(), dest);
325 parse_lhs_read(if_expr.false_case(), dest);
326 }
327}
328
329std::list<exprt> expressions_read(
330 const goto_programt::instructiont &instruction)
331{
332 std::list<exprt> dest;
333
334 switch(instruction.type())
335 {
336 case ASSUME:
337 case ASSERT:
338 case GOTO:
339 dest.push_back(instruction.get_condition());
340 break;
341
342 case SET_RETURN_VALUE:
343 dest.push_back(instruction.return_value());
344 break;
345
346 case FUNCTION_CALL:
347 for(const auto &argument : instruction.call_arguments())
348 dest.push_back(argument);
349 if(instruction.call_lhs().is_not_nil())
350 parse_lhs_read(instruction.call_lhs(), dest);
351 break;
352
353 case ASSIGN:
354 dest.push_back(instruction.assign_rhs());
355 parse_lhs_read(instruction.assign_lhs(), dest);
356 break;
357
358 case CATCH:
359 case THROW:
360 case DEAD:
361 case DECL:
362 case ATOMIC_BEGIN:
363 case ATOMIC_END:
364 case START_THREAD:
365 case END_THREAD:
366 case END_FUNCTION:
367 case LOCATION:
368 case SKIP:
369 case OTHER:
370 case INCOMPLETE_GOTO:
372 break;
373 }
374
375 return dest;
376}
377
378std::list<exprt> expressions_written(
379 const goto_programt::instructiont &instruction)
380{
381 std::list<exprt> dest;
382
383 switch(instruction.type())
384 {
385 case FUNCTION_CALL:
386 if(instruction.call_lhs().is_not_nil())
387 dest.push_back(instruction.call_lhs());
388 break;
389
390 case ASSIGN:
391 dest.push_back(instruction.assign_lhs());
392 break;
393
394 case CATCH:
395 case THROW:
396 case GOTO:
397 case SET_RETURN_VALUE:
398 case DEAD:
399 case DECL:
400 case ATOMIC_BEGIN:
401 case ATOMIC_END:
402 case START_THREAD:
403 case END_THREAD:
404 case END_FUNCTION:
405 case ASSERT:
406 case ASSUME:
407 case LOCATION:
408 case SKIP:
409 case OTHER:
410 case INCOMPLETE_GOTO:
412 break;
413 }
414
415 return dest;
416}
417
419 const exprt &src,
420 std::list<exprt> &dest)
421{
422 if(src.id()==ID_symbol)
423 dest.push_back(src);
424 else if(src.id()==ID_address_of)
425 {
426 // don't traverse!
427 }
428 else if(src.id()==ID_dereference)
429 {
430 // this reads what is pointed to plus the pointer
431 auto &deref = to_dereference_expr(src);
432 dest.push_back(deref);
433 objects_read(deref.pointer(), dest);
434 }
435 else
436 {
437 forall_operands(it, src)
438 objects_read(*it, dest);
439 }
440}
441
442std::list<exprt> objects_read(
443 const goto_programt::instructiont &instruction)
444{
445 std::list<exprt> expressions=expressions_read(instruction);
446
447 std::list<exprt> dest;
448
449 for(const auto &expr : expressions)
450 objects_read(expr, dest);
451
452 return dest;
453}
454
456 const exprt &src,
457 std::list<exprt> &dest)
458{
459 if(src.id()==ID_if)
460 {
461 auto &if_expr = to_if_expr(src);
462 objects_written(if_expr.true_case(), dest);
463 objects_written(if_expr.false_case(), dest);
464 }
465 else
466 dest.push_back(src);
467}
468
469std::list<exprt> objects_written(
470 const goto_programt::instructiont &instruction)
471{
472 std::list<exprt> expressions=expressions_written(instruction);
473
474 std::list<exprt> dest;
475
476 for(const auto &expr : expressions)
477 objects_written(expr, dest);
478
479 return dest;
480}
481
482std::string as_string(
483 const class namespacet &ns,
484 const irep_idt &function,
486{
487 std::string result;
488
489 switch(i.type())
490 {
492 return "(NO INSTRUCTION TYPE)";
493
494 case GOTO:
495 if(!i.get_condition().is_true())
496 {
497 result += "IF " + from_expr(ns, function, i.get_condition()) + " THEN ";
498 }
499
500 result+="GOTO ";
501
502 for(goto_programt::instructiont::targetst::const_iterator
503 gt_it=i.targets.begin();
504 gt_it!=i.targets.end();
505 gt_it++)
506 {
507 if(gt_it!=i.targets.begin())
508 result+=", ";
509 result+=std::to_string((*gt_it)->target_number);
510 }
511 return result;
512
513 case SET_RETURN_VALUE:
514 case OTHER:
515 case DECL:
516 case DEAD:
517 case FUNCTION_CALL:
518 case ASSIGN:
519 return from_expr(ns, function, i.get_code());
520
521 case ASSUME:
522 case ASSERT:
523 if(i.is_assume())
524 result+="ASSUME ";
525 else
526 result+="ASSERT ";
527
528 result += from_expr(ns, function, i.get_condition());
529
530 {
531 const irep_idt &comment = i.source_location().get_comment();
532 if(!comment.empty())
533 result+=" /* "+id2string(comment)+" */";
534 }
535 return result;
536
537 case SKIP:
538 return "SKIP";
539
540 case END_FUNCTION:
541 return "END_FUNCTION";
542
543 case LOCATION:
544 return "LOCATION";
545
546 case THROW:
547 return "THROW";
548
549 case CATCH:
550 return "CATCH";
551
552 case ATOMIC_BEGIN:
553 return "ATOMIC_BEGIN";
554
555 case ATOMIC_END:
556 return "ATOMIC_END";
557
558 case START_THREAD:
559 result+="START THREAD ";
560
561 if(i.targets.size()==1)
562 result+=std::to_string(i.targets.front()->target_number);
563 return result;
564
565 case END_THREAD:
566 return "END THREAD";
567
568 case INCOMPLETE_GOTO:
570 }
571
573}
574
579{
580 unsigned nr=0;
581 for(auto &i : instructions)
582 if(i.is_backwards_goto())
583 i.loop_number=nr++;
584}
585
593
595 const namespacet &ns,
596 const irep_idt &identifier,
597 std::ostream &out) const
598{
599 // output program
600
601 for(const auto &instruction : instructions)
602 output_instruction(ns, identifier, out, instruction);
603
604 return out;
605}
606
618{
619 // reset marking
620
621 for(auto &i : instructions)
622 i.target_number=instructiont::nil_target;
623
624 // mark the goto targets
625
626 for(const auto &i : instructions)
627 {
628 for(const auto &t : i.targets)
629 {
630 if(t!=instructions.end())
631 t->target_number=0;
632 }
633 }
634
635 // number the targets properly
636 unsigned cnt=0;
637
638 for(auto &i : instructions)
639 {
640 if(i.is_target())
641 {
642 i.target_number=++cnt;
644 i.target_number != 0, "GOTO instruction target cannot be zero");
645 }
646 }
647
648 // check the targets!
649 // (this is a consistency check only)
650
651 for(const auto &i : instructions)
652 {
653 for(const auto &t : i.targets)
654 {
655 if(t!=instructions.end())
656 {
658 t->target_number != 0, "instruction's number cannot be zero");
660 t->target_number != instructiont::nil_target,
661 "GOTO instruction target cannot be nil_target");
662 }
663 }
664 }
665}
666
672{
673 // Definitions for mapping between the two programs
674 typedef std::map<const_targett, targett> targets_mappingt;
676
677 clear();
678
679 // Loop over program - 1st time collects targets and copy
680
681 for(instructionst::const_iterator
682 it=src.instructions.begin();
683 it!=src.instructions.end();
684 ++it)
685 {
686 auto new_instruction=add_instruction();
687 targets_mapping[it]=new_instruction;
688 *new_instruction=*it;
689 }
690
691 // Loop over program - 2nd time updates targets
692
693 for(auto &i : instructions)
694 {
695 for(auto &t : i.targets)
696 {
697 targets_mappingt::iterator
699
701
702 t=m_target_it->second;
703 }
704 }
705
708}
709
713{
714 for(const auto &i : instructions)
715 if(i.is_assert() && !i.get_condition().is_true())
716 return true;
717
718 return false;
719}
720
723{
724 for(auto &i : instructions)
725 {
726 i.incoming_edges.clear();
727 }
728
729 for(instructionst::iterator
730 it=instructions.begin();
731 it!=instructions.end();
732 ++it)
733 {
734 for(const auto &s : get_successors(it))
735 {
736 if(s!=instructions.end())
737 s->incoming_edges.insert(it);
738 }
739 }
740}
741
743{
744 // clang-format off
745 return
746 _type == other._type &&
747 code == other.code &&
748 guard == other.guard &&
749 targets.size() == other.targets.size() &&
750 labels == other.labels;
751 // clang-format on
752}
753
755 const namespacet &ns,
756 const validation_modet vm) const
757{
758 validate_full_code(code, ns, vm);
759 validate_full_expr(guard, ns, vm);
760
761 auto expr_symbol_finder = [&](const exprt &e) {
763 find_type_symbols(e.type(), typetags);
765 const symbolt *symbol;
766 for(const auto &identifier : typetags)
767 {
769 vm,
770 !ns.lookup(identifier, symbol),
771 id2string(identifier) + " not found",
772 source_location());
773 }
774 };
775
776 auto &current_source_location = source_location();
777 auto type_finder =
778 [&ns, vm, &current_source_location](const exprt &e) {
779 if(e.id() == ID_symbol)
780 {
781 const auto &goto_symbol_expr = to_symbol_expr(e);
782 const auto &goto_id = goto_symbol_expr.get_identifier();
783
784 const symbolt *table_symbol;
785 if(!ns.lookup(goto_id, table_symbol))
786 {
788 base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns);
789
790 if(
792 table_symbol->type.id() == ID_code)
793 {
794 // If a function declaration and its definition are in different
795 // translation units they may have different return types.
796 // Thus, the return type in the symbol table may differ
797 // from the return type in the symbol expr.
798 if(
799 goto_symbol_expr.type().source_location().get_file() !=
800 table_symbol->type.source_location().get_file())
801 {
802 // temporarily fixup the return types
806
807 goto_symbol_expr_type.return_type() =
808 table_symbol_type.return_type();
809
812 }
813 }
814
815 if(
817 goto_symbol_expr.type().id() == ID_array &&
819 {
820 // If the symbol expr has an incomplete array type, it may not have
821 // a constant size value, whereas the symbol table entry may have
822 // an (assumed) constant size of 1 (which mimics gcc behaviour)
823 if(table_symbol->type.id() == ID_array)
824 {
827
830 }
831 }
832
834 vm,
836 id2string(goto_id) + " type inconsistency\n" +
837 "goto program type: " + goto_symbol_expr.type().id_string() +
838 "\n" + "symbol table type: " + table_symbol->type.id_string(),
840 }
841 }
842 };
843
844 const symbolt *table_symbol;
845 switch(_type)
846 {
848 break;
849 case GOTO:
851 vm,
852 has_target(),
853 "goto instruction expects at least one target",
854 source_location());
855 // get_target checks that targets.size()==1
857 vm,
858 get_target()->is_target() && get_target()->target_number != 0,
859 "goto target has to be a target",
860 source_location());
861 break;
862 case ASSUME:
864 vm,
865 targets.empty(),
866 "assume instruction should not have a target",
867 source_location());
868 break;
869 case ASSERT:
871 vm,
872 targets.empty(),
873 "assert instruction should not have a target",
874 source_location());
875
876 std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
877 std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
878 break;
879 case OTHER:
880 break;
881 case SKIP:
882 break;
883 case START_THREAD:
884 break;
885 case END_THREAD:
886 break;
887 case LOCATION:
888 break;
889 case END_FUNCTION:
890 break;
891 case ATOMIC_BEGIN:
892 break;
893 case ATOMIC_END:
894 break;
895 case SET_RETURN_VALUE:
897 vm,
898 code.get_statement() == ID_return,
899 "SET_RETURN_VALUE instruction should contain a return statement",
900 source_location());
901 break;
902 case ASSIGN:
904 vm,
905 code.get_statement() == ID_assign,
906 "assign instruction should contain an assign statement");
908 vm, targets.empty(), "assign instruction should not have a target");
909 break;
910 case DECL:
912 vm,
913 code.get_statement() == ID_decl,
914 "declaration instructions should contain a declaration statement",
915 source_location());
917 vm,
918 !ns.lookup(decl_symbol().get_identifier(), table_symbol),
919 "declared symbols should be known",
920 id2string(decl_symbol().get_identifier()),
921 source_location());
922 break;
923 case DEAD:
925 vm,
926 code.get_statement() == ID_dead,
927 "dead instructions should contain a dead statement",
928 source_location());
930 vm,
931 !ns.lookup(dead_symbol().get_identifier(), table_symbol),
932 "removed symbols should be known",
933 id2string(dead_symbol().get_identifier()),
934 source_location());
935 break;
936 case FUNCTION_CALL:
938 vm,
939 code.get_statement() == ID_function_call,
940 "function call instruction should contain a call statement",
941 source_location());
942
943 std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
944 std::for_each(code.depth_begin(), code.depth_end(), type_finder);
945 break;
946 case THROW:
947 break;
948 case CATCH:
949 break;
950 case INCOMPLETE_GOTO:
951 break;
952 }
953}
954
956 std::function<optionalt<exprt>(exprt)> f)
957{
958 switch(_type)
959 {
960 case OTHER:
961 if(get_other().get_statement() == ID_expression)
962 {
963 auto new_expression = f(to_code_expression(get_other()).expression());
964 if(new_expression.has_value())
965 {
966 auto new_other = to_code_expression(get_other());
967 new_other.expression() = *new_expression;
968 set_other(new_other);
969 }
970 }
971 break;
972
973 case SET_RETURN_VALUE:
974 {
975 auto new_return_value = f(return_value());
976 if(new_return_value.has_value())
977 return_value() = *new_return_value;
978 }
979 break;
980
981 case ASSIGN:
982 {
983 auto new_assign_lhs = f(assign_lhs());
984 auto new_assign_rhs = f(assign_rhs());
985 if(new_assign_lhs.has_value())
986 assign_lhs_nonconst() = new_assign_lhs.value();
987 if(new_assign_rhs.has_value())
988 assign_rhs_nonconst() = new_assign_rhs.value();
989 }
990 break;
991
992 case DECL:
993 {
994 auto new_symbol = f(decl_symbol());
995 if(new_symbol.has_value())
996 decl_symbol() = to_symbol_expr(*new_symbol);
997 }
998 break;
999
1000 case DEAD:
1001 {
1002 auto new_symbol = f(dead_symbol());
1003 if(new_symbol.has_value())
1004 dead_symbol() = to_symbol_expr(*new_symbol);
1005 }
1006 break;
1007
1008 case FUNCTION_CALL:
1009 {
1010 auto new_lhs = f(as_const(*this).call_lhs());
1011 if(new_lhs.has_value())
1012 call_lhs() = *new_lhs;
1013
1014 auto new_call_function = f(as_const(*this).call_function());
1015 if(new_call_function.has_value())
1016 call_function() = *new_call_function;
1017
1018 exprt::operandst new_arguments = as_const(*this).call_arguments();
1019 bool argument_changed = false;
1020
1021 for(auto &a : new_arguments)
1022 {
1023 auto new_a = f(a);
1024 if(new_a.has_value())
1025 {
1026 a = *new_a;
1027 argument_changed = true;
1028 }
1029 }
1030
1032 call_arguments() = std::move(new_arguments);
1033 }
1034 break;
1035
1036 case GOTO:
1037 case ASSUME:
1038 case ASSERT:
1039 case SKIP:
1040 case START_THREAD:
1041 case END_THREAD:
1042 case LOCATION:
1043 case END_FUNCTION:
1044 case ATOMIC_BEGIN:
1045 case ATOMIC_END:
1046 case THROW:
1047 case CATCH:
1048 case INCOMPLETE_GOTO:
1050 if(has_condition())
1051 {
1052 auto new_condition = f(get_condition());
1053 if(new_condition.has_value())
1054 set_condition(new_condition.value());
1055 }
1056 }
1057}
1058
1060 std::function<void(const exprt &)> f) const
1061{
1062 switch(_type)
1063 {
1064 case OTHER:
1065 if(get_other().get_statement() == ID_expression)
1066 f(to_code_expression(get_other()).expression());
1067 break;
1068
1069 case SET_RETURN_VALUE:
1070 f(return_value());
1071 break;
1072
1073 case ASSIGN:
1074 f(assign_lhs());
1075 f(assign_rhs());
1076 break;
1077
1078 case DECL:
1079 f(decl_symbol());
1080 break;
1081
1082 case DEAD:
1083 f(dead_symbol());
1084 break;
1085
1086 case FUNCTION_CALL:
1087 f(call_lhs());
1088 for(auto &a : call_arguments())
1089 f(a);
1090 break;
1091
1092 case GOTO:
1093 case ASSUME:
1094 case ASSERT:
1095 case SKIP:
1096 case START_THREAD:
1097 case END_THREAD:
1098 case LOCATION:
1099 case END_FUNCTION:
1100 case ATOMIC_BEGIN:
1101 case ATOMIC_END:
1102 case THROW:
1103 case CATCH:
1104 case INCOMPLETE_GOTO:
1106 if(has_condition())
1107 f(get_condition());
1108 }
1109}
1110
1111bool goto_programt::equals(const goto_programt &other) const
1112{
1113 if(instructions.size() != other.instructions.size())
1114 return false;
1115
1117 for(const auto &ins : instructions)
1118 {
1119 if(!ins.equals(*other_it))
1120 return false;
1121
1122 // the number of targets is the same as instructiont::equals returned "true"
1123 auto other_target_it = other_it->targets.begin();
1124 for(const auto &t : ins.targets)
1125 {
1126 if(
1127 t->location_number - ins.location_number !=
1128 (*other_target_it)->location_number - other_it->location_number)
1129 {
1130 return false;
1131 }
1132
1134 }
1135
1136 ++other_it;
1137 }
1138
1139 return true;
1140}
1141
1143std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t)
1144{
1145 switch(t)
1146 {
1148 out << "NO_INSTRUCTION_TYPE";
1149 break;
1150 case GOTO:
1151 out << "GOTO";
1152 break;
1153 case ASSUME:
1154 out << "ASSUME";
1155 break;
1156 case ASSERT:
1157 out << "ASSERT";
1158 break;
1159 case OTHER:
1160 out << "OTHER";
1161 break;
1162 case DECL:
1163 out << "DECL";
1164 break;
1165 case DEAD:
1166 out << "DEAD";
1167 break;
1168 case SKIP:
1169 out << "SKIP";
1170 break;
1171 case START_THREAD:
1172 out << "START_THREAD";
1173 break;
1174 case END_THREAD:
1175 out << "END_THREAD";
1176 break;
1177 case LOCATION:
1178 out << "LOCATION";
1179 break;
1180 case END_FUNCTION:
1181 out << "END_FUNCTION";
1182 break;
1183 case ATOMIC_BEGIN:
1184 out << "ATOMIC_BEGIN";
1185 break;
1186 case ATOMIC_END:
1187 out << "ATOMIC_END";
1188 break;
1189 case SET_RETURN_VALUE:
1190 out << "SET_RETURN_VALUE";
1191 break;
1192 case ASSIGN:
1193 out << "ASSIGN";
1194 break;
1195 case FUNCTION_CALL:
1196 out << "FUNCTION_CALL";
1197 break;
1198 case THROW:
1199 out << "THROW";
1200 break;
1201 case CATCH:
1202 out << "CATCH";
1203 break;
1204 case INCOMPLETE_GOTO:
1205 out << "INCOMPLETE_GOTO";
1206 break;
1207 }
1208
1209 return out;
1210}
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Base Type Computation.
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
bool is_incomplete() const
Definition std_types.h:805
codet representation of a goto statement.
Definition std_code.h:841
exprt & op0()
Definition expr.h:99
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:33
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
unsigned target_number
A number to identify branch targets.
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
bool is_target() const
Is this node a branch target?
codet code
Do not read or modify directly – use get_X() instead.
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
const codet & get_code() const
Get the code represented by this instruction.
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
targetst targets
The list of successor instructions.
const codet & get_other() const
Get the statement for OTHER.
goto_program_instruction_typet _type
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
unsigned location_number
A globally unique number to identify a program location.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
static const unsigned nil_target
Uniquely identify an invalid target or location.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
exprt guard
Guard for gotos, assume, assert Use condition() method to access.
const source_locationt & source_location() const
goto_program_instruction_typet type() const
What kind of instruction?
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void clear()
Clear the goto program.
void update()
Update all indices.
bool has_assertion() const
Does the goto program have an assertion?
instructionst::const_iterator const_targett
targett add_instruction()
Adds an instruction at the end.
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
std::set< irep_idt > decl_identifierst
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
void compute_location_numbers()
Compute location numbers.
void compute_target_numbers()
Compute the target numbers.
bool equals(const goto_programt &other) const
Syntactic equality: two goto_programt are equal if, and only if, they have the same number of instruc...
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
void compute_loop_numbers()
Compute loop numbers.
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
bool is_not_nil() const
Definition irep.h:380
subt & get_sub()
Definition irep.h:456
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
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().
The NIL expression.
Definition std_expr.h:2874
std::string as_string() const
const irep_idt & get_comment() const
The symbol table.
Symbol table entry.
Definition symbol.h:28
The Boolean constant true.
Definition std_expr.h:2856
#define forall_operands(it, expr)
Definition expr.h:18
Forward depth-first search iterators These iterators' copy operations are expensive,...
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
std::unordered_set< irep_idt > find_symbols_sett
static format_containert< T > format(const T &o)
Definition format.h:37
void parse_lhs_read(const exprt &src, std::list< exprt > &dest)
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
std::string as_string(const class namespacet &ns, const irep_idt &function, const goto_programt::instructiont &i)
void objects_read(const exprt &src, std::list< exprt > &dest)
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
void objects_written(const exprt &src, std::list< exprt > &dest)
Concrete Goto Program.
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
Outputs a string representation of a goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
dstringt irep_idt
Definition irep.h:37
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
static code_landingpadt & to_code_landingpad(codet &code)
Definition std_code.h:1972
code_expressiont & to_code_expression(codet &code)
Definition std_code.h:1428
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832
Author: Diffblue Ltd.
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
Definition validate.h:37
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
void validate_full_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed (full check, including checks of all subexpression...
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
validation_modet