diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail_values.ml | 583 |
1 files changed, 354 insertions, 229 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 0072d5b6..d6443a16 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -4,18 +4,34 @@ open Big_int_Z type vbit = Vone | Vzero | Vundef type number = Big_int_Z.big_int type _bool = vbit +type _string = string +type _nat = number + type value = | Vvector of vbit array * int * bool | VvectorR of value array * int * bool | Vregister of vbit array ref * int * bool * (string * (int * int)) list | Vbit of vbit (*Mostly for Vundef in place of undefined register place holders*) +let string_of_bit = function + | Vone -> "1" + | Vzero -> "0" + | Vundef -> "u" + +let string_of_bit_array a = Array.fold_left (^) "" (Array.map string_of_bit a) + +let string_of_value = function + | Vvector(bits, start, inc) -> (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array bits) + | VvectorR(values, start, inc) -> "" + | Vregister(bits, start, inc, fields) -> (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array !bits) + | Vbit(b) -> string_of_bit b + let to_bool = function | Vzero -> false | Vone -> true | Vundef -> assert false -let is_one_big i = +let is_one i = if eq_big_int i unit_big_int then Vone else Vzero @@ -24,7 +40,7 @@ let is_one_big i = let exit _ = failwith "called exit" -let is_one i = +let is_one_int i = if i = 1 then Vone else Vzero let get_barray = function @@ -56,7 +72,7 @@ let length = function | VvectorR(array,_,_) -> Array.length array | _ -> assert false -let set_start_to_length v = set_start (length v) v +let set_start_to_length v = set_start ((length v)-1) v (* XXX should take account of direction? *) let length_big v = big_int_of_int (length v) @@ -64,16 +80,19 @@ let read_register = function | Vregister(a,start,inc,_) -> Vvector(!a,start,inc) | v -> v -let vector_access v n = match v with +let vector_access_int v n = + match v with | VvectorR(array,start,is_inc) -> if is_inc then (array.(n-start)) else (array.(start-n)) | _ -> assert false -let vector_access_big v n = vector_access v (int_of_big_int n) - -let bit_vector_access v n = match v with +let vector_access_big v n = vector_access_int v (int_of_big_int n) + +let vector_access = vector_access_big + +let bit_vector_access_int v n = match v with | Vvector(array,start,is_inc) -> if is_inc then array.(n-start) @@ -84,9 +103,10 @@ let bit_vector_access v n = match v with else !array.(start-n) | _ -> assert false -let bit_vector_access_big v n = bit_vector_access v (int_of_big_int n) +let bit_vector_access_big v n = bit_vector_access_int v (int_of_big_int n) +let bit_vector_access = bit_vector_access_big -let vector_subrange v n m = +let vector_subrange_int v n m = let builder array length offset default = let new_array = Array.make length default in begin @@ -108,7 +128,8 @@ let vector_subrange v n m = Vvector(builder !array length offset Vzero,n,is_inc) | _ -> v -let vector_subrange_big v n m = vector_subrange v (int_of_big_int n) (int_of_big_int m) +let vector_subrange_big v n m = vector_subrange_int v (int_of_big_int n) (int_of_big_int m) +let vector_subrange = vector_subrange_big let get_register_field_vec reg field = match reg with @@ -117,7 +138,7 @@ let get_register_field_vec reg field = | (i,j) -> if i = j then Vbit Vundef - else vector_subrange reg i j) + else vector_subrange_int reg i j) | _ -> Vbit Vundef let get_register_field_bit reg field = @@ -126,7 +147,7 @@ let get_register_field_bit reg field = (match List.assoc field fields with | (i,j) -> if i = j - then bit_vector_access reg i + then bit_vector_access_int reg i else Vundef) | _ -> Vundef @@ -137,7 +158,7 @@ let set_register register value = match register,value with a := new_v | _ -> () -let set_vector_subrange_vec v n m new_v = +let set_vector_subrange_vec_int v n m new_v = let walker array length offset new_values = begin for x = 0 to length-1 @@ -152,9 +173,10 @@ let set_vector_subrange_vec v n m new_v = | _ -> () let set_vector_subrange_vec_big v n m new_v = - set_vector_subrange_vec v (int_of_big_int n) (int_of_big_int m) new_v + set_vector_subrange_vec_int v (int_of_big_int n) (int_of_big_int m) new_v +let set_vector_subrange_vec = set_vector_subrange_vec_big (* or maybe _int *) -let set_vector_subrange_bit v n m new_v = +let set_vector_subrange_bit_int v n m new_v = let walker array length offset new_values = begin for x = 0 to length-1 @@ -172,7 +194,9 @@ let set_vector_subrange_bit v n m new_v = | _ -> () let set_vector_subrange_bit_big v n m new_v = - set_vector_subrange_bit v (int_of_big_int n) (int_of_big_int m) new_v + set_vector_subrange_bit_int v (int_of_big_int n) (int_of_big_int m) new_v +let set_vector_subrange_bit = set_vector_subrange_bit_int + let set_register_field_v reg field new_v = match reg with @@ -199,8 +223,8 @@ let set_two_reg r1 r2 vec = let dir = get_ord r1 in let start = get_start vec in let vsize = length vec in - let r1_v = vector_subrange vec start ((if dir then size - start else start - size) - 1) in - let r2_v = vector_subrange vec (if dir then size - start else start - size) + let r1_v = vector_subrange_int vec start ((if dir then size - start else start - size) - 1) in + let r2_v = vector_subrange_int vec (if dir then size - start else start - size) (if dir then vsize - start else start - vsize) in begin set_register r1 r1_v; set_register r2 r2_v end @@ -248,7 +272,7 @@ let vector_concat l r = let has_undef = function | Vvector(array,_,_) -> let rec foreach i = - if i <= Array.length array + if i < Array.length array then if array.(i) = Vundef then true else foreach (i+1) @@ -257,7 +281,7 @@ let has_undef = function | Vregister(array,_,_,_) -> let array = !array in let rec foreach i = - if i <= Array.length array + if i < Array.length array then if array.(i) = Vundef then true else foreach (i+1) @@ -298,7 +322,7 @@ let bitwise_binop op (l,r) = let bop l arrayl arrayr = let array = Array.make l Vzero in begin - for i = 0 to l do + for i = 0 to (l-1) do array.(i) <- bitwise_binop_bit op (arrayl.(i), arrayr.(i)) done; array @@ -323,66 +347,62 @@ let rec power_int base raiseto = then 1 else base * (power_int base (raiseto - 1)) -let unsigned = function +let int_of_bit_array array = + let acc = ref 0 in + let len = Array.length array in + begin + for i = len - 1 downto 0 do + match array.(len - i - 1) with + | Vone -> acc := !acc + (power_int 2 i) + | _ -> () + done; + !acc + end + +let unsigned_int = function | (Vvector(array,_,_) as v) -> if has_undef v then assert false - else - let acc = ref 0 in - begin for i = (Array.length array) - 1 downto 0 do - match array.(i) with - | Vone -> acc := !acc + (power_int 2 i) - | _ -> () - done; - !acc - end + else int_of_bit_array array | (Vregister(array,_,_,_) as v)-> let array = !array in if has_undef v then assert false - else - let acc = ref 0 in - begin for i = (Array.length array) - 1 downto 0 do - match array.(i) with - | Vone -> acc := !acc + (power_int 2 i) - | _ -> () - done; - !acc - end + else int_of_bit_array array | _ -> assert false +let big_int_of_bit_array array = + let acc = ref zero_big_int in + let len = Array.length array in + begin + for i = len - 1 downto 0 do + match array.(len-i-1) with + | Vone -> acc := add_big_int !acc (power_int_positive_int 2 i) + | _ -> () + done; + !acc + end + let unsigned_big = function | (Vvector(array,_,_) as v) -> if has_undef v then assert false else - let acc = ref zero_big_int in - begin for i = (Array.length array) - 1 downto 0 do - match array.(i) with - | Vone -> acc := add_big_int !acc (power_int_positive_int 2 i) - | _ -> () - done; - !acc - end + big_int_of_bit_array array | (Vregister(array,_,_,_) as v)-> let array = !array in if has_undef v then assert false else - let acc = ref zero_big_int in - begin for i = (Array.length array) - 1 downto 0 do - match array.(i) with - | Vone -> acc := add_big_int !acc (power_int_positive_int 2 i) - | _ -> () - done; - !acc - end + big_int_of_bit_array array | _ -> assert false -let signed v = +let unsigned = unsigned_big + +let signed_int v = match most_significant v with - | Vone -> -(1 + (unsigned (bitwise_not v))) - | Vzero -> unsigned v + | Vone -> -(1 + (unsigned_int (bitwise_not v))) + | Vzero -> unsigned_int v | _ -> assert false let signed_big v = @@ -391,8 +411,11 @@ let signed_big v = | Vzero -> unsigned_big v | _ -> assert false -let to_num sign = if sign then signed else unsigned +let signed = signed_big + +let to_num_int sign = if sign then signed_int else unsigned_int let to_num_big sign = if sign then signed_big else unsigned_big +let to_num = to_num_big let two_big_int = big_int_of_int 2 let max_64u = pred_big_int (power_big two_big_int (big_int_of_int 64)) @@ -430,13 +453,13 @@ let rec divide_by_2_big array i n = then begin array.(i) <- Vone; divide_by_2_big array (i-1) quo end else divide_by_2_big array (i-1) quo -let rec divide_by_2 array i n = +let rec divide_by_2_int array i n = if i < 0 || n = 0 then array else let (quo,modu) = n/2, n mod 2 in - if modu = 0 - then begin array.(i) <- Vone; divide_by_2 array (i-1) quo end - else divide_by_2 array (i-1) quo + if modu = 1 + then begin array.(i) <- Vone; divide_by_2_int array (i-1) quo end + else divide_by_2_int array (i-1) quo let rec add_one_bit array co i = if i < 0 @@ -448,16 +471,16 @@ let rec add_one_bit array co i = | Vone, true -> add_one_bit array true (i-1) | Vundef,_ -> assert false -let to_vec ord len n = +let to_vec_int ord len n = let array = Array.make len Vzero in let start = if ord then 0 else len-1 in if n = 0 then Vvector(array, start, ord) else if n >= 0 - then Vvector(divide_by_2 array (len -1) n, start, ord) + then Vvector(divide_by_2_int array (len -1) n, start, ord) else let abs_n = abs n in - let abs_array = divide_by_2 array (len-1) abs_n in + let abs_array = divide_by_2_int array (len-1) abs_n in let v_abs = bitwise_not (Vvector(abs_array,start,ord)) in match v_abs with | Vvector(array,start,ord) -> Vvector(add_one_bit array false (len-1),start,ord) @@ -479,13 +502,16 @@ let to_vec_big ord len n = | Vvector(array,start,ord) -> Vvector(add_one_bit array false (len-1),start,ord) | _ -> assert false -let to_vec_inc (len,n) = to_vec true len n -let to_vec_dec (len,n) = to_vec false len n +let to_vec_inc_int (len,n) = to_vec_int true len n +let to_vec_dec_int (len,n) = to_vec_int false len n let to_vec_inc_big (len,n) = to_vec_big true len n let to_vec_dec_big (len,n) = to_vec_big false len n -let to_vec_undef ord len = +let to_vec_inc = to_vec_inc_big +let to_vec_dec = to_vec_dec_big + +let to_vec_undef_int ord len = let array = Array.make len Vundef in let start = if ord then 0 else len-1 in Vvector(array, start, ord) @@ -496,18 +522,24 @@ let to_vec_undef_big ord len = let start = if ord then 0 else len-1 in Vvector(array, start, ord) -let to_vec_inc_undef len = to_vec_undef true len -let to_vec_dec_undef len = to_vec_undef false len +let to_vec_inc_undef_int len = to_vec_undef_int true len +let to_vec_dec_undef_int len = to_vec_undef_int false len let to_vec_inc_undef_big len = to_vec_undef_big true len let to_vec_dec_undef_big len = to_vec_undef_big false len -let exts (len, vec) = to_vec (get_ord vec) len (signed vec) -let extz (len, vec) = to_vec (get_ord vec) len (unsigned vec) +let to_vec_inc_undef = to_vec_inc_undef_big +let to_vec_dec_undef = to_vec_dec_undef_big + +let exts_int (len, vec) = to_vec_int (get_ord vec) len (signed_int vec) +let extz_int (len, vec) = to_vec_int (get_ord vec) len (unsigned_int vec) let exts_big (len,vec) = to_vec_big (get_ord vec) len (signed_big vec) let extz_big (len,vec) = to_vec_big (get_ord vec) len (unsigned_big vec) +let exts = exts_big +let extz = extz_big + let arith_op op (l,r) = op l r let add_big = arith_op add_big_int let add_signed_big = arith_op add_big_int @@ -517,13 +549,21 @@ let modulo_big = arith_op mod_big_int let quot_big = arith_op div_big_int let power_big = arith_op power_big -let add = arith_op (+) -let add_signed = arith_op (+) -let minus = arith_op (-) -let multiply = arith_op ( * ) -let modulo = arith_op (mod) -let quot = arith_op (/) -let power = arith_op power_int +let add_int = arith_op (+) +let add_signed_int = arith_op (+) +let minus_int = arith_op (-) +let multiply_int = arith_op ( * ) +let modulo_int = arith_op (mod) +let quot_int = arith_op (/) +let power_int = arith_op power_int + +let add = add_big +let add_signed = add_signed_big +let minus = minus_big +let multiply = multiply_big +let modulo = modulo_big +let quot = quot_big +let power = power_big let arith_op_vec_big op sign size (l,r) = let ord = get_ord l in @@ -537,65 +577,83 @@ let minus_vec_big = arith_op_vec_big sub_big_int false unit_big_int let multiply_vec_big = arith_op_vec_big mult_big_int false two_big_int let multiply_vec_signed_big = arith_op_vec_big mult_big_int true two_big_int -let arith_op_vec op sign size (l,r) = +let arith_op_vec_int op sign size (l,r) = let ord = get_ord l in - let (l',r') = to_num sign l, to_num sign r in + let (l',r') = to_num_int sign l, to_num_int sign r in let n = arith_op op (l',r') in - to_vec ord (size * (length l)) n + to_vec_int ord (size * (length l)) n -let add_vec = arith_op_vec (+) false 1 -let add_vec_signed = arith_op_vec (+) true 1 -let minus_vec = arith_op_vec (-) false 1 -let multiply_vec = arith_op_vec ( * ) false 2 -let multiply_vec_signed = arith_op_vec ( * ) true 2 +let add_vec_int = arith_op_vec_int (+) false 1 +let add_vec_signed_int = arith_op_vec_int (+) true 1 +let minus_vec_int = arith_op_vec_int (-) false 1 +let multiply_vec_int = arith_op_vec_int ( * ) false 2 +let multiply_vec_signed_int = arith_op_vec_int ( * ) true 2 -let arith_op_vec_range op sign size (l,r) = +let add_vec = add_vec_big +let add_vec_signed = add_vec_signed_big +let minus_vec = minus_vec_big +let multiply_vec = multiply_vec_big +let multiply_vec_signed = multiply_vec_signed_big + + +let arith_op_vec_range_int op sign size (l,r) = let ord = get_ord l in - arith_op_vec op sign size (l, to_vec ord (length l) r) + arith_op_vec_int op sign size (l, to_vec_int ord (length l) r) -let add_vec_range = arith_op_vec_range (+) false 1 -let add_vec_range_signed = arith_op_vec_range (+) true 1 -let minus_vec_range = arith_op_vec_range (-) false 1 -let mult_vec_range = arith_op_vec_range ( * ) false 2 -let mult_vec_range_signed = arith_op_vec_range ( * ) true 2 +let add_vec_range_int = arith_op_vec_range_int (+) false 1 +let add_vec_range_signed_int = arith_op_vec_range_int (+) true 1 +let minus_vec_range_int = arith_op_vec_range_int (-) false 1 +let mult_vec_range_int = arith_op_vec_range_int ( * ) false 2 +let mult_vec_range_signed_int = arith_op_vec_range_int ( * ) true 2 let arith_op_vec_range_big op sign size (l,r) = let ord = get_ord l in arith_op_vec_big op sign size (l, to_vec_big ord (length_big l) r) -let add_vec_range_big = arith_op_vec_range_big add_big_int false unit_big_int -let add_vec_range_signed_big = arith_op_vec_range_big add_big_int true unit_big_int -let minus_vec_range_big = arith_op_vec_range_big sub_big_int false unit_big_int -let mult_vec_range_big = arith_op_vec_range_big mult_big_int false two_big_int +let add_vec_range_big = arith_op_vec_range_big add_big_int false unit_big_int +let add_vec_range_signed_big = arith_op_vec_range_big add_big_int true unit_big_int +let minus_vec_range_big = arith_op_vec_range_big sub_big_int false unit_big_int +let mult_vec_range_big = arith_op_vec_range_big mult_big_int false two_big_int let mult_vec_range_signed_big = arith_op_vec_range_big mult_big_int true two_big_int +let add_vec_range = add_vec_range_big +let add_vec_range_signed = add_vec_range_signed_big +let minus_vec_range = minus_vec_range_big +let mult_vec_range = mult_vec_range_big +let mult_vec_range_signed = mult_vec_range_signed_big -let arith_op_range_vec op sign size (l,r) = +let arith_op_range_vec_int op sign size (l,r) = let ord = get_ord r in - arith_op_vec op sign size ((to_vec ord (length r) l), r) + arith_op_vec_int op sign size ((to_vec_int ord (length r) l), r) -let add_range_vec = arith_op_range_vec (+) false 1 -let add_range_vec_signed = arith_op_range_vec (+) true 1 -let minus_range_vec = arith_op_range_vec (-) false 1 -let mult_range_vec = arith_op_range_vec ( * ) false 2 -let mult_range_vec_signed = arith_op_range_vec ( * ) true 2 +let add_range_vec_int = arith_op_range_vec_int (+) false 1 +let add_range_vec_signed_int = arith_op_range_vec_int (+) true 1 +let minus_range_vec_int = arith_op_range_vec_int (-) false 1 +let mult_range_vec_int = arith_op_range_vec_int ( * ) false 2 +let mult_range_vec_signed_int = arith_op_range_vec_int ( * ) true 2 let arith_op_range_vec_big op sign size (l,r) = let ord = get_ord r in arith_op_vec_big op sign size ((to_vec_big ord (length_big r) l), r) -let add_range_vec_big = arith_op_range_vec_big add_big_int false unit_big_int -let add_range_vec_signed_big = arith_op_range_vec_big add_big_int true unit_big_int -let minus_range_vec_big = arith_op_range_vec_big sub_big_int false unit_big_int -let mult_range_vec_big = arith_op_range_vec_big mult_big_int false two_big_int +let add_range_vec_big = arith_op_range_vec_big add_big_int false unit_big_int +let add_range_vec_signed_big = arith_op_range_vec_big add_big_int true unit_big_int +let minus_range_vec_big = arith_op_range_vec_big sub_big_int false unit_big_int +let mult_range_vec_big = arith_op_range_vec_big mult_big_int false two_big_int let mult_range_vec_signed_big = arith_op_range_vec_big mult_big_int true two_big_int +let add_range_vec = add_range_vec_big +let add_range_vec_signed = add_range_vec_signed_big +let minus_range_vec = minus_range_vec_big +let mult_range_vec = mult_range_vec_big +let mult_range_vec_signed = mult_range_vec_signed_big + -let arith_op_range_vec_range op sign (l,r) = arith_op op (l, to_num sign r) +let arith_op_range_vec_range_int op sign (l,r) = arith_op op (l, to_num_int sign r) -let add_range_vec_range = arith_op_range_vec_range (+) false -let add_range_vec_range_signed = arith_op_range_vec_range (+) true -let minus_range_vec_range = arith_op_range_vec_range (-) false +let add_range_vec_range_int = arith_op_range_vec_range_int (+) false +let add_range_vec_range_signed_int = arith_op_range_vec_range_int (+) true +let minus_range_vec_range_int = arith_op_range_vec_range_int (-) false let arith_op_range_vec_range_big op sign (l,r) = arith_op op (l, to_num_big sign r) @@ -603,11 +661,15 @@ let add_range_vec_range_big = arith_op_range_vec_range_big add_big_int false let add_range_vec_range_signed_big = arith_op_range_vec_range_big add_big_int true let minus_range_vec_range_big = arith_op_range_vec_range_big sub_big_int false -let arith_op_vec_range_range op sign (l,r) = arith_op op (to_num sign l,r) +let add_range_vec_range = add_range_vec_range_big +let add_range_vec_range_signed = add_range_vec_range_signed_big +let minus_range_vec_range = minus_range_vec_range_big -let add_vec_range_range = arith_op_vec_range_range (+) false -let add_vec_range_range_signed = arith_op_vec_range_range (+) true -let minus_vec_range_range = arith_op_vec_range_range (-) false +let arith_op_vec_range_range_int op sign (l,r) = arith_op op (to_num_int sign l,r) + +let add_vec_range_range_int = arith_op_vec_range_range_int (+) false +let add_vec_range_range_signed_int = arith_op_vec_range_range_int (+) true +let minus_vec_range_range_int = arith_op_vec_range_range_int (-) false let arith_op_vec_range_range_big op sign (l,r) = arith_op op (to_num_big sign l,r) @@ -615,12 +677,17 @@ let add_vec_range_range_big = arith_op_vec_range_range_big add_big_int false let add_vec_range_range_signed_big = arith_op_vec_range_range_big add_big_int true let minus_vec_range_range_big = arith_op_vec_range_range_big sub_big_int false -let arith_op_vec_vec_range op sign (l,r) = - let (l',r') = (to_num sign l,to_num sign r) in +let add_vec_range_range = add_vec_range_range_big +let add_vec_range_range_signed = add_vec_range_range_signed_big +let minus_vec_range_range = minus_vec_range_range_big + + +let arith_op_vec_vec_range_int op sign (l,r) = + let (l',r') = (to_num_int sign l,to_num_int sign r) in arith_op op (l',r') -let add_vec_vec_range = arith_op_vec_vec_range (+) false -let add_vec_vec_range_signed = arith_op_vec_vec_range (+) true +let add_vec_vec_range_int = arith_op_vec_vec_range_int (+) false +let add_vec_vec_range_signed_int = arith_op_vec_vec_range_int (+) true let arith_op_vec_vec_range_big op sign (l,r) = let (l',r') = (to_num_big sign l,to_num_big sign r) in @@ -629,15 +696,18 @@ let arith_op_vec_vec_range_big op sign (l,r) = let add_vec_vec_range_big = arith_op_vec_vec_range_big add_big_int false let add_vec_vec_range_signed_big = arith_op_vec_vec_range_big add_big_int true -let arith_op_vec_bit op sign (l,r) = +let add_vec_vec_range = add_vec_vec_range_big +let add_vec_vec_range_signed = add_vec_vec_range_signed_big + +let arith_op_vec_bit_int op sign (l,r) = let ord = get_ord l in - let l' = to_num sign l in + let l' = to_num_int sign l in let n = arith_op op (l', match r with | Vone -> 1 | _ -> 0) in - to_vec ord (length l) n + to_vec_int ord (length l) n -let add_vec_bit = arith_op_vec_bit (+) false -let add_vec_bit_signed = arith_op_vec_bit (+) true -let minus_vec_bit = arith_op_vec_bit (-) true +let add_vec_bit_int = arith_op_vec_bit_int (+) false +let add_vec_bit_signed_int = arith_op_vec_bit_int (+) true +let minus_vec_bit_int = arith_op_vec_bit_int (-) true let arith_op_vec_bit_big op sign (l,r) = let ord = get_ord l in @@ -649,16 +719,21 @@ let add_vec_bit_big = arith_op_vec_bit_big add_big_int false let add_vec_bit_signed_big = arith_op_vec_bit_big add_big_int true let minus_vec_bit_big = arith_op_vec_bit_big sub_big_int true -let rec arith_op_overflow_vec op sign size (l,r) = +let add_vec_bit = add_vec_bit_big +let add_vec_bit_signed = add_vec_bit_signed_big +let minus_vec_bit = minus_vec_bit_big + + +let rec arith_op_overflow_vec_int op sign size (l,r) = let ord = get_ord l in let len = length l in let act_size = len * size in - let (l_sign,r_sign) = (to_num sign l,to_num sign r) in - let (l_unsign,r_unsign) = (to_num false l,to_num false r) in + let (l_sign,r_sign) = (to_num_int sign l,to_num_int sign r) in + let (l_unsign,r_unsign) = (to_num_int false l,to_num_int false r) in let n = arith_op op (l_sign,r_sign) in let n_unsign = arith_op op (l_unsign,r_unsign) in - let correct_size_num = to_vec ord act_size n in - let one_more_size_u = to_vec ord (act_size +1) n_unsign in + let correct_size_num = to_vec_int ord act_size n in + let one_more_size_u = to_vec_int ord (act_size +1) n_unsign in let overflow = if (n <= (int_of_big_int (get_max_representable_in sign len))) && (n >= (int_of_big_int (get_min_representable_in sign len))) then Vzero @@ -666,12 +741,12 @@ let rec arith_op_overflow_vec op sign size (l,r) = let c_out = most_significant one_more_size_u in (correct_size_num,overflow,c_out) -let add_overflow_vec = arith_op_overflow_vec (+) false 1 -let add_overflow_vec_signed = arith_op_overflow_vec (+) true 1 -let minus_overflow_vec = arith_op_overflow_vec (-) false 1 -let minus_overflow_vec_signed = arith_op_overflow_vec (-) true 1 -let mult_overflow_vec = arith_op_overflow_vec ( * ) false 2 -let mult_overflow_vec_signed = arith_op_overflow_vec ( * ) true 2 +let add_overflow_vec_int = arith_op_overflow_vec_int (+) false 1 +let add_overflow_vec_signed_int = arith_op_overflow_vec_int (+) true 1 +let minus_overflow_vec_int = arith_op_overflow_vec_int (-) false 1 +let minus_overflow_vec_signed_int = arith_op_overflow_vec_int (-) true 1 +let mult_overflow_vec_int = arith_op_overflow_vec_int ( * ) false 2 +let mult_overflow_vec_signed_int = arith_op_overflow_vec_int ( * ) true 2 let rec arith_op_overflow_vec_big op sign size (l,r) = let ord = get_ord l in @@ -697,18 +772,25 @@ let minus_overflow_vec_signed_big = arith_op_overflow_vec_big sub_big_int true u let mult_overflow_vec_big = arith_op_overflow_vec_big mult_big_int false two_big_int let mult_overflow_vec_signed_big = arith_op_overflow_vec_big mult_big_int true two_big_int -let rec arith_op_overflow_vec_bit op sign (l,r_bit) = +let add_overflow_vec = add_overflow_vec_big +let add_overflow_vec_signed = add_overflow_vec_signed_big +let minus_overflow_vec = minus_overflow_vec_big +let minus_overflow_vec_signed = minus_overflow_vec_signed_big +let mult_overflow_vec = mult_overflow_vec_big +let mult_overflow_vec_signed = mult_overflow_vec_signed_big + +let rec arith_op_overflow_vec_bit_int op sign (l,r_bit) = let ord = get_ord l in let act_size = length l in - let l' = to_num sign l in - let l_u = to_num false l in + let l' = to_num_int sign l in + let l_u = to_num_int false l in let (n,nu,changed) = match r_bit with | Vone -> (arith_op op (l',1), arith_op op (l_u,1), true) | Vzero -> (l',l_u,false) | _ -> assert false in - let correct_size_num = to_vec ord act_size n in - let one_larger = to_vec ord (1+ act_size) nu in + let correct_size_num = to_vec_int ord act_size n in + let one_larger = to_vec_int ord (1+ act_size) nu in let overflow = if changed then if (n <= (int_of_big_int (get_max_representable_in sign act_size))) && @@ -718,9 +800,9 @@ let rec arith_op_overflow_vec_bit op sign (l,r_bit) = else Vone in (correct_size_num,overflow,most_significant one_larger) -let add_overflow_vec_bit_signed = arith_op_overflow_vec_bit (+) true -let minus_overflow_vec_bit = arith_op_overflow_vec_bit (-) false -let minus_overflow_vec_bit_signed = arith_op_overflow_vec_bit (-) true +let add_overflow_vec_bit_signed_int = arith_op_overflow_vec_bit_int (+) true +let minus_overflow_vec_bit_int = arith_op_overflow_vec_bit_int (-) false +let minus_overflow_vec_bit_signed_int = arith_op_overflow_vec_bit_int (-) true let rec arith_op_overflow_vec_bit_big op sign (l,r_bit) = let ord = get_ord l in @@ -747,8 +829,11 @@ let add_overflow_vec_bit_signed_big = arith_op_overflow_vec_bit_big add_big_int let minus_overflow_vec_bit_big = arith_op_overflow_vec_bit_big sub_big_int false let minus_overflow_vec_bit_signed_big = arith_op_overflow_vec_bit_big sub_big_int true +let add_overflow_vec_bit_signed = add_overflow_vec_bit_signed_big +let minus_overflow_vec_bit = minus_overflow_vec_bit_big +let minus_overflow_vec_bit_signed = minus_overflow_vec_bit_signed_big -let shift_op_vec op (l,r) = +let shift_op_vec_int op (l,r) = match l with | Vvector(_,start,ord) | Vregister(_,start,ord,_) -> let array = match l with | Vvector(array,_,_) -> array | Vregister(array,_,_,_) -> !array | _ -> assert false in @@ -756,49 +841,46 @@ let shift_op_vec op (l,r) = (match op with | "<<" -> let right_vec = Vvector(Array.make r Vzero,0,true) in - let left_vec = vector_subrange l r (if ord then len + start else start - len) in + let left_vec = vector_subrange_int l r (if ord then len + start else start - len) in vector_concat left_vec right_vec | ">>" -> - let right_vec = vector_subrange l start r in + let right_vec = vector_subrange_int l start r in let left_vec = Vvector(Array.make r Vzero,0,true) in vector_concat left_vec right_vec | "<<<" -> - let left_vec = vector_subrange l r (if ord then len + start else start - len) in - let right_vec = vector_subrange l start r in + let left_vec = vector_subrange_int l r (if ord then len + start else start - len) in + let right_vec = vector_subrange_int l start r in vector_concat left_vec right_vec | _ -> assert false) | _ -> assert false -let bitwise_leftshift = shift_op_vec "<<" -let bitwise_rightshift = shift_op_vec ">>" -let bitwise_rotate = shift_op_vec "<<<" - -let shift_op_vec_big op (l,r) = shift_op_vec op (l, int_of_big_int r) +let shift_op_vec_big op (l,r) = shift_op_vec_int op (l, int_of_big_int r) let bitwise_leftshift_big = shift_op_vec_big "<<" let bitwise_rightshift_big = shift_op_vec_big ">>" let bitwise_rotate_big = shift_op_vec_big "<<<" - + +let bitwise_leftshift = bitwise_leftshift_big +let bitwise_rightshift = bitwise_rightshift_big +let bitwise_rotate = bitwise_rotate_big + let rec arith_op_no0_big op (l,r) = if eq_big_int r zero_big_int then None else Some (op l r) -let modulo_big = arith_op_no0_big mod_big_int -let quot_big = arith_op_no0_big div_big_int +let modulo_no0_big = arith_op_no0_big mod_big_int +let quot_no0_big = arith_op_no0_big div_big_int -let rec arith_op_no0 op (l,r) = +let rec arith_op_no0_int op (l,r) = if r = 0 then None else Some (op l r) -let modulo = arith_op (mod) -let quot = arith_op (/) - -let rec arith_op_vec_no0 op sign size (l,r) = +let rec arith_op_vec_no0_int op sign size (l,r) = let ord = get_ord l in let act_size = ((length l) * size) in - let (l',r') = (to_num sign l,to_num sign r) in - let n = arith_op_no0 op (l',r') in + let (l',r') = (to_num_int sign l,to_num_int sign r) in + let n = arith_op_no0_int op (l',r') in let representable,n' = match n with | Some n' -> @@ -806,16 +888,16 @@ let rec arith_op_vec_no0 op sign size (l,r) = (n' >= (int_of_big_int (get_min_representable_in sign act_size)))), n' | _ -> false,0 in if representable - then to_vec ord act_size n' + then to_vec_int ord act_size n' else match l with | Vvector(_, start, _) | Vregister(_, start, _, _) -> Vvector((Array.make act_size Vundef), start, ord) | _ -> assert false -let mod_vec = arith_op_vec_no0 (mod) false 1 -let quot_vec = arith_op_vec_no0 (/) false 1 -let quot_vec_signed = arith_op_vec_no0 (/) true 1 +let mod_vec_int = arith_op_vec_no0_int (mod) false 1 +let quot_vec_int = arith_op_vec_no0_int (/) false 1 +let quot_vec_signed_int = arith_op_vec_no0_int (/) true 1 let rec arith_op_vec_no0_big op sign size (l,r) = let ord = get_ord l in @@ -840,14 +922,18 @@ let mod_vec_big = arith_op_vec_no0_big mod_big_int false unit_big_int let quot_vec_big = arith_op_vec_no0_big div_big_int false unit_big_int let quot_vec_signed_big = arith_op_vec_no0_big div_big_int true unit_big_int -let arith_op_overflow_no0_vec op sign size (l,r) = +let mod_vec = mod_vec_big +let quot_vec = quot_vec_big +let quot_vec_signed = quot_vec_signed_big + +let arith_op_overflow_no0_vec_int op sign size (l,r) = let ord = get_ord l in let rep_size = (length r) * size in let act_size = (length l) * size in - let (l',r') = ((to_num sign l),(to_num sign r)) in - let (l_u,r_u) = (to_num false l,to_num false r) in - let n = arith_op_no0 op (l',r') in - let n_u = arith_op_no0 op (l_u,r_u) in + let (l',r') = ((to_num_int sign l),(to_num_int sign r)) in + let (l_u,r_u) = (to_num_int false l,to_num_int false r) in + let n = arith_op_no0_int op (l',r') in + let n_u = arith_op_no0_int op (l_u,r_u) in let representable,n',n_u' = match n, n_u with | Some n',Some n_u' -> @@ -856,7 +942,7 @@ let arith_op_overflow_no0_vec op sign size (l,r) = | _ -> true,0,0 in let (correct_size_num,one_more) = if representable then - (to_vec ord act_size n',to_vec ord (1+act_size) n_u') + (to_vec_int ord act_size n',to_vec_int ord (1+act_size) n_u') else match l with | Vvector(_, start, _) | Vregister(_, start, _, _) -> Vvector((Array.make act_size Vundef), start, ord), @@ -865,8 +951,8 @@ let arith_op_overflow_no0_vec op sign size (l,r) = let overflow = if representable then Vzero else Vone in (correct_size_num,overflow,most_significant one_more) -let quot_overflow_vec = arith_op_overflow_no0_vec (/) false 1 -let quot_overflow_vec_signed = arith_op_overflow_no0_vec (/) true 1 +let quot_overflow_vec_int = arith_op_overflow_no0_vec_int (/) false 1 +let quot_overflow_vec_signed_int = arith_op_overflow_no0_vec_int (/) true 1 let arith_op_overflow_no0_vec_big op sign size (l,r) = let ord = get_ord l in @@ -896,11 +982,15 @@ let arith_op_overflow_no0_vec_big op sign size (l,r) = let quot_overflow_vec_big = arith_op_overflow_no0_vec_big div_big_int false unit_big_int let quot_overflow_vec_signed_big = arith_op_overflow_no0_vec_big div_big_int true unit_big_int -let arith_op_vec_range_no0 op sign size (l,r) = +let quot_overflow_vec = quot_overflow_vec_big +let quot_overflow_vec_signed = quot_overflow_vec_signed_big + + +let arith_op_vec_range_no0_int op sign size (l,r) = let ord = get_ord l in - arith_op_vec_no0 op sign size (l,(to_vec ord (length l) r)) + arith_op_vec_no0_int op sign size (l,(to_vec_int ord (length l) r)) -let mod_vec_range = arith_op_vec_range_no0 (mod) false 1 +let mod_vec_range_int = arith_op_vec_range_no0_int (mod) false 1 let arith_op_vec_range_no0_big op sign size (l,r) = let ord = get_ord l in @@ -908,13 +998,17 @@ let arith_op_vec_range_no0_big op sign size (l,r) = let mod_vec_range_big = arith_op_vec_range_no0_big mod_big_int false unit_big_int +let mod_vec_range = mod_vec_range_big + (*Need to have a default top level direction reference I think*) -let duplicate (bit,length) = +let duplicate_int (bit,length) = Vvector((Array.make length bit), 0, true) let duplicate_big (bit,length) = Vvector((Array.make (int_of_big_int length) bit), 0, true) +let duplicate = duplicate_big + let compare_op op (l,r) = if (op l r) then Vone @@ -924,27 +1018,32 @@ let lt_big = compare_op lt_big_int let gt_big = compare_op gt_big_int let lteq_big = compare_op le_big_int let gteq_big = compare_op ge_big_int -let lt : (int* int) -> vbit = compare_op (<) -let gt : (int * int) -> vbit = compare_op (>) -let lteq : (int * int) -> vbit = compare_op (<=) -let gteq : (int*int) -> vbit = compare_op (>=) - -let compare_op_vec op sign (l,r) = - let (l',r') = (to_num sign l, to_num sign r) in +let lt_int : (int* int) -> vbit = compare_op (<) +let gt_int : (int * int) -> vbit = compare_op (>) +let lteq_int : (int * int) -> vbit = compare_op (<=) +let gteq_int : (int*int) -> vbit = compare_op (>=) + +let lt = lt_big +let gt = gt_big +let lteq = lteq_big +let gteq = gteq_big + +let compare_op_vec_int op sign (l,r) = + let (l',r') = (to_num_int sign l, to_num_int sign r) in compare_op op (l',r') -let lt_vec = compare_op_vec (<) true -let gt_vec = compare_op_vec (>) true -let lteq_vec = compare_op_vec (<=) true -let gteq_vec = compare_op_vec (>=) true -let lt_vec_signed = compare_op_vec (<) true -let gt_vec_signed = compare_op_vec (>) true -let lteq_vec_signed = compare_op_vec (<=) true -let gteq_vec_signed = compare_op_vec (>=) true -let lt_vec_unsigned = compare_op_vec (<) false -let gt_vec_unsigned = compare_op_vec (>) false -let lteq_vec_unsigned = compare_op_vec (<=) false -let gteq_vec_unsigned = compare_op_vec (>=) false +let lt_vec_int = compare_op_vec_int (<) true +let gt_vec_int = compare_op_vec_int (>) true +let lteq_vec_int = compare_op_vec_int (<=) true +let gteq_vec_int = compare_op_vec_int (>=) true +let lt_vec_signed_int = compare_op_vec_int (<) true +let gt_vec_signed_int = compare_op_vec_int (>) true +let lteq_vec_signed_int = compare_op_vec_int (<=) true +let gteq_vec_signed_int = compare_op_vec_int (>=) true +let lt_vec_unsigned_int = compare_op_vec_int (<) false +let gt_vec_unsigned_int = compare_op_vec_int (>) false +let lteq_vec_unsigned_int = compare_op_vec_int (<=) false +let gteq_vec_unsigned_int = compare_op_vec_int (>=) false let compare_op_vec_big op sign (l,r) = let (l',r') = (to_num_big sign l, to_num_big sign r) in @@ -963,14 +1062,26 @@ let gt_vec_unsigned_big = compare_op_vec_big gt_big_int false let lteq_vec_unsigned_big = compare_op_vec_big le_big_int false let gteq_vec_unsigned_big = compare_op_vec_big ge_big_int false - -let compare_op_vec_range op sign (l,r) = - compare_op op ((to_num sign l),r) - -let lt_vec_range = compare_op_vec_range (<) true -let gt_vec_range = compare_op_vec_range (>) true -let lteq_vec_range = compare_op_vec_range (<=) true -let gteq_vec_range = compare_op_vec_range (>=) true +let lt_vec = lt_vec_big +let gt_vec = gt_vec_big +let lteq_vec = lteq_vec_big +let gteq_vec = gteq_vec_big +let lt_vec_signed = lt_vec_signed_big +let gt_vec_signed = gt_vec_signed_big +let lteq_vec_signed = lteq_vec_signed_big +let gteq_vec_signed = gteq_vec_signed_big +let lt_vec_unsigned = lt_vec_unsigned_big +let gt_vec_unsigned = gt_vec_unsigned_big +let lteq_vec_unsigned = lteq_vec_unsigned_big +let gteq_vec_unsigned = gteq_vec_unsigned_big + +let compare_op_vec_range_int op sign (l,r) = + compare_op op ((to_num_int sign l),r) + +let lt_vec_range_int = compare_op_vec_range_int (<) true +let gt_vec_range_int = compare_op_vec_range_int (>) true +let lteq_vec_range_int = compare_op_vec_range_int (<=) true +let gteq_vec_range_int = compare_op_vec_range_int (>=) true let compare_op_vec_range_big op sign (l,r) = compare_op op ((to_num_big sign l),r) @@ -980,13 +1091,18 @@ let gt_vec_range_big = compare_op_vec_range_big gt_big_int true let lteq_vec_range_big = compare_op_vec_range_big le_big_int true let gteq_vec_range_big = compare_op_vec_range_big ge_big_int true -let compare_op_range_vec op sign (l,r) = - compare_op op (l, (to_num sign r)) +let lt_vec_range = lt_vec_range_big +let gt_vec_range = gt_vec_range_big +let lteq_vec_range = lteq_vec_range_big +let gteq_vec_range = gteq_vec_range_big + +let compare_op_range_vec_int op sign (l,r) = + compare_op op (l, (to_num_int sign r)) -let lt_range_vec = compare_op_range_vec (<) true -let gt_range_vec = compare_op_range_vec (>) true -let lteq_range_vec = compare_op_range_vec (<=) true -let gteq_range_vec = compare_op_range_vec (>=) true +let lt_range_vec_int = compare_op_range_vec_int (<) true +let gt_range_vec_int = compare_op_range_vec_int (>) true +let lteq_range_vec_int = compare_op_range_vec_int (<=) true +let gteq_range_vec_int = compare_op_range_vec_int (>=) true let compare_op_range_vec_big op sign (l,r) = compare_op op (l, (to_num_big sign r)) @@ -996,12 +1112,16 @@ let gt_range_vec_big = compare_op_range_vec_big gt_big_int true let lteq_range_vec_big = compare_op_range_vec_big le_big_int true let gteq_range_vec_big = compare_op_range_vec_big ge_big_int true +let lt_range_vec = lt_range_vec_big +let gt_range_vec = gt_range_vec_big +let lteq_range_vec = lteq_range_vec_big +let gteq_range_vec = gteq_range_vec_big let eq (l,r) = if l == r then Vone else Vzero -let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) +let eq_vec_vec (l,r) = eq (to_num_big true l, to_num_big true r) let eq_vec (l,r) = eq_vec_vec(l,r) -let eq_vec_range (l,r) = eq (to_num false l,r) -let eq_range_vec (l,r) = eq (l, to_num false r) +let eq_vec_range (l,r) = eq (to_num_big false l,r) +let eq_range_vec (l,r) = eq (l, to_num_big false r) let eq_range = eq let eq_bit = bitwise_binop_bit (=) @@ -1009,23 +1129,28 @@ let neq (l,r) = bitwise_not_bit (eq (l,r)) let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec(l,r)) let neq_bit (l,r) = bitwise_not_bit (eq_bit(l,r)) -let mask (n,v) = match v with +let mask (n,v) = + let n' = int_of_big_int n in + match v with | Vvector (bits,start,dir) -> let current_size = Array.length bits in - let to_drop = (current_size - n) in - let bits' = Array.sub bits to_drop n in - Vvector (bits',(if dir then 0 else n-1), dir) + let to_drop = (current_size - n') in + let bits' = Array.sub bits to_drop n' in + Vvector (bits',(if dir then 0 else n'-1), dir) | VvectorR (bits,start,dir) -> let current_size = Array.length bits in - let to_drop = (current_size - n) in - let bits' = Array.sub bits to_drop n in - VvectorR (bits',(if dir then 0 else n-1), dir) + let to_drop = (current_size - n') in + let bits' = Array.sub bits to_drop n' in + VvectorR (bits',(if dir then 0 else n'-1), dir) | Vregister _ -> failwith "mask not implemented for Vregister" | Vbit _ -> failwith "mask called for bit" -let slice_raw (v, i, j) = match v with +let slice_raw (v, i, j) = + let i' = int_of_big_int i in + let j' = int_of_big_int j in + match v with | Vvector (bs, start, is_inc) -> - let bits = Array.sub bs i j in + let bits = Array.sub bs i' (j'-i'+1) in let len = Array.length bits in Vvector (bits, (if is_inc then 0 else len - 1), is_inc) | _ -> failwith "slice_raw only implemented for VVector" |