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") ?
209  impact_modet::FORWARD :
210  (cmdline.isset("backward-impact") ?
211  impact_modet::BACKWARD :
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 }
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:143
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:239
impact_modet
impact_modet
Definition: change_impact.h:18
string_abstraction.h
String Abstraction.
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:71
rewrite_union.h
Symbolic Execution.
unified_difft::output
void output(std::ostream &os) const
Definition: unified_diff.cpp:375
add_malloc_may_fail_variable_initializations.h
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:31
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
goto_inline.h
Function Inlining.
optionst
Definition: options.h:23
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:171
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:755
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
HELP_COVER
#define HELP_COVER
Definition: cover.h:30
options.h
Options.
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
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:180
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:286
syntactic_diff.h
Syntactic GOTO-DIFF.
show_properties.h
Show the properties.
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
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:1426
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:165
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.
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
add_malloc_may_fail_variable_initializations
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 ...
Definition: add_malloc_may_fail_variable_initializations.cpp:24
remove_vector.h
Remove the 'vector' data type by compilation into arrays.
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:144
config
configt config
Definition: config.cpp:24
parse_options_baset::log
messaget log
Definition: parse_options.h:43
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1326
goto_diff_parse_optionst::goto_diff_parse_optionst
goto_diff_parse_optionst(int argc, const char **argv)
Definition: goto_diff_parse_options.cpp:68
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
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_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:511
change_impact.h
Data and control-dependencies of syntactic diff.
config.h
loop_ids.h
Loop IDs.
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:77
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.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
process_goto_program.h
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:106
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