diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 380edf9a..815155e5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -7,6 +7,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.smt.Counterexample; +import liquidjava.utils.VariableFormatter; import spoon.reflect.cu.SourcePosition; /** @@ -22,7 +23,9 @@ public class RefinementError extends LJError { public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found, TranslationTable translationTable, Counterexample counterexample, String customMessage) { - super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()), + super("Refinement Error", + String.format("%s is not a subtype of %s", VariableFormatter.formatText(found.getValue().toString()), + VariableFormatter.formatText(expected.getValue().toString())), position, translationTable, customMessage); this.expected = expected; this.found = found; @@ -47,7 +50,7 @@ public String getCounterExampleString() { // only include variables that appear in the found value .filter(a -> foundVarNames.contains(a.first())) // format as "var == value" - .map(a -> a.first() + " == " + a.second()) + .map(a -> VariableFormatter.formatVariable(a.first()) + " == " + a.second()) // join with "&&" .collect(Collectors.joining(" && ")); @@ -68,4 +71,4 @@ public ValDerivationNode getExpected() { public ValDerivationNode getFound() { return found; } -} \ No newline at end of file +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index 976508cf..1e83a2bc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -2,6 +2,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Expression; +import liquidjava.utils.VariableFormatter; import spoon.reflect.cu.SourcePosition; /** @@ -16,11 +17,11 @@ public class StateRefinementError extends LJError { public StateRefinementError(SourcePosition position, Expression expected, Expression found, TranslationTable translationTable, String customMessage) { - super("State Refinement Error", - String.format("Expected state %s but found %s", expected.toString(), found.toString()), position, - translationTable, customMessage); - this.expected = expected.toString(); - this.found = found.toString(); + super("State Refinement Error", String.format("Expected state %s but found %s", + VariableFormatter.formatText(expected.toString()), VariableFormatter.formatText(found.toString())), + position, translationTable, customMessage); + this.expected = VariableFormatter.formatText(expected.toString()); + this.found = VariableFormatter.formatText(found.toString()); } public String getExpected() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java index 64eb4fad..be9afb00 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java @@ -15,6 +15,7 @@ import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.Var; +import liquidjava.utils.VariableFormatter; public class ValDerivationNode extends DerivationNode { @@ -41,17 +42,17 @@ private static class ExpressionSerializer implements JsonSerializer public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationContext context) { if (exp == null) return JsonNull.INSTANCE; - if (exp instanceof LiteralInt) - return new JsonPrimitive(((LiteralInt) exp).getValue()); - if (exp instanceof LiteralLong) - return new JsonPrimitive(((LiteralLong) exp).getValue()); - if (exp instanceof LiteralReal) - return new JsonPrimitive(((LiteralReal) exp).getValue()); - if (exp instanceof LiteralBoolean) - return new JsonPrimitive(exp.isBooleanTrue()); - if (exp instanceof Var) - return new JsonPrimitive(((Var) exp).getName()); - return new JsonPrimitive(exp.toString()); + if (exp instanceof LiteralInt v) + return new JsonPrimitive(v.getValue()); + if (exp instanceof LiteralLong v) + return new JsonPrimitive(v.getValue()); + if (exp instanceof LiteralReal v) + return new JsonPrimitive(v.getValue()); + if (exp instanceof LiteralBoolean v) + return new JsonPrimitive(v.isBooleanTrue()); + if (exp instanceof Var v) + return new JsonPrimitive(VariableFormatter.formatVariable(v.getName())); + return new JsonPrimitive(VariableFormatter.formatText(exp.toString())); } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java index c134a44e..a8dce4c5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java @@ -1,7 +1,18 @@ package liquidjava.rj_language.opt.derivation_node; +import java.lang.reflect.Type; + +import com.google.gson.JsonElement; +import com.google.gson.JsonPrimitive; +import com.google.gson.JsonSerializationContext; +import com.google.gson.JsonSerializer; +import com.google.gson.annotations.JsonAdapter; + +import liquidjava.utils.VariableFormatter; + public class VarDerivationNode extends DerivationNode { + @JsonAdapter(VariableNameSerializer.class) private final String var; private final DerivationNode origin; @@ -22,4 +33,11 @@ public String getVar() { public DerivationNode getOrigin() { return origin; } + + private static class VariableNameSerializer implements JsonSerializer { + @Override + public JsonElement serialize(String src, Type typeOfSrc, JsonSerializationContext context) { + return new JsonPrimitive(VariableFormatter.formatVariable(src)); + } + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/utils/VariableFormatter.java new file mode 100644 index 00000000..0629fbff --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/VariableFormatter.java @@ -0,0 +1,53 @@ +package liquidjava.utils; + +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +public final class VariableFormatter { + private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$"); + private static final Pattern INSTANCE_VAR_TEXT_PATTERN = Pattern.compile("#[^\\s,;:()\\[\\]{}]+_[0-9]+"); + private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' }; + + public static String formatVariable(String name) { + if (name == null) + return null; + + Matcher matcher = INSTACE_VAR_PATTERN.matcher(name); + if (!matcher.matches()) + return name; + + String baseName = matcher.group(1); + String counter = matcher.group(2); + String prefix = isSpecialIdentifier(baseName) ? "#" : ""; + return prefix + baseName + toSuperscript(counter); + } + + public static String formatText(String text) { + if (text == null) + return null; + + Matcher textMatcher = INSTANCE_VAR_TEXT_PATTERN.matcher(text); + StringBuilder sb = new StringBuilder(); + while (textMatcher.find()) { + String token = textMatcher.group(); + textMatcher.appendReplacement(sb, Matcher.quoteReplacement(formatVariable(token))); + } + textMatcher.appendTail(sb); + return sb.toString(); + } + + private static String toSuperscript(String number) { + StringBuilder sb = new StringBuilder(number.length()); + for (char c : number.toCharArray()) { + int index = c - '0'; + if (index < 0 || index >= SUPERSCRIPT_CHARS.length) + return number; + sb.append(SUPERSCRIPT_CHARS[index]); + } + return sb.toString(); + } + + private static boolean isSpecialIdentifier(String id) { + return id.equals("fresh") || id.equals("ret"); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/variable_formatter/VariableFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/variable_formatter/VariableFormatterTest.java new file mode 100644 index 00000000..98e52ea0 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/variable_formatter/VariableFormatterTest.java @@ -0,0 +1,31 @@ +package liquidjava.variable_formatter; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import liquidjava.rj_language.ast.Var; +import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; +import liquidjava.utils.VariableFormatter; + +import org.junit.jupiter.api.Test; + +class VariableFormatterTest { + + @Test + void testInstanceVariableDisplayNameFormatting() { + assertEquals("x", VariableFormatter.formatVariable("x")); + assertEquals("x²", VariableFormatter.formatVariable("#x_2")); + assertEquals("#fresh¹²", VariableFormatter.formatVariable("#fresh_12")); + assertEquals("#ret³", VariableFormatter.formatVariable("#ret_3")); + assertEquals("this#Class", VariableFormatter.formatVariable("this#Class")); + } + + @Test + void testDerivationNodeUsesSuperscriptNotation() { + ValDerivationNode node = new ValDerivationNode(new Var("#x_2"), new VarDerivationNode("#x_2")); + String serialized = node.toString(); + assertTrue(serialized.contains("\"value\": \"x²\""), "Expected derivation value to use superscript notation"); + assertTrue(serialized.contains("\"var\": \"x²\""), "Expected derivation origin to use superscript notation"); + } +}