From eaf3a7d767bbc87c3dc4d596051a11db86550697 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 5 Jan 2018 23:52:13 +0100 Subject: [PATCH 1/4] Get source location from symbol table Source locations of instructions are not reliable. --- src/goto-diff/goto_diff_base.cpp | 43 +++++++++++++++++--------------- 1 file changed, 23 insertions(+), 20 deletions(-) diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index 1ad26dbee7f..32b6b2949af 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/src/goto-diff/goto_diff_base.cpp @@ -15,6 +15,8 @@ Author: Peter Schrammel std::ostream &goto_difft::output_functions(std::ostream &out) const { + namespacet ns1(goto_model1.symbol_table); + namespacet ns2(goto_model2.symbol_table); switch(ui) { case ui_message_handlert::uit::PLAIN: @@ -24,33 +26,24 @@ std::ostream &goto_difft::output_functions(std::ostream &out) const for(irep_id_sett::const_iterator it=new_functions.begin(); it!=new_functions.end(); ++it) { - const goto_programt &program= - goto_model2.goto_functions.function_map.at(*it).body; - out << " " - << program.instructions.begin()->source_location.get_file() - << ": " << *it << "\n"; + const symbolt &symbol = ns2.lookup(*it); + out << " " << symbol.location.get_file() << ": " << *it << "\n"; } out << "modified functions:\n"; for(irep_id_sett::const_iterator it=modified_functions.begin(); it!=modified_functions.end(); ++it) { - const goto_programt &program= - goto_model2.goto_functions.function_map.at(*it).body; - out << " " - << program.instructions.begin()->source_location.get_file() - << ": " << *it << "\n"; + const symbolt &symbol = ns2.lookup(*it); + out << " " << symbol.location.get_file() << ": " << *it << "\n"; } out << "deleted functions:\n"; for(irep_id_sett::const_iterator it=deleted_functions.begin(); it!=deleted_functions.end(); ++it) { - const goto_programt &program= - goto_model1.goto_functions.function_map.at(*it).body; - out << " " - << program.instructions.begin()->source_location.get_file() - << ": " << *it << "\n"; + const symbolt &symbol = ns1.lookup(*it); + out << " " << symbol.location.get_file() << ": " << *it << "\n"; } break; } @@ -91,12 +84,22 @@ void goto_difft::convert_function( json_objectt &result, const irep_idt &function_name) const { - const goto_programt &program= - goto_model2.goto_functions.function_map.at(function_name).body; - if(!program.instructions.empty()) + // the function may be in goto_model1 or goto_model2 + if( + goto_model1.goto_functions.function_map.find(function_name) != + goto_model1.goto_functions.function_map.end()) { - result["sourceLocation"]= - json(program.instructions.begin()->source_location); + const symbolt &symbol = + namespacet(goto_model1.symbol_table).lookup(function_name); + result["sourceLocation"] = json(symbol.location); + } + else if( + goto_model2.goto_functions.function_map.find(function_name) != + goto_model2.goto_functions.function_map.end()) + { + const symbolt &symbol = + namespacet(goto_model2.symbol_table).lookup(function_name); + result["sourceLocation"] = json(symbol.location); } result["name"]=json_stringt(id2string(function_name)); } From 9ef28f411fcf1ae260050c04e99b9361c78eba03 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 5 Jan 2018 23:28:29 +0100 Subject: [PATCH 2/4] Compare relative goto target offsets Goto location numbers of unmodified functions may shift when functions are added/modified/removed. --- src/goto-diff/syntactic_diff.cpp | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/src/goto-diff/syntactic_diff.cpp b/src/goto-diff/syntactic_diff.cpp index 030d35e0f3c..68b7379b688 100644 --- a/src/goto-diff/syntactic_diff.cpp +++ b/src/goto-diff/syntactic_diff.cpp @@ -42,11 +42,22 @@ bool syntactic_difft::operator()() i_it2!=f_it->second.body.instructions.end(); ++i_it1, ++i_it2) { - 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 || - i_it1->targets != i_it2->targets) + 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; From 43d2e09d8e31ad53c6c53b0d9719af7b480ef81f Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 5 Jan 2018 23:30:19 +0100 Subject: [PATCH 3/4] Also reset fresh temporary symbol counter Otherwise temporary identifiers are not comparable in goto-diff. --- src/goto-programs/goto_convert_functions.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 8a4f28c4dd7..4aa3c8d90ee 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -16,6 +16,7 @@ Date: June 2003 #include #include #include +#include #include "goto_inline.h" @@ -145,6 +146,7 @@ void goto_convert_functionst::convert_function( // make tmp variables local to function tmp_symbol_prefix=id2string(symbol.name)+"::$tmp::"; temporary_counter=0; + reset_temporary_counter(); f.type=to_code_type(symbol.type); From 2811363409dd41364e01fdfc03aaa911ec8f021c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 5 Jan 2018 23:32:12 +0100 Subject: [PATCH 4/4] Java regression test for goto-diff --- .../goto-diff/syntactic-diff-java1/new.jar | Bin 0 -> 397 bytes .../syntactic-diff-java1/new/Test.java | 16 ++++++++++++++++ .../goto-diff/syntactic-diff-java1/old.jar | Bin 0 -> 396 bytes .../syntactic-diff-java1/old/Test.java | 16 ++++++++++++++++ .../goto-diff/syntactic-diff-java1/test.desc | 10 ++++++++++ 5 files changed, 42 insertions(+) create mode 100644 regression/goto-diff/syntactic-diff-java1/new.jar create mode 100644 regression/goto-diff/syntactic-diff-java1/new/Test.java create mode 100644 regression/goto-diff/syntactic-diff-java1/old.jar create mode 100644 regression/goto-diff/syntactic-diff-java1/old/Test.java create mode 100644 regression/goto-diff/syntactic-diff-java1/test.desc diff --git a/regression/goto-diff/syntactic-diff-java1/new.jar b/regression/goto-diff/syntactic-diff-java1/new.jar new file mode 100644 index 0000000000000000000000000000000000000000..2966f96251798ea6259ae0cb0532b0ce5f132475 GIT binary patch literal 397 zcmWIWW@Zs#U|`^2Fx;T(vnM!W>ti4CqG+q?>-(N