Changeset 1231 for src/common


Ignore:
Timestamp:
Sep 20, 2011, 7:11:41 PM (8 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.

Location:
src/common
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/Animation.ma

    r1213 r1231  
    2323axiom StoppedMidIO : String.
    2424
    25 let rec up_to_nth_step (n:nat) (ex:execstep io_out io_in) (input:list eventval) (e:execution (state ?? ex) io_out io_in) (t:trace) : res (snapshot (state ?? ex)) ≝
     25let rec up_to_nth_step (n:nat) (state:Type[0]) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (snapshot state) ≝
    2626match n with
    2727[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
     
    2929                   | e_interact o k ⇒ Error ? (msg StoppedMidIO)
    3030                   | e_wrong m ⇒ Error ? m ]
    31 | S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m ex input e' (t⧺tr)
     31| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m state input e' (t⧺tr)
    3232                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
    3333                     | e_interact o k ⇒
     
    3535                         [ nil ⇒ OK ? (input_exhausted ? t)
    3636                         | cons h tl ⇒ do i ← get_input o h;
    37                                        up_to_nth_step m ex tl (k i) t
     37                                       up_to_nth_step m state tl (k i) t
    3838                         ]
    3939                     | e_wrong m ⇒ Error ? m
     
    4141].
    4242
    43 definition exec_up_to : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → res (snapshot (state ?? fx)) ≝
    44 λfx,p,n,i. up_to_nth_step n fx i (exec_inf ?? fx p) E0.
     43definition exec_up_to : ∀fx:fullexec io_out io_in. ∀p:program ?? fx. nat → list eventval → res (snapshot (state ?? fx (make_global … p))) ≝
     44λfx,p,n,i. up_to_nth_step n ? i (exec_inf ?? fx p) E0.
    4545
    4646(* A version of exec_up_to that reports the state prior to failure. *)
     
    5252| failed' : errmsg → nat → state → snapshot' state
    5353| init_state_fail' : errmsg → snapshot' state.
    54 
     54(*
    5555let rec up_to_nth_step' (n:nat) (total:nat) (ex:execstep io_out io_in) (input:list eventval) (e:execution (state ?? ex) io_out io_in) (prev:state ?? ex) (t:trace) : snapshot' (state ?? ex) ≝
    5656match n with
     
    7979| Error m ⇒ init_state_fail' ? m
    8080].
    81 
     81*)
    8282(* Provide an easy way to get a term in proof mode for reduction.
    8383   For example,
  • src/common/Globalenvs.ma

    r1224 r1231  
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. res (genv_t (F (prog_var_names … p)));
     54  globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. genv_t (F (prog_var_names … p));
    5555   (* * Return the global environment for the given program. *)
    5656
     
    488488       (V → (list init_data)) →
    489489       genv F × mem → list (ident × region × V) →
    490        res (genv F × mem) ≝
     490       (genv F × mem) ≝
    491491λF,V,extract_init,init_env,vars.
    492492  foldl ??
    493     (λg_st: res (genv F × mem). λid_init: ident × region × V.
     493    (λg_st: genv F × mem. λid_init: ident × region × V.
    494494      let 〈id, r, init_info〉 ≝ id_init in
    495495      let init ≝ extract_init init_info in
    496         do 〈g,st〉 ← g_st;
     496      let 〈g,st〉 ≝ g_st in
    497497        match alloc_init_data st init r with [ pair st' b ⇒
    498498          let g' ≝ add_symbol ? id b g in
    499           do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init);
    500             OK ? 〈g', st''〉
     499            〈g', st'〉
    501500        ] )
    502     (OK ? init_env) vars.
    503 
    504 definition globalenv_initmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. res (genv (F (prog_var_names … p)) × mem) ≝
     501    init_env vars.
     502
     503definition init_globals : ∀F,V:Type[0].
     504       (V → (list init_data)) →
     505       genv F → mem → list (ident × region × V) →
     506       res mem ≝
     507λF,V,extract_init,g,m,vars.
     508  foldl ??
     509    (λst: res mem. λid_init: ident × region × V.
     510      let 〈id, r, init_info〉 ≝ id_init in
     511      let init ≝ extract_init init_info in
     512        do st ← st;
     513        match symbols ? g id with
     514        [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init)
     515        | None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *)
     516        ] )
     517    (OK ? m) vars.
     518
     519definition globalenv_allocmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. (genv (F (prog_var_names … p)) × mem) ≝
    505520λF,V,init_info,p.
    506521  add_globals … init_info
     
    508523   (prog_vars ?? p).
    509524
    510 definition globalenv_ : ∀F,V. (V → list init_data) → ∀p:program F V. res (genv (F (prog_var_names … p))) ≝
     525definition globalenv_ : ∀F,V. (V → list init_data) → ∀p:program F V. genv (F (prog_var_names … p)) ≝
    511526λF,V,i,p.
    512   do 〈g,m〉 ← globalenv_initmem F V i p;
    513     OK ? g.
     527  \fst (globalenv_allocmem F V i p).
     528
    514529definition init_mem_ : ∀F,V. (V → list init_data) → program F V → res (mem) ≝
    515530λF,V,i,p.
    516   do 〈g,m〉 ← globalenv_initmem F V i p;
    517     OK ? m.
     531  let 〈g,m〉 ≝ globalenv_allocmem F V i p in
     532  init_globals ? V i g m (prog_vars ?? p).
    518533
    519534
  • src/common/SmallstepExec.ma

    r1213 r1231  
    44include "common/Events.ma".
    55
    6 record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    7 { mem : Type[0]
    8 ; genv  : Type[0]
    9 ; state : Type[0]
    10 ; is_final : state → option int
    11 ; mem_of_state : state → mem
    12 ; step : genv → state → IO outty inty (trace×state)
     6record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
     7{ global : Type[0]
     8; state  : global → Type[0]
     9; is_final : ∀g. state g → option int
     10; step : ∀g. state g → IO outty inty (trace×(state g))
    1311}.
    1412
    15 let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:execstep outty inty)
    16                (g:genv ?? exec) (s:state ?? exec)
    17  : IO outty inty (trace × (state ?? exec)) ≝
     13let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:trans_system outty inty)
     14               (g:global ?? exec) (s:state ?? exec g)
     15 : IO outty inty (trace × (state ?? exec g)) ≝
    1816match n with
    1917[ O ⇒ Value ??? 〈E0, s〉
     
    4442
    4543let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
    46                        (exec:execstep output input) (ge:genv ?? exec)
    47                        (s:IO output input (trace×(state ?? exec)))
     44                       (exec:trans_system output input) (g:global ?? exec)
     45                       (s:IO output input (trace×(state ?? exec g)))
    4846                       : execution ??? ≝
    4947match s with
    5048[ Wrong m ⇒ e_wrong ??? m
    5149| Value v ⇒ match v with [ pair t s' ⇒
    52     match is_final ?? exec s' with
     50    match is_final ?? exec g s' with
    5351    [ Some r ⇒ e_stop ??? t r s'
    54     | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    55 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
     52    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] ]
     53| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
    5654].
    5755
     
    6462  here, used reflexivity instead *)
    6563
    66 axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
     64axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
    6765match s with
    6866[ Wrong m ⇒ e_wrong ??? m
    6967| Value v ⇒ match v with [ pair t s' ⇒
    70     match is_final ?? exec s' with
     68    match is_final ?? exec g s' with
    7169    [ Some r ⇒ e_stop ??? t r s'
    72     | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    73 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
     70    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] ]
     71| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
    7472].
    7573(*
     
    8381
    8482record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    85 { es1 :> execstep outty inty
    86 ; program : Type[0]
    87 ; make_initial_state : program → res (genv ?? es1 × (state ?? es1))
     83{ program : Type[0]
     84; es1 :> trans_system outty inty
     85; make_global : program → global ?? es1
     86; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
    8887}.
    8988
    90 definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx) o i ≝
     89definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
    9190λo,i,fx,p.
    9291  match make_initial_state ?? fx p with
    93   [ OK gs ⇒ exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)
     92  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
    9493  | Error m ⇒ e_wrong ??? m
    9594  ].
    9695
    97 
     96(* Some preliminary simulation stuff that's not been used yet.
    9897record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    9998{ es0 :> execstep outty inty
     
    125124          match_states sems st1' st2'
    126125}.
     126*)
Note: See TracChangeset for help on using the changeset viewer.