leventerkok / sbv Goto Github PK

add arithmetic tests for rational arithmetic to the test suite

In terms of mult/div for the SInteger type

Override default definitions of popCount and testBit to "bail out" in case the argument is symbolic, and point out the use of the sbv-replacement in the latter case.

Note that popCount is only available in GHC >= 7.4.1, so we might wait for the next HP release that'll have it. (Otherwise, we'd need some GLASGOW_HASKELL define magic..)

Need some decent documentation for SBV.

tracking path in ite choices might be beneficial. however this interacts badly with sharing. (See inline comments in the implementation of symbolicMerge). Is there a good compromise?

Z3 now comes with the QF_FP logic; supporting IEEE-754 floats. Add support for them in SBV.

The following program

{-# OPTIONS -XScopedTypeVariables #-}
import Data.SBV

f :: Symbolic SBool
f = do
    x <- exists "x" :: Symbolic SInteger
    y <- exists "y"
    return $ x .>= y

main = putStrLn =<< compileToSMTLib True f

produces the (shortened) output:

; --- formula ---
(assert (forall ((s0 Int)
                 (s1 Int))
            (let ((s2 (ite (>= s0 s1) #b1 #b0)))
            (not (= s2 #b1)))))
(check-sat)

As can be seen, the quantifiers were changed from existential to universal.
I guess that this is caused by compileToSMTLib calling the simulate function with the 'isSat' parameter set to False.

the cabal file should list the extensions we rely on (DefaultSignatures, DeriveDataTypeable, etc.) Currently we simply rely on these without any reference to them in the cabal file, which would fail to compile with versions of ghc that don't have these features.. need to collect the entire list of such dependencies and add them based on the cabal other-extensions field, the full recognized list is at: http://hackage.haskell.org/packages/archive/Cabal/1.14.0/doc/html/Language-Haskell-Extension.html#t:KnownExtension

Consider integrating with

• CVC3 (http://cs.nyu.edu/acsys/cvc3/)

• Boolector (http://fmv.jku.at/boolector/)

• STP (http://sites.google.com/site/stpfastprover/)

• MathSat (http://mathsat4.disi.unitn.it/)

• Z3 (http://research.microsoft.com/en-us/um/redmond/projects/z3/)

• OpenSMT (http://verify.inf.unisi.ch/opensmt)

  Potential issues:

• MathSat is not open-source

• Z3 is Windows only

• OpenSMT has QF_BV support but not QF_AUFBV

can we prove the diophantine solver (as coded in Haskell) correct using our SMT based solver? Could be challenging due to quantifiers and the inherent looping involved, but it might be possible to prove simpler (yet interesting) claims.

See if the "explicit" let idea can buy us anything that stable-pointers don't get us in SBV:

http://www.haskell.org/pipermail/haskell-cafe/2008-February/039639.html

The recent move to 7.4.1 dev env broke doctest based testing since doctest doesn't compile with ghc-7.4.1 yet. The call to doctest in the Makefile is currently commented out. Re-enable this once doctest becomes available.

Add the "AIG" generator example; note that we first need to make sure getModel is improved so we don't have to do the ugly exception trick if all we want to display is just one model.

In the following example,

https://github.com/nushio3/practice/blob/master/sbv/square-root.hs

SBV seems to know that there exists at least one solution to (x^2 = 2).
However, it cannot prove that (forSome x. x*x=2).

Why is this behavior? Am I doing something wrong?

Currently not very robust in parsing Yices's output for counterexamples in the presence of uninterpreted functions and arrays. Might be worth waiting till SMT-Lib2 stabilizes.

Currently the code-generator supports input args and output args separately, but there's no support for arguments that are used "in-place"; i.e., use the current values and also update them as well. Sort of like an in-out parameter.

This is not a huge deal actually, since the caller can arrange for this by passing the same argument for both as input and output appropriately, with no loss of functionality. Something like:

 foo (x, y, &x)

where x is used both as input and output.

But this comes at the cost of ugly API, and also it doesn't sound too hard to support this feature, albeit with the explosion of new functions like: cgInputOutput, cgInputOutputArr etc.

Code up AES and show how fast code can be generated from straightforward Haskell, using the T-Box implementation.

remove Eq instance from SBV for GHC >= 7.4.1; which is no longer needed/necessary since Num doesn't have Eq as a superclass anymore.

TODO items:

• add the missing code gen utils for SReals to C (user chosen map type)
• if user chosen mappings are given (real + integer), add these as comments in generated code
• test vector generation: support SReal/SIntegers there? Need to see if there's a need
• search for "realsTBD" tag, marks missing code

Need some worked out examples and test cases for the QBVF solver.

Lee Pike says:

"What about an option for SBV not to generate an example driver? The reason is that for build simplicity, I'd like to just say "build everything in the directory I've put SBV-generated files." But I have my own custom driver with it's own main."

We can easily support this; by means of a codeGen switch..

Compilation falis with the following message on my system.

$ ghc -V
The Glorious Glasgow Haskell Compilation System, version 7.4.2
$ cabal --version
cabal-install version 0.14.0
using version 1.14.0 of the Cabal library
$ cabal install sbv
Resolving dependencies...
Configuring sbv-2.1...
Building sbv-2.1...
Preprocessing library sbv-2.1...
[ 1 of 53] Compiling Data.SBV.Utils.TDiff ( Data/SBV/Utils/TDiff.hs, dist/build/Data/SBV/Utils/TDiff.o )
[ 2 of 53] Compiling Data.SBV.Utils.Lib ( Data/SBV/Utils/Lib.hs, dist/build/Data/SBV/Utils/Lib.o )
[ 3 of 53] Compiling Data.SBV.Utils.Boolean ( Data/SBV/Utils/Boolean.hs, dist/build/Data/SBV/Utils/Boolean.o )
[ 4 of 53] Compiling Data.SBV.BitVectors.AlgReals ( Data/SBV/BitVectors/AlgReals.hs, dist/build/Data/SBV/BitVectors/AlgReals.o )
[ 5 of 53] Compiling Data.SBV.BitVectors.Data ( Data/SBV/BitVectors/Data.hs, dist/build/Data/SBV/BitVectors/Data.o )

Data/SBV/BitVectors/Data.hs:1110:27:
Overlapping instances for NFData Pgm
arising from a use of rnf' Matching instances: instance NFData a => NFData (S.Seq a) -- Defined inData.Sequence'
instance NFData Pgm
-- Defined at Data/SBV/BitVectors/Data.hs:1114:10
In the first argument of seq', namelyrnf pgm'
In the second argument of seq', namely rnf pgm seq rnf cstr seq rnf outs'
In the second argument of seq', namely rnf axs seq rnf pgm seq rnf cstr seq rnf outs'
cabal: Error: some packages failed to install:
sbv-2.1 failed during the building phase. The exception was:
ExitFailure 1

(cabal install -v doesn't seem to give more helpful output)

I have both containers-0.4.2.1 and containers-0.5.0.0 installed, and cabal seems to (try to) build against containers-0.5. It compiles fine if I use:

$ cabal install sbv --constraint "containers == 0.4.2.1" --force-reinstalls

Best,

Now that we talk to Z3 in a more "interactive" way, we can implement allSat by adding extra assumptions, instead of restarting the solver. There's nothing hard in this, just code engineering..

can we build a sketch like dsl on top of sbv?

some sample usage of reals with polynomial constraints would be nice

Short-cut evals on operators are delayed too late. They should be happening earlier. While this causes performance problems at the least, it is completely unacceptable for symbolic-termination issues handled with counters.

Once Z3 team releases v3.3; where they'll start supporting MacOSX natively.

Note that this is only a two line change in the library, but the real work is in hauling the test-suite to use Z3 and accordingly SMTLib2; this'll require adding a whole bunch of new gold-files and making sure all is well. So, easy but laborious task.

There's some movement in Haskell to remove Eq req from Num class and Num req from Bits class, both of these are welcome changes as SBV instances for these are "forced".. Can't have equality on a symbolic variable, as the result might be symbolic. Make sure to reflect those changes in SBV. (Likely after the "next" haskell platform release.)

The C generator currently does not support rotates when the argument is a signed quantity. It's not quite clear if we can rely on >> and << to implement this as the C standard sounds a bit murky. We might have to figure out how to do this properly.

Note that the code generator does support rotates when the argument is an unsigned quantity, which covers most use cases in practice.

Create an example for diophantine equation solving. Consider the quantified approach to the "minimal" set problem. Are the solutions required to be all positive? Then, how does one solve something like x+y+z = -2?

support test cases involving reals? not sure if this is really needed, but might be nice to have.

Top level CAF's in the presence of uninterpreted functions are buggy. To see define:

  t = proveWith verboseSMTCfg $ f 2 .== f 3
            where f :: SWord16 -> SWord16
                  f = uninterpret "f

This will work correctly the first time you "run" t in ghci, and will choke the second time you run it, as the effects are skipped due to the CAF status of t.

A workaround is to give a dummy unit argument to t and turn it into a function; but would be nice if we didn't have to do that.

A solution along the lines of Andy Gill's reifyGraph idea might solve this problem.

Should uninterpreted functions behave like other free_ allocatable items? That would be a more consistent design, but the word/int assumption under free_ is a strong one. Need to explore the design space here.

Improve the AES code-generation example by generating code for keySchedule and encrypt/decrypt separately. Note that this will have to wait until fixed-length lists are available in Haskell, via type-naturals preferably.

Also improve the test-suite for AES, by adding extra enc/dec pairs, once the fixed-length lists are supported in the code generator.

The code generator uses way too many variables than necessary, due to the single-static assignment form it generates. It also skips a whole bunch of variable names that designate constants, as those get inlined.

In practice this works OK, since gcc (or any other decent compiler) can detect short lived variables and get rid of them easily. However, it might be nice if we did this automatically for platforms where the compilers may not do these optimizations. (Otherwise, the frames generated for calls will be too large..)

Improve the pop-count example by "computing" the table automatically

Use 64-bit numbers, as 32-bit numbers overflow very quickly..

Also, add a note on the modular arithmetic, so it'll eventually overflow no matter how big.

(Pointed out by Ian Calvert.)

Hi Levent,

I think SBV 0.9.24 (current Hackage version) on ghc7.4 is failing:

Data/SBV/BitVectors/Model.hs:555:90:
Could not deduce (Show a) arising from a use of show' from the context (Bounded a, Integral a, Num a, SymWord a) bound by the instance declaration at Data/SBV/BitVectors/Model.hs:544:10-66 Possible fix: add (Show a) to the context of the instance declaration In the second argument of(++)', namely
show (minBound :: a, maxBound :: a)' In the second argument of(++)', namely
" is out-of-bounds " ++ show (minBound :: a, maxBound :: a)' In the second argument of(++)', namely
`show x
++ " is out-of-bounds " ++ show (minBound :: a, maxBound :: a)'

I haven't built it myself under 7.4; I just noticed the build log http://hackage.haskell.org/packages/archive/sbv/0.9.24/logs/failure/ghc-7.4

There's a new version of doctest out, with support for blank-lines in the output. Should start using that for inline tests that spit out multi-lines with blanks.

Issues: it has a >= GHC 7.X dependence.. So I need to upgrade too. Also, until Haddock gets the same patch and starts being used in hackage the docs will not go through, which is a huge headache..

So, the change over to the new style will have to wait till Haddock is up..

• Polynomial arithmetic: Need more testing on the semantics of pdiv/pmod/pmult..
• CCITT: 84-inhabitants issue; mismatch with the expected number. What's the semantics?
• GenPoly: is there a better way of generating good polynomials?

The SBV->C compiler always "flattens" the functions, i.e., sequences of elements will be expanded as the C-function is produced. In idiomatic C, you would instead pass elements in arrays. So, while we can deal with arrays implicitly, the translation is not nice, it leads to signatures that are unnecessarily complicated and not idiomatic-C.

To implement this properly, we need a Haskell datatype that can represent the size of the elements in its type, similar to Cryptol's sized sequences. There is no native Haskell type that can do that, but there are some packages in Hackage that use type-level tricks to encode them. (In particular the type-level library http://hackage.haskell.org/package/type-level.) However, type-level only supports naturals up to 5000 nicely (D0, D1, .., D5000), larger numbers, while possible, are cumbersome to write. Also, the 'D' prefix is just unsightly, and being a library it's not as seamless as one would like.

The other alternative is to wait for type-naturals extension of GHC to become available (http://hackage.haskell.org/trac/ghc/ticket/4385), and use that feature instead, which should provide a better user experience. The downside of that is that it isn't clear when type-naturals will be part of GHC.

In any case, the latter option seems to be the best way forward, although we will have to delay the implementation for a while.

The next version of the Data.Bits class will have popCount field in it. Track and add this for SBV when it becomes available. The symbolic implementation will likely be table-lookup based.

The SMTLib2 translator is complicated enough that just using strings is a bit of a mess. Need to rework it and go via non-string based (pretty-printer) solution to give it some structure.

Add support for bit-blasting SBV, and integration with SAT solvers such as ABC (http://www.eecs.berkeley.edu/~alanmi/abc/)

Hi Levent,

I'd like the option to disable Makefile & example driver generation during C compilation, particularly using the compileToCLib call---it's complicates my other code generation, containing another main()---I'd like to just "build everything" in the directory with the generated code without worrying about main being multiply-defined. I see the machinery is there to do that (at least the driver can be disabled using the CgConfig options), but that's not exposed with the compileToCX API functions.

What do you suggest?

In the generated internal.h header, rather than

typedef uint8_t SBool ;

what about

typedef bool SBool ;

In particular, I'm having trouble using CBMC for static analysis, since elsewhere I equate SBool with bool.

Finalize implementation of SReals, backed by rationals on the concrete side with infinite precision algebraic reals on the SMT Side.

TODO:

• Proper support for acquiring both the root-obj and approx. values from Z3.
• How do we tell if a root-obj is precise?
• Support for allSat with reals. Tricky since we do need to have root-objects inside Haskell somehow.

Alas, we need Z3 4.0 to be released for development to see the responses..

Test suite is impacted by this bug: http://hackage.haskell.org/trac/ghc/ticket/7233

Once it's fixed, uncomment the test case: https://github.com/LeventErkok/sbv/blob/master/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs#L179

For code generation with uninterpreted functions, it'd be nicer if we had a construct like:

foo x y z = cgUninterpret "foo" x y z $ (x+y)*z

which would uninterpret the function value during code generation, but otherwise would make it available during simulation/verification. We should be able to implement this with the existing machinery of uninterpreted functions, barring some design choices.. Would be nice to explore..

Currently the SMTLib2 translator doesn't handle the cases when the mutated/reseted user defined arrays are done via non-constant initializers. This is a rare case actually (in fact, the whole use of user defined arrays is rather rare), but it can happen; so we should support it.

Note that this doesn't affect the SMTLib1 translator since all variables are in global scope. The reason the same trick doesn't work for SMTLib2 is because the non-constant initializer can be inside the forall block, either as an input, or as one of the locally defined let-bound variables.