Skip to content

Add cfg/lookup request to server mode#988

Merged
sim642 merged 7 commits intomasterfrom
server-cfg
Feb 22, 2023
Merged

Add cfg/lookup request to server mode#988
sim642 merged 7 commits intomasterfrom
server-cfg

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Feb 13, 2023 •
edited
Loading

This request allows programmatic traversal of the CFG for abstract debugging (as opposed to dumping a function's CFG in GraphViz format). The method allows two kinds of lookups:

  1. by source code location,
  2. by node ID.

In both cases the method returns:

  1. node ID and location (useful for lookups by location);
  2. next and previous nodes in the CFG.

Example session

$ rlwrap ./goblint --enable server.enabled --enable server.reparse ./tests/regression/04-mutex/01-simple_rc.c

{"jsonrpc":"2.0","id":0,"method":"analyze","params":{}}
{"id":0,"jsonrpc":"2.0","result":{"status":["Success"]}}

{"jsonrpc":"2.0","id":0,"method":"cfg/lookup","params":{"location":{"file":"tests/regression/04-mutex/01-simple_rc.c","line":18,"column":3,"byte":-1}}}
{"id":0,"jsonrpc":"2.0","result":{"node":"84","location":{"file":"tests/regression/04-mutex/01-simple_rc.c","line":18,"column":3,"byte":52985,"endLine":18,"endColumn":30,"endByte":53012},"next":[[[["Proc",null,"pthread_mutex_lock",["& mutex2"]]],"85"]],"prev":[[[["Proc",null,"pthread_create",["(pthread_t * __restrict  )(& id)","(pthread_attr_t const   * __restrict  )((void *)0)","& t_fun","(void * __restrict  )((void *)0)"]]],"83"]]}}

{"jsonrpc":"2.0","id":0,"method":"cfg/lookup","params":{"node":"85"}}
{"id":0,"jsonrpc":"2.0","result":{"node":"85","location":{"file":"tests/regression/04-mutex/01-simple_rc.c","line":19,"column":3,"byte":53016,"endLine":19,"endColumn":22,"endByte":53035},"next":[[[["Assign","myglobal","myglobal + 1"]],"86"]],"prev":[[[["Proc",null,"pthread_mutex_lock",["& mutex2"]]],"84"]]}}

TODO

/cc @FeldrinH

@sim642 sim642 added feature debugging Abstract debugging labels Feb 13, 2023
karoliineh
karoliineh approved these changes Feb 21, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@karoliineh karoliineh left a comment

Choose a reason for hiding this comment

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

Seems good to me. I think we will need approval from @FeldrinH before merging this, though.

@FeldrinH
Copy link
Copy Markdown
Collaborator

FeldrinH commented Feb 21, 2023

Looks good to me.

@sim642 sim642 mentioned this pull request Feb 22, 2023
Closed
2 tasks
@sim642 sim642 merged commit d1a17b4 into master Feb 22, 2023
@sim642 sim642 deleted the server-cfg branch February 22, 2023 08:36
sim642 added a commit that referenced this pull request Feb 22, 2023
@sim642
Fix Cilfacade indentation (PR #988)
7fd4c2a
@sim642 sim642 mentioned this pull request Feb 23, 2023
Merged
@sim642 sim642 added this to the v2.2.0 milestone Apr 5, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@karoliineh karoliineh karoliineh approved these changes

@stilscher stilscher Awaiting requested review from stilscher

+1 more reviewer

@FeldrinH FeldrinH FeldrinH approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

debugging Abstract debugging feature

Projects

None yet

Milestone

v2.2.0

Development

Successfully merging this pull request may close these issues.

3 participants

@sim642 @FeldrinH @karoliineh