- Timestamp:
- Feb 7, 2013, 9:22:22 PM (8 years ago)
- Location:
- src/LIN
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/joint_LTL_LIN.ma
r2537 r2645 36 36 (* ext_seq_labels ≝ *) ltl_lin_seq_labels 37 37 (* has_tailcalls ≝ *) false 38 (* paramsT ≝ *) unit 39 (* localsT ≝ *) void. 38 (* paramsT ≝ *) unit. 40 39 41 40 interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)). -
src/LIN/joint_LTL_LIN_semantics.ma
r2443 r2645 1 1 include "LIN/joint_LTL_LIN.ma". 2 include "joint/ SemanticUtils.ma".2 include "joint/semanticsUtils.ma". 3 3 4 4 definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e). … … 7 7 λl,a.match a with 8 8 [ Reg r ⇒ hw_reg_retrieve l r 9 | Imm b ⇒ OK … b9 | Imm b ⇒ OK … (BVByte b) 10 10 ]. 11 11 … … 17 17 hw_reg_store RegisterA (hwreg_retrieve e r) e 18 18 | int_to_reg r v ⇒ 19 hw_reg_store r ve19 hw_reg_store r (BVByte v) e 20 20 | int_to_acc _ v ⇒ 21 hw_reg_store RegisterA ve21 hw_reg_store RegisterA (BVByte v) e 22 22 ]. 23 23 … … 55 55 (* snd_arg_retrieve_ ≝ *) hw_arg_retrieve 56 56 (* pair_reg_move_ ≝ *) eval_registers_move 57 (* fetch_ra ≝ *) (load_ra …)57 (* (* fetch_ra ≝ *) (load_ra …) 58 58 (* allocate_local ≝ *) (λabs.match abs in void with [ ]) 59 (* save_frame ≝ *) (λp.λ_.λst.save_ra … st p)59 *) (* save_frame ≝ *) ?(*(λp.λ_.λst.save_ra … st p)*) 60 60 (* setup_call ≝ *) (λ_.λ_.λ_.λst.return st) 61 (* fetch_external_args≝ *) ltl_lin_fetch_external_args61 (* fetch_external_args≝ *) ?(*ltl_lin_fetch_external_args*) 62 62 (* set_result ≝ *) ltl_lin_set_result 63 63 (* call_args_for_main ≝ *) 0 … … 65 65 (* read_result ≝ *) (λ_.λ_.λ_. 66 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 [ ])67 (* eval_ext_seq ≝ *) ?(*(λ_.λ_.λs.λ_.eval_ltl_lin_seq s)*) 68 (* (* eval_ext_tailcall ≝ *) ?(*(λ_.λ_.λabs.match abs in void with [ ])*) 69 69 (* eval_ext_call ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) 70 (* pop_frame ≝ *) (λ_.λ_.λ_.λst.return st)71 (* post_op2 ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st).70 *) (* pop_frame ≝ *) ?(*(λ_.λ_.λ_.λst.return st)*) 71 (* (* post_op2 ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)*).
Note: See TracChangeset
for help on using the changeset viewer.