source: Deliverables/D2.2/8051/src/common/value.ml @ 1568

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