Convert throw into assert(false)

[vkuncak]

This is a pragmatic way to permit certain restricted code that throws exceptions while requiring that it is never invoked. It does not require lifting the entire semantics to support exceptions (which would be a more general and higher-impact solution).

I suggest that we do convert throw E into assert("Exception E thrown", false) instead of disallowing it. This will allow Stainless to accept code containing throw that should not really be reached, so it can be useful for porting existing Scala code.

We can hopefully also accept Exception as a super class (e.g. define it in stainless.lang) and permit its subclasses.

For now, we continue to disallow try in the code Stainless handles (it may make sense in lots of extern wrappers, of course).

[vkuncak]

Perhaps a clean way to do it would be to define in stainless.lang:

@extern
def throwReached[A](s: String): A
  require(false)
  ???

and then replace throw E with a call to throwReached("E")

[vkuncak]

One advantage of using such exception instead of assert is that, if ghost code is eliminated but Stainless function is used from unverified Scala code that does not meet the require clauses that Stainless assumed, then errors thrown will be easier to react to and classify than assertions.

[vkuncak]

If we address this with a PR, we should simultaneously add the Try type https://github.com/scala/scala/blob/v2.13.3/src/library/scala/util/Try.scala#L64

To handle exception handling outside code (such as I/O) the users should write

@extern
def myMethods(x:A): Try[B] = {
   Try(BufferedMuffeledReaderWriter(...))
}

where Try is defined in stainless.lang

[samuelchassot]

We can hopefully also accept Exception as a super class (e.g. define it in stainless.lang) and permit its subclasses.

Here users would have to redefine their own exception classes to use subclasses, right? For example, to use IllegalArgumentException, one would have to define her own IllegalArgumentException that extends stainless.lang.Exception. Or am I missing something?

[samuelchassot]

https://github.com/epfl-lara/stainless/blob/54399d0a62cabd8c2480b8a14cc1fbf0d684e426/frontends/library/stainless/lang/package.scala#L41

there was a tentative apparently.

[samuelchassot]

This compiles, once I removed the check in FragmentChecker:

import stainless.lang.Exception

class IllegalArgumentException(msg: String) extends Exception

object ThrowTest {
  def f(): Unit = 
    throw new IllegalArgumentException("This is an exception")
}

Now I'll be working on the extraction of throw

[vkuncak]

Sounds good. Yes, I guess users need to declare the exceptions. Having our own synonyms, including a constructor for Exception("...") might be useful.