Skip to content

Commit 63ea35a

Browse files
committed
more restructuring
1 parent 2c9d413 commit 63ea35a

File tree

8 files changed

+101
-127
lines changed

8 files changed

+101
-127
lines changed

crates/filament/src/ir_passes/mod.rs

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ mod lower;
1010
mod mono;
1111
mod phantom_check;
1212
mod prop_simplify;
13-
mod schedule;
1413
mod type_check;
1514

1615
pub use assignment_check::AssignCheck;
@@ -25,5 +24,4 @@ pub use lower::Compile;
2524
pub use mono::Monomorphize;
2625
pub use phantom_check::PhantomCheck;
2726
pub use prop_simplify::Simplify;
28-
pub use schedule::Schedule;
2927
pub use type_check::TypeCheck;

crates/filament/src/ir_passes/mono/monodeferred.rs

Lines changed: 23 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
use super::{
2-
CompKey, IntoBase, IntoUdl, MonoSig, Monomorphize, Underlying,
2+
Base, CompKey, IntoBase, IntoUdl, MonoSig, Monomorphize, Underlying,
33
UnderlyingComp,
44
};
5-
use fil_ir::{self as ir, AddCtx, Ctx};
5+
use fil_ir::{self as ir, AddCtx, Ctx, SparseInfoMap};
66
use fil_utils::{self as utils, AttrCtx};
77
use ir::DisplayCtx;
88
use itertools::Itertools;
@@ -24,6 +24,12 @@ pub struct MonoDeferred<'comp, 'pass: 'comp> {
2424

2525
/// If this component should be scheduled, this stores the scheduling type
2626
pub schedule: Option<u64>,
27+
28+
/// Existential parameter map.
29+
/// These are not interned until [Self::sig_complete_mono] as scheduling
30+
/// may affect the values of existential parameters.
31+
exist_params:
32+
SparseInfoMap<ir::Param, Base<ir::Expr>, Underlying<ir::Param>>,
2733
}
2834

2935
impl<'a, 'pass: 'a> MonoDeferred<'a, 'pass> {
@@ -39,6 +45,7 @@ impl<'a, 'pass: 'a> MonoDeferred<'a, 'pass> {
3945
monosig,
4046
// Set to false if we call `sig_partial_mono` and true once we call `sig_complete_mono`
4147
sig_mono_complete: true,
48+
exist_params: SparseInfoMap::default(),
4249
}
4350
}
4451
}
@@ -96,6 +103,17 @@ impl MonoDeferred<'_, '_> {
96103
pub fn sig_complete_mono(&mut self) {
97104
assert!(!self.sig_mono_complete);
98105

106+
// Insert the existential parameters into the monomorphization
107+
// Also extend the binding with existential parameters
108+
for (param, expr) in self.exist_params.iter() {
109+
let comp_key = self.monosig.comp_key.clone();
110+
let base_comp = self.monosig.base.comp();
111+
let v = expr.get().as_concrete(base_comp).unwrap();
112+
113+
self.pass.inst_info_mut(comp_key).add_exist_val(param, v);
114+
self.monosig.push_binding(param, v);
115+
}
116+
99117
// Make sure all assertions generated by existential parameters evaluate to true
100118
// The type checker ensures this cannot happen for Filament-level
101119
// components but externally generated components might violate their
@@ -153,19 +171,6 @@ impl MonoDeferred<'_, '_> {
153171
self.monosig.base.extend_cmds(cmd);
154172
}
155173

156-
// Extend the binding with existential parameters
157-
let info = self.pass.inst_info(&self.monosig.comp_key);
158-
for param in self.underlying.exist_params() {
159-
let param = param.ul();
160-
let Some(v) = info.get_exist_val(param) else {
161-
unreachable!(
162-
"No binding for existential parameter `{}'. Is the body missing an assignment to the parameter?",
163-
self.underlying.display(param)
164-
)
165-
};
166-
self.monosig.push_binding(param, v);
167-
}
168-
169174
// Monomorphize the rest of the signature
170175
self.sig_complete_mono();
171176

@@ -372,22 +377,10 @@ impl MonoDeferred<'_, '_> {
372377
None
373378
}
374379
ir::Command::Exists(ir::Exists { param, expr }) => {
375-
let comp_key = self.monosig.comp_key.clone();
376-
let e = self
377-
.monosig
378-
.expr(&self.underlying, expr.ul(), self.pass)
379-
.get();
380-
let base_comp = self.monosig.base.comp();
381-
let Some(v) = e.as_concrete(base_comp) else {
382-
unreachable!(
383-
"exists binding evaluated to: {}",
384-
base_comp.display(e)
385-
)
386-
};
380+
let e =
381+
self.monosig.expr(&self.underlying, expr.ul(), self.pass);
387382

388-
self.pass
389-
.inst_info_mut(comp_key)
390-
.add_exist_val(param.ul(), v);
383+
self.exist_params.push(param.ul(), e);
391384
None
392385
}
393386
// XXX(rachit): We completely get rid of facts in the program here.

crates/filament/src/ir_passes/mono/utils/comp.rs

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -130,6 +130,18 @@ impl BaseComp {
130130
pub fn resolve_prop(&mut self, prop: ir::Prop) -> Base<ir::Prop> {
131131
self.0.resolve_prop(prop).base()
132132
}
133+
134+
pub fn inputs(
135+
&self,
136+
) -> impl Iterator<Item = (Base<ir::Port>, &'_ ir::Port)> {
137+
self.0.inputs().map(|(k, v)| (k.base(), v))
138+
}
139+
140+
pub fn outputs(
141+
&self,
142+
) -> impl Iterator<Item = (Base<ir::Port>, &'_ ir::Port)> {
143+
self.0.outputs().map(|(k, v)| (k.base(), v))
144+
}
133145
}
134146

135147
impl<T> MutCtx<T, Base<T>> for BaseComp
Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,7 @@
11
mod combinational_paths;
2-
mod pass;
32
mod retime;
43
mod solve;
54

65
use combinational_paths::CombDataflow;
7-
pub use pass::Schedule;
86
use retime::Retime;
97
use solve::Solve;

crates/filament/src/ir_passes/schedule/pass.rs

Lines changed: 0 additions & 27 deletions
This file was deleted.

crates/filament/src/ir_passes/schedule/solve.rs

Lines changed: 60 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,11 @@
11
use super::CombDataflow;
2-
use crate::ir_visitor::{Action, Construct, Visitor, VisitorData};
2+
use crate::{
3+
ir_passes::{
4+
Monomorphize,
5+
mono::{BaseComp, MonoSig, Underlying, UnderlyingComp},
6+
},
7+
ir_visitor::{Action, Construct, Visitor, VisitorData},
8+
};
39
use easy_smt::{self as smt, SExpr, SExprData};
410
use fil_ir::{self as ir, AddCtx, Ctx, DisplayCtx, MutCtx};
511
use fil_utils::{AttrCtx, CompNum};
@@ -23,22 +29,59 @@ impl From<u64> for SchedulingGoal {
2329
}
2430

2531
/// Sets the proper FSM Attributes for every component
26-
pub struct Solve {
32+
pub struct Solve<'comp, 'pass: 'comp> {
2733
/// Solver context
2834
sol: smt::Context,
2935
/// Scheduling goal
3036
goal: SchedulingGoal,
3137
/// The expression to minimize
3238
minimize_expr: smt::SExpr,
33-
// /// Map from ir elements to SExprs
34-
// expr_map: ir::SparseInfoMap<ir::Expr, SExpr>,
35-
// port_map: ir::SparseInfoMap<ir::PortIdx, SExpr>,
36-
// event_map: ir::SparseInfoMap<ir::EventIdx, SExpr>,
37-
// time_map: ir::SparseInfoMap<ir::TimeIdx, SExpr>,
38-
// prop_map: ir::SparseInfoMap<ir::PropIdx, SExpr>,
39+
40+
/// The underlying component to be monomorphized
41+
pub underlying_idx: Underlying<ir::Component>,
42+
/// Underlying pointer
43+
pub pass: &'comp mut Monomorphize<'pass>,
44+
/// Struct to keep track of all the mapping information from things owned by
45+
/// `underlying` to things owned by `base`
46+
pub monosig: &'comp MonoSig,
3947
}
4048

41-
impl Solve {
49+
impl<'comp, 'pass> Solve<'comp, 'pass>
50+
where
51+
'pass: 'comp,
52+
{
53+
fn new(
54+
underlying_idx: Underlying<ir::Component>,
55+
pass: &'comp mut Monomorphize<'pass>,
56+
monosig: &'comp MonoSig,
57+
goal: u64,
58+
solver_file: Option<&str>,
59+
) -> Self {
60+
// We have to use Z3 as only it supports maximization of an objective function
61+
let (name, s_opts) = ("z3", vec!["-smt2", "-in"]);
62+
63+
let mut sol = smt::ContextBuilder::new()
64+
.replay_file(
65+
solver_file.as_ref().map(|s| fs::File::create(s).unwrap()),
66+
)
67+
.solver(name, s_opts)
68+
.build()
69+
.unwrap();
70+
71+
sol.push_many(1).unwrap();
72+
73+
Self {
74+
underlying_idx,
75+
pass,
76+
monosig,
77+
minimize_expr: sol.numeral(0),
78+
goal: goal.into(),
79+
sol,
80+
}
81+
}
82+
}
83+
84+
impl Solve<'_, '_> {
4285
/// Get the constant names for the start and end of a port
4386
pub fn get_port_name(&self, pidx: ir::PortIdx) -> (String, String) {
4487
(
@@ -225,59 +268,15 @@ impl Solve {
225268
}
226269
}
227270

228-
impl Construct for Solve {
229-
fn from(opts: &crate::cmdline::Opts, _: &mut ir::Context) -> Self {
230-
// We have to use Z3 as only it supports maximization of an objective function
231-
let (name, s_opts) = ("z3", vec!["-smt2", "-in"]);
232-
233-
let mut sol = smt::ContextBuilder::new()
234-
.replay_file(
235-
opts.solver_replay_file
236-
.as_ref()
237-
.map(|s| fs::File::create(s).unwrap()),
238-
)
239-
.solver(name, s_opts)
240-
.build()
241-
.unwrap();
242-
243-
sol.push_many(1).unwrap();
244-
245-
Self {
246-
minimize_expr: sol.numeral(0),
247-
goal: SchedulingGoal::Latency,
248-
sol,
249-
}
250-
}
251-
252-
fn clear_data(&mut self) {
253-
// Create a new solver context
254-
self.sol.pop_many(1).unwrap();
255-
self.sol.push_many(1).unwrap();
256-
}
257-
}
258-
259-
impl Visitor for Solve {
260-
fn name() -> &'static str {
261-
"schedule-solve"
262-
}
263-
264-
fn start(&mut self, data: &mut VisitorData) -> Action {
265-
// Quit the pass if this attribute does not have the #[schedule] attribute
266-
if let Some(&goal) = data.comp.attrs.get(CompNum::Schedule) {
267-
self.goal = goal.into()
268-
} else {
269-
return Action::Stop;
270-
}
271-
272-
// make sure this component only has one event
273-
assert_eq!(
274-
data.comp.events().idx_iter().count(),
275-
1,
276-
"Attempting to schedule a component with multiple events"
277-
);
278-
271+
impl Solve<'_, '_> {
272+
fn comp(&mut self) -> Action {
279273
// For the inputs and outputs of the component, we need to schedule them as expected.
280-
for (pidx, port) in data.comp.inputs().chain(data.comp.outputs()) {
274+
for (pidx, port) in self
275+
.monosig
276+
.base
277+
.inputs()
278+
.chain(self.monosig.base.outputs())
279+
{
281280
let ir::Range { start, end } = port.live.range;
282281

283282
let start = data.comp.get(start).offset.concrete(&data.comp);
@@ -304,8 +303,6 @@ impl Visitor for Solve {
304303
.assert(self.sol.eq(self.sol.numeral(end), end_expr))
305304
.unwrap();
306305
}
307-
308-
Action::Continue
309306
}
310307

311308
fn connect(

crates/filament/src/main.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -95,8 +95,7 @@ fn run(opts: &cmdline::Opts) -> Result<(), u64> {
9595
ip::Simplify,
9696
ip::AssignCheck,
9797
ip::BundleElim,
98-
ip::AssignCheck,
99-
ip::Schedule
98+
ip::AssignCheck
10099
}
101100
// type check again before lowering
102101
ir_pass_pipeline! {opts, ir;

tests/schedule/test.fil

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,14 @@ comp main<'G: 1>(
55
in: ['G, 'G+1] 32,
66
) -> (
77
out: ['G+10, 'G+11] 32
8-
)
8+
) with {
9+
some L;
10+
}
911
{
1012
let x = ?;
1113
let xx = 2;
1214
let y = x + xx;
1315
let z = y + 1;
16+
17+
L := z;
1418
}

0 commit comments

Comments
 (0)