Changeset 3259 for src/common


Ignore:
Timestamp:
May 9, 2013, 12:49:38 AM (7 years ago)
Author:
piccolo
Message:

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues.ma

    r2927 r3259  
    277277  [ BBbit b ⇒ OK … b
    278278  | _ ⇒ Error … [MSG err]].
     279
     280definition eq_option_map : ∀A: Type[0].(A → A → bool) → option A → option A → bool ≝
     281λA,eq,a1,a2.
     282match a1 with
     283[ Some x ⇒ match a2 with [Some y ⇒ eq x y | _ ⇒ false ]
     284| None ⇒ match a2 with [None ⇒ true | _ ⇒ false]
     285].
     286
     287lemma eq_option_map_elim : ∀A : Type[0].∀P:bool → Prop.∀eq,
     288x,y. (∀P:bool → Prop.∀z,w.(z = w → P true) → (z ≠w → P false) → P (eq z w)) →
     289(x = y → P true) → (x ≠ y → P false) → P (eq_option_map A eq x y).
     290#A #P #eq * [|#x] * [1,3:|*: #y] normalize #H #H1 #H2
     291[@H1 % |2,3: @H2 % #EQ destruct(EQ)] @H
     292[ #EQ @H1 >EQ %
     293| * #H3 @H2 % #EQ destruct @H3 %
     294]
     295qed.
     296
     297
     298definition eq_beval : beval → beval → bool ≝
     299λbv1,bv2.
     300match bv1 with
     301[ BVundef ⇒ match bv2 with [ BVundef ⇒ true | _ ⇒ false ]
     302| BVnonzero ⇒ match bv2 with [ BVnonzero ⇒ true | _ ⇒ false ]
     303| BVXor pt1 pt1' p1 ⇒
     304  match bv2 with
     305  [ BVXor pt2 pt2' p2 ⇒ eq_option_map … eq_pointer pt1 pt2 ∧
     306                        eq_option_map … eq_pointer pt1' pt2' ∧
     307                        eqb (part_no … p1) (part_no … p2)
     308  | _ ⇒ false
     309  ]
     310| BVByte b1 ⇒ match bv2 with [ BVByte b2 ⇒ eq_bv … b1 b2 | _ ⇒ false]
     311| BVnull p1 ⇒ match bv2 with
     312              [ BVnull p2 ⇒ eqb (part_no … p1) (part_no … p2) | _ ⇒ false ]
     313| BVptr ptr1 p1 ⇒ match bv2 with
     314                 [ BVptr ptr2 p2 ⇒ eq_pointer ptr1 ptr2 ∧
     315                                   eqb (part_no … p1) (part_no … p2)
     316                 | _ ⇒ false
     317                 ]
     318| BVpc pc1 p1 ⇒ match bv2 with
     319                [ BVpc pc2 p2 ⇒ eq_program_counter pc1 pc2 ∧
     320                  eqb (part_no … p1) (part_no … p2)
     321                | _⇒ false
     322                ]
     323].
     324
     325lemma eq_beval_elim : ∀P:bool → Prop.∀x,y.
     326(x = y → P true) → (x ≠ y → P false) → P (eq_beval x y).
     327#P *
     328[|| #pt1 #pt1' #p1 | #b1 | #p1 | #ptr1 #p1 | #pc1 #p1 ]
     329*
     330[1,8,15,22,29,36,43:
     331|2,9,16,23,30,37,44:
     332|3,10,17,24,31,38,45: #pt2 #pt2' #p2
     333|4,11,18,25,32,39,46: #b2
     334|5,12,19,26,33,40,47: #p2
     335|6,13,20,26,34,41,48: #ptr2 #p2
     336|*: #pc2 #p2
     337]
     338normalize nodelta #H1 #H2 try(@H1 %) try(@H2 % #EQ destruct)
     339whd in match eq_beval; normalize nodelta
     340[ @eq_option_map_elim
     341 [ @eq_pointer_elim
     342 |3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H %
     343 | normalize nodelta #EQ destruct(EQ) @eq_option_map_elim
     344 [ @eq_pointer_elim
     345 |3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H %
     346 | #EQ destruct(EQ) cases p1 in H1 H2; -p1 cases p2 -p2
     347   #p2 #prf #p1 #prf1 #H1 #H2 @eqb_elim
     348  [ #EQ destruct(EQ) @H1 %
     349  | * #H @H2 % #EQ destruct(EQ) @H %
     350  ]
     351 ]
     352 ]
     353| @eq_bv_elim [#EQ destruct(EQ) @H1 % | * #H @H2 % #EQ destruct(EQ) @H %]
     354| cases p1 in H1 H2; -p1 cases p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
     355 [ #EQ destruct(EQ) @H1 %
     356 | * #H @H2 % #EQ destruct @H %
     357 ]
     358| @eq_pointer_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct(EQ)
     359  cases p1 in H1 H2; -p1 cases p2 -p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
     360  [#EQ destruct @H1 %
     361  | * #H @H2 % #EQ destruct @H %
     362  ]
     363| @eq_program_counter_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct
     364  cases p1 in H1 H2; -p1 cases p2 -p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
     365  [ #EQ destruct @H1 %
     366  | * #H @H2 % #EQ destruct @H %
     367  ]
     368]
     369qed.
  • src/common/ExtraIdentifiers.ma

    r3217 r3259  
    2121[//] #i #IH #f #b @IH
    2222qed.
    23    
     23
     24let rec pm_clean (A : Type[0]) (p : positive_map A) on p : positive_map A ≝
     25match p with
     26[ pm_leaf ⇒ pm_leaf A
     27| pm_node a l r ⇒ let l' ≝ pm_clean A l in
     28                  let r' ≝ pm_clean A r in
     29                  if andb (is_none ? a)
     30                      (andb (is_pm_leaf ? l') (is_pm_leaf ? r')) then
     31                     pm_leaf A
     32                  else
     33                     pm_node ? a l' r'
     34].
     35 
     36lemma lookup_pm_clean : ∀A : Type[0].∀p,p' : positive_map A.
     37(∀i.lookup_opt A i p = lookup_opt A i p') →
     38pm_clean A p = pm_clean A p'.
     39#A #p elim p
     40[ #p' elim p' [ #_ normalize %] * [2: #a] #l #r #IHl #IHr #H normalize
     41  [ lapply(H one) normalize #EQ destruct]
     42  <IHl [2,4: #i lapply(H (p0 i)) normalize //] normalize
     43  <IHr [2,4: #i lapply(H (p1 i)) normalize //] %
     44| #opt_a #l #r #IHl #IHr *
     45  [ #H normalize lapply(H one) normalize #EQ destruct(EQ) normalize
     46    >(IHl (pm_leaf ?)) [2: #i lapply(H (p0 i)) normalize //] normalize
     47    >(IHr (pm_leaf ?)) [2: #i lapply(H (p1 i)) normalize //] %
     48  | #opt_a' #l' #r' #H normalize lapply(H one) normalize #EQ destruct(EQ)
     49    >(IHl l') [2: #i lapply(H (p0 i)) normalize //]
     50    >(IHr r') [2: #i lapply(H (p1 i)) normalize //] %
     51  ]
     52]
     53qed. 
     54
     55definition pm_find_all : ∀A : Type[0].positive_map A →
     56(Pos → A → bool) → positive_map A ≝
     57λA,p,P.fold ??
     58 (λi,a,p'.if P i a then pm_set ? i (Some ? a) p' else p') p (pm_leaf A).
     59 
     60
     61lemma pm_clean_idempotent : ∀A : Type[0].∀p : positive_map A.
     62pm_clean ? p = pm_clean ? (pm_clean ? p).
     63cases daemon
     64qed.
     65
     66 
     67lemma pm_find_all_canonic : ∀A : Type[0].∀p : positive_map A.∀P.
     68pm_find_all A p P = pm_clean A (pm_find_all A p P).
     69#A #p #P whd in match pm_find_all; normalize nodelta
     70@pm_fold_ind
     71[ %] #i #ps #a #b #H #H1 #H2 cases(P i a) normalize
     72[2: assumption] lapply H2 lapply b elim i
     73[ normalize * [ #_ %] #opt_a #l #r
     74  normalize nodelta normalize cases opt_a
     75  [2: #a1 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?);
     76      >e1 in ⊢ (??%?); % ] normalize
     77  cases(pm_clean ? l) normalize [2: #opt_a1 #l1 #r1
     78  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?); %]
     79  cases(pm_clean ? r) normalize [#EQ destruct] #opt_a1 #l1 #r1
     80  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct %
     81|*: #x #IH * normalize
     82   [1,3: #_ <IH [2,4: % ]
     83    inversion(pm_set A x ??) [2,4: #opt_a1 #l1 #r1 #_#_#_ %]
     84    #ABS @⊥ cases x in ABS; [1,4: normalize #EQ destruct] #x1 normalize
     85    #EQ destruct
     86   |*: * [2,4: #a1] #l #r normalize
     87       [1,2: #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?);
     88             >e1 in ⊢ (??%?); <IH
     89             [ @eq_f3 try % >e1 in ⊢ (???%); %
     90             | assumption
     91             | @eq_f3 try % @pm_clean_idempotent
     92             | @pm_clean_idempotent
     93             ]
     94       |*: inversion(pm_clean A l) normalize
     95           [ #H3 inversion(pm_clean A r) normalize [#_ #EQ destruct] #opt_a1 #l1 #r1
     96             #_ #_ #H4 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ  <(IH r)
     97             [2: cut(r = pm_node A opt_a1 l1 r1) [ destruct %] #H5
     98             >H5 in ⊢ (??%?); <H4 % ] inversion(pm_set A x ??)
     99             [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %]
     100             #ABS @⊥ cases x in ABS; normalize cases r normalize
     101             [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
     102             #EQ1 destruct
     103           | #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     104             <(IH r) [destruct %] destruct assumption
     105           | #H3 cases(pm_clean A r) normalize [#EQ destruct] #opt_a1 #l1 #r1
     106              #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ <(IH l) [2: >H3 destruct %]
     107              inversion(pm_set A x ??)
     108              [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %]
     109              #ABS @⊥ cases x in ABS; normalize cases l normalize
     110              [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
     111              #EQ1 destruct
     112           | #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     113             <(IH l) [2: >H3 destruct %] inversion(pm_set A x ??)
     114              [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct >e0 in ⊢ (??%?); %]
     115              #ABS @⊥ cases x in ABS; normalize cases l normalize
     116              [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
     117              #EQ1 destruct
     118           ] 
     119       ]   
     120   ]
     121]
     122qed. 
     123
    24124
    25125definition find_all : ∀tag,A. identifier_map tag A →
    26126(identifier tag → A → bool) → identifier_map tag A ≝
    27 λtag,A,m,P.foldi A (identifier_map tag A) tag
    28 (λi,a,l.if (P i a) then (add tag A l i a) else l) m (empty_map tag A).
    29 
     127λtag,A,m,P.match m with
     128  [an_id_map p ⇒ an_id_map ?? (pm_find_all A p (λx,a.P (an_identifier tag x) a))].
     129(*
    30130
    31131lemma find_all_lookup_predicate : ∀tag,A.∀m : identifier_map tag A.
     
    33133lookup tag A (find_all tag A m P) i = Some ? a →
    34134lookup tag A m i = Some ? a  ∧ (bool_to_Prop (P i a)).
    35 #tag #A #m #P #i #a whd in match find_all; normalize nodelta @foldi_ind
     135#tag #A * #m #P * #i #a whd in match find_all; normalize @pm_fold_ind
    36136[ normalize #EQ destruct
    37 | #k #ks #a1 #b * #H #H1 #H2 inversion(P k a1)
    38   [ #H3 normalize nodelta >H3
    39     cut(bool_to_Prop (eq_identifier tag i k) ∨
     137| #k #ks #a1 #b * #H #H1 #H2 inversion(P (an_identifier tag i) a1)
     138  [ cases(decidable_eq_pos i k)
     139    [#EQ destruct #H3 >H3 in H2; normalize >looku
     140
     141
     142  [#EQ destruct inversion(
     143
     144  [ #H3 normalize nodelta >H3 cases(decidable_eq_pos i k)
     145    [ #EQ destruct >H3 in H2;
     146 
     147 
     148    cut(bool_to_Prop (eq_identifier tag (an_identifier tag i) (an_identifierk) ∨
    40149     (bool_to_Prop (notb (eq_identifier tag i k))))
    41150    [@eq_identifier_elim #_ [ %%|%2 %]]
     
    68177]
    69178qed.
    70 
     179*)
    71180(*
    72181 whd in match (add ?????); whd in match (add ?????); normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.