diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index af57236d..062eb5e4 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -11,7 +11,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.8 + 0.0.10 liquidjava-verifier LiquidJava Verifier https://github.com/liquid-java/liquidjava diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java index 5cc0562e..c2092391 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java @@ -9,6 +9,7 @@ import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; +import liquidjava.utils.Utils; import java.util.HashMap; import java.util.Map; @@ -47,8 +48,7 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map var chains + */ + private static VarDerivationNode flattenVarOrigin(String varName, DerivationNode origin) { + if (origin instanceof VarDerivationNode varOrigin && Utils.isSameVariable(varOrigin.getVar(), varName)) { + return flattenVarOrigin(varOrigin.getVar(), varOrigin.getOrigin()); // recursively flatten + } + return origin != null ? new VarDerivationNode(varName, origin) : new VarDerivationNode(varName); + } } \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 275a5597..d93482a0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -42,4 +42,17 @@ public static SourcePosition getRefinementAnnotationPosition(CtElement element, return unquoted.equals(refinement); }).findFirst().map(CtElement::getPosition).orElse(element.getPosition()); } + + public static boolean isSameVariable(String var1, String var2) { + int index1 = var1.lastIndexOf('_'); + int index2 = var2.lastIndexOf('_'); + // no format + if (index1 < 0 || index2 < 0) { + return var1.equals(var2); + } + // #(.*)_n format + String name1 = var1.substring(0, index1); + String name2 = var2.substring(0, index2); + return name1.equals(name2); + } }