Changeset 2936


Ignore:
Timestamp:
Mar 21, 2013, 9:45:49 PM (4 years ago)
Author:
campbell
Message:

Disable initialisation code generation in Cminor, propogate init data
through RTLabs.

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/Cminor_semantics.ma

    r2722 r2936  
    430430  mk_fullexec … Cminor_exec make_global make_initial_state.
    431431
     432(* NB: we've pushed the initialisation code generation later, but here are the
     433   semantics for initialisation free Cminor anyway. *)   
     434
    432435definition make_noinit_global : Cminor_noinit_program → genv ≝
    433436λp. globalenv … (λx.[Init_space x]) p.
  • src/Cminor/toRTLabs.ma

    r2924 r2936  
    939939qed.
    940940
    941 definition cminor_noinit_to_rtlabs : Cminor_noinit_program → RTLabs_program ≝
     941definition cminor_to_rtlabs : Cminor_program → RTLabs_program ≝
    942942λp.transform_program … p (λ_. transf_fundef … c2ra_function).
    943943
    944 include "Cminor/initialisation.ma".
    945 
    946 definition cminor_to_rtlabs : costlabel → Cminor_program → RTLabs_program ≝
    947 λinit_cost,p. let p' ≝ replace_init init_cost p in cminor_noinit_to_rtlabs p'.
  • src/RTLabs/RTLabs_semantics.ma

    r2895 r2936  
    205205
    206206definition make_global : RTLabs_program → genv ≝
    207 λp. globalenv … (λx.[Init_space x]) p.
     207λp. globalenv … (λx.x) p.
    208208
    209209definition make_initial_state : RTLabs_program → res state ≝
    210210λp.
    211211  let ge ≝ make_global p in
    212   do m ← init_mem … (λx.[Init_space x]) p;
     212  do m ← init_mem … (λx.x) p;
    213213  let main ≝ prog_main ?? p in
    214214  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
  • src/RTLabs/RTLabs_syntax.ma

    r2601 r2936  
    9292}.
    9393
    94 (* Note that the global variables will be initialised by the code in main
    95    by this stage, so the only initialisation data is the amount of space to
    96    allocate. *)
    97 
    98 definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
     94definition RTLabs_program ≝ program (λ_.fundef internal_function) (list init_data).
    9995
    10096
  • src/compiler.ma

    r2907 r2936  
    7070  ! p ← clight_to_cminor p;
    7171  let i ≝ observe cminor_pass p in
    72   let p ≝ cminor_to_rtlabs init_cost p in
     72  let p ≝ cminor_to_rtlabs p in
    7373  let i ≝ observe rtlabs_pass p in
    7474  if check_cost_program p then
Note: See TracChangeset for help on using the changeset viewer.