source: Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma @ 1095

include "utilities/lists.ma".
include "common/Globalenvs.ma".
include "Cminor/syntax.ma".
include "RTLabs/syntax.ma".

definition env ≝ identifier_map SymbolTag register.
definition label_env ≝ identifier_map SymbolTag label.
definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
λen,gen. foldr ??
 (λidt,rsengen.
   let 〈id,ty〉 ≝ idt in
   let 〈rs,en,gen〉 ≝ rsengen in
   let 〈r,gen'〉 ≝ fresh … gen in
     〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉.

lemma populates_env : ∀l,e,u,l',e',u'.
  populate_env e u l = 〈l',e',u'〉 →
  ∀i. Exists ? (λx.\fst x = i) l →
      present ?? e' i.
#l elim l
[ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) *
| * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?);
  * [ whd in ⊢ (??%? → ?) #E1 <E1
      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z
      whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E
      whd in E:(??%?);
      >(?:e' = add ?? y id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
      whd >lookup_add_hit % #A destruct
    | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl)
      lapply (refl ? (populate_env e u tl))
      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *)
      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u''
      whd in ⊢ (??%? → ?) #E
      >(?:e' = add ?? e1 id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
      @lookup_add_oblivious
      @(IH … E1 ? H)
    ]
] qed.

lemma populate_extends : ∀l,e,u,l',e',u'.
  populate_env e u l = 〈l',e',u'〉 →
  ∀i. present ?? e i → present ?? e' i.
#l elim l 
[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
| * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
  change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl)
  lapply (refl ? (populate_env e u tl))
  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0
  >E0 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u0) #i1 #u1 #E
  whd in E:(??%?)
  >(?:e' = add ?? e0 id i1) [ 2: destruct (E) @refl ]
  #i #H @lookup_add_oblivious @(IH … E0) @H
] qed.
      
definition  populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝
λen,gen. foldr ??
 (λid,engen.
   let 〈en,gen〉 ≝ engen in
   let 〈r,gen'〉 ≝ fresh … gen in
     〈add ?? en id r, gen'〉) 〈en, gen〉.

lemma lookup_sigma : ∀tag,A,m. ∀i:(Σl:identifier tag. lookup tag A m l ≠ None ?).
  lookup tag A m i ≠ None ?.
#tag #A #m * #i #H @H
qed.

definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝
λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
cases H #H'  cases (H' (refl ??)) qed.


(* Add a statement to the graph, *without* updating the entry label. *)
definition fill_in_statement : label → statement → internal_function → internal_function ≝
λl,s,f.
  mk_internal_function (f_labgen f) (f_reggen f)
                       (f_result f) (f_params f) (f_locals f)
                       (f_stacksize f) (add ?? (f_graph f) l s)
                       (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?).
@lookup_add_oblivious @lookup_sigma
qed.

(* Add a statement to the graph, making it the entry label. *)
definition add_to_graph : label → statement → internal_function → internal_function ≝
λl,s,f.
  mk_internal_function (f_labgen f) (f_reggen f)
                       (f_result f) (f_params f) (f_locals f)
                       (f_stacksize f) (add ?? (f_graph f) l s)
                       (dp ?? l ?) (dp ?? (f_exit f) ?).
[ >lookup_add_hit % #E destruct
| @lookup_add_oblivious @lookup_sigma
] qed.

(* Add a statement with a fresh label to the start of the function.  The
   statement is parametrised by the *next* instruction's label. *)
definition add_fresh_to_graph : (label → statement) → internal_function → internal_function ≝
λs,f.
  let 〈l,g〉 ≝ fresh … (f_labgen f) in
  let s' ≝ s (f_entry f) in
    (mk_internal_function g (f_reggen f)
                       (f_result f) (f_params f) (f_locals f)
                       (f_stacksize f) (add ?? (f_graph f) l s')
                       (dp ?? l ?) (dp ?? (f_exit f) ?)).
[ >lookup_add_hit % #E destruct
| @lookup_add_oblivious @lookup_sigma
] qed.

definition fresh_reg : internal_function → typ → register × internal_function ≝
λf,ty.
  let 〈r,g〉 ≝ fresh … (f_reggen f) in
    〈r, mk_internal_function (f_labgen f) g
                       (f_result f) (f_params f) (〈r,ty〉::(f_locals f))
                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.

axiom UnknownVariable : String.

definition choose_reg : ∀env:env.∀ty.∀e:expr ty. internal_function → expr_vars ty e (present ?? env) → register × internal_function ≝
λenv,ty,e,f.
  match e return λty,e. expr_vars ty e (present ?? env) → register × internal_function with
  [ Id _ i ⇒ λEnv. 〈lookup' env i Env, f〉
  | _ ⇒ λ_.fresh_reg f ty
  ].
  
let rec foldr_all (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → B → B) (b:B) (l:list A) (H:All ? P l) on l :B ≝  
 match l return λx.All ? P x → B with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) (foldr_all A B P f b l (proj2 … H))] H.

definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ].

definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t).
                         internal_function → All ? (exprtyp_present env) es →
                         list register × internal_function ≝
λenv,es,f,Env.
  foldr_all (Σt:typ.expr t) ??
    (λe,p,acc. let 〈rs,f〉 ≝ acc in
             let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg env t e f ? ] p in
             〈r::rs,f'〉) 〈[ ], f〉 es Env.
@p qed.

lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.


lemma choose_regs_length : ∀env,es,f,p,rs,f'.
  choose_regs env es f p = 〈rs,f'〉 → |es| = |rs|.
#env #es #f elim es
[ #p #rs #f normalize #E destruct @refl
| * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E
  cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
  cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
  destruct (E4) skip (E1 E3) @eq_f @IH
  [ @(proj2 … p)
  | 3: @sym_eq @E1
  | 2: skip
  ]
] qed.

axiom BadCminorProgram : String.

let rec add_expr (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:internal_function) on e: internal_function ≝
match e return λty,e.expr_vars ty e (present ?? env) → internal_function with
[ Id _ i ⇒ λEnv.
    let r ≝ lookup' env i Env in
    match register_eq r dst with
    [ inl _ ⇒ f
    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
    ]
| Cst _ c ⇒ λ_. add_fresh_to_graph (St_const dst c) f
| Op1 _ _ op e' ⇒ λEnv.
    let 〈r,f〉 ≝ choose_reg env ? e' f Env in
    let f ≝ add_fresh_to_graph (St_op1 op dst r) f in
    add_expr env ? e' Env r f
| Op2 _ _ _ op e1 e2 ⇒ λEnv.
    let 〈r1,f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in
    let 〈r2,f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in
    let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in
    let f ≝ add_expr env ? e2 (proj2 … Env) r2 f in
    add_expr env ? e1 (proj1 … Env) r1 f
| Mem _ _ q e' ⇒ λEnv.
    let 〈r,f〉 ≝ choose_reg env ? e' f Env in
    let f ≝ add_fresh_to_graph (St_load q r dst) f in
    add_expr env ? e' Env r f
| Cond _ _ _ e' e1 e2 ⇒ λEnv.
    let resume_at ≝ f_entry f in
    let f ≝ add_expr env ? e2 (proj2 … Env) dst f in
    let lfalse ≝ f_entry f in
    let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in
    let f ≝ add_expr env ? e1 (proj2 … (proj1 … Env)) dst f in
    let 〈r,f〉 ≝ choose_reg env ? e' f (proj1 … (proj1 … Env)) in
    let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in
    add_expr env ? e' (proj1 … (proj1 … Env)) r f
| Ecost _ l e' ⇒ λEnv.
    let f ≝ add_expr env ? e' Env dst f in
    add_fresh_to_graph (St_cost l) f
] Env.

let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es)
                  (dsts:list register) (pf:|es|=|dsts|) (f:internal_function) on es: internal_function ≝
match es return λes.All ?? es → |es|=|dsts| → ? with
[ nil ⇒ λ_. match dsts return λx. ?=|x| → ? with [ nil ⇒ λ_. f | cons _ _ ⇒ λpf.⊥ ]
| cons e et ⇒ λEnv.
    match dsts return λx. ?=|x| → ? with
    [ nil ⇒ λpf.⊥
    | cons r rt ⇒ λpf.
        let f ≝ add_exprs env et ? rt ? f in
        match e return λe.? → ? with [ dp ty e ⇒ λEnv. add_expr env ty e ? r f ] (proj1 ?? Env)
    ]
] Env pf.
[ 1,2,3: normalize in pf; destruct //
| whd in Env @(proj2 … Env)
| normalize in pf; destruct @e0 ] qed.

axiom UnknownLabel : String.
axiom ReturnMismatch : String.

notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
 with precedence 10
for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
        λ${ident E}.$s ] (refl ? $t) }.

let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_vars s (present ?? env)) (exits:list label) (f:internal_function) on s : res internal_function ≝
match s return λs.stmt_vars s (present ?? env) → res internal_function with
[ St_skip ⇒ λ_. OK ? f
| St_assign _ x e ⇒ λEnv.
    let dst ≝ lookup' env x (proj1 … Env) in
    OK ? (add_expr env ? e (proj2 … Env) dst f)
| St_store _ _ q e1 e2 ⇒ λEnv.
    let 〈val_reg, f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in
    let 〈addr_reg, f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in
    let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in
    let f ≝ add_expr env ? e1 (proj1 … Env) addr_reg f in
    OK ? (add_expr env ? e2 (proj2 … Env) val_reg f)
| St_call return_opt_id e args ⇒ λEnv.
    let return_opt_reg ≝
      match return_opt_id return λo. ? → ? with
      [ None ⇒ λ_. None ?
      | Some id ⇒ λEnv. Some ? (lookup' env id ?)
      ] Env in
    let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in
    let f ≝
      match e with
      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
      | _ ⇒ 
        let 〈fnr, f〉 ≝ choose_reg env ? e f (proj2 … (proj1 … Env)) in
        let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in
        add_expr env ? e (proj2 … (proj1 … Env)) fnr f
      ] in
    OK ? (add_exprs env args (proj2 … Env) args_regs ? f)
| St_tailcall e args ⇒ λEnv.
    let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in
    let f ≝
      match e with
      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
      | _ ⇒ 
        let 〈fnr, f〉 ≝ choose_reg env ? e f (proj1 … Env) in
        let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in
        add_expr env ? e (proj1 … Env) fnr f
      ] in
    OK ? (add_exprs env args (proj2 … Env) args_regs ? f)
| St_seq s1 s2 ⇒ λEnv.
    do f ← add_stmt env label_env s2 (proj2 … Env) exits f;
    add_stmt env label_env s1 (proj1 … Env) exits f
| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    let l_next ≝ f_entry f in
    do f ← add_stmt env label_env s2 (proj2 … Env) exits f;
    let l2 ≝ f_entry f in
    let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in
    do f ← add_stmt env label_env s1 (proj2 … (proj1 … Env)) exits f;
    let 〈r,f〉 ≝ choose_reg env ? e f (proj1 … (proj1 … Env)) in
    let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in
    OK ? (add_expr env ? e (proj1 … (proj1 … Env)) r f)
| St_loop s ⇒ λEnv.
    let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *)
    let l_loop ≝ f_entry f in
    do f ← add_stmt env label_env s Env exits f;
    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
| St_block s ⇒ λEnv.
    add_stmt env label_env s Env ((f_entry f)::exits) f
| St_exit n ⇒ λEnv.
    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f)
| St_switch sz sg e tab n ⇒ λEnv.
    let 〈r,f〉 ≝ choose_reg env ? e f Env in
    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in
    do f ← foldr ?? (λcs,f.
      do f ← f;
      let 〈i,n〉 ≝ cs in
      let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
      let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in
      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
      let f ≝ add_fresh_to_graph (St_cond br l_case) f in
      let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in
        OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab;
    OK ? (add_expr env ? e Env r f)
| St_return opt_e ⇒
    let f ≝ add_fresh_to_graph (λ_. St_return) f in
    match opt_e return λo. ? → ? with
    [ None ⇒ λEnv. OK ? f
    | Some e ⇒
        match f_result f with
        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
        | Some r ⇒ match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ? e ? (\fst r) f) ]
        ]
    ]
| St_label l s' ⇒ λEnv.
    do f ← add_stmt env label_env s' Env exits f;
    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
| St_goto l ⇒ λEnv.
    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
    OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f)
| St_cost l s' ⇒ λEnv.
    do f ← add_stmt env label_env s' Env exits f;
    OK ? (add_fresh_to_graph (St_cost l) f)
] Env.
[ -f @(choose_regs_length … (sym_eq … Eregs))
| whd in Env @(proj1 … (proj1 … Env))
| -f @(choose_regs_length … (sym_eq … Eregs))
| @(λ_. St_skip l_next)
| @(St_skip (f_entry f))
| @St_skip
| @(λ_. St_skip l)
| @(λ_. St_skip l_default)
| whd in Env @Env
| @(St_skip (f_entry f))
| @(λ_.St_skip l')
] qed. 

(* Get labels from a Cminor statement. *)
let rec labels_of (s:stmt) : list ident ≝
match s with
[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
| St_loop s ⇒ labels_of s
| St_block s ⇒ labels_of s
| St_label l s ⇒ l::(labels_of s)
| St_cost _ s ⇒ labels_of s
| _ ⇒ [ ]
].

notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
 with precedence 10
for @{ match $t return λx.x = $t → ? with [ pair ${fresh xy} ${ident z} ⇒
       match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒
        λ${ident E}.$s ] ] (refl ? $t) }.


definition c2ra_function (*: internal_function → internal_function*) ≝
λf.
let labgen0 ≝ new_universe LabelTag in
let reggen0 ≝ new_universe RegisterTag in
let cminor_labels ≝ labels_of (f_body f) in
let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
let 〈result, locals, reggen〉 ≝
  match f_return f with
  [ None ⇒ 〈None ?, locals0, reggen2〉
  | Some ty ⇒
      let 〈r,gen〉 ≝ fresh … reggen2 in
        〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in
let 〈label_env, labgen1〉 ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
let 〈l,labgen〉 ≝ fresh … labgen1 in
let emptyfn ≝
  mk_internal_function
    labgen
    reggen
    result
    params
    locals
    (f_stacksize f)
    (add ?? (empty_map …) l St_return)
    l
    l in
do f ← add_stmt env label_env (f_body f) ? [ ] emptyfn;
do u1 ← check_universe_ok ? (f_labgen f);
do u2 ← check_universe_ok ? (f_reggen f);
OK ? f
.
[ @(stmt_vars_mp … (f_bound f))
  #i #H cases (Exists_append … H)
  [ #H1 @(populate_extends ?????? (sym_eq … E2))
        @(populates_env … (sym_eq … E1)) @H1
  | #H1 @(populates_env … (sym_eq … E2)) @H1
  ]
| *: >lookup_add_hit % #E destruct
]
qed.

definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
transform_partial_program ???
  (transf_partial_fundef ?? c2ra_function).

include "Cminor/initialisation.ma".

definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
λp. let p' ≝ replace_init p in cminor_to_rtlabs p.