Commit d5059645 authored by Martin Eisenmann's avatar Martin Eisenmann

Merge remote-tracking branch 'origin/master' into 4016

parents 98e83e07 7c7c6d67
...@@ -14,8 +14,18 @@ Require-Bundle: org.fortiss.af3.exploration, ...@@ -14,8 +14,18 @@ Require-Bundle: org.fortiss.af3.exploration,
com.microsoft.z3, com.microsoft.z3,
org.fortiss.af3.platform.hierarchic, org.fortiss.af3.platform.hierarchic,
org.fortiss.af3.safety;visibility:=reexport, org.fortiss.af3.safety;visibility:=reexport,
org.fortiss.tooling.kernel.ui org.fortiss.tooling.kernel.ui,
Export-Package: org.fortiss.af3.exploration.smt.backend, com.google.guava
Export-Package: org.fortiss.af3.exploration.smt,
org.fortiss.af3.exploration.smt.backend,
org.fortiss.af3.exploration.smt.migrate,
org.fortiss.af3.exploration.smt.model,
org.fortiss.af3.exploration.smt.model.dseml,
org.fortiss.af3.exploration.smt.model.dseml.impl,
org.fortiss.af3.exploration.smt.model.dseml.util,
org.fortiss.af3.exploration.smt.model.impl,
org.fortiss.af3.exploration.smt.model.util,
org.fortiss.af3.exploration.smt.modeltransformation, org.fortiss.af3.exploration.smt.modeltransformation,
org.fortiss.af3.exploration.smt.solver,
org.fortiss.af3.exploration.smt.util, org.fortiss.af3.exploration.smt.util,
test.org.fortiss.af3.exploration.smt test.org.fortiss.af3.exploration.smt
AF3ExplorationSMTActivator.java 499ee7e7485e622615a4f78be5d2e4f1ca8f235a GREEN AF3ExplorationSMTActivator.java db8c07de55429ead58b5127affc48232e31819d3 YELLOW
...@@ -16,6 +16,8 @@ ...@@ -16,6 +16,8 @@
package org.fortiss.af3.exploration.smt; package org.fortiss.af3.exploration.smt;
import org.eclipse.core.runtime.Plugin; import org.eclipse.core.runtime.Plugin;
import org.fortiss.af3.exploration.smt.cli.DumpSMTLibFileCommandLineHandler;
import org.fortiss.tooling.kernel.service.ICommandLineInterfaceService;
import org.osgi.framework.BundleContext; import org.osgi.framework.BundleContext;
/** /**
...@@ -36,6 +38,9 @@ public class AF3ExplorationSMTActivator extends Plugin { ...@@ -36,6 +38,9 @@ public class AF3ExplorationSMTActivator extends Plugin {
public void start(BundleContext context) throws Exception { public void start(BundleContext context) throws Exception {
super.start(context); super.start(context);
plugin = this; plugin = this;
ICommandLineInterfaceService cliService = ICommandLineInterfaceService.getInstance();
cliService.registerHandler("--dump-smtlib", new DumpSMTLibFileCommandLineHandler());
} }
/** {@inheritDoc} */ /** {@inheritDoc} */
......
Z3Backend.java d58fc12855dc3597e52fe0fe59cb2607d77d5583 GREEN Z3Backend.java c217750b1183c51c4f4952919d70e22b2576d7fa GREEN
...@@ -15,41 +15,32 @@ ...@@ -15,41 +15,32 @@
+--------------------------------------------------------------------------*/ +--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.backend; package org.fortiss.af3.exploration.smt.backend;
import static org.fortiss.af3.exploration.smt.modeltransformation.BasicDeploScheduleConstraint.generateDeploScheduleConstraints; import static com.google.common.collect.Sets.newHashSet;
import static org.fortiss.af3.exploration.smt.modeltransformation.BasicDeploScheduleConstraint.generateDeploScheduleSpecificConstraints; import static org.fortiss.af3.exploration.service.IDSEBackend.EXPLORATION_TYPE.FEASIBILITY_CHECK;
import static org.fortiss.af3.exploration.smt.modeltransformation.BasicDeploymentConstraint.createBasicSignalConstraints; import static org.fortiss.af3.exploration.service.IDSEBackend.EXPLORATION_TYPE.OPTIMIZATION;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createSolverSettings;
import static org.fortiss.af3.exploration.util.ExplorationUtils.isDebugVerboseEnabled; import static org.fortiss.af3.exploration.util.ExplorationUtils.isDebugVerboseEnabled;
import java.util.ArrayList; import java.util.Collection;
import java.util.HashSet; import java.util.HashMap;
import java.util.List; import java.util.Map;
import java.util.Optional; import java.util.Optional;
import java.util.Set; import java.util.Set;
import org.eclipse.core.runtime.IProgressMonitor; import org.eclipse.core.runtime.IProgressMonitor;
import org.fortiss.af3.exploration.model.ExplorationSpecification; import org.fortiss.af3.exploration.model.ExplorationSpecification;
import org.fortiss.af3.exploration.model.IExplorationConstraint;
import org.fortiss.af3.exploration.model.IExplorationTarget; import org.fortiss.af3.exploration.model.IExplorationTarget;
import org.fortiss.af3.exploration.model.SuperSetMap; import org.fortiss.af3.exploration.model.SolverSettings;
import org.fortiss.af3.exploration.model.solutions.ExplorationSolution; import org.fortiss.af3.exploration.model.solutions.ExplorationSolution;
import org.fortiss.af3.exploration.model.synthesiscategory.IDeploymentSynthesis;
import org.fortiss.af3.exploration.model.synthesiscategory.IPlatformSynthesis;
import org.fortiss.af3.exploration.model.synthesiscategory.IScheduleSynthesis;
import org.fortiss.af3.exploration.model.synthesiscategory.ISynthesisCategory;
import org.fortiss.af3.exploration.service.IDSEBackend; import org.fortiss.af3.exploration.service.IDSEBackend;
import org.fortiss.af3.exploration.smt.modeltransformation.BasicScheduleConstraint; import org.fortiss.af3.exploration.smt.solver.DeploScheduleRun;
import org.fortiss.af3.exploration.smt.modeltransformation.DeploScheduleRun; import org.fortiss.af3.exploration.smt.solver.DeploymentRun;
import org.fortiss.af3.exploration.smt.modeltransformation.DeploymentRun; import org.fortiss.af3.exploration.smt.solver.ScheduleRun;
import org.fortiss.af3.exploration.smt.modeltransformation.ScheduleRun; import org.fortiss.af3.exploration.smt.solver.SolverRun;
import org.fortiss.af3.exploration.smt.modeltransformation.SolverRun;
import org.fortiss.af3.platform.model.ExecutionUnit;
import org.fortiss.af3.platform.model.Route;
import org.fortiss.af3.schedule.model.ResourceAllocation;
import org.fortiss.af3.schedule.model.Schedule;
import org.fortiss.af3.task.model.Signal;
import org.fortiss.af3.task.model.Task;
import org.fortiss.af3.task.model.allocation.ComponentToTaskAllocationEntry;
import org.fortiss.af3.task.model.allocation.SignalToRouteAllocationEntry;
import org.fortiss.af3.task.model.allocation.TaskToExecutionUnitAllocationEntry;
import org.fortiss.af3.task.model.allocation.TaskToExecutionUnitAllocationTable;
import org.fortiss.af3.task.model.allocation.TaskWcetTable;
import org.fortiss.tooling.base.model.element.IModelElement;
/** /**
* DSE backend that uses Z3 to solve a given DSE problem. It translates a problem statement in form * DSE backend that uses Z3 to solve a given DSE problem. It translates a problem statement in form
...@@ -60,6 +51,9 @@ import org.fortiss.tooling.base.model.element.IModelElement; ...@@ -60,6 +51,9 @@ import org.fortiss.tooling.base.model.element.IModelElement;
*/ */
public class Z3Backend implements IDSEBackend { public class Z3Backend implements IDSEBackend {
/** Default timeout value in ms. */
private static int DEFAULT_TIMEOUT = 50 * 1000;
/** {@inheritDoc} */ /** {@inheritDoc} */
@Override @Override
public void validateExplorationSpecification(ExplorationSpecification spec) throws Exception { public void validateExplorationSpecification(ExplorationSpecification spec) throws Exception {
...@@ -68,85 +62,32 @@ public class Z3Backend implements IDSEBackend { ...@@ -68,85 +62,32 @@ public class Z3Backend implements IDSEBackend {
/** {@inheritDoc} */ /** {@inheritDoc} */
@Override @Override
public Set<Class<?>> getSynthesizedArtifacts() { public Map<Class<? extends ISynthesisCategory>, String> getSynthesisTypes() {
Set<Class<?>> synthArtifacts = new HashSet<>(); Map<Class<? extends ISynthesisCategory>, String> catMap = new HashMap<>();
synthArtifacts.add(TaskToExecutionUnitAllocationTable.class); catMap.put(IPlatformSynthesis.class, "Platform");
synthArtifacts.add(Schedule.class); catMap.put(IDeploymentSynthesis.class, "Deployment");
return synthArtifacts; catMap.put(IScheduleSynthesis.class, "Schedule");
return catMap;
} }
/** {@inheritDoc} */ /** {@inheritDoc} */
@Override @Override
public Optional<ExplorationSolution> executeDSE(ExplorationSpecification spec, public Set<EXPLORATION_TYPE> getExplorationTypes() {
Set<Class<? extends IModelElement>> solutionTypes, IProgressMonitor monitor, return newHashSet(FEASIBILITY_CHECK, OPTIMIZATION);
int timeoutMS) throws Exception { }
// For SMT, we must add constraints in the correct order: user last.
List<IExplorationTarget<?>> inputTargets = new ArrayList<>(spec.getTargets());
spec.getTargets().clear();
List<IExplorationTarget<?>> basicConstraints = new ArrayList<>();
SuperSetMap superSets = spec.getSearchSpace();
SolverRun solverRun;
if(solutionTypes.contains(TaskToExecutionUnitAllocationTable.class)) {
// Add SMT-specific constraints to define the basic deployment problem.
basicConstraints.addAll(createBasicSignalConstraints(superSets));
if(solutionTypes.contains(Schedule.class)) { /** {@inheritDoc} */
// Case deployment+schedule run @Override
// Add SMT-specific constraints to define the deployment+schedule problem. public SolverSettings getSolverSettings() {
List<IExplorationConstraint<?>> basicDeploScheduleConstraints = return createSolverSettings(DEFAULT_TIMEOUT, 0);
generateDeploScheduleConstraints(superSets.get(ResourceAllocation.class), }
superSets.get(Task.class), superSets.get(Signal.class),
superSets.get(ExecutionUnit.class), superSets.get(Route.class),
superSets.get(ComponentToTaskAllocationEntry.class),
superSets.get(TaskWcetTable.class));
basicConstraints.addAll(basicDeploScheduleConstraints);
// TODO (#3361): Generation of causality constraints is for now kept separated,
// because of the different treatment of routing in the pure schedule case
basicConstraints.addAll(generateDeploScheduleSpecificConstraints(superSets));
if(isDebugVerboseEnabled()) {
System.out.println("DeploScheduleRun");
}
solverRun = new DeploScheduleRun();
} else {
// Case pure deployment run
if(isDebugVerboseEnabled()) {
System.out.println("DeploymentRun");
}
solverRun = new DeploymentRun();
}
} else {
// Case pure schedule run
// Add SMT-specific constraints to define the deployment+schedule problem.
List<IExplorationConstraint<?>> basicDeploScheduleConstraints =
generateDeploScheduleConstraints(superSets.get(ResourceAllocation.class),
superSets.get(Task.class), superSets.get(Signal.class),
superSets.get(ExecutionUnit.class), superSets.get(Route.class),
superSets.get(ComponentToTaskAllocationEntry.class),
superSets.get(TaskWcetTable.class));
// Add SMT-specific constraints to define the schedule problem, in the case when a
// deployment is given
List<IExplorationConstraint<?>> basicScheduleConstraints = BasicScheduleConstraint
.generatePureScheduleConstraints(superSets.get(ResourceAllocation.class),
superSets.get(Task.class), superSets.get(ExecutionUnit.class),
superSets.get(ComponentToTaskAllocationEntry.class),
superSets.get(TaskToExecutionUnitAllocationEntry.class),
superSets.get(SignalToRouteAllocationEntry.class));
basicConstraints.addAll(basicDeploScheduleConstraints);
basicConstraints.addAll(basicScheduleConstraints);
if(isDebugVerboseEnabled()) {
System.out.println("ScheduleRun");
}
solverRun = new ScheduleRun();
}
spec.getTargets().addAll(basicConstraints);
spec.getTargets().addAll(inputTargets);
if(spec.getTargets().isEmpty()) { /** {@inheritDoc} */
throw new Exception("No exploration targets defined. Cannot perform DSE."); @Override
} public Optional<ExplorationSolution> executeDSE(ExplorationSpecification spec,
SolverSettings settings, IProgressMonitor monitor) throws Exception {
int timeout = settings.getTermination().getTimeoutMS().getValue();
SolverRun solverRun = createSolverRun(spec, timeout);
if(isDebugVerboseEnabled()) { if(isDebugVerboseEnabled()) {
// prints on screen the list of constraints for this run // prints on screen the list of constraints for this run
...@@ -158,16 +99,30 @@ public class Z3Backend implements IDSEBackend { ...@@ -158,16 +99,30 @@ public class Z3Backend implements IDSEBackend {
i++; i++;
} }
} }
ExplorationSolution expSolution = solverRun.solve(spec, timeoutMS, monitor);
// Remove additional input sets (that have potentially been created on the fly) ExplorationSolution expSolution = solverRun.solve(monitor);
// as well as basic constraints (only user-defined constraints shall be persisted)
superSets.removeKey(ResourceAllocation.class);
superSets.removeKey(SignalToRouteAllocationEntry.class);
spec.getTargets().removeAll(basicConstraints);
return Optional.of(expSolution); return Optional.of(expSolution);
} }
/**
* Creates a {@link SolverRun} instance that is specific for the {@link ISynthesisCategory}s of
* the given {@link ExplorationSpecification}.
*/
public SolverRun createSolverRun(ExplorationSpecification spec, int timeout) throws Exception {
Collection<Class<? extends ISynthesisCategory>> synthTypes = spec.getSynthTypes();
if(synthTypes.contains(IDeploymentSynthesis.class) &&
synthTypes.contains(IScheduleSynthesis.class)) {
return new DeploScheduleRun(spec, timeout);
} else if(synthTypes.contains(IDeploymentSynthesis.class)) {
return new DeploymentRun(spec, timeout);
} else if(synthTypes.contains(IScheduleSynthesis.class)) {
return new ScheduleRun(spec, timeout);
} else {
throw new Exception("No applicable " + SolverRun.class.getSimpleName() +
" was found for the given set of syntesises to perform.");
}
}
/** {@inheritDoc} */ /** {@inheritDoc} */
@Override @Override
public String getName() { public String getName() {
......
DumpSMTLibFileCommandLineHandler.java 95604962b4db14786ec8143663278c4a865bbd55 GREEN
/*-------------------------------------------------------------------------+
| Copyright 2020 fortiss GmbH |
| |
| 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 org.fortiss.af3.exploration.smt.cli;
import static org.fortiss.af3.exploration.service.IDSEBackend.EXPLORATION_TYPE.FEASIBILITY_CHECK;
import static org.fortiss.af3.exploration.util.ExplorationCLIUtils.findMatchingDSEProject;
import static org.fortiss.af3.exploration.util.ExplorationCLIUtils.getExplorationTypeByArgument;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationSpecification;
import static org.fortiss.tooling.common.util.LambdaUtils.getFirst;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getFirstParentWithType;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.pickInstanceOf;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.info;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.Map;
import java.util.Optional;
import java.util.Set;
import org.fortiss.af3.exploration.AF3ExplorationActivator;
import org.fortiss.af3.exploration.model.ExplorationSpecification;
import org.fortiss.af3.exploration.model.IExplorationConstraint;
import org.fortiss.af3.exploration.model.IExplorationObjective;
import org.fortiss.af3.exploration.model.IExplorationTarget;
import org.fortiss.af3.exploration.model.SolverSettings;
import org.fortiss.af3.exploration.model.project.DSE;
import org.fortiss.af3.exploration.model.project.ProcessStep;
import org.fortiss.af3.exploration.model.project.RuleSet;
import org.fortiss.af3.exploration.model.synthesiscategory.ISynthesisCategory;
import org.fortiss.af3.exploration.service.IDSEBackend;
import org.fortiss.af3.exploration.service.IDSEBackendService;
import org.fortiss.af3.exploration.smt.AF3ExplorationSMTActivator;
import org.fortiss.af3.exploration.smt.backend.Z3Backend;
import org.fortiss.af3.exploration.smt.solver.SolverRun;
import org.fortiss.af3.project.model.FileProject;
import org.fortiss.tooling.kernel.extension.ICommandLineSwitchHandler;
import com.microsoft.z3.Solver;
/**
* Handler to dump a SMT-Lib description of and exploration problem defined in a {@link DSE}
* project. To construct the {@link ExplorationSpecification} that is optimized, all defined
* {@link IExplorationConstraint}s matching the synthesis type are used.
* This handler supports only the generation of feasibility checks. It is intended to be used with
* solvers that support the SMT-Lib standard 2.5 such as CVC4.
*
* @author diewald
*/
public final class DumpSMTLibFileCommandLineHandler implements ICommandLineSwitchHandler {
/** DSE service used for the exploration. */
private final IDSEBackendService dseService = IDSEBackendService.getInstance();
/** {@inheritDoc} */
@Override
public boolean hasAdditionalArgument() {
return true;
}
/** {@inheritDoc} */
@Override
public void handleCLISwitch(String argument) {
DSE matchingDSE = findMatchingDSEProject(argument);
if(matchingDSE == null) {
return;
}
Set<Class<? extends ISynthesisCategory>> solutionType =
getExplorationTypeByArgument(argument);
if(solutionType.isEmpty()) {
return;
}
// Get & set the Z3 solver.
Optional<IDSEBackend> optBackend = getFirst(
dseService.findBySynthTypeAndName(solutionType, FEASIBILITY_CHECK, "Z3 (SMT)"));
if(!optBackend.isPresent()) {
error(AF3ExplorationActivator.getDefault(),
"Could not find the Z3 backend to perform the exploration.");
return;
}
Z3Backend z3Backend = (Z3Backend)optBackend.get();
Map<IDSEBackend, SolverSettings> settings = new HashMap<>();
settings.put(z3Backend, z3Backend.getSolverSettings());
ExplorationSpecification expSpec = constructExplorationSpecification(matchingDSE);
expSpec.getSynthTypes().addAll(solutionType);
SolverRun solverRun;
try {
solverRun = z3Backend.createSolverRun(expSpec, 1000);
} catch(Exception e) {
error(AF3ExplorationActivator.getDefault(),
"Could not create a solver run instance for the given synthesis type.", e);
return;
}
int numExplorationObjectives =
pickInstanceOf(IExplorationObjective.class, expSpec.getTargets()).size();
if(numExplorationObjectives > 0) {
info(AF3ExplorationSMTActivator.getDefault(),
"Optimization statements will not be " +
"dumped. This switch is only inteded to check feasibility of an " +
"optimization problem. For debugging optimization problems, set " +
"the environment varaible DSE_DEBUG_VERBOSE to \"true\".");
}
Solver solver = solverRun.createConstraintSolver();
String smtLibStr = "(set-logic ALL)\n" + "(check-sat)\n" + solver.toString();
String af3PrjName = getFirstParentWithType(matchingDSE, FileProject.class).getName();
solverRun.dumpSMTLibFile(smtLibStr, af3PrjName);
}
/**
* Constructs an {@link ExplorationSpecification} using all {@link IExplorationTarget}s from the
* given {@link DSE}.
*/
private ExplorationSpecification constructExplorationSpecification(DSE matchingDSE) {
ExplorationSpecification expSpec = createExplorationSpecification();
ProcessStep dseStep = matchingDSE.getCurrentStep();
expSpec.getTargets().addAll(getTargetsFromRuleSets(matchingDSE));
expSpec.setSearchSpace(dseStep.getSuperSetMap());
return expSpec;
}
/** Collects all targets referenced by {@link RuleSet}s of the given {@link DSE}. */
private static Collection<IExplorationTarget<?>> getTargetsFromRuleSets(DSE dse) {
Collection<IExplorationTarget<?>> allExplorationTargets = new ArrayList<>();
ProcessStep dseStep = dse.getCurrentStep();
for(RuleSet ruleSet : dseStep.getRuleSets()) {
allExplorationTargets = ruleSet.getExplorationTargets();
}
return allExplorationTargets;
}
}
SMTExplorationTargetMigrator.java 843c5e4b8ddb7ddb1ca6f670da6b3d3bb839fe88 GREEN SMTExplorationTargetMigrator.java c5cf1a5f40ea0a3c1b0940bdbb57950584d44af6 GREEN
...@@ -15,6 +15,7 @@ ...@@ -15,6 +15,7 @@
+--------------------------------------------------------------------------*/ +--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.migrate; package org.fortiss.af3.exploration.smt.migrate;
import static com.google.common.collect.Sets.newHashSet;
import static org.eclipse.emf.ecore.util.EcoreUtil.replace; import static org.eclipse.emf.ecore.util.EcoreUtil.replace;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationConstraint; import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationConstraint;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationObjective; import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationObjective;
...@@ -35,6 +36,7 @@ import org.fortiss.af3.exploration.model.project.DSE; ...@@ -35,6 +36,7 @@ import org.fortiss.af3.exploration.model.project.DSE;
import org.fortiss.af3.exploration.model.project.RuleSet; import org.fortiss.af3.exploration.model.project.RuleSet;
import org.fortiss.af3.exploration.model.solutions.ExplorationResult; import org.fortiss.af3.exploration.model.solutions.ExplorationResult;
import org.fortiss.af3.exploration.model.solutions.SingleExplorationSolution; import org.fortiss.af3.exploration.model.solutions.SingleExplorationSolution;
import org.fortiss.af3.exploration.model.synthesiscategory.IDeploymentSynthesis;
import org.fortiss.af3.exploration.smt.model.CustomDimension; import org.fortiss.af3.exploration.smt.model.CustomDimension;
import org.fortiss.af3.exploration.smt.model.SMTConstraint; import org.fortiss.af3.exploration.smt.model.SMTConstraint;
import org.fortiss.af3.exploration.smt.model.SMTObjective; import org.fortiss.af3.exploration.smt.model.SMTObjective;
...@@ -44,7 +46,7 @@ import org.fortiss.tooling.kernel.extension.data.ITopLevelElement; ...@@ -44,7 +46,7 @@ import org.fortiss.tooling.kernel.extension.data.ITopLevelElement;
/** /**
* Migrator for {@link SMTConstraint}s, {@link SMTObjective}s, and {@link CustomDimension}s to the * Migrator for {@link SMTConstraint}s, {@link SMTObjective}s, and {@link CustomDimension}s to the
* commonized {@link IExplorationTarget}s. * unified {@link IExplorationTarget}s.