Zzq/function contracts/cross package #2
Conversation
There was a problem hiding this comment.
PR Summary
This PR refines the function contracts analysis by propagating cross‑package implications, updating result types, and adjusting trigger duplication and contract checking across modules.
• In assertion/analyzer.go, a new Implications field is added to Result and populated from the function analyzer.
• In accumulation/analyzer.go, ObservePackage now accepts both full triggers and implications.
• In assertion/function/assertiontree/parse_expr_producer.go, per‐return contract checks (RetHasContract) replace the previous HasContract.
• The function analyzer now duplicates triggers for contracted functions with new caching logic; note potential index bounds and strict type assertions.
• In functioncontracts/analyzer.go, upstream contracts are merged with local inference; consider using logger.error for panic recovery.
17 file(s) reviewed, 5 comment(s)
Edit PR Review Bot Settings | Greptile
| func (r *RootAssertionNode) ParamHasContract(funcObj *types.Func, i int) bool { | ||
| ctrt := r.getSingleNonnilToNonnilContract(funcObj) | ||
| return ctrt != nil && ctrt.Ins[i] == functioncontracts.NonNil |
There was a problem hiding this comment.
logic: Ensure length of ctrt.Ins > i to avoid index out-of-range in ParamHasContract.
| func (r *RootAssertionNode) ParamHasContract(funcObj *types.Func, i int) bool { | |
| ctrt := r.getSingleNonnilToNonnilContract(funcObj) | |
| return ctrt != nil && ctrt.Ins[i] == functioncontracts.NonNil | |
| func (r *RootAssertionNode) ParamHasContract(funcObj *types.Func, i int) bool { | |
| ctrt := r.getSingleNonnilToNonnilContract(funcObj) | |
| return ctrt != nil && i < len(ctrt.Ins) && ctrt.Ins[i] == functioncontracts.NonNil |
| // value. | ||
| func (r *RootAssertionNode) RetHasContract(funcObj *types.Func, i int) bool { | ||
| ctrt := r.getSingleNonnilToNonnilContract(funcObj) | ||
| return ctrt != nil && ctrt.Outs[i] == functioncontracts.NonNil |
There was a problem hiding this comment.
logic: Add bounds check on ctrt.Outs in RetHasContract to prevent potential panic.
| // value. | |
| func (r *RootAssertionNode) RetHasContract(funcObj *types.Func, i int) bool { | |
| ctrt := r.getSingleNonnilToNonnilContract(funcObj) | |
| return ctrt != nil && ctrt.Outs[i] == functioncontracts.NonNil | |
| // value. | |
| func (r *RootAssertionNode) RetHasContract(funcObj *types.Func, i int) bool { | |
| ctrt := r.getSingleNonnilToNonnilContract(funcObj) | |
| return ctrt != nil && i < len(ctrt.Outs) && ctrt.Outs[i] == functioncontracts.NonNil |
| getFuncID(pass, "learnUnderlyingFromOuterMakeInterface"): { | ||
| &FunctionContract{Ins: []ContractVal{NonNil}, Outs: []ContractVal{NonNil}}, | ||
| }, | ||
| getFuncID(pass, "ExportedFromInfer"): { | ||
| &FunctionContract{Ins: []ContractVal{NonNil}, Outs: []ContractVal{NonNil}}, | ||
| }, | ||
| getFuncID(pass, "twoCondsMerge"): { |
There was a problem hiding this comment.
logic: Duplicate key 'ExportedFromInfer' in expected map; previous entry will be overwritten. Merge into one entry.
| getFuncID(pass, "learnUnderlyingFromOuterMakeInterface"): { | |
| &FunctionContract{Ins: []ContractVal{NonNil}, Outs: []ContractVal{NonNil}}, | |
| }, | |
| getFuncID(pass, "ExportedFromInfer"): { | |
| &FunctionContract{Ins: []ContractVal{NonNil}, Outs: []ContractVal{NonNil}}, | |
| }, | |
| getFuncID(pass, "twoCondsMerge"): { | |
| ```suggestion getFuncID(pass, "learnUnderlyingFromOuterMakeInterface"): { | |
| &FunctionContract{Ins: []ContractVal{NonNil}, Outs: []ContractVal{NonNil}}, | |
| }, | |
| getFuncID(pass, "twoCondsMerge"): { |
| func (e *Engine) activateControlledImplications(site PrimitiveSite, siteExplained ExplainedBool) { | ||
| if controlledImpl, ok := e.controlledImplicationsBySite[site]; ok && siteExplained.Val() { | ||
| for impl := range controlledImpl { | ||
| e.processSingleExtraImplication(&impl) | ||
| } | ||
| } | ||
| } |
There was a problem hiding this comment.
logic: Logic issue: In activateControlledImplications, the loop 'for impl := range controlledImpl' takes '&impl'. As the loop variable is reused, this will pass the address of the same variable in all iterations. Consider copying the value into a fresh variable before taking its address.
| func (e *Engine) activateControlledImplications(site PrimitiveSite, siteExplained ExplainedBool) { | |
| if controlledImpl, ok := e.controlledImplicationsBySite[site]; ok && siteExplained.Val() { | |
| for impl := range controlledImpl { | |
| e.processSingleExtraImplication(&impl) | |
| } | |
| } | |
| } | |
| func (e *Engine) activateControlledImplications(site PrimitiveSite, siteExplained ExplainedBool) { | |
| if controlledImpl, ok := e.controlledImplicationsBySite[site]; ok && siteExplained.Val() { | |
| for impl := range controlledImpl { | |
| implCopy := impl // Create a new variable for each iteration | |
| e.processSingleExtraImplication(&implCopy) | |
| } | |
| } | |
| } |
| // fullTrigger returns the primitive version of the full trigger. | ||
| func (p *Primitivizer) fullTrigger(trigger annotation.FullTrigger) PrimitiveFullTrigger { | ||
| // Expr is always nonnil, but our struct init analysis is capped at depth 1 so NilAway does not | ||
| // know this fact. Here, we explicitly guard against such cases to provide a hint. | ||
| if trigger.Consumer.Expr == nil { | ||
| panic(fmt.Sprintf("consume trigger %v has a nil Expr", trigger.Consumer)) | ||
| } |
There was a problem hiding this comment.
logic: Missing assignment to the Pos field in fullTrigger. Previously, it was set to trigger.Consumer.Expr.Pos() and later used for matching. Consider adding ‘Pos: trigger.Consumer.Expr.Pos(),’ in the returned struct literal.
No description provided.