source: src/common/ByteValues.ma @ 2540

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

completely separated program counters from code pointers in joint languages: the advantage is program counters with an unbounded offset in Pos

File size: 9.3 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
8definition cpointer ≝ Σp.ptype p = Code.
9definition xpointer ≝ Σp.ptype p = XData.
10unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
11unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
12
13(* this is like a code pointer, but with unbounded offset.
14   used only in the back-end, they become code pointers in LIN → ASM *)
15record program_counter : Type[0] ≝
16  { pc_block : Σb : block.block_region b = Code
17  ; pc_offset : Pos
18  }.
19
20definition eq_program_counter : program_counter → program_counter → bool ≝
21λpc1,pc2.eq_block (pc_block pc1) (pc_block pc2) ∧
22         eqb (pc_offset pc1) (pc_offset pc2).
23
24lemma eq_program_counter_elim : ∀P:bool→Prop.
25  ∀pc1,pc2.(pc1=pc2→P true)→(pc1≠pc2→P false)→P (eq_program_counter pc1 pc2).
26#P ** #bl1 #H1 #o1 ** #bl2 #H2 #o2
27#Heq #Hneq whd in ⊢ (?%);
28@eq_block_elim #EQ1
29[ @eqb_elim #EQ2 ]
30[ @Heq destruct %
31|*: @Hneq % #ABS destruct
32  [ @(absurd ?? EQ2) | @(absurd ?? EQ1) ] %
33] qed.
34
35lemma reflexive_eq_program_counter : ∀pc.eq_program_counter pc pc = true.
36** #bl1 #H1 #o1 whd in ⊢ (??%?); >eq_block_b_b >eqb_n_n % qed.
37
38definition bitvector_from_pos :
39  ∀n.Pos → BitVector n ≝
40  λn,p.bitvector_of_Z n (Zpred (pos p)).
41
42definition pos_from_bitvector :
43  ∀n.BitVector n → Pos ≝
44  λn,v.
45  match Zsucc (Z_of_unsigned_bitvector n v)
46  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
47  with
48  [ OZ ⇒ λprf.⊥
49  | pos x ⇒ λ_. x
50  | neg x ⇒ λprf.⊥
51  ] (refl …).
52@hide_prf
53elim v in prf;
54[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
55
56definition cpointer_of_pc : program_counter → option cpointer ≝
57  λpc.
58  let pc_off ≝ pc_offset pc in
59  if leb pc_off (two_power_nat offset_size) then
60    return «mk_pointer (pc_block pc) (mk_offset (bitvector_from_pos … pc_off)),?»
61  else
62    None ?.
63elim (pc_block pc) #bl #H @H qed.
64
65record part (*r: region*): Type[0] ≝
66 { part_no:> nat
67 ; part_no_ok: part_no < size_pointer (*r*)
68 }.
69
70definition part_from_sig : (Σn:ℕ.n<size_pointer) → part ≝
71λn_sig : Σn.n<size_pointer.mk_part n_sig (pi2 … n_sig).
72
73coercion sig_to_part : ∀n_sig:Σn:ℕ.n<size_pointer.part ≝
74part_from_sig on _n_sig:Σn.n<size_pointer to part.
75
76(* Byte-sized values used in the back-end.
77   Values larger than a single Byte are represented via their parts.
78   Values are either:
79  - machine integers (Bytes)
80  - parts of a pointer seen as a triple giving the representation of the
81    pointer (in terms of the memory regions such a pointer could address),
82    a memory address and an integer offset with respect to this address;
83  - a null pointer: the region denotes the pointer size
84  - the [BVundef] value denoting an arbitrary bit pattern, such as the
85    value of an uninitialized variable
86  - [BVXor] is a formal XOR between (possibly null) pointer parts
87  - [BVnonzero] is any nonzero value
88*)
89
90inductive beval: Type[0] ≝
91  | BVundef: beval
92  | BVnonzero: beval
93  | BVXor: option pointer → option pointer → part → beval (* option pointer ≈ pointer + null *)
94  | BVByte: Byte → beval
95  | BVnull: (*∀r:region.*) part  → beval
96  | BVptr: pointer → part → beval
97  | BVpc: program_counter → part → beval. (* only used in back end, needed to separate
98                                      program counters that go in the stack from
99                                      function pointers, as they are linked with
100                                      different relations in some passes *)
101
102definition eq_bv_suffix : ∀n,m,p.
103  BitVector (n + p) → BitVector (m + p) → bool ≝
104λn,m,p,v1,v2.
105let b1 ≝ \snd (vsplit … v1) in
106let b2 ≝ \snd (vsplit … v2) in
107eq_bv … b1 b2.
108
109include alias "arithmetics/nat.ma".
110
111axiom CorruptedPointer: String.
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
203axiom NotATwoBytesPointer: String.
204
205(* Should fail if the address is not representable as a pair
206   As we only have 16 bit addresses atm, it never fails *)
207definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝
208 λp.list_to_pair … (bevals_of_pointer p) (refl …).
209(*
210 λp. match p with [ mk_pointer pty pbl pok poff ⇒
211  match pty with
212   [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?)
213   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
214   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
215
216definition beval_pair_of_pc: program_counter → beval × beval ≝
217 λp. list_to_pair ? (bevals_of_pc p) (refl …).
218
219(* axiom NotACodePointer: String.
220definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
221 λp.
222  let 〈v1,v2〉 ≝ p in
223  do p ← pointer_of_bevals [v1;v2] ;
224  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
225  [ Code ⇒ λE.OK ? (mk_Sig … p E)
226  | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *)
227
228axiom ValueNotABoolean: String.
229
230definition bool_of_beval: beval → res bool ≝
231 λv.match v with
232  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
233  | BVXor _ _ _ ⇒ Error … [MSG ValueNotABoolean] (* even if in some cases we can
234                                                   tell the value, we will always
235                                                   call bool_of_beval after a
236                                                   series of XORs has been
237                                                   completed *)
238  | BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *)
239  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
240  | BVnull _ ⇒  OK … false
241  | _ ⇒ OK ? true
242  ].
243
244definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *)
245 λerr,b.match b with
246  [ BVByte b ⇒ OK … b
247  | _ ⇒ Error … [MSG err]].
248
249axiom NotAnInt32Val: String.
250definition Word_of_list_beval: list beval → res int ≝
251 λl.
252  let first_byte ≝ λl.
253   match l with
254    [ nil ⇒ Error ? [MSG NotAnInt32Val]
255    | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in
256  do 〈b1,l〉 ← first_byte l ;
257  do 〈b2,l〉 ← first_byte l ;
258  do 〈b3,l〉 ← first_byte l ;
259  do 〈b4,l〉 ← first_byte l ;
260   match l with
261    [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1)
262    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
263
264inductive bebit : Type[0] ≝
265| BBbit : bool → bebit
266| BBundef : bebit
267| BBptrcarry :
268  (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit.
269
270definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
271 λerr,b.match b with
272  [ BBbit b ⇒ OK … b
273  | _ ⇒ Error … [MSG err]].
Note: See TracBrowser for help on using the repository browser.