Fix incorrect handling in crucial bit

FStarLang · Oct 4, 2023 · 026ba48 · 026ba48
1 parent 9edbe3d
commit 026ba48
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 9 deletions.
diff --git a/lib/Simplify.ml b/lib/Simplify.ml
@@ -141,7 +141,11 @@ end
 let optimize_lets ?ifdefs files =
   let open UseAnalysis in
   let _ = (build_usage_map_and_mark ifdefs)#visit_files [] files in
+  (* if ifdefs <> None then *)
+  (*   PPrint.(Print.(print (PrintAst.print_files files ^^ hardline))); *)
   let files = (use_mark_to_remove_or_ignore (not (ifdefs = None)))#visit_files () files in
+  (* if ifdefs <> None then *)
+  (*   PPrint.(Print.(print (PrintAst.print_files files ^^ hardline))); *)
   let _ = (build_usage_map_and_mark ifdefs)#visit_files [] files in
   let files = use_mark_to_inline_temporaries#visit_files () files in
   files

diff --git a/lib/UseAnalysis.ml b/lib/UseAnalysis.ml
@@ -175,18 +175,20 @@ let use_mark_to_remove_or_ignore final = object (self)
         self#remove_trivial_let (ELet ({ b with node = { b.node with meta = Some MetaSequence }}, e1, e2))
       else if u = AtMost 0 && Helpers.is_readonly_c_expression e1 && e2.node = EBound 0 then
         e1.node
-      (* Last two cases: unclear if it's actually unused;
-         nothing really smart to do about this, except wrap in KRML_HOST_IGNORE
-         to prevent compiler warnings. *)
-      else if is_bufcreate e1 then
+      (* Definitely unused, but no optimization; push an ignore at depth *)
+      else if u = AtMost 0 then
+        ELet ({ node = { b.node with meta = Some MetaSequence }; typ = TUnit},
+          push_ignore e1,
+          e2)
+      (* Last case: unclear if it's actually unused! So we can't mess the
+         computation and push an ignore within e1. All we can do is wrap a
+         reference to the variable in KRML_HOST_IGNORE to prevent compiler
+         warnings. *)
+      else
         ELet (b, e1, with_type e2.typ (
           ELet (sequence_binding (),
             push_ignore (with_type b.typ (EBound 0)),
             DeBruijn.lift 1 e2)))
-      else
-        ELet ({ node = { b.node with meta = Some MetaSequence }; typ = TUnit},
-          push_ignore e1,
-          e2)
     else
       (* Default case *)
       self#remove_trivial_let (ELet (b, e1, e2))

diff --git a/src/Karamel.ml b/src/Karamel.ml
@@ -571,7 +571,7 @@ Supported options:|}
    * bundle. *)
   let files = Simplify.simplify0 files in
   (* Remove trivial matches now because they eliminate code that would generate
-   * spurious dependencies otherwise. *)
+   * spurious dependencies otherwise. Requires accurate use count. *)
   let files = DataTypes.simplify files in
   let files = Monomorphization.datatypes files in
   let files = DataTypes.optimize files in