Document the process for lazy loading v1

Author: NathanJPhillips

jbmc/src/java_bytecode/README.md

@@ -256,9 +256,57 @@ To be documented.
 
 To be documented.
 
-\section java-bytecode-lazy-methods-v1 Context Insensitive lazy methods (aka lazy methods v1)
-
-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
+phase; lazy loading starts at the method given by the --function argument and
+walks outwards. The following paragraphs describe the mechanism used by eager
+and context-insensitive lazy loading to achieve this.
+
+\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
+\ref java_bytecode_convert_method, passing in the method parse tree. This in
+turn uses \ref 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
+\ref java_bytecode_languaget::do_ci_lazy_method_conversion is called to do all
+conversion. This calls
+\ref ci_lazy_methodst::operator()(symbol_tablet &, method_bytecodet &, const method_convertert &),
+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
+\ref ci_lazy_methodst::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
+\ref ci_lazy_methodst::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