summaryrefslogtreecommitdiff
path: root/mips
diff options
context:
space:
mode:
Diffstat (limited to 'mips')
-rw-r--r--mips/Makefile74
-rw-r--r--mips/mips.sail4
-rw-r--r--mips/mips_extras.lem93
3 files changed, 169 insertions, 2 deletions
diff --git a/mips/Makefile b/mips/Makefile
new file mode 100644
index 00000000..7bd20737
--- /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:
+ 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.sail b/mips/mips.sail
index b18f3cda..ff34c67e 100644
--- a/mips/mips.sail
+++ b/mips/mips.sail
@@ -1,10 +1,10 @@
(* bit vectors have indices decreasing from left i.e. msb is highest index *)
default Order dec
-(* external functions *)
+(*(* external functions *)
val extern forall Nat 'm, Nat 'n. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTS (* Sign extend *)
val extern forall Nat 'n, Nat 'm. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTZ (* Zero extend *)
-
+*)
register (bit[64]) PC
(* CP0 Registers *)
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);
+]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 17:09:59 +0000