Changeset 1986 for src/common/Globalenvs.ma
 Timestamp:
 May 24, 2012, 9:35:08 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Globalenvs.ma
r1874 r1986 39 39 include "common/Mem.ma". 40 40 41 (* FIXME: unimplemented stuff in AST.ma42 axiom transform_partial_program: ∀A,B,V:Type[0]. (A → res B) → program A V → res (program B V).43 axiom transform_partial_program2: ∀A,B,V,W:Type[0]. (A → res B) → (V → res W) → program A V → res (program B W).44 axiom match_program: ∀A,B,V,W:Type[0]. program A V → program B W → Prop.45 *)46 47 record GENV : Type[2] ≝ {48 (* * ** Types and operations *)49 50 genv_t : Type[0] → Type[0];51 41 (* * The type of global environments. The parameter [F] is the type 52 42 of function descriptions. *) 53 54 globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. genv_t (F (prog_var_names … p)); 55 (* * Return the global environment for the given program. *) 56 57 init_mem: ∀F,V. (V → list init_data) → program F V → res mem; 58 (* * Return the initial memory state for the given program. *) 59 60 find_funct_ptr: ∀F: Type[0]. genv_t F → block → option F; 61 (* * Return the function description associated with the given address, 62 if any. *) 63 64 find_funct: ∀F: Type[0]. genv_t F → val → option F; 65 (* * Same as [find_funct_ptr] but the function address is given as 66 a value, which must be a pointer with offset 0. *) 67 68 find_symbol: ∀F: Type[0]. genv_t F → ident → option block (*; 69 (* * Return the address of the given global symbol, if any. *) 70 43 (* Functions are given negative block numbers *) 44 record genv_t (F:Type[0]) : Type[0] ≝ { 45 functions: block → option F; 46 nextfunction: Z; 47 symbols: ident → option block 48 }. 49 50 definition add_funct : ∀F:Type[0]. (ident × F) → genv_t F → genv_t F ≝ 51 λF,name_fun,g. 52 let blk_id ≝ nextfunction ? g in 53 let b ≝ mk_block Code blk_id in 54 mk_genv_t F ((*ZMap.set*) λb'. if eq_block b b' then (Some ? (\snd name_fun)) else (functions ? g b')) 55 (Zpred blk_id) 56 ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? b  inr _ ⇒ (symbols ? g i) ]). 57 58 definition add_symbol : ∀F:Type[0]. ident → block → genv_t F → genv_t F ≝ 59 λF,name,b,g. 60 mk_genv_t F (functions ? g) 61 (nextfunction ? g) 62 ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? b  inr _ ⇒ symbols ? g i ]). 63 64 (* Construct environment and initial memory store *) 65 definition empty_mem ≝ empty. (* XXX*) 66 definition empty : ∀F. genv_t F ≝ 67 λF. mk_genv_t F (λ_. None ?) (2) (λ_. None ?). 68 (* mkgenv (ZMap.init None) (2) (PTree.empty block).*) 69 70 definition add_functs : ∀F:Type[0]. genv_t F → list (ident × F) → genv_t F ≝ 71 λF,init,fns. 72 foldr ?? (add_funct F) init fns. 73 74 (* init *) 75 76 definition store_init_data : ∀F.genv_t F → mem → block → Z → init_data → option mem ≝ 77 λF,ge,m,b,p,id. 78 (* store checks that the address came from something capable of representing 79 addresses of the memory region in question  here there are no real 80 pointers, so use the real region. *) 81 let ptr ≝ mk_pointer (block_region ? m b) b ? (mk_offset p) in 82 match id with 83 [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n) 84  Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n) 85  Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n) 86  Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n) 87  Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n) 88  Init_addrof r' symb ofs ⇒ 89 match (*find_symbol ge symb*) symbols ? ge symb with 90 [ None ⇒ None ? 91  Some b' ⇒ 92 match pointer_compat_dec b' r' with 93 [ inl pc ⇒ store (ASTptr r') m ptr (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs)))) 94  inr _ ⇒ None ? 95 ] 96 ] 97  Init_space n ⇒ Some ? m 98  Init_null r' ⇒ store (ASTptr r') m ptr (Vnull r') 99 ]. 100 cases b // 101 qed. 102 103 definition size_init_data : init_data → nat ≝ 104 λi_data.match i_data with 105 [ Init_int8 _ ⇒ 1 106  Init_int16 _ ⇒ 2 107  Init_int32 _ ⇒ 4 108  Init_float32 _ ⇒ 4 109  Init_float64 _ ⇒ 8 110  Init_space n ⇒ max n 0 111  Init_null r ⇒ size_pointer r 112  Init_addrof r _ _ ⇒ size_pointer r]. 113 114 let rec store_init_data_list (F:Type[0]) (ge:genv_t F) 115 (m: mem) (b: block) (p: Z) (idl: list init_data) 116 on idl : option mem ≝ 117 match idl with 118 [ nil ⇒ Some ? m 119  cons id idl' ⇒ 120 match store_init_data F ge m b p id with 121 [ None ⇒ None ? 122  Some m' ⇒ store_init_data_list F ge m' b (p + size_init_data id) idl' 123 ] 124 ]. 125 126 definition size_init_data_list : list init_data → nat ≝ 127 λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O i_data. 128 129 (* Nonessential properties that may require arithmetic 130 nremark size_init_data_list_pos: 131 ∀i_data. OZ ≤ size_init_data_list i_data. 132 #i_data;elim i_data;//; 133 #a;#tl;cut (OZ ≤ size_init_data a) 134 ##[cases a;normalize;//; 135 #x;cases x;normalize;//; 136 ###Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl)); 137 cut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m) 138 ##[cases (size_init_data a) in Hsize IH; 139 ##[##1,2:/3/ 140 ##normalize;#n;#Hfalse;elim Hfalse] 141 ###Hdisc;cases Hdisc 142 ##[#Heq;nrewrite > Heq;//; 143 ###Heq;cases Heq;#x;#Heq2;nrewrite > Heq2; 144 (* TODO: arithmetics *) napply daemon] 145 ##] 146 ##] 147 qed. 148 *) 149 150 (* TODO: why doesn't this use alloc? *) 151 definition alloc_init_data : mem → list init_data → region → mem × block ≝ 152 λm,i_data,r. 153 let b ≝ mk_block r (nextblock ? m) in 154 〈mk_mem ? (update_block ? b 155 (mk_block_contents becontentT OZ (size_init_data_list i_data) (λ_.BVundef)) 156 (blocks ? m)) 157 (Zsucc (nextblock ? m)) 158 (succ_nextblock_pos ? m), 159 b〉. 160 161 (* init *) 162 163 axiom InitDataStoreFailed : String. 164 165 definition add_globals : ∀F,V:Type[0]. 166 (V → (list init_data)) → 167 genv_t F × mem → list (ident × region × V) → 168 (genv_t F × mem) ≝ 169 λF,V,extract_init,init_env,vars. 170 foldl ?? 171 (λg_st: genv_t F × mem. λid_init: ident × region × V. 172 let 〈id, r, init_info〉 ≝ id_init in 173 let init ≝ extract_init init_info in 174 let 〈g,st〉 ≝ g_st in 175 let 〈st',b〉 ≝ alloc_init_data st init r in 176 let g' ≝ add_symbol ? id b g in 177 〈g', st'〉 178 ) 179 init_env vars. 180 181 definition init_globals : ∀F,V:Type[0]. 182 (V → (list init_data)) → 183 genv_t F → mem → list (ident × region × V) → 184 res mem ≝ 185 λF,V,extract_init,g,m,vars. 186 foldl ?? 187 (λst: res mem. λid_init: ident × region × V. 188 let 〈id, r, init_info〉 ≝ id_init in 189 let init ≝ extract_init init_info in 190 do st ← st; 191 match symbols ? g id with 192 [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init) 193  None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *) 194 ] ) 195 (OK ? m) vars. 196 197 definition globalenv_allocmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. (genv_t (F (prog_var_names … p)) × mem) ≝ 198 λF,V,init_info,p. 199 add_globals … init_info 200 〈add_functs ? (empty …) (prog_funct F ? p), empty_mem ?〉 201 (prog_vars ?? p). 202 203 (* Return the global environment for the given program. *) 204 definition globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. genv_t (F (prog_var_names … p)) ≝ 205 λF,V,i,p. 206 \fst (globalenv_allocmem F V i p). 207 208 (* Return the initial memory state for the given program. *) 209 definition init_mem: ∀F,V. (V → list init_data) → program F V → res mem ≝ 210 λF,V,i,p. 211 let 〈g,m〉 ≝ globalenv_allocmem F V i p in 212 init_globals ? V i g m (prog_vars ?? p). 213 214 (* Return the function description associated with the given address, if any. *) 215 definition find_funct_ptr: ∀F: Type[0]. genv_t F → block → option F ≝ 216 λF,ge. functions ? ge. 217 218 (* Same as [find_funct_ptr] but the function address is given as 219 a value, which must be a pointer with offset 0. *) 220 definition find_funct: ∀F: Type[0]. genv_t F → val → option F ≝ 221 λF,ge,v. match v with [ Vptr ptr ⇒ if eq_offset (poff ptr) zero_offset then functions ? ge (pblock ptr) else None ?  _ ⇒ None ? ]. 222 223 (* Return the address of the given global symbol, if any. *) 224 definition find_symbol: ∀F: Type[0]. genv_t F → ident → option block ≝ 225 λF,ge. symbols ? ge. 226 227 228 lemma find_funct_find_funct_ptr : ∀F,ge,v,f. 229 find_funct F ge v = Some F f → 230 ∃pty,b,c. v = Vptr (mk_pointer pty b c zero_offset) ∧ find_funct_ptr F ge b = Some F f. 231 #F #ge * 232 [ #f #E normalize in E; destruct 233  #sz #i #f #E normalize in E; destruct 234  #f #fn #E normalize in E; destruct 235  #r #f #E normalize in E; destruct 236  * #pty #b #c * #off #f #E normalize in E; 237 cases off in E ⊢ %; [ 2,3: #x ] 238 #E normalize in E; destruct 239 %{pty} %{b} %{c} % // @E 240 ] qed. 241 242 243 (* 71 244 (* * ** Properties of the operations. *) 72 245 … … 301 474 match_program … match_fun match_var p p' → 302 475 init_mem ?? p' = init_mem ?? p*)*) 303 }. 304 305 306 let rec foldl (A,B:Type[0]) (f:A → B → A) (a:A) (l:list B) on l : A ≝ 307 match l with 308 [ nil ⇒ a 309  cons h t ⇒ foldl A B f (f a h) t 310 ]. 311 312 (* Functions are given negative block numbers *) 313 314 (* XXX: temporary definition 315 NB: only global functions, no global variables *) 316 record genv (F:Type[0]) : Type[0] ≝ { 317 functions: block → option F; 318 nextfunction: Z; 319 symbols: ident → option block 320 }. 321 (* 322 (** The rest of this library is a straightforward implementation of 323 the module signature above. *) 324 325 Module Genv: GENV. 326 327 Section GENV. 328 329 Variable F: Type[0]. (* The type of functions *) 330 Variable V: Type. (* The type of information over variables *) 331 332 Record genv : Type := mkgenv { 333 functions: ZMap.t (option F); (* mapping function ptr → function *) 334 nextfunction: Z; 335 symbols: PTree.t block (* mapping symbol → block *) 336 }. 337 338 Definition t := genv. 339 *) 340 341 definition add_funct : ∀F:Type[0]. (ident × F) → genv F → genv F ≝ 342 λF,name_fun,g. 343 let blk_id ≝ nextfunction ? g in 344 let b ≝ mk_block Code blk_id in 345 mk_genv F ((*ZMap.set*) λb'. if eq_block b b' then (Some ? (\snd name_fun)) else (functions ? g b')) 346 (Zpred blk_id) 347 ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? b  inr _ ⇒ (symbols ? g i) ]). 348 349 definition add_symbol : ∀F:Type[0]. ident → block → genv F → genv F ≝ 350 λF,name,b,g. 351 mk_genv F (functions ? g) 352 (nextfunction ? g) 353 ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? b  inr _ ⇒ symbols ? g i ]). 476 354 477 (* 355 478 Definition find_funct_ptr ? (g: genv) (b: block) : option F := … … 387 510 Qed. 388 511 *) 389 (* Construct environment and initial memory store *)390 definition empty_mem ≝ empty. (* XXX*)391 definition empty : ∀F. genv F ≝392 λF. mk_genv F (λ_. None ?) (2) (λ_. None ?).393 (* mkgenv (ZMap.init None) (2) (PTree.empty block).*)394 395 definition add_functs : ∀F:Type[0]. genv F → list (ident × F) → genv F ≝396 λF,init,fns.397 foldr ?? (add_funct F) init fns.398 399 (* init *)400 401 definition store_init_data : ∀F.genv F → mem → block → Z → init_data → option mem ≝402 λF,ge,m,b,p,id.403 (* store checks that the address came from something capable of representing404 addresses of the memory region in question  here there are no real405 pointers, so use the real region. *)406 let ptr ≝ mk_pointer (block_region ? m b) b ? (mk_offset p) in407 match id with408 [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)409  Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n)410  Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n)411  Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n)412  Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n)413  Init_addrof r' symb ofs ⇒414 match (*find_symbol ge symb*) symbols ? ge symb with415 [ None ⇒ None ?416  Some b' ⇒417 match pointer_compat_dec b' r' with418 [ inl pc ⇒ store (ASTptr r') m ptr (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))419  inr _ ⇒ None ?420 ]421 ]422  Init_space n ⇒ Some ? m423  Init_null r' ⇒ store (ASTptr r') m ptr (Vnull r')424 ].425 cases b //426 qed.427 428 definition size_init_data : init_data → nat ≝429 λi_data.match i_data with430 [ Init_int8 _ ⇒ 1431  Init_int16 _ ⇒ 2432  Init_int32 _ ⇒ 4433  Init_float32 _ ⇒ 4434  Init_float64 _ ⇒ 8435  Init_space n ⇒ max n 0436  Init_null r ⇒ size_pointer r437  Init_addrof r _ _ ⇒ size_pointer r].438 439 let rec store_init_data_list (F:Type[0]) (ge:genv F)440 (m: mem) (b: block) (p: Z) (idl: list init_data)441 on idl : option mem ≝442 match idl with443 [ nil ⇒ Some ? m444  cons id idl' ⇒445 match store_init_data F ge m b p id with446 [ None ⇒ None ?447  Some m' ⇒ store_init_data_list F ge m' b (p + size_init_data id) idl'448 ]449 ].450 451 definition size_init_data_list : list init_data → nat ≝452 λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O i_data.453 454 (* Nonessential properties that may require arithmetic455 nremark size_init_data_list_pos:456 ∀i_data. OZ ≤ size_init_data_list i_data.457 #i_data;elim i_data;//;458 #a;#tl;cut (OZ ≤ size_init_data a)459 ##[cases a;normalize;//;460 #x;cases x;normalize;//;461 ###Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));462 cut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)463 ##[cases (size_init_data a) in Hsize IH;464 ##[##1,2:/3/465 ##normalize;#n;#Hfalse;elim Hfalse]466 ###Hdisc;cases Hdisc467 ##[#Heq;nrewrite > Heq;//;468 ###Heq;cases Heq;#x;#Heq2;nrewrite > Heq2;469 (* TODO: arithmetics *) napply daemon]470 ##]471 ##]472 qed.473 *)474 475 (* TODO: why doesn't this use alloc? *)476 definition alloc_init_data : mem → list init_data → region → mem × block ≝477 λm,i_data,r.478 let b ≝ mk_block r (nextblock ? m) in479 〈mk_mem ? (update_block ? b480 (mk_block_contents becontentT OZ (size_init_data_list i_data) (λ_.BVundef))481 (blocks ? m))482 (Zsucc (nextblock ? m))483 (succ_nextblock_pos ? m),484 b〉.485 486 (* init *)487 488 axiom InitDataStoreFailed : String.489 490 definition add_globals : ∀F,V:Type[0].491 (V → (list init_data)) →492 genv F × mem → list (ident × region × V) →493 (genv F × mem) ≝494 λF,V,extract_init,init_env,vars.495 foldl ??496 (λg_st: genv F × mem. λid_init: ident × region × V.497 let 〈id, r, init_info〉 ≝ id_init in498 let init ≝ extract_init init_info in499 let 〈g,st〉 ≝ g_st in500 let 〈st',b〉 ≝ alloc_init_data st init r in501 let g' ≝ add_symbol ? id b g in502 〈g', st'〉503 )504 init_env vars.505 506 definition init_globals : ∀F,V:Type[0].507 (V → (list init_data)) →508 genv F → mem → list (ident × region × V) →509 res mem ≝510 λF,V,extract_init,g,m,vars.511 foldl ??512 (λst: res mem. λid_init: ident × region × V.513 let 〈id, r, init_info〉 ≝ id_init in514 let init ≝ extract_init init_info in515 do st ← st;516 match symbols ? g id with517 [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init)518  None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *)519 ] )520 (OK ? m) vars.521 522 definition globalenv_allocmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. (genv (F (prog_var_names … p)) × mem) ≝523 λF,V,init_info,p.524 add_globals … init_info525 〈add_functs ? (empty …) (prog_funct F ? p), empty_mem ?〉526 (prog_vars ?? p).527 528 definition globalenv_ : ∀F,V. (V → list init_data) → ∀p:program F V. genv (F (prog_var_names … p)) ≝529 λF,V,i,p.530 \fst (globalenv_allocmem F V i p).531 532 definition init_mem_ : ∀F,V. (V → list init_data) → program F V → res (mem) ≝533 λF,V,i,p.534 let 〈g,m〉 ≝ globalenv_allocmem F V i p in535 init_globals ? V i g m (prog_vars ?? p).536 537 538 539 540 definition Genv : GENV ≝ mk_GENV541 genv (* genv_t *)542 globalenv_543 init_mem_544 (λF,ge. functions ? ge) (* find_funct_ptr *)545 (λF,ge,v. match v with [ Vptr ptr ⇒ if eq_offset (poff ptr) zero_offset then functions ? ge (pblock ptr) else None ?  _ ⇒ None ? ]) (* find_funct *)546 (λF,ge. symbols ? ge) (* find_symbol *)547 (* ?548 ?549 ?550 ?551 ?552 ?*)553 .554 555 lemma find_funct_find_funct_ptr : ∀F,ge,v,f.556 find_funct Genv F ge v = Some F f →557 ∃pty,b,c. v = Vptr (mk_pointer pty b c zero_offset) ∧ find_funct_ptr Genv F ge b = Some F f.558 #F #ge *559 [ #f #E normalize in E; destruct560  #sz #i #f #E normalize in E; destruct561  #f #fn #E normalize in E; destruct562  #r #f #E normalize in E; destruct563  * #pty #b #c * #off #f #E normalize in E;564 cases off in E ⊢ %; [ 2,3: #x ]565 #E normalize in E; destruct566 %{pty} %{b} %{c} % // @E567 ] qed.568 512 569 513 (*
Note: See TracChangeset
for help on using the changeset viewer.