Changeset 718


Ignore:
Timestamp:
Mar 29, 2011, 5:54:37 PM (9 years ago)
Author:
campbell
Message:

Add an AST type (i.e., intermediate language type) for pointers.

Location:
src
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/AST.ma

    r700 r718  
    3434[ #H %2 /2/; | #H %1 //; | #H %2 /2/ ] qed.
    3535
    36 (*
    37 (* XXX: we use nats for now, but if in future we use binary like compcert
    38         then the maps will be easier to define. *)
    39 definition ident ≝ nat.
    40 definition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
    41 #x elim x;
    42 [ #y cases y; /3/;
    43 | #x' #IH #y cases y;
    44   [ %{2} % #H destruct
    45   | #y' elim (IH y');
    46     [ #e destruct; /2/
    47     | #ne %{2} /2/;
    48     ]
    49   ]
    50 ] qed.
    51 *)
    52 (* * The intermediate languages are weakly typed, using only two types:
    53   [Tint] for integers and pointers, and [Tfloat] for floating-point
    54   numbers. *)
    55 
    56 inductive typ : Type[0] ≝
    57   | ASTint : typ
    58   | ASTfloat : typ.
    59 
    60 definition typesize : typ → Z ≝ λty.
    61   match ty return λ_.Z with  [ ASTint ⇒ 4 | ASTfloat ⇒ 8 ].
    62 
    63 lemma typesize_pos: ∀ty. typesize ty > 0.
    64 #ty cases ty; //; qed.
    65 
    66 lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    67 #t1 #t2 cases t1;cases t2;/2/; %2 @nmk #H destruct; qed.
    68 
    69 lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
    70 #t1 #t2 cases t1;cases t2;/2/;
    71 [ 1,2: #ty %2 @nmk #H destruct;
    72 | #ty1 #ty2 elim (typ_eq ty1 ty2); /2/; #neq %2 @nmk
    73     #H destruct; /2/;
    74 ] qed.
    75 
    76 (* * Additionally, function definitions and function calls are annotated
    77   by function signatures indicating the number and types of arguments,
    78   as well as the type of the returned value if any.  These signatures
    79   are used in particular to determine appropriate calling conventions
    80   for the function. *)
    81 
    82 record signature : Type[0] ≝ {
    83   sig_args: list typ;
    84   sig_res: option typ
    85 }.
    86 
    87 definition proj_sig_res : signature → typ ≝ λs.
    88   match sig_res s with
    89   [ None ⇒ ASTint
    90   | Some t ⇒ t
    91   ].
    92 
    9336(* Memory spaces *)
    9437
     
    12265definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
    12366#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
     67
     68definition size_pointer : region → Z ≝
     69λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
     70
     71(* * The intermediate languages are weakly typed, using only three types:
     72  [ASTint] for integers, [ASTptr] for pointers, and [ASTfloat] for floating-point
     73  numbers. *)
     74
     75inductive typ : Type[0] ≝
     76  | ASTint : typ
     77  | ASTptr : region → typ
     78  | ASTfloat : typ.
     79
     80(* FIXME: ASTint size is not 1 for Clight32 *)
     81definition typesize : typ → Z ≝ λty.
     82  match ty return λ_.Z with  [ ASTint ⇒ 1 | ASTptr r ⇒ size_pointer r | ASTfloat ⇒ 8 ].
     83
     84lemma typesize_pos: ∀ty. typesize ty > 0.
     85#ty cases ty [ 2: * ] // qed.
     86
     87lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
     88#t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct; qed.
     89
     90lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
     91#t1 #t2 cases t1 cases t2
     92[ %1 @refl
     93| 2,3: #ty %2 % #H destruct
     94| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct /2/
     95]
     96qed.
     97
     98(* * Additionally, function definitions and function calls are annotated
     99  by function signatures indicating the number and types of arguments,
     100  as well as the type of the returned value if any.  These signatures
     101  are used in particular to determine appropriate calling conventions
     102  for the function. *)
     103
     104record signature : Type[0] ≝ {
     105  sig_args: list typ;
     106  sig_res: option typ
     107}.
     108
     109definition proj_sig_res : signature → typ ≝ λs.
     110  match sig_res s with
     111  [ None ⇒ ASTint
     112  | Some t ⇒ t
     113  ].
    124114
    125115(* * Memory accesses (load and store instructions) are annotated by
  • src/Clight/Animation.ma

    r700 r718  
    1111[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? ]
    1212| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? ]
     13| ASTptr _ ⇒ Error ?
    1314].
    1415
  • src/Clight/Cexec.ma

    r708 r718  
    442442
    443443definition eventval_type : ∀ty:typ. Type[0] ≝
    444 λty. match ty with [ ASTint ⇒ int | ASTfloat ⇒ float ].
     444λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
    445445
    446446definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    447 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTfloat ⇒ λv.EVfloat v ].
     447λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
     448*; qed.
    448449
    449450definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    450 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTfloat ⇒ λv.Vfloat v ].
     451λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
     452*; qed.
    451453
    452454lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
    453455  eventval_match (mk_eventval ty v) ty (mk_val ty v).
    454 #ty cases ty; normalize; //; qed.
     456#ty cases ty; normalize; // * *; qed.
    455457
    456458definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
     
    467469[ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
    468470| ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
    469 | _ ⇒ Some ? (Error ?)
     471| _ ⇒ Error ?
    470472].
    471473
  • src/Clight/Csyntax.ma

    r700 r718  
    447447(* * Size of a type, in bytes. *)
    448448
    449 definition sizeof_pointer : region → Z ≝
    450 λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    451 
    452449let rec sizeof (t: type) : Z ≝
    453450  match t return λ_.Z with
     
    455452  | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    456453  | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    457   | Tpointer r _ ⇒ sizeof_pointer r
     454  | Tpointer r _ ⇒ size_pointer r
    458455  | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
    459456  | Tfunction _ _ ⇒ 1
    460457  | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
    461458  | Tunion _ fld ⇒ align (Zmax 1 (sizeof_union fld)) (alignof t)
    462   | Tcomp_ptr r _ ⇒ sizeof_pointer r
     459  | Tcomp_ptr r _ ⇒ size_pointer r
    463460  ]
    464461
  • src/RTLabs/RTLabs-sem.ma

    r702 r718  
    106106
    107107definition eventval_type : ∀ty:typ. Type[0] ≝
    108 λty. match ty with [ ASTint ⇒ int | ASTfloat ⇒ float ].
     108λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
    109109
    110110definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    111 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTfloat ⇒ λv.EVfloat v ].
     111λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
     112*; qed.
    112113
    113114definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    114 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTfloat ⇒ λv.Vfloat v ].
     115λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
     116*; qed.
    115117
    116118lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
    117119  eventval_match (mk_eventval ty v) ty (mk_val ty v).
    118 #ty cases ty; normalize; //; qed.
     120#ty cases ty; normalize; //; * *; qed.
    119121
    120122definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
     
    131133[ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
    132134| ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
    133 | _ ⇒ Some ? (Error ?)
     135| _ ⇒ Error ?
    134136].
    135137
  • src/common/Mem.ma

    r700 r718  
    127127  encoding the type, size and signedness of the chunk being addressed.
    128128  The following functions extract the size information from a chunk. *)
    129 
    130 definition size_pointer : region → Z ≝
    131 λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    132129
    133130definition size_chunk : memory_chunk → Z ≝
  • src/common/Values.ma

    r700 r718  
    224224  | Vint _ ⇒ match t with [ ASTint ⇒ True | _ ⇒ False ]
    225225  | Vfloat _ ⇒ match t with [ ASTfloat ⇒ True | _ ⇒ False ]
    226   | Vptr _ _ _ ⇒ match t with [ ASTint ⇒ True | _ ⇒ False ]
     226  | Vptr _ _ _ ⇒ match t with [ ASTptr ⇒ True | _ ⇒ False ]
    227227  | _ ⇒ False
    228228  ].
Note: See TracChangeset for help on using the changeset viewer.