CHC: A number of fixes for command line arguments handling #192
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
We already had some logic to deal with this but not for all pointer cases. I copy/pasted that logic over to the cases where the current version of CHC complains for a simple hello world program that passes argv[0] to printf. There's still an open issue where there's a precondition for 'initialized(*argv)' that I have not addressed
…world program I couldn't figure out how to do it within the cCHCheckValid.ml match logic so I added the logic to the actual initialized checker. It now has a specific path that figures out if what we're looking at is argv[0] and marks it safe, closes the PO, and does not mark it for delegation. Probably not the cleanest solution, but it will do for now.
The logic was already in both cCHPOCheckNotNull.ml and in
cCHPOQuery.ml, although cCHPOCheckNotNull.ml was using
its own function instead of the one in the POQuery object.
This adds calls to the util function in the POQuery object and
nukes the private function in CheckNotNull.
With these changes, a simple hello world program no longer gets a
ton of open POs:
```
int main(int argc, char **argv) {
if (argc != 2) {
printf("ERROR: usage: %s <name>\n", argv[0]);
return 1;
}
printf("Hello world %s\n", argv[1]);
--------------------------------------------------------------------------------
| initialized-range((*(argv + 1):((char *) *)), len:cnapp(ntp((*(argv + 1):((char *) *))))|
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
| valid-mem((*(argv + 1):((char *) *))) |
| [augv[call]:$fn-entry$(-1):calls]:none |
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
| null-terminated((*(argv + 1):((char *) *))) |
| no invariants found for *(((lval (argv) +i 1):((char*)*)) |
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
| upper-bound(char,(*(argv + 1):((char *) *))) |
| no invariants for *(((lval (argv) +i 1):((char*)*)) |
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
| lower-bound(char,(*(argv + 1):((char *) *))) |
| no invariants found for *(((lval (argv) +i 1):((char*)*)) |
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
| ptr-upper-bound((*(argv + 1):((char *) *)), cnapp(ntp((*(argv + 1):((char *) *))), op:pluspi, typ: char)|
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
| in-scope((*(argv + 1):((char *) *))) |
| no invariants found for *(((lval (argv) +i 1):((char*)*)) |
--------------------------------------------------------------------------------
```
There's still one open pre-condition that I haven't figured out how to
close:
--------------------------------------------------------------------------------
| Preconditions: |
| ptr-upper-bound-deref(argv, 1, op:indexpi, typ: (char *)) |
--------------------------------------------------------------------------------
sipma
approved these changes
May 2, 2025
Contributor
sipma
left a comment
sipma
left a comment
There was a problem hiding this comment.
Thank you!
This is a good solution to handle these proof obligations.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
With these changes we no longer have a ton of open POs when programs
use command line arguments.
These fixes both issues when accessing
argv[0]directly (which is givenspecial treatment) and accessing other command line arguments after
checking that those exist (by looking at the value of
argc).Before these changes, these were all the open POs for a simple hello world
program:
Two pending things which I will tackle on the next set of commits:
close:
argcbefore accessingargvthen the diagnostics all relate to the fact that we don't haveinvariants to verify whether the access is correct or not, which makes it
sound like there's a bug in CHC. For example: