Re: Recognize valid paths

> if (x < 1)
> x = 1;
> if (x > 10)
> x = 10;
>
> I was wondering which compiler analyses might recognized such invalid
> combinations of paths. Any ideas?


That is more complicated than you might think. Analyzing anything more
than the most trivial cases will require a sophisticated logic solver
(which can not guarantee an answer in all cases). But here's the gist
of it (I'm assuming a C syntax):


assert( true );
bool firstScope = false;
assert( !firstScope );
if (x < 1) {
        assert( !firstScope && x < 1 );
        firstScope = true;
        assert( firstScope && x < 1 );
        x = 1;
        assert( firstScope && x== 1 );
}
assert( (firstScope && x == 1) || (x >= 1 && !firstScope) );
if (x > 10)
        assert( x > 10 && ((firstScope && x == 1) || (x >= 1 && !
firstScope)) );
        // |
        // V
        assert( x > 10 && !firstScope);
        x = 10;
}


I've changed several things in your example. For convenience, I've
introduced a boolean called firstScope that indicates if you've
visited the (x<1) scope. The goal here is to prove that (!firstScope)
within the (x>10) scope. I've used assert statements to show the proof
outline. Since you haven't given any precondition, we'll start with
the precondition (true) (the weakest possible condition). Then you
work your way down as you calculate the strongest postcondition of
each statement, given its precondition.


Note that calculating the strongest postcondition of a statement
usually requires you to keep track of many temporary logical
variables, but I've left them out for clarity, since we won't need
them in this simple example. I hope the simplified rules for finding
the strongest preconditions are clear from the code. I'm not sure how
I would explain them formally. But if they're unclear, I can try to
give an informal explanation.


As you can see in the proof outline, (!firstScope) is true upon
entering the (x>10) scope.


If there's a simpler way, I don't know it.

Return to the comp.compilers page.
Search the comp.compilers archives again.