I find this query quite confusing. I see the only use for this right now is to allow vareq to ask base about its WeakUpdates set.

The issue of a single varinfo representing multiple concrete variables is highly specific to base (and I guess vareq) because they pass reachable variables into called functions, allowing for this situation to arise. However, this isn't fully generic in the sense that every analysis should be considering MayBeMultiple because naively one might also expect octApron to consider this information to make weak updates. But it doesn't have to (AFAIK) because it never passes local state into called functions in the same way as base does, so the confusion doesn't arise. Also, it somehow assumes that vareq passes reachable locals into called functions in exactly the same way as base, but is that really the case? So it seems to me like this notion is specific to each analysis wrt how much it passes down.

Moreover, if it were fully generic, I'd expect it to be possible to fix #316 using the same query by having mallocWrapper claim all of the varinfos that it has returned to represent multiple concrete values (until we implement more precise uniqueness for mallocs). But again, this query wouldn't really work for that: mallocWrapper may answer the query for a malloced varinfo with true, but that wouldn't be in base's WeakUpdates set, so base answers with false and the meet of MayBool yields false. So for that kind of general use, it should be MustBool instead for a negated query like MustBeUnique, so if it's either in base's WeakUpdates or created by mallocWrapper, it wouldn't be unique any more.

But that doesn't really solve the first problem, that what is considered to be non-unique by one analysis isn't necessary non-unique for another.

is highly specific to base (and I guess vareq) because they pass reachable variables into called functions, allowing for this situation to arise

I don't really think it is. As soon as the base analysis treats something as Multiple all other analyses must also do so or not answer EvalInt queries. This is because the points-to information that is used from base does not distinguish between inner and outer instances

because naively one might also expect octApron to consider this information to make weak updates

EDIT: In principle it would have to, but it does not track variables that have their address taken, escaping this conundrum.

If it ever were enhanced to also track such variables:

// PARAM: --sets ana.activated[+] "var_eq" --sets ana.activated[+] "octApron"
int rec(int i,int* ptr) {
    int top;
    int x = 17;

    if(i == 0) {
        rec(5,&x);
        // Recursive call may have modified x
        assert(x == 17); //UNKNOWN!
    } else {
        x = 31;

        // ptr points to the outer x, it is unaffected by this assignment
        // and should be 17
        assert(*ptr == 31); //UNKNOWN!
    }
    return 0;
}

int main() {
    int t;
    rec(0,&t);

    return 0;
}

The question is just whether to fix all analyzes in this PR or make separate ones. The issue is that the octApron has x = 31 after the assignment, the address domain in base has ptr -> {&x} and asks for the value of x via the query system, to which octApron answers [31,31].

Actually, after recompiling 🙃, it does seem to work with octApron, as it does not have x as a tracked local variable, because it does not track variables who have their address taken.
So the reason one does not need to take it into account in OctApron is precisely that.

Something else must be wrong with octApron in this case because x has its address taken in rec(5,&x), so octApron shouldn't be tracking x at all.

I think your comment overlapped with mine, I have since edited it. It works precisely because it does not track variables that have their address taken.

There should probably be a comment in octApron then, explaining that due to vaddrof it doesn't need to consider it at function calls etc.

I'll add a comment

Still, I think it would make sense to flip the query to make it possible for mallocWrapper to also indicate the alloc variables as multiple/non-unique.

Sure, I'll flip it!

Actually, would it even be possible to pull this WeakUpdates stuff into a separate analysis instead of baking it into base, if other analyses should be considering it regardless of what base is doing? It

That is very complicated, it requires the reachable may-point-to sets (from the params) at function call. And if we query the base analysis for that, it is not too different from just embedding it.

I was thinking about this query again and how it would behave if mallocWrapper also answered it such that any varinfo that it created is not unique, but somehow it still doesn't make sense the way I thought it would.

MayBeMultiple (before)

MustBeUnique (now)

MustBeMultiple (should be?)

It seems to me now like the query should be MustBeMultiple because otherwise one of the varinfo multiplicity/uniqueness analyses needs to somehow subsume the other: base's WeakUpdates should also automagically contain all malloced variables?

Interesting!

MustBeMultiple is also somehow not the right thing though. If something is in this WeakUpdates set, this just means that an outer copy may be reachable not that it must be.
So the name MustBeMultiple would be very confusing, since we need to weakly update all things that may be multiple, not just those that must be.

Regardless of this, I agree that MustBool is the correct lattice. I'll see how to make this change while not making it confusing. (Maybe some comment?)

Maybe calling it IsMultiple is the right thing to do? It doesn't demand anything about must-multiplicity, but rather just asks each analysis whether it has made the varinfo multiple. And then MustBool is just the right lattice to correctly combine the answers of different analyses.

It muddies the water though because at some point we wanted all the queries to clearly be one or the other by name.

I went with the solution from the last comment now!