From 3a94b84be7f1a4180412fb474e9829a8fad9d7e6 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Tue, 10 Nov 2015 16:19:59 +0000 Subject: Update tag for register write in nested lexp Also starting to try to get elf compiling for sequential interpreter --- src/Makefile | 13 +++---------- src/_tags | 8 +++++++- src/myocamlbuild.ml | 3 ++- src/type_check.ml | 6 +++--- 4 files changed, 15 insertions(+), 15 deletions(-) (limited to 'src') 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 or : include : use_pprint, use_nums or : 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 and not : use_nums, use_lem - and not : use_nums, use_lem, use_str + and not : use_nums, use_lem, use_str, use_batteries + : use_batteries, use_lem, use_nums + : use_batteries, use_lem, use_nums + : use_batteries, use_lem, use_nums + : 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))) -- cgit v1.2.3