search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

More Performance Problems with Type Checking #112

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

(This follows on from #110) There are still some performance problems with type checking. For example:

bash-3.2$ wy compile --verify --verbose --wyaldir=. BoolList_Valid_3.whiley 
WARNING: version numbering unavailable
Parsed 1 source file(s). ....................................................... [93ms+1mb]
Typed 1 source file(s). ....................................................... [174ms+1mb]
Generated code for 1 source file(s). ........................................... [84ms+1mb]
[/Users/djp/projects/WhileyTheoremProver/./BoolList_Valid_3.wyil] applied coercion check  [0ms]
Whiley => Wyil: compiled 1 file(s) ............................................ [368ms-2mb]
Wyil => Wyal: compiled 1 file(s) .............................................. [100ms+3mb]
Parsed 1 source file(s). ............................................................ [0ms]
Typed 1 source file(s). .................................................... [14612ms+24mb]
./BoolList_Valid_3.whiley:10: loop invariant not restored
        where all { k in 0..|board| | |board[k]| == |nboard[k]| }:
DavePearce commented 7 years ago

Another example:

bash-3.2$ wy compile --verify --verbose RecursiveType_Valid_2.whiley 
WARNING: version numbering unavailable
Parsed 1 source file(s). ....................................................... [40ms+1mb]
Typed 1 source file(s). ........................................................ [68ms+1mb]
Generated code for 1 source file(s). ........................................... [53ms+1mb]
[./RecursiveType_Valid_2.wyil] applied coercion check ............................... [0ms]
Whiley => Wyil: compiled 1 file(s) ............................................ [177ms-2mb]
Wyil => Wyal: compiled 1 file(s) ............................................... [48ms+1mb]
Parsed 1 source file(s). ............................................................ [0ms]
Typed 1 source file(s). ..................................................... [6806ms+20mb]
Verified 1 source file(s). ................................................... [1844ms+1mb]
Generated code for 1 source file(s). ................................................ [0ms]
Wyal => Wyail: compiled 1 file(s) ........................................... [8651ms+21mb]