Ignore:
Timestamp:
May 19, 2011, 4:03:04 PM (10 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.