Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Introducing some structure for model method bodies #3571

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from
Draft

Introducing some structure for model method bodies #3571

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a312ab4
introducing model methods with bodies
mattulbrich Feb 23, 2025
d616f00
Allowing variables to be reassigned.
mattulbrich Feb 23, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 8 additions & 2 deletions key.core/src/main/antlr4/JmlLexer.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ lexer grammar JmlLexer;
// needed for double literals and ".."
private int _lex_pos;

private boolean parensEndExpr = false;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we reached a point in which we should rather rewrite the lexer w/o using modes for top-level and expr-mode.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wonder if these modes are really necessary in the lexer.

Yes one could name a variable "ensures", and write ensures ensures > 4;. But this is fully confusing.
I would be in favour of allowing backticks in these cases for turning keywords into identifiers.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As I did this, I came from the jmllang lexer/parser (Java+JML in ANTLR), where I used this heavily.

The advantage is, that the error messages are a little bit better. ("Expected identifier" vs "Expected identifier, ensures, requires, ... "). But the price is a complicated lexer.

I would now get rid of it, and introduce a grammar rule:

identifier: IDENTIFIER | MODEL | ENSURES | REQUIRES | ...;

I would keep modes for Strings & Co.

Do we not have (proposed) backticks for JavaDL escape of complete terms?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we not have (proposed) backticks for JavaDL escape of complete terms?

Maybe, don't know. Was that not (* ... *) ?

Actually I even actively avoid ensures ensures > 4; to be legal.
Escaping the identifier ensures seems like a natural thing to do.
Languages like SMT, SQL, ... have support for this, with explicit escapes.
(I had it in ivil, too. It was a simple addition to the parser.)

While it is a discussion worth having, it is beyond this PR that will have to accommodate to the current parser framework; and does so with not so much extra overhead.
(Just that an extra ")" leads back to toplevel mode if that is enabled -- this condition might probably even be dropped, but I wanted to be conservative.)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not so complicated: #3572

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Apparently we do not show these long "expected ....." lists anyway in our syntax error to string conversion anyway, so this may work well (eventually).


private int parenthesisLevel = 0;
private void incrParen() { parenthesisLevel++;}
private void decrParen() { parenthesisLevel--;}
Expand All @@ -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);
}
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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();};
Expand Down
10 changes: 8 additions & 2 deletions key.core/src/main/antlr4/JmlParser.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
4 changes: 2 additions & 2 deletions key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
39 changes: 36 additions & 3 deletions key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2346,7 +2346,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());
}

Expand All @@ -2363,15 +2363,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.");
Expand All @@ -2380,6 +2379,40 @@ 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, Term>> 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());
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What happens on a name clash?

var x = 1; var x = 2;

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah. This is currently allowed. You can write var x = 1; x = 2; which should be legal.

It would be nicer to ensure:

  1. If keyword "var" is present, no variable x must be in namespace
  2. If no keyword var is present, there is a variable x of compatible type present in the namespace.

It is not required technically, and everything is welldefined in either case. But it would violate Java principles.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Will add this.

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<LogicVariable, Term> 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) {
Expand Down
Loading