diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-14 19:05:15 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-15 14:00:52 -0500 |
| commit | c61d5be86e3efb978883fc60687af42192aacaff (patch) | |
| tree | ea7da7858e1561490b8795d8e71b21819fca4319 /src/CStringification.v | |
| parent | 8faf6852f5bb36f5c663386f7dfbd0ae258445f9 (diff) | |
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
Diffstat (limited to 'src/CStringification.v')
| -rw-r--r-- | src/CStringification.v | 22 |
1 files changed, 16 insertions, 6 deletions
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')) |