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

JmlLexer w/o expr mode #3572

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

JmlLexer w/o expr mode #3572

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
fa9ab56
JmlLexer w/o expr mode
wadoon Feb 27, 2025
2bf52d0
reformat
wadoon Feb 28, 2025
6312483
wip
wadoon Feb 28, 2025
6a9e8c0
fix precedence of statements
wadoon Feb 28, 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
140 changes: 49 additions & 91 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,106 +66,94 @@ 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';
//OLD: 'old';
//POST: 'post'Pred;
//PRE: 'pre' Pred;
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);
COLON: ':';
DOT: '.';
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;

/* Java keywords */
BOOLEAN: 'boolean';
BYTE: 'byte';
Expand All @@ -181,33 +169,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 Down Expand Up @@ -322,20 +285,16 @@ WORKINGSPACE: '\\working_space';

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

AND: '&';
BITWISENOT: '~';
COLON: ':';
COMMA: ',';
DIV: '/';
DOT: '.';
DOTDOT: '..';
EQUAL_SINGLE: '=';
EQV_ANTIV: '<==>' | '<=!=>';
EQ_NEQ: '==' | '!=';
EQUAL_SINGLE: '=';
GEQ: '>=';
IMPLIES: '==>';
IMPLIESBACKWARD: '<==';
Expand Down Expand Up @@ -368,8 +327,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 @@ -486,7 +444,7 @@ 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