summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/META6
-rw-r--r--src/Makefile6
-rw-r--r--src/_tags6
-rw-r--r--src/ast_util.ml85
-rw-r--r--src/ast_util.mli13
-rw-r--r--src/constant_fold.ml19
-rw-r--r--src/constant_propagation.ml2
-rw-r--r--src/constant_propagation_mutrec.ml2
-rw-r--r--src/elf_loader.ml18
-rw-r--r--src/initial_check.ml12
-rw-r--r--src/interpreter.ml504
-rw-r--r--src/isail.ml74
-rw-r--r--src/libsail.mllib60
-rw-r--r--src/monomorphise.ml3
-rw-r--r--src/ocaml_backend.ml10
-rw-r--r--src/parse_ast.ml2
-rw-r--r--src/parser.mly22
-rw-r--r--src/pretty_print_coq.ml4
-rw-r--r--src/pretty_print_lem.ml2
-rw-r--r--src/pretty_print_sail.ml6
-rw-r--r--src/rewrites.ml18
-rw-r--r--src/sail.ml31
-rw-r--r--src/specialize.ml4
-rw-r--r--src/toFromInterp_backend.ml361
-rw-r--r--src/toFromInterp_lib.ml126
-rw-r--r--src/type_check.ml63
-rw-r--r--src/type_check.mli6
-rw-r--r--src/value.ml43
28 files changed, 1297 insertions, 211 deletions
diff --git a/src/META b/src/META
new file mode 100644
index 00000000..80194d98
--- /dev/null
+++ b/src/META
@@ -0,0 +1,6 @@
+# META file of package sail:
+description = "Sail is a language for describing the instruction-set architecture (ISA) semantics of processors."
+requires = "linenoise lem linksem omd base64 yojson"
+version = "0.8"
+archive(byte) = "libsail.cma"
+archive(native) = "libsail.cmxa"
diff --git a/src/Makefile b/src/Makefile
index d71c9fb8..a002d4f3 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -103,7 +103,8 @@ sail: ast.ml jib.ml manifest.ml
ocamlbuild -use-ocamlfind sail.native sail_lib.cma sail_lib.cmxa
isail: ast.ml jib.ml manifest.ml
- ocamlbuild -use-ocamlfind isail.native
+ ocamlbuild -use-ocamlfind isail.native sail_lib.cma sail_lib.cmxa libsail.cma libsail.cmxa
+
coverage: ast.ml jib.ml manifest.ml
BISECT_COVERAGE=YES ocamlbuild -use-ocamlfind -plugin-tag 'package(bisect_ppx-ocamlbuild)' isail.native
@@ -113,6 +114,9 @@ sail.native: sail
sail.byte: ast.ml jib.ml manifest.ml
ocamlbuild -use-ocamlfind -cflag -g sail.byte
+isail.byte: ast.ml bytecode.ml share_directory.ml
+ ocamlbuild -use-ocamlfind isail.byte
+
interpreter: lem_interp/interp_ast.lem
ocamlbuild -use-ocamlfind lem_interp/extract.cmxa
ocamlbuild -use-ocamlfind lem_interp/extract.cma
diff --git a/src/_tags b/src/_tags
index f792fefa..41b443de 100644
--- a/src/_tags
+++ b/src/_tags
@@ -2,13 +2,13 @@ true: -traverse, debug, use_menhir
<**/parser.ml>: bin_annot, annot
<**/*.ml> and not <**/parser.ml>: bin_annot, annot
-<sail.{byte,native}>: package(zarith), package(linksem), package(lem), package(omd), use_pprint
-<isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), package(omd), package(yojson), use_pprint
+<sail.{byte,native}>: package(zarith), package(linksem), package(lem), package(omd), package(base64), use_pprint
+<isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), package(omd), package(base64), package(yojson), use_pprint
<isail.ml>: package(linenoise), package(yojson)
<elf_loader.ml>: package(linksem)
<latex.ml>: package(omd)
-<**/*.m{l,li}>: package(lem)
+<**/*.m{l,li}>: package(lem), package(base64)
<gen_lib>: include
<jib>: include
diff --git a/src/ast_util.ml b/src/ast_util.ml
index d0efc0de..386c080a 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -619,6 +619,80 @@ and map_lexp_annot_aux f = function
| LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2)
| LEXP_field (lexp, id) -> LEXP_field (map_lexp_annot f lexp, id)
+and map_typedef_annot f = function
+ | TD_aux (td_aux, annot) -> TD_aux (td_aux, f annot)
+
+and map_fundef_annot f = function
+ | FD_aux (fd_aux, annot) -> FD_aux (map_fundef_annot_aux f fd_aux, f annot)
+and map_fundef_annot_aux f = function
+ | FD_function (rec_opt, tannot_opt, eff_opt, funcls) -> FD_function (map_recopt_annot f rec_opt, tannot_opt, eff_opt,
+ List.map (map_funcl_annot f) funcls)
+and map_funcl_annot f = function
+ | FCL_aux (fcl, annot) -> FCL_aux (map_funcl_annot_aux f fcl, f annot)
+and map_funcl_annot_aux f = function
+ | FCL_Funcl (id, pexp) -> FCL_Funcl (id, map_pexp_annot f pexp)
+and map_recopt_annot f = function
+ | Rec_aux (rec_aux, l) -> Rec_aux (map_recopt_annot_aux f rec_aux, l)
+and map_recopt_annot_aux f = function
+ | Rec_nonrec -> Rec_nonrec
+ | Rec_rec -> Rec_rec
+ | Rec_measure (pat, exp) -> Rec_measure (map_pat_annot f pat, map_exp_annot f exp)
+
+and map_mapdef_annot f = function
+ | MD_aux (md_aux, annot) -> MD_aux (map_mapdef_annot_aux f md_aux, f annot)
+and map_mapdef_annot_aux f = function
+ | MD_mapping (id, tannot_opt, mapcls) -> MD_mapping (id, tannot_opt, List.map (map_mapcl_annot f) mapcls)
+
+and map_valspec_annot f = function
+ | VS_aux (vs_aux, annot) -> VS_aux (vs_aux, f annot)
+
+and map_scattered_annot f = function
+ | SD_aux (sd_aux, annot) -> SD_aux (map_scattered_annot_aux f sd_aux, f annot)
+and map_scattered_annot_aux f = function
+ | SD_function (rec_opt, tannot_opt, eff_opt, name) -> SD_function (map_recopt_annot f rec_opt, tannot_opt, eff_opt, name)
+ | SD_funcl fcl -> SD_funcl (map_funcl_annot f fcl)
+ | SD_variant (id, typq) -> SD_variant (id, typq)
+ | SD_unioncl (id, tu) -> SD_unioncl (id, tu)
+ | SD_mapping (id, tannot_opt) -> SD_mapping (id, tannot_opt)
+ | SD_mapcl (id, mcl) -> SD_mapcl (id, map_mapcl_annot f mcl)
+ | SD_end id -> SD_end id
+
+and map_decspec_annot f = function
+ | DEC_aux (dec_aux, annot) -> DEC_aux (map_decspec_annot_aux f dec_aux, f annot)
+and map_decspec_annot_aux f = function
+ | DEC_reg (eff1, eff2, typ, id) -> DEC_reg (eff1, eff2, typ, id)
+ | DEC_config (id, typ, exp) -> DEC_config (id, typ, map_exp_annot f exp)
+ | DEC_alias (id, als) -> DEC_alias (id, map_aliasspec_annot f als)
+ | DEC_typ_alias (typ, id, als) -> DEC_typ_alias (typ, id, map_aliasspec_annot f als)
+and map_aliasspec_annot f = function
+ | AL_aux (al_aux, annot) -> AL_aux (map_aliasspec_annot_aux f al_aux, f annot)
+and map_aliasspec_annot_aux f = function
+ | AL_subreg (reg_id, id) -> AL_subreg (map_regid_annot f reg_id, id)
+ | AL_bit (reg_id, exp) -> AL_bit (map_regid_annot f reg_id, map_exp_annot f exp)
+ | AL_slice (reg_id, exp1, exp2) -> AL_slice (map_regid_annot f reg_id, map_exp_annot f exp1, map_exp_annot f exp2)
+ | AL_concat (reg_id1, reg_id2) -> AL_concat (map_regid_annot f reg_id1, map_regid_annot f reg_id2)
+and map_regid_annot f = function
+ | RI_aux (ri_aux, annot) -> RI_aux (map_regid_annot_aux f ri_aux, f annot)
+and map_regid_annot_aux f = function
+ | RI_id id -> RI_id id
+
+and map_def_annot f = function
+ | DEF_type td -> DEF_type (map_typedef_annot f td)
+ | DEF_fundef fd -> DEF_fundef (map_fundef_annot f fd)
+ | DEF_mapdef md -> DEF_mapdef (map_mapdef_annot f md)
+ | DEF_val lb -> DEF_val (map_letbind_annot f lb)
+ | DEF_spec vs -> DEF_spec (map_valspec_annot f vs)
+ | DEF_fixity (prec, n, id) -> DEF_fixity (prec, n, id)
+ | DEF_overload (name, overloads) -> DEF_overload (name, overloads)
+ | DEF_default ds -> DEF_default ds
+ | DEF_scattered sd -> DEF_scattered (map_scattered_annot f sd)
+ | DEF_measure (id, pat, exp) -> DEF_measure (id, map_pat_annot f pat, map_exp_annot f exp)
+ | DEF_reg_dec ds -> DEF_reg_dec (map_decspec_annot f ds)
+ | DEF_internal_mutrec fds -> DEF_internal_mutrec (List.map (map_fundef_annot f) fds)
+ | DEF_pragma (name, arg, l) -> DEF_pragma (name, arg, l)
+and map_defs_annot f = function
+ | Defs defs -> Defs (List.map (map_def_annot f) defs)
+
let id_loc = function
| Id_aux (_, l) -> l
@@ -853,7 +927,7 @@ let rec string_of_exp (E_aux (exp, _)) =
| E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")"
| E_internal_plet (pat, exp, body) -> "internal_plet " ^ string_of_pat pat ^ " = " ^ string_of_exp exp ^ " in " ^ string_of_exp body
| E_nondet _ -> "NONDET"
- | E_internal_value _ -> "INTERNAL VALUE"
+ | E_internal_value v -> "INTERNAL_VALUE(" ^ Value.string_of_value v ^ ")"
and string_of_fexp (FE_aux (FE_Fexp (field, exp), _)) =
string_of_id field ^ " = " ^ string_of_exp exp
@@ -1728,6 +1802,15 @@ let unique l =
incr unique_ref;
l
+let extern_assoc backend exts =
+ try
+ try
+ Some (List.assoc backend exts)
+ with Not_found ->
+ Some (List.assoc "_" exts)
+ with Not_found ->
+ None
+
(**************************************************************************)
(* 1. Substitutions *)
(**************************************************************************)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 1f459870..cfbc26fe 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -346,8 +346,17 @@ val map_mfpat_annot : ('a annot -> 'b annot) -> 'a mfpat -> 'b mfpat
val map_mpexp_annot : ('a annot -> 'b annot) -> 'a mpexp -> 'b mpexp
val map_mapcl_annot : ('a annot -> 'b annot) -> 'a mapcl -> 'b mapcl
-(** {2 Extract locations from terms} *)
+val map_typedef_annot : ('a annot -> 'b annot) -> 'a type_def -> 'b type_def
+val map_fundef_annot : ('a annot -> 'b annot) -> 'a fundef -> 'b fundef
+val map_funcl_annot : ('a annot -> 'b annot) -> 'a funcl -> 'b funcl
+val map_mapdef_annot : ('a annot -> 'b annot) -> 'a mapdef -> 'b mapdef
+val map_valspec_annot : ('a annot -> 'b annot) -> 'a val_spec -> 'b val_spec
+val map_scattered_annot : ('a annot -> 'b annot) -> 'a scattered_def -> 'b scattered_def
+
+val map_def_annot : ('a annot -> 'b annot) -> 'a def -> 'b def
+val map_defs_annot : ('a annot -> 'b annot) -> 'a defs -> 'b defs
+(** {2 Extract locations from terms} *)
val id_loc : id -> Parse_ast.l
val kid_loc : kid -> Parse_ast.l
val typ_loc : typ -> Parse_ast.l
@@ -483,6 +492,8 @@ val locate_typ : (l -> l) -> typ -> typ
a generated number. *)
val unique : l -> l
+val extern_assoc : string -> (string * string) list -> string option
+
(** Try to find the annotation closest to the provided (simplified)
location. Note that this function makes no guarantees about finding
the closest annotation or even finding an annotation at all. This
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index fd9b322b..14d6550c 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -81,7 +81,8 @@ and exp_of_value =
| V_tuple vs ->
mk_exp (E_tuple (List.map exp_of_value vs))
| V_unit -> mk_lit_exp L_unit
- | V_attempted_read str -> mk_exp (E_id (mk_id str))
+ | V_attempted_read str ->
+ mk_exp (E_id (mk_id str))
| _ -> failwith "No expression for value"
(* We want to avoid evaluating things like print statements at compile
@@ -155,10 +156,20 @@ and is_constant_fexp (FE_aux (FE_Fexp (_, exp), _)) = is_constant exp
let rec run frame =
match frame with
| Interpreter.Done (state, v) -> v
+ | Interpreter.Fail _ ->
+ (* something went wrong, raise exception to abort constant folding *)
+ assert false
| Interpreter.Step (lazy_str, _, _, _) ->
run (Interpreter.eval_frame frame)
| Interpreter.Break frame ->
run (Interpreter.eval_frame frame)
+ | Interpreter.Effect_request (out, st, stack, Interpreter.Read_reg (reg, cont)) ->
+ (* return a dummy value to read_reg requests which we handle above
+ if an expression finally evals to it, but the interpreter
+ will fail if it tries to actually use. See value.ml *)
+ run (cont (Value.V_attempted_read reg) st)
+ | Interpreter.Effect_request _ ->
+ assert false (* effectful, raise exception to abort constant folding *)
(** This rewriting pass looks for function applications (E_app)
expressions where every argument is a literal. It passes these
@@ -177,9 +188,9 @@ let rec run frame =
- Throws an exception that isn't caught.
*)
-let initial_state ast =
+let initial_state ast env =
let lstate, gstate =
- Interpreter.initial_state ast safe_primops
+ Interpreter.initial_state ast env safe_primops
in
(lstate, { gstate with Interpreter.allow_registers = false })
@@ -243,7 +254,7 @@ let rec rewrite_constant_function_calls' ast =
let rw_defs = {
rewriters_base with
- rewrite_exp = (fun _ -> rw_exp ok not_ok (initial_state ast))
+ rewrite_exp = (fun _ -> rw_exp ok not_ok (initial_state ast Type_check.initial_env))
} in
let ast = rewrite_defs_base rw_defs ast in
(* We keep iterating until we have no more re-writes to do *)
diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index 5c99a534..ce04798a 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -310,7 +310,7 @@ let const_props defs ref_vars =
let undefined_builtin_ids = ids_of_defs (Defs Initial_check.undefined_builtin_val_specs) in
let remove_primop id = StringMap.remove (string_of_id id) in
let remove_undefined_primops = IdSet.fold remove_primop undefined_builtin_ids in
- let (lstate, gstate) = Constant_fold.initial_state defs in
+ let (lstate, gstate) = Constant_fold.initial_state defs Type_check.initial_env in
(lstate, { gstate with primops = remove_undefined_primops gstate.primops })
in
try
diff --git a/src/constant_propagation_mutrec.ml b/src/constant_propagation_mutrec.ml
index 683cc6f3..285ba45d 100644
--- a/src/constant_propagation_mutrec.ml
+++ b/src/constant_propagation_mutrec.ml
@@ -125,7 +125,7 @@ let generate_val_spec env id args l annot =
mk_typquant
in
let typschm = mk_typschm tq' typ' in
- mk_val_spec (VS_val_spec (typschm, generate_fun_id id args, (fun _ -> None), false)),
+ mk_val_spec (VS_val_spec (typschm, generate_fun_id id args, [], false)),
ksubsts
| _, Typ_aux (_, l) ->
raise (Reporting.err_unreachable l __POS__ "Function val spec is not a function type")
diff --git a/src/elf_loader.ml b/src/elf_loader.ml
index d6016c8b..99407393 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -176,6 +176,24 @@ let load_elf ?writer:(writer=write_sail_lib) name =
opt_elf_class := ELF_Class_32
)
+let load_binary ?writer:(writer=write_sail_lib) addr name =
+ let f = open_in_bin name in
+ let buf = Buffer.create 1024 in
+ try
+ while true do
+ let char = input_char f in
+ Buffer.add_char buf char;
+ done;
+ assert false
+ with
+ | End_of_file -> begin
+ Bytes.iteri (fun i ch -> writer addr i (int_of_char ch)) (Buffer.to_bytes buf);
+ close_in f
+ end
+ | exc ->
+ close_in f;
+ raise exc
+
(* The sail model can access this by externing a unit -> int function
as Elf_loader.elf_entry. *)
let elf_entry () = !opt_elf_entry
diff --git a/src/initial_check.ml b/src/initial_check.ml
index df9af97f..28446db2 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -856,8 +856,8 @@ let constraint_of_string str =
let atyp = Parser.typ_eof Lexer.token (Lexing.from_string str) in
to_ast_constraint initial_ctx atyp
-let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> Some (string_of_id id)), false))
-let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> None), false))
+let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, [("_", string_of_id id)], false))
+let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, [], false))
let quant_item_param = function
| QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
@@ -921,7 +921,7 @@ let generate_undefineds vs_ids (Defs defs) =
let undefined_td = function
| TD_enum (id, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
let typschm = typschm_of_string ("unit -> " ^ string_of_id id ^ " effect {undef}") in
- [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false));
+ [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, [], false));
mk_fundef [mk_funcl (prepend_id "undefined_" id)
(mk_pat (P_lit (mk_lit L_unit)))
(if !opt_fast_undefined && List.length ids > 0 then
@@ -931,7 +931,7 @@ let generate_undefineds vs_ids (Defs defs) =
[mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
| TD_record (id, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in
- [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
+ [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false));
mk_fundef [mk_funcl (prepend_id "undefined_" id)
pat
(mk_exp (E_record (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields)))]]
@@ -979,7 +979,7 @@ let generate_undefineds vs_ids (Defs defs) =
(mk_exp (E_app (mk_id "internal_pick",
[mk_exp (E_list (List.map (make_constr typ_to_var) constr_args))]))) letbinds
in
- [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
+ [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false));
mk_fundef [mk_funcl (prepend_id "undefined_" id)
pat
body]]
@@ -1015,7 +1015,7 @@ let generate_enum_functions vs_ids (Defs defs) =
let rec gen_enums = function
| DEF_type (TD_aux (TD_enum (id, elems, _), _)) as enum :: defs ->
let enum_val_spec name quants typ =
- mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, (fun _ -> None), !opt_enum_casts))
+ mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, [], !opt_enum_casts))
in
let range_constraint kid = nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1))) in
diff --git a/src/interpreter.ml b/src/interpreter.ml
index f01a3846..263430f1 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -52,12 +52,16 @@ open Ast
open Ast_util
open Value
+
+
type gstate =
{ registers : value Bindings.t;
allow_registers : bool; (* For some uses we want to forbid touching any registers. *)
primops : (value list -> value) StringMap.t;
letbinds : (Type_check.tannot letbind) list;
fundefs : (Type_check.tannot fundef) Bindings.t;
+ last_write_ea : (value * value * value) option;
+ typecheck_env : Type_check.Env.t;
}
type lstate =
@@ -91,18 +95,19 @@ let value_of_lit (L_aux (l_aux, _)) =
V_real (Rational.add whole frac)
| _ -> failwith "could not parse real literal"
end
- | _ -> failwith "Unimplemented value_of_lit" (* TODO *)
+ | L_undef -> failwith "value_of_lit of undefined"
+
let is_value = function
| (E_aux (E_internal_value _, _)) -> true
| _ -> false
let is_true = function
- | (E_aux (E_internal_value (V_bool b), _)) -> b == true
+ | (E_aux (E_internal_value (V_bool b), annot)) -> b
| _ -> false
let is_false = function
- | (E_aux (E_internal_value (V_bool b), _)) -> b == false
+ | (E_aux (E_internal_value (V_bool b), _)) -> not b
| _ -> false
let exp_of_value v = (E_aux (E_internal_value v, (Parse_ast.Unknown, Type_check.empty_tannot)))
@@ -127,13 +132,24 @@ type return_value =
| Return_ok of value
| Return_exception of value
+(* when changing effect arms remember to also update effect_request type below *)
type 'a response =
| Early_return of value
| Exception of value
| Assertion_failed of string
| Call of id * value list * (return_value -> 'a)
- | Gets of (state -> 'a)
- | Puts of state * (unit -> 'a)
+ | Fail of string
+ | Read_mem of (* read_kind : *) value * (* address : *) value * (* length : *) value * (value -> 'a)
+ | Write_ea of (* write_kind : *) value * (* address : *) value * (* length : *) value * (unit -> 'a)
+ | Excl_res of (bool -> 'a)
+ | Write_mem of (* write_kind : *) value * (* address : *) value * (* length : *) value * (* value : *) value * (bool -> 'a)
+ | Barrier of (* barrier_kind : *) value * (unit -> 'a)
+ | Read_reg of string * (value -> 'a)
+ | Write_reg of string * value * (unit -> 'a)
+ | Get_primop of string * ((value list -> value) -> 'a)
+ | Get_local of string * (value -> 'a)
+ | Put_local of string * value * (unit -> 'a)
+ | Get_global_letbinds of ((Type_check.tannot letbind) list -> 'a)
and 'a monad =
| Pure of 'a
@@ -143,9 +159,19 @@ let map_response f = function
| Early_return v -> Early_return v
| Exception v -> Exception v
| Assertion_failed str -> Assertion_failed str
- | Gets g -> Gets (fun s -> f (g s))
- | Puts (s, cont) -> Puts (s, fun () -> f (cont ()))
| Call (id, vals, cont) -> Call (id, vals, fun v -> f (cont v))
+ | Fail s -> Fail s
+ | Read_mem (rk, addr, len, cont) -> Read_mem (rk, addr, len, fun v -> f (cont v))
+ | Write_ea (wk, addr, len, cont) -> Write_ea (wk, addr, len, fun () -> f (cont ()))
+ | Excl_res cont -> Excl_res (fun b -> f (cont b))
+ | Write_mem (wk, addr, len, v, cont) -> Write_mem (wk, addr, len, v, fun b -> f (cont b))
+ | Barrier (bk, cont) -> Barrier (bk, fun () -> f (cont ()))
+ | Read_reg (name, cont) -> Read_reg (name, fun v -> f (cont v))
+ | Write_reg (name, v, cont) -> Write_reg (name, v, fun () -> f (cont ()))
+ | Get_primop (name, cont) -> Get_primop (name, fun op -> f (cont op))
+ | Get_local (name, cont) -> Get_local (name, fun v -> f (cont v))
+ | Put_local (name, v, cont) -> Put_local (name, v, fun () -> f (cont ()))
+ | Get_global_letbinds cont -> Get_global_letbinds (fun lbs -> f (cont lbs))
let rec liftM f = function
| Pure x -> Pure (f x)
@@ -179,12 +205,43 @@ let throw v = Yield (Exception v)
let call (f : id) (args : value list) : return_value monad =
Yield (Call (f, args, fun v -> Pure v))
-let gets : state monad =
- Yield (Gets (fun s -> Pure s))
-let puts (s : state) : unit monad =
- Yield (Puts (s, fun () -> Pure ()))
+let read_mem rk addr len : value monad =
+ Yield (Read_mem (rk, addr, len, (fun v -> Pure v)))
+
+let write_ea wk addr len : unit monad =
+ Yield (Write_ea (wk, addr, len, (fun () -> Pure ())))
+
+let excl_res () : bool monad =
+ Yield (Excl_res (fun b -> Pure b))
+
+let write_mem wk addr len v : bool monad =
+ Yield (Write_mem (wk, addr, len, v, fun b -> Pure b))
+
+let barrier bk : unit monad =
+ Yield (Barrier (bk, fun () -> Pure ()))
+
+let read_reg name : value monad =
+ Yield (Read_reg (name, fun v -> Pure v))
+let write_reg name v : unit monad =
+ Yield (Write_reg (name, v, fun () -> Pure ()))
+
+let fail s =
+ Yield (Fail s)
+
+let get_primop name : (value list -> value) monad =
+ Yield (Get_primop (name, fun op -> Pure op))
+
+let get_local name : value monad =
+ Yield (Get_local (name, fun v -> Pure v))
+
+let put_local name v : unit monad =
+ Yield (Put_local (name, v, fun () -> Pure ()))
+
+let get_global_letbinds () : (Type_check.tannot letbind) list monad =
+ Yield (Get_global_letbinds (fun lbs -> Pure lbs))
+
let early_return v = Yield (Early_return v)
let assertion_failed msg = Yield (Assertion_failed msg)
@@ -220,12 +277,11 @@ let rec build_letchain id lbs (E_aux (_, annot) as exp) =
let is_interpreter_extern id env =
let open Type_check in
- Env.is_extern id env "interpreter" || Env.is_extern id env "ocaml"
+ Env.is_extern id env "interpreter"
let get_interpreter_extern id env =
let open Type_check in
- try Env.get_extern id env "interpreter" with
- | Type_error _ -> Env.get_extern id env "ocaml"
+ Env.get_extern id env "interpreter"
let rec step (E_aux (e_aux, annot) as orig_exp) =
let wrap e_aux' = return (E_aux (e_aux', annot)) in
@@ -236,7 +292,20 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| E_block (exp :: exps) ->
step exp >>= fun exp' -> wrap (E_block (exp' :: exps))
- | E_lit lit -> return (exp_of_value (value_of_lit lit))
+ | E_lit (L_aux (L_undef, _)) ->
+ begin
+ let env = Type_check.env_of_annot annot in
+ let typ = Type_check.typ_of_annot annot in
+ let undef_exp = Ast_util.undefined_of_typ false Parse_ast.Unknown (fun _ -> ()) typ in
+ let undef_exp = Type_check.check_exp env undef_exp typ in
+ return undef_exp
+ end
+
+ | E_lit lit ->
+ begin
+ try return (exp_of_value (value_of_lit lit))
+ with Failure s -> fail ("Failure: " ^ s)
+ end
| E_if (exp, then_exp, else_exp) when is_true exp -> return then_exp
| E_if (exp, then_exp, else_exp) when is_false exp -> return else_exp
@@ -248,7 +317,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| E_assert (exp, msg) when is_true exp -> wrap unit_exp
| E_assert (exp, msg) when is_false exp && is_value msg ->
- failwith (coerce_string (value_of_exp msg))
+ assertion_failed (coerce_string (value_of_exp msg))
| E_assert (exp, msg) when is_false exp ->
step msg >>= fun msg' -> wrap (E_assert (exp, msg'))
| E_assert (exp, msg) ->
@@ -287,7 +356,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
if matched then
return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings))
else
- failwith "Match failure"
+ fail "Match failure"
| E_vector_subrange (vec, n, m) ->
wrap (E_app (mk_id "vector_subrange_dec", [vec; n; m]))
@@ -313,16 +382,50 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| [] when is_interpreter_extern id (env_of_annot annot) ->
begin
let extern = get_interpreter_extern id (env_of_annot annot) in
- if extern = "reg_deref" then
- let regname = List.hd evaluated |> value_of_exp |> coerce_ref in
- gets >>= fun (_, gstate) ->
- if gstate.allow_registers
- then return (exp_of_value (Bindings.find (mk_id regname) gstate.registers))
- else raise Not_found
- else
- gets >>= fun (_, gstate) ->
- let primop = try StringMap.find extern gstate.primops with Not_found -> failwith ("No primop " ^ extern) in
- return (exp_of_value (primop (List.map value_of_exp evaluated)))
+ match extern with
+ | "reg_deref" ->
+ let regname = List.hd evaluated |> value_of_exp |> coerce_ref in
+ read_reg regname >>= fun v -> return (exp_of_value v)
+ | "read_mem" ->
+ begin match evaluated with
+ | [rk; 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] ->
+ 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"
+ end
+ | "excl_res" ->
+ begin match evaluated with
+ | [_] ->
+ excl_res () >>= fun b -> return (exp_of_value (V_bool b))
+ | _ ->
+ fail "Wrong number of parameters to excl_res intrinsic"
+ end
+ | "write_mem" ->
+ begin match evaluated with
+ | [wk; 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"
+ end
+ | "barrier" ->
+ begin match evaluated with
+ | [bk] ->
+ barrier (value_of_exp bk) >> wrap unit_exp
+ | _ ->
+ fail "Wrong number of parameters to barrier intrinsic"
+ end
+ | _ ->
+ get_primop extern >>=
+ fun op -> try
+ return (exp_of_value (op (List.map value_of_exp evaluated)))
+ with _ as exc -> fail ("Exception calling primop '" ^ extern ^ "': " ^ Printexc.to_string exc)
end
| [] ->
call id (List.map value_of_exp evaluated) >>=
@@ -352,22 +455,28 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| E_case (exp, pexps) when not (is_value exp) ->
step exp >>= fun exp' -> wrap (E_case (exp', pexps))
- | E_case (_, []) -> failwith "Pattern matching failed"
+ | E_case (_, []) -> fail "Pattern matching failed"
| E_case (exp, Pat_aux (Pat_exp (pat, body), _) :: pexps) ->
- let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in
- if matched then
- return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings))
- else
- wrap (E_case (exp, pexps))
+ begin try
+ let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in
+ if matched then
+ return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings))
+ else
+ wrap (E_case (exp, pexps))
+ with Failure s -> fail ("Failure: " ^ s)
+ end
| E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when not (is_value guard) ->
- let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in
- if matched then
- let guard = List.fold_left (fun guard (id, v) -> subst id v guard) guard (Bindings.bindings bindings) in
- let body = List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings) in
- step guard >>= fun guard' ->
- wrap (E_case (exp, Pat_aux (Pat_when (pat, guard', body), pat_annot) :: pexps))
- else
- wrap (E_case (exp, pexps))
+ begin try
+ let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in
+ if matched then
+ let guard = List.fold_left (fun guard (id, v) -> subst id v guard) guard (Bindings.bindings bindings) in
+ let body = List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings) in
+ step guard >>= fun guard' ->
+ wrap (E_case (exp, Pat_aux (Pat_when (pat, guard', body), pat_annot) :: pexps))
+ else
+ wrap (E_case (exp, pexps))
+ with Failure s -> fail ("Failure: " ^ s)
+ end
| E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when is_true guard -> return body
| E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when is_false guard -> wrap (E_case (exp, pexps))
@@ -379,35 +488,23 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| E_exit exp -> step exp >>= fun exp' -> wrap (E_exit exp')
| E_ref id ->
- gets >>= fun (lstate, gstate) ->
- if Bindings.mem id gstate.registers && gstate.allow_registers then
- return (exp_of_value (V_ref (string_of_id id)))
- else
- failwith ("Could not find register " ^ string_of_id id)
+ return (exp_of_value (V_ref (string_of_id id)))
| E_id id ->
begin
let open Type_check in
- gets >>= fun (lstate, gstate) ->
match Env.lookup_id id (env_of_annot annot) with
- | Register _ when gstate.allow_registers ->
- let exp =
- try exp_of_value (Bindings.find id gstate.registers) with
- | Not_found ->
- (* Replace with error message? *)
- let exp = mk_exp (E_app (mk_id ("undefined_" ^ string_of_typ (typ_of orig_exp)), [mk_exp (E_lit (mk_lit (L_unit)))])) in
- Type_check.check_exp (env_of_annot annot) exp (typ_of orig_exp)
- in
- return exp
- | Register _ when not gstate.allow_registers ->
- return (exp_of_value (V_attempted_read (string_of_id id)))
- | Local (Mutable, _) -> return (local_variable id lstate gstate)
+ | Register _ ->
+ read_reg (string_of_id id) >>= fun v -> return (exp_of_value v)
+ | Local (Mutable, _) -> get_local (string_of_id id) >>= fun v -> return (exp_of_value v)
| Local (Immutable, _) ->
- let chain = build_letchain id gstate.letbinds orig_exp in
+ (* if we get here without already having substituted, it must be a top-level letbind *)
+ get_global_letbinds () >>= fun lbs ->
+ let chain = build_letchain id lbs orig_exp in
return chain
| Enum _ ->
return (exp_of_value (V_ctor (string_of_id id, [])))
- | _ -> failwith ("Couldn't find id " ^ string_of_id id)
+ | _ -> fail ("Couldn't find id " ^ string_of_id id)
end
| E_record fexps ->
@@ -456,45 +553,51 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| E_assign (lexp, exp) when not (is_value exp) -> step exp >>= fun exp' -> wrap (E_assign (lexp, exp'))
| E_assign (LEXP_aux (LEXP_memory (id, args), _), exp) -> wrap (E_app (id, args @ [exp]))
| E_assign (LEXP_aux (LEXP_field (lexp, id), ul), exp) ->
- let open Type_check in
- let lexp_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp lexp)) in
- let exp' = E_aux (E_record_update (lexp_exp, [FE_aux (FE_Fexp (id, exp), ul)]), ul) in
- wrap (E_assign (lexp, exp'))
+ begin try
+ let open Type_check in
+ let lexp_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp lexp)) in
+ let exp' = E_aux (E_record_update (lexp_exp, [FE_aux (FE_Fexp (id, exp), ul)]), ul) in
+ wrap (E_assign (lexp, exp'))
+ with Failure s -> fail ("Failure: " ^ s)
+ end
| E_assign (LEXP_aux (LEXP_vector (vec, n), lexp_annot), exp) ->
- let open Type_check in
- let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in
- let exp' = E_aux (E_vector_update (vec_exp, n, exp), lexp_annot) in
- wrap (E_assign (vec, exp'))
+ begin try
+ let open Type_check in
+ let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in
+ let exp' = E_aux (E_vector_update (vec_exp, n, exp), lexp_annot) in
+ wrap (E_assign (vec, exp'))
+ with Failure s -> fail ("Failure: " ^ s)
+ end
| E_assign (LEXP_aux (LEXP_vector_range (vec, n, m), lexp_annot), exp) ->
- let open Type_check in
- let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in
- (* FIXME: let the type checker check this *)
- let exp' = E_aux (E_vector_update_subrange (vec_exp, n, m, exp), lexp_annot) in
- wrap (E_assign (vec, exp'))
+ begin try
+ let open Type_check in
+ let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in
+ (* FIXME: let the type checker check this *)
+ let exp' = E_aux (E_vector_update_subrange (vec_exp, n, m, exp), lexp_annot) in
+ wrap (E_assign (vec, exp'))
+ with Failure s -> fail ("Failure: " ^ s)
+ end
| E_assign (LEXP_aux (LEXP_id id, _), exp) | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) ->
begin
let open Type_check in
- gets >>= fun (lstate, gstate) ->
+ let name = string_of_id id in
match Env.lookup_id id (env_of_annot annot) with
- | Register _ when gstate.allow_registers ->
- puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp
+ | Register _ ->
+ write_reg name (value_of_exp exp) >> wrap unit_exp
| Local (Mutable, _) | Unbound ->
- begin
- puts ({ locals = Bindings.add id (value_of_exp exp) lstate.locals }, gstate) >> wrap unit_exp
- end
- | _ -> failwith "Assign"
+ put_local name (value_of_exp exp) >> wrap unit_exp
+ | Local (Immutable, _) ->
+ fail ("Assignment to immutable local: " ^ name)
+ | Enum _ ->
+ fail ("Assignment to union constructor: " ^ name)
end
| E_assign (LEXP_aux (LEXP_deref reference, annot), exp) when not (is_value reference) ->
step reference >>= fun reference' -> wrap (E_assign (LEXP_aux (LEXP_deref reference', annot), exp))
| E_assign (LEXP_aux (LEXP_deref reference, annot), exp) ->
let name = coerce_ref (value_of_exp reference) in
- gets >>= fun (lstate, gstate) ->
- if Bindings.mem (mk_id name) gstate.registers && gstate.allow_registers then
- puts (lstate, { gstate with registers = Bindings.add (mk_id name) (value_of_exp exp) gstate.registers }) >> wrap unit_exp
- else
- failwith "Assign to nonexistent register"
- | E_assign (LEXP_aux (LEXP_tup lexps, annot), exp) -> failwith "Tuple assignment"
- | E_assign (LEXP_aux (LEXP_vector_concat lexps, annot), exp) -> failwith "Vector concat assignment"
+ write_reg name (value_of_exp exp) >> wrap unit_exp
+ | E_assign (LEXP_aux (LEXP_tup lexps, annot), exp) -> fail "Tuple assignment"
+ | E_assign (LEXP_aux (LEXP_vector_concat lexps, annot), exp) -> fail "Vector concat assignment"
(*
let values = coerce_tuple (value_of_exp exp) in
wrap (E_block (List.map2 (fun lexp v -> E_aux (E_assign (lexp, exp_of_value v), (Parse_ast.Unknown, None))) lexps values))
@@ -528,7 +631,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
wrap (E_block [subst id v_from body; E_aux (E_for (id, exp_of_value (value_sub_int [v_from; v_step]), exp_to, exp_step, ord, body), annot)])
| _ -> assert false
end
- | Ord_aux (Ord_var _, _) -> failwith "Polymorphic order in foreach"
+ | Ord_aux (Ord_var _, _) -> fail "Polymorphic order in foreach"
end
| E_for (id, exp_from, exp_to, exp_step, ord, body) when is_value exp_to && is_value exp_step ->
step exp_from >>= fun exp_from' -> wrap (E_for (id, exp_from', exp_to, exp_step, ord, body))
@@ -537,9 +640,23 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| E_for (id, exp_from, exp_to, exp_step, ord, body) ->
step exp_step >>= fun exp_step' -> wrap (E_for (id, exp_from, exp_to, exp_step', ord, body))
- | E_sizeof _ | E_constraint _ -> assert false (* Must be re-written before interpreting *)
+ | E_sizeof nexp ->
+ begin
+ match Type_check.big_int_of_nexp nexp with
+ | Some n -> return (exp_of_value (V_int n))
+ | None -> fail "Sizeof unevaluable nexp"
+ end
- | _ -> failwith ("Unimplemented " ^ string_of_exp orig_exp)
+ | E_cons (hd, tl) when is_value hd && is_value tl ->
+ let hd = value_of_exp hd in
+ let tl = coerce_listlike (value_of_exp tl) in
+ return (exp_of_value (V_list (hd :: tl)))
+ | E_cons (hd, tl) when is_value hd ->
+ step tl >>= fun tl' -> wrap (E_cons (hd, tl'))
+ | E_cons (hd, tl) ->
+ step hd >>= fun hd' -> wrap (E_cons (hd', tl))
+
+ | _ -> raise (Invalid_argument ("Unimplemented " ^ string_of_exp orig_exp))
and combine _ v1 v2 =
match (v1, v2) with
@@ -651,66 +768,197 @@ type frame =
| Done of state * value
| Step of string Lazy.t * state * (Type_check.tannot exp) monad * (string Lazy.t * lstate * (return_value -> (Type_check.tannot exp) monad)) list
| Break of frame
+ | Effect_request of string Lazy.t * state * (string Lazy.t * lstate * (return_value -> (Type_check.tannot exp) monad)) list * effect_request
+ | Fail of string Lazy.t * state * (Type_check.tannot exp) monad * (string Lazy.t * lstate * (return_value -> (Type_check.tannot exp) monad)) list * string
+
+(* when changing effect_request remember to also update response type above *)
+and effect_request =
+ | Read_mem of (* read_kind : *) value * (* address : *) value * (* length : *) value * (value -> state -> frame)
+ | Write_ea of (* write_kind : *) value * (* address : *) value * (* length : *) value * (unit -> state -> frame)
+ | Excl_res of (bool -> state -> frame)
+ | Write_mem of (* write_kind : *) value * (* address : *) value * (* length : *) value * (* value : *) value * (bool -> state -> frame)
+ | Barrier of (* barrier_kind : *) value * (unit -> state -> frame)
+ | Read_reg of string * (value -> state -> frame)
+ | Write_reg of string * value * (unit -> state -> frame)
let rec eval_frame' = function
| Done (state, v) -> Done (state, v)
+ | Fail (out, state, m, stack, msg) -> Fail (out, state, m, stack, msg)
| Break frame -> Break frame
+ | Effect_request (out, state, stack, eff) -> Effect_request (out, state, stack, eff)
| Step (out, state, m, stack) ->
+ let lstate, gstate = state in
match (m, stack) with
| Pure v, [] when is_value v -> Done (state, value_of_exp v)
| Pure v, (head :: stack') when is_value v ->
- Step (stack_string head, (stack_state head, snd state), stack_cont head (Return_ok (value_of_exp v)), stack')
+ Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_ok (value_of_exp v)), stack')
| Pure exp', _ ->
let out' = lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp')) in
Step (out', state, step exp', stack)
| Yield (Call(id, vals, cont)), _ when string_of_id id = "break" ->
- let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in
- let body = exp_of_fundef (Bindings.find id (snd state).fundefs) arg in
- Break (Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack))
+ begin
+ let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in
+ try
+ let body = exp_of_fundef (Bindings.find id gstate.fundefs) arg in
+ Break (Step (lazy "", (initial_lstate, gstate), return body, (out, lstate, cont) :: stack))
+ with Not_found ->
+ Step (out, state, fail ("Fundef not found: " ^ string_of_id id), stack)
+ end
| Yield (Call(id, vals, cont)), _ ->
- let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in
- let body = exp_of_fundef (Bindings.find id (snd state).fundefs) arg in
- Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack)
- | Yield (Gets cont), _ ->
- eval_frame' (Step (out, state, cont state, stack))
- | Yield (Puts (state', cont)), _ ->
+ begin
+ let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in
+ try
+ let body = exp_of_fundef (Bindings.find id gstate.fundefs) arg in
+ Step (lazy "", (initial_lstate, gstate), return body, (out, lstate, cont) :: stack)
+ with Not_found ->
+ Step (out, state, fail ("Fundef not found: " ^ string_of_id id), stack)
+ end
+
+ | Yield (Read_reg (name, cont)), _ ->
+ Effect_request (out, state, stack, Read_reg (name, fun v state' -> eval_frame' (Step (out, state', cont v, stack))))
+ | Yield (Write_reg (name, v, cont)), _ ->
+ Effect_request (out, state, stack, Write_reg (name, v, fun () state' -> eval_frame' (Step (out, state', cont (), stack))))
+ | Yield (Get_primop (name, cont)), _ ->
+ begin
+ try
+ let op = StringMap.find name gstate.primops in
+ eval_frame' (Step (out, state, cont op, stack))
+ with Not_found ->
+ eval_frame' (Step (out, state, fail ("No such primop: " ^ name), stack))
+ end
+ | Yield (Get_local (name, cont)), _ ->
+ begin
+ try
+ eval_frame' (Step (out, state, cont (Bindings.find (mk_id name) lstate.locals), stack))
+ with Not_found ->
+ eval_frame' (Step (out, state, fail ("Local not found: " ^ name), stack))
+ end
+ | Yield (Put_local (name, v, cont)), _ ->
+ let state' = ({ locals = Bindings.add (mk_id name) v lstate.locals }, gstate) in
eval_frame' (Step (out, state', cont (), stack))
+ | Yield (Get_global_letbinds cont), _ ->
+ eval_frame' (Step (out, state, cont gstate.letbinds, stack))
+ | Yield (Read_mem (rk, addr, len, cont)), _ ->
+ Effect_request (out, state, stack, Read_mem (rk, addr, len, fun result state' -> eval_frame' (Step (out, state', cont result, stack))))
+ | Yield (Write_ea (wk, addr, len, cont)), _ ->
+ Effect_request (out, state, stack, Write_ea (wk, addr, len, fun () state' -> eval_frame' (Step (out, state', cont (), stack))))
+ | Yield (Excl_res cont), _ ->
+ Effect_request (out, state, stack, Excl_res (fun b state' -> eval_frame' (Step (out, state', cont b, stack))))
+ | Yield (Write_mem (wk, addr, len, v, cont)), _ ->
+ Effect_request (out, state, stack, Write_mem (wk, addr, len, v, fun b state' -> eval_frame' (Step (out, state', cont b, stack))))
+ | Yield (Barrier (bk, cont)), _ ->
+ Effect_request (out, state, stack, Barrier (bk, fun () state' -> eval_frame' (Step (out, state', cont (), stack))))
| Yield (Early_return v), [] -> Done (state, v)
| Yield (Early_return v), (head :: stack') ->
- Step (stack_string head, (stack_state head, snd state), stack_cont head (Return_ok v), stack')
- | Yield (Assertion_failed msg), _ ->
- failwith msg
+ Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_ok v), stack')
+ | Yield (Assertion_failed msg), _ | Yield (Fail msg), _ ->
+ Fail (out, state, m, stack, msg)
| Yield (Exception v), [] ->
- failwith ("Uncaught Exception" |> Util.cyan |> Util.clear)
+ Fail (out, state, m, stack, "Uncaught exception: " ^ string_of_value v)
| Yield (Exception v), (head :: stack') ->
- Step (stack_string head, (stack_state head, snd state), stack_cont head (Return_exception v), stack')
+ Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_exception v), stack')
let eval_frame frame =
try eval_frame' frame with
| Type_check.Type_error (env, l, err) ->
raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+let default_effect_interp state eff =
+ let lstate, gstate = state in
+ match eff with
+ | Read_mem (rk, addr, len, cont) ->
+ (* all read-kinds treated the same in single-threaded interpreter *)
+ let addr' = coerce_bv addr in
+ let len' = coerce_int len in
+ let result = mk_vector (Sail_lib.read_ram (List.length addr', len', [], addr')) in
+ cont result state
+ | Write_ea (wk, addr, len, cont) ->
+ (* just store the values for the next Write_memv *)
+ let state' = (lstate, { gstate with last_write_ea = Some (wk, addr, len) }) in
+ cont () state'
+ | Excl_res cont ->
+ (* always succeeds in single-threaded interpreter *)
+ cont true state
+ | Write_mem (wk, addr, len, v, cont) ->
+ begin
+ match gstate.last_write_ea with
+ | Some (wk', addr', len') ->
+ let state' = (lstate, { gstate with last_write_ea = None }) in
+ (* all write-kinds treated the same in single-threaded interpreter *)
+ let addr' = coerce_bv addr in
+ let len' = coerce_int len in
+ let v' = coerce_bv v in
+ if Big_int.mul len' (Big_int.of_int 8) = Big_int.of_int (List.length v') then
+ let b = Sail_lib.write_ram (List.length addr', len', [], addr', v') in
+ cont b state
+ else
+ failwith "Write_memv with length mismatch to preceding Write_ea"
+ | None ->
+ failwith "Write_memv without preceding Write_ea"
+ end
+ | Barrier (bk, cont) ->
+ (* no-op in single-threaded interpreter *)
+ cont () state
+ | Read_reg (name, cont) ->
+ begin
+ if gstate.allow_registers then
+ try
+ cont (Bindings.find (mk_id name) gstate.registers) state
+ with Not_found ->
+ failwith ("Read of nonexistent register: " ^ name)
+ else
+ failwith ("Register read disallowed by allow_registers setting: " ^ name)
+ end
+ | Write_reg (name, v, cont) ->
+ begin
+ let id = mk_id name in
+ if gstate.allow_registers then
+ if Bindings.mem id gstate.registers then
+ let state' = (lstate, { gstate with registers = Bindings.add id v gstate.registers }) in
+ cont () state'
+ else
+ failwith ("Write of nonexistent register: " ^ name)
+ else
+ failwith ("Register write disallowed by allow_registers setting: " ^ name)
+ end
+
+
+
+
let rec run_frame frame =
match frame with
| Done (state, v) -> v
+ | Fail (_, _, _, _, msg) -> failwith ("run_frame got Fail: " ^ msg)
| Step (lazy_str, _, _, _) ->
run_frame (eval_frame frame)
| Break frame ->
run_frame (eval_frame frame)
+ | Effect_request (out, state, stack, eff) ->
+ run_frame (default_effect_interp state eff)
let eval_exp state exp =
run_frame (Step (lazy "", state, return exp, []))
-let initial_gstate primops ast =
+let initial_gstate primops ast env =
{ registers = Bindings.empty;
allow_registers = true;
primops = primops;
letbinds = ast_letbinds ast;
fundefs = Bindings.empty;
+ last_write_ea = None;
+ typecheck_env = env;
}
let rec initialize_registers gstate =
let process_def = function
+ | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), annot)) ->
+ begin
+ let env = Type_check.env_of_annot annot in
+ let typ = Type_check.Env.expand_synonyms env typ in
+ let exp = mk_exp (E_cast (typ, mk_exp (E_lit (mk_lit (L_undef))))) in
+ let exp = Type_check.check_exp env exp typ in
+ { gstate with registers = Bindings.add id (eval_exp (initial_lstate, gstate) exp) gstate.registers }
+ end
| DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
{ gstate with registers = Bindings.add id (eval_exp (initial_lstate, gstate) exp) gstate.registers }
| DEF_fundef fdef ->
@@ -722,4 +970,44 @@ let rec initialize_registers gstate =
initialize_registers (process_def def) (Defs defs)
| Defs [] -> gstate
-let initial_state ast primops = initial_lstate, initialize_registers (initial_gstate primops ast) ast
+let initial_state ast env primops = initial_lstate, initialize_registers (initial_gstate primops ast env) ast
+
+type value_result =
+ | Value_success of value
+ | Value_error of exn
+
+let decode_instruction state bv =
+ try
+ let env = (snd state).typecheck_env in
+ let untyped = mk_exp (E_app ((mk_id "decode"), [mk_exp (E_vector (List.map mk_lit_exp bv))])) in
+ let typed = Type_check.check_exp
+ env untyped (app_typ (mk_id "option")
+ [A_aux (A_typ (mk_typ (Typ_id (mk_id "ast"))), Parse_ast.Unknown)]) in
+ let evaled = eval_exp state typed in
+ match evaled with
+ | V_ctor ("Some", [v]) -> Value_success v
+ | V_ctor ("None", _) -> failwith "decode returned None"
+ | _ -> failwith "decode returned wrong value type"
+ with _ as exn ->
+ Value_error exn
+
+let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, Type_check.mk_tannot env typ effect))
+let annot_exp e_aux l env typ = annot_exp_effect e_aux l env typ no_effect
+let id_typ id = mk_typ (Typ_id (mk_id id))
+
+let analyse_instruction state ast =
+ let env = (snd state).typecheck_env in
+ let unk = Parse_ast.Unknown in
+ let typed = annot_exp
+ (E_app (mk_id "initial_analysis", [annot_exp (E_internal_value ast) unk env (id_typ "ast")])) unk env
+ (tuple_typ [id_typ "regfps"; id_typ "regfps"; id_typ "regfps"; id_typ "niafps"; id_typ "diafp"; id_typ "instruction_kind"])
+ in
+ Step (lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp typed)), state, return typed, [])
+
+let execute_instruction state ast =
+ let env = (snd state).typecheck_env in
+ let unk = Parse_ast.Unknown in
+ let typed = annot_exp
+ (E_app (mk_id "execute", [annot_exp (E_internal_value ast) unk env (id_typ "ast")])) unk env unit_typ
+ in
+ Step (lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp typed)), state, return typed, [])
diff --git a/src/isail.ml b/src/isail.ml
index cce56fb0..094ad3df 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -108,7 +108,7 @@ let sail_logo =
let vs_ids = ref (val_spec_ids !Interactive.ast)
-let interactive_state = ref (initial_state !Interactive.ast Value.primops)
+let interactive_state = ref (initial_state !Interactive.ast !Interactive.env Value.primops)
let interactive_bytecode = ref []
@@ -117,7 +117,9 @@ let sep = "-----------------------------------------------------" |> Util.blue |
let print_program () =
match !current_mode with
| Normal | Emacs -> ()
- | Evaluation (Step (out, _, _, stack)) ->
+ | Evaluation (Step (out, _, _, stack))
+ | Evaluation (Effect_request(out, _, stack, _))
+ | Evaluation (Fail (out, _, _, stack, _)) ->
List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline (Lazy.force code); print_endline sep);
print_endline (Lazy.force out)
| Evaluation (Done (_, v)) ->
@@ -134,6 +136,9 @@ let rec run () =
interactive_state := state;
print_endline ("Result = " ^ Value.string_of_value v);
current_mode := Normal
+ | Fail (_, _, _, _, msg) ->
+ print_endline ("Error: " ^ msg);
+ current_mode := Normal
| Step (out, state, _, stack) ->
begin
try
@@ -145,6 +150,14 @@ let rec run () =
| Break frame ->
print_endline "Breakpoint";
current_mode := Evaluation frame
+ | Effect_request (out, state, stack, eff) ->
+ begin
+ try
+ current_mode := Evaluation (Interpreter.default_effect_interp state eff)
+ with
+ | Failure str -> print_endline str; current_mode := Normal
+ end;
+ run ()
end
let rec run_steps n =
@@ -158,6 +171,9 @@ let rec run_steps n =
interactive_state := state;
print_endline ("Result = " ^ Value.string_of_value v);
current_mode := Normal
+ | Fail (_, _, _, _, msg) ->
+ print_endline ("Error: " ^ msg);
+ current_mode := Normal
| Step (out, state, _, stack) ->
begin
try
@@ -169,6 +185,14 @@ let rec run_steps n =
| Break frame ->
print_endline "Breakpoint";
current_mode := Evaluation frame
+ | Effect_request (out, state, stack, eff) ->
+ begin
+ try
+ current_mode := Evaluation (Interpreter.default_effect_interp state eff)
+ with
+ | Failure str -> print_endline str; current_mode := Normal
+ end;
+ run_steps (n - 1)
end
let help =
@@ -208,7 +232,9 @@ let help =
(color yellow "<command>") (color green ":help :type")
| ":elf" ->
sprintf ":elf %s - Load an ELF file."
- (color yellow "<file>")
+ (color yellow "<file>")
+ | ":bin" ->
+ ":bin <address> <file> - Load a binary file at the given address."
| ":r" | ":run" ->
"(:r | :run) - Completely evaluate the currently evaluating expression."
| ":s" | ":step" ->
@@ -402,7 +428,7 @@ let handle_input' input =
let ast, env = Specialize.(specialize' 1 int_specialization !Interactive.ast !Interactive.env) in
Interactive.ast := ast;
Interactive.env := env;
- interactive_state := initial_state !Interactive.ast Value.primops
+ interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops
| ":pretty" ->
print_endline (Pretty_print_sail.to_string (Latex.defs !Interactive.ast))
| ":ir" ->
@@ -441,13 +467,23 @@ let handle_input' input =
let files = Util.split_on_char ' ' arg in
let (_, ast, env) = load_files !Interactive.env files in
Interactive.ast := append_ast !Interactive.ast ast;
- interactive_state := initial_state !Interactive.ast Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
Interactive.env := env;
vs_ids := val_spec_ids !Interactive.ast
+ | ":bin" ->
+ begin
+ let args = Util.split_on_char ' ' arg in
+ match args with
+ | [addr_s; filename] ->
+ let addr = Big_int.of_string addr_s in
+ Elf_loader.load_binary addr filename
+ | _ ->
+ print_endline "Invalid argument for :bin, expected <addr> <filename>"
+ end
| ":u" | ":unload" ->
Interactive.ast := Ast.Defs [];
Interactive.env := Type_check.initial_env;
- interactive_state := initial_state !Interactive.ast Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
vs_ids := val_spec_ids !Interactive.ast;
(* See initial_check.mli for an explanation of why we need this. *)
Initial_check.have_undefined_builtins := false;
@@ -469,7 +505,7 @@ let handle_input' input =
let ast, env = Type_check.check !Interactive.env (Defs [DEF_val (mk_letbind (mk_pat (P_id (mk_id v))) exp)]) in
Interactive.ast := append_ast !Interactive.ast ast;
Interactive.env := env;
- interactive_state := initial_state !Interactive.ast Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
| _ -> print_endline "Invalid arguments for :let"
end
| ":def" ->
@@ -477,7 +513,7 @@ let handle_input' input =
let ast, env = Type_check.check !Interactive.env ast in
Interactive.ast := append_ast !Interactive.ast ast;
Interactive.env := env;
- interactive_state := initial_state !Interactive.ast Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
| ":graph" ->
let format = if arg = "" then "svg" else arg in
let dotfile, out_chan = Filename.open_temp_file "sail_graph_" ".gz" in
@@ -538,17 +574,17 @@ let handle_input' input =
end
| ":rewrites" ->
Interactive.ast := Process_file.rewrite_ast_target arg !Interactive.env !Interactive.ast;
- interactive_state := initial_state !Interactive.ast Value.primops
+ interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops
| ":prover_regstate" ->
let env, ast = prover_regstate (Some arg) !Interactive.ast !Interactive.env in
Interactive.env := env;
Interactive.ast := ast;
- interactive_state := initial_state !Interactive.ast Value.primops
+ interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops
| ":recheck" ->
let ast, env = Type_check.check Type_check.initial_env !Interactive.ast in
Interactive.env := env;
Interactive.ast := ast;
- interactive_state := initial_state !Interactive.ast Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
vs_ids := val_spec_ids !Interactive.ast
| ":compile" ->
let out_name = match !opt_file_out with
@@ -577,7 +613,7 @@ let handle_input' input =
load_into_session arg;
let (_, ast, env) = load_files ~check:true !Interactive.env [arg] in
Interactive.ast := append_ast !Interactive.ast ast;
- interactive_state := initial_state !Interactive.ast Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
Interactive.env := env;
vs_ids := val_spec_ids !Interactive.ast;
print_endline ("(message \"Checked " ^ arg ^ " done\")\n");
@@ -588,7 +624,7 @@ let handle_input' input =
| ":unload" ->
Interactive.ast := Ast.Defs [];
Interactive.env := Type_check.initial_env;
- interactive_state := initial_state !Interactive.ast Value.primops;
+ interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
vs_ids := val_spec_ids !Interactive.ast;
Initial_check.have_undefined_builtins := false;
Process_file.clear_symbols ()
@@ -644,6 +680,9 @@ let handle_input' input =
interactive_state := state;
print_endline ("Result = " ^ Value.string_of_value v);
current_mode := Normal
+ | Fail (_, _, _, _, msg) ->
+ print_endline ("Error: " ^ msg);
+ current_mode := Normal
| Step (out, state, _, stack) ->
begin
try
@@ -656,6 +695,15 @@ let handle_input' input =
| Break frame ->
print_endline "Breakpoint";
current_mode := Evaluation frame
+ | Effect_request (out, state, stack, eff) ->
+ begin
+ try
+ interactive_state := state;
+ current_mode := Evaluation (Interpreter.default_effect_interp state eff);
+ print_program ()
+ with
+ | Failure str -> print_endline str; current_mode := Normal
+ end
end
end
diff --git a/src/libsail.mllib b/src/libsail.mllib
new file mode 100644
index 00000000..734a1381
--- /dev/null
+++ b/src/libsail.mllib
@@ -0,0 +1,60 @@
+Anf
+Ast
+Ast_util
+Bitfield
+Bytecode
+C_backend
+Cgen_backend
+Constant_fold
+Constraint
+Elf_loader
+Error_format
+Graph
+Initial_check
+Interactive
+Interpreter
+Isail
+Jib
+Jib_compile
+Jib_optimize
+Jib_ssa
+Jib_util
+Latex
+Lexer
+Manifest
+Monomorphise
+Nl_flow
+Ocaml_backend
+Optimize
+Parse_ast
+Parser
+Pattern_completeness
+PPrint
+PPrintCombinators
+PPrintEngine
+PPrintRenderer
+PPrintOCaml
+Pretty_print
+Pretty_print_common
+Pretty_print_coq
+Pretty_print_lem
+Pretty_print_sail
+Process_file
+Profile
+Reporting
+Rewriter
+Rewrites
+Sail
+Sail2_values
+Sail_lib
+Scattered
+Share_directory
+Spec_analysis
+Specialize
+State
+ToFromInterp_backend
+ToFromInterp_lib
+Type_check
+Type_error
+Util
+Value
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 4d7119d7..6c82fc72 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3383,9 +3383,8 @@ let add_bitvector_casts (Defs defs) =
let bitsn = vector_typ (nvar kid) dec_ord bit_typ in
let ts = mk_typschm (mk_typquant [mk_qi_id K_int kid])
(function_typ [bitsn] bitsn no_effect) in
- let extfn _ = Some "zeroExtend" in
let mkfn name =
- mk_val_spec (VS_val_spec (ts,name,extfn,false))
+ mk_val_spec (VS_val_spec (ts,name,[("_", "zeroExtend")],false))
in
let defs = List.map mkfn (IdSet.elements !specs_required) in
check Env.empty (Defs defs)
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index c68a258d..cc1afaac 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -466,8 +466,8 @@ let ocaml_funcls ctx =
| exception Not_found -> failwith ("No val spec found for " ^ string_of_id id)
in
(* Any remaining type variables after simple_typ rewrite should
- ind icate Type-polymorphism. If we have it, we need to generate
- explic it type signatures with universal quantification. *)
+ indicate Type-polymorphism. If we have it, we need to generate
+ explicit type signatures with universal quantification. *)
let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
let pat_sym = gensym () in
let pat, exp =
@@ -625,8 +625,8 @@ let ocaml_typedef ctx (TD_aux (td_aux, (l, _))) =
Reporting.unreachable l __POS__ "Bitfield should be re-written"
let get_externs (Defs defs) =
- let extern_id (VS_aux (VS_val_spec (typschm, id, ext, _), _)) =
- match ext "ocaml" with
+ let extern_id (VS_aux (VS_val_spec (typschm, id, exts, _), _)) =
+ match Ast_util.extern_assoc "ocaml" exts with
| None -> []
| Some ext -> [(id, mk_id ext)]
in
@@ -991,6 +991,8 @@ let ocaml_compile spec defs generator_types =
let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/elf_loader.ml .") in
let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/sail_lib.ml .") in
let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/util.ml .") in
+ let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/value.ml .") in
+ let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/toFromInterp_lib.ml .") in
let tags_file = if !opt_ocaml_coverage then "_tags_coverage" else "_tags" in
let _ = Unix.system ("cp -r " ^ sail_dir ^ "/lib/" ^ tags_file ^ " _tags") in
let out_chan = open_out (spec ^ ".ml") in
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 818c9340..fcf921b7 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -443,7 +443,7 @@ type_def_aux = (* Type definition body *)
type
val_spec_aux = (* Value type specification *)
- VS_val_spec of typschm * id * (string -> string option) * bool
+ VS_val_spec of typschm * id * (string * string) list * bool
type
dec_spec_aux = (* Register declarations *)
diff --git a/src/parser.mly b/src/parser.mly
index 39ca75ff..1c7d1580 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1341,31 +1341,31 @@ let_def:
externs:
| id Colon String
- { ([(string_of_id $1, $3)], None) }
+ { [(string_of_id $1, $3)] }
| Under Colon String
- { ([], Some $3) }
+ { [("_", $3)] }
| id Colon String Comma externs
- { cons_fst (string_of_id $1, $3) $5 }
+ { (string_of_id $1, $3) :: $5 }
val_spec_def:
| Doc val_spec_def
{ doc_vs $1 $2 }
| Val id Colon typschm
- { mk_vs (VS_val_spec ($4, $2, (fun _ -> None), false)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($4, $2, [], false)) $startpos $endpos }
| Val Cast id Colon typschm
- { mk_vs (VS_val_spec ($5, $3, (fun _ -> None), true)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($5, $3, [], true)) $startpos $endpos }
| Val id Eq String Colon typschm
- { mk_vs (VS_val_spec ($6, $2, (fun _ -> Some $4), false)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($6, $2, [("_", $4)], false)) $startpos $endpos }
| Val Cast id Eq String Colon typschm
- { mk_vs (VS_val_spec ($7, $3, (fun _ -> Some $5), true)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($7, $3, [("_", $5)], true)) $startpos $endpos }
| Val String Colon typschm
- { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), (fun _ -> Some $2), false)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), [("_", $2)], false)) $startpos $endpos }
| Val Cast String Colon typschm
- { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), (fun _ -> Some $3), true)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), [("_", $3)], true)) $startpos $endpos }
| Val id Eq Lcurly externs Rcurly Colon typschm
- { mk_vs (VS_val_spec ($8, $2, (fun backend -> (assoc_opt backend $5)), false)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($8, $2, $5, false)) $startpos $endpos }
| Val Cast id Eq Lcurly externs Rcurly Colon typschm
- { mk_vs (VS_val_spec ($9, $3, (fun backend -> (assoc_opt backend $6)), true)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($9, $3, $6, true)) $startpos $endpos }
register_def:
| Register id Colon typ
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index b4f32dce..d80dabe9 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -2940,8 +2940,8 @@ let find_unimplemented defs =
IdSet.remove id unimplemented
in
let adjust_def unimplemented = function
- | DEF_spec (VS_aux (VS_val_spec (_,id,ext,_),_)) -> begin
- match ext "coq" with
+ | DEF_spec (VS_aux (VS_val_spec (_,id,exts,_),_)) -> begin
+ match Ast_util.extern_assoc "coq" exts with
| Some _ -> unimplemented
| None -> IdSet.add id unimplemented
end
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 6479a028..633d910e 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1408,7 +1408,7 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
let doc_spec_lem env (VS_aux (valspec,annot)) =
match valspec with
- | VS_val_spec (typschm,id,ext,_) when ext "lem" = None ->
+ | VS_val_spec (typschm,id,exts,_) when Ast_util.extern_assoc "lem" exts = None ->
(* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in
if contains_t_pp_var typ then empty else *)
doc_docstring_lem annot ^^
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 7f3a2b63..aa7294bd 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -470,7 +470,7 @@ and doc_atomic_exp (E_aux (e_aux, _) as exp) =
brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; equals; doc_exp exp3])
| E_vector_update_subrange (exp1, exp2, exp3, exp4) ->
brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4])
- | E_internal_value v -> string (Value.string_of_value v |> Util.green |> Util.clear)
+ | E_internal_value v -> string (Value.string_of_value v (* |> Util.green |> Util.clear *))
| _ -> parens (doc_exp exp)
and doc_fexps fexps =
separate_map (comma ^^ space) doc_fexp fexps
@@ -623,9 +623,7 @@ let doc_typdef (TD_aux(td,_)) = match td with
let doc_spec ?comment:(comment=false) (VS_aux (v, annot)) =
let doc_extern ext =
- let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^
- utf8string ("\"" ^ String.escaped id ^ "\"")) (ext b) in
- let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"; "smt"; "interpreter"; "c"]) in
+ let docs = List.map (fun (backend, rep) -> string (backend ^ ":") ^^ space ^^ utf8string ("\"" ^ String.escaped rep ^ "\"")) ext in
if docs = [] then empty else equals ^^ space ^^ braces (separate (comma ^^ space) docs)
in
match v with
diff --git a/src/rewrites.ml b/src/rewrites.ml
index e148cee4..0107cf62 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1772,7 +1772,7 @@ let rewrite_split_fun_ctor_pats fun_name env (Defs defs) =
in
let val_spec =
VS_aux (VS_val_spec
- (mk_typschm (mk_typquant quants) fun_typ, id, (fun _ -> None), false),
+ (mk_typschm (mk_typquant quants) fun_typ, id, [], false),
(Parse_ast.Unknown, empty_tannot))
in
let fundef = FD_aux (FD_function (r_o, t_o, e_o, funcls), fdannot) in
@@ -2718,7 +2718,7 @@ let construct_toplevel_string_append_func env f_id pat =
), unk)]
in
let fun_typ = (mk_typ (Typ_fn ([string_typ], option_typ, no_effect))) in
- let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, (fun _ -> None), false), unkt) in
+ let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, [], false), unkt) in
let new_val_spec, env = Type_check.check_val_spec env new_val_spec in
let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in
@@ -3971,10 +3971,10 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), l) in
let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), l) in
- let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
- let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
- let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
- let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+ let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, [], false), (Parse_ast.Unknown,())) in
+ let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, [], false), (Parse_ast.Unknown,())) in
+ let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, [], false), (Parse_ast.Unknown,())) in
+ let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, [], false), (Parse_ast.Unknown,())) in
let forwards_spec, env = Type_check.check_val_spec env forwards_spec in
let backwards_spec, env = Type_check.check_val_spec env backwards_spec in
@@ -4008,7 +4008,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
let string_defs =
begin if subtype_check env typ1 string_typ && subtype_check env string_typ typ1 then
let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
- let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+ let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in
let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in
let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
@@ -4018,7 +4018,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
else
if subtype_check env typ2 string_typ && subtype_check env string_typ typ2 then
let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
- let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+ let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in
let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in
let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
@@ -4926,6 +4926,8 @@ let rewrites_target tgt =
| "sail" -> []
| "latex" -> []
| "interpreter" -> rewrites_interpreter
+ | "tofrominterp" -> rewrites_interpreter
+ | "marshal" -> rewrites_interpreter
| _ ->
raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Invalid target for rewriting: " ^ tgt))
diff --git a/src/sail.ml b/src/sail.ml
index 9c3a3d5c..a0fc2e75 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -57,6 +57,7 @@ let opt_file_out : string option ref = ref None
let opt_interactive_script : string option ref = ref None
let opt_print_version = ref false
let opt_target = ref None
+let opt_tofrominterp_output_dir : string option ref = ref None
let opt_memo_z3 = ref false
let opt_sanity = ref false
let opt_includes_c = ref ([]:string list)
@@ -88,6 +89,15 @@ let options = Arg.align ([
( "-no_warn",
Arg.Clear Util.opt_warnings,
" do not print warnings");
+ ( "-tofrominterp",
+ set_target "tofrominterp",
+ " output OCaml functions to translate between shallow embedding and interpreter");
+ ( "-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_output_dir",
+ Arg.String (fun dir -> opt_tofrominterp_output_dir := Some dir),
+ " set a custom directory to output embedding translation OCaml");
( "-ocaml",
Arg.Tuple [set_target "ocaml"; Arg.Set Initial_check.opt_undefined_gen],
" output an OCaml translated version of the input");
@@ -121,6 +131,9 @@ let options = Arg.align ([
( "-latex_full_valspecs",
Arg.Clear Latex.opt_simple_val,
" print full valspecs in LaTeX output");
+ ( "-marshal",
+ Arg.Tuple [set_target "marshal"; Arg.Set Initial_check.opt_undefined_gen],
+ " OCaml-marshal out the rewritten AST to a file");
( "-ir",
set_target "ir",
" print intermediate representation");
@@ -379,6 +392,24 @@ let target name out_name ast type_envs =
let out = match !opt_file_out with None -> "out" | Some s -> s in
Ocaml_backend.ocaml_compile out ast ocaml_generator_info
+ | Some "tofrominterp" ->
+ let out = match !opt_file_out with None -> "out" | Some s -> s in
+ ToFromInterp_backend.tofrominterp_output !opt_tofrominterp_output_dir out ast
+
+ | Some "marshal" ->
+ let out_filename = match !opt_file_out with None -> "out" | Some s -> s in
+ let f = open_out_bin (out_filename ^ ".defs") in
+ let remove_prover (l, tannot) =
+ if Type_check.is_empty_tannot tannot then
+ (l, Type_check.empty_tannot)
+ else
+ (l, Type_check.replace_env (Type_check.Env.set_prover None (Type_check.env_of_tannot tannot)) tannot)
+ in
+ Marshal.to_string (Ast_util.map_defs_annot remove_prover ast, Type_check.Env.set_prover None type_envs) [Marshal.Compat_32]
+ |> B64.encode
+ |> output_string f;
+ close_out f
+
| Some "c" ->
let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in
let ast_c, type_envs =
diff --git a/src/specialize.ml b/src/specialize.ml
index ca33ee85..607084c8 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -62,7 +62,7 @@ let is_typ_ord_arg = function
type specialization = {
is_polymorphic : kinded_id -> bool;
instantiation_filter : kid -> typ_arg -> bool;
- extern_filter : (string -> string option) -> bool
+ extern_filter : (string * string) list -> bool
}
let typ_ord_specialization = {
@@ -74,7 +74,7 @@ let typ_ord_specialization = {
let int_specialization = {
is_polymorphic = is_int_kopt;
instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false);
- extern_filter = (fun externs -> match externs "c" with Some _ -> true | None -> false)
+ extern_filter = (fun externs -> match Ast_util.extern_assoc "c" externs with Some _ -> true | None -> false)
}
let int_specialization_with_externs = {
diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml
new file mode 100644
index 00000000..d65aaf3b
--- /dev/null
+++ b/src/toFromInterp_backend.ml
@@ -0,0 +1,361 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* All rights reserved. *)
+(* *)
+(* This software was developed by the University of Cambridge Computer *)
+(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
+(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in *)
+(* the documentation and/or other materials provided with the *)
+(* distribution. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
+(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
+(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
+(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
+(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
+(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
+(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
+(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
+(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
+(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
+(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
+(* SUCH DAMAGE. *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open PPrint
+open Type_check
+open Util
+open Pretty_print_common
+open Ocaml_backend
+
+let lem_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 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))])
+ | _ -> brackets (string "v0")
+ in
+ let fromValueKid (Kid_aux ((Var name), _)) =
+ string ("typq_" ^ name)
+ in
+ let fromValueNexp ((Nexp_aux (nexp_aux, annot)) as nexp) = match nexp_aux with
+ | Nexp_constant num -> parens (separate space [string "Big_int.of_string"; dquotes (string (Nat_big_num.to_string num))])
+ | Nexp_var var -> fromValueKid var
+ | Nexp_id id -> string (string_of_id id ^ "FromInterpValue")
+ | _ -> string ("NEXP(" ^ string_of_nexp nexp ^ ")")
+ in
+ let rec fromValueTypArg (A_aux (a_aux, _)) = match a_aux with
+ | A_typ typ -> fromValueTyp typ ""
+ | A_nexp nexp -> fromValueNexp nexp
+ | A_order order -> string ("Order_" ^ (string_of_order order))
+ | _ -> string "TYP_ARG"
+ 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]))
+ | 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]))
+ | 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\"")
+ 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))
+ | _ -> fromValueTyp typ "v0"
+ in
+ let fromValueTypq (QI_aux (qi_aux, _)) = match qi_aux with
+ | QI_id (KOpt_aux (KOpt_kind (K_aux (kind_aux, _), kid), _)) -> fromValueKid kid
+ | QI_const _ -> empty
+ in
+ let fromValueTypqs (TypQ_aux (typq_aux, _)) = match typq_aux with
+ | TypQ_no_forall -> [empty]
+ | TypQ_tq quants -> List.map fromValueTypq quants
+ in
+ match td_aux with
+ | TD_variant (id, typq, arms, _) ->
+ begin match id with
+ | Id_aux ((Id "read_kind"),_) -> empty
+ | Id_aux ((Id "write_kind"),_) -> empty
+ | 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 "regfps"),_) -> empty
+ | Id_aux ((Id "niafp"),_) -> empty
+ | Id_aux ((Id "niafps"),_) -> empty
+ | Id_aux ((Id "diafp"),_) -> empty
+ | Id_aux ((Id "diafps"),_) -> empty
+ (* | Id_aux ((Id "option"),_) -> empty *)
+ | Id_aux ((Id id_string), _)
+ | Id_aux ((Operator id_string), _) ->
+ if !lem_mode && id_string = "option" then empty else
+ let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in
+ let fromFallback = separate space [pipe; underscore; arrow; string "failwith";
+ dquotes (string ("invalid interpreter value for " ^ (string_of_id id)))] in
+ let fromInterpValue =
+ prefix 2 1
+ (separate space [string "let"; fromInterpValueName; separate space (fromValueTypqs typq @ [string "v"]); equals; string "match v with"])
+ ((separate_map hardline
+ (fun (Tu_aux (Tu_ty_id (typ, ctor_id), _)) ->
+ separate space
+ [pipe; string "V_ctor"; parens (concat [dquotes (string (string_of_id ctor_id)); comma_sp;
+ fromValueArgs typ
+ ]);
+ arrow; string (maybe_zencode_upper (string_of_id ctor_id)); fromValueVals typ
+ ]
+ )
+ arms)
+ ^^ hardline ^^ fromFallback)
+ in
+ fromInterpValue ^^ (twice hardline)
+ end
+ | TD_abbrev (Id_aux (Id "regfps", _), _, _) -> empty
+ | TD_abbrev (Id_aux (Id "niafps", _), _, _) -> 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
+ 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))]
+ | _ -> empty
+ end
+ | _ -> empty
+ in
+ let fromInterpValue =
+ (separate space [string "let"; fromInterpValueName; separate space (fromValueTypqs typq); fromInterpValspec; equals; fromValueTypArg typ_arg])
+ in
+ fromInterpValue ^^ (twice hardline)
+ end
+ | TD_enum (Id_aux (Id "read_kind", _), _, _) -> empty
+ | TD_enum (Id_aux (Id "write_kind", _), _, _) -> empty
+ | TD_enum (Id_aux (Id "barrier_kind", _), _, _) -> empty
+ | TD_enum (Id_aux (Id "trans_kind", _), _, _) -> empty
+ | TD_enum (Id_aux (Id "cache_op_kind", _), _, _) -> empty
+ | TD_enum (id, ids, _) ->
+ let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in
+ let fromFallback = separate space [pipe; underscore; arrow; string "failwith";
+ dquotes (string ("invalid interpreter value for " ^ (string_of_id id)))] in
+ let fromInterpValue =
+ prefix 2 1
+ (separate space [string "let"; fromInterpValueName; string "v"; equals; string "match v with"])
+ ((separate_map hardline
+ (fun id ->
+ separate space
+ [pipe; string "V_ctor"; parens (concat [dquotes (string (string_of_id id)); comma_sp; string "[]"]);
+ arrow; string (maybe_zencode_upper (string_of_id id))]
+ )
+ ids)
+ ^^ hardline ^^ fromFallback)
+ in
+ fromInterpValue ^^ (twice hardline)
+ | TD_record (record_id, typq, fields, _) ->
+ let fromInterpField (typ, id) =
+ separate space [string (maybe_zencode ((if !lem_mode then string_of_id record_id ^ "_" else "") ^ string_of_id id)); equals; fromValueTyp typ ("(StringMap.find \"" ^ (string_of_id id) ^ "\" fs)")]
+ in
+ let fromInterpValueName = concat [string (maybe_zencode (string_of_id record_id)); string "FromInterpValue"] in
+ let fromFallback = separate space [pipe; underscore; arrow; string "failwith";
+ dquotes (string ("invalid interpreter value for " ^ (string_of_id record_id)))] in
+ let fromInterpValue =
+ prefix 2 1
+ (separate space [string "let"; fromInterpValueName; separate space (fromValueTypqs typq @ [string "v"]); equals; string "match v with"])
+ ((separate space [pipe; string "V_record fs"; arrow; braces (separate_map (semi ^^ space) fromInterpField fields)])
+ ^^ hardline ^^ fromFallback)
+ in
+ fromInterpValue ^^ (twice hardline)
+ | _ -> empty
+
+let tointerp_typedef (TD_aux (td_aux, (l, _))) =
+ let toValueArgs (Typ_aux (typ_aux, _)) = match typ_aux with
+ | Typ_tup typs -> parens (separate comma_sp (List.mapi (fun i _ -> string ("v" ^ (string_of_int i))) typs))
+ | _ -> parens (string "v0")
+ in
+ let toValueKid (Kid_aux ((Var name), _)) =
+ string ("typq_" ^ name)
+ in
+ let toValueNexp ((Nexp_aux (nexp_aux, _)) as nexp) = match nexp_aux with
+ | Nexp_constant num -> parens (separate space [string "Big_int.of_string"; dquotes (string (Nat_big_num.to_string num))])
+ | Nexp_var var -> toValueKid var
+ | Nexp_id id -> string (string_of_id id ^ "ToInterpValue")
+ | _ -> string ("NEXP(" ^ string_of_nexp nexp ^ ")")
+ in
+ let rec toValueTypArg (A_aux (a_aux, _)) = match a_aux with
+ | A_typ typ -> toValueTyp typ ""
+ | A_nexp nexp -> toValueNexp nexp
+ | A_order order -> string ("Order_" ^ (string_of_order order))
+ | _ -> string "TYP_ARG"
+ 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]))
+ | 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]))
+ | Typ_var kid -> parens (separate space [toValueKid kid; string arg_name])
+ | _ -> parens (string "failwith \"toValueTyp: type arm unimplemented\"")
+ 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))])
+ | _ -> brackets (toValueTyp typ "v0")
+ in
+ let toValueTypq (QI_aux (qi_aux, _)) = match qi_aux with
+ | QI_id (KOpt_aux (KOpt_kind (K_aux (kind_aux, _), kid), _)) -> toValueKid kid
+ | QI_const _ -> empty
+ in
+ let toValueTypqs (TypQ_aux (typq_aux, _)) = match typq_aux with
+ | TypQ_no_forall -> [empty]
+ | TypQ_tq quants -> List.map toValueTypq quants
+ in
+ match td_aux with
+ | TD_variant (id, typq, arms, _) ->
+ begin match id with
+ | Id_aux ((Id "read_kind"),_) -> empty
+ | Id_aux ((Id "write_kind"),_) -> empty
+ | 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 "regfps"),_) -> empty
+ | Id_aux ((Id "niafp"),_) -> empty
+ | Id_aux ((Id "niafps"),_) -> empty
+ | Id_aux ((Id "diafp"),_) -> empty
+ | Id_aux ((Id "diafps"),_) -> empty
+ (* | Id_aux ((Id "option"),_) -> empty *)
+ | Id_aux ((Id id_string), _)
+ | Id_aux ((Operator id_string), _) ->
+ if !lem_mode && id_string = "option" then empty else
+ let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in
+ let toInterpValue =
+ prefix 2 1
+ (separate space [string "let"; toInterpValueName; separate space (toValueTypqs typq @ [string "v"]); equals; string "match v with"])
+ ((separate_map hardline
+ (fun (Tu_aux (Tu_ty_id (typ, ctor_id), _)) ->
+ separate space
+ [pipe; string (maybe_zencode_upper (string_of_id ctor_id)); toValueArgs typ;
+ arrow; string "V_ctor"; parens (concat [dquotes (string (string_of_id ctor_id)); comma_sp; toValueVals typ])
+ ]
+ )
+ arms))
+ in
+ toInterpValue ^^ (twice hardline)
+ end
+ | TD_abbrev (Id_aux (Id "regfps", _), _, _) -> empty
+ | TD_abbrev (Id_aux (Id "niafps", _), _, _) -> 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
+ 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"]
+ | _ -> empty
+ end
+ | _ -> empty
+ in
+ let toInterpValue =
+ (separate space [string "let"; toInterpValueName; separate space (toValueTypqs typq); toInterpValspec; equals; toValueTypArg typ_arg])
+ in
+ toInterpValue ^^ (twice hardline)
+ end
+ | TD_enum (Id_aux (Id "read_kind", _), _, _) -> empty
+ | TD_enum (Id_aux (Id "write_kind", _), _, _) -> empty
+ | TD_enum (Id_aux (Id "barrier_kind", _), _, _) -> empty
+ | TD_enum (Id_aux (Id "trans_kind", _), _, _) -> empty
+ | TD_enum (Id_aux (Id "cache_op_kind", _), _, _) -> empty
+ | TD_enum (id, ids, _) ->
+ let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in
+ let toInterpValue =
+ prefix 2 1
+ (separate space [string "let"; toInterpValueName; string "v"; equals; string "match v with"])
+ ((separate_map hardline
+ (fun id ->
+ separate space
+ [pipe; string (maybe_zencode_upper (string_of_id id));
+ arrow; string "V_ctor"; parens (concat [dquotes (string (string_of_id id)); comma_sp; string "[]"])]
+ )
+ ids))
+ in
+ toInterpValue ^^ (twice hardline)
+ | TD_record (record_id, typq, fields, _) ->
+ let toInterpField (typ, id) =
+ parens (separate comma_sp [dquotes (string (string_of_id id)); toValueTyp typ ("r." ^ (maybe_zencode ((if !lem_mode then string_of_id record_id ^ "_" else "") ^ string_of_id id)))])
+ in
+ let toInterpValueName = concat [string (maybe_zencode (string_of_id record_id)); string "ToInterpValue"] in
+ let toInterpValue =
+ prefix 2 1
+ (separate space [string "let"; toInterpValueName; separate space (toValueTypqs typq @ [string "r"]); equals])
+ (separate space [string "V_record"; parens (separate space [string "List.fold_left (fun m (k, v) -> StringMap.add k v m) StringMap.empty"; (brackets (separate_map (semi ^^ space) toInterpField fields))])])
+ in
+ toInterpValue ^^ (twice hardline)
+ | _ -> empty
+
+
+let tofrominterp_def def = match def with
+ | DEF_type td -> group (frominterp_typedef td ^^ twice hardline ^^ tointerp_typedef td ^^ twice hardline)
+ | _ -> empty
+
+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)
+ ^^ concat (List.map tofrominterp_def defs)
+
+let tofrominterp_pp_defs name f defs =
+ ToChannel.pretty 1. 80 f (tofrominterp_defs name defs)
+
+let tofrominterp_output maybe_dir name defs =
+ let dir = match maybe_dir with Some dir -> dir | None -> "." in
+ let out_chan = open_out (Filename.concat dir (name ^ "_toFromInterp2.ml")) in
+ tofrominterp_pp_defs name out_chan defs;
+ close_out out_chan
diff --git a/src/toFromInterp_lib.ml b/src/toFromInterp_lib.ml
new file mode 100644
index 00000000..c29fcd84
--- /dev/null
+++ b/src/toFromInterp_lib.ml
@@ -0,0 +1,126 @@
+(************************************************************)
+(* Support for toFromInterp *)
+(************************************************************)
+
+open Sail_lib;;
+open Value;;
+
+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 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 -> b
+ | _ -> failwith "invalid interpreter value for bit"
+
+let zbitToInterpValue v = V_bit v
+
+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 typq_'n 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 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/type_check.ml b/src/type_check.ml
index d5d42316..b6aabdc7 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -117,11 +117,10 @@ type env =
shadow_vars : int KBindings.t;
typ_synonyms : (typquant * typ_arg) Bindings.t;
overloads : (id list) Bindings.t;
- flow : (typ -> typ) Bindings.t;
enums : IdSet.t Bindings.t;
records : (typquant * (typ * id) list) Bindings.t;
accessors : (typquant * typ) Bindings.t;
- externs : (string -> string option) Bindings.t;
+ externs : (string * string) list Bindings.t;
casts : id list;
allow_casts : bool;
allow_bindings : bool;
@@ -129,7 +128,7 @@ type env =
default_order : order option;
ret_typ : typ option;
poly_undefineds : bool;
- prove : env -> n_constraint -> bool;
+ prove : (env -> n_constraint -> bool) option;
allow_unknowns : bool;
}
@@ -422,9 +421,6 @@ module Env : sig
val add_mapping : id -> typquant * typ * typ -> t -> t
val add_union_id : id -> typquant * typ -> t -> t
val get_union_id : id -> t -> typquant * typ
- val add_flow : id -> (typ -> typ) -> t -> t
- val get_flow : id -> t -> typ -> typ
- val remove_flow : id -> t -> t
val is_register : id -> t -> bool
val get_register : id -> t -> effect * effect * typ
val add_register : id -> effect -> effect -> typ -> t -> t
@@ -444,7 +440,7 @@ module Env : sig
val add_overloads : id -> id list -> t -> t
val get_overloads : id -> t -> id list
val is_extern : id -> t -> string -> bool
- val add_extern : id -> (string -> string option) -> t -> t
+ val add_extern : id -> (string * string) list -> t -> t
val get_extern : id -> t -> string -> string
val get_default_order : t -> order
val set_default_order : order_aux -> t -> t
@@ -479,7 +475,7 @@ module Env : sig
which is defined below. To break the circularity this would cause
(as the prove code depends on the environment), we add a
reference to the prover to the initial environment. *)
- val add_prover : (t -> n_constraint -> bool) -> t -> t
+ val set_prover : (t -> n_constraint -> bool) option -> t -> t
(* This must not be exported, initial_env sets up a correct initial
environment. *)
@@ -504,7 +500,6 @@ end = struct
shadow_vars = KBindings.empty;
typ_synonyms = Bindings.empty;
overloads = Bindings.empty;
- flow = Bindings.empty;
enums = Bindings.empty;
records = Bindings.empty;
accessors = Bindings.empty;
@@ -516,11 +511,11 @@ end = struct
default_order = None;
ret_typ = None;
poly_undefineds = false;
- prove = (fun _ _ -> false);
+ prove = None;
allow_unknowns = false;
}
- let add_prover f env = { env with prove = f }
+ let set_prover f env = { env with prove = f }
let allow_unknowns env = env.allow_unknowns
let set_allow_unknowns b env = { env with allow_unknowns = b }
@@ -614,7 +609,7 @@ end = struct
| _, _ -> typ_error env Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
in
let ncs = subst_args kopts args in
- if List.for_all (env.prove env) ncs
+ if (match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false)
then ()
else typ_error env (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
@@ -653,7 +648,7 @@ end = struct
in
fun l env args ->
let typ_arg, ncs = subst_args env l kopts args in
- if List.for_all (env.prove env) ncs
+ if (match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false)
then typ_arg
else typ_error env l ("Could not prove constraints " ^ string_of_list ", " string_of_n_constraint ncs
^ " in type synonym " ^ string_of_typ_arg typ_arg
@@ -1144,17 +1139,6 @@ end = struct
match Bindings.find_opt id env.variants with
| Some (typq, tus) -> typq, tus
| None -> typ_error env (id_loc id) ("union " ^ string_of_id id ^ " not found")
- let get_flow id env =
- try Bindings.find id env.flow with
- | Not_found -> fun typ -> typ
-
- let add_flow id f env =
- typ_print (lazy (adding ^ "flow constraints for " ^ string_of_id id));
- { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow }
-
- let remove_flow id env =
- typ_print (lazy ("Removing flow constraints for " ^ string_of_id id));
- { env with flow = Bindings.remove id env.flow }
let is_register id env =
Bindings.mem id env.registers
@@ -1164,7 +1148,7 @@ end = struct
| Not_found -> typ_error env (id_loc id) ("No register binding found for " ^ string_of_id id)
let is_extern id env backend =
- try not (Bindings.find id env.externs backend = None) with
+ try not (Ast_util.extern_assoc backend (Bindings.find id env.externs) = None) with
| Not_found -> false
(* Bindings.mem id env.externs *)
@@ -1173,7 +1157,7 @@ end = struct
let get_extern id env backend =
try
- match Bindings.find id env.externs backend with
+ match Ast_util.extern_assoc backend (Bindings.find id env.externs) with
| Some ext -> ext
| None -> typ_error env (id_loc id) ("No extern binding found for " ^ string_of_id id)
with
@@ -1196,8 +1180,7 @@ end = struct
let lookup_id ?raw:(raw=false) id env =
try
let (mut, typ) = Bindings.find id env.locals in
- let flow = get_flow id env in
- Local (mut, if raw then typ else flow typ)
+ Local (mut, typ)
with
| Not_found ->
try
@@ -2423,6 +2406,14 @@ let env_of_annot (l, tannot) = match tannot with
| Some t -> t.env
| None -> raise (Reporting.err_unreachable l __POS__ "no type annotation")
+let env_of_tannot tannot = match tannot with
+ | Some t -> t.env
+ | None -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "no type annotation")
+
+let typ_of_tannot tannot = match tannot with
+ | Some t -> t.typ
+ | None -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "no type annotation")
+
let env_of (E_aux (_, (l, tannot))) = env_of_annot (l, tannot)
let typ_of_annot (l, tannot) = match tannot with
@@ -3475,7 +3466,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
begin match Env.lookup_id ~raw:true v env with
| Local (Immutable, _) | Enum _ ->
typ_error env l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
- | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, Env.remove_flow v env
+ | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
| Register (_, weff, vtyp) -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ weff, env
| Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
end
@@ -4744,7 +4735,7 @@ let mk_val_spec env typq typ id =
| Typ_aux (Typ_fn (_,_,eff),_) -> eff
| _ -> no_effect
in
- DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, (fun _ -> None), false), (Parse_ast.Unknown, mk_tannot env typ eff)))
+ DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, [], false), (Parse_ast.Unknown, mk_tannot env typ eff)))
let check_tannotopt env typq ret_typ = function
| Typ_annot_opt_aux (Typ_annot_opt_none, _) -> ()
@@ -4864,9 +4855,9 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md
let check_val_spec env (VS_aux (vs, (l, _))) =
let annotate vs typ eff = DEF_spec (VS_aux (vs, (l, mk_tannot env typ eff))) in
let vs, id, typq, typ, env = match vs with
- | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, ext_opt, is_cast) ->
+ | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, exts, is_cast) ->
typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm));
- let env = Env.add_extern id ext_opt env in
+ let env = Env.add_extern id exts env in
let env = if is_cast then Env.add_cast id env else env in
let typq', typ' = expand_bind_synonyms ts_l env (typq, typ) in
(* !opt_expand_valspec controls whether the actual valspec in
@@ -4878,7 +4869,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
else
(typq, typ)
in
- let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in
+ let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, exts, is_cast) in
(vs, id, typq', typ', env)
in
let eff =
@@ -5040,14 +5031,14 @@ and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list
let initial_env =
Env.empty
- |> Env.add_prover (prove __POS__)
- |> Env.add_extern (mk_id "size_itself_int") (fun _ -> Some "size_itself_int")
+ |> Env.set_prover (Some (prove __POS__))
+ |> Env.add_extern (mk_id "size_itself_int") [("_", "size_itself_int")]
|> Env.add_val_spec (mk_id "size_itself_int")
(TypQ_aux (TypQ_tq [QI_aux (QI_id (mk_kopt K_int (mk_kid "n")),
Parse_ast.Unknown)],Parse_ast.Unknown),
function_typ [app_typ (mk_id "itself") [mk_typ_arg (A_nexp (nvar (mk_kid "n")))]]
(atom_typ (nvar (mk_kid "n"))) no_effect)
- |> Env.add_extern (mk_id "make_the_value") (fun _ -> Some "make_the_value")
+ |> Env.add_extern (mk_id "make_the_value") [("_", "make_the_value")]
|> Env.add_val_spec (mk_id "make_the_value")
(TypQ_aux (TypQ_tq [QI_aux (QI_id (mk_kopt K_int (mk_kid "n")),
Parse_ast.Unknown)],Parse_ast.Unknown),
diff --git a/src/type_check.mli b/src/type_check.mli
index 737e714e..2a413238 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -221,6 +221,8 @@ module Env : sig
val builtin_typs : typquant Bindings.t
val get_union_id : id -> t -> typquant * typ
+
+ val set_prover : (t -> n_constraint -> bool) option -> t -> t
end
(** {4 Environment helper functions} *)
@@ -347,9 +349,11 @@ val typ_error : Env.t -> Ast.l -> string -> 'a
val env_of : tannot exp -> Env.t
val env_of_annot : Ast.l * tannot -> Env.t
+val env_of_tannot : tannot -> Env.t
val typ_of : tannot exp -> typ
val typ_of_annot : Ast.l * tannot -> typ
+val typ_of_tannot : tannot -> typ
val typ_of_pat : tannot pat -> typ
val env_of_pat : tannot pat -> Env.t
@@ -424,6 +428,8 @@ val propagate_exp_effect : tannot exp -> tannot exp
val propagate_pexp_effect : tannot pexp -> tannot pexp * effect
+val big_int_of_nexp : nexp -> Big_int.num option
+
(** {2 Checking full ASTs} *)
(** Fully type-check an AST
diff --git a/src/value.ml b/src/value.ml
index d1b945a7..279d3aba 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -302,6 +302,10 @@ let value_or_vec = function
| [v1; v2] -> mk_vector (Sail_lib.or_vec (coerce_bv v1, coerce_bv v2))
| _ -> failwith "value not_vec"
+let value_xor_vec = function
+ | [v1; v2] -> mk_vector (Sail_lib.xor_vec (coerce_bv v1, coerce_bv v2))
+ | _ -> failwith "value xor_vec"
+
let value_uint = function
| [v] -> V_int (Sail_lib.uint (coerce_bv v))
| _ -> failwith "value uint"
@@ -341,6 +345,14 @@ let value_negate = function
| [v1] -> V_int (Sail_lib.negate (coerce_int v1))
| _ -> failwith "value negate"
+let value_pow2 = function
+ | [v1] -> V_int (Sail_lib.pow2 (coerce_int v1))
+ | _ -> failwith "value pow2"
+
+let value_int_power = function
+ | [v1; v2] -> V_int (Sail_lib.int_power (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value int_power"
+
let value_mult = function
| [v1; v2] -> V_int (Sail_lib.mult (coerce_int v1, coerce_int v2))
| _ -> failwith "value mult"
@@ -417,6 +429,14 @@ let value_shiftr = function
| [v1; v2] -> mk_vector (Sail_lib.shiftr (coerce_bv v1, coerce_int v2))
| _ -> failwith "value shiftr"
+let value_shift_bits_left = function
+ | [v1; v2] -> mk_vector (Sail_lib.shift_bits_left (coerce_bv v1, coerce_bv v2))
+ | _ -> failwith "value shift_bits_left"
+
+let value_shift_bits_right = function
+ | [v1; v2] -> mk_vector (Sail_lib.shift_bits_right (coerce_bv v1, coerce_bv v2))
+ | _ -> failwith "value shift_bits_right"
+
let value_vector_truncate = function
| [v1; v2] -> mk_vector (Sail_lib.vector_truncate (coerce_bv v1, coerce_int v2))
| _ -> failwith "value vector_truncate"
@@ -520,6 +540,14 @@ let value_round_down = function
| [v] -> V_int (Sail_lib.round_down (coerce_real v))
| _ -> failwith "value round_down"
+let value_quot_round_zero = function
+ | [v1; v2] -> V_int (Sail_lib.quot_round_zero (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value quot_round_zero"
+
+let value_rem_round_zero = function
+ | [v1; v2] -> V_int (Sail_lib.rem_round_zero (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value rem_round_zero"
+
let value_add_real = function
| [v1; v2] -> V_real (Sail_lib.add_real (coerce_real v1, coerce_real v2))
| _ -> failwith "value add_real"
@@ -564,6 +592,10 @@ let value_string_append = function
| [v1; v2] -> V_string (Sail_lib.string_append (coerce_string v1, coerce_string v2))
| _ -> failwith "value string_append"
+let value_decimal_string_of_bits = function
+ | [v] -> V_string (Sail_lib.decimal_string_of_bits (coerce_bv v))
+ | _ -> failwith "value decimal_string_of_bits"
+
let primops =
List.fold_left
(fun r (x, y) -> StringMap.add x y r)
@@ -578,6 +610,7 @@ let primops =
("putchar", value_putchar);
("string_of_int", fun vs -> V_string (string_of_value (List.hd vs)));
("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs)));
+ ("decimal_string_of_bits", value_decimal_string_of_bits);
("print_bits", value_print_bits);
("print_int", value_print_int);
("print_string", value_print_string);
@@ -610,6 +643,7 @@ let primops =
("not_vec", value_not_vec);
("and_vec", value_and_vec);
("or_vec", value_or_vec);
+ ("xor_vec", value_xor_vec);
("uint", value_uint);
("sint", value_sint);
("get_slice_int", value_get_slice_int);
@@ -621,6 +655,8 @@ let primops =
("zeros", value_zeros);
("shiftr", value_shiftr);
("shiftl", value_shiftl);
+ ("shift_bits_left", value_shift_bits_left);
+ ("shift_bits_right", value_shift_bits_right);
("add_int", value_add_int);
("sub_int", value_sub_int);
("div_int", value_quotient);
@@ -629,6 +665,8 @@ let primops =
("quotient", value_quotient);
("modulus", value_modulus);
("negate", value_negate);
+ ("pow2", value_pow2);
+ ("int_power", value_int_power);
("shr_int", value_shr_int);
("shl_int", value_shl_int);
("max_int", value_max_int);
@@ -656,7 +694,9 @@ let primops =
("mult_real", value_mult_real);
("round_up", value_round_up);
("round_down", value_round_down);
- ("quotient_real", value_div_real);
+ ("quot_round_zero", value_quot_round_zero);
+ ("rem_round_zero", value_rem_round_zero);
+ ("quotient_real", value_quotient_real);
("abs_real", value_abs_real);
("div_real", value_div_real);
("sqrt_real", value_sqrt_real);
@@ -676,4 +716,5 @@ let primops =
("string_length", value_string_length);
("string_startswith", value_string_startswith);
("string_drop", value_string_drop);
+ ("skip", fun _ -> V_unit);
]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 14:00:34 +0000