Skip to content

[TG-1301] Parsing nested generics #1575

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

Merged
merged 2 commits into from
Nov 14, 2017

Conversation

majakusber
Copy link

The first commit contains the implementation of this, the summary of changes is in the commit message. @thk123 and @mgudemann can you please review?

@majakusber majakusber force-pushed the nested_generics_tg1301 branch 4 times, most recently from dd59c53 to 8279c1a Compare November 9, 2017 15:26
@smowton
Copy link
Contributor

smowton commented Nov 9, 2017

Could you (a) avoid restyling lines that are otherwise untouched, and (b) do the mass-renaming of parameter -> type variable in a separate commit from the actual substantial changes here? That will make it much easier to review as (a) will reduce the line count a lot and (b) will mean 90% of lines can be skimmed as they're just a find/replace, whilst the remaining 10% are the ones that really need reading carefully.

@majakusber
Copy link
Author

@smowton Will do, thanks.

Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In future it would be helpful to ensure unrelated formatting changes are excluded or in a separate commit. It would also be useful for renamings to be done in isolated commits.

Other than that - code and tests look good. If you've not already done so - could you create a Test Gen pointer bump to verify this doesn't break any TG tests

if(is_java_generic_parameter(type))
{
return to_java_generic_parameter(type);
}
else if(is_java_generic_type(type))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this needed?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point. The whole if block is actually not needed here, type is of type typet and we just need to make sure it is a reference_typet but we don't need to cast it to any of its subtypes (it will be cast back to reference when returned). Will make the change.

@@ -69,21 +69,6 @@ SCENARIO(
}
}

THEN("It has field f3 pointing to Generic")
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Removed as duplicate?

@majakusber majakusber force-pushed the nested_generics_tg1301 branch from 8279c1a to 5667e86 Compare November 9, 2017 16:56
@smowton
Copy link
Contributor

smowton commented Nov 9, 2017

Changes look fine now. I'd carefully consider the right terminology before making a commit that changes it everywhere, though. In my understanding a function f(x, y, z) called with f(1, z, w + v) has formal parameters x, y, z instantiated by actual parameters 1, z, w + v. Thus in the context List<T, Integer> I would be tempted to say T is a formal type parameter or type variable, while Integer is an actual type parameter or simply a concrete type. However others may disagree -- I suggest quizzing wiser language analysis people such as @peterschrammel or @forejtv to check you're using a naming scheme that will agree with a new developer who has read "industry standard" terminology before.

@tautschnig
Copy link
Collaborator

I'd agree with what @smowton just said, though would add that elsewhere in the code base the terminology is "parameter" to refer to formal parameters, and "argument" to refer to actual parameters.

Copy link
Contributor

@mgudemann mgudemann left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, modulo small comment and an eventual test-gen bump to see how this works there

/// parameters of a function or the generic arguments contained within angle
/// brackets.
/// parameters of a function or the generic type variables contained within
/// angle brackets.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

might make sense to specify that it will also parse method signatures which are wrapped in (, ) brackets

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The beginning of the sentence says 'This is used for parsing the parameters of a function or...', would it be enough to change it to 'This is used for parsing the parameters of a function contained within parentheses or..' or did you mean something else?

@majakusber majakusber force-pushed the nested_generics_tg1301 branch 2 times, most recently from 90d5dca to 5ebbffd Compare November 10, 2017 09:52
@majakusber
Copy link
Author

majakusber commented Nov 10, 2017

Thanks for the comments everyone. About the mixed commit, sorry about that, I understand it's not easy to locate the crucial parts. I tried to brake it into two commits, renaming and then functionality, after Chris's comment. However, it's quite tricky as renaming for consistency cannot really be done without changing the semantics of the java_generic_parametert class (see below for explanation).

For the choice of terminology, I was keeping two things in mind: minimal changes to existing terminology we use in the code base, and the terminology from Java spec:
https://docs.oracle.com/javase/tutorial/java/generics/types.html
In Java spec, type variables and type parameters refer to the same thing - uninstantiated types such as T, although type parameter is used more often than type variable. Once invoked/instantiated, they are called type arguments. In our code base, we used type variables to refer to anything appearing between the angle brackets, see generic_type_variablest in java_generic_typet. The type of these was a vector of java_generic_parametert (uninstantiated), which had a subclass java_generic_inst_parametert (instantiated). While this class hierarchy was quite ok for terminology, it prevented the instantiated types to be generic types (exactly what we need to parse nested generics). So the special class to hold instantiated type variables was removed, the type of the generic_type_variablest in java_generic_typet changed to reference_typet (allows concrete types such as Integer, generic types and type parameters). This allowed to keep the terminology in the code base almost the same and in accordance with Java spec: type variables for mixed types, parameters for uninstantiated type variables. Much of the renaming was only to make sure that anything that can be both uninstantiated and instantiated type is called type variable rather than parameter.

Note that no change was needed for classes, java_generic_class_typet, since in a declaration of a generic class only (uninstantiated) type parameters appear in the angle brackets.

Also, note that the terminology for generics is separate from terminology for functions - in functions, parameters refer to inputs.

I hope this makes it a bit more clear, I'm happy to make changes to the terminology if something else would make more sense.

@majakusber majakusber force-pushed the nested_generics_tg1301 branch from 5ebbffd to 8b5b156 Compare November 10, 2017 10:53
@peterschrammel
Copy link
Member

@svorenova, please rebase.

@majakusber majakusber force-pushed the nested_generics_tg1301 branch 3 times, most recently from f771813 to 24bf90a Compare November 13, 2017 11:14
@majakusber
Copy link
Author

As requested by Chris in our offline discussion, the terminology has been slightly adjusted as follows:

  • type variables and type parameters are synonyms, referring to uninstantiated types, e.g., T in generic class declaration MyClass<T>,
  • type arguments refer to instantiates types, that means to anything appearing within the angle brackets for objects of generic types, e.g., if the class MyClass<T> has a field of type HashMap<T,Integer>, then both T and Integer are arguments (T must already be instantiated for the class).
    This is now fully in accordance with Java spec.

@smowton @peterschrammel Can you please take a look again?

svorenova added 2 commits November 13, 2017 14:30
Includes:

- adding the functionality itself - as part of this, the meaning of the
java_generic_parametert class changed - before it held both
uninstantiated types (type variables/parameters) and instantiated types
(type arguments), now it only holds uninstantiated types;

- removing the java_generic_inst_parameter class and flag to allow
instantiated types to be both references and generic types, the class
hierarchy changed as follows:
BEFORE:
reference_typet
   -> java_generic_parametert
       -> java_generic_inst_parametert
   -> java_generic_typet
NOW:
reference_typet
   -> java_generic_parametert
   -> java_generic_typet

- slight changes in terminology for consistency (use 'type variables'
and 'type parameters' for uninstantiated types, i.e., types specified in
generic class/method declaration, 'type arguments' for instantiated
types);

- updating utility functions for unit tests accordingly.
@majakusber majakusber force-pushed the nested_generics_tg1301 branch from 24bf90a to 21b4e7e Compare November 13, 2017 14:31
@chrisr-diffblue chrisr-diffblue merged commit af31813 into diffblue:develop Nov 14, 2017
@majakusber majakusber deleted the nested_generics_tg1301 branch November 14, 2017 16:45
smowton added a commit to smowton/cbmc that referenced this pull request May 9, 2018
e8b3cb9 Merge remote-tracking branch 'upstream/develop' into smowton/merge/develop_20171116
dc4a293 Merge pull request diffblue#1594 from reuk/reuk/cmake-fixup
48fc3d4 Merge pull request diffblue#1592 from antlechner/antonia/char-escape
538eef6 Merge pull request diffblue#1577 from smowton/smowton/fix/dependence_graph_inconsistency
d3d632d Use multi-argument form of FILE command
81e56cc Tidy up CMakeLists
f7141c0 Merge pull request diffblue#1582 from romainbrenguier/refactor/numerical-cast
8ed1023 Use UTF-16 conversion function in expr2java
a53f5bf Split UTF-16 conversion code into two cases
e0ad069 Merge pull request diffblue#1558 from NathanJPhillips/feature/complete-journalling_symbol_table
69d1a52 Added usages of base class symbol table
3e42a8d Add comment on has_symbol
a2b45e3 Update to journalling symbol table
7aa80ad Remove lookup_impl - it won't work for recording symbol table and adds complexity
cdbac8c Sort output of symbol_tablet::show
2ef1c94 Fix bug where move from const symbol collections
8035397 Style improvements
6dae8e8 Merge pull request diffblue#1515 from smowton/smowton/admin/codeowners
5297646 another ranged for
3d66779 Merge branch 'develop' of github.com.:diffblue/cbmc into develop
4b5467c another ranged for
f5dbfd4 Merge pull request diffblue#1589 from reuk/reuk/fewer-exceptions
8e99272 use ranged for
95cf5c3 Add directories without code owners and adapt code owners
8da6a81 Replace try-catch with nullptr checks
9ff48e0 Add numeric_cast template for numeric conversion
af31813 Merge pull request diffblue#1575 from svorenova/nested_generics_tg1301
21b4e7e Extend unit tests to test for nested generics
cf47dcb Extending parsing of generics to parse nested generic types
1aefb09 Merge pull request diffblue#1547 from smowton/smowton/feature/remove_virtual_functions_single_call
2b4ed77 Merge pull request diffblue#1579 from smowton/smowton/fix/cmdline_destructor
7305506 Merge pull request diffblue#1580 from smowton/smowton/fix/cast_materialised_temporary
87b9de1 Remove pointless typecasts
a59dea6 Add unit test checking dependence graph consistency
80e66ba Remove virtual functions: expose single-call entry-point
ffe02e4 Remove useless cmdlinet::clear() call
ae34e9b Merge pull request diffblue#1578 from thk123/bugfix/specalised-classes
779d0aa Merge pull request diffblue#1574 from diffblue/taint-memcpy-develop
28a4846 Merge pull request diffblue#1568 from smowton/smowton/fix/java_div_by_zero
ffd089f Constructed class to mimic the original class in all but name of symbol
7f53f02 Merge pull request diffblue#1569 from thk123/bugfix/TG-1403/generic-field-arrays
1abc75e Dependence graph: ensure grapht representation is consistent with domain
e03b0cb Abstract interpreter: add finalize hook
fa7d62a Makefile for goto-analyzer-taint-ansi-c
758ebb3 transfer taint on memcpy and memmove
d0a844b Assert denominator non-zero when Java runtime exceptions are disabled
e5744b2 Reorder code owner definition according to change risk
0f98cb4 Removed redundant if statement
ffa104c Enforce condition that generic references must refer to generic classes
6e06fbd Extending tests to deal with specialising with arrays when array fields
a01a0f2 Extend the specialisation code to handle generic fields
1ccbf83 Correctly handle generic classes that have a array field
f60d8c8 Unit utility for symbol types
21a33fa Renaming to_java_generic_class_type to remove spurious s
94ffce3 Merge pull request diffblue#1567 from mgudemann/mgudemann/feature/support_arrays_in_generic_parameters
5be97db Create new and adapt existing unit tests for generic array param
ef6b4af Post-fix arrays as generic types with their element type
4db6fc6 Merge pull request diffblue#1553 from mgudemann/bugfix/initialize_pointer_width_in_unit_test
b17ed58 Merge pull request diffblue#1555 from thk123/feature/remove-redundant-specalisation-code
9b34cdb Merge pull request diffblue#1564 from owen-jones-diffblue/bugfix/object-numbering-references
52d4326 Merge pull request diffblue#731 from tautschnig/more-rewriting
51133db Remove test checking don't specalise unspecalised generic types
bf10b1b Manually call specalisation code
bba9f76 Remove redundant regression test
3047678 Removed old method of specalising generics
2db8c45 Merge pull request diffblue#982 from tautschnig/pointer-handling
fb532e8 Generalize ID_malloc to ID_allocate with optional zero-init
3c47ccb Use invariant annotations instead of asserts
ebd5343 More unwinding should not yield additional assertion failures
cc659c9 Use a known constant offset when dereferencing
c507ccf Update all constant offsets, not just 0
0361c2a Merge pull request diffblue#1534 from svorenova/unit-test-cleanup
f653f85 Merge pull request diffblue#263 from diffblue/owen/fix-memory-bug
ede0e8c Fix bug that can cause segfault
51cbfc9 Deleting a utility function for generics
03438bb Disabling part of unit test due to a bug
e3019f2 Extending test for derived generics
f5ec45a Adding JIRA tickets cont.
1fa8e2f Adding unit test for generic fields
398c88a Applying new utility functions for generics
cce7814 Refactoring unit test utility functions to make them easier to use
c1e1ba2 Applying new function for accessing elements of arrays
e908f0c Updating utility functions to check generic/non-generic java classes
d9d9ea1 Cleaning includes, unifying scenario names, adding JIRA references
2883bb1 Extending test for generic arrays
de97e23 Adding unit test for nested generics
c9a3716 Adding unit test for functions with generics
9db9947 Extending test for generic class
89b99ce Extending test for generic functions
3e6cf35 Extending test for signature/descriptor mismatch
80be2fd Extending and cleaning test for generic class with generic inner classes
2e2e34b Renaming unit test for generic inner classes to bounded generic inner classes
c5b06e6 Breaking the old parse_generic_class into two unit tests
d3ff11c Adding a utility for checking java generic class
707ebf6 Cleaning existing unit tests
af3efea Renaming java files
14c00dc Simplify all expressions generated by flatten_byte_operators
71e9642 Extensions to simplify_byte_extract
81943f2 Split ID_and/ID_or vs ID_xor simplification
77236cc Avoid nesting of ID_with/byte_update by rewriting byte_extract to use the root object
ddd3d03 Extended simplify for byte_update, typing
7064483 simplify_typecast: simplify more pointer arithmetic
2b18e0c Merge pull request diffblue#1562 from NathanJPhillips/feature/extend-main_function_result
599a2f9 Merge pull request diffblue#264 from diffblue/smowton/fix/slice24_include
de905e7 slice24 test: switch from malloc.h to stdlib.h
89a1132 Merge pull request diffblue#1559 from NathanJPhillips/bugfix/variable-scope
0aeb459 Tidied up get_main_symbol
af2d3dd Merge pull request diffblue#1560 from NathanJPhillips/bugfix/catch-by-const-ref
c8efb6f Fix bug that can cause segfault
b7cc0ae Merge pull request diffblue#1561 from NathanJPhillips/bugfix/erroneous-replacement
7d66469 Typo in reachable
7de4858 Added copyright notice to fix linting error
476270b catch by const ref instead of by value or non-const ref
2f32aee Fixed scope of moved symbol
5057c57 Merge pull request diffblue#1557 from janmroczkowski/janmroczkowski/further-improvements-to-unified_difft
5e067bf Merge pull request diffblue#1481 from andreast271/do-c++-regression
c9b6c42 Merge pull request diffblue#1513 from romainbrenguier/feature/input-string-printable
c4486f1 Merge pull request diffblue#1552 from thk123/feature/goto-functions-utilities
2648cbb Make unified_difft::lcss return by value
cd1258a Merge pull request diffblue#1425 from romainbrenguier/feature/java_new_array_data
6e3a0b0 Make more member function static
9efb65c Merge pull request diffblue#1556 from diffblue/revert-1554-janmroczkowski/more-static-member-functions-in-unified_difft
1c96ae5 Revert "Make more member function static in unified_difft"
9cb4569 Amend doxygen comments
4550676 Added missing utilities to the Makefile
7938bac Correcting linting errors
25d765b Use a for loop rather than chained algorithms
e67d229 Renamed find declaration method
fa14b47 Renamed utility file to require_goto_statements
a657ec1 Moved functions into a namespace and documented them
b96199f Moved and simplified the code for finding sub statements
b9914a8 Add some java testing utilities.
2c175bd Update load_java_class to construct the entry point function
3453a89 Merge pull request diffblue#1554 from janmroczkowski/janmroczkowski/more-static-member-functions-in-unified_difft
feaa85f Merge pull request diffblue#1455 from romainbrenguier/doc/string-solver-documentation
c5ab866 Merge pull request diffblue#1430 from romainbrenguier/refactor/gather_indices
fac9dea Rename "#lva_mode" to "lvsa_mode"
72c8533 Make two irep IDs
55b6ac5 Merge pull request diffblue#1502 from tautschnig/merge-failed-tests-printer
dfa2ed2 Make more member function static
d378980 Style: Disabling clang-format in get
f5991ee Refactor universal_only_in_index to use expression iterators
9d1aa99 Correct constraints added for char_set
e125e8a Refactor gather_indices to use for_each instead of visitor
4b0e2d4 Create goto-gcc symlink in cmake builds and enable goto-gcc tests
7736672 Style: use NOLINTNEXTLINE to avoid cpplint errors on long links
6016bef Improve readability of code imported from failed-tests-printer.pl
dd6e431 test.pl: Use native perl instead of "cat" to print log file
3321735 Move implementation of failed-tests-printer.pl into test.pl
ba16006 Do not use shell built-ins
96e169a Use single quotes for Windows compatibility
d2c3752 Remove string_printable option from the solver
b0de0e3 Test for string printable option on input strings
4b36fc6 Merge pull request diffblue#1533 from mgudemann/fix/support_class_bounds_generics
35096b8 Initialize architecture in `instantiate_not_contains` unit test
b25630a Merge pull request diffblue#1550 from chrisr-diffblue/cleanup/java-generics-test-helpers
542a26d Stop adding printable constraints on all strings
e65e340 Use command line option for string-printable param
8e92362 Propagate string-printable option in object_factory
ae5f32e Add a printable option to string initialization
514e6a1 Add function to call constrain_character primitive
1d92c48 Add string primitive to constrain characters
cb01526 Minor refactoring in add_default_axioms
e1280cc Add utility function add_constraint_on_characters
6b88eb8 Add unit test for class / interface bound
2ed059a Support interface and class bound parsing in generics
ccdd483 Merge pull request diffblue#1545 from chrisr-diffblue/TG-1158/unit-test-for-specialising-with-array-types
73808aa Merge pull request diffblue#1544 from smowton/smowton/feature/value_set_eq_operator
0507355 Refactored unit test helpers to be more general and extend their use-cases
93ebb84 Merge commit '356aed461b387a8ae815a9901a16d26f32f102be' into develop
db758fb Add some unit test helper functions, useful for Java generics unit tests
98de899 Add a unit test for specialising Java generic types with array types
b07fcdd Documentation improvements and readme for strings
1fa64a9 Avoid using is_valid_java_array in builin_functions
0dafac2 Add unit test for goto_trace_output in Makefile
435958f Unit test for goto_trace::output
5a0343f Doc: Summary for count_type_leaves
fc363b3 Typo in goto_trace output
42c079d Use existing function for checking object is array
465e5dc Style: improve documentation in interpreter evaluate
fe2efa7 Style: Replace assert by appropriate macros
e36d7d8 Check if object is nil before writing trace
6b519ad Add identifier and rename statement to java_new_array_data
d4f1b29 Add eq and neq operators to value_sett and related types
b03ec16 Merge pull request diffblue#239 from diffblue/bugfix/value_sets_fi_and_reaching_defs_retrievals_of_dynamic_objects
db79106 Added explanatory comment for the introduced condition.
dfc6a20 Fixing C++ code-style issues.
b0742cf Disable cbmc-cpp tests in appveyor, which runs regression on windows. All cbmc-cpp tests #include <assert.h> and cbmc cannot yet parse Microsoft C++ headers.
d55a8da Add tests to cmake regression: cbmc-cover, cbmc-cpp, goto-analyzer-taint
3a4e48c Run cbmc c++ regression as part of default regression test Set is_parameter for c++ function parameter symbol
7989831 Added regression test for the fixed bug.
00b4af2 Bugfix: Explicit retrievals of DOs from value_set amd reaching_defs.

git-subtree-dir: cbmc
git-subtree-split: e8b3cb9
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants