Add definitions to Primitives.fst and start on improving/fixing the

generated F* file

6 files changed, 56 insertions, 49 deletions

diff --git a/src/Assumed.ml b/src/Assumed.ml
index 5a9fb51b..527b2395 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -227,37 +227,54 @@ module Sig = struct
   let vec_index_mut_sig : A.fun_sig = vec_index_gen_sig true
 end
 
-(** The list of assumed functions, and their signatures.
+type assumed_info = A.assumed_fun_id * A.fun_sig * bool * Identifiers.name
+
+(** The list of assumed functions and all their information:
+    - their signature
+    - a boolean indicating whether they are monadic or not (i.e., if they
+      can fail or not)
+    - their name
 
     Rk.: following what is written above, we don't include `Box::free`.
+    
+    Remark about the vector functions: for `Vec::len` to be correct and return
+    a `usize`, we have to make sure that vectors are bounded by the max usize.
+    Followingly, `Vec::push` is monadic.
  *)
-let assumed_sigs : (A.assumed_fun_id * A.fun_sig) list =
+let assumed_infos : assumed_info list =
+  let deref_pre = [ "core"; "ops"; "deref" ] in
+  let vec_pre = [ "alloc"; "vec"; "Vec" ] in
+  let index_pre = [ "core"; "ops"; "index" ] in
   [
-    (Replace, Sig.mem_replace_sig);
-    (BoxNew, Sig.box_new_sig);
-    (BoxDeref, Sig.box_deref_shared_sig);
-    (BoxDerefMut, Sig.box_deref_mut_sig);
-    (VecNew, Sig.vec_new_sig);
-    (VecPush, Sig.vec_push_sig);
-    (VecInsert, Sig.vec_insert_sig);
-    (VecLen, Sig.vec_len_sig);
-    (VecIndex, Sig.vec_index_shared_sig);
-    (VecIndexMut, Sig.vec_index_mut_sig);
+    (Replace, Sig.mem_replace_sig, false, [ "core"; "mem"; "replace" ]);
+    (BoxNew, Sig.box_new_sig, false, [ "alloc"; "boxed"; "Box"; "new" ]);
+    (BoxDeref, Sig.box_deref_shared_sig, false, deref_pre @ [ "Deref"; "deref" ]);
+    ( BoxDerefMut,
+      Sig.box_deref_mut_sig,
+      false,
+      deref_pre @ [ "DerefMut"; "deref_mut" ] );
+    (VecNew, Sig.vec_new_sig, false, vec_pre @ [ "new" ]);
+    (VecPush, Sig.vec_push_sig, true, vec_pre @ [ "push" ]);
+    (VecInsert, Sig.vec_insert_sig, true, vec_pre @ [ "insert" ]);
+    (VecLen, Sig.vec_len_sig, false, vec_pre @ [ "len" ]);
+    (VecIndex, Sig.vec_index_shared_sig, true, index_pre @ [ "Index"; "index" ]);
+    ( VecIndexMut,
+      Sig.vec_index_mut_sig,
+      true,
+      index_pre @ [ "IndexMut"; "index_mut" ] );
   ]
 
+let get_assumed_info (id : A.assumed_fun_id) : assumed_info =
+  List.find (fun (id', _, _, _) -> id = id') assumed_infos
+
 let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig =
-  snd (List.find (fun (id', _) -> id = id') assumed_sigs)
+  let _, sg, _, _ = get_assumed_info id in
+  sg
 
-let assumed_names : (A.assumed_fun_id * Identifiers.name) list =
-  [
-    (Replace, [ "core"; "mem"; "replace" ]);
-    (BoxNew, [ "alloc"; "boxed"; "Box"; "new" ]);
-    (BoxDeref, [ "core"; "ops"; "deref"; "Deref"; "deref" ]);
-    (BoxDerefMut, [ "core"; "ops"; "deref"; "DerefMut"; "deref_mut" ]);
-    (VecNew, [ "alloc"; "vec"; "Vec"; "new" ]);
-    (VecPush, [ "alloc"; "vec"; "Vec"; "push" ]);
-    (VecInsert, [ "alloc"; "vec"; "Vec"; "insert" ]);
-    (VecLen, [ "alloc"; "vec"; "Vec"; "len" ]);
-    (VecIndex, [ "core"; "ops"; "index"; "Index"; "index" ]);
-    (VecIndexMut, [ "core"; "ops"; "index"; "IndexMut"; "index_mut" ]);
-  ]
+let get_assumed_name (id : A.assumed_fun_id) : Identifiers.name =
+  let _, _, _, name = get_assumed_info id in
+  name
+
+let assumed_is_monadic (id : A.assumed_fun_id) : bool =
+  let _, _, b, _ = get_assumed_info id in
+  b
diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml
index 902156f2..6a2f680a 100644
--- a/src/CfimAstUtils.ml
+++ b/src/CfimAstUtils.ml
@@ -23,21 +23,13 @@ let lookup_fun_sig (fun_id : fun_id) (fun_defs : fun_def FunDefId.Map.t) :
     fun_sig =
   match fun_id with
   | Local id -> (FunDefId.Map.find id fun_defs).signature
-  | Assumed aid ->
-      let _, sg =
-        List.find (fun (aid', _) -> aid = aid') Assumed.assumed_sigs
-      in
-      sg
+  | Assumed aid -> Assumed.get_assumed_sig aid
 
 let lookup_fun_name (fun_id : fun_id) (fun_defs : fun_def FunDefId.Map.t) :
     Identifiers.name =
   match fun_id with
   | Local id -> (FunDefId.Map.find id fun_defs).name
-  | Assumed aid ->
-      let _, sg =
-        List.find (fun (aid', _) -> aid = aid') Assumed.assumed_names
-      in
-      sg
+  | Assumed aid -> Assumed.get_assumed_name aid
 
 (** Small utility: list the transitive parents of a region var group.
     We don't do that in an efficient manner, but it doesn't matter.
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 5ac2af4e..99598937 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -48,6 +48,8 @@ type config = {
           See the comments for [expression_contains_child_call_in_all_paths]
           for additional explanations.
        *)
+  add_unit_args : bool;
+      (** Add unit input arguments to functions with no arguments. *)
 }
 (** A configuration to control the application of the passes *)
 
@@ -615,16 +617,15 @@ let filter_if_backward_with_no_outputs (def : fun_def) : fun_def option =
   if Option.is_some def.back_id && def.signature.outputs = [] then None
   else Some def
 
-(** Add unit arguments for functions with no arguments, and change their return type *)
-let to_monadic (def : fun_def) : fun_def =
+(** Add unit arguments (optionally) for functions with no arguments, and change their return type *)
+let to_monadic (add_unit_args : bool) (def : fun_def) : fun_def =
   (* Update the body *)
   let obj =
     object
       inherit [_] map_expression as super
 
       method! visit_call env call =
-        (* If no arguments, introduce unit *)
-        if call.args = [] then
+        if call.args = [] && add_unit_args then
           let args = [ mk_value_expression unit_rvalue None ] in
           { call with args } (* Otherwise: nothing to do *)
         else super#visit_call env call
@@ -635,7 +636,7 @@ let to_monadic (def : fun_def) : fun_def =
 
   (* Update the signature: first the input types *)
   let def =
-    if def.inputs = [] then (
+    if def.inputs = [] && add_unit_args then (
       assert (def.signature.inputs = []);
       let signature = { def.signature with inputs = [ unit_ty ] } in
       let var_cnt = get_expression_min_var_counter def.body.e in
@@ -858,7 +859,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
        * **Rk.**: from now onwards, the types in the AST are correct (until now,
        * functions had return type `t` where they should have return type `result t`).
        * Also, from now onwards, the outputs list has length 1. x*)
-      let def = to_monadic def in
+      let def = to_monadic config.add_unit_args def in
       log#ldebug (lazy ("to_monadic:\n\n" ^ fun_def_to_string ctx def ^ "\n"));
 
       (* Convert the unit variables to `()` if they are used as right-values or
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 1967732d..ca214d7c 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -913,11 +913,7 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) : S.call * V.abs list =
 let fun_is_monadic (fun_id : A.fun_id) : bool =
   match fun_id with
   | A.Local _ -> true
-  | A.Assumed
-      ( A.Replace | A.BoxNew | BoxDeref | BoxDerefMut | BoxFree | VecNew
-      | VecPush | VecLen ) ->
-      false
-  | A.Assumed (A.VecInsert | VecIndex | VecIndexMut) -> true
+  | A.Assumed aid -> Assumed.assumed_is_monadic aid
 
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   match e with
diff --git a/src/Translate.ml b/src/Translate.ml
index 028114cf..913c5cf8 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -227,9 +227,9 @@ let translate_module_to_pure (config : C.partial_config)
   (* Translate all the function *signatures* *)
   let assumed_sigs =
     List.map
-      (fun (id, sg) ->
+      (fun (id, sg, _, _) ->
         (A.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg))
-      Assumed.assumed_sigs
+      Assumed.assumed_infos
   in
   let local_sigs =
     List.map
diff --git a/src/main.ml b/src/main.ml
index 193b20c2..5e652809 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -142,6 +142,7 @@ let () =
           Micro.decompose_monadic_let_bindings = !decompose_monads;
           unfold_monadic_let_bindings = !unfold_monads;
           filter_unused_monadic_calls = !filter_unused_calls;
+          add_unit_args = false;
         }
       in
       Translate.translate_module filename dest_dir config micro_passes_config