diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index c084b35a..49645ba0 100644 --- a/.github/workflows/test.yml +++ b/.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' diff --git a/Makefile b/Makefile index acf40a17..0f2adbdc 100644 --- a/Makefile +++ b/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 diff --git a/package/version b/package/version index e8e277f2..04c5555c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.16 +0.1.17 diff --git a/pyproject.toml b/pyproject.toml index 9b3f02b7..1dcf24d3 100644 --- a/pyproject.toml +++ b/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. ", diff --git a/src/kriscv/__main__.py b/src/kriscv/__main__.py index ea29c58d..870a5aa2 100644 --- a/src/kriscv/__main__.py +++ b/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 diff --git a/src/kriscv/build.py b/src/kriscv/build.py index 18921d61..6c2d5a5e 100644 --- a/src/kriscv/build.py +++ b/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) diff --git a/src/kriscv/elf_parser.py b/src/kriscv/elf_parser.py index be088d8c..92a9ff21 100644 --- a/src/kriscv/elf_parser.py +++ b/src/kriscv/elf_parser.py @@ -2,8 +2,7 @@ from typing import TYPE_CHECKING -from pyk.prelude.bytes import bytesToken -from pyk.prelude.collections import rangemap_of +from pyk.prelude.collections import map_of from pyk.prelude.kint import intToken if TYPE_CHECKING: @@ -11,22 +10,35 @@ from pyk.kast.inner import KInner -def _memory_rangemap(elf: ELFFile) -> KInner: - segments: dict[tuple[KInner, KInner], KInner] = {} +def _memory_segments(elf: ELFFile) -> dict[tuple[int, int], bytes]: + segments: dict[tuple[int, int], bytes] = {} for seg in elf.iter_segments(): if seg['p_type'] == 'PT_LOAD': start = seg['p_vaddr'] file_size = seg['p_filesz'] data = seg.data() + b'\0' * (seg['p_memsz'] - file_size) - segments[(intToken(start), intToken(start + file_size))] = bytesToken(data) - return rangemap_of(segments) + segments[(start, start + file_size)] = data + return segments -def _entry_point(elf: ELFFile) -> KInner: +def memory_map(elf: ELFFile) -> KInner: + mem_map: dict[KInner, KInner] = {} + for addr_range, data in _memory_segments(elf).items(): + start, end = addr_range + for addr in range(start, end): + mem_map[intToken(addr)] = intToken(data[addr - start]) + return map_of(mem_map) + + +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] diff --git a/src/kriscv/hello.py b/src/kriscv/hello.py deleted file mode 100644 index 6cab2ee4..00000000 --- a/src/kriscv/hello.py +++ /dev/null @@ -1,2 +0,0 @@ -def hello(name: str) -> str: - return f'Hello, {name}!' diff --git a/src/kriscv/kdist/plugin.py b/src/kriscv/kdist/plugin.py index 38cab39c..2d2f7c2b 100644 --- a/src/kriscv/kdist/plugin.py +++ b/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(), } diff --git a/src/kriscv/kdist/riscv-semantics/riscv-disassemble.md b/src/kriscv/kdist/riscv-semantics/riscv-disassemble.md new file mode 100644 index 00000000..c21ecd99 --- /dev/null +++ b/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, total] + 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) < + BType(OPCODE, (I >>Int 5) &Int 7, (I >>Int 8) &Int 31, (I >>Int 13) &Int 31, (((I >>Int 24) &Int 1) <>Int 18) &Int 63) <>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 5) &Int 255) <>Int 13) &Int 1) <>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 +``` diff --git a/src/kriscv/kdist/riscv-semantics/riscv-instructions.md b/src/kriscv/kdist/riscv-semantics/riscv-instructions.md new file mode 100644 index 00000000..97da29d0 --- /dev/null +++ b/src/kriscv/kdist/riscv-semantics/riscv-instructions.md @@ -0,0 +1,80 @@ +```k +module RISCV-INSTRUCTIONS + imports INT + + syntax Register ::= Int + + syntax Instruction ::= + RegRegImmInstr + | RegImmInstr + | RegRegRegInstr + | RegImmRegInstr + | FenceInstr + | NullaryInstr + | InvalidInstr + + syntax RegRegImmInstr ::= RegRegImmInstrName Register "," Register "," Int [symbol(RegRegImmInstr)] + syntax RegRegImmInstrName ::= + "ADDI" [symbol(ADDI)] + | "SLTI" [symbol(SLTI)] + | "SLTIU" [symbol(SLTIU)] + | "ANDI" [symbol(ANDI)] + | "ORI" [symbol(ORI)] + | "XORI" [symbol(XORI)] + | "SLLI" [symbol(SLLI)] + | "SRLI" [symbol(SRLI)] + | "SRAI" [symbol(SRAI)] + | "BEQ" [symbol(BEQ)] + | "BNE" [symbol(BNE)] + | "BLT" [symbol(BLT)] + | "BLTU" [symbol(BLTU)] + | "BGE" [symbol(BGE)] + | "BGEU" [symbol(BGEU)] + + syntax RegImmInstr ::= RegImmInstrName Register "," Int [symbol(RegImmInstr)] + syntax RegImmInstrName ::= + "LUI" [symbol(LUI)] + | "AUIPC" [symbol(AUIPC)] + | "JAL" [symbol(JAL)] + + syntax RegRegRegInstr ::= RegRegRegInstrName Register "," Register "," Register [symbol(RegRegRegInstr)] + syntax RegRegRegInstrName ::= + "ADD" [symbol(ADD)] + | "SUB" [symbol(SUB)] + | "SLT" [symbol(SLT)] + | "SLTU" [symbol(SLTU)] + | "AND" [symbol(AND)] + | "OR" [symbol(OR)] + | "XOR" [symbol(XOR)] + | "SLL" [symbol(SLL)] + | "SRL" [symbol(SRL)] + | "SRA" [symbol(SRA)] + + syntax RegImmRegInstr ::= RegImmRegInstrName Register "," Int "(" Register ")" [symbol(RegImmRegInstr)] + syntax RegImmRegInstrName ::= + "JALR" [symbol(JALR)] + | "LW" [symbol(LW)] + | "LH" [symbol(LH)] + | "LHU" [symbol(LHU)] + | "LB" [symbol(LB)] + | "LBU" [symbol(LBU)] + | "SW" [symbol(SW)] + | "SH" [symbol(SH)] + | "SB" [symbol(SB)] + + syntax FenceInstr ::= "FENCE" Int "," Int [symbol(FENCE)] + + syntax NullaryInstr ::= NullaryInstrName + syntax NullaryInstrName ::= + "FENCE.TSO" [symbol(FENCETSO)] + | "ECALL" [symbol(ECALL)] + | "EBREAK" [symbol(EBREAK)] + + syntax InvalidInstr ::= "INVALID_INSTR" [symbol(INVALID_INSTR)] + + // Truncate to length bits, then sign extend + syntax Int ::= chopAndExtend(bits: Int, length: Int) [function, total] + rule chopAndExtend(B, L) => (-1 <>Int (L -Int 1)) &Int 1 ==Int 1 + rule chopAndExtend(B, L) => B &Int (2 ^Int L -Int 1) [owise] +endmodule +``` diff --git a/src/kriscv/kdist/riscv-semantics/riscv.md b/src/kriscv/kdist/riscv-semantics/riscv.md index b9e81bf0..cf169780 100644 --- a/src/kriscv/kdist/riscv-semantics/riscv.md +++ b/src/kriscv/kdist/riscv-semantics/riscv.md @@ -1,11 +1,101 @@ ```k +requires "riscv-disassemble.md" +requires "riscv-instructions.md" + +module RISCV-CONFIGURATION + imports INT + imports MAP + imports RANGEMAP + + syntax HaltCondition + + syntax Int ::= XLEN() [macro] + rule XLEN() => 32 + + configuration + + .K + $MEM:Map // Map{Int, Int} + .Map // Map{Int, Int} + $PC:Int + + + $HALT:HaltCondition + +endmodule + +module RISCV-TERMINATION + imports RISCV-CONFIGURATION + imports BOOL + imports INT + + syntax Bool ::= shouldHalt(HaltCondition) [function] + syntax HaltCondition ::= + "NEVER" [symbol(HaltNever)] + | "ADDRESS" "(" Int ")" [symbol(HaltAtAddress)] + + + rule shouldHalt(NEVER) => false + + rule [[ shouldHalt(ADDRESS(END)) => true ]] + PC + requires END ==Int PC + + rule [[ shouldHalt(ADDRESS(END)) => false ]] + PC + requires END =/=Int PC +endmodule + +module RISCV-MEMORY + imports INT + imports MAP + imports RANGEMAP + imports RISCV-CONFIGURATION + imports RISCV-DISASSEMBLE + imports RISCV-INSTRUCTIONS + + syntax Int ::= wrapAddr(address: Int) [function] + rule wrapAddr(A) => A modInt (2 ^Int XLEN()) + + syntax Int ::= loadByte(memory: Map, address: Int) [function] + rule loadByte(MEM, ADDR) => { MEM [ wrapAddr(ADDR) ] } :>Int + + syntax Instruction ::= fetchInstr(memory: Map, address: Int) [function] + rule fetchInstr(MEM, ADDR) => + disassemble((loadByte(MEM, ADDR +Int 3) < REGS + rule writeReg(REGS, RD, VAL) => REGS[RD <- VAL] requires RD =/=Int 0 + + syntax Int ::= readReg(regs: Map, rs: Int) [function] + rule readReg(_ , 0 ) => 0 + rule readReg(REGS, RS) => { REGS[RS] } :>Int requires RS =/=Int 0 +endmodule + module RISCV -imports BYTES -imports INT -imports RANGEMAP + imports RISCV-CONFIGURATION + imports RISCV-DISASSEMBLE + imports RISCV-INSTRUCTIONS + imports RISCV-MEMORY + imports RISCV-TERMINATION + + rule .K => fetchInstr(MEM, PC) + MEM + PC + H + requires notBool shouldHalt(H) + + rule ADDI RD , RS , IMM => .K ... + REGS => writeReg(REGS, RD, chopAndExtend(readReg(REGS, RS) +Int IMM, XLEN())) + PC => wrapAddr(PC +Int 4) -configuration - $MEM:RangeMap - $PC:Int + rule LUI RD , IMM => .K ... + REGS => writeReg(REGS, RD, chopAndExtend(IMM < + PC => wrapAddr(PC +Int 4) endmodule ``` diff --git a/src/kriscv/term_builder.py b/src/kriscv/term_builder.py new file mode 100644 index 00000000..81fd1a92 --- /dev/null +++ b/src/kriscv/term_builder.py @@ -0,0 +1,230 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +from pyk.kast.inner import KApply, KSort +from pyk.prelude.kint import intToken + +if TYPE_CHECKING: + from collections.abc import Iterable + from typing import TypeVar + + from pyk.kast.inner import KInner + + T = TypeVar('T') + + +def halt_never() -> KInner: + return KApply('HaltNever') + + +def halt_at_address(address: KInner) -> KInner: + return KApply('HaltAtAddress', address) + + +def disassemble(instr: KInner) -> KInner: + return KApply('disassemble', instr) + + +def sort_instruction() -> KSort: + return KSort('Instruction') + + +def _reg_reg_imm_instr(reg_reg_imm_instr_name: KInner, reg1: KInner, reg2: KInner, imm: KInner) -> KInner: + return KApply('RegRegImmInstr', reg_reg_imm_instr_name, reg1, reg2, imm) + + +def _reg_imm_instr(reg_imm_instr_name: KInner, reg: KInner, imm: KInner) -> KInner: + return KApply('RegImmInstr', reg_imm_instr_name, reg, imm) + + +def _reg_reg_reg_instr(reg_reg_reg_instr_name: KInner, reg1: KInner, reg2: KInner, reg3: KInner) -> KInner: + return KApply('RegRegRegInstr', reg_reg_reg_instr_name, reg1, reg2, reg3) + + +def _reg_imm_reg_instr(reg_imm_reg_instr_name: KInner, reg1: KInner, imm: KInner, reg2: KInner) -> KInner: + return KApply('RegImmRegInstr', reg_imm_reg_instr_name, reg1, imm, reg2) + + +def register(num: int) -> KInner: + return intToken(num) + + +def addi_instr(rd: KInner, rs1: KInner, imm: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('ADDI'), rd, rs1, imm) + + +def slti_instr(rd: KInner, rs1: KInner, imm: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('SLTI'), rd, rs1, imm) + + +def sltiu_instr(rd: KInner, rs1: KInner, imm: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('SLTIU'), rd, rs1, imm) + + +def andi_instr(rd: KInner, rs1: KInner, imm: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('ANDI'), rd, rs1, imm) + + +def ori_instr(rd: KInner, rs1: KInner, imm: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('ORI'), rd, rs1, imm) + + +def xori_instr(rd: KInner, rs1: KInner, imm: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('XORI'), rd, rs1, imm) + + +def slli_instr(rd: KInner, rs1: KInner, shamt: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('SLLI'), rd, rs1, shamt) + + +def srli_instr(rd: KInner, rs1: KInner, shamt: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('SRLI'), rd, rs1, shamt) + + +def srai_instr(rd: KInner, rs1: KInner, shamt: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('SRAI'), rd, rs1, shamt) + + +def beq_instr(rs1: KInner, rs2: KInner, offset: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('BEQ'), rs1, rs2, offset) + + +def bne_instr(rs1: KInner, rs2: KInner, offset: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('BNE'), rs1, rs2, offset) + + +def blt_instr(rs1: KInner, rs2: KInner, offset: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('BLT'), rs1, rs2, offset) + + +def bltu_instr(rs1: KInner, rs2: KInner, offset: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('BLTU'), rs1, rs2, offset) + + +def bge_instr(rs1: KInner, rs2: KInner, offset: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('BGE'), rs1, rs2, offset) + + +def bgeu_instr(rs1: KInner, rs2: KInner, offset: KInner) -> KInner: + return _reg_reg_imm_instr(KApply('BGEU'), rs1, rs2, offset) + + +def lui_instr(rd: KInner, imm: KInner) -> KInner: + return _reg_imm_instr(KApply('LUI'), rd, imm) + + +def auipc_instr(rd: KInner, imm: KInner) -> KInner: + return _reg_imm_instr(KApply('AUIPC'), rd, imm) + + +def jal_instr(rd: KInner, offset: KInner) -> KInner: + return _reg_imm_instr(KApply('JAL'), rd, offset) + + +def add_instr(rd: KInner, rs1: KInner, rs2: KInner) -> KInner: + return _reg_reg_reg_instr(KApply('ADD'), rd, rs1, rs2) + + +def sub_instr(rd: KInner, rs1: KInner, rs2: KInner) -> KInner: + return _reg_reg_reg_instr(KApply('SUB'), rd, rs1, rs2) + + +def slt_instr(rd: KInner, rs1: KInner, rs2: KInner) -> KInner: + return _reg_reg_reg_instr(KApply('SLT'), rd, rs1, rs2) + + +def sltu_instr(rd: KInner, rs1: KInner, rs2: KInner) -> KInner: + return _reg_reg_reg_instr(KApply('SLTU'), rd, rs1, rs2) + + +def and_instr(rd: KInner, rs1: KInner, rs2: KInner) -> KInner: + return _reg_reg_reg_instr(KApply('AND'), rd, rs1, rs2) + + +def or_instr(rd: KInner, rs1: KInner, rs2: KInner) -> KInner: + return _reg_reg_reg_instr(KApply('OR'), rd, rs1, rs2) + + +def xor_instr(rd: KInner, rs1: KInner, rs2: KInner) -> KInner: + return _reg_reg_reg_instr(KApply('XOR'), rd, rs1, rs2) + + +def sll_instr(rd: KInner, rs1: KInner, rs2: KInner) -> KInner: + return _reg_reg_reg_instr(KApply('SLL'), rd, rs1, rs2) + + +def srl_instr(rd: KInner, rs1: KInner, rs2: KInner) -> KInner: + return _reg_reg_reg_instr(KApply('SRL'), rd, rs1, rs2) + + +def sra_instr(rd: KInner, rs1: KInner, rs2: KInner) -> KInner: + return _reg_reg_reg_instr(KApply('SRA'), rd, rs1, rs2) + + +def jalr_instr(rd: KInner, offset: KInner, rs1: KInner) -> KInner: + return _reg_imm_reg_instr(KApply('JALR'), rd, offset, rs1) + + +def lw_instr(rd: KInner, offset: KInner, rs1: KInner) -> KInner: + return _reg_imm_reg_instr(KApply('LW'), rd, offset, rs1) + + +def lh_instr(rd: KInner, offset: KInner, rs1: KInner) -> KInner: + return _reg_imm_reg_instr(KApply('LH'), rd, offset, rs1) + + +def lhu_instr(rd: KInner, offset: KInner, rs1: KInner) -> KInner: + return _reg_imm_reg_instr(KApply('LHU'), rd, offset, rs1) + + +def lb_instr(rd: KInner, offset: KInner, rs1: KInner) -> KInner: + return _reg_imm_reg_instr(KApply('LB'), rd, offset, rs1) + + +def lbu_instr(rd: KInner, offset: KInner, rs1: KInner) -> KInner: + return _reg_imm_reg_instr(KApply('LBU'), rd, offset, rs1) + + +def sw_instr(rs2: KInner, offset: KInner, rs1: KInner) -> KInner: + return _reg_imm_reg_instr(KApply('SW'), rs2, offset, rs1) + + +def sh_instr(rs2: KInner, offset: KInner, rs1: KInner) -> KInner: + return _reg_imm_reg_instr(KApply('SH'), rs2, offset, rs1) + + +def sb_instr(rs2: KInner, offset: KInner, rs1: KInner) -> KInner: + return _reg_imm_reg_instr(KApply('SB'), rs2, offset, rs1) + + +def _is_subseq(sub: Iterable[T], sup: Iterable[T]) -> bool: + it = iter(sup) + return all(x in it for x in sub) + + +def fence_bits(iorw_str: str) -> KInner: + if not _is_subseq(iorw_str, 'iorw'): + raise AssertionError(f"Expected a subsequence of 'iorw', but got {iorw_str!r}") + bits = ''.join('1' if c in iorw_str else '0' for c in 'iorw') + return intToken(int(bits, 2)) + + +def fence_instr(pred: KInner, succ: KInner) -> KInner: + return KApply('FENCE', pred, succ) + + +def fence_tso_instr() -> KInner: + return KApply('FENCETSO') + + +def ecall_instr() -> KInner: + return KApply('ECALL') + + +def ebreak_instr() -> KInner: + return KApply('EBREAK') + + +def invalid_instr() -> KInner: + return KApply('INVALID_INSTR') diff --git a/src/kriscv/tools.py b/src/kriscv/tools.py index f05aec46..c8887c2c 100644 --- a/src/kriscv/tools.py +++ b/src/kriscv/tools.py @@ -6,24 +6,29 @@ from pyk.kast.inner import Subst from pyk.ktool.krun import KRun from pyk.prelude.k import GENERATED_TOP_CELL +from pyk.prelude.kint import intToken -from kriscv import elf_parser +from kriscv import elf_parser, term_builder if TYPE_CHECKING: from pathlib import Path from pyk.kast.inner import KInner + from pyk.kllvm.runtime import Runtime from pyk.ktool.kprint import KPrint class Tools: __krun: KRun + __runtime: Runtime def __init__( self, definition_dir: Path, + runtime: Runtime, ) -> None: self.__krun = KRun(definition_dir) + self.__runtime = runtime @property def krun(self) -> KRun: @@ -33,6 +38,10 @@ def krun(self) -> KRun: def kprint(self) -> KPrint: return self.__krun + @property + def runtime(self) -> Runtime: + return self.__runtime + def init_config(self, config_vars: dict[str, KInner]) -> KInner: conf = self.krun.definition.init_config(sort=GENERATED_TOP_CELL) return Subst(config_vars)(conf) @@ -42,6 +51,23 @@ def run_config(self, config: KInner) -> KInner: final_config_kore = self.krun.run_pattern(config_kore) return self.krun.kore_to_kast(final_config_kore) - def run_elf(self, elf_file: Path) -> KInner: + def run_elf(self, elf_file: Path, *, end_symbol: str | None = None) -> KInner: with open(elf_file, 'rb') as f: - return self.run_config(self.init_config(elf_parser.config_vars(ELFFile(f)))) + elf = ELFFile(f) + if end_symbol is not None: + end_values = elf_parser.read_symbol(elf, end_symbol) + if len(end_values) == 0: + raise AssertionError(f'Cannot find end symbol {end_symbol!r}: {elf_file}') + if len(end_values) > 1: + raise AssertionError( + f'End symbol {end_symbol!r} should be unique, but found multiple instances: {elf_file}' + ) + halt_cond = term_builder.halt_at_address(intToken(end_values[0])) + else: + halt_cond = term_builder.halt_never() + config_vars = { + '$MEM': elf_parser.memory_map(elf), + '$PC': elf_parser.entry_point(elf), + '$HALT': halt_cond, + } + return self.run_config(self.init_config(config_vars)) diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py index c5c99f9b..34cc58d3 100644 --- a/src/tests/integration/test_integration.py +++ b/src/tests/integration/test_integration.py @@ -20,12 +20,15 @@ def _test_simple(elf_file: Path, expected_file: Path, update: bool) -> None: tools = semantics() - actual = tools.kprint.pretty_print(tools.run_elf(elf_file)) - expected = expected_file.read_text() + actual = tools.kprint.pretty_print(tools.run_elf(elf_file, end_symbol='_halt'), sort_collections=True) if update: + expected_file.touch() expected_file.write_text(actual) + return + expected_file = expected_file.resolve(strict=True) + expected = expected_file.read_text() assert actual == expected @@ -53,5 +56,5 @@ def test_simple(asm_file: Path, update_expected_output: bool, temp_dir: Path) -> ] subprocess.run(compile_cmd, check=True) assert elf_file.exists() - expected_file = Path(str(asm_file) + '.out').resolve(strict=True) + expected_file = Path(str(asm_file) + '.out') _test_simple(elf_file, expected_file, update_expected_output) diff --git a/src/tests/unit/test_unit.py b/src/tests/unit/test_unit.py index dc69d711..0449289e 100644 --- a/src/tests/unit/test_unit.py +++ b/src/tests/unit/test_unit.py @@ -1,5 +1,243 @@ -from kriscv.hello import hello +from __future__ import annotations +from typing import TYPE_CHECKING -def test_hello() -> None: - assert hello('World') == 'Hello, World!' +# isort: off +from kriscv.build import semantics + +# isort: on +import pytest +from pyk.kllvm.convert import llvm_to_pattern, pattern_to_llvm +from pyk.prelude.kint import intToken + +from kriscv import term_builder +from kriscv.term_builder import register + +if TYPE_CHECKING: + from typing import Final + + from pyk.kast.inner import KInner + +DISASS_TEST_DATA: Final = ( + ( + 'addi x1, x2, 3', + '00000000010100010000000010010011', + term_builder.addi_instr(register(1), register(2), intToken(5)), + ), + ( + 'slti x2, x3, 2047', + '01111111111100011010000100010011', + term_builder.slti_instr(register(2), register(3), intToken(2047)), + ), + ( + 'sltiu x3, x4, -2048', + '10000000000000100011000110010011', + term_builder.sltiu_instr(register(3), register(4), intToken(-2048)), + ), + ( + 'andi x4, x5, -1', + '11111111111100101111001000010011', + term_builder.andi_instr(register(4), register(5), intToken(-1)), + ), + ( + 'ori x5, x6, -2', + '11111111111000110110001010010011', + term_builder.ori_instr(register(5), register(6), intToken(-2)), + ), + ( + 'xori x6, x7, 3', + '00000000001100111100001100010011', + term_builder.xori_instr(register(6), register(7), intToken(3)), + ), + ( + 'slli x7, x8, 31', + '00000001111101000001001110010011', + term_builder.slli_instr(register(7), register(8), intToken(31)), + ), + ( + 'srli x8, x9, 1', + '00000000000101001101010000010011', + term_builder.srli_instr(register(8), register(9), intToken(1)), + ), + ( + 'srai x9, x10, 2', + '01000000001001010101010010010011', + term_builder.srai_instr(register(9), register(10), intToken(2)), + ), + ( + 'beq x10, x11, 4094', + '01111110101101010000111111100011', + term_builder.beq_instr(register(10), register(11), intToken(4094)), + ), + ( + 'bne x11, x12, -4096', + '10000000110001011001000001100011', + term_builder.bne_instr(register(11), register(12), intToken(-4096)), + ), + ( + 'blt x12, x13, 0', + '00000000110101100100000001100011', + term_builder.blt_instr(register(12), register(13), intToken(0)), + ), + ( + 'bltu x13, x14, -100', + '11111000111001101110111011100011', + term_builder.bltu_instr(register(13), register(14), intToken(-100)), + ), + ( + 'bge x14, x15, 2048', + '00000000111101110101000011100011', + term_builder.bge_instr(register(14), register(15), intToken(2048)), + ), + ( + 'bgeu x15, x15, -2050', + '11111110111101111111111101100011', + term_builder.bgeu_instr(register(15), register(15), intToken(-2050)), + ), + ( + 'lui x1, 0xFFFFF', + '11111111111111111111000010110111', + term_builder.lui_instr(register(1), intToken(int('FFFFF', 16))), + ), + ( + 'auipc x2, 0xA1', + '00000000000010100001000100010111', + term_builder.auipc_instr(register(2), intToken(int('A1', 16))), + ), + ('jal x0, -1048576', '10000000000000000000000001101111', term_builder.jal_instr(register(0), intToken(-1048576))), + ( + 'add x0, x1, x2', + '00000000001000001000000000110011', + term_builder.add_instr(register(0), register(1), register(2)), + ), + ( + 'sub x3, x4, x5', + '01000000010100100000000110110011', + term_builder.sub_instr(register(3), register(4), register(5)), + ), + ( + 'slt x6, x7, x8', + '00000000100000111010001100110011', + term_builder.slt_instr(register(6), register(7), register(8)), + ), + ( + 'sltu x9, x10, x11', + '00000000101101010011010010110011', + term_builder.sltu_instr(register(9), register(10), register(11)), + ), + ( + 'and x12, x13, x14', + '00000000111001101111011000110011', + term_builder.and_instr(register(12), register(13), register(14)), + ), + ( + 'or x15, x0, x1', + '00000000000100000110011110110011', + term_builder.or_instr(register(15), register(0), register(1)), + ), + ( + 'xor x2, x3, x4', + '00000000010000011100000100110011', + term_builder.xor_instr(register(2), register(3), register(4)), + ), + ( + 'sll x5, x6, x7', + '00000000011100110001001010110011', + term_builder.sll_instr(register(5), register(6), register(7)), + ), + ( + 'srl x8, x9, x10', + '00000000101001001101010000110011', + term_builder.srl_instr(register(8), register(9), register(10)), + ), + ( + 'sra x11, x12, x13', + '01000000110101100101010110110011', + term_builder.sra_instr(register(11), register(12), register(13)), + ), + ( + 'jalr x0, -2048(x1)', + '10000000000000001000000001100111', + term_builder.jalr_instr(register(0), intToken(-2048), register(1)), + ), + ( + 'lw x2, 2047(x3)', + '01111111111100011010000100000011', + term_builder.lw_instr(register(2), intToken(2047), register(3)), + ), + ( + 'lh x4, 0(x5)', + '00000000000000101001001000000011', + term_builder.lh_instr(register(4), intToken(0), register(5)), + ), + ( + 'lhu x6, 7(x7)', + '00000000011100111101001100000011', + term_builder.lhu_instr(register(6), intToken(7), register(7)), + ), + ( + 'lb x8, -10(x9)', + '11111111011001001000010000000011', + term_builder.lb_instr(register(8), intToken(-10), register(9)), + ), + ( + 'lbu x10, 2047(x11)', + '01111111111101011100010100000011', + term_builder.lbu_instr(register(10), intToken(2047), register(11)), + ), + ( + 'sw x2, 2047(x3)', + '01111110001000011010111110100011', + term_builder.sw_instr(register(2), intToken(2047), register(3)), + ), + ( + 'sh x4, 0(x5)', + '00000000010000101001000000100011', + term_builder.sh_instr(register(4), intToken(0), register(5)), + ), + ( + 'sb x8, -10(x9)', + '11111110100001001000101100100011', + term_builder.sb_instr(register(8), intToken(-10), register(9)), + ), + ( + 'fence ow, ir', + '00000101101000000000000000001111', + term_builder.fence_instr(term_builder.fence_bits('ow'), term_builder.fence_bits('ir')), + ), + ( + 'fence.tso', + '10000011001100000000000000001111', + term_builder.fence_tso_instr(), + ), + ( + 'ecall', + '00000000000000000000000001110011', + term_builder.ecall_instr(), + ), + ( + 'ebreak', + '00000000000100000000000001110011', + term_builder.ebreak_instr(), + ), + ( + 'invalid instruction', + '00000000000000000000000000000000', + term_builder.invalid_instr(), + ), +) + + +@pytest.mark.parametrize( + 'instr_bits,expected', + [(instr_bits, expected) for (_, instr_bits, expected) in DISASS_TEST_DATA], + ids=[test_id for test_id, *_ in DISASS_TEST_DATA], +) +def test_disassemble(instr_bits: str, expected: KInner) -> None: + assert len(instr_bits) == 32 + tools = semantics() + disass_call = term_builder.disassemble(intToken(int(instr_bits, 2))) + disass_call_llvm = pattern_to_llvm(tools.krun.kast_to_kore(disass_call, term_builder.sort_instruction())) + actual_llvm = tools.runtime.evaluate(disass_call_llvm) + actual = tools.krun.kore_to_kast(llvm_to_pattern(actual_llvm)) + assert actual == expected diff --git a/tests/README.md b/tests/README.md index d2c32d0d..5045e84a 100644 --- a/tests/README.md +++ b/tests/README.md @@ -32,4 +32,4 @@ A suite of handwritten RISC-V tests. Inputs are RISC-V ASM files `test.S` which ``` riscv64-unknown-elf-gcc -nostdlib -nostartfiles -static -march=rv32e -mabi=ilp32e -mno-relax -mlittle-endian -Xassembler -mno-arch-attr test.S ``` -NOT YET IMPLEMENTED: Each input file must define global symbols `_start` and `_end`. The test is executed with the PC initially set to `_start`, and will halt when the PC reaches `_end`. The final KAST configuration is compared against `test.S.out`. +Each input file must define global symbols `_start` and `_halt`. The test is executed with the PC initially set to `_start`, and will halt when the PC reaches `_halt`. The final KAST configuration is compared against `test.S.out`. diff --git a/tests/simple/addi-overflow.S b/tests/simple/addi-overflow.S new file mode 100644 index 00000000..74abb204 --- /dev/null +++ b/tests/simple/addi-overflow.S @@ -0,0 +1,13 @@ +.text +.globl _start +_start: + lui x1, 0x7FFFF + addi x1, x1, 2047 + addi x1, x1, 2047 + addi x1, x1, 1 + // x1 contains 2^31 - 1, the largest 32-bit two's complement integer. + // Setting x2 = x1 + 1 should overflow + addi x2, x1, 1 +.globl _halt +_halt: + nop diff --git a/tests/simple/addi-overflow.S.out b/tests/simple/addi-overflow.S.out new file mode 100644 index 00000000..75fb36be --- /dev/null +++ b/tests/simple/addi-overflow.S.out @@ -0,0 +1,24 @@ + + + + .K + + + 65536 |-> 127 65537 |-> 69 65538 |-> 76 65539 |-> 70 65540 |-> 1 65541 |-> 1 65542 |-> 1 65543 |-> 0 65544 |-> 0 65545 |-> 0 65546 |-> 0 65547 |-> 0 65548 |-> 0 65549 |-> 0 65550 |-> 0 65551 |-> 0 65552 |-> 2 65553 |-> 0 65554 |-> 243 65555 |-> 0 65556 |-> 1 65557 |-> 0 65558 |-> 0 65559 |-> 0 65560 |-> 84 65561 |-> 0 65562 |-> 1 65563 |-> 0 65564 |-> 52 65565 |-> 0 65566 |-> 0 65567 |-> 0 65568 |-> 208 65569 |-> 1 65570 |-> 0 65571 |-> 0 65572 |-> 8 65573 |-> 0 65574 |-> 0 65575 |-> 0 65576 |-> 52 65577 |-> 0 65578 |-> 32 65579 |-> 0 65580 |-> 1 65581 |-> 0 65582 |-> 40 65583 |-> 0 65584 |-> 5 65585 |-> 0 65586 |-> 4 65587 |-> 0 65588 |-> 1 65589 |-> 0 65590 |-> 0 65591 |-> 0 65592 |-> 0 65593 |-> 0 65594 |-> 0 65595 |-> 0 65596 |-> 0 65597 |-> 0 65598 |-> 1 65599 |-> 0 65600 |-> 0 65601 |-> 0 65602 |-> 1 65603 |-> 0 65604 |-> 108 65605 |-> 0 65606 |-> 0 65607 |-> 0 65608 |-> 108 65609 |-> 0 65610 |-> 0 65611 |-> 0 65612 |-> 5 65613 |-> 0 65614 |-> 0 65615 |-> 0 65616 |-> 0 65617 |-> 16 65618 |-> 0 65619 |-> 0 65620 |-> 183 65621 |-> 240 65622 |-> 255 65623 |-> 127 65624 |-> 147 65625 |-> 128 65626 |-> 240 65627 |-> 127 65628 |-> 147 65629 |-> 128 65630 |-> 240 65631 |-> 127 65632 |-> 147 65633 |-> 128 65634 |-> 16 65635 |-> 0 65636 |-> 19 65637 |-> 129 65638 |-> 16 65639 |-> 0 65640 |-> 19 65641 |-> 0 65642 |-> 0 65643 |-> 0 + + + 1 |-> 2147483647 2 |-> -2147483648 + + + 65640 + + + + + ADDRESS ( 65640 ) + + + + 0 + + \ No newline at end of file diff --git a/tests/simple/addi.S b/tests/simple/addi.S new file mode 100644 index 00000000..15fa0f0f --- /dev/null +++ b/tests/simple/addi.S @@ -0,0 +1,9 @@ +.text +.globl _start +_start: + addi x1, x0, 8 + addi x1, x1, 8 + addi x2, x1, 0 +.globl _halt +_halt: + nop diff --git a/tests/simple/addi.S.out b/tests/simple/addi.S.out new file mode 100644 index 00000000..86967e63 --- /dev/null +++ b/tests/simple/addi.S.out @@ -0,0 +1,24 @@ + + + + .K + + + 65536 |-> 127 65537 |-> 69 65538 |-> 76 65539 |-> 70 65540 |-> 1 65541 |-> 1 65542 |-> 1 65543 |-> 0 65544 |-> 0 65545 |-> 0 65546 |-> 0 65547 |-> 0 65548 |-> 0 65549 |-> 0 65550 |-> 0 65551 |-> 0 65552 |-> 2 65553 |-> 0 65554 |-> 243 65555 |-> 0 65556 |-> 1 65557 |-> 0 65558 |-> 0 65559 |-> 0 65560 |-> 84 65561 |-> 0 65562 |-> 1 65563 |-> 0 65564 |-> 52 65565 |-> 0 65566 |-> 0 65567 |-> 0 65568 |-> 200 65569 |-> 1 65570 |-> 0 65571 |-> 0 65572 |-> 8 65573 |-> 0 65574 |-> 0 65575 |-> 0 65576 |-> 52 65577 |-> 0 65578 |-> 32 65579 |-> 0 65580 |-> 1 65581 |-> 0 65582 |-> 40 65583 |-> 0 65584 |-> 5 65585 |-> 0 65586 |-> 4 65587 |-> 0 65588 |-> 1 65589 |-> 0 65590 |-> 0 65591 |-> 0 65592 |-> 0 65593 |-> 0 65594 |-> 0 65595 |-> 0 65596 |-> 0 65597 |-> 0 65598 |-> 1 65599 |-> 0 65600 |-> 0 65601 |-> 0 65602 |-> 1 65603 |-> 0 65604 |-> 100 65605 |-> 0 65606 |-> 0 65607 |-> 0 65608 |-> 100 65609 |-> 0 65610 |-> 0 65611 |-> 0 65612 |-> 5 65613 |-> 0 65614 |-> 0 65615 |-> 0 65616 |-> 0 65617 |-> 16 65618 |-> 0 65619 |-> 0 65620 |-> 147 65621 |-> 0 65622 |-> 128 65623 |-> 0 65624 |-> 147 65625 |-> 128 65626 |-> 128 65627 |-> 0 65628 |-> 19 65629 |-> 129 65630 |-> 0 65631 |-> 0 65632 |-> 19 65633 |-> 0 65634 |-> 0 65635 |-> 0 + + + 1 |-> 16 2 |-> 16 + + + 65632 + + + + + ADDRESS ( 65632 ) + + + + 0 + + \ No newline at end of file diff --git a/tests/simple/example.S b/tests/simple/example.S deleted file mode 100644 index 5d640854..00000000 --- a/tests/simple/example.S +++ /dev/null @@ -1,4 +0,0 @@ -.text -.globl _start -_start: - j _start diff --git a/tests/simple/example.S.out b/tests/simple/example.S.out deleted file mode 100644 index 5d8320b6..00000000 --- a/tests/simple/example.S.out +++ /dev/null @@ -1,11 +0,0 @@ - - - [ 65536 , 65624 ) r|-> b"\x7fELF\x01\x01\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02\x00\xf3\x00\x01\x00\x00\x00T\x00\x01\x004\x00\x00\x00\xa8\x01\x00\x00\x08\x00\x00\x004\x00 \x00\x01\x00(\x00\x05\x00\x04\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x01\x00X\x00\x00\x00X\x00\x00\x00\x05\x00\x00\x00\x00\x10\x00\x00o\x00\x00\x00" - - - 65620 - - - 0 - - \ No newline at end of file diff --git a/tests/simple/lui.S b/tests/simple/lui.S new file mode 100644 index 00000000..a2ea8f23 --- /dev/null +++ b/tests/simple/lui.S @@ -0,0 +1,9 @@ +.text +.globl _start +_start: + lui x0, 0x10 + lui x1, 0x80000 + lui x2, 0x70000 +.globl _halt +_halt: + nop diff --git a/tests/simple/lui.S.out b/tests/simple/lui.S.out new file mode 100644 index 00000000..9d628bdc --- /dev/null +++ b/tests/simple/lui.S.out @@ -0,0 +1,24 @@ + + + + .K + + + 65536 |-> 127 65537 |-> 69 65538 |-> 76 65539 |-> 70 65540 |-> 1 65541 |-> 1 65542 |-> 1 65543 |-> 0 65544 |-> 0 65545 |-> 0 65546 |-> 0 65547 |-> 0 65548 |-> 0 65549 |-> 0 65550 |-> 0 65551 |-> 0 65552 |-> 2 65553 |-> 0 65554 |-> 243 65555 |-> 0 65556 |-> 1 65557 |-> 0 65558 |-> 0 65559 |-> 0 65560 |-> 84 65561 |-> 0 65562 |-> 1 65563 |-> 0 65564 |-> 52 65565 |-> 0 65566 |-> 0 65567 |-> 0 65568 |-> 200 65569 |-> 1 65570 |-> 0 65571 |-> 0 65572 |-> 8 65573 |-> 0 65574 |-> 0 65575 |-> 0 65576 |-> 52 65577 |-> 0 65578 |-> 32 65579 |-> 0 65580 |-> 1 65581 |-> 0 65582 |-> 40 65583 |-> 0 65584 |-> 5 65585 |-> 0 65586 |-> 4 65587 |-> 0 65588 |-> 1 65589 |-> 0 65590 |-> 0 65591 |-> 0 65592 |-> 0 65593 |-> 0 65594 |-> 0 65595 |-> 0 65596 |-> 0 65597 |-> 0 65598 |-> 1 65599 |-> 0 65600 |-> 0 65601 |-> 0 65602 |-> 1 65603 |-> 0 65604 |-> 100 65605 |-> 0 65606 |-> 0 65607 |-> 0 65608 |-> 100 65609 |-> 0 65610 |-> 0 65611 |-> 0 65612 |-> 5 65613 |-> 0 65614 |-> 0 65615 |-> 0 65616 |-> 0 65617 |-> 16 65618 |-> 0 65619 |-> 0 65620 |-> 55 65621 |-> 0 65622 |-> 1 65623 |-> 0 65624 |-> 183 65625 |-> 0 65626 |-> 0 65627 |-> 128 65628 |-> 55 65629 |-> 1 65630 |-> 0 65631 |-> 112 65632 |-> 19 65633 |-> 0 65634 |-> 0 65635 |-> 0 + + + 1 |-> -2147483648 2 |-> 1879048192 + + + 65632 + + + + + ADDRESS ( 65632 ) + + + + 0 + + \ No newline at end of file