Fix incompletness with conversions to and from strings (#763)

* fix incompletness with string conversion * improve posts
viperproject · Apr 22, 2024 · 07a1cc0 · 07a1cc0
1 parent 74d12a3
commit 07a1cc0
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 7 deletions.
diff --git a/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala
@@ -86,20 +86,22 @@ class StringEncoding extends LeafTypeEncoding {
 
 
   /**
-    * Encodes the (effectul) conversion from a string to a []byte
+    * Encodes the (effectful) conversion from a string to a []byte
     * [ target = []byte(str) ] ->
     *   [
     *     var s []byte
     *     inhale forall i Int :: { &s[i] } 0 <= i && i < len(s) ==> acc(&s[i])
+    *     inhale len(s) == len(str) // (*)
     *     target = s
     *   ]
+    * Note that (*) is correct because the len() function returns the number of bytes in a string.
     */
   override def statement(ctx: Context): in.Stmt ==> CodeWriter[vpr.Stmt] = {
 
     def goA(x: in.Assertion): CodeWriter[vpr.Exp] = ctx.assertion(x)
 
     default(super.statement(ctx)) {
-      case conv@in.EffectfulConversion(target, in.SliceT(in.IntT(_, TypeBounds.Byte), _), _) =>
+      case conv@in.EffectfulConversion(target, in.SliceT(in.IntT(_, TypeBounds.Byte), _), e) =>
         // the argument of type string is not used in the viper encoding. May change in the future to be able to prove more
         // interesting properties
         val (pos, info, errT) = conv.vprMeta
@@ -108,20 +110,28 @@ class StringEncoding extends LeafTypeEncoding {
         val slice = in.LocalVar(ctx.freshNames.next(), sliceT)(conv.info)
         val vprSlice = ctx.variable(slice)
         val qtfVar = in.BoundVar("i", in.IntT(Addressability.boundVariable))(conv.info)
-        val post = in.SepForall(
+        val post1 = in.SepForall(
           vars = Vector(qtfVar),
           triggers = Vector(in.Trigger(Vector(in.Ref(in.IndexedExp(slice, qtfVar, sliceT)(conv.info))(conv.info)))(conv.info)),
           body = in.Implication(
             in.And(in.AtMostCmp(in.IntLit(BigInt(0))(conv.info), qtfVar)(conv.info), in.LessCmp(qtfVar, in.Length(slice)(conv.info))(conv.info))(conv.info),
             in.Access(in.Accessible.Address(in.IndexedExp(slice, qtfVar, sliceT)(conv.info)), in.FullPerm(conv.info))(conv.info)
           )(conv.info)
         )(conv.info)
+        val post2 = in.ExprAssertion(
+          in.EqCmp(
+            in.Length(slice)(conv.info),
+            in.Length(e)(conv.info),
+          )(conv.info)
+        )(conv.info)
 
         seqn(
           for {
             _ <- local(vprSlice)
-            vprPost <- goA(post)
-            _ <- write(vpr.Inhale(vprPost)(pos, info, errT))
+            vprPost1 <- goA(post1)
+            _ <- write(vpr.Inhale(vprPost1)(pos, info, errT))
+            vprPost2 <- goA(post2)
+            _ <- write(vpr.Inhale(vprPost2)(pos, info, errT))
             ass <- ctx.assignment(in.Assignee.Var(target), slice)(conv)
           } yield ass
         )
@@ -274,8 +284,10 @@ class StringEncoding extends LeafTypeEncoding {
 
   /** Generates the function
     *   requires forall i int :: { &s[i] } 0 <= i && i < len(s) ==> acc(&s[i], _)
+    *   ensures  len(s) == len(res) // (*)
     *   decreases _
-    *   pure func byteSliceToStrFunc(s []byte) string
+    *   pure func byteSliceToStrFunc(s []byte) (res string)
+    * Note that (*) is correct because the function len() returns the number of bytes in a string.
     */
   private val byteSliceToStrFuncName: String = "byteSliceToStrFunc"
   private val byteSliceToStrFuncGenerator: FunctionGenerator[Unit] = new FunctionGenerator[Unit] {
@@ -294,13 +306,19 @@ class StringEncoding extends LeafTypeEncoding {
           in.Access(in.Accessible.Address(in.IndexedExp(param, qtfVar, paramT)(info)), in.WildcardPerm(info))(info)
         )(info)
       )(info)
+      val post = in.ExprAssertion(
+        in.EqCmp(
+          in.Length(param)(info),
+          in.Length(res)(info),
+        )(info)
+      )(info)
 
       val func: in.PureFunction = in.PureFunction(
         name = in.FunctionProxy(byteSliceToStrFuncName)(info),
         args = Vector(param),
         results = Vector(res),
         pres = Vector(pre),
-        posts = Vector(),
+        posts = Vector(post),
         terminationMeasures = Vector(in.WildcardMeasure(None)(info)),
         backendAnnotations = Vector.empty,
         body = None,

diff --git a/src/test/resources/regressions/features/conversion/conversion-simple01.gobra b/src/test/resources/regressions/features/conversion/conversion-simple01.gobra
@@ -5,3 +5,15 @@ package main
 
 ensures res == int64(i)
 func to64(i int8) (res int64)
+
+func stringToByteSlConversion() {
+	key := []byte("dummy key xxxxxx")
+	assert acc(&key[0])
+	assert len(key) > 0
+}
+
+func byteSlToStringConversion() {
+	keyBytes := []byte{'a', 'b', 'c'}
+	key := string(keyBytes)
+	assert 0 < len(key)
+}