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/xml.h>
24 #include <util/version.h>
25 
26 #include <langapi/language.h>
27 
28 #include <ansi-c/ansi_c_language.h>
29 
35 #include <goto-programs/loop_ids.h>
45 
49 
51 
53 
54 #include <langapi/mode.h>
55 
64 
65 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
66  : parse_options_baset(JBMC_OPTIONS, argc, argv),
67  messaget(ui_message_handler),
68  ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION),
69  path_strategy_chooser()
70 {
71 }
72 
74  int argc,
75  const char **argv,
76  const std::string &extra_options)
77  : parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv),
78  messaget(ui_message_handler),
79  ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION),
80  path_strategy_chooser()
81 {
82 }
83 
85 {
86  // Default true
87  options.set_option("assertions", true);
88  options.set_option("assumptions", true);
89  options.set_option("built-in-assertions", true);
90  options.set_option("lazy-methods", true);
91  options.set_option("pretty-names", true);
92  options.set_option("propagation", true);
93  options.set_option("refine-strings", true);
94  options.set_option("sat-preprocessor", true);
95  options.set_option("simplify", true);
96  options.set_option("simplify-if", true);
97 
98  // Other default
99  options.set_option("arrays-uf", "auto");
100 }
101 
103 {
104  if(config.set(cmdline))
105  {
106  usage_error();
107  exit(1); // should contemplate EX_USAGE from sysexits.h
108  }
109 
111 
112  if(cmdline.isset("function"))
113  options.set_option("function", cmdline.get_value("function"));
114 
117 
118  if(cmdline.isset("show-symex-strategies"))
119  {
120  std::cout << path_strategy_chooser.show_strategies();
121  exit(CPROVER_EXIT_SUCCESS);
122  }
123 
125 
126  if(cmdline.isset("program-only"))
127  options.set_option("program-only", true);
128 
129  if(cmdline.isset("show-vcc"))
130  options.set_option("show-vcc", true);
131 
132  if(cmdline.isset("nondet-static"))
133  options.set_option("nondet-static", true);
134 
135  if(cmdline.isset("no-simplify"))
136  options.set_option("simplify", false);
137 
138  if(cmdline.isset("stop-on-fail") ||
139  cmdline.isset("dimacs") ||
140  cmdline.isset("outfile"))
141  options.set_option("stop-on-fail", true);
142 
143  if(
144  cmdline.isset("trace") || cmdline.isset("stack-trace") ||
145  cmdline.isset("stop-on-fail"))
146  options.set_option("trace", true);
147 
148  if(cmdline.isset("localize-faults"))
149  options.set_option("localize-faults", true);
150  if(cmdline.isset("localize-faults-method"))
151  {
152  options.set_option(
153  "localize-faults-method",
154  cmdline.get_value("localize-faults-method"));
155  }
156 
157  if(cmdline.isset("unwind"))
158  options.set_option("unwind", cmdline.get_value("unwind"));
159 
160  if(cmdline.isset("depth"))
161  options.set_option("depth", cmdline.get_value("depth"));
162 
163  if(cmdline.isset("debug-level"))
164  options.set_option("debug-level", cmdline.get_value("debug-level"));
165 
166  if(cmdline.isset("slice-by-trace"))
167  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
168 
169  if(cmdline.isset("unwindset"))
170  options.set_option("unwindset", cmdline.get_value("unwindset"));
171 
172  // constant propagation
173  if(cmdline.isset("no-propagation"))
174  options.set_option("propagation", false);
175 
176  // transform self loops to assumptions
177  options.set_option(
178  "self-loops-to-assumptions",
179  !cmdline.isset("no-self-loops-to-assumptions"));
180 
181  // all checks supported by goto_check
183 
184  // unwind loops in java enum static initialization
185  if(cmdline.isset("java-unwind-enum-static"))
186  options.set_option("java-unwind-enum-static", true);
187 
188  // check assertions
189  if(cmdline.isset("no-assertions"))
190  options.set_option("assertions", false);
191 
192  // use assumptions
193  if(cmdline.isset("no-assumptions"))
194  options.set_option("assumptions", false);
195 
196  // generate unwinding assertions
197  if(cmdline.isset("unwinding-assertions"))
198  options.set_option("unwinding-assertions", true);
199 
200  // generate unwinding assumptions otherwise
201  options.set_option(
202  "partial-loops",
203  cmdline.isset("partial-loops"));
204 
205  if(options.get_bool_option("partial-loops") &&
206  options.get_bool_option("unwinding-assertions"))
207  {
208  error() << "--partial-loops and --unwinding-assertions "
209  << "must not be given together" << eom;
210  exit(1); // should contemplate EX_USAGE from sysexits.h
211  }
212 
213  // remove unused equations
214  options.set_option(
215  "slice-formula",
216  cmdline.isset("slice-formula"));
217 
218  // simplify if conditions and branches
219  if(cmdline.isset("no-simplify-if"))
220  options.set_option("simplify-if", false);
221 
222  if(cmdline.isset("arrays-uf-always"))
223  options.set_option("arrays-uf", "always");
224  else if(cmdline.isset("arrays-uf-never"))
225  options.set_option("arrays-uf", "never");
226 
227  if(cmdline.isset("dimacs"))
228  options.set_option("dimacs", true);
229 
230  if(cmdline.isset("refine-arrays"))
231  {
232  options.set_option("refine", true);
233  options.set_option("refine-arrays", true);
234  }
235 
236  if(cmdline.isset("refine-arithmetic"))
237  {
238  options.set_option("refine", true);
239  options.set_option("refine-arithmetic", true);
240  }
241 
242  if(cmdline.isset("refine"))
243  {
244  options.set_option("refine", true);
245  options.set_option("refine-arrays", true);
246  options.set_option("refine-arithmetic", true);
247  }
248 
249  if(cmdline.isset("no-refine-strings"))
250  options.set_option("refine-strings", false);
251 
252  if(cmdline.isset("string-printable"))
253  {
254  if(cmdline.isset("no-refine-strings"))
255  {
256  warning() << "--string-printable ignored due to --no-refine-strings"
257  << eom;
258  }
259  options.set_option("string-printable", true);
260  }
261 
262  if(cmdline.isset("string-input-value"))
263  {
264  if(cmdline.isset("no-refine-strings"))
265  {
266  warning() << "--string-input-value ignored due to --no-refine-strings"
267  << eom;
268  }
269  options.set_option(
270  "string-input-value",
271  cmdline.get_values("string-input-value"));
272  }
273 
274  if(
275  cmdline.isset("no-refine-strings") &&
276  cmdline.isset("max-nondet-string-length"))
277  {
278  warning() << "--max-nondet-string-length ignored due to "
279  << "--no-refine-strings" << eom;
280  }
281 
282  if(cmdline.isset("max-node-refinement"))
283  options.set_option(
284  "max-node-refinement",
285  cmdline.get_value("max-node-refinement"));
286 
287  // SMT Options
288 
289  if(cmdline.isset("smt1"))
290  {
291  error() << "--smt1 is no longer supported" << eom;
293  }
294 
295  if(cmdline.isset("smt2"))
296  options.set_option("smt2", true);
297 
298  if(cmdline.isset("fpa"))
299  options.set_option("fpa", true);
300 
301  bool solver_set=false;
302 
303  if(cmdline.isset("boolector"))
304  {
305  options.set_option("boolector", true), solver_set=true;
306  options.set_option("smt2", true);
307  }
308 
309  if(cmdline.isset("mathsat"))
310  {
311  options.set_option("mathsat", true), solver_set=true;
312  options.set_option("smt2", true);
313  }
314 
315  if(cmdline.isset("cvc4"))
316  {
317  options.set_option("cvc4", true), solver_set=true;
318  options.set_option("smt2", true);
319  }
320 
321  if(cmdline.isset("yices"))
322  {
323  options.set_option("yices", true), solver_set=true;
324  options.set_option("smt2", true);
325  }
326 
327  if(cmdline.isset("z3"))
328  {
329  options.set_option("z3", true), solver_set=true;
330  options.set_option("smt2", true);
331  }
332 
333  if(cmdline.isset("smt2") && !solver_set)
334  {
335  if(cmdline.isset("outfile"))
336  {
337  // outfile and no solver should give standard compliant SMT-LIB
338  options.set_option("generic", true);
339  }
340  else
341  {
342  // the default smt2 solver
343  options.set_option("z3", true);
344  }
345  }
346 
347  if(cmdline.isset("beautify"))
348  options.set_option("beautify", true);
349 
350  if(cmdline.isset("no-sat-preprocessor"))
351  options.set_option("sat-preprocessor", false);
352 
353  options.set_option(
354  "pretty-names",
355  !cmdline.isset("no-pretty-names"));
356 
357  if(cmdline.isset("outfile"))
358  options.set_option("outfile", cmdline.get_value("outfile"));
359 
360  if(cmdline.isset("graphml-witness"))
361  {
362  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
363  options.set_option("stop-on-fail", true);
364  options.set_option("trace", true);
365  }
366 
367  if(cmdline.isset("symex-coverage-report"))
368  options.set_option(
369  "symex-coverage-report",
370  cmdline.get_value("symex-coverage-report"));
371 
373 
374  if(cmdline.isset("no-lazy-methods"))
375  options.set_option("lazy-methods", false);
376 
377  if(cmdline.isset("symex-driven-lazy-loading"))
378  {
379  options.set_option("symex-driven-lazy-loading", true);
380  for(const char *opt :
381  { "nondet-static",
382  "full-slice",
383  "reachability-slice",
384  "reachability-slice-fb" })
385  {
386  if(cmdline.isset(opt))
387  {
388  throw std::string("Option ") + opt +
389  " can't be used with --symex-driven-lazy-loading";
390  }
391  }
392  }
393 
394  // The 'allow-pointer-unsoundness' option prevents symex from throwing an
395  // exception when it encounters pointers that are shared across threads.
396  // This is unsound but given that pointers are ubiquitous in java this check
397  // must be disabled in order to support the analysis of multithreaded java
398  // code.
399  if(cmdline.isset("java-threading"))
400  options.set_option("allow-pointer-unsoundness", true);
401 }
402 
405 {
406  if(cmdline.isset("version"))
407  {
408  std::cout << CBMC_VERSION << '\n';
409  return 0; // should contemplate EX_OK from sysexits.h
410  }
411 
414 
415  //
416  // command line options
417  //
418 
419  optionst options;
420  try
421  {
422  get_command_line_options(options);
423  }
424 
425  catch(const char *error_msg)
426  {
427  error() << error_msg << eom;
428  return 6; // should contemplate EX_SOFTWARE from sysexits.h
429  }
430 
431  catch(const std::string &error_msg)
432  {
433  error() << error_msg << eom;
434  return 6; // should contemplate EX_SOFTWARE from sysexits.h
435  }
436 
437  //
438  // Print a banner
439  //
440  status() << "JBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
441  << "-bit " << config.this_architecture() << " "
443 
444  // output the options
445  switch(ui_message_handler.get_ui())
446  {
449  mstream << "\nOptions: \n";
450  options.output(mstream);
452  });
453  break;
455  {
456  json_objectt json_options;
457  json_options["options"] = options.to_json();
458  debug() << json_options;
459  break;
460  }
462  debug() << options.to_xml();
463  break;
464  }
465 
468 
469  if(cmdline.isset("show-parse-tree"))
470  {
471  if(cmdline.args.size()!=1)
472  {
473  error() << "Please give exactly one source file" << eom;
474  return 6;
475  }
476 
477  std::string filename=cmdline.args[0];
478 
479  #ifdef _MSC_VER
480  std::ifstream infile(widen(filename));
481  #else
482  std::ifstream infile(filename);
483  #endif
484 
485  if(!infile)
486  {
487  error() << "failed to open input file `"
488  << filename << "'" << eom;
489  return 6;
490  }
491 
492  std::unique_ptr<languaget> language=
493  get_language_from_filename(filename);
494 
495  if(language==nullptr)
496  {
497  error() << "failed to figure out type of file `"
498  << filename << "'" << eom;
499  return 6;
500  }
501 
502  language->set_language_options(options);
504 
505  status() << "Parsing " << filename << eom;
506 
507  if(language->parse(infile, filename))
508  {
509  error() << "PARSING ERROR" << eom;
510  return 6;
511  }
512 
513  language->show_parse(std::cout);
514  return 0;
515  }
516 
517  std::function<void(bmct &, const symbol_tablet &)> configure_bmc = nullptr;
518  if(options.get_bool_option("java-unwind-enum-static"))
519  {
520  configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) {
522  [&symbol_table](
523  const goto_symex_statet::call_stackt &context,
524  unsigned loop_number,
525  unsigned unwind,
526  unsigned &max_unwind) {
528  context, loop_number, unwind, max_unwind, symbol_table);
529  });
530  };
531  }
532 
533  object_factory_params.set(options);
534 
536  options.get_bool_option("java-assume-inputs-non-null");
537 
538  if(!cmdline.isset("symex-driven-lazy-loading"))
539  {
540  std::unique_ptr<goto_modelt> goto_model_ptr;
541  int get_goto_program_ret=get_goto_program(goto_model_ptr, options);
542  if(get_goto_program_ret!=-1)
543  return get_goto_program_ret;
544 
545  goto_modelt &goto_model = *goto_model_ptr;
546 
547  if(cmdline.isset("show-properties"))
548  {
551  return 0; // should contemplate EX_OK from sysexits.h
552  }
553 
554  if(set_properties(goto_model))
555  return 7; // should contemplate EX_USAGE from sysexits.h
556 
557  // The `configure_bmc` callback passed will enable enum-unwind-static if
558  // applicable.
561  options,
562  goto_model,
564  configure_bmc);
565  }
566  else
567  {
568  // Use symex-driven lazy loading:
570  *this, options, get_message_handler());
571  lazy_goto_model.initialize(cmdline.args, options);
572 
574  util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
575 
576  // The precise wording of this error matches goto-symex's complaint when no
577  // __CPROVER_start exists (if we just go ahead and run it anyway it will
578  // trip an invariant when it tries to load it)
580  {
581  error() << "the program has no entry point";
582  return 6;
583  }
584 
585  // Add failed symbols for any symbol created prior to loading any
586  // particular function:
587  add_failed_symbols(lazy_goto_model.symbol_table);
588 
589  // Provide show-goto-functions and similar dump functions after symex
590  // executes. If --paths is active, these dump routines run after every
591  // paths iteration. Its return value indicates that if we ran any dump
592  // function, then we should skip the actual solver phase.
593  auto callback_after_symex = [this, &lazy_goto_model]() {
594  return show_loaded_functions(lazy_goto_model);
595  };
596 
597  // The `configure_bmc` callback passed will enable enum-unwind-static if
598  // applicable.
601  options,
602  lazy_goto_model,
604  configure_bmc,
605  callback_after_symex);
606  }
607 }
608 
610 {
611  try
612  {
613  if(cmdline.isset("property"))
614  ::set_properties(goto_model, cmdline.get_values("property"));
615  }
616 
617  catch(const char *e)
618  {
619  error() << e << eom;
620  return true;
621  }
622 
623  catch(const std::string &e)
624  {
625  error() << e << eom;
626  return true;
627  }
628 
629  catch(int)
630  {
631  return true;
632  }
633 
634  return false;
635 }
636 
638  std::unique_ptr<goto_modelt> &goto_model,
639  const optionst &options)
640 {
641  if(cmdline.args.empty())
642  {
643  error() << "Please provide a program to verify" << eom;
644  return 6;
645  }
646 
647  try
648  {
650  *this, options, get_message_handler());
651  lazy_goto_model.initialize(cmdline.args, options);
652 
654  util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
655 
656  // Show the class hierarchy
657  if(cmdline.isset("show-class-hierarchy"))
658  {
660  return CPROVER_EXIT_SUCCESS;
661  }
662 
663  // Add failed symbols for any symbol created prior to loading any
664  // particular function:
665  add_failed_symbols(lazy_goto_model.symbol_table);
666 
667  status() << "Generating GOTO Program" << messaget::eom;
668  lazy_goto_model.load_all_functions();
669 
670  // Show the symbol table before process_goto_functions mangles return
671  // values, etc
672  if(cmdline.isset("show-symbol-table"))
673  {
675  return 0;
676  }
677  else if(cmdline.isset("list-symbols"))
678  {
680  return 0;
681  }
682 
683  // Move the model out of the local lazy_goto_model
684  // and into the caller's goto_model
686  std::move(lazy_goto_model));
687  if(goto_model == nullptr)
688  return 6;
689 
690  // show it?
691  if(cmdline.isset("show-loops"))
692  {
693  show_loop_ids(ui_message_handler.get_ui(), *goto_model);
694  return 0;
695  }
696 
697  // show it?
698  if(
699  cmdline.isset("show-goto-functions") ||
700  cmdline.isset("list-goto-functions"))
701  {
703  *goto_model,
706  cmdline.isset("list-goto-functions"));
707  return 0;
708  }
709 
710  status() << config.object_bits_info() << eom;
711  }
712 
713  catch(const char *e)
714  {
715  error() << e << eom;
716  return 6;
717  }
718 
719  catch(const std::string &e)
720  {
721  error() << e << eom;
722  return 6;
723  }
724 
725  catch(int)
726  {
727  return 6;
728  }
729 
730  catch(const std::bad_alloc &)
731  {
732  error() << "Out of memory" << eom;
733  return 6;
734  }
735 
736  return -1; // no error, continue
737 }
738 
740  goto_model_functiont &function,
741  const abstract_goto_modelt &model,
742  const optionst &options)
743 {
744  journalling_symbol_tablet &symbol_table = function.get_symbol_table();
745  namespacet ns(symbol_table);
746  goto_functionst::goto_functiont &goto_function = function.get_goto_function();
747 
748  bool using_symex_driven_loading =
749  options.get_bool_option("symex-driven-lazy-loading");
750 
751  try
752  {
753  // Removal of RTTI inspection:
755  goto_function, symbol_table, *class_hierarchy, get_message_handler());
756  // Java virtual functions -> explicit dispatch tables:
757  remove_virtual_functions(function);
758 
759  auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
760  return symbol_table.lookup_ref(id).value.is_nil() &&
761  !model.can_produce_function(id);
762  };
763 
764  remove_returns(function, function_is_stub);
765 
766  replace_java_nondet(function);
767 
768  // Similar removal of java nondet statements:
770  function,
773  ID_java);
774 
775  if(using_symex_driven_loading)
776  {
777  // remove exceptions
778  // If using symex-driven function loading we need to do this now so that
779  // symex doesn't have to cope with exception-handling constructs; however
780  // the results are slightly worse than running it in whole-program mode
781  // (e.g. dead catch sites will be retained)
783  goto_function.body,
784  symbol_table,
785  *class_hierarchy.get(),
787  }
788 
789  // add generic checks
790  goto_check(ns, options, ID_java, function.get_goto_function());
791 
792  // Replace Java new side effects
793  remove_java_new(goto_function, symbol_table, get_message_handler());
794 
795  // checks don't know about adjusted float expressions
796  adjust_float_expressions(goto_function, ns);
797 
798  // add failed symbols for anything created relating to this particular
799  // function (note this means subseqent passes mustn't create more!):
801  symbol_table.get_inserted();
802  for(const irep_idt &new_symbol_name : new_symbols)
803  {
805  symbol_table.lookup_ref(new_symbol_name),
806  symbol_table);
807  }
808 
809  // If using symex-driven function loading we must label the assertions
810  // now so symex sees its targets; otherwise we leave this until
811  // process_goto_functions, as we haven't run remove_exceptions yet, and that
812  // pass alters the CFG.
813  if(using_symex_driven_loading)
814  {
815  // label the assertions
816  label_properties(goto_function.body);
817 
818  goto_function.body.update();
819  function.compute_location_numbers();
820  goto_function.body.compute_loop_numbers();
821  }
822 
823  // update the function member in each instruction
824  function.update_instructions_function();
825  }
826 
827  catch(const char *e)
828  {
829  error() << e << eom;
830  throw;
831  }
832 
833  catch(const std::string &e)
834  {
835  error() << e << eom;
836  throw;
837  }
838 
839  catch(const std::bad_alloc &)
840  {
841  error() << "Out of memory" << eom;
842  throw;
843  }
844 }
845 
847  const abstract_goto_modelt &goto_model)
848 {
849  if(cmdline.isset("show-symbol-table"))
850  {
852  return true;
853  }
854  else if(cmdline.isset("list-symbols"))
855  {
857  return true;
858  }
859 
860  if(cmdline.isset("show-loops"))
861  {
863  return true;
864  }
865 
866  if(
867  cmdline.isset("show-goto-functions") ||
868  cmdline.isset("list-goto-functions"))
869  {
870  namespacet ns(goto_model.get_symbol_table());
872  ns,
875  goto_model.get_goto_functions(),
876  cmdline.isset("list-goto-functions"));
877  return true;
878  }
879 
880  if(cmdline.isset("show-properties"))
881  {
882  namespacet ns(goto_model.get_symbol_table());
884  ns,
887  goto_model.get_goto_functions());
888  return true;
889  }
890 
891  return false;
892 }
893 
895  goto_modelt &goto_model,
896  const optionst &options)
897 {
898  try
899  {
900  status() << "Running GOTO functions transformation passes" << eom;
901 
902  bool using_symex_driven_loading =
903  options.get_bool_option("symex-driven-lazy-loading");
904 
905  // When using symex-driven lazy loading, *all* relevant processing is done
906  // during process_goto_function, so we have nothing to do here.
907  if(using_symex_driven_loading)
908  return false;
909 
910  // remove catch and throw
912  goto_model, *class_hierarchy.get(), get_message_handler());
913 
914  // instrument library preconditions
915  instrument_preconditions(goto_model);
916 
917  // ignore default/user-specified initialization
918  // of variables with static lifetime
919  if(cmdline.isset("nondet-static"))
920  {
921  status() << "Adding nondeterministic initialization "
922  "of static/global variables" << eom;
923  nondet_static(goto_model);
924  }
925 
926  // recalculate numbers, etc.
927  goto_model.goto_functions.update();
928 
929  if(cmdline.isset("drop-unused-functions"))
930  {
931  // Entry point will have been set before and function pointers removed
932  status() << "Removing unused functions" << eom;
934  }
935 
936  // remove skips such that trivial GOTOs are deleted
937  remove_skip(goto_model);
938 
939  // label the assertions
940  // This must be done after adding assertions and
941  // before using the argument of the "property" option.
942  // Do not re-label after using the property slicer because
943  // this would cause the property identifiers to change.
944  label_properties(goto_model);
945 
946  // reachability slice?
947  if(cmdline.isset("reachability-slice-fb"))
948  {
949  if(cmdline.isset("reachability-slice"))
950  {
951  error() << "--reachability-slice and --reachability-slice-fb "
952  << "must not be given together" << eom;
953  return true;
954  }
955 
956  status() << "Performing a forwards-backwards reachability slice" << eom;
957  if(cmdline.isset("property"))
958  reachability_slicer(goto_model, cmdline.get_values("property"), true);
959  else
960  reachability_slicer(goto_model, true);
961  }
962 
963  if(cmdline.isset("reachability-slice"))
964  {
965  status() << "Performing a reachability slice" << eom;
966  if(cmdline.isset("property"))
967  reachability_slicer(goto_model, cmdline.get_values("property"));
968  else
969  reachability_slicer(goto_model);
970  }
971 
972  // full slice?
973  if(cmdline.isset("full-slice"))
974  {
975  status() << "Performing a full slice" << eom;
976  if(cmdline.isset("property"))
977  property_slicer(goto_model, cmdline.get_values("property"));
978  else
979  full_slicer(goto_model);
980  }
981 
982  // remove any skips introduced
983  remove_skip(goto_model);
984  }
985 
986  catch(const char *e)
987  {
988  error() << e << eom;
989  return true;
990  }
991 
992  catch(const std::string &e)
993  {
994  error() << e << eom;
995  return true;
996  }
997 
998  catch(int)
999  {
1000  return true;
1001  }
1002 
1003  catch(const std::bad_alloc &)
1004  {
1005  error() << "Out of memory" << eom;
1006  return true;
1007  }
1008 
1009  return false;
1010 }
1011 
1013 {
1014  static const irep_idt initialize_id = INITIALIZE_FUNCTION;
1015 
1016  return name != goto_functionst::entry_point() && name != initialize_id;
1017 }
1018 
1020  const irep_idt &function_name,
1021  symbol_table_baset &symbol_table,
1022  goto_functiont &function,
1023  bool body_available)
1024 {
1025  // Provide a simple stub implementation for any function we don't have a
1026  // bytecode implementation for:
1027 
1028  if(body_available)
1029  return false;
1030 
1031  if(!can_generate_function_body(function_name))
1032  return false;
1033 
1034  if(symbol_table.lookup_ref(function_name).mode == ID_java)
1035  {
1037  function_name,
1038  symbol_table,
1042 
1043  goto_convert_functionst converter(symbol_table, get_message_handler());
1044  converter.convert_function(function_name, function);
1045 
1046  return true;
1047  }
1048  else
1049  {
1050  return false;
1051  }
1052 }
1053 
1056 {
1057  // clang-format off
1058  std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
1059  <<
1060  "* * Copyright (C) 2001-2018 * *\n"
1061  "* * Daniel Kroening, Edmund Clarke * *\n"
1062  "* * Carnegie Mellon University, Computer Science Department * *\n"
1063  "* * kroening@kroening.com * *\n"
1064  "\n"
1065  "Usage: Purpose:\n"
1066  "\n"
1067  " jbmc [-?] [-h] [--help] show help\n"
1068  " jbmc class name of class or JAR file to be checked\n"
1069  " In the case of a JAR file, if a main class can be\n" // NOLINT(*)
1070  " inferred from --main-class, --function, or the JAR\n" // NOLINT(*)
1071  " manifest (checked in this order), the behavior is\n" // NOLINT(*)
1072  " the same as running jbmc on the corresponding\n" // NOLINT(*)
1073  " class file."
1074  "\n"
1075  "Analysis options:\n"
1077  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
1078  " --property id only check one specific property\n"
1079  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1080  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1081  "\n"
1083  "\n"
1084  "Program representations:\n"
1085  " --show-parse-tree show parse tree\n"
1086  " --show-symbol-table show loaded symbol table\n"
1087  " --list-symbols list symbols with type information\n"
1089  " --drop-unused-functions drop functions trivially unreachable\n"
1090  " from main function\n"
1092  "\n"
1093  "Program instrumentation options:\n"
1094  " --no-assertions ignore user assertions\n"
1095  " --no-assumptions ignore user assumptions\n"
1096  " --error-label label check that label is unreachable\n"
1097  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1099  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1100  "\n"
1101  "Java Bytecode frontend options:\n"
1102  " --classpath dir/jar set the classpath\n"
1103  " --main-class class-name set the name of the main class\n"
1105  // This one is handled by jbmc_parse_options not by the Java frontend,
1106  // hence its presence here:
1107  " --java-threading enable java multi-threading support (experimental)\n" // NOLINT(*)
1108  " --java-unwind-enum-static unwind loops in static initialization of enums\n" // NOLINT(*)
1109  // Currently only supported in the JBMC frontend:
1110  " --symex-driven-lazy-loading only load functions when first entered by symbolic\n" // NOLINT(*)
1111  " execution. Note that --show-symbol-table,\n"
1112  " --show-goto-functions/properties output\n"
1113  " will be restricted to loaded methods in this case,\n" // NOLINT(*)
1114  " and only output after the symex phase.\n"
1115  "\n"
1116  "Semantic transformations:\n"
1117  // NOLINTNEXTLINE(whitespace/line_length)
1118  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1119  "\n"
1120  "BMC options:\n"
1121  HELP_BMC
1122  "\n"
1123  "Backend options:\n"
1124  " --object-bits n number of bits used for object addresses\n"
1125  " --dimacs generate CNF in DIMACS format\n"
1126  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1127  " --localize-faults localize faults (experimental)\n"
1128  " --smt1 use default SMT1 solver (obsolete)\n"
1129  " --smt2 use default SMT2 solver (Z3)\n"
1130  " --boolector use Boolector\n"
1131  " --mathsat use MathSAT\n"
1132  " --cvc4 use CVC4\n"
1133  " --yices use Yices\n"
1134  " --z3 use Z3\n"
1135  " --refine use refinement procedure (experimental)\n"
1137  " --outfile filename output formula to given file\n"
1138  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1139  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1140  "\n"
1141  "Other options:\n"
1142  " --version show version and exit\n"
1143  " --xml-ui use XML-formatted output\n"
1144  " --json-ui use JSON-formatted output\n"
1146  HELP_FLUSH
1147  " --verbosity # verbosity level\n"
1149  "\n";
1150  // clang-format on
1151 }
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 convert_nondet(goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_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...
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...
std::unique_ptr< class_hierarchyt > class_hierarchy
#define HELP_REACHABILITY_SLICER
Abstract interface to eager or lazy GOTO models.
bool is_nil() const
Definition: irep.h:172
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:52
Functions for replacing virtual function call with a static function calls in functions, groups of functions and goto programs.
irep_idt mode
Language mode.
Definition: symbol.h:49
uit get_ui() const
Definition: ui_message.h:30
std::string object_bits_info()
Definition: config.cpp:1257
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:98
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.
exprt value
Initial value of symbol.
Definition: symbol.h:34
std::string get_value(char option) const
Definition: cmdline.cpp:45
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 &)
java_object_factory_parameterst object_factory_params
Pointer Dereferencing.
A GOTO model that produces function bodies on demand.
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
configt config
Definition: config.cpp:24
Remove &#39;asm&#39; statements by compiling them into suitable standard goto program instructions.
void remove_virtual_functions(const 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...
#define HELP_FUNCTIONS
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
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
void remove_instanceof(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...
path_strategy_choosert path_strategy_chooser
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:391
Unused function removal.
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:267
bool set(const cmdlinet &cmdline)
Definition: config.cpp:767
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
void add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler)
Definition: bmc.h:108
virtual const symbol_tablet & get_symbol_table() const override
#define HELP_TIMESTAMP
Definition: timestamper.h:14
argst args
Definition: cmdline.h:44
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.
void parse_java_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the java object factory parameters from a given command line.
bool can_generate_function_body(const irep_idt &name)
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
const changesett & get_inserted() const
#define INITIALIZE_FUNCTION
Nondeterministically initializes global scope variables, except for constants (such as string literal...
#define HELP_FLUSH
Definition: ui_message.h:104
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
#define HELP_STRING_REFINEMENT
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:386
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Function Inlining.
#define HELP_BMC
Definition: bmc.h:303
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 using java_object_factory.
std::unique_ptr< languaget > new_java_bytecode_language()
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
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)
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
virtual int doit() override
invoke main modules
Replace Java Nondet expressions.
std::string banner_string(const std::string &front_end, const std::string &version)
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:58
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
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
Definition: goto_function.h:26
void load_all_functions() const
Eagerly loads all functions from the symbol table.
static eomt eom
Definition: message.h:284
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:1368
static int do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, ui_message_handlert &ui, 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:502
message_handlert & get_message_handler()
Definition: message.h:174
Goto Programs with Functions.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
#define HELP_GOTO_TRACE
Definition: goto_trace.h:259
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & status() const
Definition: message.h:401
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
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
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...
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
std::unordered_set< irep_idt > changesett
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:132
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()
void set(const optionst &)
Assigns the parameters from given options.
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
Unwind loops in static initializers.
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:43
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:26
mstreamt & debug() const
Definition: message.h:416
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:33
mstreamt mstream
Definition: message.h:427
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
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)
static irep_idt this_architecture()
Definition: config.cpp:1268
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
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 ...
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:153
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)