Function backpropAcrossAssignment

assertion/function/assertiontree/backprop.go:277–410

backpropAcrossAssignment handles backpropagation for assignments, including special cases such as type switches and range statements. Moreover, it also handles special contracts such as map reads, channel reads, and type assertions by adding appropriate guards to them. Specifically, there are three

(rootNode *RootAssertionNode, lhs, rhs []ast.Expr)

// Phase 3. mark all LHS and RHS as computed.
// nonnil(lhs, rhs)
func backpropAcrossAssignment(rootNode *RootAssertionNode, lhs, rhs []ast.Expr) error {
	// For phase 1 and 2, we will first handle a few special assignments (with early return), then
	// if none of the special cases are hit, which means it is a normal assignment, we further
	// delegate the process to other functions depending on if it is many-to-one or one-to-one
	// assignment for better code clarity.
	// In all cases, we should do phase 3 before returning, so here we defer a function for phase 3.
	defer func() {
		// Phase 3
		// Now that we've back-propagated across the assignment itself, make sure we can compute
		// all of the lhs and rhs.
		for _, rhsVal := range rhs {
			rootNode.AddComputation(rhsVal)
		}
		for _, lhsVal := range lhs {
			rootNode.AddComputation(lhsVal)
		}
	}()

	// Phase 1 and 2
	// First handle a few special cases, e.g., type switches, type assertions, range statements,
	// and some cases for "ok" contracts, all of which will have a rhs with length 1.
	if len(rhs) == 1 {
		// Here we first strip the parentheses of the rhs to reveal the underlying nodes.
		rhsNode := ast.Unparen(rhs[0])

		// Type switch `x := y.(type)`, which needs special handling because TypesInfo.Defs
		// can't find an object for the lhs.
		// Note that the key distinction between a "type switch" and a "type assertion" in the
		// AST is whether the `Type` field of the AST node is nil.
		if r, ok := rhsNode.(*ast.TypeAssertExpr); ok && r.Type == nil {
			// lhs must have one element, which is *ast.Ident.
			if len(lhs) != 1 {
				return errors.New("lhs must have one element for type switches")
			}
			lhsIdent := lhs[0].(*ast.Ident)
			return backpropAcrossTypeSwitch(rootNode, lhsIdent, r.X)
		}

		if r, ok := rhsNode.(*ast.UnaryExpr); ok {
			switch r.Op {
			case token.RANGE:
				// Range statement of the form `for x := range y`, which is not overly complex to
				// handle but does involve distinct semantics.
				return backpropAcrossRange(rootNode, lhs, r.X)
			case token.AND:
				if !rootNode.functionContext.functionConfig.EnableStructInitCheck {
					// This is the case of creating a pointer and assigning it to a variable, e.g., `x := &y`,
					// where y is a non-pointer type (e.g., y := S{}).
					// Here, the pointer is always nonnil, so we can just add a ProduceTriggerNever.
					if rootNode.Pass().ExprBarsNilness(r.X) {
						if len(lhs) == 1 && !asthelper.IsEmptyExpr(lhs[0]) {
							rootNode.AddProduction(&annotation.ProduceTrigger{
								Annotation: &annotation.ProduceTriggerNever{},
								Expr:       lhs[0],
							})
						}
					}
				}