ACSL: Improve handling of dereferences #703
Conversation
| final CType type = CEnum.replaceEnumWithInt(expr.getLrValue().getCType().getUnderlyingType()); | ||
| // Perform a custom switch to RValue without any read calls | ||
| // This allows us to use also dereferences inside ACSL expressions that have to be side-effect-free | ||
| // (e.g., loop invariant or contracts) |
There was a problem hiding this comment.
But this will now also be used for ACSL asserts, right?
There was a problem hiding this comment.
Yes, it will be used for any ACSL expression.
| final Expression memoryAccess = ExpressionFactory.constructNestedArrayAccessExpression(loc, | ||
| mCHandler.getMemoryArrayForType(type), new Expression[] { heapValue.getAddress() }); | ||
| return new ExpressionResultBuilder(expr).resetLrValue(new RValue(memoryAccess, type)).build(); | ||
| } |
There was a problem hiding this comment.
Do I understand correctly that this code replaces the calls to mExprResultTransformer.switchToRValue (and related methods) that were previously made?
If so, I am a bit unsure if this is a good place to have this. For instance, it could easily get out-of-sync with changes in switchToRValue. Would it be possible to make this a specialized method e.g. mExprResultTransformer.switchToRValueWithoutSideEffects?
There was a problem hiding this comment.
Do I understand correctly that this code replaces the calls to
mExprResultTransformer.switchToRValue(and related methods) that were previously made?
Yes, any call to mExprResultTransformer.switchToRValue in ACSLHandler was replaced with a call to this method.
If so, I am a bit unsure if this is a good place to have this. For instance, it could easily get out-of-sync with changes in
switchToRValue. Would it be possible to make this a specialized method e.g.mExprResultTransformer.switchToRValueWithoutSideEffects?
We cannot get completely out-of-sync, this method still has the call to mExprResultTransformer.switchToRValue as a base case (which does currently nothing, but if this changes, it will also be visible in this method).
We could also make it a public method in ExpressionResultTransformer, but this switchToRValue does not have any memsafety-checks (even if the setting is enabled). Therefore I am not sure, if it is a good idea to have such a public method in ExpressionResultTransformer.
|
I just added two test cases. The should actually pass, since the |
Perform the switch to RValue only in the internal method dispatchSwitch
schuessf
force-pushed
the
wip/fs/acsl-arrays
branch
from
97e14cd to
4915880
Compare
In our C translation, we translate dereferences to calls to Boogie procedures, e.g.,
x = a[i];is translated to:where
read~inthas the following signature (for memsafety we have a stronger contract):This read-call is produced by
ExpressionResultTransformer::switchToRValue.For ACSL, we attempted to handle this the same way as for C. There were however two problems:
ArrayAccessExpression, the call toswitchToRValuewas missing, which led to a crash (fixed in 07b75aa)//@ assert x == a[i];looks similar to above). There are however other ACSL statements / expressions, the translation with calls does not work, as it produces not only an expression, but also auxiliary statements (e.g., function contracts, loop invariants, quantifiers in the future). Therefore I replaced the read-call by an array-access in the corresponding memory-array (e.g.,#memory_int) when handling ACSL. This was implemented through a customswitchToRValuemethod inACSLHandler(see d0b8165).Note: Before this change, every dereference was translated to a read/write-call in Boogie, where the
MemorySlicerrelied on. Therefore, we now crash, on programs with ACSL dereferences, whenMemorySliceris used (We probably have to replace#memory_inteverywhere, not only in the contracts of the read/write-procedures). @Heizmann can you have a look at this issue?