From 6388dbe96ab74a75369410ee4e28fdf4527741ed Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 20 May 2016 13:31:34 -0700 Subject: [PATCH] New ProofState type allows proofs with multiple subgoals The success/failure of a proof script is now encoded in whether or not it finished with no remaining subgoals. This is a small step toward addressing issue #9. --- src/SAWScript/Builtins.hs | 160 ++++++++++++++++++++-------------- src/SAWScript/JavaBuiltins.hs | 2 +- src/SAWScript/LLVMBuiltins.hs | 2 +- src/SAWScript/Proof.hs | 17 ++++ src/SAWScript/Value.hs | 6 +- 5 files changed, 117 insertions(+), 70 deletions(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 3db9c9f8dc..0be33c496b 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -405,8 +405,19 @@ readCore path = do sc <- getSharedContext io (mkTypedTerm sc =<< scReadExternal sc =<< readFile path) +withFirstGoal :: (ProofGoal s -> TopLevel (a, Maybe (ProofGoal s))) -> ProofScript s a +withFirstGoal f = + StateT $ \(ProofState goals concl) -> + case goals of + [] -> fail "ProofScript failed: no subgoal" + g : gs -> do + (x, mg') <- f g + case mg' of + Nothing -> return (x, ProofState gs concl) + Just g' -> return (x, ProofState (g' : gs) concl) + quickcheckGoal :: SharedContext s -> Integer -> ProofScript s SV.SatResult -quickcheckGoal sc n = StateT $ \goal -> io $ do +quickcheckGoal sc n = withFirstGoal $ \goal -> io $ do putStr $ "WARNING: using quickcheck to prove goal..." hFlush stdout let tm = goalTerm goal @@ -418,26 +429,26 @@ quickcheckGoal sc n = StateT $ \goal -> io $ do case result of Nothing -> do putStrLn $ "checked " ++ show n ++ " cases." - return (SV.Unsat, goal) + return (SV.Unsat, Nothing) -- TODO: use reasonable names here - Just cex -> return (SV.SatMulti (zip (repeat "_") cex), goal) + Just cex -> return (SV.SatMulti (zip (repeat "_") cex), Just goal) Nothing -> fail $ "quickcheck:\n" ++ "term has non-testable type" assumeValid :: ProofScript s SV.ProofResult -assumeValid = StateT $ \goal -> do +assumeValid = withFirstGoal $ \goal -> do io $ putStrLn $ "WARNING: assuming goal " ++ goalName goal ++ " is valid" - return (SV.Valid, goal) + return (SV.Valid, Nothing) assumeUnsat :: ProofScript s SV.SatResult -assumeUnsat = StateT $ \goal -> do +assumeUnsat = withFirstGoal $ \goal -> do io $ putStrLn $ "WARNING: assuming goal " ++ goalName goal ++ " is unsat" - return (SV.Unsat, goal) + return (SV.Unsat, Nothing) trivial :: ProofScript SAWCtx SV.SatResult -trivial = StateT $ \goal -> do +trivial = withFirstGoal $ \goal -> do checkTrue (goalTerm goal) - return (SV.Unsat, goal) + return (SV.Unsat, Nothing) where checkTrue :: SharedTerm SAWCtx -> TopLevel () checkTrue t = @@ -467,49 +478,49 @@ print_term_depth d t = do io $ print (ppTermDepth opts d t) printGoal :: ProofScript s () -printGoal = StateT $ \goal -> do +printGoal = withFirstGoal $ \goal -> do opts <- getTopLevelPPOpts io $ putStrLn (scPrettyTerm opts (goalTerm goal)) - return ((), goal) + return ((), Just goal) printGoalDepth :: Int -> ProofScript SAWCtx () -printGoalDepth n = StateT $ \goal -> do +printGoalDepth n = withFirstGoal $ \goal -> do opts <- getTopLevelPPOpts io $ print (ppTermDepth opts n (goalTerm goal)) - return ((), goal) + return ((), Just goal) printGoalConsts :: ProofScript SAWCtx () -printGoalConsts = StateT $ \goal -> do +printGoalConsts = withFirstGoal $ \goal -> do io $ mapM_ putStrLn $ Map.keys (getConstantSet (goalTerm goal)) - return ((), goal) + return ((), Just goal) printGoalSize :: ProofScript SAWCtx () -printGoalSize = StateT $ \goal -> do +printGoalSize = withFirstGoal $ \goal -> do let t = goalTerm goal io $ putStrLn $ "Goal shared size: " ++ show (scSharedSize t) io $ putStrLn $ "Goal unshared size: " ++ show (scTreeSize t) - return ((), goal) + return ((), Just goal) unfoldGoal :: [String] -> ProofScript SAWCtx () -unfoldGoal names = StateT $ \goal -> do +unfoldGoal names = withFirstGoal $ \goal -> do sc <- getSharedContext let trm = goalTerm goal trm' <- io $ scUnfoldConstants sc names trm - return ((), goal { goalTerm = trm' }) + return ((), Just (goal { goalTerm = trm' })) simplifyGoal :: Simpset (SharedTerm SAWCtx) -> ProofScript SAWCtx () -simplifyGoal ss = StateT $ \goal -> do +simplifyGoal ss = withFirstGoal $ \goal -> do sc <- getSharedContext let trm = goalTerm goal trm' <- io $ rewriteSharedTerm sc ss trm - return ((), goal { goalTerm = trm' }) + return ((), Just (goal { goalTerm = trm' })) beta_reduce_goal :: ProofScript SAWCtx () -beta_reduce_goal = StateT $ \goal -> do +beta_reduce_goal = withFirstGoal $ \goal -> do sc <- getSharedContext let trm = goalTerm goal trm' <- io $ betaNormalize sc trm - return ((), goal { goalTerm = trm' }) + return ((), Just (goal { goalTerm = trm' })) -- | Bit-blast a @SharedTerm@ representing a theorem and check its -- satisfiability using ABC. @@ -570,7 +581,7 @@ checkBooleanSchema s = -- | Bit-blast a @SharedTerm@ representing a theorem and check its -- satisfiability using ABC. satABC :: SharedContext s -> ProofScript s SV.SatResult -satABC sc = StateT $ \g -> io $ do +satABC sc = withFirstGoal $ \g -> io $ do let t0 = goalTerm g TypedTerm schema t <- (bindAllExts sc t0 >>= rewriteEqs sc >>= mkTypedTerm sc) checkBooleanSchema schema @@ -584,20 +595,23 @@ satABC sc = StateT $ \g -> io $ do Universal -> AIG.not lit0 -- putStrLn "Checking..." satRes <- AIG.checkSat be lit + ft <- scApplyPrelude_False sc case satRes of - AIG.Unsat -> do - -- putStrLn "UNSAT" - ft <- scApplyPrelude_False sc - return (SV.Unsat, g { goalTerm = ft }) + AIG.Unsat -> + case goalQuant g of + Existential -> return (SV.Unsat, Just (g { goalTerm = ft })) + Universal -> return (SV.Unsat, Nothing) AIG.Sat cex -> do -- putStrLn "SAT" let r = liftCexBB shapes cex - tt <- scApplyPrelude_True sc case r of Left err -> fail $ "Can't parse counterexample: " ++ err Right vs | length argNames == length vs -> do - return (SV.SatMulti (zip argNames vs), g { goalTerm = tt }) + let r' = SV.SatMulti (zip argNames vs) + case goalQuant g of + Existential -> return (r', Nothing) + Universal -> return (r', Just (g { goalTerm = ft })) | otherwise -> fail $ unwords ["ABC SAT results do not match expected arguments", show argNames, show vs] AIG.SatUnknown -> fail "Unknown result from ABC" @@ -615,7 +629,7 @@ parseDimacsSolution vars ls = map lkup vars satExternal :: Bool -> SharedContext s -> String -> [String] -> ProofScript s SV.SatResult -satExternal doCNF sc execName args = StateT $ \g -> io $ do +satExternal doCNF sc execName args = withFirstGoal $ \g -> io $ do t <- rewriteEqs sc (goalTerm g) tp <- scWhnf sc =<< scTypeOf sc t let cnfName = goalName g ++ ".cnf" @@ -638,20 +652,24 @@ satExternal doCNF sc execName args = StateT $ \g -> io $ do let ls = lines out sls = filter ("s " `isPrefixOf`) ls vls = filter ("v " `isPrefixOf`) ls + ft <- scApplyPrelude_False sc case (sls, vls) of (["s SATISFIABLE"], _) -> do let bs = parseDimacsSolution vars vls let r = liftCexBB shapes bs - tt <- scApplyPrelude_True sc case r of Left msg -> fail $ "Can't parse counterexample: " ++ msg Right vs | length argNames == length vs -> do - return (SV.SatMulti (zip argNames vs), g { goalTerm = tt }) + let r' = SV.SatMulti (zip argNames vs) + case goalQuant g of + Universal -> return (r', Just (g { goalTerm = ft })) + Existential -> return (r', Nothing) | otherwise -> fail $ unwords ["external SAT results do not match expected arguments", show argNames, show vs] - (["s UNSATISFIABLE"], []) -> do - ft <- scApplyPrelude_False sc - return (SV.Unsat, g { goalTerm = ft }) + (["s UNSATISFIABLE"], []) -> + case goalQuant g of + Universal -> return (SV.Unsat, Nothing) + Existential -> return (SV.Unsat, Just (g { goalTerm = ft })) _ -> fail $ "Unexpected result from SAT solver:\n" ++ out writeAIGWithMapping :: GIA.GIA s -> GIA.Lit s -> FilePath -> IO [Int] @@ -660,12 +678,6 @@ writeAIGWithMapping be l path = do ABC.writeAiger path (ABC.Network be [l]) return [1..nins] -unsatResult :: SharedContext s -> ProofGoal s - -> IO (SV.SatResult, ProofGoal s) -unsatResult sc g = do - ft <- scApplyPrelude_False sc - return (SV.Unsat, g { goalTerm = ft }) - rewriteEqs :: SharedContext s -> SharedTerm s -> IO (SharedTerm s) rewriteEqs sc t = do let eqs = map (mkIdent preludeName) @@ -679,7 +691,7 @@ rewriteEqs sc t = do -- | Bit-blast a @SharedTerm@ representing a theorem and check its -- satisfiability using the RME library. satRME :: SharedContext s -> ProofScript s SV.SatResult -satRME sc = StateT $ \g -> io $ do +satRME sc = withFirstGoal $ \g -> io $ do let t0 = goalTerm g TypedTerm schema t <- (bindAllExts sc t0 >>= rewriteEqs sc >>= mkTypedTerm sc) checkBooleanSchema schema @@ -693,22 +705,25 @@ satRME sc = StateT $ \g -> io $ do Universal -> RME.compl lit0 -- putStrLn "Checking..." case RME.sat lit of - Nothing -> do - -- putStrLn "UNSAT" - ft <- scApplyPrelude_False sc - return (SV.Unsat, g { goalTerm = ft }) + Nothing -> + case goalQuant g of + Existential -> do ft <- scApplyPrelude_False sc + return (SV.Unsat, Just (g { goalTerm = ft })) + Universal -> return (SV.Unsat, Nothing) Just cex -> do -- putStrLn "SAT" let m = Map.fromList cex let n = sum (map sizeFiniteType shapes) let bs = map (maybe False id . flip Map.lookup m) $ take n [0..] let r = liftCexBB shapes bs - tt <- scApplyPrelude_True sc case r of Left err -> fail $ "Can't parse counterexample: " ++ err Right vs | length argNames == length vs -> do - return (SV.SatMulti (zip argNames vs), g { goalTerm = tt }) + let r' = SV.SatMulti (zip argNames vs) + case goalQuant g of + Existential -> return (r', Nothing) + Universal -> return (r', Just g) | otherwise -> fail $ unwords ["RME SAT results do not match expected arguments", show argNames, show vs] codegenSBV :: SharedContext s -> FilePath -> String -> TypedTerm s -> IO () @@ -736,7 +751,7 @@ satSBV conf sc = satUnintSBV conf sc [] -- satisfiability using SBV. (Currently ignores satisfying assignments.) -- Constants with names in @unints@ are kept as uninterpreted functions. satUnintSBV :: SBV.SMTConfig -> SharedContext s -> [String] -> ProofScript s SV.SatResult -satUnintSBV conf sc unints = StateT $ \g -> io $ do +satUnintSBV conf sc unints = withFirstGoal $ \g -> io $ do (t', labels, lit0) <- prepSBV sc unints (goalTerm g) let lit = case goalQuant g of Existential -> lit0 @@ -747,12 +762,17 @@ satUnintSBV conf sc unints = StateT $ \g -> io $ do SBV.SatResult r <- SBV.satWith conf lit case r of SBV.Satisfiable {} -> do - tt <- scApplyPrelude_True sc + ft <- scApplyPrelude_False sc let dict = SBV.getModelDictionary r - return (getLabels labels dict argNames, g {goalTerm = tt}) + r' = getLabels labels dict argNames + case goalQuant g of + Existential -> return (r', Nothing) + Universal -> return (r', Just (g { goalTerm = ft })) SBV.Unsatisfiable {} -> do ft <- scApplyPrelude_False sc - return (SV.Unsat, g { goalTerm = ft }) + case goalQuant g of + Existential -> return (SV.Unsat, Just (g { goalTerm = ft })) + Universal -> return (SV.Unsat, Nothing) SBV.Unknown {} -> fail "Prover returned Unknown" SBV.ProofError _ ls -> fail . unlines $ "Prover returned error: " : ls SBV.TimeOut {} -> fail "Prover timed out" @@ -825,12 +845,14 @@ satWithExporter :: (SharedContext s -> FilePath -> SharedTerm s -> IO ()) -> String -> String -> ProofScript s SV.SatResult -satWithExporter exporter sc path ext = StateT $ \g -> io $ do +satWithExporter exporter sc path ext = withFirstGoal $ \g -> io $ do t <- case goalQuant g of Existential -> return (goalTerm g) Universal -> negTerm sc (goalTerm g) exporter sc ((path ++ goalName g) ++ ext) t - unsatResult sc g + case goalQuant g of + Existential -> return (SV.Unsat, Just g) + Universal -> return (SV.Unsat, Nothing) satAIG :: SharedContext s -> FilePath -> ProofScript s SV.SatResult satAIG sc path = satWithExporter writeAIG sc path ".aig" @@ -856,23 +878,28 @@ provePrim :: ProofScript SAWCtx SV.SatResult -> TypedTerm SAWCtx -> TopLevel SV.ProofResult provePrim script t = do io $ checkBooleanSchema (ttSchema t) - r <- evalStateT script (ProofGoal Universal "prove" (ttTerm t)) + (r, pstate) <- runStateT script (startProof (ProofGoal Universal "prove" (ttTerm t))) + case finishProof pstate of + Just _ -> return () + Nothing -> io $ putStrLn $ "prove: " ++ show (length (psGoals pstate)) ++ " unsolved subgoal(s)" return (SV.flipSatResult r) provePrintPrim :: ProofScript SAWCtx SV.SatResult -> TypedTerm SAWCtx -> TopLevel (Theorem SAWCtx) provePrintPrim script t = do - r <- provePrim script t + (r, pstate) <- runStateT script (startProof (ProofGoal Universal "prove" (ttTerm t))) opts <- rwPPOpts <$> getTopLevelRW - case r of - SV.Valid -> io (putStrLn "Valid") >> return (Theorem (ttTerm t)) - _ -> fail (SV.showsProofResult opts r "") + case finishProof pstate of + Just thm -> do io $ putStrLn "Valid" + return thm + Nothing -> fail $ "prove: " ++ show (length (psGoals pstate)) ++ " unsolved subgoal(s)\n" + ++ SV.showsProofResult opts (SV.flipSatResult r) "" satPrim :: ProofScript SAWCtx SV.SatResult -> TypedTerm SAWCtx -> TopLevel SV.SatResult satPrim script t = do io $ checkBooleanSchema (ttSchema t) - evalStateT script (ProofGoal Existential "sat" (ttTerm t)) + evalStateT script (startProof (ProofGoal Existential "sat" (ttTerm t))) satPrintPrim :: ProofScript SAWCtx SV.SatResult -> TypedTerm SAWCtx -> TopLevel () @@ -1085,8 +1112,10 @@ exitPrim code = Exit.exitWith exitCode timePrim :: TopLevel SV.Value -> TopLevel SV.Value timePrim a = do t1 <- liftIO $ getCurrentTime + --liftIO $ print t1 r <- a t2 <- liftIO $ getCurrentTime + --liftIO $ print t2 let diff = diffUTCTime t2 t1 liftIO $ printf "Time: %s\n" (show diff) return r @@ -1189,12 +1218,13 @@ parse_core input = do prove_core :: ProofScript SAWCtx SV.SatResult -> String -> TopLevel (Theorem SAWCtx) prove_core script input = do t <- parseCore input - r' <- evalStateT script (ProofGoal Universal "prove" t) + (r', pstate) <- runStateT script (startProof (ProofGoal Universal "prove" t)) let r = SV.flipSatResult r' opts <- rwPPOpts <$> getTopLevelRW - case r of - SV.Valid -> return (Theorem t) - _ -> fail (SV.showsProofResult opts r "") + case finishProof pstate of + Just thm -> return thm + Nothing -> fail $ "prove_core: " ++ show (length (psGoals pstate)) ++ " unsolved subgoal(s)\n" + ++ SV.showsProofResult opts r "" core_axiom :: String -> TopLevel (Theorem SAWCtx) core_axiom input = do diff --git a/src/SAWScript/JavaBuiltins.hs b/src/SAWScript/JavaBuiltins.hs index 37743318b5..fac92fa862 100644 --- a/src/SAWScript/JavaBuiltins.hs +++ b/src/SAWScript/JavaBuiltins.hs @@ -251,7 +251,7 @@ verifyJava bic opts cls mname overrides setup = do let exts = getAllExts g glam <- io $ bindExts jsc exts g io $ doExtraChecks opts bsc glam - r <- evalStateT script (ProofGoal Universal (vsVCName vs) glam) + r <- evalStateT script (startProof (ProofGoal Universal (vsVCName vs) glam)) case r of SS.Unsat -> when (verb >= 3) $ io $ putStrLn "Valid." SS.SatMulti vals -> io $ showCexResults jsc (rwPPOpts rw) ms vs exts vals diff --git a/src/SAWScript/LLVMBuiltins.hs b/src/SAWScript/LLVMBuiltins.hs index 68789ebbb2..ce901e4dd5 100644 --- a/src/SAWScript/LLVMBuiltins.hs +++ b/src/SAWScript/LLVMBuiltins.hs @@ -281,7 +281,7 @@ prover opts sc ms script vs g = do verb = verbLevel opts ppopts <- fmap rwPPOpts getTopLevelRW tt <- io (bindExts sc exts g) - r <- evalStateT script (ProofGoal Universal (vsVCName vs) tt) + r <- evalStateT script (startProof (ProofGoal Universal (vsVCName vs) tt)) case r of SV.Unsat -> when (verb >= 3) $ io $ putStrLn "Valid." SV.SatMulti vals -> io $ showCexResults sc ppopts ms vs exts vals diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index 5c03ca14a6..3c285c5930 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -26,3 +26,20 @@ data ProofGoal s = , goalName :: String , goalTerm :: SharedTerm s } + +-- | A ProofState represents a sequent, where the collection of goals +-- implies the conclusion. +data ProofState s = + ProofState + { psGoals :: [ProofGoal s] + , psConcl :: ProofGoal s + } + +startProof :: ProofGoal s -> ProofState s +startProof g = ProofState [g] g + +finishProof :: ProofState s -> Maybe (Theorem s) +finishProof (ProofState gs concl) = + case gs of + [] -> Just (Theorem (goalTerm concl)) + _ : _ -> Nothing diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 23240d071a..114a99ecc4 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -349,7 +349,7 @@ data LLVMSetupState type LLVMSetup a = StateT LLVMSetupState TopLevel a -type ProofScript s a = StateT (ProofGoal s) TopLevel a +type ProofScript s a = StateT (ProofState s) TopLevel a -- IsValue class --------------------------------------------------------------- @@ -412,10 +412,10 @@ instance FromValue a => FromValue (TopLevel a) where fromValue m2 fromValue _ = error "fromValue TopLevel" -instance IsValue a => IsValue (StateT (ProofGoal SAWCtx) TopLevel a) where +instance IsValue a => IsValue (StateT (ProofState SAWCtx) TopLevel a) where toValue m = VProofScript (fmap toValue m) -instance FromValue a => FromValue (StateT (ProofGoal SAWCtx) TopLevel a) where +instance FromValue a => FromValue (StateT (ProofState SAWCtx) TopLevel a) where fromValue (VProofScript m) = fmap fromValue m fromValue (VReturn v) = return (fromValue v) fromValue (VBind m1 v2) = do