Disallow signed int from bitvector reasoning

verus-lang · Jan 12, 2022 · 8fdd72f · 8fdd72f
1 parent 10e5a7c
commit 8fdd72f
Show file tree

Hide file tree

Showing 3 changed files with 56 additions and 7 deletions.
diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs
@@ -967,23 +967,62 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
                 BinOpKind::Shl => BinaryOp::Shl,
                 _ => unsupported_err!(expr.span, format!("binary operator {:?}", op)),
             };
-            let e = mk_expr(ExprX::Binary(vop, vlhs, vrhs));
             match op.node {
-                BinOpKind::Add | BinOpKind::Sub | BinOpKind::Mul => Ok(mk_ty_clip(&expr_typ(), &e)),
+                BinOpKind::Add | BinOpKind::Sub | BinOpKind::Mul => {
+                    let e = mk_expr(ExprX::Binary(vop, vlhs, vrhs));
+                    Ok(mk_ty_clip(&expr_typ(), &e))
+                }
                 BinOpKind::Div | BinOpKind::Rem => {
                     // TODO: disallow divide-by-zero in executable code?
                     match mk_range(tc.node_type(expr.hir_id)) {
                         IntRange::Int | IntRange::Nat | IntRange::U(_) | IntRange::USize => {
                             // Euclidean division
-                            Ok(e)
+                            Ok(mk_expr(ExprX::Binary(vop, vlhs, vrhs)))
                         }
                         IntRange::I(_) | IntRange::ISize => {
                             // Non-Euclidean division, which will need more encoding
                             unsupported_err!(expr.span, "div/mod on signed finite-width integers")
                         }
                     }
                 }
-                _ => Ok(e),
+                // disallow signed integers from bit shifting
+                // convert the signed constant on rhs to unsigned if it is 0 ~ 31.
+                BinOpKind::Shr | BinOpKind::Shl => match mk_range(tc.node_type(lhs.hir_id)) {
+                    IntRange::I(_) | IntRange::ISize => {
+                        unsupported_err!(expr.span, "bit shifting on a signed integer")
+                    }
+                    _ => {
+                        let width: u32;
+                        match mk_range(tc.node_type(rhs.hir_id)) {
+                            IntRange::ISize => width = (std::mem::size_of::<isize>() as u32) * 8,
+                            IntRange::I(n) => width = n,
+                            _ => return Ok(mk_expr(ExprX::Binary(vop, vlhs, vrhs))),
+                        };
+                        if width > 0 {
+                            if let ExprKind::Lit(lit) = &rhs.kind {
+                                if let rustc_ast::LitKind::Int(i, _) = lit.node {
+                                    if i < 32 {
+                                        let c = vir::ast::ExprX::Const(vir::ast::Constant::Nat(
+                                            Arc::new(i.to_string()),
+                                        ));
+                                        let vrhs = spanned_typed_new(
+                                            expr.span,
+                                            &Arc::new(TypX::Int(IntRange::U(width))),
+                                            c,
+                                        );
+                                        let e = mk_expr(ExprX::Binary(vop, vlhs, vrhs));
+                                        return Ok(e);
+                                    }
+                                }
+                            }
+                        };
+                        unsupported_err!(
+                            expr.span,
+                            "bit shifting with the amount of signed integer"
+                        )
+                    }
+                },
+                _ => Ok(mk_expr(ExprX::Binary(vop, vlhs, vrhs))),
             }
         }
         ExprKind::AssignOp(

diff --git a/source/vir/src/ast_util.rs b/source/vir/src/ast_util.rs
@@ -62,9 +62,6 @@ pub fn bitwidth_from_type(et: &Typ) -> Option<u32> {
     if let TypX::Int(IntRange::U(size)) = &**et {
         return Some(*size);
     }
-    if let TypX::Int(IntRange::I(size)) = &**et {
-        return Some(*size);
-    }
     return None;
 }
 

diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs
@@ -476,17 +476,30 @@ fn one_stmt(stmts: Vec<Stmt>) -> Stmt {
     if stmts.len() == 1 { stmts[0].clone() } else { Arc::new(StmtX::Block(Arc::new(stmts))) }
 }
 
+fn assert_unsigned(exp: &Exp) {
+    if let TypX::Int(range) = &*exp.typ {
+        match range {
+            IntRange::I(_) | IntRange::ISize => {
+                panic!("error: signed integer is not supported for bit-vector reasoning")
+            }
+            _ => (),
+        }
+    };
+}
+
 // convert the sst expression into bv air expression
 fn exp_to_bv_expr(state: &State, exp: &Exp) -> Expr {
     match &exp.x {
         ExpX::Const(crate::ast::Constant::Nat(s)) => {
+            assert_unsigned(exp);
             if let Some(width) = bitwidth_from_type(&exp.typ) {
                 // The width is needed when printing bv constants.
                 return Arc::new(ExprX::Const(Constant::BitVec(s.clone(), width)));
             }
             panic!("internal error: unable to get width from constant of type {:?}", exp.typ);
         }
         ExpX::Var(x) => {
+            assert_unsigned(exp);
             return string_var(&suffix_local_unique_id(x));
         }
         ExpX::Binary(op, lhs, rhs) => {