source: src/joint/BEMem.ma

Last change on this file was 2437, checked in by tranquil, 8 years ago

generalised calls to calls with pointers

File size: 4.5 KB
RevLine 
[1213]1(* Memory model used in the dynamic semantics of the back-end intermediate
2   languages. Inspired by common/Mem.ma, adapted from Compcert *)
3
4(* * This file develops the memory model that is used in the dynamic
5  semantics of all the languages used in the compiler.
6  It defines a type [mem] of memory states, the following 4 basic
7  operations over memory states, and their properties:
8- [load]: read a memory chunk at a given address;
9- [store]: store a memory chunk at a given address;
10- [alloc]: allocate a fresh memory block;
11- [free]: invalidate a memory block.
12*)
13
[1987]14include "common/ByteValues.ma".
[1213]15include "common/GenMem.ma".
16
[1988]17definition bemem ≝ mem.
[1213]18
[1882]19definition is_addressable : region → bool ≝ λr.match r with
20  [ XData ⇒ true | Code ⇒ true | _ ⇒ false ].
21
[1329]22(* CSC: only pointers to XRAM or code memory ATM *)
23definition address ≝ beval × beval.
[2286]24
[1329]25definition pointer_of_address: address → res pointer ≝
26 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
[2286]27
[2437]28definition is_address : (beval × beval) → Prop ≝ λa.
29  ∃ptr.pointer_of_address a = OK … ptr.
30
[2286]31lemma bevals_of_pointer_is_address :
32  ∀p.is_address (list_to_pair … (bevals_of_pointer p) (refl …)).
[2437]33* #bl #o
34whd in ⊢ (?%); whd %
35[2: whd in ⊢ (??%?);
36  >eq_block_b_b
37  change with (eq_bv ???) in match (eq_bv_suffix ?????);
38  >eq_bv_refl normalize %]
[1882]39qed.
[2286]40
[2176]41(* For full 8051 memory spaces
[1882]42definition pointer_compat' ≝ λb,r.
43  match b with
44  [ mk_block r' z ⇒
45    if eq_region r' r then True
46    else
47      match r with
48      [ Any ⇒ True
49      | XData ⇒ match r' with
50        [ PData ⇒ True
51        | _ ⇒ False
52        ]
53      | _ ⇒ False
54      ]
55   ].
56
57lemma pointer_compat_to_ind : ∀b,r.pointer_compat' b r → pointer_compat b r.
58** #z ** //
59qed.
60
61lemma pointer_compat_from_ind : ∀b,r.pointer_compat b r → pointer_compat' b r.
62#b #r #H inversion H
63[ #s #id #EQ1 #EQ2 #EQ3 whd >reflexive_eq_region %
64| #id #EQ1 #EQ2 #EQ3 %
65| #r #id #EQ1 #EQ2 #EQ3 whd @eq_region_elim #EQ4 destruct(EQ4) %
66]
67qed.
[2176]68*)
[2286]69(*lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
[2185]70** #a0 #a1 ***** #z #o
[2176]71#Hr
72(*
[1882]73** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr)
74cases r in Hr ⊢ %; #Hr *
[2176]75*)
[1882]76** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1
77destruct normalize
78@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
[2185]79change with (eq_bv ???) in match (eq_v ?????);
80@eq_bv_elim [2,4,6: * #ABS elim (ABS (refl …))]
[1882]81#_ #_ normalize %
[2286]82qed.*)
[1882]83   
[2286]84(*definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
[1882]85  do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».
86
87lemma address_of_pointer_is_safe :
88  ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address).
[2176]89#p normalize % qed.
90(*
[1882]91****#z #H
92lapply (pointer_compat_from_ind ?? H) * #o
93normalize %
[2176]94qed.*)
[1882]95
96definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝
97code_pointer_of_beval_pair.
98
[1395]99definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.
100
[1882]101definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer.
[2176]102cases H -H * #b #o normalize cases b * #z #EQ destruct
103%{«mk_pointer  (mk_block Code z)  o,I»}
104% [2: % [2: % [ % [ % ]]]] %
105qed.
106(*
[1882]107cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
108lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
109%{«mk_pointer ? (mk_block Code z) H o,I»}
110% [2: % [2: % [ % [ % ]] % |]|]
[2176]111qed.*)
[2286]112*)
[1882]113
114(* Paolo: why only code pointers and not XRAM too? *)
[2286]115(*definition addr_add: address → nat → res address ≝
[1329]116 λaddr,n.
[1395]117  do ptr ← code_pointer_of_address addr ;
118  OK … (address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
119normalize cases ptr #p #E @E
120qed.
[1329]121
[1882]122definition safe_addr_add: safe_address → nat → res safe_address ≝
123 λaddr,n.
124  do ptr ← code_pointer_of_address addr ;
125  OK … (safe_address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
126normalize cases ptr #p #E @E
127qed.
128
[1329]129definition addr_sub: address → nat → res address ≝
130 λaddr,n.
[1395]131  do ptr ← code_pointer_of_address addr ;
132  OK … (address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
133normalize cases ptr #p #E @E
[1882]134qed.
135
136definition safe_addr_sub: safe_address → nat → res safe_address ≝
137 λaddr,n.
138  do ptr ← code_pointer_of_address addr ;
139  OK … (safe_address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
140normalize cases ptr #p #E @E
[1993]141qed.
[2286]142*)
Note: See TracBrowser for help on using the repository browser.