From faccada92796f08260f9b54e59b804620f20a489 Mon Sep 17 00:00:00 2001 From: Christian Menard Date: Wed, 27 Sep 2023 14:44:30 +0200 Subject: [PATCH 1/4] move invocation of verifier to GeneratorBase --- .../org/lflang/generator/GeneratorBase.java | 116 ++++++++++++++++-- .../org/lflang/generator/LFGenerator.java | 106 ---------------- 2 files changed, 104 insertions(+), 118 deletions(-) diff --git a/core/src/main/java/org/lflang/generator/GeneratorBase.java b/core/src/main/java/org/lflang/generator/GeneratorBase.java index 9a31d5d235..c8ec05755f 100644 --- a/core/src/main/java/org/lflang/generator/GeneratorBase.java +++ b/core/src/main/java/org/lflang/generator/GeneratorBase.java @@ -26,14 +26,13 @@ import com.google.common.base.Objects; import com.google.common.collect.Iterables; +import java.io.BufferedReader; +import java.io.IOException; +import java.io.InputStreamReader; import java.nio.file.Path; import java.nio.file.Paths; -import java.util.ArrayList; -import java.util.LinkedHashMap; -import java.util.LinkedHashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; +import java.util.*; +import java.util.stream.Collectors; import org.eclipse.core.resources.IMarker; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.resource.Resource; @@ -41,20 +40,17 @@ import org.eclipse.lsp4j.DiagnosticSeverity; import org.eclipse.xtext.xbase.lib.IterableExtensions; import org.eclipse.xtext.xbase.lib.IteratorExtensions; +import org.lflang.AttributeUtils; import org.lflang.FileConfig; import org.lflang.MainConflictChecker; import org.lflang.MessageReporter; import org.lflang.Target; import org.lflang.TargetConfig; +import org.lflang.analyses.uclid.UclidGenerator; import org.lflang.ast.ASTUtils; import org.lflang.ast.AstTransformation; import org.lflang.graph.InstantiationGraph; -import org.lflang.lf.Connection; -import org.lflang.lf.Instantiation; -import org.lflang.lf.LfFactory; -import org.lflang.lf.Mode; -import org.lflang.lf.Reaction; -import org.lflang.lf.Reactor; +import org.lflang.lf.*; import org.lflang.util.FileUtil; import org.lflang.validation.AbstractLFValidator; @@ -182,6 +178,12 @@ public void doGenerate(Resource resource, LFGeneratorContext context) { // Markers mark problems in the Eclipse IDE when running in integrated mode. messageReporter.clearHistory(); + // If "-c" or "--clean" is specified, delete any existing generated directories. + cleanIfNeeded(context); + + // If @property annotations are used, run the LF verifier. + runVerifierIfPropertiesDetected(resource, context); + ASTUtils.setMainName(context.getFileConfig().resource, context.getFileConfig().name); createMainInstantiation(); @@ -596,6 +598,96 @@ public void reportCommandErrors(String stderr) { } } + /** Check if a clean was requested from the standalone compiler and perform the clean step. */ + protected void cleanIfNeeded(LFGeneratorContext context) { + if (context.getArgs().containsKey("clean")) { + try { + context.getFileConfig().doClean(); + } catch (IOException e) { + System.err.println("WARNING: IO Error during clean"); + } + } + } + + /** + * Check if @property is used. If so, instantiate a UclidGenerator. The verification model needs + * to be generated before the target code since code generation changes LF program (desugar + * connections, etc.). + */ + private void runVerifierIfPropertiesDetected(Resource resource, LFGeneratorContext lfContext) { + Optional mainOpt = ASTUtils.getMainReactor(resource); + if (mainOpt.isEmpty()) return; + Reactor main = mainOpt.get(); + final MessageReporter messageReporter = lfContext.getErrorReporter(); + List properties = + AttributeUtils.getAttributes(main).stream() + .filter(attr -> attr.getAttrName().equals("property")) + .collect(Collectors.toList()); + if (properties.size() > 0) { + + // Provide a warning. + messageReporter + .nowhere() + .warning( + "Verification using \"@property\" and \"--verify\" is an experimental feature. Use" + + " with caution."); + + // Generate uclid files. + UclidGenerator uclidGenerator = new UclidGenerator(lfContext, properties); + uclidGenerator.doGenerate(resource, lfContext); + + // Check the generated uclid files. + if (uclidGenerator.targetConfig.verify) { + + // Check if Uclid5 and Z3 are installed. + if (!execInstalled("uclid", "--help", "uclid 0.9.5") + || !execInstalled("z3", "--version", "Z3 version")) { + messageReporter + .nowhere() + .error( + "Fail to check the generated verification models because Uclid5 or Z3 is not" + + " installed."); + } else { + // Run the Uclid tool. + uclidGenerator.runner.run(); + } + + } else { + messageReporter + .nowhere() + .warning( + "The \"verify\" target property is set to false. Skip checking the verification" + + " model. To check the generated verification models, set the \"verify\"" + + " target property to true or pass \"--verify\" to the lfc command"); + } + } + } + + /** + * A helper function for checking if a dependency is installed on the command line. + * + * @param binaryName The name of the binary + * @param arg An argument following the binary name + * @param expectedSubstring An expected substring in the output + * @return + */ + public static boolean execInstalled(String binaryName, String arg, String expectedSubstring) { + ProcessBuilder processBuilder = new ProcessBuilder(binaryName, arg); + try { + Process process = processBuilder.start(); + BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream())); + String line; + while ((line = reader.readLine()) != null) { + if (line.contains(expectedSubstring)) { + return true; + } + } + } catch (IOException e) { + return false; // binary not present + } + return false; + } + private void reportIssue(StringBuilder message, Integer lineNumber, Path path, int severity) { DiagnosticSeverity convertedSeverity = severity == IMarker.SEVERITY_ERROR ? DiagnosticSeverity.Error : DiagnosticSeverity.Warning; diff --git a/core/src/main/java/org/lflang/generator/LFGenerator.java b/core/src/main/java/org/lflang/generator/LFGenerator.java index 84a13f6fc8..701c57fb5a 100644 --- a/core/src/main/java/org/lflang/generator/LFGenerator.java +++ b/core/src/main/java/org/lflang/generator/LFGenerator.java @@ -2,24 +2,17 @@ import com.google.inject.Inject; import com.google.inject.Injector; -import java.io.BufferedReader; import java.io.IOException; -import java.io.InputStreamReader; import java.nio.file.Path; import java.util.Arrays; -import java.util.List; -import java.util.Optional; -import java.util.stream.Collectors; import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.xtext.generator.AbstractGenerator; import org.eclipse.xtext.generator.IFileSystemAccess2; import org.eclipse.xtext.generator.IGeneratorContext; import org.eclipse.xtext.util.RuntimeIOException; -import org.lflang.AttributeUtils; import org.lflang.FileConfig; import org.lflang.MessageReporter; import org.lflang.Target; -import org.lflang.analyses.uclid.UclidGenerator; import org.lflang.ast.ASTUtils; import org.lflang.federated.generator.FedASTUtils; import org.lflang.federated.generator.FedFileConfig; @@ -34,8 +27,6 @@ import org.lflang.generator.rust.RustGenerator; import org.lflang.generator.ts.TSFileConfig; import org.lflang.generator.ts.TSGenerator; -import org.lflang.lf.Attribute; -import org.lflang.lf.Reactor; import org.lflang.scoping.LFGlobalScopeProvider; /** Generates code from your model files on save. */ @@ -117,13 +108,6 @@ public void doGenerate(Resource resource, IFileSystemAccess2 fsa, IGeneratorCont } } else { - - // If "-c" or "--clean" is specified, delete any existing generated directories. - cleanIfNeeded(lfContext); - - // If @property annotations are used, run the LF verifier. - runVerifierIfPropertiesDetected(resource, lfContext); - final GeneratorBase generator = createGenerator(lfContext); if (generator != null) { @@ -141,94 +125,4 @@ public void doGenerate(Resource resource, IFileSystemAccess2 fsa, IGeneratorCont public boolean errorsOccurred() { return generatorErrorsOccurred; } - - /** Check if a clean was requested from the standalone compiler and perform the clean step. */ - protected void cleanIfNeeded(LFGeneratorContext context) { - if (context.getArgs().containsKey("clean")) { - try { - context.getFileConfig().doClean(); - } catch (IOException e) { - System.err.println("WARNING: IO Error during clean"); - } - } - } - - /** - * Check if @property is used. If so, instantiate a UclidGenerator. The verification model needs - * to be generated before the target code since code generation changes LF program (desugar - * connections, etc.). - */ - private void runVerifierIfPropertiesDetected(Resource resource, LFGeneratorContext lfContext) { - Optional mainOpt = ASTUtils.getMainReactor(resource); - if (mainOpt.isEmpty()) return; - Reactor main = mainOpt.get(); - final MessageReporter messageReporter = lfContext.getErrorReporter(); - List properties = - AttributeUtils.getAttributes(main).stream() - .filter(attr -> attr.getAttrName().equals("property")) - .collect(Collectors.toList()); - if (properties.size() > 0) { - - // Provide a warning. - messageReporter - .nowhere() - .warning( - "Verification using \"@property\" and \"--verify\" is an experimental feature. Use" - + " with caution."); - - // Generate uclid files. - UclidGenerator uclidGenerator = new UclidGenerator(lfContext, properties); - uclidGenerator.doGenerate(resource, lfContext); - - // Check the generated uclid files. - if (uclidGenerator.targetConfig.verify) { - - // Check if Uclid5 and Z3 are installed. - if (!execInstalled("uclid", "--help", "uclid 0.9.5") - || !execInstalled("z3", "--version", "Z3 version")) { - messageReporter - .nowhere() - .error( - "Fail to check the generated verification models because Uclid5 or Z3 is not" - + " installed."); - } else { - // Run the Uclid tool. - uclidGenerator.runner.run(); - } - - } else { - messageReporter - .nowhere() - .warning( - "The \"verify\" target property is set to false. Skip checking the verification" - + " model. To check the generated verification models, set the \"verify\"" - + " target property to true or pass \"--verify\" to the lfc command"); - } - } - } - - /** - * A helper function for checking if a dependency is installed on the command line. - * - * @param binaryName The name of the binary - * @param arg An argument following the binary name - * @param expectedSubstring An expected substring in the output - * @return - */ - public static boolean execInstalled(String binaryName, String arg, String expectedSubstring) { - ProcessBuilder processBuilder = new ProcessBuilder(binaryName, arg); - try { - Process process = processBuilder.start(); - BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream())); - String line; - while ((line = reader.readLine()) != null) { - if (line.contains(expectedSubstring)) { - return true; - } - } - } catch (IOException e) { - return false; // binary not present - } - return false; - } } From 5d22a1aaba23ee6df565c360e92fa726f7129a88 Mon Sep 17 00:00:00 2001 From: Christian Menard Date: Wed, 27 Sep 2023 16:05:12 +0200 Subject: [PATCH 2/4] no need to use a custom mechanism for detecting if tools are installed --- .../org/lflang/generator/GeneratorBase.java | 45 ++++--------------- 1 file changed, 9 insertions(+), 36 deletions(-) diff --git a/core/src/main/java/org/lflang/generator/GeneratorBase.java b/core/src/main/java/org/lflang/generator/GeneratorBase.java index c8ec05755f..12194f5993 100644 --- a/core/src/main/java/org/lflang/generator/GeneratorBase.java +++ b/core/src/main/java/org/lflang/generator/GeneratorBase.java @@ -26,9 +26,7 @@ import com.google.common.base.Objects; import com.google.common.collect.Iterables; -import java.io.BufferedReader; import java.io.IOException; -import java.io.InputStreamReader; import java.nio.file.Path; import java.nio.file.Paths; import java.util.*; @@ -178,6 +176,13 @@ public void doGenerate(Resource resource, LFGeneratorContext context) { // Markers mark problems in the Eclipse IDE when running in integrated mode. messageReporter.clearHistory(); + // Configure the command factory + commandFactory.setVerbose(); + if (Objects.equal(context.getMode(), LFGeneratorContext.Mode.STANDALONE) + && context.getArgs().containsKey("quiet")) { + commandFactory.setQuiet(); + } + // If "-c" or "--clean" is specified, delete any existing generated directories. cleanIfNeeded(context); @@ -196,13 +201,6 @@ public void doGenerate(Resource resource, LFGeneratorContext context) { } } - // Configure the command factory - commandFactory.setVerbose(); - if (Objects.equal(context.getMode(), LFGeneratorContext.Mode.STANDALONE) - && context.getArgs().containsKey("quiet")) { - commandFactory.setQuiet(); - } - // Process target files. Copy each of them into the src-gen dir. // FIXME: Should we do this here? This doesn't make sense for federates the way it is // done here. @@ -640,8 +638,8 @@ private void runVerifierIfPropertiesDetected(Resource resource, LFGeneratorConte if (uclidGenerator.targetConfig.verify) { // Check if Uclid5 and Z3 are installed. - if (!execInstalled("uclid", "--help", "uclid 0.9.5") - || !execInstalled("z3", "--version", "Z3 version")) { + if (commandFactory.createCommand("uclid", List.of()) == null + || commandFactory.createCommand("z3", List.of()) == null) { messageReporter .nowhere() .error( @@ -663,31 +661,6 @@ private void runVerifierIfPropertiesDetected(Resource resource, LFGeneratorConte } } - /** - * A helper function for checking if a dependency is installed on the command line. - * - * @param binaryName The name of the binary - * @param arg An argument following the binary name - * @param expectedSubstring An expected substring in the output - * @return - */ - public static boolean execInstalled(String binaryName, String arg, String expectedSubstring) { - ProcessBuilder processBuilder = new ProcessBuilder(binaryName, arg); - try { - Process process = processBuilder.start(); - BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream())); - String line; - while ((line = reader.readLine()) != null) { - if (line.contains(expectedSubstring)) { - return true; - } - } - } catch (IOException e) { - return false; // binary not present - } - return false; - } - private void reportIssue(StringBuilder message, Integer lineNumber, Path path, int severity) { DiagnosticSeverity convertedSeverity = severity == IMarker.SEVERITY_ERROR ? DiagnosticSeverity.Error : DiagnosticSeverity.Warning; From 788ddd8eb882c005f36fea85bc7c415fa64eb5a1 Mon Sep 17 00:00:00 2001 From: Christian Menard Date: Wed, 27 Sep 2023 16:05:59 +0200 Subject: [PATCH 3/4] don't exit, but report an error message --- .../lflang/analyses/uclid/UclidRunner.java | 27 +++++++++---------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java b/core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java index b2fe3ecc71..201127af3d 100644 --- a/core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java +++ b/core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java @@ -13,6 +13,7 @@ import org.json.JSONArray; import org.json.JSONException; import org.json.JSONObject; +import org.lflang.MessageReporter; import org.lflang.analyses.statespace.StateInfo; import org.lflang.analyses.statespace.Tag; import org.lflang.generator.GeneratorCommandFactory; @@ -21,21 +22,18 @@ /** (EXPERIMENTAL) Runner for Uclid5 models. */ public class UclidRunner { - /** A list of paths to the generated files */ - List filePaths; - - /** The directory where the generated files are placed */ - public Path outputDir; - /** A factory for compiler commands. */ GeneratorCommandFactory commandFactory; /** A UclidGenerator instance */ UclidGenerator generator; + MessageReporter reporter; + // Constructor public UclidRunner(UclidGenerator generator) { this.generator = generator; + this.reporter = generator.context.getErrorReporter(); this.commandFactory = new GeneratorCommandFactory( generator.context.getErrorReporter(), generator.context.getFileConfig()); @@ -175,7 +173,7 @@ public void run() { command.run(); String output = command.getOutput().toString(); - boolean valid = !output.contains("FAILED"); + boolean valid = !output.contains("failed"); if (valid) { System.out.println("Valid!"); } else { @@ -213,7 +211,7 @@ public void run() { info.display(); } } catch (IOException e) { - System.out.println("ERROR: Not able to read from " + path.toString()); + reporter.nowhere().error("Not able to read from " + path); } } @@ -223,12 +221,13 @@ public void run() { if (expect != null) { boolean expectValid = Boolean.parseBoolean(expect); if (expectValid != valid) { - System.out.println( - "ERROR: The expected result does not match the actual result. Expected: " - + expectValid - + ", Result: " - + valid); - System.exit(1); + reporter + .nowhere() + .error( + "ERROR: The expected result does not match the actual result. Expected: " + + expectValid + + ", Result: " + + valid); } } } From cf50460f599e10ea57dea79034fafccaf6311a60 Mon Sep 17 00:00:00 2001 From: Christian Menard Date: Wed, 27 Sep 2023 17:00:32 +0200 Subject: [PATCH 4/4] fix string that is matched to check if verification was successful --- core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java b/core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java index 201127af3d..4ec0703c79 100644 --- a/core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java +++ b/core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java @@ -173,7 +173,7 @@ public void run() { command.run(); String output = command.getOutput().toString(); - boolean valid = !output.contains("failed"); + boolean valid = output.contains("PASSED"); if (valid) { System.out.println("Valid!"); } else {