Method observeImplication

inference/engine.go:500–549

observeImplication augments the inferred map with a new implication discovered as the result of an assertion. In particular, we note that all assertions discovered as FullTriggers by the assertions or affiliations analyzer are of the form `nilable X -> nilable Y`, so this method just takes the `prod

(
	producerSite,
	consumerSite primitiveSite,
	assertion primitiveFullTrigger,
)

//   - If both sites are undetermined (i.e. both are under-constrained nodes in the implication graph)
//     then we simply ensure that this assertion is present as en edge between them.
func (e *Engine) observeImplication(
	producerSite,
	consumerSite primitiveSite,
	assertion primitiveFullTrigger,
) {
	// When we observe an implication between the producer site (PS) and consumer site (CS), we
	// check their existing values in the inferred map (denoted as P and C) and behave accordingly:
	// * If either P or C is determined, the other site will be determined. Note that we do not
	//   need to continue processing after either case since we are handling the same implication
	//   (i.e., no need to handle P => C and then C => P again). This also ensures that we do not
	//   report duplicate errors when P and C are both determined and have conflicting nilabilities.
	//   Specifically:
	//     * P is nilable => C must be nilable
	//     * P is nonnil => this implication does not yield more information which can be safely discarded
	//     * C is nilable => this implication does not yield more information which can be safely discarded
	//     * C is nonnil => P must be nonnil
	//
	// * If _both_ P and C are "undetermined or does not exist", we should create an implication
	//    edge between PS and CS.

	// Nilable (true) producer => Nilable (true) consumer. We do not care about "ok" here since
	// the "ok" in the type assertion below implies this "ok == true".
	producer, _ := e.inferredMap.Load(producerSite)
	if v, ok := producer.(*DeterminedVal); ok {
		if v.Bool.Val() {
			e.observeSiteExplanation(consumerSite, TrueBecauseDeepConstraint{
				InternalAssertion: assertion,
				DeeperExplanation: v.Bool,
			})
		}
		return
	}

	// Nonnil (false) consumer => Nonnil (false) producer. We do not care about "ok" here since
	// the "ok" in the type assertion below implies this "ok == true".
	consumer, _ := e.inferredMap.Load(consumerSite)
	if v, ok := consumer.(*DeterminedVal); ok {
		if !v.Bool.Val() {
			e.observeSiteExplanation(producerSite, FalseBecauseDeepConstraint{
				InternalAssertion: assertion,
				DeeperExplanation: v.Bool,
			})
		}
		return
	}

	// If we reach here, it means that the existing values for the producer and consumer are
	// undetermined (or non-existent), so we can simply add an implication edge in the graph.
	e.inferredMap.StoreImplication(producerSite, consumerSite, assertion)
}

// 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