cprover
Loading...
Searching...
No Matches
jdiff_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JDIFF Command Line Option Processing
4
5Author: 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
26#include <goto-programs/mm_io.h>
33
35
39
40#include "java_syntactic_diff.h"
43
47 argc,
48 argv,
49 std::string("JDIFF ") + CBMC_VERSION)
50{
51}
52
54{
55 if(config.set(cmdline))
56 {
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"))
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';
84 }
85
86 //
87 // command line options
88 //
89
90 optionst 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 {
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"));
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
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
154 }
155
157 goto_model1, goto_model2, options, ui_message_handler);
158 sd();
159 sd.output_functions();
160
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 =
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"
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
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
@ M_STATISTICS
Definition message.h:171
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
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
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.
STL namespace.
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
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