lsrcz / grisette Goto Github PK

SingleU and IfU are used to pattern match on UnionPrjOp types. However, these seem to be very bad names.

Consider changing it to Single and If, and rename the corresponding data constructor for Union.

See https://github.com/lsrcz/grisette/actions/runs/9734648723/job/26862937631. The test for the (**) operator has failed during the random test.

The bug is most likely an sbv bug or a bug in our test suite, where we used encodeFloat and decodeFloat to compare FP and Float. Need more time to investigate.

We should align the *1 classes with the change to the Eq1 and Ord1 instances in base-4.18 (GHC-9.6). The change in base is described in haskell/core-libraries-committee#10.

Hello @lsrcz , I am a Rosette user who would like to move to Grisette as soon as possible, but I think I will need tutorials on Grisette to get started initially. So I was wondering when will the tutorials on it will be made available? Thanks.

QuickCheck-based fuzzer could be useful for quickly testing an implementation and generating counter-examples. Grisette introduced the bit-vector types, but not yet have Arbitrary instances for them.

The links to GitHub in the package.yaml is pointing to the legacy Grisette.

Currently, the CEGIS interface in Grisette is provided by using a single ExceptT ... UnionM container and translate the errors differently for synthesizer and verifier. A more general interface should accept a symbolic semantics (which could be angelic), and a verifier/fuzzer (which is an IO action generates counter-examples, can even be calling an external program and do not have to rely on solvers).

Currently Grisette provides a limited set of wrappers for the library monadic functions to help keep the result merged. We should add more wrappers, e.g., for StateT.

We need a way to convert from integer/int to bit vectors. An additional bit size parameter is needed so fromInteger does not work here.

Suppose we have a type:

data AST
  = Add (UnionM AST) (UnionM AST)
  | Mul (UnionM AST) (UnionM AST)
  | Lit SymInteger
   deriving (Show, Generic)
   deriving (Mergeable) via (Default AST)

Consider how to construct a value of this type. To construct the value (a + b) * (c + d), we may have to write:

Mul
  (mrgReturn $ Add (mrgReturn $ Lit "a") (mrgReturn $ Lit "b"))
  (mrgReturn $ Add (mrgReturn $ Lit "c") (mrgReturn $ Lit "d"))

This is ridiculously verbose.

A better way to construct this is to provide a type class that constructs an AST or a UnionM AST in a unified way:

class ASTBuilder ast where
  add :: UnionM AST -> UnionM AST -> ast
  mul :: UnionM AST -> UnionM AST -> ast
  lit :: SymInteger -> ast

and implement the following two instances:

instance ASTBuilder AST where
  add = Add
  mul = Mul
  lit = Lit

instance ASTBuilder (UnionM AST) where
  add l r = mrgReturn $ Add l r
  mul l r = mrgReturn $ Mul l r
  lit v = mrgReturn $ Lit v

Then we can construct (a + b) * (c + d) by

Mul (add (lit "a") (lit "b")) (add (lit "c") (lit "d"))

as expected.

This can be done with Template Haskell. It may be a good idea to have a way to configure the function names to avoid name clash.

Currently in Grisette, the symbolic bit vectors can only be shifted by Int values as it is using the Data.Bits module. We want to allow the symbolic bit vectors to be shifted by a symbolic bit vector value of the same bit size.

It's usually hard to read the symbolic values generated by Grisette. It's good to have a prettyprinter implemented for Grisette.

Proposed pretty printer library: https://hackage.haskell.org/package/prettyprinter.

Similar to state, cont, etc. in mtl, we should have a procedure to lift a pure Fresh operation into a MonadFresh. This is also related to #108 .

String is bad for performance. We should use Text.

Currently the lowerSinglePrim function can only be called on Query or Symbolic types. This should be generalized to any MonadIO types transformed by QueryT or SymbolicT.

The stock readNumber does not parse binary numbers.

> read "0b1" :: WordN 8
0b*** Exeption: Prelude.read: no parse

We need special handling for them.

The data constructors for FreshT and Fresh are currently not exported. They should be exported so that more monad classes could be implemented for them outside of Grisette.

Currently a Data.Text.Text is printed with the quotation marks, while printing a String does not.

>>> import qualified Data.Text as T
>>> gpretty ("a" :: T.Text)
"a"
>>> gpretty ("a" :: String)
a

We should remove these quotation marks for Data.Text.Text

looking at sbv it has support for both floats of arbitrary precision and rational numbers could grisette add support for them?

The current interface to the SomeIntN and SomeWordN are hard to use. We should provide interface to allow creation of these non-bit-width-tagged types from runtime bit-widths.

Possible interface may be added to the BV type class:

bv :: Natural -> Integer -> bv
> bv 12 20
0x014

There are instances for other Grisette-provided type classes for tuples up to length 8, but the ExtractSymbolics instances for tuples longer than 2 are missing.

BVSignConversion type class should be available to Data.Word and Data.Int data types.

Data.Text (https://hackage.haskell.org/package/text) is very useful in processing text data. From my experience I feel that it could be very inconvenient to work with the bytestrings. Grisette should have Data.Text support.

BVSignConversion type class should be exported by the main Grisette module.

Currently the FreshT monad can correctly merge the values generated from multiple paths, however, the Mergeable knowledge will be stripped when the runFreshT is called. We should make sure the results are merged after runFreshT is invoked.

Hello!

1. whats the current intended ghc version / cabal version build range?
2. if its already reflected into the setup-haskell style CI, where am i overlooking it
3. would you be open to adding that otherwise?
   (i guess one sub yak is making sure that the environment has some SMT solver installed for testing?)

happy to help poke at this if needed. I'm keen to use this library, but some use cases need me poking at making sure i can target at least 9.0.x - 9.6.x ghc flavors.