Changeset 879


Ignore:
Timestamp:
Jun 3, 2011, 5:35:30 PM (9 years ago)
Author:
campbell
Message:

Refine "AST" types to include size/signedness information.

Location:
src
Files:
17 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r797 r879  
    440440    #H1 #H2
    441441    >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
    442     whd; inversion H2; #x #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
     442    whd; inversion H2; #x #sz [ #sg ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
    443443    @refl
    444444| #v #f #env #k #m @refl
  • src/Clight/CexecSound.ma

    r797 r879  
    365365  [ //
    366366  | #ty #tys whd in ⊢ (???%)
    367     cases ty cases v // #v'
     367    cases ty cases v // #v' #sz try #sg
    368368    @bind_OK #evs #CHECK
    369369    @(evl_match_cons ??????? (P_res_to_P … CHECK)) //
  • src/Clight/Csyntax.ma

    r816 r879  
    2525
    2626(* * ** Types *)
    27 
    28 (* * Clight types are similar to those of C.  They include numeric types,
    29   pointers, arrays, function types, and composite types (struct and
    30   union).  Numeric types (integers and floats) fully specify the
    31   bit size of the type.  An integer type is a pair of a signed/unsigned
    32   flag and a bit size: 8, 16 or 32 bits. *)
    33 
    34 inductive signedness : Type[0] ≝
    35   | Signed: signedness
    36   | Unsigned: signedness.
    37 
    38 inductive intsize : Type[0] ≝
    39   | I8: intsize
    40   | I16: intsize
    41   | I32: intsize.
    42 
    43 (* * Float types come in two sizes: 32 bits (single precision)
    44   and 64-bit (double precision). *)
    45 
    46 inductive floatsize : Type[0] ≝
    47   | F32: floatsize
    48   | F64: floatsize.
    4927
    5028(* * The syntax of type expressions.  Some points to note:
     
    891869definition typ_of_type : type → typ ≝ λt.
    892870  match t with
    893   [ Tfloat _ ⇒ ASTfloat
    894   | _ ⇒ ASTint
     871  [ Tvoid ⇒ ASTint I32 Unsigned
     872  | Tint sz sg ⇒ ASTint sz sg
     873  | Tfloat sz ⇒ ASTfloat sz
     874  | Tpointer r _ ⇒ ASTptr r
     875  | Tarray r _ _ ⇒ ASTptr r
     876  | Tfunction _ _ ⇒ ASTptr Code
     877  | _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *)
    895878  ].
    896879
     
    898881  match t with
    899882  [ Tvoid ⇒ None ?
    900   | Tfloat _ ⇒ Some ? ASTfloat
    901   | _ ⇒ Some ? ASTint
     883  | Tint sz sg ⇒ Some ? (ASTint sz sg)
     884  | Tfloat sz ⇒ Some ? (ASTfloat sz)
     885  | Tpointer r _ ⇒ Some ? (ASTptr r)
     886  | Tarray r _ _ ⇒ Some ? (ASTptr r)
     887  | Tfunction _ _ ⇒ Some ? (ASTptr Code)
     888  | _ ⇒ None ? (* structs and unions shouldn't be converted? *)
    902889  ].
    903890
  • src/Cminor/semantics.ma

    r816 r879  
    226226    | External fn ⇒
    227227        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
    228         ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
     228        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    229229        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
    230230        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m k〉
  • src/Cminor/test/factorial.ma

    r816 r879  
    33
    44definition id_get_input := ident_of_nat 0.
    5 definition f_get_input := External internal_function (mk_external_function id_get_input (mk_signature [] (Some ? ASTint))).
     5definition f_get_input := External internal_function (mk_external_function id_get_input (mk_signature [] (Some ? (ASTint I32 Signed)))).
    66definition id_main := ident_of_nat 1.
    77definition id_main_tmp0 := ident_of_nat 5.
     
    1313definition C_cost1 := costlabel_of_nat 2.
    1414definition f_main := Internal ? (mk_internal_function
    15   (mk_signature [] (Some ? ASTint))
     15  (mk_signature [] (Some ? (ASTint I32 Signed)))
    1616  []
    1717  [id_main_tmp0; id_main_r; id_main_j; id_main_i]
  • src/Cminor/test/null-op.ma

    r776 r879  
    1717definition C_cost1 := costlabel_of_nat 1.
    1818definition f_main := Internal ? (mk_internal_function
    19   (mk_signature [] (Some ? ASTint))
     19  (mk_signature [] (Some ? (ASTint I32 Signed)))
    2020  []
    2121  [id_main_tmp0; id_main_q; id_main_p; id_main_c]
  • src/Cminor/test/search.ma

    r816 r879  
    2020definition C_cost7 := costlabel_of_nat 1.
    2121definition f_search := Internal ? (mk_internal_function
    22   (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint))
     22  (mk_signature [ASTptr Any; ASTint I8 Signed; ASTint I8 Signed] (Some ? (ASTint I8 Signed)))
    2323  [id_search_tab; id_search_size; id_search_to_find]
    2424  [id_search_tmp0; id_search_low; id_search_high; id_search_i]
     
    101101definition C_cost9 := costlabel_of_nat 18.
    102102definition f_main := Internal ? (mk_internal_function
    103   (mk_signature [] (Some ? ASTint))
     103  (mk_signature [] (Some ? (ASTint I32 Signed)))
    104104  []
    105105  [id_main_tmp0; id_main_res]
  • src/Cminor/test/sum-bad.ma

    r797 r879  
    1616definition C_cost1 := costlabel_of_nat 1.
    1717definition f_main := Internal ? (mk_internal_function
    18   (mk_signature [] (Some ? ASTint))
     18  (mk_signature [] (Some ? (ASTint I32 Signed)))
    1919  []
    2020  [id_main_tmp0; id_main_total(*; id_main_i*)]
  • src/Cminor/test/sum.ma

    r768 r879  
    1313definition C_cost1 := costlabel_of_nat 1.
    1414definition f_main := Internal ? (mk_internal_function
    15   (mk_signature [] (Some ? ASTint))
     15  (mk_signature [] (Some ? (ASTint I32 Signed)))
    1616  []
    1717  [id_main_tmp0; id_main_total; id_main_i]
  • src/Cminor/test/switcher.ma

    r816 r879  
    77
    88definition id_get := ident_of_nat 99.
    9 definition f_get := External internal_function (mk_external_function id_get (mk_signature [] (Some ? ASTint))).
     9definition f_get := External internal_function (mk_external_function id_get (mk_signature [] (Some ? (ASTint I32 Signed)))).
    1010
    1111
     
    1414definition id_main_x1 := ident_of_nat 2.
    1515definition f_main := Internal ? (mk_internal_function
    16   (mk_signature [] (Some ? ASTint))
     16  (mk_signature [] (Some ? (ASTint I32 Signed)))
    1717  []
    1818  [id_main_i; id_main_x1]
  • src/RTLabs/semantics.ma

    r816 r879  
    203203    | External fn ⇒
    204204        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    205         ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
     205        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    206206        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
    207207    ]
  • src/RTLabs/test/search.ma

    r816 r879  
    7272
    7373  definition pre_search := mk_pre_internal_function
    74     (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint))
     74    (mk_signature [ASTptr Any; ASTint I8 Signed; ASTint I8 Signed] (Some ? (ASTint I8 Signed)))
    7575    (Some ? 8)
    7676    [7; 1; 2]
     
    185185
    186186  definition pre_main := mk_pre_internal_function
    187     (mk_signature [] (Some ? ASTint))
     187    (mk_signature [] (Some ? (ASTint I32 Signed)))
    188188    (Some ? 2)
    189189    []
  • src/RTLabs/test/sum.ma

    r765 r879  
    4444
    4545  definition pre_main := mk_pre_internal_function
    46     (mk_signature [] (Some ? ASTint))
     46    (mk_signature [] (Some ? (ASTint I32 Signed)))
    4747    (Some ? 3)
    4848    []
  • src/common/AST.ma

    r849 r879  
    7878λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    7979
    80 (* * The intermediate languages are weakly typed, using only three types:
    81   [ASTint] for integers, [ASTptr] for pointers, and [ASTfloat] for floating-point
    82   numbers. *)
     80(* We maintain some reasonable type information through the front end of the
     81   compiler. *)
     82
     83inductive signedness : Type[0] ≝
     84  | Signed: signedness
     85  | Unsigned: signedness.
     86
     87inductive intsize : Type[0] ≝
     88  | I8: intsize
     89  | I16: intsize
     90  | I32: intsize.
     91
     92(* * Float types come in two sizes: 32 bits (single precision)
     93  and 64-bit (double precision). *)
     94
     95inductive floatsize : Type[0] ≝
     96  | F32: floatsize
     97  | F64: floatsize.
    8398
    8499inductive typ : Type[0] ≝
    85   | ASTint : typ
     100  | ASTint : intsize → signedness → typ
    86101  | ASTptr : region → typ
    87   | ASTfloat : typ.
     102  | ASTfloat : floatsize → typ.
    88103
    89104(* XXX aliases *)
    90105definition SigType ≝ typ.
    91 definition SigType_Int ≝ ASTint.
     106definition SigType_Int ≝ ASTint I32 Unsigned.
    92107(*
    93108| SigType_Float: SigType
     
    95110definition SigType_Ptr ≝ ASTptr Any.
    96111
    97 
    98 (* FIXME: ASTint size is not 1 for Clight32 *)
     112definition size_intsize : intsize → nat ≝
     113λsz. match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4].
     114
     115definition size_floatsize : floatsize → nat ≝
     116λsz. match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ].
     117
    99118definition typesize : typ → nat ≝ λty.
    100   match ty with [ ASTint ⇒ 1 | ASTptr r ⇒ size_pointer r | ASTfloat ⇒ 8 ].
     119  match ty with
     120  [ ASTint sz _ ⇒ size_intsize sz
     121  | ASTptr r ⇒ size_pointer r
     122  | ASTfloat sz ⇒ size_floatsize sz ].
    101123
    102124lemma typesize_pos: ∀ty. typesize ty > 0.
    103 #ty cases ty [ 2: * ] /2/ qed.
     125* *; try * /2/ qed.
    104126
    105127lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    106 #t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct; qed.
     128* * * *; try *; try *; try (%1 @refl) %2 @nmk #H destruct qed.
    107129
    108130lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
     
    132154definition proj_sig_res : signature → typ ≝ λs.
    133155  match sig_res s with
    134   [ None ⇒ ASTint
     156  [ None ⇒ ASTint I32 Unsigned
    135157  | Some t ⇒ t
    136158  ].
  • src/common/Animation.ma

    r797 r879  
    1010λo,ev.
    1111match io_in_typ o return λt. res (eventval_type t) with
    12 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? (msg IllTypedEvent) ]
    13 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
     12[ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? (msg IllTypedEvent) ]
     13| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
    1414| ASTptr _ ⇒ Error ? (msg IllTypedEvent)
    1515].
  • src/common/Events.ma

    r781 r879  
    193193inductive eventval_match: eventval -> typ -> val -> Prop :=
    194194  | ev_match_int:
    195       ∀i. eventval_match (EVint i) ASTint (Vint i)
     195      ∀i,sz,sg. eventval_match (EVint i) (ASTint sz sg) (Vint i)
    196196  | ev_match_float:
    197       ∀f. eventval_match (EVfloat f) ASTfloat (Vfloat f).
     197      ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f).
    198198
    199199inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
  • src/common/IO.ma

    r797 r879  
    66
    77definition eventval_type : ∀ty:typ. Type[0] ≝
    8 λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
     8λty. match ty with [ ASTint _ _ ⇒ int | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ].
    99
    1010definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    11 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
     11λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint _ _ ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
    1212*; qed.
    1313
    1414definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    15 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
     15λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint _ _ ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
    1616*; qed.
    1717
     
    2525λev,ty.
    2626match ty with
    27 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)]
    28 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
     27[ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)]
     28| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
    2929| _ ⇒ Error ? (msg IllTypedEvent)
    3030].
     
    3333λv,ty.
    3434match ty with
    35 [ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
    36 | ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
     35[ ASTint _ _ ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
     36| ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
    3737| _ ⇒ Error ? (msg IllTypedEvent)
    3838].
Note: See TracChangeset for help on using the changeset viewer.