From c61d5be86e3efb978883fc60687af42192aacaff Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 14 Jan 2019 19:05:15 -0500 Subject: Don't cast signed to unsigned before shifting Unfortunately, signed->unsigned casts do not commute with shifts. We take care to only extend the range when it needs extending, now. This was previously causing issues with subborrow. We should really get proofs about casts in C semantics at some point soon. Fixes #489 --- src/CStringification.v | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/CStringification.v b/src/CStringification.v index 45e0c2eb0..2321d3a3d 100644 --- a/src/CStringification.v +++ b/src/CStringification.v @@ -646,6 +646,9 @@ Module Compilers. Definition union (t1 t2 : type) : type := of_zrange_relaxed (ZRange.union (to_zrange t1) (to_zrange t2)). + Definition union_zrange (r : zrange) (t : type) : type + := of_zrange_relaxed (ZRange.union r (to_zrange t)). + Fixpoint base_interp (t : base.type) : Set := match t with | base.type.Z => type @@ -1100,8 +1103,12 @@ Module Compilers. behavior to shift >= width of the type. We should probably figure out how to not generate these things in the first - place... *) - let '(e', rin') := Zcast_up_if_needed (Some (int.of_zrange_relaxed r[0~>2^offset]%zrange)) (e, rin) in + place... + + N.B. We must preserve signedness of the + value being shifted, because shift does + not commute with mod. *) + let '(e', rin') := Zcast_up_if_needed (option_map (int.union_zrange r[0~>2^offset]%zrange) rin) (e, rin) in ret (cast_down_if_needed rout (Z_shiftr offset @@ e', rin')) | None => inr ["Invalid right-shift by a non-literal"]%string end @@ -1117,11 +1124,14 @@ Module Compilers. behavior to shift >= width of the type. We should probably figure out how to not generate these things in the first - place... *) - let rpre_out := int.of_zrange_relaxed r[0~>2^offset]%zrange in + place... + + N.B. We must preserve signedness of the + value being shifted, because shift does + not commute with mod. *) let rpre_out := match rout with - | Some rout => Some (ToString.C.int.union rout rpre_out) - | None => Some rpre_out + | Some rout => Some (int.union_zrange r[0~>2^offset] 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 ret (cast_down_if_needed rout (Z_shiftl offset @@ e', rin')) -- cgit v1.2.3