Merge pull request #4258 from FStarLang/gebner_default_smtfail

Print SMT query for failing assertions.

Author: mtzguido

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

@@ -177,19 +177,27 @@ let ill_typed_term (t:term) (expected_typ got_typ : option term)
        (ensures fun _ -> True)
 =
   let open Pulse.PP in
-  match expected_typ, got_typ with
-  | None, None -> [
-    prefix 2 1 (text "Ill-typed term:") (pp t)
-  ]
-  | Some ty, None -> [
-    prefix 2 1 (text "Ill-typed term:") (pp t);
-    prefix 2 1 (text "Expected a term of type") (pp ty);
-  ]
-  | Some ty, Some ty' -> [
-    prefix 2 1 (text "Expected term of type") (pp ty) ^/^
-    prefix 2 1 (text "got term") (pp t) ^/^
-    prefix 2 1 (text "of type") (pp ty')
-  ]
+  // We used to print the term and the expected type as part of the error
+  // message, but this is often misleading and unhelpful:
+  // - It implies that the top-level term is at fault,
+  //   but the error might be in a subterm
+  // - It implies that the term has the wrong type,
+  //   but the error might just be a failing precondition.
+  [text "Ill-typed term"]
+
+  // match expected_typ, got_typ with
+  // | None, None -> [
+    // prefix 2 1 (text "Ill-typed term:") (pp t)
+  // ]
+  // | Some ty, None -> [
+  //   prefix 2 1 (text "Ill-typed term:") (pp t);
+  //   prefix 2 1 (text "Expected a term of type") (pp ty);
+  // ]
+  // | Some ty, Some ty' -> [
+  //   prefix 2 1 (text "Expected term of type") (pp ty) ^/^
+  //   prefix 2 1 (text "got term") (pp t) ^/^
+  //   prefix 2 1 (text "of type") (pp ty')
+  // ]
 
 let instantiate_term_implicits
   (g:env) (t0:term) (expected:option typ) (inst_extra:bool)

pulse/test/LoopInvariants.fst.output.expected

@@ -4,8 +4,13 @@
   - Pulse.Lib.Reference.pts_to s 3
   - Pulse.Lib.Reference.pts_to s 2
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int)
+      (s : Pulse.Lib.Reference.ref Prims.int) (meas : Prims.unit)
+      (__ : Prims.squash (meas == ())) (__ : Prims.squash (true == true))
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to s 3 == Pulse.Lib.Reference.pts_to s 2
   - See also LoopInvariants.fst(65,4-65,10)
 
 * Info at LoopInvariants.fst(76,4-76,8):
@@ -14,7 +19,12 @@
   - Pulse.Lib.Reference.pts_to s 3
   - Pulse.Lib.Reference.pts_to s 2
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int)
+      (s : Pulse.Lib.Reference.ref Prims.int) (meas : Prims.unit)
+      (__ : Prims.squash (meas == ())) (__ : Prims.squash (true == true))
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to s 3 == Pulse.Lib.Reference.pts_to s 2
   - See also LoopInvariants.fst(76,4-76,10)
 

pulse/test/MatchBasic.fst.output.expected

@@ -2,7 +2,8 @@
   - Expected failure:
   - Could not verify that this match is exhaustive.
   - Patterns are incomplete
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (xs : Prims.list Prims.int)
+  - VC = ~(Nil? xs) ==> Prims.l_False
   - Also see: MatchBasic.fst(134,8-134,10)
 

pulse/test/Test.Recursion.fst.output.expected

@@ -1,22 +1,51 @@
 * Info at Test.Recursion.fst(84,2-84,20):
   - Expected failure:
-  - Ill-typed term: test_ghost_loop ()
-  - Expected a term of type
-      ghost fn
-        requires emp
-        ensures emp
+  - Ill-typed term
   - Could not prove termination
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env =
+      (x : Prims.unit)
+      (test_ghost_loop
+        :
+
+            x':
+              Prims.unit
+                { FStar.Range.labeled FStar.Range.range_0
+                    "Could not prove termination"
+                    (() << ()) }
+          -> ghost fn
+               requires Pulse.Lib.Core.emp
+               ensures Pulse.Lib.Core.emp)
+  - VC =
+      FStar.Range.labeled FStar.Range.range_0
+        "Could not prove termination"
+        (() << ())
 
 * Info at Test.Recursion.fst(127,4-127,22):
   - Expected failure:
-  - Ill-typed term: test5' (z - 1) (y - 1)
-  - Expected a term of type
-      ghost fn
-        requires emp
-        ensures emp
+  - Ill-typed term
   - Could not prove termination
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env =
+      (z : Prims.int) (y : Prims.nat)
+      (test5'
+        :
+
+            z': Prims.int ->
+            y':
+              Prims.nat
+                { FStar.Range.labeled FStar.Range.range_0
+                    "Could not prove termination"
+                    (z' << z) }
+          -> ghost fn
+               requires Pulse.Lib.Core.emp
+               ensures Pulse.Lib.Core.emp)
+      (_if_hyp
+        :
+        Prims.squash (Pulse.Lib.Core.rewrites_to_p (z <> 0 && y <> 0) true))
+  - VC =
+      y - 1 >= 0 /\
+      FStar.Range.labeled FStar.Range.range_0
+        "Could not prove termination"
+        (z - 1 << z)
 

pulse/test/bug-reports/Bug.DesugaringError.fst.output.expected

@@ -13,6 +13,6 @@
 
 * Info at Bug.DesugaringError.fst(36,4-36,8):
   - Expected failure:
-  - Ill-typed term: f true
+  - Ill-typed term
   - Expected expression of type Prims.nat got expression true of type Prims.bool
 

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

@@ -3,25 +3,31 @@
   - Subtyping check failed
   - Expected type FStar.Seq.Base.seq Prims.int
     got type FStar.Seq.Base.seq Prims.nat
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env =
+  - VC =
+      forall (a1: Pulse.Lib.Array.Core.array Prims.int)
+        (s1: FStar.Seq.Base.seq Prims.nat).
+        (* - Subtyping check failed\n  - Expected type FStar.Seq.Base.seq Prims.int\n    got type FStar.Seq.Base.seq Prims.nat *)
+        forall (i: Prims.int). i >= 0
   - See also Prims.fst(642,18-642,24)
 
 * Info at Bug100.fst(19,57-19,58):
   - Expected failure:
   - Subtyping check failed
   - Expected type FStar.Seq.Base.seq Prims.int
     got type FStar.Seq.Base.seq Prims.nat
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (a : Bug100.array Prims.int) (s : FStar.Seq.Base.seq Prims.nat)
+  - VC = forall (i: Prims.int). i >= 0
   - See also Prims.fst(642,18-642,24)
 
 * Info at Bug100.fst(23,11-23,17):
   - Expected failure:
-  - Ill-typed term: pts_to int a1 s1
-  - Expected a term of type slprop
+  - Ill-typed term
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (a1 : Bug100.array Prims.int) (s1 : FStar.Seq.Base.seq Prims.nat)
+  - VC = forall (i: Prims.int). Prims.l_True == (i >= 0 == true)
   - Also see: Prims.fst(165,27-165,38)
 

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

@@ -1,12 +1,9 @@
 * Info at Bug206.fst(14,2-14,6):
   - Expected failure:
-  - Ill-typed term: test x
-  - Expected a term of type
-      fn
-        requires emp
-        ensures emp
+  - Ill-typed term
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (x : Prims.nat)
+  - VC = x > 0
   - See also Bug206.fst(14,2-14,8)
 

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

@@ -2,8 +2,9 @@
   - Expected failure:
   - Failed to prove pure property: l_False
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (uu___0 : Prims.unit)
+  - VC = Prims.l_False
   - See also Bug266.fst(10,31-10,36)
 
 * Info at Bug266.fst(24,2-24,9):

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

@@ -7,8 +7,17 @@
   - Expected failure:
   - Could not prove equality between computed type int and expected type nat
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env =
+      (x : Prims.nat) (y : Prims.nat) (ctr : Pulse.Lib.Reference.ref Prims.int)
+      (acc : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit)
+      (___8 : FStar.Ghost.erased Prims.unit)
+      (__c89 : FStar.Ghost.erased (FStar.Ghost.erased Prims.int))
+      (__a910 : FStar.Ghost.erased (FStar.Ghost.erased Prims.int))
+      (__ : Prims.squash (__c89 <= x /\ __a910 == __c89 * y))
+      (__ : Prims.squash (___8 == ()))
+      (__ : Prims.squash (false == (__c89 < x)))
+  - VC = forall (i: Prims.int). Prims.l_True == (i >= 0 == true)
   - Also see: Prims.fst(165,27-165,38)
   - See also Bug267.fst(58,4-58,8)
 

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

@@ -1,8 +1,8 @@
 * Info at Bug59.fst(12,11-12,24):
   - Expected failure:
-  - Ill-typed term: pure (x == y)
-  - Expected a term of type slprop
+  - Ill-typed term
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (a : Type0) (b : Type0) (x : a) (y : b)
+  - VC = b == a