Bit-vector arithmetic questions

[ulysse-lh]

Hello,

I have two questions regarding bit-vector arithmetic, specifically division, modulo and comparisons.

• Is it normal that the modulo operation is not mentioned in UCLID's grammar in tutorial/tutorial.pdf? Since that file is newer than its .tex counterpart, I did not bother recompiling it.

• How can I get unsigned arithmetic when working with bit-vectors? From a few experiment, it seems that UCLID uses the C99 convention:

  If the quotient a/b is representable, the expression (a/b)*b + a%b shall equal a.

  However, bit-vectors seem to be always interpreted as signed.

The following snippet is the skeleton I have been experimenting with:

module main {


    define expr_to_test(): bv3 = ...;
    define expected(): bv3 = ...;
    define bool_expr_to_test(): boolean = ...;


    var inv_dbg: bv3;

    init {
        inv_dbg = expr_to_test();
    }
    next {}


    property test_expr: expr_to_test() == expected();
    property test_bool_expr: bool_expr_to_test();


    control {
        o = induction;
        check;
        print_results;
        o.print_cex;
    }
}

For example, using expr_to_test = 3bv3 % 2bv3 and expected = 1bv3, the property test_expr passes whereas using expr_to_test = 7bv3 % 5bv3 and expected = 2bv3 makes it fail and shows that inv_dbg = 7bv3. Similarly, using expr_to_test = 6bv3 / 7bv3 yields inv_dbg = 2bv3 rather than the expected 0bv3.
The behaviour is even more blatant with comparisons since using bool_expr_to_test = 3bv3 > 0bv3 makes the property test_bool_expr succeed while using bool_expr_to_test = 4bv3 > 0bv3 makes it fail.

Every time, the skeleton was run with uclid <file name>, using uclid 0.9.5.

Is it possible to get unsigned arithmetic with bit-vectors for the aforementioned operators?

[polgreen]

HI,

Ah, yes, good catch that modulo is not in the tutorial. Will add.

Bitvectors are not signed or unsigned in UCLID5, they are simply strings of bits. The relevant bitvector operators (comparison operators and modulo) can be signed or unsigned though (this is the same as how bitvector arithmetic is implemented in SMT-lib).

Signed operators: <, >, <=, >=, %, \
unsigned operators: <_u, >_u, <=_u, >=_u, %_u, \_u

[ulysse-lh]

Thank you very much for your reactivity.

I totally did not know of such unsigned version of operators. Again, thank you!

Have a nice day.