Function BackpropAcrossFunc

assertion/function/assertiontree/backprop.go:901–1082

BackpropAcrossFunc is the main driver of the backpropagation, it takes a function declaration with accompanying CFG, and back-propagates a tree of assertions across it to generate, at entry to the function, the set of assertions that must hold to avoid possible nil flow errors.

(
	ctx context.Context,
	pass *analysishelper.EnhancedPass,
	decl *ast.FuncDecl,
	functionContext FunctionContext,
	graph *cfg.CFG,
)

// with accompanying CFG, and back-propagates a tree of assertions across it to generate, at entry
// to the function, the set of assertions that must hold to avoid possible nil flow errors.
func BackpropAcrossFunc(
	ctx context.Context,
	pass *analysishelper.EnhancedPass,
	decl *ast.FuncDecl,
	functionContext FunctionContext,
	graph *cfg.CFG,
) ([]annotation.FullTrigger, int, int, error) {
	// We transform the CFG to have it reflect the implicit control flow that happens
	// inside short-circuiting boolean expressions.
	preprocessor := preprocess.New(pass)
	graph = preprocessor.CFG(graph, functionContext.funcDecl)

	// Generate rick check effects.
	richCheckBlocks, exprNonceMap := genInitialRichCheckEffects(graph, functionContext)
	richCheckBlocks = propagateRichChecks(graph, richCheckBlocks)
	blocks, preprocessing := blocksAndPreprocessingFromCFG(pass, graph, richCheckBlocks)

	// The assertion nodes for each block and an array of bools to indicate whether each block is
	// updated in this round or not.
	// DANGER: anytime a pointer is copied from currAssertions to nextAssertions, it MUST be
	// treated as immutable - if any modification (e.g. merging or backprop) is going to occur you
	// must perform a deep copy with CopyNode
	updatedLastRound, updatedThisRound := make([]bool, len(blocks)), make([]bool, len(blocks))
	currAssertions, nextAssertions := make([]*RootAssertionNode, len(blocks)), make([]*RootAssertionNode, len(blocks))

	// The assertion nodes for the entry block, we will use it as an indication for stabilization.
	// We consider the backpropagation stable if # of stable rounds > # of live blocks + tolerance.
	var currRootAssertionNode, nextRootAssertionNode *RootAssertionNode
	roundCount, stableRoundCount := 0, 0
	postOrder := computePostOrder(blocks)

	// Initialize the process by creating the assertion nodes for the return block.
	retBlock := len(blocks) - 1
	currAssertions[retBlock] = newRootAssertionNode(exprNonceMap, functionContext)
	updatedLastRound[retBlock] = true

	for slices.Contains(updatedLastRound, true) {
		roundCount++

		select {
		case <-ctx.Done():
			return nil, roundCount, stableRoundCount, fmt.Errorf("backprop early stop due to context: %w", ctx.Err())
		default:
		}

		for _, i := range postOrder {
			block := blocks[i]

			// There is no need to process non-live blocks; their assertions will simply be nil.
			if !block.Live {
				continue
			}

			if len(block.Succs) > 2 {
				return nil, roundCount, stableRoundCount, errors.New("assumptions about CFG shape violated - a block has >2 successors")
			}

			// No need to re-process the assertion node for the current block if it does not have