Changeset 1986 for src/common


Ignore:
Timestamp:
May 24, 2012, 9:35:08 AM (8 years ago)
Author:
campbell
Message:

Get rid of unused abstraction of Globalenvs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r1874 r1986  
    3939include "common/Mem.ma".
    4040
    41 (* FIXME: unimplemented stuff in AST.ma
    42 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];
    5141   (* * The type of global environments.  The parameter [F] is the type
    5242       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 *)
     44record genv_t (F:Type[0]) : Type[0] ≝ {
     45  functions: block → option F;
     46  nextfunction: Z;
     47  symbols: ident → option block
     48}.
     49
     50definition 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
     58definition 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 *)
     65definition empty_mem ≝ empty. (* XXX*)
     66definition empty : ∀F. genv_t F ≝
     67  λF. mk_genv_t F (λ_. None ?) (-2) (λ_. None ?).
     68(*  mkgenv (ZMap.init None) (-2) (PTree.empty block).*)
     69
     70definition 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
     76definition 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  ].
     100cases b //
     101qed.
     102
     103definition 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
     114let 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
     126definition 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
     130nremark 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##]
     147qed.
     148*)
     149
     150(* TODO: why doesn't this use alloc? *)
     151definition 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
     163axiom InitDataStoreFailed : String.
     164
     165definition 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
     181definition 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
     197definition 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. *)
     204definition 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. *)
     209definition 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. *)
     215definition 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. *)
     220definition 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. *)
     224definition find_symbol: ∀F: Type[0]. genv_t F → ident → option block ≝
     225λF,ge. symbols ? ge.
     226
     227
     228lemma 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(*
    71244(* * ** Properties of the operations. *)
    72245
     
    301474    match_program … match_fun match_var p p' →
    302475    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
    354477(*
    355478Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
     
    387510Qed.
    388511*)
    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 representing
    404      addresses of the memory region in question - here there are no real
    405      pointers, so use the real region. *)
    406   let ptr ≝ mk_pointer (block_region ? m b) b ? (mk_offset p) in
    407   match id with
    408   [ 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 with
    415       [ None ⇒ None ?
    416       | Some b' ⇒
    417         match pointer_compat_dec b' r' with
    418         [ 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 ? m
    423   | 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 with
    430   [ Init_int8 _ ⇒ 1
    431   | Init_int16 _ ⇒ 2
    432   | Init_int32 _ ⇒ 4
    433   | Init_float32 _ ⇒ 4
    434   | Init_float64 _ ⇒ 8
    435   | Init_space n ⇒ max n 0
    436   | Init_null r ⇒ size_pointer r
    437   | 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 with
    443   [ nil ⇒ Some ? m
    444   | cons id idl' ⇒
    445       match store_init_data F ge m b p id with
    446       [ 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 arithmetic
    455 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 Hdisc
    467       ##[#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) in
    479   〈mk_mem ? (update_block ? b
    480                  (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 in
    498       let init ≝ extract_init init_info in
    499       let 〈g,st〉 ≝ g_st in
    500         let 〈st',b〉 ≝ alloc_init_data st init r in
    501           let g' ≝ add_symbol ? id b g in
    502             〈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 in
    514       let init ≝ extract_init init_info in
    515         do st ← st;
    516         match symbols ? g id with
    517         [ 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_info
    525    〈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 in
    535   init_globals ? V i g m (prog_vars ?? p).
    536 
    537 
    538 
    539 
    540 definition Genv : GENV ≝ mk_GENV
    541   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; destruct
    560 | #sz #i #f #E normalize in E; destruct
    561 | #f #fn #E normalize in E; destruct
    562 | #r #f #E normalize in E; destruct
    563 | * #pty #b #c * #off #f #E normalize in E;
    564   cases off in E ⊢ %; [ 2,3: #x ]
    565   #E normalize in E; destruct
    566   %{pty} %{b} %{c} % // @E
    567 ] qed.
    568512
    569513(*
Note: See TracChangeset for help on using the changeset viewer.