From a312ab4b5ab4b9f49f4c8f6ff9c834a571535deb Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 23 Feb 2025 22:41:52 +0100 Subject: [PATCH 1/2] introducing model methods with bodies restricted to ifs and intermediate variables --- key.core/src/main/antlr4/JmlLexer.g4 | 10 ++++- key.core/src/main/antlr4/JmlParser.g4 | 10 ++++- .../jml/translation/JMLSpecFactory.java | 2 +- .../ilkd/key/speclang/njml/Translator.java | 39 +++++++++++++++++-- 4 files changed, 53 insertions(+), 8 deletions(-) diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index a8594d8bbf4..8b4eb5880cb 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -7,6 +7,8 @@ lexer grammar JmlLexer; // needed for double literals and ".." private int _lex_pos; + private boolean parensEndExpr = false; + private int parenthesisLevel = 0; private void incrParen() { parenthesisLevel++;} private void decrParen() { parenthesisLevel--;} @@ -20,6 +22,7 @@ lexer grammar JmlLexer; private void decrBracket() { bracketLevel--;} boolean semicolonOnToplevel() { return bracketLevel==0 && bracesLevel == 0 && parenthesisLevel==0; } + boolean parensEnd() { return parenthesisLevel == 1 && parensEndExpr; } private JmlMarkerDecision jmlMarkerDecision = new JmlMarkerDecision(this); } @@ -101,10 +104,12 @@ DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred -> pushMode(expr) DETERMINES: 'determines' -> pushMode(expr); DIVERGES: 'diverges' Pred -> pushMode(expr); //DURATION: 'duration' Pred -> pushMode(expr); +ELSE: 'else'; ENSURES: ('ensures' | 'post') (Pfree|Pred) -> pushMode(expr); FOR_EXAMPLE: 'for_example' -> pushMode(expr); //FORALL: 'forall' -> pushMode(expr); //? HELPER: 'helper'; +IF: 'if' { parensEndExpr = true; } -> pushMode(expr); IMPLIES_THAT: 'implies_that' -> pushMode(expr); IN: 'in' Pred -> pushMode(expr); INITIALLY: 'initially' -> pushMode(expr); @@ -134,6 +139,7 @@ SEPARATES: 'separates' -> pushMode(expr); SET: 'set' -> pushMode(expr); SIGNALS: ('signals' Pred | 'exsures' Pred) -> pushMode(expr); SIGNALS_ONLY: 'signals_only' Pred -> pushMode(expr); +VAR: 'var'; WHEN: 'when' Pred -> pushMode(expr); WORKING_SPACE: 'working_space' Pred -> pushMode(expr); WRITABLE: 'writable' -> pushMode(expr); @@ -361,9 +367,9 @@ XOR: '^'; GT: '>'; LT: '<'; - LPAREN: '(' {incrParen();}; -RPAREN: ')' {decrParen();}; +RPAREN_TOPLEVEL: { parensEnd() }? ')' { decrParen(); parensEndExpr = false; } -> type(RPAREN), popMode; +RPAREN: { ! parensEnd() }? ')' { decrParen(); }; LBRACE: '{' {incrBrace();}; RBRACE: '}' {decrBrace();}; LBRACKET: '[' {incrBracket();}; diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index 40f27ec6acc..5d4874c3ad9 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -152,8 +152,14 @@ name_clause: SPEC_NAME STRING_LITERAL SEMICOLON ; //old_clause: OLD modifiers type IDENT INITIALISER ; field_declaration: typespec IDENT (LBRACKET RBRACKET)* initialiser? SEMI_TOPLEVEL; -method_declaration: typespec IDENT param_list (method_body|SEMI_TOPLEVEL); -method_body: LBRACE RETURN expression SEMI_TOPLEVEL RBRACE; +method_declaration: typespec IDENT param_list (method_body=mbody_block | SEMI_TOPLEVEL); +mbody_block: LBRACE mbody_var* mbody_statement RBRACE; +mbody_statement: + RETURN expression SEMI_TOPLEVEL #mbody_return + | IF LPAREN expression RPAREN (mbody_statement | mbody_block) ELSE (mbody_statement | mbody_block) #mbody_if + ; +mbody_var: VAR IDENT EQUAL_SINGLE expression SEMI_TOPLEVEL; + param_list: LPAREN (param_decl (COMMA param_decl)*)? RPAREN; param_decl: ((NON_NULL | NULLABLE))? typespec p=IDENT (LBRACKET RBRACKET)*; history_constraint: CONSTRAINT expression; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index 008a050ccf7..248fe9f1f38 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -483,7 +483,7 @@ private void translateAxioms(Context context, ProgramVariableCollection progVars || (axioms.size() == 1 // or the first element is an empty method_decl && axioms.head().first instanceof JmlParser.Method_declarationContext && ((JmlParser.Method_declarationContext) axioms.head().first) - .method_body() == null); + .method_body == null); if (empty) { clauses.axioms.put(heap, null); } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java index a391d7e343d..a52b51399f9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java @@ -38,6 +38,7 @@ import de.uka.ilkd.key.util.mergerule.MergeParamsSpec; import de.uka.ilkd.key.util.parsing.BuildingException; +import org.antlr.v4.runtime.RuleContext; import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableList; @@ -2346,7 +2347,7 @@ public Object visitField_declaration(JmlParser.Field_declarationContext ctx) { @Override public SLExpression visitMethod_declaration(JmlParser.Method_declarationContext ctx) { - if (ctx.method_body() == null) { + if (ctx.method_body == null) { return new SLExpression(tb.tt()); } @@ -2363,7 +2364,7 @@ public SLExpression visitMethod_declaration(JmlParser.Method_declarationContext ParserRuleContext equal = JmlFacade.parseExpr(ctx.IDENT() + paramsString); Object a = accept(equal); - SLExpression body = accept(ctx.method_body().expression()); + SLExpression body = accept(ctx.method_body); SLParameters params = visitParameters(ctx.param_list()); SLExpression apply = lookupIdentifier(ctx.IDENT().getText(), null, params, ctx); @@ -2371,7 +2372,6 @@ public SLExpression visitMethod_declaration(JmlParser.Method_declarationContext boolean applyContainsHeap = TermUtil.contains(apply.getTerm(), forbiddenHeapVar); boolean bodyContainsHeap = TermUtil.contains(body.getTerm(), forbiddenHeapVar); - if (!applyContainsHeap && bodyContainsHeap) { // NOT (no heap in applies --> no heap in body) raiseError(ctx, "Heap used in a `no_state` method."); @@ -2380,6 +2380,39 @@ public SLExpression visitMethod_declaration(JmlParser.Method_declarationContext return termFactory.eq(apply, body); } + @Override + public SLExpression visitMbody_return(JmlParser.Mbody_returnContext ctx) { + return accept(ctx.expression()); + } + + @Override + public SLExpression visitMbody_block(JmlParser.Mbody_blockContext ctx) { + resolverManager.pushLocalVariablesNamespace(); + List> substList = new ArrayList<>(); + for (JmlParser.Mbody_varContext varCtx : ctx.mbody_var()) { + String name = varCtx.IDENT().getText(); + SLExpression expr = accept(varCtx.expression()); + Term term = expr.getTerm(); + LogicVariable logVar = new LogicVariable(new Name(name), term.sort()); + substList.add(new Pair<>(logVar, term)); + resolverManager.putIntoTopLocalVariablesNamespace(ImmutableList.of(logVar), javaInfo.getKeYJavaType(term.sort())); + } + SLExpression stmExpr = accept(ctx.mbody_statement()); + Term term = stmExpr.getTerm(); + for (Pair lv : substList.reversed()) { + term = tb.subst(lv.first, lv.second, term); + } + resolverManager.popLocalVariablesNamespace(); + return new SLExpression(term); + } + + @Override + public SLExpression visitMbody_if(JmlParser.Mbody_ifContext ctx) { + SLExpression cond = accept(ctx.getChild(ParserRuleContext.class, 0)); + SLExpression then = accept(ctx.getChild(ParserRuleContext.class, 1)); + SLExpression elze = accept(ctx.getChild(ParserRuleContext.class, 2)); + return new SLExpression(tb.ife(cond.getTerm(), then.getTerm(), elze.getTerm())); + } @Override public Object visitHistory_constraint(JmlParser.History_constraintContext ctx) { From d616f00447f0757307b6c414ce7828b46520f3d2 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 23 Feb 2025 22:59:38 +0100 Subject: [PATCH 2/2] Allowing variables to be reassigned. and spotlessing --- key.core/src/main/antlr4/JmlParser.g4 | 2 +- .../uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java | 4 ++-- .../main/java/de/uka/ilkd/key/speclang/njml/Translator.java | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index 5d4874c3ad9..0060642e03b 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -158,7 +158,7 @@ mbody_statement: RETURN expression SEMI_TOPLEVEL #mbody_return | IF LPAREN expression RPAREN (mbody_statement | mbody_block) ELSE (mbody_statement | mbody_block) #mbody_if ; -mbody_var: VAR IDENT EQUAL_SINGLE expression SEMI_TOPLEVEL; +mbody_var: VAR? IDENT EQUAL_SINGLE expression SEMI_TOPLEVEL; param_list: LPAREN (param_decl (COMMA param_decl)*)? RPAREN; param_decl: ((NON_NULL | NULLABLE))? typespec p=IDENT (LBRACKET RBRACKET)*; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index 248fe9f1f38..5b39c209d25 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -482,8 +482,8 @@ private void translateAxioms(Context context, ProgramVariableCollection progVars boolean empty = axioms.isEmpty() // either the list is empty || (axioms.size() == 1 // or the first element is an empty method_decl && axioms.head().first instanceof JmlParser.Method_declarationContext - && ((JmlParser.Method_declarationContext) axioms.head().first) - .method_body == null); + && ((JmlParser.Method_declarationContext) axioms + .head().first).method_body == null); if (empty) { clauses.axioms.put(heap, null); } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java index a52b51399f9..ab38663e580 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java @@ -38,7 +38,6 @@ import de.uka.ilkd.key.util.mergerule.MergeParamsSpec; import de.uka.ilkd.key.util.parsing.BuildingException; -import org.antlr.v4.runtime.RuleContext; import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableList; @@ -2395,7 +2394,8 @@ public SLExpression visitMbody_block(JmlParser.Mbody_blockContext ctx) { Term term = expr.getTerm(); LogicVariable logVar = new LogicVariable(new Name(name), term.sort()); substList.add(new Pair<>(logVar, term)); - resolverManager.putIntoTopLocalVariablesNamespace(ImmutableList.of(logVar), javaInfo.getKeYJavaType(term.sort())); + resolverManager.putIntoTopLocalVariablesNamespace(ImmutableList.of(logVar), + javaInfo.getKeYJavaType(term.sort())); } SLExpression stmExpr = accept(ctx.mbody_statement()); Term term = stmExpr.getTerm();