Skip to content

Commit 47116c0

Browse files
WolframPfeiferwadoon
WolframPfeifer
authored and
wadoon
committed
fixed report creation
1 parent de7169c commit 47116c0

8 files changed

Lines changed: 74 additions & 133 deletions

File tree

‎keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/CheckerData.java‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,17 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package org.key_project.proofmanagement.check;
55

6+
import java.net.URL;
67
import java.nio.file.Path;
78
import java.time.LocalDateTime;
89
import java.time.format.DateTimeFormatter;
910
import java.util.*;
1011

12+
import de.uka.ilkd.key.proof.Proof;
13+
import de.uka.ilkd.key.proof.init.KeYUserProblemFile;
14+
import de.uka.ilkd.key.proof.init.ProblemInitializer;
15+
import de.uka.ilkd.key.proof.io.AbstractProblemLoader;
16+
import de.uka.ilkd.key.proof.io.IntermediatePresentationProofFileParser;
1117
import de.uka.ilkd.key.settings.ChoiceSettings;
1218
import de.uka.ilkd.key.speclang.Contract;
1319
import de.uka.ilkd.key.speclang.SLEnvInput;
@@ -474,4 +480,34 @@ public void setFileTree(PathNode fileTree) {
474480
public void setDependencyGraph(DependencyGraph dependencyGraph) {
475481
this.dependencyGraph = dependencyGraph;
476482
}
483+
484+
/**
485+
* @author Alexander Weigl
486+
* @version 1 (6/18/25)
487+
*/
488+
public class ProofEntry {
489+
public LoadingState loadingState = LoadingState.UNKNOWN;
490+
public ReplayState replayState = ReplayState.UNKNOWN;
491+
public DependencyState dependencyState = DependencyState.UNKNOWN;
492+
public ProofState proofState = ProofState.UNKNOWN;
493+
494+
public boolean replaySuccess() {
495+
return replayState == ReplayState.SUCCESS;
496+
}
497+
498+
public @Nullable Path proofFile;
499+
public @Nullable KeYUserProblemFile envInput;
500+
public @Nullable ProblemInitializer problemInitializer;
501+
public @Nullable Proof proof;
502+
503+
public @Nullable Contract contract;
504+
public @Nullable URL sourceFile;
505+
public @Nullable String shortSrc;
506+
public IntermediatePresentationProofFileParser.Result parseResult;
507+
public AbstractProblemLoader.ReplayResult replayResult;
508+
509+
public Integer settingsId() {
510+
return choices2Id.get(proof.getSettings().getChoiceSettings().getDefaultChoices());
511+
}
512+
}
477513
}

‎keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/DependencyChecker.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -122,7 +122,7 @@ private boolean hasUnprovenDependencies(DependencyGraph graph, CheckerData data)
122122
changed = false;
123123
for (DependencyNode n : graph.getNodes()) {
124124
if (!closed.contains(n)) {
125-
ProofEntry entry = data.getProofEntryByContract(n.getContract());
125+
CheckerData.ProofEntry entry = data.getProofEntryByContract(n.getContract());
126126
if (entry != null) {
127127
if (entry.proofState == CheckerData.ProofState.CLOSED
128128
&& closed.containsAll(n.getDependencies().keySet())) {
@@ -148,7 +148,7 @@ private boolean hasUnprovenDependencies(DependencyGraph graph, CheckerData data)
148148

149149
// update data: all other (successfully replayed) closed proofs
150150
// have dependencies left unproven
151-
for (ProofEntry entry : data.getProofEntries()) {
151+
for (CheckerData.ProofEntry entry : data.getProofEntries()) {
152152
if (entry.dependencyState == CheckerData.DependencyState.UNKNOWN
153153
&& entry.replayState == CheckerData.ReplayState.SUCCESS) {
154154
entry.dependencyState = CheckerData.DependencyState.UNPROVEN_DEP;
@@ -179,7 +179,7 @@ private boolean hasIllegalCycles(DependencyGraph graph) {
179179

180180
// update all nodes from SCC to illegal cycle state
181181
for (DependencyNode n : scc.getNodes()) {
182-
ProofEntry entry = data.getProofEntryByContract(n.getContract());
182+
CheckerData.ProofEntry entry = data.getProofEntryByContract(n.getContract());
183183
// TODO: entry == null can not happen
184184
// (if node has dependencies it has been parsed,
185185
// thus also a proof entry exists)

‎keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java‎

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,8 @@
3939
import org.key_project.proofmanagement.io.Logger;
4040
import org.key_project.proofmanagement.io.ProofBundleHandler;
4141

42+
import org.key_project.proofmanagement.check.CheckerData.ProofEntry;
43+
4244
/**
4345
* This class provides static methods to access the prover (KeY).
4446
*
@@ -81,7 +83,7 @@ public static void ensureProofsLoaded(CheckerData data) throws ProofManagementEx
8183
// for (Path proofPath : proofPaths) {
8284
while (iterator.hasNext()) {
8385
Path proofPath = iterator.next();
84-
ProofEntry line = ensureProofEntryExists(proofPath, data);
86+
CheckerData.ProofEntry line = ensureProofEntryExists(proofPath, data);
8587
// only load every line once
8688
if (line.loadingState == CheckerData.LoadingState.UNKNOWN) {
8789
if (!loadProofTree(proofPath, line, data)) {
@@ -103,22 +105,22 @@ public static void ensureProofsLoaded(CheckerData data) throws ProofManagementEx
103105
private static ProofEntry ensureProofEntryExists(Path proofPath, CheckerData data) {
104106
ProofEntry line = findProofLine(proofPath, data);
105107
if (line == null) {
106-
line = new ProofEntry();
108+
line = data.new ProofEntry();
107109
data.getProofEntries().add(line);
108110
}
109111
return line;
110112
}
111113

112-
private static ProofEntry findProofLine(Path proofPath, CheckerData data) {
113-
for (ProofEntry line : data.getProofEntries()) {
114+
private static CheckerData.ProofEntry findProofLine(Path proofPath, CheckerData data) {
115+
for (CheckerData.ProofEntry line : data.getProofEntries()) {
114116
if (line.proofFile != null && line.proofFile.equals(proofPath)) {
115117
return line;
116118
}
117119
}
118120
return null;
119121
}
120122

121-
private static boolean loadProofTree(Path path, ProofEntry line, Logger logger)
123+
private static boolean loadProofTree(Path path, CheckerData.ProofEntry line, Logger logger)
122124
throws Exception {
123125

124126
logger.print(LogLevel.DEBUG, "Loading proof from " + path);
@@ -150,7 +152,7 @@ private static boolean loadProofTree(Path path, ProofEntry line, Logger logger)
150152
return true;
151153
}
152154

153-
private static Proof[] loadProofFile(Path path, ProofEntry line)
155+
private static Proof[] loadProofFile(Path path, CheckerData.ProofEntry line)
154156
throws Exception {
155157
Profile profile = AbstractProfile.getDefaultProfile();
156158

@@ -293,7 +295,7 @@ public static void ensureProofsReplayed(CheckerData data) throws ProofManagement
293295
List<Path> proofPaths = data.getProofPaths();
294296
ensureProofsLoaded(data);
295297

296-
for (ProofEntry line : data.getProofEntries()) {
298+
for (CheckerData.ProofEntry line : data.getProofEntries()) {
297299
// skip replay for proofs if not requested
298300
if (proofPaths.contains(line.proofFile)) {
299301
// skip proofs that have already been replayed
@@ -317,8 +319,8 @@ public static void ensureProofsReplayed(CheckerData data) throws ProofManagement
317319
}
318320
}
319321

320-
private static ReplayResult replayProof(ProofEntry line, EnvInput envInput,
321-
Logger logger) throws ProofInputException {
322+
private static ReplayResult replayProof(CheckerData.ProofEntry line, EnvInput envInput,
323+
Logger logger) throws ProofInputException {
322324
Proof proof = line.proof;
323325
logger.print(LogLevel.INFO, "Starting replay of proof " + proof.name());
324326

‎keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/MissingProofsChecker.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ private static void removeContractsWithProof(Set<Contract> contracts, CheckerDat
7272
throws ProofManagementException {
7373

7474
// compare: Is there a proof for every contract?
75-
for (ProofEntry entry : data.getProofEntries()) {
75+
for (CheckerData.ProofEntry entry : data.getProofEntries()) {
7676
Proof p = Objects.requireNonNull(entry.proof);
7777
SpecificationRepository sr = p.getServices().getSpecificationRepository();
7878
ContractPO cpo = sr.getPOForProof(p);

‎keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/ProofEntry.java‎

Lines changed: 0 additions & 106 deletions
This file was deleted.

‎keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313
import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
1414
import de.uka.ilkd.key.speclang.Contract;
1515

16-
import org.key_project.proofmanagement.check.ProofEntry;
16+
import org.key_project.proofmanagement.check.CheckerData;
1717
import org.key_project.proofmanagement.io.Logger;
1818

1919
/**
@@ -29,13 +29,13 @@ public abstract class DependencyGraphBuilder {
2929
* @param logger the logger to print out error messages generated during graph creation
3030
* @return the newly created DependencyGraph
3131
*/
32-
public static DependencyGraph buildGraph(List<ProofEntry> proofEntries,
32+
public static DependencyGraph buildGraph(List<CheckerData.ProofEntry> proofEntries,
3333
Logger logger) {
3434

3535
DependencyGraph graph = new DependencyGraph();
3636

3737
// first create the nodes of the graph (one for each loaded proof)
38-
for (ProofEntry line : proofEntries) {
38+
for (CheckerData.ProofEntry line : proofEntries) {
3939

4040
Proof proof = Objects.requireNonNull(line.proof);
4141
String contractName = proof.name().toString();
@@ -49,7 +49,7 @@ public static DependencyGraph buildGraph(List<ProofEntry> proofEntries,
4949
}
5050

5151
// add dependencies between nodes
52-
for (ProofEntry line : proofEntries) {
52+
for (CheckerData.ProofEntry line : proofEntries) {
5353
// get current node and root of proof
5454
Proof proof = Objects.requireNonNull(line.proof);
5555
DependencyNode currentNode =

‎keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010
import java.util.HashMap;
1111
import java.util.Map;
1212

13+
import freemarker.template.DefaultObjectWrapper;
1314
import org.key_project.proofmanagement.check.CheckerData;
1415
import org.key_project.proofmanagement.check.PathNode;
1516
import org.key_project.util.java.IOUtil;
@@ -43,6 +44,11 @@ public static void print(CheckerData data, Path target) throws IOException {
4344
cfg.setClassLoaderForTemplateLoading(HTMLReport.class.getClassLoader(), "/report/html");
4445
cfg.setDefaultEncoding("UTF-8");
4546

47+
// Use DefaultObjectWrapper to expose fields of objects in the data model
48+
DefaultObjectWrapper wrapper = new DefaultObjectWrapper(Configuration.VERSION_2_3_32);
49+
wrapper.setExposeFields(true);
50+
cfg.setObjectWrapper(wrapper);
51+
4652
// Load template
4753
Template template = cfg.getTemplate("report.ftl");
4854

‎keyext.proofmanagement/src/main/resources/report/html/report.ftl‎

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
<#-- @ftlvariable name="title" type="String" -->
55
<#-- @ftlvariable name="bundleFileName" type="String" -->
66
<#-- @ftlvariable name="treeRoot" type="org.key_project.proofmanagement.check.PathNode" -->
7-
<#-- @ftlvariable name="entries" type="java.util.List<org.key_project.proofmanagement.check.ProofEntry>" -->
7+
<#-- @ftlvariable name="entries" type="java.util.List<org.key_project.proofmanagement.check.CheckerData.ProofEntry>" -->
88
<#-- @ftlvariable name="graph" type="org.key_project.proofmanagement.check.dependency.DependencyGraph" -->
99
<!DOCTYPE html>
1010
<html lang="en">
@@ -93,7 +93,7 @@
9393
width:max-content;
9494
padding:10px">
9595
<#list checkerData.messages as msg>
96-
<#escape x as x?xml>
96+
<#escape x as x>
9797
${msg}
9898
</#escape>
9999
<#sep> <br/> </#sep>
@@ -157,7 +157,7 @@
157157
<td>
158158
class: ${entry.contract.KJT.javaType.name}<br>
159159
target: ${entry.contract.target.name()}<br>
160-
type: ${entry.contract.getDisplayName()}
160+
type: ${entry.contract.displayName}
161161
</td>
162162
<td>
163163
<div title="${entry.sourceFile}"> ${entry.shortSrc} </div>
@@ -171,7 +171,7 @@
171171
<td>${entry.proofState}</td>
172172
<td>${entry.dependencyState}</td>
173173

174-
<#if data.checks.replay??>
174+
<#if checkerData.checks.replay??>
175175
<#if entry.replaySuccess()>
176176
<td>
177177
Nodes: ${entry.proof.statistics.nodes} <br>
@@ -251,20 +251,23 @@
251251
</tr>
252252
</thead>
253253
<tbody>
254-
<#list graph.nodes as node>
255-
<#assign scc=graph.getSCCofNode(node) />
254+
<#list graph.node2SCC as node, scc>
256255
<tr class="blue">
257256
<td style="background-color:hsl(calc(360/${graph.nodes?size} * ${scc.id}),60%,90%);">
258-
${node.contract.name?xml}
257+
${node.contract.name}
259258
</td>
260259
<td style="background-color:hsl(calc(360/${graph.nodes?size} * ${scc.id}),60%,90%);">
261260
#${scc.id?string("00")}
262-
<#if scc.legal> (legal) <#else> (illegal) </#if>
261+
<#if scc.legal>
262+
(legal)
263+
<#else>
264+
(illegal)
265+
</#if>
263266
</td>
264267
<td>&#10230;</td>
265268
<td>
266269
<#list node.dependencies?keys as d>
267-
${d.contract.name?xml}<br>
270+
${d.contract.name}<br>
268271
</#list>
269272
</td>
270273
</tr>
@@ -292,4 +295,4 @@
292295
}
293296
</script>
294297
</body>
295-
</html>
298+
</html>

0 commit comments

Comments
 (0)