diff --git a/.larabot.conf b/.larabot.conf
index 824096f103fe25bb3c6b135e0bc84bc9fbda98d0..6a037e0addc616364cb0b049075beb1f7c2d18c7 100644
--- a/.larabot.conf
+++ b/.larabot.conf
@@ -2,6 +2,7 @@ commands = [
"sbt -batch test"
"sbt -batch integration:test"
"sbt -batch regression:test"
+ "sbt -batch genc:test"
]
trusted = [
diff --git a/build.sbt b/build.sbt
index b825fa5ba9146d4bb9e2c23f41edf3e6f756188f..0e3e147a10e395fb58a0ebb3f981b9919deb56b9 100644
--- a/build.sbt
+++ b/build.sbt
@@ -141,6 +141,14 @@ parallelExecution in IsabelleTest := false
fork in IsabelleTest := true
+// GenC Tests
+lazy val GenCTest = config("genc") extend(Test)
+
+testOptions in GenCTest := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWith "leon.genc."))
+
+parallelExecution in GenCTest := false
+
+
def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
@@ -148,9 +156,11 @@ lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "10ea
lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "372bb14d0c84953acc17f9a7e1592087adb0a3e1")
lazy val root = (project in file(".")).
- configs(RegressionTest, IsabelleTest, IntegrTest).
+ configs(RegressionTest, IsabelleTest, GenCTest, IntegrTest).
dependsOn(bonsai, scalaSmtLib).
settings(inConfig(RegressionTest)(Defaults.testTasks ++ testSettings): _*).
settings(inConfig(IntegrTest)(Defaults.testTasks ++ testSettings): _*).
settings(inConfig(IsabelleTest)(Defaults.testTasks ++ testSettings): _*).
+ settings(inConfig(GenCTest)(Defaults.testTasks ++ testSettings): _*).
settings(inConfig(Test)(Defaults.testTasks ++ testSettings): _*)
+
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 9cc0dc9c6af811444024a05dd95b93c518df31eb..f238d4a854bd881c74a3205ef5b727a220e34ae1 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -27,7 +27,9 @@ object Main {
solvers.isabelle.AdaptationPhase,
solvers.isabelle.IsabellePhase,
transformations.InstrumentationPhase,
- invariant.engine.InferInvariantsPhase)
+ invariant.engine.InferInvariantsPhase,
+ genc.GenerateCPhase,
+ genc.CFileOutputPhase)
}
// Add whatever you need here.
@@ -53,9 +55,10 @@ object Main {
val optHelp = LeonFlagOptionDef("help", "Show help message", false)
val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false)
val optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
+ val optGenc = LeonFlagOptionDef("genc", "Generate C code", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv)
+ Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optGenc)
}
lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)
@@ -151,6 +154,8 @@ object Main {
import repair.RepairPhase
import evaluators.EvaluationPhase
import solvers.isabelle.IsabellePhase
+ import genc.GenerateCPhase
+ import genc.CFileOutputPhase
import MainComponent._
import invariant.engine.InferInvariantsPhase
import transformations.InstrumentationPhase
@@ -163,11 +168,17 @@ object Main {
val isabelleF = ctx.findOptionOrDefault(optIsabelle)
val terminationF = ctx.findOptionOrDefault(optTermination)
val verifyF = ctx.findOptionOrDefault(optVerify)
+ val gencF = ctx.findOptionOrDefault(optGenc)
val evalF = ctx.findOption(optEval).isDefined
val inferInvF = ctx.findOptionOrDefault(optInferInv)
val instrumentF = ctx.findOptionOrDefault(optInstrument)
val analysisF = verifyF && terminationF
+ // Check consistency in options
+ if (gencF && !xlangF) {
+ ctx.reporter.fatalError("Generating C code with --genc requires --xlang")
+ }
+
if (helpF) {
displayVersion(ctx.reporter)
displayHelp(ctx.reporter, error = false)
@@ -175,7 +186,7 @@ object Main {
val pipeBegin: Pipeline[List[String], Program] =
ClassgenPhase andThen
ExtractionPhase andThen
- new PreprocessingPhase(xlangF)
+ new PreprocessingPhase(xlangF, gencF)
val verification = if (xlangF) VerificationPhase andThen FixReportLabels else VerificationPhase
@@ -189,6 +200,7 @@ object Main {
else if (evalF) EvaluationPhase
else if (inferInvF) InferInvariantsPhase
else if (instrumentF) InstrumentationPhase andThen FileOutputPhase
+ else if (gencF) GenerateCPhase andThen CFileOutputPhase
else verification
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index aa1e07e3c0c98834a538c633558be2c37875794b..3e93664008654edef6fa057c56451db0a108bc6b 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -153,7 +153,7 @@ trait CodeExtraction extends ASTExtractors {
}
private def isIgnored(s: Symbol) = {
- (annotationsOf(s) contains "ignore") || s.fullName.toString.endsWith(".main")
+ (annotationsOf(s) contains "ignore")
}
private def isLibrary(u: CompilationUnit) = Build.libFiles contains u.source.file.absolute.path
@@ -625,6 +625,8 @@ trait CodeExtraction extends ASTExtractors {
}
}
+ private var isLazy = Set[LeonValDef]()
+
private var defsToDefs = Map[Symbol, FunDef]()
private def defineFunDef(sym: Symbol, within: Option[LeonClassDef] = None)(implicit dctx: DefContext): FunDef = {
@@ -638,7 +640,13 @@ trait CodeExtraction extends ASTExtractors {
val tpe = if (sym.isByNameParam) FunctionType(Seq(), ptpe) else ptpe
val newID = FreshIdentifier(sym.name.toString, tpe).setPos(sym.pos)
owners += (newID -> None)
- LeonValDef(newID, sym.isByNameParam).setPos(sym.pos)
+ val vd = LeonValDef(newID).setPos(sym.pos)
+
+ if (sym.isByNameParam) {
+ isLazy += vd
+ }
+
+ vd
}
val tparamsDef = tparams.map(t => TypeParameterDef(t._2))
@@ -1534,7 +1542,7 @@ trait CodeExtraction extends ASTExtractors {
val fd = getFunDef(sym, c.pos)
val newTps = tps.map(t => extractType(t))
- val argsByName = (fd.params zip args).map(p => if (p._1.isLazy) Lambda(Seq(), p._2) else p._2)
+ val argsByName = (fd.params zip args).map(p => if (isLazy(p._1)) Lambda(Seq(), p._2) else p._2)
FunctionInvocation(fd.typed(newTps), argsByName)
@@ -1543,7 +1551,7 @@ trait CodeExtraction extends ASTExtractors {
val cd = methodToClass(fd)
val newTps = tps.map(t => extractType(t))
- val argsByName = (fd.params zip args).map(p => if (p._1.isLazy) Lambda(Seq(), p._2) else p._2)
+ val argsByName = (fd.params zip args).map(p => if (isLazy(p._1)) Lambda(Seq(), p._2) else p._2)
MethodInvocation(rec, cd, fd.typed(newTps), argsByName)
diff --git a/src/main/scala/leon/genc/CAST.scala b/src/main/scala/leon/genc/CAST.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9a9242859e799488eeb8a42170f6fcedd1b0dd13
--- /dev/null
+++ b/src/main/scala/leon/genc/CAST.scala
@@ -0,0 +1,296 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package genc
+
+import utils.UniqueCounter
+
+/*
+ * Here are defined classes used to represent AST of C programs.
+ */
+
+object CAST { // C Abstract Syntax Tree
+
+ sealed abstract class Tree
+ case object NoTree extends Tree
+
+
+ /* ------------------------------------------------------------ Types ----- */
+ abstract class Type(val rep: String) extends Tree {
+ override def toString = rep
+
+ def mutable: Type = this match {
+ case Const(typ) => typ.mutable
+ case _ => this
+ }
+ }
+
+ /* Type Modifiers */
+ case class Const(typ: Type) extends Type(s"$typ const")
+ case class Pointer(typ: Type) extends Type(s"$typ*")
+
+ /* Primitive Types */
+ case object Int32 extends Type("int32_t") // Requires <stdint.h>
+ case object Bool extends Type("bool") // Requires <stdbool.h>
+ case object Void extends Type("void")
+
+ /* Compound Types */
+ case class Struct(id: Id, fields: Seq[Var]) extends Type(id.name)
+
+
+ /* --------------------------------------------------------- Literals ----- */
+ case class IntLiteral(v: Int) extends Stmt
+ case class BoolLiteral(b: Boolean) extends Stmt
+
+
+ /* ----------------------------------------------------- Definitions ----- */
+ abstract class Def extends Tree
+
+ case class Prog(structs: Seq[Struct], functions: Seq[Fun]) extends Def
+
+ case class Fun(id: Id, retType: Type, params: Seq[Var], body: Stmt) extends Def
+
+ case class Id(name: String) extends Def {
+ // `|` is used as the margin delimiter and can cause trouble in some situations
+ def fixMargin =
+ if (name.size > 0 && name(0) == '|') "| " + name
+ else name
+ }
+
+ case class Var(id: Id, typ: Type) extends Def
+
+ /* ----------------------------------------------------------- Stmts ----- */
+ abstract class Stmt extends Tree
+ case object NoStmt extends Stmt
+
+ case class Compound(stmts: Seq[Stmt]) extends Stmt
+
+ case class Assert(pred: Stmt, error: Option[String]) extends Stmt { // Requires <assert.h>
+ require(pred.isValue)
+ }
+
+ case class DeclVar(x: Var) extends Stmt
+
+ case class DeclInitVar(x: Var, value: Stmt) extends Stmt {
+ require(value.isValue)
+ }
+
+ case class Assign(lhs: Stmt, rhs: Stmt) extends Stmt {
+ require(lhs.isValue && rhs.isValue)
+ }
+
+ // Note: we don't need to differentiate between specific
+ // operators so we only keep track of the "kind" of operator
+ // with an Id.
+ case class UnOp(op: Id, rhs: Stmt) extends Stmt {
+ require(rhs.isValue)
+ }
+
+ case class MultiOp(op: Id, stmts: Seq[Stmt]) extends Stmt {
+ require(stmts.length > 1 && stmts.forall { _.isValue })
+ }
+
+ case class SubscriptOp(ptr: Stmt, idx: Stmt) extends Stmt {
+ require(ptr.isValue && idx.isValue)
+ }
+
+ case object Break extends Stmt
+
+ case class Return(stmt: Stmt) extends Stmt {
+ require(stmt.isValue)
+ }
+
+ case class IfElse(cond: Stmt, thn: Stmt, elze: Stmt) extends Stmt {
+ require(cond.isValue)
+ }
+
+ case class While(cond: Stmt, body: Stmt) extends Stmt {
+ require(cond.isValue)
+ }
+
+ case class AccessVar(id: Id) extends Stmt
+ case class AccessRef(id: Id) extends Stmt
+ case class AccessAddr(id: Id) extends Stmt
+ case class AccessField(struct: Stmt, field: Id) extends Stmt {
+ require(struct.isValue)
+ }
+
+ case class Call(id: Id, args: Seq[Stmt]) extends Stmt {
+ require(args forall { _.isValue })
+ }
+
+ case class StructInit(args: Seq[(Id, Stmt)], struct: Struct) extends Stmt {
+ require(args forall { _._2.isValue })
+ }
+
+ case class ArrayInit(length: Stmt, valueType: Type, defaultValue: Stmt) extends Stmt {
+ require(length.isValue && defaultValue.isValue)
+ }
+
+ case class ArrayInitWithValues(valueType: Type, values: Seq[Stmt]) extends Stmt {
+ require(values forall { _.isValue })
+
+ lazy val length = values.length
+ }
+
+
+ /* -------------------------------------------------------- Factories ----- */
+ object Op {
+ def apply(op: String, rhs: Stmt) = UnOp(Id(op), rhs)
+ def apply(op: String, rhs: Stmt, lhs: Stmt) = MultiOp(Id(op), rhs :: lhs :: Nil)
+ def apply(op: String, stmts: Seq[Stmt]) = MultiOp(Id(op), stmts)
+ }
+
+ object Val {
+ def apply(id: Id, typ: Type) = typ match {
+ case Const(_) => Var(id, typ) // avoid const of const
+ case _ => Var(id, Const(typ))
+ }
+ }
+
+ /* "Templatetized" Types */
+ object Tuple {
+ def apply(bases: Seq[Type]) = {
+ val name = Id("__leon_tuple_" + bases.mkString("_") + "_t")
+
+ val fields = bases.zipWithIndex map {
+ case (typ, idx) => Var(getNthId(idx + 1), typ)
+ }
+
+ Struct(name, fields)
+ }
+
+ // Indexes start from 1, not 0!
+ def getNthId(n: Int) = Id("_" + n)
+ }
+
+ object Array {
+ def apply(base: Type) = {
+ val name = Id("__leon_array_" + base + "_t")
+ val data = Var(dataId, Pointer(base))
+ val length = Var(lengthId, Int32)
+ val fields = data :: length :: Nil
+
+ Struct(name, fields)
+ }
+
+ def lengthId = Id("length")
+ def dataId = Id("data")
+ }
+
+
+ /* ---------------------------------------------------- Introspection ----- */
+ implicit class IntrospectionOps(val stmt: Stmt) {
+ def isLiteral = stmt match {
+ case _: IntLiteral => true
+ case _: BoolLiteral => true
+ case _ => false
+ }
+
+ // True if statement can be used as a value
+ def isValue: Boolean = isLiteral || {
+ stmt match {
+ //case _: Assign => true it's probably the case but for now let's ignore it
+ case c: Compound => c.stmts.size == 1 && c.stmts.head.isValue
+ case _: UnOp => true
+ case _: MultiOp => true
+ case _: SubscriptOp => true
+ case _: AccessVar => true
+ case _: AccessRef => true
+ case _: AccessAddr => true
+ case _: AccessField => true
+ case _: Call => true
+ case _: StructInit => true
+ case _: ArrayInit => true
+ case _: ArrayInitWithValues => true
+ case _ => false
+ }
+ }
+
+ def isPure: Boolean = isLiteral || {
+ stmt match {
+ case NoStmt => true
+ case Compound(stmts) => stmts forall { _.isPure }
+ case Assert(pred, _) => pred.isPure
+ case UnOp(_, rhs) => rhs.isPure
+ case MultiOp(_, stmts) => Compound(stmts).isPure
+ case SubscriptOp(ptr, idx) => (ptr ~ idx).isPure
+ case IfElse(c, t, e) => (c ~ t ~ e).isPure
+ case While(c, b) => (c ~ b).isPure
+ case AccessVar(_) => true
+ case AccessRef(_) => true
+ case AccessAddr(_) => true
+ case AccessField(s, _) => s.isPure
+ // case Call(id, args) => true if args are pure and function `id` is pure too
+ case _ => false
+ }
+ }
+
+ def isPureValue = isValue && isPure
+ }
+
+
+ /* ------------------------------------------------------------- DSL ----- */
+ // Operator ~~ appends and flattens nested compounds
+ implicit class StmtOps(val stmt: Stmt) {
+ // In addition to combining statements together in a compound
+ // we remove the empty ones and if the resulting compound
+ // has only one statement we return this one without being
+ // wrapped into a Compound
+ def ~(other: Stmt) = {
+ val stmts = (stmt, other) match {
+ case (Compound(stmts), Compound(others)) => stmts ++ others
+ case (stmt , Compound(others)) => stmt +: others
+ case (Compound(stmts), other ) => stmts :+ other
+ case (stmt , other ) => stmt :: other :: Nil
+ }
+
+ def isNoStmt(s: Stmt) = s match {
+ case NoStmt => true
+ case _ => false
+ }
+
+ val compound = Compound(stmts filterNot isNoStmt)
+ compound match {
+ case Compound(stmts) if stmts.length == 0 => NoStmt
+ case Compound(stmts) if stmts.length == 1 => stmts.head
+ case compound => compound
+ }
+ }
+
+ def ~~(others: Seq[Stmt]) = stmt ~ Compound(others)
+ }
+
+ implicit class StmtsOps(val stmts: Seq[Stmt]) {
+ def ~~(other: Stmt) = other match {
+ case Compound(others) => Compound(stmts) ~~ others
+ case other => Compound(stmts) ~ other
+ }
+
+ def ~~~(others: Seq[Stmt]) = Compound(stmts) ~~ others
+ }
+
+ val True = BoolLiteral(true)
+ val False = BoolLiteral(false)
+
+
+ /* ------------------------------------------------ Fresh Generators ----- */
+ object FreshId {
+ private var counter = -1
+ private val leonPrefix = "__leon_"
+
+ def apply(prefix: String = ""): Id = {
+ counter += 1
+ Id(leonPrefix + prefix + counter)
+ }
+ }
+
+ object FreshVar {
+ def apply(typ: Type, prefix: String = "") = Var(FreshId(prefix), typ)
+ }
+
+ object FreshVal {
+ def apply(typ: Type, prefix: String = "") = Val(FreshId(prefix), typ)
+ }
+}
+
diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a979fd8dd0c28351948270048adf53ed597a1317
--- /dev/null
+++ b/src/main/scala/leon/genc/CConverter.scala
@@ -0,0 +1,708 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package genc
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Expressions._
+import purescala.Types._
+import xlang.Expressions._
+
+import scala.reflect.ClassTag
+
+// don't import CAST._ to decrease possible confusion between the two ASTs
+
+class CConverter(val ctx: LeonContext, val prog: Program) {
+ def convert: CAST.Prog = convertToProg(prog)
+
+ // Global data: keep track of the custom types and function of the input program
+ // Using sequences and not sets to keep track of order/dependencies
+ private var typeDecls = Seq[CAST.Struct]()
+ private var functions = Seq[CAST.Fun]()
+
+ // Extra information about inner functions' context
+ // See classes VarInfo and FunCtx and functions convertToFun and
+ // FunctionInvocation conversion
+ private var funExtraArgss = Map[CAST.Id, Seq[CAST.Id]]()
+ private val emptyFunCtx = FunCtx(Seq())
+
+ private def registerType(typ: CAST.Struct) {
+ // Types might be processed more than once as the corresponding CAST type
+ // is not cached and need to be reconstructed several time if necessary
+ if (!typeDecls.contains(typ)) {
+ typeDecls = typeDecls :+ typ
+ debug(s"New type registered: $typ")
+ }
+ }
+
+ private def registerFun(fun: CAST.Fun) {
+ // Unlike types, functions should not get defined multiple times as this
+ // would imply invalidating funExtraArgss
+ if (functions contains fun)
+ internalError("Function ${fun.id} defined more than once")
+ else
+ functions = functions :+ fun
+ }
+
+ // Register extra function argument for the function named `id`
+ private def registerFunExtraArgs(id: CAST.Id, params: Seq[CAST.Id]) {
+ funExtraArgss = funExtraArgss + ((id, params))
+ }
+
+ // Get the extra argument identifiers for the function named `id`
+ private def getFunExtraArgs(id: CAST.Id) = funExtraArgss.getOrElse(id, Seq())
+
+ // Apply the conversion function and make sure the resulting AST matches our expectation
+ private def convertTo[T](tree: Tree)(implicit funCtx: FunCtx, ct: ClassTag[T]): T = convert(tree) match {
+ case t: T => t
+ case x => internalError(s"Expected an instance of $ct when converting $tree but got $x")
+ }
+
+ // Generic conversion function
+ // Currently simple aliases in case we need later to have special treatment instead
+ private def convertToType (tree: Tree)(implicit funCtx: FunCtx) = convertTo[CAST.Type](tree)
+ private def convertToStruct(tree: Tree)(implicit funCtx: FunCtx) = convertTo[CAST.Struct](tree)
+ private def convertToId (tree: Tree)(implicit funCtx: FunCtx) = convertTo[CAST.Id](tree)
+ private def convertToStmt (tree: Tree)(implicit funCtx: FunCtx) = convertTo[CAST.Stmt](tree)
+ private def convertToVar (tree: Tree)(implicit funCtx: FunCtx) = convertTo[CAST.Var](tree)
+
+ private def convertToProg(prog: Program): CAST.Prog = {
+ // Only process the main unit
+ val (mainUnits, _) = prog.units partition { _.isMainUnit }
+
+ if (mainUnits.size == 0) fatalError("No main unit in the program")
+ if (mainUnits.size >= 2) fatalError("Multiple main units in the program")
+
+ val mainUnit = mainUnits.head
+
+ debug(s"Converting the main unit:\n$mainUnit")
+ collectSymbols(mainUnit)
+
+ CAST.Prog(typeDecls, functions)
+ }
+
+ // Look for function and structure definitions
+ private def collectSymbols(unit: UnitDef) {
+ implicit val defaultFunCtx = emptyFunCtx
+
+ unit.defs.foreach {
+ case ModuleDef(_, funDefs, _) =>
+ funDefs.foreach {
+ case fd: FunDef => convertToFun(fd) // the function gets registered here
+ case cc: CaseClassDef => convertToStruct(cc) // the type declaration gets registered here
+
+ case x => internalError(s"Unknown function definition $x: ${x.getClass}")
+ }
+
+ case x => internalError(s"Unexpected definition $x instead of a ModuleDef")
+ }
+ }
+
+ // A variable can be locally declared (e.g. function parameter or local variable)
+ // or it can be "inherited" from a more global context (e.g. inner functions have
+ // access to their outer function parameters).
+ private case class VarInfo(x: CAST.Var, local: Boolean) {
+ // Transform a local variable into a global variable
+ def lift = VarInfo(x, false)
+
+ // Generate CAST variable declaration for function signature
+ def toParam = CAST.Var(x.id, CAST.Pointer(x.typ))
+
+ // Generate CAST access statement
+ def toArg = if (local) CAST.AccessAddr(x.id) else CAST.AccessVar(x.id)
+ }
+
+ private case class FunCtx(vars: Seq[VarInfo]) {
+ // Transform local variables into "outer" variables
+ def lift = FunCtx(vars map { _.lift })
+
+ // Create a new context with more local variables
+ def extend(x: CAST.Var): FunCtx = extend(Seq(x))
+ def extend(xs: Seq[CAST.Var]): FunCtx = {
+ val newVars = xs map { VarInfo(_, true) }
+ FunCtx(vars ++ newVars)
+ }
+
+ // Check if a given variable's identifier exists in the context and is an "outer" variable
+ def hasOuterVar(id: CAST.Id) = vars exists { vi => !vi.local && vi.x.id == id }
+
+ // List all variables' ids
+ def extractIds = vars map { _.x.id }
+
+ // Generate arguments for the given identifiers according to the current context
+ def toArgs(ids: Seq[CAST.Id]) = {
+ val filtered = vars filter { ids contains _.x.id }
+ filtered map { _.toArg }
+ }
+
+ // Generate parameters (var + type)
+ def toParams = vars map { _.toParam }
+ }
+
+ // Extract inner functions too
+ private def convertToFun(fd: FunDef)(implicit funCtx: FunCtx) = {
+ // Forbid return of array as they are allocated on the stack
+ if (containsArrayType(fd.returnType)) {
+ fatalError("Returning arrays is currently not allowed")
+ }
+
+ val id = convertToId(fd.id)
+ val retType = convertToType(fd.returnType)
+ val stdParams = fd.params map convertToVar
+
+ // Prepend existing variables from the outer function context to
+ // this function's parameters
+ val extraParams = funCtx.toParams
+ val params = extraParams ++ stdParams
+
+ // Function Context:
+ // 1) Save the variables of the current context for later function invocation
+ // 2) Lift & augment funCtx with the current function's arguments
+ // 3) Propagate it to the current function's body
+
+ registerFunExtraArgs(id, funCtx.extractIds)
+
+ val funCtx2 = funCtx.lift.extend(stdParams)
+
+ val b = convertToStmt(fd.fullBody)(funCtx2)
+ val body = retType match {
+ case CAST.Void => b
+ case _ => injectReturn(b)
+ }
+
+ val fun = CAST.Fun(id, retType, params, body)
+ registerFun(fun)
+
+ fun
+ }
+
+ private def convert(tree: Tree)(implicit funCtx: FunCtx): CAST.Tree = tree match {
+ /* ---------------------------------------------------------- Types ----- */
+ case Int32Type => CAST.Int32
+ case BooleanType => CAST.Bool
+ case UnitType => CAST.Void
+
+ case ArrayType(base) =>
+ val typ = CAST.Array(convertToType(base))
+ registerType(typ)
+ typ
+
+ case TupleType(bases) =>
+ val typ = CAST.Tuple(bases map convertToType)
+ registerType(typ)
+ typ
+
+ case cd: CaseClassDef =>
+ if (cd.isAbstract) fatalError("Abstract types are not supported")
+ if (cd.hasParent) fatalError("Inheritance is not supported")
+ if (cd.isCaseObject) fatalError("Case Objects are not supported")
+ if (cd.tparams.length > 0) fatalError("Type Parameters are not supported")
+ if (cd.methods.length > 0) fatalError("Methods are not yet supported")
+
+ val id = convertToId(cd.id)
+ val fields = cd.fields map convertToVar
+ val typ = CAST.Struct(id, fields)
+
+ registerType(typ)
+ typ
+
+ case CaseClassType(cd, _) => convertToStruct(cd) // reuse `case CaseClassDef`
+
+ /* ------------------------------------------------------- Literals ----- */
+ case IntLiteral(v) => CAST.IntLiteral(v)
+ case BooleanLiteral(b) => CAST.BoolLiteral(b)
+ case UnitLiteral() => CAST.NoStmt
+
+ /* ------------------------------------ Definitions and Statements ----- */
+ case id: Identifier =>
+ if (id.name == "main") CAST.Id("main") // and not `main0`
+ else CAST.Id(id.uniqueName)
+
+ // Function parameter
+ case vd: ValDef => buildVal(vd.id, vd.getType)
+
+ // Accessing variable
+ case v: Variable => buildAccessVar(v.id)
+
+ case Block(exprs, last) =>
+ // Interleave the "bodies" of flatten expressions and their values
+ // and generate a Compound statement
+ (exprs :+ last) map convertToStmt reduce { _ ~ _ }
+
+ case Let(b, v, r) => buildLet(b, v, r, false)
+ case LetVar(b, v, r) => buildLet(b, v, r, true)
+
+ case LetDef(fds, rest) =>
+ fds foreach convertToFun // The functions get registered there
+ convertToStmt(rest)
+
+ case Assignment(varId, expr) =>
+ val f = convertAndFlatten(expr)
+ val x = buildAccessVar(varId)
+
+ val assign = CAST.Assign(x, f.value)
+
+ f.body ~~ assign
+
+ case tuple @ Tuple(exprs) =>
+ val struct = convertToStruct(tuple.getType)
+ val types = struct.fields map { _.typ }
+ val fs = convertAndNormaliseExecution(exprs, types)
+ val args = fs.values.zipWithIndex map {
+ case (arg, idx) => (CAST.Tuple.getNthId(idx + 1), arg)
+ }
+
+ fs.bodies ~~ CAST.StructInit(args, struct)
+
+ case TupleSelect(tuple1, idx) => // here idx is already 1-based
+ val struct = convertToStruct(tuple1.getType)
+ val tuple2 = convertToStmt(tuple1)
+
+ val fs = normaliseExecution((tuple2, struct) :: Nil)
+
+ val tuple = fs.values.head
+
+ fs.bodies ~~ CAST.AccessField(tuple, CAST.Tuple.getNthId(idx))
+
+ case ArrayLength(array1) =>
+ val array2 = convertToStmt(array1)
+ val arrayType = convertToType(array1.getType)
+
+ val fs = normaliseExecution((array2, arrayType) :: Nil)
+
+ val array = fs.values.head
+
+ fs.bodies ~~ CAST.AccessField(array, CAST.Array.lengthId)
+
+ case ArraySelect(array1, index1) =>
+ val array2 = convertToStmt(array1)
+ val arrayType = convertToType(array1.getType)
+ val index2 = convertToStmt(index1)
+
+ val fs = normaliseExecution((array2, arrayType) :: (index2, CAST.Int32) :: Nil)
+
+ val array = fs.values(0)
+ val index = fs.values(1)
+ val ptr = CAST.AccessField(array, CAST.Array.dataId)
+ val select = CAST.SubscriptOp(ptr, index)
+
+ fs.bodies ~~ select
+
+ case NonemptyArray(elems, Some((value1, length1))) if elems.isEmpty =>
+ val length2 = convertToStmt(length1)
+ val valueType = convertToType(value1.getType)
+ val value2 = convertToStmt(value1)
+
+ val fs = normaliseExecution((length2, CAST.Int32) :: (value2, valueType) :: Nil)
+ val length = fs.values(0)
+ val value = fs.values(1)
+
+ fs.bodies ~~ CAST.ArrayInit(length, valueType, value)
+
+ case NonemptyArray(elems, Some(_)) =>
+ fatalError("NonemptyArray with non empty elements is not supported")
+
+ case NonemptyArray(elems, None) => // Here elems is non-empty
+ // Sort values according the the key (aka index)
+ val indexes = elems.keySet.toSeq.sorted
+ val values = indexes map { elems(_) }
+
+ // Assert all types are the same
+ val types = values map { e => convertToType(e.getType) }
+ val typ = types(0)
+ val allSame = types forall { _ == typ }
+ if (!allSame) fatalError("Heterogenous arrays are not supported")
+
+ val fs = convertAndNormaliseExecution(values, types)
+
+ fs.bodies ~~ CAST.ArrayInitWithValues(typ, fs.values)
+
+ case ArrayUpdate(array1, index1, newValue1) =>
+ val array2 = convertToStmt(array1)
+ val index2 = convertToStmt(index1)
+ val newValue2 = convertToStmt(newValue1)
+ val values = array2 :: index2 :: newValue2 :: Nil
+
+ val arePure = values forall { _.isPure }
+ val areValues = array2.isValue && index2.isValue // no newValue here
+
+ newValue2 match {
+ case CAST.IfElse(cond, thn, elze) if arePure && areValues =>
+ val array = array2
+ val index = index2
+ val ptr = CAST.AccessField(array, CAST.Array.dataId)
+ val select = CAST.SubscriptOp(ptr, index)
+
+ val ifelse = buildIfElse(cond, injectAssign(select, thn),
+ injectAssign(select, elze))
+
+ ifelse
+
+ case _ =>
+ val arrayType = convertToType(array1.getType)
+ val indexType = CAST.Int32
+ val valueType = convertToType(newValue1.getType)
+ val types = arrayType :: indexType :: valueType :: Nil
+
+ val fs = normaliseExecution(values, types)
+
+ val array = fs.values(0)
+ val index = fs.values(1)
+ val newValue = fs.values(2)
+
+ val ptr = CAST.AccessField(array, CAST.Array.dataId)
+ val select = CAST.SubscriptOp(ptr, index)
+ val assign = CAST.Assign(select, newValue)
+
+ fs.bodies ~~ assign
+ }
+
+ case CaseClass(typ, args1) =>
+ val struct = convertToStruct(typ)
+ val types = struct.fields map { _.typ }
+ val argsFs = convertAndNormaliseExecution(args1, types)
+ val fieldsIds = typ.classDef.fieldsIds map convertToId
+ val args = fieldsIds zip argsFs.values
+
+ argsFs.bodies ~~ CAST.StructInit(args, struct)
+
+ case CaseClassSelector(_, x1, fieldId) =>
+ val struct = convertToStruct(x1.getType)
+ val x2 = convertToStmt(x1)
+
+ val fs = normaliseExecution((x2, struct) :: Nil)
+ val x = fs.values.head
+
+ fs.bodies ~~ CAST.AccessField(x, convertToId(fieldId))
+
+ case LessThan(lhs, rhs) => buildBinOp(lhs, "<", rhs)
+ case GreaterThan(lhs, rhs) => buildBinOp(lhs, ">", rhs)
+ case LessEquals(lhs, rhs) => buildBinOp(lhs, "<=", rhs)
+ case GreaterEquals(lhs, rhs) => buildBinOp(lhs, ">=", rhs)
+ case Equals(lhs, rhs) => buildBinOp(lhs, "==", rhs)
+
+ case Not(rhs) => buildUnOp ( "!", rhs)
+
+ case And(exprs) => buildMultiOp("&&", exprs)
+ case Or(exprs) => buildMultiOp("||", exprs)
+
+ case BVPlus(lhs, rhs) => buildBinOp(lhs, "+", rhs)
+ case BVMinus(lhs, rhs) => buildBinOp(lhs, "-", rhs)
+ case BVUMinus(rhs) => buildUnOp ( "-", rhs)
+ case BVTimes(lhs, rhs) => buildBinOp(lhs, "*", rhs)
+ case BVDivision(lhs, rhs) => buildBinOp(lhs, "/", rhs)
+ case BVRemainder(lhs, rhs) => buildBinOp(lhs, "%", rhs)
+ case BVNot(rhs) => buildUnOp ( "~", rhs)
+ case BVAnd(lhs, rhs) => buildBinOp(lhs, "&", rhs)
+ case BVOr(lhs, rhs) => buildBinOp(lhs, "|", rhs)
+ case BVXOr(lhs, rhs) => buildBinOp(lhs, "^", rhs)
+ case BVShiftLeft(lhs, rhs) => buildBinOp(lhs, "<<", rhs)
+ case BVAShiftRight(lhs, rhs) => buildBinOp(lhs, ">>", rhs)
+ case BVLShiftRight(lhs, rhs) => fatalError("operator >>> not supported")
+
+ // Ignore assertions for now
+ case Ensuring(body, _) => convert(body)
+ case Require(_, body) => convert(body)
+ case Assert(_, _, body) => convert(body)
+
+ case IfExpr(cond1, thn1, elze1) =>
+ val condF = convertAndFlatten(cond1)
+ val thn = convertToStmt(thn1)
+ val elze = convertToStmt(elze1)
+
+ condF.body ~~ buildIfElse(condF.value, thn, elze)
+
+ case While(cond1, body1) =>
+ val cond = convertToStmt(cond1)
+ val body = convertToStmt(body1)
+
+ if (cond.isPureValue) {
+ CAST.While(cond, body)
+ } else {
+ // Transform while (cond) { body } into
+ // while (true) { if (cond) { body } else { break } }
+ val condF = flatten(cond)
+ val ifelse = condF.body ~~ buildIfElse(condF.value, CAST.NoStmt, CAST.Break)
+ CAST.While(CAST.True, ifelse ~ body)
+ }
+
+ case FunctionInvocation(tfd @ TypedFunDef(fd, _), stdArgs) =>
+ // In addition to regular function parameters, add the callee's extra parameters
+ val id = convertToId(fd.id)
+ val types = tfd.params map { p => convertToType(p.getType) }
+ val fs = convertAndNormaliseExecution(stdArgs, types)
+ val extraArgs = funCtx.toArgs(getFunExtraArgs(id))
+ val args = extraArgs ++ fs.values
+
+ fs.bodies ~~ CAST.Call(id, args)
+
+ case unsupported =>
+ fatalError(s"$unsupported (of type ${unsupported.getClass}) is currently not supported by GenC")
+ }
+
+ private def buildVar(id: Identifier, typ: TypeTree)(implicit funCtx: FunCtx) =
+ CAST.Var(convertToId(id), convertToType(typ))
+
+ private def buildVal(id: Identifier, typ: TypeTree)(implicit funCtx: FunCtx) =
+ CAST.Val(convertToId(id), convertToType(typ))
+
+ private def buildAccessVar(id1: Identifier)(implicit funCtx: FunCtx) = {
+ // Depending on the context, we have to deference the variable
+ val id = convertToId(id1)
+ if (funCtx.hasOuterVar(id)) CAST.AccessRef(id)
+ else CAST.AccessVar(id)
+ }
+
+ private def buildLet(id: Identifier, value: Expr, rest1: Expr, forceVar: Boolean)
+ (implicit funCtx: FunCtx): CAST.Stmt = {
+ val (x, stmt) = buildDeclInitVar(id, value, forceVar)
+
+ // Augment ctx for the following instructions
+ val funCtx2 = funCtx.extend(x)
+ val rest = convertToStmt(rest1)(funCtx2)
+
+ stmt ~ rest
+ }
+
+
+ // Create a new variable for the given value, potentially immutable, and initialize it
+ private def buildDeclInitVar(id: Identifier, v: Expr, forceVar: Boolean)
+ (implicit funCtx: FunCtx): (CAST.Var, CAST.Stmt) = {
+ val valueF = convertAndFlatten(v)
+ val typ = v.getType
+
+ valueF.value match {
+ case CAST.IfElse(cond, thn, elze) =>
+ val x = buildVar(id, typ)
+ val decl = CAST.DeclVar(x)
+ val ifelse = buildIfElse(cond, injectAssign(x, thn), injectAssign(x, elze))
+ val init = decl ~ ifelse
+
+ (x, valueF.body ~~ init)
+
+ case value =>
+ val x = if (forceVar) buildVar(id, typ) else buildVal(id, typ)
+ val init = CAST.DeclInitVar(x, value)
+
+ (x, valueF.body ~~ init)
+ }
+ }
+
+ private def buildBinOp(lhs: Expr, op: String, rhs: Expr)(implicit funCtx: FunCtx) = {
+ buildMultiOp(op, lhs :: rhs :: Nil)
+ }
+
+ private def buildUnOp(op: String, rhs1: Expr)(implicit funCtx: FunCtx) = {
+ val rhsF = convertAndFlatten(rhs1)
+ rhsF.body ~~ CAST.Op(op, rhsF.value)
+ }
+
+ private def buildMultiOp(op: String, exprs: Seq[Expr])(implicit funCtx: FunCtx): CAST.Stmt = {
+ require(exprs.length >= 2)
+
+ val stmts = exprs map convertToStmt
+ val types = exprs map { e => convertToType(e.getType) }
+
+ buildMultiOp(op, stmts, types)
+ }
+
+ private def buildMultiOp(op: String, stmts: Seq[CAST.Stmt], types: Seq[CAST.Type]): CAST.Stmt = {
+ // Default operator constuction when either pure statements are involved
+ // or no shortcut can happen
+ def defaultBuild = {
+ val fs = normaliseExecution(stmts, types)
+ fs.bodies ~~ CAST.Op(op, fs.values)
+ }
+
+ if (stmts forall { _.isPureValue }) defaultBuild
+ else op match {
+ case "&&" =>
+ // Apply short-circuit if needed
+ if (stmts.length == 2) {
+ // Base case:
+ // { { a; v } && { b; w } }
+ // is mapped onto
+ // { a; if (v) { b; w } else { false } }
+ val av = flatten(stmts(0))
+ val bw = stmts(1)
+
+ if (bw.isPureValue) defaultBuild
+ else av.body ~~ buildIfElse(av.value, bw, CAST.False)
+ } else {
+ // Recursive case:
+ // { { a; v } && ... }
+ // is mapped onto
+ // { a; if (v) { ... } else { false } }
+ val av = flatten(stmts(0))
+ val rest = buildMultiOp(op, stmts.tail, types.tail)
+
+ if (rest.isPureValue) defaultBuild
+ else av.body ~~ buildIfElse(av.value, rest, CAST.False)
+ }
+
+ case "||" =>
+ // Apply short-circuit if needed
+ if (stmts.length == 2) {
+ // Base case:
+ // { { a; v } || { b; w } }
+ // is mapped onto
+ // { a; if (v) { true } else { b; w } }
+ val av = flatten(stmts(0))
+ val bw = stmts(1)
+
+ if (bw.isPureValue) defaultBuild
+ else av.body ~~ buildIfElse(av.value, CAST.True, bw)
+ } else {
+ // Recusrive case:
+ // { { a; v } || ... }
+ // is mapped onto
+ // { a; if (v) { true } else { ... } }
+ val av = flatten(stmts(0))
+ val rest = buildMultiOp(op, stmts.tail, types.tail)
+
+ if (rest.isPureValue) defaultBuild
+ else av.body ~~ buildIfElse(av.value, CAST.True, rest)
+ }
+
+ case _ =>
+ defaultBuild
+ }
+ }
+
+ // Flatten `if (if (cond1) thn1 else elze1) thn2 else elze2`
+ // into `if (cond1) { if (thn1) thn2 else elz2 } else { if (elz1) thn2 else elze2 }`
+ // or, if possible, into `if ((cond1 && thn1) || elz1) thn2 else elz2`
+ //
+ // Flatten `if (true) thn else elze` into `thn`
+ // Flatten `if (false) thn else elze` into `elze`
+ private def buildIfElse(cond: CAST.Stmt, thn2: CAST.Stmt, elze2: CAST.Stmt): CAST.Stmt = {
+ val condF = flatten(cond)
+
+ val ifelse = condF.value match {
+ case CAST.IfElse(cond1, thn1, elze1) =>
+ if (cond1.isPure && thn1.isPure && elze1.isPure) {
+ val bools = CAST.Bool :: CAST.Bool :: Nil
+ val ands = cond1 :: thn1 :: Nil
+ val ors = buildMultiOp("&&", ands, bools) :: elze1 :: Nil
+ val condX = buildMultiOp("||", ors, bools)
+ CAST.IfElse(condX, thn2, elze2)
+ } else {
+ buildIfElse(cond1, buildIfElse(thn1, thn2, elze2), buildIfElse(elze1, thn2, elze2))
+ }
+
+ case CAST.True => thn2
+ case CAST.False => elze2
+ case cond2 => CAST.IfElse(cond2, thn2, elze2)
+ }
+
+ condF.body ~~ ifelse
+ }
+
+ private def injectReturn(stmt: CAST.Stmt): CAST.Stmt = {
+ val f = flatten(stmt)
+
+ f.value match {
+ case CAST.IfElse(cond, thn, elze) =>
+ f.body ~~ CAST.IfElse(cond, injectReturn(thn), injectReturn(elze))
+
+ case _ =>
+ f.body ~~ CAST.Return(f.value)
+ }
+ }
+
+ private def injectAssign(x: CAST.Var, stmt: CAST.Stmt): CAST.Stmt = {
+ injectAssign(CAST.AccessVar(x.id), stmt)
+ }
+
+ private def injectAssign(x: CAST.Stmt, stmt: CAST.Stmt): CAST.Stmt = {
+ val f = flatten(stmt)
+
+ f.value match {
+ case CAST.IfElse(cond, thn, elze) =>
+ f.body ~~ CAST.IfElse(cond, injectAssign(x, thn), injectAssign(x, elze))
+
+ case _ =>
+ f.body ~~ CAST.Assign(x, f.value)
+ }
+ }
+
+ // Flattened represents a non-empty statement { a; b; ...; y; z }
+ // split into body { a; b; ...; y } and value z
+ private case class Flattened(value: CAST.Stmt, body: Seq[CAST.Stmt])
+
+ // FlattenedSeq does the same as Flattened for a sequence of non-empty statements
+ private case class FlattenedSeq(values: Seq[CAST.Stmt], bodies: Seq[CAST.Stmt])
+
+ private def flatten(stmt: CAST.Stmt) = stmt match {
+ case CAST.Compound(stmts) if stmts.isEmpty => internalError(s"Empty compound cannot be flattened")
+ case CAST.Compound(stmts) => Flattened(stmts.last, stmts.init)
+ case stmt => Flattened(stmt, Seq())
+ }
+
+ private def convertAndFlatten(expr: Expr)(implicit funCtx: FunCtx) = flatten(convertToStmt(expr))
+
+ // Normalise execution order of, for example, function parameters;
+ // `types` represents the expected type of the corresponding values
+ // in case an intermediary variable needs to be created
+ private def convertAndNormaliseExecution(exprs: Seq[Expr], types: Seq[CAST.Type])
+ (implicit funCtx: FunCtx) = {
+ require(exprs.length == types.length)
+ normaliseExecution(exprs map convertToStmt, types)
+ }
+
+ private def normaliseExecution(typedStmts: Seq[(CAST.Stmt, CAST.Type)]): FlattenedSeq =
+ normaliseExecution(typedStmts map { _._1 }, typedStmts map { _._2 })
+
+ private def normaliseExecution(stmts: Seq[CAST.Stmt], types: Seq[CAST.Type]): FlattenedSeq = {
+ require(stmts.length == types.length)
+
+ // Create temporary variables if needed
+ val stmtsFs = stmts map flatten
+ val fs = (stmtsFs zip types) map {
+ case (f, _) if f.value.isPureValue => f
+
+ case (f, typ) =>
+ // Similarly to buildDeclInitVar:
+ val (tmp, body) = f.value match {
+ case CAST.IfElse(cond, thn, elze) =>
+ val tmp = CAST.FreshVar(typ.mutable, "normexec")
+ val decl = CAST.DeclVar(tmp)
+ val ifelse = buildIfElse(cond, injectAssign(tmp, thn), injectAssign(tmp, elze))
+ val body = f.body ~~ decl ~ ifelse
+
+ (tmp, body)
+
+ case value =>
+ val tmp = CAST.FreshVal(typ, "normexec")
+ val body = f.body ~~ CAST.DeclInitVar(tmp, f.value)
+
+ (tmp, body)
+ }
+
+ val value = CAST.AccessVar(tmp.id)
+ flatten(body ~ value)
+ }
+
+ val empty = Seq[CAST.Stmt]()
+ val bodies = fs.foldLeft(empty){ _ ++ _.body }
+ val values = fs map { _.value }
+
+ FlattenedSeq(values, bodies)
+ }
+
+ private def containsArrayType(typ: TypeTree): Boolean = typ match {
+ case Int32Type => false
+ case BooleanType => false
+ case UnitType => false
+ case ArrayType(_) => true
+ case TupleType(bases) => bases exists containsArrayType
+ case CaseClassType(cd, _) => cd.fields map { _.getType } exists containsArrayType
+ }
+
+ private def internalError(msg: String) = ctx.reporter.internalError(msg)
+ private def fatalError(msg: String) = ctx.reporter.fatalError(msg)
+ private def debug(msg: String) = ctx.reporter.debug(msg)(utils.DebugSectionGenC)
+
+}
+
diff --git a/src/main/scala/leon/genc/CFileOutputPhase.scala b/src/main/scala/leon/genc/CFileOutputPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f2b7797183da17ccb6e326a85a779a4ef58be9e2
--- /dev/null
+++ b/src/main/scala/leon/genc/CFileOutputPhase.scala
@@ -0,0 +1,54 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package genc
+
+import java.io.File
+import java.io.FileWriter
+import java.io.BufferedWriter
+
+object CFileOutputPhase extends UnitPhase[CAST.Prog] {
+
+ val name = "C File Output"
+ val description = "Output converted C program to the specified file (default leon.c)"
+
+ val optOutputFile = new LeonOptionDef[String] {
+ val name = "o"
+ val description = "Output file"
+ val default = "leon.c"
+ val usageRhs = "file"
+ val parser = OptionParsers.stringParser
+ }
+
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(optOutputFile)
+
+ def apply(ctx: LeonContext, program: CAST.Prog) {
+ // Get the output file name from command line options, or use default
+ val outputFile = new File(ctx.findOptionOrDefault(optOutputFile))
+ val parent = outputFile.getParentFile()
+ try {
+ if (parent != null) {
+ parent.mkdirs()
+ }
+ } catch {
+ case _ : java.io.IOException => ctx.reporter.fatalError("Could not create directory " + parent)
+ }
+
+ // Output C code to the file
+ try {
+ val fstream = new FileWriter(outputFile)
+ val out = new BufferedWriter(fstream)
+
+ val p = new CPrinter
+ p.print(program)
+
+ out.write(p.toString)
+ out.close()
+
+ ctx.reporter.info(s"Output written to $outputFile")
+ } catch {
+ case _ : java.io.IOException => ctx.reporter.fatalError("Could not write on " + outputFile)
+ }
+ }
+
+}
diff --git a/src/main/scala/leon/genc/CPrinter.scala b/src/main/scala/leon/genc/CPrinter.scala
new file mode 100644
index 0000000000000000000000000000000000000000..eec404f0c5283bbf09e56dbe79e8335286f61ae6
--- /dev/null
+++ b/src/main/scala/leon/genc/CPrinter.scala
@@ -0,0 +1,198 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package genc
+
+import CAST._
+import CPrinterHelpers._
+
+class CPrinter(val sb: StringBuffer = new StringBuffer) {
+ override def toString = sb.toString
+
+ def print(tree: Tree) = pp(tree)(PrinterContext(0, this))
+
+ def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = tree match {
+ /* ---------------------------------------------------------- Types ----- */
+ case typ: Type => c"${typ.toString}"
+
+
+ /* ------------------------------------------------------- Literals ----- */
+ case IntLiteral(v) => c"$v"
+ case BoolLiteral(b) => c"$b"
+
+
+ /* --------------------------------------------------- Definitions ----- */
+ case Prog(structs, functions) =>
+ c"""|/* ------------------------------------ includes ----- */
+ |
+ |${nary(includeStmts, sep = "\n")}
+ |
+ |/* ---------------------- data type declarations ----- */
+ |
+ |${nary(structs map StructDecl, sep = "\n")}
+ |
+ |/* ----------------------- data type definitions ----- */
+ |
+ |${nary(structs map StructDef, sep = "\n")}
+ |
+ |/* ----------------------- function declarations ----- */
+ |
+ |${nary(functions map FunDecl, sep = "\n")}
+ |
+ |/* ------------------------ function definitions ----- */
+ |
+ |${nary(functions, sep = "\n")}
+ |"""
+
+ case f @ Fun(_, _, _, body) =>
+ c"""|${FunSign(f)}
+ |{
+ | $body
+ |}
+ |"""
+
+ case Id(name) => c"$name"
+
+
+ /* --------------------------------------------------------- Stmts ----- */
+ case NoStmt => c"/* empty */"
+
+ case Compound(stmts) =>
+ val lastIdx = stmts.length - 1
+
+ for ((stmt, idx) <- stmts.zipWithIndex) {
+ if (stmt.isValue) c"$stmt;"
+ else c"$stmt"
+
+ if (idx != lastIdx)
+ c"$NewLine"
+ }
+
+ case Assert(pred, Some(error)) => c"assert($pred); /* $error */"
+ case Assert(pred, None) => c"assert($pred);"
+
+ case Var(id, _) => c"$id"
+ case DeclVar(Var(id, typ)) => c"$typ $id;"
+
+ // If the length is a literal we don't need VLA
+ case DeclInitVar(Var(id, typ), ai @ ArrayInit(IntLiteral(length), _, _)) =>
+ val buffer = FreshId("buffer")
+ val values = for (i <- 0 until length) yield ai.defaultValue
+ c"""|${ai.valueType} $buffer[${ai.length}] = { $values };
+ |$typ $id = { .length = ${ai.length}, .data = $buffer };
+ |"""
+
+ // TODO depending on the type of array (e.g. `char`) or the value (e.g. `0`), we could use `memset`.
+ case DeclInitVar(Var(id, typ), ai: ArrayInit) => // Note that `typ` is a struct here
+ val buffer = FreshId("vla_buffer")
+ val i = FreshId("i")
+ c"""|${ai.valueType} $buffer[${ai.length}];
+ |for (${Int32} $i = 0; $i < ${ai.length}; ++$i) {
+ | $buffer[$i] = ${ai.defaultValue};
+ |}
+ |$typ $id = { .length = ${ai.length}, .data = $buffer };
+ |"""
+
+ case DeclInitVar(Var(id, typ), ai: ArrayInitWithValues) => // Note that `typ` is a struct here
+ val buffer = FreshId("buffer")
+ c"""|${ai.valueType} $buffer[${ai.length}] = { ${ai.values} };
+ |$typ $id = { .length = ${ai.length}, .data = $buffer };
+ |"""
+
+ case DeclInitVar(Var(id, typ), value) =>
+ c"$typ $id = $value;"
+
+ case Assign(lhs, rhs) =>
+ c"$lhs = $rhs;"
+
+ case UnOp(op, rhs) => c"($op$rhs)"
+ case MultiOp(op, stmts) => c"""${nary(stmts, sep = s" ${op.fixMargin} ",
+ opening = "(", closing = ")")}"""
+ case SubscriptOp(ptr, idx) => c"$ptr[$idx]"
+
+ case Break => c"break;"
+ case Return(stmt) => c"return $stmt;"
+
+ case IfElse(cond, thn, elze) =>
+ c"""|if ($cond)
+ |{
+ | $thn
+ |}
+ |else
+ |{
+ | $elze
+ |}
+ |"""
+
+ case While(cond, body) =>
+ c"""|while ($cond)
+ |{
+ | $body
+ |}
+ |"""
+
+ case AccessVar(id) => c"$id"
+ case AccessRef(id) => c"(*$id)"
+ case AccessAddr(id) => c"(&$id)"
+ case AccessField(struct, field) => c"$struct.$field"
+ case Call(id, args) => c"$id($args)"
+
+ case StructInit(args, struct) =>
+ c"(${struct.id}) { "
+ for ((id, stmt) <- args.init) {
+ c".$id = $stmt, "
+ }
+ if (!args.isEmpty) {
+ val (id, stmt) = args.last
+ c".$id = $stmt "
+ }
+ c"}"
+
+ /* --------------------------------------------------------- Error ----- */
+ case tree => sys.error(s"CPrinter: <<$tree>> was not handled properly")
+ }
+
+
+ def pp(wt: WrapperTree)(implicit ctx: PrinterContext): Unit = wt match {
+ case FunDecl(f) =>
+ c"${FunSign(f)};$NewLine"
+
+ case FunSign(Fun(id, retType, Nil, _)) =>
+ c"""|$retType
+ |$id($Void)"""
+
+ case FunSign(Fun(id, retType, params, _)) =>
+ c"""|$retType
+ |$id(${nary(params map DeclParam)})"""
+
+ case DeclParam(Var(id, typ)) =>
+ c"$typ $id"
+
+ case StructDecl(s) =>
+ c"struct $s;"
+
+ case StructDef(Struct(name, fields)) =>
+ c"""|typedef struct $name {
+ | ${nary(fields map DeclParam, sep = ";\n", closing = ";")}
+ |} $name;
+ |"""
+
+ case NewLine =>
+ c"""|
+ |"""
+ }
+
+ /** Hardcoded list of required include files from C standard library **/
+ lazy val includes = "assert.h" :: "stdbool.h" :: "stdint.h" :: Nil
+ lazy val includeStmts = includes map { i => s"#include <$i>" }
+
+ /** Wrappers to distinguish how the data should be printed **/
+ sealed abstract class WrapperTree
+ case class FunDecl(f: Fun) extends WrapperTree
+ case class FunSign(f: Fun) extends WrapperTree
+ case class DeclParam(x: Var) extends WrapperTree
+ case class StructDecl(s: Struct) extends WrapperTree
+ case class StructDef(s: Struct) extends WrapperTree
+ case object NewLine extends WrapperTree
+}
+
diff --git a/src/main/scala/leon/genc/CPrinterHelper.scala b/src/main/scala/leon/genc/CPrinterHelper.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5c32df8b7289b0ca5510d04680ab449e915a12dd
--- /dev/null
+++ b/src/main/scala/leon/genc/CPrinterHelper.scala
@@ -0,0 +1,86 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package genc
+
+import CAST.Tree
+
+/* Printer helpers adapted to C code generation */
+
+case class PrinterContext(
+ indent: Int,
+ printer: CPrinter
+)
+
+object CPrinterHelpers {
+ implicit class Printable(val f: PrinterContext => Any) extends AnyVal {
+ def print(ctx: PrinterContext) = f(ctx)
+ }
+
+ implicit class PrinterHelper(val sc: StringContext) extends AnyVal {
+ def c(args: Any*)(implicit ctx: PrinterContext): Unit = {
+ val printer = ctx.printer
+ import printer.WrapperTree
+ val sb = printer.sb
+
+ val strings = sc.parts.iterator
+ val expressions = args.iterator
+
+ var extraInd = 0
+ var firstElem = true
+
+ while(strings.hasNext) {
+ val s = strings.next.stripMargin
+
+ // Compute indentation
+ val start = s.lastIndexOf('\n')
+ if(start >= 0 || firstElem) {
+ var i = start + 1
+ while(i < s.length && s(i) == ' ') {
+ i += 1
+ }
+ extraInd = (i - start - 1) / 2
+ }
+
+ firstElem = false
+
+ // Make sure new lines are also indented
+ sb.append(s.replaceAll("\n", "\n" + (" " * ctx.indent)))
+
+ val nctx = ctx.copy(indent = ctx.indent + extraInd)
+
+ if (expressions.hasNext) {
+ val e = expressions.next
+
+ e match {
+ case ts: Seq[Any] =>
+ nary(ts).print(nctx)
+
+ case t: Tree =>
+ printer.pp(t)(nctx)
+
+ case wt: WrapperTree =>
+ printer.pp(wt)(nctx)
+
+ case p: Printable =>
+ p.print(nctx)
+
+ case e =>
+ sb.append(e.toString)
+ }
+ }
+ }
+ }
+ }
+
+ def nary(ls: Seq[Any], sep: String = ", ", opening: String = "", closing: String = ""): Printable = {
+ val (o, c) = if(ls.isEmpty) ("", "") else (opening, closing)
+ val strs = o +: List.fill(ls.size-1)(sep) :+ c
+
+ implicit pctx: PrinterContext =>
+ new StringContext(strs: _*).c(ls: _*)
+ }
+
+}
+
+
diff --git a/src/main/scala/leon/genc/GenerateCPhase.scala b/src/main/scala/leon/genc/GenerateCPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c30d32274db7370a8f9af5616df3cbe505b0389e
--- /dev/null
+++ b/src/main/scala/leon/genc/GenerateCPhase.scala
@@ -0,0 +1,20 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package genc
+
+import purescala.Definitions.Program
+
+object GenerateCPhase extends SimpleLeonPhase[Program, CAST.Prog] {
+
+ val name = "Generate C"
+ val description = "Generate equivalent C code from Leon's AST"
+
+ def apply(ctx: LeonContext, program: Program) = {
+ ctx.reporter.debug("Running code conversion phase: " + name)(utils.DebugSectionLeon)
+ val cprogram = new CConverter(ctx, program).convert
+ cprogram
+ }
+
+}
+
diff --git a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
index 3fe13e7c93fefdfcc4321159b0fa7b354788a801..d2deb1ced97b635a1459f8e0e7b531588989cf64 100644
--- a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
@@ -42,7 +42,7 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F
def constructVC(funDef: FunDef): (Expr, Expr) = {
val body = funDef.body.get
- val Lambda(Seq(ValDef(resid, _)), _) = funDef.postcondition.get
+ val Lambda(Seq(ValDef(resid)), _) = funDef.postcondition.get
val resvar = resid.toVariable
val simpBody = matchToIfThenElse(body)
diff --git a/src/main/scala/leon/invariant/util/TreeUtil.scala b/src/main/scala/leon/invariant/util/TreeUtil.scala
index 4109e59877c192570e95bb83b819ebd0a59edef7..26398130a447c3eb503e2fe0e72b4cf75a711236 100644
--- a/src/main/scala/leon/invariant/util/TreeUtil.scala
+++ b/src/main/scala/leon/invariant/util/TreeUtil.scala
@@ -182,7 +182,7 @@ object ProgramUtil {
funDef.fullBody match {
case Ensuring(_, post) => {
post match {
- case Lambda(Seq(ValDef(fromRes, _)), _) => Some(fromRes)
+ case Lambda(Seq(ValDef(fromRes)), _) => Some(fromRes)
}
}
case _ => None
diff --git a/src/main/scala/leon/purescala/CallGraph.scala b/src/main/scala/leon/purescala/CallGraph.scala
index a07b807ddaad26817322878c46d575f0a4ec1306..edeaab26953ef6734b2a334e440e04dfb59d38c5 100644
--- a/src/main/scala/leon/purescala/CallGraph.scala
+++ b/src/main/scala/leon/purescala/CallGraph.scala
@@ -7,106 +7,77 @@ import Definitions._
import Expressions._
import ExprOps._
-class CallGraph(p: Program) {
+import utils.Graphs._
- private var _calls = Set[(FunDef, FunDef)]()
+class CallGraph(p: Program) {
- private var _callers = Map[FunDef, Set[FunDef]]() // if 'foo' calls 'bar': Map(bar -> Set(foo))
- private var _callees = Map[FunDef, Set[FunDef]]() // if 'foo' calls 'bar': Map(foo -> Set(bar))
+ private def collectCallsInPats(fd: FunDef)(p: Pattern): Set[(FunDef, FunDef)] =
+ (p match {
+ case u: UnapplyPattern => Set((fd, u.unapplyFun.fd))
+ case _ => Set()
+ }) ++ p.subPatterns.flatMap(collectCallsInPats(fd))
- private var _transitiveCalls = Set[(FunDef, FunDef)]()
- private var _transitiveCallers = Map[FunDef, Set[FunDef]]()
- private var _transitiveCallees = Map[FunDef, Set[FunDef]]()
+ private def collectCalls(fd: FunDef)(e: Expr): Set[(FunDef, FunDef)] = e match {
+ case f @ FunctionInvocation(f2, _) => Set((fd, f2.fd))
+ case MatchExpr(_, cases) => cases.toSet.flatMap((mc: MatchCase) => collectCallsInPats(fd)(mc.pattern))
+ case _ => Set()
+ }
- def allCalls = _calls
- def allTransitiveCalls = _transitiveCalls
+ lazy val graph: DiGraph[FunDef, SimpleEdge[FunDef]] = {
+ var g = DiGraph[FunDef, SimpleEdge[FunDef]]()
- def isRecursive(f: FunDef) = transitivelyCalls(f, f)
+ for (fd <- p.definedFunctions; c <- collect(collectCalls(fd))(fd.fullBody)) {
+ g += SimpleEdge(c._1, c._2)
+ }
- def calls(from: FunDef, to: FunDef) = _calls contains (from -> to)
- def callers(to: FunDef) = _callers.getOrElse(to, Set())
- def callees(from: FunDef) = _callees.getOrElse(from, Set())
+ g
+ }
- def transitivelyCalls(from: FunDef, to: FunDef) = _transitiveCalls contains (from -> to)
- def transitiveCallers(to: FunDef) = _transitiveCallers.getOrElse(to, Set())
- def transitiveCallees(from: FunDef) = _transitiveCallees.getOrElse(from, Set())
+ lazy val allCalls = graph.E.map(e => e._1 -> e._2)
- // multi-source/dest
- def callees(from: Set[FunDef]): Set[FunDef] = from.flatMap(callees)
- def callers(to: Set[FunDef]): Set[FunDef] = to.flatMap(callers)
- def transitiveCallees(from: Set[FunDef]): Set[FunDef] = from.flatMap(transitiveCallees)
- def transitiveCallers(to: Set[FunDef]): Set[FunDef] = to.flatMap(transitiveCallers)
+ def isRecursive(f: FunDef) = {
+ graph.transitiveSucc(f) contains f
+ }
- lazy val stronglyConnectedComponents: Seq[Set[FunDef]] = {
- def rec(funs: Set[FunDef]): Seq[Set[FunDef]] = {
- if (funs.isEmpty) Seq()
- else {
- val h = funs.head
- val component = transitiveCallees(h).filter{ transitivelyCalls(_, h) } + h
- component +: rec(funs -- component)
- }
- }
- rec(p.definedFunctions.toSet)
+ def calls(from: FunDef, to: FunDef) = {
+ graph.E contains SimpleEdge(from, to)
}
-
- def stronglyConnectedComponent(fd: FunDef) =
- stronglyConnectedComponents.find{ _.contains(fd) }.getOrElse(Set(fd))
- private def init() {
- _calls = Set()
- _callers = Map()
- _callees = Map()
+ def callers(to: FunDef): Set[FunDef] = {
+ graph.pred(to)
+ }
+ def callers(tos: Set[FunDef]): Set[FunDef] = {
+ tos.flatMap(callers)
+ }
- // Collect all calls
- p.definedFunctions.foreach(scanForCalls)
+ def callees(from: FunDef): Set[FunDef] = {
+ graph.succ(from)
+ }
- _transitiveCalls = _calls
- _transitiveCallers = _callers
- _transitiveCallees = _callees
+ def callees(froms: Set[FunDef]): Set[FunDef] = {
+ froms.flatMap(callees)
+ }
- // Transitive calls
- transitiveClosure()
+ def transitiveCallers(to: FunDef): Set[FunDef] = {
+ graph.transitivePred(to)
}
- private def collectCallsInPats(fd: FunDef)(p: Pattern): Set[(FunDef, FunDef)] =
- (p match {
- case u: UnapplyPattern => Set((fd, u.unapplyFun.fd))
- case _ => Set()
- }) ++ p.subPatterns.flatMap(collectCallsInPats(fd))
+ def transitiveCallers(tos: Set[FunDef]): Set[FunDef] = {
+ tos.flatMap(transitiveCallers)
+ }
- private def collectCalls(fd: FunDef)(e: Expr): Set[(FunDef, FunDef)] = e match {
- case f @ FunctionInvocation(f2, _) => Set((fd, f2.fd))
- case MatchExpr(_, cases) => cases.toSet.flatMap((mc: MatchCase) => collectCallsInPats(fd)(mc.pattern))
- case _ => Set()
+ def transitiveCallees(from: FunDef): Set[FunDef] = {
+ graph.transitiveSucc(from)
}
- private def scanForCalls(fd: FunDef) {
- for( (from, to) <- collect(collectCalls(fd))(fd.fullBody) ) {
- _calls += (from -> to)
- _callees += (from -> (_callees.getOrElse(from, Set()) + to))
- _callers += (to -> (_callers.getOrElse(to, Set()) + from))
- }
+ def transitiveCallees(froms: Set[FunDef]): Set[FunDef] = {
+ froms.flatMap(transitiveCallees)
}
- private def transitiveClosure() {
- var changed = true
- while(changed) {
- val newCalls = _transitiveCalls.flatMap {
- case (from, to) => _transitiveCallees.getOrElse(to, Set()).map((from, _))
- } -- _transitiveCalls
-
- if (newCalls.nonEmpty) {
- for ((from, to) <- newCalls) {
- _transitiveCalls += (from -> to)
- _transitiveCallees += (from -> (_transitiveCallees.getOrElse(from, Set()) + to))
- _transitiveCallers += (to -> (_transitiveCallers.getOrElse(to, Set()) + from))
- }
- } else {
- changed =false
- }
- }
+ def transitivelyCalls(from: FunDef, to: FunDef): Boolean = {
+ graph.transitiveSucc(from) contains to
}
- init()
+ lazy val stronglyConnectedComponents = graph.stronglyConnectedComponents.N
}
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index bae200bbe05fa4a2a43b9cae36e0088be3f129e5..23b32e0ee96ec98dca890a4a17ae8541c20244cb 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -41,6 +41,17 @@ object Constructors {
*/
def tupleSelect(t: Expr, index: Int, originalSize: Int): Expr = tupleSelect(t, index, originalSize > 1)
+ /** $encodingof ``def foo(..) {} ...; e``.
+ * @see [[purescala.Expressions.LetDef]]
+ */
+ def letDef(defs: Seq[FunDef], e: Expr) = {
+ if (defs.isEmpty) {
+ e
+ } else {
+ LetDef(defs, e)
+ }
+ }
+
/** $encodingof ``val id = e; bd``, and returns `bd` if the identifier is not bound in `bd`.
* @see [[purescala.Expressions.Let]]
*/
@@ -323,9 +334,9 @@ object Constructors {
var defs: Seq[(Identifier, Expr)] = Seq()
val subst = formalArgs.zip(realArgs).map {
- case (ValDef(from, _), to:Variable) =>
+ case (ValDef(from), to:Variable) =>
from -> to
- case (ValDef(from, _), e) =>
+ case (ValDef(from), e) =>
val fresh = from.freshen
defs :+= (fresh -> e)
from -> Variable(fresh)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 792e43c56923a73ad3f4a8f42551dd34e6fa7989..8fb753d23d35364059115f7032bef3310c492d82 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -45,7 +45,7 @@ object Definitions {
* The optional tpe, if present, overrides the type of the underlying Identifier id
* This is useful to instantiate argument types of polymorphic functions
*/
- case class ValDef(id: Identifier, isLazy: Boolean = false) extends Definition with Typed {
+ case class ValDef(id: Identifier) extends Definition with Typed {
self: Serializable =>
val getType = id.getType
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index d15c78c951fe3f3990c16ee51422dc53b8223806..5ce8a11ec204c4fde241797dd2706d1a5be20dc0 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1148,6 +1148,15 @@ object ExprOps {
case _ => throw LeonFatalError("I can't choose simplest value for type " + tpe)
}
+ /* Checks if a given expression is 'real' and does not contain generic
+ * values. */
+ def isRealExpr(v: Expr): Boolean = {
+ !exists {
+ case gv: GenericValue => true
+ case _ => false
+ }(v)
+ }
+
def valuesOf(tp: TypeTree): Stream[Expr] = {
import utils.StreamUtils._
tp match {
@@ -1688,7 +1697,7 @@ object ExprOps {
case (Lambda(defs, body), Lambda(defs2, body2)) =>
// We remove variables introduced by lambdas.
(isHomo(body, body2) &&
- (defs zip defs2).mergeall{ case (ValDef(a1, _), ValDef(a2, _)) => Option(Map(a1 -> a2)) }
+ (defs zip defs2).mergeall{ case (ValDef(a1), ValDef(a2)) => Option(Map(a1 -> a2)) }
) -- (defs.map(_.id))
case (v1, v2) if isValue(v1) && isValue(v2) =>
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 13e4efbef15d754765776de6153c9f5a8b65c6c8..bb70a6676923db89648df770318f8c04129bad3e 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -165,6 +165,7 @@ object Expressions {
* @param body The body of the expression after the function
*/
case class LetDef(fds: Seq[FunDef], body: Expr) extends Expr {
+ assert(fds.nonEmpty)
val getType = body.getType
}
@@ -725,11 +726,11 @@ object Expressions {
case class BVShiftLeft(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
- /** $encodingof `... >>> ...` $noteBitvector (logical shift) */
+ /** $encodingof `... >> ...` $noteBitvector (arithmetic shift, sign-preserving) */
case class BVAShiftRight(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
- /** $encodingof `... >> ...` $noteBitvector (arithmetic shift, sign-preserving) */
+ /** $encodingof `... >>> ...` $noteBitvector (logical shift) */
case class BVLShiftRight(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 7bebde2f800965d26eae30befc00f92512cf72e0..039bef507339294874ad59e7e38dfe335b8f6a2f 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -11,6 +11,7 @@ import Extractors._
import PrinterHelpers._
import ExprOps.{isListLiteral, simplestValue}
import Expressions._
+import Constructors._
import Types._
import org.apache.commons.lang3.StringEscapeUtils
@@ -92,7 +93,7 @@ class PrettyPrinter(opts: PrinterOptions,
case LetDef(a::q,body) =>
p"""|$a
- |${LetDef(q, body)}"""
+ |${letDef(q, body)}"""
case LetDef(Nil,body) =>
p"""$body"""
@@ -164,6 +165,7 @@ class PrettyPrinter(opts: PrinterOptions,
case Or(exprs) => optP { p"${nary(exprs, "| || ")}" } // Ugliness award! The first | is there to shield from stripMargin()
case Not(Equals(l, r)) => optP { p"$l \u2260 $r" }
case Implies(l,r) => optP { p"$l ==> $r" }
+ case BVNot(expr) => p"~$expr"
case UMinus(expr) => p"-$expr"
case BVUMinus(expr) => p"-$expr"
case RealUMinus(expr) => p"-$expr"
@@ -358,8 +360,8 @@ class PrettyPrinter(opts: PrinterOptions,
case Not(expr) => p"\u00AC$expr"
- case vd @ ValDef(id, lzy) =>
- p"$id :${if (lzy) "=> " else ""} ${vd.getType}"
+ case vd @ ValDef(id) =>
+ p"$id : ${vd.getType}"
vd.defaultValue.foreach { fd => p" = ${fd.body.get}" }
case This(_) => p"this"
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 01e048699ec1654420ba059873dc4299724b842f..f3e7c15886fbce8b4e7c2854f0f83fc2a74e26c7 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -50,10 +50,10 @@ class ScopeSimplifier extends Transformer {
val fds_mapping = for((fd, newId) <- fds_newIds) yield {
val localScopeToRegister = ListBuffer[(Identifier, Identifier)]() // We record the mapping of these variables only for the function.
- val newArgs = for(ValDef(id, tpe) <- fd.params) yield {
+ val newArgs = for(ValDef(id) <- fd.params) yield {
val newArg = genId(id, newScope.register(localScopeToRegister))
localScopeToRegister += (id -> newArg) // This renaming happens only inside the function.
- ValDef(newArg, tpe)
+ ValDef(newArg)
}
val newFd = fd.duplicate(id = newId, params = newArgs)
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 84825d29a8ea2a293f04732fab06b2a88a36a4b8..db655365c24a7304831e818849238bba0a849de9 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -167,6 +167,11 @@ object TypeOps {
}
}
+ def isParametricType(tpe: TypeTree): Boolean = tpe match {
+ case (tp: TypeParameter) => true
+ case NAryType(tps, builder) => tps.exists(isParametricType)
+ }
+
// Helpers for instantiateType
private def typeParamSubst(map: Map[TypeParameter, TypeTree])(tpe: TypeTree): TypeTree = tpe match {
case (tp: TypeParameter) => map.getOrElse(tp, tp)
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 6b2d4272b37b4a06ba2731c5049bcc043b87c927..67d28f877019a3e4741df6d268c68fc2d86d17ee 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -177,7 +177,7 @@ object SolverFactory {
}
lazy val hasZ3 = try {
- Z3Interpreter.buildDefault.free()
+ new Z3Interpreter("z3", Array("-in", "-smt2"))
true
} catch {
case e: java.io.IOException =>
@@ -185,7 +185,7 @@ object SolverFactory {
}
lazy val hasCVC4 = try {
- CVC4Interpreter.buildDefault.free()
+ new CVC4Interpreter("cvc4", Array("-q", "--lang", "smt2.5"))
true
} catch {
case e: java.io.IOException =>
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 1fa660b55bcfc57f980a4e5165d48ead07c42a44..42d6c41ab82fd80e28776b5ce0deeb082212612c 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -34,7 +34,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
def setEvaluationFailOnChoose(b: Boolean) = { evaluator.setEvaluationFailOnChoose(b); this }
def extractFromFunDef(fd: FunDef, partition: Boolean): ExamplesBank = fd.postcondition match {
- case Some(Lambda(Seq(ValDef(id, _)), post)) =>
+ case Some(Lambda(Seq(ValDef(id)), post)) =>
// @mk FIXME: make this more general
val tests = extractTestsOf(post)
diff --git a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
index 375052dc7e5626cf635231d1c7687bba2c35f211..ed9f44768752c716b2acf0f6db9863cde1353068 100644
--- a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
@@ -60,7 +60,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
val inputVariables = tupleWrap(params.map(p => Variable(p.id): Expr))
val newCases = examples.map{ case (in, out) => exampleToCase(in, out) }
fd.postcondition match {
- case Some(Lambda(Seq(ValDef(id, tpe)), post)) =>
+ case Some(Lambda(Seq(ValDef(id)), post)) =>
if(fd.postcondition.exists { e => purescala.ExprOps.exists(_.isInstanceOf[Passes])(e) }) {
post match {
case TopLevelAnds(exprs) =>
@@ -69,7 +69,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
case _ => false
} }
if(i == -1) {
- fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), and(post, Passes(inputVariables, Variable(id), newCases))))
+ fd.postcondition = Some(Lambda(Seq(ValDef(id)), and(post, Passes(inputVariables, Variable(id), newCases))))
//ctx0.reporter.info("No top-level passes in postcondition, adding it: " + fd)
} else {
val newPasses = exprs(i) match {
@@ -78,21 +78,21 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
case _ => ???
}
val newPost = and(exprs.updated(i, newPasses) : _*)
- fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), newPost))
+ fd.postcondition = Some(Lambda(Seq(ValDef(id)), newPost))
//ctx0.reporter.info("Adding the example to the passes postcondition: " + fd)
}
}
} else {
- fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), and(post, Passes(inputVariables, Variable(id), newCases))))
+ fd.postcondition = Some(Lambda(Seq(ValDef(id)), and(post, Passes(inputVariables, Variable(id), newCases))))
//ctx0.reporter.info("No passes in postcondition, adding it:" + fd)
}
case None =>
val id = FreshIdentifier("res", fd.returnType, false)
- fd.postcondition = Some(Lambda(Seq(ValDef(id, false)), Passes(inputVariables, Variable(id), newCases)))
+ fd.postcondition = Some(Lambda(Seq(ValDef(id)), Passes(inputVariables, Variable(id), newCases)))
//ctx0.reporter.info("No postcondition, adding it: " + fd)
}
fd.body match { // TODO: Is it correct to discard the choose construct inside the body?
- case Some(Choose(Lambda(Seq(ValDef(id, tpe)), bodyChoose))) => fd.body = Some(Hole(id.getType, Nil))
+ case Some(Choose(Lambda(Seq(ValDef(id)), bodyChoose))) => fd.body = Some(Hole(id.getType, Nil))
case _ =>
}
}
@@ -106,4 +106,4 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
MatchCase(WildcardPattern(Some(id)), Some(Equals(Variable(id), in)), out)
}
}
- }
\ No newline at end of file
+ }
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 9bba63c87d50b3ca7f1adf7e445a8a0b54172b2f..d2cdb5b69f1f88b847ad91499e3946257ef6c167 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -5,7 +5,9 @@ package synthesis
package rules
import purescala.ExprOps._
+import purescala.TypeOps._
import purescala.Extractors._
+import purescala.Expressions._
import purescala.Constructors._
/** Moves the preconditions without output variables to the precondition. */
@@ -19,7 +21,13 @@ case object Assert extends NormalizingRule("Assert") {
if (exprsA.nonEmpty) {
// If there is no more postcondition, then output the solution.
if (others.isEmpty) {
- Some(solve(Solution(pre=andJoin(exprsA), defs=Set(), term=tupleWrap(p.xs.map(id => simplestValue(id.getType))))))
+ val simplestOut = simplestValue(tupleTypeWrap(p.xs.map(_.getType)))
+
+ if (!isRealExpr(simplestOut)) {
+ None
+ } else {
+ Some(solve(Solution(pre = andJoin(exprsA), defs = Set(), term = simplestOut)))
+ }
} else {
val sub = p.copy(pc = andJoin(p.pc +: exprsA), phi = andJoin(others), eb = p.qeb.filterIns(andJoin(exprsA)))
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 49663409fab1fb22dc102e35cfcfd3fb0ab5cdb4..d36cb15c0ff6f487d5d7b5e296fda0c406406886 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -19,8 +19,14 @@ case object Ground extends Rule("Ground") {
val result = solver.solveSAT(p.phi) match {
case (Some(true), model) =>
- val sol = Solution(BooleanLiteral(true), Set(), tupleWrap(p.xs.map(valuateWithModel(model))))
- RuleClosed(sol)
+ val solExpr = tupleWrap(p.xs.map(valuateWithModel(model)))
+
+ if (!isRealExpr(solExpr)) {
+ RuleFailed()
+ } else {
+ val sol = Solution(BooleanLiteral(true), Set(), solExpr)
+ RuleClosed(sol)
+ }
case (Some(false), model) =>
RuleClosed(Solution.UNSAT(p))
case _ =>
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 6085ef9eb2067fa092ffacfdefbf27532b02b5d9..679e49e38fb25ce3c4f79a26e1078651eccb69a5 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -36,7 +36,6 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
//println("SOLVING " + phi + " ...")
solver.solveSAT(phi) match {
case (Some(true), satModel) =>
-
val newNotPhi = valuateWithModelIn(notPhi, xss, satModel)
//println("REFUTING " + Not(newNotPhi) + "...")
@@ -46,8 +45,15 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
case (Some(false), _) =>
- result = Some(RuleClosed(Solution(BooleanLiteral(true), Set(), tupleWrap(p.xs.map(valuateWithModel(satModel))))))
-
+ // Model apprears valid, but it might be a fake expression (generic values)
+ val outExpr = tupleWrap(p.xs.map(valuateWithModel(satModel)))
+
+ if (!isRealExpr(outExpr)) {
+ // It does contain a generic value, we skip
+ predicates = valuateWithModelIn(phi, xss, satModel) +: predicates
+ } else {
+ result = Some(RuleClosed(Solution(BooleanLiteral(true), Set(), outExpr)))
+ }
case _ =>
continue = false
result = None
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index cce501ac15e547b53fc7f3a1fcbe7b473bb664bb..05a49a9064142bf537c3789ff28df948511f8dea 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -344,7 +344,7 @@ case object StringRender extends Rule("StringRender") {
val funId = FreshIdentifier(ctx.freshFunName(funName), alwaysShowUniqueID = true)
val argId= FreshIdentifier(tpe.typeToConvert.asString(hctx.context).toLowerCase()(0).toString, tpe.typeToConvert)
val tparams = hctx.sctx.functionContext.tparams
- val fd = new FunDef(funId, tparams, ValDef(argId) :: ctx.provided_functions.map(ValDef(_, false)).toList, StringType) // Empty function.
+ val fd = new FunDef(funId, tparams, ValDef(argId) :: ctx.provided_functions.map(ValDef(_)).toList, StringType) // Empty function.
fd
}
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index f753d3884e71e4ba76c84b72985f6401c0666256..eb3d83ed8d13b8235a98b48d4c209a2db5a7f08c 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -7,10 +7,13 @@ package rules
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Constructors._
+import purescala.TypeOps._
case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- val unconstr = p.xs.toSet -- variablesOf(p.phi)
+ val unconstr = (p.xs.toSet -- variablesOf(p.phi)).filter { x =>
+ isRealExpr(simplestValue(x.getType))
+ }
if (unconstr.nonEmpty) {
val sub = p.copy(xs = p.xs.filterNot(unconstr), eb = p.qeb.removeOuts(unconstr))
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index 677c9b852aafeadcfc96bd63f2b98aaaaf289940..4570501d7646b3f8d77d4fb484451ff957ac723f 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -5,10 +5,13 @@ package synthesis
package rules
import purescala.ExprOps._
+import purescala.TypeOps._
case object UnusedInput extends NormalizingRule("UnusedInput") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc) -- variablesOf(p.ws)
+ val unused = (p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc) -- variablesOf(p.ws)).filter { a =>
+ !isParametricType(a.getType)
+ }
if (unused.nonEmpty) {
val sub = p.copy(as = p.as.filterNot(unused), eb = p.qeb.removeIns(unused))
diff --git a/src/main/scala/leon/transformations/IntToRealProgram.scala b/src/main/scala/leon/transformations/IntToRealProgram.scala
index 5ab16991398e5dcb4352e870795fff51045fb9c9..0c313f2ff3ce79809420969a49bc2d3b6f11b2f3 100644
--- a/src/main/scala/leon/transformations/IntToRealProgram.scala
+++ b/src/main/scala/leon/transformations/IntToRealProgram.scala
@@ -140,9 +140,9 @@ abstract class ProgramTypeTransformer {
// FIXME
//add a new postcondition
newfd.fullBody = if (fd.postcondition.isDefined && newfd.body.isDefined) {
- val Lambda(Seq(ValDef(resid, lzy)), pexpr) = fd.postcondition.get
+ val Lambda(Seq(ValDef(resid)), pexpr) = fd.postcondition.get
val tempRes = mapId(resid).toVariable
- Ensuring(newfd.body.get, Lambda(Seq(ValDef(tempRes.id, lzy)), transformExpr(pexpr)))
+ Ensuring(newfd.body.get, Lambda(Seq(ValDef(tempRes.id)), transformExpr(pexpr)))
// Some(mapId(resid), transformExpr(pexpr))
} else NoTree(fd.returnType)
diff --git a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
index c4830cf40ca429358b0d2e420bbbe7f7d1f5c276..2e2e5c832e2b4d276ca75b4f2c5470bebb23a608 100644
--- a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
+++ b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
@@ -111,7 +111,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
def mapPost(pred: Expr, from: FunDef, to: FunDef) = {
pred match {
- case Lambda(Seq(ValDef(fromRes, lzy)), postCond) if (instFuncs.contains(from)) =>
+ case Lambda(Seq(ValDef(fromRes)), postCond) if (instFuncs.contains(from)) =>
val toResId = FreshIdentifier(fromRes.name, to.returnType, true)
val newpost = postMap((e: Expr) => e match {
case Variable(`fromRes`) =>
@@ -124,7 +124,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
case _ =>
None
})(postCond)
- Lambda(Seq(ValDef(toResId, lzy)), mapExpr(newpost))
+ Lambda(Seq(ValDef(toResId)), mapExpr(newpost))
case _ =>
mapExpr(pred)
}
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index a0b790243a6dc309953d07ba02d504e463185880..b3133d700fed92bb500423201dc4288832b07319 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -24,6 +24,7 @@ case object DebugSectionXLang extends DebugSection("xlang", 1 << 1
case object DebugSectionTypes extends DebugSection("types", 1 << 13)
case object DebugSectionIsabelle extends DebugSection("isabelle", 1 << 14)
case object DebugSectionReport extends DebugSection("report", 1 << 15)
+case object DebugSectionGenC extends DebugSection("genc", 1 << 16)
object DebugSections {
val all = Set[DebugSection](
@@ -42,6 +43,7 @@ object DebugSections {
DebugSectionXLang,
DebugSectionTypes,
DebugSectionIsabelle,
- DebugSectionReport
+ DebugSectionReport,
+ DebugSectionGenC
)
}
diff --git a/src/main/scala/leon/utils/GraphPrinters.scala b/src/main/scala/leon/utils/GraphPrinters.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b86882f2d42d6e7ea1816b249b3d35689b31ab67
--- /dev/null
+++ b/src/main/scala/leon/utils/GraphPrinters.scala
@@ -0,0 +1,215 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package utils
+
+import Graphs._
+
+object GraphPrinters {
+ abstract class Printer[N, E <: EdgeLike[N], G <: DiGraphLike[N, E, G]] {
+
+ def asString(g: G): String
+
+ def asFile(g: G, file: String) {
+ import java.io.{BufferedWriter, FileWriter}
+ val out = new BufferedWriter(new FileWriter(file))
+ out.write(asString(g))
+ out.close()
+ }
+ }
+
+ case class DotNode(label: String, opts: Map[String, String] = Map()) {
+ def toOpts(dot: DotHelpers): String = {
+ s"""[label="${dot.escape(label)}"]"""
+ }
+ }
+
+ class DotPrinter[N, E <: EdgeLike[N], G <: DiGraphLike[N, E, G]] extends Printer[N, E, G] {
+
+ val dot = new DotHelpers
+
+ private var nToLabel: N => String = { (n: N) => n.toString }
+
+ private var nToOpts: Seq[N => Seq[(String, String)]] = Nil
+
+ def setNodeLabel(f: N => String): Unit = {
+ nToLabel = f
+ }
+
+ def colorize(f: N => Boolean, color: String) = {
+ nToOpts :+= { (n: N) =>
+ if (f(n)) List(("color", color)) else Nil
+ }
+ }
+
+ def highlight(f: N => Boolean) = colorize(f, "red")
+
+
+ def drawNode(n: N)(implicit res: StringBuffer): Unit = {
+ var opts = Map[String, String]()
+ opts += "label" -> ("\"" + dot.escape(nToLabel(n)) + "\"")
+
+ for (f <- nToOpts) {
+ opts ++= f(n)
+ }
+
+ res append (nToS(n) +" "+opts.map{ case (n, v) => s"$n=$v" }.mkString("[", ", ", "]")+";\n")
+ }
+
+ def nToS(n: N): String = {
+ dot.uniqueName("n", n)
+ }
+
+ def eToS(e: EdgeLike[N]): String = {
+ dot.uniqueName("e", e)
+ }
+
+ def drawEdge(e: E)(implicit res: StringBuffer): Unit = {
+ e match {
+ case le: LabeledEdge[_, N] =>
+ res append dot.box(eToS(e), le.l.toString)
+ res append dot.arrow(nToS(e._1), eToS(e))
+ res append dot.arrow(eToS(e), nToS(e._2))
+ case _ =>
+ res append dot.arrow(nToS(e._1), nToS(e._2))
+ }
+ }
+
+ def asString(g: G): String = {
+ implicit val res = new StringBuffer()
+
+ res append "digraph D {\n"
+
+ g.N.foreach(drawNode)
+
+ g.E.foreach(drawEdge)
+
+ res append "}\n"
+
+ res.toString
+ }
+ }
+
+ class DotHelpers {
+ private var _nextName = 0
+ private var _nextColor = 0
+
+ private def nextName = {
+ _nextName += 1
+ _nextName.toString
+ }
+
+ private var names = Map[Any, String]()
+
+ def uniqueName(prefix: String, obj: Any) = {
+ if (!names.contains(obj)) {
+ names = names + (obj -> (prefix+nextName))
+ }
+
+ names(obj)
+ }
+
+ val bgColors = List("bisque", "khaki", "mistyrose", "lightcyan", "mediumorchid", "aquamarine", "antiquewhite")
+
+ def nextColor = {
+ _nextColor += 1
+ val colornumber: String = if((_nextColor/bgColors.size)%3 == 0) "" else ((_nextColor/bgColors.size)%3)+"";
+ bgColors(_nextColor%bgColors.size)+colornumber
+ }
+
+ val colors = List("khaki", "khaki1", "khaki2", "khaki3",
+ "khaki4", "lavender", "lavenderblush", "lavenderblush1", "lavenderblush2",
+ "lavenderblush3", "lavenderblush4", "lawngreen", "lemonchiffon",
+ "lemonchiffon1", "lemonchiffon2", "lemonchiffon3", "lemonchiffon4",
+ "lightblue", "lightblue1", "lightblue2", "lightblue3", "lightblue4",
+ "lightcoral", "lightcyan", "lightcyan1", "lightcyan2", "lightcyan3",
+ "lightcyan4", "lightgoldenrod", "lightgoldenrod1", "lightgoldenrod2",
+ "lightgoldenrod3", "lightgoldenrod4", "lightgoldenrodyellow", "lightgray",
+ "lightgrey", "lightpink", "lightpink1", "lightpink2", "lightpink3",
+ "lightpink4", "lightsalmon", "lightsalmon1", "lightsalmon2", "lightsalmon3",
+ "lightsalmon4", "lightseagreen", "lightskyblue", "lightskyblue1",
+ "lightskyblue2", "lightskyblue3", "lightskyblue4", "lightslateblue",
+ "lightslategray", "lightslategrey", "lightsteelblue", "lightsteelblue1",
+ "lightsteelblue2", "lightsteelblue3", "lightsteelblue4", "lightyellow",
+ "lightyellow1", "lightyellow2", "lightyellow3", "lightyellow4", "limegreen",
+ "linen", "magenta", "magenta1", "magenta2", "magenta3", "magenta4", "maroon",
+ "maroon1", "maroon2", "maroon3", "maroon4", "mediumaquamarine", "mediumblue",
+ "mediumorchid", "mediumorchid1", "mediumorchid2", "mediumorchid3",
+ "mediumorchid4", "mediumpurple", "mediumpurple1", "mediumpurple2",
+ "mediumpurple3", "mediumpurple4", "mediumseagreen", "mediumslateblue",
+ "mediumspringgreen", "mediumturquoise", "mediumvioletred", "midnightblue",
+ "mintcream", "mistyrose", "mistyrose1", "mistyrose2", "mistyrose3",
+ "mistyrose4", "moccasin", "navajowhite", "navajowhite1", "navajowhite2",
+ "navajowhite3", "navajowhite4", "navy", "navyblue", "none", "oldlace",
+ "olivedrab", "olivedrab1", "olivedrab2", "olivedrab3", "olivedrab4", "orange",
+ "orange1", "orange2", "orange3", "orange4", "orangered", "orangered1",
+ "orangered2", "orangered3", "orangered4", "orchid", "orchid1", "orchid2",
+ "orchid3", "orchid4", "palegoldenrod", "palegreen", "palegreen1", "palegreen2",
+ "palegreen3", "palegreen4", "paleturquoise", "paleturquoise1",
+ "paleturquoise2", "paleturquoise3", "paleturquoise4", "palevioletred",
+ "palevioletred1", "palevioletred2", "palevioletred3", "palevioletred4",
+ "papayawhip", "peachpuff", "peachpuff1", "peachpuff2", "peachpuff3",
+ "peachpuff4", "peru", "pink", "pink1", "pink2", "pink3", "pink4", "plum",
+ "plum1", "plum2", "plum3", "plum4", "powderblue", "purple", "purple1",
+ "purple2", "purple3", "purple4", "red", "red1", "red2", "red3", "red4",
+ "rosybrown", "rosybrown1", "rosybrown2", "rosybrown3", "rosybrown4",
+ "royalblue", "royalblue1", "royalblue2", "royalblue3", "royalblue4",
+ "saddlebrown", "salmon", "salmon1", "salmon2", "salmon3", "salmon4",
+ "sandybrown", "seagreen", "seagreen1", "seagreen2", "seagreen3", "seagreen4",
+ "seashell", "seashell1", "seashell2", "seashell3", "seashell4", "sienna",
+ "sienna1", "sienna2", "sienna3", "sienna4", "skyblue", "skyblue1", "skyblue2",
+ "skyblue3", "skyblue4", "slateblue", "slateblue1", "slateblue2", "slateblue3",
+ "slateblue4", "slategray", "slategray1", "slategray2", "slategray3",
+ "slategray4", "slategrey", "snow", "snow1", "snow2", "snow3", "snow4",
+ "springgreen", "springgreen1", "springgreen2", "springgreen3", "springgreen4",
+ "steelblue", "steelblue1", "steelblue2", "steelblue3", "steelblue4", "tan",
+ "tan1", "tan2", "tan3", "tan4", "thistle", "thistle1", "thistle2", "thistle3",
+ "thistle4", "tomato", "tomato1", "tomato2", "tomato3", "tomato4",
+ "transparent", "turquoise", "turquoise1", "turquoise2", "turquoise3",
+ "turquoise4", "violet", "violetred", "violetred1", "violetred2", "violetred3",
+ "violetred4", "wheat", "wheat1", "wheat2", "wheat3", "wheat4", "white",
+ "whitesmoke", "yellow", "yellow1", "yellow2", "yellow3", "yellow4",
+ "yellowgreen");
+
+ def randomColor = {
+ _nextColor += 1
+ colors(_nextColor % colors.size)
+ }
+
+ def escape(s: String) =
+ s.replaceAll("\\\\n", "__NEWLINE__")
+ .replaceAll("\\\\", "\\\\\\\\")
+ .replaceAll("\"", "\\\\\"")
+ .replaceAll("\\\n", "\\\\n")
+ .replaceAll("[^<>@a-zA-Z0-9;$.,!# \t=^:_\\\\\"'*+/&()\\[\\]{}\u03B5-]", "?")
+ .replaceAll("__NEWLINE__", "\\\\n")
+
+ def escapeStrict(s: String) = s.replaceAll("[^a-zA-Z0-9_]", "_")
+
+ def labeledArrow(x: String, label: String, y: String, options: List[String] = Nil) =
+ arrow(x, y, "label=\""+escape(label)+"\"" :: options)
+
+ def labeledDashedArrow(x: String, label: String, y: String, options: List[String] = Nil) =
+ arrow(x, y, "label=\""+escape(label)+"\"" :: "style=dashed" :: options)
+
+ def arrow(x: String, y: String, options: List[String] = Nil) = {
+ " "+x+" -> "+y+options.mkString(" [", " ", "]")+";\n"
+ }
+
+ def box(id : String, name : String, options: List[String] = Nil) = {
+ node(id, name, "shape=box" :: "color=lightblue" :: "style=filled" :: options)
+ }
+
+ def invisNode(id : String, name : String, options: List[String] = Nil) = {
+ node(id, name, "shape=none" :: options)
+ }
+
+ def dashedNode(id : String, name : String, options: List[String] = Nil) = {
+ node(id, name, "style=dashed" :: options)
+ }
+
+ def node(id: String, name: String, options: List[String] = Nil) = {
+ id +("label=\""+escape(name)+"\"" :: options).mkString(" [", ", ", "]")+";\n"
+ }
+ }
+}
diff --git a/src/main/scala/leon/utils/Graphs.scala b/src/main/scala/leon/utils/Graphs.scala
index b3aeef558790ce9427e376d0e0adba2851813b7b..1910c2aa25715acd325c53c9874bd1b86ec2a6f5 100644
--- a/src/main/scala/leon/utils/Graphs.scala
+++ b/src/main/scala/leon/utils/Graphs.scala
@@ -4,212 +4,228 @@ package leon
package utils
object Graphs {
- abstract class VertexAbs extends Serializable {
- val name: String
-
- override def toString = name
+ trait EdgeLike[Node] {
+ def _1: Node
+ def _2: Node
}
- abstract class EdgeAbs[V <: VertexAbs] extends Serializable {
- val v1: V
- val v2: V
-
- override def toString = v1 + "->" + v2
- }
-
- case class SimpleEdge[V <: VertexAbs](v1: V, v2: V) extends EdgeAbs[V]
-
- abstract class LabeledEdgeAbs[T, V <: VertexAbs] extends EdgeAbs[V] {
- val label: T
- }
-
- case class SimpleLabeledEdge[T, V <: VertexAbs](v1: V, label: T, v2: V) extends LabeledEdgeAbs[T, V]
-
- trait DirectedGraph[V <: VertexAbs, E <: EdgeAbs[V], G <: DirectedGraph[V,E,G]] extends Serializable {
- type Vertex = V
- type Edge = E
- type This = G
+ case class SimpleEdge[Node](_1: Node, _2: Node) extends EdgeLike[Node]
+ case class LabeledEdge[Label, Node](_1: Node, l: Label, _2: Node) extends EdgeLike[Node]
+ trait DiGraphLike[Node, Edge <: EdgeLike[Node], G <: DiGraphLike[Node, Edge, G]] {
// The vertices
- def V: Set[Vertex]
+ def N: Set[Node]
// The edges
def E: Set[Edge]
+
// Returns the set of incoming edges for a given vertex
- def inEdges(v: Vertex) = E.filter(_.v2 == v)
+ def inEdges(n: Node) = E.filter(_._2 == n)
// Returns the set of outgoing edges for a given vertex
- def outEdges(v: Vertex) = E.filter(_.v1 == v)
+ def outEdges(n: Node) = E.filter(_._1 == n)
// Returns the set of edges between two vertices
- def edgesBetween(from: Vertex, to: Vertex) = {
- E.filter(e => e.v1 == from && e.v2 == to)
+ def edgesBetween(from: Node, to: Node) = {
+ E.filter(e => e._1 == from && e._2 == to)
}
- /**
- * Basic Graph Operations:
- */
-
// Adds a new vertex
- def + (v: Vertex): This
+ def + (n: Node): G
// Adds new vertices
- def ++ (vs: Traversable[Vertex]): This
+ def ++ (ns: Traversable[Node]): G
// Adds a new edge
- def + (e: Edge): This
+ def + (e: Edge): G
// Removes a vertex from the graph
- def - (from: Vertex): This
+ def - (from: Node): G
// Removes a number of vertices from the graph
- def -- (from: Traversable[Vertex]): This
+ def -- (from: Traversable[Node]): G
// Removes an edge from the graph
- def - (from: Edge): This
-
- /**
- * Advanced Graph Operations:
- */
-
- // Merges two graphs
- def union(that: This): This
- // Return the strongly connected components, sorted topologically
- def stronglyConnectedComponents: Seq[Set[Vertex]]
- // Topological sorting
- def topSort: Option[Seq[Vertex]]
- // All nodes leading to v
- def transitivePredecessors(v: Vertex): Set[Vertex]
- // All nodes reachable from v
- def transitiveSuccessors(v: Vertex): Set[Vertex]
- // Is v1 reachable from v2
- def isReachable(v1: Vertex, v2: Vertex): Boolean
+ def - (from: Edge): G
}
- case class DirectedGraphImp[Vertex <: VertexAbs, Edge <: EdgeAbs[Vertex]](
- vertices: Set[Vertex],
- edges: Set[Edge],
- ins: Map[VertexAbs, Set[Edge]],
- outs: Map[VertexAbs, Set[Edge]]
- ) extends DirectedGraph[Vertex, Edge, DirectedGraphImp[Vertex, Edge]] {
-
- override def equals(o: Any): Boolean = o match {
- case other: DirectedGraphImp[_, _] =>
- this.vertices == other.vertices &&
- this.edges == other.edges &&
- (this.ins.keySet ++ other.ins.keySet).forall (k => this.ins(k) == other.ins(k)) &&
- (this.outs.keySet ++ other.outs.keySet).forall(k => this.outs(k) == other.outs(k))
-
- case _ => false
+ case class DiGraph[Node, Edge <: EdgeLike[Node]](N: Set[Node] = Set[Node](), E: Set[Edge] = Set[Edge]()) extends DiGraphLike[Node, Edge, DiGraph[Node, Edge]] with DiGraphOps[Node, Edge, DiGraph[Node, Edge]]{
+ def +(n: Node) = copy(N=N+n)
+ def ++(ns: Traversable[Node]) = copy(N=N++ns)
+ def +(e: Edge) = (this+e._1+e._2).copy(E = E + e)
+
+ def -(n: Node) = copy(N = N-n, E = E.filterNot(e => e._1 == n || e._2 == n))
+ def --(ns: Traversable[Node]) = {
+ val toRemove = ns.toSet
+ copy(N = N--ns, E = E.filterNot(e => toRemove.contains(e._1) || toRemove.contains(e._2)))
}
- def this (vertices: Set[Vertex], edges: Set[Edge]) =
- this(vertices,
- edges,
- edges.groupBy(_.v2: VertexAbs).withDefaultValue(Set()),
- edges.groupBy(_.v1: VertexAbs).withDefaultValue(Set()))
-
- def this() = this(Set(), Set())
-
- val V = vertices
- val E = edges
-
- def + (v: Vertex) = copy(
- vertices = vertices+v
- )
-
- override def inEdges(v: Vertex) = ins(v)
- override def outEdges(v: Vertex) = outs(v)
-
- def ++ (vs: Traversable[Vertex]) = copy(
- vertices = vertices++vs
- )
-
- def -- (vs: Traversable[Vertex]) = copy(
- vertices = vertices--vs,
- edges = edges -- vs.flatMap(outs) -- vs.flatMap(ins),
- ins = ((ins -- vs) map { case (vm, edges) => vm -> (edges -- vs.flatMap(outs)) }).withDefaultValue(Set()) ,
- outs = ((outs -- vs) map { case (vm, edges) => vm -> (edges -- vs.flatMap(ins)) }).withDefaultValue(Set())
- )
-
- def + (e: Edge) = copy(
- vertices = vertices + e.v1 + e.v2,
- edges = edges + e,
- ins = ins + (e.v2 -> (ins(e.v2) + e)),
- outs = outs + (e.v1 -> (outs(e.v1) + e))
- )
-
- def - (v: Vertex) = copy(
- vertices = vertices-v,
- edges = edges -- outs(v) -- ins(v),
- ins = ((ins - v) map { case (vm, edges) => vm -> (edges -- outs(v)) }).withDefaultValue(Set()) ,
- outs = ((outs - v) map { case (vm, edges) => vm -> (edges -- ins(v)) }).withDefaultValue(Set())
- )
-
- def - (e: Edge) = copy(
- vertices = vertices,
- edges = edges-e,
- ins = ins + (e.v2 -> (ins(e.v2) - e)),
- outs = outs + (e.v1 -> (outs(e.v1) - e))
- )
-
- def union(that: This): This = copy(
- vertices = this.V ++ that.V,
- edges = this.E ++ that.E,
- ins = ((this.ins.keySet ++ that.ins.keySet) map { k => k -> (this.ins(k) ++ that.ins(k)) }).toMap.withDefaultValue(Set()),
- outs = ((this.outs.keySet ++ that.outs.keySet) map { k => k -> (this.outs(k) ++ that.outs(k)) }).toMap.withDefaultValue(Set())
- )
-
- def stronglyConnectedComponents: Seq[Set[Vertex]] = ???
-
- def topSort = {
- val sccs = stronglyConnectedComponents
- if (sccs.forall(_.size == 1)) {
- Some(sccs.flatten)
- } else {
- None
- }
+ def -(e: Edge) = copy(E = E-e)
+ }
+
+
+ trait DiGraphOps[Node, Edge <: EdgeLike[Node], G <: DiGraphLike[Node, Edge, G]] {
+ this: G =>
+
+ def sources: Set[Node] = {
+ N -- E.map(_._2)
}
- def transitivePredecessors(v: Vertex): Set[Vertex] = {
- var seen = Set[Vertex]()
- def rec(v: Vertex): Set[Vertex] = {
- if (seen(v)) {
- Set()
- } else {
- seen += v
- val ins = inEdges(v).map(_.v1)
- ins ++ ins.flatMap(rec)
+ def sinks: Set[Node] = {
+ N -- E.map(_._1)
+ }
+
+ def stronglyConnectedComponents: DiGraph[Set[Node], SimpleEdge[Set[Node]]] = {
+ // Tarjan's algorithm
+ var index = 0
+ var stack = List[Node]()
+
+ var indexes = Map[Node, Int]()
+ var lowlinks = Map[Node, Int]()
+ var onStack = Set[Node]()
+
+ var nodesToScc = Map[Node, Set[Node]]()
+ var res = DiGraph[Set[Node], SimpleEdge[Set[Node]]]()
+
+ def strongConnect(n: Node): Unit = {
+ indexes += n -> index
+ lowlinks += n -> index
+ index += 1
+
+ stack = n :: stack
+ onStack += n
+
+ for (m <- succ(n)) {
+ if (!(indexes contains m)) {
+ strongConnect(m)
+ lowlinks += n -> (lowlinks(n) min lowlinks(m))
+ } else if (onStack(m)) {
+ lowlinks += n -> (lowlinks(n) min indexes(m))
+ }
+ }
+
+ if (lowlinks(n) == indexes(n)) {
+ val i = stack.indexOf(n)+1
+ val ns = stack.take(i)
+ stack = stack.drop(i)
+ val scc = ns.toSet
+ onStack --= ns
+ nodesToScc ++= ns.map(n => n -> scc)
+ res += scc
}
}
- rec(v)
- }
- def transitiveSuccessors(v: Vertex): Set[Vertex] = {
- var seen = Set[Vertex]()
- def rec(v: Vertex): Set[Vertex] = {
- if (seen(v)) {
- Set()
- } else {
- seen += v
- val outs = outEdges(v).map(_.v2)
- outs ++ outs.flatMap(rec)
+
+ for (n <- N if !(indexes contains n)) {
+ strongConnect(n)
+ }
+
+ for (e <- E) {
+ val s1 = nodesToScc(e._1)
+ val s2 = nodesToScc(e._2)
+ if (s1 != s2) {
+ res += SimpleEdge(s1, s2)
}
}
- rec(v)
+
+ res
}
- def isReachable(v1: Vertex, v2: Vertex): Boolean = {
- var seen = Set[Vertex]()
- def rec(v: Vertex): Boolean = {
- if (seen(v)) {
- false
- } else {
- seen += v
- val outs = outEdges(v).map(_.v2)
- if (outs(v2)) {
- true
- } else {
- outs.exists(rec)
+ def topSort: Seq[Node] = {
+ var res = List[Node]()
+
+ var temp = Set[Node]()
+ var perm = Set[Node]()
+
+ def visit(n: Node) {
+ if (temp(n)) {
+ throw new IllegalArgumentException("Graph is not a DAG")
+ } else if (!perm(n)) {
+ temp += n
+ for (n2 <- succ(n)) {
+ visit(n2)
}
+ perm += n
+ temp -= n
+ res ::= n
}
}
- rec(v1)
+
+ for (n <- N if !temp(n) && !perm(n)) {
+ visit(n)
+ }
+
+ res
+ }
+
+ def depthFirstSearch(from: Node)(f: Node => Unit): Unit = {
+ var visited = Set[Node]()
+
+ val stack = new collection.mutable.Stack[Node]()
+
+ stack.push(from)
+
+ while(stack.nonEmpty) {
+ val n = stack.pop
+ visited += n
+ f(n)
+ for (n2 <- succ(n) if !visited(n2)) {
+ stack.push(n2)
+ }
+ }
+ }
+
+ def fold[T](from: Node)(
+ follow: Node => Traversable[Node],
+ map: Node => T,
+ compose: List[T] => T): T = {
+
+ var visited = Set[Node]()
+
+ def visit(n: Node): T = {
+ visited += n
+
+ val toFollow = follow(n).filterNot(visited)
+ visited ++= toFollow
+
+ compose(map(n) :: toFollow.toList.map(visit))
+ }
+
+ compose(follow(from).toList.map(visit))
+ }
+
+ def succ(from: Node): Set[Node] = {
+ outEdges(from).map(_._2)
+ }
+
+ def pred(from: Node): Set[Node] = {
+ inEdges(from).map(_._1)
+ }
+
+ def transitiveSucc(from: Node): Set[Node] = {
+ fold[Set[Node]](from)(
+ succ,
+ Set(_),
+ _.toSet.flatten
+ )
}
- override def toString = "DGraph[V: "+vertices+" | E:"+edges+"]"
+ def transitivePred(from: Node): Set[Node] = {
+ fold[Set[Node]](from)(
+ pred,
+ Set(_),
+ _.toSet.flatten
+ )
+ }
+
+ def breadthFirstSearch(from: Node)(f: Node => Unit): Unit = {
+ var visited = Set[Node]()
+
+ val queue = new collection.mutable.Queue[Node]()
+
+ queue += from
+
+ while(queue.nonEmpty) {
+ val n = queue.dequeue
+ visited += n
+ f(n)
+ for (n2 <- succ(n) if !visited(n2)) {
+ queue += n2
+ }
+ }
+ }
}
}
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 4a395912a6b9dc92a9828fc90bed421baf009c97..06f35dc3a47df0a48836e6137eaae96218745d39 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -9,7 +9,7 @@ import leon.solvers.isabelle.AdaptationPhase
import leon.verification.InjectAsserts
import leon.xlang.{NoXLangFeaturesChecking, XLangDesugaringPhase}
-class PreprocessingPhase(desugarXLang: Boolean = false) extends LeonPhase[Program, Program] {
+class PreprocessingPhase(desugarXLang: Boolean = false, genc: Boolean = false) extends LeonPhase[Program, Program] {
val name = "preprocessing"
val description = "Various preprocessings on Leon programs"
@@ -39,19 +39,27 @@ class PreprocessingPhase(desugarXLang: Boolean = false) extends LeonPhase[Progra
CheckADTFieldsTypes andThen
InliningPhase
- val pipeX = if(desugarXLang) {
+ val pipeX = if (!genc && desugarXLang) {
+ // Do not desugar when generating C code
XLangDesugaringPhase andThen
debugTrees("Program after xlang desugaring")
} else {
NoopPhase[Program]()
}
+ def pipeEnd = if (genc) {
+ // No InjectAsserts, FunctionClosure and AdaptationPhase phases
+ NoopPhase[Program]()
+ } else {
+ InjectAsserts andThen
+ FunctionClosure andThen
+ AdaptationPhase
+ }
+
val phases =
pipeBegin andThen
pipeX andThen
- InjectAsserts andThen
- FunctionClosure andThen
- AdaptationPhase andThen
+ pipeEnd andThen
debugTrees("Program after pre-processing")
phases.run(ctx, p)
diff --git a/src/sphinx/genc.rst b/src/sphinx/genc.rst
new file mode 100644
index 0000000000000000000000000000000000000000..faac1f142f843e4014dbac4603784c4fa37ebe16
--- /dev/null
+++ b/src/sphinx/genc.rst
@@ -0,0 +1,122 @@
+.. _genc:
+
+Safe C Code
+===========
+
+Leon can generate from Scala code an equivalent and safe C99 code. Using the verification, repair and
+synthesis features of Leon this conversion can be made safely. Additionally, the produced code can be
+compiled with any standard-compliant C99 compiler to target the desired hardware architecture
+without extra dependencies.
+
+To convert a Scala program, one can use the ``--genc`` and ``--o=<output.c>`` command line options
+of Leon.
+
+.. NOTE::
+ Currently the memory model is limited to stack-allocated memory. Hence, no dynamic allocation
+ is done using ``malloc`` function family.
+
+
+Supported Features
+------------------
+
+The supported subset of Scala includes part of the core languages features, as well as some
+extensions from :ref:`XLang <xlang>`, while ensuring the same expression execution order in both
+languages.
+
+Currently all type and function definitions need to be included in one top level object.
+
+
+Types
+*****
+
+The following raw types and their corresponding literals are supported:
+
+.. list-table::
+ :header-rows: 1
+
+ * - Scala
+ - C99
+ * - ``Unit``
+ - ``void``
+ * - ``Boolean``
+ - ``bool``
+ * - ``Int`` (32-bit Integer)
+ - ``int32_t``
+
+Tuples
+^^^^^^
+
+Using ``TupleN[T1, ..., TN]`` results in the creation of a C structure with the same
+fields and types for every combination of any supported type ``T1, ..., TN``. The name of the
+generated structure will be unique and reflect the sequence of types.
+
+
+Arrays
+^^^^^^
+
+``Array[T]`` are implemented using regular C array when the array size is known at compile time, or
+using Variable Length Array (VLA) when the size is only available at runtime. Both types of array
+use the same unique structure type to keep track of the length of the array and its allocated
+memory.
+
+.. NOTE::
+
+ Arrays live on the stack and therefore cannot be returned by functions. This limitation is
+ extended to other types having an array as field.
+
+
+Arrays can be created using the companion object, e.g. ``Array(1, 2, 3)``, or using the
+``Array.fill`` method, e.g. ``Array.fill(size)(value)``.
+
+
+Case Classes
+^^^^^^^^^^^^
+
+The support for classes is restricted to non-recursive case classes for which fields are immutable.
+Instances of such data-types live on the stack.
+
+
+Functions
+*********
+
+Functions and nested functions are supported, with access to the variables in their respective
+scopes. However, higher order functions are as of this moment not supported.
+
+Since strings of characters are currently not available, to generate an executable program, one has
+to define a main function without any argument that returns an integer: ``def main: Int = ...``.
+
+Both ``val`` and ``var`` are supported with the limitations imposed by the :ref:`XLang <xlang>`
+extensions.
+
+
+Constructs
+**********
+
+The idiomatic ``if`` statements such as ``val b = if (x >= 0) true else false`` are converted into
+a sequence of equivalent statements.
+
+Imperative ``while`` loops are also supported.
+
+Assertions, invariant, pre- and post-conditions are not translated into C99 and are simply ignored.
+
+
+Operators
+*********
+
+The following operators are supported:
+
+.. list-table::
+ :header-rows: 1
+
+ * - Category
+ - Operators
+ * - Boolean operators
+ - ``&&``, ``||``, ``!``, ``!=``, ``==``
+ * - Comparision operators over integers
+ - ``<``, ``<=``, ``==``, ``!=``, ``>=``, ``>``
+ * - Arithmetic operators over integers
+ - ``+``, ``-`` (unary & binary), ``*``, ``/``, ``%``
+ * - Bitwise operators over integers
+ - ``&``, ``|``, ``^``, ``~``, ``<<``, ``>>``
+
+
diff --git a/src/sphinx/index.rst b/src/sphinx/index.rst
index a20401170d34be2ef293878e72b678aaac462598..cf46d2c300d3821a4cb987d657bded60597ce534 100644
--- a/src/sphinx/index.rst
+++ b/src/sphinx/index.rst
@@ -25,6 +25,7 @@ Contents:
limitations
synthesis
repair
+ genc
options
faq
references
diff --git a/src/sphinx/options.rst b/src/sphinx/options.rst
index 1c929cd29cdc5281378cd322389b867902f0ff2b..a5be01e35269e12864cd6716947727209497b337 100644
--- a/src/sphinx/options.rst
+++ b/src/sphinx/options.rst
@@ -20,41 +20,46 @@ Choosing which Leon feature to use
The first group of options determine which feature of Leon will be used.
These options are mutually exclusive (except when noted). By default, ``--verify`` is chosen.
-* ``--eval``
-
+* ``--eval``
+
Evaluates parameterless functions and value definitions.
-
+
* ``--verify``
-
+
Proves or disproves function contracts, as explained in the :ref:`verification` section.
* ``--repair``
-
+
Runs program :ref:`repair <repair>`.
-
+
* ``--synthesis``
-
+
Partially synthesizes ``choose()`` constructs (see :ref:`synthesis` section).
* ``--termination``
-
+
Runs termination analysis. Can be used along ``--verify``.
-* ``--inferInv``
+* ``--inferInv``
+
+ Infer invariants from the (instrumented) code (using Orb).
- Infer invariants from the (instrumented) code (using Orb)
+* ``--instrument``
-* ``--instrument``
+ Instrument the code for inferring time/depth/stack bounds (using Orb).
- Instrument the code for inferring time/depth/stack bounds (using Orb)
+* ``--genc``
+
+ Translate a Scala program into C99 equivalent code (see :ref:`genc` section); requires
+ ``--xlang``.
* ``--noop``
-
+
Runs the program through the extraction and preprocessing phases, then outputs it in the specified
directory. Used mostly for debugging purposes.
* ``--help``
-
+
Prints a helpful message, then exits.
@@ -65,44 +70,46 @@ Additional top-level options
These options are available to all Leon components:
* ``--debug=d1,d2,...``
-
+
Enables printing detailed messages for the components d1,d2,... .
- Available components are:
+ Available components are:
* ``datagen`` (Data generators)
-
+
* ``eval`` (Evaluators)
-
+
+ * ``genc`` (C code generation)
+
* ``isabelle`` (:ref:`The Isabelle-based solver <isabelle>`)
* ``leon`` (The top-level component)
-
+
* ``options`` (Options parsed by Leon)
-
+
* ``positions`` (When printing, attach positions to trees)
* ``repair`` (Program repair)
-
+
* ``solver`` (SMT solvers and their wrappers)
-
+
* ``synthesis`` (Program synthesis)
-
+
* ``termination`` (Termination analysis)
-
+
* ``timers`` (Timers, timer pools)
-
+
* ``trees`` (Manipulation of trees)
-
+
* ``types`` (When printing, attach types to expressions)
* ``verification`` (Verification)
-
+
* ``xlang`` (Transformation of XLang into Pure Scala programs)
* ``--functions=f1,f2,...``
-
- Only consider functions f1, f2, ... . This applies to all functionalities
+
+ Only consider functions f1, f2, ... . This applies to all functionalities
where Leon manipulates the input in a per-function basis.
Leon will match against suffixes of qualified names. For instance:
@@ -111,22 +118,22 @@ These options are available to all Leon components:
This option supports ``_`` as wildcard: ``--functions=List._`` will
match all ``List`` methods.
-* ``--solvers=s1,s2,...``
-
- Use solvers s1, s2,... . If more than one solver is chosen, all chosen
+* ``--solvers=s1,s2,...``
+
+ Use solvers s1, s2,... . If more than one solver is chosen, all chosen
solvers will be used in parallel, and the best result will be presented.
By default, the ``fairz3`` solver is picked.
-
- Some solvers are specialized in proving verification conditions
- and will have hard time finding a counterexample in case of an invalid
+
+ Some solvers are specialized in proving verification conditions
+ and will have hard time finding a counterexample in case of an invalid
verification condition, whereas some are specialized in finding
counterexamples, and some provide a compromise between the two.
Also, some solvers do not as of now support higher-order functions.
Available solvers include:
-
- * ``enum``
-
+
+ * ``enum``
+
Uses enumeration-based techniques to discover counterexamples.
This solver does not actually invoke an SMT solver,
and operates entirely on the level of Leon trees.
@@ -134,50 +141,50 @@ These options are available to all Leon components:
* ``fairz3``
Native Z3 with z3-templates for unfolding recursive functions (default).
-
+
* ``smt-cvc4``
-
- CVC4 through SMT-LIB. An algorithm within Leon takes up the unfolding
- of recursive functions, handling of lambdas etc. To use this or any
+
+ CVC4 through SMT-LIB. An algorithm within Leon takes up the unfolding
+ of recursive functions, handling of lambdas etc. To use this or any
of the following CVC4-based solvers, you need to have the ``cvc4``
executable in your system path (the latest unstable version is recommended).
-
+
* ``smt-cvc4-cex``
-
+
CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only.
Recursive functions are not unrolled, but encoded through the
``define-funs-rec`` construct available in the new SMTLIB-2.5 standard.
Currently, this solver does not handle higher-order functions.
-
+
* ``smt-cvc4-proof``
-
- CVC4 through SMT-LIB, for proofs only. Functions are encoded as in
+
+ CVC4 through SMT-LIB, for proofs only. Functions are encoded as in
``smt-cvc4-cex``.
Currently, this solver does not handle higher-order functions.
-
+
* ``smt-z3``
-
- Z3 through SMT-LIB. To use this or the next solver, you need to
+
+ Z3 through SMT-LIB. To use this or the next solver, you need to
have the ``z3`` executable in your program path (the latest stable version
is recommended). Inductive reasoning happens on the Leon side
(similarly to ``smt-cvc4``).
-
+
* ``smt-z3-q``
-
- Z3 through SMT-LIB, but (recursive) functions are not unrolled and are
+
+ Z3 through SMT-LIB, but (recursive) functions are not unrolled and are
instead encoded with universal quantification.
For example, ``def foo(x:A) = e`` would be encoded by asserting
-
+
.. math::
-
+
\forall (x:A). foo(x) = e
even if ``e`` contains an invocation to ``foo``.
Currently, this solver does not handle higher-order functions.
-
+
* ``unrollz3``
-
+
Native Z3, but inductive reasoning happens within Leon (similarly to ``smt-z3``).
* ``ground``
@@ -187,21 +194,23 @@ These options are available to all Leon components:
* ``isabelle``
Solve verification conditions via Isabelle.
-
+
* ``--strict``
- Terminate Leon after each phase if a non-fatal error is encountered
+ Terminate Leon after each phase if a non-fatal error is encountered
(such as a failed verification condition). By default, this option is activated.
* ``--timeout=t``
Set a timeout for each attempt to prove one verification condition/
repair one function (in sec.)
-
+
* ``--xlang``
-
+
Support for additional language constructs described in :ref:`xlang`.
- These constructs are desugared into :ref:`purescala` before other operations.
+ These constructs are desugared into :ref:`purescala` before other operations,
+ except for the ``--genc`` option which uses the original constructs to generate
+ :ref:`genc`.
Additional Options (by component)
---------------------------------
@@ -222,10 +231,12 @@ File Output
***********
* ``--o=dir``
-
+
Output files to the directory ``dir`` (default: leon.out).
Used when ``--noop`` is selected.
+ When used with ``--genc`` this option designates the output *file*.
+
Code Extraction
***************
@@ -245,21 +256,21 @@ Synthesis
Shrink non-deterministic programs when tests pruning works well.
* ``--cegis:vanuatoo``
-
+
Generate inputs using new korat-style generator.
-
+
* ``--costmodel=cm``
-
+
Use a specific cost model for this search.
Available: ``Naive``, ``WeightedBranches``
* ``--derivtrees``
-
+
Generate a derivation tree for every synthesized function.
The trees will be output in ``*.dot`` files.
* ``--manual=cmd``
-
+
Override Leon's automated search through the space of programs during synthesis.
Instead, the user can navigate the program space manually
by choosing which deductive synthesis rules is instantiated each time.
@@ -277,26 +288,26 @@ Fair-z3 Solver
Double-check counter-examples with evaluator.
* ``--codegen``
-
+
Use compiled evaluator instead of interpreter.
* ``--evalground``
-
+
Use evaluator on functions applied to ground arguments.
-
+
* ``--feelinglucky``
-
+
Use evaluator to find counter-examples early.
* ``--unrollcores``
-
+
Use unsat-cores to drive unrolling while remaining fair.
-
+
CVC4 Solver
***********
* ``--solver:cvc4=<cvc4-opt>``
-
+
Pass extra command-line arguments to CVC4.
Isabelle
diff --git a/src/test/resources/regression/genc/invalid/AbsFun.scala b/src/test/resources/regression/genc/invalid/AbsFun.scala
new file mode 100644
index 0000000000000000000000000000000000000000..aff9a2c80f70f5e3aef079220c1c36b29b40b2e3
--- /dev/null
+++ b/src/test/resources/regression/genc/invalid/AbsFun.scala
@@ -0,0 +1,66 @@
+import leon.lang._
+
+object AbsFun {
+
+
+ def isPositive(a : Array[Int], size : Int) : Boolean = {
+ require(a.length >= 0 && size <= a.length)
+ rec(0, a, size)
+ }
+
+ def rec(i: Int, a: Array[Int], size: Int) : Boolean = {
+ require(a.length >= 0 && size <= a.length && i >= 0)
+
+ if(i >= size) true
+ else {
+ if (a(i) < 0)
+ false
+ else
+ rec(i + 1, a, size)
+ }
+ }
+
+ // Returning Arrays is not supported by GenC
+ def abs(tab: Array[Int]): Array[Int] = {
+ require(tab.length >= 0)
+ val t = while0(Array.fill(tab.length)(0), 0, tab)
+ t._1
+ } ensuring(res => isPositive(res, res.length))
+
+
+ def while0(t: Array[Int], k: Int, tab: Array[Int]): (Array[Int], Int) = {
+ require(tab.length >= 0 &&
+ t.length == tab.length &&
+ k >= 0 &&
+ k <= tab.length &&
+ isPositive(t, k))
+
+ if(k < tab.length) {
+ val nt = if(tab(k) < 0) {
+ t.updated(k, -tab(k))
+ } else {
+ t.updated(k, tab(k))
+ }
+ while0(nt, k+1, tab)
+ } else {
+ (t, k)
+ }
+ } ensuring(res =>
+ res._2 >= tab.length &&
+ res._1.length == tab.length &&
+ res._2 >= 0 &&
+ res._2 <= tab.length &&
+ isPositive(res._1, res._2))
+
+ def property(t: Array[Int], k: Int): Boolean = {
+ require(isPositive(t, k) && t.length >= 0 && k >= 0)
+ if(k < t.length) {
+ val nt = if(t(k) < 0) {
+ t.updated(k, -t(k))
+ } else {
+ t.updated(k, t(k))
+ }
+ isPositive(nt, k+1)
+ } else true
+ } holds
+}
diff --git a/src/test/resources/regression/genc/invalid/LinearSearch.scala b/src/test/resources/regression/genc/invalid/LinearSearch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..88cadb0ef7dc5ca5425a3f1661495cb08af4df65
--- /dev/null
+++ b/src/test/resources/regression/genc/invalid/LinearSearch.scala
@@ -0,0 +1,40 @@
+import leon.lang._
+
+/* The calculus of Computation textbook */
+
+object LinearSearch {
+
+ def linearSearch(a: Array[Int], c: Int): Boolean = ({
+ require(a.length >= 0)
+ var i = 0
+ var found = false
+ (while(i < a.length) {
+ if(a(i) == c)
+ found = true
+ i = i + 1
+ }) invariant(
+ i <= a.length &&
+ i >= 0 &&
+ (if(found) contains(a, i, c) else !contains(a, i, c))
+ )
+ found
+ }) ensuring(res => if(res) contains(a, a.length, c) else !contains(a, a.length, c))
+
+ def contains(a: Array[Int], size: Int, c: Int): Boolean = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
+ content(a, size).contains(c)
+ }
+
+ // Set not supported by GenC
+ def content(a: Array[Int], size: Int): Set[Int] = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
+ var set = Set.empty[Int]
+ var i = 0
+ (while(i < size) {
+ set = set ++ Set(a(i))
+ i = i + 1
+ }) invariant(i >= 0 && i <= size)
+ set
+ }
+
+}
diff --git a/src/test/resources/regression/genc/unverified/BinarySearch.scala b/src/test/resources/regression/genc/unverified/BinarySearch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..aec7d2b5ddabc0132d6f9e885eb18c80617f7dc9
--- /dev/null
+++ b/src/test/resources/regression/genc/unverified/BinarySearch.scala
@@ -0,0 +1,82 @@
+import leon.lang._
+
+/* VSTTE 2008 - Dafny paper */
+
+object BinarySearch {
+
+ def binarySearch(a: Array[Int], key: Int): Int = ({
+ require(a.length > 0 && sorted(a, 0, a.length - 1))
+ var low = 0
+ var high = a.length - 1
+ var res = -1
+
+ (while(low <= high && res == -1) {
+ //val i = (high + low) / 2
+ val i = low + ((high - low) / 2)
+ val v = a(i)
+
+ if(v == key)
+ res = i
+
+ if(v > key)
+ high = i - 1
+ else if(v < key)
+ low = i + 1
+ }) invariant(
+ res >= -1 &&
+ res < a.length &&
+ 0 <= low &&
+ low <= high + 1 &&
+ high >= -1 &&
+ high < a.length &&
+ (if (res >= 0)
+ a(res) == key else
+ (!occurs(a, 0, low, key) && !occurs(a, high + 1, a.length, key))
+ )
+ )
+ res
+ }) ensuring(res =>
+ res >= -1 &&
+ res < a.length &&
+ (if(res >= 0) a(res) == key else !occurs(a, 0, a.length, key)))
+
+
+ def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
+ require(a.length >= 0 && to <= a.length && from >= 0)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= to)
+ false
+ else {
+ if(a(i) == key) true else rec(i+1)
+ }
+ }
+ if(from >= to)
+ false
+ else
+ rec(from)
+ }
+
+
+ def sorted(a: Array[Int], l: Int, u: Int) : Boolean = {
+ require(a.length >= 0 && l >= 0 && l <= u && u < a.length)
+ val t = sortedWhile(true, l, l, u, a)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Array[Int]): (Boolean, Int) = {
+ require(a.length >= 0 && l >= 0 && l <= u && u < a.length && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a)
+ } else (isSorted, k)
+ }
+
+
+ def main = {
+ val a = Array(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10)
+ val i = binarySearch(a, 2)
+ i - 2 // i should be 2
+ }
+
+}
+
diff --git a/src/test/resources/regression/genc/unverified/BinarySearchFun.scala b/src/test/resources/regression/genc/unverified/BinarySearchFun.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ebc97f6c6d046e2907bda89c795def7026cb4c8f
--- /dev/null
+++ b/src/test/resources/regression/genc/unverified/BinarySearchFun.scala
@@ -0,0 +1,70 @@
+import leon.lang._
+
+object BinarySearchFun {
+
+ def binarySearch(a: Array[Int], key: Int, low: Int, high: Int): Int = ({
+ require(a.length > 0 && sorted(a, low, high) &&
+ 0 <= low && low <= high + 1 && high < a.length
+ )
+
+ if (low <= high) {
+ //val i = (high + low) / 2
+ val i = low + (high - low) / 2
+
+ val v = a(i)
+
+ if (v == key) i
+ else if (v > key) binarySearch(a, key, low, i - 1)
+ else binarySearch(a, key, i + 1, high)
+ } else -1
+ }) ensuring(res =>
+ res >= -1 &&
+ res < a.length && (
+ if (res >= 0)
+ a(res) == key
+ else
+ (high < 0 || (!occurs(a, low, low + (high - low) / 2, key) &&
+ !occurs(a, low + (high - low) / 2, high, key)))
+ )
+ )
+
+
+ def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
+ require(a.length >= 0 && to <= a.length && from >= 0)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if (i >= to)
+ false
+ else {
+ if (a(i) == key) true else rec(i+1)
+ }
+ }
+ if (from >= to)
+ false
+ else
+ rec(from)
+ }
+
+
+ def sorted(a: Array[Int], l: Int, u: Int) : Boolean = {
+ require(a.length >= 0 && l >= 0 && l <= u + 1 && u < a.length)
+ val t = sortedWhile(true, l, l, u, a)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Array[Int]): (Boolean, Int) = {
+ require(a.length >= 0 && l >= 0 && l <= u+1 && u < a.length && k >= l && k <= u + 1)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a)
+ } else (isSorted, k)
+ }
+
+ def main = {
+ val a = Array(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10)
+ val i = binarySearch(a, 2, 0, a.length - 1) // should be 2
+ val j = binarySearch(a, 11, 0, a.length - 1) // should be -1
+
+ (i - 2) + (j + 1) // == 0
+ }
+}
+
diff --git a/src/test/resources/regression/genc/unverified/MaxSum.scala b/src/test/resources/regression/genc/unverified/MaxSum.scala
new file mode 100644
index 0000000000000000000000000000000000000000..033dfed30a6930f4041c60a1c4f8a9dfbb87d934
--- /dev/null
+++ b/src/test/resources/regression/genc/unverified/MaxSum.scala
@@ -0,0 +1,71 @@
+import leon.lang._
+
+/* VSTTE 2010 challenge 1 */
+
+object MaxSum {
+
+ def maxSum(a: Array[Int]): (Int, Int) = ({
+ require(a.length >= 0 && isPositive(a))
+ var sum = 0
+ var max = 0
+ var i = 0
+ (while(i < a.length) {
+ if(max < a(i))
+ max = a(i)
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant (sum <= i * max && i >= 0 && i <= a.length)
+ (sum, max)
+ }) ensuring(res => res._1 <= a.length * res._2)
+
+
+ def isPositive(a: Array[Int]): Boolean = {
+ require(a.length >= 0)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= a.length)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+
+ def summ(to : Int): Int = ({
+ require(to >= 0)
+ var i = 0
+ var s = 0
+ (while (i < to) {
+ s = s + i
+ i = i + 1
+ }) invariant (s >= 0 && i >= 0 && s == i*(i-1)/2 && i <= to)
+ s
+ }) ensuring(res => res >= 0 && res == to*(to-1)/2)
+
+
+ def sumsq(to : Int): Int = ({
+ require(to >= 0)
+ var i = 0
+ var s = 0
+ (while (i < to) {
+ s = s + i*i
+ i = i + 1
+ }) invariant (s >= 0 && i >= 0 && s == (i-1)*i*(2*i-1)/6 && i <= to)
+ s
+ }) ensuring(res => res >= 0 && res == (to-1)*to*(2*to-1)/6)
+
+ def main = {
+ val a = Array(1, 4, 6, 0, 234, 999)
+ val sm = maxSum(a)
+ val sum = sm._1
+ val max = sm._2
+ if (sum == 1244 && max == 999) 0
+ else -1
+ } ensuring { _ == 0 }
+
+}
+
diff --git a/src/test/resources/regression/genc/valid/AbsArray.scala b/src/test/resources/regression/genc/valid/AbsArray.scala
new file mode 100644
index 0000000000000000000000000000000000000000..581684e7c50d6034e751c152be9afd185e227e73
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/AbsArray.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object AbsArray {
+ def main = {
+ val a = Array(0, -1, 2, -3)
+
+ def abs() {
+ require(a.length < 10000)
+
+ var i = 0;
+ (while (i < a.length && i < 10000) {
+ a(i) = if (a(i) < 0) -a(i) else a(i)
+ i = i + 1
+ }) invariant (i >= 0 && i <= 10000)
+ }
+
+ abs()
+
+ a(0) + a(1) - 1 + a(2) - 2 + a(3) - 3 // == 0
+ } ensuring { _ == 0 }
+}
+
+
diff --git a/src/test/resources/regression/genc/valid/CaseClass.scala b/src/test/resources/regression/genc/valid/CaseClass.scala
new file mode 100644
index 0000000000000000000000000000000000000000..83f5988594336f12e67ca63980334a747fcadbb2
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/CaseClass.scala
@@ -0,0 +1,20 @@
+import leon.lang._
+
+object CaseClass {
+
+ case class Color(r: Int, g: Int, b: Int)
+
+ def red = Color(0, 255, 0)
+ def cyan = Color(0, 255, 255)
+
+ def sub(c: Color, d: Color) = Color(c.r - d.r, c.g - d.g, c.b - d.b)
+
+ def main = {
+ val c = red
+ val d = cyan
+ val z = sub(c, d).g
+ z
+ } ensuring { _ == 0 }
+
+}
+
diff --git a/src/test/resources/regression/genc/valid/ExpressionOrder.scala b/src/test/resources/regression/genc/valid/ExpressionOrder.scala
new file mode 100644
index 0000000000000000000000000000000000000000..21ea9766dffad887414d56fb3c281934ea429f1d
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/ExpressionOrder.scala
@@ -0,0 +1,153 @@
+import leon.lang._
+
+object ExpressionOrder {
+ case class Pixel(rgb: Int)
+ case class Matrix(data: Array[Int], w: Int, h: Int)
+
+ def void = ()
+
+ def fun = 0xffffff
+ def foo = 4
+ def bar(i: Int) = i * 2
+ def baz(i: Int, j: Int) = bar(i) - bar(j)
+
+ def syntaxCheck(i: Int) {
+ val p = Pixel(fun)
+ val m = Matrix(Array(0, 1, 2, 3), 2, 2)
+
+ val z = baz(foo, bar(foo))
+ val a = Array(0, 1, foo / 2, 3, bar(2), z / 1)
+
+ val t = (true, foo, bar(a(0)))
+
+ val a2 = Array.fill(4)(2)
+ val a3 = Array.fill(if (i <= 0) 1 else i)(bar(i))
+ val b = Array(1, 2, 0)
+ b(1) = if (bar(b(1)) % 2 == 0) 42 else 58
+
+ def f1 = (if (i < 0) a else b)(0)
+ def f2 = (if (i < 0) a else b).length
+
+ //def f3 = (if (i < 0) a else b)(0) = 0 // <- not supported
+
+ val c = (0, true, 2)
+ val d = (if (i > 0) i else -i, false, 0)
+
+ def f4 = (if (i < 0) d else c)._2 // expression result unused
+ }
+
+ def main = {
+ bool2int(test0(false), 1) +
+ bool2int(test1(42), 2) +
+ bool2int(test2(58), 4) +
+ bool2int(test3(false), 8) +
+ bool2int(test4(false), 16) +
+ bool2int(test6, 32) +
+ bool2int(test7, 64) +
+ bool2int(test8, 128)
+ } ensuring { _ == 0 }
+
+ def test0(b: Boolean) = {
+ val f = b && !b // == false
+
+ var c = 0
+
+ val x = f && { c = 1; true }
+
+ c == 0
+ }.holds
+
+ def test1(i: Int) = {
+ require(i > 0)
+
+ val j = i / i * 3 // == 3
+
+ var c = 0
+ val x = { c = c + 3; j } + { c = c + 1; j } * { c = c * 2; j }
+
+ c == 8 && j == 3 && x == 12
+ }.holds
+
+ def test2(i: Int) = {
+ var c = 0;
+ val x = if (i < 0) { c = 1; -i } else { c = 2; i }
+
+ if (i < 0) c == 1
+ else c == 2
+ }.holds
+
+ def test3(b: Boolean) = {
+ val f = b && !b // == false
+
+ var c = 0
+ val x = f || { c = 1; true } || { c = 2; false }
+
+ c == 1
+ }.holds
+
+ def test4(b: Boolean) = {
+ var i = 10
+ var c = 0
+
+ val f = b && !b // == false
+ val t = b || !b // == true
+
+ // The following condition is executed 11 times,
+ // and only during the last execution is the last
+ // operand evaluated
+ while ({ c = c + 1; t } && i > 0 || { c = c * 2; f }) {
+ i = i - 1
+ }
+
+ i == 0 && c == 22
+ }.holds
+
+ def test5(b: Boolean) = {
+ val f = b && !b // == false
+
+ var c = if (f) 0 else -1
+
+ c = c + (if (f) 0 else 1)
+
+ c == 0
+ }.holds
+
+ def test6 = {
+ val a = Array(0, 1, 2, 3, 4)
+
+ def rec(b: Boolean, i: Int): Boolean = {
+ require(i >= 0 && i < 2147483647) // 2^31 - 1
+
+ if (i + 1 < a.length) rec(if (a(i) < a(i + 1)) b else false, i + 1)
+ else b
+ }
+
+ rec(true, 0)
+ }.holds
+
+ def test7 = {
+ var c = 1
+
+ val a = Array(0, 1, 2, 3, 4)
+
+ a(if(a(0) == 0) { c = c + 1; 0 } else { c = c + 2; 1 }) = { c = c * 2; -1 }
+
+ c == 4
+ }.holds
+
+ def test8 = {
+ var x = 0
+
+ def bar(y: Int) = {
+ def fun(z: Int) = 1 * x * (y + z)
+
+ fun(3)
+ }
+
+ bar(2) == 0
+ }.holds
+
+ def bool2int(b: Boolean, f: Int) = if (b) 0 else f;
+}
+
+
diff --git a/src/test/resources/regression/genc/valid/IntegralColor.scala b/src/test/resources/regression/genc/valid/IntegralColor.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c64cb0fa18ac395dad37b2a8a8ffa7fa187872a2
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/IntegralColor.scala
@@ -0,0 +1,175 @@
+import leon.lang._
+
+object IntegralColor {
+
+ def isValidComponent(x: Int) = x >= 0 && x <= 255
+
+ def getRed(rgb: Int): Int = {
+ (rgb & 0x00FF0000) >> 16
+ } ensuring isValidComponent _
+
+ def getGreen(rgb: Int): Int = {
+ (rgb & 0x0000FF00) >> 8
+ } ensuring isValidComponent _
+
+ def getBlue(rgb: Int): Int = {
+ rgb & 0x000000FF
+ } ensuring isValidComponent _
+
+ def getGray(rgb: Int): Int = {
+ (getRed(rgb) + getGreen(rgb) + getBlue(rgb)) / 3
+ } ensuring isValidComponent _
+
+ def testColorSinglePixel: Boolean = {
+ val color = 0x20C0FF
+
+ 32 == getRed(color) && 192 == getGreen(color) &&
+ 255 == getBlue(color) && 159 == getGray(color)
+ }.holds
+
+ case class Color(r: Int, g: Int, b: Int)
+
+ def getColor(rgb: Int) = Color(getRed(rgb), getGreen(rgb), getBlue(rgb))
+
+ /*
+ *case class Image(width: Int, height: Int, buffer: Array[Int]) {
+ * // currently not enforced:
+ * require(width <= 1000 && height <= 1000 && buffer.length == width * height)
+ *}
+ */
+
+ def matches(value: Array[Int], expected: Array[Int]): Boolean = {
+ require(value.length == expected.length)
+
+ var test = true
+ var idx = 0
+ (while (idx < value.length) {
+ test = test && value(idx) == expected(idx)
+ idx = idx + 1
+ }) invariant { idx >= 0 && idx <= value.length }
+
+ test
+ }
+
+ def testColorWholeImage: Boolean = {
+ val WIDTH = 2
+ val HEIGHT = 2
+
+ /*
+ *val source = Image(WIDTH, HEIGHT, Array(0x20c0ff, 0x123456, 0xffffff, 0x000000))
+ *val expected = Image(WIDTH, HEIGHT, Array(159, 52, 255, 0)) // gray convertion
+ *val gray = Image(WIDTH, HEIGHT, Array.fill(4)(0))
+ */
+
+ val source = Array(0x20c0ff, 0x123456, 0xffffff, 0x000000)
+ val expected = Array(159, 52, 255, 0) // gray convertion
+ val gray = Array.fill(4)(0)
+
+ // NOTE: Cannot define a toGray function as XLang doesn't allow mutating
+ // arguments and GenC doesn't allow returning arrays
+
+ var idx = 0
+ (while (idx < WIDTH * HEIGHT) {
+ gray(idx) = getGray(source(idx))
+ idx = idx + 1
+ }) invariant { idx >= 0 && idx <= WIDTH * HEIGHT && gray.length == WIDTH * HEIGHT }
+ // NB: the last invariant is very important -- without it the verification times out
+
+ matches(gray, expected)
+ }.holds
+
+ // Only for square kernels
+ case class Kernel(size: Int, buffer: Array[Int])
+
+ def isKernelValid(kernel: Kernel): Boolean =
+ kernel.size > 0 && kernel.size < 1000 && kernel.size % 2 == 1 &&
+ kernel.buffer.length == kernel.size * kernel.size
+
+ def applyFilter(gray: Array[Int], size: Int, idx: Int, kernel: Kernel): Int = {
+ require(size > 0 && size < 1000 &&
+ gray.length == size * size &&
+ idx >= 0 && idx < gray.length &&
+ isKernelValid(kernel))
+
+ def up(x: Int): Int = {
+ if (x < 0) 0 else x
+ } ensuring { _ >= 0 }
+
+ def down(x: Int): Int = {
+ if (x >= size) size - 1 else x
+ } ensuring { _ < size }
+
+ def fix(x: Int): Int = {
+ down(up(x))
+ } ensuring { res => res >= 0 && res < size }
+
+ def at(row: Int, col: Int): Int = {
+ val r = fix(row)
+ val c = fix(col)
+
+ gray(r * size + c)
+ }
+
+ val mid = kernel.size / 2
+
+ val i = idx / size
+ val j = idx % size
+
+ var res = 0
+ var p = -mid
+ (while (p <= mid) {
+ var q = -mid
+
+ (while (q <= mid) {
+ val krow = p + mid
+ val kcol = q + mid
+
+ assert(krow >= 0 && krow < kernel.size)
+ assert(kcol >= 0 && kcol < kernel.size)
+
+ val kidx = krow * kernel.size + kcol
+
+ res += at(i + p, j + q) * kernel.buffer(kidx)
+
+ q = q + 1
+ }) invariant { q >= -mid && q <= mid + 1 }
+
+ p = p + 1
+ }) invariant { p >= -mid && p <= mid + 1 }
+
+ res
+ }
+
+ def testFilterConvolutionSmooth: Boolean = {
+ val gray = Array(127, 255, 51, 0)
+ val expected = Array(124, 158, 76, 73)
+ val size = 2 // grey is size x size
+
+ // NOTE: Cannot define a `smoothed` function as XLang doesn't allow mutating
+ // arguments and GenC doesn't allow returning arrays
+
+ val kernel = Kernel(3, Array(1, 1, 1,
+ 1, 2, 1,
+ 1, 1, 1))
+
+ val smoothed = Array.fill(gray.length)(0)
+ assert(smoothed.length == expected.length)
+
+ var idx = 0;
+ (while (idx < smoothed.length) {
+ smoothed(idx) = applyFilter(gray, size, idx, kernel) / 10
+ idx = idx + 1
+ }) invariant { idx >= 0 && idx <= smoothed.length && smoothed.length == gray.length }
+
+ matches(smoothed, expected)
+ }.holds
+
+
+ def main: Int = {
+ if (testColorSinglePixel && testColorWholeImage && testFilterConvolutionSmooth) 0
+ else 1
+ } ensuring { _ == 0 }
+
+}
+
+
diff --git a/src/test/resources/regression/genc/valid/RecursionAndNestedFunctions.scala b/src/test/resources/regression/genc/valid/RecursionAndNestedFunctions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..25f69538a19412bd8ae8267446d4eb5f05f6247b
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/RecursionAndNestedFunctions.scala
@@ -0,0 +1,37 @@
+import leon.lang._
+
+object RecursionAndNestedFunctions {
+
+ // Complex way to return i
+ def zzz(i: Int): Int = {
+ val x = 0
+
+ def rec(j: Int): Int = {
+ if (i - x == j) i
+ else if (j > i) rec(j - 1)
+ else rec(j + 1)
+ } ensuring { _ == i }
+
+ rec(4)
+ } ensuring { _ == i }
+
+
+ // Complex way to compute 100 + 2 * i
+ def foo(i: Int) = {
+ var j = i
+ def bar(x: Int) = {
+ //j = j - 1 <- not supported by leon
+ val y = x + i
+ def baz(z: Int) = z + y + i
+ //j = j + 1 <- not supported by leon
+ baz(42)
+ }
+ bar(58) + j - i
+ } ensuring { _ == 100 + 2 * i }
+
+ def main() = {
+ foo(2) - zzz(104)
+ } ensuring { _ == 0 }
+
+}
+
diff --git a/src/test/resources/regression/genc/valid/TupleArray.scala b/src/test/resources/regression/genc/valid/TupleArray.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1f2354e0613430fb95a995da6a741dda3939b143
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/TupleArray.scala
@@ -0,0 +1,25 @@
+import leon.lang._
+
+object TupleArray {
+ def exists(av: (Array[Int], Int)): Boolean = {
+ require(av._1.length < 10000)
+
+ var i = 0
+ var found = false
+ (while (!found && i < av._1.length) {
+ found = av._1(i) == av._2
+ i = i + 1
+ }) invariant (i >= 0 && i < 10000)
+ found
+ }
+
+ def main = {
+ val a = Array(0, 1, 5, -5, 9)
+ val e1 = exists((a, 0))
+ val e2 = exists((a, -1))
+ if (e1 && !e2) 0
+ else -1
+ } ensuring { _ == 0 }
+
+}
+
diff --git a/src/test/resources/regression/termination/valid/QuickSort.scala b/src/test/resources/regression/termination/valid/QuickSort.scala
index e356bdc2a2b8a1c412e90a3033ae269faf6d7df0..d4fb11ea68a7e8c96f056754c24be2e9a5f9ef4e 100644
--- a/src/test/resources/regression/termination/valid/QuickSort.scala
+++ b/src/test/resources/regression/termination/valid/QuickSort.scala
@@ -1,5 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.annotation._
import leon.lang._
object QuickSort {
@@ -29,7 +30,7 @@ object QuickSort {
case Nil() => bList
case _ => rev_append(reverse(aList),bList)
}
-
+
def greater(n:Int,list:List) : List = list match {
case Nil() => Nil()
case Cons(x,xs) => if (n < x) Cons(x,greater(n,xs)) else greater(n,xs)
@@ -51,6 +52,7 @@ object QuickSort {
case Cons(x,xs) => append(append(quickSort(smaller(x,xs)),Cons(x,equals(x,xs))),quickSort(greater(x,xs)))
}) ensuring(res => contents(res) == contents(list)) // && is_sorted(res))
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/src/test/resources/regression/termination/valid/SimpInterpret.scala b/src/test/resources/regression/termination/valid/SimpInterpret.scala
index 76fcd4145509440741b521bf26fa97dcc9af2dd9..c5255506dbb0b20308a0210ea3268a9432abaa14 100644
--- a/src/test/resources/regression/termination/valid/SimpInterpret.scala
+++ b/src/test/resources/regression/termination/valid/SimpInterpret.scala
@@ -1,15 +1,15 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-//import leon.annotation._
+import leon.annotation._
import leon.lang._
object Interpret {
- abstract class BoolTree
+ abstract class BoolTree
case class Eq(t1 : IntTree, t2 : IntTree) extends BoolTree
case class And(t1 : BoolTree, t2 : BoolTree) extends BoolTree
case class Not(t : BoolTree) extends BoolTree
- abstract class IntTree
+ abstract class IntTree
case class Const(c:Int) extends IntTree
case class Var() extends IntTree
case class Plus(t1 : IntTree, t2 : IntTree) extends IntTree
@@ -22,7 +22,7 @@ object Interpret {
}
def beval(t:BoolTree, x0 : Int) : Boolean = {
- t match {
+ t match {
case Less(t1, t2) => ieval(t1,x0) < ieval(t2,x0)
case Eq(t1, t2) => ieval(t1,x0) == ieval(t2,x0)
case And(t1, t2) => beval(t1,x0) && beval(t2,x0)
@@ -62,6 +62,7 @@ object Interpret {
!treeBad(If(Less(Const(0),Var()), Var(), Minus(Const(0),Var())))
}.holds
+ @ignore
def main(args : Array[String]) {
thereIsGoodTree()
}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
index 05889fcb726ff88728959172f2127128831802c2..3252c9acf942d682f3cef10cc358cb7c837b44bb 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
@@ -34,7 +34,7 @@ object InsertionSort {
case Nil() => true
case Cons(x, Nil()) => true
case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
+ }
/* Inserting element 'e' into a sorted list 'l' produces a sorted list with
* the expected content and size */
@@ -43,8 +43,8 @@ object InsertionSort {
l match {
case Nil() => Cons(e,Nil())
case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -54,11 +54,12 @@ object InsertionSort {
def sort(l: List): List = (l match {
case Nil() => Nil()
case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
+ }) ensuring(res => contents(res) == contents(l)
&& isSorted(res)
&& size(res) == size(l)
)
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
index 7c89f364600e95edb8c0f266cb5e22f65d1adbea..0ec78ff0d3050b6333e3fd1e229dd57f2e72cea2 100644
--- a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
@@ -34,7 +34,7 @@ object InsertionSort {
case Nil() => true
case Cons(x, Nil()) => true
case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
+ }
/* Inserting element 'e' into a sorted list 'l' produces a sorted list with
* the expected content and size */
@@ -43,8 +43,8 @@ object InsertionSort {
l match {
case Nil() => Cons(e,Nil())
case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -54,11 +54,12 @@ object InsertionSort {
def sort(l: List): List = (l match {
case Nil() => Nil()
case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
+ }) ensuring(res => contents(res) == contents(l)
&& isSorted(res)
&& size(res) == size(l)
)
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/src/test/scala/leon/genc/GenCSuite.scala b/src/test/scala/leon/genc/GenCSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..df6d30e5c0869cb6f05ba08195fab4ed73593d89
--- /dev/null
+++ b/src/test/scala/leon/genc/GenCSuite.scala
@@ -0,0 +1,219 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package genc
+
+import leon.test.LeonRegressionSuite
+
+import leon.frontends.scalac.ExtractionPhase
+import leon.regression.verification.XLangVerificationSuite
+import leon.purescala.Definitions.Program
+import leon.utils.{ PreprocessingPhase, UniqueCounter }
+
+import scala.concurrent._
+import ExecutionContext.Implicits.global
+import scala.sys.process._
+
+import org.scalatest.{ Args, Status }
+
+import java.io.ByteArrayInputStream
+import java.nio.file.{ Files, Path }
+
+class GenCSuite extends LeonRegressionSuite {
+
+ private val testDir = "regression/genc/"
+ private lazy val tmpDir = Files.createTempDirectory("genc")
+ private val ccflags = "-std=c99 -g -O0"
+ private val maxExecutionTime = 2 // seconds
+
+ private val counter = new UniqueCounter[Unit]
+ counter.nextGlobal // Start with 1
+
+ private case class ExtendedContext(leon: LeonContext, tmpDir: Path, progName: String)
+
+ // Tests are run as follows:
+ // - before mkTest is run, all valid test are verified using XLangVerificationSuite
+ // - The classic ExtractionPhase & PreprocessingPhase are run on all input files
+ // (this way the libraries are evaluated only once)
+ // - A Program is constructed for each input file
+ // - At this point no error should have occurred or something would be wrong
+ // with the extraction phases
+ // - For each Program P:
+ // + if P is expected to be convertible to C, then we make sure that:
+ // * the GenerateCPhase run without trouble,
+ // * the generated C code compiles using a C99 compiler without error,
+ // * and that, when run, the exit code is 0
+ // + if P is expected to be non-convertible to C, then we make sure that:
+ // * the GenerateCPhase fails
+ private def mkTest(files: List[String], cat: String)(block: (ExtendedContext, Program) => Unit) = {
+ val extraction =
+ ExtractionPhase andThen
+ new PreprocessingPhase(true, true)
+
+ val ctx = createLeonContext(files:_*)
+
+ try {
+ val (_, ast) = extraction.run(ctx, files)
+
+ val programs = {
+ val (user, lib) = ast.units partition { _.isMainUnit }
+ user map ( u => Program(u :: lib) )
+ }
+
+ for { prog <- programs } {
+ val name = prog.units.head.id.name
+ val ctx = createLeonContext(s"--o=$tmpDir/$name.c")
+ val xCtx = ExtendedContext(ctx, tmpDir, name)
+
+ val displayName = s"$cat/$name.scala"
+ val index = counter.nextGlobal
+
+ test(f"$index%3d: $displayName") {
+ block(xCtx, prog)
+ }
+ }
+ } catch {
+ case fe: LeonFatalError =>
+ test("Compilation") {
+ fail(ctx, "Unexpected fatal error while setting up tests", fe)
+ }
+ }
+ }
+
+ // Run a process with a timeout and return the status code
+ private def runProcess(pb: ProcessBuilder): Int = runProcess(pb.run)
+ private def runProcess(p: Process): Int = {
+ val f = Future(blocking(p.exitValue()))
+ try {
+ Await.result(f, duration.Duration(maxExecutionTime, "sec"))
+ } catch {
+ case _: TimeoutException =>
+ p.destroy()
+ throw LeonFatalError("timeout reached")
+ }
+ }
+
+ // Determine which C compiler is available
+ private def detectCompiler: Option[String] = {
+ val testCode = "int main() { return 0; }"
+ val testBinary = s"$tmpDir/test"
+
+ // NOTE this code might print error on stderr when a non-existing compiler
+ // is used. It seems that even with a special ProcessLogger the RuntimeException
+ // is printed for some reason.
+
+ def testCompiler(cc: String): Boolean = try {
+ def input = new ByteArrayInputStream(testCode.getBytes())
+ val process = s"$cc $ccflags -o $testBinary -xc -" #< input #&& s"$testBinary"
+ runProcess(process) == 0
+ } catch {
+ case _: java.lang.RuntimeException => false
+ }
+
+ val knownCompiler = "cc" :: "clang" :: "gcc" :: "mingw" :: Nil
+ // Note that VS is not in the list as we cannot specify C99 dialect
+
+ knownCompiler find testCompiler
+ }
+
+ private def convert(xCtx: ExtendedContext)(prog: Program) = {
+ try {
+ GenerateCPhase(xCtx.leon, prog)
+ } catch {
+ case fe: LeonFatalError =>
+ fail(xCtx.leon, "Convertion to C unexpectedly failed", fe)
+ }
+ }
+
+ private def saveToFile(xCtx: ExtendedContext)(cprog: CAST.Prog) = {
+ CFileOutputPhase(xCtx.leon, cprog)
+ }
+
+ private def compile(xCtx: ExtendedContext, cc: String)(unused: Unit) = {
+ val basename = s"${xCtx.tmpDir}/${xCtx.progName}"
+ val sourceFile = s"$basename.c"
+ val compiledProg = basename
+
+ val process = Process(s"$cc $ccflags $sourceFile -o $compiledProg")
+ val status = runProcess(process)
+
+ assert(status == 0, "Compilation of converted program failed")
+ }
+
+ private def evaluate(xCtx: ExtendedContext)(unused: Unit) = {
+ val compiledProg = s"${xCtx.tmpDir}/${xCtx.progName}"
+
+ // TODO memory limit
+ val process = Process(compiledProg)
+
+ val status = runProcess(process)
+ assert(status == 0, s"Evaluation of converted program failed with status [$status]")
+ }
+
+ private def forEachFileIn(cat: String)(block: (ExtendedContext, Program) => Unit) {
+ val fs = filesInResourceDir(testDir + cat, _.endsWith(".scala")).toList
+
+ fs foreach { file =>
+ assert(file.exists && file.isFile && file.canRead,
+ s"Benchmark ${file.getName} is not a readable file")
+ }
+
+ val files = fs map { _.getPath }
+
+ mkTest(files, cat)(block)
+ }
+
+ protected def testDirectory(cc: String, dir: String) = forEachFileIn(dir) { (xCtx, prog) =>
+ val converter = convert(xCtx) _
+ val saver = saveToFile(xCtx) _
+ val compiler = compile(xCtx, cc) _
+ val evaluator = evaluate(xCtx) _
+
+ val pipeline = converter andThen saver andThen compiler andThen evaluator
+
+ pipeline(prog)
+ }
+
+ protected def testValid(cc: String) = testDirectory(cc, "valid")
+ protected def testUnverified(cc: String) = testDirectory(cc, "unverified");
+
+ protected def testInvalid() = forEachFileIn("invalid") { (xCtx, prog) =>
+ intercept[LeonFatalError] {
+ GenerateCPhase(xCtx.leon, prog)
+ }
+ }
+
+ class AltVerificationSuite(override val testDir: String) extends XLangVerificationSuite {
+ override def testAll() = testValid() // Test only the valid ones
+
+ override def suiteName = "Verification Suite For GenC"
+
+ // Add a timeout for the verification
+ override val optionVariants = List(List("--solvers=smt-z3,ground"))
+ }
+
+ // Run verification suite as a nested suite
+ override def nestedSuites = {
+ // Use our test dir and not the one from XLangVerificationSuite
+ scala.collection.immutable.IndexedSeq(new AltVerificationSuite(testDir))
+ }
+
+ protected def testAll() = {
+ // Set C compiler according to the platform we're currently running on
+ detectCompiler match {
+ case Some(cc) =>
+ testValid(cc)
+ testUnverified(cc)
+ case None =>
+ test("dectecting C compiler") { fail("no C compiler found") }
+ }
+
+ testInvalid()
+ }
+
+ override def run(testName: Option[String], args: Args): Status = {
+ testAll()
+ super.run(testName, args)
+ }
+}
+
diff --git a/src/test/scala/leon/regression/verification/NewSolversSuite.scala b/src/test/scala/leon/regression/verification/NewSolversSuite.scala
index 15e02a693988e44be555c5e954be65cab4203086..5a340d1f870e019f33460fb6e386c50e58fbcbff 100644
--- a/src/test/scala/leon/regression/verification/NewSolversSuite.scala
+++ b/src/test/scala/leon/regression/verification/NewSolversSuite.scala
@@ -5,6 +5,7 @@ package leon.regression.verification
import _root_.smtlib.interpreters._
import leon._
import leon.verification.VerificationPhase
+import leon.solvers.SolverFactory
/* @EK: Disabled for now as many tests fail
class NewSolversSuite extends VerificationSuite {
@@ -14,21 +15,9 @@ class NewSolversSuite extends VerificationSuite {
val pipeBack = AnalysisPhase
val optionVariants: List[List[String]] = {
- val isCVC4Available = try {
- CVC4Interpreter.buildDefault.free()
- true
- } catch {
- case e: java.io.IOException =>
- false
- }
-
- val isZ3Available = try {
- Z3Interpreter.buildDefault.free()
- true
- } catch {
- case e: java.io.IOException =>
- false
- }
+ val isCVC4Available = SolverFactory.hasCVC4
+
+ val isZ3Available = SolverFactory.hasZ3
(
if (isCVC4Available)
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index b23fb0c4e3516121a1489752ed89dcb0835ee2d2..f2ae97880694baac498b94570f81beb1c21c422f 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -81,7 +81,7 @@ trait VerificationSuite extends LeonRegressionSuite {
private[verification] def forEachFileIn(cat: String)(block: Output => Unit) {
val fs = filesInResourceDir(testDir + cat, _.endsWith(".scala")).toList
- fs foreach { file =>
+ fs foreach { file =>
assert(file.exists && file.isFile && file.canRead,
s"Benchmark ${file.getName} is not a readable file")
}
diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
index 8511ebfea95d4d6a412d82922ffb1e6fb870d312..6fe7b07408500929063b4f57f24e1147a6cfce35 100644
--- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
@@ -3,19 +3,14 @@
package leon.regression.verification
import smtlib.interpreters.Z3Interpreter
+import leon.solvers.SolverFactory
// If you add another regression test, make sure it contains exactly one object, whose name matches the file name.
// This is because we compile all tests from each folder together.
class XLangVerificationSuite extends VerificationSuite {
val optionVariants: List[List[String]] = {
- val isZ3Available = try {
- Z3Interpreter.buildDefault.free()
- true
- } catch {
- case e: java.io.IOException =>
- false
- }
+ val isZ3Available = SolverFactory.hasZ3
List(
List(),
@@ -30,3 +25,4 @@ class XLangVerificationSuite extends VerificationSuite {
val testDir: String = "regression/verification/xlang/"
override val desugarXLang = true
}
+
diff --git a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
index 569eb95df2f7f66a05d7a825765adb6123b4d854..6c450c1c8613f74c5a6679aaaf6035f59e593e66 100644
--- a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
@@ -4,6 +4,7 @@ package leon.regression.verification
package purescala
import smtlib.interpreters.{CVC4Interpreter, Z3Interpreter}
+import leon.solvers.SolverFactory
// If you add another regression test, make sure it contains one object whose name matches the file name
// This is because we compile all tests from each folder together.
@@ -11,21 +12,9 @@ abstract class PureScalaVerificationSuite extends VerificationSuite {
val testDir = "regression/verification/purescala/"
- val isZ3Available = try {
- Z3Interpreter.buildDefault.free()
- true
- } catch {
- case e: java.io.IOException =>
- false
- }
+ val isZ3Available = SolverFactory.hasZ3
- val isCVC4Available = try {
- CVC4Interpreter.buildDefault.free()
- true
- } catch {
- case e: java.io.IOException =>
- false
- }
+ val isCVC4Available = SolverFactory.hasCVC4
val opts: List[List[String]] = {
List(
diff --git a/src/test/scala/leon/unit/utils/GraphsSuite.scala b/src/test/scala/leon/unit/utils/GraphsSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..984a427fafa5632aacacd2d667f5f1d0dec7a435
--- /dev/null
+++ b/src/test/scala/leon/unit/utils/GraphsSuite.scala
@@ -0,0 +1,275 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.unit.utils
+
+import leon.test._
+import leon.purescala.Common._
+import leon.utils.Graphs._
+
+class GraphsSuite extends LeonTestSuite {
+ abstract class Node
+ case object A extends Node
+ case object B extends Node
+ case object C extends Node
+ case object D extends Node
+ case object E extends Node
+ case object F extends Node
+ case object G extends Node
+ case object H extends Node
+
+ import scala.language.implicitConversions
+
+ implicit def tToEdge(t: (Node, Node)): SimpleEdge[Node] = {
+ SimpleEdge(t._1, t._2)
+ }
+
+ def g1 = {
+ var g = new DiGraph[Node, SimpleEdge[Node]]()
+
+ g ++= Set(A, B, C, D)
+
+ g += A -> B
+ g += B -> A
+
+ g += B -> C
+
+ g += C -> D
+ g += D -> C
+
+ // A D
+ // ↕ ↕
+ // B → C
+
+ g
+ }
+
+ def g2 = {
+ var g = new DiGraph[Node, SimpleEdge[Node]]()
+
+ g ++= Set(A, B, C, D)
+
+ g += A -> B
+ g += B -> B
+ g += B -> C
+ g += C -> D
+
+ // A → B → C → D
+ // ↻
+
+ g
+ }
+
+ def g3 = {
+ var g = new DiGraph[Node, SimpleEdge[Node]]()
+
+ g ++= Set(A, B, C, D, E, F, G, H)
+
+ g += A -> B
+ g += B -> C
+ g += C -> D
+
+ g += E -> A
+ g += A -> F
+ g += B -> F
+ g += F -> E
+ g += F -> G
+
+ g += C -> G
+ g += G -> C
+ g += H -> G
+
+
+ // A → B → C → D
+ // ↑↘ ↓ ↕
+ // E ← F → G ← H
+
+ g
+ }
+
+ def g4 = {
+ var g = new DiGraph[Node, SimpleEdge[Node]]()
+
+ g ++= Set(A, B, C, D, E, F, G, H)
+
+ g += A -> B
+ g += B -> C
+ g += C -> D
+
+ g += A -> F
+ g += B -> F
+ g += F -> E
+ g += F -> G
+
+ g += C -> G
+ g += H -> G
+
+
+ // A → B → C → D
+ // ↘ ↓ ↓
+ // E ← F → G ← H
+
+ g
+ }
+
+ def g5 = {
+ var g = new DiGraph[Node, SimpleEdge[Node]]()
+
+ g ++= Set(A, B, C, D, E, F, G, H)
+
+ g += A -> B
+ g += B -> C
+
+ g += A -> D
+ g += D -> E
+
+
+ // A → B → C F G H
+ // ↘
+ // D → E
+
+ g
+ }
+
+
+ test("Graphs basic 1") { ctx =>
+ val g = g1
+ assert(g.N.size === 4)
+ assert(g.E.size === 5)
+
+ assert(g.outEdges(A) === Set(SimpleEdge(A, B)))
+ assert(g.outEdges(B) === Set(SimpleEdge(B, A), SimpleEdge(B, C)))
+
+ assert(g.inEdges(B) === Set(SimpleEdge(A, B)))
+ assert(g.inEdges(C) === Set(SimpleEdge(B, C), SimpleEdge(D, C)))
+
+ assert(g.edgesBetween(A, B).size === 1)
+ }
+
+ test("Graphs sinks/sources 1") { ctx =>
+ val g = g1
+
+ assert(g.sources == Set())
+ assert(g.sinks == Set())
+ }
+
+ test("Graphs sinks/sources 2") { ctx =>
+ val g = g2
+
+ assert(g.N.size === 4)
+ assert(g.E.size === 4)
+
+ assert(g.sources == Set(A))
+ assert(g.sinks == Set(D))
+ }
+
+ test("Graphs SCC 1") { ctx =>
+ val g = g1
+
+ val gs = g.stronglyConnectedComponents
+
+ assert(gs.N.size === 2)
+ assert(gs.E.size === 1)
+ }
+
+ test("Graphs SCC 2") { ctx =>
+ val g = g2
+
+ val gs = g.stronglyConnectedComponents
+
+ assert(gs.N.size === 4)
+ assert(gs.E.size === 3)
+ }
+
+ test("Graphs SCC 3") { ctx =>
+ val g = g3
+
+ val gs = g.stronglyConnectedComponents
+
+ assert(gs.N === Set(Set(A, B, E, F), Set(C, G), Set(D), Set(H)))
+ }
+
+ def assertBefore[T](s: Seq[T])(n1: T, n2: T) {
+ assert(s.indexOf(n1) < s.indexOf(n2), s"Node '$n1' should be before '$n2'");
+ }
+
+ test("Graphs top-sort 1") { ctx =>
+ val g = g4
+
+
+ val seq = g.topSort
+
+ val before = assertBefore(seq)_
+
+ before(A, B)
+ before(B, F)
+ before(A, C)
+ }
+
+ test("Graphs top-sort 2 (cyclic graph fails)") { ctx =>
+ val g = g1
+
+ intercept[IllegalArgumentException] {
+ g.topSort
+ }
+ }
+
+ test("Graphs top-sort 3 (SCC is acyclic)") { ctx =>
+ val g = g3
+
+ val gs = g.stronglyConnectedComponents
+
+ val c1: Set[Node] = Set(A, B, E, F)
+ val c2: Set[Node] = Set(C, G)
+ val c3: Set[Node] = Set(D)
+ val c4: Set[Node] = Set(H)
+
+
+ val ns = gs.topSort
+
+ val before = assertBefore(ns)_
+ before(c1, c2)
+ before(c2, c3)
+ before(c4, c2)
+ }
+
+ test("Graphs DFS") { ctx =>
+ val g = g5
+
+ var visited = List[Node]()
+ g.depthFirstSearch(A) { n =>
+ visited ::= n
+ }
+ visited = visited.reverse
+
+ def isBefore(a: Node, b: Node) = visited.indexOf(a) < visited.indexOf(b)
+
+ assert(!isBefore(B, D) || isBefore(C, E))
+ assert(!isBefore(D, B) || isBefore(E, C))
+ }
+
+ test("Graphs BFS") { ctx =>
+ val g = g5
+
+ var visited = List[Node]()
+ g.breadthFirstSearch(A) { n =>
+ visited ::= n
+ }
+ visited = visited.reverse
+
+ def isBefore(a: Node, b: Node) = visited.indexOf(a) < visited.indexOf(b)
+
+ assert(isBefore(B, E))
+ assert(isBefore(D, C))
+ }
+
+ test("Graphs pred/succ 1") { ctx =>
+ val g = g2
+
+ assert(g.succ(B) == Set(B, C))
+ assert(g.pred(B) == Set(B, A))
+
+ assert(g.transitiveSucc(B) == Set(B, C, D))
+ assert(g.transitivePred(B) == Set(A, B))
+ assert(g.transitivePred(C) == Set(A, B))
+ }
+}
diff --git a/testcases/repair/DaysToYears/DaysToYears.scala b/testcases/repair/DaysToYears/DaysToYears.scala
index bb6c518b3b743ea02d0188c8a9b1a802e6685e16..3a71a49602ff9d818df2cf2e1d2476a78f9e0b3a 100644
--- a/testcases/repair/DaysToYears/DaysToYears.scala
+++ b/testcases/repair/DaysToYears/DaysToYears.scala
@@ -1,10 +1,11 @@
+import leon.annotation._
import leon.lang._
object DaysToYears {
val base : Int = 1980
-
+
def isLeapYear(y : Int): Boolean = y % 4 == 0
-
+
def daysToYears(days : Int): Int = {
require(days > 0)
daysToYears1(base, days)._1
@@ -17,16 +18,17 @@ object DaysToYears {
else if (days > 365 && !isLeapYear(year))
daysToYears1(year + 1, days - 365)
else (year, days)
- } ensuring { res =>
+ } ensuring { res =>
res._2 <= 366 &&
- res._2 > 0 &&
+ res._2 > 0 &&
res._1 >= base &&
- (((year,days), res) passes {
+ (((year,days), res) passes {
case (1980, 366 ) => (1980, 366)
case (1980, 1000) => (1982, 269)
})
- }
+ }
+ @ignore
def main(args : Array[String]) = {
println(daysToYears1(base, 10593 ))
println(daysToYears1(base, 366 ))
diff --git a/testcases/repair/DaysToYears/DaysToYears1.scala b/testcases/repair/DaysToYears/DaysToYears1.scala
index 13eec09ae4ee1a611fc5a7d916ed92e061086112..1ef2d337989c7dc1a718637777d6e97726d7a276 100644
--- a/testcases/repair/DaysToYears/DaysToYears1.scala
+++ b/testcases/repair/DaysToYears/DaysToYears1.scala
@@ -1,10 +1,11 @@
+import leon.annotation._
import leon.lang._
object DaysToYears {
val base : Int = 1980
-
+
def isLeapYear(y : Int): Boolean = y % 4 == 0
-
+
def daysToYears(days : Int): Int = {
require(days > 0)
daysToYears1(base, days)._1
@@ -17,17 +18,18 @@ object DaysToYears {
else if (days > 365 && !isLeapYear(year))
daysToYears1(year, days - 365) // FIXME forgot +1
else (year, days)
- } ensuring { res =>
+ } ensuring { res =>
res._2 <= 366 &&
- res._2 > 0 &&
+ res._2 > 0 &&
res._1 >= base &&
- (((year,days), res) passes {
+ (((year,days), res) passes {
case (1999, 14 ) => (1999, 14)
case (1980, 366) => (1980, 366)
case (1981, 366) => (1982, 1)
})
- }
+ }
+ @ignore
def main(args : Array[String]) = {
println(daysToYears1(base, 10593 ))
println(daysToYears1(base, 366 ))
diff --git a/testcases/repair/DaysToYears/DaysToYears2.scala b/testcases/repair/DaysToYears/DaysToYears2.scala
index de0d31a707bda925004cca4dd3af1784995d0051..40396f05c6c3e40c4cfd0beccee02ed7d4c59553 100644
--- a/testcases/repair/DaysToYears/DaysToYears2.scala
+++ b/testcases/repair/DaysToYears/DaysToYears2.scala
@@ -1,10 +1,11 @@
+import leon.annotation._
import leon.lang._
object DaysToYears {
val base : Int = 1980
-
+
def isLeapYear(y : Int): Boolean = y % 4 == 0
-
+
def daysToYears(days : Int): Int = {
require(days > 0)
daysToYears1(base, days)._1
@@ -16,17 +17,18 @@ object DaysToYears {
daysToYears1(year + 1, days - 366) // TODO this branch cannot be solved although it is correct because it depends on the erroneous branch
else if (days > 365 && !isLeapYear(year))
daysToYears1(year + 1, days - 365)
- else (year + 1, days) // FIXME +1
- } ensuring { res =>
+ else (year + 1, days) // FIXME +1
+ } ensuring { res =>
res._2 <= 366 &&
- res._2 > 0 &&
+ res._2 > 0 &&
res._1 >= base &&
- (((year,days), res) passes {
+ (((year,days), res) passes {
case (1980, 366 ) => (1980, 366)
case (1980, 1000) => (1982, 269)
})
- }
+ }
+ @ignore
def main(args : Array[String]) = {
println(daysToYears1(base, 10593 ))
println(daysToYears1(base, 366 ))
diff --git a/testcases/runtime/SquareRoot.scala b/testcases/runtime/SquareRoot.scala
index 87b3e985a6209da18606c28ca189440043b6e25d..95bdf52f6c9e0967da3af474ba70cadc30e9cc45 100644
--- a/testcases/runtime/SquareRoot.scala
+++ b/testcases/runtime/SquareRoot.scala
@@ -1,3 +1,4 @@
+import leon.annotation._
import leon.lang._
import leon.lang.synthesis._
@@ -23,6 +24,7 @@ object SquareRoot {
}
}
+ @ignore
def main(a: Array[String]) {
isqrt2(42)
}
diff --git a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
index 64a8ae73ddd8553ff4ca364814aa880c41b503f8..3cf66229cb37d2c00e41ab63d0fbe4fb28aa4945 100644
--- a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
+++ b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
@@ -1,3 +1,4 @@
+import leon.annotation._
import leon.lang._
import leon.collection._
@@ -50,7 +51,7 @@ object BatchedQueue {
case Cons(_, xs) => checkf(xs, p.r)
}
}
- //
+ //
// def last(p: Queue): Int = {
// require(!isEmpty(p))
// p.r match {
@@ -66,6 +67,7 @@ object BatchedQueue {
(if (isEmpty(p)) true
else content(tail(res)) ++ Set(x) == content(tail(res))))
+ @ignore
def main(args: Array[String]): Unit = {
val pair = Queue(Cons(4, Nil), Cons(3, Nil))
diff --git a/testcases/verification/case-studies/Robot3po.scala b/testcases/verification/case-studies/Robot3po.scala
index 56709fc5555175ede38fac4f00ec6e772ecb9d7d..b189db5e98852b61f9463232d1036a5fa519a8aa 100644
--- a/testcases/verification/case-studies/Robot3po.scala
+++ b/testcases/verification/case-studies/Robot3po.scala
@@ -365,7 +365,7 @@ object Robot {
}
def validState(rs: RobotState)(implicit w: World): Boolean = {
-
+
// 6) Sensors have consistent data
val recentData = rs.ns.validData && rs.hs.validData
@@ -509,6 +509,7 @@ object Robot {
}
+ @ignore
def main(a: Array[String]): Unit = {
val map0 = """|XXXXXXXXX
|XR FF X
diff --git a/testcases/verification/compilation/Interpreter.scala b/testcases/verification/compilation/Interpreter.scala
index 40dcab73cdb00b0b65dd960ca3e2427e4fa503c7..1c8e3bbde2b6dc18ba42211f2bfc498a0bcfaf71 100644
--- a/testcases/verification/compilation/Interpreter.scala
+++ b/testcases/verification/compilation/Interpreter.scala
@@ -1,12 +1,13 @@
+import leon.annotation._
import leon.lang._
object Interpret {
- abstract class BoolTree
+ abstract class BoolTree
case class Eq(t1 : IntTree, t2 : IntTree) extends BoolTree
case class And(t1 : BoolTree, t2 : BoolTree) extends BoolTree
case class Not(t : BoolTree) extends BoolTree
- abstract class IntTree
+ abstract class IntTree
case class Const(c:Int) extends IntTree
case class Var(index:Int) extends IntTree
case class Plus(t1 : IntTree, t2 : IntTree) extends IntTree
@@ -19,7 +20,7 @@ object Interpret {
}
def beval(t:BoolTree, x0 : Int) : Boolean = {
- t match {
+ t match {
case Less(t1, t2) => ieval(t1,x0) < ieval(t2,x0)
case Eq(t1, t2) => ieval(t1,x0) == ieval(t2,x0)
case And(t1, t2) => beval(t1,x0) && beval(t2,x0)
@@ -56,6 +57,7 @@ object Interpret {
!treeBad(If(Less(Const(0),Var(0)), Var(0), Minus(Const(0),Var(0))))
} holds
+ @ignore
def main(args : Array[String]) {
thereIsGoodTree()
}
diff --git a/testcases/verification/compilation/SimpInterpret.scala b/testcases/verification/compilation/SimpInterpret.scala
index fab5035897d86b4b587715cb4d7ef3459c1fed2f..6c61bad49173ecc0ff9edafc432d11eb6ffbbadb 100644
--- a/testcases/verification/compilation/SimpInterpret.scala
+++ b/testcases/verification/compilation/SimpInterpret.scala
@@ -1,5 +1,5 @@
//import scala.collection.immutable.Set
-//import leon.annotation._
+import leon.annotation._
import leon.lang._
object Interpret {
@@ -61,6 +61,7 @@ object Interpret {
!treeBad(If(Less(Const(0),Var()), Var(), Minus(Const(0),Var())))
} holds
+ @ignore
def main(args : Array[String]) {
thereIsGoodTree()
}
diff --git a/testcases/verification/graph/MST/MSTMap.scala b/testcases/verification/graph/MST/MSTMap.scala
index 1ef72da321d96c6b65977427c2aff485212c990e..e718256b6d226dea77efddadc970ffc44c7dab0f 100644
--- a/testcases/verification/graph/MST/MSTMap.scala
+++ b/testcases/verification/graph/MST/MSTMap.scala
@@ -15,16 +15,16 @@ object MSTMap {
def mst(g : Graph) : Map[(Int,Int), Int] = {
require(invariant(g) && isUndirected(g) && isConnected(g) &&
g.nVertices <= 3)
-
+
var uf_map = Map.empty[Int, Int] //map to represent parent
//relationship to model union find
var spanningTree = Map.empty[(Int,Int), Int]
var alreadyTested = Map.empty[(Int, Int), Int]
-
+
(while(!isConnected(spanningTree, g.nVertices)) {
val next_edge = getSmallestEdge(g.nVertices, g.edges, alreadyTested)
-
+
val p1 = uFind(next_edge._1, uf_map)
val p2 = uFind(next_edge._2, uf_map)
if(p1 != p2) {
@@ -45,18 +45,18 @@ object MSTMap {
// We only verify that the edge set returned corresponds to some
// spanning tree, but not that it is of minimal weight.
-
+
// Here, we always take the smallest edge regardless whether it
// creates a cycle or not,
// Leon loops
def mstBogus(g : Graph) : Map[(Int,Int), Int] = {
require(invariant(g) && isUndirected(g) && isConnected(g) &&
g.nVertices <= 4)
-
+
var edges = g.edges
var spanningTree = Map.empty[(Int,Int), Int]
var alreadyTested = Map.empty[(Int, Int), Int]
-
+
(while(!isConnected(spanningTree, g.nVertices)) {
val next_edge = getSmallestEdge(g.nVertices, edges, alreadyTested)
@@ -73,13 +73,13 @@ object MSTMap {
spanningTree
} ensuring(x => isAcyclic(x, g.nVertices) && isConnected(x, g.nVertices))
-
+
/*
-----------------------------------------------------------------------------
GRAPH FUNCTIONS
-----------------------------------------------------------------------------
*/
-
+
def invariant(g : Graph) = {
def noSelfLoops(i : Int) : Boolean = {
@@ -89,10 +89,10 @@ object MSTMap {
else
noSelfLoops(i+1)
}
-
+
g.nVertices >= 0 && noSelfLoops(0)
}
-
+
/**
Tests, if g is undirected, that is if for every edge (i,j) there is
also and edge (j,i)
@@ -108,11 +108,11 @@ object MSTMap {
var j = 0
while(j < g.nVertices && res) {
res = !edgeSet.isDefinedAt(i,j) || edgeSet.isDefinedAt(j,i)
-
+
//If weights should considered
if(res && edgeSet.isDefinedAt(i,j))
res = edgeSet(i,j) == edgeSet(j,i)
-
+
j += 1
}
i += 1
@@ -136,11 +136,11 @@ object MSTMap {
it this function would always return a valid edge, however, this
property is not easily expressible in Leon.
*/
-
+
var i = 0
val big = 100000000
var res = (-1,-1,big)
-
+
while(i < nVertices) {
var j = 0
while(j < nVertices) {
@@ -171,7 +171,7 @@ object MSTMap {
require(g.nVertices >= 0 && isUndirected(g))
isConnected(g.edges, g.nVertices)
}
-
+
def isConnected(edges : Map[(Int,Int), Int], nVertices : Int) : Boolean = {
require(nVertices >= 0)
val uf = calculateUF(edges, nVertices)._1
@@ -204,7 +204,7 @@ object MSTMap {
def calculateUF(edgeSet : Map[(Int,Int), Int], nVertices : Int) :
(Map[Int, Int], Boolean)= {
require(nVertices >= 0)
-
+
var i = 0
var uf = Map.empty[Int, Int]
var cycle = false
@@ -223,7 +223,7 @@ object MSTMap {
//"remove" twin edge
edges = edges.updated((j,i), -1)
- }
+ }
}
j += 1
}
@@ -232,7 +232,7 @@ object MSTMap {
(uf, cycle)
}
-
+
/* *************************************
Union find
*************************************** */
@@ -246,7 +246,7 @@ object MSTMap {
// naive union
val p1 = uFind(e1,s)
val p2 = uFind(e2, s)
-
+
if(p1 != p2)
//naive union
s.updated(p1, p2) //only union if theiy are really in different trees
@@ -257,7 +257,8 @@ object MSTMap {
// fsc -d classes -classpath
// ../../leon-2.0/target/scala-2.9.1-1/classes MST.scala
- // scala -classpath classes MST
+ // scala -classpath classes MST
+ @ignore
def main(args: Array[String]) {
val edges = Map((1,0) -> 10, (0,1) -> 10, (1,2) -> 12, (2,1) ->
12, (0,2) -> 18, (2,0) -> 18, (3,1) -> 20, (1,3) -> 20)
@@ -267,5 +268,5 @@ object MSTMap {
println(mst(g)); //works
println(mstBogus(g)); // crashes because postcondition doensn't hold
}
-
+
}
diff --git a/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala b/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala
index 4ac5d863e880a484a00a8fef939964607320e6db..b79751c692cf8ebcd7c2f24a85804dc210568a50 100644
--- a/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala
+++ b/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala
@@ -11,14 +11,14 @@ object DijkstrasSortedList {
* Graph representation and algorithms
**************************************************************************/
case class Graph(nVertices : Int, edges : Map[(Int,Int), Int])
-
+
// Disallow self edges? Not actually important since they can be ignored.
def invariant(g : Graph) = g.nVertices >= 0
-
+
// true if x & y have same number of nodes and y has all x's edges
def isSubGraph(x : Graph, y : Graph) : Boolean = {
require(invariant(x) && invariant(y))
-
+
var ret : Boolean = (x.nVertices == y.nVertices)
if (ret){
var i = 0
@@ -34,11 +34,11 @@ object DijkstrasSortedList {
}
ret
}
-
+
// true if every edge has a weight of at least 0
def nonnegativeWeights(g : Graph) : Boolean = {
require(invariant(g))
-
+
var ret : Boolean = true
var i = 0
while(i<g.nVertices) {
@@ -54,20 +54,20 @@ object DijkstrasSortedList {
}
ret
}
-
+
// true if b is reachable from a
def isReachable(g : Graph, a : Int, b : Int) : Boolean = {
require(invariant(g) && a >= 0 && a < g.nVertices && b >= 0 && b < g.nVertices)
-
+
//TODO
false
}
-
-
+
+
/***************************************************************************
* Sorted list representation and algorithims
**************************************************************************/
-
+
/** A list containing node, dist pairs.
*
* Sorted by distance, nearest first. Distance must be non-negative. Node
@@ -76,7 +76,7 @@ object DijkstrasSortedList {
abstract class SortedNDList
case class ListNode(node : Int, dist : Int, next : SortedNDList) extends SortedNDList
case class ListEnd() extends SortedNDList
-
+
/** List invariant (see description above) */
@induct
def sndInvariant(list : SortedNDList) : Boolean = {
@@ -91,18 +91,18 @@ object DijkstrasSortedList {
false
case ListEnd() => true //len <= 3
}
-
+
invRec(list/*, Set.empty, 0, 0*/)
}
-
+
/** Look for node in list and remove, if it exists. */
@induct
def removeFromList(list : SortedNDList, node : Int) : SortedNDList ={
// something about this times out
require(sndInvariant(list))
-
+
//println("removeFromList: "+list)
-
+
list match {
case ListNode(n,d,next) =>
if (n == node)
@@ -113,7 +113,7 @@ object DijkstrasSortedList {
case ListEnd() => list
}
} ensuring(sndInvariant(_)) // something about this generates an error: is the precondition not checked for _all_ elements or something?
-
+
/** Return true if list contains node */
@induct
def listContains(list : SortedNDList, node : Int) : Boolean ={
@@ -126,14 +126,14 @@ object DijkstrasSortedList {
case ListEnd() => false
}
}
-
+
/** Add a new node to the list, such that list remains sorted by distance.
* Assume node is not already in list. */
@induct
def addSorted(list : SortedNDList, node : Int, dist : Int) : SortedNDList = {
// something to do with this times out
require(sndInvariant(list) && !listContains(list, node) && node >= 0 && dist >= 0)
-
+
list match {
case ListNode(n,d,next) =>
if (d > dist) // insert here
@@ -144,37 +144,37 @@ object DijkstrasSortedList {
ListNode(node, dist, list)
}
} ensuring (sndInvariant(_)) // something to do with this times out
-
+
/** Update node with distance minimum of dist and current value. Add if not
* in list, and maintain sorted order. */
@induct
def updateDistInList(list : SortedNDList, node : Int, dist : Int) : SortedNDList = {
require(sndInvariant(list) && node >= 0 && dist >= 0)
-
+
val listRemoved = removeFromList(list, node)
addSorted(listRemoved, node, dist)
} ensuring(sndInvariant(_))
-
-
+
+
/***************************************************************************
* Dijkstra's algorithm
**************************************************************************/
-
+
def isNodeNotB(list : SortedNDList, b : Int) : Boolean =
list match {
case ListNode(n, _, _) => n!=b
case ListEnd() => false
}
-
+
// common precondition: g is a valid graph and a and b are valid nodes
def bounds(g : Graph, a : Int, b : Int) : Boolean =
invariant(g) && 0 <= a && a < g.nVertices && 0 <= b && b < g.nVertices
-
+
// find the shortest path from a to b in g, and return its distance
// return -1 if the two aren't connected
def shortestPath(g : Graph, a : Int, b : Int) : Int = {
require(bounds(g,a,b) && nonnegativeWeights(g))
-
+
// We should always have at least some node if we haven't reached b (so
// long as b is in the graph and connected to a).
@induct
@@ -184,20 +184,20 @@ object DijkstrasSortedList {
* We should check same invariant at function exit. But there's no point:
* it's too much for Leon to reason about at once!
*/
-
+
list match {
case ListNode(node, dist, next) if (node==b) =>
list
case ListNode(node, dist, next) =>
var n = 0
var tail : SortedNDList = next
-
+
(while (n < g.nVertices){
if (n != node && !visited.contains(n) && g.edges.isDefinedAt((node,n)))
tail = updateDistInList(tail, n, dist+g.edges((node,n)))
n = n + 1
}) invariant(sndInvariant(list) && n >= 0 && n <= g.nVertices)
-
+
spVisit (tail, visited ++ Set(node))
case ListEnd() =>
list
@@ -206,7 +206,7 @@ object DijkstrasSortedList {
case ListEnd() => !isReachable(g,a,b)
case ListNode(node,_,_) => node==b
})
-
+
// We start from a, which has distance 0. All other nodes implicitly have
// infinite distance.
val startingList : SortedNDList = ListNode(a, 0, ListEnd())
@@ -221,12 +221,13 @@ object DijkstrasSortedList {
-1
}
} ensuring (res => res >= -1 /*(if (isReachable(g,a,b)) res>=0 else res== -1)*/)
-
+
+ @ignore
def main(args: Array[String]) {
val spanningTreeE = Map((0,1) -> 1, (0,2) -> 2, (2,3) -> 5, (0,3) -> 10, (3,2) -> 0)
val spanningTree = Graph(4, spanningTreeE)
val singleGraph = Graph(1, Map.empty)
-
+
println(spanningTree)
println("from 0 to 3 (should be 7): "+shortestPath(spanningTree,0,3))
println("from 3 to 1 (no path): "+shortestPath(spanningTree,3,1))
diff --git a/testcases/verification/list-algorithms/InsertionSort.scala b/testcases/verification/list-algorithms/InsertionSort.scala
index 35062e263c1a9b869bf2c34a25196ae4fbce3811..980927204dad1e609e93dd8dcf8a364d027e113d 100644
--- a/testcases/verification/list-algorithms/InsertionSort.scala
+++ b/testcases/verification/list-algorithms/InsertionSort.scala
@@ -51,7 +51,7 @@ object InsertionSort {
case Nil() => true
case Cons(x, Nil()) => true
case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
+ }
/* Inserting element 'e' into a sorted list 'l' produces a sorted list with
* the expected content and size */
@@ -60,8 +60,8 @@ object InsertionSort {
l match {
case Nil() => Cons(e,Nil())
case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -73,8 +73,8 @@ object InsertionSort {
l match {
case Nil() => Cons(e,Nil())
case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -84,11 +84,12 @@ object InsertionSort {
def sort(l: List): List = (l match {
case Nil() => Nil()
case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
+ }) ensuring(res => contents(res) == contents(l)
&& isSorted(res)
&& size(res) == size(l)
)
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/testcases/verification/list-algorithms/MergeSort.scala b/testcases/verification/list-algorithms/MergeSort.scala
index 1bbd7f607528a9549363dec4d3e73f547f602565..5fc80d117c9eae3bddec01377683eac54f0c37cd 100644
--- a/testcases/verification/list-algorithms/MergeSort.scala
+++ b/testcases/verification/list-algorithms/MergeSort.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.annotation._
object MergeSort {
sealed abstract class List
@@ -57,6 +58,7 @@ object MergeSort {
}) ensuring(res => contents(res) == contents(list) && is_sorted(res))
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
println(ls)
diff --git a/testcases/verification/list-algorithms/QuickSort.scala b/testcases/verification/list-algorithms/QuickSort.scala
index 30b3621438bd0ef944b61f831b36379deb1470f6..1afbc3a2b4d7c5f5a54560a6aa401d396646390c 100644
--- a/testcases/verification/list-algorithms/QuickSort.scala
+++ b/testcases/verification/list-algorithms/QuickSort.scala
@@ -53,7 +53,7 @@ object QuickSort {
case Nil() => bList
case _ => rev_append(reverse(aList),bList)
}) ensuring(content(_) == content(aList) ++ content(bList))
-
+
def greater(n:Int,list:List) : List = list match {
case Nil() => Nil()
case Cons(x,xs) => if (n < x) Cons(x,greater(n,xs)) else greater(n,xs)
@@ -69,7 +69,7 @@ object QuickSort {
case Nil() => Nil()
case Cons(x,xs) => if (n>x) Cons(x,smaller(n,xs)) else smaller(n,xs)
}
-
+
@induct
def smallerProp(n: Int, list: List): Boolean = (max(smaller(n, list)) match {
case Some(m) => n > m
@@ -117,6 +117,7 @@ object QuickSort {
case Cons(x,xs) => append(append(quickSort(smaller(x,xs)),Cons(x,equals(x,xs))),quickSort(greater(x,xs)))
}) ensuring(res => content(res) == content(list)) // && isSorted(res))
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/testcases/verification/math/Prime.scala b/testcases/verification/math/Prime.scala
index d8de43f86cf8ec2528e54125dc42148f4cc49e84..1e928dcff5af0eb281f2b192bdd0a88a4cbe0fb5 100644
--- a/testcases/verification/math/Prime.scala
+++ b/testcases/verification/math/Prime.scala
@@ -1,3 +1,5 @@
+import leon.annotation._
+
object Prime {
// an attempt at defining isPrime in PureScala...
@@ -36,6 +38,7 @@ object Prime {
} ensuring(res => !res)
// Just for testing.
+ @ignore
def main(args : Array[String]) : Unit = {
def test(n : BigInt) : Unit = {
println("Is " + n + " prime ? -> " + isPrime(n))
diff --git a/testcases/verification/xlang/InsertionSort.scala b/testcases/verification/xlang/InsertionSort.scala
index 0a53cb55f4ef32b775646e1ea43a8c74b33a80c7..71dab126cda6927380c9395b39dcc49f3a550801 100644
--- a/testcases/verification/xlang/InsertionSort.scala
+++ b/testcases/verification/xlang/InsertionSort.scala
@@ -32,7 +32,7 @@ object InsertionSort {
case Nil() => true
case Cons(x, Nil()) => true
case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
+ }
def isReversedSorted(l: List): Boolean = l match {
case Nil() => true
case Cons(x, Nil()) => true
@@ -66,8 +66,8 @@ object InsertionSort {
l match {
case Nil() => Cons(e,Nil())
case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -79,8 +79,8 @@ object InsertionSort {
l match {
case Nil() => Cons(e,Nil())
case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -90,11 +90,12 @@ object InsertionSort {
def sort(l: List): List = (l match {
case Nil() => Nil()
case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
+ }) ensuring(res => contents(res) == contents(l)
&& isSorted(res)
&& size(res) == size(l)
)
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/testcases/web/demos/008_Tutorial-Robot.scala b/testcases/web/demos/008_Tutorial-Robot.scala
index c78dc15f2c48703bae470cd41578c7b141d7d9ee..bca1f367a26df843e65cea76de7029652f0b4906 100644
--- a/testcases/web/demos/008_Tutorial-Robot.scala
+++ b/testcases/web/demos/008_Tutorial-Robot.scala
@@ -365,7 +365,7 @@ object Robot {
}
def validState(rs: RobotState)(implicit w: World): Boolean = {
-
+
// 6) Sensors have consistent data
val recentData = rs.ns.validData && rs.hs.validData
@@ -509,6 +509,7 @@ object Robot {
}
+ @ignore
def main(a: Array[String]): Unit = {
val map0 = """|XXXXXXXXX
|XR FF X
diff --git a/testcases/web/verification/03_Insertion_Sort.scala b/testcases/web/verification/03_Insertion_Sort.scala
index e53b89b1732bed1dfb1c1389feacc70d4490285d..4b1c8ef7cd0b61ab0c2f91533598be792dd1b809 100644
--- a/testcases/web/verification/03_Insertion_Sort.scala
+++ b/testcases/web/verification/03_Insertion_Sort.scala
@@ -24,7 +24,7 @@ object InsertionSort {
case Nil => true
case Cons(x, Nil) => true
case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
+ }
/* Inserting element 'e' into a sorted list 'l' produces a sorted list with
* the expected content and size */
@@ -33,8 +33,8 @@ object InsertionSort {
l match {
case Nil => Cons(e,Nil)
case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -44,8 +44,8 @@ object InsertionSort {
l match {
case Nil => Cons(e,Nil)
case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -55,7 +55,7 @@ object InsertionSort {
def sort(l: List): List = (l match {
case Nil => Nil
case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
+ }) ensuring(res => contents(res) == contents(l)
&& isSorted(res)
&& size(res) == size(l)
)
@@ -69,6 +69,7 @@ object InsertionSort {
}
} ensuring(res => contents(res) == contents(l1) ++ contents(l2) && isSorted(res))
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil))))))