Emacs mode understands relationships between Sail files

Allow a file sail.json in the same directory as the sail source file
which contains the ordering and options needed for sail files involved
in a specific ISA definition. I have an example for v8.5 in sail-arm.
The interactive Sail process running within emacs then knows about the
relationship between Sail files, so C-c C-l works for files in the ARM
spec. Also added a C-c C-x command to jump to a type error. Requires
yojson library to build interactive Sail.

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))