Merge branch 'master' into highprecision

nickbattle · Nov 11, 2024 · 9c86b2d · 9c86b2d
2 parents 0e47ba6 + 38e0eb7
commit 9c86b2d
Show file tree

Hide file tree

Showing 21 changed files with 261 additions and 150 deletions.
diff --git a/annotations/documentation/AnnotationGuide.odt b/annotations/documentation/AnnotationGuide.odt
diff --git a/annotations/documentation/AnnotationGuide.pdf b/annotations/documentation/AnnotationGuide.pdf
diff --git a/lsp/src/main/java/lsp/LSPServerDebug.java b/lsp/src/main/java/lsp/LSPServerDebug.java
@@ -129,6 +129,7 @@ public void run()
 				catch (IOException e)
 				{
 					Diag.severe("LSP Server stopped: %s", e.getMessage());
+					Diag.error(e);
 				}
 
 				Diag.info("LSP %s Server closing port %d", dialect, socket.getLocalPort());

diff --git a/lsp/src/main/java/lsp/LSPServerStdio.java b/lsp/src/main/java/lsp/LSPServerStdio.java
@@ -106,6 +106,7 @@ public void run()
 		catch (IOException e)
 		{
 			Diag.error("LSP Server stopped: %s", e.getMessage());
+			Diag.error(e);
 		}
 	}
 }
diff --git a/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java
@@ -87,7 +87,13 @@ protected JSONArray launchArgs(ProofObligation po, String defaultName, boolean d
 
 		if (!apply.applyTypes.isEmpty())
 		{
-			JSONArray applyTypes = new JSONArray(apply.applyTypes);
+			JSONArray applyTypes = new JSONArray();
+
+			for (String atype: apply.applyTypes)
+			{
+				applyTypes.add(atype);
+			}
+
 			launchArgs.put("applyTypes", applyTypes);
 		}
 

diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java
@@ -84,12 +84,12 @@
 
 public class QuickCheck
 {
-	private static final long DEFAULT_TIMEOUT = 5 * 1000;	// 5s timeout
+	public static final long DEFAULT_TIMEOUT = 5000;	// 5s timeout
+
 	private int errorCount = 0;
 	private List<QCStrategy> strategies = null;		// Configured to be used
 	private List<QCStrategy> disabled = null;		// Known, but not to be used
 	private ProofObligationList chosen = null;
-	private long timeout = 0;
 
 	public QuickCheck()
 	{
@@ -183,9 +183,8 @@ else if ((names.isEmpty() && instance.useByDefault()) || names.contains(instance
 		}
 	}
 
-	public boolean initStrategies(long timeoutSecs)
+	public boolean initStrategies()
 	{
-		this.timeout = (timeoutSecs < 0) ? DEFAULT_TIMEOUT : timeoutSecs * 1000;
 		boolean doChecks = true;
 
 		for (QCStrategy strategy: strategies)
@@ -324,8 +323,6 @@ public StrategyResults getValues(ProofObligation po)
 		IterableContext ictxt = addTypeParams(po, ctxt);
 		boolean hasAllValues = false;
 		long before = System.currentTimeMillis();
-		INBindingGlobals globals = INBindingGlobals.getInstance();
-		globals.setTimeout(timeout);	// Strategies can use this
 
 		while (ictxt.hasNext())
 		{
@@ -334,7 +331,25 @@ public StrategyResults getValues(ProofObligation po)
 			for (QCStrategy strategy: strategies)
 			{
 				verbose("------------------------ Invoking %s strategy on PO #%d\n", strategy.getName(), po.number);
-				StrategyResults sresults = strategy.getValues(po, binds, ictxt);
+				StrategyResults sresults = null;
+
+				try
+				{
+					// Suspend annotation execution by the interpreter, because the
+					// expansion of invariant types can invoke them.
+					INAnnotation.suspend(true);
+
+					sresults = strategy.getValues(po, binds, ictxt);
+				}
+				catch (Throwable t)
+				{
+					errorln("Strategy " + strategy.getName() + " failed to generate values: " + t);
+					continue;
+				}
+				finally
+				{
+					INAnnotation.suspend(false);
+				}
 
 				if (sresults.provedBy != null || sresults.disprovedBy != null)	// No need to go further
 				{
@@ -465,9 +480,7 @@ else if (sresults.disprovedBy != null)
 					}
 				}
 
-				globals.setTimeout(timeout);
 				globals.setAllValues(sresults.hasAllValues);
-
 				Context ctxt = Interpreter.getInstance().getInitialContext();
 				Interpreter.getInstance().setDefaultName(po.location.module);
 
@@ -476,6 +489,7 @@ else if (sresults.disprovedBy != null)
 				Value execResult = new BooleanValue(false);
 				ContextException execException = null;
 				boolean execCompleted = false;
+				boolean timedOut = false;
 				long before = System.currentTimeMillis();
 
 				try
@@ -499,7 +513,8 @@ else if (sresults.disprovedBy != null)
 				{
 					if (e.rawMessage.equals("Execution cancelled"))
 					{
-						execResult = null;
+						execResult = new BooleanValue(false);
+						timedOut = true;
 					}
 					else if (e.number == 4024)	// 'not yet specified' expression reached
 					{
@@ -519,23 +534,18 @@ else if (e.number == 4024)	// 'not yet specified' expression reached
 
 				long after = System.currentTimeMillis() + sresults.duration;
 
-				if (execResult == null)		// cancelled
-				{
-					infoln("----");
-					printBindings(bindings);
-					infoln("----");
-					infoln(po);
-				}
-				else if (execResult instanceof BooleanValue)
+				if (execResult instanceof BooleanValue)
 				{
 					if (execResult.boolValue(ctxt))
 					{
 						POStatus outcome = null;
 						String desc = "";
 						po.setWitness(null);
 						po.setProvedBy(null);
+						po.setCounterexample(null);
+						po.setMessage(null);
 
-						if (globals.didTimeout())
+						if (timedOut)
 						{
 							outcome = POStatus.TIMEOUT;
 						}
@@ -558,8 +568,17 @@ else if (po.isExistential())
 						else if (sresults.hasAllValues && execCompleted)
 						{
 							outcome = POStatus.PROVABLE;		// All values were tested and passed, so PROVABLE
-							desc = " by finite types";
-							po.setProvedBy("finite");
+
+							if (bindings.isEmpty())
+							{
+								desc = " in all cases";
+								po.setProvedBy("fixed");
+							}
+							else
+							{
+								desc = " by finite types";
+								po.setProvedBy("finite");
+							}
 						}
 						else
 						{
@@ -568,12 +587,10 @@ else if (sresults.hasAllValues && execCompleted)
 
 						infof(outcome, "PO #%d, %s%s %s\n", po.number, outcome.toString().toUpperCase(), desc, duration(before, after));
 						po.setStatus(outcome);
-						po.setCounterexample(null);
-						po.setMessage(null);
 					}
 					else
 					{
-						if (globals.didTimeout())		// Result would have been true (above), but...
+						if (timedOut)		// Result would have been true (above), but...
 						{
 							infof(POStatus.TIMEOUT, "PO #%d, TIMEOUT %s\n", po.number, duration(before, after));
 							po.setStatus(POStatus.TIMEOUT);
@@ -614,7 +631,16 @@ else if (globals.hasMaybe() && execCompleted)
 							infof(POStatus.FAILED, "PO #%d, FAILED %s: ", po.number, duration(before, after));
 							po.setStatus(POStatus.FAILED);
 							printCounterexample(bindings);
-							po.setCounterexample(globals.getCounterexample());
+
+							if (bindings.isEmpty())		// Failed with no binds - eg. Test() with no params
+							{
+								po.setCounterexample(new Context(po.location, "Empty", null));
+							}
+							else
+							{
+								po.setCounterexample(globals.getCounterexample());
+							}
+
 							po.setWitness(null);
 
 							if (execException != null)
@@ -929,8 +955,8 @@ public void printHelp(String USAGE)
 		println(USAGE);
 		println("");
 		println("  -?|-help           - show command help");
-		println("  -q|-v              - run with minimal or verbose output");
-		println("  -t <secs>          - timeout in secs");
+		println("  -q|-v|-n           - run with minimal, verbose, basic output");
+		println("  -t <msecs>         - timeout in millisecs");
 		println("  -i <status>        - only show this result status");
 		println("  -s <strategy>      - enable this strategy (below)");
 		println("  -<strategy:option> - pass option to strategy");

diff --git a/quickcheck/src/main/java/quickcheck/commands/QCConsole.java b/quickcheck/src/main/java/quickcheck/commands/QCConsole.java
@@ -59,10 +59,20 @@ public static void setIncludes(List<POStatus> includes)
 		QCConsole.includes = includes;
 	}
 
+	public static List<POStatus> getIncludes()
+	{
+		return includes;
+	}
+
 	public static void setVerbose(boolean verbose)
 	{
 		QCConsole.verbose = verbose;
 	}
+
+	public boolean getVerbose()
+	{
+		return verbose;
+	}
 
 	public static void info(POStatus status, String m)
 	{

diff --git a/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java b/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java
@@ -34,8 +34,9 @@
 
 import com.fujitsu.vdmj.Settings;
 import com.fujitsu.vdmj.debug.ConsoleDebugReader;
-import com.fujitsu.vdmj.debug.ConsoleKeyWatcher;
+import com.fujitsu.vdmj.debug.ConsoleExecTimer;
 import com.fujitsu.vdmj.lex.Dialect;
+import com.fujitsu.vdmj.messages.Console;
 import com.fujitsu.vdmj.plugins.AnalysisCommand;
 import com.fujitsu.vdmj.plugins.PluginRegistry;
 import com.fujitsu.vdmj.plugins.analyses.POPlugin;
@@ -48,11 +49,11 @@
 
 public class QuickCheckCommand extends AnalysisCommand
 {
-	private final static String CMD = "quickcheck [-?|-help][-q|-v][-t <secs>][-i <status>]*[-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]";
+	private final static String CMD = "quickcheck [-?|-help][-q|-v|-n][-t <secs>][-i <status>]*[-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]";
 	private final static String SHORT = "quickcheck [-help][<options>][<POs>]";
 	private final static String USAGE = "Usage: " + CMD;
 	public  final static String HELP = SHORT + " - lightweight PO verification";
-			
+
 	public QuickCheckCommand(String line)
 	{
 		super(line);
@@ -70,6 +71,7 @@ public String run(String line)
 		List<String> poNames = new Vector<String>();
 		List<POStatus> includes = new Vector<POStatus>();
 		long timeout = -1;
+		boolean numbersOnly = false;
 
 		QuickCheck qc = new QuickCheck();
 
@@ -122,6 +124,11 @@ public String run(String line)
 							return USAGE;
 						}
 						break;
+
+					case "-n":
+						numbersOnly = true;
+						QCConsole.setQuiet(true);
+						break;
 
 					case "-":
 						i++;
@@ -185,8 +192,10 @@ public String run(String line)
 			println("No POs in current " + (Settings.dialect == Dialect.VDM_SL ? "module" : "class"));
 			return null;
 		}
-
-		if (qc.initStrategies(timeout))
+
+		timeout = (timeout < 0) ? QuickCheck.DEFAULT_TIMEOUT : timeout;
+
+		if (qc.initStrategies())
 		{
 			for (ProofObligation po: chosen)
 			{
@@ -195,27 +204,35 @@ public String run(String line)
 
 				if (!qc.hasErrors())
 				{
-					ConsoleKeyWatcher watcher = null;
+					ConsoleExecTimer execTimer = null;
 					ConsoleDebugReader dbg = null;
 
 					try
 					{
 						dbg = new ConsoleDebugReader();
 						dbg.start();
-						watcher = new ConsoleKeyWatcher(line);
-						watcher.start();
+						execTimer = new ConsoleExecTimer(timeout);
+						execTimer.start();
 
 						qc.checkObligation(po, results);
+
+						if (numbersOnly)
+						{
+							if (includes.isEmpty() || includes.contains(po.status))
+							{
+								Console.out.printf("PO #%d: %s\n", po.number, po.status.toString().toUpperCase());
+							}
+						}
 					}
 					catch (Exception e)
 					{
 						errorln(e);
 					}
 					finally
 					{
-						if (watcher != null)
+						if (execTimer != null)
 						{
-							watcher.interrupt();
+							execTimer.interrupt();
 						}
 
 						if (dbg != null)