cprover
goto_analyzer_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto-Analyzer Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <cstdlib> // exit()
15 #include <iostream>
16 #include <fstream>
17 #include <memory>
18 
19 #include <ansi-c/ansi_c_language.h>
20 #include <ansi-c/cprover_library.h>
21 
22 #include <assembler/remove_asm.h>
23 
24 #include <cpp/cpp_language.h>
25 #include <cpp/cprover_library.h>
26 
27 #include <jsil/jsil_language.h>
28 
41 
45 #include <analyses/goto_check.h>
47 #include <analyses/is_threaded.h>
55 
56 #include <langapi/mode.h>
57 #include <langapi/language.h>
58 
59 #include <util/config.h>
60 #include <util/exception_utils.h>
61 #include <util/exit_codes.h>
62 #include <util/options.h>
63 #include <util/unicode.h>
64 #include <util/version.h>
65 
66 #include "show_on_source.h"
67 #include "static_show_domain.h"
68 #include "static_simplifier.h"
69 #include "static_verifier.h"
70 #include "taint_analysis.h"
72 
73 void vsd_options(optionst &options, const cmdlinet &cmdline);
74 
76  int argc,
77  const char **argv)
80  argc,
81  argv,
82  std::string("GOTO-ANALYZER "))
83 {
84 }
85 
87 {
91 }
92 
94 {
95  if(config.set(cmdline))
96  {
97  usage_error();
99  }
100 
101  if(cmdline.isset("function"))
102  options.set_option("function", cmdline.get_value("function"));
103 
104  // all checks supported by goto_check
106 
107  // The user should either select:
108  // 1. a specific analysis, or
109  // 2. a tuple of task / analyser options / outputs
110 
111  // Select a specific analysis
112  if(cmdline.isset("taint"))
113  {
114  options.set_option("taint", true);
115  options.set_option("specific-analysis", true);
116  }
117  // For backwards compatibility,
118  // these are first recognised as specific analyses
119  bool reachability_task = false;
120  if(cmdline.isset("unreachable-instructions"))
121  {
122  options.set_option("unreachable-instructions", true);
123  options.set_option("specific-analysis", true);
124  reachability_task = true;
125  }
126  if(cmdline.isset("unreachable-functions"))
127  {
128  options.set_option("unreachable-functions", true);
129  options.set_option("specific-analysis", true);
130  reachability_task = true;
131  }
132  if(cmdline.isset("reachable-functions"))
133  {
134  options.set_option("reachable-functions", true);
135  options.set_option("specific-analysis", true);
136  reachability_task = true;
137  }
138  if(cmdline.isset("show-local-may-alias"))
139  {
140  options.set_option("show-local-may-alias", true);
141  options.set_option("specific-analysis", true);
142  }
143 
144  // Output format choice
145  if(cmdline.isset("text"))
146  {
147  options.set_option("text", true);
148  options.set_option("outfile", cmdline.get_value("text"));
149  }
150  else if(cmdline.isset("json"))
151  {
152  options.set_option("json", true);
153  options.set_option("outfile", cmdline.get_value("json"));
154  }
155  else if(cmdline.isset("xml"))
156  {
157  options.set_option("xml", true);
158  options.set_option("outfile", cmdline.get_value("xml"));
159  }
160  else if(cmdline.isset("dot"))
161  {
162  options.set_option("dot", true);
163  options.set_option("outfile", cmdline.get_value("dot"));
164  }
165 
166  // Task options
167  if(cmdline.isset("show"))
168  {
169  options.set_option("show", true);
170  options.set_option("general-analysis", true);
171  }
172  else if(cmdline.isset("show-on-source"))
173  {
174  options.set_option("show-on-source", true);
175  options.set_option("general-analysis", true);
176  }
177  else if(cmdline.isset("verify"))
178  {
179  options.set_option("verify", true);
180  options.set_option("general-analysis", true);
181  }
182  else if(cmdline.isset("simplify"))
183  {
184  if(cmdline.get_value("simplify") == "-")
186  "cannot output goto binary to stdout", "--simplify");
187 
188  options.set_option("simplify", true);
189  options.set_option("outfile", cmdline.get_value("simplify"));
190  options.set_option("general-analysis", true);
191 
192  // For development allow slicing to be disabled in the simplify task
193  options.set_option(
194  "simplify-slicing",
195  !(cmdline.isset("no-simplify-slicing")));
196  }
197  else if(cmdline.isset("show-intervals"))
198  {
199  // For backwards compatibility
200  options.set_option("show", true);
201  options.set_option("general-analysis", true);
202  options.set_option("intervals", true);
203  options.set_option("domain set", true);
204  }
205  else if(cmdline.isset("show-non-null"))
206  {
207  // For backwards compatibility
208  options.set_option("show", true);
209  options.set_option("general-analysis", true);
210  options.set_option("non-null", true);
211  options.set_option("domain set", true);
212  }
213  else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
214  {
215  // Partial backwards compatability, just giving these domains without
216  // a task will work. However it will use the general default of verify
217  // rather than their historical default of show.
218  options.set_option("verify", true);
219  options.set_option("general-analysis", true);
220  }
221 
222  if(options.get_bool_option("general-analysis") || reachability_task)
223  {
224  // Abstract interpreter choice
225  if(cmdline.isset("recursive-interprocedural"))
226  options.set_option("recursive-interprocedural", true);
227  else if(cmdline.isset("three-way-merge"))
228  options.set_option("three-way-merge", true);
229  else if(cmdline.isset("legacy-ait") || cmdline.isset("location-sensitive"))
230  {
231  options.set_option("legacy-ait", true);
232  // Fixes a number of other options as well
233  options.set_option("ahistorical", true);
234  options.set_option("history set", true);
235  options.set_option("one-domain-per-location", true);
236  options.set_option("storage set", true);
237  }
238  else if(cmdline.isset("legacy-concurrent") || cmdline.isset("concurrent"))
239  {
240  options.set_option("legacy-concurrent", true);
241  options.set_option("ahistorical", true);
242  options.set_option("history set", true);
243  options.set_option("one-domain-per-location", true);
244  options.set_option("storage set", true);
245  }
246  else
247  {
248  // Silently default to legacy-ait for backwards compatability
249  options.set_option("legacy-ait", true);
250  // Fixes a number of other options as well
251  options.set_option("ahistorical", true);
252  options.set_option("history set", true);
253  options.set_option("one-domain-per-location", true);
254  options.set_option("storage set", true);
255  }
256 
257  // History choice
258  if(cmdline.isset("ahistorical"))
259  {
260  options.set_option("ahistorical", true);
261  options.set_option("history set", true);
262  }
263  else if(cmdline.isset("call-stack"))
264  {
265  options.set_option("call-stack", true);
266  options.set_option(
267  "call-stack-recursion-limit", cmdline.get_value("call-stack"));
268  options.set_option("history set", true);
269  }
270  else if(cmdline.isset("loop-unwind"))
271  {
272  options.set_option("local-control-flow-history", true);
273  options.set_option("local-control-flow-history-forward", false);
274  options.set_option("local-control-flow-history-backward", true);
275  options.set_option(
276  "local-control-flow-history-limit", cmdline.get_value("loop-unwind"));
277  options.set_option("history set", true);
278  }
279  else if(cmdline.isset("branching"))
280  {
281  options.set_option("local-control-flow-history", true);
282  options.set_option("local-control-flow-history-forward", true);
283  options.set_option("local-control-flow-history-backward", false);
284  options.set_option(
285  "local-control-flow-history-limit", cmdline.get_value("branching"));
286  options.set_option("history set", true);
287  }
288  else if(cmdline.isset("loop-unwind-and-branching"))
289  {
290  options.set_option("local-control-flow-history", true);
291  options.set_option("local-control-flow-history-forward", true);
292  options.set_option("local-control-flow-history-backward", true);
293  options.set_option(
294  "local-control-flow-history-limit",
295  cmdline.get_value("loop-unwind-and-branching"));
296  options.set_option("history set", true);
297  }
298 
299  if(!options.get_bool_option("history set"))
300  {
301  // Default to ahistorical as it is the expected for of analysis
302  log.status() << "History not specified, defaulting to --ahistorical"
303  << messaget::eom;
304  options.set_option("ahistorical", true);
305  options.set_option("history set", true);
306  }
307 
308  // Domain choice
309  if(cmdline.isset("constants"))
310  {
311  options.set_option("constants", true);
312  options.set_option("domain set", true);
313  }
314  else if(cmdline.isset("dependence-graph"))
315  {
316  options.set_option("dependence-graph", true);
317  options.set_option("domain set", true);
318  }
319  else if(cmdline.isset("intervals"))
320  {
321  options.set_option("intervals", true);
322  options.set_option("domain set", true);
323  }
324  else if(cmdline.isset("non-null"))
325  {
326  options.set_option("non-null", true);
327  options.set_option("domain set", true);
328  }
329  else if(cmdline.isset("vsd") || cmdline.isset("variable-sensitivity"))
330  {
331  options.set_option("vsd", true);
332  options.set_option(
333  "data-dependencies", cmdline.isset("vsd-data-dependencies"));
334 
335  vsd_options(options, cmdline);
336  }
337  else if(cmdline.isset("dependence-graph-vs"))
338  {
339  options.set_option("dependence-graph-vs", true);
340  options.set_option("data-dependencies", true);
341 
342  vsd_options(options, cmdline);
343  }
344 
345  // Reachability questions, when given with a domain swap from specific
346  // to general tasks so that they can use the domain & parameterisations.
347  if(reachability_task)
348  {
349  if(options.get_bool_option("domain set"))
350  {
351  options.set_option("specific-analysis", false);
352  options.set_option("general-analysis", true);
353  }
354  }
355  else
356  {
357  if(!options.get_bool_option("domain set"))
358  {
359  // Default to constants as it is light-weight but useful
360  log.status() << "Domain not specified, defaulting to --constants"
361  << messaget::eom;
362  options.set_option("constants", true);
363  }
364  }
365  }
366 
367  // Storage choice
368  if(cmdline.isset("one-domain-per-history"))
369  {
370  options.set_option("one-domain-per-history", true);
371  options.set_option("storage set", true);
372  }
373  else if(cmdline.isset("one-domain-per-location"))
374  {
375  options.set_option("one-domain-per-location", true);
376  options.set_option("storage set", true);
377  }
378 
379  if(!options.get_bool_option("storage set"))
380  {
381  // one-domain-per-location and one-domain-per-history are effectively
382  // the same when using ahistorical so we default to per-history so that
383  // more sophisticated history objects work as expected
384  log.status() << "Storage not specified,"
385  << " defaulting to --one-domain-per-history" << messaget::eom;
386  options.set_option("one-domain-per-history", true);
387  options.set_option("storage set", true);
388  }
389 
390  if(cmdline.isset("validate-goto-model"))
391  {
392  options.set_option("validate-goto-model", true);
393  }
394 }
395 
400  const optionst &options,
401  const namespacet &ns)
402 {
403  auto vsd_config = vsd_configt::from_options(options);
404  auto vs_object_factory =
406 
407  // These support all of the option categories
408  if(
409  options.get_bool_option("recursive-interprocedural") ||
410  options.get_bool_option("three-way-merge"))
411  {
412  // Build the history factory
413  std::unique_ptr<ai_history_factory_baset> hf = nullptr;
414  if(options.get_bool_option("ahistorical"))
415  {
416  hf = util_make_unique<
418  }
419  else if(options.get_bool_option("call-stack"))
420  {
421  hf = util_make_unique<call_stack_history_factoryt>(
422  options.get_unsigned_int_option("call-stack-recursion-limit"));
423  }
424  else if(options.get_bool_option("local-control-flow-history"))
425  {
426  hf = util_make_unique<local_control_flow_history_factoryt>(
427  options.get_bool_option("local-control-flow-history-forward"),
428  options.get_bool_option("local-control-flow-history-backward"),
429  options.get_unsigned_int_option("local-control-flow-history-limit"));
430  }
431 
432  // Build the domain factory
433  std::unique_ptr<ai_domain_factory_baset> df = nullptr;
434  if(options.get_bool_option("constants"))
435  {
436  df = util_make_unique<
438  }
439  else if(options.get_bool_option("intervals"))
440  {
441  df = util_make_unique<
443  }
444  else if(options.get_bool_option("vsd"))
445  {
446  df = util_make_unique<variable_sensitivity_domain_factoryt>(
447  vs_object_factory, vsd_config);
448  }
449  // non-null is not fully supported, despite the historical options
450  // dependency-graph is quite heavily tied to the legacy-ait infrastructure
451  // dependency-graph-vs is very similar to dependency-graph
452 
453  // Build the storage object
454  std::unique_ptr<ai_storage_baset> st = nullptr;
455  if(options.get_bool_option("one-domain-per-history"))
456  {
457  st = util_make_unique<history_sensitive_storaget>();
458  }
459  else if(options.get_bool_option("one-domain-per-location"))
460  {
461  st = util_make_unique<location_sensitive_storaget>();
462  }
463 
464  // Only try to build the abstract interpreter if all the parts have been
465  // correctly specified and configured
466  if(hf != nullptr && df != nullptr && st != nullptr)
467  {
468  if(options.get_bool_option("recursive-interprocedural"))
469  {
471  std::move(hf), std::move(df), std::move(st));
472  }
473  else if(options.get_bool_option("three-way-merge"))
474  {
475  // Only works with VSD
476  if(options.get_bool_option("vsd"))
477  {
478  return new ai_three_way_merget(
479  std::move(hf), std::move(df), std::move(st));
480  }
481  }
482  }
483  }
484  else if(options.get_bool_option("legacy-ait"))
485  {
486  if(options.get_bool_option("constants"))
487  {
488  // constant_propagator_ait derives from ait<constant_propagator_domaint>
490  }
491  else if(options.get_bool_option("dependence-graph"))
492  {
493  return new dependence_grapht(ns);
494  }
495  else if(options.get_bool_option("dependence-graph-vs"))
496  {
498  goto_model.goto_functions, ns, vs_object_factory, vsd_config);
499  }
500  else if(options.get_bool_option("vsd"))
501  {
502  auto df = util_make_unique<variable_sensitivity_domain_factoryt>(
503  vs_object_factory, vsd_config);
504  return new ait<variable_sensitivity_domaint>(std::move(df));
505  }
506  else if(options.get_bool_option("intervals"))
507  {
508  return new ait<interval_domaint>();
509  }
510 #if 0
511  // Not actually implemented, despite the option...
512  else if(options.get_bool_option("non-null"))
513  {
514  return new ait<non_null_domaint>();
515  }
516 #endif
517  }
518  else if(options.get_bool_option("legacy-concurrent"))
519  {
520 #if 0
521  // Very few domains can work with this interpreter
522  // as it requires that changes to the domain are
523  // 'non-revertable' and it has merge shared
524  if(options.get_bool_option("dependence-graph"))
525  {
526  return new dependence_grapht(ns);
527  }
528 #endif
529  }
530 
531  // Construction failed due to configuration errors
532  return nullptr;
533 }
534 
537 {
538  if(cmdline.isset("version"))
539  {
540  std::cout << CBMC_VERSION << '\n';
541  return CPROVER_EXIT_SUCCESS;
542  }
543 
544  //
545  // command line options
546  //
547 
548  optionst options;
549  get_command_line_options(options);
552 
553  //
554  // Print a banner
555  //
556  log.status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
557  << sizeof(void *) * 8 << "-bit " << config.this_architecture()
559 
561 
563 
564  // Preserve backwards compatibility in processing
565  options.set_option("partial-inline", true);
566  options.set_option("rewrite-union", false);
567 
568  if(process_goto_program(options))
570 
571  if(cmdline.isset("validate-goto-model"))
572  {
574  }
575 
576  // show it?
577  if(cmdline.isset("show-symbol-table"))
578  {
580  return CPROVER_EXIT_SUCCESS;
581  }
582 
583  // show it?
584  if(
585  cmdline.isset("show-goto-functions") ||
586  cmdline.isset("list-goto-functions"))
587  {
589  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
590  return CPROVER_EXIT_SUCCESS;
591  }
592 
593  return perform_analysis(options);
594 }
595 
598 {
599  if(options.get_bool_option("taint"))
600  {
601  std::string taint_file=cmdline.get_value("taint");
602 
603  if(cmdline.isset("show-taint"))
604  {
605  taint_analysis(goto_model, taint_file, ui_message_handler, true);
606  return CPROVER_EXIT_SUCCESS;
607  }
608  else
609  {
610  std::string json_file=cmdline.get_value("json");
611  bool result = taint_analysis(
612  goto_model, taint_file, ui_message_handler, false, json_file);
614  }
615  }
616 
617  // If no domain is given, this lightweight version of the analysis is used.
618  if(options.get_bool_option("unreachable-instructions") &&
619  options.get_bool_option("specific-analysis"))
620  {
621  const std::string json_file=cmdline.get_value("json");
622 
623  if(json_file.empty())
624  unreachable_instructions(goto_model, false, std::cout);
625  else if(json_file=="-")
626  unreachable_instructions(goto_model, true, std::cout);
627  else
628  {
629  std::ofstream ofs(json_file);
630  if(!ofs)
631  {
632  log.error() << "Failed to open json output '" << json_file << "'"
633  << messaget::eom;
635  }
636 
638  }
639 
640  return CPROVER_EXIT_SUCCESS;
641  }
642 
643  if(options.get_bool_option("unreachable-functions") &&
644  options.get_bool_option("specific-analysis"))
645  {
646  const std::string json_file=cmdline.get_value("json");
647 
648  if(json_file.empty())
649  unreachable_functions(goto_model, false, std::cout);
650  else if(json_file=="-")
651  unreachable_functions(goto_model, true, std::cout);
652  else
653  {
654  std::ofstream ofs(json_file);
655  if(!ofs)
656  {
657  log.error() << "Failed to open json output '" << json_file << "'"
658  << messaget::eom;
660  }
661 
662  unreachable_functions(goto_model, true, ofs);
663  }
664 
665  return CPROVER_EXIT_SUCCESS;
666  }
667 
668  if(options.get_bool_option("reachable-functions") &&
669  options.get_bool_option("specific-analysis"))
670  {
671  const std::string json_file=cmdline.get_value("json");
672 
673  if(json_file.empty())
674  reachable_functions(goto_model, false, std::cout);
675  else if(json_file=="-")
676  reachable_functions(goto_model, true, std::cout);
677  else
678  {
679  std::ofstream ofs(json_file);
680  if(!ofs)
681  {
682  log.error() << "Failed to open json output '" << json_file << "'"
683  << messaget::eom;
685  }
686 
687  reachable_functions(goto_model, true, ofs);
688  }
689 
690  return CPROVER_EXIT_SUCCESS;
691  }
692 
693  if(options.get_bool_option("show-local-may-alias"))
694  {
696 
697  for(const auto &gf_entry : goto_model.goto_functions.function_map)
698  {
699  std::cout << ">>>>\n";
700  std::cout << ">>>> " << gf_entry.first << '\n';
701  std::cout << ">>>>\n";
702  local_may_aliast local_may_alias(gf_entry.second);
703  local_may_alias.output(std::cout, gf_entry.second, ns);
704  std::cout << '\n';
705  }
706 
707  return CPROVER_EXIT_SUCCESS;
708  }
709 
711 
712  if(cmdline.isset("show-properties"))
713  {
715  return CPROVER_EXIT_SUCCESS;
716  }
717 
718  if(cmdline.isset("property"))
720 
721  if(options.get_bool_option("general-analysis"))
722  {
723  // Output file factory
724  const std::string outfile=options.get_option("outfile");
725 
726  std::ofstream output_stream;
727  if(outfile != "-" && !outfile.empty())
728  output_stream.open(outfile);
729 
730  std::ostream &out(
731  (outfile == "-" || outfile.empty()) ? std::cout : output_stream);
732 
733  if(!out)
734  {
735  log.error() << "Failed to open output file '" << outfile << "'"
736  << messaget::eom;
738  }
739 
740  // Build analyzer
741  log.status() << "Selecting abstract domain" << messaget::eom;
742  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
743  std::unique_ptr<ai_baset> analyzer;
744 
745  try
746  {
747  analyzer.reset(build_analyzer(options, ns));
748  }
750  {
751  log.error() << e.what() << messaget::eom;
753  }
754 
755  if(analyzer == nullptr)
756  {
757  log.status() << "Task / Interpreter combination not supported"
758  << messaget::eom;
760  }
761 
762  // Run
763  log.status() << "Computing abstract states" << messaget::eom;
764  (*analyzer)(goto_model);
765 
766  // Perform the task
767  log.status() << "Performing task" << messaget::eom;
768 
769  bool result = true;
770 
771  if(options.get_bool_option("show"))
772  {
773  static_show_domain(goto_model, *analyzer, options, out);
774  return CPROVER_EXIT_SUCCESS;
775  }
776  else if(options.get_bool_option("show-on-source"))
777  {
779  return CPROVER_EXIT_SUCCESS;
780  }
781  else if(options.get_bool_option("verify"))
782  {
783  result = static_verifier(
784  goto_model, *analyzer, options, ui_message_handler, out);
785  }
786  else if(options.get_bool_option("simplify"))
787  {
788  PRECONDITION(!outfile.empty() && outfile != "-");
789  output_stream.close();
790  output_stream.open(outfile, std::ios::binary);
791  result = static_simplifier(
792  goto_model, *analyzer, options, ui_message_handler, out);
793  }
794  else if(options.get_bool_option("unreachable-instructions"))
795  {
797  *analyzer,
798  options,
799  out);
800  }
801  else if(options.get_bool_option("unreachable-functions"))
802  {
804  *analyzer,
805  options,
806  out);
807  }
808  else if(options.get_bool_option("reachable-functions"))
809  {
811  *analyzer,
812  options,
813  out);
814  }
815  else
816  {
817  log.error() << "Unhandled task" << messaget::eom;
819  }
820 
821  return result ?
823  }
824 
825  // Final defensive error case
826  log.error() << "no analysis option given -- consider reading --help"
827  << messaget::eom;
829 }
830 
832  const optionst &options)
833 {
834  // Remove inline assembler; this needs to happen before
835  // adding the library.
837 
838  // add the library
839  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
840  << messaget::eom;
843 
845 
846  // Common removal of types and complex constructs
847  if(::process_goto_program(goto_model, options, log))
848  return true;
849 
850  return false;
851 }
852 
855 {
856  // clang-format off
857  std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
858  << align_center_with_border("Copyright (C) 2017-2018") << '\n'
859  << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
860  << align_center_with_border("kroening@kroening.com") << '\n'
861  <<
862  "\n"
863  "Usage: Purpose:\n"
864  "\n"
865  " goto-analyzer [-h] [--help] show help\n"
866  " goto-analyzer file.c ... source file names\n"
867  "\n"
868  "Task options:\n"
869  " --show display the abstract states on the goto program\n" // NOLINT(*)
870  " --show-on-source display the abstract states on the source\n"
871  // NOLINTNEXTLINE(whitespace/line_length)
872  " --verify use the abstract domains to check assertions\n"
873  // NOLINTNEXTLINE(whitespace/line_length)
874  " --simplify file_name use the abstract domains to simplify the program\n"
875  " --unreachable-instructions list dead code\n"
876  // NOLINTNEXTLINE(whitespace/line_length)
877  " --unreachable-functions list functions unreachable from the entry point\n"
878  // NOLINTNEXTLINE(whitespace/line_length)
879  " --reachable-functions list functions reachable from the entry point\n"
880  "\n"
881  "Abstract interpreter options:\n"
882  // NOLINTNEXTLINE(whitespace/line_length)
883  " --recursive-interprocedural use recursion to handle interprocedural reasoning\n"
884  // NOLINTNEXTLINE(whitespace/line_length)
885  " --three-way-merge use VSD's three-way merge on return from function call\n"
886  // NOLINTNEXTLINE(whitespace/line_length)
887  " --legacy-ait recursion for function and one domain per location\n"
888  // NOLINTNEXTLINE(whitespace/line_length)
889  " --legacy-concurrent legacy-ait with an extended fixed-point for concurrency\n"
890  "\n"
891  "History options:\n"
892  // NOLINTNEXTLINE(whitespace/line_length)
893  " --ahistorical the most basic history, tracks locations only\n"
894  // NOLINTNEXTLINE(whitespace/line_length)
895  " --call-stack n track the calling location stack for each function\n"
896  // NOLINTNEXTLINE(whitespace/line_length)
897  " limiting to at most n recursive loops, 0 to disable\n"
898  // NOLINTNEXTLINE(whitespace/line_length)
899  " --loop-unwind n track the number of loop iterations within a function\n"
900  // NOLINTNEXTLINE(whitespace/line_length)
901  " limited to n histories per location, 0 is unlimited\n"
902  // NOLINTNEXTLINE(whitespace/line_length)
903  " --branching n track the forwards jumps (if, switch, etc.) within a function\n"
904  // NOLINTNEXTLINE(whitespace/line_length)
905  " limited to n histories per location, 0 is unlimited\n"
906  // NOLINTNEXTLINE(whitespace/line_length)
907  " --loop-unwind-and-branching n track all local control flow\n"
908  // NOLINTNEXTLINE(whitespace/line_length)
909  " limited to n histories per location, 0 is unlimited\n"
910  "\n"
911  "Domain options:\n"
912  " --constants a constant for each variable if possible\n"
913  " --intervals an interval for each variable\n"
914  " --non-null tracks which pointers are non-null\n"
915  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
916  " --vsd a configurable non-relational domain\n" // NOLINT(*)
917  " --dependence-graph-vs dependencies between instructions using VSD\n" // NOLINT(*)
918  "\n"
919  "Variable sensitivity domain (VSD) options:\n"
920  " --vsd-values value tracking - constants|intervals|set-of-constants\n"
921  " --vsd-structs struct field sensitive analysis - top-bottom|every-field\n"
922  " --vsd-arrays array entry sensitive analysis - top-bottom|every-element\n"
923  " --vsd-pointers pointer sensitive analysis - top-bottom|constants|value-set\n"
924  " --vsd-unions union sensitive analysis - top-bottom\n"
925  " --vsd-flow-insensitive disables flow sensitivity\n"
926  " --vsd-data-dependencies track data dependencies\n"
927  "\n"
928  "Storage options:\n"
929  // NOLINTNEXTLINE(whitespace/line_length)
930  " --one-domain-per-history stores a domain for each history object created\n"
931  " --one-domain-per-location stores a domain for each location reached\n"
932  "\n"
933  "Output options:\n"
934  " --text file_name output results in plain text to given file\n"
935  // NOLINTNEXTLINE(whitespace/line_length)
936  " --json file_name output results in JSON format to given file\n"
937  " --xml file_name output results in XML format to given file\n"
938  " --dot file_name output results in DOT format to given file\n"
939  "\n"
940  "Specific analyses:\n"
941  // NOLINTNEXTLINE(whitespace/line_length)
942  " --taint file_name perform taint analysis using rules in given file\n"
943  "\n"
944  "C/C++ frontend options:\n"
947  "\n"
948  "Platform options:\n"
950  "\n"
951  "Program representations:\n"
952  " --show-parse-tree show parse tree\n"
953  " --show-symbol-table show loaded symbol table\n"
956  "\n"
957  "Program instrumentation options:\n"
960  "\n"
961  "Other options:\n"
963  " --version show version and exit\n"
964  HELP_FLUSH
966  "\n";
967  // clang-format on
968 }
969 
970 void vsd_options(optionst &options, const cmdlinet &cmdline)
971 {
972  options.set_option("domain set", true);
973 
974  // Configuration of VSD
975  options.set_option("values", cmdline.get_value("vsd-values"));
976  options.set_option("pointers", cmdline.get_value("vsd-pointers"));
977  options.set_option("arrays", cmdline.get_value("vsd-arrays"));
978  options.set_option("structs", cmdline.get_value("vsd-structs"));
979  options.set_option("unions", cmdline.get_value("vsd-unions"));
980  options.set_option("flow-insensitive", cmdline.isset("vsd-flow-insensitive"));
981 }
void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
Some variables have different initial values based on what flags are being passed to cbmc; since the ...
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
std::unique_ptr< languaget > new_ansi_c_language()
History for tracking the call stack and performing interprocedural analysis.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
An easy factory implementation for histories that don't need parameters.
Definition: ai_history.h:255
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:559
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
static irep_idt this_architecture()
Definition: config.cpp:1326
static irep_idt this_operating_system()
Definition: config.cpp:1426
struct configt::ansi_ct ansi_c
virtual int doit() override
invoke main modules
ai_baset * build_analyzer(const optionst &, const namespacet &ns)
For the task, build the appropriate kind of analyzer Ideally this should be a pure function of option...
virtual void get_command_line_options(optionst &options)
goto_analyzer_parse_optionst(int argc, const char **argv)
virtual bool process_goto_program(const optionst &options)
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
virtual void help() override
display command line help
function_mapt function_map
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
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
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 ...
std::string what() const override
A human readable description of what went wrong.
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition: message.cpp:104
mstreamt & error() const
Definition: message.h:399
mstreamt & status() const
Definition: message.h:414
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:56
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
virtual void usage_error()
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
static variable_sensitivity_object_factory_ptrt configured_with(const vsd_configt &options)
configt config
Definition: config.cpp:24
#define HELP_CONFIG_LIBRARY
Definition: config.h:64
#define HELP_CONFIG_PLATFORM
Definition: config.h:83
#define HELP_CONFIG_C_CPP
Definition: config.h:35
Constant propagation.
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
std::unique_ptr< languaget > new_cpp_language()
C++ Language Module.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
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_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
Definition: exit_codes.h:21
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
Definition: exit_codes.h:25
#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 vsd_options(optionst &options, const cmdlinet &cmdline)
Goto-Analyser Command Line Option Processing.
#define GOTO_ANALYSER_OPTIONS
Program Transformation.
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:71
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
Goto Programs with Functions.
Function Inlining.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
Interval Domain.
Over-approximate Concurrency for Threaded Goto Programs.
std::unique_ptr< languaget > new_jsil_language()
Jsil Language.
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:205
Abstract interface to support a programming language.
Track function-local control flow for loop unwinding and path senstivity.
Field-insensitive, location-sensitive may-alias analysis.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
Definition: mode.cpp:38
Options.
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)
Read Goto Programs.
#define HELP_FUNCTIONS
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Definition: remove_asm.cpp:511
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
Functions for replacing virtual function call with a static function calls in functions,...
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)
#define HELP_SHOW_GOTO_FUNCTIONS
void show_on_source(const std::string &source_file, const goto_modelt &goto_model, const ai_baset &ai, message_handlert &message_handler)
output source code annotated with abstract states for given file
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)
Show the symbol table.
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
void static_show_domain(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Runs the analyzer and then prints out the domain.
bool static_simplifier(goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Simplifies the program using the information in the abstract domain.
void static_verifier(const abstract_goto_modelt &abstract_goto_model, const ai_baset &ai, propertiest &properties)
Use the information from the abstract interpreter to fill out the statuses of the passed properties.
irep_idt arch
Definition: config.h:165
static vsd_configt from_options(const optionst &options)
bool taint_analysis(goto_modelt &goto_model, const std::string &taint_file_name, message_handlert &message_handler, bool show_full, const optionalt< std::string > &json_file_name)
Taint Analysis.
An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivit...
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:106
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
List all unreachable instructions.
#define HELP_VALIDATE
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...
A forked and modified version of analyses/dependence_graph.
There are different ways of handling arrays, structures, unions and pointers.
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...
const char * CBMC_VERSION