diff --git a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/typechecker/TypeCheckHelper.java b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/typechecker/TypeCheckHelper.java index 30f88fb63af..3ce178ee0d2 100644 --- a/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/typechecker/TypeCheckHelper.java +++ b/trunk/source/Library-BoogieAST/src/de/uni_freiburg/informatik/ultimate/boogie/typechecker/TypeCheckHelper.java @@ -265,6 +265,23 @@ public static BoogieType typeCheckIfThenElseExpression(final BoogieType cond } return resultType; } + + public static BoogieType typeCheckIfThenExpression(final BoogieType condType, final BoogieType left, + final BoogieType right, final ITypeErrorReporter typeErrorReporter) { + BoogieType resultType; + if (!condType.equals(BoogieType.TYPE_ERROR) && !condType.equals(BoogieType.TYPE_BOOL)) { + // typeError(expr, "if expects boolean type: " + expr); + typeErrorReporter.report(exp -> "if expects boolean type: " + exp); + } + if (!left.isUnifiableTo(right)) { + // typeError(expr, "Type check failed for " + expr); + typeErrorReporter.report(exp -> "Type check failed for " + exp); + resultType = BoogieType.TYPE_ERROR; + } else { + resultType = left.equals(BoogieType.TYPE_ERROR) ? right : left; + } + return resultType; + } public static void typeCheckAssignStatement(final String[] lhsIds, final BoogieType[] lhsTypes, final BoogieType[] rhsTypes, final ITypeErrorReporter typeErrorReporter) { diff --git a/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/annotation/Check.java b/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/annotation/Check.java index 5def7bb39e8..5863c56bdfc 100644 --- a/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/annotation/Check.java +++ b/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/annotation/Check.java @@ -145,6 +145,10 @@ public enum Spec { * Check for requirements. Checks for incompleteness. */ INCOMPLETE, + /** + * Check for requirements. Checks for state recoverability. + */ + STATE_RECOVERABILITY, /** * Check if a petrified ICFG does provide enough thread instances. */ @@ -261,6 +265,8 @@ public static String getDefaultPositiveMessage(final Spec spec) { return "consistent"; case INCOMPLETE: return "complete"; + case STATE_RECOVERABILITY: + return "state recoverable"; case SUFFICIENT_THREAD_INSTANCES: return "petrification did provide enough thread instances (tool internal message, not intended for end users)"; case DATA_RACE: @@ -316,6 +322,8 @@ public static String getDefaultNegativeMessage(final Spec spec) { return "inconsistent"; case INCOMPLETE: return "incomplete"; + case STATE_RECOVERABILITY: + return "not recoverable"; case SUFFICIENT_THREAD_INSTANCES: return "petrification did not provide enough thread instances (tool internal message, not intended for end users)"; case DATA_RACE: diff --git a/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java b/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java index 69c322d6062..118bda4d75b 100644 --- a/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java +++ b/trunk/source/Library-UltimateModel/src/de/uni_freiburg/informatik/ultimate/core/model/preferences/UltimatePreferenceItem.java @@ -28,6 +28,8 @@ import java.util.ArrayList; import java.util.List; +import java.util.regex.Matcher; +import java.util.regex.Pattern; import de.uni_freiburg.informatik.ultimate.core.model.IController; @@ -157,6 +159,7 @@ public interface IUltimatePreferenceItemValidator { IntegerValidator ONLY_POSITIVE = new IntegerValidator(0, Integer.MAX_VALUE); IntegerValidator ONLY_POSITIVE_NON_ZERO = new IntegerValidator(1, Integer.MAX_VALUE); IntegerValidator GEQ_TWO = new IntegerValidator(2, Integer.MAX_VALUE); + StringValidator EXPR_PAIR = new StringValidator("\\s{0,1}((\\w+)\\s*([<>=!][=]*)\\s*(\\w+))\\s{0,1}$"); boolean isValid(T value); @@ -203,6 +206,38 @@ public String getInvalidValueErrorMessage(final Double value) { return "Valid range is " + mMin + " <= value <= " + mMax; } } + + public class StringValidator implements IUltimatePreferenceItemValidator { + + private final String mPattern; + + public StringValidator(String pattern) { + mPattern = pattern; + } + + @Override + public boolean isValid(final String string) { + String[] exprPairs = string.split(","); + for (String exprPair : exprPairs) { + Matcher m = match(exprPair, mPattern); + if (!m.matches()) { + return false; + } + } + return true; + } + + @Override + public String getInvalidValueErrorMessage(final String string) { + return "Expression pairs " + string + " is not in the format VALUE, ...>"; + } + } + + default Matcher match(String s, String pattern) { + Pattern p = Pattern.compile(pattern); + Matcher m = p.matcher(s); + return m; + } } } diff --git a/trunk/source/PEAtoBoogie/META-INF/MANIFEST.MF b/trunk/source/PEAtoBoogie/META-INF/MANIFEST.MF index 9de87bad960..501aff82746 100644 --- a/trunk/source/PEAtoBoogie/META-INF/MANIFEST.MF +++ b/trunk/source/PEAtoBoogie/META-INF/MANIFEST.MF @@ -22,5 +22,6 @@ Require-Bundle: com.github.jhoenicke.javacup, de.uni_freiburg.informatik.ultimate.lib.automata Export-Package: de.uni_freiburg.informatik.ultimate.pea2boogie, de.uni_freiburg.informatik.ultimate.pea2boogie.results, + de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability, de.uni_freiburg.informatik.ultimate.pea2boogie.testgen Automatic-Module-Name: de.uni.freiburg.informatik.ultimate.pea2boogie diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java index 6ddd49ed483..caea92c0567 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/IReqSymbolTable.java @@ -35,9 +35,11 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.core.model.models.IBoogieType; import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer; import de.uni_freiburg.informatik.ultimate.util.datastructures.UnionFind; public interface IReqSymbolTable { @@ -66,6 +68,12 @@ public interface IReqSymbolTable { Set getStateVars(); + // Allows you to easily add more elements to the Boogie program at any line without the need to create more + // interface methods. + Set getAuxVars(); + + AuxiliaryStatementContainer getAuxStatementContainer(); + /** * Given a variable name, return the name of the primed version of this variable. */ diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java index 8cedfe3eb2b..9cd78cd665f 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java @@ -15,6 +15,7 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.preferences.Pea2BoogiePreferences; import de.uni_freiburg.informatik.ultimate.pea2boogie.preferences.Pea2BoogiePreferences.PEATransformerMode; import de.uni_freiburg.informatik.ultimate.pea2boogie.testgen.Req2CauseTrackingPeaTransformer; +import de.uni_freiburg.informatik.ultimate.pea2boogie.testgen.Req2ModifySymbolTablePeaTransformer; import de.uni_freiburg.informatik.ultimate.pea2boogie.testgen.ReqTestResultUtil; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.Req2BoogieTranslator; @@ -55,6 +56,10 @@ private IElement generateBoogie(final List> patterns) { if (mode == PEATransformerMode.REQ_CHECK) { return generateReqCheckBoogie(patterns); } + // For checks with additional parameters that must be passed for execution. + if (mode == PEATransformerMode.REQ_PARAM_CHECK) { + return generateReqParamCheckBoogie(patterns); + } if (mode == PEATransformerMode.REQ_TEST) { return generateReqTestBoogie(patterns); } @@ -72,6 +77,22 @@ private IElement generateReqCheckBoogie(final List> patterns) { return translator.getUnit(); } + // For checks with additional parameters that must be passed for execution. + private IElement generateReqParamCheckBoogie(final List> patterns) { + final Req2ModifySymbolTablePeaTransformer transformer = + new Req2ModifySymbolTablePeaTransformer(mServices, mLogger); + + final Req2BoogieTranslator translator = + new Req2BoogieTranslator(mServices, mLogger, patterns, Collections.singletonList(transformer)); + + final VerificationResultTransformer reporter = + new VerificationResultTransformer(mLogger, mServices, translator.getReqSymbolTable()); + // register CEX transformer that removes program executions from CEX. + final UnaryOperator resultTransformer = reporter::convertTraceAbstractionResult; + mServices.getResultService().registerTransformer("CexReducer", resultTransformer); + return translator.getUnit(); + } + private IElement generateReqTestBoogie(final List> patterns) { // TODO: would it be nicer to get the symbol table via annotations? final Req2CauseTrackingPeaTransformer transformer = new Req2CauseTrackingPeaTransformer(mServices, mLogger); 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 c7db9cb43be..a36be049172 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,6 +95,7 @@ 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.ReqCheckRtInconsistentResult; +import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckStateRecoverabilityResult; import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheckSuccessResult; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.Req2BoogieTranslator; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.ReqSymboltableBuilder; @@ -153,7 +154,7 @@ public IResult convertTraceAbstractionResult(final IResult result) { final Spec spec = specs.iterator().next(); dieIfUnsupported(spec); - if (spec == Spec.CONSISTENCY || spec == Spec.VACUOUS) { + if (spec == Spec.CONSISTENCY || spec == Spec.VACUOUS || spec == Spec.STATE_RECOVERABILITY) { // a counterexample for consistency and vacuity means that the requirements are consistent or // non-vacuous isPositive = !isPositive; @@ -189,6 +190,13 @@ public IResult convertTraceAbstractionResult(final IResult result) { final String failurePath = formatTimeSequenceMap(delta2var2value); return new ReqCheckRtInconsistentResult<>(element, plugin, translatorSequence, failurePath); } + + if (spec == Spec.STATE_RECOVERABILITY) { + IBacktranslationService translatorSequenceStRec = oldRes.getCurrentBacktranslation(); + return new ReqCheckStateRecoverabilityResult<>(element, plugin, translatorSequenceStRec, + reqCheck.getMessage()); + } + return new ReqCheckFailResult<>(element, plugin, translatorSequence); } @@ -557,6 +565,7 @@ private static void dieIfUnsupported(final Spec spec) { case CONSISTENCY: case VACUOUS: case RTINCONSISTENT: + case STATE_RECOVERABILITY: return; default: throw new UnsupportedOperationException("Unknown spec type " + spec); diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java index 24452b7dbc4..ef3a579ec42 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/preferences/Pea2BoogiePreferences.java @@ -57,7 +57,6 @@ public class Pea2BoogiePreferences extends UltimatePreferenceInitializer { public static final String LABEL_CHECK_RT_INCONSISTENCY = "Check rt-inconsistency"; private static final boolean DEF_CHECK_RT_INCONSISTENCY = true; private static final String DESC_CHECK_RT_INCONSISTENCY = null; - public static final String LABEL_USE_EPSILON = "Use epsilon transformation during rt-inconsistency check"; private static final boolean DEF_USE_EPSILON = true; private static final String DESC_USE_EPSILON = null; @@ -81,6 +80,18 @@ public class Pea2BoogiePreferences extends UltimatePreferenceInitializer { + " are treated as separate requirements. If enabled, each rt-inconsistency check is of the form " + "Invariants ∧ (check over all remaining requirements). If disabled, invariants are not treated separately."; + public static final String LABEL_CHECK_STATE_RECOVERABILITY = "Check state recoverability"; + private static final boolean DEF_CHECK_STATE_RECOVERABILITY = true; + private static final String DESC_CHECK_STATE_RECOVERABILITY = + "This setting controls whether the property check state-recoverability should be done. " + + "State-recoverability checks for the specified conditions whether it can be recovered from any location in " + + "the phase event automaton. If not, there is an error message for the specified condition."; + + public static final String LABEL_STATE_RECOVERABILITY_VER_EXPR = "State recoverability expressions"; + private static final String DEF_STATE_RECOVERABILITY_VER_EXPR = "ENG_READY==true, ENG_START==false"; + private static final String DESC_STATE_RECOVERABILITY_VER_STRING = + "Enter the expressions for which state recoverability should be valid"; + public static final String LABEL_GUESS_IN_OUT = "Use heuristic to find input/output definitions (if none are given)"; private static final boolean DEF_GUESS_IN_OUT = true; @@ -99,7 +110,7 @@ public class Pea2BoogiePreferences extends UltimatePreferenceInitializer { + "step independend of length or usefulness."; public enum PEATransformerMode { - REQ_CHECK, REQ_TEST + REQ_CHECK, REQ_PARAM_CHECK, REQ_TEST } public Pea2BoogiePreferences() { @@ -110,28 +121,33 @@ public Pea2BoogiePreferences() { protected UltimatePreferenceItem[] initDefaultPreferences() { return new UltimatePreferenceItem[] { - new UltimatePreferenceItem<>(LABEL_TRANSFOMER_MODE, TRANSFOMER_MODE, DESC_TRANSFOMER_MODE, - PreferenceType.Combo, PEATransformerMode.values()), - new UltimatePreferenceItem<>(LABEL_CHECK_VACUITY, DEF_CHECK_VACUITY, DESC_CHECK_VACUITY, - PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_CHECK_CONSISTENCY, DEF_CHECK_CONSISTENCY, DESC_CHECK_CONSISTENCY, - PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_CHECK_RT_INCONSISTENCY, DEF_CHECK_RT_INCONSISTENCY, - DESC_CHECK_RT_INCONSISTENCY, PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_USE_EPSILON, DEF_USE_EPSILON, DESC_USE_EPSILON, - PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_REPORT_TRIVIAL_RT_CONSISTENCY, DEF_REPORT_TRIVIAL_RT_CONSISTENCY, - DESC_REPORT_TRIVIAL_RT_CONSISTENCY, PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_RT_INCONSISTENCY_RANGE, DEF_RT_INCONSISTENCY_RANGE, - DESC_RT_INCONSISTENCY_RANGE, PreferenceType.Integer, - IUltimatePreferenceItemValidator.ONLY_POSITIVE), - new UltimatePreferenceItem<>(LABEL_RT_INCONSISTENCY_USE_ALL_INVARIANTS, - DEF_RT_INCONSISTENCY_USE_ALL_INVARIANTS, DESC_RT_INCONSISTENCY_USE_ALL_INVARIANTS, - PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_GUESS_IN_OUT, DEF_GUESS_IN_OUT, DESC_GUESS_IN_OUT, - PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_GUESS_INITIAL, DEF_GUESS_INITIAL, DESC_GUESS_INITIAL, - PreferenceType.Boolean) }; + new UltimatePreferenceItem<>(LABEL_TRANSFOMER_MODE, TRANSFOMER_MODE, DESC_TRANSFOMER_MODE, + PreferenceType.Combo, PEATransformerMode.values()), + new UltimatePreferenceItem<>(LABEL_CHECK_VACUITY, DEF_CHECK_VACUITY, DESC_CHECK_VACUITY, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_CHECK_CONSISTENCY, DEF_CHECK_CONSISTENCY, DESC_CHECK_CONSISTENCY, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_CHECK_RT_INCONSISTENCY, DEF_CHECK_RT_INCONSISTENCY, + DESC_CHECK_RT_INCONSISTENCY, PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_USE_EPSILON, DEF_USE_EPSILON, DESC_USE_EPSILON, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_REPORT_TRIVIAL_RT_CONSISTENCY, DEF_REPORT_TRIVIAL_RT_CONSISTENCY, + DESC_REPORT_TRIVIAL_RT_CONSISTENCY, PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_RT_INCONSISTENCY_RANGE, DEF_RT_INCONSISTENCY_RANGE, + DESC_RT_INCONSISTENCY_RANGE, PreferenceType.Integer, + IUltimatePreferenceItemValidator.ONLY_POSITIVE), + new UltimatePreferenceItem<>(LABEL_RT_INCONSISTENCY_USE_ALL_INVARIANTS, + DEF_RT_INCONSISTENCY_USE_ALL_INVARIANTS, DESC_RT_INCONSISTENCY_USE_ALL_INVARIANTS, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_CHECK_STATE_RECOVERABILITY, DEF_CHECK_STATE_RECOVERABILITY, + DESC_CHECK_STATE_RECOVERABILITY, PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_STATE_RECOVERABILITY_VER_EXPR, DEF_STATE_RECOVERABILITY_VER_EXPR, + DESC_STATE_RECOVERABILITY_VER_STRING, PreferenceType.String, + IUltimatePreferenceItemValidator.EXPR_PAIR), + new UltimatePreferenceItem<>(LABEL_GUESS_IN_OUT, DEF_GUESS_IN_OUT, DESC_GUESS_IN_OUT, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_GUESS_INITIAL, DEF_GUESS_INITIAL, DESC_GUESS_INITIAL, + PreferenceType.Boolean) }; } public static IPreferenceProvider getPreferenceProvider(final IUltimateServiceProvider services) { 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 89e5190ee98..97ff8b464b0 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 @@ -31,6 +31,8 @@ import java.util.Collections; import java.util.Iterator; import java.util.List; +import java.util.Map; +import java.util.Optional; import java.util.Map.Entry; import java.util.Set; import java.util.concurrent.TimeUnit; @@ -47,6 +49,10 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.IntegerLiteral; import de.uni_freiburg.informatik.ultimate.boogie.ast.NamedAttribute; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.UnaryExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.RunningTaskInfo; import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.ToolchainCanceledException; import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.Check; @@ -60,6 +66,7 @@ import de.uni_freiburg.informatik.ultimate.lib.pea.Phase; import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseBits; import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.pea.modelchecking.DotWriterNew; import de.uni_freiburg.informatik.ultimate.lib.srparse.Durations; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType.ReqPeas; @@ -70,6 +77,11 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.generator.RtInconcistencyConditionGenerator.InvariantInfeasibleException; import de.uni_freiburg.informatik.ultimate.pea2boogie.preferences.Pea2BoogiePreferences; import de.uni_freiburg.informatik.ultimate.pea2boogie.results.ReqCheck; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.PeaPhaseProgramCounter; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxiliaryStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityGenerator; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityVerificationCondition; import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.CheckedReqLocation; import de.uni_freiburg.informatik.ultimate.util.CoreUtil; import de.uni_freiburg.informatik.ultimate.util.datastructures.CrossProducts; @@ -84,6 +96,7 @@ public class ReqCheckAnnotator implements IReq2PeaAnnotator { private static final boolean DEBUG_ONLY_FIRST_NON_TRIVIAL_RT_INCONSISTENCY = false; + private static final boolean PRINT_PEA_DOT = false; private final ILogger mLogger; private final IUltimateServiceProvider mServices; @@ -94,6 +107,7 @@ public class ReqCheckAnnotator implements IReq2PeaAnnotator { private int mCombinationNum; private boolean mCheckConsistency; private boolean mReportTrivialConsistency; + private boolean mCheckStateRecoverability; private boolean mSeparateInvariantHandling; private RtInconcistencyConditionGenerator mRtInconcistencyConditionGenerator; @@ -134,6 +148,8 @@ public List getStateChecks() { mReportTrivialConsistency = prefs.getBoolean(Pea2BoogiePreferences.LABEL_REPORT_TRIVIAL_RT_CONSISTENCY); mSeparateInvariantHandling = prefs.getBoolean(Pea2BoogiePreferences.LABEL_RT_INCONSISTENCY_USE_ALL_INVARIANTS); + mCheckStateRecoverability = prefs.getBoolean(Pea2BoogiePreferences.LABEL_CHECK_STATE_RECOVERABILITY); + // log preferences mLogger.info(String.format("%s=%s, %s=%s, %s=%s, %s=%s, %s=%s", Pea2BoogiePreferences.LABEL_CHECK_VACUITY, mCheckVacuity, Pea2BoogiePreferences.LABEL_RT_INCONSISTENCY_RANGE, mCombinationNum, @@ -171,8 +187,44 @@ private List generateAnnotations() { annotations.addAll(genChecksNonVacuity(mUnitLocation)); } annotations.addAll(genChecksRTInconsistency(mUnitLocation)); + if(mCheckStateRecoverability) { + annotations.addAll(genCheckStateRecoverability(mUnitLocation)); + } + return annotations; } + + private List genCheckStateRecoverability(final BoogieLocation bl) { + List statements = new ArrayList<>(); + StateRecoverabilityGenerator stateRecoverabilityGenerator = new StateRecoverabilityGenerator(); + AuxiliaryStatementContainer auxStatementContainer = mSymbolTable.getAuxStatementContainer(); + Map>> vePeaAuxStatementMap = stateRecoverabilityGenerator.getAuxStatementPerVerificationExpression(auxStatementContainer); + + for(Map.Entry>> entry : vePeaAuxStatementMap.entrySet()) { + StateRecoverabilityVerificationCondition ve = entry.getKey(); + + for(Map.Entry> entryPeaStRecAuxSt : entry.getValue().entrySet()) { + Set stRecAuxStSet = entryPeaStRecAuxSt.getValue(); + for(StateRecoverabilityAuxiliaryStatement stRecAuxSt : stRecAuxStSet) { + String checkLabel = "STATE_RECOVERABILITY_" + entry.getKey().getVariable() + "_" + stRecAuxSt.getPcVariable(); + + Expression globalVariableTrue = stateRecoverabilityGenerator.createExpression(bl, BoogieType.TYPE_BOOL, stRecAuxSt.getRelatedVariable(), Operator.COMPEQ, "true"); + Expression inputCondition = stateRecoverabilityGenerator.createExpression(bl, BoogiePrimitiveType.toPrimitiveType(ve.getDataType()), ve.getVariable(), ve.getOperator(), ve.getValue()); + Expression andCondition = ExpressionFactory.newBinaryExpression(bl, Operator.LOGICAND, globalVariableTrue, inputCondition); + Expression expr = ExpressionFactory.constructUnaryExpression(bl, UnaryExpression.Operator.LOGICNEG, andCondition); + + final ReqCheck check = createReqCheck(Spec.STATE_RECOVERABILITY, stRecAuxSt.getPeaPhasePc().getReq(), entryPeaStRecAuxSt.getKey(), String.join("", ve.getVerificationConditionString())); + statements .add(createAssert(expr, check, checkLabel)); } + } + } + + //Prints parallel automaton + if(PRINT_PEA_DOT) { + dotPrinter(mReqPeas); + } + + return statements ; + } private static List genCheckConsistency(final BoogieLocation bl) { final ReqCheck check = new ReqCheck(Spec.CONSISTENCY); @@ -255,7 +307,7 @@ private Statement genAssertRTInconsistency(final Entry, PhaseEven final PhaseEventAutomata[] automata = automataSet.toArray(new PhaseEventAutomata[subset.length]); final Expression expr = mRtInconcistencyConditionGenerator.generateNonDeadlockCondition(automata); - final ReqCheck check = createReqCheck(Spec.RTINCONSISTENT, subset); + final ReqCheck check = createReqCheck(Spec.RTINCONSISTENT, "", subset); if (expr == null) { if (mReportTrivialConsistency) { @@ -366,7 +418,7 @@ private Statement genAssertNonVacuous(final PatternType req, final PhaseEvent } @SafeVarargs - private static ReqCheck createReqCheck(final Check.Spec reqSpec, + private static ReqCheck createReqCheck(final Check.Spec reqSpec, final String message, final Entry, PhaseEventAutomata>... req2pea) { if (req2pea == null || req2pea.length == 0) { throw new IllegalArgumentException("subset cannot be null or empty"); @@ -379,11 +431,15 @@ private static ReqCheck createReqCheck(final Check.Spec reqSpec, peaNames[i] = req2pea[i].getValue().getName(); } - return new ReqCheck(reqSpec, reqIds, peaNames); + return new ReqCheck(reqSpec, reqIds, peaNames, message); } + private static ReqCheck createReqCheck(final Spec spec, final PatternType req, final PhaseEventAutomata aut, String message) { + return createReqCheck(spec, message, new Pair<>(req, aut)); + } + private static ReqCheck createReqCheck(final Spec spec, final PatternType req, final PhaseEventAutomata aut) { - return createReqCheck(spec, new Pair<>(req, aut)); + return createReqCheck(spec, "", new Pair<>(req, aut)); } /** @@ -412,6 +468,40 @@ private Expression genComparePhaseCounter(final int phaseIndex, final String pcN final IntegerLiteral intLiteral = ExpressionFactory.createIntegerLiteral(bl, Integer.toString(phaseIndex)); return ExpressionFactory.newBinaryExpression(bl, BinaryExpression.Operator.COMPEQ, identifier, intLiteral); } + + private void dotPrinter(List reqPeas) { + final List, PhaseEventAutomata>> counterTracePEAList = new ArrayList<>(); + for (final ReqPeas reqPea : reqPeas) { + final PatternType pattern = reqPea.getPattern(); + + for (final Entry pea : reqPea.getCounterTrace2Pea()) { + counterTracePEAList.add(new Pair<>(pattern, pea.getValue())); + } + } + final List, PhaseEventAutomata>[]> subsets = CrossProducts.subArrays(counterTracePEAList.toArray(new Entry[counterTracePEAList.size()]), counterTracePEAList.size(), new Entry[counterTracePEAList.size()]); + + for(final Entry, PhaseEventAutomata>[] subset : subsets) { + + final Set automataSet = Arrays.stream(subset).map(Entry, PhaseEventAutomata>::getValue).collect(Collectors.toSet()); + assert automataSet.size() == subset.length; + final PhaseEventAutomata[] automata = automataSet.toArray(new PhaseEventAutomata[subset.length]); + + mLogger.info("### Printing DOT for Peas ###"); + for (int i = 0; i < automata.length; ++i) { + final PhaseEventAutomata pea = automata[i]; + mLogger.info(pea.getName() + CoreUtil.getPlatformLineSeparator() + DotWriterNew.createDotString(pea)); + } + if (automata.length < 8) { + final Optional prod = Arrays.stream(automata).reduce(PhaseEventAutomata::parallel); + if (prod.isPresent()) { + mLogger.info( + "PRODUCT" + CoreUtil.getPlatformLineSeparator() + DotWriterNew.createDotString(prod.get())); + } + } + mLogger.info("### Finished printing DOT ###"); + } + + } @Override public List getPreChecks() { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java index a3d8aa03630..643f1b16ff0 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheck.java @@ -53,27 +53,34 @@ public class ReqCheck extends Check { private final String[] mReqIds; private final String[] mPeaNames; + + private final String mMessage; public ReqCheck(final Check.Spec type) { - this(EnumSet.of(type), 0, 0, new String[0], new String[0]); + this(EnumSet.of(type), 0, 0, new String[0], new String[0], ""); } + public ReqCheck(final Check.Spec type, final String[] reqIds, final String[] peaNames, String message) { + this(EnumSet.of(type), reqIds, peaNames, message); + } + public ReqCheck(final Check.Spec type, final String[] reqIds, final String[] peaNames) { - this(EnumSet.of(type), reqIds, peaNames); + this(EnumSet.of(type), reqIds, peaNames, ""); } - private ReqCheck(final EnumSet types, final String[] reqIds, final String[] peaNames) { - this(types, -1, -1, reqIds, peaNames); + private ReqCheck(final EnumSet types, final String[] reqIds, final String[] peaNames, String message) { + this(types, -1, -1, reqIds, peaNames, message); } private ReqCheck(final EnumSet types, final int startline, final int endline, final String[] reqIds, - final String[] peaNames) { + final String[] peaNames, String message) { super(types, a -> ReqCheck.getCustomPositiveMessage(a, reqIds, peaNames), a -> ReqCheck.getCustomNegativeMessage(a, reqIds, peaNames)); mStartline = startline; mEndline = endline; mReqIds = reqIds; mPeaNames = peaNames; + mMessage = message; } public int getStartLine() { @@ -128,7 +135,8 @@ public ReqCheck merge(final ReqCheck other) { final int endline = Math.max(mEndline, other.mEndline); final String[] reqIds = DataStructureUtils.concat(mReqIds, other.mReqIds); final String[] peaNames = DataStructureUtils.concat(mPeaNames, other.mPeaNames); - return new ReqCheck(newSpec, startline, endline, reqIds, peaNames); + final String message = mMessage.concat(other.getMessage()); + return new ReqCheck(newSpec, startline, endline, reqIds, peaNames, message); } public Set getReqIds() { @@ -138,13 +146,21 @@ public Set getReqIds() { public Set getPeaNames() { return new LinkedHashSet<>(Arrays.asList(mPeaNames)); } + + public String getMessage( ) { + return mMessage; + } @Override public String toString() { if (mReqIds.length == 0) { return super.toString() + " for all requirements"; } - return super.toString() + " for " + Arrays.stream(mReqIds).collect(Collectors.joining(", ")); + if(mMessage.isEmpty()) { + return super.toString() + " for " + Arrays.stream(mReqIds).collect(Collectors.joining(", ")); + } else { + return super.toString() + " for " + Arrays.stream(mReqIds).collect(Collectors.joining(", ")) + " " + mMessage; + } } @Override @@ -154,6 +170,7 @@ public int hashCode() { result = prime * result + mEndline; result = prime * result + Arrays.hashCode(mReqIds); result = prime * result + Arrays.hashCode(mPeaNames); + result = prime * result + mMessage.hashCode(); result = prime * result + mStartline; return result; } @@ -182,6 +199,9 @@ public boolean equals(final Object obj) { if (!Arrays.equals(mPeaNames, other.mPeaNames)) { return false; } + if(!mMessage.equals(other.getMessage())) { + return false; + } return true; } diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java new file mode 100644 index 00000000000..c6d2682a617 --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/results/ReqCheckStateRecoverabilityResult.java @@ -0,0 +1,60 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 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.core.model.services.IBacktranslationService; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction; +import de.uni_freiburg.informatik.ultimate.util.CoreUtil; + +/** +* +* @author Tobias Wießner +* +*/ + +public class ReqCheckStateRecoverabilityResult extends ReqCheckFailResult{ + + private final String mMessage; + + public ReqCheckStateRecoverabilityResult(final LOC element, final String plugin, final IBacktranslationService translatorSequence, final String message) { + super(element, plugin, translatorSequence); + mMessage = message; + } + + @Override + public String getLongDescription() { + final StringBuilder sb = new StringBuilder(); + sb.append(getShortDescription()); + sb.append(CoreUtil.getPlatformLineSeparator()); + if (mMessage != null) { + sb.append("Verification Condition: "); + sb.append(mMessage); + } + return sb.toString(); + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java new file mode 100644 index 00000000000..db1844b0473 --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatement.java @@ -0,0 +1,54 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 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.staterecoverability; + +import java.util.ArrayList; +import java.util.List; + +import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2Pea; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; + +/** +* +* Interface for a class containing a statement to be inserted at a certain line in the Boogie program. +* +* @author Tobias Wießner +* +*/ + +public interface AuxiliaryStatement { + + public Statement getStatement(StatementAssignment stRecExpr); + + public BoogieLocation setBoogieLocation(BoogieLocation loc); + + public BoogieLocation getBoogieLocation(); +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatementContainer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatementContainer.java new file mode 100644 index 00000000000..2e79702125f --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/AuxiliaryStatementContainer.java @@ -0,0 +1,120 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 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.staterecoverability; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; + +/** +* +* @author Tobias Wießner +* +*/ + +public class AuxiliaryStatementContainer { + public enum StatementAssignment { + DECL_VAR, ASSIGN_VAR, IF_ST; + } + + private Map mStatementMap; + private Set statements; + + public AuxiliaryStatementContainer() { + mStatementMap = new HashMap<>(); + } + + public AuxiliaryStatementContainer(AuxiliaryStatementContainer auxStatement) { + mStatementMap = auxStatement.getSreMap(); + } + + public List getStatements(StatementAssignment stRecExpr) { + List statList = new ArrayList<>(); + for(AuxiliaryStatement auxStatement : mStatementMap.values()) { + Statement s = auxStatement.getStatement(stRecExpr); + if(s != null) { + statList.add(s); + } + } + return statList; + } + + public Set getRelatedVariableForInstance(Object object) { + Set relatedVariables = new HashSet<>(); + for(Map.Entry entry : mStatementMap.entrySet()) { + if(entry.getValue().getClass().getName().equals(object.getClass().getName())) { + relatedVariables.add(entry.getKey()); + } + } + return relatedVariables; + } + + public Set setBoogieLocationForInstance(Object object, StatementAssignment stRecExpr, final BoogieLocation bl) { + Set statements = new HashSet<>(); + for(Map.Entry entry : mStatementMap.entrySet()) { + if(entry.getValue().getClass().getName().equals(object.getClass().getName())) { + Statement statement = entry.getValue().getStatement(stRecExpr); + if(statement != null) { + statement.setLoc(bl); + } + statements.add(statement); + } + } + return statements; + } + + public AuxiliaryStatement addAuxStatement(String variable, AuxiliaryStatement auxStatement) { + if(mStatementMap == null) { + mStatementMap = new HashMap<>(); + } + mStatementMap.put(variable, auxStatement); + return auxStatement; + } + + public Map getSreMap() { + return mStatementMap; + } + + public void setSreMap(Map sreMap) { + this.mStatementMap = sreMap; + } + + public Set getStatements() { + return statements; + } + + public void setStatements(Set statements) { + this.statements = statements; + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java new file mode 100644 index 00000000000..8fe05afa59d --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/PeaPhaseProgramCounter.java @@ -0,0 +1,91 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 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.staterecoverability; + +import java.util.Collection; +import java.util.Iterator; +import java.util.Map; +import java.util.Set; + +import de.uni_freiburg.informatik.ultimate.lib.pea.Phase; +import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; + +/** +* +* @author Tobias Wießner +* +*/ + +public class PeaPhaseProgramCounter { + + private final int pc; + private final Phase phase; + private final PhaseEventAutomata pea; + private final PatternType req; + + public PeaPhaseProgramCounter(final int pc, final Phase phase, final PhaseEventAutomata pea, final PatternType req) { + super(); + this.pc = pc; + this.phase = phase; + this.pea = pea; + this.req = req; + } + + @Override + public int hashCode() { + return phase.getName().hashCode(); + } + + @Override + public boolean equals(Object o) { + if(this == o) { + return true; + } + if(o instanceof Phase) { + Phase oPhase = (Phase) o; + return phase.getName().equals(oPhase.getName()); + } + return false; + } + + public int getPc() { + return pc; + } + + public Phase getPhase() { + return phase; + } + + public PhaseEventAutomata getPea() { + return pea; + } + + public PatternType getReq() { + return req; + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java new file mode 100644 index 00000000000..ac2e74b015f --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityAuxiliaryStatement.java @@ -0,0 +1,156 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 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.staterecoverability; + +import java.util.ArrayList; +import java.util.List; + +import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; + +/** +* +* @author Tobias Wießner +* +*/ + +public class StateRecoverabilityAuxiliaryStatement implements AuxiliaryStatement { + + private PeaPhaseProgramCounter peaPhasePc; + private String relatedVariable; + private BoogieLocation loc; + private String pcVariable; + private int pc; + private StateRecoverabilityVerificationCondition verificationExpression; + private Statement declVar; + private Statement assignVar; + private Statement ifSt; + + public StateRecoverabilityAuxiliaryStatement(String variable) { + this.relatedVariable = variable; + } + + public StateRecoverabilityAuxiliaryStatement(PeaPhaseProgramCounter peaPhasePc, String variable, String pcVariable, int pc, StateRecoverabilityVerificationCondition ve) { + this.peaPhasePc = peaPhasePc; + this.relatedVariable = variable; + this.pcVariable = pcVariable; + this.pc = pc; + this.verificationExpression = ve; + } + + @Override + public Statement getStatement(StatementAssignment stRecExpr) { + Statement s = null; + switch (stRecExpr) { + case DECL_VAR: + return this.getDeclVar(); + case ASSIGN_VAR: + return this.getAssignVar(); + case IF_ST: + return this.getIfSt(); + default: + break; + } + return null; + } + + public String getRelatedVariable() { + return relatedVariable; + } + + public void setRelatedVariable(String relatedVariable) { + this.relatedVariable = relatedVariable; + } + + public String getPcVariable() { + return pcVariable; + } + + public void setPcVariable(String pcVariable) { + this.pcVariable = pcVariable; + } + + public int getPc() { + return pc; + } + + public void setPc(int pc) { + this.pc = pc; + } + + public StateRecoverabilityVerificationCondition getVerificationExpression() { + return verificationExpression; + } + + public void setVerificationExpression(StateRecoverabilityVerificationCondition verificationExpression) { + this.verificationExpression = verificationExpression; + } + + public Statement getDeclVar() { + return declVar; + } + + public void setDeclVar(Statement declVar) { + this.declVar = declVar; + } + + public Statement getAssignVar() { + return assignVar; + } + + public void setAssignVar(Statement assignVar) { + this.assignVar = assignVar; + } + + public Statement getIfSt() { + return ifSt; + } + + public void setIfSt(Statement ifSt) { + this.ifSt = ifSt; + } + + public PeaPhaseProgramCounter getPeaPhasePc() { + return peaPhasePc; + } + + public void setPeaPhasePc(PeaPhaseProgramCounter peaPhasePc) { + this.peaPhasePc = peaPhasePc; + } + + @Override + public BoogieLocation setBoogieLocation(BoogieLocation loc) { + this.loc = loc; + return loc; + } + + @Override + public BoogieLocation getBoogieLocation() { + return this.loc; + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java new file mode 100644 index 00000000000..f48d5f2272a --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityGenerator.java @@ -0,0 +1,467 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 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.staterecoverability; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.function.UnaryOperator; +import java.util.stream.Collector; +import java.util.stream.Collectors; +import java.util.Set; + +import javax.management.RuntimeErrorException; + +import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation; +import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; +import de.uni_freiburg.informatik.ultimate.boogie.ast.AssignmentStatement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IntegerLiteral; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.DefaultLocation; +import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; +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.core.model.services.ILogger.LogLevel; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Boogie2SMT; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.BoogieDeclarations; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramNonOldVar; +import de.uni_freiburg.informatik.ultimate.lib.pea.BoogieBooleanExpressionDecision; +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.Phase; +import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.pea.Transition; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtSortUtils; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder.ExternalSolver; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder.SolverMode; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder.SolverSettings; +import de.uni_freiburg.informatik.ultimate.lib.srparse.Durations; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType.ReqPeas; +import de.uni_freiburg.informatik.ultimate.logic.Logics; +import de.uni_freiburg.informatik.ultimate.logic.Script; +import de.uni_freiburg.informatik.ultimate.logic.Sort; +import de.uni_freiburg.informatik.ultimate.logic.Script.LBool; +import de.uni_freiburg.informatik.ultimate.logic.Term; +import de.uni_freiburg.informatik.ultimate.logic.TermVariable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.CddToSmt; +import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.PeaResultUtil; +import de.uni_freiburg.informatik.ultimate.pea2boogie.generator.RtInconcistencyConditionGenerator; +import de.uni_freiburg.informatik.ultimate.smtinterpol.DefaultLogger; +import de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap; +import de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol; +import de.uni_freiburg.informatik.ultimate.util.ConstructionCache; + +/** + * + * @author Tobias Wießner + * + */ + +public class StateRecoverabilityGenerator { + + private IReqSymbolTable mReqSymboltable; + private Term mPrimedInvariant; + private Script mScript; + private ManagedScript mManagedScript; + private Boogie2SMT mBoogie2Smt; + private Map mVars; + private IUltimateServiceProvider mServices; + private ILogger mLogger; + private CddToSmt mCddToSmt; + private PeaResultUtil mPeaResultUtil; + private BoogieDeclarations boogieDeclarations; + + private ConstructionCache mPossibleStartLocations; + + public StateRecoverabilityGenerator() { + } + + public StateRecoverabilityGenerator(final ILogger logger, final IUltimateServiceProvider services, + final IReqSymbolTable symboltable) { + mReqSymboltable = symboltable; + mServices = services; + mLogger = logger; + + mPeaResultUtil = new PeaResultUtil(mLogger, mServices); + mScript = buildSolver(services); + mManagedScript = new ManagedScript(services, mScript); + + boogieDeclarations = new BoogieDeclarations(mReqSymboltable.getDeclarations(), mLogger); + mBoogie2Smt = new Boogie2SMT(mManagedScript, boogieDeclarations, services, false); + mVars = mBoogie2Smt.getBoogie2SmtSymbolTable().getGlobalsMap(); + + mPossibleStartLocations = new ConstructionCache<>(this::constructSearchStartLocationTerm); + mCddToSmt = new CddToSmt(mServices, mPeaResultUtil, mScript, mBoogie2Smt, boogieDeclarations, mReqSymboltable); + } + + public Map> getRelevantLocationsFromPea( + List reqPeasList, StateRecoverabilityVerificationConditionContainer vec) { + Map> veLocation = new HashMap<>(); + Set reqPeasSet = new HashSet<>(reqPeasList); + Set declaredConstants = new HashSet<>(); + Map> termPerPhase = new HashMap<>(); + + // Create Terms for every location + for (ReqPeas reqPeas : reqPeasList) { + List> ctPeaList = reqPeas.getCounterTrace2Pea(); + + for(Entry entry : ctPeaList) { + PhaseEventAutomata pea = entry.getValue(); + Phase[] phases = pea.getPhases(); + for (int i = 0; i < phases.length; ++i) { + Phase phase = phases[i]; + CDD invariantPhaseGuardCDD = phase.getStateInvariant().and(phase.getClockInvariant()); + Term parallelAutomaton = generateParallelAutomatonTerm(removeReqPeas(reqPeasSet, reqPeas), invariantPhaseGuardCDD); + + if(!termPerPhase.containsKey(reqPeas)) { + termPerPhase.put(reqPeas, new HashMap<>()); + } + termPerPhase.get(reqPeas).put(phase, parallelAutomaton); + } + } + } + + for (ReqPeas reqPea : reqPeasList) { + List> ctPeaList = reqPea.getCounterTrace2Pea(); + PatternType req = reqPea.getPattern(); + for (Entry entry : ctPeaList) { + Phase[] phases = entry.getValue().getPhases(); + for (int i = 0; i < phases.length; ++i) { + Phase phase = phases[i]; + // Check for every phase if the location can fulfill the verification expression + // TRUE -> Do not add the phase + // FALSE -> Add the phase + for (StateRecoverabilityVerificationCondition ve : vec.getVerificationExpressions().values()) { + CDD verificationConditionCcd = BoogieBooleanExpressionDecision.create(ExpressionFactory.constructUnaryExpression( + ve.getVerificationConditionExpression().getLoc(), + de.uni_freiburg.informatik.ultimate.boogie.ast.UnaryExpression.Operator.LOGICNEG, + ve.getVerificationConditionExpression())); + List invariantVeList = new ArrayList<>(); + + // Compute phase invariant ⋀ opposite verification expression + final Term termVe = mCddToSmt.toSmt(verificationConditionCcd); + invariantVeList.add(termVe); + final Term termLocation = mCddToSmt.toSmt(phase.getStateInvariant()); + invariantVeList.add(termLocation); + + // Find satisfiable model + final Term termModel = SmtUtils.and(mScript, invariantVeList); + + if (SmtUtils.checkSatTerm(mScript, termModel) == LBool.SAT) { + if (!veLocation.containsKey(ve)) { + veLocation.put(ve, new HashSet<>()); + } + + //Term possibleStartPhase = + //possibleStartPhase(phase, reqPea, reqPeasTerm.get(reqPea), termVe); + Term possibleStartPhase = + possibleStartPhase(phase, reqPea, termPerPhase.get(reqPea).get(phase), termVe); + // Declare constants for Z3 + declareConstants(mScript, possibleStartPhase, declaredConstants); + + if (SmtUtils.checkSatTerm(mScript, possibleStartPhase) == LBool.SAT) { + veLocation.get(ve).add(new PeaPhaseProgramCounter(i, phase, entry.getValue(), req)); + } + } + } + } + } + } + return veLocation; + } + + private void declareConstants(Script script, Term term, Set declaredConstants) { + Sort sort = term.getSort(); + TermVariable[] termVariables = term.getFreeVars(); + for (int i = 0; i < termVariables.length; ++i) { + // mScript.declareFun("ENG_READY", new Sort[0], sort); + TermVariable termVariable = termVariables[i]; + if (!declaredConstants.contains(termVariable.getName())) { + script.declareFun(termVariable.getName(), new Sort[0], sort); + declaredConstants.add(termVariable.getName()); + } + } + } + + private Term possibleStartPhase(Phase phase, ReqPeas reqPeas, Term parallelAutomaton, Term termVe) { + Term actualTerm = generatePhaseTerm(phase); + Term[] terms = new Term[] { actualTerm, parallelAutomaton, termVe }; + + final Term finalTerm = termAnd(terms); + return finalTerm; + } + + private Term termAnd(Term[] terms) { + final Term term = SmtUtils.and(mScript, terms); + return term; + } + + private Term generatePhaseTerm(Phase phase) { + final Term term = mCddToSmt.toSmt(phase.getStateInvariant()); + return term; + } + + private Set removeReqPeas(Set reqPeasSet, ReqPeas reqPeas) { + Set newReqPeasSet = new HashSet<>(reqPeasSet); + newReqPeasSet.remove(reqPeas); + return newReqPeasSet; + } + + /** + * Computes VE && (A_1 && A_2 && A_n && ...) + * + * A = ((p_1 && (g_1 || g_n)) || (p_2 && (g_n)) || ...) + * + * @param reqPeas + * @return term + */ + private Term generateParallelAutomatonTerm(Set reqPeas, CDD currentReqLocationCDD) { + Map reqPeasPeaArrayMap = createPeaArray(reqPeas); + CDD reqsCDD = null; + for (Map.Entry entry : reqPeasPeaArrayMap.entrySet()) { + + // Automatons per requirement + CDD peasCDD = null; + PhaseEventAutomata[] peaArray = entry.getValue(); + for (PhaseEventAutomata pea : peaArray) { + Phase[] phases = pea.getPhases(); + + // Create CDD for every location and guard + CDD[] invariantPhaseGuardArrayPerPea = new CDD[pea.getPhases().length]; + for (int i = 0; i < invariantPhaseGuardArrayPerPea.length; ++i) { + Phase phase = phases[i]; + CDD invariantPhaseGuardCDD = phase.getStateInvariant().and(phase.getClockInvariant()); + invariantPhaseGuardArrayPerPea[i] = invariantPhaseGuardCDD; + } + + // Link every location invariant-guard CDD with OR + CDD peaCDD = null; + for (int i = 0; i < invariantPhaseGuardArrayPerPea.length; ++i) { + if (peaCDD == null) { + peaCDD = invariantPhaseGuardArrayPerPea[i]; + } + peaCDD.or(invariantPhaseGuardArrayPerPea[i]); + } + + // Link every pea with AND + if (peasCDD == null) { + peasCDD = peaCDD; + } else { + peasCDD.and(peaCDD); + } + } + // Link every req with AND + if (reqsCDD == null) { + reqsCDD = peasCDD; + } else { + reqsCDD.and(peasCDD); + } + } + // Attaches the current req location CDD to the CDDs of all other requirements + if(reqsCDD != null) { + reqsCDD.and(currentReqLocationCDD); + } else { + reqsCDD = currentReqLocationCDD; + } + // Check for Null in case there is no start location, then deliver a false condition + Term term; + if(reqsCDD != null) { + term = mCddToSmt.toSmt(reqsCDD); + } else { + term = mCddToSmt.toSmt(CDD.FALSE); + } + return term; + } + + private Map createPeaArray(Set reqPeas) { + Map reqPeasPeaArrayMap = new HashMap<>(); + for (ReqPeas reqPea : reqPeas) { + List> ctPeaList = reqPea.getCounterTrace2Pea(); + Set automataSet = ctPeaList.stream() + .map(Entry::getValue).collect(Collectors.toSet()); + final PhaseEventAutomata[] automata = automataSet.toArray(new PhaseEventAutomata[automataSet.size()]); + reqPeasPeaArrayMap.put(reqPea, automata); + } + return reqPeasPeaArrayMap; + } + + private Term constructSearchStartLocationTerm(Phase phase) { + return transformAndLog(phase.getStateInvariant(), "phase invariant"); + } + + private Term transformAndLog(final CDD org, final String msg) { + final Term term = mCddToSmt.toSmt(org); + mLogger.info("Can be start location %s %s", msg, org.toGeneralString()); + return term; + } + + private static Script buildSolver(final IUltimateServiceProvider services) throws AssertionError { + SolverSettings settings = SolverBuilder.constructSolverSettings() + // .setSolverMode(SolverMode.External_ModelsAndUnsatCoreMode).setUseExternalSolver(ExternalSolver.Z3); + .setSolverMode(SolverMode.External_ModelsMode).setUseExternalSolver(ExternalSolver.Z3); + return SolverBuilder.buildAndInitializeSolver(services, settings, "RtInconsistencySolver"); + } + + public Map>> + getAuxStatementPerVerificationExpression(AuxiliaryStatementContainer auxStatementContainer) { + Map>> vePeaAuxStatementMap = + new HashMap<>(); + for (AuxiliaryStatement auxStatement : auxStatementContainer.getSreMap().values()) { + if (auxStatement instanceof StateRecoverabilityAuxiliaryStatement) { + StateRecoverabilityAuxiliaryStatement stRecAuxSt = (StateRecoverabilityAuxiliaryStatement) auxStatement; + if (!vePeaAuxStatementMap.containsKey(stRecAuxSt.getVerificationExpression())) { + vePeaAuxStatementMap.put(stRecAuxSt.getVerificationExpression(), new HashMap<>()); + } + Map> peaAuxStatementMap = + vePeaAuxStatementMap.get(stRecAuxSt.getVerificationExpression()); + if (!peaAuxStatementMap.containsKey(stRecAuxSt.getPeaPhasePc().getPea())) { + peaAuxStatementMap.put(stRecAuxSt.getPeaPhasePc().getPea(), new HashSet<>()); + } + Set stRecAuxStSet = + peaAuxStatementMap.get(stRecAuxSt.getPeaPhasePc().getPea()); + stRecAuxStSet.add(stRecAuxSt); + } + } + return vePeaAuxStatementMap; + } + + public Expression createOppositeCondition(final ILocation loc, BoogieType boogieType, String lhs, String opr, + String rhs) { + String newOpr = ""; + switch (opr) { + case "==": + newOpr = "!="; + break; + case "!=": + newOpr = "=="; + break; + case "<": + newOpr = ">="; + break; + case ">": + newOpr = "<="; + break; + case "<=": + newOpr = ">"; + break; + case ">=": + newOpr = "<"; + break; + default: + throw new RuntimeException(getClass().getName() + "Could not parse token: " + opr); + } + return createExpression(loc, boogieType, lhs, newOpr, rhs); + } + + public Expression createExpression(final ILocation loc, BoogieType boogieType, String sLhs, Operator opr, + String sRhs) { + Expression rhs = null; + Expression lhs; + lhs = new IdentifierExpression(loc, boogieType, sLhs, DeclarationInformation.DECLARATIONINFO_GLOBAL); + switch (boogieType.toString()) { + case "int": + rhs = ExpressionFactory.createIntegerLiteral(loc, sRhs); + break; + case "bool": + boolean bValue = "true".equalsIgnoreCase(sRhs) ? true : false; + rhs = ExpressionFactory.createBooleanLiteral(loc, bValue); + break; + case "real": + rhs = ExpressionFactory.createRealLiteral(loc, sRhs); + break; + case "type-error": + throw new RuntimeErrorException(null, getClass().getName() + ": " + boogieType + " no known data type."); + } + Expression expression = ExpressionFactory.newBinaryExpression(loc, opr, lhs, rhs); + return expression; + } + + public static Expression createExpression(final ILocation loc, BoogieType boogieType, String sLhs, String sOpr, + String sRhs) { + Expression rhs = null; + Expression lhs; + BinaryExpression.Operator opr; + lhs = new IdentifierExpression(loc, boogieType, sLhs, DeclarationInformation.DECLARATIONINFO_GLOBAL); + switch (boogieType.toString()) { + case "int": + rhs = ExpressionFactory.createIntegerLiteral(loc, sRhs); + break; + case "bool": + boolean bValue = "true".equalsIgnoreCase(sRhs) ? true : false; + rhs = ExpressionFactory.createBooleanLiteral(loc, bValue); + break; + case "real": + rhs = ExpressionFactory.createRealLiteral(loc, sRhs); + break; + case "type-error": + throw new RuntimeErrorException(null, + StateRecoverabilityGenerator.class.getName() + ": " + boogieType + " no known data type."); + } + opr = getOperator(sOpr); + Expression expression = ExpressionFactory.newBinaryExpression(loc, opr, lhs, rhs); + return expression; + } + + private static BinaryExpression.Operator getOperator(String sOpr) { + switch (sOpr) { + case "||": + case "|": + return Operator.LOGICOR; + case "&&": + case "&": + return Operator.LOGICAND; + case "==": + return Operator.COMPEQ; + case "!=": + return Operator.COMPNEQ; + case "<": + return Operator.COMPLT; + case ">": + return Operator.COMPGT; + case "<=": + return Operator.COMPLEQ; + case ">=": + return Operator.COMPGEQ; + default: + throw new RuntimeErrorException(null, + StateRecoverabilityGenerator.class.getName() + ": Could not parse operator."); + } + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java new file mode 100644 index 00000000000..b3d5be06ae3 --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationCondition.java @@ -0,0 +1,121 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 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.staterecoverability; + +import javax.management.RuntimeErrorException; + +import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.DefaultLocation; + +/** + * + * This class contains a condition to be verified for the property check state-recoverability. An object of this class + * is created via each condition entered in the GUI. + * + * @author Tobias Wießner + * + */ + +public class StateRecoverabilityVerificationCondition { + private final Expression verificationConditionExpression; + private final String[] expr; + private final String dataType; + private final int iVariable = 0; + private final int iOperator = 1; + private final int iValue = 2; + + public StateRecoverabilityVerificationCondition(String[] expr, String dataType) { + this.expr = expr; + this.dataType = dataType; + this.verificationConditionExpression = StateRecoverabilityGenerator.createExpression(new DefaultLocation(), getBoogiePrimitiveType(dataType), expr[iVariable], expr[iOperator], expr[iValue]); + } + + public Expression getVerificationConditionExpression() { + return verificationConditionExpression; + } + + public String[] getVerificationConditionString() { + return expr; + } + + public String getVariable() { + return expr[iVariable]; + } + + public String getOperator() { + return expr[iOperator]; + } + + public String getValue() { + return expr[iValue]; + } + + public String getDataType() { + return dataType; + } + + public boolean getBoolValue() { + if (BoogiePrimitiveType.TYPE_BOOL.equals(getBoogiePrimitiveType(dataType))) { + return Boolean.getBoolean(expr[iValue]); + } + + throw new RuntimeErrorException(null, + getClass().getName() + " data type " + dataType + " is not correct for " + expr); + } + + public int getIntegerValue() { + if (BoogiePrimitiveType.TYPE_INT.equals(getBoogiePrimitiveType(dataType))) { + return Integer.getInteger(expr[iValue]); + } + + throw new RuntimeErrorException(null, + getClass().getName() + " data type " + dataType + " is not correct for " + expr); + } + + public double getDoubleValue() { + if (BoogiePrimitiveType.TYPE_REAL.equals(getBoogiePrimitiveType(dataType))) { + return Double.parseDouble(expr[iValue]); + } + + throw new RuntimeErrorException(null, + getClass().getName() + " data type " + dataType + " is not correct for " + expr); + } + + public BoogiePrimitiveType getBoogiePrimitiveType(String sDataType) { + switch (sDataType) { + case "bool": + return BoogiePrimitiveType.TYPE_BOOL; + case "int": + return BoogiePrimitiveType.TYPE_INT; + case "real": + return BoogiePrimitiveType.TYPE_REAL; + default: + return BoogiePrimitiveType.TYPE_ERROR; + } + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java new file mode 100644 index 00000000000..054cf854207 --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/staterecoverability/StateRecoverabilityVerificationConditionContainer.java @@ -0,0 +1,136 @@ +/* + * Copyright (C) 2023 Tobias Wießner + * Copyright (C) 2023 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.staterecoverability; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import javax.management.RuntimeErrorException; + +import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.DefaultLocation; +import de.uni_freiburg.informatik.ultimate.lib.pea.CounterTrace; +import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType.ReqPeas; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2Pea; + +/** +* +* This class contains all conditions to be verified for the property check state-recoverability. +* +* @author Tobias Wießner +* +*/ + +public class StateRecoverabilityVerificationConditionContainer { + + // Pattern for input expression + public static final String exprPattern = "\\s{0,1}((\\w+)\\s*([<>=!][=]*)\\s*(\\w+))\\s{0,1}"; + + private IReq2Pea mReq2pea; + private Map mVerificationExpressions; + private Map mVariableDataTypeMap; + + public StateRecoverabilityVerificationConditionContainer(IReq2Pea req2pea) { + mReq2pea = req2pea; + mVerificationExpressions = new HashMap<>(); + getDataTypeFromReq2Pea(req2pea); + } + + private void getDataTypeFromReq2Pea(IReq2Pea req2Pea) { + Map variableDataTypeMap = new HashMap<>(); + for (ReqPeas reqPeas : req2Pea.getReqPeas()) { + List> mReq = reqPeas.getCounterTrace2Pea(); + for (Entry entry : mReq) { + PhaseEventAutomata pea = entry.getValue(); + for (Map.Entry entryVariableDataType : pea.getVariables().entrySet()) { + // TODO anpassen abhängig davon was es noch für Datentypen gibt + variableDataTypeMap.put(entryVariableDataType.getKey(), entryVariableDataType.getValue()); + } + } + } + mVariableDataTypeMap = variableDataTypeMap; + } + + public Map getVerificationExpressions() { + return mVerificationExpressions; + } + + public void addExpression(String inputExpr) { + List veList = new ArrayList<>(); + int grpVariable = 2; + int grpOperator = 3; + int grpValue = 4; + String[] exprArray = inputExpr.split(","); + for (String expr : exprArray) { + Matcher m = match(expr, exprPattern); + if (m.find()) { + String sVariable = m.group(grpVariable); + String sOperator = m.group(grpOperator); + String sValue = m.group(grpValue); + String dataType = mVariableDataTypeMap.get(sVariable); + if (dataType == null) { + BoogieType boogieType = mReq2pea.getSymboltable().getId2Type().get(sVariable); + dataType = boogieType.toString(); + if(dataType == null) { + throw new IllegalArgumentException( + getClass().getName() + " could not find data type for " + sVariable); + } + + } + veList.add(new StateRecoverabilityVerificationCondition(new String[] { sVariable, sOperator, sValue }, dataType)); + } + } + addVerificationExpression(veList); + } + + private void addVerificationExpression(List veList) { + for (StateRecoverabilityVerificationCondition ve : veList) { + addVerificationExpression(ve); + } + } + + private void addVerificationExpression(StateRecoverabilityVerificationCondition ve) { + if (mVerificationExpressions == null) { + mVerificationExpressions = new HashMap<>(); + } + mVerificationExpressions.put(ve.getVariable(), ve); + } + + private Matcher match(String s, String pattern) { + Pattern p = Pattern.compile(pattern); + Matcher m = p.matcher(s); + return m; + } +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2CauseTrackingPea.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2CauseTrackingPea.java index a24805dc9aa..e8e4b1a1379 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2CauseTrackingPea.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2CauseTrackingPea.java @@ -96,7 +96,7 @@ public void transform(final IReq2Pea req2pea) { builder.addInitPattern(p); mDurations.addInitPattern(p); if (p.getCategory() == VariableCategory.OUT) { - builder.addAuxvar(ReqTestAnnotator.getTrackingVar(p.getId()), "bool", p); + builder.addAuxVarPrimedAndUnprimed(ReqTestAnnotator.getTrackingVar(p.getId()), "bool", p); } } for (final ReqPeas reqpea : simplePeas) { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java new file mode 100644 index 00000000000..e42989f6bef --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePea.java @@ -0,0 +1,234 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.testgen; + +import java.util.ArrayList; +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.regex.Matcher; +import java.util.regex.Pattern; + +import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation; +import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation.StorageClass; +import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; +import de.uni_freiburg.informatik.ultimate.boogie.ast.AssignmentStatement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BooleanLiteral; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IfStatement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IntegerLiteral; +import de.uni_freiburg.informatik.ultimate.boogie.ast.LeftHandSide; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; +import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogiePrimitiveType; +import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.DefaultLocation; +import de.uni_freiburg.informatik.ultimate.core.model.models.IBoogieType; +import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; +import de.uni_freiburg.informatik.ultimate.core.model.preferences.IPreferenceProvider; +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.CounterTrace; +import de.uni_freiburg.informatik.ultimate.lib.pea.Decision; +import de.uni_freiburg.informatik.ultimate.lib.pea.Phase; +import de.uni_freiburg.informatik.ultimate.lib.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.pea.RangeDecision; +import de.uni_freiburg.informatik.ultimate.lib.srparse.Durations; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.DeclarationPattern; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.DeclarationPattern.VariableCategory; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType.ReqPeas; +import de.uni_freiburg.informatik.ultimate.pea2boogie.Activator; +import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.preferences.Pea2BoogiePreferences; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2Pea; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2PeaAnnotator; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.ReqCheckAnnotator; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityVerificationCondition; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityVerificationConditionContainer; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.PeaPhaseProgramCounter; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxiliaryStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityGenerator; +import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.ReqSymboltableBuilder; +import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.ReqSymboltableBuilder.ErrorInfo; +import de.uni_freiburg.informatik.ultimate.pea2boogie.translator.ReqSymboltableBuilder.ErrorType; + +public class Req2ModifySymbolTablePea implements IReq2Pea { + + private final IUltimateServiceProvider mServices; + private final ILogger mLogger; + private final List mInitPattern; + private final List mReqPeas; + private IReqSymbolTable mSymbolTable; + private final Durations mDurations; + private boolean mHasErrors; + private final IPreferenceProvider prefs; + private ILocation loc; + private StateRecoverabilityGenerator stRecGen; + + public Req2ModifySymbolTablePea(final IUltimateServiceProvider services, final ILogger logger, final List init) { + mServices = services; + mLogger = logger; + mInitPattern = init; + mReqPeas = new ArrayList<>(); + mDurations = new Durations(); + prefs = mServices.getPreferenceProvider(Activator.PLUGIN_ID); + } + + @Override + public List getReqPeas() { + return mReqPeas; + } + + @Override + public IReqSymbolTable getSymboltable() { + return mSymbolTable; + } + + @Override + public Durations getDurations() { + return mDurations; + } + + @Override + public void transform(IReq2Pea req2pea) { + final List simplePeas = req2pea.getReqPeas(); + final IReqSymbolTable oldSymbolTable = req2pea.getSymboltable(); + + final StateRecoverabilityVerificationConditionContainer vec = getVerificationExpression(req2pea); + + stRecGen = new StateRecoverabilityGenerator(mLogger, mServices, oldSymbolTable); + final ReqSymboltableBuilder builder = new ReqSymboltableBuilder(mLogger, oldSymbolTable); + + //Passing the variable definitions + for (final DeclarationPattern p : mInitPattern) { + builder.addInitPattern(p); + mDurations.addInitPattern(p); + } + + //Übergabe der PEAs + for (final ReqPeas reqpea : simplePeas) { + mReqPeas.add(reqpea); + final PatternType pattern = reqpea.getPattern(); + mDurations.addNonInitPattern(pattern); + for (final Entry pea : reqpea.getCounterTrace2Pea()) { + builder.addPea(reqpea.getPattern(), pea.getValue()); + } + } + + //Collecting the PEAs and ProgramCounter + //Necessary in Transformer since otherwise unused global variables would be in the Boogie code + Map> veLocationMap = stRecGen.getRelevantLocationsFromPea(simplePeas, vec); + + List sreList = createGlobalVariableForVerificationExpression(builder, veLocationMap, vec); + + //Creating the statements + createAssignBoolToGlobalVariableBeforeWhileLoop(sreList); + createIfStatementInWhileLoop(sreList); + + mSymbolTable = builder.constructSymbolTable(); + } + + private void createIfStatementInWhileLoop(List auxStatements) { + for(AuxiliaryStatement auxStatement : auxStatements) { + if(auxStatement instanceof StateRecoverabilityAuxiliaryStatement) { + StateRecoverabilityAuxiliaryStatement auxStatementStRec = (StateRecoverabilityAuxiliaryStatement) auxStatement; + StateRecoverabilityVerificationCondition ve = auxStatementStRec.getVerificationExpression(); + ILocation loc = auxStatementStRec.getBoogieLocation(); + // Create expression + //Opposite of verification Expression + Expression condition1 = stRecGen.createOppositeCondition(loc, BoogiePrimitiveType.toPrimitiveType(ve.getDataType()), ve.getVariable(), ve.getOperator(), ve.getValue()); + // Program counter state + Expression condition2 = stRecGen.createExpression(loc, BoogieType.TYPE_INT, auxStatementStRec.getPcVariable(), Operator.COMPEQ, String.valueOf(auxStatementStRec.getPc())); + Expression condition1And2 = ExpressionFactory.newBinaryExpression(loc, Operator.LOGICAND, condition1, condition2); + BooleanLiteral booleanLiteral = ExpressionFactory.createBooleanLiteral(loc, true); + // Create assignment + AssignmentStatement assignmentStatement = genAssignmentStmt(loc, auxStatementStRec.getRelatedVariable(), booleanLiteral); + IfStatement ifStatement = new IfStatement(loc, condition1And2, new Statement[] {assignmentStatement}, new Statement[0]); + auxStatementStRec.setIfSt(ifStatement); + } + } + } + + private StateRecoverabilityVerificationConditionContainer getVerificationExpression(IReq2Pea req2pea) { + final StateRecoverabilityVerificationConditionContainer vec = new StateRecoverabilityVerificationConditionContainer(req2pea); + //Gets verification expression from GUI + String verExpr = prefs.getString(Pea2BoogiePreferences.LABEL_STATE_RECOVERABILITY_VER_EXPR); + vec.addExpression(verExpr); + return vec; + } + + private List createGlobalVariableForVerificationExpression(ReqSymboltableBuilder builder, Map> veLocationMaptionMap, StateRecoverabilityVerificationConditionContainer vec) { + List sreList = new ArrayList<>(); + for(Map.Entry> entry : veLocationMaptionMap.entrySet()) { + for(PeaPhaseProgramCounter peaPhasePc : entry.getValue()) { + String pcName = getPcName(peaPhasePc.getPea().getName()); + int pc = peaPhasePc.getPc(); + //Erstelle für jede angegebene Bedingung eine globale Variable für alle PCs + String variable = entry.getKey().getVariable(); + String dataType = entry.getKey().getDataType(); + String globalVariable = pcName + pc + "_StRec_" + variable; + StateRecoverabilityAuxiliaryStatement auxStatement = new StateRecoverabilityAuxiliaryStatement(peaPhasePc, globalVariable, pcName, pc, entry.getKey()); + sreList.add(builder.addAuxVar(auxStatement, globalVariable, "bool", null)); + } + + } + return sreList; + } + + private void createAssignBoolToGlobalVariableBeforeWhileLoop(List auxStatements) { + for(AuxiliaryStatement auxStatement : auxStatements) { + if(auxStatement instanceof StateRecoverabilityAuxiliaryStatement) { + StateRecoverabilityAuxiliaryStatement auxStatementStateRecoverability = (StateRecoverabilityAuxiliaryStatement) auxStatement; + BooleanLiteral booleanLiteral = ExpressionFactory.createBooleanLiteral(null, false); + AssignmentStatement assignmentStatement = genAssignmentStmt(constructNewLocation(), auxStatementStateRecoverability.getRelatedVariable(), booleanLiteral); + auxStatementStateRecoverability.setAssignVar(assignmentStatement); + } + } + } + + private String getPcName(String s) { + //Decision decision = phase.getClockInvariant().getDecision(); + //if(decision != null) { + // return decision.getVar(); + //} + return s + "_pc"; + } + + private Matcher match(String text, String pattern) { + Pattern p = Pattern.compile(pattern); + Matcher m = p.matcher(text); + return m; + } + + private static AssignmentStatement genAssignmentStmt(final ILocation bl, final String id, final Expression val) { + return genAssignmentStmt(bl, new VariableLHS(bl, id), val); + } + + private static AssignmentStatement genAssignmentStmt(final ILocation bl, final VariableLHS lhs, + final Expression val) { + assert lhs.getLocation() == bl; + return new AssignmentStatement(bl, new LeftHandSide[] { lhs }, new Expression[] { val }); + } + + private ILocation constructNewLocation() { + return new DefaultLocation(); + } + + @Override + public boolean hasErrors() { + return mHasErrors; + } + + @Override + public IReq2PeaAnnotator getAnnotator() { + return new ReqCheckAnnotator(mServices, mLogger, getReqPeas(), getSymboltable(), getDurations()); + } + +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePeaTransformer.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePeaTransformer.java new file mode 100644 index 00000000000..66826783d1b --- /dev/null +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/testgen/Req2ModifySymbolTablePeaTransformer.java @@ -0,0 +1,32 @@ +package de.uni_freiburg.informatik.ultimate.pea2boogie.testgen; + +import java.util.List; +import java.util.Map; + +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.pea.PhaseEventAutomata; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.DeclarationPattern; +import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2Pea; +import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2PeaTransformer; + +public class Req2ModifySymbolTablePeaTransformer implements IReq2PeaTransformer { + + private final ILogger mLogger; + private final IUltimateServiceProvider mServices; + + public Req2ModifySymbolTablePeaTransformer(final IUltimateServiceProvider services, final ILogger logger) { + mLogger = logger; + mServices = services; + } + + @Override + public IReq2Pea transform(final IReq2Pea req2pea, final List init, final List> requirements) { + final Req2ModifySymbolTablePea req2ModifySymbolTablePea = new Req2ModifySymbolTablePea(mServices, mLogger, init); + + req2ModifySymbolTablePea.transform(req2pea); + return req2ModifySymbolTablePea; + } + +} diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java index 7259a2dc779..ddd605e56f6 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/Req2BoogieTranslator.java @@ -84,6 +84,8 @@ import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2PeaAnnotator; import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.IReq2PeaTransformer; import de.uni_freiburg.informatik.ultimate.pea2boogie.req2pea.Req2Pea; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.StateRecoverabilityAuxiliaryStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer.StatementAssignment; import de.uni_freiburg.informatik.ultimate.pea2boogie.testgen.ReqInOutGuesser; import de.uni_freiburg.informatik.ultimate.util.simplifier.NormalFormTransformer; @@ -557,11 +559,11 @@ private Statement[] genWhileLoopBody(final BoogieLocation bl) { mSymboltable.getPcName(pea.getValue()), bl)); } } - + // Assign St-Recoverability if statement + stmtList.addAll(mSymboltable.getAuxStatementContainer().getStatements(StatementAssignment.IF_ST)); stmtList.addAll(mReqCheckAnnotator.getStateChecks()); stmtList.addAll( mSymboltable.getPcVars().stream().map(this::genStateVarAssignHistory).collect(Collectors.toList())); - for (final ReqPeas reqpea : mReqPeas) { for (final Entry ct2pea : reqpea.getCounterTrace2Pea()) { final PhaseEventAutomata pea = ct2pea.getValue(); @@ -662,6 +664,9 @@ private Statement[] generateProcedureBody(final BoogieLocation bl, final List init) { modifiedVarsList.addAll(mSymboltable.getPrimedVars()); modifiedVarsList.addAll(mSymboltable.getHistoryVars()); modifiedVarsList.addAll(mSymboltable.getEventVars()); + // Adds only instance of class type StateRecoverabilityAuxStatement + modifiedVarsList.addAll(mSymboltable.getAuxStatementContainer().getRelatedVariableForInstance(new StateRecoverabilityAuxiliaryStatement(""))); final VariableLHS[] modifiedVars = new VariableLHS[modifiedVarsList.size()]; for (int i = 0; i < modifiedVars.length; i++) { diff --git a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java index 53f00f8e527..f130348bc99 100644 --- a/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java +++ b/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/ReqSymboltableBuilder.java @@ -38,6 +38,8 @@ import java.util.Set; import java.util.stream.Collectors; +import org.eclipse.core.runtime.IRegistryChangeEvent; + import de.uni_freiburg.informatik.ultimate.boogie.BoogieLocation; import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation; import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; @@ -65,6 +67,8 @@ import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.DeclarationPattern.VariableCategory; import de.uni_freiburg.informatik.ultimate.lib.srparse.pattern.PatternType; import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatement; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer; import de.uni_freiburg.informatik.ultimate.util.datastructures.UnionFind; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.LinkedHashRelation; @@ -82,6 +86,9 @@ public class ReqSymboltableBuilder { private final Map mId2Type; private final Map mId2IdExpr; private final Map mId2VarLHS; + + private final AuxiliaryStatementContainer mAuxStatements; + private final Set mAuxVars; private final Set mStateVars; private final Set mConstVars; private final Set mPrimedVars; @@ -106,6 +113,8 @@ public ReqSymboltableBuilder(final ILogger logger) { mId2IdExpr = new LinkedHashMap<>(); mId2VarLHS = new LinkedHashMap<>(); + mAuxStatements = new AuxiliaryStatementContainer(); + mAuxVars = new LinkedHashSet<>(); mStateVars = new LinkedHashSet<>(); mConstVars = new LinkedHashSet<>(); mPrimedVars = new LinkedHashSet<>(); @@ -122,6 +131,37 @@ public ReqSymboltableBuilder(final ILogger logger) { mBuiltinFunctions = generateBuildinFuntions(); } + + //Copy constructor SymbolTable + + public ReqSymboltableBuilder(ILogger logger, IReqSymbolTable iReqSymbolTable) { + mLogger = logger; + mId2Errors = new LinkedHashRelation<>(); + //mId2Type = new LinkedHashMap<>(iReqSymbolTable.getId2Type()); + //mId2IdExpr = new LinkedHashMap<>(iReqSymbolTable.getId2IdExpr()); + //mId2VarLHS = new LinkedHashMap<>(iReqSymbolTable.getId2VarLHS()); + mId2Type = new LinkedHashMap<>(); + mId2IdExpr = new LinkedHashMap<>(); + mId2VarLHS = new LinkedHashMap<>(); + + mAuxStatements = iReqSymbolTable.getAuxStatementContainer(); + mAuxVars = new LinkedHashSet(iReqSymbolTable.getAuxVars()); + mStateVars = new LinkedHashSet(iReqSymbolTable.getStateVars()); + mConstVars = new LinkedHashSet(iReqSymbolTable.getConstVars()); + mPrimedVars = new LinkedHashSet(iReqSymbolTable.getPrimedVars()); + mHistoryVars = new LinkedHashSet(iReqSymbolTable.getHistoryVars()); + mEventVars = new LinkedHashSet(iReqSymbolTable.getEventVars()); + mPcVars = new LinkedHashSet(iReqSymbolTable.getPcVars()); + mClockVars = new LinkedHashSet(iReqSymbolTable.getClockVars()); + + mReq2Loc = new LinkedHashMap<>(); + mConst2Value = new LinkedHashMap<>(iReqSymbolTable.getConstToValue()); + mInputVars = new LinkedHashSet<>(iReqSymbolTable.getInputVars()); + mOutputVars = new LinkedHashSet<>(iReqSymbolTable.getOutputVars()); + mEquivalences = iReqSymbolTable.getVariableEquivalenceClasses(); + mBuiltinFunctions = generateBuildinFuntions(); + } + public void addInitPattern(final DeclarationPattern initPattern) { final BoogiePrimitiveType type = BoogiePrimitiveType.toPrimitiveType(initPattern.getType()); @@ -198,13 +238,13 @@ private void updateEquivalences(final PhaseEventAutomata pea) { mEquivalences.union(peaVars); } - public void addAuxvar(final String name, final String typeString, final PatternType source) { + public void addAuxVarPrimedAndUnprimed(final String name, final String typeString, final PatternType source) { addVar(name, BoogiePrimitiveType.toPrimitiveType(typeString), source, mStateVars); } public IReqSymbolTable constructSymbolTable() { final String deltaVar = declareDeltaVar(); - return new ReqSymbolTable(deltaVar, mId2Type, mId2IdExpr, mId2VarLHS, mStateVars, mPrimedVars, mHistoryVars, + return new ReqSymbolTable(deltaVar, mId2Type, mId2IdExpr, mId2VarLHS, mAuxStatements, mAuxVars, mStateVars, mPrimedVars, mHistoryVars, mConstVars, mEventVars, mPcVars, mClockVars, mReq2Loc, mConst2Value, mInputVars, mOutputVars, mBuiltinFunctions, mEquivalences); } @@ -255,6 +295,24 @@ private void addVar(final String name, final BoogieType type, final PatternType< addVarOneKind(getHistoryVarId(name), type, source, mHistoryVars); addVarOneKind(getPrimedVarId(name), type, source, mPrimedVars); } + + public AuxiliaryStatement addAuxVar(final AuxiliaryStatement auxStatement, final String name, final String boogieType, final PatternType source) { + Set kind = mAuxVars; + auxStatement.setBoogieLocation(DUMMY_LOC); + switch (boogieType.toLowerCase()) { + case "bool": + case "real": + case "int": + addVarOneKind(name, BoogiePrimitiveType.toPrimitiveType(boogieType), source, kind); + return mAuxStatements.addAuxStatement(name, auxStatement); + case "event": + break; + default: + addError(name, new ErrorInfo(ErrorType.UNKNOWN_TYPE, source)); + break; + } + return null; + } private void addVarOneKind(final String name, final BoogieType type, final PatternType source, final Set kind) { @@ -348,6 +406,9 @@ private static final class ReqSymbolTable implements IReqSymbolTable { private final Map mId2VarLHS; private final Map mConst2Value; private final Map, BoogieLocation> mReq2Loc; + + private final AuxiliaryStatementContainer mAuxStatements; + private final Set mAuxVars; private final Set mStateVars; private final Set mConstVars; private final Set mPrimedVars; @@ -362,8 +423,8 @@ private static final class ReqSymbolTable implements IReqSymbolTable { private final UnionFind mEquivalences; private ReqSymbolTable(final String deltaVar, final Map id2Type, - final Map id2idExp, final Map id2VarLhs, - final Set stateVars, final Set primedVars, final Set historyVars, + final Map id2idExp, final Map id2VarLhs, final AuxiliaryStatementContainer auxStatements, + final Set auxVars, Set stateVars, final Set primedVars, final Set historyVars, final Set constVars, final Set eventVars, final Set pcVars, final Set clockVars, final Map, BoogieLocation> req2loc, final Map const2Value, final Set inputVars, final Set outputVars, @@ -372,6 +433,8 @@ private ReqSymbolTable(final String deltaVar, final Map id2T mId2IdExpr = Collections.unmodifiableMap(id2idExp); mId2VarLHS = Collections.unmodifiableMap(id2VarLhs); + mAuxStatements = auxStatements; + mAuxVars = Collections.unmodifiableSet(auxVars); mStateVars = Collections.unmodifiableSet(stateVars); mConstVars = Collections.unmodifiableSet(constVars); mPrimedVars = Collections.unmodifiableSet(primedVars); @@ -462,6 +525,21 @@ public Set getOutputVars() { public Map getConstToValue() { return mConst2Value; } + + @Override + public UnionFind getVariableEquivalenceClasses() { + return mEquivalences; + } + + @Override + public Set getAuxVars() { + return mAuxVars; + } + + @Override + public AuxiliaryStatementContainer getAuxStatementContainer( ) { + return mAuxStatements; + } @Override public String getPcName(final PhaseEventAutomata automaton) { @@ -477,6 +555,11 @@ public String getPrimedVarId(final String name) { public String getHistoryVarId(final String name) { return ReqSymboltableBuilder.getHistoryVarId(name); } + + @Override + public Map getId2Type() { + return mId2Type; + } @Override public Collection getDeclarations() { @@ -489,6 +572,7 @@ public Collection getDeclarations() { decls.addAll(constructVariableDeclarations(mPrimedVars)); decls.addAll(constructVariableDeclarations(mHistoryVars)); decls.addAll(constructVariableDeclarations(mEventVars)); + decls.addAll(constructVariableDeclarations(mAuxVars)); decls.addAll(mBuildinFunctions.values()); return decls; } @@ -522,7 +606,7 @@ private List constructConstDeclarations(final Collection id final IdentifierExpression idExpr = mId2IdExpr.get(id); final Expression axiom = new BinaryExpression(value.getLoc(), value.getType(), Operator.COMPEQ, idExpr, value); - rtr.add(new Axiom(varlist.getLocation(), EMPTY_ATTRIBUTES, axiom)); + rtr.add(new Axiom(varlist.getLocation(), EMPTY_ATTRIBUTES, axiom)); } } return rtr; @@ -552,11 +636,6 @@ private List constructVarLists(final Collection ident return identifiers.stream().map(this::constructVarlist).filter(a -> a != null).collect(Collectors.toList()); } - @Override - public UnionFind getVariableEquivalenceClasses() { - return mEquivalences; - } - } public enum ErrorType { diff --git a/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java b/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java index 9cc5fa57671..f22aaae3403 100644 --- a/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java +++ b/trunk/source/ReqToTest/src/de/uni_freiburg/informatik/ultimate/reqtotest/req/Req2TestReqSymbolTable.java @@ -37,6 +37,7 @@ import de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol; import de.uni_freiburg.informatik.ultimate.logic.TermVariable; import de.uni_freiburg.informatik.ultimate.pea2boogie.IReqSymbolTable; +import de.uni_freiburg.informatik.ultimate.pea2boogie.staterecoverability.AuxiliaryStatementContainer; import de.uni_freiburg.informatik.ultimate.reqtotest.graphtransformer.FakeBoogieVar; import de.uni_freiburg.informatik.ultimate.util.datastructures.UnionFind; @@ -128,10 +129,6 @@ public Set getConstVars() { return mConstVars; } - public Set getAuxVars() { - return mAuxVars; - } - @Override public Set getHistoryVars() { return mHistoryVars; @@ -367,4 +364,22 @@ public UnionFind getVariableEquivalenceClasses() { throw new UnsupportedOperationException(); } + @Override + public Set getAuxVars() { + // TODO Auto-generated method stub + return null; + } + + @Override + public AuxiliaryStatementContainer getAuxStatementContainer() { + // TODO Auto-generated method stub + return null; + } + + @Override + public Map getId2Type() { + // TODO Auto-generated method stub + return null; + } + }