From edff4ba336735bcd1c244a4bd7fc8f5c4464e91b Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 4 Apr 2017 10:34:42 +0100 Subject: Implement exit by raising Sail_exit exception --- src/gen_lib/sail_values.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index d287b2cd..86f8934a 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -13,6 +13,8 @@ type value = | Vregister of vbit array ref * int * bool * (string * (int * int)) list | Vbit of vbit (*Mostly for Vundef in place of undefined register place holders*) +exception Sail_exit + let string_of_bit = function | Vone -> "1" | Vzero -> "0" @@ -37,7 +39,7 @@ let is_one i = else Vzero -let exit _ = failwith "called exit" +let exit _ = raise Sail_exit let is_one_int i = -- cgit v1.2.3 From 9c51012bc47d0a66ff898ae53359764f59816a02 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 4 Apr 2017 10:36:15 +0100 Subject: implement exts and extz as manipulations on bit vectors rather than converting to integers, allowing them to work on vectors containing undef. --- src/gen_lib/sail_values.ml | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 86f8934a..a2f1286a 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -534,11 +534,34 @@ let to_vec_dec_undef_big len = to_vec_undef_big false len 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_int (len, vec) = + let barray = get_barray(vec) in + let vlen = Array.length barray in + let arr = + if (vlen < len) then + (* copy most significant bit into new bits *) + Array.append (Array.make (len - vlen) barray.(0)) barray + else + (* truncate to least significant bits *) + Array.sub barray (vlen - len) len in + let inc = get_ord vec in + Vvector(arr, (if inc then 0 else (len - 1)), inc) + +let extz_int (len, vec) = + let barray = get_barray(vec) in + let vlen = Array.length barray in + let arr = + if (vlen < len) then + (* fill new bits with zero *) + Array.append (Array.make (len - vlen) Vzero) barray + else + (* truncate to least significant bits *) + Array.sub barray (vlen - len) len in + let inc = get_ord vec in + Vvector(arr, (if inc then 0 else (len - 1)), inc) -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_big (len,vec) = exts_int (int_of_big_int len, vec) +let extz_big (len,vec) = extz_int (int_of_big_int len, vec) let exts = exts_big let extz = extz_big -- cgit v1.2.3 From c7b9060464ead8fac71824b151c25a968cb25302 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 4 Apr 2017 10:37:10 +0100 Subject: fix incorrect use of == in eq --- src/gen_lib/sail_values.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index a2f1286a..21aa48c3 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -1146,7 +1146,7 @@ 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 (l,r) = if l = r then Vone else Vzero 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_big false l,r) -- cgit v1.2.3 From 1e1b869f5c66976685901d694959dd3432597264 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 6 Apr 2017 12:25:58 +0100 Subject: minor changes in sail_values.ml to aid debugging --- src/gen_lib/sail_values.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 21aa48c3..ebde00a7 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -1,4 +1,5 @@ open Big_int_Z +open Printf (* only expected to be 0, 1, 2; 2 represents undef *) type vbit = Vone | Vzero | Vundef @@ -25,7 +26,7 @@ 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) + | Vregister(bits, start, inc, fields) -> "reg" ^ (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 @@ -159,7 +160,7 @@ let set_register register value = match register,value with a := !new_v | Vregister(a,_,_,_), Vvector(new_v,_,_) -> a := new_v - | _ -> () + | _ -> failwith "set_register of non-register" let set_vector_subrange_vec_int v n m new_v = let walker array length offset new_values = -- cgit v1.2.3