Changeset 1139
- Timestamp:
- Aug 30, 2011, 12:47:18 PM (10 years ago)
- Location:
- src
- Files:
-
- 16 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Cexec.ma
r1058 r1139 534 534 535 535 let 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; 538 538 do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p)); 539 539 do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b); -
src/Clight/CexecSound.ma
r1058 r1139 533 533 qed. 534 534 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).535 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). 536 536 #p cases p; #fns #main #vars 537 537 whd in ⊢ (???%); -
src/Clight/Csem.ma
r1058 r1139 1511 1511 inductive initial_state (p: clight_program): state -> Prop := 1512 1512 | 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 → 1515 1515 find_symbol ?? ge (prog_main ?? p) = Some ? b → 1516 1516 find_funct_ptr ?? ge b = Some ? f → … … 1529 1529 1530 1530 definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh. 1531 ∀ge. globalenv ??? p = OK ? ge →1531 ∀ge. globalenv ??? (fst ??) p = OK ? ge → 1532 1532 program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh. 1533 1533 (* -
src/Clight/Csyntax.ma
r961 r1139 318 318 data. See module [AST] for more details. *) 319 319 320 definition clight_program : Type[0] ≝ program clight_fundef type.320 definition clight_program : Type[0] ≝ program clight_fundef (list init_data × type). 321 321 322 322 (* * * Operations over types *) -
src/Clight/test/insertsort.c.ma
r965 r1139 5 5 generate Init_null at the moment. *) 6 6 7 definition myprog := mk_program clight_fundef type7 definition myprog := mk_program clight_fundef ((list init_data) × type) 8 8 [〈ident_of_nat 0 (* insert *), CL_Internal ( 9 9 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 )〉] 168 168 (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)))〉〉] 197 196 . 198 197 -
src/Clight/test/search.c.ma
r978 r1139 2 2 include "common/Animation.ma". 3 3 4 definition myprog := mk_program clight_fundef type4 definition myprog := mk_program clight_fundef ((list init_data) × type) 5 5 [〈ident_of_nat 0 (* search *), CL_Internal ( 6 6 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 2 2 include "common/Animation.ma". 3 3 4 definition myprog := mk_program clight_fundef type4 definition myprog := mk_program clight_fundef (list init_data × type) 5 5 [〈ident_of_nat 0 (* main *), CL_Internal ( 6 6 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 1, (Tint I32 Signed )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ] … … 48 48 )〉] 49 49 (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)) ; 52 52 (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)〉〉] 55 55 . 56 56 -
src/Clight/toCminor.ma
r1078 r1139 779 779 λp. 780 780 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) in781 let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in 782 782 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 40 40 〈0, St_skip〉 init). 41 41 42 definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝42 definition init_vars : list (ident × region × (list init_data)) → stmt ≝ 43 43 λ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. 45 45 46 46 definition add_statement : ident → stmt → … … 64 64 | inr _ ⇒ 〈id',f'〉 ]). 65 65 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〉). 66 definition empty_vars : list (ident × region × (list init_data)) → 67 list (ident × region × nat) ≝ 68 map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉, 69 size_init_data_list (\snd v)〉). 72 70 73 definition replace_init : Cminor_program → Cminor_ program ≝71 definition replace_init : Cminor_program → Cminor_noinit_program ≝ 74 72 λp. 75 73 mk_program ?? -
src/Cminor/semantics.ma
r961 r1139 274 274 definition make_initial_state : Cminor_program → res (genv × state) ≝ 275 275 λ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; 278 278 do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p)); 279 279 do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b); … … 282 282 definition Cminor_fullexec : fullexec io_out io_in ≝ 283 283 mk_fullexec … Cminor_exec ? make_initial_state. 284 285 definition 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 293 definition Cminor_noinit_fullexec : fullexec io_out io_in ≝ 294 mk_fullexec … Cminor_exec ? make_initial_noinit_state. -
src/Cminor/syntax.ma
r961 r1139 41 41 }. 42 42 43 definition Cminor_program ≝ program (fundef internal_function) unit. 43 definition Cminor_program ≝ program (fundef internal_function) (list init_data). 44 45 definition Cminor_noinit_program ≝ program (fundef internal_function) nat. -
src/Cminor/toRTLabs.ma
r1072 r1139 295 295 qed. 296 296 297 definition cminor_ to_rtlabs : Cminor_program → res RTLabs_program ≝297 definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝ 298 298 transform_partial_program ??? 299 299 (transf_partial_fundef ?? c2ra_function). … … 301 301 include "Cminor/initialisation.ma". 302 302 303 definition cminor_ init_to_rtlabs : Cminor_program → res RTLabs_program ≝304 λp. let p' ≝ replace_init p in cminor_ to_rtlabs p.303 definition 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 209 209 definition make_initial_state : RTLabs_program → res (genv × state) ≝ 210 210 λ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; 213 213 let main ≝ prog_main ?? p in 214 214 do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main); -
src/RTLabs/syntax.ma
r1116 r1139 40 40 41 41 (* 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. *) 43 44 44 definition RTLabs_program ≝ program (fundef internal_function) unit.45 definition RTLabs_program ≝ program (fundef internal_function) nat. 45 46 46 47 (* TO CONSIDER: -
src/common/AST.ma
r1064 r1139 282 282 prog_funct: list (ident × F); 283 283 prog_main: ident; 284 prog_vars: list (ident × (list init_data) ×region × V)284 prog_vars: list (ident × region × V) 285 285 }. 286 286 … … 290 290 291 291 definition 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). 293 293 294 294 (* * * Generic transformations over programs *) -
src/common/Globalenvs.ma
r961 r1139 52 52 of function descriptions. *) 53 53 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); 55 55 (* * Return the global environment for the given program. *) 56 56 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; 58 58 (* * Return the initial memory state for the given program. *) 59 59 … … 486 486 487 487 definition 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) → 489 490 res (genv F × mem) ≝ 490 λF,V, init_env,vars.491 λF,V,extract_init,init_env,vars. 491 492 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 496 496 do 〈g,st〉 ← g_st; 497 497 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); 500 500 OK ? 〈g', st''〉 501 ] ] ] ])501 ] ) 502 502 (OK ? init_env) vars. 503 503 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 Vp), empty_mem〉504 definition 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〉 508 508 (prog_vars ?? p). 509 509 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;510 definition 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; 513 513 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;514 definition 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; 517 517 OK ? m. 518 518
Note: See TracChangeset
for help on using the changeset viewer.