Skip to content

Commit

Permalink
feat: Detect subgraphs that are completely independent from inputs or…
Browse files Browse the repository at this point in the history
… outputs (#5402)

# Description

## Problem\*

Currently a developer can create a circuit that would use unconstrained
values in such a way, that a part of the circuit becomes completely
disconnected from the circuit inputs or outputs, making this part
completely useless as it can be taken out of any proof. This PR
introduces an Ssa pass that informs the user of this issue.

## Summary\*

An Ssa pass that detects some underconstraining issues

![image](https://github.com/noir-lang/noir/assets/4798775/cb5849d2-715b-4a6c-9947-575c2938f37a)


## Additional Context



## Documentation\*

Check one:
- [x] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[For Experimental Features]** Documentation to be submitted in a
separate PR.

# PR Checklist\*

- [x] I have tested the changes locally.
- [x] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.
  • Loading branch information
Rumata888 authored Jul 5, 2024
1 parent 688448f commit 7ea83a9
Show file tree
Hide file tree
Showing 7 changed files with 475 additions and 6 deletions.
26 changes: 24 additions & 2 deletions compiler/noirc_errors/src/reporter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ pub struct CustomDiagnostic {
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
pub enum DiagnosticKind {
Error,
Bug,
Warning,
}

Expand Down Expand Up @@ -62,6 +63,19 @@ impl CustomDiagnostic {
}
}

pub fn simple_bug(
primary_message: String,
secondary_message: String,
secondary_span: Span,
) -> CustomDiagnostic {
CustomDiagnostic {
message: primary_message,
secondaries: vec![CustomLabel::new(secondary_message, secondary_span)],
notes: Vec::new(),
kind: DiagnosticKind::Bug,
}
}

pub fn in_file(self, file_id: fm::FileId) -> FileDiagnostic {
FileDiagnostic::new(file_id, self)
}
Expand All @@ -81,6 +95,10 @@ impl CustomDiagnostic {
pub fn is_warning(&self) -> bool {
matches!(self.kind, DiagnosticKind::Warning)
}

pub fn is_bug(&self) -> bool {
matches!(self.kind, DiagnosticKind::Bug)
}
}

impl std::fmt::Display for CustomDiagnostic {
Expand Down Expand Up @@ -120,10 +138,13 @@ pub fn report_all<'files>(
silence_warnings: bool,
) -> ReportedErrors {
// Report warnings before any errors
let (warnings, mut errors): (Vec<_>, _) =
diagnostics.iter().partition(|item| item.diagnostic.is_warning());
let (warnings_and_bugs, mut errors): (Vec<_>, _) =
diagnostics.iter().partition(|item| !item.diagnostic.is_error());

let (warnings, mut bugs): (Vec<_>, _) =
warnings_and_bugs.iter().partition(|item| item.diagnostic.is_warning());
let mut diagnostics = if silence_warnings { Vec::new() } else { warnings };
diagnostics.append(&mut bugs);
diagnostics.append(&mut errors);

let error_count =
Expand Down Expand Up @@ -170,6 +191,7 @@ fn convert_diagnostic(
) -> Diagnostic<fm::FileId> {
let diagnostic = match (cd.kind, deny_warnings) {
(DiagnosticKind::Warning, false) => Diagnostic::warning(),
(DiagnosticKind::Bug, ..) => Diagnostic::bug(),
_ => Diagnostic::error(),
};

Expand Down
20 changes: 20 additions & 0 deletions compiler/noirc_evaluator/src/errors.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ pub enum RuntimeError {
#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum SsaReport {
Warning(InternalWarning),
Bug(InternalBug),
}

impl From<SsaReport> for FileDiagnostic {
Expand All @@ -78,6 +79,19 @@ impl From<SsaReport> for FileDiagnostic {
Diagnostic::simple_warning(message, secondary_message, location.span);
diagnostic.in_file(file_id).with_call_stack(call_stack)
}
SsaReport::Bug(bug) => {
let message = bug.to_string();
let (secondary_message, call_stack) = match bug {
InternalBug::IndependentSubgraph { call_stack } => {
("There is no path from the output of this brillig call to either return values or inputs of the circuit, which creates an independent subgraph. This is quite likely a soundness vulnerability".to_string(),call_stack)
}
};
let call_stack = vecmap(call_stack, |location| location);
let file_id = call_stack.last().map(|location| location.file).unwrap_or_default();
let location = call_stack.last().expect("Expected RuntimeError to have a location");
let diagnostic = Diagnostic::simple_bug(message, secondary_message, location.span);
diagnostic.in_file(file_id).with_call_stack(call_stack)
}
}
}
}
Expand All @@ -90,6 +104,12 @@ pub enum InternalWarning {
VerifyProof { call_stack: CallStack },
}

#[derive(Debug, PartialEq, Eq, Clone, Error, Serialize, Deserialize)]
pub enum InternalBug {
#[error("Input to brillig function is in a separate subgraph to output")]
IndependentSubgraph { call_stack: CallStack },
}

#[derive(Debug, PartialEq, Eq, Clone, Error)]
pub enum InternalError {
#[error("ICE: Both expressions should have degree<=1")]
Expand Down
20 changes: 16 additions & 4 deletions compiler/noirc_evaluator/src/ssa.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,8 @@ pub mod ir;
mod opt;
pub mod ssa_gen;

pub(crate) struct ArtifactsAndWarnings(Artifacts, Vec<SsaReport>);

/// Optimize the given program by converting it into SSA
/// form and performing optimizations there. When finished,
/// convert the final SSA into an ACIR program and return it.
Expand All @@ -49,10 +51,10 @@ pub mod ssa_gen;
pub(crate) fn optimize_into_acir(
program: Program,
options: &SsaEvaluatorOptions,
) -> Result<Artifacts, RuntimeError> {
) -> Result<ArtifactsAndWarnings, RuntimeError> {
let ssa_gen_span = span!(Level::TRACE, "ssa_generation");
let ssa_gen_span_guard = ssa_gen_span.enter();
let ssa = SsaBuilder::new(
let mut ssa = SsaBuilder::new(
program,
options.enable_ssa_logging,
options.force_brillig_output,
Expand Down Expand Up @@ -89,13 +91,15 @@ pub(crate) fn optimize_into_acir(
.run_pass(Ssa::array_set_optimization, "After Array Set Optimizations:")
.finish();

let ssa_level_warnings = ssa.check_for_underconstrained_values();
let brillig = time("SSA to Brillig", options.print_codegen_timings, || {
ssa.to_brillig(options.enable_brillig_logging)
});

drop(ssa_gen_span_guard);

time("SSA to ACIR", options.print_codegen_timings, || ssa.into_acir(&brillig))
let artifacts = time("SSA to ACIR", options.print_codegen_timings, || ssa.into_acir(&brillig))?;
Ok(ArtifactsAndWarnings(artifacts, ssa_level_warnings))
}

// Helper to time SSA passes
Expand Down Expand Up @@ -149,6 +153,10 @@ impl SsaProgramArtifact {
}
self.names.push(circuit_artifact.name);
}

fn add_warnings(&mut self, mut warnings: Vec<SsaReport>) {
self.warnings.append(&mut warnings);
}
}

pub struct SsaEvaluatorOptions {
Expand Down Expand Up @@ -179,14 +187,18 @@ pub fn create_program(
let func_sigs = program.function_signatures.clone();

let recursive = program.recursive;
let (generated_acirs, generated_brillig, error_types) = optimize_into_acir(program, options)?;
let ArtifactsAndWarnings((generated_acirs, generated_brillig, error_types), ssa_level_warnings) =
optimize_into_acir(program, options)?;
assert_eq!(
generated_acirs.len(),
func_sigs.len(),
"The generated ACIRs should match the supplied function signatures"
);

let mut program_artifact = SsaProgramArtifact::new(generated_brillig, error_types);

// Add warnings collected at the Ssa stage
program_artifact.add_warnings(ssa_level_warnings);
// For setting up the ABI we need separately specify main's input and return witnesses
let mut is_main = true;
for (acir, func_sig) in generated_acirs.into_iter().zip(func_sigs) {
Expand Down
2 changes: 2 additions & 0 deletions compiler/noirc_evaluator/src/ssa/acir_gen/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -431,6 +431,8 @@ impl<'a> Context<'a> {
}

warnings.extend(return_warnings);

// Add the warnings from the alter Ssa passes
Ok(self.acir_context.finish(input_witness, return_witnesses, warnings))
}

Expand Down
Loading

0 comments on commit 7ea83a9

Please sign in to comment.