Make freshVar produce a VWord instead of a VSeq for type [0].

Fixes #1093. Fixes #1094.
GaloisInc · Mar 2, 2021 · 4735117 · 4735117
1 parent 665b1c7
commit 4735117
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 3 deletions.
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
@@ -241,7 +241,8 @@ data FreshVarFns sym =
   }
 
 freshVar :: Backend sym => FreshVarFns sym -> FinType -> IO (VarShape sym)
-freshVar fns tp = case tp of
+freshVar fns tp =
+  case tp of
     FTBit         -> VarBit      <$> freshBitVar fns
     FTInteger     -> VarInteger  <$> freshIntegerVar fns Nothing Nothing
     FTRational    -> VarRational
@@ -250,7 +251,7 @@ freshVar fns tp = case tp of
     FTIntMod 0    -> panic "freshVariable" ["0 modulus not allowed"]
     FTIntMod m    -> VarInteger  <$> freshIntegerVar fns (Just 0) (Just (m-1))
     FTFloat e p   -> VarFloat    <$> freshFloatVar fns e p
-    FTSeq n FTBit | n > 0 -> VarWord     <$> freshWordVar fns (toInteger n)
+    FTSeq n FTBit -> VarWord     <$> freshWordVar fns (toInteger n)
     FTSeq n t     -> VarFinSeq (toInteger n) <$> sequence (genericReplicate n (freshVar fns t))
     FTTuple ts    -> VarTuple    <$> mapM (freshVar fns) ts
     FTRecord fs   -> VarRecord   <$> traverse (freshVar fns) fs

diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs
@@ -540,11 +540,16 @@ freshBoundedInt sym lo hi =
        Nothing -> pure ()
      return x
 
+freshBitvector :: SBV -> Integer -> IO SBV.SVal
+freshBitvector sym w
+  | w == 0 = pure (SBV.svInteger (SBV.KBounded False 0) 0)
+  | otherwise = freshBV_ sym (fromInteger w)
+
 sbvFreshFns :: SBV -> FreshVarFns SBV
 sbvFreshFns sym =
   FreshVarFns
   { freshBitVar     = freshSBool_ sym
-  , freshWordVar    = freshBV_ sym . fromInteger
+  , freshWordVar    = freshBitvector sym
   , freshIntegerVar = freshBoundedInt sym
   , freshFloatVar   = \_ _ -> return () -- TODO
   }