Add arg/dot, arg/state, arg/eval and arg/eval-int requests to server mode

[sim642]

Changes

1. Add function fields to cfg/lookup and arg/lookup responses.
2. Add arg/dot request, which returns the Graphviz string representation of the ARG.
3. Add arg/state request, which returns the JSON representation of an ARG node local state.
4. Add arg/eval request, which returns the JSON representation of a C expression evaluated at an ARG node.

The latter two are achieved by introducing a PathQuery query. The PathQuery generalizes the ability of Invariant query to only query a single path from the witness lifter. The DYojson query just returns D.to_yojson but via the query system. It is slightly hacky but allows accessing the local state representation of a particular path without bigger changes to all the Spec lifters.

TODO

• Rename arg/eval → arg/eval-int.

[FeldrinH]

aaa9cad did not resolve the issue with evaluating global variables after reanalysis. Now all global variables evaluate to top after reanalysis.

[sim642]

aaa9cad did not resolve the issue with evaluating global variables after reanalysis. Now all global variables evaluate to top after reanalysis.

Do you have a specific test case where that happens?

[FeldrinH]

// repro.c
int global = 32;

int main() {
    int local = 3;
}

// goblint.json
{
  "files": ["repro.c"]
}

After reanalysis arg/eval-int will return top for the expression global.

Note: running analysis with reset=false you need to analyze, comment out global, reanalyze, comment in global and reanalyze again to get the issue to happen. Running analysis with reset=true you just need to analyze twice.