Update to use conditional elaboration

[clayrat]

Update to use ucsd-progsys/liquid-fixpoint#734

Some caveats:

• pos/Maps and ple/pos/PolySetBar tests had to be disabled globally because they don't work with the combination of corrected theory sort signatures (ucsd-progsys/liquid-fixpoint@55211d9) and commit fac8f57. The solution to getting them working is most likely to implement the dynamic apply generation.
• benchmark-bytestring/Data/ByteString/Lazy and ple/pos/Permutations additionally have to be disabled when running the test suite with CVC5.

[clayrat]

[clayrat]

The performance charts were created before rebasing on top of #2482, so the discrepancy may be more pronounced than it really is. I will refresh them in a couple of hours.

[clayrat]

[nikivazou]

Great!!!!!! Are there tests running with cvc5? I am curious how the time compares between cvc5 and z3 :)

[clayrat]

The situtation with LH tests on CVC5 is not very straightforward, unfortunately. There are two issues at the moment:

• The PolySetBar test in the ple-pos group fails with an unknown func-sort error similar to PLE generates polymorphic applys for Sets #2438 (I am debugging this now)
• Some of the tests in the benchmark-bytestring group seem to trigger some pathological behaviour in cvc5, where the solver is left running at 100% CPU for several hours until the smtlib-backends-process API crashes with an Data.ByteString.hGetLine: end of file error.

If I exclude these two test groups, the performance seems comparable to Z3.

[clayrat]

Here are performance diffs comparing the CVC5 run excluding ple-pos and benchmark-bytestring (after) against the Z3 run (before). Both runs are done on the latest commit in this PR, i.e. d5aa806):

[clayrat]

A combination of the latest LF changes and fac8f57 causes the current breakage of tests. Previously we've had an incorrect definition of sort signatures (missing a type abstraction prefix) for elaborated set and bag operations in LF, which caused the apply machinery to always generate additional applys for Array @0 Bool and Array @0 Int. The tests still work with these fixed signatures on commits before fac8f57, but are broken after.

Looking at the commit, it seems the removal of giUseVars might be the underlying cause? @facundominguez

[clayrat]

Changing https://github.com/ucsd-progsys/liquidhaskell/blob/develop/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Qualifier.hs#L99 to

`x `S.member` (S.difference (S.fromList (giUseVars (giSrc info))) (S.fromList (specAxiomVars info)))

indeed fixes the broken https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/pos/Maps.hs but breaks the newly introduced https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/pos/Meas12.hs instead.

[facundominguez]

Looking at the commit, it seems the removal of giUseVars might be the underlying cause?

Hard to say without knowing why you would need to filter qualifiers with giUseVars.

To start somewhere, tests/pos/Maps.hs and tests/pos/Meas12.hs are passing in develop. Could you maybe describe in some detail how they are affected by this PR?

[clayrat]

The PR (or rather the underlying ucsd-progsys/liquid-fixpoint#734) introduces many changes, but the relevant change here is in https://github.com/clayrat/liquid-fixpoint/blob/cvc5-theories/src/Language/Fixpoint/Smt/Theories.hs#L495-L509:

-  , interpSym arrMapNotS "(_ map not)" (FFunc setArrSort setArrSort)
-  , interpSym arrMapOrS  "(_ map or)"  (FFunc setArrSort $ FFunc setArrSort setArrSort)
-  , interpSym arrMapAndS "(_ map and)" (FFunc setArrSort $ FFunc setArrSort setArrSort)
-  , interpSym arrMapImpS "(_ map =>)"  (FFunc setArrSort $ FFunc setArrSort setArrSort)
+  , interpSym arrMapNotS "(_ map not)" (FAbs 0 $ FFunc setArrSort setArrSort)
+  , interpSym arrMapOrS  "(_ map or)"  (FAbs 0 $ FFunc setArrSort $ FFunc setArrSort setArrSort)
+  , interpSym arrMapAndS "(_ map and)" (FAbs 0 $ FFunc setArrSort $ FFunc setArrSort setArrSort)
+  , interpSym arrMapImpS "(_ map =>)"  (FAbs 0 $ FFunc setArrSort $ FFunc setArrSort setArrSort)

....
-  , interpSym arrMapPlusB "(_ map (+ (Int Int) Int))"        (FFunc bagArrSort $ FFunc bagArrSort bagArrSort)
-  , interpSym arrMapLeB   "(_ map (<= (Int Int) Bool))"      (FFunc bagArrSort $ FFunc bagArrSort setArrSort)
-  , interpSym arrMapGtB   "(_ map (> (Int Int) Bool))"       (FFunc bagArrSort $ FFunc bagArrSort setArrSort)
-  , interpSym arrMapIteB  "(_ map (ite (Bool Int Int) Int))" (FFunc setArrSort $ FFunc bagArrSort $ FFunc bagArrSort bagArrSort)
+  , interpSym arrMapPlusB "(_ map (+ (Int Int) Int))"        (FAbs 0 $ FFunc bagArrSort $ FFunc bagArrSort bagArrSort)
+  , interpSym arrMapLeB   "(_ map (<= (Int Int) Bool))"      (FAbs 0 $ FFunc bagArrSort $ FFunc bagArrSort setArrSort)
+  , interpSym arrMapGtB   "(_ map (> (Int Int) Bool))"       (FAbs 0 $ FFunc bagArrSort $ FFunc bagArrSort setArrSort)
+  , interpSym arrMapIteB  "(_ map (ite (Bool Int Int) Int))" (FAbs 0 $ FFunc setArrSort $ FFunc bagArrSort $ FFunc bagArrSort bagArrSort)

Adding the extra outer type abstraction (FAbs 0) hides the FFunc which has the effect that applySorts no longer uses these signatures for populating the apply-sorts table by default. This is theoretically an improvement, as the size of that table reduces, however this unmasks the fact that there are some situations where the apply-sorts table has erroneously missing entries, as first noted in #2438. The commit fac8f57 apparently introduces another such situation, with the apply-sorts table missing an entry for Array Int Int (which is an LF/SMT elaboration target sort for Haskell Map), resulting in the following error on https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/pos/Maps.hs:

Unknown func-sort: (SArray SInt SInt,SInt) for (apply : func(0 , [(Array_t int int);
                       int])) (GHC.Types_LHAssumptions.len : func(0 , [(Array_t int int);
                                                                       int])) (Maps.emp : (Array_t int int))

[clayrat]

One potential workaround for this problem is to force funcSorts to generate all possible instantiations for Maps as well (the erroneous signatures existing before effectively already caused it to generate all possible instantiations for Sets and Bags), however this solution causes a significant performance degradation (most likely by blowing up the appy-sorts table size exponentially), as seen on this chart:

[facundominguez]

Only for my enlightenment, what do you think a well designed fix would be?

[clayrat]

I think the proper way forward would be to try and implement dynamic apply generation, as described in this comment: https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/src/Language/Fixpoint/Types/Theories.hs#L116-L137 This would get rid of the pregenerated apply-sort table and the problems it causes.

However, this change seems non-trivial and could take a while, in the meantime we could restore the filtering on giUseVars (and demote Meas12 back to a negative test), and then flip everything back when the dynamic solution is implemented (assuming no additional complications arise).

[facundominguez]

I'm not acquainted with the sort generation at play in the PR, but AFAIU allowing for more qualifiers, as in fac8f57, is requiring more sorts to make those qualifiers well-sorted.

What the proposed workaround achieves is to make the existing tests pass, while (I sense) other tests could be written that would also make verification crash because of missing sorts. Is this really the case?

If so we might just disable the failing test, and document the limitation in terms that users can understand, since adding giUseVars makes the code more involved without really solving the problem. But I'm happy to discuss it more, or to be corrected :)

[clayrat]

Ok, I've disabled pos/Maps and ple/pos/PolySetBar tests, here are the performance charts for Z3:

[clayrat]

For CVC5 I've additionally had to disable benchmark-bytestring/Data/ByteString/Lazy and ple/pos/Permutations tests, as these ultimately are the two triggering some pathological behaviour in the CVC5 solver itself, making it either loop forever, or run for a very long time. The comparison here is against the Z3 run, not develop:

[clayrat]

Updated to latest LF version and merged with develop

[ranjitjhala]

Btw, @clayrat -- re hanging with CVC5 -- the .liquid directory has the generated .smt2 file, which you can run directly on cvc5 (or z3 as the case may be). Did you confirm that running cvc5 directly on the file makes it hang? If so, often I've found it useful to file an issue with the relevant solver as they are then able to fix whatever the problem was...

[clayrat]

Btw, @clayrat -- re hanging with CVC5 -- the .liquid directory has the generated .smt2 file, which you can run directly on cvc5 (or z3 as the case may be). Did you confirm that running cvc5 directly on the file makes it hang? If so, often I've found it useful to file an issue with the relevant solver as they are then able to fix whatever the problem was...

Yes, that's exactly what I'm doing now, I've even located the specific statement that's causing it to hang. The problem is that this happens near the end of a ~40 Mb file that LF generates, so I'm trying to figure out if there's any way to minimize it before trying to submit. However, doing so seems to change where the hanging happens :)