Merge pull request #15 from FahrJo/dev

merge of release 0.2.0

.vscode/settings.json

@@ -9,5 +9,22 @@
     // Turn off tsc task auto detection since we have the necessary tasks as npm scripts
     "typescript.tsc.autoDetect": "off",
     "typescript.format.enable": true,
-    "cmake.configureOnOpen": false
+    "cmake.configureOnOpen": false,
+    "cSpell.words": [
+        "Automizer",
+        "blockencoding",
+        "boogietranslator",
+        "cacsl",
+        "Hoare",
+        "informatik",
+        "interpolant",
+        "Interpolants",
+        "Overapproximate",
+        "procedureinliner",
+        "rcfgbuilder",
+        "rundefinition",
+        "syntaxchecker",
+        "traceabstraction",
+        "Unsat"
+    ]
 }

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)

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)

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": [
         {
@@ -32,9 +32,9 @@
             "properties": {
                 "ultimate.mode": {
                     "type": "string",
-                    "default": "REST API",
+                    "default": "rest-api",
                     "enum": [
-                        "REST API",
+                        "rest-api",
                         "stdout"
                     ],
                     "enumDescriptions": [
@@ -45,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": "",
@@ -56,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",

src/extension.ts

@@ -5,8 +5,8 @@ import { UltimateFactory } from './ultimateFactory';
 let ultimate: Ultimate;
 let verifyOnSave: boolean;
 
-// This method is called when your extension is activated
-// Your extension is activated the very first time the command is executed
+// This method is called when the extension is activated
+// The extension is activated the very first time the command is executed
 export async function activate(context: vscode.ExtensionContext): Promise<vscode.ExtensionContext> {
     initializeUltimate(context);
 
@@ -34,34 +34,40 @@ export async function activate(context: vscode.ExtensionContext): Promise<vscode
     return context;
 }
 
-function ultimateRunHandler() {
+function ultimateRunHandler(): void {
     if (vscode.window.activeTextEditor) {
         ultimate.runOn(vscode.window.activeTextEditor.document);
     }
 }
 
 // This method is called when your extension is deactivated
-export function deactivate() {
+export function deactivate(): void {
     ultimate.dispose();
 }
 
 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,

src/httpsRequest.ts

@@ -1,18 +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, data: any = '') {
+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) => {
-            // I believe chunks can simply be joined into a string
+        let httpModule = urlOptions.protocol === 'http:' ? http : https;
+        const req = httpModule.request(urlOptions, (res) => {
             const chunks: any = [];
 
             res.on('data', (chunk) => chunks.push(chunk));
@@ -31,7 +34,7 @@ export function httpsRequest(urlOptions: string | https.RequestOptions | url.URL
         });
 
         req.on('error', reject);
-        req.write(data, 'binary');
+        req.write(querystring.stringify(data), 'binary');
         req.end();
     });
     return promise;

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().results[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().results[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);
 });