Merge pull request #2121 from GaloisInc/2120-function-arrays

Don't fail when What4 sends us a function-based array in a result.

Author: sauclovian-g

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

@@ -114,10 +114,32 @@ 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 _ _) (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) (ArrayMapping _) = do
+    -- ArrayMapping is an array represented as a function call we can
+    -- use to extract values. We can't do anything useful with this
+    -- because we don't have any clue what key values to look at and
+    -- no good way to figure that out either. So return a placeholder
+    -- value in FirstOrderValue.
+    --
+    -- (The frustrating part is that in many cases the _user_ will
+    -- know what key values to look at, but has no way to tell us.)
+    --
+    -- In principle we could change groundToFOV to return any of an
+    -- error, a FirstOrderValue, or a separate FunctionArrayValue
+    -- type, and use that channel to return the actual function
+    -- handle. (Including the function handle in a FirstOrderValue
+    -- value is problematic as things stand.) However, there's nothing
+    -- to be gained by doing this without a way to figure out what
+    -- key values to look at. And realistically, if we ever _do_
+    -- come up with a way to figure out what key values to look at,
+    -- it should be implemented in What4 so What4 never returns
+    -- ArrayMapping.
+    --
+    -- (See Note [FOVArray] in in saw-core:Verifier.SAW.FiniteValue
+    -- where FirstOrderValue is defined.)
+    ty_idx' <- typeReprToFOT ty_idx
+    ty_val' <- typeReprToFOT ty_val
+    pure $ FOVOpaqueArray ty_idx' ty_val'
 groundToFOV (BaseArrayRepr (Empty :> ty_idx) ty_val) (ArrayConcrete dfl values) = do
     ty_idx' <- typeReprToFOT ty_idx
     dfl' <- groundToFOV ty_val dfl

saw-core/src/Verifier/SAW/FiniteValue.hs

@@ -78,13 +78,20 @@ data FirstOrderType
 -- The type argument of FOVArray is the key type; the value type is
 -- derivable from the default value, which is the second argument. The third
 -- argument is an assignment for all the entries that have non-default values.
+--
+-- FOVOpaqueArray is for arrays we get back from the solver only as a
+-- function call that one can use for lookups. We can't do anything
+-- with that (see Note [FOVArray] below) so we just treat it as an
+-- opaque blob. The arguments are the key and value types, since we
+-- do at least have that info.
 data FirstOrderValue
   = FOVBit Bool
   | FOVInt Integer
   | FOVIntMod Natural Integer
   | FOVWord Natural Integer -- ^ a more efficient special case for 'FOVVec FOTBit _'.
   | FOVVec FirstOrderType [FirstOrderValue]
   | FOVArray FirstOrderType FirstOrderValue (Map FirstOrderValue FirstOrderValue)
+  | FOVOpaqueArray FirstOrderType FirstOrderType
   | FOVTuple [FirstOrderValue]
   | FOVRec (Map FieldName FirstOrderValue)
   deriving (Eq, Ord, Generic)
@@ -107,11 +114,49 @@ data FirstOrderValue
 -- clear how we'd use this, since the primary thing we do with array
 -- values that come back from the solver is print them as part of
 -- models and without a way to know what keys are present a function
--- that just extracts values is fairly useless. For the moment, if one
--- of these pops up, it fails during conversion to FOVArray.
--- 
--- Furthermore, restrictions in What4 mean that array values coming
--- back from the solver via that interface are indexed only by
+-- that just extracts values is fairly useless. If one of these pops
+-- up, it comes back as FOVOpaqueArray and we treat it as an opaque
+-- blob. Unfortuately this does happen (maybe we can improve What4 so
+-- it happens less or maybe not at all, but that's not happening right
+-- away) so we need to be able to handle it rather than erroring out
+-- or crashing.
+--
+-- Note that trying to retain the function at this level is
+-- problematic for a number of reasons:
+--
+--    1. It's not actually a first-order value, and calling it one is
+--       borrowing trouble.
+--
+--    2. We need ToJSON and FromJSON instances for solver caching, and
+--       there's no way to do that. Now, trying to stick one of these
+--       objects in the solver cache is just not going to work no
+--       matter how we handle it; but things are not structured so
+--       that we can e.g. decline to cache values that contain
+--       function-based arrays so that it's safe to stub out the
+--       ToJSON and FromJSON instances with an error invocation. That
+--       could doubtless be arranged, but it'll take work, possibly a
+--       lot of work. As things stand, we _can_ stuff FOVOpaqueArray
+--       into the solver cache, and it won't do anything useful when
+--       we unstuff it later, but it won't crash.
+--
+--    3. FirstOrderValue needs Eq and Ord instances, at least but not
+--       necessarily only for use by maps. At least one of those maps
+--       (the one used in FOVArray) is restricted to not have array
+--       values as keys; however, that's not an _explicit_ restriction
+--       (e.g. in typechecking), it's a consequence of the things
+--       What4 allows as array keys. To be halfway safe we'd need to
+--       make it an explicit restriction, and in the current state of
+--       SAW maintenance it's not really clear enough where we'd need
+--       to enforce that to keep it safe. Also, there may be other
+--       such maps about where arrays _can_ be keys, or for that
+--       matter other comparisons. In principle you could have the
+--       compiler find you all the uses by disabling the Eq and Ord
+--       instances. But that doesn't work because the ToJSON and
+--       FromJSON classes need them. The compiler then just fails on
+--       those before telling you anything else.
+--
+-- Besides all the above, restrictions in What4 mean that array values
+-- coming back from the solver via that interface are indexed only by
 -- integers or bitvectors. At this layer, though, we can support any
 -- FirstOrderValue.
 --
@@ -159,6 +204,8 @@ instance Show FirstOrderValue where
             d' = showEntry ("<default>", d)
         in
         showString "[" . commaSep (vs' ++ [d']) . showString "]"
+      FOVOpaqueArray _kty _vty ->
+        showString "[ opaque array, sorry ]"
       FOVTuple vs -> showString "(" . commaSep (map shows vs) . showString ")"
       FOVRec vm   -> showString "{" . commaSep (map showField (Map.assocs vm)) . showString "}"
     where
@@ -187,6 +234,8 @@ ppFirstOrderValue opts = loop
           vs' = map ppEntry $ Map.toAscList vs
       in
       brackets (nest 4 (sep (punctuate comma (vs' ++ [d']))))
+   FOVOpaqueArray _kty _vty ->
+      pretty "[ opaque array, sorry ]"
    FOVTuple xs   -> parens (nest 4 (sep (punctuate comma (map loop xs))))
    FOVRec xs     -> braces (sep (punctuate comma (map ppField (Map.toList xs))))
       where ppField (f,x) = pretty f <+> pretty '=' <+> loop x
@@ -264,6 +313,7 @@ firstOrderTypeOf fv =
     FOVWord n _ -> FOTVec n FOTBit
     FOVVec t vs -> FOTVec (fromIntegral (length vs)) t
     FOVArray tk d _vs -> FOTArray tk (firstOrderTypeOf d)
+    FOVOpaqueArray tk tv -> FOTArray tk tv
     FOVTuple vs -> FOTTuple (map firstOrderTypeOf vs)
     FOVRec vm   -> FOTRec (fmap firstOrderTypeOf vm)
 
@@ -391,6 +441,8 @@ scFirstOrderValue sc fv =
               v' <- scFirstOrderValue sc v
               scArrayUpdate sc tk' tv' arr k' v'
         ifoldrM visit arr0 vs
+    FOVOpaqueArray _tk _tv -> do
+        fail "Cannot convert opaque array to SharedTerm"
     FOVTuple vs -> scTuple sc =<< traverse (scFirstOrderValue sc) vs
     FOVRec vm   -> scRecord sc =<< traverse (scFirstOrderValue sc) vm
 

saw-remote-api/src/SAWServer/ProofScript.hs

@@ -231,7 +231,8 @@ exportFirstOrderExpression fv =
     FOVIntMod m i -> return $ IntegerModulo i (toInteger m)
     FOVWord w x -> return $ Num Hex (pack (showHex x "")) (toInteger w)
     FOVVec _t vs -> Sequence <$> mapM exportFirstOrderExpression vs
-    FOVArray{}  -> Left "exportFirstOrderExpression: unsupported type: Array"
+    FOVArray{} -> Left "exportFirstOrderExpression: unsupported type: Array (concrete case)"
+    FOVOpaqueArray{} -> Left "exportFirstOrderExpression: unsupported type: Array (opaque case)"
     FOVTuple vs -> Tuple <$> mapM exportFirstOrderExpression vs
     FOVRec _vm  -> Left "exportFirstOrderExpression: unsupported type: Record"