Unroll enumeration values() loops #2651
Conversation
smowton
requested review from
cesaro,
cristina-david,
kroening,
mgudemann,
NathanJPhillips,
peterschrammel,
pkesseli,
tautschnig and
thk123
as code owners
| else | ||
| return irep_idt(); | ||
| } | ||
| else if(has_suffix(id2string(current_function), ".<clinit>:()V")) |
There was a problem hiding this comment.
how do we know this is an enum's <clinit> ?
There was a problem hiding this comment.
We don't -- this function returns a candidate, which its caller checks further.
| if(id2string(clone_caller).find(".values:()[L") != std::string::npos) | ||
| return clone_caller; | ||
| else | ||
| return irep_idt(); |
There was a problem hiding this comment.
maybe better use an optionalt<irep_idt> as return value
| { | ||
| const irep_idt &clone_caller = | ||
| context.at(context.size() - 2).function_identifier; | ||
| if(id2string(clone_caller).find(".values:()[L") != std::string::npos) |
There was a problem hiding this comment.
are we sure that it will always be for an enum type's .values method ?
| else | ||
| return irep_idt(); | ||
| } | ||
|
|
||
| /// Unwind handler that special-cases the clinit (static initializer) functions | ||
| /// of enumeration classes. When java_bytecode_convert_classt has annotated them | ||
| /// with a size of the enumeration type, this forces unwinding of any loop in |
There was a problem hiding this comment.
this will also need to be updated, effectively this unwind hander will now unroll any loop in an enum's <clinit> and in an array clone when this is called from within a call to an enum's values method?
|
What about fully unrolling those enum loops before even passing anything to symbolic execution? |
smowton
force-pushed
the
smowton/feature/unroll-enum-clone-loops
branch
2 times, most recently
from
e53df5d to
ac18b8c
Compare
|
@mgudemann added comments to clarify and fixed the broken comment that you noted. @tautschnig that means a bunch of code duplication even if you never need it -- seems cleaner to re-use the existing should-I-unroll hook to me |
|
@mgudemann, @smowton, do we have tests for this? |
smowton
force-pushed
the
smowton/feature/unroll-enum-clone-loops
branch
2 times, most recently
from
76bcb03 to
6b35557
Compare
|
@peterschrammel cherry-picked the tests (and other preliminary cleanups) from #2569 |
|
@peterschrammel think CI is ok really (except for Mac snags) |
What code duplication are you worried about? The copies of instructions introduced be unrolling? I think most analyses would benefit from that, unless you are telling me the memory overhead would be prohibitive? (I don't know how much of a Java program this would apply to.) And I disagree with the re-use of the hook being cleaner: a decision that the language front-end makes is deferred until a later stage, but then actually answered by that very same language front-end. |
|
Inlining / cloning array.clone() for each enumeration type and then unrolling array.clone() perhaps hundreds of iterations. Seems wasteful considering we might not use it at all. Ideally I'd just have the front-end annotate the loop, but the annotation requires context (array.clone called from MyEnum.values), hence the current implementation. |
This enables unwind handlers to use the calling context to decide when to unwind a particular loop, the first use case being generic array clone methods called from enumeration type methods with known bounds.
If an enumeration type's values() method clones an array, we assume it is cloning the array of enumeration values and therefore is bounded by the enumeration's size, similar to the existing handling of enumeration static initializers.
Before we considered the `code_switch_caset` to belong to the target instruction which lead to uncoverable goals of the form: IF condition 1 then GOTO 1 ... 1: GOTO 2 ASSERT false // uncoverable block ... 2:
It could already do index-of-constant-array -- by replacing its custom code with simplify_expr
we can expand that to also support member-of-constant-struct, as occurs when symex's deref'ing
and then the interpreter's environment translate a variable-length array type like int[obj->length]
into int[particular_object.length] and then int[{.length = 1, .data = &xyz}.length].
Update regression tests
Currently the regression tests fail with symex driven lazy loading due to a difference in generated properties.
smowton
force-pushed
the
smowton/feature/unroll-enum-clone-loops
branch
from
6b35557 to
4f158a3
Compare
Do you have data? I think the idea of enabling context-specific unwinding bounds is a very good one and is useful well beyond the use case discussed here, assuming this is exposed all the way to the command-line. But I think it is an approach that should be taken when the program itself might not contain sufficient information. When the language front-end does have this information, it should just instruct the static loop unwinder to act on it. |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 4f158a3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80717375
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).
What is the rationale behind that? |
Avoid a weird game of "I have the answer for you but I won't tell you right now, I'll just tell you later?" In more technical terms: decoupling. I understand that lazy-loading-during-symex will make this harder and then you possibly can't do it the way I'm proposing. But wherever possible we should really try to have nicely decoupled components and avoid tying analysis and front-ends together in mysterious ways. |
|
Mostly for future reference: can we all (myself absolutely included) please make a habit of having PRs that are no more than a single feature/bugfix. It doesn't have to be just a single commit, but if it's multiple commits the author should really ask themselves whether those absolutely go together. |
5d3ea03 Merge pull request diffblue#2693 from zhixing-xu/fix_rw_range_upper 2b40338 Update test.desc c6d0427 Merge pull request diffblue#2674 from diffblue/msvc-link 318474f Merge pull request diffblue#2678 from romainbrenguier/feature/extend-builtin-functions-part3 c63030f Regression test for goto-link personality 64fedd0 Microsoft LINK personality d9f9dd9 Merge pull request diffblue#2688 from tautschnig/concat-dir-file 99946fc Merge pull request diffblue#2675 from diffblue/goto-cl-echo-file 252d857 Merge pull request diffblue#2687 from tautschnig/fo-directory 0d7ebd5 Fixed a problem where the rw_set range's upper bound not set correctly 29eab32 goto-cl: Fail invocation of trying to compile multiple files to non-directory 7f587c4 Fix concat_dir_file for Windows and unit-test it a44468b Document string_builtin_function::eval ecc0e43 Document eval_is_upper_case a345d30 Document eval_string 58307a0 Tests for String.toUpperCase 71de2e3 Tests for String.toLowerCase 579d00c Remove redundant function application ID check e2961b5 Add builtin class for string_to_upper_case fe9071b Make to_upper_case work for Latin-1 supplement 53ccd3f Refactor string_to_upper_case be477c9 Remove assumptions that input char are < 0x100 836cbad Extract an is_upper_case function 1137ffd Improve documentation of add_axioms_for_to_lower_case a71f2c0 Implement builtin string_to_lower_case function fae6a48 Merge pull request diffblue#2467 from tautschnig/vs-except 24de513 Merge pull request diffblue#2474 from tautschnig/vs-identifier e14f2f2 Merge pull request diffblue#2685 from diffblue/clcache-again 08698cc Merge pull request diffblue#2681 from diffblue/remove-aig d42020b remove --aig option cd4a163 AWS codebuild windows: set clcache base directory 1ba928c cleanup unnecessary path from configuration file 8c4801b Refactor add_axioms_for_to_lower_case 4291232 Merge pull request diffblue#2686 from diffblue/buildspec-apt-cache 3adb717 AWS codebuild: cache apt lists and packages 0efb169 remove AIGs 3a9c825 Merge pull request diffblue#2682 from diffblue/fix-clcache b9b5660 Merge pull request diffblue#2483 from tautschnig/vs-java-parameters a66ab1e CL prints the name of the file that's compiled onto stdout 0698a5f Merge pull request diffblue#2673 from diffblue/goto-cl-Fo 75855bf Java front-end: remove unused parameters 4df2187 debugging output to resolve seg fault 5bc7456 goto-cl: /Fo can set an output directory a43e4fa add is_directory to file_util.h 4ad91fb Codebuild for windows: set up cache path properly effb01b Merge pull request diffblue#2641 from diffblue/typedef-type 5ef2802 Merge pull request diffblue#2679 from tautschnig/version-string 2efea52 Refine test patterns to avoid spurious matches aa7ebbc Merge pull request diffblue#2672 from diffblue/goto-cc-multiple-source-files aaea781 Merge pull request diffblue#2671 from diffblue/fix_get_base_name 8b51faf fix get_base_name 694daaf gcc mode: error in case multiple files are given with -c and -o 09fdca3 Merge pull request diffblue#2643 from svorenova/fixup-nondet-static d42054a Merge pull request diffblue#2669 from diffblue/spurious-cover-test b391c9e introduce typedef_type in the C frontend 114030b Merge pull request diffblue#2664 from romainbrenguier/feature/extend-builtin-functions-part2 46f6231 cbmc test no longer uses --cover daff1d1 Make nondet-static replace lines in CPROVER_init 1bca129 Merge pull request diffblue#2665 from tautschnig/gcc-conditional-stmt 31366ad Tests for StringBuilder.setCharAt f4285e7 Add builtin support for string_set_char 2a8ea0f Better specify out-of-bounds case for set_char 9415a24 Refactor add_axioms_for_set_char 9762886 Refactor string_concat_char builtin function b62bf01 Make nondet-static check for ID_C_no_nondet_initialization a50562e Mark java.lang.String.Literals with ID_C_constant b3c08d3 Mark internal Java variables with ID_C_no_nondet_initialization f2dc978 Add a new comment to mark variables that should not be nondet initialized da7966c Merge pull request diffblue#2645 from mmuesly/feature_test_posix_memalign cb4a340 Merge pull request diffblue#2647 from diffblue/cleanout-jar-filet 2b27a2d Merge pull request diffblue#2622 from martin-cs/feature/context-sensitive-ait-merge-2 00b26a8 Adds a test for posix_memalign in stdlib.c 0f5a057 Merge pull request diffblue#2667 from tautschnig/slicer-cleanup 16e6462 Remove no-longer-used ifdef 96d345b Clean GCC conditional expressions in right-hand sides of declarations 086c266 Merge pull request diffblue#2651 from smowton/smowton/feature/unroll-enum-clone-loops f69b244 Merge pull request diffblue#2625 from smowton/smowton/feature/value-set-accuracy 730b3e2 Merge pull request diffblue#2655 from romainbrenguier/feature/extend-builtin-functions c4569dd remove java_class_loader_limitt from jar_filet e0f954d Merge pull request diffblue#2659 from smowton/smowton/fix/cmake-third-time-is-charm 7f547b1 Merge pull request diffblue#2656 from smowton/smowton/fix/testsuite-name 3a1593b Tests for String.valueOf(int) 7414d76 Add builtin support for string_of_int 0b44c89 Add version of make_string accepting iterators f81f082 Rename function to add_axioms_for_string_of_int 9a2a7c2 Switch version.cpp from a rule product to a byproduct 943d60c Value set: handle with, array and struct expressions more accurately 4f158a3 Mark regression tests as expecting failure for symex driven loading c9a53f9 Add regression tests for changes to JBMC enumeration support a985eae Interpreter: deal with member-of-constant-struct expressions 361469b Change source location of jump target in {table|lookup}switch 6270968 java-unwind-enum-static: also unwind clone loop in Enum.values() 714de0d Symex: expose call stack to unwinding decision making fb239ef Fix jbmc-generic-symex-driven-lazy-loading test name 28ba192 Strengthen the invariant on what are acceptable function calls. 773bc86 Convert various comments, asserts and throws into invariants. e65f027 Add comments to the abstract interpreter interface. 1fe0796 Convert various older domains to use the more recent ait API. afe32b7 Refactor the methods that access "the abstract domain at a location". aa743b3 Remove unused exception name from catch statement 5703504 Remove unused parameter identifier git-subtree-dir: cbmc git-subtree-split: 5d3ea03
No description provided.