Add assert to local_bitvector_analysis.cpp #838
Conversation
|
Happy to debug this - what command line should I be using with CBMC on that program? |
|
No arguments whatsoever - just |
|
The change is a good one, but the bug appears to lie in the input program. It has a |
|
It was generated by a fuzzer. Even ill-formed inputs should not cause the program to attempt to read invalid memory. |
|
Yes, I do agree with that, but really we should have #751 addressed. Ideally we would precisely document which parts of the code base assume consistent goto programs. |
|
A good way to do that is to use the type system. Have a type which represents/holds a goto-program in an inconsistent state, and some other classes which represent goto-programs for which specific invariants hold. The constructors for these classes can take the 'inconsistent state' program, and throw an exception if the program cannot be made consistent. This way, modules which use goto programs can specify the invariants that should hold simply by using one of the specialised goto program types in their interfaces. This is safer, more self-documenting, and simpler than having a single goto-program type which has to maintain several different sets of invariants. Of course, this only works if we also make the goto-program data private, and restrict the goto-program interface such that any modifications maintain the current set of invariants. |
|
Yes, types are a possible solution. But I'd argue that rewriting pretty much the entire code base to work with this different approach of encoding is not the most customer-focused way of spending time. There are many areas which would provide a lot better value. Hence I'd argue for doing a rather simple hack of adding invariant checks with |
|
On Tue, 2017-04-18 at 12:16 -0700, Reuben Thomas wrote:
It was generated by a fuzzer. Even ill-formed inputs should not cause the program to attempt to read invalid memory.
goto-programs aren't really an external interface; they are a convenient
dump of a data-structure. They are only intended to be produced /
consumed by the tools (and the same version of them!). This is why the
format is not documented or really constructable via anything other than
the CPROVER code. There are *many* bad things you can do with malformed
goto-programs. Until we have made an attempt at documenting what we
believe to be correct programs ( see #751 ) ... you are welcome to fuzz
but ... helping document the informal invariants we have is a much
better use of time.
|
|
On Wed, 2017-04-19 at 01:18 -0700, Reuben Thomas wrote:
A good way to do that is to use the type system. Have a type which represents/holds a goto-program in an inconsistent state, and some other classes which represent goto-programs for which specific invariants hold.
There is a potential combinatorial problem here. The C++ type system
isn't powerful enough to really handle combinations of predicates (yes,
you could with trait based design but this starts to get very ugly
compared to languages that have full dependent types). For example, you
might want to know if the program has had function pointers, returns,
vectors and exceptions removed. These won't always be removed in the
same order, or at all, so you could wind up needing 2^4 = 16 classes.
As we improve in the invariants, the number will continue to rise.
The constructors for these classes can take the 'inconsistent state' program, and throw an exception if the program cannot be made consistent.
This is not a problem we have that much; it is more about documenting
what state things are in.
This way, modules which use goto programs can specify the invariants that should hold simply by using one of the specialised goto program types in their interfaces. This is safer, more self-documenting, and simpler than having a single goto-program type which has to maintain several different sets of invariants.
Maybe but types are in many ways less flexible than explicitly located
invariants as you can't have places where they don't hold without
changing type. This can be a major headache / cost and is something
that most of the approaches to annotation for object orientated language
have run into at some point. Type / class invariants and some of Rustan
Leino's pre-Daphne works is a place to look.
Of course, this only works if we also make the goto-program data private, and restrict the goto-program interface such that any modifications maintain the current set of invariants.
works != has to be enforced by the language under all circumstances.
This is why #751 is phrased as it is. The goal is to first document (in
code) what we believe, then check it. Once we have this done, working
and it proves to be useful we could look at attempting to enforce it.
|
When running the linked program
(thanks @mgudemann for the test case) with cbmc under address-sanitizer, we get the following error:
After applying this patch, we instead trigger the new assertion:
Though I think it's probably a good idea to add this assert to avoid memory corrpution, there may be a better fix that avoids triggering this assertion altogether. Could @tautschnig or @kroening advise?