Proving (F oW) true or false: alternative method
Pascal Cuoq - 22nd Aug 2012In 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.