From c27c3052ec3f9a093b06a41f56b3a361cb65e950 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Sun, 22 Oct 2023 16:34:46 -0700
Subject: Add more support for numeric operations, xor, rotate

---
 compiler/Extract.ml      | 11 +++++++----
 compiler/FunsAnalysis.ml | 24 +++++++++++++++++++++---
 2 files changed, 28 insertions(+), 7 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index ac81d6f3..b842aea1 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 *)
@@ -498,14 +502,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 f4406653..f8aa06dc 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;
-- 
cgit v1.2.3