search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
831 stars 262 forks source link

goto-analyser simplify generates binary that can't be analyzed with goto-instrument #2689

Open polgreen opened 6 years ago

polgreen commented 6 years ago

I am using this Xen binary (which is a goto-cc build of this branch: https://github.com/nmanthey/xen/tree/gotocc): https://drive.google.com/file/d/1Vco57D_iMhQ6N1EXqLTmF1wC9WiSN3mZ/view?usp=sharing To rebuild this binary, use the docker file in this PR: https://github.com/diffblue/cbmc/pull/2504

I am running the following commands:

goto-analyzer --simplify output.binary xen-syms.binary
goto-instrument --call-graph output.binary

The error message is:

goto-instrument: local_bitvector_analysis.cpp:185: local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(const exprt&, local_bitvector_analysist::points_tot&): Assertion `rhs.op0().type().id()==ID_pointer' failed.

I am running on develop + this PR: https://github.com/diffblue/cbmc/pull/2642. I get the same error when I try develop + these patches:https://github.com/tautschnig/cbmc/tree/extend-simplifier.

martin-cs commented 6 years ago

Hmmm... that's not good. It's not entirely unprecedented though.

polgreen commented 6 years ago

I wonder if the root cause is related to either of these issues though, or if CBMC's handling of this style of low-level C code has just generally degraded a bit over the last 6 months? https://github.com/diffblue/cbmc/issues/2653 https://github.com/diffblue/cbmc/issues/2663

martin-cs commented 6 years ago

Simplify can produce code that is outside of the range of things normally produced by the C front-end so it can sometimes turn up bug in other tools based on mistaken assumptions about what can and can't happen ( #751 as ever ).