Ignore:
Timestamp:
May 19, 2011, 4:03:04 PM (9 years ago)
Author:
ayache
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/common/memory.ml

    r740 r818  
    1111
    1212
    13 (** Memory quantities is the size and type of what can be loaded or stored in
    14     memory. *)
    15 
    16 type quantity =
    17   | QInt of int (* Sized integer *)
    18   | QPtr        (* Pointer *)
    19 
    2013let string_of_quantity = function
    21   | QInt i -> string_of_int i
    22   | QPtr -> "ptr"
     14  | AST.QInt i -> "int" ^ (string_of_int (i*8))
     15  | AST.QOffset -> "offset"
     16  | AST.QPtr -> "ptr"
    2317
    2418
    2519let size_of_data = function
     20(*
    2621  | AST.Data_reserve n -> n
     22*)
    2723  | AST.Data_int8 _ -> 1
    2824  | AST.Data_int16 _ -> 2
     
    3026  | AST.Data_float32 _ -> 4
    3127  | AST.Data_float64 _ -> 8
     28
     29
     30let rec all_offsets size = match size with
     31  | AST.SQ _ -> [[]]
     32  | AST.SProd sizes ->
     33    let fi i offsets = (size, i) :: offsets in
     34    let f i size = List.map (fi i) (all_offsets size) in
     35    List.flatten (MiscPottier.mapi f sizes)
     36  | AST.SSum _ -> [[(size, 0)]]
     37  | AST.SArray (n, size') ->
     38    let all_offsets = all_offsets size' in
     39    let f i = List.map (fun offsets -> (size, i) :: offsets) all_offsets in
     40    let rec aux i =
     41      if i >= n then []
     42      else (f i) @ (aux (i+1)) in
     43    aux 0
    3244
    3345
     
    5264  val alignment : int option
    5365
    54   val size_of_quantity : quantity -> int
     66  val size_of_quantity : AST.quantity -> int
    5567
    5668  module Value : Value.S
     
    8193      [mem] and returns the value found. *)
    8294  val load : 'fun_def memory -> int -> Value.address -> Value.t
    83   val loadq : 'fun_def memory -> quantity -> Value.address -> Value.t
     95  val loadq : 'fun_def memory -> AST.quantity -> Value.address -> Value.t
    8496
    8597  (** [store mem size addr v] writes the [size] first bytes (little endian
     
    8799  val store  : 'fun_def memory -> int -> Value.address -> Value.t ->
    88100               'fun_def memory
    89   val storeq : 'fun_def memory -> quantity -> Value.address -> Value.t ->
     101  val storeq : 'fun_def memory -> AST.quantity -> Value.address -> Value.t ->
    90102               'fun_def memory
    91103
    92104  (* Globals management *)
    93105
    94   (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
    95       memory [mem], and associates the global variable [x] with the address of
    96       the block. *)
    97   val add_var : 'fun_def memory -> AST.ident -> AST.data list -> 'fun_def memory
     106  (** [add_var mem x offsets init_datas] stores the datas [init_datas] of
     107      offsets [offsets] in a new block of memory [mem], and associates the
     108      global variable [x] with the address of the block. *)
     109  val add_var :
     110    'fun_def memory -> AST.ident -> AST.abstract_size -> AST.data list option ->
     111    'fun_def memory
    98112
    99113  (** [add_fun_def mem f def] stores the function definition [def] in a new
     
    114128  val find_fun_def : 'fun_def memory -> Value.address -> 'fun_def
    115129
    116   (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
    117       of size [sizes]. *)
    118   val align : int (* starting offset *) -> int list (* sizes *) ->
     130
     131  (** [align off size] returns the aligned offsets (starting at [off]) of datas
     132      of size [size]. *)
     133  val align : int (* starting offset *) -> AST.abstract_size (* sizes *) ->
    119134              (int list (* resulting offsets *) * int (* full size *))
    120135
     136  val concrete_offsets_size : AST.abstract_size -> int list * int
     137
     138  val concrete_offsets : AST.abstract_size -> int list
     139
     140  val concrete_size : AST.abstract_size -> int
     141
     142  val concrete_offset : AST.abstract_offset -> int
     143
     144(*
    121145  val size_of_datas : AST.data list -> int
    122146
     
    127151  val alloc_datas : 'fun_def memory -> AST.data list ->
    128152                    ('fun_def memory * Value.address)
     153*)
    129154
    130155  val to_string : 'fun_def memory -> string
     
    151176
    152177  let size_of_quantity = function
    153     | QInt i -> i
    154     | QPtr -> ptr_size
     178    | AST.QInt i -> i
     179    | AST.QOffset -> int_size
     180    | AST.QPtr -> ptr_size
    155181
    156182
     
    176202  let is_multiple n m = m mod n = 0
    177203
    178   (** [align off size] returns the offset greater or equal to [off] that is
     204  (** [align_off off size] returns the offset greater or equal to [off] that is
    179205      aligned for storing a value of size [size]. *)
    180   let align off size = match D.alignment with
     206  let align_off off size = match D.alignment with
    181207    | None -> off
    182208    | Some alignment when (size <= alignment) && (is_multiple size alignment) ->
     
    191217      else Offset.add off (Offset.sub size rem)
    192218
    193   let is_aligned off size = Offset.eq off (align off size)
     219  let is_aligned off size = Offset.eq off (align_off off size)
    194220
    195221  (** [pad off] returns the offset that is obtained by adding some padding from
     
    197223  let pad off = match D.alignment with
    198224    | None -> off
    199     | Some alignment -> align off alignment
    200 
    201   (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
    202       of size [sizes]. *)
    203   let align off sizes =
    204     let rec aux (acc_offs, acc_size) off = function
    205       | [] ->
    206         let end_off = pad off in
    207         let added_size = Offset.sub end_off off in
    208         let added_size = Offset.to_int added_size in
    209         (acc_offs, acc_size + added_size)
    210       | size :: sizes ->
    211         let aligned_off = align off size in
    212         let next_off = Offset.add aligned_off (Offset.of_int size) in
    213         let added_size = Offset.sub next_off off in
    214         let added_size = Offset.to_int added_size in
    215         let acc = (acc_offs @ [aligned_off], acc_size + added_size) in
    216         aux acc next_off sizes
    217     in
    218     aux ([], 0) off sizes
     225    | Some alignment -> align_off off alignment
     226
     227  (** [pad_size off size] returns the offset that is obtained by adding [size]
     228      to the offset [off] and then adding some extra padding such that the
     229      result is aligned. *)
     230  let pad_size off size =
     231    Offset.to_int (pad (Offset.add off (Offset.of_int size)))
    219232
    220233
     
    405418
    406419  let value_of_data = function
     420(*
    407421    | AST.Data_reserve _ -> Value.undef
     422*)
    408423    | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i -> Value.of_int i
    409424    | AST.Data_float32 f | AST.Data_float64 f -> error "float not supported."
    410425
    411   let offsets_size_of_datas datas =
    412     align Offset.zero (List.map size_of_data datas)
    413 
    414   (** [alloc_datas mem datas] returns the memory and the address obtained by
    415       allocating space and storing the datas [datas] in the memory [mem]. *)
    416   let alloc_datas mem datas =
    417     let msg = "cannot allocate datas." (* TODO *) in
    418     let (offs_of_datas, size) = offsets_size_of_datas datas 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
    425     let f mem data off = match data with
    426       | AST.Data_reserve _ -> mem
    427       | _ -> store mem (size_of_data data) (shift_addr off) (value_of_data data)
    428     in
    429     (List.fold_left2 f mem datas offs_of_datas, vs)
    430 
    431   let size_of_datas datas = snd (offsets_size_of_datas datas)
    432 
    433   (** [offsets_of_datas datas] returns the aligned offsets for the datas
    434       [datas], starting at offset 0. *)
    435   let offsets_of_datas datas =
    436     let (offs_of_datas, _) = offsets_size_of_datas datas in
    437     List.combine datas (List.map Offset.to_int offs_of_datas)
    438 
    439   (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
    440       of size [sizes]. *)
    441   let align off sizes =
    442     let (offsets, size) = align (Offset.of_int off) sizes in
    443     (List.map Offset.to_int offsets, size)
     426  type concrete_size =
     427    | I of Offset.t
     428    | C of concrete_size list
     429
     430  let rec first_offset = function
     431    | I off -> off
     432    | C [] -> raise (Failure "Memory.first_offset")
     433    | C (csize :: _) -> first_offset csize
     434
     435  let first_offsets = function
     436    | I off -> [off]
     437    | C sizes -> List.map first_offset sizes
     438
     439  let rec all_offsets = function
     440    | I off -> [off]
     441    | C sizes -> List.flatten (List.map all_offsets sizes)
     442
     443  let rec full_align off = function
     444
     445    | AST.SQ q ->
     446      let size = size_of_quantity q in
     447      let start_off = align_off off size in
     448      let diff = Offset.to_int (Offset.sub start_off off) in
     449      let full_size = size + diff in
     450      (I start_off, full_size)
     451
     452    | AST.SProd sizes ->
     453      let f (l, off) size =
     454        let (csize, added_size) = full_align off size in
     455        (l @ [csize], Offset.add off (Offset.of_int added_size)) in
     456      let start_off = pad off in
     457      let (l, end_off) = List.fold_left f ([], start_off) sizes in
     458      let end_off = pad end_off in
     459      let full_size = Offset.to_int (Offset.sub end_off off) in
     460      (C l, full_size)
     461
     462    | AST.SSum sizes ->
     463      let start_off = pad off in
     464      let sizes =
     465        List.map (fun size -> snd (full_align start_off size)) sizes in
     466      let max = Offset.of_int (MiscPottier.max_list sizes) in
     467      let end_off = pad (Offset.add start_off max) in
     468      let full_size = Offset.to_int (Offset.sub end_off off) in
     469      (I start_off, full_size)
     470
     471    | AST.SArray (n, size) ->
     472      let sizes = MiscPottier.make size n in
     473      full_align off (AST.SProd sizes)
     474
     475  let align off size =
     476    let (offsets, full_size) = full_align (Offset.of_int off) size in
     477    (List.map Offset.to_int (first_offsets offsets), full_size)
     478
     479  let concrete_offsets_size = align 0
     480
     481  let concrete_offsets size = fst (concrete_offsets_size size)
     482
     483  let concrete_size size = snd (concrete_offsets_size size)
     484
     485  let concrete_offset (size, depth) =
     486    let offsets = concrete_offsets size in
     487    List.nth offsets depth
    444488
    445489
    446490  (* Globals manipulation *)
    447491
    448   (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
    449       memory [mem], and associates the global variable [x] with the address of
    450       the block. *)
    451   let add_var mem v_id datas =
    452     let (mem, vs) = alloc_datas mem datas in
    453     let addr_of_global = GlobalMap.add v_id vs mem.addr_of_global in
     492  let store_datas_opt mem addr offsets = function
     493    | None -> mem
     494    | Some datas ->
     495      let f mem (offset, data) =
     496        let addr = Value.add_address addr offset in
     497        store mem (size_of_data data) addr (value_of_data data) in
     498      let offsets = all_offsets offsets in
     499      if List.length offsets <> List.length datas then
     500        error "wrong sizes for global initializations (union type?)."
     501      else
     502        let offset_datas = List.combine offsets datas in
     503        List.fold_left f mem offset_datas
     504
     505  (** [add_var mem x size init_datas] stores the datas [init_datas] of offsets
     506      [size] in a new block of memory [mem], and associates the global variable
     507      [x] with the address of the block. *)
     508  let add_var mem v_id size datas_opt =
     509    let (offsets, size) = full_align Offset.zero size in
     510    let (mem, addr) = alloc mem size in
     511    let mem = store_datas_opt mem addr offsets datas_opt in
     512    let addr_of_global = GlobalMap.add v_id addr mem.addr_of_global in
    454513    { mem with addr_of_global = addr_of_global }
    455514
Note: See TracChangeset for help on using the changeset viewer.