-
Notifications
You must be signed in to change notification settings - Fork 42
/
Instruction.hs
2111 lines (1865 loc) · 85.1 KB
/
Instruction.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 : Lang.Crucible.LLVM.Translation.Instruction
-- Description : Translation of LLVM instructions
-- Copyright : (c) Galois, Inc 2018
-- License : BSD3
-- Maintainer : Rob Dockins <rdockins@galois.com>
-- Stability : provisional
--
-- This module represents the workhorse of the LLVM translation. It
-- is responsible for interpreting the LLVM instruction set into
-- corresponding crucible statements.
-----------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Lang.Crucible.LLVM.Translation.Instruction
( instrResultType
, generateInstr
, definePhiBlock
, assignLLVMReg
, callOrdinaryFunction
) where
import Prelude hiding (exp, pred)
import Control.Lens hiding (op, (:>) )
import Control.Monad (MonadPlus(..), forM, unless)
import Control.Monad.Except (MonadError(..), runExceptT)
import Control.Monad.State.Strict (MonadState(..))
import Control.Monad.Trans.Class (MonadTrans(..))
import Control.Monad.Trans.Maybe
import Data.Foldable (for_, toList)
import Data.Functor (void)
import Data.Int
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty((:|)))
import qualified Data.Map.Strict as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.String
import qualified Data.Text as Text
import qualified Data.Vector as V
import Numeric.Natural
import Prettyprinter (pretty)
import GHC.Exts ( Proxy#, proxy# )
import qualified Text.LLVM.AST as L
import qualified Data.BitVector.Sized as BV
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.NatRepr as NatRepr
import Data.Parameterized.Some
import What4.Utils.StringLiteral
import Lang.Crucible.CFG.Expr
import Lang.Crucible.CFG.Generator
import qualified Lang.Crucible.LLVM.Bytes as G
import Lang.Crucible.LLVM.DataLayout
import qualified Lang.Crucible.LLVM.Errors.Poison as Poison
import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB
import Lang.Crucible.LLVM.Extension
import Lang.Crucible.LLVM.MemModel
import Lang.Crucible.LLVM.MemType
import qualified Lang.Crucible.LLVM.PrettyPrint as LPP
import Lang.Crucible.LLVM.Translation.Constant
import Lang.Crucible.LLVM.Translation.Expr
import Lang.Crucible.LLVM.Translation.Monad
import Lang.Crucible.LLVM.Translation.Options
import Lang.Crucible.LLVM.Translation.Types
import Lang.Crucible.LLVM.TypeContext
import Lang.Crucible.Syntax hiding (IsExpr)
import Lang.Crucible.Types
--------------------------------------------------------------------------------
-- Assertions
-- | Add a bunch of side conditions to a value.
--
-- Allows for effectful computation of the predicates and expressions.
sideConditionsA :: forall f ty s. Applicative f
=> GlobalVar Mem
-> TypeRepr ty
-> Expr LLVM s ty
-- ^ Expression with side-condition
-> [( Bool
, f (Expr LLVM s BoolType)
, UB.UndefinedBehavior (Expr LLVM s)
)]
-- ^ Conditions to (conditionally) assert
-> f (Expr LLVM s ty)
sideConditionsA mvar tyRepr expr conds =
let middle :: Applicative g => (a, g b, c) -> g (a, b, c)
middle (a, fb, c) = (,,) <$> pure a <*> fb <*> pure c
fmapMaybe :: Functor g => g [a] -> (a -> Maybe b) -> g [b]
fmapMaybe gs h = fmap (mapMaybe h) gs
conds' :: f [LLVMSideCondition (Expr LLVM s)]
conds' = fmapMaybe (traverse middle conds) $ \(b, pred, classifier) ->
(if b then Just else const Nothing) $
LLVMSideCondition pred classifier
in flip fmap conds' $
\case
[] -> expr -- No assertions left, nothing to do.
(x:xs) -> App $ ExtensionApp $ LLVM_SideConditions mvar tyRepr (x :| xs) expr
-- | Assert that evaluation doesn't result in a poison value
poisonSideCondition :: GlobalVar Mem
-> TypeRepr ty
-> Poison.Poison (Expr LLVM s)
-> Expr LLVM s ty
-- ^ Expression with side-condition
-> Expr LLVM s BoolType
-- ^ Condition to assert
-> Expr LLVM s ty
poisonSideCondition mvar tyRepr poison expr cond =
runIdentity $ sideConditionsA mvar tyRepr expr [(True, pure cond, UB.PoisonValueCreated poison)]
--------------------------------------------------------------------------------
-- Translation
-- | Get the return type of an LLVM instruction
-- See <https://llvm.org/docs/LangRef.html#instruction-reference the language reference>.
instrResultType ::
(?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
L.Instr ->
m MemType
instrResultType instr =
case instr of
L.Arith _ x _ -> liftMemType (L.typedType x)
L.UnaryArith _ x -> liftMemType (L.typedType x)
L.Bit _ x _ -> liftMemType (L.typedType x)
L.Conv _ _ ty -> liftMemType ty
L.Call _ (L.FunTy ty _ _) _ _ -> liftMemType ty
L.Call _ ty _ _ -> throwError $ unwords ["unexpected non-function type in call:", show ty]
L.Invoke (L.FunTy ty _ _) _ _ _ _ -> liftMemType ty
L.Invoke ty _ _ _ _ -> throwError $ unwords ["unexpected non-function type in invoke:", show ty]
L.CallBr (L.FunTy ty _ _) _ _ _ _ -> liftMemType ty
L.CallBr ty _ _ _ _ -> throwError $ unwords ["unexpected non-function type in callbr:", show ty]
L.Alloca ty _ _ -> liftMemType (L.PtrTo ty)
L.Load tp _ _ _ -> liftMemType tp
L.ICmp _op tv _ -> do
inpType <- liftMemType (L.typedType tv)
case inpType of
VecType len _ -> return (VecType len (IntType 1))
_ -> return (IntType 1)
L.FCmp _op tv _ -> do
inpType <- liftMemType (L.typedType tv)
case inpType of
VecType len _ -> return (VecType len (IntType 1))
_ -> return (IntType 1)
L.Phi tp _ -> liftMemType tp
L.GEP inbounds baseTy basePtr elts ->
do gepRes <- runExceptT (translateGEP inbounds baseTy basePtr elts)
case gepRes of
Left err -> throwError err
Right (GEPResult lanes tp _gep) ->
let n = natValue lanes in
if n == 1 then
return (PtrType (MemType tp))
else
return (VecType n (PtrType (MemType tp)))
L.Select _ x _ -> liftMemType (L.typedType x)
L.ExtractValue x idxes -> liftMemType (L.typedType x) >>= go idxes
where go [] tp = return tp
go (i:is) (ArrayType n tp')
| i < fromIntegral n = go is tp'
| otherwise = throwError $ unwords ["invalid index into array type", showInstr instr]
go (i:is) (StructType si) =
case siFields si V.!? (fromIntegral i) of
Just fi -> go is (fiType fi)
Nothing -> throwError $ unwords ["invalid index into struct type", showInstr instr]
go _ _ = throwError $ unwords ["invalid type in extract value instruction", showInstr instr]
L.InsertValue x _ _ -> liftMemType (L.typedType x)
L.ExtractElt x _ ->
do tp <- liftMemType (L.typedType x)
case tp of
VecType _n tp' -> return tp'
_ -> throwError $ unwords ["extract element of non-vector type", showInstr instr]
L.InsertElt x _ _ -> liftMemType (L.typedType x)
L.ShuffleVector x _ i ->
do xtp <- liftMemType (L.typedType x)
itp <- liftMemType (L.typedType i)
case (xtp, itp) of
(VecType _n ty, VecType m _) -> return (VecType m ty)
_ -> throwError $ unwords ["invalid shufflevector:", showInstr instr]
L.LandingPad x _ _ _ -> liftMemType x
-- LLVM Language Reference: "The original value at the location is returned."
L.AtomicRW _ _ _ v _ _ -> liftMemType (L.typedType v)
L.CmpXchg _weak _volatile _ptr _old new _ _ _ ->
do let dl = llvmDataLayout ?lc
tp <- liftMemType (L.typedType new)
return (StructType (mkStructInfo dl False [tp, i1]))
L.Freeze x -> liftMemType (L.typedType x)
_ -> throwError $ unwords ["instrResultType, unsupported instruction:", showInstr instr]
-- | Given an LLVM expression of vector type, select out the ith element.
extractElt
:: forall s arch ret.
L.Instr
-> MemType -- ^ type contained in the vector
-> Integer -- ^ size of the vector
-> LLVMExpr s arch -- ^ vector expression
-> LLVMExpr s arch -- ^ index expression
-> LLVMGenerator s arch ret (LLVMExpr s arch)
extractElt _instr ty _n (UndefExpr _) _i =
return $ UndefExpr ty
extractElt _instr ty _n (ZeroExpr _) _i =
return $ ZeroExpr ty
extractElt _ ty _ _ (UndefExpr _) =
return $ UndefExpr ty
extractElt instr ty n v (ZeroExpr zty) =
let ?err = fail in
zeroExpand (proxy# :: Proxy# arch) zty $ \_archProxy tyr ex -> extractElt instr ty n v (BaseExpr tyr ex)
extractElt instr _ n (VecExpr _ vs) i
| Scalar _archProxy (LLVMPointerRepr _) (BitvectorAsPointerExpr _ x) <- asScalar i
, App (BVLit _ x') <- x
= constantExtract (BV.asUnsigned x')
where
constantExtract :: Integer -> LLVMGenerator s arch ret (LLVMExpr s arch)
constantExtract idx =
if (fromInteger idx < Seq.length vs) && (fromInteger idx < n)
then return $ Seq.index vs (fromInteger idx)
else fail (unlines ["invalid extractelement instruction (index out of bounds)", showInstr instr])
extractElt instr ty n (VecExpr _ vs) i = do
let ?err = fail
llvmTypeAsRepr ty $ \tyr -> unpackVec (proxy# :: Proxy# arch) tyr (toList vs) $
\ex -> extractElt instr ty n (BaseExpr (VectorRepr tyr) ex) i
extractElt instr _ n (BaseExpr (VectorRepr tyr) v) i =
do mvar <- getMemVar
idx <- case asScalar i of
Scalar _archProxy (LLVMPointerRepr w) x ->
do bv <- pointerAsBitvectorExpr w x
-- The value is poisoned if the index is out of bounds.
let poison = Poison.ExtractElementIndex bv
return $ poisonSideCondition
mvar
NatRepr
poison
-- returned expression
(App (BvToNat w bv))
-- assertion condition
(App (BVUlt w bv (App (BVLit w (BV.mkBV w n)))))
_ ->
fail (unlines ["invalid extractelement instruction", showInstr instr])
return $ BaseExpr tyr (App (VectorGetEntry tyr v idx))
extractElt instr _ _ _ _ = fail (unlines ["invalid extractelement instruction", showInstr instr])
-- | Given an LLVM expression of vector type, insert a new element at location ith element.
insertElt :: forall s arch ret.
L.Instr -- ^ Actual instruction
-> MemType -- ^ type contained in the vector
-> Integer -- ^ size of the vector
-> LLVMExpr s arch -- ^ vector expression
-> LLVMExpr s arch -- ^ element to insert
-> LLVMExpr s arch -- ^ index expression
-> LLVMGenerator s arch ret (LLVMExpr s arch)
insertElt _ ty _ _ _ (UndefExpr _) = do
return $ UndefExpr ty
insertElt instr ty n v a (ZeroExpr zty) = do
let ?err = fail
zeroExpand (proxy# :: Proxy# arch) zty $ \_archProxy tyr ex -> insertElt instr ty n v a (BaseExpr tyr ex)
insertElt instr ty n (UndefExpr _) a i = do
insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (UndefExpr ty))) a i
insertElt instr ty n (ZeroExpr _) a i = do
insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (ZeroExpr ty))) a i
insertElt instr _ n (VecExpr ty vs) a i
| Scalar _archProxy (LLVMPointerRepr _) (BitvectorAsPointerExpr _ x) <- asScalar i
, App (BVLit _ x') <- x
= constantInsert (BV.asUnsigned x')
where
constantInsert :: Integer -> LLVMGenerator s arch ret (LLVMExpr s arch)
constantInsert idx =
if (fromInteger idx < Seq.length vs) && (fromInteger idx < n)
then return $ VecExpr ty $ Seq.adjust (\_ -> a) (fromIntegral idx) vs
else fail (unlines ["invalid insertelement instruction (index out of bounds)", showInstr instr])
insertElt instr ty n (VecExpr _ vs) a i = do
let ?err = fail
llvmTypeAsRepr ty $ \tyr -> unpackVec (proxy# :: Proxy# arch) tyr (toList vs) $
\ex -> insertElt instr ty n (BaseExpr (VectorRepr tyr) ex) a i
insertElt instr _ n (BaseExpr (VectorRepr tyr) v) a i =
do mvar <- getMemVar
(idx :: Expr LLVM s NatType)
<- case asScalar i of
Scalar _archProxy (LLVMPointerRepr w) x ->
do bv <- pointerAsBitvectorExpr w x
-- The value is poisoned if the index is out of bounds.
let poison = Poison.InsertElementIndex bv
return $
poisonSideCondition
mvar
NatRepr
poison
-- returned expression
(App (BvToNat w bv))
-- assertion condition
(App (BVUlt w bv (App (BVLit w (BV.mkBV w n)))))
_ ->
fail (unlines ["invalid insertelement instruction", showInstr instr, show i])
let ?err = fail
unpackOne a $ \_archProxy tyra a' ->
case testEquality tyr tyra of
Just Refl ->
return $ BaseExpr (VectorRepr tyr) (App (VectorSetEntry tyr v idx a'))
Nothing -> fail (unlines ["type mismatch in insertelement instruction", showInstr instr])
insertElt instr _tp n v a i = fail (unlines ["invalid insertelement instruction", showInstr instr, show n, show v, show a, show i])
-- Given an LLVM expression of vector or structure type, select out the
-- element indicated by the sequence of given concrete indices.
extractValue
:: LLVMExpr s arch -- ^ aggregate expression
-> [Int32] -- ^ sequence of indices
-> LLVMGenerator s arch ret (LLVMExpr s arch)
extractValue v [] = return v
extractValue (UndefExpr (StructType si)) is =
extractValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, UndefExpr tp)) tps) is
where tps = map fiType $ toList $ siFields si
extractValue (UndefExpr (ArrayType n tp)) is =
extractValue (VecExpr tp $ Seq.replicate (fromIntegral n) (UndefExpr tp)) is
extractValue (ZeroExpr (StructType si)) is =
extractValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, ZeroExpr tp)) tps) is
where tps = map fiType $ toList $ siFields si
extractValue (ZeroExpr (ArrayType n tp)) is =
extractValue (VecExpr tp $ Seq.replicate (fromIntegral n) (ZeroExpr tp)) is
extractValue (StructExpr vs) (i:is)
| fromIntegral i < Seq.length vs = extractValue (snd $ Seq.index vs $ fromIntegral i) is
extractValue (VecExpr _ vs) (i:is)
| fromIntegral i < Seq.length vs = extractValue (Seq.index vs $ fromIntegral i) is
extractValue (BaseExpr (StructRepr ctx) x) (i:is)
| Just (Some idx) <- Ctx.intIndex (fromIntegral i) (Ctx.size ctx) = do
let tpr = ctx Ctx.! idx
extractValue (BaseExpr tpr (getStruct idx x)) is
extractValue (BaseExpr (VectorRepr elTp) x) (i:is)
| i >= 0 =
do let n = fromIntegral i :: Natural
extractValue (BaseExpr elTp (app (VectorGetEntry elTp x (litExpr n)))) is
extractValue _ _ = fail "invalid extractValue instruction"
-- Given an LLVM expression of vector or structure type, insert a new element in the posistion
-- given by the concrete indices.
insertValue
:: LLVMExpr s arch -- ^ aggregate expression
-> LLVMExpr s arch -- ^ element to insert
-> [Int32] -- ^ sequence of concrete indices
-> LLVMGenerator s arch ret (LLVMExpr s arch)
insertValue _ v [] = return v
insertValue (UndefExpr (StructType si)) v is =
insertValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, UndefExpr tp)) tps) v is
where tps = map fiType $ toList $ siFields si
insertValue (UndefExpr (ArrayType n tp)) v is =
insertValue (VecExpr tp $ Seq.replicate (fromIntegral n) (UndefExpr tp)) v is
insertValue (ZeroExpr (StructType si)) v is =
insertValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, ZeroExpr tp)) tps) v is
where tps = map fiType $ toList $ siFields si
insertValue (ZeroExpr (ArrayType n tp)) v is =
insertValue (VecExpr tp $ Seq.replicate (fromIntegral n) (ZeroExpr tp)) v is
insertValue (StructExpr vs) v (i:is)
| fromIntegral i < Seq.length vs = do
let (xtp, x) = Seq.index vs (fromIntegral i)
x' <- insertValue x v is
return (StructExpr (Seq.adjust (\_ -> (xtp,x')) (fromIntegral i) vs))
insertValue (VecExpr tp vs) v (i:is)
| fromIntegral i < Seq.length vs = do
let x = Seq.index vs (fromIntegral i)
x' <- insertValue x v is
return (VecExpr tp (Seq.adjust (\_ -> x') (fromIntegral i) vs))
insertValue (BaseExpr (StructRepr ctx) x) v (i:is)
| Just (Some idx) <- Ctx.intIndex (fromIntegral i) (Ctx.size ctx) = do
let tpr = ctx Ctx.! idx
x' <- insertValue (BaseExpr tpr (getStruct idx x)) v is
let ?err = fail
unpackOne x' $ \_px tpr' x'' ->
case testEquality tpr tpr' of
Just Refl -> return $ BaseExpr (StructRepr ctx) (setStruct ctx x idx x'')
Nothing -> fail "insertValue was expected to return base value of same type (struct case)"
insertValue (BaseExpr (VectorRepr elTp) x) v (i:is)
| i >= 0 =
do let n = fromIntegral i :: Natural
x' <- insertValue (BaseExpr elTp (app (VectorGetEntry elTp x (litExpr n)))) v is
let ?err = fail
unpackOne x' $ \_px tpr' x'' ->
case testEquality elTp tpr' of
Just Refl -> return $ BaseExpr (VectorRepr elTp) (app (VectorSetEntry elTp x (litExpr n) x''))
Nothing -> fail "insertValue was expected to return base value of same type (vector case)"
insertValue _ _ _ = fail "invalid insertValue instruction"
evalGEP :: forall s arch ret wptr.
wptr ~ ArchWidth arch =>
L.Instr ->
GEPResult (LLVMExpr s arch) ->
LLVMGenerator s arch ret (LLVMExpr s arch)
evalGEP instr (GEPResult _lanes finalMemType gep0) = finish =<< go gep0
where
finish xs =
case Seq.viewl xs of
x Seq.:< (Seq.null -> True) -> return (BaseExpr PtrRepr x)
_ -> return (VecExpr (PtrType (MemType finalMemType)) (fmap (BaseExpr PtrRepr) xs))
badGEP :: LLVMGenerator s arch ret a
badGEP = fail $ unlines ["Unexpected failure when evaluating GEP", showInstr instr]
asPtr :: LLVMExpr s arch -> LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
asPtr x =
case asScalar x of
Scalar _archProxy PtrRepr p -> return p
_ -> badGEP
go :: GEP n (LLVMExpr s arch) -> LLVMGenerator s arch ret (Seq (Expr LLVM s (LLVMPointerType wptr)))
go (GEP_scalar_base x) =
do p <- asPtr x
return (Seq.singleton p)
go (GEP_vector_base n x) =
do xs <- maybe badGEP (traverse (\y -> asPtr y)) (asVector x)
unless (fromIntegral (Seq.length xs) == natValue n) badGEP
return xs
go (GEP_scatter n gep) =
do xs <- go gep
unless (Seq.length xs == 1) badGEP
return (Seq.cycleTaking (widthVal n) xs)
go (GEP_field fi gep) =
do xs <- go gep
traverse (\x -> calcGEP_struct fi x) xs
go (GEP_index_each mt' gep idx) =
do xs <- go gep
traverse (\x -> calcGEP_array mt' x idx) xs
go (GEP_index_vector mt' gep idx) =
do xs <- go gep
idxs <- maybe badGEP return (asVector idx)
unless (Seq.length idxs == Seq.length xs) badGEP
traverse (\(x,i) -> calcGEP_array mt' x i) (Seq.zip xs idxs)
calcGEP_array :: forall wptr s arch ret.
wptr ~ ArchWidth arch =>
MemType {- ^ Type of the array elements -} ->
Expr LLVM s (LLVMPointerType wptr) {- ^ Base pointer -} ->
LLVMExpr s arch {- ^ index value -} ->
LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
calcGEP_array _typ base (ZeroExpr _) = return base
-- If the array index is the concrete number 0, then return the base
-- pointer unchanged.
calcGEP_array typ base idx =
do -- sign-extend the index value if necessary to make it
-- the same width as a pointer
(idx' :: Expr LLVM s (BVType wptr))
<- case asScalar idx of
Scalar _archProxy (LLVMPointerRepr w) x
| Just Refl <- testEquality w PtrWidth ->
pointerAsBitvectorExpr PtrWidth x
| Just LeqProof <- testLeq (incNat w) PtrWidth ->
do x' <- pointerAsBitvectorExpr w x
return $ app (BVSext PtrWidth w x')
_ -> fail $ unwords ["Invalid index value in GEP", show idx]
-- Calculate the size of the element memtype and check that it fits
-- in the pointer width
let dl = llvmDataLayout ?lc
let isz = G.bytesToInteger $ memTypeSize dl typ
unless (isz <= maxSigned PtrWidth)
(fail $ unwords ["Type size too large for pointer width:", show typ])
-- Perform the multiply
mvar <- getMemVar
off0 <- AtomExpr <$> (mkAtom $ app $ BVMul PtrWidth (app $ BVLit PtrWidth (BV.mkBV PtrWidth isz)) idx')
let off =
if isz == 0
then off0
else
let
-- Compute safe upper and lower bounds for the index value to
-- prevent multiplication overflow. Note that `minidx <= idx <=
-- maxidx` iff `MININT <= (isz * idx) <= MAXINT` when `isz` and
-- `idx` are considered as infinite precision integers. This
-- property holds only if we use `quot` (which rounds toward 0)
-- for the divisions in the following definitions.
-- maximum and minimum indices to prevent multiplication overflow
maxidx = maxSigned PtrWidth `quot` (max isz 1)
minidx = minSigned PtrWidth `quot` (max isz 1)
poison = Poison.GEPOutOfBounds base idx'
cond =
(app $ BVSle PtrWidth (app $ BVLit PtrWidth (BV.mkBV PtrWidth minidx)) idx') .&&
(app $ BVSle PtrWidth idx' (app $ BVLit PtrWidth (BV.mkBV PtrWidth maxidx)))
in
-- Multiplication overflow will result in a pointer which is not "in
-- bounds" for the given allocation. We translate all GEP
-- instructions as if they had the `inbounds` flag set, so the
-- result would be a poison value.
poisonSideCondition mvar (BVRepr PtrWidth) poison off0 cond
-- Perform the pointer offset arithmetic
callPtrAddOffset base off
calcGEP_struct ::
wptr ~ ArchWidth arch =>
FieldInfo ->
Expr LLVM s (LLVMPointerType wptr) ->
LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
calcGEP_struct fi base =
do -- Get the field offset and check that it fits
-- in the pointer width
let ioff = G.bytesToInteger $ fiOffset fi
unless (ioff <= maxSigned PtrWidth)
(fail $ unwords ["Field offset too large for pointer width in structure:", show ioff])
let off = app $ BVLit PtrWidth $ BV.mkBV PtrWidth ioff
-- Perform the pointer arithmetic and continue
-- Skip pointer arithmetic when offset is 0
if ioff == 0 then return base else callPtrAddOffset base off
translateConversion :: (?transOpts :: TranslationOptions) =>
L.Instr ->
L.ConvOp ->
MemType {- Input type -} ->
LLVMExpr s arch {- Value to convert -} ->
MemType {- Output type -} ->
LLVMGenerator s arch ret (LLVMExpr s arch)
-- Bitcast is a bit of a special case, handle separately
translateConversion _instr L.BitCast inty x outty = bitCast inty x outty
-- Perform translations pointwise on vectors
translateConversion instr op (VecType n inty) (explodeVector n -> Just xs) (VecType m outty)
| n == m = VecExpr outty <$> traverse (\x -> translateConversion instr op inty x outty) xs
-- Otherwise, assume scalar values and do the basic conversions
translateConversion instr op _inty x outty =
let showI = showInstr instr in
case op of
L.IntToPtr -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) _, LLVMPointerRepr w')
| Just Refl <- testEquality w PtrWidth
, Just Refl <- testEquality w' PtrWidth -> return x
(Scalar _ t v, a) ->
fail (unlines ["integer-to-pointer conversion failed: "
, showI
, show v ++ " : " ++ show (pretty t) ++ " -to- " ++ show (pretty a)
])
(NotScalar, _) -> fail (unlines ["integer-to-pointer conversion failed: non scalar", showI])
L.PtrToInt -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) _, LLVMPointerRepr w')
| Just Refl <- testEquality w PtrWidth
, Just Refl <- testEquality w' PtrWidth -> return x
_ -> fail (unlines ["pointer-to-integer conversion failed", showI])
L.Trunc -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w'))
| Just LeqProof <- isPosNat w'
, Just LeqProof <- testLeq (incNat w') w ->
do x_bv <- pointerAsBitvectorExpr w x'
let bv' = App (BVTrunc w' w x_bv)
return (BaseExpr outty' (BitvectorAsPointerExpr w' bv'))
_ -> fail (unlines [unwords ["invalid truncation:", show x, show outty], showI])
L.ZExt -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w'))
| Just LeqProof <- isPosNat w
, Just LeqProof <- testLeq (incNat w) w' ->
do x_bv <- pointerAsBitvectorExpr w x'
let bv' = App (BVZext w' w x_bv)
return (BaseExpr outty' (BitvectorAsPointerExpr w' bv'))
_ -> fail (unlines [unwords ["invalid zero extension:", show x, show outty], showI])
L.SExt -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w'))
| Just LeqProof <- isPosNat w
, Just LeqProof <- testLeq (incNat w) w' -> do
do x_bv <- pointerAsBitvectorExpr w x'
let bv' = App (BVSext w' w x_bv)
return (BaseExpr outty' (BitvectorAsPointerExpr w' bv'))
_ -> fail (unlines [unwords ["invalid sign extension", show x, show outty], showI])
#if __GLASGOW_HASKELL__ < 900
-- This is redundant, but GHC's pattern-match coverage checker is only
-- smart enough to realize this in 9.0 or later.
L.BitCast -> bitCast _inty x outty
#endif
L.UiToFp -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) x', FloatRepr fi) -> do
bv <- pointerAsBitvectorExpr w x'
return $ BaseExpr (FloatRepr fi) $ App $ FloatFromBV fi RNE bv
_ -> fail (unlines [unwords ["Invalid uitofp:", show op, show x, show outty], showI])
L.SiToFp -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) x', FloatRepr fi) -> do
bv <- pointerAsBitvectorExpr w x'
return $ BaseExpr (FloatRepr fi) $ App $ FloatFromSBV fi RNE bv
_ -> fail (unlines [unwords ["Invalid sitofp:", show op, show x, show outty], showI])
L.FpToUi -> do
let demoteToInt :: (1 <= w) => NatRepr w -> Expr LLVM s (FloatType fi) -> LLVMExpr s arch
demoteToInt w v = BaseExpr (LLVMPointerRepr w) (BitvectorAsPointerExpr w $ App $ FloatToBV w RNE v)
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (FloatRepr _) x', LLVMPointerRepr w) -> return $ demoteToInt w x'
_ -> fail (unlines [unwords ["Invalid fptoui:", show op, show x, show outty], showI])
L.FpToSi -> do
let demoteToInt :: (1 <= w) => NatRepr w -> Expr LLVM s (FloatType fi) -> LLVMExpr s arch
demoteToInt w v = BaseExpr (LLVMPointerRepr w) (BitvectorAsPointerExpr w $ App $ FloatToSBV w RNE v)
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (FloatRepr _) x', LLVMPointerRepr w) -> return $ demoteToInt w x'
_ -> fail (unlines [unwords ["Invalid fptosi:", show op, show x, show outty], showI])
L.FpTrunc -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (FloatRepr _) x', FloatRepr fi) -> do
return $ BaseExpr (FloatRepr fi) $ App $ FloatCast fi RNE x'
_ -> fail (unlines [unwords ["Invalid fptrunc:", show op, show x, show outty], showI])
L.FpExt -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (FloatRepr _) x', FloatRepr fi) -> do
return $ BaseExpr (FloatRepr fi) $ App $ FloatCast fi RNE x'
_ -> fail (unlines [unwords ["Invalid fpext:", show op, show x, show outty], showI])
--------------------------------------------------------------------------------
-- Bit Cast
bitCast :: (?lc::TypeContext,HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
MemType {- ^ starting type of the expression -} ->
LLVMExpr s arch {- ^ expression to cast -} ->
MemType {- ^ target type -} ->
LLVMGenerator s arch ret (LLVMExpr s arch)
bitCast _ (ZeroExpr _) tgtT = return (ZeroExpr tgtT)
bitCast _ (UndefExpr _) tgtT = return (UndefExpr tgtT)
-- pointer casts always succeed
bitCast (PtrType _) expr (PtrType _) = return expr
bitCast (PtrType _) expr PtrOpaqueType = return expr
bitCast PtrOpaqueType expr (PtrType _) = return expr
bitCast PtrOpaqueType expr PtrOpaqueType = return expr
-- casts between vectors of the same length can just be done pointwise
bitCast (VecType n srcT) (explodeVector n -> Just xs) (VecType n' tgtT)
| n == n' = VecExpr tgtT <$> traverse (\x -> bitCast srcT x tgtT) xs
-- otherwise, cast via an intermediate integer type of common width
bitCast srcT expr tgtT = mb =<< runMaybeT (
case (memTypeBitwidth srcT, memTypeBitwidth tgtT) of
(Just w1, Just w2) | w1 == w2 -> castToInt srcT expr >>= castFromInt tgtT w2
_ -> mzero)
where
mb = maybe (err [ "*** Invalid coercion of expression"
, indent (show expr)
, "of type"
, indent (show srcT)
, "to type"
, indent (show tgtT)
]) return
err msg = reportError $ fromString $ unlines ("[bitCast] Failed to perform cast:" : msg)
indent msg = " " ++ msg
castToInt :: (?lc::TypeContext,HasPtrWidth w, w ~ ArchWidth arch) =>
MemType {- ^ type of input expression -} ->
LLVMExpr s arch ->
MaybeT (LLVMGenerator' s arch ret) (LLVMExpr s arch)
castToInt (IntType w) (BaseExpr (LLVMPointerRepr wrepr) x)
| w == natValue wrepr
= lift (BaseExpr (BVRepr wrepr) <$> pointerAsBitvectorExpr wrepr x)
castToInt FloatType (BaseExpr (FloatRepr SingleFloatRepr) x)
= return (BaseExpr (BVRepr (knownNat @32)) (app (FloatToBinary SingleFloatRepr x)))
castToInt DoubleType (BaseExpr (FloatRepr DoubleFloatRepr) x)
= return (BaseExpr (BVRepr (knownNat @64)) (app (FloatToBinary DoubleFloatRepr x)))
castToInt X86_FP80Type (BaseExpr (FloatRepr X86_80FloatRepr) x)
= return (BaseExpr (BVRepr (knownNat @80)) (app (FloatToBinary X86_80FloatRepr x)))
castToInt (VecType n tp) (explodeVector n -> Just xs) =
do xs' <- traverse (castToInt tp) (toList xs)
MaybeT (return (vecJoin xs'))
castToInt _ _ = mzero
castFromInt :: (?lc::TypeContext,HasPtrWidth w, w ~ ArchWidth arch) =>
MemType {- ^ target type -} ->
Natural {- ^ bitvector width in bits -} ->
LLVMExpr s arch -> MaybeT (LLVMGenerator' s arch ret) (LLVMExpr s arch)
castFromInt (IntType w1) w2 (BaseExpr (BVRepr w) x)
| w1 == w2, w1 == natValue w
= return (BaseExpr (LLVMPointerRepr w) (BitvectorAsPointerExpr w x))
castFromInt FloatType 32 (BaseExpr (BVRepr w) x)
| Just Refl <- testEquality w (knownNat @32)
= return (BaseExpr (FloatRepr SingleFloatRepr) (app (FloatFromBinary SingleFloatRepr x)))
castFromInt DoubleType 64 (BaseExpr (BVRepr w) x)
| Just Refl <- testEquality w (knownNat @64)
= return (BaseExpr (FloatRepr DoubleFloatRepr) (app (FloatFromBinary DoubleFloatRepr x)))
castFromInt X86_FP80Type 80 (BaseExpr (BVRepr w) x)
| Just Refl <- testEquality w (knownNat @80)
= return (BaseExpr (FloatRepr X86_80FloatRepr) (app (FloatFromBinary X86_80FloatRepr x)))
castFromInt (VecType n tp) w expr
| n > 0
, (w',0) <- w `divMod` n
, Some wrepr' <- mkNatRepr w'
, Just LeqProof <- isPosNat wrepr'
= do xs <- MaybeT (return (vecSplit wrepr' expr))
VecExpr tp . Seq.fromList <$> traverse (castFromInt tp w') xs
castFromInt _ _ _ = mzero
-- | Join the elements of a vector into a single bit-vector value.
-- The resulting bit-vector would be of length at least one.
vecJoin :: (?lc::TypeContext,HasPtrWidth w, w ~ ArchWidth arch) =>
[LLVMExpr s arch] {- ^ Join these vector elements -} ->
Maybe (LLVMExpr s arch)
vecJoin exprs =
do (a,ys) <- List.uncons exprs
Scalar _archProxy (BVRepr (n :: NatRepr n)) e1 <- return (asScalar a)
if null ys
then do LeqProof <- testLeq (knownNat @1) n
return (BaseExpr (BVRepr n) e1)
else do BaseExpr (BVRepr m) e2 <- vecJoin ys
let p1 = leqZero @n
p2 = leqProof (knownNat @1) m
(LeqProof,LeqProof) <- return (leqAdd2 p1 p2, leqAdd2 p2 p1)
let bits u v x y = bitVal (addNat u v) (BVConcat u v x y)
return $! case llvmDataLayout ?lc ^. intLayout of
LittleEndian -> bits m n e2 e1
BigEndian -> bits n m e1 e2
bitVal ::
(1 <= n) =>
NatRepr n ->
App LLVM (Expr LLVM s) (BVType n) ->
LLVMExpr s arch
bitVal n e = BaseExpr (BVRepr n) (App e)
-- | Split a single bit-vector value into a vector of value of the given width.
vecSplit :: forall s n w arch. (?lc::TypeContext,HasPtrWidth w, w ~ ArchWidth arch, 1 <= n) =>
NatRepr n {- ^ Length of a single element -} ->
LLVMExpr s arch {- ^ Bit-vector value -} ->
Maybe [ LLVMExpr s arch ]
vecSplit elLen expr =
do Scalar _archProxy (BVRepr totLen) e <- return (asScalar expr)
let getEl :: NatRepr offset -> Maybe [ LLVMExpr s arch ]
getEl offset = let end = addNat offset elLen
in case testLeq end totLen of
Just LeqProof ->
do rest <- getEl end
let x = bitVal elLen
(BVSelect offset elLen totLen e)
return (x : rest)
Nothing ->
do Refl <- testEquality offset totLen
return []
els <- getEl (knownNat @0)
-- in `els` the least significant chunk is first
return $! case lay ^. intLayout of
LittleEndian -> els
BigEndian -> reverse els
where
lay = llvmDataLayout ?lc
bitop :: (?transOpts :: TranslationOptions) =>
L.BitOp ->
MemType ->
LLVMExpr s arch ->
LLVMExpr s arch ->
LLVMGenerator s arch ret (LLVMExpr s arch)
bitop op (VecType n tp) (explodeVector n -> Just xs) (explodeVector n -> Just ys) =
VecExpr tp <$> sequence (Seq.zipWith (\x y -> bitop op tp x y) xs ys)
bitop op _ x y =
case (asScalar x, asScalar y) of
(Scalar _archProxy (LLVMPointerRepr w) x',
Scalar _archPrxy' (LLVMPointerRepr w') y')
| Just Refl <- testEquality w w'
, Just LeqProof <- isPosNat w -> do
xbv <- pointerAsBitvectorExpr w x'
ybv <- pointerAsBitvectorExpr w y'
ex <- raw_bitop op w xbv ybv
return (BaseExpr (LLVMPointerRepr w) (BitvectorAsPointerExpr w ex))
_ -> fail $ unwords ["bitwise operation on unsupported values", show x, show y]
raw_bitop :: (?transOpts :: TranslationOptions, 1 <= w) =>
L.BitOp ->
NatRepr w ->
Expr LLVM s (BVType w) ->
Expr LLVM s (BVType w) ->
LLVMGenerator s arch ret (Expr LLVM s (BVType w))
raw_bitop op w a b =
do mvar <- getMemVar
let withSideConds val lst = sideConditionsA mvar (BVRepr w) val lst
let noLaxArith = not (laxArith ?transOpts)
case op of
L.And -> return $ App (BVAnd w a b)
L.Or -> return $ App (BVOr w a b)
L.Xor -> return $ App (BVXor w a b)
L.Shl nuw nsw -> do
let wlit = App (BVLit w (BV.width w))
result <- AtomExpr <$> mkAtom (App (BVShl w a b))
withSideConds result
[ ( noLaxArith
, pure $ App (BVUlt w b wlit) -- TODO: is this the right condition?
, UB.PoisonValueCreated $ Poison.ShlOp2Big a b
)
, ( nuw && noLaxArith
, fmap (App . BVEq w a . AtomExpr)
(mkAtom (App (BVLshr w result b)))
, UB.PoisonValueCreated $ Poison.ShlNoUnsignedWrap a b
)
, ( nsw && noLaxArith
, fmap (App . BVEq w a . AtomExpr)
(mkAtom (App (BVAshr w result b)))
, UB.PoisonValueCreated $ Poison.ShlNoSignedWrap a b
)
]
L.Lshr exact -> do
let wlit = App (BVLit w (BV.width w))
result <- AtomExpr <$> mkAtom (App (BVLshr w a b))
withSideConds result
[ ( noLaxArith
, pure $ App (BVUlt w b wlit)
, UB.PoisonValueCreated $ Poison.LshrOp2Big a b
)
, ( exact && noLaxArith
, fmap (App . BVEq w a . AtomExpr)
(mkAtom (App (BVShl w result b)))
, UB.PoisonValueCreated $ Poison.LshrExact a b
)
]
L.Ashr exact
| Just LeqProof <- isPosNat w -> do
let wlit = App (BVLit w (BV.width w))
result <- AtomExpr <$> mkAtom (App (BVAshr w a b))
withSideConds result
[ ( noLaxArith
, pure $ App (BVUlt w b wlit)
, UB.PoisonValueCreated $ Poison.AshrOp2Big a b
)
, ( exact && noLaxArith
, fmap (App . BVEq w a)
(AtomExpr <$> mkAtom (App (BVShl w result b)))
, UB.PoisonValueCreated $ Poison.AshrExact a b
)
]
| otherwise -> fail "cannot arithmetic right shift a 0-width integer"
-- | Translate an LLVM integer operation into a Crucible CFG expression.
--
-- Poison values can arise from such operations.
intop :: forall w s arch ret. (?transOpts :: TranslationOptions, 1 <= w)
=> L.ArithOp
-> NatRepr w
-> Expr LLVM s (BVType w)
-> Expr LLVM s (BVType w)
-> LLVMGenerator s arch ret (Expr LLVM s (BVType w))
intop op w a b =
do mvar <- getMemVar
let withSideConds val lst = sideConditionsA mvar (BVRepr w) val lst
let withPoison val xs =
do v <- AtomExpr <$> mkAtom val
withSideConds v $ map (\(d, e, c) -> (d, pure e, UB.PoisonValueCreated c)) xs
let z = App (BVLit w (BV.zero w))
let bNeqZero = \ub -> (True, pure (notExpr (App (BVEq w z b))), ub)
let neg1 = App (BVLit w (BV.mkBV w (-1)))
let minInt = App (BVLit w (BV.minSigned w))
let noLaxArith = not (laxArith ?transOpts)
case op of
L.Add nuw nsw -> withPoison (App (BVAdd w a b))
[ ( nuw && noLaxArith
, notExpr (App (BVCarry w a b))
, Poison.AddNoUnsignedWrap a b
)
, ( nsw && noLaxArith
, notExpr (App (BVSCarry w a b))
, Poison.AddNoSignedWrap a b
)
]
L.Sub nuw nsw -> withPoison (App (BVSub w a b))
[ ( nuw && noLaxArith
, notExpr (App (BVUlt w a b))
, Poison.SubNoUnsignedWrap a b
)
, ( nsw && noLaxArith
, notExpr (App (BVSBorrow w a b))
, Poison.SubNoSignedWrap a b
)
]
L.Mul nuw nsw -> do
let w' = addNat w w
Just LeqProof <- return $ isPosNat w'
Just LeqProof <- return $ testLeq (incNat w) w'
prod <- AtomExpr <$> mkAtom (App (BVMul w a b))
withSideConds prod
[ ( nuw && noLaxArith
, do
az <- AtomExpr <$> mkAtom (App (BVZext w' w a))
bz <- AtomExpr <$> mkAtom (App (BVZext w' w b))
wideprod <- AtomExpr <$> mkAtom (App (BVMul w' az bz))
prodz <- AtomExpr <$> mkAtom (App (BVZext w' w prod))
return (App (BVEq w' wideprod prodz))
, UB.PoisonValueCreated $ Poison.MulNoUnsignedWrap a b
)
, ( nsw && noLaxArith
, do
as <- AtomExpr <$> mkAtom (App (BVSext w' w a))
bs <- AtomExpr <$> mkAtom (App (BVSext w' w b))
wideprod <- AtomExpr <$> mkAtom (App (BVMul w' as bs))
prods <- AtomExpr <$> mkAtom (App (BVSext w' w prod))
return (App (BVEq w' wideprod prods))
, UB.PoisonValueCreated $ Poison.MulNoSignedWrap a b
)
]
L.UDiv exact -> do
q <- AtomExpr <$> mkAtom (App (BVUdiv w a b))
withSideConds q