Changeset 881 for src/Clight/toCminor.ma


Ignore:
Timestamp:
Jun 3, 2011, 5:35:31 PM (9 years ago)
Author:
campbell
Message:

Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r880 r881  
    146146
    147147inductive var_type : Type[0] ≝
    148 | Global : var_type
     148| Global : region → var_type
    149149| Stack  : nat → var_type
    150150| Local  : var_type
     
    166166].
    167167
    168 definition characterise_vars : list ident → function → var_types × nat ≝
     168definition characterise_vars : list (ident×region) → function → var_types × nat ≝
    169169λglobals, f.
    170   let m ≝ foldl ?? (λm,id. add ?? m id Global) (empty_map ??) globals in
     170  let m ≝ foldl ?? (λm,idr. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
    171171  let m ≝ foldl ?? (λm,v. add ?? m (\fst v) Local) m (fn_params f) in
    172172  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
     
    365365  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
    366366
     367definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
     368* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     369qed.
     370
    367371definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
    368372* [ #sz1 #sg1 | #r1 | #sz1 ]
     
    370374[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
    371375  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    372 | *; cases r1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     376| *; #P #p @(region_should_eq r1 ?? p)
    373377| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    374378] qed.
    375379
     380
     381lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
     382*
     383[ 5: #r #ty #n #r' normalize #E destruct @refl
     384| 6: #args #ret #r normalize #E destruct @refl
     385| *: normalize #a #b try #c try #d destruct
     386  [ cases a in d; normalize; cases b; normalize #E destruct
     387  | cases a in c; normalize #E destruct
     388  ]
     389] qed.
     390
    376391let rec translate_expr (vars:var_types) (e:expr) on e : res (CMexpr (typ_of_type (typeof e))) ≝
    377 match e with
     392match e return λe. res (CMexpr (typ_of_type (typeof e))) with
    378393[ Expr ed ty ⇒
    379394  match ed with
     
    383398      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    384399      match c with
    385       [ Global
     400      [ Global r
    386401          match access_mode ty with
    387           [ By_value q ⇒ OK ? (Mem ? q (Cst ? (Oaddrsymbol id zero)))
     402          [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id zero)))
    388403          | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id zero))
    389404          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
     
    391406      | Stack n ⇒
    392407          match access_mode ty with
    393           [ By_value q ⇒ OK ? (Mem ? q (Cst ? (Oaddrstack (repr n))))
     408          [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack (repr n))))
    394409          | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack (repr n)))
    395410          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
     
    399414  | Ederef e1 ⇒
    400415      do e1' ← translate_expr vars e1;
    401       do e1' ← typ_should_eq ? (ASTptr Any) ? e1';
    402       do e' ← match access_mode ty with
    403       [ By_value q ⇒ OK ? (Mem ? q e1')
    404       | By_reference _ ⇒ OK ? e1'
    405       | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
    406       ];
    407       typ_should_eq ? (typ_of_type (typeof e)) ? e'
     416      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     417      [ ASTptr r ⇒ λe1'.
     418          match access_mode ty return λx.access_mode ty = x → ? with
     419          [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1')
     420          | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉
     421          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
     422          ] (refl ? (access_mode ty))
     423      | _ ⇒ λ_. Error ? (msg TypeMismatch)
     424      ] e1'
    408425  | Eaddrof e1 ⇒
    409426      do e1' ← translate_addr vars e1;
    410       match typ_of_type (typeof e) return λx.res (CMexpr x) with
    411       [ ASTptr r ⇒ match r return λx.res (CMexpr (ASTptr x)) with [ Any ⇒ OK ? e1' | _ ⇒ Error ? (msg TypeMismatch) ]
     427      match typ_of_type ty return λx.res (CMexpr x) with
     428      [ ASTptr r ⇒
     429          match e1' with
     430          [ dp r1 e1' ⇒ region_should_eq r1 r ? e1'
     431          ]
    412432      | _ ⇒ Error ? (msg TypeMismatch)
    413433      ]
     
    419439      do e1' ← translate_expr vars e1;
    420440      do e2' ← translate_expr vars e2;
    421       translate_binop op (typeof e1) e1' (typeof e2) e2' (typeof e)
     441      translate_binop op (typeof e1) e1' (typeof e2) e2' ty
    422442  | Ecast ty1 e1 ⇒
    423443      do e1' ← translate_expr vars e1;
    424444      do e' ← translate_cast (typeof e1) ty1 e1';
    425       typ_should_eq ? (typ_of_type (typeof e)) ? e'
     445      typ_should_eq ? (typ_of_type ty) ? e'
    426446  | Econdition e1 e2 e3 ⇒
    427447      do e1' ← translate_expr vars e1;
    428448      do e2' ← translate_expr vars e2;
    429       do e2' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e2';
     449      do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
    430450      do e3' ← translate_expr vars e3;
    431       do e3' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e3';
     451      do e3' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e3';
    432452      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    433453      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3')
     
    437457      do e1' ← translate_expr vars e1;
    438458      do e2' ← translate_expr vars e2;
    439       do e2' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e2';
    440       match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type (typeof e))) with
     459      do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
     460      match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    441461      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst zero)))
    442462      | _ ⇒ λ_.Error ? (msg TypeMismatch)
     
    445465      do e1' ← translate_expr vars e1;
    446466      do e2' ← translate_expr vars e2;
    447       do e2' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e2';
    448       match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type (typeof e))) with
     467      do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
     468      match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    449469      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst one)) e2')
    450470      | _ ⇒ λ_.Error ? (msg TypeMismatch)
     
    455475      [ Tstruct _ fl ⇒
    456476          do e1' ← translate_addr vars e1;
    457           do off ← field_offset id fl;
    458           match access_mode ty with
    459           [ By_value q ⇒ OK ? (Mem ? q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off)))))
    460           | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off))))
    461           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
     477          match e1' with
     478          [ dp r e1' ⇒
     479            do off ← field_offset id fl;
     480            match access_mode ty with
     481            [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off)))))
     482            | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off))))
     483            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
     484            ]
    462485          ]
    463486      | Tunion _ _ ⇒
    464487          do e1' ← translate_addr vars e1;
    465           match access_mode ty with
    466           [ By_value q ⇒ OK ? (Mem ? q e1')
    467           | By_reference _ ⇒ OK ? e1'
    468           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
     488          match e1' with
     489          [ dp r e1' ⇒
     490            match access_mode ty return λx. access_mode ty = x → res (CMexpr (typ_of_type ty)) with
     491            [ By_value q ⇒ λ_. OK ? (Mem ?? q e1')
     492            | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈res (CMexpr (ASTptr r')) ↦ res (CMexpr (typ_of_type ty))⌉
     493            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
     494            ] (refl ? (access_mode ty))
    469495          ]
    470496      | _ ⇒ Error ? (msg BadlyTypedAccess)
    471497      ];
    472       typ_should_eq ? (typ_of_type (typeof e)) ? e'
     498      typ_should_eq ? (typ_of_type ty) ? e'
    473499  | Ecost l e1 ⇒
    474500      do e1' ← translate_expr vars e1;
    475501      do e' ← OK ? (Ecost ? l e1');
    476       typ_should_eq ? (typ_of_type (typeof e)) ? e'
     502      typ_should_eq ? (typ_of_type ty) ? e'
    477503  ]
    478 ] and translate_addr (vars:var_types) (e:expr) on e : res (CMexpr (ASTptr Any)) ≝
     504] and translate_addr (vars:var_types) (e:expr) on e : res (Σr.CMexpr (ASTptr r)) ≝
    479505match e with
    480506[ Expr ed _ ⇒
     
    482508  [ Evar id ⇒
    483509      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    484       match c with
    485       [ Global ⇒ OK ? (Cst ? (Oaddrsymbol id zero))
    486       | Stack n ⇒ OK ? (Cst ? (Oaddrstack (repr n)))
     510      match c return λ_. res (Σr.CMexpr (ASTptr r)) with
     511      [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id zero)))
     512      | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack (repr n))))
    487513      | Local ⇒ Error ? (msg BadlyTypedAccess) (* TODO: could rule out? *)
    488514      ]
    489515  | Ederef e1 ⇒
    490516      do e1' ← translate_expr vars e1;
    491       match typ_of_type (typeof e1) return λx. CMexpr x → res (CMexpr (ASTptr Any)) with
    492       [ ASTptr r ⇒ match r return λx. CMexpr (ASTptr x) → res (CMexpr (ASTptr Any)) with [ Any ⇒ λe1'.OK ? e1' | _ ⇒ λ_.Error ? (msg BadlyTypedAccess) ]
     517      match typ_of_type (typeof e1) return λx. CMexpr x → res (Σr. CMexpr (ASTptr r)) with
     518      [ ASTptr r ⇒ λe1'.OK ? (dp ?? r e1')
    493519      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
    494520      ] e1'
     
    498524          do e1' ← translate_addr vars e1;
    499525          do off ← field_offset id fl;
    500           OK ? (Op2 (ASTptr Any) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr Any) Oaddp e1' (Cst ? (Ointconst (repr off))))
     526          match e1' with
     527          [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst (repr off)))))
     528          ]
    501529      | Tunion _ _ ⇒ translate_addr vars e1
    502530      | _ ⇒ Error ? (msg BadlyTypedAccess)
     
    505533  ]
    506534].
     535>(access_mode_typ … E) @refl
     536qed.
    507537
    508538inductive destination : Type[0] ≝
    509539| IdDest : ident → destination
    510 | MemDest : memory_chunk → CMexpr (ASTptr Any) → destination.
     540| MemDest : ∀r:region. memory_chunk → CMexpr (ASTptr r) → destination.
    511541
    512542definition translate_dest ≝
     
    524554            match c with
    525555            [ Local ⇒ OK ? (IdDest id)
    526             | Global ⇒ OK ? (MemDest q (Cst ? (Oaddrsymbol id zero)))
    527             | Stack n ⇒ OK ? (MemDest q (Cst ? (Oaddrstack (repr n))))
     556            | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id zero)))
     557            | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack (repr n))))
    528558            ]
    529559        | _ ⇒
    530560            do e1' ← translate_addr vars e1;
    531             OK ? (MemDest q e1')
     561            match e1' with [ dp r e1' ⇒ OK ? (MemDest r q e1') ]
    532562        ]
    533563    ].
     
    563593match dest with
    564594[ IdDest id ⇒ OK ? (St_assign ? id e2')
    565 | MemDest q e1' ⇒ OK ? (St_store ? q e1' e2')
     595| MemDest r q e1' ⇒ OK ? (St_store ? r q e1' e2')
    566596].
    567597
     
    594624        match dest with
    595625        [ IdDest id ⇒ OK ? (St_call (Some ? id) ef' args')
    596         | MemDest q e1' ⇒
     626        | MemDest r q e1' ⇒
    597627            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
    598             OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store ? (typ_of_memory_chunk q) q e1' (Id ? tmp)))
     628            OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)))
    599629        ]
    600630    ]
     
    687717false;false;false;true]].
    688718
    689 definition translate_function : list ident → function → res internal_function ≝
     719definition translate_function : list (ident×region) → function → res internal_function ≝
    690720λglobals, f.
    691721  let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
     
    703733    s).
    704734
    705 definition translate_fundef : list ident → clight_fundef → res (fundef internal_function) ≝
     735definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
    706736λglobals,f.
    707737match f with
     
    712742definition clight_to_cminor : clight_program → res Cminor_program ≝
    713743λp.
    714   let globals ≝ (prog_funct_names ?? p)@(prog_var_names ?? p) in
     744  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
     745  let var_globals ≝ map … (λv. 〈\fst (\fst (\fst v)), \snd (\fst v)〉) (prog_vars ?? p) in
     746  let globals ≝ fun_globals @ var_globals in
    715747  transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p.
Note: See TracChangeset for help on using the changeset viewer.