Re: [CIL users] Switches and loops.

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 454-5900

<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
  <meta content="text/html;charset=ISO-8859-1" http-equiv="Content-Type">
  <title></title>
</head>
<body bgcolor="#ffffff" text="#000000">
Xavier Leroy wrote:
<blockquote cite="mid:478...@in..." type="cite">
  <pre wrap="">Amine Marref wrote:

  </pre>
  <blockquote type="cite">
    <blockquote type="cite">
      <pre wrap="">Does anyone know how to make the switch to if conversion and not touch
loop structure?
      </pre>
    </blockquote>
  </blockquote>
  <pre wrap=""><!---->
Mark Hills replied:
  </pre>
  <blockquote type="cite">
    <pre wrap="">Unfortunately this doesn't appear to be a minor change. The loop
structure is changed in cabs2cil.ml (search for A.WHILE to see where
this starts), so all loops are changed into something like a while(1)
loop right after parsing. CIL then just handles while(1) loops in
everything else it does. Keeping the termination check around would
require modifying code in cabs2cil.ml, cil.ml, and a number of other
files that happen to reference the Loop constructor. It would probably
also hamper simplification later, if you want to use it, since to
simplify the termination check it may have to be moved anyway.
    </pre>
  </blockquote>
  <pre wrap=""><!---->
In the Compcert verified C compiler (which uses CIL as its parser and
simplifier), we encountered the same problem described by Amine.
We were able to patch the CIL source code along the lines outlined by
Mark, but, yes, this required a number of small changes all over
the place.  Additionally, we did not update the additional analyses
and transformations found in the src/ext directory, because we do not
use them, but as a consequence our patches aren't terribly clean.

So, it can be done but doing it right (more cleanly than we did) would
take quite a bit of work.

- Xavier Leroy
  </pre>
</blockquote>
That's a pity, loops with breaks affect reducibility of CFGs which
hinders some types of analysis.<br>
<br>
<pre class="moz-signature" cols="72">-- 
Amine Marref
PhD Research Student
Real-Time Systems Group
Department of Computer Science
The University of York
Heslington
YO10 5DD
York
United Kingdom

+44 1904 432810 
</pre>
</body>
</html>