Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Avoid breaking up bitvectors in Verilog output #1369

Merged
merged 3 commits into from
Jul 14, 2021
Merged

Avoid breaking up bitvectors in Verilog output #1369

Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
3d1b748
Avoid breaking up bitvectors in Verilog output
Jul 6, 2021
4d4e40e
Remove failure case in Verilog export
Jul 8, 2021
6715a14
Merge branch 'master' into at-verilog-lazy-bv
mergify[bot] Jul 14, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 23 additions & 14 deletions src/SAWScript/Prover/Exporter.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think you can probably just return [] here? I think it's better to avoid failure cases if we can.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess the consideration is whether this function should be generic (which it otherwise mostly is) or should be specific to Verilog generation. Verilog doesn't allow vectors of size zero, so in the latter case this is the result we want. At the same time, I also like to avoid failure cases whenever possible... And I'd prefer to do something other than fail.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking at this some more, I think this will fail on empty vectors at any type, which you probably also don't want.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, and now that I look further I think your previous suggestion was right. Returning an empty list for a zero-size bit vector will result in no value on the Verilog side, not an empty value, so it'll be fine. I'll update it so that any zero-size vector will go through okay.

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
Expand All @@ -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
Expand Down