mc: add support for storm timeouts and mem limits

Author: Philipp15b

src/main.rs

@@ -11,6 +11,7 @@ use std::{
     path::PathBuf,
     process::ExitCode,
     sync::{Arc, Mutex},
+    time::{Duration, Instant},
 };
 
 use crate::{
@@ -29,7 +30,7 @@ use intrinsic::{annotations::init_calculi, distributions::init_distributions, li
 use mc::run_storm::{run_storm, storm_result_to_diagnostic};
 use proof_rules::init_encodings;
 use regex::Regex;
-use resource_limits::{await_with_resource_limits, LimitError, LimitsRef};
+use resource_limits::{await_with_resource_limits, LimitError, LimitsRef, MemorySize};
 use servers::{run_lsp_server, CliServer, LspServer, Server, ServerError};
 use slicing::init_slicing;
 use thiserror::Error;
@@ -183,7 +184,17 @@ pub struct ResourceLimitOptions {
 
     /// Memory usage limit in megabytes.
     #[arg(long = "mem", default_value = "8192")]
-    pub mem_limit: u64,
+    pub mem_limit: usize,
+}
+
+impl ResourceLimitOptions {
+    fn timeout(&self) -> Duration {
+        Duration::from_secs(self.timeout)
+    }
+
+    fn mem_limit(&self) -> MemorySize {
+        MemorySize::megabytes(self.mem_limit)
+    }
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, ValueEnum)]
@@ -239,6 +250,19 @@ pub struct JaniOptions {
     /// for constants in the model.
     #[arg(long)]
     pub storm_constants: Option<String>,
+
+    /// Timeout in seconds for running Storm.
+    ///
+    /// Caesar uses the minimum of this value and the remaining time from the
+    /// `--timeout` option.
+    #[arg(long)]
+    pub storm_timeout: Option<u64>,
+}
+
+impl JaniOptions {
+    pub fn storm_timeout(&self) -> Option<Duration> {
+        self.storm_timeout.map(Duration::from_secs)
+    }
 }
 
 #[derive(Debug, Default, Args)]
@@ -454,7 +478,7 @@ fn finalize_verify_result(
     rlimit_options: &ResourceLimitOptions,
     verify_result: Result<bool, VerifyError>,
 ) -> ExitCode {
-    let (timeout, mem_limit) = (rlimit_options.timeout, rlimit_options.mem_limit);
+    let (timeout, mem_limit) = (rlimit_options.timeout(), rlimit_options.mem_limit());
     match verify_result {
         #[allow(clippy::bool_to_int_with_if)]
         Ok(all_verified) => ExitCode::from(if all_verified { 0 } else { 1 }),
@@ -467,11 +491,14 @@ fn finalize_verify_result(
             ExitCode::from(1)
         }
         Err(VerifyError::LimitError(LimitError::Timeout)) => {
-            tracing::error!("Timed out after {} seconds, exiting.", timeout);
+            tracing::error!("Timed out after {} seconds, exiting.", timeout.as_secs());
             std::process::exit(2); // exit ASAP
         }
         Err(VerifyError::LimitError(LimitError::Oom)) => {
-            tracing::error!("Exhausted {} megabytes of memory, exiting.", mem_limit);
+            tracing::error!(
+                "Exhausted {} megabytes of memory, exiting.",
+                mem_limit.as_megabytes()
+            );
             std::process::exit(3); // exit ASAP
         }
         Err(VerifyError::UserError(err)) => {
@@ -587,8 +614,8 @@ pub async fn verify_files(
     };
     // Unpacking lots of Results with `.await??` :-)
     await_with_resource_limits(
-        Some(options.rlimit_options.timeout),
-        Some(options.rlimit_options.mem_limit),
+        Some(options.rlimit_options.timeout()),
+        Some(options.rlimit_options.mem_limit()),
         handle,
     )
     .await??
@@ -671,7 +698,7 @@ pub(crate) fn verify_test(source: &str) -> (Result<bool, VerifyError>, servers::
         .id;
 
     let options = Arc::new(options);
-    let limits_ref = LimitsRef::new(None);
+    let limits_ref = LimitsRef::new(None, None);
     let res = verify_files_main(&options, limits_ref, &mut server, &[file_id]);
     (res, server)
 }
@@ -756,6 +783,7 @@ fn verify_files_main(
         &options.jani_options,
         &mut source_units,
         server,
+        &limits_ref,
         &tcx,
         false,
     )?;
@@ -942,10 +970,14 @@ fn to_jani_loader(
         &mut *server_lock,
         &user_files,
     )?;
+    let timeout = Instant::now() + options.rlimit_options.timeout();
+    let mem_limit = options.rlimit_options.mem_limit();
+    let limits_ref = LimitsRef::new(Some(timeout), Some(mem_limit));
     to_jani_main(
         &options.jani_options,
         &mut source_units,
         server_lock.deref_mut(),
+        &limits_ref,
         &tcx,
         true,
     )
@@ -955,6 +987,7 @@ fn to_jani_main(
     options: &JaniOptions,
     source_units: &mut Vec<Item<SourceUnit>>,
     server: &mut dyn Server,
+    limits_ref: &LimitsRef,
     tcx: &TyCtx,
     is_jani_command: bool,
 ) -> Result<(), VerifyError> {
@@ -985,8 +1018,8 @@ fn to_jani_main(
             Err(err) => Err(err)?,
             Ok(Some(path)) => {
                 tracing::debug!(file=?path.display(), "wrote JANI file");
-                if let Some(which_storm) = options.run_storm {
-                    let res = run_storm(&options, which_storm, &path, vec!["reward".to_owned()]);
+                if options.run_storm.is_some() {
+                    let res = run_storm(&options, &path, vec!["reward".to_owned()], limits_ref);
                     server.add_diagnostic(storm_result_to_diagnostic(
                         &res,
                         source_unit.diagnostic_span(),

src/mc/mod.rs

@@ -216,7 +216,7 @@ pub fn proc_to_model(
 
 fn check_calculus_annotation(proc: &ProcDecl) -> Result<(), JaniConversionError> {
     if let Some(calculus) = proc.calculus {
-        if &calculus.name != "wp" || &calculus.name != "ert"
+        if &calculus.name != "wp" && &calculus.name != "ert"
         // yeah that's ugly
         {
             return Err(JaniConversionError::UnsupportedCalculus {

src/mc/run_storm.rs

@@ -4,17 +4,20 @@ use std::{
     io,
     path::Path,
     process::{Command, ExitStatus},
+    time::Duration,
 };
 
 use ariadne::ReportKind;
 use indexmap::IndexMap;
 use lsp_types::NumberOrString;
 use num::BigRational;
+use regex::Regex;
 use thiserror::Error;
 use z3rro::util::PrettyRational;
 
 use crate::{
     ast::{Diagnostic, Label, Span},
+    resource_limits::LimitsRef,
     JaniOptions, RunWhichStorm,
 };
 
@@ -62,23 +65,35 @@ pub enum StormError {
     Io(#[from] io::Error),
     #[error("{0}: {1}")]
     StormFailed(ExitStatus, String),
+    #[error("State exploration aborted after {} seconds, explored {} states", .0.as_secs(), .1)]
+    StateExplorationAborted(Duration, usize),
     #[error("Docker is not running")]
     DockerNotRunning,
 }
 
 /// Run Storm on the given JANI file and look for output for the given properties.
+///
+/// Panics if `options.run_storm` is `None`.
 pub fn run_storm(
     options: &JaniOptions,
-    option: RunWhichStorm,
     mut jani_file: &Path,
     properties: Vec<String>,
+    limits_ref: &LimitsRef,
 ) -> Result<StormOutput, StormError> {
-    let mut command = match option {
-        RunWhichStorm::Path => Command::new("storm"),
+    let which_storm = options.run_storm.unwrap();
+    let mut command = match which_storm {
+        RunWhichStorm::Path => {
+            if limits_ref.memory_limit().is_some() {
+                tracing::debug!("Memory limit is ignored when running Storm from path");
+            }
+
+            Command::new("storm")
+        }
         RunWhichStorm::DockerStable | RunWhichStorm::DockerCI => {
             let mut command = Command::new("docker");
             let jani_file_dir = jani_file.parent().unwrap().canonicalize().unwrap();
-            let image_name = match option {
+            jani_file = jani_file.file_name().unwrap().as_ref();
+            let image_name = match which_storm {
                 RunWhichStorm::DockerStable => "movesrwth/storm:stable",
                 RunWhichStorm::DockerCI => "movesrwth/storm:ci",
                 _ => unreachable!(),
@@ -89,14 +104,29 @@ pub fn run_storm(
                 .arg("-v")
                 .arg(format!("{}:/mnt", jani_file_dir.display()))
                 .arg("-w")
-                .arg("/mnt")
-                .arg(image_name)
-                .arg("storm");
-            jani_file = jani_file.file_name().unwrap().as_ref();
+                .arg("/mnt");
+
+            if let Some(mem_limit) = limits_ref.memory_limit() {
+                command
+                    .arg("--memory")
+                    .arg(format!("{}m", mem_limit.as_megabytes()));
+            }
+
+            command.arg(image_name).arg("storm");
             command
         }
     };
 
+    let caesar_timeout = limits_ref.time_left();
+    let storm_specific_timeout = options.storm_timeout();
+    let timeout = caesar_timeout
+        .and_then(|ct| storm_specific_timeout.map(|st| ct.min(st)))
+        .or(caesar_timeout)
+        .or(storm_specific_timeout);
+    if let Some(timeout) = timeout {
+        command.arg("--timeout").arg(timeout.as_secs().to_string());
+    }
+
     if options.storm_exact {
         command.arg("--exact");
     }
@@ -125,7 +155,7 @@ pub fn run_storm(
     if !output.status.success() {
         if output.status.code() == Some(125)
             && matches!(
-                option,
+                which_storm,
                 RunWhichStorm::DockerStable | RunWhichStorm::DockerCI
             )
         {
@@ -142,6 +172,17 @@ pub fn run_storm(
                     .collect(),
             });
         }
+
+        let re = Regex::new(r"Explored (\d+) states in (\d+) seconds before abort").unwrap();
+        if let Some(captures) = re.captures(&output_str) {
+            let states_explored: usize = captures[1].parse().unwrap();
+            let time_taken: u64 = captures[2].parse().unwrap();
+            return Err(StormError::StateExplorationAborted(
+                Duration::from_secs(time_taken),
+                states_explored,
+            ));
+        }
+
         Err(StormError::StormFailed(output.status, output_str))
     } else {
         let results = parse_property_results(options, properties, &output_str);