Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add support for ground bv2nat and int2bv reasoning #733

Merged
merged 3 commits into from
Jul 19, 2023
Merged

Add support for ground bv2nat and int2bv reasoning #733

merged 3 commits into from
Jul 19, 2023

Commits on Jul 12, 2023

  1. Add support for ground bv2nat and int2bv reasoning 

    This patch adds support for "combined" reasoning about the int2bv and
bv2nat symbols in the arith and bitv reasoners.

More specifically:

 - The constructors for bv2nat and int2bv in `expr.ml` are now "smart"
   and know that they are related, so that we effectivly have the
   following rewrite rules:

    `(bv2nat ((_ int2bv n) x))` -> `(mod x (pow 2 n))`
    `((_ int2bv n) (bv2nat (as x (_ BitVec m))))`
      -> `(ite (> m n) (extract (- n 1) 0 x) (zero_extend (- m n) x))`

   These are added early in the bv2nat and int2bv constructors to ensure
   that we *never* actually build `((_ int2bv n) (bv2nat e))` or
   `(bv2nat ((_ int2bv n) e))` terms. This is actualy useful because the
   simplifications done for `bv2nat` (see below) are more powerful than
   what `int2bv` can recover, and there would be information loss
   otherwise e.g. for `((_ int2bv n) (bv2nat (concat e1 e2)))` which
   would become

     `((_ int2bv n) (+ (* (bv2nat e1) (pow 2 m)) (bv2nat e2)))`

   instead of

      `(concat e1 e2)`

   (assuming that `e2` is of type `(_ BitVec m)` and `e1` of type
   `(_ BitVec |n - m|)`).

 - The arith and bitv reasoners perform constant propagation of int2bv
   and bv2nat

 - The arith reasoner performs the `((_ int2bv n) (bv2nat x))`
   conversion more aggressivey, i.e. it performs the conversion for
   terms of the form `((_ int2bv n) e)` where the semantic value of `e`
   is of the form `(bv2nat e')`

   More complex transformations, such as transforming
   `(int2bv (* 2 (bv2nat e)))` into `(concat e #b0)`, are not
   supported.

 - The bitv reasoner also performs the `(bv2nat ((_ int2bv n) e))`
   conversion more aggressively, i.e. for terms that reduce to
   `((_ int2bv n) e)` after simplification.

 - The bitv reasoner performs additional simplifications on `bv2nat`
   terms after normalization. For instance, `(bv2nat (concat x y))`
   becomes `(+ (* (pow 2 n) (bv2nat x)) (bv2nat y))` when `y` is a
   bit-vector of size `n`, and `(bv2nat (extract j i x))` becomes
   `(mod (div (bv2nat x) (pow 2 i)) (pow 2 (+ (- j i) 1)))`

 - Finally, the bitv reasoner requires that the result of `bv2nat` for a
   bitvector of size `n` is in the range `0 ..< 2^n`

Combined, this allows exploiting the arith reasoner for a variety of
problems mostly involving bitvector arithmetic with constants. In
particular, we are able to handle many aritmetic expressions involving
`bv2nat`.

On the other hand, bitvector expressions involving `int2bv` have more
limited support. Indeed, not only does `int2bv` perform less
simplifications, we are currently not able to exploit the relevant
equivalence:

  `int2bv[n](x) = int2bv[n](y) iff x = y  (mod 2^n)`
    @bclement-ocp
    bclement-ocp committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    b89c481 View commit details
    Browse the repository at this point in the history

  2. Use Z.(~$1 lsl n) rather than Z.(pow ~$2 n)

    @bclement-ocp
    bclement-ocp committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    df14d0f View commit details
    Browse the repository at this point in the history

  3. Fix infinite loop: bv2nat has type int

    @bclement-ocp
    bclement-ocp committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    be3da73 View commit details
    Browse the repository at this point in the history