First bit of gluing mips onto interpreter and eventually ppcmem infrastructure

2 files changed, 167 insertions, 0 deletions

diff --git a/mips/Makefile b/mips/Makefile
new file mode 100644
index 00000000..f8417c67
--- /dev/null
+++ b/mips/Makefile
@@ -0,0 +1,74 @@
+BITBUCKETDIR= ~/bitbucket
+SAILDIR=$(BITBUCKETDIR)/l2/
+SAIL=$(SAILDIR)/src/_build/sail.native
+BUILDDIR=./build/
+LEMDIR=$(BITBUCKETDIR)/lem/
+LEM=$(LEMDIR)/lem
+
+# we need bash to use PIPESTATUS for the error parsing
+# (if bash is not found the build will still work)
+ifneq ("$(wildcard /bin/bash)","")
+SHELL=/bin/bash
+endif
+
+
+# the order of the files is important
+MIPSSOURCES= mips.sail
+
+all: $(BUILDDIR)/mips.ml $(BUILDDIR)/mips_extras.ml
+
+lem: $(BUILDDIR)/mips.lem
+
+# this will force build everything, including the tools
+full:
+	$(MAKE) -B
+
+test: $(BUILDDIR)/test.lem
+
+### tools: these will run only if the tools don't already exist or with 'make full'
+
+$(SAIL):
+	$(MAKE) -C $(SAILDIR)
+
+$(LEM):
+	$(MAKE) -C $(LEMDIR)
+
+### tools end
+
+$(BUILDDIR):
+	mkdir -p $@
+
+$(BUILDDIR)/mips.lem: $(MIPSSOURCES) $(SAIL) | $(BUILDDIR)
+# if bash is detected we can print nicer errors
+ifeq ($(SHELL),/bin/bash)
+# 	the test at the end is so we return the exit code of sail and not parse_sail.sh
+	$(SAIL) -lem_ast $(MIPSSOURCES) 2>&1 | ./parse_sail.sh; test "$${PIPESTATUS[0]}" -eq 0
+else
+	$(SAIL) -lem_ast $(MIPSSOURCES)
+endif
+#       sail uses the name of the first file on the list
+	@mv $(<:.sail=.lem) $(BUILDDIR)mips.lem
+
+$(BUILDDIR)/mips.ml: $(BUILDDIR)mips.lem $(LEM)
+	$(LEM) -ocaml -only_changed_output -lib $(SAILDIR)/src/lem_interp/ $<
+# 	FIXME: lem bug, does not change modification time
+	touch $@
+
+$(BUILDDIR)/mips_extras.ml: $(BUILDDIR)mips_extras.lem $(LEM)
+	cp mips_extras.lem $<
+	$(LEM) -ocaml -only_changed_output -lib $(SAILDIR)/src/lem_interp/ $<
+	touch $@
+
+$(BUILDDIR)/test.lem: test.sail $(SAIL) | $(BUILDDIR)
+# if bash is detected we can print nicer errors
+ifeq ($(SHELL),/bin/bash)
+# 	the test at the end is so we return the exit code of sail and not parse_sail.sh
+	$(SAIL) -lem_ast test.sail 2>&1 | ./parse_sail.sh; test "$${PIPESTATUS[0]}" -eq 0
+else
+	$(SAIL) -lem_ast test.sail
+endif
+
+clean:
+	rm -rf $(BUILDDIR)
+
+.PHONY: all full clean test
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
new file mode 100644
index 00000000..49a618dc
--- /dev/null
+++ b/mips/mips_extras.lem
@@ -0,0 +1,93 @@
+open import Pervasives
+open import Interp_ast
+open import Interp_interface 
+open import Interp_inter_imp 
+import Set_extra
+
+
+(*MIPS specific external functions*)
+let mips_externs = [
+]
+
+let read_memory_functions : memory_reads =
+  [ ("MEMr", (MR Read_plain
+                (fun mode v -> match v with
+                   | Interp.V_tuple [location;length] ->
+                     match length with
+                     | Interp.V_lit (L_aux (L_num len) _) ->
+                       let (v,regs) = extern_mem_value mode location in
+                       (v,(natFromInteger len),regs) 
+                     | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+                       let (v,loc_regs) = extern_mem_value mode location in
+                       match loc_regs with
+                       | Nothing -> (v,(natFromInteger len),
+                                     Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
+                       | Just loc_regs -> 
+                         (v,(natFromInteger len),
+                          Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
+              end end end)));
+    ("MEMr_reserve", (MR Read_reserve (*TODO Likely this isn't really best to be the same as Power*)
+                        (fun mode v -> match v with
+                           | Interp.V_tuple [location;length] ->
+                             match length with
+                             | Interp.V_lit (L_aux (L_num len) _) ->
+                               let (v,regs) = extern_mem_value mode location in
+                               (v,(natFromInteger len),regs) 
+                             | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+                               let (v,loc_regs) = extern_mem_value mode location in
+                               match loc_regs with
+                               | Nothing -> 
+                                 (v,(natFromInteger len),
+                                  Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
+                               | Just loc_regs -> 
+                                 (v,(natFromInteger len),
+                                  Just (loc_regs++
+                                        (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
+                                 end end end)));                
+]
+let memory_writes : memory_writes = [
+  ("MEMw", (MW Write_plain 
+              (fun mode v -> match v with
+                 | Interp.V_tuple [location;length] ->
+                   match length with
+                   | Interp.V_lit (L_aux (L_num len) _) ->
+                     let (v,regs) = extern_mem_value mode location in
+                     (v,(natFromInteger len),regs)
+                   | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+                     let (v,loc_regs) = extern_mem_value mode location in
+                     match loc_regs with
+                     | Nothing -> (v,(natFromInteger len),
+                                   Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
+                     | Just loc_regs -> 
+                       (v,(natFromInteger len),
+                        Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
+                      end end end) Nothing));
+  (* As above, probably not best to be the same write kind as power *)
+  ("MEMw_conditional", (MW Write_conditional 
+                          (fun mode v -> match v with
+                             | Interp.V_tuple [location;length] ->
+                               match length with
+                               | Interp.V_lit (L_aux (L_num len) _) ->
+                                 let (v,regs) = extern_mem_value mode location in
+                                 (v,(natFromInteger len),regs)
+                               | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+                                 let (v,loc_regs) = extern_mem_value mode location in
+                                 match loc_regs with
+                                 | Nothing -> 
+                                   (v,(natFromInteger len),
+                                    Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
+                                 | Just loc_regs -> 
+                                   (v,(natFromInteger len),
+                                    Just (loc_regs++
+                                          (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
+                                end end end) 
+                            (Just (fun (IState interp_state c) success ->
+                              let v = Interp.V_lit (L_aux (if success then L_one else L_zero) Unknown) in
+                              IState (Interp.add_answer_to_stack interp_state v) c))
+     ));
+  ]
+
+let barrier_functions = [
+  (*Need to know what barrier kind to install*)
+  ("MEM_Sync", Isync);
+]