Skip to content

Commit 059da82

Browse files
author
Peter Schrammel
committed
goto-diff initial
1 parent 151bded commit 059da82

10 files changed

+1057
-2
lines changed

‎src/Makefile

+5-2
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \
22
goto-symex langapi pointer-analysis solvers util linking xmllang \
33
assembler analyses java_bytecode aa-path-symex path-symex musketeer \
4-
json cegis goto-analyzer jsil
4+
json cegis goto-analyzer jsil goto-diff
55

6-
all: cbmc.dir goto-cc.dir goto-instrument.dir path-symex.dir goto-analyzer.dir
6+
all: cbmc.dir goto-cc.dir goto-instrument.dir path-symex.dir goto-analyzer.dir goto-diff.dir
77

88
###############################################################################
99

@@ -34,6 +34,9 @@ cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
3434
goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
3535
json.dir goto-instrument.dir
3636

37+
goto-diff.dir: languages goto-programs.dir pointer-analysis.dir \
38+
linking.dir analyses.dir solvers.dir json.dir
39+
3740
goto-cc.dir: languages pointer-analysis.dir goto-programs.dir linking.dir
3841

3942
# building for a particular directory

‎src/goto-diff/Makefile

+59
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
SRC = goto_diff_main.cpp goto_diff_parse_options.cpp \
2+
goto_diff_languages.cpp goto_diff_base.cpp syntactic_diff.cpp
3+
4+
OBJ += ../ansi-c/ansi-c$(LIBEXT) \
5+
../linking/linking$(LIBEXT) \
6+
../big-int/big-int$(LIBEXT) \
7+
../goto-programs/goto-programs$(LIBEXT) \
8+
../assembler/assembler$(LIBEXT) \
9+
../pointer-analysis/pointer-analysis$(LIBEXT) \
10+
../analyses/analyses$(LIBEXT) \
11+
../langapi/langapi$(LIBEXT) \
12+
../xmllang/xmllang$(LIBEXT) \
13+
../util/util$(LIBEXT) \
14+
../solvers/solvers$(LIBEXT)
15+
16+
INCLUDES= -I ..
17+
18+
LIBS =
19+
20+
include ../config.inc
21+
include ../common
22+
23+
CLEANFILES = goto-diff$(EXEEXT)
24+
25+
all: goto-diff$(EXEEXT)
26+
27+
ifneq ($(wildcard ../cpp/Makefile),)
28+
OBJ += ../cpp/cpp$(LIBEXT)
29+
CP_CXXFLAGS += -DHAVE_CPP
30+
endif
31+
32+
ifneq ($(wildcard ../java_bytecode/Makefile),)
33+
OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
34+
CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
35+
ifneq ($(wildcard $(LIBZIPINC)),)
36+
LIBS += $(LIBZIPLIB)
37+
endif
38+
endif
39+
40+
ifneq ($(wildcard ../specc/Makefile),)
41+
OBJ += ../specc/specc$(LIBEXT)
42+
CP_CXXFLAGS += -DHAVE_SPECC
43+
endif
44+
45+
ifneq ($(wildcard ../php/Makefile),)
46+
OBJ += ../php/php$(LIBEXT)
47+
CP_CXXFLAGS += -DHAVE_PHP
48+
endif
49+
50+
###############################################################################
51+
52+
goto-diff$(EXEEXT): $(OBJ)
53+
$(LINKBIN)
54+
55+
.PHONY: goto-diff-mac-signed
56+
57+
cbmc-mac-signed: goto-diff$(EXEEXT)
58+
strip goto-diff$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) goto-diff$(EXEEXT)
59+

‎src/goto-diff/goto_diff.h

+59
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
/*******************************************************************\
2+
3+
Module: GOTO-DIFF Base Class
4+
5+
Author: Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_GOTO_DIFF_BASE_H
10+
#define CPROVER_GOTO_DIFF_BASE_H
11+
12+
#include <goto-programs/goto_model.h>
13+
#include <langapi/language_ui.h>
14+
#include <util/message.h>
15+
#include <util/json.h>
16+
17+
#include <ostream>
18+
19+
class goto_difft : public messaget
20+
{
21+
public:
22+
explicit goto_difft(
23+
const goto_modelt &_goto_model1,
24+
const goto_modelt &_goto_model2,
25+
message_handlert &_message_handler
26+
)
27+
:
28+
messaget(_message_handler),
29+
goto_model1(_goto_model1),
30+
goto_model2(_goto_model2),
31+
ui(ui_message_handlert::PLAIN),
32+
total_functions_count(0)
33+
{}
34+
35+
virtual bool operator()()=0;
36+
37+
void set_ui(language_uit::uit _ui) { ui=_ui; }
38+
39+
virtual std::ostream &output_functions(std::ostream &out) const;
40+
41+
protected:
42+
const goto_modelt &goto_model1;
43+
const goto_modelt &goto_model2;
44+
language_uit::uit ui;
45+
46+
unsigned total_functions_count;
47+
typedef std::set<irep_idt> irep_id_sett;
48+
irep_id_sett new_functions, modified_functions, deleted_functions;
49+
50+
void convert_function_group(
51+
json_arrayt &result,
52+
const irep_id_sett &function_group) const;
53+
void convert_function(
54+
json_objectt &result,
55+
const irep_idt &function_name) const;
56+
57+
};
58+
59+
#endif

‎src/goto-diff/goto_diff_base.cpp

+132
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,132 @@
1+
/*******************************************************************\
2+
3+
Module: GOTO-DIFF Base Class
4+
5+
Author: Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
#include <util/i2string.h>
10+
11+
#include "goto_diff.h"
12+
13+
/*******************************************************************\
14+
15+
Function: goto_difft::output_functions
16+
17+
Inputs:
18+
19+
Outputs:
20+
21+
Purpose:
22+
23+
\*******************************************************************/
24+
25+
std::ostream &goto_difft::output_functions(std::ostream &out) const
26+
{
27+
switch(ui)
28+
{
29+
case ui_message_handlert::PLAIN:
30+
{
31+
out << "total number of functions: " << total_functions_count << "\n";
32+
out << "new functions: \n";
33+
for(irep_id_sett::const_iterator it=new_functions.begin();
34+
it!=new_functions.end(); ++it)
35+
{
36+
const goto_programt &program=
37+
goto_model2.goto_functions.function_map.at(*it).body;
38+
out << " "
39+
<< program.instructions.begin()->source_location.get_file()
40+
<< ": " << *it << "\n";
41+
}
42+
43+
out << "modified functions: \n";
44+
for(irep_id_sett::const_iterator it=modified_functions.begin();
45+
it!=modified_functions.end(); ++it)
46+
{
47+
const goto_programt &program=
48+
goto_model2.goto_functions.function_map.at(*it).body;
49+
out << " "
50+
<< program.instructions.begin()->source_location.get_file()
51+
<< ": " << *it << "\n";
52+
}
53+
54+
out << "deleted functions: \n";
55+
for(irep_id_sett::const_iterator it=deleted_functions.begin();
56+
it!=deleted_functions.end(); ++it)
57+
{
58+
const goto_programt &program=
59+
goto_model2.goto_functions.function_map.at(*it).body;
60+
out << " "
61+
<< program.instructions.begin()->source_location.get_file()
62+
<< ": " << *it << "\n";
63+
}
64+
break;
65+
}
66+
case ui_message_handlert::JSON_UI:
67+
{
68+
json_objectt json_result;
69+
json_result["totalNumberOfFunctions"]=
70+
json_stringt(i2string(total_functions_count));
71+
convert_function_group
72+
(json_result["newFunctions"].make_array(), new_functions);
73+
convert_function_group(
74+
json_result["modifiedFunctions"].make_array(), modified_functions);
75+
convert_function_group(
76+
json_result["deletedFunctions"].make_array(), deleted_functions);
77+
out << ",\n" << json_result;
78+
break;
79+
}
80+
case ui_message_handlert::XML_UI:
81+
{
82+
out << "not supported yet";
83+
}
84+
}
85+
return out;
86+
}
87+
88+
/*******************************************************************\
89+
90+
Function: goto_difft::convert_function_group
91+
92+
Inputs:
93+
94+
Outputs:
95+
96+
Purpose:
97+
98+
\*******************************************************************/
99+
100+
void goto_difft::convert_function_group(
101+
json_arrayt &result,
102+
const irep_id_sett &function_group) const
103+
{
104+
for(irep_id_sett::const_iterator it=function_group.begin();
105+
it!=function_group.end(); ++it)
106+
{
107+
convert_function(result.push_back(jsont()).make_object(), *it);
108+
}
109+
}
110+
111+
/*******************************************************************\
112+
113+
Function: goto_difft::convert_functions
114+
115+
Inputs:
116+
117+
Outputs:
118+
119+
Purpose:
120+
121+
\*******************************************************************/
122+
123+
void goto_difft::convert_function(
124+
json_objectt &result,
125+
const irep_idt &function_name) const
126+
{
127+
const goto_programt &program=
128+
goto_model2.goto_functions.function_map.at(function_name).body;
129+
result["file"]=json_stringt(
130+
id2string(program.instructions.begin()->source_location.get_file()));
131+
result["name"]=json_stringt(id2string(function_name));
132+
}

‎src/goto-diff/goto_diff_languages.cpp

+49
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
/*******************************************************************\
2+
3+
Module: Language Registration
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <langapi/mode.h>
10+
11+
#include <ansi-c/ansi_c_language.h>
12+
#include <cpp/cpp_language.h>
13+
14+
#ifdef HAVE_SPECC
15+
#include <specc/specc_language.h>
16+
#endif
17+
18+
#ifdef HAVE_JAVA_BYTECODE
19+
#include <java_bytecode/java_bytecode_language.h>
20+
#endif
21+
22+
#include "goto_diff_parse_options.h"
23+
24+
/*******************************************************************\
25+
26+
Function: goto_diff_parse_optionst::register_languages
27+
28+
Inputs:
29+
30+
Outputs:
31+
32+
Purpose:
33+
34+
\*******************************************************************/
35+
36+
void goto_diff_parse_optionst::register_languages()
37+
{
38+
register_language(new_ansi_c_language);
39+
register_language(new_cpp_language);
40+
41+
#ifdef HAVE_SPECC
42+
register_language(new_specc_language);
43+
#endif
44+
45+
#ifdef HAVE_JAVA_BYTECODE
46+
register_language(new_java_bytecode_language);
47+
#endif
48+
}
49+

‎src/goto-diff/goto_diff_main.cpp

+54
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
/*******************************************************************\
2+
3+
Module: GOTO-DIFF Main Module
4+
5+
Author: Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
#include <util/unicode.h>
10+
11+
#ifdef IREP_HASH_STATS
12+
#include <iostream>
13+
#endif
14+
15+
#include "goto_diff_parse_options.h"
16+
17+
/*******************************************************************\
18+
19+
Function: main / wmain
20+
21+
Inputs:
22+
23+
Outputs:
24+
25+
Purpose:
26+
27+
\*******************************************************************/
28+
29+
#ifdef IREP_HASH_STATS
30+
extern unsigned long long irep_hash_cnt;
31+
extern unsigned long long irep_cmp_cnt;
32+
extern unsigned long long irep_cmp_ne_cnt;
33+
#endif
34+
35+
#ifdef _MSC_VER
36+
int wmain(int argc, const wchar_t **argv_wide)
37+
{
38+
const char **argv=narrow_argv(argc, argv_wide);
39+
#else
40+
int main(int argc, const char **argv)
41+
{
42+
#endif
43+
goto_diff_parse_optionst parse_options(argc, argv);
44+
45+
int res=parse_options.main();
46+
47+
#ifdef IREP_HASH_STATS
48+
std::cout << "IREP_HASH_CNT=" << irep_hash_cnt << std::endl;
49+
std::cout << "IREP_CMP_CNT=" << irep_cmp_cnt << std::endl;
50+
std::cout << "IREP_CMP_NE_CNT=" << irep_cmp_ne_cnt << std::endl;
51+
#endif
52+
53+
return res;
54+
}

0 commit comments

Comments
 (0)