source: src/common/ByteValues.ma @ 2443

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

changed joint's stack pointer and internal stack

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