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 
32 #include <goto-programs/loop_ids.h>
33 #include <goto-programs/mm_io.h>
48 
49 #include <goto-instrument/cover.h>
50 
52 
53 #include <langapi/mode.h>
54 
55 #include <ansi-c/cprover_library.h>
56 #include <cpp/cprover_library.h>
57 
58 #include "goto_diff.h"
59 #include "syntactic_diff.h"
60 #include "unified_diff.h"
61 #include "change_impact.h"
62 
65  goto_diff_languagest(cmdline, ui_message_handler),
66  ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION),
67  languages2(cmdline, ui_message_handler)
68 {
69 }
70 
72  int argc,
73  const char **argv,
74  const std::string &extra_options)
75  : parse_options_baset(GOTO_DIFF_OPTIONS + extra_options, argc, argv),
76  goto_diff_languagest(cmdline, ui_message_handler),
77  ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION),
78  languages2(cmdline, ui_message_handler)
79 {
80 }
81 
83 {
84  if(config.set(cmdline))
85  {
86  usage_error();
87  exit(1);
88  }
89 
90  if(cmdline.isset("program-only"))
91  options.set_option("program-only", true);
92 
93  if(cmdline.isset("show-vcc"))
94  options.set_option("show-vcc", true);
95 
96  if(cmdline.isset("cover"))
98 
99  if(cmdline.isset("mm"))
100  options.set_option("mm", cmdline.get_value("mm"));
101 
102  if(cmdline.isset("c89"))
104 
105  if(cmdline.isset("c99"))
107 
108  if(cmdline.isset("c11"))
110 
111  if(cmdline.isset("cpp98"))
112  config.cpp.set_cpp98();
113 
114  if(cmdline.isset("cpp03"))
115  config.cpp.set_cpp03();
116 
117  if(cmdline.isset("cpp11"))
118  config.cpp.set_cpp11();
119 
120  // all checks supported by goto_check
122 
123  if(cmdline.isset("debug-level"))
124  options.set_option("debug-level", cmdline.get_value("debug-level"));
125 
126  if(cmdline.isset("slice-by-trace"))
127  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
128 
129  if(cmdline.isset("unwindset"))
130  options.set_option("unwindset", cmdline.get_value("unwindset"));
131 
132  // constant propagation
133  if(cmdline.isset("no-propagation"))
134  options.set_option("propagation", false);
135  else
136  options.set_option("propagation", true);
137 
138  // check array bounds
139  if(cmdline.isset("bounds-check"))
140  options.set_option("bounds-check", true);
141  else
142  options.set_option("bounds-check", false);
143 
144  // check division by zero
145  if(cmdline.isset("div-by-zero-check"))
146  options.set_option("div-by-zero-check", true);
147  else
148  options.set_option("div-by-zero-check", false);
149 
150  // check overflow/underflow
151  if(cmdline.isset("signed-overflow-check"))
152  options.set_option("signed-overflow-check", true);
153  else
154  options.set_option("signed-overflow-check", false);
155 
156  // check overflow/underflow
157  if(cmdline.isset("unsigned-overflow-check"))
158  options.set_option("unsigned-overflow-check", true);
159  else
160  options.set_option("unsigned-overflow-check", false);
161 
162  // check overflow/underflow
163  if(cmdline.isset("float-overflow-check"))
164  options.set_option("float-overflow-check", true);
165  else
166  options.set_option("float-overflow-check", false);
167 
168  // check for NaN (not a number)
169  if(cmdline.isset("nan-check"))
170  options.set_option("nan-check", true);
171  else
172  options.set_option("nan-check", false);
173 
174  // check pointers
175  if(cmdline.isset("pointer-check"))
176  options.set_option("pointer-check", true);
177  else
178  options.set_option("pointer-check", false);
179 
180  // check for memory leaks
181  if(cmdline.isset("memory-leak-check"))
182  options.set_option("memory-leak-check", true);
183  else
184  options.set_option("memory-leak-check", false);
185 
186  // check assertions
187  if(cmdline.isset("no-assertions"))
188  options.set_option("assertions", false);
189  else
190  options.set_option("assertions", true);
191 
192  // use assumptions
193  if(cmdline.isset("no-assumptions"))
194  options.set_option("assumptions", false);
195  else
196  options.set_option("assumptions", true);
197 
198  // magic error label
199  if(cmdline.isset("error-label"))
200  options.set_option("error-label", cmdline.get_values("error-label"));
201 
202  // generate unwinding assertions
203  if(cmdline.isset("cover"))
204  options.set_option("unwinding-assertions", false);
205  else
207  "unwinding-assertions",
208  cmdline.isset("unwinding-assertions"));
209 
210  // generate unwinding assumptions otherwise
211  options.set_option("partial-loops", cmdline.isset("partial-loops"));
212 
213  if(options.get_bool_option("partial-loops") &&
214  options.get_bool_option("unwinding-assertions"))
215  {
216  error() << "--partial-loops and --unwinding-assertions"
217  << " must not be given together" << eom;
218  exit(1);
219  }
220 
221  options.set_option("show-properties", cmdline.isset("show-properties"));
222 }
223 
226 {
227  if(cmdline.isset("version"))
228  {
229  std::cout << CBMC_VERSION << '\n';
230  return CPROVER_EXIT_SUCCESS;
231  }
232 
233  //
234  // command line options
235  //
236 
241 
242  //
243  // Print a banner
244  //
245  status() << "GOTO-DIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8
246  << "-bit " << config.this_architecture() << " "
248 
249  if(cmdline.args.size()!=2)
250  {
251  error() << "Please provide two programs to compare" << eom;
253  }
254 
255  goto_modelt goto_model1, goto_model2;
256 
257  int get_goto_program_ret=
258  get_goto_program(options, *this, goto_model1);
259  if(get_goto_program_ret!=-1)
260  return get_goto_program_ret;
261  get_goto_program_ret=
262  get_goto_program(options, languages2, goto_model2);
263  if(get_goto_program_ret!=-1)
264  return get_goto_program_ret;
265 
266  if(cmdline.isset("show-loops"))
267  {
268  show_loop_ids(get_ui(), goto_model1);
269  show_loop_ids(get_ui(), goto_model2);
270  return CPROVER_EXIT_SUCCESS;
271  }
272 
273  if(
274  cmdline.isset("show-goto-functions") ||
275  cmdline.isset("list-goto-functions"))
276  {
278  goto_model1,
281  cmdline.isset("list-goto-functions"));
283  goto_model2,
286  cmdline.isset("list-goto-functions"));
287  return CPROVER_EXIT_SUCCESS;
288  }
289 
290  if(cmdline.isset("change-impact") ||
291  cmdline.isset("forward-impact") ||
292  cmdline.isset("backward-impact"))
293  {
294  impact_modet impact_mode=
295  cmdline.isset("forward-impact") ?
297  (cmdline.isset("backward-impact") ?
301  goto_model1,
302  goto_model2,
303  impact_mode,
304  cmdline.isset("compact-output"));
305 
306  return CPROVER_EXIT_SUCCESS;
307  }
308 
309  if(cmdline.isset("unified") ||
310  cmdline.isset('u'))
311  {
312  unified_difft u(goto_model1, goto_model2);
313  u();
314  u.output(std::cout);
315 
316  return CPROVER_EXIT_SUCCESS;
317  }
318 
319  syntactic_difft sd(goto_model1, goto_model2, options, ui_message_handler);
320  sd();
321  sd.output_functions();
322 
323  return CPROVER_EXIT_SUCCESS;
324 }
325 
327  const optionst &options,
329  goto_modelt &goto_model)
330 {
331  status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
332 
333  if(is_goto_binary(cmdline.args[0]))
334  {
335  if(read_goto_binary(
336  cmdline.args[0],
337  goto_model.symbol_table,
338  goto_model.goto_functions,
339  languages.get_message_handler()))
341 
342  config.set(cmdline);
343 
344  // This one is done.
345  cmdline.args.erase(cmdline.args.begin());
346  }
347  else
348  {
349  // This is a a workaround to make parse() think that there is only
350  // one source file.
351  std::string arg2("");
352  if(cmdline.args.size()==2)
353  {
354  arg2 = cmdline.args[1];
355  cmdline.args.erase(--cmdline.args.end());
356  }
357 
358  if(languages.parse() ||
359  languages.typecheck() ||
360  languages.final())
362 
363  // we no longer need any parse trees or language files
364  languages.clear_parse();
365 
366  status() << "Generating GOTO Program" << eom;
367 
368  goto_model.symbol_table=languages.symbol_table;
369  goto_convert(
370  goto_model.symbol_table,
371  goto_model.goto_functions,
373 
374  if(process_goto_program(options, goto_model))
376 
377  // if we had a second argument then we will handle it next
378  if(arg2!="")
379  cmdline.args[0]=arg2;
380  }
381 
382  return -1; // no error, continue
383 }
384 
386  const optionst &options,
387  goto_modelt &goto_model)
388 {
389  try
390  {
391  // Remove inline assembler; this needs to happen before
392  // adding the library.
393  remove_asm(goto_model);
394 
395  // add the library
396  status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
401 
402  // remove function pointers
403  status() << "Removal of function pointers and virtual functions" << eom;
405  get_message_handler(), goto_model, cmdline.isset("pointer-check"));
406 
407  mm_io(goto_model);
408 
409  // instrument library preconditions
410  instrument_preconditions(goto_model);
411 
412  // remove returns, gcc vectors, complex
413  remove_returns(goto_model);
414  remove_vector(goto_model);
415  remove_complex(goto_model);
416  rewrite_union(goto_model);
417 
418  // add generic checks
419  status() << "Generic Property Instrumentation" << eom;
420  goto_check(options, goto_model);
421 
422  // checks don't know about adjusted float expressions
423  adjust_float_expressions(goto_model);
424 
425  // recalculate numbers, etc.
426  goto_model.goto_functions.update();
427 
428  // add loop ids
430 
431  // instrument cover goals
432  if(cmdline.isset("cover"))
433  {
434  // remove skips such that trivial GOTOs are deleted and not considered
435  // for coverage annotation:
436  remove_skip(goto_model);
437 
439  return true;
440  }
441 
442  // label the assertions
443  // This must be done after adding assertions and
444  // before using the argument of the "property" option.
445  // Do not re-label after using the property slicer because
446  // this would cause the property identifiers to change.
447  label_properties(goto_model);
448 
449  // remove any skips introduced since coverage instrumentation
450  remove_skip(goto_model);
451  }
452 
453  catch(const char *e)
454  {
455  error() << e << eom;
456  return true;
457  }
458 
459  catch(const std::string &e)
460  {
461  error() << e << eom;
462  return true;
463  }
464 
465  catch(int e)
466  {
467  error() << "Numeric exception: " << e << eom;
468  return true;
469  }
470 
471  catch(const std::bad_alloc &)
472  {
473  error() << "Out of memory" << eom;
475  return true;
476  }
477 
478  return false;
479 }
480 
483 {
484  // clang-format off
485  std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n'
486  <<
487  "* * Copyright (C) 2016 * *\n"
488  "* * Daniel Kroening, Peter Schrammel * *\n"
489  "* * kroening@kroening.com * *\n"
490  "\n"
491  "Usage: Purpose:\n"
492  "\n"
493  " goto_diff [-?] [-h] [--help] show help\n"
494  " goto_diff old new goto binaries to be compared\n"
495  "\n"
496  "Diff options:\n"
499  " --syntactic do syntactic diff (default)\n"
500  " -u | --unified output unified diff\n"
501  " --change-impact | \n"
502  " --forward-impact |\n"
503  // NOLINTNEXTLINE(whitespace/line_length)
504  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
505  " --compact-output output dependencies in compact mode\n"
506  "\n"
507  "Program instrumentation options:\n"
509  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
510  "Other options:\n"
511  " --version show version and exit\n"
512  " --json-ui use JSON-formatted output\n"
513  HELP_FLUSH
515  "\n";
516  // clang-format on
517 }
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.
Functions for replacing virtual function call with a static function calls in functions,...
optionst * options
Definition: language_ui.h:57
uit get_ui() const
Definition: ui_message.h:30
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:49
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:98
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
Remove the 'complex' 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:140
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Pointer Dereferencing.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:46
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:24
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
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:160
Set the properties to check.
#define HELP_GOTO_CHECK
Definition: goto_check.h:43
Unused function removal.
bool set(const cmdlinet &cmdline)
Definition: config.cpp:767
void set_c89()
Definition: config.h:51
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
Read a goto binary from a file, but do not update config.
Perform Memory-mapped I/O instrumentation.
#define HELP_TIMESTAMP
Definition: timestamper.h:14
argst args
Definition: cmdline.h:44
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:104
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
mstreamt & error() const
Definition: message.h:386
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.
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
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:58
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)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Definition: remove_asm.cpp:516
static eomt eom
Definition: message.h:284
static irep_idt this_operating_system()
Definition: config.cpp:1368
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:53
struct configt::cppt cpp
void set_c99()
Definition: config.h:52
message_handlert & get_message_handler()
Definition: message.h:174
void set_cpp11()
Definition: config.h:142
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:401
#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 'vector' data type by compilation into arrays.
Options.
virtual void usage_error()
Show the properties.
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:50
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
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:141
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:1268
GOTO-DIFF Base Class.
goto_diff_parse_optionst(int argc, const char **argv)