search

ranjitjhala / sprite-lang

An tutorial-style implementation of liquid/refinement types for a subset of Ocaml/Reason.
BSD 3-Clause "New" or "Revised" License
140 stars 13 forks source link

how can I see the "SMTLIB" queries generated to solve the horn constraints? #8

Open jwaldmann opened 8 months ago

jwaldmann commented 8 months ago

re: https://github.com/ucsd-progsys/liquidhaskell/issues/2259#issuecomment-1910336174

I am doing

$ cabal run  -w /opt/ghc/ghc-9.4.7/bin/ghc sprite -- 1 test/L1/pos/inc02.re

the file that gets written, has extension .smt2 but the contents is not?

(constraint
 (and
  (forall ((x int) (true))
   (and
    (and
     (and
      (and)
      (forall ((VV int) (true))
       ((true))))
     (forall ((VV int) (VV == 1))
...

in the sense of

$ z3 test/L1/pos/.liquid/inc02.re.smt2
unsupported
; constraint line: 43 position: 17
shingarov commented 8 months ago

has extension .smt2 but the contents is not?

These are the VCs passed down to liquid-fixpoint. One way to investigate what happens further down the pipeline, is to clone and build https://github.com/ucsd-progsys/liquid-fixpoint and then run fixpoint manually on those inc02.re.smt2 VCs with the "save" option. Well, at least that's what I do and it has worked for me.

Beware, though, that in a few places Sprite will save slighly-broken .smt2 VCs and fixpoint complains at them. I fixed some of those places in the past but I vaguely recall there were a couple of other places, I don't remember what happened to those.

jwaldmann commented 8 months ago

ah, that works. So, I add the second command:

$ cabal run  -w /opt/ghc/ghc-9.4.7/bin/ghc sprite -- 1 test/L1/pos/inc00.re
$ fixpoint  test/L1/pos/.liquid/inc00.re.smt2  --save
-- start of file that was produced:
$ head test/L1/pos/.liquid/inc00.re.smt2.smt2 
(declare-fun x () Int)
(declare-fun v () Int)
(declare-fun cast_as_int () Int)
(declare-fun cast_as () Int)
(declare-fun v$35$$35$3 () Int)
(declare-fun apply$35$$35$15 (Int (_ BitVec 32)) Int)
...

this is still not stand-alone SMTLIB? E.g.,

$ cvc5 test/L1/pos/.liquid/inc00.re.smt2.smt2 
test/L1/pos/.liquid/inc00.re.smt2.smt2:1.11: No set-logic command was given before this point.
test/L1/pos/.liquid/inc00.re.smt2.smt2:1.11: cvc5 will make all theories available.
test/L1/pos/.liquid/inc00.re.smt2.smt2:1.11: Consider setting a stricter logic for (likely) better performance.
test/L1/pos/.liquid/inc00.re.smt2.smt2:1.11: To suppress this warning in the future use (set-logic ALL).
(error "Parse Error: test/L1/pos/.liquid/inc00.re.smt2.smt2:16.37: Symbol 'Str' not declared as a type
shingarov commented 7 months ago

fixpoint test/L1/pos/.liquid/inc00.re.smt2 --save $ cvc5 test/L1/pos/.liquid/inc00.re.smt2.smt2 (error "Parse Error: ...

This is a topic more suitable for discussing in liquid-fixpoint, because from Sprite's perspective, Sprite has generated a valid VC and here its scope ends.

Having said that. I don't think fixpoint is truly LIBSMT2-variant neutral. You need to pass it --solver cvc4 or --solver z3. Both these work for your inc00 case. I haven't tried with cvc5, I doubt cvc5 is supported.

Returning back to the subject of Sprite saving VCs,... now I am remembering. There are places where Sprite will save a VC on which fixpoint chokes but the *.re.smt2 can be easily fixed by hand (usually some silly little omission in the pretty-print). However, here is a much more annoying example, L8/pos/sum.re. Even after fixing the syntax of (qualif...), you would then need to fix missing $ in k_##4 and then fixpoint reports UNSAFE, sending for on another two-hour debug trip before you realize it's simply because the *.re.smt2 doesn't begin with fixpoint --rewrite.