From 606f33b8254af9cce1f8b3cca6e09e5dc345b18e Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Thu, 1 Aug 2024 12:41:56 -0700 Subject: [PATCH] Implement RV32 instructions (#28) * README.md: Fix call to kriscv run * Check output of run_pattern for better error messages * Fix >>aWord and >>lWord to account for >>Int requiring infinite sign extension to properly do an arithmetic shift * Sign extend the LUI immediate for when XLEN > 32 * Update CHECK_HALT rules to only apply when we haven't halted already * Add macros for simple tests * Refactor simple tests to have a YAML assertion file instead of the full configuration output * Fold addi-overflow.S into addi.S * Implement SLTI and SLTIU * Implement ANDI, ORI, and XORI * Implement SLLI, SRLI, and SRAI * Implement AUIPC and ADD * Implement SUB, SLT, SLTU, AND, OR, and XOR * Implement SLL, SRL, and SRA * Implement JAL * Implement JALR * Implement BEQ, BNE, BLT, BGE, BLTU, and BGEU * Implement LB, LH, LW, LBU, LHU, SB, SH, and SW * Implement FENCE, FENCE.TSO, ECALL, and EBREAK * Refactor the halting mechanism to make it possible to cleanly halt at any point, as will be necessary for, e.g., illegal instruction exceptions. * Pull the PC increment out into a separate pipeline step * Use a branchPC function for branch instrs rather than two separate rules * Set Version: 0.1.20 * Add comments explaining why the arithmetic >>Int is used to implement the logical >>lWord --------- Co-authored-by: devops --- Makefile | 3 + README.md | 2 +- package/version | 2 +- pyproject.toml | 2 +- src/kriscv/kdist/riscv-semantics/riscv.md | 273 +++++++++++++++++++--- src/kriscv/kdist/riscv-semantics/word.md | 19 +- src/kriscv/term_manip.py | 36 +++ src/kriscv/tools.py | 25 +- src/tests/conftest.py | 8 +- src/tests/integration/test_integration.py | 117 +++++++++- tests/README.md | 28 ++- tests/simple/add.S | 14 ++ tests/simple/add.S.assert | 1 + tests/simple/addi-overflow.S | 13 -- tests/simple/addi-overflow.S.out | 27 --- tests/simple/addi.S | 24 +- tests/simple/addi.S.assert | 1 + tests/simple/addi.S.out | 27 --- tests/simple/and.S | 15 ++ tests/simple/and.S.assert | 2 + tests/simple/andi.S | 10 + tests/simple/andi.S.assert | 2 + tests/simple/auipc.S | 16 ++ tests/simple/auipc.S.assert | 1 + tests/simple/beq.S | 13 ++ tests/simple/beq.S.assert | 1 + tests/simple/bge.S | 21 ++ tests/simple/bge.S.assert | 2 + tests/simple/bgeu.S | 21 ++ tests/simple/bgeu.S.assert | 2 + tests/simple/blt.S | 21 ++ tests/simple/blt.S.assert | 2 + tests/simple/bltu.S | 21 ++ tests/simple/bltu.S.assert | 2 + tests/simple/bne.S | 13 ++ tests/simple/bne.S.assert | 1 + tests/simple/jal.S | 19 ++ tests/simple/jal.S.assert | 1 + tests/simple/jalr.S | 20 ++ tests/simple/jalr.S.assert | 1 + tests/simple/load-store.S | 47 ++++ tests/simple/load-store.S.assert | 7 + tests/simple/lui.S | 16 +- tests/simple/lui.S.assert | 1 + tests/simple/lui.S.out | 27 --- tests/simple/or.S | 13 ++ tests/simple/or.S.assert | 1 + tests/simple/ori.S | 9 + tests/simple/ori.S.assert | 1 + tests/simple/simple.h | 19 ++ tests/simple/sll.S | 12 + tests/simple/sll.S.assert | 1 + tests/simple/slli.S | 8 + tests/simple/slli.S.assert | 1 + tests/simple/slt.S | 20 ++ tests/simple/slt.S.assert | 1 + tests/simple/slti.S | 14 ++ tests/simple/slti.S.assert | 1 + tests/simple/sltiu.S | 14 ++ tests/simple/sltiu.S.assert | 1 + tests/simple/sltu.S | 19 ++ tests/simple/sltu.S.assert | 1 + tests/simple/sra.S | 11 + tests/simple/sra.S.assert | 1 + tests/simple/sra.S.simple | 1 + tests/simple/srai.S | 8 + tests/simple/srai.S.assert | 1 + tests/simple/srl.S | 12 + tests/simple/srl.S.assert | 1 + tests/simple/srli.S | 8 + tests/simple/srli.S.assert | 1 + tests/simple/sub.S | 13 ++ tests/simple/sub.S.assert | 1 + tests/simple/xor.S | 15 ++ tests/simple/xor.S.assert | 1 + tests/simple/xori.S | 10 + tests/simple/xori.S.assert | 1 + 77 files changed, 973 insertions(+), 175 deletions(-) create mode 100644 src/kriscv/term_manip.py create mode 100644 tests/simple/add.S create mode 100644 tests/simple/add.S.assert delete mode 100644 tests/simple/addi-overflow.S delete mode 100644 tests/simple/addi-overflow.S.out create mode 100644 tests/simple/addi.S.assert delete mode 100644 tests/simple/addi.S.out create mode 100644 tests/simple/and.S create mode 100644 tests/simple/and.S.assert create mode 100644 tests/simple/andi.S create mode 100644 tests/simple/andi.S.assert create mode 100644 tests/simple/auipc.S create mode 100644 tests/simple/auipc.S.assert create mode 100644 tests/simple/beq.S create mode 100644 tests/simple/beq.S.assert create mode 100644 tests/simple/bge.S create mode 100644 tests/simple/bge.S.assert create mode 100644 tests/simple/bgeu.S create mode 100644 tests/simple/bgeu.S.assert create mode 100644 tests/simple/blt.S create mode 100644 tests/simple/blt.S.assert create mode 100644 tests/simple/bltu.S create mode 100644 tests/simple/bltu.S.assert create mode 100644 tests/simple/bne.S create mode 100644 tests/simple/bne.S.assert create mode 100644 tests/simple/jal.S create mode 100644 tests/simple/jal.S.assert create mode 100644 tests/simple/jalr.S create mode 100644 tests/simple/jalr.S.assert create mode 100644 tests/simple/load-store.S create mode 100644 tests/simple/load-store.S.assert create mode 100644 tests/simple/lui.S.assert delete mode 100644 tests/simple/lui.S.out create mode 100644 tests/simple/or.S create mode 100644 tests/simple/or.S.assert create mode 100644 tests/simple/ori.S create mode 100644 tests/simple/ori.S.assert create mode 100644 tests/simple/simple.h create mode 100644 tests/simple/sll.S create mode 100644 tests/simple/sll.S.assert create mode 100644 tests/simple/slli.S create mode 100644 tests/simple/slli.S.assert create mode 100644 tests/simple/slt.S create mode 100644 tests/simple/slt.S.assert create mode 100644 tests/simple/slti.S create mode 100644 tests/simple/slti.S.assert create mode 100644 tests/simple/sltiu.S create mode 100644 tests/simple/sltiu.S.assert create mode 100644 tests/simple/sltu.S create mode 100644 tests/simple/sltu.S.assert create mode 100644 tests/simple/sra.S create mode 100644 tests/simple/sra.S.assert create mode 100644 tests/simple/sra.S.simple create mode 100644 tests/simple/srai.S create mode 100644 tests/simple/srai.S.assert create mode 100644 tests/simple/srl.S create mode 100644 tests/simple/srl.S.assert create mode 100644 tests/simple/srli.S create mode 100644 tests/simple/srli.S.assert create mode 100644 tests/simple/sub.S create mode 100644 tests/simple/sub.S.assert create mode 100644 tests/simple/xor.S create mode 100644 tests/simple/xor.S.assert create mode 100644 tests/simple/xori.S create mode 100644 tests/simple/xori.S.assert diff --git a/Makefile b/Makefile index 0f2adbdc..8a054d17 100644 --- a/Makefile +++ b/Makefile @@ -44,6 +44,9 @@ test-unit: poetry-install test-integration: tests/riscv-arch-test-compiled poetry-install $(POETRY_RUN) pytest src/tests/integration --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS) +test-simple: poetry-install + $(POETRY_RUN) pytest src/tests/integration/test_integration.py --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS) + RISCOF_DIRS = $(shell find src/tests/integration/riscof -type d) RISCOF_FILES = $(shell find src/tests/integration/riscof -type f) diff --git a/README.md b/README.md index 7b93245a..a9d1e46c 100644 --- a/README.md +++ b/README.md @@ -25,7 +25,7 @@ make kdist-build ## Usage Execute a compiled RISC-V ELF file with the following command: ```bash -poetry -C kriscv run test.elf +poetry -C kriscv run kriscv run test.elf ``` The output shows the final K configuration, including the state of memory, all registers, and any encountered errors. Execution can also be halted at a particular global symbol by providing the `--end-symbol` flag. diff --git a/package/version b/package/version index d8a023ec..baa98378 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.19 +0.1.20 diff --git a/pyproject.toml b/pyproject.toml index 6630da57..ecc48bf8 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kriscv" -version = "0.1.19" +version = "0.1.20" description = "K tooling for the RISC-V architecture" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kriscv/kdist/riscv-semantics/riscv.md b/src/kriscv/kdist/riscv-semantics/riscv.md index a86e8c02..38241cb4 100644 --- a/src/kriscv/kdist/riscv-semantics/riscv.md +++ b/src/kriscv/kdist/riscv-semantics/riscv.md @@ -1,18 +1,17 @@ # RISC-V Execution ## Configuration The configuration is divided into two sections: -- ``, containing the state of the abstract machine -- ``, containing any additional state needed to run tests +- ``, containing the state of the abstract machine. +- ``, containing any additional state needed to run tests. The `` section contain the following cells: -- ``, a K-sequence of fetched instruction to be executed -- ``, a map from each initialized `Register` to its current value -- ``, the program counter register -- ``, a map from initialized `Word` addresses to the byte stored at the address +- ``, a K-sequence denoting a pipeline of operations to be executed. Initially, we load the `#EXECUTE` operation, which indicates that instructions should be continually fetched and executed. +- ``, a map from each initialized `Register` to its current value. +- ``, the program counter register. +- ``, a map from initialized `Word` addresses to the byte stored at the address. The `` section currently contains on a single cell: -- ``, a value indicating under which conditions the program should be halted -- ``, whether to halt the program +- ``, a value indicating under which conditions the program should be halted. ```k requires "riscv-disassemble.md" requires "riscv-instructions.md" @@ -25,48 +24,63 @@ module RISCV-CONFIGURATION imports RANGEMAP imports WORD - syntax HaltCondition + syntax KItem ::= "#EXECUTE" configuration - .K + #EXECUTE ~> .K .Map // Map{Register, Word} $PC:Word $MEM:Map // Map{Word, Int} $HALT:HaltCondition - false:Bool + + syntax HaltCondition endmodule ``` ## Termination -RISC-V does not provide a `halt` instruction, instead relying on the surrounding environment, e.g., making a sys-call to exit with a particular exit code. -For testing purposes, we then add our own custom halting mechanism denoted by a `HaltCondition` value. +RISC-V does not provide a `halt` instruction or equivalent, instead relying on the surrounding environment, e.g., making a sys-call to exit with a particular exit code. +As we do not model the surrounding environment, for testing purposes we add our own custom halting mechanism denoted by a `HaltCondition` value. -Currently, we support: -- Never halting unless a trap or exception is reached -- Halting when the `PC` reaches a particular address +This is done with three components: +- A `HaltCondition` value stored in the configuation indicating under which conditions we should halt. +- A `#CHECK_HALT` operation indicating that the halt condition should be checked. +- A `#HALT` operation which terminates the simulation by consuming all following operations in the pipeline without executing them. ```k module RISCV-TERMINATION imports RISCV-CONFIGURATION imports BOOL imports INT - syntax Instruction ::= "CHECK_HALT" + syntax KItem ::= + "#HALT" + | "#CHECK_HALT" + + rule #HALT ~> (_ => .K) ... syntax HaltCondition ::= "NEVER" [symbol(HaltNever)] | "ADDRESS" "(" Word ")" [symbol(HaltAtAddress)] - - rule CHECK_HALT => .K ... +``` +The `NEVER` condition indicates that we should never halt. +```k + rule #CHECK_HALT => .K ... NEVER +``` +The `ADDRESS(_)` condition indicates that we should halt if the `PC` reaches a particular address. +```k + rule #CHECK_HALT => #HALT ... + PC + ADDRESS(END) + requires PC ==Word END - rule CHECK_HALT => .K ... + rule #CHECK_HALT => .K ... PC ADDRESS(END) - _ => PC ==Word END + requires PC =/=Word END endmodule ``` @@ -82,10 +96,23 @@ module RISCV-MEMORY imports RISCV-INSTRUCTIONS imports WORD ``` -We abstract the particular memory representation behind a `loadByte` function which return the byte stored at a particular address. +We abstract the particular memory representation behind `loadByte` and `storeByte` functions. ```k syntax Int ::= loadByte(memory: Map, address: Word) [function] rule loadByte(MEM, ADDR) => { MEM[ADDR] } :>Int + + syntax Map ::= storeByte(memory: Map, address: Word, byte: Int) [function, total] + rule storeByte(MEM, ADDR, B) => MEM[ADDR <- B] +``` +For multi-byte loads and stores, we presume a little-endian architecture. +```k + syntax Int ::= loadBytes(memory: Map, address: Word, numBytes: Int) [function] + rule loadBytes(MEM, ADDR, 1 ) => loadByte(MEM, ADDR) + rule loadBytes(MEM, ADDR, NUM) => (loadBytes(MEM, ADDR +Word W(1), NUM -Int 1) <Int 1 + + syntax Map ::= storeBytes(memory: Map, address: Word, bytes: Int, numBytes: Int) [function] + rule storeBytes(MEM, ADDR, BS, 1 ) => storeByte(MEM, ADDR, BS) + rule storeBytes(MEM, ADDR, BS, NUM) => storeBytes(storeByte(MEM, ADDR, BS &Int 255), ADDR +Word W(1), BS >>Int 8, NUM -Int 1) requires NUM >Int 1 ``` Instructions are always 32-bits, and are stored in little-endian format regardless of the endianness of the overall architecture. ```k @@ -109,9 +136,7 @@ endmodule ``` ## Instruction Execution -The actual execution semantics has two components: -- The instruction fetch cycle, which disassembles an instruction from the current `PC` so long as the `HaltCondition` fails, placing it into the `` cell -- Rules to implement each instruction, removing the instruction from the top of the `` cell and updating any state as necessary. +The `RISCV` module contains the actual rules to fetch and execute instructions. ```k module RISCV imports RISCV-CONFIGURATION @@ -120,22 +145,210 @@ module RISCV imports RISCV-MEMORY imports RISCV-TERMINATION imports WORD +``` +`#EXECUTE` indicates that we should continuously fetch and execute instructions, loading the instruction into the `#NEXT[_]` operator. +```k + syntax KItem ::= "#NEXT" "[" Instruction "]" - rule .K => fetchInstr(MEM, PC) ~> CHECK_HALT + rule (.K => #NEXT[ fetchInstr(MEM, PC) ]) ~> #EXECUTE ... PC MEM - false ``` +`#NEXT[ I ]` sets up the pipeline to execute the the fetched instruction. +```k + rule #NEXT[ I ] => I ~> #PC[ I ] ~> #CHECK_HALT ... +``` +`#PC[ I ]` updates the `PC` as needed to fetch the next instruction after executing `I`. For most instructions, this increments `PC` by the width of the instruction (always `4` bytes in the base ISA). For branch and jump instructions, which already manually update the `PC`, this is a no-op. +```k + syntax KItem ::= "#PC" "[" Instruction "]" + + rule #PC[ I ] => .K ... + PC => PC +Word pcIncrAmount(I) + + syntax Word ::= pcIncrAmount(Instruction) [function, total] + rule pcIncrAmount(BEQ _ , _ , _ ) => W(0) + rule pcIncrAmount(BNE _ , _ , _ ) => W(0) + rule pcIncrAmount(BLT _ , _ , _ ) => W(0) + rule pcIncrAmount(BLTU _ , _ , _ ) => W(0) + rule pcIncrAmount(BGE _ , _ , _ ) => W(0) + rule pcIncrAmount(BGEU _ , _ , _ ) => W(0) + rule pcIncrAmount(JAL _ , _ ) => W(0) + rule pcIncrAmount(JALR _ , _ ( _ )) => W(0) + rule pcIncrAmount(_) => W(4) [owise] +``` +We then provide rules to consume and execute each instruction from the top of the pipeline. + `ADDI` adds the immediate `IMM` to the value in register `RS`, storing the result in register `RD`. Note that we must use `chop` to convert `IMM` from an infinitely sign-extended K `Int` to an `XLEN`-bit `Word`. ```k rule ADDI RD , RS , IMM => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS) +Word chop(IMM)) - PC => PC +Word W(4) +``` +`SLTI` treats the value in `RS` as a signed two's complement and compares it to `IMM`, writing `1` to `RD` if `RS` is less than `IMM` and `0` otherwise. +```k + rule SLTI RD , RS , IMM => .K ... + REGS => writeReg(REGS, RD, Bool2Word(readReg(REGS, RS) +``` +`SLTIU` proceeds analogously, but treating `RS` and `IMM` as XLEN-bit unsigned integers. +```k + rule SLTIU RD , RS , IMM => .K ... + REGS => writeReg(REGS, RD, Bool2Word(readReg(REGS, RS) +``` +`ADDI`, `ORI`, and `XORI` perform bitwise operations between `RS` and `IMM`, storing the result in `RD`. +```k + rule ANDI RD , RS , IMM => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS) &Word chop(IMM)) + + rule ORI RD , RS , IMM => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS) |Word chop(IMM)) + + rule XORI RD , RS , IMM => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS) xorWord chop(IMM)) +``` +`SLLI`, `SRLI`, and `SRAI` perform logical left, logical right, and arithmetic right shifts respectively. +```k + rule SLLI RD , RS , SHAMT => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS) < + + rule SRLI RD , RS , SHAMT => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS) >>lWord SHAMT) + + rule SRAI RD , RS , SHAMT => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS) >>aWord SHAMT) ``` `LUI` builds a 32-bit constant from the 20-bit immediate by setting the 12 least-significant bits to `0`, then sign extends to `XLEN` bits and places the result in register `RD`. ```k rule LUI RD , IMM => .K ... - REGS => writeReg(REGS, RD, W(IMM < - PC => PC +Word W(4) + REGS => writeReg(REGS, RD, signExtend(IMM < +``` +`AUIPC` proceeds similarly to `LUI`, but adding the sign-extended constant to the current `PC` before placing the result in `RD`. +```k + rule AUIPC RD , IMM => .K ... + REGS => writeReg(REGS, RD, PC +Word signExtend(IMM < + PC +``` +The following instructions behave analogously to their `I`-suffixed counterparts, but taking their second argument from an `RS2` register rather than an immediate. +```k + rule ADD RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) +Word readReg(REGS, RS2)) + + rule SUB RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) -Word readReg(REGS, RS2)) + + rule SLT RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, Bool2Word(readReg(REGS, RS1) + + rule SLTU RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, Bool2Word(readReg(REGS, RS1) + + rule AND RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) &Word readReg(REGS, RS2)) + + rule OR RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) |Word readReg(REGS, RS2)) + + rule XOR RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) xorWord readReg(REGS, RS2)) +``` +`SLL`, `SRL`, and `SRA` read their shift amount fom the lowest `log_2(XLEN)` bits of `RS2`. +```k + rule SLL RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) < + + rule SRL RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) >>lWord Word2UInt(readReg(REGS, RS2) &Word W(XLEN -Int 1))) + + rule SRA RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) >>aWord Word2UInt(readReg(REGS, RS2) &Word W(XLEN -Int 1))) +``` +`JAL` stores `PC + 4` in `RD`, then increments `PC` by `OFFSET`. +```k + rule JAL RD, OFFSET => .K ... + REGS => writeReg(REGS, RD, PC +Word W(4)) + PC => PC +Word chop(OFFSET) +``` +`JALR` stores `PC + 4` in `RD`, increments `PC` by the value in register `RS1` plus `OFFSET`, then sets the least-significant bit of this new `PC` to `0`. +```k + rule JALR RD, OFFSET ( RS1 ) => .K ... + REGS => writeReg(REGS, RD, PC +Word W(4)) + PC => (PC +Word (readReg(REGS, RS1) +Word chop(OFFSET))) &Word chop(-1 < +``` +`BEQ` increments `PC` by `OFFSET` so long as the values in registers `RS1` and `RS2` are equal. Otherwise, `PC` is incremented by `4`. +```k + syntax Word ::= branchPC(oldPC: Word, offset: Int, branchCond: Bool) [function, total] + rule branchPC(PC, OFFSET, COND) => PC +Word chop(OFFSET) requires COND + rule branchPC(PC, _OFFSET, COND) => PC +Word W(4) requires notBool COND + + rule BEQ RS1 , RS2 , OFFSET => .K ... + REGS + PC => branchPC(PC, OFFSET, readReg(REGS, RS1) ==Word readReg(REGS, RS2)) +``` +The remaining branch instructions proceed analogously, but performing different comparisons between `RS1` and `RS2`. +```k + rule BNE RS1 , RS2 , OFFSET => .K ... + REGS + PC => branchPC(PC, OFFSET, readReg(REGS, RS1) =/=Word readReg(REGS, RS2)) + + rule BLT RS1 , RS2 , OFFSET => .K ... + REGS + PC => branchPC(PC, OFFSET, readReg(REGS, RS1) + + rule BGE RS1 , RS2 , OFFSET => .K ... + REGS + PC => branchPC(PC, OFFSET, readReg(REGS, RS1) >=sWord readReg(REGS, RS2)) + + rule BLTU RS1 , RS2 , OFFSET => .K ... + REGS + PC => branchPC(PC, OFFSET, readReg(REGS, RS1) + + rule BGEU RS1 , RS2 , OFFSET => .K ... + REGS + PC => branchPC(PC, OFFSET, readReg(REGS, RS1) >=uWord readReg(REGS, RS2)) +``` +`LB`, `LH`, and `LW` load `1`, `2`, and `4` bytes respectively from the memory address which is `OFFSET` greater than the value in register `RS1`, then sign extends the loaded bytes and places them in register `RD`. +```k + rule LB RD , OFFSET ( RS1 ) => .K ... + REGS => writeReg(REGS, RD, signExtend(loadByte(MEM, readReg(REGS, RS1) +Word chop(OFFSET)), 8)) + MEM + + rule LH RD , OFFSET ( RS1 ) => .K ... + REGS => writeReg(REGS, RD, signExtend(loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 2), 16)) + MEM + + rule LW RD , OFFSET ( RS1 ) => .K ... + REGS => writeReg(REGS, RD, signExtend(loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 4), 32)) + MEM +``` +`LBU` and `LHU` are analogous to `LB` and `LH`, but zero-extending rather than sign-extending. +```k + rule LBU RD , OFFSET ( RS1 ) => .K ... + REGS => writeReg(REGS, RD, W(loadByte(MEM, readReg(REGS, RS1) +Word chop(OFFSET)))) + MEM + + rule LHU RD , OFFSET ( RS1 ) => .K ... + REGS => writeReg(REGS, RD, W(loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 2))) + MEM +``` +Dually, `SB`, `SH`, and `SW` store the least-significant `1`, `2`, and `4` bytes respectively from `RS2` to the memory address which is `OFFSET` greater than the value in register `RS1`. +```k + rule SB RS2 , OFFSET ( RS1 ) => .K ... + REGS + MEM => storeByte(MEM, readReg(REGS, RS1) +Word chop(OFFSET), Word2UInt(readReg(REGS, RS2)) &Int 255) + + rule SH RS2 , OFFSET ( RS1 ) => .K ... + REGS + MEM => storeBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), Word2UInt(readReg(REGS, RS2)) &Int 65535, 2) + + rule SW RS2 , OFFSET ( RS1 ) => .K ... + REGS + MEM => storeBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), Word2UInt(readReg(REGS, RS2)) &Int 4294967295, 4) +``` +We presume a single hart with exclusive access to memory, so `FENCE` and `FENCE.TSO` are no-ops. +```k + rule FENCE _PRED, _SUCC => .K ... + + rule FENCE.TSO => .K ... +``` +As we do not model the external execution environment, we leave the `ECALL` and `EBREAK` instructions unevaluated. +```k endmodule ``` diff --git a/src/kriscv/kdist/riscv-semantics/word.md b/src/kriscv/kdist/riscv-semantics/word.md index 21e92345..df562126 100644 --- a/src/kriscv/kdist/riscv-semantics/word.md +++ b/src/kriscv/kdist/riscv-semantics/word.md @@ -89,14 +89,21 @@ is used to zero-out all but the least-significant `XLEN`-bits in case of overflo syntax Word ::= Word "< chop(I1 <>Int` for `Int` to implement the logical right shift operator `>>lWord` for `Word`. Indeed, note the following: +- `Int` values are infinitely sign-extended two's complement integers. +- `>>Int` arithmetically shifts by padding with the infinitely repeated sign bit. +- For an `I:Int` underlying `W(I):Word`, only the least-significant `XLEN`-bits of `I` are populated, so the infinitely repeated sign bit is always `0`. + +That is, for any `I:Int` underlying some `W(I):Word`, applying `>>Int` will always pad with `0`s, correctly implementing a logical right shift. ```k - syntax Word ::= Word ">>aWord" Int [function] - rule W(I1) >>aWord I2 => W(I1 >>Int I2) + syntax Word ::= Word ">>lWord" Int [function] + rule W(I1) >>lWord I2 => W(I1 >>Int I2) ``` -Because K does not provide a logical right shift for `Int`, we implement it as an arithmetic shift followed by zeroing-out all the sign bits. +To actually perform an arithmetic shift over `Word`, we first convert to an infinitely sign-extended `Int` of equal value using `Word2SInt`, ensuring `>>Int` will pad with `1`s for a negative `Word`. The final result will still be infinitely sign-extended, so we must `chop` it back to a `Word`. ```k - syntax Word ::= Word ">>lWord" Int [function] - rule W(I1) >>lWord I2 => W((I1 >>Int I2) &Int (2 ^Int (XLEN -Int I2) -Int 1)) + syntax Word ::= Word ">>aWord" Int [function] + rule W1 >>aWord I2 => chop(Word2SInt(W1) >>Int I2) endmodule ``` diff --git a/src/kriscv/term_manip.py b/src/kriscv/term_manip.py new file mode 100644 index 00000000..7e2dbbb7 --- /dev/null +++ b/src/kriscv/term_manip.py @@ -0,0 +1,36 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +from pyk.kore.match import kore_int, match_app, match_symbol +from pyk.kore.syntax import App + +if TYPE_CHECKING: + from pyk.kore.syntax import Pattern + + +def kore_word(word: Pattern) -> int: + return kore_int(match_app(word, 'LblW').args[0]) + + +def strip_inj(pattern: Pattern) -> Pattern: + if isinstance(pattern, App) and pattern.symbol == 'inj': + return pattern.args[0] + return pattern + + +def match_map(pattern: Pattern) -> tuple[tuple[Pattern, Pattern], ...]: + # Same as match_map from pyk.kore.match, but not using LeftAssoc and stripping injections + stop_symbol = "Lbl'Stop'Map" + cons_symbol = "Lbl'Unds'Map'Unds'" + item_symbol = "Lbl'UndsPipe'-'-GT-Unds'" + + app = match_app(pattern) + if app.symbol == stop_symbol: + return () + + if app.symbol == item_symbol: + return ((strip_inj(app.args[0]), strip_inj(app.args[1])),) + + match_symbol(app.symbol, cons_symbol) + return match_map(app.args[0]) + match_map(app.args[1]) diff --git a/src/kriscv/tools.py b/src/kriscv/tools.py index b6f7f2b4..f250cd9e 100644 --- a/src/kriscv/tools.py +++ b/src/kriscv/tools.py @@ -3,11 +3,14 @@ from typing import TYPE_CHECKING from elftools.elf.elffile import ELFFile # type: ignore -from pyk.kast.inner import Subst +from pyk.kast.inner import KSort, Subst +from pyk.kast.manip import split_config_from +from pyk.kore.match import kore_int from pyk.ktool.krun import KRun from pyk.prelude.k import GENERATED_TOP_CELL from kriscv import elf_parser, term_builder +from kriscv.term_manip import kore_word, match_map if TYPE_CHECKING: from pathlib import Path @@ -47,7 +50,7 @@ def init_config(self, config_vars: dict[str, KInner]) -> KInner: def run_config(self, config: KInner) -> KInner: config_kore = self.krun.kast_to_kore(config, sort=GENERATED_TOP_CELL) - final_config_kore = self.krun.run_pattern(config_kore) + final_config_kore = self.krun.run_pattern(config_kore, check=True) return self.krun.kore_to_kast(final_config_kore) def run_elf(self, elf_file: Path, *, end_symbol: str | None = None) -> KInner: @@ -70,3 +73,21 @@ def run_elf(self, elf_file: Path, *, end_symbol: str | None = None) -> KInner: '$HALT': halt_cond, } return self.run_config(self.init_config(config_vars)) + + def get_registers(self, config: KInner) -> dict[int, int]: + _, cells = split_config_from(config) + regs_kore = self.krun.kast_to_kore(cells['REGS_CELL'], sort=KSort('Map')) + regs = {} + for reg, val in match_map(regs_kore): + regs[kore_int(reg)] = kore_word(val) + if 0 not in regs: + regs[0] = 0 + return regs + + def get_memory(self, config: KInner) -> dict[int, int]: + _, cells = split_config_from(config) + mem_kore = self.krun.kast_to_kore(cells['MEM_CELL'], sort=KSort('Map')) + mem = {} + for addr, val in match_map(mem_kore): + mem[kore_word(addr)] = kore_int(val) + return mem diff --git a/src/tests/conftest.py b/src/tests/conftest.py index 8b031bdc..74994c3e 100644 --- a/src/tests/conftest.py +++ b/src/tests/conftest.py @@ -14,10 +14,10 @@ def pytest_addoption(parser: Parser) -> None: parser.addoption( - '--update-expected-output', + '--save-final-config', action='store_true', default=False, - help='Write expected output files for simple tests', + help='Save the final configuration for each simple test', ) parser.addoption( '--temp-dir', @@ -27,8 +27,8 @@ def pytest_addoption(parser: Parser) -> None: @pytest.fixture -def update_expected_output(request: FixtureRequest) -> bool: - return request.config.getoption('--update-expected-output') +def save_final_config(request: FixtureRequest) -> bool: + return request.config.getoption('--save-final-config') @pytest.fixture diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py index 34cc58d3..54ee72e5 100644 --- a/src/tests/integration/test_integration.py +++ b/src/tests/integration/test_integration.py @@ -5,7 +5,10 @@ from typing import TYPE_CHECKING import pytest +import yaml +from elftools.elf.elffile import ELFFile # type: ignore +from kriscv import elf_parser from kriscv.build import semantics from ..utils import TESTS_DIR @@ -18,18 +21,108 @@ SIMPLE_TESTS: Final = tuple(asm_file for asm_file in SIMPLE_DIR.rglob('*.S')) -def _test_simple(elf_file: Path, expected_file: Path, update: bool) -> None: +def _as_unsigned(val: int, bits: int) -> int | None: + if 0 <= val and val < 2**bits: + return val + if -(2 ** (bits - 1)) <= val and val < 0: + return val + 2**bits + return None + + +def _check_regs_entry(assert_file: Path, registers: dict[int, int], reg: int, val: int) -> None: + if not (0 <= reg and reg < 16): + raise AssertionError( + f"{assert_file}: Invalid register {reg} found in 'regs'. Registers must be in the range [0, 15]." + ) + expect = _as_unsigned(val, 32) + if expect is None: + val_str = f'{val} (0x{val:08X})' if val >= 0 else f'{val}' + raise AssertionError( + f'{assert_file}: expected value {val_str} for x{reg} is not a 32-bit integer. Value must be in the range [-2147483648, 2147483647] or [0, 4294967295] ([0, 0xFFFFFFFF]).' + ) + err_msg = f'Expected x{reg} to contain {val} (0x{expect:08X}), but ' + if reg not in registers: + raise AssertionError(err_msg + f'x{reg} was never written to.') + actual = registers[reg] + if actual != expect: + raise AssertionError(err_msg + f'found {actual} (0x{actual:08X}).') + + +def _check_mem_entry(assert_file: Path, mem_symbol: int, memory: dict[int, int], offset: int, val: int) -> None: + addr = mem_symbol + offset + mem_str = f'{mem_symbol} (0x{mem_symbol:08X})' + offset_str = f'{offset} (0x{offset:08X})' + addr_str = f'{addr} (0x{addr:08X})' + if not (0 <= addr and addr < 2**32): + raise AssertionError( + f"{assert_file}: Invalid memory offset {offset_str} found in 'mem'. Symbol '_mem' is at address {mem_str}, so the absolute address {addr_str} corresponding to this offset is outside the allowed range [0, 4294967295] ([0, 0xFFFFFFFF])." + ) + expect = _as_unsigned(val, 8) + if expect is None: + val_str = f'{val} (0x{val:02X})' if val >= 0 else f'{val}' + raise AssertionError( + f'{assert_file}: expected value {val_str} for memory offset {offset_str} is not an 8-bit integer. Value must be in the range [-128, 127] or [0, 255] ([0, 0xFF]).' + ) + err_msg = ( + f'Expected memory offset {offset_str} to contain {val} (0x{expect:02X}), but ' + + '{reason}' + + f". Symbol '_mem' is at address {mem_str}, so this offset corresponds to absolute address {addr_str}." + ) + if addr not in memory: + raise AssertionError(err_msg.format(reason='this location was never written to')) + actual = memory[addr] + if actual != expect: + raise AssertionError(err_msg.format(reason=f'found {actual} (0x{actual:02X})')) + + +def _test_simple(elf_file: Path, assert_file: Path, final_config_output: Path | None) -> None: tools = semantics() - actual = tools.kprint.pretty_print(tools.run_elf(elf_file, end_symbol='_halt'), sort_collections=True) + final_config = tools.run_elf(elf_file, end_symbol='_halt') + + if final_config_output is not None: + final_config_output.touch() + pretty_config = tools.kprint.pretty_print(final_config, sort_collections=True) + final_config_output.write_text(pretty_config) - if update: - expected_file.touch() - expected_file.write_text(actual) + registers = tools.get_registers(final_config) + memory = tools.get_memory(final_config) + + assert_file = assert_file.resolve(strict=True) + asserts = yaml.safe_load(assert_file.read_bytes()) + + if asserts is None: + return + if not (set(asserts.keys()) <= {'regs', 'mem'}): + raise AssertionError(f"{assert_file}: Unexpected keys {asserts.keys()}. Expected only 'regs' or 'mem'.") + + for reg, val in asserts.get('regs', {}).items(): + if not isinstance(reg, int): + raise AssertionError(f"{assert_file}: Unexpected key {reg} in 'regs'. Expected an integer register number.") + if not isinstance(val, int): + raise AssertionError(f"{assert_file}: Unexpected value {val} in 'regs'. Expected a 32-bit integer.") + _check_regs_entry(assert_file, registers, reg, val) + + if 'mem' not in asserts: return - expected_file = expected_file.resolve(strict=True) - expected = expected_file.read_text() - assert actual == expected + with open(elf_file, 'rb') as f: + mem_symbol_vals = elf_parser.read_symbol(ELFFile(f), '_mem') + + if len(mem_symbol_vals) == 0: + raise AssertionError( + f"{assert_file}: Found 'mem' assertion entry, but test file does not contain '_mem' symbol." + ) + if len(mem_symbol_vals) > 1: + raise AssertionError( + f"{assert_file}: Found 'mem' assertion entry, but test file contains multiple instances of '_mem' symbol." + ) + mem_symbol = mem_symbol_vals[0] + for addr, val in asserts.get('mem', {}).items(): + if not isinstance(addr, int): + raise AssertionError(f"{assert_file}: Unexpected key {reg} in 'mem'. Expected an integer address.") + if not isinstance(val, int): + raise AssertionError(f"{assert_file}: Unexpected value {val} in 'mem'. Expected an 8-bit integer.") + _check_mem_entry(assert_file, mem_symbol, memory, addr, val) @pytest.mark.parametrize( @@ -37,7 +130,7 @@ def _test_simple(elf_file: Path, expected_file: Path, update: bool) -> None: SIMPLE_TESTS, ids=[str(test.relative_to(SIMPLE_DIR)) for test in SIMPLE_TESTS], ) -def test_simple(asm_file: Path, update_expected_output: bool, temp_dir: Path) -> None: +def test_simple(asm_file: Path, save_final_config: bool, temp_dir: Path) -> None: elf_file = Path(temp_dir) / (asm_file.stem + '.elf') compile_cmd = [ 'riscv64-unknown-elf-gcc', @@ -50,11 +143,13 @@ def test_simple(asm_file: Path, update_expected_output: bool, temp_dir: Path) -> '-mlittle-endian', '-Xassembler', '-mno-arch-attr', + f'-I {SIMPLE_DIR}', str(asm_file), '-o', str(elf_file), ] subprocess.run(compile_cmd, check=True) assert elf_file.exists() - expected_file = Path(str(asm_file) + '.out') - _test_simple(elf_file, expected_file, update_expected_output) + assert_file = Path(str(asm_file) + '.assert') + final_config_output = (Path(temp_dir) / (asm_file.name + '.out')) if save_final_config else None + _test_simple(elf_file, assert_file, final_config_output) diff --git a/tests/README.md b/tests/README.md index 5045e84a..b52a1df1 100644 --- a/tests/README.md +++ b/tests/README.md @@ -6,10 +6,10 @@ This directory contains the input RISC-V files for various tests. ### failing.txt A list of tests that are known to fail under the current implementation. Each line consists of a single path to a failing test file. Paths are given relative to the `riscv-semantics/tests` directory. -### riscv-arch-test / riscv-arch-test-compiled -The official RISC-V Architectural Test Suite. These are exercised in `src/tests/integration/test_conformance.py` as part of `make test_integration`. +### riscv-arch-test(-compiled) +The official RISC-V Architectural Test Suite. These are exercised in `src/tests/integration/test_conformance.py` as part of `make test-integration`. -The test source files can be found under `riscv-arch-test/riscv-test-suite` and compiled by calling `make tests/riscv-arch-test-compiled` from the repository root. This will populate the `riscv-arch-test-compiled` directory with the following contents: +The test source files can be found under `riscv-arch-test/riscv-test-suite` and are compiled by calling `make tests/riscv-arch-test-compiled` from the repository root. This will populate the `riscv-arch-test-compiled` directory with the following contents: - `database.yaml` - A database of all tests in the suite with associated information pulled from `RVTEST` macros - `test_list.yaml` @@ -24,12 +24,26 @@ The test source files can be found under `riscv-arch-test/riscv-test-suite` and - The actual compiled test files for input to `kriscv` - The directory structure mirrors `riscv-arch-test/riscv-test-suite`, but with each `.S` test file replaced by a directory of the same name containing: - `.s`, the pre-linking RISC-V ASM - - `.elf`, the fully compiled object file - - `.disass`, the disassembly of the compiled object file + - `.elf`, the fully compiled object file + - `.disass`, the disassembly of the compiled object file ### simple -A suite of handwritten RISC-V tests. Inputs are RISC-V ASM files `test.S` which are compiled to ELF with +A suite of handwritten RISC-V tests. These are exercised in `src/tests/integration/test_integration.py` as part of `make test-simple` or `make test-integration`. + +Each test consists of an input RISC-V ASM file `test.S` and a corresponding assertion file `test.S.assert`. + +The input is compiled with ``` riscv64-unknown-elf-gcc -nostdlib -nostartfiles -static -march=rv32e -mabi=ilp32e -mno-relax -mlittle-endian -Xassembler -mno-arch-attr test.S ``` -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`. +and must define global symbols `_start` and `_halt`. See the convenience macros defined in `simple.h`. + +The assertion file must be in YAML format and may contain the following entries: +- `regs`, a dictionary of entries `i: val` asserting that register `xi` has value `val` + - `i` must be in the range `[0, 15]` + - `val` must be a 32-bit integer, either signed or unsigned +- `mem`, a dictionary of entries `offset: val` asserting that memory address `_mem + offset` has value `val` + - `offset` must be an unsigned integer + - `val` must be an 8-bit integer, either signed or unsigned + +The test is executed with the PC initially set to `_start` and will halt when the PC reaches `_halt`. The final configuration is then checked against each of entries in the assertion file. diff --git a/tests/simple/add.S b/tests/simple/add.S new file mode 100644 index 00000000..de48fc56 --- /dev/null +++ b/tests/simple/add.S @@ -0,0 +1,14 @@ +#include "simple.h" + +START_TEXT + li x1, 0xDEADBEEF // x1 = 0xDEADBEEF + add x2, x1, x0 // x2 = 0xDEADBEEF + + xori x3, x1, -1 // x3 = ~x2 + addi x3, x3, 1 // x3 = ~x2 + 1 = -x2 + li x4, 0xFFFFFFFF // x4 = 0xFFFFFFFF + add x4, x4, x3 // x4 = 0xFFFFFFFF - x2 + addi x4, x4, 1 // x4 = (0xFFFFFFFF - x2) + 1 + + add x5, x2, x4 // x5 = 0xFFFFFFFF + 1 = 0 +END_TEXT diff --git a/tests/simple/add.S.assert b/tests/simple/add.S.assert new file mode 100644 index 00000000..43dc8e3a --- /dev/null +++ b/tests/simple/add.S.assert @@ -0,0 +1 @@ +regs: {2: 0xDEADBEEF, 5: 0} \ No newline at end of file diff --git a/tests/simple/addi-overflow.S b/tests/simple/addi-overflow.S deleted file mode 100644 index 74abb204..00000000 --- a/tests/simple/addi-overflow.S +++ /dev/null @@ -1,13 +0,0 @@ -.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 deleted file mode 100644 index 7a0545fd..00000000 --- a/tests/simple/addi-overflow.S.out +++ /dev/null @@ -1,27 +0,0 @@ - - - - .K - - - 1 |-> W ( 2147483647 ) 2 |-> W ( 2147483648 ) - - - W ( 65640 ) - - - W ( 65536 ) |-> 127 W ( 65537 ) |-> 69 W ( 65538 ) |-> 76 W ( 65539 ) |-> 70 W ( 65540 ) |-> 1 W ( 65541 ) |-> 1 W ( 65542 ) |-> 1 W ( 65543 ) |-> 0 W ( 65544 ) |-> 0 W ( 65545 ) |-> 0 W ( 65546 ) |-> 0 W ( 65547 ) |-> 0 W ( 65548 ) |-> 0 W ( 65549 ) |-> 0 W ( 65550 ) |-> 0 W ( 65551 ) |-> 0 W ( 65552 ) |-> 2 W ( 65553 ) |-> 0 W ( 65554 ) |-> 243 W ( 65555 ) |-> 0 W ( 65556 ) |-> 1 W ( 65557 ) |-> 0 W ( 65558 ) |-> 0 W ( 65559 ) |-> 0 W ( 65560 ) |-> 84 W ( 65561 ) |-> 0 W ( 65562 ) |-> 1 W ( 65563 ) |-> 0 W ( 65564 ) |-> 52 W ( 65565 ) |-> 0 W ( 65566 ) |-> 0 W ( 65567 ) |-> 0 W ( 65568 ) |-> 208 W ( 65569 ) |-> 1 W ( 65570 ) |-> 0 W ( 65571 ) |-> 0 W ( 65572 ) |-> 8 W ( 65573 ) |-> 0 W ( 65574 ) |-> 0 W ( 65575 ) |-> 0 W ( 65576 ) |-> 52 W ( 65577 ) |-> 0 W ( 65578 ) |-> 32 W ( 65579 ) |-> 0 W ( 65580 ) |-> 1 W ( 65581 ) |-> 0 W ( 65582 ) |-> 40 W ( 65583 ) |-> 0 W ( 65584 ) |-> 5 W ( 65585 ) |-> 0 W ( 65586 ) |-> 4 W ( 65587 ) |-> 0 W ( 65588 ) |-> 1 W ( 65589 ) |-> 0 W ( 65590 ) |-> 0 W ( 65591 ) |-> 0 W ( 65592 ) |-> 0 W ( 65593 ) |-> 0 W ( 65594 ) |-> 0 W ( 65595 ) |-> 0 W ( 65596 ) |-> 0 W ( 65597 ) |-> 0 W ( 65598 ) |-> 1 W ( 65599 ) |-> 0 W ( 65600 ) |-> 0 W ( 65601 ) |-> 0 W ( 65602 ) |-> 1 W ( 65603 ) |-> 0 W ( 65604 ) |-> 108 W ( 65605 ) |-> 0 W ( 65606 ) |-> 0 W ( 65607 ) |-> 0 W ( 65608 ) |-> 108 W ( 65609 ) |-> 0 W ( 65610 ) |-> 0 W ( 65611 ) |-> 0 W ( 65612 ) |-> 5 W ( 65613 ) |-> 0 W ( 65614 ) |-> 0 W ( 65615 ) |-> 0 W ( 65616 ) |-> 0 W ( 65617 ) |-> 16 W ( 65618 ) |-> 0 W ( 65619 ) |-> 0 W ( 65620 ) |-> 183 W ( 65621 ) |-> 240 W ( 65622 ) |-> 255 W ( 65623 ) |-> 127 W ( 65624 ) |-> 147 W ( 65625 ) |-> 128 W ( 65626 ) |-> 240 W ( 65627 ) |-> 127 W ( 65628 ) |-> 147 W ( 65629 ) |-> 128 W ( 65630 ) |-> 240 W ( 65631 ) |-> 127 W ( 65632 ) |-> 147 W ( 65633 ) |-> 128 W ( 65634 ) |-> 16 W ( 65635 ) |-> 0 W ( 65636 ) |-> 19 W ( 65637 ) |-> 129 W ( 65638 ) |-> 16 W ( 65639 ) |-> 0 W ( 65640 ) |-> 19 W ( 65641 ) |-> 0 W ( 65642 ) |-> 0 W ( 65643 ) |-> 0 - - - - - ADDRESS ( W ( 65640 ) ) - - - true - - - - 0 - - \ No newline at end of file diff --git a/tests/simple/addi.S b/tests/simple/addi.S index 15fa0f0f..13d32307 100644 --- a/tests/simple/addi.S +++ b/tests/simple/addi.S @@ -1,9 +1,15 @@ -.text -.globl _start -_start: - addi x1, x0, 8 - addi x1, x1, 8 - addi x2, x1, 0 -.globl _halt -_halt: - nop +#include "simple.h" + +START_TEXT + addi x1, x0, 8 // x1 = 8 + addi x1, x1, 8 // x1 = 16 + addi x2, x1, 0 // x2 = 16 + + lui x3, 0x7FFFF + addi x3, x3, 2047 + addi x3, x3, 2047 + addi x3, x3, 1 + // x3 contains 2^31 - 1, the largest 32-bit two's complement integer. + // Setting x2 = x1 + 1 should overflow + addi x4, x3, 1 +END_TEXT diff --git a/tests/simple/addi.S.assert b/tests/simple/addi.S.assert new file mode 100644 index 00000000..debb7e2e --- /dev/null +++ b/tests/simple/addi.S.assert @@ -0,0 +1 @@ +regs: {1: 16, 2: 16, 3: 2147483647, 4: -2147483648} diff --git a/tests/simple/addi.S.out b/tests/simple/addi.S.out deleted file mode 100644 index 250f5b29..00000000 --- a/tests/simple/addi.S.out +++ /dev/null @@ -1,27 +0,0 @@ - - - - .K - - - 1 |-> W ( 16 ) 2 |-> W ( 16 ) - - - W ( 65632 ) - - - W ( 65536 ) |-> 127 W ( 65537 ) |-> 69 W ( 65538 ) |-> 76 W ( 65539 ) |-> 70 W ( 65540 ) |-> 1 W ( 65541 ) |-> 1 W ( 65542 ) |-> 1 W ( 65543 ) |-> 0 W ( 65544 ) |-> 0 W ( 65545 ) |-> 0 W ( 65546 ) |-> 0 W ( 65547 ) |-> 0 W ( 65548 ) |-> 0 W ( 65549 ) |-> 0 W ( 65550 ) |-> 0 W ( 65551 ) |-> 0 W ( 65552 ) |-> 2 W ( 65553 ) |-> 0 W ( 65554 ) |-> 243 W ( 65555 ) |-> 0 W ( 65556 ) |-> 1 W ( 65557 ) |-> 0 W ( 65558 ) |-> 0 W ( 65559 ) |-> 0 W ( 65560 ) |-> 84 W ( 65561 ) |-> 0 W ( 65562 ) |-> 1 W ( 65563 ) |-> 0 W ( 65564 ) |-> 52 W ( 65565 ) |-> 0 W ( 65566 ) |-> 0 W ( 65567 ) |-> 0 W ( 65568 ) |-> 200 W ( 65569 ) |-> 1 W ( 65570 ) |-> 0 W ( 65571 ) |-> 0 W ( 65572 ) |-> 8 W ( 65573 ) |-> 0 W ( 65574 ) |-> 0 W ( 65575 ) |-> 0 W ( 65576 ) |-> 52 W ( 65577 ) |-> 0 W ( 65578 ) |-> 32 W ( 65579 ) |-> 0 W ( 65580 ) |-> 1 W ( 65581 ) |-> 0 W ( 65582 ) |-> 40 W ( 65583 ) |-> 0 W ( 65584 ) |-> 5 W ( 65585 ) |-> 0 W ( 65586 ) |-> 4 W ( 65587 ) |-> 0 W ( 65588 ) |-> 1 W ( 65589 ) |-> 0 W ( 65590 ) |-> 0 W ( 65591 ) |-> 0 W ( 65592 ) |-> 0 W ( 65593 ) |-> 0 W ( 65594 ) |-> 0 W ( 65595 ) |-> 0 W ( 65596 ) |-> 0 W ( 65597 ) |-> 0 W ( 65598 ) |-> 1 W ( 65599 ) |-> 0 W ( 65600 ) |-> 0 W ( 65601 ) |-> 0 W ( 65602 ) |-> 1 W ( 65603 ) |-> 0 W ( 65604 ) |-> 100 W ( 65605 ) |-> 0 W ( 65606 ) |-> 0 W ( 65607 ) |-> 0 W ( 65608 ) |-> 100 W ( 65609 ) |-> 0 W ( 65610 ) |-> 0 W ( 65611 ) |-> 0 W ( 65612 ) |-> 5 W ( 65613 ) |-> 0 W ( 65614 ) |-> 0 W ( 65615 ) |-> 0 W ( 65616 ) |-> 0 W ( 65617 ) |-> 16 W ( 65618 ) |-> 0 W ( 65619 ) |-> 0 W ( 65620 ) |-> 147 W ( 65621 ) |-> 0 W ( 65622 ) |-> 128 W ( 65623 ) |-> 0 W ( 65624 ) |-> 147 W ( 65625 ) |-> 128 W ( 65626 ) |-> 128 W ( 65627 ) |-> 0 W ( 65628 ) |-> 19 W ( 65629 ) |-> 129 W ( 65630 ) |-> 0 W ( 65631 ) |-> 0 W ( 65632 ) |-> 19 W ( 65633 ) |-> 0 W ( 65634 ) |-> 0 W ( 65635 ) |-> 0 - - - - - ADDRESS ( W ( 65632 ) ) - - - true - - - - 0 - - \ No newline at end of file diff --git a/tests/simple/and.S b/tests/simple/and.S new file mode 100644 index 00000000..ed1f323e --- /dev/null +++ b/tests/simple/and.S @@ -0,0 +1,15 @@ +#include "simple.h" + +START_TEXT + // Same as andi.S, but put immediates in registers + addi x15, x0, 21 + addi x14, x0, 0 + addi x13, x0, -10 + + li x1, 0xFFFFFFFF + and x2, x1, x15 // x2 = 21 + and x3, x1, x14 // x3 = 0 + + li x4, -11 // x4 = -11 + and x5, x4, x13 // x4 = -10 +END_TEXT diff --git a/tests/simple/and.S.assert b/tests/simple/and.S.assert new file mode 100644 index 00000000..dfc9c369 --- /dev/null +++ b/tests/simple/and.S.assert @@ -0,0 +1,2 @@ +regs: {1: 0xFFFFFFFF, 2: 21, 3: 0, 4: -11, 5: -12} + diff --git a/tests/simple/andi.S b/tests/simple/andi.S new file mode 100644 index 00000000..7ea3eb6f --- /dev/null +++ b/tests/simple/andi.S @@ -0,0 +1,10 @@ +#include "simple.h" + +START_TEXT + li x1, 0xFFFFFFFF + andi x2, x1, 21 // x2 = 21 + andi x3, x1, 0 // x3 = 0 + + li x4, -11 // x4 = -11 + andi x5, x4, -10 // x4 = -10 +END_TEXT diff --git a/tests/simple/andi.S.assert b/tests/simple/andi.S.assert new file mode 100644 index 00000000..dfc9c369 --- /dev/null +++ b/tests/simple/andi.S.assert @@ -0,0 +1,2 @@ +regs: {1: 0xFFFFFFFF, 2: 21, 3: 0, 4: -11, 5: -12} + diff --git a/tests/simple/auipc.S b/tests/simple/auipc.S new file mode 100644 index 00000000..910ec4db --- /dev/null +++ b/tests/simple/auipc.S @@ -0,0 +1,16 @@ +#include "simple.h" + +START_TEXT + auipc x0, 0x10 + + auipc x1, 0 // x1 = PC of this line + auipc x2, 0 // x2 = x1 + 4 + addi x0, x0, 0 + auipc x3, 0x80000 // x3 = x1 + 12 + 0x80000000 = x1 + 0x8000000C + + xori x4, x1, -1 // x4 = ~x1 + addi x4, x4, 1 // x4 = ~x1 + 1 = -x1 + + add x2, x2, x4 // x2 = 4 + add x3, x3, x4 // x3 = 0x8000000C +END_TEXT diff --git a/tests/simple/auipc.S.assert b/tests/simple/auipc.S.assert new file mode 100644 index 00000000..01a00ef9 --- /dev/null +++ b/tests/simple/auipc.S.assert @@ -0,0 +1 @@ +regs: {2: 4, 3: 0x8000000C} diff --git a/tests/simple/beq.S b/tests/simple/beq.S new file mode 100644 index 00000000..a7072cbd --- /dev/null +++ b/tests/simple/beq.S @@ -0,0 +1,13 @@ +#include "simple.h" + +START_TEXT + addi x15, x0, 0 + beq x0, x0, .+8 + addi x15, x0, 1 + + addi x14, x0, 0 + addi x2, x0, 1 + beq x0, x2, .+8 + addi x14, x0, 1 + nop +END_TEXT diff --git a/tests/simple/beq.S.assert b/tests/simple/beq.S.assert new file mode 100644 index 00000000..20c54115 --- /dev/null +++ b/tests/simple/beq.S.assert @@ -0,0 +1 @@ +regs: {15: 0, 14: 1} diff --git a/tests/simple/bge.S b/tests/simple/bge.S new file mode 100644 index 00000000..5ed013ad --- /dev/null +++ b/tests/simple/bge.S @@ -0,0 +1,21 @@ +#include "simple.h" + +START_TEXT + addi x15, x0, 0 + bge x0, x0, .+8 + addi x15, x0, 1 + + addi x14, x0, 0 + addi x2, x0, 1 + bge x0, x2, .+8 + addi x14, x0, 1 + + addi x13, x0, 0 + addi x3, x0, -1 + bge x0, x3, .+8 + addi x13, x0, 1 + + addi x12, x0, 0 + bge x3, x0, .+8 + addi x12, x0, 1 +END_TEXT diff --git a/tests/simple/bge.S.assert b/tests/simple/bge.S.assert new file mode 100644 index 00000000..d85c5f32 --- /dev/null +++ b/tests/simple/bge.S.assert @@ -0,0 +1,2 @@ +regs: {15: 0, 14: 1, 13: 0, 12: 1} + diff --git a/tests/simple/bgeu.S b/tests/simple/bgeu.S new file mode 100644 index 00000000..d2d819e7 --- /dev/null +++ b/tests/simple/bgeu.S @@ -0,0 +1,21 @@ +#include "simple.h" + +START_TEXT + addi x15, x0, 0 + bgeu x0, x0, .+8 + addi x15, x0, 1 + + addi x14, x0, 0 + addi x2, x0, 1 + bgeu x0, x2, .+8 + addi x14, x0, 1 + + addi x13, x0, 0 + addi x3, x0, -1 + bgeu x0, x3, .+8 + addi x13, x0, 1 + + addi x12, x0, 0 + bgeu x3, x0, .+8 + addi x12, x0, 1 +END_TEXT diff --git a/tests/simple/bgeu.S.assert b/tests/simple/bgeu.S.assert new file mode 100644 index 00000000..ae6a2a0c --- /dev/null +++ b/tests/simple/bgeu.S.assert @@ -0,0 +1,2 @@ +regs: {15: 0, 14: 1, 13: 1, 12: 0} + diff --git a/tests/simple/blt.S b/tests/simple/blt.S new file mode 100644 index 00000000..58e140e5 --- /dev/null +++ b/tests/simple/blt.S @@ -0,0 +1,21 @@ +#include "simple.h" + +START_TEXT + addi x15, x0, 0 + blt x0, x0, .+8 + addi x15, x0, 1 + + addi x14, x0, 0 + addi x2, x0, 1 + blt x0, x2, .+8 + addi x14, x0, 1 + + addi x13, x0, 0 + addi x3, x0, -1 + blt x0, x3, .+8 + addi x13, x0, 1 + + addi x12, x0, 0 + blt x3, x0, .+8 + addi x12, x0, 1 +END_TEXT diff --git a/tests/simple/blt.S.assert b/tests/simple/blt.S.assert new file mode 100644 index 00000000..ddc961d6 --- /dev/null +++ b/tests/simple/blt.S.assert @@ -0,0 +1,2 @@ +regs: {15: 1, 14: 0, 13: 1, 12: 0} + diff --git a/tests/simple/bltu.S b/tests/simple/bltu.S new file mode 100644 index 00000000..5be01fbd --- /dev/null +++ b/tests/simple/bltu.S @@ -0,0 +1,21 @@ +#include "simple.h" + +START_TEXT + addi x15, x0, 0 + bltu x0, x0, .+8 + addi x15, x0, 1 + + addi x14, x0, 0 + addi x2, x0, 1 + bltu x0, x2, .+8 + addi x14, x0, 1 + + addi x13, x0, 0 + addi x3, x0, -1 + bltu x0, x3, .+8 + addi x13, x0, 1 + + addi x12, x0, 0 + bltu x3, x0, .+8 + addi x12, x0, 1 +END_TEXT diff --git a/tests/simple/bltu.S.assert b/tests/simple/bltu.S.assert new file mode 100644 index 00000000..cfbd57a9 --- /dev/null +++ b/tests/simple/bltu.S.assert @@ -0,0 +1,2 @@ +regs: {15: 1, 14: 0, 13: 0, 12: 1} + diff --git a/tests/simple/bne.S b/tests/simple/bne.S new file mode 100644 index 00000000..b931f8b1 --- /dev/null +++ b/tests/simple/bne.S @@ -0,0 +1,13 @@ +#include "simple.h" + +START_TEXT + addi x15, x0, 0 + bne x0, x0, .+8 + addi x15, x0, 1 + + addi x14, x0, 0 + addi x2, x0, 1 + bne x0, x2, .+8 + addi x14, x0, 1 + nop +END_TEXT diff --git a/tests/simple/bne.S.assert b/tests/simple/bne.S.assert new file mode 100644 index 00000000..13782cdf --- /dev/null +++ b/tests/simple/bne.S.assert @@ -0,0 +1 @@ +regs: {15: 1, 14: 0} diff --git a/tests/simple/jal.S b/tests/simple/jal.S new file mode 100644 index 00000000..b73a7c90 --- /dev/null +++ b/tests/simple/jal.S @@ -0,0 +1,19 @@ +#include "simple.h" + +START_TEXT + jal x1, .+4 // x1 = PC_4 + 4 + auipc x2, 0 // x2 = PC_5 = PC_4 + 4 = x1 + sub x3, x1, x2 // x3 = 0 + + addi x4, x0, 0 // x4 = 0 + jal x0, .+8 + addi x4, x4, 1 // should be skipped + nop // still x4 = 0 + + addi x5, x0, 0 // x5 = 0 + jal x0, .+12 // jump to line 18 + addi x5, x5, 1 // x5 += 1 + jal x0, .+8 // jump to line 19 + jal x0, .-8 // jump to line 16 + nop // now x5 = 1 +END_TEXT diff --git a/tests/simple/jal.S.assert b/tests/simple/jal.S.assert new file mode 100644 index 00000000..7b87dbaa --- /dev/null +++ b/tests/simple/jal.S.assert @@ -0,0 +1 @@ +regs: {3: 0, 4: 0, 5: 1} diff --git a/tests/simple/jalr.S b/tests/simple/jalr.S new file mode 100644 index 00000000..fd857d8d --- /dev/null +++ b/tests/simple/jalr.S @@ -0,0 +1,20 @@ +#include "simple.h" + +START_TEXT + addi x15, x0, 1 + jalr x1, x15, 3 // x1 = PC_4 + 4 + auipc x2, 0 // x2 = PC_5 = PC_4 + 4 = x1 + sub x3, x1, x2 // x3 = 0 + + addi x4, x0, 0 // x4 = 0 + jalr x0, x0, 9 + addi x4, x4, 1 // should be skipped + nop // still x4 = 0 + + addi x5, x0, 0 // x5 = 0 + jalr x0, x0, 12 // jump to line 18 + addi x5, x5, 1 // x5 += 1 + jalr x0, x0, 8 // jump to line 19 + jalr x0, x0, -7 // jump to line 16 + nop // now x5 = 1 +END_TEXT diff --git a/tests/simple/jalr.S.assert b/tests/simple/jalr.S.assert new file mode 100644 index 00000000..7b87dbaa --- /dev/null +++ b/tests/simple/jalr.S.assert @@ -0,0 +1 @@ +regs: {3: 0, 4: 0, 5: 1} diff --git a/tests/simple/load-store.S b/tests/simple/load-store.S new file mode 100644 index 00000000..5866ffa9 --- /dev/null +++ b/tests/simple/load-store.S @@ -0,0 +1,47 @@ +#include "simple.h" + +.data +test_data: + .byte 0x80 // -128 in signed, 128 in unsigned + .hword 0x8001 // -32767 in signed, 32769 in unsigned + .word 0x7FFFFFFF // 2147483647 + +START_TEXT + la x5, test_data + la x6, results + + lb x8, 0(x5) + sw x8, 0(x6) + + lh x9, 1(x5) + sw x9, 4(x6) + + lw x10, 3(x5) + sw x10, 8(x6) + + lbu x11, 0(x5) + sw x11, 12(x6) + + lhu x12, 1(x5) + sw x12, 16(x6) + + li x13, 0xFF + sb x13, 0(x5) + + li x14, 0xAAAA + sh x14, 1(x5) + + li x15, 0xBBBBCCCC + sw x15, 3(x5) +END_TEXT + +MEMORY +results: + .align 4 + .word 0x0 + .word 0x0 + .word 0x0 + .word 0x0 + .word 0x0 + .word 0x0 + diff --git a/tests/simple/load-store.S.assert b/tests/simple/load-store.S.assert new file mode 100644 index 00000000..af858de0 --- /dev/null +++ b/tests/simple/load-store.S.assert @@ -0,0 +1,7 @@ +mem: { 0: 0x80, 1: 0xFF, 2: 0xFF, 3: 0xFF, # -128 + 4: 0x01, 5: 0x80, 6: 0xFF, 7: 0xFF, # -32767 + 8: 0xFF, 9: 0xFF, 10: 0xFF, 11: 0x7F, # 2147483647 + 12: 0x80, 13: 0x00, 14: 0x00, 15: 0x00, # 128 + 16: 0x01, 17: 0x80, 18: 0x00, 19: 0x00 # 32769 + } + diff --git a/tests/simple/lui.S b/tests/simple/lui.S index a2ea8f23..71cf13da 100644 --- a/tests/simple/lui.S +++ b/tests/simple/lui.S @@ -1,9 +1,7 @@ -.text -.globl _start -_start: - lui x0, 0x10 - lui x1, 0x80000 - lui x2, 0x70000 -.globl _halt -_halt: - nop +#include "simple.h" + +START_TEXT + lui x0, 0x10 + lui x1, 0x80000 + lui x2, 0x70000 +END_TEXT diff --git a/tests/simple/lui.S.assert b/tests/simple/lui.S.assert new file mode 100644 index 00000000..63150fe6 --- /dev/null +++ b/tests/simple/lui.S.assert @@ -0,0 +1 @@ +regs: {0: 0x0, 1: 0x80000000, 2: 0x70000000} diff --git a/tests/simple/lui.S.out b/tests/simple/lui.S.out deleted file mode 100644 index d51fdd81..00000000 --- a/tests/simple/lui.S.out +++ /dev/null @@ -1,27 +0,0 @@ - - - - .K - - - 1 |-> W ( 2147483648 ) 2 |-> W ( 1879048192 ) - - - W ( 65632 ) - - - W ( 65536 ) |-> 127 W ( 65537 ) |-> 69 W ( 65538 ) |-> 76 W ( 65539 ) |-> 70 W ( 65540 ) |-> 1 W ( 65541 ) |-> 1 W ( 65542 ) |-> 1 W ( 65543 ) |-> 0 W ( 65544 ) |-> 0 W ( 65545 ) |-> 0 W ( 65546 ) |-> 0 W ( 65547 ) |-> 0 W ( 65548 ) |-> 0 W ( 65549 ) |-> 0 W ( 65550 ) |-> 0 W ( 65551 ) |-> 0 W ( 65552 ) |-> 2 W ( 65553 ) |-> 0 W ( 65554 ) |-> 243 W ( 65555 ) |-> 0 W ( 65556 ) |-> 1 W ( 65557 ) |-> 0 W ( 65558 ) |-> 0 W ( 65559 ) |-> 0 W ( 65560 ) |-> 84 W ( 65561 ) |-> 0 W ( 65562 ) |-> 1 W ( 65563 ) |-> 0 W ( 65564 ) |-> 52 W ( 65565 ) |-> 0 W ( 65566 ) |-> 0 W ( 65567 ) |-> 0 W ( 65568 ) |-> 200 W ( 65569 ) |-> 1 W ( 65570 ) |-> 0 W ( 65571 ) |-> 0 W ( 65572 ) |-> 8 W ( 65573 ) |-> 0 W ( 65574 ) |-> 0 W ( 65575 ) |-> 0 W ( 65576 ) |-> 52 W ( 65577 ) |-> 0 W ( 65578 ) |-> 32 W ( 65579 ) |-> 0 W ( 65580 ) |-> 1 W ( 65581 ) |-> 0 W ( 65582 ) |-> 40 W ( 65583 ) |-> 0 W ( 65584 ) |-> 5 W ( 65585 ) |-> 0 W ( 65586 ) |-> 4 W ( 65587 ) |-> 0 W ( 65588 ) |-> 1 W ( 65589 ) |-> 0 W ( 65590 ) |-> 0 W ( 65591 ) |-> 0 W ( 65592 ) |-> 0 W ( 65593 ) |-> 0 W ( 65594 ) |-> 0 W ( 65595 ) |-> 0 W ( 65596 ) |-> 0 W ( 65597 ) |-> 0 W ( 65598 ) |-> 1 W ( 65599 ) |-> 0 W ( 65600 ) |-> 0 W ( 65601 ) |-> 0 W ( 65602 ) |-> 1 W ( 65603 ) |-> 0 W ( 65604 ) |-> 100 W ( 65605 ) |-> 0 W ( 65606 ) |-> 0 W ( 65607 ) |-> 0 W ( 65608 ) |-> 100 W ( 65609 ) |-> 0 W ( 65610 ) |-> 0 W ( 65611 ) |-> 0 W ( 65612 ) |-> 5 W ( 65613 ) |-> 0 W ( 65614 ) |-> 0 W ( 65615 ) |-> 0 W ( 65616 ) |-> 0 W ( 65617 ) |-> 16 W ( 65618 ) |-> 0 W ( 65619 ) |-> 0 W ( 65620 ) |-> 55 W ( 65621 ) |-> 0 W ( 65622 ) |-> 1 W ( 65623 ) |-> 0 W ( 65624 ) |-> 183 W ( 65625 ) |-> 0 W ( 65626 ) |-> 0 W ( 65627 ) |-> 128 W ( 65628 ) |-> 55 W ( 65629 ) |-> 1 W ( 65630 ) |-> 0 W ( 65631 ) |-> 112 W ( 65632 ) |-> 19 W ( 65633 ) |-> 0 W ( 65634 ) |-> 0 W ( 65635 ) |-> 0 - - - - - ADDRESS ( W ( 65632 ) ) - - - true - - - - 0 - - \ No newline at end of file diff --git a/tests/simple/or.S b/tests/simple/or.S new file mode 100644 index 00000000..9b6f3c89 --- /dev/null +++ b/tests/simple/or.S @@ -0,0 +1,13 @@ +#include "simple.h" + +START_TEXT + // Same as ori.S, but put immediates in registers + addi x15, x0, 0 + addi x14, x0, -10 + + li x1, 0xFFFFFFFF + or x2, x1, x15 // x2 = 0xFFFFFFFF + + li x4, -11 // x4 = -11 + or x5, x4, x14 // x4 = -11 +END_TEXT diff --git a/tests/simple/or.S.assert b/tests/simple/or.S.assert new file mode 100644 index 00000000..f3c01448 --- /dev/null +++ b/tests/simple/or.S.assert @@ -0,0 +1 @@ +regs: {1: 0xFFFFFFFF, 2: 0xFFFFFFFF, 4: -11, 5: -9} diff --git a/tests/simple/ori.S b/tests/simple/ori.S new file mode 100644 index 00000000..10d08cc9 --- /dev/null +++ b/tests/simple/ori.S @@ -0,0 +1,9 @@ +#include "simple.h" + +START_TEXT + li x1, 0xFFFFFFFF + ori x2, x1, 0 // x2 = 0xFFFFFFFF + + li x4, -11 // x4 = -11 + ori x5, x4, -10 // x4 = -11 +END_TEXT diff --git a/tests/simple/ori.S.assert b/tests/simple/ori.S.assert new file mode 100644 index 00000000..f3c01448 --- /dev/null +++ b/tests/simple/ori.S.assert @@ -0,0 +1 @@ +regs: {1: 0xFFFFFFFF, 2: 0xFFFFFFFF, 4: -11, 5: -9} diff --git a/tests/simple/simple.h b/tests/simple/simple.h new file mode 100644 index 00000000..3efb5bb9 --- /dev/null +++ b/tests/simple/simple.h @@ -0,0 +1,19 @@ +#pragma once + +#define START_TEXT \ + .text; \ + .globl _start; \ + _start: + +#define END_TEXT \ + .globl _halt; \ + _halt: \ + nop; + +#define HALT \ + j _halt; + +#define MEMORY \ + .data; \ + .globl _mem; \ + _mem: diff --git a/tests/simple/sll.S b/tests/simple/sll.S new file mode 100644 index 00000000..d5c0513c --- /dev/null +++ b/tests/simple/sll.S @@ -0,0 +1,12 @@ +#include "simple.h" + +START_TEXT + li x15, 0xFFFFFFE0 // x15[4:0] = 0 + li x14, 0xFFFFFFE4 // x14[4:0] = 4 + li x13, 0xFFFFFFFF // x13[4:0] = 31 + + li x1, 0xDEADBEEF + sll x2, x1, x15 // x2 = 0xDEADBEEF + sll x3, x1, x14 // x3 = 0xEADBEEF0 + sll x4, x1, x13 // x4 = 0x80000000 +END_TEXT diff --git a/tests/simple/sll.S.assert b/tests/simple/sll.S.assert new file mode 100644 index 00000000..25f8f674 --- /dev/null +++ b/tests/simple/sll.S.assert @@ -0,0 +1 @@ +regs: {1: 0xDEADBEEF, 2: 0xDEADBEEF, 3: 0xEADBEEF0, 4: 0x80000000} diff --git a/tests/simple/slli.S b/tests/simple/slli.S new file mode 100644 index 00000000..c8f870f2 --- /dev/null +++ b/tests/simple/slli.S @@ -0,0 +1,8 @@ +#include "simple.h" + +START_TEXT + li x1, 0xDEADBEEF + slli x2, x1, 0 // x2 = 0xDEADBEEF + slli x3, x1, 4 // x3 = 0xEADBEEF0 + slli x4, x1, 31 // x4 = 0x80000000 +END_TEXT diff --git a/tests/simple/slli.S.assert b/tests/simple/slli.S.assert new file mode 100644 index 00000000..25f8f674 --- /dev/null +++ b/tests/simple/slli.S.assert @@ -0,0 +1 @@ +regs: {1: 0xDEADBEEF, 2: 0xDEADBEEF, 3: 0xEADBEEF0, 4: 0x80000000} diff --git a/tests/simple/slt.S b/tests/simple/slt.S new file mode 100644 index 00000000..81857843 --- /dev/null +++ b/tests/simple/slt.S @@ -0,0 +1,20 @@ +#include "simple.h" + +START_TEXT + // Same as slti.S, but put immediates in registers + addi x15, x0, 2 + addi x14, x0, 1 + addi x13, x0, -11 + + addi x1, x0, 1 // x1 = 1 + + slt x2, x1, x15 // x2 = 1 + slt x3, x1, x14 // x3 = 0 + + addi x4, x0, 1 // x4 = 1 + slt x4, x4, x14 // x4 = 0 + + addi x5, x0, -10 // x5 = -10 + slt x6, x5, x14 // x6 = 1 + slt x7, x5, x13 // x7 = 0 +END_TEXT diff --git a/tests/simple/slt.S.assert b/tests/simple/slt.S.assert new file mode 100644 index 00000000..3304d60c --- /dev/null +++ b/tests/simple/slt.S.assert @@ -0,0 +1 @@ +regs: {1: 1, 2: 1,3: 0, 4: 0, 5: -10, 6: 1, 7: 0} diff --git a/tests/simple/slti.S b/tests/simple/slti.S new file mode 100644 index 00000000..9f55cfd1 --- /dev/null +++ b/tests/simple/slti.S @@ -0,0 +1,14 @@ +#include "simple.h" + +START_TEXT + addi x1, x0, 1 // x1 = 1 + slti x2, x1, 2 // x2 = 1 + slti x3, x1, 1 // x3 = 0 + + addi x4, x0, 1 // x4 = 1 + slti x4, x4, 1 // x4 = 0 + + addi x5, x0, -10 // x5 = -10 + slti x6, x5, 1 // x6 = 1 + slti x7, x5, -11 // x7 = 0 +END_TEXT diff --git a/tests/simple/slti.S.assert b/tests/simple/slti.S.assert new file mode 100644 index 00000000..3304d60c --- /dev/null +++ b/tests/simple/slti.S.assert @@ -0,0 +1 @@ +regs: {1: 1, 2: 1,3: 0, 4: 0, 5: -10, 6: 1, 7: 0} diff --git a/tests/simple/sltiu.S b/tests/simple/sltiu.S new file mode 100644 index 00000000..5de314a1 --- /dev/null +++ b/tests/simple/sltiu.S @@ -0,0 +1,14 @@ +#include "simple.h" + +START_TEXT + addi x1, x0, 1 // x1 = 1 + sltiu x2, x1, 2 // x2 = 1 + sltiu x3, x1, 1 // x3 = 0 + + addi x4, x0, 1 // x4 = 1 + sltiu x4, x4, 1 // x4 = 0 + + addi x5, x0, -10 // x5 = -10 + sltiu x6, x5, 1 // x6 = 0 + sltiu x7, x5, -11 // x7 = 0 +END_TEXT diff --git a/tests/simple/sltiu.S.assert b/tests/simple/sltiu.S.assert new file mode 100644 index 00000000..6064c11d --- /dev/null +++ b/tests/simple/sltiu.S.assert @@ -0,0 +1 @@ +regs: {1: 1, 2: 1, 3: 0, 4: 0, 5: -10, 6: 0, 7: 0} diff --git a/tests/simple/sltu.S b/tests/simple/sltu.S new file mode 100644 index 00000000..da9b31b7 --- /dev/null +++ b/tests/simple/sltu.S @@ -0,0 +1,19 @@ +#include "simple.h" + +START_TEXT + // Same as sltu.S, but put immediates in registers + addi x15, x0, 2 + addi x14, x0, 1 + addi x13, x0, -11 + + addi x1, x0, 1 // x1 = 1 + sltu x2, x1, x15 // x2 = 1 + sltu x3, x1, x14 // x3 = 0 + + addi x4, x0, 1 // x4 = 1 + sltu x4, x4, x14 // x4 = 0 + + addi x5, x0, -10 // x5 = -10 + sltu x6, x5, x14 // x6 = 0 + sltu x7, x5, x13 // x7 = 0 +END_TEXT diff --git a/tests/simple/sltu.S.assert b/tests/simple/sltu.S.assert new file mode 100644 index 00000000..6064c11d --- /dev/null +++ b/tests/simple/sltu.S.assert @@ -0,0 +1 @@ +regs: {1: 1, 2: 1, 3: 0, 4: 0, 5: -10, 6: 0, 7: 0} diff --git a/tests/simple/sra.S b/tests/simple/sra.S new file mode 100644 index 00000000..2a3405be --- /dev/null +++ b/tests/simple/sra.S @@ -0,0 +1,11 @@ +#include "simple.h" +START_TEXT + li x15, 0xFFFFFFE0 // x15[4:0] = 0 + li x14, 0xFFFFFFE4 // x14[4:0] = 4 + li x13, 0xFFFFFFFF // x13[4:0] = 31 + + li x1, 0xDEADBEEF + sra x2, x1, x15 // x2 = 0xDEADBEEF + sra x3, x1, x14 // x3 = 0xFDEADBEE + sra x4, x1, x13 // x4 = 0xFFFFFFFF +END_TEXT diff --git a/tests/simple/sra.S.assert b/tests/simple/sra.S.assert new file mode 100644 index 00000000..e0e38fd5 --- /dev/null +++ b/tests/simple/sra.S.assert @@ -0,0 +1 @@ +regs: {1: 0xDEADBEEF, 2: 0xDEADBEEF, 3: 0xFDEADBEE, 4: 0xFFFFFFFF} \ No newline at end of file diff --git a/tests/simple/sra.S.simple b/tests/simple/sra.S.simple new file mode 100644 index 00000000..e0e38fd5 --- /dev/null +++ b/tests/simple/sra.S.simple @@ -0,0 +1 @@ +regs: {1: 0xDEADBEEF, 2: 0xDEADBEEF, 3: 0xFDEADBEE, 4: 0xFFFFFFFF} \ No newline at end of file diff --git a/tests/simple/srai.S b/tests/simple/srai.S new file mode 100644 index 00000000..f9fed23b --- /dev/null +++ b/tests/simple/srai.S @@ -0,0 +1,8 @@ +#include "simple.h" + +START_TEXT + li x1, 0xDEADBEEF + srai x2, x1, 0 // x2 = 0xDEADBEEF + srai x3, x1, 4 // x3 = 0xFDEADBEE + srai x4, x1, 31 // x4 = 0xFFFFFFFF +END_TEXT diff --git a/tests/simple/srai.S.assert b/tests/simple/srai.S.assert new file mode 100644 index 00000000..e0e38fd5 --- /dev/null +++ b/tests/simple/srai.S.assert @@ -0,0 +1 @@ +regs: {1: 0xDEADBEEF, 2: 0xDEADBEEF, 3: 0xFDEADBEE, 4: 0xFFFFFFFF} \ No newline at end of file diff --git a/tests/simple/srl.S b/tests/simple/srl.S new file mode 100644 index 00000000..1a0f0865 --- /dev/null +++ b/tests/simple/srl.S @@ -0,0 +1,12 @@ +#include "simple.h" + +START_TEXT + li x15, 0xFFFFFFE0 // x15[4:0] = 0 + li x14, 0xFFFFFFE4 // x14[4:0] = 4 + li x13, 0xFFFFFFFF // x13[4:0] = 31 + + li x1, 0xDEADBEEF + srl x2, x1, x15 // x2 = 0xDEADBEEF + srl x3, x1, x14 // x3 = 0x0DEADBEE + srl x4, x1, x13 // x4 = 0x00000001 +END_TEXT diff --git a/tests/simple/srl.S.assert b/tests/simple/srl.S.assert new file mode 100644 index 00000000..5dafbf25 --- /dev/null +++ b/tests/simple/srl.S.assert @@ -0,0 +1 @@ +regs: {1: 0xDEADBEEF, 2: 0xDEADBEEF, 3: 0x0DEADBEE, 4: 0x00000001} \ No newline at end of file diff --git a/tests/simple/srli.S b/tests/simple/srli.S new file mode 100644 index 00000000..64b9494c --- /dev/null +++ b/tests/simple/srli.S @@ -0,0 +1,8 @@ +#include "simple.h" + +START_TEXT + li x1, 0xDEADBEEF + srli x2, x1, 0 // x2 = 0xDEADBEEF + srli x3, x1, 4 // x3 = 0x0DEADBEE + srli x4, x1, 31 // x4 = 0x00000001 +END_TEXT diff --git a/tests/simple/srli.S.assert b/tests/simple/srli.S.assert new file mode 100644 index 00000000..5dafbf25 --- /dev/null +++ b/tests/simple/srli.S.assert @@ -0,0 +1 @@ +regs: {1: 0xDEADBEEF, 2: 0xDEADBEEF, 3: 0x0DEADBEE, 4: 0x00000001} \ No newline at end of file diff --git a/tests/simple/sub.S b/tests/simple/sub.S new file mode 100644 index 00000000..9f7894b2 --- /dev/null +++ b/tests/simple/sub.S @@ -0,0 +1,13 @@ +#include "simple.h" + +START_TEXT + li x1, 0xDEADBEEF // x1 = 0xDEADBEEF + add x2, x1, x0 // x2 = 0xDEADBEEF + + sub x3, x0, x2 // x3 = -x2 + + xori x4, x2, -1 // x4 = ~x2 + addi x4, x4, 1 // x4 = ~x2 + 1 = -x2 + + sub x5, x4, x3 // x5 = 0 +END_TEXT diff --git a/tests/simple/sub.S.assert b/tests/simple/sub.S.assert new file mode 100644 index 00000000..342f3b6c --- /dev/null +++ b/tests/simple/sub.S.assert @@ -0,0 +1 @@ +regs: {2: 0xDEADBEEF, 3: 0x21524111, 4: 0x21524111, 5: 0} diff --git a/tests/simple/xor.S b/tests/simple/xor.S new file mode 100644 index 00000000..1b54aa5a --- /dev/null +++ b/tests/simple/xor.S @@ -0,0 +1,15 @@ +#include "simple.h" + +START_TEXT + // Same as xori.S, but put immediates in registers + addi x15, x0, 0 + addi x14, x0, 1 + addi x13, x0, -10 + + li x1, 0xFFFFFFFF + xor x2, x1, x15 // x2 = 0xFFFFFFFF + xor x3, x1, x14 // x2 = 0xFFFFFFFE + + li x4, -11 // x4 = -11 + xor x5, x4, x13 // x4 = 3 +END_TEXT diff --git a/tests/simple/xor.S.assert b/tests/simple/xor.S.assert new file mode 100644 index 00000000..f115c37a --- /dev/null +++ b/tests/simple/xor.S.assert @@ -0,0 +1 @@ +regs: {1: 0xFFFFFFFF, 2: 0xFFFFFFFF, 3: 0xFFFFFFFE, 4: -11, 5: 3} diff --git a/tests/simple/xori.S b/tests/simple/xori.S new file mode 100644 index 00000000..fc26790a --- /dev/null +++ b/tests/simple/xori.S @@ -0,0 +1,10 @@ +#include "simple.h" + +START_TEXT + li x1, 0xFFFFFFFF + xori x2, x1, 0 // x2 = 0xFFFFFFFF + xori x3, x1, 1 // x2 = 0xFFFFFFFE + + li x4, -11 // x4 = -11 + xori x5, x4, -10 // x4 = 3 +END_TEXT diff --git a/tests/simple/xori.S.assert b/tests/simple/xori.S.assert new file mode 100644 index 00000000..f115c37a --- /dev/null +++ b/tests/simple/xori.S.assert @@ -0,0 +1 @@ +regs: {1: 0xFFFFFFFF, 2: 0xFFFFFFFF, 3: 0xFFFFFFFE, 4: -11, 5: 3}