Skip to content

Commit

Permalink
RISCV executor
Browse files Browse the repository at this point in the history
  • Loading branch information
lvella authored and Leo Alt committed Nov 6, 2023
1 parent b465f80 commit a0df34f
Show file tree
Hide file tree
Showing 23 changed files with 1,074 additions and 81 deletions.
1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ members = [
"asm_utils",
"airgen",
"type_check",
"riscv_executor",
]

[patch."https://github.com/privacy-scaling-explorations/halo2.git"]
Expand Down
27 changes: 24 additions & 3 deletions analysis/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,18 @@ pub use macro_expansion::MacroExpander;
use ast::{asm_analysis::AnalysisASMFile, parsed::asm::ASMProgram, DiffMonitor};
use number::FieldElement;

pub fn analyze<T: FieldElement>(file: ASMProgram<T>) -> Result<AnalysisASMFile<T>, Vec<String>> {
pub fn convert_asm_to_pil<T: FieldElement>(
file: ASMProgram<T>,
) -> Result<AnalysisASMFile<T>, Vec<String>> {
let mut monitor = DiffMonitor::default();
let file = analyze(file, &mut monitor)?;
Ok(convert_analyzed_to_pil_constraints(file, &mut monitor))
}

pub fn analyze<T: FieldElement>(
file: ASMProgram<T>,
monitor: &mut DiffMonitor,
) -> Result<AnalysisASMFile<T>, Vec<String>> {
// expand macros
log::debug!("Run expand analysis step");
let file = macro_expansion::expand(file);
Expand All @@ -23,15 +32,27 @@ pub fn analyze<T: FieldElement>(file: ASMProgram<T>) -> Result<AnalysisASMFile<T

// run analysis on virtual machines, reducing them to constrained machines
log::debug!("Start asm analysis");
let file = vm::analyze(file, &mut monitor)?;
let file = vm::analyze(file, monitor)?;
log::debug!("End asm analysis");

Ok(file)
}

pub fn convert_analyzed_to_pil_constraints<T: FieldElement>(
file: AnalysisASMFile<T>,
monitor: &mut DiffMonitor,
) -> AnalysisASMFile<T> {
// remove all asm (except external instructions)
log::debug!("Run asm_to_pil");
let file = asm_to_pil::compile(file);
monitor.push(&file);

// enforce blocks using `operation_id` and `latch`
log::debug!("Run enforce_block analysis step");
let file = block_enforcer::enforce(file);
monitor.push(&file);

Ok(file)
file
}

pub mod utils {
Expand Down
4 changes: 0 additions & 4 deletions analysis/src/vm/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,6 @@ pub fn analyze<T: FieldElement>(
log::debug!("Run batch analysis step");
let file = batcher::batch(file);
monitor.push(&file);
// remove all asm (except external instructions)
log::debug!("Run asm_to_pil analysis step");
let file = asm_to_pil::compile(file);
monitor.push(&file);

Ok(file)
}
Expand Down
6 changes: 3 additions & 3 deletions ast/src/asm_analysis/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ pub struct FunctionStatements<T> {
}

pub struct BatchRef<'a, T> {
statements: &'a [FunctionStatement<T>],
pub statements: &'a [FunctionStatement<T>],
reason: &'a Option<IncompatibleSet>,
}

Expand Down Expand Up @@ -151,7 +151,7 @@ impl<T> FunctionStatements<T> {
}

/// iterate over the batches by reference
fn iter_batches(&self) -> impl Iterator<Item = BatchRef<T>> {
pub fn iter_batches(&self) -> impl Iterator<Item = BatchRef<T>> {
match &self.batches {
Some(batches) => Either::Left(batches.iter()),
None => Either::Right(
Expand Down Expand Up @@ -246,7 +246,7 @@ pub struct CallableSymbolDefinition<T> {
}

#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Default)]
pub struct CallableSymbolDefinitions<T>(BTreeMap<String, CallableSymbol<T>>);
pub struct CallableSymbolDefinitions<T>(pub BTreeMap<String, CallableSymbol<T>>);

impl<T> IntoIterator for CallableSymbolDefinitions<T> {
type Item = CallableSymbolDefinition<T>;
Expand Down
1 change: 1 addition & 0 deletions ast/src/parsed/asm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -325,6 +325,7 @@ pub enum FunctionStatement<T> {
pub enum DebugDirective {
File(usize, String, String),
Loc(usize, usize, usize),
OriginalInstruction(String),
}

#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)]
Expand Down
3 changes: 3 additions & 0 deletions ast/src/parsed/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -238,6 +238,9 @@ impl Display for DebugDirective {
DebugDirective::Loc(file, line, col) => {
write!(f, "debug loc {file} {line} {col};")
}
DebugDirective::OriginalInstruction(insn) => {
write!(f, "debug insn \"{insn}\";")
}
}
}
}
Expand Down
4 changes: 2 additions & 2 deletions ast/src/parsed/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -161,9 +161,9 @@ pub struct PolynomialName<T> {
/// A polynomial with an optional namespace
pub struct NamespacedPolynomialReference<T> {
/// The optional namespace, if `None` then this polynomial inherits the next enclosing namespace, if any
namespace: Option<String>,
pub namespace: Option<String>,
/// The underlying polynomial
pol: IndexedPolynomialReference<T>,
pub pol: IndexedPolynomialReference<T>,
}

impl<T> NamespacedPolynomialReference<T> {
Expand Down
5 changes: 2 additions & 3 deletions compiler/benches/executor_benchmark.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
use ::compiler::inputs_to_query_callback;
use analysis::analyze;
use ast::analyzed::Analyzed;
use criterion::{criterion_group, criterion_main, Criterion};

Expand All @@ -19,15 +18,15 @@ fn get_pil() -> Analyzed<T> {
let contents = compiler::compile(riscv_asm_files, &CoProcessors::base());
let parsed = parser::parse_asm::<T>(None, &contents).unwrap();
let resolved = importer::resolve(None, parsed).unwrap();
let analyzed = analyze(resolved).unwrap();
let analyzed = analysis::convert_asm_to_pil(resolved).unwrap();
let graph = airgen::compile(analyzed);
let pil = linker::link(graph).unwrap();
let analyzed = pil_analyzer::analyze_string(&format!("{pil}"));
pilopt::optimize(analyzed)
}

fn run_witgen<T: FieldElement>(analyzed: &Analyzed<T>, input: Vec<T>) {
let query_callback = inputs_to_query_callback(input);
let query_callback = inputs_to_query_callback(&input);
let (constants, degree) = constant_evaluator::generate(analyzed);
executor::witgen::WitnessGenerator::new(analyzed, degree, &constants, query_callback)
.generate();
Expand Down
80 changes: 62 additions & 18 deletions compiler/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,12 +10,15 @@ use std::path::Path;
use std::path::PathBuf;
use std::time::Instant;

use analysis::analyze;
use analysis::convert_analyzed_to_pil_constraints;
use ast::analyzed::Analyzed;
use ast::DiffMonitor;

pub mod util;
mod verify;

use analysis::analyze;
use ast::asm_analysis::AnalysisASMFile;
pub use backend::{BackendType, Proof};
use executor::witgen::QueryCallback;
use number::write_polys_file;
Expand Down Expand Up @@ -54,7 +57,7 @@ pub fn compile_pil_or_asm<T: FieldElement>(
Ok(Some(compile_pil(
Path::new(file_name),
output_dir,
inputs_to_query_callback(inputs),
inputs_to_query_callback(&inputs),
prove_with,
external_witness_values,
)))
Expand Down Expand Up @@ -123,7 +126,8 @@ pub fn compile_asm<T: FieldElement>(
Ok(compile_asm_string(
file_name,
&contents,
inputs,
&inputs,
None,
output_dir,
force_overwrite,
prove_with,
Expand All @@ -132,19 +136,11 @@ pub fn compile_asm<T: FieldElement>(
.1)
}

/// Compiles the contents of a .asm file, outputs the PIL on stdout and tries to generate
/// fixed and witness columns.
///
/// Returns the relative pil file name and the compilation result if any compilation was done.
pub fn compile_asm_string<T: FieldElement>(
pub fn compile_asm_string_to_analyzed_ast<T: FieldElement>(
file_name: &str,
contents: &str,
inputs: Vec<T>,
output_dir: &Path,
force_overwrite: bool,
prove_with: Option<BackendType>,
external_witness_values: Vec<(&str, Vec<T>)>,
) -> Result<(PathBuf, Option<CompilationResult<T>>), Vec<String>> {
monitor: &mut DiffMonitor,
) -> Result<AnalysisASMFile<T>, Vec<String>> {
let parsed = parser::parse_asm(Some(file_name), contents).unwrap_or_else(|err| {
eprintln!("Error parsing .asm file:");
err.output_to_stderr();
Expand All @@ -154,11 +150,26 @@ pub fn compile_asm_string<T: FieldElement>(
let resolved =
importer::resolve(Some(PathBuf::from(file_name)), parsed).map_err(|e| vec![e])?;
log::debug!("Run analysis");
let analysed = analyze(resolved).unwrap();
let analyzed = analyze(resolved, monitor)?;
log::debug!("Analysis done");
log::trace!("{analysed}");
log::trace!("{analyzed}");

Ok(analyzed)
}

pub fn convert_analyzed_to_pil<T: FieldElement>(
file_name: &str,
monitor: &mut DiffMonitor,
analyzed: AnalysisASMFile<T>,
inputs: &[T],
output_dir: &Path,
force_overwrite: bool,
prove_with: Option<BackendType>,
external_witness_values: Vec<(&str, Vec<T>)>,
) -> Result<(PathBuf, Option<CompilationResult<T>>), Vec<String>> {
let constraints = convert_analyzed_to_pil_constraints(analyzed, monitor);
log::debug!("Run airgen");
let graph = airgen::compile(analysed);
let graph = airgen::compile(constraints);
log::debug!("Airgen done");
log::trace!("{graph}");
log::debug!("Run linker");
Expand Down Expand Up @@ -196,6 +207,37 @@ pub fn compile_asm_string<T: FieldElement>(
))
}

/// Compiles the contents of a .asm file, outputs the PIL on stdout and tries to generate
/// fixed and witness columns.
///
/// Returns the relative pil file name and the compilation result if any compilation was done.
pub fn compile_asm_string<T: FieldElement>(
file_name: &str,
contents: &str,
inputs: &[T],
analyzed_hook: Option<&mut dyn FnMut(&AnalysisASMFile<T>)>,
output_dir: &Path,
force_overwrite: bool,
prove_with: Option<BackendType>,
external_witness_values: Vec<(&str, Vec<T>)>,
) -> Result<(PathBuf, Option<CompilationResult<T>>), Vec<String>> {
let mut monitor = DiffMonitor::default();
let analyzed = compile_asm_string_to_analyzed_ast(file_name, contents, &mut monitor)?;
if let Some(hook) = analyzed_hook {
hook(&analyzed);
};
convert_analyzed_to_pil(
file_name,
&mut monitor,
analyzed,
inputs,
output_dir,
force_overwrite,
prove_with,
external_witness_values,
)
}

pub struct CompilationResult<T: FieldElement> {
/// Constant columns, potentially incomplete (if success is false)
pub constants: Vec<(String, Vec<T>)>,
Expand Down Expand Up @@ -336,7 +378,9 @@ fn write_commits_to_fs<T: FieldElement>(
}

#[allow(clippy::print_stdout)]
pub fn inputs_to_query_callback<T: FieldElement>(inputs: Vec<T>) -> impl Fn(&str) -> Option<T> {
pub fn inputs_to_query_callback<'a, T: FieldElement>(
inputs: &'a [T],
) -> impl Fn(&str) -> Option<T> + 'a {
move |query: &str| -> Option<T> {
let items = query.split(',').map(|s| s.trim()).collect::<Vec<_>>();
match items[0] {
Expand Down
3 changes: 2 additions & 1 deletion compiler/src/verify.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,8 @@ pub fn verify_asm_string<T: FieldElement>(file_name: &str, contents: &str, input
compile_asm_string(
file_name,
contents,
inputs,
&inputs,
None,
&temp_dir,
true,
Some(BackendType::PilStarkCli),
Expand Down
4 changes: 2 additions & 2 deletions halo2/src/mock_prover.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ pub fn mock_prove<T: FieldElement>(
mod test {
use std::{fs, path::PathBuf};

use analysis::analyze;
use analysis::convert_asm_to_pil;
use number::Bn254Field;
use parser::parse_asm;
use test_log::test;
Expand All @@ -53,7 +53,7 @@ mod test {
let contents = fs::read_to_string(&location).unwrap();
let parsed = parse_asm::<Bn254Field>(Some(&location), &contents).unwrap();
let resolved = importer::resolve(Some(PathBuf::from(location)), parsed).unwrap();
let analysed = analyze(resolved).unwrap();
let analysed = convert_asm_to_pil(resolved).unwrap();
let graph = airgen::compile(analysed);
let pil = linker::link(graph).unwrap();

Expand Down
4 changes: 2 additions & 2 deletions linker/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -151,7 +151,7 @@ mod test {
};
use number::{Bn254Field, FieldElement, GoldilocksField};

use analysis::analyze;
use analysis::convert_asm_to_pil;
use parser::parse_asm;

use pretty_assertions::assert_eq;
Expand All @@ -161,7 +161,7 @@ mod test {
fn parse_analyse_and_compile<T: FieldElement>(input: &str) -> PILGraph<T> {
let parsed = parse_asm(None, input).unwrap();
let resolved = importer::resolve(None, parsed).unwrap();
airgen::compile(analyze(resolved).unwrap())
airgen::compile(convert_asm_to_pil(resolved).unwrap())
}

#[test]
Expand Down
4 changes: 3 additions & 1 deletion parser/src/powdr.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -333,6 +333,8 @@ DebugDirectiveStatement: FunctionStatement<T> = {
=> FunctionStatement::DebugDirective(l, DebugDirective::File(n.try_into().unwrap(), d, f)),
<l:@L> "debug" "loc" <f:Integer> <line:Integer> <col:Integer> ";"
=> FunctionStatement::DebugDirective(l, DebugDirective::Loc(f.try_into().unwrap(), line.try_into().unwrap(), col.try_into().unwrap())),
<l:@L> "debug" "insn" <insn:StringLiteral> ";"
=> FunctionStatement::DebugDirective(l, DebugDirective::OriginalInstruction(insn)),
}

LabelStatement: FunctionStatement<T> = {
Expand Down Expand Up @@ -549,4 +551,4 @@ FieldElement: T = {
Integer: AbstractNumberType = {
r"[0-9][0-9_]*" => AbstractNumberType::from_str(&<>.replace('_', "")).unwrap(),
r"0x[0-9A-Fa-f][0-9A-Fa-f_]*" => AbstractNumberType::from_str_radix(&<>[2..].replace('_', ""), 16).unwrap(),
}
}
3 changes: 2 additions & 1 deletion powdr_cli/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ version = "0.1.0"
edition = "2021"

[features]
default = [] # halo2 is disabled by default
default = [] # halo2 is disabled by default
halo2 = ["dep:halo2", "backend/halo2", "compiler/halo2"]

[dependencies]
Expand All @@ -14,6 +14,7 @@ log = "0.4.17"
compiler = { path = "../compiler" }
parser = { path = "../parser" }
riscv = { path = "../riscv" }
riscv_executor = { path = "../riscv_executor" }
number = { path = "../number" }
halo2 = { path = "../halo2", optional = true }
backend = { path = "../backend" }
Expand Down
Loading

0 comments on commit a0df34f

Please sign in to comment.