Merge branch 'son_traits' into son_traits_types

3 files changed, 50 insertions, 8 deletions

diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index e9391834..7d0845ed 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -100,6 +100,11 @@ type scalar_ty =
 | U64
 | U128
 
+let is_unsigned = function
+| Isize | I8 | I16 | I32 | I64 | I128 -> false
+| Usize | U8 | U16 | U32 | U64 | U128 -> true
+
+
 let scalar_min (ty : scalar_ty) : int =
   match ty with
   | Isize -> isize_min
@@ -162,6 +167,15 @@ let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
 let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
   mk_scalar ty (x * y)
 
+let scalar_lxor (#ty : scalar_ty { is_unsigned ty && ty <> Usize })
+    (x : scalar ty) (y : scalar ty) : scalar ty =
+  match ty with
+  | U8 -> FStar.UInt.logxor #8 x y
+  | U16 -> FStar.UInt.logxor #16 x y
+  | U32 -> FStar.UInt.logxor #32 x y
+  | U64 -> FStar.UInt.logxor #64 x y
+  | U128 -> FStar.UInt.logxor #128 x y
+
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
 // TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
@@ -258,7 +272,7 @@ let u32_add = scalar_add #U32
 let u64_add = scalar_add #U64
 let u128_add = scalar_add #U128
 
-/// Substraction
+/// Subtraction
 let isize_sub = scalar_sub #Isize
 let i8_sub = scalar_sub #I8
 let i16_sub = scalar_sub #I16
@@ -286,6 +300,13 @@ let u32_mul = scalar_mul #U32
 let u64_mul = scalar_mul #U64
 let u128_mul = scalar_mul #U128
 
+/// Logical operators, defined for unsigned types only, so far
+let u8_xor = scalar_lxor #U8
+let u16_xor = scalar_lxor #U16
+let u32_xor = scalar_lxor #U32
+let u64_xor = scalar_lxor #U64
+let u128_xor = scalar_lxor #U128
+
 (*** Range *)
 type range (a : Type0) = {
   start : a;
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index b1c65be9..91827a31 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -3,7 +3,6 @@
    the formatter everywhere...
 *)
 
-open Utils
 open Pure
 open PureUtils
 open TranslateCore
@@ -61,6 +60,11 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
     | Le -> "le"
     | Ge -> "ge"
     | Gt -> "gt"
+    | 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 *)
     | _ -> raise (Failure "Unreachable")
   in
   (* Remark: the Lean case is actually not used *)
@@ -445,14 +449,13 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
       F.pp_print_string fmt binop;
       F.pp_print_space fmt ();
       extract_expr false arg1
-  | _, (Lt | Le | Ge | Gt | Div | Rem | Add | Sub | Mul) ->
+  | _ ->
       let binop = named_binop_name binop int_ty in
       F.pp_print_string fmt binop;
       F.pp_print_space fmt ();
       extract_expr true arg0;
       F.pp_print_space fmt ();
-      extract_expr true arg1
-  | _, (BitXor | BitAnd | BitOr | Shl | Shr) -> raise Unimplemented);
+      extract_expr true arg1);
   if inside then F.pp_print_string fmt ")"
 
 let type_decl_kind_to_qualif (kind : decl_kind)
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 5e849ba7..1273f57d 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -58,6 +58,24 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
     let can_diverge = ref false in
     let is_rec = ref false in
 
+    (* We have some specialized knowledge of some library functions; we don't
+       have any more custom treatment than this, and these functions can be modeled
+       suitably in Primitives.fst, rather than special-casing for them all the
+       way. *)
+    let module M = struct type opaque_info = { fallible: bool; stateful: bool } end in
+    let open M in
+    let opaque_info (f: fun_decl) =
+      match f.name with
+      | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "wrapping_add" ]
+      | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "rotate_left" ] ->
+          { fallible = false; stateful = false }
+      | _ ->
+          (* Opaque function: we consider they fail by default *)
+          { fallible = true; stateful = true }
+    in
+
+    (* JP: Why not use a reduce visitor here with a tuple of the values to be
+       computed? *)
     let visit_fun (f : fun_decl) : unit =
       let obj =
         object (self)
@@ -108,9 +126,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
       assert ((not f.is_global_decl_body) || not !stateful);
       match f.body with
       | None ->
-          (* Opaque function: we consider they fail by default *)
-          obj#may_fail true;
-          stateful := (not f.is_global_decl_body) && use_state
+          let info = opaque_info f in
+          obj#may_fail info.fallible;
+          stateful := (not f.is_global_decl_body) && use_state && info.stateful
       | Some body -> obj#visit_statement () body.body
     in
     List.iter visit_fun d;