\myheading{CBMC}

\leveldown{}

So far, CBMC can prove this easily:

\begin{lstlisting}[style=customc]
// time cbmc --trace --function check 1.c

int popcount64a(uint64_t x)
{
	x = (x & m1 ) + ((x >>  1) & m1 );
	x = (x & m2 ) + ((x >>  2) & m2 );
	x = (x & m4 ) + ((x >>  4) & m4 );
	x = (x & m8 ) + ((x >>  8) & m8 );
	x = (x & m16) + ((x >> 16) & m16);
	x = (x & m32) + ((x >> 32) & m32);
	return x;
}

int popcount64b(uint64_t x)
{
	x -= (x >> 1) & m1;             
	x = (x & m2) + ((x >> 2) & m2); 
	x = (x + (x >> 4)) & m4;        
	x += x >>  8;
	x += x >> 16;
	x += x >> 32;
	return x & 0x7f;
}

int popcount64c(uint64_t x)
{
	x -= (x >> 1) & m1;             
	x = (x & m2) + ((x >> 2) & m2); 
	x = (x + (x >> 4)) & m4;        
	return (x * h01) >> 56;
}

int popcount64_naive(uint64_t x)
{
	uint64_t rt=0, i;
	for (i=0; i<64; i++)
		rt=rt+((x>>i)&1);
	return rt;
}

void check(uint64_t c)
{
	assert (popcount64a(c)==popcount64b(c));
	// etc
};
\end{lstlisting}

These functions maybe quite naive, but I've been interested how CBMC handles arrays:

\begin{lstlisting}[style=customc]
int popcount64_table(uint64_t x)
{
	uint64_t tbl[16]={0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4};

	uint64_t rt=0;

	rt=rt+tbl[(x>>(0*4))&0xf];
	rt=rt+tbl[(x>>(1*4))&0xf];
	...
	rt=rt+tbl[(x>>(14*4))&0xf];
	rt=rt+tbl[(x>>(15*4))&0xf];
	
	return rt;
}

int popcount64_table2(uint64_t x)
{
	uint64_t tbl[256]={
0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5,
1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
...
2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7,
3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5, 5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8};

	uint64_t rt=0;

	rt=rt+tbl[(x>>(0*8))&0xff];
	rt=rt+tbl[(x>>(1*8))&0xff];
	...
	rt=rt+tbl[(x>>(6*8))&0xff];
	rt=rt+tbl[(x>>(7*8))&0xff];
	
	return rt;
}
\end{lstlisting}

Things gets a bit harder with a function copypasted from a well-known HAKMEM.
It takes ~160 seconds to get job done, despite the somewhat hard (for SAT/SMT solvers) division/remainder function
with the odd divisor (63):

\begin{lstlisting}[style=customc]
int hakmem169_32(uint32_t x)
{
   x = x  - ((x >> 1)  & 033333333333)
          - ((x >> 2)  & 011111111111);
   x = (x +  (x >> 3)) & 030707070707 ;
   return x % 63; /* casting out 63 */
} 

int hakmem169_64(uint64_t x)
{
	return hakmem169_32(x>>32) + hakmem169_32(x&0xffffffff);
};
\end{lstlisting}

Things gets harder on another arcane function attributed to B.Kernighan:

\begin{lstlisting}[style=customc]
int popcount64d(uint64_t x)
{
	int count;
	for (count=0; x; count++)
		x &= x - 1; // x = x & (x-1)
	return count;
}
\end{lstlisting}

CBMC stuck in seemingly infinite "unwinding loop":

\begin{lstlisting}
CBMC version 5.10 (cbmc-5.10) 64-bit x86_64 linux
Parsing 1.c
Converting
Type-checking 1
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Unwinding loop popcount64d.0 iteration 1 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 2 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 3 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 4 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 5 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 6 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 7 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 8 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 9 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 10 file 1.c line 50 function popcount64d thread 0

...

Unwinding loop popcount64d.0 iteration 1584 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 1585 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 1586 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 1587 file 1.c line 50 function popcount64d thread 0
Unwinding loop popcount64d.0 iteration 1588 file 1.c line 50 function popcount64d thread 0

...

etc
\end{lstlisting}

I couldn't wait it for finish, so I've interrupted.

So I tried to help CBMC by manually limiting the upper bound of the loop:

\begin{lstlisting}[style=customc]
int popcount64d_my(uint64_t x)
{
	int count;
	for (count=0; count<64 && x; count++)
		x &= x - 1;
	return count;
}
\end{lstlisting}

\begin{lstlisting}
CBMC version 5.10 (cbmc-5.10) 64-bit x86_64 linux
Parsing 1.c
Converting
Type-checking 1
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Unwinding loop popcount64d_my.0 iteration 1 file 1.c line 58 function popcount64d_my thread 0
Unwinding loop popcount64d_my.0 iteration 2 file 1.c line 58 function popcount64d_my thread 0

...

Unwinding loop popcount64d_my.0 iteration 63 file 1.c line 58 function popcount64d_my thread 0
Unwinding loop popcount64d_my.0 iteration 64 file 1.c line 58 function popcount64d_my thread 0
size of program expression: 517 steps
simple slicing removed 2 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
17496 variables, 66127 clauses
\end{lstlisting}

And it takes ~42 minutes on my venerable notebook to verify this function.

I also tried to unroll the loop manually:

\begin{lstlisting}[style=customc]
int popcount64d_unrolled(uint64_t x)
{
	int count=0;
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	
	...

	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};

	// be sure x==0 upon the function exit...
	assert(x==0);
	return count;
}
\end{lstlisting}

Now it takes only 16 minutes.
Please note the assert() upon the function exit.
Yes, "x" must be "zeroed" upon the exit for obvious reasons.
However, CBMC would prove that the assert() will never throw.

What if I comment one "if (x)..." line with 4 if's?

\begin{lstlisting}
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 73.0928s

** Results:
[popcount64d_unrolled.assertion.1] assertion x==0: FAILURE
[check.assertion.1] assertion popcount64d_unrolled(c)==popcount64a(c): FAILURE

Trace for popcount64d_unrolled.assertion.1:

State 24 file 1.c line 164 thread 0
----------------------------------------------------
  INPUT c: 18446743244780863487ul (11111111 11111111 11111111 00111110 11111111 11111111 11111111 11111111)

State 27 file 1.c line 164 thread 0
----------------------------------------------------
  c=18446743244780863487ul (11111111 11111111 11111111 00111110 11111111 11111111 11111111 11111111)

State 31 file 1.c line 166 function check thread 0
----------------------------------------------------
  x=18446743244780863487ul (11111111 11111111 11111111 00111110 11111111 11111111 11111111 11111111)

...

\end{lstlisting}

You see -- the "x" variable is almost "filled" with 1's.
Yes, our modified function (with 4 of if's removed) will run incorrectly when "x" has 0-3 zero bits.

Also, SAT solver gave "SATISFIABLE", meaning, it found a counterexample.
Otherwise, it would say "UNSATISFIABLE".

\myheading{Exporting to SMT-LIB 2.x format}

... is possible.

As stated in CBMC's manual:

\begin{framed}
\begin{quotation}
CBMC for SMT-LIB Version 2

We also provide a version of CBMC with prototypical support for generating formulas in the SMT-LIB version 2 format. Use the command line options

--smt2 --outfile dest

to write the verification conditions in SMT-LIB version 2 format into the file dest. The CBMC manual is here.
\end{quotation}
\end{framed}
( \url{https://www.cprover.org/SMT-LIB-LSM/} )

\begin{lstlisting}
cbmc --smt2 --outfile dest.smt --trace --function check 1.c
\end{lstlisting}

You can get an idea what CBMC passes to a SMT solver in each case:

\lstinputlisting[style=customsmt]{\CURPATH/files/dest.smt}

\levelup{}