From b35af723c2416171ff10db47d7d3b301cd0baae7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 14 Jan 2019 21:33:39 -0500 Subject: Ensure that we only left-shift on unsigned values As per https://github.com/mit-plv/fiat-crypto/pull/490/files#r247737121 --- src/CStringification.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'src') 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 -- cgit v1.2.3