-
Notifications
You must be signed in to change notification settings - Fork 224
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* #414: testgen tester -- utilities to run multiple tests with logs and reports * 14: add testgen commands, in particular to call apalache and jsonatr * #547 add missing file updates from #529 * fix merge typo * remove ref to time: it's in another PR * fix clippy warning * TestEnv: change path parameters into AsRef<Path> * change TestEnv::full_path to return PathBuf * apply simplifications suggested by Romain * apply simplification from Romain * account for WOW Romain's suggestion on RefUnwindSafe * address Romain's suggestion on TestEnv::cleanup * cargo clippy * update CHANGELOG.md * addressed Romains's suggestions
- Loading branch information
1 parent
26ec803
commit 598a72a
Showing
8 changed files
with
509 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,150 @@ | ||
{ | ||
"description": "Transformers for Apalache counterexamples (CEs) with Tendermint blockchains", | ||
"use": [ | ||
"tendermint.json" | ||
], | ||
"input": [ | ||
{ | ||
"name": "first_state", | ||
"description": "extract the first state from Apalache CE", | ||
"kind": "INLINE", | ||
"source": "$.declarations[1].body.and | unwrap" | ||
}, | ||
{ | ||
"name": "last_state", | ||
"description": "extract the last state from Apalache CE", | ||
"kind": "INLINE", | ||
"source": "$.declarations[-2].body.and | unwrap" | ||
}, | ||
{ | ||
"name": "history", | ||
"description": "extract the history from the last state of Apalache CE", | ||
"kind": "INLINE", | ||
"source": "$last_state..[?(@.eq == 'history')].arg.atat..arg.record" | ||
}, | ||
{ | ||
"name": "states", | ||
"description": "extract all state from Apalache CE", | ||
"kind": "INLINE", | ||
"source": "$.declarations[1:-1].body.and" | ||
}, | ||
{ | ||
"name": "lightblock_commits", | ||
"description": "extract commits from a LightClient block of Apalache CE", | ||
"kind": "INLINE", | ||
"source": "$..[?(@.key.str == 'Commits')].value..str" | ||
}, | ||
{ | ||
"name": "block_validators", | ||
"description": "extract validators from a block of Apalache CE", | ||
"kind": "INLINE", | ||
"source": "$..[?(@.key.str == 'VS')].value..str" | ||
}, | ||
{ | ||
"name": "block_next_validators", | ||
"description": "extract next validators from a block of Apalache CE", | ||
"kind": "INLINE", | ||
"source": "$..[?(@.key.str == 'NextVS')].value..str" | ||
}, | ||
{ | ||
"name": "block_height", | ||
"description": "extract height from a block of Apalache CE", | ||
"kind": "INLINE", | ||
"source": "$..[?(@.key.str == 'height')].value | unwrap" | ||
}, | ||
{ | ||
"name": "block_time", | ||
"description": "extract time from a block of Apalache CE", | ||
"kind": "INLINE", | ||
"source": "$..[?(@.key.str == 'time')].value | unwrap" | ||
}, | ||
{ | ||
"name": "id_to_validator", | ||
"description": "transform an identifier into a validator expected by `tendermint-testgen validator`", | ||
"kind": "INLINE", | ||
"source": { | ||
"id": "$", | ||
"voting_power": 50 | ||
} | ||
}, | ||
{ | ||
"name": "id_to_vote", | ||
"description": "transform an identifier into a vote expected by `tendermint-testgen vote`", | ||
"kind": "INLINE", | ||
"source": { | ||
"validator": "$ | id_to_validator", | ||
"header": "$header" | ||
} | ||
}, | ||
{ | ||
"name": "block_to_header", | ||
"description": "transform a block from Apalache CE into a header expected by `tendermint-testgen header`", | ||
"kind": "INLINE", | ||
"source": { | ||
"validators": "$ | block_validators | map(id_to_validator)", | ||
"next_validators": "$ | block_next_validators | map(id_to_validator)", | ||
"height": "$ | block_height", | ||
"time": "$ | block_time" | ||
} | ||
}, | ||
{ | ||
"name": "block_to_commit", | ||
"description": "transform a block from Apalache CE into a commit expected by `tendermint-testgen commit`", | ||
"kind": "INLINE", | ||
"let": { | ||
"header": "$ | block_to_header" | ||
}, | ||
"source": { | ||
"header": "$header", | ||
"votes": "$ | lightblock_commits | map(id_to_vote)" | ||
} | ||
}, | ||
{ | ||
"name": "ids_to_validators", | ||
"description": "transform a non-empty array of identifiers into Tendermint validators", | ||
"kind": "INLINE", | ||
"source": "$ | map(id_to_validator) | map(tendermint_validator)" | ||
}, | ||
{ | ||
"name": "empty_array", | ||
"description": "just an empty array", | ||
"kind": "INLINE", | ||
"source": [] | ||
}, | ||
{ | ||
"name": "first_validator", | ||
"description": "extract first validator from a non-empty array of identifiers", | ||
"kind": "INLINE", | ||
"source": "$[0] | unwrap | id_to_validator | tendermint_validator" | ||
}, | ||
{ | ||
"name": "const_id", | ||
"description": "constant identifier", | ||
"kind": "INLINE", | ||
"source": "a" | ||
}, { | ||
"name": "fixed_validator", | ||
"description": "extract first validator from a non-empty array of identifiers", | ||
"kind": "INLINE", | ||
"source": "$const_id | id_to_validator | tendermint_validator" | ||
}, | ||
{ | ||
"name": "ids_to_validator_set", | ||
"description": "transform an array of identifiers into a JSON-encoded Tendermint validator set", | ||
"kind": "INLINE", | ||
"source": { | ||
"validators": "$ | ifelse(ids_to_validators,empty_array)", | ||
"proposer": "$ | ifelse(first_validator,fixed_validator)" | ||
} | ||
}, | ||
{ | ||
"name": "block_to_signed_header", | ||
"description": "transform a block from Apalache CE into a JSON-encoded Tendermint signed header", | ||
"kind": "INLINE", | ||
"source": { | ||
"header": "$ | block_to_header | tendermint_header", | ||
"commit": "$ | block_to_commit | tendermint_commit" | ||
} | ||
} | ||
] | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,42 @@ | ||
{ | ||
"description": "Transform an Apalache counterexample into a Tendermint LightClient test", | ||
"use": [ | ||
"unix.json", | ||
"apalache-tendermint.json" | ||
], | ||
"input": [ | ||
{ | ||
"name": "block_to_initial_block", | ||
"description": "transforms a block from Apalache CE into a JSON-encoded Tendermint initial light block", | ||
"kind": "INLINE", | ||
"source": { | ||
"signed_header": "$ | block_to_signed_header", | ||
"next_validator_set": "$ | block_next_validators | ids_to_validator_set", | ||
"trusting_period": "1400000000000", | ||
"now": "$utc_timestamp" | ||
} | ||
}, | ||
{ | ||
"name": "state_to_lite_block_verdict", | ||
"description": "transforms a block from Apalache CE into a JSON-encoded Tendermint light block", | ||
"kind": "INLINE", | ||
"let": { | ||
"block": "$..[?(@.key.str == 'current')].value" | ||
}, | ||
"source": { | ||
"block": { | ||
"signed_header": "$block | block_to_signed_header", | ||
"validator_set": "$block | block_validators | ids_to_validator_set", | ||
"next_validator_set": "$block | block_next_validators | ids_to_validator_set" | ||
}, | ||
"now": "$..[?(@.key.str == 'now')].value | unwrap | tendermint_time", | ||
"verdict": "$..[?(@.key.str == 'verdict')].value.str | unwrap" | ||
} | ||
} | ||
], | ||
"output": { | ||
"description": "auto-generated from Apalache counterexample", | ||
"initial": "$history[0]..[?(@.key.str == 'current')].value | block_to_initial_block", | ||
"input": "$history[1:] | map(state_to_lite_block_verdict)" | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
{ | ||
"description": "Transformers for generating Tendermint datastructures", | ||
"prerequisites": "add tendermint-testgen to your $PATH", | ||
"input": [ | ||
{ | ||
"name": "tendermint_validator", | ||
"kind": "COMMAND", | ||
"source": "tendermint-testgen --stdin validator" | ||
}, | ||
{ | ||
"name": "tendermint_header", | ||
"kind": "COMMAND", | ||
"source": "tendermint-testgen --stdin header" | ||
}, | ||
{ | ||
"name": "tendermint_commit", | ||
"kind": "COMMAND", | ||
"source": "tendermint-testgen --stdin commit" | ||
}, | ||
{ | ||
"name": "tendermint_vote", | ||
"kind": "COMMAND", | ||
"source": "tendermint-testgen --stdin vote" | ||
}, | ||
{ | ||
"name": "tendermint_time", | ||
"kind": "COMMAND", | ||
"source": "tendermint-testgen --stdin time" | ||
} | ||
] | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,29 @@ | ||
{ | ||
"description": "Useful external commands", | ||
"input": [ | ||
{ | ||
"name": "date", | ||
"kind": "COMMAND", | ||
"source": "date -I", | ||
"stdin": false | ||
}, | ||
{ | ||
"name": "utc_timestamp", | ||
"kind": "COMMAND", | ||
"source": "date --utc +%FT%H:%M:%S.%NZ", | ||
"stdin": false | ||
}, | ||
{ | ||
"name": "utc_timestamp_hour_ago", | ||
"kind": "COMMAND", | ||
"source": "date --utc +%FT%H:%M:%S.%NZ --date '-1 hour'", | ||
"stdin": false | ||
}, | ||
{ | ||
"name": "utc_timestamp_2hours_ago", | ||
"kind": "COMMAND", | ||
"source": "date --utc +%FT%H:%M:%S.%NZ --date '-2 hour'", | ||
"stdin": false | ||
} | ||
] | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,122 @@ | ||
use crate::{command::*, tester::TestEnv}; | ||
use serde::{Deserialize, Serialize}; | ||
use std::io; | ||
|
||
#[derive(Deserialize, Clone, Debug)] | ||
pub struct ApalacheTestBatch { | ||
pub description: String, | ||
pub model: String, | ||
pub length: Option<u64>, | ||
pub timeout: Option<u64>, | ||
pub tests: Vec<String>, | ||
} | ||
|
||
#[derive(Serialize, Deserialize, Clone, Debug)] | ||
pub struct ApalacheTestCase { | ||
pub model: String, | ||
pub test: String, | ||
pub length: Option<u64>, | ||
pub timeout: Option<u64>, | ||
} | ||
|
||
pub enum ApalacheRun { | ||
/// Apalache has found a counterexample | ||
Counterexample(CommandRun), | ||
/// Apalache has not found a counterexample up to specified length bound | ||
NoCounterexample(CommandRun), | ||
/// Apalache has found a deadlock | ||
Deadlock(CommandRun), | ||
/// Apalache model checking run failed (e.g. a parsing error) | ||
ModelError(CommandRun), | ||
/// Apalache returned an unknown error code | ||
Unknown(CommandRun), | ||
/// The tool has reached the specified timeout without producing an answer | ||
Timeout(CommandRun), | ||
} | ||
|
||
impl ApalacheRun { | ||
pub fn message(&self) -> &str { | ||
match self { | ||
ApalacheRun::Counterexample(_) => "Apalache has generated a counterexample", | ||
ApalacheRun::NoCounterexample(_) => "Apalache failed to generate a counterexample; consider increasing the length bound, or changing your test", | ||
ApalacheRun::Deadlock(_) => "Apalache has found a deadlock; please inspect your model and test", | ||
ApalacheRun::ModelError(_) => "Apalache failed to process the model; please check it", | ||
ApalacheRun::Unknown(_) => "Apalache has generated an unknown outcome; please contact Apalache developers", | ||
ApalacheRun::Timeout(_) => "Apalache failed to generate a counterexample within given time; consider increasing the timeout, or changing your test", | ||
} | ||
} | ||
} | ||
|
||
pub fn run_apalache_test(dir: &str, test: ApalacheTestCase) -> io::Result<ApalacheRun> { | ||
let inv = format!("{}Inv", test.test); | ||
|
||
// Mutate the model: negate the test assertion to get the invariant to check | ||
let mutation_failed = || { | ||
io::Error::new( | ||
io::ErrorKind::InvalidInput, | ||
"failed to mutate the model and add invariant", | ||
) | ||
}; | ||
let env = TestEnv::new(dir).ok_or_else(mutation_failed)?; | ||
let model = env.read_file(&test.model).unwrap(); | ||
let mut new_model = String::new(); | ||
for line in model.lines() { | ||
if line.starts_with(&inv) { | ||
// invariant already present; skip mutation | ||
new_model.clear(); | ||
break; | ||
} | ||
if line.starts_with("======") { | ||
new_model += &format!("{} == ~{}\n", inv, test.test); | ||
} | ||
new_model += line; | ||
new_model += "\n"; | ||
} | ||
if !new_model.is_empty() { | ||
env.write_file(&test.model, &new_model) | ||
.ok_or_else(mutation_failed)?; | ||
} | ||
|
||
// Run Apalache, and process the result | ||
let mut cmd = Command::new(); | ||
if let Some(timeout) = test.timeout { | ||
cmd.program("timeout"); | ||
cmd.arg(&timeout.to_string()); | ||
cmd.arg("apalache-mc"); | ||
} else { | ||
cmd.program("apalache-mc"); | ||
} | ||
cmd.arg("check"); | ||
cmd.arg_from_parts(vec!["--inv=", &inv]); | ||
if let Some(length) = test.length { | ||
cmd.arg_from_parts(vec!["--length=", &length.to_string()]); | ||
} | ||
cmd.arg(&test.model); | ||
if !dir.is_empty() { | ||
cmd.current_dir(dir); | ||
} | ||
match cmd.spawn() { | ||
Ok(run) => { | ||
if run.status.success() { | ||
if run.stdout.contains("The outcome is: NoError") { | ||
Ok(ApalacheRun::NoCounterexample(run)) | ||
} else if run.stdout.contains("The outcome is: Error") { | ||
Ok(ApalacheRun::Counterexample(run)) | ||
} else if run.stdout.contains("The outcome is: Deadlock") { | ||
Ok(ApalacheRun::Deadlock(run)) | ||
} else { | ||
Ok(ApalacheRun::Unknown(run)) | ||
} | ||
} else if let Some(code) = run.status.code() { | ||
match code { | ||
99 => Ok(ApalacheRun::ModelError(run)), | ||
124 => Ok(ApalacheRun::Timeout(run)), | ||
_ => Ok(ApalacheRun::Unknown(run)), | ||
} | ||
} else { | ||
Ok(ApalacheRun::Timeout(run)) | ||
} | ||
} | ||
Err(e) => Err(e), | ||
} | ||
} |
Oops, something went wrong.