Document the process for lazy loading v1

Author: NathanJPhillips

jbmc/src/java_bytecode/README.md

@@ -47,9 +47,13 @@ To be documented.
 
 To be documented.
 
-\section java-bytecode-lazy-methods-v1 Context Insensitive lazy methods (aka lazy methods v1)
+\section java-bytecode-lazy-methods-v1 Context-Insensitive lazy methods (aka lazy methods v1)
 
-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.
+
+When context-insensitive lazy loading is in operation do_ci_lazy_method_conversion is called to do all conversion. This calls ci_lazy_methodst::operator(), which creates a work list of methods to check, starting with the entry point, and classes, starting with the types of any class-typed parameters to the entry point. For each method in the work list it calls convert_and_analyze_method, which calls the same java_bytecode_languaget::convert_single_method used by eager loading to do the conversion (via a std::function object passed in via parameter method_converter) and then calls gather_virtual_callsites to locate virtual calls. Any classes that may implement an override of the virtual function called are added to the work list. Finally the symbol table is iterated over and methods that 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.
 
 \section java-bytecode-core-models-library Core Models Library