Introducing some structure for model method bodies

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();};

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;

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java

@@ -486,8 +486,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 {

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java

@@ -2351,7 +2351,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());
         }
 
@@ -2368,15 +2368,14 @@ 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);
 
         var forbiddenHeapVar = services.getTypeConverter().getHeapLDT().getHeap();
         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.");
@@ -2385,6 +2384,60 @@ 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<Pair<LogicVariable, JTerm>> substList = new ArrayList<>();
+        for (JmlParser.Mbody_varContext varCtx : ctx.mbody_var()) {
+            String name = varCtx.IDENT().getText();
+            SLExpression expr = accept(varCtx.expression());
+            JTerm term = expr.getTerm();
+            LogicVariable logVar;
+            Optional<LogicVariable> existingVar = substList.stream()
+                    .map(p -> p.first)
+                    .filter(p -> p.name().toString().equals(name))
+                    .findAny();
+            if (varCtx.VAR() != null) {
+                existingVar.ifPresent(p -> {
+                    raiseError("Variable " + name + " already declared in this block.", ctx);
+                });
+                logVar = new LogicVariable(new Name(name), term.sort());
+                resolverManager.putIntoTopLocalVariablesNamespace(ImmutableList.of(logVar),
+                    javaInfo.getKeYJavaType(term.sort()));
+            } else {
+                logVar = existingVar.orElseThrow(() -> {
+                    raiseError("Assigned variable " + name + " unknown in this block.", varCtx);
+                    return new Error("Unreachable");
+                });
+                if (!term.sort().extendsTrans(logVar.sort())) {
+                    raiseError("Assignment to variable " + name + " with incompatible type.",
+                        varCtx);
+                }
+            }
+            substList.add(new Pair<>(logVar, term));
+        }
+
+        SLExpression stmExpr = accept(ctx.mbody_statement());
+        JTerm term = stmExpr.getTerm();
+        for (Pair<LogicVariable, JTerm> 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) {