epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 49 forks source link

Error reporting from alias analysis #1513

Open vkuncak opened 2 months ago

vkuncak commented 2 months ago

In Version: 0.9.8.2-24-g54399d0-SNAPSHOT, this program:

object Test {
  def setFirst(a: Array[Int]): Array[Int] = 
    require(a.size > 0)
    a(0) = 1    
    a

  def test =
    val a = Array.fill(10)(0)
    val b = setFirst(a)
    b(0) = 2
}

gives a low level error message:

[ Error  ] Test.scala:9:13: Couldn't apply effect ReplacementEffect(b(0)) on expression var res: (Array[Int], Array[Int]) = setFirst(a)        
[ Error  ] a = @DropVCs @DropVCs res._2.asInstanceOf[Array[Int]]
[ Error  ] a = @DropVCs @DropVCs a.asInstanceOf[Array[Int]]
[ Error  ] res._1
               val b = setFirst(a)
                       ^^^^^^^^^^^

whereas assigning to the other aliased variable:

object Test {
  def setFirst(a: Array[Int]): Array[Int] = 
    require(a.size > 0)
    a(0) = 1    
    a

  def test =
    val a = Array.fill(10)(0)
    val b = setFirst(a)
    a(0) = 2
}

gives:

[ Error  ] Test.scala:9:5: Unsupported `val` definition in AntiAliasing
[ Error  ] The following variables of mutable types are shared between the binding and the body:
[ Error  ]   a: Array[Int]
               val b = setFirst(a)
               ^^^^^^^^^^^^^^^^^^^

Finally,

object Test {
  def setFirst(a: Array[Int]): Array[Int] = 
    require(a.size > 0)
    a(0) = 1    
    a

  def test =
    val a = Array.fill(10)(0)
    val b = setFirst(a)
  ()
}

actually passes, which is sort of nice, but makes things possibly hard to understand.