diff options
| author | Alasdair Armstrong | 2018-01-03 15:46:23 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-01-03 15:46:23 +0000 |
| commit | 90ca4e03c240675b1830a5e48cea5f6c9e412b2a (patch) | |
| tree | 55dd4be9239dd78ace165483336c5eee0200a05e | |
| parent | 4bb1e41bc2a1ae93e26094d827f43d2d21ec8223 (diff) | |
Updates to interpreter
Experimenting with porting riscv model to new typechecker
44 files changed, 453 insertions, 2522 deletions
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el index 91083c0e..7a420f14 100644 --- a/editors/sail2-mode.el +++ b/editors/sail2-mode.el @@ -5,7 +5,7 @@ (defconst sail2-keywords '("val" "function" "type" "struct" "union" "enum" "let" "var" "if" "then" - "else" "match" "in" "return" "register" "forall" "operator" "effect" + "else" "match" "in" "return" "register" "ref" "forall" "operator" "effect" "overload" "cast" "sizeof" "constraint" "default" "assert" "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "throw" "clause" "as" "repeat" "until" "while" "do" "foreach")) diff --git a/language/l2.ott b/language/l2.ott index 092d7077..ea4a8a6a 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -786,6 +786,7 @@ exp :: 'E_' ::= % this can be used to break out of for loops | exit exp :: :: exit {{ com halt all current execution }} + | ref id :: :: ref | throw exp :: :: throw | try exp catch pexp1 .. pexpn :: :: try %, potentially calling a system, trap, or interrupt handler with exp diff --git a/risc-v/Makefile b/risc-v/Makefile deleted file mode 100644 index bc46e4c2..00000000 --- a/risc-v/Makefile +++ /dev/null @@ -1,22 +0,0 @@ -SAIL:=../src/sail.native -LEM:=../../lem/lem - -SOURCES:=riscv_types.sail riscv.sail ../etc/regfp.sail riscv_regfp.sail - - -all: riscv.lem riscv.ml riscv_embed.lem - -riscv.lem: $(SOURCES) - $(SAIL) -lem_ast -o riscv $(SOURCES) - -riscv.ml: riscv.lem ../src/lem_interp/interp_ast.lem - $(LEM) -ocaml -lib ../src/lem_interp/ $< - - -riscv_embed.lem: $(SOURCES) -# also generates riscv_embed_sequential.lem, riscv_embed_types.lem, riscv_toFromInterp.lem - $(SAIL) -lem -lem_lib Riscv_extras_embed -o riscv $(SOURCES) - -clean: - rm -f riscv.lem riscv.ml - rm -f riscv_embed*.lem riscv_toFromInterp.lem diff --git a/risc-v/gen/ast.hgen b/risc-v/gen/ast.hgen deleted file mode 100644 index b1968173..00000000 --- a/risc-v/gen/ast.hgen +++ /dev/null @@ -1,17 +0,0 @@ -| `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 * bool * bool -| `RISCVStore of bit12 * reg * reg * wordWidth * bool * bool -| `RISCVADDIW of bit12 * reg * reg -| `RISCVSHIFTW of bit5 * reg * reg * riscvSop -| `RISCVRTYPEW of reg * reg * reg * riscvRopw -| `RISCVFENCE of bit4 * bit4 -| `RISCVFENCEI -| `RISCVLoadRes of bool * bool * reg * wordWidth * reg -| `RISCVStoreCon of bool * bool * reg * reg * wordWidth * reg -| `RISCVAMO of riscvAmoop * bool * bool * reg * reg * wordWidth * reg diff --git a/risc-v/gen/fold.hgen b/risc-v/gen/fold.hgen deleted file mode 100644 index 4c51e114..00000000 --- a/risc-v/gen/fold.hgen +++ /dev/null @@ -1,16 +0,0 @@ -| `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))) -| `RISCVLoadRes (_, _, rs1, _, rd) -> fold_reg rs1 (fold_reg rd (y_reg, y_sreg)) -| `RISCVStoreCon (_, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg))) -| `RISCVAMO (_, _, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg))) diff --git a/risc-v/gen/herdtools_ast_to_shallow_ast.hgen b/risc-v/gen/herdtools_ast_to_shallow_ast.hgen deleted file mode 100644 index 07c1d082..00000000 --- a/risc-v/gen/herdtools_ast_to_shallow_ast.hgen +++ /dev/null @@ -1,86 +0,0 @@ -| `RISCVStopFetching -> EBREAK -| `RISCVUTYPE(imm, rd, op) -> UTYPE( - translate_imm20 "imm" imm, - translate_reg "rd" rd, - translate_uop op) -| `RISCVJAL(imm, rd) -> RISCV_JAL( - translate_imm21 "imm" imm, - translate_reg "rd" rd) -| `RISCVJALR(imm, rs, rd) -> RISCV_JALR( - translate_imm12 "imm" imm, - translate_reg "rs" rd, - translate_reg "rd" rd) -| `RISCVBType(imm, rs2, rs1, op) -> BTYPE( - translate_imm13 "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, aq, rl) -> LOAD( - translate_imm12 "imm" imm, - translate_reg "rs" rs, - translate_reg "rd" rd, - translate_bool "unsigned" unsigned, - translate_wordWidth width, - translate_bool "aq" aq, - translate_bool "rl" rl) -| `RISCVStore(imm, rs, rd, width, aq, rl) -> STORE ( - translate_imm12 "imm" imm, - translate_reg "rs" rs, - translate_reg "rd" rd, - translate_wordWidth width, - translate_bool "aq" aq, - translate_bool "rl" rl) -| `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) -| `RISCVRTYPEW(rs2, rs1, rd, op) -> RTYPEW( - translate_reg "rs2" rs2, - translate_reg "rs1" rs1, - translate_reg "rd" rd, - translate_ropw op) -| `RISCVFENCE(pred, succ) -> FENCE( - translate_imm4 "pred" pred, - translate_imm4 "succ" succ) -| `RISCVFENCEI -> FENCEI -| `RISCVLoadRes(aq, rl, rs1, width, rd) -> LOADRES( - translate_bool "aq" aq, - translate_bool "rl" rl, - translate_reg "rs1" rs1, - translate_wordWidth width, - translate_reg "rd" rd) -| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> STORECON( - translate_bool "aq" aq, - translate_bool "rl" rl, - translate_reg "rs2" rs2, - translate_reg "rs1" rs1, - translate_wordWidth width, - translate_reg "rd" rd) -| `RISCVAMO (op, aq, rl, rs2, rs1, width, rd) -> AMO( - translate_amoop op, - translate_bool "aq" aq, - translate_bool "rl" rl, - translate_reg "rs2" rs2, - translate_reg "rs1" rs1, - translate_wordWidth width, - translate_reg "rd" rd) diff --git a/risc-v/gen/herdtools_types_to_shallow_types.hgen b/risc-v/gen/herdtools_types_to_shallow_types.hgen deleted file mode 100644 index e6edd24d..00000000 --- a/risc-v/gen/herdtools_types_to_shallow_types.hgen +++ /dev/null @@ -1,90 +0,0 @@ -let is_inc = false - -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_uop op = match op with - | RISCVLUI -> RISCV_LUI - | RISCVAUIPC -> RISCV_AUIPC - -let translate_bop op = match op with - | RISCVBEQ -> RISCV_BEQ - | RISCVBNE -> RISCV_BNE - | RISCVBLT -> RISCV_BLT - | RISCVBGE -> RISCV_BGE - | RISCVBLTU -> RISCV_BLTU - | RISCVBGEU -> RISCV_BGEU - -let translate_iop op = match op with - | RISCVADDI -> RISCV_ADDI - | RISCVSLTI -> RISCV_SLTI - | RISCVSLTIU -> RISCV_SLTIU - | RISCVXORI -> RISCV_XORI - | RISCVORI -> RISCV_ORI - | RISCVANDI -> RISCV_ANDI - -let translate_sop op = match op with - | RISCVSLLI -> RISCV_SLLI - | RISCVSRLI -> RISCV_SRLI - | RISCVSRAI -> RISCV_SRAI - -let translate_rop op = match op with - | RISCVADD -> RISCV_ADD - | RISCVSUB -> RISCV_SUB - | RISCVSLL -> RISCV_SLL - | RISCVSLT -> RISCV_SLT - | RISCVSLTU -> RISCV_SLTU - | RISCVXOR -> RISCV_XOR - | RISCVSRL -> RISCV_SRL - | RISCVSRA -> RISCV_SRA - | RISCVOR -> RISCV_OR - | RISCVAND -> RISCV_AND - -let translate_ropw op = match op with - | RISCVADDW -> RISCV_ADDW - | RISCVSUBW -> RISCV_SUBW - | RISCVSLLW -> RISCV_SLLW - | RISCVSRLW -> RISCV_SRLW - | RISCVSRAW -> RISCV_SRAW - -let translate_amoop op = match op with - | RISCVAMOSWAP -> AMOSWAP - | RISCVAMOADD -> AMOADD - | RISCVAMOXOR -> AMOXOR - | RISCVAMOAND -> AMOAND - | RISCVAMOOR -> AMOOR - | RISCVAMOMIN -> AMOMIN - | RISCVAMOMAX -> AMOMAX - | RISCVAMOMINU -> AMOMINU - | RISCVAMOMAXU -> AMOMAXU - -let translate_wordWidth op = match op with - | RISCVBYTE -> BYTE - | RISCVHALF -> HALF - | RISCVWORD -> WORD - | RISCVDOUBLE -> DOUBLE - -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) - -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_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/gen/lexer.hgen b/risc-v/gen/lexer.hgen deleted file mode 100644 index e42b8a62..00000000 --- a/risc-v/gen/lexer.hgen +++ /dev/null @@ -1,190 +0,0 @@ -"lui" , UTYPE { op=RISCVLUI }; -"auipc" , UTYPE { op=RISCVAUIPC }; - -"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=RISCVSLTI}; -"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=RISCVBYTE; aq=false; rl=false}; -"lbu", LOAD{unsigned=true; width=RISCVBYTE; aq=false; rl=false}; -"lh", LOAD{unsigned=false; width=RISCVHALF; aq=false; rl=false}; -"lhu", LOAD{unsigned=true; width=RISCVHALF; aq=false; rl=false}; -"lw", LOAD{unsigned=false; width=RISCVWORD; aq=false; rl=false}; -"lwu", LOAD{unsigned=true; width=RISCVWORD; aq=false; rl=false}; -"ld", LOAD{unsigned=false; width=RISCVDOUBLE; aq=false; rl=false}; - -"lb.aq", LOAD{unsigned=false; width=RISCVBYTE; aq=true; rl=false}; -"lbu.aq", LOAD{unsigned=true; width=RISCVBYTE; aq=true; rl=false}; -"lh.aq", LOAD{unsigned=false; width=RISCVHALF; aq=true; rl=false}; -"lhu.aq", LOAD{unsigned=true; width=RISCVHALF; aq=true; rl=false}; -"lw.aq", LOAD{unsigned=false; width=RISCVWORD; aq=true; rl=false}; -"lwu.aq", LOAD{unsigned=true; width=RISCVWORD; aq=true; rl=false}; -"ld.aq", LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=false}; - -"lb.aq.rl", LOAD{unsigned=false; width=RISCVBYTE; aq=true; rl=true}; -"lbu.aq.rl", LOAD{unsigned=true; width=RISCVBYTE; aq=true; rl=true}; -"lh.aq.rl", LOAD{unsigned=false; width=RISCVHALF; aq=true; rl=true}; -"lhu.aq.rl", LOAD{unsigned=true; width=RISCVHALF; aq=true; rl=true}; -"lw.aq.rl", LOAD{unsigned=false; width=RISCVWORD; aq=true; rl=true}; -"lwu.aq.rl", LOAD{unsigned=true; width=RISCVWORD; aq=true; rl=true}; -"ld.aq.rl", LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=true}; - -"sb", STORE{width=RISCVBYTE; aq=false; rl=false}; -"sh", STORE{width=RISCVHALF; aq=false; rl=false}; -"sw", STORE{width=RISCVWORD; aq=false; rl=false}; -"sd", STORE{width=RISCVDOUBLE; aq=false; rl=false}; - -"sb.rl", STORE{width=RISCVBYTE; aq=false; rl=true}; -"sh.rl", STORE{width=RISCVHALF; aq=false; rl=true}; -"sw.rl", STORE{width=RISCVWORD; aq=false; rl=true}; -"sd.rl", STORE{width=RISCVDOUBLE; aq=false; rl=true}; - -"sb.aq.rl", STORE{width=RISCVBYTE; aq=true; rl=true}; -"sh.aq.rl", STORE{width=RISCVHALF; aq=true; rl=true}; -"sw.aq.rl", STORE{width=RISCVWORD; aq=true; rl=true}; -"sd.aq.rl", STORE{width=RISCVDOUBLE; aq=true; rl=true}; - -"addiw", ADDIW (); - -"slliw", SHIFTW{op=RISCVSLLI}; -"srliw", SHIFTW{op=RISCVSRLI}; -"sraiw", SHIFTW{op=RISCVSRAI}; - -"addw", RTYPEW{op=RISCVADDW}; -"subw", RTYPEW{op=RISCVSUBW}; -"sslw", RTYPEW{op=RISCVSLLW}; -"srlw", RTYPEW{op=RISCVSRLW}; -"sraw", RTYPEW{op=RISCVSRAW}; - -"fence", FENCE (); -"r", FENCEOPTION Fence_R; -"w", FENCEOPTION Fence_W; -"rw", FENCEOPTION Fence_RW; - -"fence.i", FENCEI (); - -"lr.w", LOADRES {width=RISCVWORD; aq=false; rl=false}; -"lr.w.aq", LOADRES {width=RISCVWORD; aq=true; rl=false}; -"lr.w.aq.rl", LOADRES {width=RISCVWORD; aq=true; rl=true}; -"lr.d", LOADRES {width=RISCVDOUBLE; aq=false; rl=false}; -"lr.d.aq", LOADRES {width=RISCVDOUBLE; aq=true; rl=false}; -"lr.d.aq.rl", LOADRES {width=RISCVDOUBLE; aq=true; rl=true}; - -"sc.w", STORECON {width=RISCVWORD; aq=false; rl=false}; -"sc.w.rl", STORECON {width=RISCVWORD; aq=false; rl=true}; -"sc.w.aq.rl", STORECON {width=RISCVWORD; aq=true; rl=true}; -"sc.d", STORECON {width=RISCVDOUBLE; aq=false; rl=false}; -"sc.d.rl", STORECON {width=RISCVDOUBLE; aq=false; rl=true}; -"sc.d.aq.rl", STORECON {width=RISCVDOUBLE; aq=true; rl=true}; - -"amoswap.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOSWAP}; -"amoadd.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOADD}; -"amoand.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOAND}; -"amoor.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOOR}; -"amoxor.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOXOR}; -"amomax.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMAX}; -"amomin.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMIN}; -"amomaxu.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMAXU}; -"amominu.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMINU}; - -"amoswap.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOSWAP}; -"amoadd.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOADD}; -"amoand.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOAND}; -"amoor.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOOR}; -"amoxor.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOXOR}; -"amomax.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMAX}; -"amomin.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMIN}; -"amomaxu.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMAXU}; -"amominu.d", AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMINU}; - -"amoswap.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOSWAP}; -"amoadd.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOADD}; -"amoand.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOAND}; -"amoor.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOOR}; -"amoxor.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOXOR}; -"amomax.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMAX}; -"amomin.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMIN}; -"amomaxu.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMAXU}; -"amominu.w.aq", AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMINU}; - -"amoswap.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOSWAP}; -"amoadd.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOADD}; -"amoand.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOAND}; -"amoor.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOOR}; -"amoxor.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOXOR}; -"amomax.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMAX}; -"amomin.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMIN}; -"amomaxu.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMAXU}; -"amominu.d.aq", AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMINU}; - -"amoswap.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOSWAP}; -"amoadd.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOADD}; -"amoand.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOAND}; -"amoor.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOOR}; -"amoxor.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOXOR}; -"amomax.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMAX}; -"amomin.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMIN}; -"amomaxu.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMAXU}; -"amominu.w.rl", AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMINU}; - -"amoswap.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOSWAP}; -"amoadd.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOADD}; -"amoand.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOAND}; -"amoor.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOOR}; -"amoxor.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOXOR}; -"amomax.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMAX}; -"amomin.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMIN}; -"amomaxu.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMAXU}; -"amominu.d.rl", AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMINU}; - -"amoswap.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOSWAP}; -"amoadd.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOADD}; -"amoand.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOAND}; -"amoor.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOOR}; -"amoxor.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOXOR}; -"amomax.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMAX}; -"amomin.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMIN}; -"amomaxu.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMAXU}; -"amominu.w.aq.rl", AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMINU}; - -"amoswap.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOSWAP}; -"amoadd.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOADD}; -"amoand.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOAND}; -"amoor.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOOR}; -"amoxor.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOXOR}; -"amomax.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMAX}; -"amomin.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMIN}; -"amomaxu.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMAXU}; -"amominu.d.aq.rl", AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMINU}; - -(** pseudo instructions *********************************************) - -"li", LI () diff --git a/risc-v/gen/map.hgen b/risc-v/gen/map.hgen deleted file mode 100644 index bab5ced8..00000000 --- a/risc-v/gen/map.hgen +++ /dev/null @@ -1,15 +0,0 @@ -| `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, a, b) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a, b) -| `RISCVStore (x, r0, r1, y, z, a) -> `RISCVStore (x, map_reg r0, map_reg r1, y, z, a) -| `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) -| `RISCVLoadRes (aq, rl, rs1, w, rd) -> `RISCVLoadRes (aq, rl, map_reg rs1, w, map_reg rd) -| `RISCVStoreCon (aq, rl, rs2, rs1, w, rd) -> `RISCVStoreCon (aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd) -| `RISCVAMO (op, aq, rl, rs2, rs1, w, rd) -> `RISCVAMO (op, aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd) diff --git a/risc-v/gen/parser.hgen b/risc-v/gen/parser.hgen deleted file mode 100644 index 210e38fb..00000000 --- a/risc-v/gen/parser.hgen +++ /dev/null @@ -1,74 +0,0 @@ -| UTYPE reg COMMA NUM - { (* it's not clear if NUM here should be before or after filling the - lowest 12 bits with zeros, or if it should be signed or unsigned; - currently assuming: NUM does not include the 12 zeros, and is unsigned *) - if not (iskbituimm 20 $4) then failwith "immediate is not 20bit" - else `RISCVUTYPE ($4, $2, $1.op) } -| JAL reg COMMA NUM - { if not ($4 mod 2 = 0) then failwith "odd offset" - else if not (iskbitsimm 21 $4) then failwith "offset is not 21bit" - else `RISCVJAL ($4, $2) } -| JALR reg COMMA reg COMMA NUM - { if not (iskbitsimm 12 $6) then failwith "offset is not 12bit" - else `RISCVJALR ($6, $4, $2) } -| BTYPE reg COMMA reg COMMA NUM - { if not ($6 mod 2 = 0) then failwith "odd offset" - else if not (iskbitsimm 13 $6) then failwith "offset is not 13bit" - else `RISCVBType ($6, $4, $2, $1.op) } -| ITYPE reg COMMA reg COMMA NUM - { if $1.op <> RISCVSLTIU && not (iskbitsimm 12 $6) then failwith "immediate is not 12bit" - else if $1.op = RISCVSLTIU && not (iskbituimm 12 $6) then failwith "unsigned immediate is not 12bit" - else `RISCVIType ($6, $4, $2, $1.op) } -| ADDIW reg COMMA reg COMMA NUM - { if not (iskbitsimm 12 $6) then failwith "immediate is not 12bit" - else `RISCVADDIW ($6, $4, $2) } -| SHIFTIOP reg COMMA reg COMMA NUM - { if not (iskbituimm 6 $6) then failwith "unsigned immediate is not 6bit" - else `RISCVShiftIop ($6, $4, $2, $1.op) } -| SHIFTW reg COMMA reg COMMA NUM - { if not (iskbituimm 5 $6) then failwith "unsigned immediate is not 5bit" - else `RISCVSHIFTW ($6, $4, $2, $1.op) } -| RTYPE reg COMMA reg COMMA reg - { `RISCVRType ($6, $4, $2, $1.op) } -| LOAD reg COMMA NUM LPAR reg RPAR - { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit" - else `RISCVLoad ($4, $6, $2, $1.unsigned, $1.width, $1.aq, $1.rl) } -| STORE reg COMMA NUM LPAR reg RPAR - { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit" - else `RISCVStore ($4, $2, $6, $1.width, $1.aq, $1.rl) } -| RTYPEW reg COMMA reg COMMA reg - { `RISCVRTYPEW ($6, $4, $2, $1.op) } -| FENCE FENCEOPTION COMMA FENCEOPTION - { match ($2, $4) with - | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011) - | (Fence_R, Fence_RW) -> `RISCVFENCE (0b0010, 0b0011) - | (Fence_R, Fence_R) -> `RISCVFENCE (0b0010, 0b0010) - | (Fence_RW, Fence_W) -> `RISCVFENCE (0b0011, 0b0001) - | (Fence_W, Fence_W) -> `RISCVFENCE (0b0001, 0b0001) - | (Fence_RW, Fence_R) -> failwith "'fence rw,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" - } -| FENCEI - { `RISCVFENCEI } -| LOADRES reg COMMA LPAR reg RPAR - { `RISCVLoadRes ($1.aq, $1.rl, $5, $1.width, $2) } -| LOADRES reg COMMA NUM LPAR reg RPAR - { if $4 <> 0 then failwith "'lr' offset must be 0" else - `RISCVLoadRes ($1.aq, $1.rl, $6, $1.width, $2) } -| STORECON reg COMMA reg COMMA LPAR reg RPAR - { `RISCVStoreCon ($1.aq, $1.rl, $4, $7, $1.width, $2) } -| STORECON reg COMMA reg COMMA NUM LPAR reg RPAR - { if $6 <> 0 then failwith "'sc' offset must be 0" else - `RISCVStoreCon ($1.aq, $1.rl, $4, $8, $1.width, $2) } -| AMO reg COMMA reg COMMA LPAR reg RPAR - { `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $7, $1.width, $2) } -| AMO reg COMMA reg COMMA NUM LPAR reg RPAR - { if $6 <> 0 then failwith "'amo<op>' offset must be 0" else - `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $8, $1.width, $2) } - -/* pseudo-ops */ -| LI reg COMMA NUM - { if not (iskbitsimm 12 $4) then failwith "immediate is not 12bit (li is currently implemented only with small immediate)" - else `RISCVIType ($4, IReg R0, $2, RISCVORI) } diff --git a/risc-v/gen/pretty.hgen b/risc-v/gen/pretty.hgen deleted file mode 100644 index fc1c0000..00000000 --- a/risc-v/gen/pretty.hgen +++ /dev/null @@ -1,30 +0,0 @@ -| `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 -| `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, aq, rl) -> - sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width, aq, rl)) (pp_reg rd) imm (pp_reg rs) - -| `RISCVStore(imm, rs2, rs1, width, aq, rl) -> - sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, aq, rl)) (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) -| `RISCVFENCE(pred, succ) -> sprintf "fence %s, %s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ) -| `RISCVFENCEI -> sprintf "fence.i" - -| `RISCVLoadRes(aq, rl, rs1, width, rd) -> - sprintf "%s %s, (%s)" (pp_riscv_load_reserved_op (aq, rl, width)) (pp_reg rd) (pp_reg rs1) - -| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> - sprintf "%s %s, %s, (%s)" (pp_riscv_store_conditional_op (aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1) - -| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) -> - sprintf "%s %s, %s, (%s)" (pp_riscv_amo_op (op, aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1) diff --git a/risc-v/gen/pretty_xml.hgen b/risc-v/gen/pretty_xml.hgen deleted file mode 100644 index b0306161..00000000 --- a/risc-v/gen/pretty_xml.hgen +++ /dev/null @@ -1,137 +0,0 @@ -| `RISCVThreadStart -> ("op_thread_start", []) - -| `RISCVStopFetching -> ("op_stop_fetching", []) - -| `RISCVUTYPE(imm, rd, op) -> - ("op_U_type", - [ ("op", pp_riscv_uop op); - ("uimm", sprintf "%d" imm); - ("dest", pp_reg rd); - ]) - -| `RISCVJAL(imm, rd) -> - ("op_jal", - [ ("offset", sprintf "%d" imm); - ("dest", pp_reg rd); - ]) - -| `RISCVJALR(imm, rs1, rd) -> - ("op_jalr", - [ ("offset", sprintf "%d" imm); - ("base", pp_reg rs1); - ("dest", pp_reg rd); - ]) - -| `RISCVBType(imm, rs2, rs1, op) -> - ("op_branch", - [ ("op", pp_riscv_bop op); - ("offset", sprintf "%d" imm); - ("src2", pp_reg rs2); - ("src1", pp_reg rs1); - ]) - -| `RISCVIType(imm, rs1, rd, op) -> - ("op_I_type", - [ ("op", pp_riscv_iop op); - ("iimm", sprintf "%d" imm); - ("src", pp_reg rs1); - ("dest", pp_reg rd); - ]) - -| `RISCVShiftIop(imm, rs1, rd, op) -> - ("op_IS_type", - [ ("op", pp_riscv_sop op); - ("shamt", sprintf "%d" imm); - ("src", pp_reg rs1); - ("dest", pp_reg rd); - ]) - -| `RISCVSHIFTW(imm, rs1, rd, op) -> - ("op_ISW_type", - [ ("op", pp_riscv_sop op); - ("shamt", sprintf "%d" imm); - ("src", pp_reg rs1); - ("dest", pp_reg rd); - ]) - -| `RISCVRType (rs2, rs1, rd, op) -> - ("op_R_type", - [ ("op", pp_riscv_rop op); - ("src2", pp_reg rs2); - ("src1", pp_reg rs1); - ("dest", pp_reg rd); - ]) - -| `RISCVLoad(imm, rs1, rd, unsigned, width, aq, rl) -> - ("op_load", - [ ("aq", if aq then "true" else "false"); - ("rl", if rl then "true" else "false"); - ("width", pp_word_width width); - ("unsigned", if unsigned then "true" else "false"); - ("base", pp_reg rs1); - ("offset", sprintf "%d" imm); - ("dest", pp_reg rd); - ]) - -| `RISCVStore(imm, rs2, rs1, width, aq, rl) -> - ("op_store", - [ ("aq", if aq then "true" else "false"); - ("rl", if rl then "true" else "false"); - ("width", pp_word_width width); - ("src", pp_reg rs2); - ("base", pp_reg rs1); - ("offset", sprintf "%d" imm); - ]) - -| `RISCVADDIW(imm, rs1, rd) -> - ("op_addiw", - [ ("iimm", sprintf "%d" imm); - ("src", pp_reg rs1); - ("dest", pp_reg rd); - ]) - -| `RISCVRTYPEW(rs2, rs1, rd, op) -> - ("op_RW_type", - [ ("op", pp_riscv_ropw op); - ("src2", pp_reg rs2); - ("src1", pp_reg rs1); - ("dest", pp_reg rd); - ]) - -| `RISCVFENCE(pred, succ) -> - ("op_fence", - [ ("pred", pp_riscv_fence_option pred); - ("succ", pp_riscv_fence_option succ); - ]) - -| `RISCVFENCEI -> ("op_fence_i", []) - -| `RISCVLoadRes(aq, rl, rs1, width, rd) -> - ("op_lr", - [ ("aq", if aq then "true" else "false"); - ("rl", if rl then "true" else "false"); - ("width", pp_word_width width); - ("addr", pp_reg rs1); - ("dest", pp_reg rd); - ]) - -| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> - ("op_sc", - [ ("aq", if aq then "true" else "false"); - ("rl", if rl then "true" else "false"); - ("width", pp_word_width width); - ("addr", pp_reg rs1); - ("src", pp_reg rs2); - ("dest", pp_reg rd); - ]) - -| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) -> - ("op_amo", - [ ("op", pp_riscv_amo_op_part op); - ("aq", if aq then "true" else "false"); - ("rl", if rl then "true" else "false"); - ("width", pp_word_width width); - ("src", pp_reg rs2); - ("addr", pp_reg rs1); - ("dest", pp_reg rd); - ]) diff --git a/risc-v/gen/sail_trans_out.hgen b/risc-v/gen/sail_trans_out.hgen deleted file mode 100644 index 2f9a80f1..00000000 --- a/risc-v/gen/sail_trans_out.hgen +++ /dev/null @@ -1,23 +0,0 @@ -| ("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_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_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) -| ("LOAD", [imm; rs; rd; unsigned; width; aq; rl]) - -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) -| ("STORE", [imm; rs; rd; width; aq; rl]) - -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) -| ("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(translate_out_imm4 pred, translate_out_imm4 succ) -| ("FENCEI", []) -> `RISCVFENCEI -| ("LOADRES", [aq; rl; rs1; width; rd]) - -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) -| ("STORECON", [aq; rl; rs2; rs1; width; rd]) - -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) -| ("AMO", [op; aq; rl; rs2; rs1; width; rd]) - -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) diff --git a/risc-v/gen/shallow_ast_to_herdtools_ast.hgen b/risc-v/gen/shallow_ast_to_herdtools_ast.hgen deleted file mode 100644 index 3025992e..00000000 --- a/risc-v/gen/shallow_ast_to_herdtools_ast.hgen +++ /dev/null @@ -1,23 +0,0 @@ -| EBREAK -> `RISCVStopFetching -| UTYPE( imm, rd, op) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op) -| RISCV_JAL( imm, rd) -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg rd) -| RISCV_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_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) -| LOAD( imm, rs, rd, unsigned, width, aq, rl) - -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) -| STORE( imm, rs, rd, width, aq, rl) - -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) -| 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(translate_out_imm4 pred, translate_out_imm4 succ) -| FENCEI -> `RISCVFENCEI -| LOADRES( aq, rl, rs1, width, rd) - -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) -| STORECON( aq, rl, rs2, rs1, width, rd) - -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) -| AMO( op, aq, rl, rs2, rs1, width, rd) - -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd) diff --git a/risc-v/gen/shallow_types_to_herdtools_types.hgen b/risc-v/gen/shallow_types_to_herdtools_types.hgen deleted file mode 100644 index 6b3b7f51..00000000 --- a/risc-v/gen/shallow_types_to_herdtools_types.hgen +++ /dev/null @@ -1,84 +0,0 @@ -let translate_out_big_bit = Sail_values.unsigned - -let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst)) -let translate_out_signed_int inst bits = - let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in - if (i >= (1 lsl (bits - 1))) then - (i - (1 lsl bits)) else - i - -let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg)) - -let translate_out_uop op = match op with - | RISCV_LUI -> RISCVLUI - | RISCV_AUIPC -> RISCVAUIPC - -let translate_out_bop op = match op with - | RISCV_BEQ -> RISCVBEQ - | RISCV_BNE -> RISCVBNE - | RISCV_BLT -> RISCVBLT - | RISCV_BGE -> RISCVBGE - | RISCV_BLTU -> RISCVBLTU - | RISCV_BGEU -> RISCVBGEU - -let translate_out_iop op = match op with - | RISCV_ADDI -> RISCVADDI - | RISCV_SLTI -> RISCVSLTI - | RISCV_SLTIU -> RISCVSLTIU - | RISCV_XORI -> RISCVXORI - | RISCV_ORI -> RISCVORI - | RISCV_ANDI -> RISCVANDI - -let translate_out_sop op = match op with - | RISCV_SLLI -> RISCVSLLI - | RISCV_SRLI -> RISCVSRLI - | RISCV_SRAI -> RISCVSRAI - -let translate_out_rop op = match op with - | RISCV_ADD -> RISCVADD - | RISCV_SUB -> RISCVSUB - | RISCV_SLL -> RISCVSLL - | RISCV_SLT -> RISCVSLT - | RISCV_SLTU -> RISCVSLTU - | RISCV_XOR -> RISCVXOR - | RISCV_SRL -> RISCVSRL - | RISCV_SRA -> RISCVSRA - | RISCV_OR -> RISCVOR - | RISCV_AND -> RISCVAND - -let translate_out_ropw op = match op with - | RISCV_ADDW -> RISCVADDW - | RISCV_SUBW -> RISCVSUBW - | RISCV_SLLW -> RISCVSLLW - | RISCV_SRLW -> RISCVSRLW - | RISCV_SRAW -> RISCVSRAW - -let translate_out_amoop op = match op with - | AMOSWAP -> RISCVAMOSWAP - | AMOADD -> RISCVAMOADD - | AMOXOR -> RISCVAMOXOR - | AMOAND -> RISCVAMOAND - | AMOOR -> RISCVAMOOR - | AMOMIN -> RISCVAMOMIN - | AMOMAX -> RISCVAMOMAX - | AMOMINU -> RISCVAMOMINU - | AMOMAXU -> RISCVAMOMAXU - -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_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 -let translate_out_imm4 imm = translate_out_int imm diff --git a/risc-v/gen/token_types.hgen b/risc-v/gen/token_types.hgen deleted file mode 100644 index f29e318d..00000000 --- a/risc-v/gen/token_types.hgen +++ /dev/null @@ -1,23 +0,0 @@ -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; aq: bool; rl: bool } -type token_Store = {width : wordWidth; aq: bool; rl: bool } -type token_ADDIW = unit -type token_SHIFTW = {op : riscvSop } -type token_RTYPEW = {op : riscvRopw } -type token_FENCE = unit -type token_FENCEI = unit -type token_LoadRes = {width : wordWidth; aq: bool; rl: bool } -type token_StoreCon = {width : wordWidth; aq: bool; rl: bool } -type token_AMO = {width : wordWidth; aq: bool; rl: bool; op: riscvAmoop } - -type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW - -(* pseudo-ops *) - -type token_LI = unit diff --git a/risc-v/gen/tokens.hgen b/risc-v/gen/tokens.hgen deleted file mode 100644 index f812adbd..00000000 --- a/risc-v/gen/tokens.hgen +++ /dev/null @@ -1,19 +0,0 @@ -%token <RISCVHGenBase.token_UTYPE> UTYPE -%token <RISCVHGenBase.token_JAL> JAL -%token <RISCVHGenBase.token_JALR> JALR -%token <RISCVHGenBase.token_BType> BTYPE -%token <RISCVHGenBase.token_IType> ITYPE -%token <RISCVHGenBase.token_ShiftIop> SHIFTIOP -%token <RISCVHGenBase.token_RTYPE> RTYPE -%token <RISCVHGenBase.token_Load> LOAD -%token <RISCVHGenBase.token_Store> STORE -%token <RISCVHGenBase.token_ADDIW> ADDIW -%token <RISCVHGenBase.token_SHIFTW> SHIFTW -%token <RISCVHGenBase.token_RTYPEW> RTYPEW -%token <RISCVHGenBase.token_FENCE> FENCE -%token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION -%token <RISCVHGenBase.token_FENCEI> FENCEI -%token <RISCVHGenBase.token_LoadRes> LOADRES -%token <RISCVHGenBase.token_StoreCon> STORECON -%token <RISCVHGenBase.token_AMO> AMO -%token <RISCVHGenBase.token_LI> LI diff --git a/risc-v/gen/trans_sail.hgen b/risc-v/gen/trans_sail.hgen deleted file mode 100644 index 8b7cbe11..00000000 --- a/risc-v/gen/trans_sail.hgen +++ /dev/null @@ -1,153 +0,0 @@ -| `RISCVStopFetching -> ("EBREAK", [], []) -| `RISCVUTYPE(imm, rd, op) -> - ("UTYPE", - [ - translate_imm20 "imm" imm; - translate_reg "rd" rd; - translate_uop "op" op; - ], - []) -| `RISCVJAL(imm, rd) -> - ("JAL", - [ - translate_imm21 "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_imm13 "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, aq, rl) -> - ("LOAD", - [ - translate_imm12 "imm" imm; - translate_reg "rs" rs; - translate_reg "rd" rd; - translate_bool "unsigned" unsigned; - translate_width "width" width; - translate_bool "aq" aq; - translate_bool "rl" rl; - ], - []) -| `RISCVStore(imm, rs2, rs1, width, aq, rl) -> - ("STORE", - [ - translate_imm12 "imm" imm; - translate_reg "rs2" rs2; - translate_reg "rs1" rs1; - translate_width "width" width; - translate_bool "aq" aq; - translate_bool "rl" rl; - ], - []) -| `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; - ], - []) -| `RISCVFENCE(pred, succ) -> - ("FENCE", - [ - translate_imm4 "pred" pred; - translate_imm4 "succ" succ; - ], - []) -| `RISCVFENCEI -> - ("FENCEI", - [], - []) -| `RISCVLoadRes(aq, rl, rs1, width, rd) -> - ("LOADRES", - [ - translate_bool "aq" aq; - translate_bool "rl" rl; - translate_reg "rs1" rs1; - translate_width "width" width; - translate_reg "rd" rd; - ], - []) -| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> - ("STORECON", - [ - translate_bool "aq" aq; - translate_bool "rl" rl; - translate_reg "rs2" rs2; - translate_reg "rs1" rs1; - translate_width "width" width; - translate_reg "rd" rd; - ], - []) -| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) -> - ("AMO", - [ - translate_amoop "op" op; - translate_bool "aq" aq; - translate_bool "rl" rl; - translate_reg "rs2" rs2; - translate_reg "rs1" rs1; - translate_width "width" width; - translate_reg "rd" rd; - ], - []) diff --git a/risc-v/gen/types.hgen b/risc-v/gen/types.hgen deleted file mode 100644 index a0b75606..00000000 --- a/risc-v/gen/types.hgen +++ /dev/null @@ -1,172 +0,0 @@ -type bit20 = int -type bit12 = int -type bit6 = int -type bit5 = int -type bit4 = 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_word_width width : string = - begin match width with - | RISCVBYTE -> "b" - | RISCVHALF -> "h" - | RISCVWORD -> "w" - | RISCVDOUBLE -> "d" - end - -let pp_riscv_load_op (unsigned, width, aq, rl) = - "l" ^ - (pp_word_width width) ^ - (if unsigned then "u" else "") ^ - (if aq then ".aq" else "") ^ - (if rl then ".rl" else "") - -let pp_riscv_store_op (width, aq, rl) = - "s" ^ - (pp_word_width width) ^ - (if aq then ".aq" else "") ^ - (if rl then ".rl" else "") - -let pp_riscv_load_reserved_op (aq, rl, width) = - "lr." ^ - (pp_word_width width) ^ - (if aq then ".aq" else "") ^ - (if rl then ".rl" else "") - -let pp_riscv_store_conditional_op (aq, rl, width) = - "sc." ^ - (pp_word_width width) ^ - (if aq then ".aq" else "") ^ - (if rl then ".rl" else "") - -type riscvAmoop = - | RISCVAMOSWAP - | RISCVAMOADD - | RISCVAMOXOR - | RISCVAMOAND - | RISCVAMOOR - | RISCVAMOMIN - | RISCVAMOMAX - | RISCVAMOMINU - | RISCVAMOMAXU - -let pp_riscv_amo_op_part = function - | RISCVAMOSWAP -> "swap" - | RISCVAMOADD -> "add" - | RISCVAMOXOR -> "xor" - | RISCVAMOAND -> "and" - | RISCVAMOOR -> "or" - | RISCVAMOMIN -> "min" - | RISCVAMOMAX -> "max" - | RISCVAMOMINU -> "minu" - | RISCVAMOMAXU -> "maxu" - -let pp_riscv_amo_op (op, aq, rl, width) = - "amo" ^ - pp_riscv_amo_op_part op ^ - begin match width with - | RISCVWORD -> ".w" - | RISCVDOUBLE -> ".d" - | _ -> assert false - end ^ - (if aq then ".aq" else "") ^ - (if rl then ".rl" else "") - -let pp_riscv_fence_option = function - | 0b0011 -> "rw" - | 0b0010 -> "r" - | 0b0001 -> "w" - | _ -> failwith "unexpected fence option" diff --git a/risc-v/gen/types_sail_trans_out.hgen b/risc-v/gen/types_sail_trans_out.hgen deleted file mode 100644 index 66a2020c..00000000 --- a/risc-v/gen/types_sail_trans_out.hgen +++ /dev/null @@ -1,98 +0,0 @@ -let translate_out_big_bit = function - | (name, Bvector _, bits) -> IInt.integer_of_bit_list bits - | _ -> assert false - -let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst)) -let translate_out_signed_int inst bits = - let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in - if (i >= (1 lsl (bits - 1))) then - (i - (1 lsl bits)) else - i - -let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg)) - -let translate_out_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 -let translate_out_imm4 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 -| _ -> failwith "Unknown bop in sail translate out" - -let translate_out_iop op = match translate_out_enum op with -| 0 -> RISCVADDI -| 1 -> RISCVSLTI -| 2 -> RISCVSLTIU -| 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 -| 1 -> RISCVSUB -| 2 -> RISCVSLL -| 3 -> RISCVSLT -| 4 -> RISCVSLTU -| 5 -> RISCVXOR -| 6 -> RISCVSRL -| 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 -| 1 -> RISCVSUBW -| 2 -> RISCVSLLW -| 3 -> RISCVSRLW -| 4 -> RISCVSRAW -| _ -> failwith "Unknown ropw in sail translate out" - -let translate_out_amoop op = match translate_out_enum op with -| 0 -> RISCVAMOSWAP -| 1 -> RISCVAMOADD -| 2 -> RISCVAMOXOR -| 3 -> RISCVAMOAND -| 4 -> RISCVAMOOR -| 5 -> RISCVAMOMIN -| 6 -> RISCVAMOMAX -| 7 -> RISCVAMOMINU -| 8 -> RISCVAMOMAXU -| _ -> failwith "Unknown amoop in sail translate out" diff --git a/risc-v/gen/types_trans_sail.hgen b/risc-v/gen/types_trans_sail.hgen deleted file mode 100644 index 238c7e5b..00000000 --- a/risc-v/gen/types_trans_sail.hgen +++ /dev/null @@ -1,57 +0,0 @@ -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_amoop = translate_enum [RISCVAMOSWAP; RISCVAMOADD; RISCVAMOXOR; RISCVAMOAND; RISCVAMOOR; RISCVAMOMIN; RISCVAMOMAX; RISCVAMOMINU; RISCVAMOMAXU] - -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 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 = - (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]) diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail deleted file mode 100644 index 3d52d111..00000000 --- a/risc-v/riscv.sail +++ /dev/null @@ -1,407 +0,0 @@ -scattered typedef ast = const union - -val bit[32] -> option<ast> effect pure decode -scattered function option<ast> decode - -scattered function unit execute - -(********************************************************************) -union ast member ((bit[20]), regno, uop) UTYPE - -function clause decode ((bit[20]) imm : (regno) rd : 0b0110111) = Some(UTYPE(imm, rd, RISCV_LUI)) -function clause decode ((bit[20]) imm : (regno) rd : 0b0010111) = Some(UTYPE(imm, rd, RISCV_AUIPC)) - -function clause execute (UTYPE(imm, rd, op)) = - let (bit[64]) off = EXTS(imm : 0x000) in - let ret = switch (op) { - case RISCV_LUI -> off - case RISCV_AUIPC -> PC + off - } in - wGPR(rd, ret) - -(********************************************************************) -union ast member ((bit[21]), regno) RISCV_JAL - -function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (RISCV_JAL(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0, rd)) - -function clause execute (RISCV_JAL(imm, rd)) = { - (bit[64]) pc := PC; - wGPR(rd, pc + 4); - (bit[64]) offset := EXTS(imm); - nextPC := pc + offset; -} - -(********************************************************************) -union ast member((bit[12]), regno, regno) RISCV_JALR - -function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b1100111) = - Some(RISCV_JALR(imm, rs1, rd)) - -function clause execute (RISCV_JALR(imm, rs1, rd)) = { - (* write rd before anything else to prevent unintended strength *) - wGPR(rd, PC + 4); - (bit[64]) newPC := rGPR(rs1) + EXTS(imm); - nextPC := newPC[63..1] : 0b0; -} - -(********************************************************************) -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, RISCV_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, RISCV_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, RISCV_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, RISCV_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, RISCV_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, RISCV_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 RISCV_BEQ -> rs1_val == rs2_val - case RISCV_BNE -> rs1_val != rs2_val - case RISCV_BLT -> rs1_val <_s rs2_val - case RISCV_BGE -> rs1_val >=_s rs2_val - case RISCV_BLTU -> rs1_val <_u rs2_val - case RISCV_BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *) - } in - if (taken) then - 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, RISCV_ADDI)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_SLTI)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_SLTIU)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_XORI)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_ORI)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b111 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_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 RISCV_ADDI -> rs1_val + imm64 - case RISCV_SLTI -> EXTZ(rs1_val <_s imm64) - case RISCV_SLTIU -> EXTZ(rs1_val <_u imm64) - case RISCV_XORI -> rs1_val ^ imm64 - case RISCV_ORI -> rs1_val | imm64 - case RISCV_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, RISCV_SLLI)) -function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRLI)) -function clause decode (0b010000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRAI)) - -function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = - let rs1_val = rGPR(rs1) in - let result = switch(op) { - case RISCV_SLLI -> rs1_val >> shamt - case RISCV_SRLI -> rs1_val << shamt - case RISCV_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, RISCV_ADD)) -function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SUB)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLL)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLT)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLTU)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b100 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_XOR)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRL)) -function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRA)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b110 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_OR)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b111 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_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 RISCV_ADD -> rs1_val + rs2_val - case RISCV_SUB -> rs1_val - rs2_val - case RISCV_SLL -> rs1_val << (rs2_val[5..0]) - case RISCV_SLT -> EXTZ(rs1_val <_s rs2_val) - case RISCV_SLTU -> EXTZ(rs1_val <_u rs2_val) - case RISCV_XOR -> rs1_val ^ rs2_val - case RISCV_SRL -> rs1_val >> (rs2_val[5..0]) - case RISCV_SRA -> shift_right_arith64(rs1_val, rs2_val[5..0]) - case RISCV_OR -> rs1_val | rs2_val - case RISCV_AND -> rs1_val & rs2_val - } in - wGPR(rd, result) - -(********************************************************************) -union ast member ((bit[12]), regno, regno, bool, word_width, bool, bool) LOAD - -function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE, false, false)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF, false, false)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD, false, false)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE, false, false)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, BYTE, false, false)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, HALF, false, false)) -function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, WORD, false, false)) - -function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) = - let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in - let (bit[64]) result = if unsigned then - switch (width) { - case BYTE -> EXTZ(mem_read(addr, 1, aq, rl, false)) - case HALF -> EXTZ(mem_read(addr, 2, aq, rl, false)) - case WORD -> EXTZ(mem_read(addr, 4, aq, rl, false)) - case DOUBLE -> mem_read(addr, 8, aq, rl, false) - } - else - switch (width) { - case BYTE -> EXTS(mem_read(addr, 1, aq, rl, false)) - case HALF -> EXTS(mem_read(addr, 2, aq, rl, false)) - case WORD -> EXTS(mem_read(addr, 4, aq, rl, false)) - case DOUBLE -> mem_read(addr, 8, aq, rl, false) - } in - wGPR(rd, result) - -(********************************************************************) -union ast member ((bit[12]), regno, regno, word_width, bool, bool) STORE - -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = - Some(STORE(imm7 : imm5, rs2, rs1, BYTE, false, false)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = - Some(STORE(imm7 : imm5, rs2, rs1, HALF, false, false)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = - Some(STORE(imm7 : imm5, rs2, rs1, WORD, false, false)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = - Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE, false, false)) - -function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = - let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in { - switch (width) { - case BYTE -> mem_write_ea(addr, 1, aq, rl, false) - case HALF -> mem_write_ea(addr, 2, aq, rl, false) - case WORD -> mem_write_ea(addr, 4, aq, rl, false) - case DOUBLE -> mem_write_ea(addr, 8, aq, rl, false) - }; - let rs2_val = rGPR(rs2) in - switch (width) { - case BYTE -> mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false) - case HALF -> mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false) - case WORD -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false) - case DOUBLE -> mem_write_value(addr, 8, rs2_val, aq, rl, false) - } - } - -(********************************************************************) -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, RISCV_SLLI)) -function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRLI)) -function clause decode (0b0100000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRAI)) - -function clause execute (SHIFTW(shamt, rs1, rd, op)) = - let rs1_val = (rGPR(rs1))[31..0] in - let result = switch(op) { - case RISCV_SLLI -> rs1_val >> shamt - case RISCV_SRLI -> rs1_val << shamt - case RISCV_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, RISCV_ADDW)) -function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SUBW)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SLLW)) -function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SRLW)) -function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_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 RISCV_ADDW -> rs1_val + rs2_val - case RISCV_SUBW -> rs1_val - rs2_val - case RISCV_SLLW -> rs1_val << (rs2_val[4..0]) - case RISCV_SRLW -> rs1_val >> (rs2_val[4..0]) - case RISCV_SRAW -> shift_right_arith32(rs1_val, rs2_val[4..0]) - } 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)) = { - switch(pred, succ) { - case (0b0011, 0b0011) -> MEM_fence_rw_rw() - case (0b0010, 0b0011) -> MEM_fence_r_rw() - case (0b0010, 0b0010) -> MEM_fence_r_r() - case (0b0011, 0b0001) -> MEM_fence_rw_w() - case (0b0001, 0b0001) -> MEM_fence_w_w() - case _ -> not_implemented("unsupported fence") - } -} - -(********************************************************************) -union ast member unit FENCEI -function clause decode (0b000000000000 : 0b00000 : 0b001 : 0b00000 : 0b0001111) = Some(FENCEI) -function clause execute FENCEI = MEM_fence_i() - -(********************************************************************) -union ast member unit ECALL -function clause decode (0b000000000000 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(ECALL ()) -function clause execute ECALL = not_implemented("ECALL is not implemented") - -(********************************************************************) -union ast member unit EBREAK -function clause decode (0b000000000001 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(EBREAK ()) -function clause execute EBREAK = { exit () } - -(********************************************************************) -union ast member (bool, bool, regno, word_width, regno) LOADRES - -function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, WORD, rd)) -function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, DOUBLE, rd)) -function clause execute(LOADRES(aq, rl, rs1, width, rd)) = - let (bit[64]) addr = rGPR(rs1) in - let (bit[64]) result = - switch width { - case WORD -> EXTS(mem_read(addr, 4, aq, rl, true)) - case DOUBLE -> mem_read(addr, 8, aq, rl, true) - } in - wGPR(rd, result) - -(********************************************************************) -union ast member (bool, bool, regno, regno, word_width, regno) STORECON - -function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = - Some(STORECON(aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = - Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd)) - -function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { - (*(bit)*) status := if speculate_conditional_success() then 0 else 1; - wGPR(rd) := (bit[64]) (EXTZ([status])); - - if status == 1 then () else { - (bit[64]) addr := rGPR(rs1); - switch width { - case WORD -> mem_write_ea(addr, 4, aq, rl, true) - case DOUBLE -> mem_write_ea(addr, 8, aq, rl, true) - }; - rs2_val := rGPR(rs2); - switch width { - case WORD -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true) - case DOUBLE -> mem_write_value(addr, 8, rs2_val, aq, rl, true) - }; - }; -} - -(********************************************************************) -union ast member (amoop, bool, bool, regno, regno, word_width, regno) AMO - -function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = - Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = - Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = - Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = - Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = - Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = - Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = - Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = - Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = - Some(AMO(AMOOR , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = - Some(AMO(AMOOR , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = - Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = - Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = - Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = - Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = - Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = - Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = - Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = - Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd)) - -function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { - (bit[64]) addr := rGPR(rs1); - - switch (width) { - case WORD -> mem_write_ea(addr, 4, aq & rl, rl, true) - case DOUBLE -> mem_write_ea(addr, 8, aq & rl, rl, true) - }; - - (bit[64]) loaded := - switch (width) { - case WORD -> EXTS(mem_read(addr, 4, aq, aq & rl, true)) - case DOUBLE -> mem_read(addr, 8, aq, aq & rl, true) - }; - wGPR(rd, loaded); - - (bit[64]) rs2_val := rGPR(rs2); - (bit[64]) result := - switch(op) { - case AMOSWAP -> rs2_val - case AMOADD -> rs2_val + loaded - case AMOXOR -> rs2_val ^ loaded - case AMOAND -> rs2_val & loaded - case AMOOR -> rs2_val | loaded - - case AMOMIN -> (bit[64]) (min(signed(rs2_val), signed(loaded))) - case AMOMAX -> (bit[64]) (max(signed(rs2_val), signed(loaded))) - case AMOMINU -> (bit[64]) (min(unsigned(rs2_val), unsigned(loaded))) - case AMOMAXU -> (bit[64]) (max(unsigned(rs2_val), unsigned(loaded))) - }; - - switch (width) { - case WORD -> mem_write_value(addr, 4, result[31..0], aq & rl, rl, true) - case DOUBLE -> mem_write_value(addr, 8, result, aq & rl, rl, true) - }; -} - -(********************************************************************) - -function clause decode _ = None - -end ast -end decode -end execute diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem deleted file mode 100644 index 4ca5f9b7..00000000 --- a/risc-v/riscv_extras.lem +++ /dev/null @@ -1,83 +0,0 @@ -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 riscv_read_memory_functions : memory_reads = - [ ("MEMr", (MR Read_plain memory_parameter_transformer)); - ("MEMr_acquire", (MR Read_RISCV_acquire memory_parameter_transformer)); - ("MEMr_strong_acquire", (MR Read_RISCV_strong_acquire memory_parameter_transformer)); - ("MEMr_reserved", (MR Read_RISCV_reserved memory_parameter_transformer)); - ("MEMr_reserved_acquire", (MR Read_RISCV_reserved_acquire memory_parameter_transformer)); - ("MEMr_reserved_strong_acquire", - (MR Read_RISCV_reserved_acquire memory_parameter_transformer)); - ] - -let riscv_memory_writes : memory_writes = - [] - -let riscv_memory_eas : memory_write_eas = - [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); - ("MEMea_release", (MEA Write_RISCV_release memory_parameter_transformer)); - ("MEMea_strong_release", (MEA Write_RISCV_strong_release memory_parameter_transformer)); - ("MEMea_conditional", (MEA Write_RISCV_conditional memory_parameter_transformer)); - ("MEMea_conditional_release", (MEA Write_RISCV_conditional_release memory_parameter_transformer)); - ("MEMea_conditional_strong_release", - (MEA Write_RISCV_conditional_strong_release - memory_parameter_transformer)); - ] - -let riscv_memory_vals : memory_write_vals = - [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_release", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_strong_release", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_conditional", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_conditional_release",(MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_conditional_strong_release", - (MV memory_parameter_transformer_option_address Nothing)); - - ] - -let riscv_speculate_conditional_success : excl_res = - let f = fun (IState interp context) b -> - let bool_res = 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 bool_res) context - in - Just ("speculate_conditional_success", (ER (Just f))) - -let riscv_barrier_functions = - [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw); - ("MEM_fence_r_rw", Barrier_RISCV_r_rw); - ("MEM_fence_r_r", Barrier_RISCV_r_r); - ("MEM_fence_rw_w", Barrier_RISCV_rw_w); - ("MEM_fence_w_w", Barrier_RISCV_w_w); - ("MEM_fence_i", Barrier_RISCV_i); - ] diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem deleted file mode 100644 index 32110079..00000000 --- a/risc-v/riscv_extras_embed.lem +++ /dev/null @@ -1,71 +0,0 @@ -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_acquire : (vector bitU * integer) -> M (vector bitU) -val MEMr_strong_acquire : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserved : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserved_acquire : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserved_strong_acquire : (vector bitU * integer) -> M (vector bitU) - -let MEMr (addr,size) = read_mem false Read_plain addr size -let MEMr_acquire (addr,size) = read_mem false Read_RISCV_acquire addr size -let MEMr_strong_acquire (addr,size) = read_mem false Read_RISCV_strong_acquire addr size -let MEMr_reserved (addr,size) = read_mem false Read_RISCV_reserved addr size -let MEMr_reserved_acquire (addr,size) = read_mem false Read_RISCV_reserved_acquire addr size -let MEMr_reserved_strong_acquire (addr,size) - = read_mem false Read_RISCV_reserved_strong_acquire addr size - -val MEMea : (vector bitU * integer) -> M unit -val MEMea_release : (vector bitU * integer) -> M unit -val MEMea_strong_release : (vector bitU * integer) -> M unit -val MEMea_conditional : (vector bitU * integer) -> M unit -val MEMea_conditional_release : (vector bitU * integer) -> M unit -val MEMea_conditional_strong_release : (vector bitU * integer) -> M unit - -let MEMea (addr,size) = write_mem_ea Write_plain addr size -let MEMea_release (addr,size) = write_mem_ea Write_RISCV_release addr size -let MEMea_strong_release (addr,size) = write_mem_ea Write_RISCV_strong_release addr size -let MEMea_conditional (addr,size) = write_mem_ea Write_RISCV_conditional addr size -let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional_release addr size -let MEMea_conditional_strong_release (addr,size) - = write_mem_ea Write_RISCV_conditional_strong_release addr size - -val MEMval : (vector bitU * integer * vector bitU) -> M unit -val MEMval_release : (vector bitU * integer * vector bitU) -> M unit -val MEMval_strong_release : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional_strong_release : (vector bitU * integer * vector bitU) -> M unit - -let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_release (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_strong_release (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional_strong_release (_,_,v) - = write_mem_val v >>= fun _ -> return () - -let speculate_conditional_success () = excl_result () >>= fun b -> return (if b then B1 else B0) - -val MEM_fence_rw_rw : unit -> M unit -val MEM_fence_r_rw : unit -> M unit -val MEM_fence_r_r : unit -> M unit -val MEM_fence_rw_w : unit -> M unit -val MEM_fence_w_w : unit -> M unit -val MEM_fence_i : 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_r_r () = barrier Barrier_RISCV_r_r -let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w -let MEM_fence_w_w () = barrier Barrier_RISCV_w_w -let MEM_fence_i () = barrier Barrier_RISCV_i - -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 deleted file mode 100644 index 3c922268..00000000 --- a/risc-v/riscv_extras_embed_sequential.lem +++ /dev/null @@ -1,71 +0,0 @@ -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_acquire : (vector bitU * integer) -> M (vector bitU) -val MEMr_strong_acquire : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserved : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserved_acquire : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserved_strong_acquire : (vector bitU * integer) -> M (vector bitU) - -let MEMr (addr,size) = read_mem false Read_plain addr size -let MEMr_acquire (addr,size) = read_mem false Read_RISCV_acquire addr size -let MEMr_strong_acquire (addr,size) = read_mem false Read_RISCV_strong_acquire addr size -let MEMr_reserved (addr,size) = read_mem false Read_RISCV_reserved addr size -let MEMr_reserved_acquire (addr,size) = read_mem false Read_RISCV_reserved_acquire addr size -let MEMr_reserved_strong_acquire (addr,size) - = read_mem false Read_RISCV_reserved_strong_acquire addr size - -val MEMea : (vector bitU * integer) -> M unit -val MEMea_release : (vector bitU * integer) -> M unit -val MEMea_strong_release : (vector bitU * integer) -> M unit -val MEMea_conditional : (vector bitU * integer) -> M unit -val MEMea_conditional_release : (vector bitU * integer) -> M unit -val MEMea_conditional_strong_release : (vector bitU * integer) -> M unit - -let MEMea (addr,size) = write_mem_ea Write_plain addr size -let MEMea_release (addr,size) = write_mem_ea Write_RISCV_release addr size -let MEMea_strong_release (addr,size) = write_mem_ea Write_RISCV_strong_release addr size -let MEMea_conditional (addr,size) = write_mem_ea Write_RISCV_conditional addr size -let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional_release addr size -let MEMea_conditional_strong_release (addr,size) - = write_mem_ea Write_RISCV_conditional_strong_release addr size - -val MEMval : (vector bitU * integer * vector bitU) -> M unit -val MEMval_release : (vector bitU * integer * vector bitU) -> M unit -val MEMval_strong_release : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional_strong_release : (vector bitU * integer * vector bitU) -> M unit - -let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_release (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_strong_release (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional_strong_release (_,_,v) - = write_mem_val v >>= fun _ -> return () - -let speculate_conditional_success () = excl_result () >>= fun b -> return (if b then B1 else B0) - -val MEM_fence_rw_rw : unit -> M unit -val MEM_fence_r_rw : unit -> M unit -val MEM_fence_r_r : unit -> M unit -val MEM_fence_rw_w : unit -> M unit -val MEM_fence_w_w : unit -> M unit -val MEM_fence_i : 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_r_r () = barrier Barrier_RISCV_r_r -let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w -let MEM_fence_w_w () = barrier Barrier_RISCV_w_w -let MEM_fence_i () = barrier Barrier_RISCV_i - -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_regfp.sail b/risc-v/riscv_regfp.sail deleted file mode 100644 index dee9cc8e..00000000 --- a/risc-v/riscv_regfp.sail +++ /dev/null @@ -1,145 +0,0 @@ -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 (RISCV_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 (RISCV_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, aq, rl)) -> { (* 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 := - switch (aq, rl) { - case (false, false) -> IK_mem_read (Read_plain) - case (true, false) -> IK_mem_read (Read_RISCV_acquire) - case (false, true) -> exit "not implemented" - case (true, true) -> IK_mem_read (Read_RISCV_strong_acquire) - }; - } - case (STORE( imm, rs2, rs1, width, aq, rl)) -> { - 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 := - switch (aq, rl) { - case (false, false) -> IK_mem_write (Write_plain) - case (true, false) -> exit "not implemented" - case (false, true) -> IK_mem_write (Write_RISCV_release) - case (true, true) -> IK_mem_write (Write_RISCV_strong_release) - }; - } - 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; - } - case (FENCE(pred, succ)) -> { - ik := - switch(pred, succ) { - case (0b0011, 0b0011) -> IK_barrier (Barrier_RISCV_rw_rw) - case (0b0010, 0b0011) -> IK_barrier (Barrier_RISCV_r_rw) - case (0b0010, 0b0010) -> IK_barrier (Barrier_RISCV_r_r) - case (0b0011, 0b0001) -> IK_barrier (Barrier_RISCV_rw_w) - case (0b0001, 0b0001) -> IK_barrier (Barrier_RISCV_w_w) - case _ -> exit "not implemented" - }; - } - case (FENCEI) -> { - ik := IK_barrier (Barrier_RISCV_i); - } - case (LOADRES ( aq, rl, rs1, width, rd)) -> { - if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; - if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; - aR := iR; - ik := switch (aq, rl) { - case (false, false) -> IK_mem_read (Read_RISCV_reserved) - case (true, false) -> IK_mem_read (Read_RISCV_reserved_acquire) - case (false, true) -> exit "not implemented" - case (true, true) -> IK_mem_read (Read_RISCV_reserved_strong_acquire) - }; - } - case (STORECON( aq, rl, rs2, rs1, width, rd)) -> { - 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; - if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; - - ik := switch (aq, rl) { - case (false, false) -> IK_mem_write (Write_RISCV_conditional) - case (false, true) -> IK_mem_write (Write_RISCV_conditional_release) - case (true, _) -> exit "not implemented" - }; - } - case (AMO( op, aq, rl, rs2, rs1, width, rd)) -> { - 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; - if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; - - ik := switch (aq, rl) { - case (false, false) -> IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional) - case (false, true) -> IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release) - case (true, false) -> IK_mem_rmw (Read_RISCV_reserved_acquire, - Write_RISCV_conditional) - case (true, true) -> IK_mem_rmw (Read_RISCV_reserved_strong_acquire, - Write_RISCV_conditional_strong_release) - }; - } - }; - (iR,oR,aR,Nias,Dia,ik) -} diff --git a/risc-v/riscv_types.sail b/risc-v/riscv_types.sail deleted file mode 100644 index b584ae9b..00000000 --- a/risc-v/riscv_types.sail +++ /dev/null @@ -1,166 +0,0 @@ -default Order dec - -function forall 'a. 'a effect { escape } not_implemented((string) message) = - exit message - -typedef regval = bit[64] -typedef regno = bit[5] - -(* register (regval) x0 is hard-wired zero *) -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 <1, 31, 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 - -function unit effect { escape } check_alignment( (bit[64]) addr, (nat) width) = - if (unsigned(addr) mod width != 0) then - exit "misaligned memory access" - -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_acquire -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_strong_acquire -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_acquire -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_strong_acquire - -function forall Nat 'n. (bit[8 * 'n]) effect { rmem, escape } mem_read( (bit[64]) addr, ([|'n|]) width, (bool) aq, (bool) rl, (bool) res) = -{ - if (aq | res) then - check_alignment(addr, width); - - switch (aq, rl, res) { - case (false, false, false) -> MEMr(addr, width) - case (true, false, false) -> MEMr_acquire(addr, width) - case (false, false, true) -> MEMr_reserved(addr, width) - case (true, false, true) -> MEMr_reserved_acquire(addr, width) - case (false, true, false) -> not_implemented("load.rl is not implemented") - case (true, true, false) -> MEMr_strong_acquire(addr, width) - case (false, true, true) -> not_implemented("lr.rl is not implemented") - case (true, true, true) -> MEMr_reserved_strong_acquire(addr, width) - } -} - -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_release -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_strong_release -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_release -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_strong_release - -function forall Nat 'n. unit effect { eamem, escape } mem_write_ea( (bit[64]) addr , ([|'n|]) width, (bool) aq, (bool) rl, (bool) con) = -{ - if (rl | con) then - check_alignment(addr, width); - - switch (aq, rl, con) { - case (false, false, false) -> MEMea(addr, width) - case (false, true, false) -> MEMea_release(addr, width) - case (false, false, true) -> MEMea_conditional(addr, width) - case (false, true , true) -> MEMea_conditional_release(addr, width) - case (true, false, false) -> not_implemented("store.aq is not implemented") - case (true, true, false) -> MEMea_strong_release(addr, width) - case (true, false, true) -> not_implemented("sc.aq is not implemented") - case (true, true , true) -> MEMea_conditional_strong_release(addr, width) - } -} - -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_release -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_strong_release -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_release -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_strong_release - -function forall Nat 'n. unit effect { wmv, escape } mem_write_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) aq, (bool) rl, (bool) con) = -{ - if (rl | con) then - check_alignment(addr, width); - - switch (aq, rl, con) { - case (false, false, false) -> MEMval(addr, width, value) - case (false, true, false) -> MEMval_release(addr, width, value) - case (false, false, true) -> MEMval_conditional(addr, width, value) - case (false, true, true) -> MEMval_conditional_release(addr, width, value) - case (true, false, false) -> not_implemented("store.aq is not implemented") - case (true, true, false) -> MEMval_strong_release(addr, width, value) - case (true, false, true) -> not_implemented("sc.aq is not implemented") - case (true, true, true) -> MEMval_conditional_strong_release(addr, width, value) - } -} - -val extern unit -> bool effect {exmem} speculate_conditional_success - -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_r_r -val extern unit -> unit effect { barr } MEM_fence_rw_w -val extern unit -> unit effect { barr } MEM_fence_w_w -val extern unit -> unit effect { barr } MEM_fence_i - -typedef uop = enumerate {RISCV_LUI; RISCV_AUIPC} (* upper immediate ops *) -typedef bop = enumerate {RISCV_BEQ; RISCV_BNE; RISCV_BLT; RISCV_BGE; RISCV_BLTU; RISCV_BGEU} (* branch ops *) -typedef iop = enumerate {RISCV_ADDI; RISCV_SLTI; RISCV_SLTIU; RISCV_XORI; RISCV_ORI; RISCV_ANDI} (* immediate ops *) -typedef sop = enumerate {RISCV_SLLI; RISCV_SRLI; RISCV_SRAI} (* shift ops *) -typedef rop = enumerate {RISCV_ADD; RISCV_SUB; RISCV_SLL; RISCV_SLT; RISCV_SLTU; RISCV_XOR; RISCV_SRL; RISCV_SRA; RISCV_OR; RISCV_AND} (* reg-reg ops *) -typedef ropw = enumerate {RISCV_ADDW; RISCV_SUBW; RISCV_SLLW; RISCV_SRLW; RISCV_SRAW} (* reg-reg 32-bit ops *) -typedef amoop = enumerate {AMOSWAP; AMOADD; AMOXOR; AMOAND; AMOOR; - AMOMIN; AMOMAX; AMOMINU; AMOMAXU} (* AMO ops *) - -typedef word_width = enumerate {BYTE; HALF; WORD; DOUBLE} - -(********************************************************************) - -(* 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] diff --git a/src/ast_util.ml b/src/ast_util.ml index 7e3e0da7..4407b7f1 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -238,6 +238,8 @@ let unit_typ = mk_id_typ (mk_id "unit") let bit_typ = mk_id_typ (mk_id "bit") let real_typ = mk_id_typ (mk_id "real") let app_typ id args = mk_typ (Typ_app (id, args)) +let ref_typ typ = mk_typ (Typ_app (mk_id "ref", [mk_typ_arg (Typ_arg_typ typ)])) +let register_typ typ = mk_typ (Typ_app (mk_id "register", [mk_typ_arg (Typ_arg_typ typ)])) let atom_typ nexp = mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))])) let range_typ nexp1 nexp2 = @@ -338,6 +340,7 @@ and map_exp_annot_aux f = function | E_block xs -> E_block (List.map (map_exp_annot f) xs) | E_nondet xs -> E_nondet (List.map (map_exp_annot f) xs) | E_id id -> E_id id + | E_ref id -> E_ref id | E_lit lit -> E_lit lit | E_cast (typ, exp) -> E_cast (typ, map_exp_annot f exp) | E_app (id, xs) -> E_app (id, List.map (map_exp_annot f) xs) @@ -582,6 +585,7 @@ let rec string_of_exp (E_aux (exp, _)) = match exp with | E_block exps -> "{ " ^ string_of_list "; " string_of_exp exps ^ " }" | E_id v -> string_of_id v + | E_ref id -> "ref " ^ string_of_id id | E_sizeof nexp -> "sizeof " ^ string_of_nexp nexp | E_constraint nc -> "constraint(" ^ string_of_n_constraint nc ^ ")" | E_lit lit -> string_of_lit lit diff --git a/src/ast_util.mli b/src/ast_util.mli index 7ff46b02..a4ad92fb 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -103,6 +103,8 @@ val range_typ : nexp -> nexp -> typ val bit_typ : typ val bool_typ : typ val app_typ : id -> typ_arg list -> typ +val ref_typ : typ -> typ +val register_typ : typ -> typ val unit_typ : typ val string_typ : typ val real_typ : typ diff --git a/src/initial_check.ml b/src/initial_check.ml index 4fde87cd..0915bc38 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -472,6 +472,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) | None -> E_block(List.map (to_ast_exp k_env def_ord) exps)) | Parse_ast.E_nondet(exps) -> E_nondet(List.map (to_ast_exp k_env def_ord) exps) | Parse_ast.E_id(id) -> E_id(to_ast_id id) + | Parse_ast.E_ref(id) -> E_ref(to_ast_id id) | Parse_ast.E_lit(lit) -> E_lit(to_ast_lit lit) | Parse_ast.E_cast(typ,exp) -> E_cast(to_ast_typ k_env def_ord typ, to_ast_exp k_env def_ord exp) | Parse_ast.E_app(f,args) -> @@ -945,6 +946,7 @@ let initial_kind_env = ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})}); ("reg", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); ("register", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); + ("ref", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); ("range", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) }); ("vector", {k = K_Lam( [{k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ); ("atom", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); diff --git a/src/interpreter.ml b/src/interpreter.ml index 3356b9dc..4fd75094 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -51,9 +51,22 @@ open Ast open Ast_util open Value -(* open Type_check *) -type state = St +type gstate = + { registers : value Bindings.t } + +type lstate = + { locals : value Bindings.t } + +type state = lstate * gstate + +let initial_gstate = + { registers = Bindings.empty } + +let initial_lstate = + { locals = Bindings.empty } + +let initial_state = initial_lstate, initial_gstate let value_of_lit (L_aux (l_aux, _)) = match l_aux with @@ -63,6 +76,7 @@ let value_of_lit (L_aux (l_aux, _)) = | L_true -> V_bool true | L_false -> V_bool false | L_string str -> V_string str + | L_num n -> V_int n | _ -> failwith "Unimplemented value_of_lit" (* TODO *) let is_value = function @@ -87,23 +101,23 @@ let value_of_exp = function (**************************************************************************) type 'a response = - | Final of value + | Early_return of value | Exception of value | Assertion_failed of string | Call of id * value list * (value -> 'a) | Gets of (state -> 'a) - | Puts of state * 'a + | Puts of state * (unit -> 'a) and 'a monad = | Pure of 'a | Yield of ('a monad response) let map_response f = function - | Final v -> Final v + | Early_return v -> Early_return v | Exception v -> Exception v | Assertion_failed str -> Assertion_failed str | Gets g -> Gets (fun s -> f (g s)) - | Puts (s, x) -> Puts (s, f x) + | Puts (s, cont) -> Puts (s, fun () -> f (cont ())) | Call (id, vals, cont) -> Call (id, vals, fun v -> f (cont v)) let rec liftM f = function @@ -142,9 +156,9 @@ let gets : state monad = Yield (Gets (fun s -> Pure s)) let puts (s : state) : unit monad = - Yield (Puts (s, Pure ())) + Yield (Puts (s, fun () -> Pure ())) -let final v = Yield (Final v) +let early_return v = Yield (Early_return v) let assertion_failed msg = Yield (Assertion_failed msg) @@ -156,9 +170,22 @@ let rec subst id value (E_aux (e_aux, annot) as exp) = | E_block exps -> E_block (List.map (subst id value) exps) | E_nondet exps -> E_nondet (List.map (subst id value) exps) | E_id id' -> if Id.compare id id' = 0 then unaux_exp (exp_of_value value) else E_id id' + | E_lit lit -> E_lit lit | E_cast (typ, exp) -> E_cast (typ, subst id value exp) | E_app (fn, exps) -> E_app (fn, List.map (subst id value) exps) - | _ -> assert false (* TODO *) + | E_app_infix (exp1, op, exp2) -> E_app_infix (subst id value exp1, op, subst id value exp2) + | E_tuple exps -> E_tuple (List.map (subst id value) exps) + | E_assign (lexp, exp) -> E_assign (lexp, subst id value exp) (* Shadowing... *) + | E_let (LB_aux (LB_val (pat, bind), lb_annot), body) -> + (* TODO: Fix shadowing *) + E_let (LB_aux (LB_val (pat, subst id value bind), lb_annot), subst id value body) + | E_if (cond, then_exp, else_exp) -> + E_if (subst id value cond, subst id value then_exp, subst id value else_exp) + | E_vector exps -> E_vector (List.map (subst id value) exps) + | E_return exp -> E_return (subst id value exp) + | E_assert (exp1, exp2) -> E_assert (subst id value exp1, subst id value exp2) + | E_internal_value v -> E_internal_value v + | _ -> failwith ("subst " ^ string_of_exp exp) in wrap e_aux @@ -167,7 +194,12 @@ let rec subst id value (E_aux (e_aux, annot) as exp) = (* 2. Expression Evaluation *) (**************************************************************************) -let rec step (E_aux (e_aux, annot)) = +let unit_exp = E_lit (L_aux (L_unit, Parse_ast.Unknown)) + +let is_value_fexp (FE_aux (FE_Fexp (id, exp), _)) = is_value exp +let value_of_fexp (FE_aux (FE_Fexp (id, exp), _)) = (string_of_id id, value_of_exp exp) + +let rec step (E_aux (e_aux, annot) as orig_exp) = let wrap e_aux' = return (E_aux (e_aux', annot)) in match e_aux with | E_block [] -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown))) @@ -183,11 +215,38 @@ let rec step (E_aux (e_aux, annot)) = | E_if (exp, then_exp, else_exp) -> step exp >>= fun exp' -> wrap (E_if (exp', then_exp, else_exp)) - | E_assert (exp, msg) when is_true exp -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown))) + | E_assert (exp, msg) when is_true exp -> wrap unit_exp | E_assert (exp, msg) when is_false exp -> assertion_failed "FIXME" | E_assert (exp, msg) -> step exp >>= fun exp' -> wrap (E_assert (exp', msg)) + | E_vector exps -> + let evaluated, unevaluated = Util.take_drop is_value exps in + begin + match unevaluated with + | exp :: exps -> + step exp >>= fun exp' -> wrap (E_vector (evaluated @ exp' :: exps)) + | [] -> return (exp_of_value (V_vector (List.map value_of_exp evaluated))) + end + + (* Special rules for short circuting boolean operators *) + | E_app (id, [x; y]) when (string_of_id id = "and_bool" || string_of_id id = "or_bool") && not (is_value x) -> + step x >>= fun x' -> wrap (E_app (id, [x'; y])) + | E_app (id, [x; y]) when string_of_id id = "and_bool" && is_false x -> + return (exp_of_value (V_bool false)) + | E_app (id, [x; y]) when string_of_id id = "or_bool" && is_true x -> + return (exp_of_value (V_bool true)) + + | E_let (LB_aux (LB_val (pat, bind), lb_annot), body) when not (is_value bind) -> + step bind >>= fun bind' -> wrap (E_let (LB_aux (LB_val (pat, bind'), lb_annot), body)) + | E_let (LB_aux (LB_val (pat, bind), lb_annot), body) -> + let matched, bindings = pattern_match pat (value_of_exp bind) in + if matched then + return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings)) + else + failwith "Match failure" + + (* otherwise left-to-right evaluation order for function applications *) | E_app (id, exps) -> let evaluated, unevaluated = Util.take_drop is_value exps in begin @@ -199,7 +258,8 @@ let rec step (E_aux (e_aux, annot)) = return (exp_of_value (V_ctor (string_of_id id, List.map value_of_exp evaluated))) | [] when Env.is_extern id (env_of_annot annot) "interpreter" -> begin - let primop = StringMap.find (Env.get_extern id (env_of_annot annot) "interpreter") primops in + let extern = Env.get_extern id (env_of_annot annot) "interpreter" in + let primop = try StringMap.find extern primops with Not_found -> failwith ("No primop " ^ extern) in return (exp_of_value (primop (List.map value_of_exp evaluated))) end | [] -> liftM exp_of_value (call id (List.map value_of_exp evaluated)) @@ -211,7 +271,7 @@ let rec step (E_aux (e_aux, annot)) = | E_app_infix (x, id, y) -> step x >>= fun x' -> wrap (E_app_infix (x', id, y)) - | E_return exp when is_value exp -> final (value_of_exp exp) + | E_return exp when is_value exp -> early_return (value_of_exp exp) | E_return exp -> step exp >>= fun exp' -> wrap (E_return exp') | E_tuple exps -> @@ -238,6 +298,76 @@ let rec step (E_aux (e_aux, annot)) = | E_throw exp when is_value exp -> throw (value_of_exp exp) | E_throw exp -> step exp >>= fun exp' -> wrap (E_throw exp') + | E_id id -> + begin + let open Type_check in + gets >>= fun (lstate, gstate) -> + match Env.lookup_id id (env_of_annot annot) with + | Register _ -> + let exp = + try exp_of_value (Bindings.find id gstate.registers) with + | Not_found -> + let exp = mk_exp (E_app (mk_id ("undefined_" ^ string_of_typ (typ_of orig_exp)), [mk_exp (E_lit (mk_lit (L_unit)))])) in + Type_check.check_exp (env_of_annot annot) exp (typ_of orig_exp) + in + return exp + | Local (Mutable, _) -> return (exp_of_value (Bindings.find id lstate.locals)) + | _ -> failwith "id" + end + + | E_record (FES_aux (FES_Fexps (fexps, flag), fes_annot)) -> + let evaluated, unevaluated = Util.take_drop is_value_fexp fexps in + begin + match unevaluated with + | FE_aux (FE_Fexp (id, exp), fe_annot) :: fexps -> + step exp >>= fun exp' -> + wrap (E_record (FES_aux (FES_Fexps (evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps, flag), fes_annot))) + | [] -> + List.map value_of_fexp fexps + |> List.fold_left (fun record (field, v) -> StringMap.add field v record) StringMap.empty + |> (fun record -> V_record record) + |> exp_of_value + |> return + end + + | E_record_update (exp, fexps) when not (is_value exp) -> + step exp >>= fun exp' -> wrap (E_record_update (exp', fexps)) + | E_record_update (record, FES_aux (FES_Fexps (fexps, flag), fes_annot)) -> + let evaluated, unevaluated = Util.take_drop is_value_fexp fexps in + begin + match unevaluated with + | FE_aux (FE_Fexp (id, exp), fe_annot) :: fexps -> + step exp >>= fun exp' -> + wrap (E_record_update (record, FES_aux (FES_Fexps (evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps, flag), fes_annot))) + | [] -> + List.map value_of_fexp fexps + |> List.fold_left (fun record (field, v) -> StringMap.add field v record) (coerce_record (value_of_exp record)) + |> (fun record -> V_record record) + |> exp_of_value + |> return + end + + | E_assign (lexp, exp) when not (is_value exp) -> step exp >>= fun exp' -> wrap (E_assign (lexp, exp')) + | E_assign (LEXP_aux (LEXP_memory (id, args), _), exp) -> wrap (E_app (id, args @ [exp])) + | E_assign (LEXP_aux (LEXP_field (lexp, id), _), exp) -> + let open Type_check in + let lexp_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp lexp)) in + let ul = (Parse_ast.Unknown, None) in + let exp' = E_aux (E_record_update (lexp_exp, FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), ul)], false), ul)), ul) in + wrap (E_assign (lexp, exp')) + | E_assign (LEXP_aux (LEXP_id id, _), exp) | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) -> + begin + let open Type_check in + gets >>= fun (lstate, gstate) -> + match Env.lookup_id id (env_of_annot annot) with + | Register _ -> + puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp + | Local (Mutable, _) | Unbound -> + puts ({ lstate with locals = Bindings.add id (value_of_exp exp) lstate.locals }, gstate) >> wrap unit_exp + | _ -> failwith "Assign" + end + | E_assign _ -> assert false + | E_try (exp, pexps) when is_value exp -> return exp | E_try (exp, pexps) -> begin @@ -249,7 +379,7 @@ let rec step (E_aux (e_aux, annot)) = | E_sizeof _ | E_constraint _ -> assert false (* Must be re-written before interpreting *) - | _ -> assert false (* TODO *) + | _ -> failwith ("Unimplemented " ^ string_of_exp orig_exp) and combine _ v1 v2 = match (v1, v2) with @@ -258,6 +388,22 @@ and combine _ v1 v2 = | None, Some v2 -> Some v2 | Some v1, Some v2 -> failwith "Pattern binds same identifier twice!" +and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) = + match lexp_aux with + | LEXP_id id -> mk_exp (E_id id) + | LEXP_memory (f, args) -> mk_exp (E_app (f, args)) + | LEXP_cast (typ, id) -> mk_exp (E_cast (typ, mk_exp (E_id id))) + | LEXP_tup lexps -> mk_exp (E_tuple (List.map exp_of_lexp lexps)) + | LEXP_vector (lexp, exp) -> mk_exp (E_vector_access (exp_of_lexp lexp, exp)) + | LEXP_vector_range (lexp, exp1, exp2) -> mk_exp (E_vector_subrange (exp_of_lexp lexp, exp1, exp2)) + | LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id)) + +and lexp_assign (LEXP_aux (lexp_aux, _) as lexp) value = + print_endline ("Assigning: " ^ string_of_lexp lexp ^ " to " ^ string_of_value value |> Util.yellow |> Util.clear); + match lexp_aux with + | LEXP_id id -> Bindings.singleton id value + | _ -> failwith "Unhandled lexp_assign" + and pattern_match (P_aux (p_aux, _) as pat) value = print_endline ("Matching: " ^ string_of_pat pat ^ " with " ^ string_of_value value |> Util.yellow |> Util.clear); match p_aux with @@ -294,27 +440,38 @@ let rec get_fundef id (Defs defs) = | (DEF_fundef fdef) :: _ when Id.compare id (id_of_fundef fdef) = 0 -> fdef | _ :: defs -> get_fundef id (Defs defs) -let rec untilM p f x = - if p x then - return x - else - f (return x) >>= fun x' -> untilM p f x' - -type trace = - | Done of value - | Step of (Type_check.tannot exp) monad * (value -> (Type_check.tannot exp) monad) list - -let rec eval_exp ast m = - match m with - | Pure v when is_value v -> Done (value_of_exp v) - | Pure exp' -> - Pretty_print_sail2.pretty_sail stdout (Pretty_print_sail2.doc_exp exp'); - print_newline (); - Step (step exp', []) - | Yield (Call (id, vals, cont)) -> - print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear); - let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in - let body = exp_of_fundef (get_fundef id ast) arg in - Step (return body, [cont]) - | _ -> assert false - +let stack_cont (_, _, cont) = cont +let stack_string (str, _, _) = str +let stack_state (_, lstate, _) = lstate + +type frame = + | Done of state * value + | Step of string * state * (Type_check.tannot exp) monad * (string * lstate * (value -> (Type_check.tannot exp) monad)) list + +let rec eval_frame ast = function + | Done (state, v) -> Done (state, v) + | Step (out, state, m, stack) -> + match (m, stack) with + | Pure v, [] when is_value v -> Done (state, value_of_exp v) + | Pure v, (head :: stack') when is_value v -> + print_endline ("Returning value: " ^ string_of_value (value_of_exp v) |> Util.cyan |> Util.clear); + Step (stack_string head, (stack_state head, snd state), stack_cont head (value_of_exp v), stack') + | Pure exp', _ -> + let out' = Pretty_print_sail2.to_string (Pretty_print_sail2.doc_exp exp') in + Step (out', state, step exp', stack) + | Yield (Call(id, vals, cont)), _ -> + print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear); + let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in + let body = exp_of_fundef (get_fundef id ast) arg in + Step ("", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack) + | Yield (Gets cont), _ -> + eval_frame ast (Step (out, state, cont state, stack)) + | Yield (Puts (state', cont)), _ -> + eval_frame ast (Step (out, state', cont (), stack)) + | Yield (Early_return v), [] -> Done (state, v) + | Yield (Early_return v), (head :: stack') -> + print_endline ("Returning value: " ^ string_of_value v |> Util.cyan |> Util.clear); + Step (stack_string head, (stack_state head, snd state), stack_cont head v, stack') + | Yield (Assertion_failed msg), _ -> + failwith msg + | _ -> assert false diff --git a/src/isail.ml b/src/isail.ml index 97b92809..88835b8a 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -56,7 +56,7 @@ open Interpreter open Pretty_print_sail2 type mode = - | Evaluation of trace + | Evaluation of frame | Normal let current_mode = ref Normal @@ -86,14 +86,14 @@ let clear str = str ^ termcode 0 let sail_logo = let banner str = str |> bold |> red |> clear in - [ {| ___ ___ ___ ___ |}; - {| /\ \ /\ \ /\ \ /\__\ |}; - {| /::\ \ /::\ \ _\:\ \ /:/ / |}; - {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |}; - {| \:\:\/__/ \/\::/ / \::/\/__/ \:\ \ |}; - {| \::/ / /:/ / \:\__\ \:\__\ |}; - {| \/__/ \/__/ \/__/ \/__/ |}; - {| |} + [ " ___ ___ ___ ___ "; + " /\\ \\ /\\ \\ /\\ \\ /\\__\\"; + " /::\\ \\ /::\\ \\ _\\:\\ \\ /:/ /"; + " /\\:\\:\\__\\ /::\\:\\__\\ /\\/::\\__\\ /:/__/ "; + " \\:\\:\\/__/ \\/\\::/ / \\::/\\/__/ \\:\\ \\ "; + " \\::/ / /:/ / \\:\\__\\ \\:\\__\\"; + " \\/__/ \\/__/ \\/__/ \\/__/"; + "" ] |> List.map banner @@ -127,31 +127,27 @@ let handle_input input = | _ -> print_endline ("Unrecognised command " ^ input) else if input <> "" then let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord input) in - current_mode := Evaluation (eval_exp !interactive_ast (return exp)) + current_mode := Evaluation (eval_frame !interactive_ast (Step ("", initial_state, return exp, []))) else () end - | Evaluation trace -> + | Evaluation frame -> begin - match trace with - | Done v -> + match frame with + | Done (_, v) -> print_endline ("Result = " ^ Value.string_of_value v); current_mode := Normal - | Step (exp, stack) -> - let next = match eval_exp !interactive_ast exp with - | Step (exp', stack') -> Evaluation (Step (exp', stack' @ stack)) - | Done v when stack = [] -> - print_endline ("Result = " ^ Value.string_of_value v); - Normal - | Done v -> - print_endline ("Returning: " ^ Value.string_of_value v |> Util.cyan |> Util.clear); - Evaluation (Step (List.hd stack v, List.tl stack)) - in - current_mode := next + | Step (out, _, _, stack) -> + let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear in + List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline code; print_endline sep); + print_endline out; + current_mode := Evaluation (eval_frame !interactive_ast frame) end let () = + List.iter print_endline sail_logo; + (* Auto complete function names based on val specs *) LNoise.set_completion_callback begin @@ -177,5 +173,5 @@ let () = LNoise.history_set ~max_length:100 |> ignore; if !opt_interactive then - (List.iter print_endline sail_logo; user_input handle_input) + user_input handle_input else () diff --git a/src/lexer2.mll b/src/lexer2.mll index e2361a04..b293046f 100644 --- a/src/lexer2.mll +++ b/src/lexer2.mll @@ -130,6 +130,7 @@ let kw_table = ("inc", (fun _ -> Inc)); ("let", (fun x -> Let_)); ("var", (fun _ -> Var)); + ("ref", (fun _ -> Ref)); ("record", (fun _ -> Record)); ("Int", (fun x -> Int)); ("Order", (fun x -> Order)); @@ -171,6 +172,8 @@ let kw_table = ("escape", (fun x -> Escape)); ] + + } let ws = [' ''\t']+ diff --git a/src/parse_ast.ml b/src/parse_ast.ml index df4c2d2c..83b116a2 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -267,6 +267,7 @@ exp_aux = (* Expression *) E_block of (exp) list (* block (parsing conflict with structs?) *) | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *) | E_id of id (* identifier *) + | E_ref of id | E_lit of lit (* literal constant *) | E_cast of atyp * exp (* cast *) | E_app of id * (exp) list (* function application *) diff --git a/src/parser2.mly b/src/parser2.mly index 74812d1e..ebe829c2 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -69,6 +69,10 @@ let string_of_id = function | Id_aux (Id str, _) -> str | Id_aux (DeIid str, _) -> str +let prepend_id str1 = function + | Id_aux (Id str2, loc) -> Id_aux (Id (str1 ^ str2), loc) + | _ -> assert false + let mk_id i n m = Id_aux (i, loc n m) let mk_kid str n m = Kid_aux (Var str, loc n m) @@ -152,7 +156,7 @@ let rec desugar_rchain chain s e = %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union With Val Constraint Throw Try Catch Exit %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape -%token Repeat Until While Do Record Mutual Var +%token Repeat Until While Do Record Mutual Var Ref %nonassoc Then %nonassoc Else @@ -513,8 +517,11 @@ atomic_typ: | id Lparen typ_list Rparen { mk_typ (ATyp_app ($1, $3)) $startpos $endpos } | Register Lparen typ Rparen - { let register_id = mk_id (Id "register") $startpos $endpos in + { let register_id = mk_id (Id "register") $startpos($1) $endpos($1) in mk_typ (ATyp_app (register_id, [$3])) $startpos $endpos } + | Ref Lparen typ Rparen + { let ref_id = mk_id (Id "ref") $startpos($1) $endpos($1) in + mk_typ (ATyp_app (ref_id, [$3])) $startpos $endpos } | Lparen typ Rparen { $2 } | Lparen typ Comma typ_list Rparen @@ -953,12 +960,18 @@ atomic_exp: { mk_exp (E_cast ($3, $1)) $startpos $endpos } | lit { mk_exp (E_lit $1) $startpos $endpos } + | id MinusGt id Lparen exp_list Rparen + { mk_exp (E_app (prepend_id "_mod_" $3, mk_exp (E_ref $1) $startpos($1) $endpos($1) :: $5)) $startpos $endpos } + | atomic_exp Dot id Lparen exp_list Rparen + { mk_exp (E_app (prepend_id "_mod_" $3, $1 :: $5)) $startpos $endpos } | atomic_exp Dot id { mk_exp (E_field ($1, $3)) $startpos $endpos } | id { mk_exp (E_id $1) $startpos $endpos } | kid { mk_exp (E_sizeof (mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos } + | Ref id + { mk_exp (E_ref $2) $startpos $endpos } | id Unit { mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos } | id Lparen exp_list Rparen diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 3827376f..8f789c14 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -152,7 +152,6 @@ let effectful (Effect_aux (Effect_set effs, _)) = effectful_set effs let is_regtyp (Typ_aux (typ, _)) env = match typ with | Typ_app(id, _) when string_of_id id = "register" -> true - | Typ_id(id) when Env.is_regtyp id env -> true | _ -> false let doc_nexp_lem nexp = @@ -720,18 +719,6 @@ let doc_exp_lem, doc_let_lem = | E_field((E_aux(_,(l,fannot)) as fexp),id) -> let ft = typ_of_annot (l,fannot) in (match fannot with - | Some(env, (Typ_aux (Typ_id tid, _)), _) - | Some(env, (Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]), _)), _) - when Env.is_regtyp tid env -> - let t = (* Env.base_typ_of (env_of full_exp) *) (typ_of full_exp) in - let eff = effect_of full_exp in - let field_f = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in - let (ta,aexp_needed) = - if typ_needs_printed t - then (doc_tannot_lem sequential mwords (effectful eff) t, true) - else (empty, aexp_needed) in - let epp = field_f ^^ space ^^ (expY fexp) in - if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta) | Some(env, (Typ_aux (Typ_id tid, _)), _) when Env.is_record tid env -> let fname = if prefix_recordtype @@ -1336,9 +1323,6 @@ let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) = else let env = env_of_annot annot in (match typ with - | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env -> - separate space [string "let";doc_id_lem id;equals; - string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline | _ -> let rt = Env.base_typ_of env typ in if is_vector_typ rt then diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index 0f1ee016..22b6e9ee 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -531,3 +531,8 @@ let doc_defs (Defs(defs)) = let pp_defs f d = ToChannel.pretty 1. 80 f (doc_defs d) let pretty_sail f doc = ToChannel.pretty 1. 120 f doc + +let to_string doc = + let b = Buffer.create 120 in + ToBuffer.pretty 1. 120 b doc; + Buffer.contents b diff --git a/src/process_file.ml b/src/process_file.ml index 68e5786e..d57127a4 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -121,7 +121,7 @@ let opt_dno_cast = ref false let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t = let ienv = if !opt_dno_cast then Type_check.Env.no_casts Type_check.initial_env else Type_check.initial_env in let ast, env = Type_check.check ienv defs in - let () = if !opt_ddump_tc_ast then Pretty_print.pp_defs stdout ast else () in + let () = if !opt_ddump_tc_ast then Pretty_print_sail2.pp_defs stdout ast else () in let () = if !opt_just_check then exit 0 else () in (ast, env) diff --git a/src/rewrites.ml b/src/rewrites.ml index 25953776..a28352f5 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1389,21 +1389,6 @@ let rec rewrite_lexp_to_rhs (do_rewrite : tannot lexp -> bool) ((LEXP_aux(lexp,( let (LEXP_aux (_, lannot)) = lexp in let env = env_of_annot lannot in match Env.expand_synonyms env (typ_of_annot lannot) with - | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id regtyp_id, _)), _)]), _) - | Typ_aux (Typ_id regtyp_id, _) when Env.is_regtyp regtyp_id env -> - let base, top, ranges = Env.get_regtyp regtyp_id env in - let range, _ = - try List.find (fun (_, fid) -> Id.compare fid id = 0) ranges with - | Not_found -> - raise (Reporting_basic.err_typ l ("Field " ^ string_of_id id ^ " doesn't exist for register type " ^ string_of_id regtyp_id)) - in - let lexp_exp = E_aux (E_app (mk_id ("cast_" ^ string_of_id regtyp_id), [lexp_to_exp lexp]), (l, None)) in - let n, m = match range with - | BF_aux (BF_single n, _) -> n, n - | BF_aux (BF_range (n, m), _) -> n, m - | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le)) in - let rhs' exp = rhs (E_aux (E_vector_update_subrange (lexp_exp, simple_num l n, simple_num l m, exp), lannot)) in - (lhs, rhs') | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env -> let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), lannot)))) diff --git a/src/type_check.ml b/src/type_check.ml index c2467cee..907c23a5 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -307,9 +307,6 @@ module Env : sig val is_register : id -> t -> bool val get_register : id -> t -> typ val add_register : id -> typ -> t -> t - val add_regtyp : id -> Big_int.num -> Big_int.num -> (index_range * id) list -> t -> t - val is_regtyp : id -> t -> bool - val get_regtyp : id -> t -> Big_int.num * Big_int.num * (index_range * id) list val is_mutable : id -> t -> bool val get_constraints : t -> n_constraint list val add_constraint : n_constraint -> t -> t @@ -364,7 +361,6 @@ end = struct locals : (mut * typ) Bindings.t; union_ids : (typquant * typ) Bindings.t; registers : typ Bindings.t; - regtyps : (Big_int.num * Big_int.num * (index_range * id) list) Bindings.t; variants : (typquant * type_union list) Bindings.t; typ_vars : base_kind_aux KBindings.t; typ_synonyms : (t -> typ_arg list -> typ) Bindings.t; @@ -390,7 +386,6 @@ end = struct locals = Bindings.empty; union_ids = Bindings.empty; registers = Bindings.empty; - regtyps = Bindings.empty; variants = Bindings.empty; typ_vars = KBindings.empty; typ_synonyms = Bindings.empty; @@ -430,6 +425,7 @@ end = struct ("atom", [BK_nat]); ("vector", [BK_nat; BK_order; BK_type]); ("register", [BK_type]); + ("ref", [BK_type]); ("bit", []); ("unit", []); ("int", []); @@ -445,7 +441,6 @@ end = struct Bindings.mem id env.typ_synonyms || Bindings.mem id env.variants || Bindings.mem id env.records - || Bindings.mem id env.regtyps || Bindings.mem id env.enums || Bindings.mem id builtin_typs @@ -476,7 +471,7 @@ end = struct fst (Bindings.find id env.variants) else if Bindings.mem id env.records then fst (Bindings.find id env.records) - else if Bindings.mem id env.enums || Bindings.mem id env.regtyps then + else if Bindings.mem id env.enums then mk_typquant [] else if Bindings.mem id env.typ_synonyms then typ_error (id_loc id) ("Cannot infer kind of type synonym " ^ string_of_id id) @@ -708,7 +703,7 @@ end = struct | Mutable -> true | Immutable -> false with - | Not_found -> typ_error (id_loc id) ("No local binding found for " ^ string_of_id id) + | Not_found -> false let string_of_mtyp (mut, typ) = match mut with | Immutable -> string_of_typ typ @@ -768,29 +763,6 @@ end = struct let get_casts env = env.casts - let check_index_range cmp f t (BF_aux (ir, l)) = - match ir with - | BF_single n -> - if cmp f n && cmp n t - then n - else typ_error l ("Badly ordered index range: " ^ string_of_list ", " Big_int.to_string [f; n; t]) - | BF_range (n1, n2) -> - if cmp f n1 && cmp n1 n2 && cmp n2 t - then n2 - else typ_error l ("Badly ordered index range: " ^ string_of_list ", " Big_int.to_string [f; n1; n2; t]) - | BF_concat _ -> typ_error l "Index range concatenation currently unsupported" - - let rec check_index_ranges ids cmp base top = function - | [] -> () - | ((range, id) :: ranges) -> - if IdSet.mem id ids - then typ_error (id_loc id) ("Duplicate id " ^ string_of_id id ^ " in register typedef") - else - begin - let base' = check_index_range cmp base top range in - check_index_ranges (IdSet.add id ids) cmp base' top ranges - end - let add_register id typ env = wf_typ env typ; if Bindings.mem id env.registers @@ -801,24 +773,6 @@ end = struct { env with registers = Bindings.add id typ env.registers } end - let add_regtyp id base top ranges env = - if Bindings.mem id env.regtyps - then typ_error (id_loc id) ("Register type " ^ string_of_id id ^ " is already bound") - else - begin - typ_print ("Adding register type " ^ string_of_id id); - if Big_int.greater base top - then check_index_ranges IdSet.empty Big_int.greater (Big_int.add base (Big_int.of_int 1)) (Big_int.sub top (Big_int.of_int 1)) ranges - else check_index_ranges IdSet.empty Big_int.less (Big_int.sub base (Big_int.of_int 1)) (Big_int.add top (Big_int.of_int 1)) ranges; - { env with regtyps = Bindings.add id (base, top, ranges) env.regtyps } - end - - let is_regtyp id env = Bindings.mem id env.regtyps - - let get_regtyp id env = - try Bindings.find id env.regtyps with - | Not_found -> typ_error (id_loc id) (string_of_id id ^ " is not a register type") - let get_locals env = env.locals let lookup_id id env = @@ -923,16 +877,11 @@ end = struct rewrap (Typ_fn (aux t1, aux t2, eff)) | Typ_tup ts -> rewrap (Typ_tup (List.map aux ts)) - | Typ_app (register, [Typ_arg_aux (Typ_arg_typ rtyp,_)]) - when string_of_id register = "register" -> + | Typ_app (r, [Typ_arg_aux (Typ_arg_typ rtyp,_)]) + when string_of_id r = "register" || string_of_id r = "ref" -> aux rtyp | Typ_app (id, targs) -> rewrap (Typ_app (id, List.map aux_arg targs)) - | Typ_id id when is_regtyp id env -> - let base, top, ranges = get_regtyp id env in - let len = Big_int.succ (Big_int.abs (Big_int.sub top base)) in - vector_typ (nconstant len) (get_default_order env) bit_typ - (* TODO registers with non-default order? non-bitvector registers? *) | t -> rewrap t and aux_arg (Typ_arg_aux (targ,a)) = let rewrap targ = Typ_arg_aux (targ,a) in @@ -2173,11 +2122,6 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ if is_typ_monomorphic typ || Env.polymorphic_undefineds env then annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef]) else typ_error l ("Type " ^ string_of_typ typ ^ " failed undefined monomorphism restriction") - (* This rule allows registers of type t to be passed by name with type register<t>*) - | E_id reg, Typ_app (id, [Typ_arg_aux (Typ_arg_typ arg_typ, _)]) - when string_of_id id = "register" && Env.is_register reg env -> - let rtyp = Env.get_register reg env in - subtyp l env rtyp arg_typ; annot_exp (E_id reg) typ (* CHECK: is this subtyp the correct way around? *) | E_id id, _ when is_union_id id env -> begin match Env.lookup_id id env with @@ -2513,24 +2457,6 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as let regtyp, inferred_flexp, is_register = infer_flexp flexp in typ_debug ("REGTYP: " ^ string_of_typ regtyp ^ " / " ^ string_of_typ (Env.expand_synonyms env regtyp)); match Env.expand_synonyms env regtyp with - | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id regtyp_id, _)), _)]), _) - (* FIXME: Almost certainly broken *) - | Typ_aux (Typ_id regtyp_id, _) when Env.is_regtyp regtyp_id env -> - let eff = mk_effect [BE_wreg] in - let base, top, ranges = Env.get_regtyp regtyp_id env in - let range, _ = - try List.find (fun (_, id) -> Id.compare id field = 0) ranges with - | Not_found -> typ_error l ("Field " ^ string_of_id field ^ " doesn't exist for register type " ^ string_of_id regtyp_id) - in - let vec_typ = match range, Env.get_default_order env with - | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) -> - dvector_typ env (nint 1) (mk_typ (Typ_id (mk_id "bit"))) - | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) -> - dvector_typ env (nconstant (Big_int.add (Big_int.sub n m) (Big_int.of_int 1))) (mk_typ (Typ_id (mk_id "bit"))) - | _, _ -> typ_error l "Not implemented this register field type yet..." - in - let checked_exp = crule check_exp env exp vec_typ in - annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp eff, field)) vec_typ) checked_exp, env | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env -> let eff = if is_register then mk_effect [BE_wreg] else no_effect in let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in @@ -2565,6 +2491,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = match lexp_aux with | LEXP_id v -> begin match Env.lookup_id v env with + | Local (Immutable, Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _)) when string_of_id r = "ref" -> + subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env | Local (Immutable, _) | Enum _ | Union _ -> typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v) | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env @@ -2747,31 +2675,6 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = begin let inferred_exp = irule infer_exp env exp in match Env.expand_synonyms env (typ_of inferred_exp) with - (* Accessing a (bit) field of a register *) - | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ ((Typ_aux (Typ_id regtyp, _) as regtyp_aux)), _)]), _) - | (Typ_aux (Typ_id regtyp, _) as regtyp_aux) when Env.is_regtyp regtyp env -> - let base, top, ranges = Env.get_regtyp regtyp env in - let range, _ = - try List.find (fun (_, id) -> Id.compare id field = 0) ranges with - | Not_found -> typ_error l ("Field " ^ string_of_id field ^ " doesn't exist for register type " ^ string_of_id regtyp) - in - let checked_exp = crule check_exp env (strip_exp inferred_exp) regtyp_aux in - begin - match range, Env.get_default_order env with - | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) -> - let vec_typ = dvector_typ env (nint 1) bit_typ in - annot_exp (E_field (checked_exp, field)) vec_typ - | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) -> - let vec_typ = dvector_typ env (nconstant (Big_int.add (Big_int.sub n m) (Big_int.of_int 1))) bit_typ in - annot_exp (E_field (checked_exp, field)) vec_typ - | BF_aux (BF_single n, _), Ord_aux (Ord_inc, _) -> - let vec_typ = dvector_typ env (nint 1) bit_typ in - annot_exp (E_field (checked_exp, field)) vec_typ - | BF_aux (BF_range (n, m), _), Ord_aux (Ord_inc, _) -> - let vec_typ = dvector_typ env (nconstant (Big_int.add (Big_int.sub m n) (Big_int.of_int 1))) bit_typ in - annot_exp (E_field (checked_exp, field)) vec_typ - | _, _ -> typ_error l "Invalid register field type" - end (* Accessing a field of a record *) | Typ_aux (Typ_id rectyp, _) as typ when Env.is_record rectyp env -> begin @@ -2911,6 +2814,12 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let tpat, env = bind_pat env pat ptyp in let inferred_exp = irule infer_exp env exp in annot_exp (E_let (LB_aux (LB_val (tpat, bind_exp), (let_loc, None)), inferred_exp)) (typ_of inferred_exp) + | E_ref id when Env.is_mutable id env -> + let (_, typ) = Bindings.find id (Env.get_locals env) in + annot_exp (E_ref id) (ref_typ typ) + | E_ref id when Env.is_register id env -> + let typ = Env.get_register id env in + annot_exp (E_ref id) (register_typ typ) | _ -> typ_error l ("Cannot infer type of: " ^ string_of_exp exp) and infer_funapp l env f xs ret_ctx_typ = fst (infer_funapp' l env f (Env.get_val_spec f env) xs ret_ctx_typ) @@ -3112,6 +3021,7 @@ and propagate_exp_effect_aux = function let p_xs = List.map propagate_exp_effect xs in E_nondet p_xs, collect_effects p_xs | E_id id -> E_id id, no_effect + | E_ref id -> E_ref id, no_effect | E_lit lit -> E_lit lit, no_effect | E_cast (typ, exp) -> let p_exp = propagate_exp_effect exp in @@ -3463,6 +3373,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) = | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, ext_opt, is_cast) -> let env = match ext_opt "smt" with Some op -> Env.add_smt_op id op env | None -> env in Env.wf_typ (add_typquant quants env) typ; + typ_debug "CHECKED WELL-FORMED VAL SPEC"; let env = (* match ext_opt with | None -> env @@ -3472,7 +3383,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) = let env = if is_cast then Env.add_cast id env else env in (id, quants, typ, env) in - [DEF_spec (VS_aux (vs, (l, None)))], Env.add_val_spec id (quants, Env.expand_synonyms env typ) env + [DEF_spec (VS_aux (vs, (l, None)))], Env.add_val_spec id (quants, Env.expand_synonyms (add_typquant quants env) typ) env let check_default env (DT_aux (ds, l)) = match ds with @@ -3483,23 +3394,6 @@ let check_default env (DT_aux (ds, l)) = (* This branch allows us to write something like: default forall Nat 'n. [|'n|] name... what does this even mean?! *) | DT_typ (typschm, id) -> typ_error l ("Unsupported default construct") -let check_register env id base top ranges = - match base, top with - | Nexp_aux (Nexp_constant basec, _), Nexp_aux (Nexp_constant topc, _) -> - let no_typq = TypQ_aux (TypQ_tq [], Parse_ast.Unknown) (* Maybe could be TypQ_no_forall? *) in - (* FIXME: wrong for default Order inc? *) - let vec_typ = dvector_typ env (nconstant (Big_int.add (Big_int.sub basec topc) (Big_int.of_int 1))) bit_typ in - let cast_typ = mk_typ (Typ_fn (mk_id_typ id, vec_typ, no_effect)) in - let cast_to_typ = mk_typ (Typ_fn (vec_typ, mk_id_typ id, no_effect)) in - env - |> Env.add_regtyp id basec topc ranges - (* |> Env.add_typ_synonym id (fun _ -> vec_typ) *) - |> Env.add_val_spec (mk_id ("cast_" ^ string_of_id id)) (no_typq, cast_typ) - |> Env.add_cast (mk_id ("cast_" ^ string_of_id id)) - |> Env.add_val_spec (mk_id ("cast_to_" ^ string_of_id id)) (no_typq, cast_to_typ) - |> Env.add_cast (mk_id ("cast_to_" ^ string_of_id id)) - | _, _ -> typ_error (id_loc id) "Num expressions in register type declaration do not evaluate to constants" - let kinded_id_arg kind_id = let typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) in match kind_id with @@ -3549,7 +3443,9 @@ let mk_synonym typq typ = let typ, ncs = subst_args kopts args in if List.for_all (prove env) ncs then typ - else typ_error Parse_ast.Unknown "Could not prove constraints in type synonym" + else typ_error Parse_ast.Unknown ("Could not prove constraints " ^ string_of_list ", " string_of_n_constraint ncs + ^ " in type synonym " ^ string_of_typ typ + ^ " with " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)) let check_typedef env (TD_aux (tdef, (l, _))) = let td_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Typedef") in @@ -3567,7 +3463,6 @@ let check_typedef env (TD_aux (tdef, (l, _))) = [DEF_type (TD_aux (tdef, (l, None)))], env | TD_enum(id, nmscm, ids, _) -> [DEF_type (TD_aux (tdef, (l, None)))], Env.add_enum id ids env - | TD_register(id, base, top, ranges) -> [DEF_type (TD_aux (tdef, (l, Some (env, unit_typ, no_effect))))], check_register env id base top ranges let check_kinddef env (KD_aux (kdef, (l, _))) = let kd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented kind def") in diff --git a/src/type_check.mli b/src/type_check.mli index 8f0cd98c..33615e43 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -84,15 +84,10 @@ module Env : sig val get_register : id -> t -> typ - val get_regtyp : id -> t -> Big_int.num * Big_int.num * (index_range * id) list - (* Return all the identifiers in an enumeration. Throws a type error if the enumeration doesn't exist. *) val get_enum : id -> t -> id list - (* Returns true if id is a register type, false otherwise *) - val is_regtyp : id -> t -> bool - val get_locals : t -> (mut * typ) Bindings.t val add_local : id -> mut * typ -> t -> t diff --git a/src/util.ml b/src/util.ml index bd083a8b..51ed8926 100644 --- a/src/util.ml +++ b/src/util.ml @@ -392,4 +392,5 @@ let green str = termcode 92 ^ str let yellow str = termcode 93 ^ str let red str = termcode 91 ^ str let cyan str = termcode 96 ^ str +let blue str = termcode 94 ^ str let clear str = str ^ termcode 0 diff --git a/src/util.mli b/src/util.mli index bdf6e594..39bc8a19 100644 --- a/src/util.mli +++ b/src/util.mli @@ -238,4 +238,5 @@ val green : string -> string val red : string -> string val yellow : string -> string val cyan : string -> string +val blue : string -> string val clear : string -> string diff --git a/src/value.ml b/src/value.ml index f49b230c..59dadafe 100644 --- a/src/value.ml +++ b/src/value.ml @@ -50,33 +50,19 @@ module Big_int = Nat_big_num -type bit = B0 | B1 +module StringMap = Map.Make(String) type value = | V_vector of value list | V_list of value list | V_int of Big_int.num | V_bool of bool - | V_bit of bit + | V_bit of Sail_lib.bit | V_tuple of value list | V_unit | V_string of string | V_ctor of string * value list - -let rec string_of_value = function - | V_vector _ -> "VEC" - | V_bool true -> "true" - | V_bool false -> "false" - | V_bit B0 -> "bitzero" - | V_bit B1 -> "bitone" - | V_int n -> Big_int.to_string n - | V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" - | V_list vals -> "[" ^ Util.string_of_list ", " string_of_value vals ^ "]" - | V_unit -> "()" - | V_string str -> "\"" ^ str ^ "\"" - | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" - -let eq_value v1 v2 = string_of_value v1 = string_of_value v2 + | V_record of value StringMap.t let coerce_bit = function | V_bit b -> b @@ -90,6 +76,10 @@ let coerce_bool = function | V_bool b -> b | _ -> assert false +let coerce_record = function + | V_record record -> record + | _ -> assert false + let and_bool = function | [v1; v2] -> V_bool (coerce_bool v1 && coerce_bool v2) | _ -> assert false @@ -98,12 +88,14 @@ let or_bool = function | [v1; v2] -> V_bool (coerce_bool v1 || coerce_bool v2) | _ -> assert false -let print = function - | [v] -> print_endline (string_of_value v |> Util.red |> Util.clear); V_unit - | _ -> assert false - let tuple_value (vs : value list) : value = V_tuple vs +let mk_vector (bits : Sail_lib.bit list) : value = V_vector (List.map (fun bit -> V_bit bit) bits) + +let coerce_bit = function + | V_bit b -> b + | _ -> assert false + let coerce_tuple = function | V_tuple vs -> vs | _ -> assert false @@ -111,6 +103,11 @@ let coerce_tuple = function let coerce_listlike = function | V_tuple vs -> vs | V_list vs -> vs + | V_unit -> [] + | _ -> assert false + +let coerce_int = function + | V_int i -> i | _ -> assert false let coerce_cons = function @@ -118,9 +115,140 @@ let coerce_cons = function | V_list [] -> None | _ -> assert false +let coerce_gv = function + | V_vector vs -> vs + | _ -> assert false + +let coerce_bv = function + | V_vector vs -> List.map coerce_bit vs + | _ -> assert false + +let coerce_string = function + | V_string str -> str + | _ -> assert false + let unit_value = V_unit -module StringMap = Map.Make(String) +let value_eq_int = function + | [v1; v2] -> V_bool (Sail_lib.eq_int (coerce_int v1, coerce_int v2)) + | _ -> failwith "value eq_int" + +let value_lteq = function + | [v1; v2] -> V_bool (Sail_lib.lteq (coerce_int v1, coerce_int v2)) + | _ -> failwith "value lteq" + +let value_gteq = function + | [v1; v2] -> V_bool (Sail_lib.gteq (coerce_int v1, coerce_int v2)) + | _ -> failwith "value gteq" + +let value_lt = function + | [v1; v2] -> V_bool (Sail_lib.lt (coerce_int v1, coerce_int v2)) + | _ -> failwith "value lt" + +let value_gt = function + | [v1; v2] -> V_bool (Sail_lib.gt (coerce_int v1, coerce_int v2)) + | _ -> failwith "value gt" + +let value_eq_list = function + | [v1; v2] -> V_bool (Sail_lib.eq_list (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value eq_list" + +let value_eq_string = function + | [v1; v2] -> V_bool (Sail_lib.eq_string (coerce_string v1, coerce_string v2)) + | _ -> failwith "value eq_string" + +let value_length = function + | [v] -> V_int (coerce_gv v |> List.length |> Big_int.of_int) + | _ -> failwith "value length" + +let value_subrange = function + | [v1; v2; v3] -> mk_vector (Sail_lib.subrange (coerce_bv v1, coerce_int v2, coerce_int v3)) + | _ -> failwith "value subrange" + +let value_access = function + | [v1; v2] -> Sail_lib.access (coerce_gv v1, coerce_int v2) + | _ -> failwith "value access" + +let value_update = function + | [v1; v2; v3] -> V_vector (Sail_lib.update (coerce_gv v1, coerce_int v2, v3)) + | _ -> failwith "value update" + +let value_update_subrange = function + | [v1; v2; v3; v4] -> mk_vector (Sail_lib.update_subrange (coerce_bv v1, coerce_int v2, coerce_int v3, coerce_bv v4)) + | _ -> failwith "value update_subrange" + +let value_append = function + | [v1; v2] -> V_vector (coerce_gv v1 @ coerce_gv v2) + | _ -> failwith "value append" + +let value_not = function + | [v] -> V_bool (not (coerce_bool v)) + | _ -> failwith "value not" + +let value_not_vec = function + | [v] -> mk_vector (Sail_lib.not_vec (coerce_bv v)) + | _ -> failwith "value not_vec" + +let value_and_vec = function + | [v1; v2] -> mk_vector (Sail_lib.and_vec (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value not_vec" + +let value_or_vec = function + | [v1; v2] -> mk_vector (Sail_lib.or_vec (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value not_vec" + +let value_uint = function + | [v] -> V_int (Sail_lib.uint (coerce_bv v)) + | _ -> failwith "value uint" + +let value_sint = function + | [v] -> V_int (Sail_lib.sint (coerce_bv v)) + | _ -> failwith "value sint" + +let value_get_slice_int = function + | [v1; v2; v3] -> mk_vector (Sail_lib.get_slice_int (coerce_int v1, coerce_int v2, coerce_int v3)) + | _ -> failwith "value get_slice_int" + +let value_add = function + | [v1; v2] -> V_int (Sail_lib.add (coerce_int v1, coerce_int v2)) + | _ -> failwith "value add" + +let value_sub = function + | [v1; v2] -> V_int (Sail_lib.sub (coerce_int v1, coerce_int v2)) + | _ -> failwith "value sub" + +let value_replicate_bits = function + | [v1; v2] -> mk_vector (Sail_lib.replicate_bits (coerce_bv v1, coerce_int v2)) + | _ -> failwith "value replicate_bits" + +let rec string_of_value = function + | V_vector vs -> Sail_lib.string_of_bits (List.map coerce_bit vs) + | V_bool true -> "true" + | V_bool false -> "false" + | V_bit B0 -> "bitzero" + | V_bit B1 -> "bitone" + | V_int n -> Big_int.to_string n + | V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" + | V_list vals -> "[" ^ Util.string_of_list ", " string_of_value vals ^ "]" + | V_unit -> "()" + | V_string str -> "\"" ^ str ^ "\"" + | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" + | V_record record -> + "{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}" + +let eq_value v1 v2 = string_of_value v1 = string_of_value v2 + +let value_eq_anything = function + | [v1; v2] -> V_bool (eq_value v1 v2) + | _ -> failwith "value eq_anything" + +let value_print = function + | [v] -> print_endline (string_of_value v |> Util.red |> Util.clear); V_unit + | _ -> assert false + +let value_undefined_vector = function + | [v1; v2; v3] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, coerce_int v2, v3)) + | _ -> failwith "value undefined_vector" let primops = List.fold_left @@ -128,5 +256,35 @@ let primops = StringMap.empty [ ("and_bool", and_bool); ("or_bool", or_bool); - ("print_endline", print); + ("print_endline", value_print); + ("prerr_endline", value_print); + ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs))); + ("print_bits", fun [msg; bits] -> print_endline (coerce_string msg ^ string_of_value bits); V_unit); + ("eq_int", value_eq_int); + ("lteq", value_lteq); + ("gteq", value_gteq); + ("lt", value_lt); + ("gt", value_gt); + ("eq_list", value_eq_list); + ("eq_string", value_eq_string); + ("eq_anything", value_eq_anything); + ("length", value_length); + ("subrange", value_subrange); + ("access", value_access); + ("update", value_update); + ("update_subrange", value_update_subrange); + ("append", value_append); + ("not", value_not); + ("not_vec", value_not_vec); + ("and_vec", value_and_vec); + ("or_vec", value_or_vec); + ("uint", value_uint); + ("sint", value_sint); + ("get_slice_int", value_get_slice_int); + ("add", value_add); + ("sub", value_sub); + ("undefined_bit", fun _ -> V_bit Sail_lib.B0); + ("undefined_vector", value_undefined_vector); + ("replicate_bits", value_replicate_bits); + ("Elf_loader.elf_entry", fun _ -> V_int (Big_int.of_int 0)); ] |