Update API to new backend version

FahrJo · Jun 5, 2023 · 229b56d · 229b56d
1 parent 228c57f
commit 229b56d
Show file tree

Hide file tree

Showing 11 changed files with 219 additions and 121 deletions.
diff --git 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
@@ -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. <https://monteverdi.informatik.uni-freiburg.de/> or <https://ultimate.sopranium.de>.
+Connection to a public server running Ultimate Automizer, e.g. <https://ultimate.sopranium.de/api>.
 
-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
diff --git 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,17 +22,19 @@
     "categories": [
         "Programming Languages"
     ],
-    "activationEvents": [],
+    "activationEvents": [
+        "onLanguage:c"
+    ],
     "main": "./out/extension.js",
     "contributes": {
         "configuration": {
             "title": "Ultimate Automizer",
             "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
@@ -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
@@ -1,20 +1,21 @@
 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;
     headers: http.IncomingHttpHeaders;
     body: string;
 }
 
-export function httpsRequest(
-    urlOptions: string | https.RequestOptions | url.URL,
+export function unifiedHttpsRequest(
+    urlOptions: https.RequestOptions,
     data: any = ''
 ): Promise<HttpResponse> {
     let promise = new Promise<HttpResponse>((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
@@ -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
@@ -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;