Invariant cleanup in flattening/boolbv_index #3044
Conversation
hannes-steffenhagen-diffblue
requested review from
kroening,
martin-cs,
peterschrammel and
tautschnig
as code owners
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: c91b88b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85891642
|
|
||
| if(array_size*width!=array_bv.size()) | ||
| throw "unexpected array size"; | ||
| DATA_INVARIANT( |
There was a problem hiding this comment.
Make that a second argument to convert_bv?
| @@ -256,7 +256,7 @@ bvt boolbvt::convert_index(const index_exprt &expr) | |||
|
|
|||
| typet constant_type=index.type(); // type of index operand | |||
|
|
|||
| assert(array_size>0); | |||
There was a problem hiding this comment.
My only request is perhaps a better error message here? This shows what's going on, but not why. But I'm not too fussed about it to be honest.
hannes-steffenhagen-diffblue
force-pushed
the
feature-invariant_cleanup-flattening-index
branch
from
c91b88b to
be2046d
Compare
|
@NlightNFotis @tautschnig I believe I've addresses your comments, can you re-review once CI passes? |
| @@ -62,7 +62,7 @@ bvt boolbvt::convert_index(const index_exprt &expr) | |||
|
|
|||
| // Must have a finite size | |||
| mp_integer array_size = numeric_cast_v<mp_integer>(array_type.size()); | |||
|
|
|||
| PRECONDITION(array_size.is_ulong()); | |||
There was a problem hiding this comment.
I'd not use this. See below.
|
|
||
| if(array_size*width!=array_bv.size()) | ||
| throw "unexpected array size"; | ||
| const bvt &array_bv = convert_bv(array, array_size.to_ulong() * width); |
There was a problem hiding this comment.
Please use numeric_cast_v<std::size_t>(array_size * width) as it will 1) make sure there is no risk for overflow in the multiplication, 2) combine the check and the conversion, and 3) hide the implementation detail that bigint/.to_ulong is.
| assert(array_size>0); | ||
| DATA_INVARIANT( | ||
| array_size > 0, | ||
| "non-positive array sizes are forbidden by the C standard"); |
There was a problem hiding this comment.
This isn't about C code anymore, so we should talk about goto programs, not C code.
There was a problem hiding this comment.
We wrote this error message because we thought that goto-programs essentially model C semantics. It seems our assumption is wrong.
There was a problem hiding this comment.
Will it be okay to change it to something like "non-positive array sizes are not allowed in goto-programs"? The only problem is that I also feel kind of uneasy not being able to point to a formal standard regarding semantics like that, no matter how self-evident or obvious it might seem. Thoughts @tautschnig ?
There was a problem hiding this comment.
Historically goto-programs and C semantics have been very close, but we are trying to get this disentangled (after all a considerable business is coming from the Java front-end :-) ). I understand your sentiment, and one day we'll hopefully get goto-program semantics documented. Please use the updated message that you suggested.
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: be2046d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86029785
hannes-steffenhagen-diffblue
force-pushed
the
feature-invariant_cleanup-flattening-index
branch
from
be2046d to
1bc88a3
Compare
Also use the expected_width parameter to move one check into convert_bv
hannes-steffenhagen-diffblue
force-pushed
the
feature-invariant_cleanup-flattening-index
branch
from
1bc88a3 to
7baf62d
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 7baf62d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86129076
|
@tautschnig This has been fixed, and all CI checks now pass. Can you check if it's okay now, so that I can merge it if it is? |
Uh oh!
There was an error while loading. Please reload this page.