[SMT][Z3] Proving equivalence of two functions using CBMC and Z3 SMT-solver

... while reading the "Beautiful Code" book, the 5th chapter ("... Lessons from Designing XML Verifiers") by Elliotte Rusty Harold, I've found this piece of code (it's like isdigit() for Unicode):

bool isXMLDigit(unsigned int c)
{
        if (c >= 0x0030 && c <= 0x0039) return true; // ASCII
        if (c >= 0x0660 && c <= 0x0669) return true; // arabic
        if (c >= 0x06F0 && c <= 0x06F9) return true; // arabic
        if (c >= 0x0966 && c <= 0x096F) return true; // Devanagari

        if (c >= 0x09E6 && c <= 0x09EF) return true;

        if (c >= 0x0A66 && c <= 0x0A6F) return true; // Gurmukhi?
        if (c >= 0x0AE6 && c <= 0x0AEF) return true;

        if (c >= 0x0B66 && c <= 0x0B6F) return true;
        if (c >= 0x0BE7 && c <= 0x0BEF) return true;
        if (c >= 0x0C66 && c <= 0x0C6F) return true;

        if (c >= 0x0CE6 && c <= 0x0CEF) return true;
        if (c >= 0x0D66 && c <= 0x0D6F) return true;
        if (c >= 0x0E50 && c <= 0x0E59) return true;

        if (c >= 0x0ED0 && c <= 0x0ED9) return true;
        if (c >= 0x0F20 && c <= 0x0F29) return true; // Tibetan?

        return false;
}

... which was then optimized by the author:

bool isXMLDigit_optimized(unsigned int c)
{
        if (c < 0x0030) return false; if (c <= 0x0039) return true;
        if (c < 0x0660) return false; if (c <= 0x0669) return true;
        if (c < 0x06F0) return false; if (c <= 0x06F9) return true;
        if (c < 0x0966) return false; if (c <= 0x096F) return true;

        if (c < 0x09E6) return false; if (c <= 0x09EF) return true;
        if (c < 0x0A66) return false; if (c <= 0x0A6F) return true;
        if (c < 0x0AE6) return false; if (c <= 0x0AEF) return true;

        if (c < 0x0B66) return false; if (c <= 0x0B6F) return true;
        if (c < 0x0BE7) return false; if (c <= 0x0BEF) return true;
        if (c < 0x0C66) return false; if (c <= 0x0C6F) return true;

        if (c < 0x0CE6) return false; if (c <= 0x0CEF) return true;
        if (c < 0x0D66) return false; if (c <= 0x0D6F) return true;
        if (c < 0x0E50) return false; if (c <= 0x0E59) return true;

        if (c < 0x0ED0) return false; if (c <= 0x0ED9) return true;
        if (c < 0x0F20) return false; if (c <= 0x0F29) return true;

        return false;
}

You see, the problem with such hackish solution is that they are prone to bugs. A small unnoticed (for a long period of time) typo can ruin everything.

CBMC

Can we prove these two functions are equivalent to each other? I used KLEE in past for that , but it is not the only kid on a block. Another well-known tool is CBMC . (Stands for "C Bounded Model Checker", I think.) It also uses SMT solver as a backend engine.

I am adding this function:

void check(unsigned int c)
{
        assert (isXMLDigit_optimized(c) == isXMLDigit(c));
};

And asking CBMC to find such an input so that assert() would stop:

$ cbmc --trace --function check isXMLdigit.c

...

** Results:
[check.assertion.1] assertion isXMLDigit_optimized(c) == isXMLDigit(c): SUCCESS

** 0 of 1 failed (1 iteration)
VERIFICATION SUCCESSFUL

Try to alter any line or constant in any function and ...

** Results:
[check.assertion.1] assertion isXMLDigit_optimized(c) == isXMLDigit(c): FAILURE

Trace for check.assertion.1:

State 17 file isXMLdigit_bug.c line 64 thread 0
----------------------------------------------------
  INPUT c: 2534u (00000000 00000000 00001001 11100110)

State 20 file isXMLdigit_bug.c line 64 thread 0
----------------------------------------------------
  c=2534u (00000000 00000000 00001001 11100110)

State 24 file isXMLdigit_bug.c line 66 function check thread 0
----------------------------------------------------
  c=2534u (00000000 00000000 00001001 11100110)

State 42 file isXMLdigit_bug.c line 66 function check thread 0
----------------------------------------------------
  c=2534u (00000000 00000000 00001001 11100110)

Violated property:
  file isXMLdigit_bug.c line 66 function check
  assertion isXMLDigit_optimized(c) == isXMLDigit(c)
  return_value_isXMLDigit_optimized == return_value_isXMLDigit

c=2534 is an input leading to crash.

Z3 SMT-solver

But I also wanted to know if I can convert all this into propositional logic form and check equivalence using SMT solver.

I would add two types of boolean variables. "c"-variables for conditions. "p"-variables are like "points". Each "point" is true if execution flow reaches this point for the corresponding input.

bool isXMLDigit(unsigned int c)
{
/*p1.1*/ if (/*c1*/ c>=0x0030 && c<=0x0039) /*p1.2*/ return true;/*p1.3*/
/*p2.1*/ if (/*c2*/ c>=0x0660 && c<=0x0669) /*p2.2*/ return true;/*p2.3*/

...

/*p15.1*/if (/*c15*/c>=0x0F20 && c<=0x0F29) /*p15.2*/return true;/*p15.3*/
/*p16*/
return false;
}

p1.1 is always true (we get there for any input). p1.2 is true if p1.1 is true AND c1 condition is true. p1.3 is true if p1.1 is true AND p1.2 is false (as if no "return true" has been executed). On the next line, p2.1 is a synonym for p1.3.

The function returns false IFF (if and only if) p16==true. The function returns true IFF (p1.2 OR p2.2 OR ... OR p15.2).

Here is how I model this using SMT-LIB 2.0 LISPy language:

; /*p1.1*/ if (/*c1*/ c>=0x0030 && c<=0x0039) /*p1.2*/ return true;/*p1.3*/

(assert (= f1_p1_1 true)) ; always
(assert (= f1_c1 (and (bvuge f1_c #x0030) (bvule f1_c #x0039))))
(assert (= f1_p1_2 (and f1_p1_1 f1_c1)))
(assert (= f1_p1_3 (and f1_p1_1 (not f1_p1_2))))

; /*p2.1*/ if (/*c2*/ c>=0x0660 && c<=0x0669) /*p2.2*/ return true;/*p2.3*/

(assert (= f1_p2_1 f1_p1_3))
(assert (= f1_c2 (and (bvuge f1_c #x0660) (bvule f1_c #x0669))))
(assert (= f1_p2_2 (and f1_p2_1 f1_c2)))
(assert (= f1_p2_3 (and f1_p2_1 (not f1_p2_2))))

...

; f1() returns false IFF f1_p16
(assert (= f1_returns_false f1_p16))

; f1() return true IFF f1_p1_2 OR f1_p2_2 OR ... OR f1_p15_2
(assert (= f1_returns_true (or f1_p1_2 f1_p2_2 f1_p3_2 f1_p4_2 f1_p5_2 f1_p6_2 f1_p7_2 f1_p8_2 f1_p9_2
f1_p10_2 f1_p11_2 f1_p12_2 f1_p13_2 f1_p14_2 f1_p15_2)))

Yes, Z3Py could be used, but I chose not to "contaminate" it by Python syntax yet, to get a clearer representation of propositional logic equation.

Optimized version of the function is a bit more complex:

bool isXMLDigit_optimized(unsigned int c)
{
/*p1.1*/ if (/*c1.1*/ c<0x0030) /*p1.2*/ return false; /*p1.3*/ if (/*c1.2*/ c<=0x0039) /*p1.4*/ return true;/*p1.5*/
/*p2.1*/ if (/*c2.1*/ c<0x0660) /*p2.2*/ return false; /*p2.3*/ if (/*c2.2*/ c<=0x0669) /*p2.4*/ return true;/*p2.5*/

...

/*p15.1*/if (/*c15.1*/c<0x0F20) /*p15.2*/return false; /*p15.3*/if (/*c15.2*/c<=0x0F29) /*p15.4*/return true;/*p15.5*/
/*p16*/
return false;
}

How I model it in SMT:

; /*p1.1*/ if (/*c1.1*/ c<0x0030) /*p1.2*/ return false; /*p1.3*/ if (/*c1.2*/ c<=0x0039) /*p1.4*/ return true;/*p1.5*/

(assert (= f2_p1_1 true)) ; always
(assert (= f2_c1_1 (bvult f2_c #x0030)))
(assert (= f2_p1_2 (and f2_p1_1 f2_c1_1)))
(assert (= f2_p1_3 (and f2_p1_1 (not f2_p1_2))))
(assert (= f2_c1_2 (bvule f2_c #x0039)))
(assert (= f2_p1_4 (and f2_p1_3 f2_c1_2)))
(assert (= f2_p1_5 (and f2_p1_1 (not f2_p1_4))))

; /*p2.1*/ if (/*c2.1*/ c<0x0660) /*p2.2*/ return false; /*p2.3*/ if (/*c2.2*/ c<=0x0669) /*p2.4*/ return true;/*p2.5*/

(assert (= f2_p2_1 f2_p1_5))
(assert (= f2_c2_1 (bvult f2_c #x0660)))
(assert (= f2_p2_2 (and f2_p2_1 f2_c2_1)))
(assert (= f2_p2_3 (and f2_p2_1 (not f2_p2_2))))
(assert (= f2_c2_2 (bvule f2_c #x0669)))
(assert (= f2_p2_4 (and f2_p2_3 f2_c2_2)))
(assert (= f2_p2_5 (and f2_p2_1 (not f2_p2_4))))

And at the very end, I'm asking for such an input for both function, for which their outputs would differ:

(assert (= f1_c f2_c))
(assert (or
        (not (= f1_returns_false f2_returns_false))
        (not (= f1_returns_true f2_returns_true))))

No, Z3, CVC4 and Boolector can't find such an input, giving "unsat". The problem is small enough to be tackled by my toy-level MK85 bitblaster . Alter any constant, and SMT solver would find such an input.

Perhaps, this is what CBMC doing internally, if I understand all the things correctly.

Thanks

Thanks to Martin Nyx Brain for help with CBMC.

The files

Here

But bruteforce?

You see, you can enumerate all 16-bit inputs effortlessly. Yes, but this is a simple example itself.

More to come...