Changeset 2253


Ignore:
Timestamp:
Jul 24, 2012, 7:40:22 PM (7 years ago)
Author:
campbell
Message:

Cminor to RTLabs is now a total function.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/goto-if.test.ma

    r1914 r2253  
    3737example e2: finishes_with (repr I32 0) ? (
    3838bind ? (snapshot state) (clight_to_cminor (simplify_program myprog'))
    39 (λp1. bind ? (snapshot state) (cminor_to_rtlabs p1)
    40  (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))).
     39(λp1. let p2 ≝ cminor_to_rtlabs p1 in
     40  exec_up_to RTLabs_fullexec p2 1000 [ ])).
    4141normalize
    4242%
  • src/Clight/test/sum.test.ma

    r1876 r2253  
    2828example e2: finishes_with (repr I32 74) ? (
    2929bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
    30 (λp1. bind ? (snapshot state) (cminor_to_rtlabs p1)
    31  (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))).
     30(λp1. let p2 ≝ cminor_to_rtlabs p1 in
     31  exec_up_to RTLabs_fullexec p2 1000 [ ])).
    3232normalize
    3333%
  • src/Cminor/toRTLabs.ma

    r2252 r2253  
    390390] qed.
    391391
    392 axiom UnknownVariable : String.
    393 
    394392definition choose_reg : ∀fx.∀ty.∀e:expr ty. ∀f:partial_fn fx. expr_vars ty e (Env_has (fx_env fx)) →
    395393  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
     
    513511] qed.
    514512
    515 axiom BadCminorProgram : String.
    516513
    517514let rec add_expr (fx:fixed) (ty:typ) (e:expr ty)
     
    602599] qed.
    603600
    604 axiom UnknownLabel : String.
    605 axiom ReturnMismatch : String.
    606 
    607601definition return_ok ≝
    608602λt,s. match s with [ St_return oe ⇒ rettyp_match t oe | _ ⇒ True ].
     
    728722
    729723
    730 let rec add_stmt (fx:fixed) (s:stmt) (Env:stmts_inv fx s) (f:partial_fn fx) on s : res (Σf':partial_fn fx. add_stmt_inv fx s f f')
    731 match s return λs.stmts_inv fx s → res (Σf':partial_fn fx. add_stmt_inv … s f f') with
    732 [ St_skip ⇒ λ_. OK ? «f, ?»
     724let rec add_stmt (fx:fixed) (s:stmt) (Env:stmts_inv fx s) (f:partial_fn fx) on s : Σf':partial_fn fx. add_stmt_inv fx s f f'
     725match s return λs.stmts_inv fx s → Σf':partial_fn fx. add_stmt_inv … s f f' with
     726[ St_skip ⇒ λ_. «f, ?»
    733727| St_assign t x e ⇒ λEnv.
    734728    let dst ≝ lookup_reg (fx_env fx) x t (π1 (si_vars … (π1 Env))) in
    735     OK ? «pi1 … (add_expr … e (π2 (si_vars … (π1 Env))) f dst), ?»
     729    «pi1 … (add_expr … e (π2 (si_vars … (π1 Env))) f dst), ?»
    736730| St_store t e1 e2 ⇒ λEnv.
    737731    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (si_vars … (π1 Env))) in
     
    739733    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
    740734    let f ≝ add_expr … e1 (π1 (si_vars … (π1 Env))) f «addr_reg, ?» in
    741     OK ? «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?»
     735    «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?»
    742736| St_call return_opt_id e args ⇒ λEnv.
    743737    let return_opt_reg ≝
     
    755749        «pi1 … (add_expr … ? e (π2 (π1 (si_vars … (π1 Env)))) f «fnr, ?»), ?»
    756750      ] in
    757     OK ? «pi1 … (add_exprs … args (π2 (si_vars … (π1 Env))) args_regs ? f ?), ?»
    758 (*
    759 | St_tailcall e args ⇒ λEnv.
    760     let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
    761     let f ≝
    762       match expr_is_Id ? e with
    763       [ Some id ⇒ add_fresh_to_graph … (λ_. St_tailcall_id id args_regs) f ??
    764       | None ⇒
    765         let ❬f,fnr❭ ≝ choose_reg … e f (π1 (π1 Env)) in
    766         let f ≝ add_fresh_to_graph … (λ_. St_tailcall_ptr fnr args_regs) f ?? in
    767         «pi1 … (add_expr ? env ? e (π1 (π1 Env)) f «fnr, ?»), ?»
    768       ] in
    769     OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
    770 *)
     751    «pi1 … (add_exprs … args (π2 (si_vars … (π1 Env))) args_regs ? f ?), ?»
    771752| St_seq s1 s2 ⇒ λEnv.
    772     do f2 ← add_stmt … s2 ? f;
    773     do f1 ← add_stmt … s1 ? f2;
    774       OK ? «pi1 … f1, ?»
     753    let f2 ≝ add_stmt … s2 ? f in
     754    let f1 ≝ add_stmt … s1 ? f2 in
     755      «pi1 … f1, ?»
    775756| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    776757    let l_next ≝ pf_entry … f in
    777     do f2 ← add_stmt … s2 (π2 (π2 Env)) f;
     758    let f2 ≝ add_stmt … s2 (π2 (π2 Env)) f in
    778759    let l2 ≝ pf_entry … f2 in
    779760    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
    780     do f1 ← add_stmt … s1 (π1 (π2 Env)) f;
     761    let f1 ≝ add_stmt … s1 (π1 (π2 Env)) f in
    781762    let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in
    782763    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
    783     OK ? «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?»
    784 | St_return opt_e ⇒ λEnv. OK ? (add_return fx opt_e f Env)
    785 (*let f0 ≝ f in
    786     let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
    787     match opt_e return λo. stmt_inv ? (St_return o) → res (Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f') with
    788     [ None ⇒ λEnv. OK ? «pi1 … f, ?»
    789     | Some e ⇒
    790         match fx_rettyp … f with
    791         [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
    792         | Some r ⇒
    793             match e return λe.stmt_inv fx (St_return (Some ? e)) → res (Σf':partial_fn fx.add_stmt_inv … (St_return (Some ? e)) f0 f') with
    794             [ mk_DPair ty e ⇒ λEnv.
    795                 match typ_eq (\snd r) ty with
    796                 [ inl E ⇒ let f ≝ add_expr … ty e ? f «\fst r, ? E (* XXX E goes missing if I don't use it! *)» in
    797                           OK ? «pi1 … f, ?»
    798                 | inr _ ⇒ Error ? (msg ReturnMismatch)
    799                 ]
    800             ]
    801         ]
    802     ]*)
     764    «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?»
     765| St_return opt_e ⇒ λEnv. add_return fx opt_e f Env
    803766| St_label l s' ⇒ λEnv.
    804     do f ← add_stmt … s' (π2 Env) f;
     767    let f ≝ add_stmt … s' (π2 Env) f in
    805768    let l' ≝ lookup_label (fx_lenv fx) l ? in
    806     OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
     769    «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
    807770| St_goto l ⇒ λEnv.
    808771    let l' ≝ lookup_label (fx_lenv fx) l ? in
    809     OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
     772    «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
    810773| St_cost l s' ⇒ λEnv.
    811     do f ← add_stmt … s' (π2 Env) f;
    812     OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
     774    let f ≝ add_stmt … s' (π2 Env) f in
     775    «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
    813776] Env.
    814777try @(π2 Env)
     
    824787| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
    825788| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
     789| @sym_eq @(All2_length … (pi2 ?? args_regs))
    826790| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
    827 | @sym_eq @(All2_length … (pi2 ?? args_regs))
    828791| @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
    829792| @(π1 (π1 (si_vars … (π1 Env))))
     
    832795  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (pi2 ?? f2))
    833796  ]
    834 | #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
     797| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
    835798| #l #H cases (Exists_append … H)
    836799  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f1))
    837800  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f2))
    838801  ]
    839 | @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
    840802| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
    841 | @(si_labels … (π1 Env))
     803| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
    842804| @(pi2 … (pf_entry …))
    843805| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
    844806        | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f))
    845807        ]
     808| @(si_labels … (π1 Env))
    846809| #l1 #H whd %2 @lookup_label_lpresent
    847810| @(si_labels … (π1 Env))
     
    881844    l
    882845    l in
    883 do f ← add_stmt fixed (f_body f) ? emptyfn;
    884 OK ? (mk_internal_function
     846let f ≝ add_stmt fixed (f_body f) ? emptyfn in
     847  mk_internal_function
    885848    (pf_labgen … f)
    886849    (pf_reggen … f)
     
    894857    (pf_entry … f)
    895858    (pf_exit … f)
    896   ).
    897 [ -emptyfn @(stmt_P_mp … (f_inv f))
     859  .
     860[ #l #s #E @(labels_P_mp … (pf_closed … f l s E))
     861  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
     862  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
     863  #P' @P'
     864  | cases (label_env_contents … (sym_eq ??? El) l ?)
     865    [ #H @H
     866    | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
     867    | whd >H % #E' destruct (E')
     868    ]
     869  ]
     870  ]
     871| -emptyfn @(stmt_P_mp … (f_inv f))
    898872  #s * #V #L #R %
    899873  [ @(stmt_vars_mp … V)
     
    910884  | cases s in R ⊢ %; //
    911885  ]
    912 | #l #s #E @(labels_P_mp … (pf_closed … f l s E))
    913   #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
    914   [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
    915   #P' @P'
    916   | cases (label_env_contents … (sym_eq ??? El) l ?)
    917     [ #H @H
    918     | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
    919     | whd >H % #E' destruct (E')
    920     ]
    921   ]
    922   ]
    923886| #id #ty #r #H #L cases (populate_env_list … (sym_eq … E2) … H L)
    924887  [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1)
     
    945908qed.
    946909
    947 definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
    948 λp.transform_partial_program … p (λ_. transf_partial_fundef … c2ra_function).
     910definition cminor_noinit_to_rtlabs : Cminor_noinit_program → RTLabs_program ≝
     911λp.transform_program … p (λ_. transf_fundef … c2ra_function).
    949912
    950913include "Cminor/initialisation.ma".
    951914
    952 definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
     915definition cminor_to_rtlabs : Cminor_program → RTLabs_program ≝
    953916λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
  • src/compiler.ma

    r2205 r2253  
    1313  let p ≝ program_switch_removal p in
    1414  ! p ← clight_to_cminor p;
    15   ! p ← cminor_to_rtlabs p;
     15  let p ≝ cminor_to_rtlabs p in
    1616  return 〈p',p〉.
    1717
Note: See TracChangeset for help on using the changeset viewer.