Changeset 961 for src/common/Values.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Values.ma

    r891 r961  
    1919include "utilities/Coqlib.ma".
    2020include "common/AST.ma".
    21 include "common/Integers.ma".
    2221include "common/Floats.ma".
    2322include "common/Errors.ma".
     
    2726include "basics/logic.ma".
    2827
    29 include "utilities/binary/Z.ma".
    3028include "utilities/extralib.ma".
    3129
     
    9492
    9593definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
    96 definition shift_offset : offset → int → offset ≝
    97   λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
    98 definition neg_shift_offset : offset → int → offset ≝
    99   λo,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
    100 definition sub_offset : offset → offset → int ≝
    101   λx,y. bitvector_of_Z ? (offv x - offv y).
     94definition shift_offset : ∀n. offset → BitVector n → offset ≝
     95  λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
     96(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
     97definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
     98  λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
     99definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
     100  λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
     101definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
     102  λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
     103definition sub_offset : ∀n. offset → offset → BitVector n ≝
     104  λn,x,y. bitvector_of_Z ? (offv x - offv y).
    102105definition zero_offset ≝ mk_offset OZ.
    103106definition lt_offset : offset → offset → bool ≝
     
    117120inductive val: Type[0] ≝
    118121  | Vundef: val
    119   | Vint: int → val
     122  | Vint: ∀sz:intsize. bvint sz → val
    120123  | Vfloat: float → val
    121124  | Vnull: region → val
    122125  | Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val.
    123126
    124 definition Vzero: val ≝ Vint zero.
    125 definition Vone: val ≝ Vint one.
    126 definition Vmone: val ≝ Vint mone.
    127 
    128 definition Vtrue: val ≝ Vint one.
    129 definition Vfalse: val ≝ Vint zero.
     127definition Vzero : intsize → val ≝ λsz. Vint sz (zero ?).
     128definition Vone: intsize → val ≝ λsz. Vint sz (repr sz 1).
     129definition mone ≝ λsz. bitvector_of_Z (bitsize_of_intsize sz) (neg one).
     130definition Vmone: intsize → val ≝ λsz. Vint sz (mone ?).
     131
     132(* XXX 32bit booleans are Clight specific. *)
     133definition Vtrue: val ≝ Vone I32.
     134definition Vfalse: val ≝ Vzero I32.
    130135
    131136(* Values split into bytes.  Ideally we'd use some kind of sizeof for the
     
    140145λv. match v with
    141146[ Vundef ⇒ True
    142 | Vint _ ⇒ True
     147| Vint _ _ ⇒ True
    143148| Vfloat _ ⇒ False
    144149| Vnull r ⇒ ptr_may_be_single r = true
     
    148153definition may_be_split : val → Prop ≝
    149154λv.match v with
    150 [ Vint _ ⇒ False
     155[ Vint _ _ ⇒ False
    151156| Vnull r ⇒ ptr_may_be_single r = false
    152157| Vptr r _ _ _ ⇒ ptr_may_be_single r = false
     
    248253definition is_true : val → Prop ≝ λv.
    249254  match v with
    250   [ Vint n ⇒ n ≠ zero
     255  [ Vint _ n ⇒ n ≠ (zero ?)
    251256  | Vptr _ b _ ofs ⇒ True
    252257  | _ ⇒ False
     
    255260definition is_false : val → Prop ≝ λv.
    256261  match v with
    257   [ Vint n ⇒ n = zero
     262  [ Vint _ n ⇒ n = (zero ?)
    258263  | Vnull _ ⇒ True
    259264  | _ ⇒ False
     
    262267inductive bool_of_val: val → bool → Prop ≝
    263268  | bool_of_val_int_true:
    264       ∀n. n ≠ zero → bool_of_val (Vint n) true
     269      ∀sz,n. n ≠ zero ? → bool_of_val (Vint sz n) true
    265270  | bool_of_val_int_false:
    266       bool_of_val (Vint zero) false
     271      ∀sz. bool_of_val (Vzero sz) false
    267272  | bool_of_val_ptr:
    268273      ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true
     
    274279definition eval_bool_of_val : val → res bool ≝
    275280λv. match v with
    276 [ Vint i ⇒ OK ? (notb (eq i zero))
     281[ Vint _ i ⇒ OK ? (notb (eq_bv ? i (zero ?)))
    277282| Vnull _ ⇒ OK ? false
    278283| Vptr _ _ _ _ ⇒ OK ? true
     
    282287definition neg : val → val ≝ λv.
    283288  match v with
    284   [ Vint n ⇒ Vint (neg n)
     289  [ Vint sz n ⇒ Vint sz (two_complement_negation ? n)
    285290  | _ ⇒ Vundef
    286291  ].
     
    298303  ].
    299304
    300 definition intoffloat : val → val ≝ λv.
    301   match v with
    302   [ Vfloat f ⇒ Vint (intoffloat f)
     305definition intoffloat : intsize → val → val ≝ λsz,v.
     306  match v with
     307  [ Vfloat f ⇒ Vint sz (intoffloat ? f)
    303308  | _ ⇒ Vundef
    304309  ].
    305310
    306 definition intuoffloat : val → val ≝ λv.
    307   match v with
    308   [ Vfloat f ⇒ Vint (intuoffloat f)
     311definition intuoffloat : intsize → val → val ≝ λsz,v.
     312  match v with
     313  [ Vfloat f ⇒ Vint sz (intuoffloat ? f)
    309314  | _ ⇒ Vundef
    310315  ].
     
    312317definition floatofint : val → val ≝ λv.
    313318  match v with
    314   [ Vint n ⇒ Vfloat (floatofint n)
     319  [ Vint sz n ⇒ Vfloat (floatofint ? n)
    315320  | _ ⇒ Vundef
    316321  ].
     
    318323definition floatofintu : val → val ≝ λv.
    319324  match v with
    320   [ Vint n ⇒ Vfloat (floatofintu n)
     325  [ Vint sz n ⇒ Vfloat (floatofintu ? n)
    321326  | _ ⇒ Vundef
    322327  ].
     
    324329definition notint : val → val ≝ λv.
    325330  match v with
    326   [ Vint n ⇒ Vint (xor n mone)
     331  [ Vint sz n ⇒ Vint sz (exclusive_disjunction_bv ? n (mone ?))
    327332  | _ ⇒ Vundef
    328333  ].
    329334 
    330 (* FIXME: switch to alias, or rename, or … *)
    331 definition int_eq : int → int → bool ≝ eq.
    332335definition notbool : val → val ≝ λv.
    333336  match v with
    334   [ Vint n ⇒ of_bool (int_eq n zero)
     337  [ Vint sz n ⇒ of_bool (eq_bv ? n (zero ?))
    335338  | Vptr _ b _ ofs ⇒ Vfalse
    336339  | Vnull _ ⇒ Vtrue
     
    338341  ].
    339342
    340 definition zero_ext ≝ λnbits: nat. λv: val.
    341   match v with
    342   [ Vint n ⇒ Vint (zero_ext nbits n)
     343definition zero_ext ≝ λrsz: intsize. λv: val.
     344  match v with
     345  [ Vint sz n ⇒ Vint rsz (zero_ext … n)
    343346  | _ ⇒ Vundef
    344347  ].
    345348
    346 definition sign_ext ≝ λnbits:nat. λv:val.
    347   match v with
    348   [ Vint i ⇒ Vint (sign_ext nbits i)
     349definition sign_ext ≝ λrsz:intsize. λv:val.
     350  match v with
     351  [ Vint sz i ⇒ Vint rsz (sign_ext … i)
    349352  | _ ⇒ Vundef
    350353  ].
     
    359362definition add ≝ λv1,v2: val.
    360363  match v1 with
    361   [ Vint n1 ⇒ match v2 with
    362     [ Vint n2 ⇒ Vint (addition_n ? n1 n2)
    363     | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
     364  [ Vint sz1 n1 ⇒ match v2 with
     365    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     366                    (λn1. Vint sz2 (addition_n ? n1 n2))
     367                    Vundef
     368    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ? ofs2 n1)
    364369    | _ ⇒ Vundef ]
    365370  | Vptr r b1 p ofs1 ⇒ match v2 with
    366     [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2)
    367     | _ ⇒ Vundef ]
    368   | _ ⇒ Vundef ].
     371    [ Vint _ n2 ⇒ Vptr r b1 p (shift_offset ? ofs1 n2)
     372    | _ ⇒ Vundef ]
     373  | _ ⇒ Vundef ].
     374
     375(* XXX Is I32 the best answer for ptr subtraction? *)
    369376
    370377definition sub ≝ λv1,v2: val.
    371378  match v1 with
    372   [ Vint n1 ⇒ match v2 with
    373     [ Vint n2 ⇒ Vint (subtraction ? n1 n2)
     379  [ Vint sz1 n1 ⇒ match v2 with
     380    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     381                    (λn1. Vint sz2 (subtraction ? n1 n2))
     382                    Vundef
    374383    | _ ⇒ Vundef ]
    375384  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    376     [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)
     385    [ Vint sz2 n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2)
    377386    | Vptr r2 b2 p2 ofs2 ⇒
    378         if eq_block b1 b2 then Vint (sub_offset ofs1 ofs2) else Vundef
    379     | _ ⇒ Vundef ]
    380   | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
     387        if eq_block b1 b2 then Vint I32 (sub_offset ? ofs1 ofs2) else Vundef
     388    | _ ⇒ Vundef ]
     389  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vzero I32 | _ ⇒ Vundef ]
    381390  | _ ⇒ Vundef ].
    382391
    383392definition mul ≝ λv1, v2: val.
    384393  match v1 with
    385   [ Vint n1 ⇒ match v2 with
    386     [ Vint n2 ⇒ Vint (mul n1 n2)
     394  [ Vint sz1 n1 ⇒ match v2 with
     395    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     396                    (λn1. Vint sz2 (\snd (split … (multiplication ? n1 n2))))
     397                    Vundef
    387398    | _ ⇒ Vundef ]
    388399  | _ ⇒ Vundef ].
     
    418429definition v_and ≝ λv1, v2: val.
    419430  match v1 with
    420   [ Vint n1 ⇒ match v2 with
    421     [ Vint n2 ⇒ Vint (i_and n1 n2)
     431  [ Vint sz1 n1 ⇒ match v2 with
     432    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     433                    (λn1. Vint ? (conjunction_bv ? n1 n2))
     434                    Vundef
    422435    | _ ⇒ Vundef ]
    423436  | _ ⇒ Vundef ].
     
    425438definition or ≝ λv1, v2: val.
    426439  match v1 with
    427   [ Vint n1 ⇒ match v2 with
    428     [ Vint n2 ⇒ Vint (or n1 n2)
     440  [ Vint sz1 n1 ⇒ match v2 with
     441    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     442                    (λn1. Vint ? (inclusive_disjunction_bv ? n1 n2))
     443                    Vundef
    429444    | _ ⇒ Vundef ]
    430445  | _ ⇒ Vundef ].
     
    432447definition xor ≝ λv1, v2: val.
    433448  match v1 with
    434   [ Vint n1 ⇒ match v2 with
    435     [ Vint n2 ⇒ Vint (xor n1 n2)
     449  [ Vint sz1 n1 ⇒ match v2 with
     450    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     451                    (λn1. Vint ? (exclusive_disjunction_bv ? n1 n2))
     452                    Vundef
    436453    | _ ⇒ Vundef ]
    437454  | _ ⇒ Vundef ].
     
    550567  ].
    551568
     569definition cmp_int : ∀n. comparison → BitVector n → BitVector n → bool ≝
     570λn,c,x,y.
     571  match c with
     572  [ Ceq ⇒ eq_bv ? x y
     573  | Cne ⇒ notb (eq_bv ? x y)
     574  | Clt ⇒ lt_s ? x y
     575  | Cle ⇒ notb (lt_s ? y x)
     576  | Cgt ⇒ lt_s ? y x
     577  | Cge ⇒ notb (lt_s ? x y)
     578  ].
     579
     580definition cmpu_int : ∀n. comparison → BitVector n → BitVector n → bool ≝
     581λn,c,x,y.
     582  match c with
     583  [ Ceq ⇒ eq_bv ? x y
     584  | Cne ⇒ notb (eq_bv ? x y)
     585  | Clt ⇒ lt_u ? x y
     586  | Cle ⇒ notb (lt_u ? y x)
     587  | Cgt ⇒ lt_u ? y x
     588  | Cge ⇒ notb (lt_u ? x y)
     589  ].
     590
    552591definition cmp ≝ λc: comparison. λv1,v2: val.
    553592  match v1 with
    554   [ Vint n1 ⇒ match v2 with
    555     [ Vint n2 ⇒ of_bool (cmp c n1 n2)
     593  [ Vint sz1 n1 ⇒ match v2 with
     594    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     595                    (λn1. of_bool (cmp_int ? c n1 n2))
     596                    Vundef
    556597    | _ ⇒ Vundef ]
    557598  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    571612definition cmpu ≝ λc: comparison. λv1,v2: val.
    572613  match v1 with
    573   [ Vint n1 ⇒ match v2 with
    574     [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
     614  [ Vint sz1 n1 ⇒ match v2 with
     615    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     616                    (λn1. of_bool (cmpu_int ? c n1 n2))
     617                    Vundef
    575618    | _ ⇒ Vundef ]
    576619  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    588631  | _ ⇒ Vundef ].
    589632
    590 definition cmpf ≝ λc: comparison. λv1,v2: val.
     633definition cmpf ≝ λc: comparison. λsz:intsize. λv1,v2: val.
    591634  match v1 with
    592635  [ Vfloat f1 ⇒ match v2 with
     
    603646  is performed and [0xFFFFFFFF] is returned.   Type mismatches
    604647  (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)
     648(* XXX update comment *)
     649(* XXX is this even necessary now?
     650       should we be able to extract bytes? *)
    605651
    606652let rec load_result (chunk: memory_chunk) (v: val) ≝
    607653  match v with
    608   [ Vint n ⇒
     654  [ Vint sz n ⇒
    609655    match chunk with
    610     [ Mint8signed ⇒ Vint (sign_ext 8 n)
    611     | Mint8unsigned ⇒ Vint (zero_ext 8 n)
    612     | Mint16signed ⇒ Vint (sign_ext 16 n)
    613     | Mint16unsigned ⇒ Vint (zero_ext 16 n)
    614     | Mint32 ⇒ Vint n
     656    [ Mint8signed ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
     657    | Mint8unsigned ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
     658    | Mint16signed ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
     659    | Mint16unsigned ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
     660    | Mint32 ⇒  match sz with [ I32 ⇒ v | _ ⇒ Vundef ]
    615661    | _ ⇒ Vundef
    616662    ]
Note: See TracChangeset for help on using the changeset viewer.