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 <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 
32 #include <goto-programs/loop_ids.h>
33 #include <goto-programs/mm_io.h>
46 
48 
49 #include <goto-instrument/cover.h>
50 
52 
56 
57 #include <langapi/mode.h>
58 
59 #include "java_syntactic_diff.h"
61 #include <goto-diff/goto_diff.h>
62 #include <goto-diff/unified_diff.h>
63 
64 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
65  : parse_options_baset(JDIFF_OPTIONS, argc, argv),
66  jdiff_languagest(cmdline, ui_message_handler),
67  ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION),
68  languages2(cmdline, ui_message_handler)
69 {
70 }
71 
73  int argc,
74  const char **argv,
75  const std::string &extra_options)
76  : parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv),
77  jdiff_languagest(cmdline, ui_message_handler),
78  ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION),
79  languages2(cmdline, ui_message_handler)
80 {
81 }
82 
84 {
85  if(config.set(cmdline))
86  {
87  usage_error();
88  exit(1);
89  }
90 
91  // TODO: improve this when language front ends have been
92  // disentangled from command line parsing
93  // we always require these options
94  cmdline.set("no-lazy-methods");
95  cmdline.set("no-refine-strings");
96 
97  if(cmdline.isset("cover"))
98  parse_cover_options(cmdline, options);
99 
100  if(cmdline.isset("mm"))
101  options.set_option("mm", cmdline.get_value("mm"));
102 
103  // all checks supported by goto_check
105 
106  if(cmdline.isset("debug-level"))
107  options.set_option("debug-level", cmdline.get_value("debug-level"));
108 
109  if(cmdline.isset("slice-by-trace"))
110  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
111 
112  if(cmdline.isset("unwindset"))
113  options.set_option("unwindset", cmdline.get_value("unwindset"));
114 
115  // constant propagation
116  if(cmdline.isset("no-propagation"))
117  options.set_option("propagation", false);
118  else
119  options.set_option("propagation", true);
120 
121  // check array bounds
122  if(cmdline.isset("bounds-check"))
123  options.set_option("bounds-check", true);
124  else
125  options.set_option("bounds-check", false);
126 
127  // check division by zero
128  if(cmdline.isset("div-by-zero-check"))
129  options.set_option("div-by-zero-check", true);
130  else
131  options.set_option("div-by-zero-check", false);
132 
133  // check overflow/underflow
134  if(cmdline.isset("signed-overflow-check"))
135  options.set_option("signed-overflow-check", true);
136  else
137  options.set_option("signed-overflow-check", false);
138 
139  // check overflow/underflow
140  if(cmdline.isset("unsigned-overflow-check"))
141  options.set_option("unsigned-overflow-check", true);
142  else
143  options.set_option("unsigned-overflow-check", false);
144 
145  // check overflow/underflow
146  if(cmdline.isset("float-overflow-check"))
147  options.set_option("float-overflow-check", true);
148  else
149  options.set_option("float-overflow-check", false);
150 
151  // check for NaN (not a number)
152  if(cmdline.isset("nan-check"))
153  options.set_option("nan-check", true);
154  else
155  options.set_option("nan-check", false);
156 
157  // check pointers
158  if(cmdline.isset("pointer-check"))
159  options.set_option("pointer-check", true);
160  else
161  options.set_option("pointer-check", false);
162 
163  // check for memory leaks
164  if(cmdline.isset("memory-leak-check"))
165  options.set_option("memory-leak-check", true);
166  else
167  options.set_option("memory-leak-check", false);
168 
169  // check assertions
170  if(cmdline.isset("no-assertions"))
171  options.set_option("assertions", false);
172  else
173  options.set_option("assertions", true);
174 
175  // use assumptions
176  if(cmdline.isset("no-assumptions"))
177  options.set_option("assumptions", false);
178  else
179  options.set_option("assumptions", true);
180 
181  // magic error label
182  if(cmdline.isset("error-label"))
183  options.set_option("error-label", cmdline.get_values("error-label"));
184 
185  options.set_option("show-properties", cmdline.isset("show-properties"));
186 }
187 
190 {
191  if(cmdline.isset("version"))
192  {
193  std::cout << CBMC_VERSION << '\n';
194  return CPROVER_EXIT_SUCCESS;
195  }
196 
197  //
198  // command line options
199  //
200 
201  optionst options;
202  get_command_line_options(options);
205 
206  //
207  // Print a banner
208  //
209  status() << "JDIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8
210  << "-bit " << config.this_architecture() << " "
212 
213  if(cmdline.args.size() != 2)
214  {
215  error() << "Please provide two programs to compare" << eom;
217  }
218 
219  goto_modelt goto_model1, goto_model2;
220 
221  int get_goto_program_ret = get_goto_program(options, *this, goto_model1);
222  if(get_goto_program_ret != -1)
223  return get_goto_program_ret;
224  get_goto_program_ret = get_goto_program(options, languages2, goto_model2);
225  if(get_goto_program_ret != -1)
226  return get_goto_program_ret;
227 
228  if(cmdline.isset("show-loops"))
229  {
230  show_loop_ids(get_ui(), goto_model1);
231  show_loop_ids(get_ui(), goto_model2);
232  return CPROVER_EXIT_SUCCESS;
233  }
234 
235  if(
236  cmdline.isset("show-goto-functions") ||
237  cmdline.isset("list-goto-functions"))
238  {
240  goto_model1,
243  cmdline.isset("list-goto-functions"));
245  goto_model2,
248  cmdline.isset("list-goto-functions"));
249  return CPROVER_EXIT_SUCCESS;
250  }
251 
252  if(
253  cmdline.isset("change-impact") || cmdline.isset("forward-impact") ||
254  cmdline.isset("backward-impact"))
255  {
256  impact_modet impact_mode =
257  cmdline.isset("forward-impact")
259  : (cmdline.isset("backward-impact") ? impact_modet::BACKWARD
262  goto_model1, goto_model2, impact_mode, cmdline.isset("compact-output"));
263 
264  return CPROVER_EXIT_SUCCESS;
265  }
266 
267  if(cmdline.isset("unified") || cmdline.isset('u'))
268  {
269  unified_difft u(goto_model1, goto_model2);
270  u();
271  u.output(std::cout);
272 
273  return CPROVER_EXIT_SUCCESS;
274  }
275 
277  goto_model1, goto_model2, options, get_message_handler());
278  sd.set_ui(get_ui());
279  sd();
280  sd.output_functions();
281 
282  return CPROVER_EXIT_SUCCESS;
283 }
284 
286  const optionst &options,
288  goto_modelt &goto_model)
289 {
290  status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
291 
292  if(is_goto_binary(cmdline.args[0]))
293  {
294  if(read_goto_binary(
295  cmdline.args[0],
296  goto_model.symbol_table,
297  goto_model.goto_functions,
298  languages.get_message_handler()))
300 
301  config.set(cmdline);
302 
303  // This one is done.
304  cmdline.args.erase(cmdline.args.begin());
305  }
306  else
307  {
308  // This is a a workaround to make parse() think that there is only
309  // one source file.
310  std::string arg2("");
311  if(cmdline.args.size() == 2)
312  {
313  arg2 = cmdline.args[1];
314  cmdline.args.erase(--cmdline.args.end());
315  }
316 
317  if(languages.parse() || languages.typecheck() || languages.final())
319 
320  // we no longer need any parse trees or language files
321  languages.clear_parse();
322 
323  status() << "Generating GOTO Program" << eom;
324 
325  goto_model.symbol_table = languages.symbol_table;
326  goto_convert(
327  goto_model.symbol_table, goto_model.goto_functions, ui_message_handler);
328 
329  if(process_goto_program(options, goto_model))
331 
332  // if we had a second argument then we will handle it next
333  if(arg2 != "")
334  cmdline.args[0] = arg2;
335  }
336 
337  return -1; // no error, continue
338 }
339 
341  const optionst &options,
342  goto_modelt &goto_model)
343 {
344  try
345  {
346  // remove function pointers
347  status() << "Removal of function pointers and virtual functions" << eom;
349  get_message_handler(), goto_model, cmdline.isset("pointer-check"));
350 
351  // Java virtual functions -> explicit dispatch tables:
352  remove_virtual_functions(goto_model);
353  // remove catch and throw
354  remove_exceptions(goto_model, get_message_handler());
355  // Java instanceof -> clsid comparison:
356  remove_instanceof(goto_model, get_message_handler());
357 
358  mm_io(goto_model);
359 
360  // instrument library preconditions
361  instrument_preconditions(goto_model);
362 
363  // remove returns, gcc vectors, complex
364  remove_returns(goto_model);
365  remove_vector(goto_model);
366  remove_complex(goto_model);
367  rewrite_union(goto_model);
368 
369  // add generic checks
370  status() << "Generic Property Instrumentation" << eom;
371  goto_check(options, goto_model);
372 
373  // checks don't know about adjusted float expressions
374  adjust_float_expressions(goto_model);
375 
376  // recalculate numbers, etc.
377  goto_model.goto_functions.update();
378 
379  // add loop ids
381 
382  // remove skips such that trivial GOTOs are deleted and not considered
383  // for coverage annotation:
384  remove_skip(goto_model);
385 
386  // instrument cover goals
387  if(cmdline.isset("cover"))
388  {
389  if(instrument_cover_goals(options, goto_model, get_message_handler()))
390  return true;
391  }
392 
393  // label the assertions
394  // This must be done after adding assertions and
395  // before using the argument of the "property" option.
396  // Do not re-label after using the property slicer because
397  // this would cause the property identifiers to change.
398  label_properties(goto_model);
399 
400  // remove any skips introduced since coverage instrumentation
401  remove_skip(goto_model);
402  goto_model.goto_functions.update();
403  }
404 
405  catch(const char *e)
406  {
407  error() << e << eom;
408  return true;
409  }
410 
411  catch(const std::string &e)
412  {
413  error() << e << eom;
414  return true;
415  }
416 
417  catch(int e)
418  {
419  error() << "Numeric exception: " << e << eom;
420  return true;
421  }
422 
423  catch(const std::bad_alloc &)
424  {
425  error() << "Out of memory" << eom;
427  return true;
428  }
429 
430  return false;
431 }
432 
435 {
436  // clang-format off
437  std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n'
438  <<
439  "* * Copyright (C) 2016-2018 * *\n"
440  "* * Daniel Kroening, Peter Schrammel * *\n"
441  "* * kroening@kroening.com * *\n"
442  "\n"
443  "Usage: Purpose:\n"
444  "\n"
445  " jdiff [-?] [-h] [--help] show help\n"
446  " jdiff old new jars to be compared\n"
447  "\n"
448  "Diff options:\n"
451  " --syntactic do syntactic diff (default)\n"
452  " -u | --unified output unified diff\n"
453  " --change-impact | \n"
454  " --forward-impact |\n"
455  // NOLINTNEXTLINE(whitespace/line_length)
456  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
457  " --compact-output output dependencies in compact mode\n"
458  "\n"
459  "Program instrumentation options:\n"
461  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
462  "Java Bytecode frontend options:\n"
464  "Other options:\n"
465  " --version show version and exit\n"
466  " --json-ui use JSON-formatted output\n"
468  "\n";
469  // clang-format on
470 }
void set_ui(ui_message_handlert::uit _ui)
Definition: goto_diff.h:44
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
Symbolic Execution.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
Remove function exceptional returns.
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Remove Instance-of Operators.
Remove Indirect Function Calls.
Remove Virtual Function (Method) Calls.
uit get_ui() const
Definition: ui_message.h:37
impact_modet
Definition: change_impact.h:18
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
uit get_ui()
Definition: language_ui.h:48
void compute_loop_numbers()
Data and control-dependencies of syntactic diff.
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:78
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
Remove the &#39;complex&#39; data type by compilation into structs.
std::string get_value(char option) const
Definition: cmdline.cpp:45
STL namespace.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Pointer Dereferencing.
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:41
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
String Abstraction.
configt config
Definition: config.cpp:23
void remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Syntactic GOTO-DIFF for Java.
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
jdiff_languagest languages2
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:163
Set the properties to check.
#define HELP_GOTO_CHECK
Definition: goto_check.h:42
Unused function removal.
bool set(const cmdlinet &cmdline)
Definition: config.cpp:738
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
Perform Memory-mapped I/O instrumentation.
#define HELP_TIMESTAMP
Definition: timestamper.h:14
argst args
Definition: cmdline.h:37
ui_message_handlert ui_message_handler
virtual bool isset(char option) const
Definition: cmdline.cpp:27
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler, remove_exceptions_typest type)
removes throws/CATCH-POP/CATCH-PUSH
String Abstraction.
#define HELP_SHOW_PROPERTIES
virtual bool process_goto_program(const optionst &options, goto_modelt &goto_model)
virtual void output_functions() const
Output diff result.
virtual void set(const std::string &option)
Definition: cmdline.cpp:60
mstreamt & error() const
Definition: message.h:302
Function Inlining.
Abstract interface to support a programming language.
Loop IDs.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
Remove function returns.
std::string banner_string(const std::string &front_end, const std::string &version)
void instrument_cover_goals(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
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:56
Symbolic Execution.
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
Unified diff (using LCSS) of goto functions.
virtual int doit()
invoke main modules
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
virtual int get_goto_program(const optionst &options, jdiff_languagest &languages, goto_modelt &goto_model)
static irep_idt this_operating_system()
Definition: config.cpp:1310
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:48
message_handlert & get_message_handler()
Definition: message.h:153
Goto Programs with Functions.
void output(std::ostream &os) const
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & status() const
Definition: message.h:317
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
Definition: version.cpp:1
virtual void get_command_line_options(optionst &options)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
#define JDIFF_OPTIONS
Remove the &#39;vector&#39; data type by compilation into arrays.
Options.
virtual void usage_error()
Show the properties.
void rewrite_union(exprt &expr, const namespacet &ns)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
Coverage Instrumentation.
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files...
Definition: exit_codes.h:45
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
JDIFF Command Line Option Processing.
static void remove_complex(typet &)
removes complex data type
Program Transformation.
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:33
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
void label_properties(goto_modelt &goto_model)
jdiff_parse_optionst(int argc, const char **argv)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
languagest languages
Definition: mode.cpp:32
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
Definition: config.cpp:1213
virtual void help()
display command line help
GOTO-DIFF Base Class.