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

Last change on this file since 1568 was 1568, checked in by tranquil, 8 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
Line 
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
23(** This is the signature of the module that provides types and functions to
24    manipulate values. *)
25
26module type S =
27sig
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 rotl       : t -> t
116  val shr        : t -> t -> t
117  val shru       : t -> t -> t
118
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
127  (** Unsigned comparisions *)
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
134
135  (** A chunk is a part of a value that has the size of a memory cell. *)
136
137  type chunk
138  val string_of_chunk : chunk -> string
139  val undef_byte : chunk
140  val is_undef_byte : chunk -> bool
141
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
150
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
185end
186
187
188module Make (D : DATA_SIZE) =
189struct
190
191  let int_size = D.int_size
192  let ptr_size = D.ptr_size
193
194  (* Integer values. *)
195  module ValInt = IntValue.Make (struct let size = D.int_size end)
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
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). *)
203
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. *)
207
208  module ValBlock  = IntValue.Make (struct let size = D.int_size end)
209  module ValOffset = IntValue.Make (struct let size = D.int_size end)
210
211  type t =
212    | Val_int of ValInt.t
213    | Val_ptr of ValBlock.t * ValOffset.t
214    | Val_undef
215
216  let compare a b = match a, b with
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
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
228  (*
229    let hash = function
230    | Val_int i -> ValInt.to_int i
231    | Val_float f -> int_of_float f
232    | Val_undef -> 0
233    | Val_ptr (b,o)
234    | Val_ptrh (b,o)
235    | Val_ptrl (b,o) -> ValInt.to_int (ValInt.add b o)
236  *)
237
238  let hash = Hashtbl.hash
239
240  let equal a b = compare a b = 0
241  let eq a b = compare a b = 0
242
243  let to_string = function
244    | Val_int i -> ValInt.to_string i
245    | Val_ptr (b, off) ->
246      "VPtr(" ^ (ValBlock.to_string b) ^ ", " ^ (ValOffset.to_string off) ^ ")"
247    | Val_undef -> "undef"
248
249  let is_int = function
250    | Val_int _ -> true
251    | _ -> false
252
253  let to_int = function
254    | Val_int i -> ValInt.to_int i
255    | _ -> raise (Failure "Value.to_int")
256
257  let of_int i = Val_int (ValInt.of_int i)
258  let one = of_int 1
259
260  let of_int_repr i = Val_int i
261
262  let to_int_repr = function
263    | Val_int i -> i
264    | _ -> raise (Failure "Value.to_int_repr")
265
266  let zero      = Val_int ValInt.zero
267  let val_true  = Val_int ValInt.one
268  let val_false = Val_int ValInt.zero
269
270  let is_true = function
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)
274    | _ -> false
275
276  let is_false = function
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)
280    | _ -> false
281
282  let of_bool = function
283    | true -> val_true
284    | false -> val_false
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
298  (** Sign or 0 extensions from various bounded integers. *)
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)
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
314  let negint = unary_int_op ValInt.neg
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
322  let notint = unary_int_op ValInt.lognot
323
324  let cmpl = unary_int_op ValInt.lognot
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 ->
330      (Val_int (ValInt.add i1 i2), of_bool (ValInt.add_of i1 i2))
331    | Val_int i, Val_ptr (b, off)
332    | Val_ptr (b, off), Val_int i ->
333      let i = ValOffset.cast i in
334      (Val_ptr (b, ValOffset.add off i), of_bool (ValOffset.add_of off i))
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
340  let succ v = add v (Val_int ValInt.one)
341
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
345    | Val_int i1, Val_int i2 ->
346      (Val_int (ValInt.sub i1 i2), of_bool (ValInt.sub_uf i1 i2))
347    | Val_ptr (b, off), Val_int i ->
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))
353    | _, _ -> (Val_undef, Val_undef)
354
355  let sub v1 v2 = fst (sub_and_uf v1 v2)
356  let sub_uf v1 v2 = snd (sub_and_uf v1 v2)
357
358  let pred v = sub v (Val_int ValInt.one)
359
360  let mul = binary_int_op ValInt.mul
361
362  let is_zero = function
363    | Val_int i when ValInt.eq i ValInt.zero -> true
364    | _ -> false
365
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
369
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
374
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
379  let rotl   = unary_int_op ValInt.rotl
380  let shr    = binary_int_op ValInt.shr
381  let shru   = binary_int_op ValInt.shrl
382
383  let ext sh v n m =
384    let n = n * 8 in
385    let m = m * 8 in
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)
395
396  let zero_ext = ext shru
397  let sign_ext = ext shr
398
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
404
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
411
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
418
419
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. *)
425
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
432
433  (** A chunk is a part of a value that has the size of a memory cell. *)
434
435  type chunk =
436    | Byte_int of IntChunk.t
437    | Byte_ptr of BlockChunk.t * OffsetChunk.t
438    | Byte_undef
439
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"
446
447  let undef_byte = Byte_undef
448
449  let is_undef_byte = function
450    | Byte_undef -> true
451    | _ -> false
452
453  let break_and_cast break cast x n =
454    let ys = break x n in
455    List.map cast ys
456
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
472
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
478
479  (** [all_are_integers l] returns [true] iff the values in the list [l] all are
480      integers. *)
481  let all_are_integers =
482    let f b v = b && (match v with Byte_int _ -> true | _ -> false) in
483    List.fold_left f true
484
485  let bblock_of_chunk = function
486    | Byte_ptr (b, _) -> b
487    | _ -> assert false (* do not use on this argument *)
488
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). *)
503  let merge = function
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)
511    | _ -> Val_undef
512
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
577end
Note: See TracBrowser for help on using the repository browser.