Throw exception when symbolically evaluating enum values

GaloisInc · Jan 23, 2024 · 0a3a2e1 · 0a3a2e1
1 parent f0706f9
commit 0a3a2e1
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 3 deletions.
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
@@ -24,6 +24,7 @@ module Cryptol.Symbolic
  , ProverResult(..)
  , ProverStats
  , CounterExampleType(..)
+ , SymbolicException(..)
    -- * FinType
  , FinType(..)
  , FinNewtype(..)
@@ -44,6 +45,7 @@ module Cryptol.Symbolic
  ) where
 
 
+import qualified Control.Exception as X
 import Control.Monad (foldM)
 import Data.Map(Map)
 import Data.IORef(IORef)
@@ -120,7 +122,13 @@ data ProverResult = AllSatResult [SatResult] -- LAZY
                   | EmptyResult
                   | ProverError  String
 
+data SymbolicException = UnsupportedEnums
 
+instance Show SymbolicException where
+  showsPrec _ UnsupportedEnums =
+    showString "Enums are not currently supported with symbolic evaluation."
+
+instance X.Exception SymbolicException
 
 predArgTypes :: QueryType -> Schema -> Either String [FinType]
 predArgTypes qtype schema@(Forall ts ps ty)
@@ -294,7 +302,7 @@ freshVar fns tp =
     FTNewtype _ _ nv ->
       case nv of
         FStruct fs -> VarRecord <$> traverse (freshVar fns) fs
-        -- XXX: FEnum
+        FEnum{} -> X.throw UnsupportedEnums
 
 computeModel ::
   PrimMap ->

diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs
@@ -535,8 +535,10 @@ parseValue (FTRecord r) cvs = (VarRecord r', cvs')
         fs         = zip ns vs
         r'         = recordFromFieldsWithDisplay (displayOrder r) fs
 
-parseValue (FTNewtype _ _ (FStruct r)) cvs = parseValue (FTRecord r) cvs
---- XXX: Enum
+parseValue (FTNewtype _ _ nv) cvs =
+  case nv of
+    FStruct r -> parseValue (FTRecord r) cvs
+    FEnum{} -> X.throw UnsupportedEnums
 
 parseValue (FTFloat e p) cvs =
    (VarFloat FH.BF { FH.bfValue = bfNaN