-
Notifications
You must be signed in to change notification settings - Fork 273
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[TG-3374] Fix generic_type_index #2129
[TG-3374] Fix generic_type_index #2129
Conversation
src/java_bytecode/java_types.h
Outdated
std::find(generic_types().begin(), generic_types().end(), type); | ||
if(type_pointer != generic_types().end()) | ||
return type_pointer - generic_types().begin(); | ||
const auto type_variables = type.find(ID_type_variables); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
const auto &type_variables
src/java_bytecode/java_types.h
Outdated
{ | ||
if(type_variables == generic_types()[i].find(ID_type_variables)) | ||
return i; | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This approach will do a lot of calls to generic_types()
. At bare minimum create a temporary, but you might also do:
std::size_t index = 0;
for(const auto &generic_type : generic_types())
{
if(type_variables == generic_type.find(ID_type_variables))
return index;
++index;
}
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also discussed offline, the implementation could be made more understandable by using existing functions.
src/java_bytecode/java_types.h
Outdated
std::find(generic_types().begin(), generic_types().end(), type); | ||
if(type_pointer != generic_types().end()) | ||
return type_pointer - generic_types().begin(); | ||
const auto type_variables = type.find(ID_type_variables); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I ran the example in the test to understand better where the problem was. What happens here basically is that if in this function we are trying to find an index of a generic parameter (rather then a concrete type), the function does not work well. This is because the name of the parameter is a comment in the irep and thus does not get compared. The name of the parameter is in ID_type_variables, that's why you need to pull it out here. In order to make it more clear is happening, could you please use std::find_if
and make use of the functions is_java_generic_parameter
, to_java_generic_parameter().get_name()
?
c06c7e4
to
9369bbe
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'd really like a unit test - the change seems correct but I can't follow what was wrong before and why the attached ticket failed it.
AbstractImpl<Dummy, Dummy> dummy = new AbstractImpl<>(); | ||
ClassB b = arg.get(); | ||
int i = b.getId(); | ||
return i; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: dodgy formatting
src/java_bytecode/java_types.h
Outdated
@@ -609,12 +609,18 @@ class java_generic_symbol_typet : public symbol_typet | |||
/// in the vector of generic types. | |||
/// \param type The type we are looking for. | |||
/// \return The index of the type in the vector of generic types. | |||
optionalt<size_t> generic_type_index(const reference_typet &type) const | |||
optionalt<size_t> | |||
generic_type_index(const java_generic_parametert &type) const |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you were to write a trivial unit test for this function that would be 👌 to easily see why it was broken before but not now.
c286b78
to
d86e8e4
Compare
@thk123 I added some unit tests for this and for two other functions on which my test depended |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the tests they look really good. I've got a couple of stylistic suggestions but nothing blocking
src/java_bytecode/java_types.cpp
Outdated
return i; | ||
} | ||
return {}; | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: missing new line
src/java_bytecode/java_types.h
Outdated
@@ -579,21 +579,17 @@ class java_generic_symbol_typet : public symbol_typet | |||
public: | |||
typedef std::vector<reference_typet> generic_typest; | |||
|
|||
/// Construct a generic symbol type from base_ref and class_name_prefix which |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Docs live with the implementation
|
||
SCENARIO("generic_type_index", "[core][java_types]") | ||
{ | ||
// Arrange |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
More "in style" to use the Catch keywords GIVEN
WHEN
and THEN
instead of arrange/act/assert
// Arrange | ||
const auto symbol_type = symbol_typet("MyType"); | ||
const auto generic_symbol_type = java_generic_symbol_typet( | ||
symbol_type, "LGenericClass<TX;TY;>;", "PrefixClassName"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Suggested additions: Non-single letter generic parameter name, name corresponding to a real class
REQUIRE(indexX.value() == 0); | ||
REQUIRE(indexY.has_value()); | ||
REQUIRE(indexY.value() == 1); | ||
REQUIRE(!indexZ.has_value()); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: Prefer REQUIRE_FALSE
as harder to miss than !
{ | ||
WHEN("Ljava/lang/Integer;") | ||
{ | ||
const auto generic_symbol_type = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
generic_symbol_type
isn't a great variable name. If you could also put a TODO in these tests to indicate they aren't very comprehensive 😛
d86e8e4
to
3406eb2
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good but still few adjustments needed.
src/java_bytecode/java_types.h
Outdated
std::find(generic_types().begin(), generic_types().end(), type); | ||
if(type_pointer != generic_types().end()) | ||
return type_pointer - generic_types().begin(); | ||
const auto &type_variable = type.type_variable(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Instead of type_variable
use get_name()
to get the unique name of the parameter.
src/java_bytecode/java_types.h
Outdated
{ | ||
if( | ||
is_java_generic_parameter(generics[i]) && | ||
to_java_generic_parameter(generics[i]).type_variable() == type_variable) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Use get_name()
again, see above.
src/java_bytecode/java_types.h
Outdated
@@ -609,12 +609,18 @@ class java_generic_symbol_typet : public symbol_typet | |||
/// in the vector of generic types. | |||
/// \param type The type we are looking for. | |||
/// \return The index of the type in the vector of generic types. | |||
optionalt<size_t> generic_type_index(const reference_typet &type) const | |||
optionalt<size_t> | |||
generic_type_index(const java_generic_parametert &type) const |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please update the documentation to reflect that only a generic parameter can be passed here. Also, wherever this function is called, make sure that it's only called on a parameter - for example by adding preconditions if it's not obvious.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The type already ensures it is only called on a java_generic_parametert so I don't think a precondition is necessary
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I meant a precondition before a call to this function, elsewhere in the code.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If the function is called then the argument is a java_generic_parametert so there shouldn't be anything to check?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, that's exactly what I meant - if the object that this function is called with is already typed as java_generic_parametert
then there is nothing to check.
src/java_bytecode/java_types.h
Outdated
@@ -610,19 +599,7 @@ class java_generic_symbol_typet : public symbol_typet | |||
/// \param type The type we are looking for. | |||
/// \return The index of the type in the vector of generic types. | |||
optionalt<size_t> | |||
generic_type_index(const java_generic_parametert &type) const |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Move the documentation too.
src/java_bytecode/java_types.h
Outdated
/// For instance `java_generic_symbol_typet(symbol_typet("Map"), | ||
/// "Ljava/util/Map<TK;TV;>;", "java/util/Map")` will generate a symbol type | ||
/// with identifier "Map", and two generic types with identifier | ||
/// "java/util/Map::K" and "java/util/Map::V" respectively. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
To reflect what this does a bit better I would say - Construct a generic symbol type by extending the symbol type \p type with generic types extracted from the reference \p base_ref. This assumes that the class with name \p class_name_prefix extends/implements the class in \p type.
For the example you give, I would change the third input to "java/util/HashMap" and then the generic types identifiers become "java.util.HashMap::K" and "java.util.HashMap::V".
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually, there should be a precondition in the constructor that checks that the identifier of type
and the identifier of the type created for base_ref
are the same. But that is up to you if you want to add this here, I can do that in a separate PR.
{ | ||
auto symbol_type = symbol_typet("MyType"); | ||
const auto generic_symbol_type = java_generic_symbol_typet( | ||
symbol_type, "LGenericClass<TX;TY;>;", "PrefixClassName"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Given the missing precondition in the constructor, as mentioned above, replace this with "LMyType<TX;TY;>;"
.
} | ||
|
||
GIVEN("Generic type LGenericClass<Tkey;Tvalue;>; and" | ||
" parameters key, value, x") |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How is this example different from the previous one?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It has non-single letter generic parameter names as suggested by @thk123
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I see. Maybe you can combine them into one example though, with one single letter and one non-single letter case.
@svorenova I made the changes, can you check again? |
This function needs to look at the type_variables comment to known which argument correspondsd to the given type.
dfba832
to
a9cc5de
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good, only two minor suggestions to make the examples a bit more realistic. Please also make sure that you squash related commits before merging.
src/java_bytecode/java_types.cpp
Outdated
@@ -854,6 +854,11 @@ java_generic_symbol_typet::java_generic_symbol_typet( | |||
const typet &base_type = java_type_from_string(base_ref, class_name_prefix); | |||
PRECONDITION(is_java_generic_type(base_type)); | |||
const java_generic_typet gen_base_type = to_java_generic_type(base_type); | |||
INVARIANT( | |||
type.get_identifier() == to_symbol_type(gen_base_type.subtype()).get_identifier(), | |||
std::string("identifier of ")+type.pretty()+"\n and identifier of type "+ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please use double quotes here as well instead of std::string
.
src/java_bytecode/java_types.cpp
Outdated
/// For instance `java_generic_symbol_typet(symbol_typet("Map"), | ||
/// "Ljava/util/Map<TK;TV;>;", "java/util/Map")` will generate a symbol type | ||
/// with identifier "Map", and two generic types with identifier | ||
/// "java/util/Map::K" and "java/util/Map::V" respectively. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My previous comment on changing this example is still outstanding: please use java.util.HashMap
as the third argument and the parameter identifiers are then java.util.HashMap::K
and java.util.HashMap::V
. This then correctly corresponds to the case HashMap<K,V> extends Map<K,V>
.
} | ||
} | ||
|
||
GIVEN("Generic type Ljava/util/HashMap<TK;TV;>; and parameters K, V, T") |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sorry for being nit picking here but as I thought about the application of java_generic_symbol_typet
I would suggest to change these examples a bit to reflect why that type even exists. It is to represent the generic base of a class. So you could change the examples to say that for example given HashMap<K,V> extends Map<K,V>
the generic symbol for Map is created correctly - the generic symbol is then created with java_generic_symbol_typet(symbol_typet("java::java.util.Map"), "Ljava/util/Map<TK;TV;>;", "java.util.HashMap")
(exactly as in the documentation for the constructor actually). Similarly for the first example - PrefixClassName<X,value> extends GenericClass<X,value>
and the constructor call stays as it is.
Unit-testing this function revealed some mistakes in the examples given in the documentation.
This also adapt unit tests that would make the invariant fail.
a9cc5de
to
53bc892
Compare
20e7bca Merge pull request diffblue#2179 from cesaro/java-concurrency-support3 25e5820 Java concurrency regression tests bc539b5 Adds support for concurrency in java programs 46849e9 Adding concurrency related methods to CProver.java c817486 Merge pull request diffblue#2171 from thomasspriggs/json_tweaks f3670e3 Expose `begin` and `end` methods of underlying `std::vector` in `json_arrayt`. 402bc56 Clang format updates. 2907ba9 Allow constructon of `json_stringt` from `irep_idt`. ce674b5 Update constructor of `jsont` based on the copy and move idiom. 28117d2 Expose `emplace_back` method of underlying `std::vector` in `json_arrayt`. a589a56 Supply `value_type` typedef in `json_arrayt` for STL algorithm usage. 1d0cd01 Merge pull request diffblue#2175 from diffblue/extract-goto-functiont 76d202a use goto_function.h when only goto_functiont is used b9cd297 split out goto_functiont from goto_functions.h into separate file 784b6dd Merge pull request diffblue#2119 from svorenova/gs_tg1121_regression 1b6a939 Merge pull request diffblue#2169 from sonodtt/patch-1 faaacec Add dashboard webhooks to travis 7b0673e Merge pull request diffblue#2154 from diffblue/jar-file-cleanup d069719 Merge pull request diffblue#1915 from karkhaz/kk-abstract-paths-worklist aac16d5 Merge pull request diffblue#2159 from peterschrammel/clean-up-specc d413dd8 Merge pull request diffblue#2123 from smowton/smowton/java-object-factory-zero-initializer 995a548 Merge pull request diffblue#2164 from tautschnig/cleanup-mp-arith a4d1891 Merge pull request diffblue#2160 from diffblue/fix-java-constructor-pretty-name b9db37d Merge pull request diffblue#2163 from tautschnig/fix-test 6b064b3 pretty name of constructors now uses empty declarator b008bf3 add signature to method pretty names a9bb35c strip package name from base_name of Java class symbols 7711933 Merge pull request diffblue#2162 from tautschnig/fix-format 7d91638 Merge pull request diffblue#2148 from diffblue/remove-fixedbv-option 7e09d5f Fix duplicate output of id in format() 033f4c5 Remove unnecessary (and inconsistent) return statement 90d59d8 Remove unused global constant 29763da Fix misleading comments: the required variant of numeric_cast does not exist a2260bd remove the --fixedbv command-line option 78901ef fix in rounder in fixed-point arithmetic class 8414886 Remove SpecC support 88bbe32 Clean up references to php frontend 3f52c59 Clean up commented include 01685b6 Clean up references to SpecC frontend 916eb1f Unit tests for path exploration strategies 88db26f Merge pull request diffblue#2155 from tautschnig/mode-fixes 2fb3d2f Add missing mode 85aba52 Make new LIFO path exploration the default feef069 Doxygen uses C++ parser for .h files 17951c8 Add path strategy chooser class 685937a Path exploration pushes both successors onto queue 2a86fb4 Bugfix: always print path exploration resume point e823538 Symex paths saved onto abstract data structure bbd4253 signal errors while getting file from JAR using optional 48f1af3 Merge pull request diffblue#2145 from cesaro/concurrency-support-for-clinit 8db6b22 Merge pull request diffblue#2139 from romainbrenguier/bugfix/annotations-as-comments 94bbbba Added new cmd option to jbmc, 'java-threading' 48914be Modifies the instrumented clinit_wrapper function ce9f046 Merge pull request diffblue#2146 from diffblue/extra-float-types 46267b5 Merge pull request diffblue#2153 from diffblue/elaborate-format_expr da940a9 Test for assignement of annotated field 9d94bf7 Make annotations comments in irep_idt 52e9737 new gcc floating-point type identifiers, Fixes: diffblue#2151 c6cbf7c Merge pull request diffblue#2147 from diffblue/fix-tempdir-buffer-overflow 957881c format now prints type expressions and the values of named sub-ireps 9609a52 simplify use of get_temporary_directory 5907f68 fix potential non-zero termination of a string buffer 41d7a45 Merge pull request diffblue#2129 from romainbrenguier/bugfix/generic_type_index 53bc892 Add invariant in java_generic_symbol_type e3f240a Use get_name in generic_type_index 4a6ae9b Add java_types unit tests to Makefile 4c5144d Unit test for generic_type_index 8f0f780 Unit test for java_generic_symbol_type 41b3a6a Move java_generic_symbol_typet definitions to cpp 0afbe0f Unit test java_type_from_string and fix doc b7c9ea1 Test for abstract class with two generic arguments c141611 Fix generic_type_index 8127d4d Merge pull request diffblue#2141 from romainbrenguier/bugfix/goto-convert-mode 4948b70 Merge pull request diffblue#1712 from karkhaz/kk-flush-all e0bc5fd Merge pull request diffblue#2143 from diffblue/missing-algorithm-include fbed57e Add precondition ensuring mode is not empty 2ef91e7 Make mode an argument of goto-convert functions 2b4cd76 missing #include <algorithm> for std::find_if_not 7d11e85 Zero-initialize object factory structs 392c765 cleanup the includes in src/java_bytecode 1050637 fix a comment c57439e missing const for parameter 227e83d Adding regression tests for multi-dimensional arrays b8ffa5e Merge pull request diffblue#2135 from diffblue/solver-cleanout 0dc35fd Merge pull request diffblue#2136 from diffblue/unwind_module_cleanout f6a92cc remove bmc_constraints a2d9822 remove OpenSMT 218dc31 remove support for SMT1 e8aaf09 remove unused includes b0f7476 remove do_unwind_module hook 4d75d3d Merge branch 'develop' of github.com:diffblue/cbmc into develop 60c03b3 whitespace fix 3ea32fe Merge pull request diffblue#2134 from peterschrammel/invalid-symbol-mode b2a58c8 Assign mode to invalid objects e4230c6 Merge pull request diffblue#2130 from romainbrenguier/bugfix/if-expr-mode c6beb68 Merge pull request diffblue#2128 from tautschnig/include-cleanup 973b309 Merge pull request diffblue#2073 from tautschnig/reset-namespace a6a825a Remove unused includes b04122e Move definition of base_type_eqt to .cpp 104bc56 Use pointer_offset_bits instead of locally hacking up what it does anyway 99755fe Move asserts to invariants (and provide suitable includes) 3af3d72 Do not unnecessarily use C string functions 3c697da Add test where tmp_if_expr is introduced 746e337 Set mode of if_exprt introduced in preprocessing 73e0c0f Use C++ streams instead of C-style snprintf d351a5d Use a single global INITIALIZE_FUNCTION macro instead of __CPROVER_initialize 9c03ca3 Use iosfwd instead of ostream where possible 6b8583d Merge pull request diffblue#2100 from tautschnig/string-table-cleanup 75caefa Merge pull request diffblue#2116 from peterschrammel/java-new-pass 6c90b35 Merge pull request diffblue#2052 from romainbrenguier/bugfix/default-axioms2#TG-2138 53dfa0a Merge pull request diffblue#2120 from diffblue/optional_optnr 8f7d9f0 use optional<size_t> instead of -1 in cmdlinet a61d03f Remove java_bytecode deps from Makefiles ce9f1fc Use remove_java_new 10d0042 more files to ignore 95ea29a Merge pull request diffblue#2115 from peterschrammel/language-mode-utils ce11613 Factor out java new removal into separate pass baa15f5 Add Makefile dependency for smt2_solver bacfa27 Merge pull request diffblue#2114 from tautschnig/type-renaming 2bdaafc Add more doxygen to language.h and mode.h 74c2c3d Utility functions to get mode and language b934aaf symex_dynamic::dynamic_object_size* are constants ef83f93 array_size symbols: set mode and avoid redundant settings 8b20ebb Merge pull request diffblue#2112 from diffblue/address_of_byte_extract 66aa851 Merge pull request diffblue#2109 from LAJW/lajw/free-lambda-from-cpplint-oppression 7339638 Merge pull request diffblue#2111 from peterschrammel/bugfix/missing-java-modes 18cab61 Rephrase and justify curly brace alignment exceptions 6670703 Added an extension point for irep ids 38782bd Move enum idt to the single translation unit that actually requires it e657da8 Fix Doxygen syntax f79b453 Check that the string table does not include unused entries 61ca5df Remove unused entries from the string table b2e4ca0 Use existing irep_idts instead of strings 2b819e6 Remove unused symbolt::{to,from}_irep 0b82ee2 allow address_of of byte_extract expressions 7747442 Associate dynamic objects with respective language mode 6438ee7 Bugfix: use proper language registration in unit tests c274c15 Set mode in goto_convert auxiliary symbols 9a896f9 Replace asserts by invariants 78191ee Remove NOLINTs for lambdas. 692c4f3 Remove brace checking from cpplint d344dd9 Update coding standard b59a453 Move MAX_CONCRETE_STRING_SIZE definition to magic 05b924c Deprecate string-max-length option 132a26b Add tests showing the effect on string-max-length 0e8a863 Add test for generics array and strings b83182f Get rid of string_max_length field d726577 Make char_array_of_pointer return a reference 2154047 Get rid of default axioms for strings 1d4f26c Assign 0 to string length for null Java String ff25fe2 Weaken invariant for nil exprt as model of array 56e7b37 Make get_array return nil for long strings 5fde05a Use string-max-length as default max input-length b0c6528 Use boolbvt for getting counter examples 5b3a1a4 Remove unnecessary replace_expr a630bb7 Correct bound in test with long string e4cf694 Bugfix: Java symbol types must have mode ID_java e158bb4 Bugfix: Java array symbols must have mode ID_java d475abc Reset namespace after symbolic execution 1ef0f41 Add --flush option to flush all output git-subtree-dir: cbmc git-subtree-split: 20e7bca
This function needs to look at the type_variables comment to known which
argument corresponds to the given type.
The bug was causing problems in the case of interfaces used with two different types in the generic arguments. The added test is an example of this.