[TG-9450] Allocate array with right length when "@nondetLength" not used in Json #5106
Conversation
romainbrenguier
force-pushed
the
refactor/assign-from-json
branch
3 times, most recently
from
28b633c to
a9433c6
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: a9433c6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/127412071
Codecov Report
@@ Coverage Diff @@
## develop #5106 +/- ##
===========================================
- Coverage 66.94% 65.33% -1.61%
===========================================
Files 1145 1145
Lines 93630 93647 +17
===========================================
- Hits 62677 61187 -1490
- Misses 30953 32460 +1507
Continue to review full report at Codecov.
|
romainbrenguier
force-pushed
the
refactor/assign-from-json
branch
2 times, most recently
from
6422e28 to
d10671e
Compare
romainbrenguier
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli,
smowton and
thk123
as code owners
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d10671e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/127759742
romainbrenguier
changed the title
romainbrenguier
force-pushed
the
refactor/assign-from-json
branch
3 times, most recently
from
b01ea24 to
b420f26
Compare
|
@antlechner comments addressed, ready for re-review |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: e0aeb22).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128210163
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: b01ea24).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128210873
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: b420f26).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128214053
| @@ -457,18 +457,16 @@ static symbol_exprt nondet_length( | |||
| } | |||
|
|
|||
| /// One of the cases in the recursive algorithm: the case where \p expr | |||
| /// represents an array. | |||
| /// represents an array which is not flagged with @nondetLength. | |||
There was a problem hiding this comment.
❔ Does the @ compile correctly with Doxygen?
💡 Could mention here in/after the "Allocate array with right size when possible" commit that we only need this function for arrays that are reference-equal to some other array.
There was a problem hiding this comment.
 Does the @ compile correctly with Doxygen?
No @nondetLength didn't appear, I've added back quotes "`" and now it works.
💡 Could mention here in/after the "Allocate array with right size when possible" commit that we only need this function for arrays that are reference-equal to some other array.
Actually this function is also used in the non-reference case.
| /// We add constraints on the length: if "nondetLength" is specified in \p json, | ||
| /// then the number of elements specified in \p json should be less than or | ||
| /// equal to the length of the array. Otherwise the number of elements should be | ||
| /// We add an assume statement constraining the number of elements to be |
There was a problem hiding this comment.
💡 Might be clearer to write it the other way round (we constrain the length of the array, the number of elements is known and constant).
| java_class_typet type; | ||
| // TODO java_class_typet constructors should ensure there is always a | ||
| // @class_identifier field, and that name is always set | ||
| type.set_name("java::" + class_name); |
There was a problem hiding this comment.
⛏️ type.set_name(test_class_symbol.name)
| entry["field_name"] = [] { | ||
| json_objectt int_json; | ||
| int_json["value"] = json_numbert{"42"}; | ||
| int_json["@type"] = json_stringt{"int"}; |
There was a problem hiding this comment.
⛏️ Note that json-io, the library that the inputs to assign_from_json are based on, never uses primitives so would use java.lang.Integer instead of int here, even if the field is of type int.
| field_symbol.is_static_lifetime = true; | ||
| return field_symbol; | ||
| }()); | ||
| add_clinit(symbol_table, "TestClass"); |
There was a problem hiding this comment.
⛏️ Could save the return value to a variable here and use it as an argument to assign_from_json below.
| .get() | ||
| .get_identifier() == "symbol_to_assign"); | ||
| } | ||
| THEN("The instruction zero-initializes the struct") |
There was a problem hiding this comment.
⛏️ The code here checks for "initializes the struct" but doesn't check for "zero".
| .get() | ||
| .type() == java_reference_type(java_int_type())); | ||
| } | ||
| THEN("The instruction allocates the struct") |
There was a problem hiding this comment.
❓ Which struct? All this is checking for is an assignment to allocation_symbol.
| { | ||
| REQUIRE( | ||
| make_query(block)[7].as<code_assumet>()[0].get().type() == | ||
| bool_typet{}); |
There was a problem hiding this comment.
💡 Can we check what the assumptions for this are, rather than just check that they have boolean type?
There was a problem hiding this comment.
that's difficult to do in a robust manner because you can have different assumptions which are logically equivalent...
No functional changes
By keeping the iterator to the found entry.
This makes the assign_array_from_json a bit simpler. This is an intermediary commit towards removing the optional argument from assign_array_from_json.
This simplifies the logic in assign_array_from_json and makes its specification simpler.
This makes it so that we only have one block.add(code_assumet(...)) instruction, it is thus easier to figure out what the assumption is depending on the parameters.
romainbrenguier
force-pushed
the
refactor/assign-from-json
branch
from
b420f26 to
8d09d98
Compare
owen-mc-diffblue
requested review from
chrisr-diffblue,
kroening and
tautschnig
as code owners
Depending on whether the array has deterministic length or not. This will make it easier to allocate the array directly to the right size in the deterministic case.
When the array is not marked as nondet and is not a reference it can directly be allocated with the right size, which will allow constant propagation through arrays.
romainbrenguier
force-pushed
the
refactor/assign-from-json
branch
2 times, most recently
from
d42b140 to
14e1424
Compare
This in particular check that an array field (which is not marked nondet and not a reference) is allocated with a constant size.
romainbrenguier
force-pushed
the
refactor/assign-from-json
branch
from
14e1424 to
5829c8a
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 8d09d98).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128467148
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: d42b140).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128467475
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 14e1424).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128472197
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 5829c8a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128475220
These are refactoring commits apart from the last one, which does the actual change.
This makes array given by
--static-valuesbe directly allocated to the right size when they are not marked as@nondetLengthor references (marked with@refor@id).To fully implement TG-9450 the case of references still needs to be solved and it will be done in a separate PR.