diff options
Diffstat (limited to 'mips')
41 files changed, 1 insertions, 5411 deletions
diff --git a/mips/.gitignore b/mips/.gitignore deleted file mode 100644 index 2ee9fde0..00000000 --- a/mips/.gitignore +++ /dev/null @@ -1,5 +0,0 @@ -mips.lem -mips_types.lem -mipsScript.sml -mips_typesScript.sml -mips_extrasScript.sml
\ No newline at end of file diff --git a/mips/Holmakefile b/mips/Holmakefile deleted file mode 100644 index a31bfd4f..00000000 --- a/mips/Holmakefile +++ /dev/null @@ -1,11 +0,0 @@ -LEMDIR=../../lem/hol-lib - -INCLUDES = $(LEMDIR) ../lib/hol - -all: mipsTheory.uo -.PHONY: all - -ifdef POLY -BASE_HEAP = ../lib/hol/sail-heap - -endif diff --git a/mips/LOOKING_FOR_SOMETHING.txt b/mips/LOOKING_FOR_SOMETHING.txt new file mode 100644 index 00000000..1f462863 --- /dev/null +++ b/mips/LOOKING_FOR_SOMETHING.txt @@ -0,0 +1 @@ +The mips spec. now lives at https://github.com/CTSRD-CHERI/sail-cheri-mips . diff --git a/mips/Makefile b/mips/Makefile deleted file mode 100644 index a156428a..00000000 --- a/mips/Makefile +++ /dev/null @@ -1,74 +0,0 @@ -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:=$(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 - $(SAIL) -ocaml -o mips -memo_z3 $(filter %.sail, $^) - -mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) Makefile ../sail - $(SAIL) -O -memo_z3 -c $(filter %.sail, $^) 1> $@ - -C_WARNINGS=-Wall -Wno-unused-but-set-variable -Wno-unused-label -Wno-unused-function -Wno-maybe-uninitialized -C_OPT=-O2 -GCOV_FLAGS= -mips_c: mips.c ../lib/sail.h ../lib/*.c Makefile - gcc $(C_OPT) $(C_WARNINGS) $(GCOV_FLAGS) -g -I ../lib $< ../lib/*.c -lgmp -lz -o $@ - -# Note that for coverage purposes O1 appears optimal. O0 means lots of obviously dead code but O2 risks reducing granularity too much. -mips_c_gcov: C_OPT=-O1 -mips_c_gcov: GCOV_FLAGS=-fprofile-arcs -ftest-coverage -mips_c_gcov: mips_c - -gcovr: - gcovr -r . --html --html-detail -o index.html - -sim.dtb: sim.dts - dtc -O dtb -o $@ -b 0 $< - -mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS) - $(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ -mips_no_tlb_types.lem: mips_no_tlb.lem - -mips.lem: $(MIPS_PRE) $(SAIL_LIB_DIR)/mono_rewrites.sail $(MIPS_TLB) $(MIPS_SAILS) - $(SAIL) -lem -o mips -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ -mips_types.lem: mips.lem - -mips.v: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) - $(SAIL) -coq -dcoq_undef_axioms -o mips -coq_lib mips_extras -undefined_gen -memo_z3 $^ -mips_types.v: mips.v - -MIPS_COQ = mips_types.v mips_extras.v mips.v -COQ_LIBS = -R ../../bbv/theories bbv -R ../lib/coq Sail - -%.vo: %.v - coqc $(COQ_LIBS) $< -mips.vo: mips_types.vo mips_extras.vo - -M%.thy: m%.lem m%_types.lem mips_extras.lem - lem -isa -outdir . -lib Sail=$(SAIL_DIR)/src/gen_lib -lib Sail=$(SAIL_DIR)/src/lem_interp $^ - sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy - -%Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem - lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -i $(SAIL_DIR)/lib/hol/sail2_prompt_monad.lem -i $(SAIL_DIR)/lib/hol/sail2_prompt.lem -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ - -%Theory.uo: %Script.sml - Holmake $@ - -LOC_FILES:=$(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) -include ../etc/loc.mk - -clean: - rm -rf mips Mips.thy mips.lem mips_types.lem _sbuild mips.c mips_c - rm -f mipsScript.sml mips_typesScript.sml mips_extrasScript.sml - rm -f mips.v mips_types.v $(MIPS_COQ:%.v=%.vo) $(MIPS_COQ:%.v=%.glob) $(MIPS_COQ:%.v=.%.aux) - -Holmake cleanAll diff --git a/mips/README b/mips/README deleted file mode 100644 index 8a641e69..00000000 --- a/mips/README +++ /dev/null @@ -1,24 +0,0 @@ -This directory contains a MIPS64-style architecture specification -written in Sail. To support integration with the CHERI ISA it is -split across several files, which must be given to sail in the -following order: - - 1. mips_prelude.sail contains definitions used in the rest of the - ISA, including register declarations and helper functions, for - example for performing address translation. - - 2. mips_wrappers.sail contains wrappers and hooks around certain - functions. In straight MIPS these are mostly identity functions, but - on CHERI they are substituted for functions which implement - CHERI-specific behaviour. - - 3. mips_insts.sail contains descriptions of instructions in the form - of AST members, decode and execute function clauses (using Sail's - scattered union/function definitions). - - 4. mips_epilogue.sail just closes the function and AST union definitions. - -The CHERI sail model extends this model by adding more declarations in a -file cheri_prelude.sail, included after mips_prelude.sail, replacing -the functions in mips_wrappers.sail and adding new instruction -definitions in cheri_insts.sail. diff --git a/mips/_CoqProject b/mips/_CoqProject deleted file mode 100644 index ad38d28d..00000000 --- a/mips/_CoqProject +++ /dev/null @@ -1,2 +0,0 @@ --R ../../bbv/theories bbv --R ../lib/coq Sail
\ No newline at end of file diff --git a/mips/doc/Makefile b/mips/doc/Makefile deleted file mode 100644 index 0220a4cc..00000000 --- a/mips/doc/Makefile +++ /dev/null @@ -1,7 +0,0 @@ -all: - cat preamble.tex ../mips_prelude.sail ../mips_wrappers.sail ../mips_insts.sail ../mips_epilogue.sail postamble.tex > mips_all.tex - pdflatex mips_all.tex - -clean: - rm -rf *~ - rm -rf mips_all.* diff --git a/mips/doc/postamble.tex b/mips/doc/postamble.tex deleted file mode 100644 index 892ef896..00000000 --- a/mips/doc/postamble.tex +++ /dev/null @@ -1,2 +0,0 @@ -\end{lstlisting} -\end{document} diff --git a/mips/doc/preamble.tex b/mips/doc/preamble.tex deleted file mode 100644 index 524ec736..00000000 --- a/mips/doc/preamble.tex +++ /dev/null @@ -1,177 +0,0 @@ - -\documentclass[10pt]{article} - -\usepackage[margin=1.0in]{geometry} -\usepackage[T1]{fontenc} -\usepackage[scaled=0.82]{beramono} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% for Lem listing -\usepackage[scaled=0.82]{beramono} -\usepackage{listings} - -\newsavebox{\codebox} - -\lstdefinelanguage{SailExtraKeywords} - {morekeywords= { -% from the sail lexer -and, -alias, -as, -bitzero, -bitone, -bits, -by, -case, -clause, -const, -dec, -default, -deinfix, -effect, -Effect, -end, -enumerate, -else, -exit, -extern, -false, -forall, -foreach, -function, -if, -in, -inc, -IN, -let, -member, -Nat, -Order, -pure, -rec, -register, -scattered, -struct, -switch, -then, -true, -Type, -typedef, -undefined, -union, -with, -val, -div, -mod, -quot, -rem, -barr, -rreg, -wreg, -rmem, -wmem, -undef, -unspec, -nondet, -bool,unit,vector,range,list,bit,nat, int, uint8,uint16,uint32,uint64,implicit -} -} - -\lstdefinelanguage{LemExtraKeywords} - {morekeywords= { -% from the lem lexer - as, - fun, - function, - with, - match, - let, - and, - in, - of, - rec, - type, - module, - rename, - struct, - end, - open, - import, - include, - true, - false, - begin, - if, - then, - else, - val, - class, - instance, - default_instance, - indreln, - forall, - exists, - inline, - lem_transform, - IN, - MEM, - declare, - infix, - field, - automatic, - manual, - exhaustive, - inexhaustive, - ascii_rep, - compile_message, - set_flag, - termination_argument, - pattern_match, - right_assoc, - left_assoc, - non_assoc, - special, - target_rep, - target_type, - target_const, - lemma, - assert, - theorem, - do, - witness, - check, - % coq notation - Inductive, - Prop, -% names of targets, - ocaml, - html, - coq, - hol, - isabelle, -% these seem to be used as keywors in indreln? - input, - output, -% and more keywords for specific target code that we quote - case, - definition, -} -} - -%\lstset{basicstyle=\footnotesize\ttfamily} % -%\lstset{keywordstyle=\pmb} -%\lstset{basicstyle=\footnotesize\ttfamily} % -\lstset{basicstyle=\ttfamily} % -\lstset{keywordstyle=\bfseries} -\lstset{language=Caml} -\lstset{defaultdialect=[Objective]Caml} -\lstset{alsolanguage=SailExtraKeywords} -\lstset{mathescape} - -\lstset{escapeinside={<@}{@>}} - -%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\begin{document} - -\begin{lstlisting} diff --git a/mips/gen/ast.hgen b/mips/gen/ast.hgen deleted file mode 100644 index a251adff..00000000 --- a/mips/gen/ast.hgen +++ /dev/null @@ -1,18 +0,0 @@ -| `MIPSThreadStart -| `MIPSRType of mipsRTypeOp * reg * reg * reg -| `MIPSIType of mipsITypeOp * reg * reg * bit16 -| `MIPSShiftI of mipsShiftIOp * reg * reg * bit5 -| `MIPSShiftV of mipsShiftVOp * reg * reg * reg -| `MIPSMulDiv of mipsMulDivOp * reg * reg -| `MIPSMFHiLo of mipsMFHiLoOp * reg -| `MIPSLUI of reg * bit16 -| `MIPSLoad of mipsWordWidth * bool * bool * reg * reg * bit16 (* width, signed, linked, base, rt, offset *) -| `MIPSStore of mipsWordWidth * bool * reg * reg * bit16 (* width, conditional, base, rt, offset *) -| `MIPSLSLR of bool * bool * bool * reg * reg * bit16 (* store, double, left, base, rt, offset *) -| `MIPSSYNC -| `MIPSBEQ of reg * reg * bit16 * bool * bool (* rs, rt, offset, not equal, likely *) -| `MIPSBCMPZ of reg * bit16 * mipsCmp * bool * bool (* rs, offset, cmp, link, likely *) -| `MIPSJ of bit26 -| `MIPSJAL of bit26 -| `MIPSJR of reg -| `MIPSJALR of reg * reg (* rs, rd *) diff --git a/mips/gen/fold.hgen b/mips/gen/fold.hgen deleted file mode 100644 index 05b9c808..00000000 --- a/mips/gen/fold.hgen +++ /dev/null @@ -1,19 +0,0 @@ -| `MIPSThreadStart -> (y_reg, y_sreg) -| `MIPSRType (op, rd, rs, rt) -> fold_reg rt (fold_reg rs (fold_reg rd (y_reg, y_sreg))) -| `MIPSIType (op, rs, rt, imm) -> fold_reg rs (fold_reg rt (y_reg, y_sreg)) -| `MIPSShiftI (op, rd, rt, imm) -> fold_reg rt (fold_reg rd (y_reg, y_sreg)) -| `MIPSShiftV (op, rd, rt, rs) -> fold_reg rs (fold_reg rt (fold_reg rd (y_reg, y_sreg))) -| `MIPSMulDiv (op, rs, rt) -> fold_reg rs (fold_reg rt (y_reg, y_sreg)) -| `MIPSMFHiLo (op, rs) -> fold_reg rs (y_reg, y_sreg) -| `MIPSLUI (rt, imm) -> fold_reg rt (y_reg, y_sreg) -| `MIPSLoad (width, signed, linked, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg)) -| `MIPSStore (width, conditional, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg)) -| `MIPSLSLR (store, double, left, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg)) -| `MIPSSYNC -> (y_reg, y_sreg) -| `MIPSBEQ (rs, rt, offset, ne, likely) -> fold_reg rs (fold_reg rt (y_reg, y_sreg)) -| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> fold_reg rs (y_reg, y_sreg) -| `MIPSJ (offset) -> (y_reg, y_sreg) -| `MIPSJAL (offset) -> fold_reg (IReg(R31)) (y_reg, y_sreg) -| `MIPSJR (rd) -> fold_reg rd (y_reg, y_sreg) -| `MIPSJALR (rd, rs) -> fold_reg rd (fold_reg rs (y_reg, y_sreg)) - diff --git a/mips/gen/herdtools_ast_to_shallow_ast.hgen b/mips/gen/herdtools_ast_to_shallow_ast.hgen deleted file mode 100644 index 7b1a58d9..00000000 --- a/mips/gen/herdtools_ast_to_shallow_ast.hgen +++ /dev/null @@ -1,121 +0,0 @@ -| `MIPSThreadStart -> - SYSCALL_THREAD_START - -| `MIPSStopFetching -> - ImplementationDefinedStopFetching0 - -(* Note different argument order, which reflects difference - between instruction encoding and asm format *) -| `MIPSRType (op, rd, rs, rt) -> - (translate_rtype_op op) - ( - translate_reg "rs" rs, - translate_reg "rt" rt, - translate_reg "rd" rd - ) - - -(* Note different argument order similar to above *) -| `MIPSIType (op, rt, rs, imm) -> - (translate_itype_op op) - ( - translate_reg "rs" rs, - translate_reg "rt" rt, - translate_imm16 "imm" imm - ) - - -| `MIPSShiftI (op, rd, rt, sa) -> - (translate_shifti_op op) - ( - translate_reg "rt" rt, - translate_reg "rd" rd, - translate_imm5 "sa" sa - ) - - -| `MIPSShiftV (op, rd, rt, rs) -> - (translate_shiftv_op op) - ( - translate_reg "rs" rs, - translate_reg "rt" rt, - translate_reg "rd" rd - ) - - -| `MIPSMulDiv (op, rs, rt) -> - (translate_muldiv_op op) - ( - translate_reg "rs" rs, - translate_reg "rt" rt - ) - - -| `MIPSMFHiLo (op, rs) -> - (translate_mfhilo_op op) - ( - translate_reg "rs" rs - ) - -| `MIPSLUI (rt, imm) -> - LUI - ( - translate_reg "rt" rt, - translate_imm16 "imm" imm - ) - -| `MIPSLoad (width, signed, linked, base, rt, offset) -> - Load - ( - translate_wordsize "width" width, - translate_bool "signed" signed, - translate_bool "linked" linked, - translate_reg "base" base, - translate_reg "rt" rt, - translate_imm16 "offset" offset - ) - -| `MIPSStore (width, conditional, base, rt, offset) -> - Store - ( - translate_wordsize "width" width, - translate_bool "conditional" conditional, - translate_reg "base" base, - translate_reg "rt" rt, - translate_imm16 "offset" offset - ) - -| `MIPSLSLR (store, double, left, base, rt, offset) -> - (translate_lslr_op store double left) - ( - translate_reg "base" base, - translate_reg "rt" rt, - translate_imm16 "offset" offset - ) - -| `MIPSSYNC -> SYNC -| `MIPSBEQ (rs, rt, offset, ne, likely) -> - BEQ - (translate_reg "rs" rs, - translate_reg "rt" rt, - translate_imm16 "offset" offset, - translate_bool "ne" ne, - translate_bool "likely" likely - ) - -| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> - BCMPZ - (translate_reg "rs" rs, - translate_imm16 "offset" offset, - translate_cmp "cmp" cmp, - translate_bool "link" link, - translate_bool "likely" likely - ) -| `MIPSJ (offset) -> - J (translate_imm26 "offset" offset) -| `MIPSJAL (offset) -> - JAL (translate_imm26 "offset" offset) -| `MIPSJR(rd) -> - JR (translate_reg "rd" rd) -| `MIPSJALR(rd, rs) -> - JALR (translate_reg "rd" rd, translate_reg "rs" rs) diff --git a/mips/gen/herdtools_types_to_shallow_types.hgen b/mips/gen/herdtools_types_to_shallow_types.hgen deleted file mode 100644 index 5a0e3bfc..00000000 --- a/mips/gen/herdtools_types_to_shallow_types.hgen +++ /dev/null @@ -1,120 +0,0 @@ -let is_inc = false - -let translate_rtype_op op = uppercase (pp_rtype_op op) - -let translate_rtype_op op x = match op with - | MIPSROpADD -> ADD x - | MIPSROpADDU -> ADDU x - | MIPSROpAND -> AND x - | MIPSROpDADD -> DADD x - | MIPSROpDADDU -> DADDU x - | MIPSROpDSUB -> DSUB x - | MIPSROpDSUBU -> DSUBU x - | MIPSROpMOVN -> MOVN x - | MIPSROpMOVZ -> MOVZ x - | MIPSROpMUL -> MUL x - | MIPSROpNOR -> NOR x - | MIPSROpOR -> OR x - | MIPSROpSLT -> SLT x - | MIPSROpSLTU -> SLTU x - | MIPSROpSUB -> SUB x - | MIPSROpSUBU -> SUBU x - | MIPSROpXOR -> XOR x - -let translate_itype_op op x = match op with - | MIPSIOpADDI -> ADDI x - | MIPSIOpADDIU -> ADDIU x - | MIPSIOpANDI -> ANDI x - | MIPSIOpDADDI -> DADDI x - | MIPSIOpDADDIU -> DADDIU x - | MIPSIOpORI -> ORI x - | MIPSIOpSLTI -> SLTI x - | MIPSIOpSLTIU -> SLTIU x - | MIPSIOpXORI -> XORI x - -let translate_shifti_op op x = match op with - | MIPSDSLL -> DSLL x - | MIPSDSLL32 -> DSLL32 x - | MIPSDSRA -> DSRA x - | MIPSDSRA32 -> DSRA32 x - | MIPSDSRL -> DSRL x - | MIPSDSRL32 -> DSRL32 x - | MIPSSLL -> SLL x - | MIPSSRA -> SRA x - | MIPSSRL -> SRL x - -let translate_shiftv_op op x = match op with - | MIPSDSLLV -> DSLLV x - | MIPSDSRAV -> DSRAV x - | MIPSDSRLV -> DSRLV x - | MIPSSLLV -> SLLV x - | MIPSSRAV -> SRAV x - | MIPSSRLV -> SRLV x - -let translate_muldiv_op op x = match op with - | MIPSDDIV -> DDIV x - | MIPSDDIVU -> DDIVU x - | MIPSDIV -> DIV x - | MIPSDIVU -> DIVU x - | MIPSDMULT -> DMULT x - | MIPSDMULTU -> DMULTU x - | MIPSMADD -> MADD x - | MIPSMADDU -> MADDU x - | MIPSMSUB -> MSUB x - | MIPSMSUBU -> MSUBU x - | MIPSMULT -> MULT x - | MIPSMULTU -> MULTU x - -let translate_mfhilo_op op x = match op with - | MIPSMFHI -> MFHI x - | MIPSMFLO -> MFLO x - | MIPSMTHI -> MTHI x - | MIPSMTLO -> MTLO x - -let translate_load_op width signed linked = uppercase (pp_load_op width signed linked) - -let translate_store_op width conditional = uppercase (pp_store_op width conditional) - -let translate_lslr_op store double left x = match (store,double,left) with - | (false, false, true ) -> LWL x - | (false, false, false) -> LWR x - | (false, true , true ) -> LDL x - | (false, true , false) -> LDR x - | (true , false, true ) -> SWL x - | (true , false, false) -> SWR x - | (true , true , true ) -> SDL x - | (true , true , false) -> SDR x - -let translate_beq_op ne likely = uppercase (pp_beq_op ne likely) - -let translate_bcmpz_op cmp link likely = uppercase (pp_bcmpz_op cmp link likely) - - -let translate_reg name value = - Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int (reg_to_int value)) - -let translate_imm26 name value = - Sail_values.to_vec0 is_inc (Nat_big_num.of_int 26,Nat_big_num.of_int value) -let translate_imm16 name value = - Sail_values.to_vec0 is_inc (Nat_big_num.of_int 16,Nat_big_num.of_int value) -let translate_imm5 name value = - Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int value) -let translate_bool name = function - | true -> Sail_values.B1 - | false -> Sail_values.B0 - -let translate_wordsize _ = function - | MIPSByte -> Mips_embed_types.B2 - | MIPSHalf -> Mips_embed_types.H - | MIPSWord -> Mips_embed_types.W - | MIPSDouble -> Mips_embed_types.D - -let translate_cmp _ = function - | MIPS_EQ -> EQ' - | MIPS_NE -> NE - | MIPS_GE -> GE - | MIPS_GEU -> GEU - | MIPS_GT -> GT' - | MIPS_LE -> LE - | MIPS_LT -> LT' - | MIPS_LTU -> LTU diff --git a/mips/gen/lexer.hgen b/mips/gen/lexer.hgen deleted file mode 100644 index c01b14cc..00000000 --- a/mips/gen/lexer.hgen +++ /dev/null @@ -1,116 +0,0 @@ -"add" , RTYPE {txt="ADD" ; op=MIPSROpADD }; -"addu" , RTYPE {txt="ADDU" ; op=MIPSROpADDU }; -"and" , RTYPE {txt="AND" ; op=MIPSROpAND }; -"dadd" , RTYPE {txt="DADD" ; op=MIPSROpDADD }; -"daddu" , RTYPE {txt="DADDU" ; op=MIPSROpDADDU }; -"dsub" , RTYPE {txt="DSUB" ; op=MIPSROpDSUB }; -"dsubu" , RTYPE {txt="DSUBU" ; op=MIPSROpDSUBU }; -"movn" , RTYPE {txt="MOVN" ; op=MIPSROpMOVN }; -"movz" , RTYPE {txt="MOVZ" ; op=MIPSROpMOVZ }; -"mul" , RTYPE {txt="MUL" ; op=MIPSROpMUL }; -"nor" , RTYPE {txt="NOR" ; op=MIPSROpNOR }; -"or" , RTYPE {txt="OR" ; op=MIPSROpOR }; -"slt" , RTYPE {txt="SLT" ; op=MIPSROpSLT }; -"sltu" , RTYPE {txt="SLTU" ; op=MIPSROpSLTU }; -"sub" , RTYPE {txt="SUB" ; op=MIPSROpSUB }; -"subu" , RTYPE {txt="SUBU" ; op=MIPSROpSUBU }; -"xor" , RTYPE {txt="XOR" ; op=MIPSROpXOR }; - -"addi" , ITYPE {txt="ADDI" ; op=MIPSIOpADDI }; -"addiu" , ITYPE {txt="ADDIU" ; op=MIPSIOpADDIU }; -"andi" , ITYPE {txt="ANDI" ; op=MIPSIOpANDI }; -"daddi" , ITYPE {txt="DADDI" ; op=MIPSIOpDADDI }; -"daddiu", ITYPE {txt="DADDIU"; op=MIPSIOpDADDIU }; -"ori" , ITYPE {txt="ORI" ; op=MIPSIOpORI }; -"slti" , ITYPE {txt="SLTI" ; op=MIPSIOpSLTI }; -"sltiu" , ITYPE {txt="SLTIU" ; op=MIPSIOpSLTIU }; -"xori" , ITYPE {txt="XORI" ; op=MIPSIOpXORI }; - -"dsll" , SHIFTI {txt="DSLL" ; op=MIPSDSLL }; -"dsll32" , SHIFTI {txt="DSLL32" ; op=MIPSDSLL32 }; -"dsra" , SHIFTI {txt="DSRA" ; op=MIPSDSRA }; -"dsra32" , SHIFTI {txt="DSRA32" ; op=MIPSDSRA32 }; -"dsrl" , SHIFTI {txt="DSRL" ; op=MIPSDSRL }; -"dsrl32" , SHIFTI {txt="DSRL32" ; op=MIPSDSRL32 }; -"sll" , SHIFTI {txt="SLL" ; op=MIPSSLL }; -"sra" , SHIFTI {txt="SRA" ; op=MIPSSRA }; -"srl" , SHIFTI {txt="SRL" ; op=MIPSSRL }; - -"dsllv", SHIFTV {txt="DSLLV" ; op=MIPSDSLLV }; -"dsrav", SHIFTV {txt="DSRAV" ; op=MIPSDSRAV }; -"dsrlv", SHIFTV {txt="DSRLV" ; op=MIPSDSRLV }; -"sllv" , SHIFTV {txt="SLLV" ; op=MIPSSLLV }; -"srav" , SHIFTV {txt="SRAV" ; op=MIPSSRAV }; -"srlv" , SHIFTV {txt="SRLV" ; op=MIPSSRLV }; - -"ddiv" , MULDIV {txt="DDIV" ; op=MIPSDDIV }; -"ddivu" , MULDIV {txt="DDIVU" ; op=MIPSDDIVU }; -"div" , MULDIV {txt="DIV" ; op=MIPSDIV }; -"divu" , MULDIV {txt="DIVU" ; op=MIPSDIVU }; -"dmult" , MULDIV {txt="DMULT" ; op=MIPSDMULT }; -"dmultu", MULDIV {txt="DMULTU"; op=MIPSDMULTU }; -"madd" , MULDIV {txt="MADD" ; op=MIPSMADD }; -"maddu" , MULDIV {txt="MADDU" ; op=MIPSMADDU }; -"msub" , MULDIV {txt="MSUB" ; op=MIPSMSUB }; -"msubu" , MULDIV {txt="MSUBU" ; op=MIPSMSUBU }; -"mult" , MULDIV {txt="MULT" ; op=MIPSMULT }; -"multu" , MULDIV {txt="MULTU" ; op=MIPSMULTU }; - -"mfhi" , MFHILO {txt="MFHI" ; op=MIPSMFHI }; -"mflo" , MFHILO {txt="MFLO" ; op=MIPSMFLO }; -"mthi" , MFHILO {txt="MTHI" ; op=MIPSMTHI }; -"mtlo" , MFHILO {txt="MTLO" ; op=MIPSMTLO }; - -"lui" , LUI {txt="LUI" }; - -"lb" , LOAD {txt="LB" ; width=MIPSByte ; signed=true; linked=false }; -"lbu" , LOAD {txt="LBU" ; width=MIPSByte ; signed=false; linked=false }; -"lh" , LOAD {txt="LH" ; width=MIPSHalf ; signed=true; linked=false }; -"lhu" , LOAD {txt="LHU" ; width=MIPSHalf ; signed=false; linked=false }; -"lw" , LOAD {txt="LW" ; width=MIPSWord ; signed=true; linked=false }; -"lwu" , LOAD {txt="LWU" ; width=MIPSWord ; signed=false; linked=false }; -"ld" , LOAD {txt="LD" ; width=MIPSDouble ; signed=false; linked=false }; -"ll" , LOAD {txt="LL" ; width=MIPSWord ; signed=true; linked=true }; -"lld" , LOAD {txt="LLD" ; width=MIPSDouble ; signed=false; linked=true }; - -"sb" , STORE {txt="SB" ; width=MIPSByte ; conditional=false }; -"sh" , STORE {txt="SH" ; width=MIPSHalf ; conditional=false }; -"sw" , STORE {txt="SW" ; width=MIPSWord ; conditional=false }; -"sd" , STORE {txt="SD" ; width=MIPSDouble ; conditional=false }; -"sc" , STORE {txt="SC" ; width=MIPSWord ; conditional=true }; -"scd" , STORE {txt="SCD" ; width=MIPSDouble ; conditional=true }; - -"lwl" , LSLR {txt="LWL" ; store=false; double=false; left=true }; -"lwr" , LSLR {txt="LWR" ; store=false; double=false; left=false}; -"ldl" , LSLR {txt="LDL" ; store=false; double=true ; left=true }; -"ldr" , LSLR {txt="LDR" ; store=false; double=true ; left=false}; -"swl" , LSLR {txt="SWL" ; store=true ; double=false; left=true }; -"swr" , LSLR {txt="SWR" ; store=true ; double=false; left=false}; -"sdl" , LSLR {txt="SDL" ; store=true ; double=true ; left=true }; -"sdr" , LSLR {txt="SDR" ; store=true ; double=true ; left=false}; -"sync", SYNC {txt="SYNC"}; - -"beq", BEQ {txt="BEQ"; ne=false; likely=false }; -"beql", BEQ {txt="BEQ"; ne=false; likely=true }; -"bne", BEQ {txt="BEQ"; ne=true ; likely=false }; -"bnel", BEQ {txt="BEQ"; ne=true ; likely=true }; - -"bltz", BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=false; link=false }; -"bltzal", BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=false; link=true }; -"bltzl", BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=true; link=false }; -"bltzall",BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=true; link=true }; - -"bgez", BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=false; link=false }; -"bgezal", BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=false; link=true }; -"bgezl", BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=true; link=false }; -"bgezall",BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=true; link=true }; - -"bgtz", BCMPZ {txt="BCMPZ"; cmp=MIPS_GT; likely=false; link=false }; -"bgtzl", BCMPZ {txt="BCMPZ"; cmp=MIPS_GT; likely=true; link=false }; - -"blez", BCMPZ {txt="BCMPZ"; cmp=MIPS_LE; likely=false; link=false }; -"blezl", BCMPZ {txt="BCMPZ"; cmp=MIPS_LE; likely=true; link=false }; -"j", J {txt="J"}; -"jal", JAL {txt="JAL"}; -"jr", JR {txt="JR"}; -"jalr", JALR {txt="JALR"}; diff --git a/mips/gen/map.hgen b/mips/gen/map.hgen deleted file mode 100644 index f5116bae..00000000 --- a/mips/gen/map.hgen +++ /dev/null @@ -1,19 +0,0 @@ -| `MIPSThreadStart -> `MIPSThreadStart -| `MIPSRType (op, rd, rs, rt) -> `MIPSRType (op, map_reg rd, map_reg rs, map_reg rt) -| `MIPSIType (op, rs, rt, imm) -> `MIPSIType (op, map_reg rs, map_reg rt, imm) -| `MIPSShiftI (op, rd, rt, imm) -> `MIPSShiftI (op, map_reg rd, map_reg rt, imm) -| `MIPSShiftV (op, rd, rt, rs) -> `MIPSShiftV (op, map_reg rd, map_reg rt, map_reg rs) -| `MIPSMulDiv (op, rs, rt) -> `MIPSMulDiv (op, map_reg rs, map_reg rt) -| `MIPSMFHiLo (op, rs) -> `MIPSMFHiLo (op, map_reg rs) -| `MIPSLUI (rt, imm) -> `MIPSLUI (map_reg rt, imm) -| `MIPSLoad (width, signed, linked, base, rt, offset) -> `MIPSLoad (width, signed, linked, map_reg base, map_reg rt, offset) -| `MIPSStore (width, conditional, base, rt, offset) -> `MIPSStore (width, conditional, map_reg base, map_reg rt, offset) -| `MIPSLSLR (store, double, left, base, rt, offset) -> `MIPSLSLR (store, double, left, map_reg base, map_reg rt, offset) -| `MIPSSYNC -> `MIPSSYNC -| `MIPSBEQ (rs, rt, offset, ne, likely) -> `MIPSBEQ (map_reg rs, map_reg rt, offset, ne, likely) -| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> `MIPSBCMPZ (map_reg rs, offset, cmp, link, likely) -| `MIPSJ (offset) -> `MIPSJ (offset) -| `MIPSJAL (offset) -> `MIPSJAL (offset) (* implicit R31? *) -| `MIPSJR (rd) -> `MIPSJR (map_reg rd) -| `MIPSJALR (rd, rs) -> `MIPSJALR(map_reg rd, map_reg rs) - diff --git a/mips/gen/parser.hgen b/mips/gen/parser.hgen deleted file mode 100644 index 8f573aa5..00000000 --- a/mips/gen/parser.hgen +++ /dev/null @@ -1,34 +0,0 @@ -| RTYPE reg COMMA reg COMMA reg - { `MIPSRType ($1.op, $2, $4, $6) } -| ITYPE reg COMMA reg COMMA NUM - { `MIPSIType ($1.op, $2, $4, $6) } -| SHIFTI reg COMMA reg COMMA NUM - { `MIPSShiftI ($1.op, $2, $4, $6) } -| SHIFTV reg COMMA reg COMMA reg - { `MIPSShiftV ($1.op, $2, $4, $6) } -| MULDIV reg COMMA reg - { `MIPSMulDiv ($1.op, $2, $4) } -| MFHILO reg - { `MIPSMFHiLo ($1.op, $2) } -| LUI reg COMMA NUM - { `MIPSLUI ($2, $4) } -| LOAD reg COMMA NUM LPAR reg RPAR - { `MIPSLoad ($1.width, $1.signed, $1.linked, $6, $2, $4) } -| STORE reg COMMA NUM LPAR reg RPAR - { `MIPSStore ($1.width, $1.conditional, $6, $2, $4) } -| LSLR reg COMMA NUM LPAR reg RPAR - { `MIPSLSLR ($1.store, $1.double, $1.left, $6, $2, $4) } -| SYNC - { `MIPSSYNC } -| BEQ reg COMMA reg COMMA NUM - { `MIPSBEQ ( $2, $4, $6, $1.ne, $1.likely) } -| BCMPZ reg COMMA NUM - { `MIPSBCMPZ ( $2, $4, $1.cmp, $1.link, $1.likely) } -| J NUM - { `MIPSJ ($2) } -| JAL NUM - { `MIPSJAL ($2) } -| JR reg - { `MIPSJR ($2) } -| JALR reg COMMA reg - { `MIPSJALR ($2, $4) } diff --git a/mips/gen/pretty.hgen b/mips/gen/pretty.hgen deleted file mode 100644 index 98f56f2e..00000000 --- a/mips/gen/pretty.hgen +++ /dev/null @@ -1,36 +0,0 @@ -| `MIPSThreadStart -> "syscall 0xfffff" (* thread start *) -| `MIPSStopFetching -> "STOP" (* TODO *) -| `MIPSRType (op, rd,rs,rt) -> - sprintf "%s %s,%s,%s" (pp_rtype_op op) (pp_reg rd) (pp_reg rs) (pp_reg rt) -| `MIPSIType (op,rd,rs,imm) -> - sprintf "%s %s,%s,%d" (pp_itype_op op) (pp_reg rd) (pp_reg rs) imm -| `MIPSShiftI (op, rs, rt, imm) -> - sprintf "%s %s,%s,%d" (pp_shifti_op op) (pp_reg rs) (pp_reg rt) imm -| `MIPSShiftV (op, rd,rs,rt) -> - sprintf "%s %s,%s,%s" (pp_shiftv_op op) (pp_reg rd) (pp_reg rs) (pp_reg rt) -| `MIPSMulDiv (op, rs, rt) -> - sprintf "%s %s,%s" (pp_muldiv_op op) (pp_reg rs) (pp_reg rt) -| `MIPSMFHiLo (op, rs) -> - sprintf "%s %s" (pp_mfhilo_op op) (pp_reg rs) -| `MIPSLUI (rt, imm) -> - sprintf "lui %s,%d" (pp_reg rt) imm -| `MIPSLoad (width, signed, linked, base, rt, offset) -> - sprintf "%s %s,%d(%s)" (pp_load_op width signed linked) (pp_reg rt) offset (pp_reg base) -| `MIPSStore (width, conditional, base, rt, offset) -> - sprintf "%s %s,%d(%s)" (pp_store_op width conditional) (pp_reg rt) offset (pp_reg base) -| `MIPSLSLR (store, double, left, base, rt, offset) -> - sprintf "%s %s,%d(%s)" (pp_lslr_op store double left) (pp_reg rt) offset (pp_reg base) -| `MIPSSYNC -> "sync" -| `MIPSBEQ (rs, rt, offset, ne, likely) -> - sprintf "%s %s,%s,.%+d" (pp_beq_op ne likely) (pp_reg rs) (pp_reg rt) offset -| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> - sprintf "%s,%s,.%+d" (pp_bcmpz_op cmp link likely) (pp_reg rs) offset -| `MIPSJ (offset) -> - sprintf "j %d" offset -| `MIPSJAL (offset) -> - sprintf "jal %d" offset -| `MIPSJR(rd) -> - sprintf "jr %s" (pp_reg rd) -| `MIPSJALR(rd, rs) -> - sprintf "jalr %s,%s" (pp_reg rd) (pp_reg rs) - diff --git a/mips/gen/sail_trans_out.hgen b/mips/gen/sail_trans_out.hgen deleted file mode 100644 index f2d006e8..00000000 --- a/mips/gen/sail_trans_out.hgen +++ /dev/null @@ -1,98 +0,0 @@ -| ("SYSCALL_THREAD_START", []) -> `MIPSThreadStart -| ("ADD" , [rs; rt; rd]) -> `MIPSRType (MIPSROpADD , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("ADDU" , [rs; rt; rd]) -> `MIPSRType (MIPSROpADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("AND" , [rs; rt; rd]) -> `MIPSRType (MIPSROpAND , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("DADD" , [rs; rt; rd]) -> `MIPSRType (MIPSROpDADD , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("DADDU" , [rs; rt; rd]) -> `MIPSRType (MIPSROpDADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("DSUB" , [rs; rt; rd]) -> `MIPSRType (MIPSROpDSUB , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("DSUBU" , [rs; rt; rd]) -> `MIPSRType (MIPSROpDSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("MOVN" , [rs; rt; rd]) -> `MIPSRType (MIPSROpMOVN , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("MOVZ" , [rs; rt; rd]) -> `MIPSRType (MIPSROpMOVZ , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("MUL" , [rs; rt; rd]) -> `MIPSRType (MIPSROpMUL , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("NOR" , [rs; rt; rd]) -> `MIPSRType (MIPSROpNOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("OR" , [rs; rt; rd]) -> `MIPSRType (MIPSROpOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("SLT" , [rs; rt; rd]) -> `MIPSRType (MIPSROpSLT , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("SLTU" , [rs; rt; rd]) -> `MIPSRType (MIPSROpSLTU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("SUB" , [rs; rt; rd]) -> `MIPSRType (MIPSROpSUB , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("SUBU" , [rs; rt; rd]) -> `MIPSRType (MIPSROpSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| ("XOR" , [rs; rt; rd]) -> `MIPSRType (MIPSROpXOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) - -| ("ADDI" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| ("ADDIU" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpADDIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| ("ANDI" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpANDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm)) -| ("DADDI" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpDADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| ("DADDIU", [rs; rt; imm]) -> `MIPSIType (MIPSIOpDADDIU,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| ("ORI" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpORI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm)) -| ("SLTI" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpSLTI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| ("SLTIU" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpSLTIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| ("XORI" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpXORI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm)) - -| ("DSLL" , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSLL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| ("DSLL32" , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSLL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| ("DSRA" , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSRA , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| ("DSRA32" , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSRA32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| ("DSRL" , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSRL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| ("DSRL32" , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSRL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| ("SLL" , [rt; rd; sa]) -> `MIPSShiftI (MIPSSLL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| ("SRA" , [rt; rd; sa]) -> `MIPSShiftI (MIPSSRA , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| ("SRL" , [rt; rd; sa]) -> `MIPSShiftI (MIPSSRL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) - -| "DSLLV" , [rs; rt; rd] -> `MIPSShiftV (MIPSDSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) -| "DSRAV" , [rs; rt; rd] -> `MIPSShiftV (MIPSDSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) -| "DSRLV" , [rs; rt; rd] -> `MIPSShiftV (MIPSDSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) -| "SLLV" , [rs; rt; rd] -> `MIPSShiftV (MIPSSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) -| "SRAV" , [rs; rt; rd] -> `MIPSShiftV (MIPSSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) -| "SRLV" , [rs; rt; rd] -> `MIPSShiftV (MIPSSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) - -| "DDIV" , [rs; rt] -> `MIPSMulDiv (MIPSDDIV , (translate_out_ireg rs), (translate_out_ireg rt)) -| "DDIVU" , [rs; rt] -> `MIPSMulDiv (MIPSDDIVU , (translate_out_ireg rs), (translate_out_ireg rt)) -| "DIV" , [rs; rt] -> `MIPSMulDiv (MIPSDIV , (translate_out_ireg rs), (translate_out_ireg rt)) -| "DIVU" , [rs; rt] -> `MIPSMulDiv (MIPSDIVU , (translate_out_ireg rs), (translate_out_ireg rt)) -| "DMULT" , [rs; rt] -> `MIPSMulDiv (MIPSDMULT , (translate_out_ireg rs), (translate_out_ireg rt)) -| "DMULTU", [rs; rt] -> `MIPSMulDiv (MIPSDMULTU , (translate_out_ireg rs), (translate_out_ireg rt)) -| "MADD" , [rs; rt] -> `MIPSMulDiv (MIPSMADD , (translate_out_ireg rs), (translate_out_ireg rt)) -| "MADDU" , [rs; rt] -> `MIPSMulDiv (MIPSMADDU , (translate_out_ireg rs), (translate_out_ireg rt)) -| "MSUB" , [rs; rt] -> `MIPSMulDiv (MIPSMSUB , (translate_out_ireg rs), (translate_out_ireg rt)) -| "MSUBU" , [rs; rt] -> `MIPSMulDiv (MIPSMSUBU , (translate_out_ireg rs), (translate_out_ireg rt)) -| "MULT" , [rs; rt] -> `MIPSMulDiv (MIPSMULT , (translate_out_ireg rs), (translate_out_ireg rt)) -| "MULTU" , [rs; rt] -> `MIPSMulDiv (MIPSMULTU , (translate_out_ireg rs), (translate_out_ireg rt)) - -| "MFHI" , [rs] -> `MIPSMFHiLo (MIPSMFHI, (translate_out_ireg rs)) -| "MFLO" , [rs] -> `MIPSMFHiLo (MIPSMFLO, (translate_out_ireg rs)) -| "MTHI" , [rs] -> `MIPSMFHiLo (MIPSMTHI, (translate_out_ireg rs)) -| "MTLO" , [rs] -> `MIPSMFHiLo (MIPSMTLO, (translate_out_ireg rs)) - -| "LUI" , [rt; imm] -> `MIPSLUI ((translate_out_ireg rt), (translate_out_imm16 imm)) -| "Load", [width; signed; linked; base; rt; offset] -> - `MIPSLoad ( - (translate_out_wordWidth width), - (translate_out_bool signed), - (translate_out_bool linked), - (translate_out_ireg base), - (translate_out_ireg rt), - (translate_out_simm16 offset) - ) -| "Store", [width; conditional; base; rt; offset] -> - `MIPSStore ( - (translate_out_wordWidth width), - (translate_out_bool conditional), - (translate_out_ireg base), - (translate_out_ireg rt), - (translate_out_simm16 offset) - ) -| "LWL", [base; rt; offset] -> `MIPSLSLR (false, false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| "LWR", [base; rt; offset] -> `MIPSLSLR (false, false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| "LDL", [base; rt; offset] -> `MIPSLSLR (false, true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| "LDR", [base; rt; offset] -> `MIPSLSLR (false, true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| "SWL", [base; rt; offset] -> `MIPSLSLR (true , false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| "SWR", [base; rt; offset] -> `MIPSLSLR (true , false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| "SDL", [base; rt; offset] -> `MIPSLSLR (true , true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| "SDR", [base; rt; offset] -> `MIPSLSLR (true , true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| "SYNC", [] -> `MIPSSYNC -| "BEQ", [rs; rt; offset; ne; likely] -> `MIPSBEQ ((translate_out_ireg rs), (translate_out_ireg rt), (translate_out_simm16 offset), (translate_out_bool ne), (translate_out_bool likely)) -| "BCMPZ", [rs; offset; cmp; link; likely] -> `MIPSBCMPZ ((translate_out_ireg rs), (translate_out_simm16 offset), (translate_out_cmp cmp), (translate_out_bool link), (translate_out_bool likely)) -| "J", [offset] -> `MIPSJ (translate_out_imm26 offset) -| "JAL", [offset] -> `MIPSJAL (translate_out_imm26 offset) -| "JR", [rd] -> `MIPSJR (translate_out_ireg rd) -| "JALR", [rd; rs] -> `MIPSJALR (translate_out_ireg rd, translate_out_ireg rs) - diff --git a/mips/gen/shallow_ast_to_herdtools_ast.hgen b/mips/gen/shallow_ast_to_herdtools_ast.hgen deleted file mode 100644 index efe2c77e..00000000 --- a/mips/gen/shallow_ast_to_herdtools_ast.hgen +++ /dev/null @@ -1,98 +0,0 @@ -| SYSCALL_THREAD_START -> `MIPSThreadStart -| (ADD (rs, rt, rd)) -> `MIPSRType (MIPSROpADD , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (ADDU (rs, rt, rd)) -> `MIPSRType (MIPSROpADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (AND (rs, rt, rd)) -> `MIPSRType (MIPSROpAND , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (DADD (rs, rt, rd)) -> `MIPSRType (MIPSROpDADD , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (DADDU (rs, rt, rd)) -> `MIPSRType (MIPSROpDADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (DSUB (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUB , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (DSUBU (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (MOVN (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVN , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (MOVZ (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVZ , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (MUL (rs, rt, rd)) -> `MIPSRType (MIPSROpMUL , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (NOR (rs, rt, rd)) -> `MIPSRType (MIPSROpNOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (OR (rs, rt, rd)) -> `MIPSRType (MIPSROpOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (SLT (rs, rt, rd)) -> `MIPSRType (MIPSROpSLT , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (SLTU (rs, rt, rd)) -> `MIPSRType (MIPSROpSLTU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (SUB (rs, rt, rd)) -> `MIPSRType (MIPSROpSUB , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (SUBU (rs, rt, rd)) -> `MIPSRType (MIPSROpSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) -| (XOR (rs, rt, rd)) -> `MIPSRType (MIPSROpXOR , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt)) - -| (ADDI (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| (ADDIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| (ANDI (rs, rt, imm)) -> `MIPSIType (MIPSIOpANDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm)) -| (DADDI (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| (DADDIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDIU,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| (ORI (rs, rt, imm)) -> `MIPSIType (MIPSIOpORI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm)) -| (SLTI (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| (SLTIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm)) -| (XORI (rs, rt, imm)) -> `MIPSIType (MIPSIOpXORI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm)) - -| (DSLL (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| (DSLL32 (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| (DSRA (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| (DSRA32 (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| (DSRL (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| (DSRL32 (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| (SLL (rt, rd, sa)) -> `MIPSShiftI (MIPSSLL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| (SRA (rt, rd, sa)) -> `MIPSShiftI (MIPSSRA , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) -| (SRL (rt, rd, sa)) -> `MIPSShiftI (MIPSSRL , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa)) - -| DSLLV (rs, rt, rd) -> `MIPSShiftV (MIPSDSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) -| DSRAV (rs, rt, rd) -> `MIPSShiftV (MIPSDSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) -| DSRLV (rs, rt, rd) -> `MIPSShiftV (MIPSDSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) -| SLLV (rs, rt, rd) -> `MIPSShiftV (MIPSSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) -| SRAV (rs, rt, rd) -> `MIPSShiftV (MIPSSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) -| SRLV (rs, rt, rd) -> `MIPSShiftV (MIPSSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs)) - -| DDIV (rs, rt) -> `MIPSMulDiv (MIPSDDIV , (translate_out_ireg rs), (translate_out_ireg rt)) -| DDIVU (rs, rt) -> `MIPSMulDiv (MIPSDDIVU , (translate_out_ireg rs), (translate_out_ireg rt)) -| DIV (rs, rt) -> `MIPSMulDiv (MIPSDIV , (translate_out_ireg rs), (translate_out_ireg rt)) -| DIVU (rs, rt) -> `MIPSMulDiv (MIPSDIVU , (translate_out_ireg rs), (translate_out_ireg rt)) -| DMULT (rs, rt) -> `MIPSMulDiv (MIPSDMULT , (translate_out_ireg rs), (translate_out_ireg rt)) -| DMULTU (rs, rt) -> `MIPSMulDiv (MIPSDMULTU , (translate_out_ireg rs), (translate_out_ireg rt)) -| MADD (rs, rt) -> `MIPSMulDiv (MIPSMADD , (translate_out_ireg rs), (translate_out_ireg rt)) -| MADDU (rs, rt) -> `MIPSMulDiv (MIPSMADDU , (translate_out_ireg rs), (translate_out_ireg rt)) -| MSUB (rs, rt) -> `MIPSMulDiv (MIPSMSUB , (translate_out_ireg rs), (translate_out_ireg rt)) -| MSUBU (rs, rt) -> `MIPSMulDiv (MIPSMSUBU , (translate_out_ireg rs), (translate_out_ireg rt)) -| MULT (rs, rt) -> `MIPSMulDiv (MIPSMULT , (translate_out_ireg rs), (translate_out_ireg rt)) -| MULTU (rs, rt) -> `MIPSMulDiv (MIPSMULTU , (translate_out_ireg rs), (translate_out_ireg rt)) - -| MFHI (rs) -> `MIPSMFHiLo (MIPSMFHI, (translate_out_ireg rs)) -| MFLO (rs) -> `MIPSMFHiLo (MIPSMFLO, (translate_out_ireg rs)) -| MTHI (rs) -> `MIPSMFHiLo (MIPSMTHI, (translate_out_ireg rs)) -| MTLO (rs) -> `MIPSMFHiLo (MIPSMTLO, (translate_out_ireg rs)) - -| LUI (rt, imm) -> `MIPSLUI ((translate_out_ireg rt), (translate_out_imm16 imm)) -| Load (width, signed, linked, base, rt, offset) -> - `MIPSLoad ( - (translate_out_wordWidth width), - (translate_out_bool signed), - (translate_out_bool linked), - (translate_out_ireg base), - (translate_out_ireg rt), - (translate_out_simm16 offset) - ) -| Store (width, conditional, base, rt, offset) -> - `MIPSStore ( - (translate_out_wordWidth width), - (translate_out_bool conditional), - (translate_out_ireg base), - (translate_out_ireg rt), - (translate_out_simm16 offset) - ) -| LWL (base, rt, offset) -> `MIPSLSLR (false, false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| LWR (base, rt, offset) -> `MIPSLSLR (false, false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| LDL (base, rt, offset) -> `MIPSLSLR (false, true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| LDR (base, rt, offset) -> `MIPSLSLR (false, true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| SWL (base, rt, offset) -> `MIPSLSLR (true , false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| SWR (base, rt, offset) -> `MIPSLSLR (true , false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| SDL (base, rt, offset) -> `MIPSLSLR (true , true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| SDR (base, rt, offset) -> `MIPSLSLR (true , true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset)) -| SYNC -> `MIPSSYNC -| BEQ (rs, rt, offset, ne, likely) -> `MIPSBEQ ((translate_out_ireg rs), (translate_out_ireg rt), (translate_out_simm16 offset), (translate_out_bool ne), (translate_out_bool likely)) -| BCMPZ (rs, offset, cmp, link, likely) -> `MIPSBCMPZ ((translate_out_ireg rs), (translate_out_simm16 offset), (translate_out_cmp cmp), (translate_out_bool link), (translate_out_bool likely)) -| J (offset) -> `MIPSJ (translate_out_imm26 offset) -| JAL (offset) -> `MIPSJAL (translate_out_imm26 offset) -| JR (rd) -> `MIPSJR (translate_out_ireg rd) -| JALR (rd, rs) -> `MIPSJALR (translate_out_ireg rd, translate_out_ireg rs) - diff --git a/mips/gen/shallow_types_to_herdtools_types.hgen b/mips/gen/shallow_types_to_herdtools_types.hgen deleted file mode 100644 index a02d83b7..00000000 --- a/mips/gen/shallow_types_to_herdtools_types.hgen +++ /dev/null @@ -1,39 +0,0 @@ -let translate_out_big_bit = Sail_values.unsigned - -let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst)) -let translate_out_signed_int inst bits = - let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in - if (i >= (1 lsl (bits - 1))) then - (i - (1 lsl bits)) else - i - -let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg)) - -let translate_out_imm26 imm = translate_out_int imm - -let translate_out_imm16 imm = translate_out_int imm -let translate_out_simm16 imm = translate_out_signed_int imm 16 - -let translate_out_imm5 imm = translate_out_int imm - -let translate_out_bool = function - | Sail_values.B1 -> true - | Sail_values.B0 -> false - | _ -> failwith "translate_out_bool Undef" - - -let translate_out_wordWidth = function - | Mips_embed_types.B2 -> MIPSByte - | Mips_embed_types.H -> MIPSHalf - | Mips_embed_types.W -> MIPSWord - | Mips_embed_types.D -> MIPSDouble - -let translate_out_cmp = function - | Mips_embed_types.EQ' -> MIPS_EQ (* equal *) - | Mips_embed_types.NE -> MIPS_NE (* not equal *) - | Mips_embed_types.GE -> MIPS_GE (* signed greater than or equal *) - | Mips_embed_types.GEU -> MIPS_GEU (* unsigned greater than or equal *) - | Mips_embed_types.GT' -> MIPS_GT (* signed strictly greater than *) - | Mips_embed_types.LE -> MIPS_LE (* signed less than or equal *) - | Mips_embed_types.LT' -> MIPS_LT (* signed strictly less than *) - | Mips_embed_types.LTU -> MIPS_LTU (* unsigned less than or qual *) diff --git a/mips/gen/token_types.hgen b/mips/gen/token_types.hgen deleted file mode 100644 index 170b42d3..00000000 --- a/mips/gen/token_types.hgen +++ /dev/null @@ -1,39 +0,0 @@ -type token_RTYPE = {txt : string; op : mipsRTypeOp } -type token_ITYPE = {txt : string; op : mipsITypeOp } -type token_ShiftI = {txt : string; op : mipsShiftIOp } -type token_ShiftV = {txt : string; op : mipsShiftVOp } -type token_MulDiv = {txt : string; op : mipsMulDivOp } -type token_MFHiLo = {txt : string; op : mipsMFHiLoOp } -type token_LUI = {txt : string } -type token_Load = {txt : string; width: mipsWordWidth; signed : bool; linked : bool} -type token_Store = {txt : string; width: mipsWordWidth; conditional : bool} -type token_LSLR = {txt : string; store : bool; double : bool; left: bool } (* Load/Store Left/Right *) -type token_SYNC = {txt : string} -type token_BEQ = {txt : string; ne : bool; likely : bool } -type token_BCMPZ = {txt : string; cmp : mipsCmp; likely : bool; link : bool } -type token_J = {txt : string} -type token_JAL = {txt : string} -type token_JR = {txt : string} -type token_JALR = {txt : string} -(* -(regno, imm16, Comparison) TRAPIMM - -(regno, regno) RDHWR -(regno, regno, Comparison) TRAPREG -(regno, regno, bit[3], bool) MFC0 -(regno, regno, bit[3], bool) MTC0 -(regno, regno, imm16, bool, bool) BEQ -TLBP -TLBR -TLBWI -TLBWR - -regregimm16 CACHE -regregimm16 PREF - -unit BREAK -unit ERET -unit HCF -unit SYSCALL -unit WAIT -*)
\ No newline at end of file diff --git a/mips/gen/tokens.hgen b/mips/gen/tokens.hgen deleted file mode 100644 index 937c6354..00000000 --- a/mips/gen/tokens.hgen +++ /dev/null @@ -1,17 +0,0 @@ -%token <MIPSHGenBase.token_RTYPE> RTYPE -%token <MIPSHGenBase.token_ITYPE> ITYPE -%token <MIPSHGenBase.token_ShiftI> SHIFTI -%token <MIPSHGenBase.token_ShiftV> SHIFTV -%token <MIPSHGenBase.token_MulDiv> MULDIV -%token <MIPSHGenBase.token_MFHiLo> MFHILO -%token <MIPSHGenBase.token_LUI> LUI -%token <MIPSHGenBase.token_Load> LOAD -%token <MIPSHGenBase.token_Store> STORE -%token <MIPSHGenBase.token_LSLR> LSLR -%token <MIPSHGenBase.token_SYNC> SYNC -%token <MIPSHGenBase.token_BEQ> BEQ -%token <MIPSHGenBase.token_BCMPZ> BCMPZ -%token <MIPSHGenBase.token_J> J -%token <MIPSHGenBase.token_JAL> JAL -%token <MIPSHGenBase.token_JR> JR -%token <MIPSHGenBase.token_JALR> JALR diff --git a/mips/gen/trans_sail.hgen b/mips/gen/trans_sail.hgen deleted file mode 100644 index e42d1b19..00000000 --- a/mips/gen/trans_sail.hgen +++ /dev/null @@ -1,122 +0,0 @@ -| `MIPSThreadStart -> - ("SYSCALL_THREAD_START", [], []) -| `MIPSStopFetching -> - ("ImplementationDefinedStopFetching", - [], - []) - -(* Note different argument order, which reflects difference - between instruction encoding and asm format *) -| `MIPSRType (op, rd, rs, rt) -> - (translate_rtype_op op, - [ - translate_reg "rs" rs; - translate_reg "rt" rt; - translate_reg "rd" rd; - ], - []) - -(* Note different argument order similar to above *) -| `MIPSIType (op, rt, rs, imm) -> - (translate_itype_op op, - [ - translate_reg "rs" rs; - translate_reg "rt" rt; - translate_imm16 "imm" imm; - ], - []) - -| `MIPSShiftI (op, rd, rt, sa) -> - (translate_shifti_op op, - [ - translate_reg "rt" rt; - translate_reg "rd" rd; - translate_imm5 "sa" sa; - ], - []) - -| `MIPSShiftV (op, rd, rt, rs) -> - (translate_shiftv_op op, - [ - translate_reg "rs" rs; - translate_reg "rt" rt; - translate_reg "rd" rd; - ], - []) - -| `MIPSMulDiv (op, rs, rt) -> - (translate_muldiv_op op, - [ - translate_reg "rs" rs; - translate_reg "rt" rt; - ], - []) - -| `MIPSMFHiLo (op, rs) -> - (translate_mfhilo_op op, - [ - translate_reg "rs" rs; - ], - []) -| `MIPSLUI (rt, imm) -> - ("LUI", - [ - translate_reg "rt" rt; - translate_imm16 "imm" imm; - ], - []) -| `MIPSLoad (width, signed, linked, base, rt, offset) -> - ("Load", - [ - translate_wordsize "width" width; - translate_bool "signed" signed; - translate_bool "linked" linked; - translate_reg "base" base; - translate_reg "rt" rt; - translate_imm16 "offset" offset; - ], - []) -| `MIPSStore (width, conditional, base, rt, offset) -> - ("Store", - [ - translate_wordsize "width" width; - translate_bool "conditional" conditional; - translate_reg "base" base; - translate_reg "rt" rt; - translate_imm16 "offset" offset; - ], - []) -| `MIPSLSLR (store, double, left, base, rt, offset) -> - (translate_lslr_op store double left, - [ - translate_reg "base" base; - translate_reg "rt" rt; - translate_imm16 "offset" offset; - ], - []) -| `MIPSSYNC -> ("SYNC", [], []) -| `MIPSBEQ (rs, rt, offset, ne, likely) -> - ("BEQ", - [translate_reg "rs" rs; - translate_reg "rt" rt; - translate_imm16 "offset" offset; - translate_bool "ne" ne; - translate_bool "likely" likely; - ], []) - -| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> - ("BCMPZ", - [translate_reg "rs" rs; - translate_imm16 "offset" offset; - translate_cmp "cmp" cmp; - translate_bool "link" link; - translate_bool "likely" likely; - ], []) -| `MIPSJ (offset) -> - ("J", [translate_imm26 "offset" offset;], []) -| `MIPSJAL (offset) -> - ("JAL", [translate_imm26 "offset" offset;], []) -| `MIPSJR(rd) -> - ("JR", [translate_reg "rd" rd;], []) -| `MIPSJALR(rd, rs) -> - ("JALR", [translate_reg "rd" rd; translate_reg "rs" rs;], []) diff --git a/mips/gen/types.hgen b/mips/gen/types.hgen deleted file mode 100644 index a1c61f4b..00000000 --- a/mips/gen/types.hgen +++ /dev/null @@ -1,209 +0,0 @@ -type mipsRTypeOp = -| MIPSROpADD -| MIPSROpADDU -| MIPSROpAND -| MIPSROpDADD -| MIPSROpDADDU -| MIPSROpDSUB -| MIPSROpDSUBU -| MIPSROpMOVN -| MIPSROpMOVZ -| MIPSROpMUL -| MIPSROpNOR -| MIPSROpOR -| MIPSROpSLT -| MIPSROpSLTU -| MIPSROpSUB -| MIPSROpSUBU -| MIPSROpXOR - -let pp_rtype_op = function -| MIPSROpADD -> "add" -| MIPSROpADDU -> "addu" -| MIPSROpAND -> "and" -| MIPSROpDADD -> "dadd" -| MIPSROpDADDU -> "daddu" -| MIPSROpDSUB -> "dsub" -| MIPSROpDSUBU -> "dsubu" -| MIPSROpMOVN -> "movn" -| MIPSROpMOVZ -> "movz" -| MIPSROpMUL -> "mul" -| MIPSROpNOR -> "nor" -| MIPSROpOR -> "or" -| MIPSROpSLT -> "slt" -| MIPSROpSLTU -> "sltu" -| MIPSROpSUB -> "sub" -| MIPSROpSUBU -> "subu" -| MIPSROpXOR -> "xor" - -type bit26 = int -type bit16 = int -type bit5 = int - -type mipsITypeOp = -| MIPSIOpADDI -| MIPSIOpADDIU -| MIPSIOpANDI -| MIPSIOpDADDI -| MIPSIOpDADDIU -| MIPSIOpORI -| MIPSIOpSLTI -| MIPSIOpSLTIU -| MIPSIOpXORI - -let pp_itype_op = function -| MIPSIOpADDI -> "addi" -| MIPSIOpADDIU -> "addiu" -| MIPSIOpANDI -> "andi" -| MIPSIOpDADDI -> "daddi" -| MIPSIOpDADDIU -> "daddiu" -| MIPSIOpORI -> "ori" -| MIPSIOpSLTI -> "slti" -| MIPSIOpSLTIU -> "sltiu" -| MIPSIOpXORI -> "xori" - -type mipsShiftIOp = -| MIPSDSLL -| MIPSDSLL32 -| MIPSDSRA -| MIPSDSRA32 -| MIPSDSRL -| MIPSDSRL32 -| MIPSSLL -| MIPSSRA -| MIPSSRL - -let pp_shifti_op = function -| MIPSDSLL -> "dsll" -| MIPSDSLL32 -> "dsll32" -| MIPSDSRA -> "dsra" -| MIPSDSRA32 -> "dsra32" -| MIPSDSRL -> "dsrl" -| MIPSDSRL32 -> "dsrl32" -| MIPSSLL -> "sll" -| MIPSSRA -> "sra" -| MIPSSRL -> "srl" - -type mipsShiftVOp = -| MIPSDSLLV -| MIPSDSRAV -| MIPSDSRLV -| MIPSSLLV -| MIPSSRAV -| MIPSSRLV - -let pp_shiftv_op = function -| MIPSDSLLV -> "dsllv" -| MIPSDSRAV -> "dsrav" -| MIPSDSRLV -> "dsrlv" -| MIPSSLLV -> "sllv" -| MIPSSRAV -> "srav" -| MIPSSRLV -> "srlv" - -type mipsMulDivOp = -| MIPSDDIV -| MIPSDDIVU -| MIPSDIV -| MIPSDIVU -| MIPSDMULT -| MIPSDMULTU -| MIPSMADD -| MIPSMADDU -| MIPSMSUB -| MIPSMSUBU -| MIPSMULT -| MIPSMULTU - -let pp_muldiv_op = function -| MIPSDDIV -> "ddiv" -| MIPSDDIVU -> "ddivu" -| MIPSDIV -> "div" -| MIPSDIVU -> "divu" -| MIPSDMULT -> "dmult" -| MIPSDMULTU -> "dmultu" -| MIPSMADD -> "madd" -| MIPSMADDU -> "maddu" -| MIPSMSUB -> "msub" -| MIPSMSUBU -> "msubu" -| MIPSMULT -> "mult" -| MIPSMULTU -> "multu" - -type mipsMFHiLoOp = -| MIPSMFHI -| MIPSMFLO -| MIPSMTHI -| MIPSMTLO - -let pp_mfhilo_op = function -| MIPSMFHI -> "mfhi" -| MIPSMFLO -> "mflo" -| MIPSMTHI -> "mthi" -| MIPSMTLO -> "mtlo" - -type mipsWordWidth = -| MIPSByte -| MIPSHalf -| MIPSWord -| MIPSDouble - -type mipsCmp = -| MIPS_EQ (* equal *) -| MIPS_NE (* not equal *) -| MIPS_GE (* signed greater than or equal *) -| MIPS_GEU (* unsigned greater than or equal *) -| MIPS_GT (* signed strictly greater than *) -| MIPS_LE (* signed less than or equal *) -| MIPS_LT (* signed strictly less than *) -| MIPS_LTU (* unsigned less than or qual *) - -let pp_load_op width signed linked = match (width, signed, linked) with - | (MIPSByte, true, false) -> "lb" - | (MIPSByte, false, false) -> "lbu" - | (MIPSHalf, true, false) -> "lh" - | (MIPSHalf, false, false) -> "lhu" - | (MIPSWord, true, false) -> "lw" - | (MIPSWord, false, false) -> "lwu" - | (MIPSDouble, false, false) -> "ld" - | (MIPSWord, true, true) -> "ll" - | (MIPSDouble, false, true) -> "lld" - | _ -> failwith "unexpected load op" - -let pp_store_op width conditional = match (width, conditional) with - | (MIPSByte, false) -> "sb" - | (MIPSHalf, false) -> "sh" - | (MIPSWord, false) -> "sw" - | (MIPSDouble, false) -> "sd" - | (MIPSWord, true) -> "sc" - | (MIPSDouble, true) -> "scd" - | _ -> failwith "unexpected store op" - -let pp_lslr_op store double left = match (store, double, left) with - | (false, false, true ) -> "lwl" - | (false, false, false) -> "lwr" - | (false, true , true ) -> "ldl" - | (false, true , false) -> "ldr" - | (true , false, true ) -> "swl" - | (true , false, false) -> "swr" - | (true , true , true ) -> "sdl" - | (true , true , false) -> "sdr" - -let pp_beq_op ne likely = match (ne, likely) with - | (false, false) -> "beq" - | (false, true) -> "beql" - | (true , false) -> "bne" - | (true , true) -> "bnel" - -let pp_bcmpz_op cmp link likely = match (cmp, likely, link) with -| (MIPS_LT, false , false ) -> "bltz" -| (MIPS_LT, false , true ) -> "bltzal" -| (MIPS_LT, true , false ) -> "bltzl" -| (MIPS_LT, true , true ) -> "bltzall" -| (MIPS_GE, false , false ) -> "bgez" -| (MIPS_GE, false , true ) -> "bgezal" -| (MIPS_GE, true , false ) -> "bgezl" -| (MIPS_GE, true , true ) -> "bgezall" -| (MIPS_GT, false , false ) -> "bgtz" -| (MIPS_GT, true , false ) -> "bgtzl" -| (MIPS_LE, false , false ) -> "blez" -| (MIPS_LE, true , false ) -> "blezl" -| _ -> failwith "unknown bcmpz instruction" diff --git a/mips/gen/types_sail_trans_out.hgen b/mips/gen/types_sail_trans_out.hgen deleted file mode 100644 index ebd31fcb..00000000 --- a/mips/gen/types_sail_trans_out.hgen +++ /dev/null @@ -1,47 +0,0 @@ -let translate_out_big_bit = function - | (name, Bvector _, bits) -> IInt.integer_of_bit_list bits - | _ -> assert false - -let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst)) -let translate_out_signed_int inst bits = - let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in - if (i >= (1 lsl (bits - 1))) then - (i - (1 lsl bits)) else - i - -let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg)) - -let translate_out_imm26 imm = translate_out_int imm - -let translate_out_imm16 imm = translate_out_int imm -let translate_out_simm16 imm = translate_out_signed_int imm 16 - -let translate_out_imm5 imm = translate_out_int imm - -let translate_out_bool = function - | (name, Bit, [Bitc_one]) -> true - | (name, Bit, [Bitc_zero]) -> false - | _ -> assert false - -let translate_out_enum (name,_,bits) = - Nat_big_num.to_int (IInt.integer_of_bit_list bits) - -let translate_out_wordWidth inst = - match translate_out_enum inst with - | 0 -> MIPSByte - | 1 -> MIPSHalf - | 2 -> MIPSWord - | 3 -> MIPSDouble - | _ -> failwith "Unknown wordWidth in sail translate out" - -let translate_out_cmp inst = - match translate_out_enum inst with - | 0 -> MIPS_EQ (* equal *) - | 1 -> MIPS_NE (* not equal *) - | 2 -> MIPS_GE (* signed greater than or equal *) - | 3 -> MIPS_GEU (* unsigned greater than or equal *) - | 4 -> MIPS_GT (* signed strictly greater than *) - | 5 -> MIPS_LE (* signed less than or equal *) - | 6 -> MIPS_LT (* signed strictly less than *) - | 7 -> MIPS_LTU (* unsigned less than or qual *) - | _ -> failwith "Unknown mipsCmp in sail translate out" diff --git a/mips/gen/types_trans_sail.hgen b/mips/gen/types_trans_sail.hgen deleted file mode 100644 index 63880ae9..00000000 --- a/mips/gen/types_trans_sail.hgen +++ /dev/null @@ -1,44 +0,0 @@ -let translate_rtype_op op = uppercase (pp_rtype_op op) -let translate_itype_op op = uppercase (pp_itype_op op) -let translate_shifti_op op = uppercase (pp_shifti_op op) -let translate_shiftv_op op = uppercase (pp_shiftv_op op) -let translate_muldiv_op op = uppercase (pp_muldiv_op op) -let translate_mfhilo_op op = uppercase (pp_mfhilo_op op) -let translate_load_op width signed linked = uppercase (pp_load_op width signed linked) -let translate_store_op width conditional = uppercase (pp_store_op width conditional) -let translate_lslr_op store double left = uppercase (pp_lslr_op store double left) -let translate_beq_op ne likely = uppercase (pp_beq_op ne likely) -let translate_bcmpz_op cmp link likely = uppercase (pp_bcmpz_op cmp link likely) - -let translate_reg name value = - (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value))) -let translate_imm26 name value = - (name, Bvector (Some 26), bit_list_of_integer 26 (Nat_big_num.of_int value)) -let translate_imm16 name value = - (name, Bvector (Some 16), bit_list_of_integer 16 (Nat_big_num.of_int value)) -let translate_imm5 name value = - (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value)) -let translate_bool name value = - (name, Bit, [if value then Bitc_one else Bitc_zero]) -let translate_enum enum_values name value = - let rec bit_count n = - if n = 0 then 0 - else 1 + (bit_count (n lsr 1)) in - let rec find_index element = function - | h::tail -> if h = element then 0 else 1 + (find_index element tail) - | _ -> failwith "translate_enum could not find value" - in - let size = bit_count (List.length enum_values) in - let index = find_index value enum_values in - (name, Range0 (Some size), IInt.bit_list_of_integer size (Nat_big_num.of_int index)) -let translate_wordsize = translate_enum [MIPSByte; MIPSHalf; MIPSWord; MIPSDouble] -let translate_cmp = translate_enum [ -MIPS_EQ ;(* equal *) -MIPS_NE ;(* not equal *) -MIPS_GE ;(* signed greater than or equal *) -MIPS_GEU ;(* unsigned greater than or equal *) -MIPS_GT ;(* signed strictly greater than *) -MIPS_LE ;(* signed less than or equal *) -MIPS_LT ;(* signed strictly less than *) -MIPS_LTU ;(* unsigned less than or qual *) -]
\ No newline at end of file diff --git a/mips/main.sail b/mips/main.sail deleted file mode 100644 index 8fc48f9a..00000000 --- a/mips/main.sail +++ /dev/null @@ -1,97 +0,0 @@ - -val cycle_limit_reached = { c: "cycle_limit_reached" } : unit -> bool - -function cycle_limit_reached() = false - -register instCount : int - -val fetch_and_execute : unit -> bool effect {barr, eamem, escape, rmem, rreg, wmv, wreg, undef, wmvt, rmemt} -function fetch_and_execute () = { - PC = nextPC; - inBranchDelay = branchPending; - branchPending = 0b0; - nextPC = if inBranchDelay then delayedPC else PC + 4; - cp2_next_pc(); - instCount = instCount + 1; - if UART_WRITTEN then { - putchar(unsigned(UART_WDATA)); - UART_WRITTEN = 0b0; - }; - /* the following skips are required on mips to fake the tag effects otherwise type checker complains */ - skip_rmemt(); - skip_wmvt(); - /* prerr_bits("PC: ", PC); */ - loop_again = true; - 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."); - loop_again = false - }, - Some(ast) => execute(ast), - None() => { print("Decode failed"); loop_again=false } /* Never expect this -- unknown instruction should actually result in reserved instruction ISA-level exception (see mips_ri.sail). */ - } - } catch { - ISAException() => () /*prerr_endline("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.) . */ - }; - loop_again & not (cycle_limit_reached()); -} - -val elf_entry = { - ocaml: "Elf_loader.elf_entry", - lem: "elf_entry", - c: "elf_entry" -} : unit -> int - -val init_registers : bits(64) -> unit effect {wreg} - -function init_registers (initialPC) = { - init_cp0_state(); - init_cp2_state(); - nextPC = initialPC; -} - -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))))))); - } -} - -val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt} - -function main () = { - init_registers(to_bits(64, elf_entry())); - startTime = get_time_ns(); - while (fetch_and_execute()) do { - /* uncomment to print IPS every 10M instructions (~10s) - if (instCount == 10000000) then { - endTime = get_time_ns(); - elapsed = endTime - startTime; - inst_1e9 = instCount * 1000000000; - ips = inst_1e9 / elapsed; - print_int("*IPS*: ", ips); - startTime = get_time_ns(); - instCount = 0; - };*/ - (); - }; - - endTime = get_time_ns(); - elapsed = endTime - startTime; - inst_1e9 = instCount * 1000000000; - ips = inst_1e9 / elapsed; - dump_mips_state (); - dump_cp2_state (); - print_int("Executed instructions: ", instCount); - print_int("Nanoseconds elapsed: ", elapsed); - print_int("Instructions per second: ", ips); -} diff --git a/mips/mips_ast_decl.sail b/mips/mips_ast_decl.sail deleted file mode 100644 index e39bc270..00000000 --- a/mips/mips_ast_decl.sail +++ /dev/null @@ -1,44 +0,0 @@ -/*========================================================================*/ -/* */ -/* 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 deleted file mode 100644 index c7477a50..00000000 --- a/mips/mips_epilogue.sail +++ /dev/null @@ -1,42 +0,0 @@ -/*========================================================================*/ -/* */ -/* 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 deleted file mode 100644 index 4edb0066..00000000 --- a/mips/mips_extras.lem +++ /dev/null @@ -1,128 +0,0 @@ -open import Pervasives -open import Pervasives_extra -open import Sail2_instr_kinds -open import Sail2_values -open import Sail2_operators -open import Sail2_prompt_monad -open import Sail2_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 - -val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e -let read_tag_bool addr = - read_tag addr >>= fun t -> - maybe_fail "read_tag_bool" (bool_of_bitU t) - -val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e -let write_tag_bool addr t = write_tag addr (bitU_of_bool t) >>= fun _ -> return () - -let MEMr_tag addr size = - read_mem Read_plain addr size >>= fun v -> - read_tag_bool addr >>= fun t -> - return (t, v) - -let MEMr_tag_reserve addr size = - read_mem Read_plain addr size >>= fun v -> - read_tag_bool addr >>= fun t -> - return (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 addr size t v = write_mem_val v >>= fun _ -> write_tag_bool addr t >>= fun _ -> return () -let MEMval_tag_conditional addr size t v = write_mem_val v >>= fun b -> write_tag_bool addr 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 bs = bools_of_int (hi + 1) n in - subrange_list false bs hi lo - -val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -let get_slice_int len n lo = of_bools (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 string_of_int = show - -let shift_bits_left v n = - let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftl_bv v n)) in - maybe_fail "shift_bits_left" r -let shift_bits_right v n = - let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftr_bv v n)) in - maybe_fail "shift_bits_right" r -let shift_bits_right_arith v n = - let r = Maybe.bind (unsigned n) (fun n -> of_bits (arith_shiftr_bv v n)) in - maybe_fail "shift_bits_right_arith" r - -(* Use constants for undefined values for now *) -let undefined_string () = return "" -let undefined_unit () = return () -let undefined_int () = return (0:ii) -val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e -let undefined_vector len u = return (repeat [u] len) -val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e -let undefined_bitvector len = return (of_bools (repeat [false] len)) -val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e -let undefined_bits = undefined_bitvector -let undefined_bit () = return B0 -let undefined_real () = return (realFromFrac 0 1) -let undefined_range i j = return i -let undefined_atom i = return i -let undefined_nat () = return (0:ii) - -let skip () = return () - -val elf_entry : unit -> integer -let elf_entry () = 0 -declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry` - -let print_bits msg bs = print_endline (msg ^ (string_of_bv bs)) -let prerr_bits msg bs = prerr_endline (msg ^ (string_of_bv bs)) - -val prerr_string : string -> unit -let prerr_string _ = () -declare ocaml target_rep function prerr_string = `Pervasives.prerr_string` - -val get_time_ns : unit -> integer -let get_time_ns () = 0 -declare ocaml target_rep function get_time_ns = `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))` - -val cycle_count : unit -> unit -let cycle_count _ = () - -let inline eq_bit = eq diff --git a/mips/mips_extras.v b/mips/mips_extras.v deleted file mode 100644 index 83f39079..00000000 --- a/mips/mips_extras.v +++ /dev/null @@ -1,179 +0,0 @@ -Require Import Sail2_instr_kinds. -Require Import Sail2_values. -Require Import Sail2_operators_mwords. -Require Import Sail2_prompt_monad. -Require Import Sail2_prompt. -Require Import String. -Require Import List. -Import List.ListNotations. -(* -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 -*) -Definition MEMr {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (mword b) e := read_mem Read_plain addr size. -Definition MEMr_reserve {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (mword b) e := read_mem Read_reserve addr size. - -(*val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e*) -Definition read_tag_bool {regval a e} (addr : mword a) : monad regval bool e := - read_tag addr >>= fun t => - maybe_fail "read_tag_bool" (bool_of_bitU t). - -(*val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e*) -Definition write_tag_bool {regval a e} (addr : mword a) t : monad regval unit e := - write_tag addr (bitU_of_bool t) >>= fun _ => returnm tt. - -Definition MEMr_tag {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (bool * mword b) e := - read_mem Read_plain addr size >>= fun v => - read_tag_bool addr >>= fun t => - returnm (t, v). - -Definition MEMr_tag_reserve {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (bool * mword b) e := - read_mem Read_plain addr size >>= fun v => - read_tag_bool addr >>= fun t => - returnm (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 -*) -Definition MEMea {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_plain addr size. -Definition MEMea_conditional {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_conditional addr size. - -Definition MEMea_tag {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_plain addr size. -Definition MEMea_tag_conditional {regval a e} (addr : mword a) size : monad regval unit e := 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 -*) -Definition MEMval {regval a b e} (_ : mword a) (size : Z) (v : mword b) : monad regval unit e := write_mem_val v >>= fun _ => returnm tt. -Definition MEMval_conditional {regval a b e} (_ : mword a) (size : Z) (v : mword b) : monad regval bool e := write_mem_val v >>= fun b => returnm (if b then true else false). -Definition MEMval_tag {regval a b e} (addr : mword a) (size : Z) t (v : mword b) : monad regval unit e := write_mem_val v >>= fun _ => write_tag_bool addr t >>= fun _ => returnm tt. -Definition MEMval_tag_conditional {regval a b e} (addr : mword a) (size : Z) t (v : mword b) : monad regval bool e := write_mem_val v >>= fun b => write_tag_bool addr t >>= fun _ => returnm (if b then true else false). - -(*val MEM_sync : forall 'regval 'e. unit -> monad 'regval unit 'e*) - -Definition MEM_sync {regval e} (_:unit) : monad regval unit e := barrier Barrier_MIPS_SYNC. - -(* Some wrappers copied from aarch64_extras *) -(* TODO: Harmonise into a common library *) -(* -Definition get_slice_int_bl len n lo := - (* TODO: Is this the intended behaviour? *) - let hi := lo + len - 1 in - let bs := bools_of_int (hi + 1) n in - subrange_list false bs hi lo - -val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -Definition get_slice_int len n lo := of_bools (get_slice_int_bl len n lo) -*) -Definition write_ram {rv e} m size (_ : mword m) (addr : mword m) (data : mword (8 * size)) : monad rv unit e := - MEMea addr size >> - MEMval addr size data. - -Definition read_ram {rv e} m size `{ArithFact (size >= 0)} (_ : mword m) (addr : mword m) : monad rv (mword (8 * size)) e := MEMr addr size. -(* -Definition string_of_bits bs := string_of_bv (bits_of bs). -Definition string_of_int := show - -Definition _sign_extend bits len := maybe_failwith (of_bits (exts_bv len bits)) -Definition _zero_extend bits len := maybe_failwith (of_bits (extz_bv len bits)) -*) -Definition shift_bits_left {rv e a b} (v : mword a) (n : mword b) : monad rv (mword a) e := - maybe_fail "shift_bits_left" (unsigned n) >>= fun n => - returnm (shiftl v n). - -Definition shift_bits_right {rv e a b} (v : mword a) (n : mword b) : monad rv (mword a) e := - maybe_fail "shift_bits_right" (unsigned n) >>= fun n => - returnm (shiftr v n). - -Definition shift_bits_right_arith {rv e a b} (v : mword a) (n : mword b) : monad rv (mword a) e := - maybe_fail "shift_bits_right" (unsigned n) >>= fun n => - returnm (arith_shiftr v n). - -(* Use constants for undefined values for now *) -Definition internal_pick {rv a e} (vs : list a) : monad rv a e := -match vs with -| (h::_) => returnm h -| _ => Fail "empty list in internal_pick" -end. -Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%string. -Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt. -Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii). -(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*) -Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >= 0)} : monad rv (vec a len) e := returnm (vec_init u len). -(*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) -Definition undefined_bitvector {rv e} len `{ArithFact (len >= 0)} : monad rv (mword len) e := returnm (mword_of_int 0). -(*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) -Definition undefined_bits {rv e} := @undefined_bitvector rv e. -Definition undefined_bit {rv e} (_:unit) : monad rv bitU e := returnm BU. -(*Definition undefined_real {rv e} (_:unit) : monad rv real e := returnm (realFromFrac 0 1).*) -Definition undefined_range {rv e} i j `{ArithFact (i <= j)} : monad rv {z : Z & ArithFact (i <= z /\ z <= j)} e := returnm (build_ex i). -Definition undefined_atom {rv e} i : monad rv Z e := returnm i. -Definition undefined_nat {rv e} (_:unit) : monad rv Z e := returnm (0:ii). - -Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt. - -(*val elf_entry : unit -> integer*) -Definition elf_entry (_:unit) : Z := 0. -(*declare ocaml target_rep function elf_entry := `Elf_loader.elf_entry`*) - -(*Definition print_bits msg bs := prerr_endline (msg ^ (string_of_bits bs)) - -val get_time_ns : unit -> integer*) -Definition get_time_ns (_:unit) : Z := 0. -(*declare ocaml target_rep function get_time_ns := `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))`*) - -Definition eq_bit (x : bitU) (y : bitU) : bool := - match x, y with - | B0, B0 => true - | B1, B1 => true - | BU, BU => true - | _,_ => false - end. - -Require Import Zeuclid. -Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0 <= z <= n-1)}. -refine (existT _ (ZEuclid.modulo m n) _). -constructor. -destruct H. -assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. } -rewrite <- H at 3. -lapply (ZEuclid.mod_always_pos m n); omega. -Qed. - -(* Override the more general version *) - -Definition mults_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mults_vec l r. -Definition mult_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mult_vec l r. - - -Definition print_endline (_:string) : unit := tt. -Definition prerr_endline (_:string) : unit := tt. -Definition prerr_string (_:string) : unit := tt. -Definition putchar {T} (_:T) : unit := tt. -Require DecimalString. -Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). - -Lemma __MIPS_read_lemma : forall width, 8 * width = 8 * (8 * width ÷ 8). -intros. -rewrite Z.mul_comm. -rewrite Z.quot_mul; auto with zarith. -Qed. -Hint Resolve __MIPS_read_lemma : sail. - -Lemma MEMr_wrapper_lemma : forall size : Z, 8 * size = 8 * (8 * (8 * size ÷ 8) ÷ 8). -intros. -rewrite Z.mul_comm. -rewrite Z.quot_mul; auto with zarith. -rewrite Z.mul_comm with (m := size). -rewrite Z.quot_mul; auto with zarith. -Qed. -Hint Resolve MEMr_wrapper_lemma : sail. - diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail deleted file mode 100644 index 63c380de..00000000 --- a/mips/mips_insts.sail +++ /dev/null @@ -1,1682 +0,0 @@ -/*========================================================================*/ -/* */ -/* 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) + sign_extend(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) = sign_extend(rGPR(rs)) + sign_extend(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) = sign_extend(rGPR(rs)) + sign_extend(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) = sign_extend(opA[31 .. 0]) + sign_extend(opB[31 .. 0])in - if sum33[32] != sum33[31] then - (SignalException(Ov)) - else - wGPR(rd) = sign_extend(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) = sign_extend(opA[31 .. 0]) + sign_extend(imm) in - if sum33[32] != sum33[31] then - (SignalException(Ov)) - else - wGPR(rt) = sign_extend(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) = sign_extend(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) = sign_extend((opA[31 .. 0]) + sign_extend(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) = sign_extend(rGPR(rs)) - sign_extend(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) = sign_extend(opA[31..0]) - sign_extend(opB[31..0]) in - if temp33[32] != temp33[31] then - (SignalException(Ov)) - else - wGPR(rd) = sign_extend(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) = sign_extend(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) & zero_extend(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) | zero_extend(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) ^ zero_extend(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) = sign_extend(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) = sign_extend(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) = sign_extend(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) = sign_extend(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) = sign_extend(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) = sign_extend(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) = sign_extend(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) = zero_extend(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) = zero_extend(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) = zero_extend(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) = sign_extend(imm) in /* NB defined to sign extend here even though comparison is unsigned! */ - wGPR(rt) = zero_extend(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) = sign_extend((rsVal[31..0]) *_s (rtVal[31..0])); - wGPR(rd) = if (NotWordVal(rsVal) | NotWordVal(rtVal)) then - undefined - else - sign_extend(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 = sign_extend(result[63..32]); - LO = sign_extend(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 = sign_extend(result[63..32]); - LO = sign_extend(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 = sign_extend(result[63..32]); - LO = sign_extend(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 = sign_extend(result[63..32]); - LO = sign_extend(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 = sign_extend(result[63..32]); - LO = sign_extend(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 = sign_extend(result[63..32]); - LO = sign_extend(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 = sign_extend(r); - LO = sign_extend(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 = sign_extend(r); - LO = sign_extend(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)) = - { - execute_branch((PC + 4)[63..28] @ offset @ 0b00); - } - -/* 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)) = - { - execute_branch((PC + 4)[63..28] @ offset @ 0b00); - 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)) = - { - execute_branch(rGPR(rs)); - } - -/* 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)) = - { - execute_branch(rGPR(rs)); - 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) = (sign_extend(imm @ 0b00) + 4) in - execute_branch(PC + offset); - } - 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, zero_extend(0b0)); - if (condition) then - { - let offset : bits(64) = (sign_extend(imm @ 0b00) + 4) in - execute_branch(PC + offset); - } - else if (likely) then - { - nextPC = PC + 8 /* skip branch delay */ - }; - if (link) then - wGPR(0b11111) = linkVal - } - -/**************************************************************************************/ -/* SYSCALL/BREAK/WAIT/Trap */ -/**************************************************************************************/ - -/* $include mips_rmem.sail */ - -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) = sign_extend(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 - sign_extend(memResult) - else - zero_extend(memResult) -} - -function clause execute (Load(width, sign, linked, base, rt, offset)) = - { - vAddr : bits(64) = addrWrapper(sign_extend(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 { - W => extendLoad(MEMr_reserve_wrapper(pAddr, 4), sign), - D => extendLoad(MEMr_reserve_wrapper(pAddr, 8), sign), - _ => throw(Error_internal_error()) /* there is no llbc or llhc */ - } - } - 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(sign_extend(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 - { - W => MEMw_conditional_wrapper(pAddr, 4, rt_val[31..0]), - D => MEMw_conditional_wrapper(pAddr, 8, rt_val), - _ => throw(Error_internal_error()) /* there is no sbc or shc */ - } else false; - wGPR(rt) = zero_extend(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)) = - { - vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, WL); - 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) = sign_extend(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)) = - { - vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, WR); - 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) = sign_extend(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)) = - { - vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, WL); - 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)) = - { - vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, WR); - 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)) = - { - vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, DL); - let pAddr = TLBTranslate(vAddr, LoadData) 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)) = - { - vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, DR); - let pAddr = TLBTranslate(vAddr, LoadData) 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)) = - { - vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, DL); - 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)) = - { - vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, DR); - 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) = zero_extend(TLBIndex) in - (0x00000000 @ TLBProbe @ idx), /* 0, TLB Index */ - (0b00001,0b000) => zero_extend(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 */ - (0b00100,0b010) => CP0UserLocal, - (0b00101,0b000) => zero_extend(TLBPageMask @ 0x000), /* 5, TLB PageMask */ - (0b00110,0b000) => zero_extend(TLBWired), /* 6, TLB Wired */ - (0b00111,0b000) => zero_extend(CP0HWREna), /* 7, HWREna */ - (0b01000,0b000) => CP0BadVAddr, /* 8, BadVAddr reg */ - (0b01000,0b001) => zero_extend(0b0), /* 8, BadInstr reg XXX TODO */ - (0b01001,0b000) => zero_extend(CP0Count), /* 9, Count reg */ - (0b01010,0b000) => TLBEntryHi.bits(),/* 10, TLB EntryHi */ - (0b01011,0b000) => zero_extend(CP0Compare), /* 11, Compare reg */ - (0b01100,0b000) => zero_extend(CP0Status.bits()), /* 12, Status reg */ - (0b01101,0b000) => zero_extend(CP0Cause.bits()), /* 13, Cause reg */ - (0b01110,0b000) => CP0EPC, /* 14, EPC */ - (0b01111,0b000) => zero_extend(0x00000400), /* 15, sel 0: PrID processor ID */ - (0b01111,0b110) => zero_extend(0b0), /* 15, sel 6: CHERI core ID */ - (0b01111,0b111) => zero_extend(0b0), /* 15, sel 7: CHERI thread ID */ - (0b10000,0b000) => zero_extend(0b1 /* M */ /* 16, sel 0: Config0 */ - @ 0b000000000000000 /* Impl */ - @ 0b1 /* BE */ - @ 0b10 /* AT */ - @ 0b000 /* AR */ - @ 0b001 /* MT standard TLB */ - @ 0b0000 /* zero */ - @ CP0ConfigK0), - (0b10000,0b001) => zero_extend( /* 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) => zero_extend( /* 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) => zero_extend(0b0), /* 18, WatchLo */ - (0b10011,0b000) => zero_extend(0b0), /* 19, WatchHi */ - (0b10100,0b000) => TLBXContext.bits(), /* 20, XContext */ - (0b11110,0b000) => CP0ErrorEPC, /* 30, ErrorEPC */ - _ => (SignalException(ResI)) - } in - wGPR(rt) = if (double) then result else sign_extend(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) => CP0ConfigK0 = reg_val[2..0], /* 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 => zero_extend([bitzero]), /* CPUNum */ - 0b00001 => zero_extend([bitzero]), /* SYNCI_step */ - 0b00010 => zero_extend(CP0Count), /* Count */ - 0b00011 => zero_extend([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 deleted file mode 100644 index 6babfd19..00000000 --- a/mips/mips_prelude.sail +++ /dev/null @@ -1,649 +0,0 @@ -/*========================================================================*/ -/* */ -/* 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) -register CP0ConfigK0 : bits(3) - -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 */ - -val execute_branch : bits(64) -> unit effect {wreg} -function execute_branch(pc) = { - delayedPC = pc; - branchPending = 0b1; -} - -/* 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 { - /*prerr_string(string_of_int(i)); - prerr_bits(" <- ", v);*/ - GPR[i] = v; - }; -} - -val MEMr = {lem: "MEMr"} : forall 'n, 'n >= 0. - ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem } -val MEMr_reserve = {lem: "MEMr_reserve"} : forall 'n, 'n >= 0. - ( 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 + sign_extend(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} - -val int_of_AccessLevel : AccessLevel -> {|0, 1, 2|} effect pure -function int_of_AccessLevel level = - match level { - User => 0, - Supervisor => 1, - Kernel => 2 - } - -/*! -Returns whether the first AccessLevel is sufficient to grant access at the second, required, access level. - */ -val grantsAccess : (AccessLevel, AccessLevel) -> bool -function grantsAccess (currentLevel, requiredLevel) = - int_of_AccessLevel(currentLevel) >= int_of_AccessLevel(requiredLevel) - -/*! -Returns the current effective access level determined by accessing the relevant parts of the MIPS status register. - */ -val getAccessLevel : unit -> AccessLevel effect {rreg} -function getAccessLevel() = - 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} -enum WordTypeUnaligned = { WL, WR, DL, DR } - -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, rreg, wreg} -function MEMr_wrapper (addr, size) = - if (addr == 0x000000007f000000) then - { - let rvalid = UART_RVALID in - { - UART_RVALID = [bitzero]; - mask(0x00000000 @ UART_RDATA @ rvalid @ 0b0000000 @ 0x0000) - } - } - 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 deleted file mode 100644 index 0c77fb9f..00000000 --- a/mips/mips_regfp.sail +++ /dev/null @@ -1,455 +0,0 @@ -/*========================================================================*/ -/* */ -/* 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) = (sign_extend(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) = (sign_extend(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 deleted file mode 100644 index edce0657..00000000 --- a/mips/mips_ri.sail +++ /dev/null @@ -1,42 +0,0 @@ -/*========================================================================*/ -/* */ -/* 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_rmem.sail b/mips/mips_rmem.sail deleted file mode 100644 index 1bc47337..00000000 --- a/mips/mips_rmem.sail +++ /dev/null @@ -1,15 +0,0 @@ -/* These instructions are used for RMEM integration only */ - -/* 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()) = () - diff --git a/mips/mips_tlb.sail b/mips/mips_tlb.sail deleted file mode 100644 index a8bb819e..00000000 --- a/mips/mips_tlb.sail +++ /dev/null @@ -1,140 +0,0 @@ -/*========================================================================*/ -/* */ -/* 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) = ~(zero_extend(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) = zero_extend(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) - } -} - -/* 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 not(grantsAccess(currentAccessLevel, 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 deleted file mode 100644 index c42e4764..00000000 --- a/mips/mips_tlb_stub.sail +++ /dev/null @@ -1,48 +0,0 @@ -/*========================================================================*/ -/* */ -/* 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 deleted file mode 100644 index 43e759b9..00000000 --- a/mips/mips_wrappers.sail +++ /dev/null @@ -1,90 +0,0 @@ -/*========================================================================*/ -/* */ -/* 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 - -val addrWrapperUnaligned : (bits(64), MemAccessType, WordTypeUnaligned) -> bits(64) -function addrWrapperUnaligned(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 deleted file mode 100644 index 094f82e8..00000000 --- a/mips/prelude.sail +++ /dev/null @@ -1,223 +0,0 @@ -default Order dec - -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 - -/* this is here because if we don't have it before including vector_dec - we get infinite loops caused by interaction with bool/bit casts */ -val eq_bit2 = "eq_bit" : (bit, bit) -> bool -overload operator == = {eq_bit2} - -$include <smt.sail> -$include <flow.sail> -$include <arith.sail> -$include <option.sail> -$include <vector_dec.sail> - -val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic_eq", _:"eq_anything"} : forall ('a : Type). ('a, 'a) -> bool -overload operator == = {eq_anything} - -val not_vec = {c:"not_bits", _:"not_vec"} : forall 'n. bits('n) -> bits('n) - -overload ~ = {not_bool, not_vec} - -val not = {coq:"negb", _:"not"} : bool -> bool - -val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool -function neq_vec (x, y) = not_bool(eq_bits(x, y)) - -val neq_anything = {lem: "neq", coq: "generic_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 and_bits = {c:"and_bits", _: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) - -overload operator & = {and_bool, and_bits} - -val or_bits = {c: "or_bits", _: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) - -overload operator | = {or_bool, or_bits} - -val cast cast_unit_vec : bit -> bits(1) - -function cast_unit_vec b = match b { - bitzero => 0b0, - _ => 0b1 -} - -val print = "print_endline" : string -> unit - -val "prerr_endline" : string -> unit - -val "prerr_string" : string -> unit - -val putchar = {c:"sail_putchar", _:"putchar"} : int -> unit - -val concat_str = {lem: "stringAppend", coq: "String.append", _: "concat_str"} : (string, string) -> string - -val string_of_int = "string_of_int" : int -> string -/* Unused? -val DecStr : int -> string - -val HexStr : int -> string -*/ -val BitStr = "string_of_bits" : forall 'n. bits('n) -> string - -val xor_vec = {c: "xor_bits" , _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) - -val int_power = {ocaml: "int_power", lem: "pow", coq: "Z.pow"} : (int, int) -> int - -overload operator ^ = {xor_vec, int_power} - -val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range", c: "add_int"} : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -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) - -overload operator + = {add_range, add_int, add_vec, add_vec_int} - -val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val sub_vec = {c : "sub_bits", _:"sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) - -val sub_vec_int = {c:"sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n) - -val negate_range = {ocaml: "minus_big_int", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) - -overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int} - -overload negate = {negate_range, negate_int} - -overload operator * = {mult_int} - -val quotient_nat = {ocaml: "quotient", lem: "integerDiv", coq: "Z.div"} : (nat, nat) -> nat - -val quotient = {ocaml: "quotient", lem: "integerDiv", coq: "Z.mod"} : (int, int) -> int - -overload operator / = {quotient_nat, quotient} - -val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", coq: "Z.quot", _ : "tdiv_int"} : (int, int) -> int -val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", coq: "Z.rem", _ : "tmod_int"} : (int, int) -> int - -val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) - -overload operator % = {modulus} - -val min_nat = {lem: "min", coq: "Z.min", _: "min_int"} : (nat, nat) -> nat - -val min_int = {lem: "min", coq: "Z.min", _: "min_int"} : (int, int) -> int - -val max_nat = {lem: "max", coq: "Z.max", _: "max_int"} : (nat, nat) -> nat - -val max_int = {lem: "max", coq: "Z.max", _: "max_int"} : (int, int) -> int - -val min_atom = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : 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", coq: "max_atom", c:"max_int"} : 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)) -> bool effect {wmv} - -val __MIPS_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} -function __MIPS_write (addr, width, data) = let _ = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) in () - -val __ReadRAM = "read_ram" : forall 'n 'm, 'n >= 0. - (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} - -val __MIPS_read : forall 'n, 'n >= 0. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem} -function __MIPS_read (addr, width) = __ReadRAM(64, width, 0x0000_0000_0000_0000, addr) - -infix 8 ^^ -val operator ^^ = {lem: "replicate_bits"} : forall 'n 'm, 'm >= 0 . (bits('n), atom('m)) -> bits('n * 'm) -function operator ^^ (bs, n) = replicate_bits (bs, n) - -val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) - -union exception = { - ISAException : unit, - Error_not_implemented : string, - Error_misaligned_access : unit, - Error_EBREAK : unit, - Error_internal_error : unit -} - -val mips_sign_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) -val mips_zero_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) - -function mips_sign_extend v = sail_sign_extend(v, sizeof('m)) -function mips_zero_extend v = sail_zero_extend(v, sizeof('m)) - -overload sign_extend = {mips_sign_extend} -overload zero_extend = {mips_zero_extend} - -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 : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool -val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool -val operator <_u : forall 'n, 'n >= 0. (bits('n), bits('n)) -> bool -val operator >=_u : forall 'n, 'n >= 0. (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 b = match b { - bitone => true, - _ => 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) effect {undef} -val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef} - -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) effect {undef} - -infix 7 *_s -val operator *_s = "mults_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) - -/*! -\function{to\_bits} converts an integer to a bit vector of given length. If the integer is negative a twos-complement representation is used. If the integer is too large (or too negative) to fit in the requested length then it is truncated to the least significant bits. -*/ -val to_bits : forall 'l, 'l >= 0 .(atom('l), int) -> bits('l) -function to_bits (l, n) = get_slice_int(l, n, 0) - -val mask : forall 'm 'n , 'm >= 'n > 0 . bits('m) -> bits('n) -function mask bs = bs['n - 1 .. 0] - -val "get_time_ns" : unit -> int diff --git a/mips/sim.dts b/mips/sim.dts deleted file mode 100644 index d1720441..00000000 --- a/mips/sim.dts +++ /dev/null @@ -1,79 +0,0 @@ -/dts-v1/; -/ { - model = "SRI/Cambridge BERI simulation"; - compatible = "sri-cambridge,beri-sim"; - #address-cells = <1>; - #size-cells = <1>; - sri-cambridge,build-time = <0 1527247299>; - sri-cambridge,build-host = "TODO"; - sri-cambridge,build-path = "TODO"; - sri-cambridge,build-source-path = "TODO"; - sri-cambridge,build-source-revision = "TODO"; - - cpus { - #address-cells = <1>; - #size-cells = <1>; - status = "disabled"; - enable-method = "spin-table"; - - cpu@0 { - device-type = "cpu"; - compatible = "sri-cambridge,beri"; - - reg = <0 1>; - status = "okay"; - }; - }; - - cpuintc: cpuintc@0 { - #address-cells = <0>; - #interrupt-cells = <1>; - interrupt-controller; - compatible = "mti,cpu-interrupt-controller"; - }; - /* THE PIC IS A LIE! - FreeBSD panics if there isn't one even though - we don't actually need one if we put the UART - in polled mode. We can get away with just pointing - FreeBSD at some plain memory and telling it that - is a PIC... */ - beripic0: beripic@7f804000 { - compatible = "sri-cambridge,beri-pic"; - interrupt-controller; - #address-cells = <0>; - #interrupt-cells = <1>; - reg = <0x7f804000 0x400 - 0x7f806000 0x10 - 0x7f806080 0x10 - 0x7f806100 0x10>; - interrupts = < 2 3 4 5 6 >; - hard-interrupt-sources = <64>; - soft-interrupt-sources = <64>; - interrupt-parent = <&cpuintc>; - }; - soc { - #address-cells = <1>; - #size-cells = <1>; - #interrupt-cells = <1>; - - compatible = "simple-bus", "mips,mips4k"; - ranges; - - memory { - device_type = "memory"; - reg = <0x0 0x4000000>; - }; - - serial@7f000000 { - compatible = "altera,jtag_uart-11_0"; - reg = <0x7f000000 0x40>; - /* Removing these two lines puts the UART - in polled mode which is necessary because - we don't have a PIC or a UART capable of - generating interrupts. Fortunately FreeBSD - copes. - interrupts = <0>; - interrupt-parent = <&beripic0>;*/ - }; - }; -}; |