Skip to content

Complexity graph #7081

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Draft
wants to merge 36 commits into
base: develop
Choose a base branch
from
Draft

Complexity graph #7081

wants to merge 36 commits into from

Conversation

bquiring
Copy link

@bquiring bquiring commented Aug 22, 2022 •
edited
Loading

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

bquiring added 28 commits August 22, 2022 16:16
@bquiring
initial cfg dot program
aef4738
@bquiring
disable default
831ccf5
@bquiring
exclude unreachable functions from the control flow graph
6070b36
@bquiring
revise graph styling, add new metrics
6f7aea6
@bquiring
add metrics, use forall loops
78ee6fc
@bquiring
refactor, add symex instrumentation and add this to default cbmc call…
a220835 
…. started on sat instrumentation.
@bquiring
add solver instrumentation
e028920
@bquiring
instrument solver to fail, and constant propagator to be dumber. Disa…
78c66fc 
…bles display of symex and solver information when those haven't been run
@bquiring
add option to track symex coverage without generating a report
e214941
@bquiring
moved around files. updated but broken
dafcdcb
@bquiring
working
2a81ed8
@bquiring
add dumping of function instructions
30a73b2
@bquiring
better displaying of instructions
0b528e5
@bquiring
display instruction-level complexity
c6b8d15
@bquiring
disable conver_assignments debugging
8eaff6a
@bquiring
fix html bug with dollar signs and colons and add instruction dumping…
9cd0f0e 
… to the command line
@bquiring
updates
6b03cbb
@bquiring
rebase
e5f15ee
@bquiring
add short README
3104abf
@bquiring
small change
b92fb2b
@bquiring
fix build break
0cf70f7
@bquiring
rebase
ea706fd
@bquiring
updates to metrics and display
18b269a
@bquiring
update library function list
ab365ff
@bquiring
update library function styling
d9e6f43
@bquiring
add document and refactor
d06a8f5
@bquiring
more refactor and documentation
945486e
@bquiring
revert changes to remove_function_pointers
51933bf
@martin-cs
Copy link
Collaborator

Thanks for your contribution; it looks very exciting. We might need to do a little bit of work to make it ready for review. Please could you:

  • Write a short description of what this is supposed to do. I saw the addition to the documentation, that is great but it's also good to have some info in the PR about what your goal is, what the architecture is, why you have done things the way you have.
  • Please can you squash together commits that change the same thing. I realise it is hard when working on a new feature but if you can sort the changes into commits which each do one logical thing, it makes it much easier to review.
  • We will need some test case before this can be merged. Ideally end-to-end system tests (as in regressions but unit tests are also good if it establishes interfaces that others can use within the code).

@martin-cs
Copy link
Collaborator

Also, if possible, we shouldn't be adding commented out code. I realise it is handy during development and this is a draft PR but eventually it should become configurable or be removed.

@feliperodri feliperodri added new feature aws Bugs or features of importance to AWS CBMC users labels Aug 23, 2022
jimgrundy
jimgrundy reviewed Aug 25, 2022
View reviewed changes
src/cbmc/cbmc_parse_options.cpp
@@ -635,13 +637,53 @@ int cbmc_parse_optionst::doit()
verifier = util_make_unique<
all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>>(
options, ui_message_handler, goto_model);
// TODO: this is the branch triggered by default
Copy link
Collaborator

Choose a reason for hiding this comment

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

What needs to be done here? Maybe file an issue on whatever it is instead of leaving this isn the code.

src/goto-symex/solver_hardness.cpp
@@ -383,3 +383,8 @@ std::string solver_hardnesst::expr2string(const exprt expr)
ss << format(expr);
return ss.str();
}

Copy link
Collaborator

Choose a reason for hiding this comment

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

Could perhaps be its own PR.

src/goto-symex/solver_hardness.h
@@ -129,6 +129,9 @@ struct solver_hardnesst : public clause_hardness_collectort
solver_hardnesst &operator=(const solver_hardnesst &) = delete;
solver_hardnesst &operator=(solver_hardnesst &&) = default;

Copy link
Collaborator

Choose a reason for hiding this comment

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

Could be in it's own PR

@nwetzler nwetzler self-requested a review September 26, 2022 23:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jimgrundy jimgrundy jimgrundy left review comments

@nwetzler nwetzler Awaiting requested review from nwetzler

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs will be requested when the pull request is marked ready for review martin-cs is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel will be requested when the pull request is marked ready for review peterschrammel is a code owner

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig will be requested when the pull request is marked ready for review tautschnig is a code owner

@kroening kroening Awaiting requested review from kroening kroening will be requested when the pull request is marked ready for review kroening is a code owner

@TGWDB TGWDB Awaiting requested review from TGWDB TGWDB will be requested when the pull request is marked ready for review TGWDB is a code owner

At least 1 approving review is required to merge this pull request.

Assignees

@bquiring bquiring

Labels
aws Bugs or features of importance to AWS CBMC users new feature
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@bquiring @martin-cs @jimgrundy @feliperodri