Changeset 1452


Ignore:
Timestamp:
Oct 22, 2011, 4:26:01 AM (8 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1451 r1452  
    2121(****************************************************************************)
    2222
    23 (*CSC: XXXXXXXXXXXXXXXXX bug here; we need to change the encoding so that
    24   the block is the one of the function and the offset corresponds to the
    25   label. Code pointer arithmetics must be prevented in another way, i.e.
    26   by not allowing any increment/decrement on Code regions (with the
    27   exception of LIN's succ_pc function). If we don't do that, then the
    28   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 that
    30   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 pointers
    33   in other functions. However, there could be simpler ways to invalidate
    34   pointer arithmetics on Code pointers.
    35 *)
    3623definition graph_pointer_of_label0:
    3724 pointer → label → Σp:pointer. ptype p = Code ≝
    3825 λoldpc,l.
    3926  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))).
    4228// qed.
    4329
     
    4733  OK ? (graph_pointer_of_label0 oldpc l).
    4834
    49 (*CSC: XXXX; inverse of the previous function, but it does not check that
    50   the offset is zero and thus it never fails. *)
    5135definition graph_label_of_pointer: pointer → res label ≝
    52  λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))).
     36 λp. OK … (an_identifier ? (bitvector_of_nat … (abs (offv (poff p))))).
    5337
    5438(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
Note: See TracChangeset for help on using the changeset viewer.