-
Notifications
You must be signed in to change notification settings - Fork 63
/
Copy pathWhat4.hs
1666 lines (1465 loc) · 57.5 KB
/
What4.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 : Verifier.SAW.Simulator.What4
-- Copyright : Galois, Inc. 2012-2015
-- License : BSD3
-- Maintainer : [email protected]
-- Stability : experimental
-- Portability : non-portable (language extensions)
--
-- A symbolic simulator for saw-core terms using What4.
-- (This module is derived from Verifier.SAW.Simulator.SBV)
------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds#-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
-- WithKnownNat
{-# OPTIONS_GHC -Wno-warnings-deprecations #-}
module Verifier.SAW.Simulator.What4
( w4Solve
, w4SolveBasic
, SymFnCache
, TypedExpr(..)
, SValue
, SPrim
, Labeler(..)
, w4Eval
, w4EvalAny
, w4EvalBasic
, getLabelValues
, w4SimulatorEval
, NeutralTermException(..)
, valueToSymExpr
, symExprToValue
) where
import qualified Control.Arrow as A
import Data.Bits
import Data.IORef
import Data.Kind (Type)
import Data.List (genericTake)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Text as Text
import Data.Vector (Vector)
import qualified Data.Vector as V
import Data.Traversable as T
#if !MIN_VERSION_base(4,8,0)
import Control.Applicative
#endif
import qualified Control.Exception as X
import Control.Monad.State as ST
import Numeric.Natural (Natural)
-- saw-core
import qualified Verifier.SAW.Recognizer as R
import qualified Verifier.SAW.Simulator as Sim
import qualified Verifier.SAW.Simulator.Prims as Prims
import Verifier.SAW.SATQuery
import Verifier.SAW.SharedTerm
import Verifier.SAW.Simulator.Value
import Verifier.SAW.FiniteValue (FirstOrderType(..), FirstOrderValue(..))
import Verifier.SAW.TypedAST (FieldName, ModuleMap, toShortName, ctorPrimName, identBaseName)
-- what4
import qualified What4.Expr.Builder as B
import What4.Expr.GroundEval
import What4.Interface(SymExpr,Pred,SymInteger, IsExpr,
IsExprBuilder,IsSymExprBuilder, BoundVar)
import qualified What4.Interface as W
import What4.BaseTypes
import qualified What4.SWord as SW
import What4.SWord (SWord(..))
-- parameterized-utils
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.Context (Assignment)
import Data.Parameterized.Some
-- saw-core-what4
import Verifier.SAW.Simulator.What4.PosNat
import Verifier.SAW.Simulator.What4.FirstOrder
import Verifier.SAW.Simulator.What4.Panic
import Verifier.SAW.Simulator.What4.ReturnTrip
---------------------------------------------------------------------
-- empty datatype to index (open) type families
-- for this backend
data What4 (sym :: Type)
-- | A What4 symbolic array where the domain and co-domain types do not appear
-- in the type
data SArray sym where
SArray ::
W.IsExpr (W.SymExpr sym) =>
W.SymArray sym (Ctx.EmptyCtx Ctx.::> itp) etp ->
SArray sym
-- type abbreviations for uniform naming
type SBool sym = Pred sym
type SInt sym = SymInteger sym
type instance EvalM (What4 sym) = IO
type instance VBool (What4 sym) = SBool sym
type instance VWord (What4 sym) = SWord sym
type instance VInt (What4 sym) = SInt sym
type instance VArray (What4 sym) = SArray sym
type instance Extra (What4 sym) = What4Extra sym
type SValue sym = Value (What4 sym)
type SPrim sym = Prims.Prim (What4 sym)
-- Constraint
type Sym sym = IsSymExprBuilder sym
---------------------------------------------------------------------
data What4Extra sym =
SStream (Natural -> IO (SValue sym)) (IORef (Map Natural (SValue sym)))
instance Show (What4Extra sym) where
show (SStream _ _) = "<SStream>"
---------------------------------------------------------------------
--
-- Basic primitive table for What4 data
--
prims :: forall sym.
Sym sym => sym -> Prims.BasePrims (What4 sym)
prims sym =
Prims.BasePrims
{ Prims.bpIsSymbolicEvaluator = True
, Prims.bpAsBool = W.asConstantPred
-- Bitvectors
, Prims.bpUnpack = SW.bvUnpackBE sym
, Prims.bpPack = SW.bvPackBE sym
, Prims.bpBvAt = \w i -> SW.bvAtBE sym w (toInteger i)
, Prims.bpBvLit = \l x -> SW.bvLit sym (toInteger l) x
, Prims.bpBvSize = swBvWidth
, Prims.bpBvJoin = SW.bvJoin sym
, Prims.bpBvSlice = \ a b -> SW.bvSliceBE sym (toInteger a) (toInteger b)
-- Conditionals
, Prims.bpMuxBool = W.itePred sym
, Prims.bpMuxWord = SW.bvIte sym
, Prims.bpMuxInt = W.intIte sym
, Prims.bpMuxArray = arrayIte sym
, Prims.bpMuxExtra = muxWhat4Extra sym
-- Booleans
, Prims.bpTrue = W.truePred sym
, Prims.bpFalse = W.falsePred sym
, Prims.bpNot = W.notPred sym
, Prims.bpAnd = W.andPred sym
, Prims.bpOr = W.orPred sym
, Prims.bpXor = W.xorPred sym
, Prims.bpBoolEq = W.isEq sym
-- Bitvector logical
, Prims.bpBvNot = SW.bvNot sym
, Prims.bpBvAnd = SW.bvAnd sym
, Prims.bpBvOr = SW.bvOr sym
, Prims.bpBvXor = SW.bvXor sym
-- Bitvector arithmetic
, Prims.bpBvNeg = SW.bvNeg sym
, Prims.bpBvAdd = SW.bvAdd sym
, Prims.bpBvSub = SW.bvSub sym
, Prims.bpBvMul = SW.bvMul sym
, Prims.bpBvUDiv = SW.bvUDiv sym
, Prims.bpBvURem = SW.bvURem sym
, Prims.bpBvSDiv = SW.bvSDiv sym
, Prims.bpBvSRem = SW.bvSRem sym
, Prims.bpBvLg2 = SW.bvLg2 sym
-- Bitvector comparisons
, Prims.bpBvEq = SW.bvEq sym
, Prims.bpBvsle = SW.bvsle sym
, Prims.bpBvslt = SW.bvslt sym
, Prims.bpBvule = SW.bvule sym
, Prims.bpBvult = SW.bvult sym
, Prims.bpBvsge = SW.bvsge sym
, Prims.bpBvsgt = SW.bvsgt sym
, Prims.bpBvuge = SW.bvuge sym
, Prims.bpBvugt = SW.bvugt sym
-- Bitvector shift/rotate
, Prims.bpBvRolInt = liftRotate sym (SW.bvRol sym)
, Prims.bpBvRorInt = liftRotate sym (SW.bvRor sym)
, Prims.bpBvShlInt = \z -> liftShift sym (bvShl sym z)
, Prims.bpBvShrInt = \z -> liftShift sym (bvShr sym z)
, Prims.bpBvRol = SW.bvRol sym
, Prims.bpBvRor = SW.bvRor sym
, Prims.bpBvShl = bvShl sym
, Prims.bpBvShr = bvShr sym
-- Bitvector misc
, Prims.bpBvPopcount = SW.bvPopcount sym
, Prims.bpBvCountLeadingZeros = SW.bvCountLeadingZeros sym
, Prims.bpBvCountTrailingZeros = SW.bvCountTrailingZeros sym
, Prims.bpBvForall = bvForall sym
-- Integer operations
, Prims.bpIntAbs = W.intAbs sym
, Prims.bpIntAdd = W.intAdd sym
, Prims.bpIntSub = W.intSub sym
, Prims.bpIntMul = W.intMul sym
, Prims.bpIntDiv = W.intDiv sym
, Prims.bpIntMod = W.intMod sym
, Prims.bpIntNeg = W.intNeg sym
, Prims.bpIntEq = W.intEq sym
, Prims.bpIntLe = W.intLe sym
, Prims.bpIntLt = W.intLt sym
, Prims.bpIntMin = intMin sym
, Prims.bpIntMax = intMax sym
-- Array operations
, Prims.bpArrayConstant = arrayConstant sym
, Prims.bpArrayLookup = arrayLookup sym
, Prims.bpArrayUpdate = arrayUpdate sym
, Prims.bpArrayEq = arrayEq sym
, Prims.bpArrayCopy = arrayCopy sym
, Prims.bpArraySet = arraySet sym
, Prims.bpArrayRangeEq = arrayRangeEq sym
}
constMap :: forall sym. Sym sym => sym -> Map Ident (SPrim sym)
constMap sym =
Map.union (Prims.constMap (prims sym)) $
Map.fromList
[
-- Shifts
("Prelude.bvShl" , bvShLOp sym)
, ("Prelude.bvShr" , bvShROp sym)
, ("Prelude.bvSShr", bvSShROp sym)
-- Integers
, ("Prelude.intToNat", intToNatOp sym)
, ("Prelude.natToInt", natToIntOp sym)
, ("Prelude.intToBv" , intToBvOp sym)
, ("Prelude.bvToInt" , bvToIntOp sym)
, ("Prelude.sbvToInt", sbvToIntOp sym)
-- Integers mod n
, ("Prelude.toIntMod" , toIntModOp)
, ("Prelude.fromIntMod", fromIntModOp sym)
, ("Prelude.intModEq" , intModEqOp sym)
, ("Prelude.intModAdd" , intModBinOp sym W.intAdd)
, ("Prelude.intModSub" , intModBinOp sym W.intSub)
, ("Prelude.intModMul" , intModBinOp sym W.intMul)
, ("Prelude.intModNeg" , intModUnOp sym W.intNeg)
-- Streams
, ("Prelude.MkStream", mkStreamOp)
, ("Prelude.streamGet", streamGetOp sym)
-- Misc
, ("Prelude.expByNat", Prims.expByNatOp (prims sym))
]
-----------------------------------------------------------------------
-- Implementation of constMap primitives
swBvWidth :: SWord sym -> Int
swBvWidth x
| w <= toInteger (maxBound :: Int) = fromInteger w
| otherwise = panic "swBvWidth" ["bitvector too long", show w]
where w = SW.bvWidth x
toBool :: SValue sym -> IO (SBool sym)
toBool (VBool b) = return b
toBool x = fail $ unwords ["Verifier.SAW.Simulator.What4.toBool", show x]
toWord :: forall sym.
Sym sym => sym -> SValue sym -> IO (SWord sym)
toWord _ (VWord w) = return w
toWord sym (VVector vv) = do
-- vec :: Vector (SBool sym))
vec1 <- T.traverse force vv
vec2 <- T.traverse toBool vec1
SW.bvPackBE sym vec2
toWord _ x = fail $ unwords ["Verifier.SAW.Simulator.What4.toWord", show x]
wordFun ::
Sym sym => sym -> (SWord sym -> SPrim sym) -> SPrim sym
wordFun sym = Prims.wordFun (SW.bvPackBE sym)
valueToSymExpr :: SValue sym -> Maybe (Some (W.SymExpr sym))
valueToSymExpr = \case
VBool b -> Just $ Some b
VInt i -> Just $ Some i
VWord (DBV w) -> Just $ Some w
VArray (SArray a) -> Just $ Some a
_ -> Nothing
symExprToValue ::
IsExpr (SymExpr sym) =>
W.BaseTypeRepr tp ->
W.SymExpr sym tp ->
Maybe (SValue sym)
symExprToValue tp expr = case tp of
BaseBoolRepr -> Just $ VBool expr
BaseIntegerRepr -> Just $ VInt expr
(BaseBVRepr w) -> Just $ withKnownNat w $ VWord $ DBV expr
(BaseArrayRepr (Ctx.Empty Ctx.:> _) _) -> Just $ VArray $ SArray expr
_ -> Nothing
--
-- Integer bit/vector conversions
--
-- primitive intToNat : Integer -> Nat;
-- intToNat x == max 0 x
intToNatOp :: forall sym. Sym sym => sym -> SPrim sym
intToNatOp sym =
Prims.intFun $ \i ->
Prims.Prim $
case W.asInteger i of
Just i'
| 0 <= i' -> pure (VNat (fromInteger i'))
| otherwise -> pure (VNat 0)
Nothing ->
do z <- W.intLit sym 0
pneg <- W.intLt sym i z
i' <- W.intIte sym pneg z i
pure (VIntToNat (VInt i'))
-- primitive natToInt :: Nat -> Integer;
natToIntOp :: forall sym. Sym sym => sym -> SPrim sym
natToIntOp sym =
Prims.natFun $ \n ->
Prims.Prim (VInt <$> W.intLit sym (toInteger n))
-- interpret bitvector as unsigned integer
-- primitive bvToInt : (n : Nat) -> Vec n Bool -> Integer;
bvToIntOp :: forall sym. Sym sym => sym -> SPrim sym
bvToIntOp sym =
Prims.constFun $
wordFun sym $ \v ->
Prims.Prim (VInt <$> SW.bvToInteger sym v)
-- interpret bitvector as signed integer
-- primitive sbvToInt : (n : Nat) -> Vec n Bool -> Integer;
sbvToIntOp :: forall sym. Sym sym => sym -> SPrim sym
sbvToIntOp sym =
Prims.constFun $
wordFun sym $ \v ->
Prims.Prim (VInt <$> SW.sbvToInteger sym v)
-- primitive intToBv : (n : Nat) -> Integer -> Vec n Bool;
intToBvOp :: forall sym. Sym sym => sym -> SPrim sym
intToBvOp sym =
Prims.natFun $ \n ->
Prims.intFun $ \(x :: SymInteger sym) ->
Prims.Prim (VWord <$> SW.integerToBV sym x n)
--
-- Shifts
--
-- | Shift left, shifting in copies of the given bit
bvShl :: IsExprBuilder sym => sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvShl sym z w i =
W.iteM SW.bvIte sym z
(do w' <- SW.bvNot sym w
SW.bvNot sym =<< SW.bvShl sym w' i)
(SW.bvShl sym w i)
-- | Shift right, shifting in copies of the given bit
bvShr :: IsExprBuilder sym => sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvShr sym z w i =
W.iteM SW.bvIte sym z
(do w' <- SW.bvNot sym w
SW.bvNot sym =<< SW.bvLshr sym w' i)
(SW.bvLshr sym w i)
liftShift :: IsExprBuilder sym =>
sym ->
(SWord sym -> SWord sym -> IO (SWord sym)) ->
SWord sym -> Integer -> IO (SWord sym)
liftShift sym f w i =
f w =<< SW.bvLit sym (SW.bvWidth w) (i `min` SW.bvWidth w)
liftRotate :: IsExprBuilder sym =>
sym ->
(SWord sym -> SWord sym -> IO (SWord sym)) ->
SWord sym -> Integer -> IO (SWord sym)
liftRotate sym f w i =
f w =<< SW.bvLit sym (SW.bvWidth w) (i `mod` SW.bvWidth w)
-- | op : (n : Nat) -> Vec n Bool -> Nat -> Vec n Bool
bvShiftOp :: Sym sym => sym ->
(SWord sym -> SWord sym -> IO (SWord sym)) ->
(SWord sym -> Integer -> IO (SWord sym)) -> SPrim sym
bvShiftOp sym bvOp natOp =
Prims.constFun $ -- additional argument? the size?
wordFun sym $ \x -> -- word to shift
Prims.strictFun $ \y -> -- amount to shift as a nat
Prims.Prim $
case y of
VNat i -> VWord <$> natOp x j
where j = toInteger i `min` SW.bvWidth x
VBVToNat _ v -> VWord <$> (bvOp x =<< toWord sym v)
_ -> error $ unwords ["Verifier.SAW.Simulator.What4.bvShiftOp", show y]
-- bvShl : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;
bvShLOp :: forall sym. Sym sym => sym -> SPrim sym
bvShLOp sym = bvShiftOp sym (SW.bvShl sym)
(liftShift sym (SW.bvShl sym))
-- bvShR : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;
bvShROp :: forall sym. Sym sym => sym -> SPrim sym
bvShROp sym = bvShiftOp sym (SW.bvLshr sym)
(liftShift sym (SW.bvLshr sym))
-- bvSShR : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;
bvSShROp :: forall sym. Sym sym => sym -> SPrim sym
bvSShROp sym = bvShiftOp sym (SW.bvAshr sym)
(liftShift sym (SW.bvAshr sym))
bvForall :: W.IsSymExprBuilder sym =>
sym -> Natural -> (SWord sym -> IO (Pred sym)) -> IO (Pred sym)
bvForall sym n f =
do let indexSymbol = W.safeSymbol "i"
case mkNatRepr n of
Some w
| Just LeqProof <- testLeq (knownNat @1) w ->
withKnownNat w $ do
i <- W.freshBoundVar sym indexSymbol $ W.BaseBVRepr w
body <- f . DBV $ W.varExpr sym i
W.forallPred sym i body
| otherwise -> f ZBV
--
-- missing integer operations
--
intMin :: (IsExprBuilder sym) => sym -> SInt sym -> SInt sym -> IO (SInt sym)
intMin sym i1 i2 = do
p <- W.intLt sym i1 i2
W.intIte sym p i1 i2
intMax :: (IsExprBuilder sym) => sym -> SInt sym -> SInt sym -> IO (SInt sym)
intMax sym i1 i2 = do
p <- W.intLt sym i1 i2
W.intIte sym p i2 i1
------------------------------------------------------------
-- Integers mod n
toIntModOp :: SPrim sym
toIntModOp =
Prims.natFun $ \n ->
Prims.intFun $ \x ->
Prims.PrimValue (VIntMod n x)
fromIntModOp :: IsExprBuilder sym => sym -> SPrim sym
fromIntModOp sym =
Prims.natFun $ \n ->
Prims.intModFun $ \x ->
Prims.Prim (VInt <$> (W.intMod sym x =<< W.intLit sym (toInteger n)))
intModEqOp :: IsExprBuilder sym => sym -> SPrim sym
intModEqOp sym =
Prims.natFun $ \n ->
Prims.intModFun $ \x ->
Prims.intModFun $ \y -> Prims.Prim $
do modulus <- W.intLit sym (toInteger n)
d <- W.intSub sym x y
r <- W.intMod sym d modulus
z <- W.intLit sym 0
VBool <$> W.intEq sym r z
intModBinOp ::
IsExprBuilder sym => sym ->
(sym -> SInt sym -> SInt sym -> IO (SInt sym)) -> SPrim sym
intModBinOp sym f =
Prims.natFun $ \n ->
Prims.intModFun $ \x ->
Prims.intModFun $ \y -> Prims.Prim
(VIntMod n <$> (normalizeIntMod sym n =<< f sym x y))
intModUnOp ::
IsExprBuilder sym => sym ->
(sym -> SInt sym -> IO (SInt sym)) -> SPrim sym
intModUnOp sym f =
Prims.natFun $ \n ->
Prims.intModFun $ \x ->
Prims.Prim (VIntMod n <$> (normalizeIntMod sym n =<< f sym x))
normalizeIntMod :: IsExprBuilder sym => sym -> Natural -> SInt sym -> IO (SInt sym)
normalizeIntMod sym n x =
case W.asInteger x of
Nothing -> return x
Just i -> W.intLit sym (i `mod` toInteger n)
------------------------------------------------------------
-- Stream operations
-- MkStream :: (a :: sort 0) -> (Nat -> a) -> Stream a;
mkStreamOp :: SPrim sym
mkStreamOp =
Prims.constFun $
Prims.strictFun $ \f -> Prims.Prim $
do r <- newIORef Map.empty
return $ VExtra (SStream (\n -> apply f (ready (VNat n))) r)
-- streamGet :: (a :: sort 0) -> Stream a -> Nat -> a;
streamGetOp :: forall sym. Sym sym => sym -> SPrim sym
streamGetOp sym =
Prims.tvalFun $ \tp ->
Prims.strictFun $ \xs ->
Prims.strictFun $ \ix ->
Prims.Prim $
case ix of
VNat n -> lookupSStream xs n
VBVToNat _ w ->
do ilv <- toWord sym w
selectV sym (lazyMux @sym (muxBVal sym tp)) ((2 ^ SW.bvWidth ilv) - 1) (lookupSStream xs) ilv
v -> panic "streamGetOp" ["Expected Nat value", show v]
lookupSStream :: SValue sym -> Natural -> IO (SValue sym)
lookupSStream (VExtra (SStream f r)) n = do
m <- readIORef r
case Map.lookup n m of
Just v -> return v
Nothing -> do v <- f n
writeIORef r (Map.insert n v m)
return v
lookupSStream _ _ = fail "expected Stream"
muxBVal :: forall sym. Sym sym =>
sym -> TValue (What4 sym) -> SBool sym -> SValue sym -> SValue sym -> IO (SValue sym)
muxBVal sym = Prims.muxValue (prims sym)
muxWhat4Extra :: forall sym. Sym sym =>
sym -> TValue (What4 sym) -> SBool sym -> What4Extra sym -> What4Extra sym -> IO (What4Extra sym)
muxWhat4Extra sym (VDataType (primName -> "Prelude.Stream") [TValue tp] [] ) c x y =
do let f i = do xi <- lookupSStream (VExtra x) i
yi <- lookupSStream (VExtra y) i
muxBVal sym tp c xi yi
r <- newIORef Map.empty
return (SStream f r)
muxWhat4Extra _ tp _ _ _ = panic "muxWhat4Extra" ["Type mismatch", show tp]
-- | Lifts a strict mux operation to a lazy mux
lazyMux :: (IsExpr (SymExpr sym)) =>
(SBool sym -> a -> a -> IO a) -> (SBool sym -> IO a -> IO a -> IO a)
lazyMux muxFn c tm fm =
case W.asConstantPred c of
Just True -> tm
Just False -> fm
Nothing -> do
t <- tm
f <- fm
muxFn c t f
-- selectV merger maxValue valueFn index returns valueFn v when index has value v
-- if index is greater than maxValue, it returns valueFn maxValue. Use the ite op from merger.
selectV :: forall sym b.
Sym sym =>
sym ->
(SBool sym -> IO b -> IO b -> IO b) -> Natural -> (Natural -> IO b) -> SWord sym -> IO b
selectV sym merger maxValue valueFn vx =
case SW.bvAsUnsignedInteger vx of
Just i -> valueFn (fromInteger i :: Natural)
Nothing -> impl (swBvWidth vx) 0
where
impl :: Int -> Natural -> IO b
impl _ x | x > maxValue || x < 0 = valueFn maxValue
impl 0 y = valueFn y
impl i y = do
p <- SW.bvAtBE sym vx (toInteger j)
merger p (impl j (y `setBit` j)) (impl j y) where j = i - 1
instance Show (SArray sym) where
show (SArray arr) = show $ W.printSymExpr arr
arrayConstant ::
W.IsSymExprBuilder sym =>
sym ->
TValue (What4 sym) ->
TValue (What4 sym) ->
SValue sym ->
IO (SArray sym)
arrayConstant sym ity _elTy elm
| Just (Some idx_repr) <- valueAsBaseType ity
, Just (Some elm_expr) <- valueToSymExpr elm =
SArray <$> W.constantArray sym (Ctx.Empty Ctx.:> idx_repr) elm_expr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayConstant" ["argument type mismatch"]
arrayLookup ::
W.IsSymExprBuilder sym =>
sym ->
SArray sym ->
SValue sym ->
IO (SValue sym)
arrayLookup sym arr idx
| SArray arr_expr <- arr
, Just (Some idx_expr) <- valueToSymExpr idx
, W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr <- W.exprType arr_expr
, Just Refl <- testEquality idx_repr (W.exprType idx_expr) = do
elm_expr <- W.arrayLookup sym arr_expr (Ctx.Empty Ctx.:> idx_expr)
maybe
(panic "Verifier.SAW.Simulator.What4.Panic.arrayLookup" ["argument type mismatch"])
return
(symExprToValue elm_repr elm_expr)
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayLookup" ["argument type mismatch"]
arrayUpdate ::
W.IsSymExprBuilder sym =>
sym ->
SArray sym ->
SValue sym ->
SValue sym ->
IO (SArray sym)
arrayUpdate sym arr idx elm
| SArray arr_expr <- arr
, Just (Some idx_expr) <- valueToSymExpr idx
, Just (Some elm_expr) <- valueToSymExpr elm
, W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr <- W.exprType arr_expr
, Just Refl <- testEquality idx_repr (W.exprType idx_expr)
, Just Refl <- testEquality elm_repr (W.exprType elm_expr) =
SArray <$> W.arrayUpdate sym arr_expr (Ctx.Empty Ctx.:> idx_expr) elm_expr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayUpdate" ["argument type mismatch"]
arrayCopy ::
W.IsSymExprBuilder sym =>
sym ->
SArray sym ->
SWord sym ->
SArray sym ->
SWord sym ->
SWord sym ->
IO (SArray sym)
arrayCopy sym dest_arr dest_idx src_arr src_idx len
| SArray dest_arr_expr <- dest_arr
, DBV dest_idx_expr <- dest_idx
, SArray src_arr_expr <- src_arr
, DBV src_idx_expr <- src_idx
, DBV len_expr <- len
, W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) _ <- W.exprType dest_arr_expr
, Just Refl <- testEquality (W.exprType dest_arr_expr) (W.exprType src_arr_expr)
, Just Refl <- testEquality idx_repr (W.exprType dest_idx_expr)
, Just Refl <- testEquality idx_repr (W.exprType src_idx_expr)
, Just Refl <- testEquality idx_repr (W.exprType len_expr) =
SArray <$> W.arrayCopy sym dest_arr_expr dest_idx_expr src_arr_expr src_idx_expr len_expr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayCopy" ["argument type mismatch"]
arraySet ::
W.IsSymExprBuilder sym =>
sym ->
SArray sym ->
SWord sym ->
SValue sym ->
SWord sym ->
IO (SArray sym)
arraySet sym arr idx elm len
| SArray arr_expr <- arr
, DBV idx_expr <- idx
, Just (Some elm_expr) <- valueToSymExpr elm
, DBV len_expr <- len
, W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr <- W.exprType arr_expr
, Just Refl <- testEquality idx_repr (W.exprType idx_expr)
, Just Refl <- testEquality idx_repr (W.exprType len_expr)
, Just Refl <- testEquality elm_repr (W.exprType elm_expr) =
SArray <$> W.arraySet sym arr_expr idx_expr elm_expr len_expr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arraySet" ["argument type mismatch"]
arrayRangeEq ::
W.IsSymExprBuilder sym =>
sym ->
SArray sym ->
SWord sym ->
SArray sym ->
SWord sym ->
SWord sym ->
IO (SBool sym)
arrayRangeEq sym x_arr x_idx y_arr y_idx len
| SArray x_arr_expr <- x_arr
, DBV x_idx_expr <- x_idx
, SArray y_arr_expr <- y_arr
, DBV y_idx_expr <- y_idx
, DBV len_expr <- len
, W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) _ <- W.exprType x_arr_expr
, Just Refl <- testEquality (W.exprType x_arr_expr) (W.exprType y_arr_expr)
, Just Refl <- testEquality idx_repr (W.exprType x_idx_expr)
, Just Refl <- testEquality idx_repr (W.exprType y_idx_expr)
, Just Refl <- testEquality idx_repr (W.exprType len_expr) =
W.arrayRangeEq sym x_arr_expr x_idx_expr y_arr_expr y_idx_expr len_expr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayRangeEq" ["argument type mismatch"]
arrayEq ::
W.IsSymExprBuilder sym =>
sym ->
SArray sym ->
SArray sym ->
IO (W.Pred sym)
arrayEq sym lhs_arr rhs_arr
| SArray lhs_arr_expr <- lhs_arr
, SArray rhs_arr_expr <- rhs_arr
, W.BaseArrayRepr (Ctx.Empty Ctx.:> lhs_idx_repr) lhs_elm_repr <- W.exprType lhs_arr_expr
, W.BaseArrayRepr (Ctx.Empty Ctx.:> rhs_idx_repr) rhs_elm_repr <- W.exprType rhs_arr_expr
, Just Refl <- testEquality lhs_idx_repr rhs_idx_repr
, Just Refl <- testEquality lhs_elm_repr rhs_elm_repr =
W.arrayEq sym lhs_arr_expr rhs_arr_expr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayEq" ["argument type mismatch"]
arrayIte ::
W.IsSymExprBuilder sym =>
sym ->
W.Pred sym ->
SArray sym ->
SArray sym ->
IO (SArray sym)
arrayIte sym cond lhs_arr rhs_arr
| SArray lhs_arr_expr <- lhs_arr
, SArray rhs_arr_expr <- rhs_arr
, W.BaseArrayRepr (Ctx.Empty Ctx.:> lhs_idx_repr) lhs_elm_repr <- W.exprType lhs_arr_expr
, W.BaseArrayRepr (Ctx.Empty Ctx.:> rhs_idx_repr) rhs_elm_repr <- W.exprType rhs_arr_expr
, Just Refl <- testEquality lhs_idx_repr rhs_idx_repr
, Just Refl <- testEquality lhs_elm_repr rhs_elm_repr =
SArray <$> W.arrayIte sym cond lhs_arr_expr rhs_arr_expr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayIte" ["argument type mismatch"]
----------------------------------------------------------------------
-- | A basic symbolic simulator/evaluator: interprets a saw-core Term as
-- a symbolic value
w4SolveBasic ::
forall sym. IsSymExprBuilder sym =>
sym ->
SharedContext ->
Map Ident (SPrim sym) {- ^ additional primitives -} ->
Map VarIndex (SValue sym) {- ^ bindings for ExtCns values -} ->
IORef (SymFnCache sym) {- ^ cache for uninterpreted function symbols -} ->
Set VarIndex {- ^ 'unints' Constants in this list are kept uninterpreted -} ->
Term {- ^ term to simulate -} ->
IO (SValue sym)
w4SolveBasic sym sc addlPrims ecMap ref unintSet t =
do m <- scGetModuleMap sc
let extcns (EC ix nm ty)
| Just v <- Map.lookup ix ecMap = return v
| otherwise = parseUninterpreted sym ref (mkUnintApp (Text.unpack (toShortName nm) ++ "_" ++ show ix)) ty
let uninterpreted ec
| Set.member (ecVarIndex ec) unintSet = Just (extcns ec)
| otherwise = Nothing
let neutral _ nt = fail ("w4SolveBasic: could not evaluate neutral term: " ++ show nt)
let primHandler pn msg env _tv =
fail $ unlines
[ "Could not evaluate primitive " ++ show (primName pn)
, "On argument " ++ show (length env)
, Text.unpack msg
]
cfg <- Sim.evalGlobal m (constMap sym `Map.union` addlPrims) extcns uninterpreted neutral primHandler
Sim.evalSharedTerm cfg t
----------------------------------------------------------------------
-- Uninterpreted function cache
data SymFnWrapper sym :: Ctx.Ctx BaseType -> Type where
SymFnWrapper :: !(W.SymFn sym args ret) -> SymFnWrapper sym (args Ctx.::> ret)
type SymFnCache sym = Map W.SolverSymbol (MapF (Assignment BaseTypeRepr) (SymFnWrapper sym))
lookupSymFn ::
W.SolverSymbol -> Assignment BaseTypeRepr args -> BaseTypeRepr ty ->
SymFnCache sym -> Maybe (W.SymFn sym args ty)
lookupSymFn s args ty cache =
do m <- Map.lookup s cache
SymFnWrapper fn <- MapF.lookup (Ctx.extend args ty) m
return fn
insertSymFn ::
W.SolverSymbol -> Assignment BaseTypeRepr args -> BaseTypeRepr ty ->
W.SymFn sym args ty -> SymFnCache sym -> SymFnCache sym
insertSymFn s args ty fn = Map.alter upd s
where
upd Nothing = Just (MapF.singleton (Ctx.extend args ty) (SymFnWrapper fn))
upd (Just m) = Just (MapF.insert (Ctx.extend args ty) (SymFnWrapper fn) m)
mkSymFn ::
forall sym args ret. (IsSymExprBuilder sym) =>
sym -> IORef (SymFnCache sym) ->
String -> Assignment BaseTypeRepr args -> BaseTypeRepr ret ->
IO (W.SymFn sym args ret)
mkSymFn sym ref nm args ret =
do let s = W.safeSymbol nm
cache <- readIORef ref
case lookupSymFn s args ret cache of
Just fn -> return fn
Nothing ->
do fn <- W.freshTotalUninterpFn sym s args ret
writeIORef ref (insertSymFn s args ret fn cache)
return fn
----------------------------------------------------------------------
-- Given a constant nm of (saw-core) type ty, construct an uninterpreted
-- constant with that type.
-- Importantly: The types of these uninterpreted values are *not*
-- limited to What4 BaseTypes or FirstOrderTypes.
parseUninterpreted ::
forall sym.
(IsSymExprBuilder sym) =>
sym -> IORef (SymFnCache sym) ->
UnintApp (SymExpr sym) ->
TValue (What4 sym) -> IO (SValue sym)
parseUninterpreted sym ref app ty =
case ty of
VPiType nm _ body
-> pure $ VFun nm $ \x ->
do x' <- force x
app' <- applyUnintApp sym app x'
t2 <- applyPiBody body (ready x')
parseUninterpreted sym ref app' t2
VBoolType
-> VBool <$> mkUninterpreted sym ref app BaseBoolRepr
VIntType
-> VInt <$> mkUninterpreted sym ref app BaseIntegerRepr
VIntModType n
-> VIntMod n <$> mkUninterpreted sym ref app BaseIntegerRepr
-- 0 width bitvector is a constant
VVecType 0 VBoolType
-> return $ VWord ZBV
VVecType n VBoolType
| Just (Some (PosNat w)) <- somePosNat n
-> (VWord . DBV) <$> mkUninterpreted sym ref app (BaseBVRepr w)
VVecType n ety
-> do xs <- sequence $
[ parseUninterpreted sym ref (suffixUnintApp ("_a" ++ show i) app) ety
| i <- [0 .. n-1] ]
return (VVector (V.fromList (map ready xs)))
VArrayType ity ety
| Just (Some idx_repr) <- valueAsBaseType ity
, Just (Some elm_repr) <- valueAsBaseType ety
-> (VArray . SArray) <$>
mkUninterpreted sym ref app (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr)
VUnitType
-> return VUnit
VPairType ty1 ty2
-> do x1 <- parseUninterpreted sym ref (suffixUnintApp "_L" app) ty1
x2 <- parseUninterpreted sym ref (suffixUnintApp "_R" app) ty2
return (VPair (ready x1) (ready x2))
VRecordType elem_tps
-> (VRecordValue <$>
mapM (\(f,tp) ->
(f,) <$> ready <$>
parseUninterpreted sym ref (suffixUnintApp ("_" ++ Text.unpack f) app) tp) elem_tps)
_ -> fail $ "could not create uninterpreted symbol of type " ++ show ty
mkUninterpreted ::
forall sym t. (IsSymExprBuilder sym) =>
sym -> IORef (SymFnCache sym) ->
UnintApp (SymExpr sym) ->
BaseTypeRepr t ->
IO (SymExpr sym t)
mkUninterpreted sym ref (UnintApp nm args tys) ret =
do fn <- mkSymFn sym ref nm tys ret
W.applySymFn sym fn args
-- | A value of type @UnintApp f@ represents an uninterpreted function
-- with the given 'String' name, applied to a list of argument values
-- paired with a representation of their types. The context of
-- argument types is existentially quantified.
data UnintApp f =
forall args. UnintApp String (Assignment f args) (Assignment BaseTypeRepr args)
-- | Extract the string from an 'UnintApp'.
stringOfUnintApp :: UnintApp f -> String
stringOfUnintApp (UnintApp s _ _) = s
-- | Make an 'UnintApp' with the given name and no arguments.
mkUnintApp :: String -> UnintApp f
mkUnintApp nm = UnintApp nm Ctx.empty Ctx.empty
-- | Add a suffix to the function name of an 'UnintApp'.
suffixUnintApp :: String -> UnintApp f -> UnintApp f
suffixUnintApp s (UnintApp nm args tys) = UnintApp (nm ++ s) args tys
-- | Extend an 'UnintApp' with an additional argument.
extendUnintApp :: UnintApp f -> f ty -> BaseTypeRepr ty -> UnintApp f
extendUnintApp (UnintApp nm xs tys) x ty =
UnintApp nm (Ctx.extend xs x) (Ctx.extend tys ty)
-- | Flatten an 'SValue' to a sequence of components, each of which is
-- a symbolic value of a base type (e.g. word or boolean), and add
-- them to the list of arguments of the given 'UnintApp'. If the
-- 'SValue' contains any values built from data constructors, then
-- encode them as suffixes on the function name of the 'UnintApp'.
applyUnintApp ::
forall sym.
(W.IsExprBuilder sym) =>
sym ->
UnintApp (SymExpr sym) ->
SValue sym ->
IO (UnintApp (SymExpr sym))
applyUnintApp sym app0 v =
case v of
VUnit -> return app0
VPair x y -> do app1 <- applyUnintApp sym app0 =<< force x
app2 <- applyUnintApp sym app1 =<< force y
return app2
VRecordValue elems -> foldM (applyUnintApp sym) app0 =<< traverse (force . snd) elems
VVector xv -> foldM (applyUnintApp sym) app0 =<< traverse force xv
VBool sb -> return (extendUnintApp app0 sb BaseBoolRepr)
VInt si -> return (extendUnintApp app0 si BaseIntegerRepr)
VIntMod 0 si -> return (extendUnintApp app0 si BaseIntegerRepr)
VIntMod n si -> do n' <- W.intLit sym (toInteger n)
si' <- W.intMod sym si n'
return (extendUnintApp app0 si' BaseIntegerRepr)
VWord (DBV sw) -> return (extendUnintApp app0 sw (W.exprType sw))
VArray (SArray sa) -> return (extendUnintApp app0 sa (W.exprType sa))
VWord ZBV -> return app0
VCtorApp i ps xv -> foldM (applyUnintApp sym) app' =<< traverse force (ps++xv)
where app' = suffixUnintApp ("_" ++ (Text.unpack (identBaseName (primName i)))) app0
VNat n -> return (suffixUnintApp ("_" ++ show n) app0)
VBVToNat w v' -> applyUnintApp sym app' v'
where app' = suffixUnintApp ("_" ++ show w) app0
TValue (suffixTValue -> Just s)
-> return (suffixUnintApp s app0)
VFun _ _ ->
fail $
"Cannot create uninterpreted higher-order function " ++
show (stringOfUnintApp app0)
_ ->
fail $
"Cannot create uninterpreted function " ++
show (stringOfUnintApp app0) ++
" with argument " ++ show v
------------------------------------------------------------
w4Solve :: forall sym.
IsSymExprBuilder sym =>
sym ->
SharedContext ->
SATQuery ->
IO ([(ExtCns Term, (Labeler sym, SValue sym))], [SBool sym])
w4Solve sym sc satq =
do let varList = Map.toList (satVariables satq)
vars <- evalStateT (traverse (traverse (newVarFOT sym)) varList) 0
let varMap = Map.fromList [ (ecVarIndex ec, v) | (ec, (_,v)) <- vars ]
ref <- newIORef Map.empty
bvals <- mapM (w4SolveAssert sym sc varMap ref (satUninterp satq)) (satAsserts satq)
return (vars, bvals)
w4SolveAssert :: forall sym.
IsSymExprBuilder sym =>
sym ->
SharedContext ->