Skip to content

Commit

Permalink
chore(fv): Refactor fv optimizations
Browse files Browse the repository at this point in the history
Made a separate folder for formal verification related optimizations.
Also renamed the optimization for inlining calls in fv attributes.
  • Loading branch information
Aristotelis2002 committed Jan 6, 2025
1 parent a73cd6a commit da99902
Show file tree
Hide file tree
Showing 4 changed files with 5 additions and 3 deletions.
2 changes: 1 addition & 1 deletion compiler/noirc_evaluator/src/ssa.rs
Original file line number Diff line number Diff line change
Expand Up @@ -261,7 +261,7 @@ pub(crate) fn optimize_into_verus_vir(
.run_pass(Ssa::fold_constants_using_constraints, "After Constraint Folding:")
.run_pass(Ssa::dead_instruction_elimination, "After Dead Instruction Elimination:")
.run_pass(Ssa::array_set_optimization, "After Array Set Optimizations:")
.run_pass(Ssa::formal_verifications_optimization, "After Formal Verification Optimizations:")
.run_pass(Ssa::inline_calls_in_attributes, "After Inlining Calls in attributes:")
.finish();

drop(ssa_gen_span_guard);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ struct RightShiftInfo {
}

impl Ssa {
pub(crate) fn formal_verifications_optimization(mut self) -> Self {
pub(crate) fn inline_calls_in_attributes(mut self) -> Self {
// There is a loop bound to avoid infinite run.
for _ in 0..1000 {
if !self.has_call_instruction() {
Expand Down
2 changes: 2 additions & 0 deletions compiler/noirc_evaluator/src/ssa/opt/fv_opts/mod.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
mod fv_inline_calls;
// mod fix_value_map;
2 changes: 1 addition & 1 deletion compiler/noirc_evaluator/src/ssa/opt/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,4 +21,4 @@ mod resolve_is_unconstrained;
mod runtime_separation;
mod simplify_cfg;
mod unrolling;
mod formal_verifications;
pub(crate) mod fv_opts;

0 comments on commit da99902

Please sign in to comment.