Changeset 744 for src/Clight


Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (10 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

Location:
src/Clight
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/AST.ma

    r738 r744  
    7070#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
    7171
    72 definition size_pointer : region → Z
    73 λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
     72definition size_pointer : region → nat
     73λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    7474
    7575(* * The intermediate languages are weakly typed, using only three types:
     
    9090
    9191lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    92 #t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct; qed.
     92#t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct qed.
    9393
    9494lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
     
    9696[ %1 @refl
    9797| 2,3: #ty %2 % #H destruct
    98 | #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct /2/
     98| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/
    9999]
    100100qed.
     
    139139  | Init_float32: float → init_data
    140140  | Init_float64: float → init_data
    141   | Init_space: Z → init_data
     141  | Init_space: nat → init_data
    142142  | Init_null: region → init_data
    143143  | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
  • src/Clight/Cexec.ma

    r731 r744  
    345345#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
    346346
     347definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m).
     348#n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E
     349[ %1 | %2 ] @(eqb_elim … E) // #_ #H destruct qed.
     350
    347351let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
    348352match t1 return λt'. (t' = t2) + (t' ≠ t2) with
     
    366370    match eq_region_dec s s' with [ inl e1 ⇒
    367371      match type_eq_dec t t' with [ inl e2 ⇒
    368         match decidable_eq_Z_Type n n' with [ inl e3 ⇒ inl ???
     372        match eq_nat_dec n n' with [ inl e3 ⇒ inl ???
    369373        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    370374        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
  • src/Clight/CexecSound.ma

    r708 r744  
    66 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    77#v #ty #r
    8 cases v; [ | #i | #f | #r1 | #r #b #pc #of ]
     8cases v; [ | #i | #f | #r1 | #r' #b #pc #of ]
    99cases ty; [ 2,11,20,29,38: #sz #sg | 3,12,21,30,39: #sz | 4,13,22,31,40: #r #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
    1010#H whd in H:(??%?); destruct;
    1111[ lapply (eq_spec i zero); elim (eq i zero);
    1212  [ #e >e @bool_of_val_false //;
    13   | #ne @bool_of_val_true /2/;
     13  | #ne (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vint i) (Tint sz sg)) normalize #H @H /2/;
    1414  ]
    1515| elim (eq_dec f Fzero);
    1616  [ #e >e >(Feq_zero_true …) @bool_of_val_false //;
    17   | #ne >(Feq_zero_false …) //; @bool_of_val_true /2/;
     17  | #ne >(Feq_zero_false …) //; (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vfloat f) (Tfloat sz)) normalize #H @H /2/;
    1818  ]
    1919| @bool_of_val_false //
    20 | @bool_of_val_true //
     20| (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vptr r' b pc of) (Tpointer r ty)) normalize #H @H //
    2121] qed.
    2222
  • src/Clight/Csem.ma

    r725 r744  
    170170          if eq_block b1 b2 then
    171171            if eq (repr (sizeof ty)) zero then None ?
    172             else Some ? (Vint (divu (sub_offset ofs1 ofs2) (repr (sizeof ty))))
     172            else match division_u ? (sub_offset ofs1 ofs2) (repr (sizeof ty)) with
     173                 [ None ⇒ None ?
     174                 | Some v ⇒ Some ? (Vint v)
     175                 ]
    173176          else None ?
    174177        | _ ⇒ None ? ]
     
    202205      match v1 with
    203206      [ Vint n1 ⇒ match v2 with
    204         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (divu n1 n2))
    205 (*        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)*)
     207        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)
    206208        | _ ⇒ None ? ]
    207209      | _ ⇒ None ? ]
     
    209211      match v1 with
    210212       [ Vint n1 ⇒ match v2 with
    211          [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint(divs n1 n2))
    212 (*         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)*)
     213         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)
    213214         | _ ⇒ None ? ]
    214215      | _ ⇒ None ? ]
     
    228229      match v1 with
    229230      [ Vint n1 ⇒ match v2 with
    230         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (modu n1 n2))
    231 (*        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)*)
     231        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)
    232232        | _ ⇒ None ? ]
    233233      | _ ⇒ None ? ]
     
    235235      match v1 with
    236236      [ Vint n1 ⇒ match v2 with
    237         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (mods n1 n2))
    238 (*        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)*)
     237        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)
    239238        | _ ⇒ None ? ]
    240239      | _ ⇒ None ? ]
  • src/Clight/Csyntax.ma

    r725 r744  
    8888  | Tfloat: floatsize → type            (**r floating-point types *)
    8989  | Tpointer: region → type → type      (**r pointer types ([*ty]) *)
    90   | Tarray: region → type → Z → type    (**r array types ([ty[len]]) *)
     90  | Tarray: region → type → nat → type  (**r array types ([ty[len]]) *)
    9191  | Tfunction: typelist → type → type   (**r function types *)
    9292  | Tstruct: ident → fieldlist → type   (**r struct types *)
     
    363363(* * Natural alignment of a type, in bytes. *)
    364364(* FIXME: these are old values for 32 bit machines *)
    365 let rec alignof (t: type) : Z
    366   match t return λ_.Z (* XXX appears to infer nat otherwise *) with
     365let rec alignof (t: type) : nat
     366  match t with
    367367  [ Tvoid ⇒ 1
    368   | Tint sz _ ⇒ match sz return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    369   | Tfloat sz ⇒ match sz return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
     368  | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
     369  | Tfloat sz ⇒ match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    370370  | Tpointer _ _ ⇒ 4
    371371  | Tarray _ t' n ⇒ alignof t'
     
    376376  ]
    377377
    378 and alignof_fields (f: fieldlist) : Z
     378and alignof_fields (f: fieldlist) : nat
    379379  match f with
    380380  [ Fnil ⇒ 1
    381   | Fcons id t f' ⇒ Zmax (alignof t) (alignof_fields f')
     381  | Fcons id t f' ⇒ max (alignof t) (alignof_fields f')
    382382  ].
    383383
     
    436436  ∀f. alignof_fields f > 0.
    437437@fieldlist_ind //;
    438 #i #t #fs' #IH lapply (Zmax_r (alignof t) (alignof_fields fs'));
    439 @Zlt_to_Zle_to_Zlt //; qed.
     438#i #t #fs' #IH @max_r @IH qed.
    440439
    441440lemma alignof_pos:
    442441  ∀t. alignof t > 0.
    443442#t elim t; normalize; //;
    444 [ 1,2: #z cases z; //;
     443[ 1,2: #z cases z; /2/;
    445444| 3,4: #i @alignof_fields_pos
    446445] qed.
     
    448447(* * Size of a type, in bytes. *)
    449448
    450 let rec sizeof (t: type) : Z
    451   match t return λ_.Z with
     449let rec sizeof (t: type) : nat
     450  match t with
    452451  [ Tvoid ⇒ 1
    453   | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    454   | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
     452  | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
     453  | Tfloat f ⇒ match f with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    455454  | Tpointer r _ ⇒ size_pointer r
    456   | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
     455  | Tarray _ t' n ⇒ sizeof t' * max 1 n
    457456  | Tfunction _ _ ⇒ 1
    458   | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
    459   | Tunion _ fld ⇒ align (Zmax 1 (sizeof_union fld)) (alignof t)
     457  | Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t)
     458  | Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t)
    460459  | Tcomp_ptr r _ ⇒ size_pointer r
    461460  ]
    462461
    463 and sizeof_struct (fld: fieldlist) (pos: Z) on fld : Z
     462and sizeof_struct (fld: fieldlist) (pos: nat) on fld : nat
    464463  match fld with
    465464  [ Fnil ⇒ pos
     
    467466  ]
    468467
    469 and sizeof_union (fld: fieldlist) : Z
     468and sizeof_union (fld: fieldlist) : nat
    470469  match fld with
    471470  [ Fnil ⇒ 0
    472   | Fcons id t fld' ⇒ Zmax (sizeof t) (sizeof_union fld')
     471  | Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld')
    473472  ].
    474473(* TODO: needs some Z_times results
     
    518517Open Local Scope string_scope.
    519518*)
    520 let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
    521                               on fld : res Z
     519let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
     520                              on fld : res nat
    522521  match fld with
    523522  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
Note: See TracChangeset for help on using the changeset viewer.