Changeset 3259 for src/common

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:

• ByteValues.ma (modified) (1 diff)
• ExtraIdentifiers.ma (modified) (3 diffs)

src/common/ByteValues.ma

@@ -277 +277 @@
   [ BBbit b ⇒ OK … b
   | _ ⇒ Error … [MSG err]].
+
+definition eq_option_map : ∀A: Type[0].(A → A → bool) → option A → option A → bool ≝ 
+λA,eq,a1,a2.
+match a1 with
+[ Some x ⇒ match a2 with [Some y ⇒ eq x y | _ ⇒ false ]
+| None ⇒ match a2 with [None ⇒ true | _ ⇒ false]
+].
+
+lemma eq_option_map_elim : ∀A : Type[0].∀P:bool → Prop.∀eq,
+x,y. (∀P:bool → Prop.∀z,w.(z = w → P true) → (z ≠w → P false) → P (eq z w)) → 
+(x = y → P true) → (x ≠ y → P false) → P (eq_option_map A eq x y).
+#A #P #eq * [|#x] * [1,3:|*: #y] normalize #H #H1 #H2 
+[@H1 % |2,3: @H2 % #EQ destruct(EQ)] @H 
+[ #EQ @H1 >EQ % 
+| * #H3 @H2 % #EQ destruct @H3 %
+]
+qed.
+
+
+definition eq_beval : beval → beval → bool ≝ 
+λbv1,bv2.
+match bv1 with
+[ BVundef ⇒ match bv2 with [ BVundef ⇒ true | _ ⇒ false ]
+| BVnonzero ⇒ match bv2 with [ BVnonzero ⇒ true | _ ⇒ false ]
+| BVXor pt1 pt1' p1 ⇒ 
+  match bv2 with 
+  [ BVXor pt2 pt2' p2 ⇒ eq_option_map … eq_pointer pt1 pt2 ∧ 
+                        eq_option_map … eq_pointer pt1' pt2' ∧ 
+                        eqb (part_no … p1) (part_no … p2)
+  | _ ⇒ false
+  ]
+| BVByte b1 ⇒ match bv2 with [ BVByte b2 ⇒ eq_bv … b1 b2 | _ ⇒ false]
+| BVnull p1 ⇒ match bv2 with 
+              [ BVnull p2 ⇒ eqb (part_no … p1) (part_no … p2) | _ ⇒ false ]
+| BVptr ptr1 p1 ⇒ match bv2 with 
+                 [ BVptr ptr2 p2 ⇒ eq_pointer ptr1 ptr2 ∧ 
+                                   eqb (part_no … p1) (part_no … p2) 
+                 | _ ⇒ false 
+                 ]
+| BVpc pc1 p1 ⇒ match bv2 with 
+                [ BVpc pc2 p2 ⇒ eq_program_counter pc1 pc2 ∧ 
+                  eqb (part_no … p1) (part_no … p2) 
+                | _⇒ false 
+                ]
+].
+
+lemma eq_beval_elim : ∀P:bool → Prop.∀x,y.
+(x = y → P true) → (x ≠ y → P false) → P (eq_beval x y).
+#P *
+[|| #pt1 #pt1' #p1 | #b1 | #p1 | #ptr1 #p1 | #pc1 #p1 ]
+*
+[1,8,15,22,29,36,43:
+|2,9,16,23,30,37,44:
+|3,10,17,24,31,38,45: #pt2 #pt2' #p2
+|4,11,18,25,32,39,46: #b2
+|5,12,19,26,33,40,47: #p2
+|6,13,20,26,34,41,48: #ptr2 #p2
+|*: #pc2 #p2
+]
+normalize nodelta #H1 #H2 try(@H1 %) try(@H2 % #EQ destruct)
+whd in match eq_beval; normalize nodelta
+[ @eq_option_map_elim 
+ [ @eq_pointer_elim 
+ |3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H %
+ | normalize nodelta #EQ destruct(EQ) @eq_option_map_elim
+ [ @eq_pointer_elim
+ |3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H %
+ | #EQ destruct(EQ) cases p1 in H1 H2; -p1 cases p2 -p2
+   #p2 #prf #p1 #prf1 #H1 #H2 @eqb_elim
+  [ #EQ destruct(EQ) @H1 %
+  | * #H @H2 % #EQ destruct(EQ) @H %
+  ]
+ ]
+ ]
+| @eq_bv_elim [#EQ destruct(EQ) @H1 % | * #H @H2 % #EQ destruct(EQ) @H %]
+| cases p1 in H1 H2; -p1 cases p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
+ [ #EQ destruct(EQ) @H1 %
+ | * #H @H2 % #EQ destruct @H %
+ ]
+| @eq_pointer_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct(EQ)
+  cases p1 in H1 H2; -p1 cases p2 -p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
+  [#EQ destruct @H1 %
+  | * #H @H2 % #EQ destruct @H %
+  ]
+| @eq_program_counter_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct
+  cases p1 in H1 H2; -p1 cases p2 -p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
+  [ #EQ destruct @H1 %
+  | * #H @H2 % #EQ destruct @H %
+  ]
+]
+qed.

src/common/ExtraIdentifiers.ma

@@ -21 +21 @@
 [//] #i #IH #f #b @IH
 qed.
-    
+
+let rec pm_clean (A : Type[0]) (p : positive_map A) on p : positive_map A ≝ 
+match p with
+[ pm_leaf ⇒ pm_leaf A
+| pm_node a l r ⇒ let l' ≝ pm_clean A l in
+                  let r' ≝ pm_clean A r in
+                  if andb (is_none ? a) 
+                      (andb (is_pm_leaf ? l') (is_pm_leaf ? r')) then
+                     pm_leaf A 
+                  else
+                     pm_node ? a l' r'
+]. 
+  
+lemma lookup_pm_clean : ∀A : Type[0].∀p,p' : positive_map A.
+(∀i.lookup_opt A i p = lookup_opt A i p') → 
+pm_clean A p = pm_clean A p'.
+#A #p elim p
+[ #p' elim p' [ #_ normalize %] * [2: #a] #l #r #IHl #IHr #H normalize
+  [ lapply(H one) normalize #EQ destruct] 
+  <IHl [2,4: #i lapply(H (p0 i)) normalize //] normalize
+  <IHr [2,4: #i lapply(H (p1 i)) normalize //] %
+| #opt_a #l #r #IHl #IHr * 
+  [ #H normalize lapply(H one) normalize #EQ destruct(EQ) normalize
+    >(IHl (pm_leaf ?)) [2: #i lapply(H (p0 i)) normalize //] normalize
+    >(IHr (pm_leaf ?)) [2: #i lapply(H (p1 i)) normalize //] %
+  | #opt_a' #l' #r' #H normalize lapply(H one) normalize #EQ destruct(EQ)
+    >(IHl l') [2: #i lapply(H (p0 i)) normalize //]
+    >(IHr r') [2: #i lapply(H (p1 i)) normalize //] %
+  ]
+]
+qed.  
+
+definition pm_find_all : ∀A : Type[0].positive_map A → 
+(Pos → A → bool) → positive_map A ≝ 
+λA,p,P.fold ?? 
+ (λi,a,p'.if P i a then pm_set ? i (Some ? a) p' else p') p (pm_leaf A).
+ 
+
+lemma pm_clean_idempotent : ∀A : Type[0].∀p : positive_map A.
+pm_clean ? p = pm_clean ? (pm_clean ? p).
+cases daemon
+qed. 
+
+ 
+lemma pm_find_all_canonic : ∀A : Type[0].∀p : positive_map A.∀P.
+pm_find_all A p P = pm_clean A (pm_find_all A p P).
+#A #p #P whd in match pm_find_all; normalize nodelta
+@pm_fold_ind
+[ %] #i #ps #a #b #H #H1 #H2 cases(P i a) normalize
+[2: assumption] lapply H2 lapply b elim i 
+[ normalize * [ #_ %] #opt_a #l #r 
+  normalize nodelta normalize cases opt_a 
+  [2: #a1 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?); 
+      >e1 in ⊢ (??%?); % ] normalize
+  cases(pm_clean ? l) normalize [2: #opt_a1 #l1 #r1 
+  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?); %]
+  cases(pm_clean ? r) normalize [#EQ destruct] #opt_a1 #l1 #r1
+  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct %
+|*: #x #IH * normalize 
+   [1,3: #_ <IH [2,4: % ] 
+    inversion(pm_set A x ??) [2,4: #opt_a1 #l1 #r1 #_#_#_ %]
+    #ABS @⊥ cases x in ABS; [1,4: normalize #EQ destruct] #x1 normalize
+    #EQ destruct
+   |*: * [2,4: #a1] #l #r normalize 
+       [1,2: #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?);
+             >e1 in ⊢ (??%?); <IH 
+             [ @eq_f3 try % >e1 in ⊢ (???%); %
+             | assumption
+             | @eq_f3 try % @pm_clean_idempotent
+             | @pm_clean_idempotent
+             ]
+       |*: inversion(pm_clean A l) normalize
+           [ #H3 inversion(pm_clean A r) normalize [#_ #EQ destruct] #opt_a1 #l1 #r1
+             #_ #_ #H4 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ  <(IH r)
+             [2: cut(r = pm_node A opt_a1 l1 r1) [ destruct %] #H5
+             >H5 in ⊢ (??%?); <H4 % ] inversion(pm_set A x ??)
+             [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %]
+             #ABS @⊥ cases x in ABS; normalize cases r normalize 
+             [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ] 
+             #EQ1 destruct
+           | #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
+             <(IH r) [destruct %] destruct assumption
+           | #H3 cases(pm_clean A r) normalize [#EQ destruct] #opt_a1 #l1 #r1
+              #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ <(IH l) [2: >H3 destruct %]
+              inversion(pm_set A x ??) 
+              [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %]
+              #ABS @⊥ cases x in ABS; normalize cases l normalize 
+              [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ] 
+              #EQ1 destruct
+           | #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
+             <(IH l) [2: >H3 destruct %] inversion(pm_set A x ??) 
+              [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct >e0 in ⊢ (??%?); %]
+              #ABS @⊥ cases x in ABS; normalize cases l normalize 
+              [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ] 
+              #EQ1 destruct
+           ]  
+       ]    
+   ]
+]
+qed.  
+
 
 definition find_all : ∀tag,A. identifier_map tag A → 
 (identifier tag → A → bool) → identifier_map tag A ≝ 
-λtag,A,m,P.foldi A (identifier_map tag A) tag 
-(λi,a,l.if (P i a) then (add tag A l i a) else l) m (empty_map tag A).
-
+λtag,A,m,P.match m with 
+  [an_id_map p ⇒ an_id_map ?? (pm_find_all A p (λx,a.P (an_identifier tag x) a))].
+(*
 
 lemma find_all_lookup_predicate : ∀tag,A.∀m : identifier_map tag A. 
@@ -33 +133 @@
 lookup tag A (find_all tag A m P) i = Some ? a → 
 lookup tag A m i = Some ? a  ∧ (bool_to_Prop (P i a)).
-#tag #A #m #P #i #a whd in match find_all; normalize nodelta @foldi_ind
+#tag #A * #m #P * #i #a whd in match find_all; normalize @pm_fold_ind
 [ normalize #EQ destruct
-| #k #ks #a1 #b * #H #H1 #H2 inversion(P k a1) 
-  [ #H3 normalize nodelta >H3
-    cut(bool_to_Prop (eq_identifier tag i k) ∨ 
+| #k #ks #a1 #b * #H #H1 #H2 inversion(P (an_identifier tag i) a1) 
+  [ cases(decidable_eq_pos i k)
+    [#EQ destruct #H3 >H3 in H2; normalize >looku
+
+
+  [#EQ destruct inversion(
+
+  [ #H3 normalize nodelta >H3 cases(decidable_eq_pos i k)
+    [ #EQ destruct >H3 in H2;
+  
+  
+    cut(bool_to_Prop (eq_identifier tag (an_identifier tag i) (an_identifierk) ∨ 
      (bool_to_Prop (notb (eq_identifier tag i k)))) 
     [@eq_identifier_elim #_ [ %%|%2 %]]
@@ -68 +177 @@
 ]
 qed.
-
+*)
 (*
  whd in match (add ?????); whd in match (add ?????); normalize nodelta