From: John R. <re...@cs...> - 2008-02-03 22:11:36
|
On the Deputy list Jeremy said: > CIL's > expressions *are* side-effect free One interesting implication of side-effect free expressions is that the C->CIL conversion is making particular choices that are unspecified by C, meaning that one can reach conclusions about a CIL program that do not hold for the original C. Just as a thought experiment I'm trying to figure out if there's a way to use CIL to reason soundly about the C code that is input to CIL, rather than the C code unparsed from CIL. Perhaps as part of the C->CIL conversion, whenever CIL makes a choice, a verification condition could be emitted that requires all other possible choices to lead to the same computation? For example at present a(b(),c()); becomes t1=c(); t2=b(); a(t2,t1); In the new scheme we'd get an obligation to prove that calling b() before c() could not change the observable behavior of the program. Since obligations of this form can be hard, perhaps it would be better to simply assert that the read set of b() and the write set of c() -- and vice versa -- fail to overlap. A smart pointer analysis could discharge many obligations of that form automatically. Anyway have a sense how hard this is? Is it a week of hacking or is it research? John Regehr |