<commit_before>Workflow
========
(See 'scripts' directory for the shell scripts.  Add them to your PATH.)

0. Record standard WHILEY compiler/verifier results in a WHILEY subdirectory

   cd ../WhileyCompiler/tests/valid
   mkdir WHILEY
   wyc2results

1. Run all valid tests through Wyil2Boogie and Boogie:
   (Just the 'GOOD' subset that Whiley can compile and typecheck correctly).

   # cd ../WhileyCompiler/tests/valid
   VALID=$(ls *.whiley | fgrep -v -f WHILEY/ignore_compile.txt)
   wyboogie $VALID >OUTnnn.txt 2>&1

2. See how many tests passed/failed etc.

   wystats OUTnnn.txt

3. Analyse the result for each valid test program:

   wyresults OUTnnn.txt >OUTnnn.results

4. Compare those results against the Whiley verifier:
   (It shows all those that differ, plus summary stats at the end).

   wydiff OUTnnn.results
   wydiff OUTnnn.results OUTmmm.results   # to compare with a previous run


5. Repeat above steps for the WhileyCompiler/tests/invalid tests - none should pass.

   cd ../WhileyCompiler/tests/valid
   mkdir WHILEY
   grep "IGNORED.put(" ../../src/test/java/wyc/testing/AllInvalidTest.java \
       | sort | awk '-F"' '{print $2}' >WHILEY/ignore_compile.txt
   INVALID=$(ls *.whiley | fgrep -v -f WHILEY/ignore_compile.txt)
   wyboogie $VALID >OUTnnn.txt 2>&1
   wystats OUTnnn.txt
   wyresults OUTnnn.txt >OUTnnn.results
   echo "Now check that none of these are FullyVerified."


DONE:
Investigated running output Boogie programs using Boogaloo:
    https://bitbucket.org/nadiapolikarpova/boogaloo/wiki/Home 
    (It doesn't really 'run' the programs - it just searches for counter-examples)

Invalid Tests that pass (2019-02-18)
====================================
# none of these should be 'FullyVerified'
$ grep Full OUT101_packages.results
Ensures_Invalid_1.whiley                 FullyVerified  TODO: prove that each function is feasible.
Export_Invalid_1.whiley                  FullyVerified  Why is this not valid?  Passes Whiley verifier.
StaticVar_Invalid_5.whiley               FullyVerified  TODO: prove that each constant satisfies the claimed type.
Type_Invalid_10.whiley                   FullyVerified  Circular types.  Compiler should detect this?
Type_Invalid_11.whiley                   FullyVerified  Why is this not valid?  Passes Whiley verifier.


Results 2019-01-22 (on MacBook Pro 2013)
==================
$ time wyboogie *.whiley >OUT100b.txt 2>&1
real	14m9.191s
user	18m21.203s
sys	1m51.504s
$ wystats OUT100d.txt  (modified to record 1/10 of %).
Error Compiling:          20 	3.2%
NotImplementedYet:        35 	5.7%
Other Exceptions:          2 	0.3%
Errors in BPL:            11 	1.8%
Fully Verified:          490 	80.3%
Verify time outs:          4 	0.6%
Verify errors:            48 	7.8%
Total:  610                  (sum is 99.7%)

The differences are that with the (guarded) array equality axiom:
* 9 partially verified test programs become fully verified.
* 1 timeout proof becomes provably true. (ConstrainedRecord_Valid_9.whiley)
* 1 timeout proof becomes provably false. (BoolList_Valid_3.whiley)
$ wydiff OUT100_no_array_eq_axiom.results OUT100.results
Array_Valid_7.whiley                     PartVerified Boogie  |	Array_Valid_7.whiley                     FullyVerified
Array_Valid_8.whiley                     PartVerified Boogie  |	Array_Valid_8.whiley                     FullyVerified
Assign_Valid_5.whiley                    PartVerified Boogie  |	Assign_Valid_5.whiley                    FullyVerified
BoolList_Valid_3.whiley                  PartVerified Boogie  |	BoolList_Valid_3.whiley                  PartVerified Boogie
ConstrainedList_Valid_26.whiley          PartVerified Boogie  |	ConstrainedList_Valid_26.whiley          FullyVerified
ConstrainedRecord_Valid_9.whiley         PartVerified Boogie  |	ConstrainedRecord_Valid_9.whiley         PartVerified Boogie
ListAssign_Valid_1.whiley                PartVerified Boogie  |	ListAssign_Valid_1.whiley                FullyVerified
ListAssign_Valid_6.whiley                PartVerified Boogie  |	ListAssign_Valid_6.whiley                FullyVerified
ListGenerator_Valid_12.whiley            PartVerified Boogie  |	ListGenerator_Valid_12.whiley            FullyVerified
Subtype_Valid_1.whiley                   PartVerified Boogie  |	Subtype_Valid_1.whiley                   FullyVerified
Subtype_Valid_7.whiley                   PartVerified Boogie  |	Subtype_Valid_7.whiley                   FullyVerified

And for tests/invalid:
$ wystats OUT100.txt
Error Compiling:         235 	64%
NotImplementedYet:         5 	1%
Other Exceptions:          9 	2%
Errors in BPL:            29 	7%
Fully Verified:            5 	1%
Verify time outs:          0 	0%
Verify errors:            84 	22%
Total:  367
Note: the 5 pass programs are mostly due to needing two-pass verification.

Results 2017-10-27
==================
Add support for Value.UTF8 (Strings) in createConst.
$ wystats OUT57_const_strings.txt
Error Compiling:          11
NotImplementedYet:        75
Other Exceptions:         49
Errors in BPL:            78
Fully Verified:          325
Verify time outs:          0
Verify errors:            51


Results 2017-10-26
==================
After API updates, and git update which added a few tests.
Also, implemented ==> and <==>.
$ wystats OUT56_assert_implies.txt
Error Compiling:          11
NotImplementedYet:       106
Other Exceptions:         48
Errors in BPL:            73
Fully Verified:          305
Verify time outs:          0
Verify errors:            46

Issue: RecursiveType_Valid_28
I don't think Line 26 (assert ls.next is Link)
is valid in general, without a much stronger recursive invariant
on List and LinkedList to relate their length to their non-nullness.


Results 2017-09-05
==================
Before new IL API update.  409/548 = 74.6%
$ wystats OUT52.txt
Error Compiling:          17
NotImplementedYet:        52
Other Exceptions:         22
Errors in BPL:            24
Fully Verified:          409
Verify time outs:          3
Verify errors:            21


Results 2017-03-23
==================
(OUT41_outer_method_calls.txt, in tests_david_2017_03_19/valid)
Total tests: 531 (tests/valid has only 514)

$ wystats OUT41_outer_method_calls.txt 
Error Compiling:          34
NotImplementedYet:        44
Other Exceptions:          2
Errors in BPL:            22
Fully Verified:          406
Verify time outs:          3
Verify errors:            28

Yay!  32 method-inside-expr errors went down to just 5!
MessageSend_Valid_3.whiley  requires unfolding method calls inside exprs. 
MessageSend_Valid_4.whiley  requires unfolding method calls inside exprs.
MethodCall_Valid_2.whiley requires unfolding method calls inside exprs.
MethodCall_Valid_3.whiley requires unfolding method calls inside exprs.
Process_Valid_6.whiley requires unfolding method calls inside exprs.


Results 2016-11-08
==================
Added array index checks.
$ wystats OUT32_array_checks.txt
Error Compiling:          21
NotImplementedYet:       132
Other Exceptions:          2
Errors in BPL:            12
Fully Verified:          325
Verify time outs:          3
Verify errors:            23

$ grep -i 'bpl.*error:' OUT32_array_checks.txt
DoWhile_Valid_6.bpl(24,39): error: ")" expected
RecursiveType_Valid_7.bpl(136,72): error: invalid Type
String_Valid_4.bpl(1,20): error: ")" expected
TypeEquals_Valid_35.bpl(28,10): Error: command assigns to an immutable variable: e
UnionType_Valid_15.bpl(7,265): Error: undeclared identifier: $dum
While_Valid_22.bpl(53,22): Error: undeclared identifier: j
While_Valid_22.bpl(53,34): Error: undeclared identifier: j
While_Valid_23.bpl(25,22): Error: undeclared identifier: j
While_Valid_23.bpl(25,34): Error: undeclared identifier: j
While_Valid_42.bpl(28,19): Error: more than one declaration of variable name: j
While_Valid_42.bpl(32,19): Error: more than one declaration of variable name: j
While_Valid_42.bpl(38,26): Error: more than one declaration of variable name: j

===================================
In tests/valid
===================================

ListAccess_Valid_1.whiley has a function with no return value?


Tests where Whiley verifier passes, but Boogie fails.

===== ConstrainedList_Valid_28.whiley =====
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
ConstrainedList_Valid_28.bpl(35,13): Error BP5003: A postcondition might not hold on this return path.
ConstrainedList_Valid_28.bpl(23,5): Related location: This is the postcondition that might not hold.
Execution trace:
    ConstrainedList_Valid_28.bpl(28,5): anon0
    ConstrainedList_Valid_28.bpl(32,14): anon5_Else
    ConstrainedList_Valid_28.bpl(34,15): anon6_Then
ConstrainedList_Valid_28.bpl(38,13): Error BP5003: A postcondition might not hold on this return path.
ConstrainedList_Valid_28.bpl(20,5): Related location: This is the postcondition that might not hold.
Execution trace:
    ConstrainedList_Valid_28.bpl(28,5): anon0
    ConstrainedList_Valid_28.bpl(32,14): anon5_Else
    ConstrainedList_Valid_28.bpl(37,15): anon6_Else
ConstrainedList_Valid_28.bpl(38,13): Error BP5003: A postcondition might not hold on this return path.
ConstrainedList_Valid_28.bpl(21,5): Related location: This is the postcondition that might not hold.
Execution trace:
    ConstrainedList_Valid_28.bpl(28,5): anon0
    ConstrainedList_Valid_28.bpl(32,14): anon5_Else
    ConstrainedList_Valid_28.bpl(37,15): anon6_Else
ConstrainedList_Valid_28.bpl(38,13): Error BP5003: A postcondition might not hold on this return path.
ConstrainedList_Valid_28.bpl(24,5): Related location: This is the postcondition that might not hold.
Execution trace:
    ConstrainedList_Valid_28.bpl(28,5): anon0
    ConstrainedList_Valid_28.bpl(32,14): anon5_Else
    ConstrainedList_Valid_28.bpl(37,15): anon6_Else

Boogie program verifier finished with 1 verified, 4 errors

NOTE: this is a recursive function call, so might require induction?
Whiley verifier does not verify this one either.


===== ConstrainedList_Valid_8.whiley =====
MUTATED INPUT list : ConstrainedList_Valid_8:nat[]
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
ConstrainedList_Valid_8.bpl(44,5): Error BP5001: This assertion might not hold.
Execution trace:
    ConstrainedList_Valid_8.bpl(41,8): anon0
ConstrainedList_Valid_8.bpl(46,5): Error BP5001: This assertion might not hold.
Execution trace:
    ConstrainedList_Valid_8.bpl(41,8): anon0
ConstrainedList_Valid_8.bpl(48,5): Error BP5001: This assertion might not hold.
Execution trace:
    ConstrainedList_Valid_8.bpl(41,8): anon0

Boogie program verifier finished with 1 verified, 3 errors

This modifies xs each time xs = update(xs, ..., ...) is called.
So the update function needs a postcondition to say that it
returns a list with the same length as the input list:

    ensures |out| == |list|:

With this added, all assertions verify.

===== DoWhile_Valid_6.whiley =====
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
DoWhile_Valid_6.bpl(25,9): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
    DoWhile_Valid_6.bpl(22,7): anon0

Boogie program verifier finished with 1 verified, 1 error

NOTE: Boogie is correct - i < |items| is not true initially.
My encoding of do-while loops breaks the loop invariant, in this case,
because it checks the invariant before the first iteration.
But shouldn't an invariant be true at the beginning and end of EVERY
iteration?  In that case, this loop invariant is incorrect.

7/2/2017 After fixing do-while translation to NOT check inv before first iteration:
  I cannot see why Boogie still cannot prove the invariants:
        assert toInt(i) >= - 1;
        assert toInt(i) < arraylen(items);
        
===== DoWhile_Valid_8.whiley =====
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
DoWhile_Valid_8.bpl(24,9): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
    DoWhile_Valid_8.bpl(21,7): anon0
DoWhile_Valid_8.bpl(24,9): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
    DoWhile_Valid_8.bpl(21,7): anon0
    DoWhile_Valid_8.bpl(23,5): anon5_LoopHead
    DoWhile_Valid_8.bpl(26,19): anon5_LoopBody
    DoWhile_Valid_8.bpl(27,9): anon6_Else

Boogie program verifier finished with 1 verified, 2 errors

NOTE: same issue.

===== Ensures_Valid_3.whiley =====
$ boogie wval.bpl Ensures_Valid_3.bpl 
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
Ensures_Valid_3.bpl(52,5): Error BP5003: A postcondition might not hold on this return path.
Ensures_Valid_3.bpl(18,5): Related location: This is the postcondition that might not hold.
Execution trace:
    Ensures_Valid_3.bpl(26,7): anon0
    Ensures_Valid_3.bpl(29,5): anon9_LoopHead
    Ensures_Valid_3.bpl(29,5): anon9_LoopDone
    Ensures_Valid_3.bpl(41,5): anon11_LoopHead
    Ensures_Valid_3.bpl(41,5): anon11_LoopDone

Boogie program verifier finished with 1 verified, 1 error

NOTE: this will require looking at the counter-example model.
Probably an array equality issue?
(My WVal theory needs stronger equality axioms for arrays)

===== Fail_Valid_1.whiley =====
$ boogie wval.bpl Fail_Valid_1.bpl 
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
Fail_Valid_1.bpl(34,13): Error BP5001: This assertion might not hold.
Execution trace:
    Fail_Valid_1.bpl(26,5): anon0
    Fail_Valid_1.bpl(30,9): anon5_Else
    Fail_Valid_1.bpl(34,13): anon6_Else

Boogie program verifier finished with 1 verified, 1 error

NOTE: here the test seems to be invalid?
Because fail will be reached when input x is null.
This test works if we change the 'fail' to:
        assert x is null
        return x

===== While_Valid_22.whiley =====
mangle max : function(int[])->(int) to max$2
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
While_Valid_22.bpl(54,9): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
    While_Valid_22.bpl(50,7): anon0
    While_Valid_22.bpl(52,5): anon3_LoopHead
    While_Valid_22.bpl(57,11): anon3_LoopBody
While_Valid_22.bpl(55,9): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
    While_Valid_22.bpl(50,7): anon0
    While_Valid_22.bpl(52,5): anon3_LoopHead
    While_Valid_22.bpl(57,11): anon3_LoopBody

Boogie program verifier finished with 2 verified, 2 errors

NOTE: probably an array equality issue.




OLDER RESULTS (before implementing equality fully)
===== Complex_Valid_2.whiley =====
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
Complex_Valid_2.bpl(185,9): Error BP5003: A postcondition might not hold on this return path.
Complex_Valid_2.bpl(176,5): Related location: This is the postcondition that might not hold.
Execution trace:
    Complex_Valid_2.bpl(180,5): anon0
    Complex_Valid_2.bpl(181,13): anon11_Then
Boogie program verifier finished with 4 verified, 1 error

===== Complex_Valid_8.whiley =====
Boogie program verifier finished with 5 verified, 1 error

===== DoWhile_Valid_6.whiley =====
Boogie program verifier finished with 1 verified, 1 error

===== DoWhile_Valid_8.whiley =====
Boogie program verifier finished with 1 verified, 2 errors

===== Fail_Valid_1.whiley =====
Boogie program verifier finished with 1 verified, 1 error
  This is not valid, because when f(null) is called, the 'fail' is reachable.
  Boogie correctly detects this.

===== RecordAssign_Valid_6.whiley =====
Boogie program verifier finished with 0 verified, 1 error



====================================
Whiley Language Questions
====================================
1. What types can be compared using '==' and '!='?
    What types can be compared using '<', '<=' etc.?

<commit_msg>Add results of OUT119 improvements.<commit_after>Workflow
========
(See 'scripts' directory for the shell scripts.  Add them to your PATH.)

0. Record standard WHILEY compiler/verifier results in a WHILEY subdirectory

   cd ../WhileyCompiler/tests/valid
   mkdir WHILEY
   wyc2results

1. Run all valid tests through Wyil2Boogie and Boogie:
   (Just the 'GOOD' subset that Whiley can compile and typecheck correctly).

   # cd ../WhileyCompiler/tests/valid
   VALID=$(ls *.whiley | fgrep -v -f WHILEY/ignore_compile.txt)
   wyboogie $VALID >OUTnnn.txt 2>&1

2. See how many tests passed/failed etc.

   wystats OUTnnn.txt

3. Analyse the result for each valid test program:

   wyresults OUTnnn.txt >OUTnnn.results

4. Compare those results against the Whiley verifier:
   (It shows all those that differ, plus summary stats at the end).

   wydiff OUTnnn.results
   wydiff OUTnnn.results OUTmmm.results   # to compare with a previous run


5. Repeat above steps for the WhileyCompiler/tests/invalid tests - none should pass.

   cd ../WhileyCompiler/tests/valid
   mkdir WHILEY
   grep "IGNORED.put(" ../../src/test/java/wyc/testing/AllInvalidTest.java \
       | sort | awk '-F"' '{print $2}' >WHILEY/ignore_compile.txt
   INVALID=$(ls *.whiley | fgrep -v -f WHILEY/ignore_compile.txt)
   wyboogie $VALID >OUTnnn.txt 2>&1
   wystats OUTnnn.txt
   wyresults OUTnnn.txt >OUTnnn.results
   echo "Now check that none of these are FullyVerified."


DONE:
Investigated running output Boogie programs using Boogaloo:
    https://bitbucket.org/nadiapolikarpova/boogaloo/wiki/Home 
    (It doesn't really 'run' the programs - it just searches for counter-examples)


Invalid Tests that pass (2019-08-13)
====================================
real	4m38.105s
user	6m10.365s
sys	0m45.650s
# none of these should be 'FullyVerified'
# the last two pass because Boogie translation does not yet check type invariants after init/assign.
Ensures_Invalid_4.whiley                 FullyVerified  Whiley verifier says loop invar not restored, but seems ok?
Subtype_Invalid_10.whiley                FullyVerified  Assignment x[0].f=2 should break type invariant?

Valid Test results at 2019-08-13
================================
Total execution time: (significantly longer!  was 15-18mins)
$ time wyboogie $VALID >OUT119_type_check_init.txt 2>&1
real	23m57.637s
user	23m49.427s
sys	2m36.542s
$ wystats OUT119_type_check_init.txt
Syntax/type error:         0 	0%
Error Compiling:           0 	0%
NotImplementedYet:        23 	3%
Other Exceptions:          2 	0%
Errors in BPL:            10 	1%
Fully Verified:          543 	86%
Verify time outs:          5 	0%
Verify errors:            48 	7%
Total:  631

$ wydiff OUT119_type_check_init.results  |grep -v 'PartVerified *.*whiley *PartVerified'
Array_Valid_9.whiley                     FullyVerified	      |	Array_Valid_9.whiley                     BplErrors
Complex_Valid_10.whiley                  PartVerified	      |	Complex_Valid_10.whiley                  Timeouts Boogie prog
Complex_Valid_11.whiley                  FullyVerified	      |	Complex_Valid_11.whiley                  Timeouts Boogie prog
Complex_Valid_2.whiley                   PartVerified	      |	Complex_Valid_2.whiley                   FullyVerified
Complex_Valid_4.whiley                   PartVerified	      |	Complex_Valid_4.whiley                   FullyVerified
Complex_Valid_8.whiley                   PartVerified	      |	Complex_Valid_8.whiley                   FullyVerified
ConstrainedInt_Valid_22.whiley           PartVerified	      |	ConstrainedInt_Valid_22.whiley           FullyVerified
ConstrainedList_Valid_2.whiley           FullyVerified	      |	ConstrainedList_Valid_2.whiley           PartVerified Boogie
ConstrainedList_Valid_21.whiley          FullyVerified	      |	ConstrainedList_Valid_21.whiley          Timeouts Boogie prog
ConstrainedList_Valid_23.whiley          FullyVerified	      |	ConstrainedList_Valid_23.whiley          BplErrors
ConstrainedList_Valid_26.whiley          PartVerified	      |	ConstrainedList_Valid_26.whiley          FullyVerified
ConstrainedRecord_Valid_8.whiley         FullyVerified	      |	ConstrainedRecord_Valid_8.whiley         PartVerified Boogie
DoWhile_Valid_6.whiley                   FullyVerified	      |	DoWhile_Valid_6.whiley                   PartVerified Boogie
DoWhile_Valid_8.whiley                   FullyVerified	      |	DoWhile_Valid_8.whiley                   PartVerified Boogie
Ensures_Valid_6.whiley                   PartVerified	      |	Ensures_Valid_6.whiley                   FullyVerified
FunctionRef_Valid_9.whiley               FullyVerified	      |	FunctionRef_Valid_9.whiley               PartVerified Boogie
IfElse_Valid_4.whiley                    PartVerified	      |	IfElse_Valid_4.whiley                    FullyVerified
IntAdd_Valid_1.whiley                    PartVerified	      |	IntAdd_Valid_1.whiley                    FullyVerified
IntDiv_Valid_3.whiley                    PartVerified	      |	IntDiv_Valid_3.whiley                    FullyVerified
IntMul_Valid_2.whiley                    PartVerified	      |	IntMul_Valid_2.whiley                    FullyVerified
IntOp_Valid_1.whiley                     PartVerified	      |	IntOp_Valid_1.whiley                     FullyVerified
Lambda_Valid_6.whiley                    FullyVerified	      |	Lambda_Valid_6.whiley                    PartVerified Boogie
Lifetime_Valid_1.whiley                  FullyVerified	      |	Lifetime_Valid_1.whiley                  BplErrors
Lifetime_Valid_11.whiley                 FullyVerified	      |	Lifetime_Valid_11.whiley                 PartVerified Boogie
Lifetime_Valid_3.whiley                  FullyVerified	      |	Lifetime_Valid_3.whiley                  BplErrors
ListAccess_Valid_1.whiley                FullyVerified	      |	ListAccess_Valid_1.whiley                Exception
ListAccess_Valid_3.whiley                FullyVerified	      |	ListAccess_Valid_3.whiley                Exception
MessageSend_Valid_2.whiley               FullyVerified	      |	MessageSend_Valid_2.whiley               PartVerified Boogie
MessageSend_Valid_5.whiley               FullyVerified	      |	MessageSend_Valid_5.whiley               PartVerified Boogie
MethodCall_Valid_4.whiley                FullyVerified	      |	MethodCall_Valid_4.whiley                BplErrors
MethodRef_Valid_1.whiley                 FullyVerified	      |	MethodRef_Valid_1.whiley                 BplErrors
MethodRef_Valid_2.whiley                 FullyVerified	      |	MethodRef_Valid_2.whiley                 BplErrors
OpenRecord_Valid_4.whiley                PartVerified	      |	OpenRecord_Valid_4.whiley                FullyVerified
OpenRecord_Valid_9.whiley                PartVerified	      |	OpenRecord_Valid_9.whiley                FullyVerified
Process_Valid_1.whiley                   PartVerified	      |	Process_Valid_1.whiley                   FullyVerified
Process_Valid_11.whiley                  PartVerified	      |	Process_Valid_11.whiley                  FullyVerified
Process_Valid_7.whiley                   FullyVerified	      |	Process_Valid_7.whiley                   PartVerified Boogie
Process_Valid_8.whiley                   FullyVerified	      |	Process_Valid_8.whiley                   PartVerified Boogie
Property_Valid_10.whiley                 PartVerified	      |	Property_Valid_10.whiley                 FullyVerified
Property_Valid_11.whiley                 PartVerified	      |	Property_Valid_11.whiley                 FullyVerified
Property_Valid_12.whiley                 PartVerified	      |	Property_Valid_12.whiley                 FullyVerified
Property_Valid_15.whiley                 PartVerified	      |	Property_Valid_15.whiley                 FullyVerified
Property_Valid_4.whiley                  PartVerified	      |	Property_Valid_4.whiley                  FullyVerified
Property_Valid_7.whiley                  FullyVerified	      |	Property_Valid_7.whiley                  PartVerified Boogie
Quantifiers_Valid_2.whiley               PartVerified	      |	Quantifiers_Valid_2.whiley               FullyVerified
Record_Valid_5.whiley                    FullyVerified	      |	Record_Valid_5.whiley                    Timeouts Boogie prog
RecursiveType_Valid_2.whiley             PartVerified	      |	RecursiveType_Valid_2.whiley             FullyVerified
RecursiveType_Valid_20.whiley            FullyVerified	      |	RecursiveType_Valid_20.whiley            PartVerified Boogie
RecursiveType_Valid_29.whiley            PartVerified	      |	RecursiveType_Valid_29.whiley            FullyVerified
RecursiveType_Valid_3.whiley             PartVerified	      |	RecursiveType_Valid_3.whiley             FullyVerified
RecursiveType_Valid_4.whiley             PartVerified	      |	RecursiveType_Valid_4.whiley             FullyVerified
Reference_Valid_1.whiley                 FullyVerified	      |	Reference_Valid_1.whiley                 PartVerified Boogie
Reference_Valid_2.whiley                 PartVerified	      |	Reference_Valid_2.whiley                 FullyVerified
Reference_Valid_3.whiley                 PartVerified	      |	Reference_Valid_3.whiley                 FullyVerified
Reference_Valid_9.whiley                 FullyVerified	      |	Reference_Valid_9.whiley                 PartVerified Boogie
Requires_Valid_2.whiley                  FullyVerified	      |	Requires_Valid_2.whiley                  PartVerified Boogie
String_Valid_4.whiley                    FullyVerified	      |	String_Valid_4.whiley                    BplErrors
String_Valid_6.whiley                    PartVerified	      |	String_Valid_6.whiley                    FullyVerified
Subtype_Valid_5.whiley                   PartVerified	      |	Subtype_Valid_5.whiley                   FullyVerified
Switch_Valid_5.whiley                    FullyVerified	      |	Switch_Valid_5.whiley                    BplErrors
Template_Valid_11.whiley                 PartVerified	      |	Template_Valid_11.whiley                 FullyVerified
Template_Valid_12.whiley                 PartVerified	      |	Template_Valid_12.whiley                 FullyVerified
Template_Valid_15.whiley                 PartVerified	      |	Template_Valid_15.whiley                 FullyVerified
Template_Valid_16.whiley                 PartVerified	      |	Template_Valid_16.whiley                 FullyVerified
Template_Valid_17.whiley                 PartVerified	      |	Template_Valid_17.whiley                 FullyVerified
Template_Valid_26.whiley                 PartVerified	      |	Template_Valid_26.whiley                 FullyVerified
Template_Valid_3.whiley                  PartVerified	      |	Template_Valid_3.whiley                  FullyVerified
Template_Valid_30.whiley                 PartVerified	      |	Template_Valid_30.whiley                 FullyVerified
Template_Valid_5.whiley                  PartVerified	      |	Template_Valid_5.whiley                  FullyVerified
TypeEquals_Valid_25.whiley               PartVerified	      |	TypeEquals_Valid_25.whiley               FullyVerified
TypeEquals_Valid_30.whiley               PartVerified	      |	TypeEquals_Valid_30.whiley               FullyVerified
TypeEquals_Valid_54.whiley               PartVerified	      |	TypeEquals_Valid_54.whiley               FullyVerified
While_Valid_11.whiley                    FullyVerified	      |	While_Valid_11.whiley                    PartVerified Boogie
While_Valid_15.whiley                    PartVerified	      |	While_Valid_15.whiley                    FullyVerified
While_Valid_20.whiley                    PartVerified	      |	While_Valid_20.whiley                    FullyVerified
While_Valid_23.whiley                    FullyVerified	      |	While_Valid_23.whiley                    PartVerified Boogie
While_Valid_24.whiley                    PartVerified	      |	While_Valid_24.whiley                    FullyVerified
While_Valid_26.whiley                    PartVerified	      |	While_Valid_26.whiley                    FullyVerified
While_Valid_27.whiley                    PartVerified	      |	While_Valid_27.whiley                    FullyVerified
While_Valid_32.whiley                    PartVerified	      |	While_Valid_32.whiley                    FullyVerified
While_Valid_34.whiley                    PartVerified	      |	While_Valid_34.whiley                    FullyVerified
While_Valid_35.whiley                    PartVerified	      |	While_Valid_35.whiley                    FullyVerified
While_Valid_37.whiley                    PartVerified	      |	While_Valid_37.whiley                    FullyVerified
While_Valid_42.whiley                    FullyVerified	      |	While_Valid_42.whiley                    BplErrors
While_Valid_5.whiley                     FullyVerified	      |	While_Valid_5.whiley                     PartVerified Boogie
While_Valid_59.whiley                    FullyVerified	      |	While_Valid_59.whiley                    PartVerified Boogie
While_Valid_60.whiley                    FullyVerified	      |	While_Valid_60.whiley                    PartVerified Boogie
While_Valid_61.whiley                    FullyVerified	      |	While_Valid_61.whiley                    PartVerified Boogie
While_Valid_62.whiley                    FullyVerified	      |	While_Valid_62.whiley                    PartVerified Boogie
While_Valid_68.whiley                    PartVerified	      |	While_Valid_68.whiley                    FullyVerified
While_Valid_69.whiley                    FullyVerified	      |	While_Valid_69.whiley                    PartVerified Boogie

WhileyVerifier	Boogie
--------------	------
FullyVerified	NotImplYet	14
PartVerified	FullyVerified	51
FullyVerified	FullyVerified	492
FullyVerified	Exception	2
PartVerified	Timeouts	1
FullyVerified	Timeouts	3
PartVerified	PartVerified	25
FullyVerified	PartVerified	24
PartVerified	NotImplYet	9
FullyVerified	BplErrors	10
Total	631



Invalid Tests that pass (2019-02-18)
====================================
# none of these should be 'FullyVerified'
$ grep Full OUT101_packages.results
Ensures_Invalid_1.whiley                 FullyVerified  TODO: prove that each function is feasible.
Export_Invalid_1.whiley                  FullyVerified  Why is this not valid?  Passes Whiley verifier.
StaticVar_Invalid_5.whiley               FullyVerified  TODO: prove that each constant satisfies the claimed type.
Type_Invalid_10.whiley                   FullyVerified  Circular types.  Compiler should detect this?
Type_Invalid_11.whiley                   FullyVerified  Why is this not valid?  Passes Whiley verifier.


Results 2019-01-22 (on MacBook Pro 2013)
==================
$ time wyboogie *.whiley >OUT100b.txt 2>&1
real	14m9.191s
user	18m21.203s
sys	1m51.504s
$ wystats OUT100d.txt  (modified to record 1/10 of %).
Error Compiling:          20 	3.2%
NotImplementedYet:        35 	5.7%
Other Exceptions:          2 	0.3%
Errors in BPL:            11 	1.8%
Fully Verified:          490 	80.3%
Verify time outs:          4 	0.6%
Verify errors:            48 	7.8%
Total:  610                  (sum is 99.7%)

The differences are that with the (guarded) array equality axiom:
* 9 partially verified test programs become fully verified.
* 1 timeout proof becomes provably true. (ConstrainedRecord_Valid_9.whiley)
* 1 timeout proof becomes provably false. (BoolList_Valid_3.whiley)
$ wydiff OUT100_no_array_eq_axiom.results OUT100.results
Array_Valid_7.whiley                     PartVerified Boogie  |	Array_Valid_7.whiley                     FullyVerified
Array_Valid_8.whiley                     PartVerified Boogie  |	Array_Valid_8.whiley                     FullyVerified
Assign_Valid_5.whiley                    PartVerified Boogie  |	Assign_Valid_5.whiley                    FullyVerified
BoolList_Valid_3.whiley                  PartVerified Boogie  |	BoolList_Valid_3.whiley                  PartVerified Boogie
ConstrainedList_Valid_26.whiley          PartVerified Boogie  |	ConstrainedList_Valid_26.whiley          FullyVerified
ConstrainedRecord_Valid_9.whiley         PartVerified Boogie  |	ConstrainedRecord_Valid_9.whiley         PartVerified Boogie
ListAssign_Valid_1.whiley                PartVerified Boogie  |	ListAssign_Valid_1.whiley                FullyVerified
ListAssign_Valid_6.whiley                PartVerified Boogie  |	ListAssign_Valid_6.whiley                FullyVerified
ListGenerator_Valid_12.whiley            PartVerified Boogie  |	ListGenerator_Valid_12.whiley            FullyVerified
Subtype_Valid_1.whiley                   PartVerified Boogie  |	Subtype_Valid_1.whiley                   FullyVerified
Subtype_Valid_7.whiley                   PartVerified Boogie  |	Subtype_Valid_7.whiley                   FullyVerified

And for tests/invalid:
$ wystats OUT100.txt
Error Compiling:         235 	64%
NotImplementedYet:         5 	1%
Other Exceptions:          9 	2%
Errors in BPL:            29 	7%
Fully Verified:            5 	1%
Verify time outs:          0 	0%
Verify errors:            84 	22%
Total:  367
Note: the 5 pass programs are mostly due to needing two-pass verification.

Results 2017-10-27
==================
Add support for Value.UTF8 (Strings) in createConst.
$ wystats OUT57_const_strings.txt
Error Compiling:          11
NotImplementedYet:        75
Other Exceptions:         49
Errors in BPL:            78
Fully Verified:          325
Verify time outs:          0
Verify errors:            51


Results 2017-10-26
==================
After API updates, and git update which added a few tests.
Also, implemented ==> and <==>.
$ wystats OUT56_assert_implies.txt
Error Compiling:          11
NotImplementedYet:       106
Other Exceptions:         48
Errors in BPL:            73
Fully Verified:          305
Verify time outs:          0
Verify errors:            46

Issue: RecursiveType_Valid_28
I don't think Line 26 (assert ls.next is Link)
is valid in general, without a much stronger recursive invariant
on List and LinkedList to relate their length to their non-nullness.


Results 2017-09-05
==================
Before new IL API update.  409/548 = 74.6%
$ wystats OUT52.txt
Error Compiling:          17
NotImplementedYet:        52
Other Exceptions:         22
Errors in BPL:            24
Fully Verified:          409
Verify time outs:          3
Verify errors:            21


Results 2017-03-23
==================
(OUT41_outer_method_calls.txt, in tests_david_2017_03_19/valid)
Total tests: 531 (tests/valid has only 514)

$ wystats OUT41_outer_method_calls.txt 
Error Compiling:          34
NotImplementedYet:        44
Other Exceptions:          2
Errors in BPL:            22
Fully Verified:          406
Verify time outs:          3
Verify errors:            28

Yay!  32 method-inside-expr errors went down to just 5!
MessageSend_Valid_3.whiley  requires unfolding method calls inside exprs. 
MessageSend_Valid_4.whiley  requires unfolding method calls inside exprs.
MethodCall_Valid_2.whiley requires unfolding method calls inside exprs.
MethodCall_Valid_3.whiley requires unfolding method calls inside exprs.
Process_Valid_6.whiley requires unfolding method calls inside exprs.


Results 2016-11-08
==================
Added array index checks.
$ wystats OUT32_array_checks.txt
Error Compiling:          21
NotImplementedYet:       132
Other Exceptions:          2
Errors in BPL:            12
Fully Verified:          325
Verify time outs:          3
Verify errors:            23

$ grep -i 'bpl.*error:' OUT32_array_checks.txt
DoWhile_Valid_6.bpl(24,39): error: ")" expected
RecursiveType_Valid_7.bpl(136,72): error: invalid Type
String_Valid_4.bpl(1,20): error: ")" expected
TypeEquals_Valid_35.bpl(28,10): Error: command assigns to an immutable variable: e
UnionType_Valid_15.bpl(7,265): Error: undeclared identifier: $dum
While_Valid_22.bpl(53,22): Error: undeclared identifier: j
While_Valid_22.bpl(53,34): Error: undeclared identifier: j
While_Valid_23.bpl(25,22): Error: undeclared identifier: j
While_Valid_23.bpl(25,34): Error: undeclared identifier: j
While_Valid_42.bpl(28,19): Error: more than one declaration of variable name: j
While_Valid_42.bpl(32,19): Error: more than one declaration of variable name: j
While_Valid_42.bpl(38,26): Error: more than one declaration of variable name: j

===================================
In tests/valid
===================================

ListAccess_Valid_1.whiley has a function with no return value?


Tests where Whiley verifier passes, but Boogie fails.

===== ConstrainedList_Valid_28.whiley =====
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
ConstrainedList_Valid_28.bpl(35,13): Error BP5003: A postcondition might not hold on this return path.
ConstrainedList_Valid_28.bpl(23,5): Related location: This is the postcondition that might not hold.
Execution trace:
    ConstrainedList_Valid_28.bpl(28,5): anon0
    ConstrainedList_Valid_28.bpl(32,14): anon5_Else
    ConstrainedList_Valid_28.bpl(34,15): anon6_Then
ConstrainedList_Valid_28.bpl(38,13): Error BP5003: A postcondition might not hold on this return path.
ConstrainedList_Valid_28.bpl(20,5): Related location: This is the postcondition that might not hold.
Execution trace:
    ConstrainedList_Valid_28.bpl(28,5): anon0
    ConstrainedList_Valid_28.bpl(32,14): anon5_Else
    ConstrainedList_Valid_28.bpl(37,15): anon6_Else
ConstrainedList_Valid_28.bpl(38,13): Error BP5003: A postcondition might not hold on this return path.
ConstrainedList_Valid_28.bpl(21,5): Related location: This is the postcondition that might not hold.
Execution trace:
    ConstrainedList_Valid_28.bpl(28,5): anon0
    ConstrainedList_Valid_28.bpl(32,14): anon5_Else
    ConstrainedList_Valid_28.bpl(37,15): anon6_Else
ConstrainedList_Valid_28.bpl(38,13): Error BP5003: A postcondition might not hold on this return path.
ConstrainedList_Valid_28.bpl(24,5): Related location: This is the postcondition that might not hold.
Execution trace:
    ConstrainedList_Valid_28.bpl(28,5): anon0
    ConstrainedList_Valid_28.bpl(32,14): anon5_Else
    ConstrainedList_Valid_28.bpl(37,15): anon6_Else

Boogie program verifier finished with 1 verified, 4 errors

NOTE: this is a recursive function call, so might require induction?
Whiley verifier does not verify this one either.


===== ConstrainedList_Valid_8.whiley =====
MUTATED INPUT list : ConstrainedList_Valid_8:nat[]
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
ConstrainedList_Valid_8.bpl(44,5): Error BP5001: This assertion might not hold.
Execution trace:
    ConstrainedList_Valid_8.bpl(41,8): anon0
ConstrainedList_Valid_8.bpl(46,5): Error BP5001: This assertion might not hold.
Execution trace:
    ConstrainedList_Valid_8.bpl(41,8): anon0
ConstrainedList_Valid_8.bpl(48,5): Error BP5001: This assertion might not hold.
Execution trace:
    ConstrainedList_Valid_8.bpl(41,8): anon0

Boogie program verifier finished with 1 verified, 3 errors

This modifies xs each time xs = update(xs, ..., ...) is called.
So the update function needs a postcondition to say that it
returns a list with the same length as the input list:

    ensures |out| == |list|:

With this added, all assertions verify.

===== DoWhile_Valid_6.whiley =====
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
DoWhile_Valid_6.bpl(25,9): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
    DoWhile_Valid_6.bpl(22,7): anon0

Boogie program verifier finished with 1 verified, 1 error

NOTE: Boogie is correct - i < |items| is not true initially.
My encoding of do-while loops breaks the loop invariant, in this case,
because it checks the invariant before the first iteration.
But shouldn't an invariant be true at the beginning and end of EVERY
iteration?  In that case, this loop invariant is incorrect.

7/2/2017 After fixing do-while translation to NOT check inv before first iteration:
  I cannot see why Boogie still cannot prove the invariants:
        assert toInt(i) >= - 1;
        assert toInt(i) < arraylen(items);
        
===== DoWhile_Valid_8.whiley =====
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
DoWhile_Valid_8.bpl(24,9): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
    DoWhile_Valid_8.bpl(21,7): anon0
DoWhile_Valid_8.bpl(24,9): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
    DoWhile_Valid_8.bpl(21,7): anon0
    DoWhile_Valid_8.bpl(23,5): anon5_LoopHead
    DoWhile_Valid_8.bpl(26,19): anon5_LoopBody
    DoWhile_Valid_8.bpl(27,9): anon6_Else

Boogie program verifier finished with 1 verified, 2 errors

NOTE: same issue.

===== Ensures_Valid_3.whiley =====
$ boogie wval.bpl Ensures_Valid_3.bpl 
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
Ensures_Valid_3.bpl(52,5): Error BP5003: A postcondition might not hold on this return path.
Ensures_Valid_3.bpl(18,5): Related location: This is the postcondition that might not hold.
Execution trace:
    Ensures_Valid_3.bpl(26,7): anon0
    Ensures_Valid_3.bpl(29,5): anon9_LoopHead
    Ensures_Valid_3.bpl(29,5): anon9_LoopDone
    Ensures_Valid_3.bpl(41,5): anon11_LoopHead
    Ensures_Valid_3.bpl(41,5): anon11_LoopDone

Boogie program verifier finished with 1 verified, 1 error

NOTE: this will require looking at the counter-example model.
Probably an array equality issue?
(My WVal theory needs stronger equality axioms for arrays)

===== Fail_Valid_1.whiley =====
$ boogie wval.bpl Fail_Valid_1.bpl 
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
Fail_Valid_1.bpl(34,13): Error BP5001: This assertion might not hold.
Execution trace:
    Fail_Valid_1.bpl(26,5): anon0
    Fail_Valid_1.bpl(30,9): anon5_Else
    Fail_Valid_1.bpl(34,13): anon6_Else

Boogie program verifier finished with 1 verified, 1 error

NOTE: here the test seems to be invalid?
Because fail will be reached when input x is null.
This test works if we change the 'fail' to:
        assert x is null
        return x

===== While_Valid_22.whiley =====
mangle max : function(int[])->(int) to max$2
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
While_Valid_22.bpl(54,9): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
    While_Valid_22.bpl(50,7): anon0
    While_Valid_22.bpl(52,5): anon3_LoopHead
    While_Valid_22.bpl(57,11): anon3_LoopBody
While_Valid_22.bpl(55,9): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
    While_Valid_22.bpl(50,7): anon0
    While_Valid_22.bpl(52,5): anon3_LoopHead
    While_Valid_22.bpl(57,11): anon3_LoopBody

Boogie program verifier finished with 2 verified, 2 errors

NOTE: probably an array equality issue.




OLDER RESULTS (before implementing equality fully)
===== Complex_Valid_2.whiley =====
Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
Complex_Valid_2.bpl(185,9): Error BP5003: A postcondition might not hold on this return path.
Complex_Valid_2.bpl(176,5): Related location: This is the postcondition that might not hold.
Execution trace:
    Complex_Valid_2.bpl(180,5): anon0
    Complex_Valid_2.bpl(181,13): anon11_Then
Boogie program verifier finished with 4 verified, 1 error

===== Complex_Valid_8.whiley =====
Boogie program verifier finished with 5 verified, 1 error

===== DoWhile_Valid_6.whiley =====
Boogie program verifier finished with 1 verified, 1 error

===== DoWhile_Valid_8.whiley =====
Boogie program verifier finished with 1 verified, 2 errors

===== Fail_Valid_1.whiley =====
Boogie program verifier finished with 1 verified, 1 error
  This is not valid, because when f(null) is called, the 'fail' is reachable.
  Boogie correctly detects this.

===== RecordAssign_Valid_6.whiley =====
Boogie program verifier finished with 0 verified, 1 error



====================================
Whiley Language Questions
====================================
1. What types can be compared using '==' and '!='?
    What types can be compared using '<', '<=' etc.?


{'fraction_non_alphanumeric': 0.07761683520087456, 'fraction_numerical': 0.052746652090735174, 'mean_word_length': 2.913458110516934, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 31, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 16, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4112583', 'n_tokens_mistral': 14969, 'n_tokens_neox': 13510, 'n_words': 3721}