crate::prelude!();
use rsmt2::{print::Expr2Smt, SmtConf};
use expr::{Expr, Var};
use trans::Sys;
pub mod cexs;
pub use cexs::{Cexs, SmtParser, Solver};
#[derive(Debug, Clone)]
pub struct CheckRes<'s> {
pub okay: Set<&'s String>,
pub cexs: Cexs<'s>,
}
impl<'s> CheckRes<'s> {
pub fn new(sys: &'s Sys) -> Self {
let okay: Set<&'s String> = sys.po_s().keys().collect();
Self {
okay: okay.into(),
cexs: Cexs::new(),
}
}
pub fn all_falsified(&self) -> bool {
self.okay.is_empty()
}
pub fn has_falsifications(&self) -> bool {
!self.cexs.is_empty()
}
pub fn register_falsification(&mut self, po: &'s String, solver: &mut Solver) -> Res<()> {
if self.cexs.contains_key(po) {
bail!("trying to register PO `{}` as falsified twice")
}
if !self.okay.iter().any(|ok_po| *ok_po == po) {
bail!("trying to register unknown PO `{}` as falsified")
}
self.cexs.insert_falsification(po, solver)?;
let was_there = self.okay.remove(po);
if !was_there {
bail!("trying to to register unknown PO `{}` as falsified", po)
}
Ok(())
}
}
macro_rules! wrap {
(
$(
$(#[$meta:meta])*
$ty_name:ident
),* $(,)?
) => ($(
$(#[$meta])*
pub struct $ty_name<'sys> {
/// Internal result.
res: CheckRes<'sys>,
}
impl<'sys> $ty_name<'sys> {
/// Inner result accessor (borrow).
pub fn as_inner(&self) -> &CheckRes<'sys> {
&self.res
}
pub fn into_inner(self) -> CheckRes<'sys> {
self.res
}
}
impl<'sys> Deref for $ty_name<'sys> {
type Target = CheckRes<'sys>;
fn deref(&self) -> &CheckRes<'sys> {
&self.res
}
}
impl<'sys> DerefMut for $ty_name<'sys> {
fn deref_mut(&mut self) -> &mut CheckRes<'sys> {
&mut self.res
}
}
impl<'sys> From<CheckRes<'sys>> for $ty_name<'sys> {
fn from(res: CheckRes<'sys>) -> $ty_name {
$ty_name { res }
}
}
)*);
}
wrap! {
BaseRes,
StepRes,
BmcRes,
}
impl<'sys> BaseRes<'sys> {
pub fn merge_base_with_step(&self, step: &StepRes<'sys>) -> Res<BmcRes<'sys>> {
macro_rules! abort {
($n:expr) => {
bail!(
"asked to merge two inconsistent base/step check results ({})",
$n
)
};
}
let base = self;
if base.okay.len() + base.cexs.len() != step.okay.len() + step.cexs.len() {
abort!(format!(
"{}/{} | {}/{}",
base.okay.len(),
base.cexs.len(),
step.okay.len(),
step.cexs.len()
))
}
let mut res = CheckRes {
okay: base.okay.clone(),
cexs: Cexs::new(),
};
for inductive in &step.okay {
let was_there = res.okay.remove(inductive);
if !was_there && !base.cexs.contains_key(inductive) {
abort!(inductive)
}
}
Ok(res.into())
}
}
pub struct NegExpr<'e, E> {
expr: &'e E,
}
impl<'e, Info, E> Expr2Smt<Info> for NegExpr<'e, E>
where
E: Expr2Smt<Info>,
{
fn expr_to_smt2<W: Write>(&self, w: &mut W, i: Info) -> SmtRes<()> {
write!(w, "(not ")?;
self.expr.expr_to_smt2(w, i)?;
write!(w, ")")?;
Ok(())
}
}
pub struct InternalChecker<'sys> {
solver: Solver,
sys: &'sys Sys,
vars: Vec<Var>,
}
impl<'sys> InternalChecker<'sys> {
pub fn new(
sys: &'sys Sys,
z3_cmd: impl Into<String>,
tee: Option<impl AsRef<str>>,
) -> Res<Self> {
let z3_cmd = z3_cmd.into();
let mut split_cmd = z3_cmd.split(|c: char| c.is_whitespace());
let z3_cmd = split_cmd
.next()
.ok_or_else(|| format!("illegal Z3 command `{}`", z3_cmd))?
.trim();
let mut conf = SmtConf::z3(z3_cmd);
for opt in split_cmd {
let opt = opt.trim();
if !opt.is_empty() {
conf.option(opt);
}
}
let mut solver = conf
.spawn(cexs::SmtParser)
.chain_err(|| "while spawning z3 solver")?;
if let Some(path) = tee {
solver.path_tee(path.as_ref())?
}
let vars = sys.decls().all().collect();
Ok(Self { solver, sys, vars })
}
pub fn declare_vars(&mut self, step: Unroll) -> Res<()> {
for var in &self.vars {
self.solver
.declare_const_with(var, &var.typ(), step)
.chain_err(|| format!("while declaring variable `{}@{}`", var, step))?
}
Ok(())
}
pub fn assert_init(&mut self) -> Res<()> {
self.solver
.assert_with(self.sys.init(), 0)
.chain_err(|| "while asserting init predicate at 0")?;
Ok(())
}
#[allow(dead_code)]
pub fn assert_trans(&mut self, step: Unroll) -> Res<()> {
self.solver
.assert_with(self.sys.trans(), step)
.chain_err(|| format!("while asserting trans predicate at {}", step))?;
Ok(())
}
#[allow(dead_code)]
pub fn assert_expr(&mut self, expr: &Expr, step: Unroll) -> Res<()> {
self.solver.assert_with(expr, step).chain_err(|| {
format!(
"while asserting stateless expression `{}` at step {}",
expr, step
)
})?;
Ok(())
}
#[allow(dead_code)]
pub fn assert_po_s(&mut self, step: Unroll, res: &CheckRes) -> Res<()> {
for (name, po) in self.sys.po_s() {
if res.okay.contains(name) {
self.solver.assert_with(&po, step).chain_err(|| {
format!("while asserting negation of PO `{}` at step {}", name, step)
})?
}
}
Ok(())
}
#[allow(dead_code)]
pub fn assert_not_po_s(&mut self, step: Unroll) -> Res<()> {
for (name, po) in self.sys.po_s() {
let not_po = po.negated();
self.solver.assert_with(¬_po, step).chain_err(|| {
format!("while asserting negation of PO `{}` at step {}", name, step)
})?
}
Ok(())
}
pub fn find_po_falsifications(&mut self, step: Unroll, res: &mut CheckRes<'sys>) -> Res<bool> {
let mut changed = false;
let to_check: Vec<_> = res
.okay
.iter()
.map(|po| {
self.sys
.po_s()
.get_key_value(po as &str)
.ok_or_else(|| format!("unknown PO `{}`", po))
})
.collect();
for to_check in to_check {
let (name, po) = to_check?;
let not_po = po.negated();
self.solver.push(1)?;
self.solver.assert_with(¬_po, step).chain_err(|| {
format!("while asserting negation of PO `{}` at step {}", name, step)
})?;
if self.solver.check_sat()? {
changed = true;
res.register_falsification(name, &mut self.solver)?
}
self.solver.pop(1)?
}
Ok(changed)
}
#[allow(dead_code)]
pub fn check_sat(&mut self) -> Res<bool> {
let res = self.solver.check_sat()?;
Ok(res)
}
}
pub struct Base<'sys> {
checker: InternalChecker<'sys>,
}
impl<'sys> Base<'sys> {
pub fn new(
sys: &'sys Sys,
z3_cmd: impl Into<String>,
tee: Option<impl AsRef<str>>,
) -> Res<Self> {
let tee = tee.map(|s| format!("{}/base.smt2", s.as_ref()));
Ok(Self {
checker: InternalChecker::new(sys, z3_cmd, tee)?,
})
}
pub fn check(&mut self) -> Res<BaseRes<'sys>> {
self.checker.declare_vars(0)?;
self.checker.assert_init()?;
let mut res = CheckRes::new(&self.checker.sys);
let _ = self.checker.find_po_falsifications(0, &mut res)?;
Ok(res.into())
}
}
pub struct Step<'sys> {
checker: InternalChecker<'sys>,
}
impl<'sys> Step<'sys> {
pub fn new(
sys: &'sys Sys,
z3_cmd: impl Into<String>,
tee: Option<impl AsRef<str>>,
) -> Res<Self> {
let tee = tee.map(|s| format!("{}/step.smt2", s.as_ref()));
Ok(Self {
checker: InternalChecker::new(sys, z3_cmd, tee)?,
})
}
pub fn check(&mut self) -> Res<StepRes<'sys>> {
self.checker.declare_vars(0)?;
self.checker.declare_vars(1)?;
self.checker.assert_trans(0)?;
let mut res = CheckRes::new(&self.checker.sys);
'try_to_prove_okay_po_s: loop {
self.checker.solver.comment(&format!(
"Pushing scope to try to prove {} PO(s).",
res.okay.len()
))?;
self.checker.solver.push(1)?;
self.checker.solver.comment(&format!(
"Induction hypothesis for {} PO(s).",
res.okay.len()
))?;
self.checker.assert_po_s(0, &res)?;
let new_falsifications = self.checker.find_po_falsifications(1, &mut res)?;
if new_falsifications {
if res.okay.is_empty() {
self.checker
.solver
.comment("All POs have been falsified, done.")?;
self.checker.solver.kill()?;
break 'try_to_prove_okay_po_s Ok(res.into());
} else {
self.checker.solver.comment(
"New falsification(s) detected, popping and resuming proof attempt.",
)?;
self.checker.solver.pop(1)?;
continue 'try_to_prove_okay_po_s;
}
} else {
self.checker
.solver
.comment("Successfully proved remaining PO(s), done.")?;
self.checker.solver.kill()?;
break 'try_to_prove_okay_po_s Ok(res.into());
}
}
}
}
pub struct Bmc<'sys> {
checker: InternalChecker<'sys>,
next_step: Unroll,
check_step: Unroll,
res: BmcRes<'sys>,
}
impl<'sys> Bmc<'sys> {
pub fn new(
sys: &'sys Sys,
z3_cmd: impl Into<String>,
tee: Option<impl AsRef<str>>,
res: BmcRes<'sys>,
) -> Res<Self> {
let tee = tee.map(|s| format!("{}/bmc.smt2", s.as_ref()));
let mut checker = InternalChecker::new(sys, z3_cmd, tee)?;
checker.declare_vars(0)?;
checker.assert_init()?;
Ok(Self {
checker,
next_step: 1,
check_step: 0,
res,
})
}
pub fn res(&self) -> &BmcRes<'sys> {
&self.res
}
pub fn is_done(&self) -> bool {
self.res.all_falsified()
}
pub fn next_check_step(&self) -> Unroll {
self.check_step
}
pub fn destroy(mut self) -> Res<BmcRes<'sys>> {
self.checker
.solver
.kill()
.chain_err(|| "while killing the BMC solver")?;
Ok(self.res)
}
pub fn next_check(&mut self) -> Res<bool> {
let res = if self.check_step == 0 {
self.check()
.chain_err(|| "while checking for a falsification in the initial state(s)")?
} else {
let step = self.next_step;
self.unroll()
.chain_err(|| format!("while unrolling the system to step {}", step))?;
self.check().chain_err(|| {
format!(
"while checking for a falsification at step {}",
self.check_step
)
})?
};
Ok(res)
}
fn check(&mut self) -> Res<bool> {
if !self.next_step == self.check_step + 1 {
bail!(
"illegal configuration for a BMC check, next step is {} but check step is {}",
self.next_step,
self.check_step
)
}
let res = self
.checker
.find_po_falsifications(self.check_step, &mut self.res);
self.check_step += 1;
res
}
fn unroll(&mut self) -> Res<()> {
if !self.next_step == self.check_step || self.next_step < 1 {
bail!(
"illegal configuration for a BMC unroll, next step is {} but check step is {}",
self.next_step,
self.check_step
)
}
debug_assert!(self.next_step > 0);
self.checker.declare_vars(self.next_step)?;
let res = self.checker.assert_trans(self.next_step - 1);
self.next_step += 1;
res
}
}