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

Add new invariant to Cminor that return typs should be respected.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2250 r2251  
    10971097    stmt_P (λs1. stmt_labels (λl.ldefined s' l ∨ lpresent lbls l ∨ In ? l (labels_of_flag flag)) s1) s'.
    10981098
     1099definition return_ok : option typ → stmt → Prop ≝
     1100λot.
     1101stmt_P (λs.
     1102  match s with [ St_return oe ⇒
     1103    match oe with [ Some e ⇒ Some ? (dpi1 … e) = ot | None ⇒ None ? = ot ]
     1104  | _ ⇒ True ]).
     1105
    10991106(* trans_inv is the invariant which is enforced during the translation from Clight to Cminor.
    11001107  The involved arguments are the following:
     
    11061113  . su', a couple of a Cminor statement and fresh variable generator.
    11071114*)
    1108 definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → ((tmpgen vars) × labgen × stmt) → Prop ≝
    1109 λvars,lbls,s,uv,flag,su'.
     1115definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → option typ → ((tmpgen vars) × labgen × stmt) → Prop ≝
     1116λvars,lbls,s,uv,flag,rettyp,su'.
    11101117  let 〈uv', ul', s'〉 ≝ su' in
    11111118  stmt_inv (add_tmps vars (tmp_env … uv')) s' ∧   (* remaining variables in s' are local*)
    11121119  labels_translated lbls s s' ∧                   (* all the labels in s are transformed in label of s' using [lbls] as a map *)
    11131120  tmps_preserved vars uv uv' ∧                    (* the variables generated are local and grows in a monotonic fashion *)
     1121  return_ok rettyp s' ∧                           (* return statements have correct typ *)
    11141122  label_wf s s' lbls flag.                        (* labels are "properly" declared, as defined in [ŀabel_wf].*)
    1115                                  
    1116 let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (s:statement) on s
    1117   : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) ≝
    1118 match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) with
     1123
     1124axiom ReturnMismatch : String.
     1125
     1126let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s
     1127  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝
     1128match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) with
    11191129[ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?»
    11201130| Sassign e1 e2 ⇒
     
    11441154    ]
    11451155| Ssequence s1 s2 ⇒
    1146     do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
    1147     do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag s2;
     1156    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
     1157    do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag rettyp s2;
    11481158    OK ? «〈fgens2, St_seq s1' s2'〉, ?»
    11491159| Sifthenelse e1 s1 s2 ⇒
     
    11511161    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    11521162    [ ASTint _ _ ⇒ λe1'.
    1153          do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
    1154          do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag s2;
     1163         do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
     1164         do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag rettyp s2;
    11551165        OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?»
    11561166    | _ ⇒ λ_.Error ? (msg TypeMismatch)
     
    11631173        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
    11641174        let 〈entry, exit〉 as E2 ≝ labels in
    1165         do «fgens2, s1',H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) s1;
     1175        do «fgens2, s1',H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1;
    11661176        let converted_loop ≝
    11671177          St_label entry
     
    11791189        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
    11801190        let 〈entry, exit〉 as E2 ≝ labels in             
    1181         do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) s1;
     1191        do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1;
    11821192        let converted_loop ≝
    11831193          St_label entry
     
    11991209        let 〈labels, ul1〉 as E ≝ mklabels ul in
    12001210        let 〈entry, exit〉 as E2 ≝ labels in                           
    1201         do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls flag s1;
    1202         do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls (ConvertTo entry exit) s2;
    1203         do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo entry exit) s3;
     1211        do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls flag rettyp s1;
     1212        do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls (ConvertTo entry exit) rettyp s2;
     1213        do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo entry exit) rettyp s3;
    12041214        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    12051215        let converted_loop ≝
     
    12311241| Sreturn ret ⇒
    12321242    match ret with
    1233     [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?»
     1243    [ None ⇒
     1244        match rettyp return λx.res (Σy.trans_inv … x y) with
     1245        [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?»
     1246        | _ ⇒ Error ? (msg ReturnMismatch)
     1247        ]
    12341248    | Some e1 ⇒
    1235         do e1' ← translate_expr vars e1;
    1236         OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?»
     1249        match rettyp return λx.res (Σy.trans_inv … x y) with
     1250        [ Some rty ⇒
     1251            do e1' ← translate_expr vars e1;
     1252            do e1' ← typ_should_eq (typ_of_type (typeof e1)) rty ? e1';
     1253            OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?»
     1254        | _ ⇒ Error ? (msg ReturnMismatch)
     1255        ]
    12371256    ]
    12381257| Sswitch e1 ls ⇒ Error ? (msg FIXME)
    12391258| Slabel l s1 ⇒
    12401259    do l' as E ← lookup_label lbls l;
    1241     do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
     1260    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
    12421261    OK ? «〈fgens1, St_label l' s1'〉, ?»
    12431262| Sgoto l ⇒
     
    12451264    OK ? «〈uv, ul, St_goto l'〉, ?»
    12461265| Scost l s1 ⇒
    1247     do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
     1266    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
    12481267    OK ? «〈fgens1, St_cost l s1'〉, ?»
    12491268].
    1250 try @conj try @conj try @conj try @conj try @conj try @conj try @conj
     1269try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
    12511270try (@I)
    12521271try (#l #H elim H)
     
    12541273try (#H1 try #H2 assumption)
    12551274[ 1,5: @(tmp_preserved … p) ]
    1256 [ 1,3: elim e2' | 2,9: elim e1' | 4,7,14: elim ef' ]
    1257 [ 1,2,3,4,5,6,7 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
     1275[ 1,3: elim e2' | 2,9,24: elim e1' | 4,7,14: elim ef' ]
     1276[ 1,2,3,4,5,6,7,8 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
    12581277[ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
    12591278             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
     
    12721291[ 1: #size #sign | 2: | 3: #fsize ]
    12731292[ 1,2,3: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
     1293try @refl (* Does (at least) the return_ok cases *)
    12741294try @(match fgens1 return λx.x=fgens1 → ? with
    12751295     [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
     
    12811301     [ mk_Prod uv4 ul4 ⇒ λHfgens4.? ] (refl ? fgens4))
    12821302whd in H1 H2 H3 ⊢ ?; destruct whd nodelta in H1 H2 H3;
    1283 try (elim H1 -H1 * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1)
    1284 try (elim H2 -H2 * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2)
    1285 try (elim H3 -H3 * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3)
    1286 [ 1,2: #Hind1 #Hind2 | 3,4,9,11: #Hind | 5: #Hind1 #Hind2 #Hind3 ]
    1287 try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
     1303try (elim H1 -H1 * * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1 #Hret1)
     1304try (elim H2 -H2 * * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2 #Hret2)
     1305try (elim H3 -H3 * * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3 #Hret3)
     1306[ 1,2: #Hind1 #Hind2 | 3,4,8,10: #Hind | 5: #Hind1 #Hind2 #Hind3 ]
     1307try @conj try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
    12881308[ 1,7: @(stmt_P_mp … Hstmt_inv1) #e #Hvars @(stmt_vars_mp … Hvars) #i #t #Hlocal @(Htmps_pres2 … Hlocal)
    12891309| 2: #l #H cases (Exists_append ???? H) #Hcase
     
    13181338                | 2,5: #H %1 %2 assumption
    13191339                | 3,6: #H %2 assumption ] ]
    1320 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
    1321 [ 1,9,19,32: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
    1322 | 2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
    1323 | 3,10: whd #l #H normalize in H;
     1340try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
     1341[ 1,7,17: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1342| (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
     1343|*) 2,8: whd #l #H normalize in H;
    13241344         elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
    13251345         @conj
     
    13271347         | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l
    13281348              @(proj2 … Hlabel) ]
    1329 | 30: whd %2 %2 whd /2/
    1330 | 31: whd %2 whd /2/
    1331 | 4,16: whd %1 %1 normalize /2/
    1332 | 5,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1349| 27: whd %2 %2 whd /2/
     1350| 28: whd %2 whd /2/
     1351| 3,14: whd %1 %1 normalize /2/
     1352| 4,10: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    13331353   #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H
    13341354              | 2,6: #H %1 %2 assumption
     
    13381358                                               | 2,4: * ]
    13391359              ]
    1340 | 6: normalize %1 %1 %1 //                                                                                   
    1341 | 7,14: normalize %1 %1 %2 @Exists_append_r normalize /2/
    1342 | 11,13: whd %1 %1 normalize /2/
    1343 | 15: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
     1360| 5: normalize %1 %1 %1 //                                                                                   
     1361| 6,12: normalize %1 %1 %2 @Exists_append_r normalize /2/
     1362| 9,11: whd %1 %1 normalize /2/
     1363| 13: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
    13441364                   | 2: #H elim (Hlabels_tr1 label H)
    13451365                         #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
    13461366                         [ 1: // | 2: whd %2 assumption ]
    13471367                   ]
    1348 | 17: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1368| 15: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    13491369   #l * try * [ 1: #H %1 %1 normalize %2 @H
    13501370              | 2: #H %1 %2 assumption
    13511371              | 3: #H %2 assumption ]
    1352 | 18: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1372| 16: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    13531373   #H @(Htmps_pres3 … (Htmps_pres2 … H))
    1354 | 20: @(stmt_P_mp … Hstmt_inv3) //
    1355 | 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1374| 18: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    13561375   #H @(Htmps_pres3 … H)
    1357 | 22: whd #l #H normalize in H;
     1376| 19: whd #l #H normalize in H;
    13581377      cases (Exists_append … H) #Hcase
    13591378      [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
     
    13761395        ]
    13771396      ]
    1378 | 23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
    1379 | 24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1397| 20: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
     1398| 21: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    13801399   #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
    13811400              | 2: #H %1 %2 assumption
    13821401              | 3: #H %2 assumption ]
    1383 | 25: whd %1 %1 normalize /2/
    1384 | 26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1402| 22: whd %1 %1 normalize /2/
     1403| 23: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    13851404   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
    13861405                   @Exists_append_r @Exists_append_l @Exists_append_l
     
    13951414                     | 2: * ]
    13961415              ]
    1397 | 27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1416| 24: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    13981417   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
    13991418                   @Exists_append_r @Exists_append_l @Exists_append_l                   
     
    14071426                     | 2: * ]
    14081427              ]
    1409 | 28: whd %1 %1 normalize /2/
    1410 | 29: whd %1 %1 normalize
     1428| 25: whd %1 %1 normalize /2/
     1429| 26: whd %1 %1 normalize
    14111430      @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r
    14121431      whd %1 //
    1413 | 33: whd %1 %2 whd @(ex_intro … l) @E
     1432| 29: whd %1 %2 whd @(ex_intro … l) @E
    14141433] qed.
    14151434
     
    14181437(* params and statement aren't real parameters, they're just there for giving the invariant. *)
    14191438definition alloc_params :
    1420  ∀vars:var_types.∀lbls,statement,uv,flag. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag su)
    1421    → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag su) ≝   
    1422 λvars,lbls,statement,uv,ul,params,s. foldl ?? (λsu,it.
     1439 ∀vars:var_types.∀lbls,statement,uv,flag,rettyp. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag rettyp su)
     1440   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag rettyp su) ≝   
     1441λvars,lbls,statement,uv,ul,rettyp,params,s. foldl ?? (λsu,it.
    14231442  let 〈id,ty〉 ≝ it in
    14241443  do «result,Is» ← su;
    14251444  let 〈fgens1, s〉 as Eresult ≝ result in
    14261445  do 〈t,ty'〉 as E ← lookup' vars id;
    1427   match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul su) with
     1446  match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul rettyp su) with
    14281447  [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is»
    14291448  | Stack n ⇒ λE.
     
    14351454  [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
    14361455whd in Is ⊢ %; destruct whd in Is;
    1437 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
    1438 elim Is * * #Hincl #Hstmt_inv #Hlab_tr #Htmp_pr try assumption
     1456try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
     1457elim Is * * * #Hincl #Hstmt_inv #Hlab_tr #Hret #Htmp_pr try assumption
    14391458@(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl
    14401459qed.
     
    15511570      let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
    15521571      let uv ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in
    1553       do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (fn_body f);
    1554       do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (fn_params f) s0;
     1572      do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (opttyp_of_type (fn_return f)) (fn_body f);
     1573      do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (opttyp_of_type (fn_return f)) (fn_params f) s0;
    15551574      let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in
    15561575      let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? (fst ?? fgens) @ fn_vars f) in
     
    15701589     [ mk_Prod uv' ul' ⇒ λHfgens.? ] (refl ? fgens))
    15711590     whd in Is; <Hfgens in Is; #Is whd in Is ⊢ %;
    1572      elim Is * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hlabel_wf
     1591     elim Is * * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hreturn #Hlabel_wf
    15731592     (* merge Hlabel_wf with Hstmt_inv and eliminate right away *)
    1574      @(stmt_P_mp … (stmt_P_conj … Hstmt_inv Hlabel_wf))
    1575      #s * #Hstmt_vars #Hstmt_labels %
     1593     @(stmt_P_mp … (stmt_P_conj … (stmt_P_conj … Hstmt_inv Hlabel_wf) Hreturn))
     1594     #s * * #Hstmt_vars #Hstmt_labels #Hstmt_return %
    15761595     [ 1: (* prove that variables are either parameters or locals *)
    15771596        @(stmt_vars_mp … Hstmt_vars) #i #t #H
     
    15961615                #H @H
    15971616          ]
     1617     | cases s in Hstmt_return; // * normalize [2: * #t #e ]
     1618       cases (fn_return f) normalize #A try #B try #C try #D try #E destruct //
    15981619    ]
    15991620] qed.   
Note: See TracChangeset for help on using the changeset viewer.