Skip to content

Commit 53cf3e8

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 00b5511 commit 53cf3e8

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 (filterM, foldM, forM, forM_, when, zipWithM)
6968
import Control.Monad.Except (runExcept)
@@ -76,13 +75,11 @@ import Data.IORef (IORef, modifyIORef)
7675
import Data.Map (Map)
7776
import qualified Data.Map as Map
7877
import Data.Maybe
79-
import Data.Proxy
8078
import Data.Set (Set)
8179
import qualified Data.Set as Set
8280
import Data.Text (Text, pack)
8381
import qualified Data.Vector as V
8482
import Data.Void (absurd)
85-
import GHC.Generics (Generic)
8683
import Numeric.Natural
8784
import qualified Prettyprinter as PP
8885

@@ -93,7 +90,6 @@ import qualified Cryptol.Eval.Type as Cryptol (TValue(..), evalType)
9390
import qualified Cryptol.Utils.PP as Cryptol (pp)
9491

9592
import qualified Lang.Crucible.Backend as Crucible
96-
import qualified Lang.Crucible.Backend.Online as Crucible
9793
import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr(UnitRepr))
9894
import qualified Lang.Crucible.FunctionHandle as Crucible
9995
import qualified Lang.Crucible.LLVM.Bytes as Crucible
@@ -141,20 +137,7 @@ import SAWScript.Options
141137
import SAWScript.Panic
142138
import SAWScript.Utils (bullets, handleException)
143139

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

159142
------------------------------------------------------------------------
160143
-- Translating SAW values to Crucible values for good error messages
@@ -260,89 +243,12 @@ notEqual cond opts loc cc sc spec expected actual = do
260243

261244
------------------------------------------------------------------------
262245

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

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

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

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

0 commit comments

Comments
 (0)