source: src/joint/BEMem.ma @ 2286

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

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File size: 7.6 KB
Line 
1(* Memory model used in the dynamic semantics of the back-end intermediate
2   languages. Inspired by common/Mem.ma, adapted from Compcert *)
3
4(* * This file develops the memory model that is used in the dynamic
5  semantics of all the languages used in the compiler.
6  It defines a type [mem] of memory states, the following 4 basic
7  operations over memory states, and their properties:
8- [load]: read a memory chunk at a given address;
9- [store]: store a memory chunk at a given address;
10- [alloc]: allocate a fresh memory block;
11- [free]: invalidate a memory block.
12*)
13
14include "common/ByteValues.ma".
15include "common/GenMem.ma".
16
17definition bemem ≝ mem.
18
19definition is_addressable : region → bool ≝ λr.match r with
20  [ XData ⇒ true | Code ⇒ true | _ ⇒ false ].
21
22definition is_address : (beval × beval) → Prop ≝ λa.
23  ∃b : Σb.bool_to_Prop (is_addressable (block_region b)).
24  ∃p0,p1,o0,o1.
25    \fst a = BVptr b p0 o0 ∧ part_no … p0 = 0 ∧
26    \snd a = BVptr b p1 o1 ∧ part_no … p1 = 1 ∧
27    bool_to_Prop (vsuffix … (eq_bv 8) o0 o1).
28
29(*
30definition is_addressb : (beval × beval) → bool ≝ λa.
31  let 〈a0,a1〉 ≝ a in
32  match a0 with
33  [ BVptr b0 part0 o0 ⇒
34      is_addressable (block_region b0) ∧ eqb part0 0 ∧
35        match a1 with
36        [ BVptr b1 part1 o1 ⇒
37          eq_block b0 b1 ∧ eqb part1 1 ∧ subvector_with … (eq_bv 8) o0 o1
38        | _ ⇒ false
39        ]
40  | _ ⇒ false
41  ].
42
43lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval.
44  (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
45#P * * [||#b0|(*#r0*)#part0|#b0#part0#o0] #a1
46[5: whd in match is_addressb; normalize nodelta
47  elim (true_or_false_Prop (is_addressable (block_region b0)))
48  #H >H
49  [ @(eqb_elim part0 0) #Heq
50    [ cases a1 [||#b1|(*#r1*)#part1|#b1#part1#o1] whd in match (?∧?);
51      [5: @eq_block_elim #Heq'
52        [ @(eqb_elim part1 1) #Heq''
53          [ elim (true_or_false_Prop (subvector_with … (eq_bv 8) o0 o1)) #Heq''' >Heq'''
54            [ #Ptrue #_ @Ptrue destruct
55              %{b1} [assumption] %{part0} %{part1} %{o0} %{o1}
56              % [ % [ % [ % ]]] try assumption %
57            ]
58          ]
59        ]
60      ]
61    ]
62  ]
63]
64#_ #Pfalse @Pfalse % ** #b0' #H' * #part0' * #part1' * #o0' * #o1' ****
65#H0 #H1 #H2 #H3 #H4 destruct /2 by absurd/
66qed.
67*)
68
69(* CSC: only pointers to XRAM or code memory ATM *)
70definition address ≝ beval × beval.
71
72(* definition safe_address ≝ Sig address is_address.
73unification hint 0 ≔ ;
74P ≟ Prod beval beval
75(*------------------*)⊢
76safe_address ≡ Sig P is_address. *)
77
78definition eq_address: address → address → bool ≝
79 λaddr1,addr2.
80  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
81
82definition pointer_of_address: address → res pointer ≝
83 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
84
85lemma bevals_of_pointer_is_address :
86  ∀p.is_address (list_to_pair … (bevals_of_pointer p) (refl …)).
87* #b * #o whd in ⊢ (?%); whd
88%{b} [ elim (block_region b) % ] %{(mk_part 0 ?)} [ %2 %1 ] %{(mk_part 1 ?)} [ %1 ]
89@(vsplit_elim … 8 8 o) #o1 #o0 #EQ >EQ -o
90%{[[o0]]} %{[[o1;o0]]}
91% [2: change with (bool_to_Prop (if eq_bv ??? then ? else ?))
92      >eq_bv_refl % ]
93%%[2: normalize nodelta @vsplit_elim #pre >(Vector_O … pre) #post #EQ
94      normalize in EQ; <EQ -pre -post
95      whd in match (rvsplit ????);
96      <(vsplit_prod … (refl …)) normalize nodelta
97  | % [2: % ]
98  ]
99whd in match (rvsplit ????);
100try <(vector_append_empty … o0) in ⊢ (??%?);
101<(vsplit_prod … (refl …)) normalize nodelta %
102qed.
103
104lemma is_address_to_pointer : ∀a.is_address a → ∃p.pointer_of_address a = return p.
105* #a0 #a1 ** #bl #bl_prf ** #p0 #p0_prf ** #p1 #p1_prf * #o0' * #o1o0 ****
106#EQ1 #EQ2 #EQ3 #EQ4 destruct
107@(Vector_pair_elim … o1o0) #o1 #o0 #EQ >EQ -o1o0
108@(Vector_singl_elim … o0') #o0'' #EQ >EQ -o0'
109whd in ⊢ (?%→?);
110@eq_bv_elim #EQ * >EQ -o0''
111whd in match (pointer_of_address ?);
112>eq_block_b_b >(eqb_n_n 1)
113>vsuffix_vflatten
114[2: change with (bool_to_Prop (vsuffix ????? ([[?]]@@[[?]])))
115  @vsuffix_true change with (bool_to_Prop (if eq_bv ? o0 o0 then ? else ?))
116  >eq_bv_refl % ]
117normalize nodelta
118whd in ⊢ (??(λ_.??%?));
119% [2: % |]
120qed.
121
122(* For full 8051 memory spaces
123definition pointer_compat' ≝ λb,r.
124  match b with
125  [ mk_block r' z ⇒
126    if eq_region r' r then True
127    else
128      match r with
129      [ Any ⇒ True
130      | XData ⇒ match r' with
131        [ PData ⇒ True
132        | _ ⇒ False
133        ]
134      | _ ⇒ False
135      ]
136   ].
137
138lemma pointer_compat_to_ind : ∀b,r.pointer_compat' b r → pointer_compat b r.
139** #z ** //
140qed.
141
142lemma pointer_compat_from_ind : ∀b,r.pointer_compat b r → pointer_compat' b r.
143#b #r #H inversion H
144[ #s #id #EQ1 #EQ2 #EQ3 whd >reflexive_eq_region %
145| #id #EQ1 #EQ2 #EQ3 %
146| #r #id #EQ1 #EQ2 #EQ3 whd @eq_region_elim #EQ4 destruct(EQ4) %
147]
148qed.
149*)
150(*lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
151** #a0 #a1 ***** #z #o
152#Hr
153(*
154** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr)
155cases r in Hr ⊢ %; #Hr *
156*)
157** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1
158destruct normalize
159@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
160change with (eq_bv ???) in match (eq_v ?????);
161@eq_bv_elim [2,4,6: * #ABS elim (ABS (refl …))]
162#_ #_ normalize %
163qed.*)
164   
165definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer.
166
167example address_of_pointer_OK_to_safe :
168  ∀p,a.address_of_pointer p = OK … a → is_address a.
169#p #a whd in match address_of_pointer; normalize nodelta
170#EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
171//
172qed.
173
174(*definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
175  do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».
176
177lemma address_of_pointer_is_safe :
178  ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address).
179#p normalize % qed.
180(*
181****#z #H
182lapply (pointer_compat_from_ind ?? H) * #o
183normalize %
184qed.*)
185
186definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝
187code_pointer_of_beval_pair.
188
189definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.
190
191definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer.
192cases H -H * #b #o normalize cases b * #z #EQ destruct
193%{«mk_pointer  (mk_block Code z)  o,I»}
194% [2: % [2: % [ % [ % ]]]] %
195qed.
196(*
197cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
198lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
199%{«mk_pointer ? (mk_block Code z) H o,I»}
200% [2: % [2: % [ % [ % ]] % |]|]
201qed.*)
202*)
203
204(* Paolo: why only code pointers and not XRAM too? *)
205(*definition addr_add: address → nat → res address ≝
206 λaddr,n.
207  do ptr ← code_pointer_of_address addr ;
208  OK … (address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
209normalize cases ptr #p #E @E
210qed.
211
212definition safe_addr_add: safe_address → nat → res safe_address ≝
213 λaddr,n.
214  do ptr ← code_pointer_of_address addr ;
215  OK … (safe_address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
216normalize cases ptr #p #E @E
217qed.
218
219definition addr_sub: address → nat → res address ≝
220 λaddr,n.
221  do ptr ← code_pointer_of_address addr ;
222  OK … (address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
223normalize cases ptr #p #E @E
224qed.
225
226definition safe_addr_sub: safe_address → nat → res safe_address ≝
227 λaddr,n.
228  do ptr ← code_pointer_of_address addr ;
229  OK … (safe_address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
230normalize cases ptr #p #E @E
231qed.
232*)
Note: See TracBrowser for help on using the repository browser.