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

type signed = Unsigned | Signed

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_64u : integer) = integer_of_string "18446744073709551615"
let (max_64 : integer) = integer_of_string  "9223372036854775807"
let (min_64 : integer) = integer_of_string "-9223372036854775808"
let (max_32u : integer) = integer_of_string "4294967295"
let (max_32 : integer) = integer_of_string "2147483647"
let (min_32 : integer) = integer_of_string "-2147483648"
let (max_8 : integer) = (integerFromNat 127)
let (min_8 : integer) = (integerFromNat 0) - (integerFromNat 128)
let (max_5 : integer) = (integerFromNat 31)
let (min_5 : integer) = (integerFromNat 0)-(integerFromNat 32)

val get_max_representable_in : signed -> nat -> integer
let get_max_representable_in sign n = 
  if (n = 64) then match sign with | Signed -> max_64 | Unsigned -> max_64u end
  else if (n=32) then match sign with | Signed -> max_32 | Unsigned -> max_32u end
  else if (n=8) then max_8
  else if (n=5) then max_5
  else match sign with | Signed -> 2**n - 1 | Unsigned -> 2**n end

val get_min_representable_in : signed -> 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 detaint 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 fill_in_sparse v = 
  retaint v (match detaint 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
    end)

let is_one v = 
  retaint v
    match detaint 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_lit (L_aux b lb) -> V_lit (L_aux (if b = L_one then L_one else L_zero) lb)
      | V_unknown -> v
end ;;

let lt_range (V_tuple[v1;v2]) = 
  let lr_helper 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_unknown,_) -> V_unknown
  | (_,V_unknown) -> V_unknown
  end in
  binary_taint lr_helper v1 v2

let bit_to_bool b = match detaint b with
  | V_lit (L_aux L_zero _) -> false
  | 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
  retaint v (match detaint v with
  | V_lit lit -> lit_not lit
  | V_unknown -> V_unknown end)

let rec bitwise_not v =
  retaint v (match detaint v with
  | V_vector idx inc v ->
    V_vector idx inc (List.map bitwise_not_bit v)
  | V_unknown -> V_unknown end)

let rec bitwise_binop_bit op op_s (V_tuple [x; y]) = 
  let b_b_b_help x y = match (x,y) with
  | (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 in
  binary_taint b_b_b_help x y

let rec bitwise_binop op op_s (V_tuple [v1;v2]) =
  let b_b_help 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_unknown,_) -> V_unknown
      | (_,V_unknown) -> V_unknown end in
  binary_taint b_b_help v1 v2

(* 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 to_num signed v = 
  retaint v   
    (match detaint v with
      | (V_vector idx inc l) ->
	if has_unknown v 
	then V_unknown
	else if l=[]
	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
     end)

let to_vec_inc (V_tuple[v1;v2]) = 
  let tv_help 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_lit(L_aux (L_num n) ln)),V_unknown) -> 
	V_vector 0 true (List.replicate (natFromInteger n) V_unknown)
      | ((V_lit(L_aux (L_num n) ln)),(V_lit (L_aux L_undef _))) -> 
	V_vector 0 true (List.replicate (natFromInteger n) v2)
      | (_,V_unknown) -> V_unknown
      | (V_unknown,_) -> V_unknown
      | _ -> Assert_extra.failwith ("to_vec_inc parameters were " ^ (string_of_value (V_tuple[v1;v2])))
  end in
  binary_taint tv_help v1 v2

let to_vec_dec (V_tuple([v1;v2])) =
  let tv_fun 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_lit(L_aux (L_num n) ln)),V_unknown) -> 
	V_vector (n-1) false (List.replicate (natFromInteger n) V_unknown)
      | ((V_lit(L_aux (L_num n) ln)),(V_lit (L_aux L_undef _))) -> 
	V_vector (n-1) false (List.replicate (natFromInteger n) v2)
      | (_,V_unknown) -> V_unknown
      | (V_unknown,_) -> V_unknown
      | _ -> Assert_extra.failwith ("to_vec_dec parameters were " ^ (string_of_value (V_tuple[v1;v2])))
   end in
  binary_taint tv_fun v1 v2

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 exts (V_tuple[v1;v]) = 
  let exts_help v1 v = match (v1,v) with
    | (V_lit(L_aux (L_num len) _), V_vector _ inc _)-> to_vec inc (natFromInteger len) (to_num Signed v)
    | (V_lit(L_aux (L_num len) _), V_unknown) -> to_vec true (natFromInteger len) V_unknown
    | (V_unknown,_) -> V_unknown
  end in
  binary_taint exts_help v1 v

let extz (V_tuple[v1;v]) = 
  let extz_help v1 v = match (v1,v) with
    | (V_lit(L_aux (L_num len) _), V_vector _ inc _)-> to_vec inc (natFromInteger len) (to_num Unsigned v)
    | (V_lit(L_aux (L_num len) _), V_unknown) -> to_vec true (natFromInteger len) V_unknown
    | (V_unknown,_) -> V_unknown
  end in
  binary_taint extz_help v1 v

let eq (V_tuple [x; y]) = 
  let combo = binary_taint (fun v _ -> v) x y in
  retaint combo (V_lit (L_aux (if value_eq (detaint x) (detaint 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 = retaint v (match detaint 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_tuple [v] -> neg v
end)

let neq = compose neg eq ;;

let neq_vec = compose neg eq_vec_vec

let arith_op op (V_tuple [vl;vr]) = 
  let arith_op_help vl vr = 
    match (vl,vr) 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_unknown,_) -> V_unknown
      | (_,V_unknown) -> V_unknown
  end in 
  binary_taint arith_op_help vl vr
let rec arith_op_vec op sign size (V_tuple [vl;vr]) =
  let arith_op_help vl vr =
    match (vl,vr) 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_unknown,_) -> V_unknown
      | (_,V_unknown) -> V_unknown
  end in
  binary_taint arith_op_help vl vr
let rec arith_op_vec_vec_range op sign (V_tuple [vl;vr]) = 
  let arith_op_help vl vr =
    match (vl,vr) with
      | (V_vector _ _ _,V_vector _ _ _ ) ->
	let (l1,l2) = (to_num sign vl,to_num sign vr) in
	arith_op op (V_tuple [l1;l2])
      | (V_unknown,_) -> V_unknown
      | (_,V_unknown) -> V_unknown
   end in
   binary_taint arith_op_help vl vr
let rec arith_op_overflow_vec op over_typ sign size (V_tuple [vl;vr]) = 
  let overflow_help vl vr =
    match (vl,vr) with
      | (V_vector b ord cs1,V_vector _ _ cs2) ->
	let len = List.length cs1 in
	let act_size = len * size in
	let (is_l1_unknown,is_l2_unknown) = ((has_unknown vl), (has_unknown vr)) in
	if is_l1_unknown || is_l2_unknown 
	then (V_tuple [ (to_vec ord act_size V_unknown);V_unknown;V_unknown])
	else 
	  let (l1_sign,l2_sign) = (to_num sign vl,to_num sign vr) in
	  let (l1_unsign,l2_unsign) = (to_num Unsigned vl,to_num Unsigned vr) in
	  let n = arith_op op (V_tuple [l1_sign;l2_sign]) in
	  let n_unsign = arith_op op (V_tuple[l1_unsign;l2_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 overflow = (match n with 
	    | V_lit (L_aux (L_num n') ln) -> 
	      if (n' <= (get_max_representable_in sign len)) &&
		(n' >= (get_min_representable_in sign len))
	      then V_lit (L_aux L_zero ln)
	      else V_lit (L_aux L_one ln) end) in
	  let out_num = to_num sign correct_size_num in
	  let c_out = 
	    match detaint one_more_size_u with
	      | V_vector _ _ (b::bits) -> b 
              | v -> Assert_extra.failwith ("to_vec returned " ^ (string_of_value v)) end in
    V_tuple [correct_size_num;overflow;c_out]
  | (V_unknown,_) -> V_tuple [V_unknown;V_unknown;V_unknown]
  | (_,V_unknown) -> V_tuple [V_unknown;V_unknown;V_unknown]
  end in
  binary_taint overflow_help vl vr
let rec arith_op_overflow_vec_bit op sign size (V_tuple [vl;vr]) =
  let arith_help vl vr = 
    match (vl,vr) with
      | (V_vector b ord cs, V_lit (L_aux bit li)) ->
	let act_size = (List.length cs) * size in
	let is_v_unknown = has_unknown vl in
	if is_v_unknown 
	then V_tuple [(to_vec ord act_size V_unknown);V_unknown;V_unknown]
	else
	  let l1' = to_num sign vl in
	  let l1_u = to_num Unsigned vl in
	  let (n,nu,changed) = match bit with
	    | L_one -> (arith_op op (V_tuple [l1';(V_lit (L_aux (L_num 1) li))]),
			arith_op op (V_tuple [l1_u;(V_lit (L_aux (L_num 1) li))]), true)
	    | L_zero -> (l1',l1_u,false) end in
	let correct_size_num = to_vec ord act_size n in
	let one_larger = to_vec ord (act_size +1) nu in
	let overflow = if changed 
	  then retaint n (match detaint n with 
	    | V_lit (L_aux (L_num n') ln) -> 
	      if (n' <= (get_max_representable_in sign act_size)) &&
		(n' >= (get_min_representable_in sign act_size))
	      then V_lit (L_aux L_zero ln)
	      else V_lit (L_aux L_one ln) end) 
          else V_lit (L_aux L_zero Unknown) in
	V_tuple [correct_size_num;overflow;(match detaint one_larger with V_vector _ _ (c::rst) -> c end)]
      | (V_unknown,_) -> V_tuple [V_unknown;V_unknown;V_unknown]
      | (_,V_unknown) -> V_tuple [V_unknown;V_unknown;V_unknown]
      end in
   binary_taint arith_help vl vr

let rec arith_op_range_vec op sign size (V_tuple [vl;vr]) = 
  let arith_help vl vr = match (vl,vr) with
    | (V_unknown,_) -> V_unknown
    | (_,V_unknown) -> V_unknown
    | (n, V_vector _ ord cs) ->
      arith_op_vec op sign size (V_tuple [(to_vec ord (List.length cs) n);vr])
  end in
  binary_taint arith_help vl vr
let rec arith_op_vec_range op sign size (V_tuple [vl;vr]) = 
  let arith_help vl vr = match (vl,vr) with
    | (V_unknown,_) -> V_unknown
    | (_,V_unknown) -> V_unknown
    | (V_vector _ ord cs,n) ->
      arith_op_vec op sign size (V_tuple [vl;(to_vec ord (List.length cs) n)])
  end in
  binary_taint arith_help vl vr
let rec arith_op_range_vec_range op sign (V_tuple [vl;vr]) =
  let arith_help vl vr = match (vl,vr) with
    | (V_unknown,_) -> V_unknown
    | (_,V_unknown) -> V_unknown
    | (n,V_vector _ ord _) ->
      arith_op op (V_tuple [n;(to_num Unsigned vr)])
  end in
  binary_taint arith_help vl vr
let arith_op_vec_range_range op sign (V_tuple [vl;vr]) = 
  let arith_help vl vr = match (vl,vr) with
    | (V_unknown,_) -> V_unknown
    | (_,V_unknown) -> V_unknown
    | (V_vector _ ord _ ,n) ->
      arith_op op (V_tuple [(to_num sign vl);n])
   end in
   binary_taint arith_help vl vr
let rec arith_op_vec_bit op sign size (V_tuple [vl;vr]) =
  let arith_help vl vr =
    match (vl,vr) with
      | (V_unknown,_) -> V_unknown
      | (_,V_unknown) -> V_unknown
      | (V_vector _ ord cs,V_lit (L_aux bit _)) ->
	let l1' = to_num sign vl 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 in
   binary_taint arith_help vl vr 

let rec arith_op_no0 op (V_tuple [vl;vr]) = 
  let arith_help vl vr =
    match (vl,vr) 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_unknown,_) -> V_unknown
      | (_,V_unknown) -> V_unknown
  end in 
  binary_taint arith_help vl vr

let rec arith_op_vec_no0 op op_s sign size (V_tuple [vl;vr]) = 
  let arith_help vl vr = 
    match (vl,vr) with
      | (V_vector b ord cs, V_vector _ _ _) ->
	let act_size = (List.length cs) * size in
	let (is_l1_unknown,is_l2_unknown) = ((has_unknown vl), (has_unknown vr)) in
	let (l1',l2') = (if is_l1_unknown then V_unknown else (to_num sign vl),
                         if is_l2_unknown then V_unknown else (to_num sign vr)) 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 detaint n with 
	    | V_lit (L_aux (L_num n') ln) ->  
	      ((n' <= (get_max_representable_in sign act_size)) && (n' >= (get_min_representable_in sign 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_unknown,_) -> V_unknown
      | (_,V_unknown) -> V_unknown
   end in
   binary_taint arith_help vl vr
let rec arith_op_overflow_vec_no0 op op_s sign size (V_tuple [vl;vr]) =
  let arith_help vl vr = 
    match (vl,vr) with
      | (V_vector b ord cs, V_vector _ _ cs2) ->
	let rep_size = (List.length cs2) * size in
	let act_size = (List.length cs) * size in
	let (is_l1_unknown,is_l2_unknown) = ((has_unknown vl), (has_unknown vr)) in
	if is_l1_unknown || is_l2_unknown
	then V_tuple [to_vec ord act_size V_unknown;V_unknown;V_unknown]
	else
	  let (l1',l2') = ((to_num sign vl),(to_num sign vr)) in
	  let (l1_u,l2_u) = (to_num Unsigned vl,to_num Unsigned vr) in
	  let n = arith_op op (V_tuple [l1';l2']) in
	  let n_u = arith_op op (V_tuple [l1_u;l2_u]) in
	  let representable = 
	    match detaint n with 
	      | V_lit (L_aux (L_num n') ln) ->  
		((n' <= (get_max_representable_in sign rep_size)) && (n' >= (get_min_representable_in sign rep_size)))
	      | _ -> true end in
          let (correct_size_num,one_more) = 
	  if representable then (to_vec ord act_size n,to_vec ord (act_size+1) n_u) 
	  else let udef = V_lit (L_aux L_undef Unknown) in
	       (to_vec ord act_size udef, to_vec ord (act_size +1) udef) in
	  let overflow = if representable then V_lit (L_aux L_zero Unknown) else V_lit (L_aux L_one Unknown) in
	  let carry = match one_more with
	    | V_vector _ _ (b::bits) -> b end in
	  V_tuple [correct_size_num;overflow;carry]
	| (V_unknown,_) -> V_tuple [V_unknown;V_unknown;V_unknown]
	| (_,V_unknown) -> V_tuple [V_unknown;V_unknown;V_unknown]
   end in
  binary_taint arith_help vl vr

let rec arith_op_vec_range_no0 op op_s sign size (V_tuple [vl;vr]) =
  let arith_help vl vr =
    match (vl,vr) with
      | (V_unknown,_) -> V_unknown
      | (_,V_unknown) -> V_unknown
      | (V_vector _ ord cs,n) ->
	arith_op_vec_no0 op op_s sign size (V_tuple [vl;(to_vec ord (List.length cs) n)])
  end in
  binary_taint arith_help vl vr

let rec shift_op_vec op (V_tuple [vl;vr]) =
  let arith_op_help vl vr =
    match (vl,vr) with
      | (V_vector b ord cs,V_lit (L_aux (L_num n) _)) ->
	(match op with
	  | "<<" -> 
	    V_vector b ord 
	      ((from_n_to_n n (integerFromNat ((length cs) - 1)) cs) ++(List.replicate (natFromInteger n) (V_lit (L_aux L_zero Unknown))))
	  | ">>" ->
	    V_vector b ord
	      ((List.replicate (natFromInteger n) (V_lit (L_aux L_zero Unknown))) ++ (from_n_to_n 0 (n-1) cs))
	  | "<<<" ->
	    V_vector b ord
	      ((from_n_to_n n (integerFromNat ((length cs) -1)) cs) ++ (from_n_to_n 0 (n-1) cs)) end)
      | (V_unknown,_) -> V_unknown
      | (_,V_unknown) -> V_unknown
  end in
  binary_taint arith_op_help vl vr


let rec compare_op op (V_tuple [vl;vr]) =
  let comp_help vl vr = match (vl,vr) with
    | (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 in
   binary_taint comp_help vl vr
let rec compare_op_vec op sign (V_tuple [vl;vr]) = 
  let comp_help vl vr = match (vl,vr) with
    | (V_unknown,_) -> V_unknown
    | (_,V_unknown) -> V_unknown
    | (V_vector _ _ _,V_vector _ _ _) ->
      let (l1',l2') = (to_num sign vl, to_num sign vr) in
      compare_op op (V_tuple[l1';l2'])
   end in
   binary_taint comp_help vl vr
let rec compare_op_vec_unsigned op (V_tuple [vl;vr]) = 
  let comp_help vl vr = match (vl,vr) with
    | (V_unknown,_) -> V_unknown
    | (_,V_unknown) -> V_unknown
    | (V_vector _ _ _,V_vector _ _ _) ->
      let (l1',l2') = (to_num Unsigned vl, to_num Unsigned vr) in
      compare_op op (V_tuple[l1';l2'])
  end in
  binary_taint comp_help vl vr

let duplicate (V_tuple [vl;vr]) = 
  let dup_help vl vr =
    match (vl,vr) with
      | ((V_lit _ as v),(V_lit (L_aux (L_num n) _))) ->
	V_vector 0 true (List.replicate (natFromInteger n) v)
      | (V_unknown,(V_lit (L_aux (L_num n) _))) ->
	V_vector 0 true (List.replicate (natFromInteger n) V_unknown)
      | (V_unknown,_) -> V_unknown
    end in
  binary_taint dup_help vl vr

let rec vec_concat (V_tuple [vl;vr]) = 
  let concat_help vl vr = 
    match (vl,vr) 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_unknown,_) -> V_unknown
      | (_,V_unknown) -> V_unknown
  end in
  binary_taint concat_help vl vr

let v_length v = retaint v (match detaint v with
  | V_vector n d l -> V_lit (L_aux (L_num (integerFromNat (List.length l))) Unknown)
  | V_unknown -> V_unknown 
  | _ -> Assert_extra.failwith ("length given unexpected " ^ (string_of_value v)) 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);
  ("minus_overflow_vec_bit", arith_op_overflow_vec_bit (-) Unsigned 1);
  ("minus_overflow_vec_signed", arith_op_overflow_vec (-) "+" Signed 1);
  ("minus_overflow_vec_bit_signed", arith_op_overflow_vec_bit (-) Signed 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);
  ("bitwise_leftshift", shift_op_vec "<<");
  ("bitwise_rightshift", shift_op_vec ">>");
  ("bitwise_rotate", shift_op_vec "<<<");
  ("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);
  ("EXTZ", extz);
  ("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