key
key copied to clipboard
KeYProject
SMT Translation naming conflicts
Description
The SMT translation names a function parameter "length" to a function "length", which conflicts with the length function for objects.
Reproducible
always
Steps to reproduce
- Load example RemoveDuplicates, contract "arrayPart(int[], int)"
- SMT Preparation Macro
- Call any SMT solver
Expected SMT solver to launch and attempt to prove the goal. Actually SMT solvers do not start and fail with a handled exception.
Additional information
Exceptionde.uka.ilkd.key.util.parsing.BuildingException: You used the variable `length` like a predicate or function. at <unknown>:2:23
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.semanticError(AbstractBuilder.java:173)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitAccessterm(ExpressionBuilder.java:1490)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitAccessterm(ExpressionBuilder.java:57)
at de.uka.ilkd.key.nparser.KeYParser$AccesstermContext.accept(KeYParser.java:6585)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitPrimitive_term(KeYParserBaseVisitor.java:570)
at de.uka.ilkd.key.nparser.KeYParser$Primitive_termContext.accept(KeYParser.java:6472)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitPrimitive_labeled_term(ExpressionBuilder.java:923)
at de.uka.ilkd.key.nparser.KeYParser$Primitive_labeled_termContext.accept(KeYParser.java:6275)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitBracket_term(ExpressionBuilder.java:445)
at de.uka.ilkd.key.nparser.KeYParser$Bracket_termContext.accept(KeYParser.java:5925)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitAtom_prefix(KeYParserBaseVisitor.java:500)
at de.uka.ilkd.key.nparser.KeYParser$Atom_prefixContext.accept(KeYParser.java:5827)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitStrong_arith_term_2(ExpressionBuilder.java:400)
at de.uka.ilkd.key.nparser.KeYParser$Strong_arith_term_2Context.accept(KeYParser.java:5421)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitStrong_arith_term_1(ExpressionBuilder.java:379)
at de.uka.ilkd.key.nparser.KeYParser$Strong_arith_term_1Context.accept(KeYParser.java:5338)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitWeak_arith_term(ExpressionBuilder.java:336)
at de.uka.ilkd.key.nparser.KeYParser$Weak_arith_termContext.accept(KeYParser.java:5252)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitComparison_term(ExpressionBuilder.java:310)
at de.uka.ilkd.key.nparser.KeYParser$Comparison_termContext.accept(KeYParser.java:5153)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquality_term(ExpressionBuilder.java:299)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquality_term(ExpressionBuilder.java:57)
at de.uka.ilkd.key.nparser.KeYParser$Equality_termContext.accept(KeYParser.java:5074)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitTerm60(KeYParserBaseVisitor.java:409)
at de.uka.ilkd.key.nparser.KeYParser$Term60Context.accept(KeYParser.java:4840)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitQuantifierterm(ExpressionBuilder.java:1021)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitQuantifierterm(ExpressionBuilder.java:57)
at de.uka.ilkd.key.nparser.KeYParser$QuantifiertermContext.accept(KeYParser.java:4935)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitTerm60(KeYParserBaseVisitor.java:409)
at de.uka.ilkd.key.nparser.KeYParser$Term60Context.accept(KeYParser.java:4840)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:243)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:57)
at de.uka.ilkd.key.nparser.KeYParser$Conjunction_termContext.accept(KeYParser.java:4774)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:234)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:57)
at de.uka.ilkd.key.nparser.KeYParser$Disjunction_termContext.accept(KeYParser.java:4701)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:227)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:57)
at de.uka.ilkd.key.nparser.KeYParser$Implication_termContext.accept(KeYParser.java:4633)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:203)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:57)
at de.uka.ilkd.key.nparser.KeYParser$Equivalence_termContext.accept(KeYParser.java:4564)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:193)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:57)
at de.uka.ilkd.key.nparser.KeYParser$Elementary_update_termContext.accept(KeYParser.java:4497)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.lambda$mapOf$0(AbstractBuilder.java:122)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1625)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.mapOf(AbstractBuilder.java:122)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:178)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:57)
at de.uka.ilkd.key.nparser.KeYParser$Parallel_termContext.accept(KeYParser.java:4429)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitTerm(KeYParserBaseVisitor.java:360)
at de.uka.ilkd.key.nparser.KeYParser$TermContext.accept(KeYParser.java:4375)
at de.uka.ilkd.key.nparser.KeyAst.accept(KeyAst.java:50)
at de.uka.ilkd.key.nparser.KeyIO.parseExpression(KeyIO.java:97)
at de.uka.ilkd.key.parser.DefaultTermParser.parse(DefaultTermParser.java:69)
at de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler.handleDLAxioms(DefinedSymbolsHandler.java:251)
at de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler.introduceSymbol(DefinedSymbolsHandler.java:176)
at de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler.handle(DefinedSymbolsHandler.java:199)
at de.uka.ilkd.key.smt.newsmt2.MasterHandler.translate(MasterHandler.java:159)
at de.uka.ilkd.key.smt.newsmt2.MasterHandler.translate(MasterHandler.java:325)
at de.uka.ilkd.key.smt.newsmt2.MasterHandler.translate(MasterHandler.java:313)
at de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler.handle(IntegerOpHandler.java:101)
at de.uka.ilkd.key.smt.newsmt2.MasterHandler.translate(MasterHandler.java:146)
at de.uka.ilkd.key.smt.newsmt2.MasterHandler.translate(MasterHandler.java:189)
at de.uka.ilkd.key.smt.newsmt2.ModularSMTLib2Translator.makeSMTAsserts(ModularSMTLib2Translator.java:198)
at de.uka.ilkd.key.smt.newsmt2.ModularSMTLib2Translator.translateProblem(ModularSMTLib2Translator.java:121)
at de.uka.ilkd.key.smt.SMTSolverImplementation.translateToCommand(SMTSolverImplementation.java:343)
at de.uka.ilkd.key.smt.SMTSolverImplementation.run(SMTSolverImplementation.java:257)
- Commit: 9cc569c
Interesting observation! Thanks for reporting.
However, the problem is not SMT-related, but has to do with the fact that a local program variable length is created in the proof obligation while there is already a symbol length used in KeY (for array length). If you do a cut with length(a) = 0 you get a very similar error message.
I suppose a similar issue also occurs in the example "Lists with Loop Contracts" in the contract "mapIncrement_loopContract() normal behavior operation contract 0". Here there are two different variables present for "self". They are differentiated only by their hashcodes. Is this intended? It seems like this is still present on the main branch at time of writing.