cprover
goto_instrument_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Main Module
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <fstream>
15 #include <iostream>
16 #include <memory>
17 #include <sstream>
18 
19 #include <util/exception_utils.h>
20 #include <util/exit_codes.h>
21 #include <util/json.h>
22 #include <util/string2int.h>
23 #include <util/string_utils.h>
24 #include <util/version.h>
25 
26 #ifdef _MSC_VER
27 # include <util/unicode.h>
28 #endif
29 
36 #include <goto-programs/loop_ids.h>
53 
57 
58 #include <analyses/call_graph.h>
66 #include <analyses/is_threaded.h>
67 #include <analyses/lexical_loops.h>
70 #include <analyses/natural_loops.h>
72 #include <analyses/sese_regions.h>
73 
74 #include <ansi-c/ansi_c_language.h>
76 #include <ansi-c/cprover_library.h>
77 
78 #include <assembler/remove_asm.h>
79 
80 #include <cpp/cprover_library.h>
81 
82 #include "accelerate/accelerate.h"
83 #include "alignment_checks.h"
84 #include "branch.h"
85 #include "call_sequences.h"
86 #include "concurrency.h"
87 #include "dot.h"
88 #include "full_slicer.h"
89 #include "function.h"
90 #include "havoc_loops.h"
91 #include "horn_encoding.h"
93 #include "interrupt.h"
94 #include "k_induction.h"
95 #include "mmio.h"
96 #include "nondet_static.h"
97 #include "nondet_volatile.h"
98 #include "points_to.h"
99 #include "race_check.h"
100 #include "reachability_slicer.h"
101 #include "remove_function.h"
102 #include "rw_set.h"
103 #include "show_locations.h"
104 #include "skip_loops.h"
105 #include "splice_call.h"
106 #include "stack_depth.h"
107 #include "thread_instrumentation.h"
108 #include "undefined_functions.h"
109 #include "unwind.h"
110 #include "value_set_fi_fp_removal.h"
111 
114 {
115  if(cmdline.isset("version"))
116  {
117  std::cout << CBMC_VERSION << '\n';
118  return CPROVER_EXIT_SUCCESS;
119  }
120 
121  if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
122  {
123  help();
125  }
126 
129 
130  {
132 
134 
135  {
136  const bool validate_only = cmdline.isset("validate-goto-binary");
137 
138  if(validate_only || cmdline.isset("validate-goto-model"))
139  {
141 
142  if(validate_only)
143  {
144  return CPROVER_EXIT_SUCCESS;
145  }
146  }
147  }
148 
150 
151  if(cmdline.isset("validate-goto-model"))
152  {
154  }
155 
156  {
157  bool unwind_given=cmdline.isset("unwind");
158  bool unwindset_given=cmdline.isset("unwindset");
159  bool unwindset_file_given=cmdline.isset("unwindset-file");
160 
161  if(unwindset_given && unwindset_file_given)
162  throw "only one of --unwindset and --unwindset-file supported at a "
163  "time";
164 
165  if(unwind_given || unwindset_given || unwindset_file_given)
166  {
167  unwindsett unwindset{goto_model};
168 
169  if(unwind_given)
170  unwindset.parse_unwind(cmdline.get_value("unwind"));
171 
172  if(unwindset_file_given)
173  {
174  unwindset.parse_unwindset_file(
175  cmdline.get_value("unwindset-file"), ui_message_handler);
176  }
177 
178  if(unwindset_given)
179  {
180  unwindset.parse_unwindset(
181  cmdline.get_values("unwindset"), ui_message_handler);
182  }
183 
184  bool unwinding_assertions=cmdline.isset("unwinding-assertions");
185  bool partial_loops=cmdline.isset("partial-loops");
186  bool continue_as_loops=cmdline.isset("continue-as-loops");
187 
188  if(unwinding_assertions+partial_loops+continue_as_loops>1)
189  throw "more than one of --unwinding-assertions,--partial-loops,"
190  "--continue-as-loops selected";
191 
192  goto_unwindt::unwind_strategyt unwind_strategy=
194 
195  if(unwinding_assertions)
196  {
198  }
199  else if(partial_loops)
200  {
202  }
203  else if(continue_as_loops)
204  {
206  }
207 
208  goto_unwindt goto_unwind;
209  goto_unwind(goto_model, unwindset, unwind_strategy);
210 
211  if(cmdline.isset("log"))
212  {
213  std::string filename=cmdline.get_value("log");
214  bool have_file=!filename.empty() && filename!="-";
215 
216  jsont result=goto_unwind.output_log_json();
217 
218  if(have_file)
219  {
220 #ifdef _MSC_VER
221  std::ofstream of(widen(filename));
222 #else
223  std::ofstream of(filename);
224 #endif
225  if(!of)
226  throw "failed to open file "+filename;
227 
228  of << result;
229  of.close();
230  }
231  else
232  {
233  std::cout << result << '\n';
234  }
235  }
236 
237  // goto_unwind holds references to instructions, only do remove_skip
238  // after having generated the log above
240  }
241  }
242 
243  if(cmdline.isset("show-threaded"))
244  {
246 
247  is_threadedt is_threaded(goto_model);
248 
249  for(const auto &gf_entry : goto_model.goto_functions.function_map)
250  {
251  std::cout << "////\n";
252  std::cout << "//// Function: " << gf_entry.first << '\n';
253  std::cout << "////\n\n";
254 
255  const goto_programt &goto_program = gf_entry.second.body;
256 
257  forall_goto_program_instructions(i_it, goto_program)
258  {
259  goto_program.output_instruction(ns, gf_entry.first, std::cout, *i_it);
260  std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
261  << "\n\n";
262  }
263  }
264 
265  return CPROVER_EXIT_SUCCESS;
266  }
267 
268  if(cmdline.isset("insert-final-assert-false"))
269  {
270  log.status() << "Inserting final assert false" << messaget::eom;
271  bool fail = insert_final_assert_false(
272  goto_model,
273  cmdline.get_value("insert-final-assert-false"),
275  if(fail)
276  {
278  }
279  // otherwise, fall-through to write new binary
280  }
281 
282  if(cmdline.isset("show-value-sets"))
283  {
285 
286  // recalculate numbers, etc.
288 
289  log.status() << "Pointer Analysis" << messaget::eom;
291  value_set_analysist value_set_analysis(ns);
292  value_set_analysis(goto_model.goto_functions);
294  ui_message_handler.get_ui(), goto_model, value_set_analysis);
295  return CPROVER_EXIT_SUCCESS;
296  }
297 
298  if(cmdline.isset("show-global-may-alias"))
299  {
303 
304  // recalculate numbers, etc.
306 
307  global_may_alias_analysist global_may_alias_analysis;
308  global_may_alias_analysis(goto_model);
309  global_may_alias_analysis.output(goto_model, std::cout);
310 
311  return CPROVER_EXIT_SUCCESS;
312  }
313 
314  if(cmdline.isset("show-local-bitvector-analysis"))
315  {
318 
319  // recalculate numbers, etc.
321 
323 
324  for(const auto &gf_entry : goto_model.goto_functions.function_map)
325  {
326  local_bitvector_analysist local_bitvector_analysis(gf_entry.second, ns);
327  std::cout << ">>>>\n";
328  std::cout << ">>>> " << gf_entry.first << '\n';
329  std::cout << ">>>>\n";
330  local_bitvector_analysis.output(std::cout, gf_entry.second, ns);
331  std::cout << '\n';
332  }
333 
334  return CPROVER_EXIT_SUCCESS;
335  }
336 
337  if(cmdline.isset("show-local-safe-pointers") ||
338  cmdline.isset("show-safe-dereferences"))
339  {
340  // Ensure location numbering is unique:
342 
344 
345  for(const auto &gf_entry : goto_model.goto_functions.function_map)
346  {
347  local_safe_pointerst local_safe_pointers;
348  local_safe_pointers(gf_entry.second.body);
349  std::cout << ">>>>\n";
350  std::cout << ">>>> " << gf_entry.first << '\n';
351  std::cout << ">>>>\n";
352  if(cmdline.isset("show-local-safe-pointers"))
353  local_safe_pointers.output(std::cout, gf_entry.second.body, ns);
354  else
355  {
356  local_safe_pointers.output_safe_dereferences(
357  std::cout, gf_entry.second.body, ns);
358  }
359  std::cout << '\n';
360  }
361 
362  return CPROVER_EXIT_SUCCESS;
363  }
364 
365  if(cmdline.isset("show-sese-regions"))
366  {
367  // Ensure location numbering is unique:
369 
371 
372  for(const auto &gf_entry : goto_model.goto_functions.function_map)
373  {
374  sese_region_analysist sese_region_analysis;
375  sese_region_analysis(gf_entry.second.body);
376  std::cout << ">>>>\n";
377  std::cout << ">>>> " << gf_entry.first << '\n';
378  std::cout << ">>>>\n";
379  sese_region_analysis.output(std::cout, gf_entry.second.body, ns);
380  std::cout << '\n';
381  }
382 
383  return CPROVER_EXIT_SUCCESS;
384  }
385 
386  if(cmdline.isset("show-custom-bitvector-analysis"))
387  {
391 
393 
394  if(!cmdline.isset("inline"))
395  {
398  }
399 
400  // recalculate numbers, etc.
402 
403  custom_bitvector_analysist custom_bitvector_analysis;
404  custom_bitvector_analysis(goto_model);
405  custom_bitvector_analysis.output(goto_model, std::cout);
406 
407  return CPROVER_EXIT_SUCCESS;
408  }
409 
410  if(cmdline.isset("show-escape-analysis"))
411  {
415 
416  // recalculate numbers, etc.
418 
419  escape_analysist escape_analysis;
420  escape_analysis(goto_model);
421  escape_analysis.output(goto_model, std::cout);
422 
423  return CPROVER_EXIT_SUCCESS;
424  }
425 
426  if(cmdline.isset("custom-bitvector-analysis"))
427  {
431 
433 
434  if(!cmdline.isset("inline"))
435  {
438  }
439 
440  // recalculate numbers, etc.
442 
444 
445  custom_bitvector_analysist custom_bitvector_analysis;
446  custom_bitvector_analysis(goto_model);
447  custom_bitvector_analysis.check(
448  goto_model,
449  cmdline.isset("xml-ui"),
450  std::cout);
451 
452  return CPROVER_EXIT_SUCCESS;
453  }
454 
455  if(cmdline.isset("show-points-to"))
456  {
458 
459  // recalculate numbers, etc.
461 
463 
464  log.status() << "Pointer Analysis" << messaget::eom;
465  points_tot points_to;
466  points_to(goto_model);
467  points_to.output(std::cout);
468  return CPROVER_EXIT_SUCCESS;
469  }
470 
471  if(cmdline.isset("show-intervals"))
472  {
474 
475  // recalculate numbers, etc.
477 
478  log.status() << "Interval Analysis" << messaget::eom;
482  interval_analysis.output(goto_model, std::cout);
483  return CPROVER_EXIT_SUCCESS;
484  }
485 
486  if(cmdline.isset("show-call-sequences"))
487  {
490  return CPROVER_EXIT_SUCCESS;
491  }
492 
493  if(cmdline.isset("check-call-sequence"))
494  {
497  return CPROVER_EXIT_SUCCESS;
498  }
499 
500  if(cmdline.isset("list-calls-args"))
501  {
503 
505 
506  return CPROVER_EXIT_SUCCESS;
507  }
508 
509  if(cmdline.isset("show-rw-set"))
510  {
512 
513  if(!cmdline.isset("inline"))
514  {
516 
517  // recalculate numbers, etc.
519  }
520 
521  log.status() << "Pointer Analysis" << messaget::eom;
522  value_set_analysist value_set_analysis(ns);
523  value_set_analysis(goto_model.goto_functions);
524 
525  const symbolt &symbol=ns.lookup(ID_main);
526  symbol_exprt main(symbol.name, symbol.type);
527 
528  std::cout <<
529  rw_set_functiont(value_set_analysis, goto_model, main);
530  return CPROVER_EXIT_SUCCESS;
531  }
532 
533  if(cmdline.isset("show-symbol-table"))
534  {
536  return CPROVER_EXIT_SUCCESS;
537  }
538 
539  if(cmdline.isset("show-reaching-definitions"))
540  {
542 
544  reaching_definitions_analysist rd_analysis(ns);
545  rd_analysis(goto_model);
546  rd_analysis.output(goto_model, std::cout);
547 
548  return CPROVER_EXIT_SUCCESS;
549  }
550 
551  if(cmdline.isset("show-dependence-graph"))
552  {
554 
556  dependence_grapht dependence_graph(ns);
557  dependence_graph(goto_model);
558  dependence_graph.output(goto_model, std::cout);
559  dependence_graph.output_dot(std::cout);
560 
561  return CPROVER_EXIT_SUCCESS;
562  }
563 
564  if(cmdline.isset("count-eloc"))
565  {
567  return CPROVER_EXIT_SUCCESS;
568  }
569 
570  if(cmdline.isset("list-eloc"))
571  {
573  return CPROVER_EXIT_SUCCESS;
574  }
575 
576  if(cmdline.isset("print-path-lengths"))
577  {
579  return CPROVER_EXIT_SUCCESS;
580  }
581 
582  if(cmdline.isset("print-global-state-size"))
583  {
585  return CPROVER_EXIT_SUCCESS;
586  }
587 
588  if(cmdline.isset("list-symbols"))
589  {
591  return CPROVER_EXIT_SUCCESS;
592  }
593 
594  if(cmdline.isset("show-uninitialized"))
595  {
596  show_uninitialized(goto_model, std::cout);
597  return CPROVER_EXIT_SUCCESS;
598  }
599 
600  if(cmdline.isset("interpreter"))
601  {
604 
605  log.status() << "Starting interpreter" << messaget::eom;
607  return CPROVER_EXIT_SUCCESS;
608  }
609 
610  if(cmdline.isset("show-claims") ||
611  cmdline.isset("show-properties"))
612  {
615  return CPROVER_EXIT_SUCCESS;
616  }
617 
618  if(cmdline.isset("document-claims-html") ||
619  cmdline.isset("document-properties-html"))
620  {
622  return CPROVER_EXIT_SUCCESS;
623  }
624 
625  if(cmdline.isset("document-claims-latex") ||
626  cmdline.isset("document-properties-latex"))
627  {
629  return CPROVER_EXIT_SUCCESS;
630  }
631 
632  if(cmdline.isset("show-loops"))
633  {
635  return CPROVER_EXIT_SUCCESS;
636  }
637 
638  if(cmdline.isset("show-natural-loops"))
639  {
640  show_natural_loops(goto_model, std::cout);
641  return CPROVER_EXIT_SUCCESS;
642  }
643 
644  if(cmdline.isset("show-lexical-loops"))
645  {
646  show_lexical_loops(goto_model, std::cout);
647  }
648 
649  if(cmdline.isset("print-internal-representation"))
650  {
651  for(auto const &pair : goto_model.goto_functions.function_map)
652  for(auto const &ins : pair.second.body.instructions)
653  {
654  if(ins.get_code().is_not_nil())
655  log.status() << ins.get_code().pretty() << messaget::eom;
656  if(ins.has_condition())
657  {
658  log.status() << "[guard] " << ins.get_condition().pretty()
659  << messaget::eom;
660  }
661  }
662  return CPROVER_EXIT_SUCCESS;
663  }
664 
665  if(
666  cmdline.isset("show-goto-functions") ||
667  cmdline.isset("list-goto-functions"))
668  {
670  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
671  return CPROVER_EXIT_SUCCESS;
672  }
673 
674  if(cmdline.isset("list-undefined-functions"))
675  {
677  return CPROVER_EXIT_SUCCESS;
678  }
679 
680  // experimental: print structs
681  if(cmdline.isset("show-struct-alignment"))
682  {
684  return CPROVER_EXIT_SUCCESS;
685  }
686 
687  if(cmdline.isset("show-locations"))
688  {
690  return CPROVER_EXIT_SUCCESS;
691  }
692 
693  if(
694  cmdline.isset("dump-c") || cmdline.isset("dump-cpp") ||
695  cmdline.isset("dump-c-type-header"))
696  {
697  const bool is_cpp=cmdline.isset("dump-cpp");
698  const bool is_header = cmdline.isset("dump-c-type-header");
699  const bool h_libc=!cmdline.isset("no-system-headers");
700  const bool h_all=cmdline.isset("use-all-headers");
701  const bool harness=cmdline.isset("harness");
703 
704  // restore RETURN instructions in case remove_returns had been
705  // applied
707 
708  // dump_c (actually goto_program2code) requires valid instruction
709  // location numbers:
711 
712  if(cmdline.args.size()==2)
713  {
714  #ifdef _MSC_VER
715  std::ofstream out(widen(cmdline.args[1]));
716  #else
717  std::ofstream out(cmdline.args[1]);
718  #endif
719  if(!out)
720  {
721  log.error() << "failed to write to '" << cmdline.args[1] << "'";
723  }
724  if(is_header)
725  {
728  h_libc,
729  h_all,
730  harness,
731  ns,
732  cmdline.get_value("dump-c-type-header"),
733  out);
734  }
735  else
736  {
737  (is_cpp ? dump_cpp : dump_c)(
738  goto_model.goto_functions, h_libc, h_all, harness, ns, out);
739  }
740  }
741  else
742  {
743  if(is_header)
744  {
747  h_libc,
748  h_all,
749  harness,
750  ns,
751  cmdline.get_value("dump-c-type-header"),
752  std::cout);
753  }
754  else
755  {
756  (is_cpp ? dump_cpp : dump_c)(
757  goto_model.goto_functions, h_libc, h_all, harness, ns, std::cout);
758  }
759  }
760 
761  return CPROVER_EXIT_SUCCESS;
762  }
763 
764  if(cmdline.isset("call-graph"))
765  {
767  call_grapht call_graph(goto_model);
768 
769  if(cmdline.isset("xml"))
770  call_graph.output_xml(std::cout);
771  else if(cmdline.isset("dot"))
772  call_graph.output_dot(std::cout);
773  else
774  call_graph.output(std::cout);
775 
776  return CPROVER_EXIT_SUCCESS;
777  }
778 
779  if(cmdline.isset("reachable-call-graph"))
780  {
782  call_grapht call_graph =
785  if(cmdline.isset("xml"))
786  call_graph.output_xml(std::cout);
787  else if(cmdline.isset("dot"))
788  call_graph.output_dot(std::cout);
789  else
790  call_graph.output(std::cout);
791 
792  return 0;
793  }
794 
795  if(cmdline.isset("show-class-hierarchy"))
796  {
797  class_hierarchyt hierarchy;
798  hierarchy(goto_model.symbol_table);
799  if(cmdline.isset("dot"))
800  hierarchy.output_dot(std::cout);
801  else
803 
804  return CPROVER_EXIT_SUCCESS;
805  }
806 
807  if(cmdline.isset("dot"))
808  {
810 
811  if(cmdline.args.size()==2)
812  {
813  #ifdef _MSC_VER
814  std::ofstream out(widen(cmdline.args[1]));
815  #else
816  std::ofstream out(cmdline.args[1]);
817  #endif
818  if(!out)
819  {
820  log.error() << "failed to write to " << cmdline.args[1] << "'";
822  }
823 
824  dot(goto_model, out);
825  }
826  else
827  dot(goto_model, std::cout);
828 
829  return CPROVER_EXIT_SUCCESS;
830  }
831 
832  if(cmdline.isset("accelerate"))
833  {
835 
837 
838  log.status() << "Performing full inlining" << messaget::eom;
840 
841  log.status() << "Removing calls to functions without a body"
842  << messaget::eom;
843  remove_calls_no_bodyt remove_calls_no_body;
844  remove_calls_no_body(goto_model.goto_functions);
845 
846  log.status() << "Accelerating" << messaget::eom;
847  guard_managert guard_manager;
849  goto_model, ui_message_handler, cmdline.isset("z3"), guard_manager);
851  }
852 
853  if(cmdline.isset("horn-encoding"))
854  {
855  log.status() << "Horn-clause encoding" << messaget::eom;
857 
858  if(cmdline.args.size()==2)
859  {
860  #ifdef _MSC_VER
861  std::ofstream out(widen(cmdline.args[1]));
862  #else
863  std::ofstream out(cmdline.args[1]);
864  #endif
865 
866  if(!out)
867  {
868  log.error() << "Failed to open output file " << cmdline.args[1]
869  << messaget::eom;
871  }
872 
874  }
875  else
876  horn_encoding(goto_model, std::cout);
877 
878  return CPROVER_EXIT_SUCCESS;
879  }
880 
881  if(cmdline.isset("drop-unused-functions"))
882  {
884 
885  log.status() << "Removing unused functions" << messaget::eom;
887  }
888 
889  if(cmdline.isset("undefined-function-is-assume-false"))
890  {
893  }
894 
895  // write new binary?
896  if(cmdline.args.size()==2)
897  {
898  log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'"
899  << messaget::eom;
900 
903  else
904  return CPROVER_EXIT_SUCCESS;
905  }
906  else if(cmdline.args.size() < 2)
907  {
909  "Invalid number of positional arguments passed",
910  "[in] [out]",
911  "goto-instrument needs one input and one output file, aside from other "
912  "flags");
913  }
914 
915  help();
917  }
918 // NOLINTNEXTLINE(readability/fn_size)
919 }
920 
922  bool force)
923 {
924  if(function_pointer_removal_done && !force)
925  return;
926 
928 
929  log.status() << "Function Pointer Removal" << messaget::eom;
931  ui_message_handler, goto_model, cmdline.isset("pointer-check"));
932  log.status() << "Virtual function removal" << messaget::eom;
934  log.status() << "Cleaning inline assembler statements" << messaget::eom;
936 }
937 
942 {
943  // Don't bother if we've already done a full function pointer
944  // removal.
946  {
947  return;
948  }
949 
950  log.status() << "Removing const function pointers only" << messaget::eom;
953  goto_model,
954  cmdline.isset("pointer-check"),
955  true); // abort if we can't resolve via const pointers
956 }
957 
959 {
961  return;
962 
964 
965  if(!cmdline.isset("inline"))
966  {
967  log.status() << "Partial Inlining" << messaget::eom;
969  }
970 }
971 
973 {
975  return;
976 
977  remove_returns_done=true;
978 
979  log.status() << "Removing returns" << messaget::eom;
981 }
982 
984 {
985  log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'"
986  << messaget::eom;
987 
988  config.set(cmdline);
989 
990  auto result = read_goto_binary(cmdline.args[0], ui_message_handler);
991 
992  if(!result.has_value())
993  throw 0;
994 
995  goto_model = std::move(result.value());
996 
998 }
999 
1001 {
1002  optionst options;
1003 
1005 
1006  // disable simplify when adding various checks?
1007  if(cmdline.isset("no-simplify"))
1008  options.set_option("simplify", false);
1009  else
1010  options.set_option("simplify", true);
1011 
1012  // all checks supported by goto_check
1014 
1015  // unwind loops
1016  if(cmdline.isset("unwind"))
1017  {
1018  log.status() << "Unwinding loops" << messaget::eom;
1019  options.set_option("unwind", cmdline.get_value("unwind"));
1020  }
1021 
1022  {
1024 
1025  if(
1029  {
1031 
1033  }
1034  }
1035 
1036  // skip over selected loops
1037  if(cmdline.isset("skip-loops"))
1038  {
1039  log.status() << "Adding gotos to skip loops" << messaget::eom;
1040  if(skip_loops(
1042  throw 0;
1043  }
1044 
1046 
1047  // initialize argv with valid pointers
1048  if(cmdline.isset("model-argc-argv"))
1049  {
1050  unsigned max_argc=
1051  safe_string2unsigned(cmdline.get_value("model-argc-argv"));
1052  std::list<std::string> argv;
1053  argv.resize(max_argc);
1054 
1055  log.status() << "Adding up to " << max_argc << " command line arguments"
1056  << messaget::eom;
1057 
1058  if(model_argc_argv(
1059  goto_model, argv, true /*model_argv*/, ui_message_handler))
1060  throw 0;
1061  }
1062 
1063  if(cmdline.isset("add-cmd-line-arg"))
1064  {
1065  const std::list<std::string> &argv = cmdline.get_values("add-cmd-line-arg");
1066  unsigned argc = 0;
1067 
1068  std::stringstream ss;
1069  ss << "[";
1070  std::string sep = "";
1071  for(auto const &arg : argv)
1072  {
1073  ss << sep << "\"" << arg << "\"";
1074  argc++;
1075  sep = ", ";
1076  }
1077  ss << "]";
1078 
1079  log.status() << "Adding " << argc << " arguments: " << ss.str()
1080  << messaget::eom;
1081 
1082  if(model_argc_argv(
1083  goto_model, argv, false /*model_argv*/, ui_message_handler))
1084  throw 0;
1085  }
1086 
1087  if(cmdline.isset("remove-function-body"))
1088  {
1090  goto_model,
1091  cmdline.get_values("remove-function-body"),
1093  }
1094 
1095  // we add the library in some cases, as some analyses benefit
1096 
1097  if(cmdline.isset("add-library") ||
1098  cmdline.isset("mm"))
1099  {
1100  if(cmdline.isset("show-custom-bitvector-analysis") ||
1101  cmdline.isset("custom-bitvector-analysis"))
1102  {
1103  config.ansi_c.defines.push_back(
1104  std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS");
1105  }
1106 
1107  // add the library
1108  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
1109  << messaget::eom;
1113  }
1114 
1115  // now do full inlining, if requested
1116  if(cmdline.isset("inline"))
1117  {
1119 
1120  if(cmdline.isset("show-custom-bitvector-analysis") ||
1121  cmdline.isset("custom-bitvector-analysis"))
1122  {
1126  }
1127 
1128  log.status() << "Performing full inlining" << messaget::eom;
1130  }
1131 
1132  if(cmdline.isset("show-custom-bitvector-analysis") ||
1133  cmdline.isset("custom-bitvector-analysis"))
1134  {
1135  log.status() << "Propagating Constants" << messaget::eom;
1136  constant_propagator_ait constant_propagator_ai(goto_model);
1138  }
1139 
1140  if(cmdline.isset("escape-analysis"))
1141  {
1145 
1146  // recalculate numbers, etc.
1148 
1149  log.status() << "Escape Analysis" << messaget::eom;
1150  escape_analysist escape_analysis;
1151  escape_analysis(goto_model);
1152  escape_analysis.instrument(goto_model);
1153 
1154  // inline added functions, they are often small
1156 
1157  // recalculate numbers, etc.
1159  }
1160 
1161  if(
1164  {
1166  code_contractst contracts(goto_model, log);
1167 
1168  std::set<std::string> to_replace(
1171 
1172  std::set<std::string> to_enforce(
1175 
1176  // It’s important to keep the order of contracts instrumentation, i.e.,
1177  // first replacement then enforcement. We rely on contract replacement
1178  // and inlining of sub-function calls to properly annotate all
1179  // assignments.
1180  contracts.replace_calls(to_replace);
1181  contracts.enforce_contracts(to_enforce);
1182 
1184  contracts.apply_loop_contracts();
1185  }
1186 
1187  if(cmdline.isset("value-set-fi-fp-removal"))
1188  {
1191  }
1192 
1193  // replace function pointers, if explicitly requested
1194  if(cmdline.isset("remove-function-pointers"))
1195  {
1197  }
1198  else if(cmdline.isset("remove-const-function-pointers"))
1199  {
1201  }
1202 
1203  if(cmdline.isset("replace-calls"))
1204  {
1206 
1207  replace_callst replace_calls;
1208  replace_calls(goto_model, cmdline.get_values("replace-calls"));
1209  }
1210 
1211  if(cmdline.isset("function-inline"))
1212  {
1213  std::string function=cmdline.get_value("function-inline");
1214  PRECONDITION(!function.empty());
1215 
1216  bool caching=!cmdline.isset("no-caching");
1217 
1219 
1220  log.status() << "Inlining calls of function '" << function << "'"
1221  << messaget::eom;
1222 
1223  if(!cmdline.isset("log"))
1224  {
1226  goto_model, function, ui_message_handler, true, caching);
1227  }
1228  else
1229  {
1230  std::string filename=cmdline.get_value("log");
1231  bool have_file=!filename.empty() && filename!="-";
1232 
1234  goto_model, function, ui_message_handler, true, caching);
1235 
1236  if(have_file)
1237  {
1238 #ifdef _MSC_VER
1239  std::ofstream of(widen(filename));
1240 #else
1241  std::ofstream of(filename);
1242 #endif
1243  if(!of)
1244  throw "failed to open file "+filename;
1245 
1246  of << result;
1247  of.close();
1248  }
1249  else
1250  {
1251  std::cout << result << '\n';
1252  }
1253  }
1254 
1257  }
1258 
1259  if(cmdline.isset("partial-inline"))
1260  {
1262 
1263  log.status() << "Partial inlining" << messaget::eom;
1265 
1268  }
1269 
1270  if(cmdline.isset("remove-calls-no-body"))
1271  {
1272  log.status() << "Removing calls to functions without a body"
1273  << messaget::eom;
1274 
1275  remove_calls_no_bodyt remove_calls_no_body;
1276  remove_calls_no_body(goto_model.goto_functions);
1277 
1280  }
1281 
1282  if(cmdline.isset("constant-propagator"))
1283  {
1285 
1286  log.status() << "Propagating Constants" << messaget::eom;
1287 
1288  constant_propagator_ait constant_propagator_ai(goto_model);
1290  }
1291 
1292  if(cmdline.isset("generate-function-body"))
1293  {
1294  optionst c_object_factory_options;
1295  parse_c_object_factory_options(cmdline, c_object_factory_options);
1296  c_object_factory_parameterst object_factory_parameters(
1297  c_object_factory_options);
1298 
1299  auto generate_implementation = generate_function_bodies_factory(
1300  cmdline.get_value("generate-function-body-options"),
1301  object_factory_parameters,
1305  std::regex(cmdline.get_value("generate-function-body")),
1306  *generate_implementation,
1307  goto_model,
1309  }
1310 
1311  if(cmdline.isset("generate-havocing-body"))
1312  {
1313  optionst c_object_factory_options;
1314  parse_c_object_factory_options(cmdline, c_object_factory_options);
1315  c_object_factory_parameterst object_factory_parameters(
1316  c_object_factory_options);
1317 
1318  auto options_split =
1319  split_string(cmdline.get_value("generate-havocing-body"), ',');
1320  if(options_split.size() < 2)
1322  "not enough arguments for this option", "--generate-havocing-body"};
1323 
1324  if(options_split.size() == 2)
1325  {
1326  auto generate_implementation = generate_function_bodies_factory(
1327  std::string{"havoc,"} + options_split.back(),
1328  object_factory_parameters,
1332  std::regex(options_split[0]),
1333  *generate_implementation,
1334  goto_model,
1336  }
1337  else
1338  {
1339  CHECK_RETURN(options_split.size() % 2 == 1);
1340  for(size_t i = 1; i + 1 < options_split.size(); i += 2)
1341  {
1342  auto generate_implementation = generate_function_bodies_factory(
1343  std::string{"havoc,"} + options_split[i + 1],
1344  object_factory_parameters,
1348  options_split[0],
1349  options_split[i],
1350  *generate_implementation,
1351  goto_model,
1353  }
1354  }
1355  }
1356 
1357  // add generic checks, if needed
1359 
1360  // check for uninitalized local variables
1361  if(cmdline.isset("uninitialized-check"))
1362  {
1363  log.status() << "Adding checks for uninitialized local variables"
1364  << messaget::eom;
1366  }
1367 
1368  // check for maximum call stack size
1369  if(cmdline.isset("stack-depth"))
1370  {
1371  log.status() << "Adding check for maximum call stack size" << messaget::eom;
1372  stack_depth(
1373  goto_model,
1374  safe_string2size_t(cmdline.get_value("stack-depth")),
1376  }
1377 
1378  // ignore default/user-specified initialization of variables with static
1379  // lifetime
1380  if(cmdline.isset("nondet-static-exclude"))
1381  {
1382  log.status() << "Adding nondeterministic initialization "
1383  "of static/global variables except for "
1384  "the specified ones."
1385  << messaget::eom;
1386 
1387  nondet_static(goto_model, cmdline.get_values("nondet-static-exclude"));
1388  }
1389  else if(cmdline.isset("nondet-static"))
1390  {
1391  log.status() << "Adding nondeterministic initialization "
1392  "of static/global variables"
1393  << messaget::eom;
1395  }
1396 
1397  if(cmdline.isset("slice-global-inits"))
1398  {
1399  log.status() << "Slicing away initializations of unused global variables"
1400  << messaget::eom;
1402  }
1403 
1404  if(cmdline.isset("string-abstraction"))
1405  {
1408 
1409  log.status() << "String Abstraction" << messaget::eom;
1411  }
1412 
1413  // some analyses require function pointer removal and partial inlining
1414 
1415  if(cmdline.isset("remove-pointers") ||
1416  cmdline.isset("race-check") ||
1417  cmdline.isset("mm") ||
1418  cmdline.isset("isr") ||
1419  cmdline.isset("concurrency"))
1420  {
1422 
1423  log.status() << "Pointer Analysis" << messaget::eom;
1424  value_set_analysist value_set_analysis(ns);
1425  value_set_analysis(goto_model.goto_functions);
1426 
1427  if(cmdline.isset("remove-pointers"))
1428  {
1429  // removing pointers
1430  log.status() << "Removing Pointers" << messaget::eom;
1431  remove_pointers(goto_model, value_set_analysis);
1432  }
1433 
1434  if(cmdline.isset("race-check"))
1435  {
1436  log.status() << "Adding Race Checks" << messaget::eom;
1437  race_check(value_set_analysis, goto_model);
1438  }
1439 
1440  if(cmdline.isset("mm"))
1441  {
1442  std::string mm=cmdline.get_value("mm");
1443  memory_modelt model;
1444 
1445  // strategy of instrumentation
1446  instrumentation_strategyt inst_strategy;
1447  if(cmdline.isset("one-event-per-cycle"))
1448  inst_strategy=one_event_per_cycle;
1449  else if(cmdline.isset("minimum-interference"))
1450  inst_strategy=min_interference;
1451  else if(cmdline.isset("read-first"))
1452  inst_strategy=read_first;
1453  else if(cmdline.isset("write-first"))
1454  inst_strategy=write_first;
1455  else if(cmdline.isset("my-events"))
1456  inst_strategy=my_events;
1457  else
1458  /* default: instruments all unsafe pairs */
1459  inst_strategy=all;
1460 
1461  const unsigned max_var=
1462  cmdline.isset("max-var")?
1464  const unsigned max_po_trans=
1465  cmdline.isset("max-po-trans")?
1466  unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1467 
1468  if(mm=="tso")
1469  {
1470  log.status() << "Adding weak memory (TSO) Instrumentation"
1471  << messaget::eom;
1472  model=TSO;
1473  }
1474  else if(mm=="pso")
1475  {
1476  log.status() << "Adding weak memory (PSO) Instrumentation"
1477  << messaget::eom;
1478  model=PSO;
1479  }
1480  else if(mm=="rmo")
1481  {
1482  log.status() << "Adding weak memory (RMO) Instrumentation"
1483  << messaget::eom;
1484  model=RMO;
1485  }
1486  else if(mm=="power")
1487  {
1488  log.status() << "Adding weak memory (Power) Instrumentation"
1489  << messaget::eom;
1490  model=Power;
1491  }
1492  else
1493  {
1494  log.error() << "Unknown weak memory model '" << mm << "'"
1495  << messaget::eom;
1496  model=Unknown;
1497  }
1498 
1500 
1501  if(cmdline.isset("force-loop-duplication"))
1502  loops=all_loops;
1503  if(cmdline.isset("no-loop-duplication"))
1504  loops=no_loop;
1505 
1506  if(model!=Unknown)
1507  weak_memory(
1508  model,
1509  value_set_analysis,
1510  goto_model,
1511  cmdline.isset("scc"),
1512  inst_strategy,
1513  !cmdline.isset("cfg-kill"),
1514  cmdline.isset("no-dependencies"),
1515  loops,
1516  max_var,
1517  max_po_trans,
1518  !cmdline.isset("no-po-rendering"),
1519  cmdline.isset("render-cluster-file"),
1520  cmdline.isset("render-cluster-function"),
1521  cmdline.isset("cav11"),
1522  cmdline.isset("hide-internals"),
1524  cmdline.isset("ignore-arrays"));
1525  }
1526 
1527  // Interrupt handler
1528  if(cmdline.isset("isr"))
1529  {
1530  log.status() << "Instrumenting interrupt handler" << messaget::eom;
1531  interrupt(
1532  value_set_analysis,
1533  goto_model,
1534  cmdline.get_value("isr"));
1535  }
1536 
1537  // Memory-mapped I/O
1538  if(cmdline.isset("mmio"))
1539  {
1540  log.status() << "Instrumenting memory-mapped I/O" << messaget::eom;
1541  mmio(value_set_analysis, goto_model);
1542  }
1543 
1544  if(cmdline.isset("concurrency"))
1545  {
1546  log.status() << "Sequentializing concurrency" << messaget::eom;
1547  concurrency(value_set_analysis, goto_model);
1548  }
1549  }
1550 
1551  if(cmdline.isset("interval-analysis"))
1552  {
1553  log.status() << "Interval analysis" << messaget::eom;
1555  }
1556 
1557  if(cmdline.isset("havoc-loops"))
1558  {
1559  log.status() << "Havocking loops" << messaget::eom;
1561  }
1562 
1563  if(cmdline.isset("k-induction"))
1564  {
1565  bool base_case=cmdline.isset("base-case");
1566  bool step_case=cmdline.isset("step-case");
1567 
1568  if(step_case && base_case)
1569  throw "please specify only one of --step-case and --base-case";
1570  else if(!step_case && !base_case)
1571  throw "please specify one of --step-case and --base-case";
1572 
1573  unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1574 
1575  if(k==0)
1576  throw "please give k>=1";
1577 
1578  log.status() << "Instrumenting k-induction for k=" << k << ", "
1579  << (base_case ? "base case" : "step case") << messaget::eom;
1580 
1581  k_induction(goto_model, base_case, step_case, k);
1582  }
1583 
1584  if(cmdline.isset("function-enter"))
1585  {
1586  log.status() << "Function enter instrumentation" << messaget::eom;
1588  goto_model,
1589  cmdline.get_value("function-enter"));
1590  }
1591 
1592  if(cmdline.isset("function-exit"))
1593  {
1594  log.status() << "Function exit instrumentation" << messaget::eom;
1595  function_exit(
1596  goto_model,
1597  cmdline.get_value("function-exit"));
1598  }
1599 
1600  if(cmdline.isset("branch"))
1601  {
1602  log.status() << "Branch instrumentation" << messaget::eom;
1603  branch(
1604  goto_model,
1605  cmdline.get_value("branch"));
1606  }
1607 
1608  // add failed symbols
1610 
1611  // recalculate numbers, etc.
1613 
1614  // add loop ids
1616 
1617  // label the assertions
1619 
1620  nondet_volatile(goto_model, options);
1621 
1622  // reachability slice?
1623  if(cmdline.isset("reachability-slice"))
1624  {
1626 
1627  log.status() << "Performing a reachability slice" << messaget::eom;
1628 
1629  // reachability_slicer requires that the model has unique location numbers:
1631 
1632  if(cmdline.isset("property"))
1634  else
1636  }
1637 
1638  if(cmdline.isset("fp-reachability-slice"))
1639  {
1641 
1642  log.status() << "Performing a function pointer reachability slice"
1643  << messaget::eom;
1645  goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
1646  }
1647 
1648  // full slice?
1649  if(cmdline.isset("full-slice"))
1650  {
1653 
1654  log.status() << "Performing a full slice" << messaget::eom;
1655  if(cmdline.isset("property"))
1657  else
1658  {
1659  // full_slicer requires that the model has unique location numbers:
1662  }
1663  }
1664 
1665  // splice option
1666  if(cmdline.isset("splice-call"))
1667  {
1668  log.status() << "Performing call splicing" << messaget::eom;
1669  std::string callercallee=cmdline.get_value("splice-call");
1670  if(splice_call(
1672  callercallee,
1675  throw 0;
1676  }
1677 
1678  // aggressive slicer
1679  if(cmdline.isset("aggressive-slice"))
1680  {
1682 
1683  // reachability_slicer requires that the model has unique location numbers:
1685 
1686  log.status() << "Slicing away initializations of unused global variables"
1687  << messaget::eom;
1689 
1690  log.status() << "Performing an aggressive slice" << messaget::eom;
1691  aggressive_slicert aggressive_slicer(goto_model, ui_message_handler);
1692 
1693  if(cmdline.isset("aggressive-slice-call-depth"))
1694  aggressive_slicer.call_depth =
1695  safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
1696 
1697  if(cmdline.isset("aggressive-slice-preserve-function"))
1698  aggressive_slicer.preserve_functions(
1699  cmdline.get_values("aggressive-slice-preserve-function"));
1700 
1701  if(cmdline.isset("property"))
1702  aggressive_slicer.user_specified_properties =
1703  cmdline.get_values("property");
1704 
1705  if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
1706  aggressive_slicer.name_snippets =
1707  cmdline.get_values("aggressive-slice-preserve-functions-containing");
1708 
1709  aggressive_slicer.preserve_all_direct_paths =
1710  cmdline.isset("aggressive-slice-preserve-all-direct-paths");
1711 
1712  aggressive_slicer.doit();
1713 
1715 
1716  log.status() << "Performing a reachability slice" << messaget::eom;
1717  if(cmdline.isset("property"))
1719  else
1721  }
1722 
1723  if(cmdline.isset("ensure-one-backedge-per-target"))
1724  {
1725  log.status() << "Trying to force one backedge per target" << messaget::eom;
1727  }
1728 
1729  // recalculate numbers, etc.
1731 }
1732 
1735 {
1736  // clang-format off
1737  std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1738  << align_center_with_border("Copyright (C) 2008-2013") << '\n'
1739  << align_center_with_border("Daniel Kroening") << '\n'
1740  << align_center_with_border("kroening@kroening.com") << '\n'
1741  <<
1742  "\n"
1743  "Usage: Purpose:\n"
1744  "\n"
1745  " goto-instrument [-?] [-h] [--help] show help\n"
1746  " goto-instrument in out perform instrumentation\n"
1747  "\n"
1748  "Main options:\n"
1750  " --dot generate CFG graph in DOT format\n"
1751  " --interpreter do concrete execution\n"
1752  "\n"
1753  "Dump Source:\n"
1754  HELP_DUMP_C
1755  "\n"
1756  "Diagnosis:\n"
1758  " --show-symbol-table show loaded symbol table\n"
1759  " --list-symbols list symbols with type information\n"
1762  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1763  " --print-internal-representation\n" // NOLINTNEXTLINE(*)
1764  " show verbose internal representation of the program\n"
1765  " --list-undefined-functions list functions without body\n"
1766  " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
1767  " --show-natural-loops show natural loop heads\n"
1768  // NOLINTNEXTLINE(whitespace/line_length)
1769  " --list-calls-args list all function calls with their arguments\n"
1770  " --call-graph show graph of function calls\n"
1771  // NOLINTNEXTLINE(whitespace/line_length)
1772  " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1774  // NOLINTNEXTLINE(whitespace/line_length)
1775  " --show-threaded show instructions that may be executed by more than one thread\n"
1776  " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1777  " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1778  " *and* used as a dereference operand\n" // NOLINT(*)
1780  // NOLINTNEXTLINE(whitespace/line_length)
1781  " --validate-goto-binary check the well-formedness of the passed in goto\n"
1782  " binary and then exit\n"
1783  "\n"
1784  "Safety checks:\n"
1785  " --no-assertions ignore user assertions\n"
1788  " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
1789  " --race-check add floating-point data race checks\n"
1790  "\n"
1791  "Semantic transformations:\n"
1792  << HELP_NONDET_VOLATILE <<
1794  " --unwindset-file <file> read unwindset from file\n"
1795  " --partial-loops permit paths with partial loops\n"
1796  " --unwinding-assertions generate unwinding assertions\n"
1797  " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*)
1798  " --isr <function> instruments an interrupt service routine\n"
1799  " --mmio instruments memory-mapped I/O\n"
1800  " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
1801  " --nondet-static-exclude e same as nondet-static except for the variable e\n" //NOLINT(*)
1802  " (use multiple times if required)\n"
1803  " --check-invariant function instruments invariant checking function\n"
1805  " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*)
1806  " --undefined-function-is-assume-false\n"
1807  // NOLINTNEXTLINE(whitespace/line_length)
1808  " convert each call to an undefined function to assume(false)\n"
1812  "\n"
1813  "Loop transformations:\n"
1814  " --k-induction <k> check loops with k-induction\n"
1815  " --step-case k-induction: do step-case\n"
1816  " --base-case k-induction: do base-case\n"
1817  " --havoc-loops over-approximate all loops\n"
1818  " --accelerate add loop accelerators\n"
1819  " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" // NOLINT(*)
1820  "\n"
1821  "Memory model instrumentations:\n"
1823  "\n"
1824  "Slicing:\n"
1826  " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
1827  " --property id slice with respect to specific property only\n" // NOLINT(*)
1828  " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1829  " --aggressive-slice remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
1830  " the start function and the function containing the property(s)\n" // NOLINT(*)
1831  " --aggressive-slice-call-depth <n>\n"
1832  " used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
1833  " of the functions on the shortest path\n"
1834  " --aggressive-slice-preserve-function <f>\n"
1835  " force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
1836  " --aggressive-slice-preserve-function containing <f>\n"
1837  " force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
1838  "--aggressive-slice-preserve-all-direct-paths \n"
1839  " force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
1840  "\n"
1841  "Further transformations:\n"
1842  " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)
1843  " --inline perform full inlining\n"
1844  " --partial-inline perform partial inlining\n"
1845  " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
1846  " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
1847  " --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
1848  " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1849  " --value-set-fi-fp-removal build flow-insensitive value set and replace function pointers by a case statement\n" // NOLINT(*)
1850  " over the possible assignments. If the set of possible assignments is empty the function pointer\n" // NOLINT(*)
1851  " is removed using the standard remove-function-pointers pass. \n" // NOLINT(*)
1855  " --add-library add models of C library functions\n"
1858  // NOLINTNEXTLINE(whitespace/line_length)
1859  " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1861  "\n"
1862  "Code contracts:\n"
1866  "\n"
1867  "Other options:\n"
1868  " --version show version and exit\n"
1869  HELP_FLUSH
1870  " --xml output files in XML where supported\n"
1871  " --xml-ui use XML-formatted output\n"
1872  " --json-ui use JSON-formatted output\n"
1874  "\n";
1875  // clang-format on
1876 }
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
Definition: accelerate.cpp:638
Loop Acceleration.
void add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i....
Pointer Dereferencing.
void print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
Alignment Checks.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define HELP_ANSI_C_LANGUAGE
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition: branch.cpp:22
Branch Instrumentation.
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
Function Call Graphs.
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
void check_call_sequence(const goto_modelt &goto_model)
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
Memory-mapped I/O Instrumentation for Goto Programs.
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
Class Hierarchy.
#define HELP_SHOW_CLASS_HIERARCHY
The aggressive slicer removes the body of all the functions except those on the shortest path,...
std::list< std::string > user_specified_properties
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
std::list< std::string > name_snippets
void preserve_functions(const std::list< std::string > &function_list)
Adds a list of functions to the set of functions for the aggressive slicer to preserve.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition: ai.cpp:40
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:564
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Definition: call_graph.h:44
void output_dot(std::ostream &out) const
Definition: call_graph.cpp:255
void output(std::ostream &out) const
Definition: call_graph.cpp:272
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:53
void output_xml(std::ostream &out) const
Definition: call_graph.cpp:282
Non-graph-based representation of the class hierarchy.
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
std::list< std::string > get_comma_separated_values(const char *option) const
Collect all occurrences of option option and split their values on each comma, merging them into a si...
Definition: cmdline.cpp:121
argst args
Definition: cmdline.h:145
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:109
bool replace_calls(const std::set< std::string > &)
Replace all calls to each function in the list with that function's contract.
Definition: contracts.cpp:1567
void apply_loop_contracts()
Definition: contracts.cpp:1610
bool enforce_contracts(const std::set< std::string > &functions)
Turn requires & ensures into assumptions and assertions for each of the named functions.
Definition: contracts.cpp:1616
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1254
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
struct configt::ansi_ct ansi_c
void check(const goto_modelt &, bool xml, std::ostream &)
void instrument(goto_modelt &)
This is a may analysis (i.e.
void compute_loop_numbers()
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void help() override
display command line help
void do_indirect_call_and_rtti_removal(bool force=false)
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
int doit() override
invoke main modules
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
Definition: goto_model.h:98
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
unwind_strategyt
Definition: unwind.h:24
jsont output_log_json() const
Definition: unwind.h:70
void output_dot(std::ostream &out) const
Definition: graph.h:990
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: json.h:27
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
void output_safe_dereferences(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output safely dereferenced expressions per instruction in human-readable format.
void output(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output non-null expressions per instruction in human-readable format.
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition: message.cpp:105
mstreamt & error() const
Definition: message.h:399
mstreamt & status() const
Definition: message.h:414
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
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
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Definition: options.cpp:62
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
virtual int main()
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
void output(std::ostream &out) const
Definition: points_to.cpp:33
void output(std::ostream &out, const goto_programt &goto_program, const namespacet &ns) const
Expression to hold a symbol (variable)
Definition: std_expr.h:80
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
virtual uit get_ui() const
Definition: ui_message.h:33
This template class implements a data-flow analysis which keeps track of what values different variab...
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Encoding for Threaded Goto Programs.
configt config
Definition: config.cpp:25
#define HELP_CONFIG_LIBRARY
Definition: config.h:62
Constant propagation.
#define HELP_REPLACE_CALL
Definition: contracts.h:40
#define FLAG_REPLACE_CALL
Definition: contracts.h:39
#define FLAG_ENFORCE_CONTRACT
Definition: contracts.h:44
#define HELP_LOOP_CONTRACTS
Definition: contracts.h:35
#define FLAG_LOOP_CONTRACTS
Definition: contracts.h:34
#define HELP_ENFORCE_CONTRACT
Definition: contracts.h:45
void count_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:54
void print_global_state_size(const goto_modelt &goto_model)
Definition: count_eloc.cpp:158
void print_path_lengths(const goto_modelt &goto_model)
Definition: count_eloc.cpp:85
void list_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:68
#define HELP_GOTO_PROGRAM_STATS
Definition: count_eloc.h:30
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define CPROVER_PREFIX
Field-insensitive, location-sensitive bitvector analysis.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
#define HELP_DOCUMENT_PROPERTIES
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:353
Dump Goto-Program as DOT Graph.
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1597
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1584
void dump_c_type_header(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, const std::string module, std::ostream &out)
Definition: dump_c.cpp:1619
#define HELP_DUMP_C
Definition: dump_c.h:52
bool ensure_one_backedge_per_target(goto_programt::targett &it, goto_programt &goto_program)
Ensure one backedge per target.
Field-insensitive, location-sensitive, over-approximative escape analysis.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
Definition: exit_codes.h:62
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:101
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:76
Function Entering and Exiting.
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...
#define HELP_REPLACE_FUNCTION_BODY
Field-insensitive, location-sensitive, over-approximative escape analysis.
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
Definition: goto_check.cpp:18
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check_c.h:74
#define HELP_GOTO_CHECK
Definition: goto_check_c.h:53
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Inline every function call into the entry_point() function.
Definition: goto_inline.cpp:26
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls made from a particular function.
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
Command Line Parsing.
#define forall_goto_program_instructions(it, program)
void remove_pointers(goto_modelt &goto_model, value_setst &value_sets)
Remove dereferences in all expressions contained in the program goto_model.
#define HELP_REMOVE_POINTERS
void havoc_loops(goto_modelt &goto_model)
Havoc Loops.
void horn_encoding(const goto_modelt &, std::ostream &)
Horn-clause Encoding.
bool insert_final_assert_false(goto_modelt &goto_model, const std::string &function_to_instrument, message_handlert &message_handler)
Transform a goto program by inserting assert(false) at the end of a given function function_to_instru...
Insert final assert false into a function.
#define HELP_INSERT_FINAL_ASSERT_FALSE
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
Interpreter for GOTO Programs.
static void interrupt(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, const symbol_exprt &interrupt_handler, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:58
Interrupt Instrumentation for Goto Programs.
void interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...
Interval Analysis.
Interval Domain.
Over-approximate Concurrency for Threaded Goto Programs.
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
k-induction
void label_function_pointer_call_sites(goto_modelt &goto_model)
This ensures that call instructions can be only one of two things:
Label function pointer call sites across a goto model.
Compute lexical loops in a goto_function.
void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
Field-insensitive, location-sensitive bitvector analysis.
Local safe pointer analysis.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
Loop IDs.
static void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program)
Definition: mmio.cpp:24
Memory-mapped I/O Instrumentation for Goto Programs.
bool model_argc_argv(goto_modelt &goto_model, const std::list< std::string > &argv_args, bool model_argv, message_handlert &message_handler)
Set up argv to user-specified values (when model_argv is FALSE) or (when model_argv is TRUE) set up a...
#define HELP_ARGC_ARGV
Compute natural loops in a goto_function.
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
Definition: natural_loops.h:92
static void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
void nondet_volatile(goto_modelt &goto_model, const optionst &options)
Havoc reads from volatile expressions, if enabled in the options.
Volatile Variables.
#define HELP_NONDET_VOLATILE
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Add parameter assignments.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
Field-sensitive, location-insensitive points-to analysis.
static void race_check(value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, w_guardst &w_guards)
Definition: race_check.cpp:161
Race Detection for Threaded Goto Programs.
void function_path_reachability_slicer(goto_modelt &goto_model, const std::list< std::string > &functions_list)
Perform reachability slicing on goto_model for selected functions.
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
#define HELP_REACHABILITY_SLICER
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
Read Goto Programs.
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Definition: remove_asm.cpp:512
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
Remove calls to functions without a body.
#define HELP_REMOVE_CALLS_NO_BODY
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
void remove_functions(goto_modelt &goto_model, const std::list< std::string > &names, message_handlert &message_handler)
Remove the body of all functions listed in "names" such that an analysis will treat it as a side-effe...
Remove function definition.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, const irep_idt &function_id, bool add_safety_assertion, bool only_remove_const_fps)
Remove Indirect Function Calls.
void restore_returns(goto_modelt &goto_model)
restores return statements
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Replace function returns by assignments to global variables.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Unused function removal.
void remove_virtual_functions(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
Functions for replacing virtual function call with a static function calls in functions,...
#define HELP_REPLACE_CALLS
Definition: replace_calls.h:58
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
void restrict_function_pointers(message_handlert &message_handler, goto_modelt &goto_model, const optionst &options)
Apply function pointer restrictions to a goto_model.
Given goto functions and a list of function parameters or globals that are function pointers with lis...
#define RESTRICT_FUNCTION_POINTER_OPT
#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
#define HELP_RESTRICT_FUNCTION_POINTER
#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Symbolic Execution.
Race Detection for Threaded Goto Programs.
Single-entry, single-exit region analysis.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
#define HELP_SHOW_GOTO_FUNCTIONS
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Show program locations.
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Show the properties.
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Show the symbol table.
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
Show Value Sets.
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
Definition: skip_loops.cpp:24
Skip over selected loops by adding gotos.
void slice_global_inits(goto_modelt &goto_model, message_handlert &message_handler)
Remove initialization of global variables that are not used in any function reachable from the entry ...
Remove initializations of unused global variables.
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: splice_call.cpp:34
Harnessing for goto functions.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
static void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
Definition: stack_depth.cpp:61
Stack depth checks.
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:16
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:35
std::size_t safe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:23
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
String Abstraction.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
irep_idt arch
Definition: config.h:191
std::list< std::string > defines
Definition: config.h:235
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
void thread_exit_instrumentation(goto_programt &goto_program)
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:108
void list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
void undefined_function_abort_path(goto_modelt &goto_model)
Handling of functions without body.
std::wstring widen(const char *s)
Definition: unicode.cpp:48
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
#define HELP_UNINITIALIZED_CHECK
Definition: uninitialized.h:29
Loop unwinding.
#define HELP_UNWINDSET
Definition: unwindset.h:76
#define HELP_VALIDATE
Value Set Propagation.
void value_set_fi_fp_removal(goto_modelt &goto_model, message_handlert &message_handler)
Builds the flow-insensitive value set for all function pointers and replaces function pointers with a...
flow insensitive value set function pointer removal
const char * CBMC_VERSION
void weak_memory(memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &message_handler, bool ignore_arrays)
#define HELP_WMM_FULL
Definition: weak_memory.h:94
memory_modelt
Definition: wmm.h:18
@ Unknown
Definition: wmm.h:19
@ TSO
Definition: wmm.h:20
@ RMO
Definition: wmm.h:22
@ PSO
Definition: wmm.h:21
@ Power
Definition: wmm.h:23
loop_strategyt
Definition: wmm.h:37
@ all_loops
Definition: wmm.h:39
@ arrays_only
Definition: wmm.h:38
@ no_loop
Definition: wmm.h:40
instrumentation_strategyt
Definition: wmm.h:27
@ my_events
Definition: wmm.h:32
@ one_event_per_cycle
Definition: wmm.h:33
@ min_interference
Definition: wmm.h:29
@ read_first
Definition: wmm.h:30
@ all
Definition: wmm.h:28
@ write_first
Definition: wmm.h:31
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
Write GOTO binaries.