summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-11-29 19:29:48 +0000
committerAlasdair Armstrong2017-11-29 19:29:48 +0000
commit16c475fff5b1942eacc4f399ff14a0bca0c9cec2 (patch)
tree78931fdee36cbb9cde2001853aa016cf8cc67110 /src/lem_interp
parent636d81ee6afba69b7a2516e8149eeef3691cd67e (diff)
Better lem_ast tagging and interpreter tweaks
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp_inter_imp.lem3
-rw-r--r--src/lem_interp/run_interp_model.ml8
2 files changed, 6 insertions, 5 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 68f82ccb..e9533a2a 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -440,7 +440,8 @@ let rec interp_to_value_helper debug arg ivh_mode err_str instr direction regist
(Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
| (Interp.Action (Interp.Write_memv_tagged _ _ _ _) _,_,_) ->
(Ivh_error (Interp_interface.Internal_error ("Write memory value tagged request in a " ^ errk_str)), events_out)
- | _ -> (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str)), events_out)
+ | (outcome, _, _) ->
+ (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str ^ " " ^ Interp.string_of_outcome outcome)), events_out)
end
let call_external_functions direction outcome =
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 6978aeb9..81f0a5fd 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -433,7 +433,7 @@ let run
(List.combine nondets (List.map (fun _ -> Random.bits ()) nondets)) in
show "nondeterministic evaluation begun" "" "" "";
let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') ->
- loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) next))
+ loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies true) next))
choose_order (false,mode,!track_dependencies,env'); in
show "nondeterministic evaluation ended" "" "" "";
(step next,env',next)
@@ -445,7 +445,7 @@ let run
else begin
show "undefined triggered a non_det" "" "" "";
let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') ->
- loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) next))
+ loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies true) next))
choose_order (false,mode,!track_dependencies,env'); in
(step i_state,env',i_state) end
| Escape0(Some e,_) ->
@@ -462,11 +462,11 @@ let run
| Write_memv1 _ -> assert false)
(*| _ -> assert false*)
in
- loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies false) next) in
+ loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies true) next) in
let mode = match mode with
| None -> if eager_eval then Run else Step
| Some m -> m in
- let imode = make_mode eager_eval !track_dependencies false in
+ let imode = make_mode eager_eval !track_dependencies true in
let (IState(instr_state,context)) = istate in
let (top_exp,(top_env,top_mem)) = top_frame_exp_state instr_state in
interactf "%s: %s %s\n" (grey name) (blue "evaluate")