Outdated documentation for `--fixedbv` commandline option and where to find more documentation for `__CPROVER_fixedbv`

[hc825b]

CBMC version: 5.10
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc --fixedbv test.c
What behaviour did you expect: N/A
What happened instead: Unknown option: --fixedbv

Hi CBMC-dev,

It seems the command line option --fixedbv is removed at #2148, and the pull request says __CPROVER_fixedbv is the preferred way to reason with fixed-point numbers. However, the documentations linked below are not updated.
http://www.cprover.org/cprover-manual/modeling/floating-point/
https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/modeling-floating-point.md#math-library

Also I would like to know where I can see the models of arithmetic operators on __CPROVER_fixedbv. For example, does CBMC check overflow for arithmetic operators? How are multiplication and division modeled? Does CBMC provide models for trigonometry functions over common fixed-point formats such as __CPROVER_fixedbv[32][16]? If not, how do I provide my own approximated models?

Thanks!

[martin-cs]

It seems the command line option `--fixedbv` is removed at #2148, and the pull request says `__CPROVER_fixedbv` is the preferred way to reason with fixed-point numbers. However, the documentations linked below are not updated. http://www.cprover.org/cprover-manual/modeling/floating-point/ https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/modeling-floating-point.md#math-library

Ooops. That is a bug.

Also I would like to know where I can see the models of arithmetic operators on `__CPROVER_fixedbv`.

They are handled along with the other bit-vector operations rather than there being one place that contains all of them (as with float). For example, multiplication is: https://github.com/diffblue/cbmc/blob/972a993a2d5790c94b079e5c580f5529c8a0f3ab/src/solvers/flattening/boolbv_mult.cpp#L32 Divide is: https://github.com/diffblue/cbmc/blob/972a993a2d5790c94b079e5c580f5529c8a0f3ab/src/solvers/flattening/boolbv_div.cpp#L38

For example, does CBMC check overflow for arithmetic operators?

I have a nasty feeling that analyses/goto_check.* doesn't handle fixed point. It probably should. I suspect that there simply hasn't been anyone who wanted to use it.

How are multiplication and division modeled?

See above!

Does CBMC provide models for trigonometry functions over common fixed-point formats such as `__CPROVER_fixedbv[32][16]`?

Sorry, no. CBMC's support of trigonometry really isn't great at the moment. I'm working on it but ... it is less simple than you might think.

If not, how do I provide my own approximated models?

If you have the library that your platform uses then you could just use that. Or, you can write your own. If you wanted to integrate them into CBMC then you would need to look at the code that is here: https://github.com/diffblue/cbmc/tree/develop/src/ansi-c/library which is how we model library functions. HTH

[hc825b]

Thanks for the help and the references!

I'd like to also share some of my findings to help on the documentation.

Overflow Check

I quickly tried out two ways to see if CBMC 5.10 (installed by apt) and CBMC 5.30.0 (installed using deb file) check overflow for __CPROVER_fixedbv.
First way is to just use command options --signed-overflow-check and --unsigned-overflow-check, and I don't find additional checks for fixedbv.
Second way I tried is to manually add function calls __CPROVER_overflow_* with an assertion to check the return value. These function calls are simply ignored because the type of parameters does not match, and the assertions I added are considered violated due to the nondeterministic return value.

Modulo operator % is not supported for fixedbv

I assume the modulo operator is the same as '%' for int at bit level, so I am surprised this is not supported.
Modulo operator is handy for implementing, for example, normalize an angle to 0 to 2*pi.

Easier way to specify constant fixedbv?

To model and simplify the library I use, I need to specify several bit-masks and constants (e.g., pi, pi/2) that are the closet values in fixedbv[32][16].
But hex literal will be interpreted as int, and floating point literal is considered as double then cast to fixedbv. I think this might put quite some unnecessary burden to the back-end SAT/SMT solver.

[martin-cs]

Thanks for the feedback and sorry the fixed-point support is not more immediately usable. As for constants...a union of an array of characters and a fixed-point number should be low-overhead.