diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/libsail.mllib | 3 | ||||
| -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 |
6 files changed, 224 insertions, 16 deletions
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/sail.ml b/src/sail.ml index c2b2ed65..13fea6f2 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 39485769..83d58178 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) |