Merge.

10 files changed, 306 insertions, 177 deletions

diff --git a/src/Makefile-non-opam b/src/Makefile-non-opam
index 01026490..11f510fe 100644
--- a/src/Makefile-non-opam
+++ b/src/Makefile-non-opam
@@ -16,9 +16,11 @@ BITSTRING ?= $(srcdir)/contrib/bitstring
 BATTERIES ?= $(srcdir)/contrib/batteries-included/_build/src
 UINT ?= $(srcdir)/contrib/ocaml-uint/_build/lib
 
+export CAML_LD_LIBRARY_PATH := $(BITSTRING) $(CAML_LD_LIBRARY_PATH)
+
 LEM ?= ~/bitbucket/lem/lem
 LEMLIB ?= ~/bitbucket/lem/ocaml-lib/_build/
-OCAMLFLAGS +=  -I $(LEMLIB)/../ocaml-lib/_build # FIXME
+OCAMLFLAGS +=  -I $(LEMLIB) # FIXME
 
 .PHONY: all sail test clean doc lib power test_power test_idempotence contrib install_elf
 all: sail lib doc
@@ -50,7 +52,10 @@ ELF_LEM_SRC := $(addprefix elf_model/,missing_pervasives.lem show.lem endianness
 vpath _build/%.lem .
 vpath _build/%.cmx .
 
-CAMLP4FLAGS += -I $(srcdir)/contrib/bitstring/
+CAMLP4FLAGS += -nolib 
+CAMLP4FLAGS += -I $(srcdir)/contrib/$(BITSTRING)
+CAMLP4FLAGS += -parser o -parser op -printer p
+CAMLP4FLAGS += unix.cma 
 CAMLP4FLAGS += bitstring.cma 
 CAMLP4FLAGS += bitstring_persistent.cma 
 CAMLP4FLAGS += pa_bitstring.cmo
@@ -63,19 +68,19 @@ ELF_ML_DEPS := $(patsubst %.ml,%.d,$(ELF_ML))
 ELF_CMX := $(patsubst %.ml,%.cmx,$(ELF_ML))
 
 $(ELF_CMX): OCAMLFLAGS += \
--I $(BITSTRING) -pp 'camlp4o $(CAMLP4FLAGS)' \
+-I $(BITSTRING) -pp 'env CAML_LD_LIBRARY_PATH=$(BITSTRING) camlp4o $(CAMLP4FLAGS)' \
 -I $(BATTERIES) \
 -I $(UINT) \
 -I $(srcdir)/elf_model
 
 $(ELF_ML_DEPS): OCAMLFLAGS += \
--I $(BITSTRING) -pp 'camlp4o $(CAMLP4FLAGS)' \
+-I $(BITSTRING) -pp 'env CAML_LD_LIBRARY_PATH=$(BITSTRING) camlp4o $(CAMLP4FLAGS)' \
 -I $(BATTERIES) \
 -I $(UINT) \
 -I $(srcdir)/elf_model
 
 $(ELF_ML_DEPS): %.d: %.ml
-	ocamlfind ocamldep -native $(OCAMLFLAGS) "$<" > "$@" || (rm -f "$@"; false)
+	ocamldep -native $(OCAMLFLAGS) "$<" > "$@" || (rm -f "$@"; false)
 
 ifneq ($(MAKECMDGOALS),clean)
 include $(ELF_ML_DEPS)
@@ -91,10 +96,11 @@ elf_extract.cmxa: OCAMLFLAGS += \
 LEM_CMX :=  $(addprefix $(LEMLIB)/../ocaml-lib/,nat_num.cmx lem.cmx lem_function.cmx lem_list.cmx)
 
 %.cmx: %.ml
-	ocamlfind ocamlopt $(OCAMLFLAGS) -c "$<"
+	echo CAML_LD_LIBRARY_PATH is $$CAML_LD_LIBRARY_PATH 
+	ocamlopt $(OCAMLFLAGS) -c "$<"
 
 elf_model/elf_extract.cmxa: $(ELF_CMX)
-	ocamlfind ocamlopt $(OCAMLFLAGS) -a -o "$@" $+
+	ocamlopt $(OCAMLFLAGS) -a -o "$@" $+
 
 elf: $(ELF_CMX) $(LEM_CMX) elf_model/elf_extract.cmxa
 
diff --git a/src/contrib/checkout.sh b/src/contrib/checkout.sh
index 86c7b68d..6d423e54 100755
--- a/src/contrib/checkout.sh
+++ b/src/contrib/checkout.sh
@@ -6,7 +6,7 @@ test -d batteries-included || (git clone https://github.com/ocaml-batteries-team
 
 test -d bitstring || (git clone https://code.google.com/p/bitstring/ && \
 	cd bitstring && git checkout master)
-(cd bitstring && (test -e config.h || (aclocal && autoreconf && ./configure)) && make srcdir='$top_srcdir' )
+(cd bitstring && (test -e config.h || (aclocal && autoreconf && ./configure)) && make srcdir='$(top_srcdir)' )
 
 # To fix "-fno-defer-pop" build problem on Mac OS, brew install gcc
 # and make sure "gcc" runs the brew version (not clang). Or get ocaml
diff --git a/src/lem_interp/extract.mllib b/src/lem_interp/extract.mllib
index 6230c0e8..ebca3114 100644
--- a/src/lem_interp/extract.mllib
+++ b/src/lem_interp/extract.mllib
@@ -1,9 +1,10 @@
 Interp_ast
+Interp_utilities
+Instruction_extractor
 Interp
 Interp_lib
 Interp_interface
 Interp_inter_imp
-Instruction_extractor
 
 Pretty_interp
 Run_interp
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index 5474566d..d2597740 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -1,29 +1,30 @@
 open import Interp_ast
+open import Interp_utilities
 open import Pervasives
-import Interp
 
-type typ = 
-| Bit
-| Bitvector of maybe integer
-| Other
+type instr_parm_typ = 
+| IBit
+| IBitvector of maybe integer
+| IOther
 
-type instruction = 
-|  Instr of string * list (string * typ) * list base_effect
+type instruction_form = 
+|  Instr_form of string * list (string * instr_parm_typ) * list base_effect
 |  Skipped 
 
-val extract_instructions : string -> string -> defs Interp.tannot -> list instruction
+val extract_instructions : string -> string -> defs tannot -> list instruction_form
 
 let extract_parm (E_aux e (_,tannot)) =
   match e with
     | E_id (Id_aux (Id i) _) ->
       match tannot with
-	| Just(T_id "bit",_,_,_) -> (i,Bit)
+	| Just(T_id "bit",_,_,_) -> (i,IBit)
+	| Just(T_id "bool",_,_,_) -> (i,IBit)
 	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]),_,_,_) ->
-	  (i,Bitvector (Just len))
+	  (i,IBitvector (Just len))
 	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp _; _; T_arg_typ (T_id "bit")]),_,_,_) ->
-	  (i,Bitvector Nothing)
-	| _ -> (i,Other) end
-    | _ -> ("UNKNOWN_PARM",Other)
+	  (i,IBitvector Nothing)
+	| _ -> (i,IOther) end
+    | _ -> ("UNKNOWN_PARM",IOther)
 end
 
 let rec extract_from_decode decoder = 
@@ -32,7 +33,7 @@ let rec extract_from_decode decoder =
     | (FCL_aux (FCL_Funcl _ pat exp) _)::decoder ->
       (match exp with
 	| E_aux (E_app (Id_aux(Id id) _) parms) (_,(Just (_,Tag_ctor,_,_))) ->
-	  Instr id (List.map extract_parm parms) []
+	  Instr_form id (List.map extract_parm parms) []
 	| _ -> Skipped end)::(extract_from_decode decoder)
 end 
 
@@ -49,13 +50,13 @@ let rec extract_effects instrs execute =
   match instrs with
     | [] -> []
     | Skipped::instrs -> Skipped::(extract_effects instrs execute)
-    | (Instr id parms [])::instrs -> 
-      (Instr id parms (extract_effects_of_fcl id execute))::(extract_effects instrs execute)
+    | (Instr_form id parms [])::instrs -> 
+      (Instr_form id parms (extract_effects_of_fcl id execute))::(extract_effects instrs execute)
 end
 
 let extract_instructions decode_name execute_name defs = 
-  let (Just decoder) = Interp.find_function defs (Id_aux (Id decode_name) Unknown) in
-  let (Just executer) = Interp.find_function defs (Id_aux (Id execute_name) Unknown) in
+  let (Just decoder) = find_function defs (Id_aux (Id decode_name) Unknown) in
+  let (Just executer) = find_function defs (Id_aux (Id execute_name) Unknown) in
   let instr_no_effects = extract_from_decode decoder in
   let instructions = extract_effects instr_no_effects executer in
   instructions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 6edebc49..6febc709 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -5,14 +5,11 @@ import List_extra (* For 'nth' and 'head' where we know that they cannot fail *)
 open import String_extra (* for 'show' to convert nat to string) *)
 
 open import Interp_ast
+open import Interp_utilities
 
-type tannot = maybe (t * tag * list nec * effect)
+open import Instruction_extractor
 
-let get_exp_l (E_aux e (l,annot)) = l
-
-val pure : effect
-let pure = Effect_aux(Effect_set []) Unknown
-let unit_t = Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown
+type tannot = Interp_utilities.tannot
 
 val intern_annot : tannot -> tannot
 let intern_annot annot =
@@ -24,38 +21,10 @@ let intern_annot annot =
 
 let val_annot typ = Just(typ,Tag_empty,[],pure)
 
-(* Workaround Lem's inability to scrap my (type classes) boilerplate.
- * Implementing only Eq, and only for literals - hopefully this will
- * be enough, but we should in principle implement ordering for everything in
- * Interp_ast *)
-
-val lit_eq: lit -> lit -> bool
-let lit_eq (L_aux left _) (L_aux right _) =
-   match (left, right) with
-   | (L_unit, L_unit) -> true
-   | (L_zero, L_zero) -> true
-   | (L_one, L_one) -> true
-   | (L_true, L_true) -> true
-   | (L_false, L_false) -> true
-   | (L_num n, L_num m) -> n = m
-   | (L_hex h, L_hex h') -> h = h'
-   | (L_bin b, L_bin b') -> b = b'
-   | (L_undef, L_undef) -> true
-   | (L_string s, L_string s') -> s = s'
-   | (_, _) -> false
-end
-
-instance (Eq lit)
-  let (=) = lit_eq
-  let (<>) n1 n2 = not (lit_eq n1 n2)
-end
-
 (* This is different from OCaml: it will drop elements from the longest list. *)
 let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l')
 let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l')
 
-let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end
-
 type reg_form =
  | Reg of id * tannot
  | SubReg of id * reg_form * index_range
@@ -76,12 +45,6 @@ type value =
  | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *)
  | V_track of value * (list reg_form) (* Used when memory system wants to track what register(s) a value came from *)
 
-let rec list_to_string format sep lst = match lst with 
-  | [] -> ""
-  | [last] -> format last
-  | one::rest -> (format one) ^ sep ^ (list_to_string format sep rest)
-end
-
 let rec string_of_value v = match v with
   | V_boxref nat t -> "$#" ^ (show nat) ^ "$"
   | V_lit (L_aux lit _) -> 
@@ -151,9 +114,17 @@ type lenv = LEnv of nat * env
 let emem = LMem 1 Map.empty
 let eenv = LEnv 1 []
 
+type sub_reg_map = list (id * index_range)
+
 (*top_level is a tuple of 
-  (all definitions, letbound and enum values, register values, Typedef union constructors, sub register mappings, and register aliases) *)
-type top_level = Env of (defs tannot) * env * env * list (id * typ) * list (id * list (id * index_range)) * list (id * (alias_spec tannot))
+  (all definitions,
+   all extracted instructions (where possible),
+   letbound and enum values, 
+   register values, 
+   Typedef union constructors, 
+   sub register mappings, and register aliases) *)
+type top_level = 
+  | Env of (defs tannot) * list instruction_form * env * env * list (id * typ) * list (id * sub_reg_map) * list (id * (alias_spec tannot))
 
 type action = 
  | Read_reg of reg_form * maybe (integer * integer)
@@ -228,36 +199,6 @@ let rec to_aliases (Defs defs) =
       end 
     end
 
-val has_rmem_effect : list base_effect -> bool
-val has_barr_effect : list base_effect -> bool
-val has_wmem_effect : list base_effect -> bool
-let rec has_effect which efcts =
-  match efcts with
-  | [] -> false
-  | (BE_aux e _)::efcts ->
-    match (which,e) with
-    | (BE_rreg,BE_rreg)    -> true 
-    | (BE_wreg,BE_wreg)    -> true 
-    | (BE_rmem,BE_rmem)    -> true 
-    | (BE_wmem,BE_wmem)    -> true 
-    | (BE_barr,BE_barr)    -> true 
-    | (BE_undef,BE_undef)  -> true 
-    | (BE_unspec,BE_unspec) -> true 
-    | (BE_nondet,BE_nondet) -> true 
-    | _ -> has_effect which efcts
-    end 
-  end
-let has_rmem_effect = has_effect BE_rmem
-let has_barr_effect = has_effect BE_barr
-let has_wmem_effect = has_effect BE_wmem
-
-let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
-let get_effects (Typ_aux t _) =
-  match t with
-    | Typ_fn a r (Effect_aux (Effect_set eff) _) -> eff
-    | _ -> []
-  end
-
 val to_data_constructors : defs tannot -> list (id * typ)
 let rec to_data_constructors (Defs defs) =
   match defs with
@@ -760,23 +701,6 @@ let env_to_let mode (LEnv _ env) (E_aux e annot) =
 	           annot
 end
 
-val find_type_def : defs tannot -> id -> maybe (type_def tannot)
-val find_function : defs tannot -> id -> maybe (list (funcl tannot))
-
-let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
-  List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls
-
-let rec find_function (Defs defs) id =
-  match defs with 
-  | [] -> Nothing
-  | def::defs -> 
-    match def with
-    | DEF_fundef f -> match get_funcls id f with
-      | [] -> find_function (Defs defs) id
-      | funcs -> Just funcs end
-    | _ -> find_function (Defs defs) id
-    end end
-
 (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
 val match_pattern : pat tannot -> value -> bool * bool * lenv
 let rec match_pattern (P_aux p _) value_whole =
@@ -1068,7 +992,7 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
   end
 
 and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
-  let (Env defs lets regs ctors subregs aliases) = t_level in 
+  let (Env defs instrs lets regs ctors subregs aliases) = t_level in 
   let (typ,tag,ncs,effect) = match annot with 
     | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -1843,7 +1767,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     end
 
 and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv))) =
-   let (Env defs lets regs ctors subregs aliases) = t_level in
+   let (Env defs instrs lets regs ctors subregs aliases) = t_level in
   let (typ,tag,ncs,ef) = match annot with 
     | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -2154,7 +2078,7 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
 end	
 
 and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
-  let (Env defs lets regs ctors subregs aliases) = t_level in 
+  let (Env defs instrs lets regs ctors subregs aliases) = t_level in 
   let stack = Hole_frame (Id_aux (Id "0") Unknown)
 		          (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
 			  t_level l_env l_mem Top in
@@ -2199,14 +2123,14 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
 			        (l,(intern_annot annot))) t_level l_env l_mem Top), l_mem,l_env) end
 
 let rec to_global_letbinds (Defs defs) t_level =
-  let  (Env defs' lets regs ctors subregs aliases) = t_level in
+  let  (Env defs' instrs lets regs ctors subregs aliases) = t_level in
   match defs with
   | [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, eenv),t_level)
   | def::defs ->
     match def with
     | DEF_val lbind ->
       match interp_letbind <|eager_eval=true; track_values=false;|> t_level eenv emem lbind with
-      | ((Value v,lm,(LEnv _ le)),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs aliases)
+      | ((Value v,lm,(LEnv _ le)),_) -> to_global_letbinds (Defs defs) (Env defs' instrs (lets++le) regs ctors subregs aliases)
       | ((Action a s,lm,le),_) -> 
 	((Error Unknown "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
       | (e,_) -> (e,t_level) end
@@ -2214,14 +2138,17 @@ let rec to_global_letbinds (Defs defs) t_level =
       match tdef with
       | TD_enum id ns ids _ -> 
         let enum_vals = map (fun eid -> (eid,V_ctor eid (T_id (get_id id)) unitv)) ids in
-        to_global_letbinds (Defs defs) (Env defs' (lets++enum_vals) regs ctors subregs aliases)
+        to_global_letbinds (Defs defs) (Env defs' instrs (lets++enum_vals) regs ctors subregs aliases)
       | _ -> to_global_letbinds (Defs defs) t_level end
     | _ -> to_global_letbinds (Defs defs) t_level
     end
   end
 
+(*TODO Contemplate making decode and execute environment variables instead of these constants*)
 let to_top_env defs = 
-  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
+  let t_level = Env defs (extract_instructions "decode" "execute" defs) 
+                    [] (* empty letbind and enum values, call below will fill in any *) 
+		    (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
   let (o,t_level) = to_global_letbinds defs t_level in
   match o with
     | (Value _,_,_) -> (Nothing,t_level)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 14a286cb..19d41f8c 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -1,5 +1,6 @@
 import Interp
 import Interp_lib
+import Instruction_extractor
 open import Interp_ast
 open import Interp_interface
 open import Pervasives
@@ -27,7 +28,7 @@ end
 		   
 let intern_value v = match v with
   | Bitvector bs inc fst   -> Interp.V_vector fst inc  (to_bits bs)
-  | Bytevector bys inc fst -> Interp.V_vector fst inc 
+  | Bytevector bys -> Interp.V_vector 0 true 
     (to_bits (List.reverse
 		(List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys))))
   | Unknown -> Interp.V_unknown
@@ -40,18 +41,33 @@ let extern_reg r slice = match (r,slice) with
   | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> Reg_field x y (i,i)
 end
 
-let extern_value mode for_mem v = match v with
+let rec extern_value mode for_mem v = match v with
+  | Interp.V_track v regs -> 
+    let (external_v,_) = extern_value mode for_mem v in
+    (external_v,
+     if (for_mem && mode.Interp.track_values)
+     then (Just (List.map (fun r -> extern_reg r Nothing) regs))
+     else Nothing)
   | Interp.V_vector fst inc bits ->
     if for_mem 
-    then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, Nothing)
+    then (Bytevector (List.reverse (to_bytes (from_bits bits))), Nothing)
     else (Bitvector (from_bits bits) inc fst, Nothing)
-  | Interp.V_track (Interp.V_vector fst inc bits) regs -> 
+  | Interp.V_lit (L_aux L_zero _) -> 
     if for_mem
-    then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, 
-          if (mode.Interp.track_values) 
-          then (Just (List.map (fun r -> extern_reg r Nothing) regs))
-          else Nothing)
-    else (Bitvector (from_bits bits) inc fst, Nothing)
+    then (Bytevector [0],Nothing)
+    else (Bitvector [false] true 0, Nothing)
+  | Interp.V_lit (L_aux L_false _) ->
+    if for_mem
+    then (Bytevector [0],Nothing)
+    else (Bitvector [false] true 0, Nothing)
+  | Interp.V_lit (L_aux L_one _) -> 
+    if for_mem
+    then (Bytevector [1],Nothing)
+    else (Bitvector [true] true 0, Nothing)
+  | Interp.V_lit (L_aux L_true _) ->
+    if for_mem
+    then (Bytevector [1],Nothing)
+    else (Bitvector [true] true 0, Nothing)
   | _ -> (Unknown,Nothing)
 end
 
@@ -81,17 +97,55 @@ let memory_functions =
 		 match length with
 		   | Interp.V_lit (L_aux (L_num len) _) ->
 		     let (v,regs) = extern_value mode true location in
-		     (v,len,regs) end end)));
+		     (v,len,regs) 
+		   | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+		     let (v,loc_regs) = extern_value mode true location in
+		     match loc_regs with
+		       | Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
+		       | Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
+	      end end end)));
+    ("MEMr_reserve", (Just(Read_reserve),Nothing,
+		      (fun mode v -> match v with
+			| Interp.V_tuple [location;length] ->
+			  match length with
+			    | Interp.V_lit (L_aux (L_num len) _) ->
+			      let (v,regs) = extern_value mode true location in
+			      (v,len,regs) 
+			    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+			      let (v,loc_regs) = extern_value mode true location in
+			      match loc_regs with
+				| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
+				| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
+		       end end end)));		      
     ("MEMw", (Nothing, Just(Write_plain), 
 	      (fun mode v -> match v with
 		| Interp.V_tuple [location;length] ->
 		  match length with
 		    | Interp.V_lit (L_aux (L_num len) _) ->
 		      let (v,regs) = extern_value mode true location in
-		      (v,len,regs) end end)));
+		      (v,len,regs)
+		    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+		      let (v,loc_regs) = extern_value mode true location in
+		      match loc_regs with
+			| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
+			| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
+	       end end end)));
+    ("MEMw_conditional", (Nothing, Just(Write_conditional), 
+	      (fun mode v -> match v with
+		| Interp.V_tuple [location;length] ->
+		  match length with
+		    | Interp.V_lit (L_aux (L_num len) _) ->
+		      let (v,regs) = extern_value mode true location in
+		      (v,len,regs)
+		    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+		      let (v,loc_regs) = extern_value mode true location in
+		      match loc_regs with
+			| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
+			| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
+	      end end end)));
   ]
 
-let rec interp_to_value_helper thunk = 
+let rec interp_to_value_helper arg instr thunk = 
   match thunk() with
     | Interp.Value value -> (Just value,Nothing)
     | Interp.Error l msg -> (Nothing, Just (Internal_error msg))
@@ -99,20 +153,36 @@ let rec interp_to_value_helper thunk =
       match List.lookup i external_functions with
 	| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
 	| Just f  -> 
-          interp_to_value_helper (fun _ -> Interp.resume (make_mode true false) stack (Just (f value)))
+          interp_to_value_helper arg instr (fun _ -> Interp.resume (make_mode true false) stack (Just (f value)))
       end 
     | Interp.Action (Interp.Exit (E_aux e _)) _ ->
       match e with
-	| E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just Unsupported_instruction_error)
-	| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just Not_an_instruction_error)
+	| E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error instr))
+	| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just (Not_an_instruction_error arg))
       end 
     | _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
 end
 
+let rec find_instruction i = function
+  | [] -> Nothing
+  | Skipped::instrs -> find_instruction i instrs
+  | ((Instruction_extractor.Instr_form name parms effects) as instr)::instrs ->
+      if i = name
+      then Just instr
+      else find_instruction i instrs
+end
+
+let migrate_typ = function
+  | Instruction_extractor.IBit -> Bit
+  | Instruction_extractor.IBitvector len -> Bvector len
+  | Instruction_extractor.IOther -> Other
+end
+
 let decode_to_istate top_level value = 
   let mode = make_mode true false in
   let (arg,_) = Interp.to_exp mode Interp.eenv (intern_value value) in
-  let (instr_decoded,error) = interp_to_value_helper 
+  let (Interp.Env _ instructions _ _ _ _ _) = top_level in
+  let (instr_decoded,error) = interp_to_value_helper value ("",[],[])
     (fun _ -> Interp.resume 
       (make_mode true false) 
       (Interp.Thunk_frame 
@@ -120,8 +190,18 @@ let decode_to_istate top_level value =
 	 top_level Interp.eenv Interp.emem Interp.Top) Nothing) in
   match (instr_decoded,error) with
     | (Just instr, _) -> 
+      let instr_external = match instr with
+	| Interp.V_ctor (Id_aux (Id i) _) _ parm ->
+	  match (find_instruction i instructions) with
+	    | Just(Instruction_extractor.Instr_form name parms effects) -> 
+	      match (parm,parms) with
+		| (Interp.V_lit (L_aux L_unit _),[]) -> (name, [], effects)
+		| (value,[(p_name,ie_typ)]) -> (name, [(p_name,(migrate_typ ie_typ),fst(extern_value mode false value))], effects)
+		| (Interp.V_tuple vals,parms) -> 
+		  (name, (Interp.map2 (fun value (p_name,ie_typ) -> (p_name,(migrate_typ ie_typ),fst(extern_value mode false value))) vals parms), effects)
+          end end end in 
       let (arg,_) = Interp.to_exp mode Interp.eenv instr in
-      let (instr_decoded,error) = interp_to_value_helper
+      let (instr_decoded,error) = interp_to_value_helper value instr_external
 	(fun _ -> Interp.resume 
 	 (make_mode true false) 
 	 (Interp.Thunk_frame 
@@ -130,12 +210,13 @@ let decode_to_istate top_level value =
       match (instr_decoded,error) with
 	| (Just instr,_) ->
 	  let (arg,_) = Interp.to_exp mode Interp.eenv instr in
-	  Instr (Interp.Thunk_frame
+	  Instr instr_external
+	    (Interp.Thunk_frame
 		   (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
 		   top_level Interp.eenv Interp.emem Interp.Top)
-	| (Nothing, Just err) -> err
+	| (Nothing, Just err) -> Decode_error err
       end 
-    | (Nothing, Just err) -> err
+    | (Nothing, Just err) -> Decode_error err
 end
 
 let rec interp_to_outcome mode thunk = 
@@ -163,8 +244,8 @@ let rec interp_to_outcome mode thunk =
       match List.lookup i memory_functions with
       | (Just (_,Just write_k,f)) -> 
         let (location, length, tracking) = (f mode loc_val) in
-        let (value, val_tracking) = (extern_value mode true write_val) in
-        Write_mem write_k location length tracking value val_tracking (fun b -> next_state) 
+        let (value, v_tracking) = (extern_value mode true write_val) in
+        Write_mem write_k location length tracking value v_tracking (fun b -> next_state) 
       | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
       end 
     | Interp.Barrier (Id_aux (Id i) _) lval ->
@@ -202,8 +283,8 @@ let rec ie_loop mode i_state =
       (E_write_reg reg value)::(ie_loop mode i_state)
     | Read_mem read_k loc length tracking i_state_fun ->
       (E_read_mem read_k loc length tracking)::(ie_loop mode (i_state_fun Unknown))
-    | Write_mem write_k loc length l_track value v_track i_state_fun ->
-      (E_write_mem write_k loc length l_track value v_track)::(ie_loop mode (i_state_fun true))
+    | Write_mem write_k loc length tracking value v_tracking i_state_fun ->
+      (E_write_mem write_k loc length tracking value v_tracking)::(ie_loop mode (i_state_fun true))
     | Internal _ _ next -> (ie_loop mode next)
      end ;;
   
@@ -222,9 +303,9 @@ let rec rr_ie_loop mode i_state =
     | Read_mem read_k loc length tracking i_state_fun ->
       let (events,outcome) = (rr_ie_loop mode (i_state_fun Unknown)) in 
       (((E_read_mem read_k loc length tracking)::events),outcome)
-    | Write_mem write_k loc length l_track value v_track i_state_fun ->
+    | Write_mem write_k loc length tracking value v_tracking i_state_fun ->
       let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in
-      (((E_write_mem write_k loc length l_track value v_track)::events),outcome)
+      (((E_write_mem write_k loc length tracking value v_tracking)::events),outcome)
     | Internal _ _ next -> (rr_ie_loop mode next)
      end ;;
 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 9f967b1e..40c34480 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -1,4 +1,5 @@
 import Interp
+open import Interp_ast
 open import Pervasives
 open import Num
 
@@ -22,7 +23,7 @@ type value =
   some special registers, with no clear mapping to bits. Should
   we permit Record of (string * Bitvector) values as well?
 *)
-| Bytevector of list word8 * bool * integer (* For memory accesses : see above *)
+| Bytevector of list word8 (* For memory accesses *)
 | Unknown
 (*To add: an abstract value representing an unknown but named memory address?*)
 
@@ -35,7 +36,8 @@ type reg_name =
 | Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *)
 
 type outcome =
-(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values *)
+(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values,
+   integer is size to read, followed by registers that were used in computing that size *)
 | Read_mem of read_kind * value * integer * maybe (list reg_name) *  (value -> instruction_state)
 (* Request to write memory, first value and dependent registers is location, second is the value to write *)
 | Write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
@@ -49,16 +51,19 @@ type outcome =
 | Nondet_choice of list instruction_state * instruction_state
 (* Stop for incremental stepping, function can be used to display function call data *)
 | Internal of maybe string * maybe (unit -> string) * instruction_state
+(* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally provide a handler *)
+| Escape of maybe instruction_state
 | Done
 | Error of string
 
 type event = 
-| E_read_mem of read_kind * value * integer * maybe (list reg_name) 
+| E_read_mem of read_kind * value * integer * maybe (list reg_name)
 | E_write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name)
 | E_barrier of barrier_kind
 | E_read_reg of reg_name
 | E_write_reg of reg_name * value
 | E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*)
+(*should there be a representation for escape down here?*)
 (*To discuss: Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
 
 (* Functions to build up the initial state for interpretation *)
@@ -66,12 +71,27 @@ val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come
 val initial_instruction_state : context -> string -> list value -> instruction_state 
   (* string is a function name, list of value are the parameters to that function *)
 
-type i_state_or_error =
-  | Instr of instruction_state
-  | Unsupported_instruction_error
-  | Not_an_instruction_error
+(*Type representint the constructor parameters in instruction, other is a type not representable externally*)
+type instr_parm_typ = 
+  | Bit (*A single bit, represented as a one element Bitvector as a value*)
+  | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
+  | Bvector of maybe integer (* A bitvector type, with length when statically known *)
+
+(*A representation of the AST node for each instruction in the spec, with concrete values from this call, and the potential static effects from the funcl clause for this instruction 
+Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
+*)
+type instruction = (string * list (string * instr_parm_typ * value) * list base_effect)
+
+type decode_error = 
+  | Unsupported_instruction_error of instruction
+  | Not_an_instruction_error of value
   | Internal_error of string
 
+type i_state_or_error =
+  | Instr of instruction * instruction_state
+  | Decode_error of decode_error
+
+
 (*Function to decode an instruction and build the state to run it*)
 val decode_to_istate : context -> value -> i_state_or_error
 
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
new file mode 100644
index 00000000..37ed814d
--- /dev/null
+++ b/src/lem_interp/interp_utilities.lem
@@ -0,0 +1,93 @@
+open import Interp_ast
+open import Pervasives
+
+type tannot = maybe (t * tag * list nec * effect)
+
+let get_exp_l (E_aux e (l,annot)) = l
+
+val pure : effect
+let pure = Effect_aux(Effect_set []) Unknown
+let unit_t = Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown
+
+(* Workaround Lem's inability to scrap my (type classes) boilerplate.
+ * Implementing only Eq, and only for literals - hopefully this will
+ * be enough, but we should in principle implement ordering for everything in
+ * Interp_ast *)
+
+val lit_eq: lit -> lit -> bool
+let lit_eq (L_aux left _) (L_aux right _) =
+   match (left, right) with
+   | (L_unit, L_unit) -> true
+   | (L_zero, L_zero) -> true
+   | (L_one, L_one) -> true
+   | (L_true, L_true) -> true
+   | (L_false, L_false) -> true
+   | (L_num n, L_num m) -> n = m
+   | (L_hex h, L_hex h') -> h = h'
+   | (L_bin b, L_bin b') -> b = b'
+   | (L_undef, L_undef) -> true
+   | (L_string s, L_string s') -> s = s'
+   | (_, _) -> false
+end
+
+instance (Eq lit)
+  let (=) = lit_eq
+  let (<>) n1 n2 = not (lit_eq n1 n2)
+end
+
+let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end
+
+let rec list_to_string format sep lst = match lst with 
+  | [] -> ""
+  | [last] -> format last
+  | one::rest -> (format one) ^ sep ^ (list_to_string format sep rest)
+end 
+
+val has_rmem_effect : list base_effect -> bool
+val has_barr_effect : list base_effect -> bool
+val has_wmem_effect : list base_effect -> bool
+let rec has_effect which efcts =
+  match efcts with
+  | [] -> false
+  | (BE_aux e _)::efcts ->
+    match (which,e) with
+    | (BE_rreg,BE_rreg)    -> true 
+    | (BE_wreg,BE_wreg)    -> true 
+    | (BE_rmem,BE_rmem)    -> true 
+    | (BE_wmem,BE_wmem)    -> true 
+    | (BE_barr,BE_barr)    -> true 
+    | (BE_undef,BE_undef)  -> true 
+    | (BE_unspec,BE_unspec) -> true 
+    | (BE_nondet,BE_nondet) -> true 
+    | _ -> has_effect which efcts
+    end 
+  end
+let has_rmem_effect = has_effect BE_rmem
+let has_barr_effect = has_effect BE_barr
+let has_wmem_effect = has_effect BE_wmem
+
+let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
+let get_effects (Typ_aux t _) =
+  match t with
+    | Typ_fn a r (Effect_aux (Effect_set eff) _) -> eff
+    | _ -> []
+  end
+
+val find_type_def : defs tannot -> id -> maybe (type_def tannot)
+val find_function : defs tannot -> id -> maybe (list (funcl tannot))
+
+let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
+  List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls
+
+let rec find_function (Defs defs) id =
+  match defs with 
+  | [] -> Nothing
+  | def::defs -> 
+    match def with
+    | DEF_fundef f -> match get_funcls id f with
+      | [] -> find_function (Defs defs) id
+      | funcs -> Just funcs end
+    | _ -> find_function (Defs defs) id
+    end end
+
+
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 37c73d66..a54dc6e1 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -49,7 +49,7 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
 
 let val_to_string v = match v with
   | Bitvector(bools, _, _) -> "0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
-  | Bytevector(words, _, _)->
+  | Bytevector words->
     "0x" ^ (String.concat ""
 	    (List.map (function 
 	      | 10 -> "A"
@@ -291,7 +291,7 @@ let rec perform_action ((reg, mem) as env) = function
      perform_action env (Write_mem (id, n, slice, V_vector(zero_big_int, true, [value])))
  (* extern functions *)
  | Call_extern (name, arg) -> eval_external name arg, env
- | Step _ | Nondet _ | Exit _ -> unit_lit, env
+ | Interp.Step _ | Nondet _ | Exit _ -> unit_lit, env
  | _ -> assert false
 ;;
 
@@ -406,7 +406,7 @@ let run
       | Call_extern (f, arg) ->
           show "call_lib" (sprintf "%s(%s)" f (val_to_string_internal arg)) right (val_to_string_internal return);
           step (),env',s
-      | Step _ ->
+      | Interp.Step _ ->
           assert (return = unit_lit);
           show "breakpoint" "" "" "";
           step ~force:true (),env',s
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index fbb06eed..f8c05085 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -50,7 +50,7 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
 let val_to_string v = match v with
   | Bitvector(bools, inc, fst)-> let l = List.length bools in
     (string_of_int l) ^ " bits -- 0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
-  | Bytevector(words, inc, fst)->
+  | Bytevector words ->
     let l = List.length words in
     (string_of_int l) ^ " bytes --" ^
       (String.concat ""
@@ -191,7 +191,7 @@ module Mem = struct
     add key valu m
 
   let to_string loc v =
-    sprintf "[%s] -> %x" (val_to_string (Bytevector(loc, true, zero_big_int))) v
+    sprintf "[%s] -> %x" (val_to_string (Bytevector loc)) v
 end ;;
 
 let rec slice bitvector (start,stop) = 
@@ -202,8 +202,8 @@ let rec slice bitvector (start,stop) =
                  inc,
                  (if inc then zero_big_int else (add_big_int (sub_big_int stop start) unit_big_int)))
                 
-    | Bytevector(bytes, inc, fst) -> 
-      Bytevector((Interp.from_n_to_n start stop bytes),inc,fst) (*This is wrong, need to explode and re-encode, but maybe never happens?*)
+    | Bytevector bytes -> 
+      Bytevector((Interp.from_n_to_n start stop bytes)) (*This is wrong, need to explode and re-encode, but maybe never happens?*)
     | Unknown0 -> Unknown0
 ;;
 
@@ -245,12 +245,12 @@ let fupdate_slice original e (start,stop) =
                                     (if inc then (sub_big_int start fst) else (sub_big_int fst start))
                                     (if inc then (sub_big_int stop fst) else (sub_big_int fst stop)) bs bools), inc, fst)
       | _ -> Unknown0)
-    | Bytevector(bytes,inc,fst) -> (*Can this happen?*)
+    | Bytevector bytes -> (*Can this happen?*)
       (match e with
-      | Bytevector([byte],_,_) -> 
-        Bytevector((list_update zero_big_int start stop byte bytes),inc,fst)
-      | Bytevector(bs,_,_) ->
-        Bytevector((list_update_list zero_big_int start stop bs bytes),inc,fst)
+      | Bytevector [byte] -> 
+        Bytevector (list_update zero_big_int start stop byte bytes)
+      | Bytevector bs ->
+        Bytevector (list_update_list zero_big_int start stop bs bytes)
       | _ -> Unknown0)
     | Unknown0 -> Unknown0
 ;;
@@ -272,10 +272,10 @@ let rec format_events = function
     "     Failed with message : " ^ s ^ "\n"
   | (E_error s)::events ->
     "     Failed with message : " ^ s ^ " but continued on erroneously\n"
-  | (E_read_mem(read_kind, location, length, dep))::events ->
+  | (E_read_mem(read_kind, location, length, tracking))::events ->
     "     Read_mem at " ^ (val_to_string location) ^ " for " ^ (string_of_big_int length) ^ " bytes \n" ^
     (format_events events)
-  | (E_write_mem(write_kind,location, length, dep, value, vdep))::events ->
+  | (E_write_mem(write_kind,location, length, tracking, value, v_tracking))::events ->
     "     Write_mem at " ^ (val_to_string location) ^ " writing " ^ (val_to_string value) ^ " across " ^ (string_of_big_int length) ^ " bytes\n" ^
     (format_events events)
   | ((E_barrier b_kind)::events) ->
@@ -306,13 +306,13 @@ let rec perform_action ((reg, mem) as env) = function
    let old_val = Reg.find id reg in
    let new_val = fupdate_slice old_val value (combine_slices range mini_range) in
    (None,(Reg.add id new_val reg,mem))
- | Read_mem0(_,Bytevector(location,_,_), length, _,_) ->
+ | Read_mem0(_,(Bytevector location), length, _,_) ->
    let rec reading location length = 
      if eq_big_int length zero_big_int 
      then []
      else (Mem.find location mem)::(reading (increment location) (sub_big_int length unit_big_int)) in
-   (Some (Bytevector((List.rev (reading location length)), true, zero_big_int)), env) (*TODO: how to get order back here? *)
- | Write_mem0(_,(Bytevector(location,_,_)), length, _, (Bytevector(bytes,_,_)),_,_) ->
+   (Some (Bytevector((List.rev (reading location length)))), env)
+ | Write_mem0(_,(Bytevector location), length, _, (Bytevector bytes),_,_) ->
    let rec writing location length bytes mem = 
      if eq_big_int length zero_big_int
      then mem
@@ -440,20 +440,20 @@ let run
 	| Write_reg0(reg,value,next) ->
 	  show "write_reg" (reg_name_to_string reg) left (val_to_string value);
 	  (step next, env', next)
-	| Read_mem0(kind, location, length, dependencies, next_thunk) ->
+	| Read_mem0(kind, location, length, tracking, next_thunk) ->
 	  (match return with
 	    | Some(value) -> 
 	      show "read_mem" (val_to_string location) right (val_to_string value);
-              (match dependencies with
+              (match tracking with
               | None -> ()
               | Some(deps) ->
                 show "read_mem address depended on" (dependencies_to_string deps) "" "");
 	      let next = next_thunk value in
 	      (step next, env', next)
 	    | None -> assert false)
-	| Write_mem0(kind,location, length, dependencies, value, val_dependencies, next_thunk) ->
+	| Write_mem0(kind,location, length, tracking, value, v_tracking, next_thunk) ->
 	  show "write_mem" (val_to_string location) left (val_to_string value);
-          (match (dependencies,val_dependencies) with
+          (match (tracking,v_tracking) with
           | (None,None) -> ();
           | (Some(deps),None) ->
             show "write_mem address depended on" (dependencies_to_string deps) "" "";