Ignore:
Timestamp:
Feb 11, 2011, 4:45:38 PM (9 years ago)
Author:
campbell
Message:

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Values.ma

    r498 r500  
    4444] qed.
    4545
     46(* pointer_compat block_region pointer_region *)
     47
     48inductive pointer_compat : block → region → Prop ≝
     49|        same_compat : ∀s,id. pointer_compat (mk_block s id) s
     50|      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
     51|   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
     52
     53lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
     54* * #id *;
     55try ( %1 // )
     56%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
     57qed.
     58
     59definition is_pointer_compat : block → region → bool ≝
     60λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
     61
    4662(* * A value is either:
    4763- a machine integer;
     
    6076  | Vfloat: float → val
    6177  | Vnull: region → val
    62   | Vptr: region → block → int → val.
     78  | Vptr: ∀r:region. ∀b:block. pointer_compat b r → int → val.
    6379
    6480definition Vzero: val ≝ Vint zero.
     
    101117  match v with
    102118  [ Vint n ⇒ n ≠ zero
    103   | Vptr _ b ofs ⇒ True
     119  | Vptr _ b _ ofs ⇒ True
    104120  | _ ⇒ False
    105121  ].
     
    118134      bool_of_val (Vint zero) false
    119135  | bool_of_val_ptr:
    120       ∀r,b,ofs. bool_of_val (Vptr r b ofs) true
     136      ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true
    121137  | bool_of_val_null:
    122138      ∀r. bool_of_val (Vnull r) true.
     
    175191  match v with
    176192  [ Vint n ⇒ of_bool (int_eq n zero)
    177   | Vptr _ b ofs ⇒ Vfalse
     193  | Vptr _ b _ ofs ⇒ Vfalse
    178194  | Vnull _ ⇒ Vtrue
    179195  | _ ⇒ Vundef
     
    203219  [ Vint n1 ⇒ match v2 with
    204220    [ Vint n2 ⇒ Vint (add n1 n2)
    205     | Vptr pty b2 ofs2 ⇒ Vptr pty b2 (add ofs2 n1)
    206     | _ ⇒ Vundef ]
    207   | Vptr pty b1 ofs1 ⇒ match v2 with
    208     [ Vint n2 ⇒ Vptr pty b1 (add ofs1 n2)
     221    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (add ofs2 n1)
     222    | _ ⇒ Vundef ]
     223  | Vptr r b1 p ofs1 ⇒ match v2 with
     224    [ Vint n2 ⇒ Vptr r b1 p (add ofs1 n2)
    209225    | _ ⇒ Vundef ]
    210226  | _ ⇒ Vundef ].
     
    215231    [ Vint n2 ⇒ Vint (sub n1 n2)
    216232    | _ ⇒ Vundef ]
    217   | Vptr pty1 b1 ofs1 ⇒ match v2 with
    218     [ Vint n2 ⇒ Vptr pty1 b1 (sub ofs1 n2)
    219     | Vptr pty2 b2 ofs2 ⇒
     233  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     234    [ Vint n2 ⇒ Vptr r1 b1 p1 (sub ofs1 n2)
     235    | Vptr r2 b2 p2 ofs2 ⇒
    220236        if eq_block b1 b2 then Vint (sub ofs1 ofs2) else Vundef
    221237    | _ ⇒ Vundef ]
     
    387403    [ Vint n2 ⇒ of_bool (cmp c n1 n2)
    388404    | _ ⇒ Vundef ]
    389   | Vptr r1 b1 ofs1 ⇒ match v2 with
    390     [ Vptr r2 b2 ofs2 ⇒
     405  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     406    [ Vptr r2 b2 p2 ofs2 ⇒
    391407        if eq_block b1 b2
    392408        then of_bool (cmp c ofs1 ofs2)
     
    395411    | _ ⇒ Vundef ]
    396412  | Vnull r1 ⇒ match v2 with
    397     [ Vptr _ _ _ ⇒ cmp_mismatch c
     413    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
    398414    | Vnull r2 ⇒ cmp_match c
    399415    | _ ⇒ Vundef
     
    406422    [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
    407423    | _ ⇒ Vundef ]
    408   | Vptr r1 b1 ofs1 ⇒ match v2 with
    409     [ Vptr r2 b2 ofs2 ⇒
     424  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     425    [ Vptr r2 b2 p2 ofs2 ⇒
    410426        if eq_block b1 b2
    411427        then of_bool (cmpu c ofs1 ofs2)
     
    414430    | _ ⇒ Vundef ]
    415431  | Vnull r1 ⇒ match v2 with
    416     [ Vptr _ _ _ ⇒ cmp_mismatch c
     432    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
    417433    | Vnull r2 ⇒ cmp_match c
    418434    | _ ⇒ Vundef
     
    447463    | _ ⇒ Vundef
    448464    ]
    449   | Vptr r b ofs ⇒
     465  | Vptr r b p ofs ⇒
    450466    match chunk with
    451     [ Mpointer r' ⇒ if eq_region r r' then Vptr r b ofs else Vundef
     467    [ Mpointer r' ⇒ if eq_region r r' then Vptr r b p ofs else Vundef
    452468    | _ ⇒ Vundef
    453469    ]
Note: See TracChangeset for help on using the changeset viewer.