src/common/value.ml

   1
   2 (** This module describes the values manipulated by high level
   3     languages. *)
   4
   5
   6 let error_prefix = "Value"
   7 let error s = Error.global_error error_prefix s
   8
   9 open IntValue
  10
  11
  12 (** The representation of values depends on the size of integers and the size of
  13     addresses.  *)
  14
  15 (** This is the signature of the parameter module. *)
  16
  17 module type DATA_SIZE =
  18 sig
  19   val int_size : int
  20   val ptr_size : int
  21 end
  22
  23 (** This is the signature of the module that provides types and functions to
  24     manipulate values. *)
  25
  26 module type S =
  27 sig
  28
  29   val int_size : int
  30   val ptr_size : int
  31
  32   (** The type of values. A value may be: a bounded integer, a chunk of an
  33       address (exactly an address when they have the same size as a machine
  34       register), or undefined. *)
  35   type t
  36
  37   val compare : t -> t -> int
  38   val equal : t -> t -> bool
  39   val eq : t -> t -> bool
  40   val hash : t -> int
  41   val to_string : t -> string
  42
  43   (* The functions of this module may raise a Failure exception when
  44      trying to convert them to their various representation. *)
  45
  46   val is_int : t -> bool
  47   val to_int : t -> int
  48   val of_int : int -> t
  49
  50   val of_int_repr : IntValue.int_repr -> t
  51   val to_int_repr : t -> IntValue.int_repr
  52
  53   val of_bool   : bool -> t
  54   val to_bool   : t -> bool
  55
  56   val zero      : t
  57   val val_true  : t
  58   val val_false : t
  59   val is_true   : t -> bool
  60   val is_false  : t -> bool
  61   val undef     : t
  62
  63   (** The cast operations below returns the undefined value for non-integer
  64       values. For integer values, it will return the integer value that
  65       represents the same quantity, but using every bits (sign or zero
  66       extension) of an integer value. For example, the function [cast8unsigned]
  67       should be read as "cast from an 8 bits unsigned integer". *)
  68   val cast8unsigned  : t -> t
  69   val cast8signed    : t -> t
  70   val cast16unsigned : t -> t
  71   val cast16signed   : t -> t
  72   val cast32         : t -> t
  73
  74   (** [zero_ext v n m] performs a zero extension on [v] where [n] bytes are
  75       significant to a value where [m] bytes are significant. *)
  76   val zero_ext : t -> int -> int -> t
  77   (** [sign_ext v n m] performs a sign extension on [v] where [n] bytes are
  78       significant to a value where [m] bytes are significant. *)
  79   val sign_ext : t -> int -> int -> t
  80
  81   (** Integer opposite *)
  82   val negint  : t -> t
  83   (** Boolean negation *)
  84   val notbool : t -> t
  85   (** Bitwise not *)
  86   val notint  : t -> t
  87
  88   val succ : t -> t
  89   val pred : t -> t
  90   val cmpl : t -> t
  91
  92   (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
  93       overflows. *)
  94   val add_and_of : t -> t -> (t * t)
  95   val add        : t -> t -> t
  96   (** [add_of v1 v2] returns the [1] value if the sum of [v1] and [v2]
  97       overflows, and [0] otherwise. *)
  98   val add_of     : t -> t -> t
  99   (** [sub_and_uf v1 v2] returns the substraction of [v1] and [v2], and whether
 100       this substraction underflows. *)
 101   val sub_and_uf : t -> t -> (t * t)
 102   val sub        : t -> t -> t
 103   (** [sub_uf 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
 106   val mul        : t -> t -> t
 107   val div        : t -> t -> t
 108   val divu       : t -> t -> t
 109   val modulo     : t -> t -> t
 110   val modulou    : t -> t -> t
 111   val and_op     : t -> t -> t
 112   val or_op      : t -> t -> t
 113   val xor        : t -> t -> t
 114   val shl        : t -> t -> t
 115   val shr        : t -> t -> t
 116   val shru       : t -> t -> t
 117
 118   (** Signed comparisions *)
 119   val cmp_eq : t -> t -> t
 120   val cmp_ne : t -> t -> t
 121   val cmp_lt : t -> t -> t
 122   val cmp_ge : t -> t -> t
 123   val cmp_le : t -> t -> t
 124   val cmp_gt : t -> t -> t
 125
 126   (** Unsigned comparisions *)
 127   val cmp_eq_u : t -> t -> t
 128   val cmp_ne_u : t -> t -> t
 129   val cmp_lt_u : t -> t -> t
 130   val cmp_ge_u : t -> t -> t
 131   val cmp_le_u : t -> t -> t
 132   val cmp_gt_u : t -> t -> t
 133
 134   (** A chunk is a part of a value that has the size of a memory cell. *)
 135
 136   type chunk
 137   val string_of_chunk : chunk -> string
 138   val undef_byte : chunk
 139   val is_undef_byte : chunk -> bool
 140
 141   (** [break v] cuts [v] in chunks that each fits into a memory cell. In the
 142       resulting list, the first element is the low bits, and the last is the
 143       high bits (little endian representation). *)
 144   val break : t -> chunk list
 145   (** [merge l] creates the value where the first element of [l] is its low
 146       bits, etc, and the last element of [l] is its high bits (little endian
 147       representation). *)
 148   val merge : chunk list -> t
 149
 150   (** Addresses from the memory point of view. *)
 151
 152   (** Some architectures have pointers bigger than integers. In this case, only
 153       a chunk of pointer can fit into a machine register. Thus, an address is
 154       represented by several values (little endian representation). *)
 155
 156   type address = t list
 157   val string_of_address : address -> string
 158   val null : address
 159
 160   (** Addresses from the memory point of view. Only use the functions below in
 161       the Memory module.*)
 162
 163   (** Addresses are represented by a block, i.e. a base address, and an offset
 164       from this block. Both blocks and offsets are represented using bounded
 165       integers. *)
 166   module Block  : IntValue.S
 167   module Offset : IntValue.S
 168
 169   type mem_address
 170   val string_of_mem_address : mem_address -> string
 171
 172   val is_mem_address : address -> bool
 173
 174   val of_mem_address        : mem_address -> address
 175   val to_mem_address        : address -> mem_address
 176   val make_mem_address      : Block.t -> Offset.t -> mem_address
 177   val decompose_mem_address : mem_address -> Block.t * Offset.t
 178   val block_of_address      : address -> Block.t
 179   val offset_of_address     : address -> Offset.t
 180
 181   val change_address_offset : address -> Offset.t -> address
 182   val add_address           : address -> Offset.t -> address
 183   val eq_address            : address -> address -> bool
 184
 185 end
 186
 187
 188 module Make (D : DATA_SIZE) =
 189 struct
 190
 191   let int_size = D.int_size
 192   let ptr_size = D.ptr_size
 193
 194   module BoundedInt = IntValue.Make (struct let size = D.int_size end)
 195
 196   (* Integer values. *)
 197   module ValInt = BoundedInt
 198
 199   (* Addresses are represented by a block, i.e. a base address, and an offset
 200      from this block. Both blocks and offsets are represented using bounded
 201      integers. However, values must fit into a machine register. Some
 202      architectures, like the 8051, have addresses bigger than registers. Pointer
 203      values will only represent a part of a full pointer (or exactly a pointer
 204      when addresses fit into a register). *)
 205
 206   (* Blocks and offsets need [D.ptr_size] bits each to be represented. Indeed,
 207      one may allocate 2^[D.ptr_size] blocks of size one byte, or one block of
 208      size 2^[D.ptr_size] bytes. *)
 209
 210   module ValBlock  = BoundedInt
 211   module ValOffset = BoundedInt
 212
 213   type t =
 214     | Val_int of ValInt.t
 215     | Val_ptr of ValBlock.t * ValOffset.t
 216     | Val_undef
 217
 218   let compare a b = match a, b with
 219     | Val_int i1, Val_int i2 -> ValInt.compare i1 i2
 220     | Val_ptr (b1, off1), Val_ptr (b2, off2) ->
 221       let i1 = ValBlock.compare b1 b2 in
 222       if i1 = 0 then ValOffset.compare off1 off2
 223       else i1
 224     | Val_undef, Val_undef -> 0
 225     | Val_int _, _ -> 1
 226     | _, Val_int _ -> -1
 227     | Val_ptr _, _ -> 1
 228     | _, Val_ptr _ -> -1
 229
 230   (*
 231     let hash = function
 232     | Val_int i -> ValInt.to_int i
 233     | Val_float f -> int_of_float f
 234     | Val_undef -> 0
 235     | Val_ptr (b,o)
 236     | Val_ptrh (b,o)
 237     | Val_ptrl (b,o) -> ValInt.to_int (ValInt.add b o)
 238   *)
 239
 240   let hash = Hashtbl.hash
 241
 242   let equal a b = compare a b = 0
 243   let eq a b = compare a b = 0
 244
 245   let to_string = function
 246     | Val_int i -> ValInt.to_string i
 247     | Val_ptr (b, off) ->
 248       "VPtr(" ^ (ValBlock.to_string b) ^ ", " ^ (ValOffset.to_string off) ^ ")"
 249     | Val_undef -> "undef"
 250
 251   let is_int = function
 252     | Val_int _ -> true
 253     | _ -> false
 254
 255   let to_int = function
 256     | Val_int i -> ValInt.to_int i
 257     | _ -> raise (Failure "Value.to_int")
 258
 259   let of_int i = Val_int (ValInt.of_int i)
 260   let one = of_int 1
 261
 262   let of_int_repr i = Val_int i
 263
 264   let to_int_repr = function
 265     | Val_int i -> i
 266     | _ -> raise (Failure "Value.to_int_repr")
 267
 268   let zero      = Val_int ValInt.zero
 269   let val_true  = Val_int ValInt.one
 270   let val_false = Val_int ValInt.zero
 271
 272   let is_true = function
 273     | Val_int i -> ValInt.neq i ValInt.zero
 274     | Val_ptr (b, off) ->
 275       (ValBlock.neq b ValBlock.zero) || (ValOffset.neq off ValOffset.zero)
 276     | _ -> false
 277
 278   let is_false = function
 279     | Val_int i -> ValInt.eq i ValInt.zero
 280     | Val_ptr (b, off) ->
 281       (ValBlock.eq b ValBlock.zero) && (ValOffset.eq off ValOffset.zero)
 282     | _ -> false
 283
 284   let of_bool = function
 285     | true -> val_true
 286     | false -> val_false
 287
 288   let to_bool v =
 289     if is_true v then true
 290     else
 291       if is_false v then false
 292       else error "Undefined value."
 293
 294   let undef = Val_undef
 295
 296   let cast cast_fun = function
 297     | Val_int i -> Val_int (cast_fun i)
 298     | _ -> Val_undef
 299
 300   (** Sign or 0 extensions from various bounded integers. *)
 301   let cast8unsigned = cast (ValInt.zero_ext 8)
 302   let cast8signed = cast (ValInt.sign_ext 8)
 303   let cast16unsigned = cast (ValInt.zero_ext 16)
 304   let cast16signed = cast (ValInt.sign_ext 16)
 305   let cast32 = cast (ValInt.zero_ext 32)
 306
 307
 308   let unary_int_op f = function
 309     | Val_int i -> Val_int (f i)
 310     | _ -> Val_undef
 311
 312   let binary_int_op f v1 v2 = match v1, v2 with
 313     | Val_int i1, Val_int i2 -> Val_int (f i1 i2)
 314     | _ -> Val_undef
 315
 316   let negint = unary_int_op ValInt.neg
 317
 318   let notbool v =
 319     if is_true v then val_false
 320     else
 321       if is_false v then val_true
 322       else Val_undef
 323
 324   let notint = unary_int_op ValInt.lognot
 325
 326   let cmpl = unary_int_op ValInt.lognot
 327
 328   (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
 329       overflows. *)
 330   let add_and_of v1 v2 = match v1, v2 with
 331     | Val_int i1, Val_int i2 ->
 332       (Val_int (ValInt.add i1 i2), of_bool (ValInt.add_of i1 i2))
 333     | Val_int i, Val_ptr (b, off)
 334     | Val_ptr (b, off), Val_int i ->
 335       let i = ValOffset.cast i in
 336       (Val_ptr (b, ValOffset.add off i), of_bool (ValOffset.add_of off i))
 337     | _, _ -> (Val_undef, Val_undef)
 338
 339   let add v1 v2 = fst (add_and_of v1 v2)
 340   let add_of v1 v2 = snd (add_and_of v1 v2)
 341
 342   let succ v = add v (Val_int ValInt.one)
 343
 344   (** [sub_and_uf v1 v2] returns the substraction of [v1] and [v2], and whether
 345       this substraction underflows. *)
 346   let sub_and_uf v1 v2 = match v1, v2 with
 347     | Val_int i1, Val_int i2 ->
 348       (Val_int (ValInt.sub i1 i2), of_bool (ValInt.sub_uf i1 i2))
 349     | Val_ptr (b, off), Val_int i ->
 350       let i = ValOffset.cast i in
 351       (Val_ptr (b, ValOffset.sub off i), of_bool (ValOffset.sub_uf off i))
 352     | Val_ptr (b1, off1), Val_ptr (b2, off2) when ValBlock.eq b1 b2 ->
 353       (Val_int (ValInt.cast (ValOffset.sub off1 off2)),
 354        of_bool (ValOffset.sub_uf off1 off2))
 355     | _, _ -> (Val_undef, Val_undef)
 356
 357   let sub v1 v2 = fst (sub_and_uf v1 v2)
 358   let sub_uf v1 v2 = snd (sub_and_uf v1 v2)
 359
 360   let pred v = sub v (Val_int ValInt.one)
 361
 362   let mul = binary_int_op ValInt.mul
 363
 364   let is_zero = function
 365     | Val_int i when ValInt.eq i ValInt.zero -> true
 366     | _ -> false
 367
 368   let error_if_zero op v1 v2 =
 369     if is_zero v2 then error "Division by zero."
 370     else binary_int_op op v1 v2
 371
 372   let div     = error_if_zero ValInt.div
 373   let divu    = error_if_zero ValInt.divu
 374   let modulo  = error_if_zero ValInt.modulo
 375   let modulou = error_if_zero ValInt.modulou
 376
 377   let and_op = binary_int_op ValInt.logand
 378   let or_op  = binary_int_op ValInt.logor
 379   let xor    = binary_int_op ValInt.logxor
 380   let shl    = binary_int_op ValInt.shl
 381   let shr    = binary_int_op ValInt.shr
 382   let shru   = binary_int_op ValInt.shrl
 383
 384   let ext sh v n m =
 385     let n = n * 8 in
 386     let m = m * 8 in
 387     let real_size = D.int_size * 8 in
 388     let int_sh sh v n = sh v (of_int n) in
 389     if n >= m then
 390       if m = real_size then v
 391       else modulou v (shl one (of_int m))
 392     else
 393       let v = int_sh shl v (real_size - n) in
 394       let v = int_sh sh v (m - n) in
 395       int_sh shru v (real_size - m)
 396
 397   let zero_ext = ext shru
 398   let sign_ext = ext shr
 399
 400   let cmp f_int f_off v1 v2 = match v1, v2 with
 401     | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2)
 402     | Val_ptr (b1, off1), Val_ptr (b2, off2) when ValBlock.eq b1 b2 ->
 403       of_bool (f_off off1 off2)
 404     | _ -> Val_undef
 405
 406   let cmp_eq = cmp ValInt.eq ValOffset.eq
 407   let cmp_ne = cmp ValInt.neq ValOffset.neq
 408   let cmp_lt = cmp ValInt.lt ValOffset.lt
 409   let cmp_ge = cmp ValInt.ge ValOffset.ge
 410   let cmp_le = cmp ValInt.le ValOffset.le
 411   let cmp_gt = cmp ValInt.gt ValOffset.gt
 412
 413   let cmp_eq_u = cmp ValInt.eq ValOffset.eq
 414   let cmp_ne_u = cmp ValInt.neq ValOffset.neq
 415   let cmp_lt_u = cmp ValInt.ltu ValOffset.ltu
 416   let cmp_ge_u = cmp ValInt.geu ValOffset.geu
 417   let cmp_le_u = cmp ValInt.leu ValOffset.leu
 418   let cmp_gt_u = cmp ValInt.gtu ValOffset.gtu
 419
 420
 421   (* The memory is based on byte values. In order to be able to fit a bigger
 422      integer or pointer value in memory, we need to be able to break this value
 423      into several values of size a byte. An integer will be broken into multiple
 424      8 bits integers. A pointer will be broken into several couples of 8 bits
 425      blocks and 8 bits offsets. *)
 426
 427   module Int8 = IntValue.Int8
 428
 429   (* 8 bits integers *)
 430   module IntChunk = Int8
 431   (* 8 bits blocks *)
 432   module BlockChunk = Int8
 433   (* 8 bits offsets *)
 434   module OffsetChunk = Int8
 435
 436   (** A chunk is a part of a value that has the size of a memory cell. *)
 437
 438   type chunk =
 439     | Byte_int of IntChunk.t
 440     | Byte_ptr of BlockChunk.t * OffsetChunk.t
 441     | Byte_undef
 442
 443   let string_of_chunk = function
 444     | Byte_int i -> IntChunk.to_string i
 445     | Byte_ptr (b, off) ->
 446       "BPtr(" ^ (BlockChunk.to_string b) ^ ", " ^
 447       (OffsetChunk.to_string off) ^ ")"
 448     | Byte_undef -> "Bundef"
 449
 450   let undef_byte = Byte_undef
 451
 452   let is_undef_byte = function
 453     | Byte_undef -> true
 454     | _ -> false
 455
 456   let break_and_cast break cast x n =
 457     let ys = break x n in
 458     List.map cast ys
 459
 460   (** [break v] cuts [v] in chunks that each fits into a memory cell. In the
 461       resulting list, the first element is the low bits, and the last is the
 462       high bits (little endian representation). *)
 463   let break v =
 464     let nb_chunks = D.int_size in
 465     match v with
 466       | Val_ptr (b, off) ->
 467         let bbs = break_and_cast ValBlock.break BlockChunk.cast b nb_chunks in
 468         let boffs =
 469           break_and_cast ValOffset.break OffsetChunk.cast off nb_chunks in
 470         List.map2 (fun bb boff -> Byte_ptr (bb, boff)) bbs boffs
 471       | Val_int i ->
 472         let bis = break_and_cast ValInt.break IntChunk.cast i nb_chunks in
 473         List.map (fun i' -> Byte_int i') bis
 474       | _ -> MiscPottier.make Byte_undef nb_chunks
 475
 476   (** [all_are_pointers l] returns [true] iff the values in the list [l] all are
 477       pointers. *)
 478   let all_are_pointers =
 479     let f b v = b && (match v with Byte_ptr _ -> true | _ -> false) in
 480     List.fold_left f true
 481
 482   (** [all_are_integers l] returns [true] iff the values in the list [l] all are
 483       integers. *)
 484   let all_are_integers =
 485     let f b v = b && (match v with Byte_int _ -> true | _ -> false) in
 486     List.fold_left f true
 487
 488   let bblock_of_chunk = function
 489     | Byte_ptr (b, _) -> b
 490     | _ -> assert false (* do not use on this argument *)
 491
 492   let boffset_of_chunk = function
 493     | Byte_ptr (_, off) -> off
 494     | _ -> assert false (* do not use on this argument *)
 495
 496   let bint_of_chunk = function
 497     | Byte_int i -> i
 498     | _ -> assert false (* do not use on this argument *)
 499
 500   let cast_and_merge cast merge transform l =
 501     merge (List.map (fun x -> cast (transform x)) l)
 502
 503   (** [merge l] creates the value where the first element of [l] is its low
 504       bits, etc, and the last element of [l] is its high bits (little endian
 505       representation). *)
 506   let merge = function
 507     | l when all_are_pointers l ->
 508       let b = cast_and_merge ValBlock.cast ValBlock.merge bblock_of_chunk l in
 509       let off =
 510         cast_and_merge ValOffset.cast ValOffset.merge boffset_of_chunk l in
 511       Val_ptr (b, off)
 512     | l when all_are_integers l ->
 513       Val_int (cast_and_merge ValInt.cast ValInt.merge bint_of_chunk l)
 514     | _ -> Val_undef
 515
 516
 517   (** Addresses from the memory point of view. *)
 518
 519   (** Some architectures have pointers bigger than integers. In this case, only
 520       a chunk of pointer can fit into a machine register. Thus, an address is
 521       represented by several values (little endian representation). *)
 522
 523   type address = t list
 524
 525   let string_of_address vs =
 526     "[" ^ (MiscPottier.string_of_list " " to_string vs) ^ "]"
 527
 528
 529   (** Addresses are represented by a block, i.e. a base address, and an offset
 530       from this block. Both blocks and offsets are represented using bounded
 531       integers. *)
 532
 533   let ptr_int_size = max (D.ptr_size / D.int_size) 1
 534
 535   module Block  = IntValue.Make (struct let size = D.ptr_size end)
 536   module Offset = IntValue.Make (struct let size = D.ptr_size end)
 537
 538   type mem_address = Block.t * Offset.t
 539
 540   let string_of_mem_address (b, off) =
 541     Printf.sprintf "(%s, %s)" (Block.to_string b) (Offset.to_string off)
 542
 543   let is_mem_address =
 544     let f b v = b && (match v with | Val_ptr _ -> true | _ -> false) in
 545     List.fold_left f true
 546
 547   let of_mem_address (b, off) =
 548     let bs = Block.break b ptr_int_size in
 549     let offs = Offset.break off ptr_int_size in
 550     let f b off = Val_ptr (ValBlock.cast b, ValOffset.cast off) in
 551     List.map2 f bs offs
 552
 553   let decompose_Val_ptr = function
 554     | Val_ptr (b, off) -> (b, off)
 555     | _ -> error "Not an address."
 556
 557   let to_mem_address vs =
 558     let (bs, offs) = List.split (List.map decompose_Val_ptr vs) in
 559     let b = Block.merge (List.map Block.cast bs) in
 560     let off = Offset.merge (List.map Offset.cast offs) in
 561     (b, off)
 562
 563   let make_mem_address b off = (b, off)
 564   let decompose_mem_address addr = addr
 565   let block_of_address vs = fst (to_mem_address vs)
 566   let offset_of_address vs = snd (to_mem_address vs)
 567
 568   let null = of_mem_address (Block.zero, Offset.zero)
 569
 570   let change_address_offset vs off =
 571     let (b, _) = decompose_mem_address (to_mem_address vs) in
 572     of_mem_address (make_mem_address b off)
 573
 574   let add_address vs off' =
 575     let (b, off) = decompose_mem_address (to_mem_address vs) in
 576     let off = Offset.add off off' in
 577     of_mem_address (make_mem_address b off)
 578
 579   let eq_address addr1 addr2 =
 580     let f b v1 v2 = b && (eq v1 v2) in
 581     List.fold_left2 f true addr1 addr2
 582
 583 end