cprover
goto_analyzer_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto-Analyser 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 <cpp/cpp_language.h>
22 #include <jsil/jsil_language.h>
23 
40 
42 
43 #include <langapi/mode.h>
44 
45 #include <util/language.h>
46 #include <util/options.h>
47 #include <util/config.h>
48 #include <util/string2int.h>
49 #include <util/unicode.h>
50 
51 #include <cbmc/version.h>
52 
53 #include "taint_analysis.h"
55 #include "static_analyzer.h"
56 
58  int argc,
59  const char **argv):
61  language_uit(cmdline, ui_message_handler),
62  ui_message_handler(cmdline, "GOTO-ANALYZER " CBMC_VERSION)
63 {
64 }
65 
67 {
72 }
73 
75 {
76  // this is our default verbosity
77  unsigned int v=messaget::M_STATISTICS;
78 
79  if(cmdline.isset("verbosity"))
80  {
82  if(v>10)
83  v=10;
84  }
85 
87 }
88 
90 {
91  if(config.set(cmdline))
92  {
93  usage_error();
94  exit(1);
95  }
96 
97  #if 0
98  if(cmdline.isset("c89"))
100 
101  if(cmdline.isset("c99"))
103 
104  if(cmdline.isset("c11"))
106 
107  if(cmdline.isset("cpp98"))
108  config.cpp.set_cpp98();
109 
110  if(cmdline.isset("cpp03"))
111  config.cpp.set_cpp03();
112 
113  if(cmdline.isset("cpp11"))
114  config.cpp.set_cpp11();
115  #endif
116 
117  #if 0
118  // check assertions
119  if(cmdline.isset("no-assertions"))
120  options.set_option("assertions", false);
121  else
122  options.set_option("assertions", true);
123 
124  // use assumptions
125  if(cmdline.isset("no-assumptions"))
126  options.set_option("assumptions", false);
127  else
128  options.set_option("assumptions", true);
129 
130  // magic error label
131  if(cmdline.isset("error-label"))
132  options.set_option("error-label", cmdline.get_values("error-label"));
133  #endif
134 }
135 
138 {
139  if(cmdline.isset("version"))
140  {
141  std::cout << CBMC_VERSION << '\n';
142  return 0;
143  }
144 
145  //
146  // command line options
147  //
148 
149  optionst options;
150  get_command_line_options(options);
151  eval_verbosity();
152 
153  //
154  // Print a banner
155  //
156  status() << "GOTO-ANALYSER version " CBMC_VERSION " "
157  << sizeof(void *)*8 << "-bit "
158  << config.this_architecture() << " "
160 
162 
164  return 6;
165 
166  if(process_goto_program(options))
167  return 6;
168 
169  if(cmdline.isset("taint"))
170  {
171  std::string taint_file=cmdline.get_value("taint");
172 
173  if(cmdline.isset("show-taint"))
174  {
175  taint_analysis(goto_model, taint_file, get_message_handler(), true, "");
176  return 0;
177  }
178  else
179  {
180  std::string json_file=cmdline.get_value("json");
181  bool result=
183  goto_model, taint_file, get_message_handler(), false, json_file);
184  return result?10:0;
185  }
186  }
187 
188  if(cmdline.isset("unreachable-instructions"))
189  {
190  const std::string json_file=cmdline.get_value("json");
191 
192  if(json_file.empty())
193  unreachable_instructions(goto_model, false, std::cout);
194  else if(json_file=="-")
195  unreachable_instructions(goto_model, true, std::cout);
196  else
197  {
198  std::ofstream ofs(json_file);
199  if(!ofs)
200  {
201  error() << "Failed to open json output `"
202  << json_file << "'" << eom;
203  return 6;
204  }
205 
207  }
208 
209  return 0;
210  }
211 
212  if(cmdline.isset("unreachable-functions"))
213  {
214  const std::string json_file=cmdline.get_value("json");
215 
216  if(json_file.empty())
217  unreachable_functions(goto_model, false, std::cout);
218  else if(json_file=="-")
219  unreachable_functions(goto_model, true, std::cout);
220  else
221  {
222  std::ofstream ofs(json_file);
223  if(!ofs)
224  {
225  error() << "Failed to open json output `"
226  << json_file << "'" << eom;
227  return 6;
228  }
229 
230  unreachable_functions(goto_model, true, ofs);
231  }
232 
233  return 0;
234  }
235 
236  if(cmdline.isset("reachable-functions"))
237  {
238  const std::string json_file=cmdline.get_value("json");
239 
240  if(json_file.empty())
241  reachable_functions(goto_model, false, std::cout);
242  else if(json_file=="-")
243  reachable_functions(goto_model, true, std::cout);
244  else
245  {
246  std::ofstream ofs(json_file);
247  if(!ofs)
248  {
249  error() << "Failed to open json output `"
250  << json_file << "'" << eom;
251  return 6;
252  }
253 
254  reachable_functions(goto_model, true, ofs);
255  }
256 
257  return 0;
258  }
259 
260  if(cmdline.isset("show-local-may-alias"))
261  {
263 
265  {
266  std::cout << ">>>>\n";
267  std::cout << ">>>> " << it->first << '\n';
268  std::cout << ">>>>\n";
269  local_may_aliast local_may_alias(it->second);
270  local_may_alias.output(std::cout, it->second, ns);
271  std::cout << '\n';
272  }
273 
274  return 0;
275  }
276 
278 
279  if(cmdline.isset("show-properties"))
280  {
282  return 0;
283  }
284 
285  if(set_properties())
286  return 7;
287 
288  if(cmdline.isset("show-intervals"))
289  {
290  show_intervals(goto_model, std::cout);
291  return 0;
292  }
293 
294  if(cmdline.isset("non-null") ||
295  cmdline.isset("intervals"))
296  {
297  optionst options;
298  options.set_option("json", cmdline.get_value("json"));
299  options.set_option("xml", cmdline.get_value("xml"));
300  bool result=
302  return result?10:0;
303  }
304 
305  error() << "no analysis option given -- consider reading --help"
306  << eom;
307  return 6;
308 }
309 
311 {
312  try
313  {
314  if(cmdline.isset("property"))
316  }
317 
318  catch(const char *e)
319  {
320  error() << e << eom;
321  return true;
322  }
323 
324  catch(const std::string e)
325  {
326  error() << e << eom;
327  return true;
328  }
329 
330  catch(int)
331  {
332  return true;
333  }
334 
335  return false;
336 }
337 
339  const optionst &options)
340 {
341  try
342  {
343  #if 0
344  // Remove inline assembler; this needs to happen before
345  // adding the library.
347 
348  // add the library
350  #endif
351 
352  // remove function pointers
353  status() << "Removing function pointers and virtual functions" << eom;
355  get_message_handler(), goto_model, cmdline.isset("pointer-check"));
356  // Java virtual functions -> explicit dispatch tables:
358  // remove Java throw and catch
360  // remove rtti
362 
363  // do partial inlining
364  status() << "Partial Inlining" << eom;
366 
367  // remove returns, gcc vectors, complex
371 
372  #if 0
373  // add generic checks
374  status() << "Generic Property Instrumentation" << eom;
375  goto_check(options, goto_model);
376  #endif
377 
378  // recalculate numbers, etc.
380 
381  // add loop ids
383 
384  // show it?
385  if(cmdline.isset("show-goto-functions"))
386  {
388  return true;
389  }
390 
391  // show it?
392  if(cmdline.isset("show-symbol-table"))
393  {
395  return true;
396  }
397  }
398 
399  catch(const char *e)
400  {
401  error() << e << eom;
402  return true;
403  }
404 
405  catch(const std::string e)
406  {
407  error() << e << eom;
408  return true;
409  }
410 
411  catch(int)
412  {
413  return true;
414  }
415 
416  catch(std::bad_alloc)
417  {
418  error() << "Out of memory" << eom;
419  return true;
420  }
421 
422  return false;
423 }
424 
427 {
428  std::cout <<
429  "\n"
430  "* * GOTO-ANALYSER " CBMC_VERSION " - Copyright (C) 2016 ";
431 
432  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
433 
434  std::cout << " * *\n";
435 
436  std::cout <<
437  "* * Daniel Kroening, DiffBlue * *\n"
438  "* * kroening@kroening.com * *\n"
439  "\n"
440  "Usage: Purpose:\n"
441  "\n"
442  " goto-analyzer [-h] [--help] show help\n"
443  " goto-analyzer file.c ... source file names\n"
444  "\n"
445  "Analyses:\n"
446  "\n"
447  // NOLINTNEXTLINE(whitespace/line_length)
448  " --taint file_name perform taint analysis using rules in given file\n"
449  " --unreachable-instructions list dead code\n"
450  // NOLINTNEXTLINE(whitespace/line_length)
451  " --unreachable-functions list functions unreachable from the entry point\n"
452  // NOLINTNEXTLINE(whitespace/line_length)
453  " --reachable-functions list functions reachable from the entry point\n"
454  " --intervals interval analysis\n"
455  " --non-null non-null analysis\n"
456  "\n"
457  "Analysis options:\n"
458  // NOLINTNEXTLINE(whitespace/line_length)
459  " --json file_name output results in JSON format to given file\n"
460  " --xml file_name output results in XML format to given file\n"
461  "\n"
462  "C/C++ frontend options:\n"
463  " -I path set include path (C/C++)\n"
464  " -D macro define preprocessor macro (C/C++)\n"
465  " --arch X set architecture (default: "
466  << configt::this_architecture() << ")\n"
467  " --os set operating system (default: "
468  << configt::this_operating_system() << ")\n"
469  " --c89/99/11 set C language standard (default: "
476  "c11":"") << ")\n"
477  " --cpp98/03/11 set C++ language standard (default: "
480  "cpp98":
483  "cpp03":
486  "cpp11":"") << ")\n"
487  #ifdef _WIN32
488  " --gcc use GCC as preprocessor\n"
489  #endif
490  " --no-library disable built-in abstract C library\n"
491  "\n"
492  "Java Bytecode frontend options:\n"
493  " --classpath dir/jar set the classpath\n"
494  " --main-class class-name set the name of the main class\n"
495  "\n"
496  "Program representations:\n"
497  " --show-parse-tree show parse tree\n"
498  " --show-symbol-table show symbol table\n"
500  // NOLINTNEXTLINE(whitespace/line_length)
501  " --show-properties show the properties, but don't run analysis\n"
502  "\n"
503  "Program instrumentation options:\n"
505  "\n"
506  "Other options:\n"
507  " --version show version and exit\n"
508  "\n";
509 }
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:90
mstreamt & result()
Definition: message.h:233
struct configt::ansi_ct ansi_c
Remove function exceptional returns.
Remove Instance-of Operators.
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
Definition: remove_asm.cpp:317
Remove Indirect Function Calls.
Remove Virtual Function (Method) Calls.
mstreamt & status()
Definition: message.h:238
goto_analyzer_parse_optionst(int argc, const char **argv)
void goto_check(const namespacet &ns, const optionst &options, goto_functionst::goto_functiont &goto_function)
uit get_ui()
Definition: language_ui.h:47
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
Show the symbol table.
languaget * new_ansi_c_language()
Read Goto Programs.
Remove the &#39;complex&#39; data type by compilation into structs.
Goto-Analyser Command Line Option Processing.
std::string get_value(char option) const
Definition: cmdline.cpp:46
void show_properties(const namespacet &ns, const irep_idt &identifier, ui_message_handlert::uit ui, const goto_programt &goto_program)
void set_cpp98()
Definition: config.h:128
virtual void show_symbol_table(bool brief=false)
symbol_tablet symbol_table
Definition: goto_model.h:25
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
configt config
Definition: config.cpp:21
Remove &#39;asm&#39; statements by compiling into suitable standard code.
void remove_exceptions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes throws/CATCH-POP/CATCH-PUSH
void remove_virtual_functions(const symbol_tablet &symbol_table, goto_functionst &goto_functions)
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Set the properties to check.
#define HELP_GOTO_CHECK
Definition: goto_check.h:41
bool set(const cmdlinet &cmdline)
Definition: config.cpp:727
void set_c89()
Definition: config.h:50
languaget * new_jsil_language()
bool taint_analysis(goto_modelt &goto_model, const std::string &taint_file_name, message_handlert &message_handler, bool show_full, const std::string &json_file_name)
virtual bool isset(char option) const
Definition: cmdline.cpp:30
void remove_instanceof(symbol_tablet &symbol_table, goto_functionst &goto_functions)
See function above.
Initialize a Goto Program.
void show_intervals(const goto_modelt &goto_model, std::ostream &out)
C++ Language Module.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Function Inlining.
Abstract interface to support a programming language.
virtual bool process_goto_program(const optionst &options)
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
languaget * new_cpp_language()
virtual void help() override
display command line help
Remove function returns.
#define GOTO_ANALYSER_OPTIONS
languaget * new_java_bytecode_language()
Jsil Language.
void set_c11()
Definition: config.h:52
static c_standardt default_c_standard()
Definition: config.cpp:645
virtual void get_command_line_options(optionst &options)
List all unreachable instructions.
static irep_idt this_operating_system()
Definition: config.cpp:1258
struct configt::cppt cpp
void set_c99()
Definition: config.h:51
message_handlert & get_message_handler()
Definition: message.h:127
void set_cpp11()
Definition: config.h:130
Goto Programs with Functions.
#define HELP_SHOW_GOTO_FUNCTIONS
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
bool static_analyzer(const goto_modelt &goto_model, const optionst &options, message_handlert &message_handler)
void remove_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
mstreamt & error()
Definition: message.h:223
Taint Analysis.
Remove the &#39;vector&#39; data type by compilation into arrays.
void set_verbosity(unsigned _verbosity)
Definition: message.h:44
#define CBMC_VERSION
Definition: version.h:4
Options.
virtual void usage_error()
Show the properties.
void register_language(language_factoryt factory)
Definition: mode.cpp:31
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
static void remove_complex(typet &)
removes complex data type
void show_goto_functions(const namespacet &ns, ui_message_handlert::uit ui, const goto_functionst &goto_functions)
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
#define forall_goto_functions(it, functions)
static cpp_standardt default_cpp_standard()
Definition: config.cpp:658
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
void set_cpp03()
Definition: config.h:129
void label_properties(goto_modelt &goto_model)
bool initialize_goto_model(goto_modelt &goto_model, const cmdlinet &cmdline, message_handlert &message_handler)
goto_functionst goto_functions
Definition: goto_model.h:26
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
Definition: config.cpp:1148
Field-insensitive, location-sensitive may-alias analysis.
virtual int doit() override
invoke main modules