From 5bd5dff99c934dccae8b96d36d4aaa5dead097e9 Mon Sep 17 00:00:00 2001 From: Jon French Date: Wed, 2 Aug 2017 06:11:27 +0100 Subject: fix run_with_elf*.ml with changed lem_interp api --- src/lem_interp/run_with_elf.ml | 2 +- src/lem_interp/run_with_elf_cheri.ml | 2 +- src/lem_interp/run_with_elf_cheri128.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index d48b7e7b..2a1783db 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -1292,7 +1292,7 @@ let run () = startaddr, startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in - let context = build_context isa_defs isa_m0 [] isa_m1 isa_m2 isa_m3 [] isa_m4 None isa_externs in + let context = build_context false isa_defs isa_m0 [] isa_m1 isa_m2 isa_m3 [] isa_m4 None isa_externs in (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index eaf8ddfa..e773bf5b 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -1386,7 +1386,7 @@ let run () = startaddr, startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in - let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in + let context = build_context false isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index eca6d342..cd2e7312 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -1386,7 +1386,7 @@ let run () = startaddr, startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in - let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in + let context = build_context false isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) -- cgit v1.2.3 From 0da449b2fdf892d485f700d33620d31802944ef6 Mon Sep 17 00:00:00 2001 From: Jon French Date: Wed, 2 Aug 2017 06:12:03 +0100 Subject: add .merlin file --- .merlin | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 .merlin diff --git a/.merlin b/.merlin new file mode 100644 index 00000000..d76ab020 --- /dev/null +++ b/.merlin @@ -0,0 +1,8 @@ +S src +S src/contrib/** +S src/gen_lib/** +S src/lem_interp/** +S src/pprint/** +S src/test/** +B src/_build/** +PKG num str unix uint zarith \ No newline at end of file -- cgit v1.2.3 From 3ee583761a8b7801d0870c0b47e050ac5c8851cd Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 2 Aug 2017 14:24:52 +0100 Subject: fix sail library test interpreter glue for API change. Also fix build_context val spec which was out of dated although lem did not complain for some reason... --- src/lem_interp/interp_interface.lem | 2 +- src/test/lib/run_test_interp.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 937db466..dcc9f537 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -259,7 +259,7 @@ type outcome = (* Functions to build up the initial state for interpretation *) -val build_context : specification -> memory_reads -> memory_read_taggeds-> memory_writes -> memory_write_eas -> memory_write_vals -> memory_write_vals_tagged -> barriers -> excl_res -> external_functions -> context +val build_context : bool -> specification -> memory_reads -> memory_read_taggeds-> memory_writes -> memory_write_eas -> memory_write_vals -> memory_write_vals_tagged -> barriers -> excl_res -> external_functions -> context val initial_instruction_state : context -> string -> list register_value -> instruction_state (* string is a function name, list of value are the parameters to that function *) diff --git a/src/test/lib/run_test_interp.ml b/src/test/lib/run_test_interp.ml index 3446ef9f..5f2ace1b 100644 --- a/src/test/lib/run_test_interp.ml +++ b/src/test/lib/run_test_interp.ml @@ -45,7 +45,7 @@ open Interp_inter_imp ;; open Sail_impl_base ;; let doit () = - let context = build_context Test_lem_ast.defs [] [] [] [] [] [] [] None [] in + let context = build_context false Test_lem_ast.defs [] [] [] [] [] [] [] None [] in translate_address context E_little_endian "run" None (address_of_integer (Nat_big_num.of_int 0));; doit () ;; -- cgit v1.2.3 From be571f711102cd6659257e5ee1de3b708ebee6ab Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 28 Jul 2017 11:54:27 +0100 Subject: work around missing >=_u in sail. --- risc-v/risc-v.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/risc-v/risc-v.sail b/risc-v/risc-v.sail index edf95c62..4b90e792 100644 --- a/risc-v/risc-v.sail +++ b/risc-v/risc-v.sail @@ -126,7 +126,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = case BLT -> rs1_val <_s rs2_val case BGE -> rs1_val >=_s rs2_val case BLTU -> rs1_val <_u rs2_val - case BGEU -> rs1_val >= rs2_val (* XXX is this signed or unsigned? *) + case BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *) } in if (taken) then nextPC := PC + EXTS(imm : 0b0) -- cgit v1.2.3 From ad0d53e799c0a3dcb2548a42554d5dcae7de5a01 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 8 Aug 2017 14:11:57 +0100 Subject: work on integrating risc-v model with rmem (incomplete). --- risc-v/Makefile | 13 + risc-v/hgen/ast.hgen | 13 + risc-v/hgen/fold.hgen | 13 + risc-v/hgen/herdtools_ast_to_shallow_ast.hgen | 122 +++++++++ risc-v/hgen/herdtools_types_to_shallow_types.hgen | 121 +++++++++ risc-v/hgen/lexer.hgen | 60 +++++ risc-v/hgen/map.hgen | 12 + risc-v/hgen/parser.hgen | 24 ++ risc-v/hgen/pretty.hgen | 12 + risc-v/hgen/regs_out_in.hgen | 5 + risc-v/hgen/sail_trans_out.hgen | 12 + risc-v/hgen/shallow_ast_to_herdtools_ast.hgen | 99 ++++++++ risc-v/hgen/shallow_types_to_herdtools_types.hgen | 40 +++ risc-v/hgen/token_types.hgen | 12 + risc-v/hgen/tokens.hgen | 13 + risc-v/hgen/trans_sail.hgen | 105 ++++++++ risc-v/hgen/types.hgen | 116 +++++++++ risc-v/hgen/types_sail_trans_out.hgen | 78 ++++++ risc-v/hgen/types_trans_sail.hgen | 33 +++ risc-v/risc-v.sail | 263 -------------------- risc-v/riscv.sail | 288 ++++++++++++++++++++++ risc-v/riscv_extras.lem | 58 +++++ risc-v/riscv_extras_embed.lem | 32 +++ risc-v/riscv_extras_embed_sequential.lem | 34 +++ 24 files changed, 1315 insertions(+), 263 deletions(-) create mode 100644 risc-v/Makefile create mode 100644 risc-v/hgen/ast.hgen create mode 100644 risc-v/hgen/fold.hgen create mode 100644 risc-v/hgen/herdtools_ast_to_shallow_ast.hgen create mode 100644 risc-v/hgen/herdtools_types_to_shallow_types.hgen create mode 100644 risc-v/hgen/lexer.hgen create mode 100644 risc-v/hgen/map.hgen create mode 100644 risc-v/hgen/parser.hgen create mode 100644 risc-v/hgen/pretty.hgen create mode 100644 risc-v/hgen/regs_out_in.hgen create mode 100644 risc-v/hgen/sail_trans_out.hgen create mode 100644 risc-v/hgen/shallow_ast_to_herdtools_ast.hgen create mode 100644 risc-v/hgen/shallow_types_to_herdtools_types.hgen create mode 100644 risc-v/hgen/token_types.hgen create mode 100644 risc-v/hgen/tokens.hgen create mode 100644 risc-v/hgen/trans_sail.hgen create mode 100644 risc-v/hgen/types.hgen create mode 100644 risc-v/hgen/types_sail_trans_out.hgen create mode 100644 risc-v/hgen/types_trans_sail.hgen delete mode 100644 risc-v/risc-v.sail create mode 100644 risc-v/riscv.sail create mode 100644 risc-v/riscv_extras.lem create mode 100644 risc-v/riscv_extras_embed.lem create mode 100644 risc-v/riscv_extras_embed_sequential.lem diff --git a/risc-v/Makefile b/risc-v/Makefile new file mode 100644 index 00000000..2f6af138 --- /dev/null +++ b/risc-v/Makefile @@ -0,0 +1,13 @@ + +SAIL:=../src/sail.native + +all: lem_ast shallow + +lem_ast: riscv.sail $(SAIL) + $(SAIL) -lem_ast $< + +shallow: riscv.sail $(SAIL) + $(SAIL) -lem_lib Riscv_extras_embed -lem $< + +clean: + rm -f riscv.lem riscv_embed*.lem diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen new file mode 100644 index 00000000..ee7cb3e1 --- /dev/null +++ b/risc-v/hgen/ast.hgen @@ -0,0 +1,13 @@ +| `RISCVThreadStart +| `RISCVUTYPE of bit20 * reg * riscvUop +| `RISCVJAL of bit20 * reg +| `RISCVJALR of bit12 * reg * reg +| `RISCVBType of bit12 * reg * reg * riscvBop +| `RISCVIType of bit12 * reg * reg * riscvIop +| `RISCVShiftIop of bit6 * reg * reg * riscvSop +| `RISCVRType of reg * reg * reg * riscvRop +| `RISCVLoad of bit12 * reg * reg * bool * wordWidth +| `RISCVStore of bit12 * reg * reg * wordWidth +| `RISCVADDIW of bit12 * reg * reg +| `RISCVSHIFTW of bit5 * reg * reg * riscvSop +| `RISCVRTYPEW of reg * reg * reg * riscvRopw diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen new file mode 100644 index 00000000..03318805 --- /dev/null +++ b/risc-v/hgen/fold.hgen @@ -0,0 +1,13 @@ +| `RISCVThreadStart -> (y_reg, y_sreg) +| `RISCVUTYPE (_, r0, _) -> fold_reg r0 (y_reg, y_sreg) +| `RISCVJAL (_, r0) -> fold_reg r0 (y_reg, y_sreg) +| `RISCVJALR (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVBType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVIType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVShiftIop (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVRType (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg))) +| `RISCVLoad (_, r0, r1, _, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVStore (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVADDIW (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVSHIFTW (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVRTYPEW (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg))) diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen new file mode 100644 index 00000000..e614b714 --- /dev/null +++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen @@ -0,0 +1,122 @@ +(*| `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) +*) \ No newline at end of file diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen new file mode 100644 index 00000000..1c925e2b --- /dev/null +++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen @@ -0,0 +1,121 @@ +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/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen new file mode 100644 index 00000000..a75eef9f --- /dev/null +++ b/risc-v/hgen/lexer.hgen @@ -0,0 +1,60 @@ +"lwu" , UTYPE { op=RSICVLUI }; +"auipc" , UTYPE { op=RSICVAUIPC }; + +"jal", JAL; +"jalr", JALR; + +"beq", BTYPE {op=RISCVBEQ}; +"bne", BTYPE {op=RISCVBNE}; +"blt", BTYPE {op=RISCVBLT}; +"bge", BTYPE {op=RISCVBGE}; +"bltu", BTYPE {op=RISCVBLTU}; +"bgeu", BTYPE {op=RISCVBGEU}; + +"addi", ITYPE {op=RISCVADDI}; +"stli", ITYPE {op=RISCVSTLI}; +"sltiu", ITYPE {op=RISCVSLTIU}; +"xori", ITYPE {op=RISCVXORI}; +"ori", ITYPE {op=RISCVORI}; +"andi", ITYPE {op=RISCVANDI}; + +"slli", SHIFTIOP{op=RISCVSLLI}; +"srli", SHIFTIOP{op=RISCVSRLI}; +"srai", SHIFTIOP{op=RISCVSRAI}; + +"add", RTYPE{op=RISCVADD}; +"sub", RTYPE{op=RISCVSUB}; +"sll", RTYPE{op=RISCVSLL}; +"slt", RTYPE{op=RISCVSLT}; +"sltu", RTYPE{op=RISCVSLT}; +"xor", RTYPE{op=RISCVXOR}; +"srl", RTYPE{op=RISCVSRL}; +"sra", RTYPE{op=RISCVSRA}; +"or", RTYPE{op=RISCVOR}; +"and", RTYPE{op=RISCVAND}; + +"lb", LOAD{unsigned=false; width=RISCBYTE}; +"lbu", LOAD{unsigned=true; width=RISCBYTE}; +"lh", LOAD{unsigned=false; width=RISCVHALF}; +"lhu", LOAD{unsigned=true; width=RISCVHALF}; +"lw", LOAD{unsigned=false; width=RISCVWORD}; +"lwu", LOAD{unsigned=true; width=RISCVWORD}; +"ld", LOAD{unsigned=false; width=RISCVDOUBLE}; + +"sb", STORE{width=RISCBYTE}; +"sh", STORE{width=RISCVHALF}; +"sw", STORE{width=RISCVWORD}; +"sd", STORE{width=RISCVDOUBLE}; + +"addiw", ADDIW; + +"slliw", SHIFTW{op=RISCVSLL}; +"srliw", SHIFTW{op=RISCVSRL}; +"sraiw", SHIFTW{op=RISCVSRA}; + +"addw", RTYPEW{op=RISCVADDW}; +"subw", RTYPEW{op=RISCVSUBW}; +"sslw", RTYPEW{op=RISCVSLLW}; +"srlw", RTYPEW{op=RISCVSRLW}; +"sraw", RTYPEW{op=RISCVSRAW}; + diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen new file mode 100644 index 00000000..ff14c428 --- /dev/null +++ b/risc-v/hgen/map.hgen @@ -0,0 +1,12 @@ +| `RISCVUTYPE (x, r0, y) -> `RISCVUTYPE (x, map_reg r0, y) +| `RISCVJAL (x, r0) -> `RISCVJAL (x, map_reg r0) +| `RISCVJALR (x, r0, r1) -> `RISCVJALR (x, map_reg r0, map_reg r1) +| `RISCVBType (x, r0, r1, y) -> `RISCVBType (x, map_reg r0, map_reg r1, y) +| `RISCVIType (x, r0, r1, y) -> `RISCVIType (x, map_reg r0, map_reg r1, y) +| `RISCVShiftIop (x, r0, r1, y) -> `RISCVShiftIop (x, map_reg r0, map_reg r1, y) +| `RISCVRType (r0, r1, r2, y) -> `RISCVRType (r0, map_reg r1, map_reg r2, y) +| `RISCVLoad (x, r0, r1, y, z) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z) +| `RISCVStore (x, r0, r1, y) -> `RISCVStore (x, map_reg r0, map_reg r1, y) +| `RISCVADDIW (x, r0, r1) -> `RISCVADDIW (x, map_reg r0, map_reg r1) +| `RISCVSHIFTW (x, r0, r1, y) -> `RISCVSHIFTW (x, map_reg r0, map_reg r1, y) +| `RISCVRTYPEW (r0, r1, r2, x) -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x) diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen new file mode 100644 index 00000000..ba4dcac7 --- /dev/null +++ b/risc-v/hgen/parser.hgen @@ -0,0 +1,24 @@ +| UTYPE reg COMMA NUM + { `RISCVUTYPE($4, $2, $1.o) } +| JAL reg COMMA NUM + { `RISCVJAL($4, $2) } +| JALR reg COMMA reg COMMA NUM + { `RISCVJALR($6, $4, $2) } +| BTYPE reg COMMA reg COMMA NUM + { `RISCVBType($6, $4, $2, $1.op) } +| ITYPE reg COMMA reg COMMA NUM + { `RISCVIType(o$6, $4, $2, $1.op) } +| SHIFTIOP reg COMMA reg COMMA NUM + { `RISCVShiftIop($6, $4, $2, $1.op) } +| RTYPE reg COMMA reg COMMA reg + { `RISCVRType ($6, $3, $2, $1.op) } +| LOAD reg COMMA NUM LPAR reg RPAR + { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width) } +| STORE reg COMMA NUM LPAR reg RPAR + { `RISCVStore($4, $6, $2, $1.width) } (* reg order? *) +| ADDIW reg COMMA reg COMMA NUM + { `RISCVADDIW ($6, $4, $2) } +| SHIFTW reg COMMA reg COMMA NUM + { `RISCVSHIFTW ($6, $4, $2, $1.op) } +| RTYPEW reg COMMA reg COMMA reg + { `RISCVRTYPEW ($6, $4, $2, $1.op) } diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen new file mode 100644 index 00000000..f8cb0e30 --- /dev/null +++ b/risc-v/hgen/pretty.hgen @@ -0,0 +1,12 @@ +| `RISCVUTYPE(imm, rd, op) -> sprintf "%s %s, %d" (pp_riscv_uop op) (pp_reg rd) imm +| `RISCVJAL(imm, rd) -> sprintf "jal %s, %d" (pp_reg rd) imm +| `RISCVJALR(imm, rs, rd) -> sprintf "jalr %s, %s, %d" (pp_reg rd) (pp_reg rs) imm +| `RISCVBType(imm, rs2, rs1, op) -> sprintf "%s %s, %s, %d" (pp_riscv_bop op) (pp_reg rs1) (pp_reg rs2) imm +| `RISCVIType(imm, rs2, rs1, op) -> sprintf "%s %s, %s, %d" (pp_riscv_iop op) (pp_reg rs1) (pp_reg rs2) imm +| `RISCVShiftIop(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm +| `RISCVRType (rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_rop op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2) +| `RISCVLoad(imm, rs, rd, unsigned, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width)) (pp_reg rd) imm (pp_reg rs) +| `RISCVStore(imm, rs, rd, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op width) (pp_reg rd) imm (pp_reg rs) +| `RISCVADDIW(imm, rs, rd) -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm +| `RISCVSHIFTW(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm +| `RISCVRTYPEW(rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2) diff --git a/risc-v/hgen/regs_out_in.hgen b/risc-v/hgen/regs_out_in.hgen new file mode 100644 index 00000000..8e1fd093 --- /dev/null +++ b/risc-v/hgen/regs_out_in.hgen @@ -0,0 +1,5 @@ +(* for each instruction instance, identify the role of the registers + and possible branching: (outputs, inputs, voidstars, branch) *) + +| `MIPSAdd -> + ([], [], [], [Next]) diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen new file mode 100644 index 00000000..8064aa19 --- /dev/null +++ b/risc-v/hgen/sail_trans_out.hgen @@ -0,0 +1,12 @@ +| ("UTYPE", [imm; rd; op]) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op) +| ("JAL", [imm; rd]) -> `RISCVJAL(translate_out_simm20 imm, translate_out_ireg rd) +| ("JALR", [imm; rs; rd]) -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) +| ("BTYPE", [imm; rs2; rs1; op]) -> `RISCVBType(translate_out_simm12 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op) +| ("ITYPE", [imm; rs1; rd; op]) -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op) +| ("SHIFTIOP", [imm; rs; rd; op]) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) +| ("RTYPE", [rs2; rs1; rd; op]) -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op) +| ("LOAD", [imm; rs; rd; unsigned; width]) -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width) +| ("STORE", [imm; rs; rd; width]) -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width) +| ("ADDIW", [imm; rs; rd]) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) +| ("SHIFTW", [imm; rs; rd; op]) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) +| ("RTYPEW", [rs2; rs1; rd; op]) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op) diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen new file mode 100644 index 00000000..9473d011 --- /dev/null +++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen @@ -0,0 +1,99 @@ +(*| 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) + +*) \ No newline at end of file diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen new file mode 100644 index 00000000..2c2efd8e --- /dev/null +++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen @@ -0,0 +1,40 @@ +(*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 *) +*) \ No newline at end of file diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen new file mode 100644 index 00000000..cc993ae3 --- /dev/null +++ b/risc-v/hgen/token_types.hgen @@ -0,0 +1,12 @@ +type token_UTYPE = {op : riscvUop } +type token_JAL = unit +type token_JALR = unit +type token_BType = {op : riscvBop } +type token_IType = {op : riscvIop } +type token_ShiftIop = {op : riscvSop } +type token_RTYPE = {op : riscvRop } +type token_Load = {unsigned: bool; width : wordWidth } +type token_Store = {width : wordWidth } +type token_ADDIW = unit +type token_SHIFTW = {op : riscvSop } +type token_RTYPEW = {op : riscvRopw } diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen new file mode 100644 index 00000000..0a874b81 --- /dev/null +++ b/risc-v/hgen/tokens.hgen @@ -0,0 +1,13 @@ +%token UTYPE +%token JAL +%token JALR +%token BTYPE +%token ITYPE +%token SHIFTIOP +%token RTYPE +%token LOAD +%token STORE +%token ADDIW +%token SHIFTW +%token RTYPEW + diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen new file mode 100644 index 00000000..3b825af2 --- /dev/null +++ b/risc-v/hgen/trans_sail.hgen @@ -0,0 +1,105 @@ +| `RISCVUTYPE(imm, rd, op) -> + ("UTYPE", + [ + translate_imm20 "imm" imm; + translate_reg "rd" rd; + translate_uop "op" op; + ], + []) +| `RISCVJAL(imm, rd) -> + ("JAL", + [ + translate_imm20 "imm" imm; + translate_reg "rd" rd; + ], + []) +| `RISCVJALR(imm, rs, rd) -> + ("JALR", + [ + translate_imm12 "imm" imm; + translate_reg "rs" rd; + translate_reg "rd" rd; + ], + []) +| `RISCVBType(imm, rs2, rs1, op) -> + ("BTYPE", + [ + translate_imm12 "imm" imm; + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_bop "op" op; + ], + []) +| `RISCVIType(imm, rs1, rd, op) -> + ("ITYPE", + [ + translate_imm12 "imm" imm; + translate_reg "rs1" rs1; + translate_reg "rd" rd; + translate_iop "op" op; + ], + []) +| `RISCVShiftIop(imm, rs, rd, op) -> + ("SHIFTIOP", + [ + translate_imm6 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + translate_sop "op" op; + ], + []) +| `RISCVRType (rs2, rs1, rd, op) -> + ("RTYPE", + [ + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_reg "rd" rd; + translate_rop "op" op; + ], + []) +| `RISCVLoad(imm, rs, rd, unsigned, width) -> + ("LOAD", + [ + translate_imm12 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + translate_bool "unsigned" unsigned; + translate_width "width" width; + ], + []) +| `RISCVStore(imm, rs, rd, width) -> + ("LOAD", + [ + translate_imm12 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + translate_width "width" width; + ], + []) +| `RISCVADDIW(imm, rs, rd) -> + ("ADDIW", + [ + translate_imm12 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + ], + []) +| `RISCVSHIFTW(imm, rs, rd, op) -> + ("SHIFTW", + [ + translate_imm5 "imm" imm; + translate_reg "rs" rs; + translate_reg "rd" rd; + translate_sop "op" op; + ], + []) +| `RISCVRTYPEW(rs2, rs1, rd, op) -> + ("RTYPEW", + [ + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; + translate_reg "rd" rd; + translate_ropw "op" op; + ], + []) + diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen new file mode 100644 index 00000000..e31b11f8 --- /dev/null +++ b/risc-v/hgen/types.hgen @@ -0,0 +1,116 @@ +type bit20 = int +type bit12 = int +type bit6 = int +type bit5 = int + +type riscvUop = (* upper immediate ops *) +| RISCVLUI +| RISCVAUIPC + +let pp_riscv_uop = function +| RISCVLUI -> "lui" +| RISCVAUIPC -> "auipc" + + +type riscvBop = (* branch ops *) +| RISCVBEQ +| RISCVBNE +| RISCVBLT +| RISCVBGE +| RISCVBLTU +| RISCVBGEU + +let pp_riscv_bop = function +| RISCVBEQ -> "beq" +| RISCVBNE -> "bne" +| RISCVBLT -> "blt" +| RISCVBGE -> "bge" +| RISCVBLTU -> "bltu" +| RISCVBGEU -> "bgeu" + +type riscvIop = (* immediate ops *) +| RISCVADDI +| RISCVSLTI +| RISCVSLTIU +| RISCVXORI +| RISCVORI +| RISCVANDI + +let pp_riscv_iop = function +| RISCVADDI -> "addi" +| RISCVSLTI -> "slti" +| RISCVSLTIU -> "sltiu" +| RISCVXORI -> "xori" +| RISCVORI -> "ori" +| RISCVANDI -> "andi" + +type riscvSop = (* shift ops *) +| RISCVSLLI +| RISCVSRLI +| RISCVSRAI + +let pp_riscv_sop = function +| RISCVSLLI -> "slli" +| RISCVSRLI -> "srli" +| RISCVSRAI -> "srai" + +type riscvRop = (* reg-reg ops *) +| RISCVADD +| RISCVSUB +| RISCVSLL +| RISCVSLT +| RISCVSLTU +| RISCVXOR +| RISCVSRL +| RISCVSRA +| RISCVOR +| RISCVAND + +let pp_riscv_rop = function +| RISCVADD -> "add" +| RISCVSUB -> "sub" +| RISCVSLL -> "sll" +| RISCVSLT -> "slt" +| RISCVSLTU -> "sltu" +| RISCVXOR -> "xor" +| RISCVSRL -> "srl" +| RISCVSRA -> "sra" +| RISCVOR -> "or" +| RISCVAND -> "and" + +type riscvRopw = (* reg-reg 32-bit ops *) +| RISCVADDW +| RISCVSUBW +| RISCVSLLW +| RISCVSRLW +| RISCVSRAW + +let pp_riscv_ropw = function +| RISCVADDW -> "addw" +| RISCVSUBW -> "subw" +| RISCVSLLW -> "sllw" +| RISCVSRLW -> "srlw" +| RISCVSRAW -> "sraw" + +type wordWidth = + | RISCVBYTE + | RISCVHALF + | RISCVWORD + | RISCVDOUBLE + +let pp_riscv_load_op (unsigned, width) = match (unsigned, width) with + | (false, RISCVBYTE) -> "lb" + | (true, RISCVBYTE) -> "lbu" + | (false, RISCVHALF) -> "lh" + | (true, RISCVHALF) -> "lhu" + | (false, RISCVWORD) -> "lw" + | (true, RISCVWORD) -> "lwu" + | (_, RISCVDOUBLE) -> "ld" + | _ -> failwith "unexpected load op" + +let pp_riscv_store_op width = match width with +| RISCVBYTE -> "sb" +| RISCVHALF -> "sh" +| RISCVWORD -> "sw" +| RISCVDOUBLE -> "sd" +| _ -> failwith "unexpected store op" diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen new file mode 100644 index 00000000..99d3d375 --- /dev/null +++ b/risc-v/hgen/types_sail_trans_out.hgen @@ -0,0 +1,78 @@ +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_simm20 imm = translate_out_signed_int imm 20 +let translate_out_simm12 imm = translate_out_signed_int imm 12 +let translate_out_imm6 imm = translate_out_int imm +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 w = + match translate_out_enum w with + | 0 -> RISCVBYTE + | 1 -> RISCVHALF + | 2 -> RISCVWORD + | 3 -> RISCVDOUBLE + | _ -> failwith "Unknown wordWidth in sail translate out" + +let translate_out_uop op = match translate_out_enum op with + | 0 -> RISCVLUI + | 1 -> RISCVAUIPC + | _ -> failwith "Unknown uop in sail translate out" + +let translate_out_bop op = match translate_out_enum op with +| 0 -> RISCVBEQ +| 1 -> RISCVBNE +| 2 -> RISCVBLT +| 3 -> RISCVBGE +| 4 -> RISCVBLTU +| 5 -> RISCVBGEU + +let translate_out_iop op = match translate_out_enum op with +| 0 -> RISCVADDI +| 1 -> RISCVSLTI +| 2 -> RISCVSLTIU +| 3 -> RISCVXORI +| 4 -> RISCVORI +| 5 -> RISCVANDI + +let translate_out_sop op = match translate_out_enum op with +| 0 -> RISCVSLLI +| 1 -> RISCVSRLI +| 2 -> RISCVSRAI + +let translate_out_rop op = match translate_out_enum op with +| 0 -> RISCVADD +| 1 -> RISCVSUB +| 2 -> RISCVSLL +| 3 -> RISCVSLT +| 4 -> RISCVSLTU +| 5 -> RISCVXOR +| 6 -> RISCVSRL +| 7 -> RISCVSRA +| 8 -> RISCVOR +| 9 -> RISCVAND + +let translate_out_ropw op = match translate_out_enum op with +| 0 -> RISCVADDW +| 1 -> RISCVSUBW +| 2 -> RISCVSLLW +| 3 -> RISCVSRLW +| 4 -> RISCVSRAW diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen new file mode 100644 index 00000000..9dd36d5e --- /dev/null +++ b/risc-v/hgen/types_trans_sail.hgen @@ -0,0 +1,33 @@ +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_uop = translate_enum [RISCVLUI; RISCVAUIPC] +let translate_bop = translate_enum [RISCVBEQ; RISCVBNE; RISCVBLT; RISCVBGE; RISCVBLTU; RISCVBGEU] (* branch ops *) +let translate_iop = translate_enum [RISCVADDI; RISCVSLTI; RISCVSLTIU; RISCVXORI; RISCVORI; RISCVANDI] (* immediate ops *) +let translate_sop = translate_enum [RISCVSLLI; RISCVSRLI; RISCVSRAI] (* shift ops *) +let translate_rop = translate_enum [RISCVADD; RISCVSUB; RISCVSLL; RISCVSLT; RISCVSLTU; RISCVXOR; RISCVSRL; RISCVSRA; RISCVOR; RISCVAND] (* reg-reg ops *) +let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW; RISCVSRAW] (* reg-reg 32-bit ops *) +let translate_width = translate_enum [RISCVBYTE; RISCVHALF; RISCVWORD; RISCVDOUBLE] +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_imm20 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_imm12 name value = + (name, Bvector (Some 12), bit_list_of_integer 12 (Nat_big_num.of_int value)) +let translate_imm6 name value = + (name, Bvector (Some 6), bit_list_of_integer 6 (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]) diff --git a/risc-v/risc-v.sail b/risc-v/risc-v.sail deleted file mode 100644 index 4b90e792..00000000 --- a/risc-v/risc-v.sail +++ /dev/null @@ -1,263 +0,0 @@ -default Order dec - -typedef regval = bit[64] -typedef regno = bit[5] - -register (regval) x0 -register (regval) x1 -register (regval) x2 -register (regval) x3 -register (regval) x4 -register (regval) x5 -register (regval) x6 -register (regval) x7 -register (regval) x8 -register (regval) x9 -register (regval) x10 -register (regval) x11 -register (regval) x12 -register (regval) x13 -register (regval) x14 -register (regval) x15 -register (regval) x16 -register (regval) x17 -register (regval) x18 -register (regval) x19 -register (regval) x20 -register (regval) x21 -register (regval) x22 -register (regval) x23 -register (regval) x24 -register (regval) x25 -register (regval) x26 -register (regval) x27 -register (regval) x28 -register (regval) x29 -register (regval) x30 -register (regval) x31 - -register (bit[64]) PC -register (bit[64]) nextPC - -let (vector <0, 32, inc, (register<(regval)>)>) GPRs = - [x0, x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31] - -function (regval) rGPR ((regno) r) = - if (r == 0) then - 0 - else - GPRs[r] - -function unit wGPR((regno) r, (regval) v) = - if (r != 0) then - GPRs[r] := v - -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval - -(* Ideally these would be sail builtin *) -function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) = - let (bit[128]) v128 = EXTS(v) in - (v128 >> shift)[63..0] - -function (bit[32]) shift_right_arith32 ((bit[32]) v, (bit[5]) shift) = - let (bit[64]) v64 = EXTS(v) in - (v64 >> shift)[31..0] - -typedef uop = enumerate {LUI; AUIPC} (* upper immediate ops *) -typedef bop = enumerate {BEQ; BNE; BLT; BGE; BLTU; BGEU} (* branch ops *) -typedef iop = enumerate {ADDI; SLTI; SLTIU; XORI; ORI; ANDI} (* immediate ops *) -typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *) -typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *) -typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *) - -scattered function unit execute -scattered typedef ast = const union - -val bit[32] -> option effect pure decode - -scattered function option decode - -union ast member ((bit[20]), regno, uop) UTYPE - -function clause decode ((bit[20]) imm : (regno) rd : 0b0110111) = Some(UTYPE(imm, rd, LUI)) -function clause decode ((bit[20]) imm : (regno) rd : 0b0010111) = Some(UTYPE(imm, rd, AUIPC)) - -function clause execute (UTYPE(imm, rd, op)) = - let (bit[64]) off = EXTS(imm : 0x000) in - let ret = switch (op) { - case LUI -> off - case AUIPC -> PC + off - } in - wGPR(rd, ret) - -union ast member ((bit[20]), regno) JAL -function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm, rd)) -function clause execute (JAL(imm, rd)) = - let (bit[64]) offset = EXTS(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0) in { - nextPC := PC + offset; - wGPR(rd, PC + 4); - } - -union ast member((bit[12]), regno, regno) JALR -function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b1100111) = - Some(JALR(imm, rs1, rd)) -function clause execute (JALR(imm, rs1, rd)) = - let (bit[64]) newPC = rGPR(rs1) + EXTS(imm) in { - nextPC := newPC[63..1] : 0b0; - wGPR(rd, PC + 4); - } - -union ast member ((bit[12]), regno, regno, bop) BTYPE -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BEQ)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BNE)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLT)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGE)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLTU)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGEU)) - -function clause execute (BTYPE(imm, rs2, rs1, op)) = - let rs1_val = rGPR(rs1) in - let rs2_val = rGPR(rs2) in - let taken = switch(op) { - case BEQ -> rs1_val == rs2_val - case BNE -> rs1_val != rs2_val - case BLT -> rs1_val <_s rs2_val - case BGE -> rs1_val >=_s rs2_val - case BLTU -> rs1_val <_u rs2_val - case BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *) - } in - if (taken) then - nextPC := PC + EXTS(imm : 0b0) - -union ast member ((bit[12]), regno, regno, iop) ITYPE -function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ADDI)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTI)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTIU)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, XORI)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ORI)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b111 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ANDI)) -function clause execute (ITYPE (imm, rs1, rd, op)) = - let rs1_val = rGPR(rs1) in - let imm64 = (bit[64]) (EXTS(imm)) in - let (bit[64]) result = switch(op) { - case ADDI -> rs1_val + imm64 - case SLTI -> EXTZ(rs1_val <_s imm64) - case SLTIU -> EXTZ(rs1_val <_u imm64) - case XORI -> rs1_val ^ imm64 - case ORI -> rs1_val | imm64 - case ANDI -> rs1_val & imm64 - } in - wGPR(rd, result) - -union ast member ((bit[6]), regno, regno, sop) SHIFTIOP -function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SLLI)) -function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRLI)) -function clause decode (0b010000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRAI)) -function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = - let rs1_val = rGPR(rs1) in - let result = switch(op) { - case SLLI -> rs1_val >> shamt - case SRLI -> rs1_val << shamt - case SRAI -> shift_right_arith64(rs1_val, shamt) - } in - wGPR(rd, result) - -union ast member (regno, regno, regno, rop) RTYPE -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, ADD)) -function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SUB)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLL)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLT)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLTU)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b100 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, XOR)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRL)) -function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRA)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b110 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, OR)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b111 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, AND)) -function clause execute (RTYPE(rs2, rs1, rd, op)) = - let rs1_val = rGPR(rs1) in - let rs2_val = rGPR(rs2) in - let (bit[64]) result = switch(op) { - case ADD -> rs1_val + rs2_val - case SUB -> rs1_val - rs2_val - case SLL -> rs1_val << (rs2_val[5..0]) - case SLT -> EXTZ(rs1_val <_s rs2_val) - case SLTU -> EXTZ(rs1_val <_u rs2_val) - case XOR -> rs1_val ^ rs2_val - case SRL -> rs1_val >> (rs2_val[5..0]) - case SRA -> shift_right_arith64(rs1_val, rs2_val[5..0]) - case OR -> rs1_val | rs2_val - case AND -> rs1_val & rs2_val - } in - wGPR(rd, result) - -union ast member ((bit[12]), regno, regno, bool, [|8|]) LOAD -function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 1)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 2)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 4)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 8)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, 1)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, 2)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, 4)) -function clause execute(LOAD(imm, rs1, rd, unsigned, width)) = - let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in - let (bit[64]) result = if unsigned then - EXTZ(MEMr(addr, width)) - else - EXTS(MEMr(addr, width)) in - wGPR(rd, result) - -union ast member ((bit[12]), regno, regno, [|8|]) STORE -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 1)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 2)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 4)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 8)) -function clause execute (STORE(imm, rs2, rs1, width)) = - let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in { - MEMea(addr, width); - MEMval(addr, width, rGPR(rs2)); - } - -union ast member ((bit[12]), regno, regno) ADDIW -function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0011011) = Some(ADDIW(imm, rs1, rd)) -function clause execute (ADDIW(imm, rs1, rd)) = - let (bit[64]) imm64 = EXTS(imm) in - let (bit[64]) result64 = imm64 + rGPR(rs1) in - let (bit[64]) result32 = EXTS(result64[31..0]) in - wGPR(rd, result32) - -union ast member ((bit[5]), regno, regno, sop) SHIFTW -function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SLLI)) -function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRLI)) -function clause decode (0b0100000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRAI)) -function clause execute (SHIFTW(shamt, rs1, rd, op)) = - let rs1_val = (rGPR(rs1))[31..0] in - let result = switch(op) { - case SLLI -> rs1_val >> shamt - case SRLI -> rs1_val << shamt - case SRAI -> shift_right_arith32(rs1_val, shamt) - } in - wGPR(rd, EXTS(result)) - -union ast member (regno, regno, regno, ropw) RTYPEW -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, ADDW)) -function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SUBW)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SLLW)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRLW)) -function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRAW)) -function clause execute (RTYPEW(rs2, rs1, rd, op)) = - let rs1_val = (rGPR(rs1))[31..0] in - let rs2_val = (rGPR(rs2))[31..0] in - let (bit[32]) result = switch(op) { - case ADDW -> rs1_val + rs2_val - case SUBW -> rs1_val - rs2_val - case SLLW -> rs1_val << (rs2_val[4..0]) - case SRLW -> rs1_val >> (rs2_val[4..0]) - case SRAW -> shift_right_arith32(rs1_val, rs2_val[4..0]) - } in - wGPR(rd, EXTS(result)) - -end ast -end decode -end execute diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail new file mode 100644 index 00000000..c91a0104 --- /dev/null +++ b/risc-v/riscv.sail @@ -0,0 +1,288 @@ +default Order dec + +typedef regval = bit[64] +typedef regno = bit[5] + +register (regval) x0 +register (regval) x1 +register (regval) x2 +register (regval) x3 +register (regval) x4 +register (regval) x5 +register (regval) x6 +register (regval) x7 +register (regval) x8 +register (regval) x9 +register (regval) x10 +register (regval) x11 +register (regval) x12 +register (regval) x13 +register (regval) x14 +register (regval) x15 +register (regval) x16 +register (regval) x17 +register (regval) x18 +register (regval) x19 +register (regval) x20 +register (regval) x21 +register (regval) x22 +register (regval) x23 +register (regval) x24 +register (regval) x25 +register (regval) x26 +register (regval) x27 +register (regval) x28 +register (regval) x29 +register (regval) x30 +register (regval) x31 + +register (bit[64]) PC +register (bit[64]) nextPC + +let (vector <0, 32, inc, (register<(regval)>)>) GPRs = + [x0, x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31] + +function (regval) rGPR ((regno) r) = + if (r == 0) then + 0 + else + GPRs[r] + +function unit wGPR((regno) r, (regval) v) = + if (r != 0) then + GPRs[r] := v + +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval + +(* Ideally these would be sail builtin *) +function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) = + let (bit[128]) v128 = EXTS(v) in + (v128 >> shift)[63..0] + +function (bit[32]) shift_right_arith32 ((bit[32]) v, (bit[5]) shift) = + let (bit[64]) v64 = EXTS(v) in + (v64 >> shift)[31..0] + +typedef uop = enumerate {LUI; AUIPC} (* upper immediate ops *) +typedef bop = enumerate {BEQ; BNE; BLT; BGE; BLTU; BGEU} (* branch ops *) +typedef iop = enumerate {ADDI; SLTI; SLTIU; XORI; ORI; ANDI} (* immediate ops *) +typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *) +typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *) +typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *) + +typedef word_width = enumerate {BYTE; HALF; WORD; DOUBLE} + +scattered function unit execute +scattered typedef ast = const union + +val bit[32] -> option effect pure decode + +scattered function option decode + +union ast member ((bit[20]), regno, uop) UTYPE + +function clause decode ((bit[20]) imm : (regno) rd : 0b0110111) = Some(UTYPE(imm, rd, LUI)) +function clause decode ((bit[20]) imm : (regno) rd : 0b0010111) = Some(UTYPE(imm, rd, AUIPC)) + +function clause execute (UTYPE(imm, rd, op)) = + let (bit[64]) off = EXTS(imm : 0x000) in + let ret = switch (op) { + case LUI -> off + case AUIPC -> PC + off + } in + wGPR(rd, ret) + +union ast member ((bit[20]), regno) JAL +function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm, rd)) +function clause execute (JAL(imm, rd)) = + let (bit[64]) offset = EXTS(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0) in { + nextPC := PC + offset; + wGPR(rd, PC + 4); + } + +union ast member((bit[12]), regno, regno) JALR +function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b1100111) = + Some(JALR(imm, rs1, rd)) +function clause execute (JALR(imm, rs1, rd)) = + let (bit[64]) newPC = rGPR(rs1) + EXTS(imm) in { + nextPC := newPC[63..1] : 0b0; + wGPR(rd, PC + 4); + } + +union ast member ((bit[12]), regno, regno, bop) BTYPE +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BEQ)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BNE)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLT)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGE)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLTU)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGEU)) + +function clause execute (BTYPE(imm, rs2, rs1, op)) = + let rs1_val = rGPR(rs1) in + let rs2_val = rGPR(rs2) in + let taken = switch(op) { + case BEQ -> rs1_val == rs2_val + case BNE -> rs1_val != rs2_val + case BLT -> rs1_val <_s rs2_val + case BGE -> rs1_val >=_s rs2_val + case BLTU -> rs1_val <_u rs2_val + case BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *) + } in + if (taken) then + nextPC := PC + EXTS(imm : 0b0) + +union ast member ((bit[12]), regno, regno, iop) ITYPE +function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ADDI)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTI)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTIU)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, XORI)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ORI)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b111 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ANDI)) +function clause execute (ITYPE (imm, rs1, rd, op)) = + let rs1_val = rGPR(rs1) in + let imm64 = (bit[64]) (EXTS(imm)) in + let (bit[64]) result = switch(op) { + case ADDI -> rs1_val + imm64 + case SLTI -> EXTZ(rs1_val <_s imm64) + case SLTIU -> EXTZ(rs1_val <_u imm64) + case XORI -> rs1_val ^ imm64 + case ORI -> rs1_val | imm64 + case ANDI -> rs1_val & imm64 + } in + wGPR(rd, result) + +union ast member ((bit[6]), regno, regno, sop) SHIFTIOP +function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SLLI)) +function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRLI)) +function clause decode (0b010000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRAI)) +function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = + let rs1_val = rGPR(rs1) in + let result = switch(op) { + case SLLI -> rs1_val >> shamt + case SRLI -> rs1_val << shamt + case SRAI -> shift_right_arith64(rs1_val, shamt) + } in + wGPR(rd, result) + +union ast member (regno, regno, regno, rop) RTYPE +function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, ADD)) +function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SUB)) +function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLL)) +function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLT)) +function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLTU)) +function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b100 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, XOR)) +function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRL)) +function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRA)) +function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b110 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, OR)) +function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b111 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, AND)) +function clause execute (RTYPE(rs2, rs1, rd, op)) = + let rs1_val = rGPR(rs1) in + let rs2_val = rGPR(rs2) in + let (bit[64]) result = switch(op) { + case ADD -> rs1_val + rs2_val + case SUB -> rs1_val - rs2_val + case SLL -> rs1_val << (rs2_val[5..0]) + case SLT -> EXTZ(rs1_val <_s rs2_val) + case SLTU -> EXTZ(rs1_val <_u rs2_val) + case XOR -> rs1_val ^ rs2_val + case SRL -> rs1_val >> (rs2_val[5..0]) + case SRA -> shift_right_arith64(rs1_val, rs2_val[5..0]) + case OR -> rs1_val | rs2_val + case AND -> rs1_val & rs2_val + } in + wGPR(rd, result) + +union ast member ((bit[12]), regno, regno, bool, word_width) LOAD +function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, BYTE)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, HALF)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, WORD)) +function clause execute(LOAD(imm, rs1, rd, unsigned, width)) = + let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in + let (bit[64]) result = if unsigned then + switch (width) { + case BYTE -> EXTZ(MEMr(addr, 1)) + case WORD -> EXTZ(MEMr(addr, 2)) + case HALF -> EXTZ(MEMr(addr, 4)) + case DOUBLE -> MEMr(addr, 8) + } + else + switch (width) { + case BYTE -> EXTS(MEMr(addr, 1)) + case WORD -> EXTS(MEMr(addr, 2)) + case HALF -> EXTS(MEMr(addr, 4)) + case DOUBLE -> MEMr(addr, 8) + } in + wGPR(rd, result) + +union ast member ((bit[12]), regno, regno, word_width) STORE +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, BYTE)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, HALF)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, WORD)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE)) +function clause execute (STORE(imm, rs2, rs1, width)) = + let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in { + switch (width) { + case BYTE -> MEMea(addr, 1) + case WORD -> MEMea(addr, 2) + case HALF -> MEMea(addr, 4) + case DOUBLE -> MEMea(addr, 8) + }; + let rs2_val = rGPR(rs2) in + switch (width) { + case BYTE -> MEMval(addr, 1, rs2_val) + case WORD -> MEMval(addr, 2, rs2_val) + case HALF -> MEMval(addr, 4, rs2_val) + case DOUBLE -> MEMval(addr, 8, rs2_val) + } + } + +union ast member ((bit[12]), regno, regno) ADDIW +function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0011011) = Some(ADDIW(imm, rs1, rd)) +function clause execute (ADDIW(imm, rs1, rd)) = + let (bit[64]) imm64 = EXTS(imm) in + let (bit[64]) result64 = imm64 + rGPR(rs1) in + let (bit[64]) result32 = EXTS(result64[31..0]) in + wGPR(rd, result32) + +union ast member ((bit[5]), regno, regno, sop) SHIFTW +function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SLLI)) +function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRLI)) +function clause decode (0b0100000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRAI)) +function clause execute (SHIFTW(shamt, rs1, rd, op)) = + let rs1_val = (rGPR(rs1))[31..0] in + let result = switch(op) { + case SLLI -> rs1_val >> shamt + case SRLI -> rs1_val << shamt + case SRAI -> shift_right_arith32(rs1_val, shamt) + } in + wGPR(rd, EXTS(result)) + +union ast member (regno, regno, regno, ropw) RTYPEW +function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, ADDW)) +function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SUBW)) +function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SLLW)) +function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRLW)) +function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRAW)) +function clause execute (RTYPEW(rs2, rs1, rd, op)) = + let rs1_val = (rGPR(rs1))[31..0] in + let rs2_val = (rGPR(rs2))[31..0] in + let (bit[32]) result = switch(op) { + case ADDW -> rs1_val + rs2_val + case SUBW -> rs1_val - rs2_val + case SLLW -> rs1_val << (rs2_val[4..0]) + case SRLW -> rs1_val >> (rs2_val[4..0]) + case SRAW -> shift_right_arith32(rs1_val, rs2_val[4..0]) + } in + wGPR(rd, EXTS(result)) + +function clause decode _ = None + +end ast +end decode +end execute diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem new file mode 100644 index 00000000..c09c85c2 --- /dev/null +++ b/risc-v/riscv_extras.lem @@ -0,0 +1,58 @@ +open import Pervasives +open import Interp_ast +open import Interp_interface +open import Sail_impl_base +open import Interp_inter_imp +import Set_extra + +let memory_parameter_transformer mode v = + match v with + | Interp_ast.V_tuple [location;length] -> + let (v,loc_regs) = extern_with_track mode extern_vector_value location in + + match length with + | Interp_ast.V_lit (L_aux (L_num len) _) -> + (v,(natFromInteger len),loc_regs) + | Interp_ast.V_track (Interp_ast.V_lit (L_aux (L_num len) _)) size_regs -> + match loc_regs with + | Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))) + | Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))) + end + | _ -> Assert_extra.failwith "expected 'V_lit (L_aux (L_num _) _)' or 'V_track (V_lit (L_aux (L_num len) _)) _'" + end + | _ -> Assert_extra.failwith ("memory_parameter_transformer: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v)) + end + +let memory_parameter_transformer_option_address _mode v = + match v with + | Interp_ast.V_tuple [location;_] -> + Just (extern_vector_value location) + | _ -> Assert_extra.failwith ("memory_parameter_transformer_option_address: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v)) + end + + +let read_memory_functions : memory_reads = + [ ("MEMr", (MR Read_plain memory_parameter_transformer)); + ("MEMr_reserve", (MR Read_reserve memory_parameter_transformer)); + ] + +let memory_writes : memory_writes = + [] + +let memory_eas : memory_write_eas = + [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); + ("MEMea_conditional", (MEA Write_conditional memory_parameter_transformer)); + ] + +let memory_vals : memory_write_vals = + [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_conditional", (MV memory_parameter_transformer_option_address + (Just + (fun (IState interp context) b -> + let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in + (IState (Interp.add_answer_to_stack interp bit) context))))); + ] + +let barrier_functions = [ + ("MEM_sync", Barrier_MIPS_SYNC); + ] diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem new file mode 100644 index 00000000..cbc8bd0d --- /dev/null +++ b/risc-v/riscv_extras_embed.lem @@ -0,0 +1,32 @@ +open import Pervasives +open import Pervasives_extra +open import Sail_impl_base +open import Sail_values +open import Prompt + +val MEMr : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserve : (vector bitU * integer) -> M (vector bitU) + +let MEMr (addr,size) = read_mem false Read_plain addr size +let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size + +val MEMea : (vector bitU * integer) -> M unit +val MEMea_conditional : (vector bitU * integer) -> M unit + +let MEMea (addr,size) = write_mem_ea Write_plain addr size +let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size + +val MEMval : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU + +let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) + +val MEM_sync : unit -> M unit + +let MEM_sync () = barrier Barrier_Isync + +let duplicate (bit,len) = + let bits = repeat [bit] len in + let start = len - 1 in + Vector bits start false diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem new file mode 100644 index 00000000..7fb62161 --- /dev/null +++ b/risc-v/riscv_extras_embed_sequential.lem @@ -0,0 +1,34 @@ +open import Pervasives +open import Pervasives_extra +open import Sail_impl_base +open import Sail_values +open import State + +val MEMr : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserve : (vector bitU * integer) -> M (vector bitU) + +let MEMr (addr,size) = read_mem false Read_plain addr size +let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size + +val MEMea : (vector bitU * integer) -> M unit +val MEMea_conditional : (vector bitU * integer) -> M unit + +let MEMea (addr,size) = write_mem_ea Write_plain addr size +let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size + + +val MEMval : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU + +let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) + +val MEM_sync : unit -> M unit + +let MEM_sync () = barrier Barrier_MIPS_SYNC + + +let duplicate (bit,len) = + let bits = repeat [bit] len in + let start = len - 1 in + Vector bits start false -- cgit v1.2.3 From f8a186733a4a8afd90ef733ca32df92eb6bcecd9 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 11 Aug 2017 15:47:08 +0100 Subject: further riscv rmem integration. --- risc-v/Makefile | 10 +- risc-v/hgen/ast.hgen | 1 - risc-v/hgen/herdtools_ast_to_shallow_ast.hgen | 169 +++++++-------------- risc-v/hgen/herdtools_types_to_shallow_types.hgen | 170 ++++++++-------------- risc-v/hgen/lexer.hgen | 24 +-- risc-v/hgen/parser.hgen | 8 +- risc-v/hgen/pretty.hgen | 2 + risc-v/hgen/sail_trans_out.hgen | 1 + risc-v/hgen/shallow_ast_to_herdtools_ast.hgen | 112 ++------------ risc-v/hgen/shallow_types_to_herdtools_types.hgen | 74 +++++++--- risc-v/hgen/trans_sail.hgen | 3 +- risc-v/hgen/types_sail_trans_out.hgen | 5 + risc-v/riscv.sail | 4 + risc-v/riscv_regfp.sail | 81 +++++++++++ 14 files changed, 293 insertions(+), 371 deletions(-) create mode 100644 risc-v/riscv_regfp.sail diff --git a/risc-v/Makefile b/risc-v/Makefile index 2f6af138..856a48eb 100644 --- a/risc-v/Makefile +++ b/risc-v/Makefile @@ -1,13 +1,13 @@ SAIL:=../src/sail.native - +SOURCES:=riscv.sail ../etc/regfp.sail riscv_regfp.sail all: lem_ast shallow -lem_ast: riscv.sail $(SAIL) - $(SAIL) -lem_ast $< +lem_ast: $(SOURCES) $(SAIL) + $(SAIL) -lem_ast $(SOURCES) -shallow: riscv.sail $(SAIL) - $(SAIL) -lem_lib Riscv_extras_embed -lem $< +shallow: $(SOURCES) $(SAIL) + $(SAIL) -lem_lib Riscv_extras_embed -lem $(SOURCES) clean: rm -f riscv.lem riscv_embed*.lem diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen index ee7cb3e1..62e7cf4b 100644 --- a/risc-v/hgen/ast.hgen +++ b/risc-v/hgen/ast.hgen @@ -1,4 +1,3 @@ -| `RISCVThreadStart | `RISCVUTYPE of bit20 * reg * riscvUop | `RISCVJAL of bit20 * reg | `RISCVJALR of bit12 * reg * reg diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen index e614b714..ac6f22bd 100644 --- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen +++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen @@ -1,122 +1,57 @@ -(*| `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) - ( +| `RISCVStopFetching -> EBREAK +| `RISCVUTYPE(imm, rd, op) -> UTYPE( + translate_imm20 "imm" imm, + translate_reg "rd" rd, + translate_uop op) +| `RISCVJAL(imm, rd) -> JAL0( + translate_imm20 "imm" imm, + translate_reg "rd" rd) +| `RISCVJALR(imm, rs, rd) -> JALR0( + translate_imm12 "imm" imm, + translate_reg "rs" rd, + translate_reg "rd" rd) +| `RISCVBType(imm, rs2, rs1, op) -> BTYPE( + translate_imm12 "imm" imm, + translate_reg "rs2" rs2, + translate_reg "rs1" rs1, + translate_bop op) +| `RISCVIType(imm, rs1, rd, op) -> ITYPE( + translate_imm12 "imm" imm, + translate_reg "rs1" rs1, + translate_reg "rd" rd, + translate_iop op) +| `RISCVShiftIop(imm, rs, rd, op) -> SHIFTIOP( + translate_imm6 "imm" imm, + translate_reg "rs" rs, + translate_reg "rd" rd, + translate_sop op) +| `RISCVRType (rs2, rs1, rd, op) -> RTYPE ( + translate_reg "rs2" rs2, + translate_reg "rs1" rs1, + translate_reg "rd" rd, + translate_rop op) +| `RISCVLoad(imm, rs, rd, unsigned, width) -> LOAD( + translate_imm12 "imm" imm, 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 "rd" rd, + translate_bool "unsigned" unsigned, + translate_wordWidth width) +| `RISCVStore(imm, rs, rd, width) -> STORE ( + translate_imm12 "imm" imm, 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_wordWidth width) +| `RISCVADDIW(imm, rs, rd) -> ADDIW( + translate_imm12 "imm" imm, translate_reg "rs" rs, - translate_reg "rt" rt, - translate_reg "rd" rd - ) - - -| `MIPSMulDiv (op, rs, rt) -> - (translate_muldiv_op op) - ( + translate_reg "rd" rd) +| `RISCVSHIFTW(imm, rs, rd, op) -> SHIFTW( + translate_imm5 "imm" imm, 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) -*) \ No newline at end of file + translate_reg "rd" rd, + translate_sop op) +| `RISCVRTYPEW(rs2, rs1, rd, op) -> RTYPEW( + translate_reg "rs2" rs2, + translate_reg "rs1" rs1, + translate_reg "rd" rd, + translate_ropw op) diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen index 1c925e2b..c4a1fd37 100644 --- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen +++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen @@ -1,121 +1,71 @@ 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_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_store_op width conditional = uppercase (pp_store_op width conditional) +let translate_uop op = match op with + | RISCVLUI -> LUI0 + | RISCVAUIPC -> AUIPC + +let translate_bop op = match op with + | RISCVBEQ -> BEQ0 + | RISCVBNE -> BNE + | RISCVBLT -> BLT + | RISCVBGE -> BGE + | RISCVBLTU -> BLTU + | RISCVBGEU -> BGEU + +let translate_iop op = match op with + | RISCVADDI -> ADDI0 + | RISCVSLTI -> SLTI0 + | RISCVSLTIU -> SLTIU0 + | RISCVXORI -> XORI0 + | RISCVORI -> ORI0 + | RISCVANDI -> ANDI0 + +let translate_sop op = match op with + | RISCVSLLI -> SLLI + | RISCVSRLI -> SRLI + | RISCVSRAI -> SRAI + +let translate_rop op = match op with + | RISCVADD -> ADD0 + | RISCVSUB -> SUB0 + | RISCVSLL -> SLL0 + | RISCVSLT -> SLT0 + | RISCVSLTU -> SLTU0 + | RISCVXOR -> XOR0 + | RISCVSRL -> SRL0 + | RISCVSRA -> SRA0 + | RISCVOR -> OR0 + | RISCVAND -> AND0 + +let translate_ropw op = match op with + | RISCVADDW -> ADDW + | RISCVSUBW -> SUBW + | RISCVSLLW -> SLLW + | RISCVSRLW -> SRLW + | RISCVSRAW -> SRAW + +let translate_wordWidth op = match op with + | RISCVBYTE -> BYTE + | RISCVHALF -> HALF + | RISCVWORD -> WORD + | RISCVDOUBLE -> DOUBLE -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_bool name = function + | true -> Sail_values.B1 + | false -> Sail_values.B0 -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_imm20 name value = + Sail_values.to_vec0 is_inc (Nat_big_num.of_int 20,Nat_big_num.of_int value) +let translate_imm12 name value = + Sail_values.to_vec0 is_inc (Nat_big_num.of_int 12,Nat_big_num.of_int value) -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_imm6 name value = + Sail_values.to_vec0 is_inc (Nat_big_num.of_int 6,Nat_big_num.of_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/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen index a75eef9f..75d890e4 100644 --- a/risc-v/hgen/lexer.hgen +++ b/risc-v/hgen/lexer.hgen @@ -1,8 +1,8 @@ -"lwu" , UTYPE { op=RSICVLUI }; -"auipc" , UTYPE { op=RSICVAUIPC }; +"lwu" , UTYPE { op=RISCVLUI }; +"auipc" , UTYPE { op=RISCVAUIPC }; -"jal", JAL; -"jalr", JALR; +"jal", JAL (); +"jalr", JALR (); "beq", BTYPE {op=RISCVBEQ}; "bne", BTYPE {op=RISCVBNE}; @@ -12,7 +12,7 @@ "bgeu", BTYPE {op=RISCVBGEU}; "addi", ITYPE {op=RISCVADDI}; -"stli", ITYPE {op=RISCVSTLI}; +"stli", ITYPE {op=RISCVSLTI}; "sltiu", ITYPE {op=RISCVSLTIU}; "xori", ITYPE {op=RISCVXORI}; "ori", ITYPE {op=RISCVORI}; @@ -33,24 +33,24 @@ "or", RTYPE{op=RISCVOR}; "and", RTYPE{op=RISCVAND}; -"lb", LOAD{unsigned=false; width=RISCBYTE}; -"lbu", LOAD{unsigned=true; width=RISCBYTE}; +"lb", LOAD{unsigned=false; width=RISCVBYTE}; +"lbu", LOAD{unsigned=true; width=RISCVBYTE}; "lh", LOAD{unsigned=false; width=RISCVHALF}; "lhu", LOAD{unsigned=true; width=RISCVHALF}; "lw", LOAD{unsigned=false; width=RISCVWORD}; "lwu", LOAD{unsigned=true; width=RISCVWORD}; "ld", LOAD{unsigned=false; width=RISCVDOUBLE}; -"sb", STORE{width=RISCBYTE}; +"sb", STORE{width=RISCVBYTE}; "sh", STORE{width=RISCVHALF}; "sw", STORE{width=RISCVWORD}; "sd", STORE{width=RISCVDOUBLE}; -"addiw", ADDIW; +"addiw", ADDIW (); -"slliw", SHIFTW{op=RISCVSLL}; -"srliw", SHIFTW{op=RISCVSRL}; -"sraiw", SHIFTW{op=RISCVSRA}; +"slliw", SHIFTW{op=RISCVSLLI}; +"srliw", SHIFTW{op=RISCVSRLI}; +"sraiw", SHIFTW{op=RISCVSRAI}; "addw", RTYPEW{op=RISCVADDW}; "subw", RTYPEW{op=RISCVSUBW}; diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen index ba4dcac7..abd87c7f 100644 --- a/risc-v/hgen/parser.hgen +++ b/risc-v/hgen/parser.hgen @@ -1,5 +1,5 @@ | UTYPE reg COMMA NUM - { `RISCVUTYPE($4, $2, $1.o) } + { `RISCVUTYPE($4, $2, $1.op) } | JAL reg COMMA NUM { `RISCVJAL($4, $2) } | JALR reg COMMA reg COMMA NUM @@ -7,15 +7,15 @@ | BTYPE reg COMMA reg COMMA NUM { `RISCVBType($6, $4, $2, $1.op) } | ITYPE reg COMMA reg COMMA NUM - { `RISCVIType(o$6, $4, $2, $1.op) } + { `RISCVIType($6, $4, $2, $1.op) } | SHIFTIOP reg COMMA reg COMMA NUM { `RISCVShiftIop($6, $4, $2, $1.op) } | RTYPE reg COMMA reg COMMA reg - { `RISCVRType ($6, $3, $2, $1.op) } + { `RISCVRType ($6, $4, $2, $1.op) } | LOAD reg COMMA NUM LPAR reg RPAR { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width) } | STORE reg COMMA NUM LPAR reg RPAR - { `RISCVStore($4, $6, $2, $1.width) } (* reg order? *) + { `RISCVStore($4, $6, $2, $1.width) } | ADDIW reg COMMA reg COMMA NUM { `RISCVADDIW ($6, $4, $2) } | SHIFTW reg COMMA reg COMMA NUM diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen index f8cb0e30..0587c321 100644 --- a/risc-v/hgen/pretty.hgen +++ b/risc-v/hgen/pretty.hgen @@ -1,3 +1,5 @@ +| `RISCVThreadStart -> "start" +| `RISCVStopFetching -> "stop" | `RISCVUTYPE(imm, rd, op) -> sprintf "%s %s, %d" (pp_riscv_uop op) (pp_reg rd) imm | `RISCVJAL(imm, rd) -> sprintf "jal %s, %d" (pp_reg rd) imm | `RISCVJALR(imm, rs, rd) -> sprintf "jalr %s, %s, %d" (pp_reg rd) (pp_reg rs) imm diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen index 8064aa19..7f1ae8ea 100644 --- a/risc-v/hgen/sail_trans_out.hgen +++ b/risc-v/hgen/sail_trans_out.hgen @@ -1,3 +1,4 @@ +| ("EBREAK", []) -> `RISCVStopFetching | ("UTYPE", [imm; rd; op]) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op) | ("JAL", [imm; rd]) -> `RISCVJAL(translate_out_simm20 imm, translate_out_ireg rd) | ("JALR", [imm; rs; rd]) -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen index 9473d011..9dc80a98 100644 --- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen +++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen @@ -1,99 +1,13 @@ -(*| 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) - -*) \ No newline at end of file +| EBREAK -> `RISCVStopFetching +| UTYPE( imm, rd, op) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op) +| JAL0( imm, rd) -> `RISCVJAL(translate_out_simm20 imm, translate_out_ireg rd) +| JALR0( imm, rs, rd) -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) +| BTYPE( imm, rs2, rs1, op) -> `RISCVBType(translate_out_simm12 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op) +| ITYPE( imm, rs1, rd, op) -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op) +| SHIFTIOP( imm, rs, rd, op) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) +| RTYPE( rs2, rs1, rd, op) -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op) +| LOAD( imm, rs, rd, unsigned, width) -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width) +| STORE( imm, rs, rd, width) -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width) +| ADDIW( imm, rs, rd) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) +| SHIFTW( imm, rs, rd, op) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) +| RTYPEW( rs2, rs1, rd, op) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op) diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen index 2c2efd8e..d635efde 100644 --- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen +++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen @@ -1,4 +1,4 @@ -(*let translate_out_big_bit = Sail_values.unsigned +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 = @@ -9,32 +9,62 @@ let translate_out_signed_int inst bits = 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_uop op = match op with + | LUI0 -> RISCVLUI + | AUIPC -> RISCVAUIPC -let translate_out_imm16 imm = translate_out_int imm -let translate_out_simm16 imm = translate_out_signed_int imm 16 +let translate_out_bop op = match op with + | BEQ0 -> RISCVBEQ + | BNE -> RISCVBNE + | BLT -> RISCVBLT + | BGE -> RISCVBGE + | BLTU -> RISCVBLTU + | BGEU -> RISCVBGEU -let translate_out_imm5 imm = translate_out_int imm +let translate_out_iop op = match op with + | ADDI0 -> RISCVADDI + | SLTI0 -> RISCVSLTI + | SLTIU0 -> RISCVSLTIU + | XORI0 -> RISCVXORI + | ORI0 -> RISCVORI + | ANDI0 -> RISCVANDI + +let translate_out_sop op = match op with + | SLLI -> RISCVSLLI + | SRLI -> RISCVSRLI + | SRAI -> RISCVSRAI + +let translate_out_rop op = match op with + | ADD0 -> RISCVADD + | SUB0 -> RISCVSUB + | SLL0 -> RISCVSLL + | SLT0 -> RISCVSLT + | SLTU0 -> RISCVSLTU + | XOR0 -> RISCVXOR + | SRL0 -> RISCVSRL + | SRA0 -> RISCVSRA + | OR0 -> RISCVOR + | AND0 -> RISCVAND + +let translate_out_ropw op = match op with + | ADDW -> RISCVADDW + | SUBW -> RISCVSUBW + | SLLW -> RISCVSLLW + | SRLW -> RISCVSRLW + | SRAW -> RISCVSRAW + +let translate_out_wordWidth op = match op with + | BYTE -> RISCVBYTE + | HALF -> RISCVHALF + | WORD -> RISCVWORD + | DOUBLE -> RISCVDOUBLE 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 *) -*) \ No newline at end of file +let translate_out_simm20 imm = translate_out_signed_int imm 20 +let translate_out_simm12 imm = translate_out_signed_int imm 12 +let translate_out_imm6 imm = translate_out_int imm +let translate_out_imm5 imm = translate_out_int imm diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen index 3b825af2..fd51c81f 100644 --- a/risc-v/hgen/trans_sail.hgen +++ b/risc-v/hgen/trans_sail.hgen @@ -1,3 +1,4 @@ +| `RISCVStopFetching -> ("EBREAK", [], []) | `RISCVUTYPE(imm, rd, op) -> ("UTYPE", [ @@ -68,7 +69,7 @@ ], []) | `RISCVStore(imm, rs, rd, width) -> - ("LOAD", + ("STORE", [ translate_imm12 "imm" imm; translate_reg "rs" rs; diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen index 99d3d375..e034cf37 100644 --- a/risc-v/hgen/types_sail_trans_out.hgen +++ b/risc-v/hgen/types_sail_trans_out.hgen @@ -44,6 +44,7 @@ let translate_out_bop op = match translate_out_enum op with | 3 -> RISCVBGE | 4 -> RISCVBLTU | 5 -> RISCVBGEU +| _ -> failwith "Unknown bop in sail translate out" let translate_out_iop op = match translate_out_enum op with | 0 -> RISCVADDI @@ -52,11 +53,13 @@ let translate_out_iop op = match translate_out_enum op with | 3 -> RISCVXORI | 4 -> RISCVORI | 5 -> RISCVANDI +| _ -> failwith "Unknown iop in sail translate out" let translate_out_sop op = match translate_out_enum op with | 0 -> RISCVSLLI | 1 -> RISCVSRLI | 2 -> RISCVSRAI +| _ -> failwith "Unknown sop in sail translate out" let translate_out_rop op = match translate_out_enum op with | 0 -> RISCVADD @@ -69,6 +72,7 @@ let translate_out_rop op = match translate_out_enum op with | 7 -> RISCVSRA | 8 -> RISCVOR | 9 -> RISCVAND +| _ -> failwith "Unknown rop in sail translate out" let translate_out_ropw op = match translate_out_enum op with | 0 -> RISCVADDW @@ -76,3 +80,4 @@ let translate_out_ropw op = match translate_out_enum op with | 2 -> RISCVSLLW | 3 -> RISCVSRLW | 4 -> RISCVSRAW +| _ -> failwith "Unknown ropw in sail translate out" \ No newline at end of file diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail index c91a0104..5234d128 100644 --- a/risc-v/riscv.sail +++ b/risc-v/riscv.sail @@ -281,6 +281,10 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) = } in wGPR(rd, EXTS(result)) +union ast member unit EBREAK +function clause decode (0b000000000001 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(EBREAK ()) +function clause execute EBREAK = { exit () } + function clause decode _ = None end ast diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail new file mode 100644 index 00000000..1dff5064 --- /dev/null +++ b/risc-v/riscv_regfp.sail @@ -0,0 +1,81 @@ +let (vector <0, 32, inc, string >) GPRstr = + [ "x0", "x1", "x2", "x3", "x4", "x5", "x6", "x7", "x8", "x9", "x10", + "x11", "x12", "x13", "x14", "x15", "x16", "x17", "x18", "x19", "x20", + "x21", "x22", "x23", "x24", "x25", "x26", "x27", "x28", "x29", "x30", "x31" + ] + +let CIA_fp = RFull("CIA") +let NIA_fp = RFull("NIA") + +function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (instr) = { + iR := [|| ||]; + oR := [|| ||]; + aR := [|| ||]; + ik := IK_simple; + Nias := [|| NIAFP_successor ||]; + Dia := DIAFP_none; + + switch instr { + case (EBREAK) -> () + case (UTYPE ( imm, rd, op)) -> { + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + } + case (JAL ( imm, rd)) -> { + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + let (bit[64]) offset = EXTS(imm) in + Nias := [|| NIAFP_concrete_address (PC + offset) ||] + } + case (JALR ( imm, rs, rd)) -> { + if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + let (bit[64]) offset = EXTS(imm) in + Nias := [|| NIAFP_register (RFull(GPRstr[rs])) ||]; + } + case (BTYPE ( imm, rs2, rs1, op)) -> { + if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; + ik := IK_cond_branch; + let (bit[64]) offset = EXTS(imm) in + Nias := NIAFP_concrete_address(PC + offset) :: Nias; + } + case (ITYPE ( imm, rs, rd, op)) -> { + if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + } + case (SHIFTIOP ( imm, rs, rd, op)) -> { + if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + } + case (RTYPE ( rs2, rs1, rd, op)) -> { + if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + } + case (LOAD ( imm, rs, rd, unsign, width)) -> { (* XXX "unsigned" causes name conflict in lem shallow embedding... *) + if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + aR := iR; + ik := IK_mem_read (Read_plain); + } + case (STORE( imm, rs2, rs1, width)) -> { + if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; + if (rs1 == 0) then () else aR := RFull(GPRstr[rs1]) :: aR; + ik := IK_mem_write (Write_plain); + } + case (ADDIW ( imm, rs, rd)) -> { + if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + } + case (SHIFTW ( imm, rs, rd, op)) -> { + if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + } + case (RTYPEW ( rs2, rs1, rd, op))-> { + if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; + if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; + } + }; + (iR,oR,aR,Nias,Dia,ik) +} -- cgit v1.2.3 From 73965da84487d06066eae4b9b5fa49da8d123d7b Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 12 Aug 2017 19:04:58 +0100 Subject: Fix compilation issue for 32-bit systems --- src/type_internal.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/type_internal.ml b/src/type_internal.ml index 155e78f4..ddf0b692 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1901,8 +1901,8 @@ let int8_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 7) (big_int_o TA_nexp (mk_c_int 127)])} let int16_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 15) (big_int_of_int 32768))); TA_nexp (mk_c_int 32767)])} -let int32_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 31) (big_int_of_int 2147483648))) ; - TA_nexp (mk_c_int 2147483647)])} +let int32_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 31) (big_int_of_string "2147483648"))) ; + TA_nexp (mk_c (big_int_of_string "2147483647"))])} let int64_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 63) (big_int_of_string "9223372036854775808"))); TA_nexp (mk_c (big_int_of_string "9223372036854775807"))])} -- cgit v1.2.3 From 44850d32e227647813b44a8c97c4de57cd7a9978 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 12 Aug 2017 19:05:32 +0100 Subject: Resolve ambiguity between negation of integers and bools --- src/gen_lib/sail_values.lem | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 38f7d512..49f37381 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -266,7 +266,7 @@ let hardware_quot (a:integer) (b:integer) : integer = if ((a<0) = (b<0)) then q (* same sign -- result positive *) else - ~q (* different sign -- result negative *) + integerNegate q (* different sign -- result negative *) let quot_signed = hardware_quot @@ -956,4 +956,3 @@ let diafp_to_dia reginfo = function | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v) | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r) end - -- cgit v1.2.3 From 1a94f80b5d518e9d79daf9b253331d5b7936761f Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 14 Aug 2017 12:22:21 +0100 Subject: add risc-v fence instruction as re-using MIPS sync for now. Also place holders for FENCE.I and ECALL. --- risc-v/hgen/ast.hgen | 1 + risc-v/hgen/herdtools_ast_to_shallow_ast.hgen | 4 ++++ risc-v/hgen/herdtools_types_to_shallow_types.hgen | 3 +++ risc-v/hgen/lexer.hgen | 1 + risc-v/hgen/parser.hgen | 2 ++ risc-v/hgen/pretty.hgen | 1 + risc-v/hgen/sail_trans_out.hgen | 1 + risc-v/hgen/shallow_ast_to_herdtools_ast.hgen | 1 + risc-v/hgen/token_types.hgen | 1 + risc-v/hgen/tokens.hgen | 2 +- risc-v/hgen/trans_sail.hgen | 2 +- risc-v/riscv.sail | 16 ++++++++++++++++ risc-v/riscv_regfp.sail | 5 ++++- 13 files changed, 37 insertions(+), 3 deletions(-) diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen index 62e7cf4b..2860484e 100644 --- a/risc-v/hgen/ast.hgen +++ b/risc-v/hgen/ast.hgen @@ -10,3 +10,4 @@ | `RISCVADDIW of bit12 * reg * reg | `RISCVSHIFTW of bit5 * reg * reg * riscvSop | `RISCVRTYPEW of reg * reg * reg * riscvRopw +| `RISCVFENCE diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen index ac6f22bd..46b11310 100644 --- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen +++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen @@ -55,3 +55,7 @@ translate_reg "rs1" rs1, translate_reg "rd" rd, translate_ropw op) +| `RISCVFENCE -> FENCE ( + translate_imm4 "pred" 0, + translate_imm4 "succ" 0 +) diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen index c4a1fd37..c15b3f94 100644 --- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen +++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen @@ -69,3 +69,6 @@ let translate_imm6 name 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_imm4 name value = + Sail_values.to_vec0 is_inc (Nat_big_num.of_int 4,Nat_big_num.of_int value) diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen index 75d890e4..1888d42b 100644 --- a/risc-v/hgen/lexer.hgen +++ b/risc-v/hgen/lexer.hgen @@ -58,3 +58,4 @@ "srlw", RTYPEW{op=RISCVSRLW}; "sraw", RTYPEW{op=RISCVSRAW}; +"fence", FENCE (); diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen index abd87c7f..ba780857 100644 --- a/risc-v/hgen/parser.hgen +++ b/risc-v/hgen/parser.hgen @@ -22,3 +22,5 @@ { `RISCVSHIFTW ($6, $4, $2, $1.op) } | RTYPEW reg COMMA reg COMMA reg { `RISCVRTYPEW ($6, $4, $2, $1.op) } +| FENCE + { `RISCVFENCE } diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen index 0587c321..d8572ae2 100644 --- a/risc-v/hgen/pretty.hgen +++ b/risc-v/hgen/pretty.hgen @@ -12,3 +12,4 @@ | `RISCVADDIW(imm, rs, rd) -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm | `RISCVSHIFTW(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm | `RISCVRTYPEW(rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2) +| `RISCVFENCE -> "fence" diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen index 7f1ae8ea..a9d3159c 100644 --- a/risc-v/hgen/sail_trans_out.hgen +++ b/risc-v/hgen/sail_trans_out.hgen @@ -11,3 +11,4 @@ | ("ADDIW", [imm; rs; rd]) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) | ("SHIFTW", [imm; rs; rd; op]) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) | ("RTYPEW", [rs2; rs1; rd; op]) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op) +| ("FENCE", []) -> `RISCVFENCE diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen index 9dc80a98..9278b92e 100644 --- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen +++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen @@ -11,3 +11,4 @@ | ADDIW( imm, rs, rd) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) | SHIFTW( imm, rs, rd, op) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) | RTYPEW( rs2, rs1, rd, op) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op) +| FENCE(pred, succ) -> `RISCVFENCE diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen index cc993ae3..e778d2a9 100644 --- a/risc-v/hgen/token_types.hgen +++ b/risc-v/hgen/token_types.hgen @@ -10,3 +10,4 @@ type token_Store = {width : wordWidth } type token_ADDIW = unit type token_SHIFTW = {op : riscvSop } type token_RTYPEW = {op : riscvRopw } +type token_FENCE = unit diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen index 0a874b81..abe6a6c3 100644 --- a/risc-v/hgen/tokens.hgen +++ b/risc-v/hgen/tokens.hgen @@ -10,4 +10,4 @@ %token ADDIW %token SHIFTW %token RTYPEW - +%token FENCE diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen index fd51c81f..c2e3138b 100644 --- a/risc-v/hgen/trans_sail.hgen +++ b/risc-v/hgen/trans_sail.hgen @@ -103,4 +103,4 @@ translate_ropw "op" op; ], []) - +| `RISCVFENCE -> ("FENCE", [], []) diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail index 5234d128..e464c5f7 100644 --- a/risc-v/riscv.sail +++ b/risc-v/riscv.sail @@ -55,6 +55,7 @@ function unit wGPR((regno) r, (regval) v) = val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval +val extern unit -> unit effect { barr } MEM_sync (* Ideally these would be sail builtin *) function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) = @@ -281,10 +282,25 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) = } in wGPR(rd, EXTS(result)) +union ast member (bit[4], bit[4]) FENCE +function clause decode (0b0000 : (bit[4]) pred : (bit[4]) succ : 0b00000 : 0b000 : 0b00000 : 0b0001111) = Some(FENCE (pred, succ)) +function clause execute (FENCE(pred, succ)) = { + MEM_sync(); (* XXX use pred and succ *) +} + +union ast member unit FENCEI +function clause decode (0b0000 : 0b0000 : 0b0000 : 0b00000 : 0b001 : 0b00000 : 0b0001111) = Some(FENCEI) +function clause execute FENCEI = () (* XXX TODO *) + +union ast member unit ECALL +function clause decode (0b000000000000 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(ECALL ()) +function clause execute ECALL = () + union ast member unit EBREAK function clause decode (0b000000000001 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(EBREAK ()) function clause execute EBREAK = { exit () } + function clause decode _ = None end ast diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail index 1dff5064..0c7a67d8 100644 --- a/risc-v/riscv_regfp.sail +++ b/risc-v/riscv_regfp.sail @@ -29,7 +29,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; let (bit[64]) offset = EXTS(imm) in - Nias := [|| NIAFP_register (RFull(GPRstr[rs])) ||]; + Nias := [|| NIAFP_register (RFull(GPRstr[rs])) ||]; (* XXX this should br rs + offset... *) } case (BTYPE ( imm, rs2, rs1, op)) -> { if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR; @@ -76,6 +76,9 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; } + case (FENCE(pred, succ)) -> { + ik := IK_barrier (Barrier_MIPS_SYNC); + } }; (iR,oR,aR,Nias,Dia,ik) } -- cgit v1.2.3 From e8dcc8ab28d2d7b7764db95ba611b4d64b5bdade Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 15 Aug 2017 13:04:34 +0100 Subject: riscv: limit stores to only relevant bytes. --- risc-v/riscv.sail | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail index e464c5f7..01fcbdc4 100644 --- a/risc-v/riscv.sail +++ b/risc-v/riscv.sail @@ -236,9 +236,9 @@ function clause execute (STORE(imm, rs2, rs1, width)) = }; let rs2_val = rGPR(rs2) in switch (width) { - case BYTE -> MEMval(addr, 1, rs2_val) - case WORD -> MEMval(addr, 2, rs2_val) - case HALF -> MEMval(addr, 4, rs2_val) + case BYTE -> MEMval(addr, 1, rs2_val[7..0]) + case WORD -> MEMval(addr, 2, rs2_val[15..0]) + case HALF -> MEMval(addr, 4, rs2_val[31..0]) case DOUBLE -> MEMval(addr, 8, rs2_val) } } -- cgit v1.2.3 From e94a22447236cfb4f7e82516b1a9abcdfaf5c419 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 15 Aug 2017 13:30:44 +0100 Subject: riscv: fix word/half backwards in load. --- risc-v/riscv.sail | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail index 01fcbdc4..1a5a3b33 100644 --- a/risc-v/riscv.sail +++ b/risc-v/riscv.sail @@ -208,15 +208,15 @@ function clause execute(LOAD(imm, rs1, rd, unsigned, width)) = let (bit[64]) result = if unsigned then switch (width) { case BYTE -> EXTZ(MEMr(addr, 1)) - case WORD -> EXTZ(MEMr(addr, 2)) - case HALF -> EXTZ(MEMr(addr, 4)) + case HALF -> EXTZ(MEMr(addr, 2)) + case WORD -> EXTZ(MEMr(addr, 4)) case DOUBLE -> MEMr(addr, 8) } else switch (width) { case BYTE -> EXTS(MEMr(addr, 1)) - case WORD -> EXTS(MEMr(addr, 2)) - case HALF -> EXTS(MEMr(addr, 4)) + case HALF -> EXTS(MEMr(addr, 2)) + case WORD -> EXTS(MEMr(addr, 4)) case DOUBLE -> MEMr(addr, 8) } in wGPR(rd, result) @@ -230,15 +230,15 @@ function clause execute (STORE(imm, rs2, rs1, width)) = let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in { switch (width) { case BYTE -> MEMea(addr, 1) - case WORD -> MEMea(addr, 2) - case HALF -> MEMea(addr, 4) + case HALF -> MEMea(addr, 2) + case WORD -> MEMea(addr, 4) case DOUBLE -> MEMea(addr, 8) }; let rs2_val = rGPR(rs2) in switch (width) { case BYTE -> MEMval(addr, 1, rs2_val[7..0]) - case WORD -> MEMval(addr, 2, rs2_val[15..0]) - case HALF -> MEMval(addr, 4, rs2_val[31..0]) + case HALF -> MEMval(addr, 2, rs2_val[15..0]) + case WORD -> MEMval(addr, 4, rs2_val[31..0]) case DOUBLE -> MEMval(addr, 8, rs2_val) } } -- cgit v1.2.3 From bd47f6cea664ebb6cfd57ca405dfd4c298824b0b Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 15 Aug 2017 13:31:30 +0100 Subject: fix incorrect mnemonic for lui --- risc-v/hgen/lexer.hgen | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen index 1888d42b..3badc338 100644 --- a/risc-v/hgen/lexer.hgen +++ b/risc-v/hgen/lexer.hgen @@ -1,4 +1,4 @@ -"lwu" , UTYPE { op=RISCVLUI }; +"lui" , UTYPE { op=RISCVLUI }; "auipc" , UTYPE { op=RISCVAUIPC }; "jal", JAL (); -- cgit v1.2.3 From 1b930fe485256d2ea93690a190132878b6365016 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 15 Aug 2017 13:32:22 +0100 Subject: riscv: fix incorrect argument order for store parser. --- risc-v/hgen/parser.hgen | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen index ba780857..8bb8ae2b 100644 --- a/risc-v/hgen/parser.hgen +++ b/risc-v/hgen/parser.hgen @@ -15,7 +15,7 @@ | LOAD reg COMMA NUM LPAR reg RPAR { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width) } | STORE reg COMMA NUM LPAR reg RPAR - { `RISCVStore($4, $6, $2, $1.width) } + { `RISCVStore($4, $2, $6, $1.width) } | ADDIW reg COMMA reg COMMA NUM { `RISCVADDIW ($6, $4, $2) } | SHIFTW reg COMMA reg COMMA NUM -- cgit v1.2.3 From 1b50e19509d43c2ea27aecd76e1652c1e05482d8 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 15 Aug 2017 13:32:38 +0100 Subject: better names for store parameters. --- risc-v/hgen/trans_sail.hgen | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen index c2e3138b..4275670c 100644 --- a/risc-v/hgen/trans_sail.hgen +++ b/risc-v/hgen/trans_sail.hgen @@ -68,12 +68,12 @@ translate_width "width" width; ], []) -| `RISCVStore(imm, rs, rd, width) -> +| `RISCVStore(imm, rs2, rs1, width) -> ("STORE", [ translate_imm12 "imm" imm; - translate_reg "rs" rs; - translate_reg "rd" rd; + translate_reg "rs2" rs2; + translate_reg "rs1" rs1; translate_width "width" width; ], []) -- cgit v1.2.3 From 753d80d0527d6c334c70ff41a9857f86fc773d59 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 15 Aug 2017 13:57:44 +0100 Subject: riscv: include pred and succ fields in translation of FENCE (currently hard coded to zero --- risc-v/hgen/trans_sail.hgen | 8 +++++++- risc-v/hgen/types_trans_sail.hgen | 2 ++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen index 4275670c..28a4f4ba 100644 --- a/risc-v/hgen/trans_sail.hgen +++ b/risc-v/hgen/trans_sail.hgen @@ -103,4 +103,10 @@ translate_ropw "op" op; ], []) -| `RISCVFENCE -> ("FENCE", [], []) +| `RISCVFENCE -> + ("FENCE", + [ + translate_imm4 "pred" 0; + translate_imm4 "succ" 0; + ], + []) diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen index 9dd36d5e..4dc7707e 100644 --- a/risc-v/hgen/types_trans_sail.hgen +++ b/risc-v/hgen/types_trans_sail.hgen @@ -29,5 +29,7 @@ let translate_imm6 name value = (name, Bvector (Some 6), bit_list_of_integer 6 (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_imm4 name value = + (name, Bvector (Some 4), bit_list_of_integer 4 (Nat_big_num.of_int value)) let translate_bool name value = (name, Bit, [if value then Bitc_one else Bitc_zero]) -- cgit v1.2.3 From 6b51abc19b5af4051f53be9de3cf07f311d193c1 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 15 Aug 2017 16:18:30 +0100 Subject: remove unneeded regs_out_in.hgen files. --- mips/hgen/regs_out_in.hgen | 5 ----- risc-v/hgen/regs_out_in.hgen | 5 ----- 2 files changed, 10 deletions(-) delete mode 100644 mips/hgen/regs_out_in.hgen delete mode 100644 risc-v/hgen/regs_out_in.hgen diff --git a/mips/hgen/regs_out_in.hgen b/mips/hgen/regs_out_in.hgen deleted file mode 100644 index 8e1fd093..00000000 --- a/mips/hgen/regs_out_in.hgen +++ /dev/null @@ -1,5 +0,0 @@ -(* for each instruction instance, identify the role of the registers - and possible branching: (outputs, inputs, voidstars, branch) *) - -| `MIPSAdd -> - ([], [], [], [Next]) diff --git a/risc-v/hgen/regs_out_in.hgen b/risc-v/hgen/regs_out_in.hgen deleted file mode 100644 index 8e1fd093..00000000 --- a/risc-v/hgen/regs_out_in.hgen +++ /dev/null @@ -1,5 +0,0 @@ -(* for each instruction instance, identify the role of the registers - and possible branching: (outputs, inputs, voidstars, branch) *) - -| `MIPSAdd -> - ([], [], [], [Next]) -- cgit v1.2.3 From 1633941ba47cf87937ec0d2bfc8d840d69689f53 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 15 Aug 2017 17:21:30 +0100 Subject: riscv: store the decoded branch immediate in the ast type -- this simplifies translation to and from herdtools ast. --- risc-v/hgen/herdtools_ast_to_shallow_ast.hgen | 4 ++-- risc-v/hgen/herdtools_types_to_shallow_types.hgen | 5 +++++ risc-v/hgen/sail_trans_out.hgen | 4 ++-- risc-v/hgen/shallow_ast_to_herdtools_ast.hgen | 4 ++-- risc-v/hgen/shallow_types_to_herdtools_types.hgen | 2 ++ risc-v/hgen/trans_sail.hgen | 4 ++-- risc-v/hgen/types_sail_trans_out.hgen | 2 ++ risc-v/hgen/types_trans_sail.hgen | 6 +++++- risc-v/riscv.sail | 22 +++++++++++----------- 9 files changed, 33 insertions(+), 20 deletions(-) diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen index 46b11310..16d827e2 100644 --- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen +++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen @@ -4,14 +4,14 @@ translate_reg "rd" rd, translate_uop op) | `RISCVJAL(imm, rd) -> JAL0( - translate_imm20 "imm" imm, + translate_imm21 "imm" imm, translate_reg "rd" rd) | `RISCVJALR(imm, rs, rd) -> JALR0( translate_imm12 "imm" imm, translate_reg "rs" rd, translate_reg "rd" rd) | `RISCVBType(imm, rs2, rs1, op) -> BTYPE( - translate_imm12 "imm" imm, + translate_imm13 "imm" imm, translate_reg "rs2" rs2, translate_reg "rs1" rs1, translate_bop op) diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen index c15b3f94..361c0e61 100644 --- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen +++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen @@ -57,10 +57,15 @@ let translate_bool name = function | true -> Sail_values.B1 | false -> Sail_values.B0 +let translate_imm21 name value = + Sail_values.to_vec0 is_inc (Nat_big_num.of_int 21,Nat_big_num.of_int value) let translate_imm20 name value = Sail_values.to_vec0 is_inc (Nat_big_num.of_int 20,Nat_big_num.of_int value) +let translate_imm13 name value = + Sail_values.to_vec0 is_inc (Nat_big_num.of_int 13,Nat_big_num.of_int value) + let translate_imm12 name value = Sail_values.to_vec0 is_inc (Nat_big_num.of_int 12,Nat_big_num.of_int value) diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen index a9d3159c..6073242e 100644 --- a/risc-v/hgen/sail_trans_out.hgen +++ b/risc-v/hgen/sail_trans_out.hgen @@ -1,8 +1,8 @@ | ("EBREAK", []) -> `RISCVStopFetching | ("UTYPE", [imm; rd; op]) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op) -| ("JAL", [imm; rd]) -> `RISCVJAL(translate_out_simm20 imm, translate_out_ireg rd) +| ("JAL", [imm; rd]) -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg rd) | ("JALR", [imm; rs; rd]) -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) -| ("BTYPE", [imm; rs2; rs1; op]) -> `RISCVBType(translate_out_simm12 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op) +| ("BTYPE", [imm; rs2; rs1; op]) -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op) | ("ITYPE", [imm; rs1; rd; op]) -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op) | ("SHIFTIOP", [imm; rs; rd; op]) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) | ("RTYPE", [rs2; rs1; rd; op]) -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op) diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen index 9278b92e..da9047a3 100644 --- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen +++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen @@ -1,8 +1,8 @@ | EBREAK -> `RISCVStopFetching | UTYPE( imm, rd, op) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op) -| JAL0( imm, rd) -> `RISCVJAL(translate_out_simm20 imm, translate_out_ireg rd) +| JAL0( imm, rd) -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg rd) | JALR0( imm, rs, rd) -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) -| BTYPE( imm, rs2, rs1, op) -> `RISCVBType(translate_out_simm12 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op) +| BTYPE( imm, rs2, rs1, op) -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op) | ITYPE( imm, rs1, rd, op) -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op) | SHIFTIOP( imm, rs, rd, op) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) | RTYPE( rs2, rs1, rd, op) -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op) diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen index d635efde..8ef18f06 100644 --- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen +++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen @@ -64,7 +64,9 @@ let translate_out_bool = function | Sail_values.B0 -> false | _ -> failwith "translate_out_bool Undef" +let translate_out_simm21 imm = translate_out_signed_int imm 21 let translate_out_simm20 imm = translate_out_signed_int imm 20 +let translate_out_simm13 imm = translate_out_signed_int imm 13 let translate_out_simm12 imm = translate_out_signed_int imm 12 let translate_out_imm6 imm = translate_out_int imm let translate_out_imm5 imm = translate_out_int imm diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen index 28a4f4ba..c72e84d5 100644 --- a/risc-v/hgen/trans_sail.hgen +++ b/risc-v/hgen/trans_sail.hgen @@ -10,7 +10,7 @@ | `RISCVJAL(imm, rd) -> ("JAL", [ - translate_imm20 "imm" imm; + translate_imm21 "imm" imm; translate_reg "rd" rd; ], []) @@ -25,7 +25,7 @@ | `RISCVBType(imm, rs2, rs1, op) -> ("BTYPE", [ - translate_imm12 "imm" imm; + translate_imm13 "imm" imm; translate_reg "rs2" rs2; translate_reg "rs1" rs1; translate_bop "op" op; diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen index e034cf37..297d0cf3 100644 --- a/risc-v/hgen/types_sail_trans_out.hgen +++ b/risc-v/hgen/types_sail_trans_out.hgen @@ -11,7 +11,9 @@ let translate_out_signed_int inst bits = let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg)) +let translate_out_simm21 imm = translate_out_signed_int imm 21 let translate_out_simm20 imm = translate_out_signed_int imm 20 +let translate_out_simm13 imm = translate_out_signed_int imm 13 let translate_out_simm12 imm = translate_out_signed_int imm 12 let translate_out_imm6 imm = translate_out_int imm let translate_out_imm5 imm = translate_out_int imm diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen index 4dc7707e..1bf174fa 100644 --- a/risc-v/hgen/types_trans_sail.hgen +++ b/risc-v/hgen/types_trans_sail.hgen @@ -19,10 +19,14 @@ let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW; let translate_width = translate_enum [RISCVBYTE; RISCVHALF; RISCVWORD; RISCVDOUBLE] 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_imm21 name value = + (name, Bvector (Some 21), bit_list_of_integer 21 (Nat_big_num.of_int value)) let translate_imm20 name value = - (name, Bvector (Some 26), bit_list_of_integer 26 (Nat_big_num.of_int value)) + (name, Bvector (Some 20), bit_list_of_integer 20 (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_imm13 name value = + (name, Bvector (Some 13), bit_list_of_integer 13 (Nat_big_num.of_int value)) let translate_imm12 name value = (name, Bvector (Some 12), bit_list_of_integer 12 (Nat_big_num.of_int value)) let translate_imm6 name value = diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail index 1a5a3b33..962d8280 100644 --- a/risc-v/riscv.sail +++ b/risc-v/riscv.sail @@ -95,10 +95,10 @@ function clause execute (UTYPE(imm, rd, op)) = } in wGPR(rd, ret) -union ast member ((bit[20]), regno) JAL -function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm, rd)) +union ast member ((bit[21]), regno) JAL +function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0, rd)) function clause execute (JAL(imm, rd)) = - let (bit[64]) offset = EXTS(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0) in { + let (bit[64]) offset = EXTS(imm) in { nextPC := PC + offset; wGPR(rd, PC + 4); } @@ -112,13 +112,13 @@ function clause execute (JALR(imm, rs1, rd)) = wGPR(rd, PC + 4); } -union ast member ((bit[12]), regno, regno, bop) BTYPE -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BEQ)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BNE)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLT)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGE)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLTU)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGEU)) +union ast member ((bit[13]), regno, regno, bop) BTYPE +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BEQ)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BNE)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLT)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGE)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLTU)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGEU)) function clause execute (BTYPE(imm, rs2, rs1, op)) = let rs1_val = rGPR(rs1) in @@ -132,7 +132,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = case BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *) } in if (taken) then - nextPC := PC + EXTS(imm : 0b0) + nextPC := PC + EXTS(imm) union ast member ((bit[12]), regno, regno, iop) ITYPE function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ADDI)) -- cgit v1.2.3 From f69a7427e953504990f5eb47a260db7de1aa6201 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 16 Aug 2017 09:40:17 +0100 Subject: riscv: fix back to front args in store pretty print. --- risc-v/hgen/pretty.hgen | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen index d8572ae2..0373783d 100644 --- a/risc-v/hgen/pretty.hgen +++ b/risc-v/hgen/pretty.hgen @@ -8,7 +8,7 @@ | `RISCVShiftIop(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm | `RISCVRType (rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_rop op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2) | `RISCVLoad(imm, rs, rd, unsigned, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width)) (pp_reg rd) imm (pp_reg rs) -| `RISCVStore(imm, rs, rd, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op width) (pp_reg rd) imm (pp_reg rs) +| `RISCVStore(imm, rs2, rs1, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op width) (pp_reg rs2) imm (pp_reg rs1) | `RISCVADDIW(imm, rs, rd) -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm | `RISCVSHIFTW(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm | `RISCVRTYPEW(rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2) -- cgit v1.2.3 From e62c1e3615d1c0b54afcd88bf0938b92f1408f13 Mon Sep 17 00:00:00 2001 From: Jon French Date: Wed, 16 Aug 2017 09:51:53 +0100 Subject: lem_interp: remove broken val_to_string_internal functions, replace with string_of_value as used everywhere else --- src/lem_interp/pretty_interp.ml | 32 +------------------------ src/lem_interp/printing_functions.ml | 3 +-- src/lem_interp/printing_functions.mli | 1 - src/lem_interp/run_interp.ml | 45 +++++++---------------------------- 4 files changed, 11 insertions(+), 70 deletions(-) diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index a51598b3..9f1ea3e3 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -127,36 +127,6 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu ;; -let rec val_to_string_internal ((Interp.LMem (_,_,memory,_)) as mem) = function - | Interp_ast.V_boxref(n, t) -> val_to_string_internal mem (Pmap.find n memory) - | Interp_ast.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l) - | Interp_ast.V_tuple l -> - let repr = String.concat ", " (List.map (val_to_string_internal mem) l) in - sprintf "(%s)" repr - | Interp_ast.V_list l -> - let repr = String.concat "; " (List.map (val_to_string_internal mem) l) in - sprintf "[||%s||]" repr - | Interp_ast.V_vector (first_index, inc, l) -> - let last_index = (if (Interp_ast.IInc = inc) then List.length l - 1 else 1 - List.length l) + first_index in - let repr = - try bitvec_to_string l - with Failure _ -> - sprintf "[%s]" (String.concat "; " (List.map (val_to_string_internal mem) l)) in - sprintf "%s [%s..%s]" repr (string_of_int first_index) (string_of_int last_index) - | (Interp_ast.V_vector_sparse(first_index,last_index,inc,l,default) as v) -> - val_to_string_internal mem (Interp_lib.fill_in_sparse v) - | Interp_ast.V_record(_, l) -> - let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal mem value) in - let repr = String.concat "; " (List.map pp l) in - sprintf "{%s}" repr - | Interp_ast.V_ctor (id,_,_, value) -> - sprintf "%s %s" (id_to_string id) (val_to_string_internal mem value) - | Interp_ast.V_register _ | Interp_ast.V_register_alias _ -> - sprintf "reg-as-value" - | Interp_ast.V_unknown -> "unknown" - | Interp_ast.V_track(v,rs) -> (*"tainted by {" ^ (Interp_utilities.list_to_string Interp.string_of_reg_form "," rs) ^ "} --" ^ *) (val_to_string_internal mem v) -;; - (**************************************************************************** * PPrint-based source-to-source pretty printer ****************************************************************************) @@ -582,7 +552,7 @@ let doc_exp, doc_let = (* XXX missing case *) | E_comment _ | E_comment_struc _ -> string "" | E_internal_value v -> - string (val_to_string_internal mem v) + string (Interp.string_of_value v) | _-> failwith "internal expression escaped" and let_exp env mem add_red show_hole_contents (LB_aux(lb,_)) = match lb with diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index 79a86113..a19256a2 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -49,7 +49,6 @@ open Interp_interface ;; open Nat_big_num ;; -let val_to_string_internal = Pretty_interp.val_to_string_internal ;; let lit_to_string = Pretty_interp.lit_to_string ;; let id_to_string = Pretty_interp.id_to_string ;; let loc_to_string = Pretty_interp.loc_to_string ;; @@ -451,7 +450,7 @@ let local_variables_to_string (IState(stack,_)) = String.concat ", " (option_map (fun (id,value)-> match id with | "0" -> None (*Let's not print out the context hole again*) - | _ -> Some (id ^ "=" ^ val_to_string_internal mem value)) (Pmap.bindings_list env)) + | _ -> Some (id ^ "=" ^ Interp.string_of_value value)) (Pmap.bindings_list env)) let instr_parm_to_string (name, typ, value) = name ^"="^ diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli index 85744d61..f1a0cd4a 100644 --- a/src/lem_interp/printing_functions.mli +++ b/src/lem_interp/printing_functions.mli @@ -10,7 +10,6 @@ val loc_to_string : l -> string val get_loc : tannot exp -> string (*interp_interface.value to string*) val reg_value_to_string : register_value -> string -val val_to_string_internal : Interp.lmem -> Interp_ast.value -> string (*(*Force all representations to hex strings instead of a mixture of hex and binary strings*) val val_to_hex_string : value0 -> string*) diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml index 6f5ca07a..f61d9aaf 100644 --- a/src/lem_interp/run_interp.ml +++ b/src/lem_interp/run_interp.ml @@ -114,33 +114,6 @@ let rec reg_to_string = function | SubReg (id,r,_) -> sprintf "%s.%s" (reg_to_string r) (id_to_string id) ;; -let rec val_to_string_internal = function - | V_boxref(n, t) -> sprintf "boxref %d" n - | V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l) - | V_tuple l -> - let repr = String.concat ", " (List.map val_to_string_internal l) in - sprintf "(%s)" repr - | V_list l -> - let repr = String.concat "; " (List.map val_to_string_internal l) in - sprintf "[||%s||]" repr - | V_vector (first_index, inc, l) -> - let last_index = add_int_big_int (if inc then List.length l - 1 else 1 - List.length l) first_index in - let repr = - try bitvec_to_string (* (if inc then l else List.rev l)*) l - with Failure _ -> - sprintf "[%s]" (String.concat "; " (List.map val_to_string_internal l)) in - sprintf "%s [%s..%s]" repr (string_of_big_int first_index) (string_of_big_int last_index) - | V_record(_, l) -> - let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal value) in - let repr = String.concat "; " (List.map pp l) in - sprintf "{%s}" repr - | V_ctor (id,_, value) -> - sprintf "%s %s" (id_to_string id) (val_to_string_internal value) - | V_register r -> - sprintf "reg-as-value %s" (reg_to_string r) - | V_unknown -> "unknown" -;; - let rec top_frame_exp_state = function | Top -> raise (Invalid_argument "top_frame_exp") | Hole_frame(_, e, _, env, mem, Top) @@ -210,7 +183,7 @@ let id_compare i1 i2 = module Reg = struct include Map.Make(struct type t = id let compare = id_compare end) let to_string id v = - sprintf "%s -> %s" (id_to_string id) (val_to_string_internal v) + sprintf "%s -> %s" (id_to_string id) (string_of_value v) let find id m = (* eprintf "reg_find called with %s\n" (id_to_string id);*) let v = find id m in @@ -255,7 +228,7 @@ module Mem = struct v *) let to_string idx v = - sprintf "[%s] -> %s" (string_of_big_int idx) (val_to_string_internal v) + sprintf "[%s] -> %s" (string_of_big_int idx) (string_of_value v) end ;; @@ -412,7 +385,7 @@ let run in let rec loop mode env = function | Value v -> - debugf "%s: %s %s\n" (grey name) (blue "return") (val_to_string_internal v); + debugf "%s: %s %s\n" (grey name) (blue "return") (string_of_value v); true, mode, env | Action (a, s) -> let (top_exp,(top_env,top_mem)) = top_frame_exp_state s in @@ -429,25 +402,25 @@ let run let left = "<-" and right = "->" in let (mode',env',s) = begin match a with | Read_reg (reg, sub) -> - show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (val_to_string_internal return); + show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (string_of_value return); step (),env',s | Write_reg (reg, sub, value) -> assert (return = unit_lit); - show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (val_to_string_internal value); + show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (string_of_value value); step (),env',s | Read_mem (id, args, sub) -> - show "read_mem" (id_to_string id ^ val_to_string_internal args ^ sub_to_string sub) right (val_to_string_internal return); + show "read_mem" (id_to_string id ^ string_of_value args ^ sub_to_string sub) right (string_of_value return); step (),env',s | Write_mem (id, args, sub, value) -> assert (return = unit_lit); - show "write_mem" (id_to_string id ^ val_to_string_internal args ^ sub_to_string sub) left (val_to_string_internal value); + show "write_mem" (id_to_string id ^ string_of_value args ^ sub_to_string sub) left (string_of_value value); step (),env',s (* distinguish single argument for pretty-printing *) | Call_extern (f, (V_tuple _ as args)) -> - show "call_lib" (f ^ val_to_string_internal args) right (val_to_string_internal return); + show "call_lib" (f ^ string_of_value args) right (string_of_value return); step (),env',s | Call_extern (f, arg) -> - show "call_lib" (sprintf "%s(%s)" f (val_to_string_internal arg)) right (val_to_string_internal return); + show "call_lib" (sprintf "%s(%s)" f (string_of_value arg)) right (string_of_value return); step (),env',s | Interp.Step _ -> assert (return = unit_lit); -- cgit v1.2.3 From c6d639e0f03053b905a9cb0ab6929f4efe6153f4 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 17 Aug 2017 09:28:35 +0100 Subject: fixed the RISC-V fences (3 types: "rw,rw"/"r,rw"/"rw,w") --- risc-v/hgen/ast.hgen | 2 +- risc-v/hgen/herdtools_ast_to_shallow_ast.hgen | 7 +++---- risc-v/hgen/herdtools_types_to_shallow_types.hgen | 2 +- risc-v/hgen/lexer.hgen | 3 +++ risc-v/hgen/parser.hgen | 14 ++++++++++++-- risc-v/hgen/pretty.hgen | 2 +- risc-v/hgen/sail_trans_out.hgen | 2 +- risc-v/hgen/shallow_ast_to_herdtools_ast.hgen | 2 +- risc-v/hgen/shallow_types_to_herdtools_types.hgen | 1 + risc-v/hgen/token_types.hgen | 2 ++ risc-v/hgen/tokens.hgen | 3 ++- risc-v/hgen/trans_sail.hgen | 6 +++--- risc-v/hgen/types.hgen | 7 +++++++ risc-v/hgen/types_sail_trans_out.hgen | 3 ++- risc-v/riscv.sail | 16 ++++++++++++++-- risc-v/riscv_extras.lem | 6 ++++-- risc-v/riscv_extras_embed.lem | 8 ++++++-- risc-v/riscv_extras_embed_sequential.lem | 9 ++++++--- src/lem_interp/sail_impl_base.lem | 5 +++++ 19 files changed, 75 insertions(+), 25 deletions(-) diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen index 2860484e..8983b5ae 100644 --- a/risc-v/hgen/ast.hgen +++ b/risc-v/hgen/ast.hgen @@ -10,4 +10,4 @@ | `RISCVADDIW of bit12 * reg * reg | `RISCVSHIFTW of bit5 * reg * reg * riscvSop | `RISCVRTYPEW of reg * reg * reg * riscvRopw -| `RISCVFENCE +| `RISCVFENCE of bit4 * bit4 diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen index 16d827e2..50026612 100644 --- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen +++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen @@ -55,7 +55,6 @@ translate_reg "rs1" rs1, translate_reg "rd" rd, translate_ropw op) -| `RISCVFENCE -> FENCE ( - translate_imm4 "pred" 0, - translate_imm4 "succ" 0 -) +| `RISCVFENCE(pred, succ) -> FENCE( + translate_imm4 "pred" pred, + translate_imm4 "succ" succ) diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen index 361c0e61..4d8bd87a 100644 --- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen +++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen @@ -75,5 +75,5 @@ let translate_imm6 name 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_imm4 name value = +let translate_imm4 name value = Sail_values.to_vec0 is_inc (Nat_big_num.of_int 4,Nat_big_num.of_int value) diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen index 3badc338..5f2c8326 100644 --- a/risc-v/hgen/lexer.hgen +++ b/risc-v/hgen/lexer.hgen @@ -59,3 +59,6 @@ "sraw", RTYPEW{op=RISCVSRAW}; "fence", FENCE (); +"r", FENCEOPTION Fence_R; +"w", FENCEOPTION Fence_W; +"rw", FENCEOPTION Fence_RW; diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen index 8bb8ae2b..37fd8d8d 100644 --- a/risc-v/hgen/parser.hgen +++ b/risc-v/hgen/parser.hgen @@ -22,5 +22,15 @@ { `RISCVSHIFTW ($6, $4, $2, $1.op) } | RTYPEW reg COMMA reg COMMA reg { `RISCVRTYPEW ($6, $4, $2, $1.op) } -| FENCE - { `RISCVFENCE } +| FENCE FENCEOPTION COMMA FENCEOPTION + { match ($2, $4) with + | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011) + | (Fence_R, Fence_RW) -> `RISCVFENCE (0b0010, 0b0011) + | (Fence_RW, Fence_W) -> `RISCVFENCE (0b0011, 0b0001) + | (Fence_RW, Fence_R) -> failwith "'fence rw,r' is not supported" + | (Fence_R, Fence_R) -> failwith "'fence r,r' is not supported" + | (Fence_R, Fence_W) -> failwith "'fence r,w' is not supported" + | (Fence_W, Fence_RW) -> failwith "'fence w,rw' is not supported" + | (Fence_W, Fence_R) -> failwith "'fence w,r' is not supported" + | (Fence_W, Fence_W) -> failwith "'fence w,w' is not supported" + } diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen index 0373783d..1da3ef11 100644 --- a/risc-v/hgen/pretty.hgen +++ b/risc-v/hgen/pretty.hgen @@ -12,4 +12,4 @@ | `RISCVADDIW(imm, rs, rd) -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm | `RISCVSHIFTW(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm | `RISCVRTYPEW(rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2) -| `RISCVFENCE -> "fence" +| `RISCVFENCE(pred, succ) -> sprintf "fence %s, %s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ) diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen index 6073242e..dca5bea1 100644 --- a/risc-v/hgen/sail_trans_out.hgen +++ b/risc-v/hgen/sail_trans_out.hgen @@ -11,4 +11,4 @@ | ("ADDIW", [imm; rs; rd]) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) | ("SHIFTW", [imm; rs; rd; op]) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) | ("RTYPEW", [rs2; rs1; rd; op]) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op) -| ("FENCE", []) -> `RISCVFENCE +| ("FENCE", [pred; succ]) -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ) diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen index da9047a3..6158ebd7 100644 --- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen +++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen @@ -11,4 +11,4 @@ | ADDIW( imm, rs, rd) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) | SHIFTW( imm, rs, rd, op) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) | RTYPEW( rs2, rs1, rd, op) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op) -| FENCE(pred, succ) -> `RISCVFENCE +| FENCE( pred, succ) -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ) diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen index 8ef18f06..a891d7d0 100644 --- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen +++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen @@ -70,3 +70,4 @@ let translate_out_simm13 imm = translate_out_signed_int imm 13 let translate_out_simm12 imm = translate_out_signed_int imm 12 let translate_out_imm6 imm = translate_out_int imm let translate_out_imm5 imm = translate_out_int imm +let translate_out_imm4 imm = translate_out_int imm diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen index e778d2a9..2980b985 100644 --- a/risc-v/hgen/token_types.hgen +++ b/risc-v/hgen/token_types.hgen @@ -11,3 +11,5 @@ type token_ADDIW = unit type token_SHIFTW = {op : riscvSop } type token_RTYPEW = {op : riscvRopw } type token_FENCE = unit + +type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen index abe6a6c3..f952cf77 100644 --- a/risc-v/hgen/tokens.hgen +++ b/risc-v/hgen/tokens.hgen @@ -10,4 +10,5 @@ %token ADDIW %token SHIFTW %token RTYPEW -%token FENCE +%token FENCE +%token FENCEOPTION diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen index c72e84d5..df22d9dc 100644 --- a/risc-v/hgen/trans_sail.hgen +++ b/risc-v/hgen/trans_sail.hgen @@ -103,10 +103,10 @@ translate_ropw "op" op; ], []) -| `RISCVFENCE -> +| `RISCVFENCE(pred, succ) -> ("FENCE", [ - translate_imm4 "pred" 0; - translate_imm4 "succ" 0; + translate_imm4 "pred" pred; + translate_imm4 "succ" succ; ], []) diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen index e31b11f8..87fc9b95 100644 --- a/risc-v/hgen/types.hgen +++ b/risc-v/hgen/types.hgen @@ -2,6 +2,7 @@ type bit20 = int type bit12 = int type bit6 = int type bit5 = int +type bit4 = int type riscvUop = (* upper immediate ops *) | RISCVLUI @@ -114,3 +115,9 @@ let pp_riscv_store_op width = match width with | RISCVWORD -> "sw" | RISCVDOUBLE -> "sd" | _ -> failwith "unexpected store op" + +let pp_riscv_fence_option = function + | 0b0011 -> "rw" + | 0b0010 -> "r" + | 0b0001 -> "w" + | _ -> failwith "unexpected fence option" diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen index 297d0cf3..e22110d0 100644 --- a/risc-v/hgen/types_sail_trans_out.hgen +++ b/risc-v/hgen/types_sail_trans_out.hgen @@ -17,6 +17,7 @@ let translate_out_simm13 imm = translate_out_signed_int imm 13 let translate_out_simm12 imm = translate_out_signed_int imm 12 let translate_out_imm6 imm = translate_out_int imm let translate_out_imm5 imm = translate_out_int imm +let translate_out_imm4 imm = translate_out_int imm let translate_out_bool = function | (name, Bit, [Bitc_one]) -> true @@ -82,4 +83,4 @@ let translate_out_ropw op = match translate_out_enum op with | 2 -> RISCVSLLW | 3 -> RISCVSRLW | 4 -> RISCVSRAW -| _ -> failwith "Unknown ropw in sail translate out" \ No newline at end of file +| _ -> failwith "Unknown ropw in sail translate out" diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail index 962d8280..4a80adb0 100644 --- a/risc-v/riscv.sail +++ b/risc-v/riscv.sail @@ -52,10 +52,17 @@ function unit wGPR((regno) r, (regval) v) = if (r != 0) then GPRs[r] := v +function forall 'a. 'a effect { escape } not_implemented((string) message) = +{ + exit message; +} + val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval -val extern unit -> unit effect { barr } MEM_sync +val extern unit -> unit effect { barr } MEM_fence_rw_rw +val extern unit -> unit effect { barr } MEM_fence_r_rw +val extern unit -> unit effect { barr } MEM_fence_rw_w (* Ideally these would be sail builtin *) function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) = @@ -285,7 +292,12 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) = union ast member (bit[4], bit[4]) FENCE function clause decode (0b0000 : (bit[4]) pred : (bit[4]) succ : 0b00000 : 0b000 : 0b00000 : 0b0001111) = Some(FENCE (pred, succ)) function clause execute (FENCE(pred, succ)) = { - MEM_sync(); (* XXX use pred and succ *) + switch(pred, succ) { + case (0b0011, 0b0011) -> MEM_fence_rw_rw() + case (0b0010, 0b0011) -> MEM_fence_r_rw() + case (0b0011, 0b0001) -> MEM_fence_rw_w() + case _ -> not_implemented("unsupported fence") + } } union ast member unit FENCEI diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem index c09c85c2..aa5d8fb8 100644 --- a/risc-v/riscv_extras.lem +++ b/risc-v/riscv_extras.lem @@ -53,6 +53,8 @@ let memory_vals : memory_write_vals = (IState (Interp.add_answer_to_stack interp bit) context))))); ] -let barrier_functions = [ - ("MEM_sync", Barrier_MIPS_SYNC); +let barrier_functions = + [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw); + ("MEM_fence_r_rw", Barrier_RISCV_r_rw); + ("MEM_fence_rw_w", Barrier_RISCV_rw_w); ] diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem index cbc8bd0d..1146d1cd 100644 --- a/risc-v/riscv_extras_embed.lem +++ b/risc-v/riscv_extras_embed.lem @@ -22,9 +22,13 @@ val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) -val MEM_sync : unit -> M unit +val MEM_fence_rw_rw : unit -> M unit +val MEM_fence_r_rw : unit -> M unit +val MEM_fence_rw_w : unit -> M unit -let MEM_sync () = barrier Barrier_Isync +let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw +let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw +let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w let duplicate (bit,len) = let bits = repeat [bit] len in diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem index 7fb62161..f6709ff7 100644 --- a/risc-v/riscv_extras_embed_sequential.lem +++ b/risc-v/riscv_extras_embed_sequential.lem @@ -23,10 +23,13 @@ val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) -val MEM_sync : unit -> M unit - -let MEM_sync () = barrier Barrier_MIPS_SYNC +val MEM_fence_rw_rw : unit -> M unit +val MEM_fence_r_rw : unit -> M unit +val MEM_fence_rw_w : unit -> M unit +let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw +let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw +let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w let duplicate (bit,len) = let bits = repeat [bit] len in diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 0cdeb414..cda6702c 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -465,6 +465,11 @@ type barrier_kind = | Barrier_TM_COMMIT (* MIPS barriers *) | Barrier_MIPS_SYNC + (* RISC-V barriers *) + | Barrier_RISCV_rw_rw + | Barrier_RISCV_r_rw + | Barrier_RISCV_rw_w + instance (Show barrier_kind) let show = function -- cgit v1.2.3