summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/gen_lib/sail_operators.lem7
-rw-r--r--src/gen_lib/sail_operators_mwords.lem10
-rw-r--r--src/gen_lib/sail_values.lem92
-rw-r--r--src/monomorphise.ml74
4 files changed, 132 insertions, 51 deletions
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 826ea98f..83746c0b 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -40,6 +40,9 @@ let cast_bit_vec_basic (start, len, b) = Vector (repeat [b] len) start false
let cast_boolvec_bitvec (Vector bs start inc) =
Vector (List.map bool_to_bitU bs) start inc
let cast_vec_bl (Vector bs start inc) = bs
+let cast_bl_vec (start, len, bs) = Vector (extz_bl (len, bs)) start false
+let cast_bl_svec (start, len, bs) = Vector (bits_of_int (len, bitlist_to_signed bs)) start false
+let cast_int_vec n = of_bits (int_to_bin n)
let pp_bitu_vector (Vector elems start inc) =
let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
@@ -150,10 +153,6 @@ let extz (start, len, vec) = set_vector_start (start, to_norm_vec (get_dir vec)
let exts_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, signed_big vec))
let extz_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, unsigned_big vec))
-(* TODO *)
-let extz_bl (start, len, bits) = Vector bits start false
-let exts_bl (start, len, bits) = Vector bits start false
-
let quot = hardware_quot
let modulo (l,r) = hardware_mod l r
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 74d0acf7..ff25c37b 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -111,6 +111,9 @@ let cast_bit_vec_basic (start, len, b) = vec_to_bvec (Vector [b] start false)
let cast_boolvec_bitvec (Vector bs start inc) =
vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc)
let cast_vec_bl v = List.map bool_to_bitU (bitlistFromWord v)
+let cast_int_vec n = wordFromInteger n
+let cast_bl_vec (start, len, bs) = wordFromBitlist (List.map bitU_to_bool bs)
+let cast_bl_svec (start, len, bs) = cast_int_vec (bitlist_to_signed bs)
let pp_bitu_vector (Vector elems start inc) =
let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
@@ -210,7 +213,7 @@ end
let add_one_bit_ignore_overflow bits =
List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
-
+
val to_norm_vec : forall 'a. Size 'a => integer -> bitvector 'a
let to_norm_vec (n : integer) = wordFromInteger n
(*
@@ -247,10 +250,6 @@ let extz (start, len, vec) = to_norm_vec (unsigned vec)
let exts_big (start, len, vec) = to_vec_big (signed_big vec)
let extz_big (start, len, vec) = to_vec_big (unsigned_big vec)
-(* TODO *)
-let extz_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
-let exts_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
-
let quot = hardware_quot
let modulo (l,r) = hardware_mod l r
@@ -442,6 +441,7 @@ let bitwise_rightshift x = shift_op_vec RR_shift x (*">>"*)
let bitwise_rotate x = shift_op_vec LLL_shift x (*"<<<"*)
let shiftl = bitwise_leftshift
+let shiftr = bitwise_rightshift
let rec arith_op_no0 (op : integer -> integer -> integer) l r =
if r = 0
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 98ac2522..231b9c8e 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -156,6 +156,9 @@ let inline (|.) x y = bitwise_or_bit (x,y)
val (+.) : bitU -> bitU -> bitU
let inline (+.) x y = bitwise_xor_bit (x,y)
+
+(*** Bit lists ***)
+
val to_bin_aux : natural -> list bitU
let rec to_bin_aux x =
if x = 0 then []
@@ -175,14 +178,36 @@ let of_bin bits =
(0,0) bits in
sum
-val bitlist_to_integer : list bitU -> integer
-let bitlist_to_integer bs = integerFromNatural (of_bin bs)
+let bitwise_not_bitlist = List.map bitwise_not_bit
-val pad_zero : list bitU -> integer -> list bitU
-let rec pad_zero bits n =
- if n <= 0 then bits else pad_zero (B0 :: bits) (n -1)
+val bitlist_to_unsigned : list bitU -> integer
+let bitlist_to_unsigned bs = integerFromNatural (of_bin bs)
-let bitwise_not_bitlist = List.map bitwise_not_bit
+val bitlist_to_signed : list bitU -> integer
+let bitlist_to_signed bits =
+ match bits with
+ | B1 :: _ -> 0 - (1 + (bitlist_to_unsigned (bitwise_not_bitlist bits)))
+ | B0 :: _ -> bitlist_to_unsigned bits
+ | BU :: _ -> failwith "bitlist_to_signed applied to list with undefined bits"
+ | [] -> failwith "bitlist_to_signed applied to empty list"
+ end
+
+val pad_bitlist : bitU -> list bitU -> integer -> list bitU
+let rec pad_bitlist b bits n =
+ if n <= 0 then bits else pad_bitlist b (b :: bits) (n - 1)
+
+let ext_bl pad (len, bits) =
+ let longer = len - (integerFromNat (List.length bits)) in
+ if longer < 0 then drop (natFromInteger (abs (longer))) bits
+ else pad_bitlist pad bits longer
+
+let extz_bl (len, bits) = ext_bl B0 (len, bits)
+let exts_bl (len, bits) =
+ match bits with
+ | BU :: _ -> failwith "exts_bl: undefined bit"
+ | B1 :: _ -> ext_bl B1 (len, bits)
+ | _ -> ext_bl B0 (len, bits)
+ end
let rec add_one_bit_ignore_overflow_aux bits = match bits with
| [] -> []
@@ -194,19 +219,50 @@ end
let add_one_bit_ignore_overflow bits =
List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
-let bits_of_nat ((len : integer),(n : natural)) =
- let bits = to_bin n in
- let len_bits = integerFromNat (List.length bits) in
- let longer = len - len_bits in
- if longer < 0 then drop (natFromInteger (abs (longer))) bits
- else pad_zero bits longer
+let int_to_bin n =
+ let bits_abs = B0 :: to_bin (naturalFromInteger (abs n)) in
+ if n >= (0 : integer) then bits_abs
+ else add_one_bit_ignore_overflow (bitwise_not_bitlist bits_abs)
+
+let bits_of_nat ((len : integer),(n : natural)) = extz_bl (len, to_bin n)
+let bits_of_int ((len : integer),(n : integer)) = exts_bl (len, int_to_bin n)
+
+let nibble_of_bits = function
+ | (B0, B0, B0, B0) -> Just #'0'
+ | (B0, B0, B0, B1) -> Just #'1'
+ | (B0, B0, B1, B0) -> Just #'2'
+ | (B0, B0, B1, B1) -> Just #'3'
+ | (B0, B1, B0, B0) -> Just #'4'
+ | (B0, B1, B0, B1) -> Just #'5'
+ | (B0, B1, B1, B0) -> Just #'6'
+ | (B0, B1, B1, B1) -> Just #'7'
+ | (B1, B0, B0, B0) -> Just #'8'
+ | (B1, B0, B0, B1) -> Just #'9'
+ | (B1, B0, B1, B0) -> Just #'A'
+ | (B1, B0, B1, B1) -> Just #'B'
+ | (B1, B1, B0, B0) -> Just #'C'
+ | (B1, B1, B0, B1) -> Just #'D'
+ | (B1, B1, B1, B0) -> Just #'E'
+ | (B1, B1, B1, B1) -> Just #'F'
+ | _ -> Nothing
+ end
-let bits_of_int ((len : integer),(n : integer)) =
- let bits = bits_of_nat (len, naturalFromInteger (abs n)) in
- if n > (0 : integer)
- then bits
- else (add_one_bit_ignore_overflow (bitwise_not_bitlist bits))
+let rec hexstring_of_bits bs = match bs with
+ | b1 :: b2 :: b3 :: b4 :: bs ->
+ let n = nibble_of_bits (b1, b2, b3, b4) in
+ let s = hexstring_of_bits bs in
+ match (n, s) with
+ | (Just n, Just s) -> Just (n :: s)
+ | _ -> Nothing
+ end
+ | _ -> Nothing
+ end
+let show_bitlist bs =
+ match hexstring_of_bits bs with
+ | Just s -> toString (#'0' :: #'x' :: s)
+ | Nothing -> show bs
+ end
(*** Vectors *)
@@ -348,7 +404,7 @@ end
instance forall 'a. BitU 'a => (Bitvector (list 'a))
let bits_of v = List.map to_bitU v
let of_bits v = List.map of_bitU v
- let unsigned v = bitlist_to_integer (List.map to_bitU v)
+ let unsigned v = bitlist_to_unsigned (List.map to_bitU v)
let get_bit is_inc start v n = to_bitU (access_aux is_inc start v n)
let set_bit is_inc start v n b = update_aux is_inc start v n n [of_bitU b]
let get_bits is_inc start v i j = List.map to_bitU (slice_aux is_inc start v i j)
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 7d72b974..ff264642 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -1853,8 +1853,13 @@ module CallerKidSet = Set.Make (struct
| x -> x
end)
-module FailureSet = Set.Make (struct
- type t = Parse_ast.l * string
+(* Map from locations to string sets *)
+module Failures = Map.Make (struct
+ type t = Parse_ast.l
+ let compare = compare
+end)
+module StringSet = Set.Make (struct
+ type t = string
let compare = compare
end)
@@ -1888,7 +1893,7 @@ let string_of_dep = function
type result = {
split : ArgSet.t;
- failures : FailureSet.t;
+ failures : StringSet.t Failures.t;
(* Dependencies for arguments and type variables of each fn called, so that
if the fn uses one for a bitvector size we can track it back *)
split_on_call : (dependencies list * dependencies KBindings.t) Bindings.t; (* (arguments, kids) per fn *)
@@ -1898,7 +1903,7 @@ type result = {
let empty = {
split = ArgSet.empty;
- failures = FailureSet.empty;
+ failures = Failures.empty;
split_on_call = Bindings.empty;
split_in_caller = CallerArgSet.empty;
kid_in_caller = CallerKidSet.empty
@@ -1938,9 +1943,15 @@ let call_arg_merge k args args' =
| Some (args,kdep), Some (args',kdep')
-> Some (List.map2 dmerge args args', KBindings.merge call_kid_merge kdep kdep')
+let failure_merge _ x y =
+ match x, y with
+ | None, x -> x
+ | x, None -> x
+ | Some x, Some y -> Some (StringSet.union x y)
+
let merge rs rs' = {
split = ArgSet.union rs.split rs'.split;
- failures = FailureSet.union rs.failures rs'.failures;
+ failures = Failures.merge failure_merge rs.failures rs'.failures;
split_on_call = Bindings.merge call_arg_merge rs.split_on_call rs'.split_on_call;
split_in_caller = CallerArgSet.union rs.split_in_caller rs'.split_in_caller;
kid_in_caller = CallerKidSet.union rs.kid_in_caller rs'.kid_in_caller
@@ -2079,19 +2090,28 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
| E_cast (_,e) -> analyse_exp fn_id env assigns e
| E_app (id,args) ->
let deps, assigns, r = non_det args in
+ let (_,fn_typ) = Env.get_val_spec id (env_of_annot (l,annot)) in
+ let fn_effect = match fn_typ with
+ | Typ_aux (Typ_fn (_,_,eff),_) -> eff
+ | _ -> Effect_aux (Effect_set [],Unknown)
+ in
+ let eff_dep = match fn_effect with
+ | Effect_aux (Effect_set ([] | [BE_aux (BE_undef,_)]),_) -> dempty
+ | _ -> Unknown (l, "Effects from function application")
+ in
let kid_inst = instantiation_of exp in
(* Change kids in instantiation to the canonical ones from the type signature *)
let kid_inst = KBindings.fold (fun kid -> KBindings.add (orig_kid kid)) kid_inst KBindings.empty in
let kid_deps = KBindings.map (deps_of_uvar env.kid_deps deps) kid_inst in
- let r' =
- if Id.compare fn_id id == 0 then
- let bad = Unknown (l,"Recursive call of " ^ string_of_id id) in
- let deps = List.map (fun _ -> bad) deps in
- let kid_deps = KBindings.map (fun _ -> bad) kid_deps in
- { empty with split_on_call = Bindings.singleton id (deps, kid_deps) }
- else
- { empty with split_on_call = Bindings.singleton id (deps, kid_deps) } in
- (merge_deps deps, assigns, merge r r')
+ let rdep,r' =
+ if Id.compare fn_id id == 0 then
+ let bad = Unknown (l,"Recursive call of " ^ string_of_id id) in
+ let deps = List.map (fun _ -> bad) deps in
+ let kid_deps = KBindings.map (fun _ -> bad) kid_deps in
+ bad, { empty with split_on_call = Bindings.singleton id (deps, kid_deps) }
+ else
+ dempty, { empty with split_on_call = Bindings.singleton id (deps, kid_deps) } in
+ (merge_deps (rdep::eff_dep::deps), assigns, merge r r')
| E_tuple es
| E_list es ->
let deps, assigns, r = non_det es in
@@ -2235,7 +2255,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
| Unknown (l,msg) ->
{ r with
failures =
- FailureSet.add (l,"Unable to monomorphise " ^ string_of_nexp size ^ ": " ^ msg)
+ Failures.add l (StringSet.singleton ("Unable to monomorphise " ^ string_of_nexp size ^ ": " ^ msg))
r.failures }
else
r
@@ -2355,6 +2375,11 @@ let print_result r =
let _ = Bindings.iter print_binding r.split_on_call in
let _ = print_endline (" split_in_caller: " ^ string_of_callerset r.split_in_caller) in
let _ = print_endline (" kid_in_caller: " ^ string_of_callerkidset r.kid_in_caller) in
+ let _ = print_endline (" failures: \n " ^
+ (String.concat "\n "
+ (List.map (fun (l,s) -> Reporting_basic.loc_to_string l ^ ":\n " ^
+ String.concat "\n " (StringSet.elements s))
+ (Failures.bindings r.failures)))) in
()
let analyse_funcl debug tenv (FCL_aux (FCL_Funcl (id,pexp),_)) =
@@ -2387,29 +2412,29 @@ let analyse_defs debug env (Defs defs) =
let rec chase_deps = function
| Have (splits, caller_args, caller_kids) ->
- let splits,fails = CallerArgSet.fold add_arg caller_args (splits,FailureSet.empty) in
+ let splits,fails = CallerArgSet.fold add_arg caller_args (splits,Failures.empty) in
let splits,fails = CallerKidSet.fold add_kid caller_kids (splits,fails) in
splits, fails
| Unknown (l,msg) ->
- ArgSet.empty , FailureSet.singleton (l,("Unable to monomorphise dependency: " ^ msg))
+ ArgSet.empty , Failures.singleton l (StringSet.singleton ("Unable to monomorphise dependency: " ^ msg))
and chase_kid_caller (id,kid) =
match Bindings.find id r.split_on_call with
| (_,kid_deps) -> begin
match KBindings.find kid kid_deps with
| deps -> chase_deps deps
- | exception Not_found -> ArgSet.empty,FailureSet.empty
+ | exception Not_found -> ArgSet.empty,Failures.empty
end
- | exception Not_found -> ArgSet.empty,FailureSet.empty
+ | exception Not_found -> ArgSet.empty,Failures.empty
and chase_arg_caller (id,i) =
match Bindings.find id r.split_on_call with
| (arg_deps,_) -> chase_deps (List.nth arg_deps i)
- | exception Not_found -> ArgSet.empty,FailureSet.empty
+ | exception Not_found -> ArgSet.empty,Failures.empty
and add_arg arg (splits,fails) =
let splits',fails' = chase_arg_caller arg in
- ArgSet.union splits splits', FailureSet.union fails fails'
+ ArgSet.union splits splits', Failures.merge failure_merge fails fails'
and add_kid k (splits,fails) =
let splits',fails' = chase_kid_caller k in
- ArgSet.union splits splits', FailureSet.union fails fails'
+ ArgSet.union splits splits', Failures.merge failure_merge fails fails'
in
let _ = if debug > 1 then print_result r else () in
let splits,fails = CallerArgSet.fold add_arg r.split_in_caller (r.split,r.failures) in
@@ -2421,9 +2446,10 @@ let analyse_defs debug env (Defs defs) =
else ()
in
let _ =
- if FailureSet.is_empty fails then () else
+ if Failures.is_empty fails then () else
begin
- FailureSet.iter (fun (l,msg) -> Reporting_basic.print_err false false l "Monomorphisation" msg)
+ Failures.iter (fun l msgs ->
+ Reporting_basic.print_err false false l "Monomorphisation" (String.concat "\n" (StringSet.elements msgs)))
fails;
raise (Reporting_basic.err_general Unknown "Unable to monomorphise program")
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 17:06:57 +0000