summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.merlin2
-rw-r--r--editors/sail-mode.el23
-rw-r--r--src/_tags4
-rw-r--r--src/bitfield.ml12
-rw-r--r--src/initial_check.ml14
-rw-r--r--src/initial_check.mli7
-rw-r--r--src/isail.ml53
-rw-r--r--src/process_file.ml6
-rw-r--r--src/process_file.mli1
-rw-r--r--src/sail.ml4
-rw-r--r--src/state.ml2
11 files changed, 93 insertions, 35 deletions
diff --git a/.merlin b/.merlin
index d764f5eb..92bbd164 100644
--- a/.merlin
+++ b/.merlin
@@ -9,4 +9,4 @@ S src/lem_interp/**
S src/pprint/**
S src/test/**
B src/_build/**
-PKG num str unix uint zarith linksem lem omd linenoise \ No newline at end of file
+PKG num str unix uint zarith linksem lem omd linenoise yojson
diff --git a/editors/sail-mode.el b/editors/sail-mode.el
index 35025d52..ca34ed28 100644
--- a/editors/sail-mode.el
+++ b/editors/sail-mode.el
@@ -86,6 +86,8 @@
(setq comment-end "*/")
(setq major-mode 'sail2-mode)
(setq mode-name "Sail2")
+ (add-hook 'sail2-mode-hook
+ (lambda () (add-hook 'before-save-hook 'sail-load nil 'local)))
(run-hooks 'sail2-mode-hook))
(defvar sail-process nil)
@@ -105,7 +107,7 @@
(defun sail-start ()
"start Sail interactive mode"
(interactive)
- (setq sail-process (start-process "sail" "Sail" "sail" "-i" "-emacs"))
+ (setq sail-process (start-process "sail" "Sail" "sail" "-i" "-emacs" "-no_warn"))
(set-process-filter sail-process 'sail-filter))
(defun sail-quit ()
@@ -122,6 +124,8 @@
(overlay-put overlay 'help-echo text)
(setq mark-active nil))))
+(defvar sail-error-position nil)
+
(defun sail-error (l1 c1 l2 c2 text)
(let ((begin (save-excursion
(goto-line l1)
@@ -131,12 +135,16 @@
(goto-line l2)
(forward-char c2)
(point))))
+ (setq sail-error-position begin)
(sail-error-region begin end text)
(message text)))
-(defun sail-test ()
+(defun sail-goto-error ()
+ "Go to the next Sail error"
(interactive)
- (sail-error 6 18 6 19 "error message\ntooltip"))
+ (if sail-error-position
+ (goto-char sail-error-position)
+ (message "No errors")))
(defun sail-load ()
"load a Sail file"
@@ -145,6 +153,7 @@
(error "No sail process (call sail-start)")
(progn
(remove-overlays)
+ (setq sail-error-position nil)
(process-send-string sail-process ":unload\n")
(process-send-string sail-process (mapconcat 'identity `(":load " ,buffer-file-name "\n") "")))))
@@ -153,6 +162,7 @@
(define-key map (kbd "C-c C-s") 'sail-start)
(define-key map (kbd "C-c C-l") 'sail-load)
(define-key map (kbd "C-c C-q") 'sail-quit)
+ (define-key map (kbd "C-c C-x") 'sail-goto-error)
map))
(defun sail-build-menu ()
@@ -160,9 +170,10 @@
sail-mode-menu (list sail-mode-map)
"Sail Mode Menu."
'("Sail"
- ["Start" sail-start t]
- ["Quit" sail-quit t]
- ["Check buffer" sail-load t]))
+ ["Start interactive" sail-start t]
+ ["Quit interactive" sail-quit t]
+ ["Check buffer" sail-load t]
+ ["Goto next error" sail-goto-error t]))
(easy-menu-add sail-mode-menu))
(provide 'sail2-mode)
diff --git a/src/_tags b/src/_tags
index 4630bea8..aac18862 100644
--- a/src/_tags
+++ b/src/_tags
@@ -3,9 +3,9 @@ true: -traverse, debug, use_menhir
<**/*.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), use_pprint
+<isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), package(omd), package(yojson), use_pprint
-<isail.ml>: package(linenoise)
+<isail.ml>: package(linenoise), package(yojson)
<elf_loader.ml>: package(linksem)
<latex.ml>: package(omd)
<**/*.m{l,li}>: package(lem)
diff --git a/src/bitfield.ml b/src/bitfield.ml
index afdd5baf..e8250598 100644
--- a/src/bitfield.ml
+++ b/src/bitfield.ml
@@ -75,7 +75,7 @@ let newtype name size order =
chunk_rem :: List.rev chunks_64
in
let nt = Printf.sprintf "struct %s = {\n %s }" name (Util.string_of_list ",\n " (fun x -> x) chunks) in
- ast_of_def_string order nt
+ ast_of_def_string nt
let rec translate_indices hi lo =
if hi / 64 = lo / 64 then
@@ -97,7 +97,7 @@ let constructor name order start stop =
"}"
]
in
- combine [ast_of_def_string order constructor_val; ast_of_def_string order constructor_function]
+ combine [ast_of_def_string constructor_val; ast_of_def_string constructor_function]
(* For every index range, create a getter and setter *)
let index_range_getter name field order start stop =
@@ -108,7 +108,7 @@ let index_range_getter name field order start stop =
Printf.sprintf "v.%s_chunk_%i[%i .. %i]" name chunk start stop
in
let irg_function = Printf.sprintf "function _get_%s_%s v = %s" name field (Util.string_of_list " @ " body indices) in
- combine [ast_of_def_string order irg_val; ast_of_def_string order irg_function]
+ combine [ast_of_def_string irg_val; ast_of_def_string irg_function]
let index_range_setter name field order start stop =
let indices = translate_indices start stop in
@@ -127,7 +127,7 @@ let index_range_setter name field order start stop =
"}"
]
in
- combine [ast_of_def_string order irs_val; ast_of_def_string order irs_function]
+ combine [ast_of_def_string irs_val; ast_of_def_string irs_function]
let index_range_update name field order start stop =
let indices = translate_indices start stop in
@@ -145,10 +145,10 @@ let index_range_update name field order start stop =
]
in
let iru_overload = Printf.sprintf "overload update_%s = {_update_%s_%s}" field name field in
- combine [ast_of_def_string order iru_val; ast_of_def_string order iru_function; ast_of_def_string order iru_overload]
+ combine [ast_of_def_string iru_val; ast_of_def_string iru_function; ast_of_def_string iru_overload]
let index_range_overload name field order =
- ast_of_def_string order (Printf.sprintf "overload _mod_%s = {_get_%s_%s, _set_%s_%s}" field name field name field)
+ ast_of_def_string (Printf.sprintf "overload _mod_%s = {_get_%s_%s, _set_%s_%s}" field name field name field)
let index_range_accessor name field order (BF_aux (bf_aux, l)) =
let getter n m = index_range_getter name field order (Big_int.to_int n) (Big_int.to_int m) in
diff --git a/src/initial_check.ml b/src/initial_check.ml
index ae65f13d..d08ab8cf 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1010,18 +1010,20 @@ let generate_enum_functions vs_ids (Defs defs) =
let incremental_ctx = ref initial_ctx
-let process_ast order defs =
+let process_ast ?generate:(generate=true) defs =
let ast, ctx = to_ast !incremental_ctx defs in
incremental_ctx := ctx;
let vs_ids = val_spec_ids ast in
- if not !opt_undefined_gen then
+ if not !opt_undefined_gen && generate then
generate_enum_functions vs_ids ast
- else
+ else if generate then
ast
|> generate_undefineds vs_ids
|> generate_enum_functions vs_ids
|> generate_initialize_registers vs_ids
-
-let ast_of_def_string order str =
+ else
+ ast
+
+let ast_of_def_string str =
let def = Parser.def_eof Lexer.token (Lexing.from_string str) in
- process_ast order (P.Defs [def])
+ process_ast (P.Defs [def])
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 9d2beab2..a0bde482 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -82,8 +82,11 @@ val opt_enum_casts : bool ref
all the loaded files. *)
val have_undefined_builtins : bool ref
-val ast_of_def_string : order -> string -> unit defs
-val process_ast : order -> Parse_ast.defs -> unit defs
+val ast_of_def_string : string -> unit defs
+
+(** If the generate flag is false, then we won't generate any
+ auxilliary definitions, like the initialize_registers function *)
+val process_ast : ?generate:bool -> Parse_ast.defs -> unit defs
val val_spec_ids : 'a defs -> IdSet.t
diff --git a/src/isail.ml b/src/isail.ml
index 944b14a2..d245ab14 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -238,12 +238,56 @@ let format_pos_emacs p1 p2 contents =
let rec emacs_error l contents =
match l with
- | Parse_ast.Unknown -> "(error \"no location info\")"
+ | Parse_ast.Unknown -> "(error \"no location info: " ^ contents ^ "\")"
| Parse_ast.Range (p1, p2) -> format_pos_emacs p1 p2 contents
| Parse_ast.Unique (_, l) -> emacs_error l contents
| Parse_ast.Documented (_, l) -> emacs_error l contents
| Parse_ast.Generated l -> emacs_error l contents
+type session = {
+ id : string;
+ files : string list
+ }
+
+let default_session = {
+ id = "none";
+ files = []
+ }
+
+let session = ref default_session
+
+let parse_session file =
+ let open Yojson.Basic.Util in
+ if Sys.file_exists file then
+ let json = Yojson.Basic.from_file file in
+ let args = Str.split (Str.regexp " +") (json |> member "options" |> to_string) in
+ Arg.parse_argv ~current:(ref 0) (Array.of_list ("sail" :: args)) Sail.options (fun _ -> ()) "";
+ print_endline ("(message \"Using session " ^ file ^ "\")");
+ {
+ id = file;
+ files = json |> member "files" |> convert_each to_string
+ }
+ else
+ default_session
+
+let load_session upto file =
+ match upto with
+ | None -> None
+ | Some upto_file when Filename.basename upto_file = file -> None
+ | Some upto_file ->
+ let (_, ast, env) =
+ load_files ~generate:false !Interactive.env [Filename.concat (Filename.dirname upto_file) file]
+ in
+ Interactive.ast := append_ast !Interactive.ast ast;
+ Interactive.env := env;
+ print_endline ("(message \"Checked " ^ file ^ "...\")\n");
+ Some upto_file
+
+let load_into_session file =
+ let session_file = Filename.concat (Filename.dirname file) "sail.json" in
+ session := (if session_file = !session.id then !session else parse_session session_file);
+ ignore (List.fold_left load_session (Some file) !session.files)
+
type input = Command of string * string | Expression of string | Empty
(* This function is called on every line of input passed to the interpreter *)
@@ -419,12 +463,13 @@ let handle_input' input =
| ":load" ->
begin
try
- let files = Util.split_on_char ' ' arg in
- let (_, ast, env) = load_files !Interactive.env files in
+ 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.env := env;
- vs_ids := Initial_check.val_spec_ids !Interactive.ast
+ vs_ids := Initial_check.val_spec_ids !Interactive.ast;
+ print_endline ("(message \"Checked " ^ arg ^ " done\")\n");
with
| Reporting.Fatal_error (Err_type (l, msg)) ->
print_endline (emacs_error l (String.escaped msg))
diff --git a/src/process_file.ml b/src/process_file.ml
index 98dc725d..e8f255ff 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -239,12 +239,10 @@ let rec preprocess opts = function
let preprocess_ast opts (Parse_ast.Defs defs) = Parse_ast.Defs (preprocess opts defs)
-let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs
-
-let load_file_no_check opts order f = convert_ast order (preprocess_ast opts (parse_file f))
+let load_file_no_check opts order f = Initial_check.process_ast (preprocess_ast opts (parse_file f))
let load_file opts order env f =
- let ast = convert_ast order (preprocess_ast opts (parse_file f)) in
+ let ast = Initial_check.process_ast (preprocess_ast opts (parse_file f)) in
Type_error.check env ast
let opt_just_check = ref false
diff --git a/src/process_file.mli b/src/process_file.mli
index 4496e046..f75f6687 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -54,7 +54,6 @@ val parse_file : ?loc:Parse_ast.l -> string -> Parse_ast.defs
val clear_symbols : unit -> unit
-val convert_ast : Ast.order -> Parse_ast.defs -> unit Ast.defs
val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs
val check_ast: Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
diff --git a/src/sail.ml b/src/sail.ml
index 3675cb76..286141ab 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -312,7 +312,7 @@ let _ =
opt_file_arguments := (!opt_file_arguments) @ [s])
usage_msg
-let load_files type_envs files =
+let load_files ?generate:(generate=true) type_envs files =
if !opt_memo_z3 then Constraint.load_digests () else ();
let t = Profile.start () in
@@ -321,7 +321,7 @@ let load_files type_envs files =
List.fold_right (fun (_, Parse_ast.Defs ast_nodes) (Parse_ast.Defs later_nodes)
-> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
let ast = Process_file.preprocess_ast options ast in
- let ast = convert_ast Ast_util.inc_ord ast in
+ let ast = Initial_check.process_ast ~generate:generate ast in
Profile.finish "parsing" t;
let t = Profile.start () in
diff --git a/src/state.ml b/src/state.ml
index 74bc97b2..86fd8395 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -58,7 +58,7 @@ open PPrint
open Pretty_print_common
open Pretty_print_sail
-let defs_of_string = ast_of_def_string Ast_util.inc_ord
+let defs_of_string = ast_of_def_string
let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs (Defs defs))
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:45:10 +0000