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.

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

Fix input ordering isses in Verilog generation #1294

Merged
merged 12 commits into from
May 21, 2021
Prev Previous commit
Next Next commit
Better solution to ordering of Verilog CEXs
Instead of ad-hoc reversing in various places, adapt readFiniteValues
to be parameterized by endianness. Typical Verilog ordering, including
in that generated by What4, is little endian.
Aaron Tomb committed May 17, 2021
commit 6afd00ef0c48e7833fe73147a57a493909dc9955
2 changes: 1 addition & 1 deletion deps/what4
Submodule what4 updated 66 files
+1 −6 .github/workflows/test.yml
+4 −0 .gitmodules
+2 −0 cabal.project
+1 −0 dependencies/language-sally
+6 −5 what4-abc/src/What4/Solver/ABC.hs
+4 −4 what4-blt/src/What4/Solver/BLT.hs
+30 −0 what4-transition-system/LICENSE
+174 −0 what4-transition-system/src/What4/TransitionSystem.hs
+112 −0 what4-transition-system/src/What4/TransitionSystem/Exporter/Sally.hs
+237 −0 what4-transition-system/test/Main.hs
+52 −0 what4-transition-system/what4-transition-system.cabal
+349 −53 what4/src/What4/Config.hs
+7 −11 what4/src/What4/Expr/GroundEval.hs
+15 −11 what4/src/What4/Protocol/Online.hs
+16 −2 what4/src/What4/Protocol/SExp.hs
+93 −143 what4/src/What4/Protocol/SMTLib2.hs
+241 −0 what4/src/What4/Protocol/SMTLib2/Response.hs
+42 −8 what4/src/What4/Protocol/SMTWriter.hs
+1 −2 what4/src/What4/Protocol/VerilogWriter.hs
+15 −16 what4/src/What4/Protocol/VerilogWriter/AST.hs
+5 −0 what4/src/What4/Solver.hs
+15 −2 what4/src/What4/Solver/Adapter.hs
+33 −17 what4/src/What4/Solver/Boolector.hs
+53 −22 what4/src/What4/Solver/CVC4.hs
+28 −9 what4/src/What4/Solver/DReal.hs
+21 −7 what4/src/What4/Solver/ExternalABC.hs
+40 −19 what4/src/What4/Solver/STP.hs
+113 −73 what4/src/What4/Solver/Yices.hs
+37 −17 what4/src/What4/Solver/Z3.hs
+490 −26 what4/test/AdapterTest.hs
+599 −0 what4/test/ConfigTest.hs
+2 −2 what4/test/ExprBuilderSMTLib2.hs
+6 −1 what4/test/OnlineSolverTest.hs
+69 −0 what4/test/SolverParserTest.hs
+1 −0 what4/test/responses/err-behav-continue.exp
+1 −0 what4/test/responses/err-behav-continue.rsp
+12 −0 what4/test/responses/err-behav-unrec.exp
+1 −0 what4/test/responses/err-behav-unrec.rsp
+4 −0 what4/test/responses/error_bad.exp
+1 −0 what4/test/responses/error_bad.rsp
+1 −0 what4/test/responses/minisat_verbose_success.exp
+2 −0 what4/test/responses/minisat_verbose_success.rsp
+8 −0 what4/test/responses/minisat_verbose_success.strict.exp
+1 −0 what4/test/responses/name.exp
+1 −0 what4/test/responses/name.rsp
+12 −0 what4/test/responses/rsnunk-bad.exp
+1 −0 what4/test/responses/rsnunk-bad.rsp
+1 −0 what4/test/responses/rsnunk-incomplete.exp
+1 −0 what4/test/responses/rsnunk-incomplete.rsp
+1 −0 what4/test/responses/rsnunk-memout.exp
+1 −0 what4/test/responses/rsnunk-memout.rsp
+1 −0 what4/test/responses/rsnunk-sexp.exp
+1 −0 what4/test/responses/rsnunk-sexp.rsp
+1 −0 what4/test/responses/sat.exp
+1 −0 what4/test/responses/sat.rsp
+1 −0 what4/test/responses/success.exp
+1 −0 what4/test/responses/success.rsp
+1 −0 what4/test/responses/unknown.exp
+1 −0 what4/test/responses/unknown.rsp
+1 −0 what4/test/responses/unsat.exp
+1 −0 what4/test/responses/unsat.rsp
+2 −0 what4/test/responses/unsupported.exp
+1 −0 what4/test/responses/unsupported.rsp
+1 −0 what4/test/responses/version.exp
+1 −0 what4/test/responses/version.rsp
+24 −1 what4/what4.cabal
4 changes: 2 additions & 2 deletions intTests/test_external_abc/test.saw
Original file line number Diff line number Diff line change
@@ -40,5 +40,5 @@ let tupt = {{ \(x:[8]) (y:[8]) -> (x + y, x - y) }};
write_verilog "write_verilog_tupt.v" tupt;

// Check that Verilog counterexamples are in the right order
sr <- sat w4_abc_verilog {{ \(x:[8]) -> \(y:[32]) -> y == 0x81050fff /\ x == 2}};
caseSatResult sr undefined (\t -> prove_print yices {{ t == (0x02, 0x81050fff) }});
sr <- sat w4_abc_verilog {{ \(x:[2][2][8]) -> \(y:[32]) -> y == 0x81050fff /\ x == [[2,3],[4,5]] }};
caseSatResult sr undefined (\t -> prove_print yices {{ t == ([[0x02,0x03],[0x04,0x05]], 0x81050fff) }});
28 changes: 21 additions & 7 deletions saw-core/src/Verifier/SAW/FiniteValue.hs
Original file line number Diff line number Diff line change
@@ -309,27 +309,41 @@ scFirstOrderValue sc fv =

-- Parsing values from lists of booleans ---------------------------------------

readFiniteValue' :: FiniteType -> S.StateT [Bool] Maybe FiniteValue
readFiniteValue' ft =
data Endianness
robdockins marked this conversation as resolved.
Show resolved Hide resolved
= BigEndian
| LittleEndian

readFiniteValue' :: Endianness -> FiniteType -> S.StateT [Bool] Maybe FiniteValue
readFiniteValue' en ft =
case ft of
FTBit -> do bs <- S.get
case bs of
[] -> S.lift Nothing
b : bs' -> S.put bs' >> return (FVBit b)
FTVec n t -> fvVec t <$> S.replicateM (fromIntegral n) (readFiniteValue' t)
FTTuple ts -> FVTuple <$> traverse readFiniteValue' ts
FTRec tm -> FVRec <$> traverse readFiniteValue' tm
FTVec n t -> (fvVec t . fixup) <$> S.replicateM (fromIntegral n) (readFiniteValue' en t)
where fixup = case (t, en) of
(FTBit, LittleEndian) -> reverse
_ -> id
FTTuple ts -> FVTuple <$> traverse (readFiniteValue' en) ts
FTRec tm -> FVRec <$> traverse (readFiniteValue' en) tm

readFiniteValues :: [FiniteType] -> [Bool] -> Maybe [FiniteValue]
readFiniteValues ts bs = do
(vs, rest) <- S.runStateT (traverse readFiniteValue' ts) bs
(vs, rest) <- S.runStateT (traverse (readFiniteValue' BigEndian) ts) bs
case rest of
[] -> return vs
_ -> Nothing

readFiniteValuesLE :: [FiniteType] -> [Bool] -> Maybe [FiniteValue]
readFiniteValuesLE ts bs = do
(vs, rest) <- S.runStateT (traverse (readFiniteValue' LittleEndian) ts) bs
case rest of
[] -> return vs
_ -> Nothing

readFiniteValue :: FiniteType -> [Bool] -> Maybe FiniteValue
readFiniteValue t bs = do
(v, rest) <- S.runStateT (readFiniteValue' t) bs
(v, rest) <- S.runStateT (readFiniteValue' BigEndian t) bs
case rest of
[] -> return v
_ -> Nothing
9 changes: 4 additions & 5 deletions src/SAWScript/Prover/ABC.hs
Original file line number Diff line number Diff line change
@@ -29,7 +29,7 @@ import qualified Verifier.SAW.Simulator.BitBlast as BBSim
import SAWScript.Proof(Prop, propToSATQuery, propSize, goalProp, ProofGoal, goalType, goalNum, CEX)
import SAWScript.Prover.SolverStats (SolverStats, solverStats)
import qualified SAWScript.Prover.Exporter as Exporter
import SAWScript.Prover.Util (liftCexBB)
import SAWScript.Prover.Util (liftCexBB, liftLECexBB)

-- crucible-jvm
-- TODO, very weird import
@@ -105,12 +105,11 @@ w4AbcVerilog unints sc _hashcons goal = liftIO $
let stats = solverStats "abc_verilog" (propSize goal)
res <- if all isSpace cexText
then return Nothing
-- NB: reverse bits to get bit-order convention right
else do bits <- reverse <$> parseAigerCex cexText
case liftCexBB (reverse argTys) bits of
else do bits <- parseAigerCex cexText
case liftLECexBB argTys bits of
Left parseErr -> fail parseErr
Right vs -> return $ Just model
where model = zip argNames (map toFirstOrderValue (reverse vs))
where model = zip argNames (map toFirstOrderValue vs)
return (res, stats)

parseAigerCex :: String -> IO [Bool]
7 changes: 6 additions & 1 deletion src/SAWScript/Prover/Exporter.hs
Original file line number Diff line number Diff line change
@@ -93,7 +93,10 @@ import SAWScript.Prover.What4
import SAWScript.Value

import qualified What4.Expr.Builder as W4
import What4.Config (extendConfig)
import What4.Interface (getConfiguration)
import What4.Protocol.SMTLib2 (writeDefaultSMT2)
import What4.Protocol.SMTLib2.Response (smtParseOptions)
import What4.Protocol.VerilogWriter (exprsVerilog)
import What4.Solver.Adapter
import qualified What4.SWord as W4Sim
@@ -279,8 +282,10 @@ writeSMTLib2What4 :: SharedContext -> FilePath -> SATQuery -> TopLevel ()
writeSMTLib2What4 sc f satq = io $
do sym <- W4.newExprBuilder W4.FloatRealRepr St globalNonceGenerator
(_varMap, lit) <- W.w4Solve sym sc satq
let cfg = getConfiguration sym
extendConfig smtParseOptions cfg
withFile f WriteMode $ \h ->
writeDefaultSMT2 () "Offline SMTLib2" defaultWriteSMTLIB2Features sym h [lit]
writeDefaultSMT2 () "Offline SMTLib2" defaultWriteSMTLIB2Features Nothing sym h [lit]

writeCore :: FilePath -> Term -> TopLevel ()
writeCore path t = io $ writeFile path (scWriteExternal t)
7 changes: 7 additions & 0 deletions src/SAWScript/Prover/Util.hs
Original file line number Diff line number Diff line change
@@ -28,3 +28,10 @@ liftCexBB tys bs =
case readFiniteValues tys bs of
Nothing -> Left "Failed to lift counterexample"
Just fvs -> Right fvs

-- | Lift a counterexample containing little-endian words
liftLECexBB :: [FiniteType] -> [Bool] -> Either String [FiniteValue]
liftLECexBB tys bs =
case readFiniteValuesLE tys bs of
Nothing -> Left "Failed to lift counterexample"
Just fvs -> Right fvs