Skip to content

Instantly share code, notes, and snippets.

@ttaubert
Created February 7, 2017 00:09
Show Gist options
  • Save ttaubert/c742ba7adf040e14ff21e111a929f5b8 to your computer and use it in GitHub Desktop.
Save ttaubert/c742ba7adf040e14ff21e111a929f5b8 to your computer and use it in GitHub Desktop.
#include <stdint.h>
// 0xff if MSB(x) = 1 else 0x00
uint8_t msb(uint8_t x) {
return 0 - (x >> (8 * sizeof(x) - 1));
}
// 0xff if a >= b else 0x00
uint8_t nz(uint8_t x) {
return ~msb(~x & (x - 1));
}
// 0xff if x > 0 else 0x00
uint8_t ge(uint8_t a, uint8_t b) {
return ~msb(a ^ ((a ^ b) | ((a - b) ^ b)));
}
uint8_t add(uint8_t a, uint8_t b, uint8_t *carry) {
*carry = msb(ge(a, 0 - b) & nz(b)) & 1;
return a + b;
}
void mul(uint8_t a, uint8_t b, uint8_t *hi, uint8_t *lo) {
uint8_t a1 = a >> 4, a0 = a & 0xf;
uint8_t b1 = b >> 4, b0 = b & 0xf;
uint8_t z0 = a0 * b0;
uint8_t z2 = a1 * b1;
uint8_t z1, z1carry, carry, trash;
z1 = add(a0 * b1, a1 * b0, &z1carry);
*lo = add(z1 << 4, z0, &carry);
*hi = add(z2, (z1 >> 4) + carry, &trash);
*hi = add(*hi, z1carry << 4, &trash);
}
m <- llvm_load_module "cmul.bc";
let {{
mul : [8] -> [8] -> ([8], [8])
mul a b = (take`{8} prod, drop`{8} prod)
where prod = (pad a) * (pad b)
pad x = zero # x
}};
llvm_verify m "mul" [] do {
a <- llvm_var "a" (llvm_int 8);
b <- llvm_var "b" (llvm_int 8);
llvm_ptr "hi" (llvm_int 8);
hi <- llvm_var "*hi" (llvm_int 8);
llvm_ptr "lo" (llvm_int 8);
lo <- llvm_var "*lo" (llvm_int 8);
let res = {{ mul a b }};
llvm_ensure_eq "*hi" {{ res.0 }};
llvm_ensure_eq "*lo" {{ res.1 }};
llvm_verify_tactic abc;
};
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment