Gracefully fail on a non-tuple argument in Json!JsonSerialize and

Json!ndJsonSerialize.

Related to microsoft/CCF#5807

[Feature][TLC]

Author: lemmy

modules/tlc2/overrides/Json.java

@@ -42,7 +42,10 @@
 import com.google.gson.JsonParser;
 import com.google.gson.JsonPrimitive;
 
+import tlc2.output.EC;
+import tlc2.tool.EvalException;
 import tlc2.value.IValue;
+import tlc2.value.Values;
 import tlc2.value.impl.BoolValue;
 import tlc2.value.impl.FcnLambdaValue;
 import tlc2.value.impl.FcnRcdValue;
@@ -144,7 +147,11 @@ public static IValue deserialize(final StringValue path) throws IOException {
    */
   @TLAPlusOperator(identifier = "ndJsonSerialize", module = "Json", warn = false)
   public synchronized static BoolValue ndSerialize(final StringValue path, final Value v) throws IOException {
-	TupleValue value = (TupleValue) v.toTuple();
+	final TupleValue value = (TupleValue) v.toTuple();
+	if (value == null) {
+		throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+				new String[] { "second", "ndJsonSerialize", "sequence", Values.ppr(v.toString()) });
+	}
     File file = new File(path.val.toString());
     if (file.getParentFile() != null) {file.getParentFile().mkdirs();} // Cannot create parent dir for relative path.
     try (BufferedWriter writer = new BufferedWriter(new FileWriter(new File(path.val.toString())))) {
@@ -164,7 +171,11 @@ public synchronized static BoolValue ndSerialize(final StringValue path, final V
    */
   @TLAPlusOperator(identifier = "JsonSerialize", module = "Json", warn = false)
   public synchronized static BoolValue serialize(final StringValue path, final Value v) throws IOException {
-	TupleValue value = (TupleValue) v.toTuple();
+	final TupleValue value = (TupleValue) v.toTuple();
+	if (value == null) {
+		throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+				new String[] { "second", "JsonSerialize", "sequence", Values.ppr(v.toString()) });
+	}
     File file = new File(path.val.toString());
     if (file.getParentFile() != null) {file.getParentFile().mkdirs();} // Cannot create parent dir for relative path.
     try (BufferedWriter writer = new BufferedWriter(new FileWriter(new File(path.val.toString())))) {

tests/JsonTests.tla

@@ -166,4 +166,24 @@ ASSUME(RoundTrip)
 ASSUME LET input == <<[a |-> 3], <<<<1, 2>>, "look">>, << <<[b |-> [c |-> <<4, 5, 6>>]]>> >> >>
        IN  input = ndJsonDeserialize("tests/JsonTests.ndjson")
 
+-----
+
+ASSUME AssertError(
+           "The second argument of JsonSerialize should be a sequence, but instead it is:\n[a |-> 1, b |-> TRUE]",
+           JsonSerialize("target/json/test.json", [a |-> 1, b |-> TRUE] ))
+
+ASSUME AssertError(
+           "The second argument of ndJsonSerialize should be a sequence, but instead it is:\n[a |-> 1, b |-> TRUE]",
+           ndJsonSerialize("target/json/test.json", [a |-> 1, b |-> TRUE] ))
+
+
+ASSUME AssertError(
+           "The second argument of JsonSerialize should be a sequence, but instead it is:\n42",
+           JsonSerialize("target/json/test.json", 42 ))
+
+ASSUME AssertError(
+           "The second argument of ndJsonSerialize should be a sequence, but instead it is:\n42",
+           ndJsonSerialize("target/json/test.json", 42 ))
+
+
 =============================================================================