Skip to content

Commit

Permalink
fix compile errors
Browse files Browse the repository at this point in the history
  • Loading branch information
@wadoon
wadoon committed Apr 23, 2024
1 parent fbf6d00 commit 4545251
Show file tree
Hide file tree
Showing 33 changed files with 456 additions and 413 deletions.
15 changes: 9 additions & 6 deletions ...xecution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,10 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.symbolic_execution.rule;

import java.util.LinkedHashSet;
import java.util.List;
import java.util.Set;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.op.*;
Expand All @@ -11,15 +15,13 @@
import de.uka.ilkd.key.rule.*;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
import org.jspecify.annotations.NonNull;

import org.key_project.logic.Name;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.Pair;

import java.util.LinkedHashSet;
import java.util.List;
import java.util.Set;
import org.jspecify.annotations.NonNull;

/**
* <p>
Expand Down Expand Up @@ -180,8 +182,9 @@ public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
Set<Term> resultTerms = new LinkedHashSet<>();
for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) {
Term conditionTerm = tb.and(conditionsAndResult.conditions());
Term resultEqualityTerm = varFirst ? tb.equals(conditionsAndResult.result(), otherTerm)
: tb.equals(otherTerm, conditionsAndResult.result());
Term resultEqualityTerm =
varFirst ? tb.equals(conditionsAndResult.result(), otherTerm)
: tb.equals(otherTerm, conditionsAndResult.result());
Term resultTerm = pio.isInAntec() ? tb.imp(conditionTerm, resultEqualityTerm)
: tb.and(conditionTerm, resultEqualityTerm);
resultTerms.add(resultTerm);
Expand Down
5 changes: 3 additions & 2 deletions ...c_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -237,8 +237,9 @@ public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
if (pio.isTopLevel() || queryConditionTerm != null) {
for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) {
Term conditionTerm = tb.and(conditionsAndResult.conditions());
Term newEqualityTerm = varFirst ? tb.equals(varTerm, conditionsAndResult.result())
: tb.equals(conditionsAndResult.result(), varTerm);
Term newEqualityTerm =
varFirst ? tb.equals(varTerm, conditionsAndResult.result())
: tb.equals(conditionsAndResult.result(), varTerm);
Term resultTerm = pio.isInAntec() ? tb.imp(conditionTerm, newEqualityTerm)
: tb.and(conditionTerm, newEqualityTerm);
if (queryConditionTerm != null) {
Expand Down
102 changes: 52 additions & 50 deletions ...src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ public KeYEnvironment(U ui, InitConfig initConfig) {
* @param initConfig The loaded project.
*/
public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof,
@Nullable ProofScriptEntry proofScript, ReplayResult replayResult) {
@Nullable ProofScriptEntry proofScript, ReplayResult replayResult) {
this.ui = ui;
this.initConfig = initConfig;
this.loadedProof = loadedProof;
Expand Down
2 changes: 1 addition & 1 deletion key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ public static class File extends KeyAst<KeYParser.FileContext> {
if (ctx.problem() != null && ctx.problem().proofScript() != null) {
KeYParser.ProofScriptContext pctx = ctx.problem().proofScript();
Location location = new Location(url,
Position.newOneBased(pctx.ps.getLine(), pctx.ps.getCharPositionInLine()));
Position.newOneBased(pctx.ps.getLine(), pctx.ps.getCharPositionInLine()));

String text = pctx.ps.getText();
return new ProofScriptEntry(StringUtil.trim(text, '"'), location);
Expand Down
2 changes: 1 addition & 1 deletion key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,13 +21,13 @@
import de.uka.ilkd.key.speclang.SLEnvInput;
import de.uka.ilkd.key.util.ProgressMonitor;

import org.jspecify.annotations.Nullable;
import org.key_project.util.collection.DefaultImmutableSet;
import org.key_project.util.collection.ImmutableSet;

import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.Token;
import org.jspecify.annotations.NonNull;
import org.jspecify.annotations.Nullable;


/**
Expand Down
106 changes: 54 additions & 52 deletions key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,20 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof.io;

import java.io.ByteArrayInputStream;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.nio.charset.StandardCharsets;
import java.nio.file.*;
import java.util.*;
import java.util.function.Consumer;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import java.util.zip.ZipFile;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.nparser.KeYLexer;
import de.uka.ilkd.key.nparser.ProofScriptEntry;
Expand All @@ -22,28 +36,16 @@
import de.uka.ilkd.key.strategy.Strategy;
import de.uka.ilkd.key.strategy.StrategyProperties;
import de.uka.ilkd.key.util.ExceptionHandlerException;
import org.antlr.runtime.MismatchedTokenException;
import org.jspecify.annotations.Nullable;

import org.key_project.util.collection.Pair;
import org.key_project.util.java.IOUtil;
import org.key_project.util.reflection.ClassLoaderUtil;

import org.antlr.runtime.MismatchedTokenException;
import org.jspecify.annotations.Nullable;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import java.io.ByteArrayInputStream;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.nio.charset.StandardCharsets;
import java.nio.file.*;
import java.util.*;
import java.util.function.Consumer;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import java.util.zip.ZipFile;

/**
* <p>
* This class provides the basic functionality to load something in KeY. The loading process is done
Expand Down Expand Up @@ -196,7 +198,7 @@ public boolean hasErrors() {
// format: (expected, found)
mismatchErrors = new HashMap<>();
mismatchErrors.put(new Pair<>(KeYLexer.SEMI, KeYLexer.COMMA),
"there may be only one declaration per line");
"there may be only one declaration per line");

missedErrors = new HashMap<>();
missedErrors.put(KeYLexer.RPAREN, "closing parenthesis");
Expand All @@ -222,19 +224,19 @@ public boolean hasErrors() {
* the loaded {@link InitConfig}.
*/
public AbstractProblemLoader(File file, List<File> classPath, File bootClassPath,
List<File> includes, Profile profileOfNewProofs, boolean forceNewProfileOfNewProofs,
ProblemLoaderControl control,
boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile,
Properties poPropertiesToForce) {
List<File> includes, Profile profileOfNewProofs, boolean forceNewProfileOfNewProofs,
ProblemLoaderControl control,
boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile,
Properties poPropertiesToForce) {
this.file = file;
this.classPath = classPath;
this.bootClassPath = bootClassPath;
this.control = control;
this.profileOfNewProofs =
profileOfNewProofs != null ? profileOfNewProofs : AbstractProfile.getDefaultProfile();
profileOfNewProofs != null ? profileOfNewProofs : AbstractProfile.getDefaultProfile();
this.forceNewProfileOfNewProofs = forceNewProfileOfNewProofs;
this.askUiToSelectAProofObligationIfNotDefinedByLoadedFile =
askUiToSelectAProofObligationIfNotDefinedByLoadedFile;
askUiToSelectAProofObligationIfNotDefinedByLoadedFile;
this.poPropertiesToForce = poPropertiesToForce;
this.includes = includes;
}
Expand Down Expand Up @@ -308,14 +310,14 @@ protected void loadEnvironment() throws ProofInputException, IOException {
LOGGER.info("Loading environment from " + file);
envInput = createEnvInput(fileRepo);
LOGGER.debug(
"Environment load took " + PerfScope.formatTime(System.nanoTime() - timeBeforeEnv));
"Environment load took " + PerfScope.formatTime(System.nanoTime() - timeBeforeEnv));
problemInitializer = createProblemInitializer(fileRepo);
var beforeInitConfig = System.nanoTime();
LOGGER.info("Creating init config");
initConfig = createInitConfig();
initConfig.setFileRepo(fileRepo);
LOGGER.debug(
"Init config took " + PerfScope.formatTime(System.nanoTime() - beforeInitConfig));
"Init config took " + PerfScope.formatTime(System.nanoTime() - beforeInitConfig));
if (!problemInitializer.getWarnings().isEmpty() && !ignoreWarnings) {
control.reportWarnings(problemInitializer.getWarnings());
}
Expand Down Expand Up @@ -343,7 +345,7 @@ protected void selectAndLoadProof(ProblemLoaderControl control, InitConfig initC
* @see AbstractProblemLoader#load()
*/
protected void loadSelectedProof(LoadedPOContainer poContainer, ProofAggregate proofList,
Consumer<Proof> callbackProofLoaded)
Consumer<Proof> callbackProofLoaded)
throws ProofInputException, ProblemLoaderException {
// try to replay first proof
proof = proofList.getProof(poContainer.getProofNum());
Expand Down Expand Up @@ -381,23 +383,23 @@ protected ProblemLoaderException recoverParserErrorMessage(Exception e) {
if (c0 instanceof org.antlr.runtime.MismatchedTokenException) {
if (c0 instanceof org.antlr.runtime.MissingTokenException) {
final org.antlr.runtime.MissingTokenException mte =
(org.antlr.runtime.MissingTokenException) c0;
(org.antlr.runtime.MissingTokenException) c0;
// TODO: other commonly missed tokens
final String readable = missedErrors.get(mte.expecting);
final String token = readable == null ? "token id " + mte.expecting : readable;
final String msg = "Syntax error: missing " + token
+ (occurrence == null ? "" : " at " + occurrence.getText()) + " statement ("
+ mte.input.getSourceName() + ":" + mte.line + ")";
+ (occurrence == null ? "" : " at " + occurrence.getText()) + " statement ("
+ mte.input.getSourceName() + ":" + mte.line + ")";
return new ProblemLoaderException(this, msg, mte);
// TODO other ANTLR exceptions
} else {
final org.antlr.runtime.MismatchedTokenException mte =
(MismatchedTokenException) c0;
(MismatchedTokenException) c0;
final String genericMsg = "expected " + mte.expecting + ", but found " + mte.c;
final String readable =
mismatchErrors.get(new Pair<>(mte.expecting, mte.c));
mismatchErrors.get(new Pair<>(mte.expecting, mte.c));
final String msg = "Syntax error: " + (readable == null ? genericMsg : readable)
+ " (" + mte.input.getSourceName() + ":" + mte.line + ")";
+ " (" + mte.input.getSourceName() + ":" + mte.line + ")";
return new ProblemLoaderException(this, msg, mte);
}
}
Expand Down Expand Up @@ -446,7 +448,7 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException {
ret = new SLEnvInput(".", classPath, bootClassPath, profileOfNewProofs, includes);
} else {
ret = new SLEnvInput(file.getParentFile().getAbsolutePath(), classPath,
bootClassPath, profileOfNewProofs, includes);
bootClassPath, profileOfNewProofs, includes);
}
ret.setJavaFile(file.getAbsolutePath());
ret.setIgnoreOtherJavaFiles(loadSingleJavaFile);
Expand Down Expand Up @@ -506,26 +508,26 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException {
Path unzippedProof = tmpDir.resolve(proofFilename.toPath());

return new KeYUserProblemFile(unzippedProof.toString(), unzippedProof.toFile(),
fileRepo, control, profileOfNewProofs, false);
fileRepo, control, profileOfNewProofs, false);
} else if (filename.endsWith(".key") || filename.endsWith(".proof")
|| filename.endsWith(".proof.gz")) {
// KeY problem specification or saved proof
return new KeYUserProblemFile(filename, file, fileRepo, control, profileOfNewProofs,
filename.endsWith(".proof.gz"));
filename.endsWith(".proof.gz"));
} else if (file.isDirectory()) {
// directory containing java sources, probably enriched
// by specifications
return new SLEnvInput(file.getPath(), classPath, bootClassPath, profileOfNewProofs,
includes);
includes);
} else {
if (filename.lastIndexOf('.') != -1) {
throw new IllegalArgumentException("Unsupported file extension '"
+ filename.substring(filename.lastIndexOf('.')) + "' of read-in file "
+ filename + ". Allowed extensions are: .key, .proof, .java or "
+ "complete directories.");
+ filename.substring(filename.lastIndexOf('.')) + "' of read-in file "
+ filename + ". Allowed extensions are: .key, .proof, .java or "
+ "complete directories.");
} else {
throw new FileNotFoundException(
"File or directory\n\t " + filename + "\n not found.");
"File or directory\n\t " + filename + "\n not found.");
}
}
}
Expand Down Expand Up @@ -602,29 +604,29 @@ protected LoadedPOContainer createProofObligationContainer() throws IOException
// Load proof obligation settings
final Properties properties = new Properties();
properties.load(
new ByteArrayInputStream(proofObligation.getBytes(StandardCharsets.UTF_8)));
new ByteArrayInputStream(proofObligation.getBytes(StandardCharsets.UTF_8)));
properties.setProperty(IPersistablePO.PROPERTY_FILENAME, file.getAbsolutePath());
if (poPropertiesToForce != null) {
properties.putAll(poPropertiesToForce);
}
String poClass = properties.getProperty(IPersistablePO.PROPERTY_CLASS);
if (poClass == null || poClass.isEmpty()) {
throw new IOException("Proof obligation class property \""
+ IPersistablePO.PROPERTY_CLASS + "\" is not defiend or empty.");
+ IPersistablePO.PROPERTY_CLASS + "\" is not defiend or empty.");
}
try {
// Try to instantiate proof obligation by calling static method: public static
// LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) throws
// IOException
Class<?> poClassInstance = ClassLoaderUtil.getClassforName(poClass);
Method loadMethod =
poClassInstance.getMethod("loadFrom", InitConfig.class, Properties.class);
poClassInstance.getMethod("loadFrom", InitConfig.class, Properties.class);
return (LoadedPOContainer) loadMethod.invoke(null, initConfig, properties);
} catch (NoSuchMethodException | IllegalAccessException | IllegalArgumentException
| ClassNotFoundException e) {
| ClassNotFoundException e) {
throw new IOException(
"Can't call static factory method \"loadFrom\" on class \"" + poClass + "\".",
e);
"Can't call static factory method \"loadFrom\" on class \"" + poClass + "\".",
e);
} catch (InvocationTargetException e) {
// Try to unwrap the inner exception as good as possible
if (e.getCause() instanceof IOException) {
Expand Down Expand Up @@ -652,7 +654,7 @@ protected LoadedPOContainer createProofObligationContainer() throws IOException
protected ProofAggregate createProof(LoadedPOContainer poContainer) throws ProofInputException {

ProofAggregate proofList =
problemInitializer.startProver(initConfig, poContainer.getProofOblInput());
problemInitializer.startProver(initConfig, poContainer.getProofOblInput());

for (Proof p : proofList.getProofs()) {
// register proof
Expand Down Expand Up @@ -707,7 +709,7 @@ private ReplayResult replayProof(Proof proof) {
assert envInput instanceof KeYUserProblemFile;

IntermediatePresentationProofFileParser parser =
new IntermediatePresentationProofFileParser(proof);
new IntermediatePresentationProofFileParser(proof);
problemInitializer.tryReadProof(parser, (KeYUserProblemFile) envInput);
parserResult = parser.getResult();

Expand All @@ -718,14 +720,14 @@ private ReplayResult replayProof(Proof proof) {
// able to load proofs that used it even if the user has currently
// turned OSS off.
StrategyProperties newProps =
proof.getSettings().getStrategySettings().getActiveStrategyProperties();
proof.getSettings().getStrategySettings().getActiveStrategyProperties();
newProps.setProperty(StrategyProperties.OSS_OPTIONS_KEY, StrategyProperties.OSS_ON);
Strategy.updateStrategySettings(proof, newProps);
OneStepSimplifier.refreshOSS(proof);

replayer = new IntermediateProofReplayer(this, proof, parserResult);
replayResult =
replayer.replay(problemInitializer.getListener(), problemInitializer.getProgMon());
replayer.replay(problemInitializer.getListener(), problemInitializer.getProgMon());

lastTouchedNode = replayResult.getLastSelectedGoal() != null
? replayResult.getLastSelectedGoal().node()
Expand All @@ -746,13 +748,13 @@ private ReplayResult replayProof(Proof proof) {
}
status += (status.isEmpty() ? "Proof replayed successfully." : "\n\n")
+ (replayResult != null ? replayResult.getStatus()
: "Error while loading proof.");
: "Error while loading proof.");
if (replayResult != null) {
errors.addAll(replayResult.getErrors());
}

StrategyProperties newProps =
proof.getSettings().getStrategySettings().getActiveStrategyProperties();
proof.getSettings().getStrategySettings().getActiveStrategyProperties();
newProps.setProperty(StrategyProperties.OSS_OPTIONS_KEY, ossStatus);
Strategy.updateStrategySettings(proof, newProps);
OneStepSimplifier.refreshOSS(proof);
Expand Down
Loading

0 comments on commit 4545251

Please sign in to comment.