| // This Source Code Form is subject to the terms of the Mozilla Public |
| // License, v. 2.0. If a copy of the MPL was not distributed with this |
| // file, You can obtain one at http://mozilla.org/MPL/2.0/. |
| |
| import "bmul.cry"; |
| |
| print "Loading LLVM bitcode..."; |
| m <- llvm_load_module "../../../dist/Debug/lib/libfreeblpriv3.so.bc"; |
| |
| let SpecBinaryMul n = do { |
| x <- llvm_var "x" (llvm_int n); |
| y <- llvm_var "y" (llvm_int n); |
| llvm_ptr "r_high" (llvm_int n); |
| r_high <- llvm_var "*r_high" (llvm_int n); |
| llvm_ptr "r_low" (llvm_int n); |
| r_low <- llvm_var "*r_low" (llvm_int n); |
| |
| let res = {{ bmul x y }}; |
| llvm_ensure_eq "*r_high" {{ res.0 }}; |
| llvm_ensure_eq "*r_low" {{ res.1 }}; |
| |
| llvm_verify_tactic abc; |
| }; |
| |
| print "Proving equality for 32-bit bmul()..."; |
| time (llvm_verify m "bmul32" [] (SpecBinaryMul 32)); |