Dear SMT users and developers,
There has been renewed requests to introduce within SMT-LIB some overflow predicates for bit vectors, i.e., predicates indicating if the result of an operation on bit vectors is not corresponding to the expected integer, because of the fixed bit width. Impacted operations are: neg, add, sub, mul, div.
According to the initial request, we plan to introduce the following predicates:
bvnego
bvuaddo bvsaddo
bvusubo bvssubo
bvumulo bvsmulo
bvsdivo
with the same arguments as the corresponding operations, returning true if there is an overflow, and false if not. We do not plan to distinguish whether the result is over or below the expected value. We plan this evolution both for the 2.6 and the 3.0 versions of SMT-LIB.
We solicit comments on this by the end of January 2023. If there are no objections by then, we will proceed in adding those functions in the relevant logics and theories.
Thanks for your feedback!
Happy holidays to All,
Cesare, Clark, Pascal
--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/6fb3655e-13cb-9518-0e7e-3e067ffef9d2%40uliege.be.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/AF1CDAA4-40C1-4D8B-8734-3E536D928DB6%40uiowa.edu.
--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/503dc222-9d28-4841-8688-b3586d8520a1n%40googlegroups.com.
Dear All,
thanks for the comments. There has been some progress on this
issue, and there is a proposal for modification of the SMT-LIB BV
theory and logic. The proposed theory and logic are in
attachment, and a diff is given for convenience below.
Let me suggest that we continue the conversation here:
https://github.com/SMT-LIB/SMT-LIB-2/issues/2 . We (Cesare, Clark
and I) try to better organize our workflows for the SMT-LIB, and
this github space will help us keep track of issues and make
progress faster.
Several people have made insightful remarks, notably about the names of the operators. From several points of view, there are certainly possibilities for better names, but names do not matter that much, and in order to proceed, we need to make a decision at some point. We will review the whole discussion while we are refactoring the 3.0 version of the theory (which will anyway require rethinking names). For now (for the 2.6 version of the theory and logic), it seems that some implementers of BV decision procedures are quite attached to the names as suggested before.
Thanks and best,
Pascal
Major changes to FixedSizeBitVectors.smt2:
103a105,107
> o (_ bv0 m), with 0 < m, which takes a non-negative
integer
> n and returns the bitvector b: [0, m) → {0}
>
109a114,119
> o bv2int, which takes a bitvector b: [0, m) → {0, 1}
> with 0 < m, and returns an integer in the range [-
2^(m - 1), 2^(m - 1)),
> and is defined as follows:
>
> bv2int(b) := if b(m-1) = 0 then bv2nat(b) else
bv2nat(b) - 2^m
>
182a193,206
>
> We also define the following predicates
>
> [[(bvnego s)]] := bv2int([[s]]) >= 2^(m - 1)
>
> [[(bvuaddo s t)]] := (bv2nat([[s]]) + bv2nat([[t]])) >=
2^m
>
> [[(bvsaddo s t)]] := (bv2int([[s]]) + bv2int([[t]])) >=
2^(m - 1) or
> (bv2int([[s]]) + bv2int([[t]])) <
-2^(m - 1)
>
> [[(bvumulo s t)]] := (bv2nat([[s]]) * bv2nat([[t]])) >=
2^m
>
> [[(bvsmulo s t)]] := (bv2int([[s]]) * bv2int([[t]])) >=
2^(m - 1) or
> (bv2int([[s]]) * bv2int([[t]])) <
-2^(m - 1)
Major changes to QF_BV.smt2:
77a79,88
> (bvnego (_ BitVec m) Bool)
> - overflow predicate for 2's complement unary minus
> (bvuaddo (_ BitVec m) (_ BitVec m) Bool)
> - overflow predicate for unsigned addition modulo 2^m
> (bvsaddo (_ BitVec m) (_ BitVec m) Bool)
> - overflow predicate for signed addition on m-bit 2's
complement
> (bvumulo (_ BitVec m) (_ BitVec m) Bool)
> - overflow predicate for unsigned multiplication modulo
2^m
> (bvsmulo (_ BitVec m) (_ BitVec m) Bool)
> - overflow predicate for signed multiplication on m-bit
2's complement
104a116,121
> (bvusubo (_ BitVec m) (_ BitVec m) Bool)
> - overflow predicate for unsigned subtraction modulo
2^m
> (bvssubo (_ BitVec m) (_ BitVec m) Bool)
> - overflow predicate for signed 2's complement m-bit
subtraction
> (bvsdivo (_ BitVec m) (_ BitVec m) Bool)
> - overflow predicate for 2's complement signed division
224a242,244
> (bvusubo s t) stands for (bvult s t)
> (bvssubo s t) abbreviates (or (bvsaddo s (bvneg t)) (and
(bvnego t) (bvslt s (_ bv0 m))))
> (bvsdivo s t) abbreviates (and (bvnego s) (= t (bvnot (_
bv0 m))))