source: src/LIN/joint_LTL_LIN_semantics_paolo.ma @ 2233

Last change on this file since 2233 was 2233, checked in by tranquil, 7 years ago
  • completed update of ERTL semantics
  • some minor changes in joint semantics
File size: 3.0 KB
Line 
1include "LIN/joint_LTL_LIN_paolo.ma".
2include "joint/semanticsUtils_paolo.ma".
3
4definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
5definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
6definition hw_arg_retrieve ≝
7  λl,a.match a with
8  [ Reg r ⇒ hw_reg_retrieve l r
9  | Imm b ⇒ OK … b
10  ].
11
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 ⇒
19  hw_reg_store r v e
20| int_to_acc _ v ⇒
21  hw_reg_store RegisterA v e
22].
23
24definition 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*)
32axiom ltl_lin_fetch_external_args: external_function → state LTL_LIN_state → res (list val).
33axiom 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) *)
36axiom eval_ltl_lin_seq : ltl_lin_seq → state LTL_LIN_state → IO io_out io_in (state LTL_LIN_state).
37
38definition 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).
Note: See TracBrowser for help on using the repository browser.