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

Support contracts across packages. #42

Conversation

zzqatuber
Copy link
Contributor

@zzqatuber zzqatuber commented Aug 18, 2023

Code changes of this PR includes the general changes that support cross-package for NilAway. However, that part is not migrated to GitHub yet so I can only rebase onto zzq/function-contracts/general-nonnil. Ideally we should have another PR for the general changes to support cross-package between and rebase this PR to the PR.

What was done:

  1. Pass around function contracts analyzed across packages.
  2. Stop modifying the full triggers passed into inference engine; instead of having a new type Implication (which is exportable as package facts) to carry information from a FullTrigger and then adapt the engine to digest this new type.
  3. Export and import contracts for full triggers of contracted functions across packages, in the form of implications.

Future work:
The current implementation does not work sometimes, because it creates a primitivizer in function analyzer but the position information this primitivizer obtains will be conflicting with those obtained from the primitivizer in accumulation analyzer.

Function analyzer cannot get the column number for every object from upstream, because unlike InferredMap exported in accumuulation analyzer, the Implication exported in function analyzer does not contain every exported object in upstream (We store only duplicable implications there)

Thus, a entirely new implementation is needed. We have to move all the logic of duplicating full triggers from function analyzer to accumalation analyzer (i.e., inference phase), so we maintain only one primitivizer and the position information (column number) of upstream objects can be obtained from upstream packages correctly.

PS:
Did not find integration tests here so I did not migrate integration cross-packge tests but they can be found in the internal version of this pull request.

@zzqatuber zzqatuber marked this pull request as draft August 18, 2023 22:57
@zzqatuber zzqatuber changed the title experimental support for cross-package contracts. Support contracts across packages. Aug 18, 2023
@codecov
Copy link

codecov bot commented Aug 18, 2023

Codecov Report

Attention: Patch coverage is 65.71936% with 193 lines in your changes missing coverage. Please review.

Project coverage is 86.00%. Comparing base (881b950) to head (4dd4a18).

Files Patch % Lines
assertion/function/analyzer.go 52.77% 127 Missing and 9 partials ⚠️
inference/inferred_value.go 2.94% 33 Missing ⚠️
inference/primitive.go 82.14% 14 Missing and 6 partials ⚠️
inference/engine.go 96.87% 1 Missing and 1 partial ⚠️
assertion/function/functioncontracts/analyzer.go 96.87% 1 Missing ⚠️
inference/inferred_map.go 95.45% 1 Missing ⚠️
Additional details and impacted files
@@                            Coverage Diff                            @@
##           zzq/function-contracts/general-nonnil      #42      +/-   ##
=========================================================================
- Coverage                                  87.55%   86.00%   -1.55%     
=========================================================================
  Files                                         54       54              
  Lines                                       8547     8994     +447     
=========================================================================
+ Hits                                        7483     7735     +252     
- Misses                                       906     1084     +178     
- Partials                                     158      175      +17     

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

yuxincs added a commit that referenced this pull request Nov 29, 2023
@zzqatuber has implemented contract support in NilAway and has merged
the manual contract support (i.e., via manual annotations such as
`//contract(nonnil->nonnil)`) in main NilAway but hidden under a flag.

After internal performance validations there are no major
performance/functionality degradations of simply enabling this feature,
therefore this PR removes the hidden flag and make it available in
NilAway.

After this PR, we will prioritize merging the automatic inference of the
function contracts (i.e., PR #40 , PR #41 , and PR #42 ).
@yuxincs
Copy link
Contributor

yuxincs commented Aug 21, 2024

The functionality of this PR should (at least partially) be implemented in PR #240, so I'm closing this.

If we need to further enhance cross-package support for contract, we'll use this PR as reference and properly attribute the contributions :)

@yuxincs yuxincs closed this Aug 21, 2024
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