Arrays in query mode

[bch29]

I'm doing some work with program verification, and as part of it I tried to use SBV's array logic in query mode. It gave me an exception asking me to submit a feature request:

*** Data.SBV: Unsupported interactive/query mode feature.
***  An array update:
***    Array info: (SInteger,SInteger)
*** Data.SBV: Please report this as a feature request!

This would be very nice to have if you have time. Thanks!

[LeventErkok]

Hi.. Can you say a bit more about your use case? One reason this got left behind was I wanted to see actual use cases before making any design choices. Perhaps there's a way to code it before the query mode starts? (Updates are fully supported in the non-query section.)

A full example of what you're trying to do would help guide how this interaction should work. Thanks!

[bch29]

I've been doing Hoare triplet verification for Fortran. The reason I was using query mode is that I wanted to do a computation while retaining access to a Symbolic monad environment to get fresh symbolic variables as I go along. I put ExceptT over it because things can go wrong, but then there's no way to say "query the solver if the Symbolic value doesn't contain an error" without staying in Symbolic and using query mode. That's the only reason I was using it though, it wasn't actually necessary to query the solver more than once in a single Symbolic computation.

I've worked around it for now by throwing the error from ExceptT into Symbolic's underlying IO then catching it when I run the transformer stack. This feels ugly but it works fine for now. It would be helpful if Symbolic became a monad transformer so I could put ExceptT inside it and avoid the issue that way.

On the other hand, it seems likely that I'll want to use query mode in its full capacity in what I'm doing next. I haven't quite worked out the details yet, but I'll be implementing Chaudhury et al's continuity analysis [1] which involves discharging a lot of constraints as it proceeds. Perhaps I'll get back to you if it does turn out I need the feature.

[1] https://www.cs.rice.edu/~sc40/pubs/continuity.pdf

[LeventErkok]

I see.. That actually looks like a good use case for queries indeed, do let me know how it goes.

For array-updates in the query mode: Can you create a simple SBV program that exhibits the problem? I'll see if I can make that segment work at least, which should be a good starting point. Something that starts the query mode and does an update would suffice I suppose, but it'd be great to see exactly how you tried it.

[LeventErkok]

@bch29 I've pushed in the changes required to support arrays in query mode. It was a bit tricker than I thought; so, it would be nice if you can give it a try to make sure it works as expected. (You'll need to build from github master, let me know if that's an issue.)

[bch29]

It's throwing an error for my code, although so far I can't reproduce it in a smaller test case. While I try to reproduce it, here's the transcript and error:

** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s_2 () Bool false)
[GOOD] (define-fun s_1 () Bool true)
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () Int) ; tracks user variable "loop_arrays_i10"
[GOOD] (declare-fun s1 () Int) ; tracks user variable "loop_arrays_x8"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] (declare-fun array_0 () (Array Int Int))
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (assert s_1)
[GOOD] (define-fun s3 () Int 8)
[GOOD] (define-fun s16 () Int 1)
[GOOD] (declare-fun array_1 () (Array Int Int))
[FAIL] (assert (= array_1 (store array_0 s17 s6)))
[SYNC] Attempting to synchronize with tag: "terminating upon unexpected response (at: 2017-09-05 13:10:06.385469 BST)"
[SYNC] Synchronization achieved using tag: "terminating upon unexpected response (at: 2017-09-05 13:10:06.385469 BST)"
*** Exception: 
*** Data.SBV: Unexpected response from the solver.
***    Context : assert
***    Sent    : (assert (= array_1 (store array_0 s17 s6)))
***    Expected: success
***    Received: (error "line 16 column 34: unknown constant s17")

[bch29]

It's probably worth mentioning I'm using Data.SBV.Dynamic quite a lot, and I've also ended up using Data.SBV.Internals to translate between dynamic and typed values. I might just be doing something wrong. The same code works when evaluated outside of query mode though.

[LeventErkok]

Would be really great to see the code that gave rise to this; if you can share.

[bch29]

I'm afraid there are lots of layers of abstraction on top of SBV which will probably make it very difficult to diagnose what is going on. I should be able to share it with you though. It'll take me a little while to get it together.

[bch29]

OK, you can clone the sbv-issues branch of this repository: https://github.com/bch29/camfort/tree/sbv-issues

I've provided a stack.yaml that should make everything build. To test it, you'll want to load the module Camfort.Specification.Hoare in ghci and evaluate testHoare.

It's a big project and as I said, there's a lot of abstraction making it potentially difficult to see what's going on. That being said, I can narrow it down a little. Modules that you'd be interested by are everything under Language.Fortran.Model.* and Camfort.Verification.Hoare.CheckBackend. A lot of SBV interaction happens in the language-verification package, see the query-mode branch of https://github.com/bch29/language-verification .

[LeventErkok]

Thanks.. I'm still trying to replicate this just using SBV; but haven't had luck so far.

[LeventErkok]

Good news is that I was able to replicate this:

q5 :: Symbolic (Maybe (Word8, Int8))
q5 = do m  :: SArray Word8 Int8 <- newArray "a"

        a <- sWord8 "a"
        v <- sInt8  "v"

        query $ do let m2    = writeArray (writeArray m a v) (a+1) (v+1)
                       vRead = readArray  m2 a

                   constrain $ v + 1 ./= vRead

                   cs <- checkSat

                   case cs of
                     Unsat -> return Nothing
                     Unk   -> error "solver returned Unknown!"
                     Sat   -> do av <- getValue a
                                 vv <- getValue v
                                 return $ Just (av, vv)

I think I see the issue, will need to see if I can patch it shortly.

[LeventErkok]

@bch29 I've pushed a fix that should address this issue. Can you check to see if the problem has disappeared?

[bch29]

Yep, it seems to work now. Thanks!

[LeventErkok]

@bch29 Fantastic. I'll close this ticket then. The query mode is still rather new and there might be more gotchas, please do report if you run into anything else that looks suspicious.

[LeventErkok]

@bch29 SBV 7.3 (which includes support for arrays in query mode) is now released on Hackage.