Merge branch 'master' into autocorres-seL4

tools/autocorres/HeapLift.thy

@@ -1110,6 +1110,26 @@ lemma struct_rewrite_modifies_globals_setter [heap_abs]:
   apply (clarsimp simp: valid_globals_field_def struct_rewrite_expr_def struct_rewrite_modifies_def)
   done
 
+(* Translate Hoare modifies specs. *)
+lemma abs_spec_may_not_modify_globals[heap_abs]:
+  "abs_spec st \<top> {(a, b). meq b a} {(a, b). meq b a}"
+  apply (clarsimp simp: abs_spec_def meq_def)
+  done
+
+lemma abs_spec_modify_global[heap_abs]:
+  "valid_globals_field st old_getter old_setter new_getter new_setter \<Longrightarrow>
+   abs_spec st \<top> {(a, b). C a b} {(a, b). C' a b} \<Longrightarrow>
+   abs_spec st \<top> {(a, b). mex (\<lambda>x. C (new_setter (\<lambda>_. x) a) b)} {(a, b). mex (\<lambda>x. C' (old_setter (\<lambda>_. x) a) b)}"
+  apply (fastforce simp: abs_spec_def mex_def valid_globals_field_def)
+  done
+
+(* Remove the Hoare modifies constants after we're finished,
+ * as they have very buggy print translations.
+ * In particular, applying abs_spec_modify_global replaces the bound variable by "x"
+ * and confuses the print translation into producing "may_only_modify_globals [x]". *)
+lemmas [polish] = mex_def meq_def
+
+
 (* Signed words are stored on the heap as unsigned words. *)
 
 lemma uint_scast [simp]:

tools/autocorres/WordAbstract.thy

@@ -513,6 +513,13 @@ lemma corresTA_L2_guard:
   apply (monad_eq simp: L2_defs corresXF_def)
   done
 
+lemma corresTA_L2_spec:
+  "(\<And>s t. abstract_val (Q s) (P s t) id (P' s t)) \<Longrightarrow>
+   corresTA Q rx ex (L2_spec {(s, t). P s t}) (L2_spec {(s, t). P' s t})"
+  apply (monad_eq simp: L2_defs corresXF_def in_liftE split: sum.splits)
+  apply (erule exI)
+  done
+
 lemma corresTA_L2_condition:
   "\<lbrakk> corresTA P rx ex L L';
      corresTA Q rx ex R R';
@@ -877,6 +884,7 @@ lemmas [word_abs] =
   corresTA_L2_catch
   corresTA_L2_while
   corresTA_L2_guard
+  corresTA_L2_spec
   corresTA_L2_condition
   corresTA_L2_unknown
   corresTA_L2_recguard

tools/autocorres/local_var_extract.ML

@@ -150,18 +150,28 @@ fun mk_l2monadT stateT retT exT =
  *)
 fun parse_spec ctxt prog_info term =
   let
+    (*
+     * If simplification was turned off in L1, the spec may still contain
+     * unions and intersections, i.e. be of the form
+     *   {(s, t). f s t} \<union> {(s, t). g s t} ...
+     * 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
+
     (* Apply a dummy old and new state variable to the term. *)
-    val dummy_s = Free ("_dummy_state1", (#state_type prog_info))
-    val dummy_t = Free ("_dummy_state2", (#state_type prog_info))
+    val dummy_s = Free ("_dummy_state1", #state_type prog_info)
+    val dummy_t = Free ("_dummy_state2", #state_type prog_info)
     val dummy_tuple = HOLogic.mk_tuple [dummy_s, dummy_t]
     val t = Envir.beta_eta_contract (
         (Const (@{const_name "Set.member"},
             fastype_of dummy_tuple --> fastype_of term --> @{typ bool})
           $ dummy_tuple $ term))
 
-    (* Pull apart the "split" at the beginning of the term. *)
+    (* Pull apart the "split" at the beginning of the term, then apply
+     * to our dummy variables *)
     val t = Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt)
-        [mk_meta_eq @{thm split_def}, mk_meta_eq @{thm fst_conv}, mk_meta_eq @{thm snd_conv}] [] t
+        (map mk_meta_eq @{thms split_def fst_conv snd_conv mem_Collect_eq}) [] t
 
     (*
      * Pull out any references to any other variables into a lambda
@@ -174,6 +184,8 @@ fun parse_spec ctxt prog_info term =
     val t = Utils.abs_over "t" (globals_getter $ dummy_t) t
             |> Utils.abs_over "s" (globals_getter $ dummy_s)
             |> HOLogic.mk_case_prod
+    val t_collect = @{mk_term "Collect :: (?'s \<Rightarrow> bool) \<Rightarrow> ?'s set" ('s)}
+                       (domain_type (fastype_of t))
   in
     (* Determine if there are any references left to the dummy state
      * variable. If so, give up on the translation. *)
@@ -182,7 +194,7 @@ fun parse_spec ctxt prog_info term =
       (warning ("Can't parse spec term: "
           ^ (Utils.term_to_string ctxt term)); NONE)
     else
-      SOME t
+      SOME (t_collect $ t)
   end
 
 

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

@@ -0,0 +1,49 @@
+(*
+ * Copyright 2016, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ *)
+
+(*
+ * Tests for handling Spec constructs emitted by the C parser.
+ *)
+theory Test_Spec_Translation
+imports "../../AutoCorres"
+begin
+
+install_C_file "test_spec_translation.c"
+
+autocorres "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)
+
+lemma magic'_wp:
+  "\<lbrace>P\<rbrace> magic' x \<lbrace>\<lambda>_ s. \<exists>x. P (s\<lparr>reg_'' := x\<rparr>)\<rbrace>!"
+  apply (unfold magic'_def)
+  apply wp
+  apply (fastforce simp: lifted_globals.splits)
+  done
+
+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>!"
+  apply (unfold call_magic'_def)
+  apply (wp magic'_wp)
+  apply (fastforce simp: lifted_globals.splits)
+  done
+
+end
+
+end

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

@@ -0,0 +1,24 @@
+/*
+ * Copyright 2016, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ */
+
+volatile int reg;
+
+/** DONT_TRANSLATE
+    MODIFIES: reg */
+int magic(int x) {
+  asm volatile ("blah blah": "r"(x));
+  return x;
+}
+
+/* Make sure \<Gamma> is generated. */
+int call_magic(int x) {
+  /** GHOSTUPD: "(\<acute>x < 42, id)" */
+  return magic(x);
+}