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 
34 #include <goto-programs/loop_ids.h>
35 #include <goto-programs/mm_io.h>
50 
51 #include <goto-instrument/cover.h>
52 
54 
55 #include <langapi/mode.h>
56 
57 #include <ansi-c/cprover_library.h>
58 
59 #include <assembler/remove_asm.h>
60 
61 #include <cpp/cprover_library.h>
62 
63 #include "goto_diff.h"
64 #include "syntactic_diff.h"
65 #include "unified_diff.h"
66 #include "change_impact.h"
67 
71  argc,
72  argv,
73  std::string("GOTO-DIFF ") + CBMC_VERSION)
74 {
75 }
76 
78 {
79  if(config.set(cmdline))
80  {
81  usage_error();
82  exit(1);
83  }
84 
85  if(cmdline.isset("program-only"))
86  options.set_option("program-only", true);
87 
88  if(cmdline.isset("show-byte-ops"))
89  options.set_option("show-byte-ops", true);
90 
91  if(cmdline.isset("show-vcc"))
92  options.set_option("show-vcc", true);
93 
94  if(cmdline.isset("cover"))
95  parse_cover_options(cmdline, options);
96 
97  if(cmdline.isset("mm"))
98  options.set_option("mm", cmdline.get_value("mm"));
99 
100  // all checks supported by goto_check
102 
103  if(cmdline.isset("debug-level"))
104  options.set_option("debug-level", cmdline.get_value("debug-level"));
105 
106  if(cmdline.isset("unwindset"))
107  options.set_option("unwindset", cmdline.get_value("unwindset"));
108 
109  // constant propagation
110  if(cmdline.isset("no-propagation"))
111  options.set_option("propagation", false);
112  else
113  options.set_option("propagation", true);
114 
115  // all checks supported by goto_check
117 
118  // generate unwinding assertions
119  if(cmdline.isset("cover"))
120  options.set_option("unwinding-assertions", false);
121  else
122  options.set_option(
123  "unwinding-assertions",
124  cmdline.isset("unwinding-assertions"));
125 
126  // generate unwinding assumptions otherwise
127  options.set_option("partial-loops", cmdline.isset("partial-loops"));
128 
129  if(options.get_bool_option("partial-loops") &&
130  options.get_bool_option("unwinding-assertions"))
131  {
132  log.error() << "--partial-loops and --unwinding-assertions"
133  << " must not be given together" << messaget::eom;
134  exit(1);
135  }
136 
137  options.set_option("show-properties", cmdline.isset("show-properties"));
138 
139  // Options for process_goto_program
140  options.set_option("rewrite-union", true);
141 }
142 
145 {
146  if(cmdline.isset("version"))
147  {
148  std::cout << CBMC_VERSION << '\n';
149  return CPROVER_EXIT_SUCCESS;
150  }
151 
152  //
153  // command line options
154  //
155 
156  optionst options;
157  get_command_line_options(options);
160 
161  //
162  // Print a banner
163  //
164  log.status() << "GOTO-DIFF version " << CBMC_VERSION << " "
165  << sizeof(void *) * 8 << "-bit " << config.this_architecture()
167 
168  if(cmdline.args.size()!=2)
169  {
170  log.error() << "Please provide two programs to compare" << messaget::eom;
172  }
173 
175 
176  goto_modelt goto_model1 =
178  if(process_goto_program(options, goto_model1))
180  goto_modelt goto_model2 =
182  if(process_goto_program(options, goto_model2))
184 
185  if(cmdline.isset("show-loops"))
186  {
187  show_loop_ids(ui_message_handler.get_ui(), goto_model1);
188  show_loop_ids(ui_message_handler.get_ui(), goto_model2);
189  return CPROVER_EXIT_SUCCESS;
190  }
191 
192  if(
193  cmdline.isset("show-goto-functions") ||
194  cmdline.isset("list-goto-functions"))
195  {
197  goto_model1, ui_message_handler, cmdline.isset("list-goto-functions"));
199  goto_model2, ui_message_handler, cmdline.isset("list-goto-functions"));
200  return CPROVER_EXIT_SUCCESS;
201  }
202 
203  if(cmdline.isset("change-impact") ||
204  cmdline.isset("forward-impact") ||
205  cmdline.isset("backward-impact"))
206  {
207  impact_modet impact_mode=
208  cmdline.isset("forward-impact") ?
210  (cmdline.isset("backward-impact") ?
214  goto_model1,
215  goto_model2,
216  impact_mode,
217  cmdline.isset("compact-output"));
218 
219  return CPROVER_EXIT_SUCCESS;
220  }
221 
222  if(cmdline.isset("unified") ||
223  cmdline.isset('u'))
224  {
225  unified_difft u(goto_model1, goto_model2);
226  u();
227  u.output(std::cout);
228 
229  return CPROVER_EXIT_SUCCESS;
230  }
231 
232  syntactic_difft sd(goto_model1, goto_model2, options, ui_message_handler);
233  sd();
234  sd.output_functions();
235 
236  return CPROVER_EXIT_SUCCESS;
237 }
238 
240  const optionst &options,
241  goto_modelt &goto_model)
242 {
243  // Remove inline assembler; this needs to happen before
244  // adding the library.
245  remove_asm(goto_model);
246 
247  // add the library
248  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
249  << messaget::eom;
252 
254 
255  // Common removal of types and complex constructs
256  if(::process_goto_program(goto_model, options, log))
257  return true;
258 
259  // instrument cover goals
260  if(cmdline.isset("cover"))
261  {
262  // remove skips such that trivial GOTOs are deleted and not considered
263  // for coverage annotation:
264  remove_skip(goto_model);
265 
266  const auto cover_config =
267  get_cover_config(options, goto_model.symbol_table, ui_message_handler);
268  if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
269  return true;
270  }
271 
272  // label the assertions
273  // This must be done after adding assertions and
274  // before using the argument of the "property" option.
275  // Do not re-label after using the property slicer because
276  // this would cause the property identifiers to change.
277  label_properties(goto_model);
278 
279  // remove any skips introduced since coverage instrumentation
280  remove_skip(goto_model);
281 
282  return false;
283 }
284 
287 {
288  // clang-format off
289  std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n'
290  << align_center_with_border("Copyright (C) 2016") << '\n'
291  << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT (*)
292  << align_center_with_border("kroening@kroening.com") << '\n'
293  <<
294  "\n"
295  "Usage: Purpose:\n"
296  "\n"
297  " goto_diff [-?] [-h] [--help] show help\n"
298  " goto_diff old new goto binaries to be compared\n"
299  "\n"
300  "Diff options:\n"
303  " --syntactic do syntactic diff (default)\n"
304  " -u | --unified output unified diff\n"
305  " --change-impact | \n"
306  " --forward-impact |\n"
307  // NOLINTNEXTLINE(whitespace/line_length)
308  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
309  " --compact-output output dependencies in compact mode\n"
310  "\n"
311  "Program instrumentation options:\n"
313  HELP_COVER
314  "\n"
315  "Other options:\n"
316  " --version show version and exit\n"
317  " --json-ui use JSON-formatted output\n"
318  HELP_FLUSH
320  "\n";
321  // clang-format on
322 }
Pointer Dereferencing.
void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
Some variables have different initial values based on what flags are being passed to cbmc; since the ...
Symbolic Execution.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
Data and control-dependencies of syntactic diff.
impact_modet
Definition: change_impact.h:18
std::string get_value(char option) const
Definition: cmdline.cpp:47
virtual bool isset(char option) const
Definition: cmdline.cpp:29
argst args
Definition: cmdline.h:143
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
static irep_idt this_architecture()
Definition: config.cpp:1326
static irep_idt this_operating_system()
Definition: config.cpp:1426
struct configt::ansi_ct ansi_c
bool process_goto_program(const optionst &options, goto_modelt &goto_model)
virtual int doit()
invoke main modules
goto_diff_parse_optionst(int argc, const char **argv)
void get_command_line_options(optionst &options)
virtual void help()
display command line help
virtual void output_functions() const
Output diff result.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
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
mstreamt & error() const
Definition: message.h:399
mstreamt & status() const
Definition: message.h:414
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
virtual void usage_error()
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
virtual uit get_ui() const
Definition: ui_message.h:31
void output(std::ostream &os) const
configt config
Definition: config.cpp:24
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
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:180
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:142
Coverage Instrumentation.
#define HELP_COVER
Definition: cover.h:30
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
#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
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:71
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
Goto Programs with Functions.
GOTO-DIFF Base Class.
GOTO-DIFF Command Line Option Processing.
#define GOTO_DIFF_OPTIONS
Function Inlining.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
Abstract interface to support a programming language.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:19
Loop IDs.
Perform Memory-mapped I/O instrumentation.
Options.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
Read Goto Programs.
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:511
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
Remove the 'complex' data type by compilation into structs.
Remove Indirect Function Calls.
Replace function returns by assignments to global variables.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
Program Transformation.
Unused function removal.
Remove the 'vector' data type by compilation into arrays.
Functions for replacing virtual function call with a static function calls in functions,...
Symbolic Execution.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
#define HELP_SHOW_GOTO_FUNCTIONS
Show the properties.
#define HELP_SHOW_PROPERTIES
String Abstraction.
String Abstraction.
irep_idt arch
Definition: config.h:165
Syntactic GOTO-DIFF.
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:106
Unified diff (using LCSS) of goto functions.
const char * CBMC_VERSION