unsoundness avec bitvectors

bv_repr.smt2

Bonjour François et Bruno !

Colibri prouve le fichier en PJ, mais cela me semble incorrect. En effet, si hash et salt sont zéro, o devrait être zéro aussi et le fichier devient sat.

Qu'en pensez vous ?

(define-fun o () Int (bv2nat (bvxor (bvmul #x0000000000000005 salt) (bvmul #x0000000000000007 hash))))

(bvxor 0 0) n'est pas 0 pour moi mais 11111111111...1111, non?

Non je crois bien que (bvxor 0 0) est 0. Voici le même exemple juste avec des bitvectors, afin de pouvoir utiliser cvc4 (il gère très mal la conversion vers Int):

(set-logic ALL)
(set-info :smt-lib-version 2.6)
(declare-const salt (_ BitVec 64))
(declare-const hash (_ BitVec 64))
(define-fun o () (_ BitVec 64) (bvxor (bvmul #x0000000000000005 salt) (bvmul #x0000000000000007 hash)))
(assert
;; defqtvc
 ;; File "usergroup_examples.adb", line 42, characters 0-0
  (not (bvult #x0000000000000000 (bvurem o #x0000000000000100))))
(check-sat)
(get-value (o hash salt))

Cvc4 repond:

$ cvc4 bv.smt2 --produce-models
sat
((o #b0000000000000000000000000000000000000000000000000000000000000000) (hash #b0000000000000000000000000000000000000000000000000000000000000000) (salt #b0000000000000000000000000000000000000000000000000000000000000000))

Oh oui merci. Je ne devrais pas faire des bitvectors en faisant garde d'enfant. MErci pour l'example en bitvector pure également.

Tu m'avais mis le doute, c'est pour ça que j'ai demandé à cvc4 :-)

mentioned in commit 7f517cb8

mentioned in merge request !14 (merged)

The fix will go in !14 (merged) once @marre has some time to look into it. COLIBRI gives the correct result with the bitvector version.

Bonjour à tous, j'ai corrigé et commité le bug (encore un problème de portage des bounded int en unbounded) A priori ça doit être bon !

Merci ! J'attends que François nous donne accès à ce changement.

mentioned in commit 48aee1f7

Avec le dernier merge de François, ce problème semble être corrigé, merci ! Tenez nous au courant svp pour l'issue #27 (closed) ...

Je crois que le problème ici est corrigé.

closed

added unsoundness label