Ignore:
Timestamp:
Apr 4, 2011, 5:18:15 PM (10 years ago)
Author:
ayache
Message:

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

Location:
Deliverables/D2.2/8051/src/common
Files:
7 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D2.2/8051/src/common/intValue.ml

    r630 r740  
    7979
    8080  (** [break i n] cuts [i] in [n] parts. In the resulting list, the first
    81       element is the high bits, and the last is the low bits. *)
     81      element is the low bits, and the last is the high bits (little endian
     82      representation). *)
    8283  val break : t -> int -> t list
    8384  (** [merge l] creates the integer where the first element of [l] is its
    84       high bits, etc, and the last element of [l] is its low bits. *)
     85      low bits, etc, and the last element of [l] is its high bits (little endian
     86      representation). *)
    8587  val merge : t list -> t
    8688
    … …  
    242244
    243245  (* [break i n] cuts [i] in [n] parts. In the resulting list, the first element
    244      is the high bits, and the last is the low bits. *)
     246     is the low bits, and the last is the high bits (little endian
     247     representation). *)
    245248  let break a n =
    246249    let chunk_size = size / n in
    … …  
    252255        aux ((cast chunk) :: acc) next (i-1)
    253256    in
    254     aux [] (cast a) n
    255 
    256   (* [merge l] creates the integer where the first element of [l] is its high
    257      bits, etc, and the last element of [l] is its low bits. *)
     257    List.rev (aux [] (cast a) n)
     258
     259  (* [merge l] creates the integer where the first element of [l] is its low
     260     bits, etc, and the last element of [l] is its high bits (little endian
     261     representation). *)
    258262  let merge = function
    259263    | [] -> zero
    260264    | al ->
    261       let al = List.rev al in
    262265      let nb_chunks = List.length al in
    263266      let chunk_size = size / nb_chunks in

  • Deliverables/D2.2/8051/src/common/memory.ml

    r619 r740  
    44    following the memory model of the CompCert compiler. *)
    55
    6 open IntValue
     6(** In the module, every size is expressed in bytes. *)
    77
    88
    … …  
    1111
    1212
    13 (* Memory quantities are the size and the type of what can be loaded
    14    and stored in memory *)
    15 
    16 type memory_q =
    17   | MQ_int8signed | MQ_int8unsigned | MQ_int16signed | MQ_int16unsigned
    18   | MQ_int32 | MQ_float32 | MQ_float64 | MQ_pointer | MQ_chunk
    19 
    20 let string_of_memory_q = function
    21   | MQ_int8signed -> "int8s"
    22   | MQ_int8unsigned -> "int8u"
    23   | MQ_int16signed -> "int16s"
    24   | MQ_int16unsigned -> "int16u"
    25   | MQ_int32 -> "int32"
    26   | MQ_float32 -> "float"
    27   | MQ_float64 -> "float64"
    28   | MQ_pointer -> "ptr"
    29   | MQ_chunk -> "chunk"
    30 
    31 let mq_of_data = function
    32   | AST.Data_reserve _ -> assert false (* Should not be called on this *)
    33   | AST.Data_int8 _ -> MQ_int8signed
    34   | AST.Data_int16 _ -> MQ_int16signed
    35   | AST.Data_int32 _ -> MQ_int32
    36   | AST.Data_float32 _ -> MQ_float32
    37   | AST.Data_float64 _ -> MQ_float64
    38 
    39 let type_of_memory_q = function
    40   | MQ_int8signed | MQ_int8unsigned | MQ_int16signed | MQ_int16unsigned
    41   | MQ_int32 -> AST.Sig_int
    42   | MQ_float32 | MQ_float64 -> AST.Sig_float
    43   | MQ_pointer -> AST.Sig_ptr
    44   | MQ_chunk -> error "Trying to get the type of a pointer chunk."
     13(** Memory quantities is the size and type of what can be loaded or stored in
     14    memory. *)
     15
     16type quantity =
     17  | QInt of int (* Sized integer *)
     18  | QPtr        (* Pointer *)
     19
     20let string_of_quantity = function
     21  | QInt i -> string_of_int i
     22  | QPtr -> "ptr"
     23
     24
     25let size_of_data = function
     26  | AST.Data_reserve n -> n
     27  | AST.Data_int8 _ -> 1
     28  | AST.Data_int16 _ -> 2
     29  | AST.Data_int32 _ -> 4
     30  | AST.Data_float32 _ -> 4
     31  | AST.Data_float64 _ -> 8
    4532
    4633
    … …  
    6148sig
    6249
    63   val mq_of_ptr : memory_q
    6450  val int_size  : int
    6551  val ptr_size  : int
    6652  val alignment : int option
     53
     54  val size_of_quantity : quantity -> int
    6755
    6856  module Value : Value.S
    … …  
    7967  val empty : 'fun_def memory
    8068
    81   (** [alloc mem size] allocates a block of [size] size (in bytes) in the memory
    82       [mem]. It returns the new memory and a pointer to the beginning of the
     69  (** [alloc mem size] allocates a block of [size] bytes in the memory [mem]. It
     70      returns the new memory and the address of the beginning of the newly
    8371      allocated area. *)
    84   val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.t
     72  val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.address
    8573
    8674  (* Memory free *)
    8775
    88   val free : 'fun_def memory -> Value.t -> 'fun_def memory
     76  val free : 'fun_def memory -> Value.address -> 'fun_def memory
    8977
    9078  (* Memory load and store *)
    9179
    92   (** [load mem chunk addr] reads a value of type [chunk] at the address [addr]
    93       in memory [mem]. *)
    94   val load : 'fun_def memory -> memory_q -> Value.t -> Value.t
    95   (** [load2 mem size addr] reads a value of size [size] at the address [addr]
    96       in memory [mem]. *)
    97   val load2 : 'fun_def memory -> int -> Value.t -> Value.t
    98 
    99   (** [store mem chunk addr v] writes the value [v] interpreted as a value of
    100       type [chunk] at address [addr] in memory [mem]. *)
    101   val store  : 'fun_def memory -> memory_q -> Value.t -> Value.t ->
     80  (** [load mem size addr] reads [size] bytes from address [addr] in memory
     81      [mem] and returns the value found. *)
     82  val load : 'fun_def memory -> int -> Value.address -> Value.t
     83  val loadq : 'fun_def memory -> quantity -> Value.address -> Value.t
     84
     85  (** [store mem size addr v] writes the [size] first bytes (little endian
     86      representation) of value [v] at address [addr] in memory [mem]. *)
     87  val store  : 'fun_def memory -> int -> Value.address -> Value.t ->
    10288               'fun_def memory
    103   (** [store mem size addr v] writes the value [v] of size [size] at address
    104       [addr] in memory [mem]. *)
    105   val store2 : 'fun_def memory -> int -> Value.t -> Value.t ->
     89  val storeq : 'fun_def memory -> quantity -> Value.address -> Value.t ->
    10690               'fun_def memory
     91
     92  (* Globals management *)
    10793
    10894  (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
    … …  
    116102  val add_fun_def : 'fun_def memory -> AST.ident -> 'fun_def -> 'fun_def memory
    117103
     104  val mem_global : 'fun_def memory -> AST.ident -> bool
     105
    118106  (** [find_global mem x] returns the address associated with the global symbol
    119107      [x] in memory [mem]. [x] may be a global variable or the name of a
    120108      function. *)
    121   val find_global : 'fun_def memory -> AST.ident -> Value.t
     109  val find_global : 'fun_def memory -> AST.ident -> Value.address
    122110
    123111  (** [find_fun_def mem addr] returns the function definition found at address
    124112      [addr] in memory [mem]. Raises an error if no function definition is
    125113      found. *)
    126   val find_fun_def : 'fun_def memory -> Value.t -> 'fun_def
     114  val find_fun_def : 'fun_def memory -> Value.address -> 'fun_def
    127115
    128116  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
    … …  
    131119              (int list (* resulting offsets *) * int (* full size *))
    132120
    133   val size_of_datas    : AST.data list -> int
     121  val size_of_datas : AST.data list -> int
    134122
    135123  (** [offsets_of_datas datas] returns the aligned offsets for the datas
    … …  
    137125  val offsets_of_datas : AST.data list -> (AST.data * int (* offset *)) list
    138126
    139   val alloc_datas      : 'fun_def memory -> AST.data list ->
    140                          ('fun_def memory * Value.t)
    141 
     127  val alloc_datas : 'fun_def memory -> AST.data list ->
     128                    ('fun_def memory * Value.address)
     129
     130  val to_string : 'fun_def memory -> string
    142131  val print : 'fun_def memory -> unit
    143132
    … …  
    145134
    146135
    147 (** The functor to a memory module. *)
     136(** The functor of a memory module. *)
    148137
    149138module Make (D : DATA_SIZE) =
    … …  
    154143  module Offset = Value.Offset
    155144
    156   let mq_of_ptr = MQ_pointer
     145  let address_of_block_offset b off =
     146    Value.of_mem_address (Value.make_mem_address b off)
    157147
    158148  let int_size = D.int_size
    … …  
    160150  let alignment = D.alignment
    161151
    162 
    163   (* Contents of a variable. *)
    164 
    165   type cell =
    166     | Datum of int * Value.t (* the size of the content and its value *)
    167     | Cont                   (* the continuation of a content defined in a
    168                                 previous block *)
     152  let size_of_quantity = function
     153    | QInt i -> i
     154    | QPtr -> ptr_size
    169155
    170156
    171157  module OffsetMap = Map.Make (Offset)
    172   type offsetMap = cell OffsetMap.t
     158  type offsetMap = Value.chunk OffsetMap.t
    173159  type offset = Offset.t
    174160
     161  (* Empty cells are interpreted as an undefined byte value. *)
     162
    175163  type contents =
    176       { low   : offset ;
    177         high  : offset ;
     164      { low   : offset ; (* inclusive *)
     165        high  : offset ; (* inclusive *)
    178166        cells : offsetMap }
    179167
    … …  
    181169  let add_cells contents off v =
    182170    update_cells contents (OffsetMap.add off v contents.cells)
     171  let remove_cells contents off =
     172    update_cells contents (OffsetMap.remove off contents.cells)
    183173
    184174  (* Alignment *)
    … …  
    247237
    248238  module GlobalMap = Map.Make (String)
    249   type globalMap = Value.t GlobalMap.t
     239  type globalMap = Value.address GlobalMap.t
    250240
    251241  (* The memory.
    … …  
    263253  (* Pretty printing *)
    264254
    265   let print mem =
    266     let print_cells off = function
    267       | Datum (size, v) when Value.eq v Value.undef ->
    268         ()
    269       | Datum (size, v) ->
    270         Printf.printf "\n  %s: [%d,%s]%!"
    271           (Offset.to_string off) size (Value.to_string v)
    272       | Cont -> Printf.printf "[Cont]%!" in
    273     let print_block b content =
    274       Printf.printf "\nBlock %s: %!" (Block.to_string b) ;
    275       match content with
     255  let to_string mem =
     256    let i = ref 0 in
     257    let string_of_cell off v s =
     258      let s' = if !i mod 4 = 0 then (i := 0 ; "\n ") else "" in
     259      i := !i+1 ;
     260      let sv =
     261        if Value.is_undef_byte v then ""
     262        else Printf.sprintf "[%s]: %s"
     263          (Offset.to_string off) (Value.string_of_chunk v) in
     264      Printf.sprintf "%s%s %s" s s' sv in
     265    let string_of_cells cells = OffsetMap.fold string_of_cell cells "" in
     266    let string_of_block b content s =
     267      (Printf.sprintf "%s\nBlock %s: " s (Block.to_string b)) ^
     268      (match content with
    276269        | Contents contents ->
    277           Printf.printf "(%s -> %s)%!"
    278             (Offset.to_string contents.low) (Offset.to_string contents.high) ;
    279           OffsetMap.iter print_cells contents.cells
    280         | Fun_def _ -> Printf.printf "function definition%!" ;
    281     in
    282     BlockMap.iter print_block mem.blocks ;
    283     Printf.printf "\n%!"
     270          i := 0 ;
     271          Printf.sprintf "(%s -> %s)%s"
     272            (Offset.to_string contents.low)
     273            (Offset.to_string contents.high)
     274            (string_of_cells contents.cells)
     275        | Fun_def _ -> "function definition") in
     276    Printf.sprintf "%s\n" (BlockMap.fold string_of_block mem.blocks "")
     277
     278    let print mem = Printf.printf "%s%!" (to_string mem)
    284279
    285280
    … …  
    294289  (* Memory allocation *)
    295290
    296   (** [write_interval contents lo_off hi_off d] writes the cell [d] in the
    297       contents [contents] from the offset [lo_off] (inclusive) to the offset
    298       [hi_off] (exclusive). *)
    299   let rec write_interval contents lo_off hi_off d =
    300     if Offset.ge lo_off hi_off then contents
    301     else
    302       let contents = add_cells contents lo_off d in
    303       write_interval contents (Offset.succ lo_off) hi_off d
    304 
    305   (** [alloc2 mem lo hi] allocates in memory [mem] a new block whose readable
    306       and writable offsets are the interval [lo] (inclusive) [hi]
    307       (exclusive). *)
    308   let alloc2 mem lo hi =
     291  (** [alloc2 mem low high] allocates in memory [mem] a new block whose readable
     292      and writable offsets are the interval [low] (inclusive) [high]
     293      (inclusive). *)
     294  let alloc2 mem low high =
    309295    let b = mem.next_block in
    310     let contents = { low = lo ; high = hi ; cells = OffsetMap.empty } in
    311     let contents = write_interval contents lo hi (Datum (1, Value.undef)) in
     296    let contents = { low = low ; high = high ; cells = OffsetMap.empty } in
    312297    let blocks = BlockMap.add b (Contents contents) mem.blocks in
    313298    let next_block = Block.succ mem.next_block in
    314299    let mem' = { mem with blocks = blocks ; next_block = next_block } in
    315     (mem', Value.of_pointer (b, lo))
    316 
    317   (** [alloc mem size] allocates a block of [size] size (in bytes) in the memory
    318       [mem]. It returns the new memory and a pointer to the beginning of the
     300    (mem', address_of_block_offset b low)
     301
     302  (** [alloc mem size] allocates a block of [size] bytes in the memory [mem]. It
     303      returns the new memory and the address of the beginning of the newly
    319304      allocated area. *)
    320305  let alloc mem size =
    321     alloc2 mem Offset.zero (Offset.of_int size)
    322 
    323 
    324   let size_of_mq = function
    325     | MQ_int8unsigned | MQ_int8signed -> 1
    326     | MQ_int16unsigned | MQ_int16signed -> 2
    327     | MQ_int32 | MQ_float32 -> 4
    328     | MQ_float64 -> 8
    329     | MQ_pointer -> D.ptr_size
    330     | MQ_chunk -> D.ptr_size/2
    331 
    332   let cast_of_mq = function
    333     | MQ_int8unsigned -> Value.cast8unsigned
    334     | MQ_int8signed -> Value.cast8signed
    335     | MQ_int16unsigned -> Value.cast16unsigned
    336     | MQ_int16signed -> Value.cast16signed
    337     | MQ_int32 -> Value.cast32
    338     | MQ_float32 | MQ_float64 -> error "float not supported."
    339     | MQ_pointer | MQ_chunk -> (fun v -> v)
     306    if size = 0 then (mem, Value.null)
     307    else alloc2 mem Offset.zero (Offset.of_int (size-1))
     308
    340309
    341310  (* The 'safe'-prefixed functions below raise an error when the argument is not
    342311     of the expected form. *)
    343312
    344   let safe_to_pointer msg v =
    345     if Value.is_pointer v then Value.to_pointer v
     313  let safe_to_address msg vs =
     314    if Value.is_mem_address vs then Value.to_mem_address vs
    346315    else error msg
    347316
    348   let safe_find msg find a map =
     317  let safe_find not_found find a map =
    349318    try find a map
    350     with Not_found -> error msg
    351 
    352   let safe_find_block msg b mem = safe_find msg BlockMap.find b mem.blocks
     319    with Not_found -> not_found ()
     320
     321  let safe_find_err msg = safe_find (fun () -> error msg)
     322
     323  let safe_find_block msg b mem = safe_find_err msg BlockMap.find b mem.blocks
    353324
    354325  let safe_find_contents msg b mem = match safe_find_block msg b mem with
    … …  
    357328
    358329  let safe_find_offset msg off contents =
    359     safe_find msg OffsetMap.find off contents.cells
     330    if (Offset.leu contents.low off) && (Offset.leu off contents.high) then
     331      safe_find (fun () -> Value.undef_byte) OffsetMap.find off contents.cells
     332    else error msg
    360333
    361334  let memory_find msg mem b off =
    362335    safe_find_offset msg off (safe_find_contents msg b mem)
    363336
    364   (** [all_are_in_list msg mem b first_off last_off dl] returns [true] iff all
    365       the datas found in the block [b] of memory [mem] and between offsets
    366       [first_off] (inclusive) and [last_off] (exclusive) are in the list
    367       [dl]. *)
    368   let all_are_in_list msg mem b first_off last_off dl =
    369     let d_eq d d' = match d, d' with
    370       | Datum (size, v), Datum (size', v') -> (size = size') && (Value.eq v v')
    371       | Cont, Cont -> true
    372       | _ -> false in
    373     let rec aux d = function
    374       | [] -> false
    375       | d' :: dl -> (d_eq d d') || (aux d dl) in
    376     let dl_mem d = aux d dl in
     337
     338  (* Memory free *)
     339
     340  let free mem vs =
     341    let addr = safe_to_address "free: invalid memory address." vs in
     342    let (b, _) = Value.decompose_mem_address addr in
     343    { mem with blocks = BlockMap.remove b mem.blocks }
     344
     345
     346  (* Memory load *)
     347
     348  (** [load_bytes msg mem b off size] reads [size] bytes from the block [b] and
     349      offset [off] in memory [mem] and returns the value found. If an error
     350      occurs, [msg] will be printed. *)
     351  let load_bytes msg mem b off size =
     352    let shift_off n = Offset.add off (Offset.of_int n) in
     353    let rec aux n =
     354      if n >= size then []
     355      else (memory_find msg mem b (shift_off n)) :: (aux (n+1)) in
     356    Value.merge (aux 0)
     357
     358  (** [load mem size addr] reads [size] bytes from address [addr] in memory
     359      [mem] and returns the value found. *)
     360  let load mem size vs =
     361    let msg = "load: invalid memory access." in
     362    let addr = safe_to_address msg vs in
     363    let (b, off) = Value.decompose_mem_address addr in
     364    if not (is_aligned off size) then
     365      error "Alignment constraint violated when loading value."
     366    else load_bytes msg mem b off size
     367
     368  let loadq mem q vs = load mem (size_of_quantity q) vs
     369
     370
     371  (* Memory store *)
     372
     373  (** [store_chunks msg mem size b off chunks] writes the [size] first chunks of
     374      list [chunks] at the offset [off] of the block [b] in the memory [mem]. *)
     375  let store_chunks msg mem size b off chunks =
     376    let shift_off n = Offset.add off (Offset.of_int n) in
     377    let f i contents chunk =
     378      let off' = shift_off i in
     379      if (Offset.leu contents.low off') &&
     380         (Offset.leu off' contents.high) then
     381        if Value.is_undef_byte chunk then contents
     382        else add_cells contents off' chunk
     383      else error msg in
    377384    match safe_find_block msg b mem with
    378       | Contents contents
    379           when (Offset.le contents.low first_off) &&
    380             (Offset.le last_off contents.high) ->
    381         let rec aux off =
    382           if Offset.ge off last_off then true
    383           else
    384             if OffsetMap.mem off contents.cells then
    385               let d = OffsetMap.find off contents.cells in
    386               (dl_mem d) && (aux (Offset.succ off))
    387             else false
    388         in
    389         aux first_off
    390       | _ -> false
    391 
    392   (** [all_are_undef msg mem b first_off last_off] returns [true] iff all the
    393       datas found in the block [b] of memory [mem] and between offsets
    394       [first_off] (inclusive) and [last_off] (exclusive) are the undef value. *)
    395   let all_are_undef msg mem b first_off last_off =
    396     all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef)]
    397 
    398   (** [all_are_undef msg mem b first_off last_off] returns [true] iff all the
    399       datas found in the block [b] of memory [mem] and between offsets
    400       [first_off] (inclusive) and [last_off] (exclusive) are the undef value or
    401       the Cont cell. *)
    402   let all_are_undef_or_cont msg mem b first_off last_off =
    403     all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef) ; Cont]
    404 
    405   let string_of_alignment = function
    406     | None -> "none"
    407     | Some alignment -> string_of_int alignment
    408 
    409   (** [write_value msg mem b off size v size'] store the value [v] at the offset
    410       [off] of the block [b] in the memory [mem]. [size] is the size of the
    411       value [v], and [size'] >= [size] is the number of bytes that are actually
    412       written. When [size'] > [size], the undefined value is used to fill the
    413       remaining memory cells. *)
    414   let write_value msg mem b off size v size' =
     385      | Contents contents ->
     386        let contents = MiscPottier.foldi_until size f contents chunks in
     387        let blocks = BlockMap.add b (Contents contents) mem.blocks in
     388        { mem with blocks = blocks }
     389      | _ -> error msg
     390
     391  (** [store mem size addr v] writes the [size] first bytes (little endian
     392      representation) of value [v] at address [addr] in memory [mem]. *)
     393  let store mem size vs v =
     394    let msg = "store: invalid memory access." in
     395    let addr = safe_to_address msg vs in
     396    let (b, off) = Value.decompose_mem_address addr in
    415397    if not (is_aligned off size) then
    416398      error "Alignment constraint violated when storing value."
    417     else
    418       let shift_off n = Offset.add off (Offset.of_int n) in
    419       match safe_find_block msg b mem with
    420         | Contents contents
    421             when (Offset.le contents.low off) &&
    422               (Offset.le (shift_off size) contents.high) ->
    423           let contents = add_cells contents off (Datum (size, v)) in
    424           let contents =
    425             write_interval contents (Offset.succ off) (shift_off size) Cont in
    426           let contents =
    427             write_interval contents (shift_off size) (shift_off size')
    428               (Datum (1, Value.undef)) in
    429           let blocks = BlockMap.add b (Contents contents) mem.blocks in
    430           { mem with blocks = blocks }
    431         | _ -> error msg
    432 
    433 
    434   (* Memory free *)
    435 
    436   let free mem addr =
    437     if Value.is_pointer addr then
    438       let (b, _) = Value.to_pointer addr in
    439       { mem with blocks = BlockMap.remove b mem.blocks }
    440     else error "free: invalid memory address."
    441 
    442 
    443   (* Memory load and store *)
    444 
    445   (** [load2 mem size addr] reads a value of size [size] at the address [addr]
    446       in memory [mem]. *)
    447   let load2 mem size addr =
    448     let msg = ("load: invalid memory access. ("^(Value.to_string addr)^")") in
    449     let (b, off) = safe_to_pointer msg addr in
    450     if not (is_aligned off size) then
    451       error "Alignment constraint violated when loading value."
    452     else
    453       match memory_find msg mem b off with
    454         | Datum (size', v) when size <= size' ->
    455           v
    456               (*print_string ("Db: load m "^(string_of_memory_q chunk)^" "
    457                             ^(Value.to_string addr)^" "^(Value.to_string r)^" ("
    458                             ^(Value.to_string v)^")\n"); *)
    459         | _ -> print mem;error msg
    460 
    461   (** [load mem chunk addr] reads a value of type [chunk] at the address [addr]
    462       in memory [mem]. *)
    463   let load mem chunk addr =
    464     let size = size_of_mq chunk in
    465     cast_of_mq chunk (load2 mem size addr)
    466 
    467 
    468   (** [write_undef_before msg mem b off] replaces with undefined values the
    469       value whose last cell is at offset [off] of block [b] in memory
    470       [mem]. *)
    471   let write_undef_before msg mem b off =
    472     let contents = safe_find_contents msg b mem in
    473     let d = Datum (1, Value.undef) in
    474     let rec aux off contents =
    475       if OffsetMap.mem off contents.cells then
    476         let contents' = add_cells contents off d in
    477         match OffsetMap.find off contents.cells with
    478           | Datum _ -> contents'
    479           | Cont -> aux (Offset.pred off) contents'
    480       else contents
    481     in
    482     let contents = aux off contents in
    483     { mem with blocks = BlockMap.add b (Contents contents) mem.blocks }
    484 
    485   (** [store2 mem size addr v] writes the value [v] of size [size] at address
    486       [addr] in memory [mem]. *)
    487   let store2 mem size addr v =
    488     let msg = "store: invalid memory access." in
    489     let (b, off) = safe_to_pointer msg addr in
    490     let shift_off n = Offset.add off (Offset.of_int n) in
    491     (*print_string ("Db: store m "^(string_of_memory_q chunk)^" "
    492       ^(Value.to_string addr)^" "^(Value.to_string v)^" ("
    493       ^(Value.to_string v0)^")\n"); *)
    494     match memory_find msg mem b off with
    495       | Datum (size', _) when size <= size' ->
    496           write_value msg mem b off size v size'
    497       | Datum (size', _)
    498           when all_are_undef msg mem b (shift_off size') (shift_off size) ->
    499           write_value msg mem b off size v size'
    500       | Cont when all_are_undef_or_cont msg mem b off (shift_off size) ->
    501           let mem = write_value msg mem b off size v size in
    502           write_undef_before msg mem b (Offset.pred off)
    503       | _ -> error msg
    504 
    505   (** [store mem chunk addr v] writes the value [v] interpreted as a value of
    506       type [chunk] at address [addr] in memory [mem]. *)
    507   let store mem chunk addr v =
    508     store2 mem (size_of_mq chunk) addr (cast_of_mq chunk v)
    509 
    510 
    511 (* Data manipulation *)
     399    else store_chunks msg mem size b off (Value.break v)
     400
     401  let storeq mem q vs v = store mem (size_of_quantity q) vs v
     402
     403
     404  (* Data manipulation *)
    512405
    513406  let value_of_data = function
    514407    | AST.Data_reserve _ -> Value.undef
    515408    | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i -> Value.of_int i
    516     | AST.Data_float32 f | AST.Data_float64 f -> Value.of_float f
    517 
    518   let size_of_data = function
    519     | AST.Data_reserve n -> n
    520     | data -> size_of_mq (mq_of_data data)
     409    | AST.Data_float32 f | AST.Data_float64 f -> error "float not supported."
    521410
    522411  let offsets_size_of_datas datas =
    … …  
    526415      allocating space and storing the datas [datas] in the memory [mem]. *)
    527416  let alloc_datas mem datas =
     417    let msg = "cannot allocate datas." (* TODO *) in
    528418    let (offs_of_datas, size) = offsets_size_of_datas datas in
    529     let (mem, addr) = alloc mem size in
    530     let shift_addr off = Value.add addr (Value.of_int_repr off) in
     419    let (mem, vs) = alloc mem size in
     420    let addr = safe_to_address msg vs in
     421    let (b, off) = Value.decompose_mem_address addr in
     422    let shift_addr off' =
     423      let off = Offset.add off off' in
     424      address_of_block_offset b off in
    531425    let f mem data off = match data with
    532426      | AST.Data_reserve _ -> mem
    533       | _ -> store mem (mq_of_data data) (shift_addr off) (value_of_data data)
     427      | _ -> store mem (size_of_data data) (shift_addr off) (value_of_data data)
    534428    in
    535     (List.fold_left2 f mem datas offs_of_datas, addr)
     429    (List.fold_left2 f mem datas offs_of_datas, vs)
    536430
    537431  let size_of_datas datas = snd (offsets_size_of_datas datas)
    … …  
    550444
    551445
    552   (* Global environment manipulation *)
     446  (* Globals manipulation *)
    553447
    554448  (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
    … …  
    556450      the block. *)
    557451  let add_var mem v_id datas =
    558     let (mem, addr) = alloc_datas mem datas in
    559     let addr_of_global = GlobalMap.add v_id addr mem.addr_of_global in
     452    let (mem, vs) = alloc_datas mem datas in
     453    let addr_of_global = GlobalMap.add v_id vs mem.addr_of_global in
    560454    { mem with addr_of_global = addr_of_global }
    561455
    … …  
    566460    let b = mem.next_fun_block in
    567461    let next_fun_block = Block.pred mem.next_fun_block in
    568     let addr = Value.of_pointer (b, Offset.zero) in
    569     let addr_of_global = GlobalMap.add f_id addr mem.addr_of_global in
     462    let vs = address_of_block_offset b Offset.zero in
     463    let addr_of_global = GlobalMap.add f_id vs mem.addr_of_global in
    570464    let blocks = BlockMap.add b (Fun_def f_def) mem.blocks in
    571465    { mem with blocks = blocks ;
    572466               addr_of_global = addr_of_global ;
    573467               next_fun_block = next_fun_block }
     468
     469  let mem_global mem id = GlobalMap.mem id mem.addr_of_global
    574470
    575471  (** [find_global mem x] returns the address associated with the global symbol
    … …  
    584480      [addr] in memory [mem]. Raises an error if no function definition is
    585481      found. *)
    586   let find_fun_def mem v =
     482  let find_fun_def mem vs =
    587483    let msg = "Invalid access to a function definition." in
    588     let (b, _) = safe_to_pointer msg v in
     484    let (b, _) = Value.decompose_mem_address (safe_to_address msg vs) in
    589485    match safe_find_block msg b mem with
    590486      | Contents _ -> error msg
    591487      | Fun_def def -> def
    592488
    593 
    594  
    595 
    596489end

  • Deliverables/D2.2/8051/src/common/memory.mli

    r619 r740  
    44    following the memory model of the CompCert compiler. *)
    55
    6 (** In the module, every size are expressed in bytes. *)
     6(** In the module, every size is expressed in bytes. *)
    77
     8(** Memory quantities is the size and type of what can be loaded or stored in
     9    memory. *)
    810
    9 (* Memory quantities are the size and the type of what can be loaded
    10    and stored in memory *)
     11type quantity =
     12  | QInt of int (* Sized integer *)
     13  | QPtr        (* Pointer *)
    1114
    12 type memory_q =
    13   | MQ_int8signed | MQ_int8unsigned | MQ_int16signed | MQ_int16unsigned
    14   | MQ_int32 | MQ_float32 | MQ_float64 | MQ_pointer
    15   | MQ_chunk (* no type, just the raw content of a word size *)
     15val string_of_quantity : quantity -> string
    1616
    17 val string_of_memory_q : memory_q -> string
    18 
    19 val mq_of_data : AST.data -> memory_q
    20 
    21 val type_of_memory_q : memory_q -> AST.sig_type
     17val size_of_data  : AST.data -> int
    2218
    2319
    … …  
    2622module type DATA_SIZE =
    2723sig
    28   val int_size  : int (* in bytes *)
    29   val ptr_size  : int (* in bytes *)
    30   val alignment : int option (* in bytes, if any *)
     24  val int_size  : int
     25  val ptr_size  : int
     26  val alignment : int option
    3127end
    3228
    … …  
    3834sig
    3935
    40   val mq_of_ptr : memory_q
    4136  val int_size  : int
    4237  val ptr_size  : int
    4338  val alignment : int option
     39
     40  val size_of_quantity : quantity -> int
    4441
    4542  module Value : Value.S
    … …  
    5653  val empty : 'fun_def memory
    5754
    58   (** [alloc mem size] allocates a block of [size] size (in bytes) in the memory
    59       [mem]. It returns the new memory and a pointer to the beginning of the
     55  (** [alloc mem size] allocates a block of [size] bytes in the memory [mem]. It
     56      returns the new memory and the address of the beginning of the newly
    6057      allocated area. *)
    61   val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.t
     58  val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.address
    6259
    6360  (* Memory free *)
    6461
    65   val free : 'fun_def memory -> Value.t -> 'fun_def memory
     62  val free : 'fun_def memory -> Value.address -> 'fun_def memory
    6663
    6764  (* Memory load and store *)
    6865
    69   (** [load mem chunk addr] reads a value of type [chunk] at the address [addr]
    70       in memory [mem]. *)
    71   val load : 'fun_def memory -> memory_q -> Value.t -> Value.t
    72   (** [load2 mem size addr] reads a value of size [size] at the address [addr]
    73       in memory [mem]. *)
    74   val load2 : 'fun_def memory -> int -> Value.t -> Value.t
     66  (** [load mem size addr] reads [size] bytes from address [addr] in memory
     67      [mem] and returns the value found. *)
     68  val load  : 'fun_def memory -> int -> Value.address -> Value.t
     69  val loadq : 'fun_def memory -> quantity -> Value.address -> Value.t
    7570
    76   (** [store mem chunk addr v] writes the value [v] interpreted as a value of
    77       type [chunk] at address [addr] in memory [mem]. *)
    78   val store  : 'fun_def memory -> memory_q -> Value.t -> Value.t ->
     71  (** [store mem size addr v] writes the [size] first bytes (little endian
     72      representation) of value [v] at address [addr] in memory [mem]. *)
     73  val store  : 'fun_def memory -> int -> Value.address -> Value.t ->
    7974               'fun_def memory
    80   (** [store2 mem size addr v] writes the value [v] of size [size] at address
    81       [addr] in memory [mem]. *)
    82   val store2 : 'fun_def memory -> int -> Value.t -> Value.t ->
     75  val storeq : 'fun_def memory -> quantity -> Value.address -> Value.t ->
    8376               'fun_def memory
     77
     78  (* Globals management *)
    8479
    8580  (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
    … …  
    9388  val add_fun_def : 'fun_def memory -> AST.ident -> 'fun_def -> 'fun_def memory
    9489
     90  val mem_global : 'fun_def memory -> AST.ident -> bool
     91
    9592  (** [find_global mem x] returns the address associated with the global symbol
    9693      [x] in memory [mem]. [x] may be a global variable or the name of a
    9794      function. *)
    98   val find_global : 'fun_def memory -> AST.ident -> Value.t
     95  val find_global : 'fun_def memory -> AST.ident -> Value.address
    9996
    10097  (** [find_fun_def mem addr] returns the function definition found at address
    10198      [addr] in memory [mem]. Raises an error if no function definition is
    10299      found. *)
    103   val find_fun_def : 'fun_def memory -> Value.t -> 'fun_def
     100  val find_fun_def : 'fun_def memory -> Value.address -> 'fun_def
    104101
    105102  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
    … …  
    115112
    116113  val alloc_datas : 'fun_def memory -> AST.data list ->
    117                     ('fun_def memory * Value.t)
     114                    ('fun_def memory * Value.address)
    118115
     116  val to_string : 'fun_def memory -> string
    119117  val print : 'fun_def memory -> unit
    120118

  • Deliverables/D2.2/8051/src/common/primitive.ml

    r486 r740  
    22(** These are the functions provided by the runtime system. *)
    33
    4 let print_int = "print_int"
    5 let print_intln = "print_intln"
     4
     5let error_prefix = "Primitives"
     6let error s = Error.global_error error_prefix s
     7let warning s = Error.warning error_prefix s
     8
     9
     10let print = "print"
     11let println = "println"
    612let scan_int = "scan_int"
    713let alloc = "alloc"
    8 let modulo = "mod"
     14let newline = "newline"
    915
    1016let primitives_list =
    11   [print_int ; print_intln ; scan_int ; alloc ; modulo]
     17  [print ; println ; scan_int ; alloc ; newline]
    1218
    1319let primitives =
    … …  
    1622
    1723let is_primitive f = StringTools.Set.mem f primitives
     24
     25
     26module Interpret (M : Memory.S) = struct
     27
     28  type res = V of M.Value.t | A of M.Value.address
     29
     30  let t mem f = function
     31    | _ when f = scan_int ->
     32      Printf.printf ": %!" ;
     33      (mem, V (M.Value.of_int (int_of_string (read_line ()))))
     34    | v :: _ when f = print ->
     35      Printf.printf "%s%!" (M.Value.to_string v) ;
     36      (mem, V M.Value.zero)
     37    | v :: _ when f = println ->
     38      Printf.printf "%s\n%!" (M.Value.to_string v) ;
     39      (mem, V M.Value.zero)
     40    | v :: _ when f = alloc && M.Value.is_int v ->
     41      let size = M.Value.to_int v in
     42      let (mem, addr) = M.alloc mem size in
     43      (mem, A addr)
     44    | _ when f = newline ->
     45      Printf.printf "\n%!" ;
     46      (mem, V M.Value.zero)
     47    | _ -> error ("unknown primitive " ^ f ^ " or wrong size arguments.")
     48end
    1849
    1950
    … …  
    3566    (print_arg_types sg.AST.args)
    3667    (print_type_return sg.AST.res)
     68
     69let print_prototype =
     70  "extern void print(int);"
     71
     72let println_prototype =
     73  "extern void println(int);"
     74
     75let scan_int_prototype =
     76  "extern int scan_int(void);"
     77
     78let alloc_prototype =
     79  "extern int* alloc(int);"
     80
     81let newline_prototype =
     82  "extern void newline(void);"
     83
     84let prototypes =
     85  let ss =
     86    [print_prototype ; println_prototype ; scan_int_prototype ;
     87     alloc_prototype ; newline_prototype] in
     88  let f res s = res ^ "\n" ^ s in
     89  (List.fold_left f "" ss) ^ "\n\n"

  • Deliverables/D2.2/8051/src/common/primitive.mli

    r486 r740  
    66val is_primitive : string -> bool
    77
    8 val print_int : string
    9 val print_intln : string
     8(* extern void print(int); *)
     9val print : string
     10(* extern void println(int); *)
     11val println : string
     12(* extern int scan_int(void); *)
    1013val scan_int : string
     14(* extern int* alloc(int); *)
    1115val alloc : string
    12 val modulo : string
     16(* extern void newline(void); *)
     17val newline : string
    1318
    1419val print_sig : AST.signature -> string
     20
     21module Interpret (M : Memory.S) : sig
     22  type res = V of M.Value.t | A of M.Value.address
     23  val t : 'a M.memory -> string -> M.Value.t list -> 'a M.memory * res
     24end
     25
     26val prototypes : string

  • Deliverables/D2.2/8051/src/common/value.ml

    r619 r740  
    2121end
    2222
    23 (** This is the signature of the module that provides functions and types to
     23(** This is the signature of the module that provides types and functions to
    2424    manipulate values. *)
    2525
    … …  
    2727sig
    2828
    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. *)
     29  (** The type of values. A value may be: a bounded integer, a chunk of an
     30      address (exactly an address when they have the same size as a machine
     31      register), or undefined. *)
    3732  type t
    3833
    … …  
    5045  val of_int : int -> t
    5146
    52   val is_float : t -> bool
    53   val to_float : t -> float
    54   val of_float : float -> t
    55 
     47  val of_int_repr : IntValue.int_repr -> t
    5648  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
    6249
    6350  val of_bool   : bool -> t
    … …  
    7158  val undef     : t
    7259
    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 
     60  (** The cast operations below returns the undefined value for non-integer
     61      values. For integer values, it will return the integer value that
     62      represents the same quantity, but using every bits (sign or zero
     63      extension) of an integer value. *)
     64  val cast8unsigned  : t -> t
     65  val cast8signed    : t -> t
     66  val cast16unsigned : t -> t
    8067  val cast16signed   : t -> t
    8168  val cast32         : t -> t
    8269
     70  (** [zero_ext v n m] performs a zero extension on [v] where [n] bits are
     71      significant to a value where [m] bits are significant. *)
     72  val zero_ext : t -> int -> int -> t
     73  (** [sign_ext v n m] performs a sign extension on [v] where [n] bits are
     74      significant to a value where [m] bits are significant. *)
     75  val sign_ext : t -> int -> int -> t
     76
    8377  (** Integer opposite *)
    84   val negint        : t -> t
     78  val negint  : t -> t
    8579  (** Boolean negation *)
    86   val notbool       : t -> t
     80  val notbool : t -> t
    8781  (** 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
     82  val notint  : t -> t         
     83
     84  val succ : t -> t
     85  val pred : t -> t
     86  val cmpl : t -> t
    10087
    10188  (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
    … …  
    10693      overflows, and [0] otherwise. *)
    10794  val add_of     : t -> t -> t
    108   (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether
     95  (** [sub_and_uf v1 v2] returns the substraction of [v1] and [v2], and whether
    10996      this substraction underflows. *)
    11097  val sub_and_uf : t -> t -> (t * t)
    11198  val sub        : t -> t -> t
    112   (** [sub_of v1 v2] returns the [1] value if the substraction of [v1] and [v2]
     99  (** [sub_uf v1 v2] returns the [1] value if the substraction of [v1] and [v2]
    113100      underflows, and [0] otherwise. *)
    114101  val sub_uf     : t -> t -> t
    … …  
    124111  val shr        : t -> t -> t
    125112  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
     113
     114  (** Signed comparisions *)
     115  val cmp_eq : t -> t -> t
     116  val cmp_ne : t -> t -> t
     117  val cmp_lt : t -> t -> t
     118  val cmp_ge : t -> t -> t
     119  val cmp_le : t -> t -> t
     120  val cmp_gt : t -> t -> t
    130121
    131122  (** 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
     123  val cmp_eq_u : t -> t -> t
     124  val cmp_ne_u : t -> t -> t
     125  val cmp_lt_u : t -> t -> t
     126  val cmp_ge_u : t -> t -> t
     127  val cmp_le_u : t -> t -> t
     128  val cmp_gt_u : t -> t -> t
     129
     130  (** A chunk is a part of a value that has the size of a memory cell. *)
     131
     132  type chunk
     133  val string_of_chunk : chunk -> string
     134  val undef_byte : chunk
     135  val is_undef_byte : chunk -> bool
     136
     137  (** [break v] cuts [v] in chunks that each fits into a memory cell. In the
     138      resulting list, the first element is the low bits, and the last is the
     139      high bits (little endian representation). *)
     140  val break : t -> chunk list
     141  (** [merge l] creates the value where the first element of [l] is its low
     142      bits, etc, and the last element of [l] is its high bits (little endian
     143      representation). *)
     144  val merge : chunk list -> t
     145
     146  (** Addresses from the memory point of view. *)
     147
     148  (** Some architectures have pointers bigger than integers. In this case, only
     149      a chunk of pointer can fit into a machine register. Thus, an address is
     150      represented by several values (little endian representation). *)
     151
     152  type address = t list
     153  val string_of_address : address -> string
     154  val null : address
     155
     156  (** Addresses from the memory point of view. Only use the functions below in
     157      the Memory module.*)
     158
     159  (** Addresses are represented by a block, i.e. a base address, and an offset
     160      from this block. Both blocks and offsets are represented using bounded
     161      integers. *)
     162  module Block  : IntValue.S
     163  module Offset : IntValue.S
     164
     165  type mem_address
     166
     167  val is_mem_address : address -> bool
     168
     169  val of_mem_address        : mem_address -> address
     170  val to_mem_address        : address -> mem_address
     171  val make_mem_address      : Block.t -> Offset.t -> mem_address
     172  val decompose_mem_address : mem_address -> Block.t * Offset.t
     173  val block_of_address      : address -> Block.t
     174  val offset_of_address     : address -> Offset.t
     175
     176  val change_address_offset : address -> Offset.t -> address
     177  val add_address           : address -> Offset.t -> address
     178  val eq_address            : address -> address -> bool
    159179
    160180end
    … …  
    164184struct
    165185
    166   (* This module will be used to represent integer values. *)
    167   module Int =
    168     IntValue.Make (struct let size = D.int_size end)
     186  (* Integer values. *)
     187  module ValInt = IntValue.Make (struct let size = D.int_size end)
    169188
    170189  (* Addresses are represented by a block, i.e. a base address, and an offset
    171190     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. *)
     191     integers. However, values must fit into a machine register. Some
     192     architectures, like the 8051, have addresses bigger than registers. Pointer
     193     values will only represent a part of a full pointer (or exactly a pointer
     194     when addresses fit into a register). *)
     195
     196  (* Blocks and offsets need [D.ptr_size] bits each to be represented. Indeed,
     197     one may allocate 2^[D.ptr_size] blocks of size one byte, or one block of
     198     size 2^[D.ptr_size] bytes. *)
     199
     200  module ValBlock  = IntValue.Make (struct let size = D.int_size end)
     201  module ValOffset = IntValue.Make (struct let size = D.int_size end)
    193202
    194203  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
     204    | Val_int of ValInt.t
     205    | Val_ptr of ValBlock.t * ValOffset.t
    200206    | Val_undef
    201207
    202208  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
     209    | Val_int i1, Val_int i2 -> ValInt.compare i1 i2
     210    | Val_ptr (b1, off1), Val_ptr (b2, off2) ->
     211      let i1 = ValBlock.compare b1 b2 in
     212      if i1 = 0 then ValOffset.compare off1 off2
    210213      else i1
    211214    | Val_undef, Val_undef -> 0
    212215    | Val_int _, _ -> 1
    213216    | _, Val_int _ -> -1
    214     | Val_float _, _ -> 1
    215     | _, Val_float _ -> -1
    216217    | Val_ptr _, _ -> 1
    217218    | _, 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
     219
     220  (*
     221    let hash = function
     222    | Val_int i -> ValInt.to_int i
    226223    | Val_float f -> int_of_float f
    227224    | Val_undef -> 0
    228225    | Val_ptr (b,o)
    229226    | Val_ptrh (b,o)
    230     | Val_ptrl (b,o) -> Int.to_int (Int.add b o)
    231 *)
     227    | Val_ptrl (b,o) -> ValInt.to_int (ValInt.add b o)
     228  *)
    232229
    233230  let hash = Hashtbl.hash
    … …  
    237234
    238235  let to_string = function
    239     | Val_int i -> Int.to_string i
    240     | Val_float f -> string_of_float f
     236    | Val_int i -> ValInt.to_string i
    241237    | 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) ^ ")"
     238      "VPtr(" ^ (ValBlock.to_string b) ^ ", " ^ (ValOffset.to_string off) ^ ")"
    247239    | Val_undef -> "undef"
    248240
    … …  
    252244
    253245  let to_int = function
    254     | Val_int i -> Int.to_int i
     246    | Val_int i -> ValInt.to_int i
    255247    | _ -> raise (Failure "Value.to_int")
    256248
    257   let of_int i = Val_int (Int.of_int i)
     249  let of_int i = Val_int (ValInt.of_int i)
     250  let one = of_int 1
     251
     252  let of_int_repr i = Val_int i
    258253
    259254  let to_int_repr = function
    … …  
    261256    | _ -> raise (Failure "Value.to_int_repr")
    262257
    263   let of_int_repr i = Val_int i
    264 
    265   let is_pointer = function
    266     | Val_ptr _ -> true
     258  let zero      = Val_int ValInt.zero
     259  let val_true  = Val_int ValInt.one
     260  let val_false = Val_int ValInt.zero
     261
     262  let is_true = function
     263    | Val_int i -> ValInt.neq i ValInt.zero
     264    | Val_ptr (b, off) ->
     265      (ValBlock.neq b ValBlock.zero) || (ValOffset.neq off ValOffset.zero)
    267266    | _ -> false
    268267
    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
     268  let is_false = function
     269    | Val_int i -> ValInt.eq i ValInt.zero
     270    | Val_ptr (b, off) ->
     271      (ValBlock.eq b ValBlock.zero) && (ValOffset.eq off ValOffset.zero)
    277272    | _ -> false
    278273
    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 
    300274  let of_bool = function
    301     | true -> Val_int Int.one
    302     | false -> Val_int Int.zero
     275    | true -> val_true
     276    | false -> val_false
    303277
    304278  let to_bool v =
    … …  
    315289
    316290  (** 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)
     291  let cast8unsigned = cast (ValInt.zero_ext 8)
     292  let cast8signed = cast (ValInt.sign_ext 8)
     293  let cast16unsigned = cast (ValInt.zero_ext 16)
     294  let cast16signed = cast (ValInt.sign_ext 16)
     295  let cast32 = cast (ValInt.zero_ext 32)
    322296
    323297
    … …  
    330304    | _ -> Val_undef
    331305
    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
     306  let negint = unary_int_op ValInt.neg
    346307
    347308  let notbool v =
    … …  
    351312      else Val_undef
    352313
    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 *)
     314  let notint = unary_int_op ValInt.lognot
     315
     316  let cmpl = unary_int_op ValInt.lognot
    388317
    389318  (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
    … …  
    391320  let add_and_of v1 v2 = match v1, v2 with
    392321    | Val_int i1, Val_int i2 ->
    393       (Val_int (Int.add i1 i2), of_bool (Int.add_of i1 i2))
     322      (Val_int (ValInt.add i1 i2), of_bool (ValInt.add_of i1 i2))
    394323    | Val_int i, Val_ptr (b, off)
    395324    | 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)))
     325      let i = ValOffset.cast i in
     326      (Val_ptr (b, ValOffset.add off i), of_bool (ValOffset.add_of off i))
    406327    | _, _ -> (Val_undef, Val_undef)
    407328
    … …  
    409330  let add_of v1 v2 = snd (add_and_of v1 v2)
    410331
    411   let succ v = add v (Val_int Int.one)
     332  let succ v = add v (Val_int ValInt.one)
    412333
    413334  (** [sub_and_uf v1 v2] returns the substraction of [v1] and [v2], and whether
    … …  
    415336  let sub_and_uf v1 v2 = match v1, v2 with
    416337    | Val_int i1, Val_int i2 ->
    417       (Val_int (Int.sub i1 i2), of_bool (Int.sub_uf i1 i2))
     338      (Val_int (ValInt.sub i1 i2), of_bool (ValInt.sub_uf i1 i2))
    418339    | 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))
     340      let i = ValOffset.cast i in
     341      (Val_ptr (b, ValOffset.sub off i), of_bool (ValOffset.sub_uf off i))
     342    | Val_ptr (b1, off1), Val_ptr (b2, off2) when ValBlock.eq b1 b2 ->
     343      (Val_int (ValInt.cast (ValOffset.sub off1 off2)),
     344       of_bool (ValOffset.sub_uf off1 off2))
    432345    | _, _ -> (Val_undef, Val_undef)
    433346
    … …  
    435348  let sub_uf v1 v2 = snd (sub_and_uf v1 v2)
    436349
    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
     350  let pred v = sub v (Val_int ValInt.one)
     351
     352  let mul = binary_int_op ValInt.mul
    442353
    443354  let is_zero = function
    444     | Val_int i when Int.eq i Int.zero -> true
     355    | Val_int i when ValInt.eq i ValInt.zero -> true
    445356    | _ -> false
    446357
    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
     358  let error_if_zero op v1 v2 =
     359    if is_zero v2 then error "Division by zero."
     360    else binary_int_op op v1 v2
     361
     362  let div     = error_if_zero ValInt.div
     363  let divu    = error_if_zero ValInt.divu
     364  let modulo  = error_if_zero ValInt.modulo
     365  let modulou = error_if_zero ValInt.modulou
     366
     367  let and_op = binary_int_op ValInt.logand
     368  let or_op  = binary_int_op ValInt.logor
     369  let xor    = binary_int_op ValInt.logxor
     370  let shl    = binary_int_op ValInt.shl
     371  let shr    = binary_int_op ValInt.shr
     372  let shru   = binary_int_op ValInt.shrl
     373
     374  let ext sh v n m =
     375    let real_size = D.int_size * 8 in
     376    let int_sh sh v n = sh v (of_int n) in
     377    if n >= m then
     378      if m = real_size then v
     379      else modulou v (shl one (of_int m))
     380    else
     381      let v = int_sh shl v (real_size - n) in
     382      let v = int_sh sh v (m - n) in
     383      int_sh shru v (real_size - m)
     384
     385  let zero_ext = ext shru
     386  let sign_ext = ext shr
     387
     388  let cmp f_int f_off v1 v2 = match v1, v2 with
     389    | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2)
     390    | Val_ptr (b1, off1), Val_ptr (b2, off2) when ValBlock.eq b1 b2 ->
     391      of_bool (f_off off1 off2)
    483392    | _ -> Val_undef
    484393
    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
     394  let cmp_eq = cmp ValInt.eq ValOffset.eq
     395  let cmp_ne = cmp ValInt.neq ValOffset.neq
     396  let cmp_lt = cmp ValInt.lt ValOffset.lt
     397  let cmp_ge = cmp ValInt.ge ValOffset.ge
     398  let cmp_le = cmp ValInt.le ValOffset.le
     399  let cmp_gt = cmp ValInt.gt ValOffset.gt
     400
     401  let cmp_eq_u = cmp ValInt.eq ValOffset.eq
     402  let cmp_ne_u = cmp ValInt.neq ValOffset.neq
     403  let cmp_lt_u = cmp ValInt.ltu ValOffset.ltu
     404  let cmp_ge_u = cmp ValInt.geu ValOffset.geu
     405  let cmp_le_u = cmp ValInt.leu ValOffset.leu
     406  let cmp_gt_u = cmp ValInt.gtu ValOffset.gtu
     407
     408
     409  (* The memory is based on byte values. In order to be able to fit a bigger
     410     integer or pointer value in memory, we need to be able to break this value
     411     into several values of size a byte. An integer will be broken into multiple
     412     8 bits integers. A pointer will be broken into several couples of 8 bits
     413     blocks and 8 bits offsets. *)
     414
     415  (* 8 bits integers *)
     416  module IntChunk = IntValue.Int8
     417  (* 8 bits blocks *)
     418  module BlockChunk = IntValue.Int8
     419  (* 8 bits offsets *)
     420  module OffsetChunk = IntValue.Int8
     421
     422  (** A chunk is a part of a value that has the size of a memory cell. *)
     423
     424  type chunk =
     425    | Byte_int of IntChunk.t
     426    | Byte_ptr of BlockChunk.t * OffsetChunk.t
     427    | Byte_undef
     428
     429  let string_of_chunk = function
     430    | Byte_int i -> IntChunk.to_string i
     431    | Byte_ptr (b, off) ->
     432      "BPtr(" ^ (BlockChunk.to_string b) ^ ", " ^
     433      (OffsetChunk.to_string off) ^ ")"
     434    | Byte_undef -> "Bundef"
     435
     436  let undef_byte = Byte_undef
     437
     438  let is_undef_byte = function
     439    | Byte_undef -> true
     440    | _ -> false
     441
     442  let break_and_cast break cast x n =
     443    let ys = break x n in
     444    List.map cast ys
     445
     446  (** [break v] cuts [v] in chunks that each fits into a memory cell. In the
     447      resulting list, the first element is the low bits, and the last is the
     448      high bits (little endian representation). *)
     449  let break v =
     450    let nb_chunks = D.int_size in
     451    match v with
     452      | Val_ptr (b, off) ->
     453        let bbs = break_and_cast ValBlock.break BlockChunk.cast b nb_chunks in
     454        let boffs =
     455          break_and_cast ValOffset.break OffsetChunk.cast off nb_chunks in
     456        List.map2 (fun bb boff -> Byte_ptr (bb, boff)) bbs boffs
     457      | Val_int i ->
     458        let bis = break_and_cast ValInt.break IntChunk.cast i nb_chunks in
     459        List.map (fun i' -> Byte_int i') bis
     460      | _ -> MiscPottier.make Byte_undef nb_chunks
     461
     462  (** [all_are_pointers l] returns [true] iff the values in the list [l] all are
     463      pointers. *)
     464  let all_are_pointers =
     465    let f b v = b && (match v with Byte_ptr _ -> true | _ -> false) in
     466    List.fold_left f true
     467
     468  (** [all_are_integers l] returns [true] iff the values in the list [l] all are
    529469      integers. *)
    530470  let all_are_integers =
    531     let f b v = b && (match v with Val_int _ -> true | _ -> false) in
     471    let f b v = b && (match v with Byte_int _ -> true | _ -> false) in
    532472    List.fold_left f true
    533473
    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. *)
     474  let bblock_of_chunk = function
     475    | Byte_ptr (b, _) -> b
     476    | _ -> assert false (* do not use on this argument *)
     477
     478  let boffset_of_chunk = function
     479    | Byte_ptr (_, off) -> off
     480    | _ -> assert false (* do not use on this argument *)
     481
     482  let bint_of_chunk = function
     483    | Byte_int i -> i
     484    | _ -> assert false (* do not use on this argument *)
     485
     486  let cast_and_merge cast merge transform l =
     487    merge (List.map (fun x -> cast (transform x)) l)
     488
     489  (** [merge l] creates the value where the first element of [l] is its low
     490      bits, etc, and the last element of [l] is its high bits (little endian
     491      representation). *)
    543492  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))
     493    | l when all_are_pointers l ->
     494      let b = cast_and_merge ValBlock.cast ValBlock.merge bblock_of_chunk l in
     495      let off =
     496        cast_and_merge ValOffset.cast ValOffset.merge boffset_of_chunk l in
     497      Val_ptr (b, off)
     498    | l when all_are_integers l ->
     499      Val_int (cast_and_merge ValInt.cast ValInt.merge bint_of_chunk l)
    549500    | _ -> Val_undef
    550501
     502
     503  (** Addresses from the memory point of view. *)
     504
     505  (** Some architectures have pointers bigger than integers. In this case, only
     506      a chunk of pointer can fit into a machine register. Thus, an address is
     507      represented by several values (little endian representation). *)
     508
     509  type address = t list
     510
     511  let string_of_address vs =
     512    "[" ^ (MiscPottier.string_of_list " " to_string vs) ^ "]"
     513
     514
     515  (** Addresses are represented by a block, i.e. a base address, and an offset
     516      from this block. Both blocks and offsets are represented using bounded
     517      integers. *)
     518
     519  let ptr_int_size = max (D.ptr_size / D.int_size) 1
     520
     521  module Block  = IntValue.Make (struct let size = D.ptr_size end)
     522  module Offset = IntValue.Make (struct let size = D.ptr_size end)
     523
     524  type mem_address = Block.t * Offset.t
     525
     526  let is_mem_address =
     527    let f b v = b && (match v with | Val_ptr _ -> true | _ -> false) in
     528    List.fold_left f true
     529
     530  let of_mem_address (b, off) =
     531    let bs = Block.break b ptr_int_size in
     532    let offs = Offset.break off ptr_int_size in
     533    let f b off = Val_ptr (ValBlock.cast b, ValOffset.cast off) in
     534    List.map2 f bs offs
     535
     536  let decompose_Val_ptr = function
     537    | Val_ptr (b, off) -> (b, off)
     538    | _ -> error "Not an address."
     539
     540  let to_mem_address vs =
     541    let (bs, offs) = List.split (List.map decompose_Val_ptr vs) in
     542    let b = Block.merge (List.map Block.cast bs) in
     543    let off = Offset.merge (List.map Offset.cast offs) in
     544    (b, off)
     545
     546  let make_mem_address b off = (b, off)
     547  let decompose_mem_address addr = addr
     548  let block_of_address vs = fst (to_mem_address vs)
     549  let offset_of_address vs = snd (to_mem_address vs)
     550
     551  let null = of_mem_address (Block.zero, Offset.zero)
     552
     553  let change_address_offset vs off =
     554    let (b, _) = decompose_mem_address (to_mem_address vs) in
     555    of_mem_address (make_mem_address b off)
     556
     557  let add_address vs off' =
     558    let (b, off) = decompose_mem_address (to_mem_address vs) in
     559    let off = Offset.add off off' in
     560    of_mem_address (make_mem_address b off)
     561
     562  let eq_address addr1 addr2 =
     563    let f b v1 v2 = b && (eq v1 v2) in
     564    List.fold_left2 f true addr1 addr2
     565
    551566end

  • Deliverables/D2.2/8051/src/common/value.mli

    r619 r740  
    11
    2 (** This module describes the values manipulated by high level
    3     languages. *)
     2(** This module describes the values manipulated by high level languages. *)
    43
    54(** The representation of values depends on the size of integers and the size of
    … …  
    1413end
    1514
    16 (** This is the signature of the module that provides functions and types to
     15(** This is the signature of the module that provides types and functions to
    1716    manipulate values. *)
    1817
    … …  
    2019sig
    2120
    22   (** Addresses are represented by a block, i.e. a base address, and an offset
    23       from this block. Both blocks and offsets are represented using bounded
    24       integers. *)
    25   module Block  : IntValue.S
    26   module Offset : IntValue.S
    27 
    28   (** The type of values. A value may be: a bounded integer, a float (though
    29       they are not fully supported), an address, or undefined. *)
     21  (** The type of values. A value may be: a bounded integer, a chunk of an
     22      address (exactly an address when they have the same size as a machine
     23      register), or undefined. *)
    3024  type t
    3125
    … …  
    4337  val of_int : int -> t
    4438
    45   val is_float : t -> bool
    46   val to_float : t -> float
    47   val of_float : float -> t
    48 
     39  val of_int_repr : IntValue.int_repr -> t
    4940  val to_int_repr : t -> IntValue.int_repr
    50   val of_int_repr : IntValue.int_repr -> t
    51 
    52   val is_pointer : t -> bool
    53   val to_pointer : t -> Block.t * Offset.t
    54   val of_pointer : Block.t * Offset.t -> t
    5541
    5642  val of_bool   : bool -> t
    … …  
    6450  val undef     : t
    6551
    66 
    67   (** Sign or 0 extensions from various bounded integers. *)
    68   val cast8unsigned  : t -> t
    69   val cast8signed    : t -> t   
    70   val cast16unsigned : t -> t
     52  (** The cast operations below returns the undefined value for non-integer
     53      values. For integer values, it will return the integer value that
     54      represents the same quantity, but using every bits (sign or zero
     55      extension) of an integer value. *)
     56  val cast8unsigned  : t -> t
     57  val cast8signed    : t -> t
     58  val cast16unsigned : t -> t
    7159  val cast16signed   : t -> t
    7260  val cast32         : t -> t
    7361
     62  (** [zero_ext v n m] performs a zero extension on [v] where [n] bits are
     63      significant to a value where [m] bits are significant. *)
     64  val zero_ext : t -> int -> int -> t
     65  (** [sign_ext v n m] performs a sign extension on [v] where [n] bits are
     66      significant to a value where [m] bits are significant. *)
     67  val sign_ext : t -> int -> int -> t
     68
    7469  (** Integer opposite *)
    75   val negint        : t -> t
     70  val negint  : t -> t
    7671  (** Boolean negation *)
    77   val notbool       : t -> t
     72  val notbool : t -> t
    7873  (** Bitwise not *)
    79   val notint        : t -> t         
    80   val negf          : t -> t           
    81   val absf          : t -> t           
    82   val singleoffloat : t -> t 
    83   val intoffloat    : t -> t     
    84   val intuoffloat   : t -> t   
    85   val floatofint    : t -> t     
    86   val floatofintu   : t -> t   
     74  val notint  : t -> t         
    8775
    88   val succ       : t -> t
    89   val pred       : t -> t
    90   val cmpl       : t -> t
     76  val succ : t -> t
     77  val pred : t -> t
     78  val cmpl : t -> t
    9179
    9280  (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
    … …  
    9785      overflows, and [0] otherwise. *)
    9886  val add_of     : t -> t -> t
    99   (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether
     87  (** [sub_and_uf v1 v2] returns the substraction of [v1] and [v2], and whether
    10088      this substraction underflows. *)
    10189  val sub_and_uf : t -> t -> (t * t)
    10290  val sub        : t -> t -> t
    103   (** [sub_of v1 v2] returns the [1] value if the substraction of [v1] and [v2]
     91  (** [sub_uf v1 v2] returns the [1] value if the substraction of [v1] and [v2]
    10492      underflows, and [0] otherwise. *)
    10593  val sub_uf     : t -> t -> t
    … …  
    115103  val shr        : t -> t -> t
    116104  val shru       : t -> t -> t
    117   val addf       : t -> t -> t
    118   val subf       : t -> t -> t
    119   val mulf       : t -> t -> t
    120   val divf       : t -> t -> t
     105
     106  (** Signed comparisions *)
     107  val cmp_eq : t -> t -> t
     108  val cmp_ne : t -> t -> t
     109  val cmp_lt : t -> t -> t
     110  val cmp_ge : t -> t -> t
     111  val cmp_le : t -> t -> t
     112  val cmp_gt : t -> t -> t
    121113
    122114  (** Unsigned comparisions *)
    123   val cmp_eq_u : t -> t -> t 
    124   val cmp_ne_u : t -> t -> t 
    125   val cmp_lt_u : t -> t -> t 
    126   val cmp_ge_u : t -> t -> t 
    127   val cmp_le_u : t -> t -> t 
    128   val cmp_gt_u : t -> t -> t 
     115  val cmp_eq_u : t -> t -> t
     116  val cmp_ne_u : t -> t -> t
     117  val cmp_lt_u : t -> t -> t
     118  val cmp_ge_u : t -> t -> t
     119  val cmp_le_u : t -> t -> t
     120  val cmp_gt_u : t -> t -> t
    129121
    130   val cmp_eq_f : t -> t -> t 
    131   val cmp_ne_f : t -> t -> t 
    132   val cmp_lt_f : t -> t -> t 
    133   val cmp_ge_f : t -> t -> t 
    134   val cmp_le_f : t -> t -> t 
    135   val cmp_gt_f : t -> t -> t
     122  (** A chunk is a part of a value that has the size of a memory cell. *)
    136123
    137   val cmp_eq : t -> t -> t 
    138   val cmp_ne : t -> t -> t 
    139   val cmp_lt : t -> t -> t 
    140   val cmp_ge : t -> t -> t 
    141   val cmp_le : t -> t -> t 
    142   val cmp_gt : t -> t -> t
     124  type chunk
     125  val string_of_chunk : chunk -> string
     126  val undef_byte : chunk
     127  val is_undef_byte : chunk -> bool
    143128
    144   (** [break v n] cuts [v] in [n] parts. In the resulting list, the first
    145       element is the high bits, and the last is the low bits. *)
    146   val break : t -> int -> t list
    147   (** [merge l] creates the value where the first element of [l] is its
    148       high bits, etc, and the last element of [l] is its low bits. *)
    149   val merge : t list -> t
     129  (** [break v] cuts [v] in chunks that each fits into a memory cell. In the
     130      resulting list, the first element is the low bits, and the last is the
     131      high bits (little endian representation). *)
     132  val break : t -> chunk list
     133  (** [merge l] creates the value where the first element of [l] is its low
     134      bits, etc, and the last element of [l] is its high bits (little endian
     135      representation). *)
     136  val merge : chunk list -> t
     137
     138  (** Addresses from interpreters point of view. *)
     139
     140  (** Some architectures have pointers bigger than integers. In this case, only
     141      a chunk of pointer can fit into a machine register. Thus, an address is
     142      represented by several values (little endian representation). *)
     143
     144  type address = t list
     145  val string_of_address : address -> string
     146  val null : address
     147
     148  (** Addresses from the memory point of view. *)
     149
     150  (** Addresses are represented by a block, i.e. a base address, and an offset
     151      from this block. Both blocks and offsets are represented using bounded
     152      integers. *)
     153  module Block  : IntValue.S
     154  module Offset : IntValue.S
     155
     156  type mem_address
     157
     158  val is_mem_address : address -> bool
     159
     160  val of_mem_address        : mem_address -> address
     161  val to_mem_address        : address -> mem_address
     162  val make_mem_address      : Block.t -> Offset.t -> mem_address
     163  val decompose_mem_address : mem_address -> Block.t * Offset.t
     164  val block_of_address      : address -> Block.t
     165  val offset_of_address     : address -> Offset.t
     166
     167  val change_address_offset : address -> Offset.t -> address
     168  val add_address           : address -> Offset.t -> address
     169  val eq_address            : address -> address -> bool
    150170
    151171end
Note: See TracChangeset for help on using the changeset viewer.