Fix printing of arrays when they appear in counterexamples.

[sauclovian-g]

See commit for notes. Fixes #2049.

[RyanGlScott]

To respond to the four concerns you raise in your commit message:

1. The type matching in indexToFOV in FirstOrder.hs isn't working correctly.

I presume you're referring to this comment?

saw-script/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs

Lines 132 to 134 in 9cbbc2b

	-- XXX: presumably ty and ty2 should match and this should prevent the
	-- need for the final error case, but I can't get it to work
	indexToFOV :: BaseTypeRepr ty -> Assignment IndexLit ty2 -> Either String FirstOrderValue

If so, then I think you can (and should) make the types the same. That being, this function will still need to be partial, since IndexLit only has cases for BaseIntegerType and BaseBVType. (The fact that there aren't IndexLits for other types is a bit curious, but I don't think we need to solve that problem just yet.)

There is similar code in what4 dealing with IndexLits that is also partial (e.g., here), so would be in line with how this is handled elsewhere.

2. Fixing FirstOrderValue arrays (FOVArray) to contain actual values changes the associated JSON schema and it's not clear what the ramifications of that are.

I think this is fine. It is not at all clear to me what the previous implementation of FOVArray was meant to do, and I think your version is a strict improvement. From that perspective, I think it's fine to update the JSON schema for FOVArrays as well. The JSON schema is (AFAIU) only used as part of SAW's caching mechanism.

3. Fixing the conversion to Term changes the behavior of anything that exercised that code path. It's not clear what ramifications that has either, although since the prior behavior was to mysteriously generate types instead of values, it's fairly unlikely anything important depends on it.

Similarly, I have no idea what the previous code path was trying to do—it seems rather broken. I'd be much happier with something resembling the new code in this PR.

4. Currently if we get an ArrayMapping GroundValue array (one where you can only get values out by calling a lookup function) we fail. It's not clear if these ever appear or what should actually be done if one does.

It is absolutely possible for what4 to produce an ArrayMapping value when producing a GroundArray. Here is a proof of concept:

{-# 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
    [ ("idx27", SomeExpr idx27)
    , ("arr27", SomeExpr arr27)
    , ("idx42", SomeExpr idx42)
    , ("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 $ \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."

Running this yields:

Satisfiable, with model:
ArrayMapping
  idx27 := 27
  arr27 := True
  idx42 := 42
  arr42 := False

That being said, I don't have a clear idea of how we'd represent ArrayMapping values in SAWCore. I think it would be fine to fail for now if we encounter one.

[sauclovian-g]

1. Got it fixed, thanks (for anyone following along, part of this happened elsewhere)
2. Ok, let's just move ahead then.
3. Same
4. That is what it'll do now, so I guess we can proceed... though this should probably not be merged until the current release goes out, just in case.

[sauclovian-g]

I force-pushed to squash the fix commit. This can be reviewed now, though it shouldn't be merged until the release goes out.

[RyanGlScott]

This is fantastic. Thanks, @sauclovian-g!

Also, I'll be That Guy: please make sure to mention these changes in the changelog.

[sauclovian-g]

(also I think all the commits should get squashed before being merged; let me know if you disagree)

[sauclovian-g]

First force was to rebase on head, second to squash it all together. This should be ready to go unless it randomly explodes in the CI.

[sauclovian-g]

hmm, I tagged this "needs test" and then didn't write a test, guess I should do that

[sauclovian-g]

I have squashed it again and I'll merge it after I make lunch unless it blows up for some reason.