CBMC
Loading...
Searching...
No Matches
goto_instrument_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Main Module
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
15#include <util/exit_codes.h>
16#include <util/help_formatter.h>
17#include <util/json.h>
18#include <util/options.h>
19#include <util/string2int.h>
20#include <util/string_utils.h>
21#include <util/unicode.h>
22#include <util/version.h>
23
31#include <goto-programs/mm_io.h>
49
50#include <analyses/call_graph.h>
56#include <analyses/guard.h>
69#include <ansi-c/gcc_version.h>
72#include <cpp/cprover_library.h>
76
77#include "alignment_checks.h"
78#include "branch.h"
79#include "call_sequences.h"
80#include "concurrency.h"
81#include "dot.h"
82#include "full_slicer.h"
83#include "function.h"
84#include "havoc_loops.h"
85#include "horn_encoding.h"
87#include "interrupt.h"
88#include "k_induction.h"
89#include "mmio.h"
90#include "model_argc_argv.h"
91#include "nondet_static.h"
92#include "nondet_volatile.h"
93#include "points_to.h"
94#include "race_check.h"
95#include "remove_function.h"
96#include "rw_set.h"
97#include "show_locations.h"
98#include "skip_loops.h"
99#include "splice_call.h"
100#include "stack_depth.h"
102#include "undefined_functions.h"
103#include "unwind.h"
105
106#include <fstream> // IWYU pragma: keep
107#include <iostream>
108#include <memory>
109
111
114{
115 if(cmdline.isset("version"))
116 {
117 std::cout << CBMC_VERSION << '\n';
119 }
120
121 if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
122 {
123 help();
125 }
126
129
130 {
132
134
135 // configure gcc, if required -- get_goto_program will have set the config
137 {
138 gcc_versiont gcc_version;
139 gcc_version.get("gcc");
140 configure_gcc(gcc_version);
141 }
142
143 {
144 const bool validate_only = cmdline.isset("validate-goto-binary");
145
146 if(validate_only || cmdline.isset("validate-goto-model"))
147 {
149
150 if(validate_only)
151 {
153 }
154 }
155 }
156
157 // ignore default/user-specified initialization
158 // of matching variables with static lifetime
159 if(cmdline.isset("nondet-static-matching"))
160 {
161 log.status() << "Adding nondeterministic initialization "
162 "of matching static/global variables"
163 << messaget::eom;
165 goto_model, cmdline.get_value("nondet-static-matching"));
166 }
167
169
170 if(cmdline.isset("validate-goto-model"))
171 {
173 }
174
175 {
176 bool unwind_given=cmdline.isset("unwind");
177 bool unwindset_given=cmdline.isset("unwindset");
178 bool unwindset_file_given=cmdline.isset("unwindset-file");
179
181 throw "only one of --unwindset and --unwindset-file supported at a "
182 "time";
183
185 {
186 unwindsett unwindset;
187
188 if(unwind_given)
189 unwindset.parse_unwind(cmdline.get_value("unwind"));
190
192 {
193 unwindset.parse_unwindset_file(
194 cmdline.get_value("unwindset-file"),
197 }
198
200 {
201 unwindset.parse_unwindset(
205 }
206
207 bool continue_as_loops=cmdline.isset("continue-as-loops");
208 bool partial_loops = cmdline.isset("partial-loops");
209 bool unwinding_assertions = cmdline.isset("unwinding-assertions") ||
210 (!continue_as_loops && !partial_loops &&
211 !cmdline.isset("no-unwinding-assertions"));
213 {
214 if(unwinding_assertions)
215 {
216 throw "unwinding assertions cannot be used with "
217 "--continue-as-loops";
218 }
219 else if(partial_loops)
220 throw "partial loops cannot be used with --continue-as-loops";
221 }
222
225
226 if(unwinding_assertions)
227 {
228 if(partial_loops)
230 else
232 }
233 else if(partial_loops)
234 {
236 }
237 else if(continue_as_loops)
238 {
240 }
241
244
245 if(cmdline.isset("log"))
246 {
247 std::string filename = cmdline.value_opt("log").value_or("-");
248 bool have_file = filename != "-";
249
250 jsont result=goto_unwind.output_log_json();
251
252 if(have_file)
253 {
254 std::ofstream of(widen_if_needed(filename));
255
256 if(!of)
257 throw "failed to open file "+filename;
258
259 of << result;
260 of.close();
261 }
262 else
263 {
264 std::cout << result << '\n';
265 }
266 }
267
268 // goto_unwind holds references to instructions, only do remove_skip
269 // after having generated the log above
271 }
272 }
273
274 if(cmdline.isset("show-threaded"))
275 {
277
278 is_threadedt is_threaded(goto_model);
279
281 {
282 std::cout << "////\n";
283 std::cout << "//// Function: " << gf_entry.first << '\n';
284 std::cout << "////\n\n";
285
286 const goto_programt &goto_program = gf_entry.second.body;
287
289 {
290 i_it->output(std::cout);
291 std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
292 << "\n\n";
293 }
294 }
295
297 }
298
299 if(cmdline.isset("insert-final-assert-false"))
300 {
301 log.status() << "Inserting final assert false" << messaget::eom;
304 cmdline.get_value("insert-final-assert-false"),
306 if(fail)
307 {
309 }
310 // otherwise, fall-through to write new binary
311 }
312
313 if(cmdline.isset("show-value-sets"))
314 {
316
317 // recalculate numbers, etc.
319
320 log.status() << "Pointer Analysis" << messaget::eom;
327 }
328
329 if(cmdline.isset("show-global-may-alias"))
330 {
334
335 // recalculate numbers, etc.
337
341
343 }
344
345 if(cmdline.isset("show-local-bitvector-analysis"))
346 {
349
350 // recalculate numbers, etc.
352
354
356 {
357 local_bitvector_analysist local_bitvector_analysis(gf_entry.second, ns);
358 std::cout << ">>>>\n";
359 std::cout << ">>>> " << gf_entry.first << '\n';
360 std::cout << ">>>>\n";
361 local_bitvector_analysis.output(std::cout, gf_entry.second, ns);
362 std::cout << '\n';
363 }
364
366 }
367
368 if(cmdline.isset("show-local-safe-pointers") ||
369 cmdline.isset("show-safe-dereferences"))
370 {
371 // Ensure location numbering is unique:
373
375
377 {
379 local_safe_pointers(gf_entry.second.body);
380 std::cout << ">>>>\n";
381 std::cout << ">>>> " << gf_entry.first << '\n';
382 std::cout << ">>>>\n";
383 if(cmdline.isset("show-local-safe-pointers"))
384 local_safe_pointers.output(std::cout, gf_entry.second.body, ns);
385 else
386 {
387 local_safe_pointers.output_safe_dereferences(
388 std::cout, gf_entry.second.body, ns);
389 }
390 std::cout << '\n';
391 }
392
394 }
395
396 if(cmdline.isset("show-sese-regions"))
397 {
398 // Ensure location numbering is unique:
400
402
404 {
406 sese_region_analysis(gf_entry.second.body);
407 std::cout << ">>>>\n";
408 std::cout << ">>>> " << gf_entry.first << '\n';
409 std::cout << ">>>>\n";
410 sese_region_analysis.output(std::cout, gf_entry.second.body, ns);
411 std::cout << '\n';
412 }
413
415 }
416
417 if(cmdline.isset("show-custom-bitvector-analysis"))
418 {
422
424
425 if(!cmdline.isset("inline"))
426 {
429 }
430
431 // recalculate numbers, etc.
433
437
439 }
440
441 if(cmdline.isset("show-escape-analysis"))
442 {
446
447 // recalculate numbers, etc.
449
453
455 }
456
457 if(cmdline.isset("custom-bitvector-analysis"))
458 {
462
464
465 if(!cmdline.isset("inline"))
466 {
469 }
470
471 // recalculate numbers, etc.
473
475
480 cmdline.isset("xml-ui"),
481 std::cout);
482
484 }
485
486 if(cmdline.isset("show-points-to"))
487 {
489
490 // recalculate numbers, etc.
492
494
495 log.status() << "Pointer Analysis" << messaget::eom;
498 points_to.output(std::cout);
500 }
501
502 if(cmdline.isset("show-intervals"))
503 {
505
506 // recalculate numbers, etc.
508
509 log.status() << "Interval Analysis" << messaget::eom;
515 }
516
517 if(cmdline.isset("show-call-sequences"))
518 {
522 }
523
524 if(cmdline.isset("check-call-sequence"))
525 {
529 }
530
531 if(cmdline.isset("list-calls-args"))
532 {
534
536
538 }
539
540 if(cmdline.isset("show-rw-set"))
541 {
543
544 if(!cmdline.isset("inline"))
545 {
547
548 // recalculate numbers, etc.
550 }
551
552 log.status() << "Pointer Analysis" << messaget::eom;
555
556 const symbolt &symbol=ns.lookup(ID_main);
557 symbol_exprt main(symbol.name, symbol.type);
558
559 std::cout << rw_set_functiont(
562 }
563
564 if(cmdline.isset("show-symbol-table"))
565 {
568 }
569
570 if(cmdline.isset("show-reaching-definitions"))
571 {
574
578 rd_analysis.output(goto_model, std::cout);
579
581 }
582
583 if(cmdline.isset("show-dependence-graph"))
584 {
587
592 dependence_graph.output_dot(std::cout);
593
595 }
596
597 if(cmdline.isset("count-eloc"))
598 {
601 }
602
603 if(cmdline.isset("list-eloc"))
604 {
607 }
608
609 if(cmdline.isset("print-path-lengths"))
610 {
613 }
614
615 if(cmdline.isset("print-global-state-size"))
616 {
619 }
620
621 if(cmdline.isset("list-symbols"))
622 {
625 }
626
627 if(cmdline.isset("show-uninitialized"))
628 {
629 show_uninitialized(goto_model, std::cout);
631 }
632
633 if(cmdline.isset("interpreter"))
634 {
637
638 log.status() << "Starting interpreter" << messaget::eom;
641 }
642
643 if(cmdline.isset("show-claims") ||
644 cmdline.isset("show-properties"))
645 {
649 }
650
651 if(cmdline.isset("document-claims-html") ||
652 cmdline.isset("document-properties-html"))
653 {
656 }
657
658 if(cmdline.isset("document-claims-latex") ||
659 cmdline.isset("document-properties-latex"))
660 {
663 }
664
665 if(cmdline.isset("show-loops"))
666 {
669 }
670
671 if(cmdline.isset("show-natural-loops"))
672 {
673 show_natural_loops(goto_model, std::cout);
675 }
676
677 if(cmdline.isset("show-lexical-loops"))
678 {
679 show_lexical_loops(goto_model, std::cout);
681 }
682
683 if(cmdline.isset("print-internal-representation"))
684 {
685 for(auto const &pair : goto_model.goto_functions.function_map)
686 for(auto const &ins : pair.second.body.instructions)
687 {
688 if(ins.code().is_not_nil())
689 log.status() << ins.code().pretty() << messaget::eom;
690 if(ins.has_condition())
691 {
692 log.status() << "[guard] " << ins.condition().pretty()
693 << messaget::eom;
694 }
695 }
697 }
698
699 if(
700 cmdline.isset("show-goto-functions") ||
701 cmdline.isset("list-goto-functions"))
702 {
704 goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
706 }
707
708 if(cmdline.isset("list-undefined-functions"))
709 {
712 }
713
714 // experimental: print structs
715 if(cmdline.isset("show-struct-alignment"))
716 {
719 }
720
721 if(cmdline.isset("show-locations"))
722 {
725 }
726
727 if(
728 cmdline.isset("dump-c") || cmdline.isset("dump-cpp") ||
729 cmdline.isset("dump-c-type-header"))
730 {
731 const bool is_cpp=cmdline.isset("dump-cpp");
732 const bool is_header = cmdline.isset("dump-c-type-header");
733 const bool h_libc=!cmdline.isset("no-system-headers");
734 const bool h_all=cmdline.isset("use-all-headers");
735 const bool harness=cmdline.isset("harness");
737
738 // restore RETURN instructions in case remove_returns had been
739 // applied
741
742 // dump_c (actually goto_program2code) requires valid instruction
743 // location numbers:
745
746 if(cmdline.args.size()==2)
747 {
748 std::ofstream out(widen_if_needed(cmdline.args[1]));
749
750 if(!out)
751 {
752 log.error() << "failed to write to '" << cmdline.args[1] << "'";
754 }
755 if(is_header)
756 {
759 h_libc,
760 h_all,
761 harness,
762 ns,
763 cmdline.get_value("dump-c-type-header"),
764 out);
765 }
766 else
767 {
768 (is_cpp ? dump_cpp : dump_c)(
769 goto_model.goto_functions, h_libc, h_all, harness, ns, out);
770 }
771 }
772 else
773 {
774 if(is_header)
775 {
778 h_libc,
779 h_all,
780 harness,
781 ns,
782 cmdline.get_value("dump-c-type-header"),
783 std::cout);
784 }
785 else
786 {
787 (is_cpp ? dump_cpp : dump_c)(
788 goto_model.goto_functions, h_libc, h_all, harness, ns, std::cout);
789 }
790 }
791
793 }
794
795 if(cmdline.isset("call-graph"))
796 {
798 call_grapht call_graph(goto_model);
799
800 if(cmdline.isset("xml"))
801 call_graph.output_xml(std::cout);
802 else if(cmdline.isset("dot"))
803 call_graph.output_dot(std::cout);
804 else
805 call_graph.output(std::cout);
806
808 }
809
810 if(cmdline.isset("reachable-call-graph"))
811 {
813 call_grapht call_graph =
816 if(cmdline.isset("xml"))
817 call_graph.output_xml(std::cout);
818 else if(cmdline.isset("dot"))
819 call_graph.output_dot(std::cout);
820 else
821 call_graph.output(std::cout);
822
823 return 0;
824 }
825
826 if(cmdline.isset("show-class-hierarchy"))
827 {
830 if(cmdline.isset("dot"))
831 hierarchy.output_dot(std::cout);
832 else
834
836 }
837
838 if(cmdline.isset("dot"))
839 {
841
842 if(cmdline.args.size()==2)
843 {
844 std::ofstream out(widen_if_needed(cmdline.args[1]));
845
846 if(!out)
847 {
848 log.error() << "failed to write to " << cmdline.args[1] << "'";
850 }
851
852 dot(goto_model, out);
853 }
854 else
855 dot(goto_model, std::cout);
856
858 }
859
860 if(cmdline.isset("accelerate"))
861 {
863
865
866 log.status() << "Performing full inlining" << messaget::eom;
868
869 log.status() << "Removing calls to functions without a body"
870 << messaget::eom;
873
874 log.status() << "Accelerating" << messaget::eom;
875 guard_managert guard_manager;
877 goto_model, ui_message_handler, cmdline.isset("z3"), guard_manager);
879 }
880
881 if(cmdline.isset("horn"))
882 {
883 log.status() << "Horn-clause encoding" << messaget::eom;
885
886 if(cmdline.args.size()==2)
887 {
888 std::ofstream out(widen_if_needed(cmdline.args[1]));
889
890 if(!out)
891 {
892 log.error() << "Failed to open output file " << cmdline.args[1]
893 << messaget::eom;
895 }
896
898 }
899 else
900 horn_encoding(goto_model, std::cout);
901
903 }
904
905 if(cmdline.isset("drop-unused-functions"))
906 {
909
910 log.status() << "Removing unused functions" << messaget::eom;
912 }
913
914 if(cmdline.isset("undefined-function-is-assume-false"))
915 {
918 }
919
920 // write new binary?
921 if(cmdline.args.size()==2)
922 {
923 log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'"
924 << messaget::eom;
925
928 else
930 }
931 else if(cmdline.args.size() < 2)
932 {
934 "Invalid number of positional arguments passed",
935 "[in] [out]",
936 "goto-instrument needs one input and one output file, aside from other "
937 "flags");
938 }
939
940 help();
942 }
943// NOLINTNEXTLINE(readability/fn_size)
944}
945
947 bool force)
948{
950 return;
951
953
954 log.status() << "Function Pointer Removal" << messaget::eom;
956 log.status() << "Virtual function removal" << messaget::eom;
958 log.status() << "Cleaning inline assembler statements" << messaget::eom;
960}
961
966{
967 // Don't bother if we've already done a full function pointer
968 // removal.
970 {
971 return;
972 }
973
974 log.status() << "Removing const function pointers only" << messaget::eom;
978 true); // abort if we can't resolve via const pointers
979}
980
982{
984 return;
985
987
988 if(!cmdline.isset("inline"))
989 {
990 log.status() << "Partial Inlining" << messaget::eom;
992 }
993}
994
996{
998 return;
999
1001
1002 log.status() << "Removing returns" << messaget::eom;
1004}
1005
1007{
1008 log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'"
1009 << messaget::eom;
1010
1012
1014
1015 if(!result.has_value())
1016 throw 0;
1017
1018 goto_model = std::move(result.value());
1019
1021}
1022
1024{
1025 optionst options;
1026
1028
1029 // disable simplify when adding various checks?
1030 if(cmdline.isset("no-simplify"))
1031 options.set_option("simplify", false);
1032 else
1033 options.set_option("simplify", true);
1034
1035 // all checks supported by goto_check
1037
1038 // initialize argv with valid pointers
1039 if(cmdline.isset("model-argc-argv"))
1040 {
1041 unsigned max_argc=
1042 safe_string2unsigned(cmdline.get_value("model-argc-argv"));
1043
1044 log.status() << "Adding up to " << max_argc << " command line arguments"
1045 << messaget::eom;
1047 throw 0;
1048 }
1049
1050 if(cmdline.isset("remove-function-body"))
1051 {
1053 goto_model,
1054 cmdline.get_values("remove-function-body"),
1056 }
1057
1058 // we add the library in some cases, as some analyses benefit
1059
1060 if(
1061 cmdline.isset("add-library") || cmdline.isset("mm") ||
1062 cmdline.isset("reachability-slice") ||
1063 cmdline.isset("reachability-slice-fb") ||
1064 cmdline.isset("fp-reachability-slice"))
1065 {
1066 if(cmdline.isset("show-custom-bitvector-analysis") ||
1067 cmdline.isset("custom-bitvector-analysis"))
1068 {
1069 config.ansi_c.defines.push_back(
1070 std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS");
1071 }
1072
1073 // remove inline assembler as that may yield further library function calls
1074 // that need to be resolved
1076
1077 // add the library
1078 log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
1079 << messaget::eom;
1083 // library functions may introduce inline assembler
1084 while(has_asm(goto_model))
1085 {
1091 }
1092 }
1093
1094 {
1096
1097 if(
1101 {
1103
1105 }
1106 }
1107
1108 // skip over selected loops
1109 if(cmdline.isset("skip-loops"))
1110 {
1111 log.status() << "Adding gotos to skip loops" << messaget::eom;
1112 if(skip_loops(
1114 {
1115 throw 0;
1116 }
1117 }
1118
1119 // now do full inlining, if requested
1120 if(cmdline.isset("inline"))
1121 {
1123
1124 if(cmdline.isset("show-custom-bitvector-analysis") ||
1125 cmdline.isset("custom-bitvector-analysis"))
1126 {
1130 }
1131
1132 log.status() << "Performing full inlining" << messaget::eom;
1134 }
1135
1136 if(cmdline.isset("show-custom-bitvector-analysis") ||
1137 cmdline.isset("custom-bitvector-analysis"))
1138 {
1139 log.status() << "Propagating Constants" << messaget::eom;
1142 }
1143
1144 if(cmdline.isset("escape-analysis"))
1145 {
1149
1150 // recalculate numbers, etc.
1152
1153 log.status() << "Escape Analysis" << messaget::eom;
1156 escape_analysis.instrument(goto_model);
1157
1158 // inline added functions, they are often small
1160
1161 // recalculate numbers, etc.
1163 }
1164
1165 if(cmdline.isset("loop-contracts-file"))
1166 {
1167 const auto file_name = cmdline.get_value("loop-contracts-file");
1169 goto_model, file_name, ui_message_handler);
1170 }
1171
1172 // Initialize loop contract config from cmdline.
1173 loop_contract_configt loop_contract_config = {
1177
1178 if(
1181 {
1182 // After instrumentation, all annotated loops will be transformed to
1183 // loops execute exactly once. CBMC by default unwinds transformed loops
1184 // by twice.
1185 // Users may want to disable the default unwinding to avoid duplicate
1186 // assertions.
1187 log.warning() << "**** WARNING: transformed loops will not be unwound "
1188 << "after applying loop contracts. Note that transformed "
1189 << "loops require at least unwinding bounds 2 to pass "
1190 << "the unwinding assertions." << messaget::eom;
1191 }
1192
1194 if(use_dfcc)
1195 {
1196 if(cmdline.get_values(FLAG_DFCC).size() != 1)
1197 {
1199 "Redundant options detected",
1200 "--" FLAG_DFCC,
1201 "Use a single " FLAG_DFCC " option");
1202 }
1203
1205 log.status() << "Trying to force one backedge per target" << messaget::eom;
1207
1208 const irep_idt harness_id(cmdline.get_value(FLAG_DFCC));
1209
1210 std::set<irep_idt> to_replace(
1213
1214 if(
1217 {
1219 "Mutually exclusive options detected",
1221 "Use either --" FLAG_ENFORCE_CONTRACT
1222 " or --" FLAG_ENFORCE_CONTRACT_REC);
1223 }
1224
1228
1229 bool allow_recursive_calls =
1231
1232 std::set<std::string> to_exclude_from_nondet_static(
1233 cmdline.get_values("nondet-static-exclude").begin(),
1234 cmdline.get_values("nondet-static-exclude").end());
1235
1236 dfcc(
1237 options,
1238 goto_model,
1239 harness_id,
1240 to_enforce.empty() ? std::optional<irep_idt>{}
1241 : std::optional<irep_idt>{to_enforce.front()},
1242 allow_recursive_calls,
1243 to_replace,
1244 loop_contract_config,
1245 to_exclude_from_nondet_static,
1247 }
1248 else if((cmdline.isset(FLAG_LOOP_CONTRACTS) ||
1251 {
1253 log.status() << "Trying to force one backedge per target" << messaget::eom;
1255 code_contractst contracts(goto_model, log, loop_contract_config);
1256
1257 std::set<std::string> to_replace(
1260
1261 std::set<std::string> to_enforce(
1264
1265 std::set<std::string> to_exclude_from_nondet_static(
1266 cmdline.get_values("nondet-static-exclude").begin(),
1267 cmdline.get_values("nondet-static-exclude").end());
1268
1269 // It's important to keep the order of contracts instrumentation, i.e.,
1270 // first replacement then enforcement. We rely on contract replacement
1271 // and inlining of sub-function calls to properly annotate all
1272 // assignments.
1273 contracts.replace_calls(to_replace);
1274 contracts.enforce_contracts(to_enforce, to_exclude_from_nondet_static);
1275
1277 {
1278 contracts.apply_loop_contracts(to_exclude_from_nondet_static);
1279 }
1280 }
1281
1282 if(cmdline.isset("value-set-fi-fp-removal"))
1283 {
1286 }
1287
1288 // replace function pointers, if explicitly requested
1289 if(cmdline.isset("remove-function-pointers"))
1290 {
1292 }
1293 else if(cmdline.isset("remove-const-function-pointers"))
1294 {
1296 }
1297
1298 if(cmdline.isset("replace-calls"))
1299 {
1301
1302 replace_callst replace_calls;
1303 replace_calls(goto_model, cmdline.get_values("replace-calls"));
1304 }
1305
1306 if(cmdline.isset("function-inline"))
1307 {
1308 std::string function=cmdline.get_value("function-inline");
1309 PRECONDITION(!function.empty());
1310
1311 bool caching=!cmdline.isset("no-caching");
1312
1314
1315 log.status() << "Inlining calls of function '" << function << "'"
1316 << messaget::eom;
1317
1318 if(!cmdline.isset("log"))
1319 {
1321 goto_model, function, ui_message_handler, true, caching);
1322 }
1323 else
1324 {
1325 std::string filename = cmdline.value_opt("log").value_or("-");
1326 bool have_file = filename != "-";
1327
1329 goto_model, function, ui_message_handler, true, caching);
1330
1331 if(have_file)
1332 {
1333 std::ofstream of(widen_if_needed(filename));
1334
1335 if(!of)
1336 throw "failed to open file "+filename;
1337
1338 of << result;
1339 of.close();
1340 }
1341 else
1342 {
1343 std::cout << result << '\n';
1344 }
1345 }
1346
1349 }
1350
1351 if(cmdline.isset("partial-inline"))
1352 {
1354
1355 log.status() << "Partial inlining" << messaget::eom;
1357
1360 }
1361
1362 if(cmdline.isset("remove-calls-no-body"))
1363 {
1364 log.status() << "Removing calls to functions without a body"
1365 << messaget::eom;
1366
1369
1372 }
1373
1374 if(cmdline.isset("constant-propagator"))
1375 {
1378
1379 log.status() << "Propagating Constants" << messaget::eom;
1380 log.warning() << "**** WARNING: Constant propagation as performed by "
1381 "goto-instrument is not expected to be sound. Do not use "
1382 "--constant-propagator if soundness is important for your "
1383 "use case."
1384 << messaget::eom;
1385
1388 }
1389
1390 if(cmdline.isset("generate-function-body"))
1391 {
1394 c_object_factory_parameterst object_factory_parameters(
1396
1398 cmdline.get_value("generate-function-body-options"),
1399 object_factory_parameters,
1403 std::regex(cmdline.get_value("generate-function-body")),
1405 goto_model,
1407 false);
1408 }
1409
1410 if(cmdline.isset("generate-havocing-body"))
1411 {
1414 c_object_factory_parameterst object_factory_parameters(
1416
1417 auto options_split =
1418 split_string(cmdline.get_value("generate-havocing-body"), ',');
1419 if(options_split.size() < 2)
1421 "not enough arguments for this option", "--generate-havocing-body"};
1422
1423 if(options_split.size() == 2)
1424 {
1426 std::string{"havoc,"} + options_split.back(),
1427 object_factory_parameters,
1431 std::regex(options_split[0]),
1433 goto_model,
1435 false);
1436 }
1437 else
1438 {
1439 CHECK_RETURN(options_split.size() % 2 == 1);
1440 for(size_t i = 1; i + 1 < options_split.size(); i += 2)
1441 {
1443 std::string{"havoc,"} + options_split[i + 1],
1444 object_factory_parameters,
1448 options_split[0],
1449 options_split[i],
1451 goto_model,
1453 }
1454 }
1455 }
1456
1457 // add generic checks, if needed
1460
1461 // check for uninitalized local variables
1462 if(cmdline.isset("uninitialized-check"))
1463 {
1464 log.status() << "Adding checks for uninitialized local variables"
1465 << messaget::eom;
1467 }
1468
1469 // check for maximum call stack size
1470 if(cmdline.isset("stack-depth"))
1471 {
1472 log.status() << "Adding check for maximum call stack size" << messaget::eom;
1474 goto_model,
1475 safe_string2size_t(cmdline.get_value("stack-depth")),
1477 }
1478
1479 // ignore default/user-specified initialization of variables with static
1480 // lifetime
1481 if(cmdline.isset("nondet-static-exclude"))
1482 {
1483 log.status() << "Adding nondeterministic initialization "
1484 "of static/global variables except for "
1485 "the specified ones."
1486 << messaget::eom;
1487 std::set<std::string> to_exclude(
1488 cmdline.get_values("nondet-static-exclude").begin(),
1489 cmdline.get_values("nondet-static-exclude").end());
1491 }
1492 else if(cmdline.isset("nondet-static"))
1493 {
1494 log.status() << "Adding nondeterministic initialization "
1495 "of static/global variables"
1496 << messaget::eom;
1498 }
1499
1500 if(cmdline.isset("slice-global-inits"))
1501 {
1503
1504 log.status() << "Slicing away initializations of unused global variables"
1505 << messaget::eom;
1507 }
1508
1509 if(cmdline.isset("string-abstraction"))
1510 {
1513
1514 log.status() << "String Abstraction" << messaget::eom;
1516 }
1517
1518 // some analyses require function pointer removal and partial inlining
1519
1520 if(cmdline.isset("remove-pointers") ||
1521 cmdline.isset("race-check") ||
1522 cmdline.isset("mm") ||
1523 cmdline.isset("isr") ||
1524 cmdline.isset("concurrency"))
1525 {
1527
1528 log.status() << "Pointer Analysis" << messaget::eom;
1532
1533 if(cmdline.isset("remove-pointers"))
1534 {
1535 // removing pointers
1536 log.status() << "Removing Pointers" << messaget::eom;
1538 }
1539
1540 if(cmdline.isset("race-check"))
1541 {
1542 log.status() << "Adding Race Checks" << messaget::eom;
1544 }
1545
1546 if(cmdline.isset("mm"))
1547 {
1548 std::string mm=cmdline.get_value("mm");
1549 memory_modelt model;
1550
1551 // strategy of instrumentation
1553 if(cmdline.isset("one-event-per-cycle"))
1555 else if(cmdline.isset("minimum-interference"))
1557 else if(cmdline.isset("read-first"))
1559 else if(cmdline.isset("write-first"))
1561 else if(cmdline.isset("my-events"))
1563 else
1564 /* default: instruments all unsafe pairs */
1566
1567 const unsigned max_var=
1568 cmdline.isset("max-var")?
1570 const unsigned max_po_trans=
1571 cmdline.isset("max-po-trans")?
1572 unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1573
1574 if(mm=="tso")
1575 {
1576 log.status() << "Adding weak memory (TSO) Instrumentation"
1577 << messaget::eom;
1578 model=TSO;
1579 }
1580 else if(mm=="pso")
1581 {
1582 log.status() << "Adding weak memory (PSO) Instrumentation"
1583 << messaget::eom;
1584 model=PSO;
1585 }
1586 else if(mm=="rmo")
1587 {
1588 log.status() << "Adding weak memory (RMO) Instrumentation"
1589 << messaget::eom;
1590 model=RMO;
1591 }
1592 else if(mm=="power")
1593 {
1594 log.status() << "Adding weak memory (Power) Instrumentation"
1595 << messaget::eom;
1596 model=Power;
1597 }
1598 else
1599 {
1600 log.error() << "Unknown weak memory model '" << mm << "'"
1601 << messaget::eom;
1602 model=Unknown;
1603 }
1604
1606
1607 if(cmdline.isset("force-loop-duplication"))
1608 loops=all_loops;
1609 if(cmdline.isset("no-loop-duplication"))
1610 loops=no_loop;
1611
1612 if(model!=Unknown)
1614 model,
1616 goto_model,
1617 cmdline.isset("scc"),
1619 !cmdline.isset("cfg-kill"),
1620 cmdline.isset("no-dependencies"),
1621 loops,
1622 max_var,
1623 max_po_trans,
1624 !cmdline.isset("no-po-rendering"),
1625 cmdline.isset("render-cluster-file"),
1626 cmdline.isset("render-cluster-function"),
1627 cmdline.isset("cav11"),
1628 cmdline.isset("hide-internals"),
1630 cmdline.isset("ignore-arrays"));
1631 }
1632
1633 // Interrupt handler
1634 if(cmdline.isset("isr"))
1635 {
1636 log.status() << "Instrumenting interrupt handler" << messaget::eom;
1637 interrupt(
1639 goto_model,
1640 cmdline.get_value("isr"),
1642 }
1643
1644 // Memory-mapped I/O
1645 if(cmdline.isset("mmio"))
1646 {
1647 log.status() << "Instrumenting memory-mapped I/O" << messaget::eom;
1649 }
1650
1651 if(cmdline.isset("concurrency"))
1652 {
1653 log.status() << "Sequentializing concurrency" << messaget::eom;
1655 }
1656 }
1657
1658 if(cmdline.isset("interval-analysis"))
1659 {
1660 log.status() << "Interval analysis" << messaget::eom;
1662 }
1663
1664 if(cmdline.isset("havoc-loops"))
1665 {
1666 log.status() << "Havocking loops" << messaget::eom;
1668 }
1669
1670 if(cmdline.isset("k-induction"))
1671 {
1672 bool base_case=cmdline.isset("base-case");
1673 bool step_case=cmdline.isset("step-case");
1674
1675 if(step_case && base_case)
1676 throw "please specify only one of --step-case and --base-case";
1677 else if(!step_case && !base_case)
1678 throw "please specify one of --step-case and --base-case";
1679
1680 unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1681
1682 if(k==0)
1683 throw "please give k>=1";
1684
1685 log.status() << "Instrumenting k-induction for k=" << k << ", "
1686 << (base_case ? "base case" : "step case") << messaget::eom;
1687
1688 k_induction(goto_model, base_case, step_case, k);
1689 }
1690
1691 if(cmdline.isset("function-enter"))
1692 {
1693 log.status() << "Function enter instrumentation" << messaget::eom;
1695 goto_model,
1696 cmdline.get_value("function-enter"));
1697 }
1698
1699 if(cmdline.isset("function-exit"))
1700 {
1701 log.status() << "Function exit instrumentation" << messaget::eom;
1703 goto_model,
1704 cmdline.get_value("function-exit"));
1705 }
1706
1707 if(cmdline.isset("branch"))
1708 {
1709 log.status() << "Branch instrumentation" << messaget::eom;
1710 branch(
1711 goto_model,
1712 cmdline.get_value("branch"));
1713 }
1714
1715 // add failed symbols
1717
1718 // recalculate numbers, etc.
1720
1721 // add loop ids
1723
1724 // label the assertions
1726
1727 nondet_volatile(goto_model, options);
1728
1729 // reachability slice?
1730 if(cmdline.isset("reachability-slice"))
1731 {
1733
1734 log.status() << "Performing a reachability slice" << messaget::eom;
1735
1736 // reachability_slicer requires that the model has unique location numbers:
1738
1739 if(cmdline.isset("property"))
1740 {
1743 }
1744 else
1746 }
1747
1748 if(cmdline.isset("fp-reachability-slice"))
1749 {
1751
1752 log.status() << "Performing a function pointer reachability slice"
1753 << messaget::eom;
1755 goto_model,
1756 cmdline.get_comma_separated_values("fp-reachability-slice"),
1758 }
1759
1760 // full slice?
1761 if(cmdline.isset("full-slice"))
1762 {
1766 // full_slicer requires that the model has unique location numbers:
1768
1769 log.warning() << "**** WARNING: Experimental option --full-slice, "
1770 << "analysis results may be unsound. See "
1771 << "https://github.com/diffblue/cbmc/issues/260"
1772 << messaget::eom;
1773 log.status() << "Performing a full slice" << messaget::eom;
1774 if(cmdline.isset("property"))
1777 else
1778 {
1780 }
1781 }
1782
1783 // splice option
1784 if(cmdline.isset("splice-call"))
1785 {
1786 log.status() << "Performing call splicing" << messaget::eom;
1787 std::string callercallee=cmdline.get_value("splice-call");
1788 if(splice_call(
1793 throw 0;
1794 }
1795
1796 // aggressive slicer
1797 if(cmdline.isset("aggressive-slice"))
1798 {
1800
1801 // reachability_slicer requires that the model has unique location numbers:
1803
1804 log.status() << "Slicing away initializations of unused global variables"
1805 << messaget::eom;
1807
1808 log.status() << "Performing an aggressive slice" << messaget::eom;
1810
1811 if(cmdline.isset("aggressive-slice-call-depth"))
1812 aggressive_slicer.call_depth =
1813 safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
1814
1815 if(cmdline.isset("aggressive-slice-preserve-function"))
1816 aggressive_slicer.preserve_functions(
1817 cmdline.get_values("aggressive-slice-preserve-function"));
1818
1819 if(cmdline.isset("property"))
1820 aggressive_slicer.user_specified_properties =
1821 cmdline.get_values("property");
1822
1823 if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
1824 aggressive_slicer.name_snippets =
1825 cmdline.get_values("aggressive-slice-preserve-functions-containing");
1826
1827 aggressive_slicer.preserve_all_direct_paths =
1828 cmdline.isset("aggressive-slice-preserve-all-direct-paths");
1829
1830 aggressive_slicer.doit();
1831
1833
1834 log.status() << "Performing a reachability slice" << messaget::eom;
1835 if(cmdline.isset("property"))
1836 {
1839 }
1840 else
1842 }
1843
1844 if(cmdline.isset("ensure-one-backedge-per-target"))
1845 {
1846 log.status() << "Trying to force one backedge per target" << messaget::eom;
1848 }
1849
1850 // recalculate numbers, etc.
1852}
1853
1856{
1857 std::cout << '\n'
1858 << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1859 << align_center_with_border("Copyright (C) 2008-2013") << '\n'
1860 << align_center_with_border("Daniel Kroening") << '\n'
1861 << align_center_with_border("kroening@kroening.com") << '\n';
1862
1863 // clang-format off
1864 std::cout << help_formatter(
1865 "\n"
1866 "Usage: \tPurpose:\n"
1867 "\n"
1868 " {bgoto-instrument} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
1869 " {bgoto-instrument} {y--version} \t show version and exit\n"
1870 " {bgoto-instrument} [options] {uin} [{uout}] \t perform analysis or"
1871 " instrumentation\n"
1872 "\n"
1873 "Dump Source:\n"
1875 " {y--horn} \t print program as constrained horn clauses\n"
1876 "\n"
1877 "Diagnosis:\n"
1880 " {y--show-symbol-table} \t show loaded symbol table\n"
1881 " {y--list-symbols} \t list symbols with type information\n"
1884 " {y--show-locations} \t show all source locations\n"
1885 " {y--dot} \t generate CFG graph in DOT format\n"
1886 " {y--print-internal-representation} \t show verbose internal"
1887 " representation of the program\n"
1888 " {y--list-undefined-functions} \t list functions without body\n"
1889 " {y--list-calls-args} \t list all function calls with their arguments\n"
1890 " {y--call-graph} \t show graph of function calls\n"
1891 " {y--reachable-call-graph} \t show graph of function calls potentially"
1892 " reachable from main function\n"
1895 " {y--validate-goto-binary} \t check the well-formedness of the passed in"
1896 " goto binary and then exit\n"
1897 " {y--interpreter} \t do concrete execution\n"
1898 "\n"
1899 "Data-flow analyses:\n"
1900 " {y--show-struct-alignment} \t show struct members that might be"
1901 " concurrently accessed\n"
1902 " {y--show-threaded} \t show instructions that may be executed by more than"
1903 " one thread\n"
1904 " {y--show-local-safe-pointers} \t show pointer expressions that are"
1905 " trivially dominated by a not-null check\n"
1906 " {y--show-safe-dereferences} \t show pointer expressions that are"
1907 " trivially dominated by a not-null check *and* used as a dereference"
1908 " operand\n"
1909 " {y--show-value-sets} \t show points-to information (using value sets)\n"
1910 " {y--show-global-may-alias} \t show may-alias information over globals\n"
1911 " {y--show-local-bitvector-analysis} \t show procedure-local pointer"
1912 " analysis\n"
1913 " {y--escape-analysis} \t perform escape analysis\n"
1914 " {y--show-escape-analysis} \t show results of escape analysis\n"
1915 " {y--custom-bitvector-analysis} \t perform configurable bitvector"
1916 " analysis\n"
1917 " {y--show-custom-bitvector-analysis} \t show results of configurable"
1918 " bitvector analysis\n"
1919 " {y--interval-analysis} \t perform interval analysis\n"
1920 " {y--show-intervals} \t show results of interval analysis\n"
1921 " {y--show-uninitialized} \t show maybe-uninitialized variables\n"
1922 " {y--show-points-to} \t show points-to information\n"
1923 " {y--show-rw-set} \t show read-write sets\n"
1924 " {y--show-call-sequences} \t show function call sequences\n"
1925 " {y--show-reaching-definitions} \t show reaching definitions\n"
1926 " {y--show-dependence-graph} \t show program-dependence graph\n"
1927 " {y--show-sese-regions} \t show single-entry-single-exit regions\n"
1928 "\n"
1929 "Safety checks:\n"
1930 " {y--no-assertions} \t ignore user assertions\n"
1933 " {y--stack-depth} {un} \t add check that call stack size of non-inlined"
1934 " functions never exceeds {un}\n"
1935 " {y--race-check} \t add floating-point data race checks\n"
1936 "\n"
1937 "Semantic transformations:\n"
1939 " {y--isr} {ufunction} \t instruments an interrupt service routine\n"
1940 " {y--mmio} \t instruments memory-mapped I/O\n"
1941 " {y--nondet-static} \t add nondeterministic initialization of variables"
1942 " with static lifetime\n"
1943 " {y--nondet-static-exclude} {ue} \t same as nondet-static except for the"
1944 " variable {ue} (use multiple times if required)\n"
1945 " {y--nondet-static-matching} {ur} \t add nondeterministic initialization"
1946 " of variables with static lifetime matching regex {ur}\n"
1947 " {y--function-enter} {uf}, {y--function-exit} {uf}, {y--branch} {uf} \t"
1948 " instruments a call to {uf} at the beginning, the exit, or a branch point,"
1949 " respectively\n"
1950 " {y--splice-call} {ucaller},{ucallee} \t prepends a call to {ucallee} in"
1951 " the body of {ucaller}\n"
1952 " {y--check-call-sequence} {useq} \t instruments checks to assert that all"
1953 " call sequences match {useq}\n"
1954 " {y--undefined-function-is-assume-false} \t convert each call to an"
1955 " undefined function to assume(false)\n"
1960 " {y--add-library} \t add models of C library functions\n"
1962 " {y--model-argc-argv} {un} \t model up to {un} command line arguments\n"
1963 " {y--remove-function-body} {uf} remove the implementation of function {uf}"
1964 " (may be repeated)\n"
1967 "\n"
1968 "Semantics-preserving transformations:\n"
1969 " {y--ensure-one-backedge-per-target} \t transform loop bodies such that"
1970 " there is a single edge back to the loop head\n"
1971 " {y--drop-unused-functions} \t drop functions trivially unreachable from"
1972 " main function\n"
1974 " {y--constant-propagator} \t propagate constants and simplify"
1975 " expressions\n"
1976 " {y--inline} \t perform full inlining\n"
1977 " {y--partial-inline} \t perform partial inlining\n"
1978 " {y--function-inline} {ufunction} \t transitively inline all calls"
1979 " {ufunction} makes\n"
1980 " {y--no-caching} \t disable caching of intermediate results during"
1981 " transitive function inlining\n"
1982 " {y--log} {ufile} \t log in JSON format which code segments were inlined,"
1983 " use with {y--function-inline}\n"
1984 " {y--remove-function-pointers} \t replace function pointers by case"
1985 " statement over function calls\n"
1987 " {y--value-set-fi-fp-removal} \t build flow-insensitive value set and"
1988 " replace function pointers by a case statement over the possible"
1989 " assignments. If the set of possible assignments is empty the function"
1990 " pointer is removed using the standard remove-function-pointers pass.\n"
1991 "\n"
1992 "Loop information and transformations:\n"
1994 " {y--unwindset-file_<file>} \t read unwindset from file\n"
1995 " {y--partial-loops} \t permit paths with partial loops\n"
1996 " {y--unwinding-assertions} \t generate unwinding assertions"
1997 " (enabled by default)\n"
1998 " {y--no-unwinding-assertions} \t do not generate unwinding assertions\n"
1999 " {y--continue-as-loops} \t add loop for remaining iterations after"
2000 " unwound part\n"
2001 " {y--k-induction} {uk} \t check loops with k-induction\n"
2002 " {y--step-case} \t k-induction: do step-case\n"
2003 " {y--base-case} \t k-induction: do base-case\n"
2004 " {y--havoc-loops} \t over-approximate all loops\n"
2005 " {y--accelerate} \t add loop accelerators\n"
2006 " {y--z3} \t use Z3 when computing loop accelerators\n"
2007 " {y--skip-loops {uloop-ids} \t add gotos to skip selected loops during"
2008 " execution\n"
2009 " {y--show-lexical-loops} \t show single-entry-single-back-edge loops\n"
2010 " {y--show-natural-loops} \t show natural loop heads\n"
2011 "\n"
2012 "Memory model instrumentations:\n"
2014 "\n"
2015 "Slicing:\n"
2018 " {y--full-slice} \t slice away instructions that don't affect assertions\n"
2019 " {y--property} {uid} \t slice with respect to specific property only\n"
2020 " {y--slice-global-inits} \t slice away initializations of unused global"
2021 " variables\n"
2022 " {y--aggressive-slice} \t remove bodies of any functions not on the"
2023 " shortest path between the start function and the function containing the"
2024 " property/properties\n"
2025 " {y--aggressive-slice-call-depth} {un} \t used with aggressive-slice,"
2026 " preserves all functions within {un} function calls of the functions on"
2027 " the shortest path\n"
2028 " {y--aggressive-slice-preserve-function} {uf} \t force the aggressive"
2029 " slicer to preserve function {uf}\n"
2030 " {y--aggressive-slice-preserve-functions-containing} {uf} \t force the"
2031 " aggressive slicer to preserve all functions with names containing {uf}\n"
2032 " {y--aggressive-slice-preserve-all-direct-paths} \t force aggressive"
2033 " slicer to preserve all direct paths\n"
2034 "\n"
2035 "Code contracts:\n"
2036 HELP_DFCC
2044 "\n"
2045 "User-interface options:\n"
2047 " {y--xml} \t output files in XML where supported\n"
2048 " {y--xml-ui} \t use XML-formatted output\n"
2049 " {y--json-ui} \t use JSON-formatted output\n"
2050 " {y--verbosity} {u#} \t verbosity level\n"
2052 "\n");
2053 // clang-format on
2054}
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
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_table_baset &symbol_table, std::ostream &out)
Alignment Checks.
void cprover_c_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
#define HELP_ANSI_C_LANGUAGE
configt config
Definition config.cpp:25
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition branch.cpp:21
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,...
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:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
void output(std::ostream &out) const
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
Non-graph-based representation of the class hierarchy.
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:131
argst args
Definition cmdline.h:154
std::optional< std::string > value_opt(char option) const
Definition cmdline.cpp:53
const std::list< std::string > & get_values(const std::string &option) const
Definition cmdline.cpp:119
bool set(const cmdlinet &cmdline)
Definition config.cpp:863
void set_from_symbol_table(const symbol_table_baset &)
Definition config.cpp:1363
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
void get(const std::string &executable)
This is a may analysis (i.e.
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_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:105
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
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...
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:391
message_handlert & get_message_handler()
Definition message.h:183
mstreamt & warning() const
Definition message.h:396
@ M_STATUS
Definition message.h:169
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
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().
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
ui_message_handlert ui_message_handler
Expression to hold a symbol (variable)
Definition std_expr.h:131
Symbol table entry.
Definition symbol.h:28
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
virtual uit get_ui() const
Definition ui_message.h:33
void parse_unwind(const std::string &unwind)
Definition unwindset.cpp:23
void parse_unwindset(const std::list< std::string > &unwindset, abstract_goto_modelt &goto_model, message_handlert &message_handler)
void parse_unwindset_file(const std::string &file_name, abstract_goto_modelt &goto_model, message_handlert &message_handler)
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.
#define HELP_CONFIG_LIBRARY
Definition config.h:85
Constant propagation.
#define HELP_REPLACE_CALL
Definition contracts.h:51
#define HELP_DISABLE_SIDE_EFFECT_CHECK
Definition contracts.h:38
#define FLAG_REPLACE_CALL
Definition contracts.h:50
#define FLAG_ENFORCE_CONTRACT
Definition contracts.h:55
#define HELP_LOOP_CONTRACTS
Definition contracts.h:33
#define FLAG_LOOP_CONTRACTS
Definition contracts.h:32
#define HELP_LOOP_CONTRACTS_NO_UNWIND
Definition contracts.h:42
#define HELP_ENFORCE_CONTRACT
Definition contracts.h:56
#define HELP_LOOP_CONTRACTS_FILE
Definition contracts.h:46
#define FLAG_DISABLE_SIDE_EFFECT_CHECK
Definition contracts.h:36
#define FLAG_LOOP_CONTRACTS_NO_UNWIND
Definition contracts.h:41
void count_eloc(const goto_modelt &goto_model)
void print_global_state_size(const goto_modelt &goto_model)
void print_path_lengths(const goto_modelt &goto_model)
void list_eloc(const goto_modelt &goto_model)
#define HELP_GOTO_PROGRAM_STATS
Definition count_eloc.h:30
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
static void show_goto_functions(const goto_modelt &goto_model)
#define CPROVER_PREFIX
Field-insensitive, location-sensitive bitvector analysis.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
#define FLAG_ENFORCE_CONTRACT_REC
Definition dfcc.h:62
#define FLAG_DFCC
Definition dfcc.h:54
#define HELP_DFCC
Definition dfcc.h:57
#define HELP_ENFORCE_CONTRACT_REC
Definition dfcc.h:64
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:359
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:1681
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:1668
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:1703
#define HELP_DUMP_C
Definition dump_c.h:51
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 property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties, message_handlert &message_handler)
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion, message_handlert &message_handler)
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition function.cpp:102
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition function.cpp:77
Function Entering and Exiting.
void configure_gcc(const gcc_versiont &gcc_version)
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, bool ignore_no_match)
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.
static void transform_assertions_assumptions(goto_programt &goto_program, bool enable_assertions, bool enable_built_in_assertions, bool enable_assumptions)
Checks for Errors in C and Java Programs.
void goto_check_c(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
#define HELP_GOTO_CHECK
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Inline every function call into the entry_point() function.
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, message_handlert &message_handler)
Remove dereferences in all expressions contained in the program goto_model.
#define HELP_REMOVE_POINTERS
void dfcc(const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const loop_contract_configt loop_contract_config, const std::set< std::string > &to_exclude_from_nondet_static, message_handlert &message_handler)
Applies function contracts transformation to GOTO model, using the dynamic frame condition checking a...
Definition dfcc.cpp:93
Guard Data Structure.
void havoc_loops(goto_modelt &goto_model)
Havoc Loops.
Help Formatter.
static help_formattert help_formatter(const std::string &s)
void horn_encoding(const goto_modelt &goto_model, std::ostream &out)
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, message_handlert &message_handler)
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.
void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
Definition mm_io.cpp:154
Perform Memory-mapped I/O instrumentation.
static void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, message_handlert &message_handler)
Definition mmio.cpp:24
Memory-mapped I/O Instrumentation for Goto Programs.
bool model_argc_argv(goto_modelt &goto_model, unsigned max_argc, message_handlert &message_handler)
Set up argv with up to max_argc pointers into an array of 4096 bytes.
Initialize command line arguments.
Compute natural loops in a goto_function.
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
void nondet_static_matching(goto_modelt &goto_model, const std::string &regex)
Nondeterministically initializes global scope variables that match the given regex.
static void nondet_static(const namespacet &ns, goto_modelt &goto_model, 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
Options.
void parameter_assignments(symbol_table_baset &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_table_baset &symbol_table, const irep_idt &function_id, goto_programt &goto_program, w_guardst &w_guards, message_handlert &message_handler)
Race Detection for Threaded Goto Programs.
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability, message_handlert &message_handler)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
void function_path_reachability_slicer(goto_modelt &goto_model, const std::list< std::string > &functions_list, message_handlert &message_handler)
Perform reachability slicing on goto_model for selected functions.
#define HELP_FP_REACHABILITY_SLICER
#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, message_handlert &message_handler)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
bool has_asm(const goto_functionst &goto_functions)
returns true iff the given goto functions use asm instructions
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.
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, 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
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
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
static std::optional< exprt > rewrite_rw_ok(exprt expr, const namespacet &ns)
Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state.
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.
#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_table_baset &symbol_table, ui_message_handlert &ui)
void show_symbol_table_brief(const symbol_table_baset &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)
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_table_baset &symbol_table, message_handlert &message_handler)
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)
Stack depth checks.
unsigned safe_string2unsigned(const std::string &str, int base)
unsigned unsafe_string2unsigned(const std::string &str, int base)
std::size_t safe_string2size_t(const std::string &str, int base)
void string_abstraction(goto_modelt &goto_model, message_handlert &message_handler)
String Abstraction.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition guard_expr.h:20
Loop contract configurations.
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.
#define widen_if_needed(s)
Definition unicode.h:28
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
#define HELP_UNINITIALIZED_CHECK
Loop unwinding.
#define HELP_UNWINDSET
Definition unwindset.h:78
#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:92
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
static void write_goto_binary(std::ostream &out, const symbol_table_baset &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
Write GOTO binaries.