Changeset 1139


Ignore:
Timestamp:
Aug 30, 2011, 12:47:18 PM (8 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:
16 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1058 r1139  
    534534
    535535let rec make_initial_state (p:clight_program) : res (genv × state) ≝
    536   do ge ← globalenv Genv ?? p;
    537   do m0 ← init_mem Genv ?? p;
     536  do ge ← globalenv Genv ?? (fst ??) p;
     537  do m0 ← init_mem Genv ?? (fst ??) p;
    538538  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    539539  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
  • src/Clight/CexecSound.ma

    r1058 r1139  
    533533qed.
    534534
    535 lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
     535lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? (fst ??) p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
    536536#p cases p; #fns #main #vars
    537537whd in ⊢ (???%);
  • src/Clight/Csem.ma

    r1058 r1139  
    15111511inductive initial_state (p: clight_program): state -> Prop :=
    15121512  | initial_state_intro: ∀b,f,ge,m0.
    1513       globalenv Genv ?? p = OK ? ge →
    1514       init_mem Genv ?? p = OK ? m0 →
     1513      globalenv Genv ?? (fst ??) p = OK ? ge →
     1514      init_mem Genv ?? (fst ??) p = OK ? m0 →
    15151515      find_symbol ?? ge (prog_main ?? p) = Some ? b →
    15161516      find_funct_ptr ?? ge b = Some ? f →
     
    15291529
    15301530definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    1531   ∀ge. globalenv ??? p = OK ? ge →
     1531  ∀ge. globalenv ??? (fst ??) p = OK ? ge →
    15321532  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
    15331533(*
  • src/Clight/Csyntax.ma

    r961 r1139  
    318318  data.  See module [AST] for more details. *)
    319319
    320 definition clight_program : Type[0] ≝ program clight_fundef type.
     320definition clight_program : Type[0] ≝ program clight_fundef (list init_data × type).
    321321
    322322(* * * Operations over types *)
  • src/Clight/test/insertsort.c.ma

    r965 r1139  
    55   generate Init_null at the moment. *)
    66
    7 definition myprog := mk_program clight_fundef type
     7definition myprog := mk_program clight_fundef ((list init_data) × type)
    88  [〈ident_of_nat 0 (* insert *), CL_Internal (
    99     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  )〉 ]
     
    167167  )〉]
    168168  (ident_of_nat 12)
    169   [〈〈〈ident_of_nat 15 (* l6 *),
    170      [(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ]〉,
    171      Any〉,
    172      (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)))〉;
    173   〈〈〈ident_of_nat 16 (* l5 *),
    174     [(Init_int8 (repr I8 36)) ; (Init_space 3) ;
    175     (Init_addrof Any (ident_of_nat 15) 0)]〉, Any〉,
    176     (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)))〉;
    177   〈〈〈ident_of_nat 17 (* l4 *),
    178     [(Init_int8 (repr I8 136)) ; (Init_space 3) ;
    179     (Init_addrof Any (ident_of_nat 16) 0)]〉, Any〉,
    180     (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)))〉;
    181   〈〈〈ident_of_nat 18 (* l3 *),
    182     [(Init_int8 (repr I8 105)) ; (Init_space 3) ;
    183     (Init_addrof Any (ident_of_nat 17) 0)]〉, Any〉,
    184     (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)))〉;
    185   〈〈〈ident_of_nat 19 (* l2 *),
    186     [(Init_int8 (repr I8 234)) ; (Init_space 3) ;
    187     (Init_addrof Any (ident_of_nat 18) 0)]〉, Any〉,
    188     (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)))〉;
    189   〈〈〈ident_of_nat 20 (* l1 *),
    190     [(Init_int8 (repr I8 240)) ; (Init_space 3) ;
    191     (Init_addrof Any (ident_of_nat 19) 0)]〉, Any〉,
    192     (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)))〉;
    193   〈〈〈ident_of_nat 14 (* l0 *),
    194     [(Init_int8 (repr I8 102)) ; (Init_space 3) ;
    195     (Init_addrof Any (ident_of_nat 20) 0)]〉, Any〉,
    196     (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)))〉]
     169  [〈〈ident_of_nat 15 (* l6 *), Any〉,
     170    〈[(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ],
     171     (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)))〉〉;
     172  〈〈ident_of_nat 16 (* l5 *), Any〉,
     173    〈[(Init_int8 (repr I8 36)) ; (Init_space 3) ;
     174    (Init_addrof Any (ident_of_nat 15) 0)],
     175    (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)))〉〉;
     176  〈〈ident_of_nat 17 (* l4 *), Any〉,
     177    〈[(Init_int8 (repr I8 136)) ; (Init_space 3) ;
     178    (Init_addrof Any (ident_of_nat 16) 0)],
     179    (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)))〉〉;
     180  〈〈ident_of_nat 18 (* l3 *), Any〉,
     181    〈[(Init_int8 (repr I8 105)) ; (Init_space 3) ;
     182    (Init_addrof Any (ident_of_nat 17) 0)],
     183    (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)))〉〉;
     184  〈〈ident_of_nat 19 (* l2 *), Any〉,
     185   〈[(Init_int8 (repr I8 234)) ; (Init_space 3) ;
     186    (Init_addrof Any (ident_of_nat 18) 0)],
     187    (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)))〉〉;
     188  〈〈ident_of_nat 20 (* l1 *), Any〉,
     189   〈[(Init_int8 (repr I8 240)) ; (Init_space 3) ;
     190    (Init_addrof Any (ident_of_nat 19) 0)],
     191    (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)))〉〉;
     192  〈〈ident_of_nat 14 (* l0 *), Any〉,
     193    〈[(Init_int8 (repr I8 102)) ; (Init_space 3) ;
     194    (Init_addrof Any (ident_of_nat 20) 0)],
     195    (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)))〉〉]
    197196.
    198197
  • src/Clight/test/search.c.ma

    r978 r1139  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
     4definition myprog := mk_program clight_fundef ((list init_data) × type)
    55  [〈ident_of_nat 0 (* search *), CL_Internal (
    66     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

    r965 r1139  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
     4definition myprog := mk_program clight_fundef (list init_data × type)
    55  [〈ident_of_nat 0 (* main *), CL_Internal (
    66     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ]
     
    4848   )〉]
    4949  (ident_of_nat 0)
    50   [〈〈〈ident_of_nat 3 (* src *),
    51      [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
     50  [〈〈ident_of_nat 3 (* src *), Any〉,
     51     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
    5252     (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
    53      (Init_int8 (repr I8 4)) ]〉, Any〉,
    54      (Tarray Any (Tint I8 Unsigned ) 5)〉]
     53     (Init_int8 (repr I8 4)) ],
     54     (Tarray Any (Tint I8 Unsigned ) 5)〉]
    5555.
    5656
  • src/Clight/toCminor.ma

    r1078 r1139  
    779779λp.
    780780  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
    781   let var_globals ≝ map … (λv. 〈\fst (\fst (\fst v)), \snd (\fst v)〉) (prog_vars ?? p) in
     781  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
    782782  let globals ≝ fun_globals @ var_globals in
    783   transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p.
     783  transform_partial_program2 ???? (translate_fundef globals) (λi. OK ? (\fst i)) p.
  • 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'.
  • src/RTLabs/semantics.ma

    r1123 r1139  
    209209definition make_initial_state : RTLabs_program → res (genv × state) ≝
    210210λp.
    211   do ge ← globalenv Genv ?? p;
    212   do m ← init_mem Genv ?? p;
     211  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     212  do m ← init_mem Genv ?? (λx.[Init_space 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/syntax.ma

    r1116 r1139  
    4040
    4141(* Note that the global variables will be initialised by the code in main
    42    by this stage.  All initialisation data should only reserve space. *)
     42   by this stage, so the only initialisation data is the amount of space to
     43   allocate. *)
    4344
    44 definition RTLabs_program ≝ program (fundef internal_function) unit.
     45definition RTLabs_program ≝ program (fundef internal_function) nat.
    4546
    4647(* TO CONSIDER:
  • src/common/AST.ma

    r1064 r1139  
    282282  prog_funct: list (ident × F);
    283283  prog_main: ident;
    284   prog_vars: list (ident × (list init_data) × region × V)
     284  prog_vars: list (ident × region × V)
    285285}.
    286286
     
    290290
    291291definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
    292   map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
     292  map ?? (λx: ident × region × V. (\fst (\fst x))) (prog_vars ?? p).
    293293
    294294(* * * Generic transformations over programs *)
  • src/common/Globalenvs.ma

    r961 r1139  
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V: Type[0]. program F V → res (genv_t F);
     54  globalenv: ∀F,V: Type[0]. (V → list init_data) → program F V → res (genv_t F);
    5555   (* * Return the global environment for the given program. *)
    5656
    57   init_mem: ∀F,V: Type[0]. program F V → res mem;
     57  init_mem: ∀F,V: Type[0]. (V → list init_data) → program F V → res mem;
    5858   (* * Return the initial memory state for the given program. *)
    5959
     
    486486
    487487definition add_globals : ∀F,V:Type[0].
    488        genv F × mem → list (ident × (list init_data) × region × V) →
     488       (V → (list init_data)) →
     489       genv F × mem → list (ident × region × V) →
    489490       res (genv F × mem) ≝
    490 λF,V,init_env,vars.
     491λF,V,extract_init,init_env,vars.
    491492  foldl ??
    492     (λg_st: res (genv F × mem). λid_init: ident × (list init_data) × region × V.
    493       match id_init with [ pair id_init1 info ⇒
    494       match id_init1 with [ pair id_init2 r ⇒
    495       match id_init2 with [ pair id init ⇒
     493    (λg_st: res (genv F × mem). λid_init: ident × region × V.
     494      let 〈id, r, init_info〉 ≝ id_init in
     495      let init ≝ extract_init init_info in
    496496        do 〈g,st〉 ← g_st;
    497497        match alloc_init_data st init r with [ pair st' b ⇒
     
    499499          do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init);
    500500            OK ? 〈g', st''〉
    501         ] ] ] ])
     501        ] )
    502502    (OK ? init_env) vars.
    503503
    504 definition globalenv_initmem : ∀F,V:Type[0]. program F V → res (genv F × mem) ≝
    505 λF,V,p.
    506   add_globals F V
    507    〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
     504definition globalenv_initmem : ∀F,V:Type[0]. (V → (list init_data)) → program F V → res (genv F × mem) ≝
     505λF,V,init_info,p.
     506  add_globals F V init_info
     507   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
    508508   (prog_vars ?? p).
    509509
    510 definition globalenv_ : ∀F,V:Type[0]. program F V → res (genv F) ≝
    511 λF,V,p.
    512   do 〈g,m〉 ← globalenv_initmem F V p;
     510definition globalenv_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (genv F) ≝
     511λF,V,i,p.
     512  do 〈g,m〉 ← globalenv_initmem F V i p;
    513513    OK ? g.
    514 definition init_mem_ : ∀F,V:Type[0]. program F V → res (mem) ≝
    515 λF,V,p.
    516   do 〈g,m〉 ← globalenv_initmem F V p;
     514definition init_mem_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (mem) ≝
     515λF,V,i,p.
     516  do 〈g,m〉 ← globalenv_initmem F V i p;
    517517    OK ? m.
    518518
Note: See TracChangeset for help on using the changeset viewer.