Do the right thing when encountering 0 width bitvectors in the What4 …

…backend.

Fixes the root cause of GaloisInc/saw-script#872

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

@@ -925,7 +925,7 @@ vAsFirstOrderType v =
     _ -> Nothing
 
 valueAsBaseType :: IsSymExprBuilder sym => TValue (What4 sym) -> Maybe (Some W.BaseTypeRepr)
-valueAsBaseType v = fmap fotToBaseType $ vAsFirstOrderType v
+valueAsBaseType v = fotToBaseType =<< vAsFirstOrderType v
 
 ------------------------------------------------------------------------------
 
@@ -974,6 +974,7 @@ myfun = fmap fst A.&&& fmap snd
 
 data Labeler sym
   = BaseLabel (TypedExpr sym)
+  | ZeroWidthBVLabel
   | IntModLabel Natural (SymInteger sym)
   | VecLabel (Vector (Labeler sym))
   | TupleLabel (Vector (Labeler sym))
@@ -988,6 +989,9 @@ newVarFOT sym (FOTTuple ts) = do
   args <- traverse (return . ready) (V.toList vals)
   return (TupleLabel labels, vTuple args)
 
+newVarFOT _sym (FOTVec 0 FOTBit)
+  = return (ZeroWidthBVLabel, VWord ZBV)
+
 newVarFOT sym (FOTVec n tp)
   | tp /= FOTBit
   = do (labels,vals) <- V.unzip <$> V.replicateM (fromIntegral n) (newVarFOT sym tp)
@@ -1006,17 +1010,18 @@ newVarFOT sym (FOTIntMod n)
        return (IntModLabel n si, VIntMod n si)
 
 newVarFOT sym fot
-  | Some r <- fotToBaseType fot
+  | Just (Some r) <- fotToBaseType fot
   = do nm <- nextId
        te <- lift $ freshVar sym r nm
        sv <- lift $ typedToSValue te
        return (BaseLabel te, sv)
-
+  | otherwise
+  = fail ("Cannot create What4 variable of type: " ++ show fot)
 
 
 typedToSValue :: (IsExpr (SymExpr sym)) => TypedExpr sym -> IO (SValue sym)
 typedToSValue (TypedExpr ty expr) =
-  maybe (fail "Cannot handle") return $ symExprToValue ty expr
+  maybe (fail ("Cannot handle " ++ show ty)) return $ symExprToValue ty expr
 
 getLabelValues ::
   forall sym t.
@@ -1033,6 +1038,7 @@ getLabelValues f =
       FOVRec <$> traverse (getLabelValues f) labels
     IntModLabel n x ->
       FOVIntMod n <$> groundEval f x
+    ZeroWidthBVLabel -> pure $ FOVWord 0 0
     BaseLabel (TypedExpr ty bv) ->
       do gv <- groundEval f bv
          case (groundToFOV ty gv) of

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

@@ -43,36 +43,38 @@ import What4.Expr.GroundEval
 ---------------------------------------------------------------------
 
 -- | Convert a type expression from SAW-core to What4
-fotToBaseType :: FirstOrderType -> Some BaseTypeRepr
+fotToBaseType :: FirstOrderType -> Maybe (Some BaseTypeRepr)
 fotToBaseType FOTBit
-  = Some BaseBoolRepr
+  = Just (Some BaseBoolRepr)
 fotToBaseType FOTInt
-  = Some BaseIntegerRepr
+  = Just (Some BaseIntegerRepr)
 fotToBaseType (FOTIntMod _n)
-  = Some BaseIntegerRepr
+  = Just (Some BaseIntegerRepr)
 fotToBaseType (FOTVec nat FOTBit)
   | Just (Some (PosNat nr)) <- somePosNat nat
-  = Some (BaseBVRepr nr)
-  | otherwise  -- 0-width bit vector is 0
-  = Some BaseIntegerRepr
+  = Just (Some (BaseBVRepr nr))
+  | otherwise = Nothing
+
 fotToBaseType (FOTVec nat fot)
-  | Some assn <- listToAssn (replicate (fromIntegral nat) fot)
-  = Some (BaseStructRepr assn)
+  | Just (Some assn) <- listToAssn (replicate (fromIntegral nat) fot)
+  = Just (Some (BaseStructRepr assn))
 fotToBaseType (FOTArray fot1 fot2)
-  | Some ty1 <- fotToBaseType fot1
-  , Some ty2 <- fotToBaseType fot2
-  = Some $ BaseArrayRepr (Empty :> ty1) ty2
+  | Just (Some ty1) <- fotToBaseType fot1
+  , Just (Some ty2) <- fotToBaseType fot2
+  = Just (Some (BaseArrayRepr (Empty :> ty1) ty2))
 fotToBaseType (FOTTuple fots)
-  | Some assn <- listToAssn fots
-  = Some (BaseStructRepr assn)
-fotToBaseType (FOTRec _)
-  = error "TODO: convert to What4 records ?!"
+  | Just (Some assn) <- listToAssn fots
+  = Just (Some (BaseStructRepr assn))
+
+-- TODO: convert to What4 records ?!
+fotToBaseType _ = Nothing
 
-listToAssn :: [FirstOrderType] -> Some (Assignment BaseTypeRepr)
-listToAssn [] = Some empty
+listToAssn :: [FirstOrderType] -> Maybe (Some (Assignment BaseTypeRepr))
+listToAssn [] = Just (Some empty)
 listToAssn (fot:rest) =
   case (fotToBaseType fot, listToAssn rest) of
-    (Some bt, Some assn) -> Some $ extend assn bt
+    (Just (Some bt), Just (Some assn)) -> Just (Some (extend assn bt))
+    _ -> Nothing
 
 ---------------------------------------------------------------------
 -- | Convert a type expression from What4 to SAW-core