Changeset 2563


Ignore:
Timestamp:
Dec 19, 2012, 11:58:35 AM (7 years ago)
Author:
piccolo
Message:

Repairing ERTL: show stopper found.

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r2490 r2563  
    3737    (* call_dest ≝ *) unit
    3838    (* ext_seq ≝ *) ertl_seq
     39    (* ext_seq_labels ≝ *) (λ_.[])
    3940    (* has_tailcall ≝ *) false
    4041    (* paramsT ≝ *) ℕ
  • src/ERTL/semantics.ma

    r2286 r2563  
    1 include "joint/SemanticUtils.ma".
     1include "joint/semanticsUtils.ma".
    22include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
    33include alias "common/Identifiers.ma".
     
    1717definition ertl_reg_env ≝ ertl_psd_env × hw_register_env.
    1818
    19 definition ps_reg_store
     19definition ps_reg_store: ? → ? → ? → res ?
    2020 λr,v.λlocal_env : ertl_reg_env.
    2121  do res ← reg_store r v (psd_regs (\fst local_env)) ;
     
    3434  OK … (hwreg_retrieve … (\snd local_env) reg).
    3535
    36 definition ps_arg_retrieve ≝
     36
     37definition ps_arg_retrieve : ertl_reg_env → argument ? → res beval ≝
    3738  λlocal_env,a.
    3839  match a with
    3940  [ Reg r ⇒ ps_reg_retrieve local_env r
    40   | Imm b ⇒ return b
     41  | Imm b ⇒ return BVByte b
    4142  ].
     43
     44
    4245
    4346definition ERTL_state : sem_state_params ≝
     
    4649 (* empty_framesT ≝ *) [ ]
    4750 (* regsT ≝ *) ertl_reg_env
    48  (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉).
     51 (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉)
     52 (*load_sp ≝ *) ?
     53  (*save_sp ≝ *) ?. cases daemon qed.
    4954
    5055(* we ignore need_spilled_no as we never move framesize based values around in the
     
    5863          | HDW r ⇒ hw_reg_retrieve env r
    5964          ]
    60         | Imm bv ⇒ return bv ] ;
     65        | Imm b ⇒ return BVByte b ] ;
    6166      match \fst pr with
    6267      [ PSD r ⇒ ps_reg_store r v env
     
    6974
    7075definition ertl_save_frame:
    71  cpointer → unit → state … ERTL_state → res (state … ERTL_state) ≝
    72  λpc.λ_.λst.
    73   do st ← save_ra … st pc ;
     76 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
     77 λ_.λ_.λst.
     78  do st ← push_ra … st (pc … st) ;
    7479  OK …
    7580   (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
     
    7782
    7883(*CSC: XXXX, for external functions only*)
    79 axiom ertl_fetch_external_args: external_function → state ERTL_state → res (list val).
     84axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
    8085axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
    8186(* I think there should be a list beval in place of list val here
     
    99104λp.list_to_pair … (bevals_of_pointer p) ?. % qed.
    100105
    101 definition get_hwsp : ERTL_state → res xpointer ≝
     106definition get_hwsp : state ERTL_state → res xpointer ≝
    102107 λst.
    103108  let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
     
    105110  xdata_pointer_of_address 〈spl,sph〉.
    106111
    107 definition set_hwsp : xpointer → ERTL_state → ERTL_state ≝
     112definition set_hwsp : xpointer → state ERTL_state → state ERTL_state ≝
    108113 λsp,st.
    109114  let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
     
    114119definition eval_ertl_seq:
    115120 ∀globals. genv ERTL globals →
    116   ertl_seq → joint_internal_function ERTL globals → ERTL_state →
    117    IO io_out io_in ERTL_state
    118  λglobals,ge,stm,curr_fn,st.
     121  ertl_seq → ident → joint_internal_function ERTL globals → state ERTL_state →
     122   IO io_out io_in (state ERTL_state)
     123 λglobals,ge,stm,id,curr_fn,st.
    119124 let framesize : Byte ≝ bitvector_of_nat 8 (joint_if_stacksize … curr_fn) in
    120125  match stm with
     
    151156  | _ ⇒ st].
    152157         
    153 
    154158definition ERTL_semantics ≝
    155159  make_sem_graph_params ERTL
    156   (mk_more_sem_unserialized_params ??
     160  (λF. mk_sem_unserialized_params ??
    157161  (* st_pars            ≝ *) ERTL_state
    158162  (* acca_store_        ≝ *) ps_reg_store
     
    170174  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
    171175  (* pair_reg_move_     ≝ *) ertl_eval_move
    172   (* fetch_ra           ≝ *) (load_ra …)
     176(*  (* fetch_ra           ≝ *) ?(*(pop_ra …)*) *)
    173177  (* allocate_local     ≝ *) ertl_allocate_local
    174178  (* save_frame         ≝ *) ertl_save_frame
     
    180184  (* read_result        ≝ *) (λ_.λ_.λ_.
    181185     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    182   (* eval_ext_seq       ≝ *) eval_ertl_seq
    183   (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    184   (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    185   (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
    186   (* post_op2           ≝ *) (λ_.λ_.ertl_post_op2)).
     186  (* eval_ext_seq       ≝ *) ?(*eval_ertl_seq*)
     187(*  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
     188  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) *)
     189  (* pop_frame          ≝ *) ?(*(λ_.λ_.?(*return st_no_pc ? st*))*)
     190(*  (* post_op2           ≝ *) (λ_.λ_.ertl_post_op2)) *)).
     191[ (* pop_frame *) cases daemon (* Handle last-popped correctly *)
     192| @eval_ertl_seq (* Handle type of call *)
     193]
Note: See TracChangeset for help on using the changeset viewer.