Skip to content

Commit

Permalink
diff fact , fonctions d'arité 0 et interdiction d'utiliser des macro…
Browse files Browse the repository at this point in the history 
…s dans les equations
  • Loading branch information
hugo committed Jul 17, 2024
1 parent 78465d6 commit 312015c
Show file tree
Hide file tree
Showing 5 changed files with 81 additions and 15 deletions.
2 changes: 1 addition & 1 deletion src/features/syntax_errors.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
});
Expand Down
33 changes: 31 additions & 2 deletions src/features/wellformedness_checks.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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++){
Expand All @@ -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){
Expand Down Expand Up @@ -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<vscode.Diagnostic, vscode.CodeAction>();
Expand All @@ -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)
};
6 changes: 1 addition & 5 deletions src/grammar/tree-sitter-tamarin/example_file.spthy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:

Expand Down
53 changes: 47 additions & 6 deletions src/symbol_table/create_symbol_table.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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[] =
[
Expand Down Expand Up @@ -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 === "="){
Expand All @@ -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 === "="){
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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))

}
}
}

Expand Down
2 changes: 1 addition & 1 deletion syntaxes/tamarin.tmLanguage.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
},
{
Expand Down

0 comments on commit 312015c

Please sign in to comment.