Improving error localization in Pulse

pulse/src/checker/Pulse.Checker.If.fst

@@ -24,6 +24,7 @@ open Pulse.Checker.Base
 
 module T = FStar.Tactics.V2
 module J = Pulse.JoinComp
+module RU = Pulse.RuntimeUtils
 #set-options "--z3rlimit 40"
 
 
@@ -66,6 +67,7 @@ let check
   let check_branch (eq_v:term) (br:st_term) (is_then:bool)
   : T.Tac (checker_result_t (g_with_eq eq_v) pre post_hint)
   =
+    let branch_range = br.range in
     let br =
       let t =
         mk_term (Tm_ProofHintWithBinders {
@@ -78,7 +80,8 @@ let check
     in
 
     let ppname = mk_ppname_no_range "_if_br" in
-    let r = check (g_with_eq eq_v) pre post_hint ppname br in
+    let r = RU.with_error_bound branch_range (fun () ->
+      check (g_with_eq eq_v) pre post_hint ppname br) in
     r
   in
 

pulse/src/checker/Pulse.Checker.Prover.fst

@@ -377,6 +377,13 @@ let pure_eq_unif (g: env) (p: term) skip_eq_uvar : Dv bool =
     )
   | None -> false
 
+// Restore a previously-captured error_range_bound around a thunk.
+let with_saved_bound (saved_bound: option Range.range) (f: unit -> T.Tac 'a)
+  : T.Tac 'a =
+  match saved_bound with
+  | Some r -> RU.with_error_bound r f
+  | None -> f ()
+
 // skip_eq_uvar to support (assert foo. with pure (foo == ....))
 let prove_pure (g: env) (ctxt: list slprop_view) (skip_eq_uvar: bool) (goal: slprop_view) :
     T.Tac (option (prover_result g ctxt [goal])) =
@@ -387,9 +394,13 @@ let prove_pure (g: env) (ctxt: list slprop_view) (skip_eq_uvar: bool) (goal: slp
     if pure_eq_unif g p skip_eq_uvar then None else begin
     debug_prover g (fun _ -> Printf.sprintf "prove_pure p=%s success" (show p));
 
+    let saved_bound = RU.get_error_bound () in
     Some (| g, ctxt, [], [], fun g'' ->
  // implied by t2_typing
-      let pv = check_prop_validity g'' p in
+      // Restore the error bound that was active when this pure goal was matched.
+      // This closure is evaluated lazily (via cont_elab_thunk) after the
+      // original with_error_bound scope has exited.
+      let pv = with_saved_bound saved_bound (fun () -> check_prop_validity g'' p) in
       cont_elab_refl g ctxt ([] @ ctxt),
       (fun frame ->
 
@@ -424,12 +435,16 @@ let prove_with_pure (g: env) (ctxt: list slprop_view) skip_eq_uvar (goal: slprop
   | WithPure p n v ->
     if pure_eq_unif g p skip_eq_uvar then None else
 
+    let saved_bound = RU.get_error_bound () in
     Some (| g, ctxt, [Unknown v], [], fun g'' ->
       cont_elab_refl g ctxt ([] @ ctxt),
       (fun frame ->
 
 
-        k_elab_equiv (elab_slprops (frame @ [Unknown v] @ [])) (elab_slprops (frame @ [goal])) (intro_with_pure g'' (elab_slprops frame) p n v))
+        k_elab_equiv (elab_slprops (frame @ [Unknown v] @ [])) (elab_slprops (frame @ [goal]))
+          (fun post t ->
+            with_saved_bound saved_bound
+              (fun () -> intro_with_pure g'' (elab_slprops frame) p n v post t)))
       <: T.Tac _ |)
   | _ -> None
 
@@ -927,13 +942,18 @@ let prove_atom_result (g: env)
     T.Tac (prover_result g ctxt0 [goal]) =
   let Atom _ dup _ _ = ctxt in
   let goal = elab_slprop goal in
+  let saved_bound = RU.get_error_bound () in
   (| g, (if dup then rest_ctxt@[ctxt] else rest_ctxt), [], [ctxt], fun g' ->
-    let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
-    (if dup then
-      // Check that we can indeed synthesize a duplicable instance
-      ignore (compute_term_type g
-        (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
-          [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit])));
+    // Restore the error bound that was active when this atom was matched.
+    // This closure is evaluated lazily (via cont_elab_thunk) after the
+    // original with_error_bound scope has exited.
+    with_saved_bound saved_bound (fun () ->
+      let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
+      (if dup then
+        // Check that we can indeed synthesize a duplicable instance
+        ignore (compute_term_type g
+          (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
+            [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit]))));
     cont_elab_refl _ _ _, cont_elab_refl _ _ _ <: T.Tac _ |)
 
 // this matches atoms when they're the only unifiable pair

pulse/src/checker/Pulse.RuntimeUtils.fsti

@@ -23,6 +23,7 @@ type context = FStar.Sealed.Inhabited.sealed #(list (string & option range)) []
 val extend_context (tag:string) (r:option range) (ctx:context) : context
 val with_context (c:context) (f:unit -> T.Tac 'a) : T.Tac 'a
 val with_error_bound (r:Range.range) (f:unit -> T.Tac 'a) : T.Tac 'a
+val get_error_bound (_:unit) : T.Tac (option Range.range)
 val with_extv (k v : string) (f:unit -> T.Tac 'a) : T.Tac 'a
 val print_context (c:context) : T.Tac string
 val debug_at_level_no_module (s:string) : bool

pulse/src/ml/Pulse_RuntimeUtils.ml

@@ -22,6 +22,9 @@ let rec with_context (c:context) (f: unit -> 'a utac) : 'a utac =
 let with_error_bound (r:FStarC_Range.range) (f: unit -> 'a utac) : 'a utac =
   fun ps ->
     FStarC_Errors.with_error_bound r (fun _ -> f () ps)
+let get_error_bound () : FStarC_Range.range option utac =
+  fun _ps ->
+    FStarC_Effect.op_Bang FStarC_Errors.error_range_bound
 let with_extv (k:string) (v:string) (f: unit -> 'a utac) : 'a utac =
   fun ps ->
     let open FStarC_Options_Ext in

pulse/src/ml/pulseparser.mly

@@ -328,17 +328,25 @@ pulseStmtNoSeq:
     { PulseSyntaxExtension_Sugar.mk_while tm inv body }
   | INTRO p=pulseSLProp WITH ws=nonempty_list(indexingTerm)
     { PulseSyntaxExtension_Sugar.mk_intro p ws }
-  | bs=withBindersOpt REWRITE body=rewriteBody
-    {
-        PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders body bs
-    }
-  | bs=withBindersOpt ASSERT p=pulseSLProp
+  | REWRITE body=rewriteBody
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders body [] }
+  | bs=withBinders REWRITE body=rewriteBody
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders body bs }
+  | ASSERT p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSERT p) [] }
+  | bs=withBinders ASSERT p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSERT p) bs }
-  | bs=withBindersOpt ASSUME p=pulseSLProp
+  | ASSUME p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSUME p) [] }
+  | bs=withBinders ASSUME p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSUME p) bs }
-  | bs=withBindersOpt UNFOLD ns=optionalNames p=pulseSLProp
+  | UNFOLD ns=optionalNames p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (UNFOLD (ns,p)) [] }
+  | bs=withBinders UNFOLD ns=optionalNames p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (UNFOLD (ns,p)) bs }
-  | bs=withBindersOpt FOLD ns=optionalNames p=pulseSLProp
+  | FOLD ns=optionalNames p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (FOLD (ns,p)) [] }
+  | bs=withBinders FOLD ns=optionalNames p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (FOLD (ns,p)) bs }
   | bs=withBinders UNDERSCORE
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders WILD bs }
@@ -410,11 +418,6 @@ withBinders:
   | WITH bs=nonempty_list(multiBinder) DOT
     { List.flatten bs }
 
-withBindersOpt:
-  | w=withBinders
-    { w }
-  | { [] }
-
 ensuresSLProp:
   | ret=option(RETURNS i=lidentOrUnderscore COLON r=term { (i, r) }) ENSURES s=pulseSLProp maybe_opens=option(OPENS inv=appTermNoRecordExp { inv })
     { ret, s, maybe_opens }

pulse/test/Makefile

@@ -1,4 +1,5 @@
 SUBDIRS += bug-reports
+SUBDIRS += error_messages
 SUBDIRS += nolib
 SUBDIRS += pool
 

pulse/test/bug-reports/Bug267.fst.output.expected

@@ -21,7 +21,7 @@
   - Also see: Prims.fst(165,27-165,38)
   - See also Bug267.fst(58,4-58,8)
 
-* Info at Bug267.fst(62,53-63,17):
+* Info at Bug267.fst(63,2-63,17):
   - Expected failure:
   - Tactic failed
   - Cannot prove:

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

@@ -6,7 +6,7 @@
   - In the context:
       my_inv _b5 r
 
-* Info at IntroGhost.fst(84,46-87,24):
+* Info at IntroGhost.fst(87,2-87,24):
   - Expected failure:
   - Tactic failed
   - Cannot prove:

pulse/test/error_messages/AssertExtraContext.fst

@@ -0,0 +1,13 @@
+module AssertExtraContext
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Assert with binders where the witness is wrong
+[@@expect_failure [19]]
+fn assert_extra (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 0
+{
+  with v. assert (pts_to r v ** pure (v > 0));
+  ()
+}

pulse/test/error_messages/AssertExtraContext.fst.output.expected

@@ -0,0 +1,8 @@
+* Info at AssertExtraContext.fst(11,7-11,43):
+  - Expected failure:
+  - Failed to prove pure property: 0 > 0
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
+

pulse/test/error_messages/AtomicMismatch.fst

@@ -0,0 +1,14 @@
+module AtomicMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Using non-atomic operation in atomic context
+[@@expect_failure [228]]
+atomic
+fn atomic_fn (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  r := 1;  // Might error if := is not atomic-compatible
+  ()
+}

pulse/test/error_messages/AtomicMismatch.fst.output.expected

@@ -0,0 +1,7 @@
+* Info at AtomicMismatch.fst(12,2-12,8):
+  - Expected failure:
+  - Tactic failed
+  - Cannot compose computations in this atomic block:
+  - This computation has effect: stt
+  - The continuation has effect: stt_atomic emp_inames
+

pulse/test/error_messages/BindTypeMismatch.fst

@@ -0,0 +1,21 @@
+module BindTypeMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Binding with wrong type annotation
+fn helper ()
+  requires emp
+  returns r: int
+  ensures emp
+{
+  42
+}
+
+[@@expect_failure [228]]
+fn bind_type_err ()
+  requires emp
+  ensures emp
+{
+  let x : bool = helper ();  // ERROR: helper returns int, binding expects bool
+  ()
+}

pulse/test/error_messages/BindTypeMismatch.fst.output.expected

@@ -0,0 +1,7 @@
+* Info at BindTypeMismatch.fst(19,17-19,26):
+  - Expected failure:
+  - Tactic failed
+  - Type mismatch (NB: this is a syntactic check)
+  - Expected: bool
+  - Got: int
+

pulse/test/error_messages/ClosureError.fst

@@ -0,0 +1,19 @@
+module ClosureError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Error in a local function definition
+[@@expect_failure [19]]
+fn closure_error (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 0
+{
+  fn helper ()
+    requires pts_to r 1  // ERROR: pre says r==1 but caller has r==0
+    ensures pts_to r 1
+  {
+    ()
+  };
+  helper ();
+  ()
+}

pulse/test/error_messages/ClosureError.fst.output.expected

@@ -0,0 +1,18 @@
+* Info at ClosureError.fst(17,2-17,8):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 0
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int)
+      (helper
+        :
+        _: Prims.unit
+          -> fn
+               requires Pulse.Class.PtsTo.pts_to r 1
+               ensures Pulse.Class.PtsTo.pts_to r 1)
+  - VC = Pulse.Lib.Reference.pts_to r 0 == Pulse.Lib.Reference.pts_to r 1
+  - See also ClosureError.fst(17,2-18,4)
+

pulse/test/error_messages/DuplicateResource.fst

@@ -0,0 +1,12 @@
+module DuplicateResource
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Trying to read a ref twice without proper framing
+[@@expect_failure [228]]
+fn dup_fail (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 0 ** pts_to r 0
+{
+  ()
+}

pulse/test/error_messages/DuplicateResource.fst.output.expected

@@ -0,0 +1,8 @@
+* Info at DuplicateResource.fst(11,2-11,4):
+  - Expected failure:
+  - Tactic failed
+  - Cannot prove:
+      Pulse.Lib.Reference.pts_to r 0
+  - In the context:
+
+

pulse/test/error_messages/ExistsIntro.fst

@@ -0,0 +1,13 @@
+module ExistsIntro
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Postcondition requires existential that can't be satisfied
+[@@expect_failure [19]]
+fn exists_intro_fail (r: ref int)
+  requires pts_to r 5
+  ensures exists* v. pts_to r v ** pure (v > 10)
+{
+  // ERROR: after body, we have pts_to r 5 but need v > 10
+  ()
+}

pulse/test/error_messages/ExistsIntro.fst.output.expected

@@ -0,0 +1,8 @@
+* Info at ExistsIntro.fst(12,2-12,4):
+  - Expected failure:
+  - Failed to prove pure property: 5 > 10
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
+

pulse/test/error_messages/FailAssertion.fst

@@ -0,0 +1,13 @@
+module FailAssertion
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Failing assertion: error should point to the assert line
+[@@expect_failure [228]]
+fn test_fail_assert (x: int)
+  requires emp
+  ensures emp
+{
+  assert (x > 0);
+  ()
+}

pulse/test/error_messages/FailAssertion.fst.output.expected

@@ -0,0 +1,8 @@
+* Info at FailAssertion.fst(11,2-11,16):
+  - Expected failure:
+  - Tactic failed
+  - Cannot prove:
+      x > 0
+  - In the context:
+
+

pulse/test/error_messages/FoldError.fst

@@ -0,0 +1,15 @@
+module FoldError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+let my_inv (r: ref int) (v: int) : slprop = pts_to r v ** pure (v >= 0)
+
+// Trying to fold with mismatched context
+[@@expect_failure [19]]
+fn fold_fail (r: ref int)
+  requires pts_to r (-1)
+  ensures my_inv r (-1)
+{
+  fold (my_inv r (-1));  // ERROR: pure (v >= 0) not satisfiable with v = -1
+  ()
+}

pulse/test/error_messages/FoldError.fst.output.expected

@@ -0,0 +1,8 @@
+* Info at FoldError.fst(13,2-13,22):
+  - Expected failure:
+  - Failed to prove pure property: false
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
+