[cleanup] Remove old and unused mutation testing processor

third_party/move/move-prover/bytecode-pipeline/src/lib.rs

@@ -11,7 +11,6 @@ pub mod loop_analysis;
 pub mod memory_instrumentation;
 pub mod mono_analysis;
 pub mod mut_ref_instrumentation;
-pub mod mutation_tester;
 pub mod number_operation;
 pub mod number_operation_analysis;
 pub mod options;

third_party/move/move-prover/bytecode-pipeline/src/options.rs

@@ -52,16 +52,6 @@ pub struct ProverOptions {
     /// Whether to assume wellformedness when elements are read from memory, instead of on
     /// function entry.
     pub assume_wellformed_on_access: bool,
-    /// Indicates that we should do any mutations
-    pub mutation: bool,
-    /// Indicates that we should use the add-subtract mutation on the given block
-    pub mutation_add_sub: usize,
-    /// Indicates that we should use the subtract-add mutation on the given block
-    pub mutation_sub_add: usize,
-    /// Indicates that we should use the multiply-divide mutation on the given block
-    pub mutation_mul_div: usize,
-    /// Indicates that we should use the divide-multiply mutation on the given block
-    pub mutation_div_mul: usize,
     /// Whether to use the polymorphic boogie backend.
     pub boogie_poly: bool,
     /// Whether pack/unpack should recurse over the structure.
@@ -89,7 +79,7 @@ pub struct ProverOptions {
     /// Optional names of native methods (qualified with module name, e.g., m::foo) implementing
     /// mutable borrow semantics
     pub borrow_natives: Vec<String>,
-    /// Whether to ban convertion from int to bv at the boogie backend
+    /// Whether to ban conversion from int to bv at the boogie backend
     pub ban_int_2_bv: bool,
 }
 
@@ -106,11 +96,6 @@ impl Default for ProverOptions {
             verify_scope: VerificationScope::All,
             resource_wellformed_axiom: false,
             assume_wellformed_on_access: false,
-            mutation: false,
-            mutation_add_sub: 0,
-            mutation_sub_add: 0,
-            mutation_mul_div: 0,
-            mutation_div_mul: 0,
             boogie_poly: false,
             deep_pack_unpack: false,
             auto_trace_level: AutoTraceLevel::Off,

third_party/move/move-prover/bytecode-pipeline/src/pipeline_factory.rs

@@ -10,7 +10,7 @@ use crate::{
     global_invariant_instrumentation::GlobalInvariantInstrumentationProcessor,
     inconsistency_check::InconsistencyCheckInstrumenter, loop_analysis::LoopAnalysisProcessor,
     memory_instrumentation::MemoryInstrumentationProcessor, mono_analysis::MonoAnalysisProcessor,
-    mut_ref_instrumentation::MutRefInstrumenter, mutation_tester::MutationTester,
+    mut_ref_instrumentation::MutRefInstrumenter,
     number_operation_analysis::NumberOperationProcessor, options::ProverOptions,
     spec_instrumentation::SpecInstrumentationProcessor,
     verification_analysis::VerificationAnalysisProcessor,
@@ -56,11 +56,6 @@ pub fn default_pipeline_with_options(options: &ProverOptions) -> FunctionTargetP
         MonoAnalysisProcessor::new(),
     ]);
 
-    if options.mutation {
-        // pass which may do nothing
-        processors.push(MutationTester::new());
-    }
-
     // inconsistency check instrumentation should be the last one in the pipeline
     if options.check_inconsistency {
         processors.push(InconsistencyCheckInstrumenter::new());

third_party/move/move-prover/src/cli.rs

@@ -64,14 +64,14 @@ pub struct Options {
     /// The paths to the Move sources.
     /// Each source path should refer to either (1) a Move file or (2) a directory containing Move
     /// files, all to be compiled (e.g., not the root directory of a package---which contains
-    /// Move.toml---but a specific subdirectorysuch as `sources`, `scripts`, and/or `tests`,
+    /// Move.toml---but a specific subdirectory such as `sources`, `scripts`, and/or `tests`,
     /// depending on compilation mode).
     pub move_sources: Vec<String>,
     /// The paths to any dependencies for the Move sources. Those will not be verified but
     /// can be used by `move_sources`.
     /// Each move_dep path should refer to either (1) a Move file or (2) a directory containing
     /// Move files, all to be compiled (e.g., not the root directory of a package---which contains
-    /// Move.toml---but a specific subdirectorysuch as `sources`).
+    /// Move.toml---but a specific subdirectory such as `sources`).
     pub move_deps: Vec<String>,
     /// The values assigned to named addresses in the Move code being verified.
     pub move_named_address_values: Vec<String>,
@@ -368,54 +368,6 @@ impl Options {
                         "for benchmarking: how many times to call the backend on the verification problem",
                     ),
             )
-            .arg(
-                Arg::new("mutation")
-                    .long("mutation")
-                    .action(SetTrue)
-                    .help(
-                        "Specifies to use the mutation pass",
-                    ),
-            )
-            .arg(
-                Arg::new("mutation-add-sub")
-                    .long("mutation-add-sub")
-                    .value_name("COUNT")
-                    .value_parser(is_number)
-                    .help(
-                        "indicates that this program should mutate the indicated plus operation to a minus\
-                        specifically by modifyig the \"nth\" such operation",
-                    ),
-            )
-            .arg(
-                Arg::new("mutation-sub-add")
-                    .long("mutation-sub-add")
-                    .value_name("COUNT")
-                    .value_parser(is_number)
-                    .help(
-                        "indicates that this program should mutate the indicated minus operation to a plus\
-                        specifically by modifyig the \"nth\" such operation",
-                    ),
-            )
-            .arg(
-                Arg::new("mutation-mul-div")
-                    .long("mutation-mul-div")
-                    .value_name("COUNT")
-                    .value_parser(is_number)
-                    .help(
-                        "indicates that this program should mutate the indicated multiplication operation to a divide\
-                        specifically by modifyig the \"nth\" such operation",
-                    ),
-            )
-            .arg(
-                Arg::new("mutation-div-mul")
-                    .long("mutation-div-mul")
-                    .value_name("COUNT")
-                    .value_parser(is_number)
-                    .help(
-                        "indicates that this program should mutate the indicated divide operation to a multiplication\
-                        specifically by modifyig the \"nth\" such operation",
-                    ),
-            )
             .arg(
                 Arg::new("dependencies")
                     .long("dependency")
@@ -667,21 +619,6 @@ impl Options {
         {
             options.move_named_address_values = get_vec("named-addresses");
         }
-        if matches.get_flag("mutation") {
-            options.prover.mutation = true;
-        }
-        if matches.contains_id("mutation-add-sub") {
-            options.prover.mutation_add_sub = *matches.try_get_one("mutation-add-sub")?.unwrap();
-        }
-        if matches.contains_id("mutation-sub-add") {
-            options.prover.mutation_sub_add = *matches.try_get_one("mutation-sub-add")?.unwrap();
-        }
-        if matches.contains_id("mutation-mul-div") {
-            options.prover.mutation_mul_div = *matches.try_get_one("mutation-mul-div")?.unwrap();
-        }
-        if matches.contains_id("mutation-div-mul") {
-            options.prover.mutation_div_mul = *matches.try_get_one("mutation-div-mul")?.unwrap();
-        }
         if matches.contains_id("verify") {
             options.prover.verify_scope =
                 match matches.get_one::<String>("verify").unwrap().as_str() {