Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement fact export for manually-written and inferred function contracts #240

Merged
merged 6 commits into from
Jul 19, 2024

Conversation

yuxincs
Copy link
Contributor

@yuxincs yuxincs commented May 4, 2024

This PR implements the fact export for manually-written and inferred function contracts. Specifically it enhances the functioncontracts sub-analyzer, which imports contracts from upstream packages, parses/infers the contracts for the local package, combine the contract map and return it. It now also exports the contracts for the exported functions in the local package to be consumed by its downstream packages.

Tests are also added to ensure the fact export and import logic works.

Copy link

codecov bot commented May 4, 2024

Codecov Report

Attention: Patch coverage is 60.00000% with 8 lines in your changes missing coverage. Please review.

Project coverage is 87.51%. Comparing base (613d002) to head (44553ec).

Files Patch % Lines
assertion/function/functioncontracts/analyzer.go 61.11% 4 Missing and 3 partials ⚠️
assertion/function/analyzer.go 50.00% 1 Missing ⚠️
Additional details and impacted files
@@            Coverage Diff             @@
##             main     #240      +/-   ##
==========================================
- Coverage   87.55%   87.51%   -0.04%     
==========================================
  Files          63       63              
  Lines        7825     7842      +17     
==========================================
+ Hits         6851     6863      +12     
- Misses        796      799       +3     
- Partials      178      180       +2     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

Copy link

github-actions bot commented May 4, 2024

Golden Test

Warning

❌ NilAway errors reported on stdlib are different 📉.

3297 errors on base branch (main, 613d002)
3283 errors on test branch (6121fdf)

Diffs
+ /opt/hostedtoolcache/go/1.22.5/x64/src/math/big/int.go:190:21: Potential nil panic detected. Observed nil flow from source to dereference point: 
+ 	- elliptic/p256_test.go:70:29: result 0 of `SetString()` lacking guarding; passed as arg `x1` to `ScalarMult()` via the assignment(s):
+ 		- `new(...).SetString(...)` to `x` at elliptic/p256_test.go:64:3
+ 	- elliptic/params.go:287:27: passed as parameter `Bx` to `CurveParams.ScalarMult()` (implementing `Curve.ScalarMult()`)
+ 	- elliptic/params.go:302:33: function parameter `Bx` passed as arg `x1` to `addJacobian()`
+ 	- elliptic/params.go:147:25: function parameter `x1` passed as arg `x` to `Mul()`
+ 	- big/int.go:190:21: function parameter `x` accessed field `abs`
+ /opt/hostedtoolcache/go/1.22.5/x64/src/math/big/int.go:190:21: Potential nil panic detected. Observed nil flow from source to dereference point: 
+ 	- elliptic/p256_test.go:70:32: result 0 of `SetString()` lacking guarding; passed as arg `y1` to `ScalarMult()` via the assignment(s):
+ 		- `new(...).SetString(...)` to `y` at elliptic/p256_test.go:65:3
+ 	- elliptic/params.go:287:27: passed as parameter `By` to `CurveParams.ScalarMult()` (implementing `Curve.ScalarMult()`)
+ 	- elliptic/params.go:302:37: function parameter `By` passed as arg `y1` to `addJacobian()`
+ 	- elliptic/params.go:160:25: function parameter `y1` passed as arg `x` to `Mul()`
+ 	- big/int.go:190:21: function parameter `x` accessed field `abs`
- /opt/hostedtoolcache/go/1.22.5/x64/src/bytes/example_test.go:130:2: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- bytes/bytes.go:1344:10: literal `nil` returned from `Clone()` in position 0
- 	- bytes/example_test.go:130:2: result 0 of `Clone()` sliced into via the assignment(s):
- 		- `bytes.Clone(b)` to `clone` at bytes/example_test.go:128:2
- /opt/hostedtoolcache/go/1.22.5/x64/src/crypto/ecdsa/ecdsa.go:396:5: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- bytes/bytes.go:1344:10: literal `nil` returned from `Clone()` in position 0
- 	- ecdsa/ecdsa.go:396:5: result 0 of `Clone()` sliced into via the assignment(s):
- 		- `bytes.Clone(...)` to `hash` at ecdsa/ecdsa.go:394:4
- 
- (Same nil source could also cause potential nil panic(s) at 2 other place(s): "ecdsa/ecdsa.go:398:6", and "ecdsa/ecdsa.go:398:17".)
- /opt/hostedtoolcache/go/1.22.5/x64/src/crypto/internal/bigmod/nat.go:194:30: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- bytes/bytes.go:1344:10: literal `nil` returned from `Clone()` in position 0
- 	- ecdsa/ecdsa.go:403:34: result 0 of `Clone()` passed as arg `b` to `SetOverflowingBytes()` via the assignment(s):
- 		- `bytes.Clone(...)` to `hash` at ecdsa/ecdsa.go:394:4
- 	- bigmod/nat.go:170:23: function parameter `b` passed as arg `b` to `setBytes()`
- 	- bigmod/nat.go:194:30: function parameter `b` sliced into
- /opt/hostedtoolcache/go/1.22.5/x64/src/crypto/md5/md5.go:128:7: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- bytes/bytes.go:1344:10: literal `nil` returned from `Clone()` in position 0
- 	- encodemeta/encode.go:86:15: result 0 of `Clone()` assigned into field `encoded`
- 	- encodemeta/encode.go:104:24: field `encoded` passed as arg `p` to `Write()`
- 	- md5/md5.go:111:18: passed as parameter `p` to `digest.Write()` (implementing `Writer.Write()`)
- 	- md5/md5.go:128:7: function parameter `p` sliced into
- /opt/hostedtoolcache/go/1.22.5/x64/src/crypto/sha256/sha256.go:190:7: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- bytes/bytes.go:1344:10: literal `nil` returned from `Clone()` in position 0
- 	- fuzz/mem.go:106:9: result 0 of `Clone()` returned from `valueCopy()` in position 0
- 	- fuzz/worker.go:1068:21: result 0 of `valueCopy()` passed as arg `data` to `Sum256()` via the assignment(s):
- 		- `mem.valueCopy()` to `entryOut.Data` at fuzz/worker.go:1046:4
- 	- sha256/sha256.go:259:10: function parameter `data` passed as arg `p` to `Write()`
- 	- sha256/sha256.go:190:7: function parameter `p` sliced into
- /opt/hostedtoolcache/go/1.22.5/x64/src/crypto/sha256/sha256.go:190:7: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- bytes/bytes.go:1344:10: literal `nil` returned from `Clone()` in position 0
- 	- fuzz/mem.go:106:9: result 0 of `Clone()` returned from `valueCopy()` in position 0
- 	- fuzz/worker.go:812:27: result 0 of `valueCopy()` passed as arg `data` to `Sum256()` via the assignment(s):
- 		- `<-ws.memMu` to `mem` at fuzz/worker.go:806:2
- 	- sha256/sha256.go:259:10: function parameter `data` passed as arg `p` to `Write()`
- 	- sha256/sha256.go:190:7: function parameter `p` sliced into
- /opt/hostedtoolcache/go/1.22.5/x64/src/crypto/sha256/sha256.go:190:7: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- bytes/bytes.go:1344:10: literal `nil

 ...(truncated)...

x.go:380:54: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- bytes/bytes.go:1344:10: literal `nil` returned from `Clone()` in position 0
- 	- os/example_test.go:386:36: result 0 of `Clone()` passed as arg `data` to `WriteFile()` via the assignment(s):
- 		- `bytes.Clone(...)` to `config` at os/example_test.go:376:2
- 	- os/file.go:819:19: function parameter `data` passed as arg `b` to `Write()`
- 	- os/file.go:189:18: function parameter `b` passed as arg `b` to `write()`
- 	- os/file_posix.go:46:23: function parameter `b` passed as arg `p` to `Write()`
- 	- poll/fd_unix.go:380:54: function parameter `p` sliced into
- /opt/hostedtoolcache/go/1.22.5/x64/src/math/big/int.go:99:11: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- elliptic/elliptic_test.go:240:9: result 1 of `GenerateKey()` lacking guarding; passed as arg `x` to `Neg()` via the assignment(s):
- 		- `GenerateKey(...)` to `x` at elliptic/elliptic_test.go:236:5
- 	- big/int.go:136:8: function parameter `x` passed as arg `x` to `Set()` at big/int.go:136:8
- 	- big/int.go:99:11: function parameter `x` at big/int.go:136:8 accessed field `neg`
- /opt/hostedtoolcache/go/1.22.5/x64/src/math/big/int.go:99:11: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- elliptic/elliptic_test.go:242:9: result 2 of `GenerateKey()` lacking guarding; passed as arg `x` to `Neg()` via the assignment(s):
- 		- `GenerateKey(...)` to `y` at elliptic/elliptic_test.go:236:8
- 	- big/int.go:136:8: function parameter `x` passed as arg `x` to `Set()` at big/int.go:136:8
- 	- big/int.go:99:11: function parameter `x` at big/int.go:136:8 accessed field `neg`
- /opt/hostedtoolcache/go/1.22.5/x64/src/math/big/int.go:99:11: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- elliptic/p256_test.go:70:29: result 0 of `SetString()` lacking guarding; passed as arg `x1` to `ScalarMult()` via the assignment(s):
- 		- `new(...).SetString(...)` to `x` at elliptic/p256_test.go:64:3
- 	- elliptic/params.go:287:27: passed as parameter `Bx` to `CurveParams.ScalarMult()` (implementing `Curve.ScalarMult()`)
- 	- elliptic/params.go:302:33: function parameter `Bx` passed as arg `x1` to `addJacobian()`
- 	- elliptic/params.go:136:10: function parameter `x1` passed as arg `x` to `Set()`
- 	- big/int.go:99:11: function parameter `x` accessed field `neg`
- /opt/hostedtoolcache/go/1.22.5/x64/src/math/big/int.go:99:11: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- elliptic/p256_test.go:70:32: result 0 of `SetString()` lacking guarding; passed as arg `y1` to `ScalarMult()` via the assignment(s):
- 		- `new(...).SetString(...)` to `y` at elliptic/p256_test.go:65:3
- 	- elliptic/params.go:287:27: passed as parameter `By` to `CurveParams.ScalarMult()` (implementing `Curve.ScalarMult()`)
- 	- elliptic/params.go:302:37: function parameter `By` passed as arg `y1` to `addJacobian()`
- 	- elliptic/params.go:137:10: function parameter `y1` passed as arg `x` to `Set()`
- 	- big/int.go:99:11: function parameter `x` accessed field `neg`
- /opt/hostedtoolcache/go/1.22.5/x64/src/math/big/nat.go:1342:24: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- cryptobyte/asn1.go:330:16: unassigned variable `bytes` passed as arg `buf` to `SetBytes()`
- 	- big/int.go:515:25: function parameter `buf` passed as arg `buf` to `setBytes()`
- 	- big/nat.go:1342:24: function parameter `buf` sliced into
- /opt/hostedtoolcache/go/1.22.5/x64/src/math/big/nat.go:1342:24: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- nistec/p256_ordinv.go:101:9: unassigned variable `xOut` returned from `P256OrdInverse()` in position 0
- 	- elliptic/nistec_p256.go:28:31: result 0 of `P256OrdInverse()` passed as arg `buf` to `SetBytes()` via the assignment(s):
- 		- `nistec.P256OrdInverse(...)` to `inverse` at elliptic/nistec_p256.go:24:2
- 	- big/int.go:515:25: function parameter `buf` passed as arg `buf` to `setBytes()`
- 	- big/nat.go:1342:24: function parameter `buf` sliced into
- /opt/hostedtoolcache/go/1.22.5/x64/src/math/big/nat.go:1342:24: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- x509/name_constraints_test.go:1609:39: unassigned variable `serialBytes` passed as arg `buf` to `SetBytes()`
- 	- big/int.go:515:25: function parameter `buf` passed as arg `buf` to `setBytes()`
- 	- big/nat.go:1342:24: function parameter `buf` sliced into
- /opt/hostedtoolcache/go/1.22.5/x64/src/math/big/nat.go:1342:24: Potential nil panic detected. Observed nil flow from source to dereference point: 
- 	- x509/name_constraints_test.go:1645:39: unassigned variable `serialBytes` passed as arg `buf` to `SetBytes()`
- 	- big/int.go:515:25: function parameter `buf` passed as arg `buf` to `setBytes()`
- 	- big/nat.go:1342:24: function parameter `buf` sliced into

@yuxincs yuxincs force-pushed the yuxincs/refactor-function-contract-analyzer branch from ebec5a0 to 045d6f0 Compare May 13, 2024 23:46
@yuxincs yuxincs force-pushed the yuxincs/store-manual-and-inferred-contracts branch from cbfaa2a to a78d795 Compare May 13, 2024 23:46
@yuxincs yuxincs force-pushed the yuxincs/refactor-function-contract-analyzer branch from 045d6f0 to 4c694b0 Compare May 14, 2024 19:15
@yuxincs yuxincs force-pushed the yuxincs/store-manual-and-inferred-contracts branch from 7f66eec to 5222335 Compare May 14, 2024 19:15
Copy link
Contributor

@sonalmahajan15 sonalmahajan15 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great job supporting cross-package contracts!

if !ok || ctrts == nil {
continue
}
// The existing contracts are imported from upstream packages about upstream functions,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// The existing contracts are imported from upstream packages about upstream functions,
// The existing contracts imported from upstream packages are about upstream functions,

print(*r) // Safe due to the contract!
}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice!

Base automatically changed from yuxincs/refactor-function-contract-analyzer to main July 19, 2024 15:13
@yuxincs yuxincs force-pushed the yuxincs/store-manual-and-inferred-contracts branch from 5222335 to 44553ec Compare July 19, 2024 15:17
@yuxincs yuxincs merged commit 28b542b into main Jul 19, 2024
8 checks passed
@yuxincs yuxincs deleted the yuxincs/store-manual-and-inferred-contracts branch July 19, 2024 15:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants