Skip to content

Commit

Permalink
Merge pull request #2031 from lf-lang/verifier-fix
Browse files Browse the repository at this point in the history 
Fixed error reporting in the verifier
  • Loading branch information
@cmnrd
cmnrd authored Sep 28, 2023
2 parents 93aef01 + cf50460 commit bee1d9f
Show file tree
Hide file tree
Showing 3 changed files with 97 additions and 139 deletions.
27 changes: 13 additions & 14 deletions core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -21,21 +22,18 @@
/** (EXPERIMENTAL) Runner for Uclid5 models. */
public class UclidRunner {

/** A list of paths to the generated files */
List<Path> 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());
Expand Down Expand Up @@ -175,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 {
Expand Down Expand Up @@ -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);
}
}

Expand All @@ -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);
}
}
}
Expand Down
103 changes: 84 additions & 19 deletions core/src/main/java/org/lflang/generator/GeneratorBase.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,35 +26,29 @@

import com.google.common.base.Objects;
import com.google.common.collect.Iterables;
import java.io.IOException;
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;
import org.eclipse.emf.ecore.util.EcoreUtil;
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;

Expand Down Expand Up @@ -182,6 +176,19 @@ 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);

// If @property annotations are used, run the LF verifier.
runVerifierIfPropertiesDetected(resource, context);

ASTUtils.setMainName(context.getFileConfig().resource, context.getFileConfig().name);

createMainInstantiation();
Expand All @@ -194,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.
Expand Down Expand Up @@ -596,6 +596,71 @@ 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<Reactor> mainOpt = ASTUtils.getMainReactor(resource);
if (mainOpt.isEmpty()) return;
Reactor main = mainOpt.get();
final MessageReporter messageReporter = lfContext.getErrorReporter();
List<Attribute> 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 (commandFactory.createCommand("uclid", List.of()) == null
|| commandFactory.createCommand("z3", List.of()) == null) {
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");
}
}
}

private void reportIssue(StringBuilder message, Integer lineNumber, Path path, int severity) {
DiagnosticSeverity convertedSeverity =
severity == IMarker.SEVERITY_ERROR ? DiagnosticSeverity.Error : DiagnosticSeverity.Warning;
Expand Down
106 changes: 0 additions & 106 deletions core/src/main/java/org/lflang/generator/LFGenerator.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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. */
Expand Down Expand Up @@ -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) {
Expand All @@ -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<Reactor> mainOpt = ASTUtils.getMainReactor(resource);
if (mainOpt.isEmpty()) return;
Reactor main = mainOpt.get();
final MessageReporter messageReporter = lfContext.getErrorReporter();
List<Attribute> 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;
}
}

0 comments on commit bee1d9f

Please sign in to comment.