Avoid redundant computations in get_user_specified_clinit #5078

romainbrenguier · 2019-09-03T09:16:47Z

Some computation like json parsing and iterating through the map were done at each call to get_user_specified_clinit which is called a lot of times for projects with large json file for static values.
With this pull request on such an example the execution time went from 10 seconds to 2 seconds (mostly thanks to removing the redundant json parsing).

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).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
[na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

smowton

The lazy map feels like it's apt to get out of date, but actually it isn't, since it only includes function and field symbols, all of which are produced early (in the convert-class phase). Suggest adding comments to the map and the lazy class clarifying that get_declaring_class doesn't include e.g. local variables, which are updated by convert_single_method and therefore would cause it to get out of date.

In the same comments clarify under what circumstances it must be purged and recalculated (i.e. if some transformation creates or deletes function or field symbols).

For example, should it be purged after lazy-methods erases a bunch of unused function symbols from the symbol table?

smowton · 2019-09-03T11:17:37Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

+    const std::string filename = options.get_option("static-values");
+    jsont tmp_json;
+    if(!parse_json(filename, *message_handler, tmp_json))
+      static_values_file = std::move(tmp_json);


static_values_file -> static_values_json

smowton · 2019-09-03T11:18:22Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

+      if(!tmp_json.is_object())
+      {
+        warning() << "Provided JSON file for static-values is not a JSON "
+                  << "object, it will be ignored." << messaget::eom;


smowton · 2019-09-03T11:18:29Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

-      static_values_file = std::move(tmp_json);
+    if(parse_json(filename, *message_handler, tmp_json))
+    {
+      warning() << "Provided JSON file for static-values cannot be parsed, it"


smowton · 2019-09-03T11:19:48Z

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -769,17 +769,16 @@ code_ifthenelset get_clinit_wrapper_body(

 code_blockt get_user_specified_clinit_body(
  const irep_idt &class_id,
-  const json_objectt &json,
+  const json_objectt &static_values_file,


Param rename snuck into commit "Remove unused message handler"

smowton · 2019-09-03T11:20:27Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -217,7 +217,7 @@ void java_bytecode_languaget::set_language_options(const optionst &options)
                  << "object, it will be ignored." << messaget::eom;
      }
      else
-        static_values_file = std::move(to_json_object(tmp_json));
+        static_values_json = std::move(to_json_object(tmp_json));


Aha, this does get done. Suggest squash into earlier commit that changes the type.

romainbrenguier · 2019-09-03T13:41:57Z

@smowton I've tried to clarify when the map could get outdated. Can you check the new doc?

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 5650d05).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/125909454
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.

antlechner

Looks good!

antlechner · 2019-09-05T10:44:53Z

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -229,10 +229,10 @@ class java_bytecode_languaget:public languaget
  java_string_library_preprocesst string_preprocess;
  std::string java_cp_include_files;
  bool nondet_static;
-  /// Path to a JSON file which contains initial values of static fields (right
+  /// JSON which contains initial values of static fields (right
  /// after the static initializer of the class was run). This is read from the


💡 read from the ... option -> read from the file specified by the ... option?

antlechner · 2019-09-05T11:49:12Z

src/util/range.h

+/// Utility function to make equal_range method of multimap easier to use by
+/// returning a ranget object. For instance, we can write:
+/// `for(auto value : equal_range(map, key).filter(...).map(...)) {...}`.
+template <typename Mapt>


❔ It looks like the convention in this file is to write typenames in small letters, e.g. typename containert above?

antlechner · 2019-09-05T11:57:41Z

jbmc/src/java_bytecode/java_static_initializers.cpp

-      for(const auto &symbol_pair : symbol_table)
+      const auto class_to_declared_symbols_map =
+        class_to_declared_symbols(symbol_table);
+      for(const auto &symbol_pair :


💡 symbol_pair isn't such a good name for this any more. Maybe class_symbol_pair?

antlechner · 2019-09-05T12:30:08Z

jbmc/src/java_bytecode/java_bytecode_language.h

+/// would make later calls return an outdated map. The
+/// lazy_class_to_declared_symbols_mapt would then need to be reinitialized.
+/// Similarly if some transformation creates or deletes function or field
+/// symbols the map would get out of date and would need to be reinitialized.


💡 Could specify "creates or deletes function or field symbols in the symbol table"

antlechner · 2019-09-05T12:43:38Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1131,10 +1153,13 @@ static void notify_static_method_calls(
 /// \param symbol_table: global symbol table
 /// \param needed_lazy_methods: optionally a collection of needed methods to
 ///   update with any methods touched during the conversion
+/// \param class_to_declared_symbols: map classes to the symbols that


⛏️ map -> maps

antlechner · 2019-09-05T12:55:55Z

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -201,13 +225,18 @@ class java_bytecode_languaget:public languaget
    const irep_idt &function_id,
    symbol_table_baset &symbol_table)
  {
+    lazy_class_to_declared_symbols_mapt class_to_declared_symbols{};


❓ Why does this method create its own lazy_class_to_declared_symbols_mapt? Could this cause any problems or inconsistencies?

No inconsistency because if it is redeclared everytime this preserves the old behaviour. But yes it's not optimal I will make sure it is declared by the function which calls that one on each methods.

codecov-io · 2019-09-06T08:01:49Z

Codecov Report

Merging #5078 into develop will decrease coverage by <.01%.
The diff coverage is 91.3%.

@@             Coverage Diff             @@
##           develop    #5078      +/-   ##
===========================================
- Coverage    69.66%   69.66%   -0.01%     
===========================================
  Files         1319     1319              
  Lines       109234   109250      +16     
===========================================
+ Hits         76102    76106       +4     
- Misses       33132    33144      +12

Impacted Files	Coverage Δ
jbmc/src/java_bytecode/java_static_initializers.h	`100% <ø> (ø)`	⬆️
src/util/range.h	`100% <ø> (ø)`	⬆️
...bmc/src/java_bytecode/java_static_initializers.cpp	`98.2% <100%> (+0.42%)`	⬆️
jbmc/src/java_bytecode/java_bytecode_language.h	`76.92% <100%> (+4.19%)`	⬆️
jbmc/src/java_bytecode/java_bytecode_language.cpp	`93.08% <80.95%> (-0.67%)`	⬇️
src/util/symbol_table_builder.h	`65.21% <0%> (-17.4%)`	⬇️
src/util/journalling_symbol_table.h	`78.94% <0%> (-10.53%)`	⬇️
src/util/symbol_table_base.h	`88.46% <0%> (-3.85%)`	⬇️

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 fc0a0cd...30bc2b6. Read the comment docs.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 5450149).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/126187118
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.

No functional changes. This is so that we can avoid recomputing it in each loop.

This avoids reparsing the whole json file for each class that needs a clinit. Locally, on an example with a large json provided for --static-values, execution time went from 10s to 2s.

There is no reason to delay this check, and we can provide useful warning messages right at the start of the bytecode analysis.

No user specified static initializer should appear if the static-values is not set anyway. So this if condition can be replaced by an invariant at the call site.

This is no longer used now that the JSON parsing is done outside this function.

This is to make the equal_range method of multimap easier to use. The usage is illustrated in this commit by an example in java_static_initializers which allows use to use range-for. This will be also useful in following commits.

This is an intermediary commit towards computing this map outside of the get_user_specified_clinit_body function, so that we can avoid going through the whole symbol map at each get_user_specified_clinit_body call.

This is an intermediary commit that gets us closer to avoiding recomputing this map everytime.

This is to avoid computing the map several times and make sure it is never computed if it is not actually needed.

allredj

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

romainbrenguier requested review from cesaro, cristina-david, kroening, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners September 3, 2019 09:16

romainbrenguier requested a review from antlechner September 3, 2019 09:18

romainbrenguier assigned antlechner Sep 3, 2019

smowton approved these changes Sep 3, 2019

View reviewed changes

romainbrenguier force-pushed the refactor/user-specified-clinit branch from 2f431d4 to 0d15f12 Compare September 3, 2019 13:40

romainbrenguier added the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Sep 3, 2019

romainbrenguier mentioned this pull request Sep 3, 2019

Add unit tests for get_user_specified_clinit_body #5081

Merged

3 tasks

romainbrenguier force-pushed the refactor/user-specified-clinit branch 2 times, most recently from 44b45b7 to 5650d05 Compare September 4, 2019 13:34

allredj reviewed Sep 4, 2019

View reviewed changes

romainbrenguier removed the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Sep 5, 2019

antlechner approved these changes Sep 5, 2019

View reviewed changes

romainbrenguier mentioned this pull request Sep 5, 2019

Add a lazyt class for delaying computations #5090

Merged

6 tasks

romainbrenguier force-pushed the refactor/user-specified-clinit branch 2 times, most recently from 5450149 to dac3e16 Compare September 6, 2019 07:08

allredj reviewed Sep 6, 2019

View reviewed changes

romainbrenguier added 4 commits September 6, 2019 09:15

Move real_clinit_name declaration up

85c2f0d

No functional changes. This is so that we can avoid recomputing it in each loop.

Make get_user_specified_clinit_body take jsont arg

6a61209

This avoids reparsing the whole json file for each class that needs a clinit. Locally, on an example with a large json provided for --static-values, execution time went from 10s to 2s.

Ensure JSON file is JSON object just after parsing

c0b681a

There is no reason to delay this check, and we can provide useful warning messages right at the start of the bytecode analysis.

Make get_user_specified_clinit_body json arg non optional

8479641

No user specified static initializer should appear if the static-values is not set anyway. So this if condition can be replaced by an invariant at the call site.

romainbrenguier added 5 commits September 6, 2019 09:15

Remove unused message handler

3ed8e34

This is no longer used now that the JSON parsing is done outside this function.

Add an equal_range utility function

2d2ebca

This is to make the equal_range method of multimap easier to use. The usage is illustrated in this commit by an example in java_static_initializers which allows use to use range-for. This will be also useful in following commits.

Extract a class_to_declared_symbols method

dd45287

This is an intermediary commit towards computing this map outside of the get_user_specified_clinit_body function, so that we can avoid going through the whole symbol map at each get_user_specified_clinit_body call.

Make class_to_declared_symbols take multimap argument

67a02e6

This is an intermediary commit that gets us closer to avoiding recomputing this map everytime.

Declare a lazy_class_to_declared_symbols_mapt class

30bc2b6

This is to avoid computing the map several times and make sure it is never computed if it is not actually needed.

romainbrenguier force-pushed the refactor/user-specified-clinit branch from dac3e16 to 30bc2b6 Compare September 6, 2019 08:17

allredj reviewed Sep 6, 2019

View reviewed changes

romainbrenguier merged commit 78fc2b7 into diffblue:develop Sep 6, 2019

romainbrenguier deleted the refactor/user-specified-clinit branch September 6, 2019 09:34

Avoid redundant computations in get_user_specified_clinit #5078

Avoid redundant computations in get_user_specified_clinit #5078

Uh oh!

Conversation

romainbrenguier commented Sep 3, 2019

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!

romainbrenguier commented Sep 3, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

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!

antlechner Sep 5, 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!

codecov-io commented Sep 6, 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!

Uh oh!

antlechner Sep 5, 2019 •

edited

Loading

codecov-io commented Sep 6, 2019 •

edited

Loading