source: Deliverables/D2.3/8051/src/common/value.ml @ 453

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

Import of the Paris's sources.

File size: 15.4 KB
Line 
1
2(** This module describes the values manipulated by high level languages. *)
3
4
5let error_prefix = "Value"
6let error s = Error.global_error error_prefix s
7
8
9open IntValue
10
11
12module type DATA_SIZE =
13sig
14  val int_size : int
15  val ptr_size : int
16end
17
18
19module type S =
20sig
21
22  module Block  : IntValue.S
23  module Offset : IntValue.S
24  type t
25
26  val compare : t -> t -> int
27  val equal : t -> t -> bool
28  val eq : t -> t -> bool
29  val hash : t -> int
30  val to_string : t -> string
31
32  (* The functions of this module may raise a Failure exception when
33     trying to convert them to their various representation. *)
34
35  val is_int : t -> bool
36  val to_int : t -> int
37  val of_int : int -> t
38
39  val is_float : t -> bool
40  val to_float : t -> float
41  val of_float : float -> t
42
43  val to_int_repr : t -> IntValue.int_repr
44  val of_int_repr : IntValue.int_repr -> t
45
46  val is_pointer : t -> bool
47  val to_pointer : t -> Block.t * Offset.t
48  val of_pointer : Block.t * Offset.t -> t
49
50  val of_bool   : bool -> t
51  val to_bool   : t -> bool
52
53  val zero      : t
54  val val_true  : t
55  val val_false : t
56  val is_true   : t -> bool
57  val is_false  : t -> bool
58  val undef     : t
59
60  val cast8unsigned  : t -> t
61  val cast8signed    : t -> t   
62  val cast16unsigned : t -> t
63  val cast16signed   : t -> t   
64  val cast32         : t -> t
65
66  val negint        : t -> t         
67  val notbool       : t -> t       
68  val notint        : t -> t         
69  val negf          : t -> t           
70  val absf          : t -> t           
71  val singleoffloat : t -> t 
72  val intoffloat    : t -> t     
73  val intuoffloat   : t -> t   
74  val floatofint    : t -> t     
75  val floatofintu   : t -> t   
76
77  val succ       : t -> t
78  val pred       : t -> t
79  val cmpl       : t -> t
80  val add_and_of : t -> t -> (t * t)
81  val add        : t -> t -> t
82  val add_of     : t -> t -> t
83  val sub_and_uf : t -> t -> (t * t)
84  val sub        : t -> t -> t
85  val sub_uf     : t -> t -> t
86  val mul        : t -> t -> t
87  val div        : t -> t -> t
88  val divu       : t -> t -> t
89  val modulo     : t -> t -> t
90  val modu       : t -> t -> t
91  val and_op     : t -> t -> t
92  val or_op      : t -> t -> t
93  val xor        : t -> t -> t
94  val shl        : t -> t -> t
95  val shr        : t -> t -> t
96  val shru       : t -> t -> t
97  val addf       : t -> t -> t
98  val subf       : t -> t -> t
99  val mulf       : t -> t -> t
100  val divf       : t -> t -> t
101
102  val cmp_eq_u : t -> t -> t 
103  val cmp_ne_u : t -> t -> t 
104  val cmp_lt_u : t -> t -> t 
105  val cmp_ge_u : t -> t -> t 
106  val cmp_le_u : t -> t -> t 
107  val cmp_gt_u : t -> t -> t 
108
109  val cmp_eq_f : t -> t -> t 
110  val cmp_ne_f : t -> t -> t 
111  val cmp_lt_f : t -> t -> t 
112  val cmp_ge_f : t -> t -> t 
113  val cmp_le_f : t -> t -> t 
114  val cmp_gt_f : t -> t -> t
115
116  val cmp_eq : t -> t -> t 
117  val cmp_ne : t -> t -> t 
118  val cmp_lt : t -> t -> t 
119  val cmp_ge : t -> t -> t 
120  val cmp_le : t -> t -> t 
121  val cmp_gt : t -> t -> t
122
123  val break : t -> int -> t list
124  val merge : t list -> t
125
126end
127
128
129module Make (D : DATA_SIZE) =
130struct
131
132  module Int =
133    IntValue.Make (struct let size = D.int_size let is_signed = true end)
134
135  module Intu =
136    IntValue.Make (struct let size = D.int_size let is_signed = false end)
137
138  module Block =
139    IntValue.Make (struct let size = D.ptr_size let is_signed = true end)
140  module Offset = (* Block *)
141    IntValue.Make (struct let size = D.ptr_size let is_signed = true end)
142  module Shift =
143    IntValue.Make (struct let size = D.ptr_size/2 let is_signed = true end)
144
145  type t =
146    | Val_int of Int.t
147    | Val_float of float
148    | Val_ptr of Block.t * Offset.t
149    | Val_ptrh of Block.t * Offset.t * Shift.t
150    | Val_ptrl of Block.t * Offset.t * Shift.t
151    | Val_undef
152
153  let compare a b = match a, b with
154    | Val_int i1, Val_int i2 -> Int.compare i1 i2
155    | Val_float f1, Val_float f2 -> compare f1 f2
156    | Val_ptr (b1, off1), Val_ptr (b2, off2) ->
157      let i1 = Block.compare b1 b2 in
158      if i1 = 0 then Offset.compare off1 off2
159      else i1
160    | Val_ptrh (b1, off1, shift1), Val_ptrh (b2, off2, shift2)
161    | Val_ptrl (b1, off1, shift1), Val_ptrl (b2, off2, shift2) ->
162      let i1 = Block.compare b1 b2 in
163      if i1 = 0 then
164        let i2 = Offset.compare off1 off2 in
165        if i2 = 0 then Shift.compare shift1 shift2
166        else i2
167      else i1
168    | Val_undef, Val_undef -> 0
169    | Val_int _, _ -> 1
170    | _, Val_int _ -> -1
171    | Val_float _, _ -> 1
172    | _, Val_float _ -> -1
173    | Val_ptr _, _ -> 1
174    | _, Val_ptr _ -> -1
175    | Val_ptrh _, _ -> 1
176    | _, Val_ptrh _ -> -1
177    | Val_ptrl _, _ -> 1
178    | _, Val_ptrl _ -> -1
179
180  let hash = function 
181    | Val_int i -> Int.to_int i
182    | Val_float f -> int_of_float f
183    | Val_undef -> 0
184    | Val_ptr (b,o) -> Integer.to_int (Integer.add b o)
185    | Val_ptrh (b,o,s)
186    | Val_ptrl (b,o,s) -> Integer.to_int (Integer.add b (Integer.add o s))
187
188  let equal a b = compare a b = 0
189  let eq a b = compare a b = 0
190
191  let to_string = function
192    | Val_int i -> Int.to_string i
193    | Val_float f -> string_of_float f
194    | Val_ptr (b, off) ->
195      "Ptr(" ^ (Block.to_string b) ^ ", " ^ (Offset.to_string off) ^ ")"
196    | Val_ptrh (b, off, shift) ->
197      "PtrH(" ^ (Block.to_string b) ^ ", " ^ (Offset.to_string off) ^ ", " ^
198      (Shift.to_string shift) ^ ")"
199    | Val_ptrl (b, off, shift) ->
200      "PtrL(" ^ (Block.to_string b) ^ ", " ^ (Offset.to_string off) ^ ", " ^
201      (Shift.to_string shift) ^ ")"
202    | Val_undef -> "undef"
203
204  let is_int = function
205    | Val_int _ -> true
206    | _ -> false
207
208  let to_int = function
209    | Val_int i -> Int.to_int i
210    | _ -> raise (Failure "Value.to_int")
211
212  let of_int i = Val_int (Int.of_int i)
213
214  let to_int_repr = function
215    | Val_int i -> i
216    | _ -> raise (Failure "Value.to_int_repr")
217
218  let of_int_repr i = Val_int i
219
220  let is_pointer = function
221    | Val_ptr _ -> true
222    | _ -> false
223
224  let to_pointer = function
225    | Val_ptr (b, off) -> (b, off)
226    | _ -> raise (Failure "Value.to_pointer")
227
228  let of_pointer (b, off) = Val_ptr (b, off)
229
230  let is_float = function
231    | Val_float _ -> true
232    | _ -> false
233
234  let to_float = function
235    | Val_float f -> f
236    | _ -> raise (Failure "Value.to_float")
237
238  let of_float f = Val_float f
239
240  let zero = Val_int Int.zero
241
242  let val_true = Val_int Int.one
243
244  let val_false  = Val_int Int.zero
245
246  let is_true = function
247    | Val_int i -> Int.neq i Int.zero
248    | Val_ptr _ | Val_ptrh _ | Val_ptrl _ -> true
249    | _ -> false
250
251  let is_false = function
252    | Val_int i -> Int.eq i Int.zero
253    | _ -> false
254
255  let of_bool = function
256    | true -> Val_int Int.one
257    | false -> Val_int Int.zero
258
259  let to_bool v =
260    if is_true v then true
261    else
262      if is_false v then false
263      else error "Undefined value."
264
265  let undef = Val_undef
266
267  let cast cast_fun = function
268    | Val_int i -> Val_int (cast_fun i)
269    | _ -> Val_undef
270
271  let cast8unsigned = cast Int8u.cast
272  let cast8signed = cast Int8s.cast
273  let cast16unsigned = cast Int16u.cast
274  let cast16signed = cast Int16s.cast
275  let cast32 = cast Int32.cast
276
277
278  let unary_int_op f = function
279    | Val_int i -> Val_int (f i)
280    | _ -> Val_undef
281
282  let binary_int_op f v1 v2 = match v1, v2 with
283    | Val_int i1, Val_int i2 -> Val_int (f i1 i2)
284    | _ -> Val_undef
285
286  let binary_intu_op f v1 v2 = match v1, v2 with
287    | Val_int i1, Val_int i2 -> 
288      Val_int (Int.cast (f (Intu.cast i1) (Intu.cast i2)))
289    | _, _ -> Val_undef
290
291  let binary_int_cmp f v1 v2 = match v1, v2 with
292    | Val_int i1, Val_int i2 -> of_bool (f i1 i2)
293    | _, _ -> Val_undef
294
295  let binary_intu_cmp f v1 v2 = match v1, v2 with
296    | Val_int i1, Val_int i2 ->
297      of_bool (f (Intu.cast i1) (Intu.cast i2))
298    | _, _ -> Val_undef
299
300  let unary_float_op f = function
301    | Val_float i -> Val_float (f i)
302    | _ -> Val_undef
303
304  let binary_float_op f v1 v2 = match v1, v2 with
305    | Val_float i1, Val_float i2 -> Val_float (f i1 i2)
306    | _ -> Val_undef
307
308  let binary_float_cmp f v1 v2 = match v1, v2 with
309    | Val_float i1, Val_float i2 -> of_bool (f i1 i2)
310    | _ -> Val_undef
311
312
313  let negint = unary_int_op Int.neg
314
315  let notbool v =
316    if is_true v then val_false
317    else
318      if is_false v then val_true
319      else Val_undef
320
321  let andbool v1 v2 =
322    if is_true v1 && is_true v2 then val_true
323    else
324      if (is_true v1 && is_false v2) ||
325         (is_false v1 && is_true v2) ||
326         (is_false v1 && is_false v2) then val_false
327      else Val_undef
328
329  let orbool v1 v2 =
330    if (is_true v1 && is_true v2) ||
331       (is_true v1 && is_false v2) ||
332       (is_false v1 && is_true v2) then val_true
333    else
334      if is_false v1 && is_false v2 then val_false
335      else Val_undef
336
337  let notint = unary_int_op Int.lognot
338
339  let negf = unary_float_op (fun f -> -.f)
340
341  let absf = unary_float_op abs_float
342
343  let singleoffloat _ = assert false (* TODO *)
344
345  let intoffloat = function
346    | Val_float f -> Val_int (Int.of_int (int_of_float f))
347    | _ -> Val_undef
348
349  let intuoffloat _ = assert false (* TODO *)
350
351  let floatofint = function
352    | Val_int i -> Val_float (float_of_int (Int.to_int i))
353    | _ -> Val_undef
354
355  let floatofintu _ = assert false (* TODO *)
356
357  let add_and_of v1 v2 = match v1, v2 with
358    | Val_int i1, Val_int i2 ->
359      (Val_int (Int.add i1 i2), of_bool (Int.add_of i1 i2))
360    | Val_int i, Val_ptr (b, off)
361    | Val_ptr (b, off), Val_int i ->
362      (Val_ptr (b, Offset.add off i),
363       of_bool (Offset.add_of off (Offset.cast i)))
364    | Val_int i, Val_ptrh (b, off, shift)
365    | Val_ptrh (b, off, shift), Val_int i ->
366      (Val_ptrh (b, off, Shift.add shift i),
367       of_bool (Shift.add_of shift (Shift.cast i)))
368    | Val_int i, Val_ptrl (b, off, shift)
369    | Val_ptrl (b, off, shift), Val_int i ->
370      (Val_ptrl (b, off, Shift.add shift i),
371       of_bool (Shift.add_of shift (Shift.cast i)))
372    | _, _ -> (Val_undef, Val_undef)
373
374  let add v1 v2 = fst (add_and_of v1 v2)
375  let add_of v1 v2 = snd (add_and_of v1 v2)
376
377  let succ v = add v (Val_int Int.one)
378
379  let sub_and_uf v1 v2 = match v1, v2 with
380    | Val_int i1, Val_int i2 ->
381      (Val_int (Int.sub i1 i2), of_bool (Int.sub_uf i1 i2))
382    | Val_ptr (b, off), Val_int i ->
383      (Val_ptr (b, Offset.sub off i),
384       of_bool (Offset.sub_uf off (Offset.cast i)))
385    | Val_ptr (b1, off1), Val_ptr (b2, off2) when Block.eq b1 b2 ->
386      (Val_int (Int.cast (Offset.sub off1 off2)),
387       of_bool (Offset.sub_uf off1 off2))
388    | Val_ptrh (b, off, shift), Val_int i ->
389      (Val_ptrh (b, off, Shift.sub shift i),
390       of_bool (Shift.sub_uf shift (Shift.cast i)))
391    | Val_ptrh (b1, off1, shift1), Val_ptrh (b2, off2, shift2)
392    | Val_ptrl (b1, off1, shift1), Val_ptrl (b2, off2, shift2)
393      when Block.eq b1 b2 ->
394      let off1' = Offset.add off1 shift1 in
395      let off2' = Offset.add off2 shift2 in
396      (Val_int (Int.cast (Offset.sub off1' off2')),
397       of_bool (Offset.sub_uf off1' off2'))
398    | Val_ptrl (b, off, shift), Val_int i ->
399      (Val_ptrl (b, off, Shift.sub shift i),
400       of_bool (Shift.sub_uf shift (Shift.cast i)))
401    | _, _ -> (Val_undef, Val_undef)
402
403  let sub v1 v2 = fst (sub_and_uf v1 v2)
404  let sub_uf v1 v2 = snd (sub_and_uf v1 v2)
405
406  let pred v = sub v (Val_int Int.one)
407
408  let cmpl = unary_int_op Int.lognot
409
410  let mul = binary_int_op Int.mul
411
412  let is_zero = function
413    | Val_int i when Int.eq i Int.zero -> true
414    | _ -> false
415
416  let div v1 v2 =
417    if is_zero v2 then Val_undef
418    else binary_int_op Int.div v1 v2
419
420  let divu v1 v2 =
421    if is_zero v2 then Val_undef
422    else binary_intu_op Intu.div v1 v2
423
424  let modulo v1 v2 =
425    if is_zero v2 then Val_undef
426    else binary_int_op Int.modulo v1 v2
427
428  let modu v1 v2 =
429    if is_zero v2 then Val_undef
430    else binary_intu_op Intu.modulo v1 v2
431
432  let and_op = binary_int_op Int.logand
433
434  let or_op = binary_int_op Int.logor
435
436  let xor = binary_int_op Int.logxor
437
438  let shl = binary_int_op Int.shl
439
440  let shr = binary_int_op Int.shr
441
442  let shru = binary_int_op Int.shrl
443
444  let addf = binary_float_op (+.)
445
446  let subf = binary_float_op (-.)
447
448  let mulf = binary_float_op ( *. )
449
450  let divf v1 v2 = match v2 with
451    | Val_float f2 when f2 <> 0. -> binary_float_op (/.) v1 v2
452    | _ -> Val_undef
453
454  let cmpp_eq f_int v1 v2 = match v1, v2 with
455    | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2)
456    | Val_ptr (b1, off1), Val_ptr (b2, off2) ->
457      of_bool ((Block.eq b1 b2) && (Offset.eq off1 off2))
458    | Val_ptrh (b1, off1, shift1), Val_ptrh (b2, off2, shift2)
459    | Val_ptrl (b1, off1, shift1), Val_ptrl (b2, off2, shift2) ->
460      of_bool ((Block.eq b1 b2) && (Offset.eq off1 off2) &&
461               (Shift.eq shift1 shift2))
462    | _ -> Val_undef
463
464  let cmpp_ne cmp_eq v1 v2 = notbool (cmp_eq v1 v2)
465
466  let cmpp_lt f_int v1 v2 = match v1, v2 with
467    | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2)
468    | Val_ptr (b1, off1), Val_ptr (b2, off2) ->
469      of_bool ((Block.lt b1 b2) ||
470               ((Block.eq b1 b2) && (Offset.lt off1 off2)))
471    | Val_ptrh (b1, off1, shift1), Val_ptrh (b2, off2, shift2)
472    | Val_ptrl (b1, off1, shift1), Val_ptrl (b2, off2, shift2) ->
473      of_bool ((Block.lt b1 b2) ||
474               ((Block.eq b1 b2) && (Offset.lt off1 off2)) ||
475               ((Block.eq b1 b2) && (Offset.eq off1 off2)) &&
476                (Shift.lt shift1 shift2))
477    | _ -> Val_undef
478
479  let cmpp_ge cmp_lt v1 v2 = notbool (cmp_lt v1 v2)
480  let cmpp_le cmp_lt cmp_eq v1 v2 = orbool (cmp_lt v1 v2) (cmp_eq v1 v2)
481  let cmpp_gt cmp_le v1 v2 = notbool (cmp_le v1 v2)
482
483  let cmp_eq = cmpp_eq Int.eq
484  let cmp_ne = cmpp_ne cmp_eq
485  let cmp_lt = cmpp_lt Int.lt
486  let cmp_ge = cmpp_ge cmp_lt
487  let cmp_le = cmpp_le cmp_lt cmp_eq
488  let cmp_gt = cmpp_gt cmp_le
489
490  let cmp_eq_u = cmpp_eq Intu.eq
491  let cmp_ne_u = cmpp_ne cmp_eq_u
492  let cmp_lt_u = cmpp_lt Intu.lt
493  let cmp_ge_u = cmpp_ge cmp_lt_u
494  let cmp_le_u = cmpp_le cmp_lt_u cmp_eq_u
495  let cmp_gt_u = cmpp_gt cmp_le_u
496
497  let cmp_eq_f = binary_float_cmp (=)
498  let cmp_ne_f = binary_float_cmp (<>)
499  let cmp_lt_f = binary_float_cmp (<)
500  let cmp_ge_f = binary_float_cmp (>=)
501  let cmp_le_f = binary_float_cmp (<=)
502  let cmp_gt_f = binary_float_cmp (>)
503
504(*
505  let break v n = match n, v with
506    (* Parameter [n] is used to generalize the concept of breaking a value into
507       multiple parts. But for now, we only break values in exactly two
508       parts. *)
509    | 0, _ -> []
510    | 1, _ -> [v]
511    | 2, Val_ptr (b, off) ->
512      [Val_ptrh (b, off) ; Val_ptrl (b, off, Integer.zero)]
513    | 2, Val_int i -> [Val_int i ; Val_int i]
514    | 2, _ -> MiscPottier.make Val_undef 2
515    | _ -> error "Trying to break in more than two parts."
516
517  let merge = function
518    | [] -> Val_undef
519    | [v] -> v
520    | [Val_ptrh (b1, off1) ; Val_ptrl (b2, off2, shift)]
521        when Block.eq b1 b2 && Offset.eq off1 off2 ->
522      Val_ptr (b1, Offset.add off1 shift)
523    | [Val_int i1 ; Val_int i2] -> Val_int (Int.add i1 i2)
524    | [_ ; _] -> Val_undef
525    | _ -> error "Trying to merge more than two values."
526*)
527
528  let break v n = match n, v with
529    (* Parameter [n] is used to generalize the concept of breaking a value into
530       multiple parts. But for now, we only break values in exactly two
531       parts. *)
532    | 0, _ -> []
533    | 1, _ -> [v]
534    | 2, Val_ptr (b, off) ->
535      [Val_ptrh (b, off, Shift.zero) ; Val_ptrl (b, off, Shift.zero)]
536    | _, Val_int i -> List.map (fun i -> Val_int i) (Int.break i n)
537    | 2, _ -> MiscPottier.make Val_undef 2
538    | _ -> error "Trying to break in more than two parts."
539
540  let merge = function
541    | [] -> Val_undef
542    | [v] -> v
543    | [Val_ptrh (b1, off1, shift1) ; Val_ptrl (b2, off2, shift2)]
544        when Block.eq b1 b2 && Offset.eq off1 off2 ->
545      Val_ptr (b1, Offset.add off1 (Offset.merge [shift1 ; shift2]))
546    | [Val_int i1 ; Val_int i2] -> Val_int (Int.add i1 i2)
547    | [_ ; _] -> Val_undef
548    | _ -> error "Trying to merge more than two values."
549
550end
Note: See TracBrowser for help on using the repository browser.