Read algebraic datatype values

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<String> 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<String> 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<String> getConstructors()
+  {
+    return Collections.unmodifiableList(constructors);
+  }
+}

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<Value> 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<Value> 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<Value> getArgs()
+  {
+    return Collections.unmodifiableList(args);
+  }
+
+  @Override
+  public String toString()
+  {
+    if (args.isEmpty())
+    {
+      return constructor;
+    }
+    return constructor + "("
+        + args.stream().map(Value::toString).collect(Collectors.joining(", ")) + ")";
+  }
+}

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.
    */

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<String> 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"))

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<Value> 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.
    *

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());
+  }
 }