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