Changeset 2992


Ignore:
Timestamp:
Mar 28, 2013, 12:07:56 AM (4 years ago)
Author:
campbell
Message:

Add "only one return" invariant to RTLabs functions.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2971 r2992  
    181181; pf_entry     : Σl:label. present ?? pf_graph l
    182182; pf_exit      : Σl:label. present ?? pf_graph l
     183; pf_only_exit : ∀l. lookup … pf_graph l = Some ? St_return → l = pf_exit
    183184}.
    184185
     
    247248] qed.
    248249
     250definition not_return : statement → Prop ≝
     251λs. match s with [ St_return ⇒ False | _ ⇒ True ].
     252
    249253(* Add a statement to the graph, *without* updating the entry label. *)
    250 definition fill_in_statement : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
     254definition fill_in_statement : ∀fx. label → ∀s:statement. not_return s → ∀f:partial_fn fx.
    251255  labels_present (pf_graph … f) s →
    252256  statement_typed_in … f s →
    253257  Σf':partial_fn fx. fn_contains … f f' ≝
    254 λfx,l,s,f,p,tp.
     258λfx,l,s,NR,f,p,tp.
    255259  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
    256260                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
    257261                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ?
    258262                (mk_goto_map … (pf_gotos … f) ??) «pf_labels … f, ?» ?
    259                 «pf_entry … f, ?» «pf_exit … f, ?».
     263                «pf_entry … f, ?» «pf_exit … f, ?» ?.
    260264[ @add_statement_inv @p
    261265| @gm_img
     
    264268| @forall_nodes_add //
    265269| 6,7: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
     270| #l' #L cases (lookup_add_cases ??????? L)
     271  [ * #_ #R @⊥ <R in NR; *
     272  | @(pf_only_exit … f)
     273  ]
    266274| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
    267275] qed.
    268276
    269277(* Add a statement to the graph, making it the entry label. *)
    270 definition add_to_graph : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
     278definition add_to_graph : ∀fx. label → ∀s:statement. not_return s → ∀f:partial_fn fx.
    271279  labels_present (pf_graph … f) s →
    272280  statement_typed_in … f s →
    273281  Σf':partial_fn fx. fn_contains … f f' ≝
    274 λfx,l,s,f,p,tl.
     282λfx,l,s,NR,f,p,tl.
    275283  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
    276284                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
    277285                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ????
    278                 «l, ?» «pf_exit … f, ?».
     286                «l, ?» «pf_exit … f, ?» ?.
    279287[ @add_statement_inv @p
    280288| cases (pf_gotos … f) #m #dom #img %
     
    284292| whd >lookup_add_hit % #E destruct
    285293| @lookup_add_oblivious @(pi2 … (pf_exit … f))
     294| #l' #L cases (lookup_add_cases ??????? L)
     295  [ * #_ #R @⊥ <R in NR; *
     296  | @(pf_only_exit … f)
     297  ]
    286298| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
    287299] qed.
     
    297309                (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f)
    298310                (pf_labels … f) (pf_typed … f)
    299                 «l, PR» (pf_exit … f).
     311                «l, PR» (pf_exit … f) (pf_only_exit … f).
    300312% //
    301313qed.
     
    306318  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
    307319  (∀l. statement_typed_in … f (s l)) →
     320  (∀l. not_return (s l)) →
    308321  Σf':partial_fn fx. fn_contains … f f' ≝
    309 λfx,s,f,p,tp.
     322λfx,s,f,p,tp,NR.
    310323  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
    311324  let s' ≝ s (pf_entry … f) in
     
    313326                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
    314327                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ????
    315                    «l, ?» «pf_exit … f, ?»).
     328                   «l, ?» «pf_exit … f, ?» ?).
    316329[ 4: cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L)
    317330| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
     
    322335| whd >lookup_add_hit % #E destruct
    323336| @lookup_add_oblivious @(pi2 … (pf_exit …))
     337| #l' #L cases (lookup_add_cases ??????? L)
     338  [ * #_ #R @⊥ lapply (NR (pf_entry fx f)) whd in R:(???%); <R *
     339  | @(pf_only_exit … f)
     340  ]
    324341] qed.
    325342
     
    352369    «mk_partial_fn fx
    353370       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ?
    354        (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f) (pf_labels … f) ? (pf_entry … f) (pf_exit … f), ?»
     371       (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), ?»
    355372  in
    356373    ❬f' , ?(*«r, ?»*)❭.
     
    486503    match register_eq r dst with
    487504    [ inl _ ⇒ «f, ?»
    488     | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
     505    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ???), ?»
    489506    ]
    490 | Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ??, ?»
     507| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ???, ?»
    491508| Op1 t t' op e' ⇒ λEnv,dst.
    492509    let ❬f,r❭ ≝ choose_reg … e' f Env in
    493     let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
     510    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ??? in
    494511    let f ≝ add_expr … ? e' Env f «r, ?» in
    495512      «pi1 … f, ?»
     
    497514    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
    498515    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
    499     let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
     516    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ??? in
    500517    let f ≝ add_expr … ? e2 (proj2 … Env) f «r2, ?» in
    501518    let f ≝ add_expr … ? e1 (proj1 … Env) f «r1, ?» in
     
    503520| Mem t e' ⇒ λEnv,dst.
    504521    let ❬f,r❭ ≝ choose_reg … e' f Env in
    505     let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
     522    let f ≝ add_fresh_to_graph … (St_load t r dst) f ??? in
    506523    let f ≝ add_expr … ? e' Env f «r,?» in
    507524      «pi1 … f, ?»
     
    510527    let f ≝ add_expr … ? e2 (proj2 … Env) f dst in
    511528    let lfalse ≝ pf_entry … f in
    512     let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
     529    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ??? in
    513530    let f ≝ add_expr … ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
    514531    let ❬f,r❭ ≝ choose_reg … e' f ? in
    515     let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
     532    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ??? in
    516533    let f ≝ add_expr … ? e' (proj1 … (proj1 … Env)) f «r, ?» in
    517534      «pi1 … f, ?»
    518535| Ecost _ l e' ⇒ λEnv,dst.
    519536    let f ≝ add_expr … ? e' Env f dst in
    520     let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
     537    let f ≝ add_fresh_to_graph … (St_cost l) f ??? in
    521538      «f, ?»
    522539] Env dst.
     
    678695  (pf_result … f) (pf_envok … f) (pf_stacksize … f) (pf_graph … f)
    679696  (pf_closed … f) (pf_gotos …  f) «add … (pf_labels … f) l (pf_entry … f), ?»
    680   (pf_typed … f) (pf_entry … f) (pf_exit … f).
     697  (pf_typed … f) (pf_entry … f) (pf_exit … f) (pf_only_exit … f).
    681698#l1 #l2 cases (identifier_eq … l2 (pf_entry … f))
    682699[ #E destruct #L @(pi2 … (pf_entry … f))
     
    695712    (mk_partial_fn fx g (pf_reggen … f)
    696713                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
    697                    (pf_stacksize … f) (add ?? (pf_graph … f) l St_return) ?
     714                   (pf_stacksize … f) (add ?? (pf_graph … f) l (St_skip l)) ?
    698715                   (mk_goto_map … (add … (pf_gotos … f) l dest) ??)
    699716                   «pf_labels … f, ?» ?
    700                    «l, ?» «pf_exit … f, ?»).
     717                   «l, ?» «pf_exit … f, ?» ?).
    701718[ % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
    702 | @add_statement_inv @I
     719| #l' #s #L cases (lookup_add_cases ??????? L)
     720  [ * #E1 #E2 destruct //
     721  | #L' @(labels_P_mp … (pf_closed … f … L')) /2/
     722  ]
    703723| #l1 #l2 cases (identifier_eq … l1 l)
    704724  [ #E destruct >lookup_add_hit #E destruct @PR
     
    713733| whd >lookup_add_hit % #E destruct
    714734| @lookup_add_oblivious @(pi2 … (pf_exit …))
     735| #l' #L cases (lookup_add_cases ??????? L)
     736  [ * #_ #R lapply (eq_to_jmeq ??? R) -R #R destruct (* XXX discr hack *)
     737  | @(pf_only_exit … f)
     738  ]
    715739] qed.
    716740
     
    731755    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (si_vars … (π1 Env))) in
    732756    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (si_vars … (π1 Env))) in
    733     let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
     757    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ??? in
    734758    let f ≝ add_expr … e1 (π1 (si_vars … (π1 Env))) f «addr_reg, ?» in
    735759    «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?»
     
    743767    let f ≝
    744768      match expr_is_cst_ident ? e with
    745       [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
     769      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ???
    746770      | None ⇒
    747771        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (si_vars … (π1 Env)))) in
    748         let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
     772        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ??? in
    749773        «pi1 … (add_expr … ? e (π2 (π1 (si_vars … (π1 Env)))) f «fnr, ?»), ?»
    750774      ] in
     
    761785    let f1 ≝ add_stmt … s1 (π1 (π2 Env)) f in
    762786    let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in
    763     let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
     787    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ??? in
    764788    «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?»
    765789| St_return opt_e ⇒ λEnv. add_return fx opt_e f Env
     
    771795| St_cost l s' ⇒ λEnv.
    772796    let f ≝ add_stmt … s' (π2 Env) f in
    773     «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
     797    «pi1 … (add_fresh_to_graph … (St_cost l) f ???), ?»
    774798] Env.
    775799try @(π2 Env)
     
    834858λfx,f,PR.
    835859fold_inf ? (Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l) ? (pf_gotos … f)
    836   (λl,l',H,f'. «fill_in_statement fx l (St_skip (lookup_present ?? (pf_labels … f') l' ?)) f' ??, ?»)
     860  (λl,l',H,f'. «fill_in_statement fx l (St_skip (lookup_present ?? (pf_labels … f') l' ?)) I f' ??, ?»)
    837861  «f, λx,H.H».
    838862[ #l #PR' @(pi2 … f') @PR'
     
    874898    ?
    875899    l
    876     l in
     900    l
     901    ? in
    877902let f ≝ add_stmt fixed (f_body f) ? emptyfn in
    878903let f ≝ patch_gotos … f ? in
     
    889914    (pf_entry … f)
    890915    (pf_exit … f)
     916    (pf_only_exit … f)
    891917  .
    892918[ #l1 #l2 #L
     
    934960  ]
    935961| 9,10: whd >lookup_add_hit % #E destruct
     962| #l' #L cases (lookup_add_cases ??????? L)
     963  [ *#E >E #_ %
     964  | #L' whd in L':(??%?); destruct
     965  ]
    936966| % @refl
    937967]
  • src/RTLabs/RTLabs_syntax.ma

    r2936 r2992  
    9090; f_entry     : Σl:label. present ?? f_graph l
    9191; f_exit      : Σl:label. present ?? f_graph l
     92; f_only_exit : ∀l. lookup … f_graph l = Some ? St_return → l = f_exit
    9293}.
    9394
Note: See TracChangeset for help on using the changeset viewer.