Merge remote-tracking branch 'origin/master' into protz_cg

README.md

@@ -1,9 +1,9 @@
 KaRaMeL
 -------
 
-| Linux | Windows |
-|---------|-------|
-| [![Linux](https://msr-project-everest.visualstudio.com/Everest/_apis/build/status/Karamel/Karamel-Linux?branchName=master)](https://msr-project-everest.visualstudio.com/Everest/_build/latest?definitionId=38&branchName=master) | [![Windows](https://msr-project-everest.visualstudio.com/Everest/_apis/build/status/Karamel/Karamel-Windows?branchName=master)](https://msr-project-everest.visualstudio.com/Everest/_build/latest?definitionId=40&branchName=master) |
+| Linux  |
+|---------|
+| [![Build and Deploy](https://github.com/FStarLang/karamel/actions/workflows/linux-x64-hierarchic.yaml/badge.svg)](https://github.com/FStarLang/karamel/actions/workflows/linux-x64-hierarchic.yaml) |
 
 KaRaMeL (formerly known as KReMLin) is a tool that extracts an F\* program to
 readable C code: K&R meets ML!

dune-project

@@ -1,4 +1,4 @@
-(lang dune 3.7)
+(lang dune 3.5)
 (name karamel)
 (using menhir 2.0)
 

lib/Ast.ml

@@ -634,7 +634,7 @@ end
 (** More helpers *)
 
 let filter_decls f files =
-  List.map (fun (file, decls) -> file, KList.filter_map f decls) files
+  List.map (fun (file, decls) -> file, List.filter_map f decls) files
 
 let map_decls f files =
   List.map (fun (file, decls) -> file, List.map f decls) files

lib/AstToCFlat.ml

@@ -202,7 +202,7 @@ let align array_size pos =
 
 (* Helper *)
 let fields_of_struct =
-  List.map (fun (name, (t, _mut)) -> Option.must name, t)
+  List.map (fun (name, (t, _mut)) -> Option.get name, t)
 
 (* A TQualified can either be a struct or an enum. Same for TAnonymous. *)
 let is_enum env t =
@@ -537,9 +537,9 @@ let write_static (env: env) (lid: lident) (e: expr): string * CFlat.expr list =
         write_le dst ofs e.typ (Z.of_int (LidMap.find lid env.enums));
         []
     | EFlat fields ->
-        let layout = Option.must (layout_of env e) in
-        KList.map_flatten (fun (fname, e) ->
-          let fname = Option.must fname in
+        let layout = Option.get (layout_of env e) in
+        List.concat_map (fun (fname, e) ->
+          let fname = Option.get fname in
           let fofs = fst (List.assoc fname layout.fields) in
           write_scalar dst (ofs + fofs) e
         ) fields
@@ -607,7 +607,7 @@ let rec write_at (env: env)
             (* KPrint.bprintf "    >>> write_at: literal\n"; *)
             let locals, writes =
               fold (fun locals (fname, e) ->
-                let fname = Option.must fname in
+                let fname = Option.get fname in
                 let fofs = fst (List.assoc fname layout.fields) in
                 (* Recursively write each field of the struct at its offset. *)
                 write_at locals (ofs + fofs, e)
@@ -802,7 +802,7 @@ and mk_expr (env: env) (locals: locals) (e: expr): locals * CF.expr =
 
   | EAddrOf ({ node = EField (e1, f); _ }) ->
       (* This is the "address-of" operation from the paper. *)
-      let ofs = fst (List.assoc f (Option.must (layout_of env e1)).fields) in
+      let ofs = fst (List.assoc f (Option.get (layout_of env e1)).fields) in
       let locals, e1 = mk_expr env locals (with_type (TBuf (e1.typ, true)) (EAddrOf e1)) in
       locals, mk_add32 e1 (mk_uint32 ofs)
 
@@ -1021,7 +1021,7 @@ let mk_wrapper orig_name n_args locals =
   let args, locals = KList.split n_args locals in
   let body =
     CF.CastI64ToPacked (
-      CF.CallFunc (orig_name, KList.make (List.length args) (fun i -> CF.Var i))
+      CF.CallFunc (orig_name, List.init (List.length args) (fun i -> CF.Var i))
     )
   in
   CF.(Function { name; args; ret; locals; body; public = true })

lib/AstToCStar.ml

@@ -406,7 +406,7 @@ and mk_expr env in_stmt e =
       CStar.Cast (mk_expr env e, mk_type env t)
   | EAbort (t, s) ->
       let t = match t with Some t -> t | None -> e.typ in
-      CStar.EAbort (mk_type env t, Option.or_empty s)
+      CStar.EAbort (mk_type env t, Option.value ~default:"" s)
   | EUnit ->
       CStar.Cast (zero, CStar.Pointer CStar.Void)
   | EAny ->
@@ -631,7 +631,7 @@ and mk_stmts env e ret_type =
         fatal_error "[AstToCStar.collect EMatch]: not implemented"
 
     | EAbort (_, s) ->
-        env, CStar.Abort (Option.or_empty s) :: acc
+        env, CStar.Abort (Option.value ~default:"" s) :: acc
 
     | ESwitch (e, branches) ->
         let default, branches =

lib/AstToMiniRust.ml

@@ -35,7 +35,7 @@ module H = struct
     | _ -> None
 
   let wrapping_operator o =
-    Option.must (wrapping_operator_opt o)
+    Option.get (wrapping_operator_opt o)
 
   let is_wrapping_operator o =
     wrapping_operator_opt o <> None

lib/Builtin.ml

@@ -376,7 +376,7 @@ let make_abstract_function_or_global = function
  * - lets are replaced by vals
  * - but we keep the gte_mask and eq_mask functions *)
 let make_abstract (name, decls) =
-  name, KList.filter_map (function
+  name, List.map (function
     | DType (_, _, _, _, Abbrev _) as t ->
         Some t
     | DType _ ->
@@ -394,7 +394,7 @@ let make_abstract (name, decls) =
 (* Transforms an F* module that contains a model into a set of "assume val" that
  * will generate proper "extern" declarations in C. *)
 let make_library (name, decls) =
-  name, KList.filter_map make_abstract_function_or_global decls
+  name, List.filter_map make_abstract_function_or_global decls
 
 let is_model name =
   let is_machine_integer name =

lib/Bundle.ml

@@ -72,13 +72,13 @@ let pattern_matches (p: pat) (m: string) =
 
 (* For generating the filename. NOT for pretty-printing. *)
 let bundle_filename (api, patterns, attrs) =
-  match KList.find_opt (function Rename s -> Some s | _ -> None) attrs with
+  match List.find_map (function Rename s -> Some s | _ -> None) attrs with
   | Some s ->
       s
   | _ ->
       match api with
       | [] ->
-          String.concat "_" (KList.map_flatten (function
+          String.concat "_" (List.concat_map (function
             | Module m -> m
             | Prefix p -> p
           ) patterns)

lib/Bundles.ml

@@ -131,7 +131,7 @@ let direct_dependencies file_of file =
   let prepend lid =
     match file_of lid with
     | Some f when f <> fst file ->
-        let dep = (Option.must !current_decl, fst file, lid, f) in
+        let dep = (Option.get !current_decl, fst file, lid, f) in
         Hashtbl.replace deps f dep
     | _ ->
         ()

lib/CFlatToWasm.ml

@@ -625,10 +625,10 @@ let rec mk_callop2 env (w, o) e1 e2 =
   mk_expr env e2 @
   if is_binop (w, o) then
     mk_binop_conversion (w, o) @
-    [ dummy_phrase (W.Ast.Binary (mk_value size (Option.must (mk_binop (w, o))))) ] @
+    [ dummy_phrase (W.Ast.Binary (mk_value size (Option.get (mk_binop (w, o))))) ] @
     mk_mask w
   else if is_cmpop (w, o) then
-    [ dummy_phrase (W.Ast.Compare (mk_value size (Option.must (mk_cmpop (w, o))))) ] @
+    [ dummy_phrase (W.Ast.Compare (mk_value size (Option.get (mk_cmpop (w, o))))) ] @
     mk_mask w
   else
     failwith "todo mk_callop2"
@@ -779,7 +779,7 @@ and mk_expr env (e: expr): W.Ast.instr list =
       mk_expr env (CallFunc ("store64_le", [ e1; CallFunc ("WasmSupport_betole64", [ e2 ])]))
 
   | CallFunc (name, es) ->
-      KList.map_flatten (mk_expr env) es @
+      List.concat_map (mk_expr env) es @
       [ dummy_phrase (W.Ast.Call (mk_var (find_func env name))) ]
 
   | BufCreate (Common.Stack, n_elts, elt_size) ->
@@ -906,8 +906,8 @@ and mk_expr env (e: expr): W.Ast.instr list =
       [ dummy_phrase W.Ast.Unreachable ]
 
   | Switch (e, branches, default, s) ->
-      let vmax = KList.max (List.map (fun (c, _) -> Z.of_string (snd c)) branches) in
-      let vmin = KList.min (List.map (fun (c, _) -> Z.of_string (snd c)) branches) in
+      let vmax = KList.reduce max (List.map (fun (c, _) -> Z.of_string (snd c)) branches) in
+      let vmin = KList.reduce min (List.map (fun (c, _) -> Z.of_string (snd c)) branches) in
       if Z.( gt vmax ~$20 || lt vmin ~$0 ) then
         failwith "TODO: in AstToCFlat, don't pick Switch for matches on integers!";
 
@@ -1228,7 +1228,7 @@ let mk_module (name, decls): (string * W.Ast.module_) =
   (* Generate types for the function declarations. Re-establish the invariant
    * that the function at index i in the function index space has type i in the
    * types index space. *)
-  let types = imported_types @ KList.filter_map (function
+  let types = imported_types @ List.filter_map (function
     | Function f ->
         Some (mk_func_type f)
     | _ ->
@@ -1237,7 +1237,7 @@ let mk_module (name, decls): (string * W.Ast.module_) =
 
   (* Compile the functions. We assume all of the required functions have been
      inserted in env.funcs (ibid. globals) via the first pass. *)
-  let funcs = KList.filter_map (function
+  let funcs = List.filter_map (function
     | Function f ->
         begin try Some (mk_func (locate env (In f.name)) f) with
         | e ->
@@ -1316,7 +1316,7 @@ let mk_module (name, decls): (string * W.Ast.module_) =
   })] in
 
   (* Export all of the current module's functions & globals. *)
-  let exports = KList.filter_map (function
+  let exports = List.filter_map (function
     | Function { public; name; _ } when public ->
         Some (dummy_phrase W.Ast.({
           name = name_of_string name;

lib/CStarToC11.ml

@@ -430,7 +430,7 @@ and mk_alloc_cast m t e =
 and mk_malloc m t s =
   match t with
   | Qualified lid when Helpers.is_aligned_type lid ->
-      let sz = Option.must (mk_alignment m t) in
+      let sz = Option.get (mk_alignment m t) in
       mk_alloc_cast m t (C.Call (C.Name "KRML_ALIGNED_MALLOC", [ sz; mk_sizeof_mul m t s ]))
   | _ ->
       mk_alloc_cast m t (C.Call (C.Name "KRML_HOST_MALLOC", [ mk_sizeof_mul m t s ]))
@@ -790,7 +790,7 @@ and mk_stmt m (stmt: stmt): C.stmt list =
 
 
 and mk_stmts m stmts: C.stmt list =
-  let stmts = KList.map_flatten (mk_stmt m) stmts in
+  let stmts = List.concat_map (mk_stmt m) stmts in
   let rec fixup_c89 in_decls (stmts: C.stmt list) =
     match stmts with
     | C.Decl _ as stmt :: stmts ->
@@ -979,7 +979,7 @@ and mk_expr m (e: expr): C.expr =
   | Struct (typ, fields) ->
       if typ = None then
         failwith ("Expected a type annotation for: \n" ^ show_expr e);
-      let typ = Option.must typ in
+      let typ = Option.get typ in
       mk_compound_literal m typ fields
 
   | Field (BufRead (e, Constant (_, "0")), field) ->
@@ -998,7 +998,7 @@ and mk_expr m (e: expr): C.expr =
       Call (Name "KRML_EABORT", [ Type (mk_type m t); Literal (escape_string s) ])
 
   | Stmt s ->
-      Stmt (KList.map_flatten (mk_stmt m) s)
+      Stmt (List.concat_map (mk_stmt m) s)
 
   | Type t ->
       Type (mk_type m t)
@@ -1026,7 +1026,7 @@ and mk_type m t =
   mk_spec_and_declarator m "" t
 
 let mk_comments =
-  KList.filter_map (function
+  List.filter_map (function
     | Comment c when c <> "" ->
         Some c
     | _ ->
@@ -1038,15 +1038,15 @@ let wrap_verbatim lid flags d =
     [ Text (KPrint.bsprintf "/* SNIPPET_START: %s */" lid) ]
   else
     []) @
-  KList.filter_map (function
+  List.filter_map (function
     | Prologue s -> Some (Text s)
     | _ -> None
   ) flags @
-  KList.filter_map (function
+  List.filter_map (function
     | Deprecated s -> Some (Text (KPrint.bsprintf "KRML_DEPRECATED(\"%s\")" s))
     | _ -> None
   ) flags @
-  [ d ] @ KList.filter_map (function
+  [ d ] @ List.filter_map (function
     | Epilogue s -> Some (Text s)
     | _ -> None
   ) flags @
@@ -1230,7 +1230,7 @@ let mk_type_or_external m (w: where) ?(is_inline_static=false) (d: decl): C.decl
         let missing_names = List.length ts - List.length pp in
         let arg_names =
           if missing_names >= 0 then
-            pp @ KList.make missing_names (fun i -> KPrint.bsprintf "x%d" i)
+            pp @ List.init missing_names (fun i -> KPrint.bsprintf "x%d" i)
           else
             (* For functions that take a single unit argument, the name of the
              * unit is gone. *)
@@ -1331,7 +1331,7 @@ let mk_file m decls =
   (* In the C file, we put function bodies, global bodies, and type
    * definitions and external definitions that were private to the file only.
    * *)
-  KList.map_flatten
+  List.concat_map
     (if_header_inline_static m
       none
       (either
@@ -1351,7 +1351,7 @@ let mk_static f d =
     | Some NoInline -> Some NoInline
   in
 
-  KList.map_flatten (function
+  List.concat_map (function
     | C.Decl (comments, (qs, ts, inline, (None | Some (Static | Extern)), extra, decl_inits)) ->
         let is_func = match decl_inits with
           | [ Function _, _, _ ] -> promote_inline inline
@@ -1377,7 +1377,7 @@ let mk_public_header (m: GlobalNames.mapping) decls =
   (* Note that static_header + library means that corresponding declarations are
    * effectively dropped on the basis that the user is doing separate extraction
    * & compilation + providing the required header. *)
-  KList.map_flatten
+  List.concat_map
     (if_public (
       (if_header_inline_static m
         (mk_static (either (mk_function_or_global_body m) (mk_type_or_external m ~is_inline_static:true C)))
@@ -1386,7 +1386,7 @@ let mk_public_header (m: GlobalNames.mapping) decls =
 
 (* Private part if not already a static header, empty otherwise. *)
 let mk_internal_header (m: GlobalNames.mapping) decls =
-  KList.map_flatten
+  List.concat_map
     (if_internal (
       (if_header_inline_static m
         (mk_static (either (mk_function_or_global_body m) (mk_type_or_external m ~is_inline_static:true C)))

lib/Checker.ml

@@ -243,16 +243,16 @@ and check_fields_opt env fieldexprs fieldtyps =
   if List.length fieldexprs > List.length fieldtyps then
     checker_error env "some fields are superfluous (expr) in %a" pexpr (with_unit (EFlat fieldexprs));
   List.iter (fun (field, expr) ->
-    let field = Option.must field in
-    let t, _ = KList.assoc_opt field fieldtyps in
+    let field = Option.get field in
+    let t, _ = List.assoc (Some field) fieldtyps in
     check env t expr
   ) fieldexprs
 
 and check_fieldpats env fieldexprs fieldtyps =
   if List.length fieldexprs > List.length fieldtyps then
     checker_error env "some fields are superfluous (pat) in %a" ppat (with_unit (PRecord fieldexprs));
   List.iter (fun (field, expr) ->
-    let t, _ = KList.assoc_opt field fieldtyps in
+    let t, _ = List.assoc (Some field) fieldtyps in
     check_pat env t expr
   ) fieldexprs
 
@@ -825,7 +825,7 @@ and infer_and_check_eq: 'a. env -> ('a -> typ) -> 'a list -> typ =
     | Some t_base -> check_eqtype env t_base t
     | None -> t_base := Some t
   ) l;
-  Option.must !t_base
+  Option.get !t_base
 
 and find_field env t field =
   let t = expand_abbrev env t in
@@ -846,7 +846,7 @@ and find_field_from_def env def field =
     | Union fields ->
         List.assoc field fields, true (* owing to nocompound-literals which may mutate it *)
     | Flat fields ->
-        KList.assoc_opt field fields
+        List.assoc (Some field) fields
     | _ ->
         raise Not_found
   end with Not_found ->
@@ -892,7 +892,7 @@ and check_valid_path env e =
   match e.node with
   | EField (e, f) ->
       let t1 = check_valid_path env e in
-      fst (Option.must (find_field env t1 f))
+      fst (Option.get (find_field env t1 f))
 
   | EBufRead _
   | EBound _ ->