-
Notifications
You must be signed in to change notification settings - Fork 63
/
Copy pathOverride.hs
2570 lines (2335 loc) · 109 KB
/
Override.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
{- |
Module : SAWScript.Crucible.LLVM.Override
Description : Override matching and application for LLVM
License : BSD3
Maintainer : atomb
Stability : provisional
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ParallelListComp #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module SAWScript.Crucible.LLVM.Override
( OverrideMatcher
, OverrideMatcher'(..)
, runOverrideMatcher
, setupValueSub
, executeFreshPointer
, osAsserts
, termSub
, learnCond
, learnSetupCondition
, executeSetupCondition
, matchArg
, matchPointsToValue
, matchPointsToBitfieldValue
, assertTermEqualities
, methodSpecHandler
, valueToSC
, storePointsToValue
, storePointsToBitfieldValue
, doAllocSymInit
, diffMemTypes
, ppPointsToAsLLVMVal
, enableSMTArrayMemoryModel
) where
import Control.Lens ( _2 )
import Control.Lens.At
import Control.Lens.Each
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
import Control.Monad.Except
import Data.Either (partitionEithers)
import Data.Foldable (for_, traverse_, toList)
import Data.List
import qualified Data.List.NonEmpty as NE
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
import qualified Text.LLVM.AST as L
import qualified Cryptol.TypeCheck.AST as Cryptol (Schema(..))
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
import qualified Lang.Crucible.LLVM.DataLayout as Crucible
import qualified Lang.Crucible.LLVM.MemModel as Crucible
import qualified Lang.Crucible.LLVM.MemType as Crucible
import qualified Lang.Crucible.LLVM.Translation as Crucible
import qualified Lang.Crucible.Simulator.GlobalState as Crucible
import qualified Lang.Crucible.Simulator.OverrideSim as Crucible
import qualified Lang.Crucible.Simulator.RegMap as Crucible
import qualified Lang.Crucible.Simulator.SimError as Crucible
import qualified What4.BaseTypes as W4
import qualified What4.Config as W4
import qualified What4.Expr.Builder as W4
import qualified What4.Interface as W4
import qualified What4.LabeledPred as W4
import qualified What4.ProgramLoc as W4
import qualified What4.Symbol as W4
import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.NatRepr
import Data.Parameterized.Some (Some(..))
import qualified Data.BitVector.Sized as BV
import Verifier.SAW.Prelude (scEq)
import Verifier.SAW.SharedTerm
import Verifier.SAW.TypedAST
import Verifier.SAW.Recognizer
import Verifier.SAW.TypedTerm
import Verifier.SAW.Simulator.What4.ReturnTrip (SAWCoreState(..), toSC, bindSAWTerm)
import SAWScript.Crucible.Common
import SAWScript.Crucible.Common.MethodSpec (SetupValue(..), PointsTo)
import qualified SAWScript.Crucible.Common.MethodSpec as MS
import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), PrePost(..))
import SAWScript.Crucible.Common.Override hiding (getSymInterface)
import qualified SAWScript.Crucible.Common.Override as Ov (getSymInterface)
import SAWScript.Crucible.LLVM.MethodSpecIR
import SAWScript.Crucible.LLVM.ResolveSetupValue
import SAWScript.Crucible.LLVM.Setup.Value ()
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
------------------------------------------------------------------------
-- Translating SAW values to Crucible values for good error messages
ppLLVMVal ::
LLVMCrucibleContext arch ->
LLVMVal ->
OverrideMatcher (LLVM arch) w (PP.Doc ann)
ppLLVMVal cc val = do
sym <- Ov.getSymInterface
mem <- readGlobal (Crucible.llvmMemVar (ccLLVMContext cc))
-- TODO: remove viaShow when crucible switches to prettyprinter
pure $ PP.viaShow $ Crucible.ppLLVMValWithGlobals sym (Crucible.memImplSymbolMap mem) val
-- | Resolve a 'SetupValue' into a 'LLVMVal' and pretty-print it
ppSetupValueAsLLVMVal ::
(?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
Options {- ^ output/verbosity options -} ->
LLVMCrucibleContext arch ->
SharedContext {- ^ context for constructing SAW terms -} ->
MS.CrucibleMethodSpecIR (LLVM arch) {- ^ for name and typing environments -} ->
SetupValue (LLVM arch) ->
OverrideMatcher (LLVM arch) w (PP.Doc ann)
ppSetupValueAsLLVMVal opts cc sc spec setupval = do
(_memTy, llvmval) <- resolveSetupValueLLVM opts cc sc spec setupval
ppLLVMVal cc llvmval
-- | Try to translate the spec\'s 'SetupValue' into an 'LLVMVal', pretty-print
-- the 'LLVMVal'.
mkStructuralMismatch ::
(Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
Options {- ^ output/verbosity options -} ->
LLVMCrucibleContext arch ->
SharedContext {- ^ context for constructing SAW terms -} ->
MS.CrucibleMethodSpecIR (LLVM arch) {- ^ for name and typing environments -} ->
Crucible.LLVMVal Sym {- ^ the value from the simulator -} ->
SetupValue (LLVM arch) {- ^ the value from the spec -} ->
Crucible.MemType {- ^ the expected type -} ->
OverrideMatcher (LLVM arch) w (OverrideFailureReason (LLVM arch))
mkStructuralMismatch _opts cc _sc spec llvmval setupval memTy =
let tyEnv = MS.csAllocations spec
nameEnv = MS.csTypeNames spec
maybeMsgTy = either (const Nothing) Just $ runExcept (typeOfSetupValue cc tyEnv nameEnv setupval)
in pure $ StructuralMismatch
(PP.pretty llvmval)
(MS.ppSetupValue setupval)
maybeMsgTy
memTy
-- | Instead of using 'ppPointsTo', which prints 'SetupValue', translate
-- expressions to 'LLVMVal'.
ppPointsToAsLLVMVal ::
(?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
Options {- ^ output/verbosity options -} ->
LLVMCrucibleContext arch ->
SharedContext {- ^ context for constructing SAW terms -} ->
MS.CrucibleMethodSpecIR (LLVM arch) {- ^ for name and typing environments -} ->
PointsTo (LLVM arch) ->
OverrideMatcher (LLVM arch) w (PP.Doc ann)
ppPointsToAsLLVMVal opts cc sc spec (LLVMPointsTo md cond ptr val) = do
pretty1 <- ppSetupValueAsLLVMVal opts cc sc spec ptr
let pretty2 = PP.pretty val
pure $ PP.vcat [ "Pointer:" PP.<+> pretty1
, "Pointee:" PP.<+> pretty2
, maybe PP.emptyDoc (\tt -> "Condition:" PP.<+> MS.ppTypedTerm tt) cond
, "Assertion made at:" PP.<+>
PP.pretty (W4.plSourceLoc (MS.conditionLoc md))
]
ppPointsToAsLLVMVal opts cc sc spec (LLVMPointsToBitfield md ptr fieldName val) = do
pretty1 <- ppSetupValueAsLLVMVal opts cc sc spec ptr
let pretty2 = MS.ppSetupValue val
pure $ PP.vcat [ "Pointer (bitfield):" PP.<+> pretty1 <> PP.pretty ("." ++ fieldName)
, "Pointee:" PP.<+> pretty2
, "Assertion made at:" PP.<+>
PP.pretty (W4.plSourceLoc (MS.conditionLoc md))
]
-- | Create an error stating that the 'LLVMVal' was not equal to the 'SetupValue'
notEqual ::
(?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
PrePost ->
Options {- ^ output/verbosity options -} ->
W4.ProgramLoc {- ^ where is the assertion from? -} ->
LLVMCrucibleContext arch ->
SharedContext {- ^ context for constructing SAW terms -} ->
MS.CrucibleMethodSpecIR (LLVM arch) {- ^ for name and typing environments -} ->
SetupValue (LLVM arch) {- ^ the value from the spec -} ->
Crucible.LLVMVal Sym {- ^ the value from the simulator -} ->
OverrideMatcher (LLVM arch) w Crucible.SimError
notEqual cond opts loc cc sc spec expected actual = do
prettyLLVMVal <- ppLLVMVal cc actual
prettySetupLLVMVal <- ppSetupValueAsLLVMVal opts cc sc spec expected
let msg = unlines
[ "Equality " ++ MS.stateCond cond
, "Expected value (as a SAW value): "
, show (MS.ppSetupValue expected)
, "Expected value (as a Crucible value): "
, show prettySetupLLVMVal
, "Actual value: "
, show prettyLLVMVal
]
pure $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg ""
------------------------------------------------------------------------
-- | 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]) ->
PP.Doc
ppSymbolicFailure = uncurry ppFailure
-}
-- | Pretty-print the arguments passed to an override
ppArgs ::
forall arch args ann.
(Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
Sym ->
LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} ->
MS.CrucibleMethodSpecIR (LLVM arch) {- ^ specification for current function override -} ->
Crucible.RegMap Sym args {- ^ arguments from the simulator -} ->
IO [PP.Doc ann]
ppArgs sym cc cs (Crucible.RegMap args) = do
let expectedArgTypes = map fst (Map.elems (cs ^. MS.csArgBindings))
let aux memTy (Crucible.AnyValue tyrep val) =
do storTy <- Crucible.toStorableType memTy
llvmval <- Crucible.packMemValue sym storTy tyrep val
return (llvmval, memTy)
case Crucible.lookupGlobal (Crucible.llvmMemVar (ccLLVMContext cc)) (cc^.ccLLVMGlobals) of
Nothing -> fail "Internal error: Couldn't find LLVM memory variable"
Just mem -> do
-- TODO: remove viaShow when crucible switches to prettyprinter
map (PP.viaShow . Crucible.ppLLVMValWithGlobals sym (Crucible.memImplSymbolMap mem) . fst) <$>
liftIO (zipWithM aux expectedArgTypes (assignmentToList args))
-- | This function is responsible for implementing the \"override\" behavior
-- of method specifications. The main work done in this function to manage
-- the process of selecting between several possible different override
-- specifications that could apply. We want a proof to succeed if _any_
-- choice of method spec allows the proof to go through, which is a slightly
-- awkward thing to fit into the symbolic simulation framework.
--
-- The main work of determining the preconditions, postconditions, memory
-- updates and return value for a single specification is done by
-- the @methodSpecHandler_prestate@ and @methodSpecHandler_poststate@ functions.
--
-- In a first phase, we attempt to apply the precondition portion of each of
-- the given method specifications. Each of them that might apply generate
-- a substitution for the setup variables and a collection of preconditions
-- that guard the specification. We use these preconditions to compute
-- a multiway symbolic branch, one for each override which might apply.
--
-- In the body of each of the individual branches, we compute the postcondition
-- actions of the corresponding method specification. This will update memory
-- and compute function return values, in addition to assuming postcondition
-- predicates.
methodSpecHandler ::
forall arch rtp args ret.
( ?lc :: Crucible.TypeContext
, ?memOpts::Crucible.MemOptions
, ?w4EvalTactic :: W4EvalTactic
, ?checkAllocSymInit :: Bool
, ?singleOverrideSpecialCase :: Bool
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
Options {- ^ output/verbosity options -} ->
SharedContext {- ^ context for constructing SAW terms -} ->
LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} ->
IORef MetadataMap ->
NE.NonEmpty (MS.CrucibleMethodSpecIR (LLVM arch))
{- ^ specification for current function override -} ->
Crucible.FnHandle args ret {- ^ the handle for this function -} ->
Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym Crucible.LLVM rtp args ret
(Crucible.RegValue Sym ret)
methodSpecHandler opts sc cc mdMap css h =
ccWithBackend cc $ \bak -> do
let sym = backendGetSym bak
let fnName = NE.head css ^. csName
call_loc <- liftIO $ W4.getCurrentProgramLoc sym
liftIO $ printOutLn opts Info $ unwords
[ "Matching"
, show (length css)
, "overrides of "
, fnName
, "..."
]
Crucible.RegMap args <- Crucible.getOverrideArgs
-- First, run the precondition matcher phase. Collect together a list of the results.
-- For each override, this will either be an error message, or a matcher state and
-- a method spec.
prestates <-
do g0 <- Crucible.readGlobals
forM css $ \cs -> liftIO $
let initialFree = Set.fromList (map (ecVarIndex . tecExt)
(view (MS.csPreState . MS.csFreshVars) cs))
in runOverrideMatcher sym g0 Map.empty Map.empty initialFree (view MS.csLoc cs)
(do methodSpecHandler_prestate opts sc cc args cs
return cs)
-- Print a failure message if all overrides failed to match. Otherwise, collect
-- all the override states that might apply, and compute the conjunction of all
-- the preconditions. We'll use these to perform symbolic branches between the
-- various overrides.
branches <-
let prettyError methodSpec failureReason = do
prettyArgs <- liftIO $ ppArgs sym cc methodSpec (Crucible.RegMap args)
pure $
PP.vcat
[ MS.ppMethodSpec methodSpec
, "Arguments:"
, bullets '-' prettyArgs
, ppOverrideFailure failureReason
]
in
case partitionEithers (toList prestates) of
(errs, []) -> do
msgs <-
mapM (\(cs, err) ->
("*" PP.<>) . PP.indent 2 <$> prettyError cs err)
(zip (toList css) errs)
fail $ show $
PP.vcat ["All overrides failed during structural matching:", PP.vcat msgs]
(_, ss) -> liftIO $
forM ss $ \(cs,st) ->
return (OverrideWithPreconditions (st^.osAsserts) cs st)
-- Now we do a second phase of simple compatibility checking: we check to see
-- if any of the preconditions of the various overrides are concretely false.
-- If so, there's no use in branching on them with @symbolicBranches@.
(true, false, unknown) <- liftIO $ partitionOWPsConcrete sym branches
-- Check if there is only a single override branch that might apply at this
-- point. If so, commit to it and handle that case specially. If there is
-- more than one (or zero) branches that might apply, go to the general case.
case true ++ unknown of
[singleBranch] | ?singleOverrideSpecialCase ->
handleSingleOverrideBranch opts sc cc call_loc mdMap h singleBranch
_ -> handleOverrideBranches opts sc cc call_loc css h branches (true, false, unknown)
handleSingleOverrideBranch :: forall arch rtp args ret.
( ?lc :: Crucible.TypeContext
, ?memOpts::Crucible.MemOptions
, ?w4EvalTactic :: W4EvalTactic
, ?checkAllocSymInit :: Bool
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
Options {- ^ output/verbosity options -} ->
SharedContext {- ^ context for constructing SAW terms -} ->
LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} ->
W4.ProgramLoc {- ^ Location of the call site for error reporting-} ->
IORef MetadataMap ->
Crucible.FnHandle args ret {- ^ the handle for this function -} ->
OverrideWithPreconditions 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) =
ccWithBackend cc $ \bak -> do
let sym = backendGetSym bak
let fnName = cs ^. csName
let retTy = Crucible.handleReturnType h
liftIO $ printOutLn opts Info $ unwords
[ "Found a single potential override for"
, fnName
]
-- First assert the override preconditions
liftIO $ forM_ preconds $ \(md,W4.LabeledPred p r) ->
do (ann,p') <- W4.annotateTerm sym p
let caller = unwords ["Override called from:", show (W4.plSourceLoc call_loc)]
let md' = md{ MS.conditionContext = MS.conditionContext md ++ caller }
modifyIORef mdMap (Map.insert ann md')
Crucible.addAssertion bak (Crucible.LabeledPred p' r)
g <- Crucible.readGlobals
res <- liftIO $ runOverrideMatcher sym g
(st^.setupValueSub)
(st^.termSub)
(st^.osFree)
(st^.osLocation)
(methodSpecHandler_poststate opts sc cc retTy cs)
case res of
Left (OF loc rsn) ->
-- TODO, better pretty printing for reasons
liftIO
$ Crucible.abortExecBecause
$ Crucible.AssertionFailure
$ Crucible.SimError loc
$ Crucible.AssertFailureSimError "assumed false" (show rsn)
Right (ret,st') ->
do liftIO $ forM_ (st'^.osAssumes) $ \(_md,asum) ->
Crucible.addAssumption bak
$ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum
Crucible.writeGlobals (st'^.overrideGlobals)
Crucible.overrideReturn' (Crucible.RegEntry retTy ret)
handleOverrideBranches :: forall arch rtp args ret.
( ?lc :: Crucible.TypeContext
, ?memOpts::Crucible.MemOptions
, ?w4EvalTactic :: W4EvalTactic
, ?checkAllocSymInit :: Bool
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
Options {- ^ output/verbosity options -} ->
SharedContext {- ^ context for constructing SAW terms -} ->
LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} ->
W4.ProgramLoc {- ^ Location of the call site for error reporting-} ->
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]) ->
Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym Crucible.LLVM rtp args ret
(Crucible.RegValue Sym ret)
handleOverrideBranches opts sc cc call_loc css h branches (true, false, unknown) =
ccWithBackend cc $ \bak -> do
let sym = backendGetSym bak
let fnName = NE.head css ^. csName
Crucible.RegMap args <- Crucible.getOverrideArgs
-- Collapse the preconditions to a single predicate
branches' <- liftIO $ forM (true ++ unknown) $
\(OverrideWithPreconditions preconds cs st) ->
W4.andAllOf sym (folded . _2 . W4.labeledPred) preconds <&>
\precond -> (precond, cs, st)
-- Now use crucible's symbolic branching machinery to select between the branches.
-- Essentially, we are doing an n-way if statement on the precondition predicates
-- for each override, and selecting the first one whose preconditions hold.
--
-- Then, in the body of the branch, we run the poststate handler to update the
-- memory state, compute return values and compute postcondition predicates.
--
-- For each override branch that doesn't fail outright, we assume the relevant
-- postconditions, update the crucible global variable state, and return the
-- computed return value.
--
-- We add a final default branch that simply fails unless some previous override
-- branch has already succeeded.
liftIO $ printOutLn opts Info $ unwords
[ "Branching on"
, show (length branches')
, "override variants of"
, fnName
, "..."
]
let retTy = Crucible.handleReturnType h
res <- Crucible.regValue <$> Crucible.callOverride h
(Crucible.mkOverride' "overrideBranches" retTy
(Crucible.symbolicBranches Crucible.emptyRegMap $
[ ( precond
, do g <- Crucible.readGlobals
res <- liftIO $ runOverrideMatcher sym g
(st^.setupValueSub)
(st^.termSub)
(st^.osFree)
(st^.osLocation)
(methodSpecHandler_poststate opts sc cc retTy cs)
case res of
Left (OF loc rsn) ->
-- TODO, better pretty printing for reasons
liftIO
$ Crucible.abortExecBecause
$ Crucible.AssertionFailure
$ Crucible.SimError loc
$ Crucible.AssertFailureSimError "assumed false" (show rsn)
Right (ret,st') ->
do liftIO $ forM_ (st'^.osAssumes) $ \(_md,asum) ->
Crucible.addAssumption bak
$ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum
Crucible.writeGlobals (st'^.overrideGlobals)
Crucible.overrideReturn' (Crucible.RegEntry retTy ret)
, Just (W4.plSourceLoc (cs ^. MS.csLoc))
)
| (precond, cs, st) <- branches'
] ++
[ let e prettyArgs symFalse unsat = show $ PP.vcat $ concat
[ [ PP.pretty $
"No override specification applies for " ++ fnName ++ "."
]
, [ "Arguments:"
, bullets '-' prettyArgs
]
, if | not (null false) ->
[ PP.vcat
[ PP.pretty (unwords
[ "The following overrides had some preconditions"
, "that failed concretely:"
])
, bullets '-' (map ppConcreteFailure false)
]
]
-- See comment on ppSymbolicFailure: this needs more
-- examination to see if it's useful.
-- - | not (null symFalse) ->
-- [ PP.text (unwords
-- [ "The following overrides had some preconditions "
-- , "that failed symbolically:"
-- ]) PP.<$$> bullets '-' (map ppSymbolicFailure symFalse)
-- ]
-- Note that we only print these in case no override had
-- individually (concretely or symbolically) false
-- preconditions.
| not (null unsat) && null false && null symFalse ->
[ PP.vcat
[ PP.pretty (unwords
[ "The conjunction of these overrides' preconditions"
, "was unsatisfiable, meaning your override can never"
, "apply. You probably have unintentionally specified"
, "mutually exclusive/inconsistent preconditions."
])
, bullets '-' (unsat ^.. each . owpMethodSpec . to MS.ppMethodSpec)
]
]
| null false && null symFalse ->
[ PP.pretty (unwords
[ "No overrides had any single concretely or"
, "symbolically failing preconditions."
])
]
| otherwise -> []
, if | simVerbose opts < 3 ->
[ PP.pretty $ unwords
[ "Run SAW with --sim-verbose=3 to see a description"
, "of each override."
]
]
| otherwise ->
[ PP.vcat
[ "Here are the descriptions of each override:"
, bullets '-'
(branches ^.. each . owpMethodSpec . to MS.ppMethodSpec)
]
]
]
in ( W4.truePred sym
, liftIO $ do
-- Now that we're failing, do the additional work of figuring out
-- if any overrides had symbolically false preconditions
symFalse <- catMaybes <$> (forM unknown $ \owp ->
findFalsePreconditions bak owp <&>
\case
[] -> Nothing
ps -> Just (owp, ps))
prettyArgs <-
ppArgs sym cc (NE.head css) (Crucible.RegMap args)
unsat <-
filterM
(unsatPreconditions bak (owpPreconditions . each . _2 . W4.labeledPred))
branches
Crucible.addFailedAssertion bak
(Crucible.GenericSimError (e prettyArgs symFalse unsat))
, Just (W4.plSourceLoc call_loc)
)
]))
(Crucible.RegMap args)
liftIO $ printOutLn opts Info $ unwords ["Applied override!", fnName]
return res
------------------------------------------------------------------------
-- | Use a method spec to override the behavior of a function.
-- This function computes the pre-state portion of the override,
-- which involves reading values from arguments and memory and computing
-- substitutions for the setup value variables, and computing precondition
-- predicates.
methodSpecHandler_prestate ::
forall arch ctx.
( ?lc :: Crucible.TypeContext
, ?memOpts::Crucible.MemOptions
, ?w4EvalTactic :: W4EvalTactic
, ?checkAllocSymInit :: Bool
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
Options {- ^ output/verbosity options -} ->
SharedContext {- ^ context for constructing SAW terms -} ->
LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} ->
Ctx.Assignment (Crucible.RegEntry Sym) ctx
{- ^ the arguments to the function -} ->
MS.CrucibleMethodSpecIR (LLVM arch) {- ^ specification for current function override -} ->
OverrideMatcher (LLVM arch) RO ()
methodSpecHandler_prestate opts sc cc args cs =
do let expectedArgTypes = Map.elems (cs ^. MS.csArgBindings)
sym <- Ov.getSymInterface
let aux (memTy, setupVal) (Crucible.AnyValue tyrep val) =
do storTy <- Crucible.toStorableType memTy
pmv <- Crucible.packMemValue sym storTy tyrep val
return (pmv, memTy, setupVal)
-- todo: fail if list lengths mismatch
xs <- liftIO (zipWithM aux expectedArgTypes (assignmentToList args))
let md = MS.ConditionMetadata
{ MS.conditionLoc = cs ^. MS.csLoc
, MS.conditionTags = mempty -- TODO? should `execute_func` track tags?
, MS.conditionType = "formal argument matching"
, MS.conditionContext = ""
}
sequence_ [ matchArg opts sc cc cs PreState md x y z | (x, y, z) <- xs]
learnCond opts sc cc cs PreState (cs ^. MS.csGlobalAllocs) Map.empty (cs ^. MS.csPreState)
-- | Use a method spec to override the behavior of a function.
-- This function computes the post-state portion of the override,
-- which involves writing values into memory, computing the return value,
-- and computing postcondition predicates.
methodSpecHandler_poststate ::
forall arch ret.
( ?lc :: Crucible.TypeContext
, ?memOpts :: Crucible.MemOptions
, ?w4EvalTactic :: W4EvalTactic
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
Options {- ^ output/verbosity options -} ->
SharedContext {- ^ context for constructing SAW terms -} ->
LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} ->
Crucible.TypeRepr ret {- ^ type representation of function return value -} ->
MS.CrucibleMethodSpecIR (LLVM arch) {- ^ specification for current function override -} ->
OverrideMatcher (LLVM arch) RW (Crucible.RegValue Sym ret)
methodSpecHandler_poststate opts sc cc retTy cs =
do executeCond opts sc cc cs (cs ^. MS.csPostState)
computeReturnValue opts cc sc cs retTy (cs ^. MS.csRetValue)
-- learn pre/post condition
learnCond ::
( ?lc :: Crucible.TypeContext
, ?memOpts::Crucible.MemOptions
, ?w4EvalTactic :: W4EvalTactic
, ?checkAllocSymInit :: Bool
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
Options ->
SharedContext ->
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
PrePost ->
[MS.AllocGlobal (LLVM arch)] ->
Map AllocIndex (MS.AllocSpec (LLVM arch)) ->
MS.StateSpec (LLVM arch) ->
OverrideMatcher (LLVM arch) md ()
learnCond opts sc cc cs prepost globals extras ss =
do let loc = cs ^. MS.csLoc
matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos)
traverse_ (learnSetupCondition opts sc cc cs prepost) (ss ^. MS.csConditions)
assertTermEqualities sc cc
enforcePointerValidity sc cc ss
enforceDisjointness sc cc loc globals extras ss
enforceCompleteSubstitution loc ss
assertTermEqualities ::
(?w4EvalTactic :: W4EvalTactic) =>
SharedContext ->
LLVMCrucibleContext arch ->
OverrideMatcher (LLVM arch) md ()
assertTermEqualities sc cc = do
let assertTermEquality (t, md, e) = do
p <- instantiateExtResolveSAWPred sc cc t
addAssert p md e
traverse_ assertTermEquality =<< OM (use termEqs)
-- execute a pre/post condition
executeCond :: ( ?lc :: Crucible.TypeContext
, ?memOpts :: Crucible.MemOptions
, ?w4EvalTactic :: W4EvalTactic
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
)
=> Options
-> SharedContext
-> LLVMCrucibleContext arch
-> MS.CrucibleMethodSpecIR (LLVM arch)
-> MS.StateSpec (LLVM arch)
-> OverrideMatcher (LLVM arch) RW ()
executeCond opts sc cc cs ss = do
refreshTerms sc ss
traverse_ (executeAllocation opts sc cc) (Map.assocs (ss ^. MS.csAllocs))
overwritten_allocs <- invalidateMutableAllocs opts sc cc cs
traverse_
(executePointsTo opts sc cc cs overwritten_allocs)
(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
-- override's precondition are allocated, and meet the appropriate
-- requirements for alignment and mutability.
enforcePointerValidity ::
(?lc :: Crucible.TypeContext, ?memOpts::Crucible.MemOptions, ?w4EvalTactic :: W4EvalTactic, ?checkAllocSymInit :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
SharedContext ->
LLVMCrucibleContext arch ->
MS.StateSpec (LLVM arch) ->
OverrideMatcher (LLVM arch) md ()
enforcePointerValidity sc cc ss =
do sym <- Ov.getSymInterface
sub <- OM (use setupValueSub) -- Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch))
let allocs = view MS.csAllocs ss -- Map AllocIndex LLVMAllocSpec
let mems = Map.elems $ Map.intersectionWith (,) allocs sub
let w = Crucible.PtrWidth
let memVar = Crucible.llvmMemVar (ccLLVMContext cc)
mem <- readGlobal memVar
sequence_
[ do psz' <- instantiateExtResolveSAWSymBV sc cc Crucible.PtrWidth psz
c <-
liftIO $
Crucible.isAllocatedAlignedPointer sym w alignment mut ptr (Just psz') mem
let ploc = MS.conditionLoc allocMd
let msg =
"Pointer not valid:"
++ "\n base = " ++ show (Crucible.ppPtr ptr)
++ "\n size = " ++ showTerm psz
++ "\n required alignment = " ++ show (Crucible.fromAlignment alignment) ++ "-byte"
++ "\n required mutability = " ++ show mut
addAssert c allocMd $ Crucible.SimError ploc $
Crucible.AssertFailureSimError msg ""
case initialization of
LLVMAllocSpecSymbolicInitialization
| ?checkAllocSymInit ->
do maybeOk <- liftIO $ checkMemLoad sym mem ptr psz' alignment
let msg' = PP.vcat $ map (PP.pretty . unwords)
[ [ "Memory region not initialized:" ]
, [ " pointer =", show (Crucible.ppPtr ptr) ]
, [ " size =", showTerm psz ]
]
case maybeOk of
Just ok ->
addAssert ok allocMd $ Crucible.SimError (MS.conditionLoc allocMd) $
Crucible.AssertFailureSimError (show msg') ""
Nothing -> failure ploc (BadPointerLoad (Right msg') "")
_ -> return ()
| (LLVMAllocSpec mut _pty alignment psz allocMd fresh initialization, ptr) <- mems
, not fresh -- Fresh symbolic pointers are not assumed to be valid; don't check them
]
checkMemLoad ::
(?memOpts::Crucible.MemOptions, Crucible.IsSymInterface sym, Crucible.HasPtrWidth wptr, Crucible.HasLLVMAnn sym) =>
sym ->
Crucible.MemImpl sym ->
Crucible.LLVMPtr sym wptr ->
W4.SymBV sym wptr ->
Crucible.Alignment ->
IO (Maybe (W4.Pred sym))
checkMemLoad sym mem ptr sz align =
case BV.asNatural <$> W4.asBV sz of
Just n -> do
res <- Crucible.loadRaw sym mem ptr (Crucible.arrayType n $ Crucible.bitvectorType 1) align
case res of
Crucible.NoErr pred_ _val -> do
return $ Just pred_
_ -> return Nothing
Nothing -> do
maybe_allocation_array <- Crucible.asMemAllocationArrayStore sym Crucible.PtrWidth ptr (Crucible.memImplHeap mem)
case maybe_allocation_array of
Just (ok, _arr, _sz) -> return $ Just ok
Nothing -> return Nothing
------------------------------------------------------------------------
-- | Generate assertions that all of the memory allocations matched by
-- an override's precondition are disjoint. Read-only allocations are
-- allowed to alias other read-only allocations, however.
enforceDisjointness ::
(?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
SharedContext ->
LLVMCrucibleContext arch ->
W4.ProgramLoc ->
[MS.AllocGlobal (LLVM arch)] ->
-- | Additional allocations to check disjointness from (from prestate)
(Map AllocIndex (MS.AllocSpec (LLVM arch))) ->
MS.StateSpec (LLVM arch) ->
OverrideMatcher (LLVM arch) md ()
enforceDisjointness sc cc loc globals extras ss =
ccWithBackend cc $ \bak ->
do let sym = backendGetSym bak
sub <- OM (use setupValueSub)
mem <- readGlobal $ Crucible.llvmMemVar $ ccLLVMContext cc
-- every csAllocs entry should be present in sub
let mems = Map.elems $ Map.intersectionWith (,) (view MS.csAllocs ss) sub
let mems2 = Map.elems $ Map.intersectionWith (,) extras sub
-- Ensure that all RW regions are disjoint from each other, and
-- that all RW regions are disjoint from all RO regions.
sequence_
[ enforceDisjointAllocSpec sc cc sym loc p q
| p : ps <- tails mems
, q <- ps ++ mems2
]
-- Ensure that all RW and RO regions are disjoint from mutable
-- global regions.
let resolveAllocGlobal g@(LLVMAllocGlobal _ nm) =
do ptr <- liftIO $ Crucible.doResolveGlobal bak mem nm
pure (g, ptr)
globals' <- traverse resolveAllocGlobal globals
sequence_
[ enforceDisjointAllocGlobal sym loc p q
| p <- mems
, q <- globals'
]
-- | Assert that two LLVM allocations are disjoint from each other, if
-- they need to be. If both allocations are read-only, then they need
-- not be disjoint. Similarly, fresh pointers need not be checked for
-- disjointness.
enforceDisjointAllocSpec ::
(?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
SharedContext ->
LLVMCrucibleContext arch ->
Sym ->
W4.ProgramLoc ->
(LLVMAllocSpec, LLVMPtr (Crucible.ArchWidth arch)) ->
(LLVMAllocSpec, LLVMPtr (Crucible.ArchWidth arch)) ->
OverrideMatcher (LLVM arch) md ()
enforceDisjointAllocSpec sc cc sym loc
(LLVMAllocSpec pmut _pty _palign psz pMd pfresh _p_sym_init, p)
(LLVMAllocSpec qmut _qty _qalign qsz qMd qfresh _q_sym_init, q)
| (pmut, qmut) == (Crucible.Immutable, Crucible.Immutable) =
pure () -- Read-only allocations may alias each other
| pfresh || qfresh =
pure () -- Fresh pointers need not be disjoint
| otherwise =
do liftIO $ W4.setCurrentProgramLoc sym (MS.conditionLoc pMd)
psz' <- instantiateExtResolveSAWSymBV sc cc Crucible.PtrWidth psz
liftIO $ W4.setCurrentProgramLoc sym (MS.conditionLoc qMd)
qsz' <- instantiateExtResolveSAWSymBV sc cc Crucible.PtrWidth qsz
liftIO $ W4.setCurrentProgramLoc sym loc
c <- liftIO $ Crucible.buildDisjointRegionsAssertion
sym Crucible.PtrWidth