Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

StackOverflowError on an equivalence checking example #180

Open
drganam opened this issue Apr 3, 2022 · 0 comments
Open

StackOverflowError on an equivalence checking example #180

drganam opened this issue Apr 3, 2022 · 0 comments

Comments

@drganam
Copy link
Collaborator

drganam commented Apr 3, 2022

The following (minimized) equivalence checking example crashes with a StackOverflowError:

import stainless.lang._

object C_mem_sol1 {

  sealed abstract class Formula {}
  case class True() extends Formula
  case class Imply(p1: Formula, p2: Formula) extends Formula

  def eval1(f: Formula): Boolean = {
    f match {
      case True() => true
      case Imply(p1, p2) => true // modified, for simplification
    }
  }

  def eval(f: Formula): Boolean = {
    f match {
      case True() => true
      case Imply(f1, f2) => {
        (eval(f1), eval(f2)) match {
          case (true, true) => true
          case (true, false) => false
          case (false, true) => true
          case (false, false) => true
        }
      }
    }
  }

  def eval_template(f: Formula): Boolean = {
    f match {
      case True() => { true }
      case Imply(f1, f2) => {
        (eval_template(f1), eval_template(f2)) match {
          case (true, true) => true
          case (true, false) => false
          case (false, true) => true
          case (false, false) => true
        }
      }
    }
  } ensuring(_ => eval(f) == eval1(f))

}

Stack trace:

java.lang.StackOverflowError
	at inox.ast.Definitions$$anon$1.convert(Definitions.scala:70)
	at inox.ast.Definitions$$anon$1.convert(Definitions.scala:67)
	at inox.ast.Definitions$VariableSymbol.to(Definitions.scala:50)
	at inox.ast.Definitions$VariableSymbol.to$(Definitions.scala:50)
	at inox.ast.Expressions$Variable.to(Expressions.scala:46)
	at inox.ast.Expressions$Variable.toVal(Expressions.scala:50)
	at inox.transformers.Transformer.$anonfun$transform$3(Transformer.scala:63)
	at scala.collection.immutable.List.map(List.scala:293)
	at inox.transformers.Transformer.transform(Transformer.scala:62)
	at inox.transformers.Transformer.transform$(Transformer.scala:51)
	at inox.ast.SymbolOps$$anon$1.inox$transformers$SimplifierWithPC$$super$transform(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:307)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:163)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.$anonfun$simplify$18(SimplifierWithPC.scala:267)
	at scala.collection.immutable.List.map(List.scala:293)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:267)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.$anonfun$simplify$26(SimplifierWithPC.scala:278)
	at scala.collection.immutable.List.map(List.scala:293)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:278)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:207)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.$anonfun$simplifyAndCons$1(SimplifierWithPC.scala:316)
	at scala.collection.immutable.List.map(List.scala:293)
	at inox.transformers.SimplifierWithPC.simplifyAndCons(SimplifierWithPC.scala:316)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:271)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:107)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:131)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:233)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:219)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90)
	at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90)
	at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.isPureFunction(SimplifierWithPC.scala:63)
	at inox.transformers.SimplifierWithPC.isPureFunction$(SimplifierWithPC.scala:54)
	at inox.ast.SymbolOps$$anon$1.isPureFunction(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:268)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.$anonfun$simplifyAndCons$1(SimplifierWithPC.scala:316)
	at scala.collection.immutable.List.map(List.scala:293)
	at inox.transformers.SimplifierWithPC.simplifyAndCons(SimplifierWithPC.scala:316)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:271)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:107)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90)
	at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90)
	at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33)
	at inox.ast.SymbolOps.isPureIn(SymbolOps.scala:215)
	at inox.ast.SymbolOps.isPureIn$(SymbolOps.scala:207)
	at inox.ast.SimpleSymbols$SimpleSymbols.isPureIn(SimpleSymbols.scala:12)
	at inox.ast.SymbolOps.isPure(SymbolOps.scala:202)
	at inox.ast.SymbolOps.isPure$(SymbolOps.scala:202)
	at inox.ast.SimpleSymbols$SimpleSymbols.isPure(SimpleSymbols.scala:12)
	at inox.ast.SymbolOps.isAlwaysPure(SymbolOps.scala:204)
	at inox.ast.SymbolOps.isAlwaysPure$(SymbolOps.scala:204)
	at inox.ast.SimpleSymbols$SimpleSymbols.isAlwaysPure(SimpleSymbols.scala:12)
	at inox.ast.SymbolOps.ifExpr(SymbolOps.scala:1183)
	at inox.ast.SymbolOps.ifExpr$(SymbolOps.scala:1182)
	at inox.ast.SimpleSymbols$SimpleSymbols.ifExpr(SimpleSymbols.scala:12)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:140)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:233)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:219)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90)
	at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90)
	at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.isPureFunction(SimplifierWithPC.scala:63)
	at inox.transformers.SimplifierWithPC.isPureFunction$(SimplifierWithPC.scala:54)
	at inox.ast.SymbolOps$$anon$1.isPureFunction(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:268)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.$anonfun$simplifyAndCons$1(SimplifierWithPC.scala:316)
	at scala.collection.immutable.List.map(List.scala:293)
	at inox.transformers.SimplifierWithPC.simplifyAndCons(SimplifierWithPC.scala:316)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:271)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:107)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90)
	at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90)
	at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33)
	at inox.ast.SymbolOps.isPureIn(SymbolOps.scala:215)
	at inox.ast.SymbolOps.isPureIn$(SymbolOps.scala:207)
	at inox.ast.SimpleSymbols$SimpleSymbols.isPureIn(SimpleSymbols.scala:12)
	at inox.ast.SymbolOps.isPure(SymbolOps.scala:202)
	at inox.ast.SymbolOps.isPure$(SymbolOps.scala:202)
	at inox.ast.SimpleSymbols$SimpleSymbols.isPure(SimpleSymbols.scala:12)
	at inox.ast.SymbolOps.isAlwaysPure(SymbolOps.scala:204)
	at inox.ast.SymbolOps.isAlwaysPure$(SymbolOps.scala:204)
	at inox.ast.SimpleSymbols$SimpleSymbols.isAlwaysPure(SimpleSymbols.scala:12)
	at inox.ast.SymbolOps.ifExpr(SymbolOps.scala:1183)
	at inox.ast.SymbolOps.ifExpr$(SymbolOps.scala:1182)
	at inox.ast.SimpleSymbols$SimpleSymbols.ifExpr(SimpleSymbols.scala:12)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:140)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:233)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:219)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90)
	at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90)
	at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.isPureFunction(SimplifierWithPC.scala:63)
	at inox.transformers.SimplifierWithPC.isPureFunction$(SimplifierWithPC.scala:54)
	at inox.ast.SymbolOps$$anon$1.isPureFunction(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:268)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.$anonfun$simplifyAndCons$1(SimplifierWithPC.scala:316)
	at scala.collection.immutable.List.map(List.scala:293)
	at inox.transformers.SimplifierWithPC.simplifyAndCons(SimplifierWithPC.scala:316)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:271)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:107)
	at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92)
	at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33)
	at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90)
	at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90)
	at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33)
	at inox.ast.SymbolOps.isPureIn(SymbolOps.scala:215)
	at inox.ast.SymbolOps.isPureIn$(SymbolOps.scala:207)
	at inox.ast.SimpleSymbols$SimpleSymbols.isPureIn(SimpleSymbols.scala:12)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@drganam