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.ml128
-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.ml18
-rw-r--r--src/type_check.ml41
-rw-r--r--src/type_check.mli2
-rw-r--r--src/value.ml43
22 files changed, 702 insertions, 247 deletions
diff --git a/src/Makefile b/src/Makefile
index b0b22f77..e29a1ef0 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 5746a242..04b76a61 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -1708,6 +1708,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 fe722f5e..a2466326 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -425,6 +425,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 7321a801..031493a4 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
@@ -205,11 +213,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 88fcfddb..c6fb0589 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -149,6 +149,24 @@ let load_elf ?writer:(writer=write_sail_lib) name =
opt_elf_tohost := tohost_addr);
List.iter (load_segment ~writer:writer) segments
+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 07316c6d..f728d92d 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 7d009791..e513e0ee 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" ->
@@ -377,7 +395,7 @@ let handle_input' input =
let ast, env = Specialize.specialize !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" ->
@@ -424,13 +442,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;
@@ -466,7 +494,7 @@ let handle_input' input =
load_into_session arg;
let (_, ast, env) = load_files !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");
@@ -477,7 +505,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 ()
@@ -545,6 +573,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) ->
@@ -558,7 +595,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 8c52fce1..3167ad6b 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -4333,9 +4333,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 d51aba75..2cbdfab2 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -456,70 +456,76 @@ let ocaml_funcls ctx =
function
| [] -> failwith "Ocaml: empty function"
| [FCL_aux (FCL_Funcl (id, pexp),_)] ->
- let arg_typs, ret_typ =
- match Bindings.find id ctx.val_specs with
- | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
- | _ -> failwith "Found val spec which was not a function!"
- in
- (* Any remaining type variables after simple_typ rewrite should
- 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 =
- match pexp with
- | Pat_aux (Pat_exp (pat, exp),_) -> pat,exp
- | Pat_aux (Pat_when (pat, wh, exp),_) -> failwith "OCaml: top-level pattern guards not supported"
- in
- let annot_pat =
- let pat =
+ if Bindings.mem id ctx.externs
+ then string ("(* Omitting externed function " ^ string_of_id id ^ " *)") ^^ hardline
+ else
+ let arg_typs, ret_typ =
+ match Bindings.find id ctx.val_specs with
+ | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
+ | _ -> failwith "Found val spec which was not a function!"
+ in
+ (* Any remaining type variables after simple_typ rewrite should
+ 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 =
+ match pexp with
+ | Pat_aux (Pat_exp (pat, exp),_) -> pat,exp
+ | Pat_aux (Pat_when (pat, wh, exp),_) -> failwith "OCaml: top-level pattern guards not supported"
+ in
+ let annot_pat =
+ let pat =
+ if KidSet.is_empty kids then
+ parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs)))
+ else
+ ocaml_pat ctx pat
+ in
+ if !opt_trace_ocaml
+ then parens (separate space [pat; string "as"; pat_sym])
+ else pat
+ in
+ let call_header = function_header () in
+ let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
+ let call =
if KidSet.is_empty kids then
- parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs)))
+ separate space [call_header; zencode ctx id;
+ annot_pat; colon; ocaml_typ ctx ret_typ; equals;
+ sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
+ ^//^ ocaml_exp ctx exp
+ ^^ rparen
else
- ocaml_pat ctx pat
+ separate space [call_header; zencode ctx id; colon;
+ separate space (List.map zencode_kid (KidSet.elements kids)) ^^ dot;
+ ocaml_typ ctx (mk_typ (Typ_tup arg_typs)); string "->"; ocaml_typ ctx ret_typ; equals;
+ string "fun"; annot_pat; string "->";
+ sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
+ ^//^ ocaml_exp ctx exp
+ ^^ rparen
in
- if !opt_trace_ocaml
- then parens (separate space [pat; string "as"; pat_sym])
- else pat
- in
- let call_header = function_header () in
- let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
- let call =
- if KidSet.is_empty kids then
- separate space [call_header; zencode ctx id;
- annot_pat; colon; ocaml_typ ctx ret_typ; equals;
- sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
- ^//^ ocaml_exp ctx exp
- ^^ rparen
- else
- separate space [call_header; zencode ctx id; colon;
- separate space (List.map zencode_kid (KidSet.elements kids)) ^^ dot;
- ocaml_typ ctx (mk_typ (Typ_tup arg_typs)); string "->"; ocaml_typ ctx ret_typ; equals;
- string "fun"; annot_pat; string "->";
- sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
- ^//^ ocaml_exp ctx exp
- ^^ rparen
- in
- ocaml_funcl call string_of_arg string_of_ret
+ ocaml_funcl call string_of_arg string_of_ret
| funcls ->
let id = funcls_id funcls in
- let arg_typs, ret_typ =
- match Bindings.find id ctx.val_specs with
- | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
- | _ -> failwith "Found val spec which was not a function!"
- in
- let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
- if not (KidSet.is_empty kids) then failwith "Cannot handle polymorphic multi-clause function in OCaml backend" else ();
- let pat_sym = gensym () in
- let call_header = function_header () in
- let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
- let call =
- separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))); equals;
- sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
- ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls)
- ^^ rparen
- in
- ocaml_funcl call string_of_arg string_of_ret
+ if Bindings.mem id ctx.externs
+ then string ("(* Omitting externed function " ^ string_of_id id ^ " *)") ^^ hardline
+ else
+ let arg_typs, ret_typ =
+ match Bindings.find id ctx.val_specs with
+ | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
+ | _ -> failwith "Found val spec which was not a function!"
+ in
+ let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
+ if not (KidSet.is_empty kids) then failwith "Cannot handle polymorphic multi-clause function in OCaml backend" else ();
+ let pat_sym = gensym () in
+ let call_header = function_header () in
+ let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
+ let call =
+ separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))); equals;
+ sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
+ ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls)
+ ^^ rparen
+ in
+ ocaml_funcl call string_of_arg string_of_ret
let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) =
ocaml_funcls ctx funcls
@@ -618,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
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index eb5c3dc6..5f0d7487 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 bd832d28..2cd0dbe1 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 4596f23f..46d07cc3 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -2568,8 +2568,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 dee0a29f..aa03528f 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1377,7 +1377,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 f30d5135..67f291bd 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -624,9 +624,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 52e0cd08..d2a43b4a 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 5a70a721..44d99537 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2126,7 +2126,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
@@ -3101,7 +3101,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
@@ -4350,10 +4350,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
@@ -4387,7 +4387,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_pure, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
@@ -4397,7 +4397,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_pure, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
diff --git a/src/sail.ml b/src/sail.ml
index 06bd618e..82c1244b 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -72,6 +72,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 ([
@@ -114,13 +115,16 @@ let options = Arg.align ([
"<types> produce random generators for the given types");
( "-latex",
Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ],
- " pretty print the input to LaTeX");
+ " pretty print the input to latex");
( "-latex_prefix",
Arg.String (fun prefix -> Latex.opt_prefix := prefix),
" set a custom prefix for generated LaTeX macro command (default sail)");
( "-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");
@@ -437,6 +441,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/type_check.ml b/src/type_check.ml
index a8251e97..b9f8f323 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -109,11 +109,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;
@@ -349,9 +348,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
@@ -370,7 +366,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
@@ -429,7 +425,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;
@@ -1015,17 +1010,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
@@ -1035,7 +1019,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 *)
@@ -1044,7 +1028,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
@@ -1067,8 +1051,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
@@ -3289,7 +3272,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
@@ -4558,7 +4541,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, _) -> ()
@@ -4678,9 +4661,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
@@ -4692,7 +4675,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 =
@@ -4893,13 +4876,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 eab96b07..4ff52cd9 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -396,6 +396,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 729b3974..261b0f4e 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"
@@ -414,6 +426,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"
@@ -517,6 +537,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"
@@ -561,6 +589,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)
@@ -575,6 +607,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);
@@ -607,6 +640,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);
@@ -618,6 +652,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);
@@ -626,6 +662,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);
@@ -652,7 +690,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);
@@ -672,4 +712,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-04 23:06:07 +0000