Changeset 124 for C-semantics/Values.ma


Ignore:
Timestamp:
Sep 24, 2010, 10:31:32 AM (10 years ago)
Author:
campbell
Message:

Initial work on Clight semantics with 8051 memory spaces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Values.ma

    r14 r124  
    3636*)
    3737
     38ninductive ptr_class : Type ≝
     39| Universal : ptr_class
     40| Data : ptr_class
     41| IData : ptr_class
     42| XData : ptr_class
     43(* pdata?  I'd rather not... *)
     44| Code : ptr_class.
     45
     46ninductive ptr_class_compat : ptr_class → ptr_class → Prop ≝
     47| ptr_class_same : ∀pcl. ptr_class_compat pcl pcl
     48| ptr_univ_l : ∀pcl. ptr_class_compat Universal pcl
     49| ptr_univ_r : ∀pcl. ptr_class_compat pcl Universal.
     50
     51nlemma ptr_class_compat_sym : ∀p,p'. ptr_class_compat p p' → ptr_class_compat p' p.
     52#p p' H; ninversion H; //; nqed.
     53
     54(* TODO: should comparison and subtraction of pointers of different sorts
     55         be supported? *)
     56
    3857ninductive val: Type[0] ≝
    3958  | Vundef: val
    4059  | Vint: int -> val
    4160  | Vfloat: float -> val
    42   | Vptr: block -> int -> val.
     61  | Vptr: ptr_class → block -> int -> val.
    4362
    4463ndefinition Vzero: val ≝ Vint zero.
     
    6382  | Vint _ ⇒ match t with [ Tint ⇒ True | _ ⇒ False ]
    6483  | Vfloat _ ⇒ match t with [ Tfloat ⇒ True | _ ⇒ False ]
    65   | Vptr _ _ ⇒ match t with [ Tint ⇒ True | _ ⇒ False ]
     84  | Vptr _ _ _ ⇒ match t with [ Tint ⇒ True | _ ⇒ False ]
    6685  | _ ⇒ False
    6786  ].
     
    81100  match v with
    82101  [ Vint n ⇒ n ≠ zero
    83   | Vptr b ofs ⇒ True
     102  | Vptr _ b ofs ⇒ True
    84103  | _ ⇒ False
    85104  ].
     
    97116      bool_of_val (Vint zero) false
    98117  | bool_of_val_ptr:
    99       ∀b,ofs. bool_of_val (Vptr b ofs) true.
     118      ∀pty,b,ofs. bool_of_val (Vptr pty b ofs) true.
    100119
    101120ndefinition neg : val → val ≝ λv.
     
    152171  match v with
    153172  [ Vint n ⇒ of_bool (int_eq n zero)
    154   | Vptr b ofs ⇒ Vfalse
     173  | Vptr _ b ofs ⇒ Vfalse
    155174  | _ ⇒ Vundef
    156175  ].
     
    178197  [ Vint n1 ⇒ match v2 with
    179198    [ Vint n2 ⇒ Vint (add n1 n2)
    180     | Vptr b2 ofs2 ⇒ Vptr b2 (add ofs2 n1)
    181     | _ ⇒ Vundef ]
    182   | Vptr b1 ofs1 ⇒ match v2 with
    183     [ Vint n2 ⇒ Vptr b1 (add ofs1 n2)
     199    | Vptr pty b2 ofs2 ⇒ Vptr pty b2 (add ofs2 n1)
     200    | _ ⇒ Vundef ]
     201  | Vptr pty b1 ofs1 ⇒ match v2 with
     202    [ Vint n2 ⇒ Vptr pty b1 (add ofs1 n2)
    184203    | _ ⇒ Vundef ]
    185204  | _ ⇒ Vundef ].
     
    190209    [ Vint n2 ⇒ Vint (sub n1 n2)
    191210    | _ ⇒ Vundef ]
    192   | Vptr b1 ofs1 ⇒ match v2 with
    193     [ Vint n2 ⇒ Vptr b1 (sub ofs1 n2)
    194     | Vptr b2 ofs2 ⇒
     211  | Vptr pty1 b1 ofs1 ⇒ match v2 with
     212    [ Vint n2 ⇒ Vptr pty1 b1 (sub ofs1 n2)
     213    | Vptr pty2 b2 ofs2 ⇒
    195214        if eqZb b1 b2 then Vint (sub ofs1 ofs2) else Vundef
    196215    | _ ⇒ Vundef ]
     
    352371  [ Vint n1 ⇒ match v2 with
    353372    [ Vint n2 ⇒ of_bool (cmp c n1 n2)
    354     | Vptr b2 ofs2 ⇒
     373    | Vptr pty2 b2 ofs2 ⇒
    355374        if eq n1 zero then cmp_mismatch c else Vundef
    356375    | _ ⇒ Vundef ]
    357   | Vptr b1 ofs1 ⇒ match v2 with
    358     [ Vptr b2 ofs2 ⇒
     376  | Vptr pty1 b1 ofs1 ⇒ match v2 with
     377    [ Vptr pty2 b2 ofs2 ⇒
    359378        if eqZb b1 b2
    360379        then of_bool (cmp c ofs1 ofs2)
     
    369388  [ Vint n1 ⇒ match v2 with
    370389    [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
    371     | Vptr b2 ofs2 ⇒
     390    | Vptr pty2 b2 ofs2 ⇒
    372391        if eq n1 zero then cmp_mismatch c else Vundef
    373392    | _ ⇒ Vundef ]
    374   | Vptr b1 ofs1 ⇒ match v2 with
    375     [ Vptr b2 ofs2 ⇒
     393  | Vptr pty1 b1 ofs1 ⇒ match v2 with
     394    [ Vptr pty2 b2 ofs2 ⇒
    376395        if eqZb b1 b2
    377396        then of_bool (cmpu c ofs1 ofs2)
     
    409428    | _ ⇒ Vundef
    410429    ]
    411   | Vptr b ofs ⇒
     430  | Vptr pty b ofs ⇒
    412431    match chunk with
    413     [ Mint32 ⇒ Vptr b ofs
     432    [ Mint32 ⇒ Vptr pty b ofs
    414433    | _ ⇒ Vundef
    415434    ]
Note: See TracChangeset for help on using the changeset viewer.