New Feature: pointer theory

[aestriplex]

Dear @NikolajBjorner,

Could it worth the effort if I start to work on some basics of pointer theory? It seems to me that it could be useful for bounded model checking.

[NikolajBjorner]

Let's move this thread to 'discussions' because this could be very long.
@nunoplopes would like some form of pointer theory that is different from the theory of arrays.
I don't know the requirements for such a theory.

Going forward, new features will be added to the SMT core under src/sat/smt.
There are already some plugins for basic theories (EUF, arithmetic, bit-vectors, arrays, quantifiers), but lagging some others (strings/sequences, recursive functions, special relations). The new core is not thoroughly tested, only bit-vectors and EUF have been given some basic regression runs, arithmetic just on samples, but the idea is to ensure the new core is to be solid and maintainable. The following months will be an experience in getting this portion on par and beyond.
The interface contract to theories under sat/smt is given in sat/sat_extension.h and refined in sat/smt/sat_th.h
It is broader than the legacy core, but most methods have default implementations and can therefore be left to default.

A note on disclaimer on external, and for that matter all, contributions: if some time goes by of not addressing bug reports, or the feature is not widely used and it ends up receiving bug reports, I will be retiring these from the master branch.

[nunoplopes]

I agree the SMT world needs a new theory for memory & pointers that supports modern memory models (both hw & sw), but that's in the realm of research right now.
If you have a concrete proposal, I would be trilled to review it. In the meantime, I agree with Nikolaj that we should close this issue, there's nothing concrete to discuss for now.
BTW, the good thing is that user theories are now back, so it should be easier for anyone to prototype an implementation.

[agurfinkel]

Also very interested in this...

[aestriplex]

@nunoplopes I have only some ideas right now. When I'll have something concrete to show you, I'll open a topic under 'discussions'

[addisoncrump]

What existing papers are you looking at in particular? I'd be interested to get some background in this as it is highly applicable to some current work.

[nunoplopes]

I care mostly about LLVM's memory model (https://web.ist.utl.pt/nuno.lopes/pubs/llvmmem-oopsla18.pdf) + various weak hardware memory models.

[addisoncrump]

Okay, I'll give this a read.

[nunoplopes]

Also very interested in this...

Is it now that we are writing a paper together? 😎
More seriously, I'll ping you when I start looking into this. I wanted to prototype a user-theory in Z3. Our memory model is way too complicated to go into arrays efficiently.

[addisoncrump]

As with my other comment, you hit the nail on its head with "our memory model is way too complicated to go into arrays efficiently" 😆 Please loop me in for when you two start brainstorming.

[NikolajBjorner]

By the magic of GitHub, the issue was converted into a discussion.