Semantic Search

[prion-cloud]

This feature introduces a search provider for semantic code properties, based on Goblint's analysis results. For this purpose, a new transformation named expeval uses the built-in query system to evaluate specified arithmetic expressions (without actually transforming source code).

My corresponding bachelor thesis: Extending a Syntactic Search in C Source Code with Analysis Results from the Static Analyzer Goblint

[michael-schwarz]

Thanks for the PR!
We'll delay merging this a bit until we have cut a release for the pre-run of SVCOMP 2020.

[michael-schwarz]

Before we can merge this, we need to decide what to do with: https://github.com/faddeenkov/syntactical_analyzer (after some more cleanup of that which I'm currently doing).
This project is the base for this feature, it does the syntactical part of the search.

I see three ways to do this:

• Merge https://github.com/faddeenkov/syntactical_analyzer into our CIL fork, as it is not Goblint specific
• Merge https://github.com/faddeenkov/syntactical_analyzer into Goblint together with this
• Keeping https://github.com/faddeenkov/syntactical_analyzer as a submodule as proposed in this PR

I'd favor either 1 or 2, I think there is no real reason to have this as a submodule going forward.

[vogler]

https://github.com/faddeenkov/syntactical_analyzer does not exist. You mean https://github.com/faddeenkov/cil_fork?
By 2 you mean copy the CIL fork into Goblint? Depends how actively you want to change CIL going forward. What are the disadvantages of keeping them separate? You can have multiple opam packages in one repo, but it will increase build time and might make issues/PRs/search confusing unless you tag everything.
By 3 you also mean to merge it into our CIL fork and just use it as a submodule? Then the only difference between 1 and 3 is that 1 needs git push & opam update (& pin add/install?) to get CIL changes into goblint whereas 3 will just take the files but also slightly increase build times if CIL wasn't touched. However, for case 1 you can also just opam pin the local directory to speed it up a bit.

[sim642]

I'm guessing https://github.com/faddeenkov/syntactical_analyzer is a private repo, which is why it appears to us as non-existent. If that's the case, then it's hard to decide what to do with it without knowing what's there.

[michael-schwarz]

@sim642 is right, it is a private repository. I also can't change the visibility of my fork, so I'll have to ask my student to publish it. I invited both of you to my fork for now.

The question is whether to

• merge the code in that separate repo into CIL
• merge it into Goblint
• make it a submodule of Goblint

I don't think we need to change anything about the way we include CIL.

[michael-schwarz]

https://github.com/faddeenkov/syntactical_analyzer should be public now.

[vogler]

No strong opinion. Doesn't look like it's a lot. Probably depends on whether we want it as a separate binary or if it can be sensibly integrated into the goblint CLI.

[michael-schwarz]

I merged Olga's syntactic search into CIL as a new feature for now: https://github.com/goblint/cil/tree/feature/syntactic_search

@superbr4in can you adapt this PR to pin goblint-cil to that branch and remove the submodule and see if it works and what changes are required?

Once that works, we can merge https://github.com/goblint/cil/tree/feature/syntactic_search into the develop branch of goblint-cil, change the pin back and then merge this.

[prion-cloud]

It looks like the JsonParser module of goblint-cil.syntacticsearch collides with another module of the same name. Example usages can be found in gobConfig.ml and defaults.ml.

How could this be resolved?

[vogler]

Could pull it out into a separate library. But it's maybe better to use yojson which we have as a dependency anyway for ppx_deriving_yojson.

[michael-schwarz]

Alternatively, a solution would be renaming the module in the CIL submodule to something like QueryParser.

JsonParser is a bit generic for what it actually does (define the needed types and call the functions generated by ppx_deriving_yojson) anyway.

https://github.com/goblint/cil/blob/feature/syntactic_search/src/ext/syntaticsearch/jsonParser.ml

[prion-cloud]

Alright, it works now. The pin-depends are back again.

[michael-schwarz]

I think as soon as this is made compatible with OCaml 4.07.1, we're good to merge!
Meanwhile, I merged the syntactic search into CIL and cut a new release (goblint-cil-1.7.8).