source: src/LIN/joint_LTL_LIN_semantics.ma @ 2760

Last change on this file since 2760 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 3.1 KB
Line 
1include "LIN/joint_LTL_LIN.ma".
2include "joint/semanticsUtils.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 … (BVByte 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 (BVByte v) e
20| int_to_acc _ v ⇒
21  hw_reg_store RegisterA (BVByte 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 (* load_sp ≝ *) hwreg_retrieve_sp
31 (* store_sp ≝ *) hwreg_store_sp.
32
33(*CSC: XXXX, for external functions only*)
34axiom ltl_lin_fetch_external_args: external_function → state LTL_LIN_state → res (list val).
35axiom ltl_lin_set_result: list val → unit → state LTL_LIN_state → res (state LTL_LIN_state).
36
37(* TODO (needs another bit to be added to hdw) *)
38axiom eval_ltl_lin_seq : ltl_lin_seq → state LTL_LIN_state → IO io_out io_in (state LTL_LIN_state).
39
40definition LTL_LIN_semantics ≝
41  λF.mk_sem_unserialized_params LTL_LIN F
42  (* st_pars            ≝ *) LTL_LIN_state
43  (* acca_store_        ≝ *) (λ_.hw_reg_store RegisterA)
44  (* acca_retrieve_     ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA)
45  (* acca_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA)
46  (* accb_store_        ≝ *) (λ_.hw_reg_store RegisterB)
47  (* accb_retrieve_     ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB)
48  (* accb_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB)
49  (* dpl_store_         ≝ *) (λ_.hw_reg_store RegisterDPL)
50  (* dpl_retrieve_      ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL)
51  (* dpl_arg_retrieve_  ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL)
52  (* dph_store_         ≝ *) (λ_.hw_reg_store RegisterDPH)
53  (* dph_retrieve_      ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH)
54  (* dph_arg_retrieve_  ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH)
55  (* snd_arg_retrieve_  ≝ *) hw_arg_retrieve
56  (* pair_reg_move_     ≝ *) eval_registers_move
57(*  (* fetch_ra           ≝ *) (load_ra …)
58  (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
59*)  (* save_frame         ≝ *) ?(*(λp.λ_.λst.save_ra … st p)*)
60  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
61  (* fetch_external_args≝ *) ?(*ltl_lin_fetch_external_args*)
62  (* set_result         ≝ *) ltl_lin_set_result
63  (* call_args_for_main ≝ *) 0
64  (* call_dest_for_main ≝ *) it
65  (* read_result        ≝ *) (λ_.λ_.λ_.
66  λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
67  (* eval_ext_seq       ≝ *) ?(*(λ_.λ_.λs.λ_.eval_ltl_lin_seq s)*)
68(*  (* eval_ext_tailcall  ≝ *) ?(*(λ_.λ_.λabs.match abs in void with [ ])*)
69  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
70*)  (* pop_frame          ≝ *) ?(*(λ_.λ_.λ_.λst.return st)*)
71(*  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)*).
Note: See TracBrowser for help on using the repository browser.