[TG-9299] Fix crash in case of user provided clinit for a clinit which is not in the symbol table #5073

romainbrenguier · 2019-09-02T09:15:02Z

The look-up for clinit could fail when we had a user provided clinit but the real clinit was not in the symbol table.
This adds a test which illustrate the case that was previously causing the exception.

Each commit message has a non-empty body, explaining why the change was made.
[na] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[na] 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).
[na] 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-09-02T09:20:11Z

jbmc/regression/jbmc/deterministic_assignments_json/Empty.java

@@ -0,0 +1,3 @@
+public class Empty {


Rather that emptiness, is having or not having static fields the critical attribute?

Yes, I've clarified that in the class names

smowton · 2019-09-02T09:20:49Z

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -838,7 +838,9 @@ void assign_from_json(
  location.set_function(function_id);
  allocate_objectst allocate(ID_java, location, function_id, symbol_table);
  code_blockt body_rec;
-  const auto class_name = declaring_class(symbol_table.lookup_ref(function_id));
+  const symbolt *function_symbol = symbol_table.lookup(function_id);


is lookup-ref vs. lookup-then-invariant really that different?

yes, you get a reasonable message on failure.

jbmc/src/java_bytecode/java_static_initializers.cpp

peterschrammel · 2019-09-02T09:18:10Z

jbmc/regression/jbmc/deterministic_assignments_json/test_empty_non_empty.desc

+--
+This tests what happens when the non-empty class is substitued with an empty
+one after compilation: After compiling EmptyNonEmpty.class and Empty.class,
+Empty.class is moved to NonEmpty.class.


What does 'moved' mean?

I've clarified that

peterschrammel · 2019-09-02T09:18:40Z

jbmc/regression/jbmc/deterministic_assignments_json/EmptyNonEmpty.java

+public class EmptyNonEmpty {
+
+  /// This test is meant to illustrate what happens when the non-empty
+  /// class is substitued with an empty one after compilation.


substituted

peterschrammel · 2019-09-02T09:19:11Z

jbmc/regression/jbmc/deterministic_assignments_json/test_empty_non_empty.desc

+^SIGNAL=0$
+--
+--
+This tests what happens when the non-empty class is substitued with an empty


substituted

peterschrammel · 2019-09-02T09:21:38Z

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -777,6 +777,7 @@ code_blockt get_user_specified_clinit_body(
  std::unordered_map<std::string, object_creation_referencet> &references)
 {
  jsont json;
+  const irep_idt real_clinit_name = clinit_function_name(class_id);


(commit message) careful

peterschrammel · 2019-09-02T09:22:05Z

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -838,7 +838,9 @@ void assign_from_json(
  location.set_function(function_id);
  allocate_objectst allocate(ID_java, location, function_id, symbol_table);
  code_blockt body_rec;
-  const auto class_name = declaring_class(symbol_table.lookup_ref(function_id));
+  const symbolt *function_symbol = symbol_table.lookup(function_id);


yes, you get a reasonable message on failure.

smowton · 2019-09-02T09:43:42Z

jbmc/regression/jbmc/deterministic_assignments_json/EmptyNonEmpty.java

@@ -0,0 +1,9 @@
+public class EmptyNonEmpty {


Change this name too

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 81e1c9b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/125753721

codecov-io · 2019-09-03T15:11:09Z

Codecov Report

Merging #5073 into develop will increase coverage by <.01%.
The diff coverage is 95.65%.

@@             Coverage Diff             @@
##           develop    #5073      +/-   ##
===========================================
+ Coverage    69.67%   69.67%   +<.01%     
===========================================
  Files         1319     1319              
  Lines       109290   109298       +8     
===========================================
+ Hits         76150    76157       +7     
- Misses       33140    33141       +1

Impacted Files	Coverage Δ
...bmc/src/java_bytecode/java_static_initializers.cpp	`99.09% <100%> (-0.01%)`	⬇️
...a_static_initializers/java_static_initializers.cpp	`100% <100%> (ø)`	⬆️
jbmc/src/java_bytecode/assignments_from_json.cpp	`97.45% <66.66%> (-0.35%)`	⬇️

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 522ae30...1b3c289. Read the comment docs.

antlechner

Is there any way to add a regression test for this? See my question below: I can't see how the bug that this is fixing would occur in practice.

antlechner · 2019-09-06T11:38:00Z

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -838,7 +838,9 @@ void assign_from_json(
  location.set_function(function_id);
  allocate_objectst allocate(ID_java, location, function_id, symbol_table);
  code_blockt body_rec;
-  const auto class_name = declaring_class(symbol_table.lookup_ref(function_id));
+  const symbolt *function_symbol = symbol_table.lookup(function_id);
+  INVARIANT(function_symbol, "Function must appear in symbol table");


💡 This message is quite general, maybe include function_id in it and/or mention the context in which this was looked up.

I don't know, the backtrace of the invariant should already give us the context.

antlechner · 2019-09-06T11:43:51Z

jbmc/src/java_bytecode/java_static_initializers.cpp

+      if(symbol_table.lookup(real_clinit_name) == nullptr)
+      {
+        // Case where there is a user provided clinit, but the real clinit
+        // doesn't appear in the symbol table. This may occur when some class


❓ Do you have an example of such a class substitution? Having these additional checks in is good of course, but I don't understand how this ever happened in practice. get_user_specified_clinit_body is only called to populate the body of a synthetic_method_typet::USER_SPECIFIED_STATIC_INITIALIZER if we see one. Such a synthetic method is only created in create_user_specified_clinit_function_symbol, which in turn is only called after several ifs, one of which is symbol_table.has_symbol(clinit_function_name(class_name)).
So it looks like the only way we could end up with a user_specified_clinit but no clinit would be if clinit was first added to the symbol table, then user_specified_clinit was added, and finally clinit was removed - but I'm not aware of the latter ever happening?

@antlechner
create_user_specified_clinit_function_symbol is called if needs_clinit_wrapper is true, which is when clinit exists or some other condition. If you think this is wrong then needs_clinit_wrapper needs to be corrected.

Ah, that's the part I overlooked! needs_clinit_wrapper is true if clinit exists for this class or a superclass.
So it looks like the mistake is that currently, we create a user_specified_clinit iff we create a clinit_wrapper. But really we should be creating a user_specified_clinit iff there is a clinit.

ok, I'm still going to merge this PR since it prevents a crash but the condition for calling create_user_specified_clinit_function_symbol should be fixed. Do you want to create an issue for that?

antlechner · 2019-09-06T11:47:15Z

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -817,6 +817,13 @@ code_blockt get_user_specified_clinit_body(
          }
        }
      }
+      if(symbol_table.lookup(real_clinit_name) == nullptr)


💡 Looks like it would make more sense to move this check just below the definition of real_clinit_name.
Edit: Ah, this is done in the next commit. Those two commits should probably be squashed.

This code doesn't need a writable reference so it should call lookup instead. We also add an invariant to check that the reference does exists, this gives more helpful messages than the generic `_Map_base::at`.

The assign_from_json will fail with an invariant failure if it is called on a method name that does not exist in the symbol table so we should be careful when calling it. This also make the function return early when the real clinit is not in the symbol table, which can avoid some unecessary computation.

The declaration of the reference class_json_value prevented merging the two if, and it can be removed without making the code more complicated since it is just an alias for class_entry->second

Test what happens when clinit for a class is not in the symbol table though the JSON file contains entries for this class. This used to cause map::at to throw an exception.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 1b3c289).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/126241524

romainbrenguier requested a review from antlechner September 2, 2019 09:15

romainbrenguier requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners September 2, 2019 09:15

romainbrenguier assigned antlechner Sep 2, 2019

romainbrenguier added bugfix Java Front End labels Sep 2, 2019

romainbrenguier force-pushed the bugfix/map-base-at branch from ad55b0e to 88a25c6 Compare September 2, 2019 09:21

smowton reviewed Sep 2, 2019

View reviewed changes

peterschrammel reviewed Sep 2, 2019

View reviewed changes

romainbrenguier force-pushed the bugfix/map-base-at branch from 88a25c6 to 639ad43 Compare September 2, 2019 09:36

smowton approved these changes Sep 2, 2019

View reviewed changes

romainbrenguier force-pushed the bugfix/map-base-at branch from 639ad43 to 7cd1a87 Compare September 2, 2019 10:04

romainbrenguier requested a review from segun3d September 2, 2019 10:22

romainbrenguier force-pushed the bugfix/map-base-at branch from 7cd1a87 to 81e1c9b Compare September 3, 2019 14:08

allredj reviewed Sep 3, 2019

View reviewed changes

romainbrenguier force-pushed the bugfix/map-base-at branch from 81e1c9b to 7a15634 Compare September 4, 2019 14:25

romainbrenguier requested review from kroening and tautschnig as code owners September 4, 2019 14:25

antlechner added the dependent - do not merge label Sep 6, 2019

antlechner approved these changes Sep 6, 2019

View reviewed changes

Replace lookup_ref call by lookup

bc75a6c

This code doesn't need a writable reference so it should call lookup instead. We also add an invariant to check that the reference does exists, this gives more helpful messages than the generic `_Map_base::at`.

romainbrenguier force-pushed the bugfix/map-base-at branch from 7a15634 to 0bf781d Compare September 6, 2019 12:53

romainbrenguier added 2 commits September 6, 2019 14:01

Drop intermediary reference to keep only one if

d9f5b08

The declaration of the reference class_json_value prevented merging the two if, and it can be removed without making the code more complicated since it is just an alias for class_entry->second

Unit test for user specified clinit when there is no clinit

1b3c289

Test what happens when clinit for a class is not in the symbol table though the JSON file contains entries for this class. This used to cause map::at to throw an exception.

romainbrenguier force-pushed the bugfix/map-base-at branch from 0bf781d to 1b3c289 Compare September 6, 2019 13:30

allredj reviewed Sep 6, 2019

View reviewed changes

romainbrenguier merged commit a60f45c into diffblue:develop Sep 6, 2019

romainbrenguier deleted the bugfix/map-base-at branch September 6, 2019 15:48

[TG-9299] Fix crash in case of user provided clinit for a clinit which is not in the symbol table #5073

[TG-9299] Fix crash in case of user provided clinit for a clinit which is not in the symbol table #5073

Uh oh!

Conversation

romainbrenguier commented Sep 2, 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!

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

antlechner 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!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov-io commented Sep 3, 2019 •

edited

Loading