Changeset 1986


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

Get rid of unused abstraction of Globalenvs.

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1874 r1986  
    242242  [ Evar id ⇒
    243243      match (lookup ?? en id) with
    244       [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
     244      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
    245245      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
    246246      ]
     
    357357    ! 〈vf,tr2〉 ← exec_expr ge e m a : IO ???;
    358358    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
    359     ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ? ? ge vf);
     359    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ge vf);
    360360    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
    361361(* requires associativity of IOMonad, so rearrange it below
     
    504504
    505505definition make_global : clight_program → genv ≝
    506 λp. globalenv Genv ?? (fst ??) p.
     506λp. globalenv (fst ??) p.
    507507
    508508let rec make_initial_state (p:clight_program) : res state ≝
    509509  let ge ≝ make_global p in
    510   do m0 ← init_mem Genv ?? (fst ??) p;
    511   do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    512   do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     510  do m0 ← init_mem (fst ??) p;
     511  do b ← opt_to_res ? (msg MainMissing) (find_symbol ge (prog_main ?? p));
     512  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ge b);
    513513  OK ? (Callstate f (nil ?) Kstop m0).
    514514
  • src/Clight/Csem.ma

    r1914 r1986  
    468468  and function pointers to their definitions.  (See module [Globalenvs].) *)
    469469
    470 definition genv ≝ (genv_t Genv) clight_fundef.
     470definition genv ≝ genv_t clight_fundef.
    471471
    472472(* * The local environment maps local variables to block references.
     
    662662  | eval_Evar_global: ∀id,l,ty.
    663663      (* XXX e!id *) lookup ?? e id = None ? →
    664       find_symbol ?? ge id = Some ? l →
     664      find_symbol ge id = Some ? l →
    665665      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
    666666  | eval_Ederef: ∀a,ty,r,l,p,ofs,tr.
     
    10361036      eval_expr ge e m a vf tr1 →
    10371037      eval_exprlist ge e m al vargs tr2 →
    1038       find_funct ?? ge vf = Some ? fd →
     1038      find_funct ge vf = Some ? fd →
    10391039      type_of_fundef fd = fun_typeof a →
    10401040      step ge (State f (Scall (None ?) a al) k e m)
     
    10451045      eval_expr ge e m a vf tr2 →
    10461046      eval_exprlist ge e m al vargs tr3 →
    1047       find_funct ?? ge vf = Some ? fd →
     1047      find_funct ge vf = Some ? fd →
    10481048      type_of_fundef fd = fun_typeof a →
    10491049      step ge (State f (Scall (Some ? lhs) a al) k e m)
     
    12131213inductive initial_state (p: clight_program): state -> Prop :=
    12141214  | initial_state_intro: ∀b,f,ge,m0.
    1215       globalenv Genv ?? (fst ??) p = ge →
    1216       init_mem Genv ?? (fst ??) p = OK ? m0 →
    1217       find_symbol ?? ge (prog_main ?? p) = Some ? b →
    1218       find_funct_ptr ?? ge b = Some ? f →
     1215      globalenv (fst ??) p = ge →
     1216      init_mem (fst ??) p = OK ? m0 →
     1217      find_symbol ge (prog_main ?? p) = Some ? b →
     1218      find_funct_ptr ge b = Some ? f →
    12191219      initial_state p (Callstate f (nil ?) Kstop m0).
    12201220
     
    12311231
    12321232definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    1233   ∀ge. globalenv ??? (fst ??) p = ge →
     1233  ∀ge. globalenv (fst ??) p = ge →
    12341234  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
    12351235 
  • src/Clight/labelSimulation.ma

    r1954 r1986  
    77
    88(* TODO: make something general that can live in common/Globalenvs.ma. *)
    9 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t Genv F) (ge':genv_t Genv F) : Prop ≝ {
     9record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
    1010  rg_find_symbol: ∀s.
    11     find_symbol ?? ge s = find_symbol ?? ge' s;
     11    find_symbol … ge s = find_symbol … ge' s;
    1212  rg_find_funct: ∀v,f.
    13     find_funct ?? ge v = Some ? f →
    14     find_funct ?? ge' v = Some ? (t f);
     13    find_funct ge v = Some ? f →
     14    find_funct ge' v = Some ? (t f);
    1515  rg_find_funct_ptr: ∀b,f.
    16     find_funct_ptr ?? ge b = Some ? f →
    17     find_funct_ptr ?? ge' b = Some ? (t f)
     16    find_funct_ptr ge b = Some ? f →
     17    find_funct_ptr ge' b = Some ? (t f)
    1818}.
    1919
    2020(* FIXME with a more general result *)
    2121axiom transform_program_related : ∀F,V,init,t,p.
    22   related_globals F t (globalenv Genv ? V init p) (globalenv Genv ? V init (transform_program ??? p t)).
     22  related_globals F t (globalenv (λ_.F) V init p) (globalenv (λ_.F) V init (transform_program … p t)).
    2323(*
    2424#F #V #init #t * #vars #fns #main
     
    406406lemma opt_find_funct : ∀ge,ge',m,vf,fd.
    407407  related_globals ? label_fundef ge ge' →
    408   opt_to_io io_out io_in … m (find_funct ?? ge vf) = Value … fd →
    409   opt_to_io io_out io_in … m (find_funct ?? ge' vf) = Value … (label_fundef fd).
     408  opt_to_io io_out io_in … m (find_funct ge vf) = Value … fd →
     409  opt_to_io io_out io_in … m (find_funct ge' vf) = Value … (label_fundef fd).
    410410#ge #ge' #m #vf #fd #RG
    411411lapply (rg_find_funct … RG … vf fd)
     
    11041104(* FIXME: to globalenvs and prove *)
    11051105axiom transform_program_init_mem : ∀A,B,V,p,f,init.
    1106   init_mem Genv ?? init p = init_mem Genv ?? init (transform_program A B V p f).
     1106  init_mem ?? init p = init_mem ?? init (transform_program A B V p f).
    11071107
    11081108
  • src/Cminor/semantics.ma

    r1878 r1986  
    99
    1010definition env ≝ identifier_map SymbolTag val.
    11 definition genv ≝ (genv_t Genv) (fundef internal_function).
     11definition genv ≝ genv_t (fundef internal_function).
    1212
    1313definition stmt_inv : internal_function → env → stmt → Prop ≝ λf,en,s.
     
    314314    | St_call dst ef args ⇒ λInv.
    315315        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    316         ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
     316        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ge vf);
    317317        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
    318318        return 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
     
    447447
    448448definition make_global : Cminor_program → genv ≝
    449 λp. globalenv Genv ?? (λx.x) p.
     449λp. globalenv (λx.x) p.
    450450
    451451definition make_initial_state : Cminor_program → res state ≝
    452452λp.
    453453  let ge ≝ make_global p in
    454   do m ← init_mem Genv ?? (λx.x) p;
    455   do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    456   do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     454  do m ← init_mem (λx.x) p;
     455  do b ← opt_to_res ? (msg MainMissing) (find_symbol ge (prog_main ?? p));
     456  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ge b);
    457457  OK ? (Callstate f (nil ?) m SStop).
    458458
     
    461461
    462462definition make_noinit_global : Cminor_noinit_program → genv ≝
    463 λp. globalenv Genv ?? (λx.[Init_space x]) p.
     463λp. globalenv (λx.[Init_space x]) p.
    464464
    465465definition make_initial_noinit_state : Cminor_noinit_program → res state ≝
    466466λp.
    467467  let ge ≝ make_noinit_global p in
    468   do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    469   do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    470   do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     468  do m ← init_mem (λx.[Init_space x]) p;
     469  do b ← opt_to_res ? (msg MainMissing) (find_symbol ge (prog_main ?? p));
     470  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ge b);
    471471  OK ? (Callstate f (nil ?) m SStop).
    472472
  • src/RTLabs/semantics.ma

    r1920 r1986  
    1212include "RTLabs/syntax.ma".
    1313
    14 definition genv ≝ (genv_t Genv) (fundef internal_function).
     14definition genv ≝ genv_t (fundef internal_function).
    1515
    1616record frame : Type[0] ≝
     
    122122      return 〈E0, build_state f fs m' l ?〉
    123123  | St_call_id id args dst l ⇒ λH.
    124       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    125       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     124      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ge id);
     125      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ge b);
    126126      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    127127      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
    128128  | St_call_ptr frs args dst l ⇒ λH.
    129129      ! fv ← reg_retrieve (locals f) frs;
    130       ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
     130      ! fd ← opt_to_res … (msg BadFunction) (find_funct ge fv);
    131131      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    132132      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
     
    221221
    222222definition make_global : RTLabs_program → genv ≝
    223 λp. globalenv Genv ?? (λx.[Init_space x]) p.
     223λp. globalenv (λx.[Init_space x]) p.
    224224
    225225definition make_initial_state : RTLabs_program → res state ≝
    226226λp.
    227227  let ge ≝ make_global p in
    228   do m ← init_mem Genv ?? (λx.[Init_space x]) p;
     228  do m ← init_mem (λx.[Init_space x]) p;
    229229  let main ≝ prog_main ?? p in
    230   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    231   do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
     230  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ge main);
     231  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ge b);
    232232  OK ? (Callstate f (nil ?) (None ?) (nil ?) m).
    233233
     
    249249inductive state_rel : genv → state → state → Prop ≝
    250250| normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m')
    251 | to_call : ∀ge,f,fs,m,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst (f'::fs) m)
     251| to_call : ∀ge,f,fs,m,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst (f'::fs) m)
    252252(*
    253253| tail_call : ∀ge,f,fs,m,fd,args,dst,m'. ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst fs m')
     
    283283  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    284284  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    285   | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
    286   | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     285  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ???) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
     286  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ???) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
    287287(*
    288288  | #id #rs #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
  • 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.