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

Overflow follow up fix #3490

Merged
merged 3 commits into from
Jun 26, 2024
Merged

Overflow follow up fix #3490

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
11fa899
ensure that the update is copied to \add part of rules (\sameUpdateLe…
WolframPfeifer Jun 25, 2024
8ba8a2c
test cases for integer semantics
WolframPfeifer Jun 25, 2024
d3a1d28
adapt test oracle to changed taclets
WolframPfeifer Jun 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 30 additions & 0 deletions key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@
\find(\modality{#normalassign}{..
#loc = #seCharByteShortInt0 * #seCharByteShortInt1;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1)))
Expand All @@ -56,6 +57,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt * #seLong;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(mul(#seCharByteShortInt, #seLong)))
Expand All @@ -70,6 +72,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong * #seCharByteShortInt;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(mul(#seLong, #seCharByteShortInt)))
Expand All @@ -84,6 +87,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 * #seLong1;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(mul(#seLong0, #seLong1)))
Expand Down Expand Up @@ -280,6 +284,7 @@
\find(\modality{#normalassign}{..
#loc = #seCharByteShortInt0 - #seCharByteShortInt1;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1)))
Expand All @@ -294,6 +299,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt - #seLong;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(sub(#seCharByteShortInt, #seLong)))
Expand All @@ -308,6 +314,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong - #seCharByteShortInt;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(sub(#seLong, #seCharByteShortInt)))
Expand All @@ -323,6 +330,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 - #seLong1;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(sub(#seLong0, #seLong1)))
Expand All @@ -339,6 +347,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt0 + #seCharByteShortInt1;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inInt(add(#seCharByteShortInt0, #seCharByteShortInt1)))
Expand All @@ -354,6 +363,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt + #seLong;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(add(#seCharByteShortInt, #seLong)))
Expand All @@ -369,6 +379,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong + #seCharByteShortInt;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(add(#seLong, #seCharByteShortInt)))
Expand All @@ -384,6 +395,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 + #seLong1;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(add(#seLong0, #seLong1)))
Expand Down Expand Up @@ -541,6 +553,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt0 >> #se;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inInt(shiftright(#seLong0, #se)))
Expand All @@ -556,6 +569,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 >> #se;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inInt(shiftright(#seLong0, #se)))
Expand All @@ -573,6 +587,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt0 << #se; ...}
\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inInt(shiftleft(#seCharByteShortInt0, #se)))
Expand All @@ -588,6 +603,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 << #se;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(shiftleft(#seLong0, #se)))
Expand All @@ -605,6 +621,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt0 >>> #se; ...}
\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(unsignedshiftrightJint(#seCharByteShortInt0, #se)))
Expand All @@ -620,6 +637,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 >>> #se;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(unsignedshiftrightJlong(#seLong0, #se)))
Expand All @@ -638,6 +656,7 @@
\find(\modality{#normalassign}{..
#loc = - #seCharByteShortInt;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inInt(neg(#seCharByteShortInt)))
Expand All @@ -652,6 +671,7 @@
\find(\modality{#normalassign}{..
#loc = - #seLong;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inLong(neg(#seLong)))
Expand Down Expand Up @@ -686,6 +706,7 @@
\find(\modality{#normalassign}{..
#loc = (byte) #seShort;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inByte(#seShort))
Expand All @@ -700,6 +721,7 @@
\find(\modality{#normalassign}{..
#loc = (byte) #seInt;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inByte(#seInt))
Expand All @@ -714,6 +736,7 @@
\find(\modality{#normalassign}{..
#loc = (byte) #seLong;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inByte(#seLong))
Expand All @@ -728,6 +751,7 @@
\find(\modality{#normalassign}{..
#loc = (short) #seInt;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inShort(#seInt))
Expand All @@ -742,6 +766,7 @@
\find(\modality{#normalassign}{..
#loc = (short) #seLong;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inShort(#seLong))
Expand All @@ -754,6 +779,7 @@

narrowingIntCastLong {
\find(\modality{#normalassign}{.. #loc = (int) #seLong; ...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inInt(#seLong))
Expand All @@ -768,6 +794,7 @@
\find(\modality{#normalassign}{..
#loc = (char) #seByte;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inChar(#seByte))
Expand All @@ -783,6 +810,7 @@
\find(\modality{#normalassign}{..
#loc = (char) #seShort;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inChar(#seShort))
Expand All @@ -798,6 +826,7 @@
\find(\modality{#normalassign}{..
#loc = (char) #seInt;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inChar(#seInt))
Expand All @@ -812,6 +841,7 @@
\find(\modality{#normalassign}{..
#loc = (char) #seLong;
...}\endmodality (post))
\sameUpdateLevel
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\add(==> inChar(#seLong))
Expand Down
70 changes: 70 additions & 0 deletions key.core/src/test/java/de/uka/ilkd/key/rule/IntSemanticsTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
/* This file is part of KeY - https://key-project.org
* KeY is licensed under the GNU General Public License Version 2
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.rule;

import java.io.File;

import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.api.ProofApi;
import de.uka.ilkd.key.api.ProofManagementApi;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;

import org.key_project.util.helper.FindResources;

import org.junit.jupiter.api.Assertions;
import org.junit.jupiter.params.ParameterizedTest;
import org.junit.jupiter.params.provider.ValueSource;

/**
* These tests check that the integer taclet options still work as intended, for example that the
* additional branches for overflow checks are still generated correctly. At the moment, for each of
* the three taclet options there is one positive (provable) and one negative (unprovable) test.
*
* @author Wolfram Pfeifer
*/
class IntSemanticsTest {
private static final File TEST_DIR = new File(FindResources.getTestResourcesDirectory(),
"/de/uka/ilkd/key/rule/intSemantics/");

/**
* This test checks that certain proofs containing integer corner cases are reloadable.
*
* @param filename name of the .proof file containing a closed proof and also setting the
* desired taclet option for the integer semantics.
* @throws ProblemLoaderException should not happen
*/
@ParameterizedTest
@ValueSource(strings = { "java/mJava.proof",
"uncheckedOF/mBigint.proof",
"checkedOF/mOFCheck.proof" })
void testSemanticsProvable(String filename) throws ProblemLoaderException {
File proofFile = new File(TEST_DIR, filename);
ProofManagementApi pmapi = KeYApi.loadProof(proofFile);
Proof proof = pmapi.getLoadedProof().getProof();
// Proof should be reloaded completely now. If not, the int semantics are probably broken.
Assertions.assertTrue(proof.closed());
}

/**
* This test checks that certain contracts are not provable with the selected integer semantics.
*
* @param filename name of the .key file that points to the contract. The desired integer
* semantics need to be set correctly here!
* @throws ProblemLoaderException should not happen
*/
@ParameterizedTest
@ValueSource(strings = { "java/mJavaWrong.key",
"uncheckedOF/mBigintWrong.key",
"checkedOF/mOFCheckWrong.key", })
void testSemanticsUnprovable(String filename) throws ProblemLoaderException {
File keyFile = new File(TEST_DIR, filename);
ProofManagementApi pmapi = KeYApi.loadFromKeyFile(keyFile);
ProofApi proofApi = pmapi.getLoadedProof();
Proof proof = proofApi.getProof();
proofApi.getEnv().getProofControl().startAndWaitForAutoMode(proof);
// we expect that exactly one branch (the overflow check) is open now:
Assertions.assertEquals(1, proof.openGoals().size());
}
}
Loading
Loading