autocorres: finer control of Collect simps.

Fixes translation of empty Specs.

tools/autocorres/AutoCorresSimpset.thy

@@ -25,7 +25,10 @@ val AUTOCORRES_SIMPSET =
     (* affects boolean expressions *)
     @ @{thms word_neq_0_conv}
     (* interferes with struct_rewrite *)
-    @ @{thms ptr_coerce.simps ptr_add_0_id})
+    @ @{thms ptr_coerce.simps ptr_add_0_id}
+    (* oversimplifies Spec sets prior to L2 stage
+       (we will control this explicitly in L2Peephole) *)
+    @ @{thms CollectPairFalse})
   |> simpset_of
 
 *}

tools/autocorres/L2Peephole.thy

@@ -46,6 +46,12 @@ lemma L2_guard_false [L2opt]: "\<lbrakk> \<And>s. \<not> P s \<rbrakk> \<Longrig
   apply (monad_eq simp: L2_defs)
   done
 
+lemma L2_spec_empty [L2opt]:
+  (* FIXME: do we need both? *)
+  "L2_spec {} = L2_fail"
+  "\<lbrakk> \<And>s t. \<not> C s t \<rbrakk> \<Longrightarrow> L2_spec {(s, t). C s t} = L2_fail"
+  by (monad_eq simp: L2_defs)+
+
 lemma L2_unknown_bind [L2opt]:
   "(\<And>a b. f a = f b) \<Longrightarrow> (L2_seq (L2_unknown name) f) = f undefined"
   apply (atomize)

tools/autocorres/LocalVarExtract.thy

@@ -17,4 +17,14 @@ theory LocalVarExtract
 imports SimplConv L2Defs
 begin
 
+(* These are used to translate unsimplified L1_specs. *)
+lemma Collect_prod_inter:
+  "{(s, t). P s t} \<inter> {(s, t). Q s t} = {(s, t). P s t \<and> Q s t}"
+  by (fastforce intro: set_eqI)
+
+lemma Collect_prod_union:
+  "{(s, t). P s t} \<union> {(s, t). Q s t} = {(s, t). P s t \<or> Q s t}"
+  by (fastforce intro: set_eqI)
+
+
 end

tools/autocorres/local_var_extract.ML

@@ -157,7 +157,7 @@ fun parse_spec ctxt prog_info term =
      * We blithely rewrite them here.
      *)
     val term = Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt)
-        (map mk_meta_eq @{thms Collect_conj_eq[symmetric] Collect_disj_eq[symmetric]}) [] term
+        (map safe_mk_meta_eq @{thms Collect_prod_inter Collect_prod_union}) [] term
 
     (* Apply a dummy old and new state variable to the term. *)
     val dummy_s = Free ("_dummy_state1", #state_type prog_info)

tools/autocorres/tests/proof-tests/Test_Spec_Translation.thy

@@ -17,18 +17,18 @@ begin
 
 install_C_file "test_spec_translation.c"
 
-autocorres "test_spec_translation.c"
+autocorres [ts_rules = nondet] "test_spec_translation.c"
 
 context test_spec_translation begin
-(* We don't know what this function does, but it's guaranteed to only modify "reg". *)
-thm magic_body_def magic'_def
-thm call_magic_body_def call_magic'_def
 
 (* Check that our translation did honour the given spec. *)
 lemma validNF_spec[wp]:
   "\<lbrace>\<lambda>s. (\<exists>t. (s, t) \<in> f) \<and> (\<forall>t. (s, t) \<in> f \<longrightarrow> P () t)\<rbrace> spec f \<lbrace>P\<rbrace>!"
   by (clarsimp simp: validNF_def valid_def no_fail_def spec_def)
 
+(* We don't know what this function does, but it's guaranteed to modify only "reg". *)
+thm magic_body_def magic'_def
+
 lemma magic'_wp:
   "\<lbrace>P\<rbrace> magic' x \<lbrace>\<lambda>_ s. \<exists>x. P (s\<lparr>reg_'' := x\<rparr>)\<rbrace>!"
   apply (unfold magic'_def)
@@ -36,6 +36,9 @@ lemma magic'_wp:
   apply (fastforce simp: lifted_globals.splits)
   done
 
+(* This function is annotated with an assertion. *)
+thm call_magic_body_def call_magic'_def
+
 lemma call_magic'_wp:
   "of_int x < (42 :: 32 signed word) \<Longrightarrow>
    \<lbrace>P\<rbrace> call_magic' x \<lbrace>\<lambda>_ s. \<exists>x. P (s\<lparr>reg_'' := x\<rparr>)\<rbrace>!"
@@ -44,6 +47,14 @@ lemma call_magic'_wp:
   apply (fastforce simp: lifted_globals.splits)
   done
 
+(* This function is guaranteed to fail. *)
+thm abort_body_def abort'_def abort_spec_def
+
+lemma abort'_spec:
+  "abort' = fail"
+  apply (simp add: abort'_def)
+  done
+
 end
 
 end

tools/autocorres/tests/proof-tests/test_spec_translation.c

@@ -17,7 +17,12 @@ int magic(int x) {
   return x;
 }
 
-/* Make sure \<Gamma> is generated. */
+/* abort will generate an empty spec "{}" if optimisation is enabled. */
+/** MODIFIES:
+    FNSPEC abort_spec: "\<Gamma> \<turnstile> {} Call abort_'proc {}" */
+void abort(void);
+
+/* Test specs interleaved with function bodies. */
 int call_magic(int x) {
   /** GHOSTUPD: "(\<acute>x < 42, id)" */
   return magic(x);