blog-static/code/dyno-alloy/DynoAlloy.als

enum Flag {Method, MethodOrField, Public}

/* There is a negative version for each flag (METHOD and NOT_METHOD).
     Model this as two sets, one of positive flags, and one of netative flags,
     and interpret the bitfield to be a conjunction of both flags. */
sig Bitfield {
    , positiveFlags: set Flag
    , negativeFlags: set Flag
}

/* A filter state has filterFlags and excludeFlags, both represented as conjunctions. */ 
sig FilterState {
    , curFilter: Bitfield
}

/* Initially, no search has happeneed for a scope, so its 'found' is not set to anything. */
one sig NotSet {}

/* Finally, there's a search state (whether or not a particular scope has already been
    searched with a particular configuration). */
one sig SearchState {
    , var found: Bitfield + NotSet
}


pred bitfieldEmpty[b: Bitfield] {
    #b.positiveFlags = 0 and #b.negativeFlags = 0
}

pred bitfieldEqual[b1: Bitfield, b2: Bitfield] {
    b1.positiveFlags = b2.positiveFlags and b1.negativeFlags = b2.negativeFlags
}

pred bitfieldIntersection[b1: Bitfield, b2: Bitfield, b3: Bitfield] {
    b3.positiveFlags = b1.positiveFlags & b2.positiveFlags
    b3.negativeFlags = b1.negativeFlags & b2.negativeFlags
}

pred bitfieldSubset[b1: Bitfield, b2: Bitfield] {
    b1.positiveFlags in b2.positiveFlags
    b1.negativeFlags in b2.negativeFlags
}

pred bitfieldIncomparable[b1: Bitfield, b2: Bitfield] {
    not bitfieldSubset[b1, b2]
    not bitfieldSubset[b2, b1]
}

pred addBitfieldFlag[b1: Bitfield, b2: Bitfield, flag: Flag] {
    b2.positiveFlags = b1.positiveFlags + flag
    b2.negativeFlags = b1.negativeFlags
}

pred addBitfieldFlagNeg[b1: Bitfield, b2: Bitfield, flag: Flag] {
    b2.negativeFlags = b1.negativeFlags + flag
    b2.positiveFlags = b1.positiveFlags
}

enum Property { PMethod, PField, PPublic }

sig Symbol {
    properties: set Property
}

pred flagMatchesProperty[flag: Flag, property: Property] {
    (flag = Method and property = PMethod) or
    (flag = MethodOrField and (property = PMethod or property = PField)) or
    (flag = Public and property = PPublic)
}

pred bitfieldMatchesProperties[bitfield: Bitfield, symbol: Symbol] {
    all flag: bitfield.positiveFlags | some property: symbol.properties | flagMatchesProperty[flag, property]
    all flag: bitfield.negativeFlags | no property: symbol.properties | flagMatchesProperty[flag, property]
}

bitfieldExists: run {
    some Bitfield
}

matchingBitfieldExists: run {
    some bitfield : Bitfield, symbol : Symbol | bitfieldMatchesProperties[bitfield, symbol]
}

matchingBitfieldExists2: run {
    some bitfield : Bitfield, symbol : Symbol {
        #bitfield.positiveFlags = 1
        #bitfield.negativeFlags = 1
        #symbol.properties = 2
        bitfieldMatchesProperties[bitfield, symbol]
    }
}

fact "method and field are incompatible" {
    always no symbol: Symbol | {
        PMethod in symbol.properties and PField in symbol.properties
    }
}

fact "public and field are incompatible" {
    always no symbol: Symbol | {
        PPublic in symbol.properties and PField in symbol.properties
    }
}

matchingBitfieldExists3: run {
    some bitfield : Bitfield, symbol : Symbol {
        #bitfield.positiveFlags = 2
        #symbol.properties = 2
        bitfieldMatchesProperties[bitfield, symbol]
    }
}

pred possibleState[filterState: FilterState] {
    some initialState: FilterState {
        // Each lookup in scope starts with empty filter flags
        bitfieldEmpty[initialState.curFilter]

        // The intermediate states (bitfieldMiddle) are used for sequencing of operations.
        some bitfieldMiddle : Bitfield {
            // Add "Public" depending on skipPrivateVisibilities
            addBitfieldFlag[initialState.curFilter, bitfieldMiddle, Public] or
            bitfieldEqual[initialState.curFilter, bitfieldMiddle]

            // If it's a method receiver, add method or field restriction
            addBitfieldFlag[bitfieldMiddle, filterState.curFilter, MethodOrField] or
            // if it's not a receiver, filter to non-methods (could be overridden)
            // addBitfieldFlagNeg[bitfieldMiddle, filterState.curFilter, Method] or
            // Maybe methods are not being curFilterd but it's not a receiver, so no change.
            bitfieldEqual[bitfieldMiddle, filterState.curFilter]
        }
    }
}

possibleStateExists: run {
    some filterState : FilterState | possibleState[filterState] and #filterState.curFilter.positiveFlags = 1
}

pred update[toSet: Bitfield + NotSet, setTo: FilterState] {
    toSet' in Bitfield and bitfieldIntersection[toSet, setTo.curFilter, toSet']
}

pred newUpdate[toSet: Bitfield + NotSet, setTo: FilterState] {
    (not bitfieldIncomparable[toSet, setTo.curFilter] and update[toSet, setTo]) or
    (bitfieldIncomparable[toSet, setTo.curFilter] and toSet = toSet')
}

pred updateOrSet[toSet: Bitfield + NotSet, setTo: FilterState] {
    (toSet in NotSet and toSet' = setTo.curFilter) or
    (toSet not in NotSet and update[toSet, setTo])
}

pred excludeBitfield[found: Bitfield + NotSet, exclude: Bitfield] {
    (found != NotSet and bitfieldEqual[found, exclude]) or
    (found = NotSet and bitfieldEmpty[exclude])
}

fact init {
    all searchState: SearchState | searchState.found = NotSet
}

fact step {
    always {
        // Model that a new doLookupInScope could've occurred, with any combination of flags.
        all searchState: SearchState {
            some fs: FilterState {
                // This is a possible combination of lookup flags
                possibleState[fs]

                // If a search has been performed before, take the intersection; otherwise,
                // just insert the current filter flags.
                updateOrSet[searchState.found, fs]
            }
        }
    }
}

counterexampleNotFound: run {
    all searchState: SearchState {
        // a way that subsequent results of searching will miss things.
        eventually some symbol: Symbol,
                        fs: FilterState, fsBroken: FilterState,
                        exclude1: Bitfield, exclude2: Bitfield {
            // Some search (fs) will cause a transition / modification of the search state...
            possibleState[fs]
            updateOrSet[searchState.found, fs]
            excludeBitfield[searchState.found, exclude1]
            // Such that a later, valid search... (fsBroken)
            possibleState[fsBroken]
            excludeBitfield[searchState.found', exclude2]

            // Will allow for a symbol ...
            // ... that are left out of the original search...
            not bitfieldMatchesProperties[searchState.found, symbol]
            // ... and out of the current search
            not (bitfieldMatchesProperties[fs.curFilter, symbol] and not bitfieldMatchesProperties[exclude1, symbol])
            // But would be matched by the broken search...
            bitfieldMatchesProperties[fsBroken.curFilter, symbol]
            // ... to not be matched by a search with the new state:
            not (bitfieldMatchesProperties[fsBroken.curFilter, symbol] and not bitfieldMatchesProperties[exclude2, symbol])
        }
    }
}