Changeset 1986 for src/Clight


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

Get rid of unused abstraction of Globalenvs.

Location:
src/Clight
Files:
3 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
Note: See TracChangeset for help on using the changeset viewer.