Search code examples
algorithmcompiler-construction

Make a list of code paths mutually exclusive

This is more a general question, not specific to a language. Basically: how can I convert a list of 1-deep code paths, i.e. a list of if conditions, to a list of mutually exclusive if conditions? I.e. is there a family of algorithms to do that? I have the feeling this is a common problem in compilers.

Let's constrain the problem. We have a very simple language.

  • integer variables
  • an if/else condition with two binary operators == and !=
  • execution happens from top to bottom
  • there are no side effects: below if b = 1 and then b = 2, we can remove the first assignment

Example:

if a == 1 { b = 1 }
if a == 2 { b = 2 }
if a != 3 { b = 2 }
if a == 4 { b = 3 }

would be converted to e.g.:

if a == 4 { b = 3 }
else if a != 3 { b = 2 }

If that is solved, it would get more challenging with supporting <, >, &, |.

Solution

  • I did a bit more research. So there are two steps:

    1. detecting mutual exclusiveness
    2. make two non-mutually exclusive conditions mutually exclusive

    ad 1. Detecting mutual exclusiveness can be done using SAT solvers as sepp2k already said. Not sure how they work internally, but a colleague gave the hint of using the idea of abstraction interpretation with lattices as values.

    ad 2. In a naive approach, for two non-mutually exclusive code paths A and B, we simply replace the two with conditions A & B, A & ~B and ~A & B.