inference

package
v0.0.0-...-ba14292 Latest Latest
Warning

This package is not in the latest version of its module.

Go to latest
Published: Oct 10, 2024 License: Apache-2.0 Imports: 19 Imported by: 2

Documentation

Overview

Package inference implements the inference algorithm in NilAway to automatically infer the nilability of the annotation sites.

Index

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 NewEngine

func NewEngine(pass *analysis.Pass, diagnosticEngine conflictHandler) *Engine

NewEngine constructs an inference engine that is ready to run inference.

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

Position is the position of underlying site.

func (FalseBecauseDeepConstraint) 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

DeeperReason returns another ExplainedBool that marks the deeper reason of this constraint. It is only nonnil for deep constraints.

func (FalseBecauseShallowConstraint) Position

Position is the position of underlying site.

func (FalseBecauseShallowConstraint) String

func (FalseBecauseShallowConstraint) TriggerReprs

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

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

DeeperReason returns another ExplainedBool that marks the deeper reason of this constraint. It is only nonnil for deep constraints.

func (TrueBecauseShallowConstraint) Position

Position is the position of underlying site.

func (TrueBecauseShallowConstraint) String

func (TrueBecauseShallowConstraint) TriggerReprs

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.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL