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>
33 
34 #include <goto-instrument/cover.h>
35 
39 
40 #include "java_syntactic_diff.h"
42 #include <goto-diff/unified_diff.h>
43 
44 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
47  argc,
48  argv,
49  std::string("JDIFF ") + CBMC_VERSION)
50 {
51 }
52 
54 {
55  if(config.set(cmdline))
56  {
57  usage_error();
58  exit(1);
59  }
60 
61  // TODO: improve this when language front ends have been
62  // disentangled from command line parsing
63  // we always require these options
64  cmdline.set("no-lazy-methods");
65  cmdline.set("no-refine-strings");
67 
68  if(cmdline.isset("cover"))
69  parse_cover_options(cmdline, options);
70 
71  // all checks supported by goto_check
73 
74  options.set_option("show-properties", cmdline.isset("show-properties"));
75 }
76 
79 {
80  if(cmdline.isset("version"))
81  {
82  std::cout << CBMC_VERSION << '\n';
83  return CPROVER_EXIT_SUCCESS;
84  }
85 
86  //
87  // command line options
88  //
89 
90  optionst options;
91  get_command_line_options(options);
94 
96 
97  if(cmdline.args.size() != 2)
98  {
99  log.error() << "Please provide two programs to compare" << messaget::eom;
101  }
102 
104 
105  goto_modelt goto_model1 =
107  if(process_goto_program(options, goto_model1))
109  goto_modelt goto_model2 =
111  if(process_goto_program(options, goto_model2))
113 
114  if(cmdline.isset("show-loops"))
115  {
116  show_loop_ids(ui_message_handler.get_ui(), goto_model1);
117  show_loop_ids(ui_message_handler.get_ui(), goto_model2);
118  return CPROVER_EXIT_SUCCESS;
119  }
120 
121  if(
122  cmdline.isset("show-goto-functions") ||
123  cmdline.isset("list-goto-functions"))
124  {
126  goto_model1, ui_message_handler, cmdline.isset("list-goto-functions"));
128  goto_model2, ui_message_handler, cmdline.isset("list-goto-functions"));
129  return CPROVER_EXIT_SUCCESS;
130  }
131 
132  if(
133  cmdline.isset("change-impact") || cmdline.isset("forward-impact") ||
134  cmdline.isset("backward-impact"))
135  {
136  impact_modet impact_mode =
137  cmdline.isset("forward-impact")
139  : (cmdline.isset("backward-impact") ? impact_modet::BACKWARD
142  goto_model1, goto_model2, impact_mode, cmdline.isset("compact-output"));
143 
144  return CPROVER_EXIT_SUCCESS;
145  }
146 
147  if(cmdline.isset("unified") || cmdline.isset('u'))
148  {
149  unified_difft u(goto_model1, goto_model2);
150  u();
151  u.output(std::cout);
152 
153  return CPROVER_EXIT_SUCCESS;
154  }
155 
157  goto_model1, goto_model2, options, ui_message_handler);
158  sd();
159  sd.output_functions();
160 
161  return CPROVER_EXIT_SUCCESS;
162 }
163 
165  const optionst &options,
166  goto_modelt &goto_model)
167 {
168  // remove function pointers
169  log.status() << "Removing function pointers and virtual functions"
170  << messaget::eom;
172  ui_message_handler, goto_model, cmdline.isset("pointer-check"));
173 
174  // Java virtual functions -> explicit dispatch tables:
175  remove_virtual_functions(goto_model);
176 
177  // remove Java throw and catch
178  // This introduces instanceof, so order is important:
180 
181  // Java instanceof -> clsid comparison:
182  class_hierarchyt class_hierarchy(goto_model.symbol_table);
183  remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
184 
185  mm_io(goto_model);
186 
187  // instrument library preconditions
188  instrument_preconditions(goto_model);
189 
190  // remove returns
191  remove_returns(goto_model);
192 
193  // add generic checks
194  log.status() << "Generic Property Instrumentation" << messaget::eom;
195  goto_check_java(options, goto_model, ui_message_handler);
196 
197  // checks don't know about adjusted float expressions
198  adjust_float_expressions(goto_model);
199 
200  // recalculate numbers, etc.
201  goto_model.goto_functions.update();
202 
203  // instrument cover goals
204  if(cmdline.isset("cover"))
205  {
206  // remove skips such that trivial GOTOs are deleted and not considered for
207  // coverage annotation:
208  remove_skip(goto_model);
209 
210  const auto cover_config =
211  get_cover_config(options, goto_model.symbol_table, ui_message_handler);
212  if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
213  return true;
214  }
215 
216  // label the assertions
217  // This must be done after adding assertions and
218  // before using the argument of the "property" option.
219  // Do not re-label after using the property slicer because
220  // this would cause the property identifiers to change.
221  label_properties(goto_model);
222 
223  // remove any skips introduced since coverage instrumentation
224  remove_skip(goto_model);
225 
226  return false;
227 }
228 
231 {
232  // clang-format off
233  std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n'
234  << align_center_with_border("Copyright (C) 2016-2018") << '\n'
235  << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT(*)
236  << align_center_with_border("kroening@kroening.com") << '\n'
237  <<
238  "\n"
239  "Usage: Purpose:\n"
240  "\n"
241  " jdiff [-?] [-h] [--help] show help\n"
242  " jdiff old new jars to be compared\n"
243  "\n"
244  "Diff options:\n"
247  " --show-loops show the loops in the programs\n"
248  " -u | --unified output unified diff\n"
249  " --change-impact | \n"
250  " --forward-impact |\n"
251  // NOLINTNEXTLINE(whitespace/line_length)
252  " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
253  " --compact-output output dependencies in compact mode\n"
254  "\n"
255  "Program instrumentation options:\n"
257  HELP_COVER
258  "Java Bytecode frontend options:\n"
260  "Other options:\n"
261  " --version show version and exit\n"
262  " --json-ui use JSON-formatted output\n"
264  "\n";
265  // clang-format on
266 }
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:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
argst args
Definition: cmdline.h:145
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:58
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
virtual void output_functions() const
Output diff result.
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:186
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:148
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_java(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
#define PARSE_OPTIONS_GOTO_CHECK_JAVA(cmdline, options)
#define HELP_GOTO_CHECK_JAVA
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_r_value, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Definition: mm_io.cpp:37
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)
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:88
Program Transformation.
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 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