diff --git a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/AbstractInfFlowPO.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/AbstractInfFlowPO.java index 85b9c77e7cb..57c914f3538 100644 --- a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/AbstractInfFlowPO.java +++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/AbstractInfFlowPO.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.informationflow.proof.InfFlowCheckInfo; import de.uka.ilkd.key.informationflow.proof.InfFlowProof; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.StrategyInfoUndoMethod; import de.uka.ilkd.key.proof.init.AbstractOperationPO; @@ -18,6 +19,7 @@ import org.key_project.prover.sequent.SequentFormula; +import org.jspecify.annotations.Nullable; import org.slf4j.LoggerFactory; import static de.uka.ilkd.key.informationflow.proof.InfFlowCheckInfo.INF_FLOW_CHECK_TRUE; @@ -45,7 +47,8 @@ public Proof createProof(String proofName, JTerm poTerm, InitConfig proofConfig) } @Override - public InfFlowProof createProofObject(String proofName, String proofHeader, JTerm poTerm, + public InfFlowProof createProofObject(String proofName, + KeyAst.@Nullable Declarations proofHeader, JTerm poTerm, InitConfig proofConfig) { final InfFlowProof proof = new InfFlowProof(proofName, poTerm, proofHeader, proofConfig); diff --git a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/proof/InfFlowProof.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/proof/InfFlowProof.java index b9f9452daac..d4860ff489b 100644 --- a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/proof/InfFlowProof.java +++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/proof/InfFlowProof.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.informationflow.po.InfFlowProofSymbols; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.BuiltInRuleIndex; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Statistics; @@ -20,6 +21,8 @@ import org.key_project.prover.sequent.SequentFormula; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; + /** * The proof object used by Information Flow Proofs. * @@ -39,12 +42,14 @@ public class InfFlowProof extends Proof { */ private SideProofStatistics sideProofStatistics = null; - public InfFlowProof(String name, Sequent sequent, String header, TacletIndex rules, + public InfFlowProof(String name, Sequent sequent, KeyAst.@Nullable Declarations header, + TacletIndex rules, BuiltInRuleIndex builtInRules, InitConfig initConfig) { super(name, sequent, header, rules, builtInRules, initConfig); } - public InfFlowProof(String name, JTerm problem, String header, InitConfig initConfig) { + public InfFlowProof(String name, JTerm problem, KeyAst.@Nullable Declarations header, + InitConfig initConfig) { super(name, problem, header, initConfig); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index e3e50418712..40bf2eb61fb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.nparser; +import java.io.PrintWriter; import java.net.URI; import java.net.URISyntaxException; import java.net.URL; @@ -170,20 +171,9 @@ public ProblemInformation getProblemInformation() { * declarations of sorts, program variables, schema variables, predicates, and more. * See the grammar (KeYParser.g4) for more possible elements. */ - public String getProblemHeader() { + public KeyAst.@Nullable Declarations getProblemHeader() { final KeYParser.DeclsContext decls = ctx.decls(); - if (decls != null && decls.getChildCount() > 0) { - final Token start = decls.start; - final Token stop = decls.stop; - if (start != null && stop != null) { - int a = start.getStartIndex(); - int b = stop.getStopIndex(); - Interval interval = new Interval(a, b); - CharStream input = ctx.start.getInputStream(); - return input.getText(interval); - } - } - return ""; + return new KeyAst.Declarations(decls); } } @@ -319,4 +309,136 @@ private static List asAst(URI file, return new ScriptCommandAst(it.cmd.getText(), nargs, pargs, loc); } } + + /// Represents the user declarations in a KeY file. + /// + /// @author weigl + public static class Declarations extends KeyAst { + protected Declarations(KeYParser.DeclsContext ctx) { + super(ctx); + } + + public java.io.@Nullable File getJavaSourceLocation() { + try { + KeYParser.String_valueContext value = + ctx.javaSource(0).oneJavaSource().string_value(0); + String v = ParsingFacade.getValueDocumentation(value); + return new java.io.File(v); + } catch (NullPointerException | IndexOutOfBoundsException e) { + { + return null; + } + } + } + + /// Prints the definitions, independent of paths, to the given {@link PrintWriter}. + public void printDefinitions(PrintWriter out) { + ctx.accept(new KeYParserBaseVisitor<@Nullable Object>() { + @Override + public @Nullable Object visitOne_include(KeYParser.One_includeContext ctx) { + if (ctx.absfile != null) { + out.printf("\\include %s;", ctx.absfile.getText()); + } + return null; + } + + @Override + public @Nullable Object visitOptions_choice(KeYParser.Options_choiceContext ctx) { + printAsIs(ctx); + return null; + } + + @Override + public @Nullable Object visitOption_decls(KeYParser.Option_declsContext ctx) { + printAsIs(ctx); + return null; + } + + @Override + public @Nullable Object visitSort_decls(KeYParser.Sort_declsContext ctx) { + printAsIs(ctx); + return null; + } + + @Override + public @Nullable Object visitProg_var_decls(KeYParser.Prog_var_declsContext ctx) { + printAsIs(ctx); + return null; + } + + @Override + public @Nullable Object visitSchema_var_decls( + KeYParser.Schema_var_declsContext ctx) { + printAsIs(ctx); + return null; + } + + @Override + public @Nullable Object visitPred_decls(KeYParser.Pred_declsContext ctx) { + printAsIs(ctx); + return null; + } + + @Override + public @Nullable Object visitFunc_decls(KeYParser.Func_declsContext ctx) { + printAsIs(ctx); + return null; + } + + @Override + public @Nullable Object visitTransform_decls(KeYParser.Transform_declsContext ctx) { + printAsIs(ctx); + return null; + } + + @Override + public @Nullable Object visitDatatype_decls(KeYParser.Datatype_declsContext ctx) { + printAsIs(ctx); + return null; + } + + + @Override + public @Nullable Object visitRuleset_decls(KeYParser.Ruleset_declsContext ctx) { + printAsIs(ctx); + return null; + } + + + @Override + public @Nullable Object visitContracts(KeYParser.ContractsContext ctx) { + printAsIs(ctx); + return null; + } + + @Override + public @Nullable Object visitInvariants(KeYParser.InvariantsContext ctx) { + printAsIs(ctx); + return null; + } + + @Override + public @Nullable Object visitRulesOrAxioms(KeYParser.RulesOrAxiomsContext ctx) { + printAsIs(ctx); + return null; + } + + private void printAsIs(ParserRuleContext ctx) { + if (ctx != null) { + final Token start = ctx.start; + final Token stop = ctx.stop; + if (start != null && stop != null) { + int a = start.getStartIndex(); + int b = stop.getStopIndex(); + Interval interval = new Interval(a, b); + CharStream input = ctx.start.getInputStream(); + out.println(input.getText(interval)); + } + } + } + }); + + + } + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java index a6f5cab1498..cac1b3a60c4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java @@ -15,6 +15,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.NamespaceSet; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.pp.AbbrevMap; import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit; import de.uka.ilkd.key.proof.event.ProofDisposedEvent; @@ -43,7 +44,6 @@ import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.lookup.Lookup; -import org.jspecify.annotations.NonNull; import org.jspecify.annotations.NullMarked; import org.jspecify.annotations.Nullable; @@ -96,7 +96,7 @@ public class Proof implements ProofObject, Named { /** * declarations &c, read from a problem file or otherwise */ - private String problemHeader = ""; + private KeyAst.@Nullable Declarations problemHeader = null; /** * the proof environment (optional) @@ -136,7 +136,7 @@ public class Proof implements ProofObject, Named { private long autoModeTime = 0; - private @Nullable Strategy<@NonNull Goal> activeStrategy; + private @Nullable Strategy activeStrategy; private PropertyChangeListener settingsListener; @@ -238,7 +238,8 @@ private Proof(String name, Sequent problem, TacletIndex rules, BuiltInRuleIndex } } - public Proof(String name, Sequent problem, String header, InitConfig initConfig, + public Proof(String name, Sequent problem, KeyAst.@Nullable Declarations header, + InitConfig initConfig, Path proofFile) { this(name, problem, initConfig.createTacletIndex(), initConfig.createBuiltInRuleIndex(), initConfig); @@ -246,7 +247,8 @@ public Proof(String name, Sequent problem, String header, InitConfig initConfig, this.proofFile = proofFile; } - public Proof(String name, JTerm problem, String header, InitConfig initConfig) { + public Proof(String name, JTerm problem, KeyAst.@Nullable Declarations header, + InitConfig initConfig) { this(name, JavaDLSequentKit .createSuccSequent(ImmutableSLList.singleton(new SequentFormula(problem))), @@ -255,7 +257,8 @@ public Proof(String name, JTerm problem, String header, InitConfig initConfig) { } - public Proof(String name, Sequent sequent, String header, TacletIndex rules, + public Proof(String name, Sequent sequent, KeyAst.@Nullable Declarations header, + TacletIndex rules, BuiltInRuleIndex builtInRules, InitConfig initConfig) { this(name, sequent, rules, builtInRules, initConfig); problemHeader = header; @@ -325,7 +328,7 @@ public Name name() { } - public String header() { + public KeyAst.@Nullable Declarations header() { return problemHeader; } @@ -389,7 +392,7 @@ public AbbrevMap abbreviations() { } - public Strategy<@NonNull Goal> getActiveStrategy() { + public Strategy getActiveStrategy() { if (activeStrategy == null) { initStrategy(); } @@ -397,7 +400,7 @@ public AbbrevMap abbreviations() { } - public void setActiveStrategy(Strategy<@NonNull Goal> activeStrategy) { + public void setActiveStrategy(Strategy activeStrategy) { this.activeStrategy = activeStrategy; getSettings().getStrategySettings().setStrategy(activeStrategy.name()); updateStrategyOnGoals(); @@ -409,7 +412,7 @@ public void setActiveStrategy(Strategy<@NonNull Goal> activeStrategy) { private void updateStrategyOnGoals() { - Strategy<@NonNull Goal> ourStrategy = getActiveStrategy(); + Strategy ourStrategy = getActiveStrategy(); for (Goal goal : openGoals()) { goal.setGoalStrategy(ourStrategy); @@ -776,7 +779,7 @@ public void breadthFirstSearch(Node startNode, ProofVisitor visitor) { * @param pred non-null test function * @return a node fulfilling {@code pred} or null */ - public @Nullable Node findAny(@NonNull Predicate pred) { + public @Nullable Node findAny(Predicate pred) { Queue queue = new LinkedList<>(); queue.add(root); while (!queue.isEmpty()) { @@ -974,7 +977,7 @@ public boolean isOpenGoal(Node node) { * * @return the goal that belongs to the given node or null if the node is an inner one */ - public Goal getOpenGoal(@NonNull Node node) { + public Goal getOpenGoal(Node node) { for (final Goal result : openGoals) { if (result.node() == node) { return result; @@ -1317,7 +1320,7 @@ public void deregister(T obj, Class service) { * * @return the associated lookup */ - public @NonNull Lookup getUserData() { + public Lookup getUserData() { if (userData == null) { userData = new Lookup(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java index 3f2ef79bbeb..db13b909088 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java @@ -13,7 +13,7 @@ import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.op.*; -import de.uka.ilkd.key.proof.JavaModel; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; import de.uka.ilkd.key.proof.mgt.AxiomJustification; @@ -48,7 +48,7 @@ public abstract class AbstractPO implements IPersistablePO { protected ImmutableSet taclets; protected JTerm[] poTerms; protected String[] poNames; - private String header; + private KeyAst.Declarations header; private ProofAggregate proofAggregate; @@ -375,37 +375,6 @@ public final String name() { } - /** - * Creates declarations necessary to save/load proof in textual form (helper for createProof()). - */ - private void createProofHeader( - JavaModel model, Services services) { - - if (header != null) { - return; - } - - final StringBuilder sb = new StringBuilder(model.asKeyString()); - - // contracts - ImmutableSet contractsToSave = specRepos.getAllContracts(); - for (Contract c : contractsToSave) { - if (!c.toBeSaved()) { - contractsToSave = contractsToSave.remove(c); - } - } - if (!contractsToSave.isEmpty()) { - sb.append("\\contracts {\n"); - for (Contract c : contractsToSave) { - sb.append(c.proofToString(services)); - } - sb.append("}\n\n"); - } - - header = sb.toString(); - } - - /** * Creates a Proof (helper for getPO()). * @@ -418,8 +387,7 @@ protected Proof createProof(String proofName, JTerm poTerm, InitConfig proofConf if (proofConfig == null) { proofConfig = environmentConfig.deepCopy(); } - final JavaModel javaModel = proofConfig.getServices().getJavaModel(); - createProofHeader(javaModel, proofConfig.getServices()); + header = proofConfig.getProblemHeader(); final Proof proof = createProofObject(proofName, header, poTerm, proofConfig); @@ -428,7 +396,9 @@ protected Proof createProof(String proofName, JTerm poTerm, InitConfig proofConf } - protected Proof createProofObject(String proofName, String proofHeader, JTerm poTerm, + + protected Proof createProofObject(String proofName, KeyAst.Declarations proofHeader, + JTerm poTerm, InitConfig proofConfig) { return new Proof(proofName, poTerm, proofHeader, proofConfig); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java index 50f39d98e64..ec3f7b51f8b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.NamespaceSet; import de.uka.ilkd.key.logic.op.IProgramVariable; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.BuiltInRuleIndex; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.TacletIndex; @@ -34,6 +35,7 @@ import org.key_project.util.collection.ImmutableSet; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** * an instance of this class describes the initial configuration of the prover. This includes sorts, @@ -79,10 +81,12 @@ public class InitConfig { /** the fileRepo which is responsible for consistency between source code and proof */ private FileRepo fileRepo; + // weigl this field is never set private String originalKeYFileName; private ProofSettings settings; + private KeyAst.@Nullable Declarations header; // ------------------------------------------------------------------------- @@ -437,6 +441,7 @@ public InitConfig copyWithServices(Services services) { (HashMap>) taclet2Builder.clone()); ic.taclets = taclets; ic.originalKeYFileName = originalKeYFileName; + ic.header = header; ic.justifInfo = justifInfo.copy(); ic.fileRepo = fileRepo; // TODO: copy instead? delete via dispose method? return ic; @@ -466,4 +471,12 @@ public void activateChoice(Choice choice) { .collect(ImmutableSet.collector()) .add(choice)); } + + public KeyAst.@Nullable Declarations getProblemHeader() { + return header; + } + + public void setHeader(KeyAst.@Nullable Declarations header) { + this.header = header; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java index 7e9e1fe64b9..98e3c516394 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java @@ -158,7 +158,7 @@ public ProofAggregate getPO() { ProofSettings settings = getPreferences(); initConfig.setSettings(settings); return ProofAggregate.createProofAggregate( - new Proof(name, problem, getParseContext().getProblemHeader() + "\n", initConfig, + new Proof(name, problem, getParseContext().getProblemHeader(), initConfig, file.file()), name); } @@ -254,6 +254,12 @@ private Profile readProfileFromFile() { } } + + /// + public KeyAst.@Nullable Declarations getProblemHeader() { + return getParseContext().getProblemHeader(); + } + /** * Returns the default {@link Profile} which was defined by a constructor. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index 1b7b6fa1ed0..a8745e4c9fa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java @@ -459,6 +459,11 @@ public InitConfig prepare(EnvInput envInput) throws ProofInputException { if (Debug.ENABLE_DEBUG) { print(ic); } + + if (envInput instanceof KeYUserProblemFile uf) { + ic.setHeader(uf.getProblemHeader()); + } + return ic; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipProofSaver.java index faa12c2d085..8a89c8fe978 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipProofSaver.java @@ -37,7 +37,7 @@ public GZipProofSaver(Proof proof, String fileName, String internalVersion) { @Override protected void save(Path file) throws IOException { try (var out = new GZIPOutputStream(Files.newOutputStream(file))) { - save(out); + save(file.getParent(), out); } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 82628ed7db5..f43fe89647d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.pp.NotationInfo; import de.uka.ilkd.key.pp.PrettyPrinter; @@ -55,11 +56,14 @@ import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentFormula; import org.key_project.util.collection.ImmutableList; +import org.key_project.util.java.IOUtil; import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import static org.key_project.util.java.IOUtil.safePathRelativeTo; + /** * Saves a proof to a given {@link OutputStream}. * @@ -82,26 +86,6 @@ public class OutputStreamProofSaver { protected final boolean saveProofSteps; - /** - * Extracts java source directory from {@link Proof#header()}, if it exists. - * - * @param proof the Proof - * @return the location of the java source code or null if no such exists - */ - public static @Nullable File getJavaSourceLocation(Proof proof) { - final String header = proof.header(); - final int i = header.indexOf("\\javaSource"); - if (i >= 0) { - final int begin = header.indexOf('\"', i); - final int end = header.indexOf('\"', begin + 1); - final String sourceLocation = header.substring(begin + 1, end); - if (!sourceLocation.isEmpty()) { - return new File(sourceLocation); - } - } - return null; - } - public OutputStreamProofSaver(Proof proof) { this(proof, KeYConstants.INTERNAL_VERSION); } @@ -158,7 +142,7 @@ public String writeSettings(ProofSettings ps) { return String.format("\\settings %s \n", ps.settingsToString()); } - public void save(OutputStream out) throws IOException { + public void save(Path basePath, OutputStream out) throws IOException { CopyReferenceResolver.copyCachedGoals(proof, null, null, null); try (var ps = new PrintWriter(out, true, StandardCharsets.UTF_8)) { final ProofOblInput po = @@ -183,11 +167,9 @@ public void save(OutputStream out) throws IOException { ps.println(writeSettings(proof.getSettings())); - // declarations of symbols, sorts - // FIXME this should rather be an AST rewrite, than a bunch of regex. - String header = proof.header(); - header = makePathsRelative(header); - ps.print(header); + var header = proof.header(); + String headerStr = makePathsRelative(basePath, header); + ps.print(headerStr); proof.printSymbols(ps); @@ -221,75 +203,61 @@ public void save(OutputStream out) throws IOException { } } - protected @Nullable Path getBasePath() throws IOException { - File javaSourceLocation = getJavaSourceLocation(proof); - if (javaSourceLocation != null) { - return javaSourceLocation.toPath().toAbsolutePath(); - } else { - return null; + + /// Searches in the header for absolute paths to Java files and tries to replace them by paths + /// relative to the proof file to be saved. + /// If the given `header` is null, an empty string is returned. This is the case for proofs, + /// that are non-KeY-file not crated by KeY-files. + /// + /// @param header a string created a proper KeY-file content. + /// + /// + /// TODO weigl: If someone finds time, this function is a string manipulation mess. + /// You should rather parse the header using the [de.uka.ilkd.key.nparser.ParsingFacade] + /// and use the [de.uka.ilkd.key.nparser.builder.ProblemFinder] to extract the field. + /// Better would be to get rid of the header, and using an AST. + /// + /// + /// @see KeYUserProblemFile#getProblemHeader() + /// @see de.uka.ilkd.key.proof.init.InitConfig#getProblemHeader() + private String makePathsRelative(Path basePath, KeyAst.@Nullable Declarations header) + throws IOException { + if (header == null) { + return ""; } - } + StringWriter sw = new StringWriter(); + PrintWriter out = new PrintWriter(sw, true); - /** - * Searches in the header for absolute paths to Java files and tries to replace them by paths - * relative to the proof file to be saved. - * - * TODO weigl: if someone finds time, this function is a string manipulation mess. - * You should rather parse the header using the {@link de.uka.ilkd.key.nparser.ParsingFacade} - * and - * use the {@link de.uka.ilkd.key.nparser.builder.ProblemFinder} to extract the field. - * - * Better would be to get rid of the header, and using an AST. - */ - private String makePathsRelative(String header) { - final String[] search = - { "\\javaSource", "\\bootclasspath", "\\classpath", "\\include" }; - final String basePath; - String tmp = header; - try { - basePath = getBasePath().toString(); + header.printDefinitions(out); - // locate filenames in header - for (final String s : search) { - int i = tmp.indexOf(s); - if (i == -1) { - continue; // entry not in file - } + var jm = proof.getServices().getJavaModel(); - // put in everything before the keyword - // bugfix #1138: changed i-1 to i - String tmp2 = tmp.substring(0, i); - StringBuilder relPathString = new StringBuilder(); - i += s.length(); - final int l = tmp.indexOf(';', i); - - // there may be more than one path - while (0 <= tmp.indexOf('"', i) && tmp.indexOf('"', i) < l) { - if (!relPathString.isEmpty()) { - relPathString.append(", "); - } - - // path is always put in quotation marks - final int k = tmp.indexOf('"', i) + 1; - final int j = tmp.indexOf('"', k); - - // add new relative path - final String absPath = tmp.substring(k, j); - final String relPath = tryToMakeFilenameRelative(absPath, basePath); - final String correctedRelPath = relPath.isEmpty() ? "." : relPath; - relPathString.append(" \"").append(escapeCharacters(correctedRelPath)) - .append("\""); - i = j + 1; - } - tmp2 = tmp2 + s + relPathString + ";"; + var bootClassPath = jm.getBootClassPath(); + if (bootClassPath != null) { + out.printf("\\bootclasspath \"%s\";\n", IOUtil.safePath(bootClassPath)); + } - // put back in the rest - tmp = tmp2 + (i < tmp.length() ? tmp.substring(l + 1) : ""); + var classPath = jm.getClassPath(); + if (classPath != null && !classPath.isEmpty()) { + for (Path path : classPath) { + out.printf("\\classpath \"%s\";\\n", safePathRelativeTo(path, basePath)); } - } catch (final IOException e) { - LOGGER.warn("Failed to make relative", e); } - return tmp; + + var javaSource = jm.getModelDir(); + if (javaSource != null) { + out.printf("\\javaSource \"%s\";\n", safePathRelativeTo(javaSource, basePath)); + } + + var includedFiles = jm.getIncludedFiles(); + if (includedFiles != null && !includedFiles.isEmpty()) { + for (var includedFile : includedFiles) { + out.printf("\\include \"%s\";\n", + safePathRelativeTo(includedFile, basePath)); + } + } + + return sw.toString(); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java index a40390cd13c..b9a54002dae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java @@ -54,7 +54,8 @@ protected void save(Path file) throws IOException { String proofFileName = MiscTools.toValidFileName(proof.name() + ".proof"); // save the proof file to the FileRepo (stream is closed by the save method!) - save(repo.createOutputStream(Paths.get(proofFileName))); + final var path = Paths.get(proofFileName); + save(path.toAbsolutePath().getParent(), repo.createOutputStream(path)); // save proof bundle with the help of the FileRepo ((AbstractFileRepo) repo).saveProof(file); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java index 48148ff405a..8017ee41a75 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java @@ -117,7 +117,7 @@ public ProofSaver(Proof proof, Path file, String internalVersion, boolean savePr */ protected void save(Path file) throws IOException { try (var out = Files.newOutputStream(file)) { - save(out); + save(file.getParent(), out); } } @@ -141,23 +141,6 @@ public String save() { return errorMsg; } - @Override - protected Path getBasePath() throws IOException { - return computeBasePath(file); - } - - /** - * Computes the base path of the given proof {@link File}. - *

- * This method is used by {@link #getBasePath()} and by the Eclipse integration. - * - * @param proofFile The proof {@link File}. - * @return The computed base path of the given proof {@link File}. - */ - public static Path computeBasePath(Path proofFile) { - return proofFile.toAbsolutePath().getParent().toAbsolutePath(); - } - /** * Adds the {@link ProofSaverListener}. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/ProofObligationCreator.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/ProofObligationCreator.java index fbf9c9bdc71..18b3f49e530 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/ProofObligationCreator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/ProofObligationCreator.java @@ -148,7 +148,7 @@ private ProofAggregate create(Taclet taclet, InitConfig initConfig, // (MU 2013-08) // String header = userDefinedSymbols.createHeader(initConfig.getServices()); - Proof proof = new Proof(name, formula, "" /* header */, initConfig); + Proof proof = new Proof(name, formula, null, initConfig); userDefinedSymbols.addSymbolsToNamespaces(proof.getNamespaces()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/ProofStarter.java b/key.core/src/main/java/de/uka/ilkd/key/util/ProofStarter.java index aa5bcaa2884..f7a790838b5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/ProofStarter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/ProofStarter.java @@ -5,6 +5,7 @@ import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; @@ -50,7 +51,7 @@ public class ProofStarter { */ public static class UserProvidedInput implements ProofOblInput { - private static final String EMPTY_PROOF_HEADER = ""; + private static final KeyAst.@Nullable Declarations EMPTY_PROOF_HEADER = null; private final ProofEnvironment env; private final Sequent seq; private final String proofName; diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestLocalSymbols.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestLocalSymbols.java index 68e6f162503..b67ec93f1ab 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestLocalSymbols.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestLocalSymbols.java @@ -91,7 +91,7 @@ public void testSkolemization() throws Exception { .parseTerm("((\\forall s varr; varr=const) | (\\forall s varr; const=varr)) & " + "((\\forall s varr; varr=const) | (\\forall s varr; const=varr))"); - Proof proof = new Proof("TestLocalSymbols", target, "n/a", TacletForTests.initConfig()); + Proof proof = new Proof("TestLocalSymbols", target, null, TacletForTests.initConfig()); apply(proof, andRight, 0, 1); apply(proof, orRight, 0, 1); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/TestGoal.java b/key.core/src/test/java/de/uka/ilkd/key/proof/TestGoal.java index 507a4ec3ada..80e511d0629 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/TestGoal.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/TestGoal.java @@ -49,7 +49,7 @@ public void testSetBack0() { final InitConfig initConfig = new InitConfig(new Services(AbstractProfile.getDefaultProfile())); - proof = new Proof("", seq, "", initConfig.createTacletIndex(), + proof = new Proof("", seq, null, initConfig.createTacletIndex(), initConfig.createBuiltInRuleIndex(), initConfig); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java index b3413b681b4..263baa31f4b 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java @@ -30,7 +30,7 @@ void testSaveProblemToFile(String content) throws IOException { Sequent seq = loader.parseFile().loadProblem().getProblem(); final InitConfig initConfig = new InitConfig(new Services(AbstractProfile.getDefaultProfile())); - Proof proof = new Proof("test", seq, "", initConfig, null); + Proof proof = new Proof("test", seq, null, initConfig, null); Path file = Files.createTempFile("proofSaveTest", ".key"); String status = new ProofSaver(proof, file).save(); assertNull(status); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java index 8ddaa942b20..26e7616c76a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java @@ -11,6 +11,7 @@ import java.nio.charset.Charset; import java.nio.charset.StandardCharsets; import java.nio.file.Files; +import java.nio.file.Paths; import java.util.LinkedList; import java.util.List; import java.util.zip.ZipEntry; @@ -23,6 +24,7 @@ import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; @@ -35,6 +37,7 @@ import org.key_project.util.Streams; import org.key_project.util.java.IOUtil; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -69,6 +72,19 @@ private static String serializeStackTrace(Throwable t) { return sw.toString(); } + /** + * Extracts java source directory from {@link Proof#header()}, if it exists. + * + * @param proof the Proof + * @return the location of the java source code or null if no such exists + */ + public static @Nullable File getJavaSourceLocation(Proof proof) { + KeyAst.@Nullable Declarations header = proof.header(); + if (header == null) + return null; + return header.getJavaSourceLocation(); + } + private static abstract class SendFeedbackItem implements ActionListener { final String displayName; @@ -213,7 +229,7 @@ byte[] retrieveFileData() throws IOException { Proof proof = mediator.getSelectedProof(); OutputStreamProofSaver saver = new OutputStreamProofSaver(proof); ByteArrayOutputStream stream = new ByteArrayOutputStream(); - saver.save(stream); + saver.save(Paths.get(".").toAbsolutePath(), stream); return stream.toByteArray(); } @@ -302,7 +318,7 @@ public JavaSourceItem() { boolean isEnabled() { try { Proof proof = MainWindow.getInstance().getMediator().getSelectedProof(); - File javaSourceLocation = OutputStreamProofSaver.getJavaSourceLocation(proof); + File javaSourceLocation = getJavaSourceLocation(proof); return javaSourceLocation != null; } catch (Exception e) { return false; @@ -322,7 +338,7 @@ private void getJavaFilesRecursively(File directory, List list) { @Override void appendDataToZipOutputStream(ZipOutputStream stream) throws IOException { Proof proof = MainWindow.getInstance().getMediator().getSelectedProof(); - File javaSourceLocation = OutputStreamProofSaver.getJavaSourceLocation(proof); + File javaSourceLocation = getJavaSourceLocation(proof); List javaFiles = new LinkedList<>(); getJavaFilesRecursively(javaSourceLocation, javaFiles); for (File f : javaFiles) { diff --git a/key.util/src/main/java/org/key_project/util/java/IOUtil.java b/key.util/src/main/java/org/key_project/util/java/IOUtil.java index 9a4666f7189..aa23a415fa8 100644 --- a/key.util/src/main/java/org/key_project/util/java/IOUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/IOUtil.java @@ -350,6 +350,7 @@ public static LineInformation[] computeLineInformation(InputStream in) } + /** * A line information returned from {@link IOUtil#computeLineInformation(File)} and * {@link IOUtil#computeLineInformation(InputStream)}. @@ -823,4 +824,14 @@ public static String safePath(Path path) { var s = path.toString(); return s.replace('\\', '/'); } + + + /// Returns a string, representing the given path to `source` relatively to `basePath`. + /// @param source a path + /// @param basePath a directory + /// @return a string that is printable (escaped) for KeY files + public static String safePathRelativeTo(Path source, Path basePath) { + var abs = source.toAbsolutePath(); + return safePath(basePath.relativize(abs)); + } } diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java index 8405d27b1c2..7f4be0aebed 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java @@ -140,7 +140,7 @@ protected Proof createProof(UserInterfaceControl ui, Proof oldProof, String newN Sequent newSequent) throws ProofInputException { if (showInMainWindow) { InitConfig initConfig = oldProof.getInitConfig().deepCopy(); - final Proof proof = new Proof(newName, newSequent, "", initConfig.createTacletIndex(), + final Proof proof = new Proof(newName, newSequent, null, initConfig.createTacletIndex(), initConfig.createBuiltInRuleIndex(), initConfig.deepCopy()); proof.setEnv(oldProof.getEnv()); proof.setNamespaces(oldProof.getNamespaces());