Skip to content

Commit

Permalink
fix: correctly verify mips instruction encoding (#237)
Browse files Browse the repository at this point in the history
A lot of instructions in the MIPS spec require that certain fields
be set to zero. Most of the time this isn't actually a problem but
this can cause side-effects in a few cases. A buggy compiler could
create an issue if it ever spit out non-compliant instructions.
This PR implements those zero value enforcement checks for all
instructions that we implement.
  • Loading branch information
smartcontracts authored and ajsutton committed Aug 16, 2024
1 parent db61d2b commit b892143
Show file tree
Hide file tree
Showing 98 changed files with 1,817 additions and 18 deletions.
53 changes: 53 additions & 0 deletions cannon/mipsevm/exec/mips_instructions.go
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,9 @@ func ExecMipsCoreStepLogic(cpu *mipsevm.CpuScalars, registers *[32]uint32, memor
}
}

// Verify that the instruction is properly encoded.
CheckZeroEncoding(insn)

// ALU
val := ExecuteMipsInstruction(insn, opcode, fun, rs, rt, mem)

Expand Down Expand Up @@ -120,6 +123,56 @@ func ExecMipsCoreStepLogic(cpu *mipsevm.CpuScalars, registers *[32]uint32, memor
return HandleRd(cpu, registers, rdReg, val, true)
}

func CheckZeroEncoding(insn uint32) {
// Pick out the opcode and function code.
opcode := uint8(insn >> 26)
funcCode := uint8(insn & 0x3F)

// Pick out the registers.
rs := uint8((insn >> 21) & 0x1F)
rt := uint8((insn >> 16) & 0x1F)
rd := uint8((insn >> 11) & 0x1F)
shamt := uint8((insn >> 6) & 0x1F)

// Checks for R-type instructions.
if opcode == 0x00 {
// Check for zero rs.
if funcCode == 0x00 || funcCode == 0x02 || funcCode == 0x03 || funcCode == 0x10 || funcCode == 0x12 {
if rs != 0 {
panic("rs not zero")
}
}

// Check for zero rt.
if funcCode == 0x08 || funcCode == 0x09 || (funcCode >= 0x10 && funcCode <= 0x13) {
if rt != 0 {
panic("rt not zero")
}
}

// Check for zero rd.
if funcCode == 0x08 || funcCode == 0x11 || funcCode == 0x13 || (funcCode >= 0x18 && funcCode <= 0x1B) {
if rd != 0 {
panic("rd not zero")
}
}

// Check for zero shamt.
if funcCode == 0x08 || funcCode == 0x09 || funcCode == 0x0F || (funcCode >= 0x10 && funcCode <= 0x13) || (funcCode >= 0x18 && funcCode <= 0x1B) || (funcCode >= 0x20 && funcCode <= 0x27) || funcCode == 0x2A || funcCode == 0x2B {
if shamt != 0 {
panic("shamt not zero")
}
}
}

// Check for zero rs in LUI.
if opcode == 0x0F {
if rs != 0 {
panic("rs not zero")
}
}
}

func ExecuteMipsInstruction(insn, opcode, fun, rs, rt, mem uint32) uint32 {
if opcode == 0 || (opcode >= 8 && opcode < 0xF) {
// transform ArithLogI to SPECIAL
Expand Down
2 changes: 2 additions & 0 deletions cannon/mipsevm/tests/evm_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,8 @@ func TestEVM(t *testing.T) {
require.NotEqual(t, uint32(testutil.EndAddr), goState.GetState().GetPC(), "must not reach end")
require.True(t, goState.GetState().GetExited(), "must set exited state")
require.Equal(t, uint8(1), goState.GetState().GetExitCode(), "must exit with 1")
} else if expectPanic {
require.NotEqual(t, uint32(testutil.EndAddr), state.Cpu.PC, "must not reach end")
} else {
require.Equal(t, uint32(testutil.EndAddr), state.Cpu.PC, "must reach end")
// inspect test result
Expand Down
133 changes: 133 additions & 0 deletions cannon/mipsevm/tests/open_mips_tests/gentests.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,133 @@
# Utility for generating assembly test files for the MIPS instructions that panic when specific
# fields in the encoded instruction are nonzero. Using a script to do this is much less prone to
# human error than writing these tests by hand.

import os

# Format is (opcode, funct, shamt, rd, rt, rs, field_to_make_nonzero)
tests = {
'ADD': [('000000', '100000', '00001', '01011', '01010', '01001', 'shamt')], # SHAMT nonzero
'ADDU': [('000000', '100001', '00001', '01011', '01010', '01001', 'shamt')], # SHAMT nonzero
'AND': [('000000', '100100', '00001', '01011', '01010', '01001', 'shamt')], # SHAMT nonzero
'DIV': [
('000000', '011010', '00001', '01010', '00000', '01001', 'rd'), # RD nonzero
('000000', '011010', '00001', '00000', '01010', '01001', 'shamt'), # SHAMT nonzero
],
'DIVU': [
('000000', '011011', '00001', '01010', '00000', '01001', 'rd'), # RD nonzero
('000000', '011011', '00001', '00000', '01010', '01001', 'shamt'), # SHAMT nonzero
],
'JALR': [
('000000', '001001', '00000', '01011', '01001', '01010', 'rt'), # RT nonzero
('000000', '001001', '00001', '01011', '01001', '00000', 'shamt'), # SHAMT nonzero
],
'JR': [
('000000', '001000', '00000', '01011', '01001', '00000', 'rd'), # RD nonzero
('000000', '001000', '00000', '00000', '01001', '01010', 'rt'), # RT nonzero
('000000', '001000', '00001', '00000', '01001', '00000', 'shamt'), # SHAMT nonzero
],
'LUI': [('001111', '00000', '01010', '00000', '00000', '01001', 'rs')], # RS nonzero
'MFHI': [
('000000', '010000', '00000', '01011', '01010', '00000', 'rt'), # RT nonzero
('000000', '010000', '00001', '01011', '00000', '00000', 'shamt'), # SHAMT nonzero
('000000', '010000', '00000', '01011', '00000', '01001', 'rs'), # RS nonzero
],
'MFLO': [
('000000', '010010', '00000', '01011', '01010', '00000', 'rt'), # RT nonzero
('000000', '010010', '00001', '01011', '00000', '00000', 'shamt'), # SHAMT nonzero
('000000', '010010', '00000', '01011', '00000', '01001', 'rs'), # RS nonzero
],
'MTHI': [
('000000', '010001', '00000', '01011', '01010', '00000', 'rd'), # RD nonzero
('000000', '010001', '00000', '01001', '01010', '00000', 'rt'), # RT nonzero
('000000', '010001', '00001', '01001', '00000', '00000', 'shamt'), # SHAMT nonzero
],
'MTLO': [
('000000', '010011', '00000', '01011', '01010', '00000', 'rd'), # RD nonzero
('000000', '010011', '00000', '01001', '01010', '00000', 'rt'), # RT nonzero
('000000', '010011', '00001', '01001', '00000', '00000', 'shamt'), # SHAMT nonzero
],
'MULT': [
('000000', '011000', '00000', '01011', '01010', '00000', 'rd'), # RD nonzero
('000000', '011000', '00001', '00000', '01010', '01001', 'shamt'), # SHAMT nonzero
],
'MULTU': [
('000000', '011001', '00000', '01011', '01010', '00000', 'rd'), # RD nonzero
('000000', '011001', '00001', '00000', '01010', '01001', 'shamt'), # SHAMT nonzero
],
'NOR': [('000000', '100111', '00001', '01011', '01010', '01001', 'shamt')], # SHAMT nonzero
'OR': [('000000', '100101', '00001', '01011', '01010', '01001', 'shamt')], # SHAMT nonzero
'SLL': [('000000', '000000', '00001', '01011', '01010', '01001', 'shamt')], # SHAMT nonzero
'SLT': [('000000', '101010', '00001', '01011', '01010', '01001', 'shamt')], # SHAMT nonzero
'SLTU': [('000000', '101011', '00001', '01011', '01010', '01001', 'shamt')], # SHAMT nonzero
'SRA': [
('000000', '000011', '00001', '01011', '01010', '01001', 'shamt'), # SHAMT nonzero
('000000', '000011', '00000', '01011', '01010', '01001', 'rs'), # RS nonzero
],
'SRL': [
('000000', '000010', '00001', '01011', '01010', '01001', 'shamt'), # SHAMT nonzero
('000000', '000010', '00000', '01011', '01010', '01001', 'rs'), # RS nonzero
],
'SUB': [('000000', '100010', '00001', '01011', '01010', '01001', 'shamt')], # SHAMT nonzero
'SUBU': [('000000', '100011', '00001', '01011', '01010', '01001', 'shamt')], # SHAMT nonzero
'SYNC': [('000000', '001111', '00001', '00000', '00000', '00000', 'shamt')], # SHAMT nonzero
'XOR': [('000000', '100110', '00001', '01011', '01010', '01001', 'shamt')], # SHAMT nonzero
}

def pad_to_length(binary_str, length):
return binary_str.zfill(length)

def generate_instruction(opcode, rs, rt, rd, shamt, funct):
binary_instruction = (
pad_to_length(opcode, 6) +
pad_to_length(rs, 5) +
pad_to_length(rt, 5) +
pad_to_length(rd, 5) +
pad_to_length(shamt, 5) +
pad_to_length(funct, 6)
)
hex_instruction = hex(int(binary_instruction, 2))[2:].zfill(8)
return '0x' + hex_instruction

def create_test_file(instruction, field, hex_instruction):
return f"""###############################################################################
# Description:
# Tests that the '{instruction.lower()}' instruction panics when the {field} field is nonzero.
#
###############################################################################
.section .test, "x"
.balign 4
.set noreorder
.global test
.ent test
test:
lui $s0, 0xbfff
ori $s0, 0xfff0
ori $s1, $0, 1
# Invalid {instruction} (nonzero {field} field)
.word {hex_instruction}
sw $zero, 8($s0)
sw $s1, 4($s0)
$done:
jr $ra
nop
.end test
"""

def write_test_file(filename, content):
os.makedirs('./test', exist_ok=True)
with open(f'./test/{filename}', 'w') as file:
file.write(content)

for instr, cases in tests.items():
for params in cases:
opcode, funct, shamt, rd, rt, rs, field = params
hex_instr = generate_instruction(opcode, rs, rt, rd, shamt, funct)
test_content = create_test_file(instr, field, hex_instr)
filename = f"{instr.lower()}_nonzero_{field}_panic.asm"
write_test_file(filename, test_content)
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
###############################################################################
# Description:
# Tests that the 'add' instruction panics when the shamt field is nonzero.
#
###############################################################################

.section .test, "x"
.balign 4
.set noreorder
.global test
.ent test
test:
lui $s0, 0xbfff
ori $s0, 0xfff0
ori $s1, $0, 1

# Invalid ADD (nonzero shamt field)
.word 0x012a5860

sw $zero, 8($s0)
sw $s1, 4($s0)

$done:
jr $ra
nop

.end test
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
###############################################################################
# Description:
# Tests that the 'addu' instruction panics when the shamt field is nonzero.
#
###############################################################################

.section .test, "x"
.balign 4
.set noreorder
.global test
.ent test
test:
lui $s0, 0xbfff
ori $s0, 0xfff0
ori $s1, $0, 1

# Invalid ADDU (nonzero shamt field)
.word 0x012a5861

sw $zero, 8($s0)
sw $s1, 4($s0)

$done:
jr $ra
nop

.end test
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
###############################################################################
# Description:
# Tests that the 'and' instruction panics when the shamt field is nonzero.
#
###############################################################################

.section .test, "x"
.balign 4
.set noreorder
.global test
.ent test
test:
lui $s0, 0xbfff
ori $s0, 0xfff0
ori $s1, $0, 1

# Invalid AND (nonzero shamt field)
.word 0x012a5864

sw $zero, 8($s0)
sw $s1, 4($s0)

$done:
jr $ra
nop

.end test
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
27 changes: 27 additions & 0 deletions cannon/mipsevm/tests/open_mips_tests/test/div_nonzero_rd_panic.asm
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
###############################################################################
# Description:
# Tests that the 'div' instruction panics when the rd field is nonzero.
#
###############################################################################

.section .test, "x"
.balign 4
.set noreorder
.global test
.ent test
test:
lui $s0, 0xbfff
ori $s0, 0xfff0
ori $s1, $0, 1

# Invalid DIV (nonzero rd field)
.word 0x0120505a

sw $zero, 8($s0)
sw $s1, 4($s0)

$done:
jr $ra
nop

.end test
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
###############################################################################
# Description:
# Tests that the 'div' instruction panics when the shamt field is nonzero.
#
###############################################################################

.section .test, "x"
.balign 4
.set noreorder
.global test
.ent test
test:
lui $s0, 0xbfff
ori $s0, 0xfff0
ori $s1, $0, 1

# Invalid DIV (nonzero shamt field)
.word 0x012a005a

sw $zero, 8($s0)
sw $s1, 4($s0)

$done:
jr $ra
nop

.end test
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
###############################################################################
# Description:
# Tests that the 'divu' instruction panics when the rd field is nonzero.
#
###############################################################################

.section .test, "x"
.balign 4
.set noreorder
.global test
.ent test
test:
lui $s0, 0xbfff
ori $s0, 0xfff0
ori $s1, $0, 1

# Invalid DIVU (nonzero rd field)
.word 0x0120505b

sw $zero, 8($s0)
sw $s1, 4($s0)

$done:
jr $ra
nop

.end test
Loading

0 comments on commit b892143

Please sign in to comment.