From 0166335135cadf96aa48006f50e82c5210f364a6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 Jun 2018 08:43:10 +0200
Subject: [PATCH] wp_cas_fail/succ: Report error when proving
 vals_cas_compare_safe; fast_done is enough

---
 tests/heap_lang.ref            |  5 +++++
 tests/heap_lang.v              | 11 +++++++++++
 theories/heap_lang/proofmode.v |  8 ++++----
 3 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index eb689f8e6..ee03be85c 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -68,3 +68,8 @@
     let: "val2" := fun2 "val1" in
     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
+"not_cas_compare_safe"
+     : string
+The command has indeed failed with message:
+Ltac call to "wp_cas_suc" failed.
+Tactic failure: wp_cas_suc: Values are not safe to compare for CAS.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 09ed3ecc6..7efc06e02 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -161,5 +161,16 @@ Section printing_tests.
 
 End printing_tests.
 
+Section error_tests.
+  Context `{heapG Σ}.
+
+  Check "not_cas_compare_safe".
+  Lemma not_cas_compare_safe (l : loc) (v : val) :
+    l ↦ v -∗ WP CAS #l v v {{ _, True }}.
+  Proof.
+    iIntros "H↦". Fail wp_cas_suc.
+  Abort.
+End error_tests.
+
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
 Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index c46eafa57..17236f403 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -406,7 +406,7 @@ Tactic Notation "wp_cas_fail" :=
     [iSolveTC
     |solve_mapsto ()
     |try congruence
-    |done
+    |fast_done || fail "wp_cas_fail: Values are not safe to compare for CAS"
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
@@ -415,7 +415,7 @@ Tactic Notation "wp_cas_fail" :=
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |try congruence
-    |done
+    |fast_done || fail "wp_cas_fail: Values are not safe to compare for CAS"
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_fail: not a 'wp'"
   end.
@@ -434,7 +434,7 @@ Tactic Notation "wp_cas_suc" :=
     [iSolveTC
     |solve_mapsto ()
     |try congruence
-    |done
+    |fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
     |pm_reflexivity
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?E ?e ?Q) =>
@@ -444,7 +444,7 @@ Tactic Notation "wp_cas_suc" :=
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |try congruence
-    |done
+    |fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
     |pm_reflexivity
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_suc: not a 'wp'"
-- 
GitLab