cprover
goto_program.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: 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 
30 #include <langapi/language_util.h>
31 
32 std::ostream &goto_programt::output(std::ostream &out) const
33 {
34  return output(namespacet(symbol_tablet()), irep_idt(), out);
35 }
36 
38  const code_gotot &_code,
39  const source_locationt &l)
40 {
41  return instructiont(_code, l, INCOMPLETE_GOTO, true_exprt(), {});
42 }
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  {
257  UNREACHABLE;
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 
287  decl_identifierst &decl_identifiers) const
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 
304 void 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());
314  parse_lhs_read(index_expr.array(), dest);
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 
329 std::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:
371  case NO_INSTRUCTION_TYPE:
372  break;
373  }
374 
375  return dest;
376 }
377 
378 std::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:
411  case NO_INSTRUCTION_TYPE:
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 
442 std::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 
469 std::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 
482 std::string as_string(
483  const class namespacet &ns,
484  const irep_idt &function,
486 {
487  std::string result;
488 
489  switch(i.type())
490  {
491  case NO_INSTRUCTION_TYPE:
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  {
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:
569  UNREACHABLE;
570  }
571 
572  UNREACHABLE;
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 
587 {
592 }
593 
594 std::ostream &goto_programt::output(
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;
675  targets_mappingt targets_mapping;
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
698  m_target_it=targets_mapping.find(t);
699 
700  CHECK_RETURN(m_target_it != targets_mapping.end());
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) {
762  find_symbols_sett typetags;
763  find_type_symbols(e.type(), typetags);
764  find_symbols_or_nexts(e, 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  {
787  bool symbol_expr_type_matches_symbol_table =
788  base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns);
789 
790  if(
791  !symbol_expr_type_matches_symbol_table &&
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
803  auto goto_symbol_expr_type =
804  to_code_type(goto_symbol_expr.type());
805  auto table_symbol_type = to_code_type(table_symbol->type);
806 
807  goto_symbol_expr_type.return_type() =
808  table_symbol_type.return_type();
809 
810  symbol_expr_type_matches_symbol_table =
811  base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
812  }
813  }
814 
815  if(
816  !symbol_expr_type_matches_symbol_table &&
817  goto_symbol_expr.type().id() == ID_array &&
818  to_array_type(goto_symbol_expr.type()).is_incomplete())
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  {
825  auto symbol_table_array_type = to_array_type(table_symbol->type);
826  symbol_table_array_type.size() = nil_exprt();
827 
828  symbol_expr_type_matches_symbol_table =
829  goto_symbol_expr.type() == symbol_table_array_type;
830  }
831  }
832 
834  vm,
835  symbol_expr_type_matches_symbol_table,
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(),
839  current_source_location);
840  }
841  }
842  };
843 
844  const symbolt *table_symbol;
845  switch(_type)
846  {
847  case NO_INSTRUCTION_TYPE:
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:
903  DATA_CHECK(
904  vm,
905  code.get_statement() == ID_assign,
906  "assign instruction should contain an assign statement");
907  DATA_CHECK(
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 
1031  if(argument_changed)
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:
1049  case NO_INSTRUCTION_TYPE:
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:
1105  case NO_INSTRUCTION_TYPE:
1106  if(has_condition())
1107  f(get_condition());
1108  }
1109 }
1110 
1111 bool goto_programt::equals(const goto_programt &other) const
1112 {
1113  if(instructions.size() != other.instructions.size())
1114  return false;
1115 
1116  goto_programt::const_targett other_it = other.instructions.begin();
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 
1133  ++other_target_it;
1134  }
1135 
1136  ++other_it;
1137  }
1138 
1139  return true;
1140 }
1141 
1143 std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t)
1144 {
1145  switch(t)
1146  {
1147  case NO_INSTRUCTION_TYPE:
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.
Definition: base_type.cpp:291
Base Type Computation.
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
Definition: std_code_base.h:65
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.
Definition: goto_program.h:180
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:547
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:285
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:434
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:313
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:271
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
targetst targets
The list of successor instructions.
Definition: goto_program.h:403
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:257
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:367
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
goto_program_instruction_typet _type
Definition: goto_program.h:351
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:540
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:534
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:213
const source_locationt & source_location() const
Definition: goto_program.h:332
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:243
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:407
exprt guard
Guard for gotos, assume, assert Use condition() method to access.
Definition: goto_program.h:357
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:227
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:343
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:299
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void clear()
Clear the goto program.
Definition: goto_program.h:809
void update()
Update all indices.
bool has_assertion() const
Does the goto program have an assertion?
instructionst::const_iterator const_targett
Definition: goto_program.h:593
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:723
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:842
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.
Definition: goto_program.h:767
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())
Definition: goto_program.h:996
void compute_loop_numbers()
Compute loop numbers.
subt & get_sub()
Definition: irep.h:456
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const std::string & id_string() const
Definition: irep.h:399
bool is_not_nil() const
Definition: irep.h:380
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().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2874
const irep_idt & get_comment() const
const irep_idt & get_file() const
std::string as_string() const
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
The Boolean constant true.
Definition: std_expr.h:2856
const source_locationt & source_location() const
Definition: type.h:74
#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
Definition: find_symbols.h:21
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::ostream & operator<<(std::ostream &out, goto_program_instruction_typet t)
Outputs a string representation of a goto_program_instruction_typet
void objects_written(const exprt &src, std::list< exprt > &dest)
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
Concrete Goto Program.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:32
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ LOCATION
Definition: goto_program.h:41
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
@ ASSUME
Definition: goto_program.h:35
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)
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
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 if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
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
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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