Changeset 2443 for src/joint/Traces.ma


Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (8 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2442 r2443  
    77 ; exit: cpointer
    88 ; ev_genv: genv sparams globals
    9  ; io_env : state sparams → ∀o:io_out.res (io_in o)
     9(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
    1010 }.
    1111 
     
    1313 { prog_spars : sem_params
    1414 ; prog : joint_program prog_spars
    15  ; prog_io : state prog_spars → ∀o.res (io_in o)
     15(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
    1616 }.
    1717
     
    2828  «ptr, refl …»
    2929  (mk_genv_gen ?? (globalenv_noinit ? p) ?)
    30   (prog_io pars).
     30 (* (prog_io pars) *).
    3131(* TODO or TOBEFOUND *)
    3232cases daemon
     
    4949  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in
    5050  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
    51   let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in
     51(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
    5252  let main ≝ prog_main … p in
    53   let st0 ≝ mk_state pars (empty_framesT …) spp ispp (BBbit false) (empty_regsT … spp) m in
     53  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
     54  let st0' ≝ set_sp … spp st0 in
    5455  (* use exit sem_globals as ra and call_dest_for_main as dest *)
    55   ! st0' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
    56   let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
     56  ! st0'' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
     57  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
    5758  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
    5859  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
     
    6364  ].
    6465  [ %
    65   | cases ispb
    66   | cases spb
    67   ] normalize //
     66  | cases spb normalize //
     67  ]
    6868qed.
    6969
     
    114114qed.
    115115
     116(*
    116117let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
    117118  match c with
     
    122123  | Wrong e ⇒ Error … e
    123124  ].
     125*)
    124126
    125127definition cost_label_of_stmt :
     
    145147   (* as_status ≝ *) (state_pc p)
    146148   (* as_execute ≝ *)
    147     (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)
     149    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2)
    148150   (* as_pc ≝ *) cpointerDeq
    149151   (* as_pc_of ≝ *) (pc …)
     
    151153    (λs.
    152154      match (
    153         ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) ;
     155        ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) : IO ???;
    154156        match stmt with
    155157        [ sequential stp nxt ⇒
    156           ! 〈flow, s'〉  ← io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) ;
     158          ! 〈flow, s'〉  ← (* io_evaluate … (io_env p s) *) (eval_step … (ev_genv p) fn s stp) ;
    157159          return step_flow_classifier … flow
    158160        | final stp ⇒
    159           ! flow ← io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
     161          ! flow ← (* io_evaluate … (io_env p s) *) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
    160162          return fin_step_flow_classifier … flow
    161163        ]) with
    162       [ OK c ⇒ c
    163       | Error _ ⇒ cl_other
     164      [ Value c ⇒ c
     165      | _ ⇒ cl_other
    164166      ])
    165167   (* as_label_of_pc ≝ *)
     
    175177      succ_pc p p (pc … s1) nxt = return pc … s2)
    176178   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
    177    (* as_call_ident_≝ *) ?. cases daemon (* TODO *) qed.
     179   (* as_call_ident_≝ *)
     180   (λst.?). cases daemon (* TODO *) qed.
Note: See TracChangeset for help on using the changeset viewer.