Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- #include "klee/klee.h"
- #include <assert.h>
- #include <inttypes.h>
- #include <stdio.h>
- //types and constants used in the functions below
- const uint64_t m1 = 0x5555555555555555; //binary: 0101...
- const uint64_t m2 = 0x3333333333333333; //binary: 00110011..
- const uint64_t m4 = 0x0f0f0f0f0f0f0f0f; //binary: 4 zeros, 4 ones ...
- const uint64_t m8 = 0x00ff00ff00ff00ff; //binary: 8 zeros, 8 ones ...
- const uint64_t m16 = 0x0000ffff0000ffff; //binary: 16 zeros, 16 ones ...
- const uint64_t m32 = 0x00000000ffffffff; //binary: 32 zeros, 32 ones
- const uint64_t hff = 0xffffffffffffffff; //binary: all ones
- const uint64_t h01 = 0x0101010101010101; //the sum of 256 to the power of 0,1,2,3...
- //This is a naive implementation, shown for comparison,
- //and to help in understanding the better functions.
- //It uses 24 arithmetic operations (shift, add, and).
- int popcount_1(uint64_t x) {
- x = (x & m1 ) + ((x >> 1) & m1 ); //put count of each 2 bits into those 2 bits
- x = (x & m2 ) + ((x >> 2) & m2 ); //put count of each 4 bits into those 4 bits
- x = (x & m4 ) + ((x >> 4) & m4 ); //put count of each 8 bits into those 8 bits
- x = (x & m8 ) + ((x >> 8) & m8 ); //put count of each 16 bits into those 16 bits
- x = (x & m16) + ((x >> 16) & m16); //put count of each 32 bits into those 32 bits
- x = (x & m32) + ((x >> 32) & m32); //put count of each 64 bits into those 64 bits
- return x;
- }
- //This uses fewer arithmetic operations than any other known
- //implementation on machines with slow multiplication.
- //It uses 17 arithmetic operations.
- int popcount_2(uint64_t x) {
- x -= (x >> 1) & m1; //put count of each 2 bits into those 2 bits
- x = (x & m2) + ((x >> 2) & m2); //put count of each 4 bits into those 4 bits
- x = (x + (x >> 4)) & m4; //put count of each 8 bits into those 8 bits
- x += x >> 8; //put count of each 16 bits into their lowest 8 bits
- x += x >> 16; //put count of each 32 bits into their lowest 8 bits
- x += x >> 32; //put count of each 64 bits into their lowest 8 bits
- return x & 0x7f;
- }
- //This uses fewer arithmetic operations than any other known
- //implementation on machines with fast multiplication.
- //It uses 12 arithmetic operations, one of which is a multiply.
- int popcount_3(uint64_t x) {
- x -= (x >> 1) & m1; //put count of each 2 bits into those 2 bits
- x = (x & m2) + ((x >> 2) & m2); //put count of each 4 bits into those 4 bits
- x = (x + (x >> 4)) & m4; //put count of each 8 bits into those 8 bits
- return (x * h01)>>56; //returns left 8 bits of x + (x<<8) + (x<<16) + (x<<24) + ...
- }
- int main() {
- uint64_t x = 0;
- uint32_t choice = 0;
- klee_make_symbolic(&x, sizeof(uint64_t), "x");
- klee_make_symbolic(&choice, sizeof(uint32_t), "choice");
- klee_assume(choice < 6);
- uint64_t result0 = 0;
- uint64_t result1 = 0;
- // To prove all are equivalent execution is all orders must be tried.
- switch (choice) {
- case 0:
- printf("Trying combination 0\n");
- result0 = popcount_1(x);
- result1 = popcount_2(x);
- break;
- case 1:
- printf("Trying combination 1\n");
- result0 = popcount_1(x);
- result1 = popcount_3(x);
- break;
- case 2:
- printf("Trying combination 2\n");
- result0 = popcount_2(x);
- result1 = popcount_1(x);
- break;
- case 3:
- printf("Trying combination 3\n");
- result0 = popcount_2(x);
- result1 = popcount_3(x);
- break;
- case 4:
- printf("Trying combination 4\n");
- result0 = popcount_3(x);
- result1 = popcount_1(x);
- break;
- case 5:
- printf("Trying combination 5\n");
- result0 = popcount_3(x);
- result1 = popcount_2(x);
- break;
- default:
- assert(0 && "unreachable");
- }
- assert(result0 == result1 && "Not equivalent");
- return 0;
- }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement