diff --git a/regression/Makefile b/regression/Makefile index b2f31798489..cec34c0b37f 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -3,6 +3,7 @@ DIRS = ansi-c \ cbmc \ cpp \ cbmc-java \ + cbmc-java-inheritance \ goto-analyzer \ goto-instrument \ goto-instrument-typedef \ diff --git a/regression/cbmc-java-inheritance/Makefile b/regression/cbmc-java-inheritance/Makefile new file mode 100644 index 00000000000..dcdf752aea1 --- /dev/null +++ b/regression/cbmc-java-inheritance/Makefile @@ -0,0 +1,38 @@ +default: tests.log + +test: + @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +tests.log: ../test.pl + @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.java" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + $(RM) tests.log + +%.class: %.java ../../src/org.cprover.jar + javac -g -cp ../../src/org.cprover.jar:. $< + +nondet_java_files := $(shell find . -name "Nondet*.java") +nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files)) + +.PHONY: nondet-class-files +nondet-class-files: $(nondet_class_files) + +.PHONY: clean-nondet-class-files +clean-nondet-class-files: + -rm $(nondet_class_files) diff --git a/regression/cbmc-java-inheritance/inheritance01/A.class b/regression/cbmc-java-inheritance/inheritance01/A.class new file mode 100644 index 00000000000..90633af3927 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance01/A.class differ diff --git a/regression/cbmc-java-inheritance/inheritance01/B.class b/regression/cbmc-java-inheritance/inheritance01/B.class new file mode 100644 index 00000000000..1ba2667c1e3 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance01/B.class differ diff --git a/regression/cbmc-java-inheritance/inheritance01/test.class b/regression/cbmc-java-inheritance/inheritance01/test.class new file mode 100644 index 00000000000..c8b094f59ad Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance01/test.class differ diff --git a/regression/cbmc-java-inheritance/inheritance01/test.desc b/regression/cbmc-java-inheritance/inheritance01/test.desc new file mode 100644 index 00000000000..61ed56c4b41 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance01/test.desc @@ -0,0 +1,5 @@ +CORE +test.class +--function test.check +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java-inheritance/inheritance01/test.java b/regression/cbmc-java-inheritance/inheritance01/test.java new file mode 100644 index 00000000000..4038d8419f6 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance01/test.java @@ -0,0 +1,20 @@ +class A +{ + public int toInt() + { + return 12345; + } +} + +class B extends A +{ +} + +class test +{ + void check() + { + B b=new B(); + assert(b.toInt()==12345); + } +} diff --git a/regression/cbmc-java-inheritance/inheritance02/A.class b/regression/cbmc-java-inheritance/inheritance02/A.class new file mode 100644 index 00000000000..20d9f12ec40 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance02/A.class differ diff --git a/regression/cbmc-java-inheritance/inheritance02/B.class b/regression/cbmc-java-inheritance/inheritance02/B.class new file mode 100644 index 00000000000..cd5a6778035 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance02/B.class differ diff --git a/regression/cbmc-java-inheritance/inheritance02/test.class b/regression/cbmc-java-inheritance/inheritance02/test.class new file mode 100644 index 00000000000..09d573eb971 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance02/test.class differ diff --git a/regression/cbmc-java-inheritance/inheritance02/test.desc b/regression/cbmc-java-inheritance/inheritance02/test.desc new file mode 100644 index 00000000000..61ed56c4b41 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance02/test.desc @@ -0,0 +1,5 @@ +CORE +test.class +--function test.check +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java-inheritance/inheritance02/test.java b/regression/cbmc-java-inheritance/inheritance02/test.java new file mode 100644 index 00000000000..1aae7f2ef63 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance02/test.java @@ -0,0 +1,24 @@ +class A +{ + protected int toInt() + { + return 12345; + } +} + +class B extends A +{ + public void secondary() + { + assert(toInt()==12345); + } +} + +class test +{ + void check() + { + B b=new B(); + b.secondary(); + } +} diff --git a/regression/cbmc-java-inheritance/inheritance03/A.class b/regression/cbmc-java-inheritance/inheritance03/A.class new file mode 100644 index 00000000000..1df27f96de7 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance03/A.class differ diff --git a/regression/cbmc-java-inheritance/inheritance03/B.class b/regression/cbmc-java-inheritance/inheritance03/B.class new file mode 100644 index 00000000000..0d68ec19ee0 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance03/B.class differ diff --git a/regression/cbmc-java-inheritance/inheritance03/Z.class b/regression/cbmc-java-inheritance/inheritance03/Z.class new file mode 100644 index 00000000000..49b6e283992 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance03/Z.class differ diff --git a/regression/cbmc-java-inheritance/inheritance03/test.class b/regression/cbmc-java-inheritance/inheritance03/test.class new file mode 100644 index 00000000000..dfa16d22feb Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance03/test.class differ diff --git a/regression/cbmc-java-inheritance/inheritance03/test.desc b/regression/cbmc-java-inheritance/inheritance03/test.desc new file mode 100644 index 00000000000..61ed56c4b41 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance03/test.desc @@ -0,0 +1,5 @@ +CORE +test.class +--function test.check +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java-inheritance/inheritance03/test.java b/regression/cbmc-java-inheritance/inheritance03/test.java new file mode 100644 index 00000000000..0d965134877 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance03/test.java @@ -0,0 +1,24 @@ +class Z +{ + public int toInt() + { + return 12345; + } +} + +class A extends Z +{ +} + +class B extends A +{ +} + +class test +{ + void check() + { + B b=new B(); + assert(b.toInt()==12345); + } +} diff --git a/regression/cbmc-java-inheritance/inheritance04/A.class b/regression/cbmc-java-inheritance/inheritance04/A.class new file mode 100644 index 00000000000..90633af3927 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance04/A.class differ diff --git a/regression/cbmc-java-inheritance/inheritance04/B.class b/regression/cbmc-java-inheritance/inheritance04/B.class new file mode 100644 index 00000000000..b8d4c0dafbc Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance04/B.class differ diff --git a/regression/cbmc-java-inheritance/inheritance04/Z.class b/regression/cbmc-java-inheritance/inheritance04/Z.class new file mode 100644 index 00000000000..74b27f055a5 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance04/Z.class differ diff --git a/regression/cbmc-java-inheritance/inheritance04/test.class b/regression/cbmc-java-inheritance/inheritance04/test.class new file mode 100644 index 00000000000..7f4c18b5fde Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance04/test.class differ diff --git a/regression/cbmc-java-inheritance/inheritance04/test.desc b/regression/cbmc-java-inheritance/inheritance04/test.desc new file mode 100644 index 00000000000..61ed56c4b41 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance04/test.desc @@ -0,0 +1,5 @@ +CORE +test.class +--function test.check +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java-inheritance/inheritance04/test.java b/regression/cbmc-java-inheritance/inheritance04/test.java new file mode 100644 index 00000000000..783e0079c37 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance04/test.java @@ -0,0 +1,28 @@ +class A +{ + public int toInt() + { + return 12345; + } +} + +class B extends A +{ + public int toInt() + { + return 9999; + } +} + +class Z extends B +{ +} + +class test +{ + void check() + { + Z z=new Z(); + assert(z.toInt()==9999); + } +} diff --git a/regression/cbmc-java-inheritance/inheritance05/A.class b/regression/cbmc-java-inheritance/inheritance05/A.class new file mode 100644 index 00000000000..692fc625e18 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance05/A.class differ diff --git a/regression/cbmc-java-inheritance/inheritance05/B.class b/regression/cbmc-java-inheritance/inheritance05/B.class new file mode 100644 index 00000000000..d1f3c3841a6 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance05/B.class differ diff --git a/regression/cbmc-java-inheritance/inheritance05/test.class b/regression/cbmc-java-inheritance/inheritance05/test.class new file mode 100644 index 00000000000..549b549c5de Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance05/test.class differ diff --git a/regression/cbmc-java-inheritance/inheritance05/test.desc b/regression/cbmc-java-inheritance/inheritance05/test.desc new file mode 100644 index 00000000000..61ed56c4b41 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance05/test.desc @@ -0,0 +1,5 @@ +CORE +test.class +--function test.check +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java-inheritance/inheritance05/test.java b/regression/cbmc-java-inheritance/inheritance05/test.java new file mode 100644 index 00000000000..3d0c967b728 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance05/test.java @@ -0,0 +1,21 @@ +interface A +{ + public int toInt(); +} + +class B implements A +{ + public int toInt() + { + return 12345; + } +} + +class test +{ + void check() + { + B b=new B(); + assert(b.toInt()==12345); + } +} diff --git a/regression/cbmc-java-inheritance/inheritance06/A.java b/regression/cbmc-java-inheritance/inheritance06/A.java new file mode 100644 index 00000000000..d2f2e7b43dc --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance06/A.java @@ -0,0 +1,10 @@ +package temp; + +class A +{ + int toint() + { + return 123456; + } +} + diff --git a/regression/cbmc-java-inheritance/inheritance06/B.java b/regression/cbmc-java-inheritance/inheritance06/B.java new file mode 100644 index 00000000000..4bd0f629038 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance06/B.java @@ -0,0 +1,9 @@ +package temp; + +public class B extends A +{ + public int check() + { + return toint(); + } +} diff --git a/regression/cbmc-java-inheritance/inheritance06/temp/A.class b/regression/cbmc-java-inheritance/inheritance06/temp/A.class new file mode 100644 index 00000000000..8e5acf1693d Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance06/temp/A.class differ diff --git a/regression/cbmc-java-inheritance/inheritance06/temp/B.class b/regression/cbmc-java-inheritance/inheritance06/temp/B.class new file mode 100644 index 00000000000..a4d9cfb5fb2 Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance06/temp/B.class differ diff --git a/regression/cbmc-java-inheritance/inheritance06/test.class b/regression/cbmc-java-inheritance/inheritance06/test.class new file mode 100644 index 00000000000..53ce4d575ca Binary files /dev/null and b/regression/cbmc-java-inheritance/inheritance06/test.class differ diff --git a/regression/cbmc-java-inheritance/inheritance06/test.desc b/regression/cbmc-java-inheritance/inheritance06/test.desc new file mode 100644 index 00000000000..61ed56c4b41 --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance06/test.desc @@ -0,0 +1,5 @@ +CORE +test.class +--function test.check +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java-inheritance/inheritance06/test.java b/regression/cbmc-java-inheritance/inheritance06/test.java new file mode 100644 index 00000000000..fd8633b51bc --- /dev/null +++ b/regression/cbmc-java-inheritance/inheritance06/test.java @@ -0,0 +1,11 @@ +import temp.B; + +public class test +{ + public void check() + { + B myObject = new B(); + assert(myObject.check()==123456); + } +} + diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index b9a3cf00063..14b67ba330f 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -19,11 +19,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include +#include #include #include "java_bytecode_convert_method.h" @@ -32,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_types.h" #include "java_utils.h" #include "java_string_library_preprocess.h" +#include "java_utils.h" #include #include @@ -1428,12 +1431,12 @@ codet java_bytecode_convert_methodt::convert_instructions( assert(arg0.id()==ID_virtual_function); - // does the function symbol exist? + // if we don't have a definition for the called symbol, and we won't + // inherit a definition from a super-class, create a stub. irep_idt id=arg0.get(ID_identifier); - - if(symbol_table.symbols.find(id)==symbol_table.symbols.end()) + if(symbol_table.symbols.find(id)==symbol_table.symbols.end() && + !(is_virtual && is_method_inherited(arg0.get(ID_C_class), id))) { - // no, create stub symbolt symbol; symbol.name=id; symbol.base_name=arg0.get(ID_C_base_name); @@ -2687,3 +2690,40 @@ void java_bytecode_convert_method( java_bytecode_convert_method(class_symbol, method); } + +const bool java_bytecode_convert_methodt::is_method_inherited( + const irep_idt &classname, const irep_idt &methodid) const +{ + class_hierarchyt ch; + namespacet ns(symbol_table); + ch(symbol_table); + + std::string stripped_methodid(id2string(methodid)); + stripped_methodid.erase(0, classname.size()); + + const std::string &classpackage=java_class_to_package(id2string(classname)); + const auto &parents=ch.get_parents_trans(classname); + for(const auto &parent : parents) + { + const irep_idt id=id2string(parent)+stripped_methodid; + const symbolt *symbol; + if(!ns.lookup(id, symbol) && + symbol->type.id()==ID_code) + { + const auto &access=symbol->type.get(ID_access); + if(access==ID_public || access==ID_protected) + return true; + // methods with the default access modifier are only + // accessible within the same package. + else if(access==ID_default && + java_class_to_package(id2string(parent))==classpackage) + return true; + else if(access==ID_private) + continue; + else + INVARIANT(false, "Unexpected access modifier."); + } + } + return false; +} + diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index 8eba408ddff..f44df98be49 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -258,6 +258,10 @@ class java_bytecode_convert_methodt:public messaget bool class_needs_clinit(const irep_idt &classname); exprt get_or_create_clinit_wrapper(const irep_idt &classname); codet get_clinit_call(const irep_idt &classname); + + const bool is_method_inherited( + const irep_idt &classname, + const irep_idt &methodid) const; }; #endif diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index 656bfe1d7b2..9f8be11e4ad 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "java_utils.h" #include "java_types.h" @@ -52,3 +53,8 @@ unsigned java_method_parameter_slots(const code_typet &t) return slots; } + +const std::string java_class_to_package(const std::string &canonical_classname) +{ + return trim_from_last_delimiter(canonical_classname, '.'); +} diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index bd88cb71bb8..ef64ff9e18e 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -24,4 +24,6 @@ unsigned java_local_variable_slots(const typet &t); /// pass, upon call, the arguments of a Java method whose type is \p t. unsigned java_method_parameter_slots(const code_typet &t); +const std::string java_class_to_package(const std::string &canonical_classname); + #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index 1bf5af4f68a..77e559b96c1 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -99,3 +99,14 @@ void split_string( left=result[0]; right=result[1]; } + +std::string trim_from_last_delimiter( + const std::string &s, + const char delim) +{ + std::string result=""; + const size_t index=s.find_last_of(delim); + if(index!=std::string::npos) + result=s.substr(0, index); + return result; +} diff --git a/src/util/string_utils.h b/src/util/string_utils.h index 5e4ef23a63a..5779596cdcf 100644 --- a/src/util/string_utils.h +++ b/src/util/string_utils.h @@ -29,4 +29,8 @@ void split_string( std::string &right, bool strip=false); +std::string trim_from_last_delimiter( + const std::string &s, + const char delim); + #endif