Merge branch 'master' into afromher_rust

FStarLang · Aug 30, 2024 · cd568f8 · cd568f8
2 parents 532cc7f + fa19d37
commit cd568f8
Show file tree

Hide file tree

Showing 9 changed files with 38 additions and 10 deletions.
diff --git a/lib/Ast.ml b/lib/Ast.ml
@@ -347,6 +347,7 @@ and binder' = {
   meta: meta option;
   atom: atom_t;
     (** Only makes sense when opened! *)
+  attempt_inline: bool; (* Whether to attempt inlining, as if this was named uu__... *)
 }
 
 and binder =

diff --git a/lib/DataTypes.ml b/lib/DataTypes.ml
@@ -910,7 +910,8 @@ let rec compile_pattern env scrut pat expr =
         mut = false;
         mark = ref Mark.default;
         meta = None;
-        atom = b
+        atom = b;
+        attempt_inline = false;
       } in
       [], with_type expr.typ (ELet (b, scrut, close_binder b expr))
   | PWild ->

diff --git a/lib/Helpers.ml b/lib/Helpers.ml
@@ -140,8 +140,8 @@ let mk_deref t ?(const=false) e =
 
 (* Binder nodes ***************************************************************)
 
-let fresh_binder ?(mut=false) name typ =
-  with_type typ { name; mut; mark = ref Mark.default; meta = None; atom = Atom.fresh () }
+let fresh_binder ?(mut=false) ?(attempt_inline=false) name typ =
+  with_type typ { name; mut; mark = ref Mark.default; meta = None; attempt_inline; atom = Atom.fresh () }
 
 let mark_mut b =
   { b with node = { b.node with mut = true }}
@@ -151,7 +151,8 @@ let sequence_binding () = with_type TUnit {
   mut = false;
   mark = ref Mark.default;
   meta = Some MetaSequence;
-  atom = Atom.fresh ()
+  atom = Atom.fresh ();
+  attempt_inline = false;
 }
 
 let unused_binding = sequence_binding

diff --git a/lib/InputAst.ml b/lib/InputAst.ml
@@ -129,6 +129,7 @@ and binder = {
   name: ident;
   typ: typ;
   mut: bool;
+  meta: flag list;
 }
 
 and ident =
@@ -164,7 +165,7 @@ let flatten_arrow =
 
 type version = int
   [@@deriving yojson]
-let current_version: version = 28
+let current_version: version = 31
 
 type file = string * program
   [@@deriving yojson]

diff --git a/lib/InputAstToAst.ml b/lib/InputAstToAst.ml
@@ -62,8 +62,9 @@ let rec mk_decl = function
 and mk_binders bs =
   List.map mk_binder bs
 
-and mk_binder { I.name; typ; mut } =
-  Helpers.fresh_binder ~mut name (mk_typ typ)
+and mk_binder { I.name; typ; mut; meta } =
+  let attempt_inline = List.mem Inline meta in
+  Helpers.fresh_binder ~mut ~attempt_inline name (mk_typ typ)
 
 and mk_tfields fields =
   List.map (fun (name, (field, mut)) -> name, (mk_typ field, mut)) fields

diff --git a/lib/Simplify.ml b/lib/Simplify.ml
@@ -126,7 +126,11 @@ let use_mark_to_inline_temporaries = object (self)
     let e1 = self#visit_expr_w () e1 in
     let e2 = self#visit_expr_w () e2 in
     let _, v = !(b.node.mark) in
-    if (Helpers.is_uu b.node.name || b.node.name = "scrut" || Structs.should_rewrite b.typ = NoCopies) &&
+    if (b.node.attempt_inline ||
+        Helpers.is_uu b.node.name ||
+        b.node.name = "scrut" ||
+        Structs.should_rewrite b.typ = NoCopies
+       ) &&
       v = AtMost 1 && (
         is_readonly_c_expression e1 &&
         safe_readonly_use e2 ||

diff --git a/lib/SimplifyWasm.ml b/lib/SimplifyWasm.ml
@@ -171,7 +171,7 @@ let eta_expand = object
         let tret, targs = flatten_arrow t in
         let n = List.length targs in
         let binders, args = List.split (List.mapi (fun i t ->
-          with_type t { name = Printf.sprintf "x%d" i; mut = false; mark = ref Mark.default; meta = None; atom = Atom.fresh () },
+          with_type t { name = Printf.sprintf "x%d" i; mut = false; mark = ref Mark.default; meta = None; atom = Atom.fresh (); attempt_inline = false },
           { node = EBound (n - i - 1); typ = t }
         ) targs) in
         let body = { node = EApp (body, args); typ = tret } in

diff --git a/test/InlineLet.fst b/test/InlineLet.fst
@@ -0,0 +1,14 @@
+module InlineLet
+
+(* None of {foobar,temp_x,temp_y} should appear in the output *)
+
+let main () =
+  let open FStar.Int32 in
+  [@@CInline] let foobar = 0l in
+  add foobar 0l
+
+let foo (a:UInt32.t) =
+  let open FStar.UInt32 in
+  [@@CInline] let temp_x = a in
+  [@@CInline] let temp_y = a in
+  temp_x `add_underspec` temp_y
diff --git a/test/Makefile b/test/Makefile
@@ -60,7 +60,7 @@ ifneq ($(RECENT_GCC),"yes")
 endif
 
 CUSTOM		= count-eq count-uu check-unused check-no-constructor check-no-erased \
-  check-right-file count-deref check-global-init check-useless-alias
+  check-right-file count-deref check-global-init check-useless-alias check-inline-let
 ifneq ($(CRYPTO),)
   CRYPTO_WASM_FILES=Crypto.Symmetric.Chacha20.wasm-test
 endif
@@ -236,6 +236,11 @@ check-no-erased: $(OUTPUT_DIR)/Shifting.exe
 check-right-file: $(OUTPUT_DIR)/MonomorphizationSeparate2.exe
 	egrep -q 'typedef.*pair' $(OUTPUT_DIR)/MonomorphizationSeparate2.out/MonomorphizationSeparate1.h
 
+check-inline-let: $(OUTPUT_DIR)/InlineLet.exe
+	! grep foobar $(OUTPUT_DIR)/InlineLet.out/InlineLet.c
+	! grep temp_x $(OUTPUT_DIR)/InlineLet.out/InlineLet.c
+	! grep temp_y $(OUTPUT_DIR)/InlineLet.out/InlineLet.c
+
 clean:
 	rm -rf $(WEB_DIR) .output