Merge remote-tracking branch 'origin/main' into gebner_extraction

share/pulse/examples/Assume.fst

@@ -0,0 +1,37 @@
+module Assume
+
+#lang-pulse
+open Pulse
+
+assume val foo : int -> slprop
+
+fn test0 (x:int)
+  requires emp
+  ensures foo 1
+{
+  assume foo 1;
+}
+
+[@@expect_failure]
+fn test1 (x:int)
+  requires emp
+  ensures foo 1
+{
+  with a. assume foo 1;
+}
+
+fn test2 (x:int)
+  requires emp
+  ensures foo 1 ** foo 2
+{
+  assume foo 1;
+  assume foo 2;
+}
+
+[@@expect_failure]
+fn test3 (x:int)
+  requires emp
+  ensures foo 1 ** foo 2
+{
+  assume foo 2;
+}

share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst

@@ -30,3 +30,18 @@ ensures emp
 {
     id x y
 }
+
+fn f (x: nat)
+requires emp
+ensures emp
+{
+  ()
+}
+
+[@@expect_failure]
+fn test4 ()
+requires emp
+ensures emp
+{
+  f true
+}

share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst.expected

@@ -24,6 +24,15 @@
   - Expected expression of type Prims.nat got expression y of type Prims.bool
   - Raised within Tactics.refl_instantiate_implicits
 
+>>]
+>> Got issues: [
+* Error 228 at Bug.DesugaringError.fst(46,2-46,2):
+  - Could not check term: Bug.DesugaringError.f true
+
+* Error 189 at Bug.DesugaringError.fst(46,4-46,8):
+  - Expected expression of type Prims.nat got expression true of type Prims.bool
+  - Raised within Tactics.refl_instantiate_implicits
+
 >>]
 Verified module: Bug.DesugaringError
 All verification conditions discharged successfully

src/checker/Pulse.Checker.Abs.fst

@@ -41,16 +41,6 @@ let debug_abs g (s: unit -> T.Tac string) : T.Tac unit =
 
 (* Infers the the type of the binders from the specification alone, not the body *)
 
-let range_of_st_comp (st:st_comp) =
-  RU.union_ranges (RU.range_of_term st.pre) (RU.range_of_term st.post)
-
-let range_of_comp (c:comp) =
-  match c with
-  | C_Tot t -> RU.range_of_term t
-  | C_ST st -> range_of_st_comp st
-  | C_STAtomic _ _ st -> range_of_st_comp st
-  | C_STGhost _ st -> range_of_st_comp st
-
 let rec arrow_of_abs (env:_) (prog:st_term { Tm_Abs? prog.term })
   : T.Tac (term & t:st_term { Tm_Abs? t.term })
   = let Tm_Abs { b; q; ascription; body } = prog.term in
@@ -69,8 +59,7 @@ let rec arrow_of_abs (env:_) (prog:st_term { Tm_Abs? prog.term })
         let arr, body = arrow_of_abs env body in
         let arr = close_term arr x in
         let body = close_st_term body x in
-        let ty : term = wr (tm_arrow b q (C_Tot arr))
-                           (RU.union_ranges (RU.range_of_term b.binder_ty) (RU.range_of_term arr)) in
+        let ty : term = tm_arrow b q (C_Tot arr) in
         let prog : st_term = { prog with term = Tm_Abs { b; q; ascription; body}} in
         ty, prog
 
@@ -82,8 +71,7 @@ let rec arrow_of_abs (env:_) (prog:st_term { Tm_Abs? prog.term })
           //retain the original annotation, so that we check it wrt the inferred type in maybe_rewrite_body_typing
           let t = close_term t x in
           let annot = close_comp c x in
-          let ty : term = wr (tm_arrow b q (C_Tot t))
-                             (RU.union_ranges (RU.range_of_term b.binder_ty) (RU.range_of_term t)) in
+          let ty : term = tm_arrow b q (C_Tot t) in
           let ascription = { annotated = Some annot; elaborated = None } in
           let body = close_st_term body x in
           let prog : st_term = { prog with term = Tm_Abs { b; q; ascription; body} } in
@@ -104,8 +92,7 @@ let rec arrow_of_abs (env:_) (prog:st_term { Tm_Abs? prog.term })
         Env.fail env (Some prog.range) "Unannotated function body"
 
       | Some c -> ( //we're taking the annotation as is; remove it from the abstraction to avoid rechecking it
-        let ty : term = wr (tm_arrow b q c)
-                                 (RU.union_ranges (RU.range_of_term b.binder_ty) (range_of_comp c)) in
+        let ty : term = tm_arrow b q c in
         let ascription = empty_ascription in
         let body = close_st_term body x in
         let prog : st_term = { prog with term = Tm_Abs { b; q; ascription; body} } in

src/checker/Pulse.Checker.Match.fst

@@ -246,7 +246,7 @@ let check_branch
     fail g (Some e.range) "should not happen: pattern elaborated to Tv_Unknown";
   // T.print ("Elaborated pattern = " ^ T.term_to_string (fst (Some?.v elab_p)));
   let elab_p_tm = fst (Some?.v elab_p) in
-  let eq_typ = mk_sq_eq2 sc_u sc_ty sc (wr elab_p_tm Range.range_0) in
+  let eq_typ = mk_sq_eq2 sc_u sc_ty sc elab_p_tm in
   let g' = push_binding g' hyp_var ({name = Sealed.seal "branch equality"; range = Range.range_0 }) eq_typ in
   let e = open_st_term_bs e pulse_bs in
   let e =

src/checker/Pulse.Elaborate.Core.fst

@@ -143,14 +143,15 @@ let elab_lift #g #c1 #c2 (d:lift_comp g c1 c2) (e:R.term)
 
 let intro_pure_tm (p:term) =
   let open Pulse.Reflection.Util in
+  let rng = R.range_of_term p in
   wtag (Some STT_Ghost) 
        (Tm_STApp
         { head =
             tm_pureapp (tm_fvar (as_fv (mk_pulse_lib_core_lid "intro_pure")))
                        None
                        p;
           arg_qual = None;
-          arg = S.wr (`()) Range.range_0 })
+          arg = S.wr (`()) rng })
 
 let simple_arr (t1 t2 : R.term) : R.term =
   let b = R.pack_binder {

src/checker/Pulse.Syntax.Base.fst

@@ -20,6 +20,16 @@ module RT = FStar.Reflection.Typing
 module R = FStar.Reflection.V2
 module T = FStar.Tactics.V2
 
+let range_of_st_comp (st:st_comp) =
+  RU.union_ranges (RU.range_of_term st.pre) (RU.range_of_term st.post)
+
+let range_of_comp (c:comp) =
+  match c with
+  | C_Tot t -> RU.range_of_term t
+  | C_ST st -> range_of_st_comp st
+  | C_STAtomic _ _ st -> range_of_st_comp st
+  | C_STGhost _ st -> range_of_st_comp st
+
 let eq_univ (u1 u2:universe) : b:bool{b <==> u1 == u2} =
   let open FStar.Reflection.TermEq in
   assume (faithful_univ u1);

src/checker/Pulse.Syntax.Base.fsti

@@ -113,6 +113,8 @@ type comp =
   | C_STAtomic : inames:term -> obs:observability -> st_comp -> comp
   | C_STGhost  : inames:term -> st_comp -> comp
 
+val range_of_st_comp (st:st_comp) : R.range
+val range_of_comp (c:comp) : R.range
 
 let comp_st = c:comp {not (C_Tot? c) }
 

src/checker/Pulse.Syntax.Pure.fst

@@ -62,27 +62,27 @@ let tm_uinst (l:fv) (us:list universe) : term =
             l.fv_range
 
 let tm_constant (c:constant) : term =
-  set_range (R.pack_ln (R.Tv_Const c)) FStar.Range.range_0
+  R.pack_ln (R.Tv_Const c)
 
-let tm_refine (b:binder) (t:term) : term =
+let tm_refine (b:binder) (t:term) rng : term =
   let rb : R.simple_binder = RT.mk_simple_binder b.binder_ppname.name b.binder_ty in
   set_range (R.pack_ln (R.Tv_Refine rb t))
-            FStar.Range.range_0
+            rng
 
-let tm_let (t e1 e2:term) : term =
+let tm_let (t e1 e2:term) rng : term =
   let rb : R.simple_binder = RT.mk_simple_binder RT.pp_name_default t in
   set_range (R.pack_ln (R.Tv_Let false
                                  []
                                  rb
                                  e1
                                  e2))
-           FStar.Range.range_0
+           rng
 
 let tm_pureapp (head:term) (q:option qualifier) (arg:term) : term =
   set_range (R.mk_app head [(arg, elab_qual q)])
-            FStar.Range.range_0
+            (union_ranges (range_of_term head) (range_of_term arg))
 
-let tm_pureabs (ppname:R.ppname_t) (ty : term) (q : option qualifier) (body:term) : term =
+let tm_pureabs (ppname:R.ppname_t) (ty : term) (q : option qualifier) (body:term) rng : term =
   let open R in
   let open T in
   let b : T.binder = {
@@ -95,12 +95,12 @@ let tm_pureabs (ppname:R.ppname_t) (ty : term) (q : option qualifier) (body:term
   in
   let r = pack (Tv_Abs b body) in
   assume (~(R.Tv_Unknown? (R.inspect_ln r))); // NamedView API doesn't ensure this, it should
-  set_range r FStar.Range.range_0
+  set_range r rng
 
 let tm_arrow (b:binder) (q:option qualifier) (c:comp) : term =
   set_range (mk_arrow_with_name b.binder_ppname.name (b.binder_ty, elab_qual q)
                                                      (elab_comp c))
-            FStar.Range.range_0
+            (union_ranges (range_of_term b.binder_ty) (range_of_comp c))
 
 let tm_type (u:universe) : term = RT.tm_type u
 

src/checker/Pulse.Typing.fst

@@ -60,7 +60,7 @@ let mk_hide (u:universe) (t:term) (e:term) : term =
 
 let mk_eq2 (u:universe)
            (t:term)
-           (e0 e1:term) 
+           (e0 e1:term)
   : term
   = tm_pureapp
          (tm_pureapp (tm_pureapp (tm_uinst (as_fv R.eq2_qn) [u]) (Some Implicit) t)
@@ -426,7 +426,7 @@ let comp_withlocal_body_pre (pre:slprop) (init_t:term) (r:term) (init:term) : sl
   tm_star pre (mk_pts_to init_t r init)
 
 let comp_withlocal_body_post (post:term) (init_t:term) (r:term) : term =
-  tm_star post (tm_exists_sl u0 (as_binder init_t) (mk_pts_to init_t r (null_bvar 0)))  
+  tm_star post (tm_exists_sl u0 (as_binder init_t) (mk_pts_to init_t r (null_bvar 0)))
 
 let comp_withlocal_body (r:var) (init_t:term) (init:term) (c:comp{C_ST? c}) : comp =
   let r = null_var r in

src/ocaml/plugin/Pulse_Extract_CompilerLib.ml

@@ -85,12 +85,6 @@ let mle_name (x:mlpath) : mlexpr =
     as_expr (ML.MLE_Name x)
 
 let mle_let (x:mlletbinding) (b:mlexpr) : mlexpr =
-    (* Set the CInline attribute on *every* letbinding. This makes
-       generated C code much more compact.
-       See https://github.com/FStarLang/karamel/pull/470 *)
-    let flavors, lbs = x in
-    let lbs = lbs |> List.map (fun lb -> { lb with ML.mllb_meta = CInline :: lb.ML.mllb_meta }) in
-    let x = (flavors, lbs) in
     as_expr (ML.MLE_Let (x, b))
 
 let mle_app (x:mlexpr) (args:mlexpr list) : mlexpr =