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 
24 #include <langapi/language.h>
25 
31 #include <goto-programs/loop_ids.h>
32 #include <goto-programs/mm_io.h>
45 
47 
48 #include <goto-instrument/cover.h>
49 
51 
55 
56 #include <langapi/mode.h>
57 
58 #include "java_syntactic_diff.h"
60 #include <goto-diff/goto_diff.h>
61 #include <goto-diff/unified_diff.h>
62 
63 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
64  : parse_options_baset(JDIFF_OPTIONS, argc, argv),
65  jdiff_languagest(cmdline, ui_message_handler),
66  ui_message_handler(cmdline, "JDIFF " CBMC_VERSION),
67  languages2(cmdline, ui_message_handler)
68 {
69 }
70 
72  int argc,
73  const char **argv,
74  const std::string &extra_options)
75  : parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv),
76  jdiff_languagest(cmdline, ui_message_handler),
77  ui_message_handler(cmdline, "JDIFF " CBMC_VERSION),
78  languages2(cmdline, ui_message_handler)
79 {
80 }
81 
83 {
84  if(config.set(cmdline))
85  {
86  usage_error();
87  exit(1);
88  }
89 
90  if(cmdline.isset("cover"))
91  parse_cover_options(cmdline, options);
92 
93  if(cmdline.isset("mm"))
94  options.set_option("mm", cmdline.get_value("mm"));
95 
96  // all checks supported by goto_check
98 
99  if(cmdline.isset("debug-level"))
100  options.set_option("debug-level", cmdline.get_value("debug-level"));
101 
102  if(cmdline.isset("slice-by-trace"))
103  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
104 
105  if(cmdline.isset("unwindset"))
106  options.set_option("unwindset", cmdline.get_value("unwindset"));
107 
108  // constant propagation
109  if(cmdline.isset("no-propagation"))
110  options.set_option("propagation", false);
111  else
112  options.set_option("propagation", true);
113 
114  // check array bounds
115  if(cmdline.isset("bounds-check"))
116  options.set_option("bounds-check", true);
117  else
118  options.set_option("bounds-check", false);
119 
120  // check division by zero
121  if(cmdline.isset("div-by-zero-check"))
122  options.set_option("div-by-zero-check", true);
123  else
124  options.set_option("div-by-zero-check", false);
125 
126  // check overflow/underflow
127  if(cmdline.isset("signed-overflow-check"))
128  options.set_option("signed-overflow-check", true);
129  else
130  options.set_option("signed-overflow-check", false);
131 
132  // check overflow/underflow
133  if(cmdline.isset("unsigned-overflow-check"))
134  options.set_option("unsigned-overflow-check", true);
135  else
136  options.set_option("unsigned-overflow-check", false);
137 
138  // check overflow/underflow
139  if(cmdline.isset("float-overflow-check"))
140  options.set_option("float-overflow-check", true);
141  else
142  options.set_option("float-overflow-check", false);
143 
144  // check for NaN (not a number)
145  if(cmdline.isset("nan-check"))
146  options.set_option("nan-check", true);
147  else
148  options.set_option("nan-check", false);
149 
150  // check pointers
151  if(cmdline.isset("pointer-check"))
152  options.set_option("pointer-check", true);
153  else
154  options.set_option("pointer-check", false);
155 
156  // check for memory leaks
157  if(cmdline.isset("memory-leak-check"))
158  options.set_option("memory-leak-check", true);
159  else
160  options.set_option("memory-leak-check", false);
161 
162  // check assertions
163  if(cmdline.isset("no-assertions"))
164  options.set_option("assertions", false);
165  else
166  options.set_option("assertions", true);
167 
168  // use assumptions
169  if(cmdline.isset("no-assumptions"))
170  options.set_option("assumptions", false);
171  else
172  options.set_option("assumptions", true);
173 
174  // magic error label
175  if(cmdline.isset("error-label"))
176  options.set_option("error-label", cmdline.get_values("error-label"));
177 
178  options.set_option("show-properties", cmdline.isset("show-properties"));
179 }
180 
183 {
184  if(cmdline.isset("version"))
185  {
186  std::cout << CBMC_VERSION << '\n';
187  return CPROVER_EXIT_SUCCESS;
188  }
189 
190  //
191  // command line options
192  //
193 
194  optionst options;
195  get_command_line_options(options);
198 
199  //
200  // Print a banner
201  //
202  status() << "JDIFF version " CBMC_VERSION " " << sizeof(void *) * 8 << "-bit "
203  << config.this_architecture() << " "
205 
206  if(cmdline.args.size() != 2)
207  {
208  error() << "Please provide two programs to compare" << eom;
210  }
211 
212  goto_modelt goto_model1, goto_model2;
213 
214  int get_goto_program_ret = get_goto_program(options, *this, goto_model1);
215  if(get_goto_program_ret != -1)
216  return get_goto_program_ret;
217  get_goto_program_ret = get_goto_program(options, languages2, goto_model2);
218  if(get_goto_program_ret != -1)
219  return get_goto_program_ret;
220 
221  if(cmdline.isset("show-loops"))
222  {
223  show_loop_ids(get_ui(), goto_model1);
224  show_loop_ids(get_ui(), goto_model2);
225  return CPROVER_EXIT_SUCCESS;
226  }
227 
228  if(
229  cmdline.isset("show-goto-functions") ||
230  cmdline.isset("list-goto-functions"))
231  {
233  goto_model1,
236  cmdline.isset("list-goto-functions"));
238  goto_model2,
241  cmdline.isset("list-goto-functions"));
242  return CPROVER_EXIT_SUCCESS;
243  }
244 
245  if(
246  cmdline.isset("change-impact") || cmdline.isset("forward-impact") ||
247  cmdline.isset("backward-impact"))
248  {
249  impact_modet impact_mode =
250  cmdline.isset("forward-impact")
252  : (cmdline.isset("backward-impact") ? impact_modet::BACKWARD
255  goto_model1, goto_model2, impact_mode, cmdline.isset("compact-output"));
256 
257  return CPROVER_EXIT_SUCCESS;
258  }
259 
260  if(cmdline.isset("unified") || cmdline.isset('u'))
261  {
262  unified_difft u(goto_model1, goto_model2);
263  u();
264  u.output(std::cout);
265 
266  return CPROVER_EXIT_SUCCESS;
267  }
268 
270  goto_model1, goto_model2, options, get_message_handler());
271  sd.set_ui(get_ui());
272  sd();
273  sd.output_functions();
274 
275  return CPROVER_EXIT_SUCCESS;
276 }
277 
279  const optionst &options,
281  goto_modelt &goto_model)
282 {
283  status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
284 
285  if(is_goto_binary(cmdline.args[0]))
286  {
287  if(read_goto_binary(
288  cmdline.args[0],
289  goto_model.symbol_table,
290  goto_model.goto_functions,
291  languages.get_message_handler()))
293 
294  config.set(cmdline);
295 
296  // This one is done.
297  cmdline.args.erase(cmdline.args.begin());
298  }
299  else
300  {
301  // This is a a workaround to make parse() think that there is only
302  // one source file.
303  std::string arg2("");
304  if(cmdline.args.size() == 2)
305  {
306  arg2 = cmdline.args[1];
307  cmdline.args.erase(--cmdline.args.end());
308  }
309 
310  if(languages.parse() || languages.typecheck() || languages.final())
312 
313  // we no longer need any parse trees or language files
314  languages.clear_parse();
315 
316  status() << "Generating GOTO Program" << eom;
317 
318  goto_model.symbol_table = languages.symbol_table;
319  goto_convert(
320  goto_model.symbol_table, goto_model.goto_functions, ui_message_handler);
321 
322  if(process_goto_program(options, goto_model))
324 
325  // if we had a second argument then we will handle it next
326  if(arg2 != "")
327  cmdline.args[0] = arg2;
328  }
329 
330  return -1; // no error, continue
331 }
332 
334  const optionst &options,
335  goto_modelt &goto_model)
336 {
337  try
338  {
339  // remove function pointers
340  status() << "Removal of function pointers and virtual functions" << eom;
342  get_message_handler(), goto_model, cmdline.isset("pointer-check"));
343 
344  // Java virtual functions -> explicit dispatch tables:
345  remove_virtual_functions(goto_model);
346  // remove catch and throw
347  remove_exceptions(goto_model);
348  // Java instanceof -> clsid comparison:
349  remove_instanceof(goto_model);
350 
351  mm_io(goto_model);
352 
353  // instrument library preconditions
354  instrument_preconditions(goto_model);
355 
356  // remove returns, gcc vectors, complex
357  remove_returns(goto_model);
358  remove_vector(goto_model);
359  remove_complex(goto_model);
360  rewrite_union(goto_model);
361 
362  // add generic checks
363  status() << "Generic Property Instrumentation" << eom;
364  goto_check(options, goto_model);
365 
366  // checks don't know about adjusted float expressions
367  adjust_float_expressions(goto_model);
368 
369  // recalculate numbers, etc.
370  goto_model.goto_functions.update();
371 
372  // add loop ids
374 
375  // remove skips such that trivial GOTOs are deleted and not considered
376  // for coverage annotation:
377  remove_skip(goto_model);
378 
379  // instrument cover goals
380  if(cmdline.isset("cover"))
381  {
382  if(instrument_cover_goals(options, goto_model, get_message_handler()))
383  return true;
384  }
385 
386  // label the assertions
387  // This must be done after adding assertions and
388  // before using the argument of the "property" option.
389  // Do not re-label after using the property slicer because
390  // this would cause the property identifiers to change.
391  label_properties(goto_model);
392 
393  // remove any skips introduced since coverage instrumentation
394  remove_skip(goto_model);
395  goto_model.goto_functions.update();
396  }
397 
398  catch(const char *e)
399  {
400  error() << e << eom;
401  return true;
402  }
403 
404  catch(const std::string &e)
405  {
406  error() << e << eom;
407  return true;
408  }
409 
410  catch(int e)
411  {
412  error() << "Numeric exception: " << e << eom;
413  return true;
414  }
415 
416  catch(const std::bad_alloc &)
417  {
418  error() << "Out of memory" << eom;
420  return true;
421  }
422 
423  return false;
424 }
425 
428 {
429  // clang-format off
430  std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n'
431  <<
432  "* * Copyright (C) 2016-2018 * *\n"
433  "* * Daniel Kroening, Peter Schrammel * *\n"
434  "* * kroening@kroening.com * *\n"
435  "\n"
436  "Usage: Purpose:\n"
437  "\n"
438  " jdiff [-?] [-h] [--help] show help\n"
439  " jdiff old new jars to be compared\n"
440  "\n"
441  "Diff options:\n"
444  " --syntactic do syntactic diff (default)\n"
445  " -u | --unified output unified diff\n"
446  " --change-impact | \n"
447  " --forward-impact |\n"
448  // NOLINTNEXTLINE(whitespace/line_length)
449  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
450  " --compact-output output dependencies in compact mode\n"
451  "\n"
452  "Program instrumentation options:\n"
454  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
455  "Java Bytecode frontend options:\n"
457  "Other options:\n"
458  " --version show version and exit\n"
459  " --json-ui use JSON-formatted output\n"
461  "\n";
462  // clang-format on
463 }
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
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.
#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:737
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
Perform Memory-mapped I/O instrumentation.
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
#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
String Abstraction.
#define HELP_SHOW_PROPERTIES
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, remove_exceptions_typest type)
removes throws/CATCH-POP/CATCH-PUSH
virtual bool process_goto_program(const optionst &options, goto_modelt &goto_model)
virtual void output_functions() const
Output diff result.
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.
void adjust_float_expressions(exprt &expr, const namespacet &ns)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
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
virtual int get_goto_program(const optionst &options, jdiff_languagest &languages, goto_modelt &goto_model)
static irep_idt this_operating_system()
Definition: config.cpp:1309
#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
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:1212
virtual void help()
display command line help
GOTO-DIFF Base Class.