@@ -26,25 +26,29 @@ impl<'a> Validate<'a> {
2626 assert ! ( self . comp. valid( p) ) ;
2727 }
2828
29+ fn event ( & self , e : ir:: EventIdx ) {
30+ assert ! ( self . comp. valid( e) ) ;
31+ }
32+
2933 /// Validate the entire component
3034 fn comp ( & self ) {
3135 // Validate ports
32- for ( pidx, _ ) in self . comp . ports ( ) . iter ( ) {
36+ for pidx in self . comp . ports ( ) . idx_iter ( ) {
3337 self . port ( pidx) ;
3438 }
3539
3640 // Validate params
37- for ( pidx, _ ) in self . comp . params ( ) . iter ( ) {
41+ for pidx in self . comp . params ( ) . idx_iter ( ) {
3842 self . param ( pidx) ;
3943 }
4044
4145 // Validate invokes
42- for ( iidx, _ ) in self . comp . invocations ( ) . iter ( ) {
46+ for iidx in self . comp . invocations ( ) . idx_iter ( ) {
4347 self . invoke ( iidx) ;
4448 }
4549
4650 // Validate instances
47- for ( iidx, _ ) in self . comp . instances ( ) . iter ( ) {
51+ for iidx in self . comp . instances ( ) . idx_iter ( ) {
4852 self . instance ( iidx) ;
4953 }
5054
@@ -57,13 +61,19 @@ impl<'a> Validate<'a> {
5761 /// A Port is valid if:
5862 /// (1) All bundle-owned params point to this port
5963 /// (2) The port's owner is defined in the component and the owner says it owns the port
60- /// NOTE(rachit): A more pedantic check can enforce these in the future:
6164 /// (3) All time expressions are bound
6265 /// (4) All parameters mentioned in the range and the width are bound
6366 fn port ( & self , pidx : ir:: PortIdx ) {
64- let ir:: Port { owner, live, .. } = self . comp . get ( pidx) ;
67+ let ir:: Port {
68+ owner, live, width, ..
69+ } = self . comp . get ( pidx) ;
6570 // check (1)
66- let ir:: Liveness { idxs : par_idxs, .. } = live;
71+ let ir:: Liveness {
72+ idxs : par_idxs,
73+ lens,
74+ range,
75+ } = live;
76+
6777 for par_idx in par_idxs {
6878 match self . comp . get ( * par_idx) . owner {
6979 ir:: ParamOwner :: Let { .. } => self . comp . internal_error ( format ! (
@@ -121,19 +131,27 @@ impl<'a> Validate<'a> {
121131 }
122132 }
123133 }
134+
135+ // check (3)
136+ self . range ( range) ;
137+
138+ // check (4)
139+ self . expr ( * width) ;
140+ for len in lens {
141+ self . expr ( * len) ;
142+ }
124143 }
125144
126145 /// An invoke is valid if:
127146 /// (1) Its ports are defined in the component
128147 /// (2) Ports defined by invoke point to it
129148 /// i. port() checks that the invoke owns the port
130149 /// invoke() checks that the ports an invoke defines are owned by it
131- /// (3) Its events are valid
132- /// (4) Its events point to the invoke as their owner
150+ /// (3) Its event bindings
133151 fn invoke ( & self , iidx : ir:: InvIdx ) {
134152 assert ! ( self . comp. valid( iidx) ) ;
135153
136- let ir:: Invoke { ports, .. } = & self . comp . get ( iidx) ;
154+ let ir:: Invoke { ports, events , .. } = & self . comp . get ( iidx) ;
137155
138156 // check (1) and (2)
139157 for pidx in ports {
@@ -157,28 +175,51 @@ impl<'a> Validate<'a> {
157175 }
158176 }
159177 }
178+ // check (3)
179+ for ir:: EventBind {
180+ arg, delay, base, ..
181+ } in events
182+ {
183+ self . time ( * arg) ;
184+ self . timesub ( delay) ;
185+ // Validate that the foreign event exists
186+ assert ! ( base. apply( |e, c| c. valid( e) , self . ctx) ) ;
187+ }
160188 }
161189
162190 /// An instance is valid if:
163191 /// (1) It is defined in the component
164- /// (2) Its params are defined in the component
165- /// (3) The component it's instantiating is defined in the context
166- /// (4) The number of params passed in matches the amount present
192+ /// (2) Its existential params are defined in the component
193+ /// (3) Its ranges are valid
194+ /// (4) The component it's instantiating is defined in the context
195+ /// (5) The number of params passed in matches the amount present
167196 /// in the component signature
168197 fn instance ( & self , iidx : ir:: InstIdx ) {
169198 // check (1)
170199 let ir:: Instance {
171- comp, args : params, ..
200+ comp,
201+ args,
202+ params,
203+ lives,
204+ ..
172205 } = & self . comp [ iidx] ;
173- // check (3) and (4)
206+ // check (2)
207+ for param in params {
208+ self . param ( * param) ;
209+ }
210+ // check (3)
211+ for live in lives {
212+ self . range ( live) ;
213+ }
214+ // check (4) and (5)
174215 let comp_params = self
175216 . ctx
176217 . get ( * comp)
177218 . params ( )
178219 . iter ( )
179220 . filter ( |( _, param) | param. is_sig_owned ( ) )
180221 . count ( ) ;
181- let inst_len = params . len ( ) ;
222+ let inst_len = args . len ( ) ;
182223 if comp_params != inst_len {
183224 self . comp . internal_error (
184225 format ! ( "{comp} takes {comp_params} params, but {inst_len} were passed by {iidx}" )
@@ -207,12 +248,16 @@ impl<'a> Validate<'a> {
207248 ir:: Command :: ForLoop ( lp) => self . forloop ( lp) ,
208249 ir:: Command :: If ( cond) => self . if_stmt ( cond) ,
209250 ir:: Command :: Let ( l) => self . let_ ( l) ,
210- ir:: Command :: Fact ( _ ) => ( ) ,
251+ ir:: Command :: Fact ( f ) => self . fact ( f ) ,
211252 ir:: Command :: BundleDef ( b) => self . bundle_def ( * b) ,
212253 ir:: Command :: Exists ( e) => self . exists ( e) ,
213254 }
214255 }
215256
257+ fn fact ( & self , fact : & ir:: Fact ) {
258+ self . prop ( fact. prop ) ;
259+ }
260+
216261 fn let_ ( & self , l : & ir:: Let ) {
217262 let ir:: Let { param, expr } = l;
218263 let owner = & self . comp [ * param] . owner ;
@@ -251,23 +296,37 @@ impl<'a> Validate<'a> {
251296
252297 /// An access is valid if:
253298 /// (1) The port being accessed is valid
254- /// (2) Its start and end exprs are defined in the comp
299+ /// (2) The start and end exprs of its ranges are defined in the comp
255300 fn access ( & self , access : & ir:: Access ) {
256- let ir:: Access { port, .. } = * access;
257- self . port ( port) ;
258- // self.expr(start);
259- // self.expr(end);
301+ let ir:: Access { port, ranges } = access;
302+ self . port ( * port) ;
303+ for ( start, end) in ranges {
304+ self . expr ( * start) ;
305+ self . expr ( * end) ;
306+ }
260307 }
261308
262309 /// A loop is valid if:
263- /// (1) Its index is valid
310+ /// (1) Its index is valid and owned by a loop
264311 /// (2) Its start/end is valid
265312 /// (3) Everything in its body is valid
266313 fn forloop ( & self , lp : & ir:: Loop ) {
267- let ir:: Loop { body, .. } = lp;
268- // self.param(*index);
269- // self.expr(*start);
270- // self.expr(*end);
314+ let ir:: Loop {
315+ body,
316+ start,
317+ end,
318+ index,
319+ } = lp;
320+ let param = self . comp . get ( * index) ;
321+ if !matches ! ( param. owner, ir:: ParamOwner :: Loop ) {
322+ self . comp . internal_error ( format ! (
323+ "{} mentioned in loop but owned by {}" ,
324+ self . comp. display( * index) ,
325+ param. owner
326+ ) )
327+ }
328+ self . expr ( * start) ;
329+ self . expr ( * end) ;
271330 for cmd in body {
272331 self . command ( cmd) ;
273332 }
@@ -278,16 +337,20 @@ impl<'a> Validate<'a> {
278337 /// (2) Everything in its then-branch is valid
279338 /// (3) Everything in its alt-branch is valid
280339 fn if_stmt ( & self , if_stmt : & ir:: If ) {
281- let ir:: If { then, alt, .. } = if_stmt;
340+ let ir:: If { cond, then, alt } = if_stmt;
341+ // check (1)
342+ self . prop ( * cond) ;
343+ // check (2)
282344 for cmd in then {
283345 self . command ( cmd) ;
284346 }
347+ // check (3)
285348 for cmd in alt {
286349 self . command ( cmd) ;
287350 }
288351 }
289352 fn exists ( & self , exists : & ir:: Exists ) {
290- let ir:: Exists { param : p_idx, .. } = exists;
353+ let ir:: Exists { param : p_idx, expr } = exists;
291354 let param = self . comp . get ( * p_idx) ;
292355 // let param = self.param(*p_idx);
293356 if !matches ! ( param. owner, ir:: ParamOwner :: Exists { .. } ) {
@@ -297,6 +360,36 @@ impl<'a> Validate<'a> {
297360 param. owner
298361 ) )
299362 }
300- // self.expr(*expr);
363+ self . expr ( * expr) ;
364+ }
365+
366+ /// A prop is valid iff all of its fields are valid
367+ fn prop ( & self , pidx : ir:: PropIdx ) {
368+ pidx. valid ( self . comp ) ;
369+ }
370+
371+ /// An expr is valid iff all of its arguments are valid
372+ fn expr ( & self , eidx : ir:: ExprIdx ) {
373+ eidx. valid ( self . comp ) ;
374+ }
375+
376+ /// A time is valid iff all of its arguments are valid
377+ fn time ( & self , tidx : ir:: TimeIdx ) {
378+ tidx. valid ( self . comp ) ;
379+ }
380+
381+ fn timesub ( & self , ts : & ir:: TimeSub ) {
382+ match ts {
383+ crate :: TimeSub :: Unit ( idx) => self . expr ( * idx) ,
384+ crate :: TimeSub :: Sym { l, r } => {
385+ self . time ( * l) ;
386+ self . time ( * r) ;
387+ }
388+ }
389+ }
390+
391+ fn range ( & self , r : & ir:: Range ) {
392+ self . time ( r. start ) ;
393+ self . time ( r. end ) ;
301394 }
302395}
0 commit comments