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

version 1.1.0 released



see changelog
Signed-off-by: default avatarAlexander Weigl <weigl@kit.edu>
parent 2b23676d
package de.uka.ilkd.key.api;
import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.util.KeYConstants;
import org.jetbrains.annotations.NotNull;
import java.io.File;
import java.util.List;
......@@ -30,7 +32,6 @@ public abstract class KeYApi {
}
/**
*
* @return
*/
public static String getVersion() {
......
#KeY: ci-tool 1.1.0
ci-tool is a utility for supporting Java and JML contracts in Continuous Integration pipelines
by providing support for checking the proofability of JML with [KeY](https://key-project.org).
ci-tool is licensed under GPLv2+.
If you any suggestion feel to contact: [Alexander Weigl](https://formal.iti.kit.edu/weigl).
## Usage:
To use the ci-tool add the following lines to the ci config.
1. Get the latest version from the server:
```bash
$ wget -O ci-tool.jar https://key-project.org/ci-tool
```
2. Call ci-tool with your key-files or java file (or folder).
ci-tool tries to verify all proofs automatically and uses found proofs or script files.
```bash
$ java -jar <jarfile> [files]
```
3. Find more parameters with `-h`
```bash
$ java -jar <jarfile> -h
```
### Examples
For travis-ci:
```yaml
jdk:
- openjdk11
language: java
install:
- wget -O ci-tool.jar https://key-project.org/ci-tool
script:
- javac simplified/Keyserver.java
- java -jar ci-tool.jar simplified/Keyserver.java
```
## Changelog
* [1.1.0](https://formal.iti.kit.edu/ci-tool/keyext.citool-1.1.0-all.jar): bug fixes and support for proofs in key-files
- Change of console output
- Fix loading of proof files
- Add download URL and a website
- Known Bug: Something with the proof (search) path is wrong.
* [1.0.0](https://formal.iti.kit.edu/ci-tool/keyext.citool-1.0.0-all.jar) initial working version (*24.01.2020*)
- first release of this project after positive of the a small `jshell` utility.
- deploy on VerifyThis LTC 2020 repository
## Future features
* Accumulate statistics
* If proof remains open,
* Calculate a coverage based on statements in the
......@@ -4,6 +4,8 @@ plugins {
id 'com.github.johnrengelman.shadow' version "5.0.0"
}
version = "1.1.0"
dependencies {
implementation "org.jetbrains.kotlin:kotlin-stdlib-jdk8"
implementation project(":key.ui")
......
#!/bin/bash -x
# stop on error
set -e
rm -rf build/libs/
(cd ..;
gradle :keyext.citool:shadowJar --parallel)
cat >build/index.html <<eof
<html>
<head>
<style>body {width:60em; margin:auto;}</style>
<title>ci-tool</title></head>
<body>
eof
markdown2 -x code-friendly -x fenced-code-blocks -x header-ids -x smarty-pants \
README.md >> build/index.html
#curl https://api.github.com/markdown/raw \
# -X "POST" -H "Content-Type: text/plain" --data "@README.md"\
# >> build/index.html
echo "</body></html>" >> build/index.html
rsync -v build/libs/*citool-*-all.jar \
build/index.html\
i57adm.ira.uka.de:/misc/HomePages/UserHomePages/i57/weigl/ci-tool/
\ No newline at end of file
......@@ -9,17 +9,30 @@ import com.github.ajalt.clikt.parameters.options.multiple
import com.github.ajalt.clikt.parameters.options.option
import com.github.ajalt.clikt.parameters.types.int
import de.uka.ilkd.key.api.KeYApi
import de.uka.ilkd.key.api.ProofManagementApi
import de.uka.ilkd.key.control.AbstractProofControl
import de.uka.ilkd.key.control.AbstractUserInterfaceControl
import de.uka.ilkd.key.control.KeYEnvironment
import de.uka.ilkd.key.macros.scripts.ProofScriptEngine
import de.uka.ilkd.key.parser.Location
import de.uka.ilkd.key.proof.Proof
import de.uka.ilkd.key.settings.ChoiceSettings
import de.uka.ilkd.key.settings.ProofSettings
import de.uka.ilkd.key.speclang.Contract
import de.uka.ilkd.key.util.KeYConstants
import de.uka.ilkd.key.util.MiscTools
import java.io.File
import kotlin.system.exitProcess
import kotlin.system.measureTimeMillis
const val ESC = 27.toChar()
const val RED = 31;
const val GREEN = 32;
const val YELLOW = 33;
const val BLUE = 34;
const val MAGENTA = 35;
const val CYAN = 36;
fun color(s: Any, c: Int) = "${ESC}[${c}m$s${ESC}[0m"
/**
* A small interface for a checker scripts
......@@ -59,8 +72,6 @@ class Checker : CliktCommand() {
help = "folders to look for proofs and script files")
.multiple()
//val tacletChoices by option("-T").multiple()
private var choiceSettings: ChoiceSettings? = null
private fun initEnvironment() {
......@@ -71,88 +82,162 @@ class Checker : CliktCommand() {
choiceSettings = ProofSettings.DEFAULT_SETTINGS.choiceSettings
}
var errorlevel = 0
var errors = 0
override fun run() {
printm("KeY version: ${KeYConstants.VERSION}")
printm("KeY internal: ${KeYConstants.INTERNAL_VERSION}")
printm("Copyright: ${KeYConstants.COPYRIGHT}")
printm("More information at: https://formal.iti.kit.edu/weigl/ci-tool/")
inputFile.forEach { run(it) }
exitProcess(errorlevel)
exitProcess(errors)
}
var currentPrintLevel = 0;
fun printBlock(message: String, f: () -> Unit) {
printm(message)
currentPrintLevel++
f()
currentPrintLevel--
}
fun printm(message: String, fg: Int? = null) {
print(" ".repeat(currentPrintLevel))
if (fg != null)
println(color(message, fg))
else
println(message)
}
fun run(input: String) {
println("* $input: ")
val pm = KeYApi.loadProof(File(input),
classpath.map { File(it) },
bootClassPath?.let { File(it) },
includes.map { File(it) })
val contracts = pm.proofContracts
.filter { it.name in onlyContracts || onlyContracts.isEmpty() }
for (c in contracts) {
print(" * ${c.name}")
val filename = MiscTools.toValidFileName(c.name);
if (c.name in forbidContracts) {
println(" ... excluded (--forbid-contract) ")
} else {
if (dryRun) {
println(" ... skipped (--dry-run). ")
} else {
val proofApi = pm.startProof(c)
var proof = proofApi.proof
require(proof != null)
proof?.settings?.strategySettings?.maxSteps = autoModeStep
ProofSettings.DEFAULT_SETTINGS.strategySettings.maxSteps = autoModeStep
val proofFile = findProofFile(filename)
val scriptFile = findScriptFile(filename)
var autoMode = true
if (proofFile != null) {
println()
print(" * Proof found: $proofFile. Try loading. ")
val loaded = KeYApi.loadProof(File(proofFile),
classpath.map { File(it) },
bootClassPath?.let { File(it) },
includes.map { File(it) })
proof = loaded.loadedProof.proof
autoMode = false
}
if (scriptFile != null) {
println()
print(" * Script found: $scriptFile. Try proving. ")
autoMode = false
val script = File(scriptFile).readText()
val engine = ProofScriptEngine(script,
Location(scriptFile, 1, 1))
val startTime = System.currentTimeMillis()
engine.execute(
proofApi.env.ui as AbstractUserInterfaceControl, proofApi.proof)
val endTime = System.currentTimeMillis()
print(" ... script took ${endTime - startTime} ms... ")
}
printBlock("[INFO] Start with `$input`") {
val pm = KeYApi.loadProof(File(input),
classpath.map { File(it) },
bootClassPath?.let { File(it) },
includes.map { File(it) })
if (autoMode) {
val startTime = System.currentTimeMillis()
proofApi.env.proofControl.startAndWaitForAutoMode(proof)
val endTime = System.currentTimeMillis()
print("... auto-mode took ${endTime - startTime} ms... ")
}
val contracts = pm.proofContracts
.filter { it.name in onlyContracts || onlyContracts.isEmpty() }
if (proof.closed()) {
println("PROOF CLOSED! Rule apps: ${proof.statistics.totalRuleApps}")
} else {
println("${proof.openGoals().size()} remains open")
errorlevel = 1
printm("[INFO] Found: ${contracts.size}")
var successful = 0
var ignored = 0
var failure = 0
for (c in contracts) {
printBlock("[INFO] Contract: `${c.name}`") {
val filename = MiscTools.toValidFileName(c.name)
when {
c.name in forbidContracts -> {
printm(" [INFO] Contract excluded by `--forbid-contract`")
ignored++
}
dryRun -> {
printm("[INFO] Contract skipped by `--dry-run`")
ignored++
}
else -> {
val b = runContract(pm, c, filename)
if (b) successful++ else failure++
}
}
proof.dispose()
}
}
printm("[INFO] Summary for $input: " +
"(successful/ignored/failure) " +
"(${color(successful, GREEN)}/${color(ignored, BLUE)}/${color(failure, RED)})")
if (failure != 0)
printm("[ERR ] $input failed!", fg = RED)
}
}
private fun runContract(pm: ProofManagementApi, c: Contract?, filename: String): Boolean {
val proofApi = pm.startProof(c)
val proof = proofApi.proof
require(proof != null)
proof.settings?.strategySettings?.maxSteps = autoModeStep
ProofSettings.DEFAULT_SETTINGS.strategySettings.maxSteps = autoModeStep
val proofFile = findProofFile(filename)
val scriptFile = findScriptFile(filename)
val ui = proofApi.env.ui as AbstractUserInterfaceControl
val pc = proofApi.env.proofControl as AbstractProofControl
val closed = when {
proofFile != null -> {
printm("[INFO] Proof found: $proofFile. Try loading.")
loadProof(proofFile)
}
scriptFile != null -> {
printm("[INFO] Script found: $scriptFile. Try proving.")
loadScript(ui, proof, scriptFile)
}
else -> {
if (verbose)
printm("[INFO] No proof or script found. Fallback to auto-mode.")
runAutoMode(pc, proof)
}
}
if (closed) {
printm("[OK ] ✔ Proof closed.", fg = GREEN)
} else {
errors++
printm("[ERR ] ✘ Proof open.", fg = RED)
if (verbose)
printm("[FINE] ${proof.openGoals().size()} remains open")
}
proof.dispose()
return closed
}
private fun runAutoMode(proofControl: AbstractProofControl, proof: Proof): Boolean {
val time = measureTimeMillis {
proofControl.startAndWaitForAutoMode(proof)
}
if (verbose) {
printm("[FINE] Auto-mode took ${time / 1000.0} seconds.")
}
printStatistics(proof)
return proof.closed()
}
private fun loadScript(ui: AbstractUserInterfaceControl, proof: Proof, scriptFile: String): Boolean {
val script = File(scriptFile).readText()
val engine = ProofScriptEngine(script, Location(scriptFile, 1, 1))
val time = measureTimeMillis {
engine.execute(ui, proof)
}
print("Script execution took ${time / 1000.0} seconds.")
printStatistics(proof)
return proof.closed()
}
private fun loadProof(keyFile: String): Boolean {
val env = KeYEnvironment.load(File(keyFile))
try {
val proof = env?.loadedProof
try {
if (proof == null) {
printm("[ERR] No proof found in given KeY-file.", fg = 38)
return false
}
printStatistics(proof)
return proof.closed()
} finally {
proof?.dispose()
}
} finally {
env.dispose()
}
}
private fun printStatistics(proof: Proof) {
if (verbose) {
proof.statistics.summary.forEach { p -> printm("[FINE] ${p.first} = ${p.second}") }
}
}
......@@ -162,10 +247,10 @@ class Checker : CliktCommand() {
candidates
}
private fun findProofFile(filename: String): String? = proofFileCandidates.find { it.startsWith(filename) && (it.endsWith(".proof") || it.endsWith(".proof.gz")) }
private fun findScriptFile(filename: String): String? = proofFileCandidates.find { it.startsWith(filename) && (it.endsWith(".txt") || it.endsWith(".pscript")) }
}
fun main(args: Array<String>) = Checker().main(args)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment