Ignore:
Timestamp:
Sep 24, 2010, 10:31:32 AM (9 years ago)
Author:
campbell
Message:

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Globalenvs.ma

    r124 r125  
    6666       a value, which must be a pointer with offset 0. *)
    6767
    68   find_symbol: ∀F: Type. genv_t F → ident → option block;
     68  find_symbol: ∀F: Type. genv_t F → ident → option (memory_space × block)(*;
    6969   (* * Return the address of the given global symbol, if any. *)
    7070
    7171(* * ** Properties of the operations. *)
    72 (*
     72
    7373  find_funct_inv:
    7474    ∀F: Type. ∀ge: t F. ∀v: val. ∀f: F.
     
    142142(* * Commutation properties between program transformations
    143143  and operations over global environments. *)
    144 *)*)
     144*)
    145145  find_funct_ptr_transf:
    146146    ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
     
    171171    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
    172172    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf
    173 (*
     173
    174174(* * Commutation properties between partial program transformations
    175175  and operations over global environments. *)
     
    310310].
    311311
     312(* Functions are given negative block numbers *)
     313
    312314(* XXX: temporary definition
    313315   NB: only global functions, no global variables *)
     
    315317  functions: block → option F;
    316318  nextfunction: Z;
    317   symbols: ident → option block
     319  symbols: ident → option (memory_space × block)
    318320}.
     321(*
     322(** The rest of this library is a straightforward implementation of
     323  the module signature above. *)
     324
     325Module Genv: GENV.
     326
     327Section GENV.
     328
     329Variable F: Type.                    (* The type of functions *)
     330Variable V: Type.                    (* The type of information over variables *)
     331
     332Record 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
     338Definition t := genv.
     339*)
     340
     341ndefinition add_funct : ∀F:Type. (ident × F) → genv F → genv F ≝
     342λF,name_fun,g.
     343  let b ≝ nextfunction ? g in
     344  mk_genv F ((*ZMap.set*) λb'. if eqZb b b' then (Some ? (\snd name_fun)) else (functions ? g b'))
     345            (Zpred b)
     346            ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]).
     347
     348ndefinition add_symbol : ∀F:Type. ident → memory_space → block → genv F → genv F ≝
     349λF,name,bsp,b,g.
     350  mk_genv F (functions ? g)
     351            (nextfunction ? g)
     352            ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? 〈bsp,b〉 | inr _ ⇒ symbols ? g i ]).
     353(*
     354Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
     355  ZMap.get b g.(functions).
     356
     357Definition find_funct (g: genv) (v: val) : option F :=
     358  match v with
     359  | Vptr b ofs =>
     360      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
     361  | _ =>
     362      None
     363  end.
     364
     365Definition find_symbol ? (g: genv) (symb: ident) : option block :=
     366  PTree.get symb g.(symbols).
     367
     368Lemma find_funct_inv:
     369  forall (ge: t) (v: val) (f: F),
     370  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
     371Proof.
     372  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
     373  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
     374  exists b. congruence.
     375  discriminate.
     376Qed.
     377
     378Lemma find_funct_find_funct_ptr:
     379  forall (ge: t) (b: block),
     380  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
     381Proof.
     382  intros. simpl.
     383  generalize (Int.eq_spec Int.zero Int.zero).
     384  case (Int.eq Int.zero Int.zero); intros.
     385  auto. tauto.
     386Qed.
     387*)
     388(* Construct environment and initial memory store *)
     389ndefinition empty_mem ≝ empty. (* XXX*)
     390ndefinition empty : ∀F. genv F ≝
     391  λF. mk_genv F (λ_. None ?) (-1) (λ_. None ?).
     392(*  mkgenv (ZMap.init None) (-1) (PTree.empty block).*)
     393
     394ndefinition add_functs : ∀F:Type. genv F → list (ident × F) → genv F ≝
     395λF,init,fns.
     396  foldr ?? (add_funct F) init fns.
     397
     398ndefinition add_globals : ∀F,V:Type.
     399       genv F × mem → list (ident × (list init_data) × memory_space × V) →
     400       genv F × mem ≝
     401λF,V,init,vars.
     402  foldr ??
     403    (λid_init: ident × (list init_data) × memory_space × V. λg_st: genv F × mem.
     404      match id_init with [ mk_pair id_init1 info ⇒
     405      match id_init1 with [ mk_pair id_init2 bsp ⇒
     406      match id_init2 with [ mk_pair id init ⇒
     407      match g_st with [ mk_pair g st ⇒
     408        match alloc_init_data st init bsp with [ mk_pair st' b ⇒
     409          〈add_symbol ? id bsp b g, st'〉
     410        ] ] ] ] ])
     411    init vars.
     412
     413ndefinition globalenv_initmem : ∀F,V:Type. program F V → genv F × mem ≝
     414λF,V,p.
     415  add_globals F V
     416    〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
     417    (prog_vars ?? p).
     418
     419ndefinition globalenv_ : ∀F,V:Type. program F V → genv F ≝
     420λF,V,p.
     421  \fst (globalenv_initmem F V p).
     422ndefinition init_mem_ : ∀F,V:Type. program F V → mem ≝
     423λF,V,p.
     424  \snd (globalenv_initmem F V p).
    319425
    320426ndefinition Genv : GENV ≝ mk_GENV
    321427  genv  (* genv_t *)
    322   (λF,V,p. foldr ??
    323     (λf,ge. match f with [ mk_pair id def ⇒
    324             let b ≝ nextfunction ? ge in
    325             mk_genv ? (λb'. if eqZb b b' then Some ? def else (functions ? ge b'))
    326                       (Zsucc b)
    327                       (λi. match ident_eq id i with [ inl _ ⇒ Some ? b | inr _ ⇒ (symbols ? ge i)])
    328             ])
    329    (mk_genv ? (λ_.None ?) 0 (λ_.None ?)) (prog_funct ?? p))  (* globalenv *)
    330   (λF,V,p. empty)  (* init_mem *)
     428  globalenv_
     429  init_mem_
    331430  (λF,ge. functions ? ge) (* find_funct_ptr *)
    332431  (λF,ge,v. match v with [ Vptr _ b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
    333432  (λF,ge. symbols ? ge) (* find_symbol *)
     433(*  ?
    334434  ?
    335435  ?
    336436  ?
    337437  ?
    338   ?
    339   ?
     438  ?*)
    340439.
     440(*
    341441##[ #A B C transf p b f; nelim p; #fns main vars;
    342442    nelim fns;
    343     ##[ nnormalize; #H; ndestruct;
     443    ##[ nwhd in match globalenv_ in ⊢ %; nwhd in match globalenv_initmem in ⊢ %; nwhd in ⊢ (??%? → ??%?); normalize; #H; ndestruct;
    344444    ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??(??%?)? → ??(??%?)?);
    345445        nrewrite > (?:nextfunction ?? = length ? t);
     
    443543##] nqed.
    444544         
    445 (*
    446 (** The rest of this library is a straightforward implementation of
    447   the module signature above. *)
    448 
    449 Module Genv: GENV.
    450 
    451 Section GENV.
    452 
    453 Variable F: Type.                    (* The type of functions *)
    454 Variable V: Type.                    (* The type of information over variables *)
    455 
    456 Record genv : Type := mkgenv {
    457   functions: ZMap.t (option F);     (* mapping function ptr → function *)
    458   nextfunction: Z;
    459   symbols: PTree.t block                (* mapping symbol → block *)
    460 }.
    461 
    462 Definition t := genv.
    463 
    464 Definition add_funct (name_fun: (ident * F)) (g: genv) : genv :=
    465   let b := g.(nextfunction) in
    466   mkgenv (ZMap.set b (Some ? (snd name_fun)) g.(functions))
    467          (Zpred b)
    468          (PTree.set (fst name_fun) b g.(symbols)).
    469 
    470 Definition add_symbol (name: ident) (b: block) (g: genv) : genv :=
    471   mkgenv g.(functions)
    472          g.(nextfunction)
    473          (PTree.set name b g.(symbols)).
    474 
    475 Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
    476   ZMap.get b g.(functions).
    477 
    478 Definition find_funct (g: genv) (v: val) : option F :=
    479   match v with
    480   | Vptr b ofs =>
    481       if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
    482   | _ =>
    483       None
    484   end.
    485 
    486 Definition find_symbol ? (g: genv) (symb: ident) : option block :=
    487   PTree.get symb g.(symbols).
    488 
    489 Lemma find_funct_inv:
    490   forall (ge: t) (v: val) (f: F),
    491   find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
    492 Proof.
    493   intros until f. unfold find_funct. destruct v; try (intros; discriminate).
    494   generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
    495   exists b. congruence.
    496   discriminate.
    497 Qed.
    498 
    499 Lemma find_funct_find_funct_ptr:
    500   forall (ge: t) (b: block),
    501   find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
    502 Proof.
    503   intros. simpl.
    504   generalize (Int.eq_spec Int.zero Int.zero).
    505   case (Int.eq Int.zero Int.zero); intros.
    506   auto. tauto.
    507 Qed.
    508 
    509 (* Construct environment and initial memory store *)
    510 
    511 Definition empty : genv :=
    512   mkgenv (ZMap.init None) (-1) (PTree.empty block).
    513 
    514 Definition add_functs (init: genv) (fns: list (ident * F)) : genv :=
    515   List.fold_right add_funct init fns.
    516 
    517 Definition add_globals
    518        (init: genv * mem) (vars: list (ident * list init_data * V))
    519        : genv * mem :=
    520   List.fold_right
    521     (fun (id_init: ident * list init_data * V) (g_st: genv * mem) =>
    522        match id_init, g_st with
    523        | ((id, init), info), (g, st) =>
    524            let (st', b) := Mem.alloc_init_data st init in
    525            (add_symbol id b g, st')
    526        end)
    527     init vars.
    528 
    529 Definition globalenv_initmem (p: program F V) : (genv * mem) :=
    530   add_globals
    531     (add_functs empty p.(prog_funct), Mem.empty)
    532     p.(prog_vars).
    533 
    534 Definition globalenv (p: program F V) : genv :=
    535   fst (globalenv_initmem p).
    536 Definition init_mem  (p: program F V) : mem :=
    537   snd (globalenv_initmem p).
    538545
    539546Lemma functions_globalenv:
Note: See TracChangeset for help on using the changeset viewer.