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>
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 // TODO: do not use language_uit for this; requires a refactoring of
64 // initialize_goto_model to support parsing specific command line files
65 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
66  : parse_options_baset(JDIFF_OPTIONS, argc, argv),
67  jdiff_languagest(cmdline, ui_message_handler, &options),
68  ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION),
69  languages2(cmdline, ui_message_handler, &options)
70 {
71 }
72 
74  int argc,
75  const char **argv,
76  const std::string &extra_options)
77  : parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv),
78  jdiff_languagest(cmdline, ui_message_handler, &options),
79  ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION),
80  languages2(cmdline, ui_message_handler, &options)
81 {
82 }
83 
85 {
86  if(config.set(cmdline))
87  {
88  usage_error();
89  exit(1);
90  }
91 
92  // TODO: improve this when language front ends have been
93  // disentangled from command line parsing
94  // we always require these options
95  cmdline.set("no-lazy-methods");
96  cmdline.set("no-refine-strings");
98 
99  if(cmdline.isset("cover"))
101 
102  if(cmdline.isset("mm"))
103  options.set_option("mm", cmdline.get_value("mm"));
104 
105  // all checks supported by goto_check
107 
108  if(cmdline.isset("debug-level"))
109  options.set_option("debug-level", cmdline.get_value("debug-level"));
110 
111  if(cmdline.isset("slice-by-trace"))
112  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
113 
114  if(cmdline.isset("unwindset"))
115  options.set_option("unwindset", cmdline.get_value("unwindset"));
116 
117  // constant propagation
118  if(cmdline.isset("no-propagation"))
119  options.set_option("propagation", false);
120  else
121  options.set_option("propagation", true);
122 
123  // check array bounds
124  if(cmdline.isset("bounds-check"))
125  options.set_option("bounds-check", true);
126  else
127  options.set_option("bounds-check", false);
128 
129  // check division by zero
130  if(cmdline.isset("div-by-zero-check"))
131  options.set_option("div-by-zero-check", true);
132  else
133  options.set_option("div-by-zero-check", false);
134 
135  // check overflow/underflow
136  if(cmdline.isset("signed-overflow-check"))
137  options.set_option("signed-overflow-check", true);
138  else
139  options.set_option("signed-overflow-check", false);
140 
141  // check overflow/underflow
142  if(cmdline.isset("unsigned-overflow-check"))
143  options.set_option("unsigned-overflow-check", true);
144  else
145  options.set_option("unsigned-overflow-check", false);
146 
147  // check overflow/underflow
148  if(cmdline.isset("float-overflow-check"))
149  options.set_option("float-overflow-check", true);
150  else
151  options.set_option("float-overflow-check", false);
152 
153  // check for NaN (not a number)
154  if(cmdline.isset("nan-check"))
155  options.set_option("nan-check", true);
156  else
157  options.set_option("nan-check", false);
158 
159  // check pointers
160  if(cmdline.isset("pointer-check"))
161  options.set_option("pointer-check", true);
162  else
163  options.set_option("pointer-check", false);
164 
165  // check for memory leaks
166  if(cmdline.isset("memory-leak-check"))
167  options.set_option("memory-leak-check", true);
168  else
169  options.set_option("memory-leak-check", false);
170 
171  // check assertions
172  if(cmdline.isset("no-assertions"))
173  options.set_option("assertions", false);
174  else
175  options.set_option("assertions", true);
176 
177  // use assumptions
178  if(cmdline.isset("no-assumptions"))
179  options.set_option("assumptions", false);
180  else
181  options.set_option("assumptions", true);
182 
183  // magic error label
184  if(cmdline.isset("error-label"))
185  options.set_option("error-label", cmdline.get_values("error-label"));
186 
187  options.set_option("show-properties", cmdline.isset("show-properties"));
188 }
189 
192 {
193  if(cmdline.isset("version"))
194  {
195  std::cout << CBMC_VERSION << '\n';
196  return CPROVER_EXIT_SUCCESS;
197  }
198 
199  //
200  // command line options
201  //
202 
207 
208  //
209  // Print a banner
210  //
211  status() << "JDIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8
212  << "-bit " << config.this_architecture() << " "
214 
215  if(cmdline.args.size() != 2)
216  {
217  error() << "Please provide two programs to compare" << eom;
219  }
220 
221  goto_modelt goto_model1, goto_model2;
222 
223  int get_goto_program_ret = get_goto_program(options, *this, goto_model1);
224  if(get_goto_program_ret != -1)
225  return get_goto_program_ret;
226  get_goto_program_ret = get_goto_program(options, languages2, goto_model2);
227  if(get_goto_program_ret != -1)
228  return get_goto_program_ret;
229 
230  if(cmdline.isset("show-loops"))
231  {
232  show_loop_ids(get_ui(), goto_model1);
233  show_loop_ids(get_ui(), goto_model2);
234  return CPROVER_EXIT_SUCCESS;
235  }
236 
237  if(
238  cmdline.isset("show-goto-functions") ||
239  cmdline.isset("list-goto-functions"))
240  {
242  goto_model1,
245  cmdline.isset("list-goto-functions"));
247  goto_model2,
250  cmdline.isset("list-goto-functions"));
251  return CPROVER_EXIT_SUCCESS;
252  }
253 
254  if(
255  cmdline.isset("change-impact") || cmdline.isset("forward-impact") ||
256  cmdline.isset("backward-impact"))
257  {
258  impact_modet impact_mode =
259  cmdline.isset("forward-impact")
261  : (cmdline.isset("backward-impact") ? impact_modet::BACKWARD
264  goto_model1, goto_model2, impact_mode, cmdline.isset("compact-output"));
265 
266  return CPROVER_EXIT_SUCCESS;
267  }
268 
269  if(cmdline.isset("unified") || cmdline.isset('u'))
270  {
271  unified_difft u(goto_model1, goto_model2);
272  u();
273  u.output(std::cout);
274 
275  return CPROVER_EXIT_SUCCESS;
276  }
277 
279  goto_model1, goto_model2, options, ui_message_handler);
280  sd();
281  sd.output_functions();
282 
283  return CPROVER_EXIT_SUCCESS;
284 }
285 
287  const optionst &options,
289  goto_modelt &goto_model)
290 {
291  status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
292 
293  if(is_goto_binary(cmdline.args[0]))
294  {
295  if(read_goto_binary(
296  cmdline.args[0],
297  goto_model.symbol_table,
298  goto_model.goto_functions,
299  languages.get_message_handler()))
301 
302  config.set(cmdline);
303 
304  // This one is done.
305  cmdline.args.erase(cmdline.args.begin());
306  }
307  else
308  {
309  // This is a a workaround to make parse() think that there is only
310  // one source file.
311  std::string arg2("");
312  if(cmdline.args.size() == 2)
313  {
314  arg2 = cmdline.args[1];
315  cmdline.args.erase(--cmdline.args.end());
316  }
317 
318  if(languages.parse() || languages.typecheck() || languages.final())
320 
321  // we no longer need any parse trees or language files
322  languages.clear_parse();
323 
324  status() << "Generating GOTO Program" << eom;
325 
326  goto_model.symbol_table = languages.symbol_table;
327  goto_convert(
328  goto_model.symbol_table, goto_model.goto_functions, ui_message_handler);
329 
330  if(process_goto_program(options, goto_model))
332 
333  // if we had a second argument then we will handle it next
334  if(arg2 != "")
335  cmdline.args[0] = arg2;
336  }
337 
338  return -1; // no error, continue
339 }
340 
342  const optionst &options,
343  goto_modelt &goto_model)
344 {
345  try
346  {
347  // remove function pointers
348  status() << "Removing function pointers and virtual functions" << eom;
350  get_message_handler(), goto_model, cmdline.isset("pointer-check"));
351 
352  // Java virtual functions -> explicit dispatch tables:
353  remove_virtual_functions(goto_model);
354 
355  // remove Java throw and catch
356  // This introduces instanceof, so order is important:
358 
359  // Java instanceof -> clsid comparison:
360  class_hierarchyt class_hierarchy(goto_model.symbol_table);
361  remove_instanceof(goto_model, class_hierarchy, get_message_handler());
362 
363  mm_io(goto_model);
364 
365  // instrument library preconditions
366  instrument_preconditions(goto_model);
367 
368  // remove returns, gcc vectors, complex
369  remove_returns(goto_model);
370  remove_vector(goto_model);
371  remove_complex(goto_model);
372  rewrite_union(goto_model);
373 
374  // add generic checks
375  status() << "Generic Property Instrumentation" << eom;
376  goto_check(options, goto_model);
377 
378  // checks don't know about adjusted float expressions
379  adjust_float_expressions(goto_model);
380 
381  // recalculate numbers, etc.
382  goto_model.goto_functions.update();
383 
384  // add loop ids
386 
387  // remove skips such that trivial GOTOs are deleted and not considered
388  // for coverage annotation:
389  remove_skip(goto_model);
390 
391  // instrument cover goals
392  if(cmdline.isset("cover"))
393  {
395  return true;
396  }
397 
398  // label the assertions
399  // This must be done after adding assertions and
400  // before using the argument of the "property" option.
401  // Do not re-label after using the property slicer because
402  // this would cause the property identifiers to change.
403  label_properties(goto_model);
404 
405  // remove any skips introduced since coverage instrumentation
406  remove_skip(goto_model);
407  goto_model.goto_functions.update();
408  }
409 
410  catch(const char *e)
411  {
412  error() << e << eom;
413  return true;
414  }
415 
416  catch(const std::string &e)
417  {
418  error() << e << eom;
419  return true;
420  }
421 
422  catch(int e)
423  {
424  error() << "Numeric exception: " << e << eom;
425  return true;
426  }
427 
428  catch(const std::bad_alloc &)
429  {
430  error() << "Out of memory" << eom;
432  return true;
433  }
434 
435  return false;
436 }
437 
440 {
441  // clang-format off
442  std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n'
443  <<
444  "* * Copyright (C) 2016-2018 * *\n"
445  "* * Daniel Kroening, Peter Schrammel * *\n"
446  "* * kroening@kroening.com * *\n"
447  "\n"
448  "Usage: Purpose:\n"
449  "\n"
450  " jdiff [-?] [-h] [--help] show help\n"
451  " jdiff old new jars to be compared\n"
452  "\n"
453  "Diff options:\n"
456  " --syntactic do syntactic diff (default)\n"
457  " -u | --unified output unified diff\n"
458  " --change-impact | \n"
459  " --forward-impact |\n"
460  // NOLINTNEXTLINE(whitespace/line_length)
461  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
462  " --compact-output output dependencies in compact mode\n"
463  "\n"
464  "Program instrumentation options:\n"
466  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
467  "Java Bytecode frontend options:\n"
469  "Other options:\n"
470  " --version show version and exit\n"
471  " --json-ui use JSON-formatted output\n"
473  "\n";
474  // clang-format on
475 }
cmdlinet::args
argst args
Definition: cmdline.h:44
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
jdiff_parse_optionst::doit
virtual int doit()
invoke main modules
Definition: jdiff_parse_options.cpp:191
cover.h
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:26
impact_modet
impact_modet
Definition: change_impact.h:18
string_abstraction.h
JDIFF_OPTIONS
#define JDIFF_OPTIONS
Definition: jdiff_parse_options.h:31
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:58
rewrite_union.h
unified_difft::output
void output(std::ostream &os) const
Definition: unified_diff.cpp:367
jdiff_parse_optionst::get_command_line_options
virtual void get_command_line_options(optionst &options)
Definition: jdiff_parse_options.cpp:84
is_goto_binary
bool is_goto_binary(const std::string &filename)
Definition: read_goto_binary.cpp:168
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:42
parse_options_baset
Definition: parse_options.h:17
java_bytecode_language.h
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
Definition: java_bytecode_language.h:44
parse_java_language_options
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
Definition: java_bytecode_language.cpp:48
remove_exceptions_using_instanceof
void remove_exceptions_using_instanceof(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
Definition: remove_exceptions.cpp:594
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:27
jdiff_parse_optionst::languages2
jdiff_languagest languages2
Definition: jdiff_parse_options.h:60
impact_modet::BACKWARD
@ BACKWARD
goto_inline.h
optionst
Definition: options.h:22
CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:53
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:161
mm_io
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
read_goto_binary
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
Read a goto binary from a file, but do not update config.
Definition: read_goto_binary.cpp:36
messaget::status
mstreamt & status() const
Definition: message.h:401
cmdlinet::set
virtual void set(const std::string &option)
Definition: cmdline.cpp:60
instrument_preconditions.h
remove_virtual_functions
void remove_virtual_functions(const 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...
Definition: remove_virtual_functions.cpp:568
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:86
show_goto_functions
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:28
remove_virtual_functions.h
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:739
goto_modelt
Definition: goto_model.h:24
mode.h
show_loop_ids
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
options.h
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
messaget::eom
static eomt eom
Definition: message.h:284
impact_modet::BOTH
@ BOTH
version.h
string_instrumentation.h
unified_difft
Definition: unified_diff.h:30
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:43
goto_convert
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Definition: goto_convert.cpp:1931
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:36
remove_vector
static void remove_vector(typet &)
removes vector data type
Definition: remove_vector.cpp:167
unified_diff.h
remove_complex.h
set_properties.h
goto_difft::output_functions
virtual void output_functions() const
Output diff result.
Definition: goto_diff_base.cpp:21
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:386
goto_diff.h
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:87
mm_io.h
remove_function_pointers
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)
Definition: remove_function_pointers.cpp:520
instrument_preconditions
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Definition: instrument_preconditions.cpp:93
jdiff_parse_options.h
show_properties.h
jdiff_parse_optionst::help
virtual void help()
display command line help
Definition: jdiff_parse_options.cpp:439
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:45
java_syntactic_diff.h
rewrite_union
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Definition: rewrite_union.cpp:66
language.h
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:1368
goto_check
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
Definition: goto_check.cpp:1784
parse_cover_options
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:160
jdiff_parse_optionst::ui_message_handler
ui_message_handlert ui_message_handler
Definition: jdiff_parse_options.h:59
impact_modet::FORWARD
@ FORWARD
jdiff_parse_optionst::jdiff_parse_optionst
jdiff_parse_optionst(int argc, const char **argv)
Definition: jdiff_parse_options.cpp:65
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
read_goto_binary.h
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:50
remove_vector.h
remove_complex
static void remove_complex(typet &)
removes complex data type
Definition: remove_complex.cpp:240
remove_returns.h
remove_exceptions.h
remove_unused_functions.h
config
configt config
Definition: config.cpp:24
remove_instanceof.h
jdiff_languagest
Definition: jdiff_languages.h:18
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1268
ui_message_handlert::get_ui
uit get_ui() const
Definition: ui_message.h:30
remove_instanceof
void remove_instanceof(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...
Definition: remove_instanceof.cpp:243
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
instrument_cover_goals
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
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:43
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:767
exit_codes.h
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:261
jdiff_parse_optionst::options
optionst options
Definition: jdiff_parse_options.h:58
java_syntactic_difft
Definition: java_syntactic_diff.h:17
goto_functionst::update
void update()
Definition: goto_functions.h:91
jdiff_parse_optionst::process_goto_program
virtual bool process_goto_program(const optionst &options, goto_modelt &goto_model)
Definition: jdiff_parse_options.cpp:341
change_impact.h
config.h
loop_ids.h
adjust_float_expressions
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...
Definition: adjust_float_expressions.cpp:78
add_failed_symbols.h
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:46
goto_convert_functions.h
languages
languagest languages
Definition: mode.cpp:32
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:98
remove_skip.h
adjust_float_expressions.h
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
jdiff_parse_optionst::get_goto_program
virtual int get_goto_program(const optionst &options, jdiff_languagest &languages, goto_modelt &goto_model)
Definition: jdiff_parse_options.cpp:286
remove_function_pointers.h
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:23
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
language_uit::get_ui
uit get_ui()
Definition: language_ui.h:49
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14