Check if two "simple" 'if statements' in C are equivalent

Question

I have 'if statements' from two different sources, which try to implement the same condition possibly in a different way. The 'if statements' are C. If at all possible I need a python script that can decide whether pairs of conditions are equivalent or not. A basic example:

source1: ((op1 != v1) || ((op2 != v2) || (op3 != v3)))

source2: ((op2 != v2) || (op1 != v1) || (op3 != v3))

Of course any operator is allowed, function calls and of course parentheses.

Any ideas are welcome.

Edit 1: The function calls have no side effects.

Answer 1

Here's the thing, the problem may (or may not) be NP-complete but unless this is within the inner-loop of something important (and the number of variable are small), build the entire truth table! It's extremely easy to do. It obviously grows as 2^n, but for small n this is completely feasible. Like the comments suggest, I'm assuming that the function calls have no side effects and simply output True or False.

I've posted a mockup example that solves your stated problem, adapt as needed. I rely on pythons parser to handle the evaluation of the expression.

import pyparsing as pypar
import itertools

def python_equiv(s):
    return s.replace('||',' or ').replace('&&',' and ')

def substitute(s,truth_table, VARS):
    for v,t in zip(VARS,truth_table):
        s = s.replace(v,t)
    return s

def check_statements(A1,A2):  
    VARS = set()
    maths    = pypar.oneOf("( ! = | & )")
    keywords = pypar.oneOf("and or")
    variable = pypar.Word(pypar.alphanums)
    variable.setParseAction(lambda x: VARS.add(x[0]))
    grammar  = pypar.OneOrMore(maths | keywords | variable)

    # Determine the variable names
    grammar.parseString(A1)
    grammar.parseString(A2)

    A1 = python_equiv(A1)
    A2 = python_equiv(A2)

    bool_vals = map(str, [False,True])

    for table in itertools.product(bool_vals,repeat=len(VARS)):
        T1 = substitute(A1,table,VARS)
        T2 = substitute(A2,table,VARS)
        if eval(T1) != eval(T2):
            print "FAIL AT ", table,
            return False

    print "Statements equiv:",

    return True


# Original example
A1 = '''((op1 != v1) || ((op2 != v2) || (op3 != v3)))'''
A2 = '''((op2 != v2) ||  (op1 != v1) || (op3 != v3))'''
print check_statements(A1,A2)

# Example with a failure
A1 = '''((op1 != v1) || ((op2 != v2) || (op3 != v3)))'''
A2 = '''((op2 != v2) ||  (op1 != v1) && (op3 != v3))'''
print check_statements(A1,A2)

Gives as output:

Statements equiv: True
FAIL AT  ('False', 'False', 'False', 'False', 'False', 'True') False

Answer 2

To do this, you need control flow anlaysis to determine if the two conditions have the same control dependence (otherwise they don't execute in the same data context), full data flow analysis including points-to analysis of the C code, a side-effect analysis of functions, the ability to backslice from the root of the condition to the leaves of the expression across function calls, and then a boolean equivalence matcher that accounts for C semantics (e.g. short-circuiting, overflows, ...)

This is far beyond what you get from a C parser.