| 40 | }; |
| 41 | |
| 42 | Results verify(llvm::Function &F1, llvm::Function &F2, |
| 43 | llvm::TargetLibraryInfoWrapperPass &TLI, |
| 44 | smt::smt_initializer &smt_init, ostream &out, |
| 45 | bool print_transform, bool always_verify) { |
| 46 | auto fn1 = llvm2alive(F1, TLI.getTLI(F1), true); |
| 47 | if (!fn1) |
| 48 | return Results::Error("Could not translate '" + F1.getName().str() + |
| 49 | "' to Alive IR\n"); |
| 50 | |
| 51 | auto fn2 = llvm2alive(F2, TLI.getTLI(F2), false, fn1->getGlobalVars()); |
| 52 | if (!fn2) |
| 53 | return Results::Error("Could not translate '" + F2.getName().str() + |
| 54 | "' to Alive IR\n"); |
| 55 | |
| 56 | Results r; |
| 57 | r.t.src = std::move(*fn1); |
| 58 | r.t.tgt = std::move(*fn2); |
| 59 | |
| 60 | if (!always_verify) { |
| 61 | stringstream ss1, ss2; |
| 62 | r.t.src.print(ss1); |
| 63 | r.t.tgt.print(ss2); |
| 64 | if (std::move(ss1).str() == std::move(ss2).str()) { |
| 65 | if (print_transform) |
| 66 | r.t.print(out, {}); |
| 67 | r.status = Results::SYNTACTIC_EQ; |
| 68 | return r; |
| 69 | } |
| 70 | } |
| 71 | |
| 72 | smt_init.reset(); |
| 73 | r.t.preprocess(); |
| 74 | TransformVerify verifier(r.t, false); |
| 75 | |
| 76 | if (print_transform) |
| 77 | r.t.print(out, {}); |
| 78 | |
| 79 | { |
| 80 | auto types = verifier.getTypings(); |
| 81 | if (!types) { |
| 82 | r.status = Results::TYPE_CHECKER_FAILED; |
| 83 | return r; |
| 84 | } |
| 85 | assert(types.hasSingleTyping()); |
| 86 | } |
| 87 | |
| 88 | r.errs = verifier.verify(); |
| 89 | if (r.errs) { |
| 90 | r.status = r.errs.isUnsound() ? Results::UNSOUND : Results::FAILED_TO_PROVE; |
| 91 | } else { |
| 92 | r.status = Results::CORRECT; |
| 93 | } |
| 94 | return r; |
| 95 | } |
| 96 | |
| 97 | } // namespace |
| 98 |
no test coverage detected