search

KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
48 stars 26 forks source link

SMT Translation naming conflicts #3455

Open BookWood7th opened 7 months ago

BookWood7th commented 7 months ago
## 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 1. Load example RemoveDuplicates, contract "arrayPart(int[], int)" 2. SMT Preparation Macro 3. 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 :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
mattulbrich commented 7 months ago

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.

BookWood7th commented 7 months ago

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.