Sat, 23 Aug 2008 09:24:16 -0700 (PDT)

Related articles |
---|

Recognize valid paths plfriko@yahoo.de (Tim Frink) (2008-08-20) |

Re: Recognize valid paths m.helvensteijn@gmail.com (2008-08-23) |

Re: Recognize valid paths DrDiettrich1@aol.com (Hans-Peter Diettrich) (2008-08-24) |

Re: Recognize valid paths plfriko@yahoo.de (Tim Frink) (2008-08-26) |

Re: Recognize valid paths plfriko@yahoo.de (Tim Frink) (2008-08-26) |

Re: Recognize valid paths m.helvensteijn@gmail.com (Michiel Helvensteijn) (2008-08-27) |

Re: Recognize valid paths jeffrey.kenton@comcast.net (Jeff Kenton) (2008-09-01) |

From: | m.helvensteijn@gmail.com |

Newsgroups: | comp.compilers |

Date: | Sat, 23 Aug 2008 09:24:16 -0700 (PDT) |

Organization: | Compilers Central |

References: | 08-08-042 |

Keywords: | analysis, optimize |

Posted-Date: | 23 Aug 2008 14:40:44 EDT |

*> 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.

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.