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

NathanJPhillips · 2019-07-19T15:34:25Z

This is a replacement for the closed PR #4913. It adopts a different approach as that approach was shown to be lacking.

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.
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, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
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.

smowton · 2019-07-22T16:26:39Z

jbmc/src/java_bytecode/select_pointer_type.cpp

-    }
+    const auto *array_element_type =
+      type_try_dynamic_cast<pointer_typet>(java_array_element_type(*subtype));
+    if(array_element_type == nullptr)


This commit ("Use type_try_dynamic_cast") does more than its message says (it also switches from if(x) y to if(!x) return; y; style)

smowton · 2019-07-22T16:29:33Z

jbmc/src/java_bytecode/Makefile

@@ -5,6 +5,7 @@ SRC = assignments_from_json.cpp \
      ci_lazy_methods_needed.cpp \
      convert_java_nondet.cpp \
      expr2java.cpp \
+      generic_parameter_specialization_map.cpp \


Commit message for "Change data storage for generic_parameter_specialization_mapt" has got a bit out of hand -- the "Added ability to output..." bit probably doesn't need to be there if we're adding it at the same time as the map itself, and similarly "Add test..."

smowton · 2019-07-22T16:33:08Z

jbmc/src/java_bytecode/generic_parameter_specialization_map.h

+    map.map.container_to_specializations.size());
+  for(const auto &elt : map.map.param_to_container)
+  {
+    std::vector<irep_idt> &params = container_to_params[elt.second.first];


Using structs instead of pair would make it easier to understand what you're referring to here

smowton · 2019-07-22T16:34:46Z

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp

@@ -151,17 +123,18 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(
  {
    return;
  }
+


Spacing fixups should be in their own commit

smowton · 2019-07-22T16:36:39Z

jbmc/src/java_bytecode/select_pointer_type.cpp

 {
  auto parameter = type_try_dynamic_cast<java_generic_parametert>(pointer_type);
  if(parameter != nullptr)
  {
-    const irep_idt &parameter_name = parameter->get_name();
+    irep_idt parameter_name = parameter->get_name();


No need for this to change? const irep_idt & is pretty widely used for a const irept's data, this probably isn't the place to fight that battle

I assign to it at the bottom of the loop.

smowton · 2019-07-22T16:43:41Z

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h

@@ -23,12 +23,10 @@ class generic_parameter_specialization_map_keyst
 public:
  /// Initialize a generic-parameter-specialization-map entry owner operating
  /// on a given map. Initially it does not own any map entry.
-  /// \param _generic_parameter_specialization_map: map to operate on.
+  /// \param generic_parameter_specialization_map: map to operate on.


Probably split commit "Code cleanup", e.g. "factor out get_final_name_component", one commit per variable rename, the stuff with new_class_type, the re-spacing are all pretty independent changes.

smowton · 2019-07-22T16:44:12Z

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -1200,6 +1200,17 @@ void mark_java_implicitly_generic_class_type(
    java_implicitly_generic_class_typet new_class_type(
      class_type, implicit_generic_type_parameters);

+    // Prepend existing parameters so choose those above any inherited


This commit should include a test

codecov-io · 2019-07-24T18:34:08Z

Codecov Report

Merging #4929 into develop will increase coverage by 0.01%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #4929      +/-   ##
===========================================
+ Coverage    69.29%   69.31%   +0.01%     
===========================================
  Files         1306     1308       +2     
  Lines       108263   108314      +51     
===========================================
+ Hits         75023    75074      +51     
  Misses       33240    33240

Impacted Files	Coverage Δ
jbmc/src/java_bytecode/select_pointer_type.h	`100% <ø> (ø)`	⬆️
src/util/simplify_expr_int.cpp	`80.49% <ø> (ø)`	⬆️
..._bytecode/generic_parameter_specialization_map.cpp	`100% <100%> (ø)`
jbmc/unit/java-testing-utils/require_type.cpp	`89.93% <100%> (+0.27%)`	⬆️
...code/generic_parameter_specialization_map_keys.cpp	`100% <100%> (ø)`	⬆️
...enerics/parse_generic_class_with_inner_classes.cpp	`100% <100%> (ø)`	⬆️
.../src/java_bytecode/java_bytecode_convert_class.cpp	`94.73% <100%> (+0.15%)`	⬆️
jbmc/src/java_bytecode/select_pointer_type.cpp	`100% <100%> (ø)`	⬆️
src/util/pointer_offset_size.cpp	`94.53% <100%> (+0.01%)`	⬆️
jbmc/src/java_bytecode/java_types.h	`100% <100%> (ø)`	⬆️
... and 8 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 9643ec2...186adb8. Read the comment docs.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 833e1b7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120497981
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: fcda9ce).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120498877
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

smowton · 2019-07-25T09:22:38Z

jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp

+        param_it->second.container_index == container_index,
+        "Not all type parameters assigned to same container");
+      INVARIANT(
+        param_it->second.param_index == param_index++,


Eeep! Let's not have INVARIANT conditions with side-effects, there are some compilation settings where the first arg is discarded

smowton · 2019-07-25T09:24:00Z

jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp

+    ", ",
+    [](const java_generic_parametert &param) { return param.get_name(); });
+  msg << ">";
+  std::string msg_str = msg.str();


Debugging code accidentally left in?

smowton · 2019-07-25T09:31:11Z

jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp

@@ -187,7 +187,9 @@ SCENARIO(

    const class_typet &derived_class_type =
      require_type::require_complete_java_implicitly_generic_class(
-        derived_symbol.type, {"java::ContainsInnerClassGeneric::T"});
+        derived_symbol.type,


Double-check: do any of these tests exercise triple-nesting?

public class A<T> { class B { class C { T field; } } }

That sort of thing?

The other test in that commit does: aec9e89#diff-157ff943932394172d454093024a926cR120

smowton · 2019-07-25T09:33:37Z

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

+    // Prepend existing parameters so choose those above any inherited
+    if(is_java_generic_class_type(class_type))
+    {
+      const java_generic_class_typet::generic_typest &class_type_params =


Commit message for "Make explicit type parameters shadow implicit ones with the same names" -- can you include a brief example of what you mean by precedence here? Are we talking class A<T> { class B<T> { T field // which T is that? } }?

smowton · 2019-07-25T09:35:34Z

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

-      replacement_parameter_full_name);
-  }
+  // A replacement parameter was found, update the identifier
+  const std::string &replacement_parameter_full_name =


Message: Sp congnative -> cognitive

smowton · 2019-07-25T09:37:07Z

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

    {
      find_and_replace_parameters(
        base.type(), implicit_generic_type_parameters);
    }
+
+    class_symbol.type = new_class_type;


! This which was in the Code Cleanup commit suddenly looks like a bugfix -- the results of find_and_replace_parameters would previously have been wrongly discarded, right? Can we test the fix?

My assumption was that the thing we were changing was a reference to the same and this was just clarifying things. I'll check.

It was. I've updated the commit message to make this clear.

smowton

Brilliant, thanks for putting so much effort into this one!

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: f5f62cf).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120739813
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

NathanJPhillips · 2019-07-25T17:08:22Z

Passing CI for Diffblue bump here: https://github.com/diffblue/test-gen/runs/177289127

romainbrenguier · 2019-07-29T07:16:00Z

jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp

+      const auto result = param_to_container.emplace(
+        parameter.get_name(), container_paramt{container_index, param_index++});
+      INVARIANT(
+        result.second, "Some but not all type parameters already mapped");


I'm not sure I understand the invariant message; there is no verb. 🐂

romainbrenguier · 2019-07-29T07:18:12Z

jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp

+      const auto param_it = param_to_container.find(parameter.get_name());
+      INVARIANT(
+        param_it != param_to_container.end(),
+        "Some but not all type parameters already mapped");


romainbrenguier · 2019-07-29T07:18:21Z

jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp

+        "Some but not all type parameters already mapped");
+      INVARIANT(
+        param_it->second.container_index == container_index,
+        "Not all type parameters assigned to same container");


romainbrenguier · 2019-07-29T07:20:53Z

jbmc/src/java_bytecode/generic_parameter_specialization_map.h

+
+class generic_parameter_specialization_mapt
+{
+private:


⛏️ the public section usually appears before the private one in cbmc

romainbrenguier · 2019-07-29T07:22:34Z

jbmc/src/java_bytecode/generic_parameter_specialization_map.h

+#include "expr2java.h"
+#include "java_types.h"
+
+class generic_parameter_specialization_mapt


This needs some documentation

romainbrenguier · 2019-07-29T07:23:49Z

jbmc/src/java_bytecode/generic_parameter_specialization_map.h

+
+template <typename ostream>
+ostream &operator<<(
+  ostream &stm,


❓ Why does ostream need to be a template parameter instead of being just std::ostream?

It could be restricted to std::ostream but it doesn't need to be. I've added comment to that effect.

thomasspriggs

Looks like this fixes some stuff and I can't see any problems. Therefore this has my approval.

thomasspriggs · 2019-07-26T10:33:17Z

jbmc/src/java_bytecode/generic_parameter_specialization_map.h

+};
+
+template <typename ostream>
+ostream &operator<<(


❔ Should ostream end in a t like ostreamt if it is a type?

thomasspriggs · 2019-07-30T10:58:02Z

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -1142,8 +1142,9 @@ void mark_java_implicitly_generic_class_type(
 {
  const std::string qualified_class_name = "java::" + id2string(class_name);
  PRECONDITION(symbol_table.has_symbol(qualified_class_name));
+  // This will have its type changed


If you move the call to get_writeable_ref into your new class_symbol.type = ... line at the bottom, then this comment will no longer be necessary.

Then we would have two lookups though...

Add space between pre-checks and action Remove space between abbreviations and their usage

Previously the code relied on the fact that class_type is a reference to class_symbol.type and so after a new type got copied assigned into class_symbol.type, class_type became a reference to the new value.

This will save time hunting for the cause of problems when unit tests don't initialise the config.

This will produce better error messages when tests fail.

… block scope

This fixes the problem where we tried to unwind stacks in step that are not related, e.g. when a third generic class refers to two mutually recursive generic classes Instead stacks are created per scope (generic context) and unwound individually Also fixes problem where self-recursion isn't handled properly Add test that would have triggered invariant in get_recursively_instantiated_type

Previously they duplicated the names for the type parameters of the outer classes

Fixes problem where outer class type parameters take precedence over inner class ones Previously field would be given the type of the argument assigned to A::T, not B::T. class A<T> { class B<T> { T field; } }?

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 186adb8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121391281
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

NathanJPhillips requested a review from smowton July 19, 2019 15:34

NathanJPhillips requested review from cesaro, cristina-david, kroening, peterschrammel, pkesseli, tautschnig and thk123 as code owners July 19, 2019 15:34

NathanJPhillips force-pushed the bugfix/generic_parameter_specialization_map branch 3 times, most recently from d1c2855 to 7c01b9a Compare July 19, 2019 17:49

NathanJPhillips changed the title ~~Fix generic_parameter_specialization_map in the presence of non-symmetric generic recursion~~ Fix generic_parameter_specialization_map in the presence of non-symmetric generic recursion [TG-7815] Jul 22, 2019

NathanJPhillips added the bugfix label Jul 22, 2019

smowton reviewed Jul 22, 2019

View reviewed changes

NathanJPhillips force-pushed the bugfix/generic_parameter_specialization_map branch 2 times, most recently from 833e1b7 to fcda9ce Compare July 24, 2019 17:40

allredj reviewed Jul 24, 2019

View reviewed changes

smowton reviewed Jul 25, 2019

View reviewed changes

NathanJPhillips force-pushed the bugfix/generic_parameter_specialization_map branch from fcda9ce to 377bcc1 Compare July 25, 2019 14:57

smowton approved these changes Jul 25, 2019

View reviewed changes

NathanJPhillips force-pushed the bugfix/generic_parameter_specialization_map branch from 377bcc1 to f5f62cf Compare July 25, 2019 15:53

allredj reviewed Jul 25, 2019

View reviewed changes

thomasspriggs self-assigned this Jul 26, 2019

romainbrenguier reviewed Jul 29, 2019

View reviewed changes

thomasspriggs approved these changes Jul 30, 2019

View reviewed changes

NathanJPhillips added 2 commits July 31, 2019 10:34

Indent TODO continuation lines

b005f02

Remove prefix underscore

fed9fd8

NathanJPhillips added 17 commits July 31, 2019 10:34

Remove const modifier that doesn't do anything

bbf403e

Remove duplicated brackets

a483c86

Spacing

7aa6d23

Add space between pre-checks and action Remove space between abbreviations and their usage

Fix indentation

871994e

Use std::next to allow variable that isn't changed to be const

541e667

Use faster character version of rfind

1981bdd

Rename replacement_parameter_it

fabd863

Use == instead of compare == 0

db37e0f

Extract get_final_name_component/get_without_final_name_component

2939616

Update class type before assigning to class_symbol.type

b0319b8

Previously the code relied on the fact that class_type is a reference to class_symbol.type and so after a new type got copied assigned into class_symbol.type, class_type became a reference to the new value.

Validate config is initialised when a member_offset_expr is constructed

a1e35d8

This will save time hunting for the cause of problems when unit tests don't initialise the config.

Give separate REQUIRE statements for each element in list

e513d02

This will produce better error messages when tests fail.

Use type_try_dynamic_cast

3ca7510

Invert the iterator check to reduce cognitive load caused by extended…

75cbba1

… block scope

Change naming of implicit type parameters for inner classes

8fe86ee

Previously they duplicated the names for the type parameters of the outer classes

Make explicit type parameters shadow implicit ones with the same names

186adb8

Fixes problem where outer class type parameters take precedence over inner class ones Previously field would be given the type of the argument assigned to A::T, not B::T. class A<T> { class B<T> { T field; } }?

NathanJPhillips force-pushed the bugfix/generic_parameter_specialization_map branch from f5f62cf to 186adb8 Compare July 31, 2019 09:35

allredj reviewed Jul 31, 2019

View reviewed changes

NathanJPhillips merged commit 639b864 into diffblue:develop Jul 31, 2019

NathanJPhillips deleted the bugfix/generic_parameter_specialization_map branch July 31, 2019 12:47

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

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

Uh oh!

Conversation

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

Uh oh!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Jul 24, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

allredj left a comment

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!

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

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

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!

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

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!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

NathanJPhillips commented Jul 25, 2019

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!

Choose a reason for hiding this comment

Uh oh!

thomasspriggs left a comment

NathanJPhillips commented Jul 19, 2019 •

edited

Loading

codecov-io commented Jul 24, 2019 •

edited

Loading

smowton Jul 25, 2019 •

edited

Loading

NathanJPhillips Jul 25, 2019 •

edited

Loading

smowton Jul 25, 2019 •

edited

Loading