source: src/common/ByteValues.ma @ 2428

Last change on this file since 2428 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: 8.4 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
8record part (*r: region*): Type[0] ≝
9 { part_no:> nat
10 ; part_no_ok: part_no < size_pointer (*r*)
11 }.
12
13(* Byte-sized values used in the back-end.
14   Values larger than a single Byte are represented via their parts.
15   Values are either:
16  - machine integers (Bytes)
17  - parts of a pointer seen as a triple giving the representation of the
18    pointer (in terms of the memory regions such a pointer could address),
19    a memory address and an integer offset with respect to this address;
20  - a null pointer: the region denotes the pointer size
21  - the [BVundef] value denoting an arbitrary bit pattern, such as the
22    value of an uninitialized variable
23  - the [BVnonzero] value denoting an arbitrary but non-zero bit pattern,
24    which arise in the RTLabs → RTL pass when translating equality comparisons
25    between pointers (which get translated to multiple XORs between pointer
26    parts).   
27*)
28
29inductive beval: Type[0] ≝
30  | BVundef: beval
31  | BVnonzero: beval
32  | BVByte: Byte → beval
33  | BVnull: (*∀r:region.*) part  → beval
34  | BVptr: block → ∀p:part.Vector Byte (S p) → beval.
35
36definition eq_beval: beval → beval → bool ≝
37 λv1,v2.
38  match v1 with
39   [ BVundef      ⇒ match v2 with [ BVundef      ⇒ true                           | _ ⇒ false ]
40   | BVnonzero    ⇒ match v2 with [ BVnonzero    ⇒ true                           | _ ⇒ false ]
41   | BVByte b1    ⇒ match v2 with [ BVByte b2    ⇒ eq_bv … b1 b2                  | _ ⇒ false ]
42   | BVnull p1    ⇒ match v2 with [ BVnull p2    ⇒ eqb p1 p2                      | _ ⇒ false ]
43   | BVptr b1 p1 o1  ⇒
44      match v2 with
45      [ BVptr b2 p2 o2  ⇒
46        eq_block … b1 b2 ∧ eqb p1 p2 ∧
47          (* equivalent to equality if p1 = p2 *)
48          vprefix … (eq_bv 8) o1 o2
49      | _ ⇒ false
50      ]
51   ].
52
53include alias "arithmetics/nat.ma".
54
55axiom CorruptedPointer: String.
56
57let rec pointer_of_bevals_aux (b:block) (part: nat) (acc : BitVector (part*8))
58  (l: list beval) on l : res pointer ≝
59 match l with
60  [ nil ⇒
61     If eqb part (size_pointer (*ptype p*)) then with prf do
62      return mk_pointer b (mk_offset (acc⌈BitVector (part*8)↦?⌉))
63     else
64      Error … [MSG CorruptedPointer]
65  | cons v tl ⇒
66     match v with
67      [ BVptr b' part' o' ⇒
68        let acc' ≝ vflatten … o' in
69        if eq_block b b' ∧
70           eqb part part' ∧
71           vsuffix … eq_b acc acc' then
72           pointer_of_bevals_aux b (S part') acc' tl
73         else
74          Error … [MSG CorruptedPointer]
75      | _ ⇒ Error … [MSG CorruptedPointer]
76      ]
77  ].
78  @hide_prf
79  >commutative_times_fast
80  lapply prf @(eqb_elim part) #H * >H % qed.
81
82(* CSC: use vectors in place of lists? Or even better products of tuples
83   (more easily pattern matchable in the finite case)? requires one more parameter *)
84definition pointer_of_bevals: list beval → res pointer ≝
85 λl.
86 match l with
87  [ nil ⇒ Error … [MSG CorruptedPointer]
88  | cons he tl ⇒
89     match he with
90      [ BVptr b part o ⇒
91         if eqb part 0 then
92           pointer_of_bevals_aux b (S part) (vflatten … o) tl
93         else Error … [MSG CorruptedPointer]
94      | _ ⇒ Error … [MSG CorruptedPointer]
95      ]
96  ].
97
98(* CSC: use vectors in place of lists? Or even better products of tuples
99   (more easily pattern matchable in the finite case)? *)
100let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) on n: n + part = size_pointer (*ptype p*) → list beval ≝
101 match n with
102  [ O ⇒ λ_.[]
103  | S m ⇒ λpr': S m + part = ?.
104    let postfix ≝ rvsplit … (\snd (vsplit bool (m*8) (S part*8) (offv (poff p) ⌈BitVector ?↦?⌉))) in
105    (BVptr (pblock p) (mk_part … part …) postfix)::bevals_of_pointer_aux p (S part) m ?
106  ].
107@hide_prf
108[3: change with (?*?) in match offset_size;
109  <pr' >(commutative_times_fast ? 8) >(commutative_times_fast ? 8)
110  <distributive_times_plus_fast <plus_n_Sm_fast %
111] -postfix
112/3 by lt_plus_to_minus_r, lt_plus_to_lt_l/ qed.
113
114definition bevals_of_pointer: pointer → list beval ≝
115 λp. bevals_of_pointer_aux p 0 (size_pointer (*ptype p*)) ….
116@hide_prf @plus_n_O qed.
117
118lemma pointer_of_bevals_bevals_of_pointer:
119 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
120* #pbl * #voff
121whd in match (bevals_of_pointer ?);
122@vsplit_elim #pre #post
123normalize nodelta
124#EQ >EQ
125whd in match (bevals_of_pointer_aux ????);
126@vsplit_elim #pre' #post'
127normalize nodelta
128>(Vector_O … pre') #EQ' normalize in EQ'; <EQ' -pre' -post'
129whd in ⊢ (??%?);
130>eq_block_b_b >eqb_n_n
131>vflatten_rvsplit >vflatten_rvsplit
132>vsuffix_true
133[2: change with (bool_to_Prop (eq_bv ???)) >eq_bv_refl % ]
134normalize nodelta %
135qed.
136
137(* CSC: move elsewhere *)
138(* CSC: Wrong data-type? Use products of products *)
139definition list_to_pair: ∀A:Type[0]. ∀l:list A. length … l = 2 → A × A.
140 #A #l cases l [2: #a #tl cases tl [2: #b #tl' cases tl' [1: #_ @〈a,b〉 | #c #tl'']]]
141 #abs normalize in abs; destruct
142qed.
143
144axiom NotATwoBytesPointer: String.
145
146(* Fails if the address is not representable as a pair *)
147definition beval_pair_of_pointer: pointer → res (beval × beval) ≝
148 λp. OK … (list_to_pair … (bevals_of_pointer p) ?).
149(*
150 λp. match p with [ mk_pointer pty pbl pok poff ⇒
151  match pty with
152   [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?)
153   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
154   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
155% qed.
156
157definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝
158 λp. list_to_pair ? (bevals_of_pointer p) ?.
159(*
160 λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒
161  match pty return λpty. ? → pty = Code → ? with
162   [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ?
163   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
164[@(pi2 … p) |7: // |8: %] destruct (abs)*) %
165qed.
166
167
168axiom NotACodePointer: String.
169definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
170 λp.
171  let 〈v1,v2〉 ≝ p in
172  do p ← pointer_of_bevals [v1;v2] ;
173  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
174  [ Code ⇒ λE.OK ? (mk_Sig … p ?)
175  | _ ⇒ λ_.Error … [MSG NotACodePointer]] ?.
176// qed.
177
178axiom ValueNotABoolean: String.
179
180definition bool_of_beval: beval → res bool ≝
181 λv.match v with
182  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
183  | BVnonzero ⇒ OK … true
184  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
185  | BVnull y ⇒  OK … false
186  | BVptr p q o ⇒ OK ? true ].
187
188definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *)
189 λerr,b.match b with
190  [ BVByte b ⇒ OK … b
191  | _ ⇒ Error … [MSG err]].
192
193axiom NotAnInt32Val: String.
194definition Word_of_list_beval: list beval → res int ≝
195 λl.
196  let first_byte ≝ λl.
197   match l with
198    [ nil ⇒ Error ? [MSG NotAnInt32Val]
199    | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in
200  do 〈b1,l〉 ← first_byte l ;
201  do 〈b2,l〉 ← first_byte l ;
202  do 〈b3,l〉 ← first_byte l ;
203  do 〈b4,l〉 ← first_byte l ;
204   match l with
205    [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1)
206    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
207
208inductive bebit : Type[0] ≝
209| BBbit : bool → bebit
210| BBundef : bebit
211| BBptrcarry :
212  (* is add *) bool → block → ∀p : part.Vector Byte (S p) → Vector Byte (S p) → bebit.
213
214definition eq_bebit: bebit → bebit → bool ≝
215 λv1,v2.
216  match v1 with
217   [ BBundef      ⇒ match v2 with [ BBundef      ⇒ true                           | _ ⇒ false ]
218   | BBbit b1    ⇒ match v2 with [ BBbit b2    ⇒ eq_b b1 b2                  | _ ⇒ false ]
219   | BBptrcarry is_add1 b1 p1 o1 by1  ⇒
220      match v2 with
221      [ BBptrcarry is_add2 b2 p2 o2 by2  ⇒
222        eq_b is_add1 is_add2 ∧ eq_block … b1 b2 ∧ eqb p1 p2 ∧
223          (* equivalent to equality if p1 = p2 *)
224          vprefix … (eq_bv 8) o1 o2 ∧
225          vprefix … (eq_bv 8) by1 by2
226      | _ ⇒ false
227      ]
228   ].
229
230definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
231 λerr,b.match b with
232  [ BBbit b ⇒ OK … b
233  | _ ⇒ Error … [MSG err]].
Note: See TracBrowser for help on using the repository browser.