Requirement redundancies: Approximation of explanation via invariants

trunk/source/Library-Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/FloydHoareUtils.java

@@ -127,6 +127,29 @@ public static void createInvariantResults(final String pluginName, final IIcfg<I
 			}
 			new WitnessInvariant(invResult.getInvariant()).annotate(locNode);
 		}
+
+		// Temporary hack: Get the invariant of the pre-error location
+		// There exists only one in our use case, needs to be generalized if obtaining
+		// invariants for all pre-error locations is desired
+		final var errorLocs = IcfgUtils.getErrorLocations(icfg).iterator();
+		if (errorLocs.hasNext())
+		{
+			final var preLocs = errorLocs.next().getIncomingNodes();
+			// Hack: For reqcheck there only exists one pre-error location
+			final var preLoc = preLocs.isEmpty() ? null : preLocs.get(0);
+			if (preLoc != null)
+			{
+				final IPredicate hoare = annotation.getAnnotation(preLoc);
+				if (hoare == null)
+				{
+					return;
+				}
+				final Term formula = hoare.getFormula();
+				final var invResult =
+						new InvariantResult<IIcfgElement>(pluginName, preLoc, backTranslatorService, formula, checks);
+				reporter.accept(invResult);
+			}
+		}
 	}
 
 	public static void createProcedureContractResults(final IUltimateServiceProvider services, final String pluginName,

trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/results/InvariantResult.java

@@ -79,4 +79,8 @@ public String getLongDescription() {
 	public Set<Check> getChecks() {
 		return mChecks;
 	}
+
+	public boolean isLoopLocation() {
+		return mIsLoopLocation;
+	}
 }

trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java

@@ -46,6 +46,7 @@
 import de.uni_freiburg.informatik.ultimate.core.lib.results.AllSpecificationsHoldResult;
 import de.uni_freiburg.informatik.ultimate.core.lib.results.CounterExampleResult;
 import de.uni_freiburg.informatik.ultimate.core.lib.results.IResultWithCheck;
+import de.uni_freiburg.informatik.ultimate.core.lib.results.InvariantResult;
 import de.uni_freiburg.informatik.ultimate.core.lib.results.PositiveResult;
 import de.uni_freiburg.informatik.ultimate.core.model.models.IElement;
 import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.Spec;
@@ -93,6 +94,7 @@
 import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
 import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheck;
 import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckFailResult;
+import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckRedundancyResult;
 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.translator.Req2BoogieTranslator;
@@ -126,6 +128,7 @@ public VerificationResultTransformer(final ILogger logger, final IUltimateServic
 	public IResult convertTraceAbstractionResult(final IResult result) {
 		final AbstractResultAtElement<?> oldRes;
 		final ReqCheck reqCheck;
+		InvariantResult<?> invResult = null;
 		boolean isPositive;
 		if (result instanceof CounterExampleResult<?, ?, ?>) {
 			oldRes = (AbstractResultAtElement<?>) result;
@@ -138,6 +141,25 @@ public IResult convertTraceAbstractionResult(final IResult result) {
 		} else if (result instanceof AllSpecificationsHoldResult) {
 			// makes no sense in our context, suppress it
 			return null;
+		} else if (result instanceof InvariantResult) {
+			invResult = (InvariantResult<?>) result;
+			// Only want to process location invariants
+			if (invResult.isLoopLocation()) {
+				return result;
+			}
+			oldRes = (AbstractResultAtElement<?>) result;
+			final var check = invResult.getChecks().stream().filter(c -> c instanceof ReqCheck).findFirst();
+			if (check.isEmpty()) {
+				return null;
+			}
+			reqCheck = (ReqCheck) check.get();
+			// Important if other specs receive invariants too,
+			// in order to prevent the results to slip through to
+			// the last return unhandled
+			if (!reqCheck.getSpec().contains(Spec.REDUNDANCY)) {
+				return result;
+			}
+			isPositive = true;
 		} else {
 			return result;
 		}
@@ -187,6 +209,21 @@ public IResult convertTraceAbstractionResult(final IResult result) {
 			final String failurePath = formatTimeSequenceMap(delta2var2value);
 			return new ReqCheckRtInconsistentResult<>(element, plugin, failurePath);
 		}
+
+		// If a loop invariant result is present, transform it into the
+		// new output, rather than a generic ReqCheckFailResult
+		if (spec == Spec.REDUNDANCY && invResult != null) {
+			// Annotation needed for the result to know the respective Check
+			reqCheck.annotate(element);
+			StringBuilder resultString = new StringBuilder("");
+			final String invariant = invResult.getInvariant();
+			final Set<String> redundancySet = ReqCheckRedundancyResult.extractRedundancySet(invariant);
+			// TODO: Apply post-processing to the redundancy set here
+			resultString.append(redundancySet.toString());
+			resultString.append(" derived by location invariant: ");
+			resultString.append(invariant);
+			return new ReqCheckRedundancyResult<>(element, plugin, reqCheck.getReqIds().iterator().next(), resultString.toString());
+		}		
 		return new ReqCheckFailResult<>(element, plugin);
 	}
 

trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckRedundancyResult.java

@@ -0,0 +1,48 @@
+package de.uni_freiburg.informatik.ultimate.pea2boogie.results;
+
+import java.util.HashSet;
+import java.util.Set;
+import java.util.regex.Pattern;
+import java.util.regex.Matcher;
+
+import de.uni_freiburg.informatik.ultimate.core.model.models.IElement;
+
+public class ReqCheckRedundancyResult<LOC extends IElement> extends ReqCheckFailResult<LOC> {
+
+	private String mReqName;
+	private String mRedundancySet;
+
+	public ReqCheckRedundancyResult(LOC element, String plugin, String reqName, String redundancySet) {
+		super(element, plugin);
+		mReqName = reqName;
+		mRedundancySet = redundancySet;
+	}
+
+	@Override
+	public String getLongDescription() {
+		return "Extracted redundancy set for " + mReqName + ": " + mRedundancySet;
+	}
+
+	/*
+	 * Function that parses loop invariants represented by strings. In the terms of the regex,
+	 * we extract every name of the automata appearing inside of the loop invariant.
+	 * TODO: One issue that persist is if a user names the observable of a requirement
+	 * such that it matches the regex (for example: "input FakeReq_ct0_total_pc IS bool").
+	 * For now the method works under the assumption that names created during the formalization process are
+	 * disjoint of the variable names used in the program that simulates the intersection of automata
+	 */
+	public static Set<String> extractRedundancySet(String invariant) {
+		String regex = "[a-zA-Z_]+[a-zA-Z0-9_]*_ct(0|[1-9][0-9]*)[a-zA-Z0-9_]*_total";
+		Pattern pattern = Pattern.compile(regex);
+		Matcher matcher = pattern.matcher(invariant);
+
+		Set<String> redundancySet = new HashSet<>();
+
+		while (matcher.find()) {
+			redundancySet.add(matcher.group().split("_ct")[0]);
+		}
+
+		return redundancySet;
+	}
+
+}