Merge branch 'master' of github.com:FStarLang/karamel into _taramana_mutrec

Author: tahina-pro

include/krml/internal/target.h

@@ -46,8 +46,9 @@ typedef double float64_t;
 #  define KRML_HOST_PRINTF printf
 #endif
 
-#if (                                                                          \
-    (defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) &&             \
+#if (                                                                   \
+    ((defined(__cplusplus) && __cplusplus > 199711L) ||                 \
+     (defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L)) &&    \
     (!(defined KRML_HOST_EPRINTF)))
 #  define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
 #elif !(defined KRML_HOST_EPRINTF) && defined(_MSC_VER)

include/krml/lowstar_endianness.h

@@ -12,7 +12,7 @@
 /******************************************************************************/
 
 /* ... for Linux */
-#if defined(__linux__) || defined(__CYGWIN__) || defined (__USE_SYSTEM_ENDIAN_H__) || defined(__GLIBC__)
+#if defined(__linux__) || defined(__CYGWIN__) || defined (__USE_SYSTEM_ENDIAN_H__) || defined(__GLIBC__) || defined(ESP_PLATFORM)
 #  include <endian.h>
 
 /* ... for OSX */

lib/AstToMiniRust.ml

@@ -273,25 +273,47 @@ module Splits = struct
   (* Unlocks better comparisons in many cases *)
   let norm e =
     let exception NotConstant in
-    let rec norm (e: MiniRust.expr) =
+    let rec is_zero e =
+      try norm e = 0
+      with NotConstant -> false
+
+    and norm (e: MiniRust.expr) =
       (* This function assumes no overflow on index comparisons... FIXME *)
       match e with
       | As (e, _) ->
           norm e
+
+      | MethodCall (e1, [ "wrapping_add" ], [ e2 ])
+      | Call (Operator (Add | AddW), _, [ e1; e2 ]) when is_zero e1 ->
+          norm e2
+
+      | MethodCall (e1, [ "wrapping_add" ], [ e2 ])
+      | Call (Operator (Add | AddW), _, [ e1; e2 ]) when is_zero e2 ->
+          norm e1
+
       | MethodCall (e1, [ "wrapping_add" ], [ e2 ])
       | Call (Operator (Add | AddW), _, [ e1; e2 ]) ->
           norm e1 + norm e2
+
+      | MethodCall (e1, [ "wrapping_mul" ], [ e2 ])
+      | Call (Operator (Mult | MultW), _, [ e1; e2 ]) when is_zero e1 || is_zero e2 ->
+          0
+
       | MethodCall (e1, [ "wrapping_mul" ], [ e2 ])
       | Call (Operator (Mult | MultW), _, [ e1; e2 ]) ->
           norm e1 * norm e2
+
       | MethodCall (e1, [ "wrapping_sub" ], [ e2 ])
       | Call (Operator (Sub | SubW), _, [ e1; e2 ]) ->
           norm e1 - norm e2
+
       | MethodCall (e1, [ "wrapping_div" ], [ e2 ])
       | Call (Operator (Div | DivW), _, [ e1; e2 ]) ->
           norm e1 / norm e2
+
       | Constant (_, c) ->
           int_of_string c
+
       | _ ->
           raise NotConstant
     in
@@ -650,9 +672,9 @@ let field_type env (e: Ast.expr) f =
   [fn_t_ret] corresponds to the return type of the function we are currently
   translating, and is used for EReturn nodes.
    *)
-let rec translate_expr (env: env) (fn_t_ret: MiniRust.typ) (e: Ast.expr) : env * MiniRust.expr =
+let rec translate_expr (env: env) ?context (fn_t_ret: MiniRust.typ) (e: Ast.expr) : env * MiniRust.expr =
   (* KPrint.bprintf "translate_expr: %a : %a\n" PrintAst.Ops.pexpr e PrintAst.Ops.ptyp e.typ; *)
-  translate_expr_with_type env fn_t_ret e (translate_type env e.typ)
+  translate_expr_with_type env ?context fn_t_ret e (translate_type env e.typ)
 
 and translate_expr_list (env: env) (fn_t_ret: MiniRust.typ) (es: Ast.expr list) : env * MiniRust.expr list =
   let env, acc =
@@ -697,7 +719,7 @@ and translate_array (env: env) (fn_t_ret: MiniRust.typ) is_toplevel (init: Ast.e
 
 (* However, generally, we will have a type provided by the context that may
    necessitate the insertion of conversions *)
-and translate_expr_with_type (env: env) (fn_t_ret: MiniRust.typ) (e: Ast.expr) (t_ret: MiniRust.typ): env * MiniRust.expr =
+and translate_expr_with_type (env: env) ?(context=`Other) (fn_t_ret: MiniRust.typ) (e: Ast.expr) (t_ret: MiniRust.typ): env * MiniRust.expr =
   (* KPrint.bprintf "translate_expr_with_type: %a @@ %a\n" PrintMiniRust.ptyp t_ret PrintAst.Ops.pexpr e; *)
 
   let erase_borrow_kind_info = (object(self)
@@ -732,10 +754,16 @@ and translate_expr_with_type (env: env) (fn_t_ret: MiniRust.typ) (e: Ast.expr) (
         Constant (SizeT, x)
     | _, Constant UInt32, Constant SizeT ->
         As (x, Constant SizeT)
+
     | _, Function (_, _, ts, t), Function (_, _, ts', t') when ts = ts' && t = t' ->
         (* The type annotations coming from Ast do not feature polymorphic binders in types, but we
            do retain them in our Function type -- so we need to relax the comparison here *)
-        x
+        begin match e.node with
+        | EQualified _ when context <> `CallHead ->
+            As (x, t_ret)
+        | _ ->
+            x
+        end
 
     (* More conversions due to box-ing types. *)
     | _, Ref (_, _, Slice _), App (Name (["Box"], _), [Slice _]) ->
@@ -850,9 +878,12 @@ and translate_expr_with_type (env: env) (fn_t_ret: MiniRust.typ) (e: Ast.expr) (
   | EAny -> failwith "Unexpected EAny"
   | EAbort (_, s) ->
       env, Panic (Stdlib.Option.value ~default:"" s)
-  | EIgnore _ ->
-      failwith "unexpected: EIgnore"
-  | EApp ({ node = EOp (o, _); _ }, es) when H.is_wrapping_operator o ->
+  | EIgnore e ->
+      let t = translate_type env e.typ in
+      let env, e = translate_expr env fn_t_ret e in
+      let binding: MiniRust.binding = { name = "_"; typ = t; mut = false; ref = false } in
+      env, Let (binding, Some e, Unit)
+  | EApp ({ node = EOp (o, w); _ }, es) when H.is_wrapping_operator o && not (Constant.is_float w) ->
       let w = Helpers.assert_tint (List.hd es).typ in
       let env, es = translate_expr_list env fn_t_ret es in
       env, possibly_convert (MethodCall (List.hd es, [ H.wrapping_operator o ], List.tl es)) (Constant w)
@@ -915,7 +946,7 @@ and translate_expr_with_type (env: env) (fn_t_ret: MiniRust.typ) (e: Ast.expr) (
         | [ { typ = TUnit; node; _ } ] -> assert (node = EUnit); []
         | _ -> es
       in
-      let env, e = translate_expr env fn_t_ret e in
+      let env, e = translate_expr env ~context:`CallHead fn_t_ret e in
       let ts = List.map (translate_type env) ts in
       let env, es = translate_expr_list env fn_t_ret es in
       env, Call (e, ts, es)
@@ -934,7 +965,7 @@ and translate_expr_with_type (env: env) (fn_t_ret: MiniRust.typ) (e: Ast.expr) (
         | _ -> es, snd (Helpers.flatten_arrow e0.typ)
       in
       (* KPrint.bprintf "Translating arguments to call %a\n" PrintAst.Ops.pexpr e0; *)
-      let env, e0 = translate_expr env fn_t_ret e0 in
+      let env, e0 = translate_expr env ~context:`CallHead fn_t_ret e0 in
       let env, es = translate_expr_list_with_types env fn_t_ret es (List.map (translate_type env) ts) in
       env, possibly_convert (Call (e0, [], es)) (translate_type env e.typ)
 
@@ -1072,6 +1103,7 @@ and translate_expr_with_type (env: env) (fn_t_ret: MiniRust.typ) (e: Ast.expr) (
          sub-environments since their variables go out of scope? *)
       env, IfThenElse (e1, e2, e3)
   | ESequence _ ->
+      (* `sequence_to_let` eliminates all sequences *)
       failwith "unexpected: ESequence"
   | EAssign (e1, e2) ->
       let lvalue_type = match e1.node with
@@ -1346,7 +1378,12 @@ and translate_pat env (p: Ast.pattern): MiniRust.pat =
       ) field_names pats)
   | PUnit -> failwith "TODO: PUnit"
   | PBool _ -> failwith "TODO: PBool"
-  | PEnum _ -> failwith "TODO: PEnum"
+  | PEnum cons ->
+      (* Same as constructors, above, since enums and variants are the same in Rust (`enum`
+         keyword). *)
+      let lid = Helpers.assert_tlid p.typ in
+      let name = lookup_type env lid in
+      StructP (`Variant (name, snd cons), [])
   | PTuple ps ->
       TupleP (List.map (translate_pat env) ps)
   | PDeref _ -> failwith "TODO: PDeref"
@@ -1370,7 +1407,20 @@ let is_handled_primitively = function
 
 (* In Rust, like in C, all the declarations from the current module are in
  * scope immediately. This requires us to duplicate a little bit of work. *)
-let bind_decl env (d: Ast.decl): env =
+let bind_type_decl env (d: Ast.decl): env =
+  match d with
+  | DType (lid, _flags, _, _, _decl) ->
+      if LidMap.mem lid env.types then
+        (* Name already assigned thanks to a forward declaration *)
+        env
+      else
+        let env, name = translate_lid env lid in
+        let env = push_type env lid name in
+        env
+  | _ ->
+      env
+
+let bind_non_type_decl env (d: Ast.decl): env =
   match d with
   | DFunction (_, _, _, _, _, lid, _, _) when is_handled_primitively lid ->
       env
@@ -1429,17 +1479,9 @@ let bind_decl env (d: Ast.decl): env =
       let name = translate_unknown_lid lid in
       push_decl env lid (name, make_poly (translate_type_with_config env {default_config with keep_mut = true} t) type_parameters)
 
-  | DType (lid, _flags, _, _, decl) ->
-      let env, name =
-        if LidMap.mem lid env.types then
-          (* Name already assigned thanks to a forward declaration *)
-          env, lookup_type env lid
-        else
-          let env, name = translate_lid env lid in
-          let env = push_type env lid name in
-          env, name
-      in
-      match decl with
+  | DType (lid, _, _, _, decl) ->
+      let name = lookup_type env lid in
+      begin match decl with
       | Flat fields ->
           (* These sets are mutually exclusive, so we don't box *and* introduce a
              lifetime at the same time *)
@@ -1454,6 +1496,8 @@ let bind_decl env (d: Ast.decl): env =
           in
           let fields = List.map (fun (f, (t, _m)) ->
             let f = Option.get f in
+            (* let open PrintAst.Ops in *)
+            (* KPrint.bprintf "%a: field %s has type %a\n" plid lid f ptyp t; *)
             { MiniRust.name = f; visibility = Some Pub; typ = translate_type_with_config env { box; lifetime; keep_mut = false } t }
           ) fields in
           { env with
@@ -1479,6 +1523,7 @@ let bind_decl env (d: Ast.decl): env =
           ) env branches
       | _ ->
           env
+      end
 
 let translate_meta attributes flags =
   let comments = List.filter_map (function Common.Comment c -> Some c | _ -> None) flags in
@@ -1595,7 +1640,11 @@ let translate_decl env { derives; attributes; static; no_mangle; _ } (d: Ast.dec
       | Enum idents ->
           (* TODO: enum cases with set values *)
           (* No need to do name binding here since there are entirely resolved via the type name. *)
-          let items = List.map (fun (i, v) -> assert (v = None); snd i, None) idents in
+          let items = List.map (fun (i, (v: Z.t option)) ->
+            snd i, match v with
+            | None -> MiniRust.Unit None
+            | Some c -> Unit (Some c)
+          ) idents in
           Some (Enumeration { name; meta; items; derives; generic_params = [] })
       | Abbrev t ->
           let has_inner_pointer = has_pointer env t in
@@ -1619,7 +1668,7 @@ let translate_decl env { derives; attributes; static; no_mangle; _ } (d: Ast.dec
           let items = List.map (fun (cons, _) ->
             let fields = DataTypeMap.find (`Variant (lid, cons)) env.struct_fields in
             let fields = List.map (fun (x: MiniRust.struct_field) -> { x with visibility = None }) fields in
-            cons, Some fields
+            cons, if fields = [] then MiniRust.Unit None else MiniRust.Struct fields
           ) branches in
           Some (Enumeration { name; meta; items; derives; generic_params })
       | Union _ ->
@@ -1807,10 +1856,24 @@ let translate_files_with_metadata files metadata =
       | _ -> true
     ) decls in
 
+    (* Step 0.5: bind all *type* declarations so that types are in scope for adding functions in the
+     environment (with their types) *)
+    let env = List.fold_left (fun env d ->
+      try
+        bind_type_decl env d
+      with e ->
+        (* We do not increase failures as this will be counted below. *)
+        KPrint.bprintf "%sERROR translating type of %a: %s%s\n%s\n" Ansi.red
+          PrintAst.Ops.plid (Ast.lid_of_decl d)
+          (Printexc.to_string e) Ansi.reset
+          (Printexc.get_backtrace ());
+        env
+    ) env decls in
+
     (* Step 1: bind all declarations and add them to the environment with their types *)
     let env = List.fold_left (fun env d ->
       try
-        bind_decl env d
+        bind_non_type_decl env d
       with e ->
         (* We do not increase failures as this will be counted below. *)
         KPrint.bprintf "%sERROR translating type of %a: %s%s\n%s\n" Ansi.red

lib/Constant.ml

@@ -72,7 +72,8 @@ let unsigned_of_signed = function
 let is_signed = function
   | Int8 | Int16 | Int32 | Int64 | CInt | PtrdiffT -> true
   | UInt8 | UInt16 | UInt32 | UInt64 | SizeT -> false
-  | Bool | Float32 | Float64 -> raise (Invalid_argument "is_signed")
+  | Bool -> raise (Invalid_argument "is_signed: bool")
+  | Float32 | Float64 -> raise (Invalid_argument "is_signed: float")
 
 let is_unsigned w = not (is_signed w)
 

lib/MiniRust.ml

@@ -8,10 +8,10 @@ end
 type borrow_kind_ = Mut | Shared
 [@@deriving show]
 
-type borrow_kind = borrow_kind_ [@ opaque ]
-and constant = Constant.t [@ opaque ]
-and width = Constant.width [@ opaque ]
-and op = Constant.op [@ opaque ]
+type borrow_kind = borrow_kind_ [@ visitors.opaque ]
+and constant = Constant.t [@ visitors.opaque ]
+and width = Constant.width [@ visitors.opaque ]
+and op = Constant.op [@ visitors.opaque ]
 and name = Name.t [@ visitors.opaque ]
 
 (* Some design choices.
@@ -21,7 +21,7 @@ and name = Name.t [@ visitors.opaque ]
      between statements and expressions -- Rust is not as strict as C in that
      regard. We'll do "the right thing" once we go to a concrete Rust syntax
      tree prior to pretty-printing. *)
-and db_index = int [@ opaque ]
+and db_index = int [@ visitors.opaque ]
 [@@deriving show,
     visitors { variety = "map"; name = "map_misc"; polymorphic = true },
     visitors { variety = "reduce"; name = "reduce_misc"; polymorphic = true }]
@@ -131,7 +131,8 @@ and pat =
 (* In the Rust grammar, both variants and structs are covered by the struct
   case. We disambiguate between the two *)
 and struct_name =
-  [ `Struct of name | `Variant of name * string ] [@ opaque]
+  [ `Struct of name | `Variant of name * string ] [@ visitors.opaque]
+  [@@deriving show]
 
 and open_var = {
   name: string;
@@ -182,7 +183,7 @@ type decl =
   }
   | Enumeration of {
     name: name;
-    items: item list;
+    items: enum_variant list;
     derives: trait list;
     meta: meta;
     generic_params: generic_param list;
@@ -218,9 +219,13 @@ type decl =
     mut: bool;
   }
 
-and item =
-  (* Not supporting tuples yet *)
-  string * struct_field list option
+and enum_variant =
+  string * enum_variant_payload
+
+and enum_variant_payload =
+  | Struct of struct_field list
+  | Unit of Z.t option (* discriminant, if specified *)
+  (* TODO: tuple *)
 
 and struct_field = {
   name: string;