[CIL users] CIL input vs. output

[John R. <re...@cs...>]

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