source: src/common/ByteValues.ma @ 2755

Last change on this file since 2755 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 9.2 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 bebit : Type[0] ≝
260| BBbit : bool → bebit
261| BBundef : bebit
262| BBptrcarry :
263  (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit.
264
265definition Bit_of_val: ErrorMessage → bebit → res Bit ≝ (*CSC: move elsewhere *)
266 λerr,b.match b with
267  [ BBbit b ⇒ OK … b
268  | _ ⇒ Error … [MSG err]].
Note: See TracBrowser for help on using the repository browser.