Skip to content

Commit

Permalink
Merge pull request #2754 from o1-labs/sai/adding-test-no-action
Browse files Browse the repository at this point in the history
adding no-action test, some i instructions, and single syscall impl
svv232 authored Nov 18, 2024
2 parents 59250e7 + 4bc0b20 commit 119b5a1
Showing 4 changed files with 187 additions and 8 deletions.
Binary file added o1vm/resources/programs/riscv32i/no-action
Binary file not shown.
157 changes: 152 additions & 5 deletions o1vm/src/interpreters/riscv32i/interpreter.rs
Original file line number Diff line number Diff line change
@@ -1061,7 +1061,6 @@ pub trait InterpreterEnv {

pub fn interpret_instruction<Env: InterpreterEnv>(env: &mut Env, instr: Instruction) {
env.activate_selector(instr);

match instr {
Instruction::RType(rtype) => interpret_rtype(env, rtype),
Instruction::IType(itype) => interpret_itype(env, itype),
@@ -1077,8 +1076,155 @@ pub fn interpret_rtype<Env: InterpreterEnv>(_env: &mut Env, _instr: RInstruction
unimplemented!("TODO")
}

pub fn interpret_itype<Env: InterpreterEnv>(_env: &mut Env, _instr: IInstruction) {
unimplemented!("TODO")
pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: IInstruction) {
/* fetch instruction pointer from the program state */
let instruction_pointer = env.get_instruction_pointer();
/* compute the next instruction ptr and add one, as well record raml lookup */
let next_instruction_pointer = env.get_next_instruction_pointer();
/* read instruction from ip address */
let instruction = {
let v0 = env.read_memory(&instruction_pointer);
let v1 = env.read_memory(&(instruction_pointer.clone() + Env::constant(1)));
let v2 = env.read_memory(&(instruction_pointer.clone() + Env::constant(2)));
let v3 = env.read_memory(&(instruction_pointer.clone() + Env::constant(3)));
(v3 * Env::constant(1 << 24))
+ (v2 * Env::constant(1 << 16))
+ (v1 * Env::constant(1 << 8))
+ v0
};

/* fetch opcode from instruction bit 0 - 6 for a total len of 7 */
let opcode = {
let pos = env.alloc_scratch();
unsafe { env.bitmask(&instruction, 7, 0, pos) }
};
/* verify opcode is 7 bits */
env.range_check8(&opcode, 7);

/* decode and parse bits from the full 32 bits instruction in accordance with the Rtype riscV spec
https://www.cs.cornell.edu/courses/cs3410/2024fa/assignments/cpusim/riscv-instructions.pdf
*/
let rd = {
let pos = env.alloc_scratch();
unsafe { env.bitmask(&instruction, 12, 7, pos) }
};
env.range_check8(&rd, 5);
let funct3 = {
let pos = env.alloc_scratch();
unsafe { env.bitmask(&instruction, 15, 12, pos) }
};
env.range_check8(&funct3, 3);

let rs1 = {
let pos = env.alloc_scratch();
unsafe { env.bitmask(&instruction, 20, 15, pos) }
};
env.range_check8(&rs1, 5);

let imm = {
let pos = env.alloc_scratch();
unsafe { env.bitmask(&instruction, 32, 20, pos) }
};

env.range_check16(&imm, 12);

// check correctness of decomposition of I type function
// TODO add decoding constraint checking

match instr {
IInstruction::LoadWord => {
// lw: x[rd] = sext(M[x[rs1] + sext(offset)][31:0])
let base = env.read_register(&rs1);
let offset = env.sign_extend(&imm, 12);
let address = {
let address_scratch = env.alloc_scratch();
let overflow_scratch = env.alloc_scratch();
let (address, _overflow) =
unsafe { env.add_witness(&base, &offset, address_scratch, overflow_scratch) };
address
};
// Add a range check here for address
let v0 = env.read_memory(&address);
let v1 = env.read_memory(&(address.clone() + Env::constant(1)));
let v2 = env.read_memory(&(address.clone() + Env::constant(2)));
let v3 = env.read_memory(&(address.clone() + Env::constant(3)));
let value = (v0 * Env::constant(1 << 24))
+ (v1 * Env::constant(1 << 16))
+ (v2 * Env::constant(1 << 8))
+ v3;
let value = env.sign_extend(&value, 32);
env.write_register(&rd, value);
env.set_instruction_pointer(next_instruction_pointer.clone());
env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
}
IInstruction::AddImmediate => {
// addi: x[rd] = x[rs1] + sext(immediate)
let local_rs1 = env.read_register(&(rs1.clone()));
let local_imm = env.sign_extend(&imm, 12);
let overflow_scratch = env.alloc_scratch();
let rd_scratch = env.alloc_scratch();
let local_rd = unsafe {
let (local_rd, _overflow) =
env.add_witness(&local_rs1, &local_imm, rd_scratch, overflow_scratch);
local_rd
};
env.write_register(&rd, local_rd);
env.set_instruction_pointer(next_instruction_pointer.clone());
env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
}
IInstruction::XorImmediate => {
// xori: x[rd] = x[rs1] ^ sext(immediate)
let local_rs1 = env.read_register(&rs1);
let local_imm = env.sign_extend(&imm, 12);
let rd_scratch = env.alloc_scratch();
let local_rd = unsafe { env.xor_witness(&local_rs1, &local_imm, rd_scratch) };
env.write_register(&rd, local_rd);
env.set_instruction_pointer(next_instruction_pointer.clone());
env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
}
IInstruction::OrImmediate => {
// ori: x[rd] = x[rs1] | sext(immediate)
let local_rs1 = env.read_register(&rs1);
let local_imm = env.sign_extend(&imm, 12);
let rd_scratch = env.alloc_scratch();
let local_rd = unsafe { env.or_witness(&local_rs1, &local_imm, rd_scratch) };
env.write_register(&rd, local_rd);
env.set_instruction_pointer(next_instruction_pointer.clone());
env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
}
IInstruction::AndImmediate => {
// andi: x[rd] = x[rs1] & sext(immediate)
let local_rs1 = env.read_register(&rs1);
let local_imm = env.sign_extend(&imm, 12);
let rd_scratch = env.alloc_scratch();
let local_rd = unsafe { env.and_witness(&local_rs1, &local_imm, rd_scratch) };
env.write_register(&rd, local_rd);
env.set_instruction_pointer(next_instruction_pointer.clone());
env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
}
IInstruction::JumpAndLinkRegister => {
let addr = env.read_register(&rs1);
// jalr:
// t = pc+4;
// pc = (x[rs1] + sext(offset)) & ∼1; <- NOT NOW
// pc = (x[rs1] + sext(offset)); <- PLEASE FIXME
// x[rd] = t
let offset = env.sign_extend(&imm, 12);
let new_addr = {
let res_scratch = env.alloc_scratch();
let overflow_scratch = env.alloc_scratch();
let (res, _overflow) =
unsafe { env.add_witness(&addr, &offset, res_scratch, overflow_scratch) };
res
};
env.write_register(&rd, next_instruction_pointer.clone());
env.set_instruction_pointer(new_addr.clone());
env.set_next_instruction_pointer(new_addr.clone() + Env::constant(4u32));
}
_ => {
panic!("Unimplemented instruction: {:?}", instr);
}
};
}

pub fn interpret_stype<Env: InterpreterEnv>(_env: &mut Env, _instr: SInstruction) {
@@ -1097,6 +1243,7 @@ pub fn interpret_ujtype<Env: InterpreterEnv>(_env: &mut Env, _instr: UJInstructi
unimplemented!("TODO")
}

pub fn interpret_syscall<Env: InterpreterEnv>(_env: &mut Env, _instr: SyscallInstruction) {
unimplemented!("TODO")
pub fn interpret_syscall<Env: InterpreterEnv>(env: &mut Env, _instr: SyscallInstruction) {
// FIXME: check if it is syscall success. There is only one syscall atm
env.set_halted(Env::constant(1));
}
4 changes: 2 additions & 2 deletions o1vm/src/interpreters/riscv32i/mod.rs
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
/// The minimal number of columns required for the VM
// FIXME: the value will be updated when the interpreter is fully
// implemented. Using a small value for now.
pub const SCRATCH_SIZE: usize = 20;
pub const SCRATCH_SIZE: usize = 80;

/// Number of instructions in the ISA
// FIXME: the value might not be correct. It will be updated when the
// interpreter is fully implemented.
pub const INSTRUCTION_SET_SIZE: usize = 47;
pub const INSTRUCTION_SET_SIZE: usize = 40;
pub const PAGE_ADDRESS_SIZE: u32 = 12;
pub const PAGE_SIZE: u32 = 1 << PAGE_ADDRESS_SIZE;
pub const PAGE_ADDRESS_MASK: u32 = PAGE_SIZE - 1;
34 changes: 33 additions & 1 deletion o1vm/tests/test_riscv_elf.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,9 @@
use o1vm::interpreters::riscv32i::interpreter::{IInstruction, Instruction, RInstruction};
use mina_curves::pasta::Fp;
use o1vm::interpreters::riscv32i::{
interpreter::{IInstruction, Instruction, RInstruction},
witness::Env,
PAGE_SIZE,
};

#[test]
// Checking an instruction can be converted into a string.
@@ -17,3 +22,30 @@ fn test_instruction_can_be_converted_into_string() {
let instruction = Instruction::IType(IInstruction::LoadHalf);
assert_eq!(instruction.to_string(), "lh");
}

#[test]
fn test_no_action() {
let curr_dir = std::env::current_dir().unwrap();
let path = curr_dir.join(std::path::PathBuf::from(
"resources/programs/riscv32i/no-action",
));
let state = o1vm::elf_loader::parse_riscv32i(&path).unwrap();
let mut witness = Env::<Fp>::create(PAGE_SIZE.try_into().unwrap(), state);
// This is the output we get by running objdump -d no-action
assert_eq!(witness.registers.current_instruction_pointer, 69844);
assert_eq!(witness.registers.next_instruction_pointer, 69848);

(0..=7).for_each(|_| {
let instr = witness.step();
// li is addi, li is a pseudo instruction
assert_eq!(instr, Instruction::IType(IInstruction::AddImmediate))
});
assert_eq!(witness.registers.general_purpose[10], 0);
assert_eq!(witness.registers.general_purpose[11], 0);
assert_eq!(witness.registers.general_purpose[12], 0);
assert_eq!(witness.registers.general_purpose[13], 0);
assert_eq!(witness.registers.general_purpose[14], 0);
assert_eq!(witness.registers.general_purpose[15], 0);
assert_eq!(witness.registers.general_purpose[16], 0);
assert_eq!(witness.registers.general_purpose[17], 42);
}

0 comments on commit 119b5a1

Please sign in to comment.