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

203 lines
7.0 KiB
Alloy

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])
}
}
}