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
|
#include "Halide.h"
using namespace Halide;
using namespace Halide::Internal;
int main(int argc, char **argv) {
Param<int64_t> i64("i64");
Param<int32_t> i32("i32");
Param<int32_t> i16("i16");
Param<uint64_t> u64("u64");
Param<uint32_t> u32("u32");
Param<uint16_t> u16("u16");
Param<uint8_t> u8("u8");
// A list of Exprs we should be able to prove true by analyzing the bitwise op we do
Expr exprs[] = {
// Manipulate or isolate the low bits
(i64 & 1) < 2,
(i64 & 1) >= 0,
(i64 | 1) % 2 == 1,
(i64 & 2) <= 2,
(i64 & 2) >= 0,
(min(i32, -1) ^ (i32 & 255)) < 0,
// The commented out next case is currently beyond us, because we'd have
// to carry expr information in the bits_known format through the
// modulus op. From the bitwise or we know the second-lowest-bit is set,
// but that information isn't representable as a bound or an alignment,
// so it's lost during the analysis on the modulo op.
// (i64 | 2) % 4 >= 2,
(u64 & 1) < 2,
(u64 & 1) >= 0,
(u64 | 1) % 2 == 1,
(u64 & 2) <= 2,
(u64 & 2) >= 0,
// Beyond us for the same reason as above
// (u64 | 2) % 4 >= 2,
// Manipulate or isolate the high bits, in various types, starting with
// two common idioms for aligning a value to a multiple of 16.
((i32 & ~15) & 15) == 0,
((i32 & ~15) % 16) == 0,
((i32 & cast<int32_t>(u16 << 2)) | 5) % 8 == 5,
(i32 | 0x80000000) < 0,
cast<int32_t>(u32 & ~0x80000000) >= 0,
(cast<uint32_t>(u16) & (cast<uint32_t>(u16) << 16)) == 0,
// Setting or unsetting bits makes a number larger or smaller, respectively
(i32 & cast<int32_t>(u16)) >= 0,
(i32 & cast<int32_t>(u16)) < 0x10000,
// What happens when the known bits say a uint is too big to represent
// in our bounds? Not currently reachable, because the (intentional)
// overflow on the cast to uint causes ConstantInterval to just drop all
// information.
// (cast<uint64_t>(i64 | -2)) > u32
// Flipping the bits of an int flips it without overflow. I.e. for a
// uint8, ~x is 255 - x. This gives us bounds information.
(~clamp(u8, 3, 5)) >= 255 - 5,
(~clamp(u8, 3, 5)) <= 255 - 3,
// If we knew the trailing bits before, we still know them after
(~(i32 * 16)) % 16 == 15,
};
// Check we're not inferring *too* much, with variants of the above that
// shouldn't be provable one way or the other.
Expr negative_exprs[] = {
(i64 & 3) < 2,
(i64 & 3) >= 1,
(i64 | 1) % 4 == 1,
(i64 & 3) <= 2,
(i64 & 3) >= 1,
(max(u32, 1000) ^ (u64 & 255)) >= 1000,
(u64 & 3) < 2,
(u64 & 3) >= 1,
(u64 | 1) % 4 == 1,
(u64 & 3) <= 2,
(u64 & 2) >= 1,
((i32 & ~15) & 31) == 0,
((i32 & ~15) % 32) == 0,
((i32 & cast<int32_t>(u16 << 1)) | 5) % 8 == 5,
(i32 | 0x80000000) < -1,
cast<int16_t>(u32 & ~0x80000000) >= 0,
(cast<uint32_t>(u16) & (cast<uint32_t>(u16) << 15)) == 0,
(i32 & cast<int32_t>(u16)) >= 1,
(i32 & cast<int32_t>(u16)) < 0xffff,
(~clamp(u8, 3, 5)) >= 255 - 4,
};
for (auto e : exprs) {
if (!can_prove(e)) {
std::cerr << "Failed to prove: " << e << "\n";
return -1;
}
}
for (auto e : negative_exprs) {
if (is_const(simplify(e))) {
std::cerr << "Should not have been able to prove or disprove: " << e << "\n";
return -1;
}
}
printf("Success!\n");
return 0;
}
|
