SMT count_trailing_zeros bug?

[nwf]

With a fresh build of a4a3ab6 (admittedly, on Debian 13.1 on PowerPC Linux) and cvc5 1.1.2 (specifically, Debian's 1.1.2-2+b3), this program

default Order dec
$include <vector_dec.sail>

$counterexample
function test(T : bits(3)) -> bool = count_trailing_zeros(T) >= 0

run with sail --smt --smt-auto dies a horrible death:

Checking counterexample: test.smt2
test.smt2:2.2: No set-logic command was given before this point.
test.smt2:2.2: cvc5 will make all theories available.
test.smt2:2.2: Consider setting a stricter logic for (likely) better performance.
test.smt2:2.2: To suppress this warning in the future use (set-logic ALL).
Solver found counterexample: ok
  zz53zE0 -> 0b001
Failed to replay counterexample: error
  Function returned true
Error:
./properties/test.sail:5.9-13:
5 |function test(T : bits(3)) -> bool = count_trailing_zeros(T) >= 0
  |         ^--^
  | Property check failure for test.

I suspect that this means there's a bug in the count_trailing_zeros intrinsic implementation in the SMT backend, but I won't pretend to be certain.

FWIW, varying the length of the vector T : bits(N) a bit...

N	result
1	SMT unsat (no claimed counter example)
2	SMT unsat
3	as above
4	SMT unsat
5	as above; claimed counterexample is 0b00100
6	as above; claimed counterexample is 0b000010
7	as above; claimed counterexample is 0b0000001
8	SMT unsat

[rmn30]

Looks like it is only working for power-of-two sized bit vectors. I think maybe it should be padding with ones instead of zeros but I tried that and it didn't fix it.

[rmn30]

I'm also suspicious of the bvsub. I don't think this will work unless the bit vector is all zeros!

[rmn30]

I think the following patch works for the fbits case:

diff --git a/src/lib/smt_gen.ml b/src/lib/smt_gen.ml
index bd5bd543..4b3c5ce3 100644
--- a/src/lib/smt_gen.ml
+++ b/src/lib/smt_gen.ml
@@ -1355,7 +1355,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
     let rec tzcnt ret_sz sz smt =
       if sz == 1 then
         Ite
-          ( Fn ("=", [Extract (0, 0, sz, smt); Bitvec_lit [Sail2_values.B0]]),
+          ( Fn ("=", [smt; Bitvec_lit [Sail2_values.B0]]),
             bvint ret_sz (Big_int.of_int 1),
             bvint ret_sz Big_int.zero
           )
@@ -1383,14 +1383,9 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
     | CT_fbits sz when sz land (sz - 1) = 0 -> return (tzcnt ret_sz sz smt)
     | CT_fbits sz ->
         let padded_sz = smallest_greater_power_of_two sz in
-        let padding = bvzero (padded_sz - sz) in
+        let padding = bvone (padded_sz - sz) in
         assert (padded_sz > sz);
-        return
-          (Fn
-             ( "bvsub",
-               [tzcnt ret_sz padded_sz (Fn ("concat", [padding; smt])); bvint ret_sz (Big_int.of_int (padded_sz - sz))]
-             )
-          )
+        return (tzcnt ret_sz padded_sz (Fn ("concat", [padding; smt])))
     | CT_lbits ->
         if ret_sz > lbits_index then
           return

I've not tried for the lbits case.

[rmn30]

I tried to actually trigger then lbits case so that I can test it but couldn't figure out how @Alasdair ?

[Alasdair]

I think a good way to test that is to write a function that generates the length, like:

val get_length : unit -> int

function get_length() = 16 // could use a register if we really need to stop constant folding

$[property]
function prop() = {
  let bv = zeros(get_length());
  ...
}

Unless the optimisation is smart enough to fold get_length the int return type should hide the fixed length (I might have to add a special blackbox function at some point).

[rmn30]

This came up during testing and I found it a bit surprising:

$ cat test2.sail
$include <arith.sail>

$counterexample
function test(l : range(1,8)) -> bool = l != 9

$ sail -smt -smt_auto test2.sail
Checking counterexample: test.smt2
test.smt2:2.2: No set-logic command was given before this point.
test.smt2:2.2: cvc5 will make all theories available.
test.smt2:2.2: Consider setting a stricter logic for (likely) better performance.
test.smt2:2.2: To suppress this warning in the future use (set-logic ALL).
Solver found counterexample: ok
  zl -> 9
Replaying counterexample: ok
Error:
test2.sail:4.9-13:
4 |function test(l : range(1,8)) -> bool = l != 9
  |         ^--^
  | Property check failure for test.

It looks like sail ignores the range of l when generating the SMT? Is this expected? It's easy enough to work around. A warning might be nice...

[Alasdair]

That happens because the dependent types are removed before generating the SMT query. To work around this there is something to convert the original function types into constraints, and when that goes wrong there is a warning:

5 |$property
  |         ^ checking function argument has type bool('ex282#)
  | Identifier b is unbound. Did you mean x?
  | 
  | Type error when generating guard for a property.
  | When generating guards we convert type quantifiers from the function signature
  | into runtime checks so it must be possible to reconstruct the quantifier from
  | the function arguments. For example:
  | 
  | function f : forall 'n, 'n <= 100. (x: int('n)) -> bool
  | 
  | would cause the runtime check x <= 100 to be added to the function body.
  | To fix this error, ensure that all quantifiers have corresponding function arguments.

Not sure why it isn't working there, it's a bit ad-hoc in general. The property checking will work best when the argument types map cleanly onto fixed-length SMT bitvector types.

[rmn30]

So I now have a fix that works for the lbits case too but I'm a bit confused by the if ret_sz > bits_index. Is the else reachable?

[Alasdair]

Because of the way the SMT generation handles the control flow, you do sometimes need cases for seemly impossible type combinations. In those cases however, the value doesn't matter it just needs to be a dummy value of the correct type.

[rmn30]

So in another twist I found that we actually had an implementation of count_trailing_zeros in our Sail code and that having this was causing sail to generate incorrect SMT. Here's a minimised example:

default Order dec
$include <vector_dec.sail>

// Removings this fixes Sail SMT generation!
function count_trailing_zeros(bv) = {
  foreach(i from 0 to ('N - 1) by 1 in inc) 
    if bv[i] == bitone then {
      return i;
    }
  ;
  'N
}

$counterexample
function prop_setboundsrounddown_aligned(a : bits(32)) -> bool = {
    let b = (0b0 @ a) ;
    let c = count_trailing_zeros(b);
    unsigned(b) <= unsigned(0b1@0x00000000)
}

outputs:

Solver found counterexample: ok
  zz53zE17 -> 0x00000000
Failed to replay counterexample: error
  Function returned true
Error:
./test_cat.sail:15.9-40:
15 |function prop_setboundsrounddown_aligned(a : bits(32)) -> bool = {
   |         ^-----------------------------^
   | Property check failure for prop_setboundsrounddown_aligned.

Note that the count_trailing_zeros does not even affect the final property!

I have no idea what's going on here but getting rid of the unnecessar implementation of count_trailing_zeros and just using the builtin appears to fix the problem for me. Any thoughts @Alasdair ?

[rmn30]

(I should note that this is when run with my patch as in #1573 ).