From 0b940fb7c599e2e47cc21a2708d4cae13cb1d934 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Thu, 17 Dec 2015 13:06:06 +0000 Subject: First bit of gluing mips onto interpreter and eventually ppcmem infrastructure --- language/l2.lem | 2 +- language/l2.ott | 2 +- mips/Makefile | 74 +++++++++++++++++++++++++++++++++++++++++ mips/mips_extras.lem | 93 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 169 insertions(+), 2 deletions(-) create mode 100644 mips/Makefile create mode 100644 mips/mips_extras.lem diff --git a/language/l2.lem b/language/l2.lem index dbfcb832..d097c902 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -7,7 +7,7 @@ open import Set_extra type l = | Unknown - | Int of string * l option (*internal types, functions*) + | Int of string * maybe l (*internal types, functions*) | Range of string * nat * nat * nat * nat | Generated of l (*location for a generated node, where l is the location of the closest original source*) diff --git a/language/l2.ott b/language/l2.ott index 94362c44..d5c92fe6 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -57,7 +57,7 @@ open import Set_extra type l = | Unknown - | Int of string * l option (*internal types, functions*) + | Int of string * maybe l (*internal types, functions*) | Range of string * nat * nat * nat * nat | Generated of l (*location for a generated node, where l is the location of the closest original source*) 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); +] -- cgit v1.2.3 From f7a642bd3f8a5436873d0163114a30dad23ba9c2 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Thu, 17 Dec 2015 16:48:54 +0000 Subject: Remove external functions that the library provides, having added them to the type environment finally. (Also small cleaning of the new makefile) --- mips/Makefile | 12 ++++++------ mips/mips.sail | 4 ++-- src/type_internal.ml | 8 ++++++++ 3 files changed, 16 insertions(+), 8 deletions(-) diff --git a/mips/Makefile b/mips/Makefile index f8417c67..7bd20737 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -15,9 +15,9 @@ endif # the order of the files is important MIPSSOURCES= mips.sail -all: $(BUILDDIR)/mips.ml $(BUILDDIR)/mips_extras.ml +all: $(BUILDDIR)mips.ml $(BUILDDIR)mips_extras.ml -lem: $(BUILDDIR)/mips.lem +lem: $(BUILDDIR)mips.lem # this will force build everything, including the tools full: @@ -38,7 +38,7 @@ $(LEM): $(BUILDDIR): mkdir -p $@ -$(BUILDDIR)/mips.lem: $(MIPSSOURCES) $(SAIL) | $(BUILDDIR) +$(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 @@ -49,13 +49,13 @@ 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) +$(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 $< +$(BUILDDIR)mips_extras.ml: + cp mips_extras.lem $@ $(LEM) -ocaml -only_changed_output -lib $(SAILDIR)/src/lem_interp/ $< touch $@ diff --git a/mips/mips.sail b/mips/mips.sail index 4f468354..16a607a9 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/src/type_internal.ml b/src/type_internal.ml index 65727e1b..59a573d9 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -2101,6 +2101,14 @@ let initial_typ_env = (mk_range n_zero (mk_nv "m"))]) (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), External (Some "bitwise_rotate"),[],pure_e,pure_e,nob)); + ("EXTS",Base((((mk_nat_params ["n";"m";"o";"p"])@["ord",{k=K_Ord}]), + (mk_pure_imp (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")) + (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "m")) "m")), + External (Some "EXTS"),[],pure_e,pure_e,nob)); + ("EXTZ",Base((((mk_nat_params ["n";"m";"o";"p"])@["ord",{k=K_Ord}]), + (mk_pure_imp (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")) + (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "m")) "m")), + External (Some "EXTZ"),[],pure_e,pure_e,nob)); ] -- cgit v1.2.3