diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,30 @@ ## Next +## 0.9.12.2.1 (2026-01-14) + +- Disable LH when collecting Haddock comments and the noBackend is set [#2611](https:://github.com/ucsd-progsys/liquidhaskell/pull/2611) +- Make assume reflect error sensitive to dflags [#2607](https:://github.com/ucsd-progsys/liquidhaskell/pull/2607) +- Add a flag to dump the a-normalized core [#2605](https:://github.com/ucsd-progsys/liquidhaskell/pull/2605) +- Show solutions of non-cut kvars in error messages [#2596](https:://github.com/ucsd-progsys/liquidhaskell/pull/2596) +- Remove question marks as a distinction of predicates from other expressions [#2595](https:://github.com/ucsd-progsys/liquidhaskell/pull/2595) +- Require braces when declaring qualifier [#2594](https:://github.com/ucsd-progsys/liquidhaskell/pull/2594) +- Retire implementation of gradual refinement types [#2588](https:://github.com/ucsd-progsys/liquidhaskell/pull/2588) +- Remove old versions of PLE [#2587](https:://github.com/ucsd-progsys/liquidhaskell/pull/2587) +- Add new syntax for indexed types (Ix instead of Prop) [#2586](https:://github.com/ucsd-progsys/liquidhaskell/pull/2586) +- Handle `ByteArray#` as int in the logic [#2581](https:://github.com/ucsd-progsys/liquidhaskell/pull/2581) +- Do not ignore user qualifiers when using `--reflection` [#2580](https:://github.com/ucsd-progsys/liquidhaskell/pull/2580) +- Add set cardinality support when using cvc5 [#2577](https:://github.com/ucsd-progsys/liquidhaskell/pull/2577) +- Support the finite field theory when using cvc5 [#2571](https:://github.com/ucsd-progsys/liquidhaskell/pull/2571) [#2614](https:://github.com/ucsd-progsys/liquidhaskell/pull/2614) +- Allow to qualify predicate aliases [#2566](https:://github.com/ucsd-progsys/liquidhaskell/pull/2566) +- Implement stratified types [#2559](https:://github.com/ucsd-progsys/liquidhaskell/pull/2559) +- Resolve occurrences of imported opaquely-reflected functions [#2548](https:://github.com/ucsd-progsys/liquidhaskell/pull/2548) +- Allow to qualify type aliases [#2550](https:://github.com/ucsd-progsys/liquidhaskell/pull/2550) +- Print the amount of checked constraints when verification fails [#2545](https:://github.com/ucsd-progsys/liquidhaskell/pull/2545) +- Fix SMT crashes on reflected functions on polymorphic data types [#2542](https://github.com/ucsd-progsys/liquidhaskell/pull/2542) +- Look for cvc5 before cvc4 [#2513](https://github.com/ucsd-progsys/liquidhaskell/pull/2513) +- Change `--cores` default to 1 [#2564](https://github.com/ucsd-progsys/liquidhaskell/pull/2564) + ## 0.9.12.2 (2025-03-22) - Simplify kvar solutions in fqout files [liquid-fixpoint#741](https://github.com/ucsd-progsys/liquid-fixpoint/pull/741). diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -7,6 +7,41 @@ If you're a LiquidHaskell **user** (or just curious), you probably want to go to [the documentation website](https://ucsd-progsys.github.io/liquidhaskell/) instead. +## Trying it from Hackage + +Assuming the [Z3](https://github.com/Z3Prover/z3) SMT solver is installed and +available in your `PATH`, you can run + +``` +cabal install --lib liquidhaskell liquid-prelude liquid-vector --package-env . --force-reinstalls +ghc -fplugin=LiquidHaskell FILE.hs +``` + +`--package-env .` creates a `.ghc.environment*` file in the current folder that makes +`ghc` find the `LiquidHaskell` plugin only when invoking it from there. +Otherwise, global user configuration would be affected. + +Note that the installation step is influenced by the dependencies that are +already installed in your system, so different results may be obtained by +different users. + +## Trying it from GitHub + +The github repo only builds with GHC 9.12.2, which must be in your `PATH`. + +``` +git clone https://github.com/ucsd-progsys/liquidhaskell.git +cd liquidhaskell +git submodule update --init +cabal build liquidhaskell liquid-prelude liquid-vector + +cabal exec -- ghc -fplugin=LiquidHaskell FILE.hs +``` + +## Asking for Help + +If you have questions or you just need help, you can always reach out on our [slack channel](https://join.slack.com/t/liquidhaskell/shared_invite/enQtMjY4MTk3NDkwODE3LTFmZGFkNGEzYWRkNDJmZDQ0ZGU1MzBiZWZiZDhhNmY3YTJiMjUzYTRlNjMyZDk1NDU3ZGIxYzhlOTIzN2UxNWE), [google groups mailing list](https://groups.google.com/forum/#!forum/liquidhaskell), [GitHub issue tracker](https://github.com/ucsd-progsys/liquidhaskell/issues), or by emailing [Ranjit Jhala](https://github.com/ranjitjhala), [Niki Vazou](https://github.com/nikivazou). + # Contributing This is an open-source project, and we love getting feedback (and patches)! @@ -36,30 +71,11 @@ Pull requests don't just have to be about code: documentation can often be improved too! -## Ask for Help - -If you have further questions or you just need help, you can always reach out on our [slack channel](https://join.slack.com/t/liquidhaskell/shared_invite/enQtMjY4MTk3NDkwODE3LTFmZGFkNGEzYWRkNDJmZDQ0ZGU1MzBiZWZiZDhhNmY3YTJiMjUzYTRlNjMyZDk1NDU3ZGIxYzhlOTIzN2UxNWE), [google groups mailing list](https://groups.google.com/forum/#!forum/liquidhaskell), [GitHub issue tracker](https://github.com/ucsd-progsys/liquidhaskell/issues), or by emailing [Ranjit Jhala](https://github.com/ranjitjhala), [Niki Vazou](https://github.com/nikivazou). - # General Development Guide For those diving into the implementation of LiquidHaskell, here are a few tips: -## Running the pluging on individual files - -``` -cabal build liquidhaskell -cabal exec ghc -- -fplugin=LiquidHaskell FILE.hs -``` - -## Building - -### Cabal - -``` -cabal build -``` - -### Faster recompilation +## Faster recompilation When changing the `liquidhaskell-boot` library, sometimes we don't want to rebuild `liquidhaskell` or `liquid-vector` when testing the changes. @@ -114,6 +130,15 @@ ## How to create performance comparison charts +Firstly, make sure to remove previous compilation artifacts of tests before measuring performance, +or GHC will skip running Liquid Haskell on modules that don't need recompilation. Unfortunately, +using `-fforce-recomp` is not ideal (see [#2565](https://github.com/ucsd-progsys/liquidhaskell/pull/2565) +for more details). At the time of writing, previous compilation artifacts of tests can be removed with + +```bash +find dist-newstyle -name "tests-*" -o -name "prover-ple-lib-*" | xargs rm -r +``` + When `liquidhaskell` tests run, we can collect timing information with $ ./scripts/test/test_plugin.sh --measure-timings @@ -128,21 +153,26 @@ which will produce `tmp/*.json` files. -Then a csv report can be generated from this json files with +Then a csv report can be generated from the json files with ``` -cabal v2-run benchmark-timings -- tmp/*.json --phase LiquidHaskell -o summary.csv +cabal v2-run benchmark-timings -- tmp/*.json --phase LiquidHaskellCPU -o summary.csv ``` -On each line, the report will contain the time taken by each test. +On each line, the report will contain the the wall-clock time taken by each test. +Use `--phase LiquidHaskell` to get the wall-clock time instead. Although in that +case you need to use the `--measure-timings-j1` option when running the tests, +which validates modules one at a time. Comparison charts in `svg` format can be generated by invoking ``` -cabal v2-run plot-performance -- -b path_to_before_summary.csv -a path_to_after_summary.csv -s 50 -f "benchmark" +cabal v2-run plot-performance -- -b path_to_before_summary.csv -a path_to_after_summary.csv -s 50 ``` -This will generate three files `filtered.svg` (a subset of tests with a `benchmark` prefix, enabled by the `-f` option), -`top.svg` and `bot.svg` (top 50 speedups and slowdowns over the entire test set, both enabled by the `-s` option) in the -current directory. The `-f` and `-s` options can be used/omitted independently. If both are omitted, a single `perf.svg` +This will generate two files `top.svg` and `bot.svg` containing the top 50 speedups and slowdowns +over the entire test set, both enabled by the `-s` option) in the current directory. Alternatively, +a subset of the tests can be selected by a prefix of their names with `-f `, for instance +`-f benchmarks`. `-f` will generate a file `filtered.svg` containing the comparisons of the selected tests. +The `-f` and `-s` options can be used/omitted independently. If both are omitted, a single `perf.svg` will be produced covering the full input test set. Additionally, their effects can be combined by providing a third `-c` option (this will produce 2 files `filtered-top.svg` and `filtered-bot.svg` instead of 3). An optional key `-o` can be supplied to specify an output directory for the generated files. @@ -315,3 +345,51 @@ [processTargetModule]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L483 [processModule]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L509 +# Module Verification Process + +The following graph summarizes the verification process of a module by showing +its specification life cycle. +See [Specs.hs](./liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs) +for detailed documentation on the specification stages. +There are many moving parts hidden within each graph link, +but some places worth noticing here are +[Liquid.hs](./liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs) +—which implements constraint generation— and +[SpecFinder.hs](./liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs) +—that deals with the gathering of dependencies and `LHAssumptions`—. + +```mermaid +flowchart LR + subgraph Liquid Haskell + + subgraph Inputs + direction TB + LiftedDeps[ + Dependencies of A + LifttedSpecs + ] + CoreBinds[CoreBinds] + Bare[BarseSpec] + end + + subgraph Outputs + direction TB + T[TargetSpec] --> Constraints[Verification + Constraints] + L[LiftedSpec] + end + + Inputs --> Outputs + + end + + A>DepsOfA_LHAssumptions] --> LiftedDeps + Deps>DepsOfA.hi] --> LiftedDeps + Mod(A.hs) --> CoreBinds & Bare + Constraints -->|checked by| fixpoint([liquid-fixpoint]) + L ---> |if verified: + serialize| File>A.hi] +``` + +Reference: +[Implementing a GHC Plugin for Liquid Haskell](https://well-typed.com/blog/2020/08/implementing-a-ghc-plugin-for-liquid-haskell/). diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell -version: 0.9.12.2 +version: 0.9.12.2.1 synopsis: Liquid Types for Haskell description: Liquid Types for Haskell. license: BSD-3-Clause @@ -37,6 +37,7 @@ Data.Bits_LHAssumptions Data.Either_LHAssumptions Data.Foldable_LHAssumptions + Data.Int_LHAssumptions Data.List_LHAssumptions Data.Maybe_LHAssumptions Data.String_LHAssumptions @@ -78,7 +79,7 @@ hs-source-dirs: src build-depends: base >= 4.11.1.0 && < 5, - liquidhaskell-boot == 0.9.12.2, + liquidhaskell-boot == 0.9.12.2.1, bytestring, containers, ghc-prim @@ -87,3 +88,4 @@ if flag(devel) ghc-options: -Werror + diff --git a/src/Data/Int_LHAssumptions.hs b/src/Data/Int_LHAssumptions.hs new file mode 100644 --- /dev/null +++ b/src/Data/Int_LHAssumptions.hs @@ -0,0 +1,4 @@ +{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +module Data.Int_LHAssumptions where + +import GHC.Int_LHAssumptions() diff --git a/src/Data/Set_LHAssumptions.hs b/src/Data/Set_LHAssumptions.hs --- a/src/Data/Set_LHAssumptions.hs +++ b/src/Data/Set_LHAssumptions.hs @@ -3,7 +3,6 @@ module Data.Set_LHAssumptions where import Data.Set -import Data.Set.Internal as I import GHC.Types_LHAssumptions() import Prelude hiding (null) @@ -18,6 +17,7 @@ assume isSubsetOf :: (Ord a) => x:(Set a) -> y:(Set a) -> {v:Bool | v <=> Set_sub x y} assume member :: Ord a => x:a -> xs:(Set a) -> {v:Bool | v <=> Set_mem x xs} assume null :: Ord a => xs:(Set a) -> {v:Bool | v <=> Set_emp xs} +assume size :: xs:(Set a) -> {v:Nat | v = Set_card xs} assume empty :: {v:(Set a) | Set_emp v} assume singleton :: x:a -> {v:(Set a) | v = (Set_sng x)} @@ -45,18 +45,9 @@ define difference x y = (Set_dif x y) define empty = (Set_empty 0) define null x = (Set_emp x) +define size x = (Set_card x) define member x xs = (Set_mem x xs) define isSubsetOf x y = (Set_sub x y) define fromList xs = (Data.Set_LHAssumptions.listElts xs) - -define I.singleton x = (Set_sng x) -define I.union x y = (Set_cup x y) -define I.intersection x y = (Set_cap x y) -define I.difference x y = (Set_dif x y) -define I.empty = (Set_empty 0) -define I.null x = (Set_emp x) -define I.member x xs = (Set_mem x xs) -define I.isSubsetOf x y = (Set_sub x y) -define I.fromList xs = (Data.Set_LHAssumptions.listElts xs) @-} diff --git a/src/Data/Tuple_LHAssumptions.hs b/src/Data/Tuple_LHAssumptions.hs --- a/src/Data/Tuple_LHAssumptions.hs +++ b/src/Data/Tuple_LHAssumptions.hs @@ -14,6 +14,6 @@ measure snd :: (a, b) -> b snd (a, b) = b -qualif Fst(__v:a, __y:b): (__v = (fst __y)) -qualif Snd(__v:a, __y:b): (__v = (snd __y)) +qualif Fst(__v:a, __y:b) { __v = (fst __y) } +qualif Snd(__v:a, __y:b) { __v = (snd __y) } @-} diff --git a/src/GHC/Base_LHAssumptions.hs b/src/GHC/Base_LHAssumptions.hs --- a/src/GHC/Base_LHAssumptions.hs +++ b/src/GHC/Base_LHAssumptions.hs @@ -41,24 +41,24 @@ assume id :: x:a -> {v:a | v = x} -qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs > 0)) -qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs = 0)) +qualif IsEmp(v:Bool, xs: [a]) { v <=> (len xs > 0) } +qualif IsEmp(v:Bool, xs: [a]) { v <=> (len xs = 0) } -qualif ListZ(v: [a]) : (len v = 0) -qualif ListZ(v: [a]) : (len v >= 0) -qualif ListZ(v: [a]) : (len v > 0) +qualif ListZ(v: [a]) { len v = 0 } +qualif ListZ(v: [a]) { len v >= 0 } +qualif ListZ(v: [a]) { len v > 0 } -qualif CmpLen(v:[a], xs:[b]) : (len v = len xs ) -qualif CmpLen(v:[a], xs:[b]) : (len v >= len xs ) -qualif CmpLen(v:[a], xs:[b]) : (len v > len xs ) -qualif CmpLen(v:[a], xs:[b]) : (len v <= len xs ) -qualif CmpLen(v:[a], xs:[b]) : (len v < len xs ) +qualif CmpLen(v:[a], xs:[b]) { len v = len xs } +qualif CmpLen(v:[a], xs:[b]) { len v >= len xs } +qualif CmpLen(v:[a], xs:[b]) { len v > len xs } +qualif CmpLen(v:[a], xs:[b]) { len v <= len xs } +qualif CmpLen(v:[a], xs:[b]) { len v < len xs } -qualif EqLen(v:int, xs: [a]) : (v = len xs ) -qualif LenEq(v:[a], x: int) : (x = len v ) +qualif EqLen(v:int, xs: [a]) { v = len xs } +qualif LenEq(v:[a], x: int) { x = len v } -qualif LenDiff(v:[a], x:int) : (len v = x + 1) -qualif LenDiff(v:[a], x:int) : (len v = x - 1) -qualif LenAcc(v:int, xs:[a], n: int): (v = len xs + n) +qualif LenDiff(v:[a], x:int) { len v = x + 1 } +qualif LenDiff(v:[a], x:int) { len v = x - 1 } +qualif LenAcc(v:int, xs:[a], n: int) { v = len xs + n } @-} diff --git a/src/GHC/List_LHAssumptions.hs b/src/GHC/List_LHAssumptions.hs --- a/src/GHC/List_LHAssumptions.hs +++ b/src/GHC/List_LHAssumptions.hs @@ -52,8 +52,8 @@ assume reverse :: xs:[a] -> {v: [a] | len(v) = len(xs)} // Copy-pasted from len.hquals -qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys])) -qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys])) +qualif LenSum(v:[a], xs:[b], ys:[c]) { len([v]) = (len([xs]) + len([ys])) } +qualif LenSum(v:[a], xs:[b], ys:[c]) { len([v]) = (len([xs]) - len([ys])) } assume !! :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a diff --git a/src/GHC/Num/Integer_LHAssumptions.hs b/src/GHC/Num/Integer_LHAssumptions.hs --- a/src/GHC/Num/Integer_LHAssumptions.hs +++ b/src/GHC/Num/Integer_LHAssumptions.hs @@ -10,5 +10,7 @@ {-@ assume GHC.Num.Integer.IS :: x:Int# -> {v: Integer | v = (x :: int) } +define GHC.Num.Integer.IS x = (x) + embed Integer as int @-} diff --git a/src/GHC/Num_LHAssumptions.hs b/src/GHC/Num_LHAssumptions.hs --- a/src/GHC/Num_LHAssumptions.hs +++ b/src/GHC/Num_LHAssumptions.hs @@ -14,6 +14,8 @@ assume abs :: (Num a) => x:a -> {y:a | (x >= 0 ==> y = x) && (x < 0 ==> y = -x) } +define abs x = if x >=0 then x else -x + assume + :: x:a -> y:a -> {v:a | v = x + y } assume - :: (Num a) => x:a -> y:a -> {v:a | v = x - y } @-} diff --git a/src/GHC/Real_LHAssumptions.hs b/src/GHC/Real_LHAssumptions.hs --- a/src/GHC/Real_LHAssumptions.hs +++ b/src/GHC/Real_LHAssumptions.hs @@ -5,6 +5,7 @@ import GHC.Real import GHC.Types_LHAssumptions() +import GHC.Num_LHAssumptions() {-@ assume (^) :: x:a -> y:{n:b | n >= 0} -> {z:a | (y == 0 => z == 1) && ((x == 0 && y /= 0) <=> z == 0)} @@ -49,6 +50,12 @@ define div x y = (x / y) define mod x y = (x mod y) +define quot x y = if x >= 0 + then (if y >= 0 then x / y else -(x / -y)) + else -(-x / y) +define rem x y = if x >= 0 + then (if y >= 0 then x mod y else x mod -y) + else - (-x mod y) define fromIntegral x = (x) @-} diff --git a/src/GHC/Types_LHAssumptions.hs b/src/GHC/Types_LHAssumptions.hs --- a/src/GHC/Types_LHAssumptions.hs +++ b/src/GHC/Types_LHAssumptions.hs @@ -26,6 +26,7 @@ embed Char as Char embed Char# as Char embed Addr# as Str +embed ByteArray# as int embed Integer as int diff --git a/src/Prelude_LHAssumptions.hs b/src/Prelude_LHAssumptions.hs --- a/src/Prelude_LHAssumptions.hs +++ b/src/Prelude_LHAssumptions.hs @@ -25,38 +25,38 @@ // BOT: Do not delete EVER! -qualif Bot(v:@(0)) : (0 = 1) -qualif Bot(v:obj) : (0 = 1) -qualif Bot(v:a) : (0 = 1) -qualif Bot(v:bool) : (0 = 1) -qualif Bot(v:int) : (0 = 1) +qualif Bot(v:@(0)) { 0 = 1 } +qualif Bot(v:obj) { 0 = 1 } +qualif Bot(v:a) { 0 = 1 } +qualif Bot(v:bool) { 0 = 1 } +qualif Bot(v:int) { 0 = 1 } -qualif CmpZ(v:a) : (v < 0) -qualif CmpZ(v:a) : (v <= 0) -qualif CmpZ(v:a) : (v > 0) -qualif CmpZ(v:a) : (v >= 0) -qualif CmpZ(v:a) : (v = 0) -qualif CmpZ(v:a) : (v != 0) +qualif CmpZ(v:a) { v < 0 } +qualif CmpZ(v:a) { v <= 0 } +qualif CmpZ(v:a) { v > 0 } +qualif CmpZ(v:a) { v >= 0 } +qualif CmpZ(v:a) { v = 0 } +qualif CmpZ(v:a) { v != 0 } -qualif Cmp(v:a, x:a) : (v < x) -qualif Cmp(v:a, x:a) : (v <= x) -qualif Cmp(v:a, x:a) : (v > x) -qualif Cmp(v:a, x:a) : (v >= x) -qualif Cmp(v:a, x:a) : (v = x) -qualif Cmp(v:a, x:a) : (v != x) +qualif Cmp(v:a, x:a) { v < x } +qualif Cmp(v:a, x:a) { v <= x } +qualif Cmp(v:a, x:a) { v > x } +qualif Cmp(v:a, x:a) { v >= x } +qualif Cmp(v:a, x:a) { v = x } +qualif Cmp(v:a, x:a) { v != x } -qualif One(v:int) : v = 1 -qualif True1(v:Bool) : (v) -qualif False1(v:Bool) : (~ v) +qualif One(v:int) { v = 1 } +qualif True1(v:Bool) { v } +qualif False1(v:Bool) { ~ v } // REBARE constant papp1 : func(1, [Pred @(0); @(0); bool]) -qualif Papp(v:a, p:Pred a) : (papp1 p v) +qualif Papp(v:a, p:Pred a) { papp1 p v } // REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool]) -qualif Papp2(v:a, x:b, p:Pred a b) : (papp2 p v x) +qualif Papp2(v:a, x:b, p:Pred a b) { papp2 p v x } // REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool]) -qualif Papp3(v:a, x:b, y:c, p:Pred a b c) : (papp3 p v x y) +qualif Papp3(v:a, x:b, y:c, p:Pred a b c) { papp3 p v x y } // qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z) // REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])