Merge pull request #4 from hugotvn/master

V1.1.0 New welformedness checks and fixes.

CHANGELOG.md

@@ -1,5 +1,19 @@
 # Change Log
 
+## V1.1.0
+New welformedness checks and fixes.
+
+### New checks 
+ - Checks wether all variables in the right part of a macro are in the left part or public.
+- Checks wether all variable in the right part of an equation are in the left part.
+- Provides a quick fix for function names again with editing distance.
+- Checks wether built-ins are imported to use corresponding functions or symbols (provides a quick fix to import the right built-in).
+
+### Fixes 
+- Editing distance is now used to display all close tokens (distance < 3) and not the first one only.
+- `diff` is considered as a reserved function symbol so that there is no error while using it. 
+- Functions with arity 0 may be used without parenthesis.
+
 ## V1.0.1
 Fix package.json
 

Contribute/README_TREE_SITTER.md

@@ -1,25 +1,35 @@
- Using tree-sitter in the Tamarin plugin
+# Using tree-sitter in the Tamarin plugin
 
-### Importing the grammar 
+### Installing dependencies
+
+To install the required dependencies, one can use brew:
+
+```brew install tree-sitter docker podman```
+
+Then you need to initialize and start podman as follows:
+
+`podman machine init` and `podman machine start`
+
+### Importing the grammar
 All the files required to use the grammar in the plugin are located in src/grammar/tree-sitter-tamarin.
 
 To use tree-sitter with a new grammar, use the ```tree-sitter generate``` command.
 \
  ⚠️ this command creates all the files needed to use the grammar with Typescript, for example grammar.js, as well as json and C files. In particular, the parser is created.
 
 ### Importing the parser
-Then, to use the parser inside the vscode plugin, use: 
+Then, to use the parser inside the vscode plugin, use:
 \
-```tree-sitter build --wasm --output location_of_the_output```
+```tree-sitter build --wasm --output src/grammar/parser-tamarin.wasm```
 \
 To perform this command you need to have docker running or install the other applications suggested on tree sitter website:
 \
  https://tree-sitter.github.io/tree-sitter/creating-parsers#command-build
 \
 This command creates a dynamic .wasm library which enables you to use the parser inside the vscode plugin.
 
-### Using the parser  
-There are many ways to create an instance of the parser using a new grammar. Here we use the following approach: 
+### Using the parser
+There are many ways to create an instance of the parser using a new grammar. Here we use the following approach:
 \
 ```Typescript 
 import Parser =require( "web-tree-sitter");

Contribute/Readme_release.md

@@ -0,0 +1,23 @@
+## Documentation on how to release the extension 
+
+The plugin is available on two different websites :
+ - https://marketplace.visualstudio.com/items?itemName=tamarin-prover.tamarin-prover
+
+ - https://open-vsx.org/extension/tamarin-prover/tamarin-prover
+
+
+ For each website you will need an access token in order to publish the extension. This you can create using you azure dev ops account as described here :
+ \
+  https://code.visualstudio.com/api/working-with-extensions/publishing-extension
+ \
+ or your Eclipse account as described here : https://github.com/eclipse/openvsx/wiki/Publishing-Extensions
+\
+For vscode the access token is required before publishing using ```vsce login private_access_token```.
+
+In order to push a new version or release you will need to use the following commands : 
+```vsce publish version_n°``` for vscode and ```npx ovsx publish -p private_access_token``` for openVSX
+
+Make sure to remove all the errors otherwise it won't publish. The error messages are quite clear to help you debug. For vscode you can specify in the ```package.json``` file the files you want to include in the extension. Make sure everything necessary to run your code is present. 
+
+
+

README.md

@@ -16,6 +16,10 @@ Features:
     - Checks the arity of facts and functions.
     - Checks whether a lemma uses free terms.
     - Checks whether all facts in the premises of the rules appear in the conclusion of some (other) rule (provides a quick fix by using the closest exisiting fact, based on editing distance).
+    - Checks wether all variables in the right hand side of a macro are in the left hand side or public.
+    - Checks wether all variable in the right hand side of an equation are in the left hand side.
+    - Provides a quick fix for function names (suggestions based on editing distance).
+    - Checks wether built-ins are imported when encountering corresponding functions or symbols (provides a quick fix to import the right built-in).
 
     This is a subset of the checks performed by Tamarin. For more details on Tamarin's wellformedness checks, see the corresponding [Tamarin Prover manual section](https://tamarin-prover.com/manual/master/book/010_modeling-issues.html).
 

TODO.md

@@ -0,0 +1,2 @@
+- [] Manage preprocessor #IFDEF 
+- [] Manage preprocessor #INCLUDE

package.json

@@ -1,6 +1,6 @@
 {
   "name": "tamarin-prover",
-  "version": "1.0.1",
+  "version": "1.1.0",
   "engines": {
     "vscode": "^1.90.0"
   },
@@ -180,8 +180,11 @@
     "binding.gyp",
     "prebuilds/**",
     "bindings/node/*",
-    "src/**",
-    "syntaxes/**",
+    "src/features/**",
+    "src/grammar/parser-tamarin.wasm",
+    "src/features/**",
+    "src/extension.ts",
+    "syntaxes/tamarin.tmLanguage.json",
     "out/**",
     "LICENSE",
     "package.json",

src/extension.ts

@@ -1,5 +1,4 @@
 import * as vscode from 'vscode';
-import * as child_process from 'child_process';
 import path = require('path');
 import { runShortcut } from './features/run_shortcut';
 import { display_syntax_errors } from './features/syntax_errors';
@@ -22,7 +21,7 @@ export function activate(context: vscode.ExtensionContext) {
 
     console.log('Tamarin extension is now active');
 
-    //Fonctionnalités du plugin
+    //Plugin Features
      plugin_features(context);
 
 

src/features/rename.ts

@@ -1,6 +1,6 @@
 import * as vscode from 'vscode'
 import { symbolTables } from './syntax_errors';
-import { DeclarationType, TamarinSymbol, TamarinSymbolTable } from '../symbol_table/create_symbol_table';
+import { CreateSymbolTableResult, DeclarationType, TamarinSymbol, TamarinSymbolTable } from '../symbol_table/create_symbol_table';
 
 export function get_symbol(range : vscode.Range, symbol_table : TamarinSymbolTable): TamarinSymbol|null{
     for (let k = 0 ; k < symbol_table.getSymbols().length; k++){
@@ -11,7 +11,8 @@ export function get_symbol(range : vscode.Range, symbol_table : TamarinSymbolTab
     return null;
 }
 
-async function replace_symbol(symbol : TamarinSymbol, editor : vscode.TextEditor, newName : string ){
+/* Function used to replace a symbol by the user choice */ 
+ function replace_symbol(symbol : TamarinSymbol, editor : vscode.TextEditor, newName : string, edit : vscode.WorkspaceEdit): void{
   if (symbol.name === undefined) {
     console.error("Cannot replace symbol with undefined name");
     return;
@@ -23,25 +24,17 @@ async function replace_symbol(symbol : TamarinSymbol, editor : vscode.TextEditor
   const newNameLength = newName.length;
   const newRange = new vscode.Range(
     range.start,
-    editor.document.positionAt(editor.document.offsetAt(range.start) + newNameLength)
+    editor.document.positionAt(editor.document.offsetAt(range.start) + newNameLength - oldNameLength)
   );
-  const edit = new vscode.WorkspaceEdit();
-  edit.replace(editor.document.uri, range, newText);
-  await vscode.workspace.applyEdit(edit);
   symbol.name_range = newRange;
   symbol.name = newName;
-  // Mettre à jour la position de fin du symbole en utilisant la longueur du nouveau nom et la longueur de l'ancien nom
-  const delta = newNameLength - oldNameLength;
-  symbol.name_range = new vscode.Range(
-    symbol.name_range.start,
-    symbol.name_range.end.translate(0, delta)
-  );
+  edit.replace(editor.document.uri, range, newText);
 }
 
 
 export function RenameCommand(context : vscode.ExtensionContext){
 
-    const  provideRenameCodeAction = vscode.commands.registerCommand("Rename", async () => {
+    const provideRenameCodeAction = vscode.commands.registerCommand("Rename", async () => {
         const activeEditor = vscode.window.activeTextEditor;
         if (!activeEditor) {
             vscode.window.showErrorMessage("No active text editor");
@@ -50,7 +43,7 @@ export function RenameCommand(context : vscode.ExtensionContext){
 
         const activeFile = activeEditor.document.uri.path.split('/').pop(); 
         if(activeFile){
-            const symbolTable = symbolTables.get(activeFile);
+            const symbolTable : CreateSymbolTableResult|undefined = symbolTables.get(activeFile);
             if (!symbolTable) {
                 vscode.window.showErrorMessage("No symbol table for this file");
                 return;
@@ -77,43 +70,44 @@ export function RenameCommand(context : vscode.ExtensionContext){
         const range = new vscode.Range(startPos, endPos);
         const corresponding_symbol = get_symbol(range, symbolTable.symbolTable)
 
-
-
         const newName = await vscode.window.showInputBox({
             placeHolder: "Enter the new name"
         });
         if (!newName) {
             vscode.window.showErrorMessage("No new name provided");
             return;
         }
-
-
         let replace_count: number = 0;
+        const edit = new vscode.WorkspaceEdit();
+        const chosenSymbolName = corresponding_symbol?.name;
+
         for(let k = 0 ; k < symbolTable.symbolTable.getSymbols().length ; k++){
             let current_symbol = symbolTable.symbolTable.getSymbol(k);
             if(current_symbol.declaration === DeclarationType.PRVariable || current_symbol.declaration === DeclarationType.ActionFVariable || current_symbol.declaration === DeclarationType.CCLVariable){
-                if(corresponding_symbol?.context === current_symbol.context && corresponding_symbol?.name === current_symbol.name){
+                if(corresponding_symbol?.context === current_symbol.context && chosenSymbolName === current_symbol.name){
                     replace_count ++
-                    replace_symbol(current_symbol, activeEditor, newName);
-                } 
+                    replace_symbol(current_symbol, activeEditor, newName, edit);
+                }
             }
             else if (current_symbol.declaration === DeclarationType.LemmaVariable){
-                if(current_symbol.associated_qf?.id === corresponding_symbol?.associated_qf?.id && current_symbol.name === corresponding_symbol?.name){
+                if(current_symbol.associated_qf?.id === corresponding_symbol?.associated_qf?.id && current_symbol.name === chosenSymbolName){
                     replace_count ++
-                    replace_symbol(current_symbol, activeEditor, newName);
+                    replace_symbol(current_symbol, activeEditor, newName, edit);
                 }
             }
-            else if( current_symbol.name === corresponding_symbol?.name && current_symbol.declaration === corresponding_symbol?.declaration){
+            else if( current_symbol.name === chosenSymbolName && current_symbol.declaration === corresponding_symbol?.declaration){
                 replace_count ++
-                replace_symbol(current_symbol, activeEditor, newName);
+                replace_symbol(current_symbol, activeEditor, newName, edit);
             }
         }
 
+        vscode.workspace.applyEdit(edit);
+
         if(replace_count === 0){
             vscode.window.showErrorMessage("No such token");
         }
 
-        }
+    }
     });
 
     context.subscriptions.push(provideRenameCodeAction);

src/features/syntax_errors.ts

@@ -9,7 +9,7 @@ let diagnostics = vscode.languages.createDiagnosticCollection('Tamarin');
 export let symbolTables = new Map<string, CreateSymbolTableResult>();
 
 
-//Permet d'obtenir l'indice du noeud actuel par rapport a son père
+//given an node returns his index in his father's children list 
 function get_child_index(node : Parser.SyntaxNode): number|null{
     if(node.parent === null ){
         return null;
@@ -38,7 +38,9 @@ export function getName(node : Parser.SyntaxNode| null, editor: vscode.TextEdito
 
 
 
-
+/* Function used to detect syntax errors sent by the parser with MISSING or ERROR nodes,
+I tried to personnalize error messages according to the different cases
+I did the most common ones*/
 export async function detect_errors(editeur: vscode.TextEditor): Promise<Parser.SyntaxNode|void> {
     let editor = editeur;
     await Parser.init();
@@ -94,7 +96,7 @@ export async function detect_errors(editeur: vscode.TextEditor): Promise<Parser.
         }
     }
 
-    // Trouve les noeuds d'erreur ou de warning
+    // Find error or warning nodes
     function findMatches(node : Parser.SyntaxNode, editeur: vscode.TextEditor ) {
         if ((node.isMissing)) {
             let myId = get_child_index(node);
@@ -143,13 +145,24 @@ export async function detect_errors(editeur: vscode.TextEditor): Promise<Parser.
                 textDecoration: 'none; opacity: 0.5; background-color: none; border: none;',
             }
         });
+        //Part to detect if there is code after the end
         let hasContentAfterEnd = false;
         const text = editor.document.getText();
+        let inMultiLineComment = false;
         for (let lineNum = endPosition.line + 1; lineNum <= endOfDocumentPosition.line; lineNum++) {
             const line = text.split('\n')[lineNum];
-            if (line.trim() !== '') {
-                hasContentAfterEnd = true;
-                break;
+            // Check if the line is not empty and is not a comment
+            if (!inMultiLineComment) {
+                if (line.trim().startsWith('/*')) {
+                    inMultiLineComment = true;
+                } else if (line.trim() !== '' && !line.trim().startsWith('//')) {
+                    hasContentAfterEnd = true;
+                    break;
+                }
+            } else {
+                if (line.trim().endsWith('*/')) {
+                    inMultiLineComment = false;
+                }
             }
         }
         if (!hasContentAfterEnd) {
@@ -178,7 +191,7 @@ export async function detect_errors(editeur: vscode.TextEditor): Promise<Parser.
 }
 
 
-//Fonction principale 
+//Main function
 export function display_syntax_errors(context: vscode.ExtensionContext): void {
     let first_time = 0;
     const changed_content = vscode.workspace.onDidChangeTextDocument((event) => {
@@ -191,13 +204,13 @@ export function display_syntax_errors(context: vscode.ExtensionContext): void {
                     if (!fileName) {
                         throw new Error('Could not determine file name');
                     }  
-                    symbolTables.set(fileName, table); 
+                    symbolTables.set(fileName, table);
+                    //console.log(symbolTables)   // usefull for debugging symbol table 
                 }
             }
         });
     });
 
-    // Appeler les fonctions du plugin pour tous les éditeurs visibles
     if(first_time === 0){
     first_time ++
     vscode.window.visibleTextEditors.forEach(async (editor) => {