Frama-C news and ideas

To content | To menu | To search | Frama-C Home

Proving (F oW) true or false: alternative method

In the context of the RERS 2012 competition, the previous post points out that value analysis option -obviously-terminates can be used to prove the termination of an instrumented program, created such that its termination implies that the property (F oW) is true of the original competition program. Unfortunately, this only works in one direction. If the property (F oW) does not hold of the original competition program, this approach cannot be used to prove that. The previous post continued to offer a method, involving a counter, that works in both directions.

Preliminary remark regarding the counter method

The second method proposed in the previous post requires a state count to use as bound. I suggested to use the number of reachable states of the original (uninstrumented) program, obtained by running Frama-C's value analysis as a sound and complete abstract interpreter.

I would like to point out that instead of the state count of the original program, it is possible to use the state count of the program instrumented to stop when W is emitted. This number is by definition lower. On the other hand, the number of states of the uninstrumented program can be computed once and for all, and then be used for all formulas of the form (F oW) that apply to that program in the competition. In fact we can obtain that number for free when we check the reachability of assert(0); statements for the competition. So there is a trade-off there.

Applying the method of last post

Let us now consider Problem3.c (small-hard). One of the properties to evaluate is (F oY). The first method described in the previous post does not conclude rapidly, so there is reason to suspect that perhaps the property is false for this program. But if this is going to be our answer in the competition, we had better establish that the property is definitely false, that is, there exists an infinite execution along which Y is not emitted.

Instrumenting with a counter

To establish that the property is false using a counter, we instrument Problem3.c thus:

--- Problem3.c	2012-08-08 10:49:53.000000000 +0200
+++ Problem3_terminate_at_Y_with_counter.c	2012-08-22 13:58:30.000000000 +0200
@@ -1,9 +1,8 @@
 void assert(int x)
 {
   if (!x)
     {
-      Frama_C_show_each_assert_reached();
       /*@ assert \false; */
     }
 }
 
@@ -1649,15 +1648,16 @@
 	    } 
 	    if((((((((!(a26==1)&&(a6==1))&&!(a27==1))&&(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
 	    	error_2: assert(0);
 	    } 
-	    return -2; 
+	    /*@ assert \false ; */
 	}
 
 int main()
 {
     // default output
     int output = -1;
+    int counter = 0;
 
     // main i/o-loop
     while(1)
     {
@@ -1668,6 +1668,10 @@
 
         // operate eca engine
         output = calculate_output(input);
 
+	/*@ assert output != y ; */
+
+	counter++;
+	Frama_C_show_each_counter(counter);
     }
 }

Obtaining a bound

In order to obtain a bound, we analyze the original program, using the value analysis as a model-checker:

$ frama-c -val -slevel 100000000 Problem3.c
...
[value] Semantic level unrolling superposing up to 200 states
...

This message means there are up to a number between 200 and 300 states attached to a single statement during the analysis of the program. That statement is probably the statement just after a new input has been picked non-deterministically between 1 and 6, and the number therefore six times higher than the number of states that interests us. The abstract interpreter also distinguishes states program that differ only for variable output, again making the bound displayed in the “superposing up to” messages higher than the number we mean. But let us not try to compensate for that, just to be on the safe side.


I kid, I kid. Using the “superposing up to” message is not rigorous, since this message was not designed for that (and the message is not documented at all, I think). As a Frama-C developer with knowledge of value analysis internals, I am tempted to use 300 as a safe bound, but in order to obtain a rigorous number of states, anyone can insert the following statement in the while loop of the program:

Frama_C_show_each_state( a1, a4, a0, a15, a29, a10, a16, a22, a2, a17, a25, a7, a14, a19, a20, a8, a23, a21, a24, a13, a9, a28, a26, a6, a27, a12, a3, a11, a5, a18 );

Once filtered, sorted and de-duplicated, the list of states is exactly 31 long. Once de-duplicated, the messages printed by the call correspond exactly to unique states of the program. This method provides an exact number and it uses documented value analysis features only. The list is provided at the end of the post for the doubters.

Looking for an execution with more than 31 transitions

Knowing that we are looking for an execution where counter goes higher than 31, we can now launch the analysis of the version instrumented with counter:

$ frama-c -val -slevel 100000000 -no-val-show-progress Problem3_terminate_at_Y_with_counter.c
...
[value] Called Frama_C_show_each_counter({1})
[value] Called Frama_C_show_each_counter({1})
[value] Called Frama_C_show_each_counter({1})
[value] Called Frama_C_show_each_counter({1})
[value] Called Frama_C_show_each_counter({1})
Problem3_terminate_at_Y_with_counter.c:5:[value] Assertion got status invalid (stopping propagation).
[value] Called Frama_C_show_each_counter({2})
...
[value] Called Frama_C_show_each_counter({31})
...
[value] Called Frama_C_show_each_counter({31})
[value] Called Frama_C_show_each_counter({32})
...
[value] Called Frama_C_show_each_counter({32})
^C

This means that there is at least one infinite execution in the instrumented program, which means that the original program can execute infinitely without emitting Y.

A method not involving a transition counter

An irritating feature of the previously described method is that it does not immediately detect infinite executions that are right under its nose. There could exist, for a certain input, a transition from the initial state to itself, and the analyzer would still have to explore all other transitions, breadth-first, down to a depth of 31, before displaying the Called Frama_C_show_each_counter({32}) message that confirms the existence of an infinite execution.

A method to look for this cycle of length one would be to instrument the program differently. This is what I describe now.

Add variables to the program for the description of the predecessor state

This means transforming the declarations

	int a1 = 1;
	int a4 = 1;
...

into:

	int a1 = 1, p1 = -1;
	int a4 = 1, p4 = -1;
...

This can be done with a regexp.

Check whether a newly reached state coincides with its predecessor state

At the end of a cycle, we compare the new state with the predecessor state. Again, code doing this can be generated with a regexp:

        if 
        ((a1 == p1) &&
        (a4 == p4) &&
...
        (a18 == p18))
          Frama_C_show_each_cycle_found(1);

The above causes a message to be emitted by the analyzer as soon as a cycle is found.

Update the predecessor state

After checking whether the new state coincides with the predecessor state, it is time to update the predecessor state. Yada regexp yada:

        p1 = a1;
        p4 = a4 ;
...
        p18 = a18 ;

And presto: we detect all cycles. All cycles of length one, that is.

Maybe update the predecessor state

Although it would work great on the example that motivated this new method, detecting only cycles of length one is a little bit too specific. Let us fix that.

At the end of a cycle, instead of updating the predecessor state as above, let us maybe update it as below:

    if (any_int())
    {
            p1 = a1;
            p4 = a4 ;
...
            p18 = a18 ;
    }

With the above non-deterministic update of the predecessor state, for each vector a1, a4, ...a18 of variables propagated by the value analysis, the variables p1, p4, ...p18 contain a nondeterministic superposition of all its predecessors. Think of it as programming a quantum computer, and if you think of it this way, remember that the variables p1, p4, ...p18 are entangled: when observed, they contain matching values from one specific predecessor. They are entangled because the conditional above either update variables p1, p4, ... all at once or leaves them all unchanged.


On the other hand, different predecessors do not get mixed together because... well, because the analyzer remains complete on this program even after it being instrumented thus, for reasons I still do not want to document. Nevertheless, the important part of the argument is that a sound and complete analyzer would find the Frama_C_show_each_cycle_found(1); statement above reachable if and only if in the program instrumented to stop at Y, a state is identical to one of its predecessors. Hopefully it is possible to convince oneself of that much without being a value analysis expert—although I admit that programming nondeterministic machines is an unusual exercise.


Using Frama-C's value analysis as a sound and complete abstract interpreter, the statement Frama_C_show_each_cycle_found(1); will be reached, and a message be displayed, exactly when a state is reached that is identical to one of its predecessors. This happens if and only if there is a cycle in the transition graph of the program instrumented to stop at Y. In terms of the original program, this corresponds to (F oY) being false.

Putting the new method to the test

Running the value analysis on the program instrumented as described:

$ frama-c -val -slevel 100000000 -no-val-show-progress Problem3_terminate_at_Y_with_predecessor.c 
...
[value] Semantic level unrolling superposing up to 100 states
[value] Semantic level unrolling superposing up to 200 states
[value] Called Frama_C_show_each_cycle_found({1})
^C

Incidentally, on this example, this new method is much faster than the method involving a counter. It is not clear that it should always be the case, and on difficult examples, the two methods can perhaps be tried in parallel.

Annex: an exhaustive list of states for Problem 3

Below is the list of unique states displayed when the statement

Frama_C_show_each_state( a1, a4, a0, a15, a29, a10, a16, a22, a2, a17, a25, a7, a14, a19, a20, a8, a23, a21, a24, a13, a9, a28, a26, a6, a27, a12, a3, a11, a5, a18 );

is inserted in the while loop of Program3.c.

[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{0},{0},{0},{0},{1},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{0},{0},{0},{0},{2},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{0},{0},{0},{1},{0},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{0},{0},{1},{0},{0},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{0},{0},{1},{0},{1},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{0},{0},{1},{0},{2},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{0},{1},{0},{1},{1},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{0},{1},{0},{1},{2},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{0},{1},{1},{0},{1},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{0},{1},{1},{0},{2},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{0},{1},{1},{1},{2},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{0},{0},{0},{0},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{0},{0},{0},{1},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{0},{0},{0},{1},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{0},{0},{1},{0},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{0},{0},{1},{2},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{0},{1},{0},{0},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{0},{1},{0},{1},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{0},{1},{0},{2},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{0},{1},{1},{1},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{0},{1},{1},{2},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{1},{0},{0},{1},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{1},{0},{0},{2},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{1},{0},{0},{2},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{1},{0},{1},{2},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{1},{1},{0},{1},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{1},{1},{0},{2},{0},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{1},{1},{0},{2},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{1},{1},{1},{0},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{1},{1},{1},{1},{1},{1},{1})
[value] Called Frama_C_show_each_state({1},{1},{1},{1},{1},{1},{1},{1},{0},{0}, {0},{0},{0},{0},{0},{0},{0},{1},{1},{1}, {1},{1},{1},{1},{1},{1},{2},{0},{1},{1})


This post benefited from discussions with Sébastien Bardin, Sven Mattsen, Benjamin Monate and Boris Yakobowski.