Changeset 1139 for src/Cminor


Ignore:
Timestamp:
Aug 30, 2011, 12:47:18 PM (9 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/Cminor
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r961 r1139  
    4040  〈0, St_skip〉 init).
    4141
    42 definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
     42definition init_vars : list (ident × region × (list init_data)) → stmt ≝
    4343λvars. foldr ??
    44   (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) St_skip vars.
     44  (λvar,s. St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) St_skip vars.
    4545
    4646definition add_statement : ident → stmt →
     
    6464      | inr _ ⇒ 〈id',f'〉 ]).
    6565
    66 definition empty_vars : list (ident × (list init_data) × region × unit) →
    67                         list (ident × (list init_data) × region × unit) ≝
    68 map ?? (λv. 〈〈〈\fst (\fst (\fst v)),
    69                [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉,
    70               \snd (\fst v)〉,
    71               \snd v〉).
     66definition empty_vars : list (ident × region × (list init_data)) →
     67                        list (ident × region × nat) ≝
     68map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉,
     69              size_init_data_list (\snd v)〉).
    7270
    73 definition replace_init : Cminor_program → Cminor_program ≝
     71definition replace_init : Cminor_program → Cminor_noinit_program ≝
    7472λp.
    7573  mk_program ??
  • src/Cminor/semantics.ma

    r961 r1139  
    274274definition make_initial_state : Cminor_program → res (genv × state) ≝
    275275λp.
    276   do ge ← globalenv Genv ?? p;
    277   do m ← init_mem Genv ?? p;
     276  do ge ← globalenv Genv ?? (λx.x) p;
     277  do m ← init_mem Genv ?? (λx.x) p;
    278278  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    279279  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     
    282282definition Cminor_fullexec : fullexec io_out io_in ≝
    283283  mk_fullexec … Cminor_exec ? make_initial_state.
     284
     285definition make_initial_noinit_state : Cminor_noinit_program → res (genv × state) ≝
     286λp.
     287  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     288  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
     289  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
     290  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     291  OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
     292
     293definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
     294  mk_fullexec … Cminor_exec ? make_initial_noinit_state.
  • src/Cminor/syntax.ma

    r961 r1139  
    4141}.
    4242
    43 definition Cminor_program ≝ program (fundef internal_function) unit.
     43definition Cminor_program ≝ program (fundef internal_function) (list init_data).
     44
     45definition Cminor_noinit_program ≝ program (fundef internal_function) nat.
  • src/Cminor/toRTLabs.ma

    r1072 r1139  
    295295qed.
    296296
    297 definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
     297definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
    298298transform_partial_program ???
    299299  (transf_partial_fundef ?? c2ra_function).
     
    301301include "Cminor/initialisation.ma".
    302302
    303 definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
    304 λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
     303definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
     304λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracChangeset for help on using the changeset viewer.