Do not discard names in elab_env.

src/checker/Pulse.Checker.Bind.fst

@@ -143,6 +143,12 @@ let check_bind'
   )
   else (
     let dflt () =
+      let binder =
+        // do not generate null binders, those are ignored by SMT...
+        if T.unseal binder.binder_ppname.name = "_" then
+          { binder with binder_ppname = ppname_default }
+        else
+          binder in
       let r0 = check g ctxt ctxt_typing NoHint binder.binder_ppname e1 in
       check_if_seq_lhs g ctxt _ r0 e1;
       check_binder_typ g ctxt _ r0 binder e1;

src/checker/Pulse.Checker.Match.fst

@@ -351,6 +351,7 @@ let ctag_of_br  (#g #pre #post_hint #sc_u #sc_ty #sc:_)
 : ctag
 = let (|_, c, _|) = l in ctag_of_comp_st c
 
+#push-options "--admit_smt_queries true" // Z3 crash
 let weaken_branch_observability
       (obs:observability)
       (#g #pre:_) (#post_hint:post_hint_for_env g) 
@@ -377,6 +378,7 @@ let weaken_branch_observability
       in
       (| br, d |)
     )
+#pop-options
 
 let rec max_obs 
     (checked_brs : list comp_st)

src/checker/Pulse.Checker.fst

@@ -244,11 +244,12 @@ let rec check
   else (
     maybe_trace t g0 pre0 t.range;  
     if RU.debug_at_level (fstar_env g0) "pulse.checker" then (
-      T.print (Printf.sprintf "At %s{\nerr context:\n>%s\n\n{\n\tenv=%s\ncontext:\n%s,\n\nst_term: %s\nis_source: %s}}\n"
+      T.print (Printf.sprintf "At %s{\nerr context:\n>%s\n\n{\n\tenv=%s\ncontext:\n%s,\n\nres_ppname: %s\nst_term: %s\nis_source: %s}}\n"
                 (show t.range)
                 (RU.print_context (get_context g0))
                 (show g0)
                 (show pre0)
+                (show (T.unseal res_ppname.name))
                 (show t)
                 (show (T.unseal t.source)))
     );

src/checker/Pulse.Extract.Main.fst

@@ -111,7 +111,7 @@ let is_internal_binder (b:binder) : T.Tac bool =
   s = "_tbind_c" ||
   s = "_if_br" ||
   s = "_br" ||
-  s = "_"
+  s = "__"
 
 let is_return (e:st_term) : option term =
   match e.term with
@@ -347,7 +347,12 @@ let extract_dv_binder (b:Pulse.Syntax.Base.binder) (q:option Pulse.Syntax.Base.q
   : T.Tac R.binder =
   R.pack_binder {
     sort = b.binder_ty;
-    ppname = b.binder_ppname.name;
+    ppname =
+      // "__" binders become `int __1 = f();` in karamel
+      if T.unseal b.binder_ppname.name = "__" then
+        T.seal "_"
+      else
+        b.binder_ppname.name;
     attrs = T.unseal b.binder_attrs;
     qual = (match q with
       | Some Implicit -> R.Q_Implicit

src/checker/Pulse.Syntax.Base.fsti

@@ -43,7 +43,8 @@ type ppname = {
 }
 
 let ppname_default =  {
-    name = FStar.Sealed.seal "_";
+    // This used to be "_", but that is a *null binder* and behaves very magically
+    name = FStar.Sealed.seal "__";
     range = FStar.Range.range_0
 }
 

src/checker/Pulse.Typing.Env.fst

@@ -41,7 +41,7 @@ type env = {
   f : RT.fstar_top_env;
   bs : list (var & typ);
   f_bs : (f_bs : R.env { f_bs == extend_env_l f bs });
-  names : list ppname;
+  names : ns:list ppname { List.length ns == List.length bs };
   m : m:bmap { related bs m /\ L.length names == L.length bs };
   ctxt: Pulse.RuntimeUtils.context;
 
@@ -52,13 +52,11 @@ type env = {
 let fstar_env g = RU.env_set_context g.f g.ctxt
 
 let bindings g = g.bs
-let rec bindings_with_ppname_aux (bs:list (var & typ)) (names:list ppname)
-  : T.Tac (list (ppname & var & typ)) =
-
+let rec bindings_with_ppname_aux (bs:list (var & typ)) (names:list ppname { List.length bs == List.length names })
+  : list (ppname & var & typ) =
   match bs, names with
   | [], [] -> []
   | (x, t)::bs, n::names -> (n, x, t)::(bindings_with_ppname_aux bs names)
-  | _ -> T.fail "impossible! env bs and names have different lengths"
 let bindings_with_ppname g = bindings_with_ppname_aux g.bs g.names  
 
 
@@ -104,7 +102,7 @@ let mk_env_dom _ = assert (Set.equal (Map.domain empty_bmap) Set.empty)
 let push_binding g x p t =
   { g with bs = (x, t)::g.bs;
            names = p::g.names;
-           f_bs = RT.extend_env g.f_bs x t;
+           f_bs = R.push_binding g.f_bs { ppname = p.name; uniq = x; sort = t };
            m = Map.upd g.m x t }
 
 let push_binding_bs _ _ _ _ = ()
@@ -129,12 +127,20 @@ let rec append_memP (#a:Type) (l1 l2:list a) (x:a)
   | [] -> ()
   | _::tl -> append_memP tl l2 x
 
+let rec extend_env_impl (f:R.env) (g:env_bindings) (ns:list ppname { List.length ns == List.length g }) :
+    f':R.env { f' == extend_env_l f g } =
+  match g, ns with
+  | [], [] -> f
+  | (x, t)::g, n::ns ->
+    let f = extend_env_impl f g ns in
+    R.push_binding f { ppname = (n <: ppname).name; uniq = x; sort = t }
+
 let push_env (g1:env) (g2:env { disjoint g1 g2 }) : env =
   assume (extend_env_l (extend_env_l g1.f g1.bs) g2.bs == extend_env_l g1.f (g2.bs @ g1.bs));
   {
     f = g1.f;
     bs = g2.bs @ g1.bs;
-    f_bs = extend_env_l g1.f_bs g2.bs;
+    f_bs = extend_env_impl g1.f_bs g2.bs g2.names;
     names= g2.names @ g1.names;
     m = Map.concat g2.m g1.m;
     ctxt = g1.ctxt ;
@@ -177,7 +183,7 @@ let rec remove_binding_aux (g:env)
                                                                fst b =!= x));
 
     let g' = {g with bs = prefix;
-                     f_bs = extend_env_l g.f prefix; // Recomputing, not ideal
+                     f_bs = extend_env_impl g.f prefix prefix_names; // Recomputing, not ideal
                      names=prefix_names;
                      m
     } in
@@ -192,14 +198,14 @@ let remove_binding g =
   remove_binding_aux g [] [] g.bs g.names
 
 let remove_latest_binding g =
-  match g.bs with
-  | (x, t)::rest ->
+  match g.bs, g.names with
+  | (x, t)::rest, _::names_rest ->
     let m = Map.restrict (Set.complement (Set.singleton x)) (Map.upd g.m x tm_unknown) in
     // we need uniqueness invariant in the representation
     assume (forall (b:var & typ). List.Tot.memP b rest <==> (List.Tot.memP b g.bs /\
                                                              fst b =!= x));
     let g' = {g with bs = rest;
-                     f_bs = extend_env_l g.f rest; // Recomputing, not ideal
+                     f_bs = extend_env_impl g.f rest names_rest; // Recomputing, not ideal
                      names=L.tl g.names;
                      m;
     } in
@@ -278,7 +284,7 @@ let diff g1 g2 =
   let g3 = {
     f = g1.f;
     bs = bs3;
-    f_bs = extend_env_l g1.f bs3; // Recomputing, but probably ok
+    f_bs = extend_env_impl g1.f bs3 names3; // Recomputing, but probably ok
     names = names3;
     m = m3;
     ctxt = g1.ctxt;
@@ -393,7 +399,7 @@ let env_to_doc' (simplify:bool) (e:env) : T.Tac document =
       vtns |> T.filter (fun ((n, t), x) ->
         let is_unit = FStar.Reflection.TermEq.term_eq t (`unit) in
         let x : ppname = x in
-        let is_wild = T.unseal x.name = "_" in
+        let is_wild = T.unseal x.name = "__" in
         not (is_unit && is_wild)
       )
     else

src/checker/Pulse.Typing.Env.fsti

@@ -30,7 +30,8 @@ module Pprint = FStar.Pprint
 type binding = var & typ
 type env_bindings = list binding
 
-let extend_env_l (f:R.env) (g:env_bindings) : Tot R.env =
+// This function is marked ghost because it should not be used as it renames all variables to "x"
+let extend_env_l (f:R.env) (g:env_bindings) : GTot R.env =
   L.fold_right
     (fun (x, b) g ->
       RT.extend_env g x b)
@@ -45,7 +46,7 @@ val fstar_env (g:env) : RT.fstar_top_env
 // most recent binding at the head of the list
 //
 val bindings (g:env) : env_bindings
-val bindings_with_ppname (g:env) : T.Tac (list (ppname & var & typ))
+val bindings_with_ppname (g:env) : list (ppname & var & typ)
 
 (* Returns an F* reflection environment.
 The result is the same as taking the initial F*

test/bug-reports/Bug.SpinLock.fst.output.expected

@@ -1,7 +1,7 @@
 * Info at Bug.SpinLock.fst(45,2-45,4):
   - Expected failure:
   - Cannot prove:
-      Pulse.Lib.Reference.pts_to _ ?uu___
+      Pulse.Lib.Reference.pts_to __ ?__
   - In the context:
       Pulse.Lib.SpinLock.lock_alive my_lock
         (exists* (v: Prims.int). Pulse.Lib.Reference.pts_to r v)

test/bug-reports/Bug266.fst.output.expected

@@ -11,8 +11,8 @@
   - Current context:
       emp
   - In typing environment:
-      _#60 : Prims.squash (_ == Bug266.my_intro Prims.l_False),
-      _#59 :
+      __#60 : Prims.squash (__ == Bug266.my_intro Prims.l_False),
+      __#59 :
         Pulse.Lib.Core.stt_ghost Prims.unit
           Pulse.Lib.Core.emp_inames
           (Pulse.Lib.Core.pure Prims.l_False)

test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected

@@ -13,9 +13,9 @@
   - Current context:
       ExistsErasedAndPureEqualities.some_pred x v
   - In typing environment:
-      _#586 : Prims.squash (v_ == v),
+      __#586 : Prims.squash (v_ == v),
       v_#585 : FStar.Ghost.erased Prims.int,
-      _#451 : Prims.squash (v == v),
+      __#451 : Prims.squash (v == v),
       v#267 : FStar.Ghost.erased Prims.int,
       x#262 : Pulse.Lib.Reference.ref Prims.int
 

test/bug-reports/IntroGhost.fst.output.expected

@@ -1,7 +1,7 @@
 * Info at IntroGhost.fst(44,18-44,20):
   - Expected failure:
   - Cannot prove:
-      Pulse.Lib.Reference.pts_to r _
+      Pulse.Lib.Reference.pts_to r __
   - In the context:
       IntroGhost.my_inv b r