From 072f8a43eb471d8e0425370aabc25fbb8d6a2511 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Sat, 4 Oct 2014 17:39:54 +0100
Subject: clarify Step constructor

---
 src/lem_interp/run_interp.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 37c73d66..a9c22b6c 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -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
-- 
cgit v1.2.3


From 4f720a3ed86af52288fe614296678ccb7a4777f6 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Mon, 6 Oct 2014 17:41:42 +0100
Subject: Getting closer with non-opam makefile

---
 src/Makefile-non-opam   | 21 +++++++++++++--------
 src/contrib/checkout.sh |  2 +-
 2 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/src/Makefile-non-opam b/src/Makefile-non-opam
index 6c23c732..df9bf9cb 100644
--- a/src/Makefile-non-opam
+++ b/src/Makefile-non-opam
@@ -5,9 +5,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
@@ -41,8 +43,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 += -I $(srcdir)/contrib/bitstring/_
+CAMLP4FLAGS += -nolib 
+CAMLP4FLAGS += -I $(BITSTRING)
+CAMLP4FLAGS += -parser o -parser op -printer p
+CAMLP4FLAGS += unix.cma 
 CAMLP4FLAGS += bitstring.cma 
 CAMLP4FLAGS += bitstring_persistent.cma 
 CAMLP4FLAGS += pa_bitstring.cmo
@@ -55,19 +59,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 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)
@@ -83,10 +87,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
-- 
cgit v1.2.3


From 9124fe2d2142f2f0a7beb91438d3dbbcb8310fe9 Mon Sep 17 00:00:00 2001
From: Peter Sewell
Date: Tue, 7 Oct 2014 13:50:50 +0100
Subject: comment with suggested i_state_or_error type

---
 src/lem_interp/interp_interface.lem | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 9f967b1e..2051233d 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -72,6 +72,17 @@ type i_state_or_error =
   | Not_an_instruction_error
   | Internal_error of string
 
+(*
+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
 
-- 
cgit v1.2.3


From 8399a028fc78512214075115bcdb29015d211db9 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Tue, 7 Oct 2014 13:53:40 +0100
Subject: Put in type for instruction form for models; remove extra information
 from Bytevectors; add place holder for memory size dependency tracking

---
 src/lem_interp/extract.mllib             |  3 +-
 src/lem_interp/instruction_extractor.lem |  8 +--
 src/lem_interp/interp.lem                | 90 +-------------------------------
 src/lem_interp/interp_inter_imp.lem      | 29 +++++-----
 src/lem_interp/interp_interface.lem      | 32 +++++++++---
 src/lem_interp/run_interp.ml             |  2 +-
 src/lem_interp/run_interp_model.ml       | 32 ++++++------
 7 files changed, 64 insertions(+), 132 deletions(-)

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..e47a5252 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -1,6 +1,6 @@
 open import Interp_ast
+open import Interp_utilities
 open import Pervasives
-import Interp
 
 type typ = 
 | Bit
@@ -11,7 +11,7 @@ type instruction =
 |  Instr of string * list (string * typ) * list base_effect
 |  Skipped 
 
-val extract_instructions : string -> string -> defs Interp.tannot -> list instruction
+val extract_instructions : string -> string -> defs tannot -> list instruction
 
 let extract_parm (E_aux e (_,tannot)) =
   match e with
@@ -54,8 +54,8 @@ let rec 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..a436d652 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -5,14 +5,9 @@ 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)
-
-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 +19,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 +43,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 _) -> 
@@ -228,36 +189,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 +691,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 =
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 14a286cb..a69ea430 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -27,7 +27,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
@@ -43,11 +43,11 @@ end
 let extern_value mode for_mem v = match v with
   | 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 -> 
     if for_mem
-    then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, 
+    then (Bytevector (List.reverse (to_bytes (from_bits bits))), 
           if (mode.Interp.track_values) 
           then (Just (List.map (fun r -> extern_reg r Nothing) regs))
           else Nothing)
@@ -103,7 +103,7 @@ let rec interp_to_value_helper thunk =
       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 "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error ("",[],[])))
 	| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just Not_an_instruction_error)
       end 
     | _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
@@ -133,6 +133,7 @@ let decode_to_istate top_level value =
 	  Instr (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
       end 
     | (Nothing, Just err) -> err
@@ -156,7 +157,7 @@ let rec interp_to_outcome mode thunk =
       match List.lookup i memory_functions with
       | (Just (Just read_k,_,f)) -> 
         let (location, length, tracking) = (f mode value) in
-        Read_mem read_k location length tracking (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
+        Read_mem read_k location tracking length Nothing (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
       | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
       end
     | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
@@ -164,7 +165,7 @@ let rec interp_to_outcome mode thunk =
       | (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) 
+        Write_mem write_k location tracking length Nothing value val_tracking (fun b -> next_state) 
       | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
       end 
     | Interp.Barrier (Id_aux (Id i) _) lval ->
@@ -200,10 +201,10 @@ let rec ie_loop mode i_state =
       (E_read_reg reg)::(ie_loop mode (i_state_fun Unknown))
     | Write_reg reg value 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))
+    | Read_mem read_k loc tracking length ltracking i_state_fun ->
+      (E_read_mem read_k loc tracking length ltracking)::(ie_loop mode (i_state_fun Unknown))
+    | Write_mem write_k loc track length l_track value v_track i_state_fun ->
+      (E_write_mem write_k loc track length l_track value v_track)::(ie_loop mode (i_state_fun true))
     | Internal _ _ next -> (ie_loop mode next)
      end ;;
   
@@ -219,12 +220,12 @@ let rec rr_ie_loop mode i_state =
     | Write_reg reg value i_state->
       let (events,outcome) = (rr_ie_loop mode i_state) in
       (((E_write_reg reg value)::events), outcome)
-    | Read_mem read_k loc length tracking i_state_fun ->
+    | Read_mem read_k loc tracking  length ltracking 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 ->
+      (((E_read_mem read_k loc tracking length ltracking)::events),outcome)
+    | Write_mem write_k loc track length l_track value v_track 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 track length l_track value v_track)::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 2051233d..68e57b47 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,10 +36,11 @@ 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 *)
-| Read_mem of read_kind * value * integer * maybe (list reg_name) *  (value -> instruction_state)
+(* 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 * maybe (list reg_name) * 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)
+| Write_mem of write_kind * value * maybe (list reg_name) * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
 (* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
 (* Request to read register, will track dependency when mode.track_values *)
@@ -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_write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name)
+| E_read_mem of read_kind * value * maybe (list reg_name) * integer * maybe (list reg_name)
+| E_write_mem of write_kind * value * maybe (list reg_name) * 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,9 +71,20 @@ 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 representint the constructor parameters in instruction_form, 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_form = (string * list (string * instr_parm_typ * value) * list base_effect)
+
 type i_state_or_error =
-  | Instr of instruction_state
-  | Unsupported_instruction_error
+  | Instr of instruction_state * instruction_form
+  | Unsupported_instruction_error of instruction_form
   | Not_an_instruction_error
   | Internal_error of string
 
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index a9c22b6c..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"
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index fbb06eed..60258504 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,depl, length, dep))::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,depl, length, dep, value, vdep))::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,7 +440,7 @@ 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, ldeps, length, dependencies, next_thunk) ->
 	  (match return with
 	    | Some(value) -> 
 	      show "read_mem" (val_to_string location) right (val_to_string value);
@@ -451,7 +451,7 @@ let run
 	      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, ldeps, length, dependencies, value, val_dependencies, next_thunk) ->
 	  show "write_mem" (val_to_string location) left (val_to_string value);
           (match (dependencies,val_dependencies) with
           | (None,None) -> ();
-- 
cgit v1.2.3


From 6d15542f8fcd520b5741e733408f37a2fc9e37f8 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Tue, 7 Oct 2014 14:00:20 +0100
Subject: Merge and make real Peter's comment type

---
 src/lem_interp/interp_inter_imp.lem | 18 +++++++++---------
 src/lem_interp/interp_interface.lem | 13 +++----------
 2 files changed, 12 insertions(+), 19 deletions(-)

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index a69ea430..292552f4 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -91,7 +91,7 @@ let memory_functions =
 		      (v,len,regs) end end)));
   ]
 
-let rec interp_to_value_helper thunk = 
+let rec interp_to_value_helper arg thunk = 
   match thunk() with
     | Interp.Value value -> (Just value,Nothing)
     | Interp.Error l msg -> (Nothing, Just (Internal_error msg))
@@ -99,12 +99,12 @@ 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 (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 "no_matching_pattern") _) -> (Nothing,Just (Not_an_instruction_error arg))
       end 
     | _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
 end
@@ -112,7 +112,7 @@ 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 (instr_decoded,error) = interp_to_value_helper value
     (fun _ -> Interp.resume 
       (make_mode true false) 
       (Interp.Thunk_frame 
@@ -121,7 +121,7 @@ let decode_to_istate top_level value =
   match (instr_decoded,error) with
     | (Just instr, _) -> 
       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
 	(fun _ -> Interp.resume 
 	 (make_mode true false) 
 	 (Interp.Thunk_frame 
@@ -130,13 +130,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 ("",[],[])
+	    (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 = 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 68e57b47..ec863a41 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -82,22 +82,15 @@ Follows the form of the instruction in instruction_extractor, but populates the
 *)
 type instruction_form = (string * list (string * instr_parm_typ * value) * list base_effect)
 
-type i_state_or_error =
-  | Instr of instruction_state * instruction_form
-  | Unsupported_instruction_error of instruction_form
-  | Not_an_instruction_error
-  | Internal_error of string
-
-(*
 type decode_error = 
-  | Unsupported_instruction_error of instruction
+  | Unsupported_instruction_error of instruction_form
   | Not_an_instruction_error of value
   | Internal_error of string
 
 type i_state_or_error =
-  | Instr of instruction * instruction_state
+  | Instr of instruction_form * 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
-- 
cgit v1.2.3


From 66699a34c469caf667931975ba00775c7f6e8471 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Tue, 7 Oct 2014 14:13:13 +0100
Subject: Actually add the new file

---
 src/lem_interp/interp_utilities.lem | 93 +++++++++++++++++++++++++++++++++++++
 1 file changed, 93 insertions(+)
 create mode 100644 src/lem_interp/interp_utilities.lem

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
+
+
-- 
cgit v1.2.3


From fc6c694210a35c121822cbfd6a8a60501f728309 Mon Sep 17 00:00:00 2001
From: Peter Sewell
Date: Tue, 7 Oct 2014 14:58:57 +0100
Subject: kathy,peter: making decode integration with ppcmem2 typecheck

---
 Makefile                                 | 13 ++++++++-----
 src/lem_interp/instruction_extractor.lem |  4 ++--
 src/lem_interp/interp_inter_imp.lem      | 22 +++++++++++-----------
 src/lem_interp/interp_interface.lem      | 16 ++++++++--------
 src/lem_interp/run_interp_model.ml       | 16 ++++++++--------
 5 files changed, 37 insertions(+), 34 deletions(-)

diff --git a/Makefile b/Makefile
index f74e1d61..0267f4a6 100644
--- a/Makefile
+++ b/Makefile
@@ -1,12 +1,15 @@
-.PHONY: all src language clean power test
+.PHONY: all sail language clean power test
 
-all: src language
+all: sail interpreter language
 
-src: language
-	$(MAKE) -C $@
+sail: language
+	$(MAKE) -C src
 
 language:
-	$(MAKE) -C $@
+	$(MAKE) -C language
+
+interpreter: 
+	$(MAKE) -C src interpreter
 
 test: 
 	$(MAKE) -C src test
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index e47a5252..d4a52890 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -7,11 +7,11 @@ type typ =
 | Bitvector of maybe integer
 | Other
 
-type instruction = 
+type instruction_form = 
 |  Instr of string * list (string * typ) * list base_effect
 |  Skipped 
 
-val extract_instructions : string -> string -> defs tannot -> list instruction
+val extract_instructions : string -> string -> defs tannot -> list instruction_form
 
 let extract_parm (E_aux e (_,tannot)) =
   match e with
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 292552f4..27e5e17c 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -157,15 +157,15 @@ let rec interp_to_outcome mode thunk =
       match List.lookup i memory_functions with
       | (Just (Just read_k,_,f)) -> 
         let (location, length, tracking) = (f mode value) in
-        Read_mem read_k location tracking length Nothing (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
+        Read_mem read_k location length tracking (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
       | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
       end
     | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
       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 tracking length Nothing 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 ->
@@ -201,10 +201,10 @@ let rec ie_loop mode i_state =
       (E_read_reg reg)::(ie_loop mode (i_state_fun Unknown))
     | Write_reg reg value i_state->
       (E_write_reg reg value)::(ie_loop mode i_state)
-    | Read_mem read_k loc tracking length ltracking i_state_fun ->
-      (E_read_mem read_k loc tracking length ltracking)::(ie_loop mode (i_state_fun Unknown))
-    | Write_mem write_k loc track length l_track value v_track i_state_fun ->
-      (E_write_mem write_k loc track length l_track value v_track)::(ie_loop mode (i_state_fun true))
+    | 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 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 ;;
   
@@ -220,12 +220,12 @@ let rec rr_ie_loop mode i_state =
     | Write_reg reg value i_state->
       let (events,outcome) = (rr_ie_loop mode i_state) in
       (((E_write_reg reg value)::events), outcome)
-    | Read_mem read_k loc tracking  length ltracking i_state_fun ->
+    | 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 tracking length ltracking)::events),outcome)
-    | Write_mem write_k loc track length l_track value v_track i_state_fun ->
+      (((E_read_mem read_k loc length tracking)::events),outcome)
+    | 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 track 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 ec863a41..40c34480 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -38,9 +38,9 @@ type reg_name =
 type outcome =
 (* 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 * maybe (list reg_name) * integer * maybe (list reg_name) *  (value -> instruction_state)
+| 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 * maybe (list reg_name) * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
+| Write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
 (* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
 (* Request to read register, will track dependency when mode.track_values *)
@@ -57,8 +57,8 @@ type outcome =
 | Error of string
 
 type event = 
-| E_read_mem of read_kind * value * maybe (list reg_name) * integer * maybe (list reg_name)
-| E_write_mem of write_kind * value * maybe (list reg_name) * integer * maybe (list reg_name) * value * 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
@@ -71,7 +71,7 @@ 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 representint the constructor parameters in instruction_form, other is a type not representable externally*)
+(*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 *)
@@ -80,15 +80,15 @@ type instr_parm_typ =
 (*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_form = (string * list (string * instr_parm_typ * value) * list base_effect)
+type instruction = (string * list (string * instr_parm_typ * value) * list base_effect)
 
 type decode_error = 
-  | Unsupported_instruction_error of instruction_form
+  | Unsupported_instruction_error of instruction
   | Not_an_instruction_error of value
   | Internal_error of string
 
 type i_state_or_error =
-  | Instr of instruction_form * instruction_state
+  | Instr of instruction * instruction_state
   | Decode_error of decode_error
 
 
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 60258504..f8c05085 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -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,depl, 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,depl, 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)))), env)
- | Write_mem0(_,(Bytevector location),_, length, _, (Bytevector bytes),_,_) ->
+ | 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, ldeps, 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, ldeps, 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) "" "";
-- 
cgit v1.2.3


From 9800a6b05d5a2edc9fc62afdbc127643650666ff Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Tue, 7 Oct 2014 15:15:32 +0100
Subject: Track dependencies on size of memory access

---
 src/lem_interp/interp_inter_imp.lem | 42 +++++++++++++++++++++++++++++++++++--
 1 file changed, 40 insertions(+), 2 deletions(-)

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 27e5e17c..c18f07f7 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -81,14 +81,52 @@ 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 arg thunk = 
-- 
cgit v1.2.3


From aad2943a54b2d176c00ee5b0d42609887c78b415 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Tue, 7 Oct 2014 17:31:19 +0100
Subject: Connect interpreter to representation of instructions. Warning: this
 changes a few of the constructor names in the instruction_extractor.lem
 interface

---
 src/lem_interp/instruction_extractor.lem | 27 +++++++++++-----------
 src/lem_interp/interp.lem                | 31 +++++++++++++++++--------
 src/lem_interp/interp_inter_imp.lem      | 39 +++++++++++++++++++++++++++-----
 3 files changed, 69 insertions(+), 28 deletions(-)

diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index d4a52890..d2597740 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -2,13 +2,13 @@ open import Interp_ast
 open import Interp_utilities
 open import Pervasives
 
-type typ = 
-| Bit
-| Bitvector of maybe integer
-| Other
+type instr_parm_typ = 
+| IBit
+| IBitvector of maybe integer
+| IOther
 
 type instruction_form = 
-|  Instr of string * list (string * typ) * list base_effect
+|  Instr_form of string * list (string * instr_parm_typ) * list base_effect
 |  Skipped 
 
 val extract_instructions : string -> string -> defs tannot -> list instruction_form
@@ -17,13 +17,14 @@ 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,8 +50,8 @@ 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 = 
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index a436d652..6febc709 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -7,6 +7,8 @@ open import String_extra (* for 'show' to convert nat to string) *)
 open import Interp_ast
 open import Interp_utilities
 
+open import Instruction_extractor
+
 type tannot = Interp_utilities.tannot
 
 val intern_annot : tannot -> tannot
@@ -112,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)
@@ -982,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
@@ -1757,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
@@ -2068,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
@@ -2113,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
@@ -2128,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 c18f07f7..b930e8ec 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
@@ -129,7 +130,7 @@ let memory_functions =
 	      end end end)));
   ]
 
-let rec interp_to_value_helper arg 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))
@@ -137,20 +138,36 @@ let rec interp_to_value_helper arg thunk =
       match List.lookup i external_functions with
 	| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
 	| Just f  -> 
-          interp_to_value_helper arg (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 "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 value
+  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 
@@ -158,8 +175,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 value
+      let (instr_decoded,error) = interp_to_value_helper value instr_external
 	(fun _ -> Interp.resume 
 	 (make_mode true false) 
 	 (Interp.Thunk_frame 
@@ -168,7 +195,7 @@ 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 ("",[],[])
+	  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)
-- 
cgit v1.2.3


From 34f044d2e1b54a931c2fe50ec116310d3adb45d6 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Wed, 8 Oct 2014 10:38:15 +0100
Subject: Support exporting single bit and bool values to external bitvectors

---
 src/lem_interp/interp_inter_imp.lem | 29 ++++++++++++++++++++++-------
 1 file changed, 22 insertions(+), 7 deletions(-)

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index b930e8ec..19d41f8c 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -41,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))), 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))), 
-          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
 
-- 
cgit v1.2.3