rvim.lean

import logic.basic

structure misa := (extensions : list (string × list nat))

namespace misa
  private def gc : list (string × list nat) :=
  [⟨"M", [2]⟩, ⟨"A", [2, 1]⟩, ⟨"F", [2, 2]⟩, ⟨"D", [2, 2]⟩, ⟨"C", [2]⟩,
   ⟨"Zicsr", [2]⟩, ⟨"Zifencei", [2]⟩]

  def rv32gc : misa := ⟨⟨"32I", [2, 1]⟩ :: gc⟩
  def rv64gc : misa := ⟨⟨"64I", [2, 1]⟩ :: gc⟩
  def rv64gqcv : misa := ⟨⟨"Q", [2, 2]⟩ :: ⟨"V", [0, 7]⟩ :: rv64gc.extensions⟩

  def xlen : misa → ℕ | ⟨e⟩ :=
  if "64I" ∈ e.map prod.fst then 64 else 32

  def flen : misa → ℕ | ⟨e⟩ :=
  if "D" ∈ e.map prod.fst then 64
  else if "F" ∈ e.map prod.fst then 32
  else 0

  def ilen := 32

  def ialign : misa → ℕ | ⟨e⟩ :=
  if "C" ∈ e.map prod.fst then 16 else 32
end misa

-- @[pattern] def n := v
meta def mk_pat (n : name) (v : expr) :=
  tactic.infer_type v >>= λ t,
  tactic.add_decl (declaration.defn n [] t v reducibility_hints.abbrev tt)
  >> tactic.set_basic_attribute `pattern n

run_cmd [
  [`load,   `load_fp,  `custom_0, `misc_mem, `op_imm,   `auipc,      `op_imm_32],
  [`store,  `store_fp, `custom_1, `amo,      `op,       `lui,        `op_32    ],
  [`madd,   `msub,     `nmsub,    `nmadd,    `op_fp,    `reserved_0, `custom_2 ],
  [`branch, `jalr,     `reserved, `jal,      `system,   `reserved_1, `custom_3 ]
 ].enum.mmap' $ λ ⟨row, ns⟩, ns.enum.mmap' $ λ ⟨col, n⟩,
  let opc := 3 + col.shiftl 2 + row.shiftl 5 in
  mk_pat (`opcode ++ n) `(fin.of_nat opc : fin 128)

run_cmd [
  (0xC00, [`cycle, `time, `instret]),
  (0xC80, [`cycleh, `timeh, `instreth]),
  (0x001, [`fflags, `frm, `fcsr])
 ].mmap' $ λ ⟨base, ns⟩, ns.enum.mmap' $ λ ⟨offset, n⟩,
  mk_pat (`csr ++ n) (reflect $ base + offset)

structure regnum :=
(num : ℕ)

instance : has_zero regnum := ⟨⟨0⟩⟩

@[derive decidable_eq]
inductive reg_type | integer | float
open reg_type

structure reg (rtype : reg_type) :=
(register : regnum)

instance (rtype) : has_coe (reg rtype) regnum := ⟨reg.register⟩

inductive fmt : Type
| R  (opcode7 : fin 128) (funct3 : fin 8) (rd rs1 rs2     : regnum) (funct7 : fin 128)
| R4 (opcode7 : fin 128) (funct3 : fin 8) (rd rs1 rs2 rs3 : regnum) (funct2 : fin 4)
-- 12-bit signed immediate
| I  (opcode7 : fin 128) (funct3 : fin 8) (rd rs1     : regnum) (imm : ℤ)
-- 12-bit signed immediate
| S  (opcode7 : fin 128) (funct3 : fin 8) (   rs1 rs2 : regnum) (imm : ℤ)
-- high 12 of 13-bit signed immediate
| B  (opcode7 : fin 128) (funct3 : fin 8) (   rs1 rs2 : regnum) (imm : ℤ)
-- high 20 of 32-bit signed immediate
| U  (opcode7 : fin 128)                  (rd         : regnum) (imm : ℤ)
-- high 20 of 33-bit signed immediate
| J  (opcode7 : fin 128)                  (rd         : regnum) (imm : ℤ)

namespace fmt
  private def regs (rd rs1 rs2 rs3 : regnum := 0) :=
  (rd.num.land 31).shiftl 7 + (rs1.num.land 31).shiftl 15
  + (rs2.num.land 31).shiftl 20 + (rs3.num.land 31).shiftl 27

  private def bits (a : ℤ) (b c) :=
  (a.to_nat.shiftr c).land (2^(b - c) - 1)

  -- encoding truncates out-of-range registers and immediates
  -- fixme: immediates should be encoded in 2's complement
  def encode : fmt → ℕ
  | (R opcode7 funct3 rd rs1 rs2 funct7) :=
     opcode7.val + regs rd rs1 rs2 + funct3.val.shiftl 12 + funct7.val.shiftl 25
  | (R4 opcode7 funct3 rd rs1 rs2 rs3 funct2) :=
     opcode7.val + regs rd rs1 rs2 rs3 + funct3.val.shiftl 12
     + funct2.val.shiftl 25
  | (I opcode7 funct3 rd rs1 imm) :=
     opcode7.val + regs rd rs1 + funct3.val.shiftl 12 + imm.sign.to_nat.shiftl 31
     + (bits imm.to_nat 10 0).shiftl 20
  | (S opcode7 funct3 rs1 rs2 imm) :=
     opcode7.val + regs 0 rs1 rs2 + funct3.val.shiftl 12
     + imm.sign.to_nat.shiftl 31 + (bits imm.to_nat 10 5).shiftl 25
     + (bits imm.to_nat 4 0).shiftl 7
  | (B opcode7 funct3 rs1 rs2 imm) :=
     opcode7.val + regs 0 rs1 rs2 + funct3.val.shiftl 12
     + imm.sign.to_nat.shiftl 31 + (bits imm.to_nat 10 5).shiftl 25
     + (bits imm 4 1).shiftl 8 + (bits imm 11 11).shiftl 7
  | (U opcode7 rd imm) :=
     opcode7.val + regs rd + imm.sign.to_nat.shiftl 31
     + (bits imm.to_nat 20 12).shiftl 12
  | (J opcode7 rd imm) :=
     opcode7.val + regs rd + imm.sign.to_nat.shiftl 31 + (bits imm 10 1).shiftl 21
     + (bits imm 11 11).shiftl 20 + (bits imm 19 12).shiftl 12

  structure decoded :=
  (opcode rd funct3 rs1 rs2 funct7 : ℕ)
  (I_imm S_imm B_imm U_imm J_imm : ℤ)

  private def decode_sign (n) : ℤ := if bits n 31 31 = 1 then -1 else 1

  -- fixme: immediates are encoded in 2's complement
  def decode (n : ℕ) : decoded :=
  {
    opcode := bits n 6 0,
    rd := bits n 11 7,
    funct3 := bits n 14 12,
    rs1 := bits n 19 15,
    rs2 := bits n 24 20,
    funct7 := bits n 31 20,
    I_imm := decode_sign n * bits n 30 20,
    S_imm := decode_sign n * ((bits n 30 25).shiftl 5 + bits n 11 7),
    B_imm := decode_sign n * ((bits n 30 25).shiftl 5 + (bits n 11 8).shiftl 1
                              + (bits n 11 11).shiftl 11),
    U_imm := decode_sign n * (bits n 30 12).shiftl 12,
    J_imm := decode_sign n * ((bits n 10 1).shiftl 21 + (bits n 11 11).shiftl 20
                              + (bits n 19 12).shiftl 12),
  }
end fmt

def reg_imm (rtype) := reg rtype ⊕ ℤ

instance has_coe_reg (rtype) : has_coe (reg rtype) (reg_imm rtype) := ⟨λ r, sum.inl r⟩
instance has_coe_int (rtype) : has_coe ℤ (reg_imm rtype) := ⟨λ r, sum.inr r⟩

inductive compare | eq | ne | lt | le
inductive csr_mode | swap | set | clear
inductive rounding_mode | even | zero | down | up | max_magnitude | dyn
@[derive decidable_eq]
inductive sign_inj_mode | copy | not | xor

@[derive decidable_eq]
inductive arith
| xor | or | and | shiftl | shiftr
| add | sub | mul | mulh | div | rem

@[derive decidable_eq]
inductive arith_f
| add | sub | mul | div | rem
| sqrt | min | max
| sign_inj (mode : sign_inj_mode)
| fmadd | fmsub | fnmadd | fnmsub

inductive atomic_op | swap | add | and | or | xor | max | min

namespace arith
  abbreviation has_imm (op : arith) : Prop :=
  op ∈ [xor, or, and, shiftl, shiftr, add, sub]
end arith

namespace arith_f
  abbreviation has_rs3 (op : arith_f) : Prop :=
  op ∈ [fnmadd, fnmsub]
end arith_f

inductive inst
-- arithmetic operations
| arith (op : arith) (rd rs1 : reg integer)
  (rs2_imm : if op.has_imm then reg_imm integer else reg integer)
| arith_f (op : arith_f) (rd rs1 rs2 : reg float)
  (rs3 : if op.has_rs3 then reg float else opt_param unit ())
-- load upper immediate
| lui (rd : reg integer) (offset : ℤ) (apc : opt_param bool ff)
-- comparisons, classifications, and conversions
| compare {rtype} (c : compare) (rd : reg integer) (rs1 : reg rtype)
  (rs2 : if rtype = integer then reg_imm integer else reg float)
| classify (rd : reg integer) (rs1 : reg float)
| convert {rtype} (rd : reg rtype)
  (rs1 : reg (if rtype = integer then float else integer))
  (mv : opt_param bool ff)
-- control flow
| jump (rd : reg integer) (base : option (reg integer)) (offset : ℤ)
| branch (c : compare) (rs1 rs2 : reg integer) (offset : ℤ)
-- memory
| load {rtype} (dest : reg rtype) (base : reg integer) (offset : ℤ)
| store {rtype} (src : reg rtype) (base : reg integer) (offset : ℤ)
| fence (mode pred succ : fin 16)
| fencei
| load_reserved (rd addr : reg integer) (acquire release : bool)
| store_conditional (rd addr src : reg integer) (acquire release : bool)
| atomic (op : atomic_op) (rd rs1 rs2 : reg integer) (acquire release : bool)
-- system
| ecall
| ebreak
-- "Zicsr"
| csr (mode : csr_mode) (rd : reg integer) (rs2_imm : reg_imm integer) (addr : ℤ)

namespace inst
  open fmt arith arith_f sign_inj_mode

  private def fmt_reg_imm {rtype} (funct3 : fin 8) (funct7 : fin 128) (rd rs1 : regnum)
    : reg_imm rtype → fmt
  | (sum.inl rs2) := R opcode.op funct3 rd rs1 rs2 funct7
  | (sum.inr imm) := I opcode.op_imm funct3 rd rs1 imm

  def to_fmt : inst → fmt
  -- arithmetic operations
  | (arith add rd rs1 rs2_imm) := fmt_reg_imm 0b000 0 rd rs1 rs2_imm
  | (arith sub rd rs1 (sum.inl rs2)) := R opcode.op 0b000 rd rs1 rs2 0100000
  | (arith sub rd rs1 (sum.inr imm)) := I opcode.op_imm 0b000 rd rs1 (-imm)
  | (arith xor rd rs1 rs2_imm) := fmt_reg_imm 0b100 0 rd rs1 rs2_imm
  | (arith or  rd rs1 rs2_imm) := fmt_reg_imm 0b110 0 rd rs1 rs2_imm
  | (arith and rd rs1 rs2_imm) := fmt_reg_imm 0b111 0 rd rs1 rs2_imm
  | (arith shiftl rd rs1 rs2_imm) := fmt_reg_imm 0b001 0 rd rs1 rs2_imm
  -- fixme signed rs1 -> funct7 = 0100000
  | (arith shiftr rd rs1 rs2_imm) := fmt_reg_imm 0b101 0 rd rs1 rs2_imm
  | (arith mul rd rs1 (rs2 : reg integer)) := R opcode.op 0b000 rd rs1 rs2 0b0000001
  -- fixme signed/unsigned pairs of rs1/rs2
  | (arith mulh rd rs1 (rs2 : reg integer)) := R opcode.op 0b001 rd rs1 rs2 0b0000001
  -- fixme signed rs1 -> funct3 = 101
  | (arith div rd rs1 (rs2 : reg integer)) := R opcode.op 0b100 rd rs1 rs2 0b0000001
  -- fixme signed rs1 -> funct3 = 111
  | (arith rem rd rs1 (rs2 : reg integer)) := R opcode.op 0b110 rd rs1 rs2 0b0000001
  | (arith_f add rd rs1 rs2 ()) := R opcode.op_fp 0b000 rd rs1 rs2 0b0000001
  | (arith_f sub rd rs1 rs2 ()) := R opcode.op_fp 0b000 rd rs1 rs2 0b0000001
  | (arith_f mul rd rs1 rs2 ()) := R opcode.op_fp 0b000 rd rs1 rs2 0b0000001
  | (arith_f div rd rs1 rs2 ()) := R opcode.op_fp 0b000 rd rs1 rs2 0b0000001
  | (arith_f rem rd rs1 rs2 ()) := R opcode.op_fp 0b000 rd rs1 rs2 0b0000001
  | (arith_f min rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
  | (arith_f max rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
  | (arith_f sqrt rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
  | (arith_f (sign_inj copy) rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
  | (arith_f (sign_inj not) rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
  | (arith_f (sign_inj xor) rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
  | (arith_f fmadd rd rs1 rs2 rs3) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
  | (arith_f fmsub rd rs1 rs2 rs3) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
  | (arith_f fnmadd rd rs1 rs2 rs3) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
  | (arith_f fnmsub rd rs1 rs2 rs3) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
  -- load upper immediate
  | (lui rd offset apc) := R 0 0 0 0 0 0
  -- comparisons, classifications, and conversions
  | (compare c rd rs1 rs2) := R 0 0 0 0 0 0
  | (classify rd rs1) := R 0 0 0 0 0 0
  | (convert rd rs1 mv) := R 0 0 0 0 0 0
  -- control flow
  | (jump rd base offset) := R 0 0 0 0 0 0
  | (branch c rs1 rs2 offset) := R 0 0 0 0 0 0
  -- memory
  | (load dest base offset) := R 0 0 0 0 0 0
  | (store src base offset) := R 0 0 0 0 0 0
  | (fence mode pred succ) := R 0 0 0 0 0 0
  | fencei := R 0 0 0 0 0 0
  | (load_reserved rd addr acquire release) := R 0 0 0 0 0 0
  | (store_conditional rd addr src acquire release) := R 0 0 0 0 0 0
  | (atomic op rd rs1 rs2 acquire release) := R 0 0 0 0 0 0
  -- system
  | ecall := R 0 0 0 0 0 0
  | ebreak := R 0 0 0 0 0 0
  -- "Zicsr"
  | (csr mode rd rs2_imm addr) := R 0 0 0 0 0 0

  def encode : inst → ℕ := fmt.encode ∘ to_fmt
end inst