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

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

32 and 16 bits operations support in D2.2/8051

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