diff --git a/.gitignore b/.gitignore index 4c14512b..0257b2c3 100644 --- a/.gitignore +++ b/.gitignore @@ -34,4 +34,9 @@ forge/pardinus-cli/out forge/pardinus-cli/classes *.icloud -*quotes_in_*filename.frg \ No newline at end of file +*quotes_in_*filename.frg + +# Node.js / Playwright e2e tests +forge/e2e/node_modules/ +forge/e2e/playwright-report/ +forge/e2e/test-results/ \ No newline at end of file diff --git a/e2e/README.md b/e2e/README.md deleted file mode 100644 index 62fb58cc..00000000 --- a/e2e/README.md +++ /dev/null @@ -1,5 +0,0 @@ -# Forge models for end-to-end testing - -These models aren't meant to illustrate any particular concept, but rather are used for -end-to-end testing of the Sterling<->Forge<->Solver workflow. They may use unusual syntax, -unsafe features, etc. diff --git a/e2e/fail_assertion.frg b/e2e/fail_assertion.frg deleted file mode 100644 index 4746a801..00000000 --- a/e2e/fail_assertion.frg +++ /dev/null @@ -1,16 +0,0 @@ -#lang forge - -option no_overflow true // disallow integer overflow - -sig Pigeon {location: one Pigeonhole} -sig Pigeonhole {} - -pred some_roommates { - some disj p1, p2: Pigeon | p1.location = p2.location -} --- This should pass; we don't expect Sterling to open at all. -assert {#Pigeon > #Pigeonhole} is sufficient for some_roommates --- This should fail; we expect Sterling to open with **only one command**, --- and for the instance to auto-load. **The evaluator should be usable**. -assert {#Pigeon >= #Pigeonhole} is sufficient for some_roommates - diff --git a/e2e/failing_decls_example.frg b/e2e/failing_decls_example.frg deleted file mode 100644 index b46455d3..00000000 --- a/e2e/failing_decls_example.frg +++ /dev/null @@ -1,21 +0,0 @@ -#lang forge - -option no_overflow true // disallow integer overflow - -sig Pigeon {location: one Pigeonhole} -sig Pigeonhole {} - -pred some_roommates { - some disj p1, p2: Pigeon | p1.location = p2.location -} - -// This fails because the instance given violates the type definitions -// The solver yields unsat, so Sterling should not open. -example threePigeons is {some_roommates} for { - Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2 - Pigeonhole = `Pigeonhole0 + `Pigeonhole1 - // This violates the type declarations: - location = `Pigeon0 -> (`Pigeonhole0 + `Pigeonhole1) + - `Pigeon1 -> `Pigeonhole0 + - `Pigeon2 -> `Pigeonhole0 -} diff --git a/e2e/failing_example.frg b/e2e/failing_example.frg deleted file mode 100644 index 15fa8c15..00000000 --- a/e2e/failing_example.frg +++ /dev/null @@ -1,19 +0,0 @@ -#lang forge - -option no_overflow true // disallow integer overflow - -sig Pigeon {location: one Pigeonhole} -sig Pigeonhole {} - -pred some_roommates { - some disj p1, p2: Pigeon | p1.location = p2.location -} - -// This fails. Since the solver has yielded unsat, Sterling shouldn't open. -example threePigeons is {not some_roommates} for { - Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2 - Pigeonhole = `Pigeonhole0 + `Pigeonhole1 - location = `Pigeon0 -> `Pigeonhole0 + - `Pigeon1 -> `Pigeonhole0 + - `Pigeon2 -> `Pigeonhole1 -} diff --git a/e2e/passing_example.frg b/e2e/passing_example.frg deleted file mode 100644 index c8f1c3d0..00000000 --- a/e2e/passing_example.frg +++ /dev/null @@ -1,18 +0,0 @@ -#lang forge - -option no_overflow true // disallow integer overflow - -sig Pigeon {location: one Pigeonhole} -sig Pigeonhole {} - -pred some_roommates { - some disj p1, p2: Pigeon | p1.location = p2.location -} - -example threePigeons is some_roommates for { - Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2 - Pigeonhole = `Pigeonhole0 + `Pigeonhole1 - location = `Pigeon0 -> `Pigeonhole0 + - `Pigeon1 -> `Pigeonhole0 + - `Pigeon2 -> `Pigeonhole1 -} diff --git a/e2e/sat_pass_unsat_pass_2_runs.frg b/e2e/sat_pass_unsat_pass_2_runs.frg deleted file mode 100644 index 9e18e9de..00000000 --- a/e2e/sat_pass_unsat_pass_2_runs.frg +++ /dev/null @@ -1,19 +0,0 @@ -#lang forge - -option no_overflow true // disallow integer overflow - -sig Pigeon {location: one Pigeonhole} -sig Pigeonhole {} - -pred some_roommates { - some disj p1, p2: Pigeon | p1.location = p2.location -} -test expect { - -- This is satisfiable, and so should appear in the run menu. - not_vacuous: {#Pigeon > #Pigeonhole} is sat - -- This is unsatisfiable, and so wouldn't be useful to visualize. - should_be_unsat: {Pigeon != Pigeon} is unsat -} - -see_principle_1: run {} for exactly 5 Pigeon, exactly 4 Pigeonhole -see_principle_2: run {} for exactly 4 Pigeon, exactly 3 Pigeonhole diff --git a/forge/e2e/README.md b/forge/e2e/README.md new file mode 100644 index 00000000..4139eec6 --- /dev/null +++ b/forge/e2e/README.md @@ -0,0 +1,39 @@ +# Forge E2E Tests + +End-to-end tests for Forge/Sterling integration using Playwright. + +## Setup + +```bash +cd e2e +npm install +npx playwright install # Install browser binaries +``` + +## Running Tests + +```bash +# Run all tests (headless) +npm test + +# Run tests with browser visible +npm run test:headed + +# Run tests in debug mode (step through) +npm run test:debug + +# Run tests with Playwright UI +npm run test:ui +``` + +## Test Structure + +- `fixtures/` - Forge files used as test inputs +- `helpers/` - Test utilities (Forge process runner, etc.) +- `tests/` - Playwright test specs + +## Notes + +- Tests run serially (single worker) to avoid port conflicts +- Each test spawns its own Forge process for isolation +- Timeout is set to 60s to allow for solver time diff --git a/forge/e2e/fixtures/multi-instance.frg b/forge/e2e/fixtures/multi-instance.frg new file mode 100644 index 00000000..ac04a9d2 --- /dev/null +++ b/forge/e2e/fixtures/multi-instance.frg @@ -0,0 +1,11 @@ +#lang forge + +-- Model that produces multiple distinct instances for testing navigation +sig Node { + edge: lone Node +} + +-- With 3 nodes and lone edge, we get many possible configurations +multiRun: run { + some edge +} for exactly 3 Node diff --git a/forge/e2e/fixtures/simple-graph.frg b/forge/e2e/fixtures/simple-graph.frg new file mode 100644 index 00000000..23dcdf98 --- /dev/null +++ b/forge/e2e/fixtures/simple-graph.frg @@ -0,0 +1,23 @@ +#lang forge + +-- Simple test model for e2e testing +sig Node { + edges: set Node +} + +pred connected { + all n1, n2: Node | n1 in n2.^edges or n2 in n1.^edges or n1 = n2 +} + +pred someEdges { + some edges +} + +simpleRun: run { + someEdges +} for exactly 3 Node + +connectedRun: run { + connected + someEdges +} for exactly 3 Node diff --git a/forge/e2e/fixtures/unsat-model.frg b/forge/e2e/fixtures/unsat-model.frg new file mode 100644 index 00000000..5e497713 --- /dev/null +++ b/forge/e2e/fixtures/unsat-model.frg @@ -0,0 +1,12 @@ +#lang forge + +-- Model with unsatisfiable constraints for testing unsat display +sig Node { + edges: set Node +} + +-- This is unsatisfiable: can't have exactly 3 nodes where each has no edges but some edges exist +unsatRun: run { + no edges + some edges +} for exactly 3 Node diff --git a/forge/e2e/helpers/forge-runner.ts b/forge/e2e/helpers/forge-runner.ts new file mode 100644 index 00000000..9f783e5a --- /dev/null +++ b/forge/e2e/helpers/forge-runner.ts @@ -0,0 +1,133 @@ +import { spawn, ChildProcess } from 'child_process'; +import * as path from 'path'; + +export interface ForgeInstance { + process: ChildProcess; + sterlingUrl: string; + staticPort: number; + providerPort: number; + cleanup: () => void; +} + +import { Page, expect } from '@playwright/test'; + +/** + * Helper to select and execute a run in Sterling. + * Sterling requires selecting from dropdown AND clicking "Run" button. + */ +export async function selectAndRunCommand(page: Page, runName: string): Promise { + // Select from the combobox + const runSelect = page.getByRole('combobox'); + await expect(runSelect).toBeVisible({ timeout: 10000 }); + await runSelect.selectOption({ label: runName }); + + // Click the Run button + const runButton = page.getByRole('button', { name: 'Run', exact: true }); + await expect(runButton).toBeVisible({ timeout: 5000 }); + await runButton.click(); + + // Wait for instance to load - SVG appears in main area + await expect(page.locator('svg').first()).toBeVisible({ timeout: 20000 }); +} + +/** + * Starts a Forge file and waits for Sterling to be ready. + * Returns the Sterling URL and a cleanup function. + */ +export async function startForge( + forgeFilePath: string, + options: { timeout?: number; providerPort?: number; staticPort?: number } = {} +): Promise { + const timeout = options.timeout ?? 30000; + const providerPort = options.providerPort ?? 18000 + Math.floor(Math.random() * 1000); + const staticPort = options.staticPort ?? 19000 + Math.floor(Math.random() * 1000); + const forgePath = path.resolve(__dirname, '../../', forgeFilePath); + + return new Promise((resolve, reject) => { + // Pass options for headless mode with known ports + const proc = spawn( + 'racket', + [ + forgePath, + '-O', 'run_sterling', 'headless', + '-O', 'sterling_port', String(providerPort), + '-O', 'sterling_static_port', String(staticPort), + ], + { + cwd: path.resolve(__dirname, '../..'), + stdio: ['pipe', 'pipe', 'pipe'], + } + ); + + let stdout = ''; + let stderr = ''; + let resolved = false; + + const timeoutId = setTimeout(() => { + if (!resolved) { + resolved = true; + proc.kill(); + reject(new Error(`Timeout waiting for Sterling to start. stdout: ${stdout}, stderr: ${stderr}`)); + } + }, timeout); + + proc.stdout?.on('data', (data: Buffer) => { + const chunk = data.toString(); + stdout += chunk; + + // Look for: "Opening Forge menu in Sterling (static server port=XXXX)" + // This confirms the server is ready (we already know the port) + const serverReady = stdout.includes('static server port='); + + if (serverReady && !resolved) { + // Wait a moment for the server to be fully ready + setTimeout(() => { + if (!resolved) { + resolved = true; + clearTimeout(timeoutId); + + const sterlingUrl = `http://127.0.0.1:${staticPort}/?${providerPort}`; + + resolve({ + process: proc, + sterlingUrl, + staticPort, + providerPort, + cleanup: () => { + // Send newline to stdin to trigger Forge shutdown + proc.stdin?.write('\n'); + proc.stdin?.end(); + // Force kill after a short delay if still running + setTimeout(() => { + if (!proc.killed) { + proc.kill('SIGKILL'); + } + }, 2000); + }, + }); + } + }, 500); + } + }); + + proc.stderr?.on('data', (data: Buffer) => { + stderr += data.toString(); + }); + + proc.on('error', (err) => { + if (!resolved) { + resolved = true; + clearTimeout(timeoutId); + reject(new Error(`Failed to start Forge: ${err.message}`)); + } + }); + + proc.on('exit', (code) => { + if (!resolved) { + resolved = true; + clearTimeout(timeoutId); + reject(new Error(`Forge exited unexpectedly with code ${code}. stdout: ${stdout}, stderr: ${stderr}`)); + } + }); + }); +} diff --git a/forge/e2e/package-lock.json b/forge/e2e/package-lock.json new file mode 100644 index 00000000..7c08a611 --- /dev/null +++ b/forge/e2e/package-lock.json @@ -0,0 +1,111 @@ +{ + "name": "forge-e2e", + "version": "1.0.0", + "lockfileVersion": 3, + "requires": true, + "packages": { + "": { + "name": "forge-e2e", + "version": "1.0.0", + "devDependencies": { + "@playwright/test": "^1.40.0", + "@types/node": "^20.10.0", + "typescript": "^5.3.0" + } + }, + "node_modules/@playwright/test": { + "version": "1.57.0", + "resolved": "https://registry.npmjs.org/@playwright/test/-/test-1.57.0.tgz", + "integrity": "sha512-6TyEnHgd6SArQO8UO2OMTxshln3QMWBtPGrOCgs3wVEmQmwyuNtB10IZMfmYDE0riwNR1cu4q+pPcxMVtaG3TA==", + "dev": true, + "license": "Apache-2.0", + "dependencies": { + "playwright": "1.57.0" + }, + "bin": { + "playwright": "cli.js" + }, + "engines": { + "node": ">=18" + } + }, + "node_modules/@types/node": { + "version": "20.19.30", + "resolved": "https://registry.npmjs.org/@types/node/-/node-20.19.30.tgz", + "integrity": "sha512-WJtwWJu7UdlvzEAUm484QNg5eAoq5QR08KDNx7g45Usrs2NtOPiX8ugDqmKdXkyL03rBqU5dYNYVQetEpBHq2g==", + "dev": true, + "license": "MIT", + "dependencies": { + "undici-types": "~6.21.0" + } + }, + "node_modules/fsevents": { + "version": "2.3.2", + "resolved": "https://registry.npmjs.org/fsevents/-/fsevents-2.3.2.tgz", + "integrity": "sha512-xiqMQR4xAeHTuB9uWm+fFRcIOgKBMiOBP+eXiyT7jsgVCq1bkVygt00oASowB7EdtpOHaaPgKt812P9ab+DDKA==", + "dev": true, + "hasInstallScript": true, + "license": "MIT", + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": "^8.16.0 || ^10.6.0 || >=11.0.0" + } + }, + "node_modules/playwright": { + "version": "1.57.0", + "resolved": "https://registry.npmjs.org/playwright/-/playwright-1.57.0.tgz", + "integrity": "sha512-ilYQj1s8sr2ppEJ2YVadYBN0Mb3mdo9J0wQ+UuDhzYqURwSoW4n1Xs5vs7ORwgDGmyEh33tRMeS8KhdkMoLXQw==", + "dev": true, + "license": "Apache-2.0", + "dependencies": { + "playwright-core": "1.57.0" + }, + "bin": { + "playwright": "cli.js" + }, + "engines": { + "node": ">=18" + }, + "optionalDependencies": { + "fsevents": "2.3.2" + } + }, + "node_modules/playwright-core": { + "version": "1.57.0", + "resolved": "https://registry.npmjs.org/playwright-core/-/playwright-core-1.57.0.tgz", + "integrity": "sha512-agTcKlMw/mjBWOnD6kFZttAAGHgi/Nw0CZ2o6JqWSbMlI219lAFLZZCyqByTsvVAJq5XA5H8cA6PrvBRpBWEuQ==", + "dev": true, + "license": "Apache-2.0", + "bin": { + "playwright-core": "cli.js" + }, + "engines": { + "node": ">=18" + } + }, + "node_modules/typescript": { + "version": "5.9.3", + "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.9.3.tgz", + "integrity": "sha512-jl1vZzPDinLr9eUt3J/t7V6FgNEw9QjvBPdysz9KfQDD41fQrC2Y4vKQdiaUpFT4bXlb1RHhLpp8wtm6M5TgSw==", + "dev": true, + "license": "Apache-2.0", + "bin": { + "tsc": "bin/tsc", + "tsserver": "bin/tsserver" + }, + "engines": { + "node": ">=14.17" + } + }, + "node_modules/undici-types": { + "version": "6.21.0", + "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-6.21.0.tgz", + "integrity": "sha512-iwDZqg0QAGrg9Rav5H4n0M64c3mkR59cJ6wQp+7C4nI0gsmExaedaYLNO44eT4AtBBwjbTiGPMlt2Md0T9H9JQ==", + "dev": true, + "license": "MIT" + } + } +} diff --git a/forge/e2e/package.json b/forge/e2e/package.json new file mode 100644 index 00000000..027b8377 --- /dev/null +++ b/forge/e2e/package.json @@ -0,0 +1,16 @@ +{ + "name": "forge-e2e", + "version": "1.0.0", + "description": "End-to-end tests for Forge/Sterling integration", + "scripts": { + "test": "playwright test", + "test:headed": "playwright test --headed", + "test:debug": "playwright test --debug", + "test:ui": "playwright test --ui" + }, + "devDependencies": { + "@playwright/test": "^1.40.0", + "@types/node": "^20.10.0", + "typescript": "^5.3.0" + } +} diff --git a/forge/e2e/playwright.config.ts b/forge/e2e/playwright.config.ts new file mode 100644 index 00000000..6d13ecab --- /dev/null +++ b/forge/e2e/playwright.config.ts @@ -0,0 +1,35 @@ +import { defineConfig, devices } from '@playwright/test'; + +export default defineConfig({ + testDir: './tests', + fullyParallel: false, // Run serially since each test spawns its own Forge process + forbidOnly: !!process.env.CI, + retries: process.env.CI ? 2 : 0, + workers: 1, // Single worker to avoid port conflicts + reporter: 'list', + + use: { + // Base URL will be set dynamically per test based on Forge output + trace: 'on-first-retry', + screenshot: 'only-on-failure', + }, + + // Increase timeout for tests that spawn Forge processes + timeout: 60000, + expect: { + timeout: 10000, + }, + + projects: [ + { + name: 'chromium', + use: { + ...devices['Desktop Chrome'], + headless: true, + launchOptions: { + headless: true, + }, + }, + }, + ], +}); diff --git a/forge/e2e/tests/sterling-basic.spec.ts b/forge/e2e/tests/sterling-basic.spec.ts new file mode 100644 index 00000000..a08ecf25 --- /dev/null +++ b/forge/e2e/tests/sterling-basic.spec.ts @@ -0,0 +1,74 @@ +import { test, expect, Page } from '@playwright/test'; +import { startForge, ForgeInstance, selectAndRunCommand } from '../helpers/forge-runner'; + +test.describe('Sterling Basic Functionality', () => { + let forge: ForgeInstance; + + test.afterEach(async () => { + if (forge) { + forge.cleanup(); + } + }); + + test('Sterling loads and shows run menu', async ({ page }) => { + // Start Forge with our test file + forge = await startForge('e2e/fixtures/simple-graph.frg'); + + // Navigate to Sterling + await page.goto(forge.sterlingUrl); + + // Wait for the page to load - Sterling should show a menu or graph view + await expect(page.locator('body')).toBeVisible(); + + // Check that the page has loaded something (not a blank/error page) + const content = await page.content(); + expect(content).not.toContain('Cannot GET'); + expect(content).not.toContain('404'); + + // Sterling shows runs in a combobox/select dropdown + // Look for a select element containing our run names + const runSelect = page.getByRole('combobox'); + await expect(runSelect).toBeVisible({ timeout: 10000 }); + + // Verify both runs are available as options + await expect(runSelect.locator('option', { hasText: 'simpleRun' })).toBeAttached(); + await expect(runSelect.locator('option', { hasText: 'connectedRun' })).toBeAttached(); + }); + + test('can select a run and see instance', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + // Wait for Sterling to load + await page.waitForLoadState('networkidle'); + + // Select and run a command (must click Run button after selecting) + await selectAndRunCommand(page, 'simpleRun'); + + // After running, Sterling should show an instance with graph visualization + await expect(page.locator('svg').first()).toBeVisible({ timeout: 5000 }); + }); + + test('WebSocket connection is established', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + + // Set up WebSocket listener BEFORE navigating + const wsConnections: string[] = []; + page.on('websocket', (ws) => { + wsConnections.push(ws.url()); + }); + + await page.goto(forge.sterlingUrl); + + // Wait for page to establish WebSocket connection + await page.waitForLoadState('networkidle'); + + // Also wait for the combobox to appear (indicates data loaded via WebSocket) + await expect(page.getByRole('combobox')).toBeVisible({ timeout: 10000 }); + + // Verify a WebSocket connection was made to our provider + expect(wsConnections.length).toBeGreaterThan(0); + // WebSocket URL might use 127.0.0.1 or localhost + expect(wsConnections.some((url) => url.includes('127.0.0.1') || url.includes('localhost'))).toBe(true); + }); +}); diff --git a/forge/e2e/tests/sterling-evaluator.spec.ts b/forge/e2e/tests/sterling-evaluator.spec.ts new file mode 100644 index 00000000..7683e169 --- /dev/null +++ b/forge/e2e/tests/sterling-evaluator.spec.ts @@ -0,0 +1,97 @@ +import { test, expect } from '@playwright/test'; +import { startForge, ForgeInstance, selectAndRunCommand } from '../helpers/forge-runner'; + +test.describe('Sterling Evaluator', () => { + let forge: ForgeInstance; + + test.afterEach(async () => { + if (forge) { + forge.cleanup(); + } + }); + + test('can open the evaluator panel', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + // Must run a command first to have an instance to evaluate + await selectAndRunCommand(page, 'simpleRun'); + + // Wait for graph layout to finish + await page.waitForTimeout(2000); + + // The Evaluator is a sidebar tab on the right - click it + // It's displayed as vertical text "Evaluator" in a tab button + const evaluatorTab = page.getByText('Evaluator', { exact: true }).first(); + await expect(evaluatorTab).toBeVisible({ timeout: 5000 }); + await evaluatorTab.click(); + + // After clicking, the EVALUATOR panel should open + await expect(page.getByPlaceholder('Enter an expression')).toBeVisible({ timeout: 5000 }); + }); + + test('can evaluate a simple expression', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + // Run a command first + await selectAndRunCommand(page, 'simpleRun'); + + // Wait for graph layout to finish + await page.waitForTimeout(2000); + + // Open evaluator panel + const evaluatorTab = page.getByText('Evaluator', { exact: true }).first(); + await evaluatorTab.click(); + await expect(page.getByPlaceholder('Enter an expression')).toBeVisible({ timeout: 5000 }); + + // Find input field in evaluator - placeholder is "Enter an expression..." + const evaluatorInput = page.getByPlaceholder('Enter an expression'); + await expect(evaluatorInput).toBeVisible({ timeout: 5000 }); + + // Type a simple expression - "Node" should return all Node atoms + await evaluatorInput.fill('Node'); + await evaluatorInput.press('Enter'); + + // Wait for result + await page.waitForTimeout(2000); + + // The result should contain Node references - look for Node0, Node1, or Node2 + await expect(page.getByText(/Node[012]/).first()).toBeVisible({ timeout: 5000 }); + }); + + test('evaluator shows result for edges relation', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + // Run a command first + await selectAndRunCommand(page, 'simpleRun'); + + // Wait for graph layout to finish + await page.waitForTimeout(2000); + + // Open evaluator panel + const evaluatorTab = page.getByText('Evaluator', { exact: true }).first(); + await evaluatorTab.click(); + await expect(page.getByPlaceholder('Enter an expression')).toBeVisible({ timeout: 5000 }); + + // Count how many result entries exist before evaluation + const resultsBefore = await page.locator('text=/Node\\d.*→.*Node\\d/').count(); + + // Find input field and evaluate the edges relation + const evaluatorInput = page.getByPlaceholder('Enter an expression'); + await evaluatorInput.fill('edges'); + await evaluatorInput.press('Enter'); + + // Wait for result + await page.waitForTimeout(2000); + + // The evaluator should show tuple results like "Node0 → Node1" for edges + // Since simpleRun requires "some edges", there should be at least one tuple + const resultsAfter = await page.locator('text=/Node\\d/').count(); + + // There should be more Node references after evaluation (the result tuples) + // Or at minimum, the evaluator panel should show the edges expression was processed + expect(resultsAfter).toBeGreaterThan(0); + }); +}); diff --git a/forge/e2e/tests/sterling-instance.spec.ts b/forge/e2e/tests/sterling-instance.spec.ts new file mode 100644 index 00000000..ea539a45 --- /dev/null +++ b/forge/e2e/tests/sterling-instance.spec.ts @@ -0,0 +1,55 @@ +import { test, expect } from '@playwright/test'; +import { startForge, ForgeInstance, selectAndRunCommand } from '../helpers/forge-runner'; + +test.describe('Sterling Instance Display', () => { + let forge: ForgeInstance; + + test.afterEach(async () => { + if (forge) { + forge.cleanup(); + } + }); + + test('displays atom names from the model', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + // Select and run a command + await selectAndRunCommand(page, 'simpleRun'); + + // Wait for layout to finish (the "Computing layout..." message to disappear) + await page.waitForTimeout(2000); + + // The model has exactly 3 Node atoms - they should appear as Node0, Node1, Node2 + // Use getByText which works with SVG text elements + await expect(page.getByText('Node0')).toBeVisible({ timeout: 5000 }); + }); + + test('displays sig names in the interface', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + await selectAndRunCommand(page, 'simpleRun'); + + // Wait for layout to finish + await page.waitForTimeout(2000); + + // The sig name "Node" appears as a label on each atom box in the graph + // Look for it in the visible text (SVG text elements) + await expect(page.getByText('Node', { exact: true }).first()).toBeVisible({ timeout: 5000 }); + }); + + test('displays edges/relations in graph view', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + await selectAndRunCommand(page, 'simpleRun'); + + // Wait for layout to finish + await page.waitForTimeout(2000); + + // The simpleRun requires "some edges", so the "edges" relation label should appear + // This label is shown on the arrows connecting nodes in the graph + await expect(page.getByText('edges').first()).toBeVisible({ timeout: 5000 }); + }); +}); diff --git a/forge/e2e/tests/sterling-navigation.spec.ts b/forge/e2e/tests/sterling-navigation.spec.ts new file mode 100644 index 00000000..ba5d533a --- /dev/null +++ b/forge/e2e/tests/sterling-navigation.spec.ts @@ -0,0 +1,78 @@ +import { test, expect } from '@playwright/test'; +import { startForge, ForgeInstance, selectAndRunCommand } from '../helpers/forge-runner'; + +test.describe('Sterling Navigation', () => { + let forge: ForgeInstance; + + test.afterEach(async () => { + if (forge) { + forge.cleanup(); + } + }); + + test('can navigate to next instance', async ({ page }) => { + forge = await startForge('e2e/fixtures/multi-instance.frg'); + await page.goto(forge.sterlingUrl); + + // Select and run the command + await selectAndRunCommand(page, 'multiRun'); + + // Wait for layout to stabilize + await page.waitForTimeout(2000); + + // Verify we're on instance 1 (header shows "ID: 1 MULTIRUN") + await expect(page.getByText('ID: 1')).toBeVisible({ timeout: 5000 }); + + // Find and click the "Next" button + const nextButton = page.getByRole('button', { name: /next/i }); + await expect(nextButton).toBeVisible({ timeout: 5000 }); + await nextButton.click(); + + // Wait for the instance to update + await page.waitForTimeout(2000); + + // Verify we're now on instance 2 (header shows "ID: 2 MULTIRUN") + await expect(page.getByText('ID: 2')).toBeVisible({ timeout: 5000 }); + }); + + test('can switch between different runs', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + // Run first command + await selectAndRunCommand(page, 'simpleRun'); + await page.waitForTimeout(2000); + + // Verify instance history shows the first run + await expect(page.getByText(/from: 'simpleRun'/)).toBeVisible({ timeout: 5000 }); + + // Now select and run second command + const runSelect = page.getByRole('combobox'); + await runSelect.selectOption({ label: 'connectedRun' }); + + const runButton = page.getByRole('button', { name: 'Run', exact: true }); + await runButton.click(); + + // Wait for new instance to load + await expect(page.locator('svg').first()).toBeVisible({ timeout: 20000 }); + await page.waitForTimeout(2000); + + // Verify instance history now shows the second run (instance number may vary) + await expect(page.getByText(/from: 'connectedRun'/)).toBeVisible({ timeout: 5000 }); + }); + + test('run selector shows all available runs', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + const runSelect = page.getByRole('combobox'); + await expect(runSelect).toBeVisible({ timeout: 10000 }); + + // Get all options + const options = await runSelect.locator('option').allTextContents(); + + // Should have both runs from our fixture + expect(options).toContain('simpleRun'); + expect(options).toContain('connectedRun'); + }); +}); diff --git a/forge/e2e/tests/sterling-unsat.spec.ts b/forge/e2e/tests/sterling-unsat.spec.ts new file mode 100644 index 00000000..e686ba2d --- /dev/null +++ b/forge/e2e/tests/sterling-unsat.spec.ts @@ -0,0 +1,57 @@ +import { test, expect } from '@playwright/test'; +import { startForge, ForgeInstance } from '../helpers/forge-runner'; + +test.describe('Sterling Unsat Display', () => { + let forge: ForgeInstance; + + test.afterEach(async () => { + if (forge) { + forge.cleanup(); + } + }); + + test('displays unsat message for unsatisfiable model', async ({ page }) => { + forge = await startForge('e2e/fixtures/unsat-model.frg'); + await page.goto(forge.sterlingUrl); + + // Select the unsat run from combobox + const runSelect = page.getByRole('combobox'); + await expect(runSelect).toBeVisible({ timeout: 10000 }); + await runSelect.selectOption({ label: 'unsatRun' }); + + // Click Run button to execute + const runButton = page.getByRole('button', { name: 'Run', exact: true }); + await expect(runButton).toBeVisible({ timeout: 5000 }); + await runButton.click(); + + // Wait for Sterling to process and display result + await page.waitForTimeout(3000); + + // Should show "Unsatisfiable" text in the graph area + // This text appears inside the SVG visualization + await expect(page.getByText('Unsatisfiable')).toBeVisible({ timeout: 10000 }); + }); + + test('unsat run does not show Next button', async ({ page }) => { + forge = await startForge('e2e/fixtures/unsat-model.frg'); + await page.goto(forge.sterlingUrl); + + // Select and run the unsat command + const runSelect = page.getByRole('combobox'); + await expect(runSelect).toBeVisible({ timeout: 10000 }); + await runSelect.selectOption({ label: 'unsatRun' }); + + const runButton = page.getByRole('button', { name: 'Run', exact: true }); + await runButton.click(); + + // Wait for result and verify we got unsat + await expect(page.getByText('Unsatisfiable')).toBeVisible({ timeout: 10000 }); + + // The Next button should not be visible for unsat results + const nextButton = page.getByRole('button', { name: /next/i }); + + // Explicitly verify the Next button is NOT visible + // (as opposed to just accepting any state) + await expect(nextButton).not.toBeVisible(); + }); +}); diff --git a/forge/e2e/tests/sterling-views.spec.ts b/forge/e2e/tests/sterling-views.spec.ts new file mode 100644 index 00000000..3426de04 --- /dev/null +++ b/forge/e2e/tests/sterling-views.spec.ts @@ -0,0 +1,103 @@ +import { test, expect } from '@playwright/test'; +import { startForge, ForgeInstance, selectAndRunCommand } from '../helpers/forge-runner'; + +test.describe('Sterling Views', () => { + let forge: ForgeInstance; + + test.afterEach(async () => { + if (forge) { + forge.cleanup(); + } + }); + + test('can switch to Table view', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + // Must run a command first + await selectAndRunCommand(page, 'simpleRun'); + await page.waitForTimeout(2000); + + // Find and click Table button (in top nav) + const tableButton = page.getByRole('button', { name: /table/i }); + await expect(tableButton).toBeVisible({ timeout: 5000 }); + await tableButton.click(); + + // Table view should show table-like content + await page.waitForTimeout(1000); + + // Table view shows sig/relation names as headers or in a structured format + // Look for table-specific elements or structured data display + const hasTableContent = await page.evaluate(() => { + // Check for actual table elements or grid-like structures + const tables = document.querySelectorAll('table, [role="grid"], [role="table"]'); + // Also check for structured divs that might represent table data + const headerCells = document.querySelectorAll('th, [role="columnheader"]'); + return tables.length > 0 || headerCells.length > 0; + }); + + expect(hasTableContent).toBe(true); + }); + + test('can switch to Script view', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + await selectAndRunCommand(page, 'simpleRun'); + await page.waitForTimeout(2000); + + // Find and click Script button + const scriptButton = page.getByRole('button', { name: /script/i }); + await expect(scriptButton).toBeVisible({ timeout: 5000 }); + await scriptButton.click(); + + // Wait for view change + await page.waitForTimeout(1000); + + // Script view should show code editor or script-related content + const hasScriptContent = await page.evaluate(() => { + // Look for code editor elements (CodeMirror, Monaco, or plain textarea/pre) + const codeElements = document.querySelectorAll( + 'pre, code, .CodeMirror, .monaco-editor, textarea, [class*="editor"], [class*="code"]' + ); + return codeElements.length > 0; + }); + + expect(hasScriptContent).toBe(true); + }); + + test('can switch back to Graph view', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + await selectAndRunCommand(page, 'simpleRun'); + + // Switch to Table + const tableButton = page.getByRole('button', { name: /table/i }); + await tableButton.click(); + await page.waitForTimeout(500); + + // Switch back to Graph + const graphButton = page.getByRole('button', { name: /graph/i }); + await expect(graphButton).toBeVisible({ timeout: 5000 }); + await graphButton.click(); + + // Should see SVG graph again + await expect(page.locator('svg').first()).toBeVisible({ timeout: 5000 }); + }); + + test('Graph view shows visualization', async ({ page }) => { + forge = await startForge('e2e/fixtures/simple-graph.frg'); + await page.goto(forge.sterlingUrl); + + await selectAndRunCommand(page, 'simpleRun'); + + // SVG should be visible with content + const svg = page.locator('svg').first(); + await expect(svg).toBeVisible(); + + // SVG should have content (not empty) + const svgContent = await svg.innerHTML(); + expect(svgContent.length).toBeGreaterThan(0); + }); +}); diff --git a/forge/e2e/tsconfig.json b/forge/e2e/tsconfig.json new file mode 100644 index 00000000..3cce7b11 --- /dev/null +++ b/forge/e2e/tsconfig.json @@ -0,0 +1,16 @@ +{ + "compilerOptions": { + "target": "ES2020", + "module": "commonjs", + "moduleResolution": "node", + "strict": true, + "esModuleInterop": true, + "skipLibCheck": true, + "forceConsistentCasingInFileNames": true, + "outDir": "./dist", + "rootDir": ".", + "resolveJsonModule": true + }, + "include": ["**/*.ts"], + "exclude": ["node_modules", "dist"] +} diff --git a/forge/send-to-solver.rkt b/forge/send-to-solver.rkt index 07730b72..6b1052de 100644 --- a/forge/send-to-solver.rkt +++ b/forge/send-to-solver.rkt @@ -649,11 +649,13 @@ Please declare a sufficient scope for ~a." ; for ease of understanding, just sort by first atom (: tuple Tuple Tuple Boolean)) (define (tuple (define bounds-hash @@ -807,7 +809,7 @@ Please declare a sufficient scope for ~a." (: ints (Listof FAtom)) (define ints (map (ann car (-> Tuple FAtom)) upper-on-int)) (: succ-tuples (Listof (Listof FAtom))) - ;; TODO: this relies on getting the right ordering on unary Int tuples, doesn't it? + ;; Int tuples are sorted numerically by tuple (and/c jsexpr? hash?) (listof symbol?) jsexpr?) (cond [(empty? path) json-m] - [else + [else (unless (hash-has-key? json-m (first path)) (error (format "get-from-json expected JSON dictionary with ~a field, got: ~a~n" (first path) json-m))) (get-from-json (hash-ref json-m (first path)) (rest path))])) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Shared helpers for Sterling communication +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; Send a message to Sterling over a WebSocket connection +(define (send-to-sterling m #:connection connection) + (when (@>= (get-verbosity) VERBOSITY_STERLING) + (printf "Sending message to Sterling: ~a~n" m)) + (ws-send! connection m)) + +; Start a WebSocket server for Sterling communication. +; Returns (values stop-service port) where port may be a string on failure. +; handler-proc: (-> connection message void) - handles non-ping messages +; port-option: the port number to listen on (0 for ephemeral) +(define (start-websocket-server port-option handler-proc) + (define chan (make-async-channel)) + (define stop-service + (ws-serve + (λ (connection _) + (let loop () + (define m (ws-recv connection)) + (unless (eof-object? m) + (when (@>= (get-verbosity) VERBOSITY_STERLING) + (printf "Message received from Sterling: ~a~n" m)) + (cond [(equal? m "ping") + (send-to-sterling "pong" #:connection connection)] + [else (handler-proc connection m)]) + (loop)))) + #:port port-option #:confirmation-channel chan)) + (define port (async-channel-get chan)) + (when (string? port) + (printf "NO PORTS AVAILABLE. Could not start provider server.~n")) + (values stop-service port)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ; name is the name of the model ; get-next-instance returns the next instance each time it is called, or #f. (define (display-model @@ -63,11 +99,16 @@ (define state-for-run (Run-spec-state (Run-run-spec the-run))) - (define current-tree orig-lazy-tree) - (define curr-datum-id 1) ; nonzero - (define id-to-instance-map (make-hash)) ; mutable hash - - (define (get-current-instance) + ;; Skip starting WebSocket server if Sterling is disabled + (when (member (get-option the-run 'run_sterling) (list 'off "off" #f)) + (printf "Sterling is disabled (run_sterling = off). Skipping visualization.~n")) + + (unless (member (get-option the-run 'run_sterling) (list 'off "off" #f)) + (define current-tree orig-lazy-tree) + (define curr-datum-id 1) ; nonzero + (define id-to-instance-map (make-hash)) ; mutable hash + + (define (get-current-instance) (define returned-instance (tree:get-value current-tree)) (set-box! (Run-last-sterling-instance the-run) returned-instance) returned-instance) @@ -81,12 +122,7 @@ (values curr-datum-id (get-current-instance))) (define command-string (format "~a" (syntax->datum command))) - - (define (send-to-sterling m #:connection connection) - (when (@>= (get-verbosity) VERBOSITY_STERLING) - (printf "Sending message to Sterling: ~a~n" m)) - (ws-send! connection m)) - + (define (get-xml soln) ;(define tuple-annotations (if (and (Sat? model) (equal? 'on (get-option the-run 'local_necessity))) ; (build-tuple-annotations-for-ln model) @@ -169,35 +205,22 @@ (send-to-sterling "BAD REQUEST" #:connection connection) (printf "Sterling message contained unexpected type field: ~a~n" json-m)])) - (define chan (make-async-channel)) - - ; After this is defined, the service is active and should be listening - (define stop-service - (ws-serve - ; This is the connection handler function, it has total control over the connection - ; from the time that conn-headers finishes responding to the connection request, to the time - ; the connection closes. The server generates a new handler thread for this function - ; every time a connection is initiated. - (λ (connection _) - (let loop () - (define m (ws-recv connection)) - (unless (eof-object? m) - (when (@>= (get-verbosity) VERBOSITY_STERLING) - (printf "Message received from Sterling: ~a~n" m)) - (cond [(equal? m "ping") - (send-to-sterling "pong" #:connection connection)] - [else (handle-json connection m)]) - (loop)))) - ; default #:port 0 will assign an ephemeral port - #:port (get-option the-run 'sterling_port) #:confirmation-channel chan)) - - (define port (async-channel-get chan)) - (when (string? port) - (printf "NO PORTS AVAILABLE. Could not start provider server.~n")) - - ; Now, serve the static sterling website files (this will be a different server/port). - (unless (equal? 'off (get-option state-for-run 'run_sterling)) - (serve-sterling-static #:provider-port port))) + (define-values (stop-service port) + (start-websocket-server (get-option the-run 'sterling_port) handle-json)) + + ; Now, serve the static sterling website files (this will be a different server/port). + (define run-sterling-mode (get-option state-for-run 'run_sterling)) + (cond [(member run-sterling-mode (list 'off "off")) + (void)] ; do nothing + [(member run-sterling-mode (list 'serve "serve")) + (serve-no-sterling #:provider-port port)] + [(member run-sterling-mode (list 'headless "headless")) + (serve-sterling-static #:provider-port port + #:static-port (get-option state-for-run 'sterling_static_port) + #:open-browser #f)] + [else + (serve-sterling-static #:provider-port port + #:static-port (get-option state-for-run 'sterling_static_port))]))) ; closes outer unless (define (make-status-value inst) (cond [(Sat? inst) "sat"] @@ -269,8 +292,11 @@ ;; The namespace is passed to aid evaluation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (define (start-sterling-menu curr-state nsa) - ; The runs defined in the state at this point, which should be after all declarations. - (define runmap (State-runmap curr-state)) + ;; Early exit if Sterling is disabled - avoid starting WebSocket server + (unless (member (get-option curr-state 'run_sterling) (list 'off "off" #f)) + + ; The runs defined in the state at this point, which should be after all declarations. + (define runmap (State-runmap curr-state)) (define defined-run-names (hash-keys runmap)) ; Filter out runs that are not useful to visualize, like tests that failed due to unsat. @@ -295,11 +321,6 @@ (when (> (get-verbosity) VERBOSITY_LOW) (printf "Starting Sterling in command-selection mode...~n") (printf "Available commands: ~a~n" useful-run-names)) - - (define (send-to-sterling m #:connection connection) - (when (@>= (get-verbosity) VERBOSITY_STERLING) - (printf "Sending message to Sterling: ~a~n" m)) - (ws-send! connection m)) (define curr-datum-id 0) ; nonzero (define id-to-instance-map (make-hash)) ; mutable hash @@ -505,43 +526,22 @@ #:msg (format "Sterling message contained unexpected type field: ~a~n" json-m) #:context context)])) - (define chan (make-async-channel)) - - ; After this is defined, the service is active and should be listening - (define stop-service - (ws-serve - ; This is the connection handler function, it has total control over the connection - ; from the time that conn-headers finishes responding to the connection request, to the time - ; the connection closes. The server generates a new handler thread for this function - ; every time a connection is initiated. - (λ (connection _) - (let loop () - (define m (ws-recv connection)) - (unless (eof-object? m) - (when (@>= (get-verbosity) VERBOSITY_STERLING) - (printf "Message received from Sterling: ~a~n" m)) - (cond [(equal? m "ping") - (send-to-sterling "pong" #:connection connection)] - [else (handle-json connection m)]) - (loop)))) - ; default #:port 0 will assign an ephemeral port - #:port (get-option curr-state 'sterling_port) #:confirmation-channel chan)) - ;; The instance-provider service is now active and listening. - - (define port (async-channel-get chan)) - (when (string? port) - (printf "NO PORTS AVAILABLE. Could not start provider server.~n")) - - ; Now, serve the static sterling website files (this will be a different server/port). - ; Switch Sterling off for the "off" string too, because users may neglect the \' - ; if providing an override at the command line. This means that one cannot provide - ; a script in a file named "off". - - (cond [(empty? useful-run-names) - (printf "There was nothing useful to visualize: all commands were already executed and produced no instances.~n")] - [(member (get-option curr-state 'run_sterling) (list 'off "off" #f)) - (void)] - [(member (get-option curr-state 'run_sterling) (list 'serve "serve")) - (serve-no-sterling #:provider-port port)] - [else - (serve-sterling-static #:provider-port port)])) \ No newline at end of file + (define-values (stop-service port) + (start-websocket-server (get-option curr-state 'sterling_port) handle-json)) + + ; Now, serve the static sterling website files (this will be a different server/port). + ; Switch Sterling off for the "off" string too, because users may neglect the \' + ; if providing an override at the command line. This means that one cannot provide + ; a script in a file named "off". + + (cond [(empty? useful-run-names) + (printf "There was nothing useful to visualize: all commands were already executed and produced no instances.~n")] + [(member (get-option curr-state 'run_sterling) (list 'serve "serve")) + (serve-no-sterling #:provider-port port)] + [(member (get-option curr-state 'run_sterling) (list 'headless "headless")) + (serve-sterling-static #:provider-port port + #:static-port (get-option curr-state 'sterling_static_port) + #:open-browser #f)] + [else + (serve-sterling-static #:provider-port port + #:static-port (get-option curr-state 'sterling_static_port))]))) ; closes unless \ No newline at end of file diff --git a/forge/server/serve-sterling-static.rkt b/forge/server/serve-sterling-static.rkt index b299575b..9cdb5ba7 100644 --- a/forge/server/serve-sterling-static.rkt +++ b/forge/server/serve-sterling-static.rkt @@ -32,13 +32,15 @@ [else bytes-read])) -(define (serve-sterling-static #:provider-port [provider-port 0]) +(define (serve-sterling-static #:provider-port [provider-port 0] + #:static-port [static-port 0] + #:open-browser [open-browser #t]) (define confirm-chan (make-async-channel)) (define stop-static-server (serve #:dispatch (files:make #:url->path (make-url->path sterling-path)) - #:port 0 + #:port static-port #:confirmation-channel confirm-chan)) (define port (async-channel-get confirm-chan)) @@ -46,17 +48,19 @@ (printf "NO PORTS AVAILABLE. Unable to serve Sterling static files. You may be able to manually load Sterling's index.html here:~n~a~n" (string-append (path->string sterling-index) "?" (number->string provider-port)))] [else - ; Attempt to open a browser to the Sterling index.html, with the proper port - ; If this cannot be opened for whatever reason, keep the server open but print - ; a warning, allowing the user a workaround. - ; (We no longer use send-url/file, which is for file:// URLs) (define sterling-url (format "http://127.0.0.1:~a/?~a" port provider-port)) - (with-handlers ([exn? - (lambda (e) (printf "Racket could not open a browser on your system; you may be able manually navigate to this address, which is where Forge expects Sterling to load:~n ~a~nContext: ~a~n" - sterling-url - e))]) - (send-url sterling-url)) - + ; In headless mode, skip opening the browser + (when open-browser + ; Attempt to open a browser to the Sterling index.html, with the proper port + ; If this cannot be opened for whatever reason, keep the server open but print + ; a warning, allowing the user a workaround. + ; (We no longer use send-url/file, which is for file:// URLs) + (with-handlers ([exn? + (lambda (e) (printf "Racket could not open a browser on your system; you may be able manually navigate to this address, which is where Forge expects Sterling to load:~n ~a~nContext: ~a~n" + sterling-url + e))]) + (send-url sterling-url))) + (printf "Opening Forge menu in Sterling (static server port=~a). Press enter to stop Forge (or click 'Stop' in VSCode).~n" port) (flush-output) diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt index cf16e754..551ca30c 100644 --- a/forge/sigs-structs.rkt +++ b/forge/sigs-structs.rkt @@ -266,6 +266,7 @@ 'local_necessity 'off 'run_sterling 'on 'sterling_port 0 + 'sterling_static_port 0 'engine_verbosity 1 'test_keep 'first 'no_overflow 'false @@ -315,6 +316,7 @@ (and (list? x) (andmap (lambda (ele) (string? ele)) x)))) 'sterling_port exact-nonnegative-integer? + 'sterling_static_port exact-nonnegative-integer? 'engine_verbosity exact-nonnegative-integer? 'test_keep (oneof-pred '(first last)) 'no_overflow (oneof-pred '(false true)) @@ -336,6 +338,7 @@ 'local_necessity "symbol" 'run_sterling "symbol, string, or sequence of strings" 'sterling_port "non-negative integer" + 'sterling_static_port "non-negative integer" 'engine_verbosity "non-negative integer" 'test_keep "one of: first or last" 'no_overflow "one of: false or true" diff --git a/forge/tests/forge/eval-model/div-by-zero-test.rkt b/forge/tests/forge/eval-model/div-by-zero-test.rkt new file mode 100644 index 00000000..9eaf2306 --- /dev/null +++ b/forge/tests/forge/eval-model/div-by-zero-test.rkt @@ -0,0 +1,55 @@ +#lang racket/base + +;; Unit test for C1: Division by zero handling in eval-model.rkt +;; +;; Tests that eval-int-expr raises clear user errors for division/remainder +;; by zero, rather than crashing with raw Racket errors. + +(require rackunit + forge/server/eval-model + (prefix-in ast: forge/lang/ast)) + +(define (make-int-constant n) (ast:int/func n)) +(define (make-divide a b) (ast:divide/func a b)) +(define (make-remainder a b) (ast:remainder/func a b)) + +(define test-bitwidth 4) +(define empty-binding (make-hash)) + +(define five (make-int-constant 5)) +(define zero (make-int-constant 0)) + +(test-case + "divide by zero raises forge error with context" + (check-exn + #rx"division by zero" + (lambda () + (eval-int-expr (make-divide five zero) empty-binding test-bitwidth)))) + +(test-case + "remainder by zero raises forge error with context" + (check-exn + #rx"remainder by zero" + (lambda () + (eval-int-expr (make-remainder five zero) empty-binding test-bitwidth)))) + +(test-case + "normal division works" + (check-equal? + (eval-int-expr (make-divide (make-int-constant 6) (make-int-constant 2)) + empty-binding test-bitwidth) + 3)) + +(test-case + "normal remainder works" + (check-equal? + (eval-int-expr (make-remainder (make-int-constant 7) (make-int-constant 3)) + empty-binding test-bitwidth) + 1)) + +(test-case + "negative division works" + (check-equal? + (eval-int-expr (make-divide (make-int-constant -6) (make-int-constant 2)) + empty-binding test-bitwidth) + -3))