What4 over-eagerly produces counterexamples with ArrayMapping instead of ArrayConcrete

[RyanGlScott]

what4 has two different representation of concrete SMT arrays (i.e., GroundArrays):

• ArrayMapping: an array that is defined by a total, higher-order function.
• ArrayConcrete: an array where most indices map to a constant value, with certain indices mapping to separate values instead.

It is far preferable to have ArrayConcrete instead of ArrayMapping in counterexamples, as it is much simpler to display and inspect ArrayConcrete values than it is to display ArrayMapping.

To my surprise, what4 often produces ArrayMapping values in places where an ArrayConcrete would suffice. Consider this example, for instance:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Main (main) where

import Data.Foldable (forM_)
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Nonce (newIONonceGenerator)
import Data.Parameterized.Some (Some(..))
import System.IO (stdout)

import What4.Config
import What4.Expr
import What4.Interface
import What4.Solver
import What4.Protocol.SMTLib2

z3executable :: FilePath
z3executable = "z3"

main :: IO ()
main = do
  Some ng <- newIONonceGenerator
  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng
  extendConfig z3Options (getConfiguration sym)

  arr <-
    freshConstant
      sym
      (safeSymbol "arr")
      (BaseArrayRepr (Ctx.Empty Ctx.:> BaseIntegerRepr) BaseBoolRepr)
  idx27 <- intLit sym 27
  arr27 <- arrayLookup sym arr (Ctx.Empty Ctx.:> idx27)
  idx42 <- intLit sym 42
  arr42 <- arrayLookup sym arr (Ctx.Empty Ctx.:> idx42)
  p <- andPred sym arr27 =<< notPred sym arr42
  checkModel sym p arr
    [ ("arr27", SomeExpr arr27)
    , ("arr42", SomeExpr arr42)
    ]

data SomeExpr t where
  SomeExpr :: Show (GroundValue tp) => Expr t tp -> SomeExpr t

printGroundArray ::
  Show (GroundValue b) =>
  GroundArray idx b ->
  IO ()
printGroundArray gArr =
  case gArr of
    ArrayMapping{} ->
      putStrLn "ArrayMapping"
    ArrayConcrete def updates ->
      putStrLn $ showString "ArrayConcrete "
               . showsPrec 11 def
               . showChar ' '
               . showsPrec 11 updates
               $ ""

checkModel ::
  Show (GroundValue b) =>
  ExprBuilder t st fs ->
  BoolExpr t ->
  Expr t (BaseArrayType idx b) ->
  [(String, SomeExpr t)] ->
  IO ()
checkModel sym f arr es = do
  withZ3 sym z3executable defaultLogData{logHandle = Just stdout} $ \session -> do
    assume (sessionWriter session) f
    runCheckSat session $ \result ->
      case result of
        Sat (ge, _) -> do
          putStrLn "Satisfiable, with model:"
          gArr <- groundEval ge arr
          printGroundArray gArr
          forM_ es $ \(nm, SomeExpr e) -> do
            v <- groundEval ge e
            putStrLn $ "  " ++ nm ++ " := " ++ show v
        Unsat _ -> putStrLn "Unsatisfiable."
        Unknown -> putStrLn "Solver failed to find a solution."

Here, the SMT array arr could be concretized as an ArrayConcrete where most indices map to True, but where the value at index 42 maps to False instead. To my surprise, however, that is not what what4 picks when concretizing arr:

$ runghc Main.hs
(set-option :produce-models true)
(set-option :pp.decimal true)
; :1:0
(declare-datatypes (T0) ((Struct1 (mk-struct1 (struct1-proj0 T0)))))
(declare-fun arr () (Array Int Bool))
(define-fun x!0 () Bool (select arr 27))
(assert x!0)
(define-fun x!1 () Bool (select arr 42))
(assert (not x!1))
(check-sat)
; sat
Satisfiable, with model:
ArrayMapping
(get-value (x!0))
; ((x!0 true))
  arr27 := True
(get-value (x!1))
; ((x!1 false))
  arr42 := False
(exit)

Note that I am interleaving the SMT solver interactions (using defaultLogData{logHandle = Just stdout}), but the important bit is that ArrayMapping appears in the output rather than ArrayConcrete. What's more, this ArrayMapping does not come from the SMT solver, since there is no corresponding (get-value ...) call in the Z3 process for retrieving a model for arr. As such, this ArrayMapping must be coming from what4's own simplification rules.

We should investigate why this happens and see if we can make what4 produce an ArrayConcrete here instead of an ArrayMapping.