Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (7 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r2432 r2468  
    2323inductive constant : typ → Type[0] ≝
    2424  | Ointconst: ∀sz,sg. bvint sz → constant (ASTint sz sg)
    25   | Ofloatconst: ∀sz. float → constant (ASTfloat sz)
     25(*  | Ofloatconst: ∀sz. float → constant (ASTfloat sz) *)
    2626  | Oaddrsymbol: ident → nat → constant ASTptr (**r address of the symbol plus the offset *)
    2727  | Oaddrstack: nat → constant ASTptr.         (**r stack pointer plus the given offset *)
     
    3434  | Onotbool: ∀t,sz,sg. boolsrc t → unary_operation t (ASTint sz sg)           (**r boolean negation  *)
    3535  | Onotint:  ∀sz,sg. unary_operation (ASTint sz sg) (ASTint sz sg)            (**r bitwise complement  *)
    36   | Onegf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)                    (**r float opposite *)
    37   | Oabsf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)                    (**r float absolute value *)
    38   | Osingleoffloat: unary_operation (ASTfloat F64) (ASTfloat F32)              (**r float truncation *)
    39   | Ointoffloat:  ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Signed)  (**r signed integer to float *)
    40   | Ointuoffloat: ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Unsigned) (**r unsigned integer to float *)
    41   | Ofloatofint:  ∀fsz,sz. unary_operation (ASTint sz Signed) (ASTfloat fsz)   (**r float to signed integer *)
    42   | Ofloatofintu: ∀fsz,sz. unary_operation (ASTint sz Unsigned) (ASTfloat fsz) (**r float to unsigned integer *)
     36(*| Onegf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)*)                  (**r float opposite *)
     37(*| Oabsf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)*)                  (**r float absolute value *)
     38(*| Osingleoffloat: unary_operation (ASTfloat F64) (ASTfloat F32)*)            (**r float truncation *)
     39(*| Ointoffloat:  ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Signed)*) (**r signed integer to float *)
     40(*| Ointuoffloat: ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Unsigned)*) (**r unsigned integer to float *)
     41(*| Ofloatofint:  ∀fsz,sz. unary_operation (ASTint sz Signed) (ASTfloat fsz)*)   (**r float to signed integer *)
     42(*| Ofloatofintu: ∀fsz,sz. unary_operation (ASTint sz Unsigned) (ASTfloat fsz)*) (**r float to unsigned integer *)
    4343  | Oid: ∀t. unary_operation t t                                               (**r identity (used to move between registers *)
    4444  | Optrofint: ∀sz,sg. unary_operation (ASTint sz sg) ASTptr                   (**r int to pointer with given representation *)
     
    5959  | Oshr:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r right signed shift *)
    6060  | Oshru: ∀sz,sg. binary_operation (ASTint sz Unsigned) (ASTint sz sg)       (ASTint sz sg)       (**r right unsigned shift *)
    61   | Oaddf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float addition *)
    62   | Osubf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float subtraction *)
    63   | Omulf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float multiplication *)
    64   | Odivf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float division *)
     61(*  | Oaddf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float addition *)
     62(*  | Osubf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float subtraction *)
     63(*  | Omulf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float multiplication *)
     64(*  | Odivf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float division *)
    6565  | Ocmp: ∀sz,sg,sg'. comparison -> binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint I8 sg') (**r integer signed comparison *)
    6666  | Ocmpu: ∀sz,sg'.   comparison -> binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint I8 sg') (**r integer unsigned comparison *)
    67   | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') (**r float comparison *)
     67(*  | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') *) (**r float comparison *)
    6868  | Oaddp: ∀sz.    binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r add an integer to a pointer *)
    6969  | Osubpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r subtract int from a pointers *)
     
    7676match t with
    7777[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
    78 | ASTfloat sz ⇒ ∀f.P (Vfloat f)
     78(*| ASTfloat sz ⇒ ∀f.P (Vfloat f) *)
    7979| ASTptr ⇒ P Vnull ∧ ∀b,o. P (Vptr (mk_pointer b o))
    8080] →
    8181P v.
    8282#v #t #P *
    83 [ 1,2: //
     83[ 1: //
    8484| * //
    8585| #b #o * //
     
    9595  match cst with
    9696  [ Ointconst sz sg n ⇒ Some ? (Vint sz n)
    97   | Ofloatconst sz n ⇒ Some ? (Vfloat n)
     97(*  | Ofloatconst sz n ⇒ Some ? (Vfloat n)*)
    9898  | Oaddrsymbol s ofs ⇒
    9999      match find_symbol s with
     
    113113#t #f #sp *
    114114[ #sz #sg #i #v #E normalize in E; destruct //
    115 | #sz #f #v #E normalize in E; destruct //
     115(*| #sz #f #v #E normalize in E; destruct //*)
    116116| #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct
    117117(*  cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct *)
     
    137137      ]
    138138  | Onotint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?))) | _ ⇒ None ? ]
    139   | Onegf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
    140   | Oabsf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
     139(*  | Onegf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
     140  | Oabsf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ] 
    141141  | Osingleoffloat ⇒ Some ? (singleoffloat arg)
    142142  | Ointoffloat _ sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1)) | _ ⇒ None ? ]
    143143  | Ointuoffloat _ sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1)) | _ ⇒ None ? ]
    144144  | Ofloatofint _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1)) | _ ⇒ None ? ]
    145   | Ofloatofintu _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ]
     145  | Ofloatofintu _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ] *)
    146146  | Oid t ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
    147147  (* Only conversion of null pointers is specified. *)
     
    164164    | #b #o whd in ⊢ (??%? → ?); #E' destruct %
    165165    ]
    166   | #f *
     166(*  | #f * *)
    167167  ]
    168168| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %
     169(*
    169170| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
    170171| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
     
    174175| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
    175176| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
     177*)
    176178| #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H
    177179| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
     
    349351  | _ ⇒ None ? ].
    350352
     353(*
    351354definition ev_addf ≝ λv1,v2: val.
    352355  match v1 with
     
    375378    [ Vfloat f2 ⇒ Some ? (Vfloat (Fdiv f1 f2))
    376379    | _ ⇒ None ? ]
    377   | _ ⇒ None ? ].
     380  | _ ⇒ None ? ]. *)
    378381
    379382definition FEtrue : val ≝ Vint I8 (repr I8 1).
     
    434437  | _ ⇒ None ? ].
    435438
     439(*
    436440definition ev_cmpf ≝ λc: comparison. λv1,v2: val.
    437441  match v1 with
     
    439443    [ Vfloat f2 ⇒ Some ? (FE_of_bool (Fcmp c f1 f2))
    440444    | _ ⇒ None ? ]
    441   | _ ⇒ None ? ].
     445  | _ ⇒ None ? ]. *)
    442446
    443447definition eval_binop : mem → ∀t1,t2,t'. binary_operation t1 t2 t' → val → val → option val ≝
     
    457461  | Oshr _ _ ⇒ ev_shr
    458462  | Oshru _ _ ⇒ ev_shru
    459   | Oaddf _ ⇒ ev_addf
     463(*  | Oaddf _ ⇒ ev_addf
    460464  | Osubf _ ⇒ ev_subf
    461465  | Omulf _ ⇒ ev_mulf
    462   | Odivf _ ⇒ ev_divf
     466  | Odivf _ ⇒ ev_divf *)
    463467  | Ocmp _ _ _ c ⇒ ev_cmp c
    464468  | Ocmpu _ _ c ⇒ ev_cmpu c
    465   | Ocmpf _ _ c ⇒ ev_cmpf c
     469(*  | Ocmpf _ _ c ⇒ ev_cmpf c *)
    466470  | Oaddp _ ⇒ ev_addp
    467471  | Osubpi _ ⇒ ev_subpi
     
    490494  whd in ⊢ (??%? → ?); cases (lt_u ???) whd in ⊢ (??%? → ?); #E destruct //
    491495(* floats *)
    492 | 14,15,16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
    493   whd in ⊢ (??%? → ?); #E destruct //
     496(*| 14,15,16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
     497  whd in ⊢ (??%? → ?); #E destruct // *)
    494498(* comparisons *)
    495499| #sz #sg #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     
    497501| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
    498502  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (cmpu_int ????) #E destruct //
    499 | #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
    500   whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct //
     503(*| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
     504  whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct // *)
    501505(* pointers *)
    502 | 21,22: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
     506| 16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
    503507  whd in ⊢ (??%? → ?); [ 3,4: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
    504508| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
Note: See TracChangeset for help on using the changeset viewer.