From 3d1b7480fb3f0e845f7bfee03b3adf36e59e090a Mon Sep 17 00:00:00 2001
From: Aaron Tomb <atomb@galois.com>
Date: Tue, 6 Jul 2021 14:23:56 -0700
Subject: [PATCH 1/2] Avoid breaking up bitvectors in Verilog output

---
 src/SAWScript/Prover/Exporter.hs | 37 ++++++++++++++++++++------------
 1 file changed, 23 insertions(+), 14 deletions(-)

diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
index 3caf0fd73b..3ff2a79df8 100644
--- a/src/SAWScript/Prover/Exporter.hs
+++ b/src/SAWScript/Prover/Exporter.hs
@@ -60,6 +60,7 @@ import System.IO
 import System.IO.Temp(emptySystemTempFile)
 import Data.Text (pack)
 import Data.Text.Prettyprint.Doc.Render.Text
+import qualified Data.Vector as V
 import Prettyprinter (vcat)
 
 import Lang.JVM.ProcessUtils (readProcessExitIfFailure)
@@ -94,7 +95,7 @@ import SAWScript.Value
 
 import qualified What4.Expr.Builder as W4
 import What4.Config (extendConfig)
-import What4.Interface (getConfiguration)
+import What4.Interface (getConfiguration, IsSymExprBuilder)
 import What4.Protocol.SMTLib2 (writeDefaultSMT2)
 import What4.Protocol.SMTLib2.Response (smtParseOptions)
 import What4.Protocol.VerilogWriter (exprsVerilog)
@@ -325,7 +326,7 @@ writeVerilogSAT path satq = getSharedContext >>= \sc -> io $
      let argSValues = map (snd . snd) vars
      let argSValueNames = zip argSValues (map (toShortName . ecName) argNames)
      argTys' <- traverse f argTys
-     let mkInput (v, nm) = map (,nm) <$> flattenSValue v
+     let mkInput (v, nm) = map (,nm) <$> flattenSValue sym v
      ins <- concat <$> mapM mkInput argSValueNames
      edoc <- runExceptT $ exprsVerilog sym ins [Some bval] "f"
      case edoc of
@@ -337,20 +338,28 @@ writeVerilogSAT path satq = getSharedContext >>= \sc -> io $
          hClose h
      return (zip argNames argTys')
 
-flattenSValue :: W4Sim.SValue sym -> IO [Some (W4.SymExpr sym)]
-flattenSValue (Sim.VBool b) = return [Some b]
-flattenSValue (Sim.VWord (W4Sim.DBV w)) = return [Some w]
-flattenSValue (Sim.VPair l r) =
+flattenSValue :: IsSymExprBuilder sym => sym -> W4Sim.SValue sym -> IO [Some (W4.SymExpr sym)]
+flattenSValue _ (Sim.VBool b) = return [Some b]
+flattenSValue _ (Sim.VWord (W4Sim.DBV w)) = return [Some w]
+flattenSValue sym (Sim.VPair l r) =
   do lv <- Sim.force l
      rv <- Sim.force r
-     ls <- flattenSValue lv
-     rs <- flattenSValue rv
+     ls <- flattenSValue sym lv
+     rs <- flattenSValue sym rv
      return (ls ++ rs)
-flattenSValue (Sim.VVector ts) =
+flattenSValue sym (Sim.VVector ts) =
   do vs <- mapM Sim.force ts
-     es <- mapM flattenSValue vs
-     return (concat es)
-flattenSValue sval = fail $ "write_verilog: unsupported result type: " ++ show sval
+     let getBool (Sim.VBool b) = Just b
+         getBool _ = Nothing
+         mbs = V.map getBool vs
+     case sequence mbs of
+       Just bs ->
+         do w <- W4Sim.bvPackBE sym bs
+            case w of
+              W4Sim.DBV bv -> return [Some bv]
+              W4Sim.ZBV -> fail "write_verilog: bitvectors of size zero unsupported"
+       Nothing -> concat <$> mapM (flattenSValue sym) vs
+flattenSValue _ sval = fail $ "write_verilog: unsupported result type: " ++ show sval
 
 writeVerilog :: SharedContext -> FilePath -> Term -> IO ()
 writeVerilog sc path t = do
@@ -361,8 +370,8 @@ writeVerilog sc path t = do
   -- order, followed by free variables (probably in the order seen
   -- during traversal, because that's at least _a_ deterministic order).
   (argNames, args, _, sval) <- W4Sim.w4EvalAny sym st sc mempty mempty t
-  es <- flattenSValue sval
-  let mkInput (v, nm) = map (, pack nm) <$> flattenSValue v
+  es <- flattenSValue sym sval
+  let mkInput (v, nm) = map (, pack nm) <$> flattenSValue sym v
   ins <- concat <$> mapM mkInput (zip args argNames)
   edoc <- runExceptT $ exprsVerilog sym ins es "f"
   case edoc of

From 4d4e40e140db94eb29bcc58c27a0df13075ef3f6 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <atomb@galois.com>
Date: Thu, 8 Jul 2021 15:01:26 -0700
Subject: [PATCH 2/2] Remove failure case in Verilog export

Flattening a value containing an empty bit vector is now valid. It
simply won't appear in the list of output values.
---
 src/SAWScript/Prover/Exporter.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
index 3ff2a79df8..cde90c1218 100644
--- a/src/SAWScript/Prover/Exporter.hs
+++ b/src/SAWScript/Prover/Exporter.hs
@@ -357,7 +357,7 @@ flattenSValue sym (Sim.VVector ts) =
          do w <- W4Sim.bvPackBE sym bs
             case w of
               W4Sim.DBV bv -> return [Some bv]
-              W4Sim.ZBV -> fail "write_verilog: bitvectors of size zero unsupported"
+              W4Sim.ZBV -> return []
        Nothing -> concat <$> mapM (flattenSValue sym) vs
 flattenSValue _ sval = fail $ "write_verilog: unsupported result type: " ++ show sval