Skip to content

Commit 57769a7

Browse files
ThomasHaasThomasHaas
committed
Minor cleanup
1 parent 64ff912 commit 57769a7

1 file changed

Lines changed: 47 additions & 55 deletions

File tree

‎dartagnan/src/main/java/com/dat3m/dartagnan/verification/TaskResultAnalyzer.java‎

Lines changed: 47 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
package com.dat3m.dartagnan.verification;
22

3-
import com.dat3m.dartagnan.configuration.OptionNames;
43
import com.dat3m.dartagnan.configuration.Property;
54
import com.dat3m.dartagnan.encoding.IREvaluator;
5+
import com.dat3m.dartagnan.expression.Expression;
66
import com.dat3m.dartagnan.expression.ExpressionPrinter;
77
import com.dat3m.dartagnan.expression.booleans.BoolLiteral;
88
import com.dat3m.dartagnan.program.Program;
@@ -39,6 +39,7 @@
3939
import static com.dat3m.dartagnan.configuration.OptionNames.BOUNDS_SAVE_PATH;
4040
import static com.dat3m.dartagnan.configuration.OptionNames.IGNORE_FILTER_SPECIFICATION;
4141
import static com.dat3m.dartagnan.configuration.Property.*;
42+
import static com.dat3m.dartagnan.program.Program.SourceLanguage.*;
4243
import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.*;
4344
import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.getSourceLocationString;
4445
import static com.dat3m.dartagnan.utils.ExitCode.*;
@@ -58,26 +59,17 @@ public static TaskResultAnalyzer create() {
5859
}
5960

6061
public ResultSummary getSummaryFromException(Exception exception, String programPath) {
61-
final String message = exception.getMessage();
62+
final String message = exception.getMessage() != null ? exception.getMessage() : "Unknown error occurred";
63+
final String details = "\t" + message;
6264

6365
if (exception instanceof InterruptedException) {
64-
final String details;
65-
final ExitCode exitCode;
66-
if (message != null) {
67-
details = "\t" + message;
68-
exitCode = message.contains("Timeout")
69-
? TIMEOUT_ELAPSED
70-
: message.contains("canceled")
71-
? CANCELED
72-
: UNKNOWN_ERROR;
73-
} else {
74-
details = "\tUnknown error occurred";
75-
exitCode = UNKNOWN_ERROR;
76-
}
66+
final ExitCode exitCode =
67+
message.contains("Timeout") ? TIMEOUT_ELAPSED
68+
: message.contains("canceled") ? CANCELED
69+
: UNKNOWN_ERROR;
7770
return new ResultSummary(programPath, "", INTERRUPTED, "", "", details, 0, exitCode);
7871
} else {
7972
final String reason = exception.getClass().getSimpleName();
80-
final String details = "\t" + Optional.ofNullable(message).orElse("Unknown error occurred");
8173
return new ResultSummary(programPath, "", ERROR, "", reason, details, 0, UNKNOWN_ERROR);
8274
}
8375
}
@@ -100,7 +92,7 @@ public ResultSummary getSummaryFromSolver(TaskSolver solver, String programPath)
10092
// We only show the condition if this is the reason of the failure
10193
String condition = "";
10294
if (hasViolationsWithModel) {
103-
printWarningIfThreadStartFailed(p, model);
95+
10496
if (props.contains(PROGRAM_SPEC) && model.propertyViolated(PROGRAM_SPEC)) {
10597
reason = ResultSummary.PROGRAM_SPEC_REASON;
10698
condition = getSpecificationString(p);
@@ -114,6 +106,7 @@ public ResultSummary getSummaryFromSolver(TaskSolver solver, String programPath)
114106
ExitCode code = task.getWitness().isEmpty() ? PROGRAM_SPEC_VIOLATION : NORMAL_TERMINATION;
115107
return new ResultSummary(programPath, filter, FAIL, condition, reason, details.toString(), time, code);
116108
}
109+
117110
if (props.contains(TERMINATION) && model.propertyViolated(TERMINATION)) {
118111
reason = ResultSummary.TERMINATION_REASON;
119112
for (Event e : p.getThreadEvents()) {
@@ -131,12 +124,14 @@ public ResultSummary getSummaryFromSolver(TaskSolver solver, String programPath)
131124
ExitCode code = task.getWitness().isEmpty() ? TERMINATION_VIOLATION : NORMAL_TERMINATION;
132125
return new ResultSummary(programPath, filter, FAIL, condition, reason, details.toString(), time, code);
133126
}
127+
134128
if (props.contains(DATARACEFREEDOM) && model.propertyViolated(DATARACEFREEDOM)) {
135129
reason = ResultSummary.SVCOMP_RACE_REASON;
136130
// In validation mode, we expect to find the violation, thus NORMAL_TERMINATION
137131
ExitCode code = task.getWitness().isEmpty() ? DATA_RACE_FREEDOM_VIOLATION : NORMAL_TERMINATION;
138132
return new ResultSummary(programPath, filter, FAIL, condition, reason, details.toString(), time, code);
139133
}
134+
140135
if (props.contains(TRACKABILITY) && model.propertyViolated(TRACKABILITY)) {
141136
reason = ResultSummary.SVCOMP_UNTRACKABLE_OBJECT_REASON;
142137
for (MemoryObject o : p.getMemory().getObjects()) {
@@ -147,16 +142,18 @@ public ResultSummary getSummaryFromSolver(TaskSolver solver, String programPath)
147142
ExitCode code = task.getWitness().isEmpty() ? MEMORY_TRACKABILITY_VIOLATION : NORMAL_TERMINATION;
148143
return new ResultSummary(programPath, filter, FAIL, condition, reason, details.toString(), time, code);
149144
}
150-
final List<Axiom> violatedCATSpecs = !props.contains(CAT_SPEC) ? List.of()
151-
: task.getMemoryModel().getAxioms().stream()
152-
.filter(Axiom::isFlagged)
153-
.filter(model::isFlaggedAxiomViolated)
154-
.toList();
155-
if (!violatedCATSpecs.isEmpty()) {
156-
reason = ResultSummary.CAT_SPEC_REASON;
157-
// In validation mode, we expect to find the violation, thus NORMAL_TERMINATION
158-
ExitCode code = task.getWitness().isEmpty() ? CAT_SPEC_VIOLATION : NORMAL_TERMINATION;
159-
return new ResultSummary(programPath, filter, FAIL, condition, reason, getFlaggedPairsOutput(task, model, synContext), time, code);
145+
146+
if (props.contains(CAT_SPEC)) {
147+
final List<Axiom> violatedCATSpecs = task.getMemoryModel().getAxioms().stream()
148+
.filter(Axiom::isFlagged)
149+
.filter(model::isFlaggedAxiomViolated)
150+
.toList();
151+
if (!violatedCATSpecs.isEmpty()) {
152+
reason = ResultSummary.CAT_SPEC_REASON;
153+
// In validation mode, we expect to find the violation, thus NORMAL_TERMINATION
154+
ExitCode code = task.getWitness().isEmpty() ? CAT_SPEC_VIOLATION : NORMAL_TERMINATION;
155+
return new ResultSummary(programPath, filter, FAIL, condition, reason, getFlaggedPairsOutput(task, model, synContext), time, code);
156+
}
160157
}
161158
} else if (hasViolationsWithoutWitness) {
162159
// Only for programs with exists/forall specifications
@@ -182,6 +179,7 @@ public ResultSummary getSummaryFromSolver(TaskSolver solver, String programPath)
182179
ExitCode code = BOUNDED_RESULT;
183180
return new ResultSummary(programPath, filter, result, condition, reason, details.toString(), time, code);
184181
}
182+
185183
// We consider those cases without an explicit return to yield normal termination.
186184
// This includes verification of litmus code, independent of the verification result.
187185
// In validation mode, we expect to find the violation, thus the WITNESS_NOT_VALIDATED error
@@ -191,17 +189,18 @@ public ResultSummary getSummaryFromSolver(TaskSolver solver, String programPath)
191189

192190
public File generateWitnessIfAble(TaskSolver solver, WitnessType witnessType, String filename, String details,
193191
boolean generateWitnessForUnknown) throws IOException {
194-
if (!solver.hasModel() || (solver.getResult() == UNKNOWN && !generateWitnessForUnknown)) {
192+
if (!solver.hasModel()
193+
|| (solver.getResult() == UNKNOWN && !generateWitnessForUnknown)
194+
|| witnessType == WitnessType.NONE) {
195195
return null;
196196
}
197197

198198
final VerificationTask task = solver.getTask();
199199
switch (witnessType) {
200-
case NONE: { }
201-
case GRAPHML: {
200+
case GRAPHML -> {
202201
Preconditions.checkArgument(solver.getResult() != UNKNOWN);
203202

204-
if (!task.getProgram().getFormat().equals(Program.SourceLanguage.LLVM) || !requiresSvcompWitness(task.getProperty())) {
203+
if (!task.getProgram().getFormat().equals(LLVM) || !requiresSvcompWitness(task.getProperty())) {
205204
return null;
206205
}
207206
try {
@@ -213,7 +212,7 @@ public File generateWitnessIfAble(TaskSolver solver, WitnessType witnessType, St
213212
logger.warn(e.getMessage());
214213
}
215214
}
216-
case DOT, PNG: {
215+
case DOT, PNG -> {
217216
final SyntacticContextAnalysis synContext = newInstance(task.getProgram());
218217
final ExecutionModelNext model = solver.getExecutionGraph();
219218
// RF edges give both ordering and data flow information, thus even when the pair is in PO
@@ -225,6 +224,7 @@ public File generateWitnessIfAble(TaskSolver solver, WitnessType witnessType, St
225224
synContext, witnessType.convertToPng(), task.getConfig());
226225
}
227226
}
227+
228228
return null;
229229
}
230230

@@ -311,36 +311,28 @@ private static String getFlaggedPairsOutput(VerificationTask task, IREvaluator m
311311
return output.toString();
312312
}
313313

314-
private static void printWarningIfThreadStartFailed(Program p, IREvaluator model) {
315-
p.getThreads().stream().filter(t ->
316-
t.getEntry().isSpawned()
317-
&& model.isExecuted(t.getEntry().getCreator())
318-
&& !model.threadHasStarted(t)
319-
).forEach(t -> System.out.printf(
320-
"[WARNING] The call to pthread_create of thread %s failed. To force thread creation to succeed use --%s=true%n",
321-
t, OptionNames.THREAD_CREATE_ALWAYS_SUCCEEDS
322-
));
323-
}
324-
325314
private static String getSpecificationString(Program program) {
315+
if (!List.of(LITMUS, SPV).contains(program.getFormat())) {
316+
return "";
317+
}
318+
326319
final StringBuilder sb = new StringBuilder();
327-
final Program.SourceLanguage format = program.getFormat();
328-
if (format == Program.SourceLanguage.LITMUS || format == Program.SourceLanguage.SPV) {
329-
sb.append(program.getSpecificationType().toString().toLowerCase()).append(" ");
330-
if (program.getSpecification() != null) {
331-
sb.append(new ExpressionPrinter(true).visit(program.getSpecification()));
332-
}
333-
sb.append("\n");
320+
sb.append(program.getSpecificationType().toString().toLowerCase()).append(" ");
321+
// TODO: Can the spec really be null here?
322+
if (program.getSpecification() != null) {
323+
sb.append(new ExpressionPrinter(true).visit(program.getSpecification()));
334324
}
325+
sb.append("\n");
335326
return sb.toString();
336327
}
337328

338329
private static String getFilterString(VerificationTask task) {
339-
final Program p = task.getProgram();
340-
final boolean ignoreFilter = task.getConfig().hasProperty(IGNORE_FILTER_SPECIFICATION) && task.getConfig().getProperty(IGNORE_FILTER_SPECIFICATION).equals("true");
341-
final boolean nonEmptyFilter = !(p.getFilterSpecification() instanceof BoolLiteral bLit) || !bLit.getValue();
342-
final String filter = !ignoreFilter && nonEmptyFilter ? p.getFilterSpecification().toString() : "";
343-
return filter;
330+
if ("true".equals(task.getConfig().getProperty(IGNORE_FILTER_SPECIFICATION)))
331+
return "";
332+
333+
final Expression filter = task.getProgram().getFilterSpecification();
334+
final boolean isTrivialFilter = filter instanceof BoolLiteral bLit && bLit.getValue();
335+
return isTrivialFilter ? "" : filter.toString();
344336
}
345337

346338
}

0 commit comments

Comments
 (0)