Change IOExec interface

It now passes its arguments almost directly to Java's `ProcessBuilder`.

This avoids problems with passing arguments that include spaces and does
not assume (incorrectly) that there is a shell handling quoting.

Author: Leroy van Engelen

modules/IOUtils.tla

@@ -12,13 +12,13 @@ IODeserialize(absoluteFilename, compressed) == CHOOSE val : TRUE
 
 ----------------------------------------------------------------------------
 
-IOExec(command, parameters) == 
-  (*************************************************************************)
-  (* Spawns the given printf-style command as a sub-process of TLC.  The   *)
-  (* n-th flag in command is substituted for 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 *)
-  (*************************************************************************)
+IOExec(command) ==
+  (*******************************************************************************)
+  (* Spawns the given command as a sub-process of TLC.  The sequence of sequence *)
+  (* of strings `command' signifies the external program file to be invoked and  *)
+  (* its arguments: IOExec(<<"ls", "-lah", "/tmp">>)                             *)
+  (* see https://docs.oracle.com/javase/7/docs/api/java/lang/ProcessBuilder.html *)
+  (*******************************************************************************)
   CHOOSE r \in [exitValue : Int, stdout : STRING, stderr : STRING] : TRUE
 
 ============================================================================

modules/tlc2/overrides/IOUtils.java

@@ -69,33 +69,41 @@ public static final IValue serialize(final IValue value, final StringValue absol
 	}
 
 	@TLAPlusOperator(identifier = "IOExec", module = "IOUtils", minLevel = 1, warn = false)
-	public static Value exec(final Value command, final Value parameter) throws IOException, InterruptedException {
+	public static Value ioExec(final Value parameter) throws IOException, InterruptedException {
 		// 1. Check parameters and covert.
-		if (!(command instanceof StringValue)) {
-			throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
-					new String[] { "IOExec", "string", Values.ppr(command.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) command;
 		final TupleValue tv = (TupleValue) parameter;
-		
-		// 2. Build actual command-line by merging command and parameter.
-		final String cmd = String.format(sv.toUnquotedString(),
-				Arrays.asList(tv.getElems()).stream().map(e -> e.toUnquotedString()).toArray(size -> new Object[size]));
-		
+
+		// 2. Build actual command by converting each parameter element to a string.
+		//	No escaping or quoting is done so the process receives the exact string.
+		final String[] command = Arrays.asList(tv.getElems()).stream()
+				.map(IOUtils::convert)
+				.toArray(size -> new String[size]);
+
 		// 3. Run command-line and receive its output.
-		final Process process = new ProcessBuilder(cmd.split(" "))/*.inheritIO()*/.start();
-		
+		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
+			throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
+					new String[] { "IOExec", "sequence", Values.ppr(v.toString()) });
+		}
+		final StringValue sv = (StringValue) v;
+
+		return sv.val.toString();
+	}
+
 	private static final UniqueString EXITVALUE = UniqueString.uniqueStringOf("exitValue");
 	private static final UniqueString STDOUT = UniqueString.uniqueStringOf("stdout");
 	private static final UniqueString STDERR = UniqueString.uniqueStringOf("stderr");

tests/IOUtilsTests.tla

@@ -1,17 +1,13 @@
 ---------------------------- MODULE IOUtilsTests ----------------------------
 EXTENDS IOUtils, TLC
 
-ASSUME(LET ret == IOExec("echo %s %s", <<"foo", "bar">>) IN /\ ret.exitValue = 0 
-                                                            /\ ret.stdout = "foo bar\n"
-                                                            /\ ret.stderr = "")
-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")
-ASSUME(LET ret == IOExec("echo \"' %s", <<"\"'">>) IN /\ ret.exitValue = 0
-                                                      /\ ret.stdout = "\"' \"'\n"
-                                                      /\ ret.stderr = "")
-ASSUME(LET ret == IOExec("grep %s /dev/null", <<"foo bar">>) IN /\ ret.exitValue = 1
-                                                                /\ ret.stdout = ""
-                                                                /\ ret.stderr = "")
+\* Spaces and quotes should be passed directly to the program.
+ASSUME(LET ret == IOExec(<<"echo", "'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 == IOExec(<<"cat",  "/does/not/exist">>) IN /\ ret.exitValue = 1
+                                                           /\ ret.stdout = ""
+                                                           /\ ret.stderr = "cat: /does/not/exist: No such file or directory\n")
 
 =============================================================================