1 | (* Type of values used in the dynamic semantics of the back-end intermediate |
---|
2 | languages. Inspired by common/Values.ma, adapted from Compcert *) |
---|
3 | |
---|
4 | include "common/Pointers.ma". |
---|
5 | include "utilities/sigma.ma". |
---|
6 | |
---|
7 | record part (r: region): Type[0] ≝ |
---|
8 | { part_no:> nat |
---|
9 | ; part_no_ok: part_no ≤ size_pointer r |
---|
10 | }. |
---|
11 | |
---|
12 | (* Byte-sized values used in the back-end. |
---|
13 | Values larger than a single Byte are represented via their parts. |
---|
14 | Values are either: |
---|
15 | - machine integers (Bytes) |
---|
16 | - parts of a pointer seen as a triple giving the representation of the |
---|
17 | pointer (in terms of the memory regions such a pointer could address), |
---|
18 | a memory address and an integer offset with respect to this address; |
---|
19 | - a null pointer: the region denotes the pointer size |
---|
20 | - the [BVundef] value denoting an arbitrary bit pattern, such as the |
---|
21 | value of an uninitialized variable |
---|
22 | *) |
---|
23 | |
---|
24 | inductive beval: Type[0] ≝ |
---|
25 | | BVundef: beval |
---|
26 | | BVByte: Byte → beval |
---|
27 | | BVnull: ∀r:region. part r → beval |
---|
28 | | BVptr: ∀p:pointer. part (ptype p) → beval. |
---|
29 | |
---|
30 | definition eq_beval: beval → beval → bool ≝ |
---|
31 | λv1,v2. |
---|
32 | match v1 with |
---|
33 | [ BVundef ⇒ match v2 with [ BVundef ⇒ true | _ ⇒ false ] |
---|
34 | | BVByte b1 ⇒ match v2 with [ BVByte b2 ⇒ eq_bv … b1 b2 | _ ⇒ false ] |
---|
35 | | BVnull r1 p1 ⇒ match v2 with [ BVnull r2 p2 ⇒ eq_region … r1 r2 ∧ eqb p1 p2 | _ ⇒ false ] |
---|
36 | | BVptr P1 p1 ⇒ match v2 with [ BVptr P2 p2 ⇒ eq_pointer … P1 P2 ∧ eqb p1 p2 | _ ⇒ false ]]. |
---|
37 | |
---|
38 | axiom CorruptedValue: String. |
---|
39 | |
---|
40 | let rec pointer_of_bevals_aux (p:pointer) (part: nat) (l: list beval) on l : res pointer ≝ |
---|
41 | match l with |
---|
42 | [ nil ⇒ |
---|
43 | if eqb part (size_pointer (ptype p)) then |
---|
44 | OK … p |
---|
45 | else |
---|
46 | Error … [MSG CorruptedValue] |
---|
47 | | cons v tl ⇒ |
---|
48 | match v with |
---|
49 | [ BVptr p' part' ⇒ |
---|
50 | if eq_pointer p p' ∧ eqb part part' then |
---|
51 | pointer_of_bevals_aux p (S part) tl |
---|
52 | else |
---|
53 | Error … [MSG CorruptedValue] |
---|
54 | | _ ⇒ Error … [MSG CorruptedValue]]]. |
---|
55 | |
---|
56 | axiom NotAPointer: String. |
---|
57 | |
---|
58 | (* CSC: use vectors in place of lists? Or even better products of tuples |
---|
59 | (more easily pattern matchable in the finite case)? requires one more parameter *) |
---|
60 | definition pointer_of_bevals: list beval → res pointer ≝ |
---|
61 | λl. |
---|
62 | match l with |
---|
63 | [ nil ⇒ Error … [MSG NotAPointer] |
---|
64 | | cons he tl ⇒ |
---|
65 | match he with |
---|
66 | [ BVptr p part ⇒ |
---|
67 | if eqb part 0 then pointer_of_bevals_aux p 1 tl else Error … [MSG NotAPointer] |
---|
68 | | _ ⇒ Error … [MSG NotAPointer]]]. |
---|
69 | |
---|
70 | (* CSC: use vectors in place of lists? Or even better products of tuples |
---|
71 | (more easily pattern matchable in the finite case)? *) |
---|
72 | let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) (pr: plus part n = size_pointer (ptype p)) on n: list beval ≝ |
---|
73 | match n with |
---|
74 | [ O ⇒ λ_.[] |
---|
75 | | S m ⇒ λpr':n=S m.(BVptr p (mk_part … part …))::bevals_of_pointer_aux p (S part) m ?] (refl ? n). |
---|
76 | /3/ (*Andrea: by _ cannot be re-parsed*) qed. |
---|
77 | |
---|
78 | definition bevals_of_pointer: pointer → list beval ≝ |
---|
79 | λp. bevals_of_pointer_aux p 0 (size_pointer (ptype p)) …. |
---|
80 | // qed. |
---|
81 | |
---|
82 | lemma pointer_of_bevals_bevals_of_pointer: |
---|
83 | ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p. |
---|
84 | * * #pbl #pok #poff |
---|
85 | try % |
---|
86 | whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %] |
---|
87 | whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 2) % |
---|
88 | qed. |
---|
89 | |
---|
90 | (* CSC: move elsewhere *) |
---|
91 | (* CSC: Wrong data-type? Use products of products *) |
---|
92 | definition list_to_pair: ∀A:Type[0]. ∀l:list A. length … l = 2 → A × A. |
---|
93 | #A #l cases l [2: #a #tl cases tl [2: #b #tl' cases tl' [1: #_ @〈a,b〉 | #c #tl'']]] |
---|
94 | #abs normalize in abs; destruct |
---|
95 | qed. |
---|
96 | |
---|
97 | axiom NotATwoBytesPointer: String. |
---|
98 | |
---|
99 | (* Fails if the address is not representable as a pair *) |
---|
100 | definition beval_pair_of_pointer: pointer → res (beval × beval) ≝ |
---|
101 | λp. match p with [ mk_pointer pty pbl pok poff ⇒ |
---|
102 | match pty with |
---|
103 | [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?) |
---|
104 | | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?) |
---|
105 | | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok]. |
---|
106 | % qed. |
---|
107 | |
---|
108 | definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝ |
---|
109 | λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒ |
---|
110 | match pty return λpty. ? → pty = Code → ? with |
---|
111 | [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ? |
---|
112 | | _ ⇒ λpok'.λabs. ⊥] pok] ?. |
---|
113 | [@(pi2 … p) |7: // |8: %] destruct (abs) |
---|
114 | qed. |
---|
115 | |
---|
116 | |
---|
117 | axiom NotACodePointer: String. |
---|
118 | definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝ |
---|
119 | λp. |
---|
120 | let 〈v1,v2〉 ≝ p in |
---|
121 | do p ← pointer_of_bevals [v1;v2] ; |
---|
122 | match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with |
---|
123 | [ Code ⇒ λE.OK ? (inject … p ?) |
---|
124 | | _ ⇒ λ_.Error … [MSG NotACodePointer]] ?. |
---|
125 | // qed. |
---|
126 | |
---|
127 | axiom ValueNotABoolean: String. |
---|
128 | |
---|
129 | definition bool_of_beval: beval → res bool ≝ |
---|
130 | λv.match v with |
---|
131 | [ BVundef ⇒ Error … [MSG ValueNotABoolean] |
---|
132 | | BVByte b ⇒ OK … (eq_bv … (zero …) b) |
---|
133 | | BVnull x y ⇒ OK … false |
---|
134 | | BVptr p q ⇒ OK ? true ]. |
---|
135 | |
---|
136 | axiom BadByte: String. |
---|
137 | |
---|
138 | definition Byte_of_val: beval → res Byte ≝ (*CSC: move elsewhere *) |
---|
139 | λb.match b with |
---|
140 | [ BVByte b ⇒ OK … b |
---|
141 | | _ ⇒ Error … [MSG BadByte]]. |
---|
142 | |
---|
143 | axiom NotAnInt32Val: String. |
---|
144 | definition Word_of_list_beval: list beval → res int ≝ |
---|
145 | λl. |
---|
146 | let first_byte ≝ λl. |
---|
147 | match l with |
---|
148 | [ nil ⇒ Error ? [MSG NotAnInt32Val] |
---|
149 | | cons hd tl ⇒ do b ← Byte_of_val hd ; OK ? 〈b,tl〉 ] in |
---|
150 | do 〈b1,l〉 ← first_byte l ; |
---|
151 | do 〈b2,l〉 ← first_byte l ; |
---|
152 | do 〈b3,l〉 ← first_byte l ; |
---|
153 | do 〈b4,l〉 ← first_byte l ; |
---|
154 | match l with |
---|
155 | [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1) |
---|
156 | | _ ⇒ Error ? [MSG NotAnInt32Val] ]. |
---|
157 | |
---|
158 | (* CSC: maybe we should introduce a type of 1-bit-sized values *) |
---|
159 | definition BVtrue: beval ≝ BVByte [[false;false;false;false;false;false;false;true]]. |
---|
160 | definition BVfalse: beval ≝ BVByte (zero …). |
---|
161 | definition beval_of_bool : bool → beval ≝ λb. if b then BVtrue else BVfalse. |
---|