Merge branch 'master' into _taramana_const_source_blit

krmllib/C.String.fst

@@ -1,10 +1,7 @@
 module C.String
 
-module U8 = FStar.UInt8
 module U32 = FStar.UInt32
 
-module B = LowStar.Buffer
-module M = LowStar.Modifies
 
 open FStar.HyperStack.ST
 

krmllib/C.String.fsti

@@ -1,6 +1,5 @@
 module C.String
 
-module U8 = FStar.UInt8
 module U32 = FStar.UInt32
 
 module B = LowStar.Buffer

krmllib/C.fst

@@ -2,7 +2,6 @@ module C
 
 open FStar.HyperStack.ST
 
-module HS = FStar.HyperStack
 module U8 = FStar.UInt8
 
 // This module contains a series of bindings that already exist in C. It receives

krmllib/LowStar.Lib.AssocList.fst

@@ -5,8 +5,6 @@ module LowStar.Lib.AssocList
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
 module G = FStar.Ghost
-module L = FStar.List.Tot
-module U32 = FStar.UInt32
 module ST = FStar.HyperStack.ST
 
 module M = FStar.Map

krmllib/LowStar.Lib.AssocList.fsti

@@ -4,14 +4,9 @@ module LowStar.Lib.AssocList
 
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
-module G = FStar.Ghost
-module L = FStar.List.Tot
-module U32 = FStar.UInt32
 module ST = FStar.HyperStack.ST
 
 module M = FStar.Map
-module LL2 = LowStar.Lib.LinkedList2
-module LL1 = LowStar.Lib.LinkedList
 
 open FStar.HyperStack.ST
 open LowStar.BufferOps

krmllib/LowStar.Lib.LinkedList2.fst

@@ -14,8 +14,6 @@ open LowStar.BufferOps
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
 module G = FStar.Ghost
-module L = FStar.List.Tot
-module U32 = FStar.UInt32
 module ST = FStar.HyperStack.ST
 
 module LL1 = LowStar.Lib.LinkedList

krmllib/TestLib.fsti

@@ -3,7 +3,6 @@ module TestLib
 open FStar.HyperStack.ST
 open LowStar.Buffer
 
-module HS = FStar.HyperStack
 module Buffer = LowStar.Buffer
 
 (** Some test routines *)

krmllib/compat/C.Compat.String.fst

@@ -1,6 +1,5 @@
 module C.Compat.String
 
-module U8 = FStar.UInt8
 module U32 = FStar.UInt32
 
 module B = LowStar.Buffer

krmllib/compat/C.Compat.fst

@@ -2,7 +2,6 @@ module C.Compat
 
 open FStar.HyperStack.ST
 
-module HS = FStar.HyperStack
 module U8 = FStar.UInt8
 
 // This module contains a series of bindings that already exist in C. It receives

krmllib/compat/C.Nullity.fsti

@@ -37,9 +37,6 @@ let (!*) (#a: Type) (p: pointer a):
   (ensures (fun h0 x h1 -> B.live h1 p /\ x == B.get h0 p 0 /\ h1 == h0)) =
   B.index p 0ul
 
-module U32 = FStar.UInt32
-module Seq = FStar.Seq
-module Heap = FStar.Heap
 
 (* Two pointers with different reads are disjoint *)
 

lib/AstToMiniRust.ml

@@ -416,17 +416,24 @@ let translate_unknown_lid (m, n) =
   let m = compress_prefix m in
   List.map String.lowercase_ascii m @ [ n ]
 
-let borrow_kind_of_bool _b: MiniRust.borrow_kind =
-  Shared
+let borrow_kind_of_bool b: MiniRust.borrow_kind =
+  if b then Shared (* Constant pointer case *)
+  else Mut
 
 type config = {
   box: bool;
   lifetime: MiniRust.lifetime option;
+  (* Rely on the Ast type to set borrow mutability.
+     Should always be set to false to correctly infer
+     mutability in a later pass, except when translating
+    external (assumed) declarations *)
+  keep_mut: bool;
 }
 
 let default_config = {
   box = false;
   lifetime = None;
+  keep_mut = false;
 }
 
 let rec translate_type_with_config (env: env) (config: config) (t: Ast.typ): MiniRust.typ =
@@ -440,7 +447,7 @@ let rec translate_type_with_config (env: env) (config: config) (t: Ast.typ): Min
         MiniRust.box (Slice (translate_type_with_config env config t))
         (* Vec (translate_type_with_config env config t) *)
       else
-        Ref (config.lifetime, borrow_kind_of_bool b, Slice (translate_type_with_config env config t))
+        Ref (config.lifetime, (if config.keep_mut then borrow_kind_of_bool b else Shared), Slice (translate_type_with_config env config t))
   | TArray (t, c) -> Array (translate_type_with_config env config t, int_of_string (snd c))
   | TQualified lid ->
       let generic_params =
@@ -587,6 +594,12 @@ and translate_array (env: env) is_toplevel (init: Ast.expr): env * MiniRust.expr
 and translate_expr_with_type (env: env) (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)
+    inherit [_] MiniRust.DeBruijn.map
+    method! visit_Ref env a _ t = Ref (a, Shared, self#visit_typ env t)
+  end)#visit_typ ()
+  in
+
   let erase_lifetime_info = (object(self)
     inherit [_] MiniRust.DeBruijn.map
     method! visit_Ref env _ bk t = Ref (None, bk, self#visit_typ env t)
@@ -601,8 +614,11 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
     (*   PrintMiniRust.pexpr x *)
     (*   PrintMiniRust.ptyp t *)
     (*   PrintMiniRust.ptyp t_ret; *)
-    begin match x, t, t_ret with
-    | _, (MiniRust.Vec _ | Array _), Ref (_, k, Slice _) ->
+     (* Mutable borrows were only included for external definitions.
+        We erase them here; they will be handled during mutability inference, which will
+	be rechecked by the Rust compiler *)
+    begin match x, erase_borrow_kind_info t, erase_borrow_kind_info t_ret with
+    | _, (MiniRust.App (Name (["Box"], _), [Slice _]) | MiniRust.Vec _ | Array _), Ref (_, k, Slice _) ->
         Borrow (k, x)
     | Constant (w, x), Constant UInt32, Constant SizeT ->
         assert (w = Constant.UInt32);
@@ -615,8 +631,6 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
         x
 
     (* More conversions due to box-ing types. *)
-    | _, App (Name (["Box"], _), [Slice _]), Ref (_, k, Slice _) ->
-        Borrow (k, x)
     | _, Ref (_, _, Slice _), App (Name (["Box"], _), [Slice _]) ->
         (* COPY *)
         MethodCall (Borrow (Shared, Deref x), ["into"], [])
@@ -655,14 +669,14 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
         (* If we reach this case, we perform one last try by erasing the lifetime
            information in both terms. This is useful to handle, e.g., implicit lifetime
            annotations or annotations up to alpha-conversion.
-           Note, this is sound as lifetime mismatches will be caught by the Rust compiler *)
+           Note, this is sound as lifetime mismatches will be caught by the Rust compiler. *)
         if erase_lifetime_info t = erase_lifetime_info t_ret then
           x
         else
-          Warn.failwith "type mismatch;\n  e=%a\n  t=%a (verbose: %s)\n  t_ret=%a\n  x=%a"
+          Warn.failwith "type mismatch;\n  e=%a\n  t=%a (verbose: %s)\n  t_ret=%a (verbose: %s)\n  x=%a"
             PrintAst.Ops.pexpr e
             PrintMiniRust.ptyp t (MiniRust.show_typ t)
-            PrintMiniRust.ptyp t_ret
+            PrintMiniRust.ptyp t_ret (MiniRust.show_typ t_ret)
             PrintMiniRust.pexpr x;
     end
   in
@@ -1278,7 +1292,7 @@ let bind_decl env (d: Ast.decl): env =
 
   | DExternal (_, _, _, type_parameters, lid, t, _param_names) ->
       let name = translate_unknown_lid lid in
-      push_decl env lid (name, make_poly (translate_type env t) type_parameters)
+      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 =
@@ -1305,7 +1319,7 @@ let bind_decl env (d: Ast.decl): env =
           in
           let fields = List.map (fun (f, (t, _m)) ->
             let f = Option.get f in
-            { MiniRust.name = f; visibility = Some Pub; typ = translate_type_with_config env { box; lifetime } t }
+            { MiniRust.name = f; visibility = Some Pub; typ = translate_type_with_config env { box; lifetime; keep_mut = false } t }
           ) fields in
           { env with
             struct_fields = DataTypeMap.add (`Struct lid) fields env.struct_fields }
@@ -1322,7 +1336,7 @@ let bind_decl env (d: Ast.decl): env =
           List.fold_left (fun env (cons, fields) ->
             let cons_lid = `Variant (lid, cons) in
             let fields = List.map (fun (f, (t, _)) ->
-              { MiniRust.name = f; visibility = Some Pub; typ = translate_type_with_config env { box; lifetime } t }
+              { MiniRust.name = f; visibility = Some Pub; typ = translate_type_with_config env { box; lifetime; keep_mut = false } t }
             ) fields
             in
             { env with
@@ -1406,8 +1420,13 @@ let translate_decl env (d: Ast.decl): MiniRust.decl option =
       let meta = translate_meta flags in
       Some (MiniRust.Constant { name; typ; body; meta })
 
-  | DExternal _ ->
-      None
+  | DExternal (_, _, _, _, lid, _, _) ->
+      let name, parameters, return_type =
+        match lookup_decl env lid with
+        | name, Function (_, parameters, return_type) -> name, parameters, return_type
+        | _ -> failwith " impossible"
+      in
+      Some (MiniRust.Assumed { name; parameters; return_type })
 
   | DType (lid, flags, _, _, decl) ->
       let name = lookup_type env lid in

lib/Helpers.ml

@@ -28,7 +28,9 @@ end
 (* Creating AST nodes *********************************************************)
 
 let uint8 = TInt K.UInt8
+let uint16 = TInt K.UInt16
 let uint32 = TInt K.UInt32
+let uint64 = TInt K.UInt64
 let usize = TInt K.SizeT
 
 let type_of_op op w =
@@ -346,7 +348,7 @@ class ['self] readonly_visitor = object (self: 'self)
     | EPolyComp _
     | EOp _ ->
         List.for_all (self#visit_expr_w ()) es
-    | EQualified _ 
+    | EQualified _
     when is_readonly_builtin_lid e ->
         List.for_all (self#visit_expr_w ()) es
     | ETApp ({ node = EQualified _; _ } as e, _, _, _)

lib/MiniRust.ml

@@ -196,6 +196,14 @@ type decl =
     generic_params: generic_param list;
     meta: meta;
   }
+  (* We need to keep assumed/external functions to perform mutability inference
+     at the MiniRust level. However, these nodes will not be printed at code
+     generation *)
+  | Assumed of {
+    name: name;
+    parameters: typ list;
+    return_type: typ;
+  }
 
 and item =
   (* Not supporting tuples yet *)
@@ -383,7 +391,8 @@ let name_of_decl (d: decl) =
   | Enumeration { name; _ }
   | Struct { name; _ }
   | Function { name; _ }
-  | Constant { name; _ } ->
+  | Constant { name; _ }
+  | Assumed {name; _ } ->
       name
 
 let zero_usize: expr = Constant (Constant.SizeT, "0")

lib/OptimizeMiniRust.ml

@@ -101,7 +101,8 @@ let distill ts =
 (* Get the type of the arguments of `name`, based on the current state of
    `valuation` *)
 let lookup env valuation name =
-  (* KPrint.bprintf "lookup: %a\n" PrintMiniRust.pname name; *)
+  if not (NameMap.mem name env.signatures) then
+    KPrint.bprintf "ERROR looking up: %a\n" PrintMiniRust.pname name;
   let ts = NameMap.find name env.signatures in
   adjust ts (valuation name)
 
@@ -669,6 +670,8 @@ let infer_function (env: env) valuation (d: decl): decl =
          the traversal does not add or remove any bindings, but only increases the
          mutability, we can do a direct replacement instead of a more complex merge *)
       Function { f with body; parameters }
+  (* Assumed functions already have their mutability specified, we skip them *)
+  | Assumed _ -> d
   | _ ->
       assert false
 
@@ -1021,6 +1024,9 @@ let infer_mut_borrows files =
         List.filter_map (function
           | Function { parameters; name; _ } ->
               Some (name, List.map (fun (p: MiniRust.binding) -> p.typ) parameters)
+          | Assumed { name; parameters; _ } ->
+	      if List.exists (fun (n, _) -> n = name) builtins then None
+              else Some (name, parameters)
           | _ ->
               None
         ) decls) files))
@@ -1044,6 +1050,7 @@ let infer_mut_borrows files =
     else
       match infer_function env valuation (NameMap.find name definitions) with
       | Function { parameters; _ } -> distill (List.map (fun (b: MiniRust.binding) -> b.typ) parameters)
+      | Assumed { parameters; _ } -> distill parameters
       | _ -> failwith "impossible"
   in
 
@@ -1248,6 +1255,7 @@ let compute_derives files =
         match decl with
         | Function _ -> failwith "impossible"
         | Constant _ -> failwith "impossible"
+        | Assumed _ -> failwith "impossible"
         | Alias _  -> TraitSet.empty
         | Struct { fields; _ } ->
             let ts = List.map (fun (sf: struct_field) -> traits sf.typ) fields in
@@ -1289,4 +1297,12 @@ let simplify_minirust files =
      have introduced unit statements *)
   let files = map_funs remove_trailing_unit#visit_expr files in
   let files = add_derives (compute_derives files) files in
+
+  (* Remove Assumed definitions, and filter empty files to avoid spurious code generation *)
+  let files = List.filter_map (fun (x, l) ->
+      (* Filter out assumed declarations *)
+      match List.filter (function | Assumed _ -> false | _ -> true) l with
+      | [] -> None (* No declaration left, we do not keep this file *)
+      | l -> Some (x, l)
+    ) files in
   files

lib/PrintMiniRust.ml

@@ -605,6 +605,9 @@ let rec print_decl env (d: decl) =
       group @@
       group (print_meta meta ^^ string "type" ^/^ string target_name  ^^ print_generic_params generic_params ^/^ equals) ^/^
       group (print_typ env body ^^ semi)
+  (* Assumed declarations correspond to externals, which were propagated for mutability inference purposes.
+     They should have been filtered out during the MiniRust cleanup *)
+  | Assumed _ -> failwith "Assumed declaration remaining"
 
 and print_derives traits =
   group @@

test/Ctypes2.fst

@@ -4,8 +4,6 @@ open FStar.Mul
 open FStar.UInt
 open FStar.HyperStack.ST
 
-module M = LowStar.Modifies
-module U16 = FStar.UInt16
 module U32 = FStar.UInt32
 
 open Ctypes1

test/Ctypes4.fst

@@ -5,7 +5,6 @@ open FStar.UInt
 open FStar.HyperStack.ST
 
 module B = LowStar.Buffer
-module M = LowStar.Modifies
 module U16 = FStar.UInt16
 module U32 = FStar.UInt32
 module U128 = FStar.UInt128

test/DataTypesEq.fst

@@ -1,6 +1,5 @@
 module DataTypesEq
 
-module SoBuggy = FStar.HyperStack.ST
 
 type t =
   | A: UInt32.t -> t

test/HigherOrder2.fst

@@ -1,6 +1,5 @@
 module HigherOrder2
 
-module HS = FStar.HyperStack
 module HST = FStar.HyperStack.ST
 module I32 = FStar.Int32
 module M = LowStar.Modifies

test/HigherOrder4.fst

@@ -4,7 +4,6 @@ module B = LowStar.Buffer
 module HS = FStar.HyperStack
 module HST = FStar.HyperStack.ST
 module M = LowStar.Modifies
-module U32 = FStar.UInt32
 module I32 = FStar.Int32
 
 open LowStar.BufferOps

test/Layered.fst

@@ -1,7 +1,6 @@
 module Layered
 
 open FStar.HyperStack.ST
-module U32 = FStar.UInt32
 module HS = FStar.HyperStack
 
 inline_for_extraction

test/LinkedList1.fst

@@ -1,6 +1,5 @@
 module LinkedList1
 
-module B = FStar.Buffer
 module HS = FStar.HyperStack
 module G = FStar.Ghost
 module L = FStar.List.Tot

test/LinkedList2.fst

@@ -4,7 +4,6 @@ module B = FStar.Buffer
 module CN = C.Nullity
 module HS = FStar.HyperStack
 module G = FStar.Ghost
-module L = FStar.List.Tot
 module U32 = FStar.UInt32
 module MO = FStar.Modifies