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

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 17.5 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 functions and types to
24    manipulate values. *)
25
26module type S =
27sig
28
29  (** Addresses are represented by a block, i.e. a base address, and an offset
30      from this block. Both blocks and offsets are represented using bounded
31      integers. *)
32  module Block  : IntValue.S
33  module Offset : IntValue.S
34
35  (** The type of values. A value may be: a bounded integer, a float (though
36      they are not fully supported), an address, or undefined. *)
37  type t
38
39  val compare : t -> t -> int
40  val equal : t -> t -> bool
41  val eq : t -> t -> bool
42  val hash : t -> int
43  val to_string : t -> string
44
45  (* The functions of this module may raise a Failure exception when
46     trying to convert them to their various representation. *)
47
48  val is_int : t -> bool
49  val to_int : t -> int
50  val of_int : int -> t
51
52  val is_float : t -> bool
53  val to_float : t -> float
54  val of_float : float -> t
55
56  val to_int_repr : t -> IntValue.int_repr
57  val of_int_repr : IntValue.int_repr -> t
58
59  val is_pointer : t -> bool
60  val to_pointer : t -> Block.t * Offset.t
61  val of_pointer : Block.t * Offset.t -> t
62
63  val of_bool   : bool -> t
64  val to_bool   : t -> bool
65
66  val zero      : t
67  val val_true  : t
68  val val_false : t
69  val is_true   : t -> bool
70  val is_false  : t -> bool
71  val undef     : t
72
73  (** [cast8unsigned v] returns undefined for non-integer values. For integer
74      values, it supposes that the value is a 8 bit unsigned integer. It will
75      return the integer value that represents the same quantity, but using
76      every bits. The other cast operations behave the same way. *)
77  val cast8unsigned  : t -> t
78  val cast8signed    : t -> t   
79  val cast16unsigned : t -> t
80  val cast16signed   : t -> t
81  val cast32         : t -> t
82
83  (** Integer opposite *)
84  val negint        : t -> t
85  (** Boolean negation *)
86  val notbool       : t -> t
87  (** Bitwise not *)
88  val notint        : t -> t         
89  val negf          : t -> t           
90  val absf          : t -> t           
91  val singleoffloat : t -> t 
92  val intoffloat    : t -> t     
93  val intuoffloat   : t -> t   
94  val floatofint    : t -> t     
95  val floatofintu   : t -> t   
96
97  val succ       : t -> t
98  val pred       : t -> t
99  val cmpl       : t -> t
100
101  (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
102      overflows. *)
103  val add_and_of : t -> t -> (t * t)
104  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. *)
107  val add_of     : t -> t -> t
108  (** [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)
111  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
115  val mul        : t -> t -> t
116  val div        : t -> t -> t
117  val divu       : t -> t -> t
118  val modulo     : t -> t -> t
119  val modu       : t -> t -> t
120  val and_op     : t -> t -> t
121  val or_op      : t -> t -> t
122  val xor        : t -> t -> t
123  val shl        : t -> t -> t
124  val shr        : t -> t -> t
125  val shru       : t -> t -> t
126  val addf       : t -> t -> t
127  val subf       : t -> t -> t
128  val mulf       : t -> t -> t
129  val divf       : t -> t -> t
130
131  (** Unsigned comparisions *)
132  val cmp_eq_u : t -> t -> t 
133  val cmp_ne_u : t -> t -> t 
134  val cmp_lt_u : t -> t -> t 
135  val cmp_ge_u : t -> t -> t 
136  val cmp_le_u : t -> t -> t 
137  val cmp_gt_u : t -> t -> t 
138
139  val cmp_eq_f : t -> t -> t 
140  val cmp_ne_f : t -> t -> t 
141  val cmp_lt_f : t -> t -> t 
142  val cmp_ge_f : t -> t -> t 
143  val cmp_le_f : t -> t -> t 
144  val cmp_gt_f : t -> t -> t
145
146  val cmp_eq : t -> t -> t 
147  val cmp_ne : t -> t -> t 
148  val cmp_lt : t -> t -> t 
149  val cmp_ge : t -> t -> t 
150  val cmp_le : t -> t -> t 
151  val cmp_gt : t -> t -> t
152
153  (** [break v n] cuts [v] in [n] parts. In the resulting list, the first
154      element is the high bits, and the last is the low bits. *)
155  val break : t -> int -> t list
156  (** [merge l] creates the value where the first element of [l] is its
157      high bits, etc, and the last element of [l] is its low bits. *)
158  val merge : t list -> t
159
160end
161
162
163module Make (D : DATA_SIZE) =
164struct
165
166  (* This module will be used to represent integer values. *)
167  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)
174
175  (* Addresses are represented by a block, i.e. a base address, and an offset
176     from this block. Both blocks and offsets are represented using bounded
177     integers. *)
178
179  (* In 8051, addresses are not the same size as integers: the size of an
180     address (16 bits) is twice that of an integer (8 bits). Thus, blocks and
181     offsets need 16 bits each to be represented. Indeed, one may allocate 2^16
182     blocks of size one byte, or one block of size 2^16 bytes. *)
183
184  module Block =
185    IntValue.Make (struct let size = D.ptr_size let is_signed = true end)
186  module Offset = (* Block *)
187    IntValue.Make (struct let size = D.ptr_size let is_signed = true end)
188
189  (* We want to be able to put an address into registers, and we want to be able
190     to restore an address given values from several registers. We provide a
191     function that breaks an address into multiple parts (two parts for the
192     8051), where each part fits into a register. But an address is formed with
193     two 16 bits values (the block and the offset), so we cannot break it into
194     two parts that are each represented by an integer: we need to keep the
195     information of the block and the offset. This is the purpose of the
196     Val_ptrh (the high bits of an address) and Val_ptrl (the low bits of an
197     address) constructors. *)
198
199  type t =
200    | Val_int of Int.t
201    | Val_float of float
202    | Val_ptr of Block.t * Offset.t
203    | Val_ptrh of Block.t * Offset.t
204    | Val_ptrl of Block.t * Offset.t
205    | Val_undef
206
207  let compare a b = match a, b with
208    | Val_int i1, Val_int i2 -> Int.compare i1 i2
209    | Val_float f1, Val_float f2 -> compare f1 f2
210    | Val_ptr (b1, off1), Val_ptr (b2, off2)
211    | Val_ptrh (b1, off1), Val_ptrh (b2, off2)
212    | Val_ptrl (b1, off1), Val_ptrl (b2, off2) ->
213      let i1 = Block.compare b1 b2 in
214      if i1 = 0 then Offset.compare off1 off2
215      else i1
216    | Val_undef, Val_undef -> 0
217    | Val_int _, _ -> 1
218    | _, Val_int _ -> -1
219    | Val_float _, _ -> 1
220    | _, Val_float _ -> -1
221    | Val_ptr _, _ -> 1
222    | _, Val_ptr _ -> -1
223    | Val_ptrh _, _ -> 1
224    | _, Val_ptrh _ -> -1
225    | Val_ptrl _, _ -> 1
226    | _, Val_ptrl _ -> -1
227
228  let hash = function 
229    | Val_int i -> Int.to_int i
230    | Val_float f -> int_of_float f
231    | Val_undef -> 0
232    | Val_ptr (b,o)
233    | Val_ptrh (b,o)
234    | Val_ptrl (b,o) -> Integer.to_int (Integer.add b o)
235
236  let equal a b = compare a b = 0
237  let eq a b = compare a b = 0
238
239  let to_string = function
240    | Val_int i -> Int.to_string i
241    | Val_float f -> string_of_float f
242    | Val_ptr (b, off) ->
243      "Ptr(" ^ (Block.to_string b) ^ ", " ^ (Offset.to_string off) ^ ")"
244    | Val_ptrh (b, off) ->
245      "PtrH(" ^ (Block.to_string b) ^ ", " ^ (Offset.to_string off) ^ ")"
246    | Val_ptrl (b, off) ->
247      "PtrL(" ^ (Block.to_string b) ^ ", " ^ (Offset.to_string off) ^ ")"
248    | Val_undef -> "undef"
249
250  let is_int = function
251    | Val_int _ -> true
252    | _ -> false
253
254  let to_int = function
255    | Val_int i -> Int.to_int i
256    | _ -> raise (Failure "Value.to_int")
257
258  let of_int i = Val_int (Int.of_int i)
259
260  let to_int_repr = function
261    | Val_int i -> i
262    | _ -> raise (Failure "Value.to_int_repr")
263
264  let of_int_repr i = Val_int i
265
266  let is_pointer = function
267    | Val_ptr _ -> true
268    | _ -> false
269
270  let to_pointer = function
271    | Val_ptr (b, off) -> (b, off)
272    | _ -> raise (Failure "Value.to_pointer")
273
274  let of_pointer (b, off) = Val_ptr (b, off)
275
276  let is_float = function
277    | Val_float _ -> true
278    | _ -> false
279
280  let to_float = function
281    | Val_float f -> f
282    | _ -> raise (Failure "Value.to_float")
283
284  let of_float f = Val_float f
285
286  let zero = Val_int Int.zero
287
288  let val_true = Val_int Int.one
289
290  let val_false  = Val_int Int.zero
291
292  let is_true = function
293    | Val_int i -> Int.neq i Int.zero
294    | Val_ptr _ | Val_ptrh _ | Val_ptrl _ -> true
295    | _ -> false
296
297  let is_false = function
298    | Val_int i -> Int.eq i Int.zero
299    | _ -> false
300
301  let of_bool = function
302    | true -> Val_int Int.one
303    | false -> Val_int Int.zero
304
305  let to_bool v =
306    if is_true v then true
307    else
308      if is_false v then false
309      else error "Undefined value."
310
311  let undef = Val_undef
312
313  let cast cast_fun = function
314    | Val_int i -> Val_int (cast_fun i)
315    | _ -> Val_undef
316
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
328
329
330  let unary_int_op f = function
331    | Val_int i -> Val_int (f i)
332    | _ -> Val_undef
333
334  let binary_int_op f v1 v2 = match v1, v2 with
335    | Val_int i1, Val_int i2 -> Val_int (f i1 i2)
336    | _ -> 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
351
352  let unary_float_op f = function
353    | Val_float i -> Val_float (f i)
354    | _ -> Val_undef
355
356  let binary_float_op f v1 v2 = match v1, v2 with
357    | Val_float i1, Val_float i2 -> Val_float (f i1 i2)
358    | _ -> Val_undef
359
360  let binary_float_cmp f v1 v2 = match v1, v2 with
361    | Val_float i1, Val_float i2 -> of_bool (f i1 i2)
362    | _ -> Val_undef
363
364
365  let negint = unary_int_op Int.neg
366
367  let notbool v =
368    if is_true v then val_false
369    else
370      if is_false v then val_true
371      else Val_undef
372
373  let andbool v1 v2 =
374    if is_true v1 && is_true v2 then val_true
375    else
376      if (is_true v1 && is_false v2) ||
377        (is_false v1 && is_true v2) ||
378        (is_false v1 && is_false v2) then val_false
379      else Val_undef
380
381  let orbool v1 v2 =
382    if (is_true v1 && is_true v2) ||
383      (is_true v1 && is_false v2) ||
384      (is_false v1 && is_true v2) then val_true
385    else
386      if is_false v1 && is_false v2 then val_false
387      else Val_undef
388
389  let notint = unary_int_op Int.lognot
390
391  let negf = unary_float_op (fun f -> -.f)
392
393  let absf = unary_float_op abs_float
394
395  let singleoffloat _ = assert false (* TODO *)
396
397  let intoffloat = function
398    | Val_float f -> Val_int (Int.of_int (int_of_float f))
399    | _ -> Val_undef
400
401  let intuoffloat _ = assert false (* TODO *)
402
403  let floatofint = function
404    | Val_int i -> Val_float (float_of_int (Int.to_int i))
405    | _ -> Val_undef
406
407  let floatofintu _ = assert false (* TODO *)
408
409  (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
410      overflows. *)
411  let add_and_of v1 v2 = match v1, v2 with
412    | Val_int i1, Val_int i2 ->
413      (Val_int (Int.add i1 i2), of_bool (Int.add_of i1 i2))
414    | Val_int i, Val_ptr (b, off)
415    | Val_ptr (b, off), Val_int i ->
416      (Val_ptr (b, Offset.add off i),
417       of_bool (Offset.add_of off (Offset.cast i)))
418    | Val_int i, Val_ptrh (b, off)
419    | Val_ptrh (b, off), Val_int i ->
420      (Val_ptrh (b, Offset.add off i),
421       of_bool (Offset.add_of off (Offset.cast i)))
422    | Val_int i, Val_ptrl (b, off)
423    | Val_ptrl (b, off), Val_int i ->
424      (Val_ptrl (b, Offset.add off i),
425       of_bool (Offset.add_of off (Offset.cast i)))
426    | _, _ -> (Val_undef, Val_undef)
427
428  let add v1 v2 = fst (add_and_of v1 v2)
429  let add_of v1 v2 = snd (add_and_of v1 v2)
430
431  let succ v = add v (Val_int Int.one)
432
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
436    | Val_int i1, Val_int i2 ->
437      (Val_int (Int.sub i1 i2), of_bool (Int.sub_of i1 i2))
438    | Val_ptr (b, off), Val_int i ->
439      (Val_ptr (b, Offset.sub off i),
440       of_bool (Offset.sub_of off (Offset.cast i)))
441    | Val_ptrh (b, off), Val_int i ->
442      (Val_ptrh (b, Offset.sub off i),
443       of_bool (Offset.sub_of off (Offset.cast i)))
444    | Val_ptrl (b, off), Val_int i ->
445      (Val_ptrl (b, Offset.sub off i),
446       of_bool (Offset.sub_of off (Offset.cast i)))
447    | Val_ptr (b1, off1), Val_ptr (b2, off2)
448    | Val_ptrh (b1, off1), Val_ptrh (b2, off2)
449    | Val_ptrl (b1, off1), Val_ptrl (b2, off2) when Block.eq b1 b2 ->
450      (Val_int (Int.cast (Offset.sub off1 off2)),
451       of_bool (Offset.sub_of off1 off2))
452    | _, _ -> (Val_undef, Val_undef)
453
454  let sub v1 v2 = fst (sub_and_of v1 v2)
455  let sub_of v1 v2 = snd (sub_and_of v1 v2)
456
457  let pred v = sub v (Val_int Int.one)
458
459  let cmpl = unary_int_op Int.lognot
460
461  let mul = binary_int_op Int.mul
462
463  let is_zero = function
464    | Val_int i when Int.eq i Int.zero -> true
465    | _ -> false
466
467  let div v1 v2 =
468    if is_zero v2 then Val_undef
469    else binary_int_op Int.div v1 v2
470
471  let divu v1 v2 =
472    if is_zero v2 then Val_undef
473    else binary_intu_op Intu.div v1 v2
474
475  let modulo v1 v2 =
476    if is_zero v2 then Val_undef
477    else binary_int_op Int.modulo v1 v2
478
479  let modu v1 v2 =
480    if is_zero v2 then Val_undef
481    else binary_intu_op Intu.modulo v1 v2
482
483  let and_op = binary_int_op Int.logand
484
485  let or_op = binary_int_op Int.logor
486
487  let xor = binary_int_op Int.logxor
488
489  let shl = binary_int_op Int.shl
490
491  let shr = binary_int_op Int.shr
492
493  let shru = binary_int_op Int.shrl
494
495  let addf = binary_float_op (+.)
496
497  let subf = binary_float_op (-.)
498
499  let mulf = binary_float_op ( *. )
500
501  let divf v1 v2 = match v2 with
502    | Val_float f2 when f2 <> 0. -> binary_float_op (/.) v1 v2
503    | _ -> Val_undef
504
505  let cmpp_eq f_int v1 v2 = match v1, v2 with
506    | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2)
507    | Val_ptr (b1, off1), Val_ptr (b2, off2)
508    | 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
541
542  let cmp_eq_f = binary_float_cmp (=)
543  let cmp_ne_f = binary_float_cmp (<>)
544  let cmp_lt_f = binary_float_cmp (<)
545  let cmp_ge_f = binary_float_cmp (>=)
546  let cmp_le_f = binary_float_cmp (<=)
547  let cmp_gt_f = binary_float_cmp (>)
548
549  (** [break v n] cuts [v] in [n] parts. In the resulting list, the first
550      element is the high bits, and the last is the low bits. *)
551  let break v n = match v with
552    (* Parameter [n] is used to generalize the concept of breaking a value into
553       multiple parts. But for now, we only break values in exactly two
554       parts. *)
555    | Val_ptr (b, off) ->
556      begin match Offset.break off 2 with
557        | [off1 ; off2] -> [Val_ptrh (b, off1) ; Val_ptrl (b, off2)]
558        | _ -> assert false (* should be impossible *) end
559    | Val_int i -> List.map (fun i' -> Val_int i') (Int.break i n)
560    | v when n = 1 -> [v]
561    | _ -> MiscPottier.make Val_undef n
562
563  (** [all_are_integers l] returns [true] iff all the values in the list [l] are
564      integers. *)
565  let all_are_integers =
566    let f b v = b && (match v with Val_int _ -> true | _ -> false) in
567    List.fold_left f true
568
569  (** [integers l] supposes that [l] is a list of integer values. It the returns
570      the (list of) integers. *)
571  let integers =
572    List.map (function
573      | Val_int i -> i
574      | _ -> assert false (* should be impossible *))
575
576  (** [merge l] creates the value where the first element of [l] is its
577      high bits, etc, and the last element of [l] is its low bits. *)
578  let merge = function
579    | [v] -> v
580    | [Val_ptrh (b1, off1) ; Val_ptrl (b2, off2)] when Block.eq b1 b2 ->
581      let off = Offset.merge [off1 ; off2] in
582      Val_ptr (b1, off)
583    | l when all_are_integers l -> Val_int (Int.merge (integers l))
584    | _ -> Val_undef
585
586end
Note: See TracBrowser for help on using the repository browser.