SFunArray variant with more control over uninitialized reads

[bts]

Hi Levent,

The combination of uninterpret and SFunArray that you mentioned in #378 works very well, but a noticeable drawback of uninterpret is that falsifying models contain no information about the data in those arrays (indeed this was also the case for SArray.) To that end, I've been trying my hand at an adaptation of SFunArray that allows for a combination of free values in an array and the ability to report back assignments to those values in modelAssocs.

The approach I've taken results from the observation that every uninitialized read of an array (let's say this happens n times) could pertain to a different key, and that if n is small, we can simply explicitly provide a (free) "default value" for each of these reads. If these default values are allocated in Symbolic, they're included in the model. In order for repeated reads to the same key to return the same value, we keep track of the default values we've issued so far (vs the static initialization function in SFunArray.) A notable upshot is that this construction is unfortunately not a SymArray because readArray doesn't produce an updated array like writeArray does, and this new read needs to take the default value as well.

Here's what I currently have:

{-# LANGUAGE ScopedTypeVariables #-}

module Pact.Analyze.SBV where

import           Control.Monad.Cont (Cont, cont, mapCont, runCont, withCont)
import           Data.SBV           (EqSymbolic ((.==)), HasKind,
                                     Mergeable (symbolicMerge), SBV, SymWord,
                                     ite, uninterpret)
import qualified Data.SBV.Internals as SBVI

-- | A symbolic array which demands a new symbolic value for each read,
-- defaulting to that value if the key is not equal to any previously used to
-- access the array.
--
-- This allows fine-grained control over the array's range and better model
-- reporting, but is only suitable for use cases with smaller numbers of array
-- accesses.
--
-- This array works similarly to 'SFunArray', but instead of "default values"
-- being determined by the function initially passed to 'mkSFunArray', it uses
-- 'Cont' to allow adding 'ite's to either the /top/ or the /leaf/ a chain of
-- 'ite's:
--
-- @
--     [ ] <- a write adds a new ite here
--       ite
--         ite
--           ite
--             [ ] <- a read adds a new ite here
-- @
--
-- Once we are ready to use the array, we plug up the bottom hole with
-- 'realizeArr', which adds a final, noop else-case that will never be reached.
--
-- When we 'symbolicMerge' two 'Arr's, those separate trees will be joined
-- under a new ite:
--
-- @
--     [ ] <- writes will still add a new ite here
--       ite <- this is the new, conjoining ite
--        / \
--      ite  ite
--       ite   ite
--        ite    ite
--         [ ]     [ ]
--           `-------`-- reads will now add ites to both leaf locations
-- @
--
newtype Arr a b = Arr (Cont (SBV a -> SBV b) ())

mkArr :: Arr a b
mkArr = Arr $ cont ($ ())

realizeArr :: HasKind b => Arr a b -> SBV a -> SBV b
realizeArr (Arr m) = runCont m (\() _a -> uninterpret "__impossible")

-- | Unlike with 'SymArray', reading:
--
--     (1) requires a new symbolic value to default to, and
--     (2) returns an updated array
--
readArr
  :: (SymWord b, HasKind b)
  => Arr a b   -- ^ The array to read from
  -> SBV b     -- ^ The symbolic value this read will default to
  -> SBV a     -- ^ The symbolic key to lookup
  -> ( SBV b   -- ^ The resulting symbolic value
     , Arr a b -- ^ The updated array
     )
readArr (Arr m) defaultB a = (realizeArr arr' a, arr')
  where
    -- Here we add new conditionals to /every leaf/ of the ite tree:
    arr' = Arr $ withCont (\k () a' -> ite (a .== a') defaultB (k () a')) m

writeArr :: SymWord b => Arr a b -> SBV a -> SBV b -> Arr a b
writeArr (Arr m) a b = Arr $
  -- Here we add a new conditional to the /top/ the ite tree, like
  -- 'SFunArray':
  mapCont (\k a' -> ite (a .== a') b (k a')) m

instance SymWord b => Mergeable (Arr a b) where
  symbolicMerge _ t (Arr m1) (Arr m2) = Arr $ cont $ \k a ->
    ite t (runCont m1 k a) (runCont m2 k a)

instance (HasKind a, HasKind b) => Show (Arr a b) where
  show (Arr _) = "Arr<" ++ SBVI.showType (undefined :: a) ++ ":"
    ++ SBVI.showType (undefined :: b) ++ ">"

Is this overkill, and have I missed another approach that can more simply allow for access to/control over these uninitialized reads?

If this is something that might be useful to SBV users generally, I would be happy to put together a pull request taking any suggestions you have into account. Also naturally this Arr would need a new name if it were to live in SBV.

Thanks again! Brian

[LeventErkok]

I think you can do something simpler:

{-# LANGUAGE OverloadedStrings #-}

import Data.SBV

type A = SFunArray String Integer

aread :: String -> A -> SString -> Symbolic SInteger
aread tag a k = do v <- free tag
                   let val = readArray a k
                   constrain $ v .== val
                   return val

q :: Predicate
q = do let a :: A
           a = mkSFunArray (uninterpret "a")

       v <- aread "a[\"k\"]" a "k"

       return $ v .== 2

If I try to prove q, I get:

*Main> prove q
Falsifiable. Counter-example:
  a["k"] = 0 :: Integer

Or, if I try to satisfy it:

*Main> sat q
Satisfiable. Model:
  a["k"] = 2 :: Integer

Is this what you're trying to achieve?

[bts]

You beat me to it -- I was just typing up some text describing this same approach as an alternative :)

I shied away from this at first because I've been trying to do as much work outside Symbolic as possible, but I guess I should be reconsidering that assumption.

Indeed I think this is probably the better route to go. Thank you again!

[LeventErkok]

This is a common trick actually; used when you want to have some extra constraints on "fresh" variables. Note that the aread function can impose further constraints on the value read easily; for instance they are all greater than zero, etc.; keeps the code modular and much simpler to work with:

aread :: String -> A -> SString -> Symbolic SInteger
aread tag a k = do v <- free tag
                   let val = readArray a k
                   constrain $ v .== val
                   constrain $ v .> 0        -- or add other constraints as you see fit, any predicate would do
                   return val

[bts]

Great -- thanks!