[TG-7815] Fix bug in get_recursively_instantiated_type #4913

NathanJPhillips · 2019-07-15T16:40:49Z

This reduces the amount of code and in so doing fixes the implementation of specialization of generics.

Previously the following invariant was being triggered in non-symmetric mutual generic specialization:

Invariant check failed
File: .../lib/cbmc/jbmc/src/java_bytecode/select_pointer_type.cpp:187 function: get_recursively_instantiated_type
Condition: depth < replacements.size()
Reason: cannot access elements outside stack

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
N/A The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included in a downstream PR.
N/A My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

When there is recursion we ended up duplicating effort and the recursion-handling method is now more simple anyway. Also avoids essentially duplicated code.

smowton

Also please add at least one regression test exposing the bug (or better yet, KNOWNBUG -> CORE an existing test), and there seem to be real unit test failures in CI.

smowton · 2019-07-16T07:51:13Z

jbmc/src/java_bytecode/select_pointer_type.cpp

-  if(!is_java_generic_parameter(type))
-  {
-    return type;
+    auto types_it = generic_parameter_specialization_map.find(parameter_name);


Commit message: note what the bug was and how this fixes it

smowton · 2019-07-16T07:51:46Z

jbmc/src/java_bytecode/select_pointer_type.cpp

-
-  irep_idt current_parameter = parameter_name;
-  for(size_t depth = 0; depth < max_depth; depth++)
+  while(true)


Looks good, but since taking a map by value like this is quite unusual please add comments noting the strategy you're using here and why

The map itself is not taken by value. I don't think we need to document why passing a struct by value is OK.

I'm not sure what you mean by "not taken by value". We do make a copy here, so we can pop from the stacks of particular parameters in the map just for the sake of finding the parameter specialization, but at the call site of this function we need to keep the original full information. I agree that adding a note that points this out is useful (not arguing why it's ok, just to make the reader notice), I missed it myself at first.

smowton · 2019-07-16T07:52:59Z

jbmc/src/java_bytecode/select_pointer_type.cpp

-        return replacement_array_type;
-      }
-    }
+    auto array_element_type =


const auto * for clarity?

smowton · 2019-07-16T07:54:09Z

jbmc/src/java_bytecode/select_pointer_type.cpp

}
+

Don't re-space in the same commit as a substantial change

allredj

Should be fine once the tests are in.

allredj · 2019-07-16T08:57:36Z

jbmc/src/java_bytecode/select_pointer_type.cpp

-
-  irep_idt current_parameter = parameter_name;
-  for(size_t depth = 0; depth < max_depth; depth++)
+  while(true)


The map itself is not taken by value. I don't think we need to document why passing a struct by value is OK.

allredj · 2019-07-16T09:03:42Z

jbmc/src/java_bytecode/java_types.h

 /// Checks whether the type is a java generic parameter/variable, e.g., `T` in
 /// `List<T>`.
 /// \param type: the type to check
 /// \return true if type is a generic Java parameter type
 inline bool is_java_generic_parameter(const typet &type)
 {
-  return is_reference(type) && is_java_generic_parameter_tag(type.subtype());
+  return can_cast_type<java_generic_parametert>(type);


Should probably be in a separate commit. It does not correspond to the commit description. There are several things being changed here, and it makes it difficult to check that this commit does not introduce a behavioural change.

majakusber

Needs some cleanup but I love it 🙂

majakusber · 2019-07-16T09:03:47Z

jbmc/src/java_bytecode/select_pointer_type.h

+
+template <typename ostream>
+ostream &
+operator<<(ostream &stm, const print_generic_parameter_specialization_map &map)


👌 This is useful

majakusber · 2019-07-16T09:46:17Z

jbmc/src/java_bytecode/select_pointer_type.cpp

-
-  irep_idt current_parameter = parameter_name;
-  for(size_t depth = 0; depth < max_depth; depth++)
+  while(true)


I'm not sure what you mean by "not taken by value". We do make a copy here, so we can pop from the stacks of particular parameters in the map just for the sake of finding the parameter specialization, but at the call site of this function we need to keep the original full information. I agree that adding a note that points this out is useful (not arguing why it's ok, just to make the reader notice), I missed it myself at first.

majakusber · 2019-07-16T10:04:37Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+/// \param generic_parameter_specialization_map: Map of type names to
+///   specialization stack
+/// \return The first instantiated type for the generic type or nothing if no
+///   such instantiation exists.


This should be updated slightly - it sounds l like it's only handling the recursion case (because it's just moved from the function that was breaking recursion). Also, move the documentation to the header.

majakusber · 2019-07-16T10:18:46Z

jbmc/src/java_bytecode/select_pointer_type.cpp

-    // previous assignments
-    if(visited_nodes.find(parameter_name) != visited_nodes.end())
+    generic_parameter_specialization_mapt spec_map_copy =
+      generic_parameter_specialization_map;


💡 You're making a copy of the map over and over again, changing a single element in it in each call. I don't have any good idea how to make this less costly though.. not so nice ideas being keeping two functions, make the code uglier at the call site, or add extra arguments to the function (depth of each stack to look at). Can you think of a better way?

NathanJPhillips · 2019-07-19T15:28:01Z

This solution was inadequate. Replacing with a new solution.

NathanJPhillips added 5 commits July 15, 2019 13:16

Added ability to output generic_parameter_specialization_mapt

4abbd7a

Fixed implementation of get_recursively_instantiated_type

cf6d6fb

Use type_try_dynamic_cast

e4b7363

Remove simplistic method that assumes no recursion

8125a9f

When there is recursion we ended up duplicating effort and the recursion-handling method is now more simple anyway. Also avoids essentially duplicated code.

Avoid repeating check that will be done in called function

ec69b1b

NathanJPhillips requested review from majakusber and antlechner July 15, 2019 16:40

NathanJPhillips requested review from cesaro, cristina-david, peterschrammel, pkesseli, smowton and thk123 as code owners July 15, 2019 16:40

NathanJPhillips self-assigned this Jul 15, 2019

smowton reviewed Jul 16, 2019

View reviewed changes

allredj changed the title ~~Fix bug in get_recursively_instantiated_type~~ [TG-7815] Fix bug in get_recursively_instantiated_type Jul 16, 2019

allredj reviewed Jul 16, 2019

View reviewed changes

majakusber reviewed Jul 16, 2019

View reviewed changes

NathanJPhillips closed this Jul 19, 2019

NathanJPhillips deleted the bugfix/get_recursively_instantiated_type branch July 19, 2019 15:28

NathanJPhillips mentioned this pull request Jul 22, 2019

Fix generic_parameter_specialization_map in the presence of non-symmetric generic recursion [TG-7815] #4929

Merged

6 tasks

[TG-7815] Fix bug in get_recursively_instantiated_type #4913

[TG-7815] Fix bug in get_recursively_instantiated_type #4913

Uh oh!

Conversation

NathanJPhillips commented Jul 15, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

majakusber left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

NathanJPhillips commented Jul 19, 2019

Uh oh!

Uh oh!

NathanJPhillips commented Jul 15, 2019 •

edited

Loading