Changeset 1231 for src/Clight/Cexec.ma


Ignore:
Timestamp:
Sep 20, 2011, 7:11:41 PM (9 years ago)
Author:
campbell
Message:

Change SmallstepExec? so that states can depend on global information.
Use less suggestive names for the transition system so that it's obvious
the global information isn't restricted to Genv.
Separate set up of global environment from initialisation so that it never
fails.
Some minimal changes to get Clight execution working; rest to follow.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1147 r1231  
    499499axiom MainMissing : String.
    500500
    501 let rec make_initial_state (p:clight_program) : res (genv × state) ≝
    502   do ge ← globalenv Genv ?? (fst ??) p;
     501let rec make_global (p:clight_program) : genv ≝
     502  globalenv Genv ?? (fst ??) p.
     503
     504let rec make_initial_state (p:clight_program) : res state ≝
     505  let ge ≝ make_global p in
    503506  do m0 ← init_mem Genv ?? (fst ??) p;
    504507  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    505508  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    506   OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
     509  OK ? (Callstate f (nil ?) Kstop m0).
    507510
    508511let rec is_final (s:state) : option int ≝
     
    558561λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
    559562
    560 definition clight_exec : execstep io_out io_in ≝
    561   mk_execstep … is_final mem_of_state exec_step.
     563definition clight_exec : trans_system io_out io_in ≝
     564  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
    562565
    563566definition clight_fullexec : fullexec io_out io_in ≝
    564   mk_fullexec ?? clight_exec ? make_initial_state.
     567  mk_fullexec ??? clight_exec make_global make_initial_state.
Note: See TracChangeset for help on using the changeset viewer.