Merge pull request #522 from FStarLang/protz_uus

More aggressive elimination of temporaries

lib/CStarToC11.ml

@@ -1301,7 +1301,6 @@ let mk_type_or_external m (w: where) ?(is_inline_static=false) (d: decl): C.decl
                 (Z.of_int (List.length cases)),
               if custom_values <> [] then List.hd custom_values else Z.zero
             in
-            KPrint.bprintf "max_value=%s, min_value=%s\n" (Z.to_string max_value) (Z.to_string min_value);
             let t =
               if Z.(geq min_value zero && leq max_value (of_string "0xff")) then
                 K.UInt8

lib/Simplify.ml

@@ -132,11 +132,17 @@ let use_mark_to_inline_temporaries = object (self)
         b.node.name = "scrut" ||
         Structs.should_rewrite b.typ = NoCopies
        ) &&
-      v = AtMost 1 && (
-        is_readonly_c_expression e1 &&
-        safe_readonly_use e2 ||
-        safe_pure_use e2
-      ) (* || is_readonly_and_variable_free_c_expression e1 && b.node.mut *)
+        (v = AtMost 1 && (
+          is_readonly_c_expression e1 &&
+          safe_readonly_use e2 ||
+          safe_pure_use e2
+        ) ||
+        is_readonly_and_variable_free_c_expression e1 && not b.node.mut)
+    (* b.node.mut is an approximation of "the address of this variable is taken"
+       -- TODO this is somewhat incompatible with the phase that changes size-1
+       arrays into variables who address is taken, so we should also check beore
+       inlining that the address of this variable is not taken... this is
+       starting to be quite an expensive check! *)
     then
       (* Don't drop a potentially useful comment into the ether *)
       let e1 = { e1 with meta = e1.meta @ b.meta } in