Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Semantic unrolling and trace partitioning

  • Subject: [Frama-c-discuss] Semantic unrolling and trace partitioning
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Thu, 4 Jul 2013 22:48:55 +0200
  • In-reply-to: <CAOT7Vm2yKZemjdecL06fxb7ixtfRszmz+GSK0+kQpVNbi1x=Bg@mail.gmail.com>
  • References: <CAOT7Vm2yKZemjdecL06fxb7ixtfRszmz+GSK0+kQpVNbi1x=Bg@mail.gmail.com>
Hello,

On Thu, Jul 4, 2013 at 9:55 AM, Daniel Garcia <dhekir at gmail.com> wrote:

> I'd like to know if Frama-C's semantic unrolling (-slevel) is equivalent
> to trace partitioning. It seems somewhat similar to me, but I didn't see it
> mentioned anywhere, so maybe there are important differences between them?
>

Frama-C's semantic unrolling and trace partitioning are two techniques to
improve precision of an abstract interpreter at the cost, often but not
always, of using more resources. They have similarities but are different.

At this point I should stress that I do not read articles and that the half
of the following discussion that isn't about the implementation I
contributed to may be way off. This said, here is what I think the
difference between semantic unrolling and trace partitioning is. Consider
the example below:

int id(int a)
{
  return a;
}

y = 3;
if (c)
  x = -1;
else
  x = 2;
z = x * id(x);

Both Frama-C's value analysis (with ?semantic unrolling?) and a
hypothetical abstract interpreter with trace partitioning (let us call it
?Astr?e? for short) will avoid the faux pas of predicting that z can be -2
because both will handle the cases x == -1 and x == 2 separately. So the
effect of both techniques is the same on this example, but they arrive to
the same conclusion for different reasons.

In trace partitioning, the states with x == -1 and x == 2 are kept separate
at the assignment ?z = ?? because they have different associated traces.

In semantic unrolling, the states with x == -1 and x == 2 are kept separate
at the assignment ?z = ?? because they differ in x. The analyzer has to
check whether the second of the two state to appear at the assignment is
included in the first state. If implemented naively, when there are N
states, this check could incur O(N^2) individual inclusion tests.

Now consider another example, below.

int id(int a)
{
  return a;
}

y = 3;
if (c)
  x = 2;
else
  x = 2;
z = x * id(x);

Now, I think that trace partitioning would propagate two states over the
assignment to z, again because these states correspond to different traces.
Semantic unrolling, which does not consider traces at all, would recognize
that the second state is the same as the first one, and only propagate the
first one over the assignment to z.

Pushing the reasoning to its logical conclusion, you could use semantic
unrolling to do finite, explicit-state model-checking on C programs. This
is what we did when we participated in the RERS 2012 challenge:
http://blog.frama-c.com/index.php?tag/rers2012 . The articles are presented
in reverse order and should be read from bottom to top. The first one is
http://blog.frama-c.com/index.php?post/2012/08/06/Understand-LTL-Join-us%21.
S?bastien Bardin answered the call in that post. He also pointed out
that
semantic unrolling was most similar to ?Configurable Program Analysis? [1],
an article that I have not read (and that semantic unrolling in Frama-C's
value analysis was developed independently of).

By contrast, I do not think that you could answer the RERS 2012 challenge
with trace partitioning. The programs there have finitely many states but
infinitely many traces.

Pascal


[1] Beyer, D., Henzinger, T. A., Th ?eoduloz, G.: Configurable Software
Verification: Concretizing the Convergence of Model Checking and Program
Analysis. In:CAV 2007.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130704/9f7b1090/attachment.html>