Changeset 1139

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

Files:

• Clight/Cexec.ma (modified) (1 diff)
• Clight/CexecSound.ma (modified) (1 diff)
• Clight/Csem.ma (modified) (2 diffs)
• Clight/Csyntax.ma (modified) (1 diff)
• Clight/test/insertsort.c.ma (modified) (2 diffs)
• Clight/test/search.c.ma (modified) (1 diff)
• Clight/test/sum.c.ma (modified) (2 diffs)
• Clight/toCminor.ma (modified) (1 diff)
• Cminor/initialisation.ma (modified) (2 diffs)
• Cminor/semantics.ma (modified) (2 diffs)
• Cminor/syntax.ma (modified) (1 diff)
• Cminor/toRTLabs.ma (modified) (2 diffs)
• RTLabs/semantics.ma (modified) (1 diff)
• RTLabs/syntax.ma (modified) (1 diff)
• common/AST.ma (modified) (2 diffs)
• common/Globalenvs.ma (modified) (3 diffs)

src/Clight/Cexec.ma

@@ -534 +534 @@
 
 let rec make_initial_state (p:clight_program) : res (genv × state) ≝
-  do ge ← globalenv Genv ?? p;
-  do m0 ← init_mem Genv ?? p;
+  do ge ← globalenv Genv ?? (fst ??) p;
+  do m0 ← init_mem Genv ?? (fst ??) p;
   do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
   do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);

src/Clight/CexecSound.ma

@@ -533 +533 @@
 qed.
 
-lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
+lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? (fst ??) p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
 #p cases p; #fns #main #vars
 whd in ⊢ (???%);

src/Clight/Csem.ma

@@ -1511 +1511 @@
 inductive initial_state (p: clight_program): state -> Prop :=
   | initial_state_intro: ∀b,f,ge,m0.
-      globalenv Genv ?? p = OK ? ge →
-      init_mem Genv ?? p = OK ? m0 →
+      globalenv Genv ?? (fst ??) p = OK ? ge →
+      init_mem Genv ?? (fst ??) p = OK ? m0 →
       find_symbol ?? ge (prog_main ?? p) = Some ? b →
       find_funct_ptr ?? ge b = Some ? f →
@@ -1529 +1529 @@
 
 definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
-  ∀ge. globalenv ??? p = OK ? ge →
+  ∀ge. globalenv ??? (fst ??) p = OK ? ge →
   program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
 (*

src/Clight/Csyntax.ma

@@ -318 +318 @@
   data.  See module [AST] for more details. *)
 
-definition clight_program : Type[0] ≝ program clight_fundef type.
+definition clight_program : Type[0] ≝ program clight_fundef (list init_data × type).
 
 (* * * Operations over types *)

src/Clight/test/insertsort.c.ma

@@ -5 +5 @@
    generate Init_null at the moment. *)
 
-definition myprog := mk_program clight_fundef type
+definition myprog := mk_program clight_fundef ((list init_data) × type)
   [〈ident_of_nat 0 (* insert *), CL_Internal (
      mk_function Tvoid [〈ident_of_nat 2, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ]
@@ -167 +167 @@
   )〉]
   (ident_of_nat 12)
-  [〈〈〈ident_of_nat 15 (* l6 *),
-     [(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ]〉,
-     Any〉,
-     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 16 (* l5 *),
-    [(Init_int8 (repr I8 36)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 15) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 17 (* l4 *),
-    [(Init_int8 (repr I8 136)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 16) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 18 (* l3 *),
-    [(Init_int8 (repr I8 105)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 17) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 19 (* l2 *),
-    [(Init_int8 (repr I8 234)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 18) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 20 (* l1 *),
-    [(Init_int8 (repr I8 240)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 19) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 14 (* l0 *),
-    [(Init_int8 (repr I8 102)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 20) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉]
+  [〈〈ident_of_nat 15 (* l6 *), Any〉,
+    〈[(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ], 
+     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 16 (* l5 *), Any〉,
+    〈[(Init_int8 (repr I8 36)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 15) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 17 (* l4 *), Any〉,
+    〈[(Init_int8 (repr I8 136)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 16) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 18 (* l3 *), Any〉,
+    〈[(Init_int8 (repr I8 105)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 17) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 19 (* l2 *), Any〉,
+   〈[(Init_int8 (repr I8 234)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 18) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 20 (* l1 *), Any〉,
+   〈[(Init_int8 (repr I8 240)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 19) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 14 (* l0 *), Any〉,
+    〈[(Init_int8 (repr I8 102)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 20) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉]
 .
 

src/Clight/test/search.c.ma

@@ -2 +2 @@
 include "common/Animation.ma".
 
-definition myprog := mk_program clight_fundef type
+definition myprog := mk_program clight_fundef ((list init_data) × type)
   [〈ident_of_nat 0 (* search *), CL_Internal (
      mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]

src/Clight/test/sum.c.ma

@@ -2 +2 @@
 include "common/Animation.ma".
 
-definition myprog := mk_program clight_fundef type
+definition myprog := mk_program clight_fundef (list init_data × type)
   [〈ident_of_nat 0 (* main *), CL_Internal (
      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ]
@@ -48 +48 @@
    )〉]
   (ident_of_nat 0)
-  [〈〈〈ident_of_nat 3 (* src *),
-     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
+  [〈〈ident_of_nat 3 (* src *), Any〉,
+     〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
      (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
-     (Init_int8 (repr I8 4)) ]〉, Any〉,
-     (Tarray Any (Tint I8 Unsigned ) 5)〉]
+     (Init_int8 (repr I8 4)) ],
+     (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
 .
 

src/Clight/toCminor.ma

@@ -779 +779 @@
 λp.
   let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
-  let var_globals ≝ map … (λv. 〈\fst (\fst (\fst v)), \snd (\fst v)〉) (prog_vars ?? p) in
+  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
   let globals ≝ fun_globals @ var_globals in
-  transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p.
+  transform_partial_program2 ???? (translate_fundef globals) (λi. OK ? (\fst i)) p.

src/Cminor/initialisation.ma

@@ -40 +40 @@
   〈0, St_skip〉 init).
 
-definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
+definition init_vars : list (ident × region × (list init_data)) → stmt ≝
 λvars. foldr ??
-  (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) St_skip vars.
+  (λvar,s. St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) St_skip vars.
 
 definition add_statement : ident → stmt →
@@ -64 +64 @@
       | inr _ ⇒ 〈id',f'〉 ]).
 
-definition empty_vars : list (ident × (list init_data) × region × unit) →
-                        list (ident × (list init_data) × region × unit) ≝
-map ?? (λv. 〈〈〈\fst (\fst (\fst v)),
-               [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉,
-              \snd (\fst v)〉,
-              \snd v〉).
+definition empty_vars : list (ident × region × (list init_data)) →
+                        list (ident × region × nat) ≝
+map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉,
+              size_init_data_list (\snd v)〉).
 
-definition replace_init : Cminor_program → Cminor_program ≝
+definition replace_init : Cminor_program → Cminor_noinit_program ≝
 λp.
   mk_program ??

src/Cminor/semantics.ma

@@ -274 +274 @@
 definition make_initial_state : Cminor_program → res (genv × state) ≝
 λp.
-  do ge ← globalenv Genv ?? p;
-  do m ← init_mem Genv ?? p;
+  do ge ← globalenv Genv ?? (λx.x) p;
+  do m ← init_mem Genv ?? (λx.x) p;
   do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
   do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
@@ -282 +282 @@
 definition Cminor_fullexec : fullexec io_out io_in ≝
   mk_fullexec … Cminor_exec ? make_initial_state.
+
+definition make_initial_noinit_state : Cminor_noinit_program → res (genv × state) ≝
+λp.
+  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
+  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
+  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
+  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
+  OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
+
+definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
+  mk_fullexec … Cminor_exec ? make_initial_noinit_state.

src/Cminor/syntax.ma

@@ -41 +41 @@
 }.
 
-definition Cminor_program ≝ program (fundef internal_function) unit.
+definition Cminor_program ≝ program (fundef internal_function) (list init_data).
+
+definition Cminor_noinit_program ≝ program (fundef internal_function) nat.

src/Cminor/toRTLabs.ma

@@ -295 +295 @@
 qed.
 
-definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
+definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
 transform_partial_program ???
   (transf_partial_fundef ?? c2ra_function).
@@ -301 +301 @@
 include "Cminor/initialisation.ma".
 
-definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
-λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
+definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
+λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.

src/RTLabs/semantics.ma

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

src/RTLabs/syntax.ma

@@ -40 +40 @@
 
 (* Note that the global variables will be initialised by the code in main
-   by this stage.  All initialisation data should only reserve space. *)
+   by this stage, so the only initialisation data is the amount of space to
+   allocate. *)
 
-definition RTLabs_program ≝ program (fundef internal_function) unit.
+definition RTLabs_program ≝ program (fundef internal_function) nat.
 
 (* TO CONSIDER:

src/common/AST.ma

@@ -282 +282 @@
   prog_funct: list (ident × F);
   prog_main: ident;
-  prog_vars: list (ident × (list init_data) × region × V)
+  prog_vars: list (ident × region × V)
 }.
 
@@ -290 +290 @@
 
 definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
-  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
+  map ?? (λx: ident × region × V. (\fst (\fst x))) (prog_vars ?? p).
 
 (* * * Generic transformations over programs *)

src/common/Globalenvs.ma

@@ -52 +52 @@
        of function descriptions. *)
 
-  globalenv: ∀F,V: Type[0]. program F V → res (genv_t F);
+  globalenv: ∀F,V: Type[0]. (V → list init_data) → program F V → res (genv_t F);
    (* * Return the global environment for the given program. *)
 
-  init_mem: ∀F,V: Type[0]. program F V → res mem;
+  init_mem: ∀F,V: Type[0]. (V → list init_data) → program F V → res mem;
    (* * Return the initial memory state for the given program. *)
 
@@ -486 +486 @@
 
 definition add_globals : ∀F,V:Type[0].
-       genv F × mem → list (ident × (list init_data) × region × V) →
+       (V → (list init_data)) →
+       genv F × mem → list (ident × region × V) →
        res (genv F × mem) ≝
-λF,V,init_env,vars.
+λF,V,extract_init,init_env,vars.
   foldl ??
-    (λg_st: res (genv F × mem). λid_init: ident × (list init_data) × region × V.
-      match id_init with [ pair id_init1 info ⇒
-      match id_init1 with [ pair id_init2 r ⇒
-      match id_init2 with [ pair id init ⇒
+    (λg_st: res (genv F × mem). λid_init: ident × region × V.
+      let 〈id, r, init_info〉 ≝ id_init in
+      let init ≝ extract_init init_info in
         do 〈g,st〉 ← g_st;
         match alloc_init_data st init r with [ pair st' b ⇒
@@ -499 +499 @@
           do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init);
             OK ? 〈g', st''〉
-        ] ] ] ])
+        ] )
     (OK ? init_env) vars.
 
-definition globalenv_initmem : ∀F,V:Type[0]. program F V → res (genv F × mem) ≝
-λF,V,p.
-  add_globals F V
-   〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
+definition globalenv_initmem : ∀F,V:Type[0]. (V → (list init_data)) → program F V → res (genv F × mem) ≝
+λF,V,init_info,p.
+  add_globals F V init_info
+   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
    (prog_vars ?? p).
 
-definition globalenv_ : ∀F,V:Type[0]. program F V → res (genv F) ≝
-λF,V,p.
-  do 〈g,m〉 ← globalenv_initmem F V p;
+definition globalenv_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (genv F) ≝
+λF,V,i,p.
+  do 〈g,m〉 ← globalenv_initmem F V i p;
     OK ? g.
-definition init_mem_ : ∀F,V:Type[0]. program F V → res (mem) ≝
-λF,V,p.
-  do 〈g,m〉 ← globalenv_initmem F V p;
+definition init_mem_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (mem) ≝
+λF,V,i,p.
+  do 〈g,m〉 ← globalenv_initmem F V i p;
     OK ? m.