-
Notifications
You must be signed in to change notification settings - Fork 63
/
Copy pathBuiltins.hs
2853 lines (2569 loc) · 111 KB
/
Builtins.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.Builtins
Description : Implementations of Crucible-related SAW-Script primitives.
License : BSD3
Maintainer : atomb
Stability : provisional
-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances, MultiParamTypeClasses#-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ParallelListComp #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module SAWScript.Crucible.LLVM.Builtins
( show_cfg
, llvm_execute_func
, llvm_return
, llvm_precond
, llvm_postcond
, llvm_assert
, llvm_cfg
, llvm_extract
, llvm_compositional_extract
, llvm_verify
, llvm_refine_spec
, llvm_array_size_profile
, llvm_setup_with_tag
, crucible_setup_val_to_typed_term
, llvm_spec_size
, llvm_spec_solvers
, llvm_ghost_value
, llvm_equal
, llvm_points_to
, llvm_conditional_points_to
, llvm_points_to_at_type
, llvm_conditional_points_to_at_type
, llvm_points_to_internal
, llvm_points_to_array_prefix
, llvm_points_to_bitfield
, llvm_fresh_pointer
, llvm_unsafe_assume_spec
, llvm_fresh_var
, llvm_fresh_cryptol_var
, llvm_alloc
, llvm_alloc_aligned
, llvm_alloc_readonly
, llvm_alloc_readonly_aligned
, llvm_alloc_with_size
, llvm_alloc_sym_init
, llvm_symbolic_alloc
, llvm_alloc_global
, llvm_fresh_expanded_val
, llvm_sizeof
, llvm_cast_pointer
--
-- These function are common to LLVM & JVM implementation (not for external use)
, setupArg
, setupArgs
, getGlobalPair
, runCFG
, baseCryptolType
, displayVerifExceptionOpts
, findDecl
, findDefMaybeStatic
, setupLLVMCrucibleContext
, setupPrestateConditions
, checkSpecReturnType
, verifyPrestate
, verifyPoststate
, getPoststateObligations
, withCfgAndBlockId
, registerOverride
, lookupMemGlobal
) where
import Prelude hiding (fail)
import qualified Control.Exception as X
import Control.Lens
import Control.Monad (foldM, forM, forM_, replicateM, unless, when)
import Control.Monad.Extra (findM, whenM)
import Control.Monad.Fail (MonadFail(..))
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Reader (runReaderT)
import Control.Monad.State (MonadState(..), StateT(..), execStateT, gets)
import Control.Monad.Trans.Class (MonadTrans(..))
import qualified Data.Bimap as Bimap
import Data.Char (isDigit)
import Data.Foldable (for_, toList, fold)
import Data.Function
import Data.Functor (void)
import Data.IORef
import Data.List
import Data.List.Extra (nubOrd)
import qualified Data.List.NonEmpty as NE
import Data.Maybe
import Data.String
import Data.Map (Map)
import qualified Data.Map as Map
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HashMap
import qualified Data.Set as Set
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Time.Clock (getCurrentTime, diffUTCTime)
import qualified Data.Vector as V
import Prettyprinter
import System.IO
import qualified Text.LLVM.AST as L
import Text.URI
import qualified Control.Monad.Trans.Maybe as MaybeT
-- parameterized-utils
import Data.Parameterized.Classes
import Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import qualified Data.Parameterized.Context as Ctx
-- cryptol
import qualified Cryptol.TypeCheck.Type as Cryptol
import qualified Cryptol.TypeCheck.PP as Cryptol
import qualified Verifier.SAW.Cryptol as Cryptol
-- what4
import qualified What4.Concrete as W4
import qualified What4.Config as W4
import qualified What4.FunctionName as W4
import qualified What4.LabeledPred as W4
import qualified What4.ProgramLoc as W4
import qualified What4.Interface as W4
import qualified What4.Expr.Builder as W4
-- crucible
import qualified Lang.Crucible.Backend as Crucible
import qualified Lang.Crucible.Backend.Online as Crucible
import qualified Lang.Crucible.CFG.Core as Crucible
import qualified Lang.Crucible.CFG.Extension as Crucible
(IsSyntaxExtension)
import qualified Lang.Crucible.FunctionHandle as Crucible
import qualified Lang.Crucible.Simulator as Crucible
import qualified Lang.Crucible.Simulator.Breakpoint as Crucible
import qualified Lang.Crucible.Simulator.GlobalState as Crucible
import qualified Lang.Crucible.Simulator.PathSatisfiability as Crucible
-- crucible-llvm
import qualified Lang.Crucible.LLVM.ArraySizeProfile as Crucible
import qualified Lang.Crucible.LLVM.DataLayout as Crucible
import qualified Lang.Crucible.LLVM.Bytes as Crucible
import qualified Lang.Crucible.LLVM.Functions as Crucible
import qualified Lang.Crucible.LLVM.Intrinsics as Crucible
import qualified Lang.Crucible.LLVM.MemModel as Crucible
import qualified Lang.Crucible.LLVM.MemType as Crucible
import qualified Lang.Crucible.LLVM.PrettyPrint as Crucible
import Lang.Crucible.LLVM.QQ( llvmOvr )
import qualified Lang.Crucible.LLVM.Translation as Crucible
import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible
-- parameterized-utils
import qualified Data.Parameterized.TraversableFC as Ctx
-- saw-core
import Verifier.SAW.FiniteValue (ppFirstOrderValue)
import Verifier.SAW.SharedTerm
import Verifier.SAW.TypedAST
import Verifier.SAW.Recognizer
import Verifier.SAW.Simulator.What4.ReturnTrip
-- cryptol-saw-core
import Verifier.SAW.TypedTerm
-- saw-script
import SAWScript.AST (Located(..))
import SAWScript.Builtins (ghost_value)
import SAWScript.Proof
import SAWScript.Prover.SolverStats
import SAWScript.Prover.Versions
import SAWScript.TopLevel
import SAWScript.Value
import SAWScript.Position
import SAWScript.Exceptions
import SAWScript.Options
import SAWScript.Utils (neGroupOn, neNubOrd)
import qualified SAWScript.Crucible.Common as Common
import SAWScript.Crucible.Common (Sym, SAWCruciblePersonality)
import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), nextAllocIndex, PrePost(..))
import qualified SAWScript.Crucible.Common.MethodSpec as MS
import SAWScript.Crucible.Common.MethodSpec (SetupValue(..))
import SAWScript.Crucible.Common.Override
import qualified SAWScript.Crucible.Common.Setup.Builtins as Setup
import qualified SAWScript.Crucible.Common.Setup.Type as Setup
import SAWScript.Crucible.LLVM.Override
import SAWScript.Crucible.LLVM.ResolveSetupValue
import SAWScript.Crucible.LLVM.MethodSpecIR
import SAWScript.Panic (panic)
type AssumptionReason = (MS.ConditionMetadata, String)
type MemImpl = Crucible.MemImpl Sym
data LLVMVerificationException
= MultipleStaticFunctions L.Symbol
| DefNotFound L.Symbol [L.Symbol]
| DeclNotFound L.Symbol [L.Symbol]
| SetupError SetupError
displayVerifExceptionOpts :: Options -> LLVMVerificationException -> String
displayVerifExceptionOpts _ (MultipleStaticFunctions (L.Symbol nm)) =
"Multiple non-equal definitions for `" ++ nm ++ "`."
displayVerifExceptionOpts opts (DefNotFound (L.Symbol nm) nms) =
unlines $
[ "Could not find definition for function named `" ++ nm ++ "`."
] ++ if simVerbose opts < 3
then [ "Run SAW with --sim-verbose=3 to see all function names" ]
else "Available function names:" : map ((" " ++) . show . Crucible.ppSymbol) nms
displayVerifExceptionOpts opts (DeclNotFound (L.Symbol nm) nms) =
unlines $
[ "Could not find declaration for function named `" ++ nm ++ "`."
] ++ if simVerbose opts < 3
then [ "Run SAW with --sim-verbose=3 to see all function names" ]
else "Available function names:" : map ((" " ++) . show . Crucible.ppSymbol) nms
displayVerifExceptionOpts _ (SetupError e) =
"Error during simulation setup: " ++ show (ppSetupError e)
show_cfg :: SAW_CFG -> String
show_cfg (LLVM_CFG (Crucible.AnyCFG cfg)) = show cfg
show_cfg (JVM_CFG (Crucible.AnyCFG cfg)) = show cfg
-- | Determines whether one LLVM symbol is equivalent to another except
-- for a numeric suffix. This can determine whether one symbol is the
-- disambiguated name of a duplicated static function.
matchingStatics :: L.Symbol -> L.Symbol -> Bool
matchingStatics (L.Symbol a) (L.Symbol b) = go a b
where
go [] [] = True
go (x:xs) (y:ys) = x == y && go xs ys
go [] ('.':ds) = all isDigit ds
go ('.':ds) [] = all isDigit ds
go _ _ = False
findDefMaybeStatic :: L.Module -> String -> Either LLVMVerificationException (NE.NonEmpty L.Define)
findDefMaybeStatic llmod nm =
case NE.nonEmpty (filter (\d -> matchingStatics (L.defName d) nm') (L.modDefines llmod)) of
Nothing -> Left $ DefNotFound nm' $ map L.defName $ L.modDefines llmod
Just defs -> Right defs
where
nm' = fromString nm
findDecl :: L.Module -> String -> Either LLVMVerificationException L.Declare
findDecl llmod nm =
case find (\d -> (L.decName d) == nm') (L.modDeclares llmod) of
Just decl -> Right decl
Nothing -> Left $ DeclNotFound nm' $ map L.decName $ L.modDeclares llmod
where
nm' = fromString nm
resolveSpecName :: String -> TopLevel (String, Maybe String)
resolveSpecName nm =
if Crucible.testBreakpointFunction nm
then
let (fnName, fnSuffix) = break (== '#') nm
parentName =
case fnSuffix of
_:parentName' -> parentName'
-- TODO: Give a proper error message here instead of panicking,
-- and document __breakpoint__ naming requirements. See #2097.
[] -> panic "resolveSpecName"
[ "__breakpoint__ function not followed by #<parent_name>"
, "See https://github.com/GaloisInc/saw-script/issues/2097"
] in
return
( fnName
, Just parentName
)
else return (nm, Nothing)
llvm_verify ::
Some LLVMModule ->
String ->
[SomeLLVM MS.ProvedSpec] ->
Bool ->
LLVMCrucibleSetupM () ->
ProofScript () ->
TopLevel (SomeLLVM MS.ProvedSpec)
llvm_verify (Some lm) nm lemmas checkSat setup tactic =
do start <- io getCurrentTime
lemmas' <- checkModuleCompatibility lm lemmas
withMethodSpec checkSat lm nm setup $ \cc method_spec ->
do (stats, vcs, _) <- verifyMethodSpec cc method_spec lemmas' checkSat tactic Nothing
let lemmaSet = Set.fromList (map (view MS.psSpecIdent) lemmas')
end <- io getCurrentTime
let diff = diffUTCTime end start
ps <- io (MS.mkProvedSpec MS.SpecProved method_spec stats vcs lemmaSet diff)
returnProof $ SomeLLVM ps
llvm_refine_spec ::
Some LLVMModule ->
String ->
[SomeLLVM MS.ProvedSpec] ->
LLVMCrucibleSetupM () ->
ProofScript () ->
TopLevel (SomeLLVM MS.ProvedSpec)
llvm_refine_spec (Some lm) nm lemmas setup tactic =
do start <- io getCurrentTime
lemmas' <- checkModuleCompatibility lm lemmas
withMethodSpec False lm nm setup $ \cc method_spec ->
do (stats, deps) <- refineMethodSpec cc method_spec lemmas' tactic
let lemmaSet = Set.fromList (map (view MS.psSpecIdent) lemmas')
end <- io getCurrentTime
let diff = diffUTCTime end start
ps <- io (MS.mkProvedSpec MS.SpecProved method_spec stats deps lemmaSet diff)
returnProof $ SomeLLVM ps
llvm_unsafe_assume_spec ::
Some LLVMModule ->
String {- ^ Name of the function -} ->
LLVMCrucibleSetupM () {- ^ Boundary specification -} ->
TopLevel (SomeLLVM MS.ProvedSpec)
llvm_unsafe_assume_spec (Some lm) nm setup =
withMethodSpec False lm nm setup $ \_ method_spec ->
do printOutLnTop Info $
unwords ["Assume override", (method_spec ^. csName)]
ps <- io (MS.mkProvedSpec MS.SpecAdmitted method_spec mempty mempty mempty 0)
returnProof $ SomeLLVM ps
llvm_array_size_profile ::
ProofScript () ->
Some LLVMModule ->
String ->
[SomeLLVM MS.ProvedSpec] ->
LLVMCrucibleSetupM () ->
TopLevel [(String, [Crucible.FunctionProfile])]
llvm_array_size_profile assume (Some lm) nm lemmas setup = do
cell <- io $ newIORef (Map.empty :: Map Text.Text [Crucible.FunctionProfile])
lemmas' <- checkModuleCompatibility lm lemmas
withMethodSpec False lm nm setup $ \cc ms -> do
void . verifyMethodSpec cc ms lemmas' True assume $ Just cell
profiles <- io $ readIORef cell
pure . fmap (\(fnm, prof) -> (Text.unpack fnm, prof)) $ Map.toList profiles
llvmURI :: String -> URI
llvmURI symbol_name =
fromMaybe (error $ unwords ["mkLLVMName", "Could not create LLVM symbol name", symbol_name]) $
do sch <- mkScheme "llvm"
p <- mkPathPiece (Text.pack symbol_name)
pure URI
{ uriScheme = Just sch
, uriAuthority = Left True -- absolute path
, uriPath = Just (False, p NE.:| [])
, uriQuery = []
, uriFragment = Nothing
}
llvmNameInfo :: String -> NameInfo
llvmNameInfo symbol_name = ImportedName (llvmURI symbol_name) [ Text.pack symbol_name ]
llvm_compositional_extract ::
Some LLVMModule ->
String ->
String ->
[SomeLLVM MS.ProvedSpec] ->
Bool {- ^ check sat -} ->
LLVMCrucibleSetupM () ->
ProofScript () ->
TopLevel (SomeLLVM MS.ProvedSpec)
llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic =
do start <- io getCurrentTime
lemmas' <- checkModuleCompatibility lm lemmas
withMethodSpec checkSat lm nm setup $ \cc method_spec ->
do let value_input_parameters = mapMaybe
(\(_, setup_value) -> setupValueAsExtCns setup_value)
(Map.elems $ method_spec ^. MS.csArgBindings)
let reference_input_parameters = mapMaybe
(\case
LLVMPointsTo _ _ _ setup_value -> llvmPointsToValueAsExtCns setup_value
LLVMPointsToBitfield _ _ _ val -> setupValueAsExtCns val)
(method_spec ^. MS.csPreState ^. MS.csPointsTos)
let input_parameters = nub $ value_input_parameters ++ reference_input_parameters
let pre_free_variables = Map.fromList $
map (\x -> (tecExt x, x)) $ method_spec ^. MS.csPreState ^. MS.csFreshVars
let unsupported_input_parameters = Set.difference
(Map.keysSet pre_free_variables)
(Set.fromList input_parameters)
when (not $ Set.null unsupported_input_parameters) $
fail $ unlines
[ "Unsupported input parameters:"
, show unsupported_input_parameters
, "An input parameter must be bound by llvm_execute_func or llvm_points_to."
]
let return_output_parameter =
case method_spec ^. MS.csRetValue of
Just setup_value -> setupValueAsExtCns setup_value
Nothing -> Nothing
let reference_output_parameters =
mapMaybe
(\case
LLVMPointsTo _ _ _ setup_value -> llvmPointsToValueAsExtCns setup_value
LLVMPointsToBitfield _ _ _ val -> setupValueAsExtCns val)
(method_spec ^. MS.csPostState ^. MS.csPointsTos)
let output_parameters =
nub $ filter (isNothing . (Map.!?) pre_free_variables) $
maybeToList return_output_parameter ++ reference_output_parameters
let post_free_variables =
Map.fromList $
map (\x -> (tecExt x, x)) $ method_spec ^. MS.csPostState ^. MS.csFreshVars
let unsupported_output_parameters =
Set.difference (Map.keysSet post_free_variables) (Set.fromList output_parameters)
when (not $ Set.null unsupported_output_parameters) $
fail $ unlines
[ "Unsupported output parameters:"
, show unsupported_output_parameters
, "An output parameter must be bound by llvm_return or llvm_points_to."
]
(stats, vcs, post_override_state) <-
verifyMethodSpec cc method_spec lemmas' checkSat tactic Nothing
shared_context <- getSharedContext
let output_values =
map (((Map.!) $ post_override_state ^. termSub) . ecVarIndex) output_parameters
extracted_func <-
io $ scAbstractExts shared_context input_parameters
=<< scTuple shared_context output_values
when ([] /= getAllExts extracted_func) $
fail "Non-functional simulation summary."
let nmi = llvmNameInfo func_name
extracted_func_const <-
io $ scConstant' shared_context nmi extracted_func
=<< scTypeOf shared_context extracted_func
input_terms <- io $ traverse (scExtCns shared_context) input_parameters
applied_extracted_func <- io $ scApplyAll shared_context extracted_func_const input_terms
applied_extracted_func_selectors <-
io $ forM [1 .. (length output_parameters)] $ \i ->
mkTypedTerm shared_context
=<< scTupleSelector shared_context applied_extracted_func i (length output_parameters)
let output_parameter_substitution =
Map.fromList $
zip (map ecVarIndex output_parameters) (map ttTerm applied_extracted_func_selectors)
let substitute_output_parameters =
ttTermLens $ scInstantiateExt shared_context output_parameter_substitution
let setup_value_substitute_output_parameter setup_value
| SetupTerm term <- setup_value = SetupTerm <$> substitute_output_parameters term
| otherwise = return $ setup_value
let llvm_points_to_value_substitute_output_parameter = \case
ConcreteSizeValue val -> ConcreteSizeValue <$> setup_value_substitute_output_parameter val
SymbolicSizeValue arr sz ->
SymbolicSizeValue <$> substitute_output_parameters arr <*> substitute_output_parameters sz
extracted_ret_value <- liftIO $ mapM
setup_value_substitute_output_parameter
(method_spec ^. MS.csRetValue)
extracted_post_state_points_tos <- liftIO $ mapM
(\case
LLVMPointsTo x y z value ->
LLVMPointsTo x y z <$> llvm_points_to_value_substitute_output_parameter value
LLVMPointsToBitfield x y z value ->
LLVMPointsToBitfield x y z <$> setup_value_substitute_output_parameter value)
(method_spec ^. MS.csPostState ^. MS.csPointsTos)
let extracted_method_spec = method_spec &
MS.csRetValue .~ extracted_ret_value &
MS.csPostState . MS.csPointsTos .~ extracted_post_state_points_tos
typed_extracted_func_const <- io $ mkTypedTerm shared_context extracted_func_const
rw <- getTopLevelRW
rw' <-
liftIO $
extendEnv shared_context
(Located func_name func_name $ PosInternal "llvm_compositional_extract")
Nothing
Nothing
(VTerm typed_extracted_func_const)
rw
putTopLevelRW rw'
let lemmaSet = Set.fromList (map (view MS.psSpecIdent) lemmas')
end <- io getCurrentTime
let diff = diffUTCTime end start
ps <- io (MS.mkProvedSpec MS.SpecProved extracted_method_spec stats vcs lemmaSet diff)
returnProof (SomeLLVM ps)
setupValueAsExtCns :: SetupValue (LLVM arch) -> Maybe (ExtCns Term)
setupValueAsExtCns =
\case
SetupTerm term -> asExtCns $ ttTerm term
_ -> Nothing
llvmPointsToValueAsExtCns :: LLVMPointsToValue arch -> Maybe (ExtCns Term)
llvmPointsToValueAsExtCns =
\case
ConcreteSizeValue val -> setupValueAsExtCns val
SymbolicSizeValue arr _sz -> asExtCns $ ttTerm arr
-- | Check that all the overrides/lemmas were actually from this module
checkModuleCompatibility ::
LLVMModule arch ->
[SomeLLVM MS.ProvedSpec] ->
TopLevel [MS.ProvedSpec (LLVM arch)]
checkModuleCompatibility llvmModule = foldM step []
where
step accum (SomeLLVM lemma) =
case testEquality (lemma ^. MS.psSpec.MS.csCodebase) llvmModule of
Nothing -> throwTopLevel $ unlines
[ "Failed to apply an override that was verified against a"
, "different LLVM module"
]
Just Refl -> pure (lemma:accum)
-- -- | The real work of 'llvm_verify' and 'llvm_unsafe_assume_spec'.
withMethodSpec ::
Bool {- ^ path sat -} ->
LLVMModule arch ->
String {- ^ Name of the function -} ->
LLVMCrucibleSetupM () {- ^ Boundary specification -} ->
(( ?lc :: Crucible.TypeContext
, ?memOpts::Crucible.MemOptions
, ?w4EvalTactic :: W4EvalTactic
, ?checkAllocSymInit :: Bool
, ?singleOverrideSpecialCase :: Bool
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
TopLevel a) ->
TopLevel a
withMethodSpec pathSat lm nm setup action =
do (nm', parent) <- resolveSpecName nm
let edef = findDefMaybeStatic (modAST lm) nm'
let edecl = findDecl (modAST lm) nm'
let mtrans = modTrans lm
opts <- getOptions
defOrDecls <-
case (edef, edecl) of
(Right defs, _) -> return (NE.map Left defs)
(_, Right decl) -> return (Right decl NE.:| [])
(Left err, Left _) -> throwTopLevel (displayVerifExceptionOpts opts err)
let ?lc = mtrans ^. Crucible.transContext . Crucible.llvmTypeCtx
sosp <- rwSingleOverrideSpecialCase <$> getTopLevelRW
let ?singleOverrideSpecialCase = sosp
Crucible.llvmPtrWidth (mtrans ^. Crucible.transContext) $ \_ ->
fmap NE.head $ forM defOrDecls $ \defOrDecl ->
setupLLVMCrucibleContext pathSat lm $ \cc ->
do let sym = cc^.ccSym
pos <- getPosition
let setupLoc = toW4Loc "_SAW_verify_prestate" pos
let est0 =
case defOrDecl of
Left def -> initialCrucibleSetupState cc def setupLoc parent
Right decl -> initialCrucibleSetupStateDecl cc decl setupLoc parent
st0 <- either (throwTopLevel . show . ppSetupError) return est0
-- execute commands of the method spec
io $ W4.setCurrentProgramLoc sym setupLoc
methodSpec <-
view Setup.csMethodSpec <$>
(execStateT
(runReaderT (runLLVMCrucibleSetupM setup)
(Setup.makeCrucibleSetupRO))
st0)
io $ checkSpecArgumentTypes cc methodSpec
io $ checkSpecReturnType cc methodSpec
action cc methodSpec
verifyMethodSpec ::
( ?lc :: Crucible.TypeContext
, ?memOpts::Crucible.MemOptions
, ?w4EvalTactic :: W4EvalTactic
, ?checkAllocSymInit :: Bool
, ?singleOverrideSpecialCase :: Bool
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
[MS.ProvedSpec (LLVM arch)] ->
Bool ->
ProofScript () ->
Maybe (IORef (Map Text.Text [Crucible.FunctionProfile])) ->
TopLevel (SolverStats, [MS.VCStats], OverrideState (LLVM arch))
verifyMethodSpec cc methodSpec lemmas checkSat tactic asp =
ccWithBackend cc $ \bak ->
do printOutLnTop Info $
unwords ["Verifying", (methodSpec ^. csName) , "..."]
let sym = cc^.ccSym
profFile <- rwProfilingFile <$> getTopLevelRW
(writeFinalProfile, pfs) <- io $ Common.setupProfiling sym "llvm_verify" profFile
-- set up the metadata map for tracking proof obligation metadata
mdMap <- io $ newIORef mempty
-- set up the LLVM memory with a pristine heap
let globals = cc^.ccLLVMGlobals
let mvar = Crucible.llvmMemVar (ccLLVMContext cc)
let mem0 = lookupMemGlobal mvar globals
-- push a memory stack frame if starting from a breakpoint
let mem = case methodSpec^.csParentName of
Just parent -> mem0
{ Crucible.memImplHeap = Crucible.pushStackFrameMem
(Text.pack $ mconcat [methodSpec ^. csName, "#", parent])
(Crucible.memImplHeap mem0)
}
Nothing -> mem0
let globals1 = Crucible.llvmGlobals mvar mem
-- construct the initial state for verifications
opts <- getOptions
(args, assumes, env, globals2) <-
io $ verifyPrestate opts cc methodSpec globals1
when (detectVacuity opts)
$ checkAssumptionsForContradictions cc methodSpec tactic assumes
-- save initial path conditions
frameIdent <- io $ Crucible.pushAssumptionFrame bak
-- run the symbolic execution
printOutLnTop Info $
unwords ["Simulating", (methodSpec ^. csName) , "..."]
top_loc <- toW4Loc "llvm_verify" <$> getPosition
(ret, globals3, invSubst) <-
verifySimulate opts cc pfs methodSpec args assumes top_loc lemmas globals2 checkSat asp mdMap
-- collect the proof obligations
(asserts, post_override_state) <-
verifyPoststate cc
methodSpec env globals3 ret
mdMap
invSubst
-- restore previous assumption state
_ <- io $ Crucible.popAssumptionFrame bak frameIdent
-- attempt to verify the proof obligations
printOutLnTop Info $
unwords ["Checking proof obligations", (methodSpec ^. csName), "..."]
(stats, vcstats) <- verifyObligations cc methodSpec tactic assumes asserts
io $ writeFinalProfile
return ( stats
, vcstats
, post_override_state
)
refineMethodSpec ::
( ?lc :: Crucible.TypeContext
, ?memOpts::Crucible.MemOptions
, ?w4EvalTactic :: W4EvalTactic
, ?checkAllocSymInit :: Bool
, ?singleOverrideSpecialCase :: Bool
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
[MS.ProvedSpec (LLVM arch)] ->
ProofScript () ->
TopLevel (SolverStats, [MS.VCStats])
refineMethodSpec cc methodSpec lemmas tactic =
ccWithBackend cc $ \bak ->
do let sym = cc^.ccSym
let fnm = methodSpec ^. MS.csMethod
let isRelevant lemma_spec =
lemma_spec ^. MS.csMethod == fnm
let (relevantLemmas, irrelevantLemmas) =
partition isRelevant (map (view MS.psSpec) lemmas)
relevantLemmas' <-
case relevantLemmas of
[] -> fail $ unlines $
[ "No relevant overrides included in specification refinement for " ++ show (pretty fnm) ] ++
(if null irrelevantLemmas then [] else [ "Overrides provided for irrelevant methods:" ]) ++
[ " * " ++ show (pretty nm)
| nm <- nubOrd $ map (view MS.csMethod) $ irrelevantLemmas
]
(x:xs) -> return (x NE.:| xs)
printOutLnTop Info $
unwords ["Refining specification for", (methodSpec ^. csName) , "..."]
unless (null irrelevantLemmas) $
printOutLnTop Warn $ unlines $
[ "Irrelevant overrides included in specification refinement for " ++ show (pretty fnm) ] ++
[ " * " ++ show (pretty nm)
| nm <- nubOrd $ map (view MS.csMethod) $ irrelevantLemmas
]
profFile <- rwProfilingFile <$> getTopLevelRW
(writeFinalProfile, pfs) <- io $ Common.setupProfiling sym "llvm_refine_spec" profFile
-- set up the metadata map for tracking proof obligation metadata
mdMap <- io $ newIORef mempty
-- set up the LLVM memory with a pristine heap
let globals = cc^.ccLLVMGlobals
let mvar = Crucible.llvmMemVar (ccLLVMContext cc)
let mem = lookupMemGlobal mvar globals
let globals1 = Crucible.llvmGlobals mvar mem
-- construct the initial state for verifications
opts <- getOptions
(args, assumes, env, globals2) <-
io $ verifyPrestate opts cc methodSpec globals1
when (detectVacuity opts)
$ checkAssumptionsForContradictions cc methodSpec tactic assumes
-- save initial path conditions
frameIdent <- io $ Crucible.pushAssumptionFrame bak
-- run the symbolic execution
top_loc <- toW4Loc "llvm_refine_spec" <$> getPosition
(ret, globals3) <-
io $ refineSimulate opts cc pfs methodSpec args assumes top_loc relevantLemmas' globals2 mdMap
-- collect the proof obligations
(asserts, _post_override_state) <-
verifyPoststate cc
methodSpec env globals3 ret
mdMap
MapF.empty
-- restore previous assumption state
_ <- io $ Crucible.popAssumptionFrame bak frameIdent
-- attempt to verify the proof obligations
printOutLnTop Info $
unwords ["Checking proof obligations", (methodSpec ^. csName), "..."]
(stats, vcstats) <- verifyObligations cc methodSpec tactic assumes asserts
io $ writeFinalProfile
return ( stats
, vcstats
)
verifyObligations :: LLVMCrucibleContext arch
-> MS.CrucibleMethodSpecIR (LLVM arch)
-> ProofScript ()
-> [Crucible.LabeledPred Term AssumptionReason]
-> [(String, MS.ConditionMetadata, Term)]
-> TopLevel (SolverStats, [MS.VCStats])
verifyObligations cc mspec tactic assumes asserts =
do let sym = cc^.ccSym
st <- io $ Common.sawCoreState sym
let sc = saw_ctx st
useSequentGoals <- rwSequentGoals <$> getTopLevelRW
let assumeTerms = toListOf (folded . Crucible.labeledPred) assumes
assume <- io $ scAndList sc assumeTerms
let nm = mspec ^. csName
outs <-
forM (zip [(0::Int)..] asserts) $ \(n, (msg, md, assert)) ->
do goal <- io $ scImplies sc assume assert
goal' <- io $ boolToProp sc [] goal
sqt <- if useSequentGoals then
io $ booleansToSequent sc assumeTerms [assert]
else
return (propToSequent goal')
let ploc = MS.conditionLoc md
let gloc = (unwords [show (W4.plSourceLoc ploc)
,"in"
, show (W4.plFunction ploc)]) ++
(if null (MS.conditionContext md) then [] else
"\n" ++ MS.conditionContext md)
let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"]
proofgoal = ProofGoal
{ goalNum = n
, goalType = MS.conditionType md
, goalName = nm
, goalLoc = gloc
, goalDesc = msg
, goalSequent = sqt
, goalTags = MS.conditionTags md
}
res <- runProofScript tactic goal' proofgoal (Just ploc)
(Text.unwords
["LLVM verification condition", Text.pack (show n), Text.pack goalname])
False -- do not record this theorem in the database
useSequentGoals
case res of
ValidProof stats thm ->
return (stats, MS.VCStats md stats (thmSummary thm) (thmNonce thm) (thmDepends thm) (thmElapsedTime thm))
UnfinishedProof pst ->
do printOutLnTop Info $ unwords ["Subgoal failed:", nm, msg]
throwTopLevel $ "Proof failed " ++ show (length (psGoals pst)) ++ " goals remaining."
InvalidProof stats vals _pst ->
do printOutLnTop Info $ unwords ["Subgoal failed:", nm, msg]
printOutLnTop Info (show stats)
printOutLnTop OnlyCounterExamples "----------Counterexample----------"
opts <- sawPPOpts <$> rwPPOpts <$> getTopLevelRW
if null vals then
printOutLnTop OnlyCounterExamples "<<All settings of the symbolic variables constitute a counterexample>>"
else
let showEC ec = Text.unpack (toShortName (ecName ec)) in
let showAssignment (ec, val) = " " ++ showEC ec ++ ": " ++ show (ppFirstOrderValue opts val) in
mapM_ (printOutLnTop OnlyCounterExamples . showAssignment) vals
printOutLnTop OnlyCounterExamples "----------------------------------"
throwTopLevel "Proof failed." -- Mirroring behavior of llvm_verify
printOutLnTop Info $ unwords ["Proof succeeded!", nm]
let stats = mconcat (map fst outs)
let vcstats = map snd outs
return (stats, vcstats)
throwMethodSpec :: MS.CrucibleMethodSpecIR (LLVM arch) -> String -> IO a
throwMethodSpec mspec msg = X.throw $ LLVMMethodSpecException (mspec ^. MS.csLoc) msg
-- | Check that the specified arguments have the expected types.
--
-- The expected types are inferred from the LLVM module.
checkSpecArgumentTypes ::
Crucible.HasPtrWidth (Crucible.ArchWidth arch) =>
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
IO ()
checkSpecArgumentTypes cc mspec = mapM_ resolveArg [0..(nArgs-1)]
where
nArgs = toInteger (length (mspec ^. MS.csArgs))
tyenv = MS.csAllocations mspec
nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames
nm = mspec^.csName
checkArgTy i mt mt' =
do b <- checkRegisterCompatibility mt mt'
unless b $
throwMethodSpec mspec $ unlines
[ "Type mismatch in argument " ++ show i ++ " when verifying " ++ show nm
, "Argument is declared with type: " ++ show mt
, "but provided argument has incompatible type: " ++ show mt'
, "Note: this may be because the signature of your " ++
"function changed during compilation. If using " ++
"Clang, check the signature in the disassembled " ++
".ll file."
]
resolveArg i =
case Map.lookup i (mspec ^. MS.csArgBindings) of
Just (mt, sv) -> do
mt' <- exceptToFail (typeOfSetupValue cc tyenv nameEnv sv)
checkArgTy i mt mt'
Nothing -> throwMethodSpec mspec $ unwords
["Argument", show i, "unspecified when verifying", show nm]
-- | Check that the specified return value has the expected type.
--
-- The expected type is inferred from the LLVM module.
--
-- TODO: generalize, put in Setup.Builtins
checkSpecReturnType ::
Crucible.HasPtrWidth (Crucible.ArchWidth arch) =>
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
IO ()
checkSpecReturnType cc mspec =
case (mspec ^. MS.csRetValue, mspec ^. MS.csRet) of
(Just _, Nothing) ->
throwMethodSpec mspec $ unlines
[ "Return value specified, but function " ++ mspec ^. csName ++
" has void return type"
]
(Just sv, Just retTy) ->
do retTy' <- exceptToFail $
typeOfSetupValue cc
(MS.csAllocations mspec) -- map allocation indices to allocations
(mspec ^. MS.csPreState . MS.csVarTypeNames) -- map alloc indices to var names
sv
-- This check is too lax, see saw-script#443
b <- checkRegisterCompatibility retTy retTy'
unless b $ throwMethodSpec mspec $ unlines
[ "Incompatible types for return value when verifying " ++ mspec^.csName
, "Expected: " ++ show retTy
, "but given value of type: " ++ show retTy'
]
(Nothing, _) -> return ()
-- | Evaluate the precondition part of a Crucible method spec:
--
-- * Allocate heap space for each 'llvm_alloc' statement.
--
-- * Record an equality precondition for each 'llvm_equal'
-- statement.
--
-- * Write to memory for each 'llvm_points_to' statement. (Writes
-- to already-initialized locations are transformed into equality
-- preconditions.)
--
-- * Evaluate the function arguments from the 'llvm_execute_func'
-- statement.
--
-- Returns a tuple of (arguments, preconditions, pointer values,
-- memory).
verifyPrestate ::
( ?memOpts :: Crucible.MemOptions
, ?w4EvalTactic :: W4EvalTactic
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
Options ->
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
Crucible.SymGlobalState Sym ->
IO ([(Crucible.MemType, LLVMVal)],
[Crucible.LabeledPred Term AssumptionReason],
Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)),
Crucible.SymGlobalState Sym)
verifyPrestate opts cc mspec globals =
do let ?lc = ccTypeCtx cc
let sym = cc^.ccSym
let prestateLoc = W4.mkProgramLoc "_SAW_verify_prestate" W4.InternalPos
liftIO $ W4.setCurrentProgramLoc sym prestateLoc
let lvar = Crucible.llvmMemVar (ccLLVMContext cc)
let mem = lookupMemGlobal lvar globals
-- Allocate LLVM memory for each 'llvm_alloc'
(env, mem') <- runStateT
(Map.traverseWithKey (doAlloc cc) (mspec ^. MS.csPreState . MS.csAllocs))
mem
mem'' <- setupGlobalAllocs cc mspec mem'
mem''' <- setupPrePointsTos mspec opts cc env (mspec ^. MS.csPreState . MS.csPointsTos) mem''
let globals1 = Crucible.insertGlobal lvar mem''' globals
(globals2,cs) <-
setupPrestateConditions mspec cc mem''' env globals1 (mspec ^. MS.csPreState . MS.csConditions)
args <- resolveArguments cc mem''' mspec env
return (args, cs, env, globals2)
-- | Checks for contradictions within the given list of assumptions, by asking
-- the solver about whether their conjunction entails falsehood.
assumptionsContainContradiction ::
(Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
ProofScript () ->
[Crucible.LabeledPred Term AssumptionReason] ->
TopLevel Bool
assumptionsContainContradiction cc methodSpec tactic assumptions =
do
let sym = cc^.ccSym
st <- io $ Common.sawCoreState sym
let sc = saw_ctx st
let ploc = methodSpec^.MS.csLoc
(goal',pgl) <- io $
do
-- conjunction of all assumptions
assume <- scAndList sc (toListOf (folded . Crucible.labeledPred) assumptions)
-- implies falsehood
goal <- scImplies sc assume =<< toSC sym st (W4.falsePred sym)