source: src/LIN/joint_LTL_LIN_semantics.ma @ 1784

Last change on this file since 1784 was 1451, checked in by sacerdot, 10 years ago
  1. All axioms in LIN/semantics.ma closed
  2. succ_pc and pointer_of_label moved to more_sem_params1; their type have been changed too to implement LIN/semantics.ma
File size: 3.5 KB
RevLine 
[1380]1include "LIN/joint_LTL_LIN.ma".
2include "joint/SemanticUtils.ma".
3
[1415]4definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
5definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
6
[1451]7definition ltl_lin_more_sem_params: ∀succT. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
8 λsuccT.
[1380]9 mk_more_sem_params ?
[1451]10  unit it hw_register_env init_hw_register_env 0 it
[1415]11   hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA)
12    (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB)
13    (λ_.hw_reg_store RegisterDPL) (λe.λ_.hw_reg_retrieve e RegisterDPL)
14    (λ_.hw_reg_store RegisterDPH) (λe.λ_.hw_reg_retrieve e RegisterDPH)
[1380]15     (λlocals,dest_src.
16       match dest_src with
17       [ from_acc reg ⇒
[1415]18          do v ← hw_reg_retrieve locals RegisterA ;
19          hw_reg_store reg v locals
[1380]20       | to_acc reg ⇒
[1415]21          do v ← hw_reg_retrieve locals reg ;
[1451]22          hw_reg_store RegisterA v locals ]).
[1380]23
[1451]24definition ltl_lin_sem_params: ∀succT. sem_params ≝
25 λsuccT.mk_sem_params … (ltl_lin_more_sem_params succT).
[1380]26
[1383]27
[1380]28definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
29definition ltl_lin_pop_frame:
[1451]30 ∀succT,codeT,lookup.
[1385]31 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
[1451]32 state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝
33 λ_.λ_.λ_.λ_.λ_.λt.OK … t.
[1380]34definition ltl_lin_save_frame:
[1451]35 ∀succT. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝
36 λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
[1380]37
[1390]38(* The following implementation only works for functions that return 32 bits *)
39definition ltl_lin_result_regs:
[1451]40 ∀succT,codeT,lookup.
[1385]41 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
[1451]42 state (ltl_lin_sem_params succT) → res (list Register) ≝
43 λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets.
[1380]44
45(*CSC: XXXX, for external functions only*)
[1451]46axiom ltl_lin_fetch_external_args: ∀succT.external_function → state (ltl_lin_sem_params succT) → res (list val).
47axiom ltl_lin_set_result: ∀succT.list val → state (ltl_lin_sem_params succT) → res (state (ltl_lin_sem_params succT)).
[1380]48
[1451]49definition ltl_lin_exec_extended: ∀succT.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT) → IO io_out io_in (trace × (state (ltl_lin_sem_params succT)))
50 ≝ λsuccT,p,globals,ge,abs. ⊥.
[1380]51@abs qed.
52
53definition ltl_lin_more_sem_params2:
[1451]54 ∀succT,codeT,lookup.∀succ: succT → address → res address.∀fetch.
55 ∀pointer_of_label: ∀globals. genv globals
56  (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals))
57  →pointer→label→res (Σp0:pointer.ptype p0=Code).
[1380]58 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
[1451]59 λsuccT,codeT,lookup,succ,fetch,pointer_of_label,globals.
[1411]60  mk_more_sem_params2 …
[1451]61   (mk_more_sem_params1 … (ltl_lin_more_sem_params …)
62    succ (pointer_of_label …) (fetch globals) (load_ra …) (ltl_lin_result_regs …)
[1411]63    ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
64    (ltl_lin_fetch_external_args …) (ltl_lin_set_result …)) (ltl_lin_exec_extended …).
[1380]65
66definition ltl_lin_fullexec ≝
[1451]67 λsuccT,codeT,lookup,succ,fetch,pointer_of_label.
68  joint_fullexec … (λp. ltl_lin_more_sem_params2 succT codeT lookup succ fetch pointer_of_label (prog_var_names … p)).
Note: See TracBrowser for help on using the repository browser.