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

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

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/common/AST.mli

    r619 r818  
    11
    22(** This file defines some common structures of several languages. *)
     3
     4(** Types and Signatures *)
     5
     6type signedness = Signed | Unsigned
     7
     8type size = int (* in bytes *)
     9
     10type sig_type =
     11  | Sig_int of size * signedness
     12  | Sig_float of size * signedness
     13  | Sig_offset
     14  | Sig_ptr
     15
     16type type_return = Type_ret of sig_type | Type_void
     17
     18type signature = { args: sig_type list ; res: type_return }
     19
    320
    421type ident = string (* identifiers for variable and function names *)
     
    724
    825
    9 (* Comparison between integers or floats *)
     26(** Memory quantities is the size of what can fit in memory. *)
     27
     28type quantity =
     29  | QInt of size (* concrete size in bytes *)
     30  | QOffset      (* size of an offset *)
     31  | QPtr         (* size of a pointer *)
     32
     33type abstract_size =
     34  | SQ of quantity
     35  | SProd of abstract_size list
     36  | SSum of abstract_size list
     37  | SArray of int * abstract_size
     38
     39type abstract_offset = abstract_size * int (* nth in size *)
     40
     41
     42(** Comparison between integers or floats *)
    1043
    1144type cmp = Cmp_eq | Cmp_ne | Cmp_gt | Cmp_ge | Cmp_lt | Cmp_le
    1245
    13 (* Constants in high level languages *)
     46(** Constants in high level languages *)
    1447
    1548type cst =
    16   | Cst_int of int               (* integer constant *)
    17   | Cst_float of float           (* float constant *)
    18   | Cst_addrsymbol of ident      (* address of a global symbol *)
    19   | Cst_stackoffset of immediate (* offset in the stack *)
     49  | Cst_int of int                     (* integer constant *)
     50  | Cst_float of float                 (* float constant *)
     51  | Cst_addrsymbol of ident            (* address of a global symbol *)
     52  | Cst_stack                          (* address of the stack *)
     53  | Cst_offset of abstract_offset      (* offset *)
     54  | Cst_sizeof of abstract_size        (* size of a type *)
    2055
    21 (* Unary operations *)
     56(** Unary operations *)
    2257
    2358type op1 = 
    24   | Op_cast8unsigned  (**r 8-bit zero extension  *)
    25   | Op_cast8signed    (**r 8-bit sign extension  *)
    26   | Op_cast16unsigned (**r 16-bit zero extension  *)
    27   | Op_cast16signed   (**r 16-bit sign extension *)
    28   | Op_negint         (**r integer opposite *)
    29   | Op_notbool        (**r boolean negation  *)
    30   | Op_notint         (**r bitwise complement  *)
    31   | Op_negf           (**r float opposite *)
    32   | Op_absf           (**r float absolute value *)
    33   | Op_singleoffloat  (**r float truncation *)
    34   | Op_intoffloat     (**r signed integer to float *)
    35   | Op_intuoffloat    (**r unsigned integer to float *)
    36   | Op_floatofint     (**r float to signed integer *)
    37   | Op_floatofintu    (**r float to unsigned integer *)
    38   | Op_id             (**r identity *)
    39   | Op_ptrofint       (**r int to pointer *)
    40   | Op_intofptr       (**r pointer to int *)
     59  | Op_cast of (size * signedness) * size
     60  | Op_negint           (**r integer opposite *)
     61  | Op_notbool          (**r boolean negation  *)
     62  | Op_notint           (**r bitwise complement  *)
     63  | Op_id               (**r identity *)
     64  | Op_ptrofint         (**r int to pointer *)
     65  | Op_intofptr         (**r pointer to int *)
    4166
    42 (* Binary operations *)
     67(** Binary operations *)
    4368
    4469type op2 =
     
    4671  | Op_sub         (**r integer subtraction *)
    4772  | Op_mul         (**r integer multiplication *)
    48   | Op_div         (**r integer signed division *)
     73  | Op_div         (**r integer division *)
    4974  | Op_divu        (**r integer unsigned division *)
    50   | Op_mod         (**r integer signed modulus *)
     75  | Op_mod         (**r integer modulus *)
    5176  | Op_modu        (**r integer unsigned modulus *)
    5277  | Op_and         (**r bitwise ``and'' *)
     
    5479  | Op_xor         (**r bitwise ``xor'' *)
    5580  | Op_shl         (**r left shift *)
    56   | Op_shr         (**r right signed shift *)
    57   | Op_shru        (**r right unsigned shift *)
    58   | Op_addf        (**r float addition *)
    59   | Op_subf        (**r float subtraction *)
    60   | Op_mulf        (**r float multiplication *)
    61   | Op_divf        (**r float division *)
    62   | Op_cmp of cmp  (**r integer signed comparison *)
    63   | Op_cmpu of cmp (**r integer unsigned comparison *)
    64   | Op_cmpf of cmp (**r float comparison *)
     81  | Op_shr         (**r right shift *)
     82  | Op_shru        (**r unsigned right shift *)
     83  | Op_cmp of cmp  (**r integer comparison *)
     84  | Op_cmpu of cmp (**r unsigned integer comparison *)
    6585  | Op_addp        (**r addition for a pointer and an integer *)
    6686  | Op_subp        (**r substraction for a pointer and a integer *)
     87  | Op_subpp       (**r substraction for two pointers *)
    6788  | Op_cmpp of cmp (**r pointer comparaison *)
    6889
     
    7091
    7192type data =
     93(* (* Disabled: needed abstraction. *)
    7294  | Data_reserve of int (* only reserve some space *)
     95*)
    7396  | Data_int8 of int
    7497  | Data_int16 of int
     
    79102type data_size = Byte | HalfWord | Word
    80103
    81 (* Types and Signatures *)
    82 
    83 type sig_type = Sig_int | Sig_float | Sig_ptr
    84 
    85 type type_return = Type_ret of sig_type | Type_void
    86 
    87 type signature = { args: sig_type list ; res: type_return }
    88 
    89104(* External functions. *)
    90105
    91106type external_function = { ef_tag: ident ; ef_sig: signature }
    92 
    93107
    94108(* Traces returned by interpreters: result and cost labels are observed. The
     
    96110   languages. *)
    97111
    98 type trace = IntValue.int8 * CostLabel.t list
     112type trace = IntValue.int32 * CostLabel.t list
  • Deliverables/D2.2/8051/src/common/intValue.ml

    r740 r818  
    1111
    1212type int_repr = Big_int.big_int
     13
     14let print_int_repr = Big_int.string_of_big_int
    1315
    1416(* The parameter module. Bounded integers are characterized by the number of
     
    3032  val zero      : t
    3133  val one       : t
     34
     35  val to_signed_int_repr   : t -> int_repr
     36  val to_unsigned_int_repr : t -> int_repr
    3237
    3338  val succ    : t -> t
     
    8287      representation). *)
    8388  val break : t -> int -> t list
    84   (** [merge l] creates the integer where the first element of [l] is its
    85       low bits, etc, and the last element of [l] is its high bits (little endian
     89  (** [merge l] creates the integer where the first element of [l] is its low
     90      bits, etc, and the last element of [l] is its high bits (little endian
    8691      representation). *)
    8792  val merge : t list -> t
     
    123128    if lt_big_int a half_bound then a
    124129    else sub_big_int a _mod
     130
     131  let to_signed_int_repr a = signed a
     132
     133  let to_unsigned_int_repr a = a
    125134
    126135  let signed_op op a b = op (signed a) (signed b)
  • Deliverables/D2.2/8051/src/common/intValue.mli

    r619 r818  
    88
    99type int_repr = Big_int.big_int
     10val print_int_repr : int_repr -> string
    1011
    1112(* The parameter module. Bounded integers are characterized by the number of
     
    2728  val zero      : t
    2829  val one       : t
     30
     31  val to_signed_int_repr   : t -> int_repr
     32  val to_unsigned_int_repr : t -> int_repr
    2933
    3034  val succ    : t -> t
     
    7680
    7781  (** [break i n] cuts [i] in [n] parts. In the resulting list, the first
    78       element is the high bits, and the last is the low bits. *)
     82      element is the low bits, and the last is the high bits (little endian
     83      representation). *)
    7984  val break : t -> int -> t list
    80   (** [merge l] creates the integer where the first element of [l] is its
    81       high bits, etc, and the last element of [l] is its low bits. *)
     85  (** [merge l] creates the integer where the first element of [l] is its low
     86      bits, etc, and the last element of [l] is its high bits (little endian
     87      representation). *)
    8288  val merge : t list -> t
    8389
  • 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
  • Deliverables/D2.2/8051/src/common/memory.mli

    r740 r818  
    66(** 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. *)
    108
    11 type quantity =
    12   | QInt of int (* Sized integer *)
    13   | QPtr        (* Pointer *)
    14 
    15 val string_of_quantity : quantity -> string
     9val string_of_quantity : AST.quantity -> string
    1610
    1711val size_of_data  : AST.data -> int
     12
     13val all_offsets : AST.abstract_size -> AST.abstract_offset list list
    1814
    1915
     
    3834  val alignment : int option
    3935
    40   val size_of_quantity : quantity -> int
     36  val size_of_quantity : AST.quantity -> int
    4137
    4238  module Value : Value.S
     
    6763      [mem] and returns the value found. *)
    6864  val load  : 'fun_def memory -> int -> Value.address -> Value.t
    69   val loadq : 'fun_def memory -> quantity -> Value.address -> Value.t
     65  val loadq : 'fun_def memory -> AST.quantity -> Value.address -> Value.t
    7066
    7167  (** [store mem size addr v] writes the [size] first bytes (little endian
     
    7369  val store  : 'fun_def memory -> int -> Value.address -> Value.t ->
    7470               'fun_def memory
    75   val storeq : 'fun_def memory -> quantity -> Value.address -> Value.t ->
     71  val storeq : 'fun_def memory -> AST.quantity -> Value.address -> Value.t ->
    7672               'fun_def memory
    7773
    7874  (* Globals management *)
    7975
    80   (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
    81       memory [mem], and associates the global variable [x] with the address of
    82       the block. *)
    83   val add_var : 'fun_def memory -> AST.ident -> AST.data list -> 'fun_def memory
     76  (** [add_var mem x offsets init_datas] stores the datas [init_datas] of
     77      offsets [offsets] in a new block of memory [mem], and associates the
     78      global variable [x] with the address of the block. *)
     79  val add_var :
     80    'fun_def memory -> AST.ident -> AST.abstract_size -> AST.data list option ->
     81    'fun_def memory
    8482
    8583  (** [add_fun_def mem f def] stores the function definition [def] in a new
     
    10098  val find_fun_def : 'fun_def memory -> Value.address -> 'fun_def
    10199
    102   (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
    103       of size [sizes]. *)
    104   val align : int (* starting offset *) -> int list (* sizes *) ->
     100
     101  (** [align off size] returns the aligned offsets (starting at [off]) of datas
     102      of size [size]. *)
     103  val align : int (* starting offset *) -> AST.abstract_size (* sizes *) ->
    105104              (int list (* resulting offsets *) * int (* full size *))
    106105
     106  val concrete_offsets_size : AST.abstract_size -> int list * int
     107
     108  val concrete_offsets : AST.abstract_size -> int list
     109
     110  val concrete_size : AST.abstract_size -> int
     111
     112  val concrete_offset : AST.abstract_offset -> int
     113
     114(*
    107115  val size_of_datas : AST.data list -> int
    108116
     
    113121  val alloc_datas : 'fun_def memory -> AST.data list ->
    114122                    ('fun_def memory * Value.address)
     123*)
    115124
    116125  val to_string : 'fun_def memory -> string
  • Deliverables/D2.2/8051/src/common/primitive.ml

    r740 r818  
    88
    99
    10 let print = "print"
    11 let println = "println"
    12 let scan_int = "scan_int"
    13 let alloc = "alloc"
    14 let newline = "newline"
     10let print_schar =
     11  ("print_schar", "extern void print_schar(signed char);")
     12let print_uchar =
     13  ("print_uchar", "extern void print_uchar(unsigned char);")
     14let print_sshort =
     15  ("print_sshort", "extern void print_sshort(signed short);")
     16let print_ushort =
     17  ("print_ushort", "extern void print_ushort(unsigned short);")
     18let print_sint =
     19  ("print_sint", "extern void print_sint(signed int);")
     20let print_uint =
     21  ("print_uint", "extern void print_uint(unsigned int);")
     22let scan_int =
     23  ("scan_int", "extern int scan_int(void);")
     24let alloc =
     25  ("alloc", "extern int* alloc(int);")
     26let newline =
     27  ("newline", "extern void newline(void);")
     28let space =
     29  ("space", "extern void space(void);") 
     30
     31let ident = fst
     32
     33let proto = snd
    1534
    1635let primitives_list =
    17   [print ; println ; scan_int ; alloc ; newline]
     36  [print_schar ; print_uchar ; print_sshort ; print_ushort ;
     37   print_sint ; print_uint ; scan_int ; alloc ; newline ; space]
     38
     39
     40let args_byte_size = function
     41  | s when s = ident print_schar || s = ident print_uchar -> AST.QInt 1
     42  | s when s = ident print_sshort || s = ident print_ushort -> AST.QInt 2
     43  | s when s = ident print_sint || s = ident print_uint -> AST.QInt 4
     44  | s when s = ident scan_int || s = ident newline || s = ident space ->
     45    AST.QInt 0
     46  | s when s = ident alloc -> AST.QPtr
     47  | s -> error ("unknown primitive " ^ s ^ ".")
     48
    1849
    1950let primitives =
    2051  List.fold_left (fun res f -> StringTools.Set.add f res) StringTools.Set.empty
    21     primitives_list
     52    (List.map ident primitives_list)
    2253
    2354let is_primitive f = StringTools.Set.mem f primitives
     
    2657module Interpret (M : Memory.S) = struct
    2758
    28   type res = V of M.Value.t | A of M.Value.address
     59  type res = V of M.Value.t list | A of M.Value.address
     60
     61  let print_integer_primitives =
     62    List.map ident
     63      [print_schar ; print_uchar ; print_sshort ; print_ushort ;
     64       print_sint ; print_uint]
     65
     66  let is_print_integer_primitive f = List.mem f print_integer_primitives
     67
     68  let print_integer_primitive_funs = function
     69    | f when f = ident print_schar ->
     70      (IntValue.Int8.cast, IntValue.Int8.to_signed_int_repr)
     71    | f when f = ident print_uchar ->
     72      (IntValue.Int8.cast, IntValue.Int8.to_unsigned_int_repr)
     73    | f when f = ident print_sshort ->
     74      (IntValue.Int16.cast, IntValue.Int16.to_signed_int_repr)
     75    | f when f = ident print_ushort ->
     76      (IntValue.Int16.cast, IntValue.Int16.to_unsigned_int_repr)
     77    | f when f = ident print_sint ->
     78      (IntValue.Int32.cast, IntValue.Int32.to_signed_int_repr)
     79    | f when f = ident print_uint ->
     80      (IntValue.Int32.cast, IntValue.Int32.to_unsigned_int_repr)
     81    | f -> error ("unknown integer printing primitive " ^ f ^ ".")
     82
     83  let make_int_value vs = IntValue.Int32.merge (List.map M.Value.to_int_repr vs)
     84
     85  let print_integer f mem vs =
     86    let (cast, to_int_repr) = print_integer_primitive_funs f in
     87    let i = make_int_value vs in
     88    let i = cast i in
     89    let i = to_int_repr i in
     90    Printf.printf "%s%!" (IntValue.print_int_repr i) ;
     91    (mem, V [])
     92
     93  let are_ints args =
     94    let f res v = res && M.Value.is_int v in
     95    List.fold_left f true args
     96
     97  let res_of_int i =
     98    let i = IntValue.Int32.of_int i in
     99    let is = IntValue.Int32.break i (4 / M.Value.int_size) in
     100    List.map M.Value.of_int_repr is
    29101
    30102  let t mem f = function
    31     | _ when f = scan_int ->
     103    | args when is_print_integer_primitive f && are_ints args ->
     104      print_integer f mem args
     105    | _ when f = ident scan_int ->
    32106      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
     107      (mem, V (res_of_int (int_of_string (read_line ()))))
     108    | args when f = ident alloc && are_ints args ->
     109      let size = IntValue.Int32.to_int (make_int_value args) in
    42110      let (mem, addr) = M.alloc mem size in
    43111      (mem, A addr)
    44     | _ when f = newline ->
     112    | _ when f = ident newline ->
    45113      Printf.printf "\n%!" ;
    46       (mem, V M.Value.zero)
    47     | _ -> error ("unknown primitive " ^ f ^ " or wrong size arguments.")
     114      (mem, V [])
     115    | _ when f = ident space ->
     116      Printf.printf " %!" ;
     117      (mem, V [])
     118    | _ -> error ("unknown primitive " ^ f ^ " or bad arguments.")
    48119end
    49120
    50121
     122let print_signedness = function
     123  | AST.Signed -> "s"
     124  | AST.Unsigned -> "u"
     125
     126let print_size = string_of_int
     127
    51128let print_type = function
    52   | AST.Sig_int -> "int"
    53   | AST.Sig_float -> "float"
     129  | AST.Sig_int (size, sign) ->
     130    "int" ^ (print_size size) ^ (print_signedness sign)
     131  | AST.Sig_float (size, sign) ->
     132    "float" ^ (print_size size) ^ (print_signedness sign)
     133  | AST.Sig_offset -> "offset"
    54134  | AST.Sig_ptr -> "ptr"
    55135
     
    67147    (print_type_return sg.AST.res)
    68148
    69 let print_prototype =
    70   "extern void print(int);"
    71 
    72 let println_prototype =
    73   "extern void println(int);"
    74 
    75 let scan_int_prototype =
    76   "extern int scan_int(void);"
    77 
    78 let alloc_prototype =
    79   "extern int* alloc(int);"
    80 
    81 let newline_prototype =
    82   "extern void newline(void);"
    83 
    84149let prototypes =
    85   let ss =
    86     [print_prototype ; println_prototype ; scan_int_prototype ;
    87      alloc_prototype ; newline_prototype] in
    88150  let f res s = res ^ "\n" ^ s in
    89   (List.fold_left f "" ss) ^ "\n\n"
     151  (List.fold_left f "" (List.map proto primitives_list)) ^ "\n\n"
  • Deliverables/D2.2/8051/src/common/primitive.mli

    r740 r818  
    66val is_primitive : string -> bool
    77
    8 (* extern void print(int); *)
    9 val print : string
    10 (* extern void println(int); *)
    11 val println : string
    12 (* extern int scan_int(void); *)
    13 val scan_int : string
    14 (* extern int* alloc(int); *)
    15 val alloc : string
    16 (* extern void newline(void); *)
    17 val newline : string
     8(** Available primitives are :
     9extern void print_schar(signed char);
     10extern void print_uchar(unsigned char);
     11extern void print_sshort(signed short);
     12extern void print_ushort(unsigned short);
     13extern void print_sint(signed int);
     14extern void print_uint(unsigned int);
     15extern int scan_int(void);
     16extern int* alloc(int);
     17extern void newline(void);
     18extern void space(void); *)
    1819
    19 val print_sig : AST.signature -> string
     20val args_byte_size : string -> AST.quantity
     21
     22val print_type        : AST.sig_type -> string
     23val print_type_return : AST.type_return -> string
     24val print_sig         : AST.signature -> string
     25val print_signedness  : AST.signedness -> string
     26val print_size        : AST.size -> string
    2027
    2128module Interpret (M : Memory.S) : sig
    22   type res = V of M.Value.t | A of M.Value.address
     29  type res = V of M.Value.t list | A of M.Value.address
    2330  val t : 'a M.memory -> string -> M.Value.t list -> 'a M.memory * res
    2431end
  • Deliverables/D2.2/8051/src/common/value.ml

    r740 r818  
    2626module type S =
    2727sig
     28
     29  val int_size : int
     30  val ptr_size : int
    2831
    2932  (** The type of values. A value may be: a bounded integer, a chunk of an
     
    6164      values. For integer values, it will return the integer value that
    6265      represents the same quantity, but using every bits (sign or zero
    63       extension) of an integer value. *)
     66      extension) of an integer value. For example, the function [cast8unsigned]
     67      should be read as "cast from an 8 bits unsigned integer". *)
    6468  val cast8unsigned  : t -> t
    6569  val cast8signed    : t -> t
     
    6872  val cast32         : t -> t
    6973
    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. *)
     74  (** [zero_ext v n m] performs a zero extension on [v] where [n] bytes are
     75      significant to a value where [m] bytes are significant. *)
    7276  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. *)
     77  (** [sign_ext v n m] performs a sign extension on [v] where [n] bytes are
     78      significant to a value where [m] bytes are significant. *)
    7579  val sign_ext : t -> int -> int -> t
    7680
     
    184188struct
    185189
     190  let int_size = D.int_size
     191  let ptr_size = D.ptr_size
     192
    186193  (* Integer values. *)
    187194  module ValInt = IntValue.Make (struct let size = D.int_size end)
     
    373380
    374381  let ext sh v n m =
     382    let n = n * 8 in
     383    let m = m * 8 in
    375384    let real_size = D.int_size * 8 in
    376385    let int_sh sh v n = sh v (of_int n) in
  • Deliverables/D2.2/8051/src/common/value.mli

    r740 r818  
    1818module type S =
    1919sig
     20
     21  val int_size : int
     22  val ptr_size : int
    2023
    2124  (** The type of values. A value may be: a bounded integer, a chunk of an
     
    5356      values. For integer values, it will return the integer value that
    5457      represents the same quantity, but using every bits (sign or zero
    55       extension) of an integer value. *)
     58      extension) of an integer value. For example, the function [cast8unsigned]
     59      should be read as "cast from an 8 bits unsigned integer". *)
    5660  val cast8unsigned  : t -> t
    5761  val cast8signed    : t -> t
     
    6064  val cast32         : t -> t
    6165
    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. *)
     66  (** [zero_ext v n m] performs a zero extension on [v] where [n] bytes are
     67      significant to a value where [m] bytes are significant. *)
    6468  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. *)
     69  (** [sign_ext v n m] performs a sign extension on [v] where [n] bytes are
     70      significant to a value where [m] bytes are significant. *)
    6771  val sign_ext : t -> int -> int -> t
    6872
Note: See TracChangeset for help on using the changeset viewer.