source: src/joint/semanticsUtils.ma @ 2470

Last change on this file since 2470 was 2470, checked in by tranquil, 7 years ago

completely separated program counters from code pointers in joint languages: the advantage is program counters with an unbounded offset in Pos

File size: 3.2 KB
Line 
1include "joint/semantics.ma".
2include alias "common/Identifiers.ma".
3include "utilities/hide.ma".
4include "ASM/BitVectorTrie.ma".
5
6record hw_register_env : Type[0] ≝
7  { reg_env : BitVectorTrie beval 6
8  ; other_bit : bebit
9  }.
10
11definition empty_hw_register_env: hw_register_env ≝
12  mk_hw_register_env (Stub …) BBundef.
13
14include alias "ASM/BitVectorTrie.ma".
15
16definition hwreg_retrieve: hw_register_env → Register → beval ≝
17 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
18
19definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
20 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
21  (other_bit env).
22
23definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
24λv,env.mk_hw_register_env (reg_env env) v.
25
26definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝
27λenv.
28let spl ≝ hwreg_retrieve env RegisterSPL in
29let sph ≝ hwreg_retrieve env RegisterSPH in
30! ptr ← pointer_of_address 〈spl, sph〉 ;
31match ptype ptr return λx.ptype ptr = x → res xpointer with
32[ XData ⇒ λprf.return «ptr, prf»
33| _ ⇒ λ_.Error … [MSG BadPointer]
34] (refl …).
35
36definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝
37λenv,sp.
38let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in
39hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
40
41(*** Store/retrieve on pseudo-registers ***)
42include alias "common/Identifiers.ma".
43
44record reg_sp : Type[0] ≝
45{ reg_sp_env :> identifier_map RegisterTag beval
46; stackp : xpointer
47}.
48
49axiom BadRegister : String.
50
51definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
52
53definition reg_retrieve : register_env beval → register → res beval ≝
54 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
55
56definition reg_sp_store ≝ λreg,v,locals.
57! locals' ← reg_store reg v (reg_sp_env locals) ;
58return mk_reg_sp locals' (stackp locals).
59
60definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
61
62(*** Store/retrieve on hardware registers ***)
63
64definition init_hw_register_env: xpointer → hw_register_env ≝
65 λsp.hwreg_store_sp empty_hw_register_env sp.
66
67(******************************** GRAPHS **************************************)
68
69definition make_sem_graph_params :
70  ∀pars : unserialized_params.
71  ∀g_pars : ∀F.sem_unserialized_params pars F.
72  sem_params ≝
73  λpars,spars.
74  let g_pars ≝ mk_graph_params pars in
75  mk_sem_params
76    g_pars
77    (mk_more_sem_params
78      g_pars
79      (spars ?)
80      (word_of_identifier ?)
81      (an_identifier ?)
82      ? (refl …)
83    ).
84* #p % qed.
85
86(******************************** LINEAR **************************************)
87
88lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p.
89@pos_elim [%]
90#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
91
92
93definition make_sem_lin_params :
94  ∀pars : unserialized_params.
95  (∀F.sem_unserialized_params pars F) →
96  sem_params ≝
97  λpars,spars.
98  let lin_pars ≝ mk_lin_params pars in
99  mk_sem_params
100    lin_pars
101    (mk_more_sem_params
102      lin_pars
103      (spars ?)
104      succ_pos_of_nat
105      (λp.pred (nat_of_pos p))
106      ??
107    ).
108[ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
109| #n >nat_succ_pos %
110] qed.
Note: See TracBrowser for help on using the repository browser.