Changeset 125 for C-semantics/Globalenvs.ma

Timestamp:

Sep 24, 2010, 10:31:32 AM (10 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:

• C-semantics/Globalenvs.ma (modified) (6 diffs)

C-semantics/Globalenvs.ma

@@ -66 +66 @@
        a value, which must be a pointer with offset 0. *)
 
-  find_symbol: ∀F: Type. genv_t F → ident → option block;
+  find_symbol: ∀F: Type. genv_t F → ident → option (memory_space × block)(*;
    (* * Return the address of the given global symbol, if any. *)
 
 (* * ** Properties of the operations. *)
-(*
+
   find_funct_inv:
     ∀F: Type. ∀ge: t F. ∀v: val. ∀f: F.
@@ -142 +142 @@
 (* * Commutation properties between program transformations
   and operations over global environments. *)
-*)*)
+*)
   find_funct_ptr_transf:
     ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
@@ -171 +171 @@
     find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
     ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf
-(*
+
 (* * Commutation properties between partial program transformations
   and operations over global environments. *)
@@ -310 +310 @@
 ].
 
+(* Functions are given negative block numbers *)
+
 (* XXX: temporary definition
    NB: only global functions, no global variables *)
@@ -315 +317 @@
   functions: block → option F;
   nextfunction: Z;
-  symbols: ident → option block
+  symbols: ident → option (memory_space × block)
 }.
+(*
+(** The rest of this library is a straightforward implementation of
+  the module signature above. *)
+
+Module Genv: GENV.
+
+Section GENV.
+
+Variable F: Type.                    (* The type of functions *)
+Variable V: Type.                    (* The type of information over variables *)
+
+Record genv : Type := mkgenv {
+  functions: ZMap.t (option F);     (* mapping function ptr → function *)
+  nextfunction: Z;
+  symbols: PTree.t block                (* mapping symbol → block *)
+}.
+
+Definition t := genv.
+*)
+
+ndefinition add_funct : ∀F:Type. (ident × F) → genv F → genv F ≝
+λF,name_fun,g.
+  let b ≝ nextfunction ? g in
+  mk_genv F ((*ZMap.set*) λb'. if eqZb b b' then (Some ? (\snd name_fun)) else (functions ? g b'))
+            (Zpred b)
+            ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]).
+
+ndefinition add_symbol : ∀F:Type. ident → memory_space → block → genv F → genv F ≝
+λF,name,bsp,b,g.
+  mk_genv F (functions ? g)
+            (nextfunction ? g)
+            ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? 〈bsp,b〉 | inr _ ⇒ symbols ? g i ]).
+(*
+Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
+  ZMap.get b g.(functions).
+
+Definition find_funct (g: genv) (v: val) : option F :=
+  match v with
+  | Vptr b ofs =>
+      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
+  | _ =>
+      None
+  end.
+
+Definition find_symbol ? (g: genv) (symb: ident) : option block :=
+  PTree.get symb g.(symbols).
+
+Lemma find_funct_inv:
+  forall (ge: t) (v: val) (f: F),
+  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
+Proof.
+  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
+  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
+  exists b. congruence.
+  discriminate.
+Qed.
+
+Lemma find_funct_find_funct_ptr:
+  forall (ge: t) (b: block),
+  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b. 
+Proof.
+  intros. simpl. 
+  generalize (Int.eq_spec Int.zero Int.zero).
+  case (Int.eq Int.zero Int.zero); intros.
+  auto. tauto.
+Qed.
+*)
+(* Construct environment and initial memory store *)
+ndefinition empty_mem ≝ empty. (* XXX*)
+ndefinition empty : ∀F. genv F ≝
+  λF. mk_genv F (λ_. None ?) (-1) (λ_. None ?).
+(*  mkgenv (ZMap.init None) (-1) (PTree.empty block).*)
+
+ndefinition add_functs : ∀F:Type. genv F → list (ident × F) → genv F ≝
+λF,init,fns.
+  foldr ?? (add_funct F) init fns.
+
+ndefinition add_globals : ∀F,V:Type.
+       genv F × mem → list (ident × (list init_data) × memory_space × V) →
+       genv F × mem ≝
+λF,V,init,vars.
+  foldr ??
+    (λid_init: ident × (list init_data) × memory_space × V. λg_st: genv F × mem.
+      match id_init with [ mk_pair id_init1 info ⇒
+      match id_init1 with [ mk_pair id_init2 bsp ⇒
+      match id_init2 with [ mk_pair id init ⇒
+      match g_st with [ mk_pair g st ⇒
+        match alloc_init_data st init bsp with [ mk_pair st' b ⇒
+          〈add_symbol ? id bsp b g, st'〉
+        ] ] ] ] ])
+    init vars.
+
+ndefinition globalenv_initmem : ∀F,V:Type. program F V → genv F × mem ≝
+λF,V,p.
+  add_globals F V
+    〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
+    (prog_vars ?? p).
+
+ndefinition globalenv_ : ∀F,V:Type. program F V → genv F ≝
+λF,V,p.
+  \fst (globalenv_initmem F V p).
+ndefinition init_mem_ : ∀F,V:Type. program F V → mem ≝
+λF,V,p.
+  \snd (globalenv_initmem F V p).
 
 ndefinition Genv : GENV ≝ mk_GENV
   genv  (* genv_t *)
-  (λF,V,p. foldr ??
-    (λf,ge. match f with [ mk_pair id def ⇒
-            let b ≝ nextfunction ? ge in
-            mk_genv ? (λb'. if eqZb b b' then Some ? def else (functions ? ge b'))
-                      (Zsucc b)
-                      (λi. match ident_eq id i with [ inl _ ⇒ Some ? b | inr _ ⇒ (symbols ? ge i)])
-            ])
-   (mk_genv ? (λ_.None ?) 0 (λ_.None ?)) (prog_funct ?? p))  (* globalenv *)
-  (λF,V,p. empty)  (* init_mem *)
+  globalenv_
+  init_mem_
   (λF,ge. functions ? ge) (* find_funct_ptr *)
   (λF,ge,v. match v with [ Vptr _ b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
   (λF,ge. symbols ? ge) (* find_symbol *)
+(*  ?
   ?
   ?
   ?
   ?
-  ?
-  ?
+  ?*)
 .
+(*
 ##[ #A B C transf p b f; nelim p; #fns main vars;
     nelim fns;
-    ##[ nnormalize; #H; ndestruct;
+    ##[ nwhd in match globalenv_ in ⊢ %; nwhd in match globalenv_initmem in ⊢ %; nwhd in ⊢ (??%? → ??%?); normalize; #H; ndestruct;
     ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??(??%?)? → ??(??%?)?);
         nrewrite > (?:nextfunction ?? = length ? t);
@@ -443 +543 @@
 ##] nqed.
          
-(*
-(** The rest of this library is a straightforward implementation of
-  the module signature above. *)
-
-Module Genv: GENV.
-
-Section GENV.
-
-Variable F: Type.                    (* The type of functions *)
-Variable V: Type.                    (* The type of information over variables *)
-
-Record genv : Type := mkgenv {
-  functions: ZMap.t (option F);     (* mapping function ptr → function *)
-  nextfunction: Z;
-  symbols: PTree.t block                (* mapping symbol → block *)
-}.
-
-Definition t := genv.
-
-Definition add_funct (name_fun: (ident * F)) (g: genv) : genv :=
-  let b := g.(nextfunction) in
-  mkgenv (ZMap.set b (Some ? (snd name_fun)) g.(functions))
-         (Zpred b)
-         (PTree.set (fst name_fun) b g.(symbols)).
-
-Definition add_symbol (name: ident) (b: block) (g: genv) : genv :=
-  mkgenv g.(functions)
-         g.(nextfunction)
-         (PTree.set name b g.(symbols)).
-
-Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
-  ZMap.get b g.(functions).
-
-Definition find_funct (g: genv) (v: val) : option F :=
-  match v with
-  | Vptr b ofs =>
-      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
-  | _ =>
-      None
-  end.
-
-Definition find_symbol ? (g: genv) (symb: ident) : option block :=
-  PTree.get symb g.(symbols).
-
-Lemma find_funct_inv:
-  forall (ge: t) (v: val) (f: F),
-  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
-Proof.
-  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
-  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
-  exists b. congruence.
-  discriminate.
-Qed.
-
-Lemma find_funct_find_funct_ptr:
-  forall (ge: t) (b: block),
-  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b. 
-Proof.
-  intros. simpl. 
-  generalize (Int.eq_spec Int.zero Int.zero).
-  case (Int.eq Int.zero Int.zero); intros.
-  auto. tauto.
-Qed.
-
-(* Construct environment and initial memory store *)
-
-Definition empty : genv :=
-  mkgenv (ZMap.init None) (-1) (PTree.empty block).
-
-Definition add_functs (init: genv) (fns: list (ident * F)) : genv :=
-  List.fold_right add_funct init fns.
-
-Definition add_globals 
-       (init: genv * mem) (vars: list (ident * list init_data * V))
-       : genv * mem :=
-  List.fold_right
-    (fun (id_init: ident * list init_data * V) (g_st: genv * mem) =>
-       match id_init, g_st with
-       | ((id, init), info), (g, st) =>
-           let (st', b) := Mem.alloc_init_data st init in
-           (add_symbol id b g, st')
-       end)
-    init vars.
-
-Definition globalenv_initmem (p: program F V) : (genv * mem) :=
-  add_globals
-    (add_functs empty p.(prog_funct), Mem.empty)
-    p.(prog_vars).
-
-Definition globalenv (p: program F V) : genv :=
-  fst (globalenv_initmem p).
-Definition init_mem  (p: program F V) : mem :=
-  snd (globalenv_initmem p).
 
 Lemma functions_globalenv: