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

Update of D2.2 from Paris.

Location:
Deliverables/D2.2/8051/src/common
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/common/AST.mli

    r486 r619  
    9292
    9393
    94 (* Traces returned by interpreters: only cost labels are observed. *)
     94(* Traces returned by interpreters: result and cost labels are observed. The
     95   result is interpreted as an 8 bits integer for coherence between
     96   languages. *)
    9597
    96 type trace = CostLabel.t list
     98type trace = IntValue.int8 * CostLabel.t list
  • Deliverables/D2.2/8051/src/common/intValue.ml

    r486 r619  
     1
     2(** This module defines functions to manipulate bounded integers. They can be
     3    used to represent sequences of bits. *)
    14
    25open Big_int
    36
    47
     8(* Integers, whatever their size, will be represented using the Big_int
     9   module. This allows immediate conversion, and allows the representation of
     10   any integer (that fits into memory). *)
     11
    512type int_repr = Big_int.big_int
    613
     14(* The parameter module. Bounded integers are characterized by the number of
     15   bits used to represent them. *)
     16   
    717module type INTTYPE =
    818sig
    9   val size      : int (* in bytes *)
    10   val is_signed : bool
     19  val size : int (* in bytes *)
    1120end
     21
     22(* The signature provided to manipulate bounded integers. *)
    1223
    1324module type S = sig
     
    2031  val one       : t
    2132
    22   val succ   : t -> t
    23   val pred   : t -> t
    24   val add    : t -> t -> t
    25   (** [add_of i1 i2] returns true iff adding the unsigned value of [i1] and the
    26       unsigned value of [i2] overflows. *)
    27   val add_of : t -> t -> bool
    28   val sub    : t -> t -> t
    29   (** [sub_of i1 i2] returns true iff substracting the unsigned value of [i1]
    30       and the unsigned value of [i2] underflows. *)
    31   val sub_of : t -> t -> bool
    32   val mul    : t -> t -> t
    33   val div    : t -> t -> t
    34   val modulo : t -> t -> t
    35   val eq     : t -> t -> bool
    36   val neq    : t -> t -> bool
    37   val lt     : t -> t -> bool
    38   val le     : t -> t -> bool
    39   val gt     : t -> t -> bool
    40   val ge     : t -> t -> bool
    41   val neg    : t -> t
    42   val lognot : t -> t
    43   val logand : t -> t -> t
    44   val logor  : t -> t -> t
    45   val logxor : t -> t -> t
    46   val shl    : t -> t -> t
    47   val shr    : t -> t -> t
    48   val shrl   : t -> t -> t
    49   val max    : t -> t -> t
    50   val min    : t -> t -> t
    51   val cast   : int_repr -> t
    52   val of_int : int -> t
    53   val to_int : t -> int
     33  val succ    : t -> t
     34  val pred    : t -> t
     35  val add     : t -> t -> t
     36  (** [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *)
     37  val add_of  : t -> t -> bool
     38  val sub     : t -> t -> t
     39  (** [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2]
     40      underflows. *)
     41  val sub_uf  : t -> t -> bool
     42  val mul     : t -> t -> t
     43  val div     : t -> t -> t
     44  val divu    : t -> t -> t
     45  val modulo  : t -> t -> t
     46  val modulou : t -> t -> t
     47  val eq      : t -> t -> bool
     48  val neq     : t -> t -> bool
     49  val lt      : t -> t -> bool
     50  val ltu     : t -> t -> bool
     51  val le      : t -> t -> bool
     52  val leu     : t -> t -> bool
     53  val gt      : t -> t -> bool
     54  val gtu     : t -> t -> bool
     55  val ge      : t -> t -> bool
     56  val geu     : t -> t -> bool
     57  val neg     : t -> t
     58  val lognot  : t -> t
     59  val logand  : t -> t -> t
     60  val logor   : t -> t -> t
     61  val logxor  : t -> t -> t
     62  val shl     : t -> t -> t
     63  val shr     : t -> t -> t
     64  val shrl    : t -> t -> t
     65  val max     : t -> t -> t
     66  val maxu    : t -> t -> t
     67  val min     : t -> t -> t
     68  val minu    : t -> t -> t
     69  val cast    : int_repr -> t
     70  val of_int  : int -> t
     71  val to_int  : t -> int
     72
     73  (** [zero_ext n a] performs zero extension on [a] where [n] bits are
     74      significant. *)
     75  val zero_ext : int -> t -> t
     76  (** [sign_ext n a] performs sign extension on [a] where [n] bits are
     77      significant. *)
     78  val sign_ext : int -> t -> t
    5479
    5580  (** [break i n] cuts [i] in [n] parts. In the resulting list, the first
    5681      element is the high bits, and the last is the low bits. *)
    5782  val break : t -> int -> t list
    58   (** [merge l] creates an the integer where the first element of [l] is its
     83  (** [merge l] creates the integer where the first element of [l] is its
    5984      high bits, etc, and the last element of [l] is its low bits. *)
    6085  val merge : t list -> t
     
    6388
    6489
    65 (* First, we use a parameter module and a functor where integers may be
    66    unbounded. This will allow to create the Integer module (unbounded integers)
    67    as well as bounded integers. *)
    68 
    69 module type INTTYPE_ARB =
    70 sig
    71   val size      : int
    72   val is_signed : bool
    73   val arbitrary : bool
    74 end
    75 
    76 (* The following functor works for unbounded integers as well as for bounded
    77    intergers. *)
    78 
    79 module Make_Arb (IntType: INTTYPE_ARB) : S =
     90module Make (IntType: INTTYPE) : S =
    8091struct
    8192
     
    90101  let two = succ_big_int unit_big_int
    91102
    92   let half_bound = power_int_positive_int 2 (size-1)
    93 
    94   (* The upper bound of signed integers. *)
    95   let shbound = half_bound
    96   (* The lower bound of signed integers. *)
    97   let slbound = minus_big_int half_bound
    98 
    99   (* The upper bound of unsigned integers. *)
    100   let uhbound = mult_int_big_int 2 half_bound
    101   (* The lower bound of unsigned integers. *)
    102   let ulbound = zero
    103 
    104   (* [unsign a] returns the unsigned value of [a]. *)
    105   let unsign a =
    106     if lt_big_int a zero_big_int then add_big_int uhbound a
    107     else a
    108 
    109   (* [is_in_repr a] returns true iff [a] is a value comprised in the interval of
    110      representation. *)
    111   let is_in_repr a =
    112     if IntType.is_signed then (le_big_int slbound a) && (lt_big_int a shbound)
    113     else (le_big_int ulbound a) && (lt_big_int a uhbound)
     103  (* Integers will all be taken modulo the following value. *)
     104  let _mod = power_int_positive_int 2 size
     105
     106  (* The lower bound (inclusive). *)
     107  let lower_bound = zero
     108  (* The upper bound (inclusive). *)
     109  let upper_bound = pred_big_int _mod
    114110
    115111  (* [cast a] returns a modulo of [a] such that the result fits in the interval
    116112     of representation. *)
    117   let cast a =
    118     if IntType.arbitrary then a
    119     else
    120       if is_in_repr a then a
    121       else
    122         if IntType.is_signed then
    123           sub_big_int
    124             (mod_big_int (add_big_int a half_bound) uhbound)
    125             half_bound
    126         else mod_big_int a uhbound
     113  let cast a = mod_big_int a _mod
     114
     115  (* Half bound (exclusive), i.e. upper bound of signed integers. *)
     116  let half_bound = power_int_positive_int 2 (size-1)
     117
     118  (* Signed value of [a]. *)
     119  let signed a = sub_big_int (cast a) half_bound
     120
     121  let signed_op op a b = op (signed a) (signed b)
    127122
    128123  let succ a = cast (succ_big_int a)
     
    130125  let add a b = cast (add_big_int a b)
    131126
    132   (* [add_of i1 i2] returns true iff adding the unsigned value of [i1] and the
    133      unsigned value of [i2] overflows. *)
    134   let add_of a b =
    135     let u1 = unsign a in
    136     let u2 = unsign b in
    137     let i = add_big_int u1 u2 in
    138     ge_big_int i uhbound
     127  (* [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *)
     128  let add_of a b = gt_big_int (add_big_int a b) upper_bound
    139129
    140130  let sub a b = cast (sub_big_int a b)
    141131
    142   (* [sub_of i1 i2] returns true iff substracting the unsigned value of [i1] and
    143      the unsigned value of [i2] underflows. *)
    144   let sub_of a b =
    145     let u1 = unsign a in
    146     let u2 = unsign b in
    147     let i = sub_big_int u1 u2 in
    148     lt_big_int i zero_big_int
     132  let cast_op op a b = op (cast a) (cast b)
    149133
    150134  let mul a b = cast (mult_big_int a b)
    151   let div a b = cast (div_big_int a b)
    152   let modulo a b = cast (mod_big_int a b)
     135  let div a b = cast (signed_op div_big_int a b)
     136  let divu a b = cast_op div_big_int a b
     137  let modulo a b = cast (signed_op mod_big_int a b)
     138  let modulou a b = cast_op mod_big_int a b
     139
    153140  let eq = eq_big_int
    154141  let neq a b = not (eq a b)
    155   let lt a b = lt_big_int (cast a) (cast b)
    156   let le a b = le_big_int (cast a) (cast b)
    157   let gt a b = gt_big_int (cast a) (cast b)
    158   let ge a b = ge_big_int (cast a) (cast b)
     142  let lt a b = signed_op lt_big_int a b
     143  let le a b = signed_op le_big_int a b
     144  let gt a b = signed_op gt_big_int a b
     145  let ge a b = signed_op ge_big_int a b
     146  let ltu a b = cast_op lt_big_int a b
     147  let leu a b = cast_op le_big_int a b
     148  let gtu a b = cast_op gt_big_int a b
     149  let geu a b = cast_op ge_big_int a b
     150
     151  (* [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2] underflows. *)
     152  let sub_uf a b = lt_big_int (sub_big_int a b) zero
     153
    159154  let of_int i = cast (big_int_of_int i)
    160   let to_int i = int_of_big_int i
     155  let to_int i = int_of_big_int (cast i)
     156
    161157  let neg a = cast (minus_big_int a)
    162158
    163   let lognot a =
    164     let mone = minus_big_int unit_big_int in
    165     if IntType.is_signed then sub mone a
    166     else sub (pred uhbound) a
     159  let lognot = sub upper_bound
    167160
    168161  let shl a b =
    169     let pow = power_int_positive_big_int 2 b in
     162    let pow = power_int_positive_big_int 2 (cast b) in
    170163    cast (mult_big_int a pow)
    171164
    172165  let shr a b =
    173     let pow = power_int_positive_big_int 2 b in
    174     cast (div_big_int a pow)
    175 
    176   let shrl a b =
     166    let a = cast a in
     167    let b = cast b in
    177168    let added =
    178       if IntType.is_signed || (lt_big_int b half_bound) then zero_big_int
     169      if lt_big_int a half_bound then zero
    179170      else half_bound in
    180171    let rec aux acc b =
    181       if eq_big_int b zero_big_int then acc
     172      if eq b zero then acc
    182173      else
    183         let cont_acc = add_big_int added (div_big_int acc two) in
    184         let cont_b = pred_big_int b in
     174        let cont_acc = add added (divu acc two) in
     175        let cont_b = pred b in
    185176        aux cont_acc cont_b
    186177    in
    187178    cast (aux a b)
     179
     180  let shrl a b =
     181    let pow = power_int_positive_big_int 2 (cast b) in
     182    cast (div_big_int (cast a) pow)
    188183
    189184  let max a b = if lt a b then b else a
    190185  let min a b = if gt a b then b else a
    191 
    192   let is_odd a = eq_big_int (mod_big_int a two) unit_big_int
    193   (* [to_bits a] returns the list of bits (0 or 1) that a represents. Signed
    194      integers are represented using the 2-complement representation. *)
     186  let maxu a b = if ltu a b then b else a
     187  let minu a b = if gtu a b then b else a
     188
     189  let is_odd a = eq (modulou a two) one
     190  (* [to_bits a] returns the list of bits (0 or 1) that [a] represents. *)
    195191  let to_bits a =
    196192    let rec aux acc a i =
    197193      if i >= size then acc
    198       else aux ((is_odd a) :: acc) (div_big_int a two) (i+1)
    199     in
    200     aux [] a 0
     194      else aux ((is_odd a) :: acc) (divu a two) (i+1)
     195    in
     196    aux [] (cast a) 0
    201197
    202198  (* [from_bits bits] returns the integer that the list of bits [bits]
    203      represents. Signed integers are represented using the 2-complement
    204      representation. *)
     199     represents. *)
    205200  let from_bits bits =
    206201    let rec aux acc = function
    207202      | [] -> acc
    208203      | b :: bits ->
    209         let next_acc = mult_int_big_int 2 acc in
    210         let next_acc = if b then succ_big_int next_acc else next_acc in
     204        let next_acc = mul acc two in
     205        let next_acc = if b then succ next_acc else next_acc in
    211206        aux next_acc bits
    212207    in
    213     cast (aux zero_big_int bits)
     208    aux zero bits
    214209
    215210  (* [binary_log_op f a b] applies the binary boolean operation [f]
     
    224219  let logxor = binary_log_op xor
    225220
     221
     222  (* [zero_ext n a] performs zero extension on [a] where [n] bits are
     223     significant. *)
     224  let zero_ext n a =
     225    let pow2 = power_int_positive_int 2 n in
     226    cast (mod_big_int a pow2)
     227
     228  (* [sign_ext n a] performs sign extension on [a] where [n] bits are
     229     significant. *)
     230  let sign_ext n a =
     231    let a' = zero_ext n a in
     232    let pow2 = power_int_positive_int 2 (n-1) in
     233    let sign = divu a pow2 in
     234    if is_odd sign then
     235      let added = shr half_bound (of_int (n-1)) in
     236      add a' added
     237    else a'
     238
     239
    226240  (* [break i n] cuts [i] in [n] parts. In the resulting list, the first element
    227241     is the high bits, and the last is the low bits. *)
    228242  let break a n =
    229     let chunk_size = (8 * IntType.size) / n in
     243    let chunk_size = size / n in
    230244    let pow2_chunk_size = power_int_positive_int 2 chunk_size in
    231245    let rec aux acc a i =
    232246      if i = 0 then acc
    233247      else
    234         let (next, chunk) = Big_int.quomod_big_int a pow2_chunk_size in
     248        let (next, chunk) = quomod_big_int a pow2_chunk_size in
    235249        aux ((cast chunk) :: acc) next (i-1)
    236250    in
    237     aux [] a n
     251    aux [] (cast a) n
    238252
    239253  (* [merge l] creates the integer where the first element of [l] is its high
     
    244258      let al = List.rev al in
    245259      let nb_chunks = List.length al in
    246       let chunk_size = (8 * IntType.size) / nb_chunks in
     260      let chunk_size = size / nb_chunks in
    247261      let pow2_chunk_size = power_int_positive_int 2 chunk_size in
    248262      let rec aux pow2 = function
     
    255269
    256270
    257 module Make (IntType : INTTYPE) =
    258   Make_Arb (struct include IntType let arbitrary = false end)
    259 
    260 
    261 module Int8s : S = Make
    262   (struct
    263     let size = 1
    264     let is_signed = true
    265    end)
    266 
    267 module Int8u : S = Make
    268   (struct
    269     let size = 1
    270     let is_signed = false
    271    end)
    272 
    273 module Int16s : S = Make
    274   (struct
    275     let size = 2
    276     let is_signed = true
    277    end)
    278 
    279 module Int16u : S = Make
    280   (struct
    281     let size = 2
    282     let is_signed = false
    283    end)
    284 
    285 module Int32 : S = Make
    286   (struct
    287     let size = 4
    288     let is_signed = true
    289    end)
    290 
    291 module Integer : S = Make_Arb
    292   (struct
    293     let size = 1
    294     let is_signed = true
    295     let arbitrary = true
    296    end)
    297 
    298 
    299 type int8s   = Int8s.t
    300 type int8u   = Int8u.t
    301 type int16s  = Int16s.t
    302 type int16u  = Int16u.t
    303 type int32   = Int32.t
    304 type integer = Integer.t
     271module Int8  : S = Make (struct let size = 1 end)
     272module Int16 : S = Make (struct let size = 2 end)
     273module Int32 : S = Make (struct let size = 4 end)
     274
     275type int8  = Int8.t
     276type int16 = Int16.t
     277type int32 = Int32.t
  • Deliverables/D2.2/8051/src/common/intValue.mli

    r486 r619  
    11
    2 (** This module defines functions to manipulate integers coded on various number
    3     of bits (sized integers). *)
     2(** This module defines functions to manipulate bounded integers. They can be
     3    used to represent sequences of bits. *)
    44
    55(* Integers, whatever their size, will be represented using the Big_int
     
    99type int_repr = Big_int.big_int
    1010
    11 (* The parameter module. Sized integers are characterized by the number of bits
    12    used to represent them, and the fact that they are signed or not. *)
     11(* The parameter module. Bounded integers are characterized by the number of
     12   bits used to represent them. *)
    1313   
    1414module type INTTYPE =
    1515sig
    16   val size      : int (* in bytes *)
    17   val is_signed : bool
     16  val size : int (* in bytes *)
    1817end
    1918
    20 (* The signature provided to manipulate sized integers. *)
     19(* The signature provided to manipulate bounded integers. *)
    2120
    2221module type S = sig
     
    2928  val one       : t
    3029
    31   val succ   : t -> t
    32   val pred   : t -> t
    33   val add    : t -> t -> t
    34   (** [add_of i1 i2] returns true iff adding the unsigned value of [i1] and the
    35       unsigned value of [i2] overflows. *)
    36   val add_of : t -> t -> bool
    37   val sub    : t -> t -> t
    38   (** [sub_of i1 i2] returns true iff substracting the unsigned value of [i1]
    39       and the unsigned value of [i2] overflows. *)
    40   val sub_of : t -> t -> bool
    41   val mul    : t -> t -> t
    42   val div    : t -> t -> t
    43   val modulo : t -> t -> t
    44   val eq     : t -> t -> bool
    45   val neq    : t -> t -> bool
    46   val lt     : t -> t -> bool
    47   val le     : t -> t -> bool
    48   val gt     : t -> t -> bool
    49   val ge     : t -> t -> bool
    50   val neg    : t -> t
    51   val lognot : t -> t
    52   val logand : t -> t -> t
    53   val logor  : t -> t -> t
    54   val logxor : t -> t -> t
    55   val shl    : t -> t -> t
    56   val shr    : t -> t -> t
    57   val shrl   : t -> t -> t
    58   val max    : t -> t -> t
    59   val min    : t -> t -> t
    60   val cast   : int_repr -> t
    61   val of_int : int -> t
    62   val to_int : t -> int
     30  val succ    : t -> t
     31  val pred    : t -> t
     32  val add     : t -> t -> t
     33  (** [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *)
     34  val add_of  : t -> t -> bool
     35  val sub     : t -> t -> t
     36  (** [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2]
     37      underflows. *)
     38  val sub_uf  : t -> t -> bool
     39  val mul     : t -> t -> t
     40  val div     : t -> t -> t
     41  val divu    : t -> t -> t
     42  val modulo  : t -> t -> t
     43  val modulou : t -> t -> t
     44  val eq      : t -> t -> bool
     45  val neq     : t -> t -> bool
     46  val lt      : t -> t -> bool
     47  val ltu     : t -> t -> bool
     48  val le      : t -> t -> bool
     49  val leu     : t -> t -> bool
     50  val gt      : t -> t -> bool
     51  val gtu     : t -> t -> bool
     52  val ge      : t -> t -> bool
     53  val geu     : t -> t -> bool
     54  val neg     : t -> t
     55  val lognot  : t -> t
     56  val logand  : t -> t -> t
     57  val logor   : t -> t -> t
     58  val logxor  : t -> t -> t
     59  val shl     : t -> t -> t
     60  val shr     : t -> t -> t
     61  val shrl    : t -> t -> t
     62  val max     : t -> t -> t
     63  val maxu    : t -> t -> t
     64  val min     : t -> t -> t
     65  val minu    : t -> t -> t
     66  val cast    : int_repr -> t
     67  val of_int  : int -> t
     68  val to_int  : t -> int
     69
     70  (** [zero_ext n a] performs zero extension on [a] where [n] bits are
     71      significant. *)
     72  val zero_ext : int -> t -> t
     73  (** [sign_ext n a] performs sign extension on [a] where [n] bits are
     74      significant. *)
     75  val sign_ext : int -> t -> t
    6376
    6477  (** [break i n] cuts [i] in [n] parts. In the resulting list, the first
     
    7184end
    7285
    73 (** The functor to create bounded integers from a size and a signedness. *)
     86(** The functor to create bounded integers from a size. *)
    7487
    7588module Make: functor (IntType: INTTYPE) -> S
    7689
     90module Int8  : S
     91module Int16 : S
     92module Int32 : S
     93
     94type int8  = Int8.t
     95type int16 = Int16.t
     96type int32 = Int32.t
     97
     98
     99(*
    77100module Int8s   : S
    78101module Int8u   : S
     
    90113type int32   = Int32.t
    91114type integer = Integer.t
     115*)
  • Deliverables/D2.2/8051/src/common/memory.ml

    r486 r619  
    192192    | Some alignment when (size <= alignment) && (is_multiple size alignment) ->
    193193      let size = Offset.of_int size in
    194       let rem = Offset.modulo off size in
     194      let rem = Offset.modulou off size in
    195195      if Offset.eq rem Offset.zero then off
    196196      else Offset.add off (Offset.sub size rem)
    197197    | Some alignment ->
    198198      let size = Offset.of_int alignment in
    199       let rem = Offset.modulo off size in
     199      let rem = Offset.modulou off size in
    200200      if Offset.eq rem Offset.zero then off
    201201      else Offset.add off (Offset.sub size rem)
     
    263263  (* Pretty printing *)
    264264
    265 let print mem =
     265  let print mem =
    266266    let print_cells off = function
    267267      | Datum (size, v) when Value.eq v Value.undef ->
     
    275275      match content with
    276276        | Contents contents ->
    277             Printf.printf "(%s -> %s)%!"
    278               (Offset.to_string contents.low) (Offset.to_string contents.high) ;
    279             OffsetMap.iter print_cells contents.cells
     277          Printf.printf "(%s -> %s)%!"
     278            (Offset.to_string contents.low) (Offset.to_string contents.high) ;
     279          OffsetMap.iter print_cells contents.cells
    280280        | Fun_def _ -> Printf.printf "function definition%!" ;
    281281    in
    282282    BlockMap.iter print_block mem.blocks ;
    283283    Printf.printf "\n%!"
    284 
    285 
    286284
    287285
     
    405403    all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef) ; Cont]
    406404
     405  let string_of_alignment = function
     406    | None -> "none"
     407    | Some alignment -> string_of_int alignment
     408
    407409  (** [write_value msg mem b off size v size'] store the value [v] at the offset
    408410      [off] of the block [b] in the memory [mem]. [size] is the size of the
  • Deliverables/D2.2/8051/src/common/memory.mli

    r486 r619  
    108108              (int list (* resulting offsets *) * int (* full size *))
    109109
    110   val size_of_datas    : AST.data list -> int
     110  val size_of_datas : AST.data list -> int
    111111
    112112  (** [offsets_of_datas datas] returns the aligned offsets for the datas
     
    114114  val offsets_of_datas : AST.data list -> (AST.data * int (* offset *)) list
    115115
    116   val alloc_datas      : 'fun_def memory -> AST.data list ->
    117                          ('fun_def memory * Value.t)
     116  val alloc_datas : 'fun_def memory -> AST.data list ->
     117                    ('fun_def memory * Value.t)
    118118
    119119  val print : 'fun_def memory -> unit
  • 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 (=)
  • Deliverables/D2.2/8051/src/common/value.mli

    r486 r619  
    6464  val undef     : t
    6565
    66   (** [cast8unsigned v] returns undefined for non-integer values. For integer
    67       values, it supposes that the value is a 8 bit unsigned integer. It will
    68       return the integer value that represents the same quantity, but using
    69       every bits. The other cast operations behave the same way. *)
     66
     67  (** Sign or 0 extensions from various bounded integers. *)
    7068  val cast8unsigned  : t -> t
    7169  val cast8signed    : t -> t   
     
    9694  val add_and_of : t -> t -> (t * t)
    9795  val add        : t -> t -> t
    98   (** [add_of v1 v2] returns the 1 value if the sum of [v1] and [v2]
    99       overflows, and 0 otherwise. *)
     96  (** [add_of v1 v2] returns the [1] value if the sum of [v1] and [v2]
     97      overflows, and [0] otherwise. *)
    10098  val add_of     : t -> t -> t
    10199  (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether
    102       this substraction overflows. *)
    103   val sub_and_of : t -> t -> (t * t)
     100      this substraction underflows. *)
     101  val sub_and_uf : t -> t -> (t * t)
    104102  val sub        : t -> t -> t
    105   (** [sub_of v1 v2] returns the 1 value if the substraction of [v1] and [v2]
    106       overflows, and 0 otherwise. *)
    107   val sub_of     : t -> t -> t
     103  (** [sub_of v1 v2] returns the [1] value if the substraction of [v1] and [v2]
     104      underflows, and [0] otherwise. *)
     105  val sub_uf     : t -> t -> t
    108106  val mul        : t -> t -> t
    109107  val div        : t -> t -> t
    110108  val divu       : t -> t -> t
    111109  val modulo     : t -> t -> t
    112   val modu       : t -> t -> t
     110  val modulou    : t -> t -> t
    113111  val and_op     : t -> t -> t
    114112  val or_op      : t -> t -> t
Note: See TracChangeset for help on using the changeset viewer.