From 46039a371f2148466ddacd2867ec01699c5631bc Mon Sep 17 00:00:00 2001
From: Guilherme Silva <239806034+NoneSilva@users.noreply.github.com>
Date: Wed, 14 Oct 2026 13:06:21 +0000
Subject: [PATCH] Make IOUtils exec operators opt-in

Model-checking a specification that EXTENDS IOUtils runs OS commands via IOExec and its variants, on the machine of whoever runs the check, with no opt-in and no notice. Gate runProcess on the system property tlc2.overrides.IOUtils.enableExec, default off; set it to true to allow exec. Opt the test suite in so ant test still exercises the exec operators, and document the flag in IOUtils.tla.

Signed-off-by: Guilherme Silva <239806034+NoneSilva@users.noreply.github.com>
---
 build.xml                           | 1 +
 modules/IOUtils.tla                 | 4 ++++
 modules/tlc2/overrides/IOUtils.java | 3 +++
 tests/IOUtilsUnixTests.tla          | 2 +-
 4 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/build.xml b/build.xml
index b86c5cd..9bc7f82 100644
--- a/build.xml
+++ b/build.xml
@@ -134,6 +134,7 @@
 			<!-- Report execution statistics as azure-pipelien -->
 			<sysproperty key="tlc2.TLC.ide" value="azure-pipeline"/>
 			<sysproperty key="util.ExecutionStatisticsCollector.id" value="01ed03e40ba44f278a934849dd2b1038"/>
+			<sysproperty key="tlc2.overrides.IOUtils.enableExec" value="true"/>
 			
 			<arg value="-fp"/>
 			<arg value="1"/>
diff --git a/modules/IOUtils.tla b/modules/IOUtils.tla
index c8f914c..3de8ad9 100644
--- a/modules/IOUtils.tla
+++ b/modules/IOUtils.tla
@@ -14,6 +14,10 @@
 (* perform side effects when executed by TLC with the Java overrides.      *)
 (***************************************************************************)
 
+\* The external-process operators IOExec, IOEnvExec, IOExecTemplate and
+\* IOEnvExecTemplate are disabled by default. Set the system property
+\* -Dtlc2.overrides.IOUtils.enableExec=true to allow TLC to run OS commands.
+
 LOCAL INSTANCE TLC
 LOCAL INSTANCE Integers
 LOCAL INSTANCE Sequences
diff --git a/modules/tlc2/overrides/IOUtils.java b/modules/tlc2/overrides/IOUtils.java
index 7439b04..b44c598 100644
--- a/modules/tlc2/overrides/IOUtils.java
+++ b/modules/tlc2/overrides/IOUtils.java
@@ -370,6 +370,9 @@ private static Value runProcess(final Map<String, String> env, final String[] co
 	
 	private static Value runProcess(final ProcessBuilder processBuilder)
 			throws IOException, InterruptedException {
+		if (!Boolean.getBoolean("tlc2.overrides.IOUtils.enableExec")) {
+			throw new EvalException(EC.GENERAL, "IOUtils exec is disabled by default. Evaluating an IOUtils exec operator such as IOExec runs an OS command. Set -Dtlc2.overrides.IOUtils.enableExec=true to allow it.");
+		}
 		// 3. Run command-line and receive its output.
 		final Process process = processBuilder/* .inheritIO() */.start();
 
diff --git a/tests/IOUtilsUnixTests.tla b/tests/IOUtilsUnixTests.tla
index d55fb4a..761a901 100644
--- a/tests/IOUtilsUnixTests.tla
+++ b/tests/IOUtilsUnixTests.tla
@@ -100,7 +100,7 @@ ASSUME PrintT("IOUtilsUnixTests!C!d")
 \* Run TLC with some spec depending on CommunityModules and CM on the classpath.
 \* Pass an environment variable to the nested spec.
 ASSUME(LET ret == IOEnvExec([SOME_NESTED_VAR |-> "SOME_VAL", B |-> "23"],
-                            <<"java", "-cp", "modules:build/deps:build/modules:tlc/tla2tools.jar", "tlc2.TLC",
+                            <<"java", "-cp", "modules:build/deps:build/modules:tlc/tla2tools.jar", "-Dtlc2.overrides.IOUtils.enableExec=true", "tlc2.TLC",
                                           "-config", "Counter.cfg", "tests/nested/CounterCM">>)
                                                                  IN /\ PrintT(ret)
                                                                     /\ ret.exitValue = 0