summaryrefslogtreecommitdiff
path: root/mips
diff options
context:
space:
mode:
Diffstat (limited to 'mips')
-rw-r--r--mips/Makefile23
-rw-r--r--mips/mips_extras.lem14
2 files changed, 30 insertions, 7 deletions
diff --git a/mips/Makefile b/mips/Makefile
new file mode 100644
index 00000000..03d7ae15
--- /dev/null
+++ b/mips/Makefile
@@ -0,0 +1,23 @@
+SAIL:=../src/sail.native
+LEM:=../../lem/lem
+
+# SOURCES:=mips_prelude.sail mips_tlb.sail mips_wrappers.sail mips_insts.sail mips_ri.sail mips_epilogue.sail ../etc/regfp.sail mips_regfp.sail
+SOURCES:=mips_prelude.sail mips_tlb_stub.sail mips_wrappers.sail mips_insts.sail mips_epilogue.sail ../etc/regfp.sail mips_regfp.sail
+
+
+all: mips.lem mips.ml mips_embed.lem
+
+mips.lem: $(SOURCES)
+ $(SAIL) -lem_ast -o $(BUILD)/mips $(SOURCES)
+
+mips.ml: mips.lem ../src/lem_interp/interp_ast.lem
+ $(LEM) -ocaml -lib ../src/lem_interp/ $<
+
+
+mips_embed.lem: $(SOURCES)
+# also generates mips_embed_sequential.lem, mips_embed_types.lem, mips_toFromInterp.lem
+ $(SAIL) -lem -lem_lib Mips_extras_embed -o mips $(SOURCES)
+
+clean:
+ rm -f mips.lem mips.ml
+ rm -f mips_embed*.lem mips_toFromInterp.lem
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 1fbba038..be576fb2 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -31,25 +31,25 @@ let memory_parameter_transformer_option_address _mode v =
end
-let read_memory_functions : memory_reads =
+let mips_read_memory_functions : memory_reads =
[ ("MEMr", (MR Read_plain memory_parameter_transformer));
("MEMr_reserve", (MR Read_reserve memory_parameter_transformer));
]
-let read_memory_tagged_functions : memory_read_taggeds =
+let mips_read_memory_tagged_functions : memory_read_taggeds =
[ ("MEMr_tag", (MRT Read_plain memory_parameter_transformer));
("MEMr_tag_reserve", (MRT Read_reserve memory_parameter_transformer));
]
-let memory_writes : memory_writes =
+let mips_memory_writes : memory_writes =
[]
-let memory_eas : memory_write_eas =
+let mips_memory_eas : memory_write_eas =
[ ("MEMea", (MEA Write_plain memory_parameter_transformer));
("MEMea_conditional", (MEA Write_conditional memory_parameter_transformer));
]
-let memory_vals : memory_write_vals =
+let mips_memory_vals : memory_write_vals =
[ ("MEMval", (MV memory_parameter_transformer_option_address Nothing));
("MEMval_conditional", (MV memory_parameter_transformer_option_address
(Just
@@ -58,7 +58,7 @@ let memory_vals : memory_write_vals =
(IState (Interp.add_answer_to_stack interp bit) context)))));
]
-let memory_vals_tagged : memory_write_vals_tagged =
+let mips_memory_vals_tagged : memory_write_vals_tagged =
[
("MEMval_tag", (MVT memory_parameter_transformer_option_address Nothing));
("MEMval_tag_conditional", (MVT memory_parameter_transformer_option_address
@@ -68,6 +68,6 @@ let memory_vals_tagged : memory_write_vals_tagged =
(IState (Interp.add_answer_to_stack interp bit) context)))));
]
-let barrier_functions = [
+let mips_barrier_functions = [
("MEM_sync", Barrier_MIPS_SYNC);
]