Support int and bigint library functions

1 files changed, 438 insertions, 111 deletions

diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index 8a1a27c6..dc44ab5d 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -15,11 +15,14 @@ let to_bool = function
   | Vone  -> true
   | Vundef -> assert false
 
-let is_one i =
+let is_one_big i =
   if eq_big_int i unit_big_int
   then Vone
   else Vzero
 
+let is_one i =
+  if i = 1 then Vone else Vzero
+
 let get_barray  = function
   | Vvector(a,_,_) -> a
   | Vregister(a,_,_,_) -> !a
@@ -38,11 +41,13 @@ let get_start = function
   | _ -> assert false  
   
 let length = function
-  | Vvector(array,_,_) -> big_int_of_int (Array.length array)
-  | Vregister(array,_,_,_) -> big_int_of_int (Array.length !array)
-  | VvectorR(array,_,_) -> big_int_of_int (Array.length array)
+  | Vvector(array,_,_) -> Array.length array
+  | Vregister(array,_,_,_) -> Array.length !array
+  | VvectorR(array,_,_) -> Array.length array
   | _ -> assert false
 
+let length_big v = big_int_of_int (length v)
+
 let read_register = function
   | Vregister(a,start,inc,_) -> Vvector(!a,start,inc)
   | v -> v
@@ -53,6 +58,8 @@ let vector_access v n = match v with
     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
   | Vvector(array,start,is_inc) ->
@@ -65,6 +72,8 @@ 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 vector_subrange v n m =
   let builder array length offset default =
     let new_array = Array.make length default in
@@ -87,6 +96,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 get_register_field_vec reg field =
   match reg with
   | Vregister(_,_,_,fields) ->
@@ -128,6 +139,9 @@ let set_vector_subrange_vec v n m new_v =
     walker array length offset 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
+
 let set_vector_subrange_bit v n m new_v =
   let walker array length offset new_values =
     begin
@@ -145,6 +159,9 @@ let set_vector_subrange_bit v n m new_v =
     walker !array length offset 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
+
 let set_register_field_v reg field new_v =
   match reg with
   | Vregister(array,start,dir,fields) ->
@@ -166,10 +183,10 @@ let set_register_field_bit reg field new_v =
   | _ -> ()
 
 let set_two_reg r1 r2 vec =
-  let size = int_of_big_int (length r1) in
+  let size = length r1 in
   let dir = get_ord r1 in
   let start = get_start vec in
-  let vsize = int_of_big_int (length 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)
       (if dir then vsize - start else start - vsize) in
@@ -186,6 +203,9 @@ let make_indexed_v entries default start size dir =
     VvectorR(array, start, dir)
   end
 
+let make_indexed_v_big entries default start size dir =
+  make_indexed_v entries default (int_of_big_int start) (int_of_big_int size) dir
+
 let make_indexed_bitv entries default start size dir =
   let default_value = match default with
     | None -> Vundef
@@ -196,6 +216,9 @@ let make_indexed_bitv entries default start size dir =
     Vvector(array, start, dir)
   end
 
+let make_indexed_bitv_big entries default start size dir =
+  make_indexed_bitv entries default (int_of_big_int start) (int_of_big_int size) dir
+
 let vector_concat l r =
   match l,r with
   | Vvector(arrayl,start,ord), Vvector(arrayr,_,_) ->
@@ -283,11 +306,44 @@ let bitwise_and = bitwise_binop (&&)
 let bitwise_or = bitwise_binop (||)
 let bitwise_xor = bitwise_binop (fun x y -> (1 = (if x then 1 else 0) lxor (if y then 0 else 1)))
 
+let rec power_int base raiseto =
+  if raiseto = 0
+  then 1
+  else base * (power_int base (raiseto - 1))
+
 let unsigned = 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
+  | (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
+  | _ -> assert false
+
+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
@@ -313,12 +369,19 @@ let unsigned = function
 
 let signed v =
   match most_significant v with
-  | Vone -> minus_big_int(add_int_big_int 1 (unsigned (bitwise_not v)))
+  | Vone -> -(1 + (unsigned (bitwise_not v)))
   | Vzero -> unsigned v
   | _ -> assert false
 
+let signed_big v =
+  match most_significant v with
+  | Vone -> minus_big_int(add_int_big_int 1 (unsigned_big (bitwise_not v)))
+  | Vzero -> unsigned_big v
+  | _ -> assert false
+
 let to_num sign = if sign then signed else unsigned
-  
+let to_num_big sign = if sign then signed_big else unsigned_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))
 let max_64  = pred_big_int (power_big two_big_int (big_int_of_int 63))
@@ -347,12 +410,19 @@ let get_min_representable_in _ n =
   else minus_big_int (power_big two_big_int (big_int_of_int n))
 
 
-
-let rec divide_by_2 array i n =
+let rec divide_by_2_big array i n =
   if i < 0 || eq_big_int n zero_big_int
   then array
   else let (quo,modu) = quomod_big_int n two_big_int in
     if eq_big_int modu unit_big_int
+    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 =
+  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
 
@@ -367,16 +437,31 @@ let rec add_one_bit array co i =
     | Vundef,_ -> assert false
 
 let to_vec 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)
+  else
+    let abs_n = abs n in
+    let abs_array = divide_by_2 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)
+    | _ -> assert false
+
+let to_vec_big ord len n =
   let len = int_of_big_int len in
   let array = Array.make len Vzero in
   let start = if ord then 0 else len-1 in
   if eq_big_int n zero_big_int
   then Vvector(array, start, ord)
   else if gt_big_int n zero_big_int
-  then Vvector(divide_by_2 array (len -1) n, start, ord)
+  then Vvector(divide_by_2_big array (len -1) n, start, ord)
   else
     let abs_n = abs_big_int n in
-    let abs_array = divide_by_2 array (len-1) abs_n in
+    let abs_array = divide_by_2_big 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)
@@ -385,7 +470,15 @@ let to_vec ord len n =
 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_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 array = Array.make len Vundef in
+  let start = if ord then 0 else len-1 in
+  Vvector(array, start, ord)
+
+let to_vec_undef_big ord len = 
   let len = int_of_big_int len in
   let array = Array.make len Vundef in
   let start = if ord then 0 else len-1 in
@@ -394,86 +487,184 @@ let to_vec_undef ord len =
 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_big len = to_vec_undef_big true len
+let to_vec_dec_undef_big len = to_vec_undef_big false len
+
 let arith_op op (l,r) = op l r
-let add = arith_op add_big_int
-let add_signed = arith_op add_big_int
-let minus = arith_op sub_big_int
-let multiply = arith_op mult_big_int
-let modulo = arith_op mod_big_int
-let quot = arith_op div_big_int
-let power = arith_op power_big
+let add_big = arith_op add_big_int
+let add_signed_big = arith_op add_big_int
+let minus_big = arith_op sub_big_int
+let multiply_big = arith_op mult_big_int
+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 arith_op_vec_big op sign size (l,r) =
+  let ord = get_ord l in
+  let (l',r') = to_num_big sign l, to_num_big sign r in
+  let n = arith_op op (l',r') in
+  to_vec_big ord (mult_big_int size (length_big l)) n
+
+let add_vec_big = arith_op_vec_big add_big_int false unit_big_int
+let add_vec_signed_big = arith_op_vec_big add_big_int true unit_big_int
+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 ord = get_ord l in
   let (l',r') = to_num sign l, to_num sign r in
   let n = arith_op op (l',r') in
-  to_vec ord (mult_big_int size (length l)) n
+  to_vec ord (size * (length l)) n
 
-let add_vec = arith_op_vec add_big_int false unit_big_int
-let add_vec_signed = arith_op_vec add_big_int true unit_big_int
-let minus_vec = arith_op_vec sub_big_int false unit_big_int
-let multiply_vec = arith_op_vec mult_big_int false two_big_int
-let multiply_vec_signed = arith_op_vec mult_big_int true two_big_int
+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 arith_op_vec_range op sign size (l,r) =
   let ord = get_ord l in
   arith_op_vec op sign size (l, to_vec ord (length l) r)
 
-let add_vec_range = arith_op_vec_range add_big_int false unit_big_int
-let add_vec_range_signed = arith_op_vec_range add_big_int true unit_big_int
-let minus_vec_range = arith_op_vec_range sub_big_int false unit_big_int
-let mult_vec_range = arith_op_vec_range mult_big_int false two_big_int
-let mult_vec_range_signed = arith_op_vec_range mult_big_int true two_big_int
+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 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 mult_vec_range_signed_big = arith_op_vec_range_big mult_big_int true two_big_int
+
 
 let arith_op_range_vec op sign size (l,r) =
   let ord = get_ord r in
   arith_op_vec op sign size ((to_vec ord (length r) l), r)
 
-let add_range_vec = arith_op_range_vec add_big_int false unit_big_int
-let add_range_vec_signed = arith_op_range_vec add_big_int true unit_big_int
-let minus_range_vec = arith_op_range_vec sub_big_int false unit_big_int
-let mult_range_vec = arith_op_range_vec mult_big_int false two_big_int
-let mult_range_vec_signed = arith_op_range_vec mult_big_int true two_big_int
+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 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 mult_range_vec_signed_big = arith_op_range_vec_big mult_big_int true two_big_int
+
 
 let arith_op_range_vec_range op sign (l,r) = arith_op op (l, to_num sign r)
 
-let add_range_vec_range = arith_op_range_vec_range add_big_int false
-let add_range_vec_range_signed = arith_op_range_vec_range add_big_int true
-let minus_range_vec_range = arith_op_range_vec_range sub_big_int false
+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 arith_op_range_vec_range_big op sign (l,r) = arith_op op (l, to_num_big sign r)
+
+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_vec_range_range = arith_op_vec_range_range add_big_int false
-let add_vec_range_range_signed = arith_op_vec_range_range add_big_int true
-let minus_vec_range_range = arith_op_vec_range_range sub_big_int false
+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_big op sign (l,r) = arith_op op (to_num_big sign l,r)
+
+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
   arith_op op (l',r')
 
-let add_vec_vec_range = arith_op_vec_vec_range add_big_int false
-let add_vec_vec_range_signed = arith_op_vec_vec_range add_big_int true
+let add_vec_vec_range = arith_op_vec_vec_range (+) false
+let add_vec_vec_range_signed = arith_op_vec_vec_range (+) 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
+  arith_op op (l',r')
 
-let arith_op_vec_bit op sign size (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 ord = get_ord l in
   let l' = to_num sign l in
+  let n = arith_op op (l', match r with | Vone -> 1 | _ -> 0) in
+  to_vec 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 arith_op_vec_bit_big op sign (l,r) =
+  let ord = get_ord l in
+  let l' = to_num_big sign l in
   let n = arith_op op (l', match r with | Vone -> unit_big_int | _ -> zero_big_int) in
-  to_vec ord (mult_big_int (length l) size) n
+  to_vec_big ord (length_big l) n
     
-let add_vec_bit = arith_op_vec_bit add_big_int false unit_big_int
-let add_vec_bit_signed = arith_op_vec_bit add_big_int true unit_big_int
-let minus_vec_bit = arith_op_vec_bit sub_big_int true unit_big_int
+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 ord = get_ord l in
   let len = length l in
-  let act_size = mult_big_int len size 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 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 (succ_big_int act_size) n_unsign in
+  let one_more_size_u = to_vec 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
+    else Vone in
+  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 rec arith_op_overflow_vec_big op sign size (l,r) =
+  let ord = get_ord l in
+  let len = length_big l in
+  let act_size = mult_big_int len size in
+  let (l_sign,r_sign) = (to_num_big sign l,to_num_big sign r) in
+  let (l_unsign,r_unsign) = (to_num_big false l,to_num_big 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_big ord act_size n in
+  let one_more_size_u = to_vec_big ord (succ_big_int act_size) n_unsign in
   let overflow = if (le_big_int n (get_max_representable_in sign (int_of_big_int len))) &&
                     (ge_big_int n (get_min_representable_in sign (int_of_big_int len)))
     then Vzero
@@ -481,25 +672,50 @@ 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 add_big_int false unit_big_int
-let add_overflow_vec_signed = arith_op_overflow_vec add_big_int true unit_big_int
-let minus_overflow_vec = arith_op_overflow_vec sub_big_int false unit_big_int
-let minus_overflow_vec_signed = arith_op_overflow_vec sub_big_int true unit_big_int
-let mult_overflow_vec = arith_op_overflow_vec mult_big_int false two_big_int
-let mult_overflow_vec_signed = arith_op_overflow_vec mult_big_int true two_big_int
-    
-let rec arith_op_overflow_vec_bit op sign size (l,r_bit) =
+let add_overflow_vec_big = arith_op_overflow_vec_big add_big_int false unit_big_int
+let add_overflow_vec_signed_big = arith_op_overflow_vec_big add_big_int true unit_big_int
+let minus_overflow_vec_big = arith_op_overflow_vec_big sub_big_int false unit_big_int
+let minus_overflow_vec_signed_big = arith_op_overflow_vec_big sub_big_int true unit_big_int
+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 ord = get_ord l in
-  let act_size = mult_big_int (length l) size in
+  let act_size = length l in
   let l' = to_num sign l in
   let l_u = to_num false l in
   let (n,nu,changed) = match r_bit with
-    | Vone -> (arith_op op (l',unit_big_int), arith_op op (l_u,unit_big_int), true)
+    | 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 (succ_big_int act_size) nu in
+  let one_larger = to_vec ord (1+ act_size) nu in
+  let overflow =
+    if changed 
+    then if (n <= (int_of_big_int (get_max_representable_in sign act_size))) &&
+            (n >= (int_of_big_int (get_min_representable_in sign act_size)))
+      then Vzero
+      else Vone 
+    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 rec arith_op_overflow_vec_bit_big op sign (l,r_bit) =
+  let ord = get_ord l in
+  let act_size = length_big l in
+  let l' = to_num_big sign l in
+  let l_u = to_num_big false l in
+  let (n,nu,changed) = match r_bit with
+    | Vone -> (arith_op op (l',unit_big_int), arith_op op (l_u,unit_big_int), true)
+    | Vzero -> (l',l_u,false)
+    | _ -> assert false
+  in
+  let correct_size_num = to_vec_big ord act_size n in
+  let one_larger = to_vec_big ord (succ_big_int act_size) nu in
   let overflow =
     if changed 
     then if (le_big_int n (get_max_representable_in sign (int_of_big_int act_size))) &&
@@ -509,28 +725,28 @@ let rec arith_op_overflow_vec_bit op sign size (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 add_big_int true unit_big_int
-let minus_overflow_vec_bit = arith_op_overflow_vec_bit sub_big_int false unit_big_int
-let minus_overflow_vec_bit_signed = arith_op_overflow_vec_bit sub_big_int true unit_big_int
-    
+let add_overflow_vec_bit_signed_big = arith_op_overflow_vec_bit_big add_big_int true
+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 shift_op_vec 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
     let len = Array.length array in
-    let n = int_of_big_int r in
     (match op with
      | "<<" ->
-       let right_vec = Vvector(Array.make n Vzero,0,true) in
-       let left_vec = vector_subrange l n (if ord then len + start else start - len) in
+       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
        vector_concat left_vec right_vec
      | ">>" ->
-       let right_vec = vector_subrange l start n in
-       let left_vec = Vvector(Array.make n Vzero,0,true) in
+       let right_vec = vector_subrange 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 n (if ord then len + start else start - len) in
-       let right_vec = vector_subrange l start n in
+       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
        vector_concat left_vec right_vec
      | _ -> assert false)
   | _ -> assert false
@@ -539,41 +755,77 @@ let bitwise_leftshift = shift_op_vec "<<"
 let bitwise_rightshift = shift_op_vec ">>"
 let bitwise_rotate = shift_op_vec "<<<"
 
-let rec arith_op_no0 op (l,r) = 
+let shift_op_vec_big op (l,r) = shift_op_vec 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 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 = arith_op_no0 mod_big_int
-let quot = arith_op_no0 div_big_int
+let modulo_big = arith_op_no0_big mod_big_int
+let quot_big = arith_op_no0_big div_big_int
+
+let rec arith_op_no0 op (l,r) = 
+  if r = 0
+  then None
+  else Some (op l r)
+
+let modulo = arith_op_no0 (mod)
+let quot = arith_op_no0 (/)
 
 let rec arith_op_vec_no0 op sign size (l,r) =
   let ord = get_ord l in
-  let act_size = int_of_big_int (mult_big_int (length l) size) 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 representable,n' = 
     match n with 
     | Some n' ->  
+      ((n' <= (int_of_big_int (get_max_representable_in sign act_size))) &&
+       (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'
+  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 rec arith_op_vec_no0_big op sign size (l,r) =
+  let ord = get_ord l in
+  let act_size = int_of_big_int (mult_int_big_int (length l) size) in
+  let (l',r') = (to_num_big sign l,to_num_big sign r) in
+  let n = arith_op_no0_big op (l',r') in
+  let representable,n' = 
+    match n with 
+    | Some n' ->  
       ((le_big_int n' (get_max_representable_in sign act_size)) &&
        (ge_big_int n' (get_min_representable_in sign act_size))), n'
     | _ -> false,zero_big_int in
   if representable 
-  then to_vec ord (big_int_of_int act_size) n'
+  then to_vec_big ord (big_int_of_int 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_big_int false unit_big_int
-let quot_vec = arith_op_vec_no0 div_big_int false unit_big_int
-let quot_vec_signed = arith_op_vec_no0 div_big_int true unit_big_int
+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 ord = get_ord l in
-  let rep_size = mult_big_int (length r) size in
-  let act_size = mult_big_int (length l) size 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
@@ -581,12 +833,40 @@ let arith_op_overflow_no0_vec op sign size (l,r) =
   let representable,n',n_u' = 
     match n, n_u with 
     | Some n',Some n_u' ->  
+      ((n' <= (int_of_big_int (get_max_representable_in sign rep_size))) &&
+       (n' >= (int_of_big_int (get_min_representable_in sign rep_size))), n', n_u')
+    | _ -> 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')
+    else match l with 
+      | Vvector(_, start, _) | Vregister(_, start, _, _) ->
+        Vvector((Array.make act_size Vundef), start, ord),
+        Vvector((Array.make  (act_size + 1) Vundef), start, ord)
+      | _ -> assert false in
+  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 arith_op_overflow_no0_vec_big op sign size (l,r) =
+  let ord = get_ord l in
+  let rep_size = mult_big_int (length_big r) size in
+  let act_size = mult_big_int (length_big l) size in
+  let (l',r') = ((to_num_big sign l),(to_num_big sign r)) in
+  let (l_u,r_u) = (to_num_big false l,to_num_big false r) in
+  let n = arith_op_no0_big op (l',r') in
+  let n_u = arith_op_no0_big op (l_u,r_u) in
+  let representable,n',n_u' = 
+    match n, n_u with 
+    | Some n',Some n_u' ->  
       ((le_big_int n' (get_max_representable_in sign (int_of_big_int rep_size))) &&
        (ge_big_int n' (get_min_representable_in sign (int_of_big_int rep_size))), n', n_u')
     | _ -> true,zero_big_int,zero_big_int in
   let (correct_size_num,one_more) = 
     if representable then
-      (to_vec ord act_size n',to_vec ord (succ_big_int act_size) n_u')
+      (to_vec_big ord act_size n',to_vec_big ord (succ_big_int act_size) n_u')
     else match l with 
       | Vvector(_, start, _) | Vregister(_, start, _, _) ->
         Vvector((Array.make (int_of_big_int act_size) Vundef), start, ord),
@@ -595,62 +875,109 @@ 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 div_big_int false unit_big_int 
-let quot_overflow_vec_signed = arith_op_overflow_no0_vec div_big_int true unit_big_int 
+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 ord = get_ord l in
   arith_op_vec_no0 op sign size (l,(to_vec ord (length l) r))
 
-let mod_vec_range = arith_op_vec_range_no0 mod_big_int false unit_big_int
+let mod_vec_range = arith_op_vec_range_no0 (mod) false 1
+
+let arith_op_vec_range_no0_big op sign size (l,r) =
+  let ord = get_ord l in
+  arith_op_vec_no0_big op sign size (l,(to_vec_big ord (length_big l) r))
+
+let mod_vec_range_big = arith_op_vec_range_no0_big mod_big_int false unit_big_int
 
 (*Need to have a default top level direction reference I think*)
 let duplicate (bit,length) =
-  Vvector((Array.make (int_of_big_int length) bit), 0, true)
+  Vvector((Array.make length bit), 0, true)
 
+let duplicate_big (bit,length) =
+  Vvector((Array.make (int_of_big_int length) bit), 0, true)
 
 let compare_op op (l,r) =
   if (op l r)
   then Vone
   else Vzero
 
-let lt = compare_op lt_big_int
-let gt = compare_op gt_big_int
-let lteq = compare_op le_big_int
-let gteq = compare_op ge_big_int
+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
   compare_op op (l',r')
 
-let lt_vec = compare_op_vec lt_big_int true
-let gt_vec = compare_op_vec gt_big_int true
-let lteq_vec = compare_op_vec le_big_int true
-let gteq_vec = compare_op_vec ge_big_int true
-let lt_vec_signed = compare_op_vec lt_big_int true
-let gt_vec_signed = compare_op_vec gt_big_int true
-let lteq_vec_signed = compare_op_vec le_big_int true
-let gteq_vec_signed = compare_op_vec ge_big_int true
-let lt_vec_unsigned = compare_op_vec lt_big_int false
-let gt_vec_unsigned = compare_op_vec gt_big_int false
-let lteq_vec_unsigned = compare_op_vec le_big_int false
-let gteq_vec_unsigned = compare_op_vec ge_big_int false
+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 compare_op_vec_big op sign (l,r) = 
+  let (l',r') = (to_num_big sign l, to_num_big sign r) in
+  compare_op op (l',r')
+
+let lt_vec_big = compare_op_vec_big lt_big_int true
+let gt_vec_big = compare_op_vec_big gt_big_int true
+let lteq_vec_big = compare_op_vec_big le_big_int true
+let gteq_vec_big = compare_op_vec_big ge_big_int true
+let lt_vec_signed_big = compare_op_vec_big lt_big_int true
+let gt_vec_signed_big = compare_op_vec_big gt_big_int true
+let lteq_vec_signed_big = compare_op_vec_big le_big_int true
+let gteq_vec_signed_big = compare_op_vec_big ge_big_int true
+let lt_vec_unsigned_big = compare_op_vec_big lt_big_int false
+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 lt_big_int true
-let gt_vec_range = compare_op_vec_range gt_big_int true
-let lteq_vec_range = compare_op_vec_range le_big_int true
-let gteq_vec_range = compare_op_vec_range ge_big_int true
+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 compare_op_vec_range_big op sign (l,r) = 
+  compare_op op ((to_num_big sign l),r)
+
+let lt_vec_range_big = compare_op_vec_range_big lt_big_int true
+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_range_vec = compare_op_range_vec lt_big_int true
-let gt_range_vec = compare_op_range_vec gt_big_int true
-let lteq_range_vec = compare_op_range_vec le_big_int true
-let gteq_range_vec = compare_op_range_vec ge_big_int true
+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 compare_op_range_vec_big op sign (l,r) =
+  compare_op op (l, (to_num_big sign r))
+
+let lt_range_vec_big = compare_op_range_vec_big lt_big_int true
+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 eq (l,r) = if l == r then Vone else Vzero
 let eq_vec_range (l,r) = eq (to_num false l,r)