diff --git a/.vscode/launch.json b/.vscode/launch.json new file mode 100644 index 00000000..a3d3b123 --- /dev/null +++ b/.vscode/launch.json @@ -0,0 +1,12 @@ +{ + "configurations": [ + { + "type": "java", + "name": "Run LiquidJava", + "request": "launch", + "mainClass": "liquidjava.api.CommandLineLauncher", + "projectName": "liquidjava-verifier", + "args": "liquidjava-example/src/main/java/test" + } + ] +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Door.java b/liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Door.java new file mode 100644 index 00000000..e9532ace --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Door.java @@ -0,0 +1,11 @@ +package testSuite.classes.ambiguous_state_names_correct; + +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; + +@StateSet({"open", "closed"}) +public class Door { + + @StateRefinement(to = "open(this)") + public Door() { } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Pipe.java b/liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Pipe.java new file mode 100644 index 00000000..7701de3d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Pipe.java @@ -0,0 +1,11 @@ +package testSuite.classes.ambiguous_state_names_correct; + +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; + +@StateSet({"open", "closed"}) +public class Pipe { + + @StateRefinement(to = "open(this)") + public Pipe() { } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/SimpleTest.java new file mode 100644 index 00000000..2eaf174a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/SimpleTest.java @@ -0,0 +1,14 @@ +package testSuite.classes.ambiguous_state_names_correct; + +import liquidjava.specification.Refinement; + +public class SimpleTest { + + public static void main(String[] args) { + Door d = new Door(); // contains 'open' and 'closed' states + Pipe p = new Pipe(); // unrelated type with the same state names + requiresOpen(d); // ok iff 'open' binds to Door.open otherwise it may bind to Pipe.open and fail + } + + public static void requiresOpen(@Refinement("open(s)") Door s) { } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM1.java b/liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM1.java new file mode 100644 index 00000000..1875fc63 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM1.java @@ -0,0 +1,15 @@ +package testSuite.classes.conflicting_state_names_correct; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"uninitialized", "initialized"}) +public class SM1 { + + @StateRefinement(to="uninitialized(this)") + public SM1() {} + + + @StateRefinement(from="uninitialized(this)", to="initialized(this)") + public void initialize() {} +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM2.java b/liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM2.java new file mode 100644 index 00000000..8b545adc --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM2.java @@ -0,0 +1,15 @@ +package testSuite.classes.conflicting_state_names_correct; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"uninitialized", "initialized"}) +public class SM2 { + + @StateRefinement(to="uninitialized(this)") + public SM2() {} + + + @StateRefinement(from="uninitialized(this)", to="initialized(this)") + public void initialize() {} +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SimpleTest.java new file mode 100644 index 00000000..f8646ac3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SimpleTest.java @@ -0,0 +1,11 @@ +package testSuite.classes.conflicting_state_names_correct; + +class SimpleTest { + public static void main(String[] args) { + // both classes contain the same state names + SM1 sm1 = new SM1(); + SM2 sm2 = new SM2(); + sm1.initialize(); + sm2.initialize(); + } +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index eea4f6f6..35daad11 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -1,6 +1,7 @@ package liquidjava.processor; import liquidjava.rj_language.Predicate; +import liquidjava.utils.Utils; import spoon.reflect.reference.CtTypeReference; /** @@ -29,7 +30,7 @@ public void setNext(VCImplication c) { public String toString() { if (name != null && type != null) { String qualType = type.getQualifiedName(); - String simpleType = qualType.contains(".") ? qualType.substring(qualType.lastIndexOf(".") + 1) : qualType; + String simpleType = qualType.contains(".") ? Utils.getSimpleName(qualType) : qualType; return String.format("%-20s %s %s", "∀" + name + ":" + simpleType + ",", refinement.toString(), next != null ? " => \n" + next.toString() : ""); } else diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index d604a00d..a09fb0e4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -335,7 +335,7 @@ public void addGhostFunction(GhostFunction gh) { public boolean hasGhost(String name) { for (GhostFunction g : ghosts) { - if (g.getName().equals(name)) + if (g.matches(name)) return true; } return false; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java index c81f5c12..769f4680 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java @@ -12,40 +12,39 @@ public class GhostFunction { private String name; private List> param_types; private CtTypeReference return_type; + private String prefix; - private String klassName; - - public GhostFunction(GhostDTO f, Factory factory, String path, String klass) { - name = f.getName(); - return_type = Utils.getType(f.getReturn_type().equals(klass) ? path : f.getReturn_type(), factory); - param_types = new ArrayList<>(); + public GhostFunction(GhostDTO f, Factory factory, String prefix) { + String klass = this.getParentClassName(prefix); + this.name = f.getName(); + this.return_type = Utils.getType(f.getReturn_type().equals(klass) ? prefix : f.getReturn_type(), factory); + this.param_types = new ArrayList<>(); + this.prefix = prefix; for (String t : f.getParam_types()) { - param_types.add(Utils.getType(t.equals(klass) ? path : t, factory)); + this.param_types.add(Utils.getType(t.equals(klass) ? prefix : t, factory)); } } public GhostFunction(String name, List param_types, CtTypeReference return_type, Factory factory, - String path, String klass) { + String prefix) { + String klass = this.getParentClassName(prefix); + String type = return_type.toString().equals(klass) ? prefix : return_type.toString(); this.name = name; - this.return_type = Utils.getType(return_type.toString().equals(klass) ? path : return_type.toString(), factory); + this.return_type = Utils.getType(type, factory); this.param_types = new ArrayList<>(); + this.prefix = prefix; for (int i = 0; i < param_types.size(); i++) { String mType = param_types.get(i).toString(); - this.param_types.add(Utils.getType(mType.equals(klass) ? path : mType, factory)); + this.param_types.add(Utils.getType(mType.equals(klass) ? prefix : mType, factory)); } - this.klassName = klass; } - protected GhostFunction(String name, List> list, CtTypeReference return_type, String klass) { + protected GhostFunction(String name, List> list, CtTypeReference return_type, String prefix) { this.name = name; this.return_type = return_type; this.param_types = new ArrayList<>(); this.param_types = list; - this.klassName = klass; - } - - public String getName() { - return name; + this.prefix = prefix; } public CtTypeReference getReturnType() { @@ -67,7 +66,30 @@ public String toString() { return sb.toString(); } + public String getName() { + return name; + } + + public String getPrefix() { + return prefix; + } + + public String getQualifiedName() { + return Utils.qualifyName(prefix, name); + } + public String getParentClassName() { - return klassName; + return getParentClassName(prefix); + } + + private String getParentClassName(String pref) { + return Utils.getSimpleName(pref); + } + + // Match by fully qualified name, exact simple name or by comparing the simple name of the provided identifier + // This allows references written in a different class (different prefix) to still match + public boolean matches(String name) { + return this.getQualifiedName().equals(name) || this.name.equals(name) + || this.name.equals(Utils.getSimpleName(name)); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java index 6252c1c5..64974bdf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java @@ -9,9 +9,8 @@ public class GhostParentState extends GhostFunction { private ArrayList states; - public GhostParentState(String name, List params, CtTypeReference ret, Factory factory, - String qualifiedName, String simpleName) { - super(name, params, ret, factory, qualifiedName, simpleName); + public GhostParentState(String name, List params, CtTypeReference ret, Factory factory, String prefix) { + super(name, params, ret, factory, prefix); states = new ArrayList<>(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java index 8b14adae..3cdcacb7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java @@ -9,8 +9,8 @@ public class GhostState extends GhostFunction { private GhostFunction parent; private Predicate refinement; - public GhostState(String name, List> list, CtTypeReference return_type, String klass) { - super(name, list, return_type, klass); + public GhostState(String name, List> list, CtTypeReference return_type, String prefix) { + super(name, list, return_type, prefix); } public void setGhostParent(GhostFunction parent) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java index 9c367c2b..9bb59f18 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java @@ -12,6 +12,7 @@ public class AliasDTO { private List varTypes; private List varNames; private Expression expression; + private String ref; public AliasDTO(String name, List> varTypes, List varNames, Expression expression) { super(); @@ -26,7 +27,15 @@ public AliasDTO(String name2, List varTypes2, List varNames2, St this.name = name2; this.varTypes = varTypes2; this.varNames = varNames2; - this.expression = RefinementsParser.createAST(ref); + this.ref = ref; + } + + // Parse the alias expression using the given the prefix to ensure ghost names are qualified consistently with + // where the alias is declared or used + public void parse(String prefix) throws ParsingException { + if (ref != null) { + this.expression = RefinementsParser.createAST(ref, prefix); + } } public String getName() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index fe8de3c5..1be4493a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -12,6 +12,7 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.ParsingException; import liquidjava.rj_language.parsing.RefinementsParser; +import liquidjava.utils.Utils; import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtField; @@ -40,7 +41,7 @@ public void visitCtInterface(CtInterface intrface) { Optional externalRefinements = getExternalRefinement(intrface); if (externalRefinements.isPresent()) { - prefix = externalRefinements.get(); + this.prefix = externalRefinements.get(); try { getRefinementFromAnnotation(intrface); } catch (ParsingException e) { @@ -89,9 +90,7 @@ protected void getGhostFunction(String value, CtElement element) { // RefinementParser.parseFunctionDecl(value); GhostDTO f = RefinementsParser.getGhostDeclaration(value); if (f != null && element.getParent() instanceof CtInterface) { - String[] a = prefix.split("\\."); - String d = a[a.length - 1]; - GhostFunction gh = new GhostFunction(f, factory, prefix, d); + GhostFunction gh = new GhostFunction(f, factory, prefix); context.addGhostFunction(gh); } @@ -104,13 +103,12 @@ protected void getGhostFunction(String value, CtElement element) { @Override protected Optional createStateGhost(int order, CtElement element) { - String[] a = prefix.split("\\."); - String klass = a[a.length - 1]; + String klass = Utils.getSimpleName(prefix); if (klass != null) { CtTypeReference ret = factory.Type().INTEGER_PRIMITIVE; List params = Arrays.asList(klass); - GhostFunction gh = new GhostFunction(String.format("%s_state%d", klass.toLowerCase(), order), params, ret, - factory, prefix, klass); + String name = String.format("state%d", order); + GhostFunction gh = new GhostFunction(name, params, ret, factory, prefix); return Optional.of(gh); } return Optional.empty(); @@ -123,7 +121,6 @@ protected String getQualifiedClassName(CtElement elem) { @Override protected String getSimpleClassName(CtElement elem) { - String[] a = prefix.split("\\."); - return a[a.length - 1]; + return Utils.getSimpleName(prefix); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index aeae4792..2114067b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -128,7 +128,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) { CtLiteral s = (CtLiteral) ce; String f = s.getValue(); GhostState gs = new GhostState(f, g.getParametersTypes(), factory.Type().BOOLEAN_PRIMITIVE, - g.getParentClassName()); + g.getPrefix()); gs.setGhostParent(g); gs.setRefinement( /* new OperationPredicate(new InvocationPredicate(f, THIS), "<-->", */ @@ -194,9 +194,8 @@ protected Optional createStateGhost(int order, CtElement element) if (klass != null) { CtTypeReference ret = factory.Type().INTEGER_PRIMITIVE; List params = Arrays.asList(klass.getSimpleName()); - GhostFunction gh = new GhostFunction( - String.format("%s_state%d", klass.getSimpleName().toLowerCase(), order), params, ret, factory, - klass.getQualifiedName(), klass.getSimpleName()); + String name = String.format("state%d", order); + GhostFunction gh = new GhostFunction(name, params, ret, factory, klass.getQualifiedName()); return Optional.of(gh); } return Optional.empty(); @@ -207,7 +206,7 @@ protected void getGhostFunction(String value, CtElement element) { GhostDTO f = RefinementsParser.getGhostDeclaration(value); if (f != null && element.getParent() instanceof CtClass) { CtClass klass = (CtClass) element.getParent(); - GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName(), klass.getSimpleName()); + GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName()); context.addGhostFunction(gh); } } catch (ParsingException e) { @@ -233,6 +232,7 @@ protected void handleAlias(String value, CtElement element) { path = ((CtInterface) element).getQualifiedName(); } if (klass != null && path != null) { + a.parse(path); AliasWrapper aw = new AliasWrapper(a, factory, WILD_VAR, context, klass, path); context.addAlias(aw); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 0711807d..82cbf15d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -3,7 +3,9 @@ import java.util.ArrayList; import java.util.HashMap; import java.util.List; +import java.util.Set; import java.util.Stack; +import java.util.function.Consumer; import java.util.regex.Pattern; import java.util.stream.Collectors; import liquidjava.errors.ErrorEmitter; @@ -20,6 +22,7 @@ import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.factory.Factory; +import spoon.reflect.reference.CtTypeReference; public class VCChecker { private final Context context; @@ -47,10 +50,11 @@ public void processSubtyping(Predicate expectedType, List list, Stri Predicate premises = new Predicate(); Predicate et = new Predicate(); try { - premises = premisesBeforeChange.changeStatesToRefinements(list, s, errorEmitter) + List filtered = filterGhostStatesForVariables(list, mainVars, lrv); + premises = premisesBeforeChange.changeStatesToRefinements(filtered, s, errorEmitter) .changeAliasToRefinement(context, f); - et = expectedType.changeStatesToRefinements(list, s, errorEmitter).changeAliasToRefinement(context, f); + et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f); } catch (Exception e1) { printError(premises, expectedType, element, map, e1.getMessage()); return; @@ -87,9 +91,10 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List< Predicate et = new Predicate(); try { premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(list, s, errorEmitter) + List filtered = filterGhostStatesForVariables(list, mainVars, lrv); + premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s, errorEmitter) .changeAliasToRefinement(context, f); - et = expectedType.changeStatesToRefinements(list, s, errorEmitter).changeAliasToRefinement(context, f); + et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f); } catch (Exception e) { return false; // printError(premises, expectedType, element, map, e.getMessage()); @@ -100,6 +105,47 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List< return smtChecks(premises, et, p); } + /** + * Reduce the ghost states list to those whose declaring class (prefix) matches any of the involved variable types + * or their supertypes This prevents ambiguous simple name substitutions across unrelated classes that share state + * names + */ + private List filterGhostStatesForVariables(List list, List mainVars, + List vars) { + if (list.isEmpty()) + return list; + + // Collect all relevant qualified type names from involved variables and their supertypes + if (list == null || list.isEmpty()) + return list; + + // Collect all relevant qualified type names (types + supertypes), keeping order and deduping + Set allowedPrefixes = new java.util.LinkedHashSet<>(); + Consumer collect = rv -> { + if (rv.getType() != null) { + allowedPrefixes.add(rv.getType().getQualifiedName()); + } + for (CtTypeReference st : rv.getSuperTypes()) { + if (st != null) { + allowedPrefixes.add(st.getQualifiedName()); + } + } + }; + mainVars.forEach(collect); + vars.forEach(collect); + + if (allowedPrefixes.isEmpty()) + return list; // avoid over-filtering when types are unknown + + List filtered = list.stream().filter(g -> { + String prefix = (g.getParent() != null) ? g.getParent().getPrefix() : g.getPrefix(); + return allowedPrefixes.contains(prefix); + }).collect(Collectors.toList()); + + // If nothing matched, keep original to avoid accidental empties + return filtered.isEmpty() ? list : filtered; + } + private VCImplication joinPredicates(Predicate expectedType, List mainVars, List vars, HashMap map) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 93ae6503..8b1806fd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -6,6 +6,7 @@ import java.util.List; import java.util.Map; import java.util.Optional; + import liquidjava.processor.context.Context; import liquidjava.processor.context.RefinedFunction; import liquidjava.processor.context.RefinedVariable; @@ -16,6 +17,7 @@ import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.ParsingException; +import liquidjava.utils.Utils; import spoon.reflect.code.CtConstructorCall; import spoon.reflect.code.CtExpression; import spoon.reflect.code.CtFieldRead; @@ -90,7 +92,8 @@ public void getMethodRefinements(CtMethod method) throws ParsingException rtc.getContext().addFunctionToContext(f); auxGetMethodRefinements(method, f); - AuxStateHandler.handleMethodState(method, f, rtc); + String prefix = method.getDeclaringType().getQualifiedName(); + AuxStateHandler.handleMethodState(method, f, rtc, prefix); if (klass != null) AuxHierarchyRefinememtsPassage.checkFunctionInSupertypes(klass, method, f, rtc); @@ -98,8 +101,7 @@ public void getMethodRefinements(CtMethod method) throws ParsingException public void getMethodRefinements(CtMethod method, String prefix) throws ParsingException { String constructorName = ""; - String[] pac = prefix.split("\\."); - String k = pac[pac.length - 1]; + String k = Utils.getSimpleName(prefix); String functionName = String.format("%s.%s", prefix, method.getSimpleName()); if (k.equals(method.getSimpleName())) { // is a constructor @@ -114,7 +116,7 @@ public void getMethodRefinements(CtMethod method, String prefix) throws P rtc.getContext().addFunctionToContext(f); auxGetMethodRefinements(method, f); - AuxStateHandler.handleMethodState(method, f, rtc); + AuxStateHandler.handleMethodState(method, f, rtc, prefix); if (functionName.equals(constructorName) && !f.hasStateChange()) { AuxStateHandler.setDefaultState(f, rtc); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index f21329aa..b08c80da 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -72,15 +72,13 @@ private static void setConstructorStates(RefinedFunction f, List sets = getDifferentSets(tc, klass); // ?? for (GhostFunction sg : sets) { if (sg.getReturnType().toString().equals("int")) { - Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), + Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), s), Predicate.createLit("0", Utils.INT)); c = Predicate.createConjunction(c, p); } else { @@ -96,9 +94,9 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) { f.setAllStates(los); } - private static List getDifferentSets(TypeChecker tc, String klass) { + private static List getDifferentSets(TypeChecker tc, String klassQualified) { List sets = new ArrayList<>(); - List l = tc.getContext().getGhostState(klass); + List l = getGhostStatesFor(klassQualified, tc); if (l != null) { for (GhostState g : l) { if (g.getParent() == null) { @@ -120,11 +118,11 @@ private static List getDifferentSets(TypeChecker tc, String klass * * @throws ParsingException */ - public static void handleMethodState(CtMethod method, RefinedFunction f, TypeChecker tc) + public static void handleMethodState(CtMethod method, RefinedFunction f, TypeChecker tc, String prefix) throws ParsingException { List> an = getStateAnnotation(method); if (!an.isEmpty()) { - setFunctionStates(f, an, tc, method); + setFunctionStates(f, an, tc, method, prefix); } // f.setState(an, context.getGhosts(), method); @@ -141,33 +139,31 @@ public static void handleMethodState(CtMethod method, RefinedFunction f, Type * @throws ParsingException */ private static void setFunctionStates(RefinedFunction f, List> anns, - TypeChecker tc, CtElement element) throws ParsingException { + TypeChecker tc, CtElement element, String prefix) throws ParsingException { List l = new ArrayList<>(); for (CtAnnotation an : anns) { - l.add(getStates(an, f, tc, element)); + l.add(getStates(an, f, tc, element, prefix)); } f.setAllStates(l); } @SuppressWarnings({ "rawtypes" }) private static ObjectState getStates(CtAnnotation ctAnnotation, RefinedFunction f, - TypeChecker tc, CtElement e) throws ParsingException { + TypeChecker tc, CtElement e, String prefix) throws ParsingException { Map m = ctAnnotation.getAllValues(); String from = TypeCheckingUtils.getStringFromAnnotation(m.get("from")); String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to")); ObjectState state = new ObjectState(); - if (from != null) // has From - { - state.setFrom(createStatePredicate(from, f.getTargetClass(), tc, e, false)); + if (from != null) { // has From + state.setFrom(createStatePredicate(from, f.getTargetClass(), tc, e, false, prefix)); } - if (to != null) // has To - { - state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true)); + if (to != null) { // has To + state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true, prefix)); } if (from != null && to == null) // has From but not To -> the state remains the same { - state.setTo(createStatePredicate(from, f.getTargetClass(), tc, e, true)); + state.setTo(createStatePredicate(from, f.getTargetClass(), tc, e, true, prefix)); } if (from == null && to != null) // has To but not From -> enters with true and exists with a specific state { @@ -177,8 +173,8 @@ private static ObjectState getStates(CtAnnotation ctAnnota } private static Predicate createStatePredicate(String value, /* RefinedFunction f */ String targetClass, - TypeChecker tc, CtElement e, boolean isTo) throws ParsingException { - Predicate p = new Predicate(value, e, tc.getErrorEmitter()); + TypeChecker tc, CtElement e, boolean isTo, String prefix) throws ParsingException { + Predicate p = new Predicate(value, e, tc.getErrorEmitter(), prefix); String t = targetClass; // f.getTargetClass(); CtTypeReference r = tc.getFactory().Type().createReference(t); @@ -200,10 +196,8 @@ private static Predicate createStatePredicate(String value, /* RefinedFunction f } private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) { - String[] temp = t.split("\\."); - String simpleT = temp[temp.length - 1]; - List gs = p.getStateInvocations(tc.getContext().getGhostState(simpleT)); - List sets = getDifferentSets(tc, simpleT); + List gs = p.getStateInvocations(getGhostStatesFor(t, tc)); + List sets = getDifferentSets(tc, t); for (GhostState g : gs) { if (g.getParent() == null && sets.contains(g)) { sets.remove(g); @@ -214,6 +208,34 @@ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) return addOldStates(p, Predicate.createVar(tc.THIS), sets, tc); } + /** + * Collect ghost states for the given qualified class name and its immediate supertypes (superclass and interfaces). + */ + private static List getGhostStatesFor(String qualifiedClass, TypeChecker tc) { + // Keep order: class, then superclass, then interfaces; avoid duplicates + java.util.LinkedHashSet typeNames = new java.util.LinkedHashSet<>(); + typeNames.add(Utils.getSimpleName(qualifiedClass)); + + CtTypeReference ref = tc.getFactory().Type().createReference(qualifiedClass); + if (ref != null) { + CtTypeReference sup = ref.getSuperclass(); + if (sup != null) + typeNames.add(Utils.getSimpleName(sup.getQualifiedName())); + for (CtTypeReference itf : ref.getSuperInterfaces()) { + if (itf != null) + typeNames.add(Utils.getSimpleName(itf.getQualifiedName())); + } + } + + List res = new ArrayList<>(); + for (String tn : typeNames) { + List states = tc.getContext().getGhostState(tn); + if (states != null) + res.addAll(states); + } + return res; + } + /** * Create predicate with the equalities with previous versions of the object e.g., ghostfunction1(this) == * ghostfunction1(old(this)) @@ -229,8 +251,8 @@ private static Predicate addOldStates(Predicate p, Predicate th, List fw, TypeChecker tc) { } VariableInstance vi = invocation_callee.get(); - String instanceName = vi.getName(); Predicate prevState = vi.getRefinement().substituteVariable(tc.WILD_VAR, instanceName) .substituteVariable(parentTargetName, instanceName); @@ -340,8 +361,10 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { ObjectState stateChange = new ObjectState(); try { - Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false); - Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true); + String prefix = field.getDeclaringType().getQualifiedName(); + Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false, + prefix); + Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true, prefix); stateChange.setFrom(fromPredicate); stateChange.setTo(toPredicate); } catch (ParsingException e) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 978f1e56..eca80729 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -25,6 +25,7 @@ import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.utils.Utils; import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtType; import spoon.reflect.factory.Factory; /** @@ -35,6 +36,7 @@ public class Predicate { protected Expression exp; + protected String prefix; /** Create a predicate with the expression true */ public Predicate() { @@ -51,9 +53,25 @@ public Predicate() { * @throws ParsingException */ public Predicate(String ref, CtElement element, ErrorEmitter e) throws ParsingException { + this(ref, element, e, element.getParent(CtType.class).getQualifiedName()); + } + + /** + * Create a new predicate with a refinement and a given prefix for the class + * + * @param ref + * @param element + * @param e + * @param prefix + * + * @throws ParsingException + */ + public Predicate(String ref, CtElement element, ErrorEmitter e, String prefix) throws ParsingException { + this.prefix = prefix; exp = parse(ref, element, e); - if (e.foundError()) + if (e.foundError()) { return; + } if (!(exp instanceof GroupExpression)) { exp = new GroupExpression(exp); } @@ -66,16 +84,16 @@ public Predicate(Expression e) { protected Expression parse(String ref, CtElement element, ErrorEmitter e) throws ParsingException { try { - return RefinementsParser.createAST(ref); + return RefinementsParser.createAST(ref, prefix); } catch (ParsingException e1) { ErrorHandler.printSyntaxError(e1.getMessage(), ref, element, e); throw e1; } } - protected Expression innerParse(String ref, ErrorEmitter e) { + protected Expression innerParse(String ref, ErrorEmitter e, String prefix) { try { - return RefinementsParser.createAST(ref); + return RefinementsParser.createAST(ref, prefix); } catch (ParsingException e1) { ErrorHandler.printSyntaxError(e1.getMessage(), ref, e); } @@ -113,14 +131,14 @@ public List getVariableNames() { public List getStateInvocations(List lgs) { if (lgs == null) return new ArrayList<>(); - List all = lgs.stream().map(p -> p.getName()).collect(Collectors.toList()); + List all = lgs.stream().map(p -> p.getQualifiedName()).collect(Collectors.toList()); List toAdd = new ArrayList<>(); exp.getStateInvocations(toAdd, all); List gh = new ArrayList<>(); for (String n : toAdd) { for (GhostState g : lgs) - if (g.getName().equals(n)) + if (g.matches(n)) gh.add(g); } @@ -162,10 +180,16 @@ private void expressionGetOldVariableNames(Expression exp, List ls) { public Predicate changeStatesToRefinements(List ghostState, String[] toChange, ErrorEmitter ee) { Map nameRefinementMap = new HashMap<>(); - for (GhostState gs : ghostState) - if (gs.getRefinement() != null) // is a state and not a ghost state - nameRefinementMap.put(gs.getName(), innerParse(gs.getRefinement().toString(), ee)); - + for (GhostState gs : ghostState) { + if (gs.getRefinement() != null) { // is a state and not a ghost state + String name = gs.getQualifiedName(); + Expression exp = innerParse(gs.getRefinement().toString(), ee, gs.getPrefix()); + nameRefinementMap.put(name, exp); + // Also allow simple name lookup to enable hierarchy matching + String simple = Utils.getSimpleName(name); + nameRefinementMap.putIfAbsent(simple, exp); + } + } Expression e = exp.substituteState(nameRefinementMap, toChange); return new Predicate(e); } @@ -181,8 +205,7 @@ public String toString() { @Override public Predicate clone() { - Predicate c = new Predicate(exp.clone()); - return c; + return new Predicate(exp.clone()); } public Expression getExpression() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index 49426ca2..da75ec71 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -8,6 +8,7 @@ import liquidjava.processor.facade.AliasDTO; import liquidjava.rj_language.ast.typing.TypeInfer; import liquidjava.smt.TranslatorToZ3; +import liquidjava.utils.Utils; import spoon.reflect.factory.Factory; public abstract class Expression { @@ -98,10 +99,13 @@ public Expression substituteState(Map subMap, String[] toCha Expression e = clone(); if (this instanceof FunctionInvocation) { FunctionInvocation fi = (FunctionInvocation) this; - if (subMap.containsKey(fi.name) && fi.children.size() == 1 && fi.children.get(0) instanceof Var) { // object + String key = fi.name; + String simple = Utils.getSimpleName(key); + boolean has = subMap.containsKey(key) || subMap.containsKey(simple); + if (has && fi.children.size() == 1 && fi.children.get(0) instanceof Var) { // object // state Var v = (Var) fi.children.get(0); - Expression sub = subMap.get(fi.name).clone(); + Expression sub = (subMap.containsKey(key) ? subMap.get(key) : subMap.get(simple)).clone(); for (String s : toChange) { sub = sub.substitute(new Var(s), v); } @@ -119,10 +123,13 @@ private void auxSubstituteState(Map subMap, String[] toChang Expression exp = children.get(i); if (exp instanceof FunctionInvocation) { FunctionInvocation fi = (FunctionInvocation) exp; - if (subMap.containsKey(fi.name) && fi.children.size() == 1 && fi.children.get(0) instanceof Var) { // object + String key = fi.name; + String simple = Utils.getSimpleName(key); + boolean has = subMap.containsKey(key) || subMap.containsKey(simple); + if (has && fi.children.size() == 1 && fi.children.get(0) instanceof Var) { // object // state Var v = (Var) fi.children.get(0); - Expression sub = subMap.get(fi.name).clone(); + Expression sub = (subMap.containsKey(key) ? subMap.get(key) : subMap.get(simple)).clone(); for (String s : toChange) { sub = sub.substitute(new Var(s), v); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java index 9e93690e..f920ff7f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java @@ -5,6 +5,7 @@ import java.util.List; import java.util.stream.Collectors; import liquidjava.smt.TranslatorToZ3; +import liquidjava.utils.Utils; public class FunctionInvocation extends Expression { String name; @@ -50,8 +51,18 @@ public void getVariableNames(List toAdd) { @Override public void getStateInvocations(List toAdd, List all) { - if (!toAdd.contains(name) && all.contains(name)) - toAdd.add(name); + if (!toAdd.contains(name)) { + // Accept either qualified or simple name + if (all.contains(name)) { + toAdd.add(name); + } else { + String simple = Utils.getSimpleName(name); + boolean matchesSimple = all.stream() + .anyMatch(s -> s.equals(simple) || (s.contains(".") && Utils.getSimpleName(s).equals(simple))); + if (matchesSimple) + toAdd.add(name); + } + } for (Expression e : getArgs()) e.getStateInvocations(toAdd, all); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java index 9f902fac..4bcf17d4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java @@ -95,7 +95,7 @@ else if (e.isBooleanOperation()) { // >, >=, <, <=, ==, != } private static Optional> functionType(Context ctx, Factory factory, FunctionInvocation e) { - Optional gh = ctx.getGhosts().stream().filter(g -> g.getName().equals(e.getName())).findAny(); + Optional gh = ctx.getGhosts().stream().filter(g -> g.matches(e.getName())).findAny(); return gh.map(i -> i.getReturnType()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java index 55daed4a..ed049551 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java @@ -17,9 +17,10 @@ public class RefinementsParser { - public static Expression createAST(String toParse) throws ParsingException { + public static Expression createAST(String toParse, String prefix) throws ParsingException { ParseTree pt = compile(toParse); - return CreateASTVisitor.create(pt); + CreateASTVisitor visitor = new CreateASTVisitor(prefix); + return visitor.create(pt); } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index d647875a..102c9e58 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -14,6 +14,8 @@ import liquidjava.rj_language.ast.LiteralString; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; +import liquidjava.utils.Utils; + import org.antlr.v4.runtime.tree.ParseTree; import org.apache.commons.lang3.NotImplementedException; import rj.grammar.RJParser.AliasCallContext; @@ -55,7 +57,13 @@ */ public class CreateASTVisitor { - public static Expression create(ParseTree rc) { + String prefix; + + public CreateASTVisitor(String prefix) { + this.prefix = prefix; + } + + public Expression create(ParseTree rc) { if (rc instanceof ProgContext) return progCreate((ProgContext) rc); else if (rc instanceof StartContext) @@ -76,20 +84,20 @@ else if (rc instanceof LiteralContext) return null; } - private static Expression progCreate(ProgContext rc) { + private Expression progCreate(ProgContext rc) { if (rc.start() != null) return create(rc.start()); return null; } - private static Expression startCreate(ParseTree rc) { + private Expression startCreate(ParseTree rc) { if (rc instanceof StartPredContext) return create(((StartPredContext) rc).pred()); // alias and ghost do not have evaluation return null; } - private static Expression predCreate(ParseTree rc) { + private Expression predCreate(ParseTree rc) { if (rc instanceof PredGroupContext) return new GroupExpression(create(((PredGroupContext) rc).pred())); else if (rc instanceof PredNegateContext) @@ -104,7 +112,7 @@ else if (rc instanceof IteContext) return create(((PredExpContext) rc).exp()); } - private static Expression expCreate(ParseTree rc) { + private Expression expCreate(ParseTree rc) { if (rc instanceof ExpGroupContext) return new GroupExpression(create(((ExpGroupContext) rc).exp())); else if (rc instanceof ExpBoolContext) { @@ -116,7 +124,7 @@ else if (rc instanceof ExpBoolContext) { } } - private static Expression operandCreate(ParseTree rc) { + private Expression operandCreate(ParseTree rc) { if (rc instanceof OpLiteralContext) return create(((OpLiteralContext) rc).literalExpression()); else if (rc instanceof OpArithContext) @@ -135,7 +143,7 @@ else if (rc instanceof OpGroupContext) return null; } - private static Expression literalExpressionCreate(ParseTree rc) { + private Expression literalExpressionCreate(ParseTree rc) { if (rc instanceof LitGroupContext) return new GroupExpression(create(((LitGroupContext) rc).literalExpression())); else if (rc instanceof LitContext) @@ -150,11 +158,12 @@ else if (rc instanceof VarContext) { } } - private static Expression functionCallCreate(FunctionCallContext rc) { + private Expression functionCallCreate(FunctionCallContext rc) { if (rc.ghostCall() != null) { GhostCallContext gc = rc.ghostCall(); List le = getArgs(gc.args()); - return new FunctionInvocation(gc.ID().getText(), le); + String name = Utils.qualifyName(prefix, gc.ID().getText()); + return new FunctionInvocation(name, le); } else { AliasCallContext gc = rc.aliasCall(); List le = getArgs(gc.args()); @@ -162,7 +171,7 @@ private static Expression functionCallCreate(FunctionCallContext rc) { } } - private static List getArgs(ArgsContext args) { + private List getArgs(ArgsContext args) { List le = new ArrayList<>(); if (args != null) for (PredContext oc : args.pred()) { @@ -171,7 +180,7 @@ private static List getArgs(ArgsContext args) { return le; } - private static Expression literalCreate(LiteralContext literalContext) { + private Expression literalCreate(LiteralContext literalContext) { if (literalContext.BOOL() != null) return new LiteralBoolean(literalContext.BOOL().getText()); else if (literalContext.STRING() != null) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index 2cf2ca7a..5c5539d2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -127,7 +127,8 @@ public static void addGhostStates(Context z3, List ghostState, private static void addGhostFunction(Context z3, GhostFunction gh, Map> funcTranslation) { List> paramTypes = gh.getParametersTypes(); Sort ret = getSort(z3, gh.getReturnType().toString()); - Sort[] d = paramTypes.stream().map(t -> t.toString()).map(t -> getSort(z3, t)).toArray(Sort[]::new); - funcTranslation.put(gh.getName(), z3.mkFuncDecl(gh.getName(), d, ret)); + Sort[] domain = paramTypes.stream().map(t -> t.toString()).map(t -> getSort(z3, t)).toArray(Sort[]::new); + String name = gh.getQualifiedName(); + funcTranslation.put(name, z3.mkFuncDecl(name, domain, ret)); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 1a373e7d..b4219d2a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -17,6 +17,8 @@ import java.util.List; import java.util.Map; import liquidjava.processor.context.AliasWrapper; +import liquidjava.utils.Utils; + import org.apache.commons.lang3.NotImplementedException; public class TranslatorToZ3 implements AutoCloseable { @@ -90,11 +92,10 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws Exce return makeStore(name, params); if (name.equals("getFromIndex")) return makeSelect(name, params); - - if (!funcTranslation.containsKey(name)) - throw new NotFoundError("Function '" + name + "' not found"); - FuncDecl fd = funcTranslation.get(name); + if (fd == null) + fd = resolveFunctionDeclFallback(name, params); + Sort[] s = fd.getDomain(); for (int i = 0; i < s.length; i++) { Expr param = params[i]; @@ -114,6 +115,37 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws Exce return z3.mkApp(fd, params); } + /** + * Fallback resolver for function declarations when an exact qualified name lookup fails. Tries to match by simple + * name and number of parameters, preferring an exact qualified-name match if found among candidates; otherwise + * returns the first compatible candidate and relies on later coercion via var supertypes. + */ + private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) throws Exception { + String simple = Utils.getSimpleName(name); + FuncDecl candidate = null; + for (Map.Entry> entry : funcTranslation.entrySet()) { + String k = entry.getKey(); + String simpleK = Utils.getSimpleName(k); + if (simple.equals(simpleK)) { + FuncDecl fTry = entry.getValue(); + Sort[] dom = fTry.getDomain(); + if (dom.length == params.length) { + // Prefer exact qualified name match if available + if (k.equals(name)) { + candidate = fTry; + break; + } + // Otherwise first compatible match + candidate = fTry; + } + } + } + if (candidate != null) { + return candidate; + } + throw new NotFoundError("Function '" + name + "' not found"); + } + @SuppressWarnings({ "unchecked", "rawtypes" }) private Expr makeSelect(String name, Expr[] params) { if (params.length == 2 && params[0] instanceof ArrayExpr) diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 80a3ee43..145707d9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -1,5 +1,7 @@ package liquidjava.utils; +import java.util.Set; + import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtTypeReference; @@ -34,6 +36,8 @@ public class Utils { public static final String LONG = "long"; public static final String FLOAT = "float"; + private static final Set DEFAULT_NAMES = Set.of("old", "length", "addToIndex", "getFromIndex"); + public static CtTypeReference getType(String type, Factory factory) { // TODO complete switch (type) { @@ -54,4 +58,14 @@ public static CtTypeReference getType(String type, Factory factory) { return factory.createReference(type); } } + + public static String getSimpleName(String name) { + return name.contains(".") ? name.substring(name.lastIndexOf('.') + 1) : name; + } + + public static String qualifyName(String prefix, String name) { + if (DEFAULT_NAMES.contains(name)) + return name; // dont qualify + return String.format("%s.%s", prefix, name); + } }