From 06920e6453ef7a0f4e5e372ca1bbfa012fa258f7 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 4 Jun 2021 15:48:05 -0700 Subject: [PATCH 01/18] Use Lumberjack for crux output of messages, exceptions, CruxSimulationResult, and ProvedGoals. --- .../examples/cbl/branch.out.good | 6 +- .../examples/cbl/infeasible.out.good | 6 +- .../examples/cbl/small_threads.out.good | 6 +- .../examples/cbl/threads.out.good | 6 +- .../examples/cbl/threads_ids.out.good | 6 +- crucible-concurrency/src/Cruces/CrucesMain.hs | 14 +- .../src/Cruces/ExploreCrux.hs | 2 +- .../pthread-divine/one_time_barrier.out.good | 11 +- .../c/pthread-divine/ring_1w1r-1.out.good | 11 +- .../c/pthread-lit/fkp2013-1.out.good | 6 +- .../c/pthread-lit/qw2004-2.out.good | 6 +- .../c/pthread/bigshot_p.out.good | 6 +- .../c/pthread/fib_bench-2.out.good | 6 +- .../c/pthread/fib_bench_longer-2.out.good | 6 +- .../sv-benchmarks/c/pthread/queue.out.good | 6 +- .../c/pthread/reorder_2.out.good | 6 +- .../c/pthread/singleton_b.out.good | 6 +- .../sv-benchmarks/c/pthread/stack-2.out.good | 6 +- .../c/pthread/stateful01-1.out.good | 6 +- .../c/pthread/twostage_3.out.good | 6 +- crucible-concurrency/test/Main.hs | 2 +- crux-llvm/crux-llvm.cabal | 9 + crux-llvm/src/Crux/LLVM/Compile.hs | 18 +- crux-llvm/src/Crux/LLVM/Simulate.hs | 9 +- crux-llvm/src/CruxLLVMMain.hs | 37 ++- crux-llvm/svcomp/Main.hs | 79 ++--- .../golden-loop-merging/issue_478_unsafe.good | 7 +- .../golden-loop-merging/loop_exit_unsafe.good | 7 +- .../loop_sequence_unsafe.good | 31 +- .../golden-loop-merging/nested_unsafe.good | 39 +-- .../test-data/golden/golden/double_free.good | 22 +- crux-llvm/test/Test.hs | 7 +- crux-mir/crux-mir.cabal | 2 + crux-mir/src/Mir/Language.hs | 23 +- crux-mir/test/Test.hs | 2 +- crux/crux.cabal | 3 + crux/src/Crux.hs | 277 +++++++++--------- crux/src/Crux/Config/Common.hs | 4 +- crux/src/Crux/FormatOut.hs | 90 ++++++ crux/src/Crux/Goal.hs | 11 +- crux/src/Crux/Log.hs | 203 +++++++++---- crux/src/Crux/Types.hs | 35 ++- uc-crux-llvm/src/UCCrux/LLVM/Main.hs | 19 +- uc-crux-llvm/test/Test.hs | 41 ++- uc-crux-llvm/uc-crux-llvm.cabal | 3 +- 45 files changed, 666 insertions(+), 448 deletions(-) create mode 100644 crux/src/Crux/FormatOut.hs diff --git a/crucible-concurrency/examples/cbl/branch.out.good b/crucible-concurrency/examples/cbl/branch.out.good index 917d787a3..0d2842a15 100644 --- a/crucible-concurrency/examples/cbl/branch.out.good +++ b/crucible-concurrency/examples/cbl/branch.out.good @@ -1,2 +1,4 @@ -Failure for examples/cbl/branch.cbl:33:5: error: in t1 -Bad assertion, admittedly +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] examples/cbl/branch.cbl:33:5: error: in t1 +[Crux] Bad assertion, admittedly diff --git a/crucible-concurrency/examples/cbl/infeasible.out.good b/crucible-concurrency/examples/cbl/infeasible.out.good index 587578020..6544e0b30 100644 --- a/crucible-concurrency/examples/cbl/infeasible.out.good +++ b/crucible-concurrency/examples/cbl/infeasible.out.good @@ -1,2 +1,4 @@ -Failure for examples/cbl/infeasible.cbl:39:5: error: in main -ASDF +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] examples/cbl/infeasible.cbl:39:5: error: in main +[Crux] ASDF diff --git a/crucible-concurrency/examples/cbl/small_threads.out.good b/crucible-concurrency/examples/cbl/small_threads.out.good index e38e12385..008d59a96 100644 --- a/crucible-concurrency/examples/cbl/small_threads.out.good +++ b/crucible-concurrency/examples/cbl/small_threads.out.good @@ -1,2 +1,4 @@ -Failure for examples/cbl/small_threads.cbl:14:5: error: in main -Positive counter +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] examples/cbl/small_threads.cbl:14:5: error: in main +[Crux] Positive counter diff --git a/crucible-concurrency/examples/cbl/threads.out.good b/crucible-concurrency/examples/cbl/threads.out.good index 2165e3412..49ac7fc46 100644 --- a/crucible-concurrency/examples/cbl/threads.out.good +++ b/crucible-concurrency/examples/cbl/threads.out.good @@ -1,2 +1,4 @@ -Failure for examples/cbl/threads.cbl:11:5: error: in main -Positive counter +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] examples/cbl/threads.cbl:11:5: error: in main +[Crux] Positive counter diff --git a/crucible-concurrency/examples/cbl/threads_ids.out.good b/crucible-concurrency/examples/cbl/threads_ids.out.good index e107165e2..dfa00d760 100644 --- a/crucible-concurrency/examples/cbl/threads_ids.out.good +++ b/crucible-concurrency/examples/cbl/threads_ids.out.good @@ -1,2 +1,4 @@ -Failure for examples/cbl/threads_ids.cbl:14:5: error: in main -Positive counter +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] examples/cbl/threads_ids.cbl:14:5: error: in main +[Crux] Positive counter diff --git a/crucible-concurrency/src/Cruces/CrucesMain.hs b/crucible-concurrency/src/Cruces/CrucesMain.hs index fdef3d40d..8cd80cf2f 100644 --- a/crucible-concurrency/src/Cruces/CrucesMain.hs +++ b/crucible-concurrency/src/Cruces/CrucesMain.hs @@ -153,13 +153,7 @@ run (cruxOpts, opts) = return () -printCounterexamples :: (?outputConfig::Crux.OutputConfig) => ProvedGoals a -> IO () -printCounterexamples gs = case gs of - AtLoc _ _ gs1 -> printCounterexamples gs1 - Branch g1 g2 -> printCounterexamples g1 >> printCounterexamples g2 - Goal _ (c, _) _ res -> - let msg = show c - in case res of - NotProved _ (Just _) -> do - Crux.outputLn ("Failure for " ++ msg) - _ -> return () +printCounterexamples :: Crux.Logs + => ProvedGoals (Either AssumptionReason SimError) + -> IO () +printCounterexamples = Crux.logGoal diff --git a/crucible-concurrency/src/Cruces/ExploreCrux.hs b/crucible-concurrency/src/Cruces/ExploreCrux.hs index 2967e7fa9..4b7ccd72d 100644 --- a/crucible-concurrency/src/Cruces/ExploreCrux.hs +++ b/crucible-concurrency/src/Cruces/ExploreCrux.hs @@ -116,8 +116,8 @@ exploreOvr symOnline cruxOpts mainAct = do sym <- getSymInterface ctx <- use stateContext todo <- liftIO $ getProofObligations sym - let ?outputConfig = Crux.defaultOutputConfig { Crux._quiet = True } let cruxOpts' = cruxOpts { Crux.quietMode = True, Crux.simVerbose = 0 } + let ?outputConfig = Crux.defaultOutputConfig Nothing (processed, _) <- liftIO $ proveGoalsOnline sym cruxOpts' ctx (\_ _ -> return mempty) todo let provedAll = totalProcessedGoals processed == provedGoals processed when provedAll $ liftIO $ clearProofObligations sym diff --git a/crucible-concurrency/sv-benchmarks/c/pthread-divine/one_time_barrier.out.good b/crucible-concurrency/sv-benchmarks/c/pthread-divine/one_time_barrier.out.good index 5f27e0d04..9e925e20b 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread-divine/one_time_barrier.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread-divine/one_time_barrier.out.good @@ -1,4 +1,7 @@ -Failure for sv-benchmarks/c/pthread-divine/one_time_barrier.cbl:26:5: error: in barrier1_wait -Wait on used barrier! -Failure for sv-benchmarks/c/pthread-divine/one_time_barrier.cbl:26:5: error: in barrier1_wait -Wait on used barrier! +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread-divine/one_time_barrier.cbl:26:5: error: in barrier1_wait +[Crux] Wait on used barrier! +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread-divine/one_time_barrier.cbl:26:5: error: in barrier1_wait +[Crux] Wait on used barrier! diff --git a/crucible-concurrency/sv-benchmarks/c/pthread-divine/ring_1w1r-1.out.good b/crucible-concurrency/sv-benchmarks/c/pthread-divine/ring_1w1r-1.out.good index bcfac63b7..3a65dd916 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread-divine/ring_1w1r-1.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread-divine/ring_1w1r-1.out.good @@ -1,4 +1,7 @@ -Failure for sv-benchmarks/c/pthread-divine/ring_1w1r-1.cbl:137:5: error: in reader_maybe_buggy -Should fail -Failure for sv-benchmarks/c/pthread-divine/ring_1w1r-1.cbl:137:5: error: in reader_maybe_buggy -Should fail +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread-divine/ring_1w1r-1.cbl:137:5: error: in reader_maybe_buggy +[Crux] Should fail +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread-divine/ring_1w1r-1.cbl:137:5: error: in reader_maybe_buggy +[Crux] Should fail diff --git a/crucible-concurrency/sv-benchmarks/c/pthread-lit/fkp2013-1.out.good b/crucible-concurrency/sv-benchmarks/c/pthread-lit/fkp2013-1.out.good index 48c80a045..4b4d93359 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread-lit/fkp2013-1.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread-lit/fkp2013-1.out.good @@ -1,2 +1,4 @@ -Failure for sv-benchmarks/c/pthread-lit/fkp2013-1.cbl:7:5: error: in thr1 -max x +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread-lit/fkp2013-1.cbl:7:5: error: in thr1 +[Crux] max x diff --git a/crucible-concurrency/sv-benchmarks/c/pthread-lit/qw2004-2.out.good b/crucible-concurrency/sv-benchmarks/c/pthread-lit/qw2004-2.out.good index ba146cbc1..148cd4feb 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread-lit/qw2004-2.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread-lit/qw2004-2.out.good @@ -1,2 +1,4 @@ -Failure for sv-benchmarks/c/pthread-lit/qw2004-2.cbl:48:5: error: in BCSP_PnpAdd -Not Stopped +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread-lit/qw2004-2.cbl:48:5: error: in BCSP_PnpAdd +[Crux] Not Stopped diff --git a/crucible-concurrency/sv-benchmarks/c/pthread/bigshot_p.out.good b/crucible-concurrency/sv-benchmarks/c/pthread/bigshot_p.out.good index 405ec1c0b..8ae121802 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread/bigshot_p.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread/bigshot_p.out.good @@ -1,2 +1,4 @@ -Failure for sv-benchmarks/c/pthread/bigshot_p.cbl:61:5: error: in main -ASDF +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread/bigshot_p.cbl:61:5: error: in main +[Crux] ASDF diff --git a/crucible-concurrency/sv-benchmarks/c/pthread/fib_bench-2.out.good b/crucible-concurrency/sv-benchmarks/c/pthread/fib_bench-2.out.good index 036c4f558..a44942656 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread/fib_bench-2.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread/fib_bench-2.out.good @@ -1,2 +1,4 @@ -Failure for sv-benchmarks/c/pthread/fib_bench-2.cbl:75:5: error: in main -Not reachable? +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread/fib_bench-2.cbl:75:5: error: in main +[Crux] Not reachable? diff --git a/crucible-concurrency/sv-benchmarks/c/pthread/fib_bench_longer-2.out.good b/crucible-concurrency/sv-benchmarks/c/pthread/fib_bench_longer-2.out.good index 93427fefb..afd78a287 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread/fib_bench_longer-2.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread/fib_bench_longer-2.out.good @@ -1,2 +1,4 @@ -Failure for sv-benchmarks/c/pthread/fib_bench_longer-2.cbl:75:5: error: in main -Not reachable? +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread/fib_bench_longer-2.cbl:75:5: error: in main +[Crux] Not reachable? diff --git a/crucible-concurrency/sv-benchmarks/c/pthread/queue.out.good b/crucible-concurrency/sv-benchmarks/c/pthread/queue.out.good index 180ebde7b..c94166659 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread/queue.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread/queue.out.good @@ -1,2 +1,4 @@ -Failure for sv-benchmarks/c/pthread/queue.cbl:99:5: error: in t2 -I think this fails +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread/queue.cbl:99:5: error: in t2 +[Crux] I think this fails diff --git a/crucible-concurrency/sv-benchmarks/c/pthread/reorder_2.out.good b/crucible-concurrency/sv-benchmarks/c/pthread/reorder_2.out.good index 39125a509..532f56083 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread/reorder_2.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread/reorder_2.out.good @@ -1,2 +1,4 @@ -Failure for sv-benchmarks/c/pthread/reorder_2.cbl:20:5: error: in checkThread -Incorrect +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread/reorder_2.cbl:20:5: error: in checkThread +[Crux] Incorrect diff --git a/crucible-concurrency/sv-benchmarks/c/pthread/singleton_b.out.good b/crucible-concurrency/sv-benchmarks/c/pthread/singleton_b.out.good index b650412c2..51efdfeba 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread/singleton_b.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread/singleton_b.out.good @@ -1,2 +1,4 @@ -Failure for sv-benchmarks/c/pthread/singleton_b.cbl:43:5: error: in main -Buggy! +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread/singleton_b.cbl:43:5: error: in main +[Crux] Buggy! diff --git a/crucible-concurrency/sv-benchmarks/c/pthread/stack-2.out.good b/crucible-concurrency/sv-benchmarks/c/pthread/stack-2.out.good index e68f854da..b4038ffe7 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread/stack-2.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread/stack-2.out.good @@ -1,2 +1,4 @@ -Failure for sv-benchmarks/c/pthread/stack-2.cbl:33:5: error: in pop -Underflow! +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread/stack-2.cbl:33:5: error: in pop +[Crux] Underflow! diff --git a/crucible-concurrency/sv-benchmarks/c/pthread/stateful01-1.out.good b/crucible-concurrency/sv-benchmarks/c/pthread/stateful01-1.out.good index ea5d043d8..011c41408 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread/stateful01-1.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread/stateful01-1.out.good @@ -1,2 +1,4 @@ -Failure for sv-benchmarks/c/pthread/stateful01-1.cbl:36:5: error: in main -This fails +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread/stateful01-1.cbl:36:5: error: in main +[Crux] This fails diff --git a/crucible-concurrency/sv-benchmarks/c/pthread/twostage_3.out.good b/crucible-concurrency/sv-benchmarks/c/pthread/twostage_3.out.good index aa6f0fb27..21fa388d7 100644 --- a/crucible-concurrency/sv-benchmarks/c/pthread/twostage_3.out.good +++ b/crucible-concurrency/sv-benchmarks/c/pthread/twostage_3.out.good @@ -1,2 +1,4 @@ -Failure for sv-benchmarks/c/pthread/twostage_3.cbl:32:7: error: in funcB -Wrong? +[Crux] Attempting to prove verification conditions. +[Crux] Found counterexample for verification goal +[Crux] sv-benchmarks/c/pthread/twostage_3.cbl:32:7: error: in funcB +[Crux] Wrong? diff --git a/crucible-concurrency/test/Main.hs b/crucible-concurrency/test/Main.hs index 6ba90166c..86a5a62c9 100644 --- a/crucible-concurrency/test/Main.hs +++ b/crucible-concurrency/test/Main.hs @@ -66,5 +66,5 @@ testSimulator inFile outFile = Crux.checkPathSat = True }, defaultCrucesOptions) - let ?outputConfig = Crux.OutputConfig False outh outh True + let ?outputConfig = Crux.mkOutputConfig False outh outh $ Just (fst options) run options diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal index fb39a85c9..4932de3d7 100644 --- a/crux-llvm/crux-llvm.cabal +++ b/crux-llvm/crux-llvm.cabal @@ -91,6 +91,7 @@ library logict, llvm-pretty, llvm-pretty-bc-parser, + lumberjack >= 1.0 && < 1.1, mtl, parameterized-utils, prettyprinter >= 1.7.0, @@ -131,9 +132,16 @@ executable crux-llvm-svcomp async >= 2.2, ansi-terminal, crux-llvm, + lumberjack, time, unix + other-modules: + Paths_crux_llvm + + autogen-modules: + Paths_crux_llvm + test-suite crux-llvm-test import: bldflags, testdefs @@ -145,5 +153,6 @@ test-suite crux-llvm-test build-depends: crux-llvm, deepseq, + lumberjack, parsec, versions diff --git a/crux-llvm/src/Crux/LLVM/Compile.hs b/crux-llvm/src/Crux/LLVM/Compile.hs index be18c4043..cc7592222 100644 --- a/crux-llvm/src/Crux/LLVM/Compile.hs +++ b/crux-llvm/src/Crux/LLVM/Compile.hs @@ -9,7 +9,7 @@ module Crux.LLVM.Compile where import Control.Applicative -import Control.Exception ( SomeException(..), try, displayException ) +import Control.Exception ( SomeException(..), try ) import Control.Monad ( guard, unless, when, forM_ ) import Control.Monad.Logic ( observeAll ) import qualified Data.Foldable as Fold @@ -76,7 +76,7 @@ runClang :: Logs => CruxOptions -> LLVMOptions -> [String] -> IO () runClang cruxOpts llvmOpts params = do let clang = clangBin llvmOpts allParams = clangOpts llvmOpts ++ params - when (simVerbose cruxOpts > 1) $ say "CLANG" $ unwords (clang : map show allParams) + say Noisily "CLANG" $ T.unwords (T.pack <$> (clang : map show allParams)) (res,sout,serr) <- readProcessWithExitCode clang allParams "" case res of ExitSuccess -> return () @@ -234,20 +234,20 @@ makeCounterExamplesLLVM cruxOpts llvmOpts res let suff = case plSourceLoc (simErrorLoc c) of SourcePos _ l _ -> show l _ -> "unknown" - msg = show c skipGoal = case simErrorReason c of ResourceExhausted _ -> True _ -> False in case (r, skipGoal) of (NotProved _ (Just m), False) -> - do sayFail "Crux" ("Counter example for " ++ msg) - try (buildModelExes cruxOpts llvmOpts suff (ppModelC m)) >>= \case - Left (ex :: SomeException) -> - sayFail "Crux" (unlines ["Failed to build counterexample executable", displayException ex]) + do try (buildModelExes cruxOpts llvmOpts suff (ppModelC m)) >>= \case + Left (ex :: SomeException) -> do + logGoal gs + say Fail "Crux" "Failed to build counterexample executable" + logException ex Right (_prt,dbg) -> do - say "Crux" ("*** debug executable: " ++ dbg) - say "Crux" ("*** break on line: " ++ suff) + say Simply "Crux" ("*** debug executable: " <> T.pack dbg) + say Simply "Crux" ("*** break on line: " <> T.pack suff) _ -> return () buildModelExes :: Logs => CruxOptions -> LLVMOptions -> String -> String -> IO (FilePath,FilePath) diff --git a/crux-llvm/src/Crux/LLVM/Simulate.hs b/crux-llvm/src/Crux/LLVM/Simulate.hs index 6965466fa..76df1d618 100644 --- a/crux-llvm/src/Crux/LLVM/Simulate.hs +++ b/crux-llvm/src/Crux/LLVM/Simulate.hs @@ -16,6 +16,7 @@ import qualified Data.List as List import Control.Lens ((&), (%~), (^.), view) import Control.Monad.State(liftIO) import Data.Text (Text) +import qualified Data.Text as T import GHC.Exts ( proxy# ) import System.IO (stdout) @@ -192,8 +193,9 @@ prepLLVMModule llvmOpts halloc sym bcFile memVar = do let ?lc = llvmCtxt ^. llvmTypeCtx in llvmPtrWidth llvmCtxt $ \ptrW -> withPtrWidth ptrW $ do - liftIO $ say "Crux" $ unwords [ "Using pointer width:", show ptrW - , "for file", bcFile] + say Simply "Crux" $ T.unwords [ "Using pointer width:" + , T.pack $ show ptrW + , "for file", T.pack bcFile] populateAllGlobals sym (globalInitMap trans) =<< initializeAllMemory sym llvmCtxt llvmMod return $ PreppedLLVM llvmMod (Some trans) memVar mem @@ -207,7 +209,8 @@ checkFun nm mp = Just (_, AnyCFG anyCfg) -> case cfgArgTypes anyCfg of Empty -> - do liftIO $ say "Crux" ("Simulating function " ++ show nm) + do liftIO $ say Simply "Crux" ("Simulating function " + <> T.pack (show nm)) (callCFG anyCfg emptyRegMap) >> return () _ -> throwCError BadFun -- TODO(lb): Suggest uc-crux-llvm? Nothing -> throwCError (MissingFun nm) diff --git a/crux-llvm/src/CruxLLVMMain.hs b/crux-llvm/src/CruxLLVMMain.hs index a8a024371..eb297bf39 100644 --- a/crux-llvm/src/CruxLLVMMain.hs +++ b/crux-llvm/src/CruxLLVMMain.hs @@ -1,36 +1,35 @@ {-# Language OverloadedStrings #-} module CruxLLVMMain - ( mainWithOutputTo, mainWithOutputConfig, defaultOutputConfig, processLLVMOptions ) + ( mainWithOutputTo, mainWithOutputConfig + , Crux.defaultOutputConfig + , Crux.mkOutputConfig + , processLLVMOptions ) where -import System.Exit - ( ExitCode ) -import System.IO - ( Handle ) -import System.FilePath - ( dropExtension, takeFileName, () ) -import System.Directory - ( createDirectoryIfMissing ) +import System.Directory ( createDirectoryIfMissing ) +import System.Exit ( ExitCode ) +import System.FilePath ( dropExtension, takeFileName, () ) +import System.IO ( Handle ) -- crux import qualified Crux -import Crux.Log (OutputConfig(..), defaultOutputConfig) -import Crux.Config.Common(CruxOptions(..)) +import Crux.Log ( OutputConfig(..) ) +import Crux.Config.Common (CruxOptions(..)) -- local -import Crux.LLVM.Config -import Crux.LLVM.Compile -import Crux.LLVM.Simulate -import Paths_crux_llvm (version) +import Crux.LLVM.Config +import Crux.LLVM.Compile +import Crux.LLVM.Simulate +import Paths_crux_llvm (version) mainWithOutputTo :: Handle -> IO ExitCode -mainWithOutputTo h = mainWithOutputConfig (OutputConfig False h h False) +mainWithOutputTo h = mainWithOutputConfig $ Crux.mkOutputConfig True h h -mainWithOutputConfig :: OutputConfig -> IO ExitCode -mainWithOutputConfig outCfg = do +mainWithOutputConfig :: (Maybe CruxOptions -> OutputConfig) -> IO ExitCode +mainWithOutputConfig mkOutCfg = do cfg <- llvmCruxConfig - Crux.loadOptions outCfg "crux-llvm" version cfg $ \initOpts -> + Crux.loadOptions mkOutCfg "crux-llvm" version cfg $ \initOpts -> do (cruxOpts, llvmOpts) <- processLLVMOptions initOpts bcFile <- genBitCode cruxOpts llvmOpts res <- Crux.runSimulator cruxOpts (simulateLLVMFile bcFile llvmOpts) diff --git a/crux-llvm/svcomp/Main.hs b/crux-llvm/svcomp/Main.hs index 97a7ee6ec..a5dca1513 100644 --- a/crux-llvm/svcomp/Main.hs +++ b/crux-llvm/svcomp/Main.hs @@ -16,6 +16,7 @@ module Main (main) where import Control.Concurrent.Async( async, wait ) import Control.Exception (bracket, catch, throwIO, SomeException, fromException, AsyncException, displayException, try ) +import qualified Data.Text as T import Data.Aeson ( encode, ToJSON(..), FromJSON, ToJSONKey, eitherDecode', object ) import Data.Bits( bit ) @@ -50,9 +51,10 @@ import Crux.Types as Crux import Crux.LLVM.Config import Crux.LLVM.Compile import Crux.LLVM.Simulate -import CruxLLVMMain( processLLVMOptions ) +import CruxLLVMMain ( processLLVMOptions, defaultOutputConfig ) import Paths_crux_llvm (version) + main :: IO () main = do cfg <- llvmCruxConfig @@ -81,13 +83,13 @@ genSVCOMPBitCode cruxOpts llvmOpts svOpts tm = concat <$> mapM goTask (zip [0::I handler e | Just (_::AsyncException) <- fromException e = throwIO e | otherwise = - do sayFail "SVCOMP" $ unlines [ "Failed to compile task:" - , show (verificationSourceFile task) - , displayException e] - removeDirectoryRecursive outputPath `catch` \e' -> - sayFail "SVCOMP" $ unlines [ "Double fault! While trying to remove:" - , outputPath - , displayException (e'::SomeException)] + do say Fail "SVCOMP" ("Failed to compile task:" + <> (T.pack $ show $ verificationSourceFile task)) + logException e + removeDirectoryRecursive outputPath `catch` \e' -> do + say Fail "SVCOMP" ("Double fault! While trying to remove: " + <> T.pack outputPath) + logException (e'::SomeException) return [(n, task, Left e)] @@ -99,18 +101,18 @@ genSVCOMPBitCode cruxOpts llvmOpts svOpts tm = concat <$> mapM goTask (zip [0::I processVerificationTask _tgt _num task | or [ isSuffixOf bl (verificationSourceFile task) | bl <- svcompBlacklist svOpts ] - = do sayWarn "SVCOMP" $ unlines + = do say Warn "SVCOMP" $ T.unlines [ "Skipping:" - , " " ++ verificationSourceFile task ++ " due to blacklist" + , " " <> T.pack (verificationSourceFile task) <> " due to blacklist" ] return Nothing processVerificationTask tgt num task = let files = verificationInputFiles task in if null files - then do sayWarn "SVCOMP" $ unlines + then do say Warn "SVCOMP" $ T.unlines [ "Skipping:" - , " " ++ verificationSourceFile task ++ " because no input files are present" + , " " <> T.pack (verificationSourceFile task) <> " because no input files are present" ] return Nothing else @@ -205,10 +207,10 @@ evaluateBenchmarkLLVM cruxOpts llvmOpts svOpts ts = readHdl <- fdToHandle readFd jsonReadHdl <- fdToHandle jsonReadFd - sayOK "SVCOMP" $ concat - [ "Evaluating:\n" - , " " ++ taskRoot ++ "\n" - , " " ++ sourceFile + say OK "SVCOMP" $ T.unlines + [ "Evaluating:" + , " " <> T.pack taskRoot + , " " <> T.pack sourceFile ] startTime <- getCurrentTime @@ -236,19 +238,29 @@ evaluateBenchmarkLLVM cruxOpts llvmOpts svOpts ts = res <- wait ares let wallTime = diffUTCTime endTime startTime - sayOK "SVCOMP" $ unwords ["Elapsed wall-clock time:", show wallTime] + say OK "SVCOMP" $ T.unwords ["Elapsed wall-clock time:" + , T.pack $ show wallTime + ] case st of Just (Exited ExitSuccess) -> return () Just (Exited (ExitFailure x)) -> - sayFail "SVCOMP" $ unwords ["Evaluation process exited with failure code", show x] + say Fail "SVCOMP" + $ T.unwords ["Evaluation process exited with failure code" + , T.pack $ show x + ] Just (Terminated sig _) -> - sayWarn "SVCOMP" $ unwords ["Evaluation process terminated by signal", show sig] + say Warn "SVCOMP" + $ T.unwords ["Evaluation process terminated by signal" + , T.pack $ show sig + ] Just (Stopped sig) -> - sayWarn "SVCOMP" $ unwords ["Evaluation process stopped by signal", show sig] + say Warn "SVCOMP" $ T.unwords ["Evaluation process stopped by signal" + , T.pack $ show sig + ] Nothing -> - sayFail "SVCOMP" "Could not retrieve evauation process status" + say Fail "SVCOMP" "Could not retrieve evaluation process status" return EvaluationData { taskRoot = taskRoot @@ -309,7 +321,7 @@ evaluateSingleTask writeHdl jsonHdl cruxOpts llvmOpts bsRoot num task inpBCFile let inputs = map (srcRoot ) (verificationInputFiles task) let cruxOpts' = cruxOpts { outDir = taskRoot, inputFiles = inputs } - let ?outputConfig = OutputConfig False writeHdl writeHdl False + let ?outputConfig = Crux.mkOutputConfig True writeHdl writeHdl $ Just cruxOpts mres <- try $ do res <- Crux.runSimulator cruxOpts' (simulateLLVMFile inpBCFile llvmOpts) @@ -318,10 +330,8 @@ evaluateSingleTask writeHdl jsonHdl cruxOpts llvmOpts bsRoot num task inpBCFile case mres of Left e -> - do sayFail "SVCOMP" $ unlines - [ "Simulator threw exception:" - , displayException (e :: SomeException) - ] + do say Fail "SVCOMP" "Simulator threw exception:" + logException (e :: SomeException) hClose writeHdl hClose jsonHdl exitFailure @@ -352,22 +362,25 @@ evaluateSingleTask writeHdl jsonHdl cruxOpts llvmOpts bsRoot num task inpBCFile Unknown -> Nothing case expectedResult of - Nothing -> sayWarn "SVCOMP" $ unlines (["No verdict to evaluate!"] ++ map show (verificationProperties task)) + Nothing -> say Warn "SVCOMP" + $ T.unlines ("No verdict to evaluate!" + : (T.pack . show + <$> (verificationProperties task))) Just True -> case verdict of Verified -> - sayOK "SVCOMP" "CORRECT (Verified)" + say OK "SVCOMP" "CORRECT (Verified)" Falsified -> - sayFail "SVCOMP" $ unwords ["FAILED! benchmark should be verified"] - Unknown -> sayWarn "SVCOMP" "UNKNOWN (Should verify)" + say Fail "SVCOMP" $ "FAILED! benchmark should be verified" + Unknown -> say Warn "SVCOMP" "UNKNOWN (Should verify)" Just False -> case verdict of Verified -> - sayFail "SVCOMP" $ unwords ["FAILED! benchmark should contain an error!"] + say Fail "SVCOMP" $ "FAILED! benchmark should contain an error!" Falsified -> - sayOK "SVCOMP" "CORRECT (Falisifed)" + say OK "SVCOMP" "CORRECT (Falsifed)" Unknown -> - sayWarn "SVCOMP" "UNKNOWN (Should falsify)" + say Warn "SVCOMP" "UNKNOWN (Should be falsified)" LBS.hPut jsonHdl (encode EvaluationResult{ .. }) diff --git a/crux-llvm/test-data/golden/golden-loop-merging/issue_478_unsafe.good b/crux-llvm/test-data/golden/golden-loop-merging/issue_478_unsafe.good index 945c21f1c..cfb8f0baf 100644 --- a/crux-llvm/test-data/golden/golden-loop-merging/issue_478_unsafe.good +++ b/crux-llvm/test-data/golden/golden-loop-merging/issue_478_unsafe.good @@ -1,7 +1,4 @@ -[Crux] Counter example for test-data/golden/golden-loop-merging/issue_478_unsafe.c:35:0: error: in main -crucible_assert [Crux] Found counterexample for verification goal -test-data/golden/golden-loop-merging/issue_478_unsafe.c:35:0: error: in main -crucible_assert - +[Crux] test-data/golden/golden-loop-merging/issue_478_unsafe.c:35:0: error: in main +[Crux] crucible_assert [Crux] Overall status: Invalid. diff --git a/crux-llvm/test-data/golden/golden-loop-merging/loop_exit_unsafe.good b/crux-llvm/test-data/golden/golden-loop-merging/loop_exit_unsafe.good index d95b00e12..64df81716 100644 --- a/crux-llvm/test-data/golden/golden-loop-merging/loop_exit_unsafe.good +++ b/crux-llvm/test-data/golden/golden-loop-merging/loop_exit_unsafe.good @@ -1,7 +1,4 @@ -[Crux] Counter example for test-data/golden/golden-loop-merging/loop_exit_unsafe.c:18:0: error: in main -crucible_assert [Crux] Found counterexample for verification goal -test-data/golden/golden-loop-merging/loop_exit_unsafe.c:18:0: error: in main -crucible_assert - +[Crux] test-data/golden/golden-loop-merging/loop_exit_unsafe.c:18:0: error: in main +[Crux] crucible_assert [Crux] Overall status: Invalid. diff --git a/crux-llvm/test-data/golden/golden-loop-merging/loop_sequence_unsafe.good b/crux-llvm/test-data/golden/golden-loop-merging/loop_sequence_unsafe.good index 682390f04..e6263f3b3 100644 --- a/crux-llvm/test-data/golden/golden-loop-merging/loop_sequence_unsafe.good +++ b/crux-llvm/test-data/golden/golden-loop-merging/loop_sequence_unsafe.good @@ -1,25 +1,16 @@ -[Crux] Counter example for test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main -crucible_assert -[Crux] Counter example for test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main -crucible_assert -[Crux] Counter example for test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main -crucible_assert -[Crux] Counter example for test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main -crucible_assert [Crux] Found counterexample for verification goal -test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main -crucible_assert - +[Crux] test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main +[Crux] crucible_assert +[Crux] [Crux] Found counterexample for verification goal -test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main -crucible_assert - +[Crux] test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main +[Crux] crucible_assert +[Crux] [Crux] Found counterexample for verification goal -test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main -crucible_assert - +[Crux] test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main +[Crux] crucible_assert +[Crux] [Crux] Found counterexample for verification goal -test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main -crucible_assert - +[Crux] test-data/golden/golden-loop-merging/loop_sequence_unsafe.c:32:0: error: in main +[Crux] crucible_assert [Crux] Overall status: Invalid. diff --git a/crux-llvm/test-data/golden/golden-loop-merging/nested_unsafe.good b/crux-llvm/test-data/golden/golden-loop-merging/nested_unsafe.good index b5711d9e0..e8983a2a1 100644 --- a/crux-llvm/test-data/golden/golden-loop-merging/nested_unsafe.good +++ b/crux-llvm/test-data/golden/golden-loop-merging/nested_unsafe.good @@ -1,31 +1,20 @@ -[Crux] Counter example for test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main -crucible_assert -[Crux] Counter example for test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main -crucible_assert -[Crux] Counter example for test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main -crucible_assert -[Crux] Counter example for test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main -crucible_assert -[Crux] Counter example for test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main -crucible_assert [Crux] Found counterexample for verification goal -test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main -crucible_assert - +[Crux] test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main +[Crux] crucible_assert +[Crux] [Crux] Found counterexample for verification goal -test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main -crucible_assert - +[Crux] test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main +[Crux] crucible_assert +[Crux] [Crux] Found counterexample for verification goal -test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main -crucible_assert - +[Crux] test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main +[Crux] crucible_assert +[Crux] [Crux] Found counterexample for verification goal -test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main -crucible_assert - +[Crux] test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main +[Crux] crucible_assert +[Crux] [Crux] Found counterexample for verification goal -test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main -crucible_assert - +[Crux] test-data/golden/golden-loop-merging/nested_unsafe.c:19:0: error: in main +[Crux] crucible_assert [Crux] Overall status: Invalid. diff --git a/crux-llvm/test-data/golden/golden/double_free.good b/crux-llvm/test-data/golden/golden/double_free.good index 05fbcc438..3ff8e9fc8 100644 --- a/crux-llvm/test-data/golden/golden/double_free.good +++ b/crux-llvm/test-data/golden/golden/double_free.good @@ -1,16 +1,12 @@ ???? -[Crux] Counter example for test-data/golden/golden/double_free.c:16:3: error: in main -Undefined behavior encountered -Details: - `free` called on a pointer to already-freed memory [Crux] Found counterexample for verification goal -test-data/golden/golden/double_free.c:16:3: error: in main -Undefined behavior encountered -Details: - `free` called on a pointer to already-freed memory - Pointer: (10, 0x0:[64]) - Reference: - The C language standard, version C11 - §7.22.3.3 The free function, ¶2 - Document URL: http://www.iso-9899.info/n1570.html +[Crux] test-data/golden/golden/double_free.c:16:3: error: in main +[Crux] Undefined behavior encountered +[Crux] Details: +[Crux] `free` called on a pointer to already-freed memory +[Crux] Pointer: (10, 0x0:[64]) +[Crux] Reference: +[Crux] The C language standard, version C11 +[Crux] §7.22.3.3 The free function, ¶2 +[Crux] Document URL: http://www.iso-9899.info/n1570.html [Crux] Overall status: Invalid. diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs index 0dd61f633..57ee5711e 100644 --- a/crux-llvm/test/Test.hs +++ b/crux-llvm/test/Test.hs @@ -27,7 +27,6 @@ import qualified Test.Tasty as TT import Test.Tasty.HUnit ( testCase, assertFailure ) import qualified Test.Tasty.Sugar as TS -import qualified Crux.Log as C import qualified CruxLLVMMain as C @@ -249,6 +248,7 @@ mkTest clangVer sweet _ expct = [ ("--config=" <>) <$> lookup "config" (TS.associated expct) , Just $ "--solver=" <> solver + , Just "--quiet" ] failureMsg = let bss = BSIO.pack . fmap (toEnum . fromEnum) . show in \case Left e -> "***[test]*** Crux failed with exception: " <> bss (show (e :: SomeException)) <> "\n" @@ -257,9 +257,8 @@ mkTest clangVer sweet _ expct = r <- withFile outFile WriteMode $ \h -> (try $ withArgs (cfargs <> [TS.rootFile sweet]) $ - -- Quiet mode, don't print colors - let quietMode = True in - C.mainWithOutputConfig (C.OutputConfig False h h quietMode)) + let coloredOutput = False + in (C.mainWithOutputConfig $ C.mkOutputConfig coloredOutput h h)) BSIO.writeFile resFName $ failureMsg r checkResult = diff --git a/crux-mir/crux-mir.cabal b/crux-mir/crux-mir.cabal index b09485776..9d0875e72 100644 --- a/crux-mir/crux-mir.cabal +++ b/crux-mir/crux-mir.cabal @@ -33,6 +33,7 @@ library parameterized-utils >= 1.0.8, containers, lens, + lumberjack >= 1.0 && < 1.1, vector, mtl, regex-compat, @@ -129,6 +130,7 @@ test-suite test deepseq, directory, filepath, + lumberjack, parsec, process, crux-mir, diff --git a/crux-mir/src/Mir/Language.hs b/crux-mir/src/Mir/Language.hs index 3bff55583..74f63ab62 100644 --- a/crux-mir/src/Mir/Language.hs +++ b/crux-mir/src/Mir/Language.hs @@ -105,18 +105,20 @@ import Mir.Concurrency import Paths_crux_mir (version) main :: IO () -main = mainWithOutputConfig defaultOutputConfig noExtraOverrides >>= exitWith +main = mainWithOutputConfig Crux.defaultOutputConfig noExtraOverrides >>= exitWith mainWithExtraOverrides :: BindExtraOverridesFn -> IO () mainWithExtraOverrides bindExtra = - mainWithOutputConfig defaultOutputConfig bindExtra >>= exitWith + mainWithOutputConfig Crux.defaultOutputConfig bindExtra >>= exitWith mainWithOutputTo :: Handle -> BindExtraOverridesFn -> IO ExitCode -mainWithOutputTo h bindExtra = mainWithOutputConfig (OutputConfig False h h False) bindExtra +mainWithOutputTo h = mainWithOutputConfig $ Crux.mkOutputConfig False h h -mainWithOutputConfig :: OutputConfig -> BindExtraOverridesFn -> IO ExitCode -mainWithOutputConfig outCfg bindExtra = - Crux.loadOptions outCfg "crux-mir" version mirConfig $ runTestsWithExtraOverrides bindExtra +mainWithOutputConfig :: (Maybe Crux.CruxOptions -> OutputConfig) + -> BindExtraOverridesFn -> IO ExitCode +mainWithOutputConfig mkOutCfg bindExtra = + Crux.loadOptions mkOutCfg "crux-mir" version mirConfig + $ runTestsWithExtraOverrides bindExtra type BindExtraOverridesFn = forall sym p t st fs args ret blocks rtp a r. (C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) => @@ -266,7 +268,7 @@ runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do -- is enabled. when (not (concurrency mirOpts) && printResultOnly mirOpts) $ do str <- showRegEntry @sym col resTy res - liftIO $ outputLn str + liftIO $ say Simply "Crux-MIR" $ Text.pack str when (not (concurrency mirOpts) && not (printResultOnly mirOpts) && resTy /= TyTuple []) $ do str <- showRegEntry @sym col resTy res @@ -355,11 +357,10 @@ runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do let printCounterexamples gs = case gs of AtLoc _ _ gs1 -> printCounterexamples gs1 Branch g1 g2 -> printCounterexamples g1 >> printCounterexamples g2 - Goal _ (c, _) _ res -> - let msg = show c - in case res of + Goal _ (_, _) _ res -> + case res of NotProved _ (Just m) -> do - outputLn ("Failure for " ++ msg) + logGoal gs when (showModel mirOpts) $ do outputLn "Model:" mjs <- Crux.modelJS m diff --git a/crux-mir/test/Test.hs b/crux-mir/test/Test.hs index 6bacc1c35..e7a8ff81e 100644 --- a/crux-mir/test/Test.hs +++ b/crux-mir/test/Test.hs @@ -88,7 +88,7 @@ runCrux rustFile outHandle mode = do _ -> "", Crux.branchCoverage = (mode == RcmCoverage) } , Mir.defaultMirOptions { Mir.printResultOnly = (mode == RcmConcrete) }) - let ?outputConfig = Crux.OutputConfig False outHandle outHandle quiet + let ?outputConfig = Crux.mkOutputConfig False outHandle outHandle Nothing _exitCode <- Mir.runTests options return () diff --git a/crux/crux.cabal b/crux/crux.cabal index 570bb5412..f9dea80d2 100644 --- a/crux/crux.cabal +++ b/crux/crux.cabal @@ -27,12 +27,14 @@ library attoparsec, bv-sized >= 1.0.0, containers, + contravariant >= 1.5 && < 1.6, crucible, directory, filepath, haskeline >= 0.7, lens, libBF >= 0.6 && < 0.7, + lumberjack >= 1.0 && < 1.1, mtl >= 2.1, parameterized-utils >= 1.0 && < 2.2, prettyprinter >= 1.7.0, @@ -59,6 +61,7 @@ library exposed-modules: Crux, Crux.Types, + Crux.FormatOut, Crux.Goal, Crux.Log, Crux.ProgressBar, diff --git a/crux/src/Crux.hs b/crux/src/Crux.hs index a265d1f6e..3be6bccb2 100644 --- a/crux/src/Crux.hs +++ b/crux/src/Crux.hs @@ -1,17 +1,20 @@ -{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE NoMonoLocalBinds #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# Language RankNTypes, ImplicitParams, TypeApplications, MultiWayIf #-} {-# Language OverloadedStrings, FlexibleContexts, ScopedTypeVariables #-} {-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-} + module Crux ( runSimulator , postprocessSimResult , loadOptions - , withOutputConfig + , mkOutputConfig + , defaultOutputConfig , SimulatorCallback(..) , RunnableState(..) , pattern RunnableState @@ -24,67 +27,69 @@ module Crux ) where import qualified Control.Exception as Ex -import Control.Lens -import Control.Monad ( unless, void ) -import Data.Text (Text) -import qualified Data.Text as Text -import Data.Foldable -import Data.IORef -import Data.List ( intercalate ) -import Data.Maybe ( fromMaybe ) -import Data.Proxy ( Proxy(..) ) +import Control.Lens +import Control.Monad ( unless, void, when ) +import Data.Foldable +import Data.Functor.Contravariant ( (>$<) ) +import Data.Functor.Contravariant.Divisible ( divide ) +import Data.IORef +import Data.Maybe ( fromMaybe ) +import Data.Proxy ( Proxy(..) ) import qualified Data.Sequence as Seq +import Data.Text (Text) import qualified Data.Text as T -import qualified Data.Text.Lazy as TL -import qualified Data.Version as Version (showVersion) -import Data.Version (Version) -import Data.Void -import Control.Monad(when) -import Prettyprinter +import Data.Version (Version) +import qualified Data.Version as Version ( showVersion ) +import Data.Void +import qualified Lumberjack as LJ +import Prettyprinter import qualified Prettyprinter.Render.Text as PR -import System.Console.Terminal.Size ( size, Window(..) ) -import System.Exit(exitSuccess, ExitCode(..), exitFailure, exitWith) -import System.Directory(createDirectoryIfMissing) -import System.FilePath(()) - -import Data.Parameterized.Classes -import Data.Parameterized.Nonce(newIONonceGenerator, NonceGenerator) -import Data.Parameterized.Some ( Some(..) ) - -import Lang.Crucible.Backend -import Lang.Crucible.Backend.Online +import qualified System.Console.ANSI as AC +import System.Console.Terminal.Size ( size, Window(..) ) +import System.Directory (createDirectoryIfMissing) +import System.Exit (exitSuccess, ExitCode(..), exitFailure, exitWith) +import System.FilePath (()) +import System.IO ( Handle, hPutStr, stdout, stderr ) + +import Data.Parameterized.Classes +import Data.Parameterized.Nonce (newIONonceGenerator, NonceGenerator) +import Data.Parameterized.Some ( Some(..) ) + +import Lang.Crucible.Backend +import Lang.Crucible.Backend.Online import qualified Lang.Crucible.Backend.Simple as CBS -import Lang.Crucible.CFG.Extension -import Lang.Crucible.Simulator -import Lang.Crucible.Simulator.BoundedExec -import Lang.Crucible.Simulator.BoundedRecursion -import Lang.Crucible.Simulator.Profiling -import Lang.Crucible.Simulator.PathSatisfiability -import Lang.Crucible.Simulator.PathSplitting -import Lang.Crucible.Types - - -import What4.Config (Opt, ConfigOption, setOpt, getOptionSetting, verbosity, extendConfig) -import What4.InterpretedFloatingPoint (IsInterpretedFloatExprBuilder) -import What4.Interface (IsExprBuilder, getConfiguration) -import What4.Expr (GroundEvalFn) +import Lang.Crucible.CFG.Extension +import Lang.Crucible.Simulator +import Lang.Crucible.Simulator.BoundedExec +import Lang.Crucible.Simulator.BoundedRecursion +import Lang.Crucible.Simulator.PathSatisfiability +import Lang.Crucible.Simulator.PathSplitting +import Lang.Crucible.Simulator.Profiling +import Lang.Crucible.Types + + +import What4.Config (Opt, ConfigOption, setOpt, getOptionSetting, verbosity, extendConfig) +import What4.Expr (GroundEvalFn) import qualified What4.Expr.Builder as WEB -import What4.FunctionName (FunctionName) -import What4.Protocol.Online (OnlineSolver) +import What4.FunctionName (FunctionName) +import What4.Interface (IsExprBuilder, getConfiguration) +import What4.InterpretedFloatingPoint (IsInterpretedFloatExprBuilder) +import What4.Protocol.Online (OnlineSolver) import qualified What4.Solver as WS -import What4.Solver.CVC4 (cvc4Timeout) -import What4.Solver.Z3 (z3Timeout) -import What4.Solver.Yices (yicesEnableMCSat, yicesGoalTimeout) - -import Crux.Log -import Crux.Types -import Crux.Config -import Crux.Goal -import Crux.Report +import What4.Solver.CVC4 (cvc4Timeout) +import What4.Solver.Yices (yicesEnableMCSat, yicesGoalTimeout) +import What4.Solver.Z3 (z3Timeout) + +import Crux.Config +import Crux.Config.Common +import Crux.Config.Doc import qualified Crux.Config.Load as Cfg import qualified Crux.Config.Solver as CCS -import Crux.Config.Common -import Crux.Config.Doc +import Crux.FormatOut ( sayWhatFailedGoals, sayWhatResultStatus ) +import Crux.Goal +import Crux.Log +import Crux.Report +import Crux.Types import qualified Crux.Version as Crux pattern RunnableState :: forall sym . () => forall ext personality . (IsSyntaxExtension ext, HasModel personality) => ExecState (personality sym) sym ext (RegEntry sym UnitType) -> RunnableState sym @@ -125,11 +130,8 @@ newtype SimulatorCallback -- status, generate user-consumable reports and compute the exit code. postprocessSimResult :: Logs => CruxOptions -> CruxSimulationResult -> IO ExitCode postprocessSimResult opts res = - do -- print goals that failed - printFailedGoals opts res - - -- print the overall result - reportStatus res + do -- print goals that failed and overall result + logSimResult res -- Generate report generateReport opts res @@ -144,44 +146,100 @@ postprocessSimResult opts res = -- just print something and exit, so this function may never call -- its continuation. loadOptions :: - OutputConfig -> + (Maybe CruxOptions -> OutputConfig) -> Text {- ^ Name -} -> Version -> Config opts -> (Logs => (CruxOptions, opts) -> IO a) -> IO a -loadOptions outCfg nm ver config cont = +loadOptions mkOutCfg nm ver config cont = do let optSpec = cfgJoin cruxOptions config opts <- Cfg.loadConfig nm optSpec case opts of Cfg.ShowHelp -> - do let ?outputConfig = outCfg + do let ?outputConfig = mkOutCfg Nothing showHelp nm optSpec exitSuccess Cfg.ShowVersion -> - do let ?outputConfig = outCfg + do let ?outputConfig = mkOutCfg Nothing showVersion nm ver exitSuccess Cfg.Options (crux, os) files -> - do let ?outputConfig = outCfg & quiet %~ (|| quietMode crux) + do let ?outputConfig = mkOutCfg (Just crux) crux' <- postprocessOptions crux { inputFiles = files ++ inputFiles crux } cont (crux', os) `Ex.catch` \(e :: Ex.SomeException) -> - do let ?outputConfig = outCfg + do let ?outputConfig = mkOutCfg Nothing case (Ex.fromException e :: Maybe ExitCode) of Just exitCode -> exitWith exitCode - Nothing -> sayFail "Crux" (Ex.displayException e) >> exitFailure + Nothing -> logException e >> exitFailure + showHelp :: Logs => Text -> Config opts -> IO () showHelp nm cfg = do outWidth <- maybe 80 (\(Window _ w) -> w) <$> size let opts = LayoutOptions $ AvailablePerLine outWidth 0.98 - outputLn (TL.unpack $ PR.renderLazy $ layoutPretty opts (configDocs nm cfg)) + say OK "Crux" (PR.renderStrict $ layoutPretty opts (configDocs nm cfg)) showVersion :: Logs => Text -> Version -> IO () showVersion nm ver = - outputLn $ "crux version: " <> Crux.version <> ", " <> Text.unpack nm <> " version: " <> Version.showVersion ver + say OK "Crux" $ T.unwords [ "version: " <> T.pack Crux.version <> "," + , nm + , "version: " <> T.pack (Version.showVersion ver) + ] + + +-- | Create an OutputConfig for Crux, based on an indication of +-- whether colored output should be used, the normal and error output +-- handles, and the parsed CruxOptions. The following CruxOptions +-- affect the generated OutputConfig: +-- +-- printFailures +-- quietMode + +mkOutputConfig :: Bool -> Handle -> Handle -> Maybe CruxOptions -> OutputConfig +mkOutputConfig withColors outHandle errHandle opts = + let lgWhat = let la = LJ.LogAction $ logToStd withColors outHandle errHandle + -- TODO simVerbose may not be the best setting to use here... + baseline = if maybe False ((> 1) . simVerbose) opts + then Noisily + else Simply + in if maybe False quietMode opts + then logfltr OK >$< la + else logfltr baseline >$< la + logfltr allowed = \case + SayNothing -> SayNothing + w@(SayWhat lvl _ _) -> if lvl >= allowed then w else SayNothing + SayMore m1 m2 -> case (logfltr allowed m1, logfltr allowed m2) of + (SayNothing, SayNothing) -> SayNothing + (SayNothing, m) -> m + (m, SayNothing) -> m + (m1', m2') -> SayMore m1' m2' + + lgGoal = sayWhatFailedGoals (maybe True printFailures opts) >$< lgWhat + splitResults r@(CruxSimulationResult _cmpl gls) = (snd <$> gls, r) + in OutputConfig + { + _outputHandle = outHandle + , _quiet = maybe True quietMode opts + , _logWhat = lgWhat + , _logExc = let seeRed = AC.hSetSGR errHandle + [ AC.SetConsoleIntensity AC.BoldIntensity + , AC.SetColor AC.Foreground AC.Vivid AC.Red] + seeCalm = AC.hSetSGR errHandle [AC.Reset] + dispExc = hPutStr errHandle . Ex.displayException + in if withColors + then LJ.LogAction $ \e -> Ex.bracket_ seeRed seeCalm $ dispExc e + else LJ.LogAction $ dispExc + , _logSimResult = divide splitResults + lgGoal + (sayWhatResultStatus >$< lgWhat) + , _logGoal = Seq.singleton >$< lgGoal + } + +defaultOutputConfig :: Maybe CruxOptions -> OutputConfig +defaultOutputConfig = Crux.mkOutputConfig True stdout stderr -------------------------------------------------------------------------------- @@ -283,7 +341,7 @@ withSelectedOnlineBackend cruxOpts nonceGen selectedSolver maybeExplicitFloatMod CCS.STP -> do -- We don't have a timeout option for STP case goalTimeout cruxOpts of - Just _ -> sayWarn "Crux" "Goal timeout requested but not supported by STP" + Just _ -> say Warn "Crux" "Goal timeout requested but not supported by STP" Nothing -> return () withSTPOnlineBackend floatRepr nonceGen (k floatRepr) @@ -436,14 +494,6 @@ withSolverAdapters solverOffs k = base adapters = k adapters go nextOff withAdapters adapters = withSolverAdapter nextOff (\adapter -> withAdapters (adapter:adapters)) -withOutputConfig :: - OutputConfig -> - CruxOptions -> - (Logs => a) -> - a -withOutputConfig outCfg opts k = k - where ?outputConfig = outCfg & quiet %~ (|| (quietMode opts)) - -- | Parse through all of the user-provided options and start up the verification process -- -- This figures out which solvers need to be run, and in which modes. It takes @@ -456,9 +506,8 @@ runSimulator :: SimulatorCallback -> IO CruxSimulationResult runSimulator cruxOpts simCallback = do - when (simVerbose cruxOpts > 1) $ - do let fileText = intercalate ", " (map show (inputFiles cruxOpts)) - say "Crux" ("Checking " ++ fileText) + say Noisily "Crux" ("Checking " + <> T.intercalate ", " (T.pack <$> inputFiles cruxOpts)) createDirectoryIfMissing True (outDir cruxOpts) compRef <- newIORef ProgramComplete glsRef <- newIORef Seq.empty @@ -562,13 +611,13 @@ doSimWithResults cruxOpts simCallback compRef glsRef sym execFeatures profInfo m (map genericToExecutionFeature execFeatures ++ exts) initSt (resultCont frm explainFailure . Result) - say "Crux" ("Total paths explored: " ++ show i) + say Simply "Crux" ("Total paths explored: " <> T.pack (show i)) unless (null ws) $ - sayWarn "Crux" - (unwords [show (Seq.length ws), "paths remaining not explored: program might not be fully verified"]) + say Warn "Crux" + (T.unwords [ T.pack $ show (Seq.length ws) + , "paths remaining not explored: program might not be fully verified"]) - when (simVerbose cruxOpts > 1) $ do - say "Crux" "Simulation complete." + say Noisily "Crux" "Simulation complete." when (isProfiling cruxOpts) $ writeProf profInfo CruxSimulationResult <$> readIORef compRef <*> readIORef glsRef @@ -579,7 +628,7 @@ doSimWithResults cruxOpts simCallback compRef glsRef sym execFeatures profInfo m do timedOut <- case res of TimeoutResult {} -> - do sayWarn "Crux" "Simulation timed out! Program might not be fully verified!" + do say Warn "Crux" "Simulation timed out! Program might not be fully verified!" writeIORef compRef ProgramIncomplete return True _ -> return False @@ -588,7 +637,7 @@ doSimWithResults cruxOpts simCallback compRef glsRef sym execFeatures profInfo m inFrame profInfo "" $ do todo <- getProofObligations sym when (isJust todo) $ - say "Crux" "Attempting to prove verification conditions." + say Simply "Crux" "Attempting to prove verification conditions." (nms, proved) <- goalProver cruxOpts ctx explainFailure todo mgt <- provedGoalsTree ctx proved case mgt of @@ -614,55 +663,3 @@ computeExitCode (CruxSimulationResult cmpl gls) = maximum . (base:) . fmap f . t ExitSuccess else ExitFailure 1 - -printFailedGoals :: - Logs => - CruxOptions -> - CruxSimulationResult -> - IO () -printFailedGoals opts (CruxSimulationResult _cmpl allGls) - | printFailures opts && not (quietMode opts) = mapM_ (printFailed . snd) (toList allGls) - | otherwise = return () - - where - printFailed (AtLoc _ _ gls) = printFailed gls - printFailed (Branch gls1 gls2) = printFailed gls1 >> printFailed gls2 - printFailed (Goal _asmps _goal _trivial (Proved _)) = return () - printFailed (Goal _asmps (err, _msg) _trivial (NotProved ex mdl)) - | skipIncompleteReports opts - , SimError _ (ResourceExhausted _) <- err - = return () - - | Just _ <- mdl - = sayFail "Crux" (show $ vcat [ "Found counterexample for verification goal", ex ]) - - | otherwise - = sayFail "Crux" (show $ vcat [ "Failed to prove verification goal", ex ]) - -reportStatus :: - Logs => - CruxSimulationResult -> - IO () -reportStatus (CruxSimulationResult cmpl gls) = - do let tot = sum (totalProcessedGoals . fst <$> gls) - proved = sum (provedGoals . fst <$> gls) - disproved = sum (disprovedGoals . fst <$> gls) - incomplete = sum (incompleteGoals . fst <$> gls) - unknown = tot - (proved + disproved + incomplete) - if tot == 0 then - do say "Crux" "All goals discharged through internal simplification." - else - do say "Crux" "Goal status:" - say "Crux" (" Total: " ++ show tot) - say "Crux" (" Proved: " ++ show proved) - say "Crux" (" Disproved: " ++ show disproved) - say "Crux" (" Incomplete: " ++ show incomplete) - say "Crux" (" Unknown: " ++ show unknown) - if | disproved > 0 -> - sayFail "Crux" "Overall status: Invalid." - | incomplete > 0 || cmpl == ProgramIncomplete -> - sayWarn "Crux" "Overall status: Unknown (incomplete)." - | unknown > 0 -> sayWarn "Crux" "Overall status: Unknown." - | proved == tot -> sayOK "Crux" "Overall status: Valid." - | otherwise -> - sayFail "Crux" "Internal error computing overall status." diff --git a/crux/src/Crux/Config/Common.hs b/crux/src/Crux/Config/Common.hs index 7927ae6e5..e3cc543b0 100644 --- a/crux/src/Crux/Config/Common.hs +++ b/crux/src/Crux/Config/Common.hs @@ -37,7 +37,7 @@ checkPathStrategyInteractions crux = AlwaysMergePaths -> return crux SplitAndExploreDepthFirst | profileCrucibleFunctions crux || branchCoverage crux -> - do sayWarn "Crux" "Path splitting strategies are incompatible with Crucible profiling. Profiling is disabled!" + do say Warn "Crux" "Path splitting strategies are incompatible with Crucible profiling. Profiling is disabled!" return crux { profileCrucibleFunctions = False, branchCoverage = False } | otherwise -> return crux @@ -47,7 +47,7 @@ checkPathSatInteractions crux = True -> return crux False | branchCoverage crux -> - do sayWarn "Crux" "Branch coverage requires enabling path satisfiability checking. Coverage measurement is disabled!" + do say Warn "Crux" "Branch coverage requires enabling path satisfiability checking. Coverage measurement is disabled!" return crux { branchCoverage = False } | otherwise -> return crux diff --git a/crux/src/Crux/FormatOut.hs b/crux/src/Crux/FormatOut.hs new file mode 100644 index 000000000..6cbdcd5d1 --- /dev/null +++ b/crux/src/Crux/FormatOut.hs @@ -0,0 +1,90 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE OverloadedStrings #-} +-- | This module provides various default formatters for outputting +-- information in human readable form. Alternative versions should be +-- used where appropriate. + +module Crux.FormatOut + ( + sayWhatResultStatus + , sayWhatFailedGoals + ) +where + +import Data.Foldable ( toList ) +import Data.Sequence (Seq) +import Data.Text ( Text ) +import Prettyprinter ( (<+>) ) +import qualified Prettyprinter as PP +import qualified Prettyprinter.Render.Text as PPR + +import Lang.Crucible.Backend ( AssumptionReason ) +import qualified Lang.Crucible.Simulator.SimError as CSE + +import Crux.Types + + +sayWhatResultStatus :: CruxSimulationResult -> SayWhat +sayWhatResultStatus (CruxSimulationResult cmpl gls) = + let tot = sum (totalProcessedGoals . fst <$> gls) + proved = sum (provedGoals . fst <$> gls) + disproved = sum (disprovedGoals . fst <$> gls) + incomplete = sum (incompleteGoals . fst <$> gls) + unknown = tot - (proved + disproved + incomplete) + goalSummary = if tot == 0 then + "All goals discharged through internal simplification." + else + PP.nest 2 $ + PP.vcat [ "Goal status:" + , "Total:" <+> PP.pretty tot + , "Proved:" <+> PP.pretty proved + , "Disproved:" <+> PP.pretty disproved + , "Incomplete:" <+> PP.pretty incomplete + , "Unknown:" <+> PP.pretty unknown + ] + in SayMore + (SayWhat Simply "Crux" $ ppToText goalSummary) + $ if | disproved > 0 -> + SayWhat Fail "Crux" "Overall status: Invalid." + | incomplete > 0 || cmpl == ProgramIncomplete -> + SayWhat Warn "Crux" "Overall status: Unknown (incomplete)." + | unknown > 0 -> SayWhat Warn "Crux" "Overall status: Unknown." + | proved == tot -> SayWhat OK "Crux" "Overall status: Valid." + | otherwise -> + SayWhat Fail "Crux" "Internal error computing overall status." + +sayWhatFailedGoals :: Bool + -> Seq (ProvedGoals (Either AssumptionReason CSE.SimError)) + -> SayWhat +sayWhatFailedGoals skipIncompl allGls = + let failedDoc = \case + AtLoc _ _ gls -> failedDoc gls + Branch gls1 gls2 -> failedDoc gls1 <> failedDoc gls2 + Goal _asmps _goal _trivial (Proved _) -> [] + Goal _asmps (err, _msg) _trivial (NotProved ex mdl) -> + if | skipIncompl, CSE.SimError _ (CSE.ResourceExhausted _) <- err -> [] + | Just _ <- mdl -> + [ PP.nest 2 $ PP.vcat + [ "Found counterexample for verification goal" + -- n.b. prefer the prepared pretty explanation, but + -- if not available, use the NotProved information. + -- Don't show both: they tend to be duplications. + , if null (show ex) then PP.viaShow err else ex + -- TODO the msg is typically the string + -- representation of the crucible term that failed. + -- It might be nice to have a debug or noisy flag + -- that would enable emitting this, since it tends + -- to be rather lengthy. + -- , PP.pretty msg + ] ] + | otherwise -> + [ PP.nest 2 $ PP.vcat [ "Failed to prove verification goal", ex ] ] + allDocs = mconcat (failedDoc <$> toList allGls) + in if null allDocs + then SayNothing + else SayWhat Fail "Crux" $ ppToText $ PP.vsep allDocs + + +ppToText :: PP.Doc ann -> Text +ppToText = PPR.renderStrict . PP.layoutPretty PP.defaultLayoutOptions diff --git a/crux/src/Crux/Goal.hs b/crux/src/Crux/Goal.hs index 0521329bb..96e15f0f0 100644 --- a/crux/src/Crux/Goal.hs +++ b/crux/src/Crux/Goal.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# Language ImplicitParams #-} @@ -245,8 +246,8 @@ proveGoalsOffline adapters opts ctx explainFailure (Just gs0) = do case details of NotProved _ (Just _) -> when (failfast && not (isResourceExhausted p)) $ - sayOK "Crux" "Counterexample found, skipping remaining goals" - _ -> return () + say OK "Crux" "Counterexample found, skipping remaining goals" + _ -> return () return (Prove (p, details)) Left es -> do modifyIORef' goalNum (updateProcessedGoals p (NotProved mempty Nothing)) @@ -308,7 +309,7 @@ dispatchSolversOnGoalAsync mtimeoutSeconds adapters withAdapter = do await as' es Nothing -> do mapM_ kill as - return $ Right $ NotProved (pretty "(Timeout)") Nothing + return $ Right $ NotProved "(Timeout)" Nothing withTimeout action | Just seconds <- mtimeoutSeconds = ST.timeout (round seconds * 1000000) action @@ -348,7 +349,7 @@ proveGoalsOnline sym opts ctxt explainFailure (Just gs0) = do goalNum <- newIORef (ProcessedGoals 0 0 0 0) nameMap <- newIORef Map.empty when (unsatCores opts && yicesMCSat opts) $ - sayWarn "Crux" "Warning: skipping unsat cores because MC-SAT is enabled." + say Warn "Crux" "Warning: skipping unsat cores because MC-SAT is enabled." (start,end,finish) <- if view quiet ?outputConfig then return (\_ -> return (), return (), return ()) @@ -408,7 +409,7 @@ proveGoalsOnline sym opts ctxt explainFailure (Just gs0) = let gt = NotProved explain (Just (ModelView vals)) modifyIORef' gn (updateProcessedGoals p gt) when (failfast && not (isResourceExhausted p)) $ - (sayOK "Crux" "Counterexample found, skipping remaining goals.") + (say OK "Crux" "Counterexample found, skipping remaining goals.") return (Prove (p, gt)) Unknown -> do explain <- explainFailure Nothing p diff --git a/crux/src/Crux/Log.hs b/crux/src/Crux/Log.hs index 7b859791f..3f517d610 100644 --- a/crux/src/Crux/Log.hs +++ b/crux/src/Crux/Log.hs @@ -1,80 +1,163 @@ -{-# LANGUAGE ImplicitParams, ConstraintKinds #-} --- from crucible-c/src/Log.hs +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} + module Crux.Log ( - -- * Configuring output + -- * Output Configuration Logs, - OutputConfig(..), showColors, outputHandle, errorHandle, defaultOutputConfig, quiet, - -- * Performing output - say, sayOK, sayWarn, sayFail, output, outputLn + OutputConfig(..) + , outputHandle + , quiet + -- * Standard output API functions + , SayWhat(..) + , SayLevel(..) + , say + , logException + , logSimResult + , logGoal + -- * Low-level output API functions + , output + , outputLn + -- * Converting and emitting output + , logToStd ) where -import Control.Exception (bracket_) -import Control.Lens +import Control.Exception ( SomeException, bracket_, ) +import Control.Lens +import Data.Text ( Text, lines ) +import Data.Text.IO as TIO +import qualified Lumberjack as LJ +import System.Console.ANSI +import System.IO + +import Lang.Crucible.Backend ( AssumptionReason ) +import qualified Lang.Crucible.Simulator.SimError as CSE + +import Crux.Types + +---------------------------------------------------------------------- +-- Various functions used by the main code to generate logging output + +-- | Main function used to log/output a general text message of some kind +say :: Logs => SayLevel -> Text -> Text -> IO () +say lvl frm = LJ.writeLog (?outputConfig ^. logWhat) . SayWhat lvl frm + +-- | Function used to log/output exception information +logException :: Logs => SomeException -> IO () +logException = LJ.writeLog (_logExc ?outputConfig) + +-- | Function used to output the summary result for a completed simulation +logSimResult :: Logs => CruxSimulationResult -> IO () +logSimResult = LJ.writeLog (_logSimResult ?outputConfig) -import System.Console.ANSI -import System.IO +-- | Function used to output any individual goal proof failures from a simulation +logGoal :: Logs => ProvedGoals (Either AssumptionReason CSE.SimError) -> IO () +logGoal = LJ.writeLog (_logGoal ?outputConfig) + +---------------------------------------------------------------------- +-- Logging types and constraints + +-- | The Logs constraint should be applied for any function that will +-- use the main logging functions: says, logException, logSimResult, +-- or logGoal. type Logs = (?outputConfig :: OutputConfig) -- | Global options for Crux's main. These are not CruxOptions because -- they are expected to be set directly by main, rather than by a -- user's command-line options. They exist primarily to improve the -- testability of the code. +-- +-- The Crux mkOutputConfig is recommended as a helper function for +-- creating this object, although it can be initialized directly if +-- needed. data OutputConfig = - OutputConfig { _showColors :: Bool - , _outputHandle :: Handle - , _errorHandle :: Handle + OutputConfig { _outputHandle :: Handle , _quiet :: Bool + , _logWhat :: LJ.LogAction IO SayWhat + , _logExc :: LJ.LogAction IO SomeException + , _logSimResult :: LJ.LogAction IO CruxSimulationResult + , _logGoal :: LJ.LogAction IO (ProvedGoals + (Either AssumptionReason + CSE.SimError)) } -showColors :: Lens' OutputConfig Bool -showColors = lens _showColors (\ o s -> o { _showColors = s }) - -outputHandle :: Lens' OutputConfig Handle -outputHandle = lens _outputHandle (\ o h -> o { _outputHandle = h }) - -errorHandle :: Lens' OutputConfig Handle -errorHandle = lens _errorHandle (\ o h -> o { _errorHandle = h }) - -quiet :: Lens' OutputConfig Bool -quiet = lens _quiet (\ o b -> o { _quiet = b }) - -defaultOutputConfig :: OutputConfig -defaultOutputConfig = OutputConfig True stdout stderr False +-- | Some client code will want to output to the main output stream +-- directly instead of using the logging/output functions above. It +-- can either get the _outputHandle directly or it can use the +-- output/outputLn functions below. +outputHandle :: Getter OutputConfig Handle +outputHandle f o = o <$ f (_outputHandle o) + +-- | Lens to allow client code to determine if running in quiet mode. +quiet :: Getter OutputConfig Bool +quiet f o = o <$ f (_quiet o) + +logWhat :: Getter OutputConfig (LJ.LogAction IO SayWhat) +logWhat f o = o <$ f (_logWhat o) + + +---------------------------------------------------------------------- +-- Logging default implementations (can be over-ridden by different +-- front end configurations). + +-- | This is the default logging output function for a SayWhat +-- message. It will emit the information with possible coloring (if +-- enabled via the first argument) to the proper handle (normal output +-- goes to the first handle, error output goes to the second handle, +-- and the same handle may be used for both). +-- +-- Front-ends that don't have specific output needs can simply use +-- this function. Alternative output functions can be used where +-- useful (e.g. JSON output). +logToStd :: Bool -> Handle -> Handle -> SayWhat -> IO () +logToStd withColors outH errH = \case + SayWhat lvl frm msg -> + let sayer = case lvl of + OK -> colOut Green outH + Warn -> colOut Yellow errH + Fail -> colOut Red errH + Simply -> straightOut outH + Noisily -> straightOut outH + colOut clr = + if withColors + then \hndl l -> do bracket_ + (hSetSGR hndl [ SetConsoleIntensity BoldIntensity + , SetColor Foreground Vivid clr]) + (hSetSGR hndl [Reset]) + (TIO.hPutStr hndl $ "[" <> frm <> "] ") + TIO.hPutStrLn hndl l + else straightOut + straightOut hndl l = do TIO.hPutStr hndl $ "[" <> frm <> "] " + TIO.hPutStrLn hndl l + in mapM_ sayer $ Data.Text.lines msg + SayMore s1 s2 -> do logToStd withColors outH errH s1 + logToStd withColors outH errH s2 + SayNothing -> return () + + +---------------------------------------------------------------------- +-- Direct Output + +-- | This function emits output to the normal output handle (specified +-- at initialization time). This function is not recommended for +-- general use (the 'says', 'logException', 'logSimResult', 'logGoal', +-- etc. are preferred), but can be used by code needing more control +-- over the output formatting. +-- +-- This function does _not_ emit a newline at the end of the output. output :: Logs => String -> IO () -output str = hPutStr (view outputHandle ?outputConfig) str +output str = System.IO.hPutStr (view outputHandle ?outputConfig) str + +-- | This function emits output to the normal output handle (specified +-- at initialization time). This function is not recommended for +-- general use (the 'says', 'logException', 'logSimResult', 'logGoal', +-- etc. are preferred), but can be used by code needing more control +-- over the output formatting. +-- +-- This function emits a newline at the end of the output. outputLn :: Logs => String -> IO () -outputLn str = hPutStrLn (view outputHandle ?outputConfig) str - -outputColored :: Logs => Color -> String -> IO () -outputColored c msg = - let outH = view outputHandle ?outputConfig - inColor = view showColors ?outputConfig - in if inColor - then bracket_ - (hSetSGR outH [SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid c]) - (hSetSGR outH [Reset]) - (hPutStr outH msg) - else output msg - -sayOK :: Logs => String -> String -> IO () -sayOK = sayCol Green - -sayWarn :: Logs => String -> String -> IO () -sayWarn = sayCol Yellow - -sayFail :: Logs => String -> String -> IO () -sayFail = sayCol Red - -say :: Logs => String -> String -> IO () -say x y - | view quiet ?outputConfig = return () - | otherwise = outputLn ("[" ++ x ++ "] " ++ y) - -sayCol :: Logs => Color -> String -> String -> IO () -sayCol col x y = - do output "[" - outputColored col x - outputLn ("] " ++ y) +outputLn str = System.IO.hPutStrLn (view outputHandle ?outputConfig) str diff --git a/crux/src/Crux/Types.hs b/crux/src/Crux/Types.hs index 6c44eb18c..9e336f615 100644 --- a/crux/src/Crux/Types.hs +++ b/crux/src/Crux/Types.hs @@ -2,8 +2,9 @@ module Crux.Types where import qualified Control.Lens as L -import Data.Sequence (Seq) import Data.Parameterized.Map (MapF) +import Data.Sequence (Seq) +import Data.Text ( Text ) import Data.Void import Prettyprinter @@ -12,7 +13,6 @@ import What4.Interface (Pred) import What4.ProgramLoc import Lang.Crucible.Backend -import Lang.Crucible.Simulator.SimError import Lang.Crucible.Simulator import Lang.Crucible.Types @@ -76,7 +76,10 @@ data ProcessedGoals = data ProofResult a = Proved [a] - | NotProved (Doc Void) (Maybe ModelView) -- ^ An explanation of the failure and counter example, if any + | NotProved (Doc Void) (Maybe ModelView) + -- ^ The first argument is an explanation of the failure and + -- counter example as provided by the Explainer (if any) and the + -- second maybe a model for the counter-example. deriving (Functor) type LPred sym = LabeledPred (Pred sym) @@ -87,10 +90,17 @@ data ProvedGoals a = | Goal [(AssumptionReason,String)] (SimError,String) Bool (ProofResult a) -- ^ Keeps only the explanations for the relevant assumptions. - -- The 'Maybe Int' in the assumptions corresponds to its depth in the tree - -- (i.e., the step number, if this is a path assumption) - -- The 'Bool' indicates if the goal is trivial (i.e., the assumptions - -- are inconsistent) + -- + -- * The array of (AssumptionReason,String) is the set of + -- assumptions for this Goal. + -- + -- * The (SimError,String) is information about the failure, + -- with the specific SimError (Lang.Crucible.Simulator) and a + -- string representation of the Crucible term that encountered + -- the error. + -- + -- * The 'Bool' (third argument) indicates if the goal is + -- trivial (i.e., the assumptions are inconsistent) data ProgramCompleteness @@ -146,6 +156,15 @@ data Entry ty = Entry { entryName :: String -- conditions under which an SMT query is satisfiable. newtype ModelView = ModelView { modelVals :: MapF BaseTypeRepr Vals } +---------------------------------------------------------------------- +-- Various things that can be logged/output +-- | Specify some general text that should be presented (to the user). +data SayWhat = SayWhat SayLevel Text Text -- ^ fields are: Level From Message + | SayMore SayWhat SayWhat + | SayNothing - +-- | Specify the verbosity/severity level of a message. These are in +-- ordinal order for possible filtering, and higher levels may be sent +-- to a different location (e.g. stderr v.s. stdout). +data SayLevel = Noisily | Simply | OK | Warn | Fail deriving (Eq, Ord) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs index c4d9a018b..dfe28d917 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs @@ -21,7 +21,7 @@ Stability : provisional module UCCrux.LLVM.Main ( mainWithOutputTo, mainWithOutputConfig, - defaultOutputConfig, + Crux.defaultOutputConfig, loopOnFunctions, translateLLVMModule, translateFile, @@ -61,9 +61,7 @@ import Lang.Crucible.LLVM.Translation -- crux import qualified Crux - import Crux.Config.Common -import Crux.Log (say, OutputConfig(..), defaultOutputConfig) -- local import Crux.LLVM.Config @@ -84,13 +82,13 @@ import UCCrux.LLVM.Run.Loop (loopOnFunction) {- ORMOLU_ENABLE -} mainWithOutputTo :: Handle -> IO ExitCode -mainWithOutputTo h = mainWithOutputConfig (OutputConfig False h h False) +mainWithOutputTo h = mainWithOutputConfig $ Crux.mkOutputConfig False h h -mainWithOutputConfig :: OutputConfig -> IO ExitCode -mainWithOutputConfig outCfg = +mainWithOutputConfig :: (Maybe CruxOptions -> Crux.OutputConfig) -> IO ExitCode +mainWithOutputConfig mkOutCfg = do conf <- Config.ucCruxLLVMConfig - Crux.loadOptions outCfg "uc-crux-llvm" version conf $ \opts -> + Crux.loadOptions mkOutCfg "uc-crux-llvm" version conf $ \opts -> do (appCtx, cruxOpts, ucOpts) <- Config.processUCCruxLLVMOptions opts path <- genBitCode cruxOpts (Config.ucLLVMOptions ucOpts) @@ -118,8 +116,9 @@ mainWithOutputConfig outCfg = flip Map.traverseWithKey results $ \func (SomeBugfindingResult result) -> do - say "Crux" ("Results for " <> func) - say "Crux" $ Text.unpack (Result.printFunctionSummary (summary result)) + Crux.say Crux.Simply "Crux" ("Results for " <> Text.pack func) + Crux.say Crux.Simply "Crux" + $ Result.printFunctionSummary (summary result) return ExitSuccess translateLLVMModule :: @@ -168,7 +167,7 @@ translateFile ucOpts halloc memVar moduleFilePath = -- | Postcondition: The keys of the returned map are exactly the entryPoints of -- the 'UCCruxLLVMOptions'. loopOnFunctions :: - (?outputConfig :: OutputConfig) => + (Crux.Logs) => AppContext -> ModuleContext m arch -> Crucible.HandleAllocator -> diff --git a/uc-crux-llvm/test/Test.hs b/uc-crux-llvm/test/Test.hs index 329229883..7226e80c3 100644 --- a/uc-crux-llvm/test/Test.hs +++ b/uc-crux-llvm/test/Test.hs @@ -121,10 +121,9 @@ findBugs llvmModule file fns = withFile (testDir file <> ".output") WriteMode $ \h -> do let isRealFile = isNothing llvmModule - let outCfg = Crux.OutputConfig False h h True + let mkOutCfg = Crux.mkOutputConfig False h h conf <- Config.ucCruxLLVMConfig - (appCtx, path, cruxOpts, ucOpts) <- - Crux.loadOptions outCfg "uc-crux-llvm" version conf $ \(cruxOpts, ucOpts) -> + Crux.loadOptions mkOutCfg "uc-crux-llvm" version conf $ \(cruxOpts, ucOpts) -> do -- With Yices, cast_float_to_pointer_write.c hangs let cruxOpts' = @@ -155,25 +154,23 @@ findBugs llvmModule file fns = Right path -> pure path else pure "" - pure (appCtx, path, cruxOpts'', ucOpts'') - -- TODO(lb): It would be nice to print this only when the test fails - -- putStrLn - -- ( unwords - -- [ "\nReproduce with:\n", - -- "cabal v2-run exe:uc-crux-llvm -- ", - -- "--entry-points", - -- intercalate " --entry-points " (map show fns), - -- testDir file - -- ] - -- ) - let ?outputConfig = outCfg - halloc <- newHandleAllocator - memVar <- mkMemVar "uc-crux-llvm:test_llvm_memory" halloc - SomeModuleContext' modCtx <- - case llvmModule of - Just lMod -> translateLLVMModule ucOpts halloc memVar path lMod - Nothing -> translateFile ucOpts halloc memVar path - loopOnFunctions appCtx modCtx halloc cruxOpts ucOpts + -- TODO(lb): It would be nice to print this only when the test fails + -- putStrLn + -- ( unwords + -- [ "\nReproduce with:\n", + -- "cabal v2-run exe:uc-crux-llvm -- ", + -- "--entry-points", + -- intercalate " --entry-points " (map show fns), + -- testDir file + -- ] + -- ) + halloc <- newHandleAllocator + memVar <- mkMemVar "uc-crux-llvm:test_llvm_memory" halloc + SomeModuleContext' modCtx <- + case llvmModule of + Just lMod -> translateLLVMModule ucOpts'' halloc memVar path lMod + Nothing -> translateFile ucOpts'' halloc memVar path + loopOnFunctions appCtx modCtx halloc cruxOpts'' ucOpts'' inFile :: FilePath -> [(String, String -> Result.SomeBugfindingResult -> IO ())] -> TT.TestTree inFile file specs = diff --git a/uc-crux-llvm/uc-crux-llvm.cabal b/uc-crux-llvm/uc-crux-llvm.cabal index 95d926b60..06966d6de 100644 --- a/uc-crux-llvm/uc-crux-llvm.cabal +++ b/uc-crux-llvm/uc-crux-llvm.cabal @@ -85,7 +85,7 @@ library filepath, lens, llvm-pretty, - lumberjack, + lumberjack >= 1.0 && < 1.1, mtl, panic, parameterized-utils, @@ -139,6 +139,7 @@ test-suite uc-crux-llvm-test crux-llvm, filepath, llvm-pretty, + lumberjack, parameterized-utils, tasty >= 0.10, tasty-hunit >= 0.10, From cc2458fc7b9b60b1116936eeb27f4663c0771bc1 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 4 Jun 2021 16:21:40 -0700 Subject: [PATCH 02/18] uc-crux-llvm updates to satisfy linter. --- uc-crux-llvm/src/UCCrux/LLVM/Main.hs | 2 +- uc-crux-llvm/test/Test.hs | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs index dfe28d917..37ea26511 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs @@ -167,7 +167,7 @@ translateFile ucOpts halloc memVar moduleFilePath = -- | Postcondition: The keys of the returned map are exactly the entryPoints of -- the 'UCCruxLLVMOptions'. loopOnFunctions :: - (Crux.Logs) => + Crux.Logs => AppContext -> ModuleContext m arch -> Crucible.HandleAllocator -> diff --git a/uc-crux-llvm/test/Test.hs b/uc-crux-llvm/test/Test.hs index 7226e80c3..ac6781d4b 100644 --- a/uc-crux-llvm/test/Test.hs +++ b/uc-crux-llvm/test/Test.hs @@ -40,7 +40,6 @@ but may be imprecise. If that's not the current state, such a comment indicates a very real bug. -} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} From 23e56afd79ad469d9b831b14004f54f0390050b4 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 4 Jun 2021 16:46:06 -0700 Subject: [PATCH 03/18] Additional changes to satisfy uc-crux-llvm linter. --- uc-crux-llvm/src/UCCrux/LLVM/Main.hs | 4 +- uc-crux-llvm/test/Test.hs | 88 +++++++++++++--------------- 2 files changed, 42 insertions(+), 50 deletions(-) diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs index 37ea26511..6e80ff5ea 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs @@ -117,8 +117,8 @@ mainWithOutputConfig mkOutCfg = \func (SomeBugfindingResult result) -> do Crux.say Crux.Simply "Crux" ("Results for " <> Text.pack func) - Crux.say Crux.Simply "Crux" - $ Result.printFunctionSummary (summary result) + Crux.say Crux.Simply "Crux" $ + Result.printFunctionSummary (summary result) return ExitSuccess translateLLVMModule :: diff --git a/uc-crux-llvm/test/Test.hs b/uc-crux-llvm/test/Test.hs index ac6781d4b..acb400a66 100644 --- a/uc-crux-llvm/test/Test.hs +++ b/uc-crux-llvm/test/Test.hs @@ -48,7 +48,7 @@ a very real bug. module Main (main) where {- ORMOLU_DISABLE -} -import Control.Exception (SomeException, try, displayException) +import Control.Exception ( try ) import Data.Foldable (for_) import qualified Data.Text as Text import qualified Data.Map as Map @@ -122,54 +122,46 @@ findBugs llvmModule file fns = let isRealFile = isNothing llvmModule let mkOutCfg = Crux.mkOutputConfig False h h conf <- Config.ucCruxLLVMConfig - Crux.loadOptions mkOutCfg "uc-crux-llvm" version conf $ \(cruxOpts, ucOpts) -> - do - -- With Yices, cast_float_to_pointer_write.c hangs - let cruxOpts' = - cruxOpts - { Crux.inputFiles = [testDir file], - Crux.solver = "z3" - } - let ucOpts' = ucOpts {Config.entryPoints = fns} - (appCtx, cruxOpts'', ucOpts'') <- Config.processUCCruxLLVMOptions (cruxOpts', ucOpts') - path <- - if isRealFile - then - try - ( genBitCode - cruxOpts'' - ( (Config.ucLLVMOptions ucOpts') - { -- NB(lb): The -fno-wrapv here ensures that - -- Clang will emit 'nsw' flags even on platforms - -- using nixpkgs, which injects - -- -fno-strict-overflow by default. - clangOpts = ["-fno-wrapv"] - } - ) - ) - >>= \case - Left (exc :: SomeException) -> - error ("Trouble when running Clang:" ++ displayException exc) - Right path -> pure path - else pure "" + Crux.loadOptions mkOutCfg "uc-crux-llvm" version conf $ \(cruxOpts, ucOpts) -> do + let cruxOpts' = cruxOpts + { Crux.inputFiles = [testDir file], + -- With Yices, cast_float_to_pointer_write.c hangs + Crux.solver = "z3" + } + let ucOpts' = ucOpts {Config.entryPoints = fns} + (appCtx, cruxOpts'', ucOpts'') <- Config.processUCCruxLLVMOptions (cruxOpts', ucOpts') + path <- do let uclopts = (Config.ucLLVMOptions ucOpts') + { -- NB(lb): The -fno-wrapv here ensures that + -- Clang will emit 'nsw' flags even on platforms + -- using nixpkgs, which injects + -- -fno-strict-overflow by default. + clangOpts = ["-fno-wrapv"] + } + complain exc = do + Crux.say Crux.Fail "UC-Crux-LLVM" "Trouble when running Clang:" + Crux.logException exc + error "aborting" + if isRealFile + then try (genBitCode cruxOpts'' uclopts) >>= either complain return + else return "" - -- TODO(lb): It would be nice to print this only when the test fails - -- putStrLn - -- ( unwords - -- [ "\nReproduce with:\n", - -- "cabal v2-run exe:uc-crux-llvm -- ", - -- "--entry-points", - -- intercalate " --entry-points " (map show fns), - -- testDir file - -- ] - -- ) - halloc <- newHandleAllocator - memVar <- mkMemVar "uc-crux-llvm:test_llvm_memory" halloc - SomeModuleContext' modCtx <- - case llvmModule of - Just lMod -> translateLLVMModule ucOpts'' halloc memVar path lMod - Nothing -> translateFile ucOpts'' halloc memVar path - loopOnFunctions appCtx modCtx halloc cruxOpts'' ucOpts'' + -- TODO(lb): It would be nice to print this only when the test fails + -- putStrLn + -- ( unwords + -- [ "\nReproduce with:\n", + -- "cabal v2-run exe:uc-crux-llvm -- ", + -- "--entry-points", + -- intercalate " --entry-points " (map show fns), + -- testDir file + -- ] + -- ) + halloc <- newHandleAllocator + memVar <- mkMemVar "uc-crux-llvm:test_llvm_memory" halloc + SomeModuleContext' modCtx <- + case llvmModule of + Just lMod -> translateLLVMModule ucOpts'' halloc memVar path lMod + Nothing -> translateFile ucOpts'' halloc memVar path + loopOnFunctions appCtx modCtx halloc cruxOpts'' ucOpts'' inFile :: FilePath -> [(String, String -> Result.SomeBugfindingResult -> IO ())] -> TT.TestTree inFile file specs = From a6bf2938743169039c275d463659e704bda2656a Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 4 Jun 2021 16:52:43 -0700 Subject: [PATCH 04/18] Resolve yet more uc-crux-llvm linter grievances. --- uc-crux-llvm/test/Test.hs | 41 +++++++++++++++++++++------------------ 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/uc-crux-llvm/test/Test.hs b/uc-crux-llvm/test/Test.hs index acb400a66..812589678 100644 --- a/uc-crux-llvm/test/Test.hs +++ b/uc-crux-llvm/test/Test.hs @@ -123,27 +123,30 @@ findBugs llvmModule file fns = let mkOutCfg = Crux.mkOutputConfig False h h conf <- Config.ucCruxLLVMConfig Crux.loadOptions mkOutCfg "uc-crux-llvm" version conf $ \(cruxOpts, ucOpts) -> do - let cruxOpts' = cruxOpts - { Crux.inputFiles = [testDir file], - -- With Yices, cast_float_to_pointer_write.c hangs - Crux.solver = "z3" - } + let cruxOpts' = + cruxOpts + { Crux.inputFiles = [testDir file], + -- With Yices, cast_float_to_pointer_write.c hangs + Crux.solver = "z3" + } let ucOpts' = ucOpts {Config.entryPoints = fns} (appCtx, cruxOpts'', ucOpts'') <- Config.processUCCruxLLVMOptions (cruxOpts', ucOpts') - path <- do let uclopts = (Config.ucLLVMOptions ucOpts') - { -- NB(lb): The -fno-wrapv here ensures that - -- Clang will emit 'nsw' flags even on platforms - -- using nixpkgs, which injects - -- -fno-strict-overflow by default. - clangOpts = ["-fno-wrapv"] - } - complain exc = do - Crux.say Crux.Fail "UC-Crux-LLVM" "Trouble when running Clang:" - Crux.logException exc - error "aborting" - if isRealFile - then try (genBitCode cruxOpts'' uclopts) >>= either complain return - else return "" + path <- do + let uclopts = + (Config.ucLLVMOptions ucOpts') + { -- NB(lb): The -fno-wrapv here ensures that + -- Clang will emit 'nsw' flags even on platforms + -- using nixpkgs, which injects + -- -fno-strict-overflow by default. + clangOpts = ["-fno-wrapv"] + } + complain exc = do + Crux.say Crux.Fail "UC-Crux-LLVM" "Trouble when running Clang:" + Crux.logException exc + error "aborting" + if isRealFile + then try (genBitCode cruxOpts'' uclopts) >>= either complain return + else return "" -- TODO(lb): It would be nice to print this only when the test fails -- putStrLn From 8190a28dba373b494c7d60785ce94ed33f6bc6be Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 7 Jun 2021 08:01:29 -0700 Subject: [PATCH 05/18] Pass known cruxOpts to output config in crucible-concurrency. --- crucible-concurrency/src/Cruces/ExploreCrux.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crucible-concurrency/src/Cruces/ExploreCrux.hs b/crucible-concurrency/src/Cruces/ExploreCrux.hs index 4b7ccd72d..2c13a442d 100644 --- a/crucible-concurrency/src/Cruces/ExploreCrux.hs +++ b/crucible-concurrency/src/Cruces/ExploreCrux.hs @@ -117,7 +117,7 @@ exploreOvr symOnline cruxOpts mainAct = ctx <- use stateContext todo <- liftIO $ getProofObligations sym let cruxOpts' = cruxOpts { Crux.quietMode = True, Crux.simVerbose = 0 } - let ?outputConfig = Crux.defaultOutputConfig Nothing + let ?outputConfig = Crux.defaultOutputConfig $ Just cruxOpts' (processed, _) <- liftIO $ proveGoalsOnline sym cruxOpts' ctx (\_ _ -> return mempty) todo let provedAll = totalProcessedGoals processed == provedGoals processed when provedAll $ liftIO $ clearProofObligations sym From 522541ed7aa176fe0771efdc3d6b6a76db47618d Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 7 Jun 2021 08:05:59 -0700 Subject: [PATCH 06/18] Pass known cruxOpts to output config in crux tests. --- crux-mir/test/Test.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/crux-mir/test/Test.hs b/crux-mir/test/Test.hs index e7a8ff81e..797e6e0c3 100644 --- a/crux-mir/test/Test.hs +++ b/crux-mir/test/Test.hs @@ -88,7 +88,8 @@ runCrux rustFile outHandle mode = do _ -> "", Crux.branchCoverage = (mode == RcmCoverage) } , Mir.defaultMirOptions { Mir.printResultOnly = (mode == RcmConcrete) }) - let ?outputConfig = Crux.mkOutputConfig False outHandle outHandle Nothing + let ?outputConfig = Crux.mkOutputConfig False outHandle outHandle $ + Just (fst options) _exitCode <- Mir.runTests options return () From 5f583e160e9dedfec1c5a01fe82b005ce4360145 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 7 Jun 2021 08:15:16 -0700 Subject: [PATCH 07/18] Add more description to mkOutputConfig describing effects of Nothing for CruxOptions --- crux/src/Crux.hs | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/crux/src/Crux.hs b/crux/src/Crux.hs index 3be6bccb2..fca986510 100644 --- a/crux/src/Crux.hs +++ b/crux/src/Crux.hs @@ -192,11 +192,18 @@ showVersion nm ver = -- | Create an OutputConfig for Crux, based on an indication of -- whether colored output should be used, the normal and error output --- handles, and the parsed CruxOptions. The following CruxOptions --- affect the generated OutputConfig: +-- handles, and the parsed CruxOptions. -- --- printFailures --- quietMode +-- If no CruxOptions are available (i.e. Nothing, as used in the +-- preliminary portions of loadOptions), then a default output stance +-- is applied; the default stance is described along with the +-- individual option below. +-- +-- The following CruxOptions affect the generated OutputConfig: +-- +-- * printFailures (default stance: True) +-- * quietMode (default stance: False) +-- * simVerbose (default stance: False) mkOutputConfig :: Bool -> Handle -> Handle -> Maybe CruxOptions -> OutputConfig mkOutputConfig withColors outHandle errHandle opts = From fc7ea7aa9e7f53d76591883911ddb52db319d32b Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 7 Jun 2021 08:56:55 -0700 Subject: [PATCH 08/18] Update ormolu action version to try to fix CI --- .github/workflows/uc-crux-llvm-lint.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/uc-crux-llvm-lint.yaml b/.github/workflows/uc-crux-llvm-lint.yaml index f5af15fbc..88a15fd65 100644 --- a/.github/workflows/uc-crux-llvm-lint.yaml +++ b/.github/workflows/uc-crux-llvm-lint.yaml @@ -22,7 +22,7 @@ jobs: tar xvf hlint.tar.gz ./hlint-3.3/hlint exe src test - - uses: mrkkrp/ormolu-action@v1 + - uses: mrkkrp/ormolu-action@v2 with: pattern: | uc-crux-llvm/exe/**/*.hs From 832aef2b25df6bcd6af4c2cf45ce72ca619a4882 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 7 Jun 2021 09:05:18 -0700 Subject: [PATCH 09/18] Disable linting check that seems to have linter implementation issues at present. --- .github/workflows/uc-crux-llvm-lint.yaml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/uc-crux-llvm-lint.yaml b/.github/workflows/uc-crux-llvm-lint.yaml index 88a15fd65..bfeb9890f 100644 --- a/.github/workflows/uc-crux-llvm-lint.yaml +++ b/.github/workflows/uc-crux-llvm-lint.yaml @@ -23,6 +23,10 @@ jobs: ./hlint-3.3/hlint exe src test - uses: mrkkrp/ormolu-action@v2 + # This is currently disabled, since it complains about + # problems in uc-crux-llvm (without many details) that + # GHC says don't exist. 2021 June 07 + if: false with: pattern: | uc-crux-llvm/exe/**/*.hs From 946e1a7128fab56c219fad23c380076f6921dd5b Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 7 Jun 2021 11:57:26 -0700 Subject: [PATCH 10/18] Use standard evaluation of quiet mode configuration or default. --- crux/src/Crux.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/crux/src/Crux.hs b/crux/src/Crux.hs index fca986510..81f22520a 100644 --- a/crux/src/Crux.hs +++ b/crux/src/Crux.hs @@ -212,9 +212,10 @@ mkOutputConfig withColors outHandle errHandle opts = baseline = if maybe False ((> 1) . simVerbose) opts then Noisily else Simply - in if maybe False quietMode opts + in if beQuiet then logfltr OK >$< la else logfltr baseline >$< la + beQuiet = maybe False quietMode opts logfltr allowed = \case SayNothing -> SayNothing w@(SayWhat lvl _ _) -> if lvl >= allowed then w else SayNothing @@ -229,7 +230,7 @@ mkOutputConfig withColors outHandle errHandle opts = in OutputConfig { _outputHandle = outHandle - , _quiet = maybe True quietMode opts + , _quiet = beQuiet , _logWhat = lgWhat , _logExc = let seeRed = AC.hSetSGR errHandle [ AC.SetConsoleIntensity AC.BoldIntensity From a2faaa0a036c6b42561ad75edc9d28e2baa4fa5e Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 7 Jun 2021 11:58:10 -0700 Subject: [PATCH 11/18] Fix syntax error in uc-crux-llvm test. --- uc-crux-llvm/test/Test.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/uc-crux-llvm/test/Test.hs b/uc-crux-llvm/test/Test.hs index 812589678..ed89ad032 100644 --- a/uc-crux-llvm/test/Test.hs +++ b/uc-crux-llvm/test/Test.hs @@ -144,9 +144,9 @@ findBugs llvmModule file fns = Crux.say Crux.Fail "UC-Crux-LLVM" "Trouble when running Clang:" Crux.logException exc error "aborting" - if isRealFile - then try (genBitCode cruxOpts'' uclopts) >>= either complain return - else return "" + in if isRealFile + then try (genBitCode cruxOpts'' uclopts) >>= either complain return + else return "" -- TODO(lb): It would be nice to print this only when the test fails -- putStrLn From 02a83351d1c4eb5dc4662f42fa995ee9913055f3 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 7 Jun 2021 13:51:33 -0700 Subject: [PATCH 12/18] Fix misspelling of attempted in crux-mir counterexample failure messages. --- crux-mir/src/Mir/FancyMuxTree.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crux-mir/src/Mir/FancyMuxTree.hs b/crux-mir/src/Mir/FancyMuxTree.hs index faf3a530a..cc95dcdbb 100644 --- a/crux-mir/src/Mir/FancyMuxTree.hs +++ b/crux-mir/src/Mir/FancyMuxTree.hs @@ -355,7 +355,7 @@ readFancyMuxTree' :: (IsExprBuilder sym, IsBoolSolver sym, MonadIO m) => readFancyMuxTree' sym f mux t = readFancyMuxTree sym f mux t >>= \my -> case my of Just y -> return y Nothing -> liftIO $ addFailedAssertion sym $ GenericSimError $ - "attemted to read empty mux tree" + "attempted to read empty mux tree" readPartialFancyMuxTree :: (IsExprBuilder sym, IsBoolSolver sym, MonadIO m) => sym -> @@ -391,7 +391,7 @@ zipFancyMuxTrees' :: (IsExprBuilder sym, IsBoolSolver sym, MonadIO m) => zipFancyMuxTrees' sym f mux tx ty = zipFancyMuxTrees sym f mux tx ty >>= \my -> case my of Just y -> return y Nothing -> liftIO $ addFailedAssertion sym $ GenericSimError $ - "attemted to read empty mux tree" + "attempted to read empty mux tree" mergeFancyMuxTree :: (IsExprBuilder sym, OrdSkel a, MonadIO m) => sym -> (Pred sym -> a -> a -> m a) -> From 81562fc907b53a779d0c8c6ea8f963f7c9c2ba56 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Mon, 7 Jun 2021 15:11:21 -0700 Subject: [PATCH 13/18] Added delineator before final results output from crux-mir. --- crux-mir/src/Mir/Language.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/crux-mir/src/Mir/Language.hs b/crux-mir/src/Mir/Language.hs index 74f63ab62..7525bb513 100644 --- a/crux-mir/src/Mir/Language.hs +++ b/crux-mir/src/Mir/Language.hs @@ -389,6 +389,7 @@ runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do let skipSummary = printResultOnly mirOpts && resComp == ProgramComplete && Seq.null resGoals if not skipSummary then do outputLn "" + say Simply "Crux-MIR" "---- FINAL RESULTS ----" Crux.postprocessSimResult cruxOpts res else return ExitSuccess From c9d915e7595a16639afbe4e74a33f4ef1ad8b73e Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Wed, 9 Jun 2021 21:48:53 -0700 Subject: [PATCH 14/18] logSimResult takes a flag to request display of failed goals; removes crux-mir output duplication. --- crucible-wasm/tool/Main.hs | 2 +- crux-llvm/src/CruxLLVMMain.hs | 2 +- crux-mir/src/Mir/Language.hs | 2 +- crux/src/Crux.hs | 15 +++++++++------ crux/src/Crux/Log.hs | 11 +++++++---- 5 files changed, 19 insertions(+), 13 deletions(-) diff --git a/crucible-wasm/tool/Main.hs b/crucible-wasm/tool/Main.hs index c2dcc6f0a..274feea07 100644 --- a/crucible-wasm/tool/Main.hs +++ b/crucible-wasm/tool/Main.hs @@ -69,4 +69,4 @@ main = Crux.loadOptions Crux.defaultOutputConfig "crux-wasm" version cruxWasmConfig \(cruxOpts, wasmOpts) -> do res <- Crux.runSimulator cruxOpts (simulateWasm cruxOpts wasmOpts) - exitWith =<< Crux.postprocessSimResult cruxOpts res + exitWith =<< Crux.postprocessSimResult True cruxOpts res diff --git a/crux-llvm/src/CruxLLVMMain.hs b/crux-llvm/src/CruxLLVMMain.hs index eb297bf39..c855593ea 100644 --- a/crux-llvm/src/CruxLLVMMain.hs +++ b/crux-llvm/src/CruxLLVMMain.hs @@ -34,7 +34,7 @@ mainWithOutputConfig mkOutCfg = do bcFile <- genBitCode cruxOpts llvmOpts res <- Crux.runSimulator cruxOpts (simulateLLVMFile bcFile llvmOpts) makeCounterExamplesLLVM cruxOpts llvmOpts res - Crux.postprocessSimResult cruxOpts res + Crux.postprocessSimResult True cruxOpts res processLLVMOptions :: (CruxOptions,LLVMOptions) -> IO (CruxOptions,LLVMOptions) processLLVMOptions (cruxOpts,llvmOpts) = diff --git a/crux-mir/src/Mir/Language.hs b/crux-mir/src/Mir/Language.hs index 7525bb513..73f190ea4 100644 --- a/crux-mir/src/Mir/Language.hs +++ b/crux-mir/src/Mir/Language.hs @@ -390,7 +390,7 @@ runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do if not skipSummary then do outputLn "" say Simply "Crux-MIR" "---- FINAL RESULTS ----" - Crux.postprocessSimResult cruxOpts res + Crux.postprocessSimResult False cruxOpts res else return ExitSuccess diff --git a/crux/src/Crux.hs b/crux/src/Crux.hs index 81f22520a..8012d8a02 100644 --- a/crux/src/Crux.hs +++ b/crux/src/Crux.hs @@ -128,10 +128,10 @@ newtype SimulatorCallback -- | Given the result of a simulation and proof run, report the overall -- status, generate user-consumable reports and compute the exit code. -postprocessSimResult :: Logs => CruxOptions -> CruxSimulationResult -> IO ExitCode -postprocessSimResult opts res = +postprocessSimResult :: Logs => Bool -> CruxOptions -> CruxSimulationResult -> IO ExitCode +postprocessSimResult showFailedGoals opts res = do -- print goals that failed and overall result - logSimResult res + logSimResult showFailedGoals res -- Generate report generateReport opts res @@ -240,9 +240,12 @@ mkOutputConfig withColors outHandle errHandle opts = in if withColors then LJ.LogAction $ \e -> Ex.bracket_ seeRed seeCalm $ dispExc e else LJ.LogAction $ dispExc - , _logSimResult = divide splitResults - lgGoal - (sayWhatResultStatus >$< lgWhat) + , _logSimResult = \showDetails -> + if showDetails + then divide splitResults + lgGoal + (sayWhatResultStatus >$< lgWhat) + else sayWhatResultStatus >$< lgWhat , _logGoal = Seq.singleton >$< lgGoal } diff --git a/crux/src/Crux/Log.hs b/crux/src/Crux/Log.hs index 3f517d610..bbfa691b6 100644 --- a/crux/src/Crux/Log.hs +++ b/crux/src/Crux/Log.hs @@ -47,9 +47,11 @@ say lvl frm = LJ.writeLog (?outputConfig ^. logWhat) . SayWhat lvl frm logException :: Logs => SomeException -> IO () logException = LJ.writeLog (_logExc ?outputConfig) --- | Function used to output the summary result for a completed simulation -logSimResult :: Logs => CruxSimulationResult -> IO () -logSimResult = LJ.writeLog (_logSimResult ?outputConfig) +-- | Function used to output the summary result for a completed +-- simulation. If the flag is true, show the details of each failed +-- goal before showing the summary. +logSimResult :: Logs => Bool -> CruxSimulationResult -> IO () +logSimResult showFailedGoals = LJ.writeLog (_logSimResult ?outputConfig showFailedGoals) -- | Function used to output any individual goal proof failures from a simulation logGoal :: Logs => ProvedGoals (Either AssumptionReason CSE.SimError) -> IO () @@ -77,7 +79,8 @@ data OutputConfig = , _quiet :: Bool , _logWhat :: LJ.LogAction IO SayWhat , _logExc :: LJ.LogAction IO SomeException - , _logSimResult :: LJ.LogAction IO CruxSimulationResult + , _logSimResult :: Bool -> LJ.LogAction IO CruxSimulationResult + -- ^ True to show individual goals, false for summary only , _logGoal :: LJ.LogAction IO (ProvedGoals (Either AssumptionReason CSE.SimError)) From ac13cce3cbc5da0892252c78912b562af7fe5542 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 11 Jun 2021 08:49:40 -0700 Subject: [PATCH 15/18] Update crucible-jvm for added simulation post processing result argument. --- crucible-jvm/tool/Main.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crucible-jvm/tool/Main.hs b/crucible-jvm/tool/Main.hs index d517258d4..68207dd96 100644 --- a/crucible-jvm/tool/Main.hs +++ b/crucible-jvm/tool/Main.hs @@ -205,5 +205,5 @@ main = Crux.loadOptions Crux.defaultOutputConfig "crux-jvm" version cruxJVMConfig $ \(cruxOpts, jvmOpts) -> do jvmOpts' <- processJVMOptions jvmOpts - exitWith =<< Crux.postprocessSimResult cruxOpts =<< + exitWith =<< Crux.postprocessSimResult True cruxOpts =<< Crux.runSimulator cruxOpts (simulateJVM cruxOpts jvmOpts') From 9c65b019cd4e786aded1b69cab6c3fefe64ba969 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 11 Jun 2021 08:50:17 -0700 Subject: [PATCH 16/18] Revert to always output mode for crux-mir run extra overrides test message --- crux-mir/src/Mir/Language.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crux-mir/src/Mir/Language.hs b/crux-mir/src/Mir/Language.hs index 73f190ea4..921ba7114 100644 --- a/crux-mir/src/Mir/Language.hs +++ b/crux-mir/src/Mir/Language.hs @@ -268,7 +268,7 @@ runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do -- is enabled. when (not (concurrency mirOpts) && printResultOnly mirOpts) $ do str <- showRegEntry @sym col resTy res - liftIO $ say Simply "Crux-MIR" $ Text.pack str + liftIO $ outputLn str when (not (concurrency mirOpts) && not (printResultOnly mirOpts) && resTy /= TyTuple []) $ do str <- showRegEntry @sym col resTy res From 0dc58bbcf15380f799e0a95cad23a12184cd473b Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 11 Jun 2021 09:39:05 -0700 Subject: [PATCH 17/18] Update crux-mir output difference message for proper filename mention. --- crux-mir/test/Test.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crux-mir/test/Test.hs b/crux-mir/test/Test.hs index 797e6e0c3..76138c4f9 100644 --- a/crux-mir/test/Test.hs +++ b/crux-mir/test/Test.hs @@ -167,7 +167,7 @@ doGoldenTest rustFile goodFile outFile act = goldenTest (takeBaseName rustFile) (act >> BS.readFile outFile) (\good out -> return $ if good == out then Nothing else Just $ "files " ++ goodFile ++ " and " ++ outFile ++ " differ; " ++ - goodFile ++ " contains:\n" ++ BS8.toString out) + outFile ++ " contains:\n" ++ BS8.toString out) (\out -> BS.writeFile goodFile out) main :: IO () From ebe3481f0f7d5b5b1e7274eff4150dc3b75362b4 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 11 Jun 2021 09:39:27 -0700 Subject: [PATCH 18/18] Update crux-mir golden test results. --- .../test/symb_eval/alloc/out_of_bounds.good | 10 +++--- .../test/symb_eval/alloc/uninit_read.good | 10 +++--- .../test/symb_eval/any/downcast_fail.good | 5 +-- .../test/symb_eval/bytes/put_overflow.good | 5 +-- .../test/symb_eval/concretize/assert.good | 12 ++++--- crux-mir/test/symb_eval/crux/early_fail.good | 12 ++++--- crux-mir/test/symb_eval/crux/fail_return.good | 24 +++++++------ crux-mir/test/symb_eval/crux/mixed_fail.good | 24 +++++++------ crux-mir/test/symb_eval/crux/multi.good | 24 +++++++------ crux-mir/test/symb_eval/crypto/bytes.good | 35 +++++++++++-------- crux-mir/test/symb_eval/num/checked_add.good | 5 +-- crux-mir/test/symb_eval/num/checked_div.good | 15 ++++---- crux-mir/test/symb_eval/num/checked_mul.good | 5 +-- .../symb_eval/num/checked_mul_signed.good | 5 +-- .../test/symb_eval/overrides/bad_symb1.good | 5 +-- .../test/symb_eval/overrides/bad_symb2.good | 5 +-- .../test/symb_eval/overrides/override2.good | 7 ++-- .../test/symb_eval/overrides/override5.good | 7 ++-- .../test/symb_eval/sym_bytes/construct.good | 7 ++-- .../test/symb_eval/sym_bytes/deserialize.good | 5 +-- 20 files changed, 133 insertions(+), 94 deletions(-) diff --git a/crux-mir/test/symb_eval/alloc/out_of_bounds.good b/crux-mir/test/symb_eval/alloc/out_of_bounds.good index 9b647b3d4..689cb4e08 100644 --- a/crux-mir/test/symb_eval/alloc/out_of_bounds.good +++ b/crux-mir/test/symb_eval/alloc/out_of_bounds.good @@ -3,9 +3,11 @@ test out_of_bounds/3a1fbbbh::crux_test[0]: FAILED failures: ---- out_of_bounds/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for test/symb_eval/alloc/out_of_bounds.rs:12:9: 12:24: error: in out_of_bounds/3a1fbbbh::crux_test[0] -vector index out of range: the length is 10 but the index is BV 12 -Failure for test/symb_eval/alloc/out_of_bounds.rs:12:9: 12:24: error: in out_of_bounds/3a1fbbbh::crux_test[0] -attemted to read empty mux tree +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/alloc/out_of_bounds.rs:12:9: 12:24: error: in out_of_bounds/3a1fbbbh::crux_test[0] +[Crux] vector index out of range: the length is 10 but the index is BV 12 +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/alloc/out_of_bounds.rs:12:9: 12:24: error: in out_of_bounds/3a1fbbbh::crux_test[0] +[Crux] attempted to read empty mux tree [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/alloc/uninit_read.good b/crux-mir/test/symb_eval/alloc/uninit_read.good index b4768b6b7..b184913f6 100644 --- a/crux-mir/test/symb_eval/alloc/uninit_read.good +++ b/crux-mir/test/symb_eval/alloc/uninit_read.good @@ -3,9 +3,11 @@ test uninit_read/3a1fbbbh::crux_test[0]: FAILED failures: ---- uninit_read/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for test/symb_eval/alloc/uninit_read.rs:9:9: 9:23: error: in uninit_read/3a1fbbbh::crux_test[0] -Attempted to read uninitialized vector index -Failure for test/symb_eval/alloc/uninit_read.rs:9:9: 9:23: error: in uninit_read/3a1fbbbh::crux_test[0] -attemted to read empty mux tree +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/alloc/uninit_read.rs:9:9: 9:23: error: in uninit_read/3a1fbbbh::crux_test[0] +[Crux] Attempted to read uninitialized vector index +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/alloc/uninit_read.rs:9:9: 9:23: error: in uninit_read/3a1fbbbh::crux_test[0] +[Crux] attempted to read empty mux tree [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/any/downcast_fail.good b/crux-mir/test/symb_eval/any/downcast_fail.good index 81ef56691..342800fae 100644 --- a/crux-mir/test/symb_eval/any/downcast_fail.good +++ b/crux-mir/test/symb_eval/any/downcast_fail.good @@ -3,7 +3,8 @@ test downcast_fail/3a1fbbbh::crux_test[0]: FAILED failures: ---- downcast_fail/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for test/symb_eval/any/downcast_fail.rs:10:14: 10:15: error: in downcast_fail/3a1fbbbh::crux_test[0] -failed to downcast Any as BVRepr 32 +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/any/downcast_fail.rs:10:14: 10:15: error: in downcast_fail/3a1fbbbh::crux_test[0] +[Crux] failed to downcast Any as BVRepr 32 [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/bytes/put_overflow.good b/crux-mir/test/symb_eval/bytes/put_overflow.good index 8e728d1ed..93b3a0633 100644 --- a/crux-mir/test/symb_eval/bytes/put_overflow.good +++ b/crux-mir/test/symb_eval/bytes/put_overflow.good @@ -3,7 +3,8 @@ test put_overflow/3a1fbbbh::f[0]: FAILED failures: ---- put_overflow/3a1fbbbh::f[0] counterexamples ---- -Failure for internal: error: in bytes/3a1fbbbh::{{impl}}[4]::put_slice[0] -panicking::begin_panic, called from bytes/3a1fbbbh::{{impl}}[4]::put_slice[0] +[Crux] Found counterexample for verification goal +[Crux] internal: error: in bytes/3a1fbbbh::{{impl}}[4]::put_slice[0] +[Crux] panicking::begin_panic, called from bytes/3a1fbbbh::{{impl}}[4]::put_slice[0] [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/concretize/assert.good b/crux-mir/test/symb_eval/concretize/assert.good index 90708d9a8..61d2c731a 100644 --- a/crux-mir/test/symb_eval/concretize/assert.good +++ b/crux-mir/test/symb_eval/concretize/assert.good @@ -3,10 +3,12 @@ test assert/3a1fbbbh::crux_test[0]: returned 1, FAILED failures: ---- assert/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:46:17: 46:82 !test/symb_eval/concretize/assert.rs:10:5: 10:82: error: in assert/3a1fbbbh::crux_test[0] -MIR assertion at test/symb_eval/concretize/assert.rs:10:5: - 100 + 157 == 1 -Failure for test/symb_eval/concretize/assert.rs:11:16: 11:17: error: in assert/3a1fbbbh::crux_test[0] -Unsupported feature: Attempted to mux ANY values of different runtime type StructRepr [BVRepr 8] IntrinsicRepr MirReference [BVRepr 8] +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:46:17: 46:82 !test/symb_eval/concretize/assert.rs:10:5: 10:82: error: in assert/3a1fbbbh::crux_test[0] +[Crux] MIR assertion at test/symb_eval/concretize/assert.rs:10:5: +[Crux] 100 + 157 == 1 +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/concretize/assert.rs:11:16: 11:17: error: in assert/3a1fbbbh::crux_test[0] +[Crux] Unsupported feature: Attempted to mux ANY values of different runtime type StructRepr [BVRepr 8] IntrinsicRepr MirReference [BVRepr 8] [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/crux/early_fail.good b/crux-mir/test/symb_eval/crux/early_fail.good index fc02ecf71..587dba9f7 100644 --- a/crux-mir/test/symb_eval/crux/early_fail.good +++ b/crux-mir/test/symb_eval/crux/early_fail.good @@ -4,12 +4,14 @@ test early_fail/3a1fbbbh::fail2[0]: FAILED failures: ---- early_fail/3a1fbbbh::fail1[0] counterexamples ---- -Failure for internal: error: in early_fail/3a1fbbbh::fail1[0] -panicking::begin_panic, called from early_fail/3a1fbbbh::fail1[0] +[Crux] Found counterexample for verification goal +[Crux] internal: error: in early_fail/3a1fbbbh::fail1[0] +[Crux] panicking::begin_panic, called from early_fail/3a1fbbbh::fail1[0] ---- early_fail/3a1fbbbh::fail2[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/early_fail.rs:17:5: 17:30: error: in early_fail/3a1fbbbh::fail2[0] -MIR assertion at test/symb_eval/crux/early_fail.rs:17:5: - x == 0 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/early_fail.rs:17:5: 17:30: error: in early_fail/3a1fbbbh::fail2[0] +[Crux] MIR assertion at test/symb_eval/crux/early_fail.rs:17:5: +[Crux] x == 0 [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/crux/fail_return.good b/crux-mir/test/symb_eval/crux/fail_return.good index 7a7336bce..221e6cf97 100644 --- a/crux-mir/test/symb_eval/crux/fail_return.good +++ b/crux-mir/test/symb_eval/crux/fail_return.good @@ -4,17 +4,21 @@ test fail_return/3a1fbbbh::fail2[0]: returned 123, FAILED failures: ---- fail_return/3a1fbbbh::fail1[0] counterexamples ---- -Failure for test/symb_eval/crux/fail_return.rs:8:22: 8:27: error: in fail_return/3a1fbbbh::fail1[0] -attempt to add with overflow -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/fail_return.rs:8:5: 8:33: error: in fail_return/3a1fbbbh::fail1[0] -MIR assertion at test/symb_eval/crux/fail_return.rs:8:5: - x + 1 > x +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/crux/fail_return.rs:8:22: 8:27: error: in fail_return/3a1fbbbh::fail1[0] +[Crux] attempt to add with overflow +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/fail_return.rs:8:5: 8:33: error: in fail_return/3a1fbbbh::fail1[0] +[Crux] MIR assertion at test/symb_eval/crux/fail_return.rs:8:5: +[Crux] x + 1 > x ---- fail_return/3a1fbbbh::fail2[0] counterexamples ---- -Failure for test/symb_eval/crux/fail_return.rs:15:22: 15:27: error: in fail_return/3a1fbbbh::fail2[0] -attempt to add with overflow -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/fail_return.rs:15:5: 15:33: error: in fail_return/3a1fbbbh::fail2[0] -MIR assertion at test/symb_eval/crux/fail_return.rs:15:5: - x + 1 > x +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/crux/fail_return.rs:15:22: 15:27: error: in fail_return/3a1fbbbh::fail2[0] +[Crux] attempt to add with overflow +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/fail_return.rs:15:5: 15:33: error: in fail_return/3a1fbbbh::fail2[0] +[Crux] MIR assertion at test/symb_eval/crux/fail_return.rs:15:5: +[Crux] x + 1 > x [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/crux/mixed_fail.good b/crux-mir/test/symb_eval/crux/mixed_fail.good index 426c9780d..475d2467d 100644 --- a/crux-mir/test/symb_eval/crux/mixed_fail.good +++ b/crux-mir/test/symb_eval/crux/mixed_fail.good @@ -6,17 +6,21 @@ test mixed_fail/3a1fbbbh::pass2[0]: ok failures: ---- mixed_fail/3a1fbbbh::fail1[0] counterexamples ---- -Failure for test/symb_eval/crux/mixed_fail.rs:8:22: 8:27: error: in mixed_fail/3a1fbbbh::fail1[0] -attempt to add with overflow -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/mixed_fail.rs:8:5: 8:33: error: in mixed_fail/3a1fbbbh::fail1[0] -MIR assertion at test/symb_eval/crux/mixed_fail.rs:8:5: - x + 1 > x +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/crux/mixed_fail.rs:8:22: 8:27: error: in mixed_fail/3a1fbbbh::fail1[0] +[Crux] attempt to add with overflow +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/mixed_fail.rs:8:5: 8:33: error: in mixed_fail/3a1fbbbh::fail1[0] +[Crux] MIR assertion at test/symb_eval/crux/mixed_fail.rs:8:5: +[Crux] x + 1 > x ---- mixed_fail/3a1fbbbh::fail2[0] counterexamples ---- -Failure for test/symb_eval/crux/mixed_fail.rs:14:22: 14:27: error: in mixed_fail/3a1fbbbh::fail2[0] -attempt to add with overflow -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/mixed_fail.rs:14:5: 14:33: error: in mixed_fail/3a1fbbbh::fail2[0] -MIR assertion at test/symb_eval/crux/mixed_fail.rs:14:5: - x + 2 > x +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/crux/mixed_fail.rs:14:22: 14:27: error: in mixed_fail/3a1fbbbh::fail2[0] +[Crux] attempt to add with overflow +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/mixed_fail.rs:14:5: 14:33: error: in mixed_fail/3a1fbbbh::fail2[0] +[Crux] MIR assertion at test/symb_eval/crux/mixed_fail.rs:14:5: +[Crux] x + 2 > x [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/crux/multi.good b/crux-mir/test/symb_eval/crux/multi.good index 9eee3ce47..13ef40568 100644 --- a/crux-mir/test/symb_eval/crux/multi.good +++ b/crux-mir/test/symb_eval/crux/multi.good @@ -5,19 +5,23 @@ test multi/3a1fbbbh::fail3[0]: FAILED failures: ---- multi/3a1fbbbh::fail1[0] counterexamples ---- -Failure for test/symb_eval/crux/multi.rs:8:22: 8:27: error: in multi/3a1fbbbh::fail1[0] -attempt to add with overflow -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/multi.rs:8:5: 8:33: error: in multi/3a1fbbbh::fail1[0] -MIR assertion at test/symb_eval/crux/multi.rs:8:5: - x + 1 > x +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/crux/multi.rs:8:22: 8:27: error: in multi/3a1fbbbh::fail1[0] +[Crux] attempt to add with overflow +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/multi.rs:8:5: 8:33: error: in multi/3a1fbbbh::fail1[0] +[Crux] MIR assertion at test/symb_eval/crux/multi.rs:8:5: +[Crux] x + 1 > x ---- multi/3a1fbbbh::fail2[0] counterexamples ---- -Failure for internal: error: in multi/3a1fbbbh::fail2[0] -panicking::begin_panic, called from multi/3a1fbbbh::fail2[0] +[Crux] Found counterexample for verification goal +[Crux] internal: error: in multi/3a1fbbbh::fail2[0] +[Crux] panicking::begin_panic, called from multi/3a1fbbbh::fail2[0] ---- multi/3a1fbbbh::fail3[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/multi.rs:20:5: 20:30: error: in multi/3a1fbbbh::assert_zero[0] -MIR assertion at test/symb_eval/crux/multi.rs:20:5: - x == 0 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/multi.rs:20:5: 20:30: error: in multi/3a1fbbbh::assert_zero[0] +[Crux] MIR assertion at test/symb_eval/crux/multi.rs:20:5: +[Crux] x == 0 [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/crypto/bytes.good b/crux-mir/test/symb_eval/crypto/bytes.good index 910370bf1..a799a428c 100644 --- a/crux-mir/test/symb_eval/crypto/bytes.good +++ b/crux-mir/test/symb_eval/crypto/bytes.good @@ -3,20 +3,25 @@ test bytes/3a1fbbbh::f[0]: FAILED failures: ---- bytes/3a1fbbbh::f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0] -MIR assertion at test/symb_eval/crypto/bytes.rs:85:7: - a[i] == b[i] -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0] -MIR assertion at test/symb_eval/crypto/bytes.rs:85:7: - a[i] == b[i] -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0] -MIR assertion at test/symb_eval/crypto/bytes.rs:85:7: - a[i] == b[i] -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0] -MIR assertion at test/symb_eval/crypto/bytes.rs:85:7: - a[i] == b[i] -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0] -MIR assertion at test/symb_eval/crypto/bytes.rs:85:7: - a[i] == b[i] +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0] +[Crux] MIR assertion at test/symb_eval/crypto/bytes.rs:85:7: +[Crux] a[i] == b[i] +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0] +[Crux] MIR assertion at test/symb_eval/crypto/bytes.rs:85:7: +[Crux] a[i] == b[i] +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0] +[Crux] MIR assertion at test/symb_eval/crypto/bytes.rs:85:7: +[Crux] a[i] == b[i] +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0] +[Crux] MIR assertion at test/symb_eval/crypto/bytes.rs:85:7: +[Crux] a[i] == b[i] +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0] +[Crux] MIR assertion at test/symb_eval/crypto/bytes.rs:85:7: +[Crux] a[i] == b[i] [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/num/checked_add.good b/crux-mir/test/symb_eval/num/checked_add.good index ccf17ddcd..6c0c35192 100644 --- a/crux-mir/test/symb_eval/num/checked_add.good +++ b/crux-mir/test/symb_eval/num/checked_add.good @@ -3,7 +3,8 @@ test checked_add/3a1fbbbh::crux_test[0]: returned 44, FAILED failures: ---- checked_add/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for test/symb_eval/num/checked_add.rs:5:5: 5:12: error: in checked_add/3a1fbbbh::crux_test[0] -attempt to add with overflow +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/num/checked_add.rs:5:5: 5:12: error: in checked_add/3a1fbbbh::crux_test[0] +[Crux] attempt to add with overflow [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/num/checked_div.good b/crux-mir/test/symb_eval/num/checked_div.good index d151923c2..04b9ed52c 100644 --- a/crux-mir/test/symb_eval/num/checked_div.good +++ b/crux-mir/test/symb_eval/num/checked_div.good @@ -3,11 +3,14 @@ test checked_div/3a1fbbbh::crux_test[0]: returned 65, FAILED failures: ---- checked_div/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for test/symb_eval/num/checked_div.rs:3:5: 3:10: error: in checked_div/3a1fbbbh::div_signed[0] -attempt to divide with overflow -Failure for test/symb_eval/num/checked_div.rs:3:5: 3:10: error: in checked_div/3a1fbbbh::div_signed[0] -attempt to divide by zero -Failure for test/symb_eval/num/checked_div.rs:8:5: 8:10: error: in checked_div/3a1fbbbh::div_unsigned[0] -attempt to divide by zero +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/num/checked_div.rs:3:5: 3:10: error: in checked_div/3a1fbbbh::div_signed[0] +[Crux] attempt to divide with overflow +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/num/checked_div.rs:3:5: 3:10: error: in checked_div/3a1fbbbh::div_signed[0] +[Crux] attempt to divide by zero +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/num/checked_div.rs:8:5: 8:10: error: in checked_div/3a1fbbbh::div_unsigned[0] +[Crux] attempt to divide by zero [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/num/checked_mul.good b/crux-mir/test/symb_eval/num/checked_mul.good index 8bf03b5d8..66144abe8 100644 --- a/crux-mir/test/symb_eval/num/checked_mul.good +++ b/crux-mir/test/symb_eval/num/checked_mul.good @@ -3,7 +3,8 @@ test checked_mul/3a1fbbbh::crux_test[0]: returned 44, FAILED failures: ---- checked_mul/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for test/symb_eval/num/checked_mul.rs:4:5: 4:12: error: in checked_mul/3a1fbbbh::crux_test[0] -attempt to multiply with overflow +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/num/checked_mul.rs:4:5: 4:12: error: in checked_mul/3a1fbbbh::crux_test[0] +[Crux] attempt to multiply with overflow [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/num/checked_mul_signed.good b/crux-mir/test/symb_eval/num/checked_mul_signed.good index 8633f424e..dc3587bb6 100644 --- a/crux-mir/test/symb_eval/num/checked_mul_signed.good +++ b/crux-mir/test/symb_eval/num/checked_mul_signed.good @@ -3,7 +3,8 @@ test checked_mul_signed/3a1fbbbh::crux_test[0]: returned 44, FAILED failures: ---- checked_mul_signed/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for test/symb_eval/num/checked_mul_signed.rs:4:5: 4:13: error: in checked_mul_signed/3a1fbbbh::crux_test[0] -attempt to multiply with overflow +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/num/checked_mul_signed.rs:4:5: 4:13: error: in checked_mul_signed/3a1fbbbh::crux_test[0] +[Crux] attempt to multiply with overflow [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/overrides/bad_symb1.good b/crux-mir/test/symb_eval/overrides/bad_symb1.good index 4a8266cf2..961e57159 100644 --- a/crux-mir/test/symb_eval/overrides/bad_symb1.good +++ b/crux-mir/test/symb_eval/overrides/bad_symb1.good @@ -3,7 +3,8 @@ test bad_symb1/3a1fbbbh::crux_test[0]: FAILED failures: ---- bad_symb1/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for lib/crucible/symbolic.rs:24:64: 24:68 !lib/crucible/symbolic.rs:30:1: 36:2: error: in crucible/3a1fbbbh::symbolic[0]::{{impl}}[1]::symbolic[0] -symbolic variable name must be a concrete string +[Crux] Found counterexample for verification goal +[Crux] lib/crucible/symbolic.rs:24:64: 24:68 !lib/crucible/symbolic.rs:30:1: 36:2: error: in crucible/3a1fbbbh::symbolic[0]::{{impl}}[1]::symbolic[0] +[Crux] symbolic variable name must be a concrete string [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/overrides/bad_symb2.good b/crux-mir/test/symb_eval/overrides/bad_symb2.good index 878825ec1..c8af1add3 100644 --- a/crux-mir/test/symb_eval/overrides/bad_symb2.good +++ b/crux-mir/test/symb_eval/overrides/bad_symb2.good @@ -3,7 +3,8 @@ test bad_symb2/3a1fbbbh::crux_test[0]: FAILED failures: ---- bad_symb2/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for lib/crucible/symbolic.rs:24:64: 24:68 !lib/crucible/symbolic.rs:30:1: 36:2: error: in crucible/3a1fbbbh::symbolic[0]::{{impl}}[1]::symbolic[0] -invalid symbolic variable name "\NUL:., /": Identifier must start with a letter. +[Crux] Found counterexample for verification goal +[Crux] lib/crucible/symbolic.rs:24:64: 24:68 !lib/crucible/symbolic.rs:30:1: 36:2: error: in crucible/3a1fbbbh::symbolic[0]::{{impl}}[1]::symbolic[0] +[Crux] invalid symbolic variable name "\NUL:., /": Identifier must start with a letter. [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/overrides/override2.good b/crux-mir/test/symb_eval/overrides/override2.good index ad6905592..e86a759ab 100644 --- a/crux-mir/test/symb_eval/overrides/override2.good +++ b/crux-mir/test/symb_eval/overrides/override2.good @@ -3,8 +3,9 @@ test override2/3a1fbbbh::f[0]: FAILED failures: ---- override2/3a1fbbbh::f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/overrides/override2.rs:9:5: 9:50: error: in override2/3a1fbbbh::f[0] -MIR assertion at test/symb_eval/overrides/override2.rs:9:5: - foo.wrapping_add(1) == foo +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/overrides/override2.rs:9:5: 9:50: error: in override2/3a1fbbbh::f[0] +[Crux] MIR assertion at test/symb_eval/overrides/override2.rs:9:5: +[Crux] foo.wrapping_add(1) == foo [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/overrides/override5.good b/crux-mir/test/symb_eval/overrides/override5.good index 387bcec72..d41d7bf36 100644 --- a/crux-mir/test/symb_eval/overrides/override5.good +++ b/crux-mir/test/symb_eval/overrides/override5.good @@ -3,8 +3,9 @@ test override5/3a1fbbbh::f[0]: FAILED failures: ---- override5/3a1fbbbh::f[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/overrides/override5.rs:10:5: 10:48: error: in override5/3a1fbbbh::f[0] -MIR assertion at test/symb_eval/overrides/override5.rs:10:5: - foo.wrapping_add(1) != 0 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/overrides/override5.rs:10:5: 10:48: error: in override5/3a1fbbbh::f[0] +[Crux] MIR assertion at test/symb_eval/overrides/override5.rs:10:5: +[Crux] foo.wrapping_add(1) != 0 [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/sym_bytes/construct.good b/crux-mir/test/symb_eval/sym_bytes/construct.good index 9fcf0660d..e04654a2d 100644 --- a/crux-mir/test/symb_eval/sym_bytes/construct.good +++ b/crux-mir/test/symb_eval/sym_bytes/construct.good @@ -3,8 +3,9 @@ test construct/3a1fbbbh::crux_test[0]: returned Symbolic BV, FAILED failures: ---- construct/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/sym_bytes/construct.rs:13:5: 13:36: error: in construct/3a1fbbbh::crux_test[0] -MIR assertion at test/symb_eval/sym_bytes/construct.rs:13:5: - sym2[0] == 0 +[Crux] Found counterexample for verification goal +[Crux] ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/sym_bytes/construct.rs:13:5: 13:36: error: in construct/3a1fbbbh::crux_test[0] +[Crux] MIR assertion at test/symb_eval/sym_bytes/construct.rs:13:5: +[Crux] sym2[0] == 0 [Crux] Overall status: Invalid. diff --git a/crux-mir/test/symb_eval/sym_bytes/deserialize.good b/crux-mir/test/symb_eval/sym_bytes/deserialize.good index 805942231..481c7d740 100644 --- a/crux-mir/test/symb_eval/sym_bytes/deserialize.good +++ b/crux-mir/test/symb_eval/sym_bytes/deserialize.good @@ -3,7 +3,8 @@ test deserialize/3a1fbbbh::crux_test[0]: returned Symbolic BV, FAILED failures: ---- deserialize/3a1fbbbh::crux_test[0] counterexamples ---- -Failure for test/symb_eval/sym_bytes/deserialize.rs:19:21: 19:44: error: in deserialize/3a1fbbbh::deserialize[0] -attempt to add with overflow +[Crux] Found counterexample for verification goal +[Crux] test/symb_eval/sym_bytes/deserialize.rs:19:21: 19:44: error: in deserialize/3a1fbbbh::deserialize[0] +[Crux] attempt to add with overflow [Crux] Overall status: Invalid.