cprover
jbmc_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JBMC Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "jbmc_parse_options.h"
13 
14 #include <fstream>
15 #include <cstdlib> // exit()
16 #include <iostream>
17 #include <memory>
18 
19 #include <util/config.h>
20 #include <util/exit_codes.h>
21 #include <util/invariant.h>
22 #include <util/make_unique.h>
23 #include <util/unicode.h>
24 #include <util/version.h>
25 #include <util/xml.h>
26 
27 #include <langapi/language.h>
28 
29 #include <ansi-c/ansi_c_language.h>
30 
36 
41 #include <goto-programs/loop_ids.h>
50 
54 
56 
58 
60 
61 #include <langapi/mode.h>
62 
76 
77 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
80  argc,
81  argv,
82  std::string("JBMC ") + CBMC_VERSION)
83 {
86 }
87 
89  int argc,
90  const char **argv,
91  const std::string &extra_options)
93  JBMC_OPTIONS + extra_options,
94  argc,
95  argv,
96  std::string("JBMC ") + CBMC_VERSION)
97 {
100 }
101 
103 {
104  // Default true
105  options.set_option("assertions", true);
106  options.set_option("assumptions", true);
107  options.set_option("built-in-assertions", true);
108  options.set_option("lazy-methods", true);
109  options.set_option("pretty-names", true);
110  options.set_option("propagation", true);
111  options.set_option("refine-strings", true);
112  options.set_option("sat-preprocessor", true);
113  options.set_option("simple-slice", true);
114  options.set_option("simplify", true);
115  options.set_option("simplify-if", true);
116  options.set_option("show-goto-symex-steps", false);
117 
118  // Other default
119  options.set_option("arrays-uf", "auto");
120 }
121 
123 {
124  if(config.set(cmdline))
125  {
126  usage_error();
127  exit(1); // should contemplate EX_USAGE from sysexits.h
128  }
129 
131 
132  if(cmdline.isset("function"))
133  options.set_option("function", cmdline.get_value("function"));
134 
137 
138  if(cmdline.isset("max-field-sensitivity-array-size"))
139  {
140  options.set_option(
141  "max-field-sensitivity-array-size",
142  cmdline.get_value("max-field-sensitivity-array-size"));
143  }
144 
145  if(cmdline.isset("no-array-field-sensitivity"))
146  {
147  if(cmdline.isset("max-field-sensitivity-array-size"))
148  {
149  log.error()
150  << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
151  << " must not be given together" << messaget::eom;
153  }
154  options.set_option("no-array-field-sensitivity", true);
155  }
156 
157  if(cmdline.isset("show-symex-strategies"))
158  {
160  exit(CPROVER_EXIT_SUCCESS);
161  }
162 
164 
165  if(cmdline.isset("program-only"))
166  options.set_option("program-only", true);
167 
168  if(cmdline.isset("show-vcc"))
169  options.set_option("show-vcc", true);
170 
171  if(cmdline.isset("nondet-static"))
172  options.set_option("nondet-static", true);
173 
174  if(cmdline.isset("no-simplify"))
175  options.set_option("simplify", false);
176 
177  if(cmdline.isset("stop-on-fail") ||
178  cmdline.isset("dimacs") ||
179  cmdline.isset("outfile"))
180  options.set_option("stop-on-fail", true);
181 
182  if(
183  cmdline.isset("trace") || cmdline.isset("compact-trace") ||
184  cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
186  !cmdline.isset("cover")))
187  {
188  options.set_option("trace", true);
189  }
190 
191  if(cmdline.isset("validate-trace"))
192  {
193  options.set_option("validate-trace", true);
194  options.set_option("trace", true);
195  }
196 
197  if(cmdline.isset("localize-faults"))
198  options.set_option("localize-faults", true);
199 
200  if(cmdline.isset("symex-complexity-limit"))
201  {
202  options.set_option(
203  "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
204  }
205 
206  if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
207  {
208  options.set_option(
209  "symex-complexity-failed-child-loops-limit",
210  cmdline.get_value("symex-complexity-failed-child-loops-limit"));
211  }
212 
213  if(cmdline.isset("unwind"))
214  options.set_option("unwind", cmdline.get_value("unwind"));
215 
216  if(cmdline.isset("depth"))
217  options.set_option("depth", cmdline.get_value("depth"));
218 
219  if(cmdline.isset("debug-level"))
220  options.set_option("debug-level", cmdline.get_value("debug-level"));
221 
222  if(cmdline.isset("unwindset"))
223  options.set_option("unwindset", cmdline.get_value("unwindset"));
224 
225  // constant propagation
226  if(cmdline.isset("no-propagation"))
227  options.set_option("propagation", false);
228 
229  // transform self loops to assumptions
230  options.set_option(
231  "self-loops-to-assumptions",
232  !cmdline.isset("no-self-loops-to-assumptions"));
233 
234  // all checks supported by goto_check
236 
237  // unwind loops in java enum static initialization
238  if(cmdline.isset("java-unwind-enum-static"))
239  options.set_option("java-unwind-enum-static", true);
240 
241  // check assertions
242  if(cmdline.isset("no-assertions"))
243  options.set_option("assertions", false);
244 
245  // use assumptions
246  if(cmdline.isset("no-assumptions"))
247  options.set_option("assumptions", false);
248 
249  // generate unwinding assertions
250  if(cmdline.isset("unwinding-assertions"))
251  options.set_option("unwinding-assertions", true);
252 
253  // generate unwinding assumptions otherwise
254  options.set_option(
255  "partial-loops",
256  cmdline.isset("partial-loops"));
257 
258  if(options.get_bool_option("partial-loops") &&
259  options.get_bool_option("unwinding-assertions"))
260  {
261  log.error() << "--partial-loops and --unwinding-assertions "
262  << "must not be given together" << messaget::eom;
263  exit(1); // should contemplate EX_USAGE from sysexits.h
264  }
265 
266  // remove unused equations
267  options.set_option(
268  "slice-formula",
269  cmdline.isset("slice-formula"));
270 
271  // simplify if conditions and branches
272  if(cmdline.isset("no-simplify-if"))
273  options.set_option("simplify-if", false);
274 
275  if(cmdline.isset("arrays-uf-always"))
276  options.set_option("arrays-uf", "always");
277  else if(cmdline.isset("arrays-uf-never"))
278  options.set_option("arrays-uf", "never");
279 
280  if(cmdline.isset("dimacs"))
281  options.set_option("dimacs", true);
282 
283  if(cmdline.isset("refine-arrays"))
284  {
285  options.set_option("refine", true);
286  options.set_option("refine-arrays", true);
287  }
288 
289  if(cmdline.isset("refine-arithmetic"))
290  {
291  options.set_option("refine", true);
292  options.set_option("refine-arithmetic", true);
293  }
294 
295  if(cmdline.isset("refine"))
296  {
297  options.set_option("refine", true);
298  options.set_option("refine-arrays", true);
299  options.set_option("refine-arithmetic", true);
300  }
301 
302  if(cmdline.isset("no-refine-strings"))
303  options.set_option("refine-strings", false);
304 
305  if(cmdline.isset("string-printable") && cmdline.isset("no-refine-strings"))
306  {
308  "cannot use --string-printable with --no-refine-strings",
309  "--string-printable");
310  }
311 
312  if(cmdline.isset("string-input-value") && cmdline.isset("no-refine-strings"))
313  {
315  "cannot use --string-input-value with --no-refine-strings",
316  "--string-input-value");
317  }
318 
319  if(
320  cmdline.isset("no-refine-strings") &&
321  cmdline.isset("max-nondet-string-length"))
322  {
324  "cannot use --max-nondet-string-length with --no-refine-strings",
325  "--max-nondet-string-length");
326  }
327 
328  if(cmdline.isset("max-node-refinement"))
329  options.set_option(
330  "max-node-refinement",
331  cmdline.get_value("max-node-refinement"));
332 
333  // SMT Options
334 
335  if(cmdline.isset("smt1"))
336  {
337  log.error() << "--smt1 is no longer supported" << messaget::eom;
339  }
340 
341  if(cmdline.isset("smt2"))
342  options.set_option("smt2", true);
343 
344  if(cmdline.isset("fpa"))
345  options.set_option("fpa", true);
346 
347  bool solver_set=false;
348 
349  if(cmdline.isset("boolector"))
350  {
351  options.set_option("boolector", true), solver_set=true;
352  options.set_option("smt2", true);
353  }
354 
355  if(cmdline.isset("mathsat"))
356  {
357  options.set_option("mathsat", true), solver_set=true;
358  options.set_option("smt2", true);
359  }
360 
361  if(cmdline.isset("cvc4"))
362  {
363  options.set_option("cvc4", true), solver_set=true;
364  options.set_option("smt2", true);
365  }
366 
367  if(cmdline.isset("yices"))
368  {
369  options.set_option("yices", true), solver_set=true;
370  options.set_option("smt2", true);
371  }
372 
373  if(cmdline.isset("z3"))
374  {
375  options.set_option("z3", true), solver_set=true;
376  options.set_option("smt2", true);
377  }
378 
379  if(cmdline.isset("smt2") && !solver_set)
380  {
381  if(cmdline.isset("outfile"))
382  {
383  // outfile and no solver should give standard compliant SMT-LIB
384  options.set_option("generic", true);
385  }
386  else
387  {
388  // the default smt2 solver
389  options.set_option("z3", true);
390  }
391  }
392 
393  if(cmdline.isset("beautify"))
394  options.set_option("beautify", true);
395 
396  if(cmdline.isset("no-sat-preprocessor"))
397  options.set_option("sat-preprocessor", false);
398 
399  options.set_option(
400  "pretty-names",
401  !cmdline.isset("no-pretty-names"));
402 
403  if(cmdline.isset("outfile"))
404  options.set_option("outfile", cmdline.get_value("outfile"));
405 
406  if(cmdline.isset("graphml-witness"))
407  {
408  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
409  options.set_option("stop-on-fail", true);
410  options.set_option("trace", true);
411  }
412 
413  if(cmdline.isset("symex-coverage-report"))
414  options.set_option(
415  "symex-coverage-report",
416  cmdline.get_value("symex-coverage-report"));
417 
418  if(cmdline.isset("validate-ssa-equation"))
419  {
420  options.set_option("validate-ssa-equation", true);
421  }
422 
423  if(cmdline.isset("validate-goto-model"))
424  {
425  options.set_option("validate-goto-model", true);
426  }
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';
468  return CPROVER_EXIT_SUCCESS;
469  }
470 
473 
474  //
475  // command line options
476  //
477 
478  optionst options;
479  get_command_line_options(options);
480 
481  //
482  // Print a banner
483  //
484  log.status() << "JBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
485  << "-bit " << config.this_architecture() << " "
487 
488  // output the options
489  switch(ui_message_handler.get_ui())
490  {
493  log.debug(), [&options](messaget::mstreamt &debug_stream) {
494  debug_stream << "\nOptions: \n";
495  options.output(debug_stream);
496  debug_stream << messaget::eom;
497  });
498  break;
500  {
501  json_objectt json_options{{"options", options.to_json()}};
502  log.debug() << json_options;
503  break;
504  }
506  log.debug() << options.to_xml();
507  break;
508  }
509 
512 
513  if(!((cmdline.isset("jar") && cmdline.args.empty()) ||
514  (cmdline.isset("gb") && cmdline.args.empty()) ||
515  (!cmdline.isset("jar") && !cmdline.isset("gb") &&
516  (cmdline.args.size() == 1))))
517  {
518  log.error() << "Please give exactly one class name, "
519  << "and/or use -jar jarfile or --gb goto-binary"
520  << messaget::eom;
522  }
523 
524  if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree"))
525  {
526  std::string main_class = cmdline.args[0];
527  // `java` accepts slashes and dots as package separators
528  std::replace(main_class.begin(), main_class.end(), '/', '.');
529  config.java.main_class = main_class;
530  cmdline.args.pop_back();
531  }
532 
533  if(cmdline.isset("jar"))
534  {
535  cmdline.args.push_back(cmdline.get_value("jar"));
536  }
537 
538  if(cmdline.isset("gb"))
539  {
540  cmdline.args.push_back(cmdline.get_value("gb"));
541  }
542 
543  // Shows the parse tree of the main class
544  if(cmdline.isset("show-parse-tree"))
545  {
546  std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
547  CHECK_RETURN(language != nullptr);
548  language->set_language_options(options);
549  language->set_message_handler(ui_message_handler);
550 
551  log.status() << "Parsing ..." << messaget::eom;
552 
553  if(static_cast<java_bytecode_languaget *>(language.get())->parse())
554  {
555  log.error() << "PARSING ERROR" << messaget::eom;
557  }
558 
559  language->show_parse(std::cout);
560  return CPROVER_EXIT_SUCCESS;
561  }
562 
563  object_factory_params.set(options);
564 
566  options.get_bool_option("java-assume-inputs-non-null");
567 
568  std::unique_ptr<abstract_goto_modelt> goto_model_ptr;
569  int get_goto_program_ret = get_goto_program(goto_model_ptr, options);
570  if(get_goto_program_ret != -1)
571  return get_goto_program_ret;
572 
573  if(
574  options.get_bool_option("program-only") ||
575  options.get_bool_option("show-vcc") ||
576  (options.get_bool_option("symex-driven-lazy-loading") &&
577  (cmdline.isset("show-symbol-table") || cmdline.isset("list-symbols") ||
578  cmdline.isset("show-goto-functions") ||
579  cmdline.isset("list-goto-functions") ||
580  cmdline.isset("show-properties") || cmdline.isset("show-loops"))))
581  {
582  if(options.get_bool_option("paths"))
583  {
585  options, ui_message_handler, *goto_model_ptr);
586  (void)verifier();
587  }
588  else
589  {
591  options, ui_message_handler, *goto_model_ptr);
592  (void)verifier();
593  }
594 
595  if(options.get_bool_option("symex-driven-lazy-loading"))
596  {
597  // We can only output these after goto-symex has run.
598  (void)show_loaded_symbols(*goto_model_ptr);
599  (void)show_loaded_functions(*goto_model_ptr);
600  }
601 
602  return CPROVER_EXIT_SUCCESS;
603  }
604 
605  if(
606  options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
607  {
608  if(options.get_bool_option("paths"))
609  {
611  options, ui_message_handler, *goto_model_ptr);
612  (void)verifier();
613  }
614  else
615  {
617  options, ui_message_handler, *goto_model_ptr);
618  (void)verifier();
619  }
620 
621  return CPROVER_EXIT_SUCCESS;
622  }
623 
624  std::unique_ptr<goto_verifiert> verifier = nullptr;
625 
626  if(
627  options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
628  {
629  verifier =
630  util_make_unique<stop_on_fail_verifiert<java_single_path_symex_checkert>>(
631  options, ui_message_handler, *goto_model_ptr);
632  }
633  else if(
634  options.get_bool_option("stop-on-fail") &&
635  !options.get_bool_option("paths"))
636  {
637  if(options.get_bool_option("localize-faults"))
638  {
639  verifier =
642  options, ui_message_handler, *goto_model_ptr);
643  }
644  else
645  {
646  verifier = util_make_unique<
648  options, ui_message_handler, *goto_model_ptr);
649  }
650  }
651  else if(
652  !options.get_bool_option("stop-on-fail") &&
653  options.get_bool_option("paths"))
654  {
657  options, ui_message_handler, *goto_model_ptr);
658  }
659  else if(
660  !options.get_bool_option("stop-on-fail") &&
661  !options.get_bool_option("paths"))
662  {
663  if(options.get_bool_option("localize-faults"))
664  {
665  verifier =
668  options, ui_message_handler, *goto_model_ptr);
669  }
670  else
671  {
674  options, ui_message_handler, *goto_model_ptr);
675  }
676  }
677  else
678  {
679  UNREACHABLE;
680  }
681 
682  const resultt result = (*verifier)();
683  verifier->report();
684  return result_to_exit_code(result);
685 }
686 
688  std::unique_ptr<abstract_goto_modelt> &goto_model_ptr,
689  const optionst &options)
690 {
691  if(options.is_set("context-include") || options.is_set("context-exclude"))
692  method_context = get_context(options);
693  lazy_goto_modelt lazy_goto_model =
695  lazy_goto_model.initialize(cmdline.args, options);
696 
698  util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
699 
700  // Show the class hierarchy
701  if(cmdline.isset("show-class-hierarchy"))
702  {
704  return CPROVER_EXIT_SUCCESS;
705  }
706 
707  // Add failed symbols for any symbol created prior to loading any
708  // particular function:
709  add_failed_symbols(lazy_goto_model.symbol_table);
710 
711  if(!options.get_bool_option("symex-driven-lazy-loading"))
712  {
713  log.status() << "Generating GOTO Program" << messaget::eom;
714  lazy_goto_model.load_all_functions();
715 
716  // show symbol table or list symbols
717  if(show_loaded_symbols(lazy_goto_model))
718  return CPROVER_EXIT_SUCCESS;
719 
720  // Move the model out of the local lazy_goto_model
721  // and into the caller's goto_model
723  std::move(lazy_goto_model));
724  if(goto_model_ptr == nullptr)
726 
727  goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
728 
729  // if we added the ansi-c library models here this should also call
730  // add_malloc_may_fail_variable_initializations(goto_model);
731  // here
732 
733  if(cmdline.isset("validate-goto-model"))
734  {
735  goto_model.validate();
736  }
737 
738  if(show_loaded_functions(goto_model))
739  return CPROVER_EXIT_SUCCESS;
740 
741  if(cmdline.isset("property"))
742  ::set_properties(goto_model, cmdline.get_values("property"));
743  }
744  else
745  {
746  // The precise wording of this error matches goto-symex's complaint when no
747  // __CPROVER_start exists (if we just go ahead and run it anyway it will
748  // trip an invariant when it tries to load it)
750  {
751  log.error() << "the program has no entry point" << messaget::eom;
753  }
754 
755  if(cmdline.isset("validate-goto-model"))
756  {
757  lazy_goto_model.validate();
758  }
759 
760  goto_model_ptr =
761  util_make_unique<lazy_goto_modelt>(std::move(lazy_goto_model));
762  }
763 
765 
766  return -1; // no error, continue
767 }
768 
770  goto_model_functiont &function,
771  const abstract_goto_modelt &model,
772  const optionst &options)
773 {
774  journalling_symbol_tablet &symbol_table = function.get_symbol_table();
775  namespacet ns(symbol_table);
776  goto_functionst::goto_functiont &goto_function = function.get_goto_function();
777 
778  bool using_symex_driven_loading =
779  options.get_bool_option("symex-driven-lazy-loading");
780 
781  // Removal of RTTI inspection:
783  function.get_function_id(),
784  goto_function,
785  symbol_table,
788  // Java virtual functions -> explicit dispatch tables:
790 
791  auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
792  return symbol_table.lookup_ref(id).value.is_nil() &&
793  !model.can_produce_function(id);
794  };
795 
796  remove_returns(function, function_is_stub);
797 
798  replace_java_nondet(function);
799 
800  // Similar removal of java nondet statements:
802 
803  if(using_symex_driven_loading)
804  {
805  // remove exceptions
806  // If using symex-driven function loading we need to do this now so that
807  // symex doesn't have to cope with exception-handling constructs; however
808  // the results are slightly worse than running it in whole-program mode
809  // (e.g. dead catch sites will be retained)
811  function.get_function_id(),
812  goto_function.body,
813  symbol_table,
814  *class_hierarchy.get(),
816  }
817 
818  // add generic checks
819  goto_check(
820  function.get_function_id(), function.get_goto_function(), ns, options);
821 
822  // Replace Java new side effects
824  function.get_function_id(),
825  goto_function,
826  symbol_table,
828 
829  // checks don't know about adjusted float expressions
830  adjust_float_expressions(goto_function, ns);
831 
832  // add failed symbols for anything created relating to this particular
833  // function (note this means subsequent passes mustn't create more!):
835  symbol_table.get_inserted();
836  for(const irep_idt &new_symbol_name : new_symbols)
837  {
839  symbol_table.lookup_ref(new_symbol_name), symbol_table);
840  }
841 
842  // If using symex-driven function loading we must label the assertions
843  // now so symex sees its targets; otherwise we leave this until
844  // process_goto_functions, as we haven't run remove_exceptions yet, and that
845  // pass alters the CFG.
846  if(using_symex_driven_loading)
847  {
848  // label the assertions
849  label_properties(goto_function.body);
850 
851  goto_function.body.update();
852  function.compute_location_numbers();
853  goto_function.body.compute_loop_numbers();
854  }
855 }
856 
858  const abstract_goto_modelt &goto_model)
859 {
860  if(cmdline.isset("show-symbol-table"))
861  {
863  return true;
864  }
865  else if(cmdline.isset("list-symbols"))
866  {
868  return true;
869  }
870 
871  return false;
872 }
873 
875  const abstract_goto_modelt &goto_model)
876 {
877  if(cmdline.isset("show-loops"))
878  {
880  return true;
881  }
882 
883  if(
884  cmdline.isset("show-goto-functions") ||
885  cmdline.isset("list-goto-functions"))
886  {
887  namespacet ns(goto_model.get_symbol_table());
889  ns,
891  goto_model.get_goto_functions(),
892  cmdline.isset("list-goto-functions"));
893  return true;
894  }
895 
896  if(cmdline.isset("show-properties"))
897  {
898  namespacet ns(goto_model.get_symbol_table());
900  return true;
901  }
902 
903  return false;
904 }
905 
907  goto_modelt &goto_model,
908  const optionst &options)
909 {
910  log.status() << "Running GOTO functions transformation passes"
911  << messaget::eom;
912 
913  bool using_symex_driven_loading =
914  options.get_bool_option("symex-driven-lazy-loading");
915 
916  // When using symex-driven lazy loading, *all* relevant processing is done
917  // during process_goto_function, so we have nothing to do here.
918  if(using_symex_driven_loading)
919  return false;
920 
921  // remove catch and throw
923 
924  // instrument library preconditions
925  instrument_preconditions(goto_model);
926 
927  // ignore default/user-specified initialization
928  // of variables with static lifetime
929  if(cmdline.isset("nondet-static"))
930  {
931  log.status() << "Adding nondeterministic initialization "
932  "of static/global variables"
933  << messaget::eom;
934  nondet_static(goto_model);
935  }
936 
937  // recalculate numbers, etc.
938  goto_model.goto_functions.update();
939 
940  if(cmdline.isset("drop-unused-functions"))
941  {
942  // Entry point will have been set before and function pointers removed
943  log.status() << "Removing unused functions" << messaget::eom;
945  }
946 
947  // remove skips such that trivial GOTOs are deleted
948  remove_skip(goto_model);
949 
950  // label the assertions
951  // This must be done after adding assertions and
952  // before using the argument of the "property" option.
953  // Do not re-label after using the property slicer because
954  // this would cause the property identifiers to change.
955  label_properties(goto_model);
956 
957  // reachability slice?
958  if(cmdline.isset("reachability-slice-fb"))
959  {
960  if(cmdline.isset("reachability-slice"))
961  {
962  log.error() << "--reachability-slice and --reachability-slice-fb "
963  << "must not be given together" << messaget::eom;
964  return true;
965  }
966 
967  log.status() << "Performing a forwards-backwards reachability slice"
968  << messaget::eom;
969  if(cmdline.isset("property"))
970  reachability_slicer(goto_model, cmdline.get_values("property"), true);
971  else
972  reachability_slicer(goto_model, true);
973  }
974 
975  if(cmdline.isset("reachability-slice"))
976  {
977  log.status() << "Performing a reachability slice" << messaget::eom;
978  if(cmdline.isset("property"))
979  reachability_slicer(goto_model, cmdline.get_values("property"));
980  else
981  reachability_slicer(goto_model);
982  }
983 
984  // full slice?
985  if(cmdline.isset("full-slice"))
986  {
987  log.status() << "Performing a full slice" << messaget::eom;
988  if(cmdline.isset("property"))
989  property_slicer(goto_model, cmdline.get_values("property"));
990  else
991  full_slicer(goto_model);
992  }
993 
994  // remove any skips introduced
995  remove_skip(goto_model);
996 
997  return false;
998 }
999 
1001 {
1002  static const irep_idt initialize_id = INITIALIZE_FUNCTION;
1003 
1004  return name != goto_functionst::entry_point() && name != initialize_id;
1005 }
1006 
1008  const irep_idt &function_name,
1009  symbol_table_baset &symbol_table,
1010  goto_functiont &function,
1011  bool body_available)
1012 {
1013  // Provide a simple stub implementation for any function we don't have a
1014  // bytecode implementation for:
1015 
1016  if(
1017  body_available &&
1018  (!method_context || (*method_context)(id2string(function_name))))
1019  return false;
1020 
1021  if(!can_generate_function_body(function_name))
1022  return false;
1023 
1024  if(symbol_table.lookup_ref(function_name).mode == ID_java)
1025  {
1027  function_name,
1028  symbol_table,
1032 
1033  goto_convert_functionst converter(symbol_table, ui_message_handler);
1034  converter.convert_function(function_name, function);
1035 
1036  return true;
1037  }
1038  else
1039  {
1040  return false;
1041  }
1042 }
1043 
1046 {
1047  // clang-format off
1048  std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
1049  << align_center_with_border("Copyright (C) 2001-2018") << '\n'
1050  << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
1051  << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
1052  << align_center_with_border("kroening@kroening.com") << '\n'
1053  << "\n"
1054  "Usage: Purpose:\n"
1055  "\n"
1056  " jbmc [-?] [-h] [--help] show help\n"
1057  " jbmc\n"
1059  " jbmc\n"
1061  " jbmc\n"
1063  " jbmc\n"
1065  "\n"
1068  "\n"
1069  "Analysis options:\n"
1071  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
1072  " --property id only check one specific property\n"
1073  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1074  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1075  " (implies --trace)\n"
1077  "\n"
1078  "Program representations:\n"
1079  " --show-parse-tree show parse tree\n"
1080  " --show-symbol-table show loaded symbol table\n"
1081  " --list-symbols list symbols with type information\n"
1083  " --drop-unused-functions drop functions trivially unreachable\n"
1084  " from main function\n"
1086  "\n"
1087  "Program instrumentation options:\n"
1088  " --no-assertions ignore user assertions\n"
1089  " --no-assumptions ignore user assumptions\n"
1090  " --error-label label check that label is unreachable\n"
1091  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1093  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1094  "\n"
1095  "Java Bytecode frontend options:\n"
1097  // This one is handled by jbmc_parse_options not by the Java frontend,
1098  // hence its presence here:
1099  " --java-threading enable java multi-threading support (experimental)\n" // NOLINT(*)
1100  " --java-unwind-enum-static unwind loops in static initialization of enums\n" // NOLINT(*)
1101  // Currently only supported in the JBMC frontend:
1102  " --symex-driven-lazy-loading only load functions when first entered by symbolic\n" // NOLINT(*)
1103  " execution. Note that --show-symbol-table,\n"
1104  " --show-goto-functions/properties output\n"
1105  " will be restricted to loaded methods in this case,\n" // NOLINT(*)
1106  " and only output after the symex phase.\n"
1107  "\n"
1108  "Semantic transformations:\n"
1109  // NOLINTNEXTLINE(whitespace/line_length)
1110  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1111  "\n"
1112  "BMC options:\n"
1113  HELP_BMC
1114  "\n"
1115  "Backend options:\n"
1116  " --object-bits n number of bits used for object addresses\n"
1117  " --dimacs generate CNF in DIMACS format\n"
1118  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1119  " --localize-faults localize faults (experimental)\n"
1120  " --smt1 use default SMT1 solver (obsolete)\n"
1121  " --smt2 use default SMT2 solver (Z3)\n"
1122  " --boolector use Boolector\n"
1123  " --mathsat use MathSAT\n"
1124  " --cvc4 use CVC4\n"
1125  " --yices use Yices\n"
1126  " --z3 use Z3\n"
1127  " --refine use refinement procedure (experimental)\n"
1129  " --outfile filename output formula to given file\n"
1130  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1131  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1132  "\n"
1133  "Other options:\n"
1134  " --version show version and exit\n"
1139  HELP_FLUSH
1140  " --verbosity # verbosity level\n"
1142  "\n";
1143  // clang-format on
1144 }
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:202
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:47
virtual bool isset(char option) const
Definition: cmdline.cpp:29
argst args
Definition: cmdline.h:143
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
std::string object_bits_info()
Definition: config.cpp:1315
static irep_idt this_architecture()
Definition: config.cpp:1326
struct configt::javat java
static irep_idt this_operating_system()
Definition: config.cpp:1426
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:27
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
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:387
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...
virtual const symbol_tablet & get_symbol_table() const override
std::unordered_set< irep_idt > changesett
const changesett & get_inserted() const
A GOTO model that produces function bodies on demand.
void load_all_functions() const
Eagerly loads all functions from the symbol table.
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 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...
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:104
mstreamt & error() const
Definition: message.h:399
mstreamt & status() const
Definition: message.h:414
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:138
mstreamt & debug() const
Definition: message.h:429
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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
void output(std::ostream &out) const
Outputs the options to out
Definition: options.cpp:121
virtual void usage_error()
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
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.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
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:31
configt config
Definition: config.cpp:24
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(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:71
Goto Programs with Functions.
Function Inlining.
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:287
#define HELP_GOTO_TRACE
Definition: goto_trace.h:279
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
prefix_filtert get_context(const optionst &options)
std::unique_ptr< languaget > new_java_bytecode_language()
#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
Unwind loops in static initializers.
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:19
Loop IDs.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
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:38
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
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:140
resultt
The result of goto verifying.
Definition: properties.h:44
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:85
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:496
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
#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:248
void set(const optionst &)
Assigns the parameters from given options.
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:106
#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