Add arg/lookup request to server mode

[sim642]

This is analogous to #988, but for traversing the ARG (abstract reachability graph) instead of the CFG. The option exp.arg is added to enable ARG construction outside of SV-COMP witness mode.

As opposed to cfg/lookup, this request has two extensions:

1. If neither node nor location are given, the entry node of the ARG is returned.
2. Returns a JSON array instead of a single result. This is necessary when looking up by location to return ARG nodes for all contexts and paths at the same node. In other cases a singleton array is returned.

[FeldrinH]

Would it be possible to add some kind of context identifier to the returned ARG node data? It would be useful for finding nodes with the same context when jumping from an existing set of nodes to a target location in the ARG. It could also be useful later for querying data about the context of a specific node.

[sim642]

Would it be possible to add some kind of context identifier to the returned ARG node data? It would be useful for finding nodes with the same context when jumping from an existing set of nodes to a target location in the ARG. It could also be useful later for querying data about the context of a specific node.

I added the fields context and path to expose this information. context is the one you wanted for contexts, but ARG nodes also identify a particular path within a path-sensitive analysis, hence the path field. Although the latter might not be relevant to you since ARG traversal follows paths itself anyway.
Both are exposed as JSON strings because they should be treated as opaque identifiers.

[sim642]

The discussed TODOs should now be implemented. Also there's an option exp.argdot which dumps the ARG for Graphviz, which is easier to use than all the SV-COMP stuff. It also includes the "step over function call" edges, which aren't present in witnesses.

[FeldrinH]

It would be convenient if the edge info also contained the CFG node id in addition to the ARG node id.
Besides that, the current API works well for my needs.

[FeldrinH]

I have discovered what seems to be a bug:
If you analyze a file, then edit it and then reanalyze it then afterwards arg/lookup returns incorrect source code locations.
Repro:

// test.c:
int main() {
    return 0;
}

$ goblint --enable exp.arg --enable server.enabled --enable server.reparse test.c
{"jsonrpc":"2.0","id":"1","method":"analyze","params":{}}
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 2
  dead: 0
  total lines: 2
{"id":"1","jsonrpc":"2.0","result":{"status":["Success"]}}
{"jsonrpc":"2.0","id":"2","method":"arg/lookup","params":{}}
{"id":"2","jsonrpc":"2.0","result":[{"node":"fun1620main(9)[7]","cfg_node":"fun1620","context":"9","path":"7","location":{"file":"test.c","line":1,"column":1,"byte":126,"endLine":3,"endColumn":1,"endByte":150},"next":[{"edge":{"cfg":{"string":"(body)","type":"entry","function":"main"}},"node":"s77(9)[7]"}],"prev":[]}]}
// Some blank lines are added to the start of test.c here
{"jsonrpc":"2.0","id":"3","method":"analyze","params":{}}
change_info = { unchanged = 437; changed = 0; added = 0; removed = 0 }
Removing data for changed and removed functions...
Restarting write-only to bot main
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 2
  dead: 0
  total lines: 2
{"id":"3","jsonrpc":"2.0","result":{"status":["Success"]}}
{"jsonrpc":"2.0","id":"4","method":"arg/lookup","params":{}}
{"id":"4","jsonrpc":"2.0","result":[{"node":"fun1620main(9)[7]","cfg_node":"fun1620","context":"9","path":"7","location":{"file":"test.c","line":1,"column":1,"byte":126,"endLine":3,"endColumn":1,"endByte":150},"next":[{"edge":{"cfg":{"string":"(body)","type":"entry","function":"main"}},"node":"s77(9)[7]"}],"prev":[]}]}
^CAnalysis was aborted by SIGINT (Ctrl-C)!
$ goblint --enable exp.arg --enable server.enabled --enable server.reparse test.c
{"jsonrpc":"2.0","id":"1","method":"analyze","params":{}}
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 2
  dead: 0
  total lines: 2
{"id":"1","jsonrpc":"2.0","result":{"status":["Success"]}}
{"jsonrpc":"2.0","id":"2","method":"arg/lookup","params":{}}
{"id":"2","jsonrpc":"2.0","result":[{"node":"fun1620main(9)[7]","cfg_node":"fun1620","context":"9","path":"7","location":{"file":"test.c","line":7,"column":1,"byte":132,"endLine":9,"endColumn":1,"endByte":156},"next":[{"edge":{"cfg":{"string":"(body)","type":"entry","function":"main"}},"node":"s77(9)[7]"}],"prev":[]}]}

Note that the line numbers are incorrect after test.c was changed but become correct after a restart.
Tested with Goblint version heads/arg-lookup-0-gcafbcc063.

[sim642]

Both improvements should now be made.

[FeldrinH]

Everything seems to be functional and the API works well for my use cases.