diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs index 6e01203e38..e09eba8ac9 100644 --- a/src/SAWScript/Crucible/Common/Override.hs +++ b/src/SAWScript/Crucible/Common/Override.hs @@ -13,6 +13,7 @@ Stability : provisional {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} @@ -52,6 +53,15 @@ module SAWScript.Crucible.Common.Override , failure , getSymInterface , enforceCompleteSubstitution + , refreshTerms + , OverrideWithPreconditions(..) + , owpPreconditions + , owpMethodSpec + , partitionOWPsConcrete + , partitionBySymbolicPreds + , findFalsePreconditions + , unsatPreconditions + , ppConcreteFailure -- , assignmentToList , MetadataMap @@ -59,7 +69,7 @@ module SAWScript.Crucible.Common.Override import qualified Control.Exception as X import Control.Lens -import Control.Monad (unless) +import Control.Monad (foldM, unless) import Control.Monad.Trans.State hiding (get, put) import Control.Monad.State.Class (MonadState(..)) import Control.Monad.Error.Class (MonadError) @@ -68,8 +78,10 @@ import qualified Control.Monad.Fail as Fail import Control.Monad.Trans.Except import Control.Monad.Trans.Class import Control.Monad.IO.Class +import Data.Proxy (Proxy(..)) import qualified Data.Map as Map import Data.Map (Map) +import Data.Maybe (fromMaybe) import Data.Set (Set) import Data.Typeable (Typeable) import Data.Void @@ -81,8 +93,11 @@ import Data.Parameterized.Some (Some) import Data.Parameterized.TraversableFC (toListFC) import Verifier.SAW.SharedTerm as SAWVerifier +import Verifier.SAW.TypedAST as SAWVerifier import Verifier.SAW.TypedTerm as SAWVerifier +import qualified Lang.Crucible.Backend as Crucible +import qualified Lang.Crucible.Backend.Online as Crucible import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr, GlobalVar) import qualified Lang.Crucible.Simulator.GlobalState as Crucible import qualified Lang.Crucible.Simulator.RegMap as Crucible @@ -93,9 +108,10 @@ import qualified What4.LabeledPred as W4 import qualified What4.ProgramLoc as W4 import SAWScript.Exceptions -import SAWScript.Crucible.Common (Sym) +import SAWScript.Crucible.Common (Backend, OnlineSolver, Sym) import SAWScript.Crucible.Common.MethodSpec as MS import SAWScript.Crucible.Common.Setup.Value as MS +import SAWScript.Utils (bullets) -- TODO, not sure this is the best place for this definition type MetadataMap = @@ -397,6 +413,115 @@ enforceCompleteSubstitution loc ss = unless (null missing) (failure loc (AmbiguousVars missing)) +-- | Allocate fresh variables for all of the "fresh" vars +-- used in this phase and add them to the term substitution. +refreshTerms :: + SharedContext {- ^ shared context -} -> + MS.StateSpec ext {- ^ current phase spec -} -> + OverrideMatcher ext w () +refreshTerms sc ss = + do extension <- Map.fromList <$> traverse freshenTerm (view MS.csFreshVars ss) + OM (termSub %= Map.union extension) + where + freshenTerm (TypedExtCns _cty ec) = + do ec' <- liftIO $ scFreshEC sc (toShortName (ecName ec)) (ecType ec) + new <- liftIO $ scExtCns sc ec' + return (ecVarIndex ec, new) + +-- | An override packaged together with its preconditions, labeled with some +-- human-readable info about each condition. +data OverrideWithPreconditions ext = + OverrideWithPreconditions + { _owpPreconditions :: [(MS.ConditionMetadata, LabeledPred Sym)] + -- ^ c.f. '_osAsserts' + , _owpMethodSpec :: MS.CrucibleMethodSpecIR ext + , owpState :: OverrideState ext + } + deriving (Generic) + +makeLenses ''OverrideWithPreconditions + +-- | Partition into three groups: +-- * Preconditions concretely succeed +-- * Preconditions concretely fail +-- * Preconditions are symbolic +partitionOWPsConcrete :: forall ext. + Sym -> + [OverrideWithPreconditions ext] -> + IO ([OverrideWithPreconditions ext], [OverrideWithPreconditions ext], [OverrideWithPreconditions ext]) +partitionOWPsConcrete sym = + let trav = owpPreconditions . each . _2 . W4.labeledPred + in W4.partitionByPredsM (Just sym) $ + foldlMOf trav (W4.andPred sym) (W4.truePred sym) + +-- | Like 'W4.partitionByPreds', but partitions on solver responses, not just +-- concretized values. +partitionBySymbolicPreds :: + (OnlineSolver solver, Foldable t) => + Backend solver {- ^ solver connection -} -> + (a -> W4.Pred Sym) {- ^ how to extract predicates -} -> + t a -> + IO (Map Crucible.BranchResult [a]) +partitionBySymbolicPreds sym getPred = + let step mp a = + Crucible.considerSatisfiability sym Nothing (getPred a) <&> \k -> + Map.insertWith (++) k [a] mp + in foldM step Map.empty + +-- | Find individual preconditions that are symbolically false +-- +-- We should probably be using unsat cores for this. +findFalsePreconditions :: + OnlineSolver solver => + Backend solver -> + OverrideWithPreconditions ext -> + IO [(MS.ConditionMetadata, LabeledPred Sym)] +findFalsePreconditions bak owp = + fromMaybe [] . Map.lookup (Crucible.NoBranch False) <$> + partitionBySymbolicPreds bak (view (_2 . W4.labeledPred)) (owp ^. owpPreconditions) + +-- | Is this group of predicates collectively unsatisfiable? +unsatPreconditions :: + OnlineSolver solver => + Backend solver {- ^ solver connection -} -> + Fold s (W4.Pred Sym) {- ^ how to extract predicates -} -> + s {- ^ a container full of predicates -}-> + IO Bool +unsatPreconditions bak container getPreds = do + let sym = Crucible.backendGetSym bak + conj <- W4.andAllOf sym container getPreds + Crucible.considerSatisfiability bak Nothing conj >>= + \case + Crucible.NoBranch False -> pure True + _ -> pure False + +-- | Print a message about failure of an override's preconditions +ppFailure :: + (PP.Pretty (ExtType ext), PP.Pretty (MethodId ext)) => + OverrideWithPreconditions ext -> + [LabeledPred Sym] -> + PP.Doc ann +ppFailure owp false = + PP.vcat + [ MS.ppMethodSpec (owp ^. owpMethodSpec) + -- TODO: remove viaShow when crucible switches to prettyprinter + , bullets '*' (map (PP.viaShow . Crucible.ppSimError) + (false ^.. traverse . W4.labeledPredMsg)) + ] + +-- | Print a message about concrete failure of an override's preconditions +-- +-- Assumes that the override it's being passed does have concretely failing +-- preconditions. Otherwise, the error won't make much sense. +ppConcreteFailure :: + (PP.Pretty (ExtType ext), PP.Pretty (MethodId ext)) => + OverrideWithPreconditions ext -> + PP.Doc ann +ppConcreteFailure owp = + let (_, false, _) = + W4.partitionLabeledPreds (Proxy :: Proxy Sym) (map snd (owp ^. owpPreconditions)) + in ppFailure owp false + ------------------------------------------------------------------------ -- | Forget the type indexes and length of the arguments. diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 231338987e..258249647c 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -369,21 +369,6 @@ executeCond opts sc cc cs ss = traverse_ (executeSetupCondition opts sc cc cs) (ss ^. MS.csConditions) --- | Allocate fresh variables for all of the "fresh" vars --- used in this phase and add them to the term substitution. -refreshTerms :: - SharedContext {- ^ shared context -} -> - StateSpec {- ^ current phase spec -} -> - OverrideMatcher CJ.JVM w () -refreshTerms sc ss = - do extension <- Map.fromList <$> traverse freshenTerm (view MS.csFreshVars ss) - OM (termSub %= Map.union extension) - where - freshenTerm (TypedExtCns _cty ec) = - do ec' <- liftIO $ scFreshEC sc (toShortName (ecName ec)) (ecType ec) - new <- liftIO $ scExtCns sc ec' - return (ecVarIndex ec, new) - ------------------------------------------------------------------------ -- | Generate assertions that all of the memory allocations matched by diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 695cb50b44..f28768f11b 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -63,7 +63,6 @@ import Control.Lens.Fold import Control.Lens.Getter import Control.Lens.Lens import Control.Lens.Setter -import Control.Lens.TH import Control.Exception as X import Control.Monad (filterM, foldM, forM, forM_, when, zipWithM) import Control.Monad.Except (runExcept) @@ -76,13 +75,11 @@ import Data.IORef (IORef, modifyIORef) import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe -import Data.Proxy import Data.Set (Set) import qualified Data.Set as Set import Data.Text (Text, pack) import qualified Data.Vector as V import Data.Void (absurd) -import GHC.Generics (Generic) import Numeric.Natural import qualified Prettyprinter as PP @@ -93,7 +90,6 @@ import qualified Cryptol.Eval.Type as Cryptol (TValue(..), evalType) import qualified Cryptol.Utils.PP as Cryptol (pp) import qualified Lang.Crucible.Backend as Crucible -import qualified Lang.Crucible.Backend.Online as Crucible import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr(UnitRepr)) import qualified Lang.Crucible.FunctionHandle as Crucible import qualified Lang.Crucible.LLVM.Bytes as Crucible @@ -141,20 +137,7 @@ import SAWScript.Options import SAWScript.Panic import SAWScript.Utils (bullets, handleException) -type LabeledPred sym = W4.LabeledPred (W4.Pred sym) Crucible.SimError - --- | An override packaged together with its preconditions, labeled with some --- human-readable info about each condition. -data OverrideWithPreconditions arch = - OverrideWithPreconditions - { _owpPreconditions :: [(MS.ConditionMetadata, LabeledPred Sym)] - -- ^ c.f. '_osAsserts' - , _owpMethodSpec :: MS.CrucibleMethodSpecIR (LLVM arch) - , owpState :: OverrideState (LLVM arch) - } - deriving (Generic) - -makeLenses ''OverrideWithPreconditions +type instance Pointer' (LLVM arch) Sym = LLVMPtr (Crucible.ArchWidth arch) ------------------------------------------------------------------------ -- Translating SAW values to Crucible values for good error messages @@ -260,89 +243,12 @@ notEqual cond opts loc cc sc spec expected actual = do ------------------------------------------------------------------------ --- | Partition into three groups: --- * Preconditions concretely succeed --- * Preconditions concretely fail --- * Preconditions are symbolic -partitionOWPsConcrete :: forall arch. - Sym -> - [OverrideWithPreconditions arch] -> - IO ([OverrideWithPreconditions arch], [OverrideWithPreconditions arch], [OverrideWithPreconditions arch]) -partitionOWPsConcrete sym = - let traversal = owpPreconditions . each . _2 . W4.labeledPred - in W4.partitionByPredsM (Just sym) $ - foldlMOf traversal (W4.andPred sym) (W4.truePred sym) - --- | Like 'W4.partitionByPreds', but partitions on solver responses, not just --- concretized values. -partitionBySymbolicPreds :: - (OnlineSolver solver, Foldable t) => - Backend solver {- ^ solver connection -} -> - (a -> W4.Pred Sym) {- ^ how to extract predicates -} -> - t a -> - IO (Map Crucible.BranchResult [a]) -partitionBySymbolicPreds sym getPred = - let step mp a = - Crucible.considerSatisfiability sym Nothing (getPred a) <&> \k -> - Map.insertWith (++) k [a] mp - in foldM step Map.empty - --- | Find individual preconditions that are symbolically false --- --- We should probably be using unsat cores for this. -findFalsePreconditions :: - OnlineSolver solver => - Backend solver -> - OverrideWithPreconditions arch -> - IO [(MS.ConditionMetadata, LabeledPred Sym)] -findFalsePreconditions bak owp = - fromMaybe [] . Map.lookup (Crucible.NoBranch False) <$> - partitionBySymbolicPreds bak (view (_2 . W4.labeledPred)) (owp ^. owpPreconditions) - --- | Is this group of predicates collectively unsatisfiable? -unsatPreconditions :: - OnlineSolver solver => - Backend solver {- ^ solver connection -} -> - Fold s (W4.Pred Sym) {- ^ how to extract predicates -} -> - s {- ^ a container full of predicates -}-> - IO Bool -unsatPreconditions bak container getPreds = do - let sym = backendGetSym bak - conj <- W4.andAllOf sym container getPreds - Crucible.considerSatisfiability bak Nothing conj >>= - \case - Crucible.NoBranch False -> pure True - _ -> pure False - --- | Print a message about failure of an override's preconditions -ppFailure :: - OverrideWithPreconditions arch -> - [LabeledPred Sym] -> - PP.Doc ann -ppFailure owp false = - PP.vcat - [ MS.ppMethodSpec (owp ^. owpMethodSpec) - -- TODO: remove viaShow when crucible switches to prettyprinter - , bullets '*' (map (PP.viaShow . Crucible.ppSimError) - (false ^.. traverse . W4.labeledPredMsg)) - ] - --- | Print a message about concrete failure of an override's preconditions --- --- Assumes that the override it's being passed does have concretely failing --- preconditions. Otherwise, the error won't make much sense. -ppConcreteFailure :: OverrideWithPreconditions arch -> PP.Doc ann -ppConcreteFailure owp = - let (_, false, _) = - W4.partitionLabeledPreds (Proxy :: Proxy Sym) (map snd (owp ^. owpPreconditions)) - in ppFailure owp false - -- | Print a message about symbolic failure of an override's preconditions -- -- TODO: Needs additional testing. Are these messages useful? {- ppSymbolicFailure :: - (OverrideWithPreconditions arch, [LabeledPred Sym]) -> + (OverrideWithPreconditions (LLVM arch), [LabeledPred Sym]) -> PP.Doc ppSymbolicFailure = uncurry ppFailure -} @@ -489,7 +395,7 @@ handleSingleOverrideBranch :: forall arch rtp args ret. W4.ProgramLoc {- ^ Location of the call site for error reporting-} -> IORef MetadataMap -> Crucible.FnHandle args ret {- ^ the handle for this function -} -> - OverrideWithPreconditions arch -> + OverrideWithPreconditions (LLVM arch) -> Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym Crucible.LLVM rtp args ret (Crucible.RegValue Sym ret) handleSingleOverrideBranch opts sc cc call_loc mdMap h (OverrideWithPreconditions preconds cs st) = @@ -548,8 +454,8 @@ handleOverrideBranches :: forall arch rtp args ret. NE.NonEmpty (MS.CrucibleMethodSpecIR (LLVM arch)) {- ^ specification for current function override -} -> Crucible.FnHandle args ret {- ^ the handle for this function -} -> - [OverrideWithPreconditions arch] -> - ([OverrideWithPreconditions arch],[OverrideWithPreconditions arch],[OverrideWithPreconditions arch]) -> + [OverrideWithPreconditions (LLVM arch)] -> + ([OverrideWithPreconditions (LLVM arch)],[OverrideWithPreconditions (LLVM arch)],[OverrideWithPreconditions (LLVM arch)]) -> Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym Crucible.LLVM rtp args ret (Crucible.RegValue Sym ret) @@ -834,21 +740,6 @@ executeCond opts sc cc cs ss = do (ss ^. MS.csPointsTos) traverse_ (executeSetupCondition opts sc cc cs) (ss ^. MS.csConditions) --- | Allocate fresh variables for all of the "fresh" vars --- used in this phase and add them to the term substitution. -refreshTerms :: - SharedContext {- ^ shared context -} -> - MS.StateSpec (LLVM arch) {- ^ current phase spec -} -> - OverrideMatcher (LLVM arch) md () -refreshTerms sc ss = - do extension <- Map.fromList <$> traverse freshenTerm (view MS.csFreshVars ss) - OM (termSub %= Map.union extension) - where - freshenTerm (TypedExtCns _cty ec) = - do ec' <- liftIO $ scFreshEC sc (toShortName (ecName ec)) (ecType ec) - new <- liftIO $ scExtCns sc ec' - return (ecVarIndex ec, new) - ------------------------------------------------------------------------ -- | Generate assertions that all of the memory regions matched by an