Last active
February 7, 2017 00:06
-
-
Save ttaubert/ecf5b710e849ddfefa81c14a70631eec to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <stdint.h> | |
uint8_t add(uint8_t a, uint8_t b) { | |
uint8_t sum = a + b; | |
return sum < a ? UINT8_MAX : sum; | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
m1 <- llvm_load_module "add.bc"; | |
m2 <- llvm_load_module "cadd.bc"; | |
add <- llvm_extract m1 "add" llvm_pure; | |
cadd <- llvm_extract m2 "add" llvm_pure; | |
let thm = {{ \x y -> add x y == cadd x y }}; | |
prove_print abc thm; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#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 lt(uint8_t a, uint8_t b) { | |
return msb(a ^ ((a ^ b) | ((a - b) ^ b))); | |
} | |
uint8_t add(uint8_t a, uint8_t b) { | |
return (a + b) | lt(a + b, a); | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment