Changeset 1452 for src/joint

Timestamp:

Oct 22, 2011, 4:26:01 AM (9 years ago)

Author:

sacerdot

Message:

Bug fixed: labels MUST be represented as pointers whose block is the block of
the function the label is defined in. This invariant is used later everywhere to
retrieve the function given the pointer.

File:

• src/joint/SemanticUtils.ma (modified) (2 diffs)

src/joint/SemanticUtils.ma

@@ -21 +21 @@
 (****************************************************************************)
 
-(*CSC: XXXXXXXXXXXXXXXXX bug here; we need to change the encoding so that
-  the block is the one of the function and the offset corresponds to the
-  label. Code pointer arithmetics must be prevented in another way, i.e.
-  by not allowing any increment/decrement on Code regions (with the
-  exception of LIN's succ_pc function). If we don't do that, then the
-  find_funct_ptr (e.g. in graph_fetch_statement) are not correct! *)
-(*CSC: XXXX; do we need to create a brand new chunk per label, so that
-  pointer operations on labels are not semantically valid?
-  ATM, the pointers are not valid (they do not point to allocated regions)
-  and, moreover, they conflict with function blocks and with other pointers
-  in other functions. However, there could be simpler ways to invalidate
-  pointer arithmetics on Code pointers.
-*)
 definition graph_pointer_of_label0:
  pointer → label → Σp:pointer. ptype p = Code ≝
  λoldpc,l.
   mk_pointer Code
-   (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l))))
-   ? (mk_offset OZ). 
+   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (nat_of_bitvector ? (word_of_identifier … l))). 
 // qed.
 
@@ -47 +33 @@
   OK ? (graph_pointer_of_label0 oldpc l). 
 
-(*CSC: XXXX; inverse of the previous function, but it does not check that
-  the offset is zero and thus it never fails. *)
 definition graph_label_of_pointer: pointer → res label ≝
- λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))).
+ λp. OK … (an_identifier ? (bitvector_of_nat … (abs (offv (poff p))))).
 
 (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.