Changeset 2992 for src/Cminor

Timestamp:

Mar 28, 2013, 12:07:56 AM (7 years ago)

Author:

campbell

Message:

Add "only one return" invariant to RTLabs functions.

File:

• src/Cminor/toRTLabs.ma (modified) (24 diffs)

src/Cminor/toRTLabs.ma

@@ -181 +181 @@
 ; pf_entry     : Σl:label. present ?? pf_graph l
 ; pf_exit      : Σl:label. present ?? pf_graph l
+; pf_only_exit : ∀l. lookup … pf_graph l = Some ? St_return → l = pf_exit
 }.
 
@@ -247 +248 @@
 ] qed.
 
+definition not_return : statement → Prop ≝
+λs. match s with [ St_return ⇒ False | _ ⇒ True ].
+
 (* Add a statement to the graph, *without* updating the entry label. *)
-definition fill_in_statement : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
+definition fill_in_statement : ∀fx. label → ∀s:statement. not_return s → ∀f:partial_fn fx.
   labels_present (pf_graph … f) s →
   statement_typed_in … f s →
   Σf':partial_fn fx. fn_contains … f f' ≝
-λfx,l,s,f,p,tp.
+λfx,l,s,NR,f,p,tp.
   mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
                 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                 (pf_stacksize … f) (add ?? (pf_graph … f) l s) ?
                 (mk_goto_map … (pf_gotos … f) ??) «pf_labels … f, ?» ?
-                «pf_entry … f, ?» «pf_exit … f, ?».
+                «pf_entry … f, ?» «pf_exit … f, ?» ?.
 [ @add_statement_inv @p
 | @gm_img
@@ -264 +268 @@
 | @forall_nodes_add //
 | 6,7: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
+| #l' #L cases (lookup_add_cases ??????? L)
+  [ * #_ #R @⊥ <R in NR; *
+  | @(pf_only_exit … f)
+  ]
 | % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ] 
 ] qed.
 
 (* Add a statement to the graph, making it the entry label. *)
-definition add_to_graph : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
+definition add_to_graph : ∀fx. label → ∀s:statement. not_return s → ∀f:partial_fn fx.
   labels_present (pf_graph … f) s →
   statement_typed_in … f s →
   Σf':partial_fn fx. fn_contains … f f' ≝
-λfx,l,s,f,p,tl.
+λfx,l,s,NR,f,p,tl.
   mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
                 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                 (pf_stacksize … f) (add ?? (pf_graph … f) l s) ????
-                «l, ?» «pf_exit … f, ?».
+                «l, ?» «pf_exit … f, ?» ?.
 [ @add_statement_inv @p
 | cases (pf_gotos … f) #m #dom #img %
@@ -284 +292 @@
 | whd >lookup_add_hit % #E destruct
 | @lookup_add_oblivious @(pi2 … (pf_exit … f))
+| #l' #L cases (lookup_add_cases ??????? L)
+  [ * #_ #R @⊥ <R in NR; *
+  | @(pf_only_exit … f)
+  ]
 | % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
 ] qed.
@@ -297 +309 @@
                 (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f)
                 (pf_labels … f) (pf_typed … f)
-                «l, PR» (pf_exit … f).
+                «l, PR» (pf_exit … f) (pf_only_exit … f).
 % //
 qed.
@@ -306 +318 @@
   (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
   (∀l. statement_typed_in … f (s l)) →
+  (∀l. not_return (s l)) →
   Σf':partial_fn fx. fn_contains … f f' ≝
-λfx,s,f,p,tp.
+λfx,s,f,p,tp,NR.
   let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
   let s' ≝ s (pf_entry … f) in
@@ -313 +326 @@
                    (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                    (pf_stacksize … f) (add ?? (pf_graph … f) l s') ????
-                   «l, ?» «pf_exit … f, ?»).
+                   «l, ?» «pf_exit … f, ?» ?).
 [ 4: cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L)
 | % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
@@ -322 +335 @@
 | whd >lookup_add_hit % #E destruct
 | @lookup_add_oblivious @(pi2 … (pf_exit …))
+| #l' #L cases (lookup_add_cases ??????? L)
+  [ * #_ #R @⊥ lapply (NR (pf_entry fx f)) whd in R:(???%); <R *
+  | @(pf_only_exit … f)
+  ]
 ] qed.
 
@@ -352 +369 @@
     «mk_partial_fn fx
        (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ?
-       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f) (pf_labels … f) ? (pf_entry … f) (pf_exit … f), ?»
+       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f) (pf_labels … f) ? (pf_entry … f) (pf_exit … f) (pf_only_exit … f), ?»
   in
     ❬f' , ?(*«r, ?»*)❭.
@@ -486 +503 @@
     match register_eq r dst with
     [ inl _ ⇒ «f, ?»
-    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
+    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ???), ?»
     ]
-| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ??, ?»
+| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ???, ?»
 | Op1 t t' op e' ⇒ λEnv,dst.
     let ❬f,r❭ ≝ choose_reg … e' f Env in
-    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
+    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ??? in
     let f ≝ add_expr … ? e' Env f «r, ?» in
       «pi1 … f, ?»
@@ -497 +514 @@
     let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
     let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
-    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
+    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ??? in
     let f ≝ add_expr … ? e2 (proj2 … Env) f «r2, ?» in
     let f ≝ add_expr … ? e1 (proj1 … Env) f «r1, ?» in
@@ -503 +520 @@
 | Mem t e' ⇒ λEnv,dst.
     let ❬f,r❭ ≝ choose_reg … e' f Env in
-    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
+    let f ≝ add_fresh_to_graph … (St_load t r dst) f ??? in
     let f ≝ add_expr … ? e' Env f «r,?» in
       «pi1 … f, ?»
@@ -510 +527 @@
     let f ≝ add_expr … ? e2 (proj2 … Env) f dst in
     let lfalse ≝ pf_entry … f in
-    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
+    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ??? in
     let f ≝ add_expr … ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
     let ❬f,r❭ ≝ choose_reg … e' f ? in
-    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
+    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ??? in
     let f ≝ add_expr … ? e' (proj1 … (proj1 … Env)) f «r, ?» in
       «pi1 … f, ?»
 | Ecost _ l e' ⇒ λEnv,dst.
     let f ≝ add_expr … ? e' Env f dst in
-    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
+    let f ≝ add_fresh_to_graph … (St_cost l) f ??? in
       «f, ?»
 ] Env dst.
@@ -678 +695 @@
   (pf_result … f) (pf_envok … f) (pf_stacksize … f) (pf_graph … f)
   (pf_closed … f) (pf_gotos …  f) «add … (pf_labels … f) l (pf_entry … f), ?»
-  (pf_typed … f) (pf_entry … f) (pf_exit … f).
+  (pf_typed … f) (pf_entry … f) (pf_exit … f) (pf_only_exit … f).
 #l1 #l2 cases (identifier_eq … l2 (pf_entry … f))
 [ #E destruct #L @(pi2 … (pf_entry … f))
@@ -695 +712 @@
     (mk_partial_fn fx g (pf_reggen … f)
                    (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
-                   (pf_stacksize … f) (add ?? (pf_graph … f) l St_return) ?
+                   (pf_stacksize … f) (add ?? (pf_graph … f) l (St_skip l)) ?
                    (mk_goto_map … (add … (pf_gotos … f) l dest) ??)
                    «pf_labels … f, ?» ?
-                   «l, ?» «pf_exit … f, ?»).
+                   «l, ?» «pf_exit … f, ?» ?).
 [ % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
-| @add_statement_inv @I
+| #l' #s #L cases (lookup_add_cases ??????? L)
+  [ * #E1 #E2 destruct //
+  | #L' @(labels_P_mp … (pf_closed … f … L')) /2/
+  ]
 | #l1 #l2 cases (identifier_eq … l1 l)
   [ #E destruct >lookup_add_hit #E destruct @PR
@@ -713 +733 @@
 | whd >lookup_add_hit % #E destruct
 | @lookup_add_oblivious @(pi2 … (pf_exit …))
+| #l' #L cases (lookup_add_cases ??????? L)
+  [ * #_ #R lapply (eq_to_jmeq ??? R) -R #R destruct (* XXX discr hack *)
+  | @(pf_only_exit … f)
+  ]
 ] qed.
 
@@ -731 +755 @@
     let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (si_vars … (π1 Env))) in
     let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (si_vars … (π1 Env))) in
-    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
+    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ??? in
     let f ≝ add_expr … e1 (π1 (si_vars … (π1 Env))) f «addr_reg, ?» in
     «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?»
@@ -743 +767 @@
     let f ≝
       match expr_is_cst_ident ? e with
-      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
+      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ???
       | None ⇒ 
         let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (si_vars … (π1 Env)))) in
-        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
+        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ??? in
         «pi1 … (add_expr … ? e (π2 (π1 (si_vars … (π1 Env)))) f «fnr, ?»), ?»
       ] in
@@ -761 +785 @@
     let f1 ≝ add_stmt … s1 (π1 (π2 Env)) f in
     let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in
-    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
+    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ??? in
     «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?»
 | St_return opt_e ⇒ λEnv. add_return fx opt_e f Env
@@ -771 +795 @@
 | St_cost l s' ⇒ λEnv.
     let f ≝ add_stmt … s' (π2 Env) f in
-    «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
+    «pi1 … (add_fresh_to_graph … (St_cost l) f ???), ?»
 ] Env.
 try @(π2 Env)
@@ -834 +858 @@
 λfx,f,PR.
 fold_inf ? (Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l) ? (pf_gotos … f)
-  (λl,l',H,f'. «fill_in_statement fx l (St_skip (lookup_present ?? (pf_labels … f') l' ?)) f' ??, ?»)
+  (λl,l',H,f'. «fill_in_statement fx l (St_skip (lookup_present ?? (pf_labels … f') l' ?)) I f' ??, ?»)
   «f, λx,H.H».
 [ #l #PR' @(pi2 … f') @PR'
@@ -874 +898 @@
     ?
     l
-    l in
+    l
+    ? in
 let f ≝ add_stmt fixed (f_body f) ? emptyfn in
 let f ≝ patch_gotos … f ? in
@@ -889 +914 @@
     (pf_entry … f)
     (pf_exit … f)
+    (pf_only_exit … f)
   .
 [ #l1 #l2 #L
@@ -934 +960 @@
   ]
 | 9,10: whd >lookup_add_hit % #E destruct
+| #l' #L cases (lookup_add_cases ??????? L)
+  [ *#E >E #_ %
+  | #L' whd in L':(??%?); destruct
+  ]
 | % @refl
 ]