Changeset 1139 for src/Clight


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/Clight
Files:
8 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.
Note: See TracChangeset for help on using the changeset viewer.