Changeset 2107

Timestamp:

Jun 22, 2012, 2:07:38 PM (7 years ago)

Author:

campbell

Message:

Memory initialisation and program transformations.

Location:

src

Files:

• Clight/labelSimulation.ma (modified) (2 diffs)
• common/Globalenvs.ma (modified) (7 diffs)

src/Clight/labelSimulation.ma

@@ -1065 +1065 @@
 ] qed.
 
-(* FIXME: to globalenvs and prove *)
-axiom transform_program_init_mem : ∀A,B,V,p,f,init.
-  init_mem ?? init p = init_mem ?? init (transform_program A B V p f).
-
 
 lemma initial_state_in_simulation : ∀p,s.
@@ -1086 +1082 @@
 [ whd in ⊢ (??%?);
   change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?);
-  <transform_program_init_mem >Em in ⊢ (??%?);
+  >init_mem_transf >Em in ⊢ (??%?);
   whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
   whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain')

src/common/Globalenvs.ma

@@ -259 +259 @@
 ] qed.
 
-lemma matching_globals_get_same_blocks : ∀A,B,V,W,initV,initW.
+lemma add_globals_match : ∀A,B,V,W,initV,initW.
   ∀P:(ident × region × V) → (ident × region × W) → Prop.
   (∀v,w. P v w → \fst v = \fst w ∧ size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
@@ -265 +265 @@
   symbols ? ge = symbols … ge' →
   All2 … P vars vars' →
-  symbols … (\fst (add_globals A V initV 〈ge,m〉 vars)) = symbols … (\fst (add_globals B W initW 〈ge',m〉 vars')).
+  symbols … (\fst (add_globals A V initV 〈ge,m〉 vars)) = symbols … (\fst (add_globals B W initW 〈ge',m〉 vars')) ∧  
+  \snd (add_globals A V initV 〈ge,m〉 vars) = \snd (add_globals B W initW 〈ge',m〉 vars').
 #A #B #V #W #initV #initW #P #varsOK
 #vars elim vars
-[ #ge #ge' #m * [ #E #_ @E | #h #t #_ * ]
+[ #ge #ge' #m * [ #E #_ % // @E | #h #t #_ * ]
 | * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ]
   * * #id' #r' #w #tl' #E * #p #TL
@@ -277 +278 @@
   cases (varsOK … p) #E1 #E2
   destruct >E2 cases (alloc ????) #m' #b
-  @IH //
+  @IH /2/
   whd in match (add_symbol ????);
   whd in match (add_symbol ????);
@@ -387 +388 @@
   and operations over global environments. *)
 
-  init_mem_transf:
-    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
-    init_mem ?? (transform_program … transf p) = init_mem ?? p;
   find_funct_ptr_rev_transf:
     ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
@@ -615 +613 @@
 change with (add_globals ?????) in match (foldl ?????);
 change with (add_globals ?????) in match (foldl ? (ident×region×V) ???);
-@(matching_globals_get_same_blocks … Mvars)
-[ * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
-| @(matching_fns_get_same_blocks … Mfns) 
+@(proj1 … (add_globals_match … Mvars))
+[ @(matching_fns_get_same_blocks … Mfns) 
   #f #g @match_funct_entry_id
+| * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
 ] qed.
   
@@ -672 +670 @@
 qed.
 
-(* Package up transform_program results nicely. *)
+lemma store_init_data_symbols : ∀A,B,ge,ge',m,b,o,d.
+  symbols A ge = symbols … ge' →
+  store_init_data A ge m b o d = store_init_data B ge' m b o d.
+#A #B #ge #ge' #m #b #o #d #SYM
+whd in ⊢ (??%%);
+cases d #d' try @refl
+#id #n whd in ⊢ (??%%);
+whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl
+qed.
+
+lemma store_init_data_list_symbols : ∀A,B,ge,ge',b.
+  symbols A ge = symbols … ge' →
+  ∀d,m,o. store_init_data_list A ge m b o d = store_init_data_list B ge' m b o d.
+#A #B #ge #ge' #b #SYM #d elim d
+[ //
+| #hd #tl #IH #m #o
+  whd in ⊢ (??%%);
+  >(store_init_data_symbols … SYM)
+  cases (store_init_data ??????) 
+  [ %
+  | #m' @IH
+  ]
+] qed.
+
+lemma init_globals_match : ∀A,B,V,W. ∀P:ident × region × V → ident × region × W → Prop.
+  ∀iV,iW. (∀v,w. P v w → \fst v = \fst w ∧ iV (\snd v) = iW (\snd w)) →
+  ∀ge:genv_t A. ∀ge':genv_t B.
+  symbols … ge = symbols … ge' →
+   ∀m. ∀vars,vars'.
+  All2 … P vars vars' →
+  init_globals A V iV ge m vars = init_globals B W iW ge' m vars'.
+#A #B #V #W #P #iV #iW #varsOK #ge #ge' #SYM #m #vars
+whd in ⊢ (? → ? → ??%%);
+generalize in match (OK ? m);
+elim vars
+[ #rm *
+  [ #_ % 
+  | #h #t *
+  ]
+| * #idr #v #tl #IH #rm
+  * [ * ]
+  * #idr' #w #tl'
+  * #p cases (varsOK … p) #E1 #E2 destruct #TL
+  whd in ⊢ (??%%); cases idr' #id #r cases rm #m'
+  whd in ⊢ (??(????%?)(????%?));
+  [ whd in match (find_symbol ?? id);
+    whd in match (find_symbol B ? id);
+    >SYM cases (lookup ??? id)
+    [ 2: #b whd in ⊢ (??(????%?)(????%?)); >E2 >(store_init_data_list_symbols … SYM) ]
+  ] @IH //
+] qed.
+
+lemma
+  init_mem_match:
+    ∀M:matching.
+    ∀iV,iW. (∀v,w. match_varinfo M v w → iV v = iW w) →
+    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
+    match_program … M p p' →
+    init_mem … iW p' = init_mem … iV p.
+* #A #B #V #W #match_fn #match_var #iV #iW #iSAME #p #p' * #Mvars #Mfns #Mmain
+whd in ⊢ (??%%);
+change with (add_globals ?????) in match (globalenv_allocmem ??? p'); 
+change with (add_globals ?????) in match (globalenv_allocmem ??? p);
+cases (add_globals_match (A ?) (B ?) V W iV iW ?? (prog_vars … p) ??? (prog_vars … p') ? Mvars)
+[ 8: @(matching_fns_get_same_blocks … Mfns)
+     #f0 #g0 * //
+| cases (add_globals ?????) #ge1 #m1
+  cases (add_globals ?????) #ge2 #m2
+  #SYM #MEM destruct @sym_eq @(init_globals_match … Mvars)
+  [ #v0 #w0 * #id #r #v #w /3/
+  | @SYM
+  ]
+| 4: #v0 #w0 * #id #r #v #w #V % // >iSAME //
+| *: skip
+] qed.
+
+lemma
+  init_mem_transf:
+    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
+    init_mem … iV (transform_program … p transf) = init_mem … iV p.
+#A #B #C #iV #transf #p
+@(init_mem_match … (transform_program_match … transf ?))
+//
+qed.
+    
+
+(* Package up transform_program results for global envs nicely. *)
 
 record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
@@ -732 +816 @@
     ∀s: ident.
     find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
-  init_mem_match:
-    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
-           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
-    match_program … match_fun match_var p p' →
-    init_mem ?? p' = init_mem ?? p*)
-
+*)
 (*
 Definition find_funct_ptr ? (g: genv) (b: block) : option F :=