Sinf/Cosf not being correctly evaluated

[ssoudan]

Might have missed something but so far I think the following is happening:
Rust intrinsics::sinf32() is substituted with C sinf() which itself seems to be substituted inside CBMC.

This code does some __CPROVER_assume() but no actual calculation of the sinus (in https://github.com/diffblue/cbmc/blob/16240afb9a855951533a57a0343b1737dd3f0168/src/ansi-c/library/math.c#L508):

/* FUNCTION: sinf */

float __VERIFIER_nondet_float();

float sinf(float x)
{
  // gross over-approximation
  float ret=__VERIFIER_nondet_float();

  if(__CPROVER_isinff(x) || __CPROVER_isnanf(x))
    __CPROVER_assume(__CPROVER_isnanf(ret));
  else
  {
    __CPROVER_assume(ret<=1);
    __CPROVER_assume(ret>=-1);
    __CPROVER_assume(x!=0 || ret==0);
  }

  return ret;
}

The result from kani perspective is that the following code fails the verification:

use std::f32::consts::FRAC_PI_2;

#[cfg_attr(kani, kani::proof)]
fn main() {
    let a = FRAC_PI_2;
    println!("a={}", a);

    let sin_a = a.sin();
    println!("sin_a={:.}", sin_a);
    assert_eq!(sin_a, 1.);
}

using the following command line invocation:

kani src/sinf.rs    
Checking harness main...
CBMC 5.60.0 (cbmc-5.60.0)
CBMC version 5.60.0 (cbmc-5.60.0) 64-bit arm64 macos
Reading GOTO program from file src/sinf.out.for-main
Generating GOTO Program
Adding CPROVER library (arm64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.00116479s
size of program expression: 76 steps
slicing removed 39 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 3.25e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00020675s
Running propositional reduction
Post-processing
Runtime Post-process: 1.9166e-05s
Solving with MiniSAT 2.2.1 with simplifier
97 variables, 455 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000529333s
Runtime decision procedure: 0.000793542s

RESULTS:
Check 1: main.assertion.1
         - Status: FAILURE
         - Description: "assertion failed: sin_a == 1."
         - Location: src/sinf.rs:10:5 in function main


SUMMARY: 
 ** 1 of 1 failed
Failed Checks: assertion failed: sin_a == 1.
 File: "/goo/src/sinf.rs", line 10, in main

VERIFICATION:- FAILED

while:

cargo run --bin sinf
   Compiling foo v0.1.0 (/goo)
    Finished dev [unoptimized + debuginfo] target(s) in 0.67s
     Running `target/debug/sinf`
a=1.5707964
sin_a=1

Not sure what is a good solution here but this is misleading as is.

[adpaco-aws]

Hi @ssoudan , thank you for opening the issue!

You're right: The CBMC model for the sine function is an over-approximation that returns 0 if the argument is 0, and a nondeterministic value between -1 and 1 otherwise. I agree that this is misleading and have opened diffblue/cbmc#6999 in order to get more precise models for these intrinsics.

[ssoudan]

Thanks!

[tedinski]

Do you have a specific goal here? Or just trying things out? Just curious.

It's really hard to accurately model many numerical functions. It might be feasible to get it right when it's given a constant (non-symbolic) value, but getting more accurate than that might be a non-goal for Kani.

[ssoudan]

Hi Ted,

it's a bit of both. I’m exploring to figure out how practical it is to use kani in addition to testing for service-like programs - not that likely to deal with floats, and ended up trying it on a pet drone flight controller project to verify the control logic is not going to burst into NaN/Inf.

Understand the verification (even the definition) of FP operations can be challenging and would come at a cost that might be prohibitive. If this is a non-goal for Kani, I suggest updating the table in https://model-checking.github.io/kani/rust-feature-support/intrinsics.html with additional disclaimers for these operations.

Just throwing ideas: best case would be to be able to specify what ‘theory’ to use for a verification and/or be able to refine it (not sure if an SMT-LIB 2 lib can readily be found and used, musl as a pure c version of sin() and libm as a pure rust implementation of it) but that might be too far fetched.

In any case, thanks for the work being done here!

[tedinski]

1. We should revisit the limitations section for sure, even if to make sure it's accurate to our current capabilities...
2. This is a good point about "what theory." We'd been thinking about a stubbing mechanism for Kani (replacing a function like read with an abstraction specific to the proof you're doing) but hadn't considered intrinsics. Stubbing instrinsics would be good too. Then you might be able to use something that at least characterizes Inf/Nan behavior...