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

Jump to bottom

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 all commits
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 -> return []
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