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

Potential overflows detected by Prusti #974

Closed
djc opened this issue Feb 26, 2023 · 16 comments
Closed

Potential overflows detected by Prusti #974

djc opened this issue Feb 26, 2023 · 16 comments

Comments

@djc
Copy link
Member

djc commented Feb 26, 2023

See https://github.com/viperproject/prusti-dev.

Screenshot 2023-02-26 at 22 17 30

@xemwebe
Copy link

xemwebe commented Apr 15, 2023

While looking into this, I stumbled over how to deal with cases, where potential overflow is detected by prust, but considering the actual range of parameters can never happen. E.g. consider DateTime::years_since (the first hit in your list):

    pub fn years_since(&self, base: Self) -> Option<u32> {
        let mut years = self.year() - base.year();
        ...
    }

Since the allowed year range is -262144..=262143, the subtraction can never underflow nor overflow with years as i32. However, this might change if the allow year range should be eventually extended to cover the full range of i32.

@xemwebe
Copy link

xemwebe commented Apr 15, 2023

I have marked all detected code pieces and added some fixes here: https://github.com/xemwebe/chrono.git

@jtmoon79
Copy link
Contributor

I have marked all detected code pieces and added some fixes here: https://github.com/xemwebe/chrono.git

Thanks @xemwebe . Can you post a direct link to the diff that maintainers should look at?

@xemwebe
Copy link

xemwebe commented Apr 15, 2023

@jtmoon79 : sure, here is the link: https://github.com/xemwebe/chrono/compare/main..fix-overflows
Please note that this branch is yet far from completing the issue, but merely a basis for discussions.

@xemwebe
Copy link

xemwebe commented Apr 16, 2023

TimeDelta has methods add, neg, mul and div could all overflow. How would you like to handle these? Mark these functions as deprecated and write new methods with and appending _opt and returning an Option?

Also, these methods

const fn div_mod_floor_64(this: i64, other: i64) -> (i64, i64);
const fn div_floor_64(this: i64, other: i64) -> i64;
const fn mod_floor_64(this: i64, other: i64) -> i64;
const fn div_rem_64(this: i64, other: i64) -> (i64, i64);

seem to duplicate the methods of the Integer trait, except for the const feature. Could these functions be merged to remove duplicates?

There is also the issue, that all cases of diversions a/b or a%b could overflow, if a is the minimal integer (e.g. i32::MIN) and b==-1 since -i32::MIN==i32::MAX+1. At least some of these cases seem to be undetected by prusti.

@xemwebe
Copy link

xemwebe commented Apr 16, 2023

I have updated my findings.

@jtmoon79
Copy link
Contributor

jtmoon79 commented Apr 16, 2023

TimeDelta has methods add, neg, mul and div could all overflow. How would you like to handle these? Mark these functions as deprecated and write new methods with and appending _opt and returning an Option?

At first glance, that seems a reasonable way to slowly introduce more safety, and matches the approach done for dates.

I'd wait for @djc and/or @esheppa chime in.


Also, these methods ... seem to duplicate the methods of the Integer trait, except for the const feature. Could these functions be merged to remove duplicates?

I know what you're getting at but it would help me if you created a new Draft PR or your own new branch to demonstrate exactly your intent. Could that be done?


There is also the issue, that all cases of diversions a/b or a%b could overflow, if a is the minimal integer (e.g. i32::MIN) and b==-1 since -i32::MIN==i32::MAX+1. At least some of these cases seem to be undetected by prusti.

Is this covered by your latest code in src/utils.rs?

    fn safe_mod(self, other: Self) -> Self {

(https://github.com/xemwebe/chrono/compare/main..fix-overflows#diff-23af5356f6001cd3993cd3c801fb7716ea02d1e504081b9fb569332db6107e80R49-R55)

@djc
Copy link
Member Author

djc commented Apr 17, 2023

So I think the current plan is to redefine TimeDelta as roughly enum TimeDelta { Forward(std::core::Duration), Backward(std::core::Duration) }, and we would probably not define any methods on it. I think @esheppa started some PRs in this direction.

@esheppa
Copy link
Collaborator

esheppa commented Apr 17, 2023

In the latest PR's I've defined it using Result rather than an entirely new enum, (as that allows using the same principle everywhere, eg with Days, Weeks and Months if desired) - which would prevent us adding any methods anyway

@xemwebe
Copy link

xemwebe commented Apr 17, 2023

Also, these methods ... seem to duplicate the methods of the Integer trait, except for the const feature. Could these functions be merged to remove duplicates?

I know what you're getting at but it would help me if you created a new Draft PR or your own new branch to demonstrate exactly your intent. Could that be done?

Yes, of course, I could try if this would work without problems.

There is also the issue, that all cases of diversions a/b or a%b could overflow, if a is the minimal integer (e.g. i32::MIN) and b==-1 since -i32::MIN==i32::MAX+1. At least some of these cases seem to be undetected by prusti.

Is this covered by your latest code in src/utils.rs?

    fn safe_mod(self, other: Self) -> Self {

(https://github.com/xemwebe/chrono/compare/main..fix-overflows#diff-23af5356f6001cd3993cd3c801fb7716ea02d1e504081b9fb569332db6107e80R49-R55)

Yes, but only for a%b, which is the simpler case, since i32::MIN%(-1)==0, which does not introduce the requirement for introducing Option or Result, other than the case i32::MIN/(-1)==i32::MAX+1.

@xemwebe
Copy link

xemwebe commented Apr 17, 2023

In the latest PR's I've defined it using Result rather than an entirely new enum, (as that allows using the same principle everywhere, eg with Days, Weeks and Months if desired) - which would prevent us adding any methods anyway

Which PR is this?

@xemwebe
Copy link

xemwebe commented Apr 17, 2023

Also, these methods ... seem to duplicate the methods of the Integer trait, except for the const feature. Could these functions be merged to remove duplicates?

I know what you're getting at but it would help me if you created a new Draft PR or your own new branch to demonstrate exactly your intent. Could that be done?

Yes, of course, I could try if this would work without problems.
const fn are not allowed in traits, therefore this functions could not be removed.

@xemwebe
Copy link

xemwebe commented Apr 18, 2023

update after some overflows have been fixed by merge to 0.4.x

This rises a question: What merge policy do you follow with respect to 0.4.x, 0.5.x, and main? Is 0.4.x regularly merged to 0.5-alpha, which will eventually be merged to main?

@xemwebe
Copy link

xemwebe commented Apr 19, 2023

I was trying to prepare a PR for at least those fixes that are not related to TimeDelta (which won't stay at it is) and do not require to break any signature (which would be required for some timestamp methods and the div related method in the Integer trait).
I am a bit confused what would be the best target branch to merge to. 0.5-alpha is kind of out-of-date. Is this branch still active? Would main be the better target (the Integer trait which will be effected, is a recent addition to the main branch)?

@pitdicker
Copy link
Collaborator

pitdicker commented Jun 4, 2023

List of all the potential overflows in this issue and their status:

It is curious that this didn't catch the overflows in #1048 and #1093.

@djc
Copy link
Member Author

djc commented Jun 4, 2023

Awesome work, thanks.

@djc djc closed this as completed Jun 4, 2023
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

No branches or pull requests

5 participants