/
Z3ConstraintManager.cpp
1646 lines (1387 loc) · 55.4 KB
/
Z3ConstraintManager.cpp
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
//== Z3ConstraintManager.cpp --------------------------------*- C++ -*--==//
//
// The LLVM Compiler Infrastructure
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#include "clang/Basic/TargetInfo.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
#include "clang/Config/config.h"
using namespace clang;
using namespace ento;
#if CLANG_ANALYZER_WITH_Z3
#include <z3.h>
// Forward declarations
namespace {
class Z3Expr;
class ConstraintZ3 {};
} // end anonymous namespace
typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
// Expansion of REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, Z3SetPair)
namespace clang {
namespace ento {
template <>
struct ProgramStateTrait<ConstraintZ3>
: public ProgramStatePartialTrait<ConstraintZ3Ty> {
static void *GDMIndex() {
static int Index;
return &Index;
}
};
} // end namespace ento
} // end namespace clang
namespace {
class Z3Config {
friend class Z3Context;
Z3_config Config;
public:
Z3Config() : Config(Z3_mk_config()) {
// Enable model finding
Z3_set_param_value(Config, "model", "true");
// Disable proof generation
Z3_set_param_value(Config, "proof", "false");
// Set timeout to 15000ms = 15s
Z3_set_param_value(Config, "timeout", "15000");
}
~Z3Config() { Z3_del_config(Config); }
}; // end class Z3Config
class Z3Context {
Z3_context ZC_P;
public:
static Z3_context ZC;
Z3Context() : ZC_P(Z3_mk_context_rc(Z3Config().Config)) { ZC = ZC_P; }
~Z3Context() {
Z3_del_context(ZC);
Z3_finalize_memory();
ZC_P = nullptr;
}
}; // end class Z3Context
class Z3Sort {
friend class Z3Expr;
Z3_sort Sort;
Z3Sort() : Sort(nullptr) {}
Z3Sort(Z3_sort ZS) : Sort(ZS) {
Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
}
public:
/// Override implicit copy constructor for correct reference counting.
Z3Sort(const Z3Sort &Copy) : Sort(Copy.Sort) {
Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
}
/// Provide move constructor
Z3Sort(Z3Sort &&Move) : Sort(nullptr) { *this = std::move(Move); }
/// Provide move assignment constructor
Z3Sort &operator=(Z3Sort &&Move) {
if (this != &Move) {
if (Sort)
Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
Sort = Move.Sort;
Move.Sort = nullptr;
}
return *this;
}
~Z3Sort() {
if (Sort)
Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
}
// Return a boolean sort.
static Z3Sort getBoolSort() { return Z3Sort(Z3_mk_bool_sort(Z3Context::ZC)); }
// Return an appropriate bitvector sort for the given bitwidth.
static Z3Sort getBitvectorSort(unsigned BitWidth) {
return Z3Sort(Z3_mk_bv_sort(Z3Context::ZC, BitWidth));
}
// Return an appropriate floating-point sort for the given bitwidth.
static Z3Sort getFloatSort(unsigned BitWidth) {
Z3_sort Sort;
switch (BitWidth) {
default:
llvm_unreachable("Unsupported floating-point bitwidth!");
break;
case 16:
Sort = Z3_mk_fpa_sort_16(Z3Context::ZC);
break;
case 32:
Sort = Z3_mk_fpa_sort_32(Z3Context::ZC);
break;
case 64:
Sort = Z3_mk_fpa_sort_64(Z3Context::ZC);
break;
case 128:
Sort = Z3_mk_fpa_sort_128(Z3Context::ZC);
break;
}
return Z3Sort(Sort);
}
// Return an appropriate sort for the given AST.
static Z3Sort getSort(Z3_ast AST) {
return Z3Sort(Z3_get_sort(Z3Context::ZC, AST));
}
Z3_sort_kind getSortKind() const {
return Z3_get_sort_kind(Z3Context::ZC, Sort);
}
unsigned getBitvectorSortSize() const {
assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!");
return Z3_get_bv_sort_size(Z3Context::ZC, Sort);
}
unsigned getFloatSortSize() const {
assert(getSortKind() == Z3_FLOATING_POINT_SORT &&
"Not a floating-point sort!");
return Z3_fpa_get_ebits(Z3Context::ZC, Sort) +
Z3_fpa_get_sbits(Z3Context::ZC, Sort);
}
bool operator==(const Z3Sort &Other) const {
return Z3_is_eq_sort(Z3Context::ZC, Sort, Other.Sort);
}
Z3Sort &operator=(const Z3Sort &Move) {
Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Move.Sort));
Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
Sort = Move.Sort;
return *this;
}
void print(raw_ostream &OS) const {
OS << Z3_sort_to_string(Z3Context::ZC, Sort);
}
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Sort
class Z3Expr {
friend class Z3Model;
friend class Z3Solver;
Z3_ast AST;
Z3Expr(Z3_ast ZA) : AST(ZA) { Z3_inc_ref(Z3Context::ZC, AST); }
// Return an appropriate floating-point rounding mode.
static Z3Expr getFloatRoundingMode() {
// TODO: Don't assume nearest ties to even rounding mode
return Z3Expr(Z3_mk_fpa_rne(Z3Context::ZC));
}
// Determine whether two float semantics are equivalent
static bool areEquivalent(const llvm::fltSemantics &LHS,
const llvm::fltSemantics &RHS) {
return (llvm::APFloat::semanticsPrecision(LHS) ==
llvm::APFloat::semanticsPrecision(RHS)) &&
(llvm::APFloat::semanticsMinExponent(LHS) ==
llvm::APFloat::semanticsMinExponent(RHS)) &&
(llvm::APFloat::semanticsMaxExponent(LHS) ==
llvm::APFloat::semanticsMaxExponent(RHS)) &&
(llvm::APFloat::semanticsSizeInBits(LHS) ==
llvm::APFloat::semanticsSizeInBits(RHS));
}
public:
/// Override implicit copy constructor for correct reference counting.
Z3Expr(const Z3Expr &Copy) : AST(Copy.AST) { Z3_inc_ref(Z3Context::ZC, AST); }
/// Provide move constructor
Z3Expr(Z3Expr &&Move) : AST(nullptr) { *this = std::move(Move); }
/// Provide move assignment constructor
Z3Expr &operator=(Z3Expr &&Move) {
if (this != &Move) {
if (AST)
Z3_dec_ref(Z3Context::ZC, AST);
AST = Move.AST;
Move.AST = nullptr;
}
return *this;
}
~Z3Expr() {
if (AST)
Z3_dec_ref(Z3Context::ZC, AST);
}
/// Get the corresponding IEEE floating-point type for a given bitwidth.
static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
switch (BitWidth) {
default:
llvm_unreachable("Unsupported floating-point semantics!");
break;
case 16:
return llvm::APFloat::IEEEhalf();
case 32:
return llvm::APFloat::IEEEsingle();
case 64:
return llvm::APFloat::IEEEdouble();
case 128:
return llvm::APFloat::IEEEquad();
}
}
/// Construct a Z3Expr from a unary operator, given a Z3_context.
static Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) {
Z3_ast AST;
switch (Op) {
default:
llvm_unreachable("Unimplemented opcode");
break;
case UO_Minus:
AST = Z3_mk_bvneg(Z3Context::ZC, Exp.AST);
break;
case UO_Not:
AST = Z3_mk_bvnot(Z3Context::ZC, Exp.AST);
break;
case UO_LNot:
AST = Z3_mk_not(Z3Context::ZC, Exp.AST);
break;
}
return Z3Expr(AST);
}
/// Construct a Z3Expr from a floating-point unary operator, given a
/// Z3_context.
static Z3Expr fromFloatUnOp(const UnaryOperator::Opcode Op,
const Z3Expr &Exp) {
Z3_ast AST;
switch (Op) {
default:
llvm_unreachable("Unimplemented opcode");
break;
case UO_Minus:
AST = Z3_mk_fpa_neg(Z3Context::ZC, Exp.AST);
break;
case UO_LNot:
return Z3Expr::fromUnOp(Op, Exp);
}
return Z3Expr(AST);
}
/// Construct a Z3Expr from a n-ary binary operator.
static Z3Expr fromNBinOp(const BinaryOperator::Opcode Op,
const std::vector<Z3_ast> &ASTs) {
Z3_ast AST;
switch (Op) {
default:
llvm_unreachable("Unimplemented opcode");
break;
case BO_LAnd:
AST = Z3_mk_and(Z3Context::ZC, ASTs.size(), ASTs.data());
break;
case BO_LOr:
AST = Z3_mk_or(Z3Context::ZC, ASTs.size(), ASTs.data());
break;
}
return Z3Expr(AST);
}
/// Construct a Z3Expr from a binary operator, given a Z3_context.
static Z3Expr fromBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op,
const Z3Expr &RHS, bool isSigned) {
Z3_ast AST;
assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
"AST's must have the same sort!");
switch (Op) {
default:
llvm_unreachable("Unimplemented opcode");
break;
// Multiplicative operators
case BO_Mul:
AST = Z3_mk_bvmul(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_Div:
AST = isSigned ? Z3_mk_bvsdiv(Z3Context::ZC, LHS.AST, RHS.AST)
: Z3_mk_bvudiv(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_Rem:
AST = isSigned ? Z3_mk_bvsrem(Z3Context::ZC, LHS.AST, RHS.AST)
: Z3_mk_bvurem(Z3Context::ZC, LHS.AST, RHS.AST);
break;
// Additive operators
case BO_Add:
AST = Z3_mk_bvadd(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_Sub:
AST = Z3_mk_bvsub(Z3Context::ZC, LHS.AST, RHS.AST);
break;
// Bitwise shift operators
case BO_Shl:
AST = Z3_mk_bvshl(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_Shr:
AST = isSigned ? Z3_mk_bvashr(Z3Context::ZC, LHS.AST, RHS.AST)
: Z3_mk_bvlshr(Z3Context::ZC, LHS.AST, RHS.AST);
break;
// Relational operators
case BO_LT:
AST = isSigned ? Z3_mk_bvslt(Z3Context::ZC, LHS.AST, RHS.AST)
: Z3_mk_bvult(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_GT:
AST = isSigned ? Z3_mk_bvsgt(Z3Context::ZC, LHS.AST, RHS.AST)
: Z3_mk_bvugt(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_LE:
AST = isSigned ? Z3_mk_bvsle(Z3Context::ZC, LHS.AST, RHS.AST)
: Z3_mk_bvule(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_GE:
AST = isSigned ? Z3_mk_bvsge(Z3Context::ZC, LHS.AST, RHS.AST)
: Z3_mk_bvuge(Z3Context::ZC, LHS.AST, RHS.AST);
break;
// Equality operators
case BO_EQ:
AST = Z3_mk_eq(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_NE:
return Z3Expr::fromUnOp(UO_LNot,
Z3Expr::fromBinOp(LHS, BO_EQ, RHS, isSigned));
break;
// Bitwise operators
case BO_And:
AST = Z3_mk_bvand(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_Xor:
AST = Z3_mk_bvxor(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_Or:
AST = Z3_mk_bvor(Z3Context::ZC, LHS.AST, RHS.AST);
break;
// Logical operators
case BO_LAnd:
case BO_LOr: {
std::vector<Z3_ast> Args = {LHS.AST, RHS.AST};
return Z3Expr::fromNBinOp(Op, Args);
}
}
return Z3Expr(AST);
}
/// Construct a Z3Expr from a special floating-point binary operator, given
/// a Z3_context.
static Z3Expr fromFloatSpecialBinOp(const Z3Expr &LHS,
const BinaryOperator::Opcode Op,
const llvm::APFloat::fltCategory &RHS) {
Z3_ast AST;
switch (Op) {
default:
llvm_unreachable("Unimplemented opcode");
break;
// Equality operators
case BO_EQ:
switch (RHS) {
case llvm::APFloat::fcInfinity:
AST = Z3_mk_fpa_is_infinite(Z3Context::ZC, LHS.AST);
break;
case llvm::APFloat::fcNaN:
AST = Z3_mk_fpa_is_nan(Z3Context::ZC, LHS.AST);
break;
case llvm::APFloat::fcNormal:
AST = Z3_mk_fpa_is_normal(Z3Context::ZC, LHS.AST);
break;
case llvm::APFloat::fcZero:
AST = Z3_mk_fpa_is_zero(Z3Context::ZC, LHS.AST);
break;
}
break;
case BO_NE:
return Z3Expr::fromFloatUnOp(
UO_LNot, Z3Expr::fromFloatSpecialBinOp(LHS, BO_EQ, RHS));
break;
}
return Z3Expr(AST);
}
/// Construct a Z3Expr from a floating-point binary operator, given a
/// Z3_context.
static Z3Expr fromFloatBinOp(const Z3Expr &LHS,
const BinaryOperator::Opcode Op,
const Z3Expr &RHS) {
Z3_ast AST;
assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
"AST's must have the same sort!");
switch (Op) {
default:
llvm_unreachable("Unimplemented opcode");
break;
// Multiplicative operators
case BO_Mul: {
Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
AST = Z3_mk_fpa_mul(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
break;
}
case BO_Div: {
Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
AST = Z3_mk_fpa_div(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
break;
}
case BO_Rem:
AST = Z3_mk_fpa_rem(Z3Context::ZC, LHS.AST, RHS.AST);
break;
// Additive operators
case BO_Add: {
Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
AST = Z3_mk_fpa_add(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
break;
}
case BO_Sub: {
Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
AST = Z3_mk_fpa_sub(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
break;
}
// Relational operators
case BO_LT:
AST = Z3_mk_fpa_lt(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_GT:
AST = Z3_mk_fpa_gt(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_LE:
AST = Z3_mk_fpa_leq(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_GE:
AST = Z3_mk_fpa_geq(Z3Context::ZC, LHS.AST, RHS.AST);
break;
// Equality operators
case BO_EQ:
AST = Z3_mk_fpa_eq(Z3Context::ZC, LHS.AST, RHS.AST);
break;
case BO_NE:
return Z3Expr::fromFloatUnOp(UO_LNot,
Z3Expr::fromFloatBinOp(LHS, BO_EQ, RHS));
break;
// Logical operators
case BO_LAnd:
case BO_LOr:
return Z3Expr::fromBinOp(LHS, Op, RHS, false);
}
return Z3Expr(AST);
}
/// Construct a Z3Expr from a SymbolData, given a Z3_context.
static Z3Expr fromData(const SymbolID ID, bool isBool, bool isFloat,
uint64_t BitWidth) {
llvm::Twine Name = "$" + llvm::Twine(ID);
Z3Sort Sort;
if (isBool)
Sort = Z3Sort::getBoolSort();
else if (isFloat)
Sort = Z3Sort::getFloatSort(BitWidth);
else
Sort = Z3Sort::getBitvectorSort(BitWidth);
Z3_symbol Symbol = Z3_mk_string_symbol(Z3Context::ZC, Name.str().c_str());
Z3_ast AST = Z3_mk_const(Z3Context::ZC, Symbol, Sort.Sort);
return Z3Expr(AST);
}
/// Construct a Z3Expr from a SymbolCast, given a Z3_context.
static Z3Expr fromCast(const Z3Expr &Exp, QualType ToTy, uint64_t ToBitWidth,
QualType FromTy, uint64_t FromBitWidth) {
Z3_ast AST;
if ((FromTy->isIntegralOrEnumerationType() &&
ToTy->isIntegralOrEnumerationType()) ||
(FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
(FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
(FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
// Special case: Z3 boolean type is distinct from bitvector type, so
// must use if-then-else expression instead of direct cast
if (FromTy->isBooleanType()) {
assert(ToBitWidth > 0 && "BitWidth must be positive!");
Z3Expr Zero = Z3Expr::fromInt("0", ToBitWidth);
Z3Expr One = Z3Expr::fromInt("1", ToBitWidth);
AST = Z3_mk_ite(Z3Context::ZC, Exp.AST, One.AST, Zero.AST);
} else if (ToBitWidth > FromBitWidth) {
AST = FromTy->isSignedIntegerOrEnumerationType()
? Z3_mk_sign_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,
Exp.AST)
: Z3_mk_zero_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,
Exp.AST);
} else if (ToBitWidth < FromBitWidth) {
AST = Z3_mk_extract(Z3Context::ZC, ToBitWidth - 1, 0, Exp.AST);
} else {
// Both are bitvectors with the same width, ignore the type cast
return Exp;
}
} else if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
if (ToBitWidth != FromBitWidth) {
Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
AST = Z3_mk_fpa_to_fp_float(Z3Context::ZC, RoundingMode.AST, Exp.AST,
Sort.Sort);
} else {
return Exp;
}
} else if (FromTy->isIntegralOrEnumerationType() &&
ToTy->isRealFloatingType()) {
Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
AST = FromTy->isSignedIntegerOrEnumerationType()
? Z3_mk_fpa_to_fp_signed(Z3Context::ZC, RoundingMode.AST,
Exp.AST, Sort.Sort)
: Z3_mk_fpa_to_fp_unsigned(Z3Context::ZC, RoundingMode.AST,
Exp.AST, Sort.Sort);
} else if (FromTy->isRealFloatingType() &&
ToTy->isIntegralOrEnumerationType()) {
Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
AST = ToTy->isSignedIntegerOrEnumerationType()
? Z3_mk_fpa_to_sbv(Z3Context::ZC, RoundingMode.AST, Exp.AST,
ToBitWidth)
: Z3_mk_fpa_to_ubv(Z3Context::ZC, RoundingMode.AST, Exp.AST,
ToBitWidth);
} else {
llvm_unreachable("Unsupported explicit type cast!");
}
return Z3Expr(AST);
}
/// Construct a Z3Expr from a boolean, given a Z3_context.
static Z3Expr fromBoolean(const bool Bool) {
Z3_ast AST = Bool ? Z3_mk_true(Z3Context::ZC) : Z3_mk_false(Z3Context::ZC);
return Z3Expr(AST);
}
/// Construct a Z3Expr from a finite APFloat, given a Z3_context.
static Z3Expr fromAPFloat(const llvm::APFloat &Float) {
Z3_ast AST;
Z3Sort Sort = Z3Sort::getFloatSort(
llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true);
Z3Expr Z3Int = Z3Expr::fromAPSInt(Int);
AST = Z3_mk_fpa_to_fp_bv(Z3Context::ZC, Z3Int.AST, Sort.Sort);
return Z3Expr(AST);
}
/// Construct a Z3Expr from an APSInt, given a Z3_context.
static Z3Expr fromAPSInt(const llvm::APSInt &Int) {
Z3Sort Sort = Z3Sort::getBitvectorSort(Int.getBitWidth());
Z3_ast AST =
Z3_mk_numeral(Z3Context::ZC, Int.toString(10).c_str(), Sort.Sort);
return Z3Expr(AST);
}
/// Construct a Z3Expr from an integer, given a Z3_context.
static Z3Expr fromInt(const char *Int, uint64_t BitWidth) {
Z3Sort Sort = Z3Sort::getBitvectorSort(BitWidth);
Z3_ast AST = Z3_mk_numeral(Z3Context::ZC, Int, Sort.Sort);
return Z3Expr(AST);
}
/// Construct an APFloat from a Z3Expr, given the AST representation
static bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST,
llvm::APFloat &Float, bool useSemantics = true) {
assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT &&
"Unsupported sort to floating-point!");
llvm::APSInt Int(Sort.getFloatSortSize(), true);
const llvm::fltSemantics &Semantics =
Z3Expr::getFloatSemantics(Sort.getFloatSortSize());
Z3Sort BVSort = Z3Sort::getBitvectorSort(Sort.getFloatSortSize());
if (!Z3Expr::toAPSInt(BVSort, AST, Int, true)) {
return false;
}
if (useSemantics &&
!Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) {
assert(false && "Floating-point types don't match!");
return false;
}
Float = llvm::APFloat(Semantics, Int);
return true;
}
/// Construct an APSInt from a Z3Expr, given the AST representation
static bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int,
bool useSemantics = true) {
switch (Sort.getSortKind()) {
default:
llvm_unreachable("Unsupported sort to integer!");
case Z3_BV_SORT: {
if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) {
assert(false && "Bitvector types don't match!");
return false;
}
uint64_t Value[2];
// Force cast because Z3 defines __uint64 to be a unsigned long long
// type, which isn't compatible with a unsigned long type, even if they
// are the same size.
Z3_get_numeral_uint64(Z3Context::ZC, AST,
reinterpret_cast<__uint64 *>(&Value[0]));
if (Sort.getBitvectorSortSize() <= 64) {
Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true);
} else if (Sort.getBitvectorSortSize() == 128) {
Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST));
Z3_get_numeral_uint64(Z3Context::ZC, AST,
reinterpret_cast<__uint64 *>(&Value[1]));
Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true);
} else {
assert(false && "Bitwidth not supported!");
return false;
}
return true;
}
case Z3_BOOL_SORT:
if (useSemantics && Int.getBitWidth() < 1) {
assert(false && "Boolean type doesn't match!");
return false;
}
Int = llvm::APSInt(
llvm::APInt(Int.getBitWidth(),
Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1
: 0),
true);
return true;
}
}
void Profile(llvm::FoldingSetNodeID &ID) const {
ID.AddInteger(Z3_get_ast_hash(Z3Context::ZC, AST));
}
bool operator<(const Z3Expr &Other) const {
llvm::FoldingSetNodeID ID1, ID2;
Profile(ID1);
Other.Profile(ID2);
return ID1 < ID2;
}
/// Comparison of AST equality, not model equivalence.
bool operator==(const Z3Expr &Other) const {
assert(Z3_is_eq_sort(Z3Context::ZC, Z3_get_sort(Z3Context::ZC, AST),
Z3_get_sort(Z3Context::ZC, Other.AST)) &&
"AST's must have the same sort");
return Z3_is_eq_ast(Z3Context::ZC, AST, Other.AST);
}
/// Override implicit move constructor for correct reference counting.
Z3Expr &operator=(const Z3Expr &Move) {
Z3_inc_ref(Z3Context::ZC, Move.AST);
Z3_dec_ref(Z3Context::ZC, AST);
AST = Move.AST;
return *this;
}
void print(raw_ostream &OS) const {
OS << Z3_ast_to_string(Z3Context::ZC, AST);
}
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Expr
class Z3Model {
Z3_model Model;
public:
Z3Model(Z3_model ZM) : Model(ZM) { Z3_model_inc_ref(Z3Context::ZC, Model); }
/// Override implicit copy constructor for correct reference counting.
Z3Model(const Z3Model &Copy) : Model(Copy.Model) {
Z3_model_inc_ref(Z3Context::ZC, Model);
}
/// Provide move constructor
Z3Model(Z3Model &&Move) : Model(nullptr) { *this = std::move(Move); }
/// Provide move assignment constructor
Z3Model &operator=(Z3Model &&Move) {
if (this != &Move) {
if (Model)
Z3_model_dec_ref(Z3Context::ZC, Model);
Model = Move.Model;
Move.Model = nullptr;
}
return *this;
}
~Z3Model() {
if (Model)
Z3_model_dec_ref(Z3Context::ZC, Model);
}
/// Given an expression, extract the value of this operand in the model.
bool getInterpretation(const Z3Expr &Exp, llvm::APSInt &Int) const {
Z3_func_decl Func =
Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
return false;
Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
Z3Sort Sort = Z3Sort::getSort(Assign);
return Z3Expr::toAPSInt(Sort, Assign, Int, true);
}
/// Given an expression, extract the value of this operand in the model.
bool getInterpretation(const Z3Expr &Exp, llvm::APFloat &Float) const {
Z3_func_decl Func =
Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
return false;
Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
Z3Sort Sort = Z3Sort::getSort(Assign);
return Z3Expr::toAPFloat(Sort, Assign, Float, true);
}
void print(raw_ostream &OS) const {
OS << Z3_model_to_string(Z3Context::ZC, Model);
}
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Model
class Z3Solver {
friend class Z3ConstraintManager;
Z3_solver Solver;
Z3Solver(Z3_solver ZS) : Solver(ZS) {
Z3_solver_inc_ref(Z3Context::ZC, Solver);
}
public:
/// Override implicit copy constructor for correct reference counting.
Z3Solver(const Z3Solver &Copy) : Solver(Copy.Solver) {
Z3_solver_inc_ref(Z3Context::ZC, Solver);
}
/// Provide move constructor
Z3Solver(Z3Solver &&Move) : Solver(nullptr) { *this = std::move(Move); }
/// Provide move assignment constructor
Z3Solver &operator=(Z3Solver &&Move) {
if (this != &Move) {
if (Solver)
Z3_solver_dec_ref(Z3Context::ZC, Solver);
Solver = Move.Solver;
Move.Solver = nullptr;
}
return *this;
}
~Z3Solver() {
if (Solver)
Z3_solver_dec_ref(Z3Context::ZC, Solver);
}
/// Given a constraint, add it to the solver
void addConstraint(const Z3Expr &Exp) {
Z3_solver_assert(Z3Context::ZC, Solver, Exp.AST);
}
/// Given a program state, construct the logical conjunction and add it to
/// the solver
void addStateConstraints(ProgramStateRef State) {
// TODO: Don't add all the constraints, only the relevant ones
ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
// Construct the logical AND of all the constraints
if (I != IE) {
std::vector<Z3_ast> ASTs;
while (I != IE)
ASTs.push_back(I++->second.AST);
Z3Expr Conj = Z3Expr::fromNBinOp(BO_LAnd, ASTs);
addConstraint(Conj);
}
}
/// Check if the constraints are satisfiable
Z3_lbool check() { return Z3_solver_check(Z3Context::ZC, Solver); }
/// Push the current solver state
void push() { return Z3_solver_push(Z3Context::ZC, Solver); }
/// Pop the previous solver state
void pop(unsigned NumStates = 1) {
assert(Z3_solver_get_num_scopes(Z3Context::ZC, Solver) >= NumStates);
return Z3_solver_pop(Z3Context::ZC, Solver, NumStates);
}
/// Get a model from the solver. Caller should check the model is
/// satisfiable.
Z3Model getModel() {
return Z3Model(Z3_solver_get_model(Z3Context::ZC, Solver));
}
/// Reset the solver and remove all constraints.
void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
}; // end class Z3Solver
void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
llvm::report_fatal_error("Z3 error: " +
llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
}
class Z3ConstraintManager : public SimpleConstraintManager {
Z3Context Context;
mutable Z3Solver Solver;
public:
Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
: SimpleConstraintManager(SE, SB),
Solver(Z3_mk_simple_solver(Z3Context::ZC)) {
Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler);
}
//===------------------------------------------------------------------===//
// Implementation for interface from ConstraintManager.
//===------------------------------------------------------------------===//
bool canReasonAbout(SVal X) const override;
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
const llvm::APSInt *getSymVal(ProgramStateRef State,
SymbolRef Sym) const override;
ProgramStateRef removeDeadBindings(ProgramStateRef St,
SymbolReaper &SymReaper) override;
void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
const char *sep) override;
//===------------------------------------------------------------------===//
// Implementation for interface from SimpleConstraintManager.
//===------------------------------------------------------------------===//
ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
bool Assumption) override;
ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
const llvm::APSInt &From,
const llvm::APSInt &To,
bool InRange) override;
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
bool Assumption) override;
private:
//===------------------------------------------------------------------===//
// Internal implementation.
//===------------------------------------------------------------------===//
// Check whether a new model is satisfiable, and update the program state.
ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym,
const Z3Expr &Exp);
// Generate and check a Z3 model, using the given constraint.
Z3_lbool checkZ3Model(ProgramStateRef State, const Z3Expr &Exp) const;
// Generate a Z3Expr that represents the given symbolic expression.
// Sets the hasComparison parameter if the expression has a comparison
// operator.
// Sets the RetTy parameter to the final return type after promotions and
// casts.
Z3Expr getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,
bool *hasComparison = nullptr) const;
// Generate a Z3Expr that takes the logical not of an expression.
Z3Expr getZ3NotExpr(const Z3Expr &Exp) const;
// Generate a Z3Expr that compares the expression to zero.
Z3Expr getZ3ZeroExpr(const Z3Expr &Exp, QualType RetTy,
bool Assumption) const;
// Recursive implementation to unpack and generate symbolic expression.
// Sets the hasComparison and RetTy parameters. See getZ3Expr().
Z3Expr getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
bool *hasComparison) const;
// Wrapper to generate Z3Expr from SymbolData.
Z3Expr getZ3DataExpr(const SymbolID ID, QualType Ty) const;
// Wrapper to generate Z3Expr from SymbolCast.
Z3Expr getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, QualType Ty) const;
// Wrapper to generate Z3Expr from BinarySymExpr.
// Sets the hasComparison and RetTy parameters. See getZ3Expr().
Z3Expr getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
QualType *RetTy) const;
// Wrapper to generate Z3Expr from unpacked binary symbolic expression.
// Sets the RetTy parameter. See getZ3Expr().
Z3Expr getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
BinaryOperator::Opcode Op, const Z3Expr &RHS,
QualType RTy, QualType *RetTy) const;
//===------------------------------------------------------------------===//
// Helper functions.
//===------------------------------------------------------------------===//
// Recover the QualType of an APSInt.
// TODO: Refactor to put elsewhere
QualType getAPSIntType(const llvm::APSInt &Int) const;
// Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
std::pair<llvm::APSInt, QualType> fixAPSInt(const llvm::APSInt &Int) const;
// Perform implicit type conversion on binary symbolic expressions.
// May modify all input parameters.
// TODO: Refactor to use built-in conversion functions
void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType <y,
QualType &RTy) const;
// Perform implicit integer type conversion.
// May modify all input parameters.