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] [Value Analysis] multi state propagation

  • Subject: [Frama-c-discuss] [Value Analysis] multi state propagation
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Wed, 6 Feb 2013 17:16:12 +0100
  • In-reply-to: <51078966.40703@free.fr>
  • References: <51078966.40703@free.fr>
Hi Anne,

On Tue, Jan 29, 2013 at 9:33 AM, Anne Pacalet <anne.pacalet at free.fr> wrote:
> what is exactly what I expected. But unfortunately, it seems that
> the two states are then merged before being propagated to the 'main'
> as shown by the second Frama_C_dump_each (in 'main') :
> [value] DUMPING STATE of file test.c line 19
>         N ? {0; 1}
>         f ? [--..--]
>         =END OF DUMP==
[snip]
> I managed to get the precise result with :
> $ frama-c -val test.c -slevel 100 -val-split-return-function local:0
[snip]
>
> But it doesn't scale when the call stack is deeper.
>
> What would be great is to be able to specify "something" about
> either 'ext'
> (like : ensures f == 0 || f > 0;)
> or in 'local'
> (like: ensures (f == 0 && N == \old(N)) || (f > 0 && N == \old(N)+1);)
> and to tell the analysis that we would like to propagate the two states.

As you have noticed, Value fuses all possible states when it finishes
the analysis of a function. This is a trade-off between (1) precision
(2) avoiding a combinatorial explosion with large amounts of slevel
(3) making the use of slevel a bit predictable. On some function
calls, it may be important precision-wise to separate between
different final states. The option  -val-split-return-function that
you discovered was introduced for this reason. However, it remains
experimental, and in fact should have been marked as such. One of its
limitations is that you need enough slevel in the caller and in the
callee to guarantee that the states you are interested in are
propagated disjointly.

The feature you would like, specifying (typically through ACSL
disjunctions) that some states must remain separate during analysis,
has been under consideration for quite some time now. It is indeed the
next step logical step after -val-split-return-function. However,
implementing such a feature requires invasive changes in the way Value
propagates its state during a function analysis. Also, there are some
subtle practical and semantical issues. To name a few:
- can the annotations used to separate blocks be local to a block?
- how do we specify that we want to keep a loop index always exact ?
(A disjunction makes no sense in this case)
- what happens when the disjunction does not cover all possible states ?
etc.
Unfortunately, we are unlikely to find the time to implement such an
invasive change without a collaborative project. If you believe this
feature would be useful to you, do not hesitate to contact Florent or
support at frama-c.com to discuss such a collaborative effort.

--
Boris


On Tue, Jan 29, 2013 at 9:33 AM, Anne Pacalet <anne.pacalet at free.fr> wrote:
> Hello List,
>
> I am trying to use the value analysis to have precise results
> on an example that is similar to this very simplified one :
> ------------------------------------------
> //@ assigns \nothing;
> unsigned int ext (void);
>
> int N = 0;
>
> unsigned int local (void) {
>   unsigned int f = ext ();
>   if (f) N++;
>   Frama_C_dump_each ();
>   return f;
> }
>
> int main (void) {
>   unsigned int f = local ();
>   Frama_C_dump_each ();
>   if (f) N--;
>   //@ assert N == 0;
>   return 0;
> }
> ------------------------------------------
>
> Using : frama-c -val test.c -slevel 100
> The first Frama_C_dump_each (in 'local') shows
> that the context is split in two parts :
> [value] DUMPING STATE of file test.c line 13
>         N ? {1}
>         f ? [1..4294967295]
>         =END OF DUMP==
> [value] DUMPING STATE of file test.c line 13
>         N ? {0}
>         f ? {0}
>         =END OF DUMP==
> what is exactly what I expected. But unfortunately, it seems that
> the two states are then merged before being propagated to the 'main'
> as shown by the second Frama_C_dump_each (in 'main') :
> [value] DUMPING STATE of file test.c line 19
>         N ? {0; 1}
>         f ? [--..--]
>         =END OF DUMP==
> I then get :
> test.c:20:[value] assigning non deterministic value for the first time
> test.c:21:[value] Assertion got status unknown.
>
> I managed to get the precise result with :
> $ frama-c -val test.c -slevel 100 -val-split-return-function local:0
> [value] DUMPING STATE of file test.c line 19
>         N ? {0}
>         f ? {0}
>         =END OF DUMP==
> [value] DUMPING STATE of file test.c line 19
>         N ? {1}
>         f ? [1..4294967295]
>         =END OF DUMP==
> test.c:21:[value] Assertion got status valid.
>
> But it doesn't scale when the call stack is deeper.
>
> What would be great is to be able to specify "something" about
> either 'ext'
> (like : ensures f == 0 || f > 0;)
> or in 'local'
> (like: ensures (f == 0 && N == \old(N)) || (f > 0 && N == \old(N)+1);)
> and to tell the analysis that we would like to propagate the two states.
>
> Is it possible to do something like that ?
> Did I missed something ?
>
> Thanks in advance for your help.
> --
> Anne.
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss



-- 
Boris