Changeset 1139 for src/common


Ignore:
Timestamp:
Aug 30, 2011, 12:47:18 PM (8 years ago)
Author:
campbell
Message:

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1064 r1139  
    282282  prog_funct: list (ident × F);
    283283  prog_main: ident;
    284   prog_vars: list (ident × (list init_data) × region × V)
     284  prog_vars: list (ident × region × V)
    285285}.
    286286
     
    290290
    291291definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
    292   map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
     292  map ?? (λx: ident × region × V. (\fst (\fst x))) (prog_vars ?? p).
    293293
    294294(* * * Generic transformations over programs *)
  • src/common/Globalenvs.ma

    r961 r1139  
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V: Type[0]. program F V → res (genv_t F);
     54  globalenv: ∀F,V: Type[0]. (V → list init_data) → program F V → res (genv_t F);
    5555   (* * Return the global environment for the given program. *)
    5656
    57   init_mem: ∀F,V: Type[0]. program F V → res mem;
     57  init_mem: ∀F,V: Type[0]. (V → list init_data) → program F V → res mem;
    5858   (* * Return the initial memory state for the given program. *)
    5959
     
    486486
    487487definition add_globals : ∀F,V:Type[0].
    488        genv F × mem → list (ident × (list init_data) × region × V) →
     488       (V → (list init_data)) →
     489       genv F × mem → list (ident × region × V) →
    489490       res (genv F × mem) ≝
    490 λF,V,init_env,vars.
     491λF,V,extract_init,init_env,vars.
    491492  foldl ??
    492     (λg_st: res (genv F × mem). λid_init: ident × (list init_data) × region × V.
    493       match id_init with [ pair id_init1 info ⇒
    494       match id_init1 with [ pair id_init2 r ⇒
    495       match id_init2 with [ pair id init ⇒
     493    (λg_st: res (genv F × mem). λid_init: ident × region × V.
     494      let 〈id, r, init_info〉 ≝ id_init in
     495      let init ≝ extract_init init_info in
    496496        do 〈g,st〉 ← g_st;
    497497        match alloc_init_data st init r with [ pair st' b ⇒
     
    499499          do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init);
    500500            OK ? 〈g', st''〉
    501         ] ] ] ])
     501        ] )
    502502    (OK ? init_env) vars.
    503503
    504 definition globalenv_initmem : ∀F,V:Type[0]. program F V → res (genv F × mem) ≝
    505 λF,V,p.
    506   add_globals F V
    507    〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
     504definition globalenv_initmem : ∀F,V:Type[0]. (V → (list init_data)) → program F V → res (genv F × mem) ≝
     505λF,V,init_info,p.
     506  add_globals F V init_info
     507   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
    508508   (prog_vars ?? p).
    509509
    510 definition globalenv_ : ∀F,V:Type[0]. program F V → res (genv F) ≝
    511 λF,V,p.
    512   do 〈g,m〉 ← globalenv_initmem F V p;
     510definition globalenv_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (genv F) ≝
     511λF,V,i,p.
     512  do 〈g,m〉 ← globalenv_initmem F V i p;
    513513    OK ? g.
    514 definition init_mem_ : ∀F,V:Type[0]. program F V → res (mem) ≝
    515 λF,V,p.
    516   do 〈g,m〉 ← globalenv_initmem F V p;
     514definition init_mem_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (mem) ≝
     515λF,V,i,p.
     516  do 〈g,m〉 ← globalenv_initmem F V i p;
    517517    OK ? m.
    518518
Note: See TracChangeset for help on using the changeset viewer.