@@ -337,54 +337,91 @@ module LocalNameBinding<LocationSig Location, LocalNameBindingInputSig<Location>
337337 )
338338 }
339339
340- private predicate accessCandInLookupScope ( AstNode n , string name , Scope lookup ) {
341- accessCand ( n , name ) and
342- (
343- lookupStartsAt ( n , lookup )
344- or
345- not lookupStartsAt ( n , _) and
346- lookup = getEnclosingScope ( n )
347- )
348- }
349-
350- pragma [ nomagic]
351- private predicate lookupInScope ( string name , Scope lookup , Scope scope ) {
352- accessCandInLookupScope ( _, name , lookup ) and
353- scope = lookup
354- or
355- exists ( Scope mid |
356- lookupInScope ( name , lookup , mid ) and
357- not declInScope ( name , mid ) and
358- not isTopScope ( mid ) and
359- scope = getEnclosingScope ( mid )
360- )
361- }
362-
363340 private predicate declInScope ( string name , AstNode scope ) {
364341 declInScope ( _, name , scope ) or
365342 implicitDeclInScope ( name , scope )
366343 }
367344
345+ signature predicate accessCandSig ( AstNode n , string name ) ;
346+
368347 /**
369- * Holds if `name`, when resolved from `lookup`, may resolve to one of the uncertain members of `scope`.
348+ * Allows resolution of access candidates.
349+ *
350+ * This is instantiated once by the local name binding library itself in order to populate `LocalAccess`.
351+ * It can be instantiated further by the client, to resolve additional lookups at a later evaluation stage.
370352 */
371- pragma [ nomagic]
372- private predicate lookupInUncertainScope ( string name , Scope lookup , Scope scope ) {
373- lookupInScope ( name , lookup , scope ) and
374- uncertainScope ( scope ) and
375- not declInScope ( name , scope )
353+ module ResolveAccesses< accessCandSig / 2 accessCandInput> {
354+ private predicate accessCandInLookupScope ( AstNode n , string name , Scope lookup ) {
355+ accessCandInput ( n , name ) and
356+ (
357+ lookupStartsAt ( n , lookup )
358+ or
359+ not lookupStartsAt ( n , _) and
360+ lookup = getEnclosingScope ( n )
361+ )
362+ }
363+
364+ pragma [ nomagic]
365+ private predicate lookupInScope ( string name , Scope lookup , Scope scope ) {
366+ accessCandInLookupScope ( _, name , lookup ) and
367+ scope = lookup
368+ or
369+ exists ( Scope mid |
370+ lookupInScope ( name , lookup , mid ) and
371+ not declInScope ( name , mid ) and
372+ not isTopScope ( mid ) and
373+ scope = getEnclosingScope ( mid )
374+ )
375+ }
376+
377+ pragma [ nomagic]
378+ private predicate resolveInScope ( string name , Scope lookup , Local l ) {
379+ exists ( Scope scope | lookupInScope ( name , lookup , scope ) |
380+ l = TExplicitLocal ( _, name , scope ) or
381+ l = TImplicitLocal ( name , scope )
382+ )
383+ }
384+
385+ /** Holds if `access` resolves to `l`. */
386+ predicate access ( AstNode access , Local l ) {
387+ exists ( Scope lookup , string name |
388+ accessCandInLookupScope ( access , name , lookup ) and
389+ resolveInScope ( name , lookup , l )
390+ )
391+ }
392+
393+ /**
394+ * Holds if `name`, when resolved from `lookup`, may resolve to one of the uncertain members of `scope`.
395+ */
396+ pragma [ nomagic]
397+ private predicate lookupInUncertainScope ( string name , Scope lookup , Scope scope ) {
398+ lookupInScope ( name , lookup , scope ) and
399+ uncertainScope ( scope ) and
400+ not declInScope ( name , scope )
401+ }
402+
403+ /**
404+ * Gets an uncertain scope in which the `accessCand` pair may resolve.
405+ */
406+ AstNode getAnUncertainScope ( AstNode access , string name ) {
407+ exists ( Scope lookup |
408+ accessCandInLookupScope ( access , name , lookup ) and
409+ lookupInUncertainScope ( name , lookup , result )
410+ )
411+ }
376412 }
377413
378- /**
379- * Gets an uncertain scope in which the `accessCand` pair may resolve.
380- */
381- AstNode getAnUncertainScope ( AstNode access , string name ) {
382- exists ( Scope lookup |
383- accessCandInLookupScope ( access , name , lookup ) and
384- lookupInUncertainScope ( name , lookup , result )
385- )
414+ private module DefaultAccesses = ResolveAccesses< accessCand / 2 > ;
415+
416+ /** Holds if `access` resolves to `l`. */
417+ cached
418+ private predicate access ( AstNode access , Local l ) {
419+ CachedStage:: ref ( ) and
420+ DefaultAccesses:: access ( access , l )
386421 }
387422
423+ predicate getAnUncertainScope = DefaultAccesses:: getAnUncertainScope / 2 ;
424+
388425 cached
389426 private newtype TLocal =
390427 TExplicitLocal ( AstNode definingNode , string name , AstNode scope ) {
@@ -447,23 +484,10 @@ module LocalNameBinding<LocationSig Location, LocalNameBindingInputSig<Location>
447484 override string getName ( ) { result = name }
448485
449486 override Location getLocation ( ) { result = scope .getLocation ( ) }
450- }
451-
452- pragma [ nomagic]
453- private predicate resolveInScope ( string name , Scope lookup , Local l ) {
454- exists ( Scope scope | lookupInScope ( name , lookup , scope ) |
455- l = TExplicitLocal ( _, name , scope ) or
456- l = TImplicitLocal ( name , scope )
457- )
458- }
459487
460- cached
461- private predicate access ( AstNode access , Local l ) {
462- CachedStage:: ref ( ) and
463- exists ( Scope lookup , string name |
464- accessCandInLookupScope ( access , name , lookup ) and
465- resolveInScope ( name , lookup , l )
466- )
488+ /** Holds if this variable has the given name and scope. */
489+ pragma [ nomagic]
490+ predicate hasNameAndScope ( string name_ , AstNode scope_ ) { name = name_ and scope = scope_ }
467491 }
468492
469493 /** A local access. */
0 commit comments