-
Notifications
You must be signed in to change notification settings - Fork 15
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #31 from mbeddr/modelcheck
model checking support
- Loading branch information
Showing
25 changed files
with
861 additions
and
44 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
import org.jetbrains.kotlin.gradle.tasks.KotlinCompile | ||
|
||
import java.net.URI | ||
|
||
group = "de.itemis.mps" | ||
|
||
plugins { | ||
kotlin("jvm") | ||
`maven-publish` | ||
`java-gradle-plugin` | ||
} | ||
|
||
repositories { | ||
mavenCentral() | ||
maven { | ||
url = URI("https://projects.itemis.de/nexus/content/repositories/mbeddr") | ||
} | ||
} | ||
|
||
val nexusUsername: String? by project | ||
val nexusPassword: String? by project | ||
|
||
val kotlinArgParserVersion: String by project | ||
val mpsVersion: String by project | ||
|
||
val pluginVersion = "2" | ||
|
||
version = if (project.hasProperty("forceCI") || project.hasProperty("teamcity")) { | ||
de.itemis.mps.gradle.GitBasedVersioning.getVersion(mpsVersion, pluginVersion) | ||
} else { | ||
"$mpsVersion.$pluginVersion-SNAPSHOT" | ||
} | ||
|
||
|
||
val mpsConfiguration = configurations.create("mps") | ||
|
||
dependencies { | ||
implementation(kotlin("stdlib-jdk8")) | ||
implementation("com.xenomachina:kotlin-argparser:$kotlinArgParserVersion") | ||
mpsConfiguration("com.jetbrains:mps:$mpsVersion") | ||
compileOnly(mpsConfiguration.resolve().map { zipTree(it) }.first().matching { include("lib/*.jar", "plugins/modelchecker/**/*.jar", "plugins/http-support/**/*.jar")}) | ||
implementation(project(":project-loader")) | ||
} | ||
|
||
tasks.withType<KotlinCompile> { | ||
kotlinOptions.jvmTarget = "1.8" | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,140 @@ | ||
package de.itemis.mps.gradle.modelcheck | ||
|
||
import com.xenomachina.argparser.ArgParser | ||
import com.xenomachina.argparser.mainBody | ||
import de.itemis.mps.gradle.project.loader.Args | ||
import de.itemis.mps.gradle.project.loader.executeWithProject | ||
import jetbrains.mps.checkers.* | ||
import jetbrains.mps.errors.MessageStatus | ||
import jetbrains.mps.errors.item.IssueKindReportItem | ||
import jetbrains.mps.ide.httpsupport.runtime.base.HttpSupportUtil | ||
import jetbrains.mps.ide.modelchecker.platform.actions.ModelCheckerIssueFinder | ||
import jetbrains.mps.ide.modelchecker.platform.actions.ModelCheckerSettings | ||
import jetbrains.mps.ide.modelchecker.platform.actions.UnresolvedReferencesChecker | ||
import jetbrains.mps.progress.EmptyProgressMonitor | ||
import jetbrains.mps.project.Project | ||
import jetbrains.mps.project.validation.StructureChecker | ||
import jetbrains.mps.typesystemEngine.checker.TypesystemChecker | ||
import jetbrains.mps.util.CollectConsumer | ||
import org.apache.log4j.Logger | ||
|
||
private val logger = Logger.getLogger("de.itemis.mps.gradle.generate") | ||
|
||
class ModelCheckArgs(parser: ArgParser) : Args(parser) { | ||
val models by parser.adding("--model", | ||
help = "list of models to generate") | ||
val warningAsError by parser.flagging("--warning-as-error", help = "treat model checker warning as errors") | ||
val dontFailOnError by parser.flagging("--error-no-fail", help = "report errors but don't fail the build") | ||
} | ||
|
||
fun printInfo(msg: String) { | ||
logger.info(msg) | ||
} | ||
|
||
fun printWarn(msg: String) { | ||
logger.warn(msg) | ||
} | ||
|
||
fun printError(msg: String) { | ||
logger.error(msg) | ||
} | ||
|
||
fun printResult(item: IssueKindReportItem, project: Project, args: ModelCheckArgs) { | ||
val path = IssueKindReportItem.PATH_OBJECT.get(item) | ||
|
||
val info = ::printInfo | ||
val warn = if (args.warningAsError) { | ||
::printError | ||
} else { | ||
::printWarn | ||
} | ||
|
||
val err = ::printError | ||
|
||
val print = fun (severity: MessageStatus, msg: String) { | ||
when(severity) { | ||
MessageStatus.OK -> info(msg) | ||
MessageStatus.WARNING -> warn(msg) | ||
MessageStatus.ERROR -> err(msg) | ||
} | ||
} | ||
|
||
when (path) { | ||
is IssueKindReportItem.PathObject.ModulePathObject -> { | ||
val module = path.resolve(project.repository) | ||
print(item.severity, "${item.message}[${module.moduleName}]") | ||
} | ||
is IssueKindReportItem.PathObject.ModelPathObject -> { | ||
val model = path.resolve(project.repository) | ||
print(item.severity, "${item.message} [${model.name.longName}]") | ||
} | ||
is IssueKindReportItem.PathObject.NodePathObject -> { | ||
val node = path.resolve(project.repository) | ||
val url = HttpSupportUtil.getURL(node) | ||
print(item.severity, "${item.message} [$url]") | ||
} | ||
else -> print(item.severity, item.message) | ||
} | ||
} | ||
|
||
fun modelCheckProject(args: ModelCheckArgs, project: Project) : Boolean { | ||
|
||
// see ModelCheckerSettings.getSpecificCheckers for details | ||
// we do not call into that class because we don't want to load the settings from the user | ||
val checkers = listOf(TypesystemChecker(), | ||
ConstraintsChecker(), | ||
RefScopeChecker(), | ||
TargetConceptChecker(), | ||
UsedLanguagesChecker(), | ||
StructureChecker(), | ||
ModelPropertiesChecker(), | ||
UnresolvedReferencesChecker(project), | ||
ModuleChecker()) | ||
|
||
|
||
// We don't use ModelCheckerIssueFinder because it has strange dependency on the ModelCheckerSettings which we | ||
// want to avoid when running in headless mode | ||
val errorCollector = CollectConsumer<IssueKindReportItem>() | ||
val checker = ModelCheckerBuilder(false).createChecker(checkers) | ||
|
||
val itemsToCheck = ModelCheckerBuilder.ItemsToCheck() | ||
|
||
project.modelAccess.runReadAction { | ||
if(args.models.isNotEmpty()) { | ||
itemsToCheck.models.addAll(project.projectModulesWithGenerators.flatMap { it.models }.filter { args.models.contains(it.name.longName) }) | ||
} else { | ||
itemsToCheck.models.addAll(project.projectModulesWithGenerators.flatMap { it.models }) | ||
} | ||
checker.check(itemsToCheck, project.repository, errorCollector, EmptyProgressMonitor()) | ||
|
||
// We need read access here to resolve the node pointers in the report items | ||
errorCollector.result.map{ printResult(it, project, args) } | ||
} | ||
|
||
val hasErrors = if (args.warningAsError) { | ||
errorCollector.result.any { it.severity == MessageStatus.WARNING } | ||
} else { | ||
errorCollector.result.any { it.severity == MessageStatus.ERROR } | ||
} | ||
|
||
return hasErrors | ||
} | ||
|
||
fun main(args: Array<String>) = mainBody { | ||
|
||
val parsed = ArgParser(args).parseInto(::ModelCheckArgs) | ||
var hasErrors = true | ||
try { | ||
hasErrors = executeWithProject(parsed) { project -> modelCheckProject(parsed, project) } | ||
} catch (ex: java.lang.Exception) { | ||
logger.fatal("error model checking", ex) | ||
} catch (t: Throwable) { | ||
logger.fatal("error model checking", t) | ||
} | ||
|
||
if (hasErrors && !parsed.dontFailOnError) { | ||
System.exit(-1) | ||
} | ||
|
||
System.exit(0) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,5 +1,5 @@ | ||
rootProject.name = "mps-gradle-plugin" | ||
include("execute-generators") | ||
include("project-loader") | ||
|
||
enableFeaturePreview("STABLE_PUBLISHING") | ||
include("modelcheck") | ||
enableFeaturePreview("STABLE_PUBLISHING") |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
package de.itemis.mps.gradle | ||
|
||
import org.gradle.api.GradleException | ||
import org.gradle.api.Project | ||
import org.gradle.api.artifacts.Configuration | ||
import java.io.File | ||
|
||
data class Plugin( | ||
var id: String, | ||
var path: String | ||
) | ||
|
||
data class Macro( | ||
var name: String, | ||
var value: String | ||
) | ||
|
||
open class BasePluginExtensions { | ||
lateinit var mpsConfig: Configuration | ||
var mpsLocation: File? = null | ||
var plugins: List<Plugin> = emptyList() | ||
var pluginLocation: File? = null | ||
var macros: List<Macro> = emptyList() | ||
var projectLocation: File? = null | ||
var debug = false | ||
} | ||
|
||
fun argsFromBaseExtension(extensions: BasePluginExtensions): MutableList<String> { | ||
val pluginLocation = if (extensions.pluginLocation != null) { | ||
sequenceOf("--plugin-location=${extensions.pluginLocation!!.absolutePath}") | ||
} else { | ||
emptySequence() | ||
} | ||
|
||
|
||
val projectLocation = extensions.projectLocation ?: throw GradleException("No project path set") | ||
val prj = sequenceOf("--project=${projectLocation.absolutePath}") | ||
|
||
return sequenceOf(pluginLocation, | ||
extensions.plugins.map { "--plugin=${it.id}:${it.path}" }.asSequence(), | ||
extensions.macros.map { "--macro=${it.name}:${it.value}" }.asSequence(), | ||
prj).flatten().toMutableList() | ||
} |
Oops, something went wrong.