Function learnNilness

assertion/function/functioncontracts/infer.go:160–200

learnNilness learns nilness for the block succ, extended from one nilnessTable table of its predecessor pred. The function creates a new nilnessTable that stores **only newly learned** nilness for succ block and a bool flag that indicates whether a conflict is seen when going to succ block from pred

(succ *ssa.BasicBlock, pred *ssa.BasicBlock, table nilnessTable)

// not learn nilness for al kinds of conditions. For now we support only what is supported in
// the function branch.
func learnNilness(succ *ssa.BasicBlock, pred *ssa.BasicBlock, table nilnessTable) (nilnessTable, bool) {
	lTable := nilnessTable{} // learned nilnessTable
	eqSucc, neSucc, binOp := branch(pred)
	// TODO: for now we learn nilness from only these two condition: ? == ? and ? != ?
	if binOp == nil || eqSucc == nil || neSucc == nil {
		// TODO: only binOp == nil is sufficient, but nilaway would not be happy with it.
		return lTable, true
	}
	// TODO: each successor should learn a different nilness in terms of the variable
	//  involved in the condition.
	xnil := table.nilnessOf(binOp.X)
	ynil := table.nilnessOf(binOp.Y)

	// Both operands are known of nilness.
	// Determine whether the branch is reachable.
	if xnil != unknown && ynil != unknown {
		if (xnil == ynil && succ == eqSucc) || (xnil != ynil && succ == neSucc) {
			return lTable, true
		}
		// conflict
		return lTable, false
	}

	// Only one operand is known of nilness.
	if ynil == unknown {
		// learn the nilness of Y
		if succ == eqSucc {
			lTable.expandNilness(binOp.Y, xnil)
		} else {
			lTable.expandNilness(binOp.Y, xnil.negate())
		}
	} else {
		// learn the nilness of X
		if succ == eqSucc {
			lTable.expandNilness(binOp.X, ynil)
		} else {
			lTable.expandNilness(binOp.X, ynil.negate())
		}
	}
	return lTable, true
}

// deriveContracts checks nilness of parameter and return values at every exit block to infer
// contracts.