Ensure ASCIIStringEncoder does not attempt to decode strings of length < 2
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?