source: src/joint/semanticsUtils.ma @ 2645

Last change on this file since 2645 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: 4.1 KB
RevLine 
[2601]1include "joint/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]49definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
50
51definition reg_retrieve : register_env beval → register → res beval ≝
52 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
53
[2443]54definition reg_sp_store ≝ λreg,v,locals.
55! locals' ← reg_store reg v (reg_sp_env locals) ;
56return mk_reg_sp locals' (stackp locals).
57
58definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
59
[1302]60(*** Store/retrieve on hardware registers ***)
61
[2286]62definition init_hw_register_env: xpointer → hw_register_env ≝
[2443]63 λsp.hwreg_store_sp empty_hw_register_env sp.
[1415]64
[2286]65(******************************** GRAPHS **************************************)
[1300]66
[2286]67definition make_sem_graph_params :
[2443]68  ∀pars : unserialized_params.
69  ∀g_pars : ∀F.sem_unserialized_params pars F.
[2286]70  sem_params ≝
[2443]71  λpars,spars.
72  let g_pars ≝ mk_graph_params pars in
[2286]73  mk_sem_params
[2443]74    g_pars
[2529]75    (spars ?)
76    (word_of_identifier ?)
77    (an_identifier ?)
78    ? (refl …).
[2470]79* #p % qed.
[2286]80
81(******************************** LINEAR **************************************)
82
[2470]83lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p.
84@pos_elim [%]
85#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
[2286]86
87definition make_sem_lin_params :
[2443]88  ∀pars : unserialized_params.
89  (∀F.sem_unserialized_params pars F) →
[2286]90  sem_params ≝
[2443]91  λpars,spars.
92  let lin_pars ≝ mk_lin_params pars in
[2286]93  mk_sem_params
[2443]94    lin_pars
[2529]95    (spars ?)
96    succ_pos_of_nat
97    (λp.pred (nat_of_pos p))
98    ??.
99[ #n >nat_succ_pos %
100| @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
[2470]101] qed.
[2529]102
103
104
105
106lemma fetch_statement_eq : ∀p:sem_params.∀g.
107  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
108  ∀i,fn,s.
109  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
110  let pt ≝ point_of_pc … ptr in
111  stmt_at … (joint_if_code … fn) pt = Some ? s →
112  fetch_statement … ge ptr = OK … 〈i, fn, s〉.
113#p #g #ge #ptr #i #f #s #EQ1 #EQ2
114whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
115>EQ2 %
116qed.
117
118lemma fetch_statement_inv : ∀p:sem_params.∀g.
119  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
120  ∀i,fn,s.
121  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
122  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧
123  let pt ≝ point_of_pc p ptr in
124  stmt_at … (joint_if_code … fn) pt = Some ? s.
125#p #g #ge #ptr #i #fn #s #H
126elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
127elim (bind_inversion ????? H) #s' * #H
128lapply (opt_eq_from_res ???? H) -H #EQ2
129whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
130qed.
131
Note: See TracBrowser for help on using the repository browser.