Fix bvsdiv and fp.to_ubv fp.to_sbv (#168)

* Fix bvsdiv divided by zero

* [fp.to_ubv] fix parameters order

* [Model] add tests for bitv.sdiv

src/model/bitv.ml

@@ -37,7 +37,10 @@ let is_unsigned_integer size z =
 let ubitv n t =
   let t = Value.extract_exn ~ops t in
   (* the typing of expressions should guarantee that this never happens *)
-  if not (is_unsigned_integer n t) then invalid_arg "not unsigned integer";
+  if not (is_unsigned_integer n t) then
+    (invalid_arg
+      (Format.asprintf "%a is not an unsigned integer of size %i"
+         Z.pp_print t n));
   t
 
 let from_bitv n t =
@@ -154,8 +157,10 @@ let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
   | B.Bitv_sdiv n ->
     op2 ~cst ~size:n (fun a b ->
         let b = sbitv n b in
-        if Z.equal b Z.zero then extract n Z.one
-        else extract n (Z.div (sbitv n a) b))
+        let a = sbitv n a in
+        if Z.equal b Z.zero then
+          if Z.sign a >= 0 then extract n Z.minus_one else extract n Z.one
+        else extract n (Z.div a b))
   | B.Bitv_srem n ->
     op2 ~cst ~size:n (fun a b ->
         let b = sbitv n b in

src/standard/expr.ml

@@ -2576,11 +2576,11 @@ module Term = struct
           )
       let to_ubv =
         with_cache ~cache:(Hashtbl.create 13) (fun (e,s,bv) ->
-            mk' ~builtin:(Builtin.To_ubv (bv,e,s)) "fp.to_ubv" [] [Ty.roundingMode;Ty.float e s] (Ty.bitv bv)
+            mk' ~builtin:(Builtin.To_ubv (e,s,bv)) "fp.to_ubv" [] [Ty.roundingMode;Ty.float e s] (Ty.bitv bv)
           )
       let to_sbv =
         with_cache ~cache:(Hashtbl.create 13) (fun (e,s,bv) ->
-            mk' ~builtin:(Builtin.To_sbv (bv,e,s)) "fp.to_sbv" [] [Ty.roundingMode;Ty.float e s] (Ty.bitv bv)
+            mk' ~builtin:(Builtin.To_sbv (e,s,bv)) "fp.to_sbv" [] [Ty.roundingMode;Ty.float e s] (Ty.bitv bv)
           )
 
     end

tests/model/bitv/division_by_zero.smt2

@@ -14,6 +14,9 @@
 (assert (= #b1 (bvudiv #b0 #b0)))
 (assert (= #b1 (bvudiv #b1 #b0)))
 (assert (= #b11 (bvudiv #b11 #b00)))
+(assert (= #b11 (bvudiv #b00 #b00)))
+(assert (= #b11 (bvudiv #b01 #b00)))
+(assert (= #b11 (bvudiv #b00 #b00)))
 
 (declare-fun a () (_ BitVec 2))
 (assert (= #b11 (bvudiv #b00 a)))
@@ -22,12 +25,18 @@
 ;;;;; remainder by zero evaluates to the first operand.
 (assert (= #b0 (bvurem #b0 #b0)))
 (assert (= #b1 (bvurem #b1 #b0)))
-(assert (= #b11 (bvudiv #b11 #b00)))
+(assert (= #b11 (bvurem #b11 #b00)))
+(assert (= #b00 (bvurem #b00 #b00)))
+(assert (= #b01 (bvurem #b01 #b00)))
+(assert (= #b00 (bvurem #b00 #b00)))
 
-;;;;; bvsdiv by zero evaluates to first operand if it's positive, otherwise 1.
+;;;;; bvsdiv by zero evaluates to -1 if it's positive, otherwise 1.
 (assert (= #b1 (bvsdiv #b0 #b0)))
 (assert (= #b1 (bvsdiv #b1 #b0)))
 (assert (= #b01 (bvsdiv #b11 #b00)))
+(assert (= #b01 (bvsdiv #b10 #b00)))
+(assert (= #b11 (bvsdiv #b01 #b00)))
+(assert (= #b11 (bvsdiv #b00 #b00)))
 
 ;;;;; bvsrem by zero evaluates to the first operand.
 (assert (= #b0 (bvsrem #b0 #b0)))