- Timestamp:
- Oct 22, 2011, 4:26:01 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/SemanticUtils.ma
r1451 r1452 21 21 (****************************************************************************) 22 22 23 (*CSC: XXXXXXXXXXXXXXXXX bug here; we need to change the encoding so that24 the block is the one of the function and the offset corresponds to the25 label. Code pointer arithmetics must be prevented in another way, i.e.26 by not allowing any increment/decrement on Code regions (with the27 exception of LIN's succ_pc function). If we don't do that, then the28 find_funct_ptr (e.g. in graph_fetch_statement) are not correct! *)29 (*CSC: XXXX; do we need to create a brand new chunk per label, so that30 pointer operations on labels are not semantically valid?31 ATM, the pointers are not valid (they do not point to allocated regions)32 and, moreover, they conflict with function blocks and with other pointers33 in other functions. However, there could be simpler ways to invalidate34 pointer arithmetics on Code pointers.35 *)36 23 definition graph_pointer_of_label0: 37 24 pointer → label → Σp:pointer. ptype p = Code ≝ 38 25 λoldpc,l. 39 26 mk_pointer Code 40 (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l)))) 41 ? (mk_offset OZ). 27 (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (nat_of_bitvector ? (word_of_identifier … l))). 42 28 // qed. 43 29 … … 47 33 OK ? (graph_pointer_of_label0 oldpc l). 48 34 49 (*CSC: XXXX; inverse of the previous function, but it does not check that50 the offset is zero and thus it never fails. *)51 35 definition graph_label_of_pointer: pointer → res label ≝ 52 λp. OK … (an_identifier ? (bitvector_of_nat … (abs ( block_id (pblockp))))).36 λp. OK … (an_identifier ? (bitvector_of_nat … (abs (offv (poff p))))). 53 37 54 38 (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
Note: See TracChangeset
for help on using the changeset viewer.