diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 15 | ||||
| -rw-r--r-- | src/ast_util.mli | 2 | ||||
| -rw-r--r-- | src/interpreter.ml | 6 | ||||
| -rw-r--r-- | src/libsail.mllib | 3 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 1 | ||||
| -rw-r--r-- | src/sail.ml | 6 | ||||
| -rw-r--r-- | src/sail_lib.ml | 7 | ||||
| -rw-r--r-- | src/toFromInterp_backend.ml | 65 | ||||
| -rw-r--r-- | src/toFromInterp_lib_bitlist.ml | 142 | ||||
| -rw-r--r-- | src/toFromInterp_lib_mword.ml (renamed from src/toFromInterp_lib.ml) | 17 | ||||
| -rw-r--r-- | src/value.ml | 9 |
11 files changed, 253 insertions, 20 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 33af1be7..12777506 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -1457,7 +1457,10 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) = initial_check.ml. i.e. the rewriter should only encounter this case when re-writing those functions. *) wrap (E_id (prepend_id "typ_" (id_of_kid kid))) typ - | Typ_internal_unknown | Typ_bidir _ | Typ_fn _ | Typ_exist _ -> assert false (* Typ_exist should be re-written *) + | Typ_internal_unknown -> assert false + | Typ_bidir _ -> assert false + | Typ_fn _ -> assert false + | Typ_exist _ -> assert false (* Typ_exist should be re-written *) and undefined_of_typ_args mwords l annot (A_aux (typ_arg_aux, _) as typ_arg) = match typ_arg_aux with | A_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))] @@ -2141,3 +2144,13 @@ let rec find_annot_defs sl = function let rec find_annot_ast sl (Defs defs) = find_annot_defs sl defs +let string_of_lx lx = + let open Lexing in + Printf.sprintf "%s,%d,%d,%d" lx.pos_fname lx.pos_lnum lx.pos_bol lx.pos_cnum + +let rec simple_string_of_loc = function + | Parse_ast.Unknown -> "Unknown" + | Parse_ast.Unique (n, l) -> "Unique(" ^ string_of_int n ^ ", " ^ simple_string_of_loc l ^ ")" + | Parse_ast.Generated l -> "Generated(" ^ simple_string_of_loc l ^ ")" + | Parse_ast.Range (lx1,lx2) -> "Range(" ^ string_of_lx lx1 ^ "->" ^ string_of_lx lx2 ^ ")" + | Parse_ast.Documented (_,l) -> "Documented(_," ^ simple_string_of_loc l ^ ")" diff --git a/src/ast_util.mli b/src/ast_util.mli index cfbc26fe..c8f3cc5c 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -523,3 +523,5 @@ val subst_kids_typ_arg : nexp KBindings.t -> typ_arg -> typ_arg val quant_item_subst_kid : kid -> kid -> quant_item -> quant_item val typquant_subst_kid : kid -> kid -> typquant -> typquant + +val simple_string_of_loc : Parse_ast.l -> string diff --git a/src/interpreter.ml b/src/interpreter.ml index 9acfeb26..db4f45f6 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -388,14 +388,14 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = read_reg regname >>= fun v -> return (exp_of_value v) | "read_mem" -> begin match evaluated with - | [rk; addr; len] -> + | [rk; addrsize; addr; len] -> read_mem (value_of_exp rk) (value_of_exp addr) (value_of_exp len) >>= fun v -> return (exp_of_value v) | _ -> fail "Wrong number of parameters to read_mem intrinsic" end | "write_mem_ea" -> begin match evaluated with - | [wk; addr; len] -> + | [wk; addrsize; addr; len] -> write_ea (value_of_exp wk) (value_of_exp addr) (value_of_exp len) >> wrap unit_exp | _ -> fail "Wrong number of parameters to write_ea intrinsic" @@ -409,7 +409,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = end | "write_mem" -> begin match evaluated with - | [wk; addr; len; v] -> + | [wk; addrsize; addr; len; v] -> write_mem (value_of_exp wk) (value_of_exp v) (value_of_exp len) (value_of_exp v) >>= fun b -> return (exp_of_value (V_bool b)) | _ -> fail "Wrong number of parameters to write_memv intrinsic" diff --git a/src/libsail.mllib b/src/libsail.mllib index 1a992391..b9d91834 100644 --- a/src/libsail.mllib +++ b/src/libsail.mllib @@ -51,7 +51,8 @@ Spec_analysis Specialize State ToFromInterp_backend -ToFromInterp_lib +ToFromInterp_lib_mword +ToFromInterp_lib_bitlist Type_check Type_error Util diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 708749cc..5306e07c 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1192,6 +1192,7 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "trans_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty + | Id_aux ((Id "cache_op_kind"),_) -> empty | Id_aux ((Id "regfp"),_) -> empty | Id_aux ((Id "niafp"),_) -> empty | Id_aux ((Id "diafp"),_) -> empty diff --git a/src/sail.ml b/src/sail.ml index daec1fdb..eff90fa3 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -95,6 +95,9 @@ let options = Arg.align ([ ( "-tofrominterp_lem", Arg.Tuple [set_target "tofrominterp"; Arg.Set ToFromInterp_backend.lem_mode], " output embedding translation for the Lem backend rather than the OCaml backend, implies -tofrominterp"); + ( "-tofrominterp_mwords", + Arg.Tuple [set_target "tofrominterp"; Arg.Set ToFromInterp_backend.mword_mode], + " output embedding translation in machine-word mode rather than bit-list mode, implies -tofrominterp"); ( "-tofrominterp_output_dir", Arg.String (fun dir -> opt_tofrominterp_output_dir := Some dir), " set a custom directory to output embedding translation OCaml"); @@ -202,6 +205,9 @@ let options = Arg.align ([ ( "-Oaarch64_fast", Arg.Set Jib_compile.optimize_aarch64_fast_struct, " apply ARMv8.5 specific optimizations (potentially unsound in general)"); + ( "-Ofast_undefined", + Arg.Set Initial_check.opt_fast_undefined, + " turn on fast-undefined mode"); ( "-static", Arg.Set C_backend.opt_static, " make generated C functions static"); diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 61e62d76..13ed491b 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -1,5 +1,12 @@ module Big_int = Nat_big_num +(* for ToFromInterp_lib_foo *) +module type BitType = sig + type t + val b0 : t + val b1 : t +end + type 'a return = { return : 'b . 'a -> 'b } type 'za zoption = | ZNone of unit | ZSome of 'za;; diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml index d65aaf3b..6b8fede4 100644 --- a/src/toFromInterp_backend.ml +++ b/src/toFromInterp_backend.ml @@ -57,10 +57,29 @@ open Pretty_print_common open Ocaml_backend let lem_mode = ref false +let mword_mode = ref false let maybe_zencode s = if !lem_mode then String.uncapitalize_ascii s else zencode_string s let maybe_zencode_upper s = if !lem_mode then String.capitalize_ascii s else zencode_upper_string s +let rec rewriteExistential (kids : kinded_id list) (Typ_aux (typ_aux, annot) as typ) = + print_endline (string_of_typ typ); + match typ_aux with + | Typ_tup typs -> Typ_aux (Typ_tup (List.map (rewriteExistential kids) typs), annot) + | Typ_exist _ -> Reporting.unreachable annot __POS__ "nested Typ_exist in rewriteExistential" + | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var kid, _)), _)]) + when (string_of_id id = "atom" || string_of_id id = "int") -> + (* List.exists (fun k -> string_of_kid (kopt_kid k) = string_of_kid kid) kids -> *) + print_endline("*** rewriting to int - kid is '" ^ string_of_kid kid ^ "'" ); + Typ_aux (Typ_id (mk_id "int"), annot) + | Typ_internal_unknown + | Typ_id _ + | Typ_var _ + | Typ_fn _ + | Typ_bidir _ + | Typ_app _ -> + typ + let frominterp_typedef (TD_aux (td_aux, (l, _))) = let fromValueArgs (Typ_aux (typ_aux, _)) = match typ_aux with | Typ_tup typs -> brackets (separate space [string "V_tuple"; brackets (separate (semi ^^ space) (List.mapi (fun i _ -> string ("v" ^ (string_of_int i))) typs))]) @@ -79,20 +98,30 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) = | A_typ typ -> fromValueTyp typ "" | A_nexp nexp -> fromValueNexp nexp | A_order order -> string ("Order_" ^ (string_of_order order)) - | _ -> string "TYP_ARG" + | A_bool _ -> parens (string "boolFromInterpValue") and fromValueTyp ((Typ_aux (typ_aux, l)) as typ) arg_name = match typ_aux with | Typ_id id -> parens (concat [string (maybe_zencode (string_of_id id)); string ("FromInterpValue"); space; string arg_name]) (* special case bit vectors for lem *) | Typ_app (Id_aux (Id "vector", _), [A_aux (A_nexp len_nexp, _); A_aux (A_order (Ord_aux (Ord_dec, _)), _); A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit", _)), _)), _)]) when !lem_mode -> - parens (separate space ([string (maybe_zencode "bitsFromInterpValue"); fromValueNexp len_nexp; string arg_name])) + parens (separate space ([string (maybe_zencode "bitsFromInterpValue"); string arg_name])) | Typ_app (typ_id, typ_args) -> assert (typ_args <> []); - parens (separate space ([string (maybe_zencode (string_of_id typ_id) ^ "FromInterpValue")] @ List.map fromValueTypArg typ_args @ [string arg_name])) + if string_of_id typ_id = "bits" then + parens (separate space ([string "bitsFromInterpValue"] @ [string arg_name])) + else + parens (separate space ([string (maybe_zencode (string_of_id typ_id) ^ "FromInterpValue")] @ List.map fromValueTypArg typ_args @ [string arg_name])) | Typ_var kid -> parens (separate space [fromValueKid kid; string arg_name]) | Typ_fn _ -> parens (string "failwith \"fromValueTyp: Typ_fn arm unimplemented\"") - | _ -> parens (string "failwith \"fromValueTyp: type arm unimplemented\"") + | Typ_bidir _ -> parens (string "failwith \"fromValueTyp: Typ_bidir arm unimplemented\"") + | Typ_exist (kids, _, t) -> parens (fromValueTyp (rewriteExistential kids t) arg_name) + | Typ_tup typs -> parens (string ("match " ^ arg_name ^ " with V_tuple ") ^^ + brackets (separate (string ";" ^^ space) + (List.mapi (fun i _ -> string (arg_name ^ "_tup" ^ string_of_int i)) typs)) ^^ + (string " -> ") ^^ + parens (separate comma_sp (List.mapi (fun i t -> fromValueTyp t (arg_name ^ "_tup" ^ string_of_int i)) typs))) + | Typ_internal_unknown -> failwith "escaped Typ_internal_unknown" in let fromValueVals ((Typ_aux (typ_aux, l)) as typ) = match typ_aux with | Typ_tup typs -> parens (separate comma_sp (List.mapi (fun i typ -> fromValueTyp typ ("v" ^ (string_of_int i))) typs)) @@ -147,13 +176,14 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) = end | TD_abbrev (Id_aux (Id "regfps", _), _, _) -> empty | TD_abbrev (Id_aux (Id "niafps", _), _, _) -> empty + | TD_abbrev (Id_aux (Id "bits", _), _, _) when !lem_mode -> empty | TD_abbrev (id, typq, typ_arg) -> begin let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in (* HACK: print a type annotation for abbrevs of unquantified types, to help cases ocaml can't type-infer on its own *) let fromInterpValspec = (* HACK because of lem renaming *) - if string_of_id id = "opcode" then empty else + if string_of_id id = "opcode" || string_of_id id = "integer" then empty else match typ_arg with | A_aux (A_typ _, _) -> begin match typq with | TypQ_aux (TypQ_no_forall, _) -> separate space [colon; string "value"; arrow; string (maybe_zencode (string_of_id id))] @@ -222,19 +252,30 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) = | A_typ typ -> toValueTyp typ "" | A_nexp nexp -> toValueNexp nexp | A_order order -> string ("Order_" ^ (string_of_order order)) - | _ -> string "TYP_ARG" + | A_bool _ -> parens (string "boolToInterpValue") and toValueTyp ((Typ_aux (typ_aux, l)) as typ) arg_name = match typ_aux with | Typ_id id -> parens (concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"; space; string arg_name]) (* special case bit vectors for lem *) | Typ_app (Id_aux (Id "vector", _), [A_aux (A_nexp len_nexp, _); A_aux (A_order (Ord_aux (Ord_dec, _)), _); A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit", _)), _)), _)]) when !lem_mode -> - parens (separate space ([string (maybe_zencode "bitsToInterpValue"); toValueNexp len_nexp; string arg_name])) + parens (separate space ([string (maybe_zencode "bitsToInterpValue"); string arg_name])) | Typ_app (typ_id, typ_args) -> assert (typ_args <> []); - parens (separate space ([string ((maybe_zencode (string_of_id typ_id)) ^ "ToInterpValue")] @ List.map toValueTypArg typ_args @ [string arg_name])) + if string_of_id typ_id = "bits" then + parens (separate space ([string "bitsToInterpValue"] @ [string arg_name])) + else + parens (separate space ([string ((maybe_zencode (string_of_id typ_id)) ^ "ToInterpValue")] @ List.map toValueTypArg typ_args @ [string arg_name])) | Typ_var kid -> parens (separate space [toValueKid kid; string arg_name]) - | _ -> parens (string "failwith \"toValueTyp: type arm unimplemented\"") + | Typ_fn _ -> parens (string "failwith \"toValueTyp: Typ_fn arm unimplemented\"") + | Typ_bidir _ -> parens (string "failwith \"toValueTyp: Typ_bidir arm unimplemented\"") + | Typ_exist (kids, _, t) -> parens (toValueTyp (rewriteExistential kids t) arg_name) + | Typ_tup typs -> parens (string ("match " ^ arg_name ^ " with ") ^^ + parens (separate comma_sp (List.mapi (fun i _ -> string (arg_name ^ "_tup" ^ string_of_int i)) typs)) ^^ + (string " -> V_tuple ") ^^ + brackets (separate (string ";" ^^ space) + (List.mapi (fun i t -> toValueTyp t (arg_name ^ "_tup" ^ string_of_int i)) typs))) + | Typ_internal_unknown -> failwith "escaped Typ_internal_unknown" in let toValueVals ((Typ_aux (typ_aux, _)) as typ) = match typ_aux with | Typ_tup typs -> brackets (separate space [string "V_tuple"; brackets (separate (semi ^^ space) (List.mapi (fun i typ -> toValueTyp typ ("v" ^ (string_of_int i))) typs))]) @@ -284,13 +325,14 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) = end | TD_abbrev (Id_aux (Id "regfps", _), _, _) -> empty | TD_abbrev (Id_aux (Id "niafps", _), _, _) -> empty + | TD_abbrev (Id_aux (Id "bits", _), _, _) when !lem_mode -> empty | TD_abbrev (id, typq, typ_arg) -> begin let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in (* HACK: print a type annotation for abbrevs of unquantified types, to help cases ocaml can't type-infer on its own *) let toInterpValspec = (* HACK because of lem renaming *) - if string_of_id id = "opcode" then empty else + if string_of_id id = "opcode" || string_of_id id = "integer" then empty else match typ_arg with | A_aux (A_typ _, _) -> begin match typq with | TypQ_aux (TypQ_no_forall, _) -> separate space [colon; string (maybe_zencode (string_of_id id)); arrow; string "value"] @@ -343,12 +385,13 @@ let tofrominterp_def def = match def with let tofrominterp_defs name (Defs defs) = (string "open Sail_lib;;" ^^ hardline) ^^ (string "open Value;;" ^^ hardline) - ^^ (string "open ToFromInterp_lib;;" ^^ hardline) ^^ (if !lem_mode then (string "open Sail2_instr_kinds;;" ^^ hardline) else empty) ^^ (string ("open " ^ String.capitalize_ascii name ^ ";;") ^^ hardline) ^^ (if !lem_mode then (string ("open " ^ String.capitalize_ascii name ^ "_types;;") ^^ hardline) else empty) ^^ (if !lem_mode then (string ("open " ^ String.capitalize_ascii name ^ "_extras;;") ^^ hardline) else empty) ^^ (string "module Big_int = Nat_big_num" ^^ ocaml_def_end) + ^^ (if !mword_mode then (string "include ToFromInterp_lib_mword" ^^ hardline) else empty) + ^^ (if not !mword_mode then (string "include ToFromInterp_lib_bitlist.Make(struct type t = Sail2_values.bitU0 let b0 = Sail2_values.B00 let b1 = Sail2_values.B10 end)" ^^ hardline) else empty) ^^ concat (List.map tofrominterp_def defs) let tofrominterp_pp_defs name f defs = diff --git a/src/toFromInterp_lib_bitlist.ml b/src/toFromInterp_lib_bitlist.ml new file mode 100644 index 00000000..d47beca3 --- /dev/null +++ b/src/toFromInterp_lib_bitlist.ml @@ -0,0 +1,142 @@ +(************************************************************) +(* Support for toFromInterp *) +(************************************************************) + +open Sail_lib;; +open Value;; + +module Make(BitT : BitType) = struct + +type vector_order = + | Order_inc + | Order_dec + +(* zencoded variants are for the OCaml backend, non-zencoded are for the Lem backend compiled to OCaml. + Sometimes they're just aliased. *) + +let zunitFromInterpValue v = match v with + | V_unit -> () + | _ -> failwith "invalid interpreter value for unit" + +let zunitToInterpValue () = V_unit + +let unitFromInterpValue = zunitFromInterpValue +let unitToInterpValue = zunitToInterpValue + +let zatomFromInterpValue typq_'n v = match v with + | V_int i when typq_'n = i -> i + | _ -> failwith "invalid interpreter value for atom" + +let zatomToInterpValue typq_'n v = + assert (typq_'n = v); + V_int v + +let atomFromInterpValue = zatomFromInterpValue +let atomToInterpValue = zatomToInterpValue + +let zintFromInterpValue v = match v with + | V_int i -> i + | _ -> failwith "invalid interpreter value for int" + +let zintToInterpValue v = V_int v + +let intFromInterpValue = zintFromInterpValue +let intToInterpValue = zintToInterpValue + +let znatFromInterpValue v = match v with + | V_int i when i >= Big_int.zero -> i + | _ -> failwith "invalid interpreter value for nat" + +let znatToInterpValue v = + assert (v >= Big_int.zero); + V_int v + +let natFromInterpValue = znatFromInterpValue +let natToInterpValue = znatToInterpValue + +let zrangeFromInterpValue low high v = match v with + | V_int i when i >= low && i <= high -> i + | _ -> failwith (Printf.sprintf "invalid interpreter value for range(%s, %s)" (Big_int.to_string low) (Big_int.to_string high)) + +let zrangeToInterpValue low high v = + assert (v >= low && v <= high); + V_int v + +let rangeFromInterpValue = zrangeFromInterpValue +let rangeToInterpValue = zrangeToInterpValue + + +let zboolFromInterpValue v = match v with + | V_bool b -> b + | _ -> failwith "invalid interpreter value for bool" + +let zboolToInterpValue v = V_bool v + +let boolFromInterpValue = zboolFromInterpValue +let boolToInterpValue = zboolToInterpValue + +let zstringFromInterpValue v = match v with + | V_string s -> s + | _ -> failwith "invalid interpreter value for string" + +let zstringToInterpValue v = V_string v + +let stringFromInterpValue = zstringFromInterpValue +let stringToInterpValue = zstringToInterpValue + +let zlistFromInterpValue typq_'a v = match v with + | V_list vs -> List.map typq_'a vs + | _ -> failwith "invalid interpreter value for list" + +let zlistToInterpValue typq_'a v = V_list (List.map typq_'a v) + +let listFromInterpValue = zlistFromInterpValue +let listToInterpValue = zlistToInterpValue + +let zvectorFromInterpValue typq_'n typq_'ord typq_'a v = match v with + | V_vector vs -> + assert (Big_int.of_int (List.length vs) = typq_'n); + List.map typq_'a vs + | _ -> failwith "invalid interpreter value for vector" + +let zvectorToInterpValue typq_'n typq_'ord typq_'a v = + assert (Big_int.of_int (List.length v) = typq_'n); + V_vector (List.map typq_'a v) + +let vectorFromInterpValue = zvectorFromInterpValue +let vectorToInterpValue = zvectorToInterpValue + +let zbitFromInterpValue v = match v with + | V_bit b -> (match b with + | Sail_lib.B0 -> BitT.b0 + | Sail_lib.B1 -> BitT.b1) + | _ -> failwith "invalid interpreter value for bit" + +let zbitToInterpValue v = V_bit (match v with + | b when b = BitT.b0 -> Sail_lib.B0 + | b when b = BitT.b1 -> Sail_lib.B1 + | _ -> failwith "invalid BitT (usually bitU) value for bit") + +let bitFromInterpValue = zbitFromInterpValue +let bitToInterpValue = zbitToInterpValue + +let optionFromInterpValue typq_'a v = match v with + | V_ctor ("None", [v0]) -> None + | V_ctor ("Some", [v0]) -> Some (typq_'a v0) + | _ -> failwith "invalid interpreter value for option" + +let optionToInterpValue typq_'a v = match v with + | None -> V_ctor ("None", [(unitToInterpValue ())]) + | Some (v0) -> V_ctor ("Some", [(typq_'a v0)]) + + +let bitsFromInterpValue v = match v with + | V_vector vs -> + List.map bitFromInterpValue vs + | _ -> failwith "invalid interpreter value for bits" + +let bitsToInterpValue v = + V_vector (List.map bitToInterpValue v) + + +end diff --git a/src/toFromInterp_lib.ml b/src/toFromInterp_lib_mword.ml index c29fcd84..fb937f11 100644 --- a/src/toFromInterp_lib.ml +++ b/src/toFromInterp_lib_mword.ml @@ -52,6 +52,17 @@ let znatToInterpValue v = let natFromInterpValue = znatFromInterpValue let natToInterpValue = znatToInterpValue +let zrangeFromInterpValue low high v = match v with + | V_int i when i >= low && i <= high -> i + | _ -> failwith (Printf.sprintf "invalid interpreter value for range(%s, %s)" (Big_int.to_string low) (Big_int.to_string high)) + +let zrangeToInterpValue low high v = + assert (v >= low && v <= high); + V_int v + +let rangeFromInterpValue = zrangeFromInterpValue +let rangeToInterpValue = zrangeToInterpValue + let zboolFromInterpValue v = match v with | V_bool b -> b @@ -112,15 +123,13 @@ let optionToInterpValue typq_'a v = match v with | Some (v0) -> V_ctor ("Some", [(typq_'a v0)]) -let bitsFromInterpValue typq_'n v = match v with +let bitsFromInterpValue v = match v with | V_vector vs -> - assert (Big_int.of_int (List.length vs) = typq_'n); Lem.wordFromBitlist (List.map (fun b -> bitFromInterpValue b |> Sail_lib.bool_of_bit) vs) | _ -> failwith "invalid interpreter value for bits" -let bitsToInterpValue typq_'n v = +let bitsToInterpValue v = let bs = Lem.bitlistFromWord v in - assert (Big_int.of_int (List.length bs) = typq_'n); V_vector (List.map (fun b -> Sail_lib.bit_of_bool b |> bitToInterpValue) bs) diff --git a/src/value.ml b/src/value.ml index 6ccecac0..6c2e0839 100644 --- a/src/value.ml +++ b/src/value.ml @@ -170,6 +170,10 @@ let coerce_tuple = function | V_tuple vs -> vs | _ -> assert false +let coerce_list = function + | V_list vs -> vs + | _ -> assert false + let coerce_listlike = function | V_tuple vs -> vs | V_list vs -> vs @@ -282,6 +286,10 @@ let value_append = function | [v1; v2] -> V_vector (coerce_gv v1 @ coerce_gv v2) | _ -> failwith "value append" +let value_append_list = function + | [v1; v2] -> V_list (coerce_list v1 @ coerce_list v2) + | _ -> failwith "value_append_list" + let value_slice = function | [v1; v2; v3] -> V_vector (Sail_lib.slice (coerce_gv v1, coerce_int v2, coerce_int v3)) | _ -> failwith "value slice" @@ -647,6 +655,7 @@ let primops = ("update_subrange", value_update_subrange); ("slice", value_slice); ("append", value_append); + ("append_list", value_append_list); ("not", value_not); ("not_vec", value_not_vec); ("and_vec", value_and_vec); |