source: src/common/ByteValues.ma @ 2176

Last change on this file since 2176 was 2176, checked in by campbell, 7 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File size: 6.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".
6
7record 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
24inductive beval: Type[0] ≝
25  | BVundef: beval
26  | BVByte: Byte → beval
27  | BVnull: (*∀r:region.*) part  → beval
28  | BVptr: ∀p:pointer. part (*ptype p*) → beval.
29
30definition 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 p1    ⇒ match v2 with [ BVnull p2    ⇒ eqb p1 p2                      | _ ⇒ false ]
36   | BVptr P1 p1  ⇒ match v2 with [ BVptr P2 p2  ⇒ eq_pointer … P1 P2 ∧ eqb p1 p2 | _ ⇒ false ]].
37
38axiom CorruptedValue: String.
39
40let 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
56axiom 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 *)
60definition 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)? *)
72let 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
78definition bevals_of_pointer: pointer → list beval ≝
79 λp. bevals_of_pointer_aux p 0 (size_pointer (*ptype p*)) ….
80// qed.
81
82lemma pointer_of_bevals_bevals_of_pointer:
83 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
84* #pbl #poff
85try %
86whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) (*[2,3: %]*)
87whd in ⊢ (??%?);(* >reflexive_eq_pointer >(eqb_n_n 2)*) %
88qed.
89
90(* CSC: move elsewhere *)
91(* CSC: Wrong data-type? Use products of products *)
92definition 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
95qed.
96
97axiom NotATwoBytesPointer: String.
98
99(* Fails if the address is not representable as a pair *)
100definition beval_pair_of_pointer: pointer → res (beval × beval) ≝
101 λp. OK … (list_to_pair … (bevals_of_pointer p) ?).
102(*
103 λp. match p with [ mk_pointer pty pbl pok poff ⇒
104  match pty with
105   [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?)
106   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
107   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
108% qed.
109
110definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝
111 λp. list_to_pair ? (bevals_of_pointer p) ?.
112(*
113 λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒
114  match pty return λpty. ? → pty = Code → ? with
115   [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ?
116   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
117[@(pi2 … p) |7: // |8: %] destruct (abs)*) %
118qed.
119
120
121axiom NotACodePointer: String.
122definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
123 λp.
124  let 〈v1,v2〉 ≝ p in
125  do p ← pointer_of_bevals [v1;v2] ;
126  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
127  [ Code ⇒ λE.OK ? (mk_Sig … p ?)
128  | _ ⇒ λ_.Error … [MSG NotACodePointer]] ?.
129// qed.
130
131axiom ValueNotABoolean: String.
132
133definition bool_of_beval: beval → res bool ≝
134 λv.match v with
135  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
136  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
137  | BVnull y ⇒  OK … false
138  | BVptr p q ⇒ OK ? true ].
139
140axiom BadByte: String.
141
142definition Byte_of_val: beval → res Byte ≝ (*CSC: move elsewhere *)
143 λb.match b with
144  [ BVByte b ⇒ OK … b
145  | _ ⇒ Error … [MSG BadByte]].
146
147axiom NotAnInt32Val: String.
148definition Word_of_list_beval: list beval → res int ≝
149 λl.
150  let first_byte ≝ λl.
151   match l with
152    [ nil ⇒ Error ? [MSG NotAnInt32Val]
153    | cons hd tl ⇒ do b ← Byte_of_val hd ; OK ? 〈b,tl〉 ] in
154  do 〈b1,l〉 ← first_byte l ;
155  do 〈b2,l〉 ← first_byte l ;
156  do 〈b3,l〉 ← first_byte l ;
157  do 〈b4,l〉 ← first_byte l ;
158   match l with
159    [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1)
160    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
161
162(* CSC: maybe we should introduce a type of 1-bit-sized values *)
163definition BVtrue: beval ≝ BVByte [[false;false;false;false;false;false;false;true]].
164definition BVfalse: beval ≝ BVByte (zero …).
165definition beval_of_bool : bool → beval ≝ λb. if b then BVtrue else BVfalse.
Note: See TracBrowser for help on using the repository browser.