powif64 intrinsic is not currently supported by Kani

[acgetchell]

Requested feature:

Support powif64.

Use case:

https://github.com/acgetchell/cdt-rs/blob/main/src/lib.rs#L161

Test case:

https://github.com/acgetchell/cdt-rs/actions/runs/6180157100/job/16776172095#step:3:4374

[zhassan-aws]

Thanks @acgetchell for the feature request.

@adpaco-aws I see that the support for powif64 was removed in #1081 because it was unaudited. Are you aware of any missing checks for it that need to be instrumented?

[adpaco-aws]

No, I'm not aware of any checks. I believe that testing correctness, and maybe check what's the output for NaN values, would suffice to add it back.

[zhassan-aws]

It seems that CBMC is missing the power functions, e.g.

#include <stdio.h>
#include <math.h>

int main() {
    double a, b, c;

    a = 1.0;
    b = 1.0;
    c = pow(a, b);
    printf("%f\n", c);

    return 0;
}

$ goto-cc pow.c
$ goto-instrument --add-library ./a.out ./b.out
$ cbmc b.out
Starting Bounded Model Checking
**** WARNING: no body for function pow

@tautschnig are these not supported in CBMC?

I tried __builtin_pow, but these didn't work either.

[tautschnig]

Yes, CBMC does not ship library models for these: it’s not obvious how to come up with an implementation that works without doing a series of multiplications. Doing those would likely have prohibitive cost.

[zhassan-aws]

I see. Would it make sense to use an over-approximating model that bails out and returns non-det in some cases (e.g. similar to sqrt)?

@acgetchell as far as I could see, the code only uses powi(2):

https://github.com/acgetchell/cdt-rs/blob/main/src/triangulation.rs#L32
?

If this is the case, a workaround would be to replace the powi with a multiplication operation.

[tautschnig]

Yes, CBMC does not ship library models for these: it’s not obvious how to come up with an implementation that works without doing a series of multiplications. Doing those would likely have prohibitive cost.

It seems there actually are efficient approximations, though we'd have to be careful how we could argue soundness. See https://schraudolph.org/pubs/Schraudolph99.pdf and https://martin.ankerl.com/2007/10/04/optimized-pow-approximation-for-java-and-c-c/.

[tautschnig]

Yes, CBMC does not ship library models for these: it’s not obvious how to come up with an implementation that works without doing a series of multiplications. Doing those would likely have prohibitive cost.

It seems there actually are efficient approximations, though we'd have to be careful how we could argue soundness. See https://schraudolph.org/pubs/Schraudolph99.pdf and https://martin.ankerl.com/2007/10/04/optimized-pow-approximation-for-java-and-c-c/.

diffblue/cbmc#7906 proposes to add these approximations to CBMC.

[zhassan-aws]

Nice, thanks!