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/exit_codes.h>
20 #include <util/config.h>
21 #include <util/unicode.h>
22 #include <util/invariant.h>
23 
24 #include <langapi/language.h>
25 
26 #include <ansi-c/ansi_c_language.h>
27 
33 #include <goto-programs/loop_ids.h>
43 
47 
49 
51 
52 #include <langapi/mode.h>
53 
62 
63 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv):
64  parse_options_baset(JBMC_OPTIONS, argc, argv),
65  messaget(ui_message_handler),
66  ui_message_handler(cmdline, "JBMC " CBMC_VERSION),
67  path_strategy_chooser()
68 {
69 }
70 
72  int argc,
73  const char **argv,
74  const std::string &extra_options):
75  parse_options_baset(JBMC_OPTIONS+extra_options, argc, argv),
76  messaget(ui_message_handler),
77  ui_message_handler(cmdline, "JBMC " CBMC_VERSION),
78  path_strategy_chooser()
79 {
80 }
81 
83 {
84  if(config.set(cmdline))
85  {
86  usage_error();
87  exit(1); // should contemplate EX_USAGE from sysexits.h
88  }
89 
90  if(cmdline.isset("show-symex-strategies"))
91  {
94  }
95 
97 
98  if(cmdline.isset("program-only"))
99  options.set_option("program-only", true);
100 
101  if(cmdline.isset("show-vcc"))
102  options.set_option("show-vcc", true);
103 
104  if(cmdline.isset("cover"))
105  parse_cover_options(cmdline, options);
106 
107  if(cmdline.isset("no-simplify"))
108  options.set_option("simplify", false);
109  else
110  options.set_option("simplify", true);
111 
112  if(cmdline.isset("stop-on-fail") ||
113  cmdline.isset("dimacs") ||
114  cmdline.isset("outfile"))
115  options.set_option("stop-on-fail", true);
116  else
117  options.set_option("stop-on-fail", false);
118 
119  if(cmdline.isset("trace") ||
120  cmdline.isset("stop-on-fail"))
121  options.set_option("trace", true);
122 
123  if(cmdline.isset("localize-faults"))
124  options.set_option("localize-faults", true);
125  if(cmdline.isset("localize-faults-method"))
126  {
127  options.set_option(
128  "localize-faults-method",
129  cmdline.get_value("localize-faults-method"));
130  }
131 
132  if(cmdline.isset("unwind"))
133  options.set_option("unwind", cmdline.get_value("unwind"));
134 
135  if(cmdline.isset("depth"))
136  options.set_option("depth", cmdline.get_value("depth"));
137 
138  if(cmdline.isset("debug-level"))
139  options.set_option("debug-level", cmdline.get_value("debug-level"));
140 
141  if(cmdline.isset("slice-by-trace"))
142  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
143 
144  if(cmdline.isset("unwindset"))
145  options.set_option("unwindset", cmdline.get_value("unwindset"));
146 
147  // constant propagation
148  if(cmdline.isset("no-propagation"))
149  options.set_option("propagation", false);
150  else
151  options.set_option("propagation", true);
152 
153  // transform self loops to assumptions
154  options.set_option(
155  "self-loops-to-assumptions",
156  !cmdline.isset("no-self-loops-to-assumptions"));
157 
158  // all checks supported by goto_check
160 
161  // unwind loops in java enum static initialization
162  if(cmdline.isset("java-unwind-enum-static"))
163  options.set_option("java-unwind-enum-static", true);
164 
165  // check assertions
166  if(cmdline.isset("no-assertions"))
167  options.set_option("assertions", false);
168  else
169  options.set_option("assertions", true);
170 
171  // use assumptions
172  if(cmdline.isset("no-assumptions"))
173  options.set_option("assumptions", false);
174  else
175  options.set_option("assumptions", true);
176 
177  // magic error label
178  if(cmdline.isset("error-label"))
179  options.set_option("error-label", cmdline.get_values("error-label"));
180 
181  // generate unwinding assertions
182  if(cmdline.isset("cover"))
183  options.set_option("unwinding-assertions", false);
184  else
185  {
186  options.set_option(
187  "unwinding-assertions",
188  cmdline.isset("unwinding-assertions"));
189  }
190 
191  // generate unwinding assumptions otherwise
192  options.set_option(
193  "partial-loops",
194  cmdline.isset("partial-loops"));
195 
196  if(options.get_bool_option("partial-loops") &&
197  options.get_bool_option("unwinding-assertions"))
198  {
199  error() << "--partial-loops and --unwinding-assertions "
200  << "must not be given together" << eom;
201  exit(1); // should contemplate EX_USAGE from sysexits.h
202  }
203 
204  // remove unused equations
205  options.set_option(
206  "slice-formula",
207  cmdline.isset("slice-formula"));
208 
209  // simplify if conditions and branches
210  if(cmdline.isset("no-simplify-if"))
211  options.set_option("simplify-if", false);
212  else
213  options.set_option("simplify-if", true);
214 
215  if(cmdline.isset("arrays-uf-always"))
216  options.set_option("arrays-uf", "always");
217  else if(cmdline.isset("arrays-uf-never"))
218  options.set_option("arrays-uf", "never");
219  else
220  options.set_option("arrays-uf", "auto");
221 
222  if(cmdline.isset("dimacs"))
223  options.set_option("dimacs", true);
224 
225  if(cmdline.isset("refine-arrays"))
226  {
227  options.set_option("refine", true);
228  options.set_option("refine-arrays", true);
229  }
230 
231  if(cmdline.isset("refine-arithmetic"))
232  {
233  options.set_option("refine", true);
234  options.set_option("refine-arithmetic", true);
235  }
236 
237  if(cmdline.isset("refine"))
238  {
239  options.set_option("refine", true);
240  options.set_option("refine-arrays", true);
241  options.set_option("refine-arithmetic", true);
242  }
243 
244  if(cmdline.isset("refine-strings"))
245  {
246  options.set_option("refine-strings", true);
247  options.set_option("string-printable", cmdline.isset("string-printable"));
248  if(cmdline.isset("string-max-length"))
249  options.set_option(
250  "string-max-length", cmdline.get_value("string-max-length"));
251  }
252 
253  if(cmdline.isset("max-node-refinement"))
254  options.set_option(
255  "max-node-refinement",
256  cmdline.get_value("max-node-refinement"));
257 
258  // SMT Options
259  bool version_set=false;
260 
261  if(cmdline.isset("smt1"))
262  {
263  options.set_option("smt1", true);
264  options.set_option("smt2", false);
265  version_set=true;
266  }
267 
268  if(cmdline.isset("smt2"))
269  {
270  // If both are given, smt2 takes precedence
271  options.set_option("smt1", false);
272  options.set_option("smt2", true);
273  version_set=true;
274  }
275 
276  if(cmdline.isset("fpa"))
277  options.set_option("fpa", true);
278 
279  bool solver_set=false;
280 
281  if(cmdline.isset("boolector"))
282  {
283  options.set_option("boolector", true), solver_set=true;
284  if(!version_set)
285  options.set_option("smt2", true), version_set=true;
286  }
287 
288  if(cmdline.isset("mathsat"))
289  {
290  options.set_option("mathsat", true), solver_set=true;
291  if(!version_set)
292  options.set_option("smt2", true), version_set=true;
293  }
294 
295  if(cmdline.isset("cvc3"))
296  {
297  options.set_option("cvc3", true), solver_set=true;
298  if(!version_set)
299  options.set_option("smt1", true), version_set=true;
300  }
301 
302  if(cmdline.isset("cvc4"))
303  {
304  options.set_option("cvc4", true), solver_set=true;
305  if(!version_set)
306  options.set_option("smt2", true), version_set=true;
307  }
308 
309  if(cmdline.isset("yices"))
310  {
311  options.set_option("yices", true), solver_set=true;
312  if(!version_set)
313  options.set_option("smt2", true), version_set=true;
314  }
315 
316  if(cmdline.isset("z3"))
317  {
318  options.set_option("z3", true), solver_set=true;
319  if(!version_set)
320  options.set_option("smt2", true), version_set=true;
321  }
322 
323  if(cmdline.isset("opensmt"))
324  {
325  options.set_option("opensmt", true), solver_set=true;
326  if(!version_set)
327  options.set_option("smt1", true), version_set=true;
328  }
329 
330  if(version_set && !solver_set)
331  {
332  if(cmdline.isset("outfile"))
333  {
334  // outfile and no solver should give standard compliant SMT-LIB
335  options.set_option("generic", true), solver_set=true;
336  }
337  else
338  {
339  if(options.get_bool_option("smt1"))
340  {
341  options.set_option("boolector", true), solver_set=true;
342  }
343  else
344  {
345  INVARIANT(options.get_bool_option("smt2"), "smt2 set");
346  options.set_option("z3", true), solver_set=true;
347  }
348  }
349  }
350 
351  // Either have solver and standard version set, or neither.
352  INVARIANT(version_set==solver_set, "solver and version set");
353 
354  if(cmdline.isset("beautify"))
355  options.set_option("beautify", true);
356 
357  if(cmdline.isset("no-sat-preprocessor"))
358  options.set_option("sat-preprocessor", false);
359  else
360  options.set_option("sat-preprocessor", true);
361 
362  options.set_option(
363  "pretty-names",
364  !cmdline.isset("no-pretty-names"));
365 
366  if(cmdline.isset("outfile"))
367  options.set_option("outfile", cmdline.get_value("outfile"));
368 
369  if(cmdline.isset("graphml-witness"))
370  {
371  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
372  options.set_option("stop-on-fail", true);
373  options.set_option("trace", true);
374  }
375 
376  if(cmdline.isset("symex-coverage-report"))
377  options.set_option(
378  "symex-coverage-report",
379  cmdline.get_value("symex-coverage-report"));
380 
382 
383  if(cmdline.isset("symex-driven-lazy-loading"))
384  {
385  options.set_option("symex-driven-lazy-loading", true);
386  for(const char *opt :
387  { "nondet-static",
388  "full-slice",
389  "lazy-methods",
390  "reachability-slice",
391  "reachability-slice-fb" })
392  {
393  if(cmdline.isset(opt))
394  {
395  throw std::string("Option ") + opt +
396  " can't be used with --symex-driven-lazy-loading";
397  }
398  }
399  }
400 
401  // The 'allow-pointer-unsoundness' option prevents symex from throwing an
402  // exception when it encounters pointers that are shared across threads.
403  // This is unsound but given that pointers are ubiquitous in java this check
404  // must be disabled in order to support the analysis of multithreaded java
405  // code.
406  if(cmdline.isset("java-threading"))
407  options.set_option("allow-pointer-unsoundness", true);
408 }
409 
412 {
413  if(cmdline.isset("version"))
414  {
415  std::cout << CBMC_VERSION << '\n';
416  return 0; // should contemplate EX_OK from sysexits.h
417  }
418 
419  //
420  // command line options
421  //
422 
423  optionst options;
424  try
425  {
426  get_command_line_options(options);
427  }
428 
429  catch(const char *error_msg)
430  {
431  error() << error_msg << eom;
432  return 6; // should contemplate EX_SOFTWARE from sysexits.h
433  }
434 
435  catch(const std::string &error_msg)
436  {
437  error() << error_msg << eom;
438  return 6; // should contemplate EX_SOFTWARE from sysexits.h
439  }
440 
443 
444  //
445  // Print a banner
446  //
447  status() << "JBMC version " CBMC_VERSION " "
448  << sizeof(void *)*8 << "-bit "
449  << config.this_architecture() << " "
451 
454 
455  if(cmdline.isset("show-parse-tree"))
456  {
457  if(cmdline.args.size()!=1)
458  {
459  error() << "Please give exactly one source file" << eom;
460  return 6;
461  }
462 
463  std::string filename=cmdline.args[0];
464 
465  #ifdef _MSC_VER
466  std::ifstream infile(widen(filename));
467  #else
468  std::ifstream infile(filename);
469  #endif
470 
471  if(!infile)
472  {
473  error() << "failed to open input file `"
474  << filename << "'" << eom;
475  return 6;
476  }
477 
478  std::unique_ptr<languaget> language=
479  get_language_from_filename(filename);
480 
481  if(language==nullptr)
482  {
483  error() << "failed to figure out type of file `"
484  << filename << "'" << eom;
485  return 6;
486  }
487 
488  language->get_language_options(cmdline);
490 
491  status() << "Parsing " << filename << eom;
492 
493  if(language->parse(infile, filename))
494  {
495  error() << "PARSING ERROR" << eom;
496  return 6;
497  }
498 
499  language->show_parse(std::cout);
500  return 0;
501  }
502 
503  std::function<void(bmct &, const symbol_tablet &)> configure_bmc = nullptr;
504  if(options.get_bool_option("java-unwind-enum-static"))
505  {
506  configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) {
508  [&symbol_table](
509  const irep_idt &function_id,
510  unsigned loop_number,
511  unsigned unwind,
512  unsigned &max_unwind) {
514  function_id,
515  loop_number,
516  unwind,
517  max_unwind,
518  symbol_table);
519  });
520  };
521  }
522 
524  cmdline.isset("java-max-input-array-length")
525  ? std::stoul(cmdline.get_value("java-max-input-array-length"))
528  cmdline.isset("string-max-input-length")
529  ? std::stoul(cmdline.get_value("string-max-input-length"))
532  cmdline.isset("java-max-input-tree-depth")
533  ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
535 
536  stub_objects_are_not_null = cmdline.isset("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  *this,
565  configure_bmc);
566  }
567  else
568  {
569  // Use symex-driven lazy loading:
571  *this, options, get_message_handler());
572  lazy_goto_model.initialize(cmdline);
573 
574  // The precise wording of this error matches goto-symex's complaint when no
575  // __CPROVER_start exists (if we just go ahead and run it anyway it will
576  // trip an invariant when it tries to load it)
578  {
579  error() << "the program has no entry point";
580  return 6;
581  }
582 
583  // Add failed symbols for any symbol created prior to loading any
584  // particular function:
585  add_failed_symbols(lazy_goto_model.symbol_table);
586 
587  // If applicable, parse the coverage instrumentation configuration, which
588  // will be used in process_goto_function:
589  cover_config =
591  options, lazy_goto_model.symbol_table, get_message_handler());
592 
593  // Provide show-goto-functions and similar dump functions after symex
594  // executes. If --paths is active, these dump routines run after every
595  // paths iteration. Its return value indicates that if we ran any dump
596  // function, then we should skip the actual solver phase.
597  auto callback_after_symex = [this, &lazy_goto_model]() {
598  return show_loaded_functions(lazy_goto_model);
599  };
600 
601  // The `configure_bmc` callback passed will enable enum-unwind-static if
602  // applicable.
603  return
606  options,
607  lazy_goto_model,
609  *this,
610  configure_bmc,
611  callback_after_symex);
612  }
613 }
614 
616 {
617  try
618  {
619  if(cmdline.isset("property"))
620  ::set_properties(goto_model, cmdline.get_values("property"));
621  }
622 
623  catch(const char *e)
624  {
625  error() << e << eom;
626  return true;
627  }
628 
629  catch(const std::string &e)
630  {
631  error() << e << eom;
632  return true;
633  }
634 
635  catch(int)
636  {
637  return true;
638  }
639 
640  return false;
641 }
642 
644  std::unique_ptr<goto_modelt> &goto_model,
645  const optionst &options)
646 {
647  if(cmdline.args.empty())
648  {
649  error() << "Please provide a program to verify" << eom;
650  return 6;
651  }
652 
653  try
654  {
656  *this, options, get_message_handler());
657  lazy_goto_model.initialize(cmdline);
658 
659  // Show the class hierarchy
660  if(cmdline.isset("show-class-hierarchy"))
661  {
662  class_hierarchyt hierarchy;
663  hierarchy(lazy_goto_model.symbol_table);
666  return CPROVER_EXIT_SUCCESS;
667  }
668 
669  // Add failed symbols for any symbol created prior to loading any
670  // particular function:
671  add_failed_symbols(lazy_goto_model.symbol_table);
672 
673  status() << "Generating GOTO Program" << messaget::eom;
674  lazy_goto_model.load_all_functions();
675 
676  // Show the symbol table before process_goto_functions mangles return
677  // values, etc
678  if(cmdline.isset("show-symbol-table"))
679  {
681  lazy_goto_model.symbol_table, ui_message_handler.get_ui());
682  return 0;
683  }
684 
685  // Move the model out of the local lazy_goto_model
686  // and into the caller's goto_model
688  std::move(lazy_goto_model));
689  if(goto_model == nullptr)
690  return 6;
691 
692  // show it?
693  if(cmdline.isset("show-loops"))
694  {
695  show_loop_ids(ui_message_handler.get_ui(), *goto_model);
696  return 0;
697  }
698 
699  // show it?
700  if(
701  cmdline.isset("show-goto-functions") ||
702  cmdline.isset("list-goto-functions"))
703  {
705  *goto_model,
708  cmdline.isset("list-goto-functions"));
709  return 0;
710  }
711 
712  status() << config.object_bits_info() << eom;
713  }
714 
715  catch(const char *e)
716  {
717  error() << e << eom;
718  return 6;
719  }
720 
721  catch(const std::string &e)
722  {
723  error() << e << eom;
724  return 6;
725  }
726 
727  catch(int)
728  {
729  return 6;
730  }
731 
732  catch(const std::bad_alloc &)
733  {
734  error() << "Out of memory" << eom;
735  return 6;
736  }
737 
738  return -1; // no error, continue
739 }
740 
742  goto_model_functiont &function,
743  const abstract_goto_modelt &model,
744  const optionst &options)
745 {
746  journalling_symbol_tablet &symbol_table = function.get_symbol_table();
747  namespacet ns(symbol_table);
748  goto_functionst::goto_functiont &goto_function = function.get_goto_function();
749 
750  bool using_symex_driven_loading =
751  options.get_bool_option("symex-driven-lazy-loading");
752 
753  try
754  {
755  // Removal of RTTI inspection:
756  remove_instanceof(goto_function, symbol_table);
757  // Java virtual functions -> explicit dispatch tables:
758  remove_virtual_functions(function);
759 
760  if(using_symex_driven_loading)
761  {
762  // remove exceptions
763  // If using symex-driven function loading we need to do this now so that
764  // symex doesn't have to cope with exception-handling constructs; however
765  // the results are slightly worse than running it in whole-program mode
766  // (e.g. dead catch sites will be retained)
768  goto_function.body,
769  symbol_table,
771  }
772 
773  auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
774  return symbol_table.lookup_ref(id).value.is_nil() &&
775  !model.can_produce_function(id);
776  };
777 
778  remove_returns(function, function_is_stub);
779 
780  replace_java_nondet(function);
781 
782  // Similar removal of java nondet statements:
784  function,
787  ID_java);
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!):
800  journalling_symbol_tablet::changesett new_symbols =
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 insert the coverage goals
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  // instrument cover goals
816  if(cmdline.isset("cover"))
817  {
818  INVARIANT(
819  cover_config != nullptr, "cover config should have been parsed");
821  }
822 
823  // label the assertions
824  label_properties(goto_function.body);
825 
826  goto_function.body.update();
827  function.compute_location_numbers();
828  goto_function.body.compute_loop_numbers();
829  }
830 
831  // update the function member in each instruction
832  function.update_instructions_function();
833  }
834 
835  catch(const char *e)
836  {
837  error() << e << eom;
838  throw;
839  }
840 
841  catch(const std::string &e)
842  {
843  error() << e << eom;
844  throw;
845  }
846 
847  catch(const std::bad_alloc &)
848  {
849  error() << "Out of memory" << eom;
850  throw;
851  }
852 }
853 
855  const abstract_goto_modelt &goto_model)
856 {
857  if(cmdline.isset("show-symbol-table"))
858  {
860  goto_model.get_symbol_table(), ui_message_handler.get_ui());
861  return true;
862  }
863 
864  if(cmdline.isset("show-loops"))
865  {
867  return true;
868  }
869 
870  if(
871  cmdline.isset("show-goto-functions") ||
872  cmdline.isset("list-goto-functions"))
873  {
874  namespacet ns(goto_model.get_symbol_table());
876  ns,
879  goto_model.get_goto_functions(),
880  cmdline.isset("list-goto-functions"));
881  return true;
882  }
883 
884  if(cmdline.isset("show-properties"))
885  {
886  namespacet ns(goto_model.get_symbol_table());
888  ns,
891  goto_model.get_goto_functions());
892  return true;
893  }
894 
895  return false;
896 }
897 
899  goto_modelt &goto_model,
900  const optionst &options)
901 {
902  try
903  {
904  status() << "Running GOTO functions transformation passes" << eom;
905 
906  bool using_symex_driven_loading =
907  options.get_bool_option("symex-driven-lazy-loading");
908 
909  // When using symex-driven lazy loading, *all* relevant processing is done
910  // during process_goto_function, so we have nothing to do here.
911  if(using_symex_driven_loading)
912  return false;
913 
914  // remove catch and throw
915  // (introduces instanceof but request it is removed)
918 
919  // instrument library preconditions
920  instrument_preconditions(goto_model);
921 
922  // ignore default/user-specified initialization
923  // of variables with static lifetime
924  if(cmdline.isset("nondet-static"))
925  {
926  status() << "Adding nondeterministic initialization "
927  "of static/global variables" << eom;
928  nondet_static(goto_model);
929  }
930 
931  // recalculate numbers, etc.
932  goto_model.goto_functions.update();
933 
934  if(cmdline.isset("drop-unused-functions"))
935  {
936  // Entry point will have been set before and function pointers removed
937  status() << "Removing unused functions" << eom;
939  }
940 
941  // remove skips such that trivial GOTOs are deleted and not considered
942  // for coverage annotation:
943  remove_skip(goto_model);
944 
945  // instrument cover goals
946  if(cmdline.isset("cover"))
947  {
948  if(instrument_cover_goals(options, goto_model, get_message_handler()))
949  return true;
950  }
951 
952  // label the assertions
953  // This must be done after adding assertions and
954  // before using the argument of the "property" option.
955  // Do not re-label after using the property slicer because
956  // this would cause the property identifiers to change.
957  label_properties(goto_model);
958 
959  // reachability slice?
960  if(cmdline.isset("reachability-slice-fb"))
961  {
962  if(cmdline.isset("reachability-slice"))
963  {
964  error() << "--reachability-slice and --reachability-slice-fb "
965  << "must not be given together" << eom;
966  return true;
967  }
968 
969  status() << "Performing a forwards-backwards reachability slice" << eom;
970  if(cmdline.isset("property"))
971  reachability_slicer(goto_model, cmdline.get_values("property"), true);
972  else
973  reachability_slicer(goto_model, true);
974  }
975 
976  if(cmdline.isset("reachability-slice"))
977  {
978  status() << "Performing a reachability slice" << eom;
979  if(cmdline.isset("property"))
980  reachability_slicer(goto_model, cmdline.get_values("property"));
981  else
982  reachability_slicer(goto_model);
983  }
984 
985  // full slice?
986  if(cmdline.isset("full-slice"))
987  {
988  status() << "Performing a full slice" << eom;
989  if(cmdline.isset("property"))
990  property_slicer(goto_model, cmdline.get_values("property"));
991  else
992  full_slicer(goto_model);
993  }
994 
995  // remove any skips introduced since coverage instrumentation
996  remove_skip(goto_model);
997  }
998 
999  catch(const char *e)
1000  {
1001  error() << e << eom;
1002  return true;
1003  }
1004 
1005  catch(const std::string &e)
1006  {
1007  error() << e << eom;
1008  return true;
1009  }
1010 
1011  catch(int)
1012  {
1013  return true;
1014  }
1015 
1016  catch(const std::bad_alloc &)
1017  {
1018  error() << "Out of memory" << eom;
1019  return true;
1020  }
1021 
1022  return false;
1023 }
1024 
1026 {
1027  static const irep_idt initialize_id = INITIALIZE_FUNCTION;
1028 
1029  return name != goto_functionst::entry_point() && name != initialize_id;
1030 }
1031 
1033  const irep_idt &function_name,
1034  symbol_table_baset &symbol_table,
1035  goto_functiont &function,
1036  bool body_available)
1037 {
1038  // Provide a simple stub implementation for any function we don't have a
1039  // bytecode implementation for:
1040 
1041  if(body_available)
1042  return false;
1043 
1044  if(!can_generate_function_body(function_name))
1045  return false;
1046 
1047  if(symbol_table.lookup_ref(function_name).mode == ID_java)
1048  {
1050  function_name,
1051  symbol_table,
1055 
1056  goto_convert_functionst converter(symbol_table, get_message_handler());
1057  converter.convert_function(function_name, function);
1058 
1059  return true;
1060  }
1061  else
1062  {
1063  return false;
1064  }
1065 }
1066 
1069 {
1070  // clang-format off
1071  std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
1072  <<
1073  "* * Copyright (C) 2001-2018 * *\n"
1074  "* * Daniel Kroening, Edmund Clarke * *\n"
1075  "* * Carnegie Mellon University, Computer Science Department * *\n"
1076  "* * kroening@kroening.com * *\n"
1077  "\n"
1078  "Usage: Purpose:\n"
1079  "\n"
1080  " jbmc [-?] [-h] [--help] show help\n"
1081  " jbmc class name of class to be checked\n"
1082  "\n"
1083  "Analysis options:\n"
1085  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
1086  " --property id only check one specific property\n"
1087  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1088  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1089  "\n"
1091  "\n"
1092  "Program representations:\n"
1093  " --show-parse-tree show parse tree\n"
1094  " --show-symbol-table show loaded symbol table\n"
1096  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1098  "\n"
1099  "Program instrumentation options:\n"
1101  " --no-assertions ignore user assertions\n"
1102  " --no-assumptions ignore user assumptions\n"
1103  " --error-label label check that label is unreachable\n"
1104  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
1105  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1107  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1108  "\n"
1109  "Java Bytecode frontend options:\n"
1110  " --classpath dir/jar set the classpath\n"
1111  " --main-class class-name set the name of the main class\n"
1113  // This one is handled by jbmc_parse_options not by the Java frontend,
1114  // hence its presence here:
1115  " --java-threading enable experimental support for java multi-threading\n"// NOLINT(*)
1116  " --java-unwind-enum-static try to unwind loops in static initialization of enums\n" // NOLINT(*)
1117  // Currently only supported in the JBMC frontend:
1118  " --symex-driven-lazy-loading only load functions when first entered by symbolic execution\n" // NOLINT(*)
1119  " Note --show-symbol-table/goto-functions/properties output\n" // NOLINT(*)
1120  " will be restricted to loaded methods in this case, and only\n" // NOLINT(*)
1121  " output after the symex phase\n"
1122  "\n"
1123  "BMC options:\n"
1124  HELP_BMC
1125  "\n"
1126  "Backend options:\n"
1127  " --object-bits n number of bits used for object addresses\n"
1128  " --dimacs generate CNF in DIMACS format\n"
1129  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1130  " --localize-faults localize faults (experimental)\n"
1131  " --smt1 use default SMT1 solver (obsolete)\n"
1132  " --smt2 use default SMT2 solver (Z3)\n"
1133  " --boolector use Boolector\n"
1134  " --mathsat use MathSAT\n"
1135  " --cvc4 use CVC4\n"
1136  " --yices use Yices\n"
1137  " --z3 use Z3\n"
1138  " --refine use refinement procedure (experimental)\n"
1139  " --refine-strings use string refinement (experimental)\n"
1140  " --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*)
1141  " --string-max-length add constraint on the length of strings\n" // NOLINT(*)
1142  " --string-max-input-length add constraint on the length of input strings\n" // NOLINT(*)
1143  " --outfile filename output formula to given file\n"
1144  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1145  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1146  "\n"
1147  "Other options:\n"
1148  " --version show version and exit\n"
1149  " --xml-ui use XML-formatted output\n"
1150  " --json-ui use JSON-formatted output\n"
1152  HELP_FLUSH
1153  " --verbosity # verbosity level\n"
1155  "\n";
1156  // clang-format on
1157 }
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:56
Remove Virtual Function (Method) Calls.
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:1202
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
#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
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 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:205
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:561
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)
#define HELP_GOTO_CHECK
Definition: goto_check.h:42
Unused function removal.
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:234
bool set(const cmdlinet &cmdline)
Definition: config.cpp:737
void add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler)
Definition: bmc.h:115
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
#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.
#define HELP_SHOW_PROPERTIES
#define MAX_NONDET_ARRAY_LENGTH_DEFAULT
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, remove_exceptions_typest type)
removes throws/CATCH-POP/CATCH-PUSH
#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
tvt java_enum_static_init_unwind_handler(const irep_idt &function_id, 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...
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:317
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)
void adjust_float_expressions(exprt &expr, const namespacet &ns)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
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.
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)
static irep_idt this_operating_system()
Definition: config.cpp:1309
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:231
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
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 MAX_NONDET_STRING_LENGTH
void label_properties(goto_modelt &goto_model)
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:1212
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)