More work on GDB interface

The following now works to run sail on every HVC call with hafnium

function gdb_init() -> unit = {
  // Connect to QEMU via GDB
  sail_gdb_qemu("");
  sail_gdb_symbol_file("hafnium.elf.sym");
  sail_gdb_send("break-insert sync_lower_exception")
}

function gdb() -> unit = {
  gdb_init();
  while true do {
    sail_gdb_send("exec-continue");
    sail_gdb_sync()
  }
}

6 files changed, 288 insertions, 6 deletions

diff --git a/src/gdbmi.ml b/src/gdbmi.ml
index 00408388..14b4d4c3 100644
--- a/src/gdbmi.ml
+++ b/src/gdbmi.ml
@@ -49,6 +49,11 @@
 (**************************************************************************)
 
 open Printf
+open Gdbmi_types
+
+let parse_gdb_response str =
+  let lexbuf = Lexing.from_string str in
+  Gdbmi_parser.response_eof Gdbmi_lexer.token lexbuf
 
 type gdb_session = (in_channel * out_channel * in_channel) option
 
@@ -65,7 +70,7 @@ let not_connected = Reporting.err_general Parse_ast.Unknown "Not connected to gd
 let rec wait_for' regexp stdout =
   let line = input_line stdout in
   if Str.string_match regexp line 0 then (
-    print_endline line
+    line
   ) else (
     print_endline Util.(line |> dim |> clear);
     wait_for' regexp stdout
@@ -84,13 +89,31 @@ let send_sync session cmd =
   | None -> raise not_connected
   | Some (stdout, stdin, _) ->
      let token = gdb_token () in
-     let cmd =sprintf "%i-%s\n" token cmd in
+     let cmd = sprintf "%i-%s\n" token cmd in
      print_string Util.(cmd |> yellow |> clear);
      flush stdin;
      output_string stdin cmd;
      flush stdin;
      wait_for token stdout
 
+let send_regular session cmd =
+  match session with
+  | None -> raise not_connected
+  | Some (stdout, stdin, _) ->
+     let token = gdb_token () in
+     print_endline Util.(cmd |> yellow |> clear);
+     flush stdin;
+     output_string stdin (cmd ^ "\n");
+     flush stdin;
+     ignore (wait_for_gdb stdout)
+
+let gdb_sync session ast =
+  let gdb_register_names = parse_gdb_response (send_sync session "data-list-register-names") in
+  let gdb_register_values = parse_gdb_response (send_sync session "data-list-register-values x") in
+  print_endline (send_sync session "data-list-register-values x");
+  ()
+
+
 let () =
   let open Interactive in
   let session = ref None in
@@ -98,12 +121,12 @@ let () =
   let gdb_start arg =
     let stdout, stdin, stderr = Unix.open_process_full (sprintf "%s --interpreter=mi" !gdb_command) [||] in
     session := Some (stdout, stdin, stderr);
-    wait_for_gdb stdout;
-    if arg = "" then () else send_sync !session arg
+    wait_for_gdb stdout |> ignore;
+    if arg = "" then () else print_endline (send_sync !session arg)
   in
 
   let gdb_send arg =
-    if arg = "" then () else send_sync !session arg
+    if arg = "" then () else print_endline (send_sync !session arg)
   in
 
   register_command
@@ -132,3 +155,14 @@ let () =
     ~name:"gdb_send"
     ~help:"Send a GDB/MI command to a child GDB process and wait for it to complete"
     (ArgString ("command", fun cmd -> Action (fun () -> gdb_send cmd)));
+
+  register_command
+    ~name:"gdb_sync"
+    ~help:"Sync sail registers with GDB"
+    (Action (fun () -> gdb_sync !session !ast));
+
+  (ArgString ("symbol_file", fun file -> Action (fun () ->
+    send_regular !session ("symbol-file " ^ file)
+  ))) |> register_command
+           ~name:"gdb_symbol_file"
+           ~help:"Load debugging symbols into GDB";
diff --git a/src/gdbmi_lexer.mll b/src/gdbmi_lexer.mll
new file mode 100644
index 00000000..d55ea3cb
--- /dev/null
+++ b/src/gdbmi_lexer.mll
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+{
+
+open Gdbmi_parser
+
+let unescaped s = Scanf.sscanf ("\"" ^ s ^ "\"") "%S%!" (fun x -> x)
+
+}
+
+let ws = [' ''\t']+
+let letter = ['a'-'z''A'-'Z''?']
+let digit = ['0'-'9']
+let hexdigit = ['0'-'9''A'-'F''a'-'f']
+let alphanum = letter|digit
+let startident = letter
+let ident = alphanum|['-']
+let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
+
+rule token = parse
+  | ws
+    { token lexbuf }
+  | "\n"
+    { Lexing.new_line lexbuf;
+      token lexbuf }
+  | "="					{ Eq }
+  | "["                                 { Lsquare }
+  | "]"                                 { Rsquare }
+  | "{"                                 { Lcurly }
+  | "}"                                 { Rcurly }
+  | ","                                 { Comma }
+  | "^"                                 { Caret }
+  | digit+ as i                         { Num (int_of_string i) }
+  | startident ident* as i              { Id i }
+  | '"'                                 { String (string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf) }
+  | eof                                 { Eof }
+
+and string pos b = parse
+  | ([^'"''\n''\\']*'\n' as i)          { Lexing.new_line lexbuf;
+                                          Buffer.add_string b i;
+                                          string pos b lexbuf }
+  | ([^'"''\n''\\']* as i)              { Buffer.add_string b i; string pos b lexbuf }
+  | escape_sequence as i                { Buffer.add_string b i; string pos b lexbuf }
+  | '\\' '\n' ws                        { Lexing.new_line lexbuf; string pos b lexbuf }
+  | '\\'                                { assert false (*raise (Reporting.Fatal_error (Reporting.Err_syntax (pos,
+                                            "illegal backslash escape in string"*) }
+  | '"'                                 { let s = unescaped(Buffer.contents b) in
+                                          (*try Ulib.UTF8.validate s; s
+                                          with Ulib.UTF8.Malformed_code ->
+                                            raise (Reporting.Fatal_error (Reporting.Err_syntax (pos,
+                                              "String literal is not valid utf8"))) *) s }
+  | eof                                 { assert false (*raise (Reporting.Fatal_error (Reporting.Err_syntax (pos,
+                                            "String literal not terminated")))*) }
\ No newline at end of file
diff --git a/src/gdbmi_parser.mly b/src/gdbmi_parser.mly
new file mode 100644
index 00000000..5ae5027f
--- /dev/null
+++ b/src/gdbmi_parser.mly
@@ -0,0 +1,85 @@
+/**************************************************************************/
+/*     Sail                                                               */
+/*                                                                        */
+/*  Copyright (c) 2013-2017                                               */
+/*    Kathyrn Gray                                                        */
+/*    Shaked Flur                                                         */
+/*    Stephen Kell                                                        */
+/*    Gabriel Kerneis                                                     */
+/*    Robert Norton-Wright                                                */
+/*    Christopher Pulte                                                   */
+/*    Peter Sewell                                                        */
+/*    Alasdair Armstrong                                                  */
+/*    Brian Campbell                                                      */
+/*    Thomas Bauereiss                                                    */
+/*    Anthony Fox                                                         */
+/*    Jon French                                                          */
+/*    Dominic Mulligan                                                    */
+/*    Stephen Kell                                                        */
+/*    Mark Wassell                                                        */
+/*                                                                        */
+/*  All rights reserved.                                                  */
+/*                                                                        */
+/*  This software was developed by the University of Cambridge Computer   */
+/*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  */
+/*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   */
+/*                                                                        */
+/*  Redistribution and use in source and binary forms, with or without    */
+/*  modification, are permitted provided that the following conditions    */
+/*  are met:                                                              */
+/*  1. Redistributions of source code must retain the above copyright     */
+/*     notice, this list of conditions and the following disclaimer.      */
+/*  2. Redistributions in binary form must reproduce the above copyright  */
+/*     notice, this list of conditions and the following disclaimer in    */
+/*     the documentation and/or other materials provided with the         */
+/*     distribution.                                                      */
+/*                                                                        */
+/*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    */
+/*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     */
+/*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       */
+/*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   */
+/*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          */
+/*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      */
+/*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      */
+/*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   */
+/*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    */
+/*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    */
+/*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    */
+/*  SUCH DAMAGE.                                                          */
+/**************************************************************************/
+
+%{
+
+open Gdbmi_types
+
+%}
+
+%token Eof
+%token Eq Lsquare Rsquare Lcurly Rcurly Comma Caret
+%token <string> String Id
+%token <int> Num
+
+%start response_eof
+%type <Gdbmi_types.response> response_eof
+
+%%
+
+map_elem:
+  | Id Eq output
+    { ($1, $3) }
+
+output:
+  | String
+    { String $1 }
+  | Lsquare separated_list(Comma, output) Rsquare
+    { Seq $2 }
+  | Lcurly separated_list(Comma, map_elem) Rcurly
+    { Assoc $2 }
+
+response:
+  | Num Caret Id Comma separated_list(Comma, map_elem)
+    { Result ($1, $3, $5) }
+
+response_eof:
+  | response Eof
+    { $1 }
\ No newline at end of file
diff --git a/src/gdbmi_types.ml b/src/gdbmi_types.ml
new file mode 100644
index 00000000..9be54a87
--- /dev/null
+++ b/src/gdbmi_types.ml
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+type output =
+  | Assoc of (string * output) list
+  | Seq of output list
+  | String of string
+
+type response =
+  | Result of int * string * (string * output) list
diff --git a/src/interpreter.ml b/src/interpreter.ml
index dd322369..baa3f240 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -286,6 +286,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
   match e_aux with
   | E_block [] -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown)))
   | E_block [exp] when is_value exp -> return exp
+  | E_block [E_aux (E_block _, _) as exp] -> return exp
   | E_block (exp :: exps) when is_value exp -> wrap (E_block exps)
   | E_block (exp :: exps) ->
      step exp >>= fun exp' -> wrap (E_block (exp' :: exps))
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index b3675263..218ebf22 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -502,7 +502,11 @@ and doc_atomic_exp (E_aux (e_aux, _) as exp) =
      brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; equals; doc_exp exp3])
   | E_vector_update_subrange (exp1, exp2, exp3, exp4) ->
      brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4])
-  | E_internal_value v -> string (Value.string_of_value v (* |> Util.green |> Util.clear *))
+  | E_internal_value v ->
+     if !Interactive.opt_interactive then
+       string (Value.string_of_value v |> Util.green |> Util.clear)
+     else
+       string (Value.string_of_value v)
   | _ -> parens (doc_exp exp)
 and doc_fexps fexps =
   separate_map (comma ^^ space) doc_fexp fexps