Ignore:
Timestamp:
Dec 19, 2011, 2:48:33 PM (8 years ago)
Author:
campbell
Message:

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1612 r1626  
    8282.
    8383
    84 definition var_types ≝ identifier_map SymbolTag var_type.
     84definition var_types ≝ identifier_map SymbolTag (var_type × type).
    8585
    8686axiom UndeclaredIdentifier : String.
     
    8989λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
    9090
    91 definition local_id : var_types → ident → Prop ≝
    92 λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False | _ ⇒ True ] | _ ⇒ False ].
     91(* Assert that an identifier is a local variable with the given typ. *)
     92definition local_id : var_types → ident → typ → Prop ≝
     93λvars,id,t. match lookup' vars id with [ OK vt ⇒ match (\fst vt) with [ Global _ ⇒ False | _ ⇒ t = typ_of_type (\snd vt) ] | _ ⇒ False ].
    9394
    9495(* Note that the semantics allows locals to shadow globals.
     
    105106].
    106107
    107 definition characterise_vars : list (ident×region) → function → var_types × nat ≝
     108definition characterise_vars : list (ident×region×type) → function → var_types × nat ≝
    108109λglobals, f.
    109   let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
     110  let m ≝ foldr ?? (λidrt,m. add ?? m (\fst (\fst idrt)) 〈Global (\snd (\fst idrt)), \snd idrt〉) (empty_map ??) globals in
    110111  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
    111112  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
     
    115116                           then 〈Stack stack_high,stack_high + sizeof ty〉
    116117                           else 〈Local, stack_high〉 in
    117       〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
     118      〈add ?? m id 〈c, ty〉, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
    118119  〈m,stacksize〉.
    119120
    120 lemma local_id_add_global : ∀vars,id,r,id'.
    121   local_id (add ?? vars id (Global r)) id' → local_id vars id'.
    122 #var #id #r #id'
     121lemma local_id_add_global : ∀vars,id,r,t,id',t'.
     122  local_id (add ?? vars id 〈Global r, t〉) id' t' → local_id vars id' t'.
     123#var #id #r #t #id' #t'
    123124whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?);
    124125cases (identifier_eq ? id id')
     
    127128] qed.
    128129
    129 lemma local_id_add_miss : ∀vars,id,t,id'.
    130   id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
    131 #vars #id #t #id' #NE
     130lemma local_id_add_miss : ∀vars,id,vt,id',t'.
     131  id ≠ id' → local_id (add ?? vars id vt) id' t' → local_id vars id' t'.
     132#vars #id #vt #id' #t' #NE
    132133whd in ⊢ (% → %);
    133134whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]);
     
    138139lemma characterise_vars_all : ∀l,f,vars,n.
    139140  characterise_vars l f = 〈vars,n〉 →
    140   ∀i. local_id vars i
    141       Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
     141  ∀i,t. local_id vars i t
     142        Exists ? (λx.\fst x = i ∧ typ_of_type (\snd x) = t) (fn_params f @ fn_vars f).
    142143#globals #f
    143144whd in ⊢ (∀_.∀_.??%? → ?);
    144145elim (fn_params f @ fn_vars f)
    145 [ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H @False_ind
     146[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #t #H @False_ind
    146147  elim globals in H;
    147148  [ normalize //
    148   | * #id #rg #t #IH whd in ⊢ (?%? → ?); #H @IH @(local_id_add_global ???? H)
     149  | * * #id #rg #t #tl #IH whd in ⊢ (?%?? → ?); #H @IH @(local_id_add_global … H)
    149150  ]
    150 | * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i
     151| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i #t
     152
     153  #H >(contract_pair var_types nat ?) in E;
     154  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     155  cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     156  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
     157
    151158  cases (identifier_eq ? id i)
    152   [ #E' <E' #H % @refl
    153   | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
    154     whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    155     cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    156     #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
    157     @(IH m0 n0)
     159  [ 1,3: #E' >E' in EQ2:%; #EQ2 % %
     160    [ 1,3: @refl
     161    | *: destruct (EQ2) change with (add ?????) in H:(?%??);
     162      whd in H; whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]); >lookup_add_hit in H;
     163      whd in ⊢ (% → ?); #E'' >E'' @refl
     164    ]
     165  | *: #NE %2 @(IH m0 n0)
    158166    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ
    159167    | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE
     
    446454  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
    447455  | Evar id ⇒
    448       do c as E ← lookup' vars id;
     456      do 〈c,t〉 as E ← lookup' vars id;
    449457      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
    450458      [ Global r ⇒ λ_.
     
    460468          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    461469          ]
    462       | Local ⇒ λE. OK ? «Id ? id, ?»
     470      | Local ⇒ λE. type_should_eq t ty (λt.Σe':CMexpr (typ_of_type t).expr_vars (typ_of_type t) e' (local_id vars))  («Id (typ_of_type t) id, ?»)
    463471      ] E
    464472  | Ederef e1 ⇒
     
    572580  match ed with
    573581  [ Evar id ⇒
    574       do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
     582      do 〈c,t〉 ← lookup' vars id;
    575583      match c return λ_. res (𝚺r.Σz:CMexpr (ASTptr r).?) with
    576584      [ Global r ⇒ OK ? ❬r, «Cst ? (Oaddrsymbol id 0), ?»❭
     
    599607].
    600608whd try @I
    601 [ >E @I
     609[ >E whd @refl
    602610| >(E ? (refl ??)) @refl
    603611| 3,4: @pi2
     
    615623
    616624inductive destination (vars:var_types) : Type[0] ≝
    617 | IdDest : ∀id:ident. local_id vars id → destination vars
     625| IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars
    618626| MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
    619627
     
    629637        match ed1 with
    630638        [ Evar id ⇒
    631             do c as E ← lookup' vars id;
     639            do 〈c,t〉 as E ← lookup' vars id;
    632640            match c return λx.? → ? with
    633             [ Local ⇒ λE. OK ? (IdDest vars id ?)
     641            [ Local ⇒ λE. OK ? (IdDest vars id t ?)
    634642            | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0)))
    635643            | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n)))
     
    640648        ]
    641649    ].
    642 whd // >E @I
     650whd // >E @refl
    643651qed.
    644652
     
    686694do dest ← translate_dest vars e1 (typeof e2);
    687695match dest with
    688 [ IdDest id p ⇒ OK ? «St_assign ? id e2', ?»
     696[ IdDest id ty p ⇒
     697    do e2' ← type_should_eq (typeof e2) ty ? e2';
     698    OK ? «St_assign ? id e2', ?»
    689699| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
    690700].
     
    712722record tmpgen : Type[0] ≝ {
    713723  tmp_universe : universe SymbolTag;
    714   tmp_env : list (ident × typ)
     724  tmp_env : list (ident × type)
    715725}.
    716726
    717 definition alloc_tmp : memory_chunk → tmpgen → ident × tmpgen ≝
    718 λc,g.
     727definition alloc_tmp : type → tmpgen → ident × tmpgen ≝
     728λty,g.
    719729  let 〈tmp,u〉 ≝ fresh ? (tmp_universe g) in
    720   〈tmp, mk_tmpgen u (〈tmp, typ_of_memory_chunk c〉::(tmp_env g))〉.
     730  〈tmp, mk_tmpgen u (〈tmp, ty〉::(tmp_env g))〉.
    721731
    722732lemma lookup_label_hit : ∀lbls,l,l'.
     
    728738definition add_tmps : var_types → tmpgen → var_types ≝
    729739λvs,g.
    730   foldr ?? (λidty,vs. add ?? vs (\fst idty) Local) vs (tmp_env g).
     740  foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs (tmp_env g).
    731741
    732742definition tmps_preserved : var_types → tmpgen → tmpgen → Prop ≝
    733743λvars,u1,u2.
    734   ∀id. local_id (add_tmps vars u1) id → local_id (add_tmps vars u2) id.
     744  ∀id,ty. local_id (add_tmps vars u1) id ty → local_id (add_tmps vars u2) id ty.
    735745
    736746lemma alloc_tmp_preserves : ∀tmp,u,u',vars,q.
    737747  〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
     748cases daemon (* XXX freshness
    738749#tmp #g #g' #vars #q
    739750whd in ⊢ (???% → ?); #E
     
    744755[ >E >lookup_add_hit @I
    745756| cases E #NE >lookup_add_miss [ @H | /2/
    746 ] qed.
     757] *) qed.
    747758
    748759definition trans_inv : var_types → lenv → statement → tmpgen → (stmt×tmpgen) → Prop ≝
     
    763774qed.
    764775
    765 lemma local_id_add_local_oblivious : ∀vars,id,id'.
    766   local_id vars id → local_id (add ?? vars id' Local) id.
    767 #vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
     776(* XXX Not true without fresh id' XXX
     777lemma local_id_add_local_oblivious : ∀vars,id,ty,id',ty'.
     778  local_id vars id ty → local_id (add ?? vars id' 〈Local, ty'〉) id ty.
     779#vars #id #ty #id' #ty' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
    768780cases (identifier_eq ? id id')
    769781[ #E >E >lookup_add_hit @I
    770782| #NE >lookup_add_miss [ @H | /2/
    771783] qed.
    772 
    773 lemma local_id_add_tmps_oblivious : ∀vars,id,u.
    774   local_id vars id → local_id (add_tmps vars u) id.
     784*)
     785
     786(* XXX freshness XXX *)
     787axiom local_id_add_tmps_oblivious : ∀vars,id,ty,u.
     788  local_id vars id ty → local_id (add_tmps vars u) id ty.
     789(*
    775790#vars #id * #u #l #H elim l
    776791[ //
    777792| * #id' #ty #tl @local_id_add_local_oblivious
    778793] qed.
     794*)
    779795
    780796lemma add_tmps_oblivious : ∀vars,lbls,s,u.
     
    784800#s' * #H1 #H2 %
    785801[ @(stmt_vars_mp … H1)
    786   #id @local_id_add_tmps_oblivious
     802  #id #t @local_id_add_tmps_oblivious
    787803| @H2
    788804] qed.
    789805
    790 lemma local_id_fresh_tmp : ∀tmp,u,q,u0,vars.
    791   〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
    792 #tmp #u #q #u0 #vars
     806lemma local_id_fresh_tmp : ∀tmp,u,ty,u0,vars.
     807  〈tmp,u〉 = alloc_tmp ty u0 → local_id (add_tmps vars u) tmp (typ_of_type ty).
     808#tmp #u #ty #u0 #vars
    793809whd in ⊢ (???% → ?); #E
    794810destruct
    795 whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
    796 @I
     811whd in ⊢ (?%??); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
     812@refl
    797813qed.
    798814
     
    812828        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
    813829        match dest with
    814         [ IdDest id p ⇒ OK ? «〈St_call (Some ? id) ef' args', u〉, ?»
     830        [ IdDest id ty p ⇒ OK ? «〈St_call (Some ? 〈id,typ_of_type ty〉) ef' args', u〉, ?»
    815831        | MemDest r q e1' ⇒
    816             let 〈tmp, u〉 as Etmp ≝ alloc_tmp q u in
    817             OK ? «〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉, ?»
     832            let 〈tmp, u〉 as Etmp ≝ alloc_tmp (typeof e1) u in
     833            OK ? «〈St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r q e1' (Id ? tmp)), u〉, ?»
    818834        ]
    819835    ]
     
    891907try @I
    892908try (#l #H @(match H in False with [ ]))
    893 try (#id #H @H)
     909try (#id #ty #H @H)
    894910[ @add_tmps_oblivious @(pi2 ?? s')
    895911| @local_id_add_tmps_oblivious @p
    896912]
    897 try (@sub_pi2 #x @expr_vars_mp #i @local_id_add_tmps_oblivious)
    898 [ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i @local_id_add_tmps_oblivious
     913try (@sub_pi2 #x @expr_vars_mp #i #ty @local_id_add_tmps_oblivious)
     914[ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i #ty' @local_id_add_tmps_oblivious
    899915| 2,4: @(local_id_fresh_tmp … Etmp)
    900916| @(alloc_tmp_preserves … Etmp)
     
    907923    %{l'} % [ 1,3: @E2 | *: @Exists_append_r @D2 ]
    908924  ]
    909 | 10,14: cases H2 #_ #TP2 #id #L @TP2 cases H1 #_ #TP1 @TP1 @L
     925| 10,14: cases H2 #_ #TP2 #id #ty #L @TP2 cases H1 #_ #TP1 @TP1 @L
    910926| 15,18: @(π1 (π1 H1))
    911927| 16,19: cases H1 * #_ #L1 #_ #l #H cases (L1 l H) #l' * #E1 #D1
     
    913929| 17,20: @(π2 H1)
    914930(* Sfor *)
    915 | @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @(π2 H2) @H | @H5 ]
     931| @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #ty #H @(π2 H3) @(π2 H2) @H | @H5 ]
    916932| @(π1 (π1 H3))
    917 | @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @H | @H5 ]
     933| @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #ty #H @(π2 H3) @H | @H5 ]
    918934| #l #H cases (Exists_append … H)
    919935  [ #EX1 cases H1 * #S1 #L1 #_ cases (L1 l EX1) #l' * #E1 #D1
     
    926942    ]
    927943  ]
    928 | #id #H @(π2 H3) @(π2 H2) @(π2 H1) @H
     944| #id #ty #H @(π2 H3) @(π2 H2) @(π2 H1) @H
    929945(* Slabel *)
    930946| %{l} @E
     
    948964  let 〈id,ty〉 ≝ it in
    949965   do «s,u, Is» ← su;
    950   do t as E ← lookup' vars id;
     966  do 〈t,ty'〉 as E ← lookup' vars id;
    951967  match t return λx.? → ? with
    952968  [ Local ⇒ λE. OK (Σs:stmt×tmpgen.?) «〈s,u〉,Is»
     
    957973      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    958974      ];
    959       OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, u〉, ?»
     975      OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s, u〉, ?»
    960976  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
    961977  ] E) (OK ? s) params.
    962978try @conj try @conj try @conj try @conj try @conj try @conj
    963979try @I
    964 [ @(expr_vars_mp … (λid. local_id_add_tmps_oblivious vars id u)) whd >E @I
     980[ @(expr_vars_mp … (λid,ty. local_id_add_tmps_oblivious vars id ty u)) whd >E @refl
    965981| @(π1 (π1 Is))
    966982| @(π2 (π1 Is))
     
    10301046qed.
    10311047
    1032 lemma local_id_split : ∀vars,tmpgen,i.
    1033   local_id (add_tmps vars tmpgen) i
    1034   local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen).
    1035 #vars #tmpgen #i
    1036 whd in ⊢ (?%? → ?);
     1048lemma local_id_split : ∀vars,tmpgen,i,t.
     1049  local_id (add_tmps vars tmpgen) i t
     1050  local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env tmpgen).
     1051#vars #tmpgen #i #t
     1052whd in ⊢ (?%?? → ?);
    10371053elim (tmp_env tmpgen)
    10381054[ #H %1 @H
    10391055| * #id #ty #tl #IH
    10401056  cases (identifier_eq ? i id)
    1041   [ #E >E #H %2 whd %1 @refl
     1057  [ #E >E #H %2 whd %1 % [ @refl | whd in H; whd in H:(match % with [_⇒?|_⇒?]); >lookup_add_hit in H; #E1 >E1 @refl ]
    10421058  | #NE #H cases (IH ?)
    10431059    [ #H' %1 @H'
     
    10571073] qed.
    10581074
    1059 definition translate_function : universe SymbolTag → list (ident×region) → function → res internal_function ≝
     1075definition translate_function : universe SymbolTag → list (ident×region×type) → function → res internal_function ≝
    10601076λtmpuniverse, globals, f.
    10611077  do «lbls, Ilbls» ← build_label_env (fn_body f);
     
    10671083    (opttyp_of_type (fn_return f))
    10681084    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
    1069     ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
     1085    ((map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env tmp @ fn_vars f)))
    10701086    stacksize
    10711087    s ?).
     
    10741090#s1 * #H1 #H2 %
    10751091[ @(stmt_vars_mp … H1)
    1076   #i #H
     1092  #i #t #H
    10771093  cases (local_id_split … H)
    1078   [ #H' @Exists_squeeze >map_append
    1079     @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) @H'
     1094  [ #H' >map_append
     1095    @Exists_map [ 2: @Exists_squeeze @(characterise_vars_all … (sym_eq ??? E) i t) @H'
    10801096                | skip
    1081                 | * #id #ty #E1 <E1 @refl
     1097                | * #id #ty * #E1 #E2 <E1 <E2 @refl
    10821098                ]
    1083   | #EX @Exists_append_r @Exists_append_l @EX
     1099  | #EX @Exists_append_r <map_append @Exists_append_l @Exists_map [2: @EX | skip | * #id #ty * #E1 #E2 <E1 <E2 % @refl ]
    10841100  ]
    10851101| @(stmt_labels_mp … H2)
     
    10901106] qed.
    10911107
    1092 definition translate_fundef : universe SymbolTag → list (ident×region) → clight_fundef → res (fundef internal_function) ≝
     1108definition translate_fundef : universe SymbolTag → list (ident×region×type) → clight_fundef → res (fundef internal_function) ≝
    10931109λtmpuniverse,globals,f.
    10941110match f with
     
    11051121λp.
    11061122  let tmpuniverse ≝ universe_for_program p in
    1107   let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
    1108   let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
     1123  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
     1124  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
    11091125  let globals ≝ fun_globals @ var_globals in
    11101126  transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).
Note: See TracChangeset for help on using the changeset viewer.