| 46 | }; |
| 47 | |
| 48 | struct LoopLikeFunctionApproximator { |
| 49 | // input: (i, is the last iter?) |
| 50 | // output: (value, nonpoison, UB, continue?) |
| 51 | using fn_t = function<tuple<expr, expr, AndExpr, expr>(unsigned, bool)>; |
| 52 | fn_t ith_exec; |
| 53 | |
| 54 | LoopLikeFunctionApproximator(fn_t ith_exec) : ith_exec(std::move(ith_exec)) {} |
| 55 | |
| 56 | // (value, nonpoison, UB) |
| 57 | tuple<expr, expr, expr> encode(IR::State &s, unsigned unroll_cnt) { |
| 58 | AndExpr prefix; |
| 59 | return _loop(s, prefix, 0, unroll_cnt); |
| 60 | } |
| 61 | |
| 62 | // (value, nonpoison, UB) |
| 63 | tuple<expr, expr, expr> _loop(IR::State &s, AndExpr &prefix, unsigned i, |
| 64 | unsigned unroll_cnt) { |
| 65 | bool is_last = i >= unroll_cnt - 1; |
| 66 | auto [res_i, np_i, ub_i, continue_i] = ith_exec(i, is_last); |
| 67 | auto ub = ub_i(); |
| 68 | prefix.add(ub_i); |
| 69 | |
| 70 | // Keep going if the function is being applied to a constant input |
| 71 | if (i < 512) |
| 72 | is_last &= !continue_i.isConst(); |
| 73 | |
| 74 | if (is_last) |
| 75 | s.addPre(prefix().implies(!continue_i)); |
| 76 | |
| 77 | if (is_last || continue_i.isFalse() || ub.isFalse() || !s.isViablePath()) |
| 78 | return { std::move(res_i), std::move(np_i), std::move(ub) }; |
| 79 | |
| 80 | prefix.add(continue_i); |
| 81 | auto [val_next, np_next, ub_next] = _loop(s, prefix, i + 1, unroll_cnt); |
| 82 | return { expr::mkIf(continue_i, std::move(val_next), std::move(res_i)), |
| 83 | np_i && continue_i.implies(np_next), |
| 84 | ub && continue_i.implies(ub_next) }; |
| 85 | } |
| 86 | }; |
| 87 | |
| 88 | uint64_t getGlobalVarSize(const IR::Value *V) { |
| 89 | if (auto *V2 = isNoOp(*V)) |