Skip to content

Commit

Permalink
Merge branch 'development' into spirv
Browse files Browse the repository at this point in the history
  • Loading branch information
@natgavrilenko
natgavrilenko authored Jan 12, 2024
2 parents 63d2dd7 + 28bb592 commit 9e6c114
Showing 1 changed file with 32 additions and 28 deletions.
60 changes: 32 additions & 28 deletions dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ public class Dartagnan extends BaseOptions {
private static final Logger logger = LogManager.getLogger(Dartagnan.class);

private static final Set<String> supportedFormats =
ImmutableSet.copyOf(Arrays.asList(".litmus", ".c", ".i", "ll"));
ImmutableSet.copyOf(Arrays.asList(".litmus", ".c", ".i", ".ll"));

private Dartagnan(Configuration config) throws InvalidConfigurationException {
config.recursiveInject(this);
Expand All @@ -87,18 +87,13 @@ public static void main(String[] args) throws Exception {
GlobalSettings.configure(config);
LogGlobalSettings();

if (Arrays.stream(args).noneMatch(a -> supportedFormats.stream().anyMatch(a::endsWith))) {
throw new IllegalArgumentException("Input program not given or format not recognized");
}
// get() is guaranteed to succeed
File fileProgram = new File(Arrays.stream(args).filter(a -> supportedFormats.stream().anyMatch(a::endsWith)).findFirst().get());
File fileProgram = new File(Arrays.stream(args).filter(a -> supportedFormats.stream().anyMatch(a::endsWith))
.findFirst()
.orElseThrow(() -> new IllegalArgumentException("Input program not given or format not recognized")));
logger.info("Program path: " + fileProgram);

if (Arrays.stream(args).noneMatch(a -> a.endsWith(".cat"))) {
throw new IllegalArgumentException("CAT model not given or format not recognized");
}
// get() is guaranteed to succeed
File fileModel = new File(Arrays.stream(args).filter(a -> a.endsWith(".cat")).findFirst().get());
File fileModel = new File(Arrays.stream(args).filter(a -> a.endsWith(".cat")).findFirst()
.orElseThrow(() -> new IllegalArgumentException("CAT model not given or format not recognized")));
logger.info("CAT file path: " + fileModel);

Wmm mcm = new ParserCat().parse(fileModel);
Expand Down Expand Up @@ -147,7 +142,7 @@ public static void main(String[] args) throws Exception {
BasicLogManager.create(solverConfig),
sdm.getNotifier(),
o.getSolver());
ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
ModelChecker modelChecker;
if (properties.contains(DATARACEFREEDOM)) {
if (properties.size() > 1) {
Expand Down Expand Up @@ -215,14 +210,17 @@ public static void main(String[] args) throws Exception {
}
}

private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker, String summary) {
private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover,
ModelChecker modelChecker, String summary) {
// ------------------ Generate Witness, if possible ------------------
final EnumSet<Property> properties = task.getProperty();
if (task.getProgram().getFormat().equals(SourceLanguage.LLVM) && modelChecker.hasModel() && properties.contains(PROGRAM_SPEC)) {
if (task.getProgram().getFormat().equals(SourceLanguage.LLVM) && modelChecker.hasModel()
&& properties.contains(PROGRAM_SPEC)) {
try {
WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, modelChecker.getResult(), summary);
WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover,
modelChecker.getResult(), summary);
if (w.canBeBuilt()) {
// We can only write witnesses if the path to the original C file was given.
// We can only write witnesses if the path to the original C file was given.
w.build().write();
}
} catch (InvalidConfigurationException e) {
Expand All @@ -231,7 +229,8 @@ private static void generateWitnessIfAble(VerificationTask task, ProverEnvironme
}
}

public static String generateResultSummary(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker) throws SolverException {
public static String generateResultSummary(VerificationTask task, ProverEnvironment prover,
ModelChecker modelChecker) throws SolverException {
// ----------------- Generate output of verification result -----------------
final Program p = task.getProgram();
final EnumSet<Property> props = task.getProperty();
Expand All @@ -250,10 +249,11 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
printWarningIfThreadStartFailed(p, encCtx, prover);
if (props.contains(PROGRAM_SPEC) && FALSE.equals(model.evaluate(PROGRAM_SPEC.getSMTVariable(encCtx)))) {
summary.append("===== Program specification violation found =====\n");
for(Assert ass: p.getThreadEvents(Assert.class)) {
for (Assert ass : p.getThreadEvents(Assert.class)) {
final boolean isViolated = TRUE.equals(model.evaluate(encCtx.execution(ass)))
&& FALSE.equals(model.evaluate(encCtx.encodeExpressionAsBooleanAt(ass.getExpression(), ass)));
if(isViolated) {
&& FALSE.equals(
model.evaluate(encCtx.encodeExpressionAsBooleanAt(ass.getExpression(), ass)));
if (isViolated) {
final String callStack = makeContextString(
synContext.getContextInfo(ass).getContextOfType(CallContext.class), " -> ");
summary
Expand All @@ -269,9 +269,9 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
}
if (props.contains(LIVENESS) && FALSE.equals(model.evaluate(LIVENESS.getSMTVariable(encCtx)))) {
summary.append("============ Liveness violation found ============\n");
for(CondJump e : p.getThreadEvents(CondJump.class)) {
if(e.hasTag(Tag.SPINLOOP) && TRUE.equals(model.evaluate(encCtx.execution(e)))
&& TRUE.equals(model.evaluate(encCtx.jumpCondition(e)))) {
for (CondJump e : p.getThreadEvents(CondJump.class)) {
if (e.hasTag(Tag.SPINLOOP) && TRUE.equals(model.evaluate(encCtx.execution(e)))
&& TRUE.equals(model.evaluate(encCtx.jumpCondition(e)))) {
final String callStack = makeContextString(
synContext.getContextInfo(e).getContextOfType(CallContext.class), " -> ");
summary
Expand All @@ -286,7 +286,8 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
}
final List<Axiom> violatedCATSpecs = task.getMemoryModel().getAxioms().stream()
.filter(Axiom::isFlagged)
.filter(ax -> props.contains(CAT_SPEC) && FALSE.equals(model.evaluate(CAT_SPEC.getSMTVariable(ax, encCtx))))
.filter(ax -> props.contains(CAT_SPEC)
&& FALSE.equals(model.evaluate(CAT_SPEC.getSMTVariable(ax, encCtx))))
.toList();
if (!violatedCATSpecs.isEmpty()) {
summary.append("======= CAT specification violation found =======\n");
Expand Down Expand Up @@ -329,7 +330,8 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
} else {
final List<Axiom> violatedCATSpecs = task.getMemoryModel().getAxioms().stream()
.filter(Axiom::isFlagged)
.filter(ax -> props.contains(CAT_SPEC) && FALSE.equals(model.evaluate(CAT_SPEC.getSMTVariable(ax, encCtx))))
.filter(ax -> props.contains(CAT_SPEC)
&& FALSE.equals(model.evaluate(CAT_SPEC.getSMTVariable(ax, encCtx))))
.toList();
for (Axiom violatedAx : violatedCATSpecs) {
summary.append("Flag ")
Expand All @@ -344,7 +346,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
logger.warn("Unexpected result for litmus test: {}", result);
summary.append(result).append("\n");
} else if (task.getProperty().contains(PROGRAM_SPEC)) {
//... which can be good or bad (no witness = bad, not violation = good)
// ... which can be good or bad (no witness = bad, not violation = good)
summary.append("Condition ").append(p.getSpecification().toStringWithType()).append("\n");
summary.append(result == PASS ? "Ok" : "No").append("\n");
}
Expand All @@ -353,9 +355,11 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
return summary.toString();
}

private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverEnvironment prover) throws SolverException {
private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverEnvironment prover)
throws SolverException {
for (Event e : p.getThreadEvents()) {
if (e.hasTag(Tag.STARTLOAD) && BigInteger.ZERO.equals(prover.getModel().evaluate(encoder.value((Load) e)))) {
if (e.hasTag(Tag.STARTLOAD)
&& BigInteger.ZERO.equals(prover.getModel().evaluate(encoder.value((Load) e)))) {
// This msg should be displayed even if the logging is off
System.out.printf(
"[WARNING] The call to pthread_create of thread %s failed. To force thread creation to succeed use --%s=true%n",
Expand Down

0 comments on commit 9e6c114

Please sign in to comment.