Documentation of lazy loading v1 [DOC-38] #2803

NathanJPhillips · 2018-08-21T17:44:10Z

No description provided.

cesaro · 2018-08-21T19:42:30Z

jbmc/src/java_bytecode/README.md


-To be documented.
+\ref java_bytecode_languaget::typecheck calls [java_bytecode_convert_class](\ref java_bytecode_languaget::java_bytecode_convert_class) (for each class loaded by the class loader) to create symbols for all classes and the methods in them. The methods, along with their parsed representation (including bytecode) are also added to a map called \ref java_bytecode_languaget::method_bytecode via a reference held in \ref java_bytecode_convert_classt::method_bytecode. typecheck then performs a switch over the value of [lazy_methods_mode](\ref java_bytecode_languaget::lazy_methods_mode). If lazy_methods_mode is \ref lazy_methods_modet::LAZY_METHODS_MODE_CONTEXT_INSENSITIVE then context-insensitive lazy loading is used.


Should we have lines broken at 80 characters? It's much easier to read diffs

Add a link for typecheck

peterschrammel · 2018-08-21T22:28:27Z

jbmc/src/java_bytecode/README.md


-To be documented.
+\ref java_bytecode_languaget::typecheck calls [java_bytecode_convert_class](\ref java_bytecode_languaget::java_bytecode_convert_class) (for each class loaded by the class loader) to create symbols for all classes and the methods in them. The methods, along with their parsed representation (including bytecode) are also added to a map called \ref java_bytecode_languaget::method_bytecode via a reference held in \ref java_bytecode_convert_classt::method_bytecode. typecheck then performs a switch over the value of [lazy_methods_mode](\ref java_bytecode_languaget::lazy_methods_mode). If lazy_methods_mode is \ref lazy_methods_modet::LAZY_METHODS_MODE_CONTEXT_INSENSITIVE then context-insensitive lazy loading is used.


Add a link for typecheck

peterschrammel · 2018-08-21T22:29:50Z

jbmc/src/java_bytecode/README.md

-To be documented.
+\ref java_bytecode_languaget::typecheck calls [java_bytecode_convert_class](\ref java_bytecode_languaget::java_bytecode_convert_class) (for each class loaded by the class loader) to create symbols for all classes and the methods in them. The methods, along with their parsed representation (including bytecode) are also added to a map called \ref java_bytecode_languaget::method_bytecode via a reference held in \ref java_bytecode_convert_classt::method_bytecode. typecheck then performs a switch over the value of [lazy_methods_mode](\ref java_bytecode_languaget::lazy_methods_mode). If lazy_methods_mode is \ref lazy_methods_modet::LAZY_METHODS_MODE_CONTEXT_INSENSITIVE then context-insensitive lazy loading is used.
+
+Context-insensitive lazy loading is an alternative method body loading strategy to eager loading, which is selected when lazy_methods_mode is \ref java_bytecode_languaget::LAZY_METHODS_MODE_EAGER. Under eager loading \ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &) is called once for each method listed in method_bytecode (described above). This then calls \ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, optionalt<ci_lazy_methods_neededt>) without a ci_lazy_methods_neededt object, which calls java_bytecode_convert_method, passing in the method parse tree. This in turn uses java_bytecode_convert_methodt to turn the bytecode into symbols for the parameters and local variables and finish populating the symbol for the method, including converting the instructions to a codet.


Turn all identifiers into links (entire document)

Just first occurrence of each reference or every one?

smowton · 2018-08-22T08:21:22Z

Suggest adding a short section prior to all this close-up technical detail that briefly describes the strategies without citing particular method names. Eager loading simply loads every method belonging to classes found in the first phase; lazy loading starts at the method given by the --function argument and walks outwards, briefly explain the virtual call strategy, briefly explain reasons why we consider a method accessible...

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 6c05a85).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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).

peterschrammel · 2018-09-06T17:19:13Z

jbmc/src/java_bytecode/README.md

+have been converted, their parameters and local variables, globals accessed
+from these methods and classes are kept, everything else is thrown away. This
+leaves a symbol table that contains reachable symbols fully populated,
+including the instructions for methods converted to a codet.


allredj

Passed Diffblue compatibility checks (cbmc commit: be8e0b3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84138811

owen-mc-diffblue · 2018-09-10T12:41:22Z

jbmc/src/java_bytecode/README.md

-To be documented.
+\section java-bytecode-lazy-methods-v1 Context-Insensitive lazy methods (aka lazy methods v1)
+
+Eager loading simply loads every method belonging to classes found in the first


It's not clear what Eager Loading is. I think it would be clearer to make this section about Loading Strategies and have subsections for Eager Loading and Context-Insensitive Lazy Methods. If you don't want to do that, at least have a first sentence which introduces Eager Loading.

owen-mc-diffblue

More suggestions to improve it, but it's good enough that you could just merge it if you want.

owen-mc-diffblue · 2018-09-10T15:39:30Z

jbmc/src/java_bytecode/README.md

+\section loading-strategies Loading strategies
+
+Loading strategies are policies that determine what classes and method bodies
+ are loaded. On an inital pass, the symbols for all classes in all paths on the 


inital -> initial

owen-mc-diffblue · 2018-09-10T15:39:34Z

jbmc/src/java_bytecode/README.md

+Loading strategies are policies that determine what classes and method bodies
+ are loaded. On an inital pass, the symbols for all classes in all paths on the 
+ Java classpath are loaded. Eager loading is a policy that then loads method 
+ bodies for every one of these classes and for all the method bodies in these


This sentence doesn't make sense to me... we load all the method bodies for all the method bodies...

owen-mc-diffblue · 2018-09-10T15:42:48Z

jbmc/src/java_bytecode/README.md

+Context-insensitive lazy loading starts at the method given by the `--function`
+ argument and follows type references (e.g. in the definitions of fields and 
+ method parameters) and function references (at function call sites) to 
+ locate further classes and methods to load.


This line and the two above are indented by a space

owen-mc-diffblue · 2018-09-10T15:45:38Z

jbmc/src/java_bytecode/README.md

+ method parameters) and function references (at function call sites) to 
+ locate further classes and methods to load.
+
+If [lazy_methods_mode](\ref java_bytecode_languaget::lazy_methods_mode) is


This sentence seems out of place here. Would it be better at the beginning of this subsection? The first few sentences of this subsection don't really flow, like they were written separately and put together later.

allredj

Passed Diffblue compatibility checks (cbmc commit: d85ed15).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84322492

NathanJPhillips self-assigned this Aug 21, 2018

NathanJPhillips requested a review from smowton August 21, 2018 17:44

NathanJPhillips requested review from cesaro, cristina-david, mgudemann, peterschrammel, pkesseli and thk123 as code owners August 21, 2018 17:44

cesaro reviewed Aug 21, 2018

View reviewed changes

peterschrammel added the documentation label Aug 21, 2018

peterschrammel reviewed Aug 21, 2018

View reviewed changes

peterschrammel assigned thk123 Aug 21, 2018

peterschrammel assigned NathanJPhillips and unassigned thk123 and NathanJPhillips Aug 30, 2018

NathanJPhillips force-pushed the documentation/lazy-loading branch from dc3e785 to 6c05a85 Compare September 4, 2018 16:03

NathanJPhillips requested review from peterschrammel and cesaro September 4, 2018 16:04

allredj reviewed Sep 4, 2018

View reviewed changes

peterschrammel approved these changes Sep 6, 2018

View reviewed changes

NathanJPhillips force-pushed the documentation/lazy-loading branch from 6c05a85 to be8e0b3 Compare September 7, 2018 13:29

allredj reviewed Sep 7, 2018

View reviewed changes

owen-mc-diffblue suggested changes Sep 10, 2018

View reviewed changes

NathanJPhillips force-pushed the documentation/lazy-loading branch from 14b095b to d411a2a Compare September 10, 2018 15:08

NathanJPhillips requested a review from owen-mc-diffblue September 10, 2018 15:09

owen-mc-diffblue approved these changes Sep 10, 2018

View reviewed changes

NathanJPhillips force-pushed the documentation/lazy-loading branch from d411a2a to d85ed15 Compare September 10, 2018 15:53

Document loading strategies including the mechanism for lazy loading v1

d85ed15

owen-mc-diffblue approved these changes Sep 10, 2018

View reviewed changes

NathanJPhillips merged commit e32c469 into diffblue:develop Sep 10, 2018

NathanJPhillips deleted the documentation/lazy-loading branch September 10, 2018 17:03

allredj reviewed Sep 10, 2018

View reviewed changes


		To be documented.
		\ref java_bytecode_languaget::typecheck calls [java_bytecode_convert_class](\ref java_bytecode_languaget::java_bytecode_convert_class) (for each class loaded by the class loader) to create symbols for all classes and the methods in them. The methods, along with their parsed representation (including bytecode) are also added to a map called \ref java_bytecode_languaget::method_bytecode via a reference held in \ref java_bytecode_convert_classt::method_bytecode. typecheck then performs a switch over the value of [lazy_methods_mode](\ref java_bytecode_languaget::lazy_methods_mode). If lazy_methods_mode is \ref lazy_methods_modet::LAZY_METHODS_MODE_CONTEXT_INSENSITIVE then context-insensitive lazy loading is used.

Documentation of lazy loading v1 [DOC-38] #2803

Documentation of lazy loading v1 [DOC-38] #2803

Uh oh!

Conversation

NathanJPhillips commented Aug 21, 2018

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!

smowton commented Aug 22, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

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!

owen-mc-diffblue 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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

smowton commented Aug 22, 2018 •

edited

Loading