From f42e1a8adbf220bd03862bb08ca5103b6e1cde09 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 4 Nov 2019 20:36:17 +0000
Subject: Allow overriding the interpreter effects

This allows read_mem and read_reg effects to be handled by GDB
---
 src/interpreter.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'src/interpreter.ml')

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, []))
-- 
cgit v1.2.3