Skip to content

Commit a697049

Browse files
RyanGlScottRyanGlScott
committed
Refactor: Move some definitions to SAWScript.Crucible.Common.Override
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.
1 parent fd32bd7 commit a697049

File tree

3 files changed

+132
-131
lines changed

3 files changed

+132
-131
lines changed

‎src/SAWScript/Crucible/Common/Override.hs

+127-2
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Stability : provisional
1313
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
1414
{-# LANGUAGE LambdaCase #-}
1515
{-# LANGUAGE MultiParamTypeClasses #-}
16+
{-# LANGUAGE RankNTypes #-}
1617
{-# LANGUAGE StandaloneDeriving #-}
1718
{-# LANGUAGE TemplateHaskell #-}
1819
{-# LANGUAGE TypeFamilies #-}
@@ -52,14 +53,23 @@ module SAWScript.Crucible.Common.Override
5253
, failure
5354
, getSymInterface
5455
, enforceCompleteSubstitution
56+
, refreshTerms
57+
, OverrideWithPreconditions(..)
58+
, owpPreconditions
59+
, owpMethodSpec
60+
, partitionOWPsConcrete
61+
, partitionBySymbolicPreds
62+
, findFalsePreconditions
63+
, unsatPreconditions
64+
, ppConcreteFailure
5565
--
5666
, assignmentToList
5767
, MetadataMap
5868
) where
5969

6070
import qualified Control.Exception as X
6171
import Control.Lens
62-
import Control.Monad (unless)
72+
import Control.Monad (foldM, unless)
6373
import Control.Monad.Trans.State hiding (get, put)
6474
import Control.Monad.State.Class (MonadState(..))
6575
import Control.Monad.Error.Class (MonadError)
@@ -68,8 +78,10 @@ import qualified Control.Monad.Fail as Fail
6878
import Control.Monad.Trans.Except
6979
import Control.Monad.Trans.Class
7080
import Control.Monad.IO.Class
81+
import Data.Proxy (Proxy(..))
7182
import qualified Data.Map as Map
7283
import Data.Map (Map)
84+
import Data.Maybe (fromMaybe)
7385
import Data.Set (Set)
7486
import Data.Typeable (Typeable)
7587
import Data.Void
@@ -81,8 +93,11 @@ import Data.Parameterized.Some (Some)
8193
import Data.Parameterized.TraversableFC (toListFC)
8294

8395
import Verifier.SAW.SharedTerm as SAWVerifier
96+
import Verifier.SAW.TypedAST as SAWVerifier
8497
import Verifier.SAW.TypedTerm as SAWVerifier
8598

99+
import qualified Lang.Crucible.Backend as Crucible
100+
import qualified Lang.Crucible.Backend.Online as Crucible
86101
import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr, GlobalVar)
87102
import qualified Lang.Crucible.Simulator.GlobalState as Crucible
88103
import qualified Lang.Crucible.Simulator.RegMap as Crucible
@@ -93,9 +108,10 @@ import qualified What4.LabeledPred as W4
93108
import qualified What4.ProgramLoc as W4
94109

95110
import SAWScript.Exceptions
96-
import SAWScript.Crucible.Common (Sym)
111+
import SAWScript.Crucible.Common (Backend, OnlineSolver, Sym)
97112
import SAWScript.Crucible.Common.MethodSpec as MS
98113
import SAWScript.Crucible.Common.Setup.Value as MS
114+
import SAWScript.Utils (bullets)
99115

100116
-- TODO, not sure this is the best place for this definition
101117
type MetadataMap =
@@ -397,6 +413,115 @@ enforceCompleteSubstitution loc ss =
397413

398414
unless (null missing) (failure loc (AmbiguousVars missing))
399415

416+
-- | Allocate fresh variables for all of the "fresh" vars
417+
-- used in this phase and add them to the term substitution.
418+
refreshTerms ::
419+
SharedContext {- ^ shared context -} ->
420+
MS.StateSpec ext {- ^ current phase spec -} ->
421+
OverrideMatcher ext w ()
422+
refreshTerms sc ss =
423+
do extension <- Map.fromList <$> traverse freshenTerm (view MS.csFreshVars ss)
424+
OM (termSub %= Map.union extension)
425+
where
426+
freshenTerm (TypedExtCns _cty ec) =
427+
do ec' <- liftIO $ scFreshEC sc (toShortName (ecName ec)) (ecType ec)
428+
new <- liftIO $ scExtCns sc ec'
429+
return (ecVarIndex ec, new)
430+
431+
-- | An override packaged together with its preconditions, labeled with some
432+
-- human-readable info about each condition.
433+
data OverrideWithPreconditions ext =
434+
OverrideWithPreconditions
435+
{ _owpPreconditions :: [(MS.ConditionMetadata, LabeledPred Sym)]
436+
-- ^ c.f. '_osAsserts'
437+
, _owpMethodSpec :: MS.CrucibleMethodSpecIR ext
438+
, owpState :: OverrideState ext
439+
}
440+
deriving (Generic)
441+
442+
makeLenses ''OverrideWithPreconditions
443+
444+
-- | Partition into three groups:
445+
-- * Preconditions concretely succeed
446+
-- * Preconditions concretely fail
447+
-- * Preconditions are symbolic
448+
partitionOWPsConcrete :: forall ext.
449+
Sym ->
450+
[OverrideWithPreconditions ext] ->
451+
IO ([OverrideWithPreconditions ext], [OverrideWithPreconditions ext], [OverrideWithPreconditions ext])
452+
partitionOWPsConcrete sym =
453+
let trav = owpPreconditions . each . _2 . W4.labeledPred
454+
in W4.partitionByPredsM (Just sym) $
455+
foldlMOf trav (W4.andPred sym) (W4.truePred sym)
456+
457+
-- | Like 'W4.partitionByPreds', but partitions on solver responses, not just
458+
-- concretized values.
459+
partitionBySymbolicPreds ::
460+
(OnlineSolver solver, Foldable t) =>
461+
Backend solver {- ^ solver connection -} ->
462+
(a -> W4.Pred Sym) {- ^ how to extract predicates -} ->
463+
t a ->
464+
IO (Map Crucible.BranchResult [a])
465+
partitionBySymbolicPreds sym getPred =
466+
let step mp a =
467+
Crucible.considerSatisfiability sym Nothing (getPred a) <&> \k ->
468+
Map.insertWith (++) k [a] mp
469+
in foldM step Map.empty
470+
471+
-- | Find individual preconditions that are symbolically false
472+
--
473+
-- We should probably be using unsat cores for this.
474+
findFalsePreconditions ::
475+
OnlineSolver solver =>
476+
Backend solver ->
477+
OverrideWithPreconditions ext ->
478+
IO [(MS.ConditionMetadata, LabeledPred Sym)]
479+
findFalsePreconditions bak owp =
480+
fromMaybe [] . Map.lookup (Crucible.NoBranch False) <$>
481+
partitionBySymbolicPreds bak (view (_2 . W4.labeledPred)) (owp ^. owpPreconditions)
482+
483+
-- | Is this group of predicates collectively unsatisfiable?
484+
unsatPreconditions ::
485+
OnlineSolver solver =>
486+
Backend solver {- ^ solver connection -} ->
487+
Fold s (W4.Pred Sym) {- ^ how to extract predicates -} ->
488+
s {- ^ a container full of predicates -}->
489+
IO Bool
490+
unsatPreconditions bak container getPreds = do
491+
let sym = Crucible.backendGetSym bak
492+
conj <- W4.andAllOf sym container getPreds
493+
Crucible.considerSatisfiability bak Nothing conj >>=
494+
\case
495+
Crucible.NoBranch False -> pure True
496+
_ -> pure False
497+
498+
-- | Print a message about failure of an override's preconditions
499+
ppFailure ::
500+
(PP.Pretty (ExtType ext), PP.Pretty (MethodId ext)) =>
501+
OverrideWithPreconditions ext ->
502+
[LabeledPred Sym] ->
503+
PP.Doc ann
504+
ppFailure owp false =
505+
PP.vcat
506+
[ MS.ppMethodSpec (owp ^. owpMethodSpec)
507+
-- TODO: remove viaShow when crucible switches to prettyprinter
508+
, bullets '*' (map (PP.viaShow . Crucible.ppSimError)
509+
(false ^.. traverse . W4.labeledPredMsg))
510+
]
511+
512+
-- | Print a message about concrete failure of an override's preconditions
513+
--
514+
-- Assumes that the override it's being passed does have concretely failing
515+
-- preconditions. Otherwise, the error won't make much sense.
516+
ppConcreteFailure ::
517+
(PP.Pretty (ExtType ext), PP.Pretty (MethodId ext)) =>
518+
OverrideWithPreconditions ext ->
519+
PP.Doc ann
520+
ppConcreteFailure owp =
521+
let (_, false, _) =
522+
W4.partitionLabeledPreds (Proxy :: Proxy Sym) (map snd (owp ^. owpPreconditions))
523+
in ppFailure owp false
524+
400525
------------------------------------------------------------------------
401526

402527
-- | Forget the type indexes and length of the arguments.

‎src/SAWScript/Crucible/JVM/Override.hs

-15
Original file line numberDiff line numberDiff line change
@@ -369,21 +369,6 @@ executeCond opts sc cc cs ss =
369369
traverse_ (executeSetupCondition opts sc cc cs) (ss ^. MS.csConditions)
370370

371371

372-
-- | Allocate fresh variables for all of the "fresh" vars
373-
-- used in this phase and add them to the term substitution.
374-
refreshTerms ::
375-
SharedContext {- ^ shared context -} ->
376-
StateSpec {- ^ current phase spec -} ->
377-
OverrideMatcher CJ.JVM w ()
378-
refreshTerms sc ss =
379-
do extension <- Map.fromList <$> traverse freshenTerm (view MS.csFreshVars ss)
380-
OM (termSub %= Map.union extension)
381-
where
382-
freshenTerm (TypedExtCns _cty ec) =
383-
do ec' <- liftIO $ scFreshEC sc (toShortName (ecName ec)) (ecType ec)
384-
new <- liftIO $ scExtCns sc ec'
385-
return (ecVarIndex ec, new)
386-
387372
------------------------------------------------------------------------
388373

389374
-- | Generate assertions that all of the memory allocations matched by

‎src/SAWScript/Crucible/LLVM/Override.hs

+5-114
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,6 @@ import Control.Lens.Fold
6363
import Control.Lens.Getter
6464
import Control.Lens.Lens
6565
import Control.Lens.Setter
66-
import Control.Lens.TH
6766
import Control.Exception as X
6867
import Control.Monad
6968
import Control.Monad.Except
@@ -75,13 +74,11 @@ import Data.IORef (IORef, modifyIORef)
7574
import Data.Map (Map)
7675
import qualified Data.Map as Map
7776
import Data.Maybe
78-
import Data.Proxy
7977
import Data.Set (Set)
8078
import qualified Data.Set as Set
8179
import Data.Text (Text, pack)
8280
import qualified Data.Vector as V
8381
import Data.Void (absurd)
84-
import GHC.Generics (Generic)
8582
import Numeric.Natural
8683
import qualified Prettyprinter as PP
8784

@@ -92,7 +89,6 @@ import qualified Cryptol.Eval.Type as Cryptol (TValue(..), evalType)
9289
import qualified Cryptol.Utils.PP as Cryptol (pp)
9390

9491
import qualified Lang.Crucible.Backend as Crucible
95-
import qualified Lang.Crucible.Backend.Online as Crucible
9692
import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr(UnitRepr))
9793
import qualified Lang.Crucible.FunctionHandle as Crucible
9894
import qualified Lang.Crucible.LLVM.Bytes as Crucible
@@ -140,20 +136,7 @@ import SAWScript.Options
140136
import SAWScript.Panic
141137
import SAWScript.Utils (bullets, handleException)
142138

143-
type LabeledPred sym = W4.LabeledPred (W4.Pred sym) Crucible.SimError
144-
145-
-- | An override packaged together with its preconditions, labeled with some
146-
-- human-readable info about each condition.
147-
data OverrideWithPreconditions arch =
148-
OverrideWithPreconditions
149-
{ _owpPreconditions :: [(MS.ConditionMetadata, LabeledPred Sym)]
150-
-- ^ c.f. '_osAsserts'
151-
, _owpMethodSpec :: MS.CrucibleMethodSpecIR (LLVM arch)
152-
, owpState :: OverrideState (LLVM arch)
153-
}
154-
deriving (Generic)
155-
156-
makeLenses ''OverrideWithPreconditions
139+
type instance Pointer' (LLVM arch) Sym = LLVMPtr (Crucible.ArchWidth arch)
157140

158141
------------------------------------------------------------------------
159142
-- Translating SAW values to Crucible values for good error messages
@@ -259,89 +242,12 @@ notEqual cond opts loc cc sc spec expected actual = do
259242

260243
------------------------------------------------------------------------
261244

262-
-- | Partition into three groups:
263-
-- * Preconditions concretely succeed
264-
-- * Preconditions concretely fail
265-
-- * Preconditions are symbolic
266-
partitionOWPsConcrete :: forall arch.
267-
Sym ->
268-
[OverrideWithPreconditions arch] ->
269-
IO ([OverrideWithPreconditions arch], [OverrideWithPreconditions arch], [OverrideWithPreconditions arch])
270-
partitionOWPsConcrete sym =
271-
let traversal = owpPreconditions . each . _2 . W4.labeledPred
272-
in W4.partitionByPredsM (Just sym) $
273-
foldlMOf traversal (W4.andPred sym) (W4.truePred sym)
274-
275-
-- | Like 'W4.partitionByPreds', but partitions on solver responses, not just
276-
-- concretized values.
277-
partitionBySymbolicPreds ::
278-
(OnlineSolver solver, Foldable t) =>
279-
Backend solver {- ^ solver connection -} ->
280-
(a -> W4.Pred Sym) {- ^ how to extract predicates -} ->
281-
t a ->
282-
IO (Map Crucible.BranchResult [a])
283-
partitionBySymbolicPreds sym getPred =
284-
let step mp a =
285-
Crucible.considerSatisfiability sym Nothing (getPred a) <&> \k ->
286-
Map.insertWith (++) k [a] mp
287-
in foldM step Map.empty
288-
289-
-- | Find individual preconditions that are symbolically false
290-
--
291-
-- We should probably be using unsat cores for this.
292-
findFalsePreconditions ::
293-
OnlineSolver solver =>
294-
Backend solver ->
295-
OverrideWithPreconditions arch ->
296-
IO [(MS.ConditionMetadata, LabeledPred Sym)]
297-
findFalsePreconditions bak owp =
298-
fromMaybe [] . Map.lookup (Crucible.NoBranch False) <$>
299-
partitionBySymbolicPreds bak (view (_2 . W4.labeledPred)) (owp ^. owpPreconditions)
300-
301-
-- | Is this group of predicates collectively unsatisfiable?
302-
unsatPreconditions ::
303-
OnlineSolver solver =>
304-
Backend solver {- ^ solver connection -} ->
305-
Fold s (W4.Pred Sym) {- ^ how to extract predicates -} ->
306-
s {- ^ a container full of predicates -}->
307-
IO Bool
308-
unsatPreconditions bak container getPreds = do
309-
let sym = backendGetSym bak
310-
conj <- W4.andAllOf sym container getPreds
311-
Crucible.considerSatisfiability bak Nothing conj >>=
312-
\case
313-
Crucible.NoBranch False -> pure True
314-
_ -> pure False
315-
316-
-- | Print a message about failure of an override's preconditions
317-
ppFailure ::
318-
OverrideWithPreconditions arch ->
319-
[LabeledPred Sym] ->
320-
PP.Doc ann
321-
ppFailure owp false =
322-
PP.vcat
323-
[ MS.ppMethodSpec (owp ^. owpMethodSpec)
324-
-- TODO: remove viaShow when crucible switches to prettyprinter
325-
, bullets '*' (map (PP.viaShow . Crucible.ppSimError)
326-
(false ^.. traverse . W4.labeledPredMsg))
327-
]
328-
329-
-- | Print a message about concrete failure of an override's preconditions
330-
--
331-
-- Assumes that the override it's being passed does have concretely failing
332-
-- preconditions. Otherwise, the error won't make much sense.
333-
ppConcreteFailure :: OverrideWithPreconditions arch -> PP.Doc ann
334-
ppConcreteFailure owp =
335-
let (_, false, _) =
336-
W4.partitionLabeledPreds (Proxy :: Proxy Sym) (map snd (owp ^. owpPreconditions))
337-
in ppFailure owp false
338-
339245
-- | Print a message about symbolic failure of an override's preconditions
340246
--
341247
-- TODO: Needs additional testing. Are these messages useful?
342248
{-
343249
ppSymbolicFailure ::
344-
(OverrideWithPreconditions arch, [LabeledPred Sym]) ->
250+
(OverrideWithPreconditions (LLVM arch), [LabeledPred Sym]) ->
345251
PP.Doc
346252
ppSymbolicFailure = uncurry ppFailure
347253
-}
@@ -488,7 +394,7 @@ handleSingleOverrideBranch :: forall arch rtp args ret.
488394
W4.ProgramLoc {- ^ Location of the call site for error reporting-} ->
489395
IORef MetadataMap ->
490396
Crucible.FnHandle args ret {- ^ the handle for this function -} ->
491-
OverrideWithPreconditions arch ->
397+
OverrideWithPreconditions (LLVM arch) ->
492398
Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym Crucible.LLVM rtp args ret
493399
(Crucible.RegValue Sym ret)
494400
handleSingleOverrideBranch opts sc cc call_loc mdMap h (OverrideWithPreconditions preconds cs st) =
@@ -547,8 +453,8 @@ handleOverrideBranches :: forall arch rtp args ret.
547453
NE.NonEmpty (MS.CrucibleMethodSpecIR (LLVM arch))
548454
{- ^ specification for current function override -} ->
549455
Crucible.FnHandle args ret {- ^ the handle for this function -} ->
550-
[OverrideWithPreconditions arch] ->
551-
([OverrideWithPreconditions arch],[OverrideWithPreconditions arch],[OverrideWithPreconditions arch]) ->
456+
[OverrideWithPreconditions (LLVM arch)] ->
457+
([OverrideWithPreconditions (LLVM arch)],[OverrideWithPreconditions (LLVM arch)],[OverrideWithPreconditions (LLVM arch)]) ->
552458
Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym Crucible.LLVM rtp args ret
553459
(Crucible.RegValue Sym ret)
554460

@@ -833,21 +739,6 @@ executeCond opts sc cc cs ss = do
833739
(ss ^. MS.csPointsTos)
834740
traverse_ (executeSetupCondition opts sc cc cs) (ss ^. MS.csConditions)
835741

836-
-- | Allocate fresh variables for all of the "fresh" vars
837-
-- used in this phase and add them to the term substitution.
838-
refreshTerms ::
839-
SharedContext {- ^ shared context -} ->
840-
MS.StateSpec (LLVM arch) {- ^ current phase spec -} ->
841-
OverrideMatcher (LLVM arch) md ()
842-
refreshTerms sc ss =
843-
do extension <- Map.fromList <$> traverse freshenTerm (view MS.csFreshVars ss)
844-
OM (termSub %= Map.union extension)
845-
where
846-
freshenTerm (TypedExtCns _cty ec) =
847-
do ec' <- liftIO $ scFreshEC sc (toShortName (ecName ec)) (ecType ec)
848-
new <- liftIO $ scExtCns sc ec'
849-
return (ecVarIndex ec, new)
850-
851742
------------------------------------------------------------------------
852743

853744
-- | Generate assertions that all of the memory regions matched by an

0 commit comments

Comments
 (0)