autocorres: fix a bug in l2_opt.

JIRA issue VER-510

tools/autocorres/L2Opt.thy

@@ -96,6 +96,10 @@ lemma simp_expr_weaken:
 
 (*
  * Monad simplification rules.
+ *
+ * When solving "monad_equiv P A B R E", the l2_opt tactics assume that P is concrete;
+ * to ensure this, monad_equiv rules should result in R being instantiated.
+ * See e.g. monad_equiv_unreachable where we have to constrain the rule.
  *)
 
 lemma monad_equiv_gets [L2flow]:
@@ -322,8 +326,12 @@ lemma monad_equiv_recguard [L2flow]:
 
 lemma monad_equiv_unreachable' [L2flow]:
   "monad_equiv (\<lambda>_. False) L (L2_gets (\<lambda>_. undefined) [''L2Opt_internal_var'']) Q R"
-  apply (monad_eq simp: monad_equiv_def L2_defs simp_expr_def valid_def validE_def)
-  done
+  by (simp add: monad_equiv_def)
+
+(* avoid leaving schematic Q in goal *)
+lemma monad_equiv_unreachable [L2flow]:
+  "monad_equiv (\<lambda>_. False) L (L2_gets (\<lambda>_. undefined) [''L2Opt_internal_var'']) (\<lambda>_ _. False) R"
+  by (rule monad_equiv_unreachable')
 
 lemma monad_equiv_split [L2flow]:
   "\<lbrakk> \<And>a b. monad_equiv (P (a, b)) (X a b) (Y a b) (Q a b) (E a b) \<rbrakk> \<Longrightarrow>

tools/autocorres/l2_opt.ML

@@ -96,11 +96,15 @@ fun simp_monad_equiv_pre_tac ctxt =
       Const (@{const_name Trueprop}, _) $
         (Const (@{const_name monad_equiv}, _) $ P $ _ $ _ $ _ $ _) =>
         let
+          (* If P is schematic, we could end up with flex-flex pairs that Isabelle refuses to solve.
+           * Our monad_equiv rules should never allow this to happen. *)
+          val _ = if not (exists_subterm is_Var P) then () else
+                    raise CTERM ("autocorres: bad schematic in monad_equiv_pre", [Thm.cprem_of thm 1])
           (* Perform basic simplification of the term. *)
           val simp_thm = Simplifier.asm_full_rewrite (map_opt_simpset false ctxt) (Thm.cterm_of ctxt P)
         in
           (resolve_tac ctxt [@{thm monad_equiv_weaken_pre''} OF [simp_thm]] 1
-            ORELSE (fn t => raise (CTERM ("failed to prove goal", [Thm.cprem_of t 1])))) thm
+            ORELSE (fn t => raise (CTERM ("autocorres: monad_equiv_pre failed to prove goal", [Thm.cprem_of t 1])))) thm
         end
     | _ =>
         all_tac thm

tools/autocorres/tests/parse-tests/l2_opt_invariant.c

@@ -0,0 +1,16 @@
+/*
+ * Used to break l2_opt.
+ * Because monad_equiv_unreachable' didn't instantiate the postcond
+ * and left another subgoal with a schematic precond, which caused
+ * something or other to break. It's a long story.
+ *
+ * JIRA issue VER-510
+ */
+
+void foo(int *x) {
+  int z;
+  if (!(*x)) {
+    /* always fails */
+    z = 1 / *x;
+  }
+}