| 1 | include "LIN/joint_LTL_LIN.ma". |
|---|
| 2 | include "joint/SemanticUtils.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 … 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 v e |
|---|
| 20 | | int_to_acc _ v ⇒ |
|---|
| 21 | hw_reg_store RegisterA 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 | |
|---|
| 31 | (*CSC: XXXX, for external functions only*) |
|---|
| 32 | axiom ltl_lin_fetch_external_args: external_function → state LTL_LIN_state → res (list val). |
|---|
| 33 | axiom ltl_lin_set_result: list val → unit → state LTL_LIN_state → res (state LTL_LIN_state). |
|---|
| 34 | |
|---|
| 35 | (* TODO (needs another bit to be added to hdw) *) |
|---|
| 36 | axiom eval_ltl_lin_seq : ltl_lin_seq → state LTL_LIN_state → IO io_out io_in (state LTL_LIN_state). |
|---|
| 37 | |
|---|
| 38 | definition LTL_LIN_semantics ≝ |
|---|
| 39 | λF.mk_more_sem_unserialized_params LTL_LIN F |
|---|
| 40 | (* st_pars ≝ *) LTL_LIN_state |
|---|
| 41 | (* acca_store_ ≝ *) (λ_.hw_reg_store RegisterA) |
|---|
| 42 | (* acca_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA) |
|---|
| 43 | (* acca_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA) |
|---|
| 44 | (* accb_store_ ≝ *) (λ_.hw_reg_store RegisterB) |
|---|
| 45 | (* accb_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB) |
|---|
| 46 | (* accb_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB) |
|---|
| 47 | (* dpl_store_ ≝ *) (λ_.hw_reg_store RegisterDPL) |
|---|
| 48 | (* dpl_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL) |
|---|
| 49 | (* dpl_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL) |
|---|
| 50 | (* dph_store_ ≝ *) (λ_.hw_reg_store RegisterDPH) |
|---|
| 51 | (* dph_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH) |
|---|
| 52 | (* dph_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH) |
|---|
| 53 | (* snd_arg_retrieve_ ≝ *) hw_arg_retrieve |
|---|
| 54 | (* pair_reg_move_ ≝ *) eval_registers_move |
|---|
| 55 | (* fetch_ra ≝ *) (load_ra …) |
|---|
| 56 | (* allocate_local ≝ *) (λabs.match abs in void with [ ]) |
|---|
| 57 | (* save_frame ≝ *) (λp.λ_.λst.save_ra … st p) |
|---|
| 58 | (* setup_call ≝ *) (λ_.λ_.λ_.λst.return st) |
|---|
| 59 | (* fetch_external_args≝ *) ltl_lin_fetch_external_args |
|---|
| 60 | (* set_result ≝ *) ltl_lin_set_result |
|---|
| 61 | (* call_args_for_main ≝ *) 0 |
|---|
| 62 | (* call_dest_for_main ≝ *) it |
|---|
| 63 | (* read_result ≝ *) (λ_.λ_.λ_. |
|---|
| 64 | λst.return map … (hwreg_retrieve (regs … st)) RegisterRets) |
|---|
| 65 | (* eval_ext_seq ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s) |
|---|
| 66 | (* eval_ext_tailcall ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) |
|---|
| 67 | (* eval_ext_call ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) |
|---|
| 68 | (* pop_frame ≝ *) (λ_.λ_.λ_.λst.return st) |
|---|
| 69 | (* post_op2 ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st). |
|---|
