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/unicode.h>
23 #include <util/version.h>
24 
25 #include <langapi/language.h>
26 
27 #include <ansi-c/ansi_c_language.h>
28 
34 #include <goto-programs/loop_ids.h>
44 
48 
50 
52 
53 #include <langapi/mode.h>
54 
63 
64 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
65  : parse_options_baset(JBMC_OPTIONS, argc, argv),
66  messaget(ui_message_handler),
67  ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION),
68  path_strategy_chooser()
69 {
70 }
71 
73  int argc,
74  const char **argv,
75  const std::string &extra_options)
76  : parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv),
77  messaget(ui_message_handler),
78  ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION),
79  path_strategy_chooser()
80 {
81 }
82 
84 {
85  // Default true
86  options.set_option("assertions", true);
87  options.set_option("assumptions", true);
88  options.set_option("built-in-assertions", true);
89  options.set_option("pretty-names", true);
90  options.set_option("propagation", true);
91  options.set_option("refine-strings", true);
92  options.set_option("sat-preprocessor", true);
93  options.set_option("simplify", true);
94  options.set_option("simplify-if", true);
95 
96  // Other default
97  options.set_option("arrays-uf", "auto");
98 }
99 
101 {
102  if(config.set(cmdline))
103  {
104  usage_error();
105  exit(1); // should contemplate EX_USAGE from sysexits.h
106  }
107 
109 
110  if(cmdline.isset("show-symex-strategies"))
111  {
112  std::cout << path_strategy_chooser.show_strategies();
113  exit(CPROVER_EXIT_SUCCESS);
114  }
115 
117 
118  if(cmdline.isset("program-only"))
119  options.set_option("program-only", true);
120 
121  if(cmdline.isset("show-vcc"))
122  options.set_option("show-vcc", true);
123 
124  if(cmdline.isset("cover"))
125  parse_cover_options(cmdline, options);
126 
127  if(cmdline.isset("no-simplify"))
128  options.set_option("simplify", false);
129 
130  if(cmdline.isset("stop-on-fail") ||
131  cmdline.isset("dimacs") ||
132  cmdline.isset("outfile"))
133  options.set_option("stop-on-fail", true);
134 
135  if(cmdline.isset("trace") ||
136  cmdline.isset("stop-on-fail"))
137  options.set_option("trace", true);
138 
139  if(cmdline.isset("localize-faults"))
140  options.set_option("localize-faults", true);
141  if(cmdline.isset("localize-faults-method"))
142  {
143  options.set_option(
144  "localize-faults-method",
145  cmdline.get_value("localize-faults-method"));
146  }
147 
148  if(cmdline.isset("unwind"))
149  options.set_option("unwind", cmdline.get_value("unwind"));
150 
151  if(cmdline.isset("depth"))
152  options.set_option("depth", cmdline.get_value("depth"));
153 
154  if(cmdline.isset("debug-level"))
155  options.set_option("debug-level", cmdline.get_value("debug-level"));
156 
157  if(cmdline.isset("slice-by-trace"))
158  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
159 
160  if(cmdline.isset("unwindset"))
161  options.set_option("unwindset", cmdline.get_value("unwindset"));
162 
163  // constant propagation
164  if(cmdline.isset("no-propagation"))
165  options.set_option("propagation", false);
166 
167  // transform self loops to assumptions
168  options.set_option(
169  "self-loops-to-assumptions",
170  !cmdline.isset("no-self-loops-to-assumptions"));
171 
172  // all checks supported by goto_check
174 
175  // unwind loops in java enum static initialization
176  if(cmdline.isset("java-unwind-enum-static"))
177  options.set_option("java-unwind-enum-static", true);
178 
179  // check assertions
180  if(cmdline.isset("no-assertions"))
181  options.set_option("assertions", false);
182 
183  // use assumptions
184  if(cmdline.isset("no-assumptions"))
185  options.set_option("assumptions", false);
186 
187  // generate unwinding assertions
188  if(cmdline.isset("cover"))
189  options.set_option("unwinding-assertions", false);
190  else
191  {
192  options.set_option(
193  "unwinding-assertions",
194  cmdline.isset("unwinding-assertions"));
195  }
196 
197  // generate unwinding assumptions otherwise
198  options.set_option(
199  "partial-loops",
200  cmdline.isset("partial-loops"));
201 
202  if(options.get_bool_option("partial-loops") &&
203  options.get_bool_option("unwinding-assertions"))
204  {
205  error() << "--partial-loops and --unwinding-assertions "
206  << "must not be given together" << eom;
207  exit(1); // should contemplate EX_USAGE from sysexits.h
208  }
209 
210  // remove unused equations
211  options.set_option(
212  "slice-formula",
213  cmdline.isset("slice-formula"));
214 
215  // simplify if conditions and branches
216  if(cmdline.isset("no-simplify-if"))
217  options.set_option("simplify-if", false);
218 
219  if(cmdline.isset("arrays-uf-always"))
220  options.set_option("arrays-uf", "always");
221  else if(cmdline.isset("arrays-uf-never"))
222  options.set_option("arrays-uf", "never");
223 
224  if(cmdline.isset("dimacs"))
225  options.set_option("dimacs", true);
226 
227  if(cmdline.isset("refine-arrays"))
228  {
229  options.set_option("refine", true);
230  options.set_option("refine-arrays", true);
231  }
232 
233  if(cmdline.isset("refine-arithmetic"))
234  {
235  options.set_option("refine", true);
236  options.set_option("refine-arithmetic", true);
237  }
238 
239  if(cmdline.isset("refine"))
240  {
241  options.set_option("refine", true);
242  options.set_option("refine-arrays", true);
243  options.set_option("refine-arithmetic", true);
244  }
245 
246  if(cmdline.isset("no-refine-strings"))
247  options.set_option("refine-strings", false);
248 
249  if(cmdline.isset("string-printable"))
250  options.set_option("string-printable", true);
251 
252  if(cmdline.isset("no-refine-strings") && cmdline.isset("string-printable"))
253  {
254  warning() << "--string-printable ignored due to --no-refine-strings" << eom;
255  }
256 
257  if(
258  cmdline.isset("no-refine-strings") &&
259  cmdline.isset("max-nondet-string-length"))
260  {
261  warning() << "--max-nondet-string-length ignored due to "
262  << "--no-refine-strings" << eom;
263  }
264 
265  if(cmdline.isset("max-node-refinement"))
266  options.set_option(
267  "max-node-refinement",
268  cmdline.get_value("max-node-refinement"));
269 
270  // SMT Options
271 
272  if(cmdline.isset("smt1"))
273  {
274  error() << "--smt1 is no longer supported" << eom;
276  }
277 
278  if(cmdline.isset("smt2"))
279  options.set_option("smt2", true);
280 
281  if(cmdline.isset("fpa"))
282  options.set_option("fpa", true);
283 
284  bool solver_set=false;
285 
286  if(cmdline.isset("boolector"))
287  {
288  options.set_option("boolector", true), solver_set=true;
289  options.set_option("smt2", true);
290  }
291 
292  if(cmdline.isset("mathsat"))
293  {
294  options.set_option("mathsat", true), solver_set=true;
295  options.set_option("smt2", true);
296  }
297 
298  if(cmdline.isset("cvc4"))
299  {
300  options.set_option("cvc4", true), solver_set=true;
301  options.set_option("smt2", true);
302  }
303 
304  if(cmdline.isset("yices"))
305  {
306  options.set_option("yices", true), solver_set=true;
307  options.set_option("smt2", true);
308  }
309 
310  if(cmdline.isset("z3"))
311  {
312  options.set_option("z3", true), solver_set=true;
313  options.set_option("smt2", true);
314  }
315 
316  if(cmdline.isset("smt2") && !solver_set)
317  {
318  if(cmdline.isset("outfile"))
319  {
320  // outfile and no solver should give standard compliant SMT-LIB
321  options.set_option("generic", true);
322  }
323  else
324  {
325  // the default smt2 solver
326  options.set_option("z3", true);
327  }
328  }
329 
330  if(cmdline.isset("beautify"))
331  options.set_option("beautify", true);
332 
333  if(cmdline.isset("no-sat-preprocessor"))
334  options.set_option("sat-preprocessor", false);
335 
336  options.set_option(
337  "pretty-names",
338  !cmdline.isset("no-pretty-names"));
339 
340  if(cmdline.isset("outfile"))
341  options.set_option("outfile", cmdline.get_value("outfile"));
342 
343  if(cmdline.isset("graphml-witness"))
344  {
345  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
346  options.set_option("stop-on-fail", true);
347  options.set_option("trace", true);
348  }
349 
350  if(cmdline.isset("symex-coverage-report"))
351  options.set_option(
352  "symex-coverage-report",
353  cmdline.get_value("symex-coverage-report"));
354 
356 
357  if(cmdline.isset("symex-driven-lazy-loading"))
358  {
359  options.set_option("symex-driven-lazy-loading", true);
360  for(const char *opt :
361  { "nondet-static",
362  "full-slice",
363  "lazy-methods",
364  "reachability-slice",
365  "reachability-slice-fb" })
366  {
367  if(cmdline.isset(opt))
368  {
369  throw std::string("Option ") + opt +
370  " can't be used with --symex-driven-lazy-loading";
371  }
372  }
373  }
374 
375  // The 'allow-pointer-unsoundness' option prevents symex from throwing an
376  // exception when it encounters pointers that are shared across threads.
377  // This is unsound but given that pointers are ubiquitous in java this check
378  // must be disabled in order to support the analysis of multithreaded java
379  // code.
380  if(cmdline.isset("java-threading"))
381  options.set_option("allow-pointer-unsoundness", true);
382 }
383 
386 {
387  if(cmdline.isset("version"))
388  {
389  std::cout << CBMC_VERSION << '\n';
390  return 0; // should contemplate EX_OK from sysexits.h
391  }
392 
393  //
394  // command line options
395  //
396 
397  optionst options;
398  try
399  {
400  get_command_line_options(options);
401  }
402 
403  catch(const char *error_msg)
404  {
405  error() << error_msg << eom;
406  return 6; // should contemplate EX_SOFTWARE from sysexits.h
407  }
408 
409  catch(const std::string &error_msg)
410  {
411  error() << error_msg << eom;
412  return 6; // should contemplate EX_SOFTWARE from sysexits.h
413  }
414 
417 
418  //
419  // Print a banner
420  //
421  status() << "JBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
422  << "-bit " << config.this_architecture() << " "
424 
427 
428  if(cmdline.isset("show-parse-tree"))
429  {
430  if(cmdline.args.size()!=1)
431  {
432  error() << "Please give exactly one source file" << eom;
433  return 6;
434  }
435 
436  std::string filename=cmdline.args[0];
437 
438  #ifdef _MSC_VER
439  std::ifstream infile(widen(filename));
440  #else
441  std::ifstream infile(filename);
442  #endif
443 
444  if(!infile)
445  {
446  error() << "failed to open input file `"
447  << filename << "'" << eom;
448  return 6;
449  }
450 
451  std::unique_ptr<languaget> language=
452  get_language_from_filename(filename);
453 
454  if(language==nullptr)
455  {
456  error() << "failed to figure out type of file `"
457  << filename << "'" << eom;
458  return 6;
459  }
460 
461  language->get_language_options(cmdline);
463 
464  status() << "Parsing " << filename << eom;
465 
466  if(language->parse(infile, filename))
467  {
468  error() << "PARSING ERROR" << eom;
469  return 6;
470  }
471 
472  language->show_parse(std::cout);
473  return 0;
474  }
475 
476  std::function<void(bmct &, const symbol_tablet &)> configure_bmc = nullptr;
477  if(options.get_bool_option("java-unwind-enum-static"))
478  {
479  configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) {
481  [&symbol_table](
482  const goto_symex_statet::call_stackt &context,
483  unsigned loop_number,
484  unsigned unwind,
485  unsigned &max_unwind) {
487  context, loop_number, unwind, max_unwind, symbol_table);
488  });
489  };
490  }
491 
493  cmdline.isset("java-max-input-array-length")
494  ? std::stoul(cmdline.get_value("java-max-input-array-length"))
497  cmdline.isset("max-nondet-string-length")
498  ? std::stoul(cmdline.get_value("max-nondet-string-length"))
499  : cmdline.isset("string-max-input-length") // obsolete; will go away
500  ? std::stoul(cmdline.get_value("string-max-input-length"))
503  cmdline.isset("java-max-input-tree-depth")
504  ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
506 
507  stub_objects_are_not_null = cmdline.isset("java-assume-inputs-non-null");
508 
509  if(!cmdline.isset("symex-driven-lazy-loading"))
510  {
511  std::unique_ptr<goto_modelt> goto_model_ptr;
512  int get_goto_program_ret=get_goto_program(goto_model_ptr, options);
513  if(get_goto_program_ret!=-1)
514  return get_goto_program_ret;
515 
516  goto_modelt &goto_model = *goto_model_ptr;
517 
518  if(cmdline.isset("show-properties"))
519  {
522  return 0; // should contemplate EX_OK from sysexits.h
523  }
524 
525  if(set_properties(goto_model))
526  return 7; // should contemplate EX_USAGE from sysexits.h
527 
528  // The `configure_bmc` callback passed will enable enum-unwind-static if
529  // applicable.
532  options,
533  goto_model,
535  *this,
536  configure_bmc);
537  }
538  else
539  {
540  // Use symex-driven lazy loading:
542  *this, options, get_message_handler());
543  lazy_goto_model.initialize(cmdline);
544 
545  // The precise wording of this error matches goto-symex's complaint when no
546  // __CPROVER_start exists (if we just go ahead and run it anyway it will
547  // trip an invariant when it tries to load it)
549  {
550  error() << "the program has no entry point";
551  return 6;
552  }
553 
554  // Add failed symbols for any symbol created prior to loading any
555  // particular function:
556  add_failed_symbols(lazy_goto_model.symbol_table);
557 
558  // If applicable, parse the coverage instrumentation configuration, which
559  // will be used in process_goto_function:
560  cover_config =
562  options, lazy_goto_model.symbol_table, get_message_handler());
563 
564  // Provide show-goto-functions and similar dump functions after symex
565  // executes. If --paths is active, these dump routines run after every
566  // paths iteration. Its return value indicates that if we ran any dump
567  // function, then we should skip the actual solver phase.
568  auto callback_after_symex = [this, &lazy_goto_model]() {
569  return show_loaded_functions(lazy_goto_model);
570  };
571 
572  // The `configure_bmc` callback passed will enable enum-unwind-static if
573  // applicable.
574  return
577  options,
578  lazy_goto_model,
580  *this,
581  configure_bmc,
582  callback_after_symex);
583  }
584 }
585 
587 {
588  try
589  {
590  if(cmdline.isset("property"))
591  ::set_properties(goto_model, cmdline.get_values("property"));
592  }
593 
594  catch(const char *e)
595  {
596  error() << e << eom;
597  return true;
598  }
599 
600  catch(const std::string &e)
601  {
602  error() << e << eom;
603  return true;
604  }
605 
606  catch(int)
607  {
608  return true;
609  }
610 
611  return false;
612 }
613 
615  std::unique_ptr<goto_modelt> &goto_model,
616  const optionst &options)
617 {
618  if(cmdline.args.empty())
619  {
620  error() << "Please provide a program to verify" << eom;
621  return 6;
622  }
623 
624  try
625  {
627  *this, options, get_message_handler());
628  lazy_goto_model.initialize(cmdline);
629 
630  // Show the class hierarchy
631  if(cmdline.isset("show-class-hierarchy"))
632  {
633  class_hierarchyt hierarchy;
634  hierarchy(lazy_goto_model.symbol_table);
637  return CPROVER_EXIT_SUCCESS;
638  }
639 
640  // Add failed symbols for any symbol created prior to loading any
641  // particular function:
642  add_failed_symbols(lazy_goto_model.symbol_table);
643 
644  status() << "Generating GOTO Program" << messaget::eom;
645  lazy_goto_model.load_all_functions();
646 
647  // Show the symbol table before process_goto_functions mangles return
648  // values, etc
649  if(cmdline.isset("show-symbol-table"))
650  {
652  lazy_goto_model.symbol_table, ui_message_handler.get_ui());
653  return 0;
654  }
655 
656  // Move the model out of the local lazy_goto_model
657  // and into the caller's goto_model
659  std::move(lazy_goto_model));
660  if(goto_model == nullptr)
661  return 6;
662 
663  // show it?
664  if(cmdline.isset("show-loops"))
665  {
666  show_loop_ids(ui_message_handler.get_ui(), *goto_model);
667  return 0;
668  }
669 
670  // show it?
671  if(
672  cmdline.isset("show-goto-functions") ||
673  cmdline.isset("list-goto-functions"))
674  {
676  *goto_model,
679  cmdline.isset("list-goto-functions"));
680  return 0;
681  }
682 
683  status() << config.object_bits_info() << eom;
684  }
685 
686  catch(const char *e)
687  {
688  error() << e << eom;
689  return 6;
690  }
691 
692  catch(const std::string &e)
693  {
694  error() << e << eom;
695  return 6;
696  }
697 
698  catch(int)
699  {
700  return 6;
701  }
702 
703  catch(const std::bad_alloc &)
704  {
705  error() << "Out of memory" << eom;
706  return 6;
707  }
708 
709  return -1; // no error, continue
710 }
711 
713  goto_model_functiont &function,
714  const abstract_goto_modelt &model,
715  const optionst &options)
716 {
717  journalling_symbol_tablet &symbol_table = function.get_symbol_table();
718  namespacet ns(symbol_table);
719  goto_functionst::goto_functiont &goto_function = function.get_goto_function();
720 
721  bool using_symex_driven_loading =
722  options.get_bool_option("symex-driven-lazy-loading");
723 
724  try
725  {
726  // Removal of RTTI inspection:
727  remove_instanceof(goto_function, symbol_table, get_message_handler());
728  // Java virtual functions -> explicit dispatch tables:
729  remove_virtual_functions(function);
730 
731  if(using_symex_driven_loading)
732  {
733  // remove exceptions
734  // If using symex-driven function loading we need to do this now so that
735  // symex doesn't have to cope with exception-handling constructs; however
736  // the results are slightly worse than running it in whole-program mode
737  // (e.g. dead catch sites will be retained)
739  goto_function.body,
740  symbol_table,
743  }
744 
745  auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
746  return symbol_table.lookup_ref(id).value.is_nil() &&
747  !model.can_produce_function(id);
748  };
749 
750  remove_returns(function, function_is_stub);
751 
752  replace_java_nondet(function);
753 
754  // Similar removal of java nondet statements:
756  function,
759  ID_java);
760 
761  // add generic checks
762  goto_check(ns, options, ID_java, function.get_goto_function());
763 
764  // Replace Java new side effects
765  remove_java_new(goto_function, symbol_table, get_message_handler());
766 
767  // checks don't know about adjusted float expressions
768  adjust_float_expressions(goto_function, ns);
769 
770  // add failed symbols for anything created relating to this particular
771  // function (note this means subseqent passes mustn't create more!):
772  journalling_symbol_tablet::changesett new_symbols =
773  symbol_table.get_inserted();
774  for(const irep_idt &new_symbol_name : new_symbols)
775  {
777  symbol_table.lookup_ref(new_symbol_name),
778  symbol_table);
779  }
780 
781  // If using symex-driven function loading we must insert the coverage goals
782  // now so symex sees its targets; otherwise we leave this until
783  // process_goto_functions, as we haven't run remove_exceptions yet, and that
784  // pass alters the CFG.
785  if(using_symex_driven_loading)
786  {
787  // instrument cover goals
788  if(cmdline.isset("cover"))
789  {
790  INVARIANT(
791  cover_config != nullptr, "cover config should have been parsed");
793  }
794 
795  // label the assertions
796  label_properties(goto_function.body);
797 
798  goto_function.body.update();
799  function.compute_location_numbers();
800  goto_function.body.compute_loop_numbers();
801  }
802 
803  // update the function member in each instruction
804  function.update_instructions_function();
805  }
806 
807  catch(const char *e)
808  {
809  error() << e << eom;
810  throw;
811  }
812 
813  catch(const std::string &e)
814  {
815  error() << e << eom;
816  throw;
817  }
818 
819  catch(const std::bad_alloc &)
820  {
821  error() << "Out of memory" << eom;
822  throw;
823  }
824 }
825 
827  const abstract_goto_modelt &goto_model)
828 {
829  if(cmdline.isset("show-symbol-table"))
830  {
832  goto_model.get_symbol_table(), ui_message_handler.get_ui());
833  return true;
834  }
835 
836  if(cmdline.isset("show-loops"))
837  {
839  return true;
840  }
841 
842  if(
843  cmdline.isset("show-goto-functions") ||
844  cmdline.isset("list-goto-functions"))
845  {
846  namespacet ns(goto_model.get_symbol_table());
848  ns,
851  goto_model.get_goto_functions(),
852  cmdline.isset("list-goto-functions"));
853  return true;
854  }
855 
856  if(cmdline.isset("show-properties"))
857  {
858  namespacet ns(goto_model.get_symbol_table());
860  ns,
863  goto_model.get_goto_functions());
864  return true;
865  }
866 
867  return false;
868 }
869 
871  goto_modelt &goto_model,
872  const optionst &options)
873 {
874  try
875  {
876  status() << "Running GOTO functions transformation passes" << eom;
877 
878  bool using_symex_driven_loading =
879  options.get_bool_option("symex-driven-lazy-loading");
880 
881  // When using symex-driven lazy loading, *all* relevant processing is done
882  // during process_goto_function, so we have nothing to do here.
883  if(using_symex_driven_loading)
884  return false;
885 
886  // remove catch and throw
887  // (introduces instanceof but request it is removed)
889  goto_model,
892 
893  // instrument library preconditions
894  instrument_preconditions(goto_model);
895 
896  // ignore default/user-specified initialization
897  // of variables with static lifetime
898  if(cmdline.isset("nondet-static"))
899  {
900  status() << "Adding nondeterministic initialization "
901  "of static/global variables" << eom;
902  nondet_static(goto_model);
903  }
904 
905  // recalculate numbers, etc.
906  goto_model.goto_functions.update();
907 
908  if(cmdline.isset("drop-unused-functions"))
909  {
910  // Entry point will have been set before and function pointers removed
911  status() << "Removing unused functions" << eom;
913  }
914 
915  // remove skips such that trivial GOTOs are deleted and not considered
916  // for coverage annotation:
917  remove_skip(goto_model);
918 
919  // instrument cover goals
920  if(cmdline.isset("cover"))
921  {
922  if(instrument_cover_goals(options, goto_model, get_message_handler()))
923  return true;
924  }
925 
926  // label the assertions
927  // This must be done after adding assertions and
928  // before using the argument of the "property" option.
929  // Do not re-label after using the property slicer because
930  // this would cause the property identifiers to change.
931  label_properties(goto_model);
932 
933  // reachability slice?
934  if(cmdline.isset("reachability-slice-fb"))
935  {
936  if(cmdline.isset("reachability-slice"))
937  {
938  error() << "--reachability-slice and --reachability-slice-fb "
939  << "must not be given together" << eom;
940  return true;
941  }
942 
943  status() << "Performing a forwards-backwards reachability slice" << eom;
944  if(cmdline.isset("property"))
945  reachability_slicer(goto_model, cmdline.get_values("property"), true);
946  else
947  reachability_slicer(goto_model, true);
948  }
949 
950  if(cmdline.isset("reachability-slice"))
951  {
952  status() << "Performing a reachability slice" << eom;
953  if(cmdline.isset("property"))
954  reachability_slicer(goto_model, cmdline.get_values("property"));
955  else
956  reachability_slicer(goto_model);
957  }
958 
959  // full slice?
960  if(cmdline.isset("full-slice"))
961  {
962  status() << "Performing a full slice" << eom;
963  if(cmdline.isset("property"))
964  property_slicer(goto_model, cmdline.get_values("property"));
965  else
966  full_slicer(goto_model);
967  }
968 
969  // remove any skips introduced since coverage instrumentation
970  remove_skip(goto_model);
971  }
972 
973  catch(const char *e)
974  {
975  error() << e << eom;
976  return true;
977  }
978 
979  catch(const std::string &e)
980  {
981  error() << e << eom;
982  return true;
983  }
984 
985  catch(int)
986  {
987  return true;
988  }
989 
990  catch(const std::bad_alloc &)
991  {
992  error() << "Out of memory" << eom;
993  return true;
994  }
995 
996  return false;
997 }
998 
1000 {
1001  static const irep_idt initialize_id = INITIALIZE_FUNCTION;
1002 
1003  return name != goto_functionst::entry_point() && name != initialize_id;
1004 }
1005 
1007  const irep_idt &function_name,
1008  symbol_table_baset &symbol_table,
1009  goto_functiont &function,
1010  bool body_available)
1011 {
1012  // Provide a simple stub implementation for any function we don't have a
1013  // bytecode implementation for:
1014 
1015  if(body_available)
1016  return false;
1017 
1018  if(!can_generate_function_body(function_name))
1019  return false;
1020 
1021  if(symbol_table.lookup_ref(function_name).mode == ID_java)
1022  {
1024  function_name,
1025  symbol_table,
1029 
1030  goto_convert_functionst converter(symbol_table, get_message_handler());
1031  converter.convert_function(function_name, function);
1032 
1033  return true;
1034  }
1035  else
1036  {
1037  return false;
1038  }
1039 }
1040 
1043 {
1044  // clang-format off
1045  std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
1046  <<
1047  "* * Copyright (C) 2001-2018 * *\n"
1048  "* * Daniel Kroening, Edmund Clarke * *\n"
1049  "* * Carnegie Mellon University, Computer Science Department * *\n"
1050  "* * kroening@kroening.com * *\n"
1051  "\n"
1052  "Usage: Purpose:\n"
1053  "\n"
1054  " jbmc [-?] [-h] [--help] show help\n"
1055  " jbmc class name of class to be checked\n"
1056  "\n"
1057  "Analysis options:\n"
1059  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
1060  " --property id only check one specific property\n"
1061  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1062  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1063  "\n"
1065  "\n"
1066  "Program representations:\n"
1067  " --show-parse-tree show parse tree\n"
1068  " --show-symbol-table show loaded symbol table\n"
1070  " --drop-unused-functions drop functions trivially unreachable\n"
1071  " from main function\n"
1073  "\n"
1074  "Program instrumentation options:\n"
1075  " --no-assertions ignore user assertions\n"
1076  " --no-assumptions ignore user assumptions\n"
1077  " --error-label label check that label is unreachable\n"
1078  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
1079  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1081  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1082  "\n"
1083  "Java Bytecode frontend options:\n"
1084  " --classpath dir/jar set the classpath\n"
1085  " --main-class class-name set the name of the main class\n"
1087  // This one is handled by jbmc_parse_options not by the Java frontend,
1088  // hence its presence here:
1089  " --java-threading enable java multi-threading support (experimental)\n" // NOLINT(*)
1090  " --java-unwind-enum-static unwind loops in static initialization of enums\n" // NOLINT(*)
1091  // Currently only supported in the JBMC frontend:
1092  " --symex-driven-lazy-loading only load functions when first entered by symbolic\n" // NOLINT(*)
1093  " execution. Note that --show-symbol-table,\n"
1094  " --show-goto-functions/properties output\n"
1095  " will be restricted to loaded methods in this case,\n" // NOLINT(*)
1096  " and only output after the symex phase.\n"
1097  "\n"
1098  "BMC options:\n"
1099  HELP_BMC
1100  "\n"
1101  "Backend options:\n"
1102  " --object-bits n number of bits used for object addresses\n"
1103  " --dimacs generate CNF in DIMACS format\n"
1104  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1105  " --localize-faults localize faults (experimental)\n"
1106  " --smt1 use default SMT1 solver (obsolete)\n"
1107  " --smt2 use default SMT2 solver (Z3)\n"
1108  " --boolector use Boolector\n"
1109  " --mathsat use MathSAT\n"
1110  " --cvc4 use CVC4\n"
1111  " --yices use Yices\n"
1112  " --z3 use Z3\n"
1113  " --refine use refinement procedure (experimental)\n"
1114  " --no-refine-strings turn off string refinement\n"
1115  " --string-printable restrict to printable strings (experimental)\n" // NOLINT(*)
1116  " --max-nondet-string-length bound the length of nondet (e.g. input) strings\n" // NOLINT(*)
1117  " --outfile filename output formula to given file\n"
1118  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1119  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1120  "\n"
1121  "Other options:\n"
1122  " --version show version and exit\n"
1123  " --xml-ui use XML-formatted output\n"
1124  " --json-ui use JSON-formatted output\n"
1126  HELP_FLUSH
1127  " --verbosity # verbosity level\n"
1129  "\n";
1130  // clang-format on
1131 }
Remove Java New Operators.
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
Symbolic Execution.
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
jbmc_parse_optionst(int argc, const char **argv)
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
Abstract interface to eager or lazy GOTO models.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Remove function exceptional returns.
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Remove Instance-of Operators.
std::wstring widen(const char *s)
Definition: unicode.cpp:46
Remove Virtual Function (Method) Calls.
Non-graph-based representation of the class hierarchy.
irep_idt mode
Language mode.
Definition: symbol.h:52
uit get_ui() const
Definition: ui_message.h:37
virtual void get_language_options(const cmdlinet &)
Definition: language.h:43
std::string object_bits_info()
Definition: config.cpp:1203
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.
Show the symbol table.
Show the goto functions.
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:78
static void set_default_options(optionst &)
Set the options that have default values.
#define HELP_SHOW_CLASS_HIERARCHY
#define JBMC_OPTIONS
Java simple opaque stub generation.
std::string get_value(char option) const
Definition: cmdline.cpp:45
void java_generate_simple_method_stub(const irep_idt &function_name, symbol_table_baset &symbol_table, bool assume_non_null, const object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
object_factory_parameterst object_factory_params
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Definition: mode.cpp:101
STL namespace.
JBMC Command Line Option Processing.
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
Pointer Dereferencing.
Model that holds partially loaded map of functions.
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
std::unique_ptr< cover_configt > cover_config
configt config
Definition: config.cpp:23
Remove &#39;asm&#39; statements by compiling into suitable standard code.
void remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
#define HELP_FUNCTIONS
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
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, an lvalue, and doesn&#39;t already have one.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
static int do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, const ui_message_handlert::uit &ui, messaget &message, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr)
Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand)...
Definition: bmc.cpp:559
path_strategy_choosert path_strategy_chooser
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:163
Set the properties to check.
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
mstreamt & warning() const
Definition: message.h:307
Unused function removal.
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:258
bool set(const cmdlinet &cmdline)
Definition: config.cpp:738
void add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler)
Definition: bmc.h:115
#define HELP_TIMESTAMP
Definition: timestamper.h:14
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert::uit ui)
argst args
Definition: cmdline.h:37
std::string show_strategies() const
suitable for displaying as a front-end help message
virtual bool isset(char option) const
Definition: cmdline.cpp:27
void set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const
add paths and exploration-strategy option, suitable to be invoked from front-ends.
bool can_generate_function_body(const irep_idt &name)
size_t max_nondet_tree_depth
Maximum depth for object hierarchy on input.
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler, remove_exceptions_typest type)
removes throws/CATCH-POP/CATCH-PUSH
#define HELP_SHOW_PROPERTIES
#define MAX_NONDET_ARRAY_LENGTH_DEFAULT
#define INITIALIZE_FUNCTION
Nondeterministic initialization of certain global scope variables.
#define HELP_FLUSH
Definition: ui_message.h:108
void initialize(const cmdlinet &cmdline)
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:302
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Function Inlining.
#define HELP_BMC
Definition: bmc.h:315
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&#39;ve already loaded but is frozen in the sense t...
::goto_functiont goto_functiont
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
Abstract interface to support a programming language.
Loop IDs.
Convert side_effect_expr_nondett expressions.
std::unique_ptr< languaget > new_java_bytecode_language()
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
Remove function returns.
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
virtual int doit() override
invoke main modules
Replace Java Nondet expressions.
std::string banner_string(const std::string &front_end, const std::string &version)
void instrument_cover_goals(goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler)
Applies instrumenters to given goto program.
Definition: cover.cpp:33
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:56
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
virtual void help() override
display command line help
void load_all_functions() const
Eagerly loads all functions from the symbol table.
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
Author: Diffblue Ltd.
int get_goto_program(std::unique_ptr< goto_modelt > &goto_model, const optionst &)
virtual void show_parse(std::ostream &out)=0
bool show_loaded_functions(const abstract_goto_modelt &goto_model)
std::vector< framet > call_stackt
static irep_idt this_operating_system()
Definition: config.cpp:1310
message_handlert & get_message_handler()
Definition: message.h:153
void convert_nondet(goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const object_factory_parameterst &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...
size_t max_nondet_array_length
Maximum value for the non-deterministically-chosen length of an array.
Goto Programs with Functions.
static irep_idt entry_point()
#define HELP_GOTO_TRACE
Definition: goto_trace.h:252
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & status() const
Definition: message.h:317
bool set_properties(goto_modelt &goto_model)
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
Definition: version.cpp:1
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...
size_t max_nondet_string_length
Maximum value for the non-deterministically-chosen length of a string.
The symbol table base class interface.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
void show_class_hierarchy(const class_hierarchyt &hierarchy, message_handlert &message_handler, ui_message_handlert::uit ui, bool children_only)
Output the class hierarchy.
Slicing.
void remove_java_new(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.
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
std::unique_ptr< languaget > new_ansi_c_language()
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
Unwind loops in static initializers.
ui_message_handlert ui_message_handler
void get_command_line_options(optionst &)
virtual void usage_error()
Show the properties.
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
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...
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
#define MAX_NONDET_TREE_DEPTH
virtual bool parse(std::istream &instream, const std::string &path)=0
Program Transformation.
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:28
#define MAX_NONDET_STRING_LENGTH
void label_properties(goto_modelt &goto_model)
tvt java_enum_static_init_unwind_handler(const goto_symex_statet::call_stackt &context, unsigned loop_number, unsigned unwind_count, unsigned &unwind_max, const symbol_tablet &symbol_table)
Unwind handler that special-cases the clinit (static initializer) functions of enumeration classes...
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
std::unique_ptr< cover_configt > get_cover_config(const optionst &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Build data structures controlling coverage from command-line options.
Definition: cover.cpp:187
static irep_idt this_architecture()
Definition: config.cpp:1213
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)