Update tag for register write in nested lexp

Also starting to try to get elf compiling for sequential interpreter

4 files changed, 15 insertions, 15 deletions

diff --git a/src/Makefile b/src/Makefile
index 34b58c6d..57ae0981 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -11,6 +11,9 @@ interpreter:
 	ocamlbuild lem_interp/extract.cmxa
 	ocamlbuild lem_interp/extract.cma
 
+elf:
+	ocamlbuild -use-ocamlfind -pkgs batteries,uint src_elf/main_elf.native
+
 test: sail interpreter
 	ocamlbuild test/run_tests.native
 	./run_tests.native
@@ -23,16 +26,6 @@ install_elf:
 	cp -p ../../system-v-abi/src/*.ml elf_model/
 	cp -p -r ../../system-v-abi/src/libraries elf_model/libraries
 
-elf:
-	$(MAKE) -C elf_model ocaml_native
-	mkdir -p _build/elf_model
-	cp -p elf_model/*.cmi _build/elf_model/
-	cp -p elf_model/*.cmx _build/elf_model/
-	cp -p elf_model/*.o _build/elf_model/
-	cd _build/elf_model ;\
-	ocamlfind ocamlopt -package batteries -package uint -package bitstring -I $(LEMLIBOCAML) -a -o elf_extract.cmxa missing_pervasives.cmx \
-show.cmx endianness.cmx error.cmx ml_bindings.cmx default_printing.cmx bitstring_local.cmx elf_types.cmx elf_header.cmx elf_file1.cmx elf_program_header_table.cmx elf_executable_file2.cmx string_table.cmx elf_section_header_table.cmx elf_interpreted_segment.cmx elf_symbol_table.cmx elf_executable_file3.cmx elf_linking_file2.cmx elf_linking_file3.cmx elf_relocation.cmx sail_interface.cmx
-
 
 power: sail interpreter elf
 	mkdir -p _build/test
diff --git a/src/_tags b/src/_tags
index 334566bd..09cca695 100644
--- a/src/_tags
+++ b/src/_tags
@@ -3,9 +3,15 @@ true: -traverse, debug
 <lem_interp> or <test>:  include
 <sail.{byte,native}>: use_pprint, use_nums
 <pprint> or <pprint/src>: include
+<{src_elf,src_elf/abis,src_elf/abis/power64,src_elf/abis/amd64,src_elf/abis/aarch64,src_elf/adaptors}> : include
+
 # see http://caml.inria.fr/mantis/view.php?id=4943
 <lem_interp/*> and not <lem_interp/*.cmxa>: use_nums, use_lem
-<test/*> and not <test/*.cmxa>: use_nums, use_lem, use_str
+<test/*> and not <test/*.cmxa>: use_nums, use_lem, use_str, use_batteries
+<src_elf/*.ml> : use_batteries, use_lem, use_nums
+<src_elf/abis/*.ml> : use_batteries, use_lem, use_nums
+<src_elf/abis/*/*.ml> : use_batteries, use_lem, use_nums
+<src_elf/adaptors/*.ml> : use_batteries, use_lem, use_nums, use_unix
 
 # disable partial match and unused variable warnings
 <**/*.ml>: warn_y
diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml
index e38dbb4d..c0172700 100644
--- a/src/myocamlbuild.ml
+++ b/src/myocamlbuild.ml
@@ -37,7 +37,8 @@ dispatch begin function
     (* ocaml_lib "lem_interp/interp"; *)
     ocaml_lib ~extern:true ~dir:lem_libdir  ~tag_name:"use_lem" lem_lib;
     ocaml_lib ~extern:false ~dir:"pprint/src" ~tag_name:"use_pprint" "pprint/src/PPrintLib";
-
+    ocaml_lib ~extern:true ~dir:"src_elf_libraries/batteries/_build/src" ~tag_name:"use_batteries" "src_elf_libraries/batteries";
+    
     rule "lem -> ml"
     ~prod: "%.ml"
     ~dep: "%.lem"
diff --git a/src/type_check.ml b/src/type_check.ml
index 6b738c97..37d9ba19 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1538,7 +1538,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
               | Tapp("register",[TA_typ t]) | Tabbrev(_,{t=Tapp("register",[TA_typ t])}) -> t,true,false
               | Tapp("reg",[TA_typ t]) -> t,false,false
               | _ -> item_t,false,true in
-          let ef = if add_reg_write then add_effect (BE_aux(BE_wreg,l)) efl else efl in
+          let ef,tag = if add_reg_write then (add_effect (BE_aux(BE_wreg,l)) efl,External None) else (efl,tag) in
           if is_top && reg_still_required && reg_required
           then typ_error l "Assignment expected a register or non-parameter non-letbound identifier to mutate"
           else
@@ -1739,7 +1739,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
                   let (bf_t, _, _) = range_to_type_inc bf in ((id_to_string id),bf_t))
                 ranges 
             in
-            let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e,pure_e,nob)) in
+            let tannot = into_register d_env (Base(([],ty),External None,[],pure_e,pure_e,nob)) in
             (TD_aux(td,(l,tannot)),
              Env({d_env with rec_env = ((id',Register,tannot,franges)::d_env.rec_env);
                abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env)))
@@ -1782,7 +1782,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
                 (fun (bf,id) -> let (bf_t, _, _) = range_to_type_dec bf in (id_to_string id, bf_t))
                 ranges 
             in
-            let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e,pure_e,nob)) in
+            let tannot = into_register d_env (Base(([],ty),External None,[],pure_e,pure_e,nob)) in
             (TD_aux(td,(l,tannot)),
              Env({d_env with rec_env = (id',Register,tannot,franges)::d_env.rec_env;
                abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env)))