Ignore:
Timestamp:
Sep 20, 2011, 7:11:41 PM (9 years ago)
Author:
campbell
Message:

Change SmallstepExec? so that states can depend on global information.
Use less suggestive names for the transition system so that it's obvious
the global information isn't restricted to Genv.
Separate set up of global environment from initialisation so that it never
fails.
Some minimal changes to get Clight execution working; rest to follow.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r1224 r1231  
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. res (genv_t (F (prog_var_names … p)));
     54  globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. genv_t (F (prog_var_names … p));
    5555   (* * Return the global environment for the given program. *)
    5656
     
    488488       (V → (list init_data)) →
    489489       genv F × mem → list (ident × region × V) →
    490        res (genv F × mem) ≝
     490       (genv F × mem) ≝
    491491λF,V,extract_init,init_env,vars.
    492492  foldl ??
    493     (λg_st: res (genv F × mem). λid_init: ident × region × V.
     493    (λg_st: genv F × mem. λid_init: ident × region × V.
    494494      let 〈id, r, init_info〉 ≝ id_init in
    495495      let init ≝ extract_init init_info in
    496         do 〈g,st〉 ← g_st;
     496      let 〈g,st〉 ≝ g_st in
    497497        match alloc_init_data st init r with [ pair st' b ⇒
    498498          let g' ≝ add_symbol ? id b g in
    499           do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init);
    500             OK ? 〈g', st''〉
     499            〈g', st'〉
    501500        ] )
    502     (OK ? init_env) vars.
    503 
    504 definition globalenv_initmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. res (genv (F (prog_var_names … p)) × mem) ≝
     501    init_env vars.
     502
     503definition init_globals : ∀F,V:Type[0].
     504       (V → (list init_data)) →
     505       genv F → mem → list (ident × region × V) →
     506       res mem ≝
     507λF,V,extract_init,g,m,vars.
     508  foldl ??
     509    (λst: res mem. λid_init: ident × region × V.
     510      let 〈id, r, init_info〉 ≝ id_init in
     511      let init ≝ extract_init init_info in
     512        do st ← st;
     513        match symbols ? g id with
     514        [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init)
     515        | None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *)
     516        ] )
     517    (OK ? m) vars.
     518
     519definition globalenv_allocmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. (genv (F (prog_var_names … p)) × mem) ≝
    505520λF,V,init_info,p.
    506521  add_globals … init_info
     
    508523   (prog_vars ?? p).
    509524
    510 definition globalenv_ : ∀F,V. (V → list init_data) → ∀p:program F V. res (genv (F (prog_var_names … p))) ≝
     525definition globalenv_ : ∀F,V. (V → list init_data) → ∀p:program F V. genv (F (prog_var_names … p)) ≝
    511526λF,V,i,p.
    512   do 〈g,m〉 ← globalenv_initmem F V i p;
    513     OK ? g.
     527  \fst (globalenv_allocmem F V i p).
     528
    514529definition init_mem_ : ∀F,V. (V → list init_data) → program F V → res (mem) ≝
    515530λF,V,i,p.
    516   do 〈g,m〉 ← globalenv_initmem F V i p;
    517     OK ? m.
     531  let 〈g,m〉 ≝ globalenv_allocmem F V i p in
     532  init_globals ? V i g m (prog_vars ?? p).
    518533
    519534
Note: See TracChangeset for help on using the changeset viewer.