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?

https://github.com/GaloisInc/saw-script/blob/9cbbc2b7a3496efc78c3772d893078397965a79d/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs#L132-L134

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:

```hs {-# 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.

[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.