Changeset 2936 for src

Timestamp:

Mar 21, 2013, 9:45:49 PM (7 years ago)

Author:

campbell

Message:

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

Location:

src

Files:

• Cminor/Cminor_semantics.ma (modified) (1 diff)
• Cminor/toRTLabs.ma (modified) (1 diff)
• RTLabs/RTLabs_semantics.ma (modified) (1 diff)
• RTLabs/RTLabs_syntax.ma (modified) (1 diff)
• compiler.ma (modified) (1 diff)

src/Cminor/Cminor_semantics.ma

@@ -430 +430 @@
   mk_fullexec … Cminor_exec make_global make_initial_state.
 
+(* NB: we've pushed the initialisation code generation later, but here are the
+   semantics for initialisation free Cminor anyway. *)   
+
 definition make_noinit_global : Cminor_noinit_program → genv ≝
 λp. globalenv … (λx.[Init_space x]) p.

src/Cminor/toRTLabs.ma

@@ -939 +939 @@
 qed.
 
-definition cminor_noinit_to_rtlabs : Cminor_noinit_program → RTLabs_program ≝
+definition cminor_to_rtlabs : Cminor_program → RTLabs_program ≝
 λp.transform_program … p (λ_. transf_fundef … c2ra_function).
 
-include "Cminor/initialisation.ma".
-
-definition cminor_to_rtlabs : costlabel → Cminor_program → RTLabs_program ≝
-λinit_cost,p. let p' ≝ replace_init init_cost p in cminor_noinit_to_rtlabs p'.

src/RTLabs/RTLabs_semantics.ma

@@ -205 +205 @@
 
 definition make_global : RTLabs_program → genv ≝
-λp. globalenv … (λx.[Init_space x]) p.
+λp. globalenv … (λx.x) p.
 
 definition make_initial_state : RTLabs_program → res state ≝
 λp.
   let ge ≝ make_global p in
-  do m ← init_mem … (λx.[Init_space x]) p;
+  do m ← init_mem … (λx.x) p;
   let main ≝ prog_main ?? p in
   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);

src/RTLabs/RTLabs_syntax.ma

@@ -92 +92 @@
 }.
 
-(* Note that the global variables will be initialised by the code in main
-   by this stage, so the only initialisation data is the amount of space to
-   allocate. *)
-
-definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
+definition RTLabs_program ≝ program (λ_.fundef internal_function) (list init_data).
 
 

src/compiler.ma

@@ -70 +70 @@
   ! p ← clight_to_cminor p;
   let i ≝ observe cminor_pass p in
-  let p ≝ cminor_to_rtlabs init_cost p in
+  let p ≝ cminor_to_rtlabs p in
   let i ≝ observe rtlabs_pass p in
   if check_cost_program p then