normalized_conjunction.cpp 23.8 KB
Newer Older
Tim Gymnich's avatar
Tim Gymnich committed
1
2
3
4
5
6
7
//
//  normalized_conjunction.cpp
//  ADTTests
//
//  Created by Tim Gymnich on 17.1.20.
//

Tim Gymnich's avatar
Tim Gymnich committed
8
#include "normalized_conjunction.h"
Tim Gymnich's avatar
Tim Gymnich committed
9

Tim Gymnich's avatar
Tim Gymnich committed
10
11
#include "llvm/IR/CFG.h"

Tim Gymnich's avatar
Tim Gymnich committed
12
using namespace llvm;
Tim Gymnich's avatar
Tim Gymnich committed
13
14
15

namespace pcpo {

Tim Gymnich's avatar
Tim Gymnich committed
16
// MARK: - Initializers
Tim Gymnich's avatar
Tim Gymnich committed
17

Tim Gymnich's avatar
Tim Gymnich committed
18
19
NormalizedConjunction::NormalizedConjunction(Function const& f) {
    for (Argument const& arg: f.args()) {
Tim Gymnich's avatar
Tim Gymnich committed
20
        get(&arg) = LinearEquality(&arg);
Tim Gymnich's avatar
Tim Gymnich committed
21
        validVariables.insert(&arg);
Tim Gymnich's avatar
Tim Gymnich committed
22
    }
Tim Gymnich's avatar
Tim Gymnich committed
23
    isBottom = f.arg_empty();
Tim Gymnich's avatar
Tim Gymnich committed
24
}
Tim Gymnich's avatar
Tim Gymnich committed
25

Tim Gymnich's avatar
Tim Gymnich committed
26
NormalizedConjunction::NormalizedConjunction(Function const* callee_func, NormalizedConjunction const& state, CallInst const* call) {
Tim Gymnich's avatar
Tim Gymnich committed
27
    assert(callee_func->arg_size() == call->getNumArgOperands());
Tim Gymnich's avatar
Tim Gymnich committed
28
29
    for (Argument const& arg: callee_func->args()) {
        Value* value = call->getArgOperand(arg.getArgNo());
Tim Gymnich's avatar
Tim Gymnich committed
30
        if (value->getType()->isIntegerTy()) {
Tim Gymnich's avatar
Tim Gymnich committed
31
            if (ConstantInt const* c = dyn_cast<ConstantInt>(value)) {
Tim Gymnich's avatar
Tim Gymnich committed
32
                get(&arg) = { &arg, 1 , nullptr, c->getSExtValue() };
Tim Gymnich's avatar
Tim Gymnich committed
33
            } else if (state.values.count(value) > 0) {
Tim Gymnich's avatar
Tim Gymnich committed
34
                LinearEquality value_equality = state.values.at(value);
Tim Gymnich's avatar
Tim Gymnich committed
35
                LinearEquality eq = { &arg, value_equality.a , value_equality.x, value_equality.b };
Tim Gymnich's avatar
Tim Gymnich committed
36
                get(&arg) = { &arg, value_equality.a , value_equality.x, value_equality.b };
Tim Gymnich's avatar
Tim Gymnich committed
37
38
            } else {
                get(&arg) = { &arg, 1 , value, 0 };
Tim Gymnich's avatar
Tim Gymnich committed
39
            }
Tim Gymnich's avatar
Tim Gymnich committed
40
            validVariables.insert(&arg);
Tim Gymnich's avatar
Tim Gymnich committed
41
        }
Tim Gymnich's avatar
Tim Gymnich committed
42
    }
Tim Gymnich's avatar
Tim Gymnich committed
43
    isBottom = false;
Tim Gymnich's avatar
Tim Gymnich committed
44
45
}

Tim Gymnich's avatar
Tim Gymnich committed
46
NormalizedConjunction::NormalizedConjunction(std::unordered_map<Value const*, LinearEquality> const& equalaties) {
Tim Gymnich's avatar
Tim Gymnich committed
47
    this->values = equalaties;
Tim Gymnich's avatar
Tim Gymnich committed
48
    isBottom = equalaties.empty();
Tim Gymnich's avatar
Tim Gymnich committed
49
50
51
    for (auto& [key, value]: equalaties) {
        validVariables.insert(key);
    }
Tim Gymnich's avatar
Tim Gymnich committed
52
53
54
}


Tim Gymnich's avatar
Tim Gymnich committed
55
56
57
// MARK: - AbstractState Interface

/// Handles the evaluation of merging points
Tim Gymnich's avatar
Tim Gymnich committed
58
59
60
void NormalizedConjunction::applyPHINode(BasicBlock const& bb, std::vector<NormalizedConjunction> pred_values,
                  Instruction const& phi) {
    PHINode const* phiNode = dyn_cast<PHINode>(&phi);
Tim Gymnich's avatar
Tim Gymnich committed
61
62
63
64
65
66
67

    int i = 0;

    for (BasicBlock const* pred_bb: llvm::predecessors(&bb)) {
        auto& incoming_value = *phiNode->getIncomingValueForBlock(pred_bb);
        auto& incoming_state = pred_values[i];

Tim Gymnich's avatar
Tim Gymnich committed
68
        if (ConstantInt const* c = dyn_cast<ConstantInt>(&incoming_value)) {
Tim Gymnich's avatar
Tim Gymnich committed
69
70
71
72
73
            NormalizedConjunction acc = *this;
            acc.linearAssignment(&phi, 1, nullptr, c->getSExtValue());
            merge(Merge_op::UPPER_BOUND, acc);
        } else if (incoming_state.values.count(&incoming_value) != 0) {
            NormalizedConjunction acc = *this;
Tim Gymnich's avatar
Tim Gymnich committed
74
            LinearEquality pred_value = incoming_state[&incoming_value];
Tim Gymnich's avatar
Tim Gymnich committed
75
76
            acc.linearAssignment(&phi, pred_value.a, pred_value.x, pred_value.b);
            merge(Merge_op::UPPER_BOUND, acc);
Tim Gymnich's avatar
Tim Gymnich committed
77
78
79
80
     } else {
          NormalizedConjunction acc = *this;
          acc.nonDeterminsticAssignment(&phi);
          merge(Merge_op::UPPER_BOUND, acc);
Tim Gymnich's avatar
Tim Gymnich committed
81
82
        }
        i++;
Tim Gymnich's avatar
Tim Gymnich committed
83
84
85
    }
}

Tim Gymnich's avatar
Tim Gymnich committed
86
void NormalizedConjunction::applyCallInst(Instruction const& inst, BasicBlock const* end_block, NormalizedConjunction const& callee_state) {
Tim Gymnich's avatar
Tim Gymnich committed
87
88
89
90
    std::vector<LinearEquality> operands;

    //iterate through all instructions of it till we find a return statement
    for (auto& iter_inst: *end_block) {
Tim Gymnich's avatar
Tim Gymnich committed
91
92
        if (ReturnInst const* ret_inst = dyn_cast<ReturnInst>(&iter_inst)) {
            Value const* ret_val = ret_inst->getReturnValue();
Tim Gymnich's avatar
Tim Gymnich committed
93
94
95
            dbgs(4) << "\t\tFound return instruction\n";
            if (callee_state.values.find(ret_val) != callee_state.values.end()) {
                dbgs(4) << "\t\tReturn evaluated, merging parameters\n";
96
                LinearEquality retEq = callee_state.values.at(ret_val);
Tim Gymnich's avatar
Tim Gymnich committed
97
                get(&inst) = {&inst, retEq.a, retEq.x, retEq.b};
Tim Gymnich's avatar
Tim Gymnich committed
98
                validVariables.insert(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
99
100
101
102
103
104
105
            } else {
                dbgs(4) << "\t\tReturn not evaluated, setting to bottom\n";
            }
        }
    }
}

Tim Gymnich's avatar
Tim Gymnich committed
106
107
void NormalizedConjunction::applyReturnInst(Instruction const& inst) {
    Value const* ret_val = dyn_cast<ReturnInst>(&inst)->getReturnValue();
Tim Gymnich's avatar
Tim Gymnich committed
108
    if (ret_val && ret_val->getType()->isIntegerTy()) {
Tim Gymnich's avatar
Tim Gymnich committed
109
        if (ConstantInt const* c = dyn_cast<ConstantInt>(ret_val)) {
Tim Gymnich's avatar
Tim Gymnich committed
110
            get(&inst) = LinearEquality(c);
Tim Gymnich's avatar
Tim Gymnich committed
111
        } else if (values.find(ret_val) != values.end()) {
112
            LinearEquality eq = values.at(ret_val);
Tim Gymnich's avatar
Tim Gymnich committed
113
            get(&inst) = {&inst, eq.a, eq.x, eq.b};
Tim Gymnich's avatar
Tim Gymnich committed
114
115
        }
    }
Tim Gymnich's avatar
Tim Gymnich committed
116
    validVariables.insert(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
117
118
}

Tim Gymnich's avatar
Tim Gymnich committed
119
void NormalizedConjunction::applyDefault(Instruction const& inst) {
Tim Gymnich's avatar
Tim Gymnich committed
120
    std::vector<LinearEquality> operands;
Tim Gymnich's avatar
Tim Gymnich committed
121
    
Tim Gymnich's avatar
Tim Gymnich committed
122
    if (inst.getNumOperands() != 2) return nonDeterminsticAssignment(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
123
124

    // We only deal with integer types
Tim Gymnich's avatar
Tim Gymnich committed
125
    IntegerType const* type = dyn_cast<IntegerType>(inst.getType());
Tim Gymnich's avatar
Tim Gymnich committed
126
    if (not type) return nonDeterminsticAssignment(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
127
    
Tim Gymnich's avatar
Tim Gymnich committed
128
    type = dyn_cast<IntegerType>(inst.getOperand(0)->getType());
Tim Gymnich's avatar
Tim Gymnich committed
129
    if (not type) return nonDeterminsticAssignment(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
130
    
Tim Gymnich's avatar
Tim Gymnich committed
131
    type = dyn_cast<IntegerType>(inst.getOperand(1)->getType());
Tim Gymnich's avatar
Tim Gymnich committed
132
    if (not type) return nonDeterminsticAssignment(&inst);
133

134
135
136
137
    if (isa<UndefValue>(inst.getOperand(0)) || isa<UndefValue>(inst.getOperand(1))) {
        return nonDeterminsticAssignment(&inst);
    }
    
Tim Gymnich's avatar
Tim Gymnich committed
138
    for (Value const* value: inst.operand_values()) {
Tim Gymnich's avatar
Tim Gymnich committed
139
140
        operands.push_back(LinearEquality(value));
    }
Tim Gymnich's avatar
Tim Gymnich committed
141
142
    
    switch (inst.getOpcode()) {
Tim Gymnich's avatar
Tim Gymnich committed
143
        case Instruction::Add:
Tim Gymnich's avatar
Tim Gymnich committed
144
            return Add(inst);
Tim Gymnich's avatar
Tim Gymnich committed
145
        case Instruction::Sub:
Tim Gymnich's avatar
Tim Gymnich committed
146
            return Sub(inst);
Tim Gymnich's avatar
Tim Gymnich committed
147
        case Instruction::Mul:
Tim Gymnich's avatar
Tim Gymnich committed
148
            return Mul(inst);
Tim Gymnich's avatar
Tim Gymnich committed
149
150
        case Instruction::SDiv:
        case Instruction::UDiv:
Tim Gymnich's avatar
Tim Gymnich committed
151
        default:
Tim Gymnich's avatar
Tim Gymnich committed
152
            return nonDeterminsticAssignment(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
153
    }
Tim Gymnich's avatar
Tim Gymnich committed
154
155

    debug_output(inst, operands);
Tim Gymnich's avatar
Tim Gymnich committed
156
157
}

Tim Gymnich's avatar
Tim Gymnich committed
158
bool NormalizedConjunction::merge(Merge_op::Type op, NormalizedConjunction const& other) {
Tim Gymnich's avatar
Tim Gymnich committed
159
160
161
162
    if (other.isBottom) {
        return false;
    } else if (isBottom) {
        values = other.values;
Tim Gymnich's avatar
Tim Gymnich committed
163
        validVariables = other.validVariables;
Tim Gymnich's avatar
Tim Gymnich committed
164
165
166
167
        isBottom = false;
        return true;
    }

Tim Gymnich's avatar
Tim Gymnich committed
168
169
170
171
    switch (op) {
        case Merge_op::UPPER_BOUND: return leastUpperBound(other);
        default: abort();
    }
Tim Gymnich's avatar
Tim Gymnich committed
172
173
}

Tim Gymnich's avatar
Tim Gymnich committed
174
// MARK: - Lattice Operations
Tim Gymnich's avatar
Tim Gymnich committed
175

Tim Gymnich's avatar
Tim Gymnich committed
176
177
178
179
bool NormalizedConjunction::leastUpperBound(NormalizedConjunction rhs) {
    // set of all occuring variables in E1 and E2
    std::set<Value const*> vars, varsE1, varsE2;
    std::set<LinearEquality> E1, E2;
Tim Gymnich's avatar
Tim Gymnich committed
180

Tim Gymnich's avatar
Tim Gymnich committed
181
182
183
    auto mapToSeccond = [](std::pair<Value const*, LinearEquality> p){ return p.second; };
    transform(values, std::inserter(E1, E1.end()), mapToSeccond);
    transform(rhs.values, std::inserter(E2, E2.end()), mapToSeccond);
Tim Gymnich's avatar
Tim Gymnich committed
184
    
Tim Gymnich's avatar
Tim Gymnich committed
185
186
187
188
189
190
191
192
193
194
195
196
    auto mapToY = [](LinearEquality eq){ return eq.y; };
    transform(E1, std::inserter(varsE1, varsE1.end()), mapToY);
    transform(E2, std::inserter(varsE2, varsE2.end()), mapToY);
    std::set_union(varsE1.begin(), varsE1.end(), varsE2.begin(), varsE2.end(), std::inserter(vars, vars.end()));
    
    std::set<Value const*> dX1, dX2;
    
    std::set_difference(vars.begin(), vars.end(), varsE1.begin(), varsE1.end(), std::inserter(dX1, dX1.end()));
    std::set_difference(vars.begin(), vars.end(), varsE2.begin(), varsE2.end(), std::inserter(dX2, dX2.end()));
            
    // extend E1 by trivial equalities
    for (auto d: dX1) {
Tim Gymnich's avatar
Tim Gymnich committed
197
198
199
200
        if (validVariables.count(d) > 0) {
            LinearEquality eq = {d, 1, d, 0};
            E1.insert(eq);
        } else {
Tim Gymnich's avatar
Tim Gymnich committed
201
            E1.insert(rhs[d]);
Tim Gymnich's avatar
Tim Gymnich committed
202
        }
Tim Gymnich's avatar
Tim Gymnich committed
203
    }
Tim Gymnich's avatar
Tim Gymnich committed
204
205
206
    
    // extend E2 by trivial equalities
    for (auto d: dX2) {
Tim Gymnich's avatar
Tim Gymnich committed
207
208
209
210
        if (rhs.validVariables.count(d) > 0) {
            LinearEquality eq = {d, 1, d, 0};
            E2.insert(eq);
        } else {
Tim Gymnich's avatar
Tim Gymnich committed
211
            E2.insert(operator[](d));
Tim Gymnich's avatar
Tim Gymnich committed
212
        }
Tim Gymnich's avatar
Tim Gymnich committed
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
    }
    
    std::set<LinearEquality> X0 = computeX0(E1, E2);
    std::set<LinearEquality> X1 = computeX1(E1, E2);
    std::set<LinearEquality> X2 = computeX2(E1, E2);
    std::set<LinearEquality> X3 = computeX2(E2, E1);
    std::set<LinearEquality> X4 = computeX4(E1, E2);
    
    // E1 U E2 = E'0 AND E'1 AND E'2 AND E'3 AND E'4
    
    std::set<LinearEquality> leastUpperBound;
    leastUpperBound.insert(X0.begin(), X0.end());
    leastUpperBound.insert(X1.begin(), X1.end());
    leastUpperBound.insert(X2.begin(), X2.end());
    leastUpperBound.insert(X3.begin(), X3.end());
    leastUpperBound.insert(X4.begin(), X4.end());
    
    std::unordered_map<Value const*, LinearEquality> result;
    
    auto addMapping = [](LinearEquality eq){ return std::make_pair(eq.y,eq); };
    transform(leastUpperBound, std::inserter(result, result.end()), addMapping);
Tim Gymnich's avatar
Tim Gymnich committed
234

Tim Gymnich's avatar
Tim Gymnich committed
235
236
    bool changed = values != result;
    
Tim Gymnich's avatar
Tim Gymnich committed
237
    values = result;
Tim Gymnich's avatar
Tim Gymnich committed
238
    validVariables.insert(rhs.validVariables.begin(), rhs.validVariables.end());
Tim Gymnich's avatar
Tim Gymnich committed
239

Tim Gymnich's avatar
Tim Gymnich committed
240
    return changed;
Tim Gymnich's avatar
Tim Gymnich committed
241
}
Tim Gymnich's avatar
Tim Gymnich committed
242

Tim Gymnich's avatar
Tim Gymnich committed
243
244
// MARK: Helpers

Tim Gymnich's avatar
Tim Gymnich committed
245
/// XO / E'0: set of variables where the right hand side in E1 and E2 coincide
Tim Gymnich's avatar
Tim Gymnich committed
246
247
std::set<LinearEquality> NormalizedConjunction::computeX0(std::set<LinearEquality> const& E1, std::set<LinearEquality> const& E2) {
    std::set<LinearEquality> X0;
Tim Gymnich's avatar
Tim Gymnich committed
248
249
    std::set_intersection(E1.begin(), E1.end(), E2.begin(), E2.end(), std::inserter(X0, X0.end()));
    // Remove trivial equalities
Tim Gymnich's avatar
Tim Gymnich committed
250
251
    std::set<LinearEquality> filteredX0;
    auto filterTrivialEqualaties = [](LinearEquality eq){ return eq.y != eq.x;};
Tim Gymnich's avatar
Tim Gymnich committed
252
    copy_if(X0, std::inserter(filteredX0, filteredX0.end()), filterTrivialEqualaties);
Tim Gymnich's avatar
Tim Gymnich committed
253
    
Tim Gymnich's avatar
Tim Gymnich committed
254
255
256
257
    return filteredX0;
}

/// X1 / E'1: set of variables where the right hand side is constant but does not coincide in E1 and E2
Tim Gymnich's avatar
Tim Gymnich committed
258
259
260
std::set<LinearEquality> NormalizedConjunction::computeX1(std::set<LinearEquality> const& E1, std::set<LinearEquality> const& E2) {
    std::set<LinearEquality> X1;
    std::set<std::pair<LinearEquality, LinearEquality>> differentConstants;
Tim Gymnich's avatar
Tim Gymnich committed
261
262
    
    assert(E1.size() == E2.size() && "E1 and E2 should have the same set of variables in the same order");
Tim Gymnich's avatar
Tim Gymnich committed
263
264
265
266
267
268
269
    
    for (auto itE1 = E1.begin(), itE2 = E2.begin(); itE1 != E1.end() && itE2 != E2.end(); ++itE1, ++itE2) {
        auto eq1 = *itE1;
        auto eq2 = *itE2;
        assert(eq1.y == eq2.y && "left hand side of equations should be the same");
        if (eq1.isConstant() && eq2.isConstant() && eq1.b != eq2.b) {
            differentConstants.insert({eq1,eq2});
Tim Gymnich's avatar
Tim Gymnich committed
270
        }
Tim Gymnich's avatar
Tim Gymnich committed
271
272
273
274
    }
    
    if (!differentConstants.empty()) {
        // pop first element
Tim Gymnich's avatar
Tim Gymnich committed
275
        std::pair<LinearEquality, LinearEquality> h = *differentConstants.begin();
Tim Gymnich's avatar
Tim Gymnich committed
276
        differentConstants.erase(differentConstants.begin());
Tim Gymnich's avatar
Tim Gymnich committed
277
        
Tim Gymnich's avatar
Tim Gymnich committed
278
279
280
281
        for (auto i: differentConstants) {
            // find a linear equation that contains both points P1(c(1)i, c(1)h) and P2(c(2)i, c(2)h)
            // y = a * x + b
            auto y = i.first.y;
Tim Gymnich's avatar
Tim Gymnich committed
282
283
            int64_t a = ((i.second.b - i.first.b)) / (h.second.b - h.first.b);
            auto x = h.first.y;
Tim Gymnich's avatar
Tim Gymnich committed
284
            int64_t b = -a * h.first.b + i.first.b;
Tim Gymnich's avatar
Tim Gymnich committed
285
            LinearEquality eq = {y, a, x, b};
Tim Gymnich's avatar
Tim Gymnich committed
286
            X1.insert(eq);
Tim Gymnich's avatar
Tim Gymnich committed
287
        }
Tim Gymnich's avatar
Tim Gymnich committed
288
    }
Tim Gymnich's avatar
Tim Gymnich committed
289
290
291
292
    return X1;
}

/// X2 / E'2: set of variables where the right hand side of E1 is constant but the rhs of E2 contains a variable.
Tim Gymnich's avatar
Tim Gymnich committed
293
294
295
std::set<LinearEquality> NormalizedConjunction::computeX2(std::set<LinearEquality> const& E1, std::set<LinearEquality> const& E2) {
    std::set<LinearEquality> X2;
    std::set<std::pair<LinearEquality, LinearEquality>> differentConstants;
Tim Gymnich's avatar
Tim Gymnich committed
296
    
Tim Gymnich's avatar
Tim Gymnich committed
297
    assert(E1.size() == E2.size() && "E1 and E2 should have the same set of variables in the same order");
Tim Gymnich's avatar
Tim Gymnich committed
298
    
Tim Gymnich's avatar
Tim Gymnich committed
299
300
301
302
303
304
    for (auto itE1 = E1.begin(), itE2 = E2.begin(); itE1 != E1.end() && itE2 != E2.end(); ++itE1, ++itE2) {
        auto eq1 = *itE1;
        auto eq2 = *itE2;
        assert(eq1.y == eq2.y && "left hand side of equations should be the same");
        if (eq1.isConstant() && !eq2.isConstant()) {
            differentConstants.insert({eq1,eq2});
Tim Gymnich's avatar
Tim Gymnich committed
305
306
307
        }
    }
    
Tim Gymnich's avatar
Tim Gymnich committed
308
    std::vector<std::set<std::pair<LinearEquality, LinearEquality>>> Pi2;
Tim Gymnich's avatar
Tim Gymnich committed
309
    
Tim Gymnich's avatar
Tim Gymnich committed
310
    for (auto jt = differentConstants.begin(); jt != differentConstants.end();) {
Tim Gymnich's avatar
Tim Gymnich committed
311
        std::set<std::pair<LinearEquality, LinearEquality>> equivalenceClass;
Tim Gymnich's avatar
Tim Gymnich committed
312
313
314
        auto j = *jt;
        equivalenceClass.insert(j);
        jt = differentConstants.erase(jt);
Tim Gymnich's avatar
Tim Gymnich committed
315
        
Tim Gymnich's avatar
Tim Gymnich committed
316
317
318
319
320
        // partition differentConstants
        for (auto it = jt; it != differentConstants.end(); ) {
            auto i = *it;
            bool condition1 = i.second.x == j.second.x;
            bool condition2 = (i.first.b - i.second.b) / (i.second.a) == (j.first.b - j.second.b) / (j.second.a);
Tim Gymnich's avatar
Tim Gymnich committed
321
            if (condition1 && condition2) {
Tim Gymnich's avatar
Tim Gymnich committed
322
323
324
325
326
                equivalenceClass.insert(i);
                it = differentConstants.erase(it);
                jt = differentConstants.begin();
            } else {
                it++;
Tim Gymnich's avatar
Tim Gymnich committed
327
            }
Tim Gymnich's avatar
Tim Gymnich committed
328
        }
Tim Gymnich's avatar
Tim Gymnich committed
329
                
Tim Gymnich's avatar
Tim Gymnich committed
330
        Pi2.push_back(equivalenceClass);
Tim Gymnich's avatar
Tim Gymnich committed
331
    }
Tim Gymnich's avatar
Tim Gymnich committed
332
    
Tim Gymnich's avatar
Tim Gymnich committed
333
334
    // form equaltites for partitions in Pi2
    for (auto q: Pi2) {
Tim Gymnich's avatar
Tim Gymnich committed
335
        auto h = *q.begin();
Tim Gymnich's avatar
Tim Gymnich committed
336
337
338
339
        q.erase(q.begin());
        for (auto i: q) {
            // xi = ai/ah * xh + ( bi - (ai * bh) / ah)
            auto y = i.first.y;
Tim Gymnich's avatar
Tim Gymnich committed
340
            auto a = i.second.a / h.second.a;
Tim Gymnich's avatar
Tim Gymnich committed
341
            auto x = h.first.y;
Tim Gymnich's avatar
Tim Gymnich committed
342
            auto b = i.second.b - (i.second.a * h.second.b) / h.second.a;
Tim Gymnich's avatar
Tim Gymnich committed
343
            LinearEquality eq = {y, a, x, b};
Tim Gymnich's avatar
Tim Gymnich committed
344
345
346
            X2.insert(eq);
        }
    }
Tim Gymnich's avatar
Tim Gymnich committed
347
348
349
    return X2;
}

Tim Gymnich's avatar
Tim Gymnich committed
350
351
352
std::set<LinearEquality> NormalizedConjunction::computeX4(std::set<LinearEquality> const& E1, std::set<LinearEquality> const& E2) {
    std::set<LinearEquality> X4;
    std::set<std::pair<LinearEquality, LinearEquality>> differentConstants;
Tim Gymnich's avatar
Tim Gymnich committed
353
    
Tim Gymnich's avatar
Tim Gymnich committed
354
    assert(E1.size() == E2.size() && "E1 and E2 should have the same set of variables in the same order");
Tim Gymnich's avatar
Tim Gymnich committed
355
    
Tim Gymnich's avatar
Tim Gymnich committed
356
357
358
359
    for (auto itE1 = E1.begin(), itE2 = E2.begin(); itE1 != E1.end() && itE2 != E2.end(); ++itE1, ++itE2) {
        auto eq1 = *itE1;
        auto eq2 = *itE2;
        assert(eq1.y == eq2.y && "left hand side of equations should be the same");
Tim Gymnich's avatar
Tim Gymnich committed
360
        if (!eq1.isConstant() && !eq2.isConstant() && eq1 != eq2) {
Tim Gymnich's avatar
Tim Gymnich committed
361
            differentConstants.insert({eq1,eq2});
Tim Gymnich's avatar
Tim Gymnich committed
362
        }
Tim Gymnich's avatar
Tim Gymnich committed
363
364
    }
    
Tim Gymnich's avatar
Tim Gymnich committed
365
    std::vector<std::set<std::pair<LinearEquality, LinearEquality>>> Pi4;
Tim Gymnich's avatar
Tim Gymnich committed
366
367
    
    // partition differentConstants
Tim Gymnich's avatar
Tim Gymnich committed
368
    for (auto it = differentConstants.begin(); it != differentConstants.end();) {
Tim Gymnich's avatar
Tim Gymnich committed
369
370
        std::set<std::pair<LinearEquality, LinearEquality>> equivalenceClass;
        std::pair<LinearEquality, LinearEquality> i = *it;
Tim Gymnich's avatar
Tim Gymnich committed
371
372
373
374
        equivalenceClass.insert(i);
        it = differentConstants.erase(it);
        
        for (auto jt = it; jt != differentConstants.end(); ) {
Tim Gymnich's avatar
Tim Gymnich committed
375
            std::pair<LinearEquality, LinearEquality> j = *jt;
Tim Gymnich's avatar
Tim Gymnich committed
376
377
378
            bool condition1 = i.first.x == j.first.x && i.second.x == j.second.x;
            bool condition2 = i.second.a / (i.first.a) == j.second.a / (j.first.a);
            bool condition3 = (i.first.b - i.second.b) / (i.first.a) == (j.first.b - j.second.b) / (j.first.a);
Tim Gymnich's avatar
Tim Gymnich committed
379
            if (condition1 && condition2 && condition3) {
Tim Gymnich's avatar
Tim Gymnich committed
380
381
382
383
384
                equivalenceClass.insert(j);
                jt = differentConstants.erase(jt);
                it = differentConstants.begin();
            } else {
                jt++;
Tim Gymnich's avatar
Tim Gymnich committed
385
386
            }
        }
Tim Gymnich's avatar
Tim Gymnich committed
387

Tim Gymnich's avatar
Tim Gymnich committed
388
389
390
391
392
393
394
395
396
397
        Pi4.push_back(equivalenceClass);
    }
    
    // form equaltites for partitions in Pi4
    for (auto q: Pi4) {
        auto h = *q.begin();
        q.erase(q.begin());
        for (auto i: q) {
            // xi = ai/ah * xh + ( bi - (ai * bh) / ah)
            auto y = i.first.y;
Tim Gymnich's avatar
Tim Gymnich committed
398
            auto a = i.second.a / h.second.a;
Tim Gymnich's avatar
Tim Gymnich committed
399
400
            auto x = h.first.y;
            auto b = i.second.b - (i.second.a * h.second.b) / (h.second.a);
Tim Gymnich's avatar
Tim Gymnich committed
401
            LinearEquality eq = {y, a, x, b};
Tim Gymnich's avatar
Tim Gymnich committed
402
            X4.insert(eq);
Tim Gymnich's avatar
Tim Gymnich committed
403
        }
Tim Gymnich's avatar
Tim Gymnich committed
404
405
406
407
    }
    return X4;
}

Tim Gymnich's avatar
Tim Gymnich committed
408
// MARK: - Abstract Assignments
Tim Gymnich's avatar
Tim Gymnich committed
409

Tim Gymnich's avatar
Tim Gymnich committed
410
/// [xi := ?]
Tim Gymnich's avatar
Tim Gymnich committed
411
void NormalizedConjunction::nonDeterminsticAssignment(Value const* xi) {
Tim Gymnich's avatar
Tim Gymnich committed
412
    assert(xi != nullptr && "xi cannot be NULL");
Tim Gymnich's avatar
Tim Gymnich committed
413
    auto xj = get(xi).x;
Tim Gymnich's avatar
Tim Gymnich committed
414
    validVariables.insert(xi);
Tim Gymnich's avatar
Tim Gymnich committed
415
    
Tim Gymnich's avatar
Tim Gymnich committed
416
    if (xi != xj && xj != 0) {
Tim Gymnich's avatar
Tim Gymnich committed
417
        get(xi) = {xi, 1, xi, 0};
Tim Gymnich's avatar
Tim Gymnich committed
418
419
    } else {
        // find all equations using xi
Tim Gymnich's avatar
Tim Gymnich committed
420
421
422
        auto predicate = [&xi](std::pair<Value const*, LinearEquality> p){ return p.second.x == xi && p.second.y != xi ;};
        auto it = std::find_if(values.begin(), values.end(), predicate);
        if (it != values.end()) {
Tim Gymnich's avatar
Tim Gymnich committed
423
            auto xk = (*it).second;
Tim Gymnich's avatar
Tim Gymnich committed
424
425
426
            for (it = std::find_if(++it, values.end(), predicate);
                 it != values.end();
                 it = std::find_if(++it, values.end(), predicate)) {
Tim Gymnich's avatar
Tim Gymnich committed
427
                auto& xl = it->second;
Tim Gymnich's avatar
Tim Gymnich committed
428
                get(xl.y) = {xl.y, 1, xk.y, xl.b - xk.b};
Tim Gymnich's avatar
Tim Gymnich committed
429
            }
Tim Gymnich's avatar
Tim Gymnich committed
430
            get(xk.y) = {xk.y, 1, xk.y, 0};
Tim Gymnich's avatar
Tim Gymnich committed
431
        }
Tim Gymnich's avatar
Tim Gymnich committed
432
        get(xi) = {xi, 1, xi, 0};
Tim Gymnich's avatar
Tim Gymnich committed
433
    }
Tim Gymnich's avatar
Tim Gymnich committed
434

Tim Gymnich's avatar
Tim Gymnich committed
435
436
437
}

/// [xi := a * xj + b]
Tim Gymnich's avatar
Tim Gymnich committed
438
void NormalizedConjunction::linearAssignment(Value const* xi, int64_t a, Value const* xj, int64_t b) {
Tim Gymnich's avatar
Tim Gymnich committed
439
440
    assert(xi != nullptr && "xi cannot be NULL");

Tim Gymnich's avatar
Tim Gymnich committed
441
    nonDeterminsticAssignment(xi);
Tim Gymnich's avatar
Tim Gymnich committed
442
443
    validVariables.insert(xi);

Tim Gymnich's avatar
Tim Gymnich committed
444
    // make sure xj exists
Tim Gymnich's avatar
Tim Gymnich committed
445
    auto xjS = values.find(xj) != values.end() ? get(xj).x : xj;
Tim Gymnich's avatar
Tim Gymnich committed
446
447
    auto bS = values.find(xj) != values.end() ? get(xj).b : 0;
    auto aS = values.find(xj) != values.end() ? get(xj).a : 1;
448
449
450
    
    if (!(a % aS == 0 && (-bS - b) % aS == 0)) {
        // Precison loss due to int division! Abort
Tim Gymnich's avatar
Tim Gymnich committed
451
        return;
452
    }
Tim Gymnich's avatar
Tim Gymnich committed
453
454
    
    if (xi > xjS) {
Tim Gymnich's avatar
Tim Gymnich committed
455
        get(xi) = {xi, aS * a, xjS, a * bS + b};
Tim Gymnich's avatar
Tim Gymnich committed
456
        return;
Tim Gymnich's avatar
Tim Gymnich committed
457
    } else {
Tim Gymnich's avatar
Tim Gymnich committed
458
459
        auto pred = [&xjS](std::pair<Value const*, LinearEquality> p){ return p.second.x == xjS && p.second.y != xjS; };
        for (auto xk: make_filter_range(values, pred)) {
Tim Gymnich's avatar
Tim Gymnich committed
460
            get(xk.second.y) = {xk.second.y, xk.second.a * a/aS, xi, (-bS - b) / aS + xk.second.b};
Tim Gymnich's avatar
Tim Gymnich committed
461
        }
Tim Gymnich's avatar
Tim Gymnich committed
462
        get(xjS) = {xjS, a/aS, xi, (-bS - b) / aS};
Tim Gymnich's avatar
Tim Gymnich committed
463
464
465
    }
}

Tim Gymnich's avatar
Tim Gymnich committed
466
// MARK: - Abstract Operations
Tim Gymnich's avatar
Tim Gymnich committed
467

Tim Gymnich's avatar
Tim Gymnich committed
468
// [xi := xj + b]
Tim Gymnich's avatar
Tim Gymnich committed
469
// [xi := xj + xk]
Tim Gymnich's avatar
Tim Gymnich committed
470
// [xi := bj + bk]
Tim Gymnich's avatar
Tim Gymnich committed
471
void NormalizedConjunction::Add(Instruction const& inst) {
Tim Gymnich's avatar
Tim Gymnich committed
472
473
474
    auto op1 = inst.getOperand(0);
    auto op2 = inst.getOperand(1);
    
Tim Gymnich's avatar
Tim Gymnich committed
475
476
477
478
479
    // [xi := bj + bk]
    if (isa<ConstantInt>(op1) && (isa<ConstantInt>(op2))) {
        auto b1 = dyn_cast<ConstantInt>(op1);
        auto b2 = dyn_cast<ConstantInt>(op2);
        return linearAssignment(&inst, 1, nullptr, b1->getSExtValue() + b2->getSExtValue() );
Tim Gymnich's avatar
Tim Gymnich committed
480
    // [xi := b + xj]
Tim Gymnich's avatar
Tim Gymnich committed
481
    }  else if (isa<ConstantInt>(op1) && isa<Value>(op2)) {
Tim Gymnich's avatar
Tim Gymnich committed
482
        auto b = dyn_cast<ConstantInt>(op1);
Tim Gymnich's avatar
Tim Gymnich committed
483
        return linearAssignment(&inst, 1, op2, b->getSExtValue());
Tim Gymnich's avatar
Tim Gymnich committed
484
    // [xi := xj + b]
Tim Gymnich's avatar
Tim Gymnich committed
485
    } else if (isa<ConstantInt>(op2) && isa<Value>(op1)) {
Tim Gymnich's avatar
Tim Gymnich committed
486
        auto b = dyn_cast<ConstantInt>(op2);
Tim Gymnich's avatar
Tim Gymnich committed
487
        return linearAssignment(&inst, 1, op1, b->getSExtValue());
Tim Gymnich's avatar
Tim Gymnich committed
488
    // [xi := xj + xk]
Tim Gymnich's avatar
Tim Gymnich committed
489
    } else if (isa<Value>(op1) && isa<Value>(op2)) {
Tim Gymnich's avatar
Tim Gymnich committed
490
        // [xi := bj + xk]
Tim Gymnich's avatar
Tim Gymnich committed
491
492
        if (get(op1).isConstant()) {
            return linearAssignment(&inst, 1, op2, get(op1).b);
Tim Gymnich's avatar
Tim Gymnich committed
493
        // [xi := xj + bk]
Tim Gymnich's avatar
Tim Gymnich committed
494
495
        } else if (get(op2).isConstant()) {
            return linearAssignment(&inst, 1, op1, get(op2).b);
Tim Gymnich's avatar
Tim Gymnich committed
496
        // [xi := xj + xk]
Tim Gymnich's avatar
Tim Gymnich committed
497
        } else {
Tim Gymnich's avatar
Tim Gymnich committed
498
            return nonDeterminsticAssignment(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
499
        }
Tim Gymnich's avatar
Tim Gymnich committed
500
    // [xi := bj + bk]
Tim Gymnich's avatar
Tim Gymnich committed
501
502
    } else {
        assert(false);
Tim Gymnich's avatar
Tim Gymnich committed
503
        return nonDeterminsticAssignment(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
504
505
506
    }
}

Tim Gymnich's avatar
Tim Gymnich committed
507
508
/// [xi := xj - x]
void NormalizedConjunction::Sub(Instruction const& inst) {
Tim Gymnich's avatar
Tim Gymnich committed
509
510
511
   auto op1 = inst.getOperand(0);
   auto op2 = inst.getOperand(1);
   
Tim Gymnich's avatar
Tim Gymnich committed
512
513
514
515
516
517
518
    // [xi := bj - bk]
    if (isa<ConstantInt>(op1) && (isa<ConstantInt>(op2))) {
        auto b1 = dyn_cast<ConstantInt>(op1);
        auto b2 = dyn_cast<ConstantInt>(op2);
        return linearAssignment(&inst, 1, nullptr, b1->getSExtValue() - b2->getSExtValue() );
    // [xi := b - xj]
    } else if (isa<ConstantInt>(op1) && isa<Value>(op2)) {
Tim Gymnich's avatar
Tim Gymnich committed
519
       auto b = dyn_cast<ConstantInt>(op1);
Tim Gymnich's avatar
Tim Gymnich committed
520
       return linearAssignment(&inst, 1, op2, -b->getSExtValue());
Tim Gymnich's avatar
Tim Gymnich committed
521
522
523
   // [xi := xj - b]
   } else if (isa<ConstantInt>(op2) && isa<Value>(op1)) {
       auto b = dyn_cast<ConstantInt>(op2);
Tim Gymnich's avatar
Tim Gymnich committed
524
       return linearAssignment(&inst, 1, op1, -b->getSExtValue());
Tim Gymnich's avatar
Tim Gymnich committed
525
526
527
   // [xi := xj - xk]
   } else if (isa<Value>(op1) && isa<Value>(op2)) {
       // [xi := bj - xk]
Tim Gymnich's avatar
Tim Gymnich committed
528
529
       if (get(op1).isConstant()) {
           return linearAssignment(&inst, 1, op2, -get(op1).b);
Tim Gymnich's avatar
Tim Gymnich committed
530
       // [xi := xj - bk]
Tim Gymnich's avatar
Tim Gymnich committed
531
532
       } else if (get(op2).isConstant()) {
           return linearAssignment(&inst, 1, op1, -get(op2).b);
Tim Gymnich's avatar
Tim Gymnich committed
533
534
       // [xi := xj - xk]
       } else {
Tim Gymnich's avatar
Tim Gymnich committed
535
           return nonDeterminsticAssignment(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
536
537
538
       }
   } else {
       assert(false);
Tim Gymnich's avatar
Tim Gymnich committed
539
       return nonDeterminsticAssignment(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
540
541
542
543
   }
}

// [xi := a * xj]
Tim Gymnich's avatar
Tim Gymnich committed
544
void NormalizedConjunction::Mul(Instruction const& inst) {
Tim Gymnich's avatar
Tim Gymnich committed
545
546
547
    auto op1 = inst.getOperand(0);
    auto op2 = inst.getOperand(1);
    
Tim Gymnich's avatar
Tim Gymnich committed
548
549
550
551
552
    // [xi := aj * ak]
    if (isa<ConstantInt>(op1) && (isa<ConstantInt>(op2))) {
        auto b1 = dyn_cast<ConstantInt>(op1);
        auto b2 = dyn_cast<ConstantInt>(op2);
        return linearAssignment(&inst, 1, nullptr, b1->getSExtValue() * b2->getSExtValue() );
Tim Gymnich's avatar
Tim Gymnich committed
553
    // [xi := a * xj]
Tim Gymnich's avatar
Tim Gymnich committed
554
    } else if (isa<ConstantInt>(op1) && isa<Value>(op2)) {
Tim Gymnich's avatar
Tim Gymnich committed
555
        auto a = dyn_cast<ConstantInt>(op1);
556
557
558
559
560
561
        int64_t a_val = a->getSExtValue();
        if (a_val == 0) {
            return linearAssignment(&inst, 1, nullptr, 0);
        } else {
            return linearAssignment(&inst, a_val, op2, 0);
        }
Tim Gymnich's avatar
Tim Gymnich committed
562
    // [xi := xj * a]
Tim Gymnich's avatar
Tim Gymnich committed
563
    } else if (isa<ConstantInt>(op2) && isa<Value>(op1)) {
Tim Gymnich's avatar
Tim Gymnich committed
564
        auto a = dyn_cast<ConstantInt>(op2);
565
566
567
568
569
570
        int64_t a_val = a->getSExtValue();
        if (a_val == 0) {
            return linearAssignment(&inst, 1, nullptr, 0);
        } else {
            return linearAssignment(&inst, a_val, op2, 0);
        }
Tim Gymnich's avatar
Tim Gymnich committed
571
572
573
    // [xi := xj * xk]
    } else if (isa<Value>(op1) && isa<Value>(op2)) {
        // [xi := aj * xk]
Tim Gymnich's avatar
Tim Gymnich committed
574
        if (get(op1).isConstant()) {
575
576
577
578
579
            if (get(op1).b == 0) {
                return linearAssignment(&inst, 1, nullptr, 0);
            } else {
                return linearAssignment(&inst, get(op1).b, op2, 0);
            }
Tim Gymnich's avatar
Tim Gymnich committed
580
        // [xi := xj * ak]
Tim Gymnich's avatar
Tim Gymnich committed
581
        } else if (get(op2).isConstant()) {
582
583
584
585
586
            if (get(op2).b == 0) {
                return linearAssignment(&inst, 1, nullptr, 0);
            } else {
                return linearAssignment(&inst, get(op2).b, op1, 0);
            }
Tim Gymnich's avatar
Tim Gymnich committed
587
588
        // [xi := xj * xk]
        } else {
Tim Gymnich's avatar
Tim Gymnich committed
589
            return nonDeterminsticAssignment(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
590
        }
Tim Gymnich's avatar
Tim Gymnich committed
591
592
    } else {
        assert(false);
Tim Gymnich's avatar
Tim Gymnich committed
593
        return nonDeterminsticAssignment(&inst);
Tim Gymnich's avatar
Tim Gymnich committed
594
595
596
    }
}

597
598
599
// MARK: - Operators

LinearEquality& NormalizedConjunction::operator[](Value const* value) {
Tim Gymnich's avatar
Tim Gymnich committed
600
601
602
603
    return get(value);
}

LinearEquality& NormalizedConjunction::get(Value const* value) {
604
605
606
607
608
609
610
    if (values.count(value) == 0) {
        LinearEquality eq = {value, 1, value, 0};
        values[value] = eq;
    }
    return values[value];
}

Tim Gymnich's avatar
Tim Gymnich committed
611
// MARK: - Debug
Tim Gymnich's avatar
Tim Gymnich committed
612

Tim Gymnich's avatar
Tim Gymnich committed
613
void NormalizedConjunction::debug_output(Instruction const& inst, std::vector<LinearEquality> operands) {
Tim Gymnich's avatar
Tim Gymnich committed
614
615
    dbgs(3).indent(2) << inst << " // " << values.at(&inst) << ", args ";
    {int i = 0;
Tim Gymnich's avatar
Tim Gymnich committed
616
    for (Value const* value: inst.operand_values()) {
Tim Gymnich's avatar
Tim Gymnich committed
617
618
619
620
621
622
        if (i) dbgs(3) << ", ";
        if (value->getName().size()) dbgs(3) << '%' << value->getName() << " = ";
        dbgs(3) << operands[i];
        ++i;
    }}
    dbgs(3) << '\n';
Tim Gymnich's avatar
Tim Gymnich committed
623
624
}

Tim Gymnich's avatar
Tim Gymnich committed
625
void NormalizedConjunction::printIncoming(BasicBlock const& bb, raw_ostream& out, int indentation = 0) const {
Tim Gymnich's avatar
Tim Gymnich committed
626
627
    // @Speed: This is quadratic, could be linear
    bool nothing = true;
Tim Gymnich's avatar
Tim Gymnich committed
628
    for (std::pair<Value const*, LinearEquality> const& i: values) {
Tim Gymnich's avatar
Tim Gymnich committed
629
630
        bool read    = false;
        bool written = false;
Tim Gymnich's avatar
Tim Gymnich committed
631
        for (Instruction const& inst: bb) {
Tim Gymnich's avatar
Tim Gymnich committed
632
            if (&inst == i.first) written = true;
Tim Gymnich's avatar
Tim Gymnich committed
633
            for (Value const* v: inst.operand_values()) {
Tim Gymnich's avatar
Tim Gymnich committed
634
635
636
                if (v == i.first) read = true;
            }
        }
Tim Gymnich's avatar
Tim Gymnich committed
637

Tim Gymnich's avatar
Tim Gymnich committed
638
639
640
641
642
643
644
645
        if (read and not written) {
            out.indent(indentation) << '%' << i.first->getName() << " = " << i.second << '\n';
            nothing = false;
        }
    }
    if (nothing) {
        out.indent(indentation) << "<nothing>\n";
    }
Tim Gymnich's avatar
Tim Gymnich committed
646
647
}

Tim Gymnich's avatar
Tim Gymnich committed
648
void NormalizedConjunction::printOutgoing(BasicBlock const& bb, raw_ostream& out, int indentation = 0) const {
Tim Gymnich's avatar
Tim Gymnich committed
649
    for (auto const& i: values) {
Tim Gymnich's avatar
Tim Gymnich committed
650
        if (ReturnInst::classof(i.first)) {
Tim Gymnich's avatar
Tim Gymnich committed
651
            out.indent(indentation) << "<ret> = " << i.second << '\n';
Tim Gymnich's avatar
Tim Gymnich committed
652
        } else {
Tim Gymnich's avatar
Tim Gymnich committed
653
            out.indent(indentation) << '%' << i.first->getName() << " = " << i.second << '\n';
Tim Gymnich's avatar
Tim Gymnich committed
654
655
656
657
        }
    }
}

Tim Gymnich's avatar
Tim Gymnich committed
658
} /* end of namespace pcpo */