summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile3
-rw-r--r--src/_tags6
-rw-r--r--src/ast_util.ml9
-rw-r--r--src/ast_util.mli3
-rw-r--r--src/constant_fold.ml20
-rw-r--r--src/elf_loader.ml18
-rw-r--r--src/initial_check.ml12
-rw-r--r--src/interpreter.ml540
-rw-r--r--src/isail.ml51
-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.ml4
-rw-r--r--src/process_file.ml2
-rw-r--r--src/rewrites.ml16
-rw-r--r--src/sail.ml33
-rw-r--r--src/toFromInterp_backend.ml294
-rw-r--r--src/toFromInterp_lib.ml101
-rw-r--r--src/type_check.ml53
-rw-r--r--src/type_check.mli4
-rw-r--r--src/value.ml43
24 files changed, 1060 insertions, 195 deletions
diff --git a/src/Makefile b/src/Makefile
index beba66df..abf49423 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -113,6 +113,9 @@ sail.native: sail
sail.byte: ast.ml bytecode.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 aac18862..fbea6a00 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
<pprint> or <pprint/src>: include
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 158b40a8..548cd15e 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -1714,6 +1714,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 0c42d9d3..bef4a238 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -426,6 +426,9 @@ val locate_typ : (l -> l) -> typ -> typ
a generated number. *)
val unique : l -> l
+
+val extern_assoc : string -> (string * string) list -> string option
+
(** Substitutions *)
(* The function X_subst substitutes a type argument into something of
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 6ad1f663..2c46f38b 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -78,7 +78,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
@@ -126,6 +127,13 @@ let rec run frame =
run (Interpreter.eval_frame frame)
| Interpreter.Break frame ->
run (Interpreter.eval_frame frame)
+ | Interpreter.Effect_request (st, 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
@@ -144,13 +152,13 @@ let rec run frame =
- Throws an exception that isn't caught.
*)
-let rec rewrite_constant_function_calls' ast =
+let rec rewrite_constant_function_calls' env ast =
let rewrite_count = ref 0 in
let ok () = incr rewrite_count in
let not_ok () = decr rewrite_count in
let lstate, gstate =
- Interpreter.initial_state ast safe_primops
+ Interpreter.initial_state ast env safe_primops
in
let gstate = { gstate with Interpreter.allow_registers = false } in
@@ -207,11 +215,11 @@ let rec rewrite_constant_function_calls' ast =
let ast = rewrite_defs_base rw_defs ast in
(* We keep iterating until we have no more re-writes to do *)
if !rewrite_count > 0
- then rewrite_constant_function_calls' ast
+ then rewrite_constant_function_calls' env ast
else ast
-let rewrite_constant_function_calls ast =
+let rewrite_constant_function_calls env ast =
if !optimize_constant_fold then
- rewrite_constant_function_calls' ast
+ rewrite_constant_function_calls' env ast
else
ast
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 5893563b..33844a72 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -808,8 +808,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 val_spec_ids (Defs defs) =
let val_spec_id (VS_aux (vs_aux, _)) =
@@ -884,7 +884,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
@@ -894,7 +894,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)))]]
@@ -942,7 +942,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]]
@@ -978,7 +978,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 1e1bb816..737f937e 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,7 +95,8 @@ 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
@@ -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_memv of 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_memv (v, cont) -> Write_memv (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_memv v : bool monad =
+ Yield (Write_memv (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,47 @@ 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_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_memv" ->
+ begin match evaluated with
+ | [v] ->
+ write_memv (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 -> return (exp_of_value (op (List.map value_of_exp evaluated)))
end
| [] ->
call id (List.map value_of_exp evaluated) >>=
@@ -352,22 +452,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 +485,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 ->
@@ -451,45 +545,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))
@@ -523,7 +623,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))
@@ -532,9 +632,14 @@ 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)
+ | _ -> fail ("Unimplemented " ^ string_of_exp orig_exp)
and combine _ v1 v2 =
match (v1, v2) with
@@ -635,6 +740,61 @@ let rec ast_letbinds (Defs defs) =
| DEF_val lb :: defs -> lb :: ast_letbinds (Defs defs)
| _ :: defs -> ast_letbinds (Defs defs)
+let rk_of_string = function
+ | "Read_plain" -> Sail2_instr_kinds.Read_plain
+ | "Read_reserve" -> Sail2_instr_kinds.Read_reserve
+ | "Read_acquire" -> Sail2_instr_kinds.Read_acquire
+ | "Read_exclusive" -> Sail2_instr_kinds.Read_exclusive
+ | "Read_exclusive_acquire" -> Sail2_instr_kinds.Read_exclusive_acquire
+ | "Read_stream" -> Sail2_instr_kinds.Read_stream
+ | "Read_RISCV_acquire" -> Sail2_instr_kinds.Read_RISCV_acquire
+ | "Read_RISCV_strong_acquire" -> Sail2_instr_kinds.Read_RISCV_strong_acquire
+ | "Read_RISCV_reserved" -> Sail2_instr_kinds.Read_RISCV_reserved
+ | "Read_RISCV_reserved_acquire" -> Sail2_instr_kinds.Read_RISCV_reserved_acquire
+ | "Read_RISCV_reserved_strong_acquire" -> Sail2_instr_kinds.Read_RISCV_reserved_strong_acquire
+ | "Read_X86_locked" -> Sail2_instr_kinds.Read_X86_locked
+ | s -> failwith ("Unknown read kind: " ^ s)
+
+let wk_of_string = function
+ | "Write_plain" -> Sail2_instr_kinds.Write_plain
+ | "Write_conditional" -> Sail2_instr_kinds.Write_conditional
+ | "Write_release" -> Sail2_instr_kinds.Write_release
+ | "Write_exclusive" -> Sail2_instr_kinds.Write_exclusive
+ | "Write_exclusive_release" -> Sail2_instr_kinds.Write_exclusive_release
+ | "Write_RISCV_release" -> Sail2_instr_kinds.Write_RISCV_release
+ | "Write_RISCV_strong_release" -> Sail2_instr_kinds.Write_RISCV_strong_release
+ | "Write_RISCV_conditional" -> Sail2_instr_kinds.Write_RISCV_conditional
+ | "Write_RISCV_conditional_release" -> Sail2_instr_kinds.Write_RISCV_conditional_release
+ | "Write_RISCV_conditional_strong_release" -> Sail2_instr_kinds.Write_RISCV_conditional_strong_release
+ | "Write_X86_locked" -> Sail2_instr_kinds.Write_X86_locked
+ | s -> failwith ("Unknown write kind: " ^ s)
+
+let bk_of_string = function
+ | "Barrier_Sync" -> Sail2_instr_kinds.Barrier_Sync
+ | "Barrier_LwSync" -> Sail2_instr_kinds.Barrier_LwSync
+ | "Barrier_Eieio" -> Sail2_instr_kinds.Barrier_Eieio
+ | "Barrier_Isync" -> Sail2_instr_kinds.Barrier_Isync
+ | "Barrier_DMB" -> Sail2_instr_kinds.Barrier_DMB
+ | "Barrier_DMB_ST" -> Sail2_instr_kinds.Barrier_DMB_ST
+ | "Barrier_DMB_LD" -> Sail2_instr_kinds.Barrier_DMB_LD
+ | "Barrier_DSB" -> Sail2_instr_kinds.Barrier_DSB
+ | "Barrier_DSB_ST" -> Sail2_instr_kinds.Barrier_DSB_ST
+ | "Barrier_DSB_LD" -> Sail2_instr_kinds.Barrier_DSB_LD
+ | "Barrier_ISB" -> Sail2_instr_kinds.Barrier_ISB
+ | "Barrier_MIPS_SYNC" -> Sail2_instr_kinds.Barrier_MIPS_SYNC
+ | "Barrier_RISCV_rw_rw" -> Sail2_instr_kinds.Barrier_RISCV_rw_rw
+ | "Barrier_RISCV_r_rw" -> Sail2_instr_kinds.Barrier_RISCV_r_rw
+ | "Barrier_RISCV_r_r" -> Sail2_instr_kinds.Barrier_RISCV_r_r
+ | "Barrier_RISCV_rw_w" -> Sail2_instr_kinds.Barrier_RISCV_rw_w
+ | "Barrier_RISCV_w_w" -> Sail2_instr_kinds.Barrier_RISCV_w_w
+ | "Barrier_RISCV_w_rw" -> Sail2_instr_kinds.Barrier_RISCV_w_rw
+ | "Barrier_RISCV_rw_r" -> Sail2_instr_kinds.Barrier_RISCV_rw_r
+ | "Barrier_RISCV_r_w" -> Sail2_instr_kinds.Barrier_RISCV_r_w
+ | "Barrier_RISCV_w_r" -> Sail2_instr_kinds.Barrier_RISCV_w_r
+ | "Barrier_RISCV_i" -> Sail2_instr_kinds.Barrier_RISCV_i
+ | "Barrier_x86_MFENCE" -> Sail2_instr_kinds.Barrier_x86_MFENCE
+ | s -> failwith ("Unknown barrier kind: " ^ s)
+
let initial_lstate =
{ locals = Bindings.empty }
@@ -646,45 +806,161 @@ 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 state * effect_request
+
+(* 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_memv of 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)
| Break frame -> Break frame
+ | Effect_request (state, eff) -> Effect_request (state, 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 (state, Read_reg (name, fun v state' -> eval_frame' (Step (out, state', cont v, stack))))
+ | Yield (Write_reg (name, v, cont)), _ ->
+ Effect_request (state, 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 (state, 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 (state, Write_ea (wk, addr, len, fun () state' -> eval_frame' (Step (out, state', cont (), stack))))
+ | Yield (Excl_res cont), _ ->
+ Effect_request (state, Excl_res (fun b state' -> eval_frame' (Step (out, state', cont b, stack))))
+ | Yield (Write_memv (v, cont)), _ ->
+ Effect_request (state, Write_memv (v, fun b state' -> eval_frame' (Step (out, state', cont b, stack))))
+ | Yield (Barrier (bk, cont)), _ ->
+ Effect_request (state, 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), _ ->
+ Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_ok v), stack')
+ | Yield (Assertion_failed msg), _ | Yield (Fail msg), _ ->
failwith msg
| Yield (Exception v), [] ->
failwith ("Uncaught Exception" |> Util.cyan |> Util.clear)
| 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_memv (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
@@ -692,20 +968,32 @@ let rec run_frame frame =
run_frame (eval_frame frame)
| Break frame ->
run_frame (eval_frame frame)
+ | Effect_request (state, 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 ->
@@ -717,4 +1005,48 @@ 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 =
+ try
+ 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
+ let evaled = eval_exp state typed in
+ Value_success evaled
+ with _ as exn ->
+ Value_error exn
+
+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 4c7cf8d6..30e02b36 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -111,7 +111,7 @@ let sail_logo =
let vs_ids = ref (Initial_check.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 []
@@ -164,6 +164,14 @@ let rec run () =
| Break frame ->
print_endline "Breakpoint";
current_mode := Evaluation frame
+ | Effect_request (state, eff) ->
+ begin
+ try
+ current_mode := Evaluation (Interpreter.default_effect_interp state eff)
+ with
+ | Failure str -> print_endline str; current_mode := Normal
+ end;
+ run ()
end
| Bytecode _ -> ()
@@ -190,6 +198,14 @@ let rec run_steps n =
| Break frame ->
print_endline "Breakpoint";
current_mode := Evaluation frame
+ | Effect_request (state, 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
| Bytecode _ -> ()
@@ -208,6 +224,8 @@ let help = function
":help <command> - Get a description of <command>. Commands are prefixed with a colon, e.g. :help :type."
| ":elf" ->
":elf <file> - Load an ELF 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" ->
@@ -368,7 +386,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))
| ":compile" ->
@@ -415,13 +433,23 @@ let handle_input' input =
let (_, ast, env) = load_files !Interactive.env files in
let ast = Process_file.rewrite_ast_interpreter !Interactive.env ast 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 := Initial_check.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 := Initial_check.val_spec_ids !Interactive.ast;
(* See initial_check.mli for an explanation of why we need this. *)
Initial_check.have_undefined_builtins := false;
@@ -457,7 +485,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 := Initial_check.val_spec_ids !Interactive.ast;
print_endline ("(message \"Checked " ^ arg ^ " done\")\n");
@@ -468,7 +496,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 := Initial_check.val_spec_ids !Interactive.ast;
Initial_check.have_undefined_builtins := false;
Process_file.clear_symbols ()
@@ -536,6 +564,15 @@ let handle_input' input =
| Break frame ->
print_endline "Breakpoint";
current_mode := Evaluation frame
+ | Effect_request (state, 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
| Bytecode (gstate, stack) ->
@@ -549,7 +586,7 @@ let handle_input' input =
current_mode := Bytecode (gstate, stack);
print_program ()
end
-
+
let handle_input input =
try handle_input' input with
| Type_check.Type_error (env, l, err) ->
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index f0472385..9b954611 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -4348,9 +4348,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 a5f0653b..f42a279b 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -465,8 +465,8 @@ let ocaml_funcls ctx =
| _ -> failwith "Found val spec which was not a function!"
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 =
@@ -624,8 +624,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
@@ -990,6 +990,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 2ff7b5e2..b86d4dd5 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 4004f53d..9f7e2e0c 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 42780012..4553de56 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -2762,8 +2762,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 1c30e06e..6adcec46 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1378,7 +1378,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 27f626ea..56026c81 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -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/process_file.ml b/src/process_file.ml
index e7bf8d30..3c2d4a22 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -409,7 +409,7 @@ let rewrite_ast_ocaml env = rewrite env Rewrites.rewrite_defs_ocaml
let rewrite_ast_c env ast =
ast
|> rewrite env Rewrites.rewrite_defs_c
- |> rewrite env [("constant_fold", fun _ -> Constant_fold.rewrite_constant_function_calls)]
+ |> rewrite env [("constant_fold", fun _ -> Constant_fold.rewrite_constant_function_calls env)]
let rewrite_ast_interpreter env = rewrite env Rewrites.rewrite_defs_interpreter
let rewrite_ast_check env = rewrite env Rewrites.rewrite_defs_check
diff --git a/src/rewrites.ml b/src/rewrites.ml
index d8cb5a5d..0be6825a 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2127,7 +2127,7 @@ let rewrite_split_fun_constr_pats fun_name env (Defs defs) =
in
let val_spec =
VS_aux (VS_val_spec
- (mk_typschm typquant fun_typ, id, (fun _ -> None), false),
+ (mk_typschm typquant 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
@@ -3102,7 +3102,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
@@ -4355,10 +4355,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
@@ -4392,7 +4392,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
@@ -4402,7 +4402,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
diff --git a/src/sail.ml b/src/sail.ml
index 949663d4..eb25f56d 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -59,6 +59,8 @@ let opt_print_version = ref false
let opt_print_initial_env = ref false
let opt_print_verbose = ref false
let opt_print_lem = ref false
+let opt_print_tofrominterp = ref false
+let opt_tofrominterp_output_dir : string option ref = ref None
let opt_print_ocaml = ref false
let opt_print_c = ref false
let opt_print_latex = ref false
@@ -72,6 +74,7 @@ let opt_libs_coq = ref ([]:string list)
let opt_file_arguments = ref ([]:string list)
let opt_process_elf : string option ref = ref None
let opt_ocaml_generators = ref ([]:string list)
+let opt_marshal_defs = ref false
let opt_slice = ref ([]:string list)
let options = Arg.align ([
@@ -94,6 +97,15 @@ let options = Arg.align ([
( "-no_warn",
Arg.Clear Util.opt_warnings,
" do not print warnings");
+ ( "-tofrominterp",
+ Arg.Set opt_print_tofrominterp,
+ " output OCaml functions to translate between shallow embedding and interpreter");
+ ( "-tofrominterp_lem",
+ Arg.Set ToFromInterp_backend.lem_mode,
+ " output embedding translation for the Lem backend rather than the OCaml backend");
+ ( "-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 [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen],
" output an OCaml translated version of the input");
@@ -127,6 +139,9 @@ let options = Arg.align ([
( "-latex_full_valspecs",
Arg.Clear Latex.opt_simple_val,
" print full valspecs in LaTeX output");
+ ( "-marshal",
+ Arg.Set opt_marshal_defs,
+ " OCaml-marshal out the rewritten AST to a file");
( "-c",
Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen],
" output a C translated version of the input");
@@ -418,6 +433,12 @@ let main() =
let out = match !opt_file_out with None -> "out" | Some s -> s in
Ocaml_backend.ocaml_compile out ast_ocaml ocaml_generator_info
else ());
+ (if !opt_print_tofrominterp
+ then
+ let ast = rewrite_ast_interpreter type_envs ast in
+ let out = match !opt_file_out with None -> "out" | Some s -> s in
+ ToFromInterp_backend.tofrominterp_output !opt_tofrominterp_output_dir out ast
+ else ());
(if !(opt_print_c)
then
let ast_c = rewrite_ast_c type_envs ast in
@@ -463,6 +484,18 @@ let main() =
close_out chan
end
else ());
+ (if !(opt_marshal_defs)
+ then
+ begin
+ let ast_marshal = rewrite_ast_ocaml type_envs ast in
+ let out_filename = match !opt_file_out with None -> "out" | Some s -> s in
+ let f = open_out_bin (out_filename ^ ".defs") in
+ Marshal.to_string ast_marshal [Marshal.No_sharing; Marshal.Compat_32]
+ |> B64.encode
+ |> output_string f;
+ close_out f
+ end
+ else ());
if !opt_memo_z3 then Constraint.save_digests () else ()
end
diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml
new file mode 100644
index 00000000..5a03ca83
--- /dev/null
+++ b/src/toFromInterp_backend.ml
@@ -0,0 +1,294 @@
+(**************************************************************************)
+(* 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 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 (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, _)) = 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
+ | _ -> string "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])
+ | 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 "regfp"),_) -> empty
+ | Id_aux ((Id "niafp"),_) -> empty
+ | Id_aux ((Id "diafp"),_) -> empty *)
+ (* | Id_aux ((Id "option"),_) -> empty *)
+ | _ ->
+ 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, typq, typ_arg) ->
+ let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in
+ let fromInterpValue =
+ (separate space [string "let"; fromInterpValueName; separate space (fromValueTypqs typq); equals; fromValueTypArg typ_arg])
+ in
+ fromInterpValue ^^ (twice hardline)
+ | 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 (id, typq, fields, _) ->
+ let fromInterpField (typ, id) =
+ separate space [string (maybe_zencode (string_of_id id)); equals; fromValueTyp typ ("(StringMap.find \"" ^ (string_of_id id) ^ "\" fs)")]
+ in
+ 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 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, _)) = 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
+ | _ -> string "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])
+ | 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 (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 "regfp"),_) -> empty
+ | Id_aux ((Id "niafp"),_) -> empty
+ | Id_aux ((Id "diafp"),_) -> empty *)
+ (* | Id_aux ((Id "option"),_) -> empty *)
+ | _ ->
+ 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, typq, typ_arg) ->
+ let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in
+ let toInterpValue =
+ (separate space [string "let"; toInterpValueName; separate space (toValueTypqs typq); equals; toValueTypArg typ_arg])
+ in
+ toInterpValue ^^ (twice hardline)
+ | 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 (id, typq, fields, _) ->
+ let toInterpField (typ, id) =
+ parens (separate comma_sp [dquotes (string (string_of_id id)); toValueTyp typ ("r." ^ (maybe_zencode (string_of_id id)))])
+ in
+ 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 "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)
+ ^^ (string ("open " ^ String.capitalize_ascii name ^ ";;") ^^ hardline)
+ ^^ (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 ^ "_toFromInterp.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..5e776853
--- /dev/null
+++ b/src/toFromInterp_lib.ml
@@ -0,0 +1,101 @@
+(************************************************************)
+(* Support for toFromInterp *)
+(************************************************************)
+
+open Sail_lib;;
+open Value;;
+
+type vector_order =
+ | Order_inc
+ | Order_dec
+
+
+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
diff --git a/src/type_check.ml b/src/type_check.ml
index 5bc3cc2d..a69d24cf 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -114,11 +114,10 @@ type env =
shadow_vars : int KBindings.t;
typ_synonyms : (Ast.l -> env -> typ_arg list -> 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;
@@ -126,7 +125,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;
}
@@ -419,9 +418,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
@@ -440,7 +436,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
@@ -475,7 +471,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. *)
@@ -500,7 +496,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;
@@ -512,11 +507,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 }
@@ -610,7 +605,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)
@@ -1094,17 +1089,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
@@ -1114,7 +1098,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 *)
@@ -1123,7 +1107,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
@@ -1146,8 +1130,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
@@ -3421,7 +3404,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
@@ -4690,7 +4673,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, _) -> ()
@@ -4810,9 +4793,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
@@ -4824,7 +4807,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 =
@@ -5017,7 +5000,7 @@ 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.set_prover (Some (prove __POS__))
(* |> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args))) *)
(* Internal functions for Monomorphise.AtomToItself *)
@@ -5025,13 +5008,13 @@ let initial_env =
(* |> Env.add_val_spec (mk_id "int")
* (TypQ_aux (TypQ_no_forall, Parse_ast.Unknown), Typ_aux (Typ_bidir (int_typ, string_typ), Parse_ast.Unknown)) *)
- |> Env.add_extern (mk_id "size_itself_int") (fun _ -> Some "size_itself_int")
+ |> 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 15110b37..bd4c88dc 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -214,6 +214,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
(** Push all the type variables and constraints from a typquant into
@@ -408,6 +410,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 AST} *)
(** Fully type-check an AST
diff --git a/src/value.ml b/src/value.ml
index 8f8e651a..843a943b 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -280,6 +280,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"
@@ -319,6 +323,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"
@@ -418,6 +430,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"
@@ -521,6 +541,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"
@@ -565,6 +593,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)
@@ -579,6 +611,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);
@@ -611,6 +644,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);
@@ -622,6 +656,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);
@@ -630,6 +666,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);
@@ -657,7 +695,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);
@@ -677,4 +717,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 18:28:10 +0000