Changeset 2251


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.

Location:
src
Files:
5 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.   
  • src/Cminor/initialisation.ma

    r2249 r2251  
    1919].
    2020
    21 (* None of the additional code introduces locals or labels. *)
     21(* None of the additional code introduces locals, labels or returns. *)
    2222definition stmt_inv : stmt → Prop ≝
    23   stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s).
     23  stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s ∧ match s with [ St_return _ ⇒ False | _ ⇒ True ]).
    2424 
    2525discriminator option.
     
    3838    ]
    3939].
    40 % //
     40% /2/
    4141cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p;
    42 destruct;/2/
     42destruct;/3/
    4343qed.
    4444
     
    5050     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
    5151  〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init).
    52 [ % //
     52[ % /2/
    5353| elim init
    54   [ % //
    55   | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % // | @(pi2 … (init_datum …)) ] | @IH ]
     54  [ % /2/
     55  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%);
     56    % [ % [ % /2/ | @(pi2 … (init_datum …)) ] | @IH ]
    5657] qed.
    5758
    5859definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
    5960λvars. foldr ? (Σs:stmt. stmt_inv s)
    60   (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
    61 % [ % [ % // | @(pi2 … s) ] | @(pi2 … (init_var …)) ]
     61  (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? (conj ?? I I) I)) vars.
     62% [ % [ % /2/ | @(pi2 … s) ] | @(pi2 … (init_var …)) ]
    6263qed.
    6364
    6465lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
    6566#s elim s //
    66 [ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
     67[ #s1 #s2 #IH1 #IH2 * * * * #_ #_ #_ #H1 #H2 whd in ⊢ (??%?);
    6768  >(IH1 H1) >(IH2 H2) @refl
    6869| #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
    6970  >(IH1 H1) >(IH2 H2) @refl
    70 | #l #s #IH * * #_ *
     71| #l #s #IH * * * #_ *
    7172| #l #s #IH * * #_ #_ #H @(IH H)
    7273] qed.
     
    9596%
    9697[ % [ % // |
    97   @(stmt_P_mp … H) #s * #V #L %
     98  @(stmt_P_mp … H) #s * * #V #L #R %
    9899  [ @(stmt_vars_mp … V) #i #t *
    99100  | @(stmt_labels_mp … L) #l *
     101  | cases s in R ⊢ %; // #x *
    100102  ]
    101103  ]
  • src/Cminor/semantics.ma

    r2232 r2251  
    395395| 7,8:
    396396  @(stmt_P_mp … (f_inv f))
    397   #s * #V #L %
     397  #s * #V #L #R %
    398398  [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX)
    399399    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en))
  • src/Cminor/syntax.ma

    r2249 r2251  
    128128].
    129129
    130 record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (s:stmt) : Prop ≝ {
     130inductive rettyp_match : option typ → option (𝚺t.expr t) → Prop ≝
     131| rettyp_none : rettyp_match (None ?) (None ?)
     132| rettyp_some : ∀t,e. rettyp_match (Some ? t) (Some ? ❬t,e❭).
     133
     134record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (rettyp:option typ) (s:stmt) : Prop ≝ {
    131135  cm_inv_var : stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) env) s;
    132   cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s
     136  cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s;
     137  cm_inv_return : match s with [ St_return oe ⇒ rettyp_match rettyp oe
     138                               | _ ⇒ True ]
    133139}.
    134140
     
    142148     (* Ensure that variables appear in the params and vars list with the
    143149        correct typ; and that all goto labels used are declared. *)
    144 ; f_inv       : stmt_P (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body)) f_body
     150; f_inv       : stmt_P (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body) f_return) f_body
    145151}.
    146152
  • src/Cminor/toRTLabs.ma

    r2232 r2251  
    837837  ).
    838838[ -emptyfn @(stmt_P_mp … (f_inv f))
    839   #s * #V #L %
     839  #s * #V #L #R %
    840840  [ @(stmt_vars_mp … V)
    841841    #i #t #H cases (Exists_append … H)
Note: See TracChangeset for help on using the changeset viewer.