Changeset 818 for Deliverables/D2.2/8051/src/common
- Timestamp:
- May 19, 2011, 4:03:04 PM (10 years ago)
- Location:
- Deliverables/D2.2/8051/src/common
- Files:
-
- 9 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/src/common/AST.mli
r619 r818 1 1 2 2 (** This file defines some common structures of several languages. *) 3 4 (** Types and Signatures *) 5 6 type signedness = Signed | Unsigned 7 8 type size = int (* in bytes *) 9 10 type sig_type = 11 | Sig_int of size * signedness 12 | Sig_float of size * signedness 13 | Sig_offset 14 | Sig_ptr 15 16 type type_return = Type_ret of sig_type | Type_void 17 18 type signature = { args: sig_type list ; res: type_return } 19 3 20 4 21 type ident = string (* identifiers for variable and function names *) … … 7 24 8 25 9 (* Comparison between integers or floats *) 26 (** Memory quantities is the size of what can fit in memory. *) 27 28 type quantity = 29 | QInt of size (* concrete size in bytes *) 30 | QOffset (* size of an offset *) 31 | QPtr (* size of a pointer *) 32 33 type 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 39 type abstract_offset = abstract_size * int (* nth in size *) 40 41 42 (** Comparison between integers or floats *) 10 43 11 44 type cmp = Cmp_eq | Cmp_ne | Cmp_gt | Cmp_ge | Cmp_lt | Cmp_le 12 45 13 (* Constants in high level languages *)46 (** Constants in high level languages *) 14 47 15 48 type 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 *) 20 55 21 (* Unary operations *)56 (** Unary operations *) 22 57 23 58 type 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 *) 41 66 42 (* Binary operations *)67 (** Binary operations *) 43 68 44 69 type op2 = … … 46 71 | Op_sub (**r integer subtraction *) 47 72 | Op_mul (**r integer multiplication *) 48 | Op_div (**r integer signeddivision *)73 | Op_div (**r integer division *) 49 74 | Op_divu (**r integer unsigned division *) 50 | Op_mod (**r integer signedmodulus *)75 | Op_mod (**r integer modulus *) 51 76 | Op_modu (**r integer unsigned modulus *) 52 77 | Op_and (**r bitwise ``and'' *) … … 54 79 | Op_xor (**r bitwise ``xor'' *) 55 80 | 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 *) 65 85 | Op_addp (**r addition for a pointer and an integer *) 66 86 | Op_subp (**r substraction for a pointer and a integer *) 87 | Op_subpp (**r substraction for two pointers *) 67 88 | Op_cmpp of cmp (**r pointer comparaison *) 68 89 … … 70 91 71 92 type data = 93 (* (* Disabled: needed abstraction. *) 72 94 | Data_reserve of int (* only reserve some space *) 95 *) 73 96 | Data_int8 of int 74 97 | Data_int16 of int … … 79 102 type data_size = Byte | HalfWord | Word 80 103 81 (* Types and Signatures *)82 83 type sig_type = Sig_int | Sig_float | Sig_ptr84 85 type type_return = Type_ret of sig_type | Type_void86 87 type signature = { args: sig_type list ; res: type_return }88 89 104 (* External functions. *) 90 105 91 106 type external_function = { ef_tag: ident ; ef_sig: signature } 92 93 107 94 108 (* Traces returned by interpreters: result and cost labels are observed. The … … 96 110 languages. *) 97 111 98 type trace = IntValue.int 8* CostLabel.t list112 type trace = IntValue.int32 * CostLabel.t list -
Deliverables/D2.2/8051/src/common/intValue.ml
r740 r818 11 11 12 12 type int_repr = Big_int.big_int 13 14 let print_int_repr = Big_int.string_of_big_int 13 15 14 16 (* The parameter module. Bounded integers are characterized by the number of … … 30 32 val zero : t 31 33 val one : t 34 35 val to_signed_int_repr : t -> int_repr 36 val to_unsigned_int_repr : t -> int_repr 32 37 33 38 val succ : t -> t … … 82 87 representation). *) 83 88 val break : t -> int -> t list 84 (** [merge l] creates the integer where the first element of [l] is its 85 lowbits, etc, and the last element of [l] is its high bits (little endian89 (** [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 86 91 representation). *) 87 92 val merge : t list -> t … … 123 128 if lt_big_int a half_bound then a 124 129 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 125 134 126 135 let signed_op op a b = op (signed a) (signed b) -
Deliverables/D2.2/8051/src/common/intValue.mli
r619 r818 8 8 9 9 type int_repr = Big_int.big_int 10 val print_int_repr : int_repr -> string 10 11 11 12 (* The parameter module. Bounded integers are characterized by the number of … … 27 28 val zero : t 28 29 val one : t 30 31 val to_signed_int_repr : t -> int_repr 32 val to_unsigned_int_repr : t -> int_repr 29 33 30 34 val succ : t -> t … … 76 80 77 81 (** [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). *) 79 84 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). *) 82 88 val merge : t list -> t 83 89 -
Deliverables/D2.2/8051/src/common/memory.ml
r740 r818 11 11 12 12 13 (** Memory quantities is the size and type of what can be loaded or stored in14 memory. *)15 16 type quantity =17 | QInt of int (* Sized integer *)18 | QPtr (* Pointer *)19 20 13 let 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" 23 17 24 18 25 19 let size_of_data = function 20 (* 26 21 | AST.Data_reserve n -> n 22 *) 27 23 | AST.Data_int8 _ -> 1 28 24 | AST.Data_int16 _ -> 2 … … 30 26 | AST.Data_float32 _ -> 4 31 27 | AST.Data_float64 _ -> 8 28 29 30 let 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 32 44 33 45 … … 52 64 val alignment : int option 53 65 54 val size_of_quantity : quantity -> int66 val size_of_quantity : AST.quantity -> int 55 67 56 68 module Value : Value.S … … 81 93 [mem] and returns the value found. *) 82 94 val load : 'fun_def memory -> int -> Value.address -> Value.t 83 val loadq : 'fun_def memory -> quantity -> Value.address -> Value.t95 val loadq : 'fun_def memory -> AST.quantity -> Value.address -> Value.t 84 96 85 97 (** [store mem size addr v] writes the [size] first bytes (little endian … … 87 99 val store : 'fun_def memory -> int -> Value.address -> Value.t -> 88 100 '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 -> 90 102 'fun_def memory 91 103 92 104 (* Globals management *) 93 105 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 98 112 99 113 (** [add_fun_def mem f def] stores the function definition [def] in a new … … 114 128 val find_fun_def : 'fun_def memory -> Value.address -> 'fun_def 115 129 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 *) -> 119 134 (int list (* resulting offsets *) * int (* full size *)) 120 135 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 (* 121 145 val size_of_datas : AST.data list -> int 122 146 … … 127 151 val alloc_datas : 'fun_def memory -> AST.data list -> 128 152 ('fun_def memory * Value.address) 153 *) 129 154 130 155 val to_string : 'fun_def memory -> string … … 151 176 152 177 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 155 181 156 182 … … 176 202 let is_multiple n m = m mod n = 0 177 203 178 (** [align off size] returns the offset greater or equal to [off] that is204 (** [align_off off size] returns the offset greater or equal to [off] that is 179 205 aligned for storing a value of size [size]. *) 180 let align off size = match D.alignment with206 let align_off off size = match D.alignment with 181 207 | None -> off 182 208 | Some alignment when (size <= alignment) && (is_multiple size alignment) -> … … 191 217 else Offset.add off (Offset.sub size rem) 192 218 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) 194 220 195 221 (** [pad off] returns the offset that is obtained by adding some padding from … … 197 223 let pad off = match D.alignment with 198 224 | 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))) 219 232 220 233 … … 405 418 406 419 let value_of_data = function 420 (* 407 421 | AST.Data_reserve _ -> Value.undef 422 *) 408 423 | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i -> Value.of_int i 409 424 | AST.Data_float32 f | AST.Data_float64 f -> error "float not supported." 410 425 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 444 488 445 489 446 490 (* Globals manipulation *) 447 491 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 454 513 { mem with addr_of_global = addr_of_global } 455 514 -
Deliverables/D2.2/8051/src/common/memory.mli
r740 r818 6 6 (** In the module, every size is expressed in bytes. *) 7 7 8 (** Memory quantities is the size and type of what can be loaded or stored in9 memory. *)10 8 11 type quantity = 12 | QInt of int (* Sized integer *) 13 | QPtr (* Pointer *) 14 15 val string_of_quantity : quantity -> string 9 val string_of_quantity : AST.quantity -> string 16 10 17 11 val size_of_data : AST.data -> int 12 13 val all_offsets : AST.abstract_size -> AST.abstract_offset list list 18 14 19 15 … … 38 34 val alignment : int option 39 35 40 val size_of_quantity : quantity -> int36 val size_of_quantity : AST.quantity -> int 41 37 42 38 module Value : Value.S … … 67 63 [mem] and returns the value found. *) 68 64 val load : 'fun_def memory -> int -> Value.address -> Value.t 69 val loadq : 'fun_def memory -> quantity -> Value.address -> Value.t65 val loadq : 'fun_def memory -> AST.quantity -> Value.address -> Value.t 70 66 71 67 (** [store mem size addr v] writes the [size] first bytes (little endian … … 73 69 val store : 'fun_def memory -> int -> Value.address -> Value.t -> 74 70 '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 -> 76 72 'fun_def memory 77 73 78 74 (* Globals management *) 79 75 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 84 82 85 83 (** [add_fun_def mem f def] stores the function definition [def] in a new … … 100 98 val find_fun_def : 'fun_def memory -> Value.address -> 'fun_def 101 99 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 *) -> 105 104 (int list (* resulting offsets *) * int (* full size *)) 106 105 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 (* 107 115 val size_of_datas : AST.data list -> int 108 116 … … 113 121 val alloc_datas : 'fun_def memory -> AST.data list -> 114 122 ('fun_def memory * Value.address) 123 *) 115 124 116 125 val to_string : 'fun_def memory -> string -
Deliverables/D2.2/8051/src/common/primitive.ml
r740 r818 8 8 9 9 10 let print = "print" 11 let println = "println" 12 let scan_int = "scan_int" 13 let alloc = "alloc" 14 let newline = "newline" 10 let print_schar = 11 ("print_schar", "extern void print_schar(signed char);") 12 let print_uchar = 13 ("print_uchar", "extern void print_uchar(unsigned char);") 14 let print_sshort = 15 ("print_sshort", "extern void print_sshort(signed short);") 16 let print_ushort = 17 ("print_ushort", "extern void print_ushort(unsigned short);") 18 let print_sint = 19 ("print_sint", "extern void print_sint(signed int);") 20 let print_uint = 21 ("print_uint", "extern void print_uint(unsigned int);") 22 let scan_int = 23 ("scan_int", "extern int scan_int(void);") 24 let alloc = 25 ("alloc", "extern int* alloc(int);") 26 let newline = 27 ("newline", "extern void newline(void);") 28 let space = 29 ("space", "extern void space(void);") 30 31 let ident = fst 32 33 let proto = snd 15 34 16 35 let 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 40 let 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 18 49 19 50 let primitives = 20 51 List.fold_left (fun res f -> StringTools.Set.add f res) StringTools.Set.empty 21 primitives_list52 (List.map ident primitives_list) 22 53 23 54 let is_primitive f = StringTools.Set.mem f primitives … … 26 57 module Interpret (M : Memory.S) = struct 27 58 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 29 101 30 102 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 -> 32 106 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 42 110 let (mem, addr) = M.alloc mem size in 43 111 (mem, A addr) 44 | _ when f = newline ->112 | _ when f = ident newline -> 45 113 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.") 48 119 end 49 120 50 121 122 let print_signedness = function 123 | AST.Signed -> "s" 124 | AST.Unsigned -> "u" 125 126 let print_size = string_of_int 127 51 128 let 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" 54 134 | AST.Sig_ptr -> "ptr" 55 135 … … 67 147 (print_type_return sg.AST.res) 68 148 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 84 149 let prototypes = 85 let ss =86 [print_prototype ; println_prototype ; scan_int_prototype ;87 alloc_prototype ; newline_prototype] in88 150 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 6 6 val is_primitive : string -> bool 7 7 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 : 9 extern void print_schar(signed char); 10 extern void print_uchar(unsigned char); 11 extern void print_sshort(signed short); 12 extern void print_ushort(unsigned short); 13 extern void print_sint(signed int); 14 extern void print_uint(unsigned int); 15 extern int scan_int(void); 16 extern int* alloc(int); 17 extern void newline(void); 18 extern void space(void); *) 18 19 19 val print_sig : AST.signature -> string 20 val args_byte_size : string -> AST.quantity 21 22 val print_type : AST.sig_type -> string 23 val print_type_return : AST.type_return -> string 24 val print_sig : AST.signature -> string 25 val print_signedness : AST.signedness -> string 26 val print_size : AST.size -> string 20 27 21 28 module Interpret (M : Memory.S) : sig 22 type res = V of M.Value.t | A of M.Value.address29 type res = V of M.Value.t list | A of M.Value.address 23 30 val t : 'a M.memory -> string -> M.Value.t list -> 'a M.memory * res 24 31 end -
Deliverables/D2.2/8051/src/common/value.ml
r740 r818 26 26 module type S = 27 27 sig 28 29 val int_size : int 30 val ptr_size : int 28 31 29 32 (** The type of values. A value may be: a bounded integer, a chunk of an … … 61 64 values. For integer values, it will return the integer value that 62 65 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". *) 64 68 val cast8unsigned : t -> t 65 69 val cast8signed : t -> t … … 68 72 val cast32 : t -> t 69 73 70 (** [zero_ext v n m] performs a zero extension on [v] where [n] b its are71 significant to a value where [m] b its 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. *) 72 76 val zero_ext : t -> int -> int -> t 73 (** [sign_ext v n m] performs a sign extension on [v] where [n] b its are74 significant to a value where [m] b its 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. *) 75 79 val sign_ext : t -> int -> int -> t 76 80 … … 184 188 struct 185 189 190 let int_size = D.int_size 191 let ptr_size = D.ptr_size 192 186 193 (* Integer values. *) 187 194 module ValInt = IntValue.Make (struct let size = D.int_size end) … … 373 380 374 381 let ext sh v n m = 382 let n = n * 8 in 383 let m = m * 8 in 375 384 let real_size = D.int_size * 8 in 376 385 let int_sh sh v n = sh v (of_int n) in -
Deliverables/D2.2/8051/src/common/value.mli
r740 r818 18 18 module type S = 19 19 sig 20 21 val int_size : int 22 val ptr_size : int 20 23 21 24 (** The type of values. A value may be: a bounded integer, a chunk of an … … 53 56 values. For integer values, it will return the integer value that 54 57 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". *) 56 60 val cast8unsigned : t -> t 57 61 val cast8signed : t -> t … … 60 64 val cast32 : t -> t 61 65 62 (** [zero_ext v n m] performs a zero extension on [v] where [n] b its are63 significant to a value where [m] b its 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. *) 64 68 val zero_ext : t -> int -> int -> t 65 (** [sign_ext v n m] performs a sign extension on [v] where [n] b its are66 significant to a value where [m] b its 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. *) 67 71 val sign_ext : t -> int -> int -> t 68 72
Note: See TracChangeset
for help on using the changeset viewer.