2020-12-04 23:40 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001251Frama-CPlug-in > jessiepublic2013-03-27 09:44
Reporterboris 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001251: Binary search doesn't verify anymore after upgrade
DescriptionAfter upgarding to why 2.31 and why3 0.73, my binary search program doesn't verify with Alt-Ergo, Z3, and CVC3 and a timeout of 10s.

In particular, the
loop invariant \forall integer i; 0 <= i < low ==> a[i] < val;
doesn't verify.

The code did verify with the previous version of Jessie and it verifies with wp.

The same is true for another program, mismatch.c.

This is a show stopper as the binary search is frequently used to demonstrate formal verification.
TagsNo tags attached.
Attached Files
  • c file icon mismatch.c (699 bytes) 2012-07-31 10:53 -
    /*@	requires \valid(a+(0..length-1)) && \valid(b+(0..length-1));
        ensures  (\forall integer k; 0 <= k < length ==> a[k] == b[k])  ==>  \result == -1;
        ensures !(\forall integer k; 0 <= k < length ==> a[k] == b[k])  ==>  0 <= \result < length && a[\result] != b[\result];
    	assigns \nothing;
    */
    int mismatch(int a[], int b[], int length)
    {
    	int k;
    	/*@	loop invariant \forall integer l; 0 <= l < k ==> a[l] == b[l];
    		loop invariant 0 <= k;
    		loop assigns k;
    		loop variant length - k;
    	*/
    	for (k = 0; k < length; k++)
    		if(a[k] != b[k]) return k;
    	return -1;
    }
    
    
    int main() {
    	int a[] = {12,4,5,3,99};
    	int b[] = {12,4,6,2,99};
    	int k;
    
    	k = mismatch(a, b, 5);
    	//@assert k == 2;
    	return 0;
    }
    
    c file icon mismatch.c (699 bytes) 2012-07-31 10:53 +
  • c file icon binary-search.c (1,190 bytes) 2012-08-20 20:27 -
    /*@ predicate Sorted{L}(int *a, integer l, integer r) =
    		\forall integer i,j; l <= i < j <= r ==> a[i] <= a[j];
     */
    
    /*@ requires \valid(a+ (0..a_length-1)) && a_length >= 0;
    	requires Sorted(a,0,a_length-1);
    	assigns \nothing;
    	behavior success:
    		assumes \exists integer res; 0 <= res <= a_length-1 && a[res] == val;
    		ensures 0 <= \result <= a_length-1	&&	a[\result] == val;
    	behavior failure:
    		assumes !(\exists integer res; 0 <= res <= a_length-1 && a[res] == val);
    		ensures \result == -1;
    	complete behaviors;
    	disjoint behaviors;
     */
    int bsearch(int a[], int a_length, int val) {
    	int low, mid, high;
    
    	low = 0; high = a_length-1;
    	/*@ loop invariant 0 <= low && high <= a_length-1;
    		loop invariant \forall integer i; 0 <= i < low  ==>  a[i] < val;
    		loop invariant \forall integer i; high < i <= a_length-1  ==>  a[i] > val;
    		loop assigns low, high, mid;
    		loop variant high-low;
    	*/
    	while(low <= high) {
    		mid = low + (high - low) / 2;
    //		mid = (high + low) / 2;
    		if (a[mid] < val) low = mid+1;
    		else if(a[mid] > val) high = mid-1;
    		else return mid;
    	}
    	return -1;
    }
    
    
    
    int main() {
    	int a[6] = {1,3,4,6,8,19};
    	int k = bsearch(a, 6, -8);
    	//assert k == -1;
    	return 0;
    }
    
    c file icon binary-search.c (1,190 bytes) 2012-08-20 20:27 +
  • html file icon bts1251.html (10,998 bytes) 2012-08-21 13:30
  • png file icon gWhy.png (281,751 bytes) 2012-08-21 15:05
  • ? file icon .why3.conf (1,358 bytes) 2012-08-21 18:18
  • ? file icon .whyrc (458 bytes) 2012-08-21 18:19
  • ? file icon why3.conf (327 bytes) 2012-08-22 13:27
  • html file icon binary-search.html (3,117 bytes) 2012-08-22 20:36

-Relationships
+Relationships

-Notes

~0003401

cmarche (developer)

The attached file is mismatch.c and does not contain a binary search function.
Please provide the proper example so that I can figure out the problem.

~0003403

boris (reporter)

Sorry, this is the binary search file.

~0003404

cmarche (developer)

I can't reproduce the problem, for me the program is proved.

I attach the results I obtained with several versions of those provers, see bts1251.html.

Please give more info on what is not proved on your side.

~0003405

cmarche (developer)

By the way, you could send your own results by sending the .xml file that is located in

  binary-search.jessie/binary-search/why3session.xml

note that the html file can be generated using

  why3session html binary-search.jessie/binary-search

resulting in a file

  binary-search.jessie/binary-search/binary-search.html

~0003407

boris (reporter)

As bts1251 shows, Alt-Ergo and CVC3 time-out why trying to prove

loop invariant \forall integer i; 0 <= i < low ==> a[i] < val;

The same happens on my system with Z3 4.0. It used to verify with Alt-Ergo with the previous version of why. However, it verifies with Simplify. I use the command line

frama-c -jessie -jessie-atp=gui -pp-annot

since the why3 gui doesn't work (see why3 bug 14672).

Unfortunately, there is no .xml-file located in any subdirectory:

~/progs/c/frama-c/binary-search$ find . -type f -name *.xml
~/progs/c/frama-c/binary-search$

Therefore, I can't generate an html-file:
~/progs/c/frama-c/binary-search$ why3session html binary-search.jessie/binary-search

anomaly: Not_found

~0003408

cmarche (developer)

Sorry, I did not understand you were using Why2 GUI, not Why3.

Could you send me your ~/.why3.conf so that I can try to figure out what is the problem with Why3 ?

Alos, did you do "why3config --detect" ?

~0003409

boris (reporter)

I haven't done "why3config --detect" yet. This command gives an error

The plugin /usr/local/lib/why3/plugins/tptpfof.cmxs dynlink failed :
Dynlink error : error loading shared library: /usr/local/lib/why3/plugins/tptpfo

but it detects my provers. If I now run

frama-c -jessie binary-search.c

I still get

[jessie] Calling VCs generator.
why3ml [...] binary-search.mlw

field 'name' is missing
make: *** [why3ml] Error 1
[jessie] user error: Jessie subprocess failed: make -f binary-search.makefile why3ml

I reported this as bug 14672 in the why3 bts.

~0003411

cmarche (developer)

I am still trying to understand the problem but no success yet. Please could you attach the following file ?

/usr/local/lib/why/why3/why3.conf

~0003412

cmarche (developer)

Sorry, I don't understand where is the problem.

I tried to make fresh install of why3 0.73 and why 2.31 and the problem does not show up with me.

The only possibility I see would be that for some reason your why3 does not use the ~/.why3.conf generated but some other configuration file. Could you check that?

One possible try: run manually the command

why3ide --debug-all t.jessie/t.mlw

and send me what is printed on screen

~0003413

boris (reporter)

Maybe you mean binary-search instead of t?

~/progs/c/frama-c/binary-search$ why3ide --debug-all binary-search.jessie/binary-search.mlw
<0.011314>[Info] Init the GTK interface...<0.017468> done.
<0.017506>[Info] reading icons...<0.037217> done.
<0.074332>[Info] Creating tree model...<0.075364> done
<0.103482>[Info] found regular file 'binary-search.jessie/binary-search.mlw'
<0.103531>[Info] using 'binary-search.jessie/binary-search' as directory for the project
<0.103573>[Info] 'binary-search.jessie/binary-search' does not exists. Creating directory of that name for the project
<0.103685>[Info] Opening session...
            <0.103715>[Info] update_session: shape_version = 2
            <0.103741>[Info] update_session: done
            <0.103754>[Sched] init scheduler max=2
<0.103804>
[Info] Opening session: done
<0.103845>[Info] adding file ../binary-search.mlw in database
<0.103868>[Load] file '../binary-search.mlw'
Error while reading file '../binary-search.mlw':
Library file not found: jessie3

/usr/local/lib$ find . -type f -name jessie3*
./why/why3/jessie3_integer.why
./why/why3/jessie3.why
./why/why3/jessie3.mlw

/usr/local/lib$ ocamlc -v
The Objective Caml compiler, version 3.12.1
Standard library directory: /usr/lib/ocaml

I use Debian 7.

~0003414

cmarche (developer)

Last edited: 2012-08-22 16:58

I'm surprised that the error "field name is missing" does not show up.
What happens if you do

  why3ide --debug-all --extra-config /usr/local/lib/why/why3/why3.conf binary-search.jessie/binary-search.mlw

and then if you retry

  frama-c -jessie binary-search.c

?

~0003415

boris (reporter)

~/progs/c/frama-c/binary-search$ why3ide --debug-all --extra-config /usr/local/lib/why/why3/why3.conf binary-search.jessie/binary-search.mlw

field 'name' is missing
~/progs/c/frama-c/binary-search$ frama-c -jessie binary-search.c
[kernel] preprocessing with "gcc -C -E -I. -dD binary-search.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir binary-search.jessie
[jessie] File binary-search.jessie/binary-search.jc written.
[jessie] File binary-search.jessie/binary-search.cloc written.
[jessie] Calling Jessie tool in subdir binary-search.jessie
Generating Why function bsearch
Generating Why function main
[jessie] Calling VCs generator.
why3ml [...] binary-search.mlw

field 'name' is missing
make: *** [why3ml] Error 1
[jessie] user error: Jessie subprocess failed: make -f binary-search.makefile why3ml

~0003416

cmarche (developer)

Then this shows that the problem is related to /usr/local/lib/why/why3/why3.conf
Great!

But still I don't see why...

could you edit the file /usr/local/lib/why/why3/why3.conf and remove the section headed by [prover coq], and try again please ?

Indeed you can remove everything except the first two lines
[main]
loadpath = " ..."

~0003417

cmarche (developer)

Even better: I've now been able to reproduce the bug !

The [prover coq] section appearing in /usr/local/lib/why/why3/why3.conf causes problem if
Coq is not installed, which is your case.

OK, thanks for your time, I'm now able to fix the problem.

In the meantime, removing the [prover coq] section should work for you

~0003418

boris (reporter)

Alright, I can use why3 now. While the binary search itself now verifies, the call in main doesn't. I split all unproven goals until no further split was possible. Yet, "Function main, Safety" runs in a time-out (see attachment).

~0003419

cmarche (developer)

The problem with main unproved is related to the weaknesses of Jessie regarding allocation. I guess you mean it was proved with Why2 before ?

~0003420

boris (reporter)

Yes, all VCs in binary-search.c were proved with the previous version of Why2/Jessie and Alt-Ergo.

~0003421

cmarche (developer)

Indeed you found another bug ! it was introduced by the migration of the Jessie memory model from Why2 to Why3.

You can fixed yourselves, by modifying the file

/usr/local/lib/why/why3/jessi3.mlw

look for this
---------------
val free_parameter (a:ref (alloc_table 't)) (p:pointer 't) :
  { p = null (* allowed, see man 3 free *) /\
---------------
and change the last /\ by \/

This is fixed in the devt version. I think we are going to make a bug-fix release of Why 2 soon,

Thanks again for testing and finding thoses bugs !

~0003778

signoles (manager)

Fixed in Frama-C Oxygen + Why 2.32.
+Notes

-Issue History
Date Modified Username Field Change
2012-07-31 10:53 boris New Issue
2012-07-31 10:53 boris Status new => assigned
2012-07-31 10:53 boris Assigned To => cmarche
2012-07-31 10:53 boris File Added: mismatch.c
2012-08-20 14:06 cmarche Note Added: 0003401
2012-08-20 20:27 boris File Added: binary-search.c
2012-08-20 20:28 boris Note Added: 0003403
2012-08-21 13:30 cmarche File Added: bts1251.html
2012-08-21 13:31 cmarche Note Added: 0003404
2012-08-21 13:35 cmarche Note Added: 0003405
2012-08-21 15:05 boris Note Added: 0003407
2012-08-21 15:05 boris File Added: gWhy.png
2012-08-21 15:58 cmarche Note Added: 0003408
2012-08-21 18:18 boris Note Added: 0003409
2012-08-21 18:18 boris File Added: .why3.conf
2012-08-21 18:19 boris File Added: .whyrc
2012-08-22 12:41 cmarche Note Added: 0003411
2012-08-22 13:27 boris File Added: why3.conf
2012-08-22 13:47 cmarche Note Added: 0003412
2012-08-22 14:35 boris Note Added: 0003413
2012-08-22 16:31 cmarche Note Added: 0003414
2012-08-22 16:58 cmarche Note Edited: 0003414
2012-08-22 17:09 boris Note Added: 0003415
2012-08-22 17:38 cmarche Note Added: 0003416
2012-08-22 17:44 cmarche Note Added: 0003417
2012-08-22 20:36 boris File Added: binary-search.html
2012-08-22 20:39 boris Note Added: 0003418
2012-08-23 10:20 cmarche Note Added: 0003419
2012-08-23 10:30 boris Note Added: 0003420
2012-08-23 10:37 cmarche Note Added: 0003421
2012-08-23 10:41 cmarche Status assigned => resolved
2012-08-23 10:41 cmarche Resolution open => fixed
2013-03-27 09:43 signoles Note Added: 0003778
2013-03-27 09:44 signoles Fixed in Version => Frama-C Oxygen-20120901
2013-03-27 09:44 signoles Status resolved => closed
+Issue History