Remove graph printing

Author: Patrick-6

genmc-sys/src/lib.rs

@@ -269,7 +269,6 @@ mod ffi {
         /// If there are more executions, this method prepares for the next execution and returns `true`.
         fn isExplorationDone(self: Pin<&mut MiriGenMCShim>) -> bool;
 
-        fn printGraph(self: Pin<&mut MiriGenMCShim>);
         fn printEstimationResults(self: &MiriGenMCShim, elapsed_time_sec: f64);
     }
 }

genmc-sys/src_cpp/MiriInterface.hpp

@@ -113,8 +113,6 @@ struct MiriGenMCShim : private GenMCDriver {
 		return --globalInstructions[tid].event;
 	}
 
-	void printGraph() { GenMCDriver::debugPrintGraph(); }
-
 	void printEstimationResults(const double elapsed_time_sec) const
 	{
 		// TODO GENMC(CLEANUP): should this happen on the Rust side?

src/bin/miri.rs

@@ -194,7 +194,6 @@ impl rustc_driver::Callbacks for MiriCompilerCalls {
             if genmc_config.do_estimation()
                 && miri_genmc::run_genmc_mode(
                     &config,
-                    genmc_config,
                     eval_entry_once,
                     miri_genmc::Mode::Estimation,
                 )
@@ -205,7 +204,6 @@ impl rustc_driver::Callbacks for MiriCompilerCalls {
 
             let return_code = miri_genmc::run_genmc_mode(
                 &config,
-                genmc_config,
                 eval_entry_once,
                 miri_genmc::Mode::Verification,
             )

src/concurrency/genmc/config.rs

@@ -6,7 +6,6 @@ use super::GenmcParams;
 #[derive(Debug, Default, Clone)]
 pub struct GenmcConfig {
     pub(super) params: GenmcParams,
-    print_exec_graphs: bool,
     do_estimation: bool,
 }
 
@@ -16,10 +15,6 @@ impl GenmcConfig {
         self.params.log_level_trace = true;
     }
 
-    pub fn print_exec_graphs(&self) -> bool {
-        self.print_exec_graphs
-    }
-
     pub fn do_estimation(&self) -> bool {
         self.do_estimation
     }
@@ -49,9 +44,6 @@ impl GenmcConfig {
         if trimmed_arg == "log-trace" {
             // TODO GENMC: maybe expand to allow more control over log level?
             genmc_config.set_log_level_trace();
-        } else if trimmed_arg == "print-graphs" {
-            // TODO GENMC (DOCUMENTATION)
-            genmc_config.print_exec_graphs = true;
         } else if trimmed_arg == "estimate" {
             // TODO GENMC (DOCUMENTATION): naming, off/on by default?
             genmc_config.do_estimation = true;

src/concurrency/genmc/dummy.rs

@@ -51,10 +51,6 @@ impl GenmcCtx {
         unreachable!()
     }
 
-    pub fn print_genmc_graph(&self) {
-        unreachable!()
-    }
-
     pub fn is_exploration_done(&self) -> bool {
         unreachable!()
     }
@@ -272,10 +268,6 @@ impl GenmcConfig {
         }
     }
 
-    pub fn print_exec_graphs(&self) -> bool {
-        unreachable!()
-    }
-
     pub fn do_estimation(&self) -> bool {
         unreachable!()
     }

src/concurrency/genmc/miri_genmc.rs

@@ -2,7 +2,7 @@ use std::fmt::Display;
 use std::rc::Rc;
 use std::time::Instant;
 
-use crate::{GenmcConfig, GenmcCtx, MiriConfig};
+use crate::{GenmcCtx, MiriConfig};
 
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub enum Mode {
@@ -21,7 +21,6 @@ impl Display for Mode {
 
 pub fn run_genmc_mode(
     config: &MiriConfig,
-    genmc_config: &GenmcConfig,
     eval_entry: impl Fn(Rc<GenmcCtx>) -> Option<i32>,
     mode: Mode,
 ) -> Option<i32> {
@@ -32,10 +31,6 @@ pub fn run_genmc_mode(
         tracing::info!("Miri-GenMC loop {}", rep + 1);
         let result = eval_entry(genmc_ctx.clone());
 
-        if genmc_config.print_exec_graphs() {
-            genmc_ctx.print_genmc_graph();
-        }
-
         // TODO GENMC (ERROR REPORTING): we currently do this here, so we can still print the GenMC graph above
         let return_code = result?;
 

src/concurrency/genmc/mod.rs

@@ -99,13 +99,6 @@ impl GenmcCtx {
         mc.as_ref().getExploredExecutionCount()
     }
 
-    pub fn print_genmc_graph(&self) {
-        info!("GenMC: print the Execution graph");
-        let mut mc = self.handle.borrow_mut();
-        let pinned_mc = mc.as_mut();
-        pinned_mc.printGraph();
-    }
-
     /// This function determines if we should continue exploring executions or if we are done.
     ///
     /// In GenMC mode, the input program should be repeatedly executed until this function returns `true` or an error is found.