Merge pull request #75 from FStarLang/_taramana_shift

Require shift RHS to be uint32_t, allow any unsigned int LHS

Author: tahina-pro

src/pass/check.rs

@@ -278,9 +278,21 @@ impl<'a> Checker<'a> {
                         | BinOp::Sub
                         | BinOp::BitAnd
                         | BinOp::BitOr
-                        | BinOp::BitXor
-                        | BinOp::Shl
-                        | BinOp::Shr => check_eq(self),
+                        | BinOp::BitXor => check_eq(self),
+                        BinOp::Shl | BinOp::Shr => {
+                            let u32_ty: MaybeRc<Type> = TypeT::Int {
+                                signed: false,
+                                width: 32,
+                            }
+                            .with_loc(rhs.loc.clone())
+                            .into();
+                            if !env.vtype_eq(rhs_ty.clone().into(), u32_ty) {
+                                self.report(
+                                    format!("shift amount must be uint32_t, not {}", rhs_ty),
+                                    &rval.loc,
+                                )
+                            }
+                        }
                     }
                 }
             }

src/pass/elab.rs

@@ -247,9 +247,7 @@ impl<'a> Elaborator<'a> {
                     | BinOp::Implies
                     | BinOp::BitAnd
                     | BinOp::BitOr
-                    | BinOp::BitXor
-                    | BinOp::Shl
-                    | BinOp::Shr => {
+                    | BinOp::BitXor => {
                         if let Some(meet_type) = env.meet_type(lhs_ty.clone(), rhs_ty.clone()) {
                             if !env.vtype_eq(lhs_ty, meet_type.clone()) {
                                 cast_to(lhs, meet_type.clone().to_rc())
@@ -267,6 +265,17 @@ impl<'a> Elaborator<'a> {
                             );
                         }
                     }
+                    BinOp::Shl | BinOp::Shr => {
+                        let u32_ty: MaybeRc<Type> = TypeT::Int {
+                            signed: false,
+                            width: 32,
+                        }
+                        .with_loc(rhs.loc.clone())
+                        .into();
+                        if !env.vtype_eq(rhs_ty, u32_ty.clone()) {
+                            cast_to(rhs, u32_ty.to_rc())
+                        }
+                    }
                 }
             }
             ExprT::BoolLit(_) => {}

test/bitops.c

@@ -36,3 +36,15 @@ uint32_t test_shr(uint32_t a, uint32_t b)
 {
     return a >> b;
 }
+
+uint64_t test_shl64(uint64_t a, uint32_t b)
+    _requires(b < 64u)
+{
+    return a << b;
+}
+
+uint64_t test_shr64(uint64_t a, uint32_t b)
+    _requires(b < 64u)
+{
+    return a >> b;
+}