diff --git a/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.css b/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.css index 75fd479a..f180fe26 100644 --- a/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.css +++ b/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.css @@ -59,6 +59,50 @@ padding: 0 !important; } +.condition-syntax-error { + display: flex; + flex-shrink: 0; + align-items: flex-start; + gap: 0.25rem; + margin-top: 0.25rem; + font-size: 0.75rem; + line-height: 1.2; + text-align: left; + overflow-wrap: anywhere; + color: var(--p-red-500, #ef4444); +} + +.condition-syntax-error .pi { + font-size: 0.75rem; + line-height: 1.2; +} + +.condition-form { + position: relative; +} + +.condition-syntax-error--floating { + position: absolute; + top: 100%; + left: 0; + right: 0; + z-index: 10; + pointer-events: none; + padding: 0.125rem 0.375rem; + background: var(--p-card-background, #ffffff); + border: 1px solid var(--p-textarea-invalid-border-color, #f87171); + border-radius: 0.375rem; + box-shadow: 0 2px 6px rgba(0, 0, 0, 0.12); +} + +.condition-syntax-error--floating span { + display: -webkit-box; + -webkit-box-orient: vertical; + -webkit-line-clamp: 4; + line-clamp: 4; + overflow: hidden; +} + .condition-dialog { } diff --git a/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.html b/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.html index 977dd94d..64d406a3 100644 --- a/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.html +++ b/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.html @@ -1,6 +1,6 @@
-
-
+
+ + @if (dialogSyntaxCheck.error(); as error) { + + + {{ error }} + + }
{ - let component: ConditionEditorComponent; - let fixture: ComponentFixture; +type Editor = ComponentFixture; + +describe("ConditionEditorComponent", () => { + let fixture: Editor; + let allEditors: Editor[]; + + const createEditor = (condition: BehaviorSubject): Editor => { + const editor = TestBed.createComponent(ConditionEditorComponent); + editor.componentRef.setInput("condition", condition); + editor.detectChanges(); + allEditors.push(editor); + return editor; + }; + + const setCondition = (text: string) => { + const condition = new BehaviorSubject(new Condition(text)); + fixture.componentRef.setInput("condition", condition); + fixture.detectChanges(); + return condition; + }; + + const type = (editor: Editor, text: string) => { + editor.componentInstance.onConditionChange(text); + allEditors.forEach((e) => e.detectChanges()); + }; + + const shownError = (editor: Editor = fixture): string | null => { + editor.detectChanges(); + return ( + editor.nativeElement + .querySelector(".condition-syntax-error") + ?.textContent.trim() ?? null + ); + }; + + const textareaIsInvalid = (): boolean => + fixture.nativeElement + .querySelector("textarea") + .classList.contains("p-invalid"); + + const leaveField = (editor: Editor) => + editor.nativeElement + .querySelector("textarea") + .dispatchEvent(new FocusEvent("focusout", { bubbles: true })); beforeEach(async () => { await TestBed.configureTestingModule({ imports: [ConditionEditorComponent], - providers: [provideHttpClient(),provideAnimations()] - }) - .compileComponents(); - + providers: [ + provideHttpClient(), + provideAnimations(), + { provide: GREEN_COLOURED_CONDITIONS, useValue: [] }, + { provide: RED_COLOURED_CONDITIONS, useValue: [] }, + ], + }).compileComponents(); + fixture = TestBed.createComponent(ConditionEditorComponent); - component = fixture.componentInstance; - component.condition.set(new Condition("")) - fixture.detectChanges(); + allEditors = [fixture]; + }); + + it("should create", () => { + setCondition(""); + expect(fixture.componentInstance).toBeTruthy(); + }); + + it("shows no error for an empty condition", () => { + setCondition(""); + expect(shownError()).toBeNull(); + expect(textareaIsInvalid()).toBeFalse(); + }); + + it("shows no error for a valid condition", () => { + setCondition("A.length > 0 && i == 0"); + expect(shownError()).toBeNull(); + expect(textareaIsInvalid()).toBeFalse(); + }); + + it("shows only the message of the error", () => { + setCondition("a > b c"); + expect(shownError()).toBe( + "Unexpected 'c', expected an operator or the end of the condition", + ); + }); + + it("shows the error of an invalid condition immediately after loading", () => { + setCondition("a > b c"); + expect(shownError()).not.toBeNull(); + expect(textareaIsInvalid()).toBeTrue(); }); - it('should create', () => { - expect(component).toBeTruthy(); + it("does not check the syntax if validation is disabled", () => { + fixture.componentRef.setInput("validateJml", false); + setCondition("i = i + 1;"); + expect(shownError()).toBeNull(); + expect(textareaIsInvalid()).toBeFalse(); }); + + it("shows the error of typed text after a pause", fakeAsync(() => { + setCondition(""); + type(fixture, "a >"); + expect(shownError()).toBeNull(); + + tick(SYNTAX_CHECK_DELAY_MS - 1); + expect(shownError()).toBeNull(); + + tick(1); + expect(shownError()).toBe( + "Unexpected end of condition, expected an expression", + ); + })); + + it("restarts the delay on each typed character", fakeAsync(() => { + setCondition(""); + type(fixture, "a >"); + tick(SYNTAX_CHECK_DELAY_MS - 100); + type(fixture, "a > ("); + tick(SYNTAX_CHECK_DELAY_MS - 100); + expect(shownError()).toBeNull(); + + tick(100); + expect(shownError()).toContain("expected an expression"); + })); + + it("removes the error immediately when the typed text is valid", fakeAsync(() => { + setCondition("a >"); + expect(shownError()).not.toBeNull(); + + type(fixture, "a > b"); + expect(shownError()).toBeNull(); + expect(textareaIsInvalid()).toBeFalse(); + })); + + it("shows the error immediately when leaving the field", fakeAsync(() => { + setCondition(""); + type(fixture, "a >"); + leaveField(fixture); + expect(shownError()).toContain("expected an expression"); + tick(SYNTAX_CHECK_DELAY_MS); + })); + + it("updates the condition when typing", () => { + const condition = setCondition(""); + type(fixture, "a > b"); + expect(condition.getValue().condition).toBe("a > b"); + }); + + it("does not react to clicks on the error message", () => { + setCondition("a >"); + fixture.detectChanges(); + const message = fixture.nativeElement.querySelector( + ".condition-syntax-error", + ); + expect(getComputedStyle(message).pointerEvents).toBe("none"); + }); + + for (const sharing of ["subject", "condition object"]) { + describe(`with a condition shared between editors by the ${sharing}`, () => { + let typingEditor: Editor; + let otherEditor: Editor; + + beforeEach(() => { + const condition = new Condition("i == 0"); + const subject = new BehaviorSubject(condition); + typingEditor = createEditor(subject); + otherEditor = createEditor( + sharing === "subject" + ? subject + : new BehaviorSubject(condition), + ); + }); + + it("shows the error of typed text in all editors after the same pause", fakeAsync(() => { + type(typingEditor, "i = 0"); + tick(SYNTAX_CHECK_DELAY_MS - 1); + expect(shownError(typingEditor)).toBeNull(); + expect(shownError(otherEditor)).toBeNull(); + + tick(1); + expect(shownError(typingEditor)).toContain("Assignment '='"); + expect(shownError(otherEditor)).toContain("Assignment '='"); + })); + + it("removes the error in all editors immediately when fixed", fakeAsync(() => { + type(typingEditor, "i = 0"); + tick(SYNTAX_CHECK_DELAY_MS); + type(typingEditor, "i == 0"); + expect(shownError(typingEditor)).toBeNull(); + expect(shownError(otherEditor)).toBeNull(); + })); + + it("shows the error in all editors immediately when leaving the field", fakeAsync(() => { + type(typingEditor, "i = 0"); + leaveField(typingEditor); + expect(shownError(typingEditor)).toContain("Assignment '='"); + expect(shownError(otherEditor)).toContain("Assignment '='"); + tick(SYNTAX_CHECK_DELAY_MS); + })); + + it("does not affect editors of other conditions when leaving the field", fakeAsync(() => { + const unrelatedEditor = createEditor( + new BehaviorSubject(new Condition("a > b")), + ); + type(unrelatedEditor, "a >"); + type(typingEditor, "i = 0"); + leaveField(typingEditor); + expect(shownError(unrelatedEditor)).toBeNull(); + tick(SYNTAX_CHECK_DELAY_MS); + expect(shownError(unrelatedEditor)).not.toBeNull(); + })); + }); + } }); diff --git a/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.ts b/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.ts index 1504b0b9..998aafdb 100644 --- a/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.ts +++ b/frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.ts @@ -1,5 +1,17 @@ -import { Component, EventEmitter, Input, Output, inject } from "@angular/core"; +import { + Component, + DoCheck, + EventEmitter, + Input, + OnChanges, + OnDestroy, + Output, + SimpleChanges, + inject, + signal, +} from "@angular/core"; import { Condition, ICondition } from "../../../../types/condition/condition"; +import { checkJmlSyntax } from "../../../../types/condition/jml-syntax-checker"; import { AiChatService } from "../../../../services/ai-chat/ai-chat.service"; import { Textarea } from "@openng/optimus-ui/textarea"; import { FloatLabelModule } from "@openng/optimus-ui/floatlabel"; @@ -9,11 +21,49 @@ import { } from "../../editor.component"; import { $dt } from "@openng/optimus-ui-themes"; import { FormsModule } from "@angular/forms"; -import { BehaviorSubject } from "rxjs"; +import { BehaviorSubject, Subject, filter } from "rxjs"; import { AsyncPipe } from "@angular/common"; import { Button } from "@openng/optimus-ui/button"; import { Dialog } from "@openng/optimus-ui/dialog"; +export const SYNTAX_CHECK_DELAY_MS = 2000; + +class ConditionSyntaxCheck { + public readonly error = signal(null); + private timeout?: ReturnType; + + constructor(private readonly isEnabled: () => boolean) {} + + public checkNow(text: string | undefined): void { + this.cancel(); + this.error.set(this.findError(text)); + } + + public checkDelayed(text: string | undefined): void { + this.cancel(); + const error = this.findError(text); + if (error === null) { + this.error.set(null); + } else { + this.timeout = setTimeout( + () => this.error.set(error), + SYNTAX_CHECK_DELAY_MS, + ); + } + } + + public cancel(): void { + clearTimeout(this.timeout); + } + + private findError(text: string | undefined): string | null { + if (!this.isEnabled() || !text) { + return null; + } + return checkJmlSyntax(text)?.message ?? null; + } +} + /** * Editor in the statements for the {@link Condition} * @link https://material.angular.io/components/form-field/overview @@ -26,7 +76,10 @@ import { Dialog } from "@openng/optimus-ui/dialog"; standalone: true, styleUrl: "./condition-editor.component.css", }) -export class ConditionEditorComponent { +export class ConditionEditorComponent implements OnChanges, DoCheck, OnDestroy { + private static nextId = 0; + private static readonly checkNowRequests = new Subject(); + private _aiChatService = inject(AiChatService); protected greenConditions = inject(GREEN_COLOURED_CONDITIONS); protected redConditions = inject(RED_COLOURED_CONDITIONS); @@ -43,6 +96,7 @@ export class ConditionEditorComponent { @Input() public editable: boolean | null = true; @Input() public inline = false; @Input() public showAiButton = false; + @Input() public validateJml = true; /** * Emitter to emit the condition @@ -54,11 +108,53 @@ export class ConditionEditorComponent { new EventEmitter(); protected dialogConditionText: string = ""; + protected readonly syntaxCheck = new ConditionSyntaxCheck( + () => this.validateJml, + ); + protected readonly dialogSyntaxCheck = new ConditionSyntaxCheck( + () => this.validateJml, + ); + protected readonly syntaxErrorId = `condition-syntax-error-${ConditionEditorComponent.nextId++}`; + private checkedText?: string; + private readonly checkNowSubscription = ConditionEditorComponent.checkNowRequests + .pipe(filter((condition) => condition === this.condition?.getValue())) + .subscribe(() => this.checkSyntaxNow()); + /** Inserted by Angular inject() migration for backwards compatibility */ constructor(...args: unknown[]); public constructor() {} + public ngOnChanges(changes: SimpleChanges): void { + if (changes["condition"] || changes["validateJml"]) { + this.checkSyntaxNow(); + } + } + + public ngDoCheck(): void { + const text = this.condition?.getValue()?.condition; + if (text !== this.checkedText) { + this.checkedText = text; + this.syntaxCheck.checkDelayed(text); + } + } + + public ngOnDestroy(): void { + this.checkNowSubscription.unsubscribe(); + this.syntaxCheck.cancel(); + this.dialogSyntaxCheck.cancel(); + } + + private checkSyntaxNow(): void { + this.checkedText = this.condition?.getValue()?.condition; + this.syntaxCheck.checkNow(this.checkedText); + } + + protected onEditingFinished(): void { + ConditionEditorComponent.checkNowRequests.next(this.condition.getValue()); + this.conditionEditingFinished.emit(); + } + /** * Function for sending the condition content to the ai chat * @see AiChatService @@ -105,15 +201,23 @@ export class ConditionEditorComponent { protected onEditConditionClick() { this.dialogConditionText = this.condition.getValue().condition; + this.dialogSyntaxCheck.checkNow(this.dialogConditionText); this.isDialogVisible = true; } + protected onDialogConditionChange(text: string) { + this.dialogConditionText = text; + this.dialogSyntaxCheck.checkDelayed(text); + } + protected onDialogDiscardClick() { this.isDialogVisible = false; } protected onDialogSaveClick() { this.onConditionChange(this.dialogConditionText); + ConditionEditorComponent.checkNowRequests.next(this.condition.getValue()); + this.dialogSyntaxCheck.cancel(); this.isDialogVisible = false; } } diff --git a/frontend/src/app/components/editor/statements/composition-statement/composition-statement.component.html b/frontend/src/app/components/editor/statements/composition-statement/composition-statement.component.html index ce79fc89..45905827 100644 --- a/frontend/src/app/components/editor/statements/composition-statement/composition-statement.component.html +++ b/frontend/src/app/components/editor/statements/composition-statement/composition-statement.component.html @@ -8,7 +8,7 @@ > } - +
} - +
diff --git a/frontend/src/app/components/editor/statements/composition-statement/composition-statement.component.ts b/frontend/src/app/components/editor/statements/composition-statement/composition-statement.component.ts index cbb4d210..0985eb19 100644 --- a/frontend/src/app/components/editor/statements/composition-statement/composition-statement.component.ts +++ b/frontend/src/app/components/editor/statements/composition-statement/composition-statement.component.ts @@ -1,6 +1,9 @@ import { Component, Input, OnInit, inject } from "@angular/core"; -import { StatementComponent } from "../statement/statement.component"; +import { + STATEMENT_BOTTOM_SPACE_PX, + StatementComponent, +} from "../statement/statement.component"; import { Refinement } from "../../../../types/refinement"; import { TreeService } from "../../../../services/tree/tree.service"; import { MatGridListModule } from "@angular/material/grid-list"; @@ -45,6 +48,7 @@ export class CompositionStatementComponent { @Input() public icon = "pi pi-circle"; @Input() _node!: CompositionStatementNode; + protected readonly bottomSpace = STATEMENT_BOTTOM_SPACE_PX; /** Inserted by Angular inject() migration for backwards compatibility */ constructor(...args: unknown[]); diff --git a/frontend/src/app/components/editor/statements/simple-statement/simple-statement.component.html b/frontend/src/app/components/editor/statements/simple-statement/simple-statement.component.html index 2d7a16a4..7c1c1a53 100644 --- a/frontend/src/app/components/editor/statements/simple-statement/simple-statement.component.html +++ b/frontend/src/app/components/editor/statements/simple-statement/simple-statement.component.html @@ -5,6 +5,7 @@ [editable]="true" placeholder="Statement" [showAiButton]="true" + [validateJml]="false" (textChanged)="onEditableContentChanged()" (synthesizeRequested)="synthesizeWithAi()"> diff --git a/frontend/src/app/components/editor/statements/statement/statement.component.css b/frontend/src/app/components/editor/statements/statement/statement.component.css index 168e3cd0..1d8c779a 100644 --- a/frontend/src/app/components/editor/statements/statement/statement.component.css +++ b/frontend/src/app/components/editor/statements/statement/statement.component.css @@ -43,6 +43,18 @@ border-right-width: 0; overflow: hidden; } +:host > p-card { + pointer-events: auto; +} + +:host ::ng-deep .mat-drawer-inner-container { + overflow: visible; +} +:host ::ng-deep .example-container:has(.mat-drawer-opened .condition-syntax-error--floating), +:host ::ng-deep .example-container:has(.mat-drawer-opened .condition-syntax-error--floating) .mat-drawer-opened { + overflow: visible; +} + .example-sidenav-content { display: flex; height: 100%; diff --git a/frontend/src/app/components/editor/statements/statement/statement.component.html b/frontend/src/app/components/editor/statements/statement/statement.component.html index 62fb38e4..b36e560f 100644 --- a/frontend/src/app/components/editor/statements/statement/statement.component.html +++ b/frontend/src/app/components/editor/statements/statement/statement.component.html @@ -7,7 +7,7 @@ } @if (!hideSourceHandle) { - + } { + describe("valid conditions", () => { + const exampleConditions = [ + "i > 7", + "appears(A, x, 0, A.length)", + "A[i] == x", + "appears(A, x, 0, A.length) && i == A.length-1", + "!appears(A,x,i+1,A.length) && (A[i] != x)", + "A[i]==x", + "i", + "(A[i] != x)", + "A != null", + "i >= 0 && i < A.length", + "maxe(A, 0, A.length, i)", + "A.length > 0 && i == 0 && j == 1", + "maxe(A,0,j,i) && (j!=A.length) && A[j] <= A[i]", + "A.length - j", + "true", + "newBalance == balance + x && newBalance >= limit", + "containsOldElements(A, \\old(A)) && sort(A)", + "partSort(A,i) && i < A.length && j == A.length-2", + "partSort(A,i) && (\\forall int h; (j < h && h < A.length ==> A[j+1] <= A[h])) && j>=i", + "partSort(A,i) && (\\forall int h; (j < h && h < A.length ==> A[j+1] <= A[h])) && j>=i & A[j] > A[j+1]", + "(\\forall int m; (0 <= m && m < A.length ==> (\\forall int n; (0 <= n && n < A.length ==> (m != n ==> A[m] != A[n])))))", + "(\\old(balance) + x >= limit ==> balance == \\old(balance) + x) && " + + "(\\old(balance) + x < limit ==> balance == \\old(balance))", + "i == \\old(i) + 1", + "newBalance == balance+x", + ]; + + for (const condition of exampleConditions) { + it(`accepts example condition '${condition}'`, () => { + expect(checkJmlSyntax(condition)).toBeNull(); + }); + } + + const otherValidConditions = [ + "a * b / c % d + e - f", + "a | b ^ c & d", + "a || b && c", + "a <=> b", + "a ==> b ==> c", + "-a < ~b", + "!!a", + "- -a", + "f()", + "f(g(a, h()), A[f(i)])", + "\\exists int k; (A[k] == x)", + "\\forall int k; (k > 0) && k2 > 0", + "this.x == 0", + "i == 2147483647", + "a\n&& b", + "\t a == b \r\n", + "_a1 == B_2", + ]; + + for (const condition of otherValidConditions) { + it(`accepts '${JSON.stringify(condition)}'`, () => { + expect(checkJmlSyntax(condition)).toBeNull(); + }); + } + + it("does not report empty conditions", () => { + expect(checkJmlSyntax("")).toBeNull(); + expect(checkJmlSyntax(" \n ")).toBeNull(); + expect(checkJmlSyntax(null)).toBeNull(); + expect(checkJmlSyntax(undefined)).toBeNull(); + }); + }); + + describe("invalid conditions", () => { + const invalidConditions: { + condition: string; + start: number; + end: number; + message: string; + }[] = [ + { + condition: "a = b", + start: 2, + end: 3, + message: + "Assignment '=' is not allowed in a condition, use '==' for equality", + }, + { + condition: "a <==> b", + start: 4, + end: 5, + message: + "Assignment '=' is not allowed in a condition, use '==' for equality", + }, + { + condition: "a => b", + start: 2, + end: 3, + message: + "Assignment '=' is not allowed in a condition, use '==' for equality", + }, + { + condition: "a # b", + start: 2, + end: 3, + message: "Invalid character '#'", + }, + { + condition: "a ? b : c", + start: 2, + end: 3, + message: "Invalid character '?'", + }, + { + condition: "\\result == 0", + start: 0, + end: 7, + message: + "Unknown JML keyword '\\result', expected one of \\forall, \\exists, \\old", + }, + { + condition: "a == \\", + start: 5, + end: 6, + message: + "Unknown JML keyword '\\', expected one of \\forall, \\exists, \\old", + }, + { + condition: "a >", + start: 3, + end: 3, + message: "Unexpected end of condition, expected an expression", + }, + { + condition: "(a > b", + start: 6, + end: 6, + message: "Unexpected end of condition, expected ')'", + }, + { + condition: "f(a", + start: 3, + end: 3, + message: "Unexpected end of condition, expected ',' or ')'", + }, + { + condition: "f(", + start: 2, + end: 2, + message: "Unexpected end of condition, expected an expression", + }, + { + condition: "A[i", + start: 3, + end: 3, + message: "Unexpected end of condition, expected ']'", + }, + { + condition: "A.", + start: 2, + end: 2, + message: "Unexpected end of condition, expected an identifier", + }, + { + condition: "a > b c", + start: 6, + end: 7, + message: + "Unexpected 'c', expected an operator or the end of the condition", + }, + { + condition: "a > b)", + start: 5, + end: 6, + message: + "Unexpected ')', expected an operator or the end of the condition", + }, + { + condition: "A[i].length > 0", + start: 4, + end: 5, + message: + "Unexpected '.', expected an operator or the end of the condition", + }, + { + condition: "a.b.c", + start: 3, + end: 4, + message: + "Unexpected '.', expected an operator or the end of the condition", + }, + { + condition: "A[i][j]", + start: 4, + end: 5, + message: + "Unexpected '[', expected an operator or the end of the condition", + }, + { + condition: "a ! b", + start: 2, + end: 3, + message: + "Unexpected '!', expected an operator or the end of the condition", + }, + { + condition: "1abc", + start: 1, + end: 4, + message: + "Unexpected 'abc', expected an operator or the end of the condition", + }, + { + condition: "a && && b", + start: 5, + end: 7, + message: "Unexpected '&&', expected an expression", + }, + { + condition: "()", + start: 1, + end: 2, + message: "Unexpected ')', expected an expression", + }, + { + condition: "int > 0", + start: 0, + end: 3, + message: "Unexpected 'int', expected an expression", + }, + { + condition: "f(a b)", + start: 4, + end: 5, + message: "Expected ',' or ')' but found 'b'", + }, + { + condition: "f(a,)", + start: 4, + end: 5, + message: "Unexpected ')', expected an expression", + }, + { + condition: "f(,a)", + start: 2, + end: 3, + message: "Unexpected ',', expected an expression", + }, + { + condition: "A[i)", + start: 3, + end: 4, + message: "Expected ']' but found ')'", + }, + { + condition: "A.0", + start: 2, + end: 3, + message: "Expected an identifier but found '0'", + }, + { + condition: "\\old(A[i])", + start: 6, + end: 7, + message: "Expected ')' but found '['", + }, + { + condition: "\\old(1)", + start: 5, + end: 6, + message: "Expected an identifier but found '1'", + }, + { + condition: "\\forall boolean b; (b)", + start: 8, + end: 15, + message: "Expected 'int' but found 'boolean'", + }, + { + condition: "\\forall int i (i > 0)", + start: 14, + end: 15, + message: "Expected ';' but found '('", + }, + { + condition: "\\forall int i; i > 0", + start: 15, + end: 16, + message: "Expected '(' but found 'i'", + }, + { + condition: "\\exists int i; 0 <= i; (A[i] == x)", + start: 15, + end: 16, + message: "Expected '(' but found '0'", + }, + { + condition: "(\\forall int i; (i > 0)", + start: 23, + end: 23, + message: "Unexpected end of condition, expected ')'", + }, + { + condition: "i == 2147483648", + start: 5, + end: 15, + message: "Number '2147483648' is too large, the maximum is 2147483647", + }, + ]; + + for (const { condition, start, end, message } of invalidConditions) { + it(`rejects '${condition}'`, () => { + expect(checkJmlSyntax(condition)).toEqual({ message, start, end }); + }); + } + + it("shortens long input in the message", () => { + expect(checkJmlSyntax("a > b abcdefghijklmnopqrstuvwxyz")).toEqual({ + message: + "Unexpected 'abcdefghijklmnopqrst…', expected an operator or the end of the condition", + start: 6, + end: 32, + }); + }); + + it("does not shorten input of the maximum length", () => { + expect(checkJmlSyntax("a > b abcdefghijklmnopqrst")!.message).toBe( + "Unexpected 'abcdefghijklmnopqrst', expected an operator or the end of the condition", + ); + }); + }); +}); diff --git a/frontend/src/app/types/condition/jml-syntax-checker.ts b/frontend/src/app/types/condition/jml-syntax-checker.ts new file mode 100644 index 00000000..4a3dcf4c --- /dev/null +++ b/frontend/src/app/types/condition/jml-syntax-checker.ts @@ -0,0 +1,366 @@ +export interface JmlSyntaxError { + message: string; + start: number; + end: number; +} + +type TokenKind = "identifier" | "keyword" | "number" | "operator" | "separator"; + +interface Token { + kind: TokenKind; + value: string; + start: number; + end: number; +} + +const BINARY_OPERATOR_PRECEDENCE: ReadonlyMap = new Map([ + ["*", 1], + ["/", 1], + ["%", 1], + ["+", 2], + ["-", 2], + ["<", 3], + ["<=", 3], + [">", 3], + [">=", 3], + ["==", 4], + ["!=", 4], + ["&", 5], + ["^", 6], + ["|", 7], + ["&&", 8], + ["||", 9], + ["==>", 10], + ["<=>", 10], +]); + +const MAX_PRECEDENCE = Math.max(...BINARY_OPERATOR_PRECEDENCE.values()); + +const JML_KEYWORDS: readonly string[] = ["\\forall", "\\exists", "\\old"]; + +const KEYWORDS: readonly string[] = ["int"]; + +const SEPARATORS: readonly string[] = ["(", ")", ".", "[", "]", ";", ","]; + +const SINGLE_CHAR_OPERATORS: readonly string[] = [ + "+", + "-", + "*", + "/", + "%", + "~", + "^", +]; + +const WHITESPACE: readonly string[] = [" ", "\t", "\r", "\n"]; + +const MAX_INT_LITERAL = 2147483647; + +const MAX_QUOTED_LENGTH = 20; + +function quote(input: string): string { + return input.length > MAX_QUOTED_LENGTH + ? `'${input.substring(0, MAX_QUOTED_LENGTH)}…'` + : `'${input}'`; +} + +class JmlSyntaxException extends Error { + constructor( + message: string, + public readonly start: number, + public readonly end: number, + ) { + super(message); + } +} + +function isIdentifierChar(c: string): boolean { + return /^[0-9A-Za-z_]$/.test(c); +} + +function isDigit(c: string): boolean { + return /^[0-9]$/.test(c); +} + +function tokenize(source: string): Token[] { + const tokens: Token[] = []; + let pos = 0; + + const push = (kind: TokenKind, value: string) => { + tokens.push({ kind, value, start: pos, end: pos + value.length }); + pos += value.length; + }; + + const readWhile = (from: number, predicate: (c: string) => boolean) => { + let end = from; + while (end < source.length && predicate(source[end])) { + end++; + } + return source.substring(from, end); + }; + + while (pos < source.length) { + const c = source[pos]; + const next = source[pos + 1]; + const afterNext = source[pos + 2]; + + if (WHITESPACE.includes(c)) { + pos++; + } else if (SEPARATORS.includes(c)) { + push("separator", c); + } else if (SINGLE_CHAR_OPERATORS.includes(c)) { + push("operator", c); + } else if (c === "&" || c === "|") { + push("operator", next === c ? c + c : c); + } else if (c === "\\") { + const name = "\\" + readWhile(pos + 1, isIdentifierChar); + if (!JML_KEYWORDS.includes(name)) { + throw new JmlSyntaxException( + `Unknown JML keyword ${quote(name)}, expected one of ${JML_KEYWORDS.join(", ")}`, + pos, + pos + name.length, + ); + } + push("operator", name); + } else if (c === "<") { + push("operator", next === "=" ? (afterNext === ">" ? "<=>" : "<=") : "<"); + } else if (c === ">") { + push("operator", next === "=" ? ">=" : ">"); + } else if (c === "!") { + push("operator", next === "=" ? "!=" : "!"); + } else if (c === "=") { + if (next !== "=") { + throw new JmlSyntaxException( + "Assignment '=' is not allowed in a condition, use '==' for equality", + pos, + pos + 1, + ); + } + push("operator", afterNext === ">" ? "==>" : "=="); + } else if (isDigit(c)) { + push("number", readWhile(pos, isDigit)); + } else if (isIdentifierChar(c)) { + const name = readWhile(pos, isIdentifierChar); + push(KEYWORDS.includes(name) ? "keyword" : "identifier", name); + } else { + throw new JmlSyntaxException(`Invalid character '${c}'`, pos, pos + 1); + } + } + + return tokens; +} + +class ConditionSyntaxParser { + private idx = 0; + + constructor( + private readonly tokens: Token[], + private readonly sourceLength: number, + ) {} + + public parseCondition(): void { + this.parseExpression(); + if (this.hasMore()) { + const token = this.peek(); + throw this.errorAt( + token, + `Unexpected ${quote(token.value)}, expected an operator or the end of the condition`, + ); + } + } + + private parseExpression(): void { + this.parseExpressionWithPrecedence(MAX_PRECEDENCE); + } + + private parseExpressionWithPrecedence(precedence: number): void { + this.parseOperand(precedence); + while ( + this.hasMore() && + this.binaryPrecedence(this.peek()) === precedence + ) { + this.idx++; + this.parseOperand(precedence); + } + } + + private parseOperand(precedence: number): void { + if (precedence <= 1) { + this.parseFactor(); + } else { + this.parseExpressionWithPrecedence(precedence - 1); + } + } + + private parseFactor(): void { + const token = this.expectMore("an expression"); + + if (this.is(token, "separator", "(")) { + this.idx++; + this.parseExpression(); + this.expect("separator", ")"); + return; + } + + if ( + this.is(token, "operator", "-") || + this.is(token, "operator", "!") || + this.is(token, "operator", "~") + ) { + this.idx++; + this.parseFactor(); + return; + } + + if (this.is(token, "operator", "\\old")) { + this.idx++; + this.expect("separator", "("); + this.expectIdentifier(); + this.expect("separator", ")"); + return; + } + + if ( + this.is(token, "operator", "\\forall") || + this.is(token, "operator", "\\exists") + ) { + this.idx++; + this.expect("keyword", "int"); + this.expectIdentifier(); + this.expect("separator", ";"); + this.expect("separator", "("); + this.parseExpression(); + this.expect("separator", ")"); + return; + } + + if (token.kind === "identifier") { + this.idx++; + const following = this.hasMore() ? this.peek() : undefined; + if (following && this.is(following, "separator", "(")) { + this.parseCallArguments(); + } else if (following && this.is(following, "separator", "[")) { + this.idx++; + this.parseExpression(); + this.expect("separator", "]"); + } else if (following && this.is(following, "separator", ".")) { + this.idx++; + this.expectIdentifier(); + } + return; + } + + if (token.kind === "number") { + if (Number(token.value) > MAX_INT_LITERAL) { + throw this.errorAt( + token, + `Number ${quote(token.value)} is too large, the maximum is ${MAX_INT_LITERAL}`, + ); + } + this.idx++; + return; + } + + throw this.errorAt( + token, + `Unexpected ${quote(token.value)}, expected an expression`, + ); + } + + private parseCallArguments(): void { + this.expect("separator", "("); + if (this.hasMore() && this.is(this.peek(), "separator", ")")) { + this.idx++; + return; + } + while (true) { + this.parseExpression(); + const token = this.expectMore("',' or ')'"); + if (this.is(token, "separator", ")")) { + this.idx++; + return; + } + if (!this.is(token, "separator", ",")) { + throw this.errorAt( + token, + `Expected ',' or ')' but found ${quote(token.value)}`, + ); + } + this.idx++; + } + } + + private binaryPrecedence(token: Token): number | undefined { + return token.kind === "operator" + ? BINARY_OPERATOR_PRECEDENCE.get(token.value) + : undefined; + } + + private expect(kind: TokenKind, value: string): void { + const token = this.expectMore(`'${value}'`); + if (!this.is(token, kind, value)) { + throw this.errorAt( + token, + `Expected '${value}' but found ${quote(token.value)}`, + ); + } + this.idx++; + } + + private expectIdentifier(): void { + const token = this.expectMore("an identifier"); + if (token.kind !== "identifier") { + throw this.errorAt( + token, + `Expected an identifier but found ${quote(token.value)}`, + ); + } + this.idx++; + } + + private expectMore(expected: string): Token { + if (!this.hasMore()) { + throw new JmlSyntaxException( + `Unexpected end of condition, expected ${expected}`, + this.sourceLength, + this.sourceLength, + ); + } + return this.peek(); + } + + private is(token: Token, kind: TokenKind, value: string): boolean { + return token.kind === kind && token.value === value; + } + + private hasMore(): boolean { + return this.idx < this.tokens.length; + } + + private peek(): Token { + return this.tokens[this.idx]; + } + + private errorAt(token: Token, message: string): JmlSyntaxException { + return new JmlSyntaxException(message, token.start, token.end); + } +} + +export function checkJmlSyntax( + condition: string | null | undefined, +): JmlSyntaxError | null { + if (!condition || condition.trim() === "") { + return null; + } + + try { + const tokens = tokenize(condition); + new ConditionSyntaxParser(tokens, condition.length).parseCondition(); + return null; + } catch (e) { + if (e instanceof JmlSyntaxException) { + return { message: e.message, start: e.start, end: e.end }; + } + throw e; + } +} diff --git a/frontend/src/styles.css b/frontend/src/styles.css index bc1913be..7a409c4e 100644 --- a/frontend/src/styles.css +++ b/frontend/src/styles.css @@ -44,6 +44,10 @@ body { -moz-osx-font-smoothing: grayscale; } +.vflow-node > foreignObject { + pointer-events: none; +} + .conditionTileWidth { width: 270px; }