tendermint_testgen/
apalache.rs

1use std::{fmt::Write as _, io};
2
3use serde::{Deserialize, Serialize};
4
5use crate::{command::*, tester::TestEnv};
6
7#[derive(Deserialize, Clone, Debug)]
8pub struct ApalacheTestBatch {
9    pub description: String,
10    pub model: String,
11    pub length: Option<u64>,
12    pub timeout: Option<u64>,
13    pub tests: Vec<String>,
14}
15
16#[derive(Serialize, Deserialize, Clone, Debug)]
17pub struct ApalacheTestCase {
18    pub model: String,
19    pub test: String,
20    pub length: Option<u64>,
21    pub timeout: Option<u64>,
22}
23
24pub enum ApalacheRun {
25    /// Apalache has found a counterexample
26    Counterexample(CommandRun),
27    /// Apalache has not found a counterexample up to specified length bound
28    NoCounterexample(CommandRun),
29    /// Apalache has found a deadlock
30    Deadlock(CommandRun),
31    /// Apalache model checking run failed (e.g. a parsing error)
32    ModelError(CommandRun),
33    /// Apalache returned an unknown error code
34    Unknown(CommandRun),
35    /// The tool has reached the specified timeout without producing an answer
36    Timeout(CommandRun),
37}
38
39impl ApalacheRun {
40    pub fn message(&self) -> &str {
41        match self {
42            ApalacheRun::Counterexample(_) => "Apalache has generated a counterexample",
43            ApalacheRun::NoCounterexample(_) => "Apalache failed to generate a counterexample; consider increasing the length bound, or changing your test",
44            ApalacheRun::Deadlock(_) => "Apalache has found a deadlock; please inspect your model and test",
45            ApalacheRun::ModelError(_) => "Apalache failed to process the model; please check it",
46            ApalacheRun::Unknown(_) => "Apalache has generated an unknown outcome; please contact Apalache developers",
47            ApalacheRun::Timeout(_) => "Apalache failed to generate a counterexample within given time; consider increasing the timeout, or changing your test",
48        }
49    }
50}
51
52pub fn run_apalache_test(dir: &str, test: ApalacheTestCase) -> io::Result<ApalacheRun> {
53    let inv = format!("{}Inv", test.test);
54
55    // Mutate the model: negate the test assertion to get the invariant to check
56    let mutation_failed = || {
57        io::Error::new(
58            io::ErrorKind::InvalidInput,
59            "failed to mutate the model and add invariant",
60        )
61    };
62    let env = TestEnv::new(dir).ok_or_else(mutation_failed)?;
63    let model = env.read_file(&test.model).unwrap();
64    let mut new_model = String::new();
65    for line in model.lines() {
66        if line.starts_with(&inv) {
67            // invariant already present; skip mutation
68            new_model.clear();
69            break;
70        }
71        if line.starts_with("======") {
72            let _ = writeln!(new_model, "{} == ~{}", inv, test.test);
73        }
74        new_model += line;
75        new_model += "\n";
76    }
77    if !new_model.is_empty() {
78        env.write_file(&test.model, &new_model)
79            .ok_or_else(mutation_failed)?;
80    }
81
82    // Run Apalache, and process the result
83    let mut cmd = Command::new();
84    if let Some(timeout) = test.timeout {
85        cmd.program("timeout");
86        cmd.arg(&timeout.to_string());
87        cmd.arg("apalache-mc");
88    } else {
89        cmd.program("apalache-mc");
90    }
91    cmd.arg("check");
92    cmd.arg_from_parts(vec!["--inv=", &inv]);
93    cmd.arg("--init=InitTest");
94    cmd.arg("--next=NextTest");
95    if let Some(length) = test.length {
96        cmd.arg_from_parts(vec!["--length=", &length.to_string()]);
97    }
98    cmd.arg(&test.model);
99    if !dir.is_empty() {
100        cmd.current_dir(dir);
101    }
102    match cmd.spawn() {
103        Ok(run) => {
104            if run.status.success() {
105                if run.stdout.contains("The outcome is: NoError") {
106                    Ok(ApalacheRun::NoCounterexample(run))
107                } else if run.stdout.contains("The outcome is: Error") {
108                    Ok(ApalacheRun::Counterexample(run))
109                } else if run.stdout.contains("The outcome is: Deadlock") {
110                    Ok(ApalacheRun::Deadlock(run))
111                } else {
112                    Ok(ApalacheRun::Unknown(run))
113                }
114            } else if let Some(code) = run.status.code() {
115                match code {
116                    99 => Ok(ApalacheRun::ModelError(run)),
117                    124 => Ok(ApalacheRun::Timeout(run)),
118                    _ => Ok(ApalacheRun::Unknown(run)),
119                }
120            } else {
121                Ok(ApalacheRun::Timeout(run))
122            }
123        },
124        Err(e) => Err(e),
125    }
126}
tendermint_testgen/apalache.rs

tendermint_testgen/
apalache.rs
