Fix printing of SMT arrays when they appear in counterexamples.

- make room for values in FirstOrderValue arrays
- fix the printer functions accordingly
- we now need From/ToJSONKey instances for FirstOrderValue
- this requires Ord for FirstOrderValue and FirstOrderType
- fix the conversion of FirstOrderValue arrays to Term
- convert GroundValue array values to FirstOrderValue array values

There are three things to be aware of in case they come back to
haunt us:

- Fixing FirstOrderValue arrays (FOVArray) to contain actual values
changes the associated JSON schema. We think this only affects the
solver caching mechanism, so there's some possibility that users will
have to flush/regenerate their caches. More likely nobody will have
exercised this path, since it after all doesn't actually work; any
such current cache entries don't contain the array contents.

- Fixing the conversion to Term changes the behavior of anything that
exercised that code path. This is also probably nothing of
significance; since the the prior behavior was to mysteriously
generate types instead of values, which could hardly fail to go off
the rails downstream, it's fairly unlikely anything important depends
on it.

- 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 in practice or what should actually be
done if one does. This is a more significant possibility, though,
because the behavior now is to fail and that impacts not only the
marginal code paths described above but also the printing of
counterexamples. So we might need to add more support in the future.

This change adds indexed-traversable to saw-core and saw-core-what4,
but the rest of saw already depends on it so this has no real effect.

It also adds a test case. I've noted the provenance of the included
LLVM byte-code blob as per saw-script #1157.

CHANGES.md

@@ -1,3 +1,10 @@
+# next -- TBA
+
+## Bug fixes
+
+* Counterexamples including SMT arrays are now printed with the array
+  contents instead of placeholder text.
+
 # Version 1.2 -- 2024-08-30
 
 ## New Features

intTests/test2049/.gitignore

@@ -0,0 +1,3 @@
+*.rawlog
+*.log
+*.diff

intTests/test2049/Makefile

@@ -0,0 +1,18 @@
+# The current checked-in test.bc was generated by:
+#    Apple clang version 15.0.0 (clang-1500.1.0.2.5)
+#    Target: arm64-apple-darwin22.6.0
+#    Thread model: posix
+#    InstalledDir: /Library/Developer/CommandLineTools/usr/bin
+# but neither the target nor the clang/llvm version is expected to be
+# significant.
+CC = clang
+CFLAGS = -g -O0
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc

intTests/test2049/Test.cry

@@ -0,0 +1,2 @@
+import Array
+type Table = Array [8] [8]

intTests/test2049/test.c

@@ -0,0 +1,12 @@
+#include <stdint.h>
+
+static uint8_t table[256];
+
+void assign(uint8_t k, uint8_t v) {
+   table[k] = v;
+}
+
+void zero(uint8_t k) {
+  assign(k, 0);
+}
+

intTests/test2049/test.log.1.good

@@ -0,0 +1,23 @@
+ Loading file "test.saw"
+ Assume override assign
+ Verifying zero ...
+ Simulating zero ...
+ Registering overrides for `assign`
+   variant `Symbol "assign"`
+ Matching 1 overrides of  assign ...
+ Branching on 1 override variants of assign ...
+ Applied override! assign
+ Checking proof obligations zero ...
+ Subgoal failed: zero test.saw:60:1: error: in ghost_value
+Literal equality postcondition
+
+ SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 334}
+ ----------Counterexample----------
+   zero::table: [1 := 1, <default> := 0]
+   zero::k: 1
+ ----------------------------------
+ Stack trace:
+"llvm_verify" (test.saw:60:1-60:12)
+Proof failed.
+
+FAILED

intTests/test2049/test.log.2.good

@@ -0,0 +1,23 @@
+ Loading file "test.saw"
+ Assume override assign
+ Verifying zero ...
+ Simulating zero ...
+ Registering overrides for `assign`
+   variant `Symbol "assign"`
+ Matching 1 overrides of  assign ...
+ Branching on 1 override variants of assign ...
+ Applied override! assign
+ Checking proof obligations zero ...
+ Subgoal failed: zero test.saw:60:1: error: in ghost_value
+Literal equality postcondition
+
+ SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 334}
+ ----------Counterexample----------
+   zero::table: [0 := 0, <default> := 1]
+   zero::k: 1
+ ----------------------------------
+ Stack trace:
+"llvm_verify" (test.saw:60:1-60:12)
+Proof failed.
+
+FAILED

intTests/test2049/test.saw

@@ -0,0 +1,60 @@
+// Test printing a counterexample that contains an array.
+
+enable_experimental;
+import "Test.cry";
+
+// make some ghost state
+casper <- declare_ghost_state "casper";
+
+// write a (correct) spec for assign; it updates the table with k := v
+let assign_spec = do {
+   // initial state
+   table <- llvm_fresh_cryptol_var "assign::table" {| Table |};
+
+   // get args
+   k <- llvm_fresh_var "k" (llvm_int 8);
+   v <- llvm_fresh_var "v" (llvm_int 8);
+
+   // updated state
+   let table' = {{ arrayUpdate table k v }};
+
+   // run the function
+   llvm_ghost_value casper table;
+   llvm_execute_func [crucible_term k, crucible_term v];
+   llvm_ghost_value casper table';
+};
+
+// write a (wrong) spec for zero; it sets an entry of the table to zero
+let zero_spec = do {
+   // make an initial state
+   table <- llvm_fresh_cryptol_var "zero::table" {| Table |};
+
+   // make an arg
+   k <- llvm_fresh_var "zero::k" (llvm_int 8);
+
+
+   // Restrict the args and initial state so the output is more
+   // deterministic. (There are still two possible counterexamples
+   // and we can't distinguish them without being able to assert
+   // equality of arrays, which Cryptol rejects.) (And actually
+   // there's infinitely many more but it's reasonable to assume
+   // the solver will return a minimal array model.)
+   llvm_assert {{ k == 1 }};
+   llvm_assert {{ arrayLookup table 0 == 0 }};
+   llvm_assert {{ arrayLookup table 1 == 1 }};
+
+   // use a wrong final state
+   let table' = table;
+
+   // run the function
+   llvm_ghost_value casper table;
+   llvm_execute_func [crucible_term k];
+   llvm_ghost_value casper table';
+};
+
+mod <- llvm_load_module "test.bc";
+
+// (we could verify assign, but it's giving me noise about the static
+// allocation and that's not the point here)
+assign <- llvm_unsafe_assume_spec mod "assign" assign_spec;
+llvm_verify mod "zero" [assign] false zero_spec w4;

intTests/test2049/test.sh

@@ -0,0 +1,47 @@
+# Don't exit randomly
+set +e
+
+#
+# This is a hacked subset of what's in support/test-and-diff.sh
+# because we need to be able to check either of two reference outputs.
+# FUTURE: update test-and-diff to support that.
+#
+# to clean: rm -f test.log test.rawlog *.diff
+# 
+
+# run the test
+$SAW test.saw > test.rawlog 2>&1 || echo FAILED >> test.rawlog
+
+# Prune the timestamps and the current directory
+CURDIR=$(pwd -P || pwd)
+sed < test.rawlog > test.log '
+    /^\[[0-9][0-9]:[0-9][0-9]:[0-9][0-9]\.[0-9][0-9][0-9]\] /{
+        s/^..............//
+    }
+    s,'"$CURDIR"'/,,
+'
+
+# diff
+diff -u test.log.1.good test.log > test.log.1.diff 2>&1
+diff -u test.log.2.good test.log > test.log.2.diff 2>&1
+
+# If both diffs are nonempty, we failed.
+if [ -s test.log.1.diff ] && [ -s test.log.2.diff ]; then
+    echo "*** diff 1:"
+    cat test.log.1.diff
+    echo "*** diff 2:"
+    cat test.log.2.diff
+
+    cat 1>&2 <<EOF
+Unexpected test diffs.
+If the new output is correct, update the reference outputs, but
+please don't do so without thinking. Be sure to make corresponding
+updates to all the reference outputs.
+EOF
+
+    # We failed.
+    exit 1
+fi
+
+# done
+exit 0

saw-core-what4/saw-core-what4.cabal

@@ -18,6 +18,7 @@ library
     base >= 4.9,
     bv-sized >= 1.0.0,
     containers,
+    indexed-traversable,
     lens,
     mtl,
     saw-core,

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

@@ -29,6 +29,8 @@ module Verifier.SAW.Simulator.What4.FirstOrder
   ) where
 
 import qualified Data.BitVector.Sized as BV
+import qualified Data.Map as Map
+import Data.Foldable.WithIndex (ifoldlM)
 import Data.Parameterized.TraversableFC (FoldableFC(..))
 import Data.Parameterized.Some(Some(..))
 import Data.Parameterized.Context hiding (replicate)
@@ -38,6 +40,7 @@ import Verifier.SAW.Simulator.What4.PosNat
 import Verifier.SAW.FiniteValue (FirstOrderType(..),FirstOrderValue(..))
 
 import What4.BaseTypes
+import What4.IndexLit
 import What4.Expr.GroundEval
 
 ---------------------------------------------------------------------
@@ -111,13 +114,29 @@ groundToFOV BaseRealRepr    _         = Left "Real is not FOV"
 groundToFOV BaseComplexRepr         _ = Left "Complex is not FOV"
 groundToFOV (BaseStringRepr _)      _ = Left "String is not FOV"
 groundToFOV (BaseFloatRepr _)       _ = Left "Floating point is not FOV"
-groundToFOV (BaseArrayRepr (Empty :> ty) b) _
-  | Right fot1 <- typeReprToFOT ty
-  , Right fot2 <- typeReprToFOT b
-  = pure $ FOVArray fot1 fot2
-groundToFOV (BaseArrayRepr _idx _b) _ = Left "Unsupported FOV Array"
+groundToFOV (BaseArrayRepr _ _) (ArrayMapping _) =
+    -- We don't have a way to represent ArrayMapping in FirstOrderValue
+    -- (see note in FiniteValue.hs where FirstOrderValue's defined)
+    Left "Unsupported FOV Array (values only available by lookup)"
+groundToFOV (BaseArrayRepr (Empty :> ty_idx) ty_val) (ArrayConcrete dfl values) = do
+    ty_idx' <- typeReprToFOT ty_idx
+    dfl' <- groundToFOV ty_val dfl
+    let convert idx values' v = do
+          let idx' = indexToFOV idx
+          v' <- groundToFOV ty_val v
+          return $ Map.insert idx' v' values'
+    values' <- ifoldlM convert Map.empty values
+    pure $ FOVArray ty_idx' dfl' values'
+groundToFOV (BaseArrayRepr _ _) _ =
+    Left "Unsupported FOV array (unexpected key type)"
 groundToFOV (BaseStructRepr ctx) tup  = FOVTuple <$> tupleToList ctx tup
 
+indexToFOV :: Assignment IndexLit (EmptyCtx ::> ty) -> FirstOrderValue
+indexToFOV (Empty :> IntIndexLit k) =
+    FOVInt k
+indexToFOV (Empty :> BVIndexLit w k) =
+    FOVWord (natValue w) (BV.asUnsigned k)
+
 
 tupleToList :: Assignment BaseTypeRepr ctx ->
              Assignment GroundValueWrapper ctx -> Either String [FirstOrderValue]

saw-core/saw-core.cabal

@@ -35,6 +35,7 @@ library
     extra,
     filepath,
     hashable >= 1.3.4,
+    indexed-traversable,
     lens >= 3.8,
     modern-uri >= 0.3.2 && < 0.4,
     MonadRandom,