github/powdr
1
1
Fork 0
mirror of https://github.com/powdr-labs/powdr.git synced 2026-05-13 03:00:26 -04:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #994 from powdr-labs/merging-instructions

Browse Source 
Merging instructions and saving a couple of columns.
This commit is contained in:
Lucas Clemente Vella
2024-02-01 14:34:20 +00:00
committed by GitHub
parent e157f3fbd9 2940dafb5d
commit 66a4da83aa
3 changed files with 39 additions and 65 deletions
Download Patch File Download Diff File Expand all files Collapse all files

36
riscv-executor/src/lib.rs
View File

@@ -558,16 +558,12 @@ impl<'a, 'b, F: FieldElement> Executor<'a, 'b, F> {
vec![]
}
"jump" => {
self.proc.set_pc(args[0]);
Vec::new()
}
"load_label" => args,
"jump_dyn" => {
"jump" | "jump_dyn" => {
let next_pc = self.proc.get_pc().u() + 1;
self.proc.set_pc(args[0]);
Vec::new()
vec![next_pc.into()]
}
"jump_to_bootloader_input" => {
let bootloader_input_idx = args[0].0 as usize;
@@ -576,32 +572,6 @@ impl<'a, 'b, F: FieldElement> Executor<'a, 'b, F> {
Vec::new()
}
"jump_and_link_dyn" => {
let pc = self.proc.get_pc();
self.proc.set_reg("x1", pc.u() + 1);
self.proc.set_pc(args[0]);
Vec::new()
}
"call" => {
let pc = self.proc.get_pc();
self.proc.set_reg("x1", pc.u() + 1);
self.proc.set_pc(args[0]);
Vec::new()
}
"tail" => {
self.proc.set_pc(args[0]);
self.proc.set_reg("x6", args[0]);
Vec::new()
}
"ret" => {
let target = self.proc.get_reg("x1");
self.proc.set_pc(target);
Vec::new()
}
"branch_if_nonzero" => {
if args[0].0 != 0 {
self.proc.set_pc(args[1]);

52
riscv/src/compiler.rs
View File

@@ -187,10 +187,10 @@ pub fn compile(
.into_iter()
.map(|(id, dir, file)| format!(".debug file {id} {} {};", quote(&dir), quote(&file)))
.chain(bootloader_and_shutdown_routine_lines)
.chain(["call __data_init;".to_string()])
.chain(["x1 <== jump(__data_init);".to_string()])
.chain([
format!("// Set stack pointer\nx2 <=X= {stack_start};"),
"call __runtime_start;".to_string(),
"x1 <== jump(__runtime_start);".to_string(),
"return;".to_string(), // This is not "riscv ret", but "return from powdr asm function".
])
.chain(
@@ -200,7 +200,10 @@ pub fn compile(
)
.chain(["// This is the data initialization routine.\n__data_init:".to_string()])
.chain(data_code)
.chain(["// This is the end of the data initialization routine.\nret;".to_string()])
.chain([
"// This is the end of the data initialization routine.\ntmp1 <== jump_dyn(x1);"
.to_string(),
])
.collect();
// The program ROM needs to fit the degree, so we use the next power of 2.
@@ -475,12 +478,10 @@ fn preamble(degree: u64, coprocessors: &CoProcessors, with_bootloader: bool) ->
// ============== control-flow instructions ==============
instr jump l: label { pc' = l }
instr load_label l: label -> X { X = l }
instr jump_dyn X { pc' = X }
instr jump_and_link_dyn X { pc' = X, x1' = pc + 1 }
instr call l: label { pc' = l, x1' = pc + 1 }
instr ret { pc' = x1 }
instr jump l: label -> Y { pc' = l, Y = pc + 1}
instr jump_dyn X -> Y { pc' = X, Y = pc + 1}
instr branch_if_nonzero X, l: label { pc' = (1 - XIsZero) * l + XIsZero * (pc + 1) }
instr branch_if_zero X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) }
@@ -933,7 +934,11 @@ fn try_coprocessor_substitution(label: &str, coprocessors: &CoProcessors) -> Opt
fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcessors) -> Vec<String> {
match instr {
// load/store registers
"li" => {
"li" | "la" => {
// The difference between "li" and "la" in RISC-V is that the former
// is for loading values as is, and the later is for loading PC
// relative values. But since we work on a higher abstraction level,
// for us they are the same thing.
let (rd, imm) = ri(args);
only_if_no_write_to_zero(format!("{rd} <=X= {imm};"), rd)
}
@@ -942,10 +947,6 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso
let (rd, imm) = ri(args);
only_if_no_write_to_zero(format!("{rd} <=X= {};", imm << 12), rd)
}
"la" => {
let (rd, addr) = ri(args);
only_if_no_write_to_zero(format!("{rd} <=X= {};", addr), rd)
}
"mv" => {
let (rd, rs) = rr(args);
only_if_no_write_to_zero(format!("{rd} <=X= {rs};"), rd)
@@ -1250,14 +1251,17 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso
// jump and call
"j" => {
if let [label] = args {
vec![format!("jump {};", argument_to_escaped_symbol(label))]
vec![format!(
"tmp1 <== jump({});",
argument_to_escaped_symbol(label)
)]
} else {
panic!()
}
}
"jr" => {
let rs = r(args);
vec![format!("jump_dyn {rs};")]
vec![format!("tmp1 <== jump_dyn({rs});")]
}
"jal" => {
let (_rd, _label) = rl(args);
@@ -1266,7 +1270,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso
"jalr" => {
// TODO there is also a form that takes more arguments
let rs = r(args);
vec![format!("jump_and_link_dyn {rs};")]
vec![format!("x1 <== jump_dyn({rs});")]
}
"call" | "tail" => {
// Depending on what symbol is called, the call is replaced by a
@@ -1282,9 +1286,9 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso
};
match (replacement, instr) {
(None, instr) => {
let instr = if instr == "tail" { "jump" } else { instr };
let arg = argument_to_escaped_symbol(label);
vec![format!("{instr} {arg};")]
let dest = if instr == "tail" { "tmp1" } else { "x1" };
vec![format!("{dest} <== jump({arg});")]
}
// Both "call" and "tail" are pseudoinstructions that are
// supposed to use x6 to calculate the high bits of the
@@ -1292,7 +1296,9 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso
// but no sane program would rely on this behavior, so we are
// probably fine.
(Some(replacement), "call") => vec![replacement],
(Some(replacement), "tail") => vec![replacement, "ret;".to_string()],
(Some(replacement), "tail") => {
vec![replacement, "tmp1 <== jump_dyn(x1);".to_string()]
}
(Some(_), _) => unreachable!(),
}
}
@@ -1308,7 +1314,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso
}
"ret" => {
assert!(args.is_empty());
vec!["ret;".to_string()]
vec!["tmp1 <== jump_dyn(x1);".to_string()]
}
// memory access
@@ -1402,7 +1408,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso
format!("mstore {rd} + {off} - tmp2, tmp1;"),
]
}
"nop" => vec![],
"fence" | "fence.i" | "nop" => vec![],
"unimp" => vec!["fail;".to_string()],
// Special instruction that is inserted to allow dynamic label references
@@ -1411,9 +1417,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso
only_if_no_write_to_zero(format!("{rd} <== load_label({label});"), rd)
}
// atomic and synchronization
"fence" | "fence.i" => vec![],
// atomic instructions
insn if insn.starts_with("amoadd.w") => {
let (rd, rs2, rs1, off) = rrro(args);
assert_eq!(off, 0);

16
riscv/src/continuations/bootloader.rs
View File

@@ -138,19 +138,19 @@ pub fn bootloader_and_shutdown_routine(submachine_initialization: &[String]) ->
bootloader.push_str(&format!(
r#"
// Skip the next instruction
jump submachine_init;
tmp1 <== jump(submachine_init);
// For convenience, this instruction has a known fixed PC ({DEFAULT_PC}) and just jumps
// to whatever comes after the bootloader + shutdown routine. This avoids having to count
// the instructions of the bootloader and the submachine initialization.
jump computation_start;
tmp1 <== jump(computation_start);
// Similarly, this instruction has a known fixed PC ({SHUTDOWN_START}) and just jumps
// to the shutdown routine.
jump shutdown_start;
tmp1 <== jump(shutdown_start);
shutdown_sink:
jump shutdown_sink;
tmp1 <== jump(shutdown_sink);
// Submachine initialization: Calls each submachine once, because that helps witness
// generation figure out default values that can be used if the machine is never used.
@@ -282,7 +282,7 @@ P4 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OF
P5 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OFFSET} + 1 + {WORDS_PER_PAGE} + 4 + {i} * 4 + 1);
P6 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OFFSET} + 1 + {WORDS_PER_PAGE} + 4 + {i} * 4 + 2);
P7 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OFFSET} + 1 + {WORDS_PER_PAGE} + 4 + {i} * 4 + 3);
jump bootloader_level_{i}_end;
tmp1 <== jump(bootloader_level_{i}_end);
bootloader_level_{i}_is_right:
P4 <=X= P0;
P5 <=X= P1;
@@ -307,7 +307,7 @@ branch_if_nonzero P0 - x5, bootloader_memory_hash_mismatch;
branch_if_nonzero P1 - x6, bootloader_memory_hash_mismatch;
branch_if_nonzero P2 - x7, bootloader_memory_hash_mismatch;
branch_if_nonzero P3 - x8, bootloader_memory_hash_mismatch;
jump bootloader_memory_hash_ok;
tmp1 <== jump(bootloader_memory_hash_ok);
bootloader_memory_hash_mismatch:
fail;
bootloader_memory_hash_ok:
@@ -322,7 +322,7 @@ P2 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OF
P3 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OFFSET} + 1 + {WORDS_PER_PAGE} + 3);
// Repeat Merkle proof validation loop to compute updated Merkle root
jump bootloader_merkle_proof_validation_loop;
tmp1 <== jump(bootloader_merkle_proof_validation_loop);
bootloader_update_memory_hash:
@@ -478,7 +478,7 @@ branch_if_nonzero x2 - x1, shutdown_start_page_loop;
shutdown_end_page_loop:
jump shutdown_sink;
tmp1 <== jump(shutdown_sink);
// END OF SHUTDOWN ROUTINE