diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-14 21:33:39 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-15 14:00:52 -0500 |
| commit | b35af723c2416171ff10db47d7d3b301cd0baae7 (patch) | |
| tree | 6c190548ab91e04e7915a35d38ad862b20207c26 | |
| parent | 456cffcd2e808a3a9c3ff47f988138bbce555e0e (diff) | |
Ensure that we only left-shift on unsigned values
| -rw-r--r-- | src/CStringification.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/CStringification.v b/src/CStringification.v index b61421bc4..6aba9746f 100644 --- a/src/CStringification.v +++ b/src/CStringification.v @@ -1126,11 +1126,12 @@ Module Compilers. generate these things in the first place... - N.B. We must preserve signedness of the - value being shifted, because shift does - not commute with mod. *) + N.B. We make sure that we only + left-shift unsigned values, since + shifting into the sign bit is undefined + behavior. *) let rpre_out := match rout with - | Some rout => Some (int.union_zrange r[0~>2^offset] rout) + | Some rout => Some (int.union_zrange r[0~>2^offset] (int.unsigned_counterpart_of rout)) | None => Some (int.of_zrange_relaxed r[0~>2^offset]%zrange) end in let '(e', rin') := Zcast_up_if_needed rpre_out (e, rin) in |