Changeset 744 for src/common/Values.ma


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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Values.ma

    r718 r744  
    2323include "common/Errors.ma".
    2424
    25 include "ASM/Vector.ma".
     25include "ASM/BitVectorZ.ma".
    2626
    2727include "basics/logic.ma".
     28
     29include "utilities/binary/Z.ma".
    2830
    2931(* To define pointers we need a few details about the memory model.
     
    8890definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
    8991definition shift_offset : offset → int → offset ≝
    90   λo,i. mk_offset (offv o + signed i).
     92  λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
    9193definition neg_shift_offset : offset → int → offset ≝
    92   λo,i. mk_offset (offv o - signed i).
     94  λo,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
    9395definition sub_offset : offset → offset → int ≝
    94   λx,y. repr (offv x - offv y).
     96  λx,y. bitvector_of_Z ? (offv x - offv y).
    9597definition zero_offset ≝ mk_offset OZ.
    9698definition lt_offset : offset → offset → bool ≝
     
    321323  ].
    322324
    323 definition zero_ext ≝ λnbits: Z. λv: val.
     325definition zero_ext ≝ λnbits: nat. λv: val.
    324326  match v with
    325327  [ Vint n ⇒ Vint (zero_ext nbits n)
     
    327329  ].
    328330
    329 definition sign_ext ≝ λnbits:Z. λv:val.
     331definition sign_ext ≝ λnbits:nat. λv:val.
    330332  match v with
    331333  [ Vint i ⇒ Vint (sign_ext nbits i)
     
    343345  match v1 with
    344346  [ Vint n1 ⇒ match v2 with
    345     [ Vint n2 ⇒ Vint (add n1 n2)
     347    [ Vint n2 ⇒ Vint (addition_n ? n1 n2)
    346348    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
    347349    | _ ⇒ Vundef ]
     
    354356  match v1 with
    355357  [ Vint n1 ⇒ match v2 with
    356     [ Vint n2 ⇒ Vint (sub n1 n2)
     358    [ Vint n2 ⇒ Vint (subtraction ? n1 n2)
    357359    | _ ⇒ Vundef ]
    358360  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    12051207qed.
    12061208
    1207 (*
    1208 Lemma zero_ext_lessdef:
    1209   forall n v1 v2, lessdef v1 v2 -> lessdef (zero_ext n v1) (zero_ext n v2).
    1210 Proof.
    1211   intros; inv H; simpl; auto.
    1212 Qed.
    1213 *)
     1209lemma zero_ext_lessdef:
     1210  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2).
     1211#n #v1 #v2 #H inversion H // #v #E1 #E2 destruct //
     1212qed.
     1213
    12141214lemma sign_ext_lessdef:
    12151215  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
Note: See TracChangeset for help on using the changeset viewer.