Changeset 2783 for src/ERTLptr


Ignore:
Timestamp:
Mar 6, 2013, 12:09:52 PM (8 years ago)
Author:
piccolo
Message:

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

Location:
src/ERTLptr
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptr.ma

    r2674 r2783  
    2424    (* has_tailcall ≝ *) false
    2525    (* paramsT ≝ *) ℕ.
     26   
     27definition ERTLptr_functs ≝ mk_get_pseudo_reg_functs ERTLptr_uns
     28(* acc_a_regs *) (λr.[r])
     29(* acc_b_regs *) (λr.[r])
     30(* acc_a_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
     31(* acc_b_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
     32(* dpl_regs *) (λr.[r])
     33(* dph_regs *) (λr.[r])
     34(* dpl_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
     35(* dph_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
     36(* snd_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
     37(* pair_move_regs *) (λx.(regs_from_move_dst (\fst x)) @ (regs_from_move_src (\snd x)))
     38(* f_call_args *) (λ_.[ ])
     39(* f_call_dest *) (λ_.[ ])
     40(* ext_seq_regs *)
     41  (λs.match s with [ LOW_ADDRESS r _ ⇒ [r]
     42                   | HIGH_ADDRESS r _ ⇒ [r]
     43                   | ertlptr_ertl s' ⇒ ertl_ext_seq_regs s'
     44                   ])
     45(* params_regs *) (λ_.[ ]).
    2646
    27 definition ERTLptr ≝ mk_graph_params ERTLptr_uns.
     47definition ERTLptr ≝ mk_graph_params (mk_uns_params ERTLptr_uns ERTLptr_functs).
    2848definition ertlptr_program ≝ joint_program ERTLptr.
    2949 
  • src/ERTLptr/ERTLptr_semantics.ma

    r2666 r2783  
    55
    66definition ertlptr_save_frame:
    7  call_kind → unit → ident → state_pc ERTL_state → res (state … ERTL_state) ≝
    8  λk.λ_.λid.λst.
    9  do st ← match k with [ID ⇒ push_ra … st (pc … st) |
    10  PTR ⇒ return (st_no_pc … st)] ; OK …
    11    (set_frms ERTL_state (〈\fst (regs ERTL_state st),id〉 :: (st_frms … st))
    12     (set_regs ERTL_state 〈empty_map …,\snd (regs … st)〉 st)).
     7 call_kind → unit  → state_pc ERTL_state → res (state … ERTL_state) ≝
     8 λk.λ_.λst.
     9 ! st' ← match k with
     10  [ ID ⇒ push_ra … st (pc … st)
     11  | PTR ⇒ return (st : state ?)
     12  ] ;
     13 ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
     14  return
     15   (set_frms ERTL_state (〈\fst (regs ERTL_state st'), pc_block (pc … st)〉 :: frms)
     16    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
    1317
    1418definition eval_ertlptr_seq:
     
    5357     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    5458  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertlptr_seq F gl ge stm id)
    55   (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …).
     59  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
     60 
    5661definition ERTLptr_semantics ≝
    57   make_sem_graph_params ERTLptr ERTLptr_sem_uns.
     62  mk_sem_graph_params ERTLptr ERTLptr_sem_uns.
Note: See TracChangeset for help on using the changeset viewer.