Ignore:
Timestamp:
Mar 2, 2011, 3:27:41 PM (9 years ago)
Author:
ayache
Message:

Update of D2.2 from Paris.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/common/value.ml

    r486 r619  
    103103  val add_and_of : t -> t -> (t * t)
    104104  val add        : t -> t -> t
    105   (** [add_of v1 v2] returns the 1 value if the sum of [v1] and [v2]
    106       overflows, and 0 otherwise. *)
     105  (** [add_of v1 v2] returns the [1] value if the sum of [v1] and [v2]
     106      overflows, and [0] otherwise. *)
    107107  val add_of     : t -> t -> t
    108108  (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether
    109       this substraction overflows. *)
    110   val sub_and_of : t -> t -> (t * t)
     109      this substraction underflows. *)
     110  val sub_and_uf : t -> t -> (t * t)
    111111  val sub        : t -> t -> t
    112   (** [sub_of v1 v2] returns the 1 value if the substraction of [v1] and [v2]
    113       overflows, and 0 otherwise. *)
    114   val sub_of     : t -> t -> t
     112  (** [sub_of v1 v2] returns the [1] value if the substraction of [v1] and [v2]
     113      underflows, and [0] otherwise. *)
     114  val sub_uf     : t -> t -> t
    115115  val mul        : t -> t -> t
    116116  val div        : t -> t -> t
    117117  val divu       : t -> t -> t
    118118  val modulo     : t -> t -> t
    119   val modu       : t -> t -> t
     119  val modulou    : t -> t -> t
    120120  val and_op     : t -> t -> t
    121121  val or_op      : t -> t -> t
     
    166166  (* This module will be used to represent integer values. *)
    167167  module Int =
    168     IntValue.Make (struct let size = D.int_size let is_signed = true end)
    169 
    170   (* This module will be used to define unsigned operations on integer
    171      values. *)
    172   module Intu =
    173     IntValue.Make (struct let size = D.int_size let is_signed = false end)
     168    IntValue.Make (struct let size = D.int_size end)
    174169
    175170  (* Addresses are represented by a block, i.e. a base address, and an offset
     
    183178
    184179  module Block =
    185     IntValue.Make (struct let size = D.ptr_size let is_signed = true end)
     180    IntValue.Make (struct let size = D.ptr_size end)
    186181  module Offset = (* Block *)
    187     IntValue.Make (struct let size = D.ptr_size let is_signed = true end)
     182    IntValue.Make (struct let size = D.ptr_size end)
    188183
    189184  (* We want to be able to put an address into registers, and we want to be able
     
    226221    | _, Val_ptrl _ -> -1
    227222
     223(*
    228224  let hash = function
    229225    | Val_int i -> Int.to_int i
     
    232228    | Val_ptr (b,o)
    233229    | Val_ptrh (b,o)
    234     | Val_ptrl (b,o) -> Integer.to_int (Integer.add b o)
     230    | Val_ptrl (b,o) -> Int.to_int (Int.add b o)
     231*)
     232
     233  let hash = Hashtbl.hash
    235234
    236235  let equal a b = compare a b = 0
     
    315314    | _ -> Val_undef
    316315
    317   (** [cast8unsigned v] returns undefined for non-integer values. For integer
    318       values, it supposes that the value is a 8 bit unsigned integer. It will
    319       return the integer value that represents the same quantity, but using
    320       every bits (2-completement representation). The other cast operations
    321       behave the same way. *)
    322 
    323   let cast8unsigned = cast Int8u.cast
    324   let cast8signed = cast Int8s.cast
    325   let cast16unsigned = cast Int16u.cast
    326   let cast16signed = cast Int16s.cast
    327   let cast32 = cast Int32.cast
     316  (** Sign or 0 extensions from various bounded integers. *)
     317  let cast8unsigned = cast (Int.zero_ext 8)
     318  let cast8signed = cast (Int.sign_ext 8)
     319  let cast16unsigned = cast (Int.zero_ext 16)
     320  let cast16signed = cast (Int.sign_ext 16)
     321  let cast32 = cast (Int.zero_ext 32)
    328322
    329323
     
    335329    | Val_int i1, Val_int i2 -> Val_int (f i1 i2)
    336330    | _ -> Val_undef
    337 
    338   let binary_intu_op f v1 v2 = match v1, v2 with
    339     | Val_int i1, Val_int i2 ->
    340       Val_int (Int.cast (f (Intu.cast i1) (Intu.cast i2)))
    341     | _, _ -> Val_undef
    342 
    343   let binary_int_cmp f v1 v2 = match v1, v2 with
    344     | Val_int i1, Val_int i2 -> of_bool (f i1 i2)
    345     | _, _ -> Val_undef
    346 
    347   let binary_intu_cmp f v1 v2 = match v1, v2 with
    348     | Val_int i1, Val_int i2 ->
    349       of_bool (f (Intu.cast i1) (Intu.cast i2))
    350     | _, _ -> Val_undef
    351331
    352332  let unary_float_op f = function
     
    431411  let succ v = add v (Val_int Int.one)
    432412
    433   (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether
    434       this substraction overflows. *)
    435   let sub_and_of v1 v2 = match v1, v2 with
     413  (** [sub_and_uf v1 v2] returns the substraction of [v1] and [v2], and whether
     414      this substraction underflows. *)
     415  let sub_and_uf v1 v2 = match v1, v2 with
    436416    | Val_int i1, Val_int i2 ->
    437       (Val_int (Int.sub i1 i2), of_bool (Int.sub_of i1 i2))
     417      (Val_int (Int.sub i1 i2), of_bool (Int.sub_uf i1 i2))
    438418    | Val_ptr (b, off), Val_int i ->
    439419      (Val_ptr (b, Offset.sub off i),
    440        of_bool (Offset.sub_of off (Offset.cast i)))
     420       of_bool (Offset.sub_uf off (Offset.cast i)))
    441421    | Val_ptrh (b, off), Val_int i ->
    442422      (Val_ptrh (b, Offset.sub off i),
    443        of_bool (Offset.sub_of off (Offset.cast i)))
     423       of_bool (Offset.sub_uf off (Offset.cast i)))
    444424    | Val_ptrl (b, off), Val_int i ->
    445425      (Val_ptrl (b, Offset.sub off i),
    446        of_bool (Offset.sub_of off (Offset.cast i)))
     426       of_bool (Offset.sub_uf off (Offset.cast i)))
    447427    | Val_ptr (b1, off1), Val_ptr (b2, off2)
    448428    | Val_ptrh (b1, off1), Val_ptrh (b2, off2)
    449429    | Val_ptrl (b1, off1), Val_ptrl (b2, off2) when Block.eq b1 b2 ->
    450430      (Val_int (Int.cast (Offset.sub off1 off2)),
    451        of_bool (Offset.sub_of off1 off2))
     431       of_bool (Offset.sub_uf off1 off2))
    452432    | _, _ -> (Val_undef, Val_undef)
    453433
    454   let sub v1 v2 = fst (sub_and_of v1 v2)
    455   let sub_of v1 v2 = snd (sub_and_of v1 v2)
     434  let sub v1 v2 = fst (sub_and_uf v1 v2)
     435  let sub_uf v1 v2 = snd (sub_and_uf v1 v2)
    456436
    457437  let pred v = sub v (Val_int Int.one)
     
    471451  let divu v1 v2 =
    472452    if is_zero v2 then Val_undef
    473     else binary_intu_op Intu.div v1 v2
     453    else binary_int_op Int.divu v1 v2
    474454
    475455  let modulo v1 v2 =
     
    477457    else binary_int_op Int.modulo v1 v2
    478458
    479   let modu v1 v2 =
     459  let modulou v1 v2 =
    480460    if is_zero v2 then Val_undef
    481     else binary_intu_op Intu.modulo v1 v2
     461    else binary_int_op Int.modulou v1 v2
    482462
    483463  let and_op = binary_int_op Int.logand
     
    503483    | _ -> Val_undef
    504484
    505   let cmpp_eq f_int v1 v2 = match v1, v2 with
     485  let cmp f_int f_ptr v1 v2 = match v1, v2 with
    506486    | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2)
    507487    | Val_ptr (b1, off1), Val_ptr (b2, off2)
    508488    | Val_ptrh (b1, off1), Val_ptrh (b2, off2)
    509     | Val_ptrl (b1, off1), Val_ptrl (b2, off2) ->
    510       of_bool ((Block.eq b1 b2) && (Offset.eq off1 off2))
    511     | _ -> Val_undef
    512 
    513   let cmpp_ne cmp_eq v1 v2 = notbool (cmp_eq v1 v2)
    514 
    515   let cmpp_lt f_int v1 v2 = match v1, v2 with
    516     | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2)
    517     | Val_ptr (b1, off1), Val_ptr (b2, off2)
    518     | Val_ptrh (b1, off1), Val_ptrh (b2, off2)
    519     | Val_ptrl (b1, off1), Val_ptrl (b2, off2) ->
    520       of_bool ((Block.lt b1 b2) ||
    521                ((Block.eq b1 b2) && (Offset.lt off1 off2)))
    522     | _ -> Val_undef
    523 
    524   let cmpp_ge cmp_lt v1 v2 = notbool (cmp_lt v1 v2)
    525   let cmpp_le cmp_lt cmp_eq v1 v2 = orbool (cmp_lt v1 v2) (cmp_eq v1 v2)
    526   let cmpp_gt cmp_le v1 v2 = notbool (cmp_le v1 v2)
    527 
    528   let cmp_eq = cmpp_eq Int.eq
    529   let cmp_ne = cmpp_ne cmp_eq
    530   let cmp_lt = cmpp_lt Int.lt
    531   let cmp_ge = cmpp_ge cmp_lt
    532   let cmp_le = cmpp_le cmp_lt cmp_eq
    533   let cmp_gt = cmpp_gt cmp_le
    534 
    535   let cmp_eq_u = cmpp_eq Intu.eq
    536   let cmp_ne_u = cmpp_ne cmp_eq_u
    537   let cmp_lt_u = cmpp_lt Intu.lt
    538   let cmp_ge_u = cmpp_ge cmp_lt_u
    539   let cmp_le_u = cmpp_le cmp_lt_u cmp_eq_u
    540   let cmp_gt_u = cmpp_gt cmp_le_u
     489    | Val_ptrl (b1, off1), Val_ptrl (b2, off2) when Block.eq b1 b2 ->
     490      of_bool (f_ptr off1 off2)
     491    | _ -> Val_undef
     492
     493  let cmp_eq = cmp Int.eq Offset.eq
     494  let cmp_ne = cmp Int.neq Offset.neq
     495  let cmp_lt = cmp Int.lt Offset.lt
     496  let cmp_ge = cmp Int.ge Offset.ge
     497  let cmp_le = cmp Int.le Offset.le
     498  let cmp_gt = cmp Int.gt Offset.gt
     499
     500  let cmp_eq_u = cmp Int.eq Offset.eq
     501  let cmp_ne_u = cmp Int.neq Offset.neq
     502  let cmp_lt_u = cmp Int.ltu Offset.ltu
     503  let cmp_ge_u = cmp Int.geu Offset.geu
     504  let cmp_le_u = cmp Int.leu Offset.leu
     505  let cmp_gt_u = cmp Int.gtu Offset.gtu
    541506
    542507  let cmp_eq_f = binary_float_cmp (=)
Note: See TracChangeset for help on using the changeset viewer.