Skip to content

Commit

Permalink
Refactor: Move some definitions to SAWScript.Crucible.Common.Override
Browse files Browse the repository at this point in the history 
These previously existed as internal definitions in the LLVM and JVM backends,
but nothing about these definitions are specific any particular backend. In a
subsequent patch, I will make use of these definitions in the MIR backend, so
it is nice to avoid having to duplicate them further.
  • Loading branch information
@RyanGlScott
RyanGlScott committed Nov 22, 2023
1 parent 69f0dc5 commit 256251d
Show file tree
Hide file tree
Showing 3 changed files with 132 additions and 131 deletions.
129 changes: 127 additions & 2 deletions src/SAWScript/Crucible/Common/Override.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Stability : provisional
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
Expand Down Expand Up @@ -52,14 +53,23 @@ module SAWScript.Crucible.Common.Override
, failure
, getSymInterface
, enforceCompleteSubstitution
, refreshTerms
, OverrideWithPreconditions(..)
, owpPreconditions
, owpMethodSpec
, partitionOWPsConcrete
, partitionBySymbolicPreds
, findFalsePreconditions
, unsatPreconditions
, ppConcreteFailure
--
, assignmentToList
, MetadataMap
) where

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)
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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 =
Expand Down Expand Up @@ -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.
Expand Down
15 changes: 0 additions & 15 deletions src/SAWScript/Crucible/JVM/Override.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
119 changes: 5 additions & 114 deletions src/SAWScript/Crucible/LLVM/Override.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
-}
Expand Down Expand Up @@ -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) =
Expand Down Expand Up @@ -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)

Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 256251d

Please sign in to comment.