From a2f3d603f4f661ef9b0aad2ddab2fa7db4f76627 Mon Sep 17 00:00:00 2001 From: Josh Date: Tue, 22 Sep 2026 14:49:02 -0500 Subject: [PATCH 01/21] Add safe mode option, which sets the no_include flag for Kind 2 --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index ae4432c..f798430 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -39,6 +39,8 @@ public class Kind2Api { private List otherOptions; + private Boolean safeMode; + // module smt private SolverOption smtSolver; private QESolverOption qeSmtSolver; @@ -129,6 +131,7 @@ public class Kind2Api { */ public Kind2Api() { otherOptions = new ArrayList<>(); + safeMode = false; smtSolver = null; qeSmtSolver = null; itpSmtSolver = null; @@ -764,10 +767,26 @@ public List getOptions() { options.add("--fake_filepath"); options.add(fakeFilepath); } + if (safeMode != null){ + options.add("--no_include"); + options.add(safeMode.toString()); + } options.addAll(this.otherOptions); return options; } + /** + * If called with true, enables safe mode for this API instance. + * Safe mode enables the following features: disabling the use of include statements, + * automatic use of docker containers for executions of Kind 2 (to be implemented) + *

+ * Default: false + * @param safeMode whether or not to enable safe mode. + */ + public void setSafeMode(boolean safeMode){ + this.safeMode = true; + } + /** * Set the main SMT solver *

From c0fc6ab686ae8c08cf5a14395cca286f7ae8b161 Mon Sep 17 00:00:00 2001 From: Josh Date: Fri, 25 Sep 2026 12:04:07 -0500 Subject: [PATCH 02/21] Implement docker in safe mode --- Dockerfile | 3 + .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 273 +++++++++++++++--- 2 files changed, 233 insertions(+), 43 deletions(-) create mode 100644 Dockerfile diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 0000000..75fa28e --- /dev/null +++ b/Dockerfile @@ -0,0 +1,3 @@ +FROM ubuntu:24.04 + +ENTRYPOINT [] \ No newline at end of file diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 2316c5e..277d843 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -36,6 +36,10 @@ public class Kind2Api { */ public static String KIND2 = "kind2"; private static final long POLL_INTERVAL = 100; + private static final Double SAFE_MODE_CPU_USAGE = 1.0; + private static final String SAFE_MODE_MEMORY_USAGE = "2g"; + private static final String SAFE_MODE_MEMORY_SWAP = SAFE_MODE_MEMORY_USAGE; + private List otherOptions; @@ -286,17 +290,23 @@ public void done() {} * @throws Kind2Exception if {@code uri} is not a local file or Kind 2 fails to run */ public String interpret(URI uri, String main, String json) { - List options = new ArrayList<>(); - options.add(KIND2); - options.addAll(getOptions()); + File interpreterFile = ApiUtil.writeInterpreterFile(json); + Path lustreFile = toLocalPath(uri).toAbsolutePath().normalize(); + + List options = getInterpreterCommand( + interpreterFile, + lustreFile + ); + options.add("--lus_main"); options.add(main); options.add("--enable"); options.add("interpreter"); - options.add("--interpreter_input_file"); - options.add(ApiUtil.writeInterpreterFile(json).getAbsolutePath()); - options.add(toLocalPath(uri).toString()); + ProcessBuilder builder = new ProcessBuilder(options); + + setApiDebug(); + debug.println("Kind 2 command(URI Interpret):\n" + ApiUtil.getQuotedCommand(builder.command())); try { Process process = builder.start(); final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); @@ -344,16 +354,21 @@ private static Path toLocalPath(URI uri) { * @throws Kind2Exception if Kind 2 fails to run */ public String interpret(String program, String main, String json) { - List options = new ArrayList<>(); - options.add(KIND2); - options.addAll(getOptions()); + + File interpreterFile = ApiUtil.writeInterpreterFile(json); + + List options = + getInterpreterCommand(interpreterFile, null); + options.add("--lus_main"); options.add(main); options.add("--enable"); options.add("interpreter"); - options.add("--interpreter_input_file"); - options.add(ApiUtil.writeInterpreterFile(json).getAbsolutePath()); + ProcessBuilder builder = new ProcessBuilder(options); + + setApiDebug(); + debug.println("Kind 2 command(String Interpret):\n " + ApiUtil.getQuotedCommand(builder.command())); try { Process process = builder.start(); process.getOutputStream().write(program.getBytes()); @@ -406,6 +421,7 @@ public void execute(String program, Result result, IProgressMonitor monitor, Res private void callKind2(String program, Result result, IProgressMonitor monitor, ResultListener listener) throws IOException, InterruptedException { ProcessBuilder builder = getKind2ProcessBuilder(); + setApiDebug(); debug.println("Kind 2 command: " + ApiUtil.getQuotedCommand(builder.command())); Process process = null; boolean exceptionThrown = false; @@ -464,15 +480,144 @@ private void callKind2(String program, Result result, IProgressMonitor monitor, } } + private String dockerImage = "kind2-safe:latest"; + private static final String DOCKER_KIND2 = "/usr/local/bin/kind2"; + private static final String DOCKER_INTERPRETER_INPUT = "/tmp/interpreter-input.json"; + private static final String DOCKER_LUSTRE_FILE = "/tmp/program.lus"; + + public void setDockerImage(String dockerImage) { + this.dockerImage = dockerImage; + } private ProcessBuilder getKind2ProcessBuilder() { List options = new ArrayList<>(); - options.add(KIND2); + + if (safeMode) { + Path kind2Path = Paths.get(KIND2).normalize().toAbsolutePath(); + Path z3Path = Paths.get(z3Bin).normalize().toAbsolutePath(); + if (!kind2Path.isAbsolute()) { + throw new Kind2Exception("Kind 2 path must be absolute: " + KIND2); + } + + if (!kind2Path.toFile().isFile()) { + throw new Kind2Exception( + "Kind 2 executable does not exist: " + kind2Path); + } + + options.add("docker"); + options.add("run"); + options.add("--rm"); + options.add("-i"); + + options.add("--cpus"); + options.add(SAFE_MODE_CPU_USAGE.toString()); + + options.add("--memory"); + options.add(SAFE_MODE_MEMORY_USAGE); + + options.add("--memory-swap"); + options.add(SAFE_MODE_MEMORY_SWAP); + + options.add("--network"); + options.add("none"); + + options.add("--mount"); + options.add( + "type=bind,source=" + kind2Path + + ",target=/usr/local/bin/kind2,readonly"); + options.add("--mount"); + options.add( + "type=bind,source=" + z3Path + + ",target=/usr/local/bin/z3,readonly" + ); + options.add(dockerImage); + options.add("/usr/local/bin/kind2"); + } else { + options.add(KIND2); + } + options.addAll(getOptions()); + ProcessBuilder builder = new ProcessBuilder(options); builder.redirectErrorStream(true); return builder; } + + private List getInterpreterCommand(File interpreterFile, Path lustreFile) { + List options = new ArrayList<>(); + + if (!safeMode) { + options.add(KIND2); + options.addAll(getOptions()); + + options.add("--interpreter_input_file"); + options.add(interpreterFile.getAbsolutePath()); + + if (lustreFile != null) { + options.add(lustreFile.toString()); + } + + return options; + } + Path z3Path = Paths.get(z3Bin).normalize().toAbsolutePath(); + Path kind2Path = Paths.get(KIND2).normalize().toAbsolutePath(); + + options.add("docker"); + options.add("run"); + options.add("--rm"); + options.add("-i"); + + options.add("--cpus"); + options.add(SAFE_MODE_CPU_USAGE.toString()); + + options.add("--memory"); + options.add(SAFE_MODE_MEMORY_USAGE); + + options.add("--memory-swap"); + options.add(SAFE_MODE_MEMORY_SWAP); + + options.add("--network"); + options.add("none"); + + options.add("--mount"); + options.add( + "type=bind,source=" + kind2Path + + ",target=/usr/local/bin/kind2,readonly"); + options.add("--mount"); + options.add( + "type=bind,source=" + z3Path + + ",target=/usr/local/bin/z3,readonly" + ); + + options.add("--mount"); + options.add( + "type=bind,source=" + interpreterFile.getAbsolutePath() + + ",target=" + DOCKER_INTERPRETER_INPUT + + ",readonly"); + + if (lustreFile != null) { + options.add("--mount"); + options.add( + "type=bind,source=" + lustreFile.toAbsolutePath() + + ",target=" + DOCKER_LUSTRE_FILE + + ",readonly"); + } + + options.add(dockerImage); + options.add(DOCKER_KIND2); + + options.addAll(getOptions()); + + options.add("--interpreter_input_file"); + options.add(DOCKER_INTERPRETER_INPUT); + + if (lustreFile != null) { + options.add(DOCKER_LUSTRE_FILE); + } + + return options; + } + /** * Sets additional options to pass to Kind 2 executable. * @@ -529,37 +674,79 @@ public List getOptions() { options.add("--smt_short_names"); options.add(smtShortNames.toString()); } - if (bitwuzlaBin != null) { - options.add("--bitwuzla_bin"); - options.add(bitwuzlaBin); - } - if (cvc5Bin != null) { - options.add("--cvc5_bin"); - options.add(cvc5Bin); - } - if (mathsatBin != null) { - options.add("--mathsat_bin"); - options.add(mathsatBin); - } - if (opensmtBin != null) { - options.add("--opensmt_bin"); - options.add(opensmtBin); - } - if (smtinterpolJar != null) { - options.add("--smtinterpol_jar"); - options.add(smtinterpolJar); - } - if (yicesBin != null) { - options.add("--yices_bin"); - options.add(yicesBin); - } - if (yices2Bin != null) { - options.add("--yices2_bin"); - options.add(yices2Bin); - } - if (z3Bin != null) { - options.add("--z3_bin"); - options.add(z3Bin); + if(!safeMode){ + if (bitwuzlaBin != null) { + options.add("--bitwuzla_bin"); + options.add(bitwuzlaBin); + } + if (cvc5Bin != null) { + options.add("--cvc5_bin"); + options.add(cvc5Bin); + } + if (mathsatBin != null) { + options.add("--mathsat_bin"); + options.add(mathsatBin); + } + if (opensmtBin != null) { + options.add("--opensmt_bin"); + options.add(opensmtBin); + } + if (smtinterpolJar != null) { + options.add("--smtinterpol_jar"); + options.add(smtinterpolJar); + } + if (yicesBin != null) { + options.add("--yices_bin"); + options.add(yicesBin); + } + if (yices2Bin != null) { + options.add("--yices2_bin"); + options.add(yices2Bin); + } + if (z3Bin != null) { + options.add("--z3_bin"); + options.add(z3Bin); + } + } else { // safe mode, use fixed container paths + if (bitwuzlaBin != null) { + options.add("--bitwuzla_bin"); + options.add("/usr/local/bin/bitwuzla"); + } + + if (cvc5Bin != null) { + options.add("--cvc5_bin"); + options.add("/usr/local/bin/cvc5"); + } + + if (mathsatBin != null) { + options.add("--mathsat_bin"); + options.add("/usr/local/bin/mathsat"); + } + + if (opensmtBin != null) { + options.add("--opensmt_bin"); + options.add("/usr/local/bin/opensmt"); + } + + if (smtinterpolJar != null) { + options.add("--smtinterpol_jar"); + options.add("/usr/local/lib/smtinterpol.jar"); + } + + if (yicesBin != null) { + options.add("--yices_bin"); + options.add("/usr/local/bin/yices"); + } + + if (yices2Bin != null) { + options.add("--yices2_bin"); + options.add("/usr/local/bin/yices-smt2"); + } + + if (z3Bin != null) { + options.add("--z3_bin"); + options.add("/usr/local/bin/z3"); + } } if (smtTrace != null) { options.add("--smt_trace"); From 5b135dd5f2b5bc414295e0ba5b535bdaa67511af Mon Sep 17 00:00:00 2001 From: Josh Date: Mon, 28 Sep 2026 17:31:54 -0500 Subject: [PATCH 03/21] Add methods to change Docker usage arguments --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 39 +++++++++++++++++-- 1 file changed, 36 insertions(+), 3 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 277d843..c29c959 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -36,9 +36,9 @@ public class Kind2Api { */ public static String KIND2 = "kind2"; private static final long POLL_INTERVAL = 100; - private static final Double SAFE_MODE_CPU_USAGE = 1.0; - private static final String SAFE_MODE_MEMORY_USAGE = "2g"; - private static final String SAFE_MODE_MEMORY_SWAP = SAFE_MODE_MEMORY_USAGE; + private static Double SAFE_MODE_CPU_USAGE = 1.0; + private static String SAFE_MODE_MEMORY_USAGE = "2g"; + private static String SAFE_MODE_MEMORY_SWAP = SAFE_MODE_MEMORY_USAGE; private List otherOptions; @@ -961,6 +961,39 @@ public List getOptions() { options.addAll(this.otherOptions); return options; } + /** + * Sets the amount of CPU usage that the API allows each execution of Kind 2 to use. + * Units are in cores, so a value of 1.5 means "Use up to 1.5 CPU cores" + *

+ * Default: 1.0 + * @param usage Usage (in cores) allowed to executions of Kind 2. + */ + public void setSafeModeCpuUsage(double usage){ + SAFE_MODE_CPU_USAGE = usage; + } + /** + * Sets the amount of physical memory usage that the API allows each execution of Kind 2 to use. + * Units are included in the string, so "1.5g" means "Use up to 1.5 gigabytes of RAM" + * Alternative units: 'g' for gigabytes, 'm' for megabytes, 'k' for kilobytes, 'b' for bytes + *

+ * Default: "2g" + * @param amount of physical memory allowed to executions of Kind 2. + */ + public void setSafeModeMemoryUsage(String amount){ + SAFE_MODE_MEMORY_USAGE = amount; + } + /** + * Sets the cumulative amount of swap space and physical memory usage that the + * API allows each execution of Kind 2 to use. + * Units are included in the string, so "1.5g" means "Use up to 1.5 gigabytes of RAM" + * Alternative units: 'g' for gigabytes, 'm' for megabytes, 'k' for kilobytes, 'b' for bytes + *

+ * Default: "2g" + * @param amount of swap + physical memory allowed to executions of Kind 2. + */ + public void setSafeModeSwapUsage(String amount){ + SAFE_MODE_MEMORY_SWAP = amount; + } /** * If called with true, enables safe mode for this API instance. From 4d4ad884c5abae588387e77771fccb3d48a8a859 Mon Sep 17 00:00:00 2001 From: Josh Date: Tue, 29 Sep 2026 01:26:08 -0500 Subject: [PATCH 04/21] Add checks on usage values and improve javadoc --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 53 ++++++++++++++----- 1 file changed, 39 insertions(+), 14 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index c29c959..66002a8 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -36,9 +36,9 @@ public class Kind2Api { */ public static String KIND2 = "kind2"; private static final long POLL_INTERVAL = 100; - private static Double SAFE_MODE_CPU_USAGE = 1.0; - private static String SAFE_MODE_MEMORY_USAGE = "2g"; - private static String SAFE_MODE_MEMORY_SWAP = SAFE_MODE_MEMORY_USAGE; + private static Double safeModeCpuUsage = 1.0; + private static String safeModeMemoryUsage = "2g"; + private static String safeModeSwapUsage = safeModeMemoryUsage; private List otherOptions; @@ -509,13 +509,13 @@ private ProcessBuilder getKind2ProcessBuilder() { options.add("-i"); options.add("--cpus"); - options.add(SAFE_MODE_CPU_USAGE.toString()); + options.add(safeModeCpuUsage.toString()); options.add("--memory"); - options.add(SAFE_MODE_MEMORY_USAGE); + options.add(safeModeMemoryUsage); options.add("--memory-swap"); - options.add(SAFE_MODE_MEMORY_SWAP); + options.add(safeModeSwapUsage); options.add("--network"); options.add("none"); @@ -568,13 +568,13 @@ private List getInterpreterCommand(File interpreterFile, Path lustreFile options.add("-i"); options.add("--cpus"); - options.add(SAFE_MODE_CPU_USAGE.toString()); + options.add(safeModeCpuUsage.toString()); options.add("--memory"); - options.add(SAFE_MODE_MEMORY_USAGE); + options.add(safeModeMemoryUsage); options.add("--memory-swap"); - options.add(SAFE_MODE_MEMORY_SWAP); + options.add(safeModeSwapUsage); options.add("--network"); options.add("none"); @@ -961,6 +961,7 @@ public List getOptions() { options.addAll(this.otherOptions); return options; } + /** * Sets the amount of CPU usage that the API allows each execution of Kind 2 to use. * Units are in cores, so a value of 1.5 means "Use up to 1.5 CPU cores" @@ -969,30 +970,54 @@ public List getOptions() { * @param usage Usage (in cores) allowed to executions of Kind 2. */ public void setSafeModeCpuUsage(double usage){ - SAFE_MODE_CPU_USAGE = usage; + if(usage <= 0.0) throw new IllegalArgumentException("CPU usage was set to " + usage + + ", but a positive value is expected (e.g. 1.5)"); + safeModeCpuUsage = usage; + } + + private void validateMemoryValue(String value, String setting){ + if (value == null || value.length() < 2) { + throw new IllegalArgumentException(setting + " was set to " + value + + ", but a positive integer value with a unit was expected (e.g. 1g)"); + } + String unit = String.valueOf(value.charAt(value.length()-1)).toLowerCase(); + String num = value.substring(0, value.length()-1); + String allowedUnits = "gmkb"; + if (!allowedUnits.contains(unit)){ + throw new IllegalArgumentException(setting + " was set to " + value + + ", but a unit was expected (e.g. 1g)"); + } + try { + if (Integer.parseInt(num) <= 0) throw new NumberFormatException(); + } catch (NumberFormatException e) { + throw new IllegalArgumentException(setting + " was set to " + value + + ", but a positive integer value with a unit was expected (e.g. 1g)"); + } } /** * Sets the amount of physical memory usage that the API allows each execution of Kind 2 to use. - * Units are included in the string, so "1.5g" means "Use up to 1.5 gigabytes of RAM" + * Units are included in the string, so "1g" means "Use up to 1 gigabyte of RAM" * Alternative units: 'g' for gigabytes, 'm' for megabytes, 'k' for kilobytes, 'b' for bytes *

* Default: "2g" * @param amount of physical memory allowed to executions of Kind 2. */ public void setSafeModeMemoryUsage(String amount){ - SAFE_MODE_MEMORY_USAGE = amount; + validateMemoryValue(amount, "Memory usage"); + safeModeMemoryUsage = amount; } /** * Sets the cumulative amount of swap space and physical memory usage that the * API allows each execution of Kind 2 to use. - * Units are included in the string, so "1.5g" means "Use up to 1.5 gigabytes of RAM" + * Units are included in the string, "1g" means "Use up to 1 gigabyte of combined physical memory and swap" * Alternative units: 'g' for gigabytes, 'm' for megabytes, 'k' for kilobytes, 'b' for bytes *

* Default: "2g" * @param amount of swap + physical memory allowed to executions of Kind 2. */ public void setSafeModeSwapUsage(String amount){ - SAFE_MODE_MEMORY_SWAP = amount; + validateMemoryValue(amount, "Swap usage"); + safeModeSwapUsage = amount; } /** From 6342b10609a70eefd9019dd1dc3bee8c260def07 Mon Sep 17 00:00:00 2001 From: Josh Date: Tue, 29 Sep 2026 01:35:02 -0500 Subject: [PATCH 05/21] Remove debug prints --- src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 66002a8..2fe5b74 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -305,7 +305,6 @@ public String interpret(URI uri, String main, String json) { ProcessBuilder builder = new ProcessBuilder(options); - setApiDebug(); debug.println("Kind 2 command(URI Interpret):\n" + ApiUtil.getQuotedCommand(builder.command())); try { Process process = builder.start(); @@ -367,7 +366,6 @@ public String interpret(String program, String main, String json) { ProcessBuilder builder = new ProcessBuilder(options); - setApiDebug(); debug.println("Kind 2 command(String Interpret):\n " + ApiUtil.getQuotedCommand(builder.command())); try { Process process = builder.start(); @@ -421,7 +419,6 @@ public void execute(String program, Result result, IProgressMonitor monitor, Res private void callKind2(String program, Result result, IProgressMonitor monitor, ResultListener listener) throws IOException, InterruptedException { ProcessBuilder builder = getKind2ProcessBuilder(); - setApiDebug(); debug.println("Kind 2 command: " + ApiUtil.getQuotedCommand(builder.command())); Process process = null; boolean exceptionThrown = false; From 534defae0d02ac2f9e109837fb29cd11b5b7f6ac Mon Sep 17 00:00:00 2001 From: Josh Date: Tue, 29 Sep 2026 12:34:57 -0500 Subject: [PATCH 06/21] Make usage variables fields --- .../java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 2fe5b74..b320794 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -36,9 +36,12 @@ public class Kind2Api { */ public static String KIND2 = "kind2"; private static final long POLL_INTERVAL = 100; - private static Double safeModeCpuUsage = 1.0; - private static String safeModeMemoryUsage = "2g"; - private static String safeModeSwapUsage = safeModeMemoryUsage; + private static final Double DEFAULT_SAFE_MODE_CPU_USAGE = 1.0; + private static final String DEFAULT_SAFE_MODE_MEMORY_USAGE = "2g"; + private static final String DEFAULT_SAFE_MODE_SWAP_USAGE = DEFAULT_SAFE_MODE_MEMORY_USAGE; + private Double safeModeCpuUsage; + private String safeModeMemoryUsage; + private String safeModeSwapUsage; private List otherOptions; @@ -201,6 +204,9 @@ public Kind2Api() { lusMain = null; lusMainType = null; lusMainConst = null; + safeModeCpuUsage = DEFAULT_SAFE_MODE_CPU_USAGE; + safeModeMemoryUsage = DEFAULT_SAFE_MODE_MEMORY_USAGE; + safeModeSwapUsage = DEFAULT_SAFE_MODE_SWAP_USAGE; } DebugLogger debug = new DebugLogger(); From c1b4d79d682dfeb7c81e1f334c06707a4c467b93 Mon Sep 17 00:00:00 2001 From: Josh Date: Tue, 29 Sep 2026 14:25:27 -0500 Subject: [PATCH 07/21] Up the limit of swap usage when memory setting exceeds it --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index b320794..a63c2b1 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -997,16 +997,41 @@ private void validateMemoryValue(String value, String setting){ ", but a positive integer value with a unit was expected (e.g. 1g)"); } } + /** + * This function should onlt be called after v has been validated by validateMemoryValue(). + * @param v the source string + * @return the number of bytes that v represents + */ + private long memoryValueToBytes(String v){ + + long value = Long.parseLong(v.substring(0, v.length()-1)); + char unit = v.charAt(v.toLowerCase().length()-1); + long modifier; + switch(unit){ + case 'b': modifier = 1L; break; + case 'k': modifier = 1000L; break; + case 'm': modifier = 1000L^2; break; + case 'g': modifier = 1000L^3; break; + default: /* Should be impossible given validateMemoryValue() was called on v beforehand */ throw new IllegalArgumentException(v + " is not a valid memory value"); + } + this.setApiDebug(); + apiDebug(v + "=" + value*modifier + " bytes"); + return value*modifier; + } /** * Sets the amount of physical memory usage that the API allows each execution of Kind 2 to use. * Units are included in the string, so "1g" means "Use up to 1 gigabyte of RAM" * Alternative units: 'g' for gigabytes, 'm' for megabytes, 'k' for kilobytes, 'b' for bytes + * If the value set here exceeds the safe mode swap usage, the swap usage is increased to the amount provided. *

* Default: "2g" * @param amount of physical memory allowed to executions of Kind 2. */ public void setSafeModeMemoryUsage(String amount){ validateMemoryValue(amount, "Memory usage"); + if (memoryValueToBytes(amount) > memoryValueToBytes(safeModeSwapUsage)){ + safeModeSwapUsage = amount; + } safeModeMemoryUsage = amount; } /** From c6771f7aaa95813661f7ea7027c77932419fd8e8 Mon Sep 17 00:00:00 2001 From: Josh Date: Tue, 29 Sep 2026 14:44:10 -0500 Subject: [PATCH 08/21] Fix errors in calculation, cleanup --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index a63c2b1..1775b0d 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -987,14 +987,12 @@ private void validateMemoryValue(String value, String setting){ String num = value.substring(0, value.length()-1); String allowedUnits = "gmkb"; if (!allowedUnits.contains(unit)){ - throw new IllegalArgumentException(setting + " was set to " + value + - ", but a unit was expected (e.g. 1g)"); + throw new IllegalArgumentException(setting + " was set to " + value + + ", but a unit was expected (e.g. 1g)"); } - try { - if (Integer.parseInt(num) <= 0) throw new NumberFormatException(); - } catch (NumberFormatException e) { + if (Integer.parseInt(num) <= 0){ throw new IllegalArgumentException(setting + " was set to " + value + - ", but a positive integer value with a unit was expected (e.g. 1g)"); + ", but a positive integer value with a unit was expected (e.g. 1g)"); } } /** @@ -1010,12 +1008,10 @@ private long memoryValueToBytes(String v){ switch(unit){ case 'b': modifier = 1L; break; case 'k': modifier = 1000L; break; - case 'm': modifier = 1000L^2; break; - case 'g': modifier = 1000L^3; break; + case 'm': modifier = 1000L * 1000L; break; + case 'g': modifier = 1000L * 1000L * 1000L; break; default: /* Should be impossible given validateMemoryValue() was called on v beforehand */ throw new IllegalArgumentException(v + " is not a valid memory value"); } - this.setApiDebug(); - apiDebug(v + "=" + value*modifier + " bytes"); return value*modifier; } /** From d8a25d63ac86c84c9e2af5f2f7d327f3a2bbf445 Mon Sep 17 00:00:00 2001 From: Josh Date: Tue, 29 Sep 2026 15:16:59 -0500 Subject: [PATCH 09/21] Include all available solvers in Docker call --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 59 +++++++++---------- 1 file changed, 27 insertions(+), 32 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 1775b0d..2553070 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -491,21 +491,31 @@ private void callKind2(String program, Result result, IProgressMonitor monitor, public void setDockerImage(String dockerImage) { this.dockerImage = dockerImage; } + private void mountIfPresent(List options, String binPath){ + if (binPath != null) { + Path path = Paths.get(binPath).normalize().toAbsolutePath(); + String filename = path.getFileName().toString(); + options.add("--mount"); + options.add( + "type=bind,source=" + path + + ",target=/usr/local/bin/"+ filename + ",readonly" + ); + } + } + private void mountSolversToDocker(List options){ + mountIfPresent(options, bitwuzlaBin); + mountIfPresent(options, cvc5Bin); + mountIfPresent(options, mathsatBin); + mountIfPresent(options, opensmtBin); + mountIfPresent(options, smtinterpolJar); + mountIfPresent(options, yicesBin); + mountIfPresent(options, yices2Bin); + mountIfPresent(options, z3Bin); + } private ProcessBuilder getKind2ProcessBuilder() { List options = new ArrayList<>(); if (safeMode) { - Path kind2Path = Paths.get(KIND2).normalize().toAbsolutePath(); - Path z3Path = Paths.get(z3Bin).normalize().toAbsolutePath(); - if (!kind2Path.isAbsolute()) { - throw new Kind2Exception("Kind 2 path must be absolute: " + KIND2); - } - - if (!kind2Path.toFile().isFile()) { - throw new Kind2Exception( - "Kind 2 executable does not exist: " + kind2Path); - } - options.add("docker"); options.add("run"); options.add("--rm"); @@ -522,16 +532,10 @@ private ProcessBuilder getKind2ProcessBuilder() { options.add("--network"); options.add("none"); - - options.add("--mount"); - options.add( - "type=bind,source=" + kind2Path - + ",target=/usr/local/bin/kind2,readonly"); - options.add("--mount"); - options.add( - "type=bind,source=" + z3Path + - ",target=/usr/local/bin/z3,readonly" - ); + mountIfPresent(options, KIND2); + + mountSolversToDocker(options); + options.add(dockerImage); options.add("/usr/local/bin/kind2"); } else { @@ -562,8 +566,6 @@ private List getInterpreterCommand(File interpreterFile, Path lustreFile return options; } - Path z3Path = Paths.get(z3Bin).normalize().toAbsolutePath(); - Path kind2Path = Paths.get(KIND2).normalize().toAbsolutePath(); options.add("docker"); options.add("run"); @@ -582,15 +584,8 @@ private List getInterpreterCommand(File interpreterFile, Path lustreFile options.add("--network"); options.add("none"); - options.add("--mount"); - options.add( - "type=bind,source=" + kind2Path - + ",target=/usr/local/bin/kind2,readonly"); - options.add("--mount"); - options.add( - "type=bind,source=" + z3Path + - ",target=/usr/local/bin/z3,readonly" - ); + mountIfPresent(options, KIND2); + mountSolversToDocker(options); options.add("--mount"); options.add( From b68cda1c85f24b3eece478062bfd8bbd2f92b7ba Mon Sep 17 00:00:00 2001 From: Josh Date: Tue, 29 Sep 2026 15:31:35 -0500 Subject: [PATCH 10/21] Quote user-provided paths in docker calls --- src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 2553070..66abf0d 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -497,8 +497,8 @@ private void mountIfPresent(List options, String binPath){ String filename = path.getFileName().toString(); options.add("--mount"); options.add( - "type=bind,source=" + path - + ",target=/usr/local/bin/"+ filename + ",readonly" + "type=bind,source=\"" + path + + "\",target=/usr/local/bin/"+ filename + ",readonly" ); } } From bf361226c11ea0f655b8df37ebe851fcdb517e13 Mon Sep 17 00:00:00 2001 From: Josh Date: Thu, 1 Oct 2026 12:02:39 -0500 Subject: [PATCH 11/21] Implement safe mode path validation and update Docker mount logic --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 192 ++++++++++-------- 1 file changed, 108 insertions(+), 84 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 66abf0d..56b41f0 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -12,6 +12,7 @@ import java.io.InputStreamReader; import java.net.URI; import java.net.URISyntaxException; +import java.nio.file.InvalidPathException; import java.nio.file.Path; import java.nio.file.Paths; import java.util.ArrayList; @@ -491,9 +492,36 @@ private void callKind2(String program, Result result, IProgressMonitor monitor, public void setDockerImage(String dockerImage) { this.dockerImage = dockerImage; } - private void mountIfPresent(List options, String binPath){ + private Path requireSafeModePath(String settingName, String configuredPath) { + if (configuredPath == null) { + return null; + } + + final Path path; + try { + path = Paths.get(configuredPath).normalize(); + } catch (InvalidPathException e) { + throw new Kind2Exception(settingName + " is not a valid path: " + configuredPath, e); + } + + if (!path.isAbsolute()) { + throw new Kind2Exception(settingName + " must be set to an absolute path in safe mode: " + configuredPath); + } + + if (!path.toFile().exists()) { + throw new Kind2Exception(settingName + " does not exist: " + path); + } + + if (!path.toFile().isFile()) { + throw new Kind2Exception(settingName + " is not a file: " + path); + } + + return path; + } + + private void mountIfPresent(List options, String settingName, String binPath){ if (binPath != null) { - Path path = Paths.get(binPath).normalize().toAbsolutePath(); + Path path = requireSafeModePath(settingName, binPath); String filename = path.getFileName().toString(); options.add("--mount"); options.add( @@ -503,19 +531,19 @@ private void mountIfPresent(List options, String binPath){ } } private void mountSolversToDocker(List options){ - mountIfPresent(options, bitwuzlaBin); - mountIfPresent(options, cvc5Bin); - mountIfPresent(options, mathsatBin); - mountIfPresent(options, opensmtBin); - mountIfPresent(options, smtinterpolJar); - mountIfPresent(options, yicesBin); - mountIfPresent(options, yices2Bin); - mountIfPresent(options, z3Bin); + mountIfPresent(options, "bitwuzlaBin", bitwuzlaBin); + mountIfPresent(options, "cvc5Bin", cvc5Bin); + mountIfPresent(options, "mathsatBin", mathsatBin); + mountIfPresent(options, "opensmtBin", opensmtBin); + mountIfPresent(options, "smtinterpolJar", smtinterpolJar); + mountIfPresent(options, "yicesBin", yicesBin); + mountIfPresent(options, "yices2Bin", yices2Bin); + mountIfPresent(options, "z3Bin", z3Bin); } private ProcessBuilder getKind2ProcessBuilder() { List options = new ArrayList<>(); - if (safeMode) { + if (safeMode != null && safeMode) { options.add("docker"); options.add("run"); options.add("--rm"); @@ -532,7 +560,7 @@ private ProcessBuilder getKind2ProcessBuilder() { options.add("--network"); options.add("none"); - mountIfPresent(options, KIND2); + mountIfPresent(options, "KIND2", KIND2); mountSolversToDocker(options); @@ -553,67 +581,67 @@ private ProcessBuilder getKind2ProcessBuilder() { private List getInterpreterCommand(File interpreterFile, Path lustreFile) { List options = new ArrayList<>(); - if (!safeMode) { - options.add(KIND2); - options.addAll(getOptions()); + if (safeMode != null && safeMode) { + options.add("docker"); + options.add("run"); + options.add("--rm"); + options.add("-i"); - options.add("--interpreter_input_file"); - options.add(interpreterFile.getAbsolutePath()); + options.add("--cpus"); + options.add(safeModeCpuUsage.toString()); - if (lustreFile != null) { - options.add(lustreFile.toString()); - } + options.add("--memory"); + options.add(safeModeMemoryUsage); - return options; - } + options.add("--memory-swap"); + options.add(safeModeSwapUsage); - options.add("docker"); - options.add("run"); - options.add("--rm"); - options.add("-i"); + options.add("--network"); + options.add("none"); - options.add("--cpus"); - options.add(safeModeCpuUsage.toString()); + mountIfPresent(options, "KIND2", KIND2); + mountSolversToDocker(options); + + options.add("--mount"); + options.add( + "type=bind,source=" + interpreterFile.getAbsolutePath() + + ",target=" + DOCKER_INTERPRETER_INPUT + + ",readonly"); - options.add("--memory"); - options.add(safeModeMemoryUsage); + if (lustreFile != null) { + options.add("--mount"); + options.add( + "type=bind,source=" + lustreFile.toAbsolutePath() + + ",target=" + DOCKER_LUSTRE_FILE + + ",readonly"); + } - options.add("--memory-swap"); - options.add(safeModeSwapUsage); + options.add(dockerImage); + options.add(DOCKER_KIND2); - options.add("--network"); - options.add("none"); + options.addAll(getOptions()); - mountIfPresent(options, KIND2); - mountSolversToDocker(options); + options.add("--interpreter_input_file"); + options.add(DOCKER_INTERPRETER_INPUT); - options.add("--mount"); - options.add( - "type=bind,source=" + interpreterFile.getAbsolutePath() - + ",target=" + DOCKER_INTERPRETER_INPUT - + ",readonly"); + if (lustreFile != null) { + options.add(DOCKER_LUSTRE_FILE); + } - if (lustreFile != null) { - options.add("--mount"); - options.add( - "type=bind,source=" + lustreFile.toAbsolutePath() - + ",target=" + DOCKER_LUSTRE_FILE - + ",readonly"); + return options; } - options.add(dockerImage); - options.add(DOCKER_KIND2); - - options.addAll(getOptions()); + options.add(KIND2); + options.addAll(getOptions()); - options.add("--interpreter_input_file"); - options.add(DOCKER_INTERPRETER_INPUT); + options.add("--interpreter_input_file"); + options.add(interpreterFile.getAbsolutePath()); - if (lustreFile != null) { - options.add(DOCKER_LUSTRE_FILE); - } + if (lustreFile != null) { + options.add(lustreFile.toString()); + } - return options; + return options; } /** @@ -672,79 +700,73 @@ public List getOptions() { options.add("--smt_short_names"); options.add(smtShortNames.toString()); } - if(!safeMode){ - if (bitwuzlaBin != null) { + if(safeMode != null && safeMode){ + if (bitwuzlaBin != null) { options.add("--bitwuzla_bin"); - options.add(bitwuzlaBin); + options.add("/usr/local/bin/bitwuzla"); } if (cvc5Bin != null) { options.add("--cvc5_bin"); - options.add(cvc5Bin); + options.add("/usr/local/bin/cvc5"); } if (mathsatBin != null) { options.add("--mathsat_bin"); - options.add(mathsatBin); + options.add("/usr/local/bin/mathsat"); } if (opensmtBin != null) { options.add("--opensmt_bin"); - options.add(opensmtBin); + options.add("/usr/local/bin/opensmt"); } if (smtinterpolJar != null) { options.add("--smtinterpol_jar"); - options.add(smtinterpolJar); + options.add("/usr/local/lib/smtinterpol.jar"); } if (yicesBin != null) { options.add("--yices_bin"); - options.add(yicesBin); + options.add("/usr/local/bin/yices"); } if (yices2Bin != null) { options.add("--yices2_bin"); - options.add(yices2Bin); + options.add("/usr/local/bin/yices-smt2"); } if (z3Bin != null) { options.add("--z3_bin"); - options.add(z3Bin); + options.add("/usr/local/bin/z3"); } } else { // safe mode, use fixed container paths - if (bitwuzlaBin != null) { + if (bitwuzlaBin != null) { options.add("--bitwuzla_bin"); - options.add("/usr/local/bin/bitwuzla"); + options.add(bitwuzlaBin); } - if (cvc5Bin != null) { options.add("--cvc5_bin"); - options.add("/usr/local/bin/cvc5"); + options.add(cvc5Bin); } - if (mathsatBin != null) { options.add("--mathsat_bin"); - options.add("/usr/local/bin/mathsat"); + options.add(mathsatBin); } - if (opensmtBin != null) { options.add("--opensmt_bin"); - options.add("/usr/local/bin/opensmt"); + options.add(opensmtBin); } - if (smtinterpolJar != null) { options.add("--smtinterpol_jar"); - options.add("/usr/local/lib/smtinterpol.jar"); + options.add(smtinterpolJar); } - if (yicesBin != null) { options.add("--yices_bin"); - options.add("/usr/local/bin/yices"); + options.add(yicesBin); } - if (yices2Bin != null) { options.add("--yices2_bin"); - options.add("/usr/local/bin/yices-smt2"); + options.add(yices2Bin); } - if (z3Bin != null) { options.add("--z3_bin"); - options.add("/usr/local/bin/z3"); + options.add(z3Bin); } + } if (smtTrace != null) { options.add("--smt_trace"); @@ -1042,7 +1064,9 @@ public void setSafeModeSwapUsage(String amount){ /** * If called with true, enables safe mode for this API instance. * Safe mode enables the following features: disabling the use of include statements, - * automatic use of docker containers for executions of Kind 2 (to be implemented) + * automatic use of docker containers for executions of Kind 2. + * In safe mode, the location of the Kind 2 executable and solvers will not be searched + * for on the PATH variable: they must be set via the API *

* Default: false * @param safeMode whether or not to enable safe mode. From 920aae8a7869ebae89da96d0b990087e1c7c128b Mon Sep 17 00:00:00 2001 From: Josh Date: Thu, 1 Oct 2026 17:10:56 -0500 Subject: [PATCH 12/21] Handle paths with spaces --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 56b41f0..4f7c4b1 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -426,6 +426,7 @@ public void execute(String program, Result result, IProgressMonitor monitor, Res private void callKind2(String program, Result result, IProgressMonitor monitor, ResultListener listener) throws IOException, InterruptedException { ProcessBuilder builder = getKind2ProcessBuilder(); + setApiDebug(); debug.println("Kind 2 command: " + ApiUtil.getQuotedCommand(builder.command())); Process process = null; boolean exceptionThrown = false; @@ -521,14 +522,15 @@ private Path requireSafeModePath(String settingName, String configuredPath) { private void mountIfPresent(List options, String settingName, String binPath){ if (binPath != null) { - Path path = requireSafeModePath(settingName, binPath); - String filename = path.getFileName().toString(); - options.add("--mount"); - options.add( - "type=bind,source=\"" + path - + "\",target=/usr/local/bin/"+ filename + ",readonly" - ); - } + Path path = requireSafeModePath(settingName, binPath); + String filename = path.getFileName().toString(); + String dockerSourcePath = path.toString().replace(" ", "\\\\ "); + options.add("--mount"); + options.add( + "type=bind,source=" + dockerSourcePath + + ",target=/usr/local/bin/"+ filename + ",readonly" + ); + } } private void mountSolversToDocker(List options){ mountIfPresent(options, "bitwuzlaBin", bitwuzlaBin); From c2fc074144ff135afa7a1dd7c6318217bc88a4ba Mon Sep 17 00:00:00 2001 From: Josh Date: Thu, 1 Oct 2026 17:38:47 -0500 Subject: [PATCH 13/21] Fix unit mismatch in memory calculation --- src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 4f7c4b1..384a155 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -1026,9 +1026,9 @@ private long memoryValueToBytes(String v){ long modifier; switch(unit){ case 'b': modifier = 1L; break; - case 'k': modifier = 1000L; break; - case 'm': modifier = 1000L * 1000L; break; - case 'g': modifier = 1000L * 1000L * 1000L; break; + case 'k': modifier = 1024L; break; + case 'm': modifier = 1024L * 1024L; break; + case 'g': modifier = 1024L * 1024L * 1024L; break; default: /* Should be impossible given validateMemoryValue() was called on v beforehand */ throw new IllegalArgumentException(v + " is not a valid memory value"); } return value*modifier; From 2a1ca8bc8700f54947484354c5f38ede9cf83617 Mon Sep 17 00:00:00 2001 From: Josh Date: Thu, 1 Oct 2026 17:39:00 -0500 Subject: [PATCH 14/21] Remove debug call --- src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 384a155..0ada107 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -426,7 +426,6 @@ public void execute(String program, Result result, IProgressMonitor monitor, Res private void callKind2(String program, Result result, IProgressMonitor monitor, ResultListener listener) throws IOException, InterruptedException { ProcessBuilder builder = getKind2ProcessBuilder(); - setApiDebug(); debug.println("Kind 2 command: " + ApiUtil.getQuotedCommand(builder.command())); Process process = null; boolean exceptionThrown = false; From 42665abd8c0ecad98e2ba51131550b6b71f524ee Mon Sep 17 00:00:00 2001 From: Josh Date: Thu, 1 Oct 2026 17:45:36 -0500 Subject: [PATCH 15/21] Normalize paths inside docker container --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 49 +++++++++++-------- 1 file changed, 28 insertions(+), 21 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 0ada107..61e899d 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -486,6 +486,14 @@ private void callKind2(String program, Result result, IProgressMonitor monitor, private String dockerImage = "kind2-safe:latest"; private static final String DOCKER_KIND2 = "/usr/local/bin/kind2"; + private static final String DOCKER_BITWUZLA_BIN = "/usr/local/bin/bitwuzla"; + private static final String DOCKER_CVC5_BIN = "/usr/local/bin/cvc5"; + private static final String DOCKER_MATHSAT_BIN = "/usr/local/bin/mathsat"; + private static final String DOCKER_OPENSMT_BIN = "/usr/local/bin/opensmt"; + private static final String DOCKER_SMTINTERPOL_JAR = "/usr/local/lib/smtinterpol.jar"; + private static final String DOCKER_YICES_BIN = "/usr/local/bin/yices"; + private static final String DOCKER_YICES2_BIN = "/usr/local/bin/yices-smt2"; + private static final String DOCKER_Z3_BIN = "/usr/local/bin/z3"; private static final String DOCKER_INTERPRETER_INPUT = "/tmp/interpreter-input.json"; private static final String DOCKER_LUSTRE_FILE = "/tmp/program.lus"; @@ -519,27 +527,26 @@ private Path requireSafeModePath(String settingName, String configuredPath) { return path; } - private void mountIfPresent(List options, String settingName, String binPath){ + private void mountIfPresent(List options, String settingName, String binPath, String dockerTargetPath){ if (binPath != null) { Path path = requireSafeModePath(settingName, binPath); - String filename = path.getFileName().toString(); String dockerSourcePath = path.toString().replace(" ", "\\\\ "); options.add("--mount"); options.add( "type=bind,source=" + dockerSourcePath - + ",target=/usr/local/bin/"+ filename + ",readonly" + + ",target=" + dockerTargetPath + ",readonly" ); } } private void mountSolversToDocker(List options){ - mountIfPresent(options, "bitwuzlaBin", bitwuzlaBin); - mountIfPresent(options, "cvc5Bin", cvc5Bin); - mountIfPresent(options, "mathsatBin", mathsatBin); - mountIfPresent(options, "opensmtBin", opensmtBin); - mountIfPresent(options, "smtinterpolJar", smtinterpolJar); - mountIfPresent(options, "yicesBin", yicesBin); - mountIfPresent(options, "yices2Bin", yices2Bin); - mountIfPresent(options, "z3Bin", z3Bin); + mountIfPresent(options, "bitwuzlaBin", bitwuzlaBin, DOCKER_BITWUZLA_BIN); + mountIfPresent(options, "cvc5Bin", cvc5Bin, DOCKER_CVC5_BIN); + mountIfPresent(options, "mathsatBin", mathsatBin, DOCKER_MATHSAT_BIN); + mountIfPresent(options, "opensmtBin", opensmtBin, DOCKER_OPENSMT_BIN); + mountIfPresent(options, "smtinterpolJar", smtinterpolJar, DOCKER_SMTINTERPOL_JAR); + mountIfPresent(options, "yicesBin", yicesBin, DOCKER_YICES_BIN); + mountIfPresent(options, "yices2Bin", yices2Bin, DOCKER_YICES2_BIN); + mountIfPresent(options, "z3Bin", z3Bin, DOCKER_Z3_BIN); } private ProcessBuilder getKind2ProcessBuilder() { List options = new ArrayList<>(); @@ -561,7 +568,7 @@ private ProcessBuilder getKind2ProcessBuilder() { options.add("--network"); options.add("none"); - mountIfPresent(options, "KIND2", KIND2); + mountIfPresent(options, "KIND2", KIND2, DOCKER_KIND2); mountSolversToDocker(options); @@ -600,7 +607,7 @@ private List getInterpreterCommand(File interpreterFile, Path lustreFile options.add("--network"); options.add("none"); - mountIfPresent(options, "KIND2", KIND2); + mountIfPresent(options, "KIND2", KIND2, DOCKER_KIND2); mountSolversToDocker(options); options.add("--mount"); @@ -704,35 +711,35 @@ public List getOptions() { if(safeMode != null && safeMode){ if (bitwuzlaBin != null) { options.add("--bitwuzla_bin"); - options.add("/usr/local/bin/bitwuzla"); + options.add(DOCKER_BITWUZLA_BIN); } if (cvc5Bin != null) { options.add("--cvc5_bin"); - options.add("/usr/local/bin/cvc5"); + options.add(DOCKER_CVC5_BIN); } if (mathsatBin != null) { options.add("--mathsat_bin"); - options.add("/usr/local/bin/mathsat"); + options.add(DOCKER_MATHSAT_BIN); } if (opensmtBin != null) { options.add("--opensmt_bin"); - options.add("/usr/local/bin/opensmt"); + options.add(DOCKER_OPENSMT_BIN); } if (smtinterpolJar != null) { options.add("--smtinterpol_jar"); - options.add("/usr/local/lib/smtinterpol.jar"); + options.add(DOCKER_SMTINTERPOL_JAR); } if (yicesBin != null) { options.add("--yices_bin"); - options.add("/usr/local/bin/yices"); + options.add(DOCKER_YICES_BIN); } if (yices2Bin != null) { options.add("--yices2_bin"); - options.add("/usr/local/bin/yices-smt2"); + options.add(DOCKER_YICES2_BIN); } if (z3Bin != null) { options.add("--z3_bin"); - options.add("/usr/local/bin/z3"); + options.add(DOCKER_Z3_BIN); } } else { // safe mode, use fixed container paths if (bitwuzlaBin != null) { From bb3fd495c572afe645c2698ecd0ee93d324c21f1 Mon Sep 17 00:00:00 2001 From: Josh Date: Thu, 1 Oct 2026 17:54:54 -0500 Subject: [PATCH 16/21] Allow commas in file paths of solvers and Kind 2 --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 24 +++++++++---------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 61e899d..726c295 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -527,15 +527,19 @@ private Path requireSafeModePath(String settingName, String configuredPath) { return path; } + private static String csvQuote(String text) { + return "\"" + text.replace("\"", "\"\"") + "\""; + } + + private static String bindMountSpec(Path sourcePath, String dockerTargetPath) { + return "type=bind," + csvQuote("source=" + sourcePath) + ",target=" + dockerTargetPath + ",readonly"; + } + private void mountIfPresent(List options, String settingName, String binPath, String dockerTargetPath){ if (binPath != null) { Path path = requireSafeModePath(settingName, binPath); - String dockerSourcePath = path.toString().replace(" ", "\\\\ "); options.add("--mount"); - options.add( - "type=bind,source=" + dockerSourcePath - + ",target=" + dockerTargetPath + ",readonly" - ); + options.add(bindMountSpec(path, dockerTargetPath)); } } private void mountSolversToDocker(List options){ @@ -611,17 +615,11 @@ private List getInterpreterCommand(File interpreterFile, Path lustreFile mountSolversToDocker(options); options.add("--mount"); - options.add( - "type=bind,source=" + interpreterFile.getAbsolutePath() - + ",target=" + DOCKER_INTERPRETER_INPUT - + ",readonly"); + options.add(bindMountSpec(interpreterFile.toPath(), DOCKER_INTERPRETER_INPUT)); if (lustreFile != null) { options.add("--mount"); - options.add( - "type=bind,source=" + lustreFile.toAbsolutePath() - + ",target=" + DOCKER_LUSTRE_FILE - + ",readonly"); + options.add(bindMountSpec(lustreFile.toAbsolutePath(), DOCKER_LUSTRE_FILE)); } options.add(dockerImage); From f01df75149ba17a3ba51a13881e0a00f148c6bf1 Mon Sep 17 00:00:00 2001 From: Josh Date: Thu, 1 Oct 2026 17:56:57 -0500 Subject: [PATCH 17/21] Reject setting the swap usage to a value below the physical memory usage --- src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 726c295..af24795 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -1064,6 +1064,10 @@ public void setSafeModeMemoryUsage(String amount){ */ public void setSafeModeSwapUsage(String amount){ validateMemoryValue(amount, "Swap usage"); + if (memoryValueToBytes(amount) < memoryValueToBytes(safeModeMemoryUsage)) { + throw new IllegalArgumentException("Swap usage was set to " + amount + + ", but it must be greater than or equal to the memory usage (" + safeModeMemoryUsage + ")"); + } safeModeSwapUsage = amount; } From 241d1a866b8c10655b65ae81297ed46d6ab25d43 Mon Sep 17 00:00:00 2001 From: Josh Date: Thu, 1 Oct 2026 18:03:55 -0500 Subject: [PATCH 18/21] Update docker image --- Dockerfile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 75fa28e..086d222 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,3 +1,4 @@ -FROM ubuntu:24.04 +ARG JAVA_MAJOR=8 +FROM eclipse-temurin:${JAVA_MAJOR}-jre ENTRYPOINT [] \ No newline at end of file From 58e981a439490a51428c69e9d93127c3a6a2651a Mon Sep 17 00:00:00 2001 From: Josh Date: Thu, 1 Oct 2026 18:04:03 -0500 Subject: [PATCH 19/21] Add docker build script --- build-docker.sh | 1 + 1 file changed, 1 insertion(+) create mode 100755 build-docker.sh diff --git a/build-docker.sh b/build-docker.sh new file mode 100755 index 0000000..7ed46bf --- /dev/null +++ b/build-docker.sh @@ -0,0 +1 @@ +docker build -t kind2-safe:latest . From 5dd8afe5571fc59dfbfde80b3d48c9c00ce030ed Mon Sep 17 00:00:00 2001 From: Josh Date: Thu, 1 Oct 2026 18:19:15 -0500 Subject: [PATCH 20/21] Update comment --- src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index af24795..6fd13c9 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -739,7 +739,7 @@ public List getOptions() { options.add("--z3_bin"); options.add(DOCKER_Z3_BIN); } - } else { // safe mode, use fixed container paths + } else { // normal mode, use given paths if (bitwuzlaBin != null) { options.add("--bitwuzla_bin"); options.add(bitwuzlaBin); From 0879fd616aaf9a6d787c7bec7ce073b8c8ccf8f7 Mon Sep 17 00:00:00 2001 From: Josh Date: Thu, 1 Oct 2026 18:25:10 -0500 Subject: [PATCH 21/21] Fix lowercase bug --- src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 6fd13c9..09c5742 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -1026,7 +1026,7 @@ private void validateMemoryValue(String value, String setting){ private long memoryValueToBytes(String v){ long value = Long.parseLong(v.substring(0, v.length()-1)); - char unit = v.charAt(v.toLowerCase().length()-1); + char unit = Character.toLowerCase(v.charAt(v.length()-1)); long modifier; switch(unit){ case 'b': modifier = 1L; break;