Merge pull request #79 from ftsrg/identifiers

Add --stacktrace option to cli tools
ftsrg · Sep 7, 2020 · 6bea2e0 · 6bea2e0
2 parents 7559648 + 3212b18
commit 6bea2e0
Show file tree

Hide file tree

Showing 11 changed files with 68 additions and 26 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.0.1"
+    version = "2.1.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/cfa-cli/README.md b/subprojects/cfa-cli/README.md
@@ -102,5 +102,6 @@ Otherwise, the output is simply in `dot` format.
 
 | Flag | Description |
 |--|--|
+| `--stacktrace` | Print full stack trace for exceptions. |
 | `--benchmark` | Benchmark mode, only print metrics in csv format. |
 | `--header` | Print the header for the benchmark mode csv format. |
diff --git a/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java
@@ -121,6 +121,9 @@ public class CfaCli {
 	@Parameter(names = "--metrics", description = "Print metrics about the CFA without running the algorithm")
 	boolean metrics = false;
 
+	@Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception")
+	boolean stacktrace = false;
+
 	private Logger logger;
 
 	public CfaCli(final String[] args) {
@@ -296,10 +299,15 @@ private void printError(final Throwable ex) {
 			writer.cell("[EX] " + ex.getClass().getSimpleName() + message);
 		} else {
 			logger.write(Level.RESULT, "Exception of type %s occurred%n", ex.getClass().getSimpleName());
-			logger.write(Level.MAINSTEP, "Message:%n%s%n", ex.getMessage());
-			final StringWriter errors = new StringWriter();
-			ex.printStackTrace(new PrintWriter(errors));
-			logger.write(Level.SUBSTEP, "Trace:%n%s%n", errors.toString());
+			logger.write(Level.RESULT, "Message:%n%s%n", ex.getMessage());
+			if (stacktrace) {
+				final StringWriter errors = new StringWriter();
+				ex.printStackTrace(new PrintWriter(errors));
+				logger.write(Level.RESULT, "Trace:%n%s%n", errors.toString());
+			}
+			else {
+				logger.write(Level.RESULT, "Use --stacktrace for stack trace%n");
+			}
 		}
 	}
 

diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java
@@ -41,9 +41,7 @@
 import org.antlr.v4.runtime.Token;
 
 import java.math.BigInteger;
-import java.util.Collection;
-import java.util.Collections;
-import java.util.List;
+import java.util.*;
 import java.util.stream.Collectors;
 import java.util.stream.IntStream;
 import java.util.stream.Stream;
@@ -801,7 +799,9 @@ private boolean[] decodeHexadecimalBvContent(String lit) {
 
 		@Override
 		public RefExpr<?> visitIdExpr(final IdExprContext ctx) {
-			final Symbol symbol = currentScope.resolve(ctx.id.getText()).get();
+			Optional<? extends Symbol> optSymbol = currentScope.resolve(ctx.id.getText());
+			if (optSymbol.isEmpty()) throw new NoSuchElementException("Identifier '" + ctx.id.getText() + "' not found");
+			final Symbol symbol = optSymbol.get();
 			final Decl<?> decl = (Decl<?>) env.eval(symbol);
 			return decl.getRef();
 		}

diff --git a/subprojects/sts-cli/README.md b/subprojects/sts-cli/README.md
@@ -80,5 +80,6 @@ All arguments are optional, except `--model`.
 
 | Flag | Description |
 |--|--|
+| `--stacktrace` | Print full stack trace for exceptions. |
 | `--benchmark` | Benchmark mode, only print metrics in csv format. |
 | `--header` | Print the header for the benchmark mode csv format. |
diff --git a/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java
@@ -100,6 +100,9 @@ public class StsCli {
 	@Parameter(names = {"--header"}, description = "Print only a header (for benchmarks)", help = true)
 	boolean headerOnly = false;
 
+	@Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception")
+	boolean stacktrace = false;
+
 	private Logger logger;
 
 	public StsCli(final String[] args) {
@@ -206,10 +209,15 @@ private void printError(final Throwable ex) {
 			writer.cell("[EX] " + ex.getClass().getSimpleName() + message);
 		} else {
 			logger.write(Level.RESULT, "Exception of type %s occurred%n", ex.getClass().getSimpleName());
-			logger.write(Level.MAINSTEP, "Message:%n%s%n", ex.getMessage());
-			final StringWriter errors = new StringWriter();
-			ex.printStackTrace(new PrintWriter(errors));
-			logger.write(Level.SUBSTEP, "Trace:%n%s%n", errors.toString());
+			logger.write(Level.RESULT, "Message:%n%s%n", ex.getMessage());
+			if (stacktrace) {
+				final StringWriter errors = new StringWriter();
+				ex.printStackTrace(new PrintWriter(errors));
+				logger.write(Level.RESULT, "Trace:%n%s%n", errors.toString());
+			}
+			else {
+				logger.write(Level.RESULT, "Use --stacktrace for stack trace%n");
+			}
 		}
 	}
 

diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java b/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java
@@ -44,6 +44,7 @@
 import java.math.BigInteger;
 import java.util.Collection;
 import java.util.List;
+import java.util.NoSuchElementException;
 import java.util.Optional;
 import java.util.stream.Stream;
 
@@ -535,7 +536,7 @@ public RatLitExpr visitRatLitExpr(final RatLitExprContext ctx) {
 	public Expr<?> visitIdExpr(final IdExprContext ctx) {
 		final Optional<? extends Symbol> optSymbol = currentScope.resolve(ctx.id.getText());
 
-		checkArgument(optSymbol.isPresent());
+		if (optSymbol.isEmpty()) throw new NoSuchElementException("Identifier '" + ctx.id.getText() + "' not found");
 		final Symbol symbol = optSymbol.get();
 
 		checkArgument(symbol instanceof DeclSymbol);

diff --git a/subprojects/xsts-cli/README.md b/subprojects/xsts-cli/README.md
@@ -91,5 +91,6 @@ In general, values between `5` to `50` perform well (see Section 3.1.1 of [our J
 
 | Flag | Description |
 |--|--|
+| `--stacktrace` | Print full stack trace for exceptions. |
 | `--benchmark` | Benchmark mode, only print metrics in csv format. |
 | `--header` | Print the header for the benchmark mode csv format. |
diff --git a/subprojects/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java b/subprojects/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java
@@ -86,6 +86,9 @@ public class XstsCli {
     @Parameter(names = {"--header"}, description = "Print only a header (for benchmarks)", help = true)
     boolean headerOnly = false;
 
+    @Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception")
+    boolean stacktrace = false;
+
     private Logger logger;
 
     public XstsCli(final String[] args) {
@@ -189,10 +192,15 @@ private void printError(final Throwable ex) {
             writer.cell("[EX] " + ex.getClass().getSimpleName() + message);
         } else {
             logger.write(Logger.Level.RESULT, "Exception of type %s occurred%n", ex.getClass().getSimpleName());
-            logger.write(Logger.Level.MAINSTEP, "Message:%n%s%n", ex.getMessage());
-            final StringWriter errors = new StringWriter();
-            ex.printStackTrace(new PrintWriter(errors));
-            logger.write(Logger.Level.SUBSTEP, "Trace:%n%s%n", errors.toString());
+            logger.write(Logger.Level.RESULT, "Message:%n%s%n", ex.getMessage());
+            if (stacktrace) {
+                final StringWriter errors = new StringWriter();
+                ex.printStackTrace(new PrintWriter(errors));
+                logger.write(Logger.Level.RESULT, "Trace:%n%s%n", errors.toString());
+            }
+            else {
+                logger.write(Logger.Level.RESULT, "Use --stacktrace for stack trace%n");
+            }
         }
     }
 

diff --git a/subprojects/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java b/subprojects/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java
@@ -15,10 +15,7 @@
  */
 package hu.bme.mit.theta.xta.cli;
 
-import java.io.FileInputStream;
-import java.io.FileNotFoundException;
-import java.io.IOException;
-import java.io.InputStream;
+import java.io.*;
 
 import com.beust.jcommander.JCommander;
 import com.beust.jcommander.Parameter;
@@ -30,6 +27,7 @@
 import hu.bme.mit.theta.analysis.unit.UnitPrec;
 import hu.bme.mit.theta.analysis.utils.ArgVisualizer;
 import hu.bme.mit.theta.analysis.utils.TraceVisualizer;
+import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.common.table.BasicTableWriter;
 import hu.bme.mit.theta.common.table.TableWriter;
 import hu.bme.mit.theta.common.visualization.Graph;
@@ -67,6 +65,9 @@ public final class XtaCli {
 	@Parameter(names = {"--header", "-h"}, description = "Print only a header (for benchmarks)", help = true)
 	boolean headerOnly = false;
 
+	@Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception")
+	boolean stacktrace = false;
+
 	public XtaCli(final String[] args) {
 		this.args = args;
 		this.writer = new BasicTableWriter(System.out, ",", "\"", "\"");
@@ -125,10 +126,19 @@ private void printError(final Throwable ex) {
 		final String message = ex.getMessage() == null ? "" : ": " + ex.getMessage();
 		if (benchmarkMode) {
 			writer.cell("[EX] " + ex.getClass().getSimpleName() + message);
-			writer.newRow();
 		} else {
-			System.out.println("Exception occured: " + ex.getClass().getSimpleName());
-			System.out.println("Message: " + ex.getMessage());
+			System.out.println("Exception of type " + ex.getClass().getSimpleName() + " occurred");
+			System.out.println("Message:");
+			System.out.println(ex.getMessage());
+			if (stacktrace) {
+				final StringWriter errors = new StringWriter();
+				ex.printStackTrace(new PrintWriter(errors));
+				System.out.println("Trace:");
+				System.out.println(errors);
+			}
+			else {
+				System.out.println("Use --stacktrace for stack trace");
+			}
 		}
 	}
 

diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaExpression.java b/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaExpression.java
@@ -44,6 +44,8 @@
 import java.math.BigInteger;
 import java.util.Collection;
 import java.util.List;
+import java.util.NoSuchElementException;
+import java.util.Optional;
 import java.util.stream.Stream;
 
 import static com.google.common.base.Preconditions.checkArgument;
@@ -115,7 +117,9 @@ public Expr<?> visitFalseExpression(final FalseExpressionContext ctx) {
         @Override
         public Expr<?> visitIdExpression(final IdExpressionContext ctx) {
             final String name = ctx.fId.getText();
-            final Symbol symbol = scope.resolve(name).get();
+            Optional<? extends Symbol> optSymbol = scope.resolve(name);
+            if (optSymbol.isEmpty()) throw new NoSuchElementException("Identifier '" + name + "' not found");
+            final Symbol symbol = optSymbol.get();
 
             if (env.isDefined(symbol)) {
                 // A variable, synchronization label, or a constant already defined