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-vcc"))
87  options.set_option("show-vcc", true);
88 
89  if(cmdline.isset("cover"))
90  parse_cover_options(cmdline, options);
91 
92  if(cmdline.isset("mm"))
93  options.set_option("mm", cmdline.get_value("mm"));
94 
95  if(cmdline.isset("c89"))
97 
98  if(cmdline.isset("c99"))
100 
101  if(cmdline.isset("c11"))
103 
104  if(cmdline.isset("cpp98"))
105  config.cpp.set_cpp98();
106 
107  if(cmdline.isset("cpp03"))
108  config.cpp.set_cpp03();
109 
110  if(cmdline.isset("cpp11"))
111  config.cpp.set_cpp11();
112 
113  // all checks supported by goto_check
115 
116  if(cmdline.isset("debug-level"))
117  options.set_option("debug-level", cmdline.get_value("debug-level"));
118 
119  if(cmdline.isset("unwindset"))
120  options.set_option("unwindset", cmdline.get_value("unwindset"));
121 
122  // constant propagation
123  if(cmdline.isset("no-propagation"))
124  options.set_option("propagation", false);
125  else
126  options.set_option("propagation", true);
127 
128  // check array bounds
129  if(cmdline.isset("bounds-check"))
130  options.set_option("bounds-check", true);
131  else
132  options.set_option("bounds-check", false);
133 
134  // check division by zero
135  if(cmdline.isset("div-by-zero-check"))
136  options.set_option("div-by-zero-check", true);
137  else
138  options.set_option("div-by-zero-check", false);
139 
140  // check overflow/underflow
141  if(cmdline.isset("signed-overflow-check"))
142  options.set_option("signed-overflow-check", true);
143  else
144  options.set_option("signed-overflow-check", false);
145 
146  // check overflow/underflow
147  if(cmdline.isset("unsigned-overflow-check"))
148  options.set_option("unsigned-overflow-check", true);
149  else
150  options.set_option("unsigned-overflow-check", false);
151 
152  // check overflow/underflow
153  if(cmdline.isset("float-overflow-check"))
154  options.set_option("float-overflow-check", true);
155  else
156  options.set_option("float-overflow-check", false);
157 
158  // check for NaN (not a number)
159  if(cmdline.isset("nan-check"))
160  options.set_option("nan-check", true);
161  else
162  options.set_option("nan-check", false);
163 
164  // check pointers
165  if(cmdline.isset("pointer-check"))
166  options.set_option("pointer-check", true);
167  else
168  options.set_option("pointer-check", false);
169 
170  // check for memory leaks
171  if(cmdline.isset("memory-leak-check"))
172  options.set_option("memory-leak-check", true);
173  else
174  options.set_option("memory-leak-check", false);
175 
176  // check assertions
177  if(cmdline.isset("no-assertions"))
178  options.set_option("assertions", false);
179  else
180  options.set_option("assertions", true);
181 
182  // use assumptions
183  if(cmdline.isset("no-assumptions"))
184  options.set_option("assumptions", false);
185  else
186  options.set_option("assumptions", true);
187 
188  // magic error label
189  if(cmdline.isset("error-label"))
190  options.set_option("error-label", cmdline.get_values("error-label"));
191 
192  // generate unwinding assertions
193  if(cmdline.isset("cover"))
194  options.set_option("unwinding-assertions", false);
195  else
196  options.set_option(
197  "unwinding-assertions",
198  cmdline.isset("unwinding-assertions"));
199 
200  // generate unwinding assumptions otherwise
201  options.set_option("partial-loops", cmdline.isset("partial-loops"));
202 
203  if(options.get_bool_option("partial-loops") &&
204  options.get_bool_option("unwinding-assertions"))
205  {
206  log.error() << "--partial-loops and --unwinding-assertions"
207  << " must not be given together" << messaget::eom;
208  exit(1);
209  }
210 
211  options.set_option("show-properties", cmdline.isset("show-properties"));
212 }
213 
216 {
217  if(cmdline.isset("version"))
218  {
219  std::cout << CBMC_VERSION << '\n';
220  return CPROVER_EXIT_SUCCESS;
221  }
222 
223  //
224  // command line options
225  //
226 
227  optionst options;
228  get_command_line_options(options);
231 
232  //
233  // Print a banner
234  //
235  log.status() << "GOTO-DIFF version " << CBMC_VERSION << " "
236  << sizeof(void *) * 8 << "-bit " << config.this_architecture()
238 
239  if(cmdline.args.size()!=2)
240  {
241  log.error() << "Please provide two programs to compare" << messaget::eom;
243  }
244 
246 
247  goto_modelt goto_model1 =
249  if(process_goto_program(options, goto_model1))
251  goto_modelt goto_model2 =
253  if(process_goto_program(options, goto_model2))
255 
256  if(cmdline.isset("show-loops"))
257  {
258  show_loop_ids(ui_message_handler.get_ui(), goto_model1);
259  show_loop_ids(ui_message_handler.get_ui(), goto_model2);
260  return CPROVER_EXIT_SUCCESS;
261  }
262 
263  if(
264  cmdline.isset("show-goto-functions") ||
265  cmdline.isset("list-goto-functions"))
266  {
268  goto_model1, ui_message_handler, cmdline.isset("list-goto-functions"));
270  goto_model2, ui_message_handler, cmdline.isset("list-goto-functions"));
271  return CPROVER_EXIT_SUCCESS;
272  }
273 
274  if(cmdline.isset("change-impact") ||
275  cmdline.isset("forward-impact") ||
276  cmdline.isset("backward-impact"))
277  {
278  impact_modet impact_mode=
279  cmdline.isset("forward-impact") ?
281  (cmdline.isset("backward-impact") ?
285  goto_model1,
286  goto_model2,
287  impact_mode,
288  cmdline.isset("compact-output"));
289 
290  return CPROVER_EXIT_SUCCESS;
291  }
292 
293  if(cmdline.isset("unified") ||
294  cmdline.isset('u'))
295  {
296  unified_difft u(goto_model1, goto_model2);
297  u();
298  u.output(std::cout);
299 
300  return CPROVER_EXIT_SUCCESS;
301  }
302 
303  syntactic_difft sd(goto_model1, goto_model2, options, ui_message_handler);
304  sd();
305  sd.output_functions();
306 
307  return CPROVER_EXIT_SUCCESS;
308 }
309 
311  const optionst &options,
312  goto_modelt &goto_model)
313 {
314  {
315  // Remove inline assembler; this needs to happen before
316  // adding the library.
317  remove_asm(goto_model);
318 
319  // add the library
320  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
321  << messaget::eom;
325 
326  // remove function pointers
327  log.status() << "Removal of function pointers and virtual functions"
328  << messaget::eom;
330  ui_message_handler, goto_model, cmdline.isset("pointer-check"));
331 
332  mm_io(goto_model);
333 
334  // instrument library preconditions
335  instrument_preconditions(goto_model);
336 
337  // remove returns, gcc vectors, complex
338  remove_returns(goto_model);
339  remove_vector(goto_model);
340  remove_complex(goto_model);
341  rewrite_union(goto_model);
342 
343  // add generic checks
344  log.status() << "Generic Property Instrumentation" << messaget::eom;
345  goto_check(options, goto_model);
346 
347  // checks don't know about adjusted float expressions
348  adjust_float_expressions(goto_model);
349 
350  // recalculate numbers, etc.
351  goto_model.goto_functions.update();
352 
353  // add loop ids
355 
356  // instrument cover goals
357  if(cmdline.isset("cover"))
358  {
359  // remove skips such that trivial GOTOs are deleted and not considered
360  // for coverage annotation:
361  remove_skip(goto_model);
362 
363  const auto cover_config =
364  get_cover_config(options, goto_model.symbol_table, ui_message_handler);
365  if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
366  return true;
367  }
368 
369  // label the assertions
370  // This must be done after adding assertions and
371  // before using the argument of the "property" option.
372  // Do not re-label after using the property slicer because
373  // this would cause the property identifiers to change.
374  label_properties(goto_model);
375 
376  // remove any skips introduced since coverage instrumentation
377  remove_skip(goto_model);
378  }
379 
380  return false;
381 }
382 
385 {
386  // clang-format off
387  std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n'
388  << align_center_with_border("Copyright (C) 2016") << '\n'
389  << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT (*)
390  << align_center_with_border("kroening@kroening.com") << '\n'
391  <<
392  "\n"
393  "Usage: Purpose:\n"
394  "\n"
395  " goto_diff [-?] [-h] [--help] show help\n"
396  " goto_diff old new goto binaries to be compared\n"
397  "\n"
398  "Diff options:\n"
401  " --syntactic do syntactic diff (default)\n"
402  " -u | --unified output unified diff\n"
403  " --change-impact | \n"
404  " --forward-impact |\n"
405  // NOLINTNEXTLINE(whitespace/line_length)
406  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
407  " --compact-output output dependencies in compact mode\n"
408  "\n"
409  "Program instrumentation options:\n"
411  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
412  "Other options:\n"
413  " --version show version and exit\n"
414  " --json-ui use JSON-formatted output\n"
415  HELP_FLUSH
417  "\n";
418  // clang-format on
419 }
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:85
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
cover.h
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:310
impact_modet
impact_modet
Definition: change_impact.h:18
string_abstraction.h
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:60
rewrite_union.h
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:28
impact_modet::BACKWARD
@ BACKWARD
goto_inline.h
optionst
Definition: options.h:23
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:168
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:400
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
remove_asm.h
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
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:2143
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:283
impact_modet::BOTH
@ BOTH
configt::ansi_c
struct configt::ansi_ct ansi_c
version.h
string_instrumentation.h
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
instrument_cover_goals
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)
Applies instrumenters to given goto program.
Definition: cover.cpp:33
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:45
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:141
unified_diff.h
remove_complex.h
set_properties.h
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:171
goto_difft::output_functions
virtual void output_functions() const
Output diff result.
Definition: goto_diff_base.cpp:21
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:385
initialize_goto_model.h
goto_diff.h
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:146
mm_io.h
goto_diff_parse_optionst::help
virtual void help()
display command line help
Definition: goto_diff_parse_options.cpp:384
instrument_preconditions
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Definition: instrument_preconditions.cpp:90
syntactic_diff.h
show_properties.h
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:143
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:46
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
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:1375
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:137
goto_diff_parse_options.h
impact_modet::FORWARD
@ FORWARD
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
read_goto_binary.h
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_complex
static void remove_complex(typet &)
removes complex data type
Definition: remove_complex.cpp:231
remove_returns.h
remove_unused_functions.h
goto_diff_parse_optionst::doit
virtual int doit()
invoke main modules
Definition: goto_diff_parse_options.cpp:215
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:1275
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:44
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:77
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:768
exit_codes.h
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
config.h
loop_ids.h
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
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_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:99
remove_skip.h
adjust_float_expressions.h
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:107
remove_function_pointers.h
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:133
cprover_library.h
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:105
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:142
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