From e598a7440d0eb8eb8028790ff6a2edbac2d18289 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 9 Dec 2020 18:53:52 -0800 Subject: [PATCH] Rearrange the method whereby we `:check` or `:prove`, etc all the loaded properties. Instead of listing all the loaded properties and then parsing their names, we instead directly use the internal names retrieved from the module. This avoids problems arising from the names of the properties not being in scope. Separately, we should add settings for controlling exactly which properties should be considered; right now it is always all loaded properties. Fixes #639 --- src/Cryptol/REPL/Command.hs | 175 ++++++++++++++++++++++------------ src/Cryptol/REPL/Monad.hs | 6 +- src/Cryptol/Testing/Random.hs | 8 -- 3 files changed, 115 insertions(+), 74 deletions(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index eca8893d3..e0020cec5 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -339,22 +339,20 @@ evalCmd str lineNum mbBatch = do -- comment or empty input does nothing pure () -printCounterexample :: CounterExampleType -> P.Expr P.PName -> [Concrete.Value] -> REPL () -printCounterexample cexTy pexpr vs = +printCounterexample :: CounterExampleType -> Doc -> [Concrete.Value] -> REPL () +printCounterexample cexTy exprDoc vs = do ppOpts <- getPPValOpts docs <- mapM (rEval . E.ppValue Concrete ppOpts) vs - let doc = ppPrec 3 pexpr -- function application has precedence 3 - rPrint $ hang doc 2 (sep docs) <+> + rPrint $ hang exprDoc 2 (sep docs) <+> case cexTy of SafetyViolation -> text "~> ERROR" PredicateFalsified -> text "= False" -printSatisfyingModel :: P.Expr P.PName -> [Concrete.Value] -> REPL () -printSatisfyingModel pexpr vs = +printSatisfyingModel :: Doc -> [Concrete.Value] -> REPL () +printSatisfyingModel exprDoc vs = do ppOpts <- getPPValOpts docs <- mapM (rEval . E.ppValue Concrete ppOpts) vs - let doc = ppPrec 3 pexpr -- function application has precedence 3 - rPrint $ hang doc 2 (sep docs) <+> text ("= True") + rPrint $ hang exprDoc 2 (sep docs) <+> text ("= True") dumpTestsCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL () @@ -385,25 +383,48 @@ dumpTestsCmd outFile str pos fnm = data QCMode = QCRandom | QCExhaust deriving (Eq, Show) + -- | Randomly test a property, or exhaustively check it if the number -- of values in the type under test is smaller than the @tests@ -- environment variable, or we specify exhaustive testing. qcCmd :: QCMode -> String -> (Int,Int) -> Maybe FilePath -> REPL () -qcCmd qcMode "" pos fnm = +qcCmd qcMode "" _pos _fnm = do (xs,disp) <- getPropertyNames let nameStr x = show (fixNameDisp disp (pp x)) if null xs then rPutStrLn "There are no properties in scope." - else forM_ xs $ \x -> - -- TOOD, this is pretty bogus. Should find a way to do - -- this directly from the 'Name' instead of parsing it again. + else forM_ xs $ \(x,d) -> do let str = nameStr x rPutStr $ "property " ++ str ++ " " - qcCmd qcMode str pos fnm + let texpr = T.EVar x + let schema = M.ifDeclSig d + nd <- M.mctxNameDisp <$> getFocusedEnv + let doc = fixNameDisp nd (pp texpr) + void (qcExpr qcMode doc texpr schema) qcCmd qcMode str pos fnm = do expr <- replParseExpr str pos fnm - (val,ty) <- replEvalExpr expr + (_,texpr,schema) <- replCheckExpr expr + nd <- M.mctxNameDisp <$> getFocusedEnv + let doc = fixNameDisp nd (ppPrec 3 expr) -- function application has precedence 3 + void (qcExpr qcMode doc texpr schema) + + +data TestReport = TestReport + { _reportExpr :: Doc + , _reportResult :: TestResult + , _reportTestsRun :: Integer + , _reportTestsPossible :: Maybe Integer + } + +qcExpr :: + QCMode -> + Doc -> + T.Expr -> + T.Schema -> + REPL TestReport +qcExpr qcMode exprDoc texpr schema = + do (val,ty) <- replEvalCheckedExpr texpr schema testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests" tenv <- E.envTypes . M.deEnv <$> getDynEnv let tyv = E.evalValType tenv ty @@ -418,15 +439,15 @@ qcCmd qcMode str pos fnm = val vss) (\ex -> do rPutStrLn "\nTest interrupted..." num <- io $ readIORef testsRef - let report = TestReport Pass str num (Just sz) - ppReport (map E.tValTy tys) expr False report + let report = TestReport exprDoc Pass num (Just sz) + ppReport (map E.tValTy tys) False report rPutStrLn $ interruptedExhaust num sz Ex.throwM (ex :: Ex.SomeException)) - let report = TestReport res str num (Just sz) + let report = TestReport exprDoc res num (Just sz) delProgress delTesting - ppReport (map E.tValTy tys) expr True report - --return [report] + ppReport (map E.tValTy tys) True report + return report Just (sz,tys,_,gens) | qcMode == QCRandom -> do rPutStrLn "Using random testing." @@ -437,20 +458,20 @@ qcCmd qcMode str pos fnm = testNum val gens g) (\ex -> do rPutStrLn "\nTest interrupted..." num <- io $ readIORef testsRef - let report = TestReport Pass str num sz - ppReport (map E.tValTy tys) expr False report + let report = TestReport exprDoc Pass num sz + ppReport (map E.tValTy tys) False report case sz of Just n -> rPutStrLn $ coverageString num n _ -> return () Ex.throwM (ex :: Ex.SomeException)) - let report = TestReport res str num sz + let report = TestReport exprDoc res num sz delProgress delTesting - ppReport (map E.tValTy tys) expr False report + ppReport (map E.tValTy tys) False report case sz of Just n | isPass res -> rPutStrLn $ coverageString testNum n _ -> return () - --return [report] + return report _ -> raise (TypeNotTestable ty) where @@ -480,7 +501,6 @@ qcCmd qcMode str pos fnm = ++ showValNum ++ " values)" - totProgressWidth = 4 -- 100% lg2 :: Integer -> Integer @@ -490,7 +510,6 @@ qcCmd qcMode str pos fnm = in round $ logBase 2 valNumD :: Integer prt msg = rPutStr msg >> io (hFlush stdout) - prtLn msg = rPutStrLn msg >> io (hFlush stdout) ppProgress percentRef testsRef this tot = do io $ writeIORef testsRef this @@ -514,17 +533,20 @@ qcCmd qcMode str pos fnm = delTesting = del (length testingMsg) delProgress = del totProgressWidth - ppReport _tys _expr isExhaustive (TestReport Pass _str testNum _testPossible) = - do prtLn $ "Passed " ++ show testNum ++ " tests." + +ppReport :: [T.Type] -> Bool -> TestReport -> REPL () +ppReport _tys isExhaustive (TestReport _exprDoc Pass testNum _testPossible) = + do rPutStrLn ("Passed " ++ show testNum ++ " tests.") when isExhaustive (rPutStrLn "Q.E.D.") - ppReport tys expr _ (TestReport failure _str _testNum _testPossible) = - ppFailure tys expr failure +ppReport tys _ (TestReport exprDoc failure _testNum _testPossible) = + ppFailure tys exprDoc failure - ppFailure tys pexpr failure = do +ppFailure :: [T.Type] -> Doc -> TestResult -> REPL () +ppFailure tys exprDoc failure = do opts <- getPPValOpts case failure of FailFalse vs -> do - printCounterexample PredicateFalsified pexpr vs + printCounterexample PredicateFalsified exprDoc vs case (tys,vs) of ([t],[v]) -> bindItVariableVal t v _ -> let fs = [ M.packIdent ("arg" ++ show (i::Int)) | i <- [ 1 .. ] ] @@ -533,10 +555,10 @@ qcCmd qcMode str pos fnm = in bindItVariableVal t v FailError err [] -> do - prtLn "ERROR" + rPutStrLn "ERROR" rPrint (pp err) FailError err vs -> do - prtLn "ERROR for the following inputs:" + rPutStrLn "ERROR for the following inputs:" mapM_ (\v -> rPrint =<< (rEval $ E.ppValue Concrete opts v)) vs rPrint (pp err) Pass -> panic "Cryptol.REPL.Command" ["unexpected Test.Pass"] @@ -612,12 +634,16 @@ safeCmd str pos fnm = do fileName <- getKnownUser "smtfile" let mfile = if fileName == "-" then Nothing else Just fileName pexpr <- replParseExpr str pos fnm + nd <- M.mctxNameDisp <$> getFocusedEnv + let exprDoc = fixNameDisp nd (ppPrec 3 pexpr) -- function application has precedence 3 + let rng = fromMaybe (mkInteractiveRange pos fnm) (getLoc pexpr) + (_,texpr,schema) <- replCheckExpr pexpr if proverName `elem` ["offline","sbv-offline","w4-offline"] then - offlineProveSat proverName SafetyQuery pexpr mfile + offlineProveSat proverName SafetyQuery texpr schema mfile else - do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName SafetyQuery pexpr mfile) + do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName SafetyQuery texpr schema mfile) case result of EmptyResult -> panic "REPL.Command" [ "got EmptyResult for online prover query" ] @@ -634,8 +660,8 @@ safeCmd str pos fnm = do (t,e) <- mkSolverResult "counterexample" rng False (Right tes) ~(EnvBool yes) <- getUser "show-examples" - when yes $ printCounterexample cexType pexpr vs - when yes $ printSafetyViolation pexpr vs + when yes $ printCounterexample cexType exprDoc vs + when yes $ printSafetyViolation texpr schema vs void $ bindItVariable t e @@ -651,31 +677,49 @@ safeCmd str pos fnm = do -- on the expression given. See ticket #66 for a discussion of this -- design. cmdProveSat :: Bool -> String -> (Int,Int) -> Maybe FilePath -> REPL () -cmdProveSat isSat "" pos fnm = +cmdProveSat isSat "" _pos _fnm = do (xs,disp) <- getPropertyNames let nameStr x = show (fixNameDisp disp (pp x)) if null xs then rPutStrLn "There are no properties in scope." - else forM_ xs $ \x -> + else forM_ xs $ \(x,d) -> do let str = nameStr x if isSat then rPutStr $ ":sat " ++ str ++ "\n\t" else rPutStr $ ":prove " ++ str ++ "\n\t" - cmdProveSat isSat str pos fnm + let texpr = T.EVar x + let schema = M.ifDeclSig d + nd <- M.mctxNameDisp <$> getFocusedEnv + let doc = fixNameDisp nd (pp texpr) + proveSatExpr isSat (M.nameLoc x) doc texpr schema + cmdProveSat isSat str pos fnm = do + pexpr <- replParseExpr str pos fnm + nd <- M.mctxNameDisp <$> getFocusedEnv + let doc = fixNameDisp nd (ppPrec 3 pexpr) -- function application has precedence 3 + (_,texpr,schema) <- replCheckExpr pexpr + let rng = fromMaybe (mkInteractiveRange pos fnm) (getLoc pexpr) + proveSatExpr isSat rng doc texpr schema + +proveSatExpr :: + Bool -> + Range -> + Doc -> + T.Expr -> + T.Schema -> + REPL () +proveSatExpr isSat rng exprDoc texpr schema = do let cexStr | isSat = "satisfying assignment" | otherwise = "counterexample" qtype <- if isSat then SatQuery <$> getUserSatNum else pure ProveQuery proverName <- getKnownUser "prover" fileName <- getKnownUser "smtfile" let mfile = if fileName == "-" then Nothing else Just fileName - pexpr <- replParseExpr str pos fnm - let rng = fromMaybe (mkInteractiveRange pos fnm) (getLoc pexpr) if proverName `elem` ["offline","sbv-offline","w4-offline"] then - offlineProveSat proverName qtype pexpr mfile + offlineProveSat proverName qtype texpr schema mfile else - do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName qtype pexpr mfile) + do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName qtype texpr schema mfile) case result of EmptyResult -> panic "REPL.Command" [ "got EmptyResult for online prover query" ] @@ -695,12 +739,12 @@ cmdProveSat isSat str pos fnm = do (t,e) <- mkSolverResult cexStr rng isSat (Right tes) ~(EnvBool yes) <- getUser "show-examples" - when yes $ printCounterexample cexType pexpr vs + when yes $ printCounterexample cexType exprDoc vs -- if there's a safety violation, evalute the counterexample to -- find and print the actual concrete error case cexType of - SafetyViolation -> when yes $ printSafetyViolation pexpr vs + SafetyViolation -> when yes $ printSafetyViolation texpr schema vs _ -> return () void $ bindItVariable t e @@ -725,7 +769,7 @@ cmdProveSat isSat str pos fnm = do _ -> collectTes resultRecs ~(EnvBool yes) <- getUser "show-examples" - when yes $ forM_ vss (printSatisfyingModel pexpr) + when yes $ forM_ vss (printSatisfyingModel exprDoc) case (ty, exprs) of (t, [e]) -> void $ bindItVariable t e @@ -734,25 +778,26 @@ cmdProveSat isSat str pos fnm = do seeStats <- getUserShowProverStats when seeStats (showProverStats firstProver stats) -printSafetyViolation :: P.Expr P.PName -> [E.GenValue Concrete] -> REPL () -printSafetyViolation pexpr vs = + +printSafetyViolation :: T.Expr -> T.Schema -> [E.GenValue Concrete] -> REPL () +printSafetyViolation texpr schema vs = catch - (do (fn,_) <- replEvalExpr pexpr + (do (fn,_) <- replEvalCheckedExpr texpr schema rEval (E.forceValue =<< foldM (\f v -> E.fromVFun Concrete f (pure v)) fn vs)) (\case EvalError eex -> rPutStrLn (show (pp eex)) ex -> raise ex) - -onlineProveSat :: String - -> QueryType - -> P.Expr P.PName - -> Maybe FilePath - -> REPL (Maybe String,ProverResult,ProverStats) -onlineProveSat proverName qtype parseExpr mfile = do +onlineProveSat :: + String -> + QueryType -> + T.Expr -> + T.Schema -> + Maybe FilePath -> + REPL (Maybe String,ProverResult,ProverStats) +onlineProveSat proverName qtype expr schema mfile = do verbose <- getKnownUser "debug" modelValidate <- getUserProverValidate - (_, expr, schema) <- replCheckExpr parseExpr validEvalContext expr validEvalContext schema decls <- fmap M.deDecls getDynEnv @@ -780,11 +825,11 @@ onlineProveSat proverName qtype parseExpr mfile = do stas <- io (readIORef timing) return (firstProver,res,stas) -offlineProveSat :: String -> QueryType -> P.Expr P.PName -> Maybe FilePath -> REPL () -offlineProveSat proverName qtype parseExpr mfile = do +offlineProveSat :: String -> QueryType -> T.Expr -> T.Schema -> Maybe FilePath -> REPL () +offlineProveSat proverName qtype expr schema mfile = do verbose <- getKnownUser "debug" modelValidate <- getUserProverValidate - (_, expr, schema) <- replCheckExpr parseExpr + decls <- fmap M.deDecls getDynEnv timing <- io (newIORef 0) ~(EnvBool ignoreSafety) <- getUser "ignore-safety" @@ -1670,7 +1715,11 @@ replSpecExpr e = liftModuleCmd $ S.specialize e replEvalExpr :: P.Expr P.PName -> REPL (Concrete.Value, T.Type) replEvalExpr expr = do (_,def,sig) <- replCheckExpr expr - validEvalContext def + replEvalCheckedExpr def sig + +replEvalCheckedExpr :: T.Expr -> T.Schema -> REPL (Concrete.Value, T.Type) +replEvalCheckedExpr def sig = + do validEvalContext def validEvalContext sig me <- getModuleEnv diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 13ec9b1f4..65c200eb6 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -556,12 +556,12 @@ getTypeNames = return (map (show . pp) (Map.keys (M.neTypes fNames))) -- | Return a list of property names, sorted by position in the file. -getPropertyNames :: REPL ([M.Name],NameDisp) +getPropertyNames :: REPL ([(M.Name,M.IfaceDecl)],NameDisp) getPropertyNames = do fe <- getFocusedEnv let xs = M.ifDecls (M.mctxDecls fe) - ps = sortBy (comparing (from . M.nameLoc)) - [ x | (x,d) <- Map.toList xs, + ps = sortBy (comparing (from . M.nameLoc . fst)) + [ (x,d) | (x,d) <- Map.toList xs, T.PragmaProperty `elem` M.ifDeclPragmas d ] return (ps, M.mctxNameDisp fe) diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs index 9b5a2926e..3bdf97d58 100644 --- a/src/Cryptol/Testing/Random.hs +++ b/src/Cryptol/Testing/Random.hs @@ -19,7 +19,6 @@ module Cryptol.Testing.Random , randomValue , dumpableType , testableType -, TestReport(..) , TestResult(..) , isPass , returnTests @@ -395,13 +394,6 @@ typeValues ty = -------------------------------------------------------------------------------- -- Driver function -data TestReport = TestReport { - reportResult :: TestResult - , reportProp :: String -- ^ The property as entered by the user - , reportTestsRun :: Integer - , reportTestsPossible :: Maybe Integer - } - exhaustiveTests :: MonadIO m => (Integer -> m ()) {- ^ progress callback -} -> Value {- ^ function under test -} ->