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 
33 #include <goto-programs/loop_ids.h>
34 #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 
57 #include <assembler/remove_asm.h>
58 
59 #include <cpp/cprover_library.h>
60 
61 #include "goto_diff.h"
62 #include "syntactic_diff.h"
63 #include "unified_diff.h"
64 #include "change_impact.h"
65 
69  argc,
70  argv,
71  std::string("GOTO-DIFF ") + CBMC_VERSION)
72 {
73 }
74 
76 {
77  if(config.set(cmdline))
78  {
79  usage_error();
80  exit(1);
81  }
82 
83  if(cmdline.isset("program-only"))
84  options.set_option("program-only", true);
85 
86  if(cmdline.isset("show-byte-ops"))
87  options.set_option("show-byte-ops", true);
88 
89  if(cmdline.isset("show-vcc"))
90  options.set_option("show-vcc", true);
91 
92  if(cmdline.isset("cover"))
93  parse_cover_options(cmdline, options);
94 
95  if(cmdline.isset("mm"))
96  options.set_option("mm", cmdline.get_value("mm"));
97 
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 
116  // all checks supported by goto_check
118 
119  if(cmdline.isset("debug-level"))
120  options.set_option("debug-level", cmdline.get_value("debug-level"));
121 
122  if(cmdline.isset("unwindset"))
123  options.set_option("unwindset", cmdline.get_value("unwindset"));
124 
125  // constant propagation
126  if(cmdline.isset("no-propagation"))
127  options.set_option("propagation", false);
128  else
129  options.set_option("propagation", true);
130 
131  // check array bounds
132  if(cmdline.isset("bounds-check"))
133  options.set_option("bounds-check", true);
134  else
135  options.set_option("bounds-check", false);
136 
137  // check division by zero
138  if(cmdline.isset("div-by-zero-check"))
139  options.set_option("div-by-zero-check", true);
140  else
141  options.set_option("div-by-zero-check", false);
142 
143  // check overflow/underflow
144  if(cmdline.isset("signed-overflow-check"))
145  options.set_option("signed-overflow-check", true);
146  else
147  options.set_option("signed-overflow-check", false);
148 
149  // check overflow/underflow
150  if(cmdline.isset("unsigned-overflow-check"))
151  options.set_option("unsigned-overflow-check", true);
152  else
153  options.set_option("unsigned-overflow-check", false);
154 
155  // check overflow/underflow
156  if(cmdline.isset("float-overflow-check"))
157  options.set_option("float-overflow-check", true);
158  else
159  options.set_option("float-overflow-check", false);
160 
161  // check for NaN (not a number)
162  if(cmdline.isset("nan-check"))
163  options.set_option("nan-check", true);
164  else
165  options.set_option("nan-check", false);
166 
167  // check pointers
168  if(cmdline.isset("pointer-check"))
169  options.set_option("pointer-check", true);
170  else
171  options.set_option("pointer-check", false);
172 
173  // check for memory leaks
174  if(cmdline.isset("memory-leak-check"))
175  options.set_option("memory-leak-check", true);
176  else
177  options.set_option("memory-leak-check", false);
178 
179  // check assertions
180  if(cmdline.isset("no-assertions"))
181  options.set_option("assertions", false);
182  else
183  options.set_option("assertions", true);
184 
185  // use assumptions
186  if(cmdline.isset("no-assumptions"))
187  options.set_option("assumptions", false);
188  else
189  options.set_option("assumptions", true);
190 
191  // magic error label
192  if(cmdline.isset("error-label"))
193  options.set_option("error-label", cmdline.get_values("error-label"));
194 
195  // generate unwinding assertions
196  if(cmdline.isset("cover"))
197  options.set_option("unwinding-assertions", false);
198  else
199  options.set_option(
200  "unwinding-assertions",
201  cmdline.isset("unwinding-assertions"));
202 
203  // generate unwinding assumptions otherwise
204  options.set_option("partial-loops", cmdline.isset("partial-loops"));
205 
206  if(options.get_bool_option("partial-loops") &&
207  options.get_bool_option("unwinding-assertions"))
208  {
209  log.error() << "--partial-loops and --unwinding-assertions"
210  << " must not be given together" << messaget::eom;
211  exit(1);
212  }
213 
214  options.set_option("show-properties", cmdline.isset("show-properties"));
215 }
216 
219 {
220  if(cmdline.isset("version"))
221  {
222  std::cout << CBMC_VERSION << '\n';
223  return CPROVER_EXIT_SUCCESS;
224  }
225 
226  //
227  // command line options
228  //
229 
230  optionst options;
231  get_command_line_options(options);
234 
235  //
236  // Print a banner
237  //
238  log.status() << "GOTO-DIFF version " << CBMC_VERSION << " "
239  << sizeof(void *) * 8 << "-bit " << config.this_architecture()
241 
242  if(cmdline.args.size()!=2)
243  {
244  log.error() << "Please provide two programs to compare" << messaget::eom;
246  }
247 
249 
250  goto_modelt goto_model1 =
252  if(process_goto_program(options, goto_model1))
254  goto_modelt goto_model2 =
256  if(process_goto_program(options, goto_model2))
258 
259  if(cmdline.isset("show-loops"))
260  {
261  show_loop_ids(ui_message_handler.get_ui(), goto_model1);
262  show_loop_ids(ui_message_handler.get_ui(), goto_model2);
263  return CPROVER_EXIT_SUCCESS;
264  }
265 
266  if(
267  cmdline.isset("show-goto-functions") ||
268  cmdline.isset("list-goto-functions"))
269  {
271  goto_model1, ui_message_handler, cmdline.isset("list-goto-functions"));
273  goto_model2, ui_message_handler, cmdline.isset("list-goto-functions"));
274  return CPROVER_EXIT_SUCCESS;
275  }
276 
277  if(cmdline.isset("change-impact") ||
278  cmdline.isset("forward-impact") ||
279  cmdline.isset("backward-impact"))
280  {
281  impact_modet impact_mode=
282  cmdline.isset("forward-impact") ?
284  (cmdline.isset("backward-impact") ?
288  goto_model1,
289  goto_model2,
290  impact_mode,
291  cmdline.isset("compact-output"));
292 
293  return CPROVER_EXIT_SUCCESS;
294  }
295 
296  if(cmdline.isset("unified") ||
297  cmdline.isset('u'))
298  {
299  unified_difft u(goto_model1, goto_model2);
300  u();
301  u.output(std::cout);
302 
303  return CPROVER_EXIT_SUCCESS;
304  }
305 
306  syntactic_difft sd(goto_model1, goto_model2, options, ui_message_handler);
307  sd();
308  sd.output_functions();
309 
310  return CPROVER_EXIT_SUCCESS;
311 }
312 
314  const optionst &options,
315  goto_modelt &goto_model)
316 {
317  {
318  // Remove inline assembler; this needs to happen before
319  // adding the library.
320  remove_asm(goto_model);
321 
322  // add the library
323  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
324  << messaget::eom;
328 
329  // remove function pointers
330  log.status() << "Removal of function pointers and virtual functions"
331  << messaget::eom;
333  ui_message_handler, goto_model, cmdline.isset("pointer-check"));
334 
335  mm_io(goto_model);
336 
337  // instrument library preconditions
338  instrument_preconditions(goto_model);
339 
340  // remove returns, gcc vectors, complex
341  remove_returns(goto_model);
342  remove_vector(goto_model);
343  remove_complex(goto_model);
344  rewrite_union(goto_model);
345 
346  // add generic checks
347  log.status() << "Generic Property Instrumentation" << messaget::eom;
348  goto_check(options, goto_model);
349 
350  // checks don't know about adjusted float expressions
351  adjust_float_expressions(goto_model);
352 
353  // recalculate numbers, etc.
354  goto_model.goto_functions.update();
355 
356  // add loop ids
358 
359  // instrument cover goals
360  if(cmdline.isset("cover"))
361  {
362  // remove skips such that trivial GOTOs are deleted and not considered
363  // for coverage annotation:
364  remove_skip(goto_model);
365 
366  const auto cover_config =
367  get_cover_config(options, goto_model.symbol_table, ui_message_handler);
368  if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
369  return true;
370  }
371 
372  // label the assertions
373  // This must be done after adding assertions and
374  // before using the argument of the "property" option.
375  // Do not re-label after using the property slicer because
376  // this would cause the property identifiers to change.
377  label_properties(goto_model);
378 
379  // remove any skips introduced since coverage instrumentation
380  remove_skip(goto_model);
381  }
382 
383  return false;
384 }
385 
388 {
389  // clang-format off
390  std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n'
391  << align_center_with_border("Copyright (C) 2016") << '\n'
392  << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT (*)
393  << align_center_with_border("kroening@kroening.com") << '\n'
394  <<
395  "\n"
396  "Usage: Purpose:\n"
397  "\n"
398  " goto_diff [-?] [-h] [--help] show help\n"
399  " goto_diff old new goto binaries to be compared\n"
400  "\n"
401  "Diff options:\n"
404  " --syntactic do syntactic diff (default)\n"
405  " -u | --unified output unified diff\n"
406  " --change-impact | \n"
407  " --forward-impact |\n"
408  // NOLINTNEXTLINE(whitespace/line_length)
409  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
410  " --compact-output output dependencies in compact mode\n"
411  "\n"
412  "Program instrumentation options:\n"
414  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
415  "Other options:\n"
416  " --version show version and exit\n"
417  " --json-ui use JSON-formatted output\n"
418  HELP_FLUSH
420  "\n";
421  // clang-format on
422 }
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:91
cover.h
Coverage Instrumentation.
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:26
goto_diff_parse_optionst::process_goto_program
bool process_goto_program(const optionst &options, goto_modelt &goto_model)
Definition: goto_diff_parse_options.cpp:313
impact_modet
impact_modet
Definition: change_impact.h:18
string_abstraction.h
String Abstraction.
configt::ansi_ct::set_c99
void set_c99()
Definition: config.h:53
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:61
rewrite_union.h
Symbolic Execution.
unified_difft::output
void output(std::ostream &os) const
Definition: unified_diff.cpp:367
parse_options_baset::ui_message_handler
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
parse_options_baset
Definition: parse_options.h:20
GOTO_DIFF_OPTIONS
#define GOTO_DIFF_OPTIONS
Definition: goto_diff_parse_options.h:29
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
impact_modet::BACKWARD
@ BACKWARD
goto_inline.h
Function Inlining.
optionst
Definition: options.h:23
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:171
mm_io
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:32
messaget::status
mstreamt & status() const
Definition: message.h:414
instrument_preconditions.h
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
remove_virtual_functions.h
Functions for replacing virtual function call with a static function calls in functions,...
remove_asm.h
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
change_impact
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
Definition: change_impact.cpp:745
goto_modelt
Definition: goto_model.h:26
mode.h
show_loop_ids
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:19
options.h
Options.
goto_check
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
Definition: goto_check.cpp:2231
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
messaget::eom
static eomt eom
Definition: message.h:297
instrument_cover_goals
static void instrument_cover_goals(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
Applies instrumenters to given goto program.
Definition: cover.cpp:37
impact_modet::BOTH
@ BOTH
configt::ansi_c
struct configt::ansi_ct ansi_c
version.h
string_instrumentation.h
String Abstraction.
unified_difft
Definition: unified_diff.h:31
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:43
goto_diff_parse_optionst::register_languages
void register_languages()
Definition: goto_diff_languages.cpp:19
syntactic_difft
Definition: syntactic_diff.h:18
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:47
remove_vector
static void remove_vector(typet &)
removes vector data type
Definition: remove_vector.cpp:166
configt::cppt::set_cpp98
void set_cpp98()
Definition: config.h:151
unified_diff.h
Unified diff (using LCSS) of goto functions.
remove_complex.h
Remove the 'complex' data type by compilation into structs.
set_properties.h
Set the properties to check.
get_cover_config
cover_configt get_cover_config(const optionst &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Build data structures controlling coverage from command-line options.
Definition: cover.cpp:176
goto_difft::output_functions
virtual void output_functions() const
Output diff result.
Definition: goto_diff_base.cpp:21
CBMC_VERSION
const char * CBMC_VERSION
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:399
initialize_goto_model.h
Initialize a Goto Program.
goto_diff.h
GOTO-DIFF Base Class.
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:163
mm_io.h
Perform Memory-mapped I/O instrumentation.
goto_diff_parse_optionst::help
virtual void help()
display command line help
Definition: goto_diff_parse_options.cpp:387
instrument_preconditions
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Definition: instrument_preconditions.cpp:90
syntactic_diff.h
Syntactic GOTO-DIFF.
show_properties.h
Show the properties.
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:153
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
rewrite_union
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Definition: rewrite_union.cpp:66
language.h
Abstract interface to support a programming language.
HELP_SHOW_PROPERTIES
#define HELP_SHOW_PROPERTIES
Definition: show_properties.h:29
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1402
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:85
show_goto_functions
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:26
parse_cover_options
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:142
goto_diff_parse_options.h
GOTO-DIFF Command Line Option Processing.
impact_modet::FORWARD
@ FORWARD
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
read_goto_binary.h
Read Goto Programs.
CPROVER_EXIT_INCORRECT_TASK
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
Definition: exit_codes.h:49
remove_vector.h
Remove the 'vector' data type by compilation into arrays.
remove_complex
static void remove_complex(typet &)
removes complex data type
Definition: remove_complex.cpp:231
remove_returns.h
Replace function returns by assignments to global variables.
remove_unused_functions.h
Unused function removal.
goto_diff_parse_optionst::doit
virtual int doit()
invoke main modules
Definition: goto_diff_parse_options.cpp:218
config
configt config
Definition: config.cpp:24
parse_options_baset::log
messaget log
Definition: parse_options.h:43
configt::ansi_ct::set_c11
void set_c11()
Definition: config.h:54
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1302
configt::ansi_ct::set_c89
void set_c89()
Definition: config.h:52
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
goto_diff_parse_optionst::goto_diff_parse_optionst
goto_diff_parse_optionst(int argc, const char **argv)
Definition: goto_diff_parse_options.cpp:66
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:45
cprover_c_library_factory
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:79
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:256
goto_functionst::update
void update()
Definition: goto_functions.h:81
remove_asm
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:512
change_impact.h
Data and control-dependencies of syntactic diff.
config.h
loop_ids.h
Loop IDs.
adjust_float_expressions
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Definition: adjust_float_expressions.cpp:78
add_failed_symbols.h
Pointer Dereferencing.
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
initialize_goto_model
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Definition: initialize_goto_model.cpp:59
goto_convert_functions.h
Goto Programs with Functions.
goto_diff_parse_optionst::get_command_line_options
void get_command_line_options(optionst &options)
Definition: goto_diff_parse_options.cpp:75
configt::cpp
struct configt::cppt cpp
CPROVER_EXIT_SUCCESS
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
messaget::eval_verbosity
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
remove_skip.h
Program Transformation.
adjust_float_expressions.h
Symbolic Execution.
remove_function_pointers
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, const irep_idt &function_id, bool add_safety_assertion, bool only_remove_const_fps)
Definition: remove_function_pointers.cpp:519
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
remove_function_pointers.h
Remove Indirect Function Calls.
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
align_center_with_border
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
Definition: parse_options.cpp:150
cprover_library.h
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:106
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:152
cprover_cpp_library_factory
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:38