Introduce IOExecTemplate operator

This operator makes it a bit easier to invoke processes by using the `%s`
format specifier as an argument placeholder.

Note that this this does not allow for spaces in the process path (e.g.
`C:\Program Files\...`) and only supports a single `%s` within a word
(space delimited part of the template).

Author: Leroy van Engelen

modules/IOUtils.tla

@@ -21,4 +21,13 @@ IOExec(command) ==
   (*******************************************************************************)
   CHOOSE r \in [exitValue : Int, stdout : STRING, stderr : STRING] : TRUE
 
+IOExecTemplate(commandTemplate, parameters) ==
+  (*************************************************************************)
+  (* Spawns the given printf-style command as a sub-process of TLC.  The   *)
+  (* n-th flag in `commandTemplate' is substituted with the n-th element   *)
+  (* of the sequence `parameters': IOExec("ls %s %s", <<"-lah", "/tmp">>)  *)
+  (* see http://docs.oracle.com/javase/7/docs/api/java/util/Formatter.html *)
+  (*************************************************************************)
+  CHOOSE r \in [exitValue : Int, stdout : STRING, stderr : STRING] : TRUE
+
 ============================================================================

modules/tlc2/overrides/IOUtils.java

@@ -93,6 +93,47 @@ public static Value ioExec(final Value parameter) throws IOException, Interrupte
 		return new RecordValue(EXEC_NAMES, new Value[] {exitCode, stdout, stderr}, false);
 	}
 
+	@TLAPlusOperator(identifier = "IOExecTemplate", module = "IOUtils", minLevel = 1, warn = false)
+	public static Value ioExecTemplate(final Value commandTemplate, final Value parameter) throws IOException, InterruptedException {
+		// 1. Check parameters and covert.
+		if (!(commandTemplate instanceof StringValue)) {
+			throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
+					new String[] { "IOExec", "string", Values.ppr(commandTemplate.toString()) });
+		}
+		if (!(parameter instanceof TupleValue)) {
+			throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
+					new String[] { "IOExec", "sequence", Values.ppr(parameter.toString()) });
+		}
+		final StringValue sv = (StringValue) commandTemplate;
+		final TupleValue tv = (TupleValue) parameter;
+
+		// 2. Build actual command-line by merging command and parameter.
+		// XXX does not support multiple %s inside a template part
+		final String[] command = sv.val.toString().split("\\s+");
+		int j = 0;
+		for (int i = 0; i < command.length; ++i) {
+			if (command[i].contains("%s")) {
+                if (j < tv.elems.length) {
+                    command[i] = String.format(command[i], ((StringValue) tv.elems[j++]).val.toString());
+                } else {
+                    // Too many %s
+                    // XXX throw proper exception
+                    throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
+                            new String[] { "IOExec", "sequence", Values.ppr(parameter.toString()) });
+                }
+			}
+		}
+
+		// 3. Run command-line and receive its output.
+		final Process process = new ProcessBuilder(command)/*.inheritIO()*/.start();
+
+		final StringValue stdout = new StringValue(new String(process.getInputStream().readAllBytes()));
+		final StringValue stderr = new StringValue(new String(process.getErrorStream().readAllBytes()));
+		final IntValue exitCode = IntValue.gen(process.waitFor());
+
+		return new RecordValue(EXEC_NAMES, new Value[] {exitCode, stdout, stderr}, false);
+	}
+
 	private static String convert(IValue v) {
 		if (! (v instanceof StringValue)) {
 			// XXX Proper exception

tests/IOUtilsTests.tla

@@ -10,4 +10,14 @@ ASSUME(LET ret == IOExec(<<"cat",  "/does/not/exist">>) IN /\ ret.exitValue = 1
                                                            /\ ret.stdout = ""
                                                            /\ ret.stderr = "cat: /does/not/exist: No such file or directory\n")
 
+\* Spaces and quotes should be passed directly to the program.
+ASSUME(LET ret == IOExecTemplate("echo '%s'  \"%s\"", <<" foo", "bar ">>) IN /\ ret.exitValue = 0
+                                                                             /\ ret.stdout = "' foo' \"bar \"\n"
+                                                                             /\ ret.stderr = "")
+
+\* Exit values and standard error should be returned properly.
+ASSUME(LET ret == IOExecTemplate("cat /does/not/exist", <<>>) IN /\ ret.exitValue = 1
+                                                                 /\ ret.stdout = ""
+                                                                 /\ ret.stderr = "cat: /does/not/exist: No such file or directory\n")
+
 =============================================================================