diff --git a/src/features/syntax_errors.ts b/src/features/syntax_errors.ts index 1188391..33d35c2 100644 --- a/src/features/syntax_errors.ts +++ b/src/features/syntax_errors.ts @@ -191,7 +191,7 @@ 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); } } }); diff --git a/src/features/wellformedness_checks.ts b/src/features/wellformedness_checks.ts index c16d67d..5f1bb12 100644 --- a/src/features/wellformedness_checks.ts +++ b/src/features/wellformedness_checks.ts @@ -99,6 +99,22 @@ export function check_reserved_facts(node : Parser.SyntaxNode, editor : vscode.T else if((fact_name === ReservedFacts[3] || fact_name === ReservedFacts[4] || fact_name === ReservedFacts[5]) && node.parent?.grammarType === 'simple_rule' ){ build_warning_display(child, editor, diags, "You are not supposed to use KD KU or action K in a rule "); } + else if( fact_name === ReservedFacts[6]){ + if(get_arity(child.child(2)?.children) != 2){ + build_error_display(child, editor, diags, "Error : incorrect arity for diff fact, 2 arguments expected") + } + } + } + else if (child.grammarType === 'nary_app'){ + const fact_name_node = child.child(0); + if (fact_name_node !== null && fact_name_node !== undefined) { + const fact_name = getName(fact_name_node, editor); + if(fact_name === ReservedFacts[6]){ + if(node.grammarType === DeclarationType.Equation || node.grammarType === 'mset_term'){ + build_warning_display(child, editor, diags , "Warning : diff fact cannot be used in an equation") + } + } + } } else { check_reserved_facts(child, editor, diags) @@ -226,7 +242,7 @@ function check_variable_is_defined_in_premise(symbol_table : TamarinSymbolTable, for( let i = 0 ; i < symbol_table.getSymbols().length; i++){ let current_symbol = symbol_table.getSymbol(i); if(current_symbol.type === '$'){continue}; // Do not take into account public variables - if(current_symbol.declaration === DeclarationType.CCLVariable){ + if(current_symbol.declaration === DeclarationType.CCLVariable || current_symbol.declaration === DeclarationType.ActionFVariable){ let current_context = current_symbol.context; let is_break = false; for (let j = 0; j < symbol_table.getSymbols().length; j++){ @@ -243,7 +259,7 @@ function check_variable_is_defined_in_premise(symbol_table : TamarinSymbolTable, } } if(!is_break){ - build_error_display(current_symbol.node, editor, diags, "Error: this variable is used in conclusion but doesn't appear in premise"); + build_error_display(current_symbol.node, editor, diags, "Error: this variable is used in the second part of the rule but doesn't appear in premise"); } } else if ((current_symbol.declaration === DeclarationType.LinearF || current_symbol.declaration === DeclarationType.PersistentF) && current_symbol.node.parent?.grammarType === DeclarationType.Premise){ @@ -450,6 +466,18 @@ function check_free_term_in_lemma(symbol_table : TamarinSymbolTable, editor: vsc } } +function check_macro_not_in_equation(symbol_table : TamarinSymbolTable, editor: vscode.TextEditor, diags: vscode.Diagnostic[]){ + for(let symbol of symbol_table.getSymbols()){ + if(symbol.declaration === DeclarationType.NARY){ + for ( let macros of symbol_table.getSymbols()){ + if(macros.declaration === DeclarationType.Macro && macros.name === symbol.name && symbol.context.grammarType === DeclarationType.Equation){ + build_error_display(symbol.node, editor, diags, "Error : a macro shoud not be used in an equation ") + } + } + } + } +} + const fixMap = new Map(); @@ -475,4 +503,5 @@ export function checks_with_table(symbol_table : TamarinSymbolTable, editor: vsc check_action_fact(symbol_table, editor, diags); check_function_macros_and_facts_arity(symbol_table, editor, diags); check_free_term_in_lemma(symbol_table, editor, diags); + check_macro_not_in_equation(symbol_table, editor, diags) }; diff --git a/src/grammar/tree-sitter-tamarin/example_file.spthy b/src/grammar/tree-sitter-tamarin/example_file.spthy index c08f5c1..a330ef3 100644 --- a/src/grammar/tree-sitter-tamarin/example_file.spthy +++ b/src/grammar/tree-sitter-tamarin/example_file.spthy @@ -10,12 +10,8 @@ Date: June 2024 theory WideMouthedFrog begin -functions : strike/2 -equations : strike(a,b) = a + b * 2, - femme(bb) = a + b - -macros : balabla(a,b,c) = h(a) + b * d +equations : Blablac(c,a,b) = c + b + diff(mazvom, vzzvzv) lemma coucou: diff --git a/src/symbol_table/create_symbol_table.ts b/src/symbol_table/create_symbol_table.ts index f00f25c..2964c43 100644 --- a/src/symbol_table/create_symbol_table.ts +++ b/src/symbol_table/create_symbol_table.ts @@ -157,7 +157,7 @@ export enum variable_types{ TEMP = '#' } -export const ReservedFacts: string[] = ['Fr','In','Out','KD','KU','K'] ; +export const ReservedFacts: string[] = ['Fr','In','Out','KD','KU','K','diff'] ; const ExistingBuiltIns : string[] = [ @@ -232,7 +232,7 @@ class SymbolTableVisitor{ for(let grandchild of child.children){ if(grandchild.grammarType === DeclarationType.Macro){ this.registerfucntion(grandchild, DeclarationType.Macro, getName(grandchild.child(0),editor),get_macro_arity(grandchild.children),root, get_range(grandchild.child(0),editor)) - this.register_facts_searched(grandchild,editor, root,DeclarationType.NARY ) + this.register_facts_searched(grandchild,editor, grandchild,DeclarationType.NARY ) let eqcount = 0 ; for(let ggchild of grandchild.children){ if(ggchild.grammarType === "="){ @@ -248,7 +248,8 @@ class SymbolTableVisitor{ } } else if (grandchild.grammarType === DeclarationType.Equation){ - this.register_facts_searched(grandchild, editor, root, DeclarationType.NARY); + check_reserved_facts(grandchild, editor, diags) + this.register_facts_searched(grandchild, editor, grandchild, DeclarationType.NARY); let eqcount = 0 ; for(let ggchild of grandchild.children){ if(ggchild.grammarType === "="){ @@ -323,7 +324,19 @@ class SymbolTableVisitor{ let vars: Parser.SyntaxNode[] = find_variables(node); for(let k = 0; k < vars.length; k++){ if(vars[k].grammarType === DeclarationType.MVONF){ - this.registerident(vars[k], type, getName(vars[k].child(0), editor),root, get_range(vars[k].child(0), editor)) + let isregistered = false + for(let symbol of this.symbolTable.getSymbols()){ + if(symbol.declaration === DeclarationType.Functions){ + if(symbol.name === getName(vars[k], editor)){ + isregistered = true; + this.registerfucntion(vars[k], DeclarationType.NARY, symbol.name,0,root, get_range(vars[k],editor) ) + } + } + else {continue;} + } + if(! isregistered){ + this.registerident(vars[k], type, getName(vars[k].child(0), editor),root, get_range(vars[k].child(0), editor)) + } } else{ this.registerident(vars[k], type, getName(vars[k].child(1), editor),root, get_range(vars[k].child(1), editor), vars[k].child(0)?.grammarType) @@ -333,7 +346,19 @@ class SymbolTableVisitor{ private register_vars_left_macro_part(node :Parser.SyntaxNode, type : DeclarationType, editor : vscode.TextEditor, root : Parser.SyntaxNode){ if(node.grammarType === DeclarationType.MVONF){ - this.registerident(node, type, getName(node.child(0), editor),root, get_range(node.child(0), editor)) + let isregistered = false + for(let symbol of this.symbolTable.getSymbols()){ + if(symbol.declaration === DeclarationType.Functions){ + if(symbol.name === getName(node, editor)){ + isregistered = true; + this.registerfucntion(node, DeclarationType.NARY, symbol.name,0,root, get_range(node,editor) ) + } + } + else {continue;} + } + if(! isregistered){ + this.registerident(node, type, getName(node.child(0), editor),root, get_range(node.child(0), editor)) + } } else if (node.grammarType === 'pub_var' ||node.grammarType === 'fresh_var' || node.grammarType === 'nat_var'|| node.grammarType === 'temporal_var'){ this.registerident(node, type, getName(node.child(1), editor),root, get_range(node.child(1), editor), node.child(0)?.grammarType) @@ -351,7 +376,19 @@ class SymbolTableVisitor{ } if(vars[k].parent !== null){ if(vars[k].grammarType === DeclarationType.MVONF || (vars[k].grammarType === DeclarationType.TMPV && vars[k].children.length === 1)){ - this.registerident(vars[k], type, getName(vars[k].child(0), editor),context, get_range(vars[k].child(0), editor)) + let isregistered = false + for(let symbol of this.symbolTable.getSymbols()){ + if(symbol.declaration === DeclarationType.Functions){ + if(symbol.name === getName(vars[k], editor)){ + isregistered = true; + this.registerfucntion(vars[k], DeclarationType.NARY, symbol.name,0,context, get_range(vars[k],editor) ) + } + } + else {continue;} + } + if(! isregistered){ + this.registerident(vars[k], type, getName(vars[k].child(0), editor),context, get_range(vars[k].child(0), editor)) + } } else{ this.registerident(vars[k], type, getName(vars[k].child(1), editor),context,get_range(vars[k].child(1), editor) , vars[k].child(0)?.grammarType) @@ -394,6 +431,10 @@ class SymbolTableVisitor{ this.registerfucntion(vars[k], convert(vars[k].grammarType) , getName(vars[k].child(0),editor),arity, root, get_range(vars[k].child(0),editor)) } } + else{ + this.registerfucntion(vars[k], convert(vars[k].grammarType) , getName(vars[k].child(0),editor),0, root, get_range(vars[k].child(0),editor)) + + } } } diff --git a/syntaxes/tamarin.tmLanguage.json b/syntaxes/tamarin.tmLanguage.json index aa49f51..9a9cc3e 100644 --- a/syntaxes/tamarin.tmLanguage.json +++ b/syntaxes/tamarin.tmLanguage.json @@ -23,7 +23,7 @@ "name": "keyword.control" }, { - "match": "\\b(xor|aenc|adec|senc|sdec|sign|verify|Eq|eq|hashing|signing|revealing-signing|diffie-hellman|symmetric-encryption|asymmetric-encryption|multiset|bilinear-pairing|h|H|sk|pk|Fr|In|Out|K)\\b", + "match": "\\b(xor|aenc|adec|senc|sdec|sign|verify|Eq|eq|hashing|signing|revealing-signing|diffie-hellman|symmetric-encryption|asymmetric-encryption|multiset|bilinear-pairing|h|H|sk|pk|Fr|In|Out|K|diff)\\b", "name": "variable.language" }, {