path: root/src/lem_interp/interp_lib.lem

open import Pervasives
open import Interp
open import Interp_ast
import Assert_extra Maybe_extra (* For failwith for error reporting while debugging; and for fromJust when we know it's not Nothing *)
open import Num
open import List
open import Word
open import Bool

let hardware_mod (a: integer) (b:integer) : integer = 
 if a < 0 && b < 0
 then (abs a) mod (abs b)
 else if (a < 0 && b >= 0) 
 then (a mod b) - b
 else a mod b

let hardware_quot (a:integer) (b:integer) : integer = 
  if a < 0 && b < 0
  then (abs a) / (abs b)
  else if (a < 0 && b > 0) 
  then (a/b) + 1
  else a/b

val integer_of_string : string -> integer
declare ocaml target_rep function integer_of_string = `Big_int.big_int_of_string`

let (max_64 : integer) = integer_of_string  "9223372036854775807"
let (min_64 : integer) = integer_of_string "-9223372036854775808"
let (max_32 : integer) = integer_of_string "2147483647"
let (min_32 : integer) = integer_of_string "-2147483648"
let (min_8 : integer) = (integerFromNat 0) - (integerFromNat 128)
let (max_8 : integer) = (integerFromNat 127)
let (min_5 : integer) = (integerFromNat 0)-(integerFromNat 32)
let (max_5 : integer) = (integerFromNat 32)

val get_max_representable_in : nat -> integer
let get_max_representable_in n = 
  if (n = 64) then max_64
  else if (n=32) then max_32
  else if (n=8) then max_8
  else if (n=5) then max_5
  else 2**n - 1

val get_min_representable_in : nat -> integer
let get_min_representable_in n = 
  if (n = 64) then min_64
  else if (n=32) then min_32
  else if (n=8) then min_8
  else if (n=5) then min_5
  else 0-(2**n)


let rec carry_out v1 v2 c = 
  (match (v1,v2) with
    | ([],[]) -> c
    | (b1::v1,b2::v2) ->
      (match (b1,b2,c) with
	| (V_lit (L_aux L_one _), V_lit (L_aux L_one _), V_lit (L_aux L_one _)) -> (carry_out v1 v2 c) (*carry out*)
	| (V_lit (L_aux L_one _), V_lit (L_aux L_one _), V_lit (L_aux L_zero _)) -> (carry_out v1 v2 b1) (* carry out*)
	| (V_lit (L_aux L_one _), V_lit (L_aux L_zero _), V_lit (L_aux L_one _)) -> (carry_out v1 v2 c) (* carry out*)
	| (V_lit (L_aux L_one _), V_lit (L_aux L_zero _), V_lit (L_aux L_zero _)) -> (carry_out v1 v2 c) (* none *)
	| (V_lit (L_aux L_zero _), V_lit (L_aux L_one _), V_lit (L_aux L_one _)) -> (carry_out v1 v2 c) (* carry out *)
	| (V_lit (L_aux L_zero _), V_lit (L_aux L_one _), V_lit (L_aux L_zero _)) -> (carry_out v1 v2 c) (* none *)
	| (V_lit (L_aux L_zero _), V_lit (L_aux L_zero _), V_lit (L_aux L_one _)) -> (carry_out v1 v2 b1) (* none *)
	| (V_lit (L_aux L_zero _), V_lit (L_aux L_zero _), V_lit (L_aux L_zero _)) -> (carry_out v1 v2 c) (* none *)
       end)
   end)

let ignore_sail x = V_lit (L_aux L_unit Unknown) ;;

let compose f g x = f (V_tuple [g x]) ;;

let zeroi = integerFromNat 0
let onei = integerFromNat 1
let twoi = integerFromNat 2

let is_unknown v = match v with
  | V_unknown -> true
  | _ -> false
end 

let has_unknown v = match v with
  | V_vector _ _ vs -> List.any is_unknown vs
end

let rec sparse_walker update ni processed_length length ls df =
  if processed_length = length 
  then []
  else match ls with
  | [] -> replicate (natFromInteger (length - processed_length)) df
  | (i,v)::ls -> 
    if ni = i 
    then v::(sparse_walker update (update ni) (processed_length + 1) length ls df)
    else df::(sparse_walker update (update ni) (processed_length + 1) length ((i,v)::ls) df)
end

let rec fill_in_sparse v = match v with
  | V_vector_sparse first length inc ls df -> 
    V_vector first inc (sparse_walker (if inc then (fun (x: integer) -> x + onei) else (fun (x: integer) -> x - onei)) first zeroi length ls df)
  | V_unknown -> V_unknown
  | V_track v r -> taint (fill_in_sparse v) r
end    

let is_one v = match v with 
  | V_lit (L_aux (L_num n) lb) -> V_lit (L_aux (if n=1 then L_one else L_zero) lb)
  | V_track (V_lit (L_aux (L_num n) lb)) r -> V_track (V_lit (L_aux (if n=1 then L_one else L_zero) lb)) r
  | V_lit (L_aux b lb) -> V_lit (L_aux (if b = L_one then L_one else L_zero) lb)
  | V_track (V_lit (L_aux b lb)) r -> V_track (V_lit (L_aux (if b = L_one then L_one else L_zero) lb)) r
  | V_track V_unkown _ -> v
  | V_unknown -> v
end ;;

let rec lt_range (V_tuple[v1;v2]) = match (v1,v2) with 
  | (V_lit (L_aux (L_num l1) lr),V_lit (L_aux (L_num l2) ll)) ->
    if l1 < l2
    then V_lit (L_aux L_one Unknown)
    else V_lit (L_aux L_zero Unknown)
  | (V_track v1 r1, V_track v2 r2) -> 
    taint (lt_range (V_tuple [v1;v2])) (r1++r2)
  | (V_track v1 r1, v2) ->
    taint (lt_range (V_tuple [v1;v2])) r1
  | (v1,V_track v2 r2) ->
    taint (lt_range (V_tuple [v1;v2])) r2
  | (V_unknown,_) -> V_unknown
  | (_,V_unknown) -> V_unknown
end ;;

let bit_to_bool b = match b with
  | V_lit (L_aux L_zero _) -> false
  | V_track (V_lit (L_aux L_zero _)) _ -> false
  | V_lit (L_aux L_one _) -> true
  | V_track (V_lit (L_aux L_one _)) _ -> true
  end ;;
let bool_to_bit b = match b with
    false -> V_lit (L_aux L_zero Unknown)
  | true -> V_lit (L_aux L_one Unknown)
  end ;;

let bitwise_not_bit v = 
  let lit_not (L_aux l loc) = match l with
    | L_zero -> (V_lit (L_aux L_one loc))
    | L_one  -> (V_lit (L_aux L_zero loc)) end in
  match v with
  | V_lit lit -> lit_not lit
  | V_track (V_lit lit) r -> V_track (lit_not lit) r 
  | V_unknown -> v
  | V_track V_unknown r -> v
end;; 

let rec bitwise_not v =
  match v with
  | V_vector idx inc v ->
    V_vector idx inc (List.map bitwise_not_bit v)
  | V_unknown -> v
  | V_track bv r -> taint (bitwise_not bv) r
end ;;

let rec bitwise_binop_bit op op_s (V_tuple [x; y]) = match (x,y) with
  | (V_track x rx,V_track y ry) ->
    taint ((bitwise_binop_bit op op_s) (V_tuple[x; y])) (rx ++ ry)
  | (V_track x rx,y) ->
    taint ((bitwise_binop_bit op op_s) (V_tuple[x;y])) rx
  | (x,V_track y ry) ->
    taint ((bitwise_binop_bit op op_s) (V_tuple[x;y])) ry
  | (V_vector _ _ [b],y) -> bitwise_binop_bit op op_s (V_tuple [b; y])
  | (_,V_vector _ _ [b]) -> bitwise_binop_bit op op_s (V_tuple [x; b])
  | (V_unknown,_) -> V_unknown
  | (_,V_unknown) -> V_unknown
  | (V_lit (L_aux L_undef li), v) -> 
    (match op_s with 
      | "|" -> y
      | "&" -> x
      | "^" -> y
     end )
  | (v,V_lit (L_aux L_undef li)) ->
    (match op_s with
      | "|" -> x
      | "&" -> y
      | "^" -> y
     end)
  | _ -> bool_to_bit (op (bit_to_bool x) (bit_to_bool y))
end ;;

let rec bitwise_binop op op_s (V_tuple [v1;v2]) =
  match (v1,v2) with
  | (V_vector idx inc v, V_vector idx' inc' v') ->
  (* typechecker ensures inc = inc', idx = idx' and length v = length v' *)
    V_vector idx inc (List.map (fun (x,y) -> (bitwise_binop_bit op op_s (V_tuple[x; y]))) (List.zip v v'))
  | (V_track v1 r1, V_track v2 r2) ->
    taint (bitwise_binop op op_s (V_tuple [v1;v2])) (r1 ++ r2)
  | (V_track v1 r1,v2) ->
    taint (bitwise_binop op op_s (V_tuple [v1;v2])) r1
  | (v1,V_track v2 r2) ->
    taint (bitwise_binop op op_s (V_tuple [v1;v2])) r2
  | (V_unknown,_) -> V_unknown
  | (_,V_unknown) -> V_unknown
end ;;

type signed = Unsigned | Signed

(* BitSeq expects LSB first.
 * By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
 * hence MSB first.
 * http://en.wikipedia.org/wiki/Bit_numbering *)
let rec to_num signed v = 
  match v with
  | (V_vector idx inc l) ->
    if has_unknown v 
    then V_unknown
    else 
  (* Word library in Lem expects bitseq with LSB first *)
      let l = reverse l in
  (* Make sure the last bit is a zero to force unsigned numbers *)
      let l = (match signed with | Signed -> l | Unsigned -> l ++ [V_lit (L_aux L_zero Unknown)] end) in
      V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown)
  | V_unknown -> V_unknown
  | V_track v r -> taint (to_num signed v) r
end ;;

let rec to_vec_inc (V_tuple[v1;v2]) = match (v1,v2) with
  | (V_lit(L_aux (L_num len) _), (V_lit(L_aux (L_num n) ln))) ->
    let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
    V_vector 0 true (map bool_to_bit (reverse l)) 
  | (V_track v1 r1,V_track v2 r2) -> taint (to_vec_inc (V_tuple[v1;v2])) (r1++r2)
  | (V_track v1 r1,v2) -> taint (to_vec_inc (V_tuple[v1;v2])) r1
  | (v1,V_track v2 r2) -> taint (to_vec_inc (V_tuple[v1;v2])) r2
  | ((V_lit(L_aux (L_num n) ln)),V_unknown) -> 
    V_vector 0 true (List.replicate (natFromInteger n) V_unknown)
  | (_,V_unknown) -> V_unknown
  | (V_unknown,_) -> V_unknown
  | _ -> Assert_extra.failwith ("to_vec_inc parameters were " ^ (string_of_value (V_tuple[v1;v2])))
end
;;
let rec to_vec_dec (V_tuple([v1;v2])) = match (v1,v2) with 
  | (V_lit(L_aux (L_num len) _), (V_lit(L_aux (L_num n) ln))) ->
    let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
    V_vector (len - 1) false (map bool_to_bit (reverse l)) 
  | (V_track v1 r1,V_track v2 r2) -> taint (to_vec_dec (V_tuple[v1;v2])) (r1++r2)
  | (V_track v1 r1,v2) -> taint (to_vec_dec (V_tuple[v1;v2])) r1
  | (v1,V_track v2 r2) -> taint (to_vec_dec (V_tuple[v1;v2])) r2
  | ((V_lit(L_aux (L_num n) ln)),V_unknown) -> 
    V_vector (n-1) false (List.replicate (natFromInteger n) V_unknown)
  | (_,V_unknown) -> V_unknown
  | (V_unknown,_) -> V_unknown
  | _ -> Assert_extra.failwith ("to_vec_dec parameters were " ^ (string_of_value (V_tuple[v1;v2])))
end
;;
let to_vec ord len n =
  if ord
  then to_vec_inc (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
  else to_vec_dec (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
;;

let rec exts (V_tuple[v1;v]) = match v1 with
  | V_lit(L_aux (L_num len) _) -> (match v with
      | V_vector _ inc _  -> to_vec inc (natFromInteger len) (to_num Signed v)
      | V_unknown -> V_unknown
      | V_track v r2 -> taint (exts (V_tuple[v1;v])) r2 end)
  | V_unknown -> v1
  | V_track v1 r1 -> taint (exts (V_tuple[v1;v])) r1
end
;;

let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;;
(* XXX interpret vectors as unsigned numbers for equality *)
let eq_vec_range (V_tuple [v; r]) = eq (V_tuple [to_num Unsigned v; r]) ;;
let eq_range_vec (V_tuple [r; v]) = eq (V_tuple [r; to_num Unsigned v]) ;;
let eq_vec_vec (V_tuple [v;v2]) = eq (V_tuple [to_num Signed v; to_num Signed v2]);;

let rec neg v = match v with
  | V_lit (L_aux arg la) -> 
    V_lit (L_aux (match arg with
      | L_one -> L_zero
      | L_zero -> L_one end) la) 
  | V_unknown -> V_unknown
  | V_track v r -> taint (neg v) r
  | V_tuple [v] -> neg v
end 
;;

let neq = compose neg eq ;;

let neq_vec = compose neg eq_vec_vec

let rec arith_op op (V_tuple args) = match args with
  | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (op x y)) lx)
  | [V_track v1 r1;V_track v2 r2] -> taint (arith_op op (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1;v2] -> taint (arith_op op (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] -> taint (arith_op op (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  end ;;
let rec arith_op_vec op sign size (V_tuple args) = match args with
  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
    let (l1',l2') = (to_num sign l1,to_num sign l2) in
    let n = arith_op op (V_tuple [l1';l2']) in
    to_vec ord ((List.length cs) * size) n
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_vec op sign size (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1;v2] ->
    taint (arith_op_vec op sign size (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] ->
    taint (arith_op_vec op sign size (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
end ;;
let rec arith_op_vec_vec_range op sign (V_tuple args) = match args with
  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
    let (l1',l2') = (to_num sign l1,to_num sign l2) in
    arith_op op (V_tuple [l1';l2'])
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1;v2] ->
    taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] ->
    taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
end ;;
let rec arith_op_overflow_vec op sign size (V_tuple args) = match args with
  | [(V_vector b ord cs1 as l1);(V_vector _ _ cs2 as l2)] ->
    let act_size = (List.length cs1) * size in
    let (is_l1_unknown,is_l2_unknown) = ((has_unknown l1), (has_unknown l2)) in
    let (l1',l2') = (if is_l1_unknown then V_unknown else (to_num sign l1),
                     if is_l2_unknown then V_unknown else (to_num sign l2)) in
    let n = if is_l1_unknown || is_l2_unknown then V_unknown else arith_op op (V_tuple [l1';l2']) in
    let correct_size_num = to_vec ord act_size n in
    let overflow = if (is_l1_unknown || is_l2_unknown) then V_unknown 
      else (match n with 
	| V_lit (L_aux (L_num n') ln) -> 
	  if (n' <= (get_max_representable_in act_size)) &&
	     (n' >= (get_min_representable_in act_size))
	  then V_lit (L_aux L_zero ln)
	  else V_lit (L_aux L_one ln)
	| _ -> V_unknown end) in
    let c_out = if (is_l1_unknown || is_l2_unknown) then V_unknown
      else let detaint x = match x with | V_track v _ -> v | _ -> x end in
      (carry_out (List.reverse (List.map detaint cs1)) (List.reverse (List.map detaint cs2)) (V_lit (L_aux L_zero Unknown))) in
    V_tuple [correct_size_num;overflow;c_out]
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_overflow_vec op sign size (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1;v2] ->
    taint (arith_op_overflow_vec op sign size (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] ->
    taint (arith_op_overflow_vec op sign size (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_tuple [V_unknown;V_unknown;V_unknown]
  | [_;V_unknown] -> V_tuple [V_unknown;V_unknown;V_unknown]
end ;;
let rec arith_op_overflow_vec_bit op sign size (V_tuple args) = match args with
  | [(V_vector b ord cs as l1);(V_lit (L_aux L_one li))] ->
    let l1' = to_num sign l1 in
    let n = arith_op op (V_tuple [l1';(V_lit (L_aux (L_num 1) li))]) in
    let correct_size_num = to_vec ord ((List.length cs) * size) n in
    let one_larger = to_num Signed (to_vec ord (((List.length cs) * size) +1) n) in
    let overflow =  neq (V_tuple [correct_size_num;one_larger]) in
    V_tuple [correct_size_num;overflow;V_lit (L_aux L_zero Unknown)]
  | [(V_vector b ord cs as l1);(V_lit (L_aux L_zero li))] ->
    let l1' = to_num sign l1 in
    let n = arith_op op (V_tuple [l1';(V_lit (L_aux (L_num 0) li))]) in
    let correct_size_num = to_vec ord ((List.length cs) * size) n in
    let one_larger = to_num Signed (to_vec ord (((List.length cs) * size) +1) n) in
    let overflow =  neq (V_tuple [correct_size_num;one_larger]) in
    V_tuple [correct_size_num;overflow;V_lit (L_aux L_zero Unknown)]    
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_overflow_vec_bit op sign size (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1;v2] ->
    taint (arith_op_overflow_vec_bit op sign size (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] ->
    taint (arith_op_overflow_vec_bit op sign size (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_tuple [V_unknown;V_unknown;V_unknown]
  | [_;V_unknown] -> V_tuple [V_unknown;V_unknown;V_unknown]
end ;;


let rec arith_op_range_vec op sign size (V_tuple args) = match args with
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1; v2] ->
    taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] -> 
    taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  | [n; (V_vector _ ord cs as l2)] ->
    arith_op_vec op sign size (V_tuple [(to_vec ord (List.length cs) n);l2])
end ;;
let rec arith_op_vec_range op sign size (V_tuple args) = match args with
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1; v2] ->
    taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] -> 
    taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  | [(V_vector _ ord cs as l1);n] ->
    arith_op_vec op sign size (V_tuple [l1;(to_vec ord (List.length cs) n)])
end ;;
let rec arith_op_range_vec_range op sign (V_tuple args) = match args with
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_range_vec_range op sign (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1; v2] ->
    taint (arith_op_range_vec_range op sign (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] -> 
    taint (arith_op_range_vec_range op sign (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  | [n;(V_vector _ ord _ as l2)] ->
    arith_op op (V_tuple [n;(to_num Unsigned l2)])
end ;;
let rec arith_op_vec_range_range op sign (V_tuple args) = match args with
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_vec_range_range op sign (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1; v2] ->
    taint (arith_op_vec_range_range op sign (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] -> 
    taint (arith_op_vec_range_range op sign (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  | [(V_vector _ ord _ as l1);n] ->
    arith_op op (V_tuple [(to_num sign l1);n])
end ;;
let rec arith_op_vec_bit op sign size (V_tuple args) = match args with
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1; v2] ->
    taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] -> 
    taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  | [(V_vector _ ord cs as l1);V_lit (L_aux bit _)] ->
    let l1' = to_num sign l1 in
    let n = arith_op op (V_tuple 
			   [l1';
			    V_lit 
			      (L_aux (L_num (match bit with | L_one -> 1 | L_zero -> 0 end)) Unknown)])
    in
    to_vec ord ((List.length cs) * size) n
end 
;;
let rec arith_op_no0 op (V_tuple args) = match args with
  | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> 
    if y = 0 
    then V_lit (L_aux L_undef ly)
    else V_lit(L_aux (L_num (op x y)) lx)
  | [V_track v1 r1;V_track v2 r2] -> taint (arith_op_no0 op (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1;v2] -> taint (arith_op_no0 op (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] -> taint (arith_op_no0 op (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  end ;;

let rec arith_op_vec_no0 op op_s sign size (V_tuple args) = match args with
  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
    let act_size = (List.length cs) * size in
    let (is_l1_unknown,is_l2_unknown) = ((has_unknown l1), (has_unknown l2)) in
    let (l1',l2') = (if is_l1_unknown then V_unknown else (to_num sign l1),
                     if is_l2_unknown then V_unknown else (to_num sign l2)) in
    let n = if is_l1_unknown || is_l2_unknown then V_unknown else arith_op op (V_tuple [l1';l2']) in
    let representable = 
      match n with 
	| V_lit (L_aux (L_num n') ln) ->  
	  let rep_size = (if op_s = "quot" then act_size/2 else act_size) in
	  ((n' <= (get_max_representable_in act_size)) && (n' >= (get_min_representable_in act_size)))
	| _ -> true end in
    if representable then to_vec ord act_size n else to_vec ord act_size (V_lit (L_aux L_undef Unknown))
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_vec_no0 op op_s sign size (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1;v2] ->
    taint (arith_op_vec_no0 op op_s sign size (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] ->
    taint (arith_op_vec_no0 op op_s sign size (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
end ;;
let rec arith_op_overflow_vec_no0 op op_s sign size (V_tuple args) = match args with
  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
    let act_size = (List.length cs) * size in
    let (is_l1_unknown,is_l2_unknown) = ((has_unknown l1), (has_unknown l2)) in
    let (l1',l2') = (if is_l1_unknown then V_unknown else (to_num sign l1),
                     if is_l2_unknown then V_unknown else (to_num sign l2)) in
    let n = if is_l1_unknown || is_l2_unknown then V_unknown else arith_op op (V_tuple [l1';l2']) in
    let representable = 
      match n with 
	| V_lit (L_aux (L_num n') ln) ->  
	  let rep_size = (if op_s = "quot" then act_size/2 else act_size) in
	  ((n' <= (get_max_representable_in act_size)) && (n' >= (get_min_representable_in act_size)))
	| _ -> true end in
    let correct_size_num = if representable then to_vec ord act_size n else to_vec ord act_size (V_lit (L_aux L_undef Unknown)) in
    let overflow = if (has_unknown l1 || has_unknown l2) then V_unknown else 
	if representable then V_lit (L_aux L_zero Unknown) else V_lit (L_aux L_one Unknown) in
    V_tuple [correct_size_num;overflow;V_lit (L_aux L_zero Unknown)]
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_overflow_vec_no0 op op_s sign size (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1;v2] ->
    taint (arith_op_overflow_vec_no0 op op_s sign size (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] ->
    taint (arith_op_overflow_vec_no0 op op_s sign size (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_tuple [V_unknown;V_unknown;V_unknown]
  | [_;V_unknown] -> V_tuple [V_unknown;V_unknown;V_unknown]
end ;;

let rec arith_op_vec_range_no0 op op_s sign size (V_tuple args) = match args with
  | [V_track v1 r1;V_track v2 r2] ->
    taint (arith_op_vec_range_no0 op op_s sign size (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1; v2] ->
    taint (arith_op_vec_range_no0 op op_s sign size (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] -> 
    taint (arith_op_vec_range_no0 op op_s sign size (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  | [(V_vector _ ord cs as l1);n] ->
    arith_op_vec_no0 op op_s sign size (V_tuple [l1;(to_vec ord (List.length cs) n)])
end ;;

let rec compare_op op (V_tuple args) = match args with
  | [V_track v1 r1;V_track v2 r2] ->
    taint (compare_op op (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1;v2] ->
    taint (compare_op op (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] ->
    taint (compare_op op (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> 
    if (op x y)
    then V_lit(L_aux L_one lx)
    else V_lit(L_aux L_zero lx)
end ;;
let rec compare_op_vec op sign (V_tuple args) = match args with
  | [V_track v1 r1;V_track v2 r2] ->
    taint (compare_op_vec op sign (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1;v2] ->
    taint (compare_op_vec op sign (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] ->
    taint (compare_op_vec op sign (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  | [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
    let (l1',l2') = (to_num sign l1, to_num sign l2) in
    compare_op op (V_tuple[l1';l2'])
end ;;
let rec compare_op_vec_unsigned op (V_tuple args) = match args with
  | [V_track v1 r1;V_track v2 r2] ->
    taint (compare_op_vec_unsigned op (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1;v2] ->
    taint (compare_op_vec_unsigned op (V_tuple [v1;v2])) r1
  | [v1;V_track v2 r2] ->
    taint (compare_op_vec_unsigned op (V_tuple [v1;v2])) r2
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  | [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
    let (l1',l2') = (to_num Unsigned l1, to_num Unsigned l2) in
    compare_op op (V_tuple[l1';l2'])
end ;;



let rec duplicate (V_tuple args) = match args with
  | [V_track v1 r1;V_track v2 r2] -> taint (duplicate (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1; v2] -> taint (duplicate (V_tuple[v1;v2])) r1 
  | [v1;V_track v2 r2] -> taint (duplicate (V_tuple[v1;v2])) r2 
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  | [(V_lit _ as v);(V_lit (L_aux (L_num n) _))] ->
    (V_vector 0 true (List.replicate (natFromInteger n) v))
end

let rec vec_concat (V_tuple args) = match args with
  | [V_vector n d l; V_vector n' d' l'] ->
      (* XXX d = d' ? dropping n' ? *)
      V_vector n d (l ++ l')
  | [V_lit l; (V_vector n d l' as x)] -> vec_concat (V_tuple [litV_to_vec l d; x])
  | [(V_vector n d l' as x); V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l d]) 
  | [V_track v1 r1;V_track v2 r2] -> taint (vec_concat (V_tuple [v1;v2])) (r1++r2)
  | [V_track v1 r1; v2] -> taint (vec_concat (V_tuple[v1;v2])) r1 
  | [v1; V_track v2 r2] -> taint (vec_concat (V_tuple[v1;v2])) r2 
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  
  end ;;

let rec v_length v = match v with
  | V_vector n d l -> V_lit (L_aux (L_num (integerFromNat (List.length l))) Unknown)
  | V_unknown -> V_unknown
  | V_track v r -> taint (v_length v) r
end ;;

let function_map = [
  ("ignore", ignore_sail);            
  ("length", v_length);
  ("add", arith_op (+));
  ("add_vec", arith_op_vec (+) Unsigned 1);
  ("add_vec_range", arith_op_vec_range (+) Unsigned  1);
  ("add_vec_range_range", arith_op_vec_range_range (+) Unsigned);
  ("add_range_vec", arith_op_range_vec (+) Unsigned 1);
  ("add_range_vec_range", arith_op_range_vec_range (+) Unsigned);
  ("add_vec_vec_range", arith_op_vec_vec_range (+) Unsigned);
  ("add_vec_bit", arith_op_vec_bit (+) Unsigned 1);
  ("add_overflow_vec", arith_op_overflow_vec (+) Unsigned 1);
  ("add_signed", arith_op (+));
  ("add_vec_signed", arith_op_vec (+) Signed 1);
  ("add_vec_range_signed", arith_op_vec_range (+) Signed 1);
  ("add_vec_range_range_signed", arith_op_vec_range_range (+) Signed);
  ("add_range_vec_signed", arith_op_range_vec (+) Signed 1);
  ("add_range_vec_range_signed", arith_op_range_vec_range (+) Signed);
  ("add_vec_vec_range_signed", arith_op_vec_vec_range (+) Signed);
  ("add_vec_bit_signed", arith_op_vec_bit (+) Signed 1);
  ("add_overflow_vec_signed", arith_op_overflow_vec (+) Signed 1);
  ("add_overflow_vec_bit_signed", arith_op_overflow_vec_bit (+) Signed 1);
  ("minus", arith_op (-));
  ("minus_vec", arith_op_vec (-) Unsigned 1);
  ("minus_vec_range", arith_op_vec_range (-) Unsigned 1);
  ("minus_range_vec", arith_op_range_vec (-) Unsigned 1);
  ("minus_vec_range_range", arith_op_vec_range_range (-) Unsigned);
  ("minus_range_vec_range", arith_op_range_vec_range (-) Unsigned);
  ("minus_vec_bit", arith_op_vec_bit (-) Unsigned 1);
  ("minus_overflow_vec", arith_op_overflow_vec (-) Unsigned 1);
  ("multiply", arith_op ( * ));
  ("multiply_vec", arith_op_vec ( * ) Unsigned 2);
  ("mult_range_vec", arith_op_range_vec ( * ) Unsigned 2);
  ("mult_vec_range", arith_op_vec_range ( * ) Unsigned 2);
  ("mult_overflow_vec", arith_op_overflow_vec ( * ) Unsigned 2);
  ("multiply_vec_signed", arith_op_vec ( * ) Signed 2);
  ("mult_range_vec_signed", arith_op_range_vec ( * ) Signed 2);
  ("mult_vec_range_signed", arith_op_vec_range ( * ) Signed 2);
  ("mult_overflow_vec_signed", arith_op_overflow_vec ( * ) Signed 2);
  ("mod", arith_op_no0 (mod));
  ("mod_vec", arith_op_vec_no0 hardware_mod "mod" Unsigned 1);
  ("mod_vec_range", arith_op_vec_range_no0 hardware_mod "mod" Unsigned 1);
  ("quot", arith_op_no0 hardware_quot);
  ("quot_vec", arith_op_vec_no0 hardware_quot "quot" Unsigned 1);
  ("quot_overflow_vec", arith_op_overflow_vec_no0 hardware_quot "quot" Unsigned 1);
  ("quot_vec_signed", arith_op_vec_no0 hardware_quot "quot" Signed 1);
  ("quot_overflow_vec_signed", arith_op_overflow_vec_no0 hardware_quot "quot" Signed 1);
  ("eq", eq);
  ("eq_vec_range", eq_vec_range);
  ("eq_range_vec", eq_range_vec);
  ("neq", neq);
  ("vec_concat", vec_concat);
  ("is_one", is_one);
  ("to_num_inc", to_num Unsigned);
  ("to_num_dec", to_num Unsigned);
  ("EXTS", exts);
  ("to_vec_inc", to_vec_inc);
  ("to_vec_dec", to_vec_dec);
  ("bitwise_not", bitwise_not);
  ("bitwise_not_bit", bitwise_not_bit);
  ("bitwise_and", bitwise_binop (&&) "&");
  ("bitwise_or", bitwise_binop (||) "|");
  ("bitwise_xor", bitwise_binop xor "^");
  ("bitwise_and_bit", bitwise_binop_bit (&&) "&");
  ("bitwise_or_bit", bitwise_binop_bit (||) "|");
  ("bitwise_xor_bit", bitwise_binop_bit xor "^");
  ("lt", compare_op (<));
  ("gt", compare_op (>));
  ("lteq", compare_op (<=));
  ("gteq", compare_op (>=));
  ("lt_vec", compare_op_vec (<) Signed);
  ("gt_vec", compare_op_vec (>) Signed);
  ("lteq_vec", compare_op_vec (<=) Signed);
  ("gteq_vec", compare_op_vec (>=) Signed);
  ("lt_vec_signed", compare_op_vec (<) Signed);
  ("gt_vec_signed", compare_op_vec (>) Signed);
  ("lteq_vec_signed", compare_op_vec (<=) Signed);
  ("gteq_vec_signed", compare_op_vec (>=) Signed);
  ("lt_vec_unsigned", compare_op_vec (<) Unsigned);
  ("gt_vec_unsigned", compare_op_vec (>) Unsigned);
  ("lteq_vec_unsigned", compare_op_vec (<=) Unsigned);
  ("gteq_vec_unsigned", compare_op_vec (>=) Unsigned);
  ("ltu", compare_op_vec_unsigned (<));
  ("gtu", compare_op_vec_unsigned (>));
  ("duplicate", duplicate);
] ;;

let eval_external name v = match List.lookup name function_map with
  | Just f -> f v
  | Nothing -> Assert_extra.failwith ("missing library function " ^ name)
  end