source: src/common/ByteValues.ma @ 2624

Last change on this file since 2624 was 2608, checked in by garnier, 8 years ago

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

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
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
113axiom CorruptedPointer: String.
114
115(* CSC: use vectors in place of lists? Or even better products of tuples
116   (more easily pattern matchable in the finite case)? requires one more parameter *)
117definition pointer_of_bevals: list beval → res pointer ≝
118 λl.
119 match l with
120  [ nil ⇒ Error … [MSG CorruptedPointer]
121  | cons bv1 tl ⇒
122    match tl with
123    [ nil ⇒ Error … [MSG CorruptedPointer]
124    | cons bv2 tl' ⇒
125      match tl' with
126      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
127      | nil ⇒
128        match bv1 with
129        [ BVptr ptr1 p1 ⇒
130          match bv2 with
131          [ BVptr ptr2 p2 ⇒
132            if eqb p1 0 ∧ eqb p2 1 ∧ eq_block (pblock ptr1) (pblock ptr2) ∧
133               eq_bv_suffix 8 8 8 (offv (poff ptr1)) (offv (poff ptr2))
134            then
135              return ptr2
136            else Error … [MSG CorruptedPointer]
137          | _ ⇒ Error … [MSG CorruptedPointer]
138          ]
139        | _ ⇒ Error … [MSG CorruptedPointer]
140        ]
141      ]
142    ]
143  ].
144
145definition pc_of_bevals: list beval → res program_counter ≝
146 λl.
147 match l with
148  [ nil ⇒ Error … [MSG CorruptedPointer]
149  | cons bv1 tl ⇒
150    match tl with
151    [ nil ⇒ Error … [MSG CorruptedPointer]
152    | cons bv2 tl' ⇒
153      match tl' with
154      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
155      | nil ⇒
156        match bv1 with
157        [ BVpc ptr1 p1 ⇒
158          match bv2 with
159          [ BVpc ptr2 p2 ⇒
160            if eqb p1 0 ∧ eqb p2 1 ∧ eq_program_counter ptr1 ptr2 then
161              return ptr2
162            else Error … [MSG CorruptedPointer]
163          | _ ⇒ Error … [MSG CorruptedPointer]
164          ]
165        | _ ⇒ Error … [MSG CorruptedPointer]
166        ]
167      ]
168    ]
169  ].
170
171definition bevals_of_pointer ≝
172 λp:pointer.
173 map ?? (λn_sig.BVptr p (part_from_sig n_sig)) (range_strong size_pointer).
174
175definition bevals_of_pc ≝
176 λp:program_counter.
177 map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer).
178
179lemma pointer_of_bevals_bevals_of_pointer:
180 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
181#ptr
182whd in match (bevals_of_pointer ?);
183whd in ⊢ (??%?);
184>eq_block_b_b
185change with (eq_bv ???) in match (eq_bv_suffix ?????);
186>eq_bv_refl %
187qed.
188
189lemma pc_of_bevals_bevals_of_pc:
190 ∀p. pc_of_bevals (bevals_of_pc p) = OK … p.
191#ptr
192whd in match (bevals_of_pc ?);
193whd in ⊢ (??%?);
194>reflexive_eq_program_counter
195%
196qed.
197
198(* CSC: move elsewhere *)
199(* CSC: Wrong data-type? Use products of products *)
200definition list_to_pair: ∀A:Type[0]. ∀l:list A. length … l = 2 → A × A.
201 #A #l cases l [2: #a #tl cases tl [2: #b #tl' cases tl' [1: #_ @〈a,b〉 | #c #tl'']]]
202 #abs normalize in abs; destruct
203qed.
204
205axiom NotATwoBytesPointer: String.
206
207(* Should fail if the address is not representable as a pair
208   As we only have 16 bit addresses atm, it never fails *)
209definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝
210 λp.list_to_pair … (bevals_of_pointer p) (refl …).
211(*
212 λp. match p with [ mk_pointer pty pbl pok poff ⇒
213  match pty with
214   [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?)
215   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
216   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
217
218definition beval_pair_of_pc: program_counter → beval × beval ≝
219 λp. list_to_pair ? (bevals_of_pc p) (refl …).
220
221(* axiom NotACodePointer: String.
222definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
223 λp.
224  let 〈v1,v2〉 ≝ p in
225  do p ← pointer_of_bevals [v1;v2] ;
226  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
227  [ Code ⇒ λE.OK ? (mk_Sig … p E)
228  | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *)
229
230axiom ValueNotABoolean: String.
231
232definition bool_of_beval: beval → res bool ≝
233 λv.match v with
234  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
235  | BVXor _ _ _ ⇒ Error … [MSG ValueNotABoolean] (* even if in some cases we can
236                                                   tell the value, we will always
237                                                   call bool_of_beval after a
238                                                   series of XORs has been
239                                                   completed *)
240  | BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *)
241  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
242  | BVnull _ ⇒  OK … false
243  | _ ⇒ OK ? true
244  ].
245
246definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *)
247 λerr,b.match b with
248  [ BVByte b ⇒ OK … b
249  | _ ⇒ Error … [MSG err]].
250
251axiom NotAnInt32Val: String.
252definition Word_of_list_beval: list beval → res int ≝
253 λl.
254  let first_byte ≝ λl.
255   match l with
256    [ nil ⇒ Error ? [MSG NotAnInt32Val]
257    | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in
258  do 〈b1,l〉 ← first_byte l ;
259  do 〈b2,l〉 ← first_byte l ;
260  do 〈b3,l〉 ← first_byte l ;
261  do 〈b4,l〉 ← first_byte l ;
262   match l with
263    [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1)
264    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
265
266inductive bebit : Type[0] ≝
267| BBbit : bool → bebit
268| BBundef : bebit
269| BBptrcarry :
270  (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit.
271
272definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
273 λerr,b.match b with
274  [ BBbit b ⇒ OK … b
275  | _ ⇒ Error … [MSG err]].
Note: See TracBrowser for help on using the repository browser.