-
Notifications
You must be signed in to change notification settings - Fork 44
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix translation of atomic functions #685
Conversation
Previously we translated C-expressions possibly twice due to the optimization for pointer reads/writes and made everything atomic (to handle stdatomic functions). Now, we make sure that the expression is only translated once and we separate the ExpressionResult of the original expressions and the corresponding read/write, s.t. we can control the atomicity for stdatomic functions properly. Therefore we replaced the methods by an interface IPointerReadWrite (and matching implementations).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for making sure these functions work correctly!
I took a look, and it seems a good change. I was not able to check every atomic function in precise detail though. I left some comments on the general mechanism, mostly asking for documentation / explanation.
...g/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java
Outdated
Show resolved
Hide resolved
...g/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java
Outdated
Show resolved
Hide resolved
...g/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java
Outdated
Show resolved
Hide resolved
@maul-esel This interface was not really necessary, |
PR #657 added support for atomic functions. This had however two problems (in the current version):
__atomic_store_n(&x, 1, 5)
tox := 1
inside an atomic block rather thanwrite~(x, 1)
(see d08b25f and in the PR). This way the arguments were dispatched possibly multiple times, which is problematic if they have side-effects (see atomic_load_n_sideeffects.c).__atomic_store_n(&x, expr1, expr2)
only the actual write onx
is atomic, not the evaluation ofexpr1
orexpr2
. This could have led to missed data-races (see atomic_memory_order.c)__atomic_load
, but only the read should be atomic (fixed in f2e474d)To fix these issues, the PR adds an interfaceIPointerReadWrite
(and two implementations) that allows to get the dispatched argument, a read and a write separately (s.t. we can "control" the atomicity) and that guarantees that the dispatch is only done once. This interface is the used inStandardFunctionHandler
for the translation of atomic functions.To fix these issues, the PR adds three separate method to
ExpressionResultTransformer
:dispatchPointerLValue
to dispatch the pointer expression, but tries to produceLocalLValue
makePointerAssignment
writes to the given address, produces simple assignment forLocalLValue
and write-call forHeapLValue
readPointerValue
reads from the given address, always returns an aux-var asRValue
, assigns theLocalLValue
to the aux-var or reads to the aux-var from the memory forHeapLValue