verifying the condition of if statement

[Mohxen]

Hello all,

Please let me know if there is any pass to verify the condition of an if statement. For example, can it consider a.isValid() && !b.isValid() and !(!a.isValid() || b.isValid()) as the same condition?

Thank you in advance :)

[fruffy]

What do you mean with verify? Transform boolean expressions using Demorgan Rules? Not sure if there is a pass, StrengthReduction might do some similar transformations.

[Mohxen]

Thank you, Fabian. About 'verify expression', I mean, the compiler can understand the equality of expressions and redundant expressions can point to the same node. I checked the StrengthReduction pass; It covers logic Not but does not support DeMorgan laws. I think it covers some situations, but it cannot verify expressions generally.

[jafingerhut]

I would repeat Fabian's first question: What do you mean by "verify"?

For example, suppose the P4 source code has an if condition (hdr.ipv4.proto == 6). What are you thinking the compiler would do to "verify" that expression?

The compiler parses it to ensure it has valid syntax.

The compiler checks that hdr.ipv4.proto is a valid expression, e.g. hdr is a variable, of which ipv4 is a member, of which proto is in turn a member of hdr.ipv4.

The compiler checks that the type of hdr.ipv4.proto is one that can be compared via == to the expression 6.

Is there something else you mean by "verify" besides those things?

[Mohxen]

Thank you @jafingerhut and @fruffy. Perhaps 'verify' was not the correct term to use, but my main point is that simplifying pass (strengthReduction) in P4C is incomplete. For example, P4C cannot optimize the following code into the code provided below. I believe we need Boolean Optimization and Algebraic Simplification passes.

apply{
    if(!(!a.isvalid() || b.isvalid())){
        X
    }
    if(a.isvalid() && !b.isvalid()){
        Y
    }
}

Into:

apply{
  if(a.isvalid() && !b.isvalid()){
    X
    Y
  }
}

[vlstill]

[...] my main point is that simplifying pass (strengthReduction) in P4C is incomplete.

It pretty much has to be incomplete. Checking that two conditions are equivalent (i.e. one is satisfied if and only if the other is satisfied) is a hard problem. To solve it somewhat generally, the compiler would need to employ SAT/SMT solver. I don't think this is done very often in compilers since most of the time the compilation speed is quite important too. In theory it could be useful for targets that are very resource constrained, but in many practical P4 targets I guess it will not matter too much.

Also note that matters get even worse when the variables in the conditions can change between the conditions.

You might be able to heuristically merge some simple cases (e.g. pushing negations inward and disregarding order for commutative operations on values without side effects) but I doubt that will do a lot improvement.

Overall, I think the effort would be quite big for something that is a rather pathological occurrence / code smell in most cases.

[fruffy]

I think it is a good idea to add more passes that transform code. After all, the compiler is meant to have a library of passes you can pick and choose from. We also have easy access to Z3 now and can convert IR expressions into Z3 expressions. We could even do things like Karnaugh-Map transformations.

That being said, this problem is not as easy as it seems, primarily because of side effects. For example, in

apply{
    if(!(!a.isvalid() || b.isvalid())){
        X
    }
    if(a.isvalid() && !b.isvalid()){
        Y
    }
}

X could change the value of a or b. Your transformation needs to be semantics-preserving and check for that. This can quickly get expensive.