diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Datatype.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Datatype.java new file mode 100644 index 0000000..201bcd0 --- /dev/null +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Datatype.java @@ -0,0 +1,42 @@ +/* + * Copyright (c) 2020, Board of Trustees of the University of Iowa + * All rights reserved. + * + * Licensed under the BSD 3-Clause License. See LICENSE in the project root for license information. + */ + +package edu.uiowa.cs.clc.kind2.results; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +/** + * Kind2 type for algebraic datatypes. + */ +public class Datatype extends Type +{ + private final List constructors; + + /** + * Constructs a datatype with the given name and constructors. + * + * @param name the name of the datatype + * @param constructors the names of the datatype's constructors + */ + public Datatype(String name, List constructors) + { + super(name); + this.constructors = new ArrayList<>(constructors); + } + + /** + * Returns the names of this datatype's constructors. + * + * @return the names of this datatype's constructors + */ + public List getConstructors() + { + return Collections.unmodifiableList(constructors); + } +} diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/DatatypeValue.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/DatatypeValue.java new file mode 100644 index 0000000..2e30a1d --- /dev/null +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/DatatypeValue.java @@ -0,0 +1,73 @@ +/* + * Copyright (c) 2020, Board of Trustees of the University of Iowa + * All rights reserved. + * + * Licensed under the BSD 3-Clause License. See LICENSE in the project root for license information. + */ + +package edu.uiowa.cs.clc.kind2.results; + +import com.google.gson.JsonElement; + +import java.util.Collections; +import java.util.List; +import java.util.stream.Collectors; + +/** + * The value of a kind2 algebraic datatype: a constructor applied to its + * fields, which is a constructor name alone when the constructor takes none. + */ +public class DatatypeValue extends Value +{ + private final String constructor; + private final List args; + + /** + * Constructs a datatype value from one Kind 2 stream value. + * + * @param kind2StepValue the step this value belongs to + * @param kind2Type the type of the value + * @param jsonElement the Kind 2 json element holding the value + * @param constructor the name of the constructor this value was built with + * @param args the fields the constructor was applied to + */ + public DatatypeValue(StepValue kind2StepValue, Type kind2Type, JsonElement jsonElement, + String constructor, List args) + { + super(kind2StepValue, kind2Type, jsonElement); + this.constructor = constructor; + this.args = args; + } + + /** + * Returns the name of the constructor this value was built with. + * + * @return the name of the constructor this value was built with + */ + public String getConstructor() + { + return constructor; + } + + /** + * Returns the fields the constructor was applied to, which is empty for a + * constructor that takes none. + * + * @return the fields the constructor was applied to + */ + public List getArgs() + { + return Collections.unmodifiableList(args); + } + + @Override + public String toString() + { + if (args.isEmpty()) + { + return constructor; + } + return constructor + "(" + + args.stream().map(Value::toString).collect(Collectors.joining(", ")) + ")"; + } +} diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Labels.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Labels.java index 24e9b0f..df311eb 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Labels.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Labels.java @@ -140,6 +140,21 @@ private Labels() * The element type of an array type, or the underlying type of a subrange type. */ public static final String baseType = "baseType"; + + /** + * The constructors of a datatype. + */ + public static final String constructors = "constructors"; + + /** + * The constructor an algebraic datatype value was built with. + */ + public static final String constructor = "constructor"; + + /** + * The fields a datatype constructor was applied to. + */ + public static final String args = "args"; /** * The class of a stream, which is one of input, output, or local. */ diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java index 286260f..69c455a 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java @@ -9,6 +9,10 @@ import edu.uiowa.cs.clc.kind2.Kind2Exception; import com.google.gson.JsonElement; +import com.google.gson.JsonObject; + +import java.util.ArrayList; +import java.util.List; /** * An abstract class for all kind2 types. @@ -40,6 +44,31 @@ public static Type getType(String type) { return getType(type, null); } + /** + * Builds the datatype described by the given type information. The element + * type of an array is named without any information of its own, so a + * datatype reached that way is left with its constructors unknown rather + * than rejected. + */ + private static Type makeDatatype(JsonElement typeInfo) + { + if (typeInfo == null) + { + return new Datatype("datatype", new ArrayList<>()); + } + JsonObject info = typeInfo.getAsJsonObject(); + String name = info.has(Labels.name) ? info.get(Labels.name).getAsString() : "datatype"; + List constructors = new ArrayList<>(); + if (info.has(Labels.constructors)) + { + for (JsonElement constructor : info.get(Labels.constructors).getAsJsonArray()) + { + constructors.add(constructor.getAsString()); + } + } + return new Datatype(name, constructors); + } + private static Type makeNestedArray(String baseType, int numDims){ if (numDims == 0){ return getType(baseType); @@ -80,6 +109,8 @@ public static Type getType(String typeString, JsonElement typeInfo) String baseType = typeInfo.getAsJsonObject().get(Labels.baseType).getAsString(); int numIndicies = typeInfo.getAsJsonObject().get("sizes").getAsJsonArray().size(); return makeNestedArray(baseType, numIndicies); + case "datatype": + return makeDatatype(typeInfo); default: { if (typeString.matches("subrange \\[.*?\\] of int")) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Value.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Value.java index d99fb3e..a975de0 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Value.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Value.java @@ -10,6 +10,9 @@ import com.google.gson.GsonBuilder; import com.google.gson.JsonArray; import com.google.gson.JsonElement; +import com.google.gson.JsonObject; +import com.google.gson.JsonPrimitive; +import edu.uiowa.cs.clc.kind2.Kind2Exception; import java.util.ArrayList; import java.util.List; @@ -105,6 +108,31 @@ public static Value getKind2Value(StepValue kind2StepValue, Type kind2Type, Json return new ArrayValue(kind2StepValue, kind2Type, jsonElement, values); } + if (kind2Type instanceof Datatype) + { + // Kind 2 releases up to 3.0.0 wrote a constructor taking no fields as a + // bare name rather than as a constructor with an empty field list, and + // gson read that name as a string. Read it as the constructor it names, + // so that the output of those releases is still understood. + if (jsonElement.isJsonPrimitive()) + { + return new DatatypeValue(kind2StepValue, kind2Type, jsonElement, + jsonElement.getAsString().trim(), new ArrayList<>()); + } + + JsonObject object = jsonElement.getAsJsonObject(); + String constructor = object.get(Labels.constructor).getAsString(); + List args = new ArrayList<>(); + if (object.has(Labels.args)) + { + for (JsonElement arg : object.get(Labels.args).getAsJsonArray()) + { + args.add(getKind2Value(kind2StepValue, getFieldType(arg), arg)); + } + } + return new DatatypeValue(kind2StepValue, kind2Type, jsonElement, constructor, args); + } + if (kind2Type instanceof Enum) { return new EnumValue(kind2StepValue, kind2Type, jsonElement); @@ -113,6 +141,59 @@ public static Value getKind2Value(StepValue kind2StepValue, Type kind2Type, Json throw new UnsupportedOperationException(kind2Type.toString()); } + /** + * Returns the type to read a datatype constructor's field as. Kind 2 does + * not name the types of a constructor's fields in its output, so the type + * is taken from the shape of the json: an object naming a constructor is + * another datatype value, an object with a numerator and a denominator is a + * real, and a primitive is whichever of a Boolean, a number or a name it + * holds. A name covers a constructor of an enumeration and a value of an + * uninterpreted sort alike, neither of which carries anything else. + * + * @param jsonElement the Kind 2 json element holding the field + * @return the type to read the field as + */ + private static Type getFieldType(JsonElement jsonElement) + { + if (jsonElement.isJsonArray()) + { + JsonArray array = jsonElement.getAsJsonArray(); + // An empty array has no element to take a type from. Nothing reads the + // element type of one, since it has no elements to read. + return new Array(array.size() == 0 ? new Bool() : getFieldType(array.get(0))); + } + + if (jsonElement.isJsonObject()) + { + JsonObject object = jsonElement.getAsJsonObject(); + if (object.has(Labels.constructor)) + { + return new Datatype("datatype", new ArrayList<>()); + } + if (object.has(Labels.numerator) && object.has(Labels.denominator)) + { + return new Real(); + } + throw new Kind2Exception("Unrecognized datatype field: " + jsonElement); + } + + if (jsonElement.isJsonPrimitive()) + { + JsonPrimitive primitive = jsonElement.getAsJsonPrimitive(); + if (primitive.isBoolean()) + { + return new Bool(); + } + if (primitive.isNumber()) + { + return primitive.getAsString().matches("-?\\d+") ? new Int() : new Real(); + } + return new Enum("enum"); + } + + throw new Kind2Exception("Unrecognized datatype field: " + jsonElement); + } + /** * Returns the Kind2 json output for this object. * diff --git a/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java b/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java index 23662b4..e4b3891 100644 --- a/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java +++ b/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java @@ -12,6 +12,7 @@ import java.math.RoundingMode; import java.nio.file.Files; import java.nio.file.Paths; +import java.util.Arrays; import java.util.List; import static org.junit.jupiter.api.Assertions.assertEquals; @@ -575,4 +576,59 @@ void real() throws IOException assertNotNull(result.getRoot()); System.out.println(result); } + /** + * A counterexample over an algebraic datatype. A constructor taking no + * fields is written as a constructor with an empty field list. + */ + @Test + void datatypeCounterExample() + { + String json = "[{'objectType' : 'log','level' : 'info','source' : 'parse','value' : 'kind2 v3.0.0'},{'objectType' : 'analysisStart','top' : 'main','concrete' : [],'abstract' : [],'assumptions' : []},{'objectType' : 'property','name' : 'InvProp[l6c3]','source' : 'PropAnnot','file' : './examples/adt.lus','line' : 6,'column' : 3,'runtime' : {'unit' : 'sec', 'timeout' : false, 'value' : 0.010},'k' : 0,'answer' : {'source' : 'bmc', 'value' : 'falsifiable'},'counterExample' :[{'blockType' : 'node','name' : 'main','streams' :[{'name' : 'l','type' : 'datatype','typeInfo' : {'name' : 'List','constructors' : ['Nil','Cons']},'class' : 'input','instantValues' : [[0, {'constructor' : 'Nil', 'args' : []}],[1, {'constructor' : 'Cons', 'args' : [1, {'constructor' : 'Nil', 'args' : []}]}]]}]}]},{'objectType' : 'analysisStop'}]"; + + Result result = Result.analyzeJsonResult(json); + assertNotNull(result.getRoot()); + + Property property = result.getRoot().getAnalyses().get(0).getFalsifiedProperties().get(0); + Stream stream = property.getCounterExample().getTopNode().getStreams().get(0); + + Datatype datatype = (Datatype) stream.getKind2Type(); + assertEquals("List", datatype.toString()); + assertEquals(Arrays.asList("Nil", "Cons"), datatype.getConstructors()); + + DatatypeValue nil = (DatatypeValue) stream.getStepValues().get(0).getKind2Value(); + assertEquals("Nil", nil.getConstructor()); + assertTrue(nil.getArgs().isEmpty()); + assertEquals("Nil", nil.toString()); + + DatatypeValue cons = (DatatypeValue) stream.getStepValues().get(1).getKind2Value(); + assertEquals("Cons", cons.getConstructor()); + assertEquals(2, cons.getArgs().size()); + assertEquals("1", cons.getArgs().get(0).toString()); + assertEquals("Nil", cons.getArgs().get(1).toString()); + assertEquals("Cons(1, Nil)", cons.toString()); + } + + /** + * Kind 2 releases up to 3.0.0 wrote a constructor taking no fields as a + * bare name, which gson read as a string. That output still reads as the + * constructor it names. + */ + @Test + void datatypeCounterExampleFromOlderKind2() + { + String json = "[{'objectType' : 'log','level' : 'info','source' : 'parse','value' : 'kind2 v3.0.0'},{'objectType' : 'analysisStart','top' : 'main','concrete' : [],'abstract' : [],'assumptions' : []},{'objectType' : 'property','name' : 'InvProp[l6c3]','source' : 'PropAnnot','file' : './examples/adt.lus','line' : 6,'column' : 3,'runtime' : {'unit' : 'sec', 'timeout' : false, 'value' : 0.010},'k' : 0,'answer' : {'source' : 'bmc', 'value' : 'falsifiable'},'counterExample' :[{'blockType' : 'node','name' : 'main','streams' :[{'name' : 'l','type' : 'datatype','typeInfo' : {'name' : 'List','constructors' : ['Nil','Cons']},'class' : 'input','instantValues' : [[0, Nil],[1, {'constructor' : 'Cons', 'args' : [1, Nil]}]]}]}]},{'objectType' : 'analysisStop'}]"; + + Result result = Result.analyzeJsonResult(json); + assertNotNull(result.getRoot()); + + Property property = result.getRoot().getAnalyses().get(0).getFalsifiedProperties().get(0); + Stream stream = property.getCounterExample().getTopNode().getStreams().get(0); + + DatatypeValue nil = (DatatypeValue) stream.getStepValues().get(0).getKind2Value(); + assertEquals("Nil", nil.getConstructor()); + assertTrue(nil.getArgs().isEmpty()); + + DatatypeValue cons = (DatatypeValue) stream.getStepValues().get(1).getKind2Value(); + assertEquals("Cons(1, Nil)", cons.toString()); + } }