cprover
goto_diff_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: GOTO-DIFF Command Line Option Processing
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <fstream>
15 #include <cstdlib> // exit()
16 #include <iostream>
17 #include <memory>
18 
19 #include <util/string2int.h>
20 #include <util/config.h>
21 #include <util/language.h>
22 #include <util/options.h>
23 
37 #include <goto-programs/loop_ids.h>
39 
41 
42 #include <langapi/mode.h>
43 
44 #include <cbmc/version.h>
45 
46 #include "goto_diff.h"
47 #include "syntactic_diff.h"
48 #include "unified_diff.h"
49 #include "change_impact.h"
50 
53  goto_diff_languagest(cmdline, ui_message_handler),
54  ui_message_handler(cmdline, "GOTO-DIFF " CBMC_VERSION),
55  languages2(cmdline, ui_message_handler)
56 {
57 }
58 
60  int argc,
61  const char **argv,
62  const std::string &extra_options):
63  parse_options_baset(GOTO_DIFF_OPTIONS+extra_options, argc, argv),
64  goto_diff_languagest(cmdline, ui_message_handler),
65  ui_message_handler(cmdline, "GOTO-DIFF " CBMC_VERSION),
66  languages2(cmdline, ui_message_handler)
67 {
68 }
69 
71 {
72  // this is our default verbosity
73  unsigned int v=messaget::M_STATISTICS;
74 
75  if(cmdline.isset("verbosity"))
76  {
78  if(v>10)
79  v=10;
80  }
81 
83 }
84 
86 {
87  if(config.set(cmdline))
88  {
89  usage_error();
90  exit(1);
91  }
92 
93  if(cmdline.isset("program-only"))
94  options.set_option("program-only", true);
95 
96  if(cmdline.isset("show-vcc"))
97  options.set_option("show-vcc", true);
98 
99  if(cmdline.isset("cover"))
100  options.set_option("cover", cmdline.get_value("cover"));
101 
102  if(cmdline.isset("mm"))
103  options.set_option("mm", cmdline.get_value("mm"));
104 
105  if(cmdline.isset("c89"))
107 
108  if(cmdline.isset("c99"))
110 
111  if(cmdline.isset("c11"))
113 
114  if(cmdline.isset("cpp98"))
115  config.cpp.set_cpp98();
116 
117  if(cmdline.isset("cpp03"))
118  config.cpp.set_cpp03();
119 
120  if(cmdline.isset("cpp11"))
121  config.cpp.set_cpp11();
122 
123  if(cmdline.isset("no-simplify"))
124  options.set_option("simplify", false);
125  else
126  options.set_option("simplify", true);
127 
128  if(cmdline.isset("all-claims") || // will go away
129  cmdline.isset("all-properties")) // use this one
130  options.set_option("all-properties", true);
131  else
132  options.set_option("all-properties", false);
133 
134  if(cmdline.isset("unwind"))
135  options.set_option("unwind", cmdline.get_value("unwind"));
136 
137  if(cmdline.isset("depth"))
138  options.set_option("depth", cmdline.get_value("depth"));
139 
140  if(cmdline.isset("debug-level"))
141  options.set_option("debug-level", cmdline.get_value("debug-level"));
142 
143  if(cmdline.isset("slice-by-trace"))
144  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
145 
146  if(cmdline.isset("unwindset"))
147  options.set_option("unwindset", cmdline.get_value("unwindset"));
148 
149  // constant propagation
150  if(cmdline.isset("no-propagation"))
151  options.set_option("propagation", false);
152  else
153  options.set_option("propagation", true);
154 
155  // check array bounds
156  if(cmdline.isset("bounds-check"))
157  options.set_option("bounds-check", true);
158  else
159  options.set_option("bounds-check", false);
160 
161  // check division by zero
162  if(cmdline.isset("div-by-zero-check"))
163  options.set_option("div-by-zero-check", true);
164  else
165  options.set_option("div-by-zero-check", false);
166 
167  // check overflow/underflow
168  if(cmdline.isset("signed-overflow-check"))
169  options.set_option("signed-overflow-check", true);
170  else
171  options.set_option("signed-overflow-check", false);
172 
173  // check overflow/underflow
174  if(cmdline.isset("unsigned-overflow-check"))
175  options.set_option("unsigned-overflow-check", true);
176  else
177  options.set_option("unsigned-overflow-check", false);
178 
179  // check overflow/underflow
180  if(cmdline.isset("float-overflow-check"))
181  options.set_option("float-overflow-check", true);
182  else
183  options.set_option("float-overflow-check", false);
184 
185  // check for NaN (not a number)
186  if(cmdline.isset("nan-check"))
187  options.set_option("nan-check", true);
188  else
189  options.set_option("nan-check", false);
190 
191  // check pointers
192  if(cmdline.isset("pointer-check"))
193  options.set_option("pointer-check", true);
194  else
195  options.set_option("pointer-check", false);
196 
197  // check for memory leaks
198  if(cmdline.isset("memory-leak-check"))
199  options.set_option("memory-leak-check", true);
200  else
201  options.set_option("memory-leak-check", false);
202 
203  // check assertions
204  if(cmdline.isset("no-assertions"))
205  options.set_option("assertions", false);
206  else
207  options.set_option("assertions", true);
208 
209  // use assumptions
210  if(cmdline.isset("no-assumptions"))
211  options.set_option("assumptions", false);
212  else
213  options.set_option("assumptions", true);
214 
215  // magic error label
216  if(cmdline.isset("error-label"))
217  options.set_option("error-label", cmdline.get_values("error-label"));
218 
219  // generate unwinding assertions
220  if(cmdline.isset("cover"))
221  options.set_option("unwinding-assertions", false);
222  else
223  options.set_option(
224  "unwinding-assertions",
225  cmdline.isset("unwinding-assertions"));
226 
227  // generate unwinding assumptions otherwise
228  options.set_option("partial-loops", cmdline.isset("partial-loops"));
229 
230  if(options.get_bool_option("partial-loops") &&
231  options.get_bool_option("unwinding-assertions"))
232  {
233  error() << "--partial-loops and --unwinding-assertions"
234  << " must not be given together" << eom;
235  exit(1);
236  }
237 }
238 
241 {
242  if(cmdline.isset("version"))
243  {
244  std::cout << CBMC_VERSION << '\n';
245  return 0;
246  }
247 
248  //
249  // command line options
250  //
251 
252  optionst options;
253  get_command_line_options(options);
254  eval_verbosity();
255 
256  //
257  // Print a banner
258  //
259  status() << "GOTO-DIFF version " CBMC_VERSION " "
260  << sizeof(void *)*8 << "-bit "
261  << config.this_architecture() << " "
263 
264  if(cmdline.args.size()!=2)
265  {
266  error() << "Please provide two programs to compare" << eom;
267  return 6;
268  }
269 
270  goto_modelt goto_model1, goto_model2;
271 
272  int get_goto_program_ret=
273  get_goto_program(options, *this, goto_model1);
274  if(get_goto_program_ret!=-1)
275  return get_goto_program_ret;
276  get_goto_program_ret=
277  get_goto_program(options, languages2, goto_model2);
278  if(get_goto_program_ret!=-1)
279  return get_goto_program_ret;
280 
281  if(cmdline.isset("show-goto-functions"))
282  {
283  show_goto_functions(goto_model1, get_ui());
284  show_goto_functions(goto_model2, get_ui());
285  return 0;
286  }
287 
288  if(cmdline.isset("change-impact") ||
289  cmdline.isset("forward-impact") ||
290  cmdline.isset("backward-impact"))
291  {
292  // Workaround to avoid deps not propagating between return and end_func
293  remove_returns(goto_model1);
294  remove_returns(goto_model2);
295 
296  impact_modet impact_mode=
297  cmdline.isset("forward-impact") ?
299  (cmdline.isset("backward-impact") ?
303  goto_model1,
304  goto_model2,
305  impact_mode,
306  cmdline.isset("compact-output"));
307 
308  return 0;
309  }
310 
311  if(cmdline.isset("unified") ||
312  cmdline.isset('u'))
313  {
314  unified_difft u(goto_model1, goto_model2);
315  u();
316  u.output(std::cout);
317 
318  return 0;
319  }
320 
321  std::unique_ptr<goto_difft> goto_diff;
322  goto_diff = std::unique_ptr<goto_difft>(
323  new syntactic_difft(goto_model1, goto_model2, get_message_handler()));
324  goto_diff->set_ui(get_ui());
325 
326  (*goto_diff)();
327 
328  goto_diff->output_functions(std::cout);
329 
330  return 0;
331 }
332 
334  const optionst &options,
336  goto_modelt &goto_model)
337 {
338  status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
339 
340  if(is_goto_binary(cmdline.args[0]))
341  {
342  if(read_goto_binary(
343  cmdline.args[0],
344  goto_model.symbol_table,
345  goto_model.goto_functions,
346  languages.get_message_handler()))
347  return 6;
348 
349  config.set(cmdline);
351 
352  // This one is done.
353  cmdline.args.erase(cmdline.args.begin());
354  }
355  else
356  {
357  // This is a a workaround to make parse() think that there is only
358  // one source file.
359  std::string arg2("");
360  if(cmdline.args.size()==2)
361  {
362  arg2 = cmdline.args[1];
363  cmdline.args.erase(--cmdline.args.end());
364  }
365 
366  if(languages.parse() ||
367  languages.typecheck() ||
368  languages.final())
369  return 6;
370 
371  // we no longer need any parse trees or language files
372  languages.clear_parse();
373 
374  status() << "Generating GOTO Program" << eom;
375 
376  goto_model.symbol_table=languages.symbol_table;
377  goto_convert(
378  goto_model.symbol_table,
379  goto_model.goto_functions,
381 
382  // if we had a second argument then we will handle it next
383  if(arg2!="")
384  cmdline.args[0]=arg2;
385  }
386 
387  return -1; // no error, continue
388 }
389 
391  const optionst &options,
392  goto_modelt &goto_model)
393 {
395  goto_functionst &goto_functions = goto_model.goto_functions;
396 
397  try
398  {
400 
401  // Remove inline assembler; this needs to happen before
402  // adding the library.
403  remove_asm(symbol_table, goto_functions);
404 
405  // add the library
407 
408  // remove function pointers
409  status() << "Function Pointer Removal" << eom;
412  symbol_table,
413  goto_functions,
414  cmdline.isset("pointer-check"));
415 
416  // do partial inlining
417  status() << "Partial Inlining" << eom;
418  goto_partial_inline(goto_functions, ns, ui_message_handler);
419 
420  // remove returns, gcc vectors, complex
421  remove_returns(symbol_table, goto_functions);
422  remove_vector(symbol_table, goto_functions);
423  remove_complex(symbol_table, goto_functions);
424 
425  // add failed symbols
426  // needs to be done before pointer analysis
428 
429  // recalculate numbers, etc.
430  goto_functions.update();
431 
432  // add loop ids
433  goto_functions.compute_loop_numbers();
434 
435  // show it?
436  if(cmdline.isset("show-loops"))
437  {
438  show_loop_ids(get_ui(), goto_functions);
439  return true;
440  }
441 
442  // show it?
443  if(cmdline.isset("show-goto-functions"))
444  {
445  show_goto_functions(ns, get_ui(), goto_functions);
446  return true;
447  }
448  }
449 
450  catch(const char *e)
451  {
452  error() << e << eom;
453  return true;
454  }
455 
456  catch(const std::string e)
457  {
458  error() << e << eom;
459  return true;
460  }
461 
462  catch(int)
463  {
464  return true;
465  }
466 
467  catch(std::bad_alloc)
468  {
469  error() << "Out of memory" << eom;
470  return true;
471  }
472 
473  return false;
474 }
475 
478 {
479  std::cout <<
480  "\n"
481  // NOLINTNEXTLINE(whitespace/line_length)
482  "* * GOTO_DIFF " CBMC_VERSION " - Copyright (C) 2016 * *\n"
483  "* * Daniel Kroening, Peter Schrammel * *\n"
484  "* * kroening@kroening.com * *\n"
485  "\n"
486  "Usage: Purpose:\n"
487  "\n"
488  " goto_diff [-?] [-h] [--help] show help\n"
489  " goto_diff old new goto binaries to be compared\n"
490  "\n"
491  "Diff options:\n"
493  " --syntactic do syntactic diff (default)\n"
494  " -u | --unified output unified diff\n"
495  " --change-impact | \n"
496  " --forward-impact |\n"
497  // NOLINTNEXTLINE(whitespace/line_length)
498  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
499  " --compact-output output dependencies in compact mode\n"
500  "\n"
501  "Other options:\n"
502  " --version show version and exit\n"
503  " --json-ui use JSON-formatted output\n"
504  "\n";
505 }
virtual std::ostream & output_functions(std::ostream &out) const
symbol_tablet symbol_table
Definition: language_ui.h:24
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:90
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
struct configt::ansi_ct ansi_c
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
Definition: remove_asm.cpp:317
Remove Indirect Function Calls.
mstreamt & status()
Definition: message.h:238
impact_modet
Definition: change_impact.h:18
uit get_ui()
Definition: language_ui.h:47
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
virtual int get_goto_program(const optionst &options, goto_diff_languagest &languages, goto_modelt &goto_model)
Data and control-dependencies of syntactic diff.
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
Remove the &#39;complex&#39; data type by compilation into structs.
#define GOTO_DIFF_OPTIONS
std::string get_value(char option) const
Definition: cmdline.cpp:46
void set_cpp98()
Definition: config.h:128
symbol_tablet symbol_table
Definition: goto_model.h:25
Pointer Dereferencing.
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
goto_diff_languagest languages2
String Abstraction.
virtual void help()
display command line help
configt config
Definition: config.cpp:21
Remove &#39;asm&#39; statements by compiling into suitable standard code.
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.
void set_ui(language_uit::uit _ui)
Definition: goto_diff.h:40
Unused function removal.
bool set(const cmdlinet &cmdline)
Definition: config.cpp:727
void set_c89()
Definition: config.h:50
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
argst args
Definition: cmdline.h:35
virtual bool isset(char option) const
Definition: cmdline.cpp:30
String Abstraction.
virtual int doit()
invoke main modules
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Function Inlining.
Abstract interface to support a programming language.
Loop IDs.
Syntactic GOTO-DIFF.
virtual void get_command_line_options(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)
virtual bool process_goto_program(const optionst &options, goto_modelt &goto_model)
Remove function returns.
GOTO-DIFF Command Line Option Processing.
Unified diff (using LCSS) of goto functions.
void set_c11()
Definition: config.h:52
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1091
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.
void output(std::ostream &os) const
ui_message_handlert ui_message_handler
#define HELP_SHOW_GOTO_FUNCTIONS
void remove_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
mstreamt & error()
Definition: message.h:223
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 set_option(const std::string &option, const bool value)
Definition: options.cpp:24
void add_failed_symbols(symbol_tablet &symbol_table)
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 set_cpp03()
Definition: config.h:129
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
goto_functionst goto_functions
Definition: goto_model.h:26
languagest languages
Definition: mode.cpp:29
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
Definition: config.cpp:1148
GOTO-DIFF Base Class.
goto_diff_parse_optionst(int argc, const char **argv)