source: src/common/ByteValues.ma

Last change on this file was 3259, checked in by piccolo, 7 years ago

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

File size: 12.7 KB
Line 
1(* Type of values used in the dynamic semantics of the back-end intermediate
2   languages, and the memory model for the whole compiler. Inspired by
3   common/Values.ma, adapted from Compcert *)
4
5include "common/Pointers.ma".
6include "utilities/hide.ma".
7
8
9definition cpointer ≝ Σp.ptype p = Code.
10definition xpointer ≝ Σp.ptype p = XData.
11unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
12unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
13
14
15(* this is like a code pointer, but with unbounded offset.
16   used only in the back-end, they become code pointers in LIN → ASM *)
17record program_counter : Type[0] ≝
18  { pc_block : Σb : block.block_region b = Code
19  ; pc_offset : Pos
20  }.
21
22definition eq_program_counter : program_counter → program_counter → bool ≝
23λpc1,pc2.eq_block (pc_block pc1) (pc_block pc2) ∧
24         eqb (pc_offset pc1) (pc_offset pc2).
25
26lemma eq_program_counter_elim : ∀P:bool→Prop.
27  ∀pc1,pc2.(pc1=pc2→P true)→(pc1≠pc2→P false)→P (eq_program_counter pc1 pc2).
28#P ** #bl1 #H1 #o1 ** #bl2 #H2 #o2
29#Heq #Hneq whd in ⊢ (?%);
30@eq_block_elim #EQ1
31[ @eqb_elim #EQ2 ]
32[ @Heq destruct %
33|*: @Hneq % #ABS destruct
34  [ @(absurd ?? EQ2) | @(absurd ?? EQ1) ] %
35] qed.
36
37lemma reflexive_eq_program_counter : ∀pc.eq_program_counter pc pc = true.
38** #bl1 #H1 #o1 whd in ⊢ (??%?); >eq_block_b_b >eqb_n_n % qed.
39
40definition bitvector_from_pos :
41  ∀n.Pos → BitVector n ≝
42  λn,p.bitvector_of_Z n (Zpred (pos p)).
43
44definition pos_from_bitvector :
45  ∀n.BitVector n → Pos ≝
46  λn,v.
47  match Zsucc (Z_of_unsigned_bitvector n v)
48  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
49  with
50  [ OZ ⇒ λprf.⊥
51  | pos x ⇒ λ_. x
52  | neg x ⇒ λprf.⊥
53  ] (refl …).
54@hide_prf
55elim v in prf;
56[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
57
58definition cpointer_of_pc : program_counter → option cpointer ≝
59  λpc.
60  let pc_off ≝ pc_offset pc in
61  if leb pc_off (two_power_nat offset_size) then
62    return «mk_pointer (pc_block pc) (mk_offset (bitvector_from_pos … pc_off)),?»
63  else
64    None ?.
65elim (pc_block pc) #bl #H @H qed.
66
67record part (*r: region*): Type[0] ≝
68 { part_no:> nat
69 ; part_no_ok: part_no < size_pointer (*r*)
70 }.
71
72definition part_from_sig : (Σn:ℕ.n<size_pointer) → part ≝
73λn_sig : Σn.n<size_pointer.mk_part n_sig (pi2 … n_sig).
74
75coercion sig_to_part : ∀n_sig:Σn:ℕ.n<size_pointer.part ≝
76part_from_sig on _n_sig:Σn.n<size_pointer to part.
77
78(* Byte-sized values used in the back-end.
79   Values larger than a single Byte are represented via their parts.
80   Values are either:
81  - machine integers (Bytes)
82  - parts of a pointer seen as a triple giving the representation of the
83    pointer (in terms of the memory regions such a pointer could address),
84    a memory address and an integer offset with respect to this address;
85  - a null pointer: the region denotes the pointer size
86  - the [BVundef] value denoting an arbitrary bit pattern, such as the
87    value of an uninitialized variable
88  - [BVXor] is a formal XOR between (possibly null) pointer parts
89  - [BVnonzero] is any nonzero value
90*)
91
92inductive beval: Type[0] ≝
93  | BVundef: beval
94  | BVnonzero: beval
95  | BVXor: option pointer → option pointer → part → beval (* option pointer ≈ pointer + null *)
96  | BVByte: Byte → beval
97  | BVnull: (*∀r:region.*) part  → beval
98  | BVptr: pointer → part → beval
99  | BVpc: program_counter → part → beval. (* only used in back end, needed to separate
100                                      program counters that go in the stack from
101                                      function pointers, as they are linked with
102                                      different relations in some passes *)
103
104definition eq_bv_suffix : ∀n,m,p.
105  BitVector (n + p) → BitVector (m + p) → bool ≝
106λn,m,p,v1,v2.
107let b1 ≝ \snd (vsplit … v1) in
108let b2 ≝ \snd (vsplit … v2) in
109eq_bv … b1 b2.
110
111include alias "arithmetics/nat.ma".
112
113(* CSC: use vectors in place of lists? Or even better products of tuples
114   (more easily pattern matchable in the finite case)? requires one more parameter *)
115definition pointer_of_bevals: list beval → res pointer ≝
116 λl.
117 match l with
118  [ nil ⇒ Error … [MSG CorruptedPointer]
119  | cons bv1 tl ⇒
120    match tl with
121    [ nil ⇒ Error … [MSG CorruptedPointer]
122    | cons bv2 tl' ⇒
123      match tl' with
124      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
125      | nil ⇒
126        match bv1 with
127        [ BVptr ptr1 p1 ⇒
128          match bv2 with
129          [ BVptr ptr2 p2 ⇒
130            if eqb p1 0 ∧ eqb p2 1 ∧ eq_block (pblock ptr1) (pblock ptr2) ∧
131               eq_bv_suffix 8 8 8 (offv (poff ptr1)) (offv (poff ptr2))
132            then
133              return ptr2
134            else Error … [MSG CorruptedPointer]
135          | _ ⇒ Error … [MSG CorruptedPointer]
136          ]
137        | _ ⇒ Error … [MSG CorruptedPointer]
138        ]
139      ]
140    ]
141  ].
142
143definition pc_of_bevals: list beval → res program_counter ≝
144 λl.
145 match l with
146  [ nil ⇒ Error … [MSG CorruptedPointer]
147  | cons bv1 tl ⇒
148    match tl with
149    [ nil ⇒ Error … [MSG CorruptedPointer]
150    | cons bv2 tl' ⇒
151      match tl' with
152      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
153      | nil ⇒
154        match bv1 with
155        [ BVpc ptr1 p1 ⇒
156          match bv2 with
157          [ BVpc ptr2 p2 ⇒
158            if eqb p1 0 ∧ eqb p2 1 ∧ eq_program_counter ptr1 ptr2 then
159              return ptr2
160            else Error … [MSG CorruptedPointer]
161          | _ ⇒ Error … [MSG CorruptedPointer]
162          ]
163        | _ ⇒ Error … [MSG CorruptedPointer]
164        ]
165      ]
166    ]
167  ].
168
169definition bevals_of_pointer ≝
170 λp:pointer.
171 map ?? (λn_sig.BVptr p (part_from_sig n_sig)) (range_strong size_pointer).
172
173definition bevals_of_pc ≝
174 λp:program_counter.
175 map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer).
176
177lemma pointer_of_bevals_bevals_of_pointer:
178 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
179#ptr
180whd in match (bevals_of_pointer ?);
181whd in ⊢ (??%?);
182>eq_block_b_b
183change with (eq_bv ???) in match (eq_bv_suffix ?????);
184>eq_bv_refl %
185qed.
186
187lemma pc_of_bevals_bevals_of_pc:
188 ∀p. pc_of_bevals (bevals_of_pc p) = OK … p.
189#ptr
190whd in match (bevals_of_pc ?);
191whd in ⊢ (??%?);
192>reflexive_eq_program_counter
193%
194qed.
195
196(* CSC: move elsewhere *)
197(* CSC: Wrong data-type? Use products of products *)
198definition list_to_pair: ∀A:Type[0]. ∀l:list A. length … l = 2 → A × A.
199 #A #l cases l [2: #a #tl cases tl [2: #b #tl' cases tl' [1: #_ @〈a,b〉 | #c #tl'']]]
200 #abs normalize in abs; destruct
201qed.
202
203(* Should fail if the address is not representable as a pair
204   As we only have 16 bit addresses atm, it never fails *)
205definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝
206 λp.list_to_pair … (bevals_of_pointer p) (refl …).
207(*
208 λp. match p with [ mk_pointer pty pbl pok poff ⇒
209  match pty with
210   [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?)
211   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
212   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
213
214definition beval_pair_of_pc: program_counter → beval × beval ≝
215 λp. list_to_pair ? (bevals_of_pc p) (refl …).
216
217(*
218definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
219 λp.
220  let 〈v1,v2〉 ≝ p in
221  do p ← pointer_of_bevals [v1;v2] ;
222  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
223  [ Code ⇒ λE.OK ? (mk_Sig … p E)
224  | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *)
225
226definition bool_of_beval: beval → res bool ≝
227 λv.match v with
228  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
229  | BVXor _ _ _ ⇒ Error … [MSG ValueNotABoolean] (* even if in some cases we can
230                                                   tell the value, we will always
231                                                   call bool_of_beval after a
232                                                   series of XORs has been
233                                                   completed *)
234  | BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *)
235  | BVByte b ⇒ OK … (¬eq_bv … (zero …) b)
236  | BVnull _ ⇒  OK … false
237  | _ ⇒ OK ? true
238  ].
239
240definition Byte_of_val: ErrorMessage → beval → res Byte ≝ (*CSC: move elsewhere *)
241 λerr,b.match b with
242  [ BVByte b ⇒ OK … b
243  | _ ⇒ Error … [MSG err]].
244
245definition Word_of_list_beval: list beval → res int ≝
246 λl.
247  let first_byte ≝ λl.
248   match l with
249    [ nil ⇒ Error ? [MSG NotAnInt32Val]
250    | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in
251  do 〈b1,l〉 ← first_byte l ;
252  do 〈b2,l〉 ← first_byte l ;
253  do 〈b3,l〉 ← first_byte l ;
254  do 〈b4,l〉 ← first_byte l ;
255   match l with
256    [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1)
257    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
258
259inductive add_or_sub : Type[0] ≝
260| do_add : add_or_sub
261| do_sub : add_or_sub.
262
263definition eq_add_or_sub : add_or_sub → add_or_sub → bool ≝
264λx,y.match x with
265[ do_add ⇒ match y with [ do_add ⇒ true | _ ⇒ false ]
266| do_sub ⇒ match y with [ do_sub ⇒ true | _ ⇒ false ]
267].
268
269inductive bebit : Type[0] ≝
270| BBbit : bool → bebit
271| BBundef : bebit
272| BBptrcarry :
273  add_or_sub → pointer → ∀p : part.BitVector (8*S p) → bebit.
274
275definition Bit_of_val: ErrorMessage → bebit → res Bit ≝ (*CSC: move elsewhere *)
276 λerr,b.match b with
277  [ BBbit b ⇒ OK … b
278  | _ ⇒ Error … [MSG err]].
279
280definition eq_option_map : ∀A: Type[0].(A → A → bool) → option A → option A → bool ≝
281λA,eq,a1,a2.
282match a1 with
283[ Some x ⇒ match a2 with [Some y ⇒ eq x y | _ ⇒ false ]
284| None ⇒ match a2 with [None ⇒ true | _ ⇒ false]
285].
286
287lemma eq_option_map_elim : ∀A : Type[0].∀P:bool → Prop.∀eq,
288x,y. (∀P:bool → Prop.∀z,w.(z = w → P true) → (z ≠w → P false) → P (eq z w)) →
289(x = y → P true) → (x ≠ y → P false) → P (eq_option_map A eq x y).
290#A #P #eq * [|#x] * [1,3:|*: #y] normalize #H #H1 #H2
291[@H1 % |2,3: @H2 % #EQ destruct(EQ)] @H
292[ #EQ @H1 >EQ %
293| * #H3 @H2 % #EQ destruct @H3 %
294]
295qed.
296
297
298definition eq_beval : beval → beval → bool ≝
299λbv1,bv2.
300match bv1 with
301[ BVundef ⇒ match bv2 with [ BVundef ⇒ true | _ ⇒ false ]
302| BVnonzero ⇒ match bv2 with [ BVnonzero ⇒ true | _ ⇒ false ]
303| BVXor pt1 pt1' p1 ⇒
304  match bv2 with
305  [ BVXor pt2 pt2' p2 ⇒ eq_option_map … eq_pointer pt1 pt2 ∧
306                        eq_option_map … eq_pointer pt1' pt2' ∧
307                        eqb (part_no … p1) (part_no … p2)
308  | _ ⇒ false
309  ]
310| BVByte b1 ⇒ match bv2 with [ BVByte b2 ⇒ eq_bv … b1 b2 | _ ⇒ false]
311| BVnull p1 ⇒ match bv2 with
312              [ BVnull p2 ⇒ eqb (part_no … p1) (part_no … p2) | _ ⇒ false ]
313| BVptr ptr1 p1 ⇒ match bv2 with
314                 [ BVptr ptr2 p2 ⇒ eq_pointer ptr1 ptr2 ∧
315                                   eqb (part_no … p1) (part_no … p2)
316                 | _ ⇒ false
317                 ]
318| BVpc pc1 p1 ⇒ match bv2 with
319                [ BVpc pc2 p2 ⇒ eq_program_counter pc1 pc2 ∧
320                  eqb (part_no … p1) (part_no … p2)
321                | _⇒ false
322                ]
323].
324
325lemma eq_beval_elim : ∀P:bool → Prop.∀x,y.
326(x = y → P true) → (x ≠ y → P false) → P (eq_beval x y).
327#P *
328[|| #pt1 #pt1' #p1 | #b1 | #p1 | #ptr1 #p1 | #pc1 #p1 ]
329*
330[1,8,15,22,29,36,43:
331|2,9,16,23,30,37,44:
332|3,10,17,24,31,38,45: #pt2 #pt2' #p2
333|4,11,18,25,32,39,46: #b2
334|5,12,19,26,33,40,47: #p2
335|6,13,20,26,34,41,48: #ptr2 #p2
336|*: #pc2 #p2
337]
338normalize nodelta #H1 #H2 try(@H1 %) try(@H2 % #EQ destruct)
339whd in match eq_beval; normalize nodelta
340[ @eq_option_map_elim
341 [ @eq_pointer_elim
342 |3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H %
343 | normalize nodelta #EQ destruct(EQ) @eq_option_map_elim
344 [ @eq_pointer_elim
345 |3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H %
346 | #EQ destruct(EQ) cases p1 in H1 H2; -p1 cases p2 -p2
347   #p2 #prf #p1 #prf1 #H1 #H2 @eqb_elim
348  [ #EQ destruct(EQ) @H1 %
349  | * #H @H2 % #EQ destruct(EQ) @H %
350  ]
351 ]
352 ]
353| @eq_bv_elim [#EQ destruct(EQ) @H1 % | * #H @H2 % #EQ destruct(EQ) @H %]
354| cases p1 in H1 H2; -p1 cases p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
355 [ #EQ destruct(EQ) @H1 %
356 | * #H @H2 % #EQ destruct @H %
357 ]
358| @eq_pointer_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct(EQ)
359  cases p1 in H1 H2; -p1 cases p2 -p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
360  [#EQ destruct @H1 %
361  | * #H @H2 % #EQ destruct @H %
362  ]
363| @eq_program_counter_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct
364  cases p1 in H1 H2; -p1 cases p2 -p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
365  [ #EQ destruct @H1 %
366  | * #H @H2 % #EQ destruct @H %
367  ]
368]
369qed.
Note: See TracBrowser for help on using the repository browser.