diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-05-02 19:19:12 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-05-02 19:19:12 +0200 |
commit | 1f35599abe1b82f565a9a1b1ee03f60df362f22d (patch) | |
tree | 09d7dab28169a68600e54149e3575c79247cdc4f /powerpc/Stacklayout.v | |
parent | 3b448f597344109183c2436d477deed0ed820d6f (diff) | |
download | compcert-1f35599abe1b82f565a9a1b1ee03f60df362f22d.tar.gz compcert-1f35599abe1b82f565a9a1b1ee03f60df362f22d.zip |
Fix evaluation order in emulation of bitfield assignment
A bitfield assignment `x.b = f()` is expanded into a read-modify-write
on `x.carrier`. Wrong results can occur if `x.carrier` is read before
the call to `f()`, and `f` itself modifies a bitfield with the same
carrier `x.carrier`.
In this temporary fix, we play on the evaluation order implemented by
the SimplExpr pass of CompCert (left-to-right for side-effecting
subexpression) to make sure the read part of the read-modify-write
sequence occurs after the evaluation of the right-hand side.
More substantial fixes will be considered later.
Fixes: #395
Diffstat (limited to 'powerpc/Stacklayout.v')
0 files changed, 0 insertions, 0 deletions