[depends: #708] Write Stack for storing pointer values #1120
Conversation
…be picked independently.
The option string --show --intervals is more flexible, --show-intervals is now an alias.
This includes skeleton code written by @martin-cs. Added hook for running the variable sensitivity Involved removing messaget inheritance since we require a zero parameter constructor for ai_baset Terminate correctly Made the domain correclty find the fixed point. The merge operation returns whether the merge actually changed any values by implementing a operator== for each of the abstract objects. Further, when merging a map, if a key is absent from one map then we remove it from the other unless the map is bottom. Adding handlers for the special types They are just stubs at the moment, returning top as we need the abstract objects that represent them. Updated interface for ai_domain_baset
Adding ==operator to the constant abstract value
These clasess will represent the basis for complex types with helper methods to read and write to/from them. They however will still be just a 2 element abstraction (top or bottom)
Made so the read returns a bottom element if it is bottom. Made the write return itself if true to faciliate sharing.
In release builds, the top/bottom status of the enviroment was undefined. This ensures the enviroment is set to top (i.e. an entry point).
Previously each abstract object that implemented merge had to correctly redirect merging top with anything or merging with a bottom. This is now handled directly in the root merge by checking the three cases where the base merge must be used. If this is bottom must still be handled by derived classes as we must create an abstract object of the same type.
At some point this commit needs backdating as the ai_domain interface has changed under our feet.
Previously the order of the libraries in LIB would effect whether the unit tests compiled. Use OBJ rather than LIBS to ensure the --start-group/--end-group flags are used in linking. Previously, if a file in CProver changed, though the libraries would be rebuilt, the unit tests wouldn't be relinked against the new library, meaning you would get out of date binaries. This change ensures that the link process is rerun if any of the libraries are rebuilt.
In turns the error return state into a CATCH exception so the test will fail without cluttering tests with checks on the flag when it is just setup code for the actual test.
The auxilary function had the same flags requried for the test, so added a utility constructor that allows specifying of name and type.
…feature/write-stack
…tion Deals with storing a stack to write to things like: &a[1] &s.comp &a[x] + 1 By building a stack as parsing the expression tree. It does not support pointer arithmetic outside the scope of an array (e.g. within a struct) This will be used to store pointer values.
Pointers into arrays was creating a top stack even though the result was valid. Corrected so didn't throw them away (need to look at the base of the stack, not the top). Also made the tests verify that they don't create a top stack when they shouldn't. Also made it impossible to get the expression of a top stack.
|
Is there published work that describes this approach? What I am wondering about is how branching (any non-linear control-flow) interacts with those stacks? |
| REQUIRE(out_expr.id()==ID_address_of); | ||
| const member_exprt &member_exrp= | ||
| require_exprt::require_member(out_expr.op0(), "comp"); | ||
| // TODO: verify member expr |
| REQUIRE(out_expr.id()==ID_address_of); | ||
| const member_exprt &member_exrp= | ||
| require_exprt::require_member(out_expr.op0(), "comp2"); | ||
| // TODO: verify member expr |
|
@tautschnig Sorry- I'm not sure I understand your concern. This part of work is essentially a way of taking an AST representing a pointers value and partially evaluating it in the environment so we can represent a pointers value in a symbolic way. This seems to be me an orthogonal problem to branching/non-linear control flow? If for example you mean how does it handle: int a;
int b;
int * c;
if(NONDET())
{
c = &a;
}
else
{
c = &b;
}Then this is handled by the |
Yes, I'm starting to understand - sorry, I just didn't quite understand what this PR was touching upon. "A more sophisticated mechanism for storing pointers." was a bit too brief for me to be able to grasp. It's still not clear to me why turning a particular branch of a tree (an |
This works correctly so we don't need to cautiously throw away stacks of pointers to structs. The original concern was pointers to structs being used as pointers to the first component, but the goto program introduces a cast which means we don't create the pointer. Added a unit test to document this behavior.
We have to turn on pointer sensitivity or otherwise when evaluating these expressions we won't get the correct write stack.
thk123
force-pushed
the
feature/write-stack
branch
from
0fcf280 to
6120ca2
Compare
tautschnig
changed the title
|
I am going to close this PR as it appears that work on it has been inactive for an extended period of time. This is not any judgement on how worthwhile this work is. This is part of an effort to reduce the number of open PRs which are not being actively worked on. Getting this PR merged would require someone to be willing to put the work into rebasing and addressing any remaining CI failures, assuming that this work has not been merged as part of another PR. If it is worthwhile to get this merged and someone is willing to put in the work, then the branch should be re-based on the latest version of develop and the PR re-opened. |
A more sophisticated mechanism for storing pointers. It supports pointers to things like:
It does this by taking an expression and converting it into a stack that can then be converted back to an expression.
This is dependent on the variable sensitivity domain #708
It also uses the improvements to the unit test framework #1111 ✅
Real diff: https://github.com/diffblue/cbmc/pull/1120/files/964b8c841bebe266643159eb377eadef89df4336..0fcf28001b576ff4ed9aebf06dc678ce3c1a61e8