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.

Sign up for GitHub

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

Jump to bottom

Overflow checking #3027

Merged
merged 10 commits into from
Mar 23, 2023
Merged

Overflow checking #3027

merged 10 commits into from
Mar 23, 2023

Conversation

jwiesler
Copy link
Contributor

@jwiesler jwiesler commented Feb 6, 2023 •
edited
Loading

This is a follow up to #3014.

This MR implements overflow checking of all arithmetic operations in code by opening a new goal where the absence of overflows has to be proven.

Furthermore, it deduplicates and rearranges a lot of rules.

There are some todos where I was unsure, if you know an answer to any of them please add a comment.

@jwiesler jwiesler self-assigned this Feb 6, 2023
@jwiesler jwiesler added Feature New feature or request Review Request Waiting for review labels Feb 6, 2023
@jwiesler jwiesler changed the title Overflow checking Draft: Overflow checking Feb 6, 2023
@mattulbrich mattulbrich marked this pull request as draft February 7, 2023 07:20
@mattulbrich
Copy link
Member

Where are thr todo items?

@jwiesler
Copy link
Contributor Author

jwiesler commented Feb 7, 2023 •
edited
Loading

The todos are in code.

Edit: opened reviews for them.

jwiesler
jwiesler commented Feb 7, 2023
View reviewed changes
key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key Outdated Show resolved Hide resolved
key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key Outdated Show resolved Hide resolved
key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key Outdated Show resolved Hide resolved
key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key Outdated Show resolved Hide resolved
key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key Outdated Show resolved Hide resolved
key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key Outdated Show resolved Hide resolved
key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key Outdated Show resolved Hide resolved
@samysweb samysweb mentioned this pull request Mar 13, 2023
Draft
14 tasks
unp1
unp1 approved these changes Mar 20, 2023
View reviewed changes
Copy link
Member

@unp1 unp1 left a comment

Choose a reason for hiding this comment

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

The only additional comment I have is to check whether the ruleset "defOps_expandRanges" is still used. Otherwise it should be removed from the ruleSetsDeclarations.key file as well as its computation in JavaCardDLStrategy.

@jwiesler
Copy link
Contributor Author

defOps_expandRanges is still used by the same taclets as before, e.g. replace_char_MIN and expandInRangeChar.

@jwiesler jwiesler changed the title Draft: Overflow checking Overflow checking Mar 20, 2023
@jwiesler jwiesler marked this pull request as ready for review March 21, 2023 11:42
@jwiesler jwiesler added this pull request to the merge queue Mar 23, 2023
Merged via the queue into KeYProject:main with commit 623a20e Mar 23, 2023
@jwiesler jwiesler deleted the overflowChecking branch March 23, 2023 11:10
@WolframPfeifer WolframPfeifer mentioned this pull request Nov 15, 2023
Closed
@WolframPfeifer WolframPfeifer mentioned this pull request Jun 21, 2024
Merged
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@unp1 unp1 unp1 approved these changes

@mattulbrich mattulbrich Awaiting requested review from mattulbrich

Assignees

@jwiesler jwiesler

Labels
Feature New feature or request Review Request Waiting for review
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@jwiesler @mattulbrich @unp1 @wadoon