Remove use of partial fields and add warning.

Partial fields are the situation where an ADT is defined with record
syntax.  The field accessors are of type `ADT -> field`, but the field
is only valid for one constructor of the ADT, so proper usage requires
matching on the constructor before using field accessors, and omitting
this matching can lead to invalid accesses.

This change modifies the only use of this in What4 to ensure that the
Record types are not ADT's and vice-versa.

what4/src/What4/Interface.hs

@@ -79,6 +79,8 @@ module What4.Interface
   , IsExprBuilder(..)
   , IsSymExprBuilder(..)
   , SolverEvent(..)
+  , SolverStartSATQuery(..)
+  , SolverEndSATQuery(..)
 
     -- ** Bitvector operations
   , bvJoinVector
@@ -392,11 +394,17 @@ instance HashableF e => HashableF (ArrayResultWrapper e idx) where
 --   installed via @setSolverLogListener@ whenever an interesting
 --   event occurs.
 data SolverEvent
-  = SolverStartSATQuery
+  = SolverStartSATQuery SolverStartSATQuery
+  | SolverEndSATQuery SolverEndSATQuery
+ deriving (Show, Generic)
+
+data SolverStartSATQuery = SolverStartSATQueryRec
     { satQuerySolverName :: !String
     , satQueryReason     :: !String
     }
-  | SolverEndSATQuery
+ deriving (Show, Generic)
+
+data SolverEndSATQuery = SolverEndSATQueryRec
     { satQueryResult     :: !(SatResult () ())
     , satQueryError      :: !(Maybe String)
     }

what4/src/What4/Protocol/Online.hs

@@ -58,7 +58,9 @@ import           System.Process
                    (ProcessHandle, terminateProcess, waitForProcess)
 
 import           What4.Expr
-import           What4.Interface (SolverEvent(..))
+import           What4.Interface (SolverEvent(..)
+                                 , SolverStartSATQuery(..)
+                                 , SolverEndSATQuery(..) )
 import           What4.ProblemFeatures
 import           What4.Protocol.SMTWriter
 import           What4.SatResult
@@ -320,17 +322,17 @@ checkWithAssumptions proc rsn ps =
          do tms <- forM ps (mkFormula conn)
             nms <- forM tms (freshBoundVarName conn EqualityDefinition [] BoolTypeMap)
             solverLogFn proc
-              SolverStartSATQuery
+              (SolverStartSATQuery $ SolverStartSATQueryRec
               { satQuerySolverName = solverName proc
               , satQueryReason = rsn
-              }
+              })
             addCommands conn (checkWithAssumptionsCommands conn nms)
             sat_result <- getSatResult proc
             solverLogFn proc
-              SolverEndSATQuery
+              (SolverEndSATQuery $ SolverEndSATQueryRec
               { satQueryResult = sat_result
               , satQueryError = Nothing
-              }
+              })
             return (nms, sat_result)
 
 checkWithAssumptionsAndModel ::
@@ -355,17 +357,17 @@ check p rsn =
     Nothing ->
       do let c = solverConn p
          solverLogFn p
-           SolverStartSATQuery
+           (SolverStartSATQuery $ SolverStartSATQueryRec
            { satQuerySolverName = solverName p
            , satQueryReason = rsn
-           }
+           })
          addCommands c (checkCommands c)
          sat_result <- getSatResult p
          solverLogFn p
-           SolverEndSATQuery
+           (SolverEndSATQuery $ SolverEndSATQueryRec
            { satQueryResult = sat_result
            , satQueryError = Nothing
-           }
+           })
          return sat_result
 
 -- | Send a check command to the solver and get the model in the case of a SAT result.

what4/src/What4/Protocol/SMTLib2.hs

@@ -1051,10 +1051,10 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
     -> IO b
   runSolverInOverride solver ack feats sym logData predicates cont = do
     I.logSolverEvent sym
-      I.SolverStartSATQuery
+      (I.SolverStartSATQuery $ I.SolverStartSATQueryRec
         { I.satQuerySolverName = show solver
         , I.satQueryReason     = logReason logData
-        }
+        })
     path <- defaultSolverPath solver sym
     withSolver solver ack feats sym path (logData{logVerbosity=2}) $ \session -> do
       -- Assume the predicates hold.
@@ -1062,10 +1062,10 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
       -- Run check SAT and get the model back.
       runCheckSat session $ \result -> do
         I.logSolverEvent sym
-          I.SolverEndSATQuery
+          (I.SolverEndSATQuery $ I.SolverEndSATQueryRec
             { I.satQueryResult = forgetModelAndCore result
             , I.satQueryError  = Nothing
-            }
+            })
         cont result
 
 -- | A default method for writing SMTLib2 problems without any

what4/src/What4/Solver/DReal.hs

@@ -275,10 +275,10 @@ runDRealInOverride sym logData ps modelFn = do
   p <- andAllOf sym folded ps
   solver_path <- findSolverPath drealPath (getConfiguration sym)
   logSolverEvent sym
-    SolverStartSATQuery
+    (SolverStartSATQuery $ SolverStartSATQueryRec
     { satQuerySolverName = "dReal"
     , satQueryReason = logReason logData
-    }
+    })
   withProcessHandles solver_path ["--model", "--in", "--format", "smt2"] Nothing $ \(in_h, out_h, err_h, ph) -> do
 
       -- Log stderr to output.
@@ -338,10 +338,10 @@ runDRealInOverride sym logData ps modelFn = do
           logCallbackVerbose logData 2 "dReal terminated."
 
           logSolverEvent sym
-             SolverEndSATQuery
+             (SolverEndSATQuery $ SolverEndSATQueryRec
              { satQueryResult = forgetModelAndCore res
              , satQueryError  = Nothing
-             }
+             })
 
           return r
         ExitFailure exit_code ->

what4/src/What4/Solver/Yices.hs

@@ -1113,10 +1113,10 @@ runYicesInOverride sym logData conditions resultFn = do
   logCallbackVerbose logData 2 "Calling Yices to check sat"
   -- Check Problem features
   logSolverEvent sym
-    SolverStartSATQuery
+    (SolverStartSATQuery $ SolverStartSATQueryRec
     { satQuerySolverName = "Yices"
     , satQueryReason = logReason logData
-    }
+    })
   features <- checkSupportedByYices condition
   enableMCSat <- getOpt =<< getOptionSetting yicesEnableMCSat cfg
   goalTimeout <- SolverGoalTimeout <$> (getOpt =<< getOptionSetting yicesGoalTimeout cfg)
@@ -1168,10 +1168,10 @@ runYicesInOverride sym logData conditions resultFn = do
                              }
       sat_result <- getSatResult yp
       logSolverEvent sym
-        SolverEndSATQuery
+        (SolverEndSATQuery $ SolverEndSATQueryRec
         { satQueryResult = sat_result
         , satQueryError  = Nothing
-        }
+        })
       r <-
          case sat_result of
            Sat () -> resultFn . Sat =<< getModel yp

what4/what4.cabal

@@ -58,6 +58,7 @@ common bldflags
                -Werror=missing-methods
                -Werror=overlapping-patterns
                -Wcompat
+               -Wpartial-fields
 
 common testdefs
   hs-source-dirs: test