Allow overriding the interpreter effects

This allows read_mem and read_reg effects to be handled by GDB

7 files changed, 113 insertions, 23 deletions

diff --git a/src/gdbmi.ml b/src/gdbmi.ml
index 14b4d4c3..bcefb002 100644
--- a/src/gdbmi.ml
+++ b/src/gdbmi.ml
@@ -48,6 +48,8 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+open Ast
+open Ast_util
 open Printf
 open Gdbmi_types
 
@@ -107,12 +109,82 @@ let send_regular session cmd =
      flush stdin;
      ignore (wait_for_gdb stdout)
 
-let gdb_sync session ast =
+let synced_registers = ref []
+
+let gdb_sync session =
   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 names = match gdb_register_names with
+    | Result (_, "done", output) ->
+       List.assoc "register-names" output |> gdb_seq |> List.map gdb_string
+    | _ -> failwith "GDB could not get register names"
+  in
+  let values = match gdb_register_values with
+    | Result (_, "done", output) ->
+       List.assoc "register-values" output
+       |> gdb_seq
+       |> List.map gdb_assoc
+       |> List.map (List.assoc "value")
+       |> List.map gdb_string
+    | _ -> failwith "GDB could not get register names"
+  in
+  synced_registers := List.combine names values
+
+let gdb_list_registers session =
+  gdb_sync session;
+  List.iter (fun (name, value) ->
+      print_endline (sprintf "%s: %s" name value)
+    ) !synced_registers
+
+let gdb_read_mem session addr data_size =
+  let open Value in
+  let cmd = sprintf "data-read-memory %s x 1 1 %i" (Sail_lib.string_of_bits addr) (Big_int.to_int data_size) in
+  (* An example response looks something like:
+
+     7^done,addr="0x0000000040009e64",nr-bytes="4",total-bytes="4",next-row="0x0000000040009e68",
+     prev-row="0x0000000040009e60",next-page="0x0000000040009e68",prev-page="0x0000000040009e60",
+     memory=[{addr="0x0000000040009e64",data=["0x03","0xfc","0x5a","0xd3"]}]
+     *)
+  match parse_gdb_response (send_sync session cmd) with
+  | Result (_, "done", output) ->
+     List.assoc "memory" output |> gdb_seq
+     |> List.hd |> gdb_assoc
+     |> List.assoc "data" |> gdb_seq
+     |> List.rev_map (fun byte -> Sail_lib.byte_of_int (int_of_string (gdb_string byte)))
+     |> List.concat
+
+  | _ -> failwith "Unexpected response from GDB"
+
+let value_gdb_read_ram session =
+  let open Value in
+  function
+  | [addr_size; data_size; _; addr] ->
+     mk_vector (gdb_read_mem session (coerce_bv addr) (coerce_int data_size))
+
+  | _ -> failwith "gdb_read_ram"
+
+let gdb_effect_interp session state eff =
+  let open Value in
+  let open Interpreter in
+  let lstate, gstate = state in
+  match eff with
+  | Read_mem (rk, addr, len, cont) ->
+     let result = mk_vector (gdb_read_mem session (coerce_bv addr) (coerce_int len)) in
+     cont result state
+  | Read_reg (name, cont) ->
+     begin match List.assoc_opt name !synced_registers with
+     | Some value ->
+        let value = mk_vector (Sail_lib.to_bits' (64, Big_int.of_string value)) in
+        cont value state
+     | None ->
+        cont (Bindings.find (mk_id name) gstate.registers) state
+     end
+  | _ ->
+     failwith "Unsupported in GDB state"
+
+let gdb_hooks session =
+  Value.add_primop "read_ram" (value_gdb_read_ram session);
+  Interpreter.set_effect_interp (gdb_effect_interp session)
 
 let () =
   let open Interactive in
@@ -159,7 +231,17 @@ let () =
   register_command
     ~name:"gdb_sync"
     ~help:"Sync sail registers with GDB"
-    (Action (fun () -> gdb_sync !session !ast));
+    (Action (fun () -> gdb_sync !session));
+
+  register_command
+    ~name:"gdb_list_registers"
+    ~help:"Sync sail registers with GDB and list them"
+    (Action (fun () -> gdb_list_registers !session));
+
+  register_command
+    ~name:"gdb_hooks"
+    ~help:"Make reading and writing memory go via GDB"
+    (Action (fun () -> gdb_hooks !session));
 
   (ArgString ("symbol_file", fun file -> Action (fun () ->
     send_regular !session ("symbol-file " ^ file)
diff --git a/src/gdbmi_types.ml b/src/gdbmi_types.ml
index 9be54a87..13877a83 100644
--- a/src/gdbmi_types.ml
+++ b/src/gdbmi_types.ml
@@ -53,5 +53,17 @@ type output =
   | Seq of output list
   | String of string
 
+let gdb_seq = function
+  | Seq xs -> xs
+  | _ -> failwith "Expected GDB sequence"
+
+let gdb_string = function
+  | String xs -> xs
+  | _ -> failwith "Expected GDB string"
+
+let gdb_assoc = function
+  | Assoc xs -> xs
+  | _ -> failwith "Expected GDB associative list"
+
 type response =
   | Result of int * string * (string * output) list
diff --git a/src/interactive.ml b/src/interactive.ml
index 0fad3caf..2cca944c 100644
--- a/src/interactive.ml
+++ b/src/interactive.ml
@@ -51,7 +51,7 @@
 open Ast
 open Ast_util
 open Printf
-   
+
 let opt_interactive = ref false
 let opt_emacs_mode = ref false
 let opt_suppress_banner = ref false
@@ -72,7 +72,7 @@ type action =
   | Action of (unit -> unit)
 
 let commands = ref []
-            
+
 let reflect_typ action =
   let open Type_check in
   let rec arg_typs = function
diff --git a/src/interpreter.ml b/src/interpreter.ml
index baa3f240..4c048c09 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -203,7 +203,6 @@ 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 read_mem rk addr len : value monad =
   Yield (Read_mem (rk, addr, len, (fun v -> Pure v)))
 
@@ -826,7 +825,8 @@ let rec eval_frame' = function
      | Yield (Get_primop (name, cont)), _ ->
         begin
           try
-            let op = StringMap.find name gstate.primops in
+            (* If we are in the toplevel interactive interpreter allow the set of primops to be changed dynamically *)
+            let op = StringMap.find name (if !Interactive.opt_interactive then !Value.primops else 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))
@@ -927,8 +927,9 @@ let default_effect_interp state eff =
          failwith ("Register write disallowed by allow_registers setting: " ^ name)
      end
 
+let effect_interp = ref default_effect_interp
 
-
+let set_effect_interp interp = effect_interp := interp
 
 let rec run_frame frame =
   match frame with
@@ -939,7 +940,7 @@ let rec run_frame frame =
   | Break frame ->
      run_frame (eval_frame frame)
   | Effect_request (out, state, stack, eff) ->
-     run_frame (default_effect_interp state eff)
+     run_frame (!effect_interp state eff)
 
 let eval_exp state exp =
   run_frame (Step (lazy "", state, return exp, []))
diff --git a/src/isail.ml b/src/isail.ml
index 138d8d31..01ffe33f 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -175,7 +175,7 @@ let setup_sail_scripting () =
       ) !commands;
     sail_scripting_primops_once := false
   )
- 
+
 let print_program () =
   match !current_mode with
   | Normal | Emacs -> ()
@@ -215,7 +215,7 @@ let rec run () =
        | Effect_request (out, state, stack, eff) ->
           begin
             try
-              current_mode := Evaluation (Interpreter.default_effect_interp state eff)
+              current_mode := Evaluation (!Interpreter.effect_interp state eff)
             with
             | Failure str -> print_endline str; current_mode := Normal
           end;
@@ -250,7 +250,7 @@ let rec run_steps n =
        | Effect_request (out, state, stack, eff) ->
           begin
             try
-              current_mode := Evaluation (Interpreter.default_effect_interp state eff)
+              current_mode := Evaluation (!Interpreter.effect_interp state eff)
             with
             | Failure str -> print_endline str; current_mode := Normal
           end;
@@ -716,7 +716,7 @@ let handle_input' input =
            begin
              try
                interactive_state := state;
-               current_mode := Evaluation (Interpreter.default_effect_interp state eff);
+               current_mode := Evaluation (!Interpreter.effect_interp state eff);
                print_program ()
              with
              | Failure str -> print_endline str; current_mode := Normal
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 164bcefa..8251f9b4 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -274,9 +274,7 @@ let rec replicate_bits (bits, n) =
 
 let identity x = x
 
-
-
-(* 
+(*
 Returns list of n bits of integer m starting from offset o >= 0 (bits numbered from least significant). 
 Uses twos-complement representation for m<0 and pads most significant bits in sign-extended way. 
 Most significant bit is head of returned list.
@@ -529,7 +527,7 @@ let fast_read_ram (data_size, addr) =
   !vector
 
 let tag_ram = (ref Mem.empty : (bool Mem.t) ref);;
-  
+
 let write_tag_bool (addr, tag) =
   let addri = uint addr in
   tag_ram := Mem.add addri tag !tag_ram
@@ -551,7 +549,6 @@ let lor_int (n, m) = Big_int.bitwise_or n m
 let land_int (n, m) = Big_int.bitwise_and n m
 let lxor_int (n, m) = Big_int.bitwise_xor n m
 
-
 let debug (str1, n, str2, v) = prerr_endline (str1 ^ Big_int.to_string n ^ str2 ^ string_of_bits v)
 
 let eq_string (str1, str2) = String.compare str1 str2 == 0
diff --git a/src/value.ml b/src/value.ml
index 751c10d7..69023bc3 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -486,7 +486,7 @@ let value_undefined_vector = function
 let value_undefined_bitvector = function
   | [v] -> V_vector (Sail_lib.undefined_vector (coerce_int v, V_bit (Sail_lib.B0)))
   | _ -> failwith "value undefined_bitvector"
-       
+
 let value_read_ram = function
   | [v1; v2; v3; v4] -> mk_vector (Sail_lib.read_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4))
   | _ -> failwith "value read_ram"
@@ -751,5 +751,3 @@ let primops = ref
 
 let add_primop name impl =
   primops := StringMap.add name impl !primops
-  
-