cprover
jdiff_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JDIFF Command Line Option Processing
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "jdiff_parse_options.h"
13 
14 #include <cstdlib> // exit()
15 #include <iostream>
16 
17 #include <util/config.h>
18 #include <util/exit_codes.h>
19 #include <util/options.h>
20 #include <util/version.h>
21 
25 #include <goto-programs/loop_ids.h>
26 #include <goto-programs/mm_io.h>
36 
37 #include <goto-instrument/cover.h>
38 
42 
43 #include "java_syntactic_diff.h"
45 #include <goto-diff/unified_diff.h>
46 
47 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
50  argc,
51  argv,
52  std::string("JDIFF ") + CBMC_VERSION)
53 {
54 }
55 
57 {
58  if(config.set(cmdline))
59  {
60  usage_error();
61  exit(1);
62  }
63 
64  // TODO: improve this when language front ends have been
65  // disentangled from command line parsing
66  // we always require these options
67  cmdline.set("no-lazy-methods");
68  cmdline.set("no-refine-strings");
70 
71  if(cmdline.isset("cover"))
72  parse_cover_options(cmdline, options);
73 
74  if(cmdline.isset("mm"))
75  options.set_option("mm", cmdline.get_value("mm"));
76 
77  // all checks supported by goto_check
79 
80  if(cmdline.isset("debug-level"))
81  options.set_option("debug-level", cmdline.get_value("debug-level"));
82 
83  if(cmdline.isset("unwindset"))
84  options.set_option("unwindset", cmdline.get_value("unwindset"));
85 
86  // constant propagation
87  if(cmdline.isset("no-propagation"))
88  options.set_option("propagation", false);
89  else
90  options.set_option("propagation", true);
91 
92  // check array bounds
93  if(cmdline.isset("bounds-check"))
94  options.set_option("bounds-check", true);
95  else
96  options.set_option("bounds-check", false);
97 
98  // check division by zero
99  if(cmdline.isset("div-by-zero-check"))
100  options.set_option("div-by-zero-check", true);
101  else
102  options.set_option("div-by-zero-check", false);
103 
104  // check overflow/underflow
105  if(cmdline.isset("signed-overflow-check"))
106  options.set_option("signed-overflow-check", true);
107  else
108  options.set_option("signed-overflow-check", false);
109 
110  // check overflow/underflow
111  if(cmdline.isset("unsigned-overflow-check"))
112  options.set_option("unsigned-overflow-check", true);
113  else
114  options.set_option("unsigned-overflow-check", false);
115 
116  // check overflow/underflow
117  if(cmdline.isset("float-overflow-check"))
118  options.set_option("float-overflow-check", true);
119  else
120  options.set_option("float-overflow-check", false);
121 
122  // check for NaN (not a number)
123  if(cmdline.isset("nan-check"))
124  options.set_option("nan-check", true);
125  else
126  options.set_option("nan-check", false);
127 
128  // check pointers
129  if(cmdline.isset("pointer-check"))
130  options.set_option("pointer-check", true);
131  else
132  options.set_option("pointer-check", false);
133 
134  // check for memory leaks
135  if(cmdline.isset("memory-leak-check"))
136  options.set_option("memory-leak-check", true);
137  else
138  options.set_option("memory-leak-check", false);
139 
140  // check assertions
141  if(cmdline.isset("no-assertions"))
142  options.set_option("assertions", false);
143  else
144  options.set_option("assertions", true);
145 
146  // use assumptions
147  if(cmdline.isset("no-assumptions"))
148  options.set_option("assumptions", false);
149  else
150  options.set_option("assumptions", true);
151 
152  // magic error label
153  if(cmdline.isset("error-label"))
154  options.set_option("error-label", cmdline.get_values("error-label"));
155 
156  options.set_option("show-properties", cmdline.isset("show-properties"));
157 }
158 
161 {
162  if(cmdline.isset("version"))
163  {
164  std::cout << CBMC_VERSION << '\n';
165  return CPROVER_EXIT_SUCCESS;
166  }
167 
168  //
169  // command line options
170  //
171 
172  optionst options;
173  get_command_line_options(options);
176 
178 
179  if(cmdline.args.size() != 2)
180  {
181  log.error() << "Please provide two programs to compare" << messaget::eom;
183  }
184 
186 
187  goto_modelt goto_model1 =
189  if(process_goto_program(options, goto_model1))
191  goto_modelt goto_model2 =
193  if(process_goto_program(options, goto_model2))
195 
196  if(cmdline.isset("show-loops"))
197  {
198  show_loop_ids(ui_message_handler.get_ui(), goto_model1);
199  show_loop_ids(ui_message_handler.get_ui(), goto_model2);
200  return CPROVER_EXIT_SUCCESS;
201  }
202 
203  if(
204  cmdline.isset("show-goto-functions") ||
205  cmdline.isset("list-goto-functions"))
206  {
208  goto_model1, ui_message_handler, cmdline.isset("list-goto-functions"));
210  goto_model2, ui_message_handler, cmdline.isset("list-goto-functions"));
211  return CPROVER_EXIT_SUCCESS;
212  }
213 
214  if(
215  cmdline.isset("change-impact") || cmdline.isset("forward-impact") ||
216  cmdline.isset("backward-impact"))
217  {
218  impact_modet impact_mode =
219  cmdline.isset("forward-impact")
221  : (cmdline.isset("backward-impact") ? impact_modet::BACKWARD
224  goto_model1, goto_model2, impact_mode, cmdline.isset("compact-output"));
225 
226  return CPROVER_EXIT_SUCCESS;
227  }
228 
229  if(cmdline.isset("unified") || cmdline.isset('u'))
230  {
231  unified_difft u(goto_model1, goto_model2);
232  u();
233  u.output(std::cout);
234 
235  return CPROVER_EXIT_SUCCESS;
236  }
237 
239  goto_model1, goto_model2, options, ui_message_handler);
240  sd();
241  sd.output_functions();
242 
243  return CPROVER_EXIT_SUCCESS;
244 }
245 
247  const optionst &options,
248  goto_modelt &goto_model)
249 {
250  {
251  // remove function pointers
252  log.status() << "Removing function pointers and virtual functions"
253  << messaget::eom;
255  ui_message_handler, goto_model, cmdline.isset("pointer-check"));
256 
257  // Java virtual functions -> explicit dispatch tables:
258  remove_virtual_functions(goto_model);
259 
260  // remove Java throw and catch
261  // This introduces instanceof, so order is important:
263 
264  // Java instanceof -> clsid comparison:
265  class_hierarchyt class_hierarchy(goto_model.symbol_table);
266  remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
267 
268  mm_io(goto_model);
269 
270  // instrument library preconditions
271  instrument_preconditions(goto_model);
272 
273  // remove returns, gcc vectors, complex
274  remove_returns(goto_model);
275  remove_vector(goto_model);
276  remove_complex(goto_model);
277  rewrite_union(goto_model);
278 
279  // add generic checks
280  log.status() << "Generic Property Instrumentation" << messaget::eom;
281  goto_check(options, goto_model);
282 
283  // checks don't know about adjusted float expressions
284  adjust_float_expressions(goto_model);
285 
286  // recalculate numbers, etc.
287  goto_model.goto_functions.update();
288 
289  // add loop ids
291 
292  // remove skips such that trivial GOTOs are deleted and not considered
293  // for coverage annotation:
294  remove_skip(goto_model);
295 
296  // instrument cover goals
297  if(cmdline.isset("cover"))
298  {
299  const auto cover_config =
300  get_cover_config(options, goto_model.symbol_table, ui_message_handler);
301  if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
302  return true;
303  }
304 
305  // label the assertions
306  // This must be done after adding assertions and
307  // before using the argument of the "property" option.
308  // Do not re-label after using the property slicer because
309  // this would cause the property identifiers to change.
310  label_properties(goto_model);
311 
312  // remove any skips introduced since coverage instrumentation
313  remove_skip(goto_model);
314  goto_model.goto_functions.update();
315  }
316 
317  return false;
318 }
319 
322 {
323  // clang-format off
324  std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n'
325  << align_center_with_border("Copyright (C) 2016-2018") << '\n'
326  << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT(*)
327  << align_center_with_border("kroening@kroening.com") << '\n'
328  <<
329  "\n"
330  "Usage: Purpose:\n"
331  "\n"
332  " jdiff [-?] [-h] [--help] show help\n"
333  " jdiff old new jars to be compared\n"
334  "\n"
335  "Diff options:\n"
338  " --syntactic do syntactic diff (default)\n"
339  " -u | --unified output unified diff\n"
340  " --change-impact | \n"
341  " --forward-impact |\n"
342  // NOLINTNEXTLINE(whitespace/line_length)
343  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
344  " --compact-output output dependencies in compact mode\n"
345  "\n"
346  "Program instrumentation options:\n"
348  HELP_COVER
349  "Java Bytecode frontend options:\n"
351  "Other options:\n"
352  " --version show version and exit\n"
353  " --json-ui use JSON-formatted output\n"
355  "\n";
356  // clang-format on
357 }
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Symbolic Execution.
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
Non-graph-based representation of the class hierarchy.
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
virtual void set(const std::string &option, bool value=true)
Set option option to value, or true if the value is omitted.
Definition: cmdline.cpp:57
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
virtual void output_functions() const
Output diff result.
void compute_loop_numbers()
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
jdiff_parse_optionst(int argc, const char **argv)
void register_languages() override
void help() override
display command line help
bool process_goto_program(const optionst &options, goto_modelt &goto_model)
void get_command_line_options(optionst &options)
int doit() override
invoke main modules
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
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
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
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:70
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
Syntactic GOTO-DIFF for Java.
JDIFF Command Line Option Processing.
#define JDIFF_OPTIONS
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
Loop IDs.
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:36
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)
static void remove_complex(typet &)
removes complex data type
Remove the 'complex' data type by compilation into structs.
void remove_exceptions_using_instanceof(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
Remove function exceptional returns.
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)
Remove Indirect Function Calls.
void remove_instanceof(const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
Remove Instance-of Operators.
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
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:86
Program Transformation.
static void remove_vector(typet &)
removes vector data type
Remove the 'vector' data type by compilation into arrays.
void remove_virtual_functions(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
Functions for replacing virtual function call with a static function calls in functions,...
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
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
#define HELP_TIMESTAMP
Definition: timestamper.h:14
Unified diff (using LCSS) of goto functions.
const char * CBMC_VERSION