diff options
| l---------[-rw-r--r--] | aarch64/mono/mono_rewrites.sail | 158 | ||||
| -rw-r--r-- | lib/mono_rewrites.sail | 157 | ||||
| -rw-r--r-- | mips/.gitignore | 5 | ||||
| -rw-r--r-- | mips/Holmakefile | 11 | ||||
| -rw-r--r-- | mips/Makefile | 13 | ||||
| -rw-r--r-- | mips/prelude.sail | 2 |
6 files changed, 184 insertions, 162 deletions
diff --git a/aarch64/mono/mono_rewrites.sail b/aarch64/mono/mono_rewrites.sail index c9164b6c..10f2d07b 100644..120000 --- a/aarch64/mono/mono_rewrites.sail +++ b/aarch64/mono/mono_rewrites.sail @@ -1,157 +1 @@ -/* Definitions for use with the -mono_rewrites option */ - -/* External definitions not in the usual asl prelude */ - -infix 6 << - -val shiftleft = "shiftl" : forall 'n ('ord : Order). - (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure - -overload operator << = {shiftleft} - -infix 6 >> - -val shiftright = "shiftr" : forall 'n ('ord : Order). - (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure - -overload operator >> = {shiftright} - -val arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order). - (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure - -val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extzv(v) = extz_vec(sizeof('m),v) - -val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extsv(v) = exts_vec(sizeof('m),v) - -/* This is generated internally to deal with case splits which reveal the size - of a bitvector */ -val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure - -/* Definitions for the rewrites */ - -val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure -function slice_mask(i,l) = - let one : bits('n) = extzv(0b1) in - ((one << l) - one) << i - -val is_zero_subrange : forall 'n, 'n >= 0. - (bits('n), int, int) -> bool effect pure - -function is_zero_subrange (xs, i, j) = { - (xs & slice_mask(j, i-j)) == extzv(0b0) -} - -val is_ones_subrange : forall 'n, 'n >= 0. - (bits('n), int, int) -> bool effect pure - -function is_ones_subrange (xs, i, j) = { - let m : bits('n) = slice_mask(j,j-i) in - (xs & m) == m -} - -val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0. - (bits('n), int, int, bits('m), int, int) -> bits('r) effect pure - -function slice_slice_concat (xs, i, l, ys, i', l') = { - let xs = (xs & slice_mask(i,l)) >> i in - let ys = (ys & slice_mask(i',l')) >> i' in - extzv(xs) << l' | extzv(ys) -} - -val slice_zeros_concat : forall 'n 'p 'q 'r, 'r = 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0. - (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure - -function slice_zeros_concat (xs, i, l, l') = { - let xs = (xs & slice_mask(i,l)) >> i in - extzv(xs) << l' -} - -/* Assumes initial vectors are of equal size */ - -val subrange_subrange_eq : forall 'n, 'n >= 0. - (bits('n), int, int, bits('n), int, int) -> bool effect pure - -function subrange_subrange_eq (xs, i, j, ys, i', j') = { - let xs = (xs & slice_mask(j,i-j)) >> j in - let ys = (ys & slice_mask(j',i'-j')) >> j' in - xs == ys -} - -val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's = 'o - ('p - 1) + 'q - ('r - 1) & 'n >= 0 & 'm >= 0. - (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure - -function subrange_subrange_concat (xs, i, j, ys, i', j') = { - let xs = (xs & slice_mask(j,i-j)) >> j in - let ys = (ys & slice_mask(j',i'-j')) >> j' in - extzv(xs) << i' - (j' - 1) | extzv(ys) -} - -val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int, int) -> bits('m) effect pure - -function place_subrange(xs,i,j,shift) = { - let xs = (xs & slice_mask(j,i-j)) >> j in - extzv(xs) << shift -} - -val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int, int) -> bits('m) effect pure - -function place_slice(xs,i,l,shift) = { - let xs = (xs & slice_mask(i,l)) >> i in - extzv(xs) << shift -} - -val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int) -> bits('m) effect pure - -function zext_slice(xs,i,l) = { - let xs = (xs & slice_mask(i,l)) >> i in - extzv(xs) -} - -val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int) -> bits('m) effect pure - -function sext_slice(xs,i,l) = { - let xs = arith_shiftright(((xs & slice_mask(i,l)) << ('n - i - l)), 'n - l) in - extsv(xs) -} - -/* This has different names in the aarch64 prelude (UInt) and the other - preludes (unsigned). To avoid variable name clashes, we redeclare it - here with a suitably awkward name. */ -val _builtin_unsigned = { - ocaml: "uint", - lem: "uint", - interpreter: "uint", - c: "sail_uint" -} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) - -val unsigned_slice : forall 'n, 'n >= 0. - (bits('n), int, int) -> int effect pure - -function unsigned_slice(xs,i,l) = { - let xs = (xs & slice_mask(i,l)) >> i in - _builtin_unsigned(xs) -} - -val unsigned_subrange : forall 'n, 'n >= 0. - (bits('n), int, int) -> int effect pure - -function unsigned_subrange(xs,i,j) = { - let xs = (xs & slice_mask(j,i-j)) >> i in - _builtin_unsigned(xs) -} - - -val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure - -function zext_ones(m) = { - let v : bits('n) = extsv(0b1) in - v >> ('n - m) -} +../../lib/mono_rewrites.sail
\ No newline at end of file diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail new file mode 100644 index 00000000..c9164b6c --- /dev/null +++ b/lib/mono_rewrites.sail @@ -0,0 +1,157 @@ +/* Definitions for use with the -mono_rewrites option */ + +/* External definitions not in the usual asl prelude */ + +infix 6 << + +val shiftleft = "shiftl" : forall 'n ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure + +overload operator << = {shiftleft} + +infix 6 >> + +val shiftright = "shiftr" : forall 'n ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure + +overload operator >> = {shiftright} + +val arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure + +val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure +function extzv(v) = extz_vec(sizeof('m),v) + +val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure +function extsv(v) = exts_vec(sizeof('m),v) + +/* This is generated internally to deal with case splits which reveal the size + of a bitvector */ +val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure + +/* Definitions for the rewrites */ + +val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure +function slice_mask(i,l) = + let one : bits('n) = extzv(0b1) in + ((one << l) - one) << i + +val is_zero_subrange : forall 'n, 'n >= 0. + (bits('n), int, int) -> bool effect pure + +function is_zero_subrange (xs, i, j) = { + (xs & slice_mask(j, i-j)) == extzv(0b0) +} + +val is_ones_subrange : forall 'n, 'n >= 0. + (bits('n), int, int) -> bool effect pure + +function is_ones_subrange (xs, i, j) = { + let m : bits('n) = slice_mask(j,j-i) in + (xs & m) == m +} + +val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0. + (bits('n), int, int, bits('m), int, int) -> bits('r) effect pure + +function slice_slice_concat (xs, i, l, ys, i', l') = { + let xs = (xs & slice_mask(i,l)) >> i in + let ys = (ys & slice_mask(i',l')) >> i' in + extzv(xs) << l' | extzv(ys) +} + +val slice_zeros_concat : forall 'n 'p 'q 'r, 'r = 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0. + (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure + +function slice_zeros_concat (xs, i, l, l') = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) << l' +} + +/* Assumes initial vectors are of equal size */ + +val subrange_subrange_eq : forall 'n, 'n >= 0. + (bits('n), int, int, bits('n), int, int) -> bool effect pure + +function subrange_subrange_eq (xs, i, j, ys, i', j') = { + let xs = (xs & slice_mask(j,i-j)) >> j in + let ys = (ys & slice_mask(j',i'-j')) >> j' in + xs == ys +} + +val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's = 'o - ('p - 1) + 'q - ('r - 1) & 'n >= 0 & 'm >= 0. + (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure + +function subrange_subrange_concat (xs, i, j, ys, i', j') = { + let xs = (xs & slice_mask(j,i-j)) >> j in + let ys = (ys & slice_mask(j',i'-j')) >> j' in + extzv(xs) << i' - (j' - 1) | extzv(ys) +} + +val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int, int) -> bits('m) effect pure + +function place_subrange(xs,i,j,shift) = { + let xs = (xs & slice_mask(j,i-j)) >> j in + extzv(xs) << shift +} + +val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int, int) -> bits('m) effect pure + +function place_slice(xs,i,l,shift) = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) << shift +} + +val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int) -> bits('m) effect pure + +function zext_slice(xs,i,l) = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) +} + +val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int) -> bits('m) effect pure + +function sext_slice(xs,i,l) = { + let xs = arith_shiftright(((xs & slice_mask(i,l)) << ('n - i - l)), 'n - l) in + extsv(xs) +} + +/* This has different names in the aarch64 prelude (UInt) and the other + preludes (unsigned). To avoid variable name clashes, we redeclare it + here with a suitably awkward name. */ +val _builtin_unsigned = { + ocaml: "uint", + lem: "uint", + interpreter: "uint", + c: "sail_uint" +} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) + +val unsigned_slice : forall 'n, 'n >= 0. + (bits('n), int, int) -> int effect pure + +function unsigned_slice(xs,i,l) = { + let xs = (xs & slice_mask(i,l)) >> i in + _builtin_unsigned(xs) +} + +val unsigned_subrange : forall 'n, 'n >= 0. + (bits('n), int, int) -> int effect pure + +function unsigned_subrange(xs,i,j) = { + let xs = (xs & slice_mask(j,i-j)) >> i in + _builtin_unsigned(xs) +} + + +val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure + +function zext_ones(m) = { + let v : bits('n) = extsv(0b1) in + v >> ('n - m) +} diff --git a/mips/.gitignore b/mips/.gitignore new file mode 100644 index 00000000..2ee9fde0 --- /dev/null +++ b/mips/.gitignore @@ -0,0 +1,5 @@ +mips.lem +mips_types.lem +mipsScript.sml +mips_typesScript.sml +mips_extrasScript.sml
\ No newline at end of file diff --git a/mips/Holmakefile b/mips/Holmakefile new file mode 100644 index 00000000..a31bfd4f --- /dev/null +++ b/mips/Holmakefile @@ -0,0 +1,11 @@ +LEMDIR=../../lem/hol-lib + +INCLUDES = $(LEMDIR) ../lib/hol + +all: mipsTheory.uo +.PHONY: all + +ifdef POLY +BASE_HEAP = ../lib/hol/sail-heap + +endif diff --git a/mips/Makefile b/mips/Makefile index c0670380..100687e8 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -19,8 +19,7 @@ mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS) $(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ mips_no_tlb_types.lem: mips_no_tlb.lem -# TODO: Use monomorphisation so that we can switch to machine words -mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) +mips.lem: $(MIPS_PRE) $(SAIL_LIB_DIR)/mono_rewrites.sail $(MIPS_TLB) $(MIPS_SAILS) $(SAIL) -lem -o mips -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ mips_types.lem: mips.lem @@ -28,8 +27,16 @@ M%.thy: m%.lem m%_types.lem mips_extras.lem lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy +%Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem + lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ + +%Theory.uo: %Script.sml + Holmake $@ + LOC_FILES:=$(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) include ../etc/loc.mk clean: - rm -rf mips Mips.thy mips.lem _sbuild + rm -rf mips Mips.thy mips.lem mips_types.lem _sbuild + rm -f mipsScript.sml mips_typesScript.sml mips_extrasScript.sml + -Holmake cleanAll diff --git a/mips/prelude.sail b/mips/prelude.sail index 5bb79f97..f805876a 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -310,5 +310,3 @@ val mask : forall 'm 'n , 'm >= 'n > 0 . bits('m) -> bits('n) function mask bs = bs['n - 1 .. 0] val "get_time_ns" : unit -> int - -$include <mono_rewrites.sail> |