Merge pull request #39 from AeneasVerif/afromher_shifts

Add support for bitshifts

4 files changed, 29 insertions, 11 deletions

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 85ab1112..73ccac44 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -786,7 +786,7 @@ let unop_name (unop : unop) : string =
     like [<]).
  *)
 let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
-  let binop =
+  let binop_s =
     match binop with
     | Div -> "div"
     | Rem -> "rem"
@@ -800,16 +800,14 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
     | BitXor -> "xor"
     | BitAnd -> "and"
     | BitOr -> "or"
-    | Shl -> "lsl"
-    | Shr ->
-        "asr"
-        (* NOTE: make sure arithmetic shift right is implemented, i.e. OCaml's asr operator, not lsr *)
+    | Shl -> "shl"
+    | Shr -> "shr"
     | _ -> raise (Failure "Unreachable")
   in
   (* Remark: the Lean case is actually not used *)
   match !backend with
-  | Lean -> int_name int_ty ^ "." ^ binop
-  | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop
+  | Lean -> int_name int_ty ^ "." ^ binop_s
+  | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop_s
 
 (** A list of keywords/identifiers used by the backend and with which we
     want to check collision.
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index ca9984be..3657627b 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -163,7 +163,7 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
   (match (!backend, binop) with
   | HOL4, (Eq | Ne)
   | (FStar | Coq | Lean), (Eq | Lt | Le | Ne | Ge | Gt)
-  | Lean, (Div | Rem | Add | Sub | Mul) ->
+  | Lean, (Div | Rem | Add | Sub | Mul | Shl | Shr | BitXor | BitOr | BitAnd) ->
       let binop =
         match binop with
         | Eq -> "="
@@ -177,7 +177,11 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
         | Add -> "+"
         | Sub -> "-"
         | Mul -> "*"
-        | _ -> raise (Failure "Unreachable")
+        | Shl -> "<<<"
+        | Shr -> ">>>"
+        | BitXor -> "^^^"
+        | BitOr -> "|||"
+        | BitAnd -> "&&&"
       in
       let binop =
         match !backend with FStar | Lean | HOL4 -> binop | Coq -> "s" ^ binop
@@ -188,8 +192,17 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
       F.pp_print_space fmt ();
       extract_expr false arg1
   | _ ->
+      let binop_is_shift = match binop with Shl | Shr -> true | _ -> false in
       let binop = named_binop_name binop int_ty in
       F.pp_print_string fmt binop;
+      (* In the case of F*, for shift operations, because machine integers
+         are simply integers with a refinement, if the second argument is a
+         constant we need to provide the second implicit type argument *)
+      if binop_is_shift && !backend = FStar && is_const arg1 then (
+        F.pp_print_space fmt ();
+        let ty = ty_as_integer arg1.ty in
+        F.pp_print_string fmt
+          ("#" ^ StringUtils.capitalize_first_letter (int_name ty)));
       F.pp_print_space fmt ();
       extract_expr true arg0;
       F.pp_print_space fmt ();
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index cc0580be..ac6c9ede 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -580,7 +580,10 @@ let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
             | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr ->
                 assert (int_ty1 = int_ty2);
                 TLiteral (TInteger int_ty1)
-            | Shl | Shr -> raise Unimplemented
+            | Shl | Shr ->
+                (* The number of bits can be of a different integer type
+                   than the operand *)
+                TLiteral (TInteger int_ty1)
             | Ne | Eq -> raise (Failure "Unreachable"))
         | _ -> raise (Failure "Invalid inputs for binop")
     in
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 4df3ee73..f5b055fd 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1755,7 +1755,11 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
         | [ arg0; arg1 ] ->
             let int_ty0 = ty_as_integer arg0.ty in
             let int_ty1 = ty_as_integer arg1.ty in
-            assert (int_ty0 = int_ty1);
+            (match binop with
+            (* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *)
+            | E.Shl | E.Shr -> ()
+            | _ -> assert (int_ty0 = int_ty1)
+            );
             let effect_info =
               {
                 can_fail = ExpressionsUtils.binop_can_fail binop;