Skip to content

JmlLexer w/o expr mode #3572

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

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

JmlLexer w/o expr mode #3572

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
7a540eb
JmlLexer w/o expr mode
wadoon Feb 27, 2025
b4cd111
implement backtick escape
wadoon Mar 15, 2025
8e36909
solve: \result is special in JML, do not quote these names
wadoon Mar 15, 2025
fc678fe
escape required in test case for instance
wadoon Mar 15, 2025
bd36fce
if assignable clause is given, but a Term wanted, return the locset-term
wadoon Mar 16, 2025
97c6c41
restore old precedences
wadoon Mar 17, 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
162 changes: 56 additions & 106 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 @@ -66,105 +66,82 @@ PUBLIC: 'public';
PURE: 'pure';
RETURN_BEHAVIOR: 'return_' BEHAVIOR;
FINAL: 'final';
MODEL: 'model'/* -> pushMode(expr)*/;
MODEL: 'model'/* */;

fragment Pred: '_redundantly'?; //suffix
fragment Pfree: '_free'?; //suffix

ACCESSIBLE: 'accessible' Pred -> pushMode(expr);
ASSERT: 'assert' Pred -> pushMode(expr);
ASSUME: 'assume' Pred -> pushMode(expr);
ACCESSIBLE: 'accessible' Pred;
ASSERT: 'assert' Pred;
ASSUME: 'assume' Pred;
/**
* The name 'assignable' is kept here for legacy reasons.
* Note that KeY does only verify what can be modified (i.e., what is 'modifiable').
*/
ASSIGNABLE
: ('assignable' | 'assigns' | 'assigning' |
'modifiable' | 'modifies' | 'modifying' |
'writable' | 'writes' | 'writing') (Pfree|Pred) -> pushMode(expr);
'writable' | 'writes' | 'writing') (Pfree|Pred);
/**
* The name 'assignable' is kept here for legacy reasons.
* Note that KeY does only verify what can be modified (i.e., what is 'modifiable').
*/
LOOP_ASSIGNABLE
: ('loop_assignable' | 'loop_assigns' | 'loop_assigning' |
'loop_modifiable' | 'loop_modifies' | 'loop_modifying' |
'loop_writable' | 'loop_writes' | 'loop_writing') (Pfree|Pred) -> pushMode(expr);
AXIOM: 'axiom' -> pushMode(expr);
BREAKS: 'breaks' -> pushMode(expr);
CAPTURES: 'captures' Pred -> pushMode(expr);
'loop_writable' | 'loop_writes' | 'loop_writing') (Pfree|Pred);
AXIOM: 'axiom';
BREAKS: 'breaks';
CAPTURES: 'captures' Pred;
CODE: 'code'; //?
CONSTRAINT: 'constraint' Pred -> pushMode(expr);
CONTINUES: 'continues' -> pushMode(expr);
CONSTRAINT: 'constraint' Pred;
CONTINUES: 'continues';
DEBUG: 'debug'; //?
DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred -> pushMode(expr);
DETERMINES: 'determines' -> pushMode(expr);
DIVERGES: 'diverges' Pred -> pushMode(expr);
//DURATION: 'duration' Pred -> pushMode(expr);
ENSURES: ('ensures' | 'post') (Pfree|Pred) -> pushMode(expr);
FOR_EXAMPLE: 'for_example' -> pushMode(expr);
//FORALL: 'forall' -> pushMode(expr); //?
DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred;
DETERMINES: 'determines';
DIVERGES: 'diverges' Pred;
DURATION: 'duration' Pred;
ENSURES: ('ensures' | 'post') (Pfree|Pred);
FOR_EXAMPLE: 'for_example';
//FORALL: 'forall'; //?
HELPER: 'helper';
IMPLIES_THAT: 'implies_that' -> pushMode(expr);
IN: 'in' Pred -> pushMode(expr);
INITIALLY: 'initially' -> pushMode(expr);
IMPLIES_THAT: 'implies_that';
IN: 'in' Pred;
INITIALLY: 'initially';
INSTANCE: 'instance';
INVARIANT: 'invariant' (Pfree|Pred) -> pushMode(expr);
INVARIANT: 'invariant' (Pfree|Pred);
LOOP_CONTRACT: 'loop_contract';
LOOP_INVARIANT: ('loop_invariant' | 'maintaining') (Pfree|Pred) -> pushMode(expr);
LOOP_INVARIANT: ('loop_invariant' | 'maintaining') (Pfree|Pred);
LOOP_DETERMINES: 'loop_determines'; // internal translation for 'determines' in loop invariants
LOOP_SEPARATES: 'loop_separates'; //KeY extension, deprecated
MAPS: 'maps' Pred -> pushMode(expr);
MEASURED_BY: 'measured_by' Pred -> pushMode(expr);
MAPS: 'maps' Pred;
MEASURED_BY: 'measured_by' Pred;
MERGE_POINT: 'merge_point';
MERGE_PROC: 'merge_proc';
MERGE_PARAMS: 'merge_params' -> pushMode(expr);
MONITORED: 'monitored' -> pushMode(expr);
MONITORS_FOR: 'monitors_for' -> pushMode(expr);
//OLD: 'old' -> pushMode(expr);
//POST: 'post'Pred -> pushMode(expr);
//PRE: 'pre' Pred -> pushMode(expr);
MERGE_PARAMS: 'merge_params';
MONITORED: 'monitored';
MONITORS_FOR: 'monitors_for';
READABLE: 'readable';
REPRESENTS: 'represents' Pred -> pushMode(expr);
REQUIRES: ('requires'| 'pre') (Pfree|Pred) -> pushMode(expr);
RETURN: 'return' -> pushMode(expr);
RETURNS: 'returns' -> pushMode(expr);
RESPECTS: 'respects' -> pushMode(expr);
SEPARATES: 'separates' -> pushMode(expr);
SET: 'set' -> pushMode(expr);
SIGNALS: ('signals' Pred | 'exsures' Pred) -> pushMode(expr);
SIGNALS_ONLY: 'signals_only' Pred -> pushMode(expr);
WHEN: 'when' Pred -> pushMode(expr);
WORKING_SPACE: 'working_space' Pred -> pushMode(expr);
WRITABLE: 'writable' -> pushMode(expr);

REPRESENTS: 'represents' Pred;
REQUIRES: ('requires'| 'pre') (Pfree|Pred);
RETURN: 'return';
RETURNS: 'returns';
RESPECTS: 'respects';
SEPARATES: 'separates';
SET: 'set';
SIGNALS: ('signals' Pred | 'exsures' Pred);
SIGNALS_ONLY: 'signals_only' Pred;
WHEN: 'when' Pred;
WORKING_SPACE: 'working_space' Pred;
WRITABLE: 'writable';
JML_ML_END: '*/' -> channel(HIDDEN);
WS: (' ' | '\t' | '\n' | '\r' | '@')+ -> channel(HIDDEN);
NEST_START: '{|' ;
NEST_END: '|}' ;
C_RBRACKET: ']' -> type(RBRACKET);
C_LBRACKET: '[' -> type(LBRACKET);
SEMICOLON : ';' -> type(SEMI_TOPLEVEL);
C_LBRACE: '{' -> type(LBRACE);
C_RBRACE: '}' -> type(RBRACE);
C_EQUAL: '=' -> type(EQUAL_SINGLE), pushMode(expr);
C_LPAREN: '(' -> type(LPAREN);
C_RPAREN: ')' -> type(RPAREN);
C_STRING_LITERAL: '"' -> pushMode(string), more;
C_IDENT: '\\'? LETTER (LETTERORDIGIT)* -> type(IDENT);
C_COLON: ':' -> type(COLON);
C_DOT: '.' -> type(DOT);
C_COMMA: ',' -> type(COMMA);

SL_COMMENT: {jmlMarkerDecision.isComment("//")}? ('//' ('\n'|'\r'|EOF) | '//' ~'@' ~('\n'|'\r')*) -> channel(HIDDEN);
ML_COMMENT: {jmlMarkerDecision.isComment("/*")}? '/*' -> more, pushMode(mlComment);

JML_SL_START: {!jmlMarkerDecision.isComment("//")}? '//' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN);
JML_ML_START: {!jmlMarkerDecision.isComment("/*")}?'/*' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN);

ERROR_CHAR: .;

mode expr;
COLON: ':';
DOT: '.';
COMMA: ',';

/* Java keywords */
BOOLEAN: 'boolean';
Expand All @@ -181,33 +158,8 @@ THIS: 'this';
TRUE: 'true';
VOID: 'void';

E_NULLABLE: 'nullable'->type(NULLABLE);
E_NONNULL: 'non_null' -> type(NON_NULL);


DEPENDS: 'depends'; // internal translation for 'accessible' on model fields

/* JML and JML* keywords */
/*ACCESSIBLE: 'accessible';
MODIFIABLE: 'modifiable';
BREAKS: 'breaks';
CONTINUES: 'continues';
DECREASES: 'decreases'; // internal translation for 'measured_by'
DETERMINES: 'determines'; //KeY extension, not official JML
ENSURES: 'ensures';
ENSURES_FREE: 'ensures_free';
MODEL_METHOD_AXIOM: 'model_method_axiom'; //KeY extension, not official JML
MERGE_PARAMS: 'merge_params'; //KeY extension, not official JML
NON_NULL: 'non_null';
NULLABLE: 'nullable';
REPRESENTS: 'represents';
REQUIRES: 'requires';
REQUIRES_FREE: 'requires_free';
RETURNS: 'returns'; //KeY extension, not official JML
SEPARATES: 'separates'; //KeY extension, not official JML
SIGNALS: 'signals';
SIGNALS_ONLY: 'signals_only';*/

/* JML keywords prefixed with a backslash */
ALLFIELDS: '\\all_fields'; //KeY extension, not official JML
ALLOBJECTS: '\\all_objects'; //KeY extension, not official JML
Expand All @@ -219,7 +171,7 @@ BY: '\\by'; //KeY extension, not official JML
DECLASSIFIES: '\\declassifies'; //KeY extension, not official JML
DISJOINT: '\\disjoint'; //KeY extension, not official JML
DOMAIN_IMPLIES_CREATED: '\\domain_implies_created'; //KeY extension, not official JML
DURATION: '\\duration';
ESC_DURATION: '\\duration';
ELEMTYPE: '\\elemtype';
EMPTYSET: '\\empty';
ERASES: '\\erases'; //KeY extension, not official JML
Expand Down Expand Up @@ -320,22 +272,19 @@ WORKINGSPACE: '\\working_space';
// ONLY_CALLED: '\\only_called';
// ONLY_CAPTURED: '\\only_captured';

E_JML_SL_START: '//@' -> type(JML_SL_START), channel(HIDDEN);
E_JML_ML_START: '/*@' -> type(JML_ML_START), channel(HIDDEN);
E_JML_ML_END: '*/' -> channel(HIDDEN);
E_SL_COMMENT: {jmlMarkerDecision.isComment("//")}? ('//' ('\n'|'\r'|EOF) | '//' ~'@' ~('\n'|'\r')*) -> type(COMMENT), channel(HIDDEN);
E_ML_COMMENT: {jmlMarkerDecision.isComment("/*")}? '/*' -> more, pushMode(mlComment);
SL_COMMENT: {jmlMarkerDecision.isComment("//")}? ('//' ('\n'|'\r'|EOF) | '//' ~'@' ~('\n'|'\r')*) -> channel(HIDDEN);
ML_COMMENT: {jmlMarkerDecision.isComment("/*")}? '/*' -> more, pushMode(mlComment);

JML_SL_START: {!jmlMarkerDecision.isComment("//")}? '//' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN);
JML_ML_START: {!jmlMarkerDecision.isComment("/*")}?'/*' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN);

AND: '&';
BITWISENOT: '~';
COLON: ':';
COMMA: ',';
DIV: '/';
DOT: '.';
DOTDOT: '..';
EQUAL_SINGLE: '=';
EQV_ANTIV: '<==>' | '<=!=>';
EQ_NEQ: '==' | '!=';
EQUAL_SINGLE: '=';
GEQ: '>=';
IMPLIES: '==>';
IMPLIESBACKWARD: '<==';
Expand Down Expand Up @@ -368,8 +317,7 @@ LBRACE: '{' {incrBrace();};
RBRACE: '}' {decrBrace();};
LBRACKET: '[' {incrBracket();};
RBRACKET: ']' {decrBracket();};
SEMI_TOPLEVEL: { semicolonOnToplevel()}? ';' -> popMode; //jump back to contract mode
SEMI: { ! semicolonOnToplevel()}? ';';
SEMI: ';';

fragment LETTER: 'a'..'z' | 'A'..'Z' | '_' | '$';

Expand Down Expand Up @@ -446,10 +394,13 @@ DOUBLE_LITERAL
fragment
LETTERORDIGIT: LETTER | DIGIT;

ESCAPED_IDENTIFIER: '`' IDENT '`' -> type(IDENT);
IDENT: LETTER (LETTERORDIGIT)*;
JML_IDENT: '\\' IDENT ;
JML_IDENT: '\\' IDENT;
JML_ESCAPED_IDENT: '`' JML_IDENT '`' -> type(JML_IDENT);
SPECIAL_IDENT: '<'IDENT'>';


//DL_ESCAPE: '\\dl_' LETTER ( LETTERORDIGIT )* ;

/*
Expand Down Expand Up @@ -483,10 +434,9 @@ STRING_LITERAL: '"' -> pushMode(string),more;
E_WS: [ \t\n\r\u000c@]+ -> channel(HIDDEN), type(WS);
INFORMAL_DESCRIPTION: '(*' ( '*' ~')' | ~'*' )* '*)';

DOC_COMMENT: '/**' -> pushMode(mlComment);
fragment PRAGMA: '\\nowarn';

E_ERROR_CHAR: . -> type(ERROR_CHAR);
ERROR_CHAR: .;

mode mlComment;
ML_COMMENT_END: ('*/'|EOF) -> type(COMMENT), channel(HIDDEN), popMode;
Expand Down
Loading
Loading