source: src/common/ByteValues.ma @ 2462

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

separated in back end values program counters from code pointers (intended to hold function pointers only): same signature, but separation needed the proof of some passes

File size: 7.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
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
13record part (*r: region*): Type[0] ≝
14 { part_no:> nat
15 ; part_no_ok: part_no < size_pointer (*r*)
16 }.
17
18definition part_from_sig : (Σn:ℕ.n<size_pointer) → part ≝
19λn_sig : Σn.n<size_pointer.mk_part n_sig (pi2 … n_sig).
20
21coercion sig_to_part : ∀n_sig:Σn:ℕ.n<size_pointer.part ≝
22part_from_sig on _n_sig:Σn.n<size_pointer to part.
23
24(* Byte-sized values used in the back-end.
25   Values larger than a single Byte are represented via their parts.
26   Values are either:
27  - machine integers (Bytes)
28  - parts of a pointer seen as a triple giving the representation of the
29    pointer (in terms of the memory regions such a pointer could address),
30    a memory address and an integer offset with respect to this address;
31  - a null pointer: the region denotes the pointer size
32  - the [BVundef] value denoting an arbitrary bit pattern, such as the
33    value of an uninitialized variable
34  - [BVXor] is a formal XOR between (possibly null) pointer parts
35  - [BVnonzero] is any nonzero value
36*)
37
38inductive beval: Type[0] ≝
39  | BVundef: beval
40  | BVnonzero: beval
41  | BVXor: option pointer → option pointer → part → beval (* option pointer ≈ pointer + null *)
42  | BVByte: Byte → beval
43  | BVnull: (*∀r:region.*) part  → beval
44  | BVptr: pointer → part → beval
45  | BVpc: cpointer → part → beval. (* only used in back end, needed to separate
46                                      program counters that go in the stack from
47                                      function pointers, as they are linked with
48                                      different relations in some passes *)
49
50definition eq_bv_suffix : ∀n,m,p.
51  BitVector (n + p) → BitVector (m + p) → bool ≝
52λn,m,p,v1,v2.
53let b1 ≝ \snd (vsplit … v1) in
54let b2 ≝ \snd (vsplit … v2) in
55eq_bv … b1 b2.
56
57include alias "arithmetics/nat.ma".
58
59axiom CorruptedPointer: String.
60
61(* CSC: use vectors in place of lists? Or even better products of tuples
62   (more easily pattern matchable in the finite case)? requires one more parameter *)
63definition pointer_of_bevals: list beval → res pointer ≝
64 λl.
65 match l with
66  [ nil ⇒ Error … [MSG CorruptedPointer]
67  | cons bv1 tl ⇒
68    match tl with
69    [ nil ⇒ Error … [MSG CorruptedPointer]
70    | cons bv2 tl' ⇒
71      match tl' with
72      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
73      | nil ⇒
74        match bv1 with
75        [ BVptr ptr1 p1 ⇒
76          match bv2 with
77          [ BVptr ptr2 p2 ⇒
78            if eqb p1 0 ∧ eqb p2 1 ∧ eq_block (pblock ptr1) (pblock ptr2) ∧
79               eq_bv_suffix 8 8 8 (offv (poff ptr1)) (offv (poff ptr2))
80            then
81              return ptr2
82            else Error … [MSG CorruptedPointer]
83          | _ ⇒ Error … [MSG CorruptedPointer]
84          ]
85        | _ ⇒ Error … [MSG CorruptedPointer]
86        ]
87      ]
88    ]
89  ].
90
91definition pc_of_bevals: list beval → res cpointer ≝
92 λl.
93 match l with
94  [ nil ⇒ Error … [MSG CorruptedPointer]
95  | cons bv1 tl ⇒
96    match tl with
97    [ nil ⇒ Error … [MSG CorruptedPointer]
98    | cons bv2 tl' ⇒
99      match tl' with
100      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
101      | nil ⇒
102        match bv1 with
103        [ BVpc ptr1 p1 ⇒
104          match bv2 with
105          [ BVpc ptr2 p2 ⇒
106            if eqb p1 0 ∧ eqb p2 1 ∧ eq_pointer ptr1 ptr2 then
107              return ptr2
108            else Error … [MSG CorruptedPointer]
109          | _ ⇒ Error … [MSG CorruptedPointer]
110          ]
111        | _ ⇒ Error … [MSG CorruptedPointer]
112        ]
113      ]
114    ]
115  ].
116
117definition bevals_of_pointer ≝
118 λp:pointer.
119 map ?? (λn_sig.BVptr p (part_from_sig n_sig)) (range_strong size_pointer).
120
121definition bevals_of_pc ≝
122 λp:cpointer.
123 map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer).
124
125lemma pointer_of_bevals_bevals_of_pointer:
126 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
127#ptr
128whd in match (bevals_of_pointer ?);
129whd in ⊢ (??%?);
130>eq_block_b_b
131change with (eq_bv ???) in match (eq_bv_suffix ?????);
132>eq_bv_refl %
133qed.
134
135lemma pc_of_bevals_bevals_of_pc:
136 ∀p. pc_of_bevals (bevals_of_pc p) = OK … p.
137#ptr
138whd in match (bevals_of_pc ?);
139whd in ⊢ (??%?);
140>reflexive_eq_pointer
141%
142qed.
143
144(* CSC: move elsewhere *)
145(* CSC: Wrong data-type? Use products of products *)
146definition list_to_pair: ∀A:Type[0]. ∀l:list A. length … l = 2 → A × A.
147 #A #l cases l [2: #a #tl cases tl [2: #b #tl' cases tl' [1: #_ @〈a,b〉 | #c #tl'']]]
148 #abs normalize in abs; destruct
149qed.
150
151axiom NotATwoBytesPointer: String.
152
153(* Should fail if the address is not representable as a pair
154   As we only have 16 bit addresses atm, it never fails *)
155definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝
156 λp.list_to_pair … (bevals_of_pointer p) (refl …).
157(*
158 λp. match p with [ mk_pointer pty pbl pok poff ⇒
159  match pty with
160   [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?)
161   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
162   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
163
164definition beval_pair_of_pc: cpointer → beval × beval ≝
165 λp. list_to_pair ? (bevals_of_pc p) (refl …).
166
167(* axiom NotACodePointer: String.
168definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
169 λp.
170  let 〈v1,v2〉 ≝ p in
171  do p ← pointer_of_bevals [v1;v2] ;
172  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
173  [ Code ⇒ λE.OK ? (mk_Sig … p E)
174  | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *)
175
176axiom ValueNotABoolean: String.
177
178definition bool_of_beval: beval → res bool ≝
179 λv.match v with
180  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
181  | BVXor _ _ _ ⇒ Error … [MSG ValueNotABoolean] (* even if in some cases we can
182                                                   tell the value, we will always
183                                                   call bool_of_beval after a
184                                                   series of XORs has been
185                                                   completed *)
186  | BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *)
187  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
188  | BVnull _ ⇒  OK … false
189  | _ ⇒ OK ? true
190  ].
191
192definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *)
193 λerr,b.match b with
194  [ BVByte b ⇒ OK … b
195  | _ ⇒ Error … [MSG err]].
196
197axiom NotAnInt32Val: String.
198definition Word_of_list_beval: list beval → res int ≝
199 λl.
200  let first_byte ≝ λl.
201   match l with
202    [ nil ⇒ Error ? [MSG NotAnInt32Val]
203    | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in
204  do 〈b1,l〉 ← first_byte l ;
205  do 〈b2,l〉 ← first_byte l ;
206  do 〈b3,l〉 ← first_byte l ;
207  do 〈b4,l〉 ← first_byte l ;
208   match l with
209    [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1)
210    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
211
212inductive bebit : Type[0] ≝
213| BBbit : bool → bebit
214| BBundef : bebit
215| BBptrcarry :
216  (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit.
217
218definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
219 λerr,b.match b with
220  [ BBbit b ⇒ OK … b
221  | _ ⇒ Error … [MSG err]].
Note: See TracBrowser for help on using the repository browser.