Soufflé Language Server

[jdaridis]

As part of my Undergraduate Thesis, I developed a Language Server and a plugin for VS Code for Soufflé. For now, the only client supported is VS Code, but since it is based on LSP it is trivial to extend support for all major source-code editors.

https://github.com/jdaridis/souffle-lsp-plugin

https://marketplace.visualstudio.com/items?itemName=i-daridis.souffle-lang-server

[psubotic]

Awesome.

…

On Thu, Nov 3, 2022 at 12:16 PM Ioannis Daridis ***@***.***> wrote: As part of my Undergraduate Thesis, I developed a Language Server and a plugin for VS Code for Soufflé. For now, the only client supported is VS Code, but since it is based on LSP it is trivial to extend support for all major source-code editors. https://github.com/jdaridis/souffle-lsp-plugin https://marketplace.visualstudio.com/items?itemName=i-daridis.souffle-lang-server — Reply to this email directly, view it on GitHub <#2350>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAC3OOJIRCZ4WGQWEEPPJLDWGONJJANCNFSM6AAAAAARWAV2AQ> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[XiaowenHu96]

Impressive!

[mingodad]

Great work !

I'm just testing this extension right now and noticed it's lacking syntax highlight for keywords/strings, and it's nice the goto definition and other niceties.
I just updated the EBNF for railroad diagram here #1970 I think it can help other parser creators.

[jdaridis]

There is an existing plugin for Soufflé syntax highlight, so I didn't re-implement it.

[mingodad]

And looking at the parser https://github.com/jdaridis/souffle-lsp-plugin/blob/master/grammar/Souffle.g4 I can see it's missing some new added elements like:

INCLUDE ::= ".include"
ONCE ::= ".once"
...
FOLD ::= "fold"
...

[jdaridis]

I am adding them

[mingodad]

Thank you for pointing out the need to use/install the other vscode plugin.

[mingodad]

I just tested using https://www.bottlecaps.de/convert/ to convert and generate railroad diagram from your https://github.com/jdaridis/souffle-lsp-plugin/blob/master/grammar/Souffle.g4 and it works fine, I'm comparing now the railroad diagram generated from both yours and mine that doesn't include the detailed lex data like yours.

[jdaridis]

Note that the grammar I use has some additions/modifications to the standard one. I made some changes that helped me with the preprocessor parsing.

[mingodad]

I noticed that you have preprocessor_macro in several places that the original parser doesn't seem to have, like:

qualified_name
         ::= ( IDENT | preprocessor_macro ) ( '.' IDENT )*
...
term     ::= '!'* ( atom | constraint | '(' disjunction ')' | preprocessor_macro )
...

There is a reason for it ?

[mingodad]

I think that you already answered it, thank you !

[mingodad]

Also you are missing something in args rule:
Your:

arg      ::= STRING
...
           | ( 'autoinc' '(' | '(' arg | 'as' '(' arg ',' qualified_name | ( '@' IDENT | functor_built_in ) '(' arg_list ) ')'
...

Actual souffle:

arg      ::= STRING
...
           | AT ( IDENT LPAREN arg_list RPAREN | AT IDENT arg_list COLON arg COMMA aggregate_body )
...

[jdaridis]

I think that the grammar is okay now.

[mingodad]

How do you test it ?
Do you have a simple build that only lex/parse and run through all *.dl files in souffle/tests ?

[jdaridis]

When I developed it, I set the parser to bail out and throw an exception when it fails and catch the exception, incrementing an error counter.
Then I test it by hand in all the major Souffle libraries, those listed on the Souffle site (Doop, GIgahorse etc), and see how many errors I counted. So far it covers 100% of the code in the libraries (apart from 2 which have custom preprocessor scripts).

[jdaridis]

I attach as a reference the table with the results I got from that testing.

[mingodad]

I'm testing it in vscodium with the source file shown bellow and noticed it can't recognize the rule Car inside count:{Car(_,"blue")} to jump to definition but it does recognize it in other places.

//souffle -D- arithRec.dl
.decl A(n: number)
.output A
A(1).
A(x+1) :- A(x), x < 9 .

.decl B(x:number)
.output B
B(0 lor 2).

.decl C(x: symbol)
C("a"). C("b"). C("c"). C("d").

.decl D(x: symbol, y: number)
.output D
D(x, autoinc()) :- C(x).

.decl Car(name: symbol, colour:symbol)
Car("Audi", "blue").
Car("VW", "red").
Car("BMW", "blue").

.decl BlueCarCount(x: number)
BlueCarCount(c) :- c = count:{Car(_,"blue")}.
 .output BlueCarCount

 .decl E(n:number)
E(1). E(10). E(100).
.decl MaxE(x: number)
MaxE(y) :- y = max x:{E(x)}.
 .output MaxE

// Pair of numbers
.type Pair = [a:number, b:number]

.decl F(p: Pair)  // declare a set of pairs
.output F
F([1,2]).
F([3,4]).
F([4,5]).

.decl Flatten(a:number, b:number) output
Flatten(a,b) :- F([a,b]).

[jdaridis]

This is not a problem with the grammar, it parses correctly. In the initial version, as part of my Thesis, I collected information about the basic structure of a Souffle program, leaving some functionality behind (eg aggregate functions). There is room for improvement for a more complete tool

[mingodad]

Thank you again for your great work so far !

[mingodad]

A suggestion for an improvement showing the documentation comment, I noticed that when hover over a predicate a tool-tip appear showing the declaration and an one line comment before it, but not multi line comment:

// The `index`'th step of `insn` points to `alloc` and resulted from a sequence
  // of index operations starting with `baseAlloc` at index 0.
  .decl gep_points_to(?insn: GetElementPtrInstruction,
                      ?index: GepIndex,
              ?baseAlloc: Allocation,
              ?alloc: Allocation)

// Indexing the pointer with a zero offset is a no-op.
  // E.g.,
  //   `getelementptr i32, i32* %MyVar, i64 0` points to
  //   `some_alloc` if `%MyVar` points to `some_alloc`
  gep_points_to(?insn, 0, ?alloc, ?alloc) :-
    gep_indexes_from(?insn, 0, ?alloc, ?alloc, ?type),
    pointer_type(?type),
    gep_zero_index_offset(?insn, 0).

The tool-tip shown when hover over gep_points_to(?insn, 0, ?alloc, ?alloc):

gep_points_to(?insn: GetElementPtrInstruction, ?index: GepIndex, ?baseAlloc: Allocation, ?alloc: Allocation)
of index operations starting with baseAlloc at index 0.

Would be nice to show the full documentation comment.

[jdaridis]

This is a known issue, the tool supports multiline comments if written in the C style /* */. We are working with the Gigahorse team to port their comments to this style to support multiline tooltips.

For now, the /* */ style of comments is fully supported.

[mingodad]

Thank you for reply !
I did tried before using /**/ style comments before posting my suggestion here but I was not getting the full comment, but after your reply I did it again and found that it only shows if the file is saved.

[jdaridis]

Yes, the server reparses the document on save, and the changes one makes are reflected on the server. It is this way for every change to the document, not only comments. I did that to save on processing power rather than parsing the document continuously.

[mingodad]

Thank you again for reply !
Another suggestion would be to maybe merge or show the specific comment for a predicate, see bellow an example where would be nice to have a tool-tip that merge or show the specific (matching arguments) when hover over gep_indexes_from(?insn, 0, ?alloc, ?alloc, ?type):

  /* The `index`'th step of `insn` indexes from `alloc` at type `type` and resulted
   from indexing `baseAlloc` at index 0. `baseAlloc` is recorded to track which
   allocation contexts the points-to information for `alloc` should be recorded
   for when translating `gep_points_to` facts to `var_points_to` facts.
  */
  .decl gep_indexes_from(?insn: GetElementPtrInstruction,
                        ?index: GepIndex,
                ?baseAlloc: Allocation,
                ?alloc: Allocation,
                ?type: Type)

  /* The first index of a getelementptr instr indexes any allocation pointed
   to by its base operand.
   */
  gep_indexes_from(?insn, 0, ?alloc, ?alloc, ?type) :-
    !gep_is_vector_based(?insn),
    getelementptr_instr_base(?insn, ?base),
    operand_points_to(_, ?alloc, _, ?base),
    getelementptr_instr_base_type(?insn, ?type).

  /* The remaining indexes of a getelementptr instr index from the allocations
   pointed to by the previous index, filtered by GEP type compatibility, as
   described above.
   */
  gep_indexes_from(?insn, ?n, ?baseAlloc, ?alloc, ?type) :-
    getelementptr_instr_index(?insn, ?n, _),
    gep_points_to(?insn, ?n - 1, ?baseAlloc, ?alloc),
    getelementptr_instrterm_type(?insn, ?n, ?type),
    _alloc_type_and_path(?alloc, ?allocType, ?component),
    _gep_type_compatible(?type, ?allocType, ?component).

  /* The `index`'th step of `insn` points to `alloc` and resulted from a sequence
   of index operations starting with `baseAlloc` at index 0.
   */
  .decl gep_points_to(?insn: GetElementPtrInstruction,
                      ?index: GepIndex,
              ?baseAlloc: Allocation,
              ?alloc: Allocation)

  //------------------------------------------------------------------------------
  // Handling the first index
  //
  // The first index operation in a getelementptr instr is special because
  // it is the only index operation that operates on a pointer. (See "The Often
  // Misunderstood GEP Instruction": https://llvm.org/docs/GetElementPtr.html)
  //------------------------------------------------------------------------------

  /* Indexing the pointer with a zero offset is a no-op.
   E.g.,
     `getelementptr i32, i32* %MyVar, i64 0` points to
     `some_alloc` if `%MyVar` points to `some_alloc`
     */
  gep_points_to(?insn, 0, ?alloc, ?alloc) :-
    gep_indexes_from(?insn, 0, ?alloc, ?alloc, ?type),  //!!!<<<  When hovering over here !!!!!!
    pointer_type(?type),
    gep_zero_index_offset(?insn, 0).

  /* Indexing the pointer at an offset for which a subregion of
   the indexed allocation exists.
   E.g.,
     `getelementptr i32, i32* %MyVar, i64 5` points to
     `some_alloc[5]` if `%MyVar` points to `some_alloc` and
     `some_alloc` has a subregion at array index 5.
  */
  gep_points_to(?insn, 0, ?baseAlloc, ?alloc) :-
    gep_indexes_from(?insn, 0, ?baseAlloc, ?baseAlloc, ?type),
    pointer_type(?type),
    basic_allocation(?baseAlloc),
    gep_zero_index_offset(?insn, ?offset),
    alloc_subregion_offset(?baseAlloc, ?alloc, ?offset).

[jdaridis]

Yes, that would be a great idea. I will try to think of a way to implement it in a sensible way

[jdaridis]

I have updated the README file with some of the caveats the server has (eg save to reparse, comment style, etc)

[langston-barrett]

@jdaridis FYI, I have a relatively complete tree-sitter grammar for Souffle available here: https://github.com/langston-barrett/tree-sitter-souffle. One of the nice things about tree-sitter is that it gives you parse trees even in the presence of syntax errors, which is great for editor integrations. Not sure if ANTLR has a similar capability.

Awesome work on the language server!

[jdaridis]

One of the reasons I used ANTLR was the nice integration with Java and the lsp4j library from the Eclipse foundation.

I thought about using tree sitter for a while, but from a little research, I found that it is not really suitable for a language server, because the language server runs in another process and communicates with the editor with JSON RPC and the continuous communication about the parse tree would be too much. Tree sitter is better suited for in-editor work and in this scenario, there is great benefit from the incomplete parse trees.

[mingodad]

Here is @langston-barrett grammar converted (with this script https://github.com/mingodad/plgh/blob/main/json2ebnf.js and manually fixed) to an EBNF understood by https://www.bottlecaps.de/rr/ui .
Copy and paste on https://www.bottlecaps.de/rr/ui on tab Edit Grammar then click on tab View Diagram to see a navigable railroad idagram.

//
// From tree-sitter-souffle/src/grammar.json
//
//
// EBNF to generate railroad diagram at https://www.bottlecaps.de/rr/ui
//
program ::=  ( block_comment |  line_comment |  pragma |  functor_decl |  component_decl |  component_init |  directive |  _rule |  fact |  relation_decl |  type_decl |  legacy_type_decl |  preprocessor ) * 
preprocessor ::=  '#line'  (  [0-9]+ )  (  string ) 
//block_comment ::=  '/*  [^*]*\*+([^/*][^*]*\*+)* /' 
line_comment ::=  '//'  [^#x0A]* '\n' 
pragma ::=  '.pragma'  (  string )  (  string ) ? 
functor_decl ::=  '.functor'  (  ident )  ( '('  ( ( (  _type_name )  |  (  attribute )  ) ?  ( ','  ( (  _type_name )  |  (  attribute )  )  ) *  )  ')'  )  ':'  (  _type_name )  'stateful' ? 
component_decl ::=  '.comp'  (  component_type )  ( ':'  ( (  component_type )  ( ','  (  component_type )  ) *  )  ) ?  '{'  (  ( block_comment |  line_comment |  component_decl |  component_init |  directive |  fact |  relation_decl |  _rule |  type_decl |  preprocessor |  ( '.override'  ident )  ) *  )  '}' 
component_type ::=  (  ident )  ( '<'  ( (  ident )  ( ','  (  ident )  ) *  )  '>'  ) ? 
component_init ::=  '.init'  (  ident )  '='  (  component_type ) 
directive ::=  (  _directive_qualifier )  ( (  qualified_name )  ( ','  (  qualified_name )  ) *  )  ( '('  ( ( (  ident )  '='  (  _directive_value )  ) ?  ( ','  ( (  ident )  '='  (  _directive_value )  )  ) *  )  ')'  ) ? 
_directive_qualifier ::=  '.input'  |  '.limitsize'  |  '.output'  |  '.printsize' 
_directive_value ::=  string |  ident |  number
bool ::=  'true'  |  'false' 
_rule ::=  monotonic_rule |  subsumptive_rule
monotonic_rule ::=  (  ( atom ( ','  atom ) *  )  )  ':-'  (  disjunction )  '.'  (  query_plan?  ) 
subsumptive_rule ::=  (  atom )  '<='  (  atom )  ':-'  (  disjunction )  '.'  (  query_plan?  ) 
query_plan ::=  '.plan'  ( ( (  [0-9]+ )  ':'  ( '('  ( (  [0-9]+ ) ?  ( ','  (  [0-9]+ )  ) *  )  ')'  )  )  ( ','  ( (  [0-9]+ )  ':'  ( '('  ( (  [0-9]+ ) ?  ( ','  (  [0-9]+ )  ) *  )  ')'  )  )  ) *  ) 
disjunction ::=   (  ( conjunction ( ';'  conjunction ) *  )  ) 
negation ::=   (  '!'  ) 
conjunction ::=  ( negation*  ( atom |  _constraint |  ( '('  disjunction ')'  )  )  )  ( ','  ( negation*  ( atom |  _constraint |  ( '('  disjunction ')'  )  )  )  ) * 
_constraint ::=  bool |  comparison |  match |  contains
match ::=  'match'  ( '('  ( (  _argument ) ?  ( ','  (  _argument )  ) *  )  ')'  ) 
contains ::=  'contains'  ( '('  ( (  _argument ) ?  ( ','  (  _argument )  ) *  )  ')'  ) 
comparison ::=  (  _argument )  (  ( '='  |  '!='  |  '<='  |  '>='  |  '<'  |  '>'  )  )  (  _argument ) 
fact ::=  (  atom )  '.' 
atom ::=  (  qualified_name )  ( '('  ( (  _argument ) ?  ( ','  (  _argument )  ) *  )  ')'  ) 
_argument ::=  anonymous |  constant |  variable |  nil |  record_constructor |  adt_constructor |  ( '('  _argument ')'  )  |  as |  functor_call |  aggregator |  unary_op |  binary_op
adt_constructor ::=  '$'  (  qualified_name )  ( '('  ( (  _argument ) ?  ( ','  (  _argument )  ) *  )  ')'  ) ? 
record_constructor ::=  ( '['  ( _argument?  ( ','  _argument ) *  )  ']'  ) 
constant ::=  ipv4 |  number |  string
//ipv4 ::=  "[0-9]{0,3}\.[0-9]{0,3}\.[0-9]{0,3}\.[0-9]"/*{0,3}*/
//string ::=  '([^"]|\\")*'
number ::=  float |  integer |  unsigned
integer ::=  decimal |  hex |  binary
decimal ::=   (  '-'?[0-9]+ ) 
unsigned ::=  [0-9]+u
hex ::=  '0x'([0-9]|[A-F]|[a-f])+
binary ::=  '0b'[0-1]+
float ::=   (  '-'?[0-9]+'.'[0-9]+ ) 
variable ::=  ident
nil ::=  'nil' 
anonymous ::=  '_' 
as ::=  'as'  '('  (  _argument )  ','  (  _type_name )  ')' 
functor_call ::=  (  ( user_defined_functor |  intrinsic_functor )  )  ( '('  ( (  _argument ) ?  ( ','  (  _argument )  ) *  )  ')'  ) 
user_defined_functor ::=  '@'  (  ident ) 
intrinsic_functor ::=   (  ( 'acos'  |  'acosh'  |  'asin'  |  'asinh'  |  'atan'  |  'atanh'  |  'cos'  |  'cosh'  |  'exp'  |  'log'  |  'sin'  |  'sinh'  |  'tan'  |  'tanh'  |  'autoinc'  |  'cat'  |  'max'  |  'min'  |  'ord'  |  'strlen'  |  'substr'  |  'to_float'  |  'to_number'  |  'to_string'  |  'to_unsigned'  )  ) 
aggregator ::=  ( ( ( ( (  ( 'max'  |  'mean'  |  'min'  |  'sum'  )  )  (  _argument )  )  |  'count'  )  ':'  (  ( atom |  ( '{'  disjunction '}'  )  )  )  )  |  range ) 
range ::=  'range'  ( '('  ( (  _argument )  ','  (  _argument )  ( ','  (  _argument )  ) ?  )  ')'  ) 
_unary_operator ::=   (  ( 'bnot'  |  'lnot'  |  '-'  |  '~'  |  '!'  )  ) 
unary_op ::=   (  ( (  _unary_operator )  (  _argument )  )  ) 
binary_op ::=   (  ( (  _argument )  (  '+'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '-'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '*'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '/'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '%'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '^'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  'land'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  'lor'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  'lxor'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  'band'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  'bor'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  'bxor'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  'bshl'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  'bshr'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  'bshru'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '&'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '|'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '&&'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '||'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '**'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '^^'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '<<'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '>>'  )  (  _argument )  )  )  |   (  ( (  _argument )  (  '>>>'  )  (  _argument )  )  ) 
relation_decl ::=  '.decl'  (  ( ident?  ( ','  ident ) *  )  )  ( '('  ( (  attribute ) ?  ( ','  (  attribute )  ) *  )  ')'  )  (  _relation_qualifier*  )  (  choice_domain ) ? 
_relation_qualifier ::=  'brie'  |  'btree'  |  'btree_delete'  |  'eqrel'  |  'inline'  |  'magic'  |  'no_inline'  |  'no_magic'  |  'override'  |  'overridable'  |  'input'  |  'output'  |  'printsize' 
choice_domain ::=  'choice-domain'  ( ( ident |  ( '('  ( ident ( ','  ident ) *  )  ')'  )  )  ( ','  ( ident |  ( '('  ( ident ( ','  ident ) *  )  ')'  )  )  ) *  ) 
legacy_type_decl ::=  (  ( '.number_type'  |  '.symbol_type'  )  )  (  _type_name ) 
type_decl ::=  '.type'  ( ( type_synonym |  subtype |  type_union |  type_record |  adt )  |  legacy_bare_type_decl ) 
legacy_bare_type_decl ::=  (  ident ) 
subtype ::=  (  ident )  '<:'  (  _type_name ) 
type_synonym ::=  (  ident )  '='  (  _type_name ) 
type_union ::=   (  ( (  ident )  '='  (  ( _type_name ( '|'  _type_name ) +  )  )  )  ) 
type_record ::=   (  ( (  ident )  '='  ( '['  ( (  attribute ) ?  ( ','  (  attribute )  ) *  )  ']'  )  )  ) 
adt ::=   (  ( (  ident )  '='  (  ( _adt_branch ( '|'  _adt_branch ) *  )  )  )  ) 
_adt_branch ::=  (  ident )  ( '{'  ( (  attribute ) ?  ( ','  (  attribute )  ) *  )  '}'  ) 
_type_name ::=  primitive_type |  qualified_name
primitive_type ::=  'number'  |  'symbol'  |  'unsigned'  |  'float' 
attribute ::=  (  ident )  ':'  (  _type_name ) 
qualified_name ::=   (  ( ident ( '.'  ident ) *  )  ) 
ident ::=  ('_'|'?'|[A-Z]|[a-z])(([A-Z]|[a-z])|[0-9]|'_'|'?')*

[quentin]

Hi,
Regarding documentation comments I have been exploring a rust-doc like approach where /// and //! stand for outer and inner documentation. I have a souffle-doc tool that generates a static html documentation from a given Souffle program.

I may share this tool if that can be of any inspiration.

[jdaridis]

That's an interesting idea. I will look into it.

For the time being, I added a code action to reformat the documentation comments from // to /* */.

[jdaridis]

Just added integration with souffle-lint.

[b-scholz]

I have created a fork under souffle-lang for visibility.