Switched to bytecode compiler for executing interpreter to avoid stack overflow

3 files changed, 17 insertions, 8 deletions

diff --git a/src/Makefile b/src/Makefile
index 298d22c8..e0c1e45c 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -79,7 +79,8 @@ LEM = $(BITBUCKET_ROOT)/lem/lem
 LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib
 ELFDIR= $(BITBUCKET_ROOT)/linksem
 ZARITH_DIR=$(LEMLIBOCAML)/dependencies/zarith
-ZARITH_LIB=$(ZARITH_DIR)/zarith.cmxa
+ZARITH_LIB=$(ZARITH_DIR)/zarith.cma
+# ZARITH_LIB=$(ZARITH_DIR)/zarith.cmxa
 
 SAIL_LIB_DIR:=$(SAIL_DIR)/lib
 MIPS_SAIL_DIR:=$(SAIL_DIR)/mips_new_tc
@@ -204,8 +205,11 @@ count: _build/cheri_trimmed.sail _build/mips_trimmed.sail
 %.ml: %.lem
 	$(LEM) -only_changed_output -ocaml -lib lem_interp/ $<
 
+#run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter
+#	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml  -o run_mips.native
+
 run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter
-	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml  -o run_mips.native
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlc $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cma $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cma $(ELFDIR)/src/linksem.cma  _build/pprint/src/PPrintLib.cma _build/lem_interp/extract.cma _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml  -o run_mips.native
 
 run_cheri.native:  _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter
 	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml  -o run_cheri.native
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index 8bc19f8c..056f0100 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -127,7 +127,10 @@ let rec extract_patt_parm (P_aux p (_,tannot)) =
 let rec extract_from_execute fcls = match fcls with
   | [] -> []
   | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) parms) _) _) (_,Just(_,_,_,Effect_aux(Effect_set efs) _,_))::fcls ->
-    (Instr_form i (List.map extract_patt_parm parms) efs)::extract_from_execute fcls
+     (Instr_form i (List.map extract_patt_parm parms) efs)::extract_from_execute fcls
+  | _ :: fcls ->
+     (* AA: Find out what breaks this *)
+     extract_from_execute fcls
 end
 
 let rec extract_effects instrs execute = 
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 443a2c63..65d99780 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -300,13 +300,15 @@ let rec pp_format_nes nes =
      nes) ^*) "]"
 
 let pp_format_annot = function
-  | _ -> "Nothing"
-
-    (*
   | None -> "Nothing"
   | Some (_, typ, eff) ->
-    "(Just (" ^ pp_format_typ_lem typ ^ ", " ^ pp_format_effects_lem eff ^ "))"
-     *)
+     "(Just ("
+     ^ pp_format_typ_lem typ ^ ", "
+     ^ "Tag_empty" ^ ", "
+     ^ "[], "
+     ^ pp_format_effects_lem eff ^ ", "
+     ^ pp_format_effects_lem eff
+     ^ "))"
 
 (*
   | NoTyp -> "Nothing"