From f2c6113f62722f06a072b1f73b16039915af29e5 Mon Sep 17 00:00:00 2001 From: UnsignedByte Date: Fri, 18 Oct 2024 14:10:46 +0000 Subject: [PATCH 1/5] fix discharge --- crates/filament/src/ir_passes/discharge.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/crates/filament/src/ir_passes/discharge.rs b/crates/filament/src/ir_passes/discharge.rs index a14986f0..9f769b22 100644 --- a/crates/filament/src/ir_passes/discharge.rs +++ b/crates/filament/src/ir_passes/discharge.rs @@ -74,9 +74,9 @@ pub struct Discharge { /// Defined functions for `some` parameters on components comp_param_map: HashMap, smt::SExpr>, - // Defined names - param_map: ir::DenseIndexInfo, - ev_map: ir::DenseIndexInfo, + // Defined names. These are sparse in case certain parameters or events have been invalidated. + param_map: ir::SparseInfoMap, + ev_map: ir::SparseInfoMap, // Composite expressions expr_map: ir::DenseIndexInfo, time_map: ir::DenseIndexInfo, From f93a48e5ab022c5109138fa7a76abb1c2f0c90ad Mon Sep 17 00:00:00 2001 From: UnsignedByte Date: Mon, 21 Oct 2024 14:13:39 +0000 Subject: [PATCH 2/5] fix discharge --- crates/filament/src/ir_passes/bundle_elim.rs | 33 +++++-- crates/filament/src/ir_passes/discharge.rs | 95 +++++++++++--------- crates/filament/src/main.rs | 11 +++ 3 files changed, 87 insertions(+), 52 deletions(-) diff --git a/crates/filament/src/ir_passes/bundle_elim.rs b/crates/filament/src/ir_passes/bundle_elim.rs index 57e16c96..ac4f144b 100644 --- a/crates/filament/src/ir_passes/bundle_elim.rs +++ b/crates/filament/src/ir_passes/bundle_elim.rs @@ -3,9 +3,9 @@ use crate::{ ir_visitor::{Action, Construct, Visitor, VisitorData}, }; use fil_ir::{ - self as ir, Access, AddCtx, Bind, Command, Component, Connect, Ctx, - DenseIndexInfo, DisplayCtx, Expr, Foreign, Info, InvIdx, Invoke, Liveness, - MutCtx, Port, PortIdx, PortOwner, Range, SparseInfoMap, Subst, Time, + self as ir, Access, AddCtx, Bind, Component, Connect, Ctx, DenseIndexInfo, + DisplayCtx, Expr, Foreign, InvIdx, Invoke, Liveness, MutCtx, Port, PortIdx, + PortOwner, Range, SparseInfoMap, Subst, Time, }; use fil_utils as utils; use itertools::Itertools; @@ -147,12 +147,26 @@ impl BundleElim { let info = comp.add(info.clone()); // adds the new port to the component and return its index - comp.add(Port { + let pidx = comp.add(Port { live, owner, info, // duplicate the info width, - }) + }); + + // Fill in the live idxs with a new dummy index + let port = ir::Param { + owner: ir::ParamOwner::bundle(pidx), + info: comp.add(ir::Info::param( + "_".into(), + utils::GPosIdx::UNKNOWN, + )), + }; + let port = comp.add(port); + + comp.get_mut(pidx).live.idxs.push(port); + + pidx }) .collect(); // delete the original port @@ -228,7 +242,7 @@ impl Visitor for BundleElim { connect: &mut Connect, data: &mut VisitorData, ) -> Action { - let Connect { src, dst, .. } = connect; + let Connect { src, dst, info } = connect; if !self.context.get(data.idx).contains(dst.port) { // we are writing to a local port here. @@ -253,11 +267,12 @@ impl Visitor for BundleElim { src.into_iter() .zip_eq(dst) .map(|(src, dst)| { - Command::Connect(Connect { + Connect { src: Access::port(src, &mut data.comp), dst: Access::port(dst, &mut data.comp), - info: data.comp.add(Info::empty()), - }) + info: *info, + } + .into() }) .collect(), ) diff --git a/crates/filament/src/ir_passes/discharge.rs b/crates/filament/src/ir_passes/discharge.rs index 9f769b22..6c949dca 100644 --- a/crates/filament/src/ir_passes/discharge.rs +++ b/crates/filament/src/ir_passes/discharge.rs @@ -78,8 +78,8 @@ pub struct Discharge { param_map: ir::SparseInfoMap, ev_map: ir::SparseInfoMap, // Composite expressions - expr_map: ir::DenseIndexInfo, - time_map: ir::DenseIndexInfo, + expr_map: ir::SparseInfoMap, + time_map: ir::SparseInfoMap, // Propositions prop_map: ir::DenseIndexInfo, // Propositions that have already been checked @@ -484,32 +484,36 @@ impl Discharge { } } - fn expr_to_sexp(&mut self, expr: &ir::Expr) -> smt::SExpr { + fn expr_to_sexp(&mut self, expr: &ir::Expr) -> Option { match expr { - ir::Expr::Param(p) => self.param_map[*p], - ir::Expr::Concrete(n) => self.num(*n), + ir::Expr::Param(p) => self.param_map.find(*p).cloned(), + ir::Expr::Concrete(n) => Some(self.num(*n)), ir::Expr::Bin { op, lhs, rhs } => { - let l = self.expr_map[*lhs]; - let r = self.expr_map[*rhs]; - match op { - ast::Op::Add => self.plus(l, r), - ast::Op::Sub => self.sub(l, r), - ast::Op::Mul => self.times(l, r), - ast::Op::Div => self.div(l, r), - ast::Op::Mod => self.modulo(l, r), - } + let l = self.expr_map.find(*lhs); + let r = self.expr_map.find(*rhs); + l.and_then(|&l| { + r.map(|&r| match op { + ast::Op::Add => self.plus(l, r), + ast::Op::Sub => self.sub(l, r), + ast::Op::Mul => self.times(l, r), + ast::Op::Div => self.div(l, r), + ast::Op::Mod => self.modulo(l, r), + }) + }) } ir::Expr::Fn { op, args } => { let args = args.iter().map(|e| self.expr_map[*e]); - self.sol.list( + Some(self.sol.list( iter::once(self.func_map[op]).chain(args).collect_vec(), - ) + )) } ir::Expr::If { cond, then, alt } => { - let then = self.expr_map[*then]; - let alt = self.expr_map[*alt]; + let then = self.expr_map.find(*then); + let alt = self.expr_map.find(*alt); let cond = self.prop_map[*cond]; - self.sol.ite(cond.get(), then, alt) + then.and_then(|&then| { + alt.map(|&alt| self.sol.ite(cond.get(), then, alt)) + }) } } } @@ -610,28 +614,30 @@ impl Visitor for Discharge { let bs = self.sol.bool_sort(); // Declare all expressions for (idx, expr) in data.comp.exprs().iter() { - // do props inside of exprs ahead of time - let relevant_props = idx - .relevant_props(&data.comp) - .into_iter() - .map(|i| (i, data.comp.get(i))); + // If this expression refers to an invalid parameter, skip it + if let Some(assign) = self.expr_to_sexp(expr) { + // do props inside of exprs ahead of time + let relevant_props = idx + .relevant_props(&data.comp) + .into_iter() + .map(|i| (i, data.comp.get(i))); + + for (pidx, prop) in relevant_props { + let assign = self.prop_to_sexp(prop); + let sexp = self + .sol + .define_const(Discharge::fmt_prop(pidx), bs, assign) + .unwrap(); + self.prop_map.insert(pidx, SExprWrapper::SExpr(sexp)); + } - for (pidx, prop) in relevant_props { - let assign = self.prop_to_sexp(prop); let sexp = self .sol - .define_const(Discharge::fmt_prop(pidx), bs, assign) + .define_const(Self::fmt_expr(idx), int, assign) .unwrap(); - self.prop_map.insert(pidx, SExprWrapper::SExpr(sexp)); + self.overflow_assert(sexp); + self.expr_map.push(idx, sexp); } - - let assign = self.expr_to_sexp(expr); - let sexp = self - .sol - .define_const(Self::fmt_expr(idx), int, assign) - .unwrap(); - self.overflow_assert(sexp); - self.expr_map.push(idx, sexp); } // Assert bindings for all let-bound parameters @@ -647,13 +653,16 @@ impl Visitor for Discharge { // Declare all time expressions for (idx, ir::Time { event, offset }) in data.comp.times().iter() { - let assign = self.plus(self.ev_map[*event], self.expr_map[*offset]); - let sexp = self - .sol - .define_const(Self::fmt_time(idx), int, assign) - .unwrap(); - self.overflow_assert(sexp); - self.time_map.push(idx, sexp); + if self.ev_map.contains(*event) && self.expr_map.contains(*offset) { + let assign = + self.plus(self.ev_map[*event], self.expr_map[*offset]); + let sexp = self + .sol + .define_const(Self::fmt_time(idx), int, assign) + .unwrap(); + self.overflow_assert(sexp); + self.time_map.push(idx, sexp); + } } // Declare all propositions diff --git a/crates/filament/src/main.rs b/crates/filament/src/main.rs index c49d7116..c4860a25 100644 --- a/crates/filament/src/main.rs +++ b/crates/filament/src/main.rs @@ -97,6 +97,17 @@ fn run(opts: &cmdline::Opts) -> Result<(), u64> { ip::BundleElim, ip::AssignCheck } + // type check again before lowering + ir_pass_pipeline! {opts, ir; + ip::BuildDomination + // ip::TypeCheck, + // ip::IntervalCheck, + // ip::PhantomCheck, + // ip::Assume + } + if !opts.unsafe_skip_discharge { + ir_pass_pipeline! {opts, ir; ip::Discharge } + } // Return early if we're asked to dump the interface if opts.dump_interface { From 1f484f1ec85cb228de7f10be6a4dedaea2c2ee91 Mon Sep 17 00:00:00 2001 From: UnsignedByte Date: Mon, 21 Oct 2024 15:12:29 +0000 Subject: [PATCH 3/5] filter by validity --- crates/filament/src/ir_passes/discharge.rs | 95 ++++++++++++---------- crates/filament/src/main.rs | 10 +-- crates/ir/src/expr.rs | 11 ++- crates/ir/src/fact.rs | 19 ++++- crates/ir/src/time.rs | 10 ++- 5 files changed, 92 insertions(+), 53 deletions(-) diff --git a/crates/filament/src/ir_passes/discharge.rs b/crates/filament/src/ir_passes/discharge.rs index 6c949dca..ea22d4b4 100644 --- a/crates/filament/src/ir_passes/discharge.rs +++ b/crates/filament/src/ir_passes/discharge.rs @@ -484,36 +484,32 @@ impl Discharge { } } - fn expr_to_sexp(&mut self, expr: &ir::Expr) -> Option { + fn expr_to_sexp(&mut self, expr: &ir::Expr) -> smt::SExpr { match expr { - ir::Expr::Param(p) => self.param_map.find(*p).cloned(), - ir::Expr::Concrete(n) => Some(self.num(*n)), + ir::Expr::Param(p) => self.param_map[*p], + ir::Expr::Concrete(n) => self.num(*n), ir::Expr::Bin { op, lhs, rhs } => { - let l = self.expr_map.find(*lhs); - let r = self.expr_map.find(*rhs); - l.and_then(|&l| { - r.map(|&r| match op { - ast::Op::Add => self.plus(l, r), - ast::Op::Sub => self.sub(l, r), - ast::Op::Mul => self.times(l, r), - ast::Op::Div => self.div(l, r), - ast::Op::Mod => self.modulo(l, r), - }) - }) + let l = self.expr_map[*lhs]; + let r = self.expr_map[*rhs]; + match op { + ast::Op::Add => self.plus(l, r), + ast::Op::Sub => self.sub(l, r), + ast::Op::Mul => self.times(l, r), + ast::Op::Div => self.div(l, r), + ast::Op::Mod => self.modulo(l, r), + } } ir::Expr::Fn { op, args } => { let args = args.iter().map(|e| self.expr_map[*e]); - Some(self.sol.list( + self.sol.list( iter::once(self.func_map[op]).chain(args).collect_vec(), - )) + ) } ir::Expr::If { cond, then, alt } => { - let then = self.expr_map.find(*then); - let alt = self.expr_map.find(*alt); + let then = self.expr_map[*then]; + let alt = self.expr_map[*alt]; let cond = self.prop_map[*cond]; - then.and_then(|&then| { - alt.map(|&alt| self.sol.ite(cond.get(), then, alt)) - }) + self.sol.ite(cond.get(), then, alt) } } } @@ -613,31 +609,34 @@ impl Visitor for Discharge { let bs = self.sol.bool_sort(); // Declare all expressions - for (idx, expr) in data.comp.exprs().iter() { - // If this expression refers to an invalid parameter, skip it - if let Some(assign) = self.expr_to_sexp(expr) { - // do props inside of exprs ahead of time - let relevant_props = idx - .relevant_props(&data.comp) - .into_iter() - .map(|i| (i, data.comp.get(i))); - - for (pidx, prop) in relevant_props { - let assign = self.prop_to_sexp(prop); - let sexp = self - .sol - .define_const(Discharge::fmt_prop(pidx), bs, assign) - .unwrap(); - self.prop_map.insert(pidx, SExprWrapper::SExpr(sexp)); - } + for (idx, expr) in data + .comp + .exprs() + .iter() + .filter(|(idx, _)| idx.valid(&data.comp)) + { + // do props inside of exprs ahead of time + let relevant_props = idx + .relevant_props(&data.comp) + .into_iter() + .map(|i| (i, data.comp.get(i))); + for (pidx, prop) in relevant_props { + let assign = self.prop_to_sexp(prop); let sexp = self .sol - .define_const(Self::fmt_expr(idx), int, assign) + .define_const(Discharge::fmt_prop(pidx), bs, assign) .unwrap(); - self.overflow_assert(sexp); - self.expr_map.push(idx, sexp); + self.prop_map.insert(pidx, SExprWrapper::SExpr(sexp)); } + + let assign = self.expr_to_sexp(expr); + let sexp = self + .sol + .define_const(Self::fmt_expr(idx), int, assign) + .unwrap(); + self.overflow_assert(sexp); + self.expr_map.push(idx, sexp); } // Assert bindings for all let-bound parameters @@ -652,7 +651,12 @@ impl Visitor for Discharge { } // Declare all time expressions - for (idx, ir::Time { event, offset }) in data.comp.times().iter() { + for (idx, ir::Time { event, offset }) in data + .comp + .times() + .iter() + .filter(|(idx, _)| idx.valid(&data.comp)) + { if self.ev_map.contains(*event) && self.expr_map.contains(*offset) { let assign = self.plus(self.ev_map[*event], self.expr_map[*offset]); @@ -666,7 +670,12 @@ impl Visitor for Discharge { } // Declare all propositions - for (idx, prop) in data.comp.props().iter() { + for (idx, prop) in data + .comp + .props() + .iter() + .filter(|(idx, _)| idx.valid(&data.comp)) + { // Define assertion equating the proposition to its assignment let assign = self.prop_to_sexp(prop); if let Ok(sexp) = diff --git a/crates/filament/src/main.rs b/crates/filament/src/main.rs index c4860a25..e6ca3b6a 100644 --- a/crates/filament/src/main.rs +++ b/crates/filament/src/main.rs @@ -99,11 +99,11 @@ fn run(opts: &cmdline::Opts) -> Result<(), u64> { } // type check again before lowering ir_pass_pipeline! {opts, ir; - ip::BuildDomination - // ip::TypeCheck, - // ip::IntervalCheck, - // ip::PhantomCheck, - // ip::Assume + ip::BuildDomination, + ip::TypeCheck, + ip::IntervalCheck, + ip::PhantomCheck, + ip::Assume } if !opts.unsafe_skip_discharge { ir_pass_pipeline! {opts, ir; ip::Discharge } diff --git a/crates/ir/src/expr.rs b/crates/ir/src/expr.rs index d7b6fc04..83e00249 100644 --- a/crates/ir/src/expr.rs +++ b/crates/ir/src/expr.rs @@ -1,5 +1,5 @@ -use super::{AddCtx, Component, Ctx, ExprIdx, ParamIdx}; -use crate::{construct_binop, Prop, PropIdx}; +use super::{AddCtx, Component, Ctx, ExprIdx, MutCtx, ParamIdx}; +use crate::{construct_binop, Param, Prop, PropIdx}; use fil_ast as ast; use std::fmt::Display; @@ -112,6 +112,13 @@ impl ExprIdx { /// Queries over [ExprIdx] impl ExprIdx { + pub fn valid( + &self, + ctx: &(impl Ctx + Ctx + MutCtx), + ) -> bool { + self.relevant_vars(ctx).iter().all(|p| ctx.valid(*p)) + } + pub fn relevant_props( &self, ctx: &(impl Ctx + Ctx), diff --git a/crates/ir/src/fact.rs b/crates/ir/src/fact.rs index c11981c0..633596c0 100644 --- a/crates/ir/src/fact.rs +++ b/crates/ir/src/fact.rs @@ -1,5 +1,7 @@ -use super::{idxs::PropIdx, AddCtx, Ctx, ExprIdx, InfoIdx, TimeIdx, TimeSub}; -use crate::{construct_binop, EventIdx, Expr, ParamIdx, Time}; +use super::{ + idxs::PropIdx, AddCtx, Ctx, ExprIdx, InfoIdx, MutCtx, TimeIdx, TimeSub, +}; +use crate::{construct_binop, Event, EventIdx, Expr, Param, ParamIdx, Time}; use std::fmt::{self, Display}; #[derive(Clone, PartialEq, Eq, Hash)] @@ -357,6 +359,19 @@ impl PropIdx { } } } + + pub fn valid( + &self, + ctx: &(impl Ctx + + Ctx