source: src/joint/BEValues.ma @ 1228

Last change on this file since 1228 was 1213, checked in by sacerdot, 9 years ago

1) New values (joint/BEValues.ma) and memory model for the back-ends

(joint/BEMem.ma) where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/Pointers.ma and common/GenMem.ma shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in Mem.ma
(cut&paste code).

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