source: src/joint/semanticsUtils.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 4.1 KB
Line 
1include "joint/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    (spars ?)
78    (word_of_identifier ?)
79    (an_identifier ?)
80    ? (refl …).
81* #p % qed.
82
83(******************************** LINEAR **************************************)
84
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.
88
89definition make_sem_lin_params :
90  ∀pars : unserialized_params.
91  (∀F.sem_unserialized_params pars F) →
92  sem_params ≝
93  λpars,spars.
94  let lin_pars ≝ mk_lin_params pars in
95  mk_sem_params
96    lin_pars
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
103] qed.
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.