Collapse warnings in vector properties into single warning (#871)

* Collapse warnings in vector properties into single warning

* Fix GHC 8.X compatability

ChangeLog.md

@@ -8,6 +8,8 @@
 
 * Improved the ordering of constraints in generated query files.
 
+* When multiple similar warnings are thrown at different indices of the same property vector (i.e. properties of type `Vector Bool n`), they are now collapsed into a single warning.
+
 ## Version 0.15
 
 * Added functions `min` and `max` over rationals.

vehicle/src/Vehicle/Compile/Print/Warning.hs

@@ -1,11 +1,18 @@
 {-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+{-# HLINT ignore "Use <$>" #-}
 
 module Vehicle.Compile.Print.Warning where
 
+import Data.Bifunctor (Bifunctor (..))
 import Data.List (sortOn)
 import Data.List.NonEmpty (NonEmpty, sort)
-import Data.Set qualified as Set
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map qualified as Map
+import Data.Tuple (swap)
 import Vehicle.Data.Assertion (UnderConstrainedVariableStatus, prettyUnderConstrainedVariable)
+import Vehicle.Data.Tensor (TensorIndices)
 import Vehicle.Prelude
 import Vehicle.Prelude.Warning
 import Vehicle.Verify.Core
@@ -25,19 +32,14 @@ instance Pretty SummarisedCompileWarning where
         <+> quotePretty status
         <+> "without needing to call the verifier. This usually indicates a fault with either the"
         <+> "specification or any external datasets used."
-    UnderSpecifiedProblemSpaceVariablesSummary propertyAddress unsolvedVars -> do
-      let varsDoc = concatWith (\u v -> u <> "," <+> v) (fmap quotePretty (Set.toList unsolvedVars))
-      let pluralisedVarsDoc
-            | length unsolvedVars == 1 = "variable" <+> varsDoc <+> "is"
-            | otherwise = "variables" <+> varsDoc <+> "are"
-
+    UnderSpecifiedProblemSpaceVariablesSummary _ propertyName unsolvedVars -> do
       "In property"
-        <+> quotePretty propertyAddress
-        <+> "the quantified"
-        <+> pluralisedVarsDoc
-        <+> "not always directly related to the input or output of a network."
-        <+> "This is frequently indicative of a bug in the specification."
-    UnsoundStrictOrderConversionsSummary queryFormatID propertyAddress _ ->
+        <+> quotePretty propertyName
+        <+> "there are quantified variables that not always directly related to the input or output of a network."
+        <+> "This is frequently indicative of a bug in the specification. These variables are:"
+        <> line
+        <> prettyObjectsAndTensorIndicesList prettyVariables propertyName unsolvedVars
+    UnsoundStrictOrderConversionsSummary queryFormatID _ propertyAddress _ ->
       "In property"
         <+> quotePretty propertyAddress
         <> ", at least one of the generated queries were found"
@@ -56,18 +58,18 @@ instance Pretty SummarisedCompileWarning where
         <> line
         <> line
         <> "See https://github.com/vehicle-lang/vehicle/issues/74 for further details."
-    AllConstantNetworkInputVariablesSummary _ propertyAddress queryIDs ->
-      "In property"
-        <+> quotePretty propertyAddress
-        <> ", in"
-          <+> prettyQueryIDs queryIDs
-          <+> "all network inputs were fixed to be constants."
-          <+> "Unfortunately there is a known bug in Marabou that it sometimes erroneously returns"
-          <+> "'unsat' for these type of queries."
+    AllConstantNetworkInputVariablesSummary _ _ propertyName queryIDs ->
+      "In some of the queries generated by property"
+        <+> quotePretty propertyName
+        <+> "all network inputs were fixed to be constants."
+        <+> "Unfortunately there is a known bug in Marabou that it sometimes erroneously returns"
+        <+> "'unsat' for these type of queries. The queries are:"
+        <> line
+        <> prettyObjectsAndTensorIndicesList prettyQueryIDs propertyName queryIDs
         <> line
         <> line
         <> "See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details."
-    UnboundedNetworkInputVariablesSummary queryFormat propertyAddress varsByQueryID ->
+    UnboundedNetworkInputVariablesSummary queryFormat _ propertyAddress varsByQueryID ->
       "In property"
         <+> quotePretty propertyAddress
         <> ", the following network input variables do not always have both"
@@ -85,7 +87,36 @@ instance Pretty SummarisedCompileWarning where
             <> line
             <> indent 2 (vsep $ dotDotList 5 $ fmap prettyUnderConstrainedVariable vars)
 
-prettyQueryIDs :: NonEmpty QueryID -> Doc a
-prettyQueryIDs ids =
-  (if length ids == 1 then "query" else "queries")
-    <+> prettyNonEmptyList (fmap pretty (sort ids))
+prettyObjects :: (Ord a, Pretty a) => Bool -> Doc b -> Doc b -> NonEmpty a -> Doc b
+prettyObjects quote single plural ids =
+  (if length ids == 1 then single else plural)
+    <+> prettyNonEmptyList (fmap (if quote then quotePretty else pretty) (sort ids))
+
+prettyQueryIDs :: NonEmpty QueryID -> Doc b
+prettyQueryIDs = prettyObjects False "query" "queries"
+
+prettyVariables :: NonEmpty Name -> Doc a
+prettyVariables = prettyObjects True "variable" "variables"
+
+prettyTensorIndices :: PropertyName -> NonEmpty TensorIndices -> Maybe (Doc b)
+prettyTensorIndices name indices
+  | indices == [[]] = Nothing
+  | otherwise = do
+      let addresses = fmap (quotePretty . PropertyAddress (-1) name) indices
+      Just $ prettyNonEmptyList addresses
+
+prettyObjectsAndTensorIndices :: (NonEmpty a -> Doc b) -> PropertyName -> (NonEmpty a, NonEmpty TensorIndices) -> Doc b
+prettyObjectsAndTensorIndices prettyObject name (ids, indices) = do
+  let indicesDoc = prettyTensorIndices name indices
+  prettyObject ids <> maybe "" (" in" <+>) indicesDoc
+
+prettyObjectsAndTensorIndicesList :: (Ord a) => (NonEmpty a -> Doc b) -> PropertyName -> NonEmpty (a, TensorIndices) -> Doc b
+prettyObjectsAndTensorIndicesList prettyObject name objectsAndIndices = do
+  -- Singleton.nonEmpty doesn't exist until base 4.15
+  let nonEmptySingleton x = [x]
+  -- First map by indices that share the same objects
+  let indicesMap = Map.fromListWith (<>) (NonEmpty.toList $ fmap (second nonEmptySingleton) objectsAndIndices)
+  -- Then find the objects that share the same queries
+  let objectsMap = Map.fromListWith (<>) $ fmap (second nonEmptySingleton . swap) (Map.toList indicesMap)
+  let finalGroups = fmap swap $ Map.toList objectsMap
+  indent 2 (vsep (fmap (\x -> "-" <+> prettyObjectsAndTensorIndices prettyObject name x) finalGroups))

vehicle/src/Vehicle/Prelude/Warning.hs

@@ -6,17 +6,17 @@ module Vehicle.Prelude.Warning
 where
 
 import Data.List (sortBy)
-import Data.List.NonEmpty (NonEmpty, sort)
+import Data.List.NonEmpty (NonEmpty)
 import Data.Map (Map)
 import Data.Map qualified as Map (insertWith, singleton, toList, unionWith)
 import Data.Set (Set)
-import Data.Set qualified as Set (singleton)
 import Data.Tuple (swap)
 import Vehicle.Compile.Context.Bound.Core
 import Vehicle.Data.Assertion
 import Vehicle.Data.Builtin.Core
 import Vehicle.Data.Builtin.Tensor
 import Vehicle.Data.Code.Value
+import Vehicle.Data.Tensor (TensorIndices)
 import Vehicle.Prelude (Name)
 import Vehicle.Resource (ExternalResource)
 import Vehicle.Verify.Core
@@ -36,10 +36,10 @@ data CompileWarning
 data SummarisedCompileWarning
   = UnusedResourcesSummary ExternalResource (Set Name)
   | TrivialPropertySummary PropertyAddress Bool
-  | UnderSpecifiedProblemSpaceVariablesSummary PropertyAddress (Set Name)
-  | UnsoundStrictOrderConversionsSummary QueryFormatID PropertyAddress Int
-  | AllConstantNetworkInputVariablesSummary QueryFormatID PropertyAddress (NonEmpty QueryID)
-  | UnboundedNetworkInputVariablesSummary QueryFormatID PropertyAddress [(NonEmpty QueryID, [(Name, UnderConstrainedVariableStatus)])]
+  | UnderSpecifiedProblemSpaceVariablesSummary PropertyID PropertyName (NonEmpty (Name, TensorIndices))
+  | UnsoundStrictOrderConversionsSummary QueryFormatID PropertyID PropertyName Int
+  | AllConstantNetworkInputVariablesSummary QueryFormatID PropertyID PropertyName (NonEmpty (QueryID, TensorIndices))
+  | UnboundedNetworkInputVariablesSummary QueryFormatID PropertyID PropertyName [(NonEmpty QueryID, [(Name, UnderConstrainedVariableStatus)])]
 
 --------------------------------------------------------------------------------
 -- Combinable compile warnings
@@ -48,10 +48,10 @@ type UnderConstrainedSignature = [(Name, UnderConstrainedVariableStatus)]
 
 data CombiningState = CombiningState
   { uniqueWarnings :: [SummarisedCompileWarning],
-    underSpecifiedProblemSpaceVars :: Map PropertyAddress (Set Name),
-    unsoundStrictnessConversions :: Map (QueryFormatID, PropertyAddress) Int,
-    allConstantNetworkInputVars :: Map (QueryFormatID, PropertyAddress) (NonEmpty QueryID),
-    unboundedNetworkInputs :: Map (QueryFormatID, PropertyAddress) (Map UnderConstrainedSignature (NonEmpty QueryID)),
+    underSpecifiedProblemSpaceVars :: Map (PropertyID, PropertyName) (NonEmpty (Name, TensorIndices)),
+    unsoundStrictnessConversions :: Map (QueryFormatID, PropertyID, PropertyName) Int,
+    allConstantNetworkInputVars :: Map (QueryFormatID, PropertyID, PropertyName) (NonEmpty (QueryID, TensorIndices)),
+    unboundedNetworkInputs :: Map (QueryFormatID, PropertyID, PropertyName) (Map UnderConstrainedSignature (NonEmpty QueryID)),
     inefficientTensorCode :: Map Name [(Builtin, NamedBoundCtx, Value TensorBuiltin)]
   }
 
@@ -70,24 +70,25 @@ addWarningToState CombiningState {..} = \case
       { uniqueWarnings = TrivialPropertySummary r names : uniqueWarnings,
         ..
       }
-  UnderSpecifiedProblemSpaceVar property var ->
+  UnderSpecifiedProblemSpaceVar PropertyAddress {..} var ->
     CombiningState
-      { underSpecifiedProblemSpaceVars = Map.insertWith (<>) property (Set.singleton var) underSpecifiedProblemSpaceVars,
+      { underSpecifiedProblemSpaceVars = Map.insertWith (<>) (propertyID, propertyName) [(var, propertyIndices)] underSpecifiedProblemSpaceVars,
         ..
       }
-  UnsoundStrictOrderConversion queryFormat (propertyAddress, _queryID) ->
+  UnsoundStrictOrderConversion queryFormat (PropertyAddress {..}, _queryID) ->
     CombiningState
-      { unsoundStrictnessConversions = Map.insertWith (+) (queryFormat, propertyAddress) 1 unsoundStrictnessConversions,
+      { unsoundStrictnessConversions = Map.insertWith (+) (queryFormat, propertyID, propertyName) 1 unsoundStrictnessConversions,
         ..
       }
-  AllConstantNetworkInputVars queryFormat (propertyAddress, queryID) ->
+  AllConstantNetworkInputVars queryFormat (PropertyAddress {..}, queryID) ->
     CombiningState
-      { allConstantNetworkInputVars = Map.insertWith (<>) (queryFormat, propertyAddress) [queryID] allConstantNetworkInputVars,
+      { allConstantNetworkInputVars =
+          Map.insertWith (<>) (queryFormat, propertyID, propertyName) [(queryID, propertyIndices)] allConstantNetworkInputVars,
         ..
       }
-  UnboundedNetworkInputVariables queryFormat (propertyAddress, queryID) vars ->
+  UnboundedNetworkInputVariables queryFormat (PropertyAddress {..}, queryID) vars ->
     CombiningState
-      { unboundedNetworkInputs = Map.insertWith (Map.unionWith (<>)) (queryFormat, propertyAddress) (Map.singleton vars [queryID]) unboundedNetworkInputs,
+      { unboundedNetworkInputs = Map.insertWith (Map.unionWith (<>)) (queryFormat, propertyID, propertyName) (Map.singleton vars [queryID]) unboundedNetworkInputs,
         ..
       }
 
@@ -97,36 +98,37 @@ groupWarnings warnings = stateToWarnings $ foldl addWarningToState emptyState wa
 stateToWarnings :: CombiningState -> [SummarisedCompileWarning]
 stateToWarnings CombiningState {..} =
   sortBy compareWarning $
-    do
-      uniqueWarnings
+    uniqueWarnings
       <> fmap combineUnderSpecifiedProblemSpaceVars (Map.toList underSpecifiedProblemSpaceVars)
       <> fmap combineUnsoundStrictnessConversions (Map.toList unsoundStrictnessConversions)
       <> fmap combineAllConstantNetworkInputVars (Map.toList allConstantNetworkInputVars)
       <> fmap combineUnboundedNetworkInputVars (Map.toList unboundedNetworkInputs)
 
-combineUnderSpecifiedProblemSpaceVars :: (PropertyAddress, Set Name) -> SummarisedCompileWarning
-combineUnderSpecifiedProblemSpaceVars (property, vars) = UnderSpecifiedProblemSpaceVariablesSummary property vars
+combineUnderSpecifiedProblemSpaceVars :: ((PropertyID, PropertyName), NonEmpty (Name, TensorIndices)) -> SummarisedCompileWarning
+combineUnderSpecifiedProblemSpaceVars ((propertyID, property), vars) = UnderSpecifiedProblemSpaceVariablesSummary propertyID property vars
 
-combineUnsoundStrictnessConversions :: ((QueryFormatID, PropertyAddress), Int) -> SummarisedCompileWarning
-combineUnsoundStrictnessConversions ((queryFormatID, property), number) = UnsoundStrictOrderConversionsSummary queryFormatID property number
+combineUnsoundStrictnessConversions :: ((QueryFormatID, PropertyID, PropertyName), Int) -> SummarisedCompileWarning
+combineUnsoundStrictnessConversions ((queryFormatID, propertyID, property), number) =
+  UnsoundStrictOrderConversionsSummary queryFormatID propertyID property number
 
-combineAllConstantNetworkInputVars :: ((QueryFormatID, PropertyAddress), NonEmpty QueryID) -> SummarisedCompileWarning
-combineAllConstantNetworkInputVars ((queryFormatID, property), queries) = AllConstantNetworkInputVariablesSummary queryFormatID property (sort queries)
+combineAllConstantNetworkInputVars :: ((QueryFormatID, PropertyID, PropertyName), NonEmpty (QueryID, TensorIndices)) -> SummarisedCompileWarning
+combineAllConstantNetworkInputVars ((queryFormatID, propertyID, property), queries) =
+  AllConstantNetworkInputVariablesSummary queryFormatID propertyID property queries
 
-combineUnboundedNetworkInputVars :: ((QueryFormatID, PropertyAddress), Map UnderConstrainedSignature (NonEmpty QueryID)) -> SummarisedCompileWarning
-combineUnboundedNetworkInputVars ((queryFormatID, property), constraintsBySignature) = do
+combineUnboundedNetworkInputVars :: ((QueryFormatID, PropertyID, PropertyName), Map UnderConstrainedSignature (NonEmpty QueryID)) -> SummarisedCompileWarning
+combineUnboundedNetworkInputVars ((queryFormatID, propertyID, property), constraintsBySignature) = do
   let result = swap <$> Map.toList constraintsBySignature
-  UnboundedNetworkInputVariablesSummary queryFormatID property result
+  UnboundedNetworkInputVariablesSummary queryFormatID propertyID property result
 
 compareWarning :: SummarisedCompileWarning -> SummarisedCompileWarning -> Ordering
 compareWarning w1 w2 = compare (warningPropertyId w1) (warningPropertyId w2)
   where
     warningPropertyId :: SummarisedCompileWarning -> Maybe PropertyID
     warningPropertyId w =
-      propertyID <$> case w of
+      case w of
         UnusedResourcesSummary {} -> Nothing
-        TrivialPropertySummary address _ -> Just address
-        UnderSpecifiedProblemSpaceVariablesSummary address _ -> Just address
-        UnsoundStrictOrderConversionsSummary _ address _ -> Just address
-        AllConstantNetworkInputVariablesSummary _ address _ -> Just address
-        UnboundedNetworkInputVariablesSummary _ address _ -> Just address
+        TrivialPropertySummary address _ -> Just $ propertyID address
+        UnderSpecifiedProblemSpaceVariablesSummary propertyID _ _ -> Just propertyID
+        UnsoundStrictOrderConversionsSummary _ propertyID _ _ -> Just propertyID
+        AllConstantNetworkInputVariablesSummary _ propertyID _ _ -> Just propertyID
+        UnboundedNetworkInputVariablesSummary _ propertyID _ _ -> Just propertyID

vehicle/tests/golden/compile/issue712/MarabouQueries.err.golden

@@ -1,5 +1,6 @@
 
-Warning: In property 'isMalicious', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries.
+Warning: In some of the queries generated by property 'isMalicious' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are:
+  - query 1
 
 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.
 

vehicle/tests/golden/compile/issue765/MarabouQueries.err.golden

@@ -1,5 +1,6 @@
 
-Warning: In property 'p', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries.
+Warning: In some of the queries generated by property 'p' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are:
+  - query 1
 
 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.
 

vehicle/tests/golden/compile/simple-arithmetic/Marabou.err.golden

@@ -1,5 +1,6 @@
 
-Warning: In property 'property', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries.
+Warning: In some of the queries generated by property 'property' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are:
+  - query 1
 
 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.
 

vehicle/tests/golden/compile/simple-constantNetworkInput/Marabou.err.golden

@@ -1,5 +1,6 @@
 
-Warning: In property 'p', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries.
+Warning: In some of the queries generated by property 'p' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are:
+  - query 1
 
 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.
 

vehicle/tests/golden/compile/simple-foreach/Marabou.err.golden

@@ -1,10 +1,6 @@
 
-Warning: In property 'index!0', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries.
-
-See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.
-
-
-Warning: In property 'index!1', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries.
+Warning: In some of the queries generated by property 'index' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are:
+  - query 1 in 'index!0' and 'index!1'
 
 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.