source: src/LIN/joint_LTL_LIN_semantics.ma @ 3007

Last change on this file since 3007 was 2969, checked in by sacerdot, 8 years ago

Dead axiom removed :-)

File size: 3.9 KB
RevLine 
[1380]1include "LIN/joint_LTL_LIN.ma".
[2645]2include "joint/semanticsUtils.ma".
[1380]3
[1415]4definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
5definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
[2286]6definition hw_arg_retrieve ≝
7  λl,a.match a with
8  [ Reg r ⇒ hw_reg_retrieve l r
[2645]9  | Imm b ⇒ OK … (BVByte b)
[2286]10  ].
[1415]11
[2286]12definition eval_registers_move ≝ λe,m.
13match m with
14[ from_acc r _ ⇒
15  hw_reg_store r (hwreg_retrieve e RegisterA) e
16| to_acc _ r ⇒
17  hw_reg_store RegisterA (hwreg_retrieve e r) e
18| int_to_reg r v ⇒
[2645]19  hw_reg_store r (BVByte v) e
[2286]20| int_to_acc _ v ⇒
[2645]21  hw_reg_store RegisterA (BVByte v) e
[2286]22].
[1380]23
[2286]24definition LTL_LIN_state : sem_state_params ≝
25  mk_sem_state_params
26 (* framesT ≝ *) unit
27 (* empty_framesT ≝ *) it
28 (* regsT ≝ *) hw_register_env
[2443]29 (* empty_regsT ≝ *) init_hw_register_env
30 (* load_sp ≝ *) hwreg_retrieve_sp
31 (* store_sp ≝ *) hwreg_store_sp.
[1380]32
33(*CSC: XXXX, for external functions only*)
[2837]34axiom ltl_lin_fetch_external_args: external_function → state LTL_LIN_state → ℕ → res (list val).
[2286]35axiom ltl_lin_set_result: list val → unit → state LTL_LIN_state → res (state LTL_LIN_state).
[1380]36
[2783]37definition LTL_LIN_save_frame :
38call_kind → unit → state_pc LTL_LIN_state → res(state LTL_LIN_state) ≝
39λk.λ_.λst. match k with
40[ PTR ⇒ return (st_no_pc … st)
41| ID ⇒ push_ra … st (pc … st)
[2837]42].
[2783]43
[2837]44definition eval_LTL_LIN_ext_seq :
45 ∀F.∀globals.∀ge : genv_gen F globals.ltl_lin_seq → ident → state LTL_LIN_state → res (state LTL_LIN_state) ≝
46λF,globals,ge,s,curr_id,st.
47match s with
48[ SAVE_CARRY ⇒
49  let regs ≝ hwreg_set_other … (carry … st) (regs … st) in
50  return set_regs LTL_LIN_state regs st
51| RESTORE_CARRY ⇒
52  let carry ≝ other_bit (regs … st) in
53  return set_carry LTL_LIN_state carry st
[2956]54| LOW_ADDRESS r l ⇒  ! pc_lab ← gen_pc_from_label … ge curr_id l;
[2837]55                    let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
56                    let regs ≝ hwreg_store r addrl (regs … st) in
57                    return set_regs LTL_LIN_state regs st
[2956]58| HIGH_ADDRESS r l ⇒ ! pc_lab ← gen_pc_from_label … ge curr_id l;
[2837]59                    let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
60                    let regs ≝ hwreg_store r addrh (regs … st) in
61                    return set_regs LTL_LIN_state regs st
62].
63
[2286]64definition LTL_LIN_semantics ≝
[2443]65  λF.mk_sem_unserialized_params LTL_LIN F
[2286]66  (* st_pars            ≝ *) LTL_LIN_state
67  (* acca_store_        ≝ *) (λ_.hw_reg_store RegisterA)
68  (* acca_retrieve_     ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA)
69  (* acca_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA)
70  (* accb_store_        ≝ *) (λ_.hw_reg_store RegisterB)
71  (* accb_retrieve_     ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB)
72  (* accb_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB)
73  (* dpl_store_         ≝ *) (λ_.hw_reg_store RegisterDPL)
74  (* dpl_retrieve_      ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL)
75  (* dpl_arg_retrieve_  ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL)
76  (* dph_store_         ≝ *) (λ_.hw_reg_store RegisterDPH)
77  (* dph_retrieve_      ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH)
78  (* dph_arg_retrieve_  ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH)
79  (* snd_arg_retrieve_  ≝ *) hw_arg_retrieve
80  (* pair_reg_move_     ≝ *) eval_registers_move
[2645]81(*  (* fetch_ra           ≝ *) (load_ra …)
[2286]82  (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
[2783]83*)  (* save_frame         ≝ *) LTL_LIN_save_frame
[2286]84  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
[2837]85  (* fetch_external_args≝ *) ltl_lin_fetch_external_args
[2286]86  (* set_result         ≝ *) ltl_lin_set_result
87  (* call_args_for_main ≝ *) 0
88  (* call_dest_for_main ≝ *) it
89  (* read_result        ≝ *) (λ_.λ_.λ_.
90  λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
[2837]91  (* eval_ext_seq       ≝ *) (eval_LTL_LIN_ext_seq ?)
92  (* pop_frame          ≝ *) ((λ_.λ_.λ_.λ_.λst.pop_ra … st)).
Note: See TracBrowser for help on using the repository browser.