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 
18 #include <util/config.h>
19 #include <util/exit_codes.h>
20 #include <util/options.h>
21 #include <util/version.h>
22 
26 #include <goto-programs/loop_ids.h>
31 
32 #include <goto-instrument/cover.h>
33 
34 #include <ansi-c/cprover_library.h>
35 
36 #include <assembler/remove_asm.h>
37 
38 #include <cpp/cprover_library.h>
39 
40 #include "syntactic_diff.h"
41 #include "unified_diff.h"
42 #include "change_impact.h"
43 
47  argc,
48  argv,
49  std::string("GOTO-DIFF ") + CBMC_VERSION)
50 {
51 }
52 
54 {
55  if(config.set(cmdline))
56  {
57  usage_error();
58  exit(1);
59  }
60 
61  if(cmdline.isset("program-only"))
62  options.set_option("program-only", true);
63 
64  if(cmdline.isset("show-byte-ops"))
65  options.set_option("show-byte-ops", true);
66 
67  if(cmdline.isset("show-vcc"))
68  options.set_option("show-vcc", true);
69 
70  if(cmdline.isset("cover"))
71  parse_cover_options(cmdline, options);
72 
73  if(cmdline.isset("mm"))
74  options.set_option("mm", cmdline.get_value("mm"));
75 
76  // all checks supported by goto_check
78 
79  if(cmdline.isset("debug-level"))
80  options.set_option("debug-level", cmdline.get_value("debug-level"));
81 
82  if(cmdline.isset("unwindset"))
83  options.set_option("unwindset", cmdline.get_value("unwindset"));
84 
85  // constant propagation
86  if(cmdline.isset("no-propagation"))
87  options.set_option("propagation", false);
88  else
89  options.set_option("propagation", true);
90 
91  // all checks supported by goto_check
93 
94  // generate unwinding assertions
95  if(cmdline.isset("cover"))
96  options.set_option("unwinding-assertions", false);
97  else
98  options.set_option(
99  "unwinding-assertions",
100  cmdline.isset("unwinding-assertions"));
101 
102  // generate unwinding assumptions otherwise
103  options.set_option("partial-loops", cmdline.isset("partial-loops"));
104 
105  if(options.get_bool_option("partial-loops") &&
106  options.get_bool_option("unwinding-assertions"))
107  {
108  log.error() << "--partial-loops and --unwinding-assertions"
109  << " must not be given together" << messaget::eom;
110  exit(1);
111  }
112 
113  options.set_option("show-properties", cmdline.isset("show-properties"));
114 
115  // Options for process_goto_program
116  options.set_option("rewrite-union", true);
117 }
118 
121 {
122  if(cmdline.isset("version"))
123  {
124  std::cout << CBMC_VERSION << '\n';
125  return CPROVER_EXIT_SUCCESS;
126  }
127 
128  //
129  // command line options
130  //
131 
132  optionst options;
133  get_command_line_options(options);
136 
137  log_version_and_architecture("GOTO-DIFF");
138 
139  if(cmdline.args.size()!=2)
140  {
141  log.error() << "Please provide two programs to compare" << messaget::eom;
143  }
144 
146 
147  goto_modelt goto_model1 =
149  if(process_goto_program(options, goto_model1))
151  goto_modelt goto_model2 =
153  if(process_goto_program(options, goto_model2))
155 
156  if(cmdline.isset("show-loops"))
157  {
158  show_loop_ids(ui_message_handler.get_ui(), goto_model1);
159  show_loop_ids(ui_message_handler.get_ui(), goto_model2);
160  return CPROVER_EXIT_SUCCESS;
161  }
162 
163  if(
164  cmdline.isset("show-goto-functions") ||
165  cmdline.isset("list-goto-functions"))
166  {
168  goto_model1, ui_message_handler, cmdline.isset("list-goto-functions"));
170  goto_model2, ui_message_handler, cmdline.isset("list-goto-functions"));
171  return CPROVER_EXIT_SUCCESS;
172  }
173 
174  if(cmdline.isset("change-impact") ||
175  cmdline.isset("forward-impact") ||
176  cmdline.isset("backward-impact"))
177  {
178  impact_modet impact_mode=
179  cmdline.isset("forward-impact") ?
181  (cmdline.isset("backward-impact") ?
185  goto_model1,
186  goto_model2,
187  impact_mode,
188  cmdline.isset("compact-output"));
189 
190  return CPROVER_EXIT_SUCCESS;
191  }
192 
193  if(cmdline.isset("unified") ||
194  cmdline.isset('u'))
195  {
196  unified_difft u(goto_model1, goto_model2);
197  u();
198  u.output(std::cout);
199 
200  return CPROVER_EXIT_SUCCESS;
201  }
202 
203  syntactic_difft sd(goto_model1, goto_model2, options, ui_message_handler);
204  sd();
205  sd.output_functions();
206 
207  return CPROVER_EXIT_SUCCESS;
208 }
209 
211  const optionst &options,
212  goto_modelt &goto_model)
213 {
214  // Remove inline assembler; this needs to happen before
215  // adding the library.
216  remove_asm(goto_model);
217 
218  // add the library
219  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
220  << messaget::eom;
223 
225 
226  // Common removal of types and complex constructs
227  if(::process_goto_program(goto_model, options, log))
228  return true;
229 
230  // instrument cover goals
231  if(cmdline.isset("cover"))
232  {
233  // remove skips such that trivial GOTOs are deleted and not considered
234  // for coverage annotation:
235  remove_skip(goto_model);
236 
237  const auto cover_config =
238  get_cover_config(options, goto_model.symbol_table, ui_message_handler);
239  if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
240  return true;
241  }
242 
243  // label the assertions
244  // This must be done after adding assertions and
245  // before using the argument of the "property" option.
246  // Do not re-label after using the property slicer because
247  // this would cause the property identifiers to change.
248  label_properties(goto_model);
249 
250  // remove any skips introduced since coverage instrumentation
251  remove_skip(goto_model);
252 
253  return false;
254 }
255 
258 {
259  // clang-format off
260  std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n'
261  << align_center_with_border("Copyright (C) 2016") << '\n'
262  << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT (*)
263  << align_center_with_border("kroening@kroening.com") << '\n'
264  <<
265  "\n"
266  "Usage: Purpose:\n"
267  "\n"
268  " goto_diff [-?] [-h] [--help] show help\n"
269  " goto_diff old new goto binaries to be compared\n"
270  "\n"
271  "Diff options:\n"
274  " --syntactic do syntactic diff (default)\n"
275  " -u | --unified output unified diff\n"
276  " --change-impact | \n"
277  " --forward-impact |\n"
278  // NOLINTNEXTLINE(whitespace/line_length)
279  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
280  " --compact-output output dependencies in compact mode\n"
281  "\n"
282  "Program instrumentation options:\n"
284  HELP_COVER
285  "\n"
286  "Other options:\n"
287  " --version show version and exit\n"
288  " --json-ui use JSON-formatted output\n"
289  HELP_FLUSH
291  "\n";
292  // clang-format on
293 }
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 ...
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
struct configt::ansi_ct ansi_c
int doit() override
invoke main modules
bool process_goto_program(const optionst &options, goto_modelt &goto_model)
void help() override
display command line help
goto_diff_parse_optionst(int argc, const char **argv)
void get_command_line_options(optionst &options)
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:105
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()
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
virtual uit get_ui() const
Definition: ui_message.h:33
void output(std::ostream &os) const
configt config
Definition: config.cpp:25
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:32
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:70
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
GOTO-DIFF Command Line Option Processing.
#define GOTO_DIFF_OPTIONS
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
Loop IDs.
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)
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.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
Program Transformation.
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
irep_idt arch
Definition: config.h:164
Syntactic GOTO-DIFF.
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:108
Unified diff (using LCSS) of goto functions.
const char * CBMC_VERSION