Implement disassembler and instruction fetch cycle

.github/workflows/test.yml

@@ -43,12 +43,10 @@ jobs:
         run: make check
       - name: 'Run pyupgrade'
         run: make pyupgrade
-      - name: 'Run unit tests'
-        run: make test-unit
 
-  integration-tests:
+  build-and-test:
     needs: code-quality-checks
-    name: 'Integration Tests'
+    name: 'Build and Test'
     runs-on: [self-hosted, linux, normal]
     env:
       CONTAINER: riscv-integration-${{ github.sha }}
@@ -66,6 +64,8 @@ jobs:
         run: docker exec --user user ${CONTAINER} poetry install
       - name: 'Build semantics'
         run: docker exec --user user ${CONTAINER} make kdist-build
+      - name: 'Run unit tests'
+        run: docker exec --user user ${CONTAINER} make test-unit
       - name: 'Run integration tests'
         run: docker exec --user user ${CONTAINER} make test-integration
       - name: 'Tear down Docker'

Makefile

@@ -23,7 +23,7 @@ poetry-install:
 # Semantics
 
 kdist-build: poetry-install
-	$(POETRY) run kdist -v build riscv-semantics.llvm
+	$(POETRY) run kdist -v build riscv-semantics.llvm riscv-semantics.kllvm riscv-semantics.kllvm-runtime
 
 kdist-clean: poetry-install
 	$(POETRY) run kdist clean

package/version

@@ -1 +1 @@
-0.1.16
+0.1.17

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.16"
+version = "0.1.17"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/kriscv/__main__.py

@@ -19,6 +19,7 @@ class KRISCVOpts: ...
 @dataclass
 class RunOpts(KRISCVOpts):
     input_file: Path
+    end_symbol: str | None
 
 
 def kriscv(args: Sequence[str]) -> None:
@@ -35,14 +36,14 @@ def _parse_args(args: Sequence[str]) -> KRISCVOpts:
 
     match ns.command:
         case 'run':
-            return RunOpts(input_file=Path(ns.input_file).resolve(strict=True))
+            return RunOpts(input_file=Path(ns.input_file).resolve(strict=True), end_symbol=ns.end_symbol)
         case _:
             raise AssertionError()
 
 
 def _kriscv_run(opts: RunOpts) -> None:
     tools = semantics()
-    final_conf = tools.run_elf(opts.input_file)
+    final_conf = tools.run_elf(opts.input_file, end_symbol=opts.end_symbol)
     print(tools.kprint.pretty_print(final_conf))
 
 
@@ -53,7 +54,7 @@ def _arg_parser() -> ArgumentParser:
 
     run_parser = command_parser.add_parser('run', help='execute RISC-V ELF files programs')
     run_parser.add_argument('input_file', metavar='FILE', help='RISC-V ELF file to run')
-
+    run_parser.add_argument('--end-symbol', type=str, help='Symbol marking the address which terminates execution')
     return parser
 
 

src/kriscv/build.py

@@ -1,7 +1,19 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
 from pyk.kdist import kdist
+from pyk.kllvm import importer
 
 from .tools import Tools
 
+if TYPE_CHECKING:
+    from typing import Final
+
+importer.import_kllvm(kdist.get('riscv-semantics.kllvm'))
+
+runtime: Final = importer.import_runtime(kdist.get('riscv-semantics.kllvm-runtime'))
+
 
 def semantics() -> Tools:
-    return Tools(definition_dir=kdist.get('riscv-semantics.llvm'))
+    return Tools(definition_dir=kdist.get('riscv-semantics.llvm'), runtime=runtime)

src/kriscv/elf_parser.py

@@ -11,7 +11,7 @@
     from pyk.kast.inner import KInner
 
 
-def _memory_rangemap(elf: ELFFile) -> KInner:
+def memory_rangemap(elf: ELFFile) -> KInner:
     segments: dict[tuple[KInner, KInner], KInner] = {}
     for seg in elf.iter_segments():
         if seg['p_type'] == 'PT_LOAD':
@@ -22,11 +22,15 @@ def _memory_rangemap(elf: ELFFile) -> KInner:
     return rangemap_of(segments)
 
 
-def _entry_point(elf: ELFFile) -> KInner:
+def entry_point(elf: ELFFile) -> KInner:
     return intToken(elf.header['e_entry'])
 
 
-def config_vars(elf: ELFFile) -> dict[str, KInner]:
-    memory = _memory_rangemap(elf)
-    pc = _entry_point(elf)
-    return {'$MEM': memory, '$PC': pc}
+def read_symbol(elf: ELFFile, symbol: str) -> list[int]:
+    symtab = elf.get_section_by_name('.symtab')
+    if symtab is None:
+        return []
+    syms = symtab.get_symbol_by_name(symbol)
+    if syms is None:
+        return []
+    return [sym['st_value'] for sym in syms]

src/kriscv/kdist/plugin.py

@@ -1,11 +1,13 @@
 from __future__ import annotations
 
 import shutil
+import sys
 from pathlib import Path
 from typing import TYPE_CHECKING
 
 from pyk.kbuild.utils import k_version
 from pyk.kdist.api import Target
+from pyk.kllvm.compiler import compile_kllvm, compile_runtime
 from pyk.ktool.kompile import kompile
 
 if TYPE_CHECKING:
@@ -40,6 +42,37 @@ def deps(self) -> tuple[str]:
         return ('riscv-semantics.source',)
 
 
+class KLLVMTarget(Target):
+    def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None:
+        compile_kllvm(output_dir, verbose=verbose)
+
+    def context(self) -> dict[str, str]:
+        return {
+            'k-version': k_version().text,
+            'python-path': sys.executable,
+            'python-version': sys.version,
+        }
+
+
+class KLLVMRuntimeTarget(Target):
+    def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None:
+        compile_runtime(
+            definition_dir=deps['riscv-semantics.llvm'],
+            target_dir=output_dir,
+            verbose=verbose,
+        )
+
+    def deps(self) -> tuple[str, ...]:
+        return ('riscv-semantics.llvm',)
+
+    def context(self) -> dict[str, str]:
+        return {
+            'k-version': k_version().text,
+            'python-path': sys.executable,
+            'python-version': sys.version,
+        }
+
+
 __TARGETS__: Final = {
     'source': SourceTarget(),
     'llvm': KompileTarget(
@@ -51,4 +84,6 @@ def deps(self) -> tuple[str]:
             'warnings_to_errors': True,
         },
     ),
+    'kllvm': KLLVMTarget(),
+    'kllvm-runtime': KLLVMRuntimeTarget(),
 }

src/kriscv/kdist/riscv-semantics/riscv-disassemble.md

@@ -0,0 +1,141 @@
+```k
+requires "riscv-instructions.md"
+
+module RISCV-DISASSEMBLE
+  imports RISCV-INSTRUCTIONS
+  imports INT
+  imports STRING
+
+  syntax OpCode ::=
+      RTypeOpCode
+    | ITypeOpCode
+    | STypeOpCode
+    | BTypeOpCode
+    | UTypeOpCode
+    | JTypeOpCode
+    | UnrecognizedOpCode
+
+  syntax RTypeOpCode ::=
+      "OP"
+  syntax ITypeOpCode ::=
+      "JALR"
+    | "LOAD"
+    | "OP-IMM"
+    | "MISC-MEM"
+    | "SYSTEM"
+  syntax STypeOpCode ::=
+      "STORE"
+  syntax BTypeOpCode ::=
+      "BRANCH"
+  syntax UTypeOpCode ::=
+      "LUI"
+    | "AUIPC"
+  syntax JTypeOpCode ::=
+      "JAL"
+  syntax UnrecognizedOpCode ::=
+      "UNRECOGNIZED"
+
+  syntax OpCode ::= decodeOpCode(Int) [function]
+  rule decodeOpCode(55 ) => LUI
+  rule decodeOpCode(23 ) => AUIPC
+  rule decodeOpCode(111) => JAL
+  rule decodeOpCode(103) => JALR
+  rule decodeOpCode(99 ) => BRANCH
+  rule decodeOpCode(3  ) => LOAD
+  rule decodeOpCode(35 ) => STORE
+  rule decodeOpCode(19 ) => OP-IMM
+  rule decodeOpCode(51 ) => OP
+  rule decodeOpCode(15 ) => MISC-MEM
+  rule decodeOpCode(115) => SYSTEM
+  rule decodeOpCode(_  ) => UNRECOGNIZED [owise]
+
+  syntax EncodingType ::=
+      RType(opcode: RTypeOpCode, funct3: Int, funct7: Int, rd: Register, rs1: Register, rs2: Register)
+    | IType(opcode: ITypeOpCode, funct3: Int, rd: Register, rs1: Register, imm: Int)
+    | SType(opcode: STypeOpCode, funct3: Int, rs1: Register, rs2: Register, imm: Int)
+    | BType(opcode: BTypeOpCode, funct3: Int, rs1: Register, rs2: Register, imm: Int)
+    | UType(opcode: UTypeOpCode, rd: Register, imm: Int)
+    | JType(opcode: JTypeOpCode, rd: Register, imm: Int)
+    | UnrecognizedEncodingType(Int)
+
+  syntax EncodingType ::=
+      decode(Int) [function, total]
+    | decodeWithOp(OpCode, Int) [function]
+
+  rule decode(I) => decodeWithOp(decodeOpCode(I &Int 127), I >>Int 7)
+
+  rule decodeWithOp(OPCODE:RTypeOpCode, I) =>
+    RType(OPCODE, (I >>Int 5) &Int 7, (I >>Int 18) &Int 127, I &Int 31, (I >>Int 8) &Int 31, (I >>Int 13) &Int 31)
+  rule decodeWithOp(OPCODE:ITypeOpCode, I) =>
+    IType(OPCODE, (I >>Int 5) &Int 7, I &Int 31, (I >>Int 8) &Int 31, (I >>Int 13) &Int 4095)
+  rule decodeWithOp(OPCODE:STypeOpCode, I) =>
+    SType(OPCODE, (I >>Int 5) &Int 7, (I >>Int 8) &Int 31, (I >>Int 13) &Int 31, (((I >>Int 18) &Int 127) <<Int 5) |Int (I &Int 31))
+  rule decodeWithOp(OPCODE:BTypeOpCode, I) =>
+    BType(OPCODE, (I >>Int 5) &Int 7, (I >>Int 8) &Int 31, (I >>Int 13) &Int 31, (((I >>Int 24) &Int 1) <<Int 11) |Int ((I &Int 1) <<Int 10) |Int (((I >>Int 18) &Int 63) <<Int 4) |Int ((I >>Int 1) &Int 15))
+  rule decodeWithOp(OPCODE:UTypeOpCode, I) =>
+    UType(OPCODE, I &Int 31, (I >>Int 5) &Int 1048575)
+  rule decodeWithOp(OPCODE:JTypeOpCode, I) =>
+    JType(OPCODE, I &Int 31, (((I >>Int 24) &Int 1) <<Int 19) |Int (((I >>Int 5) &Int 255) <<Int 11) |Int (((I >>Int 13) &Int 1) <<Int 10) |Int ((I >>Int 14) &Int 1023))
+  rule decodeWithOp(_:UnrecognizedOpCode, I) =>
+    UnrecognizedEncodingType(I)
+
+  syntax Instruction ::= disassemble(Int) [symbol(disassemble), function, total, memo]
+                       | disassemble(EncodingType) [function, total]
+
+  rule disassemble(I:Int) => disassemble(decode(I))
+
+  rule disassemble(RType(OP, 0, 0,  RD, RS1, RS2)) => ADD  RD , RS1 , RS2
+  rule disassemble(RType(OP, 0, 32, RD, RS1, RS2)) => SUB  RD , RS1 , RS2
+  rule disassemble(RType(OP, 1, 0,  RD, RS1, RS2)) => SLL  RD , RS1 , RS2
+  rule disassemble(RType(OP, 2, 0,  RD, RS1, RS2)) => SLT  RD , RS1 , RS2
+  rule disassemble(RType(OP, 3, 0,  RD, RS1, RS2)) => SLTU RD , RS1 , RS2
+  rule disassemble(RType(OP, 4, 0,  RD, RS1, RS2)) => XOR  RD , RS1 , RS2
+  rule disassemble(RType(OP, 5, 0,  RD, RS1, RS2)) => SRL  RD , RS1 , RS2
+  rule disassemble(RType(OP, 5, 32, RD, RS1, RS2)) => SRA  RD , RS1 , RS2
+  rule disassemble(RType(OP, 6, 0,  RD, RS1, RS2)) => OR   RD , RS1 , RS2
+  rule disassemble(RType(OP, 7, 0,  RD, RS1, RS2)) => AND  RD , RS1 , RS2
+
+  rule disassemble(IType(OP-IMM, 0, RD, RS1, IMM)) => ADDI  RD , RS1 , chopAndExtend(IMM, 12)
+  rule disassemble(IType(OP-IMM, 1, RD, RS1, IMM)) => SLLI  RD , RS1 , IMM &Int 31 requires (IMM >>Int 5) &Int 127 ==Int 0
+  rule disassemble(IType(OP-IMM, 2, RD, RS1, IMM)) => SLTI  RD , RS1 , chopAndExtend(IMM, 12)
+  rule disassemble(IType(OP-IMM, 3, RD, RS1, IMM)) => SLTIU RD , RS1 , chopAndExtend(IMM, 12)
+  rule disassemble(IType(OP-IMM, 4, RD, RS1, IMM)) => XORI  RD , RS1 , chopAndExtend(IMM, 12)
+  rule disassemble(IType(OP-IMM, 5, RD, RS1, IMM)) => SRLI  RD , RS1 , IMM &Int 31 requires (IMM >>Int 5) &Int 127 ==Int 0
+  rule disassemble(IType(OP-IMM, 5, RD, RS1, IMM)) => SRAI  RD , RS1 , IMM &Int 31 requires (IMM >>Int 5) &Int 127 ==Int 32
+  rule disassemble(IType(OP-IMM, 6, RD, RS1, IMM)) => ORI   RD , RS1 , chopAndExtend(IMM, 12)
+  rule disassemble(IType(OP-IMM, 7, RD, RS1, IMM)) => ANDI  RD , RS1 , chopAndExtend(IMM, 12)
+
+
+  rule disassemble(IType(JALR, 0, RD, RS1, IMM)) => JALR RD , chopAndExtend(IMM, 12) ( RS1 )
+
+  rule disassemble(IType(LOAD, 0, RD, RS1, IMM)) => LB  RD , chopAndExtend(IMM, 12) ( RS1 )
+  rule disassemble(IType(LOAD, 1, RD, RS1, IMM)) => LH  RD , chopAndExtend(IMM, 12) ( RS1 )
+  rule disassemble(IType(LOAD, 2, RD, RS1, IMM)) => LW  RD , chopAndExtend(IMM, 12) ( RS1 )
+  rule disassemble(IType(LOAD, 4, RD, RS1, IMM)) => LBU RD , chopAndExtend(IMM, 12) ( RS1 )
+  rule disassemble(IType(LOAD, 5, RD, RS1, IMM)) => LHU RD , chopAndExtend(IMM, 12) ( RS1 )
+
+  rule disassemble(IType(MISC-MEM, 0, 0, 0, 2099)) => FENCE.TSO
+  rule disassemble(IType(MISC-MEM, 0, 0, 0, IMM)) => FENCE (IMM >>Int 4) &Int 15 , IMM &Int 15 requires (IMM >>Int 8) &Int 15 ==Int 0
+
+  rule disassemble(IType(SYSTEM, 0, 0, 0, 0)) => ECALL
+  rule disassemble(IType(SYSTEM, 0, 0, 0, 1)) => EBREAK
+
+  rule disassemble(SType(STORE, 0, RS1, RS2, IMM)) => SB RS2 , chopAndExtend(IMM, 12) ( RS1 )
+  rule disassemble(SType(STORE, 1, RS1, RS2, IMM)) => SH RS2 , chopAndExtend(IMM, 12) ( RS1 )
+  rule disassemble(SType(STORE, 2, RS1, RS2, IMM)) => SW RS2 , chopAndExtend(IMM, 12) ( RS1 )
+
+  rule disassemble(BType(BRANCH, 0, RS1, RS2, IMM)) => BEQ  RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
+  rule disassemble(BType(BRANCH, 1, RS1, RS2, IMM)) => BNE  RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
+  rule disassemble(BType(BRANCH, 4, RS1, RS2, IMM)) => BLT  RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
+  rule disassemble(BType(BRANCH, 5, RS1, RS2, IMM)) => BGE  RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
+  rule disassemble(BType(BRANCH, 6, RS1, RS2, IMM)) => BLTU RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
+  rule disassemble(BType(BRANCH, 7, RS1, RS2, IMM)) => BGEU RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
+
+  rule disassemble(UType(LUI, RD, IMM))   => LUI   RD , IMM
+  rule disassemble(UType(AUIPC, RD, IMM)) => AUIPC RD , IMM
+
+  rule disassemble(JType(JAL, RD, IMM)) => JAL RD , chopAndExtend(IMM, 20) *Int 2
+
+  rule disassemble(_:EncodingType) => INVALID_INSTR [owise]
+endmodule
+```