Fix printing of arrays when they appear in counterexamples.

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,