diff --git a/CHANGELOG.md b/CHANGELOG.md index a0dc01b..f429754 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +## [0.2.0] - 2023-06-03 + +- Change to new REST-API of Ultimate + ## [0.1.2] - 2023-04-18 - add command to trigger verification manually (default now) diff --git a/README.md b/README.md index 74956b0..8d6cbde 100644 --- a/README.md +++ b/README.md @@ -10,9 +10,10 @@ A formal verification by Ultimate Automizer on the file is performed and the res ## Requirements -Connection to a public server running Ultimate Automizer, e.g. or . +Connection to a public server running Ultimate Automizer, e.g. . -Alternatively a container providing the API can be executed inside Docker. +Alternatively a container providing the API can be executed inside Docker. A dockerfile to host the +Backend locally can be found [here](https://github.com/FahrJo/ultimate-automizer-docker). ## Extension Settings @@ -29,11 +30,14 @@ This extension contributes the following settings: * Make sure the right Java version us used as default version if running Ultimate locally. * Windows version only working properly by using the REST API mode since Ultimate 0.2.3 was not working on my Windows test machine properly. -* The result representation (code highlighting, log output etc.) so far looks differently for `REST API` and `stdout` mode. This is due to the output of Ultimate in the two different modes. -* So far there is no Dockerfile/Image available to host the REST API backend locally in a container. +* The result representation (code highlighting, log output etc.) so far looks differently for `rest-api` and `stdout` mode. This is due to the output of Ultimate in the two different modes. ## Release Notes +### 0.2.0 + +Change to new REST-API of Ultimate + ### 0.1.2 Add command to trigger verification manually (default now) diff --git a/images/demo.gif b/images/demo.gif index f656130..0b5cb05 100644 Binary files a/images/demo.gif and b/images/demo.gif differ diff --git a/package.json b/package.json index 429e3da..ec62908 100644 --- a/package.json +++ b/package.json @@ -2,7 +2,7 @@ "name": "ultimate-automizer", "displayName": "Ultimate Automizer", "description": "This extension runs a formal verification on the current active C file.", - "version": "0.1.2", + "version": "0.2.0", "publisher": "FahrJo", "contributors": [ { @@ -22,7 +22,9 @@ "categories": [ "Programming Languages" ], - "activationEvents": [], + "activationEvents": [ + "onLanguage:c" + ], "main": "./out/extension.js", "contributes": { "configuration": { @@ -30,9 +32,9 @@ "properties": { "ultimate.mode": { "type": "string", - "default": "REST API", + "default": "rest-api", "enum": [ - "REST API", + "rest-api", "stdout" ], "enumDescriptions": [ @@ -43,9 +45,14 @@ }, "ultimate.url": { "type": "string", - "default": "https://monteverdi.informatik.uni-freiburg.de", + "default": "https://ultimate.sopranium.de/api", "description": "Base URL of the API endpoint." }, + "ultimate.refreshDelay": { + "type": "number", + "default": 3000, + "description": "Delay between result polling in rest-api mode. If the property Url is a known public server, a delay of at least 3000 ms is enforced" + }, "ultimate.executablePath": { "type": "string", "default": "", @@ -54,12 +61,12 @@ "ultimate.settingsPath": { "type": "string", "default": "", - "description": "Path to the settings (*.epl/*.epf) of Ultimate (is not accessed when using the REST API)." + "description": "Path to the settings (*.epl/*.epf) of Ultimate (is not accessed when using the REST API). A default toolchain is used if not defined" }, "ultimate.toolchainPath": { "type": "string", "default": "", - "description": "Path to the toolchain (*.xml) of Ultimate (is not accessed when using the REST API)." + "description": "Path to the toolchain (*.xml) of Ultimate. A default toolchain is used if not defined." }, "ultimate.verifyOnSave": { "type": "boolean", diff --git a/src/extension.ts b/src/extension.ts index ab90805..9ab2d7b 100644 --- a/src/extension.ts +++ b/src/extension.ts @@ -47,21 +47,27 @@ export function deactivate(): void { function initializeUltimate(context: vscode.ExtensionContext): void { let mode = vscode.workspace.getConfiguration().get('ultimate.mode'); + let settings = vscode.Uri.file( + vscode.workspace.getConfiguration().get('ultimate.settingsPath')! + ); + let toolchain = vscode.Uri.file( + vscode.workspace.getConfiguration().get('ultimate.toolchainPath')! + ); switch (mode) { - case 'REST API': + case 'REST API': // keep compatibility with old versions > 2.0 + case 'rest-api': let ultimateUrl: string = vscode.workspace.getConfiguration().get('ultimate.url')!; - ultimate = UltimateFactory.createUltimateUsingPublicApi(context, ultimateUrl); + ultimate = UltimateFactory.createUltimateUsingRestApi( + context, + ultimateUrl, + settings, + toolchain + ); break; case 'stdout': let ultimatePath = vscode.Uri.file( vscode.workspace.getConfiguration().get('ultimate.executablePath')! ); - let settings = vscode.Uri.file( - vscode.workspace.getConfiguration().get('ultimate.settingsPath')! - ); - let toolchain = vscode.Uri.file( - vscode.workspace.getConfiguration().get('ultimate.toolchainPath')! - ); ultimate = UltimateFactory.createUltimateUsingLog( context, ultimatePath, diff --git a/src/httpsRequest.ts b/src/httpsRequest.ts index 70cb059..e43a71a 100644 --- a/src/httpsRequest.ts +++ b/src/httpsRequest.ts @@ -1,6 +1,6 @@ import * as http from 'http'; import * as https from 'https'; -import * as url from 'url'; +import * as querystring from 'querystring'; export interface HttpResponse { statusCode: number | undefined; @@ -8,13 +8,14 @@ export interface HttpResponse { body: string; } -export function httpsRequest( - urlOptions: string | https.RequestOptions | url.URL, +export function unifiedHttpsRequest( + urlOptions: https.RequestOptions, data: any = '' ): Promise { let promise = new Promise((resolve, reject) => { // Inspired from https://gist.github.com/ktheory/df3440b01d4b9d3197180d5254d7fb65 - const req = https.request(urlOptions, (res) => { + let httpModule = urlOptions.protocol === 'http:' ? http : https; + const req = httpModule.request(urlOptions, (res) => { const chunks: any = []; res.on('data', (chunk) => chunks.push(chunk)); @@ -33,7 +34,7 @@ export function httpsRequest( }); req.on('error', reject); - req.write(data, 'binary'); + req.write(querystring.stringify(data), 'binary'); req.end(); }); return promise; diff --git a/src/test/suite/ultimateByHttp.test.ts b/src/test/suite/ultimateByHttp.test.ts index c77a788..b448240 100644 --- a/src/test/suite/ultimateByHttp.test.ts +++ b/src/test/suite/ultimateByHttp.test.ts @@ -1,6 +1,5 @@ import * as assert from 'assert'; import * as vscode from 'vscode'; -import * as fs from 'fs'; import { UltimateByHttp } from '../../ultimateByHttp'; suite('UltimateByHttp Test Suite', () => { @@ -15,32 +14,36 @@ suite('UltimateByHttp Test Suite', () => { test('requestOfValidFile', async () => { let ultimate = new UltimateByHttp( extensionContext, - false, - 'https://monteverdi.informatik.uni-freiburg.de' + vscode.Uri.file(''), + vscode.Uri.file(''), + 'https://ultimate.sopranium.de/api' ); ultimate.runOn(''); await new Promise((f) => setTimeout(f, 5000)); - let results = JSON.stringify(ultimate.getResultsOfLastRun()[0]); - const expectedResult = - '{"startLNr":-1,"startCol":-1,"endLNr":-1,"endCol":-1,"logLvl":"info","shortDesc":"All specifications hold","type":"invariant","longDesc":"We were not able to verify any specifiation because the program does not contain any specification."}'; - assert.strictEqual(results, expectedResult); + let results = ultimate.getResultsOfLastRun()[0]; + const expectedResult = JSON.parse( + '{"startLNr":-1,"startCol":-1,"endLNr":-1,"endCol":-1,"logLvl":"info","shortDesc":"All specifications hold","type":"positive","longDesc":"We were not able to verify any specification because the program does not contain any specification."}' + ); + assert.deepEqual(results, expectedResult); }).timeout(10000); test('requestOfSyntaxError', async () => { let ultimate = new UltimateByHttp( extensionContext, - false, - 'https://monteverdi.informatik.uni-freiburg.de' + vscode.Uri.file(''), + vscode.Uri.file(''), + 'https://ultimate.sopranium.de/api' ); ultimate.runOn('a'); await new Promise((f) => setTimeout(f, 5000)); - let results = JSON.stringify(ultimate.getResultsOfLastRun()[0]); - const expectedResult = - '{"startLNr":-1,"startCol":0,"endLNr":0,"endCol":0,"logLvl":"error","shortDesc":"Incorrect Syntax","type":"syntaxError","longDesc":"Syntax check with command \\"gcc -std=c11 -pedantic -w -fsyntax-only\\" returned the following output. \\n:1:1: error: expected \\u0018=\\u0019, \\u0018,\\u0019, \\u0018;\\u0019, \\u0018asm\\u0019 or \\u0018__attribute__\\u0019 at end of input\\n 1 | a\\n | ^"}'; - assert.strictEqual(results, expectedResult); + let results = ultimate.getResultsOfLastRun()[0]; + const expectedResult = JSON.parse( + '{"startLNr":-1,"startCol":0,"endLNr":0,"endCol":0,"logLvl":"error","shortDesc":"Incorrect Syntax","type":"syntaxError","longDesc":"Syntax check with command \\"gcc -std=c11 -pedantic -w -fsyntax-only\\" returned the following output. \\n1:1: error: expected \'=\', \',\', \';\', \'asm\' or \'__attribute__\' at end of input\\n 1 | a\\n | ^"}' + ); + assert.deepEqual(results, expectedResult); }).timeout(10000); }); diff --git a/src/ultimate.ts b/src/ultimate.ts index 861c8a3..e8ee7ae 100644 --- a/src/ultimate.ts +++ b/src/ultimate.ts @@ -1,10 +1,6 @@ import * as vscode from 'vscode'; +import * as fs from 'fs'; export interface Ultimate { - /** - * Initializes the external tool - */ - setup(): any; - /** * Execute Ultimate Automizer on the current active file * @param code C code to verify @@ -37,8 +33,9 @@ export abstract class UltimateBase implements Ultimate { //protected response: UltimateResponse = undefined!; protected results: SingleUltimateResult[] = []; protected error: string | undefined; + protected settingsFilePath = vscode.Uri.file(''); + protected toolchainFilePath = vscode.Uri.file(''); - protected containerIsStarted = false; private ultimateIsRunning = false; private progressCancellationToken: vscode.CancellationTokenSource | null = null; @@ -63,10 +60,23 @@ export abstract class UltimateBase implements Ultimate { private initOutputChannel(): void { this.extensionContext.subscriptions.push(this.outputChannel); this.outputChannel.appendLine('Ultimate activated'); - this.outputChannel.show(); } - public abstract setup(): any; + public setToolchainFile(path: vscode.Uri): void { + if (fs.existsSync(path.fsPath) && path.fsPath.match(/(.*\.xml$)/)) { + this.toolchainFilePath = path; + } else { + console.log(`Toolchain file ${path} does not exist`); + } + } + + public setSettingsFile(path: vscode.Uri): void { + if (fs.existsSync(path.fsPath) && path.fsPath.match(/(.*\.epf$)/)) { + this.settingsFilePath = path; + } else { + console.log(`Settings file ${path} does not exist`); + } + } // Execute Ultimate Automizer on C code public abstract runOn(code: string): void; diff --git a/src/ultimateByHttp.ts b/src/ultimateByHttp.ts index f2a522d..f1570da 100644 --- a/src/ultimateByHttp.ts +++ b/src/ultimateByHttp.ts @@ -1,53 +1,45 @@ import * as vscode from 'vscode'; +import * as fs from 'fs'; import { SingleUltimateResult, UltimateBase } from './ultimate'; -import { HttpResponse, httpsRequest } from './httpsRequest'; +import { HttpResponse, unifiedHttpsRequest } from './httpsRequest'; export class UltimateByHttp extends UltimateBase { - private baseUrl: URL; - private useDockerContainer = false; - - constructor(context: vscode.ExtensionContext, useDocker: boolean = false, baseUrl?: string) { + private apiUrl: URL; + private requestId = ''; + public refreshTimeInMilliseconds = 500; + + constructor( + context: vscode.ExtensionContext, + settings: vscode.Uri, + toolchain: vscode.Uri, + apiUrl: string + ) { super(context); - this.baseUrl = new URL(baseUrl || ''); - this.useDockerContainer = useDocker; - } - - public setup(): void { - if (this.useDockerContainer) { - if (this.containerIsStarted) { - vscode.window.showInformationMessage('Docker container already running.'); - } else { - vscode.window.showInformationMessage('Start Docker container...'); - - // TODO: start Docker container - - if (this.containerIsStarted) { - vscode.window.showInformationMessage('Ultimate Docker container started!'); - } else { - vscode.window.showErrorMessage( - 'Error occurred during start of Ultimate Docker container!' - ); - } - } - } + this.apiUrl = new URL(apiUrl); + this.setSettingsFile(settings); + this.setToolchainFile(toolchain); } - public runOn(input: string | vscode.TextDocument): void { - let cCode = ''; + public runOn(input: string | vscode.TextDocument, language: string = 'c'): void { + let code = ''; + let fileExtension = language; let document: vscode.TextDocument; - if (this.isDocument(input) && input.languageId === 'c') { + if (this.isDocument(input) && (input.languageId === 'c' || input.languageId === 'boogie')) { document = input; - cCode = document.getText(); + code = document.getText(); + fileExtension = vscode.window.activeTextEditor?.document.uri.fsPath.split('.').pop()!; } else if (typeof input === 'string') { - cCode = input; + code = input; } if (!this.isLocked()) { this.lockUltimate(); this.outputChannel.clear(); this.showProgressInStatusBar('Fetching Ultimate results...'); - this.fetchResults(cCode.trim()) + this.fetchResults(code.trim(), fileExtension) .then((response) => this.parseResponse(response)) + .then(() => this.pollResults()) + .then(() => this.outputChannel.show()) .then(() => this.printResultsToOutput()) .then(() => this.printResultsToLog()) .then(() => this.embedDiagnosticInfoInto(document)) @@ -61,19 +53,27 @@ export class UltimateByHttp extends UltimateBase { } } - public fetchResults(cCode: string): Promise { - let values = 'action=execute'; - values += '&code=' + encodeURIComponent(cCode); - values += - '&cAutomizer_deunifreiburginformatikultimatepluginsgeneratorcacsl2boogietranslatorcheckforthemainprocedureifallallocatedmemorywasfreed=false'; - values += - '&cAutomizer_deunifreiburginformatikultimatepluginsgeneratorcacsl2boogietranslatorcheckabsenceofsignedintegeroverflows=false'; - values += '&taskID=AUTOMIZER_C&tcID=cAutomizer'; + public fetchResults(code: string, fileExtension: string): Promise { + let body = { + action: 'execute', + code: code, + toolchain: { + id: 'cAutomizer', + }, + /* eslint-disable @typescript-eslint/naming-convention */ + code_file_extension: '.' + fileExtension, + user_settings: this.getSettingsFromFile(), + ultimate_toolchain_xml: this.getToolchainFromFile(), + /* eslint-enable @typescript-eslint/naming-convention */ + }; + + let defaultPort = this.apiUrl.protocol === 'http:' ? 80 : 443; let options = { - hostname: this.baseUrl.hostname, - port: 443, - path: '/tomcat/WebsiteEclipseBridge/if?' + values, + protocol: this.apiUrl.protocol, + hostname: this.apiUrl.hostname, + port: this.apiUrl.port || defaultPort, + path: this.apiUrl.pathname, method: 'POST', headers: { /* eslint-disable @typescript-eslint/naming-convention */ @@ -83,15 +83,87 @@ export class UltimateByHttp extends UltimateBase { }, }; - return httpsRequest(options); + return unifiedHttpsRequest(options, body); + } + + protected getToolchainFromFile(): string { + let toolchain = ` + CAutomizerTC + + + + + + + + `; + if ( + fs.existsSync(this.toolchainFilePath.fsPath) && + fs.lstatSync(this.settingsFilePath.fsPath).isFile() + ) { + toolchain = fs.readFileSync(this.toolchainFilePath.fsPath).toString(); + } + return toolchain; + } + + protected getSettingsFromFile(): string { + let settings = ''; + if ( + fs.existsSync(this.settingsFilePath.fsPath) && + fs.lstatSync(this.settingsFilePath.fsPath).isFile() + ) { + settings = fs.readFileSync(this.settingsFilePath.fsPath).toString(); + } + return '{"user_settings":[{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator","name":"Check absence of data races in concurrent programs","key":"Check absence of data races in concurrent programs","id":"cacsl2boogietranslator.check.absence.of.data.races.in.concurrent.programs","visible":true,"default":true,"type":"bool","value":false},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator","name":"Check absence of signed integer overflows","key":"Check absence of signed integer overflows","id":"cacsl2boogietranslator.check.absence.of.signed.integer.overflows","visible":true,"default":true,"type":"bool","value":false},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator","name":"Check division by zero","key":"Check division by zero","id":"cacsl2boogietranslator.check.division.by.zero","visible":false,"default":"IGNORE","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator","name":"Check if freed pointer was valid","key":"Check if freed pointer was valid","id":"cacsl2boogietranslator.check.if.freed.pointer.was.valid","visible":false,"default":false,"type":"bool","value":false},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator","name":"Pointer to allocated memory at dereference","key":"Pointer to allocated memory at dereference","id":"cacsl2boogietranslator.pointer.to.allocated.memory.at.dereference","visible":false,"default":"IGNORE","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator","name":"Check array bounds for arrays that are off heap","key":"Check array bounds for arrays that are off heap","id":"cacsl2boogietranslator.check.array.bounds.for.arrays.that.are.off.heap","visible":false,"default":"IGNORE","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator","name":"Check for the main procedure if all allocated memory was freed","key":"Check for the main procedure if all allocated memory was freed","id":"cacsl2boogietranslator.check.for.the.main.procedure.if.all.allocated.memory.was.freed","visible":false,"default":false,"type":"bool","value":false},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator","name":"If two pointers are subtracted or compared they have the same base address","key":"If two pointers are subtracted or compared they have the same base address","id":"cacsl2boogietranslator.if.two.pointers.are.subtracted.or.compared.they.have.the.same.base.address","visible":false,"default":"IGNORE","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator","name":"Pointer base address is valid at dereference","key":"Pointer base address is valid at dereference","id":"cacsl2boogietranslator.pointer.base.address.is.valid.at.dereference","visible":false,"default":"IGNORE","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator","name":"Overapproximate operations on floating types","key":"Overapproximate operations on floating types","id":"cacsl2boogietranslator.overapproximate.operations.on.floating.types","visible":false,"default":true,"type":"bool","value":false},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator","name":"Use constant arrays","key":"Use constant arrays","id":"cacsl2boogietranslator.use.constant.arrays","visible":false,"default":true,"type":"bool","value":false},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder","name":"Size of a code block","key":"Size of a code block","id":"rcfgbuilder.size.of.a.code.block","visible":false,"default":"SequenceOfStatements","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder","name":"SMT solver","key":"SMT solver","id":"rcfgbuilder.smt.solver","visible":false,"default":"External_DefaultMode","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction","name":"Compute Interpolants along a Counterexample","key":"Compute Interpolants along a Counterexample","id":"traceabstraction.compute.interpolants.along.a.counterexample","visible":false,"default":"FPandBP","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction","name":"SMT solver","key":"SMT solver","id":"traceabstraction.smt.solver","visible":false,"default":"External_ModelsAndUnsatCoreMode","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction","name":"Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG","key":"Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG","id":"traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg","visible":false,"default":true,"type":"bool","value":false},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction","name":"Positions where we compute the Hoare Annotation","key":"Positions where we compute the Hoare Annotation","id":"traceabstraction.positions.where.we.compute.the.hoare.annotation","visible":false,"default":"LoopsAndPotentialCycles","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction","name":"Trace refinement strategy","key":"Trace refinement strategy","id":"traceabstraction.trace.refinement.strategy","visible":false,"default":"CAMEL","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction","name":"Trace refinement exception blacklist","key":"Trace refinement exception blacklist","id":"traceabstraction.trace.refinement.exception.blacklist","visible":false,"default":"DEPENDING","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction","name":"Automaton type used in concurrency analysis","key":"Automaton type used in concurrency analysis","id":"traceabstraction.automaton.type.used.in.concurrency.analysis","visible":false,"default":"PETRI_NET","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction","name":"Apply one-shot large block encoding in concurrent analysis","key":"Apply one-shot large block encoding in concurrent analysis","id":"traceabstraction.apply.one-shot.large.block.encoding.in.concurrent.analysis","visible":false,"default":false,"type":"bool","value":false},{"plugin_id":"de.uni_freiburg.informatik.ultimate.boogie.procedureinliner","name":"Ignore calls to procedures called more than once","key":"Ignore calls to procedures called more than once","id":"procedureinliner.ignore.calls.to.procedures.called.more.than.once","visible":false,"default":"ONLY_FOR_SEQUENTIAL_PROGRAMS","type":"string"},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.blockencoding","name":"Create parallel compositions if possible","key":"Create parallel compositions if possible","id":"blockencoding.create.parallel.compositions.if.possible","visible":false,"default":false,"type":"bool","value":false},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.blockencoding","name":"Rewrite not-equals","key":"Rewrite not-equals","id":"blockencoding.rewrite.not-equals","visible":false,"default":false,"type":"bool","value":false},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.blockencoding","name":"Use SBE","key":"Use SBE","id":"blockencoding.use.sbe","visible":false,"default":true,"type":"bool","value":false},{"plugin_id":"de.uni_freiburg.informatik.ultimate.plugins.blockencoding","name":"Minimize states even if more edges are added than removed.","key":"Minimize states even if more edges are added than removed.","id":"blockencoding.minimize.states.even.if.more.edges.are.added.than.removed","visible":false,"default":false,"type":"bool","value":false}]}'; } private parseResponse(httpResponse: HttpResponse): void { let response = JSON.parse(httpResponse.body); this.results = response.results ? response.results : []; + this.requestId = response.requestId; this.error = response.error; } + private delay(ms: number): Promise { + return new Promise((resolve) => setTimeout(resolve, ms)); + } + + private pollResults(): Promise { + let defaultPort = this.apiUrl.protocol === 'http:' ? 80 : 443; + + let options = { + protocol: this.apiUrl.protocol, + hostname: this.apiUrl.hostname, + port: this.apiUrl.port || defaultPort, + path: this.apiUrl.pathname + '/job/get/' + this.requestId, + method: 'GET', + headers: { + /* eslint-disable @typescript-eslint/naming-convention */ + Accept: '*/*', + Connection: 'keep-alive', + /* eslint-enable @typescript-eslint/naming-convention */ + }, + }; + + return unifiedHttpsRequest(options).then((httpResponse): any => { + let response = JSON.parse(httpResponse.body); + switch (response.status.toLowerCase()) { + case 'done': + this.results = response.results; + Promise.resolve(response); + break; + case 'error': + Promise.reject(response.error); + break; + default: + // repeat polling recursively at given timeouts + return this.delay(this.refreshTimeInMilliseconds).then(() => + this.pollResults() + ); + } + }); + } + protected printResultsToOutput(): void { if (this.error) { this.outputChannel.appendLine(this.error); diff --git a/src/ultimateByLog.ts b/src/ultimateByLog.ts index 0aecbc7..c00a314 100644 --- a/src/ultimateByLog.ts +++ b/src/ultimateByLog.ts @@ -1,13 +1,10 @@ import * as cp from 'child_process'; -import * as fs from 'fs'; import * as path from 'path'; import * as vscode from 'vscode'; import { SingleUltimateResult, UltimateBase } from './ultimate'; export class UltimateByLog extends UltimateBase { private executable: path.ParsedPath; - private settingsFilePath = vscode.Uri.file(''); - private toolchainFilePath = vscode.Uri.file(''); protected response = new UltimateResultParser(''); constructor( @@ -18,26 +15,8 @@ export class UltimateByLog extends UltimateBase { ) { super(context); this.executable = path.parse(executable.fsPath); - this.setSettings(settings); - this.setToolchain(toolchain); - } - - public setup(): void {} - - public setToolchain(path: vscode.Uri): void { - if (fs.existsSync(path.fsPath) && path.fsPath.match(/(.*\.xml$)/)) { - this.toolchainFilePath = path; - } else { - console.log(`Toolchain file ${path} does not exist`); - } - } - - public setSettings(path: vscode.Uri): void { - if (fs.existsSync(path.fsPath) && path.fsPath.match(/(.*\.epf$)/)) { - this.settingsFilePath = path; - } else { - console.log(`Settings file ${path} does not exist`); - } + this.setSettingsFile(settings); + this.setToolchainFile(toolchain); } // TODO: Run on String! diff --git a/src/ultimateFactory.ts b/src/ultimateFactory.ts index bc9682d..9828afe 100644 --- a/src/ultimateFactory.ts +++ b/src/ultimateFactory.ts @@ -3,6 +3,11 @@ import { Ultimate } from './ultimate'; import { UltimateByHttp } from './ultimateByHttp'; import { UltimateByLog } from './ultimateByLog'; +const publicKnownAPIs = [ + 'https://ultimate.sopranium.de/api', + 'https://monteverdi.informatik.uni-freiburg.de', +]; + export class UltimateFactory { static createUltimateUsingLog( context: vscode.ExtensionContext, @@ -10,18 +15,25 @@ export class UltimateFactory { settings: vscode.Uri, toolchain: vscode.Uri ): Ultimate { - return new UltimateByLog(context, executable, settings, toolchain); + let newUltimateInstance = new UltimateByLog(context, executable, settings, toolchain); + return newUltimateInstance; } - static createUltimateUsingPublicApi( + static createUltimateUsingRestApi( context: vscode.ExtensionContext, - baseUrl?: string + apiUrl: string, + settings: vscode.Uri, + toolchain: vscode.Uri ): Ultimate { - let defaultUrl = 'https://monteverdi.informatik.uni-freiburg.de'; - return new UltimateByHttp(context, false, baseUrl || defaultUrl); - } + let newUltimateInstance = new UltimateByHttp(context, settings, toolchain, apiUrl); + let refreshTime: number = + vscode.workspace.getConfiguration().get('ultimate.refreshRate') || 3000; + + if (publicKnownAPIs.includes(apiUrl)) { + refreshTime = Math.min(3000, refreshTime); + } - static createUltimateUsingOwnDockerContainer(context: vscode.ExtensionContext): Ultimate { - return new UltimateByHttp(context, true); + newUltimateInstance.refreshTimeInMilliseconds = refreshTime; + return newUltimateInstance; } }