tests/1-branches/tests/0301-conditional-allocation-two.x should fail

[jorendorff]

The test is shown below. The actual code does not implement the abstract in the case that x and y are both nonzero. The abstract says it should return a new allocation in that case, but the code returns NULL.

I didn't fully debug this. For some reason, after splitting on x in the abstract, in the branch where x is true, Xr0 doesn't then split on !y.

#include <stdlib.h>

void *
test(int x, int y) ~ [
    if (x) {
        return .malloc(1);
    } else if (y) {
        return NULL;
    } else {
        return .malloc(1);
    }
]{
    if (!y) {
        return malloc(1);
    }
    return NULL;
}

[jorendorff]

OK, this is because props_get can only return true or false; it can't return an "undecideable condition" error (which would trigger splitting).

[akiarie]

This is another really good spot.

The shallow cause is a hack we added to get a certain kind of branching case working, that we let creep into master.

I've taken out the hack for now, and this test fails, as it should. (Accordingly, I've added a failure and success case based on it.)

The deep cause is the entire props library is a placeholder for some sounder logical analysis that we want to introduce. In particular, right now we model propositions as ast_exprs, whereas this will only done for irreducible propositions (such as the value of a function that has no abstract). For splitting on the values of parameters like x and y, what should happen is the range of possible values, modelled in the state as $0 and $1, should change according to the assumption. So when assuming that x is true, we should have $0 change from int:{MIN:MAX} to int:{MIN:0, 1:MAX}, and when assuming !x, we should have $0 become int:{0}, and so forth. We'll be introducing this logical analysis in the coming weeks and tracking it under #49.