source: src/common/ByteValues.ma @ 2927

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

stupid bug in bool_of_beval

File size: 9.5 KB
RevLine 
[1213]1(* Type of values used in the dynamic semantics of the back-end intermediate
[1987]2   languages, and the memory model for the whole compiler. Inspired by
3   common/Values.ma, adapted from Compcert *)
[1213]4
5include "common/Pointers.ma".
[2286]6include "utilities/hide.ma".
[1213]7
[2608]8
[2462]9definition cpointer ≝ Σp.ptype p = Code.
10definition xpointer ≝ Σp.ptype p = XData.
11unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
12unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
13
[2608]14
[2470]15(* this is like a code pointer, but with unbounded offset.
16   used only in the back-end, they become code pointers in LIN → ASM *)
17record program_counter : Type[0] ≝
18  { pc_block : Σb : block.block_region b = Code
19  ; pc_offset : Pos
20  }.
21
22definition eq_program_counter : program_counter → program_counter → bool ≝
23λpc1,pc2.eq_block (pc_block pc1) (pc_block pc2) ∧
24         eqb (pc_offset pc1) (pc_offset pc2).
25
26lemma eq_program_counter_elim : ∀P:bool→Prop.
27  ∀pc1,pc2.(pc1=pc2→P true)→(pc1≠pc2→P false)→P (eq_program_counter pc1 pc2).
28#P ** #bl1 #H1 #o1 ** #bl2 #H2 #o2
29#Heq #Hneq whd in ⊢ (?%);
30@eq_block_elim #EQ1
31[ @eqb_elim #EQ2 ]
32[ @Heq destruct %
33|*: @Hneq % #ABS destruct
34  [ @(absurd ?? EQ2) | @(absurd ?? EQ1) ] %
35] qed.
36
37lemma reflexive_eq_program_counter : ∀pc.eq_program_counter pc pc = true.
38** #bl1 #H1 #o1 whd in ⊢ (??%?); >eq_block_b_b >eqb_n_n % qed.
39
40definition bitvector_from_pos :
41  ∀n.Pos → BitVector n ≝
42  λn,p.bitvector_of_Z n (Zpred (pos p)).
43
44definition pos_from_bitvector :
45  ∀n.BitVector n → Pos ≝
46  λn,v.
47  match Zsucc (Z_of_unsigned_bitvector n v)
48  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
49  with
50  [ OZ ⇒ λprf.⊥
51  | pos x ⇒ λ_. x
52  | neg x ⇒ λprf.⊥
53  ] (refl …).
54@hide_prf
55elim v in prf;
56[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
57
58definition cpointer_of_pc : program_counter → option cpointer ≝
59  λpc.
60  let pc_off ≝ pc_offset pc in
61  if leb pc_off (two_power_nat offset_size) then
62    return «mk_pointer (pc_block pc) (mk_offset (bitvector_from_pos … pc_off)),?»
63  else
64    None ?.
65elim (pc_block pc) #bl #H @H qed.
66
[2176]67record part (*r: region*): Type[0] ≝
[1213]68 { part_no:> nat
[2176]69 ; part_no_ok: part_no < size_pointer (*r*)
[1213]70 }.
71
[2435]72definition part_from_sig : (Σn:ℕ.n<size_pointer) → part ≝
73λn_sig : Σn.n<size_pointer.mk_part n_sig (pi2 … n_sig).
74
75coercion sig_to_part : ∀n_sig:Σn:ℕ.n<size_pointer.part ≝
76part_from_sig on _n_sig:Σn.n<size_pointer to part.
77
[1213]78(* Byte-sized values used in the back-end.
79   Values larger than a single Byte are represented via their parts.
80   Values are either:
81  - machine integers (Bytes)
82  - parts of a pointer seen as a triple giving the representation of the
83    pointer (in terms of the memory regions such a pointer could address),
84    a memory address and an integer offset with respect to this address;
85  - a null pointer: the region denotes the pointer size
86  - the [BVundef] value denoting an arbitrary bit pattern, such as the
87    value of an uninitialized variable
[2435]88  - [BVXor] is a formal XOR between (possibly null) pointer parts
89  - [BVnonzero] is any nonzero value
[1213]90*)
91
92inductive beval: Type[0] ≝
93  | BVundef: beval
[2286]94  | BVnonzero: beval
[2435]95  | BVXor: option pointer → option pointer → part → beval (* option pointer ≈ pointer + null *)
[1213]96  | BVByte: Byte → beval
[2176]97  | BVnull: (*∀r:region.*) part  → beval
[2462]98  | BVptr: pointer → part → beval
[2470]99  | BVpc: program_counter → part → beval. (* only used in back end, needed to separate
[2462]100                                      program counters that go in the stack from
101                                      function pointers, as they are linked with
102                                      different relations in some passes *)
[1213]103
[2435]104definition eq_bv_suffix : ∀n,m,p.
105  BitVector (n + p) → BitVector (m + p) → bool ≝
106λn,m,p,v1,v2.
107let b1 ≝ \snd (vsplit … v1) in
108let b2 ≝ \snd (vsplit … v2) in
109eq_bv … b1 b2.
[1213]110
[2286]111include alias "arithmetics/nat.ma".
[1213]112
113(* CSC: use vectors in place of lists? Or even better products of tuples
114   (more easily pattern matchable in the finite case)? requires one more parameter *)
115definition pointer_of_bevals: list beval → res pointer ≝
116 λl.
117 match l with
[2286]118  [ nil ⇒ Error … [MSG CorruptedPointer]
[2435]119  | cons bv1 tl ⇒
120    match tl with
121    [ nil ⇒ Error … [MSG CorruptedPointer]
122    | cons bv2 tl' ⇒
123      match tl' with
124      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
125      | nil ⇒
126        match bv1 with
127        [ BVptr ptr1 p1 ⇒
128          match bv2 with
129          [ BVptr ptr2 p2 ⇒
130            if eqb p1 0 ∧ eqb p2 1 ∧ eq_block (pblock ptr1) (pblock ptr2) ∧
131               eq_bv_suffix 8 8 8 (offv (poff ptr1)) (offv (poff ptr2))
132            then
133              return ptr2
134            else Error … [MSG CorruptedPointer]
135          | _ ⇒ Error … [MSG CorruptedPointer]
136          ]
137        | _ ⇒ Error … [MSG CorruptedPointer]
138        ]
[2286]139      ]
[2435]140    ]
[2286]141  ].
[1213]142
[2470]143definition pc_of_bevals: list beval → res program_counter ≝
[2462]144 λl.
145 match l with
146  [ nil ⇒ Error … [MSG CorruptedPointer]
147  | cons bv1 tl ⇒
148    match tl with
149    [ nil ⇒ Error … [MSG CorruptedPointer]
150    | cons bv2 tl' ⇒
151      match tl' with
152      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
153      | nil ⇒
154        match bv1 with
155        [ BVpc ptr1 p1 ⇒
156          match bv2 with
157          [ BVpc ptr2 p2 ⇒
[2470]158            if eqb p1 0 ∧ eqb p2 1 ∧ eq_program_counter ptr1 ptr2 then
[2462]159              return ptr2
160            else Error … [MSG CorruptedPointer]
161          | _ ⇒ Error … [MSG CorruptedPointer]
162          ]
163        | _ ⇒ Error … [MSG CorruptedPointer]
164        ]
165      ]
166    ]
167  ].
168
[2435]169definition bevals_of_pointer ≝
170 λp:pointer.
171 map ?? (λn_sig.BVptr p (part_from_sig n_sig)) (range_strong size_pointer).
[1213]172
[2462]173definition bevals_of_pc ≝
[2470]174 λp:program_counter.
[2462]175 map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer).
176
[1213]177lemma pointer_of_bevals_bevals_of_pointer:
178 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
[2435]179#ptr
[2286]180whd in match (bevals_of_pointer ?);
181whd in ⊢ (??%?);
[2435]182>eq_block_b_b
183change with (eq_bv ???) in match (eq_bv_suffix ?????);
184>eq_bv_refl %
[1213]185qed.
186
[2462]187lemma pc_of_bevals_bevals_of_pc:
188 ∀p. pc_of_bevals (bevals_of_pc p) = OK … p.
189#ptr
190whd in match (bevals_of_pc ?);
191whd in ⊢ (??%?);
[2470]192>reflexive_eq_program_counter
[2462]193%
194qed.
195
[1213]196(* CSC: move elsewhere *)
197(* CSC: Wrong data-type? Use products of products *)
198definition list_to_pair: ∀A:Type[0]. ∀l:list A. length … l = 2 → A × A.
199 #A #l cases l [2: #a #tl cases tl [2: #b #tl' cases tl' [1: #_ @〈a,b〉 | #c #tl'']]]
200 #abs normalize in abs; destruct
201qed.
202
[2443]203(* Should fail if the address is not representable as a pair
204   As we only have 16 bit addresses atm, it never fails *)
205definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝
206 λp.list_to_pair … (bevals_of_pointer p) (refl …).
[2176]207(*
[1213]208 λp. match p with [ mk_pointer pty pbl pok poff ⇒
209  match pty with
210   [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?)
211   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
[2176]212   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
[1213]213
[2470]214definition beval_pair_of_pc: program_counter → beval × beval ≝
[2462]215 λp. list_to_pair ? (bevals_of_pc p) (refl …).
[1395]216
[2645]217(*
[1395]218definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
219 λp.
220  let 〈v1,v2〉 ≝ p in
221  do p ← pointer_of_bevals [v1;v2] ;
222  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
[2435]223  [ Code ⇒ λE.OK ? (mk_Sig … p E)
[2462]224  | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *)
[1395]225
[1213]226definition bool_of_beval: beval → res bool ≝
227 λv.match v with
228  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
[2435]229  | BVXor _ _ _ ⇒ Error … [MSG ValueNotABoolean] (* even if in some cases we can
230                                                   tell the value, we will always
231                                                   call bool_of_beval after a
232                                                   series of XORs has been
233                                                   completed *)
[2462]234  | BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *)
[2927]235  | BVByte b ⇒ OK … (¬eq_bv … (zero …) b)
[2435]236  | BVnull _ ⇒  OK … false
237  | _ ⇒ OK ? true
238  ].
[1213]239
[2645]240definition Byte_of_val: ErrorMessage → beval → res Byte ≝ (*CSC: move elsewhere *)
[2286]241 λerr,b.match b with
[1213]242  [ BVByte b ⇒ OK … b
[2286]243  | _ ⇒ Error … [MSG err]].
[1213]244
[1359]245definition Word_of_list_beval: list beval → res int ≝
246 λl.
247  let first_byte ≝ λl.
248   match l with
249    [ nil ⇒ Error ? [MSG NotAnInt32Val]
[2286]250    | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in
[1359]251  do 〈b1,l〉 ← first_byte l ;
252  do 〈b2,l〉 ← first_byte l ;
253  do 〈b3,l〉 ← first_byte l ;
254  do 〈b4,l〉 ← first_byte l ;
255   match l with
256    [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1)
257    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
258
[2927]259inductive add_or_sub : Type[0] ≝
260| do_add : add_or_sub
261| do_sub : add_or_sub.
262
263definition eq_add_or_sub : add_or_sub → add_or_sub → bool ≝
264λx,y.match x with
265[ do_add ⇒ match y with [ do_add ⇒ true | _ ⇒ false ]
266| do_sub ⇒ match y with [ do_sub ⇒ true | _ ⇒ false ]
267].
268
[2286]269inductive bebit : Type[0] ≝
270| BBbit : bool → bebit
271| BBundef : bebit
272| BBptrcarry :
[2927]273  add_or_sub → pointer → ∀p : part.BitVector (8*S p) → bebit.
[2275]274
[2645]275definition Bit_of_val: ErrorMessage → bebit → res Bit ≝ (*CSC: move elsewhere *)
[2286]276 λerr,b.match b with
277  [ BBbit b ⇒ OK … b
[2645]278  | _ ⇒ Error … [MSG err]].
Note: See TracBrowser for help on using the repository browser.