From da9990216c1768188d46b709ea1760d24e90c9a5 Mon Sep 17 00:00:00 2001 From: Aristotelis Papanis Date: Fri, 20 Dec 2024 13:43:54 +0200 Subject: [PATCH] chore(fv): Refactor fv optimizations Made a separate folder for formal verification related optimizations. Also renamed the optimization for inlining calls in fv attributes. --- compiler/noirc_evaluator/src/ssa.rs | 2 +- .../opt/{formal_verifications.rs => fv_opts/fv_inline_calls.rs} | 2 +- compiler/noirc_evaluator/src/ssa/opt/fv_opts/mod.rs | 2 ++ compiler/noirc_evaluator/src/ssa/opt/mod.rs | 2 +- 4 files changed, 5 insertions(+), 3 deletions(-) rename compiler/noirc_evaluator/src/ssa/opt/{formal_verifications.rs => fv_opts/fv_inline_calls.rs} (99%) create mode 100644 compiler/noirc_evaluator/src/ssa/opt/fv_opts/mod.rs diff --git a/compiler/noirc_evaluator/src/ssa.rs b/compiler/noirc_evaluator/src/ssa.rs index 80ec343a375..044241ae6de 100644 --- a/compiler/noirc_evaluator/src/ssa.rs +++ b/compiler/noirc_evaluator/src/ssa.rs @@ -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); diff --git a/compiler/noirc_evaluator/src/ssa/opt/formal_verifications.rs b/compiler/noirc_evaluator/src/ssa/opt/fv_opts/fv_inline_calls.rs similarity index 99% rename from compiler/noirc_evaluator/src/ssa/opt/formal_verifications.rs rename to compiler/noirc_evaluator/src/ssa/opt/fv_opts/fv_inline_calls.rs index 4d53e0f8170..ff3dac19ce3 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/formal_verifications.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/fv_opts/fv_inline_calls.rs @@ -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() { diff --git a/compiler/noirc_evaluator/src/ssa/opt/fv_opts/mod.rs b/compiler/noirc_evaluator/src/ssa/opt/fv_opts/mod.rs new file mode 100644 index 00000000000..343159a828f --- /dev/null +++ b/compiler/noirc_evaluator/src/ssa/opt/fv_opts/mod.rs @@ -0,0 +1,2 @@ +mod fv_inline_calls; +// mod fix_value_map; \ No newline at end of file diff --git a/compiler/noirc_evaluator/src/ssa/opt/mod.rs b/compiler/noirc_evaluator/src/ssa/opt/mod.rs index 48950078253..156df4f1309 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/mod.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/mod.rs @@ -21,4 +21,4 @@ mod resolve_is_unconstrained; mod runtime_separation; mod simplify_cfg; mod unrolling; -mod formal_verifications; +pub(crate) mod fv_opts;