diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java index 5c7b32ec8f7..712925aac83 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java @@ -95,8 +95,11 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckFailResult; import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckRtInconsistentResult; import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckSuccessResult; +import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckVacuousResult; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.Req2BoogieTranslator; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.ReqSymboltableBuilder; +import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.VacuityAnnotation; +import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.BoogieIcfgLocation; import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.CodeBlock; import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.CodeBlockFactory; import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.ParallelComposition; @@ -187,6 +190,15 @@ public IResult convertTraceAbstractionResult(final IResult result) { final String failurePath = formatTimeSequenceMap(delta2var2value); return new ReqCheckRtInconsistentResult<>(element, plugin, failurePath); } + if (spec == Spec.VACUOUS) { + // Return a ReqCheckVacuousResult, i.e., a ReqCheckFailResult with additional + // VacuityAnnotation containing an invariant that might be enforced by the + // vacuous requirement. + VacuityAnnotation enforcedInv = VacuityAnnotation + .getAnnotation(((BoogieIcfgLocation) element).getBoogieASTNode()); + return new ReqCheckVacuousResult<>(element, plugin, + enforcedInv.getInvariant().toString()); + } return new ReqCheckFailResult<>(element, plugin); } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java index 858924bfbac..9fe16c070b9 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/req2pea/ReqCheckAnnotator.java @@ -29,8 +29,10 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.Collections; +import java.util.HashMap; import java.util.Iterator; import java.util.List; +import java.util.Map; import java.util.Map.Entry; import java.util.Set; import java.util.concurrent.TimeUnit; @@ -57,6 +59,7 @@ import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.BoogieDeclarations; +import de.uni_freiburg.informatik.ultimate.lib.pea.CDD; import de.uni_freiburg.informatik.ultimate.lib.pea.CounterTrace; import de.uni_freiburg.informatik.ultimate.lib.pea.PEAComplement; import de.uni_freiburg.informatik.ultimate.lib.pea.Phase; @@ -75,6 +78,7 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.preferences.Pea2BoogiePreferences.PEATransformerMode; import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheck; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.CheckedReqLocation; +import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.VacuityAnnotation; import de.uni_freiburg.informatik.ultimate.util.CoreUtil; import de.uni_freiburg.informatik.ultimate.util.datastructures.CrossProducts; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; @@ -108,6 +112,7 @@ public class ReqCheckAnnotator implements IReq2PeaAnnotator { private final List mReqPeas; private final Durations mDurations; + private CDD mEnforcedInv; public ReqCheckAnnotator(final IUltimateServiceProvider services, final ILogger logger, final List reqPeas, final IReqSymbolTable symbolTable, final Durations durations) { @@ -442,7 +447,10 @@ private List genChecksNonVacuity(final BoogieLocation bl) { final PatternType pattern = reqpea.getPattern(); for (final Entry pea : reqpea.getCounterTrace2Pea()) { final Statement assertStmt = genAssertNonVacuous(pattern, pea.getValue(), bl); + if (assertStmt != null) { + VacuityAnnotation vacAnnotation = new VacuityAnnotation(mEnforcedInv); + vacAnnotation.annotate(assertStmt); stmtList.add(assertStmt); } } @@ -467,6 +475,7 @@ private List genChecksNonVacuity(final BoogieLocation bl) { private Statement genAssertNonVacuous(final PatternType req, final PhaseEventAutomata aut, final BoogieLocation bl) { final List phases = aut.getPhases(); + mEnforcedInv = CDD.TRUE; // compute the maximal phase number occurring in the automaton. int maxBits = 0; @@ -487,20 +496,32 @@ private Statement genAssertNonVacuous(final PatternType req, final PhaseEvent // check that one of those phases is eventually reached. final List checkReached = new ArrayList<>(); + final Map enforcedInv = new HashMap<>(); + if (pnr > 0) { for (int i = 0; i < phases.size(); i++) { final PhaseBits bits = phases.get(i).getPhaseBits(); if (bits == null || (bits.getActive() & 1 << pnr - 1) == 0) { checkReached.add(genComparePhaseCounter(i, mSymbolTable.getPcName(aut), bl)); } + // Store state invariants of PEA locations where max DC phase is not active. + if (bits.getActive() < (1 << pnr - 1)) { + enforcedInv.put(phases.get(i), phases.get(i).getStateInv()); + } } } + // Store invariant enforced by the requirement in case of vacuity + if (enforcedInv.size() == 1) { + mEnforcedInv = (CDD) enforcedInv.values().toArray()[0]; + } if (checkReached.isEmpty()) { return null; } + final Expression disjunction = genDisjunction(checkReached, bl); final ReqCheck check = createReqCheck(Spec.VACUOUS, req, aut); final String label = "VACUOUS_" + aut.getName(); + return createAssert(disjunction, check, label); } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckVacuousResult.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckVacuousResult.java new file mode 100644 index 00000000000..3523764b8c1 --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckVacuousResult.java @@ -0,0 +1,58 @@ +/* + * Copyright (C) 2024 University of Freiburg + * + * This file is part of the ULTIMATE PEAtoBoogie plug-in. + * + * The ULTIMATE PEAtoBoogie plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE PEAtoBoogie plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE PEAtoBoogie plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE PEAtoBoogie plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE PEAtoBoogie plug-in grant you additional permission + * to convey the resulting work. + */ +package de.uni_freiburg.informatik.ultimate.pea2boogie.results; + +import de.uni_freiburg.informatik.ultimate.core.model.models.IElement; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction; +import de.uni_freiburg.informatik.ultimate.lib.pea.CDD; +import de.uni_freiburg.informatik.ultimate.util.CoreUtil; + + +public final class ReqCheckVacuousResult + extends ReqCheckFailResult { + + private final String mEnforcedInvariant; + + public ReqCheckVacuousResult(final LOC element, final String plugin, final String enforcedInvariant) { + super(element, plugin); + mEnforcedInvariant = enforcedInvariant; + } + + public ReqCheckVacuousResult(final LOC element, final String plugin) { + this(element, plugin, null); + } + + @Override + public String getLongDescription() { + final StringBuilder sb = new StringBuilder(); + sb.append(getShortDescription()); + if (mEnforcedInvariant != CDD.TRUE.toString()) { + sb.append(CoreUtil.getPlatformLineSeparator()); + sb.append("Vacous requirement silently enforces invariant: " + mEnforcedInvariant); + } + return sb.toString(); + } +} \ No newline at end of file diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/VacuityAnnotation.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/VacuityAnnotation.java new file mode 100644 index 00000000000..4aa601110da --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/VacuityAnnotation.java @@ -0,0 +1,61 @@ +/* + * Copyright (C) 2024 University of Freiburg + * + * This file is part of the ULTIMATE Core. + * + * The ULTIMATE Core is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE Core is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE Core. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE Core, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE Core grant you additional permission + * to convey the resulting work. + */ +package de.uni_freiburg.informatik.ultimate.pea2boogie.translator; + +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.ModernAnnotations; +import de.uni_freiburg.informatik.ultimate.core.model.models.IElement; +import de.uni_freiburg.informatik.ultimate.core.model.models.ModelUtils; +import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.IAnnotations; +import de.uni_freiburg.informatik.ultimate.lib.pea.CDD; + +/** + * + * Annotation for vacuity checks. This marks whether a vacuous requirement + * enforces a trivial invariant. + * + */ + +public class VacuityAnnotation extends ModernAnnotations { + + private static final long serialVersionUID = 1L; + private final CDD mEnforcedInvariant; + + public VacuityAnnotation(final CDD enforcedInv) { + mEnforcedInvariant = enforcedInv; + } + + public CDD getInvariant() { + return mEnforcedInvariant; + } + + public IAnnotations annotate(final IElement elem) { + return elem.getPayload().getAnnotations().put(VacuityAnnotation.class.getName(), this); + } + + public static VacuityAnnotation getAnnotation(final IElement node) { + return ModelUtils.getAnnotation(node, VacuityAnnotation.class); + } +}