Lazy function loading #1563
Merged
Lazy function loading #1563
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
NathanJPhillips
requested review from
kroening,
martin-cs,
mgudemann,
peterschrammel,
smowton,
tautschnig and
thk123
as code owners
|
The first 7 commits are from #1558 (waiting to be merged). Do not merge this until that PR has been merged and this one has been rebased on it. |
|
Tagging do-not-merge until predecessor PRs are merged |
smowton
approved these changes
Nov 6, 2017
|
Note: needs @kroening review before merge |
NathanJPhillips
force-pushed
the
feature/lazy-loading
branch
2 times, most recently
from
cb9badb to
2e5c5c4
Compare
NathanJPhillips
force-pushed
the
feature/lazy-loading
branch
from
2e5c5c4 to
4a81511
Compare
NathanJPhillips
requested review from
cesaro and
chrisr-diffblue
as code owners
NathanJPhillips
force-pushed
the
feature/lazy-loading
branch
from
4a81511 to
c1a02cc
Compare
|
Now mergeable once test failures are addressed |
NathanJPhillips
force-pushed
the
feature/lazy-loading
branch
10 times, most recently
from
76f0980 to
73c5007
Compare
Made load_all_functions compatible with some functions having already been loaded by using the lazy load procedure
After convert each function in convert_lazy_method call instrument and typecheck
The symbolt was erased and recreated rather than being modified. This was bad as it invalidated the reference to the symbol that we now use later.
Load the main function into the symbol table before generating the entry point so that we have access to its parameter names Allow attempts to load a function already loaded for non-lazy cases
Otherwise symbols won't have reproducible names
Remove line that depends on generated symbol name - Lucas confirms it wasn't the purpose of the test anyway.
Don't store followed type as type of superclass when doing clean cast as it may later change since we can now convert more methods after typechecking and doing this may change the type
NathanJPhillips
force-pushed
the
feature/lazy-loading
branch
from
03a7733 to
a2cf16d
Compare
|
I think everything is answered, fixed or an issue created to track it now. Tests are all passing. |
peterschrammel
approved these changes
Dec 21, 2017
|
TG passes too. Seems ready to go then. |
|
I am sticking a 'do not merge' label on it to reduce risk for a planned TG release on 3rd Jan. We'll merge it right after that. Besides, an approval is required by @tautschnig or @kroening. |
tautschnig
approved these changes
Dec 21, 2017
|
Added a new label (Merge on 4 Jan) as there might be more coming up the next days that shouldn't get merged until then. Obviously I know nothing about about the release so feel free to change that. |
smowton
added a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
67ec6f2 Merge remote-tracking branch 'upstream/develop' into pull-support-20180104 fabc99e Merge pull request diffblue#1563 from NathanJPhillips/feature/lazy-loading 2d67e42 Merge pull request diffblue#1692 from NathanJPhillips/feature/numbering-at 5266ba2 Merge commit 'ac4756fc3bb0e853f04de2b69f300d65cfbfc553' into pull-support-20171212 4f4a9c7 Add at method to template_numberingt d9cc0c0 Merge pull request diffblue#1685 from peterschrammel/remove-existing-coverage-goals f13c871 Update a comment in instrument_cover_goals 6c39443 Remove existing coverage goals a2cf16d Store symbol type instead of followed type when clean casting f96efb4 Change template parameter name to not clash with existing type b0cd57b Encapsulate lazy_goto_modelt::goto_functions ef02f4d Update test to handle changed symbol creation order 441d269 Reset counter used by get_fresh_aux_symbol in unit tests f759f25 Fix new test to run remove_java_new pass cb09d8e Fix new tests to use lazy loading 166563f Do lowering of java_new as a function-level pass 3779782 Always convert the main function from bytecode into the symbol_table 7e52e22 Always allow the main function not to have a body c938b08 Encapsulate maps in language_filest 87c6b28 Don't erase symbol in java_bytecode_convert_methodt::convert e3e44c8 Do type-checking as a function pass 2ba1364 Update load_all_functions 5f06e36 Recreate initialize in final aa5440b Moved call to final to lazy_goto_modelt::finalize a659bc0 Add lazy_goto_functions_mapt 7e1ecc9 Allow post-processing functions to run on a function-by-function basis 0c05be6 Allow convert_lazy_method on functions that don't have a lazy body 05a8da2 Make goto_convert_functions not add directly to function map c078858 Introduce lazy_goto_modelt a22dd1c Merge pull request diffblue#1671 from thk123/bugfix/TG-1278/correct-access-level 5b6eb00 Merge pull request diffblue#1668 from romainbrenguier/bugfix/string-index-of#TG-1846 9062853 Tidied up the generic specalised class copying the base class visibility f934ca3 String classes should be public 7b06a00 Merge pull request diffblue#1498 from smowton/smowton/feature/call_graph_improvements f3b4c9b Test for verification of the indexOf method 9a7fa2d Correct lower bound in String indexOf 682cd1a Use a symbol generator to avoid name clashes 28a2ada Access in empty array should be unconstrained d41403f Merge pull request diffblue#1665 from romainbrenguier/bugfix/string-out-of-bound#TG-1808 ac7e649 Use CProverString function in jbmc tests 22dc353 Add CProverString class for jbmc-strings tests ef610b3 Use CProverString functions in strings-smoke-tests 5c716c1 Add a CProverString class for string-smoke-tests 6b619e0 Deactivate preprocessing of charAt and substring bcfaaa4 Merge pull request diffblue#1664 from svorenova/refactoring_tg1190 c2a8bae Refactoring in specialization of generic classes 7a98e15 Rename call graph constructors 6228ed3 Slice global inits: use improved call graph d136bbc Expose limited call graph via goto-instrument 9c29bee Improve call graph unit tests 8ed3ccb Add documentation to call graph 8f6f429 Add call graph helpers 3b06a16 Call graph: add constructors that only include reachable functions 9b65862 grapht: add get_reachable function aaa8513 Call graph -> grapht transformation 8115248 Call graph: optionally record callsites git-subtree-dir: cbmc git-subtree-split: 67ec6f2
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is quite long, I'd recommend reviewing commit-by-commit. It has been reviewed in part in Security Scanner but @smowton feels it is ready to be reviewed for inclusion in to CBMC now.
In the end this version eagerly loads all functions (although it does it by pulling them in explicitly). Individual users are free to alter this behaviour.