Changeset 2251 for src/Cminor

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/Cminor

Files:

• initialisation.ma (modified) (4 diffs)
• semantics.ma (modified) (1 diff)
• syntax.ma (modified) (2 diffs)
• toRTLabs.ma (modified) (1 diff)

src/Cminor/initialisation.ma

@@ -19 +19 @@
 ].
 
-(* None of the additional code introduces locals or labels. *)
+(* None of the additional code introduces locals, labels or returns. *)
 definition stmt_inv : stmt → Prop ≝
-  stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s).
+  stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s ∧ match s with [ St_return _ ⇒ False | _ ⇒ True ]).
   
 discriminator option.
@@ -38 +38 @@
     ]
 ].
-% //
+% /2/
 cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p;
-destruct;/2/
+destruct;/3/
 qed.
 
@@ -50 +50 @@
      〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
   〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init).
-[ % //
+[ % /2/
 | elim init
-  [ % //
-  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % // | @(pi2 … (init_datum …)) ] | @IH ]
+  [ % /2/
+  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%);
+    % [ % [ % /2/ | @(pi2 … (init_datum …)) ] | @IH ]
 ] qed. 
 
 definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
 λvars. foldr ? (Σs:stmt. stmt_inv s)
-  (λ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.
-% [ % [ % // | @(pi2 … s) ] | @(pi2 … (init_var …)) ]
+  (λ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.
+% [ % [ % /2/ | @(pi2 … s) ] | @(pi2 … (init_var …)) ]
 qed.
 
 lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
 #s elim s //
-[ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
+[ #s1 #s2 #IH1 #IH2 * * * * #_ #_ #_ #H1 #H2 whd in ⊢ (??%?);
   >(IH1 H1) >(IH2 H2) @refl 
 | #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
   >(IH1 H1) >(IH2 H2) @refl
-| #l #s #IH * * #_ *
+| #l #s #IH * * * #_ *
 | #l #s #IH * * #_ #_ #H @(IH H)
 ] qed.
@@ -95 +96 @@
 %
 [ % [ % // |
-  @(stmt_P_mp … H) #s * #V #L %
+  @(stmt_P_mp … H) #s * * #V #L #R %
   [ @(stmt_vars_mp … V) #i #t *
   | @(stmt_labels_mp … L) #l *
+  | cases s in R ⊢ %; // #x *
   ]
   ]

src/Cminor/semantics.ma

@@ -395 +395 @@
 | 7,8:
   @(stmt_P_mp … (f_inv f))
-  #s * #V #L %
+  #s * #V #L #R %
   [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX)
     [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en))

src/Cminor/syntax.ma

@@ -128 +128 @@
 ].
 
-record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (s:stmt) : Prop ≝ {
+inductive rettyp_match : option typ → option (𝚺t.expr t) → Prop ≝
+| rettyp_none : rettyp_match (None ?) (None ?)
+| rettyp_some : ∀t,e. rettyp_match (Some ? t) (Some ? ❬t,e❭).
+
+record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (rettyp:option typ) (s:stmt) : Prop ≝ {
   cm_inv_var : stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) env) s;
-  cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s
+  cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s;
+  cm_inv_return : match s with [ St_return oe ⇒ rettyp_match rettyp oe
+                               | _ ⇒ True ]
 }.
 
@@ -142 +148 @@
      (* Ensure that variables appear in the params and vars list with the
         correct typ; and that all goto labels used are declared. *)
-; f_inv       : stmt_P (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body)) f_body
+; f_inv       : stmt_P (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body) f_return) f_body
 }.
 

src/Cminor/toRTLabs.ma

@@ -837 +837 @@
   ).
 [ -emptyfn @(stmt_P_mp … (f_inv f))
-  #s * #V #L %
+  #s * #V #L #R %
   [ @(stmt_vars_mp … V)
     #i #t #H cases (Exists_append … H)