diff --git a/build.gradle.kts b/build.gradle.kts index 8c70a92e68..d1b9ab25d5 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -11,7 +11,7 @@ buildscript { allprojects { group = "hu.bme.mit.inf.theta" - version = "4.0.0" + version = "4.1.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/PorLts.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/PorLts.java new file mode 100644 index 0000000000..34787ca6ad --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/PorLts.java @@ -0,0 +1,268 @@ +/* + * Copyright 2022 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.analysis.algorithm; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.type.Type; + +import java.util.*; +import java.util.function.Predicate; + +/** + * LTS with a POR (Partial Order Reduction) algorithm applied as a filter when returning enabled actions. + * + * @param the type of the state + * @param the type of the action (transition in the state space) + * @param the type of the transition in the original formalism + */ +public abstract class PorLts implements LTS { + + /* CACHE COLLECTIONS */ + + /** + * Shared objects (~global variables) used by a transition. + */ + private final HashMap>> usedSharedObjects = new HashMap<>(); + + /** + * Shared objects (~global variables) that are used by the key transition or by transitions reachable from the + * current state via a given transition. + */ + private final HashMap>> influencedSharedObjects = new HashMap<>(); + + /** + * Backward transitions in the transition system (a transition of a loop). + */ + protected final Set backwardTransitions = new HashSet<>(); + + + /** + * Returns the enabled actions in the ARG from the given state filtered with a POR algorithm. + * + * @param state the state whose enabled actions we would like to know + * @return the enabled actions + */ + @Override + public Collection getEnabledActionsFor(S state) { + // Collecting enabled actions + Collection allEnabledActions = getAllEnabledActionsFor(state); + + // Calculating the persistent set starting from every (or some of the) enabled transition; the minimal persistent set is stored + Collection minimalPersistentSet = new HashSet<>(); + Collection persistentSetFirstActions = getPersistentSetFirstActions(allEnabledActions); + for (A firstAction : persistentSetFirstActions) { + Collection persistentSet = calculatePersistentSet(allEnabledActions, firstAction); + if (minimalPersistentSet.size() == 0 || persistentSet.size() < minimalPersistentSet.size()) { + minimalPersistentSet = persistentSet; + } + } + + return minimalPersistentSet; + } + + /** + * Calculates a persistent set of enabled actions starting from a particular action. + * + * @param enabledActions the enabled actions in the present state + * @param firstAction the action who will be added to the persistent set as the first action + * @return the persistent set of enabled actions + */ + protected Collection calculatePersistentSet(Collection enabledActions, A firstAction) { + if (isBackwardAction(firstAction)) { + return new HashSet<>(enabledActions); + } + + Set persistentSet = new HashSet<>(); + Set otherActions = new HashSet<>(enabledActions); // actions not in the persistent set + persistentSet.add(firstAction); + otherActions.remove(firstAction); + + boolean addedNewAction = true; + while (addedNewAction) { + addedNewAction = false; + Set actionsToRemove = new HashSet<>(); + for (A action : otherActions) { + // for every action that is not in the persistent set it is checked whether it should be added to the persistent set + // (because it is dependent with an action already in the persistent set) + if (persistentSet.stream().anyMatch(persistentSetAction -> areDependents(persistentSetAction, action))) { + if (isBackwardAction(action)) { + return new HashSet<>(enabledActions); // see POR algorithm for the reason of removing backward transitions + } + + persistentSet.add(action); + actionsToRemove.add(action); + addedNewAction = true; + } + } + actionsToRemove.forEach(otherActions::remove); + } + + return persistentSet; + } + + /** + * Returns all the enabled actions in a state. + * + * @param state the state whose enabled actions are to be returned + * @return the enabled actions in the state + */ + protected abstract Collection getAllEnabledActionsFor(S state); + + /** + * Returns the actions from where persistent sets will be calculated (a subset of the given enabled actions). + * The default implementation returns all enabled actions. + * + * @param allEnabledActions all the enabled actions in the present state + * @return the actions from where persistent sets will be calculated + */ + protected Collection getPersistentSetFirstActions(Collection allEnabledActions) { + return allEnabledActions; + } + + /** + * Determines whether an action is dependent with another one (based on the notions introduced for the POR + * algorithm) already in the persistent set. + * + * @param persistentSetAction the action in the persistent set + * @param action the other action (not in the persistent set) + * @return true, if the two actions are dependent in the context of persistent sets + */ + protected boolean areDependents(A persistentSetAction, A action) { + return canEnOrDisableEachOther(persistentSetAction, action) || + getInfluencedSharedObjects(getTransitionOf(action)).stream().anyMatch(varDecl -> + getCachedUsedSharedObjects(getTransitionOf(persistentSetAction)).contains(varDecl)); + } + + /** + * Determines whether two actions can enable or disable each other (if true, the two actions are dependent). + * + * @param action1 action 1 + * @param action2 action 2 + * @return true, if the two actions can enable or disable each other + */ + protected abstract boolean canEnOrDisableEachOther(A action1, A action2); + + /** + * Determines whether the given action is a backward action. + * + * @param action the action to be classified as backward action or non-backward action + * @return true, if the action is a backward action + */ + protected boolean isBackwardAction(A action) { + return backwardTransitions.contains(getTransitionOf(action)); + } + + /** + * Get the original transition of an action (from which the action has been created). + * + * @param action whose original transition is to be returned + * @return the original transition + */ + protected abstract T getTransitionOf(A action); + + /** + * Returns the successive transitions of a transition (transitions whose source is the target of the given + * parameter). + * + * @param transition whose successive transitions is to be returned + * @return the successive transitions of the transition given as the parameter + */ + protected abstract Set getSuccessiveTransitions(T transition); + + + /** + * Returns the shared objects (~global variables) that an action uses (it is present in one of its labels). + * + * @param transition whose shared objects are to be returned + * @return the set of used shared objects + */ + protected abstract Set> getDirectlyUsedSharedObjects(T transition); + + /** + * Returns the shared objects (~global variables) that an action uses. + * + * @param transition whose shared objects are to be returned + * @return the set of directly or indirectly used shared objects + */ + protected Set> getUsedSharedObjects(T transition) { + return getDirectlyUsedSharedObjects(transition); + } + + /** + * Same as {@link PorLts#getUsedSharedObjects(T transition)} with an additional cache layer. + * + * @param transition whose shared objects are to be returned + * @return the set of directly or indirectly used shared objects + */ + private Set> getCachedUsedSharedObjects(T transition) { + if (!usedSharedObjects.containsKey(transition)) { + Set> vars = getUsedSharedObjects(transition); + usedSharedObjects.put(transition, vars); + } + return usedSharedObjects.get(transition); + } + + /** + * Returns the shared objects (~global variables) used by the given transition or by transitions that are reachable + * via the given transition ("influenced shared objects"). + * + * @param transition whose successor transitions' shared objects are to be returned. + * @return the set of influenced shared objects + */ + protected Set> getInfluencedSharedObjects(T transition) { + if (!influencedSharedObjects.containsKey(transition)) { + influencedSharedObjects.put(transition, getSharedObjectsWithBFS(transition, t -> true)); + } + return influencedSharedObjects.get(transition); + } + + /** + * Returns shared objects (~global variables) encountered in a search starting from a given transition. + * + * @param startTransition the start point (transition) of the search + * @param visitTransition the predicate that tells whether a transition has to be explored + * @return the set of encountered shared objects + */ + protected Set> getSharedObjectsWithBFS(T startTransition, Predicate visitTransition) { + Set> vars = new HashSet<>(); + List exploredTransitions = new ArrayList<>(); + List transitionsToExplore = new ArrayList<>(); + transitionsToExplore.add(startTransition); + + while (!transitionsToExplore.isEmpty()) { + T exploring = transitionsToExplore.remove(0); + vars.addAll(getDirectlyUsedSharedObjects(exploring)); + Set successiveTransitions = getSuccessiveTransitions(exploring); + + for (var newTransition : successiveTransitions) { + if (!exploredTransitions.contains(newTransition) && visitTransition.test(newTransition)) { + transitionsToExplore.add(newTransition); + } + } + exploredTransitions.add(exploring); + } + return vars; + } + + /** + * Collects backward transitions of the transition system. + */ + protected abstract void collectBackwardTransitions(); +} diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/common/XcfaConfigBuilder.java b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/common/XcfaConfigBuilder.java index 10550c1f18..d0babcf0db 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/common/XcfaConfigBuilder.java +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/common/XcfaConfigBuilder.java @@ -66,11 +66,7 @@ import hu.bme.mit.theta.xcfa.analysis.common.autoexpl.XcfaGlobalStaticAutoExpl; import hu.bme.mit.theta.xcfa.analysis.common.autoexpl.XcfaNewAtomsAutoExpl; import hu.bme.mit.theta.xcfa.analysis.common.autoexpl.XcfaNewOperandsAutoExpl; -import hu.bme.mit.theta.xcfa.analysis.impl.interleavings.XcfaInitFunc; -import hu.bme.mit.theta.xcfa.analysis.impl.interleavings.XcfaLts; -import hu.bme.mit.theta.xcfa.analysis.impl.interleavings.XcfaOrd; -import hu.bme.mit.theta.xcfa.analysis.impl.interleavings.XcfaPrecRefiner; -import hu.bme.mit.theta.xcfa.analysis.impl.interleavings.XcfaTransFunc; +import hu.bme.mit.theta.xcfa.analysis.impl.interleavings.*; import hu.bme.mit.theta.xcfa.analysis.impl.singlethread.XcfaDistToErrComparator; import hu.bme.mit.theta.xcfa.analysis.impl.singlethread.XcfaSTInitFunc; import hu.bme.mit.theta.xcfa.analysis.impl.singlethread.XcfaSTLts; @@ -101,7 +97,7 @@ public enum Refinement { public enum Algorithm { SINGLETHREAD { @Override - public LTS, ? extends XcfaAction> getLts() { + public LTS, ? extends XcfaAction> getLts(XCFA xcfa) { return new XcfaSTLts(); } @@ -134,7 +130,7 @@ public Analysis, ? extends XcfaAction> getLts() { + public LTS, ? extends XcfaAction> getLts(XCFA xcfa) { return new XcfaLts(); } @@ -162,9 +158,41 @@ public PartialOrd> getPartialOrder(final Part public Analysis, A, XcfaPrec

> getAnalysis(final List initLocs, final Analysis analysis) { return XcfaAnalysis.create(initLocs, getPartialOrder(analysis.getPartialOrd()), getInitFunc(initLocs, analysis.getInitFunc()), getTransFunc(analysis.getTransFunc())); } + }, + + INTERLEAVINGS_POR { + @Override + public LTS, ? extends XcfaAction> getLts(XCFA xcfa) { + return new XcfaPorLts(xcfa); + } + + @Override + public InitFunc, XcfaPrec

> getInitFunc(List initLocs, InitFunc initFunc) { + return INTERLEAVINGS.getInitFunc(initLocs, initFunc); + } + + @Override + public TransFunc, A, XcfaPrec

> getTransFunc(TransFunc transFunc) { + return INTERLEAVINGS.getTransFunc(transFunc); + } + + @Override + public

PrecRefiner, ? extends StmtAction, XcfaPrec

, R> getPrecRefiner(RefutationToPrec refToPrec) { + return INTERLEAVINGS.getPrecRefiner(refToPrec); + } + + @Override + public PartialOrd> getPartialOrder(PartialOrd partialOrd) { + return INTERLEAVINGS.getPartialOrder(partialOrd); + } + + @Override + public Analysis, ? extends A, ? extends XcfaPrec

> getAnalysis(List initLoc, Analysis analysis) { + return INTERLEAVINGS.getAnalysis(initLoc, analysis); + } }; - public abstract LTS, ? extends XcfaAction> getLts(); + public abstract LTS, ? extends XcfaAction> getLts(XCFA xcfa); public abstract InitFunc, XcfaPrec

> getInitFunc(final List initLocs, final InitFunc initFunc); @@ -299,7 +327,7 @@ public XcfaConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { } public XcfaConfig build(final XCFA xcfa) { - final LTS lts = algorithm.getLts(); + final LTS lts = algorithm.getLts(xcfa); final Abstractor abstractor; final Refiner refiner; final XcfaPrec prec; diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/interleavings/XcfaAction.java b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/interleavings/XcfaAction.java index 527a55a581..baf1e047de 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/interleavings/XcfaAction.java +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/interleavings/XcfaAction.java @@ -29,19 +29,25 @@ public class XcfaAction extends hu.bme.mit.theta.xcfa.analysis.common.XcfaAction { private final Integer process; + private final XcfaEdge edge; private final List labels; private final XcfaLocation source; private final XcfaLocation target; - protected XcfaAction(final Integer process, final XcfaLocation source, final XcfaLocation target, final List labels) { + protected XcfaAction(final Integer process, final XcfaEdge edge, final List labels) { this.process = checkNotNull(process); - this.source = checkNotNull(source); - this.target = checkNotNull(target); + this.edge = checkNotNull(edge); + this.source = checkNotNull(edge.getSource()); + this.target = checkNotNull(edge.getTarget()); this.labels = checkNotNull(labels); } public static XcfaAction create(final Integer process, final XcfaEdge edge) { - return new XcfaAction(process, edge.getSource(), edge.getTarget(), edge.getLabels()); + return new XcfaAction(process, edge, edge.getLabels()); + } + + public XcfaEdge getEdge() { + return edge; } public XcfaLocation getSource() { @@ -75,6 +81,6 @@ public Integer getProcess() { } public XcfaAction withLabels(final List stmts) { - return new XcfaAction(process, source, target, stmts); + return new XcfaAction(process, edge, stmts); } } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/interleavings/XcfaLts.java b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/interleavings/XcfaLts.java index b7ec673697..b36b514a32 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/interleavings/XcfaLts.java +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/interleavings/XcfaLts.java @@ -25,6 +25,12 @@ import java.util.List; public final class XcfaLts implements LTS, XcfaAction> { + /** + * Returns the enabled actions in the ARG from the given state. + * + * @param state the state whose enabled actions we would like to know + * @return the enabled actions + */ @Override public Collection getEnabledActionsFor(final XcfaState state) { final List xcfaActions = new ArrayList<>(); diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/interleavings/XcfaPorLts.java b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/interleavings/XcfaPorLts.java new file mode 100644 index 0000000000..5754d2bc1b --- /dev/null +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/interleavings/XcfaPorLts.java @@ -0,0 +1,150 @@ +/* + * Copyright 2022 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.xcfa.analysis.impl.interleavings; + +import hu.bme.mit.theta.analysis.algorithm.PorLts; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.xcfa.model.XCFA; +import hu.bme.mit.theta.xcfa.model.XcfaEdge; +import hu.bme.mit.theta.xcfa.model.XcfaLabel; +import hu.bme.mit.theta.xcfa.model.XcfaLocation; +import hu.bme.mit.theta.xcfa.model.utils.LabelUtils; + +import java.util.*; +import java.util.stream.Collectors; + +public class XcfaPorLts extends PorLts, XcfaAction, XcfaEdge> { + + private final XCFA xcfa; + + private final XcfaLts simpleXcfaLts = new XcfaLts(); + + private final Random random = new Random(); + + public XcfaPorLts(XCFA xcfa) { + this.xcfa = xcfa; + collectBackwardTransitions(); + } + + @Override + protected Collection getAllEnabledActionsFor(XcfaState state) { + return simpleXcfaLts.getEnabledActionsFor(state); + } + + @Override + protected Collection getPersistentSetFirstActions(Collection allEnabledActions) { + var enabledActionsByProcess = allEnabledActions.stream().collect(Collectors.groupingBy(XcfaAction::getProcess)); + List enabledProcesses = new ArrayList<>(enabledActionsByProcess.keySet()); + Collections.shuffle(enabledProcesses); + Collection firstActions = new HashSet<>(); + + for (Integer enabledProcess : enabledProcesses) { + var actionsByProcess = enabledActionsByProcess.get(enabledProcess); + firstActions.add(actionsByProcess.get(random.nextInt(actionsByProcess.size()))); + } + return firstActions; + } + + @Override + protected boolean canEnOrDisableEachOther(XcfaAction action1, XcfaAction action2) { + return action1.getProcess().equals(action2.getProcess()); + } + + @Override + protected XcfaEdge getTransitionOf(XcfaAction action) { + return action.getEdge(); + } + + @Override + protected Set getSuccessiveTransitions(XcfaEdge edge) { + var outgoingEdges = new HashSet<>(edge.getTarget().getOutgoingEdges()); + List startThreads = edge.getLabels().stream() + .filter(label -> label instanceof XcfaLabel.StartThreadXcfaLabel) + .map(label -> (XcfaLabel.StartThreadXcfaLabel) label).collect(Collectors.toList()); + if (startThreads.size() > 0) { // for start thread labels, the thread procedure must be explored, too! + startThreads.forEach(startThread -> + outgoingEdges.addAll(startThread.getProcess().getMainProcedure().getInitLoc().getOutgoingEdges())); + } + return outgoingEdges; + } + + /** + * Returns the global variables that an edge uses (it is present in one of its labels). + * + * @param edge whose global variables are to be returned + * @return the set of used global variables + */ + @Override + protected Set> getDirectlyUsedSharedObjects(XcfaEdge edge) { + Set> vars = new HashSet<>(); + edge.getLabels().forEach(label -> LabelUtils.getVars(label).forEach(usedVar -> { + if (xcfa.getGlobalVars().contains(usedVar)) { + vars.add(usedVar); + } + })); + return vars; + } + + /** + * Returns the global variables that an edge uses or if it is the start of an atomic block the global variables + * that are used in the atomic block. + * + * @param edge whose global variables are to be returned + * @return the set of directly or indirectly used global variables + */ + @Override + protected Set> getUsedSharedObjects(XcfaEdge edge) { + Set> vars; + var labels = edge.getLabels(); + if (labels.stream().anyMatch(label -> label instanceof XcfaLabel.AtomicBeginXcfaLabel)) { + vars = getSharedObjectsWithBFS(edge, xcfaEdge -> xcfaEdge.getLabels().stream().noneMatch(label -> label instanceof XcfaLabel.AtomicEndXcfaLabel)); + } else { + vars = getDirectlyUsedSharedObjects(edge); + } + return vars; + } + + /** + * Collects backward edges of the given XCFA. + */ + @Override + protected void collectBackwardTransitions() { + for (var process : xcfa.getProcesses()) { + for (var procedure : process.getProcedures()) { + // DFS for every procedure of the XCFA to discover backward edges + Set visitedLocations = new HashSet<>(); + Stack stack = new Stack<>(); + + stack.push(procedure.getInitLoc()); // start from the initial location of the procedure + while (!stack.isEmpty()) { + XcfaLocation visiting = stack.pop(); + visitedLocations.add(visiting); + for (var outgoingEdge : visiting.getOutgoingEdges()) { + var target = outgoingEdge.getTarget(); + if (visitedLocations.contains(target)) { // backward edge + backwardTransitions.add(outgoingEdge); + } else { + stack.push(target); + } + } + } + } + } + } +} diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/portfolio/ComplexPortfolio.java b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/portfolio/ComplexPortfolio.java index e3be272ea4..c6b6ffa172 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/portfolio/ComplexPortfolio.java +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/portfolio/ComplexPortfolio.java @@ -50,13 +50,13 @@ public class ComplexPortfolio extends AbstractPortfolio { private XcfaConfigBuilder.Search search = null; private XcfaConfigBuilder.Algorithm algorithm = null; - public ComplexPortfolio(Logger.Level logLevel, String modelName, String smtlibhome) throws Exception { + public ComplexPortfolio(Logger.Level logLevel, String modelName, String smtlibhome, XcfaConfigBuilder.Algorithm algorithm) throws Exception { super(logLevel, modelName, smtlibhome); // registers solver factories if (ArchitectureConfig.multiThreading) { - algorithm = XcfaConfigBuilder.Algorithm.INTERLEAVINGS; + this.algorithm = algorithm; search = XcfaConfigBuilder.Search.BFS; } else { - algorithm = XcfaConfigBuilder.Algorithm.SINGLETHREAD; + this.algorithm = XcfaConfigBuilder.Algorithm.SINGLETHREAD; search = XcfaConfigBuilder.Search.ERR; } } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.java b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.java index 4da7e64d97..db9c2493c8 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.java +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.java @@ -204,6 +204,9 @@ public class XcfaCli { @Parameter(names = "--algorithm", description = "Algorithm to use when solving multithreaded programs") XcfaConfigBuilder.Algorithm algorithm = XcfaConfigBuilder.Algorithm.SINGLETHREAD; + @Parameter(names = "--lbe", description = "Large-block encoding level") + SimpleLbePass.LBELevel lbeLevel = SimpleLbePass.LBELevel.NO_LBE; + //////////// SMTLib options //////////// @Parameter(names = "--smt-home", description = "The path of the solver registry") @@ -221,9 +224,6 @@ public class XcfaCli { @Parameter(names = "--validate-abstraction-solver", description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.") boolean validateAbstractionSolver = false; - @Parameter(names = "--lbe", description = "Large-block encoding level") - SimpleLbePass.LBELevel lbeLevel = SimpleLbePass.LBELevel.NO_LBE; - //////////// CONFIGURATION OPTIONS END //////////// private Logger logger; @@ -253,7 +253,6 @@ private void run() { File inputOrModel = input == null ? model : input; logger = new ConsoleLogger(logLevel); - ; /// version if (versionInfo) { @@ -442,7 +441,7 @@ private void run() { } break; case COMPLEX: - ComplexPortfolio complexPortfolio = new ComplexPortfolio(logLevel, this.input.getName(), home); + ComplexPortfolio complexPortfolio = new ComplexPortfolio(logLevel, this.input.getName(), home, algorithm); try { complexPortfolio.executeAnalysis(xcfa, initTime); } catch (PortfolioTimeoutException pte) { @@ -521,7 +520,7 @@ private void executeSingleConfiguration(XCFA xcfa) throws Exception { final Solver solver1 = refinementSolverFactory.createSolver(); // TODO handle separate solvers in a nicer way final Solver solver2 = abstractionSolverFactory.createSolver(); // TODO handle separate solvers in a nicer way final ExplStmtAnalysis domainAnalysis = ExplStmtAnalysis.create(solver2, True(), maxEnum); - final LTS lts = algorithm.getLts(); + final LTS lts = algorithm.getLts(xcfa); final InitFunc, XcfaPrec> initFunc = algorithm.getInitFunc(xcfa.getProcesses().stream().map(proc -> proc.getMainProcedure().getInitLoc()).collect(Collectors.toList()), domainAnalysis.getInitFunc()); final TransFunc, StmtAction, XcfaPrec> transFunc = diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/utils/FrontendXcfaBuilder.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/utils/FrontendXcfaBuilder.java index e556281eb8..c6241ce971 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/utils/FrontendXcfaBuilder.java +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/utils/FrontendXcfaBuilder.java @@ -790,39 +790,30 @@ public XcfaLocation visit(CWhile statement, ParamPack param) { builder.addLoc(outerBeforeGuard); propagateMetadata(statement, outerBeforeGuard); for (int i = 0; i < (UNROLL_COUNT == 0 ? 1 : UNROLL_COUNT); ++i) { - if (((CCompound) body).getcStatementList().size() == 0) { - final AssumeStmt assume = Assume(Eq(guard.getExpression(), CComplexType.getType(guard.getExpression()).getNullValue())); - propagateMetadata(guard, assume); - xcfaEdge = XcfaEdge.of(initLoc, endLoc, List.of(Stmt(assume))); - builder.addEdge(xcfaEdge); - propagateMetadata(statement, xcfaEdge); - return endLoc; - } else { - XcfaLocation innerLoop = getAnonymousLoc(builder); - builder.addLoc(innerLoop); - propagateMetadata(statement, innerLoop); - XcfaLocation testEndLoc = buildWithoutPostStatement(guard, new ParamPack(builder, initLoc, null, null, returnLoc)); - if (UNROLL_COUNT > 0) { - initLoc = getAnonymousLoc(builder); - builder.addLoc(initLoc); - propagateMetadata(statement, initLoc); - } - final AssumeStmt assume = Assume(Neq(guard.getExpression(), CComplexType.getType(guard.getExpression()).getNullValue())); - propagateMetadata(guard, assume); - xcfaEdge = XcfaEdge.of(testEndLoc, innerLoop, List.of(Stmt(assume))); - builder.addEdge(xcfaEdge); - propagateMetadata(statement, xcfaEdge); - final AssumeStmt assume1 = Assume(Eq(guard.getExpression(), CComplexType.getType(guard.getExpression()).getNullValue())); - propagateMetadata(guard, assume1); - xcfaEdge = XcfaEdge.of(testEndLoc, outerBeforeGuard, List.of(Stmt(assume1))); - builder.addEdge(xcfaEdge); - propagateMetadata(statement, xcfaEdge); - XcfaLocation lastGuard = buildPostStatement(guard, new ParamPack(builder, innerLoop, endLoc, initLoc, returnLoc)); - XcfaLocation lastBody = body.accept(this, new ParamPack(builder, lastGuard, endLoc, initLoc, returnLoc)); - xcfaEdge = XcfaEdge.of(lastBody, initLoc, List.of()); - builder.addEdge(xcfaEdge); - propagateMetadata(statement, xcfaEdge); + XcfaLocation innerLoop = getAnonymousLoc(builder); + builder.addLoc(innerLoop); + propagateMetadata(statement, innerLoop); + XcfaLocation testEndLoc = buildWithoutPostStatement(guard, new ParamPack(builder, initLoc, null, null, returnLoc)); + if (UNROLL_COUNT > 0) { + initLoc = getAnonymousLoc(builder); + builder.addLoc(initLoc); + propagateMetadata(statement, initLoc); } + final AssumeStmt assume = Assume(Neq(guard.getExpression(), CComplexType.getType(guard.getExpression()).getNullValue())); + propagateMetadata(guard, assume); + xcfaEdge = XcfaEdge.of(testEndLoc, innerLoop, List.of(Stmt(assume))); + builder.addEdge(xcfaEdge); + propagateMetadata(statement, xcfaEdge); + final AssumeStmt assume1 = Assume(Eq(guard.getExpression(), CComplexType.getType(guard.getExpression()).getNullValue())); + propagateMetadata(guard, assume1); + xcfaEdge = XcfaEdge.of(testEndLoc, outerBeforeGuard, List.of(Stmt(assume1))); + builder.addEdge(xcfaEdge); + propagateMetadata(statement, xcfaEdge); + XcfaLocation lastGuard = buildPostStatement(guard, new ParamPack(builder, innerLoop, endLoc, initLoc, returnLoc)); + XcfaLocation lastBody = body.accept(this, new ParamPack(builder, lastGuard, endLoc, initLoc, returnLoc)); + xcfaEdge = XcfaEdge.of(lastBody, initLoc, List.of()); + builder.addEdge(xcfaEdge); + propagateMetadata(statement, xcfaEdge); } XcfaLocation outerLastGuard = buildPostStatement(guard, new ParamPack(builder, outerBeforeGuard, null, null, null)); xcfaEdge = XcfaEdge.of(outerLastGuard, endLoc, List.of());