SMT generation

[kaiboy05]

Hi, I was going to do some testing with the SMT generator feature of sail. However, when I try to generate the SMT after specifying the property, the program did not terminate.

May I know is there any requirement for the functions in the property in order to generate the SMT? Does it need the function does not contain any recursive function? (Since I could not see there is an unwind depth option when generating the SMT), and does it support the mapping?

Thank you very much.

Update: Here is an example of sail file that is not generating the SMT, I think it may be because of the recursive function.

val      countLeadZero : forall 'n, 'n >= 1. bits('n) -> nat
function countLeadZero (a) = {
  if (length(a) == 1) then (if a[0] == bitzero then 1 else 0) else
  match a[length(a) - 1] {
    bitzero => 1 + countLeadZero (a[(length(a) - 2) .. 0]),
    bitone => 0
  }
}

$property
function totestproperty2(xs: bits(32)) -> bool = {
  let result = countLeadZero(xs);

  (result <= 32)
}

[Alasdair]

Yes, the functions cannot be recursive. There is an unroll directive, which looks like:

$optimize unroll 32
val      countLeadZero : forall 'n, 'n >= 1. bits('n) -> nat

There is also special support for counting leading zeros as a builtin, see test/smt/lzcnt.unsat.smt.

[kaiboy05]

Thank you very much.

I just tried the unroll directive like this:

$optimize unroll 2
val      countLeadZero : forall 'n, 'n >= 1. bits('n) -> nat
function countLeadZero (a) = {
  if (length(a) == 1) then (if a[0] == bitzero then 1 else 0) else
  match a[length(a) - 1] {
    bitzero => 1 + countLeadZero (a[(length(a) - 2) .. 0]),
    bitone => 0
  }
}

$property
function totestproperty(xs: bits(128)) -> bool = {
  let result = countLeadZero(xs);

  (result <= 128)
}

But it still could not terminate.

I tried to remove all the recursive bit of my code (not the countLeadZero function above, but a very long function), but when I was trying to generate it again, it shows an error:

Error:
Failure Cannot perform conversion from (%i64, %bv16) to (%i, %bv16)

I could not find out which part of my code gives this error, but I could run the function in the top level. May I know what is the possible cause of this error?

[Alasdair]

That looks like a bug, I'll have a look and see if I can fix it.

Thinking about it more unroll may just not do what you want because it'll unroll the function definition n times but the final case will still be recursive. Our main use case for SMT generation was finding counterexamples for capability encoding and decoding scheme properties in CHERI, which are non-recursive, so it's just not something we had to deal with. I actually added count leading zeros as a builtin because it was used in those schemes and I wanted to avoid having to deal with its recursive definition.

I should note that I have mostly moved away from trying to generate SMT directly from Sail towards a symbolic execution based approach: https://github.com/rems-project/isla