diff --git a/cabal.project b/cabal.project index fe0f598b6f..7e9daddc3f 100644 --- a/cabal.project +++ b/cabal.project @@ -4,6 +4,7 @@ packages: crux-mir-comp cryptol-saw-core rme + verif-viewer saw-core saw-core-aig saw-core-sbv diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 087e128f9e..33617f7bc6 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -1624,9 +1624,9 @@ scCryptolType sc t = scCryptolEq :: SharedContext -> Term -> Term -> IO Term scCryptolEq sc x y = do rules <- concat <$> traverse defRewrites defs - let ss = addConvs natConversions (addRules rules emptySimpset) - tx <- scTypeOf sc x >>= rewriteSharedTerm sc ss >>= scCryptolType sc - ty <- scTypeOf sc y >>= rewriteSharedTerm sc ss >>= scCryptolType sc + let ss = addConvs natConversions (addRules rules emptySimpset :: Simpset ()) + tx <- scTypeOf sc x >>= rewriteSharedTerm sc ss >>= scCryptolType sc . snd + ty <- scTypeOf sc y >>= rewriteSharedTerm sc ss >>= scCryptolType sc . snd unless (tx == ty) $ panic "scCryptolEq" [ "scCryptolEq: type mismatch between" diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs index c6a03265d5..0a7e3578de 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs @@ -18,7 +18,7 @@ import Verifier.SAW.Rewriter import Verifier.SAW.SharedTerm import Verifier.SAW.Term.Functor -mkCryptolSimpset :: SharedContext -> IO Simpset +mkCryptolSimpset :: SharedContext -> IO (Simpset a) mkCryptolSimpset sc = do m <- scFindModule sc cryptolModuleName scSimpset sc (cryptolDefs m) [] [] diff --git a/examples/ecdsa/ecdsa.saw b/examples/ecdsa/ecdsa.saw index fa18900957..2b9aa29b18 100644 --- a/examples/ecdsa/ecdsa.saw +++ b/examples/ecdsa/ecdsa.saw @@ -289,7 +289,7 @@ let ss0 = add_prelude_eqs [ "bvShiftL_bvShl" , "bvShiftR_bvShr" ] cry_ss; -let crule t = rewrite ss0 t; +let assume_rule t = prove_print (admit "assume rule") (rewrite ss0 t); let prove_rule t = prove_print abc (rewrite ss0 t); let ss1 = add_prelude_eqs @@ -365,16 +365,19 @@ ec_join_split_768 <- prove_rule {{ \x -> ec_join768 (ec_split768 x) == x }}; ec_split_join_768 <- prove_rule {{ \x -> ec_split768 (ec_join768 x) == x }}; // Axiomatic rules: For now, we assume these without proof. -let mul_java_elim = crule {{ \(a:[768]) -> \(x:[384]) -> \(y:[384]) -> - mul_java::mul_java (a, x, y) == p384_field::p384_safe_product (x, y) }}; -let sq_java_elim = crule {{ \(a:[768]) -> \(x:[384]) -> - mul_java::sq_java (a, x) == p384_field::p384_safe_product (x, x) }}; +mul_java_elim <- assume_rule + {{ \(a:[768]) -> \(x:[384]) -> \(y:[384]) -> + mul_java::mul_java (a, x, y) == p384_field::p384_safe_product (x, y) }}; + +sq_java_elim <- assume_rule + {{ \(a:[768]) -> \(x:[384]) -> + mul_java::sq_java (a, x) == p384_field::p384_safe_product (x, x) }}; let basic_simps = [ ec_join_split , at12, at24 ]; let ss3 = addsimps basic_simps ss2; -let ss4 = addsimps' [mul_java_elim, sq_java_elim] ss3; +let ss4 = addsimps [mul_java_elim, sq_java_elim] ss3; let ss = add_prelude_defs [ "bvUpd" , "bvAt" diff --git a/examples/misc/rewrite.saw b/examples/misc/rewrite.saw index 70082d8a0d..0a5debedcf 100644 --- a/examples/misc/rewrite.saw +++ b/examples/misc/rewrite.saw @@ -1,9 +1,12 @@ -let crule t = do { ss <- cryptol_ss ; rewrite ss t; }; +let ss = cryptol_ss (); +let crule t = rewrite ss t; rule <- crule {{ \(x:[384]) -> join ((split x) : [12][32]) == x }}; +rule_thm <- prove_print (admit "assume rule") rule; + print "== Original version of rule:"; print_term rule; -let rule_ss = addsimps' [rule] empty_ss; +let rule_ss = addsimps [rule_thm] empty_ss; t <- rewrite rule_ss rule; print "== Rule rewritten with itself:"; print_term t; diff --git a/saw-core/src/Verifier/SAW/Constant.hs b/saw-core/src/Verifier/SAW/Constant.hs index 2b064868f3..53e2f886f0 100644 --- a/saw-core/src/Verifier/SAW/Constant.hs +++ b/saw-core/src/Verifier/SAW/Constant.hs @@ -18,5 +18,5 @@ import Verifier.SAW.Conversion scConst :: SharedContext -> Text -> Term -> IO Term scConst sc name t = do ty <- scTypeOf sc t - ty' <- rewriteSharedTerm sc (addConvs natConversions emptySimpset) ty + (_,ty') <- rewriteSharedTerm sc (addConvs natConversions emptySimpset :: Simpset ()) ty scConstant sc name t ty' diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index 6db48c95b0..df6bb5ab2a 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/saw-core/src/Verifier/SAW/Rewriter.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE BangPatterns #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveFoldable #-} @@ -25,6 +26,7 @@ module Verifier.SAW.Rewriter , ctxtRewriteRule , lhsRewriteRule , rhsRewriteRule + , annRewriteRule , ruleOfTerm , ruleOfTerms , ruleOfProp @@ -62,6 +64,7 @@ import Data.Foldable (Foldable) import Control.Monad.Identity import Control.Monad.State import Control.Monad.Trans.Maybe +import Data.IORef import qualified Data.Foldable as Foldable import Data.Map (Map) import qualified Data.List as List @@ -80,23 +83,31 @@ import Verifier.SAW.Term.Functor import Verifier.SAW.TypedAST import qualified Verifier.SAW.TermNet as Net -data RewriteRule - = RewriteRule { ctxt :: [Term], lhs :: Term, rhs :: Term, permutative :: Bool } - deriving (Eq, Show) +data RewriteRule a + = RewriteRule { ctxt :: [Term], lhs :: Term, rhs :: Term, permutative :: Bool, annotation :: Maybe a } + deriving (Show) -- ^ Invariant: The set of loose variables in @lhs@ must be exactly -- @[0 .. length ctxt - 1]@. The @rhs@ may contain a subset of these. -ctxtRewriteRule :: RewriteRule -> [Term] +-- NB, exclude the annotation from equality tests +instance Eq (RewriteRule a) where + RewriteRule c1 l1 r1 p1 _a1 == RewriteRule c2 l2 r2 p2 _a2 = + c1 == c2 && l1 == l2 && r1 == r2 && p1 == p2 + +ctxtRewriteRule :: RewriteRule a -> [Term] ctxtRewriteRule = ctxt -lhsRewriteRule :: RewriteRule -> Term +lhsRewriteRule :: RewriteRule a -> Term lhsRewriteRule = lhs -rhsRewriteRule :: RewriteRule -> Term +rhsRewriteRule :: RewriteRule a -> Term rhsRewriteRule = rhs -instance Net.Pattern RewriteRule where - toPat (RewriteRule _ lhs _ _) = Net.toPat lhs +annRewriteRule :: RewriteRule a -> Maybe a +annRewriteRule = annotation + +instance Net.Pattern (RewriteRule a) where + toPat (RewriteRule _ lhs _ _ _) = Net.toPat lhs ---------------------------------------------------------------------- -- Matching @@ -283,15 +294,15 @@ equalNatIdent = mkIdent (mkModuleName ["Prelude"]) "equalNat" -- | Converts a universally quantified equality proposition from a -- Term representation to a RewriteRule. -ruleOfTerm :: Term -> RewriteRule -ruleOfTerm t = +ruleOfTerm :: Term -> Maybe a -> RewriteRule a +ruleOfTerm t ann = case unwrapTermF t of -- NOTE: this assumes the Coq-style equality type Eq X x y, where both X -- (the type of x and y) and x are parameters, and y is an index FTermF (DataTypeApp ident [_, x] [y]) - | ident == eqIdent -> mkRewriteRule [] x y + | ident == eqIdent -> mkRewriteRule [] x y ann Pi _ ty body -> rule { ctxt = ty : ctxt rule } - where rule = ruleOfTerm body + where rule = ruleOfTerm body ann _ -> error "ruleOfSharedTerm: Illegal argument" -- Test whether a rewrite rule is permutative @@ -305,46 +316,46 @@ rulePermutes lhs rhs = Nothing -> False -- but here we have a looping rule, not good! Just _ -> True -mkRewriteRule :: [Term] -> Term -> Term -> RewriteRule -mkRewriteRule c l r = - RewriteRule {ctxt = c, lhs = l, rhs = r , permutative = rulePermutes l r} +mkRewriteRule :: [Term] -> Term -> Term -> Maybe a -> RewriteRule a +mkRewriteRule c l r ann = + RewriteRule {ctxt = c, lhs = l, rhs = r , permutative = rulePermutes l r, annotation = ann} -- | Converts a universally quantified equality proposition between the -- two given terms to a RewriteRule. -ruleOfTerms :: Term -> Term -> RewriteRule -ruleOfTerms l r = mkRewriteRule [] l r +ruleOfTerms :: Term -> Term -> RewriteRule a +ruleOfTerms l r = mkRewriteRule [] l r Nothing -- | Converts a parameterized equality predicate to a RewriteRule, -- returning 'Nothing' if the predicate is not an equation. -ruleOfProp :: Term -> Maybe RewriteRule -ruleOfProp (R.asPi -> Just (_, ty, body)) = - do rule <- ruleOfProp body +ruleOfProp :: Term -> Maybe a -> Maybe (RewriteRule a) +ruleOfProp (R.asPi -> Just (_, ty, body)) ann = + do rule <- ruleOfProp body ann Just rule { ctxt = ty : ctxt rule } -ruleOfProp (R.asLambda -> Just (_, ty, body)) = - do rule <- ruleOfProp body +ruleOfProp (R.asLambda -> Just (_, ty, body)) ann = + do rule <- ruleOfProp body ann Just rule { ctxt = ty : ctxt rule } -ruleOfProp (R.asApplyAll -> (R.isGlobalDef ecEqIdent -> Just (), [_, _, x, y])) = - Just $ mkRewriteRule [] x y -ruleOfProp (R.asApplyAll -> (R.isGlobalDef bvEqIdent -> Just (), [_, x, y])) = - Just $ mkRewriteRule [] x y -ruleOfProp (R.asApplyAll -> (R.isGlobalDef equalNatIdent -> Just (), [x, y])) = - Just $ mkRewriteRule [] x y -ruleOfProp (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) = - Just $ mkRewriteRule [] x y -ruleOfProp (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) = - Just $ mkRewriteRule [] x y -ruleOfProp (unwrapTermF -> Constant _ body) = ruleOfProp body -ruleOfProp (R.asEq -> Just (_, x, y)) = - Just $ mkRewriteRule [] x y -ruleOfProp (R.asEqTrue -> Just body) = ruleOfProp body -ruleOfProp _ = Nothing +ruleOfProp (R.asApplyAll -> (R.isGlobalDef ecEqIdent -> Just (), [_, _, x, y])) ann = + Just $ mkRewriteRule [] x y ann +ruleOfProp (R.asApplyAll -> (R.isGlobalDef bvEqIdent -> Just (), [_, x, y])) ann = + Just $ mkRewriteRule [] x y ann +ruleOfProp (R.asApplyAll -> (R.isGlobalDef equalNatIdent -> Just (), [x, y])) ann = + Just $ mkRewriteRule [] x y ann +ruleOfProp (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) ann = + Just $ mkRewriteRule [] x y ann +ruleOfProp (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) ann = + Just $ mkRewriteRule [] x y ann +ruleOfProp (unwrapTermF -> Constant _ body) ann = ruleOfProp body ann +ruleOfProp (R.asEq -> Just (_, x, y)) ann = + Just $ mkRewriteRule [] x y ann +ruleOfProp (R.asEqTrue -> Just body) ann = ruleOfProp body ann +ruleOfProp _ _ = Nothing -- | Generate a rewrite rule from the type of an identifier, using 'ruleOfTerm' -scEqRewriteRule :: SharedContext -> Ident -> IO RewriteRule -scEqRewriteRule sc i = ruleOfTerm <$> scTypeOfGlobal sc i +scEqRewriteRule :: SharedContext -> Ident -> IO (RewriteRule a) +scEqRewriteRule sc i = ruleOfTerm <$> scTypeOfGlobal sc i <*> pure Nothing -- | Collects rewrite rules from named constants, whose types must be equations. -scEqsRewriteRules :: SharedContext -> [Ident] -> IO [RewriteRule] +scEqsRewriteRules :: SharedContext -> [Ident] -> IO [RewriteRule a] scEqsRewriteRules sc = mapM (scEqRewriteRule sc) -- | Transform the given rewrite rule to a set of one or more @@ -353,19 +364,19 @@ scEqsRewriteRules sc = mapM (scEqRewriteRule sc) -- * If the rhs is a lambda, then add an argument to the lhs. -- * If the rhs is a recursor, then split into a separate rule for each constructor. -- * If the rhs is a record, then split into a separate rule for each accessor. -scExpandRewriteRule :: SharedContext -> RewriteRule -> IO (Maybe [RewriteRule]) -scExpandRewriteRule sc (RewriteRule ctxt lhs rhs _) = +scExpandRewriteRule :: SharedContext -> RewriteRule a -> IO (Maybe [RewriteRule a]) +scExpandRewriteRule sc (RewriteRule ctxt lhs rhs _ ann) = case rhs of (R.asLambda -> Just (_, ty, body)) -> do let ctxt' = ctxt ++ [ty] lhs1 <- incVars sc 0 1 lhs var0 <- scLocalVar sc 0 lhs' <- scApply sc lhs1 var0 - return $ Just [mkRewriteRule ctxt' lhs' body] + return $ Just [mkRewriteRule ctxt' lhs' body ann] (R.asRecordValue -> Just m) -> do let mkRule (k, x) = do l <- scRecordSelect sc lhs k - return (mkRewriteRule ctxt l x) + return (mkRewriteRule ctxt l x ann) Just <$> traverse mkRule (Map.assocs m) (R.asApplyAll -> (R.asRecursorApp -> Just (d, params, p_ret, cs_fs, _ixs, R.asLocalVar -> Just i), @@ -406,9 +417,9 @@ scExpandRewriteRule sc (RewriteRule ctxt lhs rhs _) = rhs2 <- scApplyAll sc rhs1 more' rhs3 <- betaReduce rhs2 -- re-fold recursive occurrences of the original rhs - let ss = addRule (mkRewriteRule ctxt rhs lhs) emptySimpset - rhs' <- rewriteSharedTerm sc ss rhs3 - return (mkRewriteRule ctxt' lhs' rhs') + let ss = addRule (mkRewriteRule ctxt rhs lhs Nothing) emptySimpset + (_,rhs') <- rewriteSharedTerm sc (ss :: Simpset ()) rhs3 + return (mkRewriteRule ctxt' lhs' rhs' ann) dt <- scRequireDataType sc d rules <- traverse ctorRule (dtCtors dt) return (Just rules) @@ -432,7 +443,7 @@ scExpandRewriteRule sc (RewriteRule ctxt lhs rhs _) = Just (_, _, body) -> instantiateVar sc 0 arg body -- | Repeatedly apply the rule transformations in 'scExpandRewriteRule'. -scExpandRewriteRules :: SharedContext -> [RewriteRule] -> IO [RewriteRule] +scExpandRewriteRules :: SharedContext -> [RewriteRule a] -> IO [RewriteRule a] scExpandRewriteRules sc rs = case rs of [] -> return [] @@ -444,12 +455,12 @@ scExpandRewriteRules sc rs = -- | Create a rewrite rule for a definition that expands the definition, if it -- has a body to expand to, otherwise return the empty list -scDefRewriteRules :: SharedContext -> Def -> IO [RewriteRule] +scDefRewriteRules :: SharedContext -> Def -> IO [RewriteRule a] scDefRewriteRules _ (Def { defBody = Nothing }) = return [] scDefRewriteRules sc (Def { defIdent = ident, defBody = Just body }) = do lhs <- scGlobalDef sc ident rhs <- scSharedTerm sc body - scExpandRewriteRules sc [mkRewriteRule [] lhs rhs] + scExpandRewriteRules sc [mkRewriteRule [] lhs rhs Nothing] ---------------------------------------------------------------------- @@ -457,40 +468,40 @@ scDefRewriteRules sc (Def { defIdent = ident, defBody = Just body }) = -- | Invariant: 'Simpset's should not contain reflexive rules. We avoid -- adding them in 'addRule' below. -type Simpset = Net.Net (Either RewriteRule Conversion) +type Simpset a = Net.Net (Either (RewriteRule a) Conversion) -emptySimpset :: Simpset +emptySimpset :: Simpset a emptySimpset = Net.empty -addRule :: RewriteRule -> Simpset -> Simpset +addRule :: RewriteRule a -> Simpset a -> Simpset a addRule rule | lhs rule /= rhs rule = Net.insert_term (lhs rule, Left rule) | otherwise = id -delRule :: RewriteRule -> Simpset -> Simpset +delRule :: RewriteRule a -> Simpset a -> Simpset a delRule rule = Net.delete_term (lhs rule, Left rule) -addRules :: [RewriteRule] -> Simpset -> Simpset +addRules :: [RewriteRule a] -> Simpset a -> Simpset a addRules rules ss = foldr addRule ss rules -addSimp :: Term -> Simpset -> Simpset -addSimp prop = addRule (ruleOfTerm prop) +addSimp :: Term -> Maybe a -> Simpset a -> Simpset a +addSimp prop ann = addRule (ruleOfTerm prop ann) -delSimp :: Term -> Simpset -> Simpset -delSimp prop = delRule (ruleOfTerm prop) +delSimp :: Term -> Simpset a -> Simpset a +delSimp prop = delRule (ruleOfTerm prop Nothing) -addConv :: Conversion -> Simpset -> Simpset +addConv :: Conversion -> Simpset a -> Simpset a addConv conv = Net.insert_term (conv, Right conv) -addConvs :: [Conversion] -> Simpset -> Simpset +addConvs :: [Conversion] -> Simpset a -> Simpset a addConvs convs ss = foldr addConv ss convs -scSimpset :: SharedContext -> [Def] -> [Ident] -> [Conversion] -> IO Simpset +scSimpset :: SharedContext -> [Def] -> [Ident] -> [Conversion] -> IO (Simpset a) scSimpset sc defs eqIdents convs = do defRules <- concat <$> traverse (scDefRewriteRules sc) defs eqRules <- mapM (scEqRewriteRule sc) eqIdents return $ addRules defRules $ addRules eqRules $ addConvs convs $ emptySimpset -listRules :: Simpset -> [RewriteRule] +listRules :: Simpset a -> [RewriteRule a] listRules ss = [ r | Left r <- Net.content ss ] ---------------------------------------------------------------------- @@ -557,7 +568,7 @@ appCollectedArgs t = step0 (unshared t) [] -- step2: analyse an arg. look inside tuples, sequences (TBD), more calls to f step2 :: TermF Term -> TermF Term -> [Term] step2 f (FTermF (PairValue x y)) = (step2 f $ unshared x) ++ (step2 f $ unshared y) - step2 f (s@(App g a)) = possibly_curried_args s f (unshared g) (step2 f $ unshared a) + step2 f (s@(App g a)) = possibly_curried_args s f (unshared g) (step2 f $ unshared a) step2 _ a = [Unshared a] -- possibly_curried_args :: TermF Term -> TermF Term -> TermF Term -> [Term] -> [Term] @@ -579,29 +590,43 @@ reduceSharedTerm sc (asIotaRedex -> Just (d, params, p_ret, cs_fs, c, args)) = Just $ scReduceRecursor sc d params p_ret cs_fs c args reduceSharedTerm _ _ = Nothing --- | Rewriter for shared terms -rewriteSharedTerm :: SharedContext -> Simpset -> Term -> IO Term +-- | Rewriter for shared terms. The annotations of any used rules are collected +-- and returned in the result set. +rewriteSharedTerm :: forall a. Ord a => SharedContext -> Simpset a -> Term -> IO (Set a, Term) rewriteSharedTerm sc ss t0 = do cache <- newCache - let ?cache = cache in rewriteAll t0 + let ?cache = cache + setRef <- newIORef mempty + let ?annSet = setRef + t <- rewriteAll t0 + anns <- readIORef setRef + pure (anns, t) + where - rewriteAll :: (?cache :: Cache IO TermIndex Term) => Term -> IO Term + rewriteAll :: (?cache :: Cache IO TermIndex Term, ?annSet :: IORef (Set a)) => Term -> IO Term rewriteAll (Unshared tf) = traverseTF rewriteAll tf >>= scTermF sc >>= rewriteTop rewriteAll STApp{ stAppIndex = tidx, stAppTermF = tf } = useCache ?cache tidx (traverseTF rewriteAll tf >>= scTermF sc >>= rewriteTop) - traverseTF :: (a -> IO a) -> TermF a -> IO (TermF a) + + traverseTF :: forall b. (b -> IO b) -> TermF b -> IO (TermF b) traverseTF _ tf@(Constant {}) = pure tf traverseTF f tf = traverse f tf - rewriteTop :: (?cache :: Cache IO TermIndex Term) => Term -> IO Term + + rewriteTop :: (?cache :: Cache IO TermIndex Term, ?annSet :: IORef (Set a)) => Term -> IO Term rewriteTop t = case reduceSharedTerm sc t of Nothing -> apply (Net.unify_term ss t) t Just io -> rewriteAll =<< io - apply :: (?cache :: Cache IO TermIndex Term) => - [Either RewriteRule Conversion] -> Term -> IO Term + + recordAnn :: (?annSet :: IORef (Set a)) => Maybe a -> IO () + recordAnn Nothing = return () + recordAnn (Just a) = modifyIORef' ?annSet (Set.insert a) + + apply :: (?cache :: Cache IO TermIndex Term, ?annSet :: IORef (Set a)) => + [Either (RewriteRule a) Conversion] -> Term -> IO Term apply [] t = return t - apply (Left (RewriteRule {ctxt, lhs, rhs, permutative}) : rules) t = do + apply (Left (RewriteRule {ctxt, lhs, rhs, permutative, annotation}) : rules) t = do result <- scMatch sc lhs t case result of Nothing -> apply rules t @@ -620,11 +645,12 @@ rewriteSharedTerm sc ss t0 = do t' <- instantiateVarList sc 0 (Map.elems inst) rhs case termWeightLt t' t of - True -> rewriteAll t' -- keep the result only if it is "smaller" + True -> recordAnn annotation >> rewriteAll t' -- keep the result only if it is "smaller" False -> apply rules t | otherwise -> do -- putStrLn "REWRITING:" -- print lhs + recordAnn annotation rewriteAll =<< instantiateVarList sc 0 (Map.elems inst) rhs apply (Right conv : rules) t = do -- putStrLn "REWRITING:" @@ -634,20 +660,27 @@ rewriteSharedTerm sc ss t0 = Just tb -> rewriteAll =<< runTermBuilder tb (scGlobalDef sc) (scTermF sc) -- | Type-safe rewriter for shared terms -rewriteSharedTermTypeSafe - :: SharedContext -> Simpset -> Term -> IO Term +rewriteSharedTermTypeSafe :: forall a. Ord a => + SharedContext -> Simpset a -> Term -> IO (Set a, Term) rewriteSharedTermTypeSafe sc ss t0 = do cache <- newCache - let ?cache = cache in rewriteAll t0 + let ?cache = cache + annRef <- newIORef mempty + let ?annSet = annRef + t <- rewriteAll t0 + anns <- readIORef annRef + return (anns, t) + where - rewriteAll :: (?cache :: Cache IO TermIndex Term) => + rewriteAll :: (?cache :: Cache IO TermIndex Term, ?annSet :: IORef (Set a)) => Term -> IO Term rewriteAll (Unshared tf) = rewriteTermF tf >>= scTermF sc >>= rewriteTop rewriteAll STApp{ stAppIndex = tidx, stAppTermF = tf } = -- putStrLn "Rewriting term:" >> print t >> useCache ?cache tidx (rewriteTermF tf >>= scTermF sc >>= rewriteTop) - rewriteTermF :: (?cache :: Cache IO TermIndex Term) => + + rewriteTermF :: (?cache :: Cache IO TermIndex Term, ?annSet :: IORef (Set a)) => TermF Term -> IO (TermF Term) rewriteTermF tf = case tf of @@ -662,7 +695,8 @@ rewriteSharedTermTypeSafe sc ss t0 = Lambda pat t e -> Lambda pat t <$> rewriteAll e Constant{} -> return tf _ -> return tf -- traverse rewriteAll tf - rewriteFTermF :: (?cache :: Cache IO TermIndex Term) => + + rewriteFTermF :: (?cache :: Cache IO TermIndex Term, ?annSet :: IORef (Set a)) => FlatTermF Term -> IO (FlatTermF Term) rewriteFTermF ftf = case ftf of @@ -689,24 +723,33 @@ rewriteSharedTermTypeSafe sc ss t0 = Primitive{} -> return ftf StringLit{} -> return ftf ExtCns{} -> return ftf - rewriteTop :: (?cache :: Cache IO TermIndex Term) => + + rewriteTop :: (?cache :: Cache IO TermIndex Term, ?annSet :: IORef (Set a)) => Term -> IO Term rewriteTop t = apply (Net.match_term ss t) t - apply :: (?cache :: Cache IO TermIndex Term) => - [Either RewriteRule Conversion] -> + + recordAnn :: (?annSet :: IORef (Set a)) => Maybe a -> IO () + recordAnn Nothing = return () + recordAnn (Just a) = modifyIORef' ?annSet (Set.insert a) + + apply :: (?cache :: Cache IO TermIndex Term, ?annSet :: IORef (Set a)) => + [Either (RewriteRule a) Conversion] -> Term -> IO Term apply [] t = return t apply (Left rule : rules) t = case first_order_match (lhs rule) t of Nothing -> apply rules t - Just inst -> rewriteAll =<< instantiateVarList sc 0 (Map.elems inst) (rhs rule) + Just inst -> + do recordAnn (annotation rule) + rewriteAll =<< instantiateVarList sc 0 (Map.elems inst) (rhs rule) apply (Right conv : rules) t = case runConversion conv t of Nothing -> apply rules t Just tb -> rewriteAll =<< runTermBuilder tb (scGlobalDef sc) (scTermF sc) -- | Generate a new SharedContext that normalizes terms as it builds them. -rewritingSharedContext :: SharedContext -> Simpset -> SharedContext +-- Rule annotations are ignored. +rewritingSharedContext :: SharedContext -> Simpset a -> SharedContext rewritingSharedContext sc ss = sc' where sc' = sc { scTermF = rewriteTop } @@ -721,11 +764,11 @@ rewritingSharedContext sc ss = sc' Nothing -> apply (Net.match_term ss t) t where t = Unshared tf - apply :: [Either RewriteRule Conversion] -> + apply :: [Either (RewriteRule a) Conversion] -> Term -> IO Term apply [] (Unshared tf) = scTermF sc tf apply [] STApp{ stAppTermF = tf } = scTermF sc tf - apply (Left (RewriteRule _ l r _) : rules) t = + apply (Left (RewriteRule _ l r _ _ann) : rules) t = case first_order_match l t of Nothing -> apply rules t Just inst @@ -741,11 +784,12 @@ rewritingSharedContext sc ss = sc' -- FIXME: is there some way to have sensable term replacement in the presence of loose variables -- and/or under binders? -replaceTerm :: SharedContext - -> Simpset -- ^ A simpset of rewrite rules to apply along with the replacement - -> (Term, Term) -- ^ (pat,repl) is a tuple of a pattern term to replace and a replacement term - -> Term -- ^ the term in which to perform the replacement - -> IO Term +replaceTerm :: Ord a => + SharedContext -> + Simpset a {- ^ A simpset of rewrite rules to apply along with the replacement -} -> + (Term, Term) {- ^ (pat,repl) is a tuple of a pattern term to replace and a replacement term -} -> + Term {- ^ the term in which to perform the replacement -} -> + IO (Set a, Term) replaceTerm sc ss (pat, repl) t = do let fvs = looseVars pat unless (fvs == emptyBitSet) $ fail $ unwords @@ -782,7 +826,7 @@ hoistIfs sc t = do `app` (scLocalVar sc 3) - rules <- map ruleOfTerm <$> mapM (scTypeOfGlobal sc) + rules <- map (\rt -> ruleOfTerm rt Nothing) <$> mapM (scTypeOfGlobal sc) [ "Prelude.ite_true" , "Prelude.ite_false" , "Prelude.ite_not" @@ -806,38 +850,42 @@ hoistIfs sc t = do , "Prelude.not_or" , "Prelude.not_and" ] - let ss = addRules rules emptySimpset + let ss :: Simpset () = addRules rules emptySimpset - (t', conds) <- doHoistIfs sc ss cache itePat =<< rewriteSharedTerm sc ss t + (t', conds) <- doHoistIfs sc ss cache itePat . snd =<< rewriteSharedTerm sc ss t splitConds sc ss (map fst conds) t' -splitConds :: SharedContext -> Simpset -> [Term] -> Term -> IO Term -splitConds _ _ [] = return -splitConds sc ss (c:cs) = splitCond sc ss c >=> splitConds sc ss cs +splitConds :: Ord a => SharedContext -> Simpset a -> [Term] -> Term -> IO Term +splitConds sc ss = go + where + go [] t = return t + go (c:cs) t = go cs =<< splitCond sc ss c t -splitCond :: SharedContext -> Simpset -> Term -> Term -> IO Term +splitCond :: Ord a => SharedContext -> Simpset a -> Term -> Term -> IO Term splitCond sc ss c t = do ty <- scTypeOf sc t trueTerm <- scBool sc True falseTerm <- scBool sc False - then_branch <- replaceTerm sc ss (c, trueTerm) t - else_branch <- replaceTerm sc ss (c, falseTerm) t + (_,then_branch) <- replaceTerm sc ss (c, trueTerm) t + (_,else_branch) <- replaceTerm sc ss (c, falseTerm) t scGlobalApply sc "Prelude.ite" [ty, c, then_branch, else_branch] + type HoistIfs s = (Term, [(Term, Set (ExtCns Term))]) orderTerms :: SharedContext -> [Term] -> IO [Term] orderTerms _sc xs = return $ List.sort xs -doHoistIfs :: SharedContext - -> Simpset - -> Cache IO TermIndex (HoistIfs s) - -> Term - -> Term - -> IO (HoistIfs s) +doHoistIfs :: Ord a => + SharedContext -> + Simpset a -> + Cache IO TermIndex (HoistIfs s) -> + Term -> + Term -> + IO (HoistIfs s) doHoistIfs sc ss hoistCache itePat = go where go :: Term -> IO (HoistIfs s) diff --git a/saw-core/src/Verifier/SAW/SCTypeCheck.hs b/saw-core/src/Verifier/SAW/SCTypeCheck.hs index b3029e4cd8..26cd05f8fb 100644 --- a/saw-core/src/Verifier/SAW/SCTypeCheck.hs +++ b/saw-core/src/Verifier/SAW/SCTypeCheck.hs @@ -544,7 +544,7 @@ typeCheckWHNF = liftTCM scTypeCheckWHNF -- | The 'IO' version of 'typeCheckWHNF' scTypeCheckWHNF :: SharedContext -> Term -> IO Term scTypeCheckWHNF sc t = - do t' <- rewriteSharedTerm sc (addConvs natConversions emptySimpset) t + do (_, t') <- rewriteSharedTerm sc (addConvs natConversions emptySimpset :: Simpset ()) t scWhnf sc t' -- | Check that one type is a subtype of another, assuming both arguments are diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 4d00a97c4f..870f442562 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -47,15 +47,15 @@ import Verifier.SAW.TypedTerm (TypedTerm, CryptolModule) import SAWScript.Crucible.LLVM.Builtins (CheckPointsToType) import SAWScript.Crucible.LLVM.X86 (defaultStackBaseAlign) -import qualified SAWScript.Crucible.Common.MethodSpec as CMS (CrucibleMethodSpecIR, GhostGlobal) +import qualified SAWScript.Crucible.Common.MethodSpec as CMS (ProvedSpec, GhostGlobal) import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (SomeLLVM, LLVMModule) import SAWScript.Options (defaultOptions) import SAWScript.Position (Pos(..)) import SAWScript.Prover.Rewrite (basic_ss) -import SAWScript.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, TopLevelRO(..), TopLevelRW(..), defaultPPOpts) +import SAWScript.Proof (newTheoremDB) +import SAWScript.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, TopLevelRO(..), TopLevelRW(..), defaultPPOpts, SAWSimpset) import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm) -import Verifier.SAW.Rewriter (Simpset) import qualified Cryptol.Utils.Ident as Cryptol import qualified Argo @@ -189,6 +189,7 @@ initialState readFileFn = halloc <- Crucible.newHandleAllocator jvmTrans <- CJ.mkInitialJVMContext halloc cwd <- getCurrentDirectory + db <- newTheoremDB let ro = TopLevelRO { roSharedContext = sc , roJavaCodebase = jcb @@ -202,6 +203,7 @@ initialState readFileFn = #endif , roInitWorkDir = cwd , roBasicSS = ss + , roTheoremDB = db } rw = TopLevelRW { rwValues = mempty @@ -276,15 +278,15 @@ data CrucibleSetupTypeRepr :: Type -> Type where data ServerVal = VTerm TypedTerm - | VSimpset Simpset + | VSimpset SAWSimpset | VType Cryptol.Schema | VCryptolModule CryptolModule -- from SAW, includes Term mappings | VJVMClass JSS.Class | VJVMCrucibleSetup (Pair CrucibleSetupTypeRepr JVMSetupM) | VLLVMCrucibleSetup (Pair CrucibleSetupTypeRepr LLVMCrucibleSetupM) | VLLVMModule (Some CMS.LLVMModule) - | VJVMMethodSpecIR (CMS.CrucibleMethodSpecIR CJ.JVM) - | VLLVMMethodSpecIR (CMS.SomeLLVM CMS.CrucibleMethodSpecIR) + | VJVMMethodSpecIR (CMS.ProvedSpec CJ.JVM) + | VLLVMMethodSpecIR (CMS.SomeLLVM CMS.ProvedSpec) | VGhostVar CMS.GhostGlobal instance Show ServerVal where @@ -306,7 +308,7 @@ class IsServerVal a where instance IsServerVal TypedTerm where toServerVal = VTerm -instance IsServerVal Simpset where +instance IsServerVal SAWSimpset where toServerVal = VSimpset instance IsServerVal Cryptol.Schema where @@ -315,10 +317,10 @@ instance IsServerVal Cryptol.Schema where instance IsServerVal CryptolModule where toServerVal = VCryptolModule -instance IsServerVal (CMS.CrucibleMethodSpecIR CJ.JVM) where +instance IsServerVal (CMS.ProvedSpec CJ.JVM) where toServerVal = VJVMMethodSpecIR -instance IsServerVal (CMS.SomeLLVM CMS.CrucibleMethodSpecIR) where +instance IsServerVal (CMS.SomeLLVM CMS.ProvedSpec) where toServerVal = VLLVMMethodSpecIR instance IsServerVal JSS.Class where @@ -375,7 +377,7 @@ getJVMClass n = VJVMClass c -> return c _other -> Argo.raise (notAJVMClass n) -getJVMMethodSpecIR :: ServerName -> Argo.Command SAWState (CMS.CrucibleMethodSpecIR CJ.JVM) +getJVMMethodSpecIR :: ServerName -> Argo.Command SAWState (CMS.ProvedSpec CJ.JVM) getJVMMethodSpecIR n = do v <- getServerVal n case v of @@ -396,14 +398,14 @@ getLLVMSetup n = VLLVMCrucibleSetup setup -> return setup _other -> Argo.raise (notAnLLVMSetup n) -getLLVMMethodSpecIR :: ServerName -> Argo.Command SAWState (CMS.SomeLLVM CMS.CrucibleMethodSpecIR) +getLLVMMethodSpecIR :: ServerName -> Argo.Command SAWState (CMS.SomeLLVM CMS.ProvedSpec) getLLVMMethodSpecIR n = do v <- getServerVal n case v of VLLVMMethodSpecIR ir -> return ir _other -> Argo.raise (notAnLLVMMethodSpecIR n) -getSimpset :: ServerName -> Argo.Command SAWState Simpset +getSimpset :: ServerName -> Argo.Command SAWState SAWSimpset getSimpset n = do v <- getServerVal n case v of diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index 99b9a9bab9..553438c7c8 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -57,7 +57,6 @@ import SAWServer setServerVal ) import SAWServer.Data.Contract ( PointsTo(PointsTo), - GhostValue(..), Allocated(Allocated), ContractVar(ContractVar), Contract(preVars, preConds, preAllocated, prePointsTos, @@ -131,7 +130,7 @@ interpretJVMSetup fileReader bic cenv0 ss = evalStateT (traverse_ go ss) (mempty lift (jvm_alloc_object c) >>= save name . Val go (SetupAlloc _ ty _ Nothing) = error $ "cannot allocate type: " ++ show ty - go (SetupGhostValue _serverName _displayName _v) = get >>= \env -> lift $ + go (SetupGhostValue _serverName _displayName _v) = get >>= \_env -> lift $ error "nyi: ghost points-to" go (SetupPointsTo src tgt _chkTgt _cond) = get >>= \env -> lift $ do _ptr <- getSetupVal env src diff --git a/saw-remote-api/src/SAWServer/ProofScript.hs b/saw-remote-api/src/SAWServer/ProofScript.hs index 8293ef1ba1..f4ec075a68 100644 --- a/saw-remote-api/src/SAWServer/ProofScript.hs +++ b/saw-remote-api/src/SAWServer/ProofScript.hs @@ -154,7 +154,6 @@ makeSimpset params = do v <- getServerVal n case v of VSimpset ss' -> return (merge ss ss') - VTerm t -> return (addSimp (ttTerm t) ss) _ -> Argo.raise (notASimpset n) ss <- foldM add emptySimpset (ssElements params) setServerVal (ssResult params) ss diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 4dc754678d..dc75fe5c6e 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -286,8 +286,8 @@ replacePrim pat replace t = do unless c $ fail $ unlines [ "terms do not have convertible types", show tpat, show ty1, show trepl, show ty2 ] - let ss = emptySimpset - t' <- io $ replaceTerm sc ss (tpat, trepl) (ttTerm t) + let ss = emptySimpset :: SV.SAWSimpset + (_,t') <- io $ replaceTerm sc ss (tpat, trepl) (ttTerm t) io $ do ty <- scTypeOf sc (ttTerm t) @@ -358,7 +358,7 @@ assumeValid = execTactic $ tacticSolve $ \goal -> do printOutLnTop Warn $ "WARNING: assuming goal " ++ goalName goal ++ " is valid" pos <- SV.getPosition - let admitMsg = "assumeValid: " ++ goalName goal + let admitMsg = "assumeValid: " <> Text.pack (goalName goal) let stats = solverStats "ADMITTED" (propSize (goalProp goal)) return (stats, SolveSuccess (Admitted admitMsg pos (goalProp goal))) @@ -367,11 +367,11 @@ assumeUnsat = execTactic $ tacticSolve $ \goal -> do printOutLnTop Warn $ "WARNING: assuming goal " ++ goalName goal ++ " is unsat" pos <- SV.getPosition - let admitMsg = "assumeUnsat: " ++ goalName goal + let admitMsg = "assumeUnsat: " <> Text.pack (goalName goal) let stats = solverStats "ADMITTED" (propSize (goalProp goal)) return (stats, SolveSuccess (Admitted admitMsg pos (goalProp goal))) -admitProof :: String -> ProofScript () +admitProof :: Text -> ProofScript () admitProof msg = execTactic $ tacticSolve $ \goal -> do printOutLnTop Warn $ "WARNING: admitting goal " ++ goalName goal @@ -494,11 +494,11 @@ unfoldGoal unints = prop' <- io (unfoldProp sc unints' (goalProp goal)) return (prop', UnfoldEvidence unints') -simplifyGoal :: Simpset -> ProofScript () +simplifyGoal :: SV.SAWSimpset -> ProofScript () simplifyGoal ss = execTactic $ tacticChange $ \goal -> do sc <- getSharedContext - prop' <- io (simplifyProp sc ss (goalProp goal)) + (_,prop') <- io (simplifyProp sc ss (goalProp goal)) return (prop', RewriteEvidence ss) goal_eval :: [String] -> ProofScript () @@ -524,7 +524,8 @@ goal_apply thm = goal_assume :: ProofScript Theorem goal_assume = do sc <- SV.scriptTopLevel getSharedContext - execTactic (tacticAssume sc) + pos <- SV.scriptTopLevel SV.getPosition + execTactic (tacticAssume sc pos) goal_intro :: Text -> ProofScript TypedTerm goal_intro s = @@ -814,10 +815,11 @@ provePrim script t = do sc <- getSharedContext prop <- io $ predicateToProp sc Universal (ttTerm t) let goal = ProofGoal 0 "prove" "prove" prop - res <- SV.runProofScript script goal + res <- SV.runProofScript script goal Nothing "prove_prim" case res of UnfinishedProof pst -> printOutLnTop Info $ "prove: " ++ show (length (psGoals pst)) ++ " unsolved subgoal(s)" + ValidProof _ thm -> SV.recordProof thm _ -> return () return res @@ -830,7 +832,7 @@ provePrintPrim script t = do prop <- io $ predicateToProp sc Universal (ttTerm t) let goal = ProofGoal 0 "prove" "prove" prop opts <- rwPPOpts <$> getTopLevelRW - res <- SV.runProofScript script goal + res <- SV.runProofScript script goal Nothing "prove_print_prim" let failProof pst = fail $ "prove: " ++ show (length (psGoals pst)) ++ " unsolved subgoal(s)\n" ++ SV.showsProofResult opts res "" @@ -850,7 +852,7 @@ satPrim script t = sc <- getSharedContext prop <- io $ predicateToProp sc Existential (ttTerm t) let goal = ProofGoal 0 "sat" "sat" prop - res <- SV.runProofScript script goal + res <- SV.runProofScript script goal Nothing "sat" case res of InvalidProof stats cex _ -> return (SV.Sat stats cex) ValidProof stats _thm -> return (SV.Unsat stats) @@ -880,26 +882,26 @@ quickCheckPrintPrim opts sc numTests tt = "----------Counterexample----------\n" ++ showList cex' "" -cryptolSimpset :: TopLevel Simpset +cryptolSimpset :: TopLevel SV.SAWSimpset cryptolSimpset = do sc <- getSharedContext io $ Cryptol.mkCryptolSimpset sc -addPreludeEqs :: [Text] -> Simpset -> TopLevel Simpset +addPreludeEqs :: [Text] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset addPreludeEqs names ss = do sc <- getSharedContext eqRules <- io $ mapM (scEqRewriteRule sc) (map qualify names) return (addRules eqRules ss) where qualify = mkIdent (mkModuleName ["Prelude"]) -addCryptolEqs :: [Text] -> Simpset -> TopLevel Simpset +addCryptolEqs :: [Text] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset addCryptolEqs names ss = do sc <- getSharedContext eqRules <- io $ mapM (scEqRewriteRule sc) (map qualify names) return (addRules eqRules ss) where qualify = mkIdent (mkModuleName ["Cryptol"]) -add_core_defs :: Text -> [Text] -> Simpset -> TopLevel Simpset +add_core_defs :: Text -> [Text] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset add_core_defs modname names ss = do sc <- getSharedContext defs <- io $ mapM (getDef sc) names -- FIXME: warn if not found @@ -913,16 +915,16 @@ add_core_defs modname names ss = Just d -> return d Nothing -> fail $ Text.unpack $ modname <> " definition " <> n <> " not found" -add_prelude_defs :: [Text] -> Simpset -> TopLevel Simpset +add_prelude_defs :: [Text] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset add_prelude_defs = add_core_defs "Prelude" -add_cryptol_defs :: [Text] -> Simpset -> TopLevel Simpset +add_cryptol_defs :: [Text] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset add_cryptol_defs = add_core_defs "Cryptol" -rewritePrim :: Simpset -> TypedTerm -> TopLevel TypedTerm +rewritePrim :: SV.SAWSimpset -> TypedTerm -> TopLevel TypedTerm rewritePrim ss (TypedTerm schema t) = do sc <- getSharedContext - t' <- io $ rewriteSharedTerm sc ss t + (_,t') <- io $ rewriteSharedTerm sc ss t return (TypedTerm schema t') unfold_term :: [String] -> TypedTerm -> TopLevel TypedTerm @@ -938,23 +940,24 @@ beta_reduce_term (TypedTerm schema t) = do t' <- io $ betaNormalize sc t return (TypedTerm schema t') -addsimp :: Theorem -> Simpset -> TopLevel Simpset +addsimp :: Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset addsimp thm ss = do sc <- getSharedContext - io (propToRewriteRule sc (thmProp thm)) >>= \case + io (propToRewriteRule sc (thmProp thm) (Just (thmNonce thm))) >>= \case Nothing -> fail "addsimp: theorem not an equation" Just rule -> pure (addRule rule ss) -addsimp' :: Term -> Simpset -> TopLevel Simpset +-- TODO: remove this, it implicitly adds axioms +addsimp' :: Term -> SV.SAWSimpset -> TopLevel SV.SAWSimpset addsimp' t ss = - case ruleOfProp t of + case ruleOfProp t Nothing of Nothing -> fail "addsimp': theorem not an equation" Just rule -> pure (addRule rule ss) -addsimps :: [Theorem] -> Simpset -> TopLevel Simpset +addsimps :: [Theorem] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset addsimps thms ss = foldM (flip addsimp) ss thms -addsimps' :: [Term] -> Simpset -> TopLevel Simpset +addsimps' :: [Term] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset addsimps' ts ss = foldM (flip addsimp') ss ts print_type :: Term -> TopLevel () @@ -1019,7 +1022,6 @@ lambdas vars tt = -- | Apply the given Term to the given values, and evaluate to a -- final value. --- TODO: Take (ExtCns, FiniteValue) instead of (Term, FiniteValue) cexEvalFn :: SharedContext -> [(ExtCns Term, FirstOrderValue)] -> Term -> IO Concrete.CValue cexEvalFn sc args tm = do @@ -1289,7 +1291,7 @@ prove_core script input = t <- parseCore input p <- io (termToProp sc t) opts <- rwPPOpts <$> getTopLevelRW - res <- SV.runProofScript script (ProofGoal 0 "prove" "prove" p) + res <- SV.runProofScript script (ProofGoal 0 "prove" "prove" p) Nothing "prove_core" let failProof pst = fail $ "prove_core: " ++ show (length (psGoals pst)) ++ " unsolved subgoal(s)\n" ++ SV.showsProofResult opts res "" @@ -1304,13 +1306,17 @@ core_axiom input = pos <- SV.getPosition t <- parseCore input p <- io (termToProp sc t) - SV.returnProof (admitTheorem "core_axiom" pos p) + db <- roTheoremDB <$> getTopLevelRO + thm <- io (admitTheorem db "core_axiom" p pos "core_axiom") + SV.returnProof thm core_thm :: String -> TopLevel Theorem core_thm input = do t <- parseCore input sc <- getSharedContext - thm <- io (proofByTerm sc t) + pos <- SV.getPosition + db <- roTheoremDB <$> getTopLevelRO + thm <- io (proofByTerm sc db t pos "core_thm") SV.returnProof thm get_opt :: Int -> TopLevel String @@ -1429,5 +1435,16 @@ summarize_verification = let jspecs = [ s | SV.VJVMMethodSpec s <- values ] lspecs = [ s | SV.VLLVMCrucibleMethodSpec s <- values ] thms = [ t | SV.VTheorem t <- values ] - summary = computeVerificationSummary jspecs lspecs thms + db <- roTheoremDB <$> getTopLevelRO + summary <- io (computeVerificationSummary db jspecs lspecs thms) io $ putStrLn $ prettyVerificationSummary summary + +summarize_verification_json :: String -> TopLevel () +summarize_verification_json fpath = + do values <- rwProofs <$> getTopLevelRW + let jspecs = [ s | SV.VJVMMethodSpec s <- values ] + lspecs = [ s | SV.VLLVMCrucibleMethodSpec s <- values ] + thms = [ t | SV.VTheorem t <- values ] + db <- roTheoremDB <$> getTopLevelRO + summary <- io (computeVerificationSummary db jspecs lspecs thms) + io (writeFile fpath (jsonVerificationSummary summary)) diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index 492d472086..cc9fd41d24 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -26,13 +26,18 @@ module SAWScript.Crucible.Common.MethodSpec where import Data.Constraint (Constraint) import Data.Map (Map) import qualified Data.Map as Map +import Data.Set (Set) +import Data.Time.Clock import Data.Void (Void) + import Control.Monad.Trans.Maybe import Control.Monad.Trans (lift) import Control.Lens import Data.Kind (Type) import qualified Prettyprinter as PP +import Data.Parameterized.Nonce + -- what4 import What4.ProgramLoc (ProgramLoc(plSourceLoc), Position) @@ -48,6 +53,7 @@ import Verifier.SAW.SharedTerm as SAWVerifier import SAWScript.Options import SAWScript.Prover.SolverStats import SAWScript.Utils (bullets) +import SAWScript.Proof (TheoremNonce) -- | How many allocations have we made in this method spec? newtype AllocIndex = AllocIndex Int @@ -373,13 +379,45 @@ data CrucibleMethodSpecIR ext = , _csArgBindings :: Map Integer (ExtType ext, SetupValue ext) -- ^ function arguments , _csRetValue :: Maybe (SetupValue ext) -- ^ function return value , _csGlobalAllocs :: [AllocGlobal ext] -- ^ globals allocated - , _csSolverStats :: SolverStats -- ^ statistics about the proof that produced this , _csCodebase :: Codebase ext -- ^ the codebase this spec was verified against , _csLoc :: ProgramLoc -- ^ where in the SAWscript was this spec? } makeLenses ''CrucibleMethodSpecIR +data ProofMethod + = SpecAdmitted + | SpecProved + +type SpecNonce ext = Nonce GlobalNonceGenerator (ProvedSpec ext) + +data ProvedSpec ext = + ProvedSpec + { _psSpecIdent :: Nonce GlobalNonceGenerator (ProvedSpec ext) + , _psProofMethod :: ProofMethod + , _psSpec :: CrucibleMethodSpecIR ext + , _psSolverStats :: SolverStats -- ^ statistics about the proof that produced this + , _psTheoremDeps :: Set TheoremNonce -- ^ theorems depended on by this proof + , _psSpecDeps :: Set (SpecNonce ext) + -- ^ Other proved specifications this proof depends on + , _psElapsedTime :: NominalDiffTime -- ^ The time elapsed during the proof of this specification + } + +makeLenses ''ProvedSpec + +mkProvedSpec :: + ProofMethod -> + CrucibleMethodSpecIR ext -> + SolverStats -> + Set TheoremNonce -> + Set (SpecNonce ext) -> + NominalDiffTime -> + IO (ProvedSpec ext) +mkProvedSpec m mspec stats thms sps elapsed = + do n <- freshNonce globalNonceGenerator + let ps = ProvedSpec n m mspec stats thms sps elapsed + return ps + -- TODO: remove when what4 switches to prettyprinter prettyPosition :: Position -> PP.Doc ann prettyPosition = PP.viaShow @@ -428,7 +466,6 @@ makeCrucibleMethodSpecIR meth args ret loc code = do ,_csArgBindings = Map.empty ,_csRetValue = Nothing ,_csGlobalAllocs = [] - ,_csSolverStats = mempty ,_csLoc = loc ,_csCodebase = code } diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index cd55c40edf..d65f2797ba 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -62,6 +62,7 @@ import qualified Data.Set as Set import qualified Data.Sequence as Seq import Data.Text (Text) import qualified Data.Text as Text +import Data.Time.Clock (getCurrentTime, diffUTCTime) import qualified Data.Vector as V import Data.Void (absurd) import Prettyprinter @@ -132,7 +133,8 @@ import SAWScript.Crucible.JVM.ResolveSetupValue import SAWScript.Crucible.JVM.BuiltinsJVM () type SetupValue = MS.SetupValue CJ.JVM -type CrucibleMethodSpecIR = MS.CrucibleMethodSpecIR CJ.JVM +type Lemma = MS.ProvedSpec CJ.JVM +type MethodSpec = MS.CrucibleMethodSpecIR CJ.JVM type SetupCondition = MS.SetupCondition CJ.JVM -- TODO: something useful with the global pair? @@ -188,13 +190,14 @@ excludedRefs = Set.fromList jvm_verify :: J.Class -> String {- ^ method name -} -> - [CrucibleMethodSpecIR] {- ^ overrides -} -> + [Lemma] {- ^ overrides -} -> Bool {- ^ path sat checking -} -> JVMSetupM () -> ProofScript () -> - TopLevel CrucibleMethodSpecIR + TopLevel Lemma jvm_verify cls nm lemmas checkSat setup tactic = - do cb <- getJavaCodebase + do start <- io getCurrentTime + cb <- getJavaCodebase opts <- getOptions -- allocate all of the handles/static vars that are referenced -- (directly or indirectly) by this class @@ -241,16 +244,21 @@ jvm_verify cls nm lemmas checkSat setup tactic = _ <- io $ Crucible.popAssumptionFrame sym frameIdent -- attempt to verify the proof obligations - stats <- verifyObligations cc methodSpec tactic assumes asserts + (stats,thms) <- verifyObligations cc methodSpec tactic assumes asserts io $ writeFinalProfile - returnProof (methodSpec & MS.csSolverStats .~ stats) + + let lemmaSet = Set.fromList (map (view MS.psSpecIdent) lemmas) + end <- io getCurrentTime + let diff = diffUTCTime end start + ps <- io (MS.mkProvedSpec MS.SpecProved methodSpec stats thms lemmaSet diff) + returnProof ps jvm_unsafe_assume_spec :: J.Class -> String {- ^ Name of the method -} -> JVMSetupM () {- ^ Boundary specification -} -> - TopLevel CrucibleMethodSpecIR + TopLevel Lemma jvm_unsafe_assume_spec cls nm setup = do cc <- setupCrucibleContext cls cb <- getJavaCodebase @@ -260,29 +268,32 @@ jvm_unsafe_assume_spec cls nm setup = let loc = SS.toW4Loc "_SAW_assume_spec" pos let st0 = initialCrucibleSetupState cc (cls', method) loc ms <- (view Setup.csMethodSpec) <$> execStateT (runJVMSetupM setup) st0 - returnProof ms + + ps <- io (MS.mkProvedSpec MS.SpecAdmitted ms mempty mempty mempty 0) + returnProof ps verifyObligations :: JVMCrucibleContext -> - CrucibleMethodSpecIR -> + MethodSpec -> ProofScript () -> [Crucible.LabeledPred Term Crucible.AssumptionReason] -> - [(String, Term)] -> - TopLevel SolverStats + [(String, W4.ProgramLoc, Term)] -> + TopLevel (SolverStats, Set TheoremNonce) verifyObligations cc mspec tactic assumes asserts = do let sym = cc^.jccBackend st <- io $ sawCoreState sym let sc = saw_ctx st assume <- io $ scAndList sc (toListOf (folded . Crucible.labeledPred) assumes) let nm = mspec ^. csMethodName - stats <- forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) -> do + outs <- forM (zip [(0::Int)..] asserts) $ \(n, (msg, ploc, assert)) -> do goal <- io $ scImplies sc assume assert goal' <- io $ boolToProp sc [] goal -- TODO, generalize over inputs let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"] proofgoal = ProofGoal n "vc" goalname goal' - res <- runProofScript tactic proofgoal + res <- runProofScript tactic proofgoal (Just ploc) $ Text.unwords + ["JVM verification condition:", Text.pack (show n), Text.pack goalname] case res of - ValidProof stats _thm -> return stats -- TODO, do something with these theorems! + ValidProof stats thm -> return (stats, thmNonce thm) InvalidProof stats vals _pst -> do printOutLnTop Info $ unwords ["Subgoal failed:", nm, msg] printOutLnTop Info (show stats) @@ -296,7 +307,10 @@ verifyObligations cc mspec tactic assumes asserts = io $ fail $ "Proof failed " ++ show (length (psGoals pst)) ++ " goals remaining." printOutLnTop Info $ unwords ["Proof succeeded!", nm] - return (mconcat stats) + + let stats = mconcat (map fst outs) + let thms = mconcat (map (Set.singleton . snd) outs) + return (stats, thms) -- | Evaluate the precondition part of a Crucible method spec: -- @@ -316,7 +330,7 @@ verifyObligations cc mspec tactic assumes asserts = -- memory). verifyPrestate :: JVMCrucibleContext -> - CrucibleMethodSpecIR -> + MethodSpec -> Crucible.SymGlobalState Sym -> IO ([(J.Type, JVMVal)], [Crucible.LabeledPred Term Crucible.AssumptionReason], @@ -411,8 +425,8 @@ storageType ty = J.ClassType{} -> STRef resolveArguments :: - JVMCrucibleContext -> - CrucibleMethodSpecIR -> + JVMCrucibleContext -> + MethodSpec -> Map AllocIndex JVMRefVal -> IO [(J.Type, JVMVal)] resolveArguments cc mspec env = mapM resolveArg [0..(nArgs-1)] @@ -447,10 +461,10 @@ resolveArguments cc mspec env = mapM resolveArg [0..(nArgs-1)] -- function spec, write the given value to the address of the given -- pointer. setupPrePointsTos :: - CrucibleMethodSpecIR -> - JVMCrucibleContext -> + MethodSpec -> + JVMCrucibleContext -> Map AllocIndex JVMRefVal -> - [JVMPointsTo] -> + [JVMPointsTo] -> Crucible.SymGlobalState Sym -> IO (Crucible.SymGlobalState Sym) setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts @@ -493,10 +507,10 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts -- | Collects boolean terms that should be assumed to be true. setupPrestateConditions :: - CrucibleMethodSpecIR -> - JVMCrucibleContext -> - Map AllocIndex JVMRefVal -> - [SetupCondition] -> + MethodSpec -> + JVMCrucibleContext -> + Map AllocIndex JVMRefVal -> + [SetupCondition] -> IO [Crucible.LabeledPred Term Crucible.AssumptionReason] setupPrestateConditions mspec cc env = aux [] where @@ -547,7 +561,7 @@ registerOverride :: JVMCrucibleContext -> Crucible.SimContext (SAWCruciblePersonality Sym) Sym CJ.JVM -> W4.ProgramLoc -> - [CrucibleMethodSpecIR] -> + [MethodSpec] -> Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym CJ.JVM rtp args ret () registerOverride opts cc _ctx top_loc cs = do let sym = cc^.jccBackend @@ -574,15 +588,15 @@ registerOverride opts cc _ctx top_loc cs = -------------------------------------------------------------------------------- verifySimulate :: - Options -> - JVMCrucibleContext -> + Options -> + JVMCrucibleContext -> [Crucible.GenericExecutionFeature Sym] -> - CrucibleMethodSpecIR -> - [(a, JVMVal)] -> + MethodSpec -> + [(a, JVMVal)] -> [Crucible.LabeledPred Term Crucible.AssumptionReason] -> - W4.ProgramLoc -> - [CrucibleMethodSpecIR] -> - Crucible.SymGlobalState Sym -> + W4.ProgramLoc -> + [Lemma] -> + Crucible.SymGlobalState Sym -> Bool {- ^ path sat checking -} -> IO (Maybe (J.Type, JVMVal), Crucible.SymGlobalState Sym) verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat = @@ -613,7 +627,8 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat = do liftIO $ putStrLn "registering standard overrides" _ <- Strict.runStateT (mapM_ CJ.register_jvm_override CJ.stdOverrides) jc liftIO $ putStrLn "registering user-provided overrides" - mapM_ (registerOverride opts cc simctx top_loc) (groupOn (view csMethodName) lemmas) + mapM_ (registerOverride opts cc simctx top_loc) + (groupOn (view csMethodName) (map (view MS.psSpec) lemmas)) liftIO $ putStrLn "registering assumptions" liftIO $ do preds <- (traverse . Crucible.labeledPred) (resolveSAWPred cc) assumes @@ -684,12 +699,12 @@ scAndList sc = conj . filter nontrivial -------------------------------------------------------------------------------- verifyPoststate :: - JVMCrucibleContext {- ^ crucible context -} -> - CrucibleMethodSpecIR {- ^ specification -} -> + JVMCrucibleContext {- ^ crucible context -} -> + MethodSpec {- ^ specification -} -> Map AllocIndex JVMRefVal {- ^ allocation substitution -} -> Crucible.SymGlobalState Sym {- ^ global variables -} -> Maybe (J.Type, JVMVal) {- ^ optional return value -} -> - TopLevel [(String, Term)] {- ^ generated labels and verification conditions -} + TopLevel [(String, W4.ProgramLoc, Term)] {- ^ generated labels and verification conditions -} verifyPoststate cc mspec env0 globals ret = do opts <- getOptions sc <- getSharedContext @@ -721,12 +736,12 @@ verifyPoststate cc mspec env0 globals ret = where sym = cc^.jccBackend - verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError _loc err))) = + verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError loc err))) = do st <- sawCoreState sym hypTerm <- scAndList sc =<< mapM (toSC sym st) (toListOf (folded . Crucible.labeledPred) hyps) conclTerm <- toSC sym st concl obligation <- scImplies sc hypTerm conclTerm - return ("safety assertion: " ++ Crucible.simErrorReasonMsg err, obligation) + return ("safety assertion: " ++ Crucible.simErrorReasonMsg err, loc, obligation) matchResult opts sc = case (ret, mspec ^. MS.csRetValue) of diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index a2f56ebfa0..ca129de60b 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -103,11 +103,13 @@ import Data.Map (Map) import qualified Data.Map as Map import Data.HashMap.Strict (HashMap) import qualified Data.HashMap.Strict as HashMap +import Data.Set (Set) import qualified Data.Set as Set import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Data.Text (Text) import qualified Data.Text as Text +import Data.Time.Clock (getCurrentTime, diffUTCTime) import qualified Data.Vector as V import Prettyprinter import System.IO @@ -266,33 +268,39 @@ resolveSpecName nm = llvm_verify :: Some LLVMModule -> String -> - [SomeLLVM MS.CrucibleMethodSpecIR] -> + [SomeLLVM MS.ProvedSpec] -> Bool -> LLVMCrucibleSetupM () -> ProofScript () -> - TopLevel (SomeLLVM MS.CrucibleMethodSpecIR) + TopLevel (SomeLLVM MS.ProvedSpec) llvm_verify (Some lm) nm lemmas checkSat setup tactic = - do lemmas' <- checkModuleCompatibility lm lemmas + do start <- io getCurrentTime + lemmas' <- checkModuleCompatibility lm lemmas withMethodSpec checkSat lm nm setup $ \cc method_spec -> - do (res_method_spec, _) <- verifyMethodSpec cc method_spec lemmas' checkSat tactic Nothing - returnProof $ SomeLLVM res_method_spec + do (stats, deps, _) <- verifyMethodSpec cc method_spec lemmas' checkSat tactic Nothing + let lemmaSet = Set.fromList (map (view MS.psSpecIdent) lemmas') + end <- io getCurrentTime + let diff = diffUTCTime end start + ps <- io (MS.mkProvedSpec MS.SpecProved method_spec stats deps lemmaSet diff) + returnProof $ SomeLLVM ps llvm_unsafe_assume_spec :: Some LLVMModule -> String {- ^ Name of the function -} -> LLVMCrucibleSetupM () {- ^ Boundary specification -} -> - TopLevel (SomeLLVM MS.CrucibleMethodSpecIR) + TopLevel (SomeLLVM MS.ProvedSpec) llvm_unsafe_assume_spec (Some lm) nm setup = withMethodSpec False lm nm setup $ \_ method_spec -> do printOutLnTop Info $ unwords ["Assume override", (method_spec ^. csName)] - returnProof $ SomeLLVM method_spec + ps <- io (MS.mkProvedSpec MS.SpecAdmitted method_spec mempty mempty mempty 0) + returnProof $ SomeLLVM ps llvm_array_size_profile :: ProofScript () -> Some LLVMModule -> String -> - [SomeLLVM MS.CrucibleMethodSpecIR] -> + [SomeLLVM MS.ProvedSpec] -> LLVMCrucibleSetupM () -> TopLevel [(String, [Crucible.FunctionProfile])] llvm_array_size_profile assume (Some lm) nm lemmas setup = do @@ -323,13 +331,14 @@ llvm_compositional_extract :: Some LLVMModule -> String -> String -> - [SomeLLVM MS.CrucibleMethodSpecIR] -> + [SomeLLVM MS.ProvedSpec] -> Bool {- ^ check sat -} -> LLVMCrucibleSetupM () -> ProofScript () -> - TopLevel (SomeLLVM MS.CrucibleMethodSpecIR) + TopLevel (SomeLLVM MS.ProvedSpec) llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic = - do lemmas' <- checkModuleCompatibility lm lemmas + do start <- io getCurrentTime + lemmas' <- checkModuleCompatibility lm lemmas withMethodSpec checkSat lm nm setup $ \cc method_spec -> do let value_input_parameters = mapMaybe (\(_, setup_value) -> setupValueAsExtCns setup_value) @@ -373,7 +382,8 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic = , "An output parameter must be bound by llvm_return or llvm_points_to." ] - (res_method_spec, post_override_state) <- verifyMethodSpec cc method_spec lemmas' checkSat tactic Nothing + (stats, deps, post_override_state) <- + verifyMethodSpec cc method_spec lemmas' checkSat tactic Nothing shared_context <- getSharedContext @@ -412,12 +422,12 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic = extracted_ret_value <- liftIO $ mapM setup_value_substitute_output_parameter - (res_method_spec ^. MS.csRetValue) + (method_spec ^. MS.csRetValue) extracted_post_state_points_tos <- liftIO $ mapM (\(LLVMPointsTo x y z value) -> LLVMPointsTo x y z <$> llvm_points_to_value_substitute_output_parameter value) - (res_method_spec ^. MS.csPostState ^. MS.csPointsTos) - let extracted_method_spec = res_method_spec & + (method_spec ^. MS.csPostState ^. MS.csPointsTos) + let extracted_method_spec = method_spec & MS.csRetValue .~ extracted_ret_value & MS.csPostState . MS.csPointsTos .~ extracted_post_state_points_tos @@ -433,7 +443,12 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic = rw putTopLevelRW rw' - return $ SomeLLVM extracted_method_spec + let lemmaSet = Set.fromList (map (view MS.psSpecIdent) lemmas') + + end <- io getCurrentTime + let diff = diffUTCTime end start + ps <- io (MS.mkProvedSpec MS.SpecProved extracted_method_spec stats deps lemmaSet diff) + returnProof (SomeLLVM ps) setupValueAsExtCns :: SetupValue (LLVM arch) -> Maybe (ExtCns Term) setupValueAsExtCns = @@ -450,12 +465,12 @@ llvmPointsToValueAsExtCns = -- | Check that all the overrides/lemmas were actually from this module checkModuleCompatibility :: LLVMModule arch -> - [SomeLLVM MS.CrucibleMethodSpecIR] -> - TopLevel [MS.CrucibleMethodSpecIR (LLVM arch)] + [SomeLLVM MS.ProvedSpec] -> + TopLevel [MS.ProvedSpec (LLVM arch)] checkModuleCompatibility llvmModule = foldM step [] where step accum (SomeLLVM lemma) = - case testEquality (lemma ^. MS.csCodebase) llvmModule of + case testEquality (lemma ^. MS.psSpec.MS.csCodebase) llvmModule of Nothing -> throwTopLevel $ unlines [ "Failed to apply an override that was verified against a" , "different LLVM module" @@ -516,11 +531,11 @@ verifyMethodSpec :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> - [MS.CrucibleMethodSpecIR (LLVM arch)] -> + [MS.ProvedSpec (LLVM arch)] -> Bool -> ProofScript () -> Maybe (IORef (Map Text.Text [Crucible.FunctionProfile])) -> - TopLevel (MS.CrucibleMethodSpecIR (LLVM arch), OverrideState (LLVM arch)) + TopLevel (SolverStats, Set TheoremNonce, OverrideState (LLVM arch)) verifyMethodSpec cc methodSpec lemmas checkSat tactic asp = do printOutLnTop Info $ unwords ["Verifying", (methodSpec ^. csName) , "..."] @@ -577,33 +592,36 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp = -- attempt to verify the proof obligations printOutLnTop Info $ unwords ["Checking proof obligations", (methodSpec ^. csName), "..."] - stats <- verifyObligations cc methodSpec tactic assumes asserts + (stats, deps) <- verifyObligations cc methodSpec tactic assumes asserts io $ writeFinalProfile - return (methodSpec & MS.csSolverStats .~ stats, post_override_state) - + return ( stats + , deps + , post_override_state + ) verifyObligations :: LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> ProofScript () -> [Crucible.LabeledPred Term Crucible.AssumptionReason] - -> [(String, Term)] - -> TopLevel SolverStats + -> [(String, W4.ProgramLoc, Term)] + -> TopLevel (SolverStats, Set TheoremNonce) verifyObligations cc mspec tactic assumes asserts = do let sym = cc^.ccBackend st <- io $ Common.sawCoreState sym let sc = saw_ctx st assume <- io $ scAndList sc (toListOf (folded . Crucible.labeledPred) assumes) let nm = mspec ^. csName - stats <- - forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) -> + outs <- + forM (zip [(0::Int)..] asserts) $ \(n, (msg, ploc, assert)) -> do goal <- io $ scImplies sc assume assert goal' <- io $ boolToProp sc [] goal let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"] proofgoal = ProofGoal n "vc" goalname goal' - res <- runProofScript tactic proofgoal + res <- runProofScript tactic proofgoal (Just ploc) $ Text.unwords + ["LLVM verification condition", Text.pack (show n), Text.pack goalname] case res of - ValidProof stats _thm -> return stats -- TODO do something with these theorems + ValidProof stats thm -> return (stats, thmNonce thm) UnfinishedProof pst -> do printOutLnTop Info $ unwords ["Subgoal failed:", nm, msg] throwTopLevel $ "Proof failed " ++ show (length (psGoals pst)) ++ " goals remaining." @@ -621,7 +639,10 @@ verifyObligations cc mspec tactic assumes asserts = printOutLnTop OnlyCounterExamples "----------------------------------" throwTopLevel "Proof failed." -- Mirroring behavior of llvm_verify printOutLnTop Info $ unwords ["Proof succeeded!", nm] - return (mconcat stats) + + let stats = mconcat (map fst outs) + let deps = mconcat (map (Set.singleton . snd) outs) + return (stats, deps) throwMethodSpec :: MS.CrucibleMethodSpecIR (LLVM arch) -> String -> IO a throwMethodSpec mspec msg = X.throw $ LLVMMethodSpecException (mspec ^. MS.csLoc) msg @@ -766,7 +787,7 @@ assumptionsContainContradiction cc tactic assumptions = goal <- scImplies sc assume =<< toSC sym st (W4.falsePred sym) goal' <- boolToProp sc [] goal return $ ProofGoal 0 "vc" "vacuousness check" goal' - res <- runProofScript tactic pgl + res <- runProofScript tactic pgl Nothing "vacuousness check" case res of ValidProof _ _ -> return True InvalidProof _ _ _ -> return False @@ -1129,7 +1150,7 @@ verifySimulate :: [(Crucible.MemType, LLVMVal)] -> [Crucible.LabeledPred Term Crucible.AssumptionReason] -> W4.ProgramLoc -> - [MS.CrucibleMethodSpecIR (LLVM arch)] -> + [MS.ProvedSpec (LLVM arch)] -> Crucible.SymGlobalState Sym -> Bool -> Maybe (IORef (Map Text.Text [Crucible.FunctionProfile])) -> @@ -1148,7 +1169,8 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat as let patSatGenExecFeature = if checkSat then [psatf] else [] when checkSat checkYicesVersion let (funcLemmas, invLemmas) = - partition (isNothing . view csParentName) lemmas + partition (isNothing . view csParentName) + (map (view MS.psSpec) lemmas) breakpoints <- forM (groupOn (view csParentName) invLemmas) $ \specs -> @@ -1239,7 +1261,7 @@ verifyPoststate :: Map AllocIndex (LLVMPtr wptr) {- ^ allocation substitution -} -> Crucible.SymGlobalState Sym {- ^ global variables -} -> Maybe (Crucible.MemType, LLVMVal) {- ^ optional return value -} -> - TopLevel ([(String, Term)], OverrideState (LLVM arch)) {- ^ generated labels and verification conditions -} + TopLevel ([(String, W4.ProgramLoc, Term)], OverrideState (LLVM arch)) {- ^ generated labels and verification conditions -} verifyPoststate cc mspec env0 globals ret = do poststateLoc <- toW4Loc "_SAW_verify_poststate" <$> getPosition sc <- getSharedContext @@ -1279,12 +1301,12 @@ verifyPoststate cc mspec env0 globals ret = where sym = cc^.ccBackend - verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err)) = + verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err@(Crucible.SimError loc _))) = do st <- Common.sawCoreState sym hypTerm <- toSC sym st =<< W4.andAllOf sym (folded . Crucible.labeledPred) hyps conclTerm <- toSC sym st concl obligation <- scImplies sc hypTerm conclTerm - return (unlines ["safety assertion:", show err], obligation) + return (unlines ["safety assertion:", show err], loc, obligation) matchResult opts sc = case (ret, mspec ^. MS.csRetValue) of @@ -2170,13 +2192,13 @@ llvm_ghost_value ghost val = LLVMCrucibleSetupM $ do loc <- getW4Position "llvm_ghost_value" Setup.addCondition (MS.SetupCond_Ghost () loc ghost val) -llvm_spec_solvers :: SomeLLVM (MS.CrucibleMethodSpecIR) -> [String] -llvm_spec_solvers (SomeLLVM mir) = - Set.toList $ solverStatsSolvers $ (view MS.csSolverStats) $ mir +llvm_spec_solvers :: SomeLLVM MS.ProvedSpec -> [String] +llvm_spec_solvers (SomeLLVM ps) = + Set.toList $ solverStatsSolvers $ view MS.psSolverStats $ ps -llvm_spec_size :: SomeLLVM MS.CrucibleMethodSpecIR -> Integer +llvm_spec_size :: SomeLLVM MS.ProvedSpec -> Integer llvm_spec_size (SomeLLVM mir) = - solverStatsGoalSize $ mir ^. MS.csSolverStats + solverStatsGoalSize $ mir ^. MS.psSolverStats crucible_setup_val_to_typed_term :: AllLLVM SetupValue -> diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index 859dd6dfb4..cd95d600d3 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -135,6 +135,8 @@ import qualified SAWScript.Crucible.Common.Setup.Type as Setup import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL +import SAWScript.Proof (TheoremNonce) + import Verifier.SAW.Simulator.What4.ReturnTrip ( toSC, saw_ctx ) import Verifier.SAW.Rewriter (Simpset) @@ -323,7 +325,7 @@ data LLVMCrucibleContext arch = , _ccBackend :: Sym , _ccLLVMSimContext :: Crucible.SimContext (SAWCruciblePersonality Sym) Sym CL.LLVM , _ccLLVMGlobals :: Crucible.SymGlobalState Sym - , _ccBasicSS :: Simpset + , _ccBasicSS :: Simpset TheoremNonce } makeLenses ''LLVMCrucibleContext diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index f5a4f4713c..70e14aeb7e 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -373,7 +373,7 @@ resolveSAWPred cc tm = do st <- sawCoreState sym let sc = saw_ctx st let ss = cc^.ccBasicSS - tm' <- rewriteSharedTerm sc ss tm + (_,tm') <- rewriteSharedTerm sc ss tm mx <- case getAllExts tm' of -- concretely evaluate if it is a closed term [] -> do modmap <- scGetModuleMap sc diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 5478e56c1b..43f48450c2 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -41,10 +41,11 @@ import Data.Foldable (foldlM) import qualified Data.List.NonEmpty as NE import qualified Data.Vector as Vector import qualified Data.Text as Text +import Data.Set (Set) +import qualified Data.Set as Set import Data.Text (Text) import Data.Text.Encoding (decodeUtf8, encodeUtf8) -import qualified Data.Set as Set -import Data.Set (Set) +import Data.Time.Clock (getCurrentTime, diffUTCTime) import qualified Data.Map as Map import Data.Map (Map) import Data.Maybe @@ -288,10 +289,11 @@ llvm_verify_x86 :: Bool {- ^ Whether to enable path satisfiability checking -} -> LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> ProofScript () {- ^ Tactic used to use when discharging goals -} -> - TopLevel (SomeLLVM MS.CrucibleMethodSpecIR) + TopLevel (SomeLLVM MS.ProvedSpec) llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat setup tactic | Just Refl <- testEquality (C.LLVM.X86Repr $ knownNat @64) . C.LLVM.llvmArch $ modTrans llvmModule ^. C.LLVM.transContext = do + start <- io getCurrentTime let ?ptrWidth = knownNat @64 let ?recordLLVMAnnotation = \_ _ -> return () sc <- getSharedContext @@ -449,9 +451,13 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se ar C.TimeoutResult{} -> fail "Execution timed out" - stats <- checkGoals sym opts sc tactic + (stats,thms) <- checkGoals sym opts sc tactic + + end <- io getCurrentTime + let diff = diffUTCTime end start + ps <- io (MS.mkProvedSpec MS.SpecProved methodSpec stats thms mempty diff) + returnProof $ SomeLLVM ps - returnProof $ SomeLLVM (methodSpec & MS.csSolverStats .~ stats) | otherwise = fail "LLVM module must be 64-bit" -------------------------------------------------------------------------------- @@ -943,7 +949,7 @@ checkGoals :: Options -> SharedContext -> ProofScript () -> - TopLevel SolverStats + TopLevel (SolverStats, Set TheoremNonce) checkGoals sym opts sc tactic = do gs <- liftIO $ getGoals sym liftIO . printOutLn opts Info $ mconcat @@ -951,12 +957,13 @@ checkGoals sym opts sc tactic = do , show $ length gs , " goals" ] - stats <- forM (zip [0..] gs) $ \(n, g) -> do + outs <- forM (zip [0..] gs) $ \(n, g) -> do term <- liftIO $ gGoal sc g let proofgoal = ProofGoal n "vc" (show $ gMessage g) term - res <- runProofScript tactic proofgoal + res <- runProofScript tactic proofgoal (Just (gLoc g)) $ Text.unwords + ["X86 verification condition", Text.pack (show n), Text.pack (show (gMessage g))] case res of - ValidProof stats _thm -> return stats -- TODO do something with these theorems + ValidProof stats thm -> return (stats, thmNonce thm) UnfinishedProof pst -> do printOutLnTop Info $ unwords ["Subgoal failed:", show $ gMessage g] printOutLnTop Info (show (psStats pst)) @@ -975,4 +982,7 @@ checkGoals sym opts sc tactic = do printOutLnTop OnlyCounterExamples "----------------------------------" throwTopLevel "Proof failed." liftIO $ printOutLn opts Info "All goals succeeded" - return (mconcat stats) + + let stats = mconcat (map fst outs) + let thms = mconcat (map (Set.singleton . snd) outs) + return (stats, thms) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index dcd84c02d4..a76de8ade1 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -34,7 +34,7 @@ import Control.Applicative import Data.Traversable hiding ( mapM ) #endif import qualified Control.Exception as X -import Control.Monad (unless, (>=>)) +import Control.Monad (unless, (>=>), when) import Control.Monad.IO.Class (liftIO) import qualified Data.ByteString as BS import Data.Foldable (foldrM) @@ -62,6 +62,7 @@ import SAWScript.Parser (parseSchema) import SAWScript.TopLevel import SAWScript.Utils import SAWScript.Value +import SAWScript.Proof (newTheoremDB) import SAWScript.Prover.Rewrite(basic_ss) import SAWScript.Prover.Exporter import Verifier.SAW.Conversion @@ -364,11 +365,12 @@ interpretStmt printBinds stmt = writeVerificationSummary :: TopLevel () writeVerificationSummary = do do + db <- roTheoremDB <$> getTopLevelRO values <- rwProofs <$> getTopLevelRW let jspecs = [ s | VJVMMethodSpec s <- values ] lspecs = [ s | VLLVMCrucibleMethodSpec s <- values ] thms = [ t | VTheorem t <- values ] - summary = computeVerificationSummary jspecs lspecs thms + summary <- io (computeVerificationSummary db jspecs lspecs thms) opts <- roOptions <$> getTopLevelRO dir <- roInitWorkDir <$> getTopLevelRO case summaryFile opts of @@ -380,11 +382,12 @@ writeVerificationSummary = do Pretty -> prettyVerificationSummary in io $ writeFile f' $ formatSummary summary -interpretFile :: FilePath -> TopLevel () -interpretFile file = do +interpretFile :: FilePath -> Bool {- ^ run main? -} -> TopLevel () +interpretFile file runMain = do opts <- getOptions stmts <- io $ SAWScript.Import.loadFile opts file mapM_ stmtWithPrint stmts + when runMain interpretMain writeVerificationSummary where stmtWithPrint s = do let withPos str = unlines $ @@ -436,6 +439,7 @@ buildTopLevelEnv proxy opts = ss <- basic_ss sc jcb <- JCB.loadCodebase (jarList opts) (classPath opts) (javaBinDirs opts) currDir <- getCurrentDirectory + thmDB <- newTheoremDB Crucible.withHandleAllocator $ \halloc -> do let ro0 = TopLevelRO { roSharedContext = sc @@ -446,6 +450,7 @@ buildTopLevelEnv proxy opts = , roProxy = proxy , roInitWorkDir = currDir , roBasicSS = ss + , roTheoremDB = thmDB } let bic = BuiltinContext { biSharedContext = sc @@ -485,7 +490,7 @@ processFile proxy opts file = do oldpath <- getCurrentDirectory file' <- canonicalizePath file setCurrentDirectory (takeDirectory file') - _ <- runTopLevel (interpretFile file' >> interpretMain) ro rw + _ <- runTopLevel (interpretFile file' True) ro rw `X.catch` (handleException opts) setCurrentDirectory oldpath return () @@ -583,7 +588,7 @@ include_value file = do oldpath <- io $ getCurrentDirectory file' <- io $ canonicalizePath file io $ setCurrentDirectory (takeDirectory file') - interpretFile file' + interpretFile file' False io $ setCurrentDirectory oldpath set_ascii :: Bool -> TopLevel () @@ -1557,7 +1562,7 @@ primitives = Map.fromList , "goals 'prop1' and 'prop2'." ] , prim "empty_ss" "Simpset" - (pureVal emptySimpset) + (pureVal (emptySimpset :: SAWSimpset)) Current [ "The empty simplification rule set, containing no rules." ] @@ -1608,20 +1613,24 @@ primitives = Map.fromList Current [ "Add a proved equality theorem to a given simplification rule set." ] - , prim "addsimp'" "Term -> Simpset -> Simpset" - (funVal2 addsimp') - Current - [ "Add an arbitrary equality term to a given simplification rule set." ] - , prim "addsimps" "[Theorem] -> Simpset -> Simpset" (funVal2 addsimps) Current [ "Add proved equality theorems to a given simplification rule set." ] + , prim "addsimp'" "Term -> Simpset -> Simpset" + (funVal2 addsimp') + Deprecated + [ "Add an arbitrary equality term to a given simplification rule set." + , "Use `admit` or `core_axiom` and `addsimp` instead." + ] + , prim "addsimps'" "[Term] -> Simpset -> Simpset" (funVal2 addsimps') - Current - [ "Add arbitrary equality terms to a given simplification rule set." ] + Deprecated + [ "Add arbitrary equality terms to a given simplification rule set." + , "Use `admit` or `core_axiom` and `addsimps` instead." + ] , prim "rewrite" "Simpset -> Term -> Term" (funVal2 rewritePrim) @@ -2901,6 +2910,13 @@ primitives = Map.fromList [ "Print a human-readable summary of all verifications performed" , "so far." ] + + , prim "summarize_verification_json" "String -> TopLevel ()" + (pureVal summarize_verification_json) + Experimental + [ "Print a JSON summary of all verifications performed" + , "so far into the named file." + ] ] where diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index 709db3b9b5..50dccc7866 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -29,10 +29,23 @@ module SAWScript.Proof , ppProp , propToSATQuery + , TheoremDB + , newTheoremDB + , reachableTheorems + , Theorem , thmProp , thmStats , thmEvidence + , thmLocation + , thmProgramLoc + , thmReason + , thmNonce + , thmDepends + , thmElapsedTime + , thmSummary + , TheoremNonce + , TheoremSummary(..) , admitTheorem , solverTheorem @@ -77,12 +90,17 @@ module SAWScript.Proof import qualified Control.Monad.Fail as F import Control.Monad.Except +import Data.IORef import Data.Maybe (fromMaybe) +import Data.Map (Map) import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set import Data.Text (Text) import qualified Data.Text as Text +import Data.Time.Clock + +import Data.Parameterized.Nonce import Verifier.SAW.Prelude (scApplyPrelude_False) import Verifier.SAW.Recognizer @@ -98,11 +116,14 @@ import Verifier.SAW.SCTypeCheck (scTypeCheckError) import Verifier.SAW.Simulator.Concrete (evalSharedTerm) import Verifier.SAW.Simulator.Value (asFirstOrderTypeValue, Value(..), TValue(..)) +import What4.ProgramLoc (ProgramLoc) + import SAWScript.Position import SAWScript.Prover.SolverStats import SAWScript.Crucible.Common as Common import qualified Verifier.SAW.Simulator.What4 as W4Sim import qualified Verifier.SAW.Simulator.What4.ReturnTrip as W4Sim +import SAWScript.Panic(panic) -- | A proposition is a saw-core type of type `Prop`. -- In particular, this includes any pi type whose result @@ -144,9 +165,9 @@ propToTerm :: SharedContext -> Prop -> IO Term propToTerm _sc (Prop tm) = pure tm -- | Attempt to interpret a proposition as a rewrite rule. -propToRewriteRule :: SharedContext -> Prop -> IO (Maybe (RewriteRule)) -propToRewriteRule _sc (Prop tm) = - case ruleOfProp tm of +propToRewriteRule :: SharedContext -> Prop -> Maybe a -> IO (Maybe (RewriteRule a)) +propToRewriteRule _sc (Prop tm) ann = + case ruleOfProp tm ann of Nothing -> pure Nothing Just r -> pure (Just r) @@ -171,10 +192,10 @@ unfoldProp sc unints (Prop tm) = return (Prop tm') -- | Rewrite the proposition using the provided Simpset -simplifyProp :: SharedContext -> Simpset -> Prop -> IO Prop +simplifyProp :: Ord a => SharedContext -> Simpset a -> Prop -> IO (Set a, Prop) simplifyProp sc ss (Prop tm) = - do tm' <- rewriteSharedTerm sc ss tm - return (Prop tm') + do (a, tm') <- rewriteSharedTerm sc ss tm + return (a, Prop tm') -- | Evaluate the given proposition by round-tripping -- through the What4 formula representation. This will @@ -235,6 +256,8 @@ prettyProp opts (Prop tm) = scPrettyTerm opts tm ppProp :: PPOpts -> Prop -> SawDoc ppProp opts (Prop tm) = ppTerm opts tm +type TheoremNonce = Nonce GlobalNonceGenerator Theorem + -- | A theorem is a proposition which has been wrapped in a -- constructor indicating that it has already been proved, -- and contains @Evidence@ for its truth. @@ -243,12 +266,52 @@ data Theorem = { _thmProp :: Prop , _thmStats :: SolverStats , _thmEvidence :: Evidence + , _thmLocation :: Pos + , _thmProgramLoc :: Maybe ProgramLoc + , _thmReason :: Text + , _thmNonce :: TheoremNonce + , _thmDepends :: Set TheoremNonce + , _thmElapsedTime :: NominalDiffTime + , _thmSummary :: TheoremSummary } -- INVARIANT: the provided evidence is valid for the included proposition - | LocalAssumption Prop + | LocalAssumption Prop Pos TheoremNonce -- This constructor is used to construct "hypothetical" theorems that -- are intended to be used in local scopes when proving implications. +data TheoremDB = + TheoremDB + -- TODO, maybe this should be a summary or something simpler? + { theoremMap :: IORef (Map.Map TheoremNonce Theorem) + } + +newTheoremDB :: IO TheoremDB +newTheoremDB = TheoremDB <$> newIORef mempty + +recordTheorem :: TheoremDB -> Theorem -> IO Theorem +recordTheorem _ (LocalAssumption _ pos _) = + panic "recordTheorem" ["Tried to record a local assumption as a top-level", show pos] +recordTheorem db thm@Theorem{ _thmNonce = n } = + do modifyIORef (theoremMap db) (Map.insert n thm) + return thm + +reachableTheorems :: TheoremDB -> Set TheoremNonce -> IO (Map TheoremNonce Theorem) +reachableTheorems db roots = + do m <- readIORef (theoremMap db) + pure $! Set.foldl' (loop m) mempty roots + + where + loop m visited curr + | Just _ <- Map.lookup curr visited = visited + + | Just thm <- Map.lookup curr m = + Set.foldl' (loop m) + (Map.insert curr thm visited) + (thmDepends thm) + + | otherwise = + panic "reachableTheorems" ["Could not find theorem with identifier", show (indexValue curr)] + -- | Check that the purported theorem is valid. -- -- This checks that the given theorem object does not correspond @@ -258,16 +321,36 @@ data Theorem = -- does not totally guarantee the theorem is true, as it does -- not rerun any solver-provided proofs, and it accepts admitted -- propositions and quickchecked propositions as valid. -validateTheorem :: SharedContext -> Theorem -> IO () +validateTheorem :: SharedContext -> TheoremDB -> Theorem -> IO () -validateTheorem _sc (LocalAssumption p) = +validateTheorem _ _ (LocalAssumption p loc _n) = fail $ unlines - [ "Illegal use of unbound local hypothesis" + [ "Illegal use of unbound local hypothesis generated at " ++ show loc , showTerm (unProp p) ] -validateTheorem sc Theorem{ _thmProp = p, _thmEvidence = e } = - checkEvidence sc e p +validateTheorem sc db Theorem{ _thmProp = p, _thmEvidence = e, _thmDepends = thmDep } = + do (deps,_) <- checkEvidence sc db e p + unless (Set.isSubsetOf deps thmDep) + (fail $ unlines ["Theorem failed to declare its depencences correctly" + , show deps, show thmDep ]) + +data TheoremSummary + = AdmittedTheorem Text + | TestedTheorem Integer + | ProvedTheorem SolverStats + +instance Monoid TheoremSummary where + mempty = ProvedTheorem mempty + +instance Semigroup TheoremSummary where + AdmittedTheorem msg <> _ = AdmittedTheorem msg + _ <> AdmittedTheorem msg = AdmittedTheorem msg + TestedTheorem x <> TestedTheorem y = TestedTheorem (min x y) + TestedTheorem x <> _ = TestedTheorem x + _ <> TestedTheorem y = TestedTheorem y + ProvedTheorem s1 <> ProvedTheorem s2 = ProvedTheorem (s1<>s2) + -- | This datatype records evidence for the truth of a proposition. data Evidence @@ -278,7 +361,7 @@ data Evidence -- | This type of evidence refers to a local assumption that -- must have been introduced by a surrounding @AssumeEvidence@ -- constructor. - | LocalAssumptionEvidence Prop + | LocalAssumptionEvidence Prop TheoremNonce -- | This type of evidence is produced when the given proposition -- has been dispatched to a solver which has indicated that it @@ -295,7 +378,7 @@ data Evidence -- | This type of evidence is produced when the given proposition -- has been explicitly assumed without other evidence at the -- user's direction. - | Admitted String Pos Prop -- TODO, Text instead? + | Admitted Text Pos Prop -- | This type of evidence is produced when a given proposition is trivially -- true. @@ -316,7 +399,7 @@ data Evidence -- proposition must match the hypothesis of the goal, and the included -- evidence must match the conclusion of the goal. The proposition is -- allowed to appear inside the evidence as a local assumption. - | AssumeEvidence Prop Evidence + | AssumeEvidence TheoremNonce Prop Evidence -- | This type of evidence is used to prove a universally-quantified statement. | ForallEvidence (ExtCns Term) Evidence @@ -328,7 +411,7 @@ data Evidence -- | This type of evidence is used to modify a goal to prove via rewriting. -- The goal to prove is rewritten by the given simpset; then the provided -- evidence is used to check the modified goal. - | RewriteEvidence Simpset Evidence + | RewriteEvidence (Simpset TheoremNonce) Evidence -- | This type of evidence is used to modify a goal to prove via unfolding -- constant definitions. The goal to prove is modified by unfolding @@ -345,26 +428,61 @@ data Evidence -- | The the proposition proved by a given theorem. thmProp :: Theorem -> Prop -thmProp (LocalAssumption p) = p +thmProp (LocalAssumption p _loc _n) = p thmProp Theorem{ _thmProp = p } = p -- | Retrieve any solver stats from the proved theorem. thmStats :: Theorem -> SolverStats -thmStats (LocalAssumption _) = mempty +thmStats (LocalAssumption _ _ _) = mempty thmStats Theorem{ _thmStats = stats } = stats -- | Retrive the evidence associated with this theorem. thmEvidence :: Theorem -> Evidence -thmEvidence (LocalAssumption p) = LocalAssumptionEvidence p +thmEvidence (LocalAssumption p _ n) = LocalAssumptionEvidence p n thmEvidence Theorem{ _thmEvidence = e } = e +-- | The SAW source location that generated this theorem +thmLocation :: Theorem -> Pos +thmLocation (LocalAssumption _p loc _) = loc +thmLocation Theorem{ _thmLocation = loc } = loc + +-- | The program location (if any) of the program under +-- verification giving rise to this theorem +thmProgramLoc :: Theorem -> Maybe ProgramLoc +thmProgramLoc (LocalAssumption{}) = Nothing +thmProgramLoc Theorem{ _thmProgramLoc = ploc } = ploc + +-- | Describes the reason this theorem was generated +thmReason :: Theorem -> Text +thmReason (LocalAssumption _ _ _) = "local assumption" +thmReason Theorem{ _thmReason = r } = r + +-- | Returns a unique identifier for this theorem +thmNonce :: Theorem -> TheoremNonce +thmNonce (LocalAssumption _ _ n) = n +thmNonce Theorem{ _thmNonce = n } = n + +-- | Returns the set of theorem identifiers that this theorem depends on +thmDepends :: Theorem -> Set TheoremNonce +thmDepends LocalAssumption{} = mempty +thmDepends Theorem { _thmDepends = s } = s + +-- | Returns the amount of time elapsed during the proof of this theorem +thmElapsedTime :: Theorem -> NominalDiffTime +thmElapsedTime LocalAssumption{} = 0 +thmElapsedTime Theorem{ _thmElapsedTime = tm } = tm + +thmSummary :: Theorem -> TheoremSummary +thmSummary LocalAssumption{} = mempty +thmSummary Theorem { _thmSummary = sy } = sy + splitEvidence :: [Evidence] -> IO Evidence splitEvidence [e1,e2] = pure (SplitEvidence e1 e2) splitEvidence _ = fail "splitEvidence: expected two evidence values" -assumeEvidence :: Prop -> [Evidence] -> IO Evidence -assumeEvidence p [e] = pure (AssumeEvidence p e) -assumeEvidence _ _ = fail "assumeEvidence: expected one evidence value" +assumeEvidence :: TheoremNonce -> Prop -> [Evidence] -> IO Evidence +assumeEvidence n p [e] = pure (AssumeEvidence n p e) +assumeEvidence _ _ _ = fail "assumeEvidence: expected one evidence value" forallEvidence :: ExtCns Term -> [Evidence] -> IO Evidence forallEvidence x [e] = pure (ForallEvidence x e) @@ -375,50 +493,106 @@ cutEvidence thm [e] = pure (CutEvidence thm e) cutEvidence _ _ = fail "cutEvidence: expected one evidence value" -- | Construct a theorem directly via a proof term. -proofByTerm :: SharedContext -> Term -> IO Theorem -proofByTerm sc prf = +proofByTerm :: SharedContext -> TheoremDB -> Term -> Pos -> Text -> IO Theorem +proofByTerm sc db prf loc rsn = do ty <- scTypeOf sc prf p <- termToProp sc ty - return + n <- freshNonce globalNonceGenerator + recordTheorem db Theorem { _thmProp = p , _thmStats = mempty , _thmEvidence = ProofTerm prf + , _thmLocation = loc + , _thmProgramLoc = Nothing + , _thmReason = rsn + , _thmNonce = n + , _thmDepends = mempty + , _thmElapsedTime = 0 + , _thmSummary = ProvedTheorem mempty } -- | Construct a theorem directly from a proposition and evidence -- for that proposition. The evidence will be validated to -- check that it supports the given proposition; if not, an -- error will be raised. -constructTheorem :: SharedContext -> Prop -> Evidence -> IO Theorem -constructTheorem sc p e = - do checkEvidence sc e p - return +constructTheorem :: + SharedContext -> + TheoremDB -> + Prop -> + Evidence -> + Pos -> + Maybe ProgramLoc -> + Text -> + NominalDiffTime -> + IO Theorem +constructTheorem sc db p e loc ploc rsn elapsed = + do (deps,sy) <- checkEvidence sc db e p + n <- freshNonce globalNonceGenerator + recordTheorem db Theorem { _thmProp = p , _thmStats = mempty , _thmEvidence = e + , _thmLocation = loc + , _thmProgramLoc = ploc + , _thmReason = rsn + , _thmNonce = n + , _thmDepends = deps + , _thmElapsedTime = elapsed + , _thmSummary = sy } -- | Admit the given theorem without evidence. -- The provided message allows the user to -- explain why this proposition is being admitted. -admitTheorem :: String -> Pos -> Prop -> Theorem -admitTheorem msg pos p = - Theorem - { _thmProp = p - , _thmStats = solverStats "ADMITTED" (propSize p) - , _thmEvidence = Admitted msg pos p - } +admitTheorem :: + TheoremDB -> + Text -> + Prop -> + Pos -> + Text -> + IO Theorem +admitTheorem db msg p loc rsn = + do n <- freshNonce globalNonceGenerator + recordTheorem db + Theorem + { _thmProp = p + , _thmStats = solverStats "ADMITTED" (propSize p) + , _thmEvidence = Admitted msg loc p + , _thmLocation = loc + , _thmProgramLoc = Nothing + , _thmReason = rsn + , _thmNonce = n + , _thmDepends = mempty + , _thmElapsedTime = 0 + , _thmSummary = AdmittedTheorem msg + } -- | Construct a theorem that an external solver has proved. -solverTheorem :: Prop -> SolverStats -> Theorem -solverTheorem p stats = - Theorem - { _thmProp = p - , _thmStats = stats - , _thmEvidence = SolverEvidence stats p - } +solverTheorem :: + TheoremDB -> + Prop -> + SolverStats -> + Pos -> + Text -> + NominalDiffTime -> + IO Theorem +solverTheorem db p stats loc rsn elapsed = + do n <- freshNonce globalNonceGenerator + recordTheorem db + Theorem + { _thmProp = p + , _thmStats = stats + , _thmEvidence = SolverEvidence stats p + , _thmLocation = loc + , _thmReason = rsn + , _thmProgramLoc = Nothing + , _thmNonce = n + , _thmDepends = mempty + , _thmElapsedTime = elapsed + , _thmSummary = ProvedTheorem stats + } -- | A @ProofGoal@ contains a proposition to be proved, along with -- some metadata. @@ -468,10 +642,11 @@ predicateToProp sc quant = loop [] data ProofState = ProofState { _psGoals :: [ProofGoal] - , _psConcl :: Prop + , _psConcl :: (Prop,Pos,Maybe ProgramLoc,Text) , _psStats :: SolverStats , _psTimeout :: Maybe Integer , _psEvidence :: [Evidence] -> IO Evidence + , _psStartTime :: UTCTime } psTimeout :: ProofState -> Maybe Integer @@ -483,31 +658,39 @@ psGoals = _psGoals psStats :: ProofState -> SolverStats psStats = _psStats --- | Verify that the given evidence in fact supports --- the given proposition. -checkEvidence :: SharedContext -> Evidence -> Prop -> IO () -checkEvidence sc = check mempty +-- | Verify that the given evidence in fact supports the given proposition. +-- Returns the identifers of all the theorems depened on while checking evidence. +checkEvidence :: SharedContext -> TheoremDB -> Evidence -> Prop -> IO (Set TheoremNonce, TheoremSummary) +checkEvidence sc db = \e p -> do hyps <- Map.keysSet <$> readIORef (theoremMap db) + check hyps e p + where - checkApply _hyps (Prop p) [] = return p + checkApply _hyps (Prop p) [] = return (mempty, mempty, p) checkApply hyps (Prop p) (e:es) | Just (_lnm, tp, body) <- asPi p , looseVars body == emptyBitSet - = do check hyps e =<< termToProp sc tp - checkApply hyps (Prop body) es + = do (d1,sy1) <- check hyps e =<< termToProp sc tp + (d2,sy2,p') <- checkApply hyps (Prop body) es + return (Set.union d1 d2, sy1 <> sy2, p') | otherwise = fail $ unlines [ "Apply evidence mismatch: non-function or dependent function" , showTerm p ] - checkTheorem :: Set Term -> Theorem -> IO () - checkTheorem hyps (LocalAssumption p) = - unless (Set.member (unProp p) hyps) $ fail $ unlines + checkTheorem :: Set TheoremNonce -> Theorem -> IO () + checkTheorem hyps (LocalAssumption p loc n) = + unless (Set.member n hyps) $ fail $ unlines [ "Attempt to reference a local hypothesis that is not in scope" + , "Generated at " ++ show loc , showTerm (unProp p) ] checkTheorem _hyps Theorem{} = return () - check :: Set Term -> Evidence -> Prop -> IO () + check :: + Set TheoremNonce -> + Evidence -> + Prop -> + IO (Set TheoremNonce, TheoremSummary) check hyps e p@(Prop ptm) = case e of ProofTerm tm -> do ty <- scTypeCheckError sc tm @@ -517,43 +700,49 @@ checkEvidence sc = check mempty , showTerm ptm , showTerm tm ] + return (mempty, ProvedTheorem mempty) - LocalAssumptionEvidence (Prop l) -> - unless (Set.member l hyps) $ fail $ unlines + LocalAssumptionEvidence (Prop l) n -> + do unless (Set.member n hyps) $ fail $ unlines [ "Illegal use of local hypothesis" , showTerm l ] + return (Set.singleton n, ProvedTheorem mempty) - SolverEvidence _stats (Prop p') -> + SolverEvidence stats (Prop p') -> do ok <- scConvertible sc False ptm p' unless ok $ fail $ unlines [ "Solver proof does not prove the required proposition" , showTerm ptm , showTerm p' ] + return (mempty, ProvedTheorem stats) Admitted msg pos (Prop p') -> do ok <- scConvertible sc False ptm p' unless ok $ fail $ unlines [ "Admitted proof does not match the required proposition " ++ show pos - , msg + , Text.unpack msg , showTerm ptm , showTerm p' ] + return (mempty, AdmittedTheorem msg) - QuickcheckEvidence _n (Prop p') -> + QuickcheckEvidence n (Prop p') -> do ok <- scConvertible sc False ptm p' unless ok $ fail $ unlines [ "Quickcheck evidence does not match the required proposition" , showTerm ptm , showTerm p' ] + return (mempty, TestedTheorem n) TrivialEvidence -> - unless (propIsTrivial p) $ fail $ unlines - [ "Proposition is not trivial" - , showTerm ptm - ] + do unless (propIsTrivial p) $ fail $ unlines + [ "Proposition is not trivial" + , showTerm ptm + ] + return mempty SplitEvidence e1 e2 -> splitProp sc p >>= \case @@ -562,37 +751,45 @@ checkEvidence sc = check mempty , showTerm ptm ] Just (p1,p2) -> - do check hyps e1 p1 - check hyps e2 p2 + do d1 <- check hyps e1 p1 + d2 <- check hyps e2 p2 + return (d1 <> d2) ApplyEvidence thm es -> do checkTheorem hyps thm - p' <- checkApply hyps (thmProp thm) es + (d,sy,p') <- checkApply hyps (thmProp thm) es ok <- scConvertible sc False ptm p' unless ok $ fail $ unlines [ "Apply evidence does not match the required proposition" , showTerm ptm , showTerm p' ] + return (Set.insert (thmNonce thm) d, sy) CutEvidence thm e' -> do checkTheorem hyps thm p' <- scFun sc (unProp (thmProp thm)) ptm - check hyps e' (Prop p') + (d,sy) <- check hyps e' (Prop p') + return (Set.insert (thmNonce thm) d, sy) UnfoldEvidence vars e' -> do p' <- unfoldProp sc vars p check hyps e' p' RewriteEvidence ss e' -> - do p' <- simplifyProp sc ss p - check hyps e' p' + do (d1,p') <- simplifyProp sc ss p + unless (Set.isSubsetOf d1 hyps) $ fail $ unlines + [ "Rewrite step used theorem not in hypothesis database" + , show (Set.difference d1 hyps) + ] + (d2,sy) <- check hyps e' p' + return (Set.union d1 d2, sy) EvalEvidence vars e' -> do p' <- evalProp sc vars p check hyps e' p' - AssumeEvidence (Prop p') e' -> + AssumeEvidence n (Prop p') e' -> case asPi ptm of Nothing -> fail $ unlines ["Assume evidence expected function prop", showTerm ptm] Just (_lnm, ty, body) -> @@ -606,7 +803,8 @@ checkEvidence sc = check mempty [ "Assume evidence cannot be used on a dependent proposition" , showTerm ptm ] - check (Set.insert p' hyps) e' (Prop body) + (d,sy) <- check (Set.insert n hyps) e' (Prop body) + return (Set.delete n d, sy) ForallEvidence x e' -> case asPi ptm of @@ -639,23 +837,35 @@ setProofTimeout :: Integer -> ProofState -> ProofState setProofTimeout to ps = ps { _psTimeout = Just to } -- | Initialize a proof state with a single goal to prove. -startProof :: ProofGoal -> ProofState -startProof g = ProofState [g] (goalProp g) mempty Nothing passthroughEvidence +startProof :: ProofGoal -> Pos -> Maybe ProgramLoc -> Text -> IO ProofState +startProof g pos ploc rsn = + do start <- getCurrentTime + pure (ProofState [g] (goalProp g,pos,ploc,rsn) mempty Nothing passthroughEvidence start) -- | Attempt to complete a proof by checking that all subgoals have been discharged, -- and validate the computed evidence to ensure that it supports the original -- proposition. If successful, return the completed @Theorem@ and a summary -- of solver resources used in the proof. -finishProof :: SharedContext -> ProofState -> IO ProofResult -finishProof sc ps@(ProofState gs concl stats _ checkEv) = +finishProof :: SharedContext -> TheoremDB -> ProofState -> IO ProofResult +finishProof sc db ps@(ProofState gs (concl,loc,ploc,rsn) stats _ checkEv start) = case gs of [] -> do e <- checkEv [] - checkEvidence sc e concl - let thm = Theorem + (deps,sy) <- checkEvidence sc db e concl + n <- freshNonce globalNonceGenerator + end <- getCurrentTime + thm <- recordTheorem db + Theorem { _thmProp = concl , _thmStats = stats , _thmEvidence = e + , _thmLocation = loc + , _thmProgramLoc = ploc + , _thmReason = rsn + , _thmNonce = n + , _thmDepends = deps + , _thmElapsedTime = diffUTCTime end start + , _thmSummary = sy } pure (ValidProof stats thm) _ : _ -> @@ -688,7 +898,7 @@ newtype Tactic m a = -- | Choose the first subgoal in the current proof state and apply the given -- proof tactic. withFirstGoal :: F.MonadFail m => Tactic m a -> ProofState -> m (Either (SolverStats, CEX) (a, ProofState)) -withFirstGoal (Tactic f) (ProofState goals concl stats timeout evidenceCont) = +withFirstGoal (Tactic f) (ProofState goals concl stats timeout evidenceCont start) = case goals of [] -> fail "ProofScript failed: no subgoal" g : gs -> runExceptT (f g) >>= \case @@ -698,7 +908,7 @@ withFirstGoal (Tactic f) (ProofState goals concl stats timeout evidenceCont) = do let (es1, es2) = splitAt (length gs') es e <- buildTacticEvidence es1 evidenceCont (e:es2) - return (Right (x, ProofState (gs' <> gs) concl (stats <> stats') timeout evidenceCont')) + return (Right (x, ProofState (gs' <> gs) concl (stats <> stats') timeout evidenceCont' start)) predicateToSATQuery :: SharedContext -> Set VarIndex -> Term -> IO SATQuery predicateToSATQuery sc unintSet tm0 = @@ -849,15 +1059,16 @@ tacticIntro sc usernm = Tactic \goal -> -- hypothesis. Return a @Theorem@ representing this local assumption. -- This hypothesis should only be used for proving subgoals arising -- from this call to @tacticAssume@ or evidence verification will later fail. -tacticAssume :: (F.MonadFail m, MonadIO m) => SharedContext -> Tactic m Theorem -tacticAssume _sc = Tactic \goal -> +tacticAssume :: (F.MonadFail m, MonadIO m) => SharedContext -> Pos -> Tactic m Theorem +tacticAssume _sc loc = Tactic \goal -> case asPi (unProp (goalProp goal)) of Just (_nm, tp, body) | looseVars body == emptyBitSet -> do let goal' = goal{ goalProp = Prop body } let p = Prop tp - let thm' = LocalAssumption p - return (thm', mempty, [goal'], assumeEvidence p) + n <- liftIO (freshNonce globalNonceGenerator) + let thm' = LocalAssumption p loc n + return (thm', mempty, [goal'], assumeEvidence n p) _ -> fail "assume tactic failed: not a function, or a dependent function" diff --git a/src/SAWScript/Prover/Rewrite.hs b/src/SAWScript/Prover/Rewrite.hs index 7de2ebaea0..67f2643992 100644 --- a/src/SAWScript/Prover/Rewrite.hs +++ b/src/SAWScript/Prover/Rewrite.hs @@ -18,7 +18,7 @@ import Verifier.SAW.Term.Functor(preludeName, mkIdent, Ident, mkModuleName) import Verifier.SAW.Conversion import Verifier.SAW.SharedTerm(SharedContext,scFindDef) -basic_ss :: SharedContext -> IO Simpset +basic_ss :: SharedContext -> IO (Simpset a) basic_ss sc = do rs1 <- concat <$> traverse (defRewrites sc) defs rs2 <- scEqsRewriteRules sc eqs @@ -69,7 +69,7 @@ basic_ss sc = -defRewrites :: SharedContext -> Ident -> IO [RewriteRule] +defRewrites :: SharedContext -> Ident -> IO [RewriteRule a] defRewrites sc ident = scFindDef sc ident >>= \maybe_def -> case maybe_def of diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index eeed97aa45..2dd2a83e89 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -126,15 +126,15 @@ data Value -- operations in these monads can fail at runtime. | VTopLevel (TopLevel Value) | VProofScript (ProofScript Value) - | VSimpset Simpset + | VSimpset SAWSimpset | VTheorem Theorem ----- | VLLVMCrucibleSetup !(LLVMCrucibleSetupM Value) - | VLLVMCrucibleMethodSpec (CMSLLVM.SomeLLVM CMS.CrucibleMethodSpecIR) + | VLLVMCrucibleMethodSpec (CMSLLVM.SomeLLVM CMS.ProvedSpec) | VLLVMCrucibleSetupValue (CMSLLVM.AllLLVM CMS.SetupValue) ----- | VJVMSetup !(JVMSetupM Value) - | VJVMMethodSpec !(CMS.CrucibleMethodSpecIR CJ.JVM) + | VJVMMethodSpec !(CMS.ProvedSpec CJ.JVM) | VJVMSetupValue !(CMS.SetupValue CJ.JVM) ----- | VLLVMModuleSkeleton ModuleSkeleton @@ -154,6 +154,8 @@ data Value | VCFG SAW_CFG | VGhostVar CMS.GhostGlobal +type SAWSimpset = Simpset TheoremNonce + data AIGNetwork where AIGNetwork :: (Typeable l, Typeable g, AIG.IsAIG l g) => AIG.Network l g -> AIGNetwork @@ -165,7 +167,7 @@ data SAW_CFG where JVM_CFG :: Crucible.AnyCFG JVM -> SAW_CFG data BuiltinContext = BuiltinContext { biSharedContext :: SharedContext - , biBasicSS :: Simpset + , biBasicSS :: SAWSimpset } deriving Generic @@ -220,7 +222,7 @@ showsProofResult opts r = case r of ValidProof _ _ -> showString "Valid" InvalidProof _ ts _ -> showString "Invalid: [" . showMulti "" ts - UnfinishedProof st -> showString "Unfinished: " . shows (length (psGoals st)) . showString " goals remaining" + UnfinishedProof st -> showString "Unfinished: " . shows (length (psGoals st)) . showString " goals remaining" where opts' = sawPPOpts opts showVal t = shows (ppFirstOrderValue opts' t) @@ -245,7 +247,7 @@ showsSatResult opts r = showMulti _ [] = showString "]" showMulti s (eqn : eqns) = showString s . showEqn eqn . showMulti ", " eqns -showSimpset :: PPOpts -> Simpset -> String +showSimpset :: PPOpts -> Simpset a -> String showSimpset opts ss = unlines ("Rewrite Rules" : "=============" : map (show . ppRule) (listRules ss)) where @@ -382,7 +384,8 @@ data TopLevelRO = , roPosition :: SS.Pos , roProxy :: AIGProxy , roInitWorkDir :: FilePath - , roBasicSS :: Simpset + , roBasicSS :: SAWSimpset + , roTheoremDB :: TheoremDB } data TopLevelRW = @@ -459,7 +462,7 @@ getOptions = TopLevel (asks roOptions) getProxy :: TopLevel AIGProxy getProxy = TopLevel (asks roProxy) -getBasicSS :: TopLevel Simpset +getBasicSS :: TopLevel SAWSimpset getBasicSS = TopLevel (asks roBasicSS) localOptions :: (Options -> Options) -> TopLevel a -> TopLevel a @@ -488,10 +491,12 @@ putTopLevelRW :: TopLevelRW -> TopLevel () putTopLevelRW rw = TopLevel (put rw) returnProof :: IsValue v => v -> TopLevel v -returnProof v = do - rw <- getTopLevelRW - putTopLevelRW rw { rwProofs = toValue v : rwProofs rw } - return v +returnProof v = recordProof v >> return v + +recordProof :: IsValue v => v -> TopLevel () +recordProof v = + do rw <- getTopLevelRW + putTopLevelRW rw { rwProofs = toValue v : rwProofs rw } -- | Access the current state of Java Class translation getJVMTrans :: TopLevel CJ.JVMContext @@ -605,14 +610,17 @@ newtype JVMSetupM a = JVMSetupM { runJVMSetupM :: JVMSetup a } newtype ProofScript a = ProofScript { unProofScript :: ExceptT (SolverStats, CEX) (StateT ProofState TopLevel) a } deriving (Functor, Applicative, Monad) -runProofScript :: ProofScript a -> ProofGoal -> TopLevel ProofResult -runProofScript (ProofScript m) gl = - do (r,pstate) <- runStateT (runExceptT m) (startProof gl) +runProofScript :: ProofScript a -> ProofGoal -> Maybe ProgramLoc -> Text -> TopLevel ProofResult +runProofScript (ProofScript m) gl ploc rsn = + do pos <- getPosition + ps <- io (startProof gl pos ploc rsn) + (r,pstate) <- runStateT (runExceptT m) ps case r of Left (stats,cex) -> return (InvalidProof stats cex pstate) Right _ -> do sc <- getSharedContext - io (finishProof sc pstate) + db <- roTheoremDB <$> getTopLevelRO + io (finishProof sc db pstate) scriptTopLevel :: TopLevel a -> ProofScript a scriptTopLevel m = ProofScript (lift (lift m)) @@ -760,19 +768,19 @@ instance FromValue SAW_CFG where fromValue (VCFG t) = t fromValue _ = error "fromValue CFG" -instance IsValue (CMSLLVM.SomeLLVM CMS.CrucibleMethodSpecIR) where +instance IsValue (CMSLLVM.SomeLLVM CMS.ProvedSpec) where toValue mir = VLLVMCrucibleMethodSpec mir -instance FromValue (CMSLLVM.SomeLLVM CMS.CrucibleMethodSpecIR) where +instance FromValue (CMSLLVM.SomeLLVM CMS.ProvedSpec) where fromValue (VLLVMCrucibleMethodSpec mir) = mir - fromValue _ = error "fromValue CrucibleMethodSpecIR" + fromValue _ = error "fromValue ProvedSpec LLVM" -instance IsValue (CMS.CrucibleMethodSpecIR CJ.JVM) where +instance IsValue (CMS.ProvedSpec CJ.JVM) where toValue t = VJVMMethodSpec t -instance FromValue (CMS.CrucibleMethodSpecIR CJ.JVM) where +instance FromValue (CMS.ProvedSpec CJ.JVM) where fromValue (VJVMMethodSpec t) = t - fromValue _ = error "fromValue CrucibleMethodSpecIR" + fromValue _ = error "fromValue ProvedSpec JVM" instance IsValue ModuleSkeleton where toValue s = VLLVMModuleSkeleton s @@ -867,10 +875,10 @@ instance FromValue Bool where fromValue (VBool b) = b fromValue _ = error "fromValue Bool" -instance IsValue Simpset where +instance IsValue SAWSimpset where toValue ss = VSimpset ss -instance FromValue Simpset where +instance FromValue SAWSimpset where fromValue (VSimpset ss) = ss fromValue _ = error "fromValue Simpset" diff --git a/src/SAWScript/VerificationSummary.hs b/src/SAWScript/VerificationSummary.hs index 56f96411ee..60799cdd1a 100644 --- a/src/SAWScript/VerificationSummary.hs +++ b/src/SAWScript/VerificationSummary.hs @@ -16,11 +16,13 @@ module SAWScript.VerificationSummary ) where import Control.Lens ((^.)) +import qualified Data.Map as Map import qualified Data.Set as Set import Data.String import Prettyprinter -import Data.Aeson (encode, (.=), Value(..), object) +import Data.Aeson (encode, (.=), Value(..), object, toJSON) import qualified Data.ByteString.Lazy.UTF8 as BLU +import Data.Parameterized.Nonce import qualified Lang.Crucible.JVM as CJ import SAWScript.Crucible.Common.MethodSpec @@ -30,10 +32,11 @@ import qualified SAWScript.Crucible.JVM.MethodSpecIR as CMSJVM import SAWScript.Proof import SAWScript.Prover.SolverStats import qualified Verifier.SAW.Term.Pretty as PP -import What4.ProgramLoc (ProgramLoc(plSourceLoc)) +import What4.ProgramLoc (ProgramLoc(..)) +import What4.FunctionName -type JVMTheorem = CMS.CrucibleMethodSpecIR CJ.JVM -type LLVMTheorem = CMSLLVM.SomeLLVM CMS.CrucibleMethodSpecIR +type JVMTheorem = CMS.ProvedSpec CJ.JVM +type LLVMTheorem = CMSLLVM.SomeLLVM CMS.ProvedSpec data VerificationSummary = VerificationSummary @@ -45,8 +48,8 @@ data VerificationSummary = vsVerifSolvers :: VerificationSummary -> Set.Set String vsVerifSolvers vs = Set.unions $ - map (\ms -> solverStatsSolvers (ms ^. csSolverStats)) (vsJVMMethodSpecs vs) ++ - map (\(CMSLLVM.SomeLLVM ms) -> solverStatsSolvers (ms ^. csSolverStats)) (vsLLVMMethodSpecs vs) + map (\ms -> solverStatsSolvers (ms ^. psSolverStats)) (vsJVMMethodSpecs vs) ++ + map (\(CMSLLVM.SomeLLVM ms) -> solverStatsSolvers (ms ^. psSolverStats)) (vsLLVMMethodSpecs vs) vsTheoremSolvers :: VerificationSummary -> Set.Set String vsTheoremSolvers = Set.unions . map getSolvers . vsTheorems @@ -55,30 +58,68 @@ vsTheoremSolvers = Set.unions . map getSolvers . vsTheorems vsAllSolvers :: VerificationSummary -> Set.Set String vsAllSolvers vs = Set.union (vsVerifSolvers vs) (vsTheoremSolvers vs) -computeVerificationSummary :: [JVMTheorem] -> [LLVMTheorem] -> [Theorem] -> VerificationSummary -computeVerificationSummary = VerificationSummary +computeVerificationSummary :: TheoremDB -> [JVMTheorem] -> [LLVMTheorem] -> [Theorem] -> IO VerificationSummary +computeVerificationSummary db js ls thms = + do let roots = mconcat ( + [ j ^. psTheoremDeps | j <- js ] ++ + [ l ^. psTheoremDeps | CMSLLVM.SomeLLVM l <- ls ] ++ + [ Set.singleton (thmNonce t) | t <- thms ]) + thms' <- Map.elems <$> reachableTheorems db roots + pure (VerificationSummary js ls thms') -- TODO: we could make things instances of a ToJSON typeclass instead of using the two methods below. -msToJSON :: forall ext . Pretty (MethodId ext) => CMS.CrucibleMethodSpecIR ext -> Value +msToJSON :: forall ext . Pretty (MethodId ext) => CMS.ProvedSpec ext -> Value msToJSON cms = object [ ("type" .= ("method" :: String)) - , ("method" .= (show $ pretty $ cms ^. csMethod)) - , ("loc" .= (show $ pretty $ plSourceLoc $ cms ^. csLoc)) - , ("status" .= (statusString $ cms ^. csSolverStats)) - , ("specification" .= ("unknown" :: String)) -- TODO + , ("id" .= (indexValue $ cms ^. psSpecIdent)) + , ("method" .= (show $ pretty $ cms ^. psSpec.csMethod)) + , ("loc" .= (show $ pretty $ plSourceLoc $ cms ^. psSpec.csLoc)) + , ("status" .= case cms ^. psProofMethod of + SpecAdmitted -> "assumed" :: String + SpecProved -> "verified") +-- , ("specification" .= ("unknown" :: String)) -- TODO + , ("dependencies" .= toJSON + (map indexValue (Set.toList (cms ^. psSpecDeps)) ++ + map indexValue (Set.toList (cms ^. psTheoremDeps)))) + , ("elapsedtime" .= toJSON (cms ^. psElapsedTime)) ] thmToJSON :: Theorem -> Value -thmToJSON thm = object [ +thmToJSON thm = object ([ ("type" .= ("property" :: String)) - , ("loc" .= ("unknown" :: String)) -- TODO: Theorem has no attached location information - , ("status" .= (statusString $ thmStats thm)) - , ("term" .= (show $ ppProp PP.defaultPPOpts $ thmProp thm)) + , ("id" .= (indexValue $ thmNonce thm)) + , ("loc" .= (show $ thmLocation thm)) + , ("reason" .= (thmReason thm)) + , ("dependencies" .= toJSON (map indexValue (Set.toList (thmDepends thm)))) + , ("elapsedtime" .= toJSON (thmElapsedTime thm)) + ] ++ theoremStatus + ++ case thmProgramLoc thm of + Nothing -> [] + Just ploc -> [("ploc" .= plocToJSON ploc)] + ) + where + theoremStatus = case thmSummary thm of + ProvedTheorem stats -> + [ ("status" .= ("verified" :: String)) + , ("provers" .= toJSON (Set.toList (solverStatsSolvers stats))) + ] + TestedTheorem n -> + [ ("status" .= ("tested" :: String)) + , ("numtests" .= toJSON n) + ] + AdmittedTheorem msg -> + [ ("status" .= ("assumed" :: String)) + , ("admitmsg" .= msg) + ] + +-- , ("term" .= (show $ ppProp PP.defaultPPOpts $ thmProp thm)) + +plocToJSON :: ProgramLoc -> Value +plocToJSON ploc = object + [ "function" .= toJSON (functionName (plFunction ploc)) + , "loc" .= show (plSourceLoc ploc) ] -statusString :: SolverStats -> String -statusString stats = if ((Set.null s) || (Set.member "ADMITTED" s)) then "assumed" else "verified" - where s = solverStatsSolvers stats jsonVerificationSummary :: VerificationSummary -> String jsonVerificationSummary (VerificationSummary jspecs lspecs thms) = @@ -103,9 +144,9 @@ prettyVerificationSummary vs@(VerificationSummary jspecs lspecs thms) = sectionWithItems _ _ [] = mempty sectionWithItems nm prt items = vsep [section nm, "", vsep (map prt items)] - verifStatus s = if Set.null (solverStatsSolvers (s ^. CMS.csSolverStats)) - then "assumed" - else "verified" + verifStatus s = case s ^. CMS.psProofMethod of + CMS.SpecAdmitted -> "assumed" + CMS.SpecProved -> "verified" -- TODO: ultimately the goal is for the following to summarize all -- preconditions made by this verification, but we need to extract -- a bunch more information for that to be meaningful. @@ -117,14 +158,14 @@ prettyVerificationSummary vs@(VerificationSummary jspecs lspecs thms) = prettyJVMSpecs ss = sectionWithItems "JVM Methods Analyzed" prettyJVMSpec ss prettyJVMSpec s = - vsep [ item (fromString (s ^. CMSJVM.csMethodName)) + vsep [ item (fromString (s ^. CMS.psSpec.CMSJVM.csMethodName)) -- , subitem (condStatus s) , subitem (verifStatus s) ] prettyLLVMSpecs ss = sectionWithItems "LLVM Functions Analyzed" prettyLLVMSpec ss prettyLLVMSpec (CMSLLVM.SomeLLVM s) = - vsep [ item (fromString (s ^. CMSLLVM.csName)) + vsep [ item (fromString (s ^. CMS.psSpec.CMSLLVM.csName)) -- , subitem (condStatus s) , subitem (verifStatus s) ] diff --git a/verif-viewer/tools/VerifViewer.hs b/verif-viewer/tools/VerifViewer.hs new file mode 100644 index 0000000000..0d8ddef5e3 --- /dev/null +++ b/verif-viewer/tools/VerifViewer.hs @@ -0,0 +1,295 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} + +module Main where + +import Control.Monad +import Data.Aeson +import Data.Aeson.Types (Parser) +import qualified Data.Aeson.Types as AE +import Data.Maybe (isJust) +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Foldable (toList) +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.Text.Lazy as TL +import qualified Data.Text.Lazy.IO as TL +import qualified Data.Set as Set +import System.IO +import System.Exit (exitFailure) +import System.Environment (getArgs) +import Data.Time.Clock + +import qualified Data.Attoparsec.ByteString as AT +import qualified Data.ByteString as BS +import qualified Data.GraphViz as GV +import qualified Data.GraphViz.Attributes as GV +import qualified Data.GraphViz.Attributes.Complete as GV +import qualified Data.GraphViz.Printing as GV +import qualified Data.GraphViz.Attributes.HTML as HTML + +main :: IO () +main = + do [f,o] <- getArgs + bs <- BS.readFile f + case AT.parseOnly json' bs of + Left msg -> putStrLn msg >> exitFailure + Right v -> + case AE.parse parseNodes v of + AE.Error msg -> putStrLn msg >> exitFailure + AE.Success ns -> handleNodes o ns + +handleNodes :: FilePath -> [SummaryNode] -> IO () +handleNodes o ns = TL.writeFile o (GV.renderDot (GV.toDot dot)) + where + dot = GV.graphElemsToDot params nodes uniqEdges + + params :: GV.GraphvizParams Integer SummaryNode () Integer SummaryNode + params = GV.defaultParams + { GV.fmtNode = fmt + , GV.globalAttributes = + [ GV.GraphAttrs [ GV.RankDir GV.FromLeft , GV.RankSep [2.0], GV.Splines GV.Ortho ] ] + } + + nodeMap :: Map Integer SummaryNode + nodeMap = Map.fromList [ (summaryNodeId n, n) | n <- ns ] + + revMethodDep :: Map Integer Integer + revMethodDep = Map.fromList $ + do MethodSummary i s <- ns + t <- methodDeps s + Just (TheoremSummary _ _) <- pure (Map.lookup t nodeMap) + pure (t, i) + + nodes :: [(Integer,SummaryNode)] + nodes = do n <- ns + if isVCGoal (summaryNodeId n) then [] else pure (summaryNodeId n, n) + + isVCGoal :: Integer -> Bool + isVCGoal i = isJust (Map.lookup i revMethodDep) + + uniqEdges :: [(Integer,Integer,())] + uniqEdges = Set.toList (Set.fromList edges) + + edges :: [(Integer,Integer,())] + edges = do n <- ns + let i = case n of + TheoremSummary i thm + | Just parent <- Map.lookup i revMethodDep -> parent + _ -> summaryNodeId n + n' <- filter (not . isVCGoal) (summaryNodeDeps n) + pure (i,n',()) + + fmt :: (Integer, SummaryNode) -> GV.Attributes + fmt (_, TheoremSummary _ s) = fmtThm s + fmt (_, MethodSummary _ s) = fmtMethod nodeMap s + + +fmtThm :: TheoremNode -> GV.Attributes +fmtThm thm = [ GV.shape GV.Trapezium + , GV.Tooltip (TL.fromStrict (thmTooltip thm)) + , GV.textLabel (TL.fromStrict lab) + , GV.style GV.filled + , GV.FillColor [GV.toWC (thmColor thm)] + ] + + where + lab = thmStatusText thm <> "\n" <> T.pack (show (thmElapsedTime thm)) + + +fmtMethod :: Map Integer SummaryNode -> MethodNode -> GV.Attributes +fmtMethod nodeMap mn = [ GV.Label (GV.HtmlLabel top), GV.Shape GV.PlainText ] + where + top = + if null subs then + HTML.Table (HTML.HTable Nothing [HTML.CellBorder 0] [ HTML.Cells [main] ]) + else + HTML.Table (HTML.HTable Nothing [HTML.CellBorder 0] [ HTML.Cells [main], HTML.Cells [subsTab]]) + + main = HTML.LabelCell + [ HTML.Title (TL.fromStrict maintt) + , HTML.HRef "#" + , HTML.BGColor fillcol + ] + (HTML.Text [ HTML.Str (TL.fromStrict maintext) ]) + + subsTab :: HTML.Cell + subsTab = HTML.LabelCell [] (HTML.Table (HTML.HTable Nothing [HTML.Border 0, HTML.CellBorder 1] [HTML.Cells subs])) + + vcs = do d <- methodDeps mn + Just (TheoremSummary i thm) <- pure (Map.lookup d nodeMap) + pure (i,thm) + + subs :: [HTML.Cell] + subs = map (uncurry mkSub) vcs + + mkSub :: Integer -> TheoremNode -> HTML.Cell + mkSub i thm = HTML.LabelCell attrs (HTML.Text [ HTML.Str (TL.fromStrict (T.pack (show (thmElapsedTime thm)))) ]) + where + attrs = + [ HTML.BGColor (thmColor thm) + , HTML.Title (TL.fromStrict (thmStatusText thm <> "\n" <> thmTooltip thm)) + , HTML.HRef "#" + ] + + fillcol = statusColor $ + foldr (<>) (methodToStatus mn) (map (thmToStatus . snd) vcs) + + maintext = + T.intercalate "\n" + [ methodName mn + , T.pack (show (methodElapsedtime mn)) + ] + maintt = methodLoc mn + + +data Status = Proved | Tested | Assumed + +statusColor :: Status -> GV.Color +statusColor Proved = GV.X11Color GV.Green +statusColor Tested = GV.X11Color GV.Yellow +statusColor Assumed = GV.X11Color GV.Red + +instance Semigroup Status where + Assumed <> _ = Assumed + _ <> Assumed = Assumed + Tested <> Proved = Tested + Proved <> Tested = Tested + Tested <> Tested = Tested + Proved <> Proved = Proved + +thmToStatus :: TheoremNode -> Status +thmToStatus thm = case thmStatus thm of + TheoremVerified{} -> Proved + TheoremTested{} -> Tested + TheoremAdmitted{} -> Assumed + +methodToStatus :: MethodNode -> Status +methodToStatus mn = case methodStatus mn of + MethodAssumed -> Assumed + MethodVerified -> Proved + +thmColor :: TheoremNode -> GV.Color +thmColor = statusColor . thmToStatus + +thmStatusText :: TheoremNode -> Text +thmStatusText thm = T.intercalate "\n" $ + case thmStatus thm of + TheoremVerified sls -> [T.unwords ("verified:" : sls)] + TheoremTested nm -> [T.unwords ["tested:", T.pack (show nm)]] + TheoremAdmitted msg -> ["Admitted!", msg] + + +thmTooltip :: TheoremNode -> Text +thmTooltip thm = T.intercalate "\n" $ + ([ thmReason thm + , thmLoc thm + ] ++ + case thmPLoc thm of + Nothing -> [] + Just (fn,l) -> [ fn <> " " <> l ]) + + +parseNodes :: Value -> Parser [SummaryNode] +parseNodes = withArray "summary nodes" (mapM parseNode . toList) + +parseNode :: Value -> Parser SummaryNode +parseNode = withObject "summary node" $ \o -> + do i <- o .: "id" + tp <- o .: "type" + case tp :: Text of + "method" -> MethodSummary i <$> parseMethodNode o + "property" -> TheoremSummary i <$> parseTheoremNode o + _ -> fail ("unexpected 'type' value " ++ show tp) + +parseMethodNode :: Object -> Parser MethodNode +parseMethodNode o = + MethodNode <$> + o .: "method" <*> + o .: "loc" <*> + parseMethodStatus o <*> + parseDeps o <*> + o .: "elapsedtime" + +parseMethodStatus :: Object -> Parser MethodStatus +parseMethodStatus o = + do st <- o .: "status" + case st :: Text of + "assumed" -> pure MethodAssumed + "verified" -> pure MethodVerified + _ -> fail ("Unexpected moethod status " ++ show st) + +parseDeps :: Object -> Parser [Integer] +parseDeps o = (o .: "dependencies") >>= parseJSONList + +parseTheoremNode :: Object -> Parser TheoremNode +parseTheoremNode o = + TheoremNode <$> + o .: "loc" <*> + o .: "reason" <*> + o .: "elapsedtime" <*> + parseTheoremStatus o <*> + (o .:? "ploc" >>= traverse parsePLoc) <*> + parseDeps o + +parsePLoc :: Value -> Parser (Text, Text) +parsePLoc = withObject "ploc" $ \o -> + do fn <- o .: "function" + l <- o .: "loc" + pure (fn,l) + +parseTheoremStatus :: Object -> Parser TheoremStatus +parseTheoremStatus o = + do st <- o .: "status" + case st :: Text of + "verified" -> TheoremVerified <$> (o .: "provers" >>= parseJSONList) + "tested" -> TheoremTested <$> (o .: "numtests") + "assumed" -> TheoremAdmitted <$> (o .: "admitmsg") + _ -> fail ("Unexpected theorem status " ++ show st) + +data SummaryNode + = TheoremSummary Integer TheoremNode + | MethodSummary Integer MethodNode + deriving (Show) + +summaryNodeId :: SummaryNode -> Integer +summaryNodeId (TheoremSummary i _) = i +summaryNodeId (MethodSummary i _) = i + +summaryNodeDeps :: SummaryNode -> [Integer] +summaryNodeDeps (TheoremSummary _ s) = thmDeps s +summaryNodeDeps (MethodSummary _ s) = methodDeps s + + +data TheoremNode = + TheoremNode + { thmLoc :: Text + , thmReason :: Text + , thmElapsedTime :: NominalDiffTime + , thmStatus :: TheoremStatus + , thmPLoc :: Maybe (Text, Text) + , thmDeps :: [Integer] + } + deriving (Show) + +data TheoremStatus + = TheoremVerified [Text] + | TheoremTested Integer + | TheoremAdmitted Text + deriving (Show) + +data MethodNode = + MethodNode + { methodName :: Text + , methodLoc :: Text + , methodStatus :: MethodStatus + , methodDeps :: [Integer] + , methodElapsedtime :: NominalDiffTime + } + deriving (Show) + +data MethodStatus + = MethodAssumed + | MethodVerified + deriving (Show) diff --git a/verif-viewer/verif-viewer.cabal b/verif-viewer/verif-viewer.cabal new file mode 100644 index 0000000000..bf050dd626 --- /dev/null +++ b/verif-viewer/verif-viewer.cabal @@ -0,0 +1,54 @@ +Name: verif-viewer +Version: 0.1 +License: BSD3 +License-file: LICENSE +Author: Galois, Inc. +Maintainer: rdockins@galois.com +Copyright: (c) 2021 Galois Inc. +Category: Formal Methods +Build-type: Simple +cabal-version: >= 1.8 +Synopsis: Verification Summary Viewer +Description: + Translate JSON verification summaries into GraphViz format + to produce a graph-based view of a verification effort. + +library + build-tools: + alex >= 3.1.3, + happy >= 1.9.6 + + build-depends: + base == 4.*, + aeson, + attoparsec, + fgl, + graphviz, + text + hs-source-dirs: src + exposed-modules: + + + GHC-options: -Wall -Werror -Wcompat + if impl(ghc == 8.0.1) + ghc-options: -Wno-redundant-constraints + GHC-prof-options: -fprof-auto -fprof-cafs + extensions: + DeriveFunctor + GeneralizedNewtypeDeriving + ImplicitParams + ViewPatterns + +executable verif-viewer + main-is: VerifViewer.hs + hs-source-dirs: tools + build-depends: + base >= 4 + , aeson + , attoparsec + , containers + , text + , verif-viewer + , bytestring + , time + , graphviz \ No newline at end of file