From 56aedab536c905d3423e488ec9110b738d03bbf7 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 29 Sep 2017 16:18:37 +0100
Subject: Add MIPS->Isabelle target to Makefile

---
 mips_new_tc/mips_regfp.sail | 16 ++++++++--------
 src/Makefile                |  8 ++++++--
 2 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/mips_new_tc/mips_regfp.sail b/mips_new_tc/mips_regfp.sail
index 36750583..4980aa2c 100644
--- a/mips_new_tc/mips_regfp.sail
+++ b/mips_new_tc/mips_regfp.sail
@@ -41,13 +41,13 @@ let (vector <0, 32, inc, string >) GPRs =
 let CIA_fp = RFull("CIA")
 let NIA_fp = RFull("NIA")
 
-function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (instr) = {
-  iR := [|| ||];
-  oR := [|| ||];
-  aR := [|| ||];
-  ik := IK_simple;
-  Nias := [|| ||];
-  Dia := DIAFP_none;
+function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ((ast) instr) = {
+  (regfps) iR := [|| ||];
+  (regfps) oR := [|| ||];
+  (regfps) aR := [|| ||];
+  (instruction_kind) ik := IK_simple;
+  (niafps) Nias := [|| ||];
+  (diafp) Dia := DIAFP_none;
 
   switch instr {
     case (DADDIU (rs, rt, imm)) -> {
@@ -65,7 +65,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
     }
     case (DADD (rs, rt, rd)) -> {
       if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
-      if rt == 0 then () else oR := RFull(GPRs[rt]) :: oR;
+      if rd == 0 then () else oR := RFull(GPRs[rd]) :: oR;
     }
     case (ADD(rs, rt, rd)) -> {
       if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
diff --git a/src/Makefile b/src/Makefile
index 1bac0b71..d0001868 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -125,10 +125,14 @@ _build/mips.lem: $(MIPS_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_ast -o mips $(MIPS_SAILS)
 
-_build/mips_embed_types.lem: $(MIPS_SAILS) ./sail.native
+_build/mips_embed_types.lem: $(MIPS_NOTLB_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
-	../sail.native -lem_lib "Mips_extras_embed" -lem -o mips $(MIPS_NOTLB_SAILS)
+	../sail.native -lem_lib "Mips_extras_embed" -lem -lem_mwords -o mips $(MIPS_NOTLB_SAILS)
+
+_build/Mips_embed.thy: _build/mips_embed_types.lem
+	cd _build ;\
+	lem -isa -outdir . -lib ../lem_interp -lib ../gen_lib $(MIPS_SAIL_DIR)/mips_extras_embed.lem mips_embed_types.lem mips_embed.lem
 
 _build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native
 	mkdir -p _build
-- 
cgit v1.2.3