Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 1f35599a authored by Xavier Leroy's avatar Xavier Leroy
Browse files

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
parent 3b448f59
......@@ -267,7 +267,7 @@ let bitfield_extract env bf carrier =
unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y)
unsigned int mask = ((1U << sz) - 1) << ofs;
return (x & ~mask) | ((y << ofs) & mask);
return ((y << ofs) & mask) | (x & ~mask);
If the bitfield is of type _Bool, the new value (y above) must be converted
......@@ -284,7 +284,7 @@ let bitfield_assign env bf carrier newval =
eshift env Oshl newval_casted (intconst (Int64.of_int bf.bf_pos) IUInt) in
let newval_masked = ebinint env Oand newval_shifted msk
and oldval_masked = ebinint env Oand carrier notmsk in
ebinint env Oor oldval_masked newval_masked
ebinint env Oor newval_masked oldval_masked
(* Initialize a bitfield *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment