Ignore:
Timestamp:
Nov 14, 2012, 10:31:55 AM (7 years ago)
Author:
tranquil
Message:

separated in back end values program counters from code pointers (intended to hold function pointers only): same signature, but separation needed the proof of some passes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues.ma

    r2443 r2462  
    55include "common/Pointers.ma".
    66include "utilities/hide.ma".
     7
     8definition cpointer ≝ Σp.ptype p = Code.
     9definition xpointer ≝ Σp.ptype p = XData.
     10unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
     11unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
    712
    813record part (*r: region*): Type[0] ≝
     
    3742  | BVByte: Byte → beval
    3843  | BVnull: (*∀r:region.*) part  → beval
    39   | BVptr: pointer → part → beval.
     44  | BVptr: pointer → part → beval
     45  | BVpc: cpointer → part → beval. (* only used in back end, needed to separate
     46                                      program counters that go in the stack from
     47                                      function pointers, as they are linked with
     48                                      different relations in some passes *)
    4049
    4150definition eq_bv_suffix : ∀n,m,p.
     
    8089  ].
    8190
     91definition pc_of_bevals: list beval → res cpointer ≝
     92 λl.
     93 match l with
     94  [ nil ⇒ Error … [MSG CorruptedPointer]
     95  | cons bv1 tl ⇒
     96    match tl with
     97    [ nil ⇒ Error … [MSG CorruptedPointer]
     98    | cons bv2 tl' ⇒
     99      match tl' with
     100      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
     101      | nil ⇒
     102        match bv1 with
     103        [ BVpc ptr1 p1 ⇒
     104          match bv2 with
     105          [ BVpc ptr2 p2 ⇒
     106            if eqb p1 0 ∧ eqb p2 1 ∧ eq_pointer ptr1 ptr2 then
     107              return ptr2
     108            else Error … [MSG CorruptedPointer]
     109          | _ ⇒ Error … [MSG CorruptedPointer]
     110          ]
     111        | _ ⇒ Error … [MSG CorruptedPointer]
     112        ]
     113      ]
     114    ]
     115  ].
     116
    82117definition bevals_of_pointer ≝
    83118 λp:pointer.
    84119 map ?? (λn_sig.BVptr p (part_from_sig n_sig)) (range_strong size_pointer).
     120
     121definition bevals_of_pc ≝
     122 λp:cpointer.
     123 map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer).
    85124
    86125lemma pointer_of_bevals_bevals_of_pointer:
     
    92131change with (eq_bv ???) in match (eq_bv_suffix ?????);
    93132>eq_bv_refl %
     133qed.
     134
     135lemma pc_of_bevals_bevals_of_pc:
     136 ∀p. pc_of_bevals (bevals_of_pc p) = OK … p.
     137#ptr
     138whd in match (bevals_of_pc ?);
     139whd in ⊢ (??%?);
     140>reflexive_eq_pointer
     141%
    94142qed.
    95143
     
    114162   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
    115163
    116 definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝
    117  λp. list_to_pair ? (bevals_of_pointer p) (refl …).
    118 (*
    119  λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒
    120   match pty return λpty. ? → pty = Code → ? with
    121    [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ?
    122    | _ ⇒ λpok'.λabs. ⊥] pok] ?.
    123 [@(pi2 … p) |7: // |8: %] destruct (abs)*)
    124 
    125 axiom NotACodePointer: String.
     164definition beval_pair_of_pc: cpointer → beval × beval ≝
     165 λp. list_to_pair ? (bevals_of_pc p) (refl …).
     166
     167(* axiom NotACodePointer: String.
    126168definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
    127169 λp.
     
    130172  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
    131173  [ Code ⇒ λE.OK ? (mk_Sig … p E)
    132   | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …).
     174  | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *)
    133175
    134176axiom ValueNotABoolean: String.
     
    142184                                                   series of XORs has been
    143185                                                   completed *)
     186  | BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *)
    144187  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
    145188  | BVnull _ ⇒  OK … false
Note: See TracChangeset for help on using the changeset viewer.