Skip to content

Ensure ASCIIStringEncoder does not attempt to decode strings of length < 2

Viktor Kuncak requested to merge github/fork/romac/asciistringencoder-bug into master

Created by: romac

Previously, when decoder would attempt to read the first two bytes of any non-empty string it was given, which obviously fails when the string has length 1. This commit fixes that by directly returning any string of length < 2.

I ran into this bug while running the termination checker over this benchmark:

import stainless.lang._
import stainless.annotation._
import stainless.collection._

object kv {

  sealed abstract class Label
  object Label {
    case class Get(key: String) extends Label
    case class Put(key: String, value: String) extends Label
  }

  sealed abstract class Op
  case class Pure(value: Option[String]) extends Op
  case class Get(key: String, next: Option[String] => Op) extends Op
  case class Put(key: String, value: String, next: () => Op) extends Op

  def get(key: String)(next: Option[String] => Op): Op = Get(key, next)
  def put(key: String, value: String)(next: () => Op): Op = Put(key, value, next)
  def pure(value: Option[String]): Op = Pure(value)

  val program =
    put("foo", "bar") { () =>
      get("foo") { value =>
        pure(value)
      }
    }

  def interpret(op: Op)(kv: Map[String, String], trace: List[Label], fuel: Int): (Option[String], List[Label]) = {
    require(fuel > 0)
    decreases(fuel)

    op match {
      case Get(key, next) =>
        interpret(next(kv get key))(kv, Label.Get(key) :: trace, fuel - 1)

      case Put(key, value, next) =>
        interpret(next())(kv.updated(key, value), Label.Put(key, value) :: trace, fuel - 1)

      case Pure(value) =>
        (value, trace)
    }
  }

  def test(map: Map[String, String], trace: List[Label]) = {
    val (res, resTrace) = interpret(program)(map, trace, 100)
    res == Some("bar") &&
    resTrace.take(2).reverse == List(Label.Put("foo", "bar"), Label.Get("foo"))
  } holds

}

Should I submit it to stainless, or should I rather add the TIP output from the termination checker to inox' test suite, or both?

Merge request reports