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

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

Update of D2.2 from Paris.

File size: 16.1 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 underflows. *)
110  val sub_and_uf : 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      underflows, and [0] otherwise. *)
114  val sub_uf     : 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 modulou    : 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 end)
169
170  (* Addresses are represented by a block, i.e. a base address, and an offset
171     from this block. Both blocks and offsets are represented using bounded
172     integers. *)
173
174  (* In 8051, addresses are not the same size as integers: the size of an
175     address (16 bits) is twice that of an integer (8 bits). Thus, blocks and
176     offsets need 16 bits each to be represented. Indeed, one may allocate 2^16
177     blocks of size one byte, or one block of size 2^16 bytes. *)
178
179  module Block =
180    IntValue.Make (struct let size = D.ptr_size end)
181  module Offset = (* Block *)
182    IntValue.Make (struct let size = D.ptr_size end)
183
184  (* We want to be able to put an address into registers, and we want to be able
185     to restore an address given values from several registers. We provide a
186     function that breaks an address into multiple parts (two parts for the
187     8051), where each part fits into a register. But an address is formed with
188     two 16 bits values (the block and the offset), so we cannot break it into
189     two parts that are each represented by an integer: we need to keep the
190     information of the block and the offset. This is the purpose of the
191     Val_ptrh (the high bits of an address) and Val_ptrl (the low bits of an
192     address) constructors. *)
193
194  type t =
195    | Val_int of Int.t
196    | Val_float of float
197    | Val_ptr of Block.t * Offset.t
198    | Val_ptrh of Block.t * Offset.t
199    | Val_ptrl of Block.t * Offset.t
200    | Val_undef
201
202  let compare a b = match a, b with
203    | Val_int i1, Val_int i2 -> Int.compare i1 i2
204    | Val_float f1, Val_float f2 -> compare f1 f2
205    | Val_ptr (b1, off1), Val_ptr (b2, off2)
206    | Val_ptrh (b1, off1), Val_ptrh (b2, off2)
207    | Val_ptrl (b1, off1), Val_ptrl (b2, off2) ->
208      let i1 = Block.compare b1 b2 in
209      if i1 = 0 then Offset.compare off1 off2
210      else i1
211    | Val_undef, Val_undef -> 0
212    | Val_int _, _ -> 1
213    | _, Val_int _ -> -1
214    | Val_float _, _ -> 1
215    | _, Val_float _ -> -1
216    | Val_ptr _, _ -> 1
217    | _, Val_ptr _ -> -1
218    | Val_ptrh _, _ -> 1
219    | _, Val_ptrh _ -> -1
220    | Val_ptrl _, _ -> 1
221    | _, Val_ptrl _ -> -1
222
223(*
224  let hash = function
225    | Val_int i -> Int.to_int i
226    | Val_float f -> int_of_float f
227    | Val_undef -> 0
228    | Val_ptr (b,o)
229    | Val_ptrh (b,o)
230    | Val_ptrl (b,o) -> Int.to_int (Int.add b o)
231*)
232
233  let hash = Hashtbl.hash
234
235  let equal a b = compare a b = 0
236  let eq a b = compare a b = 0
237
238  let to_string = function
239    | Val_int i -> Int.to_string i
240    | Val_float f -> string_of_float f
241    | Val_ptr (b, off) ->
242      "Ptr(" ^ (Block.to_string b) ^ ", " ^ (Offset.to_string off) ^ ")"
243    | Val_ptrh (b, off) ->
244      "PtrH(" ^ (Block.to_string b) ^ ", " ^ (Offset.to_string off) ^ ")"
245    | Val_ptrl (b, off) ->
246      "PtrL(" ^ (Block.to_string b) ^ ", " ^ (Offset.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 -> Int.to_int i
255    | _ -> raise (Failure "Value.to_int")
256
257  let of_int i = Val_int (Int.of_int i)
258
259  let to_int_repr = function
260    | Val_int i -> i
261    | _ -> raise (Failure "Value.to_int_repr")
262
263  let of_int_repr i = Val_int i
264
265  let is_pointer = function
266    | Val_ptr _ -> true
267    | _ -> false
268
269  let to_pointer = function
270    | Val_ptr (b, off) -> (b, off)
271    | _ -> raise (Failure "Value.to_pointer")
272
273  let of_pointer (b, off) = Val_ptr (b, off)
274
275  let is_float = function
276    | Val_float _ -> true
277    | _ -> false
278
279  let to_float = function
280    | Val_float f -> f
281    | _ -> raise (Failure "Value.to_float")
282
283  let of_float f = Val_float f
284
285  let zero = Val_int Int.zero
286
287  let val_true = Val_int Int.one
288
289  let val_false  = Val_int Int.zero
290
291  let is_true = function
292    | Val_int i -> Int.neq i Int.zero
293    | Val_ptr _ | Val_ptrh _ | Val_ptrl _ -> true
294    | _ -> false
295
296  let is_false = function
297    | Val_int i -> Int.eq i Int.zero
298    | _ -> false
299
300  let of_bool = function
301    | true -> Val_int Int.one
302    | false -> Val_int Int.zero
303
304  let to_bool v =
305    if is_true v then true
306    else
307      if is_false v then false
308      else error "Undefined value."
309
310  let undef = Val_undef
311
312  let cast cast_fun = function
313    | Val_int i -> Val_int (cast_fun i)
314    | _ -> Val_undef
315
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)
322
323
324  let unary_int_op f = function
325    | Val_int i -> Val_int (f i)
326    | _ -> Val_undef
327
328  let binary_int_op f v1 v2 = match v1, v2 with
329    | Val_int i1, Val_int i2 -> Val_int (f i1 i2)
330    | _ -> Val_undef
331
332  let unary_float_op f = function
333    | Val_float i -> Val_float (f i)
334    | _ -> Val_undef
335
336  let binary_float_op f v1 v2 = match v1, v2 with
337    | Val_float i1, Val_float i2 -> Val_float (f i1 i2)
338    | _ -> Val_undef
339
340  let binary_float_cmp f v1 v2 = match v1, v2 with
341    | Val_float i1, Val_float i2 -> of_bool (f i1 i2)
342    | _ -> Val_undef
343
344
345  let negint = unary_int_op Int.neg
346
347  let notbool v =
348    if is_true v then val_false
349    else
350      if is_false v then val_true
351      else Val_undef
352
353  let andbool v1 v2 =
354    if is_true v1 && is_true v2 then val_true
355    else
356      if (is_true v1 && is_false v2) ||
357        (is_false v1 && is_true v2) ||
358        (is_false v1 && is_false v2) then val_false
359      else Val_undef
360
361  let orbool v1 v2 =
362    if (is_true v1 && is_true v2) ||
363      (is_true v1 && is_false v2) ||
364      (is_false v1 && is_true v2) then val_true
365    else
366      if is_false v1 && is_false v2 then val_false
367      else Val_undef
368
369  let notint = unary_int_op Int.lognot
370
371  let negf = unary_float_op (fun f -> -.f)
372
373  let absf = unary_float_op abs_float
374
375  let singleoffloat _ = assert false (* TODO *)
376
377  let intoffloat = function
378    | Val_float f -> Val_int (Int.of_int (int_of_float f))
379    | _ -> Val_undef
380
381  let intuoffloat _ = assert false (* TODO *)
382
383  let floatofint = function
384    | Val_int i -> Val_float (float_of_int (Int.to_int i))
385    | _ -> Val_undef
386
387  let floatofintu _ = assert false (* TODO *)
388
389  (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
390      overflows. *)
391  let add_and_of v1 v2 = match v1, v2 with
392    | Val_int i1, Val_int i2 ->
393      (Val_int (Int.add i1 i2), of_bool (Int.add_of i1 i2))
394    | Val_int i, Val_ptr (b, off)
395    | Val_ptr (b, off), Val_int i ->
396      (Val_ptr (b, Offset.add off i),
397       of_bool (Offset.add_of off (Offset.cast i)))
398    | Val_int i, Val_ptrh (b, off)
399    | Val_ptrh (b, off), Val_int i ->
400      (Val_ptrh (b, Offset.add off i),
401       of_bool (Offset.add_of off (Offset.cast i)))
402    | Val_int i, Val_ptrl (b, off)
403    | Val_ptrl (b, off), Val_int i ->
404      (Val_ptrl (b, Offset.add off i),
405       of_bool (Offset.add_of off (Offset.cast i)))
406    | _, _ -> (Val_undef, Val_undef)
407
408  let add v1 v2 = fst (add_and_of v1 v2)
409  let add_of v1 v2 = snd (add_and_of v1 v2)
410
411  let succ v = add v (Val_int Int.one)
412
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
416    | Val_int i1, Val_int i2 ->
417      (Val_int (Int.sub i1 i2), of_bool (Int.sub_uf i1 i2))
418    | Val_ptr (b, off), Val_int i ->
419      (Val_ptr (b, Offset.sub off i),
420       of_bool (Offset.sub_uf off (Offset.cast i)))
421    | Val_ptrh (b, off), Val_int i ->
422      (Val_ptrh (b, Offset.sub off i),
423       of_bool (Offset.sub_uf off (Offset.cast i)))
424    | Val_ptrl (b, off), Val_int i ->
425      (Val_ptrl (b, Offset.sub off i),
426       of_bool (Offset.sub_uf off (Offset.cast i)))
427    | Val_ptr (b1, off1), Val_ptr (b2, off2)
428    | Val_ptrh (b1, off1), Val_ptrh (b2, off2)
429    | Val_ptrl (b1, off1), Val_ptrl (b2, off2) when Block.eq b1 b2 ->
430      (Val_int (Int.cast (Offset.sub off1 off2)),
431       of_bool (Offset.sub_uf off1 off2))
432    | _, _ -> (Val_undef, Val_undef)
433
434  let sub v1 v2 = fst (sub_and_uf v1 v2)
435  let sub_uf v1 v2 = snd (sub_and_uf v1 v2)
436
437  let pred v = sub v (Val_int Int.one)
438
439  let cmpl = unary_int_op Int.lognot
440
441  let mul = binary_int_op Int.mul
442
443  let is_zero = function
444    | Val_int i when Int.eq i Int.zero -> true
445    | _ -> false
446
447  let div v1 v2 =
448    if is_zero v2 then Val_undef
449    else binary_int_op Int.div v1 v2
450
451  let divu v1 v2 =
452    if is_zero v2 then Val_undef
453    else binary_int_op Int.divu v1 v2
454
455  let modulo v1 v2 =
456    if is_zero v2 then Val_undef
457    else binary_int_op Int.modulo v1 v2
458
459  let modulou v1 v2 =
460    if is_zero v2 then Val_undef
461    else binary_int_op Int.modulou v1 v2
462
463  let and_op = binary_int_op Int.logand
464
465  let or_op = binary_int_op Int.logor
466
467  let xor = binary_int_op Int.logxor
468
469  let shl = binary_int_op Int.shl
470
471  let shr = binary_int_op Int.shr
472
473  let shru = binary_int_op Int.shrl
474
475  let addf = binary_float_op (+.)
476
477  let subf = binary_float_op (-.)
478
479  let mulf = binary_float_op ( *. )
480
481  let divf v1 v2 = match v2 with
482    | Val_float f2 when f2 <> 0. -> binary_float_op (/.) v1 v2
483    | _ -> Val_undef
484
485  let cmp f_int f_ptr v1 v2 = match v1, v2 with
486    | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2)
487    | Val_ptr (b1, off1), Val_ptr (b2, off2)
488    | Val_ptrh (b1, off1), Val_ptrh (b2, off2)
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
506
507  let cmp_eq_f = binary_float_cmp (=)
508  let cmp_ne_f = binary_float_cmp (<>)
509  let cmp_lt_f = binary_float_cmp (<)
510  let cmp_ge_f = binary_float_cmp (>=)
511  let cmp_le_f = binary_float_cmp (<=)
512  let cmp_gt_f = binary_float_cmp (>)
513
514  (** [break v n] cuts [v] in [n] parts. In the resulting list, the first
515      element is the high bits, and the last is the low bits. *)
516  let break v n = match v with
517    (* Parameter [n] is used to generalize the concept of breaking a value into
518       multiple parts. But for now, we only break values in exactly two
519       parts. *)
520    | Val_ptr (b, off) ->
521      begin match Offset.break off 2 with
522        | [off1 ; off2] -> [Val_ptrh (b, off1) ; Val_ptrl (b, off2)]
523        | _ -> assert false (* should be impossible *) end
524    | Val_int i -> List.map (fun i' -> Val_int i') (Int.break i n)
525    | v when n = 1 -> [v]
526    | _ -> MiscPottier.make Val_undef n
527
528  (** [all_are_integers l] returns [true] iff all the values in the list [l] are
529      integers. *)
530  let all_are_integers =
531    let f b v = b && (match v with Val_int _ -> true | _ -> false) in
532    List.fold_left f true
533
534  (** [integers l] supposes that [l] is a list of integer values. It the returns
535      the (list of) integers. *)
536  let integers =
537    List.map (function
538      | Val_int i -> i
539      | _ -> assert false (* should be impossible *))
540
541  (** [merge l] creates the value where the first element of [l] is its
542      high bits, etc, and the last element of [l] is its low bits. *)
543  let merge = function
544    | [v] -> v
545    | [Val_ptrh (b1, off1) ; Val_ptrl (b2, off2)] when Block.eq b1 b2 ->
546      let off = Offset.merge [off1 ; off2] in
547      Val_ptr (b1, off)
548    | l when all_are_integers l -> Val_int (Int.merge (integers l))
549    | _ -> Val_undef
550
551end
Note: See TracBrowser for help on using the repository browser.