Changeset 1096


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

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

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma

    r1087 r1096  
    741741    ].
    742742*)
    743 definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.stmt_vars s (local_id vars)) ≝
     743
     744definition lenv ≝ identifier_map SymbolTag (identifier Label).
     745
     746definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup ?? lbls l' = Some ? l.
     747
     748definition stmt_inv ≝
     749λvars. λlbls:lenv.
     750  stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s).
     751
     752definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝
    744753λvars,e1,e2.
    745754do e2' ← translate_expr vars e2;
     
    749758| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
    750759].
    751 whd
     760#ls whd %
    752761[ % // @sig_ok
     762| @I
    753763| % @sig_ok
     764| @I
    754765] qed.
    755766
     
    783794] qed.
    784795
    785 let rec translate_statement (vars:var_types) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs:stmt.stmt_vars s (local_id vars)) ≝
     796axiom MissingLabel : String.
     797
     798definition lookup_label ≝
     799λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
     800
     801lemma lookup_label_hit : ∀lbls,l,l'.
     802  lookup_label lbls l = OK ? l' →
     803  lpresent lbls l'.
     804#lbls #l #l' whd in ⊢ (??%? → %) #E %{l} cases (lookup ??? l) in E ⊢ %
     805normalize #x try #y destruct /2/
     806qed.
     807
     808let rec translate_statement (vars:var_types) (lbls:lenv) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs:stmt.stmt_inv vars lbls s) ≝
    786809match s with
    787810[ Sskip ⇒ OK ? «St_skip, ?»
    788 | Sassign e1 e2 ⇒ translate_assign vars e1 e2
     811| Sassign e1 e2 ⇒
     812    do s' ← translate_assign vars e1 e2;
     813    OK ? «eject ?? s', ?»
    789814| Scall ret ef args ⇒
    790815    do ef' ← translate_expr vars ef;
     
    803828    ]
    804829| Ssequence s1 s2 ⇒
    805     do s1' ← translate_statement vars tmp tmpp s1;
    806     do s2' ← translate_statement vars tmp tmpp s2;
     830    do s1' ← translate_statement vars lbls tmp tmpp s1;
     831    do s2' ← translate_statement vars lbls tmp tmpp s2;
    807832    OK ? «St_seq s1' s2', ?»
    808833| Sifthenelse e1 s1 s2 ⇒
     
    810835    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    811836    [ ASTint _ _ ⇒ λe1'.
    812         do s1' ← translate_statement vars tmp tmpp s1;
    813         do s2' ← translate_statement vars tmp tmpp s2;
     837        do s1' ← translate_statement vars lbls tmp tmpp s1;
     838        do s2' ← translate_statement vars lbls tmp tmpp s2;
    814839        OK ? «St_ifthenelse ?? e1' s1' s2', ?»
    815840    | _ ⇒ λ_.Error ? (msg TypeMismatch)
     
    819844    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    820845    [ ASTint _ _ ⇒ λe1'.
    821         do s1' ← translate_statement vars tmp tmpp s1;
     846        do s1' ← translate_statement vars lbls tmp tmpp s1;
    822847        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    823848        OK ? «St_block
     
    830855    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    831856    [ ASTint _ _ ⇒ λe1'.
    832         do s1' ← translate_statement vars tmp tmpp s1;
     857        do s1' ← translate_statement vars lbls tmp tmpp s1;
    833858        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    834859        OK ? «St_block
     
    841866    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    842867    [ ASTint _ _ ⇒ λe1'.
    843         do s1' ← translate_statement vars tmp tmpp s1;
    844         do s2' ← translate_statement vars tmp tmpp s2;
    845         do s3' ← translate_statement vars tmp tmpp s3;
     868        do s1' ← translate_statement vars lbls tmp tmpp s1;
     869        do s2' ← translate_statement vars lbls tmp tmpp s2;
     870        do s3' ← translate_statement vars lbls tmp tmpp s3;
    846871        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    847872        OK ? «St_seq s1'
     
    862887| Sswitch e1 ls ⇒ Error ? (msg FIXME)
    863888| Slabel l s1 ⇒
    864     do s1' ← translate_statement vars tmp tmpp s1;
    865     OK ? «St_label l s1', ?»
    866 | Sgoto l ⇒ OK ? «St_goto l, ?»
     889    do l' as E ← lookup_label lbls l;
     890    do s1' ← translate_statement vars lbls tmp tmpp s1;
     891    OK ? «St_label l' s1', ?»
     892| Sgoto l ⇒
     893    do l' as E ← lookup_label lbls l;
     894    OK ? «St_goto l', ?»
    867895| Scost l s1 ⇒
    868     do s1' ← translate_statement vars tmp tmpp s1;
     896    do s1' ← translate_statement vars lbls tmp tmpp s1;
    869897    OK ? «St_cost l s1', ?»
    870898].
    871 whd try @I
    872 [ % [ % [ @p | @sig_ok ] | @(sig_ok ? (All ??)) ]
    873 | % [ whd % [ % [ @sig_ok | @sig_ok ] | @(sig_ok ? (All ??)) ] | whd % @sig_ok ]
    874 | % [ % [ @I | @sig_ok ] | @(sig_ok ? (All ??)) ]
    875 | % @sig_ok
    876 | % [ % @sig_ok | @sig_ok ]
    877 | % [ % @sig_ok | whd @I ]
    878 | % [ @sig_ok | whd % [ % [ @sig_ok | @I ] | @I ] ]
    879 | % [ @sig_ok | whd % [ % [ @sig_ok | whd % @sig_ok ] | @I ] ]
    880 | @sig_ok
    881 | @sig_ok
    882 | @sig_ok
     899try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
     900try @I
     901try @(sig_ok ? (λs.stmt_inv ?? s))
     902try @(sig_ok ? (λe.expr_vars ? e ?))
     903try @(sig_ok ? (λs.stmt_vars ?? s))
     904try @(sig_ok ? (λs.stmt_labels ?? s))
     905try @(sig_ok ? (All ??))
     906try @(sig_ok ? (local_id vars))
     907try @(lookup_label_hit … E)
     908[ @(sig_ok ?? s')
     909| @p
     910] qed.
     911
     912let rec labels_defined (s:statement) : list ident ≝
     913match s with
     914[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
     915| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
     916| Swhile _ s ⇒ labels_defined s
     917| Sdowhile _ s ⇒ labels_defined s
     918| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
     919| Sswitch _ ls ⇒ labels_defined_switch ls
     920| Slabel l s ⇒ l::(labels_defined s)
     921| Scost _ s ⇒ labels_defined s
     922| _ ⇒ [ ]
     923]
     924and labels_defined_switch (ls:labeled_statements) : list ident ≝
     925match ls with
     926[ LSdefault s ⇒ labels_defined s
     927| LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls
     928].
     929
     930lemma OK_sig_eq : ∀A,P,x,xp,y,yp. OK (Σx:A.P x) «x,xp» = OK (Σx:A.P x) «y,yp» → x = y.
     931#A #P #x #xp #y #yp #E destruct @refl
     932qed.
     933
     934definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
     935
     936lemma Exists_append : ∀A,P,l1,l2.
     937  Exists A P (l1@l2) →
     938  Exists A P l1 ∨ Exists A P l2.
     939#A #P #l1 elim l1
     940[ #l2 #H %2 @H
     941| #h #t #IH #l2 whd in ⊢ (% → ?) *
     942  [ #H %1 %1 @H
     943  | #H cases (IH l2 H) /4/
     944  ]
     945] qed.
     946
     947lemma Exists_append_l : ∀A,P,l1,l2.
     948  Exists A P l1 → Exists A P (l1@l2).
     949#A #P #l1 #l2 elim l1
     950[ *
     951| #h #t #IH *
     952  [ #H %1 @H
     953  | #H %2 @IH @H
     954  ]
     955] qed.
     956
     957lemma Exists_append_r : ∀A,P,l1,l2.
     958  Exists A P l2 → Exists A P (l1@l2).
     959#A #P #l1 #l2 elim l1
     960[ #H @H
     961| #h #t #IH #H %2 @IH @H
     962] qed.
     963
     964lemma reflmatch : ∀A,B,e.∀P:∀v:A. e = OK ? v → res B.∀x.
     965 match e return λx.e = x → ? with [ OK v ⇒ P v | Error m ⇒ λ_.Error ? m ] (refl ? e) = OK ? x →
     966 ∃v,p. P v p = OK ? x.
     967#A #B *
     968[ #v #P #x normalize #H %{v} % [ @refl | @H ]
     969| #m #P #x normalize #H destruct
     970] qed.
     971
     972lemma labels_translated : ∀vars,lbls,tmp,tmpp,s,l,s',p.
     973  (Exists ? (λl'.l' = l) (labels_defined s)) →
     974  translate_statement vars lbls tmp tmpp s = OK ? «s', p» →
     975  ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'.
     976#vars #lbls #tmp #tmpp #s #l @(statement_ind … s) (* FIXME: once switch is done we'll need something else here *)
     977[ #s' #p *
     978| #e1 #e2 #s' #p *
     979| #eo #e #args #s' #p *
     980| #s1 #s2 #IH1 #IH2 #s' #p #H #E
     981  cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
     982  cases (bind_inversion ????? E) * #s2' #I2 * #E2 -E #E
     983  <(OK_sig_eq ?????? E) -E;
     984  cases (Exists_append ???? H)
     985  [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_l @L2 ]
     986  | #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @L2 ]
     987  ]
     988| #e #s1 #s2 #IH1 #IH2 #s' #p #H #E
     989  (* Carefully get rid of the equality that will screw up the case analysis *)
     990  cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
     991  [ #sz #sg #e' #E
     992    cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
     993    cases (bind_inversion ????? E) * #s2' #I2 * #E2 -E #E
     994    <(OK_sig_eq ?????? E) -E;
     995    cases (Exists_append ???? H)
     996    [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_l @L2 ]
     997    | #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @L2 ]
     998    ]
     999  | *: #x #e' normalize #E destruct
     1000  ]
     1001| #e #s #IH #s' #p #H #E
     1002  (* Carefully get rid of the equality that will screw up the case analysis *)
     1003  cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
     1004  [ #sz #sg #e' #E
     1005    cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
     1006    <(OK_sig_eq ?????? E) -E;
     1007    cases (IH s1' I1 H E1) #l' * #La #Lb %{l'} % [ @La | whd; normalize in ⊢ (???%) >append_nil @Lb ]
     1008  | *: #x #e' normalize #E destruct
     1009  ]
     1010| #e #s #IH #s' #p #H #E
     1011  (* Carefully get rid of the equality that will screw up the case analysis *)
     1012  cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
     1013  [ #sz #sg #e' #E
     1014    cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
     1015    <(OK_sig_eq ?????? E) -E;
     1016    cases (IH s1' I1 H E1) #l' * #La #Lb %{l'} % [ @La | whd; normalize in ⊢ (???%) >append_nil @Lb ]
     1017  | *: #x #e' normalize #E destruct
     1018  ]
     1019| #s1 #e #s1 #s2 #IH1 #IH2 #IH3 #s' #p #H #E
     1020  (* Carefully get rid of the equality that will screw up the case analysis *)
     1021  cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
     1022  [ #sz #sg #e' #E
     1023    cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
     1024    cases (bind_inversion ????? E) * #s2' #I2 * #E2 -E #E
     1025    cases (bind_inversion ????? E) * #s3' #I3 * #E3 -E #E
     1026    <(OK_sig_eq ?????? E) -E;
     1027    cases (Exists_append ???? H)
     1028    [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_l @L2 ]
     1029    | -H #H cases (Exists_append ???? H)
     1030      [ #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @Exists_append_l @Exists_append_r @L2 ]
     1031      | #H3 cases (IH3 s3' I3 H3 E3) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @Exists_append_l @Exists_append_l @L2 ]
     1032      ]
     1033    ]
     1034  | *: #x #e' normalize #E destruct
     1035  ]
     1036| #s' #p *
     1037| #s' #p *
     1038| #eo #s' #p *
     1039| #e #ls #IH #s' #p #H #E whd in E:(??%?); destruct (* FIXME once switch is implemented ... *)
     1040| #l0 #s0 #IH #s' #p #H
     1041  whd in ⊢ (??%? → ?) #E cases (reflmatch ????? E) -E #l1 * #El #E
     1042  cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
     1043  <(OK_sig_eq ?????? E) -E;
     1044  cases H
     1045  [ #El' %{l1} <El' % [ @El | %1 @refl ]
     1046  | #H1 cases (IH s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | %2 @L2 ]
     1047  ]
     1048| #l0 #s' #p *
     1049| #l0 #s0 #IH #s' #p #H #E
     1050  cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
     1051  <(OK_sig_eq ?????? E) -E;
     1052  @(IH s1' I1 H E1)
    8831053] qed.
    8841054
    8851055axiom ParamGlobalMixup : String.
    8861056
    887 definition alloc_params : ∀vars:var_types. list (ident×type) → (Σs:stmt.stmt_vars s (local_id vars)) → res (Σs:stmt.stmt_vars s (local_id vars)) ≝
    888 λvars,params,s. foldl ?? (λs,it.
     1057definition alloc_params : ∀vars:var_types.∀ls. list (ident×type) → (Σs:stmt. stmt_inv vars ls s) → res (Σs:stmt.stmt_inv vars ls s) ≝
     1058λvars,ls,params,s. foldl ?? (λs,it.
    8891059  let 〈id,ty〉 ≝ it in
    8901060  do s ← s;
     
    9011071  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
    9021072  ] E) (OK ? s) params.
    903 whd % [ whd % [ @I | whd >E @I ] | @sig_ok ]
    904 qed.
     1073try @conj try @conj try @conj try @conj try @conj
     1074try @I
     1075[ whd >E @I
     1076| @(sig_ok … s)
     1077] qed.
    9051078
    9061079definition bigid1 ≝ an_identifier SymbolTag [[
     
    9481121] qed.
    9491122
     1123(* We only record labels from Slabel, not Sgoto, so that we detect badly formed
     1124   programs. *)
     1125let rec extend_label_env (s:statement) (lbls:lenv) (u:universe ?) : lenv × (universe ?) ≝
     1126match s with
     1127[ Ssequence s1 s2 ⇒
     1128    let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in
     1129    extend_label_env s2 lbls u
     1130| Sifthenelse _ s1 s2 ⇒
     1131    let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in
     1132    extend_label_env s2 lbls u
     1133| Swhile _ s ⇒ extend_label_env s lbls u
     1134| Sdowhile _ s ⇒ extend_label_env s lbls u
     1135| Sfor s1 _ s2 s3 ⇒
     1136    let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in
     1137    let 〈lbls,u〉 ≝ extend_label_env s2 lbls u in
     1138    extend_label_env s3 lbls u
     1139| Sswitch _ ls ⇒ extend_label_env' ls lbls u
     1140| Slabel l s ⇒
     1141    let 〈l',u〉 ≝ fresh ? u in
     1142    extend_label_env s (add … lbls l l') u
     1143| Scost _ s ⇒ extend_label_env s lbls u
     1144| _ ⇒ 〈lbls,u〉
     1145]
     1146and extend_label_env' (ls:labeled_statements) (lbls:lenv) (u:universe ?) : lenv × (universe ?) ≝
     1147match ls with
     1148[ LSdefault s ⇒ extend_label_env s lbls u
     1149| LScase _ _ s ls ⇒
     1150    let 〈lbls,u〉 ≝ extend_label_env s lbls u in
     1151    extend_label_env' ls lbls u
     1152].
     1153
     1154definition build_label_env ≝ λbody. extend_label_env body (empty_map ??) (new_universe ?).
     1155
    9501156(* FIXME: the temporary handling is nonsense, I'm afraid. *)
    9511157definition translate_function : list (ident×region) → function → res internal_function ≝
    9521158λglobals, f.
     1159  let 〈lbls, label_universe〉 ≝ build_label_env (fn_body f) in
    9531160  let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in
    9541161  let tmp ≝ bigid1 in (* FIXME *)
    9551162  let tmpp ≝ bigid2 in (* FIXME *)
    9561163  let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in
    957   do s ← translate_statement vartypes tmp tmpp (fn_body f);
    958   do s ← alloc_params vartypes (fn_params f) s;
     1164  do s as E1 ← translate_statement vartypes lbls tmp tmpp (fn_body f);
     1165  do s as E2 ← alloc_params vartypes lbls (fn_params f) s;
    9591166  OK ? (mk_internal_function
    9601167    (opttyp_of_type (fn_return f))
     
    9651172[ whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit %
    9661173| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
    967 | @stmt_vars_mp [ 3: @sig_ok | skip ]
     1174| @(stmt_P_mp ???? (sig_ok ?? s))
     1175  #s1 * #H1 #H2 % [ 2: @H2 ]
     1176  @stmt_vars_mp [ 3: @sig_ok | skip ]
    9681177  #i #H cases (identifier_eq ? tmp i)
    9691178  [ #E <E @Exists_mid @refl
  • 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.