Ignore:
Timestamp:
May 9, 2013, 12:49:38 AM (6 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

File:
1 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.
Note: See TracChangeset for help on using the changeset viewer.