Changeset 1238


Ignore:
Timestamp:
Sep 21, 2011, 4:25:36 PM (8 years ago)
Author:
campbell
Message:

Update Cminor and RTLabs to fit SmallstepExec? changes.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/search.c.ma

    r1224 r1238  
    192192include "Cminor/semantics.ma".
    193193
     194example e1: finishes_with (repr I32 3) ? (bind ? (snapshot state) (clight_to_cminor myprog) (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
     195(*
    194196example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     197*)
    195198normalize
    196199@refl
     
    202205example e2: finishes_with (repr 3) ? (
    203206do p1 ← clight_to_cminor myprog;
     207bind ? (snapshot state) (cminor_to_rtlabs p1) (λp2.
     208 exec_up_to RTLabs_fullexec p2 1000 [ ])).
     209(*
     210example e2: finishes_with (repr 3) ? (
     211do p1 ← clight_to_cminor myprog;
    204212do p2 ← cminor_to_rtlabs p1;
    205  exec_up_to RTLabs_fullexec p2 1000 [ ]).
     213 exec_up_to RTLabs_fullexec p2 1000 [ ]).*)
    206214normalize
    207215@refl
  • src/Cminor/semantics.ma

    r1139 r1238  
    267267].
    268268
    269 definition Cminor_exec : execstep io_out io_in ≝
    270   mk_execstep … ? is_final mem_of_state eval_step.
     269definition Cminor_exec : trans_system io_out io_in ≝
     270  mk_trans_system … ? (λ_.is_final) eval_step.
    271271
    272272axiom MainMissing : String.
    273273
    274 definition make_initial_state : Cminor_program → res (genv × state) ≝
     274definition make_global : Cminor_program → genv ≝
     275λp. globalenv Genv ?? (λx.x) p.
     276
     277definition make_initial_state : Cminor_program → res state ≝
    275278λp.
    276   do ge ← globalenv Genv ?? (λx.x) p;
     279  let ge ≝ make_global p in
    277280  do m ← init_mem Genv ?? (λx.x) p;
    278281  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    279282  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    280   OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
     283  OK ? (Callstate f (nil ?) m Kstop).
    281284
    282285definition Cminor_fullexec : fullexec io_out io_in ≝
    283   mk_fullexec … Cminor_exec ? make_initial_state.
    284 
    285 definition make_initial_noinit_state : Cminor_noinit_program → res (genv × state) ≝
     286  mk_fullexec … Cminor_exec make_global make_initial_state.
     287
     288definition make_noinit_global : Cminor_noinit_program → genv ≝
     289λp. globalenv Genv ?? (λx.[Init_space x]) p.
     290
     291definition make_initial_noinit_state : Cminor_noinit_program → res state ≝
    286292λp.
    287   do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     293  let ge ≝ make_noinit_global p in
    288294  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    289295  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    290296  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    291   OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
     297  OK ? (Callstate f (nil ?) m Kstop).
    292298
    293299definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
    294   mk_fullexec … Cminor_exec ? make_initial_noinit_state.
     300  mk_fullexec … Cminor_exec make_noinit_global make_initial_noinit_state.
  • src/RTLabs/semantics.ma

    r1139 r1238  
    204204].
    205205
    206 definition RTLabs_exec : execstep io_out io_in ≝
    207   mk_execstep … ? is_final mem_of_state eval_statement.
    208 
    209 definition make_initial_state : RTLabs_program → res (genv × state) ≝
     206definition RTLabs_exec : trans_system io_out io_in ≝
     207  mk_trans_system … ? (λ_.is_final) eval_statement.
     208
     209definition make_global : RTLabs_program → genv ≝
     210λp. globalenv Genv ?? (λx.[Init_space x]) p.
     211
     212definition make_initial_state : RTLabs_program → res state ≝
    210213λp.
    211   do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     214  let ge ≝ make_global p in
    212215  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    213216  let main ≝ prog_main ?? p in
    214217  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    215218  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    216   OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
     219  OK ? (Callstate f (nil ?) (None ?) (nil ?) m).
    217220
    218221definition RTLabs_fullexec : fullexec io_out io_in ≝
    219   mk_fullexec … RTLabs_exec ? make_initial_state.
    220 
     222  mk_fullexec … RTLabs_exec make_global make_initial_state.
     223
Note: See TracChangeset for help on using the changeset viewer.