Skip to content

Commit 346179a

Browse files
wadoonwadoon
committed
enabling multi-threading in TGMain
1 parent 4603f13 commit 346179a

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

44 files changed

+389
-199
lines changed

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Constants.java renamed to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Constants.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/* This file is part of KeY - https://key-project.org
22
* KeY is licensed under the GNU General Public License Version 2
33
* SPDX-License-Identifier: GPL-2.0-only */
4-
package de.uka.ilkd.key.testgen.template;
4+
package de.uka.ilkd.key.testgen;
55

66
import org.key_project.util.java.StringUtil;
77

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Format.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,5 +4,5 @@
44
package de.uka.ilkd.key.testgen;
55

66
public enum Format {
7-
JUnit4, JUnit5
7+
JUNIT_4, JUNIT_5
88
}

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,6 @@
2323
import de.uka.ilkd.key.smt.model.Model;
2424
import de.uka.ilkd.key.smt.solvertypes.SolverType;
2525
import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
26-
import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
2726

2827
import org.key_project.logic.Namespace;
2928
import org.key_project.prover.sequent.Sequent;

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,9 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.testgen;
55

6+
import java.util.Objects;
7+
import java.util.Set;
8+
69
import de.uka.ilkd.key.java.Services;
710
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
811
import de.uka.ilkd.key.logic.JTerm;
@@ -23,14 +26,15 @@
2326
import org.key_project.logic.op.Operator;
2427
import org.key_project.logic.sort.Sort;
2528

29+
import org.jspecify.annotations.Nullable;
30+
31+
import org.key_project.logic.sort.Sort;
32+
2633
import org.jspecify.annotations.Nullable;
2734
import org.jspecify.annotations.Nullable;
2835
import org.slf4j.Logger;
2936
import org.slf4j.LoggerFactory;
3037

31-
import java.util.Objects;
32-
import java.util.Set;
33-
3438
public record ProofInfo(Proof proof, Services services) {
3539
private static final Logger LOGGER = LoggerFactory.getLogger(ProofInfo.class);
3640

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGMain.java‎

Lines changed: 81 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,23 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.testgen;
55

6+
import java.io.File;
7+
import java.util.ArrayList;
8+
import java.util.LinkedList;
9+
import java.util.List;
10+
import java.util.concurrent.Callable;
11+
import java.util.concurrent.Executors;
12+
import java.util.concurrent.Future;
13+
import java.util.regex.Pattern;
14+
615
import de.uka.ilkd.key.api.ProofManagementApi;
716
import de.uka.ilkd.key.control.KeYEnvironment;
817
import de.uka.ilkd.key.proof.Proof;
918
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
1019
import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
1120
import de.uka.ilkd.key.speclang.Contract;
12-
import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
13-
import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLogger;
21+
import de.uka.ilkd.key.testgen.smt.testgen.TGPhase;
22+
import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLifecycleListener;
1423
import org.slf4j.Logger;
1524
import org.slf4j.LoggerFactory;
1625
import picocli.CommandLine;
@@ -34,35 +43,43 @@ public static void main(String[] args) throws ProblemLoaderException, Interrupte
3443
@CommandLine.Parameters(description = "KeY or Java file.", arity = "1..*")
3544
private List<File> files = new LinkedList<>();
3645

46+
@CommandLine.Parameters(description = "Number of parallel jobs", defaultValue = "4")
47+
private int numberOfThreads = 4;
48+
3749
@CommandLine.Option(names = {"-s", "--symbex"},
38-
description = "apply symbex", negatable = true)
50+
description = "apply symbolic execution", negatable = true)
3951
private boolean symbex;
4052

41-
@CommandLine.Option(names = {"-c", "--contract"},
42-
arity = "*",
43-
description = "name of the contract to be loaded in the Java environment")
53+
@CommandLine.Option(names = { "-c", "--contract" }, arity = "*",
54+
description = "name of the contract to be loaded in the Java environment. Can be a regular expression")
4455
private List<String> contractNames = new ArrayList<>();
4556

4657
@CommandLine.Option(names = {"--all-contracts"},
47-
description = "name of the contract to be loaded in the Java environment")
58+
description = "test case generation for all contracts")
4859
private boolean allContracts = false;
4960

50-
5161
@CommandLine.Option(names = {"-o", "--output"}, description = "Output folder")
5262
private File outputFolder = new File("out");
5363

5464
@CommandLine.Option(names = {"-r", "--rfl"}, description = "Use Reflection class", negatable = true)
5565
private boolean useReflection = false;
5666

57-
@CommandLine.Option(names = {"-f", "--format"}, description = "Use Reflection class")
58-
private Format format = Format.JUnit4;
67+
@CommandLine.Option(names = { "-f", "--format" },
68+
description = "use Reflection class for instantiation")
69+
private Format format = Format.JUNIT_4;
5970

60-
61-
@CommandLine.Option(names = {"--max-unwinds"}, description = "max unwinds")
71+
@CommandLine.Option(names = { "--max-unwinds" }, description = "max unwinds of loops")
6272
private int maxUnwinds = 10;
73+
6374
@CommandLine.Option(names = {"--dups"}, description = "remove duplicates", negatable = true)
6475
private boolean removeDuplicates;
6576

77+
@CommandLine.Option(names = { "--only-tests" },
78+
description = "only put test classes directly in the output folder, no build file, no copy of sources",
79+
negatable = true)
80+
private boolean onlyTestClasses;
81+
82+
6683
@Override
6784
public Integer call() throws Exception {
6885
if (SolverTypes.Z3_CE_SOLVER.checkForSupport()) {
@@ -73,13 +90,27 @@ public Integer call() throws Exception {
7390
}
7491

7592
var settings = new TestGenerationSettings();
76-
TestGenerationLogger log = new SysoutTestGenerationLogger();
93+
TestGenerationLifecycleListener log = new SysoutTestGenerationLifecycleListener();
7794
settings.setOutputPath(outputFolder.getAbsolutePath());
78-
settings.setRFL(useReflection);
95+
settings.setUseRFL(useReflection);
7996
settings.setFormat(format);
8097
settings.setApplySymbolicExecution(symbex);
8198
settings.setMaxUnwinds(maxUnwinds);
8299
settings.setRemoveDuplicates(removeDuplicates);
100+
settings.setOnlyTestClasses(onlyTestClasses);
101+
102+
var contractNameMatcher = Pattern.compile(String.join("|", contractNames))
103+
.asMatchPredicate();
104+
105+
if (allContracts) {
106+
LOGGER.info("I accept every contract given by `--all-contracts`");
107+
} else if (contractNames.isEmpty()) {
108+
LOGGER.info(
109+
"Only printing the contracts. You need to give contracts with `-c` or use `--all-contracts`.");
110+
} else {
111+
LOGGER.info("Regex matching against contract names is: {}", contractNameMatcher);
112+
}
113+
83114

84115
for (File file : files) {
85116
List<Proof> proofs = new LinkedList<>();
@@ -93,39 +124,55 @@ public Integer call() throws Exception {
93124
final var name = contract.getName();
94125
if (print) {
95126
LOGGER.info("Contract found: {}", name);
96-
}
97-
98-
if (allContracts || contractNames.contains(name)) {
127+
} else if (allContracts || contractNameMatcher.test(name)) {
99128
proofs.add(api.startProof(contract).getProof());
100129
}
101130
}
102131
} else { // key file
103132
proofs = List.of(proof);
104133
}
105134

106-
for (Proof p : proofs) {
107-
TestgenFacade.generateTestcases(env, p, settings, log);
108-
p.dispose();
109-
}
135+
LOGGER.info("Number of proof found: {}", proofs.size());
110136

111-
env.dispose();
137+
var exec = Executors.newFixedThreadPool(numberOfThreads);
138+
try {
139+
LOGGER.info("Start processing with {} threads", numberOfThreads);
140+
var tasks = proofs.stream().map(
141+
p -> TestgenFacade.generateTestcasesTask(env, p, settings, log)).toList();
142+
var futures = tasks.stream().map(exec::submit).toList();
143+
for (Future<?> future : futures) {
144+
future.wait();
145+
}
146+
} finally {
147+
proofs.forEach(Proof::dispose);
148+
env.dispose();
149+
}
112150
}
113151
return 0;
114152
}
153+
}
115154

116-
private static class SysoutTestGenerationLogger implements TestGenerationLogger {
117-
@Override
118-
public void writeln(String message) {
119-
LOGGER.info(message);
120-
}
121155

122-
@Override
123-
public void writeException(Throwable throwable) {
124-
LOGGER.error("Error occurred!", throwable);
125-
}
156+
class SysoutTestGenerationLifecycleListener implements TestGenerationLifecycleListener {
157+
private final static Logger LOGGER = LoggerFactory.getLogger("main");
158+
159+
@Override
160+
public void writeln(@Nullable String message) {
161+
if(message!=null){ LOGGER.info(message);}
162+
}
163+
164+
@Override
165+
public void writeException(Object sender, Throwable throwable) {
166+
LOGGER.error("Error occurred!", throwable);
167+
}
168+
169+
@Override
170+
public void finish(Object sender) {
171+
172+
}
173+
174+
@Override
175+
public void phase(Object sender, TGPhase phase) {
126176

127-
@Override
128-
public void close() {
129-
}
130177
}
131178
}

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGReporter.java‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
4+
package de.uka.ilkd.key.testgen;
5+
6+
import de.uka.ilkd.key.testgen.smt.testgen.TGPhase;
7+
import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLifecycleListener;
8+
9+
/**
10+
* @author Alexander Weigl
11+
* @version 1 (24.05.24)
12+
*/
13+
public record TGReporter(TestGenerationLifecycleListener log) {
14+
public void writeln(String message) {
15+
log.writeln(this, message);
16+
}
17+
18+
public void reportException(Exception e) {
19+
log.writeException(this, e);
20+
}
21+
22+
public void phase(TGPhase phase) {
23+
log.phase(this, phase);
24+
}
25+
26+
public void finish() {
27+
log.finish(this);
28+
}
29+
}

0 commit comments

Comments
 (0)