cprover
jbmc_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JBMC Command Line Option Processing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "jbmc_parse_options.h"
13
14#include <cstdlib> // exit()
15#include <iostream>
16#include <memory>
17
18#include <util/config.h>
19#include <util/exit_codes.h>
20#include <util/invariant.h>
21#include <util/make_unique.h>
22#include <util/version.h>
23#include <util/xml.h>
24
25#include <langapi/language.h>
26
28
34
47
51
53
55
57
58#include <langapi/mode.h>
59
72
73jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
76 argc,
77 argv,
78 std::string("JBMC ") + CBMC_VERSION)
79{
83
85 int argc,
86 const char **argv,
87 const std::string &extra_options)
89 JBMC_OPTIONS + extra_options,
90 argc,
91 argv,
92 std::string("JBMC ") + CBMC_VERSION)
93{
96}
97
99{
100 // Default true
101 options.set_option("assertions", true);
102 options.set_option("assumptions", true);
103 options.set_option("built-in-assertions", true);
104 options.set_option("lazy-methods", true);
105 options.set_option("pretty-names", true);
106 options.set_option("propagation", true);
107 options.set_option("refine-strings", true);
108 options.set_option("sat-preprocessor", true);
109 options.set_option("simple-slice", true);
110 options.set_option("simplify", true);
111 options.set_option("simplify-if", true);
112 options.set_option("show-goto-symex-steps", false);
113
114 // Other default
115 options.set_option("arrays-uf", "auto");
116 options.set_option("depth", UINT32_MAX);
117}
118
120{
121 if(config.set(cmdline))
122 {
123 usage_error();
124 exit(1); // should contemplate EX_USAGE from sysexits.h
125 }
126
128
129 if(cmdline.isset("function"))
130 options.set_option("function", cmdline.get_value("function"));
131
134
135 if(cmdline.isset("max-field-sensitivity-array-size"))
136 {
137 options.set_option(
138 "max-field-sensitivity-array-size",
139 cmdline.get_value("max-field-sensitivity-array-size"));
140 }
141
142 if(cmdline.isset("no-array-field-sensitivity"))
143 {
144 if(cmdline.isset("max-field-sensitivity-array-size"))
145 {
146 log.error()
147 << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
148 << " must not be given together" << messaget::eom;
150 }
151 options.set_option("no-array-field-sensitivity", true);
152 }
153
154 if(cmdline.isset("show-symex-strategies"))
155 {
158 }
159
161
162 if(cmdline.isset("program-only"))
163 options.set_option("program-only", true);
164
165 if(cmdline.isset("show-vcc"))
166 options.set_option("show-vcc", true);
167
168 if(cmdline.isset("nondet-static"))
169 options.set_option("nondet-static", true);
170
171 if(cmdline.isset("no-simplify"))
172 options.set_option("simplify", false);
173
174 if(cmdline.isset("stop-on-fail") ||
175 cmdline.isset("dimacs") ||
176 cmdline.isset("outfile"))
177 options.set_option("stop-on-fail", true);
178
179 if(
180 cmdline.isset("trace") || cmdline.isset("compact-trace") ||
181 cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
183 !cmdline.isset("cover")))
184 {
185 options.set_option("trace", true);
186 }
187
188 if(cmdline.isset("validate-trace"))
189 {
190 options.set_option("validate-trace", true);
191 options.set_option("trace", true);
192 }
193
194 if(cmdline.isset("localize-faults"))
195 options.set_option("localize-faults", true);
196
197 if(cmdline.isset("symex-complexity-limit"))
198 {
199 options.set_option(
200 "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
201 }
202
203 if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
204 {
205 options.set_option(
206 "symex-complexity-failed-child-loops-limit",
207 cmdline.get_value("symex-complexity-failed-child-loops-limit"));
208 }
209
210 if(cmdline.isset("unwind"))
211 options.set_option("unwind", cmdline.get_value("unwind"));
212
213 if(cmdline.isset("depth"))
214 options.set_option("depth", cmdline.get_value("depth"));
215
216 if(cmdline.isset("debug-level"))
217 options.set_option("debug-level", cmdline.get_value("debug-level"));
218
219 if(cmdline.isset("unwindset"))
220 options.set_option("unwindset", cmdline.get_value("unwindset"));
221
222 // constant propagation
223 if(cmdline.isset("no-propagation"))
224 options.set_option("propagation", false);
225
226 // transform self loops to assumptions
227 options.set_option(
228 "self-loops-to-assumptions",
229 !cmdline.isset("no-self-loops-to-assumptions"));
230
231 // all checks supported by goto_check_java
233
234 // unwind loops in java enum static initialization
235 if(cmdline.isset("java-unwind-enum-static"))
236 options.set_option("java-unwind-enum-static", true);
237
238 // check assertions
239 if(cmdline.isset("no-assertions"))
240 options.set_option("assertions", false);
241
242 // use assumptions
243 if(cmdline.isset("no-assumptions"))
244 options.set_option("assumptions", false);
245
246 // generate unwinding assertions
247 if(cmdline.isset("unwinding-assertions"))
248 options.set_option("unwinding-assertions", true);
249
250 // generate unwinding assumptions otherwise
251 options.set_option(
252 "partial-loops",
253 cmdline.isset("partial-loops"));
254
255 if(options.get_bool_option("partial-loops") &&
256 options.get_bool_option("unwinding-assertions"))
257 {
258 log.error() << "--partial-loops and --unwinding-assertions "
259 << "must not be given together" << messaget::eom;
260 exit(1); // should contemplate EX_USAGE from sysexits.h
261 }
262
263 // remove unused equations
264 options.set_option(
265 "slice-formula",
266 cmdline.isset("slice-formula"));
267
268 // simplify if conditions and branches
269 if(cmdline.isset("no-simplify-if"))
270 options.set_option("simplify-if", false);
271
272 if(cmdline.isset("arrays-uf-always"))
273 options.set_option("arrays-uf", "always");
274 else if(cmdline.isset("arrays-uf-never"))
275 options.set_option("arrays-uf", "never");
276
277 if(cmdline.isset("dimacs"))
278 options.set_option("dimacs", true);
279
280 if(cmdline.isset("refine-arrays"))
281 {
282 options.set_option("refine", true);
283 options.set_option("refine-arrays", true);
284 }
285
286 if(cmdline.isset("refine-arithmetic"))
287 {
288 options.set_option("refine", true);
289 options.set_option("refine-arithmetic", true);
290 }
291
292 if(cmdline.isset("refine"))
293 {
294 options.set_option("refine", true);
295 options.set_option("refine-arrays", true);
296 options.set_option("refine-arithmetic", true);
297 }
298
299 if(cmdline.isset("no-refine-strings"))
300 options.set_option("refine-strings", false);
301
302 if(cmdline.isset("string-printable") && cmdline.isset("no-refine-strings"))
303 {
305 "cannot use --string-printable with --no-refine-strings",
306 "--string-printable");
307 }
308
309 if(cmdline.isset("string-input-value") && cmdline.isset("no-refine-strings"))
310 {
312 "cannot use --string-input-value with --no-refine-strings",
313 "--string-input-value");
314 }
315
316 if(
317 cmdline.isset("no-refine-strings") &&
318 cmdline.isset("max-nondet-string-length"))
319 {
321 "cannot use --max-nondet-string-length with --no-refine-strings",
322 "--max-nondet-string-length");
323 }
324
325 if(cmdline.isset("max-node-refinement"))
326 options.set_option(
327 "max-node-refinement",
328 cmdline.get_value("max-node-refinement"));
329
330 // SMT Options
331
332 if(cmdline.isset("smt1"))
333 {
334 log.error() << "--smt1 is no longer supported" << messaget::eom;
336 }
337
338 if(cmdline.isset("smt2"))
339 options.set_option("smt2", true);
340
341 if(cmdline.isset("fpa"))
342 options.set_option("fpa", true);
343
344 bool solver_set=false;
345
346 if(cmdline.isset("boolector"))
347 {
348 options.set_option("boolector", true), solver_set=true;
349 options.set_option("smt2", true);
350 }
351
352 if(cmdline.isset("mathsat"))
353 {
354 options.set_option("mathsat", true), solver_set=true;
355 options.set_option("smt2", true);
356 }
357
358 if(cmdline.isset("cvc4"))
359 {
360 options.set_option("cvc4", true), solver_set=true;
361 options.set_option("smt2", true);
362 }
363
364 if(cmdline.isset("yices"))
365 {
366 options.set_option("yices", true), solver_set=true;
367 options.set_option("smt2", true);
368 }
369
370 if(cmdline.isset("z3"))
371 {
372 options.set_option("z3", true), solver_set=true;
373 options.set_option("smt2", true);
374 }
375
376 if(cmdline.isset("smt2") && !solver_set)
377 {
378 if(cmdline.isset("outfile"))
379 {
380 // outfile and no solver should give standard compliant SMT-LIB
381 options.set_option("generic", true);
382 }
383 else
384 {
385 // the default smt2 solver
386 options.set_option("z3", true);
387 }
388 }
389
390 if(cmdline.isset("beautify"))
391 options.set_option("beautify", true);
392
393 if(cmdline.isset("no-sat-preprocessor"))
394 options.set_option("sat-preprocessor", false);
395
396 options.set_option(
397 "pretty-names",
398 !cmdline.isset("no-pretty-names"));
399
400 if(cmdline.isset("outfile"))
401 options.set_option("outfile", cmdline.get_value("outfile"));
402
403 if(cmdline.isset("graphml-witness"))
404 {
405 options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
406 options.set_option("stop-on-fail", true);
407 options.set_option("trace", true);
408 }
409
410 if(cmdline.isset("symex-coverage-report"))
411 options.set_option(
412 "symex-coverage-report",
413 cmdline.get_value("symex-coverage-report"));
414
415 if(cmdline.isset("validate-ssa-equation"))
416 {
417 options.set_option("validate-ssa-equation", true);
418 }
419
420 if(cmdline.isset("validate-goto-model"))
421 {
422 options.set_option("validate-goto-model", true);
423 }
424
425 options.set_option(
426 "symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
427
429
430 if(cmdline.isset("no-lazy-methods"))
431 options.set_option("lazy-methods", false);
432
433 if(cmdline.isset("symex-driven-lazy-loading"))
434 {
435 options.set_option("symex-driven-lazy-loading", true);
436 for(const char *opt :
437 { "nondet-static",
438 "full-slice",
439 "reachability-slice",
440 "reachability-slice-fb" })
441 {
442 if(cmdline.isset(opt))
443 {
444 throw std::string("Option ") + opt +
445 " can't be used with --symex-driven-lazy-loading";
446 }
447 }
448 }
449
450 // The 'allow-pointer-unsoundness' option prevents symex from throwing an
451 // exception when it encounters pointers that are shared across threads.
452 // This is unsound but given that pointers are ubiquitous in java this check
453 // must be disabled in order to support the analysis of multithreaded java
454 // code.
455 if(cmdline.isset("java-threading"))
456 options.set_option("allow-pointer-unsoundness", true);
457
458 if(cmdline.isset("show-goto-symex-steps"))
459 options.set_option("show-goto-symex-steps", true);
460}
461
464{
465 if(cmdline.isset("version"))
466 {
467 std::cout << CBMC_VERSION << '\n';
469 }
470
473
474 //
475 // command line options
476 //
477
478 optionst options;
480
482
483 // output the options
484 switch(ui_message_handler.get_ui())
485 {
488 log.debug(), [&options](messaget::mstreamt &debug_stream) {
489 debug_stream << "\nOptions: \n";
490 options.output(debug_stream);
491 debug_stream << messaget::eom;
492 });
493 break;
495 {
496 json_objectt json_options{{"options", options.to_json()}};
497 log.debug() << json_options;
498 break;
499 }
501 log.debug() << options.to_xml();
502 break;
503 }
504
507
508 if(!((cmdline.isset("jar") && cmdline.args.empty()) ||
509 (cmdline.isset("gb") && cmdline.args.empty()) ||
510 (!cmdline.isset("jar") && !cmdline.isset("gb") &&
511 (cmdline.args.size() == 1))))
512 {
513 log.error() << "Please give exactly one class name, "
514 << "and/or use -jar jarfile or --gb goto-binary"
515 << messaget::eom;
517 }
518
519 if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree"))
520 {
521 std::string main_class = cmdline.args[0];
522 // `java` accepts slashes and dots as package separators
523 std::replace(main_class.begin(), main_class.end(), '/', '.');
524 config.java.main_class = main_class;
525 cmdline.args.pop_back();
526 }
527
528 if(cmdline.isset("jar"))
529 {
530 cmdline.args.push_back(cmdline.get_value("jar"));
531 }
532
533 if(cmdline.isset("gb"))
534 {
535 cmdline.args.push_back(cmdline.get_value("gb"));
536 }
537
538 // Shows the parse tree of the main class
539 if(cmdline.isset("show-parse-tree"))
540 {
541 std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
542 CHECK_RETURN(language != nullptr);
543 language->set_language_options(options);
544 language->set_message_handler(ui_message_handler);
545
546 log.status() << "Parsing ..." << messaget::eom;
547
548 if(static_cast<java_bytecode_languaget *>(language.get())->parse())
549 {
550 log.error() << "PARSING ERROR" << messaget::eom;
552 }
553
554 language->show_parse(std::cout);
556 }
557
558 object_factory_params.set(options);
559
561 options.get_bool_option("java-assume-inputs-non-null");
562
563 std::unique_ptr<abstract_goto_modelt> goto_model_ptr;
564 int get_goto_program_ret = get_goto_program(goto_model_ptr, options);
565 if(get_goto_program_ret != -1)
566 return get_goto_program_ret;
567
568 if(
569 options.get_bool_option("program-only") ||
570 options.get_bool_option("show-vcc") ||
571 (options.get_bool_option("symex-driven-lazy-loading") &&
572 (cmdline.isset("show-symbol-table") || cmdline.isset("list-symbols") ||
573 cmdline.isset("show-goto-functions") ||
574 cmdline.isset("list-goto-functions") ||
575 cmdline.isset("show-properties") || cmdline.isset("show-loops"))))
576 {
577 if(options.get_bool_option("paths"))
578 {
580 options, ui_message_handler, *goto_model_ptr);
581 (void)verifier();
582 }
583 else
584 {
586 options, ui_message_handler, *goto_model_ptr);
587 (void)verifier();
588 }
589
590 if(options.get_bool_option("symex-driven-lazy-loading"))
591 {
592 // We can only output these after goto-symex has run.
593 (void)show_loaded_symbols(*goto_model_ptr);
594 (void)show_loaded_functions(*goto_model_ptr);
595 }
596
598 }
599
600 if(
601 options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
602 {
603 if(options.get_bool_option("paths"))
604 {
606 options, ui_message_handler, *goto_model_ptr);
607 (void)verifier();
608 }
609 else
610 {
612 options, ui_message_handler, *goto_model_ptr);
613 (void)verifier();
614 }
615
617 }
618
619 std::unique_ptr<goto_verifiert> verifier = nullptr;
620
621 if(
622 options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
623 {
624 verifier =
625 util_make_unique<stop_on_fail_verifiert<java_single_path_symex_checkert>>(
626 options, ui_message_handler, *goto_model_ptr);
627 }
628 else if(
629 options.get_bool_option("stop-on-fail") &&
630 !options.get_bool_option("paths"))
631 {
632 if(options.get_bool_option("localize-faults"))
633 {
634 verifier =
637 options, ui_message_handler, *goto_model_ptr);
638 }
639 else
640 {
641 verifier = util_make_unique<
643 options, ui_message_handler, *goto_model_ptr);
644 }
645 }
646 else if(
647 !options.get_bool_option("stop-on-fail") &&
648 options.get_bool_option("paths"))
649 {
652 options, ui_message_handler, *goto_model_ptr);
653 }
654 else if(
655 !options.get_bool_option("stop-on-fail") &&
656 !options.get_bool_option("paths"))
657 {
658 if(options.get_bool_option("localize-faults"))
659 {
660 verifier =
663 options, ui_message_handler, *goto_model_ptr);
664 }
665 else
666 {
669 options, ui_message_handler, *goto_model_ptr);
670 }
671 }
672 else
673 {
675 }
676
677 const resultt result = (*verifier)();
678 verifier->report();
679 return result_to_exit_code(result);
680}
681
683 std::unique_ptr<abstract_goto_modelt> &goto_model_ptr,
684 const optionst &options)
685{
686 if(options.is_set("context-include") || options.is_set("context-exclude"))
687 method_context = get_context(options);
688 lazy_goto_modelt lazy_goto_model =
690 lazy_goto_model.initialize(cmdline.args, options);
691
693 util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
694
695 // Show the class hierarchy
696 if(cmdline.isset("show-class-hierarchy"))
697 {
700 }
701
702 // Add failed symbols for any symbol created prior to loading any
703 // particular function:
704 add_failed_symbols(lazy_goto_model.symbol_table);
705
706 if(!options.get_bool_option("symex-driven-lazy-loading"))
707 {
708 log.status() << "Generating GOTO Program" << messaget::eom;
709 lazy_goto_model.load_all_functions();
710
711 // show symbol table or list symbols
712 if(show_loaded_symbols(lazy_goto_model))
714
715 // Move the model out of the local lazy_goto_model
716 // and into the caller's goto_model
718 std::move(lazy_goto_model));
719 if(goto_model_ptr == nullptr)
721
722 goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
723
724 if(cmdline.isset("validate-goto-model"))
725 {
726 goto_model.validate();
727 }
728
729 if(show_loaded_functions(goto_model))
731
732 if(cmdline.isset("property"))
733 ::set_properties(goto_model, cmdline.get_values("property"));
734 }
735 else
736 {
737 // The precise wording of this error matches goto-symex's complaint when no
738 // __CPROVER_start exists (if we just go ahead and run it anyway it will
739 // trip an invariant when it tries to load it)
741 {
742 log.error() << "the program has no entry point" << messaget::eom;
744 }
745
746 if(cmdline.isset("validate-goto-model"))
747 {
748 lazy_goto_model.validate();
749 }
750
751 goto_model_ptr =
752 util_make_unique<lazy_goto_modelt>(std::move(lazy_goto_model));
753 }
754
756
757 return -1; // no error, continue
758}
759
761 goto_model_functiont &function,
762 const abstract_goto_modelt &model,
763 const optionst &options)
764{
765 journalling_symbol_tablet &symbol_table = function.get_symbol_table();
766 namespacet ns(symbol_table);
767 goto_functionst::goto_functiont &goto_function = function.get_goto_function();
768
769 bool using_symex_driven_loading =
770 options.get_bool_option("symex-driven-lazy-loading");
771
772 // Removal of RTTI inspection:
774 function.get_function_id(),
775 goto_function,
776 symbol_table,
779 // Java virtual functions -> explicit dispatch tables:
781
782 auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
783 return symbol_table.lookup_ref(id).value.is_nil() &&
784 !model.can_produce_function(id);
785 };
786
787 remove_returns(function, function_is_stub);
788
789 replace_java_nondet(function);
790
791 // Similar removal of java nondet statements:
793
794 if(using_symex_driven_loading)
795 {
796 // remove exceptions
797 // If using symex-driven function loading we need to do this now so that
798 // symex doesn't have to cope with exception-handling constructs; however
799 // the results are slightly worse than running it in whole-program mode
800 // (e.g. dead catch sites will be retained)
802 function.get_function_id(),
803 goto_function.body,
804 symbol_table,
805 *class_hierarchy.get(),
807 }
808
809 // add generic checks
811 function.get_function_id(),
812 function.get_goto_function(),
813 ns,
814 options,
816
817 // Replace Java new side effects
819 function.get_function_id(),
820 goto_function,
821 symbol_table,
823
824 // checks don't know about adjusted float expressions
825 adjust_float_expressions(goto_function, ns);
826
827 // add failed symbols for anything created relating to this particular
828 // function (note this means subsequent passes mustn't create more!):
830 symbol_table.get_inserted();
831 for(const irep_idt &new_symbol_name : new_symbols)
832 {
834 symbol_table.lookup_ref(new_symbol_name), symbol_table);
835 }
836
837 // If using symex-driven function loading we must label the assertions
838 // now so symex sees its targets; otherwise we leave this until
839 // process_goto_functions, as we haven't run remove_exceptions yet, and that
840 // pass alters the CFG.
841 if(using_symex_driven_loading)
842 {
843 // label the assertions
844 label_properties(goto_function.body);
845
846 goto_function.body.update();
847 function.compute_location_numbers();
848 goto_function.body.compute_loop_numbers();
849 }
850}
851
853 const abstract_goto_modelt &goto_model)
854{
855 if(cmdline.isset("show-symbol-table"))
856 {
858 return true;
859 }
860 else if(cmdline.isset("list-symbols"))
861 {
863 return true;
864 }
865
866 return false;
867}
868
870 const abstract_goto_modelt &goto_model)
871{
872 if(cmdline.isset("show-loops"))
873 {
875 return true;
876 }
877
878 if(
879 cmdline.isset("show-goto-functions") ||
880 cmdline.isset("list-goto-functions"))
881 {
882 namespacet ns(goto_model.get_symbol_table());
884 ns,
886 goto_model.get_goto_functions(),
887 cmdline.isset("list-goto-functions"));
888 return true;
889 }
890
891 if(cmdline.isset("show-properties"))
892 {
893 namespacet ns(goto_model.get_symbol_table());
895 return true;
896 }
897
898 return false;
899}
900
902 goto_modelt &goto_model,
903 const optionst &options)
904{
905 log.status() << "Running GOTO functions transformation passes"
906 << messaget::eom;
907
908 bool using_symex_driven_loading =
909 options.get_bool_option("symex-driven-lazy-loading");
910
911 // When using symex-driven lazy loading, *all* relevant processing is done
912 // during process_goto_function, so we have nothing to do here.
913 if(using_symex_driven_loading)
914 return false;
915
916 // remove catch and throw
918
919 // instrument library preconditions
920 instrument_preconditions(goto_model);
921
922 // ignore default/user-specified initialization
923 // of variables with static lifetime
924 if(cmdline.isset("nondet-static"))
925 {
926 log.status() << "Adding nondeterministic initialization "
927 "of static/global variables"
928 << messaget::eom;
929 nondet_static(goto_model);
930 }
931
932 // recalculate numbers, etc.
933 goto_model.goto_functions.update();
934
935 if(cmdline.isset("drop-unused-functions"))
936 {
937 // Entry point will have been set before and function pointers removed
938 log.status() << "Removing unused functions" << messaget::eom;
940 }
941
942 // remove skips such that trivial GOTOs are deleted
943 remove_skip(goto_model);
944
945 // label the assertions
946 // This must be done after adding assertions and
947 // before using the argument of the "property" option.
948 // Do not re-label after using the property slicer because
949 // this would cause the property identifiers to change.
950 label_properties(goto_model);
951
952 // reachability slice?
953 if(cmdline.isset("reachability-slice-fb"))
954 {
955 if(cmdline.isset("reachability-slice"))
956 {
957 log.error() << "--reachability-slice and --reachability-slice-fb "
958 << "must not be given together" << messaget::eom;
959 return true;
960 }
961
962 log.status() << "Performing a forwards-backwards reachability slice"
963 << messaget::eom;
964 if(cmdline.isset("property"))
965 reachability_slicer(goto_model, cmdline.get_values("property"), true);
966 else
967 reachability_slicer(goto_model, true);
968 }
969
970 if(cmdline.isset("reachability-slice"))
971 {
972 log.status() << "Performing a reachability slice" << messaget::eom;
973 if(cmdline.isset("property"))
974 reachability_slicer(goto_model, cmdline.get_values("property"));
975 else
976 reachability_slicer(goto_model);
977 }
978
979 // full slice?
980 if(cmdline.isset("full-slice"))
981 {
982 log.status() << "Performing a full slice" << messaget::eom;
983 if(cmdline.isset("property"))
984 property_slicer(goto_model, cmdline.get_values("property"));
985 else
986 full_slicer(goto_model);
987 }
988
989 // remove any skips introduced
990 remove_skip(goto_model);
991
992 return false;
993}
994
996{
997 static const irep_idt initialize_id = INITIALIZE_FUNCTION;
998
999 return name != goto_functionst::entry_point() && name != initialize_id;
1000}
1001
1003 const irep_idt &function_name,
1004 symbol_table_baset &symbol_table,
1005 goto_functiont &function,
1006 bool body_available)
1007{
1008 // Provide a simple stub implementation for any function we don't have a
1009 // bytecode implementation for:
1010
1011 if(
1012 body_available &&
1013 (!method_context || (*method_context)(id2string(function_name))))
1014 return false;
1015
1016 if(!can_generate_function_body(function_name))
1017 return false;
1018
1019 if(symbol_table.lookup_ref(function_name).mode == ID_java)
1020 {
1022 function_name,
1023 symbol_table,
1027
1028 goto_convert_functionst converter(symbol_table, ui_message_handler);
1029 converter.convert_function(function_name, function);
1030
1031 return true;
1032 }
1033 else
1034 {
1035 return false;
1036 }
1037}
1038
1041{
1042 // clang-format off
1043 std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
1044 << align_center_with_border("Copyright (C) 2001-2018") << '\n'
1045 << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
1046 << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
1047 << align_center_with_border("kroening@kroening.com") << '\n'
1048 << "\n"
1049 "Usage: Purpose:\n"
1050 "\n"
1051 " jbmc [-?] [-h] [--help] show help\n"
1052 " jbmc\n"
1054 " jbmc\n"
1056 " jbmc\n"
1058 " jbmc\n"
1060 "\n"
1063 "\n"
1064 "Analysis options:\n"
1066 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
1067 " --property id only check one specific property\n"
1068 " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1069 " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1070 " (implies --trace)\n"
1072 "\n"
1073 "Program representations:\n"
1074 " --show-parse-tree show parse tree\n"
1075 " --show-symbol-table show loaded symbol table\n"
1076 " --list-symbols list symbols with type information\n"
1078 " --drop-unused-functions drop functions trivially unreachable\n"
1079 " from main function\n"
1081 "\n"
1082 "Program instrumentation options:\n"
1083 " --no-assertions ignore user assertions\n"
1084 " --no-assumptions ignore user assumptions\n"
1085 " --error-label label check that label is unreachable\n"
1086 " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1088 " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1089 "\n"
1090 "Java Bytecode frontend options:\n"
1092 // This one is handled by jbmc_parse_options not by the Java frontend,
1093 // hence its presence here:
1094 " --java-threading enable java multi-threading support (experimental)\n" // NOLINT(*)
1095 " --java-unwind-enum-static unwind loops in static initialization of enums\n" // NOLINT(*)
1096 // Currently only supported in the JBMC frontend:
1097 " --symex-driven-lazy-loading only load functions when first entered by symbolic\n" // NOLINT(*)
1098 " execution. Note that --show-symbol-table,\n"
1099 " --show-goto-functions/properties output\n"
1100 " will be restricted to loaded methods in this case,\n" // NOLINT(*)
1101 " and only output after the symex phase.\n"
1102 "\n"
1103 "Semantic transformations:\n"
1104 // NOLINTNEXTLINE(whitespace/line_length)
1105 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1106 "\n"
1107 "BMC options:\n"
1108 HELP_BMC
1109 "\n"
1110 "Backend options:\n"
1111 " --object-bits n number of bits used for object addresses\n"
1112 " --dimacs generate CNF in DIMACS format\n"
1113 " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1114 " --localize-faults localize faults (experimental)\n"
1115 " --smt1 use default SMT1 solver (obsolete)\n"
1116 " --smt2 use default SMT2 solver (Z3)\n"
1117 " --boolector use Boolector\n"
1118 " --mathsat use MathSAT\n"
1119 " --cvc4 use CVC4\n"
1120 " --yices use Yices\n"
1121 " --z3 use Z3\n"
1122 " --refine use refinement procedure (experimental)\n"
1124 " --outfile filename output formula to given file\n"
1125 " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1126 " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1127 "\n"
1128 "Other options:\n"
1129 " --version show version and exit\n"
1135 " --verbosity # verbosity level\n"
1137 "\n";
1138 // clang-format on
1139}
void add_failed_symbol_if_needed(const symbolt &symbol, symbol_table_baset &symbol_table)
Create a failed-dereference symbol for the given base symbol if it is pointer-typed,...
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 adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Symbolic Execution.
Goto Verifier for Verifying all Properties.
Goto verifier for verifying all properties that stores traces and localizes faults.
Goto verifier for verifying all properties that stores traces.
std::unique_ptr< languaget > new_ansi_c_language()
#define HELP_BMC
Definition: bmc_util.h:201
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
#define HELP_SHOW_CLASS_HIERARCHY
Abstract interface to eager or lazy GOTO models.
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert.
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
argst args
Definition: cmdline.h:145
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:109
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
std::string object_bits_info()
Definition: config.cpp:1339
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
const irep_idt & get_function_id()
Get function id.
Definition: goto_model.h:232
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition: goto_model.h:225
void compute_location_numbers()
Re-number our goto_function.
Definition: goto_model.h:209
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition: goto_model.h:218
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
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool is_nil() const
Definition: irep.h:376
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
bool show_loaded_functions(const abstract_goto_modelt &goto_model)
void get_command_line_options(optionst &)
bool can_generate_function_body(const irep_idt &name)
std::unique_ptr< class_hierarchyt > class_hierarchy
bool show_loaded_symbols(const abstract_goto_modelt &goto_model)
virtual int doit() override
invoke main modules
virtual void help() override
display command line help
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
java_object_factory_parameterst object_factory_params
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
optionalt< prefix_filtert > method_context
See java_bytecode_languaget::method_context.
int get_goto_program(std::unique_ptr< abstract_goto_modelt > &goto_model, const optionst &)
jbmc_parse_optionst(int argc, const char **argv)
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
static void set_default_options(optionst &)
Set the options that have default values.
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
const changesett & get_inserted() const
std::unordered_set< irep_idt > changesett
A GOTO model that produces function bodies on demand.
void load_all_functions() const
Eagerly loads all functions from the symbol table.
static std::unique_ptr< goto_modelt > process_whole_model_and_freeze(lazy_goto_modelt &&model)
The model returned here has access to the functions we've already loaded but is frozen in the sense t...
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.
static lazy_goto_modelt from_handler_object(THandler &handler, const optionst &options, message_handlert &message_handler)
Create a lazy_goto_modelt from a object that defines function/module pass handlers.
void initialize(const std::vector< std::string > &files, const optionst &options)
Performs initial symbol table and language_filest initialization from a given commandline and parsed ...
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
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 & debug() const
Definition: message.h:429
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition: message.cpp:139
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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
json_objectt to_json() const
Returns the options as JSON key value pairs.
Definition: options.cpp:93
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
xmlt to_xml() const
Returns the options in XML format.
Definition: options.cpp:104
virtual void usage_error()
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
Stops when the first failing property is found and localizes the fault Requires an incremental goto c...
Stops when the first failing property is found.
The symbol table base class interface.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
virtual uit get_ui() const
Definition: ui_message.h:33
configt config
Definition: config.cpp:25
void convert_nondet(const irep_idt &function_identifier, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &user_object_factory_parameters, const irep_idt &mode)
For each instruction in the goto program, checks if it is an assignment from nondet and replaces it w...
Convert side_effect_expr_nondett expressions using java_object_factory.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
Definition: exit_codes.h:49
#define CPROVER_EXIT_PARSE_ERROR
An error during parsing of the input program.
Definition: exit_codes.h:37
#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 goto_check_java(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_JAVA(cmdline, options)
Goto Programs with Functions.
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:285
#define HELP_GOTO_TRACE
Definition: goto_trace.h:277
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
std::unique_ptr< languaget > new_java_bytecode_language()
prefix_filtert get_context(const optionst &options)
#define HELP_JAVA_METHOD_NAME
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define HELP_JAVA_GOTO_BINARY
#define HELP_JAVA_CLASSPATH
#define HELP_JAVA_JAR
#define HELP_JAVA_CLASS_NAME
Goto Checker using Bounded Model Checking for Java.
Goto Checker using Bounded Model Checking for Java.
void parse_java_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the java object factory parameters from a given command line.
Goto Checker using Single Path Symbolic Execution for Java.
Goto Checker using Single Path Symbolic Execution for Java.
#define HELP_JAVA_TRACE_VALIDATION
JBMC Command Line Option Processing.
#define JBMC_OPTIONS
void json_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parses the JSON-formatted command line from stdin.
#define HELP_JSON_INTERFACE
Abstract interface to support a programming language.
Author: Diffblue Ltd.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
Loop IDs.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
Definition: mode.cpp:39
STL namespace.
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...
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)
void parse_path_strategy_options(const cmdlinet &cmdline, optionst &options, message_handlert &message_handler)
add paths and exploration-strategy option, suitable to be invoked from front-ends.
std::string show_path_strategies()
suitable for displaying as a front-end help message
Storage of symbolic execution paths to resume.
int result_to_exit_code(resultt result)
Definition: properties.cpp:143
resultt
The result of goto verifying.
Definition: properties.h:45
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
#define HELP_FUNCTIONS
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
Remove function exceptional returns.
void remove_instanceof(const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
Remove Instance-of Operators.
void remove_java_new(const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
Replace every java_new or java_new_array by a malloc side-effect and zero initialization.
Remove Java New Operators.
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,...
static void replace_java_nondet(goto_programt &goto_program)
Checks each instruction in the goto program to see whether it is a method returning nondet.
Replace Java Nondet expressions.
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
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)
Show the goto functions.
#define HELP_SHOW_GOTO_FUNCTIONS
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 java_generate_simple_method_stub(const irep_idt &function_name, symbol_table_baset &symbol_table, bool assume_non_null, const java_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
Java simple opaque stub generation.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define INITIALIZE_FUNCTION
Goto Verifier for stopping at the first failing property.
Goto Verifier for stopping at the first failing property and localizing the fault.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
#define HELP_STRING_REFINEMENT
irep_idt main_class
Definition: config.h:313
void set(const optionst &)
Assigns the parameters from given options.
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:108
#define HELP_VALIDATE
const char * CBMC_VERSION
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
#define HELP_XML_INTERFACE
Definition: xml_interface.h:39