Changeset 2251 for src/Cminor


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/Cminor
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • 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.