Documentation ¶
Overview ¶
Package inference implements the inference algorithm in NilAway to automatically infer the nilability of the annotation sites.
Index ¶
- func GobRegister()
- type DeterminedVal
- type Engine
- type ExplainedBool
- type ExplainedFalse
- type ExplainedTrue
- type FalseBecauseAnnotation
- type FalseBecauseDeepConstraint
- type FalseBecauseShallowConstraint
- type InferredMap
- func (*InferredMap) AFact()
- func (i *InferredMap) CheckDeepTypeAnn(name *types.TypeName) (annotation.Val, bool)
- func (i *InferredMap) CheckFieldAnn(fld *types.Var) (annotation.Val, bool)
- func (i *InferredMap) CheckFuncCallSiteParamAnn(key *annotation.CallSiteParamAnnotationKey) (annotation.Val, bool)
- func (i *InferredMap) CheckFuncCallSiteRetAnn(key *annotation.CallSiteRetAnnotationKey) (annotation.Val, bool)
- func (i *InferredMap) CheckFuncParamAnn(fdecl *types.Func, num int) (annotation.Val, bool)
- func (i *InferredMap) CheckFuncRecvAnn(fdecl *types.Func) (annotation.Val, bool)
- func (i *InferredMap) CheckFuncRetAnn(fdecl *types.Func, num int) (annotation.Val, bool)
- func (i *InferredMap) CheckGlobalVarAnn(v *types.Var) (annotation.Val, bool)
- func (i *InferredMap) Export(pass *analysis.Pass)
- func (i *InferredMap) GobDecode(input []byte) error
- func (i *InferredMap) GobEncode() (b []byte, err error)
- func (i *InferredMap) Len() int
- func (i *InferredMap) Load(site primitiveSite) (value InferredVal, ok bool)
- func (i *InferredMap) OrderedRange(f func(primitiveSite, InferredVal) bool)
- func (i *InferredMap) StoreDetermined(site primitiveSite, value ExplainedBool)
- func (i *InferredMap) StoreImplication(from primitiveSite, to primitiveSite, assertion primitiveFullTrigger)
- type InferredVal
- type ModeOfInference
- type TrueBecauseAnnotation
- type TrueBecauseDeepConstraint
- type TrueBecauseShallowConstraint
- type UndeterminedVal
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func GobRegister ¶
func GobRegister()
GobRegister must be called in an `init` function before attempting to run any procedure that can deal with InferredAnnotationMaps as Facts. If not, gob encoding/decoding will be unable to handle the data structures. The called function RegisterName maintains an internal mapping to ensure that the association between names and structs is bijective
Types ¶
type DeterminedVal ¶
type DeterminedVal struct { // Bool marks the reason why this value is determined, e.g., because the annotation says so, // or because it is being passed to a nonnil site. Bool ExplainedBool }
An DeterminedVal placed on annotation site X in an InferredMap indicates that site X must be either nilable or nonnil (see the enclosed ExplainedBool for which one and why) as a result of information that we've observed either in this package or an upstream package. If conflicting ExplainedBoolVals are ever calculated for the same site, this produces an overconstrainedConflict.
type Engine ¶
type Engine struct {
// contains filtered or unexported fields
}
Engine is the structure responsible for running the inference: it contains methods to run various tasks for the inference and stores an internal map that can be obtained by calling Engine.InferredMap.
func (*Engine) InferredMap ¶
func (e *Engine) InferredMap() *InferredMap
InferredMap returns the current inferred annotation map, callers must treat this map as read-only and do not directly modify it. Any further updates must be made via the Engine.
func (*Engine) ObserveAnnotations ¶
func (e *Engine) ObserveAnnotations(pkgAnnotations *annotation.ObservedMap, mode ModeOfInference)
ObserveAnnotations does one of two things. If the inferenceType is FullInfer, then it reads ONLY those annotations that are "set" (a separate flag for both nilability and deep nilability) in an annotation.Val - corresponding to syntactically provided annotations but not default annotations. Otherwise, it reads ALL values from the map pkgAnnotations including non-syntactically present annotations that simply arose from defaults. In this latter case, the subsequent calls to observeAssertion below cannot determine any local annotation sites, because they're all already determined, but they can yield failures.
func (*Engine) ObservePackage ¶
func (e *Engine) ObservePackage(pkgFullTriggers []annotation.FullTrigger)
ObservePackage observes all the annotations and assertions computed locally about the current package. The assertions are sorted based on whether they are already known to trigger without reliance on annotation sites, such as `x` in `x = nil; x.f`, which will generate `SingleAssertionFailure`s, whether they rely on only a single annotation site, determining that annotation site as a <Val>BecauseShallowConstraint by a call to observeSiteExplanation if necessary, or whether they rely on two annotation sites, in which case they result in a call to observeImplication. Before all assertions are sorted and handled thus, the annotations read for the package are iterated over and observed via calls to observeSiteExplanation as a <Val>BecauseAnnotation.
func (*Engine) ObserveUpstream ¶
func (e *Engine) ObserveUpstream()
ObserveUpstream imports all information from upstream dependencies. Specifically, it iterates over the direct imports of the passed pass's package, using the Facts mechanism to observe any InferredMap's that were computed by multi-package inference for that imported package. We copy the information not just into Mapping, but also into UpstreamMapping. As more information is observed through a call to ObservePackage, it will be added to Mapping but not UpstreamMapping, then, on a call to Export, only the information present in Mapping but not UpstreamMapping is exported to ensure minimization of output.
type ExplainedBool ¶
type ExplainedBool interface { fmt.Stringer Val() bool Position() token.Position TriggerReprs() (producer fmt.Stringer, consumer fmt.Stringer) DeeperReason() ExplainedBool }
An ExplainedBool is a boolean value, wrapped by a "reason" that we came to the conclusion it should have that value. ExplainedBools are used as labels on annotation sites once their state (true for nilable, false for nonnil) is established, with the explanations serving primarily to generate error messages in the case that conflicting labels are required for a given site. The currently used explanations are: - <Val>BecauseShallowConstraint: Applied to site X when X was half of an assertion where the other half was fixed as a definite site of nil production or nonnil consumption - <Val>BecauseDeepConstraint: Applied to site X when X was half of an assertion where the other half was fixed, but through a deeper chain of assertions - <Val>BecauseAnnotation: Applied to site X when a syntactic annotation was discovered on X
type ExplainedFalse ¶
type ExplainedFalse struct{}
ExplainedFalse is a common embedding in all instances of ExplainedBool that wrap the value `false`
func (ExplainedFalse) Val ¶
func (ExplainedFalse) Val() bool
Val for an ExplainedFalse always returns `false` (this is the point of an ExplainedFalse)
type ExplainedTrue ¶
type ExplainedTrue struct{}
ExplainedTrue is a common embedding in all instances of ExplainedBool that wrap the value `true`
func (ExplainedTrue) Val ¶
func (ExplainedTrue) Val() bool
Val for an ExplainedTrue always returns `true` (this is the point of an ExplainedTrue)
type FalseBecauseAnnotation ¶
type FalseBecauseAnnotation struct { ExplainedFalse AnnotationPos token.Position }
FalseBecauseAnnotation is used as the label for a site X on which a literal annotation "//nonnil(x)" has been discovered - forcing that site to be nonnil.
func (FalseBecauseAnnotation) DeeperReason ¶
func (f FalseBecauseAnnotation) DeeperReason() ExplainedBool
DeeperReason returns another ExplainedBool that marks the deeper reason of this constraint. It is only nonnil for deep constraints.
func (FalseBecauseAnnotation) Position ¶
func (f FalseBecauseAnnotation) Position() token.Position
Position is the position of underlying site.
func (FalseBecauseAnnotation) String ¶
func (FalseBecauseAnnotation) String() string
func (FalseBecauseAnnotation) TriggerReprs ¶
func (FalseBecauseAnnotation) TriggerReprs() (fmt.Stringer, fmt.Stringer)
TriggerReprs simply returns nil, nil since this constraint is the result of an annotation.
type FalseBecauseDeepConstraint ¶
type FalseBecauseDeepConstraint struct { ExplainedFalse InternalAssertion primitiveFullTrigger DeeperExplanation ExplainedBool }
FalseBecauseDeepConstraint is used as the label for a site X when an assertion of the form `nilable X -> nilable Y` is discovered along with some reason for Y to be nonnil, besides it necessarily being so because it always fires. This reason could be any ExplainedFalse - such as `FalseBecauseAnnotation`, `FalseBecauseShallowConstraint`, or another `FalseBecauseDeepConstraint`.
func (FalseBecauseDeepConstraint) DeeperReason ¶
func (f FalseBecauseDeepConstraint) DeeperReason() ExplainedBool
DeeperReason returns another ExplainedBool that marks the deeper reason of this constraint. It is only nonnil for deep constraints.
func (FalseBecauseDeepConstraint) Position ¶
func (f FalseBecauseDeepConstraint) Position() token.Position
Position is the position of underlying site.
func (FalseBecauseDeepConstraint) String ¶
func (f FalseBecauseDeepConstraint) String() string
func (FalseBecauseDeepConstraint) TriggerReprs ¶
func (f FalseBecauseDeepConstraint) TriggerReprs() (fmt.Stringer, fmt.Stringer)
TriggerReprs returns the compact representation structs for the producer and consumer.
type FalseBecauseShallowConstraint ¶
type FalseBecauseShallowConstraint struct { ExplainedFalse ExternalAssertion primitiveFullTrigger }
FalseBecauseShallowConstraint is used as the label for site X when an assertion of the form `nilable X -> nilable Y` is discovered and the trigger for `nilable Y` always fires (i.e. yields nonnil) - for example because it is the dereferenced as a pointer or passed to a field access. In all cases, this constrains the site X to be nonnil, so we label X with `ExplainedFalse` as a `FalseBecauseShallowConstraint`, wrapped along with the assertion that we discovered to yield the falsehood.
func (FalseBecauseShallowConstraint) DeeperReason ¶
func (f FalseBecauseShallowConstraint) DeeperReason() ExplainedBool
DeeperReason returns another ExplainedBool that marks the deeper reason of this constraint. It is only nonnil for deep constraints.
func (FalseBecauseShallowConstraint) Position ¶
func (f FalseBecauseShallowConstraint) Position() token.Position
Position is the position of underlying site.
func (FalseBecauseShallowConstraint) String ¶
func (f FalseBecauseShallowConstraint) String() string
func (FalseBecauseShallowConstraint) TriggerReprs ¶
func (f FalseBecauseShallowConstraint) TriggerReprs() (fmt.Stringer, fmt.Stringer)
TriggerReprs returns the compact representation structs for the producer and consumer.
type InferredMap ¶
type InferredMap struct {
// contains filtered or unexported fields
}
An InferredMap is the state accumulated by multi-package inference. It's field `Mapping` maps a set of known annotation sites to InferredAnnotationVals - which can be either a fixed bool value along with explanation for why it was fixed - an DeterminedVal - or an UndeterminedVal indicating that site's place in the known implication graph between underconstrained sites. The set of sites mapped to UndeterminedBoolVals is guaranteed to be closed under following `Implicant`s and `Implicate`s pointers.
Additionally, a field upstreamMapping is stored indicating a stable copy of the information gleaned from upstream packages. Both mapping and upstreamMapping are initially populated with the same informations, but observation functions (observeSiteExplanation and observeImplication) add information only to Mapping. On export, iterations combined with calls to inferredValDiff on shared keys is used to ensure that only information present in `Mapping` but not `UpstreamMapping` is exported.
func (*InferredMap) AFact ¶
func (*InferredMap) AFact()
AFact allows InferredAnnotationMaps to be imported and exported via the Facts mechanism.
func (*InferredMap) CheckDeepTypeAnn ¶
func (i *InferredMap) CheckDeepTypeAnn(name *types.TypeName) (annotation.Val, bool)
CheckDeepTypeAnn checks this InferredMap for a concrete mapping of the type name key provideed
func (*InferredMap) CheckFieldAnn ¶
func (i *InferredMap) CheckFieldAnn(fld *types.Var) (annotation.Val, bool)
CheckFieldAnn checks this InferredMap for a concrete mapping of the field key provided
func (*InferredMap) CheckFuncCallSiteParamAnn ¶
func (i *InferredMap) CheckFuncCallSiteParamAnn(key *annotation.CallSiteParamAnnotationKey) (annotation.Val, bool)
CheckFuncCallSiteParamAnn checks this InferredMap for a concrete mapping of the call site param key provided.
func (*InferredMap) CheckFuncCallSiteRetAnn ¶
func (i *InferredMap) CheckFuncCallSiteRetAnn(key *annotation.CallSiteRetAnnotationKey) (annotation.Val, bool)
CheckFuncCallSiteRetAnn checks this InferredMap for a concrete mapping of the call site return key provided.
func (*InferredMap) CheckFuncParamAnn ¶
func (i *InferredMap) CheckFuncParamAnn(fdecl *types.Func, num int) (annotation.Val, bool)
CheckFuncParamAnn checks this InferredMap for a concrete mapping of the param key provided
func (*InferredMap) CheckFuncRecvAnn ¶
func (i *InferredMap) CheckFuncRecvAnn(fdecl *types.Func) (annotation.Val, bool)
CheckFuncRecvAnn checks this InferredMap for a concrete mapping of the receiver key provided
func (*InferredMap) CheckFuncRetAnn ¶
func (i *InferredMap) CheckFuncRetAnn(fdecl *types.Func, num int) (annotation.Val, bool)
CheckFuncRetAnn checks this InferredMap for a concrete mapping of the return key provided
func (*InferredMap) CheckGlobalVarAnn ¶
func (i *InferredMap) CheckGlobalVarAnn(v *types.Var) (annotation.Val, bool)
CheckGlobalVarAnn checks this InferredMap for a concrete mapping of the global variable key provided
func (*InferredMap) Export ¶
func (i *InferredMap) Export(pass *analysis.Pass)
Export only encodes new information not already present in the upstream maps, and it does not encode all (in the go sense; i.e. capitalized) annotation sites (See chooseSitesToExport). This ensures that only _incremental_ information is exported by this package and plays a _vital_ role in minimizing build output.
func (*InferredMap) GobDecode ¶
func (i *InferredMap) GobDecode(input []byte) error
GobDecode decodes the InferredMap from buffer.
func (*InferredMap) GobEncode ¶
func (i *InferredMap) GobEncode() (b []byte, err error)
GobEncode encodes the inferred map via gob encoding.
func (*InferredMap) Len ¶
func (i *InferredMap) Len() int
Len returns the number of annotation sites currently stored in the map.
func (*InferredMap) Load ¶
func (i *InferredMap) Load(site primitiveSite) (value InferredVal, ok bool)
Load returns the value stored in the map for an annotation site, or nil if no value is present. The ok result indicates whether value was found in the map.
func (*InferredMap) OrderedRange ¶
func (i *InferredMap) OrderedRange(f func(primitiveSite, InferredVal) bool)
OrderedRange calls f sequentially for each annotation site and inferred value present in the map in insertion order. If f returns false, range stops the iteration.
func (*InferredMap) StoreDetermined ¶
func (i *InferredMap) StoreDetermined(site primitiveSite, value ExplainedBool)
StoreDetermined sets the inferred value for an annotation site.
func (*InferredMap) StoreImplication ¶
func (i *InferredMap) StoreImplication(from primitiveSite, to primitiveSite, assertion primitiveFullTrigger)
StoreImplication stores an implication edge between the `from` and `to` annotation sites in the graph with the assertion for error reporting.
type InferredVal ¶
type InferredVal interface {
// contains filtered or unexported methods
}
An InferredVal is the information that we export about an annotation site after having witnessed an assertion about that site. If that assertion, and any other we've observed here and in upstream packages, tie the site to a necessary nilness or nonnilness, then an `DeterminedVal` will be used - which just wraps an `ExplainedBool` indicating the chain of implications FROM a definitely-produces-nil site TO this site forcing it to be nilable, or the chain of implications FROM this site TO a consumes-as-nonnil site forcing it to be nonnil. If we witness an assertion involving this annotation site, but it does not force the site to be nilable or nonnil, then an `UndeterminedVal` is used - which just annotates this site with a list of assertions from it to other sites (its implicates), and from other sites to it (its implicants).
In summary, InferredAnnotationVals are the values in the maps InferredMap that we export to indicate the state of multi-package inference between packages.
type ModeOfInference ¶
type ModeOfInference int
ModeOfInference is effectively an enum indicating the possible ways that we may conduct inference for NilAway
const ( // NoInfer implies that all annotations sites are determined by syntactic annotations if present // and default otherwise NoInfer ModeOfInference = iota // FullInfer implies that no annotation site will be fixed before a sequence of assertions demands // it - this is the fully sound and complete version of inference: implication graphs are shared // between packages FullInfer )
func DetermineMode ¶
func DetermineMode(pass *analysis.Pass) ModeOfInference
DetermineMode searches the files in this package for docstrings that indicate inference should be entirely suppressed (returns NoInfer). By default, if no such docstring is found, multi-package inference is used (returns FullInfer).
type TrueBecauseAnnotation ¶
type TrueBecauseAnnotation struct { ExplainedTrue AnnotationPos token.Position }
TrueBecauseAnnotation is used as the label for a site X on which a literal annotation "//nilable(x)" has been discovered - forcing that site to be nilable.
func (TrueBecauseAnnotation) DeeperReason ¶
func (TrueBecauseAnnotation) DeeperReason() ExplainedBool
DeeperReason returns another ExplainedBool that marks the deeper reason of this constraint. It is only nonnil for deep constraints.
func (TrueBecauseAnnotation) Position ¶
func (t TrueBecauseAnnotation) Position() token.Position
Position is the position of underlying site.
func (TrueBecauseAnnotation) String ¶
func (TrueBecauseAnnotation) String() string
func (TrueBecauseAnnotation) TriggerReprs ¶
func (TrueBecauseAnnotation) TriggerReprs() (fmt.Stringer, fmt.Stringer)
TriggerReprs simply returns nil, nil since this constraint is the result of an annotation.
type TrueBecauseDeepConstraint ¶
type TrueBecauseDeepConstraint struct { ExplainedTrue InternalAssertion primitiveFullTrigger DeeperExplanation ExplainedBool }
TrueBecauseDeepConstraint is used as the label for a site Y when an assertion of the form `nilable X -> nilable Y` is discovered along with some reason for X to be nilable, besides it necessarily being so because it always fires. This reason could be any ExplainedTrue - such as `TrueBecauseAnnotation`, `TrueBecauseShallowConstraint`, or another `TrueBecauseDeepConstraint`.
func (TrueBecauseDeepConstraint) DeeperReason ¶
func (t TrueBecauseDeepConstraint) DeeperReason() ExplainedBool
DeeperReason returns another ExplainedBool that marks the deeper reason of this constraint. It is only nonnil for deep constraints.
func (TrueBecauseDeepConstraint) Position ¶
func (t TrueBecauseDeepConstraint) Position() token.Position
Position is the position of underlying site.
func (TrueBecauseDeepConstraint) String ¶
func (t TrueBecauseDeepConstraint) String() string
func (TrueBecauseDeepConstraint) TriggerReprs ¶
func (t TrueBecauseDeepConstraint) TriggerReprs() (fmt.Stringer, fmt.Stringer)
TriggerReprs returns the compact representation structs for the producer and consumer.
type TrueBecauseShallowConstraint ¶
type TrueBecauseShallowConstraint struct { ExplainedTrue ExternalAssertion primitiveFullTrigger }
TrueBecauseShallowConstraint is used as the label for site Y when an assertion of the form `nilable X -> nilable Y` is discovered and the trigger for `nilable X` always fires (i.e. yields nilable) - for example because it is the literal nil or an unguarded map read. In all cases, this constrains the site Y to be nilable, so we label Y with `ExplainedTrue` as a `TrueBecauseShallowConstraint`, wrapped along with the assertion that we discovered to yield the truth.
func (TrueBecauseShallowConstraint) DeeperReason ¶
func (t TrueBecauseShallowConstraint) DeeperReason() ExplainedBool
DeeperReason returns another ExplainedBool that marks the deeper reason of this constraint. It is only nonnil for deep constraints.
func (TrueBecauseShallowConstraint) Position ¶
func (t TrueBecauseShallowConstraint) Position() token.Position
Position is the position of underlying site.
func (TrueBecauseShallowConstraint) String ¶
func (t TrueBecauseShallowConstraint) String() string
func (TrueBecauseShallowConstraint) TriggerReprs ¶
func (t TrueBecauseShallowConstraint) TriggerReprs() (fmt.Stringer, fmt.Stringer)
TriggerReprs returns the compact representation structs for the producer and consumer.
type UndeterminedVal ¶
type UndeterminedVal struct { // Implicants stores upstream constraints to this site. Implicants *orderedmap.OrderedMap[primitiveSite, primitiveFullTrigger] // Implicates stores downstream constraints from this site. Implicates *orderedmap.OrderedMap[primitiveSite, primitiveFullTrigger] }
An UndeterminedVal placed on annotation site X in an InferredMap indicates that we have witnessed at least one assertion about site X, but those assertions do not fix a nilability to the site. If X is the producer of the assertion, then the assertion (along with its consumer) will be added to the list `Implicates` of this UndeterminedVal, and if X is the consumer, then the assertion (along with its producer) will be added to the list `Implicants`.
As multi-package inference proceeds, these UndeterminedVal's serve to define the known implication graph between underconstrained annotation sites. That graph will continue to grow across packages until one of its nodes is forced to be nilable or nonnil due to a definite nil production or nonnil consumption, at which point a walk of the graph will be performed from that definite site to also fix (as ExplainedBoolVals) any other sites that become definite as a result. In this case of a definite nil production discovered, the graph will be walked "forwards" - i.e. using the "Implicates" pointers - assigning true (nilable) to every site discovered, and in the case of a definite nonnil consumption discovered, the graph will be walked "backwards" - i.e. using the "Implicants" pointers - assigning false (nonnil) to every site discovered.