Commit c0a20122 authored by Alexander Weigl's avatar Alexander Weigl
Browse files

Merge remote-tracking branch 'origin/master' into weigl/kp2

* origin/master:
  replace GenRAP
  More Awareness for SonarQube Results
  Update .gitlab-ci.yml file
  Reports checkstyle issues via the codequality interface of gitlab-ci.
  Fix NullPointerException in absence of a source code file
  Improve automation with a rule dealing with nonNull(heap, null, sz) cases
  closes #1558
  fixing #991
parents 533fa955 030a6c71
......@@ -74,6 +74,7 @@ sonarqube:
script:
- cd key
- gradle --build-cache --continue -Dsonar.qualitygate.wait=true -DjacocoEnabled=true testFast sonarqube
- ./scripts/tools/sonarqube_hint.py
only:
- merge_requests
- master
......@@ -93,12 +94,13 @@ checkstyle:
image: wadoon/key-test-docker:jdk11
allow_failure: true
script:
- echo "**** Check the commit's gitlab page for a readable checkstyle report ****"
- (key/scripts/tools/checkstyle/runIncrementalCheckstyle.sh | tee report.txt) || true
- key/scripts/tools/checkstyle/publishAudit.py report.txt
- key/scripts/tools/checkstyle/translateAudit.py report.txt > report.json
artifacts:
name: "checkstyle-report-$CI_JOB_ID"
expire_in: 1 year
when: always
paths:
- report.txt
\ No newline at end of file
- report.txt
when: always
reports:
codequality: report.json
expire_in: 1 year
# KeY -- Deductive Java Program Verifier
[![Bugs](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=bugs)](https://sonarcloud.io/dashboard?id=key-main) [![Code Smells](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=code_smells)](https://sonarcloud.io/dashboard?id=key-main) [![Coverage](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=coverage)](https://sonarcloud.io/dashboard?id=key-main) [![Duplicated Lines (%)](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=duplicated_lines_density)](https://sonarcloud.io/dashboard?id=key-main) [![Lines of Code](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=ncloc)](https://sonarcloud.io/dashboard?id=key-main) [![Maintainability Rating](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=sqale_rating)](https://sonarcloud.io/dashboard?id=key-main) [![Quality Gate Status](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=alert_status)](https://sonarcloud.io/dashboard?id=key-main) [![Reliability Rating](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=reliability_rating)](https://sonarcloud.io/dashboard?id=key-main) [![Security Rating](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=security_rating)](https://sonarcloud.io/dashboard?id=key-main) [![Technical Debt](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=sqale_index)](https://sonarcloud.io/dashboard?id=key-main) [![Vulnerabilities](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=vulnerabilities)](https://sonarcloud.io/dashboard?id=key-main)
This folder contains the interactive theorem prover KeY for the verification of Java programs.
You can find more information on KeY on our [website](https://key-project.org) or in use the
You can find more information on KeY on our [website](https://key-project.org) or in use the
documentation in the companion repository [key-docs](https://git.key-project.org/key/key-docs).
The current version is 2.8.0, licensed under GPL v2.
The current version is 2.8.0, licensed under GPL v2.
## Requirements:
## Requirements:
* Hardware: >=2 GB RAM
* Operating System: Linux/Unix, MacOSX, Windows
* Java SE 8 or newer
* Optionally, KeY can make use of the following binaries:
* SMT Solvers:
* [Z3](https://github.com/Z3Prover/z3)
* [CVC4](http://cvc4.cs.stanford.edu/web/)
* SMT Solvers:
* [Z3](https://github.com/Z3Prover/z3)
* [CVC4](http://cvc4.cs.stanford.edu/web/)
## Content of the KeY folder
This folder provides a [gradle](https://gradle.org)-managed project following
This folder provides a [gradle](https://gradle.org)-managed project following
[Maven's standard folder layout](https://maven.apache.org/guides/introduction/introduction-to-the-standard-directory-layout.html).
There are several modules in this folder. In general every `key.*/` contains a core component of KeY. Additional
and optional components are in `keyext.*/` folders. The file `build.gradle` is the root build script describing
There are several modules in this folder. In general every `key.*/` contains a core component of KeY. Additional
and optional components are in `keyext.*/` folders. The file `build.gradle` is the root build script describing
the dependencies and build tasks for all sub-modules.
`key.util`, `key.core` and `key.ui` are the base for the product "KeY Prover". Special care are needed
if you plan to make changes here.
`key.util`, `key.core` and `key.ui` are the base for the product "KeY Prover". Special care are needed
if you plan to make changes here.
## Compile and Run KeY
Assuming you are in directory `key/`, the directory of this README file,
Assuming you are in directory `key/`, the directory of this README file,
then you can create a runnable and deployable version with one of these commands:
1. With `./gradlew :key.ui:run` you can run the user interface of KeY directly from the repository.
2. Use `./gradlew classes` to compile KeY, includes running JavaCC and Antlr, additional use `./gradlew testClasses` if
you also want to compile the JUnit test classes.
2. Use `./gradlew classes` to compile KeY, includes running JavaCC and Antlr, additional use `./gradlew testClasses` if
you also want to compile the JUnit test classes.
3. Test your installation with `./gradlew test` or `./gradlew testFast`.
3. Test your installation with `./gradlew test` or `./gradlew testFast`.
The later command disables the slow running test cases.
You can select a specific test case with `--tests` argument. Wildcards are allowed.
You can select a specific test case with `--tests` argument. Wildcards are allowed.
```
./gradlew :key.<subproject>:test --tests "<class>.<method>"
```
You can debug KeY by adding the `--debug-jvm` option, then attaching a debugger at `localhost:5005`.
4. You can create a single jar-version, aka *fat jar*, of KeY with
4. You can create a single jar-version, aka *fat jar*, of KeY with
```
./gradlew :key.ui:shadowJar
./gradlew :key.ui:shadowJar
```
The file is generated in `key.ui/build/libs/key-*-exe.jar`.
5. A distributiion is build with
5. A distributiion is build with
```
./gradlew :key.ui:installDist :key.ui:distZip
```
The distribution can tested by calling `key.ui/install/key/bin/key.ui`
The distribution can tested by calling `key.ui/install/key/bin/key.ui`
and is zipped in `key.ui/build/distributions`.
The distribution gives you potential of using single jar files.
# Developing KeY
* Quality is automatically assessed using [SonarQube](https://sonarqube.org) on each merge requests.
The results of the assessments can be found on
[SonarCloud.io](https://sonarcloud.io/dashboard?id=key-main)
([Branches](https://sonarcloud.io/project/branches?id=key-main))
The rules and quality gate are maintained by Alexander Weigl
<weigl@kit.edu> currently.
* More guideline and documentation for the KeY development can be found under
[key-docs](https://key-project.org/docs/).
# Issues and Bug Reports
If you encounter problems, please send a message to
......@@ -72,17 +89,18 @@ If you encounter problems, please send a message to
<support@key-project.org>
# License Remark
```
This is the KeY project - Integrated Deductive Software Design
Copyright (C) 2001-2011 Universität Karlsruhe, Germany
Universität Koblenz-Landau, Germany
and Chalmers University of Technology, Sweden
Copyright (C) 2011-2020 Karlsruhe Institute of Technology, Germany
Technical University Darmstadt, Germany
Chalmers University of Technology, Sweden
Universität Koblenz-Landau, Germany
and Chalmers University of Technology, Sweden
Copyright (C) 2011-2021 Karlsruhe Institute of Technology, Germany
Technical University Darmstadt, Germany
Chalmers University of Technology, Sweden
The KeY system is protected by the GNU General Public License.
The KeY system is protected by the GNU General Public License.
See LICENSE.TXT for details.
```
......@@ -156,7 +156,9 @@ public class WhileInvariantTransformation extends WhileLoopTransformation {
// unique representation of the replaced return
Statement assignExpr = KeYJavaASTFactory.assign(returnExpr,
x.getExpression(), x.getPositionInfo());
stmnts = KeYJavaASTFactory.block(assignFlag, assignExpr,
// changed order of statements to fix #991 (MT-1579)
stmnts = KeYJavaASTFactory.block(assignExpr, assignFlag,
breakInnerLabel);
} else
// Keep the PositionInfo because it is required for symbolic
......
......@@ -1410,6 +1410,15 @@
\heuristics(simplify_enlarging)
};
nullIsNotNonNull {
\schemaVar \term Object o;
\schemaVar \term Heap heapSV;
\schemaVar \term int depth;
\find (nonNull(heapSV,null,depth))
\replacewith ( false )
\heuristics(concrete)
};
nonNullZero {
\schemaVar \term Object o;
\schemaVar \term Heap heapSV;
......
......@@ -6,23 +6,37 @@ import de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile;
import java.io.File;
import java.io.IOException;
import java.io.InputStream;
import java.nio.charset.StandardCharsets;
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
import java.util.*;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;
import java.util.TreeSet;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
/**
* Generation of test cases (JUnit) for given proof collection files.
* <p>
* This class is intended to be called from gradle. See the gradle task
* {@code generateRunAllProofs}.
* <p>
* The considered proof collections files are configured
* statically in {@link #collections}.
*
* @author Alexander Weigl
* @version 1 (6/14/20)
*/
public class GenerateUnitTests {
static String outputFolder;
static String[] collections = new String[]{
/**
* Output folder. Set on command line.
*/
private static String outputFolder;
/**
* List of considered proofs collections.
*/
private final static String[] collections = new String[]{
RunAllProofsFunctional.INDEX_FILE,
RunAllProofsInfFlow.INDEX_FILE
};
......@@ -48,7 +62,7 @@ public class GenerateUnitTests {
}
}
static final String TEMPLATE_CONTENT = "package $packageName;\n" +
private static final String TEMPLATE_CONTENT = "package $packageName;\n" +
"\n" +
"import org.junit.*;\n" +
//"import de.uka.ilkd.key.util.NamedRunner;\n" +
......@@ -77,29 +91,23 @@ public class GenerateUnitTests {
"\n" +
"}\n";
private static String readAll(InputStream stream) {
byte[] buffer = new byte[1024 * 1024];
try {
int len = stream.read(buffer);
return new String(buffer, 0, len, StandardCharsets.UTF_8);
} catch (IOException e) {
e.printStackTrace();
}
return "";
}
/**
* Generates the test classes for the given proof collection,
* and writes the java files.
*
* @param col
* @param unit
* @throws IOException if the file is not writable
*/
private static void createUnitClass(ProofCollection col, RunAllProofsTestUnit unit) throws IOException {
String packageName = "de.uka.ilkd.key.proof.runallproofs.units";
String packageName = "de.uka.ilkd.key.proof.runallproofs";
String name = unit.getTestName();
String className = name
.replaceAll("\\.java", "")
.replaceAll("\\.key", "")
.replaceAll("[^a-zA-Z0-9]+", "_");
Path tmpDir = unit.getTempDir();
List<TestFile> files = unit.getTestFiles();
ProofCollectionSettings settings = unit.getSettings();
Map<String, String> vars = new TreeMap<>();
vars.put("className", className);
vars.put("packageName", packageName);
......@@ -117,7 +125,7 @@ public class GenerateUnitTests {
vars.put("timeout", "");
if (false) {
if (false) {// disabled
int globalTimeout = 0;
if (globalTimeout > 0)
vars.put("timeout", "@Rule public Timeout globalTimeout = Timeout.seconds(" + globalTimeout + ");");
......@@ -127,7 +135,7 @@ public class GenerateUnitTests {
Set<String> usedMethodNames = new TreeSet<>();
int clashCounter = 0;
for (TestFile file : unit.getTestFiles()) {
for (TestFile<?> file : unit.getTestFiles()) {
File keyFile = file.getKeYFile();
String testName = keyFile.getName()
.replaceAll("\\.java", "")
......@@ -139,24 +147,23 @@ public class GenerateUnitTests {
}
usedMethodNames.add(testName);
int timeout = 0;// (timeout <= 0 ? parent.timeout : 0)
String to = timeout > 0 ? "timeout=${1000 * timeout}" : "";
//int timeout = 0; (timeout <= 0 ? parent.timeout : 0)
String to = ""; //timeout > 0 ? "timeout=${1000 * timeout}" : "";
methods.append("\n");
methods.append("@Test(").append(to).append(")")
//.append("@TestName(\"").append(keyFile.getName()).append("\")")
.append("public void test").append(testName).append("() throws Exception {\n");
// "// This tests is based on").append(keyFile.getAbsolutePath()).append("\n");
String path = keyFile.getAbsolutePath().replace("\\", "/");
switch (file.getTestProperty()) {
case PROVABLE:
methods.append("assertProvability(\"").append(path).append("\");");
methods.append("assertProvability(\"").append(keyFile.getAbsolutePath()).append("\");");
break;
case NOTPROVABLE:
methods.append("assertUnProvability(\"").append(path).append("\");");
methods.append("assertUnProvability(\"").append(keyFile.getAbsolutePath()).append("\");");
break;
case LOADABLE:
methods.append("assertLoadability(\"").append(path).append("\");");
methods.append("assertLoadability(\"").append(keyFile.getAbsolutePath()).append("\");");
break;
}
methods.append("}");
......
......@@ -20,8 +20,22 @@ import java.util.List;
import static org.junit.Assert.*;
/**
* This class provides an API for running proves in JUnit test cases.
* <p>
* It is not intended to use this class outside of JUnit tests.
* The API mimics the same behavior as run-all-proves.
* So {@link #assertLoadability(String)}, {@link #assertLoadability(String)},
* and {@link #assertUnProvability(String)}
* correspond to the commands in the proof collection file.
* <p>
* Use the the member variables to configure the execution. Their meaning is identical to the variable in
* {@link de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollection}.
* <p>
* This class is used by generated unit tests from the proof collections.
*
* @author Alexander Weigl
* @version 1 (12.07.19)
* @see GenerateUnitTests
*/
public class ProveTest {
protected boolean verbose = Boolean.getBoolean("prooftests.verbose");
......@@ -46,8 +60,7 @@ public class ProveTest {
runKey(file, TestProperty.LOADABLE);
}
public void runKey(String file, TestProperty testProperty) throws Exception {
private void runKey(String file, TestProperty testProperty) throws Exception {
// Initialize KeY settings.
ProofSettings.DEFAULT_SETTINGS.loadSettingsFromString(globalSettings);
if (localSettings != null && !"".equals(localSettings)) {
......@@ -104,37 +117,21 @@ public class ProveTest {
}
}
String message = (success ? "pass: " : "FAIL: ")
+ "Verifying property \"" + testProperty.toString().toLowerCase()
+ "\"" + (success ? " was successful " : " failed ") + "for file: "
+ keyFile.toString();
String message = String.format("%sVerifying property \"%s\"%sfor file: %s",
success ? "pass: " : "FAIL: ",
testProperty.toString().toLowerCase(),
success ? " was successful " : " failed ",
keyFile.toString());
if (!success) {
fail(message);
}
}
private void debugOut(String format, Object... args) {
if (verbose) {
System.err.format(format, args);
}
}
private void appendStatistics(Proof loadedProof, File keyFile) {
// Write statistics.
StatisticsFile statisticsFile = getStatisticsFile();
if (statisticsFile != null) {
try {
statisticsFile.appendStatistics(loadedProof, keyFile);
} catch (IOException e) {
e.printStackTrace();
}
}
}
/**
* Override this method in order to change reload behaviour.
*/
protected void reload(File proofFile, Proof loadedProof) throws Exception {
private void reload(File proofFile, Proof loadedProof) throws Exception {
if (reloadEnabled) {
System.err.println("Test reloadability.");
// Save the available proof to a temporary file.
......@@ -151,8 +148,8 @@ public class ProveTest {
* By overriding this method we can change the way how we invoke automode,
* for instance if we want to use a different strategy.
*/
protected void autoMode(KeYEnvironment<DefaultUserInterfaceControl> env, Proof loadedProof,
Pair<String, Location> script) throws Exception {
private void autoMode(KeYEnvironment<DefaultUserInterfaceControl> env, Proof loadedProof,
Pair<String, Location> script) throws Exception {
// Run KeY prover.
if (script == null) {
// auto mode
......@@ -222,4 +219,21 @@ public class ProveTest {
return null;
}
}
\ No newline at end of file
private void appendStatistics(Proof loadedProof, File keyFile) {
// Write statistics.
StatisticsFile statisticsFile = getStatisticsFile();
if (statisticsFile != null) {
try {
statisticsFile.appendStatistics(loadedProof, keyFile);
} catch (IOException e) {
e.printStackTrace();
}
}
}
private void debugOut(String format, Object... args) {
if (verbose) {
System.err.format(format, args);
}
}
}
......@@ -148,7 +148,7 @@ public final class StrategySelectionView extends JPanel implements TabPanel {
JScrollPane javaDLOptionsScrollPane =
new JScrollPane(javaDLOptionsPanel,
ScrollPaneConstants.VERTICAL_SCROLLBAR_AS_NEEDED,
ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER);
ScrollPaneConstants.HORIZONTAL_SCROLLBAR_AS_NEEDED);
javaDLOptionsPanel.setEnabled(true);
......
......@@ -1071,6 +1071,10 @@ public final class SourceView extends JComponent {
symbExHighlights.clear();
if (lines == null) {
return;
}
try {
int mostRecentLine = -1;
......
......@@ -17,9 +17,9 @@ def getenv(*args):
rawReport = sys.argv[1]
SERVER = "https://git.key-project.org/"
URL, PID, TOKEN, SHA, BID, JID = getenv("CI_PROJECT_URL", "CI_PROJECT_ID",
URL, PID, TOKEN, SHA, BID, JID, MR_IID = getenv("CI_PROJECT_URL", "CI_PROJECT_ID",
"CI_COMMENT_TOKEN", "CI_COMMIT_SHA",
"CI_BUILD_ID", "CI_JOB_ID")
"CI_BUILD_ID", "CI_JOB_ID", "CI_MERGE_REQUEST_IID")
everythingIsFine = True
......@@ -65,7 +65,14 @@ You can produce a report locally by executing `key/key/scripts/tools/checkstyle/
print(note)
import requests
reportUrl = "%s/api/v4/projects/%s/repository/commits/%s/comments" % (SERVER,PID,SHA)
commitReportUrl = "%s/api/v4/projects/%s/repository/commits/%s/comments" % (SERVER,PID,SHA)
mergeRequestReportUrl = "%s/api/v4/projects/%s/merge_requests/%s/notes" %(SERVER, PID, MR_IID)
if MR_IID != "":
reportUrl = mergeRequestReportUrl
else:
reportUrl = commitReportUrl
print("Send report to", reportUrl)
resp = requests.post(reportUrl, data={ b'private_token': TOKEN, b'note':note })
print(note)
......
#!/usr/bin/python3
import sys
import os
import re
import json
from hashlib import sha224
# workflow:
# - runIncrementalCheckstyle.sh | tee report.txt
# - publishAudit.py report.txt
# The original was written in perl and is available under publishAudit.pl
# Written by Alexander Weigl
# Refactored in May 2018, by Mattias Ulbrich
def getenv(*args):
"relaxed access to environment"
return map(lambda x: os.environ.get(x, ""), args)
REGEX = re.compile(r'\[(?P<level>.*?)\] (?P<path>.*\/(?P<file>.*?)):(?P<line>\d+)(:\d+)?: (?P<msg>.*)')
#info, minor, major, blocker,critical
LEVEL_TO_SEVERITY = {
'INFO': 'info',
'WARN': 'minor',
'ERROR': 'major'
}
def main(filename):
with open(filename) as raw:
statistics = {'ERROR':0, 'WARN':0, 'INFO':0}
reports = list()
for line in raw:
m = REGEX.match(line)
if m:
old = statistics[m.group('level')]
statistics[m.group('level')] = old + 1
fingerprint = sha224(line.encode()).hexdigest()
#see https://docs.gitlab.com/ee/user/project/merge_requests/code_quality.html#implementing-a-custom-tool
entry = {
'description': m.group('msg'),
'fingerprint': fingerprint,
'severity': LEVEL_TO_SEVERITY[m.group('level')],
'location.path': os.path.join(m.group('path'),m.group('file')),
'location.lines.begin': m.group('line')
}
reports.append(entry)
json.dump(reports, sys.stdout, indent=4)
everythingIsFine = statistics['ERROR'] > 0 or statistics['WARN'] > 0
sys.exit(statistics["ERROR"])
######################################################
if __name__=='__main__':
main(sys.argv[1])
#!/usr/bin/python3
import sys
import os
import re
import urllib
import json
import pprint
import requests
HOST = "https://git.key-project.org/api/v4"
URL = os.environ["CI_PROJECT_URL"]
PROJECT_ID = os.environ["CI_PROJECT_ID"]
MR_IID = os.environ["CI_MERGE_REQUEST_IID"]
TOKEN = os.environ["CI_COMMENT_TOKEN"]
note = "SonarQube analysis was triggered. The [:beetle: results will appear on SonarCloud](https://sonarcloud.io/dashboard?id=key-main&pullRequest=%s) soon." % MR_IID
def isSonarQubeComment(obj):
return obj['body'].startswith("SonarQube analysis was triggered.")
checkUrl = "%s/projects/%s/merge_requests/%s/notes" % (HOST, PROJECT_ID, MR_IID)
print("Check For Hint at: ", checkUrl)
resp = requests.get(checkUrl, headers={"Private-Token": TOKEN})
if resp.status_code != 200:
print(resp.content)
sys.exit(0)
notesOnMr = resp.json()
print("Founds %s comments" % len(notesOnMr))
print("Check for comment on SonarQube.")
if not any(map(isSonarQubeComment, notesOnMr)):
reportUrl = "%s/projects/%s/merge_requests/%s/notes"% (HOST, PROJECT_ID, MR_IID)
print("Send report to", reportUrl)
resp = requests.post(reportUrl, data={ b'private_token': TOKEN, b'body': note })