Add JDIFF tool
This commit is contained in:
Peter Schrammel
parent
a20f2c1427
commit
45887539d1
|
|
@ -64,15 +64,11 @@ set_target_properties(
|
|||
goto-instrument-lib
|
||||
goto-programs
|
||||
goto-symex
|
||||
java_bytecode
|
||||
jbmc
|
||||
jbmc-lib
|
||||
jsil
|
||||
json
|
||||
langapi
|
||||
linking
|
||||
miniBDD
|
||||
miniz
|
||||
mmcc
|
||||
pointer-analysis
|
||||
solvers
|
||||
|
|
@ -85,6 +81,8 @@ set_target_properties(
|
|||
java_bytecode
|
||||
jbmc
|
||||
jbmc-lib
|
||||
jdiff
|
||||
jdiff-lib
|
||||
java-testing-utils
|
||||
java-unit
|
||||
miniz
|
||||
|
|
|
|||
|
|
@ -16,3 +16,4 @@ endmacro(generic_includes)
|
|||
add_subdirectory(miniz)
|
||||
add_subdirectory(java_bytecode)
|
||||
add_subdirectory(jbmc)
|
||||
add_subdirectory(jdiff)
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
DIRS = jbmc java_bytecode miniz
|
||||
DIRS = jbmc jdiff java_bytecode miniz
|
||||
|
||||
include config.inc
|
||||
|
||||
.PHONY: all
|
||||
all: jbmc.dir
|
||||
all: jbmc.dir jdiff.dir
|
||||
|
||||
# building cbmc proper
|
||||
.PHONY: cprover.dir
|
||||
|
|
@ -16,6 +16,9 @@ java_bytecode.dir: miniz.dir
|
|||
.PHONY: jbmc.dir
|
||||
jbmc.dir: java_bytecode.dir cprover.dir
|
||||
|
||||
.PHONY: jdiff.dir
|
||||
jdiff.dir: java_bytecode.dir cprover.dir
|
||||
|
||||
.PHONY: miniz.dir
|
||||
miniz.dir:
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,28 @@
|
|||
# Library
|
||||
file(GLOB_RECURSE sources "*.cpp" "*.h")
|
||||
list(REMOVE_ITEM sources
|
||||
${CMAKE_CURRENT_SOURCE_DIR}/jdiff_main.cpp
|
||||
)
|
||||
add_library(jdiff-lib ${sources})
|
||||
|
||||
generic_includes(jdiff-lib)
|
||||
|
||||
target_link_libraries(jdiff-lib
|
||||
ansi-c
|
||||
linking
|
||||
big-int
|
||||
pointer-analysis
|
||||
goto-diff-lib
|
||||
goto-instrument-lib
|
||||
goto-programs
|
||||
goto-symex
|
||||
analyses
|
||||
java_bytecode
|
||||
langapi
|
||||
xml
|
||||
util
|
||||
)
|
||||
|
||||
# Executable
|
||||
add_executable(jdiff jdiff_main.cpp)
|
||||
target_link_libraries(jdiff jdiff-lib)
|
||||
|
|
@ -0,0 +1,56 @@
|
|||
SRC = jdiff_languages.cpp \
|
||||
jdiff_main.cpp \
|
||||
jdiff_parse_options.cpp \
|
||||
java_syntactic_diff.cpp \
|
||||
# Empty last line
|
||||
|
||||
OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
|
||||
..//java_bytecode/java_bytecode$(LIBEXT) \
|
||||
../$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
|
||||
../$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
|
||||
../$(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-diff/syntactic_diff$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-diff/unified_diff$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-diff/change_impact$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-diff/goto_diff_base$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_branch$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_condition$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_decision$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_location$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_other$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-instrument/cover_util$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/goto-symex/rewrite_union$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
|
||||
../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
|
||||
../$(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \
|
||||
../$(CPROVER_DIR)/src/util/util$(LIBEXT) \
|
||||
../miniz/miniz$(OBJEXT) \
|
||||
../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
|
||||
# Empty last line
|
||||
|
||||
INCLUDES= -I .. -I ../$(CPROVER_DIR)/src
|
||||
|
||||
LIBS =
|
||||
|
||||
include ../config.inc
|
||||
include ../$(CPROVER_DIR)/src/config.inc
|
||||
include ../$(CPROVER_DIR)/src/common
|
||||
|
||||
CLEANFILES = jdiff$(EXEEXT)
|
||||
|
||||
all: jdiff$(EXEEXT)
|
||||
|
||||
###############################################################################
|
||||
|
||||
jdiff$(EXEEXT): $(OBJ)
|
||||
$(LINKBIN)
|
||||
|
||||
.PHONY: jdiff-mac-signed
|
||||
|
||||
jdiff-mac-signed: jdiff$(EXEEXT)
|
||||
strip jdiff$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) jdiff$(EXEEXT)
|
||||
|
|
@ -0,0 +1,7 @@
|
|||
\ingroup module_hidden
|
||||
\defgroup jdiff jdiff
|
||||
|
||||
# Folder jdiff
|
||||
|
||||
`jdiff/` is a tool that offers functionality similar to the `diff`
|
||||
tool, but for Java programs.
|
||||
|
|
@ -0,0 +1,129 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Syntactic GOTO-DIFF for Java
|
||||
|
||||
Author: Peter Schrammel
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
/// \file
|
||||
/// Syntactic GOTO-DIFF for Java
|
||||
|
||||
#include "java_syntactic_diff.h"
|
||||
|
||||
#include <goto-programs/goto_model.h>
|
||||
|
||||
bool java_syntactic_difft::operator()()
|
||||
{
|
||||
forall_goto_functions(it, goto_model1.goto_functions)
|
||||
{
|
||||
if(!it->second.body_available())
|
||||
continue;
|
||||
|
||||
goto_functionst::function_mapt::const_iterator f_it =
|
||||
goto_model2.goto_functions.function_map.find(it->first);
|
||||
if(
|
||||
f_it == goto_model2.goto_functions.function_map.end() ||
|
||||
!f_it->second.body_available())
|
||||
{
|
||||
deleted_functions.insert(it->first);
|
||||
continue;
|
||||
}
|
||||
|
||||
// check access qualifiers
|
||||
const symbolt *fun1 = goto_model1.symbol_table.lookup(it->first);
|
||||
CHECK_RETURN(fun1 != nullptr);
|
||||
const symbolt *fun2 = goto_model2.symbol_table.lookup(it->first);
|
||||
CHECK_RETURN(fun2 != nullptr);
|
||||
const irep_idt &class_name = fun1->type.get(ID_C_class);
|
||||
bool function_access_changed =
|
||||
fun1->type.get(ID_access) != fun2->type.get(ID_access);
|
||||
bool class_access_changed = false;
|
||||
bool field_access_changed = false;
|
||||
if(!class_name.empty())
|
||||
{
|
||||
const symbolt *class1 = goto_model1.symbol_table.lookup(class_name);
|
||||
CHECK_RETURN(class1 != nullptr);
|
||||
const symbolt *class2 = goto_model2.symbol_table.lookup(class_name);
|
||||
CHECK_RETURN(class2 != nullptr);
|
||||
class_access_changed =
|
||||
class1->type.get(ID_access) != class2->type.get(ID_access);
|
||||
const class_typet &class_type1 = to_class_type(class1->type);
|
||||
const class_typet &class_type2 = to_class_type(class2->type);
|
||||
for(const auto &field1 : class_type1.components())
|
||||
{
|
||||
for(const auto &field2 : class_type2.components())
|
||||
{
|
||||
if(field1.get_name() == field2.get_name())
|
||||
{
|
||||
field_access_changed = field1.get_access() != field2.get_access();
|
||||
break;
|
||||
}
|
||||
}
|
||||
if(field_access_changed)
|
||||
break;
|
||||
}
|
||||
}
|
||||
if(function_access_changed || class_access_changed || field_access_changed)
|
||||
{
|
||||
modified_functions.insert(it->first);
|
||||
continue;
|
||||
}
|
||||
|
||||
if(
|
||||
it->second.body.instructions.size() !=
|
||||
f_it->second.body.instructions.size())
|
||||
{
|
||||
modified_functions.insert(it->first);
|
||||
continue;
|
||||
}
|
||||
|
||||
goto_programt::instructionst::const_iterator i_it1 =
|
||||
it->second.body.instructions.begin();
|
||||
for(goto_programt::instructionst::const_iterator
|
||||
i_it2 = f_it->second.body.instructions.begin();
|
||||
i_it1 != it->second.body.instructions.end() &&
|
||||
i_it2 != f_it->second.body.instructions.end();
|
||||
++i_it1, ++i_it2)
|
||||
{
|
||||
long jump_difference1 = 0;
|
||||
if(!i_it1->targets.empty())
|
||||
{
|
||||
jump_difference1 =
|
||||
i_it1->get_target()->location_number - i_it1->location_number;
|
||||
}
|
||||
long jump_difference2 = 0;
|
||||
if(!i_it2->targets.empty())
|
||||
{
|
||||
jump_difference2 =
|
||||
i_it2->get_target()->location_number - i_it2->location_number;
|
||||
}
|
||||
if(
|
||||
i_it1->code != i_it2->code || i_it1->function != i_it2->function ||
|
||||
i_it1->type != i_it2->type || i_it1->guard != i_it2->guard ||
|
||||
jump_difference1 != jump_difference2)
|
||||
{
|
||||
modified_functions.insert(it->first);
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
forall_goto_functions(it, goto_model2.goto_functions)
|
||||
{
|
||||
if(!it->second.body_available())
|
||||
continue;
|
||||
|
||||
total_functions_count++;
|
||||
|
||||
goto_functionst::function_mapt::const_iterator f_it =
|
||||
goto_model1.goto_functions.function_map.find(it->first);
|
||||
if(
|
||||
f_it == goto_model1.goto_functions.function_map.end() ||
|
||||
!f_it->second.body_available())
|
||||
new_functions.insert(it->first);
|
||||
}
|
||||
|
||||
return !(
|
||||
new_functions.empty() && modified_functions.empty() &&
|
||||
deleted_functions.empty());
|
||||
}
|
||||
|
|
@ -0,0 +1,32 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Syntactic GOTO-DIFF for Java
|
||||
|
||||
Author: Peter Schrammel
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
/// \file
|
||||
/// Syntactic GOTO-DIFF for Java
|
||||
|
||||
#ifndef CPROVER_JDIFF_JAVA_SYNTACTIC_DIFF_H
|
||||
#define CPROVER_JDIFF_JAVA_SYNTACTIC_DIFF_H
|
||||
|
||||
#include <goto-diff/goto_diff.h>
|
||||
|
||||
class java_syntactic_difft : public goto_difft
|
||||
{
|
||||
public:
|
||||
java_syntactic_difft(
|
||||
const goto_modelt &_goto_model1,
|
||||
const goto_modelt &_goto_model2,
|
||||
const optionst &_options,
|
||||
message_handlert &_message_handler)
|
||||
: goto_difft(_goto_model1, _goto_model2, _options, _message_handler)
|
||||
{
|
||||
}
|
||||
|
||||
virtual bool operator()();
|
||||
};
|
||||
|
||||
#endif // CPROVER_JDIFF_JAVA_SYNTACTIC_DIFF_H
|
||||
|
|
@ -0,0 +1,21 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Language Registration
|
||||
|
||||
Author: Peter Schrammel
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
/// \file
|
||||
/// Language Registration
|
||||
|
||||
#include "jdiff_languages.h"
|
||||
|
||||
#include <langapi/mode.h>
|
||||
|
||||
#include <java_bytecode/java_bytecode_language.h>
|
||||
|
||||
void jdiff_languagest::register_languages()
|
||||
{
|
||||
register_language(new_java_bytecode_language);
|
||||
}
|
||||
|
|
@ -0,0 +1,33 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: JDIFF Languages
|
||||
|
||||
Author: Peter Schrammel
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
/// \file
|
||||
/// JDIFF Languages
|
||||
|
||||
#ifndef CPROVER_JDIFF_JDIFF_LANGUAGES_H
|
||||
#define CPROVER_JDIFF_JDIFF_LANGUAGES_H
|
||||
|
||||
#include <goto-programs/goto_model.h>
|
||||
#include <langapi/language_ui.h>
|
||||
|
||||
class jdiff_languagest : public language_uit
|
||||
{
|
||||
public:
|
||||
explicit jdiff_languagest(
|
||||
const cmdlinet &cmdline,
|
||||
ui_message_handlert &ui_message_handler)
|
||||
: language_uit(cmdline, ui_message_handler)
|
||||
{
|
||||
register_languages();
|
||||
}
|
||||
|
||||
protected:
|
||||
virtual void register_languages();
|
||||
};
|
||||
|
||||
#endif // CPROVER_JDIFF_JDIFF_LANGUAGES_H
|
||||
|
|
@ -0,0 +1,47 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: JDIFF Main Module
|
||||
|
||||
Author: Peter Schrammel
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
/// \file
|
||||
/// JDIFF Main Module
|
||||
|
||||
#include "jdiff_parse_options.h"
|
||||
|
||||
#include <util/unicode.h>
|
||||
|
||||
#ifdef IREP_HASH_STATS
|
||||
#include <iostream>
|
||||
#endif
|
||||
|
||||
#ifdef IREP_HASH_STATS
|
||||
extern unsigned long long irep_hash_cnt;
|
||||
extern unsigned long long irep_cmp_cnt;
|
||||
extern unsigned long long irep_cmp_ne_cnt;
|
||||
#endif
|
||||
|
||||
#ifdef _MSC_VER
|
||||
int wmain(int argc, const wchar_t **argv_wide)
|
||||
{
|
||||
auto vec = narrow_argv(argc, argv_wide);
|
||||
auto narrow = to_c_str_array(std::begin(vec), std::end(vec));
|
||||
auto argv = narrow.data();
|
||||
#else
|
||||
int main(int argc, const char **argv)
|
||||
{
|
||||
#endif
|
||||
jdiff_parse_optionst parse_options(argc, argv);
|
||||
|
||||
int res = parse_options.main();
|
||||
|
||||
#ifdef IREP_HASH_STATS
|
||||
std::cout << "IREP_HASH_CNT=" << irep_hash_cnt << '\n';
|
||||
std::cout << "IREP_CMP_CNT=" << irep_cmp_cnt << '\n';
|
||||
std::cout << "IREP_CMP_NE_CNT=" << irep_cmp_ne_cnt << '\n';
|
||||
#endif
|
||||
|
||||
return res;
|
||||
}
|
||||
|
|
@ -0,0 +1,484 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: JDIFF Command Line Option Processing
|
||||
|
||||
Author: Peter Schrammel
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
/// \file
|
||||
/// JDIFF Command Line Option Processing
|
||||
|
||||
#include "jdiff_parse_options.h"
|
||||
|
||||
#include <cstdlib> // exit()
|
||||
#include <fstream>
|
||||
#include <iostream>
|
||||
#include <memory>
|
||||
|
||||
#include <util/config.h>
|
||||
#include <util/exit_codes.h>
|
||||
#include <util/make_unique.h>
|
||||
#include <util/options.h>
|
||||
#include <util/string2int.h>
|
||||
|
||||
#include <langapi/language.h>
|
||||
|
||||
#include <goto-programs/adjust_float_expressions.h>
|
||||
#include <goto-programs/goto_convert_functions.h>
|
||||
#include <goto-programs/goto_inline.h>
|
||||
#include <goto-programs/instrument_preconditions.h>
|
||||
#include <goto-programs/link_to_library.h>
|
||||
#include <goto-programs/loop_ids.h>
|
||||
#include <goto-programs/mm_io.h>
|
||||
#include <goto-programs/read_goto_binary.h>
|
||||
#include <goto-programs/remove_complex.h>
|
||||
#include <goto-programs/remove_function_pointers.h>
|
||||
#include <goto-programs/remove_returns.h>
|
||||
#include <goto-programs/remove_skip.h>
|
||||
#include <goto-programs/remove_unused_functions.h>
|
||||
#include <goto-programs/remove_vector.h>
|
||||
#include <goto-programs/remove_virtual_functions.h>
|
||||
#include <goto-programs/set_properties.h>
|
||||
#include <goto-programs/show_properties.h>
|
||||
#include <goto-programs/string_abstraction.h>
|
||||
#include <goto-programs/string_instrumentation.h>
|
||||
|
||||
#include <goto-symex/rewrite_union.h>
|
||||
|
||||
#include <goto-instrument/cover.h>
|
||||
|
||||
#include <pointer-analysis/add_failed_symbols.h>
|
||||
|
||||
#include <java_bytecode/java_bytecode_language.h>
|
||||
#include <java_bytecode/remove_exceptions.h>
|
||||
#include <java_bytecode/remove_instanceof.h>
|
||||
|
||||
#include <langapi/mode.h>
|
||||
|
||||
#include <cbmc/version.h>
|
||||
|
||||
#include "java_syntactic_diff.h"
|
||||
#include <goto-diff/change_impact.h>
|
||||
#include <goto-diff/goto_diff.h>
|
||||
#include <goto-diff/unified_diff.h>
|
||||
|
||||
jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
|
||||
: parse_options_baset(JDIFF_OPTIONS, argc, argv),
|
||||
jdiff_languagest(cmdline, ui_message_handler),
|
||||
ui_message_handler(cmdline, "JDIFF " CBMC_VERSION),
|
||||
languages2(cmdline, ui_message_handler)
|
||||
{
|
||||
}
|
||||
|
||||
::jdiff_parse_optionst::jdiff_parse_optionst(
|
||||
int argc,
|
||||
const char **argv,
|
||||
const std::string &extra_options)
|
||||
: parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv),
|
||||
jdiff_languagest(cmdline, ui_message_handler),
|
||||
ui_message_handler(cmdline, "JDIFF " CBMC_VERSION),
|
||||
languages2(cmdline, ui_message_handler)
|
||||
{
|
||||
}
|
||||
|
||||
void jdiff_parse_optionst::eval_verbosity()
|
||||
{
|
||||
// this is our default verbosity
|
||||
unsigned int v = messaget::M_STATISTICS;
|
||||
|
||||
if(cmdline.isset("verbosity"))
|
||||
{
|
||||
v = unsafe_string2unsigned(cmdline.get_value("verbosity"));
|
||||
if(v > 10)
|
||||
v = 10;
|
||||
}
|
||||
|
||||
ui_message_handler.set_verbosity(v);
|
||||
}
|
||||
|
||||
void jdiff_parse_optionst::get_command_line_options(optionst &options)
|
||||
{
|
||||
if(config.set(cmdline))
|
||||
{
|
||||
usage_error();
|
||||
exit(1);
|
||||
}
|
||||
|
||||
if(cmdline.isset("cover"))
|
||||
parse_cover_options(cmdline, options);
|
||||
|
||||
if(cmdline.isset("mm"))
|
||||
options.set_option("mm", cmdline.get_value("mm"));
|
||||
|
||||
// all checks supported by goto_check
|
||||
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
|
||||
|
||||
if(cmdline.isset("debug-level"))
|
||||
options.set_option("debug-level", cmdline.get_value("debug-level"));
|
||||
|
||||
if(cmdline.isset("slice-by-trace"))
|
||||
options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
|
||||
|
||||
if(cmdline.isset("unwindset"))
|
||||
options.set_option("unwindset", cmdline.get_value("unwindset"));
|
||||
|
||||
// constant propagation
|
||||
if(cmdline.isset("no-propagation"))
|
||||
options.set_option("propagation", false);
|
||||
else
|
||||
options.set_option("propagation", true);
|
||||
|
||||
// check array bounds
|
||||
if(cmdline.isset("bounds-check"))
|
||||
options.set_option("bounds-check", true);
|
||||
else
|
||||
options.set_option("bounds-check", false);
|
||||
|
||||
// check division by zero
|
||||
if(cmdline.isset("div-by-zero-check"))
|
||||
options.set_option("div-by-zero-check", true);
|
||||
else
|
||||
options.set_option("div-by-zero-check", false);
|
||||
|
||||
// check overflow/underflow
|
||||
if(cmdline.isset("signed-overflow-check"))
|
||||
options.set_option("signed-overflow-check", true);
|
||||
else
|
||||
options.set_option("signed-overflow-check", false);
|
||||
|
||||
// check overflow/underflow
|
||||
if(cmdline.isset("unsigned-overflow-check"))
|
||||
options.set_option("unsigned-overflow-check", true);
|
||||
else
|
||||
options.set_option("unsigned-overflow-check", false);
|
||||
|
||||
// check overflow/underflow
|
||||
if(cmdline.isset("float-overflow-check"))
|
||||
options.set_option("float-overflow-check", true);
|
||||
else
|
||||
options.set_option("float-overflow-check", false);
|
||||
|
||||
// check for NaN (not a number)
|
||||
if(cmdline.isset("nan-check"))
|
||||
options.set_option("nan-check", true);
|
||||
else
|
||||
options.set_option("nan-check", false);
|
||||
|
||||
// check pointers
|
||||
if(cmdline.isset("pointer-check"))
|
||||
options.set_option("pointer-check", true);
|
||||
else
|
||||
options.set_option("pointer-check", false);
|
||||
|
||||
// check for memory leaks
|
||||
if(cmdline.isset("memory-leak-check"))
|
||||
options.set_option("memory-leak-check", true);
|
||||
else
|
||||
options.set_option("memory-leak-check", false);
|
||||
|
||||
// check assertions
|
||||
if(cmdline.isset("no-assertions"))
|
||||
options.set_option("assertions", false);
|
||||
else
|
||||
options.set_option("assertions", true);
|
||||
|
||||
// use assumptions
|
||||
if(cmdline.isset("no-assumptions"))
|
||||
options.set_option("assumptions", false);
|
||||
else
|
||||
options.set_option("assumptions", true);
|
||||
|
||||
// magic error label
|
||||
if(cmdline.isset("error-label"))
|
||||
options.set_option("error-label", cmdline.get_values("error-label"));
|
||||
|
||||
options.set_option("show-properties", cmdline.isset("show-properties"));
|
||||
}
|
||||
|
||||
/// invoke main modules
|
||||
int jdiff_parse_optionst::doit()
|
||||
{
|
||||
if(cmdline.isset("version"))
|
||||
{
|
||||
std::cout << CBMC_VERSION << '\n';
|
||||
return CPROVER_EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
//
|
||||
// command line options
|
||||
//
|
||||
|
||||
optionst options;
|
||||
get_command_line_options(options);
|
||||
eval_verbosity();
|
||||
|
||||
//
|
||||
// Print a banner
|
||||
//
|
||||
status() << "JDIFF version " CBMC_VERSION " " << sizeof(void *) * 8 << "-bit "
|
||||
<< config.this_architecture() << " "
|
||||
<< config.this_operating_system() << eom;
|
||||
|
||||
if(cmdline.args.size() != 2)
|
||||
{
|
||||
error() << "Please provide two programs to compare" << eom;
|
||||
return CPROVER_EXIT_INCORRECT_TASK;
|
||||
}
|
||||
|
||||
goto_modelt goto_model1, goto_model2;
|
||||
|
||||
int get_goto_program_ret = get_goto_program(options, *this, goto_model1);
|
||||
if(get_goto_program_ret != -1)
|
||||
return get_goto_program_ret;
|
||||
get_goto_program_ret = get_goto_program(options, languages2, goto_model2);
|
||||
if(get_goto_program_ret != -1)
|
||||
return get_goto_program_ret;
|
||||
|
||||
if(cmdline.isset("show-loops"))
|
||||
{
|
||||
show_loop_ids(get_ui(), goto_model1);
|
||||
show_loop_ids(get_ui(), goto_model2);
|
||||
return CPROVER_EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
if(
|
||||
cmdline.isset("show-goto-functions") ||
|
||||
cmdline.isset("list-goto-functions"))
|
||||
{
|
||||
show_goto_functions(
|
||||
goto_model1,
|
||||
get_message_handler(),
|
||||
ui_message_handler.get_ui(),
|
||||
cmdline.isset("list-goto-functions"));
|
||||
show_goto_functions(
|
||||
goto_model2,
|
||||
get_message_handler(),
|
||||
ui_message_handler.get_ui(),
|
||||
cmdline.isset("list-goto-functions"));
|
||||
return CPROVER_EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
if(
|
||||
cmdline.isset("change-impact") || cmdline.isset("forward-impact") ||
|
||||
cmdline.isset("backward-impact"))
|
||||
{
|
||||
impact_modet impact_mode =
|
||||
cmdline.isset("forward-impact")
|
||||
? impact_modet::FORWARD
|
||||
: (cmdline.isset("backward-impact") ? impact_modet::BACKWARD
|
||||
: impact_modet::BOTH);
|
||||
change_impact(
|
||||
goto_model1, goto_model2, impact_mode, cmdline.isset("compact-output"));
|
||||
|
||||
return CPROVER_EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
if(cmdline.isset("unified") || cmdline.isset('u'))
|
||||
{
|
||||
unified_difft u(goto_model1, goto_model2);
|
||||
u();
|
||||
u.output(std::cout);
|
||||
|
||||
return CPROVER_EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
java_syntactic_difft sd(
|
||||
goto_model1, goto_model2, options, get_message_handler());
|
||||
sd.set_ui(get_ui());
|
||||
sd();
|
||||
sd.output_functions();
|
||||
|
||||
return CPROVER_EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
int jdiff_parse_optionst::get_goto_program(
|
||||
const optionst &options,
|
||||
jdiff_languagest &languages,
|
||||
goto_modelt &goto_model)
|
||||
{
|
||||
status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
|
||||
|
||||
if(is_goto_binary(cmdline.args[0]))
|
||||
{
|
||||
if(read_goto_binary(
|
||||
cmdline.args[0],
|
||||
goto_model.symbol_table,
|
||||
goto_model.goto_functions,
|
||||
languages.get_message_handler()))
|
||||
return CPROVER_EXIT_INCORRECT_TASK;
|
||||
|
||||
config.set(cmdline);
|
||||
|
||||
// This one is done.
|
||||
cmdline.args.erase(cmdline.args.begin());
|
||||
}
|
||||
else
|
||||
{
|
||||
// This is a a workaround to make parse() think that there is only
|
||||
// one source file.
|
||||
std::string arg2("");
|
||||
if(cmdline.args.size() == 2)
|
||||
{
|
||||
arg2 = cmdline.args[1];
|
||||
cmdline.args.erase(--cmdline.args.end());
|
||||
}
|
||||
|
||||
if(languages.parse() || languages.typecheck() || languages.final())
|
||||
return CPROVER_EXIT_INCORRECT_TASK;
|
||||
|
||||
// we no longer need any parse trees or language files
|
||||
languages.clear_parse();
|
||||
|
||||
status() << "Generating GOTO Program" << eom;
|
||||
|
||||
goto_model.symbol_table = languages.symbol_table;
|
||||
goto_convert(
|
||||
goto_model.symbol_table, goto_model.goto_functions, ui_message_handler);
|
||||
|
||||
if(process_goto_program(options, goto_model))
|
||||
return CPROVER_EXIT_INTERNAL_ERROR;
|
||||
|
||||
// if we had a second argument then we will handle it next
|
||||
if(arg2 != "")
|
||||
cmdline.args[0] = arg2;
|
||||
}
|
||||
|
||||
return -1; // no error, continue
|
||||
}
|
||||
|
||||
bool jdiff_parse_optionst::process_goto_program(
|
||||
const optionst &options,
|
||||
goto_modelt &goto_model)
|
||||
{
|
||||
try
|
||||
{
|
||||
// add the library
|
||||
link_to_library(goto_model, get_message_handler());
|
||||
|
||||
// remove function pointers
|
||||
status() << "Removal of function pointers and virtual functions" << eom;
|
||||
remove_function_pointers(
|
||||
get_message_handler(), goto_model, cmdline.isset("pointer-check"));
|
||||
|
||||
// Java virtual functions -> explicit dispatch tables:
|
||||
remove_virtual_functions(goto_model);
|
||||
// remove catch and throw
|
||||
remove_exceptions(goto_model);
|
||||
// Java instanceof -> clsid comparison:
|
||||
remove_instanceof(goto_model);
|
||||
|
||||
mm_io(goto_model);
|
||||
|
||||
// instrument library preconditions
|
||||
instrument_preconditions(goto_model);
|
||||
|
||||
// remove returns, gcc vectors, complex
|
||||
remove_returns(goto_model);
|
||||
remove_vector(goto_model);
|
||||
remove_complex(goto_model);
|
||||
rewrite_union(goto_model);
|
||||
|
||||
// add generic checks
|
||||
status() << "Generic Property Instrumentation" << eom;
|
||||
goto_check(options, goto_model);
|
||||
|
||||
// checks don't know about adjusted float expressions
|
||||
adjust_float_expressions(goto_model);
|
||||
|
||||
// recalculate numbers, etc.
|
||||
goto_model.goto_functions.update();
|
||||
|
||||
// add loop ids
|
||||
goto_model.goto_functions.compute_loop_numbers();
|
||||
|
||||
// remove skips such that trivial GOTOs are deleted and not considered
|
||||
// for coverage annotation:
|
||||
remove_skip(goto_model);
|
||||
|
||||
// instrument cover goals
|
||||
if(cmdline.isset("cover"))
|
||||
{
|
||||
if(instrument_cover_goals(options, goto_model, get_message_handler()))
|
||||
return true;
|
||||
}
|
||||
|
||||
// label the assertions
|
||||
// This must be done after adding assertions and
|
||||
// before using the argument of the "property" option.
|
||||
// Do not re-label after using the property slicer because
|
||||
// this would cause the property identifiers to change.
|
||||
label_properties(goto_model);
|
||||
|
||||
// remove any skips introduced since coverage instrumentation
|
||||
remove_skip(goto_model);
|
||||
goto_model.goto_functions.update();
|
||||
}
|
||||
|
||||
catch(const char *e)
|
||||
{
|
||||
error() << e << eom;
|
||||
return true;
|
||||
}
|
||||
|
||||
catch(const std::string &e)
|
||||
{
|
||||
error() << e << eom;
|
||||
return true;
|
||||
}
|
||||
|
||||
catch(int e)
|
||||
{
|
||||
error() << "Numeric exception: " << e << eom;
|
||||
return true;
|
||||
}
|
||||
|
||||
catch(const std::bad_alloc &)
|
||||
{
|
||||
error() << "Out of memory" << eom;
|
||||
exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
|
||||
return true;
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
/// display command line help
|
||||
void jdiff_parse_optionst::help()
|
||||
{
|
||||
// clang-format off
|
||||
std::cout <<
|
||||
"\n"
|
||||
// NOLINTNEXTLINE(whitespace/line_length)
|
||||
"* * JDIFF " CBMC_VERSION " - Copyright (C) 2016-2018 * *\n"
|
||||
"* * Daniel Kroening, Peter Schrammel * *\n"
|
||||
"* * kroening@kroening.com * *\n"
|
||||
"\n"
|
||||
"Usage: Purpose:\n"
|
||||
"\n"
|
||||
" jdiff [-?] [-h] [--help] show help\n"
|
||||
" jdiff old new jars to be compared\n"
|
||||
"\n"
|
||||
"Diff options:\n"
|
||||
HELP_SHOW_GOTO_FUNCTIONS
|
||||
HELP_SHOW_PROPERTIES
|
||||
" --syntactic do syntactic diff (default)\n"
|
||||
" -u | --unified output unified diff\n"
|
||||
" --change-impact | \n"
|
||||
" --forward-impact |\n"
|
||||
// NOLINTNEXTLINE(whitespace/line_length)
|
||||
" --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
|
||||
" --compact-output output dependencies in compact mode\n"
|
||||
"\n"
|
||||
"Program instrumentation options:\n"
|
||||
HELP_GOTO_CHECK
|
||||
" --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
|
||||
"Java Bytecode frontend options:\n"
|
||||
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
|
||||
"Other options:\n"
|
||||
" --version show version and exit\n"
|
||||
" --json-ui use JSON-formatted output\n"
|
||||
HELP_TIMESTAMP
|
||||
"\n";
|
||||
// clang-format on
|
||||
}
|
||||
|
|
@ -0,0 +1,74 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: JDIFF Command Line Option Processing
|
||||
|
||||
Author: Peter Schrammel
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
/// \file
|
||||
/// JDIFF Command Line Option Processing
|
||||
|
||||
#ifndef CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H
|
||||
#define CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H
|
||||
|
||||
#include <analyses/goto_check.h>
|
||||
|
||||
#include <util/parse_options.h>
|
||||
#include <util/timestamper.h>
|
||||
#include <util/ui_message.h>
|
||||
|
||||
#include <goto-programs/goto_model.h>
|
||||
#include <goto-programs/show_goto_functions.h>
|
||||
#include <goto-programs/show_properties.h>
|
||||
|
||||
#include "jdiff_languages.h"
|
||||
|
||||
class goto_modelt;
|
||||
class optionst;
|
||||
|
||||
// clang-format off
|
||||
#define JDIFF_OPTIONS \
|
||||
"(json-ui)" \
|
||||
OPT_SHOW_GOTO_FUNCTIONS \
|
||||
OPT_SHOW_PROPERTIES \
|
||||
OPT_GOTO_CHECK \
|
||||
"(cover):" \
|
||||
"(verbosity):(version)" \
|
||||
OPT_TIMESTAMP \
|
||||
"u(unified)(change-impact)(forward-impact)(backward-impact)" \
|
||||
"(compact-output)"
|
||||
// clang-format on
|
||||
|
||||
class jdiff_parse_optionst : public parse_options_baset, public jdiff_languagest
|
||||
{
|
||||
public:
|
||||
virtual int doit();
|
||||
virtual void help();
|
||||
|
||||
jdiff_parse_optionst(int argc, const char **argv);
|
||||
jdiff_parse_optionst(
|
||||
int argc,
|
||||
const char **argv,
|
||||
const std::string &extra_options);
|
||||
|
||||
protected:
|
||||
ui_message_handlert ui_message_handler;
|
||||
jdiff_languagest languages2;
|
||||
|
||||
virtual void get_command_line_options(optionst &options);
|
||||
|
||||
virtual int get_goto_program(
|
||||
const optionst &options,
|
||||
jdiff_languagest &languages,
|
||||
goto_modelt &goto_model);
|
||||
|
||||
virtual bool
|
||||
process_goto_program(const optionst &options, goto_modelt &goto_model);
|
||||
|
||||
void eval_verbosity();
|
||||
|
||||
void preprocessing();
|
||||
};
|
||||
|
||||
#endif // CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H
|
||||
Loading…
Reference in New Issue