From f564dcb9c6693612e6bf6a28b457dc96ba859c27 Mon Sep 17 00:00:00 2001 From: Isaac Amundson Date: Wed, 22 May 2024 11:28:49 -0500 Subject: [PATCH 1/6] initial cli --- com.rockwellcollins.atc.agree.cli/.classpath | 7 + com.rockwellcollins.atc.agree.cli/.gitignore | 1 + com.rockwellcollins.atc.agree.cli/.project | 28 ++ .../.settings/org.eclipse.jdt.core.prefs | 9 + .../META-INF/MANIFEST.MF | 20 ++ .../build.properties | 4 + com.rockwellcollins.atc.agree.cli/plugin.xml | 18 ++ .../atc/agree/cli/Activator.java | 45 +++ .../rockwellcollins/atc/agree/cli/Agree.java | 265 +++++++++++++++++ .../rockwellcollins/atc/agree/cli/Util.java | 272 ++++++++++++++++++ .../agree/cli/results/AgreeJsonResult.java | 5 + .../atc/agree/cli/results/AgreeOutput.java | 101 +++++++ .../cli/results/SyntaxValidationIssue.java | 52 ++++ .../cli/results/SyntaxValidationResults.java | 45 +++ 14 files changed, 872 insertions(+) create mode 100644 com.rockwellcollins.atc.agree.cli/.classpath create mode 100644 com.rockwellcollins.atc.agree.cli/.gitignore create mode 100644 com.rockwellcollins.atc.agree.cli/.project create mode 100644 com.rockwellcollins.atc.agree.cli/.settings/org.eclipse.jdt.core.prefs create mode 100644 com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF create mode 100644 com.rockwellcollins.atc.agree.cli/build.properties create mode 100644 com.rockwellcollins.atc.agree.cli/plugin.xml create mode 100644 com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java create mode 100644 com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java create mode 100644 com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Util.java create mode 100644 com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeJsonResult.java create mode 100644 com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeOutput.java create mode 100644 com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/SyntaxValidationIssue.java create mode 100644 com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/SyntaxValidationResults.java diff --git a/com.rockwellcollins.atc.agree.cli/.classpath b/com.rockwellcollins.atc.agree.cli/.classpath new file mode 100644 index 000000000..81fe078c2 --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/.classpath @@ -0,0 +1,7 @@ + + + + + + + diff --git a/com.rockwellcollins.atc.agree.cli/.gitignore b/com.rockwellcollins.atc.agree.cli/.gitignore new file mode 100644 index 000000000..ae3c17260 --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/.gitignore @@ -0,0 +1 @@ +/bin/ diff --git a/com.rockwellcollins.atc.agree.cli/.project b/com.rockwellcollins.atc.agree.cli/.project new file mode 100644 index 000000000..1bede2f08 --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/.project @@ -0,0 +1,28 @@ + + + com.rockwellcollins.atc.agree.cli + + + + + + org.eclipse.jdt.core.javabuilder + + + + + org.eclipse.pde.ManifestBuilder + + + + + org.eclipse.pde.SchemaBuilder + + + + + + org.eclipse.pde.PluginNature + org.eclipse.jdt.core.javanature + + diff --git a/com.rockwellcollins.atc.agree.cli/.settings/org.eclipse.jdt.core.prefs b/com.rockwellcollins.atc.agree.cli/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 000000000..62ef3488c --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,9 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.targetPlatform=17 +org.eclipse.jdt.core.compiler.compliance=17 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enablePreviewFeatures=disabled +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.problem.reportPreviewFeatures=warning +org.eclipse.jdt.core.compiler.release=enabled +org.eclipse.jdt.core.compiler.source=17 diff --git a/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF b/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF new file mode 100644 index 000000000..cbb6d5001 --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF @@ -0,0 +1,20 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: Cli +Bundle-SymbolicName: com.rockwellcollins.atc.agree.cli;singleton:=true +Bundle-Version: 3.1.1.qualifier +Bundle-Activator: com.rockwellcollins.atc.agree.cli.Activator +Bundle-Vendor: ROCKWELLCOLLINS +Require-Bundle: org.eclipse.ui, + org.eclipse.core.runtime, + org.eclipse.emf.ecore;bundle-version="2.27.0", + org.eclipse.xtext, + org.osate.xtext.aadl2, + com.rockwellcollins.atc.agree, + org.osate.aadl2, + org.osate.pluginsupport, + com.google.gson, + org.osate.aadl2.instantiation +Bundle-RequiredExecutionEnvironment: JavaSE-17 +Automatic-Module-Name: com.rockwellcollins.atc.agree.cli +Bundle-ActivationPolicy: lazy diff --git a/com.rockwellcollins.atc.agree.cli/build.properties b/com.rockwellcollins.atc.agree.cli/build.properties new file mode 100644 index 000000000..cc91072ec --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/build.properties @@ -0,0 +1,4 @@ +source.. = src/ +bin.includes = META-INF/,\ + .,\ + plugin.xml diff --git a/com.rockwellcollins.atc.agree.cli/plugin.xml b/com.rockwellcollins.atc.agree.cli/plugin.xml new file mode 100644 index 000000000..4264c2e41 --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/plugin.xml @@ -0,0 +1,18 @@ + + + + + + + + + + + diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java new file mode 100644 index 000000000..d2b7045cd --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java @@ -0,0 +1,45 @@ +package com.rockwellcollins.atc.agree.cli; + +import org.eclipse.osgi.service.environment.EnvironmentInfo; +import org.osgi.framework.BundleActivator; +import org.osgi.framework.BundleContext; +import org.osgi.framework.ServiceReference; + + +public class Activator implements BundleActivator { + + private static BundleContext context; + + static BundleContext getContext() { + return context; + } + + @Override + public void start(BundleContext bundleContext) throws Exception { + Activator.context = bundleContext; + } + + @Override + public void stop(BundleContext bundleContext) throws Exception { + Activator.context = null; + } + + // Gets the workspace path contained in the -data framework cmd line arg + public static String getWorkspace() { + final ServiceReference infoRef = context.getServiceReference(EnvironmentInfo.class); + if (infoRef != null) { + final EnvironmentInfo envInfo = context.getService(infoRef); + if (envInfo != null) { + context.ungetService(infoRef); + for (int i = 0; i < envInfo.getFrameworkArgs().length; ++i) { + if ("-data".equals(envInfo.getFrameworkArgs()[i].toLowerCase()) + && i < envInfo.getFrameworkArgs().length - 1) { + return envInfo.getFrameworkArgs()[i + 1]; + } + } + } + } + return null; + } + +} diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java new file mode 100644 index 000000000..54885cfb7 --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java @@ -0,0 +1,265 @@ +package com.rockwellcollins.atc.agree.cli; + +import java.io.File; +import java.util.Arrays; +import java.util.Date; +import java.util.List; + +import org.apache.commons.cli.CommandLine; +import org.apache.commons.cli.CommandLineParser; +import org.apache.commons.cli.DefaultParser; +import org.apache.commons.cli.HelpFormatter; +import org.apache.commons.cli.Option; +import org.apache.commons.cli.Options; +import org.apache.commons.cli.ParseException; +import org.eclipse.emf.common.util.URI; +import org.eclipse.emf.ecore.plugin.EcorePlugin; +import org.eclipse.emf.ecore.resource.Resource; +import org.eclipse.equinox.app.IApplication; +import org.eclipse.equinox.app.IApplicationContext; +import org.eclipse.xtext.resource.XtextResourceSet; +import org.osate.aadl2.AadlPackage; +import org.osate.aadl2.ComponentImplementation; +import org.osate.aadl2.instance.InstancePackage; +import org.osate.aadl2.instance.SystemInstance; +import org.osate.aadl2.instantiation.InstantiateModel; +import org.osate.aadl2.modelsupport.util.AadlUtil; +import org.osate.aadl2.util.Aadl2ResourceFactoryImpl; +import org.osate.aadl2.util.Aadl2Util; +import org.osate.pluginsupport.PluginSupportUtil; +import org.osate.xtext.aadl2.Aadl2StandaloneSetup; + +import com.google.inject.Injector; +import com.rockwellcollins.atc.agree.AgreeStandaloneSetup; +import com.rockwellcollins.atc.agree.cli.results.AgreeJsonResult; +import com.rockwellcollins.atc.agree.cli.results.AgreeOutput; +import com.rockwellcollins.atc.agree.cli.results.SyntaxValidationResults; + + +public class Agree implements IApplication { + + private final static String HELP = "h"; + private final static String DATA = "data"; + private final static String APPLICATION = "application"; + private final static String NO_SPLASH = "noSplash"; + private final static String PROJECT = "p"; + private final static String COMP_IMPL = "c"; + private final static String OUTPUT = "o"; + private final static String VALIDATION_ONLY = "v"; + private final static String EXIT_ON_VALIDATION_WARNING = "w"; + private final static String FILES = "f"; + + @Override + public Object start(IApplicationContext context) throws Exception { + + System.out.println("Starting AGREE analysis"); + + context.applicationRunning(); + + // Read the meta information about the plug-ins to get the annex information. + EcorePlugin.ExtensionProcessor.process(null); + + // Output Json object + final AgreeOutput output = new AgreeOutput(); + output.setDate((new Date()).toString()); + + // Process command line options + String workspace = Activator.getWorkspace(); + String projPath = null; + String component = null; + String outputPath = null; + String[] fileArray = null; + boolean exitOnValidationWarning = false; + boolean validationOnly = false; + boolean exit = false; + + // Application Args + final String[] args = (String[]) context.getArguments().get("application.args"); + System.out.println("Application args: " + Arrays.toString(args)); + System.out.println("Workspace: " + workspace); + + // create Options + final Options options = new Options(); + options.addOption(HELP, "help", false, "print this message"); + options.addOption(NO_SPLASH, false, "optional, hide the splash screen, default false"); + options.addOption(DATA, true, "required, path of workspace"); + options.addOption(APPLICATION, true, + "required, the name of this analysis (com.rockwellcollins.atc.resolute.cli.Resolute)"); + options.addOption(PROJECT, "project", true, "required, project path (relative to workspace)"); + options.addOption(COMP_IMPL, "compImpl", true, "qualified component implementation name"); + options.addOption(OUTPUT, "output", true, "output JSON file absolute path"); + options.addOption(VALIDATION_ONLY, "validationOnly", false, "validation only, default false"); + options.addOption(EXIT_ON_VALIDATION_WARNING, "exitOnValidtionWarning", false, + "exit on validation warning, default false"); + Option option = new Option(FILES, "files", true, "Supplementary AADL files (absolute paths)"); + option.setArgs(Option.UNLIMITED_VALUES); + options.addOption(option); + + // parse options + try { + final CommandLineParser parser = new DefaultParser(); + final CommandLine commandLine = parser.parse(options, args); + + if (commandLine.hasOption(HELP)) { + exit = true; + output.setStatus(AgreeOutput.INTERRUPTED); + } + if (workspace == null || workspace.isBlank()) { + exit = true; + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("A workspace must be specified."); + } + if (commandLine.hasOption(COMP_IMPL)) { + component = commandLine.getOptionValue(COMP_IMPL); + output.setComponent(component); + // expects qualified name + if (!component.contains("::")) { + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Component implementation qualified name must be specified."); + exit = true; + } + } + if (commandLine.hasOption(PROJECT)) { + projPath = workspace + File.separator + commandLine.getOptionValue(PROJECT); + output.setProject(projPath); + } else { + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Project path must be specified."); + exit = true; + } + if (commandLine.hasOption(OUTPUT)) { + outputPath = commandLine.getOptionValue(OUTPUT); + } + if (commandLine.hasOption(FILES)) { + fileArray = commandLine.getOptionValues(FILES); + } + if (commandLine.hasOption(VALIDATION_ONLY)) { + validationOnly = true; + } + if (commandLine.hasOption(EXIT_ON_VALIDATION_WARNING)) { + exitOnValidationWarning = true; + } + final String[] remainder = commandLine.getArgs(); + for (String argument : remainder) { + final String message = "WARNING: unknown arguement " + argument + + ". See --help for command line options."; + output.addStatusMessage(message); + System.err.println(message); + } + } catch (ParseException exception) { + final String message = "Parse error: " + exception.getMessage(); + System.err.println(message); + output.addStatusMessage(message); + exit = true; + } + + + if (exit) { + final HelpFormatter formatter = new HelpFormatter(); + formatter.printHelp("osate", options); + Util.writeOutput(output, outputPath); + return IApplication.EXIT_OK; + } + + // Initialize the AADL meta model + final Injector injector = new Aadl2StandaloneSetup().createInjectorAndDoEMFRegistration(); + + AgreeStandaloneSetup.doSetup(); + + // Initialize the meta model for instance models -- need both lines + Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("aaxl2", new Aadl2ResourceFactoryImpl()); + InstancePackage.eINSTANCE.eClass(); + + // Get the resource set from the Injector obtained from initializing the AADL meta model + final XtextResourceSet resourceSet = injector.getInstance(XtextResourceSet.class); + + if (resourceSet == null) { + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Unable to initialize resource set"); + Util.writeOutput(output, outputPath); + return IApplication.EXIT_OK; + } + + // Add plug-in contributions to resource set + for (URI uri : PluginSupportUtil.getContributedAadl()) { + resourceSet.getResource(uri, true); + } + + // Load project AADL files + try { + Util.loadProjectAadlFiles(projPath, fileArray, resourceSet); + } catch (Exception e) { + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage(e.getMessage()); + Util.writeOutput(output, outputPath); + return IApplication.EXIT_OK; + } + + // Validate resource set + final SyntaxValidationResults validationResults = Util.validateResourceSet(resourceSet); + // Add validation results to output + output.setSyntaxValidationResults(validationResults); + + // If there are any errors, do not continue + // Don't continue if user doesn't want any warnings + // Don't continue if user only wants to validate model + if (validationResults.getErrors() > 0 || (exitOnValidationWarning && validationResults.getWarnings() > 0)) { + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Syntax validation issues found."); + Util.writeOutput(output, outputPath); + return IApplication.EXIT_OK; + } else if (validationOnly) { + output.setStatus(AgreeOutput.COMPLETED); + Util.writeOutput(output, outputPath); + return IApplication.EXIT_OK; + } + + // Run AGREE + ComponentImplementation compImpl = null; + for (Resource resource : resourceSet.getResources()) { + + if (!resource.getContents().isEmpty() && resource.getContents().get(0) instanceof AadlPackage) { + final AadlPackage pkg = (AadlPackage) resource.getContents().get(0); + if (pkg.getName().equalsIgnoreCase(Aadl2Util.getPackageName(component))) { + + compImpl = (ComponentImplementation) AadlUtil.findNamedElementInList( + AadlUtil.getAllComponentImpl(pkg), Aadl2Util.getItemNameWithoutQualification(component)); + break; + } + } + } + if (compImpl != null) { + try { + final SystemInstance si = InstantiateModel.instantiate(compImpl); + final List results = runAgree(); + output.setStatus(AgreeOutput.COMPLETED); + output.setResults(results); + Util.writeOutput(output, outputPath); + } catch (Exception e) { + e.printStackTrace(); + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage(e.getMessage()); + Util.writeOutput(output, outputPath); + return IApplication.EXIT_OK; + } + } else { + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Could not find component implementation in project."); + Util.writeOutput(output, outputPath); + return IApplication.EXIT_OK; + } + + return IApplication.EXIT_OK; + + } + + private List runAgree() { + return null; + } + + @Override + public void stop() { + + } + +} diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Util.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Util.java new file mode 100644 index 000000000..d16d819d1 --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Util.java @@ -0,0 +1,272 @@ +package com.rockwellcollins.atc.agree.cli; + +import java.io.File; +import java.io.FileWriter; +import java.io.IOException; +import java.io.InputStream; +import java.net.URL; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +import javax.xml.parsers.DocumentBuilder; +import javax.xml.parsers.DocumentBuilderFactory; + +import org.eclipse.emf.common.util.URI; +import org.eclipse.emf.ecore.resource.Resource; +import org.eclipse.emf.ecore.resource.ResourceSet; +import org.eclipse.xtext.diagnostics.Severity; +import org.eclipse.xtext.resource.XtextResource; +import org.eclipse.xtext.resource.XtextResourceSet; +import org.eclipse.xtext.util.CancelIndicator; +import org.eclipse.xtext.validation.CheckMode; +import org.eclipse.xtext.validation.IResourceValidator; +import org.eclipse.xtext.validation.Issue; +import org.w3c.dom.Document; +import org.w3c.dom.Node; +import org.w3c.dom.NodeList; + +import com.google.gson.Gson; +import com.google.gson.GsonBuilder; +import com.google.gson.stream.JsonWriter; +import com.rockwellcollins.atc.agree.cli.results.AgreeOutput; +import com.rockwellcollins.atc.agree.cli.results.SyntaxValidationIssue; +import com.rockwellcollins.atc.agree.cli.results.SyntaxValidationResults; + + +public class Util { + + // Load project specific AADL files + public static void loadProjectAadlFiles(String projPath, String[] libArray, XtextResourceSet resourceSet) + throws Exception { + + final List projectFiles = findFiles(Paths.get(projPath), "aadl"); + final File projectRootDirectory = new File(projPath); + final File projectFile = new File(projectRootDirectory, ".project"); + final String projName = getProjectName(projectFile); + + for (String pFile : projectFiles) { + final File projFile = new File(pFile); + loadFile(projectRootDirectory, projName, projFile, resourceSet); + } + + // load user specified AADL libs + if (libArray != null) { + for (String libName : libArray) { + loadLibFile(libName, resourceSet); + } + } + + // load referenced project AADL files + final String projParentPath = projectRootDirectory.getParent(); + final List refProjNames = new ArrayList<>(); + getRefProjName(refProjNames, projName, projParentPath); + for (String refProjName : refProjNames) { + // assuming reference project is at the same level of main project + final File refProj = new File(projParentPath, refProjName); + final List refProjFileNames = findFiles(refProj.toPath(), "aadl"); + for (String refProjFileName : refProjFileNames) { + final File refProjFile = new File(refProjFileName); + loadFile(projectRootDirectory, projName, refProjFile, resourceSet); + } + } + } + + // Validation resource set + public static SyntaxValidationResults validateResourceSet(XtextResourceSet resourceSet) { + + final List syntaxValidationIssues = new ArrayList<>(); + int numErrors = 0; + int numWarnings = 0; + for (Resource resource : resourceSet.getResources()) { + if (resource.getURI().isPlatformResource()) { +// System.out.println("Validating " + resource.getURI().toString()); + final IResourceValidator validator = ((XtextResource) resource).getResourceServiceProvider() + .getResourceValidator(); + final List issues = validator.validate(resource, CheckMode.ALL, CancelIndicator.NullImpl); + for (Issue issue : issues) { + final SyntaxValidationIssue valIssue = new SyntaxValidationIssue(); + if (issue.getSeverity().equals(Severity.ERROR)) { + ++numErrors; + valIssue.setSeverity("error"); + } else if (issue.getSeverity().equals(Severity.WARNING)) { + ++numWarnings; + valIssue.setSeverity("warning"); + } + valIssue.setIssue(issue.getMessage()); + valIssue.setFile(resource.getURI().toPlatformString(true)); + valIssue.setLine(issue.getLineNumber()); + syntaxValidationIssues.add(valIssue); +// System.out.println(issue.getMessage()); + } + } + } + + return new SyntaxValidationResults(numWarnings, numErrors, syntaxValidationIssues); + } + + private static List findFiles(Path path, String fileExtension) throws Exception { + + if (!Files.isDirectory(path)) { + throw new IllegalArgumentException("Path must be a directory!"); + } + + final List result; + + try (Stream walk = Files.walk(path)) { + result = walk + .filter(p -> !Files.isDirectory(p)) + .map(p -> p.toString().toLowerCase()) + .filter(f -> f.endsWith(fileExtension)) + .collect(Collectors.toList()); + } + return result; + } + + /** Adapted from + * here. + * + * load file as Xtext resource into resource set + * @param filePath String + * @param rs ResourceSet + * @return + */ + //https://github.com/sireum/osate-plugin/blob/master/org.sireum.aadl.osate/src/main/java/org/sireum/aadl/osate/util/AadlProjectUtil.java + + private static Resource loadFile(File projectRootDirectory, String projectName, File file, ResourceSet rs) + throws Exception { + + final URL url = new URL("file:" + file.getAbsolutePath()); + InputStream stream = null; + try { + stream = url.openConnection().getInputStream(); + } catch (Exception ex) { + throw new Exception("Error loading file " + file.toString()); + } + + final String normalizedRelPath = relativize(projectRootDirectory, file).replace("\\", "/"); + + // came up with this uri by comparing what OSATE IDE serialized AIR produces + final URI resourceUri = URI.createPlatformResourceURI(projectName + "/" + normalizedRelPath, true); + final Resource res = rs.createResource(resourceUri); + if (res == null) { + throw new Exception("Error loading file " + projectName + "/" + normalizedRelPath); + } + try { +// System.out.println("Loading " + file.getAbsolutePath()); + res.load(stream, Collections.EMPTY_MAP); + return res; + } catch (IOException e) { + throw new Exception("Error loading file " + projectName + "/" + normalizedRelPath); + } + } + + // User specified AADL file path may be outside workspace, cannot use relative path from main project + private static Resource loadLibFile(String filePath, ResourceSet rs) { + try { + final URL url = new URL("file:" + filePath); + final InputStream stream = url.openConnection().getInputStream(); + + final Path path = Paths.get(filePath); + final URI resourceUri = URI.createPlatformResourceURI("Lib/" + path.getFileName().toString(), true); + final Resource res = rs.createResource(resourceUri); + +// System.out.println("Loading " + filePath); + res.load(stream, Collections.EMPTY_MAP); + return res; + } catch (IOException e) { +// System.err.println("Error loading file " + filePath); + return null; + } + } + + private static String relativize(File root, File other) { + return Paths.get(root.toURI()).relativize(Paths.get(other.toURI())).toString(); + } + + private static String getProjectName(File projectFile) throws Exception { + final DocumentBuilderFactory factory = DocumentBuilderFactory.newInstance(); + final DocumentBuilder builder = factory.newDocumentBuilder(); + final Document doc = builder.parse(projectFile); + doc.getDocumentElement().normalize(); + final org.w3c.dom.Element root = doc.getDocumentElement(); + final NodeList list = doc.getElementsByTagName("name"); + + for (int i = 0; i < list.getLength(); i++) { + final Node node = list.item(i); + if (node.getNodeType() == Node.ELEMENT_NODE) { + final org.w3c.dom.Element element = (org.w3c.dom.Element) node; + // "name" tag could be used at lower level e.g. "" + if (element.getParentNode().isEqualNode(root)) { + return element.getTextContent(); + } + } + } + throw new Exception("Error getting project name from file " + projectFile.toString()); + } + + // A reference project could depend on another reference project + private static void getRefProjName(List list, String project, String parent) throws Exception { + + final File refProj = new File(parent, project); + final File projectFile = new File(refProj, ".project"); + final List refProjList = getReferenceProjectName(projectFile); + if (!refProjList.isEmpty()) { + for (String refProjName : refProjList) { + // avoid duplicate and break circular reference + if (!list.contains(refProjName)) { + list.add(refProjName); + getRefProjName(list, refProjName, parent); + } + } + } + } + + private static List getReferenceProjectName(File projectFile) throws Exception { + final List refProjNameList = new ArrayList<>(); + final DocumentBuilderFactory factory = DocumentBuilderFactory.newInstance(); + final DocumentBuilder builder = factory.newDocumentBuilder(); + final Document doc = builder.parse(projectFile); + doc.getDocumentElement().normalize(); + final NodeList list = doc.getElementsByTagName("projects"); + + for (int i = 0; i < list.getLength(); i++) { + final Node node = list.item(i); + if (node.getNodeType() == Node.ELEMENT_NODE) { + final org.w3c.dom.Element element = (org.w3c.dom.Element) node; + final Node projNode = element.getElementsByTagName("project").item(0); + // Handle empty reference project list + if (projNode != null) { + refProjNameList.add(projNode.getTextContent()); + } + } + } + return refProjNameList; + } + + public static void writeOutput(AgreeOutput output, String outputPath) { + + // Convert to json + final Gson gson = new GsonBuilder().setPrettyPrinting().create(); + try { + if (outputPath != null) { + final File outputFile = new File(outputPath); + final JsonWriter jsonWriter = new JsonWriter(new FileWriter(outputFile)); + jsonWriter.setIndent(" "); + gson.toJson(output, output.getClass(), jsonWriter); + jsonWriter.close(); + } + } catch (Exception e) { + System.out.println("Error writing to " + outputPath); + } + + // Write to std out + System.out.println(gson.toJson(output)); + } + +} diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeJsonResult.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeJsonResult.java new file mode 100644 index 000000000..e3addcc77 --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeJsonResult.java @@ -0,0 +1,5 @@ +package com.rockwellcollins.atc.agree.cli.results; + +public class AgreeJsonResult { + +} diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeOutput.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeOutput.java new file mode 100644 index 000000000..c3f625869 --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeOutput.java @@ -0,0 +1,101 @@ +package com.rockwellcollins.atc.agree.cli.results; + +import java.util.ArrayList; +import java.util.List; + + +public class AgreeOutput { + + public final static String COMPLETED = "Analysis Completed"; + public final static String INTERRUPTED = "Analysis Interrupted"; + + private String date; + private String project; + private String component; + private ArrayList statusMessages; + private String status; + private SyntaxValidationResults syntaxValidation; + private List results; + + public AgreeOutput() { + + } + + public AgreeOutput(AgreeOutput output) { + setDate(output.getDate()); + setProject(output.getProject()); + setComponent(output.getComponent()); + setStatusMessages(output.getStatusMessages()); + setStatus(output.getStatus()); + setSyntaxValidationResults(output.getSyntaxValidationResults()); + } + + public String getDate() { + return this.date; + } + + public String getProject() { + return this.project; + } + + public String getComponent() { + return this.component; + } + + public String getStatus() { + return this.status; + } + + public ArrayList getStatusMessages() { + return this.statusMessages; + } + + public SyntaxValidationResults getSyntaxValidationResults() { + return this.syntaxValidation; + } + + public void setDate(String date) { + this.date = date; + } + + public void setProject(String project) { + this.project = project; + } + + public void setComponent(String component) { + this.component = component; + } + + public void setStatus(String status) { + this.status = status; + } + + public void setStatusMessages(ArrayList statusMessages) { +// if (this.message == null || this.message.isBlank()) { +// this.message = message; +// } else { +// this.message += System.lineSeparator() + message; +// } + this.statusMessages = statusMessages; + } + + public void addStatusMessage(String statusMessages) { + if (this.statusMessages == null) { + this.statusMessages = new ArrayList<>(); + } + this.statusMessages.add(statusMessages); + } + + public void setSyntaxValidationResults(SyntaxValidationResults syntaxValidationResults) { + this.syntaxValidation = syntaxValidationResults; + } + + public List getResults() { + return this.results; + } + + public void setResults(List results) { + this.results = results; + } + +} diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/SyntaxValidationIssue.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/SyntaxValidationIssue.java new file mode 100644 index 000000000..ed672b0ce --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/SyntaxValidationIssue.java @@ -0,0 +1,52 @@ +package com.rockwellcollins.atc.agree.cli.results; + +public class SyntaxValidationIssue { + private String severity; + private String issue; + private String file; + private int line; + + public SyntaxValidationIssue() { + + } + + public SyntaxValidationIssue(String severity, String issue, String file, int line) { + this.severity = severity; + this.issue = issue; + this.file = file; + this.line = line; + } + + public String getSeverity() { + return this.severity; + } + + public String getIssue() { + return this.issue; + } + + public String getFile() { + return this.file; + } + + public int getLine() { + return this.line; + } + + public void setSeverity(String severity) { + this.severity = severity; + } + + public void setIssue(String issue) { + this.issue = issue; + } + + public void setFile(String file) { + this.file = file; + } + + public void setLine(int line) { + this.line = line; + } + +} diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/SyntaxValidationResults.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/SyntaxValidationResults.java new file mode 100644 index 000000000..ab365f1f8 --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/SyntaxValidationResults.java @@ -0,0 +1,45 @@ +package com.rockwellcollins.atc.agree.cli.results; + +import java.util.List; + +public class SyntaxValidationResults { + private int warnings; + private int errors; + private List issues; + + public SyntaxValidationResults() { + + } + + public SyntaxValidationResults(int warnings, int errors, List issues) { + this.warnings = warnings; + this.errors = errors; + if (!issues.isEmpty()) { + this.issues = issues; + } + } + + public int getWarnings() { + return this.warnings; + } + + public int getErrors() { + return this.errors; + } + + public List getIssues() { + return this.issues; + } + + public void setWarnings(int warnings) { + this.warnings = warnings; + } + + public void setErrors(int errors) { + this.errors = errors; + } + + public void setIssues(List issues) { + this.issues = issues; + } +} From a8e203e08363e94012d513f26587385c73c46ac6 Mon Sep 17 00:00:00 2001 From: Isaac Amundson Date: Sat, 25 May 2024 16:55:44 -0500 Subject: [PATCH 2/6] verify single layer --- .../META-INF/MANIFEST.MF | 4 +- com.rockwellcollins.atc.agree.cli/.classpath | 2 + com.rockwellcollins.atc.agree.cli/.gitignore | 2 + .../META-INF/MANIFEST.MF | 10 +- .../build.properties | 5 +- com.rockwellcollins.atc.agree.cli/pom.xml | 116 ++++++ .../atc/agree/cli/Activator.java | 19 +- .../rockwellcollins/atc/agree/cli/Agree.java | 380 +++++++++++++++++- .../META-INF/MANIFEST.MF | 4 +- .../feature.xml | 14 + .../META-INF/MANIFEST.MF | 2 +- pom.xml | 1 + 12 files changed, 534 insertions(+), 25 deletions(-) create mode 100644 com.rockwellcollins.atc.agree.cli/pom.xml diff --git a/com.rockwellcollins.atc.agree.analysis/META-INF/MANIFEST.MF b/com.rockwellcollins.atc.agree.analysis/META-INF/MANIFEST.MF index 76dde8697..b3849d0d9 100644 --- a/com.rockwellcollins.atc.agree.analysis/META-INF/MANIFEST.MF +++ b/com.rockwellcollins.atc.agree.analysis/META-INF/MANIFEST.MF @@ -14,8 +14,8 @@ Require-Bundle: org.eclipse.ui;bundle-version="[3.119.0,4.0.0)", org.osate.aadl2;bundle-version="[5.0.0,6.0.0)", org.osate.ui;bundle-version="[6.0.0,7.0.0)", org.osate.xtext.aadl2.properties;bundle-version="[3.0.0,4.0.0)", - com.rockwellcollins.atc.agree;bundle-version="[3.0.0,4.0.0)", - com.rockwellcollins.atc.agree.ui;bundle-version="[3.1.0,4.0.0)", + com.rockwellcollins.atc.agree;bundle-version="[3.1.0,4.0.0)", + com.rockwellcollins.atc.agree.ui;bundle-version="[3.2.0,4.0.0)", org.osate.ge;bundle-version="[3.0.0,4.0.0)", org.eclipse.emf.ecore;bundle-version="[2.23.0,3.0.0)", com.collins.trustedsystems.z3;bundle-version="[4.0.0,5.0.0)", diff --git a/com.rockwellcollins.atc.agree.cli/.classpath b/com.rockwellcollins.atc.agree.cli/.classpath index 81fe078c2..0a272a96b 100644 --- a/com.rockwellcollins.atc.agree.cli/.classpath +++ b/com.rockwellcollins.atc.agree.cli/.classpath @@ -1,5 +1,7 @@ + + diff --git a/com.rockwellcollins.atc.agree.cli/.gitignore b/com.rockwellcollins.atc.agree.cli/.gitignore index ae3c17260..a861e9273 100644 --- a/com.rockwellcollins.atc.agree.cli/.gitignore +++ b/com.rockwellcollins.atc.agree.cli/.gitignore @@ -1 +1,3 @@ /bin/ +/lib/ +/target/ diff --git a/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF b/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF index cbb6d5001..845ada5bd 100644 --- a/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF +++ b/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF @@ -2,7 +2,7 @@ Manifest-Version: 1.0 Bundle-ManifestVersion: 2 Bundle-Name: Cli Bundle-SymbolicName: com.rockwellcollins.atc.agree.cli;singleton:=true -Bundle-Version: 3.1.1.qualifier +Bundle-Version: 1.0.100 Bundle-Activator: com.rockwellcollins.atc.agree.cli.Activator Bundle-Vendor: ROCKWELLCOLLINS Require-Bundle: org.eclipse.ui, @@ -13,8 +13,12 @@ Require-Bundle: org.eclipse.ui, com.rockwellcollins.atc.agree, org.osate.aadl2, org.osate.pluginsupport, - com.google.gson, - org.osate.aadl2.instantiation + org.osate.aadl2.instantiation, + com.collins.trustedsystems.jkindapi, + com.rockwellcollins.atc.agree.analysis Bundle-RequiredExecutionEnvironment: JavaSE-17 Automatic-Module-Name: com.rockwellcollins.atc.agree.cli Bundle-ActivationPolicy: lazy +Bundle-ClassPath: lib/commons-cli.jar, + lib/gson.jar, + . diff --git a/com.rockwellcollins.atc.agree.cli/build.properties b/com.rockwellcollins.atc.agree.cli/build.properties index cc91072ec..ca214f145 100644 --- a/com.rockwellcollins.atc.agree.cli/build.properties +++ b/com.rockwellcollins.atc.agree.cli/build.properties @@ -1,4 +1,7 @@ source.. = src/ bin.includes = META-INF/,\ .,\ - plugin.xml + plugin.xml,\ + lib/gson.jar,\ + lib/commons-cli.jar + diff --git a/com.rockwellcollins.atc.agree.cli/pom.xml b/com.rockwellcollins.atc.agree.cli/pom.xml new file mode 100644 index 000000000..a216297fa --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/pom.xml @@ -0,0 +1,116 @@ + + + 4.0.0 + + com.rockwellcollins.atc.agree + com.rockwellcollins.atc.agree.parent + 3.0.2 + + com.rockwellcollins.atc.agree.cli + 1.0.100 + eclipse-plugin + + 1.5.0 + 2.8.9 + + + + + + org.apache.maven.plugins + maven-dependency-plugin + 3.2.0 + + + copy-dependencies + initialize + + copy + + + + + com.google.code.gson + gson + ${gson.version} + + + commons-cli + commons-cli + ${commons-cli.version} + + + lib + true + true + true + + + + + + + + + org.apache.maven.plugins + maven-clean-plugin + 2.5 + + + + ${basedir}/lib + + **/* + + + + + + + org.eclipse.m2e + lifecycle-mapping + 1.0.0 + + + + + + + org.apache.maven.plugins + + + maven-dependency-plugin + + + [3.0.0,) + + + copy + + + + + + + + + + + + + + + + + + commons-cli + commons-cli + ${commons-cli.version} + + + com.google.code.gson + gson + ${gson.version} + + + diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java index d2b7045cd..ba98f581b 100644 --- a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java @@ -1,14 +1,18 @@ package com.rockwellcollins.atc.agree.cli; import org.eclipse.osgi.service.environment.EnvironmentInfo; -import org.osgi.framework.BundleActivator; +import org.eclipse.ui.plugin.AbstractUIPlugin; import org.osgi.framework.BundleContext; import org.osgi.framework.ServiceReference; -public class Activator implements BundleActivator { +//public class Activator implements BundleActivator { +public class Activator extends AbstractUIPlugin { private static BundleContext context; + + // The shared instance + private static Activator plugin; static BundleContext getContext() { return context; @@ -17,11 +21,22 @@ static BundleContext getContext() { @Override public void start(BundleContext bundleContext) throws Exception { Activator.context = bundleContext; + plugin = this; } @Override public void stop(BundleContext bundleContext) throws Exception { Activator.context = null; + plugin = null; + } + + /** + * Returns the shared instance + * + * @return the shared instance + */ + public static Activator getDefault() { + return plugin; } // Gets the workspace path contained in the -data framework cmd line arg diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java index 54885cfb7..81b6aa58a 100644 --- a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java @@ -1,9 +1,18 @@ package com.rockwellcollins.atc.agree.cli; import java.io.File; +import java.util.ArrayDeque; +import java.util.ArrayList; import java.util.Arrays; +import java.util.Collections; import java.util.Date; +import java.util.HashMap; +import java.util.HashSet; import java.util.List; +import java.util.Map; +import java.util.Queue; +import java.util.Set; +import java.util.stream.Collectors; import org.apache.commons.cli.CommandLine; import org.apache.commons.cli.CommandLineParser; @@ -12,14 +21,23 @@ import org.apache.commons.cli.Option; import org.apache.commons.cli.Options; import org.apache.commons.cli.ParseException; +import org.eclipse.core.runtime.IProgressMonitor; +import org.eclipse.core.runtime.IStatus; +import org.eclipse.core.runtime.NullProgressMonitor; +import org.eclipse.core.runtime.Status; import org.eclipse.emf.common.util.URI; import org.eclipse.emf.ecore.plugin.EcorePlugin; import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.equinox.app.IApplication; import org.eclipse.equinox.app.IApplicationContext; import org.eclipse.xtext.resource.XtextResourceSet; +import org.eclipse.xtext.util.Pair; import org.osate.aadl2.AadlPackage; +import org.osate.aadl2.AnnexSubclause; import org.osate.aadl2.ComponentImplementation; +import org.osate.aadl2.ComponentType; +import org.osate.aadl2.Element; +import org.osate.aadl2.instance.ComponentInstance; import org.osate.aadl2.instance.InstancePackage; import org.osate.aadl2.instance.SystemInstance; import org.osate.aadl2.instantiation.InstantiateModel; @@ -31,13 +49,44 @@ import com.google.inject.Injector; import com.rockwellcollins.atc.agree.AgreeStandaloneSetup; +import com.rockwellcollins.atc.agree.agree.AgreeSubclause; +import com.rockwellcollins.atc.agree.analysis.AgreeException; +import com.rockwellcollins.atc.agree.analysis.AgreeLayout; +import com.rockwellcollins.atc.agree.analysis.AgreeLogger; +import com.rockwellcollins.atc.agree.analysis.AgreeRenaming; +import com.rockwellcollins.atc.agree.analysis.AgreeUtils; +import com.rockwellcollins.atc.agree.analysis.ConsistencyResult; +import com.rockwellcollins.atc.agree.analysis.ast.AgreeASTBuilder; +import com.rockwellcollins.atc.agree.analysis.ast.AgreeNode; +import com.rockwellcollins.atc.agree.analysis.ast.AgreeProgram; +import com.rockwellcollins.atc.agree.analysis.ast.AgreeStatement; +import com.rockwellcollins.atc.agree.analysis.extentions.AgreeAutomater; +import com.rockwellcollins.atc.agree.analysis.extentions.AgreeAutomaterRegistry; +import com.rockwellcollins.atc.agree.analysis.extentions.ExtensionRegistry; +import com.rockwellcollins.atc.agree.analysis.lustre.visitors.RenamingVisitor; +import com.rockwellcollins.atc.agree.analysis.preferences.PreferenceConstants; +import com.rockwellcollins.atc.agree.analysis.preferences.PreferencesUtil; +import com.rockwellcollins.atc.agree.analysis.saving.AgreeFileUtil; +import com.rockwellcollins.atc.agree.analysis.translation.LustreAstBuilder; +import com.rockwellcollins.atc.agree.analysis.views.AgreeResultsLinker; import com.rockwellcollins.atc.agree.cli.results.AgreeJsonResult; import com.rockwellcollins.atc.agree.cli.results.AgreeOutput; import com.rockwellcollins.atc.agree.cli.results.SyntaxValidationResults; +import jkind.JKindException; +import jkind.api.JKindApi; +import jkind.api.JRealizabilityApi; +import jkind.api.KindApi; +import jkind.api.results.AnalysisResult; +import jkind.api.results.CompositeAnalysisResult; +import jkind.api.results.JKindResult; +import jkind.api.results.JRealizabilityResult; +import jkind.lustre.Node; +import jkind.lustre.Program; + public class Agree implements IApplication { - + private final static String HELP = "h"; private final static String DATA = "data"; private final static String APPLICATION = "application"; @@ -49,20 +98,28 @@ public class Agree implements IApplication { private final static String EXIT_ON_VALIDATION_WARNING = "w"; private final static String FILES = "f"; + protected AgreeResultsLinker linker = new AgreeResultsLinker(); + protected Queue queue = new ArrayDeque<>(); + private Map rerunAdviceMap = new HashMap<>(); + private int adviceCount = 0; + private enum AnalysisType { + AssumeGuarantee, Consistency, Realizability + }; + @Override public Object start(IApplicationContext context) throws Exception { - + System.out.println("Starting AGREE analysis"); context.applicationRunning(); // Read the meta information about the plug-ins to get the annex information. EcorePlugin.ExtensionProcessor.process(null); - + // Output Json object final AgreeOutput output = new AgreeOutput(); output.setDate((new Date()).toString()); - + // Process command line options String workspace = Activator.getWorkspace(); String projPath = null; @@ -84,7 +141,7 @@ public Object start(IApplicationContext context) throws Exception { options.addOption(NO_SPLASH, false, "optional, hide the splash screen, default false"); options.addOption(DATA, true, "required, path of workspace"); options.addOption(APPLICATION, true, - "required, the name of this analysis (com.rockwellcollins.atc.resolute.cli.Resolute)"); + "required, the name of this analysis (com.rockwellcollins.atc.agree.cli.Agree)"); options.addOption(PROJECT, "project", true, "required, project path (relative to workspace)"); options.addOption(COMP_IMPL, "compImpl", true, "qualified component implementation name"); options.addOption(OUTPUT, "output", true, "output JSON file absolute path"); @@ -152,15 +209,15 @@ public Object start(IApplicationContext context) throws Exception { output.addStatusMessage(message); exit = true; } - - + + if (exit) { final HelpFormatter formatter = new HelpFormatter(); formatter.printHelp("osate", options); Util.writeOutput(output, outputPath); return IApplication.EXIT_OK; } - + // Initialize the AADL meta model final Injector injector = new Aadl2StandaloneSetup().createInjectorAndDoEMFRegistration(); @@ -213,7 +270,7 @@ public Object start(IApplicationContext context) throws Exception { Util.writeOutput(output, outputPath); return IApplication.EXIT_OK; } - + // Run AGREE ComponentImplementation compImpl = null; for (Resource resource : resourceSet.getResources()) { @@ -230,8 +287,7 @@ public Object start(IApplicationContext context) throws Exception { } if (compImpl != null) { try { - final SystemInstance si = InstantiateModel.instantiate(compImpl); - final List results = runAgree(); + final List results = runAgree(compImpl); output.setStatus(AgreeOutput.COMPLETED); output.setResults(results); Util.writeOutput(output, outputPath); @@ -250,13 +306,309 @@ public Object start(IApplicationContext context) throws Exception { } return IApplication.EXIT_OK; - + + } + + private List runAgree(ComponentImplementation compImpl) { + + try { + final SystemInstance si = InstantiateModel.instantiate(compImpl); + AnalysisResult result; + CompositeAnalysisResult wrapper = new CompositeAnalysisResult(""); + +// if (isRecursive()) { +// if (AgreeUtils.usingKind2()) { +// throw new AgreeException("Kind2 only supports monolithic verification"); +// } +// result = buildAnalysisResult(ci.getName(), si); +// wrapper.addChild(result); +// result = wrapper; +// } else if (isRealizability()) { +// AgreeProgram agreeProgram = new AgreeASTBuilder().getAgreeProgram(si, false); +// +// Program program = LustreAstBuilder.getRealizabilityLustreProgram(agreeProgram); +// wrapper.addChild(createVerification("Realizability Check", si, program, agreeProgram, +// AnalysisType.Realizability)); +// result = wrapper; +// } else { + CompositeAnalysisResult wrapperTop = new CompositeAnalysisResult("Verification for " + compImpl.getName()); + wrapVerificationResult(si, wrapperTop); + wrapper.addChild(wrapperTop); + result = wrapper; +// } + +// showView(result, linker); + doAnalysis(compImpl, new NullProgressMonitor()); + System.out.println(result.toString()); + } catch (Throwable e) { + // TODO +// String messages = getNestedMessages(e); +// return new Status(IStatus.ERROR, Activator.PLUGIN_ID, 0, messages, e); + } + + return null; + } + + private void wrapVerificationResult(ComponentInstance si, CompositeAnalysisResult wrapper) { +// AgreeProgram agreeProgram = new AgreeASTBuilder().getAgreeProgram(si, isMonolithic()); + AgreeProgram agreeProgram = new AgreeASTBuilder().getAgreeProgram(si, false); + + + // generate different lustre depending on which model checker we are + // using + + Program program; + if (AgreeUtils.usingKind2()) { +// if (!isMonolithic()) { + throw new AgreeException("Kind2 now only supports monolithic verification"); +// } +// program = LustreContractAstBuilder.getContractLustreProgram(agreeProgram); + } else { + program = LustreAstBuilder.getAssumeGuaranteeLustreProgram(agreeProgram); + } + List> consistencies = LustreAstBuilder.getConsistencyChecks(agreeProgram); + + wrapper.addChild( + createVerification("Contract Guarantees", si, program, agreeProgram, AnalysisType.AssumeGuarantee)); + for (Pair consistencyAnalysis : consistencies) { + wrapper.addChild(createVerification(consistencyAnalysis.getFirst(), si, consistencyAnalysis.getSecond(), + agreeProgram, AnalysisType.Consistency)); + } + } + + private AnalysisResult createVerification(String resultName, ComponentInstance compInst, Program lustreProgram, + AgreeProgram agreeProgram, AnalysisType analysisType) { + + ///////// +// Logger logger = Logger.getLogger("MyLog"); +// FileHandler fh; +// try { + + // This block configure the logger with handler and formatter +// fh = new FileHandler("/home/thomas/zzz.log"); +// logger.addHandler(fh); +// SimpleFormatter formatter = new SimpleFormatter(); +// fh.setFormatter(formatter); +// logger.info("Agree Program:"); +// AgreeASTPrettyprinter pp = new AgreeASTPrettyprinter(); +// pp.visit(agreeProgram); +// logger.info(pp.toString()); + +// } catch (SecurityException ex) { +// ex.printStackTrace(); +// } +// catch (IOException ex) { +// ex.printStackTrace(); +// } + //////////////// + + AgreeAutomaterRegistry aAReg = (AgreeAutomaterRegistry) ExtensionRegistry + .getRegistry(ExtensionRegistry.AGREE_AUTOMATER_EXT_ID); + List automaters = aAReg.getAgreeAutomaters(); + AgreeRenaming renaming = new AgreeRenaming(); + AgreeLayout layout = new AgreeLayout(); + Node mainNode = null; + for (Node node : lustreProgram.nodes) { + if (node.id.equals(lustreProgram.main)) { + mainNode = node; + break; + } + } + + if (mainNode == null) { + throw new AgreeException("Could not find main lustre node after translation"); + } + + List properties = new ArrayList<>(); + + RenamingVisitor.addRenamings(lustreProgram, renaming, compInst, layout); + addProperties(renaming, properties, mainNode, agreeProgram); + + for (AgreeAutomater aa : automaters) { + renaming = aa.rename(renaming); + layout = aa.transformLayout(layout); + } + + JKindResult result; + switch (analysisType) { + case Consistency: + result = new ConsistencyResult(resultName, mainNode.properties, Collections.singletonList(true), renaming); + break; + case Realizability: + result = new JRealizabilityResult(resultName, renaming); + break; + case AssumeGuarantee: + final Set invertedProperties = renaming.getInvertedProperties(); + List invertedPropertyMask = mainNode.properties.stream().map(p -> invertedProperties.contains(p)) + .collect(Collectors.toList()); + result = new JKindResult(resultName, properties, invertedPropertyMask, renaming); + break; + default: + throw new AgreeException("Unhandled Analysis Type"); + } + + queue.add(result); + + ComponentImplementation compImpl = AgreeUtils.getInstanceImplementation(compInst); + linker.setProgram(result, lustreProgram); + linker.setComponent(result, compImpl); + linker.setContract(result, getContract(compImpl)); + linker.setLayout(result, layout); + linker.setReferenceMap(result, renaming.getRefMap()); + linker.setLog(result, AgreeLogger.getLog()); + linker.setRenaming(result, renaming); + + // System.out.println(program); + return result; + } - - private List runAgree() { + + private void addProperties(AgreeRenaming renaming, List properties, Node mainNode, + AgreeProgram agreeProgram) { + + // there is a special case in the AgreeRenaming which handles this + // translation + if (AgreeUtils.usingKind2()) { + addKind2Properties(agreeProgram.topNode, properties, renaming, "_TOP", ""); + } else { + properties.addAll(mainNode.properties); + } + + Set strs = new HashSet<>(); + for (String prop : properties) { + String renamed = renaming.rename(prop); + if (!strs.add(renamed)) { + throw new AgreeException("Multiple properties named \"" + renamed + "\""); + } + } + + } + + private void addKind2Properties(AgreeNode agreeNode, List properties, AgreeRenaming renaming, + String prefix, String userPropPrefix) { + int i = 0; + + String propPrefix = (userPropPrefix.equals("")) ? "" : userPropPrefix + ": "; + for (AgreeStatement statement : agreeNode.lemmas) { + renaming.addExplicitRename(prefix + "[" + (++i) + "]", propPrefix + statement.string); + properties.add(prefix.replaceAll("\\.", AgreeASTBuilder.dotChar) + "[" + i + "]"); + } + for (AgreeStatement statement : agreeNode.guarantees) { + renaming.addExplicitRename(prefix + "[" + (++i) + "]", propPrefix + statement.string); + properties.add(prefix.replaceAll("\\.", AgreeASTBuilder.dotChar) + "[" + i + "]"); + } + + userPropPrefix = userPropPrefix.equals("") ? "" : userPropPrefix + "."; + for (AgreeNode subNode : agreeNode.subNodes) { + addKind2Properties(subNode, properties, renaming, prefix + "." + subNode.id, userPropPrefix + subNode.id); + } + } + + private AgreeSubclause getContract(ComponentImplementation ci) { + ComponentType ct = ci.getOwnedRealization().getImplemented(); + for (AnnexSubclause annex : ct.getOwnedAnnexSubclauses()) { + if (annex instanceof AgreeSubclause) { + return (AgreeSubclause) annex; + } + } return null; } + private IStatus doAnalysis(final Element root, final IProgressMonitor globalMonitor) { + + Thread analysisThread = new Thread() { + @Override + public void run() { + + // Record the analysis start time and get model hashcode for + // saving to property analysis log, if necessary + String modelHash = ""; + long startTime = 0; + if (Activator.getDefault().getPreferenceStore().getBoolean(PreferenceConstants.PREF_PROP_LOG)) { + try { + modelHash = AgreeFileUtil.getModelHashcode(root); + startTime = System.currentTimeMillis(); + } catch (Exception e) { + System.out.println(e.getMessage()); + return; + } + } + +// try { +// activateTerminateHandlers(globalMonitor); + KindApi api = PreferencesUtil.getKindApi(); + KindApi consistApi = PreferencesUtil.getConsistencyApi(); + JRealizabilityApi realApi = PreferencesUtil.getJRealizabilityApi(); + + while (!queue.isEmpty() && !globalMonitor.isCanceled()) { + JKindResult result = queue.peek(); + NullProgressMonitor subMonitor = new NullProgressMonitor(); +// monitorRef.set(subMonitor); + + Program program = linker.getProgram(result); + + if (api instanceof JKindApi) { + String resultName = result.getName(); + String adviceFileName = rerunAdviceMap.get(resultName); + if (adviceFileName == null) { + adviceFileName = "agree_advice" + adviceCount++; + rerunAdviceMap.put(resultName, adviceFileName); + } else { + ((JKindApi) api).setReadAdviceFile(adviceFileName); + } + ((JKindApi) api).setWriteAdviceFile(adviceFileName); + } + + try { + if (result instanceof ConsistencyResult) { + consistApi.execute(program, result, subMonitor); + } else if (result instanceof JRealizabilityResult) { + realApi.execute(program, (JRealizabilityResult) result, subMonitor); + } else { + api.execute(program, result, subMonitor); + } + } catch (JKindException e) { + + System.out.println("******** JKindException Text ********"); + e.printStackTrace(System.out); + + String errStr = e.getMessage(); + int l = Math.min(errStr.length(), 300); + System.out.println(e.getMessage().substring(0, l)); + + break; + } + + // Print to property analysis log, if necessary + if (Activator.getDefault().getPreferenceStore().getBoolean(PreferenceConstants.PREF_PROP_LOG)) { + AgreeFileUtil.printLog(result, startTime, modelHash); + } + + queue.remove(); + } + + while (!queue.isEmpty()) { + queue.remove().cancel(); + } +// } finally { +// deactivateTerminateHandlers(); +// enableRerunHandler(root); +// } + + } + }; + analysisThread.start(); + while (analysisThread.isAlive()) { + try { + Thread.sleep(1000); + } catch (InterruptedException e) { + // TODO Auto-generated catch block + e.printStackTrace(); + } + } + return Status.OK_STATUS; + } + @Override public void stop() { diff --git a/com.rockwellcollins.atc.agree.codegen/META-INF/MANIFEST.MF b/com.rockwellcollins.atc.agree.codegen/META-INF/MANIFEST.MF index aeaec4501..569b6108a 100644 --- a/com.rockwellcollins.atc.agree.codegen/META-INF/MANIFEST.MF +++ b/com.rockwellcollins.atc.agree.codegen/META-INF/MANIFEST.MF @@ -8,8 +8,8 @@ Bundle-Vendor: ROCKWELLCOLLINS Require-Bundle: org.eclipse.ui;bundle-version="[3.119.0,4.0.0)", org.eclipse.core.runtime;bundle-version="[3.20.0,4.0.0)", org.osate.aadl2;bundle-version="[5.0.0,6.0.0)", - com.rockwellcollins.atc.agree.analysis;bundle-version="[2.8.0,3.0.0)", - com.rockwellcollins.atc.agree;bundle-version="[3.0.0,4.0.0)", + com.rockwellcollins.atc.agree.analysis;bundle-version="[2.10.0,3.0.0)", + com.rockwellcollins.atc.agree;bundle-version="[3.1.0,4.0.0)", org.osate.annexsupport;bundle-version="[4.0.1,5.0.0)", org.osate.xtext.aadl2.properties;bundle-version="[3.0.0,4.0.0)", org.eclipse.core.resources;bundle-version="[3.9.1,4.0.0)", diff --git a/com.rockwellcollins.atc.agree.feature/feature.xml b/com.rockwellcollins.atc.agree.feature/feature.xml index f94a93d02..2785d541a 100644 --- a/com.rockwellcollins.atc.agree.feature/feature.xml +++ b/com.rockwellcollins.atc.agree.feature/feature.xml @@ -138,6 +138,13 @@ SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. version="0.0.0" unpack="false"/> + + + + diff --git a/com.rockwellcollins.atc.agree.ui/META-INF/MANIFEST.MF b/com.rockwellcollins.atc.agree.ui/META-INF/MANIFEST.MF index 19023f396..b147fadc6 100644 --- a/com.rockwellcollins.atc.agree.ui/META-INF/MANIFEST.MF +++ b/com.rockwellcollins.atc.agree.ui/META-INF/MANIFEST.MF @@ -5,7 +5,7 @@ Bundle-Vendor: Rockwell Collins, Inc. Bundle-Version: 3.2.1.qualifier Bundle-SymbolicName: com.rockwellcollins.atc.agree.ui; singleton:=true Bundle-ActivationPolicy: lazy -Require-Bundle: com.rockwellcollins.atc.agree;bundle-version="[3.0.0,4.0.0)";visibility:=reexport, +Require-Bundle: com.rockwellcollins.atc.agree;bundle-version="[3.1.0,4.0.0)";visibility:=reexport, org.eclipse.xtext.ui;bundle-version="[2.25.0,3.0.0)", org.eclipse.ui.editors;bundle-version="[3.5.0,4.0.0)", org.eclipse.ui.ide;bundle-version="[3.5.0,4.0.0)", diff --git a/pom.xml b/pom.xml index e64ef793a..81f171686 100644 --- a/pom.xml +++ b/pom.xml @@ -47,6 +47,7 @@ com.rockwellcollins.atc.agree com.rockwellcollins.atc.agree.analysis + com.rockwellcollins.atc.agree.cli com.rockwellcollins.atc.agree.codegen com.rockwellcollins.atc.agree.doc com.rockwellcollins.atc.agree.feature From 0029ef66a047dea83ba30fce1ec8c5f24c2d7e19 Mon Sep 17 00:00:00 2001 From: Isaac Amundson Date: Tue, 28 May 2024 15:56:11 -0500 Subject: [PATCH 3/6] command line arguments --- .../preferences/PreferenceInitializer.java | 2 + .../META-INF/MANIFEST.MF | 3 +- .../atc/agree/cli/Activator.java | 18 - .../rockwellcollins/atc/agree/cli/Agree.java | 457 +++++++++++++----- 4 files changed, 332 insertions(+), 148 deletions(-) diff --git a/com.rockwellcollins.atc.agree.analysis/src/com/rockwellcollins/atc/agree/analysis/preferences/PreferenceInitializer.java b/com.rockwellcollins.atc.agree.analysis/src/com/rockwellcollins/atc/agree/analysis/preferences/PreferenceInitializer.java index 78dc913ec..785681179 100644 --- a/com.rockwellcollins.atc.agree.analysis/src/com/rockwellcollins/atc/agree/analysis/preferences/PreferenceInitializer.java +++ b/com.rockwellcollins.atc.agree.analysis/src/com/rockwellcollins/atc/agree/analysis/preferences/PreferenceInitializer.java @@ -34,7 +34,9 @@ public void initializeDefaultPreferences() { IPreferenceStore store = Activator.getDefault().getPreferenceStore(); store.setDefault(PreferenceConstants.PREF_MODEL_CHECKER, PreferenceConstants.MODEL_CHECKER_JKIND); store.setDefault(PreferenceConstants.PREF_SOLVER, PreferenceConstants.SOLVER_SMTINTERPOL); + store.setDefault(PreferenceConstants.PREF_NO_KINDUCTION, false); store.setDefault(PreferenceConstants.PREF_INDUCT_CEX, true); + store.setDefault(PreferenceConstants.PREF_SUPPORT, false); store.setDefault(PreferenceConstants.PREF_SMOOTH_CEX, false); store.setDefault(PreferenceConstants.PREF_UNSPECIFIED_AADL_PROPERTIES, false); store.setDefault(PreferenceConstants.PREF_DISPLAY_DECIMAL_CEX, false); diff --git a/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF b/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF index 845ada5bd..3740b51a4 100644 --- a/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF +++ b/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF @@ -15,7 +15,8 @@ Require-Bundle: org.eclipse.ui, org.osate.pluginsupport, org.osate.aadl2.instantiation, com.collins.trustedsystems.jkindapi, - com.rockwellcollins.atc.agree.analysis + com.rockwellcollins.atc.agree.analysis, + org.osate.annexsupport Bundle-RequiredExecutionEnvironment: JavaSE-17 Automatic-Module-Name: com.rockwellcollins.atc.agree.cli Bundle-ActivationPolicy: lazy diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java index ba98f581b..44d20b3cc 100644 --- a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Activator.java @@ -38,23 +38,5 @@ public void stop(BundleContext bundleContext) throws Exception { public static Activator getDefault() { return plugin; } - - // Gets the workspace path contained in the -data framework cmd line arg - public static String getWorkspace() { - final ServiceReference infoRef = context.getServiceReference(EnvironmentInfo.class); - if (infoRef != null) { - final EnvironmentInfo envInfo = context.getService(infoRef); - if (envInfo != null) { - context.ungetService(infoRef); - for (int i = 0; i < envInfo.getFrameworkArgs().length; ++i) { - if ("-data".equals(envInfo.getFrameworkArgs()[i].toLowerCase()) - && i < envInfo.getFrameworkArgs().length - 1) { - return envInfo.getFrameworkArgs()[i + 1]; - } - } - } - } - return null; - } } diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java index 81b6aa58a..4e10804be 100644 --- a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java @@ -21,6 +21,7 @@ import org.apache.commons.cli.Option; import org.apache.commons.cli.Options; import org.apache.commons.cli.ParseException; +import org.eclipse.core.resources.ResourcesPlugin; import org.eclipse.core.runtime.IProgressMonitor; import org.eclipse.core.runtime.IStatus; import org.eclipse.core.runtime.NullProgressMonitor; @@ -30,10 +31,12 @@ import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.equinox.app.IApplication; import org.eclipse.equinox.app.IApplicationContext; +import org.eclipse.jface.preference.IPreferenceStore; import org.eclipse.xtext.resource.XtextResourceSet; import org.eclipse.xtext.util.Pair; import org.osate.aadl2.AadlPackage; import org.osate.aadl2.AnnexSubclause; +import org.osate.aadl2.ComponentClassifier; import org.osate.aadl2.ComponentImplementation; import org.osate.aadl2.ComponentType; import org.osate.aadl2.Element; @@ -44,12 +47,16 @@ import org.osate.aadl2.modelsupport.util.AadlUtil; import org.osate.aadl2.util.Aadl2ResourceFactoryImpl; import org.osate.aadl2.util.Aadl2Util; +import org.osate.annexsupport.AnnexUtil; import org.osate.pluginsupport.PluginSupportUtil; import org.osate.xtext.aadl2.Aadl2StandaloneSetup; import com.google.inject.Injector; import com.rockwellcollins.atc.agree.AgreeStandaloneSetup; +import com.rockwellcollins.atc.agree.agree.AgreeContractSubclause; +import com.rockwellcollins.atc.agree.agree.AgreePackage; import com.rockwellcollins.atc.agree.agree.AgreeSubclause; +import com.rockwellcollins.atc.agree.analysis.Activator; import com.rockwellcollins.atc.agree.analysis.AgreeException; import com.rockwellcollins.atc.agree.analysis.AgreeLayout; import com.rockwellcollins.atc.agree.analysis.AgreeLogger; @@ -68,8 +75,8 @@ import com.rockwellcollins.atc.agree.analysis.preferences.PreferencesUtil; import com.rockwellcollins.atc.agree.analysis.saving.AgreeFileUtil; import com.rockwellcollins.atc.agree.analysis.translation.LustreAstBuilder; +import com.rockwellcollins.atc.agree.analysis.translation.LustreContractAstBuilder; import com.rockwellcollins.atc.agree.analysis.views.AgreeResultsLinker; -import com.rockwellcollins.atc.agree.cli.results.AgreeJsonResult; import com.rockwellcollins.atc.agree.cli.results.AgreeOutput; import com.rockwellcollins.atc.agree.cli.results.SyntaxValidationResults; @@ -94,17 +101,38 @@ public class Agree implements IApplication { private final static String PROJECT = "p"; private final static String COMP_IMPL = "c"; private final static String OUTPUT = "o"; + private final static String FILES = "f"; + // Run options + private final static String VERIFICATION = "v"; + // Preferences + private final static String MODEL_CHECKER = "m"; + private final static String SOLVER = "s"; + private final static String DISABLE_K_INDUCTION = "disableKInduction"; + private final static String NO_INDUCTIVE_COUNTEREXAMPLES = "noInductiveCounterexamples"; + private final static String GET_SET_OF_SUPPORT = "getSetOfSupport"; + private final static String GENERATE_SMOOTH_COUNTEREXAMPLES = "generateSmoothCounterexamples"; + private final static String ANALYZE_UNSPECIFIED_AADL_PROPERTIES = "analyzeUnspecifiedAADLProperties"; + private final static String DISPLAY_COUNTEREXAMPLES_AS_DECIMAL = "displayCounterexamplesAsDecimal"; + private final static String GENERATE_BLAMED_COUNTEREXAMPLES = "generateBlamedCounterexamples"; + private final static String MAX_INDUCTION_DEPTH = "maxInductionDepth"; + private final static String MAX_PDR_INSTANCES = "maxPDRInstances"; + private final static String TIMEOUT = "timeout"; + private final static String CONSISTENCY_DEPTH = "consistencyDepth"; + // Validation options private final static String VALIDATION_ONLY = "v"; private final static String EXIT_ON_VALIDATION_WARNING = "w"; - private final static String FILES = "f"; - protected AgreeResultsLinker linker = new AgreeResultsLinker(); - protected Queue queue = new ArrayDeque<>(); + private AgreeResultsLinker linker = new AgreeResultsLinker(); + private Queue queue = new ArrayDeque<>(); private Map rerunAdviceMap = new HashMap<>(); private int adviceCount = 0; private enum AnalysisType { AssumeGuarantee, Consistency, Realizability }; + private enum VerificationStrategy { + Single, All, Monolithic, Realizability + } + private VerificationStrategy strategy = null; @Override public Object start(IApplicationContext context) throws Exception { @@ -121,11 +149,25 @@ public Object start(IApplicationContext context) throws Exception { output.setDate((new Date()).toString()); // Process command line options - String workspace = Activator.getWorkspace(); + String workspace = ResourcesPlugin.getWorkspace().getRoot().getLocation().toString(); String projPath = null; String component = null; String outputPath = null; String[] fileArray = null; + final IPreferenceStore store = Activator.getDefault().getPreferenceStore(); + // Reset preferences to default values + store.setToDefault(PreferenceConstants.PREF_MODEL_CHECKER); + store.setToDefault(PreferenceConstants.PREF_SOLVER); + store.setToDefault(PreferenceConstants.PREF_NO_KINDUCTION); + store.setToDefault(PreferenceConstants.PREF_SUPPORT); + store.setToDefault(PreferenceConstants.PREF_SMOOTH_CEX); + store.setToDefault(PreferenceConstants.PREF_UNSPECIFIED_AADL_PROPERTIES); + store.setToDefault(PreferenceConstants.PREF_DISPLAY_DECIMAL_CEX); + store.setToDefault(PreferenceConstants.PREF_BLAME_CEX); + store.setToDefault(PreferenceConstants.PREF_DEPTH); + store.setToDefault(PreferenceConstants.PREF_PDR_MAX); + store.setToDefault(PreferenceConstants.PREF_TIMEOUT); + store.setToDefault(PreferenceConstants.PREF_CONSIST_DEPTH); boolean exitOnValidationWarning = false; boolean validationOnly = false; boolean exit = false; @@ -143,14 +185,28 @@ public Object start(IApplicationContext context) throws Exception { options.addOption(APPLICATION, true, "required, the name of this analysis (com.rockwellcollins.atc.agree.cli.Agree)"); options.addOption(PROJECT, "project", true, "required, project path (relative to workspace)"); - options.addOption(COMP_IMPL, "compImpl", true, "qualified component implementation name"); - options.addOption(OUTPUT, "output", true, "output JSON file absolute path"); + options.addOption(COMP_IMPL, "compImpl", true, "required, qualified component implementation name"); + options.addOption(OUTPUT, "output", true, "required, output JSON file absolute path"); + Option option = new Option(FILES, "files", true, "optional, supplementary AADL files (absolute paths)"); + option.setArgs(Option.UNLIMITED_VALUES); + options.addOption(option); + options.addOption(VERIFICATION, "verification", true, "required, verification strategy (single, all, monolithic, realizability)"); + options.addOption(MODEL_CHECKER, "modelChecker", true, "optional, model checker, default " + store.getString(PreferenceConstants.PREF_MODEL_CHECKER)); + options.addOption(SOLVER, "solver", true, "optional, SMT solver, default " + store.getString(PreferenceConstants.PREF_SOLVER)); + options.addOption(DISABLE_K_INDUCTION, false, "optional, disable k-induction"); + options.addOption(NO_INDUCTIVE_COUNTEREXAMPLES, false, "optional, do not generate inductive counterexamples"); + options.addOption(GET_SET_OF_SUPPORT, false, "optional, get set of support"); + options.addOption(GENERATE_SMOOTH_COUNTEREXAMPLES, false, "optional, generate smooth counterexamples"); + options.addOption(ANALYZE_UNSPECIFIED_AADL_PROPERTIES, false, "optional, analyze unspecified AADL properties"); + options.addOption(DISPLAY_COUNTEREXAMPLES_AS_DECIMAL, false, "optional, display counterexamples as decimal"); + options.addOption(GENERATE_BLAMED_COUNTEREXAMPLES, false, "optional, generate blamed counterexamples"); + options.addOption(MAX_INDUCTION_DEPTH, true, "optional, maximum induction depth, default " + store.getInt(PreferenceConstants.PREF_DEPTH)); + options.addOption(MAX_PDR_INSTANCES, true, "optional, maximum number of PDR instances, default " + store.getInt(PreferenceConstants.PREF_PDR_MAX)); + options.addOption(TIMEOUT, true, "optional, timeout (ms), default " + store.getInt(PreferenceConstants.PREF_TIMEOUT)); + options.addOption(CONSISTENCY_DEPTH, true, "optional, consistency depth, default " + store.getInt(PreferenceConstants.PREF_CONSIST_DEPTH)); options.addOption(VALIDATION_ONLY, "validationOnly", false, "validation only, default false"); options.addOption(EXIT_ON_VALIDATION_WARNING, "exitOnValidtionWarning", false, "exit on validation warning, default false"); - Option option = new Option(FILES, "files", true, "Supplementary AADL files (absolute paths)"); - option.setArgs(Option.UNLIMITED_VALUES); - options.addOption(option); // parse options try { @@ -190,6 +246,152 @@ public Object start(IApplicationContext context) throws Exception { if (commandLine.hasOption(FILES)) { fileArray = commandLine.getOptionValues(FILES); } + if (commandLine.hasOption(VERIFICATION)) { + switch (commandLine.getOptionValue(VERIFICATION).toLowerCase()) { + case "single": + strategy = VerificationStrategy.Single; + break; + case "all": + strategy = VerificationStrategy.All; + break; + case "monolithic": + strategy = VerificationStrategy.Monolithic; + break; + case "realizability": + strategy = VerificationStrategy.Realizability; + break; + default: + exit = true; + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Invalid verification type. " + commandLine.getOptionValue(VERIFICATION) + " is not supported."); + } + } else { + exit = true; + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("A verification type must be specified (single, all, monolithic, realizability)."); + } + if (commandLine.hasOption(MODEL_CHECKER)) { + switch (commandLine.getOptionValue(MODEL_CHECKER).toLowerCase()) { + case "jkind": + store.setValue(PreferenceConstants.PREF_MODEL_CHECKER, PreferenceConstants.MODEL_CHECKER_JKIND); + break; + case "kind2": + store.setValue(PreferenceConstants.PREF_MODEL_CHECKER, PreferenceConstants.MODEL_CHECKER_KIND2); + break; + case "kind2remote": + store.setValue(PreferenceConstants.PREF_MODEL_CHECKER, PreferenceConstants.MODEL_CHECKER_KIND2WEB); + break; + case "sally": + store.setValue(PreferenceConstants.PREF_MODEL_CHECKER, PreferenceConstants.MODEL_CHECKER_SALLY); + break; + default: + exit = true; + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Invalid model checker. " + commandLine.getOptionValue(MODEL_CHECKER) + " is not supported. Valid options are: JKind, Kind2, Kind2Remote, Sally."); + } + } + if (commandLine.hasOption(SOLVER)) { + switch (commandLine.getOptionValue(SOLVER).toLowerCase()) { + case "smtinterpol": + store.setValue(PreferenceConstants.PREF_SOLVER, PreferenceConstants.SOLVER_SMTINTERPOL); + break; + case "yices": + store.setValue(PreferenceConstants.PREF_SOLVER, PreferenceConstants.SOLVER_YICES); + break; + case "yices2": + store.setValue(PreferenceConstants.PREF_SOLVER, PreferenceConstants.SOLVER_YICES2); + break; + case "z3": + store.setValue(PreferenceConstants.PREF_SOLVER, PreferenceConstants.SOLVER_Z3); + break; + case "cvc4": + store.setValue(PreferenceConstants.PREF_SOLVER, PreferenceConstants.SOLVER_CVC4); + break; + case "cvc5": + // TODO set pref + break; + case "dreal": + store.setValue(PreferenceConstants.PREF_SOLVER, PreferenceConstants.SOLVER_DREAL); + break; + default: + exit = true; + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Invalid solver. " + commandLine.getOptionValue(SOLVER) + " is not supported. Valid options are: SMTInterpol, Yices, Yices2, Z3, CVC4, CVC5, dReal."); + } + } + if (commandLine.hasOption(DISABLE_K_INDUCTION)) { + store.setValue(PreferenceConstants.PREF_NO_KINDUCTION, true); + } + if (commandLine.hasOption(NO_INDUCTIVE_COUNTEREXAMPLES)) { + store.setValue(PreferenceConstants.PREF_INDUCT_CEX, false); + } + if (commandLine.hasOption(GET_SET_OF_SUPPORT)) { + store.setValue(PreferenceConstants.PREF_SUPPORT, true); + } + if (commandLine.hasOption(GENERATE_SMOOTH_COUNTEREXAMPLES)) { + store.setValue(PreferenceConstants.PREF_SMOOTH_CEX, true); + } + if (commandLine.hasOption(ANALYZE_UNSPECIFIED_AADL_PROPERTIES)) { + store.setValue(PreferenceConstants.PREF_UNSPECIFIED_AADL_PROPERTIES, true); + } + if (commandLine.hasOption(DISPLAY_COUNTEREXAMPLES_AS_DECIMAL)) { + store.setValue(PreferenceConstants.PREF_DISPLAY_DECIMAL_CEX, true); + } + if (commandLine.hasOption(GENERATE_BLAMED_COUNTEREXAMPLES)) { + store.setValue(PreferenceConstants.PREF_BLAME_CEX, true); + } + if (commandLine.hasOption(MAX_INDUCTION_DEPTH)) { + try { + final int i = Integer.parseInt(commandLine.getOptionValue(MAX_INDUCTION_DEPTH)); + if (i < 0) { + throw new NumberFormatException("Value must be greater than zero."); + } + store.setValue(PreferenceConstants.PREF_DEPTH, i); + } catch (NumberFormatException e) { + exit = true; + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Invalid maximum induction depth specified. " + e.getMessage()); + } + } + if (commandLine.hasOption(MAX_PDR_INSTANCES)) { + try { + final int i = Integer.parseInt(commandLine.getOptionValue(MAX_PDR_INSTANCES)); + if (i < 0) { + throw new NumberFormatException("Value must be greater than zero."); + } + store.setValue(PreferenceConstants.PREF_PDR_MAX, i); + } catch (NumberFormatException e) { + exit = true; + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Invalid maximum PDR instances specified. " + e.getMessage()); + } + } + if (commandLine.hasOption(TIMEOUT)) { + try { + final int i = Integer.parseInt(commandLine.getOptionValue(TIMEOUT)); + if (i < 0) { + throw new NumberFormatException("Value must be greater than zero."); + } + store.setValue(PreferenceConstants.PREF_TIMEOUT, i); + } catch (NumberFormatException e) { + exit = true; + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Invalid timeout specified. " + e.getMessage()); + } + } + if (commandLine.hasOption(CONSISTENCY_DEPTH)) { + try { + final int i = Integer.parseInt(commandLine.getOptionValue(CONSISTENCY_DEPTH)); + if (i < 0) { + throw new NumberFormatException("Value must be greater than zero."); + } + store.setValue(PreferenceConstants.PREF_CONSIST_DEPTH, i); + } catch (NumberFormatException e) { + exit = true; + output.setStatus(AgreeOutput.INTERRUPTED); + output.addStatusMessage("Invalid consistency depth specified. " + e.getMessage()); + } + } if (commandLine.hasOption(VALIDATION_ONLY)) { validationOnly = true; } @@ -198,7 +400,7 @@ public Object start(IApplicationContext context) throws Exception { } final String[] remainder = commandLine.getArgs(); for (String argument : remainder) { - final String message = "WARNING: unknown arguement " + argument + final String message = "WARNING: unknown argument " + argument + ". See --help for command line options."; output.addStatusMessage(message); System.err.println(message); @@ -287,9 +489,10 @@ public Object start(IApplicationContext context) throws Exception { } if (compImpl != null) { try { - final List results = runAgree(compImpl); + final AnalysisResult results = runAgree(compImpl); output.setStatus(AgreeOutput.COMPLETED); - output.setResults(results); + // TODO deal with output +// output.setResults(results); Util.writeOutput(output, outputPath); } catch (Exception e) { e.printStackTrace(); @@ -309,60 +512,87 @@ public Object start(IApplicationContext context) throws Exception { } - private List runAgree(ComponentImplementation compImpl) { + private AnalysisResult runAgree(ComponentImplementation compImpl) throws Exception { - try { - final SystemInstance si = InstantiateModel.instantiate(compImpl); - AnalysisResult result; - CompositeAnalysisResult wrapper = new CompositeAnalysisResult(""); - -// if (isRecursive()) { -// if (AgreeUtils.usingKind2()) { -// throw new AgreeException("Kind2 only supports monolithic verification"); -// } -// result = buildAnalysisResult(ci.getName(), si); -// wrapper.addChild(result); -// result = wrapper; -// } else if (isRealizability()) { -// AgreeProgram agreeProgram = new AgreeASTBuilder().getAgreeProgram(si, false); -// -// Program program = LustreAstBuilder.getRealizabilityLustreProgram(agreeProgram); -// wrapper.addChild(createVerification("Realizability Check", si, program, agreeProgram, -// AnalysisType.Realizability)); -// result = wrapper; -// } else { - CompositeAnalysisResult wrapperTop = new CompositeAnalysisResult("Verification for " + compImpl.getName()); - wrapVerificationResult(si, wrapperTop); - wrapper.addChild(wrapperTop); - result = wrapper; -// } - -// showView(result, linker); - doAnalysis(compImpl, new NullProgressMonitor()); - System.out.println(result.toString()); - } catch (Throwable e) { - // TODO -// String messages = getNestedMessages(e); -// return new Status(IStatus.ERROR, Activator.PLUGIN_ID, 0, messages, e); + final SystemInstance si = InstantiateModel.instantiate(compImpl); + AnalysisResult result; + CompositeAnalysisResult wrapper = new CompositeAnalysisResult(""); + + if (strategy == VerificationStrategy.All) { + if (AgreeUtils.usingKind2()) { + throw new AgreeException("Kind2 only supports monolithic verification"); + } + result = buildAnalysisResult(compImpl.getName(), si); + wrapper.addChild(result); + result = wrapper; + } else if (strategy == VerificationStrategy.Realizability) { + AgreeProgram agreeProgram = new AgreeASTBuilder().getAgreeProgram(si, false); + + Program program = LustreAstBuilder.getRealizabilityLustreProgram(agreeProgram); + wrapper.addChild(createVerification("Realizability Check", si, program, agreeProgram, + AnalysisType.Realizability)); + result = wrapper; + } else { + CompositeAnalysisResult wrapperTop = new CompositeAnalysisResult("Verification for " + compImpl.getName()); + wrapVerificationResult(si, wrapperTop); + wrapper.addChild(wrapperTop); + result = wrapper; } + doAnalysis(compImpl, new NullProgressMonitor()); + System.out.println(result.toString()); + + return result; + } + + private AnalysisResult buildAnalysisResult(String name, ComponentInstance ci) { + CompositeAnalysisResult result = new CompositeAnalysisResult("Verification for " + name); + + if (containsAGREEAnnex(ci)) { + wrapVerificationResult(ci, result); + ComponentImplementation compImpl = AgreeUtils.getInstanceImplementation(ci); + for (ComponentInstance subInst : ci.getComponentInstances()) { + if (AgreeUtils.getInstanceImplementation(subInst) != null) { + AnalysisResult buildAnalysisResult = buildAnalysisResult(subInst.getName(), subInst); + if (buildAnalysisResult != null) { + result.addChild(buildAnalysisResult); + } + } + } + + if (result.getChildren().size() != 0) { + linker.setComponent(result, compImpl); + return result; + } + } return null; } + + private boolean containsAGREEAnnex(ComponentInstance ci) { + ComponentClassifier compClass = ci.getComponentClassifier(); + if (compClass instanceof ComponentImplementation) { + compClass = ((ComponentImplementation) compClass).getType(); + } + for (AnnexSubclause annex : AnnexUtil.getAllAnnexSubclauses(compClass, + AgreePackage.eINSTANCE.getAgreeContractSubclause())) { + if (annex instanceof AgreeContractSubclause) { + return true; + } + } + return false; + } private void wrapVerificationResult(ComponentInstance si, CompositeAnalysisResult wrapper) { -// AgreeProgram agreeProgram = new AgreeASTBuilder().getAgreeProgram(si, isMonolithic()); - AgreeProgram agreeProgram = new AgreeASTBuilder().getAgreeProgram(si, false); + AgreeProgram agreeProgram = new AgreeASTBuilder().getAgreeProgram(si, strategy == VerificationStrategy.Monolithic); - - // generate different lustre depending on which model checker we are - // using + // generate different lustre depending on which model checker we are using Program program; if (AgreeUtils.usingKind2()) { -// if (!isMonolithic()) { + if (strategy != VerificationStrategy.Monolithic) { throw new AgreeException("Kind2 now only supports monolithic verification"); -// } -// program = LustreContractAstBuilder.getContractLustreProgram(agreeProgram); + } + program = LustreContractAstBuilder.getContractLustreProgram(agreeProgram); } else { program = LustreAstBuilder.getAssumeGuaranteeLustreProgram(agreeProgram); } @@ -379,29 +609,6 @@ private void wrapVerificationResult(ComponentInstance si, CompositeAnalysisResul private AnalysisResult createVerification(String resultName, ComponentInstance compInst, Program lustreProgram, AgreeProgram agreeProgram, AnalysisType analysisType) { - ///////// -// Logger logger = Logger.getLogger("MyLog"); -// FileHandler fh; -// try { - - // This block configure the logger with handler and formatter -// fh = new FileHandler("/home/thomas/zzz.log"); -// logger.addHandler(fh); -// SimpleFormatter formatter = new SimpleFormatter(); -// fh.setFormatter(formatter); -// logger.info("Agree Program:"); -// AgreeASTPrettyprinter pp = new AgreeASTPrettyprinter(); -// pp.visit(agreeProgram); -// logger.info(pp.toString()); - -// } catch (SecurityException ex) { -// ex.printStackTrace(); -// } -// catch (IOException ex) { -// ex.printStackTrace(); -// } - //////////////// - AgreeAutomaterRegistry aAReg = (AgreeAutomaterRegistry) ExtensionRegistry .getRegistry(ExtensionRegistry.AGREE_AUTOMATER_EXT_ID); List automaters = aAReg.getAgreeAutomaters(); @@ -458,7 +665,6 @@ private AnalysisResult createVerification(String resultName, ComponentInstance c linker.setLog(result, AgreeLogger.getLog()); linker.setRenaming(result, renaming); - // System.out.println(program); return result; } @@ -534,66 +740,60 @@ public void run() { } } -// try { -// activateTerminateHandlers(globalMonitor); - KindApi api = PreferencesUtil.getKindApi(); - KindApi consistApi = PreferencesUtil.getConsistencyApi(); - JRealizabilityApi realApi = PreferencesUtil.getJRealizabilityApi(); - - while (!queue.isEmpty() && !globalMonitor.isCanceled()) { - JKindResult result = queue.peek(); - NullProgressMonitor subMonitor = new NullProgressMonitor(); -// monitorRef.set(subMonitor); - - Program program = linker.getProgram(result); - - if (api instanceof JKindApi) { - String resultName = result.getName(); - String adviceFileName = rerunAdviceMap.get(resultName); - if (adviceFileName == null) { - adviceFileName = "agree_advice" + adviceCount++; - rerunAdviceMap.put(resultName, adviceFileName); - } else { - ((JKindApi) api).setReadAdviceFile(adviceFileName); - } - ((JKindApi) api).setWriteAdviceFile(adviceFileName); - } - try { - if (result instanceof ConsistencyResult) { - consistApi.execute(program, result, subMonitor); - } else if (result instanceof JRealizabilityResult) { - realApi.execute(program, (JRealizabilityResult) result, subMonitor); - } else { - api.execute(program, result, subMonitor); - } - } catch (JKindException e) { + KindApi api = PreferencesUtil.getKindApi(); + KindApi consistApi = PreferencesUtil.getConsistencyApi(); + JRealizabilityApi realApi = PreferencesUtil.getJRealizabilityApi(); - System.out.println("******** JKindException Text ********"); - e.printStackTrace(System.out); + while (!queue.isEmpty() && !globalMonitor.isCanceled()) { + JKindResult result = queue.peek(); + NullProgressMonitor subMonitor = new NullProgressMonitor(); - String errStr = e.getMessage(); - int l = Math.min(errStr.length(), 300); - System.out.println(e.getMessage().substring(0, l)); + Program program = linker.getProgram(result); - break; + if (api instanceof JKindApi) { + String resultName = result.getName(); + String adviceFileName = rerunAdviceMap.get(resultName); + if (adviceFileName == null) { + adviceFileName = "agree_advice" + adviceCount++; + rerunAdviceMap.put(resultName, adviceFileName); + } else { + ((JKindApi) api).setReadAdviceFile(adviceFileName); } + ((JKindApi) api).setWriteAdviceFile(adviceFileName); + } - // Print to property analysis log, if necessary - if (Activator.getDefault().getPreferenceStore().getBoolean(PreferenceConstants.PREF_PROP_LOG)) { - AgreeFileUtil.printLog(result, startTime, modelHash); + try { + if (result instanceof ConsistencyResult) { + consistApi.execute(program, result, subMonitor); + } else if (result instanceof JRealizabilityResult) { + realApi.execute(program, (JRealizabilityResult) result, subMonitor); + } else { + api.execute(program, result, subMonitor); } + } catch (JKindException e) { + // TODO make sure error reporting is correct + System.out.println("******** JKindException Text ********"); + e.printStackTrace(System.out); - queue.remove(); + String errStr = e.getMessage(); + int l = Math.min(errStr.length(), 300); + System.out.println(e.getMessage().substring(0, l)); + + break; } - while (!queue.isEmpty()) { - queue.remove().cancel(); + // Print to property analysis log, if necessary + if (Activator.getDefault().getPreferenceStore().getBoolean(PreferenceConstants.PREF_PROP_LOG)) { + AgreeFileUtil.printLog(result, startTime, modelHash); } -// } finally { -// deactivateTerminateHandlers(); -// enableRerunHandler(root); -// } + + queue.remove(); + } + + while (!queue.isEmpty()) { + queue.remove().cancel(); + } } }; @@ -602,7 +802,6 @@ public void run() { try { Thread.sleep(1000); } catch (InterruptedException e) { - // TODO Auto-generated catch block e.printStackTrace(); } } From d1f66fc1fb6e8e08fd16b29a94d8d04fbda05ec6 Mon Sep 17 00:00:00 2001 From: Isaac Amundson Date: Fri, 31 May 2024 19:23:25 -0500 Subject: [PATCH 4/6] output --- .../rockwellcollins/atc/agree/cli/Agree.java | 45 ++++---- .../rockwellcollins/atc/agree/cli/Util.java | 102 ++++++++++++++---- .../agree/cli/results/AgreeJsonResult.java | 5 - .../atc/agree/cli/results/AgreeOutput.java | 14 +-- 4 files changed, 116 insertions(+), 50 deletions(-) delete mode 100644 com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeJsonResult.java diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java index 4e10804be..a5a3567c7 100644 --- a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java @@ -103,7 +103,7 @@ public class Agree implements IApplication { private final static String OUTPUT = "o"; private final static String FILES = "f"; // Run options - private final static String VERIFICATION = "v"; + private final static String STRATEGY = "strategy"; // Preferences private final static String MODEL_CHECKER = "m"; private final static String SOLVER = "s"; @@ -116,7 +116,7 @@ public class Agree implements IApplication { private final static String GENERATE_BLAMED_COUNTEREXAMPLES = "generateBlamedCounterexamples"; private final static String MAX_INDUCTION_DEPTH = "maxInductionDepth"; private final static String MAX_PDR_INSTANCES = "maxPDRInstances"; - private final static String TIMEOUT = "timeout"; + private final static String TIMEOUT = "t"; private final static String CONSISTENCY_DEPTH = "consistencyDepth"; // Validation options private final static String VALIDATION_ONLY = "v"; @@ -168,6 +168,7 @@ public Object start(IApplicationContext context) throws Exception { store.setToDefault(PreferenceConstants.PREF_PDR_MAX); store.setToDefault(PreferenceConstants.PREF_TIMEOUT); store.setToDefault(PreferenceConstants.PREF_CONSIST_DEPTH); + store.setToDefault(PreferenceConstants.PREF_PROP_LOG); boolean exitOnValidationWarning = false; boolean validationOnly = false; boolean exit = false; @@ -180,7 +181,7 @@ public Object start(IApplicationContext context) throws Exception { // create Options final Options options = new Options(); options.addOption(HELP, "help", false, "print this message"); - options.addOption(NO_SPLASH, false, "optional, hide the splash screen, default false"); + options.addOption(NO_SPLASH, false, "optional, hide the splash screen"); options.addOption(DATA, true, "required, path of workspace"); options.addOption(APPLICATION, true, "required, the name of this analysis (com.rockwellcollins.atc.agree.cli.Agree)"); @@ -190,7 +191,7 @@ public Object start(IApplicationContext context) throws Exception { Option option = new Option(FILES, "files", true, "optional, supplementary AADL files (absolute paths)"); option.setArgs(Option.UNLIMITED_VALUES); options.addOption(option); - options.addOption(VERIFICATION, "verification", true, "required, verification strategy (single, all, monolithic, realizability)"); + options.addOption(STRATEGY, true, "required, verification strategy (single, all, monolithic, realizability)"); options.addOption(MODEL_CHECKER, "modelChecker", true, "optional, model checker, default " + store.getString(PreferenceConstants.PREF_MODEL_CHECKER)); options.addOption(SOLVER, "solver", true, "optional, SMT solver, default " + store.getString(PreferenceConstants.PREF_SOLVER)); options.addOption(DISABLE_K_INDUCTION, false, "optional, disable k-induction"); @@ -202,8 +203,8 @@ public Object start(IApplicationContext context) throws Exception { options.addOption(GENERATE_BLAMED_COUNTEREXAMPLES, false, "optional, generate blamed counterexamples"); options.addOption(MAX_INDUCTION_DEPTH, true, "optional, maximum induction depth, default " + store.getInt(PreferenceConstants.PREF_DEPTH)); options.addOption(MAX_PDR_INSTANCES, true, "optional, maximum number of PDR instances, default " + store.getInt(PreferenceConstants.PREF_PDR_MAX)); - options.addOption(TIMEOUT, true, "optional, timeout (ms), default " + store.getInt(PreferenceConstants.PREF_TIMEOUT)); - options.addOption(CONSISTENCY_DEPTH, true, "optional, consistency depth, default " + store.getInt(PreferenceConstants.PREF_CONSIST_DEPTH)); + options.addOption(TIMEOUT, "timeout", true, "optional, timeout (ms), default " + store.getInt(PreferenceConstants.PREF_TIMEOUT)); + options.addOption(CONSISTENCY_DEPTH, true, "optional, consistency depth, default " + store.getInt(PreferenceConstants.PREF_CONSIST_DEPTH)); options.addOption(VALIDATION_ONLY, "validationOnly", false, "validation only, default false"); options.addOption(EXIT_ON_VALIDATION_WARNING, "exitOnValidtionWarning", false, "exit on validation warning, default false"); @@ -246,8 +247,8 @@ public Object start(IApplicationContext context) throws Exception { if (commandLine.hasOption(FILES)) { fileArray = commandLine.getOptionValues(FILES); } - if (commandLine.hasOption(VERIFICATION)) { - switch (commandLine.getOptionValue(VERIFICATION).toLowerCase()) { + if (commandLine.hasOption(STRATEGY)) { + switch (commandLine.getOptionValue(STRATEGY).toLowerCase()) { case "single": strategy = VerificationStrategy.Single; break; @@ -263,7 +264,7 @@ public Object start(IApplicationContext context) throws Exception { default: exit = true; output.setStatus(AgreeOutput.INTERRUPTED); - output.addStatusMessage("Invalid verification type. " + commandLine.getOptionValue(VERIFICATION) + " is not supported."); + output.addStatusMessage("Invalid verification strategy. " + commandLine.getOptionValue(STRATEGY) + " is not supported."); } } else { exit = true; @@ -340,7 +341,7 @@ public Object start(IApplicationContext context) throws Exception { if (commandLine.hasOption(GENERATE_BLAMED_COUNTEREXAMPLES)) { store.setValue(PreferenceConstants.PREF_BLAME_CEX, true); } - if (commandLine.hasOption(MAX_INDUCTION_DEPTH)) { + if (commandLine.hasOption(MAX_INDUCTION_DEPTH)) { try { final int i = Integer.parseInt(commandLine.getOptionValue(MAX_INDUCTION_DEPTH)); if (i < 0) { @@ -489,10 +490,18 @@ public Object start(IApplicationContext context) throws Exception { } if (compImpl != null) { try { - final AnalysisResult results = runAgree(compImpl); - output.setStatus(AgreeOutput.COMPLETED); - // TODO deal with output -// output.setResults(results); + final CompositeAnalysisResult results = runAgree(compImpl); + output.setResults(results); + final jkind.api.results.Status status = results.getMultiStatus().getOverallStatus(); + if (status.equals(jkind.api.results.Status.VALID) + || status.equals(jkind.api.results.Status.VALID_REFINED)) { + output.setStatus(AgreeOutput.VALID); + } else if (status.equals(jkind.api.results.Status.INVALID) + || status.equals(jkind.api.results.Status.INCONSISTENT)) { + output.setStatus(AgreeOutput.INVALID); + } else { + output.setStatus(AgreeOutput.INTERRUPTED); + } Util.writeOutput(output, outputPath); } catch (Exception e) { e.printStackTrace(); @@ -512,7 +521,7 @@ public Object start(IApplicationContext context) throws Exception { } - private AnalysisResult runAgree(ComponentImplementation compImpl) throws Exception { + private CompositeAnalysisResult runAgree(ComponentImplementation compImpl) throws Exception { final SystemInstance si = InstantiateModel.instantiate(compImpl); AnalysisResult result; @@ -542,9 +551,9 @@ private AnalysisResult runAgree(ComponentImplementation compImpl) throws Excepti doAnalysis(compImpl, new NullProgressMonitor()); System.out.println(result.toString()); - return result; + return wrapper; } - + private AnalysisResult buildAnalysisResult(String name, ComponentInstance ci) { CompositeAnalysisResult result = new CompositeAnalysisResult("Verification for " + name); @@ -567,7 +576,7 @@ private AnalysisResult buildAnalysisResult(String name, ComponentInstance ci) { } return null; } - + private boolean containsAGREEAnnex(ComponentInstance ci) { ComponentClassifier compClass = ci.getComponentClassifier(); if (compClass instanceof ComponentImplementation) { diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Util.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Util.java index d16d819d1..2ccbea032 100644 --- a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Util.java +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Util.java @@ -10,13 +10,20 @@ import java.nio.file.Paths; import java.util.ArrayList; import java.util.Collections; +import java.util.HashMap; import java.util.List; +import java.util.Map; import java.util.stream.Collectors; import java.util.stream.Stream; import javax.xml.parsers.DocumentBuilder; import javax.xml.parsers.DocumentBuilderFactory; +import org.eclipse.core.resources.IProject; +import org.eclipse.core.resources.IProjectDescription; +import org.eclipse.core.resources.ResourcesPlugin; +import org.eclipse.core.runtime.CoreException; +import org.eclipse.core.runtime.NullProgressMonitor; import org.eclipse.emf.common.util.URI; import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.emf.ecore.resource.ResourceSet; @@ -31,6 +38,8 @@ import org.w3c.dom.Node; import org.w3c.dom.NodeList; +import com.google.gson.ExclusionStrategy; +import com.google.gson.FieldAttributes; import com.google.gson.Gson; import com.google.gson.GsonBuilder; import com.google.gson.stream.JsonWriter; @@ -38,7 +47,6 @@ import com.rockwellcollins.atc.agree.cli.results.SyntaxValidationIssue; import com.rockwellcollins.atc.agree.cli.results.SyntaxValidationResults; - public class Util { // Load project specific AADL files @@ -50,6 +58,17 @@ public static void loadProjectAadlFiles(String projPath, String[] libArray, Xtex final File projectFile = new File(projectRootDirectory, ".project"); final String projName = getProjectName(projectFile); + // Add project to workspace + addProjectToWorkspace(projPath, projName); + + // Map project folder to project name (they could be different) + final Map projMap = new HashMap<>(); + final List dotProjFiles = findFiles(projectRootDirectory.getParentFile().toPath(), "project"); + for (String dotProjFile : dotProjFiles) { + final File projFile = new File(dotProjFile); + projMap.put(getProjectName(projFile), projFile.getParentFile().getAbsolutePath()); + } + for (String pFile : projectFiles) { final File projFile = new File(pFile); loadFile(projectRootDirectory, projName, projFile, resourceSet); @@ -63,16 +82,17 @@ public static void loadProjectAadlFiles(String projPath, String[] libArray, Xtex } // load referenced project AADL files - final String projParentPath = projectRootDirectory.getParent(); final List refProjNames = new ArrayList<>(); - getRefProjName(refProjNames, projName, projParentPath); + getRefProjName(refProjNames, projName, projMap); for (String refProjName : refProjNames) { - // assuming reference project is at the same level of main project - final File refProj = new File(projParentPath, refProjName); + // Add reference project to workspace + addProjectToWorkspace(projMap.get(refProjName), refProjName); + + final File refProj = new File(projMap.get(refProjName)); final List refProjFileNames = findFiles(refProj.toPath(), "aadl"); for (String refProjFileName : refProjFileNames) { final File refProjFile = new File(refProjFileName); - loadFile(projectRootDirectory, projName, refProjFile, resourceSet); + loadFile(new File(projMap.get(refProjName)), refProjName, refProjFile, resourceSet); } } } @@ -85,7 +105,6 @@ public static SyntaxValidationResults validateResourceSet(XtextResourceSet resou int numWarnings = 0; for (Resource resource : resourceSet.getResources()) { if (resource.getURI().isPlatformResource()) { -// System.out.println("Validating " + resource.getURI().toString()); final IResourceValidator validator = ((XtextResource) resource).getResourceServiceProvider() .getResourceValidator(); final List issues = validator.validate(resource, CheckMode.ALL, CancelIndicator.NullImpl); @@ -102,7 +121,6 @@ public static SyntaxValidationResults validateResourceSet(XtextResourceSet resou valIssue.setFile(resource.getURI().toPlatformString(true)); valIssue.setLine(issue.getLineNumber()); syntaxValidationIssues.add(valIssue); -// System.out.println(issue.getMessage()); } } } @@ -121,7 +139,7 @@ private static List findFiles(Path path, String fileExtension) throws Ex try (Stream walk = Files.walk(path)) { result = walk .filter(p -> !Files.isDirectory(p)) - .map(p -> p.toString().toLowerCase()) + .map(p -> p.toString()) .filter(f -> f.endsWith(fileExtension)) .collect(Collectors.toList()); } @@ -158,7 +176,6 @@ private static Resource loadFile(File projectRootDirectory, String projectName, throw new Exception("Error loading file " + projectName + "/" + normalizedRelPath); } try { -// System.out.println("Loading " + file.getAbsolutePath()); res.load(stream, Collections.EMPTY_MAP); return res; } catch (IOException e) { @@ -176,11 +193,9 @@ private static Resource loadLibFile(String filePath, ResourceSet rs) { final URI resourceUri = URI.createPlatformResourceURI("Lib/" + path.getFileName().toString(), true); final Resource res = rs.createResource(resourceUri); -// System.out.println("Loading " + filePath); res.load(stream, Collections.EMPTY_MAP); return res; } catch (IOException e) { -// System.err.println("Error loading file " + filePath); return null; } } @@ -211,23 +226,26 @@ private static String getProjectName(File projectFile) throws Exception { } // A reference project could depend on another reference project - private static void getRefProjName(List list, String project, String parent) throws Exception { + private static void getRefProjName(List list, String projectName, Map projMap) + throws Exception { - final File refProj = new File(parent, project); - final File projectFile = new File(refProj, ".project"); - final List refProjList = getReferenceProjectName(projectFile); + final File projectFile = new File(projMap.get(projectName), ".project"); + if (!projectFile.exists()) { + throw new Exception("Project " + projectName + " was not found in the workspace."); + } + final List refProjList = getReferenceProjectNames(projectFile); if (!refProjList.isEmpty()) { for (String refProjName : refProjList) { // avoid duplicate and break circular reference if (!list.contains(refProjName)) { list.add(refProjName); - getRefProjName(list, refProjName, parent); + getRefProjName(list, refProjName, projMap); } - } + } + } } - } - private static List getReferenceProjectName(File projectFile) throws Exception { + private static List getReferenceProjectNames(File projectFile) throws Exception { final List refProjNameList = new ArrayList<>(); final DocumentBuilderFactory factory = DocumentBuilderFactory.newInstance(); final DocumentBuilder builder = factory.newDocumentBuilder(); @@ -249,10 +267,52 @@ private static List getReferenceProjectName(File projectFile) throws Exc return refProjNameList; } + /** + * When running from the command line, project must be explicitly added to the workspace + * @param projPath - Absolute path to project directory + * @param projName - Name of project + */ + private static void addProjectToWorkspace(String projPath, String projName) throws Exception { + + IProject project = ResourcesPlugin.getWorkspace().getRoot().getProject(projName); + IProjectDescription projectDescription = ResourcesPlugin.getWorkspace() + .newProjectDescription(project.getName()); + projectDescription.setLocation(new org.eclipse.core.runtime.Path(projPath)); + + try { + if (!project.exists()) { + project.create(projectDescription, new NullProgressMonitor()); + } + if (!project.isOpen()) { + project.open(new NullProgressMonitor()); + } + } catch (CoreException e) { + throw new Exception("Problem accessing project " + projName + ": " + e.getMessage()); + } + } + public static void writeOutput(AgreeOutput output, String outputPath) { + ExclusionStrategy exStrat = new ExclusionStrategy() { + + @Override + public boolean shouldSkipClass(Class arg0) { + return false; + } + + @Override + public boolean shouldSkipField(FieldAttributes f) { + return (f.getName().equals("pcs") || f.getName().equals("ticker") + || f.getName().equals("renaming") + || f.getName().equals("parent")); + } + }; + // Convert to json - final Gson gson = new GsonBuilder().setPrettyPrinting().create(); + final Gson gson = new GsonBuilder().setExclusionStrategies(exStrat) + .setPrettyPrinting() + .disableHtmlEscaping() + .create(); try { if (outputPath != null) { final File outputFile = new File(outputPath); diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeJsonResult.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeJsonResult.java deleted file mode 100644 index e3addcc77..000000000 --- a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeJsonResult.java +++ /dev/null @@ -1,5 +0,0 @@ -package com.rockwellcollins.atc.agree.cli.results; - -public class AgreeJsonResult { - -} diff --git a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeOutput.java b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeOutput.java index c3f625869..f7bde5ed3 100644 --- a/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeOutput.java +++ b/com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/results/AgreeOutput.java @@ -1,13 +1,15 @@ package com.rockwellcollins.atc.agree.cli.results; import java.util.ArrayList; -import java.util.List; +import jkind.api.results.CompositeAnalysisResult; public class AgreeOutput { public final static String COMPLETED = "Analysis Completed"; public final static String INTERRUPTED = "Analysis Interrupted"; + public final static String VALID = "No Counterexamples Found"; + public final static String INVALID = "Counterexamples Found"; private String date; private String project; @@ -15,7 +17,7 @@ public class AgreeOutput { private ArrayList statusMessages; private String status; private SyntaxValidationResults syntaxValidation; - private List results; + private CompositeAnalysisResult results; public AgreeOutput() { @@ -89,13 +91,13 @@ public void addStatusMessage(String statusMessages) { public void setSyntaxValidationResults(SyntaxValidationResults syntaxValidationResults) { this.syntaxValidation = syntaxValidationResults; } - - public List getResults() { + + + public CompositeAnalysisResult getResults() { return this.results; } - public void setResults(List results) { + public void setResults(CompositeAnalysisResult results) { this.results = results; } - } From e2c53fcab76e9a60389ea0baf25fc85e73f0cd38 Mon Sep 17 00:00:00 2001 From: Isaac Amundson Date: Wed, 5 Jun 2024 13:16:09 -0500 Subject: [PATCH 5/6] pom fix --- com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF | 2 +- com.rockwellcollins.atc.agree.cli/pom.xml | 4 ++-- com.rockwellcollins.atc.agree.feature/feature.xml | 8 +------- 3 files changed, 4 insertions(+), 10 deletions(-) diff --git a/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF b/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF index 3740b51a4..1cd46a09f 100644 --- a/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF +++ b/com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF @@ -2,7 +2,7 @@ Manifest-Version: 1.0 Bundle-ManifestVersion: 2 Bundle-Name: Cli Bundle-SymbolicName: com.rockwellcollins.atc.agree.cli;singleton:=true -Bundle-Version: 1.0.100 +Bundle-Version: 1.0.1.qualifier Bundle-Activator: com.rockwellcollins.atc.agree.cli.Activator Bundle-Vendor: ROCKWELLCOLLINS Require-Bundle: org.eclipse.ui, diff --git a/com.rockwellcollins.atc.agree.cli/pom.xml b/com.rockwellcollins.atc.agree.cli/pom.xml index a216297fa..fcec04a5a 100644 --- a/com.rockwellcollins.atc.agree.cli/pom.xml +++ b/com.rockwellcollins.atc.agree.cli/pom.xml @@ -4,10 +4,10 @@ com.rockwellcollins.atc.agree com.rockwellcollins.atc.agree.parent - 3.0.2 + 2.10.1-SNAPSHOT com.rockwellcollins.atc.agree.cli - 1.0.100 + 1.0.1-SNAPSHOT eclipse-plugin 1.5.0 diff --git a/com.rockwellcollins.atc.agree.feature/feature.xml b/com.rockwellcollins.atc.agree.feature/feature.xml index 2785d541a..989428384 100644 --- a/com.rockwellcollins.atc.agree.feature/feature.xml +++ b/com.rockwellcollins.atc.agree.feature/feature.xml @@ -76,6 +76,7 @@ SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + @@ -170,11 +171,4 @@ SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. install-size="0" version="0.0.0"/> - - From 69237cb0538b8ca5090e742b800af7692565c00f Mon Sep 17 00:00:00 2001 From: iamundson <36237616+iamundson@users.noreply.github.com> Date: Wed, 5 Jun 2024 14:22:55 -0500 Subject: [PATCH 6/6] Create README.md --- com.rockwellcollins.atc.agree.cli/README.md | 40 +++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 com.rockwellcollins.atc.agree.cli/README.md diff --git a/com.rockwellcollins.atc.agree.cli/README.md b/com.rockwellcollins.atc.agree.cli/README.md new file mode 100644 index 000000000..ea0762126 --- /dev/null +++ b/com.rockwellcollins.atc.agree.cli/README.md @@ -0,0 +1,40 @@ +# Running AGREE from the command line + +AGREE can be run from the command line. All AGREE tool preferences, along with other run options can be specified as command line arguments. Usage is as follows: + +| Argument | Description | +|---|---| +| -analyzeUnspecifiedAADLProperties | optional, analyze unspecified AADL properties | +| -application | required, the name of this analysis (com.rockwellcollins.atc.agree.cli.Agree) | +| -c,--compImpl | required, qualified component implementation name | +| -consistencyDepth | optional, consistency depth, default 1 | +| -data | required, path of workspace | +| -disableKInduction | optional, disable k-induction | +| -displayCounterexamplesAsDecimal | optional, display counterexamples as decimal | +| -f,--files | optional, supplementary AADL files (absolute paths) | +| -generateBlamedCounterexamples | optional, generate blamed counterexamples | +| -generateSmoothCounterexamples | optional, generate smooth counterexamples | +| -getSetOfSupport | optional, get set of support | +| -h,--help | print this message | +| -m,--modelChecker | optional, model checker, default JKind | +| -maxInductionDepth | optional, maximum induction depth, default 200 | +| -maxPDRInstances | optional, maximum number of PDR instances, default 0 | +| -noInductiveCounterexamples | optional, do not generate inductive counterexamples | +| -noSplash | optional, hide the splash screen | +| -o,--output | required, output JSON file absolute path | +| -p,--project | required, project path (relative to workspace) | +| -s,--solver | optional, SMT solver, default SMTInterpol | +| -strategy | required, verification strategy (single, all, monolithic, realizability) | +| -t,--timeout | optional, timeout (ms), default 100 | +| -v,--validationOnly | validation only, default false | +| -w,--exitOnValidtionWarning | exit on validation warning, default false | + +# Example + +Using the AGREE toy_example to demonstrate usage, assume the project folder is located at C:\models\toy_example. To perform a single layer analysis on the top_level.impl component in the Integer package, run the following command: + +`osate.exe -application com.rockwellcollins.atc.agree.cli.Agree -noSplash -data C:/models -p Toy_Example -c Integer_Toy::top_level.Impl -strategy single -o C:/models/toy_example/output/AgreeResults.json` + +Executing `osatec.exe` with the same arguments will capture debug output in the terminal. + +The AGREE output will be written to a file in json format if the `-o` argument is provided.