From e679a17a19a93a7dc2cc3465910e056e88657e69 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 7 Feb 2026 01:51:15 +0100 Subject: [PATCH] compute a proper problem header including also the taclets --- .../uka/ilkd/key/proof/init/AbstractPO.java | 7 ++-- .../uka/ilkd/key/proof/init/InitConfig.java | 12 +++++++ .../key/proof/init/KeYUserProblemFile.java | 6 ++++ .../key/proof/init/ProblemInitializer.java | 5 +++ .../key/proof/io/OutputStreamProofSaver.java | 33 ++++++++++++------- 5 files changed, 46 insertions(+), 17 deletions(-) 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 3f2ef79bbe..1f766c2fcc 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 @@ -378,9 +378,7 @@ public final String name() { /** * Creates declarations necessary to save/load proof in textual form (helper for createProof()). */ - private void createProofHeader( - JavaModel model, Services services) { - + private void createProofHeader(JavaModel model, Services services) { if (header != null) { return; } @@ -418,8 +416,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); 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 50f39d98e6..969c6ef6e9 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 @@ -34,6 +34,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 +80,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 @Nullable String header; // ------------------------------------------------------------------------- @@ -437,6 +440,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 +470,12 @@ public void activateChoice(Choice choice) { .collect(ImmutableSet.collector()) .add(choice)); } + + public @Nullable String getProblemHeader() { + return header; + } + + public void setHeader(@Nullable String 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 7e9e1fe64b..f286612132 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 @@ -254,6 +254,12 @@ private Profile readProfileFromFile() { } } + + /// + public @Nullable String 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 1b7b6fa1ed..a8745e4c9f 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/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 82628ed7db..aa77b050d7 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 @@ -21,6 +21,7 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.IPersistablePO; +import de.uka.ilkd.key.proof.init.KeYUserProblemFile; import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.proof.init.ProofOblInput; import de.uka.ilkd.key.proof.io.IProofFileParser.ProofElementID; @@ -230,18 +231,26 @@ public void save(OutputStream out) throws IOException { } } - /** - * 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) { + /// 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(@Nullable String header) { + if (header == null) { + return ""; + } final String[] search = { "\\javaSource", "\\bootclasspath", "\\classpath", "\\include" }; final String basePath;