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