From 265fcd4a7cfea4a81802e03529d6a012b4b8cc57 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 22 Sep 2026 11:23:09 -0500 Subject: [PATCH] Read a machine integer as an integer Kind 2 has two surface syntaxes for machine integers: the keywords `uint8` through `int64`, and `uint`/`sint` for a width of any size. Its JSON output names every one of them in the general form, including the eight that have a keyword, so the `case "int8":` arms of `Type.getType` never matched anything it printed. A machine integer therefore fell to the default of that switch, which treats a name it does not know as an enumeration, and arrived as an `Enum` holding an `EnumValue`: a consumer got the name of a constant where it wanted a number, with no `IntValue` and no `BigInteger` to do arithmetic with. Reading the general form gives back an `Int` holding an `IntValue`. Like the cases for the eight keywords, it gives the width up rather than carrying it, which also means a width with no keyword of its own, such as `uint<24>`, reads like any other. Co-Authored-By: Claude Opus 5 (1M context) --- .../edu/uiowa/cs/clc/kind2/results/Type.java | 10 ++++++ .../clc/kind2/results/Kind2ResultTests.java | 33 +++++++++++++++++++ 2 files changed, 43 insertions(+) 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 69c455a..c6f6b9a 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 @@ -122,6 +122,16 @@ public static Type getType(String typeString, JsonElement typeInfo) return new SubRange(min, max); } + // A machine integer, of any width. Kind 2 names every one of them + // this way in its JSON output, the eight that have a keyword of + // their own included, so the cases above never match what it prints + // and this is what reaches a machine integer. Like those cases, it + // gives the width up and reports the stream as an integer. + if (typeString.matches("(u|s)int<[1-9][0-9]*>")) + { + return new Int(); + } + if (typeString.startsWith("array of")) { String elementTypeName = typeString.replaceFirst("array of", "").trim(); 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 e4b3891..5fc2569 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 @@ -9,6 +9,7 @@ package edu.uiowa.cs.clc.kind2.results; import java.io.IOException; +import java.math.BigInteger; import java.math.RoundingMode; import java.nio.file.Files; import java.nio.file.Paths; @@ -631,4 +632,36 @@ void datatypeCounterExampleFromOlderKind2() DatatypeValue cons = (DatatypeValue) stream.getStepValues().get(1).getKind2Value(); assertEquals("Cons(1, Nil)", cons.toString()); } + /** + * A counterexample over machine integers. Kind 2 names them in the general + * form, which admits a width that has no keyword of its own, and they are + * integers rather than names. + */ + @Test + void machineIntegerCounterExample() + { + String json = "[{'objectType' : 'log','level' : 'info','source' : 'parse','value' : 'kind2 v3.0.0'},{'objectType' : 'analysisStart','top' : 'main','concrete' : [],'abstract' : [],'assumptions' : []},{'objectType' : 'property','name' : 'InvProp[l8c3]','source' : 'PropAnnot','file' : './examples/bv.lus','line' : 8,'column' : 3,'runtime' : {'unit' : 'sec', 'timeout' : false, 'value' : 0.010},'k' : 0,'answer' : {'source' : 'bmc', 'value' : 'falsifiable'},'counterExample' :[{'blockType' : 'node','name' : 'main','streams' :[{'name' : 'i','type' : 'uint<8>','class' : 'local','instantValues' : [[0, 200],[1, 201]]},{'name' : 'j','type' : 'sint<8>','class' : 'local','instantValues' : [[0, 127],[1, -128]]},{'name' : 'k','type' : 'uint<24>','class' : 'local','instantValues' : [[0, 16777215]]}]}]},{'objectType' : 'analysisStop'}]"; + + Result result = Result.analyzeJsonResult(json); + assertNotNull(result.getRoot()); + + Property property = result.getRoot().getAnalyses().get(0).getFalsifiedProperties().get(0); + List streams = property.getCounterExample().getTopNode().getStreams(); + + for (Stream stream : streams) + { + assertTrue(stream.getKind2Type() instanceof Int, + stream.getName() + " should be an integer, not " + stream.getKind2Type()); + } + + IntValue unsigned = (IntValue) streams.get(0).getStepValues().get(0).getKind2Value(); + assertEquals(new BigInteger("200"), unsigned.getValue()); + + IntValue negative = (IntValue) streams.get(1).getStepValues().get(1).getKind2Value(); + assertEquals(new BigInteger("-128"), negative.getValue()); + + // A width with no keyword of its own, which only the general form names + IntValue wide = (IntValue) streams.get(2).getStepValues().get(0).getKind2Value(); + assertEquals(new BigInteger("16777215"), wide.getValue()); + } }