Changeset 1206


Ignore:
Timestamp:
Sep 12, 2011, 4:20:57 PM (8 years ago)
Author:
campbell
Message:

First stage of fixing temporary generation in Clight/toCminor.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1194 r1206  
    544544axiom FIXME : String.
    545545
    546 let rec translate_statement (vars:var_types) (tmp:ident) (tmpp:ident) (s:statement) on s : res stmt ≝
     546record tmpgen : Type[0] ≝ {
     547  tmp_universe : universe SymbolTag;
     548  tmp_env : list (ident × typ)
     549}.
     550
     551definition alloc_tmp : memory_chunk → tmpgen → ident × tmpgen ≝
     552λc,g.
     553  let 〈tmp,u〉 ≝ fresh ? (tmp_universe g) in
     554  〈tmp, mk_tmpgen u (〈tmp, typ_of_memory_chunk c〉::(tmp_env g))〉.
     555
     556let rec translate_statement (vars:var_types) (u:tmpgen) (s:statement) on s : res (stmt×tmpgen) ≝
    547557match s with
    548 [ Sskip ⇒ OK ? St_skip
    549 | Sassign e1 e2 ⇒ translate_assign vars e1 e2
     558[ Sskip ⇒ OK ? 〈St_skip, u〉
     559| Sassign e1 e2 ⇒ do s' ← translate_assign vars e1 e2; OK ? 〈s',u〉
    550560| Scall ret ef args ⇒
    551561    do ef' ← translate_expr vars ef;
     
    553563    do args' ← mmap … (translate_expr_sigma vars) args;
    554564    match ret with
    555     [ None ⇒ OK ? (St_call (None ?) ef' args')
     565    [ None ⇒ OK ? 〈St_call (None ?) ef' args', u〉
    556566    | Some e1 ⇒
    557567        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
    558568        match dest with
    559         [ IdDest id ⇒ OK ? (St_call (Some ? id) ef' args')
     569        [ IdDest id ⇒ OK ? 〈St_call (Some ? id) ef' args', u〉
    560570        | MemDest r q e1' ⇒
    561             let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
    562             OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)))
     571            let 〈tmp, u〉 ≝ alloc_tmp q u in
     572            OK ? 〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉
    563573        ]
    564574    ]
    565575| Ssequence s1 s2 ⇒
    566     do s1' ← translate_statement vars tmp tmpp s1;
    567     do s2' ← translate_statement vars tmp tmpp s2;
    568     OK ? (St_seq s1' s2')
     576    do 〈s1', u〉 ← translate_statement vars u s1;
     577    do 〈s2', u〉 ← translate_statement vars u s2;
     578    OK ? 〈St_seq s1' s2', u〉
    569579| Sifthenelse e1 s1 s2 ⇒
    570580    do e1' ← translate_expr vars e1;
    571581    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    572582    [ ASTint _ _ ⇒ λe1'.
    573         do s1' ← translate_statement vars tmp tmpp s1;
    574         do s2' ← translate_statement vars tmp tmpp s2;
    575         OK ? (St_ifthenelse ?? e1' s1' s2')
     583        do 〈s1', u〉 ← translate_statement vars u s1;
     584        do 〈s2', u〉 ← translate_statement vars u s2;
     585        OK ? 〈St_ifthenelse ?? e1' s1' s2', u〉
    576586    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    577587    ] e1'
     
    580590    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    581591    [ ASTint _ _ ⇒ λe1'.
    582         do s1' ← translate_statement vars tmp tmpp s1;
     592        do 〈s1', u〉 ← translate_statement vars u s1;
    583593        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    584         OK ? (St_block
     594        OK ? St_block
    585595               (St_loop
    586                  (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))))
     596                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉
    587597    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    588598    ] e1'
     
    591601    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    592602    [ ASTint _ _ ⇒ λe1'.
    593         do s1' ← translate_statement vars tmp tmpp s1;
     603        do 〈s1',u〉 ← translate_statement vars u s1;
    594604        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    595         OK ? (St_block
     605        OK ? St_block
    596606               (St_loop
    597                  (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))))
     607                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉
    598608    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    599609    ] e1'
     
    602612    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    603613    [ ASTint _ _ ⇒ λe1'.
    604         do s1' ← translate_statement vars tmp tmpp s1;
    605         do s2' ← translate_statement vars tmp tmpp s2;
    606         do s3' ← translate_statement vars tmp tmpp s3;
     614        do 〈s1', u〉 ← translate_statement vars u s1;
     615        do 〈s2', u〉 ← translate_statement vars u s2;
     616        do 〈s3', u〉 ← translate_statement vars u s3;
    607617        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    608         OK ? (St_seq s1'
     618        OK ? St_seq s1'
    609619             (St_block
    610620               (St_loop
    611                  (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))))
     621                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉
    612622    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    613623    ] e1'
    614 | Sbreak ⇒ OK ? (St_exit 1)
    615 | Scontinue ⇒ OK ? (St_exit 0)
     624| Sbreak ⇒ OK ? 〈St_exit 1, u〉
     625| Scontinue ⇒ OK ? 〈St_exit 0, u〉
    616626| Sreturn ret ⇒
    617627    match ret with
    618     [ None ⇒ OK ? (St_return (None ?))
     628    [ None ⇒ OK ? 〈St_return (None ?), u〉
    619629    | Some e1 ⇒
    620630        do e1' ← translate_expr vars e1;
    621         OK ? (St_return (Some ? (dp … e1')))
     631        OK ? 〈St_return (Some ? (dp … e1')), u〉
    622632    ]
    623633| Sswitch e1 ls ⇒ Error ? (msg FIXME)
    624634| Slabel l s1 ⇒
    625     do s1' ← translate_statement vars tmp tmpp s1;
    626     OK ? (St_label l s1')
    627 | Sgoto l ⇒ OK ? (St_goto l)
     635    do 〈s1', u〉 ← translate_statement vars u s1;
     636    OK ? 〈St_label l s1', u〉
     637| Sgoto l ⇒ OK ? 〈St_goto l, u〉
    628638| Scost l s1 ⇒
    629     do s1' ← translate_statement vars tmp tmpp s1;
    630     OK ? (St_cost l s1')
     639    do 〈s1', u〉 ← translate_statement vars u s1;
     640    OK ? 〈St_cost l s1', u〉
    631641].
    632642
     
    650660  ]) (OK ? s) params.
    651661
    652 definition bigid1 ≝ an_identifier SymbolTag [[
     662definition bigu ≝ mk_universe SymbolTag [[
    653663false;true;false;false;
    654664false;false;false;false;
    655665false;false;false;false;
    656 false;false;false;false]].
    657 definition bigid2 ≝ an_identifier SymbolTag [[
    658 false;true;false;false;
    659 false;false;false;false;
    660 false;false;false;false;
    661 false;false;false;true]].
    662 
    663 (* FIXME: the temporary handling is nonsense, I'm afraid. *)
     666false;false;false;false]] false.
     667
     668(* FIXME: the temporary handling is a bit dodgy, I'm afraid. *)
    664669definition translate_function : list (ident×region) → function → res internal_function ≝
    665670λglobals, f.
    666671  let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
    667   let tmp ≝ bigid1 in (* FIXME *)
    668   let tmpp ≝ bigid2 in (* FIXME *)
    669   do s ← translate_statement vartypes tmp tmpp (fn_body f);
     672  let tmp ≝ mk_tmpgen bigu [ ] in (* FIXME *)
     673  do 〈s,tmp〉 ← translate_statement vartypes tmp (fn_body f);
    670674  do s ← alloc_params vartypes (fn_params f) s;
    671675  OK ? (mk_internal_function
    672676    (opttyp_of_type (fn_return f))
    673677    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
    674     (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
     678    ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
    675679    stacksize
    676680    s).
Note: See TracChangeset for help on using the changeset viewer.