Changeset 718 for src/Clight


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/Clight
Files:
4 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
Note: See TracChangeset for help on using the changeset viewer.