source: src/joint/semanticsUtils.ma @ 2536

Last change on this file since 2536 was 2529, checked in by tranquil, 8 years ago

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File size: 4.1 KB
RevLine 
[1299]1include "joint/semantics.ma".
[1359]2include alias "common/Identifiers.ma".
[2286]3include "utilities/hide.ma".
4include "ASM/BitVectorTrie.ma".
[1299]5
[2286]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 ≝
[2443]12  mk_hw_register_env (Stub …) BBundef.
[2286]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))
[2443]21  (other_bit env).
[2286]22
23definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
[2443]24λv,env.mk_hw_register_env (reg_env env) v.
[2286]25
[2443]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 …).
[2286]35
[2443]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
[1302]41(*** Store/retrieve on pseudo-registers ***)
[2286]42include alias "common/Identifiers.ma".
[1299]43
[2443]44record reg_sp : Type[0] ≝
45{ reg_sp_env :> identifier_map RegisterTag beval
46; stackp : xpointer
47}.
48
[1300]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
[2443]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
[1302]62(*** Store/retrieve on hardware registers ***)
63
[2286]64definition init_hw_register_env: xpointer → hw_register_env ≝
[2443]65 λsp.hwreg_store_sp empty_hw_register_env sp.
[1415]66
[2286]67(******************************** GRAPHS **************************************)
[1300]68
[2286]69definition make_sem_graph_params :
[2443]70  ∀pars : unserialized_params.
71  ∀g_pars : ∀F.sem_unserialized_params pars F.
[2286]72  sem_params ≝
[2443]73  λpars,spars.
74  let g_pars ≝ mk_graph_params pars in
[2286]75  mk_sem_params
[2443]76    g_pars
[2529]77    (spars ?)
78    (word_of_identifier ?)
79    (an_identifier ?)
80    ? (refl …).
[2470]81* #p % qed.
[2286]82
83(******************************** LINEAR **************************************)
84
[2470]85lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p.
86@pos_elim [%]
87#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
[2286]88
89definition make_sem_lin_params :
[2443]90  ∀pars : unserialized_params.
91  (∀F.sem_unserialized_params pars F) →
[2286]92  sem_params ≝
[2443]93  λpars,spars.
94  let lin_pars ≝ mk_lin_params pars in
[2286]95  mk_sem_params
[2443]96    lin_pars
[2529]97    (spars ?)
98    succ_pos_of_nat
99    (λp.pred (nat_of_pos p))
100    ??.
101[ #n >nat_succ_pos %
102| @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
[2470]103] qed.
[2529]104
105
106
107
108lemma fetch_statement_eq : ∀p:sem_params.∀g.
109  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
110  ∀i,fn,s.
111  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
112  let pt ≝ point_of_pc … ptr in
113  stmt_at … (joint_if_code … fn) pt = Some ? s →
114  fetch_statement … ge ptr = OK … 〈i, fn, s〉.
115#p #g #ge #ptr #i #f #s #EQ1 #EQ2
116whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
117>EQ2 %
118qed.
119
120lemma fetch_statement_inv : ∀p:sem_params.∀g.
121  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
122  ∀i,fn,s.
123  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
124  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧
125  let pt ≝ point_of_pc p ptr in
126  stmt_at … (joint_if_code … fn) pt = Some ? s.
127#p #g #ge #ptr #i #fn #s #H
128elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
129elim (bind_inversion ????? H) #s' * #H
130lapply (opt_eq_from_res ???? H) -H #EQ2
131whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
132qed.
133
Note: See TracBrowser for help on using the repository browser.