From 05a4a75d328d3bd8469167f6f23dda918146117a Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 4 May 2018 19:08:15 +0100 Subject: Bit of hackery to MIPS prelude and Makefiles to get monomorphised CHERI --- mips/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mips/Makefile') diff --git a/mips/Makefile b/mips/Makefile index 00703f62..a6a5bbdf 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -21,7 +21,7 @@ mips_no_tlb_types.lem: mips_no_tlb.lem # TODO: Use monomorphisation so that we can switch to machine words mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) - $(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen -memo_z3 $^ + $(SAIL) -lem -o mips -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ mips_types.lem: mips.lem M%.thy: m%.lem m%_types.lem mips_extras.lem -- cgit v1.2.3 From c37130ba4ac69be6a298476b24b1f93811df4bb4 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 17 May 2018 12:12:02 +0100 Subject: Clean up MIPS for HOL4 a little Move mono_rewrites into lib --- mips/Makefile | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'mips/Makefile') diff --git a/mips/Makefile b/mips/Makefile index c0670380..100687e8 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -19,8 +19,7 @@ mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS) $(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ mips_no_tlb_types.lem: mips_no_tlb.lem -# TODO: Use monomorphisation so that we can switch to machine words -mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) +mips.lem: $(MIPS_PRE) $(SAIL_LIB_DIR)/mono_rewrites.sail $(MIPS_TLB) $(MIPS_SAILS) $(SAIL) -lem -o mips -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ mips_types.lem: mips.lem @@ -28,8 +27,16 @@ M%.thy: m%.lem m%_types.lem mips_extras.lem lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy +%Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem + lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ + +%Theory.uo: %Script.sml + Holmake $@ + LOC_FILES:=$(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) include ../etc/loc.mk clean: - rm -rf mips Mips.thy mips.lem _sbuild + rm -rf mips Mips.thy mips.lem mips_types.lem _sbuild + rm -f mipsScript.sml mips_typesScript.sml mips_extrasScript.sml + -Holmake cleanAll -- cgit v1.2.3 From 2c533959ae0bc96d5e648497a74a79e430d4feea Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 4 Jun 2018 16:48:04 +0100 Subject: Add mips.c target in Makefile. Currently triggers assertion failure in c_backend. still need to merge changes to prelude.sail. --- mips/Makefile | 3 +++ 1 file changed, 3 insertions(+) (limited to 'mips/Makefile') diff --git a/mips/Makefile b/mips/Makefile index 100687e8..b612c1d0 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -15,6 +15,9 @@ MIPS_MAIN:=$(MIPS_SAIL_DIR)/main.sail mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) $(SAIL) -ocaml -o mips -memo_z3 $^ +mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) + $(SAIL) -memo_z3 -c $^ 1> $@ + mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS) $(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ mips_no_tlb_types.lem: mips_no_tlb.lem -- cgit v1.2.3 From dd21e688ec4d601d71f52bae56a40bf67e713d72 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 7 Jun 2018 17:40:12 +0100 Subject: add mips_c target. --- mips/Makefile | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'mips/Makefile') diff --git a/mips/Makefile b/mips/Makefile index b612c1d0..cc36f952 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -15,8 +15,11 @@ MIPS_MAIN:=$(MIPS_SAIL_DIR)/main.sail mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) $(SAIL) -ocaml -o mips -memo_z3 $^ -mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) - $(SAIL) -memo_z3 -c $^ 1> $@ +mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) Makefile + $(SAIL) -O -memo_z3 -c $(filter %.sail, $^) 1> $@ + +mips_c: mips.c ../lib/sail.h Makefile + gcc -O2 -g -I ../lib $< -l gmp -o $@ mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS) $(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ @@ -40,6 +43,6 @@ LOC_FILES:=$(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) include ../etc/loc.mk clean: - rm -rf mips Mips.thy mips.lem mips_types.lem _sbuild + rm -rf mips Mips.thy mips.lem mips_types.lem _sbuild mips.c mips_c rm -f mipsScript.sml mips_typesScript.sml mips_extrasScript.sml -Holmake cleanAll -- cgit v1.2.3 From 3398a9debf4aaf084db28bd4aa8606b264d47df9 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 8 Jun 2018 11:58:07 +0100 Subject: add sail as dependency of mips targets. --- mips/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'mips/Makefile') diff --git a/mips/Makefile b/mips/Makefile index cc36f952..6abf1848 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -12,10 +12,10 @@ MIPS_TLB_STUB:=$(MIPS_SAIL_DIR)/mips_tlb_stub.sail MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail MIPS_MAIN:=$(MIPS_SAIL_DIR)/main.sail -mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) - $(SAIL) -ocaml -o mips -memo_z3 $^ +mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) ../sail + $(SAIL) -ocaml -o mips -memo_z3 $(filter %.sail, $^) -mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) Makefile +mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) Makefile ../sail $(SAIL) -O -memo_z3 -c $(filter %.sail, $^) 1> $@ mips_c: mips.c ../lib/sail.h Makefile -- cgit v1.2.3