Method buildFromSingleFullTrigger

inference/engine.go:338–384

(trigger annotation.FullTrigger)

}

func (e *Engine) buildFromSingleFullTrigger(trigger annotation.FullTrigger) {
	pKind, cKind := trigger.Producer.Annotation.Kind(), trigger.Consumer.Annotation.Kind()
	pSite, cSite := trigger.Producer.Annotation.UnderlyingSite(), trigger.Consumer.Annotation.UnderlyingSite()
	// NilAway does not know that (kind == Conditional || DeepConditional) => (site != nil),
	// so we have to add some redundant checks in the corresponding cases to give some hints.
	// TODO: remove those redundant nilness checks for sites.
	switch {
	case pKind == annotation.Always && cKind == annotation.Always:
		// Producer always produces nilable value -> consumer always consumes nonnil value.
		// We simply generate a failure for this case.
		e.diagnosticEngine.AddSingleAssertionConflict(trigger)

	case pKind == annotation.Always && (cKind == annotation.Conditional || cKind == annotation.DeepConditional):
		// Producer always produces nilable value -> consumer unknown.
		// We propagate nilable to this consumer site.
		if cSite == nil {
			panic("trigger is conditional but the underlying site is nil")
		}
		site := e.primitive.site(cSite, cKind == annotation.DeepConditional)
		e.observeSiteExplanation(site, TrueBecauseShallowConstraint{
			ExternalAssertion: e.primitive.fullTrigger(trigger),
		})

	case (pKind == annotation.Conditional || pKind == annotation.DeepConditional) && (cKind == annotation.Always):
		// Producer unknown -> consumer always consumes nonnil value.
		// We propagate nonnil to the producer site.
		if pSite == nil {
			panic("trigger is conditional but the underlying site is nil")
		}
		site := e.primitive.site(pSite, pKind == annotation.DeepConditional)
		e.observeSiteExplanation(site, FalseBecauseShallowConstraint{
			ExternalAssertion: e.primitive.fullTrigger(trigger),
		})

	case (pKind == annotation.Conditional || pKind == annotation.DeepConditional) &&
		(cKind == annotation.Conditional || cKind == annotation.DeepConditional):
		// Producer unknown -> consumer unknown.
		// We store this implication in our map as UndeterminedBool.
		if pSite == nil || cSite == nil {
			panic("trigger is conditional but the underlying site is nil")
		}
		producer := e.primitive.site(pSite, pKind == annotation.DeepConditional)
		consumer := e.primitive.site(cSite, cKind == annotation.DeepConditional)

		e.observeImplication(producer, consumer, e.primitive.fullTrigger(trigger))
	}
}

// observeSiteExplanation augments inferred map with a definite value for the passed
// site `site` - the definite value being given as the ExplainedBool `siteExplained`. Any conflicts