Skip to content

Add arg/lookup request to server mode#1001

Merged
sim642 merged 25 commits intomasterfrom
arg-lookup
Mar 2, 2023
Merged

Add arg/lookup request to server mode#1001
sim642 merged 25 commits intomasterfrom
arg-lookup

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Feb 23, 2023

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.

@sim642 sim642 added cleanup Refactoring, clean-up feature debugging Abstract debugging labels Feb 23, 2023
@sim642 sim642 requested a review from FeldrinH February 23, 2023 12:44
@FeldrinH
Copy link
Copy Markdown
Collaborator

FeldrinH commented Feb 23, 2023 •
edited
Loading

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 sim642 self-assigned this Feb 23, 2023
@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Feb 27, 2023

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
Copy link
Copy Markdown
Member Author

sim642 commented Feb 28, 2023

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
Copy link
Copy Markdown
Collaborator

FeldrinH commented Feb 28, 2023

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
Copy link
Copy Markdown
Collaborator

FeldrinH commented Feb 28, 2023 •
edited
Loading

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
Copy link
Copy Markdown
Member Author

sim642 commented Mar 1, 2023

Both improvements should now be made.

FeldrinH
FeldrinH approved these changes Mar 1, 2023
View reviewed changes
Copy link
Copy Markdown
Collaborator

@FeldrinH FeldrinH left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@sim642 sim642 merged commit 3ef473c into master Mar 2, 2023
@sim642 sim642 deleted the arg-lookup branch March 2, 2023 08:01
sim642 added a commit that referenced this pull request Mar 2, 2023
@sim642
Fix ArgTools indentation (PR #1001)
f8aaf56
sim642 added a commit that referenced this pull request Mar 3, 2023
@sim642
Fix ViolationZ3 compilation (PR #1001)
2f29b8b
@sim642 sim642 added this to the v2.2.0 milestone Apr 5, 2023
@sim642 sim642 mentioned this pull request Sep 13, 2023
Closed
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 13, 2023
@sim642
[new release] goblint (2.2.0)
eb80bce 
CHANGES:

* Add `setjmp`/`longjmp` analysis (goblint/analyzer#887, goblint/analyzer#970, goblint/analyzer#1015, goblint/analyzer#1019).
* Refactor race analysis to lazy distribution (goblint/analyzer#1084, goblint/analyzer#1089, goblint/analyzer#1136, goblint/analyzer#1016).
* Add thread-unsafe library function call analysis (goblint/analyzer#723, goblint/analyzer#1082).
* Add mutex type analysis and mutex API analysis (goblint/analyzer#800, goblint/analyzer#839, goblint/analyzer#1073).
* Add interval set domain and string literals domain (goblint/analyzer#901, goblint/analyzer#966, goblint/analyzer#994, goblint/analyzer#1048).
* Add affine equalities analysis (goblint/analyzer#592).
* Add use-after-free analysis (goblint/analyzer#1050, goblint/analyzer#1114).
* Add dead code elimination transformation (goblint/analyzer#850, goblint/analyzer#979).
* Add taint analysis for partial contexts (goblint/analyzer#553, goblint/analyzer#952).
* Add YAML witness validation via unassume (goblint/analyzer#796, goblint/analyzer#977, goblint/analyzer#1044, goblint/analyzer#1045, goblint/analyzer#1124).
* Add incremental analysis rename detection (goblint/analyzer#774, goblint/analyzer#777).
* Fix address sets unsoundness (goblint/analyzer#822, goblint/analyzer#967, goblint/analyzer#564, goblint/analyzer#1032, goblint/analyzer#998, goblint/analyzer#1031).
* Fix thread escape analysis unsoundness (goblint/analyzer#939, goblint/analyzer#984, goblint/analyzer#1074, goblint/analyzer#1078).
* Fix many incremental analysis issues (goblint/analyzer#627, goblint/analyzer#836, goblint/analyzer#835, goblint/analyzer#841, goblint/analyzer#932, goblint/analyzer#678, goblint/analyzer#942, goblint/analyzer#949, goblint/analyzer#950, goblint/analyzer#957, goblint/analyzer#955, goblint/analyzer#954, goblint/analyzer#960, goblint/analyzer#959, goblint/analyzer#1004, goblint/analyzer#558, goblint/analyzer#1010, goblint/analyzer#1091).
* Fix server mode for abstract debugging (goblint/analyzer#983, goblint/analyzer#990, goblint/analyzer#997, goblint/analyzer#1000, goblint/analyzer#1001, goblint/analyzer#1013, goblint/analyzer#1018, goblint/analyzer#1017, goblint/analyzer#1026, goblint/analyzer#1027).
* Add documentation for configuration JSON schema and OCaml API (goblint/analyzer#999, goblint/analyzer#1054, goblint/analyzer#1055, goblint/analyzer#1053).
* Add many library function specifications (goblint/analyzer#962, goblint/analyzer#996, goblint/analyzer#1028, goblint/analyzer#1079, goblint/analyzer#1121, goblint/analyzer#1135, goblint/analyzer#1138).
* Add OCaml 5.0 support (goblint/analyzer#1003, goblint/analyzer#945, goblint/analyzer#1162).
@sim642 sim642 mentioned this pull request Nov 6, 2023
Merged
@sim642 sim642 mentioned this pull request Apr 22, 2025
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@FeldrinH FeldrinH FeldrinH approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@sim642 sim642

Labels

cleanup Refactoring, clean-up debugging Abstract debugging feature

Projects

None yet

Milestone

v2.2.0

Development

Successfully merging this pull request may close these issues.

2 participants

@sim642 @FeldrinH