Ignore:
Timestamp:
Aug 3, 2011, 1:04:48 PM (9 years ago)
Author:
campbell
Message:

Checkpoint part way through adding proper C label checking to the branch.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

    r1087 r1096  
    3939] qed.
    4040
     41axiom Label : String.
     42
    4143inductive stmt : Type[0] ≝
    4244| St_skip : stmt
     
    5456| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
    5557| St_return : option (Σt. expr t) → stmt
    56 | St_label : ident → stmt → stmt
    57 | St_goto : ident → stmt
     58| St_label : identifier Label → stmt → stmt
     59| St_goto : identifier Label → stmt
    5860| St_cost : costlabel → stmt → stmt.
    5961
     62let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
     63match s with
     64[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
     65| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
     66| St_loop s' ⇒ P s ∧ stmt_P P s'
     67| St_block s' ⇒ P s ∧ stmt_P P s'
     68| St_label _ s' ⇒ P s ∧ stmt_P P s'
     69| St_cost _ s' ⇒ P s ∧ stmt_P P s'
     70| _ ⇒ P s
     71].
     72
     73lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
     74#P * normalize /2/
     75[ #s1 #s2 * * /2/
     76| #sz #sg #e #s1 #s2 * * /2/
     77| 3,4: #s * /2/
     78| 5,6: #i #s normalize * /2/
     79] qed.
     80
    6081(* Assert a predicate on every variable or parameter identifier. *)
    61 let rec stmt_vars (s:stmt) (P:ident → Prop) on s : Prop ≝
     82definition stmt_vars : (ident → Prop) → stmt → Prop ≝
     83λP,s.
    6284match s with
    63 [ St_skip ⇒ True
    64 | St_assign _ i e ⇒ P i ∧ expr_vars ? e P
     85[ St_assign _ i e ⇒ P i ∧ expr_vars ? e P
    6586| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    6687| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
    6788| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
    68 | St_seq s1 s2 ⇒ stmt_vars s1 P ∧ stmt_vars s2 P
    69 | St_ifthenelse _ _ e s1 s2 ⇒ expr_vars ? e P ∧ stmt_vars s1 P ∧ stmt_vars s2 P
    70 | St_loop s ⇒ stmt_vars s P
    71 | St_block s ⇒ stmt_vars s P
    72 | St_exit _ ⇒ True
     89| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
    7390| St_switch _ _ e _ _ ⇒ expr_vars ? e P
    7491| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ]
    75 | St_label _ s ⇒ stmt_vars s P
    76 | St_goto _ ⇒ True
    77 | St_cost _ s ⇒ stmt_vars s P
     92| _ ⇒ True
    7893].
    7994
    80 lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars s P → stmt_vars s Q.
     95definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝
     96λP,s.
     97match s with
     98[ St_label l _ ⇒ P l
     99| St_goto l ⇒ P l
     100| _ ⇒ True
     101].
     102
     103lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
     104#P #Q #H #s elim s /2/
     105[ #s1 #s2 #H1 #H2 normalize * * /4/
     106| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
     107| #s #H * /5/
     108| #s #H * /5/
     109| #l #s #H * /5/
     110| #l #s #H * /5/
     111] qed.
     112
     113lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars P s → stmt_vars Q s.
    81114#P #Q #H #s elim s normalize
    82115[ //
     
    86119| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
    87120| #s1 #s2 #H1 #H2 * /3/
    88 | #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
     121| #sz #sg #e #s1 #s2 #H1 #H2 /5/
    89122| 8,9: #s #H1 #H2 /2/
    90123| //
     
    96129] qed.
    97130
     131(* Get labels from a Cminor statement. *)
     132let rec labels_of (s:stmt) : list (identifier Label) ≝
     133match s with
     134[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
     135| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
     136| St_loop s ⇒ labels_of s
     137| St_block s ⇒ labels_of s
     138| St_label l s ⇒ l::(labels_of s)
     139| St_cost _ s ⇒ labels_of s
     140| _ ⇒ [ ]
     141].
     142
    98143record internal_function : Type[0] ≝
    99144{ f_return    : option typ
     
    102147; f_stacksize : nat
    103148; f_body      : stmt
    104 ; f_bound     : stmt_vars f_body (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars))
     149; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
     150                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
    105151}.
    106152
Note: See TracChangeset for help on using the changeset viewer.