Changeset 2251 for src/Clight/toCminor.ma

Timestamp:

Jul 24, 2012, 7:40:21 PM (8 years ago)

Author:

campbell

Message:

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

File:

• src/Clight/toCminor.ma (modified) (23 diffs)

src/Clight/toCminor.ma

@@ -1097 +1097 @@
     stmt_P (λs1. stmt_labels (λl.ldefined s' l ∨ lpresent lbls l ∨ In ? l (labels_of_flag flag)) s1) s'.
 
+definition return_ok : option typ → stmt → Prop ≝
+λot.
+stmt_P (λs.
+  match s with [ St_return oe ⇒
+    match oe with [ Some e ⇒ Some ? (dpi1 … e) = ot | None ⇒ None ? = ot ]
+  | _ ⇒ True ]).
+
 (* trans_inv is the invariant which is enforced during the translation from Clight to Cminor.
   The involved arguments are the following:
@@ -1106 +1113 @@
   . su', a couple of a Cminor statement and fresh variable generator.
 *)
-definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → ((tmpgen vars) × labgen × stmt) → Prop ≝
-λvars,lbls,s,uv,flag,su'. 
+definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → option typ → ((tmpgen vars) × labgen × stmt) → Prop ≝
+λvars,lbls,s,uv,flag,rettyp,su'. 
   let 〈uv', ul', s'〉 ≝ su' in
   stmt_inv (add_tmps vars (tmp_env … uv')) s' ∧   (* remaining variables in s' are local*)
   labels_translated lbls s s' ∧                   (* all the labels in s are transformed in label of s' using [lbls] as a map *)
   tmps_preserved vars uv uv' ∧                    (* the variables generated are local and grows in a monotonic fashion *)
+  return_ok rettyp s' ∧                           (* return statements have correct typ *)
   label_wf s s' lbls flag.                        (* labels are "properly" declared, as defined in [ŀabel_wf].*) 
-                                 
-let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (s:statement) on s 
-  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) ≝
-match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) with
+
+axiom ReturnMismatch : String.
+
+let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s 
+  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝
+match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) with
 [ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?»
 | Sassign e1 e2 ⇒
@@ -1144 +1154 @@
     ]
 | Ssequence s1 s2 ⇒
-    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
-    do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag s2;
+    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
+    do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag rettyp s2;
     OK ? «〈fgens2, St_seq s1' s2'〉, ?»
 | Sifthenelse e1 s1 s2 ⇒
@@ -1151 +1161 @@
     match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
     [ ASTint _ _ ⇒ λe1'.
-         do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
-         do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag s2;
+         do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
+         do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag rettyp s2;
         OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?»
     | _ ⇒ λ_.Error ? (msg TypeMismatch)
@@ -1163 +1173 @@
         let 〈labels, ul1〉 as E1 ≝ mklabels ul in
         let 〈entry, exit〉 as E2 ≝ labels in
-        do «fgens2, s1',H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) s1;
+        do «fgens2, s1',H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1;
         let converted_loop ≝
           St_label entry
@@ -1179 +1189 @@
         let 〈labels, ul1〉 as E1 ≝ mklabels ul in
         let 〈entry, exit〉 as E2 ≝ labels in              
-        do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) s1;
+        do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1;
         let converted_loop ≝
           St_label entry
@@ -1199 +1209 @@
         let 〈labels, ul1〉 as E ≝ mklabels ul in
         let 〈entry, exit〉 as E2 ≝ labels in                            
-        do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls flag s1;
-        do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls (ConvertTo entry exit) s2;
-        do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo entry exit) s3;
+        do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls flag rettyp s1;
+        do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls (ConvertTo entry exit) rettyp s2;
+        do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo entry exit) rettyp s3;
         (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
         let converted_loop ≝
@@ -1231 +1241 @@
 | Sreturn ret ⇒
     match ret with
-    [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?»
+    [ None ⇒ 
+        match rettyp return λx.res (Σy.trans_inv … x y) with
+        [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?»
+        | _ ⇒ Error ? (msg ReturnMismatch)
+        ]
     | Some e1 ⇒
-        do e1' ← translate_expr vars e1;
-        OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?»
+        match rettyp return λx.res (Σy.trans_inv … x y) with
+        [ Some rty ⇒
+            do e1' ← translate_expr vars e1;
+            do e1' ← typ_should_eq (typ_of_type (typeof e1)) rty ? e1';
+            OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?»
+        | _ ⇒ Error ? (msg ReturnMismatch)
+        ]
     ]
 | Sswitch e1 ls ⇒ Error ? (msg FIXME)
 | Slabel l s1 ⇒
     do l' as E ← lookup_label lbls l;
-    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
+    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
     OK ? «〈fgens1, St_label l' s1'〉, ?»
 | Sgoto l ⇒
@@ -1245 +1264 @@
     OK ? «〈uv, ul, St_goto l'〉, ?»
 | Scost l s1 ⇒
-    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
+    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
     OK ? «〈fgens1, St_cost l s1'〉, ?»
 ].
-try @conj try @conj try @conj try @conj try @conj try @conj try @conj
+try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
 try (@I)
 try (#l #H elim H)
@@ -1254 +1273 @@
 try (#H1 try #H2 assumption)
 [ 1,5: @(tmp_preserved … p) ]
-[ 1,3: elim e2' | 2,9: elim e1' | 4,7,14: elim ef' ]
-[ 1,2,3,4,5,6,7 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
+[ 1,3: elim e2' | 2,9,24: elim e1' | 4,7,14: elim ef' ]
+[ 1,2,3,4,5,6,7,8 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
 [ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
              | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
@@ -1272 +1291 @@
 [ 1: #size #sign | 2: | 3: #fsize ]
 [ 1,2,3: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
+try @refl (* Does (at least) the return_ok cases *)
 try @(match fgens1 return λx.x=fgens1 → ? with
      [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
@@ -1281 +1301 @@
      [ mk_Prod uv4 ul4 ⇒ λHfgens4.? ] (refl ? fgens4))
 whd in H1 H2 H3 ⊢ ?; destruct whd nodelta in H1 H2 H3;
-try (elim H1 -H1 * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1)
-try (elim H2 -H2 * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2)
-try (elim H3 -H3 * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3)
-[ 1,2: #Hind1 #Hind2 | 3,4,9,11: #Hind | 5: #Hind1 #Hind2 #Hind3 ]
-try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
+try (elim H1 -H1 * * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1 #Hret1)
+try (elim H2 -H2 * * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2 #Hret2)
+try (elim H3 -H3 * * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3 #Hret3)
+[ 1,2: #Hind1 #Hind2 | 3,4,8,10: #Hind | 5: #Hind1 #Hind2 #Hind3 ]
+try @conj try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
 [ 1,7: @(stmt_P_mp … Hstmt_inv1) #e #Hvars @(stmt_vars_mp … Hvars) #i #t #Hlocal @(Htmps_pres2 … Hlocal)
 | 2: #l #H cases (Exists_append ???? H) #Hcase
@@ -1318 +1338 @@
                 | 2,5: #H %1 %2 assumption
                 | 3,6: #H %2 assumption ] ]
-try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
-[ 1,9,19,32: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
-| 2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
-| 3,10: whd #l #H normalize in H;
+try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
+[ 1,7,17: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
+| (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
+|*) 2,8: whd #l #H normalize in H;
          elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
          @conj
@@ -1327 +1347 @@
          | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l
               @(proj2 … Hlabel) ]
-| 30: whd %2 %2 whd /2/
-| 31: whd %2 whd /2/
-| 4,16: whd %1 %1 normalize /2/
-| 5,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
+| 27: whd %2 %2 whd /2/
+| 28: whd %2 whd /2/
+| 3,14: whd %1 %1 normalize /2/
+| 4,10: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H
               | 2,6: #H %1 %2 assumption
@@ -1338 +1358 @@
                                                | 2,4: * ]
               ]
-| 6: normalize %1 %1 %1 //                                                                                   
-| 7,14: normalize %1 %1 %2 @Exists_append_r normalize /2/
-| 11,13: whd %1 %1 normalize /2/
-| 15: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
+| 5: normalize %1 %1 %1 //                                                                                   
+| 6,12: normalize %1 %1 %2 @Exists_append_r normalize /2/
+| 9,11: whd %1 %1 normalize /2/
+| 13: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
                    | 2: #H elim (Hlabels_tr1 label H)
                          #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
                          [ 1: // | 2: whd %2 assumption ]
                    ]
-| 17: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
+| 15: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    #l * try * [ 1: #H %1 %1 normalize %2 @H
               | 2: #H %1 %2 assumption
               | 3: #H %2 assumption ]
-| 18: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
+| 16: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    #H @(Htmps_pres3 … (Htmps_pres2 … H))
-| 20: @(stmt_P_mp … Hstmt_inv3) //
-| 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
+| 18: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    #H @(Htmps_pres3 … H)
-| 22: whd #l #H normalize in H;
+| 19: whd #l #H normalize in H;
       cases (Exists_append … H) #Hcase
       [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
@@ -1376 +1395 @@
         ]
       ]
-| 23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
-| 24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
+| 20: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
+| 21: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
               | 2: #H %1 %2 assumption
               | 3: #H %2 assumption ]
-| 25: whd %1 %1 normalize /2/
-| 26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
+| 22: whd %1 %1 normalize /2/
+| 23: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
                    @Exists_append_r @Exists_append_l @Exists_append_l 
@@ -1395 +1414 @@
                      | 2: * ]
               ]
-| 27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
+| 24: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
                    @Exists_append_r @Exists_append_l @Exists_append_l                    
@@ -1407 +1426 @@
                      | 2: * ]
               ]
-| 28: whd %1 %1 normalize /2/
-| 29: whd %1 %1 normalize
+| 25: whd %1 %1 normalize /2/
+| 26: whd %1 %1 normalize
       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r 
       whd %1 //
-| 33: whd %1 %2 whd @(ex_intro … l) @E
+| 29: whd %1 %2 whd @(ex_intro … l) @E
 ] qed.
 
@@ -1418 +1437 @@
 (* params and statement aren't real parameters, they're just there for giving the invariant. *)
 definition alloc_params :
- ∀vars:var_types.∀lbls,statement,uv,flag. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag su) 
-   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag su) ≝   
-λvars,lbls,statement,uv,ul,params,s. foldl ?? (λsu,it.
+ ∀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) 
+   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag rettyp su) ≝   
+λvars,lbls,statement,uv,ul,rettyp,params,s. foldl ?? (λsu,it.
   let 〈id,ty〉 ≝ it in
   do «result,Is» ← su;
   let 〈fgens1, s〉 as Eresult ≝ result in
   do 〈t,ty'〉 as E ← lookup' vars id;
-  match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul su) with
+  match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul rettyp su) with
   [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is»
   | Stack n ⇒ λE.
@@ -1435 +1454 @@
   [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
 whd in Is ⊢ %; destruct whd in Is;
-try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
-elim Is * * #Hincl #Hstmt_inv #Hlab_tr #Htmp_pr try assumption
+try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
+elim Is * * * #Hincl #Hstmt_inv #Hlab_tr #Hret #Htmp_pr try assumption
 @(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl
 qed.
@@ -1551 +1570 @@
       let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
       let uv ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in
-      do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (fn_body f);
-      do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (fn_params f) s0;
+      do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (opttyp_of_type (fn_return f)) (fn_body f);
+      do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (opttyp_of_type (fn_return f)) (fn_params f) s0;
       let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in
       let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? (fst ?? fgens) @ fn_vars f) in
@@ -1570 +1589 @@
      [ mk_Prod uv' ul' ⇒ λHfgens.? ] (refl ? fgens))
      whd in Is; <Hfgens in Is; #Is whd in Is ⊢ %;
-     elim Is * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hlabel_wf
+     elim Is * * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hreturn #Hlabel_wf
      (* merge Hlabel_wf with Hstmt_inv and eliminate right away *)
-     @(stmt_P_mp … (stmt_P_conj … Hstmt_inv Hlabel_wf))
-     #s * #Hstmt_vars #Hstmt_labels %
+     @(stmt_P_mp … (stmt_P_conj … (stmt_P_conj … Hstmt_inv Hlabel_wf) Hreturn))
+     #s * * #Hstmt_vars #Hstmt_labels #Hstmt_return %
      [ 1: (* prove that variables are either parameters or locals *)
         @(stmt_vars_mp … Hstmt_vars) #i #t #H
@@ -1596 +1615 @@
                 #H @H
           ]
+     | cases s in Hstmt_return; // * normalize [2: * #t #e ]
+       cases (fn_return f) normalize #A try #B try #C try #D try #E destruct //
     ]
 ] qed.