From f36f5af39d18c738630ed248226eae7970eed121 Mon Sep 17 00:00:00 2001 From: Rachit Nigam Date: Mon, 4 Sep 2023 22:34:23 +0530 Subject: [PATCH] break things because exists binding logic is wrong --- src/ir/comp.rs | 3 -- src/ir/control.rs | 15 +++++++++ src/ir/fact.rs | 2 +- src/ir/from_ast/astconv.rs | 19 +++++++----- src/ir/from_ast/build_ctx.rs | 50 ------------------------------ src/ir/mod.rs | 4 ++- src/ir/printer/comp.rs | 22 ++++++++++--- src/ir/utils/traversal.rs | 3 +- src/ir/validate.rs | 50 ++++++++++++++++-------------- src/ir_passes/discharge.rs | 43 ++++++++++++++++--------- src/ir_passes/hoist_facts.rs | 35 +++++++++------------ src/ir_passes/lower/compile.rs | 3 ++ src/ir_passes/mono/monodeferred.rs | 1 + src/ir_visitor/visitor.rs | 9 ++++++ 14 files changed, 134 insertions(+), 125 deletions(-) diff --git a/src/ir/comp.rs b/src/ir/comp.rs index a19aa60e0..b825ad506 100644 --- a/src/ir/comp.rs +++ b/src/ir/comp.rs @@ -58,9 +58,6 @@ pub struct Component { /// Facts defined in the component signature pub facts: Vec, - /// Existentially quantified parameters and their binding - pub exists_params: Vec<(ParamIdx, Option)>, - /// Commands in the component pub cmds: Vec, diff --git a/src/ir/control.rs b/src/ir/control.rs index 42d9f17c9..ccba1c264 100644 --- a/src/ir/control.rs +++ b/src/ir/control.rs @@ -21,6 +21,8 @@ pub enum Command { If(If), /// An `assume` or `assert` fact Fact(Fact), + /// An `exists` binding + Exists(Exists), } impl Command { pub fn is_loop(&self) -> bool { @@ -66,6 +68,11 @@ impl From for Command { Command::Fact(fact) } } +impl From for Command { + fn from(exists: Exists) -> Self { + Command::Exists(exists) + } +} #[derive(Clone, PartialEq, Eq)] /// An instantiated component @@ -183,3 +190,11 @@ impl EventBind { } } } + +#[derive(Clone, PartialEq, Eq)] +pub struct Exists { + /// The existentially quantified parameter + pub param: ParamIdx, + /// The binding for the parameter + pub expr: ExprIdx, +} diff --git a/src/ir/fact.rs b/src/ir/fact.rs index fea2bcd8e..25b7c4b5e 100644 --- a/src/ir/fact.rs +++ b/src/ir/fact.rs @@ -14,7 +14,7 @@ impl fmt::Display for Cmp { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let op = match self { Cmp::Gt => ">", - Cmp::Eq => "=", + Cmp::Eq => "==", Cmp::Gte => ">=", }; write!(f, "{}", op) diff --git a/src/ir/from_ast/astconv.rs b/src/ir/from_ast/astconv.rs index dda6bdf20..af75520eb 100644 --- a/src/ir/from_ast/astconv.rs +++ b/src/ir/from_ast/astconv.rs @@ -3,8 +3,8 @@ use super::build_ctx::{OwnedParam, OwnedPort}; use super::{BuildCtx, Sig, SigMap}; use crate::diagnostics; use crate::ir::{ - AddCtx, Cmp, Ctx, EventIdx, ExprIdx, InterfaceSrc, MutCtx, ParamIdx, - PortIdx, PropIdx, TimeIdx, + AddCtx, Cmp, Ctx, DisplayCtx, EventIdx, ExprIdx, InterfaceSrc, MutCtx, + ParamIdx, PortIdx, PropIdx, TimeIdx, }; use crate::utils::{GPosIdx, Idx}; use crate::{ast, ir}; @@ -545,9 +545,7 @@ impl<'prog> BuildCtx<'prog> { self.add_let_param(param.copy(), e); } ast::SigBind::Exists { param, cons } => { - let p_idx = - self.param(param.clone(), ir::ParamOwner::Exists); - self.add_exists_param(p_idx); + self.param(param.clone(), ir::ParamOwner::Exists); // Constraints on existentially quantified parameters for pc in cons { let info = self.comp().add(ir::Info::assert( @@ -819,8 +817,15 @@ impl<'prog> BuildCtx<'prog> { ast::Command::Instance(inst) => self.instance(inst)?, ast::Command::Exists(ast::Exists { param, bind }) => { let expr = self.expr(bind.inner().clone())?; - self.set_exists_bind(param, expr)?; - vec![] + let owner = OwnedParam::Local(param.copy()); + let param_expr = self.get_param(&owner, param.pos())?; + let Some(param) = param_expr.as_param(self.comp()) else { + unreachable!( + "Existing LHS is an expression: {}", + self.comp().display(param_expr) + ) + }; + vec![ir::Exists { param, expr }.into()] } ast::Command::Fact(ast::Fact { cons, checked }) => { let reason = self.comp().add( diff --git a/src/ir/from_ast/build_ctx.rs b/src/ir/from_ast/build_ctx.rs index 1035c3720..63229208f 100644 --- a/src/ir/from_ast/build_ctx.rs +++ b/src/ir/from_ast/build_ctx.rs @@ -218,56 +218,6 @@ impl<'prog> BuildCtx<'prog> { self.param_map.insert(OwnedParam::Local(id), expr); } - /// Mark a parameter as existentially quantified. - pub fn add_exists_param(&mut self, param: ir::ParamIdx) { - self.comp.exists_params.push((param, None)); - } - - /// Provide the binding for an existentially quantified parameter. - pub fn set_exists_bind( - &mut self, - param: ast::Loc, - expr: ir::ExprIdx, - ) -> BuildRes<()> { - let p_idx = self - .get_param(&OwnedParam::local(param.copy()), param.pos())? - .as_param(&self.comp) - .unwrap(); - let diag = &mut self.diag; - - if let Some((_, bind)) = self - .comp - .exists_params - .iter_mut() - .find(|(p, _)| *p == p_idx) - { - // If there is already a binding, then we have a problem - if bind.is_some() { - let msg = format!( - "existential parameter `{param}' already has a binding", - param = param - ); - let err = Error::malformed(msg.clone()) - .add_note(diag.add_info(msg, param.pos())); - diag.add_error(err); - return Err(std::mem::take(diag)); - } - *bind = Some(expr); - Ok(()) - } else { - let msg = format!( - "parameter `{param}' is not existentially quantified", - param = param - ); - let err = Error::malformed(msg).add_note(diag.add_info( - "parameter is not existentially quantified", - param.pos(), - )); - diag.add_error(err); - Err(std::mem::take(diag)) - } - } - pub fn get_param( &mut self, param: &OwnedParam, diff --git a/src/ir/mod.rs b/src/ir/mod.rs index 67bae4739..25d7888f5 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -17,7 +17,9 @@ mod validate; pub use comp::Component; pub use context::Context; -pub use control::{Command, Connect, EventBind, If, Instance, Invoke, Loop}; +pub use control::{ + Command, Connect, EventBind, Exists, If, Instance, Invoke, Loop, +}; pub use ctx::{AddCtx, Ctx, MutCtx}; pub use expr::Expr; pub use fact::{Cmp, CmpOp, Fact, Prop}; diff --git a/src/ir/printer/comp.rs b/src/ir/printer/comp.rs index 96611d183..e7eee4cfc 100644 --- a/src/ir/printer/comp.rs +++ b/src/ir/printer/comp.rs @@ -75,13 +75,18 @@ impl<'a> Printer<'a> { write!(f, "{:indent$}}}", "") } ir::Command::If(c) => { - writeln!(f, "{:indent$}if {} {{", "", c.cond)?; + writeln!( + f, + "{:indent$}if {} {{", + "", + self.ctx.display(c.cond) + )?; self.commands(&c.then, indent + 2, f)?; - writeln!(f, "{:indent$}}}", "")?; + write!(f, "{:indent$}}}", "")?; if !c.alt.is_empty() { - writeln!(f, "{:indent$}else {{", "")?; + writeln!(f, " else {{")?; self.commands(&c.alt, indent + 2, f)?; - writeln!(f, "{:indent$}}}", "")?; + write!(f, "{:indent$}}}", "")?; } Ok(()) } @@ -102,6 +107,15 @@ impl<'a> Printer<'a> { ) } } + ir::Command::Exists(ir::Exists { param, expr }) => { + write!( + f, + "{:indent$}exists {} = {};", + "", + self.ctx.display(*param), + self.ctx.display(*expr) + ) + } } } diff --git a/src/ir/utils/traversal.rs b/src/ir/utils/traversal.rs index 902ab1ae9..c595d4db3 100644 --- a/src/ir/utils/traversal.rs +++ b/src/ir/utils/traversal.rs @@ -103,7 +103,8 @@ impl Traversal { ir::Command::Connect(_) | ir::Command::BundleDef(_) | ir::Command::Invoke(_) - | ir::Command::Fact(_) => (), + | ir::Command::Fact(_) + | ir::Command::Exists(_) => (), } } } diff --git a/src/ir/validate.rs b/src/ir/validate.rs index 8bffddcf1..dd6074376 100644 --- a/src/ir/validate.rs +++ b/src/ir/validate.rs @@ -210,12 +210,12 @@ impl<'a> Validate<'a> { /// (1) It is defined in the component /// (2) Its owner is defined in the component /// (3) Its owner points to it? - fn param(&self, pidx: ir::ParamIdx) { + fn param(&self, pidx: ir::ParamIdx) -> &ir::Param { // check (1) - this will panic if param not defined - let ir::Param { owner, .. } = &self.comp.get(pidx); + let param = &self.comp.get(pidx); // check (2) and (3) - match owner { + match ¶m.owner { ir::ParamOwner::Sig | ir::ParamOwner::Exists | ir::ParamOwner::Loop => { /* Nothing to check */ } @@ -232,6 +232,8 @@ impl<'a> Validate<'a> { } } } + + param } /// An invoke is valid if: @@ -314,27 +316,14 @@ impl<'a> Validate<'a> { /// (1) The structures that it contains are valid fn command(&self, cmd: &ir::Command) { match cmd { - ir::Command::Instance(iidx) => { - self.instance(*iidx); - } - ir::Command::Invoke(iidx) => { - self.invoke(*iidx); - } - ir::Command::Connect(con) => { - self.connect(con); - } - ir::Command::ForLoop(lp) => { - self.forloop(lp); - } - ir::Command::If(cond) => { - self.if_stmt(cond); - } - ir::Command::Fact(fact) => { - self.fact(fact); - } - ir::Command::BundleDef(b) => { - self.bundle_def(*b); - } + ir::Command::Instance(iidx) => self.instance(*iidx), + ir::Command::Invoke(iidx) => self.invoke(*iidx), + ir::Command::Connect(con) => self.connect(con), + ir::Command::ForLoop(lp) => self.forloop(lp), + ir::Command::If(cond) => self.if_stmt(cond), + ir::Command::Fact(fact) => self.fact(fact), + ir::Command::BundleDef(b) => self.bundle_def(*b), + ir::Command::Exists(e) => self.exists(e), } } @@ -439,4 +428,17 @@ impl<'a> Validate<'a> { let ir::Fact { prop, .. } = *fact; self.prop(prop); } + + fn exists(&self, exists: &ir::Exists) { + let ir::Exists { param: p_idx, expr } = exists; + let param = self.param(*p_idx); + if !matches!(param.owner, ir::ParamOwner::Exists) { + self.comp.internal_error(format!( + "{} mentioned in existential binding but owned by {}", + self.comp.display(*p_idx), + param.owner + )) + } + self.expr(*expr); + } } diff --git a/src/ir_passes/discharge.rs b/src/ir_passes/discharge.rs index 047a4fa5d..338463628 100644 --- a/src/ir_passes/discharge.rs +++ b/src/ir_passes/discharge.rs @@ -22,7 +22,7 @@ impl Assign { .iter() .filter_map(|(k, v)| { // Attempt to parse value as a number - match v.parse::() { + match v.parse::() { Ok(v) if v == 0 => None, _ => Some(format!("{} = {v}", ctx.display(*k))), } @@ -133,12 +133,14 @@ impl Construct for Discharge { } impl Discharge { - fn fmt_param(param: ir::ParamIdx) -> String { - format!("param{}", param.get()) + fn fmt_param(param: ir::ParamIdx, ctx: &ir::Component) -> String { + format!("|{}@param{}|", ctx.display(param), param.get()) + // format!("param{}", param.get()) } - fn fmt_event(event: ir::EventIdx) -> String { - format!("event{}", event.get()) + fn fmt_event(event: ir::EventIdx, ctx: &ir::Component) -> String { + format!("|{}@event{}|", ctx.display(event), event.get()) + // format!("event{}", event.get()) } fn fmt_expr(expr: ir::ExprIdx) -> String { @@ -191,19 +193,30 @@ impl Discharge { .unique() .map(|p| { let s = self.param_map[*p]; + log::debug!("{} -> {}", self.sol.display(s), p); rev_map.insert(s, *p); s }) .collect_vec(); + let num_vars = sexps.len(); + + let model = self.sol.get_value(sexps).unwrap(); + assert!(model.len() == num_vars, + "{num_vars} relevant variables but the model contains assignments for {} variables", + model.len() + ); Assign( - self.sol - .get_value(sexps) - .unwrap() + model .into_iter() - .map(|(p, v)| { - let p = rev_map[&p]; - (p, self.sol.display(v).to_string()) + .flat_map(|(p, v)| { + let Some(&p) = rev_map.get(&p) else { + unreachable!( + "missing binding for sexp {}", + self.sol.display(p) + ); + }; + Some((p, self.sol.display(v).to_string())) }) .collect_vec(), ) @@ -225,7 +238,6 @@ impl Discharge { ctx.display(prop.consequent(ctx)); 100 ); - self.sol.assert(self.sol.not(actlit)).unwrap(); let out = match res { smt::Response::Sat => { if self.show_models { @@ -239,6 +251,8 @@ impl Discharge { smt::Response::Unsat => None, smt::Response::Unknown => panic!("Solver returned unknown"), }; + // Deassert the actlit after the `get-model` call. + self.sol.assert(self.sol.not(actlit)).unwrap(); self.checked.insert(prop, out); } if let Some(assign) = &self.checked[&prop] { @@ -359,12 +373,13 @@ impl Visitor for Discharge { } fn start(&mut self, data: &mut VisitorData) -> Action { + let comp = &data.comp; // Declare all parameters let int = self.sol.int_sort(); for (idx, _) in data.comp.params().iter() { let sexp = self .sol - .declare_fun(Self::fmt_param(idx), vec![], int) + .declare_fun(Self::fmt_param(idx, comp), vec![], int) .unwrap(); self.param_map.push(idx, sexp); } @@ -373,7 +388,7 @@ impl Visitor for Discharge { for (idx, _) in data.comp.events().iter() { let sexp = self .sol - .declare_fun(Self::fmt_event(idx), vec![], int) + .declare_fun(Self::fmt_event(idx, comp), vec![], int) .unwrap(); self.ev_map.push(idx, sexp); } diff --git a/src/ir_passes/hoist_facts.rs b/src/ir_passes/hoist_facts.rs index 2c1b835af..27bb1acaa 100644 --- a/src/ir_passes/hoist_facts.rs +++ b/src/ir_passes/hoist_facts.rs @@ -29,7 +29,7 @@ impl HoistFacts { } /// Insert a new path condition - fn insert(&mut self, prop: ir::PropIdx) { + fn add_to_pc(&mut self, prop: ir::PropIdx) { self.path_cond.push(prop); } @@ -48,26 +48,21 @@ impl Visitor for HoistFacts { "hoist-facts" } - /// Add the assignments to the existentially quantified parameters as - /// assumptions to the path condition of the component. - fn start(&mut self, data: &mut VisitorData) -> Action { - let ctx = &mut data.comp; - for (param, val) in ctx.exists_params.clone() { - let Some(e) = val else { - continue; - }; - let prop = param.expr(ctx).equal(e, ctx); - self.insert(prop); - } - Action::Continue - } - /// Collect all assumptions in a given scope and add them to the path condition. /// We do this so that all asserts in a scope are affected by all assumes. - fn start_cmds(&mut self, cmds: &mut Vec, _: &mut VisitorData) { + fn start_cmds( + &mut self, + cmds: &mut Vec, + data: &mut VisitorData, + ) { + let ctx = &mut data.comp; cmds.iter().for_each(|cmd| match cmd { ir::Command::Fact(fact) if fact.is_assume() => { - self.insert(fact.prop) + self.add_to_pc(fact.prop) + } + ir::Command::Exists(ir::Exists { param, expr }) => { + let prop = param.expr(ctx).equal(*expr, ctx); + self.add_to_pc(prop); } _ => (), }) @@ -87,13 +82,13 @@ impl Visitor for HoistFacts { fn do_if(&mut self, i: &mut ir::If, data: &mut VisitorData) -> Action { self.push(); - self.insert(i.cond); + self.add_to_pc(i.cond); let ac = self.visit_cmds(&mut i.then, data); assert!(ac == Action::Continue); self.pop(); self.push(); - self.insert(i.cond.not(&mut data.comp)); + self.add_to_pc(i.cond.not(&mut data.comp)); let ac = self.visit_cmds(&mut i.alt, data); assert!(ac == Action::Continue); self.pop(); @@ -114,7 +109,7 @@ impl Visitor for HoistFacts { let idx = index.expr(comp); let start = idx.gte(*start, comp); let end = idx.lt(*end, comp); - self.insert(start.and(end, comp)); + self.add_to_pc(start.and(end, comp)); Action::Continue } diff --git a/src/ir_passes/lower/compile.rs b/src/ir_passes/lower/compile.rs index 3b91138de..0978aa9fc 100644 --- a/src/ir_passes/lower/compile.rs +++ b/src/ir_passes/lower/compile.rs @@ -258,6 +258,9 @@ impl Compile { ir::Command::BundleDef(_) => { unreachable!("bundle definitions should have been compiled away.") } + ir::Command::Exists(_) => { + unreachable!("exists should have been compiled away.") + } ir::Command::Instance(_) // ignore instances and invokes as these are compiled first | ir::Command::Invoke(_) | ir::Command::Fact(_) => (), diff --git a/src/ir_passes/mono/monodeferred.rs b/src/ir_passes/mono/monodeferred.rs index af1cfa5d7..8983ec4fc 100644 --- a/src/ir_passes/mono/monodeferred.rs +++ b/src/ir_passes/mono/monodeferred.rs @@ -340,6 +340,7 @@ impl<'a, 'pass: 'a> MonoDeferred<'a, 'pass> { // If we want to do this long term, this should be done in a // separate pass and monomorphization should fail on facts. ir::Command::Fact(_) => None, + ir::Command::Exists(_) => todo!("Monomorphizing exist bindings"), } } } diff --git a/src/ir_visitor/visitor.rs b/src/ir_visitor/visitor.rs index a9920deda..d34550faa 100644 --- a/src/ir_visitor/visitor.rs +++ b/src/ir_visitor/visitor.rs @@ -181,6 +181,14 @@ where Action::Continue } + fn exists( + &mut self, + _: &mut ir::Exists, + _data: &mut VisitorData, + ) -> Action { + Action::Continue + } + fn visit_cmd( &mut self, cmd: &mut ir::Command, @@ -194,6 +202,7 @@ where ir::Command::ForLoop(l) => self.do_loop(l, data), ir::Command::If(i) => self.do_if(i, data), ir::Command::Fact(f) => self.fact(f, data), + ir::Command::Exists(e) => self.exists(e, data), } }