fixed bug #59

uuverifiers · Jul 31, 2024 · e7dd48d · e7dd48d
1 parent 1f0a06e
commit e7dd48d
Show file tree

Hide file tree

Showing 6 changed files with 80 additions and 10 deletions.
diff --git a/regression-tests/horn-bv/Answers b/regression-tests/horn-bv/Answers
@@ -179,5 +179,13 @@ unsat
 
 0: FALSE
 
+sign-extend.smt2
+Warning: ignoring get-model
+sat
+
+bv2intnat.smt2
+Warning: ignoring get-model
+sat
+
 int2bv.smt2
 unsat
diff --git a/regression-tests/horn-bv/bv2intnat.smt2 b/regression-tests/horn-bv/bv2intnat.smt2
@@ -0,0 +1,24 @@
+(set-logic HORN)
+(declare-fun foo ((_ BitVec 1)) Bool)
+(declare-fun bar (Int Int) Bool)
+(assert (foo (_ bv1 1)))
+
+; bv2int: cast from signed bit-vectors to ints
+; bv2nat: cast from unsigned bit-vectors to ints
+(assert
+  (forall
+    ((x (_ BitVec 1)))
+    (=> (foo x) (bar (bv2int x) (bv2nat x)))))
+
+; int2bv and nat2bv have the same semantics
+(assert
+  (forall
+    ((x Int) (y Int))
+    (=> (bar x y) (= ((_ int2bv 1) x) (_ bv1 1))
+                  (= ((_ nat2bv 1) y) (_ bv1 1)))))
+(assert
+  (forall
+    ((x Int) (y Int))
+    (=> (bar x y) (distinct x y))))
+(check-sat)
+(get-model)
diff --git a/regression-tests/horn-bv/runtests b/regression-tests/horn-bv/runtests
@@ -31,7 +31,9 @@ TESTS="inconclusive.smt2 \
        nonlinear.smt2 \
        quantifier.smt2 \
        substring.error.nts.smt2 \
-       conjunctElimBug.smt2"
+       conjunctElimBug.smt2 \
+       sign-extend.smt2 \
+       bv2intnat.smt2"
 
 #       test0.correct.pierre_bv8.smt2 \
 #       test0.correct.pierre_bv32.smt2 \

diff --git a/regression-tests/horn-bv/sign-extend.smt2 b/regression-tests/horn-bv/sign-extend.smt2
@@ -0,0 +1,17 @@
+; Problem that is sat; due to incorrect handling of sign_extend,
+; Eldarica reported unsat in earlier versions.
+
+(set-logic HORN)
+(declare-fun foo ((_ BitVec 1)) Bool)
+(declare-fun bar ((_ BitVec 2)) Bool)
+(assert (foo (_ bv1 1)))
+(assert
+  (forall
+    ((x (_ BitVec 1)))
+    (=> (foo x) (bar ((_ sign_extend 1) x)))))
+(assert
+  (forall
+    ((x (_ BitVec 2)))
+    (=> (bar x) (= x (_ bv3 2)))))
+(check-sat)
+(get-model)
diff --git a/src/main/scala/lazabs/ast/ASTree.scala b/src/main/scala/lazabs/ast/ASTree.scala
@@ -144,8 +144,8 @@ object ASTree {
   case class BVsle(bits : Int)   extends BinaryOperator("bvsle")
   case class BVcomp(bits : Int)  extends BinaryOperator("bvcomp")
 
-  case class BV2Int()            extends UnaryOperator ("bv2int")
-  case class BV2Nat()            extends UnaryOperator ("bv2nat")
+  case class BV2Int(bits : Int)  extends UnaryOperator ("bv2int")
+  case class BV2Nat(bits : Int)  extends UnaryOperator ("bv2nat")
 
   case class Int2BV(bits : Int)  extends UnaryOperator ("int2bv")
 

diff --git a/src/main/scala/lazabs/prover/PrincessWrapper.scala b/src/main/scala/lazabs/prover/PrincessWrapper.scala
@@ -290,10 +290,10 @@ class PrincessWrapper {
       case BinaryExpression(left, BVBinPred(pred, bits), right) =>
         pred(bits, f2pterm(left), f2pterm(right))
 
-      case UnaryExpression(BV2Int(), arg) =>
-        ModuloArithmetic.cast2Int(f2pterm(arg))
-      case UnaryExpression(BV2Nat(), arg) =>
-        ModuloArithmetic.cast2Int(f2pterm(arg))
+      case UnaryExpression(BV2Int(bits), arg) =>
+        ModuloArithmetic.cast2SignedBV(bits, f2pterm(arg))
+      case UnaryExpression(BV2Nat(bits), arg) =>
+        ModuloArithmetic.cast2UnsignedBV(bits, f2pterm(arg))
       case UnaryExpression(Int2BV(bits), arg) =>
         ModuloArithmetic.cast2UnsignedBV(bits, f2pterm(arg))
 
@@ -482,7 +482,7 @@ class PrincessWrapper {
         val ModuloArithmetic.SignedBVSort(bits2) =
           ModuloArithmetic.ModSort(lower2, upper2)
         UnaryExpression(Int2BV(bits1),
-          UnaryExpression(BV2Int(),
+          UnaryExpression(BV2Int(bits2),
                           rvT(arg)).stype(IntegerType())).stype(BVType(bits1))
       }
 
@@ -496,15 +496,34 @@ class PrincessWrapper {
             UnaryExpression(Int2BV(bits), argExpr).stype(BVType(bits))
           case BVType(bits2) =>
             UnaryExpression(Int2BV(bits),
-              UnaryExpression(BV2Nat(),
+              UnaryExpression(BV2Nat(bits2),
                               argExpr).stype(IntegerType())).stype(BVType(bits))
           case t =>
             throw new Exception("Unhandled type: " + t)
         }
       }
 
+      case IFunApp(ModuloArithmetic.mod_cast,
+                   Seq(IIntLit(lower), IIntLit(upper), arg)) => {
+        val ModuloArithmetic.SignedBVSort(bits) =
+          ModuloArithmetic.ModSort(lower, upper)
+        val argExpr = rvT(arg)
+        argExpr.stype match {
+          case BVType(_) =>
+            UnaryExpression(BV2Int(bits), argExpr).stype(IntegerType())
+          case t =>
+            throw new Exception("Unhandled type: " + t)
+        }
+      }
+
       case IFunApp(ModuloArithmetic.int_cast, Seq(arg)) => {
-        UnaryExpression(BV2Int(), rvT(arg)).stype(IntegerType())
+        val sub = rvT(arg)
+        sub.stype match {
+          case BVType(bits) =>
+            UnaryExpression(BV2Int(bits), sub).stype(IntegerType())
+          case t =>
+            throw new Exception("Unhandled type: " + t)
+        }
       }
 
       case IFunApp(fun, Seq(IIntLit(IdealInt(bits)), left, right))