diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/Makefile | 31 | ||||
| -rw-r--r-- | mips/main.sail | 57 | ||||
| -rw-r--r-- | mips/mips_ast_decl.sail | 44 | ||||
| -rw-r--r-- | mips/mips_epilogue.sail | 42 | ||||
| -rw-r--r-- | mips/mips_extras.lem | 94 | ||||
| -rw-r--r-- | mips/mips_insts.sail | 1708 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 620 | ||||
| -rw-r--r-- | mips/mips_regfp.sail | 455 | ||||
| -rw-r--r-- | mips/mips_ri.sail | 42 | ||||
| -rw-r--r-- | mips/mips_tlb.sail | 148 | ||||
| -rw-r--r-- | mips/mips_tlb_stub.sail | 48 | ||||
| -rw-r--r-- | mips/mips_wrappers.sail | 86 | ||||
| -rw-r--r-- | mips/prelude.sail | 391 |
13 files changed, 3766 insertions, 0 deletions
diff --git a/mips/Makefile b/mips/Makefile new file mode 100644 index 00000000..55d8e986 --- /dev/null +++ b/mips/Makefile @@ -0,0 +1,31 @@ +THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST))) +SAIL_DIR:=$(realpath $(dir $(THIS_MAKEFILE))..) +export SAIL_DIR +SAIL_LIB_DIR:=$(SAIL_DIR)/lib +MIPS_SAIL_DIR:=$(SAIL_DIR)/mips + +SAIL:=$(SAIL_DIR)/sail + +MIPS_PRE:=$(SAIL_LIB_DIR)/flow.sail $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail +MIPS_TLB:=$(MIPS_SAIL_DIR)/mips_tlb.sail +MIPS_TLB_STUB:=$(MIPS_SAIL_DIR)/mips_tlb_stub.sail +MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +MIPS_MAIN:=$(MIPS_SAIL_DIR)/main.sail + +mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) + $(SAIL) -ocaml -o mips $^ + +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 $^ +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) + $(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen $^ +mips_types.lem: mips.lem + +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 $^ + +clean: + rm -rf mips Mips.thy mips.lem _sbuild diff --git a/mips/main.sail b/mips/main.sail new file mode 100644 index 00000000..2df5c0f8 --- /dev/null +++ b/mips/main.sail @@ -0,0 +1,57 @@ + + + +val fetch_and_execute : unit -> unit effect {barr, eamem, escape, rmem, rreg, wmv, wreg, undef, wmvt, rmemt} +function fetch_and_execute () = { + while true do { + PC = nextPC; + inBranchDelay = branchPending; + branchPending = 0b0; + nextPC = if inBranchDelay then delayedPC else PC + 4; + cp2_next_pc(); + + print_bits("PC: ", PC); + try { + let pc_pa = TranslatePC(PC); + /*print_bits("pa: ", pc_pa);*/ + let instr = MEMr_wrapper(pc_pa, 4); + /*print_bits("hex: ", instr);*/ + let instr_ast = decode(instr); + match instr_ast { + Some(HCF()) => { + print("simulation stopped due to halt instruction."); + return (); + }, + Some(ast) => execute(ast), + None() => {print("Decode failed"); exit (())} /* Never expect this -- unknown instruction should actually result in reserved instruction ISA-level exception (see mips_ri.sail). */ + } + } catch { + ISAException() => print("EXCEPTION") + /* ISA-level exception occurrred either during TranslatePC or execute -- + just continue from nextPC, which should have been set to the appropriate + exception vector (along with clearing branchPending etc.) . */ + }; + }; + skip_rmemt(); + skip_wmvt(); +} + +val elf_entry = "Elf_loader.elf_entry" : unit -> int + +val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt} + +function dump_mips_state () : unit -> unit = { + print_bits("DEBUG MIPS PC ", PC); + foreach (idx from 0 to 31) { + print(concat_str("DEBUG MIPS REG ", concat_str(string_of_int(idx), concat_str(" ", BitStr(rGPR(to_bits(5,idx))))))); + } +} + +function main () = { + init_cp0_state(); + init_cp2_state(); + nextPC = to_bits(64, elf_entry()); + fetch_and_execute(); + dump_mips_state (); + dump_cp2_state () +} diff --git a/mips/mips_ast_decl.sail b/mips/mips_ast_decl.sail new file mode 100644 index 00000000..e39bc270 --- /dev/null +++ b/mips/mips_ast_decl.sail @@ -0,0 +1,44 @@ +/*========================================================================*/ +/* */ +/* Copyright (c) 2015-2017 Robert M. Norton */ +/* Copyright (c) 2015-2017 Kathyrn Gray */ +/* All rights reserved. */ +/* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*========================================================================*/ + +/* misp_insts.sail: mips instruction decode and execute clauses and AST node + declarations */ + +scattered union ast + +val execute : ast -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg} +scattered function execute + +val decode : bits(32) -> option(ast) effect pure +scattered function decode diff --git a/mips/mips_epilogue.sail b/mips/mips_epilogue.sail new file mode 100644 index 00000000..c7477a50 --- /dev/null +++ b/mips/mips_epilogue.sail @@ -0,0 +1,42 @@ +/*========================================================================*/ +/* */ +/* Copyright (c) 2015-2017 Robert M. Norton */ +/* Copyright (c) 2015-2017 Kathyrn Gray */ +/* All rights reserved. */ +/* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*========================================================================*/ + +/* mips_epilogue.sail: end of decode, execute and AST definitions. */ + +end decode +end execute +end ast + +val supported_instructions : ast -> option(ast) +function supported_instructions instr = Some(instr) diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem new file mode 100644 index 00000000..920277f6 --- /dev/null +++ b/mips/mips_extras.lem @@ -0,0 +1,94 @@ +open import Pervasives +open import Pervasives_extra +open import Sail_instr_kinds +open import Sail_values +open import Sail_operators +open import Prompt_monad +open import Prompt + +val MEMr : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e +val MEMr_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e +val MEMr_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e +val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e + +let MEMr addr size = read_mem Read_plain addr size +let MEMr_reserve addr size = read_mem Read_reserve addr size + +let MEMr_tag addr size = + read_mem Read_plain addr size >>= fun v -> + read_tag addr >>= fun t -> + return (bool_of_bitU t, v) + +let MEMr_tag_reserve addr size = + read_mem Read_plain addr size >>= fun v -> + read_tag addr >>= fun t -> + return (bool_of_bitU t, v) + + +val MEMea : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e +val MEMea_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e +val MEMea_tag : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e +val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e + +let MEMea addr size = write_mem_ea Write_plain addr size +let MEMea_conditional addr size = write_mem_ea Write_conditional addr size + +let MEMea_tag addr size = write_mem_ea Write_plain addr size +let MEMea_tag_conditional addr size = write_mem_ea Write_conditional addr size + + +val MEMval : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval unit 'e +val MEMval_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval bool 'e +val MEMval_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval unit 'e +val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e + +let MEMval _ size v = write_mem_val v >>= fun _ -> return () +let MEMval_conditional _ size v = write_mem_val v >>= fun b -> return (if b then true else false) +let MEMval_tag _ size t v = write_mem_val v >>= fun _ -> write_tag_val (bitU_of_bool t) >>= fun _ -> return () +let MEMval_tag_conditional _ size t v = write_mem_val v >>= fun b -> write_tag_val (bitU_of_bool t) >>= fun _ -> return (if b then true else false) + +val MEM_sync : forall 'regval 'e. unit -> monad 'regval unit 'e + +let MEM_sync () = barrier Barrier_MIPS_SYNC + +(* Some wrappers copied from aarch64_extras *) +(* TODO: Harmonise into a common library *) + +let get_slice_int_bl len n lo = + (* TODO: Is this the intended behaviour? *) + let hi = lo + len - 1 in + let bits = bits_of_int (hi + 1) n in + get_bits false bits hi lo + +val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a +let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo) + +let write_ram _ size _ addr data = + MEMea addr size >> + MEMval addr size data + +let read_ram _ size _ addr = MEMr addr size + +let sign_extend bits len = exts_bv len bits +let zero_extend bits len = extz_bv len bits + +let shift_bits_left v n = shiftl_bv v (unsigned n) +let shift_bits_right v n = shiftr_bv v (unsigned n) +let shift_bits_right_arith v n = arith_shiftr_bv v (unsigned n) + +(* TODO: These could be monadic instead of hardcoded *) +let internal_pick vs = head vs +let undefined_string () = "" +let undefined_unit () = () +let undefined_int () = (0:ii) +let undefined_bool () = false +val undefined_vector : forall 'a. integer -> 'a -> list 'a +let undefined_vector len u = repeat [u] len +val undefined_bitvector : forall 'a. Bitvector 'a => integer -> 'a +let undefined_bitvector len = of_bits (repeat [B0] len) +let undefined_bits len = undefined_bitvector len +let undefined_bit () = B0 +let undefined_real () = realFromFrac 0 1 +let undefined_range i j = i +let undefined_atom i = i +let undefined_nat () = (0:ii) diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail new file mode 100644 index 00000000..e8f9a0f7 --- /dev/null +++ b/mips/mips_insts.sail @@ -0,0 +1,1708 @@ +/*========================================================================*/ +/* */ +/* Copyright (c) 2015-2017 Robert M. Norton */ +/* Copyright (c) 2015-2017 Kathyrn Gray */ +/* All rights reserved. */ +/* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*========================================================================*/ + +/* misp_insts.sail: mips instruction decode and execute clauses and AST node + declarations */ + +/**************************************************************************************/ +/* [D]ADD[I][U] various forms of ADD */ +/**************************************************************************************/ + +/* DADDIU Doubleword Add Immediate Unsigned -- + the simplest possible instruction, no undefined behaviour or exceptions + reg, reg, immediate */ + +union clause ast = DADDIU : (regno, regno, imm16) + +function clause decode (0b011001 @ rs : regno @ rt : regno @ imm : imm16) = + Some(DADDIU(rs, rt, imm)) + +function clause execute (DADDIU (rs, rt, imm)) = + { + wGPR(rt) = rGPR(rs) + EXTS(imm) + } + +/* DADDU Doubleword Add Unsigned -- another very simple instruction, + reg, reg, reg */ + +union clause ast = DADDU : (regno, regno, regno) + +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101101) = + Some(DADDU(rs, rt, rd)) + +function clause execute (DADDU (rs, rt, rd)) = + { + wGPR(rd) = rGPR(rs) + rGPR(rt) + } + +/* DADDI Doubleword Add Immediate + reg, reg, imm with possible exception */ + +union clause ast = DADDI : (regno, regno, bits(16)) + +function clause decode (0b011000 @ rs : regno @ rt : regno @ imm : imm16) = + Some(DADDI(rs, rt, imm)) + +function clause execute (DADDI (rs, rt, imm)) = + { + let sum65 : bits(65) = EXTS(rGPR(rs)) + EXTS(imm) in + { + if (sum65[64] != sum65[63]) then + (SignalException(Ov)) + else + wGPR(rt) = sum65[63..0] + } + } + +/* DADD Doubleword Add + reg, reg, reg with possible exception */ + +union clause ast = DADD : (regno, regno, regno) + +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101100) = + Some(DADD(rs, rt, rd)) + +function clause execute (DADD (rs, rt, rd)) = + { + let sum65 : bits(65) = EXTS(rGPR(rs)) + EXTS(rGPR(rt)) in + { + if sum65[64] != sum65[63] then + (SignalException(Ov)) + else + wGPR(rd) = sum65[63..0] + } + } + +/* ADD 32-bit add -- reg, reg, reg with possible undefined behaviour or exception */ + +union clause ast = ADD : (regno, regno, regno) + +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100000) = + Some(ADD(rs, rt, rd)) + +function clause execute (ADD(rs, rt, rd)) = + { + opA : bits(64) = rGPR(rs); + opB : bits(64) = rGPR(rt); + if NotWordVal(opA) | NotWordVal(opB) then + wGPR(rd) = undefined /* XXX could exit instead */ + else + let sum33 : bits(33) = EXTS(opA[31 .. 0]) + EXTS(opB[31 .. 0])in + if sum33[32] != sum33[31] then + (SignalException(Ov)) + else + wGPR(rd) = EXTS(sum33[31..0]) + } + +/* ADDI 32-bit add immediate -- reg, reg, imm with possible undefined behaviour or exception */ + +union clause ast = ADDI : (regno, regno, bits(16)) + +function clause decode (0b001000 @ rs : regno @ rt : regno @ imm : imm16) = + Some(ADDI(rs, rt, imm)) + +function clause execute (ADDI(rs, rt, imm)) = + { + opA = rGPR(rs); + if NotWordVal(opA) then + wGPR(rt) = undefined /* XXX could exit instead */ + else + let sum33 : bits(33) = EXTS(opA[31 .. 0]) + EXTS(imm) in + if sum33[32] != sum33[31] then + (SignalException(Ov)) + else + wGPR(rt) = EXTS(sum33[31..0]) + } + +/* ADDU 32-bit add immediate -- reg, reg, reg with possible undefined behaviour */ + +union clause ast = ADDU : (regno, regno, regno) + +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100001) = + Some(ADDU(rs, rt, rd)) + +function clause execute (ADDU(rs, rt, rd)) = + { + opA = rGPR(rs); + opB = rGPR(rt); + if NotWordVal(opA) | NotWordVal(opB) then + wGPR(rd) = undefined + else + wGPR(rd) = EXTS(opA[31..0] + opB[31..0]) + } + + +/* ADDIU 32-bit add immediate -- reg, reg, imm with possible undefined behaviour */ + +union clause ast = ADDIU : (regno, regno, bits(16)) + +function clause decode (0b001001 @ rs : regno @ rt : regno @ imm : imm16) = + Some(ADDIU(rs, rt, imm)) + +function clause execute (ADDIU(rs, rt, imm)) = + { + opA = rGPR(rs); + if NotWordVal(opA) then + wGPR(rt) = undefined /* XXX could exit instead */ + else + wGPR(rt) = EXTS((opA[31 .. 0]) + EXTS(imm)) + } + +/**************************************************************************************/ +/* [D]SUB[U] various forms of SUB */ +/**************************************************************************************/ + +/* DSUBU doubleword subtract 'unsigned' reg, reg, reg */ + +union clause ast = DSUBU : (regno, regno, regno) + +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101111) = + Some(DSUBU(rs, rt, rd)) + +function clause execute (DSUBU (rs, rt, rd)) = + { + wGPR(rd) = rGPR(rs) - rGPR(rt) + } + +/* DSUB reg, reg, reg with possible exception */ + +union clause ast = DSUB : (regno, regno, regno) + +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101110) = + Some(DSUB(rs, rt, rd)) + +function clause execute (DSUB (rs, rt, rd)) = + { + let temp65 : bits(65) = EXTS(rGPR(rs)) - EXTS(rGPR(rt)) in + { + if temp65[64] != temp65[63] then + (SignalException(Ov)) + else + wGPR(rd) = temp65[63..0] + } + } + +/* SUB 32-bit sub -- reg, reg, reg with possible undefined behaviour or exception */ + +union clause ast = SUB : (regno, regno, regno) + +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100010) = + Some(SUB(rs, rt, rd)) + +function clause execute (SUB(rs, rt, rd)) = + { + opA = rGPR(rs); + opB = rGPR(rt); + if NotWordVal(opA) | NotWordVal(opB) then + wGPR(rd) = undefined /* XXX could instead */ + else + let temp33 : bits(33) = EXTS(opA[31..0]) - EXTS(opB[31..0]) in + if temp33[32] != temp33[31] then + (SignalException(Ov)) + else + wGPR(rd) = EXTS(temp33[31..0]) + } + +/* SUBU 32-bit 'unsigned' sub -- reg, reg, reg with possible undefined behaviour */ + +union clause ast = SUBU : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100011) = + Some(SUBU(rs, rt, rd)) + +function clause execute (SUBU(rs, rt, rd)) = + { + opA = rGPR(rs); + opB = rGPR(rt); + if NotWordVal(opA) | NotWordVal(opB) then + wGPR(rd) = undefined + else + wGPR(rd) = EXTS(opA[31..0] - opB[31..0]) + } + +/**************************************************************************************/ +/* Logical bitwise operations */ +/**************************************************************************************/ + +/* AND reg, reg, reg */ + +union clause ast = AND : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100100) = + Some(AND(rs, rt, rd)) + +function clause execute (AND (rs, rt, rd)) = + { + wGPR(rd) = (rGPR(rs) & rGPR(rt)) + } + +/* ANDI reg, reg, imm */ + +union clause ast = ANDI : (regno, regno, bits(16)) +function clause decode (0b001100 @ rs : regno @ rt : regno @ imm : imm16) = + Some(ANDI(rs, rt, imm)) +function clause execute (ANDI (rs, rt, imm)) = + { + wGPR(rt) = (rGPR(rs) & EXTZ(imm)) + } + +/* OR reg, reg, reg */ + +union clause ast = OR : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100101) = + Some(OR(rs, rt, rd)) +function clause execute (OR (rs, rt, rd)) = + { + wGPR(rd) = (rGPR(rs) | rGPR(rt)) + } + +/* ORI reg, reg, imm */ + +union clause ast = ORI : (regno, regno, bits(16)) +function clause decode (0b001101 @ rs : regno @ rt : regno @ imm : imm16) = + Some(ORI(rs, rt, imm)) +function clause execute (ORI (rs, rt, imm)) = + { + wGPR(rt) = (rGPR(rs) | EXTZ(imm)) + } + +/* NOR reg, reg, reg */ + +union clause ast = NOR : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100111) = + Some(NOR(rs, rt, rd)) +function clause execute (NOR (rs, rt, rd)) = + { + wGPR(rd) = ~(rGPR(rs) | rGPR(rt)) + } + +/* XOR reg, reg, reg */ + +union clause ast = XOR : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b100110) = + Some(XOR(rs, rt, rd)) +function clause execute (XOR (rs, rt, rd)) = + { + wGPR(rd) = (rGPR(rs) ^ rGPR(rt)) + } + +/* XORI reg, reg, imm */ +union clause ast = XORI : (regno, regno, bits(16)) +function clause decode (0b001110 @ rs : regno @ rt : regno @ imm : imm16) = + Some(XORI(rs, rt, imm)) +function clause execute (XORI (rs, rt, imm)) = + { + wGPR(rt) = (rGPR(rs) ^ EXTZ(imm)) + } + +/* LUI reg, imm 32-bit load immediate into upper 16 bits */ +union clause ast = LUI : (regno, imm16) +function clause decode (0b001111 @ 0b00000 @ rt : regno @ imm : imm16) = + Some(LUI(rt, imm)) +function clause execute (LUI (rt, imm)) = + { + wGPR(rt) = EXTS(imm @ 0x0000) + } + +/**************************************************************************************/ +/* 64-bit shift operations */ +/**************************************************************************************/ + +/* DSLL reg, reg, imm5 */ + +union clause ast = DSLL : (regno, regno, regno) +function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111000) = + Some(DSLL(rt, rd, sa)) +function clause execute (DSLL (rt, rd, sa)) = + { + + wGPR(rd) = (rGPR(rt) << sa) + } + +/* DSLL32 reg, reg, imm5 */ + +union clause ast = DSLL32 : (regno, regno, regno) +function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111100) = + Some(DSLL32(rt, rd, sa)) +function clause execute (DSLL32 (rt, rd, sa)) = + { + wGPR(rd) = (rGPR(rt) << (0b1 @ sa)) + } + +/* DSLLV reg, reg, reg */ + +union clause ast = DSLLV : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b010100) = + Some(DSLLV(rs, rt, rd)) +function clause execute (DSLLV (rs, rt, rd)) = + { + wGPR(rd) = (rGPR(rt) << ((rGPR(rs))[5 .. 0])) + } + +/* DSRA arithmetic shift duplicating sign bit - reg, reg, imm5 */ + +union clause ast = DSRA : (regno, regno, regno) +function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111011) = + Some(DSRA(rt, rd, sa)) +function clause execute (DSRA (rt, rd, sa)) = + { + temp = rGPR(rt); + wGPR(rd) = temp >>_s sa + } + +/* DSRA32 reg, reg, imm5 */ + +union clause ast = DSRA32 : (regno, regno, regno) +function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111111) = + Some(DSRA32(rt, rd, sa)) +function clause execute (DSRA32 (rt, rd, sa)) = + { + temp = rGPR(rt); + sa32 = 0b1 @ sa; /* sa+32 */ + wGPR(rd) = temp >>_s sa32 + } + +/* DSRAV reg, reg, reg */ +union clause ast = DSRAV : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b010111) = + Some(DSRAV(rs, rt, rd)) +function clause execute (DSRAV (rs, rt, rd)) = + { + temp = rGPR(rt); + sa = rGPR(rs)[5..0]; + wGPR(rd) = temp >>_s sa + } + +/* DSRL shift right logical - reg, reg, imm5 */ + +union clause ast = DSRL : (regno, regno, regno) +function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111010) = + Some(DSRL(rt, rd, sa)) +function clause execute (DSRL (rt, rd, sa)) = + { + temp = rGPR(rt); + wGPR(rd) = temp >> sa; + } + +/* DSRL32 reg, reg, imm5 */ + +union clause ast = DSRL32 : (regno, regno, regno) +function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : bits(5) @ 0b111110) = + Some(DSRL32(rt, rd, sa)) +function clause execute (DSRL32 (rt, rd, sa)) = + { + temp = rGPR(rt); + sa32 = 0b1 @ sa; /* sa+32 */ + wGPR(rd) = temp >> sa32; + } + +/* DSRLV reg, reg, reg */ + +union clause ast = DSRLV : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b010110) = + Some(DSRLV(rs, rt, rd)) +function clause execute (DSRLV (rs, rt, rd)) = + { + temp = rGPR(rt); + sa = rGPR(rs)[5..0]; + wGPR(rd) = temp >> sa; + } + +/**************************************************************************************/ +/* 32-bit shift operations */ +/**************************************************************************************/ + +/* SLL 32-bit shift left */ + +union clause ast = SLL : (regno, regno, regno) +function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : regno @ 0b000000) = + Some(SLL(rt, rd, sa)) +function clause execute (SLL(rt, rd, sa)) = + { + rt32 = rGPR(rt)[31..0]; + wGPR(rd) = EXTS(rt32 << sa); + } + +/* SLLV 32-bit shift left variable */ + +union clause ast = SLLV : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b000100) = + Some(SLLV(rs, rt, rd)) +function clause execute (SLLV(rs, rt, rd)) = + { + sa = rGPR(rs)[4..0]; + rt32 = rGPR(rt)[31..0]; + wGPR(rd) = EXTS(rt32 << sa) + } + +/* SRA 32-bit arithmetic shift right */ + +union clause ast = SRA : (regno, regno, regno) +function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : regno @ 0b000011) = + Some(SRA(rt, rd, sa)) +function clause execute (SRA(rt, rd, sa)) = + { + temp = rGPR(rt); + if (NotWordVal(temp)) then + wGPR(rd) = undefined + else { + rt32 = temp[31..0]; + wGPR(rd) = EXTS(rt32 >>_s sa); + } + } + +/* SRAV 32-bit arithmetic shift right variable */ + +union clause ast = SRAV : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b000111) = + Some(SRAV(rs, rt, rd)) +function clause execute (SRAV(rs, rt, rd)) = + { + temp = rGPR(rt); + sa = rGPR(rs)[4..0]; + if (NotWordVal(temp)) then + wGPR(rd) = undefined + else { + rt32 = temp[31..0]; + wGPR(rd) = EXTS(rt32 >>_s sa) + } + } + +/* SRL 32-bit shift right */ + +union clause ast = SRL : (regno, regno, regno) +function clause decode (0b000000 @ 0b00000 @ rt : regno @ rd : regno @ sa : regno @ 0b000010) = + Some(SRL(rt, rd, sa)) +function clause execute (SRL(rt, rd, sa)) = + { + temp = rGPR(rt); + if (NotWordVal(temp)) then + wGPR(rd) = undefined + else { + rt32 = temp[31..0]; + wGPR(rd) = EXTS(rt32 >> sa); + } + } + +/* SRLV 32-bit shift right variable */ + +union clause ast = SRLV : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b000110) = + Some(SRLV(rs, rt, rd)) +function clause execute (SRLV(rs, rt, rd)) = + { + temp = rGPR(rt); + sa = (rGPR(rs))[4..0]; + if (NotWordVal(temp)) then + wGPR(rd) = undefined + else { + rt32 = temp[31..0]; + wGPR(rd) = EXTS(rt32 >> sa); + } + } + +/**************************************************************************************/ +/* set less than / conditional move */ +/**************************************************************************************/ + +/* SLT set if less than (signed) */ + +union clause ast = SLT : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101010) = + Some(SLT(rs, rt, rd)) +function clause execute (SLT(rs, rt, rd)) = + { + wGPR(rd) = EXTZ(if (rGPR(rs) <_s rGPR(rt)) then 0b1 else 0b0) + } + +/* SLT set if less than immediate (signed) */ + +union clause ast = SLTI : (regno, regno, bits(16)) +function clause decode (0b001010 @ rs : regno @ rt : regno @ imm : imm16) = + Some(SLTI(rs, rt, imm)) +function clause execute (SLTI(rs, rt, imm)) = + { + let imm_val = signed(imm) in + let rs_val = signed(rGPR(rs)) in + wGPR(rt) = EXTZ(if (rs_val < imm_val) then 0b1 else 0b0) + } + +/* SLTU set if less than unsigned */ + +union clause ast = SLTU : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b101011) = + Some(SLTU(rs, rt, rd)) +function clause execute (SLTU(rs, rt, rd)) = + { + let rs_val = rGPR(rs) in + let rt_val = rGPR(rt) in + wGPR(rd) = EXTZ(if (rs_val <_u rt_val) then 0b1 else 0b0) + } + +/* SLTIU set if less than immediate unsigned */ + +union clause ast = SLTIU : (regno, regno, bits(16)) +function clause decode (0b001011 @ rs : regno @ rt : regno @ imm : imm16) = + Some(SLTIU(rs, rt, imm)) +function clause execute (SLTIU(rs, rt, imm)) = + { + let rs_val = rGPR(rs) in + let immext : bits(64) = EXTS(imm) in /* NB defined to sign extend here even though comparison is unsigned! */ + wGPR(rt) = EXTZ(if (rs_val <_u immext) then 0b1 else 0b0) + } + +/* MOVN move if non-zero */ + +union clause ast = MOVN : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b001011) = + Some(MOVN(rs, rt, rd)) +function clause execute (MOVN(rs, rt, rd)) = + { + if (rGPR(rt) != 0x0000000000000000) then + wGPR(rd) = rGPR(rs) + } + +/* MOVZ move if zero */ + +union clause ast = MOVZ : (regno, regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b001010) = + Some(MOVZ(rs, rt, rd)) +function clause execute (MOVZ(rs, rt, rd)) = + { + if (rGPR(rt) == 0x0000000000000000) then + wGPR(rd) = rGPR(rs) + } + +/******************************************************************************/ +/* MUL/DIV instructions */ +/******************************************************************************/ + +/* MFHI move from HI register */ +union clause ast = MFHI : regno +function clause decode (0b000000 @ 0b0000000000 @ rd : regno @ 0b00000 @ 0b010000) = + Some(MFHI(rd)) +function clause execute (MFHI(rd)) = + { + wGPR(rd) = HI + } + +/* MFLO move from LO register */ +union clause ast = MFLO : regno +function clause decode (0b000000 @ 0b0000000000 @ rd : regno @ 0b00000 @ 0b010010) = + Some(MFLO(rd)) +function clause execute (MFLO(rd)) = + { + wGPR(rd) = LO + } + +/* MTHI move to HI register */ +union clause ast = MTHI : regno +function clause decode (0b000000 @ rs : regno @ 0b000000000000000 @ 0b010001) = + Some(MTHI(rs)) +function clause execute (MTHI(rs)) = + { + HI = rGPR(rs) + } + +/* MTLO move to LO register */ +union clause ast = MTLO : regno +function clause decode (0b000000 @ rs : regno @ 0b000000000000000 @ 0b010011) = + Some(MTLO(rs)) +function clause execute (MTLO(rs)) = + { + LO = rGPR(rs) + } + +/* MUL 32-bit multiply into GPR */ +union clause ast = MUL : (regno, regno, regno) +function clause decode (0b011100 @ rs : regno @ rt : regno @ rd : regno @ 0b00000 @ 0b000010) = + Some(MUL(rs, rt, rd)) +function clause execute (MUL(rs, rt, rd)) = + { + rsVal = rGPR(rs); + rtVal = rGPR(rt); + result : bits(64) = EXTS((rsVal[31..0]) *_s (rtVal[31..0])); + wGPR(rd) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + undefined + else + EXTS(result[31..0]); + /* HI and LO are technically undefined after MUL, but this causes problems with tests and + (potentially) context switch so just leave them alone + HI = undefined; + LO = undefined; + */ + } + +/* MULT 32-bit multiply into HI/LO */ +union clause ast = MULT : (regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011000) = + Some(MULT(rs, rt)) +function clause execute (MULT(rs, rt)) = + { + rsVal = rGPR(rs); + rtVal = rGPR(rt); + result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + undefined + else + (rsVal[31..0]) *_s (rtVal[31..0]); + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); + } + +/* MULTU 32-bit unsignedm rultiply into HI/LO */ +union clause ast = MULTU : (regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011001) = + Some(MULTU(rs, rt)) +function clause execute (MULTU(rs, rt)) = + { + rsVal = rGPR(rs); + rtVal = rGPR(rt); + result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + undefined + else + (rsVal[31..0]) *_u (rtVal[31..0]); + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); + } + +/* DMULT 64-bit multiply into HI/LO */ +union clause ast = DMULT : (regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011100) = + Some(DMULT(rs, rt)) +function clause execute (DMULT(rs, rt)) = + { + result = rGPR(rs) *_s rGPR(rt); + HI = (result[127..64]); + LO = (result[63..0]); + } + +/* DMULTU 64-bit unsigned multiply into HI/LO */ +union clause ast = DMULTU : (regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011101) = + Some(DMULTU(rs, rt)) +function clause execute (DMULTU(rs, rt)) = + { + result = rGPR(rs) *_u rGPR(rt); + HI = (result[127..64]); + LO = (result[63..0]); + } + +/* MADD 32-bit signed multiply and add into HI/LO */ +union clause ast = MADD : (regno, regno) +function clause decode (0b011100 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b000000) = + Some(MADD(rs, rt)) +function clause execute (MADD(rs, rt)) = + { + rsVal = rGPR(rs); + rtVal = rGPR(rt); + mul_result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + undefined + else + rsVal[31..0] *_s rtVal[31..0]; + result = mul_result + (HI[31..0] @ LO[31..0]); + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); + } + +/* MADDU 32-bit unsigned multiply and add into HI/LO */ +union clause ast = MADDU : (regno, regno) +function clause decode (0b011100 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b000001) = + Some(MADDU(rs, rt)) +function clause execute (MADDU(rs, rt)) = + { + rsVal = rGPR(rs); + rtVal = rGPR(rt); + mul_result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + undefined + else + rsVal[31..0] *_u rtVal[31..0]; + result = mul_result + (HI[31..0] @ LO[31..0]); + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); + } + +/* MSUB 32-bit signed multiply and sub from HI/LO */ +union clause ast = MSUB : (regno, regno) +function clause decode (0b011100 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b000100) = + Some(MSUB(rs, rt)) +function clause execute (MSUB(rs, rt)) = + { + rsVal = rGPR(rs); + rtVal = rGPR(rt); + mul_result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + undefined + else + rsVal[31..0] *_s rtVal[31..0]; + result = (HI[31..0] @ LO[31..0]) - mul_result; + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); + } + +/* MSUBU 32-bit unsigned multiply and sub from HI/LO */ +union clause ast = MSUBU : (regno, regno) +function clause decode (0b011100 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b000101) = + Some(MSUBU(rs, rt)) +function clause execute (MSUBU(rs, rt)) = + { + rsVal = rGPR(rs); + rtVal = rGPR(rt); + mul_result : bits(64) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then + undefined + else + rsVal[31..0] *_u rtVal[31..0]; + result = (HI[31..0] @ LO[31..0]) - mul_result; + HI = EXTS(result[63..32]); + LO = EXTS(result[31..0]); + } + +/* DIV 32-bit divide into HI/LO */ +union clause ast = DIV : (regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011010) = + Some(DIV(rs, rt)) +function clause execute (DIV(rs, rt)) = + { + rsVal = rGPR(rs); + rtVal = rGPR(rt); + let (q, r) = + if (NotWordVal(rsVal) | NotWordVal(rtVal) | (rtVal == 0x0000000000000000)) then + (undefined : bits(32), undefined : bits(32)) + else + let si = signed((rsVal[31..0])) in + let ti = signed((rtVal[31..0])) in + let qi = quot_round_zero(si, ti) in + let ri = si - (ti*qi) in + (to_bits(32, qi), to_bits(32, ri)) + in + { + HI = EXTS(r); + LO = EXTS(q); + } + } + +/* DIVU 32-bit unsigned divide into HI/LO */ +union clause ast = DIVU : (regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011011) = + Some(DIVU(rs, rt)) +function clause execute (DIVU(rs, rt)) = + { + rsVal = rGPR(rs); + rtVal = rGPR(rt); + let (q, r) = + if (NotWordVal(rsVal) | NotWordVal(rtVal) | rtVal == 0x0000000000000000) then + (undefined : bits(32), undefined : bits(32)) + else + let si = unsigned(rsVal[31..0]) in + let ti = unsigned(rtVal[31..0]) in + let qi = quot_round_zero(si, ti) in + let ri = rem_round_zero(si, ti) in + (to_bits(32, qi), to_bits(32, ri)) + in + { + HI = EXTS(r); + LO = EXTS(q); + } + } + +/* DDIV 64-bit divide into HI/LO */ +union clause ast = DDIV : (regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011110) = + Some(DDIV(rs, rt)) +function clause execute (DDIV(rs, rt)) = + { + rsVal = signed(rGPR(rs)); + rtVal = signed(rGPR(rt)); + let (q , r) = + if (rtVal == 0) + then (undefined : bits(64), undefined : bits(64)) + else + let qi = quot_round_zero(rsVal, rtVal) in + let ri = (rsVal - (qi * rtVal)) in + (to_bits(64, qi), to_bits(64, ri)) in + { + LO = q; + HI = r; + } + } + +/* DDIV 64-bit divide into HI/LO */ +union clause ast = DDIVU : (regno, regno) +function clause decode (0b000000 @ rs : regno @ rt : regno @ 0b00000 @ 0b00000 @ 0b011111) = + Some(DDIVU(rs, rt)) +function clause execute (DDIVU(rs, rt)) = + { + rsVal = unsigned(rGPR(rs)); + rtVal = unsigned(rGPR(rt)); + let (q, r) = + if (rtVal == 0) + then (undefined : bits(64), undefined : bits(64)) + else + let qi = quot_round_zero(rsVal, rtVal) in + let ri = rem_round_zero(rsVal, rtVal) in + (to_bits(64, qi), to_bits(64, ri)) in + { + LO = q; + HI = r; + } + } + +/**************************************************************************************/ +/* Jump instructions -- unconditional branches */ +/**************************************************************************************/ + +/* J - jump, the simplest control flow instruction, with branch delay slot */ +union clause ast = J : bits(26) +function clause decode (0b000010 @ offset : bits(26)) = + Some(J(offset)) +function clause execute (J(offset)) = + { + delayedPC = (PC + 4)[63..28] @ offset @ 0b00; + branchPending = 0b1 + } + +/* JAL - jump and link */ +union clause ast = JAL : bits(26) +function clause decode (0b000011 @ offset : bits(26)) = + Some(JAL(offset)) +function clause execute (JAL(offset)) = + { + delayedPC = (PC + 4)[63..28] @ offset @ 0b00; + branchPending = 0b1; + wGPR(0b11111) = PC + 8; + } + +/* JR -- jump via register */ +union clause ast = JR : regno +function clause decode (0b000000 @ rs : regno @ 0b00000 @ 0b00000 @ hint : regno @ 0b001000) = + Some(JR(rs)) /* hint is ignored */ +function clause execute (JR(rs)) = + { + delayedPC = rGPR(rs); + branchPending = 0b1; + } + +/* JALR -- jump via register with link */ +union clause ast = JALR : (regno, regno) +function clause decode (0b000000 @ rs : regno @ 0b00000 @ rd : regno @ hint : regno @ 0b001001) = + Some(JALR(rs, rd)) /* hint is ignored */ +function clause execute (JALR(rs, rd)) = + { + delayedPC = rGPR(rs); + branchPending = 0b1; + wGPR(rd) = PC + 8; + } + +/**************************************************************************************/ +/* B[N]EQ[L] - branch on (not) equal (likely) */ +/* Conditional branch instructions with two register operands */ +/**************************************************************************************/ + +union clause ast = BEQ : (regno, regno, imm16, bool, bool) +function clause decode (0b000100 @ rs : regno @ rt : regno @ imm : imm16) = + Some(BEQ(rs, rt, imm, false, false)) /* BEQ */ +function clause decode (0b010100 @ rs : regno @ rt : regno @ imm : imm16) = + Some(BEQ(rs, rt, imm, false, true)) /* BEQL */ +function clause decode (0b000101 @ rs : regno @ rt : regno @ imm : imm16) = + Some(BEQ(rs, rt, imm, true , false)) /* BNE */ +function clause decode (0b010101 @ rs : regno @ rt : regno @ imm : imm16) = + Some(BEQ(rs, rt, imm, true , true)) /* BNEL */ +function clause execute (BEQ(rs, rd, imm, ne, likely)) = + { + if ((rGPR(rs) == rGPR(rd)) ^ ne) then + { + let offset : bits(64) = (EXTS(imm @ 0b00) + 4) in + delayedPC = PC + offset; + branchPending = 0b1; + } + else + { + if (likely) then + nextPC = PC + 8; /* skip branch delay */ + } + } + +/* + + Branches comparing with zero (single register operand, possible link in r31) +*/ + +/**************************************************************************************/ +/* BGEZ[AL][L] - branch on comparison with zero (possibly link, likely) */ +/* Conditional branch instructions with single register operand */ +/**************************************************************************************/ + +union clause ast = BCMPZ : (regno, imm16, Comparison, bool, bool) +function clause decode (0b000001 @ rs : regno @ 0b00000 @ imm : imm16) = + Some(BCMPZ(rs, imm, LT, false, false)) /* BLTZ */ +function clause decode (0b000001 @ rs : regno @ 0b10000 @ imm : imm16) = + Some(BCMPZ(rs, imm, LT, true, false)) /* BLTZAL */ +function clause decode (0b000001 @ rs : regno @ 0b00010 @ imm : imm16) = + Some(BCMPZ(rs, imm, LT, false, true)) /* BLTZL */ +function clause decode (0b000001 @ rs : regno @ 0b10010 @ imm : imm16) = + Some(BCMPZ(rs, imm, LT, true, true)) /* BLTZALL */ + +function clause decode (0b000001 @ rs : regno @ 0b00001 @ imm : imm16) = + Some(BCMPZ(rs, imm, GE, false, false)) /* BGEZ */ +function clause decode (0b000001 @ rs : regno @ 0b10001 @ imm : imm16) = + Some(BCMPZ(rs, imm, GE, true, false)) /* BGEZAL */ +function clause decode (0b000001 @ rs : regno @ 0b00011 @ imm : imm16) = + Some(BCMPZ(rs, imm, GE, false, true)) /* BGEZL */ +function clause decode (0b000001 @ rs : regno @ 0b10011 @ imm : imm16) = + Some(BCMPZ(rs, imm, GE, true, true)) /* BGEZALL */ + +function clause decode (0b000111 @ rs : regno @ 0b00000 @ imm : imm16) = + Some(BCMPZ(rs, imm, GT, false, false)) /* BGTZ */ +function clause decode (0b010111 @ rs : regno @ 0b00000 @ imm : imm16) = + Some(BCMPZ(rs, imm, GT, false, true)) /* BGTZL */ + +function clause decode (0b000110 @ rs : regno @ 0b00000 @ imm : imm16) = + Some(BCMPZ(rs, imm, LE, false, false)) /* BLEZ */ +function clause decode (0b010110 @ rs : regno @ 0b00000 @ imm : imm16) = + Some(BCMPZ(rs, imm, LE, false, true)) /* BLEZL */ + +function clause execute (BCMPZ(rs, imm, cmp, link, likely)) = + { + linkVal = PC + 8; + regVal = rGPR(rs); + condition = compare(cmp, regVal, EXTZ(0b0)); + if (condition) then + { + let offset : bits(64) = (EXTS(imm @ 0b00) + 4) in + delayedPC = PC + offset; + branchPending = 0b1; + } + else if (likely) then + { + nextPC = PC + 8 /* skip branch delay */ + }; + if (link) then + wGPR(0b11111) = linkVal + } + +/**************************************************************************************/ +/* SYSCALL/BREAK/WAIT/Trap */ +/**************************************************************************************/ + +/* Co-opt syscall 0xfffff for use as thread start in pccmem */ +union clause ast = SYSCALL_THREAD_START : unit +function clause decode (0b000000 @ 0xfffff @ 0b001100) = + Some(SYSCALL_THREAD_START()) +function clause execute (SYSCALL_THREAD_START()) = () + + +/* fake stop fetching instruction for ppcmem, execute doesn't do anything, + decode never produces it */ + +union clause ast = ImplementationDefinedStopFetching : unit +function clause execute (ImplementationDefinedStopFetching()) = () + + +union clause ast = SYSCALL : unit +function clause decode (0b000000 @ code : bits(20) @ 0b001100) = + Some(SYSCALL()) /* code is ignored */ +function clause execute (SYSCALL()) = + { + (SignalException(Sys)) + } + +/* BREAK is identical to SYSCALL exception for the exception raised */ +union clause ast = BREAK : unit +function clause decode (0b000000 @ code : bits(20) @ 0b001101) = + Some(BREAK()) /* code is ignored */ +function clause execute (BREAK()) = + { + (SignalException(Bp)) + } + +/* Accept WAIT as a NOP */ +union clause ast = WAIT : unit +function clause decode (0b010000 @ 0x80000 @ 0b100000) = + Some(WAIT()) /* we only accept code == 0 */ +function clause execute (WAIT()) = { + nextPC = PC; +} + +/* Trap instructions with two register operands */ +union clause ast = TRAPREG : (regno, regno, Comparison) +function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 0b110000) = + Some(TRAPREG(rs, rt, GE)) /* TGE */ +function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 0b110001) = + Some(TRAPREG(rs, rt, GEU)) /* TGEU */ +function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 0b110010) = + Some(TRAPREG(rs, rt, LT)) /* TLT */ +function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 0b110011) = + Some(TRAPREG(rs, rt, LTU)) /* TLTU */ +function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 0b110100) = + Some(TRAPREG(rs, rt, EQ)) /* TEQ */ +function clause decode (0b000000 @ rs : regno @ rt : regno @ code : bits(10) @ 0b110110) = + Some(TRAPREG(rs, rt, NE)) /* TNE */ +function clause execute (TRAPREG(rs, rt, cmp)) = + { + rs_val = rGPR(rs); + rt_val = rGPR(rt); + condition = compare(cmp, rs_val, rt_val); + if (condition) then + (SignalException(Tr)) + } + + +/* Trap instructions with one register and one immediate operand */ +union clause ast = TRAPIMM : (regno, imm16, Comparison) +function clause decode (0b000001 @ rs : regno @ 0b01100 @ imm : imm16) = + Some(TRAPIMM(rs, imm, EQ)) /* TEQI */ +function clause decode (0b000001 @ rs : regno @ 0b01110 @ imm : imm16) = + Some(TRAPIMM(rs, imm, NE)) /* TNEI */ +function clause decode (0b000001 @ rs : regno @ 0b01000 @ imm : imm16) = + Some(TRAPIMM(rs, imm, GE)) /* TGEI */ +function clause decode (0b000001 @ rs : regno @ 0b01001 @ imm : imm16) = + Some(TRAPIMM(rs, imm, GEU)) /* TGEIU */ +function clause decode (0b000001 @ rs : regno @ 0b01010 @ imm : imm16) = + Some(TRAPIMM(rs, imm, LT)) /* TLTI */ +function clause decode (0b000001 @ rs : regno @ 0b01011 @ imm : imm16) = + Some(TRAPIMM(rs, imm, LTU)) /* TLTIU */ +function clause execute (TRAPIMM(rs, imm, cmp)) = + { + rs_val = rGPR(rs); + imm_val : bits(64) = EXTS(imm); + condition = compare(cmp, rs_val, imm_val); + if (condition) then + (SignalException(Tr)) + } + +/**************************************************************************************/ +/* Load instructions -- various width/signs */ +/**************************************************************************************/ + +union clause ast = Load : (WordType, bool, bool, regno, regno, imm16) +function clause decode (0b100000 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(B, true, false, base, rt, offset)) /* LB */ +function clause decode (0b100100 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(B, false, false, base, rt, offset)) /* LBU */ +function clause decode (0b100001 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(H, true, false, base, rt, offset)) /* LH */ +function clause decode (0b100101 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(H, false, false, base, rt, offset)) /* LHU */ +function clause decode (0b100011 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(W, true, false, base, rt, offset)) /* LW */ +function clause decode (0b100111 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(W, false, false, base, rt, offset)) /* LWU */ +function clause decode (0b110111 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(D, false, false, base, rt, offset)) /* LD */ +function clause decode (0b110000 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(W, true, true, base, rt, offset)) /* LL */ +function clause decode (0b110100 @ base : regno @ rt : regno @ offset : imm16) = + Some(Load(D, false, true, base, rt, offset)) /* LLD */ + +val extendLoad : forall 'sz, 'sz <= 64 . (bits('sz), bool) -> bits(64) effect pure +function extendLoad(memResult, sign) = { + if (sign) then + EXTS(memResult) + else + EXTZ(memResult) +} + +function clause execute (Load(width, sign, linked, base, rt, offset)) = + { + vAddr : bits(64) = addrWrapper(EXTS(offset) + rGPR(base), LoadData, width); + if ~ (isAddressAligned(vAddr, width)) then + (SignalExceptionBadAddr(AdEL, vAddr)) /* unaligned access */ + else + let pAddr = (TLBTranslate(vAddr, LoadData)) in + { + memResult : bits(64) = if (linked) then + { + CP0LLBit = 0b1; + CP0LLAddr = pAddr; + match width { + B => extendLoad(MEMr_reserve_wrapper(pAddr, 1), sign), + H => extendLoad(MEMr_reserve_wrapper(pAddr, 2), sign), + W => extendLoad(MEMr_reserve_wrapper(pAddr, 4), sign), + D => extendLoad(MEMr_reserve_wrapper(pAddr, 8), sign) + } + } + else + { + match width { + B => extendLoad(MEMr_wrapper(pAddr, 1), sign), + H => extendLoad(MEMr_wrapper(pAddr, 2), sign), + W => extendLoad(MEMr_wrapper(pAddr, 4), sign), + D => extendLoad(MEMr_wrapper(pAddr, 8), sign) + } + }; + wGPR(rt) = memResult + } + } + +/**************************************************************************************/ +/* Store instructions -- various widths */ +/**************************************************************************************/ + +union clause ast = Store : (WordType, bool, regno, regno, imm16) +function clause decode (0b101000 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(B, false, base, rt, offset)) /* SB */ +function clause decode (0b101001 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(H, false, base, rt, offset)) /* SH */ +function clause decode (0b101011 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(W, false, base, rt, offset)) /* SW */ +function clause decode (0b111111 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(D, false, base, rt, offset)) /* SD */ +function clause decode (0b111000 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(W, true, base, rt, offset)) /* SC */ +function clause decode (0b111100 @ base : regno @ rt : regno @ offset : imm16) = + Some(Store(D, true, base, rt, offset)) /* SCD */ +function clause execute (Store(width, conditional, base, rt, offset)) = + { + vAddr : bits(64) = addrWrapper(EXTS(offset) + rGPR(base), StoreData, width); + rt_val = rGPR(rt); + if ~ (isAddressAligned(vAddr, width)) then + (SignalExceptionBadAddr(AdES, vAddr)) /* unaligned access */ + else + let pAddr = (TLBTranslate(vAddr, StoreData)) in + { + if (conditional) then + { + success : bool = if (CP0LLBit[0]) then match width + { + B => MEMw_conditional_wrapper(pAddr, 1, rt_val[7..0]), + H => MEMw_conditional_wrapper(pAddr, 2, rt_val[15..0]), + W => MEMw_conditional_wrapper(pAddr, 4, rt_val[31..0]), + D => MEMw_conditional_wrapper(pAddr, 8, rt_val) + } else false; + wGPR(rt) = EXTZ(success) + } + else + match width + { + B => MEMw_wrapper(pAddr, 1) = rt_val[7..0], + H => MEMw_wrapper(pAddr, 2) = rt_val[15..0], + W => MEMw_wrapper(pAddr, 4) = rt_val[31..0], + D => MEMw_wrapper(pAddr, 8) = rt_val + } + } + } + +/* LWL - Load word left (big-endian only) */ + +union clause ast = LWL : (regno, regno, bits(16)) +function clause decode(0b100010 @ base : regno @ rt : regno @ offset : imm16) = + Some(LWL(base, rt, offset)) +function clause execute(LWL(base, rt, offset)) = + { + /* XXX length check not quite right, but conservative */ + vAddr = addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); + let pAddr = (TLBTranslate(vAddr, LoadData)) in + { + mem_val = MEMr_wrapper (pAddr[63..2] @ 0b00, 4); /* read word of interest */ + reg_val = rGPR(rt); + result : bits(32) = match vAddr[1..0] + { + 0b00 => mem_val, + 0b01 => mem_val[23..0] @ reg_val[07..0], + 0b10 => mem_val[15..0] @ reg_val[15..0], + 0b11 => mem_val[07..0] @ reg_val[23..0] + }; + wGPR(rt) = EXTS(result); + } + } +union clause ast = LWR : (regno, regno, bits(16)) +function clause decode(0b100110 @ base : regno @ rt : regno @ offset : imm16) = + Some(LWR(base, rt, offset)) +function clause execute(LWR(base, rt, offset)) = + { + /* XXX length check not quite right, but conservative */ + vAddr = addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); + let pAddr = (TLBTranslate(vAddr, LoadData)) in + { + mem_val = MEMr_wrapper(pAddr[63..2] @ 0b00, 4); /* read word of interest */ + reg_val = rGPR(rt); + result : bits(32) = match vAddr[1..0] + { + 0b00 => reg_val[31..8] @ mem_val[31..24], + 0b01 => reg_val[31..16] @ mem_val[31..16], + 0b10 => reg_val[31..24] @ mem_val[31..8], + 0b11 => mem_val + }; + wGPR(rt) = EXTS(result) + } + } + +/* SWL - Store word left */ +union clause ast = SWL : (regno, regno, bits(16)) +function clause decode(0b101010 @ base : regno @ rt : regno @ offset : imm16) = + Some(SWL(base, rt, offset)) +function clause execute(SWL(base, rt, offset)) = + { + /* XXX length check not quite right, but conservative */ + vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, W); + let pAddr = TLBTranslate(vAddr, StoreData) in + { + reg_val = rGPR(rt); + match vAddr[1..0] + { + 0b00 => (MEMw_wrapper(pAddr, 4) = reg_val[31..0]), + 0b01 => (MEMw_wrapper(pAddr, 3) = reg_val[31..8]), + 0b10 => (MEMw_wrapper(pAddr, 2) = reg_val[31..16]), + 0b11 => (MEMw_wrapper(pAddr, 1) = reg_val[31..24]) + } + } + } + +union clause ast = SWR : (regno, regno, bits(16)) +function clause decode(0b101110 @ base : regno @ rt : regno @ offset : imm16) = + Some(SWR(base, rt, offset)) +function clause execute(SWR(base, rt, offset)) = + { + /* XXX length check not quite right, but conservative */ + vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, W); + let pAddr = TLBTranslate(vAddr, StoreData) in + { + wordAddr = pAddr[63..2] @ 0b00; + reg_val = rGPR(rt); + match vAddr[1..0] + { + 0b00 => (MEMw_wrapper(wordAddr, 1) = reg_val[7..0]), + 0b01 => (MEMw_wrapper(wordAddr, 2) = reg_val[15..0]), + 0b10 => (MEMw_wrapper(wordAddr, 3) = reg_val[23..0]), + 0b11 => (MEMw_wrapper(wordAddr, 4) = reg_val[31..0]) + } + } + } + +/* Load double-word left */ +union clause ast = LDL : (regno, regno, bits(16)) +function clause decode(0b011010 @ base : regno @ rt : regno @ offset : imm16) = + Some(LDL(base, rt, offset)) +function clause execute(LDL(base, rt, offset)) = + { + /* XXX length check not quite right, but conservative */ + vAddr = addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); + let pAddr = TLBTranslate(vAddr, StoreData) in + { + mem_val = MEMr_wrapper(pAddr[63..3] @ 0b000, 8); /* read double of interest */ + reg_val = rGPR(rt); + wGPR(rt) = match vAddr[2..0] + { + 0b000 => mem_val, + 0b001 => mem_val[55..0] @ reg_val[7..0], + 0b010 => mem_val[47..0] @ reg_val[15..0], + 0b011 => mem_val[39..0] @ reg_val[23..0], + 0b100 => mem_val[31..0] @ reg_val[31..0], + 0b101 => mem_val[23..0] @ reg_val[39..0], + 0b110 => mem_val[15..0] @ reg_val[47..0], + 0b111 => mem_val[07..0] @ reg_val[55..0] + }; + } + } + +/* Load double-word right */ +union clause ast = LDR : (regno, regno, bits(16)) +function clause decode(0b011011 @ base : regno @ rt : regno @ offset : imm16) = + Some(LDR(base, rt, offset)) +function clause execute(LDR(base, rt, offset)) = + { + /* XXX length check not quite right, but conservative */ + vAddr = addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); + let pAddr = TLBTranslate(vAddr, StoreData) in + { + mem_val = MEMr_wrapper(pAddr[63..3] @ 0b000, 8); /* read double of interest */ + reg_val = rGPR(rt); + wGPR(rt) = match vAddr[2..0] + { + 0b000 => reg_val[63..08] @ mem_val[63..56], + 0b001 => reg_val[63..16] @ mem_val[63..48], + 0b010 => reg_val[63..24] @ mem_val[63..40], + 0b011 => reg_val[63..32] @ mem_val[63..32], + 0b100 => reg_val[63..40] @ mem_val[63..24], + 0b101 => reg_val[63..48] @ mem_val[63..16], + 0b110 => reg_val[63..56] @ mem_val[63..08], + 0b111 => mem_val + }; + } + } + +/* SDL - Store double-word left */ +union clause ast = SDL : (regno, regno, bits(16)) +function clause decode(0b101100 @ base : regno @ rt : regno @ offset : imm16) = + Some(SDL(base, rt, offset)) +function clause execute(SDL(base, rt, offset)) = + { + /* XXX length check not quite right, but conservative */ + vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, D); + let pAddr = TLBTranslate(vAddr, StoreData) in + { + reg_val = rGPR(rt); + match vAddr[2..0] + { + 0b000 => (MEMw_wrapper(pAddr, 8) = reg_val[63..00]), + 0b001 => (MEMw_wrapper(pAddr, 7) = reg_val[63..08]), + 0b010 => (MEMw_wrapper(pAddr, 6) = reg_val[63..16]), + 0b011 => (MEMw_wrapper(pAddr, 5) = reg_val[63..24]), + 0b100 => (MEMw_wrapper(pAddr, 4) = reg_val[63..32]), + 0b101 => (MEMw_wrapper(pAddr, 3) = reg_val[63..40]), + 0b110 => (MEMw_wrapper(pAddr, 2) = reg_val[63..48]), + 0b111 => (MEMw_wrapper(pAddr, 1) = reg_val[63..56]) + } + } + } + + +/* SDR - Store double-word right */ +union clause ast = SDR : (regno, regno, bits(16)) +function clause decode(0b101101 @ base : regno @ rt : regno @ offset : imm16) = + Some(SDR(base, rt, offset)) +function clause execute(SDR(base, rt, offset)) = + { + /* XXX length check not quite right, but conservative */ + vAddr = addrWrapper(EXTS(offset) + rGPR(base), StoreData, D); + let pAddr = TLBTranslate(vAddr, StoreData) in + { + reg_val = rGPR(rt); + wordAddr = pAddr[63..3] @ 0b000; + match vAddr[2..0] + { + 0b000 => (MEMw_wrapper(wordAddr, 1) = reg_val[07..0]), + 0b001 => (MEMw_wrapper(wordAddr, 2) = reg_val[15..0]), + 0b010 => (MEMw_wrapper(wordAddr, 3) = reg_val[23..0]), + 0b011 => (MEMw_wrapper(wordAddr, 4) = reg_val[31..0]), + 0b100 => (MEMw_wrapper(wordAddr, 5) = reg_val[39..0]), + 0b101 => (MEMw_wrapper(wordAddr, 6) = reg_val[47..0]), + 0b110 => (MEMw_wrapper(wordAddr, 7) = reg_val[55..0]), + 0b111 => (MEMw_wrapper(wordAddr, 8) = reg_val[63..0]) + } + } + } + +/* CACHE - manipulate (non-existent) caches */ + +union clause ast = CACHE : (regno, regno, bits(16)) +function clause decode (0b101111 @ base : regno @ op : regno @ imm : imm16) = + Some(CACHE(base, op, imm)) +function clause execute (CACHE(base, op, imm)) = + checkCP0Access () /* pretty much a NOP because no caches */ + +/* PREF - prefetching into (non-existent) caches */ + +union clause ast = PREF : (regno, regno, bits(16)) +function clause decode (0b110011 @ base : regno @ op : regno @ imm : imm16) = + Some(PREF(base, op, imm)) +function clause execute (PREF(base, op, imm)) = + () /* XXX NOP */ + + +/* SYNC - Memory barrier */ +union clause ast = SYNC : unit +function clause decode (0b000000 @ 0b00000 @ 0b00000 @ 0b00000 @ stype : regno @ 0b001111) = + Some(SYNC()) /* stype is currently ignored */ +function clause execute(SYNC()) = + MEM_sync() + +union clause ast = MFC0 : (regno, regno, bits(3), bool) +function clause decode (0b010000 @ 0b00000 @ rt : regno @ rd : regno @ 0b00000000 @ sel : bits(3)) = + Some(MFC0(rt, rd, sel, false)) /* MFC0 */ +function clause decode (0b010000 @ 0b00001 @ rt : regno @ rd : regno @ 0b00000000 @ sel : bits(3)) = + Some(MFC0(rt, rd, sel, true)) /* DMFC0 */ +function clause execute (MFC0(rt, rd, sel, double)) = { + checkCP0Access(); + let result : bits(64) = match (rd, sel) + { + (0b00000,0b000) => let idx : bits(31) = EXTZ(TLBIndex) in + (0x00000000 @ TLBProbe @ idx), /* 0, TLB Index */ + (0b00001,0b000) => EXTZ(TLBRandom), /* 1, TLB Random */ + (0b00010,0b000) => TLBEntryLo0.bits(), /* 2, TLB EntryLo0 */ + (0b00011,0b000) => TLBEntryLo1.bits(), /* 3, TLB EntryLo1 */ + (0b00100,0b000) => TLBContext.bits(), /* 4, TLB Context */ + (0b00101,0b000) => EXTZ(TLBPageMask @ 0x000), /* 5, TLB PageMask */ + (0b00110,0b000) => EXTZ(TLBWired), /* 6, TLB Wired */ + (0b00111,0b000) => EXTZ(CP0HWREna), /* 7, HWREna */ + (0b01000,0b000) => CP0BadVAddr, /* 8, BadVAddr reg */ + (0b01000,0b001) => EXTZ(0b0), /* 8, BadInstr reg XXX TODO */ + (0b01001,0b000) => EXTZ(CP0Count), /* 9, Count reg */ + (0b01010,0b000) => TLBEntryHi.bits(),/* 10, TLB EntryHi */ + (0b01011,0b000) => EXTZ(CP0Compare), /* 11, Compare reg */ + (0b01100,0b000) => EXTZ(CP0Status.bits()), /* 12, Status reg */ + (0b01101,0b000) => EXTZ(CP0Cause.bits()), /* 13, Cause reg */ + (0b01110,0b000) => CP0EPC, /* 14, EPC */ + (0b01111,0b000) => EXTZ(0x00000400), /* 15, sel 0: PrID processor ID */ + (0b01111,0b110) => EXTZ(0b0), /* 15, sel 6: CHERI core ID */ + (0b01111,0b111) => EXTZ(0b0), /* 15, sel 7: CHERI thread ID */ + (0b10000,0b000) => EXTZ(0b1 /* M */ /* 16, sel 0: Config0 */ + @ 0b000000000000000 /* Impl */ + @ 0b1 /* BE */ + @ 0b10 /* AT */ + @ 0b000 /* AR */ + @ 0b001 /* MT standard TLB */ + @ 0b0000 /* zero */ + @ 0b000), + (0b10000,0b001) => EXTZ( /* 16, sel 1: Config1 */ + 0b1 /* M */ + @ TLBIndexMax /* MMU size-1 */ + @ 0b000 /* IS icache sets */ + @ 0b000 /* IL icache lines */ + @ 0b000 /* IA icache assoc. */ + @ 0b000 /* DS dcache sets */ + @ 0b000 /* DL dcache lines */ + @ 0b000 /* DA dcache assoc. */ + @ bool_to_bits(have_cp2) /* C2 CP2 presence */ + @ 0b0 /* MD MDMX implemented */ + @ 0b0 /* PC performance counters */ + @ 0b0 /* WR watch registers */ + @ 0b0 /* CA 16e code compression */ + @ 0b0 /* EP EJTAG */ + @ 0b0), /* FP FPU present */ + (0b10000,0b010) => EXTZ( /* 16, sel 2: Config2 */ + 0b1 /* M */ + @ 0b000 /* TU L3 control */ + @ 0b0000 /* TS L3 sets */ + @ 0b0000 /* TL L3 lines */ + @ 0b0000 /* TA L3 assoc. */ + @ 0b0000 /* SU L2 control */ + @ 0b0000 /* SS L2 sets */ + @ 0b0000 /* SL L2 lines */ + @ 0b0000), /* SA L2 assoc. */ + (0b10000,0b011) => 0x0000000000002000, /* 16, sel 3: Config3 zero except for bit 13 == ulri */ + (0b10000,0b101) => 0x0000000000000000, /* 16, sel 5: Config5 beri specific -- no extended TLB */ + (0b10001,0b000) => CP0LLAddr, /* 17, sel 0: LLAddr */ + (0b10010,0b000) => EXTZ(0b0), /* 18, WatchLo */ + (0b10011,0b000) => EXTZ(0b0), /* 19, WatchHi */ + (0b10100,0b000) => TLBXContext.bits(), /* 20, XContext */ + (0b11110,0b000) => CP0ErrorEPC, /* 30, ErrorEPC */ + _ => (SignalException(ResI)) + } in + wGPR(rt) = if (double) then result else EXTS(result[31..0]) +} + +/* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) */ +union clause ast = HCF : unit +function clause decode (0b010000 @ 0b00100 @ rt : regno @ 0b10111 @ 0b00000000000) = + Some(HCF()) + +function clause decode (0b010000 @ 0b00100 @ rt : regno @ 0b11010 @ 0b00000000000) = + Some(HCF()) + +function clause execute (HCF()) = + () /* halt instruction actually executed by interpreter framework */ + +union clause ast = MTC0 : (regno, regno, bits(3), bool) +function clause decode (0b010000 @ 0b00100 @ rt : regno @ rd : regno @ 0b00000000 @ sel : bits(3)) = + Some(MTC0(rt, rd, sel, false)) /* MTC0 */ +function clause decode (0b010000 @ 0b00101 @ rt : regno @ rd : regno @ 0b00000000 @ sel : bits(3)) = + Some(MTC0(rt, rd, sel, true)) /* DMTC0 */ +function clause execute (MTC0(rt, rd, sel, double)) = { + checkCP0Access(); + let reg_val = rGPR(rt) in + match (rd, sel) + { + (0b00000,0b000) => TLBIndex = mask(reg_val), /* NB no write to TLBProbe */ + (0b00001,0b000) => (), /* TLBRandom is read only */ + (0b00010,0b000) => TLBEntryLo0->bits() = reg_val, + (0b00011,0b000) => TLBEntryLo1->bits() = reg_val, + (0b00100,0b000) => TLBContext->PTEBase() = reg_val[63..23], + (0b00100,0b010) => CP0UserLocal = reg_val, + (0b00101,0b000) => TLBPageMask = reg_val[28..13], + (0b00110,0b000) => { + TLBWired = mask(reg_val); + TLBRandom = TLBIndexMax; + }, + (0b00111,0b000) => CP0HWREna = (reg_val[31..29] @ 0b0000000000000000000000000 @ reg_val[3..0]), + (0b01000,0b000) => (), /* BadVAddr read only */ + (0b01001,0b000) => CP0Count = reg_val[31..0], + (0b01010,0b000) => { + TLBEntryHi->R() = reg_val[63..62]; + TLBEntryHi->VPN2() = reg_val[39..13]; + TLBEntryHi->ASID() = reg_val[7..0]; + }, + (0b01011,0b000) => { /* 11, sel 0: Compare reg */ + CP0Compare = reg_val[31..0]; + CP0Cause->IP() = CP0Cause.IP() & 0x7f; /* clear IP7 */ + }, + (0b01100,0b000) => { /* 12 Status */ + CP0Status->CU() = reg_val[31..28]; + CP0Status->BEV() = reg_val[22]; + CP0Status->IM() = reg_val[15..8]; + CP0Status->KX() = reg_val[7]; + CP0Status->SX() = reg_val[6]; + CP0Status->UX() = reg_val[5]; + CP0Status->KSU() = reg_val[4..3]; + CP0Status->ERL() = reg_val[2]; + CP0Status->EXL() = reg_val[1]; + CP0Status->IE() = reg_val[0]; + }, + (0b01101,0b000) => { /* 13 Cause */ + CP0Cause->IV() = reg_val[23]; /* TODO special interrupt vector not implemeneted */ + let ip = CP0Cause.IP() in + CP0Cause->IP() = ((ip[7..2]) @ (reg_val[9..8])); + }, + (0b01110,0b000) => CP0EPC = reg_val, /* 14, EPC */ + (0b10000,0b000) => (), /* XXX ignore K0 cache config 16: Config0 */ + (0b10100,0b000) => TLBXContext->XPTEBase() = reg_val[63..33], + (0b11110,0b000) => CP0ErrorEPC = reg_val, /* 30, ErrorEPC */ + _ => (SignalException(ResI)) + } +} + +val TLBWriteEntry : TLBIndexT -> unit effect {rreg, wreg, escape} +function TLBWriteEntry(idx) = { + pagemask = TLBPageMask; + match pagemask { + 0x0000 => (), + 0x0003 => (), + 0x000f => (), + 0x003f => (), + 0x00ff => (), + 0x03ff => (), + 0x0fff => (), + 0x3fff => (), + 0xffff => (), + _ => (SignalException(MCheck)) + }; + let i as atom(_) = unsigned(idx) in + let entry = TLBEntries[i] in { + entry.pagemask() = pagemask; + entry.r() = TLBEntryHi.R(); + entry.vpn2() = TLBEntryHi.VPN2(); + entry.asid() = TLBEntryHi.ASID(); + entry.g() = ((TLBEntryLo0.G()) & (TLBEntryLo1.G())); + entry.valid() = bitone; + entry.caps0() = TLBEntryLo0.CapS(); + entry.capl0() = TLBEntryLo0.CapL(); + entry.pfn0() = TLBEntryLo0.PFN(); + entry.c0() = TLBEntryLo0.C(); + entry.d0() = TLBEntryLo0.D(); + entry.v0() = TLBEntryLo0.V(); + entry.caps1() = TLBEntryLo1.CapS(); + entry.capl1() = TLBEntryLo1.CapL(); + entry.pfn1() = TLBEntryLo1.PFN(); + entry.c1() = TLBEntryLo1.C(); + entry.d1() = TLBEntryLo1.D(); + entry.v1() = TLBEntryLo1.V(); + } +} + +union clause ast = TLBWI : unit +function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000010) = Some(TLBWI() : ast) +function clause execute (TLBWI()) = { + checkCP0Access(); + TLBWriteEntry(TLBIndex); +} + +union clause ast = TLBWR : unit +function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000110) = Some(TLBWR() : ast) +function clause execute (TLBWR()) = { + checkCP0Access(); + TLBWriteEntry(TLBRandom); +} + +union clause ast = TLBR : unit +function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000001) = Some(TLBR() : ast) +function clause execute (TLBR()) = { + checkCP0Access(); + let i as atom(_) = unsigned(TLBIndex) in + let entry = reg_deref(TLBEntries[i]) in { + TLBPageMask = entry.pagemask(); + TLBEntryHi->R() = entry.r(); + TLBEntryHi->VPN2() = entry.vpn2(); + TLBEntryHi->ASID() = entry.asid(); + TLBEntryLo0->CapS()= entry.caps0(); + TLBEntryLo0->CapL()= entry.capl0(); + TLBEntryLo0->PFN() = entry.pfn0(); + TLBEntryLo0->C() = entry.c0(); + TLBEntryLo0->D() = entry.d0(); + TLBEntryLo0->V() = entry.v0(); + TLBEntryLo0->G() = entry.g(); + TLBEntryLo1->CapS()= entry.caps1(); + TLBEntryLo1->CapL()= entry.capl1(); + TLBEntryLo1->PFN() = entry.pfn1(); + TLBEntryLo1->C() = entry.c1(); + TLBEntryLo1->D() = entry.d1(); + TLBEntryLo1->V() = entry.v1(); + TLBEntryLo1->G() = entry.g(); + } +} + +union clause ast = TLBP : unit +function clause decode (0b010000 @ 0b10000000000000000000 @ 0b001000) = Some(TLBP() : ast) +function clause execute (TLBP()) = { + checkCP0Access(); + let result = tlbSearch(TLBEntryHi.bits()) in + match result { + (Some(idx)) => { + TLBProbe = [bitzero]; + TLBIndex = idx; + }, + None() => { + TLBProbe = [bitone]; + TLBIndex = 0b000000; + } + } +} + +union clause ast = RDHWR : (regno, regno) +function clause decode (0b011111 @ 0b00000 @ rt : regno @ rd : regno @ 0b00000 @ 0b111011) = + Some(RDHWR(rt, rd)) +function clause execute (RDHWR(rt, rd)) = { + let accessLevel = getAccessLevel() in + let haveAccessLevel : bool = accessLevel == Kernel in + let haveCU0 : bool = bitone == (CP0Status.CU()[0]) in + let rdi as atom(_) = unsigned(rd) in + let haveHWREna : bool = bitone == (CP0HWREna[rdi]) in + if ~(haveAccessLevel | haveCU0 | haveHWREna) then + (SignalException(ResI)); + let temp : bits(64) = match rd { + 0b00000 => EXTZ([bitzero]), /* CPUNum */ + 0b00001 => EXTZ([bitzero]), /* SYNCI_step */ + 0b00010 => EXTZ(CP0Count), /* Count */ + 0b00011 => EXTZ([bitone]), /* Count resolution */ + 0b11101 => CP0UserLocal, /* User local register */ + _ => (SignalException(ResI)) + } in + wGPR(rt) = temp; +} + +union clause ast = ERET : unit + +function clause decode (0b010000 @ 0b1 @ 0b0000000000000000000 @ 0b011000) = + Some(ERET()) +function clause execute (ERET()) = + { + checkCP0Access(); + ERETHook(); + CP0LLBit = 0b0; + if (CP0Status.ERL() == bitone) then + { + nextPC = CP0ErrorEPC; + CP0Status->ERL() = 0b0; + } + else + { + nextPC = CP0EPC; + CP0Status->EXL() = 0b0; + } + } diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail new file mode 100644 index 00000000..b4f09548 --- /dev/null +++ b/mips/mips_prelude.sail @@ -0,0 +1,620 @@ +/*========================================================================*/ +/* */ +/* Copyright (c) 2015-2017 Robert M. Norton */ +/* Copyright (c) 2015-2017 Kathyrn Gray */ +/* All rights reserved. */ +/* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*========================================================================*/ + +/* mips_prelude.sail: declarations of mips registers, and functions common + to mips instructions (e.g. address translation) */ + +register PC : bits(64) +register nextPC : bits(64) + +/* CP0 Registers */ + +bitfield CauseReg : bits(32) = { + BD : 31, /* branch delay */ + /*Z0 : 30,*/ + CE : 29.. 28, /* for coprocessor enable exception */ + /*Z1 : 27.. 24,*/ + IV : 23, /* special interrupt vector not supported */ + WP : 22, /* watchpoint exception occurred */ + /*Z2 : 21.. 16, */ + IP : 15.. 8, /* interrupt pending bits */ + /*Z3 : 7,*/ + ExcCode : 6.. 2, /* code of last exception */ + /*Z4 : 1.. 0,*/ +} + +bitfield TLBEntryLoReg : bits(64) = { + CapS : 63, + CapL : 62, + PFN : 29.. 6, + C : 5.. 3, + D : 2, + V : 1, + G : 0, +} + +bitfield TLBEntryHiReg : bits(64) = { + R : 63.. 62, + VPN2 : 39.. 13, + ASID : 7.. 0, +} + +bitfield ContextReg : bits(64) = { + PTEBase : 63.. 23, + BadVPN2 : 22.. 4, + /*ZR : 3.. 0,*/ +} + +bitfield XContextReg : bits(64) = { + XPTEBase : 63.. 33, + XR : 32.. 31, + XBadVPN2 : 30.. 4, +} + +let TLBNumEntries = 64 +type TLBIndexT = (bits(6)) +let TLBIndexMax : TLBIndexT = 0b111111 + +val MAX : forall 'n. atom('n) -> atom(2 ^ 'n - 1) effect pure +function MAX(n) = pow2(n) - 1 + +let MAX_U64 = MAX(64) /*unsigned(0xffffffffffffffff)*/ +let MAX_VA = MAX(40) /*unsigned(0xffffffffff)*/ +let MAX_PA = MAX(36) /*unsigned(0xfffffffff)*/ + +bitfield TLBEntry : bits(117) = { + pagemask : 116.. 101, + r : 100.. 99, + vpn2 : 98.. 72, + asid : 71.. 64, + g : 63, + valid : 62, + caps1 : 61, + capl1 : 60, + pfn1 : 59.. 36, + c1 : 35.. 33, + d1 : 32, + v1 : 31, + caps0 : 30, + capl0 : 29, + pfn0 : 28.. 5, + c0 : 4.. 2, + d0 : 1, + v0 : 0, +} + +register TLBProbe : bits(1) +register TLBIndex : TLBIndexT +register TLBRandom : TLBIndexT +register TLBEntryLo0 : TLBEntryLoReg +register TLBEntryLo1 : TLBEntryLoReg +register TLBContext : ContextReg +register TLBPageMask : bits(16) +register TLBWired : TLBIndexT +register TLBEntryHi : TLBEntryHiReg +register TLBXContext : XContextReg + +register TLBEntry00 : TLBEntry +register TLBEntry01 : TLBEntry +register TLBEntry02 : TLBEntry +register TLBEntry03 : TLBEntry +register TLBEntry04 : TLBEntry +register TLBEntry05 : TLBEntry +register TLBEntry06 : TLBEntry +register TLBEntry07 : TLBEntry +register TLBEntry08 : TLBEntry +register TLBEntry09 : TLBEntry +register TLBEntry10 : TLBEntry +register TLBEntry11 : TLBEntry +register TLBEntry12 : TLBEntry +register TLBEntry13 : TLBEntry +register TLBEntry14 : TLBEntry +register TLBEntry15 : TLBEntry +register TLBEntry16 : TLBEntry +register TLBEntry17 : TLBEntry +register TLBEntry18 : TLBEntry +register TLBEntry19 : TLBEntry +register TLBEntry20 : TLBEntry +register TLBEntry21 : TLBEntry +register TLBEntry22 : TLBEntry +register TLBEntry23 : TLBEntry +register TLBEntry24 : TLBEntry +register TLBEntry25 : TLBEntry +register TLBEntry26 : TLBEntry +register TLBEntry27 : TLBEntry +register TLBEntry28 : TLBEntry +register TLBEntry29 : TLBEntry +register TLBEntry30 : TLBEntry +register TLBEntry31 : TLBEntry +register TLBEntry32 : TLBEntry +register TLBEntry33 : TLBEntry +register TLBEntry34 : TLBEntry +register TLBEntry35 : TLBEntry +register TLBEntry36 : TLBEntry +register TLBEntry37 : TLBEntry +register TLBEntry38 : TLBEntry +register TLBEntry39 : TLBEntry +register TLBEntry40 : TLBEntry +register TLBEntry41 : TLBEntry +register TLBEntry42 : TLBEntry +register TLBEntry43 : TLBEntry +register TLBEntry44 : TLBEntry +register TLBEntry45 : TLBEntry +register TLBEntry46 : TLBEntry +register TLBEntry47 : TLBEntry +register TLBEntry48 : TLBEntry +register TLBEntry49 : TLBEntry +register TLBEntry50 : TLBEntry +register TLBEntry51 : TLBEntry +register TLBEntry52 : TLBEntry +register TLBEntry53 : TLBEntry +register TLBEntry54 : TLBEntry +register TLBEntry55 : TLBEntry +register TLBEntry56 : TLBEntry +register TLBEntry57 : TLBEntry +register TLBEntry58 : TLBEntry +register TLBEntry59 : TLBEntry +register TLBEntry60 : TLBEntry +register TLBEntry61 : TLBEntry +register TLBEntry62 : TLBEntry +register TLBEntry63 : TLBEntry + +let TLBEntries : vector(64, dec, register(TLBEntry)) = [ + ref TLBEntry63, + ref TLBEntry62, + ref TLBEntry61, + ref TLBEntry60, + ref TLBEntry59, + ref TLBEntry58, + ref TLBEntry57, + ref TLBEntry56, + ref TLBEntry55, + ref TLBEntry54, + ref TLBEntry53, + ref TLBEntry52, + ref TLBEntry51, + ref TLBEntry50, + ref TLBEntry49, + ref TLBEntry48, + ref TLBEntry47, + ref TLBEntry46, + ref TLBEntry45, + ref TLBEntry44, + ref TLBEntry43, + ref TLBEntry42, + ref TLBEntry41, + ref TLBEntry40, + ref TLBEntry39, + ref TLBEntry38, + ref TLBEntry37, + ref TLBEntry36, + ref TLBEntry35, + ref TLBEntry34, + ref TLBEntry33, + ref TLBEntry32, + ref TLBEntry31, + ref TLBEntry30, + ref TLBEntry29, + ref TLBEntry28, + ref TLBEntry27, + ref TLBEntry26, + ref TLBEntry25, + ref TLBEntry24, + ref TLBEntry23, + ref TLBEntry22, + ref TLBEntry21, + ref TLBEntry20, + ref TLBEntry19, + ref TLBEntry18, + ref TLBEntry17, + ref TLBEntry16, + ref TLBEntry15, + ref TLBEntry14, + ref TLBEntry13, + ref TLBEntry12, + ref TLBEntry11, + ref TLBEntry10, + ref TLBEntry09, + ref TLBEntry08, + ref TLBEntry07, + ref TLBEntry06, + ref TLBEntry05, + ref TLBEntry04, + ref TLBEntry03, + ref TLBEntry02, + ref TLBEntry01, + ref TLBEntry00 +] + +register CP0Compare : bits(32) +register CP0Cause : CauseReg +register CP0EPC : bits(64) +register CP0ErrorEPC : bits(64) +register CP0LLBit : bits(1) +register CP0LLAddr : bits(64) +register CP0BadVAddr : bits(64) +register CP0Count : bits(32) +register CP0HWREna : bits(32) +register CP0UserLocal : bits(64) + +bitfield StatusReg : bits(32) = { + CU : 31.. 28, /* co-processor enable bits */ + /* RP/FR/RE/MX/PX not implemented */ + BEV : 22, /* use boot exception vectors (initialised to one) */ + /* TS/SR/NMI not implemented */ + IM : 15.. 8, /* Interrupt mask */ + KX : 7, /* kernel 64-bit enable */ + SX : 6, /* supervisor 64-bit enable */ + UX : 5, /* user 64-bit enable */ + KSU : 4.. 3, /* Processor mode */ + ERL : 2, /* error level (should be initialised to one, but BERI is different) */ + EXL : 1, /* exception level */ + IE : 0, /* interrupt enable */ +} +register CP0Status : StatusReg + +/* Implementation registers -- not ISA defined */ +register branchPending : bits(1) /* Set by branch instructions to implement branch delay */ +register inBranchDelay : bits(1) /* Needs to be set by outside world when in branch delay slot */ +register delayedPC : bits(64) /* Set by branch instructions to implement branch delay */ + +/* General purpose registers */ + + +/* Special registers For MUL/DIV */ +register HI : bits(64) +register LO : bits(64) + +register GPR : vector(32, dec, bits(64)) + +/* JTAG Uart registers */ + +register UART_WDATA : bits(8) +register UART_WRITTEN : bits(1) +register UART_RDATA : bits(8) +register UART_RVALID : bits(1) + +/* Check whether a given 64-bit vector is a properly sign extended 32-bit word */ +val NotWordVal : bits(64) -> bool effect pure +function NotWordVal (word) = + (word[31] ^^ 32) != word[63..32] + +/* Read numbered GP reg. (r0 is always zero) */ +val rGPR : bits(5) -> bits(64) effect {rreg} +function rGPR idx = { + let i as atom(_) = unsigned(idx) in + if i == 0 then 0x0000000000000000 else GPR[i] +} + +/* Write numbered GP reg. (writes to r0 ignored) */ +val wGPR : (bits(5), bits(64)) -> unit effect {wreg} +function wGPR (idx, v) = { + let i as atom(_) = unsigned(idx) in + if i == 0 then () else GPR[i] = v +} + +val MEMr = {lem: "MEMr"} : forall 'n. + ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem } +val MEMr_reserve = {lem: "MEMr_reserve"} : forall 'n. + ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem } +val MEM_sync = {lem: "MEM_sync"} : + unit -> unit effect { barr } + +val MEMea = {lem: "MEMea"} : forall 'n. + ( bits(64) , atom('n)) -> unit effect { eamem } +val MEMea_conditional = {lem: "MEMea_conditional"} : forall 'n. + ( bits(64) , atom('n)) -> unit effect { eamem } +val MEMval = {lem: "MEMval"} : forall 'n. + ( bits(64) , atom('n), bits(8*'n)) -> unit effect { wmv } +val MEMval_conditional = {lem: "MEMval_conditional"} : forall 'n. + ( bits(64) , atom('n), bits(8*'n)) -> bool effect { wmv } + +/* Extern nops with effects, sometimes useful for faking effect */ +val skip_eamem = "skip" : unit -> unit effect {eamem} +val skip_barr = "skip" : unit -> unit effect {barr} +val skip_wreg = "skip" : unit -> unit effect {wreg} +val skip_rreg = "skip" : unit -> unit effect {rreg} +val skip_wmvt = "skip" : unit -> unit effect {wmvt} +val skip_rmemt = "skip" : unit -> unit effect {rmemt} +val skip_escape = "skip" : unit -> unit effect {escape} + +function MEMr (addr, size) = __MIPS_read(addr, size) +function MEMr_reserve (addr, size) = __MIPS_read(addr, size) +function MEM_sync () = skip_barr() + +function MEMea (addr, size) = skip_eamem() +function MEMea_conditional (addr, size) = skip_eamem() +function MEMval (addr, size, data) = __MIPS_write(addr, size, data) +function MEMval_conditional (addr, size, data) = { __MIPS_write(addr, size, data); true } + +enum Exception = +{ + Interrupt, TLBMod, TLBL, TLBS, AdEL, AdES, Sys, Bp, ResI, CpU, Ov, Tr, C2E, C2Trap, + XTLBRefillL, XTLBRefillS, XTLBInvL, XTLBInvS, MCheck +} + +/* Return the ISA defined code for an exception condition */ +function ExceptionCode (ex) : Exception -> bits(5)= + let x : bits(8) = match ex + { + Interrupt => 0x00, /* Interrupt */ + TLBMod => 0x01, /* TLB modification exception */ + TLBL => 0x02, /* TLB exception (load or fetch) */ + TLBS => 0x03, /* TLB exception (store) */ + AdEL => 0x04, /* Address error (load or fetch) */ + AdES => 0x05, /* Address error (store) */ + Sys => 0x08, /* Syscall */ + Bp => 0x09, /* Breakpoint */ + ResI => 0x0a, /* Reserved instruction */ + CpU => 0x0b, /* Coprocessor Unusable */ + Ov => 0x0c, /* Arithmetic overflow */ + Tr => 0x0d, /* Trap */ + C2E => 0x12, /* C2E coprocessor 2 exception */ + C2Trap => 0x12, /* C2Trap maps to same exception code, different vector */ + XTLBRefillL => 0x02, + XTLBRefillS => 0x03, + XTLBInvL => 0x02, + XTLBInvS => 0x03, + MCheck => 0x18 + } in x[4..0] + + +val SignalExceptionMIPS : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg} +function SignalExceptionMIPS (ex, kccBase) = + { + /* Only update EPC and BD if not already in EXL mode */ + if (~ (CP0Status.EXL())) then + { + if (inBranchDelay[0]) then + { + CP0EPC = PC - 4; + CP0Cause->BD() = 0b1; + } + else + { + CP0EPC = PC; + CP0Cause->BD() = 0b0; + } + }; + + /* choose an exception vector to branch to. Some are not supported + e.g. Reset */ + vectorOffset = + if (CP0Status.EXL()) then + 0x180 /* Always use common vector if in exception mode already */ + else if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) then + 0x080 + else if (ex == C2Trap) then + 0x280 /* Special vector for CHERI traps */ + else + 0x180; /* Common vector */ + vectorBase : bits(64) = if CP0Status.BEV() then + 0xFFFFFFFFBFC00200 + else + 0xFFFFFFFF80000000; + /* On CHERI we have to subtract KCC.base so that we end up at the + right absolute vector address after indirecting via new PCC */ + nextPC = vectorBase + EXTS(vectorOffset) - kccBase; + CP0Cause->ExcCode() = ExceptionCode(ex); + CP0Status->EXL() = 0b1; + throw (ISAException()); + } + +/* Defined either in mips_wrappers (directly calling SignalExceptionMIPS) or in cheri_prelude_common (cheri things plus above) */ +val SignalException : forall ('o : Type) . Exception -> 'o effect {escape, rreg, wreg} + +val SignalExceptionBadAddr : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg} +function SignalExceptionBadAddr(ex, badAddr) = + { + CP0BadVAddr = badAddr; + SignalException(ex); + } + +val SignalExceptionTLB : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg} +function SignalExceptionTLB(ex, badAddr) = { + CP0BadVAddr = badAddr; + TLBContext->BadVPN2() = (badAddr[31..13]); + TLBXContext->XBadVPN2()= (badAddr[39..13]); + TLBXContext->XR() = (badAddr[63..62]); + TLBEntryHi->R() = (badAddr[63..62]); + TLBEntryHi->VPN2() = (badAddr[39..13]); + SignalException(ex); +} + +enum MemAccessType = {Instruction, LoadData, StoreData} +enum AccessLevel = {User, Supervisor, Kernel} + +function getAccessLevel() : unit -> AccessLevel= + if ((CP0Status.EXL()) | (CP0Status.ERL())) then + Kernel + else match CP0Status.KSU() + { + 0b00 => Kernel, + 0b01 => Supervisor, + 0b10 => User, + _ => User /* behaviour undefined, assume user */ + } + +val checkCP0Access : unit->unit effect{escape, rreg, wreg} +function checkCP0Access () = + { + let accessLevel = getAccessLevel() in + if ((accessLevel != Kernel) & (~(CP0Status.CU()[0]))) then + { + CP0Cause->CE() = 0b00; + SignalException(CpU); + } + } + +val incrementCP0Count : unit -> unit effect {rreg,wreg,escape} +function incrementCP0Count() = { + TLBRandom = (if (TLBRandom == TLBWired) + then (TLBIndexMax) else (TLBRandom - 1)); + + CP0Count = (CP0Count + 1); + if (CP0Count == CP0Compare) then { + CP0Cause->IP() = CP0Cause.IP() | 0x80; /* IP7 is timer interrupt */ + }; + + let ims = CP0Status.IM() in + let ips = CP0Cause.IP() in + let ie = CP0Status.IE() in + let exl = CP0Status.EXL() in + let erl = CP0Status.ERL() in + if ((~(exl)) & (~(erl)) & ie & ((ips & ims) != 0x00)) then + SignalException(Interrupt); +} + +type regno = bits(5) /* a register number */ +type imm16 = bits(16) /* 16-bit immediate */ +/* a commonly used instruction format with three register operands */ +type regregreg = (regno, regno, regno) +/* a commonly used instruction format with two register operands and 16-bit immediate */ +type regregimm16 = (regno, regno, imm16) + +enum decode_failure = { + no_matching_pattern, + unsupported_instruction, + illegal_instruction, + internal_error +} + +/* Used by branch and trap instructions */ +enum Comparison = { + EQ, /* equal */ + NE, /* not equal */ + GE, /* signed greater than or equal */ + GEU,/* unsigned greater than or equal */ + GT, /* signed strictly greater than */ + LE, /* signed less than or equal */ + LT, /* signed strictly less than */ + LTU /* unsigned less than or qual */ +} + +val compare : (Comparison, bits(64), bits(64)) -> bool +function compare (cmp, valA, valB) = + match cmp { + EQ => valA == valB, + NE => valA != valB, + GE => valA >=_s valB, + GEU => valA >=_u valB, + GT => valB <_s valA, + LE => valB >=_s valA, + LT => valA <_s valB, + LTU => valA <_u valB + } +enum WordType = { B, H, W, D} + +val wordWidthBytes : WordType -> range(1, 8) +function wordWidthBytes(w) = + match w { + B => 1, + H => 2, + W => 4, + D => 8 + } + +/* This function checks that memory accesses are naturally aligned + -- it is disabled in favour of BERI specific behaviour below. +function bool isAddressAligned(addr, (WordType) wordType) = + match wordType { + B => true + H => (addr[0] == 0) + W => (addr[1..0] == 0b00) + D => (addr[2..0] == 0b000) + } +*/ + +/* BERI relaxes the natural alignment requirement for loads and stores + but still throws an exception if an access spans a cache line + boundary. Here we assume this is 32 bytes so that we don't have to + worry about clearing multiple tags when an access spans more than + one capability. Capability load/stores are still naturally + aligned. Provided this is a factor of smallest supported page size + (4k) we don't need to worry about accesses spanning page boundaries + either. +*/ +let alignment_width = 16 +val isAddressAligned : (bits(64), WordType) -> bool +function isAddressAligned (addr, wordType) = + let a = unsigned(addr) in + a / alignment_width == (a + wordWidthBytes(wordType) - 1) / alignment_width + +val reverse_endianness = "reverse_endianness" : forall 'W, 'W >= 1. bits(8 * 'W) -> bits(8 * 'W) effect pure + +/* +function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness' (w, value) = +{ + ([:8 * 'W:]) width = length(value); + if width <= 8 + then value + else value[7..0] : reverse_endianness'(w - 1, value[(width - 1) .. 8]) +} + + + +function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness ((bits(8 * 'W)) value) = +{ + reverse_endianness'(sizeof 'W, value) +}*/ + +val MEMr_wrapper : forall 'n, 1 <= 'n <=8 . (bits(64), atom('n)) -> bits(8*'n) effect {rmem} +function MEMr_wrapper (addr, size) = reverse_endianness(MEMr (addr, size)) +/* TODO + if (addr == 0x000000007f000000) then + { + let rvalid = UART_RVALID in + let rdata = (bits(8 * 'n)) (mask(0x00000000 : UART_RDATA : rvalid : 0b0000000 : 0x0000)) in + { + UART_RVALID = [bitzero]; + rdata + } + } + else if (addr == 0x000000007f000004) then + mask(0x000000000004ffff) /* Always plenty of write space available and jtag activity */ + else + reverse_endianness(MEMr(addr, size)) /* MEMr assumes little endian */ */ + +val MEMr_reserve_wrapper : forall 'n, 1 <= 'n <= 8 . ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem } +function MEMr_reserve_wrapper (addr , size) = + reverse_endianness(MEMr_reserve(addr, size)) + + +function init_cp0_state () : unit -> unit = { + CP0Status->BEV() = bitone; +} + +val init_cp2_state : unit -> unit effect {wreg} +val cp2_next_pc: unit -> unit effect {rreg, wreg} +val dump_cp2_state : unit -> unit effect {rreg, escape} diff --git a/mips/mips_regfp.sail b/mips/mips_regfp.sail new file mode 100644 index 00000000..4bf96022 --- /dev/null +++ b/mips/mips_regfp.sail @@ -0,0 +1,455 @@ +/*========================================================================*/ +/* */ +/* Copyright (c) 2015-2017 Robert M. Norton */ +/* Copyright (c) 2015-2017 Kathyrn Gray */ +/* All rights reserved. */ +/* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*========================================================================*/ + +let GPRs : vector <0, 32, inc, string > = + [ "GPR00", "GPR01", "GPR02", "GPR03", "GPR04", "GPR05", "GPR06", "GPR07", "GPR08", "GPR09", "GPR10", + "GPR11", "GPR12", "GPR13", "GPR14", "GPR15", "GPR16", "GPR17", "GPR18", "GPR19", "GPR20", + "GPR21", "GPR22", "GPR23", "GPR24", "GPR25", "GPR26", "GPR27", "GPR28", "GPR29", "GPR30", "GPR31" + ] + +let CIA_fp = RFull("CIA") +let NIA_fp = RFull("NIA") + +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 { + (DADDIU (rs, rt, imm)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (DADDU (rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (DADDI (rs, rt, imm)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (DADD (rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (ADD(rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (ADDI(rs, rt, imm)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (ADDU(rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (ADDIU(rs, rt, imm)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (DSUBU (rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (DSUB (rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (SUB(rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (SUBU(rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (AND (rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (ANDI (rs, rt, imm)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (OR (rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (ORI (rs, rt, imm)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (NOR (rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (XOR (rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (XORI (rs, rt, imm)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (LUI (rt, imm)) => { + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (DSLL (rt, rd, sa)) => { + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (DSLL32 (rt, rd, sa)) => { + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (DSLLV (rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (DSRA (rt, rd, sa)) => { + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (DSRA32 (rt, rd, sa)) => { + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (DSRAV (rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (DSRL (rt, rd, sa)) => { + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (DSRL32 (rt, rd, sa)) => { + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (DSRLV (rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (SLL(rt, rd, sa)) => { + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (SLLV(rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (SRA(rt, rd, sa)) => { + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (SRAV(rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (SRL(rt, rd, sa)) => { + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (SRLV(rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (SLT(rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (SLTI(rs, rt, imm)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (SLTU(rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (SLTIU(rs, rt, imm)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (MOVN(rs, rt, rd)) => { + /* XXX don't always write rd */ + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (MOVZ(rs, rt, rd)) => { + /* XXX don't always write rd */ + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (MFHI(rd)) => { + iR = RFull("HI") :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (MFLO(rd)) => { + iR = RFull("LO") :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (MTHI(rs)) => { + oR = RFull("HI") :: oR; + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + } + (MTLO(rs)) => { + oR = RFull("LO") :: oR; + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + } + (MUL(rs, rt, rd)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + if rd == 0 then () else oR = RFull(GPRs[rd]) :: oR; + } + (MULT(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (MULTU(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (DMULT(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (DMULTU(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (MADD(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + iR = RFull("HI") :: RFull ("LO") :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (MADDU(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + iR = RFull("HI") :: RFull ("LO") :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (MSUB(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + iR = RFull("HI") :: RFull ("LO") :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (MSUBU(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + iR = RFull("HI") :: RFull ("LO") :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (DIV(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (DIVU(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (DDIV(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (DDIVU(rs, rt)) => { + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + oR = RFull("HI") :: RFull ("LO") :: oR; + } + (J(offset)) => { + /* XXX actually unconditional jump */ + /*ik = IK_cond_branch;*/ + Dia = DIAFP_concrete((PC + 4)[63..28] : offset : 0b00); + } + (JAL(offset)) => { + /* XXX actually unconditional jump */ + /*ik = IK_cond_branch;*/ + oR = RFull("GPR31") :: oR; + Dia = DIAFP_concrete((PC + 4)[63..28] : offset : 0b00); + } + (JR(rs)) => { + /* XXX actually unconditional jump */ + /*ik = IK_cond_branch;*/ + iR = RFull(GPRs[rs]) :: iR; + Dia = DIAFP_reg(RFull(GPRs[rs])); + } + (JALR(rs, rd)) => { + /* XXX actually unconditional jump */ + /*ik = IK_cond_branch;*/ + iR = RFull(GPRs[rs]) :: iR; + oR = RFull("GPR31") :: oR; + Dia = DIAFP_reg(RFull(GPRs[rs])); + } + (BEQ(rs, rd, imm, ne, likely)) => { + ik = IK_cond_branch; + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if rd == 0 then () else iR = RFull(GPRs[rd]) :: iR; + let offset : bits(64) = (EXTS(imm : 0b00) + 4) in + Dia = DIAFP_concrete (PC + offset); + } + (BCMPZ(rs, imm, cmp, link, likely)) => { + ik = IK_cond_branch; + if rs == 0 then () else iR = RFull(GPRs[rs]) :: iR; + if link then + oR = RFull("GPR31") :: oR; + let offset : bits(64) = (EXTS(imm : 0b00) + 4) in + Dia = DIAFP_concrete (PC + offset); + } + (SYSCALL_THREAD_START) => () +/* + + case (SYSCALL) = + case (BREAK) = + case (WAIT) = { + case (TRAPREG(rs, rt, cmp)) = + case (TRAPIMM(rs, imm, cmp)) = +*/ + (Load(width, signed, linked, base, rt, offset)) => { + ik = IK_mem_read (if linked then Read_reserve else Read_plain); + if linked then oR = RFull("CP0LLBit")::RFull("CP0LLAddr")::oR else (); + if base == 0 then () else aR = RFull(GPRs[base]) :: aR; + iR = aR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (Store(width, conditional, base, rt, offset)) => { + ik = IK_mem_write(if conditional then Write_conditional else Write_plain); + if base == 0 then () else aR = RFull(GPRs[base]) :: aR; + iR = aR; + if conditional then iR = RFull("CP0LLBit")::iR else (); + if (conditional & (rt != 0)) then oR = RFull(GPRs[rt])::oR else (); + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + } + (LWL(base, rt, offset)) => { + ik = IK_mem_read(Read_plain); + if base == 0 then () else aR = RFull(GPRs[base]) :: aR; + iR = aR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (LWR(base, rt, offset)) => { + ik = IK_mem_read(Read_plain); + if base == 0 then () else aR = RFull(GPRs[base]) :: aR; + iR = aR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (SWL(base, rt, offset)) => { + ik = IK_mem_write(Write_plain); + if base == 0 then () else aR = RFull(GPRs[base]) :: aR; + iR = aR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + } + (SWR(base, rt, offset)) => { + ik = IK_mem_write(Write_plain); + if base == 0 then () else aR = RFull(GPRs[base]) :: aR; + iR = aR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + } + (LDL(base, rt, offset)) => { + ik = IK_mem_read(Read_plain); + if base == 0 then () else aR = RFull(GPRs[base]) :: aR; + iR = aR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (LDR(base, rt, offset)) => { + ik = IK_mem_read(Read_plain); + if base == 0 then () else aR = RFull(GPRs[base]) :: aR; + iR = aR; + if rt == 0 then () else oR = RFull(GPRs[rt]) :: oR; + } + (SDL(base, rt, offset)) => { + ik = IK_mem_write(Write_plain); + if base == 0 then () else aR = RFull(GPRs[base]) :: aR; + iR = aR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + } + (SDR(base, rt, offset)) => { + ik = IK_mem_write(Write_plain); + if base == 0 then () else aR = RFull(GPRs[base]) :: aR; + iR = aR; + if rt == 0 then () else iR = RFull(GPRs[rt]) :: iR; + } +/* + case (CACHE(base, op, imm)) = + case (PREF(base, op, imm)) = +*/ + (SYNC) => { + iK = IK_barrier(Barrier_MIPS_SYNC); + } +/* + case (MFC0(rt, rd, sel, double)) + case (HCF) + case (MTC0(rt, rd, sel, double)) + case (TLBWI) + case (TLBWR) + case (TLBR) + case ((TLBP)) + case (RDHWR(rt, rd)) + case (ERET) +*/ + }; + (iR,oR,aR,Nias,Dia,ik) +} diff --git a/mips/mips_ri.sail b/mips/mips_ri.sail new file mode 100644 index 00000000..edce0657 --- /dev/null +++ b/mips/mips_ri.sail @@ -0,0 +1,42 @@ +/*========================================================================*/ +/* */ +/* Copyright (c) 2015-2017 Robert M. Norton */ +/* Copyright (c) 2015-2017 Kathyrn Gray */ +/* All rights reserved. */ +/* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*========================================================================*/ + +/* mips_ri.sail: only use if want unknown instructions to throw + exception (like real hardware) instead of die (convenient for ppcmem) */ + +union clause ast = RI : unit +function clause decode _ = Some(RI()) +function clause execute (RI()) = + SignalException (ResI) + diff --git a/mips/mips_tlb.sail b/mips/mips_tlb.sail new file mode 100644 index 00000000..741eb84c --- /dev/null +++ b/mips/mips_tlb.sail @@ -0,0 +1,148 @@ +/*========================================================================*/ +/* */ +/* Copyright (c) 2015-2017 Robert M. Norton */ +/* Copyright (c) 2015-2017 Kathyrn Gray */ +/* All rights reserved. */ +/* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*========================================================================*/ + +val tlbEntryMatch : (bits(2), bits(27), bits(8), TLBEntry) -> bool effect pure +function tlbEntryMatch(r, vpn2, asid, entry) = + let entryValid = entry.valid() in + let entryR = entry.r() in + let entryMask = entry.pagemask() in + let entryVPN = entry.vpn2() in + let entryASID = entry.asid() in + let entryG = entry.g() in + let vpnMask : bits(27) = ~(EXTZ(entryMask)) in + (entryValid & + (r == entryR) & + ((vpn2 & vpnMask) == ((entryVPN) & vpnMask)) & + ((asid == (entryASID)) | (entryG))) + +val tlbSearch : bits(64) -> option(TLBIndexT) effect {rreg} +function tlbSearch(VAddr) = + let r = (VAddr[63..62]) in + let vpn2 = (VAddr[39..13]) in + let asid = TLBEntryHi.ASID() in { + foreach (idx from 0 to 63) { + if(tlbEntryMatch(r, vpn2, asid, reg_deref(TLBEntries[idx]))) then + return Some(to_bits(6, idx)) + }; + None() + } + +/** For given virtual address and accessType returns physical address and +bool flag indicating whether capability stores / loads are permitted for +page (depending on access type). */ + +val TLBTranslate2 : (bits(64), MemAccessType) -> (bits(64), bool) effect {rreg, wreg, undef, escape} +function TLBTranslate2 (vAddr, accessType) = { + let idx = tlbSearch(vAddr) in + match idx { + Some(idx) => + let i as atom(_) = unsigned(idx) in + let entry = reg_deref(TLBEntries[i]) in + let entryMask = entry.pagemask() in + let 'evenOddBit : range(12,28) = match (entryMask) { + 0x0000 => 12, + 0x0003 => 14, + 0x000f => 16, + 0x003f => 18, + 0x00ff => 20, + 0x03ff => 22, + 0x0fff => 24, + 0x3fff => 26, + 0xffff => 28, + _ => undefined + } in + let isOdd = (vAddr[evenOddBit]) in + let (caps : bits(1), capl : bits(1), pfn : bits(24), d : bits(1), v : bits(1)) = + if (isOdd) then + (entry.caps1(), entry.capl1(), entry.pfn1(), entry.d1(), entry.v1()) + else + (entry.caps0(), entry.capl0(), entry.pfn0(), entry.d0(), entry.v0()) in + if (~(v)) then + SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr) + else if ((accessType == StoreData) & ~(d)) then + SignalExceptionTLB(TLBMod, vAddr) + else + let res : bits(64) = EXTZ(pfn[23..(evenOddBit - 12)] @ vAddr[(evenOddBit - 1) .. 0]) in + (res, bits_to_bool(if (accessType == StoreData) then caps else capl)), + None() => SignalExceptionTLB( + if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr) + } +} + +val cast_AccessLevel : AccessLevel -> int effect pure +function cast_AccessLevel level = + match level { + User => 0, + Supervisor => 1, + Kernel => 2 + } + +/* perform TLB translation. bool is CHERI specific TLB bits noStoreCap/suppressTag */ +val TLBTranslateC : (bits(64), MemAccessType) -> (bits(64), bool) effect {escape, rreg, undef, wreg} +function TLBTranslateC (vAddr, accessType) = + { + let currentAccessLevel = getAccessLevel() in + let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in + let (requiredLevel, addr) : (AccessLevel, option(bits(64))) = match (vAddr[63..62]) { + 0b11 => match (compat32, vAddr[30..29]) { /* xkseg */ + (true, 0b11) => (Kernel, None() : option(bits(64))), /* kseg3 mapped 32-bit compat */ + (true, 0b10) => (Supervisor, None() : option(bits(64))), /* sseg mapped 32-bit compat */ + (true, 0b01) => (Kernel, Some(0x00000000 @ 0b000 @ vAddr[28..0])), /* kseg1 unmapped uncached 32-bit compat */ + (true, 0b00) => (Kernel, Some(0x00000000 @ 0b000 @ vAddr[28..0])), /* kseg0 unmapped cached 32-bit compat */ + (_, _) => (Kernel, None() : option(bits(64))) /* xkseg mapped */ + }, + 0b10 => (Kernel, Some(0b00000 @ vAddr[58..0])), /* xkphys bits 61-59 are cache mode (ignored) */ + 0b01 => (Supervisor, None() : option(bits(64))), /* xsseg - supervisor mapped */ + 0b00 => (User, None() : option(bits(64))) /* xuseg - user mapped */ + } in + if (cast_AccessLevel(currentAccessLevel) < cast_AccessLevel(requiredLevel)) then + SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr) + else + let (pa, c) : (bits(64), bool) = match addr { + Some(a) => (a, false), + None() => if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then + SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr) + else + TLBTranslate2(vAddr, accessType) + } + in if (unsigned(pa) > MAX_PA) then + SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr) + else + (pa, c) + } + +/* TLB translate function for MIPS (throws away capability flag) */ +val TLBTranslate : (bits(64), MemAccessType) -> bits(64) effect {rreg, wreg, escape, undef} +function TLBTranslate (vAddr, accessType) = + let (addr, c) = TLBTranslateC(vAddr, accessType) in addr diff --git a/mips/mips_tlb_stub.sail b/mips/mips_tlb_stub.sail new file mode 100644 index 00000000..f0ffb9dd --- /dev/null +++ b/mips/mips_tlb_stub.sail @@ -0,0 +1,48 @@ +/*========================================================================*/ +/* */ +/* Copyright (c) 2015-2017 Robert M. Norton */ +/* Copyright (c) 2015-2017 Kathyrn Gray */ +/* All rights reserved. */ +/* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*========================================================================*/ + +$ifndef _MIPS_TLB_STUB +$define _MIPS_TLB_STUB + +val tlbEntryMatch : (bits(2), bits(27), bits(8), TLBEntry) -> bool effect pure +function tlbSearch(VAddr) : bits(64) -> option(TLBIndexT) = None + +val TLBTranslate2 : (bits(64), MemAccessType) -> (bits(64), bool) effect pure +function TLBTranslate (vAddr, accessType) : (bits(64), MemAccessType) -> bits(64) = + vAddr + +val TLBTranslateC : (bits(64), MemAccessType) -> (bits(64), bool) effect pure +function TLBTranslateC (vAddr, accessType) : (bits(64), MemAccessType) -> (bits(64), bool) = (vAddr, false) + +$endif diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail new file mode 100644 index 00000000..70e6fa83 --- /dev/null +++ b/mips/mips_wrappers.sail @@ -0,0 +1,86 @@ +/*========================================================================*/ +/* */ +/* Copyright (c) 2015-2017 Robert M. Norton */ +/* Copyright (c) 2015-2017 Kathyrn Gray */ +/* All rights reserved. */ +/* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*========================================================================*/ + +/* mips_wrappers.sail: wrappers functions and hooks for CHERI extensibility + (mostly identity functions here) */ + +val MEMw_wrapper : forall 'n, 1 <= 'n <= 8. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {eamem, wmv, wreg} + +function MEMw_wrapper(addr, size, data) = + let ledata = reverse_endianness(data) in + if (addr == 0x000000007f000000) then + { + UART_WDATA = ledata[7..0]; + UART_WRITTEN = bitone; + } else { + MEMea(addr, size); + MEMval(addr, size, ledata); + } + +val MEMw_conditional_wrapper : forall 'n, 1 <= 'n <= 8. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {eamem, wmv} + +function MEMw_conditional_wrapper(addr, size, data) = + { + MEMea_conditional(addr, size); + MEMval_conditional(addr, size, reverse_endianness(data)) + } + +val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64) +function addrWrapper(addr, accessType, width) = + addr + +$ifdef _MIPS_TLB_STUB +val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape} +$else +val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape, undef} +$endif + +function TranslatePC (vAddr) = { + incrementCP0Count(); + if (vAddr[1..0] != 0b00) then /* bad PC alignment */ + (SignalExceptionBadAddr(AdEL, vAddr)) + else + TLBTranslate(vAddr, Instruction) +} + +let have_cp2 = false + +function SignalException (ex) = SignalExceptionMIPS(ex, 0x0000000000000000) + +val ERETHook : unit -> unit +function ERETHook() = () + +function init_cp2_state () = skip_wreg() +function cp2_next_pc() = {skip_wreg(); skip_rreg()} +function dump_cp2_state () = {skip_rreg(); skip_escape();} diff --git a/mips/prelude.sail b/mips/prelude.sail new file mode 100644 index 00000000..5b89521f --- /dev/null +++ b/mips/prelude.sail @@ -0,0 +1,391 @@ +default Order dec + +type bits ('n : Int) = vector('n, dec, bit) +union option ('a : Type) = {None : unit, Some : 'a} + +val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool + +val eq_string = {ocaml: "eq_string", lem: "eq"} : (string, string) -> bool + +val eq_real = {ocaml: "eq_real", lem: "eq"} : (real, real) -> bool + +val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool + +val bitvector_length = {ocaml: "length", lem: "length"} : forall 'n. bits('n) -> atom('n) +val vector_length = {ocaml: "length", lem: "length_list"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) +val list_length = {ocaml: "length", lem: "length_list"} : forall ('a : Type). list('a) -> int + +overload length = {bitvector_length, vector_length, list_length} + +val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} +/* sneaky deref with no effect necessary for bitfield writes */ +val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a + +overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything} + +val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. + (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) + +val bitvector_access = {ocaml: "access", lem: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n. + (bits('n), atom('m)) -> bit + +val any_vector_access = {ocaml: "access", lem: "access_list_dec"} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. + (vector('n, dec, 'a), atom('m)) -> 'a + +overload vector_access = {bitvector_access, any_vector_access} + +val bitvector_update = {ocaml: "update", lem: "update_vec_dec"} : forall 'n. + (bits('n), int, bit) -> bits('n) + +val any_vector_update = {ocaml: "update", lem: "update_list_dec"} : forall 'n ('a : Type). + (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) + +overload vector_update = {bitvector_update, any_vector_update} + +val update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o. + (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) + +val vcons = {lem: "cons_vec"} : forall ('n : Int) ('a : Type). + ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a) + +val bitvector_concat = {ocaml: "append", lem: "concat_vec"} : forall ('n : Int) ('m : Int). + (bits('n), bits('m)) -> bits('n + 'm) + +val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). + (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) + +overload append = {bitvector_concat, vector_concat} + +val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n) + +overload ~ = {not_bool, not_vec} + +val not = "not" : bool -> bool + +val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool +function neq_vec (x, y) = not_bool(eq_vec(x, y)) + +val neq_anything = {lem: "neq"} : forall ('a : Type). ('a, 'a) -> bool +function neq_anything (x, y) = not_bool(x == y) + +overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} + +val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) + +val and_vec = {lem: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) + +function and_vec (xs, ys) = builtin_and_vec(xs, ys) + +overload operator & = {and_bool, and_vec} + +val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) + +val or_vec = {lem: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) + +function or_vec (xs, ys) = builtin_or_vec(xs, ys) + +overload operator | = {or_bool, or_vec} + +val unsigned = {ocaml: "uint", lem: "unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) + +val signed = {ocaml: "sint", lem: "signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) + +val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) + +val __SetSlice_bits = "set_slice" : forall 'n 'm. + (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n) + +val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int + +val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int + +val __raw_GetSlice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w) + +val __GetSlice_int : forall 'n. (atom('n), int, int) -> bits('n) + +function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o) + +val __raw_SetSlice_bits : forall 'n 'w. + (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n) + +val __raw_GetSlice_bits : forall 'n 'w. + (atom('n), atom('w), bits('n), int) -> bits('w) + +val __SignExtendSlice = {lem: "exts_slice"} : forall 'm. (bits('m), int, int) -> bits('m) + +val __ZeroExtendSlice = {lem: "extz_slice"} : forall 'm. (bits('m), int, int) -> bits('m) + +val cast cast_unit_vec : bit -> bits(1) + +function cast_unit_vec bitzero = 0b0 +and cast_unit_vec bitone = 0b1 + +val print = "prerr_endline" : string -> unit + +val putchar = "putchar" : forall ('a : Type). 'a -> unit + +val concat_str = {ocaml: "concat_str", lem: "stringAppend"} : (string, string) -> string + +val string_of_int = "string_of_int" : int -> string + +val DecStr : int -> string + +val HexStr : int -> string + +val BitStr = "string_of_bits" : forall 'n. bits('n) -> string + +val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) + +val int_power = {ocaml: "int_power", lem: "pow"} : (int, int) -> int + +val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> real + +overload operator ^ = {xor_vec, int_power, real_power} + +val add_range = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm 'o 'p. + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) + +val add_int = {ocaml: "add_int", lem: "integerAdd"} : (int, int) -> int + +val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) + +val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n) + +val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real + +overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real} + +val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p. + (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) + +val sub_int = {ocaml: "sub_int", lem: "integerMinus"} : (int, int) -> int + +val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) + +val "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n) + +val sub_real = {ocaml: "sub_real", lem: "realMinus"} : (real, real) -> real + +val negate_range = {ocaml: "minus_big_int", lem: "integerNegate"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) + +val negate_int = {ocaml: "minus_big_int", lem: "integerNegate"} : int -> int + +val negate_real = {ocaml: "Num.minus_num", lem: "realNegate"} : real -> real + +overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real} + +overload negate = {negate_range, negate_int, negate_real} + +val mult_range = {ocaml: "mult", lem: "integerMult"} : forall 'n 'm 'o 'p. + (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p) + +val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int + +val mult_real = {ocaml: "mult_real", lem: "realMult"} : (real, real) -> real + +overload operator * = {mult_range, mult_int, mult_real} + +val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt"} : real -> real + +val gteq_real = {ocaml: "gteq_real", lem: "gteq"} : (real, real) -> bool + +overload operator >= = {gteq_atom, gteq_int, gteq_real} + +val lteq_real = {ocaml: "lteq_real", lem: "lteq"} : (real, real) -> bool + +overload operator <= = {lteq_atom, lteq_int, lteq_real} + +val gt_real = {ocaml: "gt_real", lem: "gt"} : (real, real) -> bool + +overload operator > = {gt_atom, gt_int, gt_real} + +val lt_real = {ocaml: "lt_real", lem: "lt"} : (real, real) -> bool + +overload operator < = {lt_atom, lt_int, lt_real} + +val RoundDown = {ocaml: "round_down", lem: "realFloor"} : real -> int + +val RoundUp = {ocaml: "round_up", lem: "realCeiling"} : real -> int + +val abs_int = {ocaml: "abs_int", lem: "abs"} : int -> int + +val abs_real = {ocaml: "abs_real", lem: "abs"} : real -> real + +overload abs = {abs_int, abs_real} + +val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat + +val quotient_real = {ocaml: "quotient_real", lem: "realDiv"} : (real, real) -> real + +val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int + +overload operator / = {quotient_nat, quotient, quotient_real} + +val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot"} : (int, int) -> int +val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod"} : (int, int) -> int + +val modulus = {ocaml: "modulus", lem: "hardware_mod"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) + +overload operator % = {modulus} + +val Real = {ocaml: "Num.num_of_big_int", lem: "realFromInteger"} : int -> real + +val shl_int = "shl_int" : (int, int) -> int + +val shr_int = "shr_int" : (int, int) -> int + +val min_nat = {ocaml: "min_int", lem: "min"} : (nat, nat) -> nat + +val min_int = {ocaml: "min_int", lem: "min"} : (int, int) -> int + +val max_nat = {ocaml: "max_int", lem: "max"} : (nat, nat) -> nat + +val max_int = {ocaml: "max_int", lem: "max"} : (int, int) -> int + +val min_atom = {ocaml: "min_int", lem: "min"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)} + +val max_atom = {ocaml: "max_int", lem: "max"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)} + +overload min = {min_atom, min_nat, min_int} + +overload max = {max_atom, max_nat, max_int} + +val __WriteRAM = "write_ram" : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmv} + +val __MIPS_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} +function __MIPS_write (addr, width, data) = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) + +val __TraceMemoryWrite : forall 'n 'm. + (atom('n), bits('m), bits(8 * 'n)) -> unit + +val __ReadRAM = "read_ram" : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __MIPS_read : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem} +function __MIPS_read (addr, width) = __ReadRAM(64, width, 0x0000_0000_0000_0000, addr) + +val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit + +val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) + +infix 8 ^^ +val operator ^^ = {lem: "replicate_bits"} : forall 'n 'm . (bits('n), atom('m)) -> bits('n * 'm) +function operator ^^ (bs, n) = replicate_bits (bs, n) + +val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)} + +function ex_nat 'n = n + +val cast ex_int : int -> {'n, true. atom('n)} + +function ex_int 'n = n + +/* +val cast ex_range : forall 'n 'm. range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('o)} + +function ex_range (n as 'N) = n +*/ + +val coerce_int_nat : int -> nat effect {escape} + +function coerce_int_nat 'x = { + assert(constraint('x >= 0)); + x +} + +val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0. + (bits('m), int, atom('n)) -> bits('n) + +val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) + +val print_int = "print_int" : (string, int) -> unit +val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit +val print_string = "print_string" : (string, string) -> unit + +union exception = { + ISAException : unit, + Error_not_implemented : string, + Error_misaligned_access : unit, + Error_EBREAK : unit, + Error_internal_error : unit +} + +val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) + +val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) +val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) + +function EXTS v = sign_extend(v, sizeof('m)) +function EXTZ v = zero_extend(v, sizeof('m)) + +val zeros : forall 'n, 'n >= 0 . unit -> bits('n) +function zeros() = replicate_bits (0b0,'n) + +val ones : forall 'n, 'n >= 0 . unit -> bits('n) +function ones() = replicate_bits (0b1,'n) + +infix 4 <_s +infix 4 >=_s +infix 4 <_u +infix 4 >=_u + +val operator <_s = {lem: "slt_vec"} : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_s = {lem: "sgteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool +val operator <_u = {lem: "ult_vec"} : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_u = {lem: "ugteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool + +function operator <_s (x, y) = signed(x) < signed(y) +function operator >=_s (x, y) = signed(x) >= signed(y) +function operator <_u (x, y) = unsigned(x) < unsigned(y) +function operator >=_u (x, y) = unsigned(x) >= unsigned(y) + +val cast bool_to_bits : bool -> bits(1) +function bool_to_bits x = if x then 0b1 else 0b0 + +val cast bit_to_bool : bit -> bool +function bit_to_bool bitone = true +and bit_to_bool bitzero = false + +val cast bits_to_bool : bits(1) -> bool +function bits_to_bool x = bit_to_bool(x[0]) + +infix 1 >> +infix 1 << +infix 1 >>_s + +val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) +val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) + +val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) +val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) + +overload operator >> = {shift_bits_right, shiftr} +overload operator << = {shift_bits_left, shiftl} +val operator >>_s = "shift_bits_right_arith" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) + +infix 7 *_s +val operator *_s = "smult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n) +infix 7 *_u +val operator *_u = "mult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n) + +val vector64 : int -> bits(64) + +function vector64 n = __raw_GetSlice_int(64, n, 0) + +val to_bits : forall 'l.(atom('l), int) -> bits('l) +function to_bits (l, n) = __raw_GetSlice_int(l, n, 0) + +function break () : unit -> unit = () + +val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o. + (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) + +val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o. + (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit) + +overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc} + +val mask : forall 'm 'n , 'm >= 'n > 0 . bits('m) -> bits('n) +function mask bs = bs['n - 1 .. 0] |