source: src/common/ByteValues.ma @ 2275

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