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 <cstdlib> // exit()
15 #include <fstream>
16 #include <iostream>
17 #include <memory>
18 
19 #include <util/config.h>
20 #include <util/exit_codes.h>
21 #include <util/make_unique.h>
22 #include <util/options.h>
23 #include <util/version.h>
24 
25 #include <langapi/language.h>
26 
30 #include <goto-programs/mm_io.h>
45 #include <goto-programs/loop_ids.h>
47 
49 
50 #include <goto-instrument/cover.h>
51 
53 
54 #include <langapi/mode.h>
55 
56 #include <ansi-c/cprover_library.h>
57 #include <cpp/cprover_library.h>
58 
59 #include "goto_diff.h"
60 #include "syntactic_diff.h"
61 #include "unified_diff.h"
62 #include "change_impact.h"
63 
66  goto_diff_languagest(cmdline, ui_message_handler),
67  ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION),
68  languages2(cmdline, ui_message_handler)
69 {
70 }
71 
73  int argc,
74  const char **argv,
75  const std::string &extra_options)
76  : parse_options_baset(GOTO_DIFF_OPTIONS + extra_options, argc, argv),
77  goto_diff_languagest(cmdline, ui_message_handler),
78  ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION),
79  languages2(cmdline, ui_message_handler)
80 {
81 }
82 
84 {
85  if(config.set(cmdline))
86  {
87  usage_error();
88  exit(1);
89  }
90 
91  if(cmdline.isset("program-only"))
92  options.set_option("program-only", true);
93 
94  if(cmdline.isset("show-vcc"))
95  options.set_option("show-vcc", true);
96 
97  if(cmdline.isset("cover"))
98  parse_cover_options(cmdline, options);
99 
100  if(cmdline.isset("mm"))
101  options.set_option("mm", cmdline.get_value("mm"));
102 
103  if(cmdline.isset("c89"))
105 
106  if(cmdline.isset("c99"))
108 
109  if(cmdline.isset("c11"))
111 
112  if(cmdline.isset("cpp98"))
113  config.cpp.set_cpp98();
114 
115  if(cmdline.isset("cpp03"))
116  config.cpp.set_cpp03();
117 
118  if(cmdline.isset("cpp11"))
119  config.cpp.set_cpp11();
120 
121  // all checks supported by goto_check
123 
124  if(cmdline.isset("debug-level"))
125  options.set_option("debug-level", cmdline.get_value("debug-level"));
126 
127  if(cmdline.isset("slice-by-trace"))
128  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
129 
130  if(cmdline.isset("unwindset"))
131  options.set_option("unwindset", cmdline.get_value("unwindset"));
132 
133  // constant propagation
134  if(cmdline.isset("no-propagation"))
135  options.set_option("propagation", false);
136  else
137  options.set_option("propagation", true);
138 
139  // check array bounds
140  if(cmdline.isset("bounds-check"))
141  options.set_option("bounds-check", true);
142  else
143  options.set_option("bounds-check", false);
144 
145  // check division by zero
146  if(cmdline.isset("div-by-zero-check"))
147  options.set_option("div-by-zero-check", true);
148  else
149  options.set_option("div-by-zero-check", false);
150 
151  // check overflow/underflow
152  if(cmdline.isset("signed-overflow-check"))
153  options.set_option("signed-overflow-check", true);
154  else
155  options.set_option("signed-overflow-check", false);
156 
157  // check overflow/underflow
158  if(cmdline.isset("unsigned-overflow-check"))
159  options.set_option("unsigned-overflow-check", true);
160  else
161  options.set_option("unsigned-overflow-check", false);
162 
163  // check overflow/underflow
164  if(cmdline.isset("float-overflow-check"))
165  options.set_option("float-overflow-check", true);
166  else
167  options.set_option("float-overflow-check", false);
168 
169  // check for NaN (not a number)
170  if(cmdline.isset("nan-check"))
171  options.set_option("nan-check", true);
172  else
173  options.set_option("nan-check", false);
174 
175  // check pointers
176  if(cmdline.isset("pointer-check"))
177  options.set_option("pointer-check", true);
178  else
179  options.set_option("pointer-check", false);
180 
181  // check for memory leaks
182  if(cmdline.isset("memory-leak-check"))
183  options.set_option("memory-leak-check", true);
184  else
185  options.set_option("memory-leak-check", false);
186 
187  // check assertions
188  if(cmdline.isset("no-assertions"))
189  options.set_option("assertions", false);
190  else
191  options.set_option("assertions", true);
192 
193  // use assumptions
194  if(cmdline.isset("no-assumptions"))
195  options.set_option("assumptions", false);
196  else
197  options.set_option("assumptions", true);
198 
199  // magic error label
200  if(cmdline.isset("error-label"))
201  options.set_option("error-label", cmdline.get_values("error-label"));
202 
203  // generate unwinding assertions
204  if(cmdline.isset("cover"))
205  options.set_option("unwinding-assertions", false);
206  else
207  options.set_option(
208  "unwinding-assertions",
209  cmdline.isset("unwinding-assertions"));
210 
211  // generate unwinding assumptions otherwise
212  options.set_option("partial-loops", cmdline.isset("partial-loops"));
213 
214  if(options.get_bool_option("partial-loops") &&
215  options.get_bool_option("unwinding-assertions"))
216  {
217  error() << "--partial-loops and --unwinding-assertions"
218  << " must not be given together" << eom;
219  exit(1);
220  }
221 
222  options.set_option("show-properties", cmdline.isset("show-properties"));
223 }
224 
227 {
228  if(cmdline.isset("version"))
229  {
230  std::cout << CBMC_VERSION << '\n';
231  return CPROVER_EXIT_SUCCESS;
232  }
233 
234  //
235  // command line options
236  //
237 
238  optionst options;
239  get_command_line_options(options);
242 
243  //
244  // Print a banner
245  //
246  status() << "GOTO-DIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8
247  << "-bit " << config.this_architecture() << " "
249 
250  if(cmdline.args.size()!=2)
251  {
252  error() << "Please provide two programs to compare" << eom;
254  }
255 
256  goto_modelt goto_model1, goto_model2;
257 
258  int get_goto_program_ret=
259  get_goto_program(options, *this, goto_model1);
260  if(get_goto_program_ret!=-1)
261  return get_goto_program_ret;
262  get_goto_program_ret=
263  get_goto_program(options, languages2, goto_model2);
264  if(get_goto_program_ret!=-1)
265  return get_goto_program_ret;
266 
267  if(cmdline.isset("show-loops"))
268  {
269  show_loop_ids(get_ui(), goto_model1);
270  show_loop_ids(get_ui(), goto_model2);
271  return CPROVER_EXIT_SUCCESS;
272  }
273 
274  if(
275  cmdline.isset("show-goto-functions") ||
276  cmdline.isset("list-goto-functions"))
277  {
279  goto_model1,
282  cmdline.isset("list-goto-functions"));
284  goto_model2,
287  cmdline.isset("list-goto-functions"));
288  return CPROVER_EXIT_SUCCESS;
289  }
290 
291  if(cmdline.isset("change-impact") ||
292  cmdline.isset("forward-impact") ||
293  cmdline.isset("backward-impact"))
294  {
295  impact_modet impact_mode=
296  cmdline.isset("forward-impact") ?
298  (cmdline.isset("backward-impact") ?
302  goto_model1,
303  goto_model2,
304  impact_mode,
305  cmdline.isset("compact-output"));
306 
307  return CPROVER_EXIT_SUCCESS;
308  }
309 
310  if(cmdline.isset("unified") ||
311  cmdline.isset('u'))
312  {
313  unified_difft u(goto_model1, goto_model2);
314  u();
315  u.output(std::cout);
316 
317  return CPROVER_EXIT_SUCCESS;
318  }
319 
320  syntactic_difft sd(goto_model1, goto_model2, options, get_message_handler());
321  sd.set_ui(get_ui());
322  sd();
323  sd.output_functions();
324 
325  return CPROVER_EXIT_SUCCESS;
326 }
327 
329  const optionst &options,
331  goto_modelt &goto_model)
332 {
333  status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
334 
335  if(is_goto_binary(cmdline.args[0]))
336  {
337  if(read_goto_binary(
338  cmdline.args[0],
339  goto_model.symbol_table,
340  goto_model.goto_functions,
341  languages.get_message_handler()))
343 
344  config.set(cmdline);
345 
346  // This one is done.
347  cmdline.args.erase(cmdline.args.begin());
348  }
349  else
350  {
351  // This is a a workaround to make parse() think that there is only
352  // one source file.
353  std::string arg2("");
354  if(cmdline.args.size()==2)
355  {
356  arg2 = cmdline.args[1];
357  cmdline.args.erase(--cmdline.args.end());
358  }
359 
360  if(languages.parse() ||
361  languages.typecheck() ||
362  languages.final())
364 
365  // we no longer need any parse trees or language files
366  languages.clear_parse();
367 
368  status() << "Generating GOTO Program" << eom;
369 
370  goto_model.symbol_table=languages.symbol_table;
371  goto_convert(
372  goto_model.symbol_table,
373  goto_model.goto_functions,
375 
376  if(process_goto_program(options, goto_model))
378 
379  // if we had a second argument then we will handle it next
380  if(arg2!="")
381  cmdline.args[0]=arg2;
382  }
383 
384  return -1; // no error, continue
385 }
386 
388  const optionst &options,
389  goto_modelt &goto_model)
390 {
391  try
392  {
393  // Remove inline assembler; this needs to happen before
394  // adding the library.
395  remove_asm(goto_model);
396 
397  // add the library
398  status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
403 
404  // remove function pointers
405  status() << "Removal of function pointers and virtual functions" << eom;
407  get_message_handler(), goto_model, cmdline.isset("pointer-check"));
408 
409  mm_io(goto_model);
410 
411  // instrument library preconditions
412  instrument_preconditions(goto_model);
413 
414  // remove returns, gcc vectors, complex
415  remove_returns(goto_model);
416  remove_vector(goto_model);
417  remove_complex(goto_model);
418  rewrite_union(goto_model);
419 
420  // add generic checks
421  status() << "Generic Property Instrumentation" << eom;
422  goto_check(options, goto_model);
423 
424  // checks don't know about adjusted float expressions
425  adjust_float_expressions(goto_model);
426 
427  // recalculate numbers, etc.
428  goto_model.goto_functions.update();
429 
430  // add loop ids
432 
433  // instrument cover goals
434  if(cmdline.isset("cover"))
435  {
436  // remove skips such that trivial GOTOs are deleted and not considered
437  // for coverage annotation:
438  remove_skip(goto_model);
439 
440  if(instrument_cover_goals(options, goto_model, get_message_handler()))
441  return true;
442  }
443 
444  // label the assertions
445  // This must be done after adding assertions and
446  // before using the argument of the "property" option.
447  // Do not re-label after using the property slicer because
448  // this would cause the property identifiers to change.
449  label_properties(goto_model);
450 
451  // remove any skips introduced since coverage instrumentation
452  remove_skip(goto_model);
453  }
454 
455  catch(const char *e)
456  {
457  error() << e << eom;
458  return true;
459  }
460 
461  catch(const std::string &e)
462  {
463  error() << e << eom;
464  return true;
465  }
466 
467  catch(int e)
468  {
469  error() << "Numeric exception: " << e << eom;
470  return true;
471  }
472 
473  catch(const std::bad_alloc &)
474  {
475  error() << "Out of memory" << eom;
477  return true;
478  }
479 
480  return false;
481 }
482 
485 {
486  // clang-format off
487  std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n'
488  <<
489  "* * Copyright (C) 2016 * *\n"
490  "* * Daniel Kroening, Peter Schrammel * *\n"
491  "* * kroening@kroening.com * *\n"
492  "\n"
493  "Usage: Purpose:\n"
494  "\n"
495  " goto_diff [-?] [-h] [--help] show help\n"
496  " goto_diff old new goto binaries to be compared\n"
497  "\n"
498  "Diff options:\n"
501  " --syntactic do syntactic diff (default)\n"
502  " -u | --unified output unified diff\n"
503  " --change-impact | \n"
504  " --forward-impact |\n"
505  // NOLINTNEXTLINE(whitespace/line_length)
506  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
507  " --compact-output output dependencies in compact mode\n"
508  "\n"
509  "Program instrumentation options:\n"
511  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
512  "Other options:\n"
513  " --version show version and exit\n"
514  " --json-ui use JSON-formatted output\n"
515  HELP_FLUSH
517  "\n";
518  // clang-format on
519 }
void set_ui(ui_message_handlert::uit _ui)
Definition: goto_diff.h:44
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
Symbolic Execution.
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 instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Remove Indirect Function Calls.
Remove Virtual Function (Method) Calls.
uit get_ui() const
Definition: ui_message.h:37
impact_modet
Definition: change_impact.h:18
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
uit get_ui()
Definition: language_ui.h:48
void compute_loop_numbers()
virtual int get_goto_program(const optionst &options, goto_diff_languagest &languages, goto_modelt &goto_model)
Data and control-dependencies of syntactic diff.
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest...
Definition: message.cpp:78
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:45
void set_cpp98()
Definition: config.h:139
STL namespace.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Pointer Dereferencing.
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:41
goto_diff_languagest languages2
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
String Abstraction.
virtual void help()
display command line help
configt config
Definition: config.cpp:23
Remove &#39;asm&#39; statements by compiling into suitable standard code.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:163
Set the properties to check.
#define HELP_GOTO_CHECK
Definition: goto_check.h:42
Unused function removal.
bool set(const cmdlinet &cmdline)
Definition: config.cpp:738
void set_c89()
Definition: config.h:51
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
Perform Memory-mapped I/O instrumentation.
#define HELP_TIMESTAMP
Definition: timestamper.h:14
argst args
Definition: cmdline.h:37
virtual bool isset(char option) const
Definition: cmdline.cpp:27
String Abstraction.
#define HELP_SHOW_PROPERTIES
virtual int doit()
invoke main modules
virtual void output_functions() const
Output diff result.
#define HELP_FLUSH
Definition: ui_message.h:108
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
mstreamt & error() const
Definition: message.h:302
irep_idt arch
Definition: config.h:84
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)
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Remove function returns.
GOTO-DIFF Command Line Option Processing.
std::string banner_string(const std::string &front_end, const std::string &version)
void instrument_cover_goals(goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler)
Applies instrumenters to given goto program.
Definition: cover.cpp:33
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:56
Symbolic Execution.
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
Unified diff (using LCSS) of goto functions.
void set_c11()
Definition: config.h:53
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
removes assembler
Definition: remove_asm.cpp:482
static irep_idt this_operating_system()
Definition: config.cpp:1310
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:48
struct configt::cppt cpp
void set_c99()
Definition: config.h:52
message_handlert & get_message_handler()
Definition: message.h:153
void set_cpp11()
Definition: config.h:141
Goto Programs with Functions.
void output(std::ostream &os) const
ui_message_handlert ui_message_handler
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & status() const
Definition: message.h:317
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
Definition: version.cpp:1
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
Remove the &#39;vector&#39; data type by compilation into arrays.
Options.
virtual void usage_error()
Show the properties.
void rewrite_union(exprt &expr, const namespacet &ns)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
Coverage Instrumentation.
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files...
Definition: exit_codes.h:45
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
static void remove_complex(typet &)
removes complex data type
Program Transformation.
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Definition: mm_io.cpp:33
void set_cpp03()
Definition: config.h:140
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
languagest languages
Definition: mode.cpp:32
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
Definition: config.cpp:1213
GOTO-DIFF Base Class.
goto_diff_parse_optionst(int argc, const char **argv)