@@ -29,22 +29,22 @@ impl<'a> Validate<'a> {
2929 /// Validate the entire component
3030 fn comp ( & self ) {
3131 // Validate ports
32- for ( pidx, _ ) in self . comp . ports ( ) . iter ( ) {
32+ for pidx in self . comp . ports ( ) . idx_iter ( ) {
3333 self . port ( pidx) ;
3434 }
3535
3636 // Validate params
37- for ( pidx, _ ) in self . comp . params ( ) . iter ( ) {
37+ for pidx in self . comp . params ( ) . idx_iter ( ) {
3838 self . param ( pidx) ;
3939 }
4040
4141 // Validate invokes
42- for ( iidx, _ ) in self . comp . invocations ( ) . iter ( ) {
42+ for iidx in self . comp . invocations ( ) . idx_iter ( ) {
4343 self . invoke ( iidx) ;
4444 }
4545
4646 // Validate instances
47- for ( iidx, _ ) in self . comp . instances ( ) . iter ( ) {
47+ for iidx in self . comp . instances ( ) . idx_iter ( ) {
4848 self . instance ( iidx) ;
4949 }
5050
@@ -57,13 +57,19 @@ impl<'a> Validate<'a> {
5757 /// A Port is valid if:
5858 /// (1) All bundle-owned params point to this port
5959 /// (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:
6160 /// (3) All time expressions are bound
6261 /// (4) All parameters mentioned in the range and the width are bound
6362 fn port ( & self , pidx : ir:: PortIdx ) {
64- let ir:: Port { owner, live, .. } = self . comp . get ( pidx) ;
63+ let ir:: Port {
64+ owner, live, width, ..
65+ } = self . comp . get ( pidx) ;
6566 // check (1)
66- let ir:: Liveness { idxs : par_idxs, .. } = live;
67+ let ir:: Liveness {
68+ idxs : par_idxs,
69+ lens,
70+ range,
71+ } = live;
72+
6773 for par_idx in par_idxs {
6874 match self . comp . get ( * par_idx) . owner {
6975 ir:: ParamOwner :: Let { .. } => self . comp . internal_error ( format ! (
@@ -121,19 +127,27 @@ impl<'a> Validate<'a> {
121127 }
122128 }
123129 }
130+
131+ // check (3)
132+ self . range ( range) ;
133+
134+ // check (4)
135+ self . expr ( * width) ;
136+ for len in lens {
137+ self . expr ( * len) ;
138+ }
124139 }
125140
126141 /// An invoke is valid if:
127142 /// (1) Its ports are defined in the component
128143 /// (2) Ports defined by invoke point to it
129144 /// i. port() checks that the invoke owns the port
130145 /// 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
146+ /// (3) Its event bindings are valid
133147 fn invoke ( & self , iidx : ir:: InvIdx ) {
134148 assert ! ( self . comp. valid( iidx) ) ;
135149
136- let ir:: Invoke { ports, .. } = & self . comp . get ( iidx) ;
150+ let ir:: Invoke { ports, events , .. } = & self . comp . get ( iidx) ;
137151
138152 // check (1) and (2)
139153 for pidx in ports {
@@ -157,28 +171,51 @@ impl<'a> Validate<'a> {
157171 }
158172 }
159173 }
174+ // check (3)
175+ for ir:: EventBind {
176+ arg, delay, base, ..
177+ } in events
178+ {
179+ self . time ( * arg) ;
180+ self . timesub ( delay) ;
181+ // Validate that the foreign event exists
182+ assert ! ( base. apply( |e, c| c. valid( e) , self . ctx) ) ;
183+ }
160184 }
161185
162186 /// An instance is valid if:
163187 /// (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
188+ /// (2) Its existential params are defined in the component
189+ /// (3) Its ranges are valid
190+ /// (4) The component it's instantiating is defined in the context
191+ /// (5) The number of params passed in matches the amount present
167192 /// in the component signature
168193 fn instance ( & self , iidx : ir:: InstIdx ) {
169194 // check (1)
170195 let ir:: Instance {
171- comp, args : params, ..
196+ comp,
197+ args,
198+ params,
199+ lives,
200+ ..
172201 } = & self . comp [ iidx] ;
173- // check (3) and (4)
202+ // check (2)
203+ for param in params {
204+ self . param ( * param) ;
205+ }
206+ // check (3)
207+ for live in lives {
208+ self . range ( live) ;
209+ }
210+ // check (4) and (5)
174211 let comp_params = self
175212 . ctx
176213 . get ( * comp)
177214 . params ( )
178215 . iter ( )
179216 . filter ( |( _, param) | param. is_sig_owned ( ) )
180217 . count ( ) ;
181- let inst_len = params . len ( ) ;
218+ let inst_len = args . len ( ) ;
182219 if comp_params != inst_len {
183220 self . comp . internal_error (
184221 format ! ( "{comp} takes {comp_params} params, but {inst_len} were passed by {iidx}" )
@@ -187,6 +224,7 @@ impl<'a> Validate<'a> {
187224 }
188225
189226 fn bundle_def ( & self , b : ir:: PortIdx ) {
227+ self . port ( b) ;
190228 // The port in a bundle def must have a local owner
191229 let ir:: Port { owner, .. } = & self . comp [ b] ;
192230 match owner {
@@ -207,12 +245,16 @@ impl<'a> Validate<'a> {
207245 ir:: Command :: ForLoop ( lp) => self . forloop ( lp) ,
208246 ir:: Command :: If ( cond) => self . if_stmt ( cond) ,
209247 ir:: Command :: Let ( l) => self . let_ ( l) ,
210- ir:: Command :: Fact ( _ ) => ( ) ,
248+ ir:: Command :: Fact ( f ) => self . fact ( f ) ,
211249 ir:: Command :: BundleDef ( b) => self . bundle_def ( * b) ,
212250 ir:: Command :: Exists ( e) => self . exists ( e) ,
213251 }
214252 }
215253
254+ fn fact ( & self , fact : & ir:: Fact ) {
255+ self . prop ( fact. prop ) ;
256+ }
257+
216258 fn let_ ( & self , l : & ir:: Let ) {
217259 let ir:: Let { param, expr } = l;
218260 let owner = & self . comp [ * param] . owner ;
@@ -251,23 +293,37 @@ impl<'a> Validate<'a> {
251293
252294 /// An access is valid if:
253295 /// (1) The port being accessed is valid
254- /// (2) Its start and end exprs are defined in the comp
296+ /// (2) The start and end exprs of its ranges are defined in the comp
255297 fn access ( & self , access : & ir:: Access ) {
256- let ir:: Access { port, .. } = * access;
257- self . port ( port) ;
258- // self.expr(start);
259- // self.expr(end);
298+ let ir:: Access { port, ranges } = access;
299+ self . port ( * port) ;
300+ for ( start, end) in ranges {
301+ self . expr ( * start) ;
302+ self . expr ( * end) ;
303+ }
260304 }
261305
262306 /// A loop is valid if:
263- /// (1) Its index is valid
307+ /// (1) Its index is valid and owned by a loop
264308 /// (2) Its start/end is valid
265309 /// (3) Everything in its body is valid
266310 fn forloop ( & self , lp : & ir:: Loop ) {
267- let ir:: Loop { body, .. } = lp;
268- // self.param(*index);
269- // self.expr(*start);
270- // self.expr(*end);
311+ let ir:: Loop {
312+ body,
313+ start,
314+ end,
315+ index,
316+ } = lp;
317+ let param = self . comp . get ( * index) ;
318+ if !matches ! ( param. owner, ir:: ParamOwner :: Loop ) {
319+ self . comp . internal_error ( format ! (
320+ "{} mentioned in loop but owned by {}" ,
321+ self . comp. display( * index) ,
322+ param. owner
323+ ) )
324+ }
325+ self . expr ( * start) ;
326+ self . expr ( * end) ;
271327 for cmd in body {
272328 self . command ( cmd) ;
273329 }
@@ -278,16 +334,20 @@ impl<'a> Validate<'a> {
278334 /// (2) Everything in its then-branch is valid
279335 /// (3) Everything in its alt-branch is valid
280336 fn if_stmt ( & self , if_stmt : & ir:: If ) {
281- let ir:: If { then, alt, .. } = if_stmt;
337+ let ir:: If { cond, then, alt } = if_stmt;
338+ // check (1)
339+ self . prop ( * cond) ;
340+ // check (2)
282341 for cmd in then {
283342 self . command ( cmd) ;
284343 }
344+ // check (3)
285345 for cmd in alt {
286346 self . command ( cmd) ;
287347 }
288348 }
289349 fn exists ( & self , exists : & ir:: Exists ) {
290- let ir:: Exists { param : p_idx, .. } = exists;
350+ let ir:: Exists { param : p_idx, expr } = exists;
291351 let param = self . comp . get ( * p_idx) ;
292352 // let param = self.param(*p_idx);
293353 if !matches ! ( param. owner, ir:: ParamOwner :: Exists { .. } ) {
@@ -297,6 +357,36 @@ impl<'a> Validate<'a> {
297357 param. owner
298358 ) )
299359 }
300- // self.expr(*expr);
360+ self . expr ( * expr) ;
361+ }
362+
363+ /// A prop is valid iff all of its fields are valid
364+ fn prop ( & self , pidx : ir:: PropIdx ) {
365+ assert ! ( pidx. valid( self . comp) ) ;
366+ }
367+
368+ /// An expr is valid iff all of its arguments are valid
369+ fn expr ( & self , eidx : ir:: ExprIdx ) {
370+ assert ! ( eidx. valid( self . comp) ) ;
371+ }
372+
373+ /// A time is valid iff all of its arguments are valid
374+ fn time ( & self , tidx : ir:: TimeIdx ) {
375+ assert ! ( tidx. valid( self . comp) ) ;
376+ }
377+
378+ fn timesub ( & self , ts : & ir:: TimeSub ) {
379+ match ts {
380+ crate :: TimeSub :: Unit ( idx) => self . expr ( * idx) ,
381+ crate :: TimeSub :: Sym { l, r } => {
382+ self . time ( * l) ;
383+ self . time ( * r) ;
384+ }
385+ }
386+ }
387+
388+ fn range ( & self , r : & ir:: Range ) {
389+ self . time ( r. start ) ;
390+ self . time ( r. end ) ;
301391 }
302392}
0 commit comments