Commit 3ef4672e authored by Eva Darulova's avatar Eva Darulova

clean up of frontend, and adding Leon acknowledgeement

parent ad07d1bd
Copyright (c) 2009-2015 EPFL, Lausanne, unless otherwise specified. All rights
reserved.
This software was developed by the Laboratory for Automated Reasoning and
Analysis (LARA) of the Swiss Federal Institute of Technology (EPFL), Lausanne,
Switzerland.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
and/or other materials provided with the distribution.
THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ''AS IS'' AND ANY
EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
The views and conclusions contained in the software and documentation are those
of the authors and should not be interpreted as representing official policies,
either expressed or implied, of EPFL.
Project Daisy
Acknowledgements
----
A big portion of the infrastructure has been inspired by and sometimes
directly taken from the Leon project (see the LEON_LICENSE).
Especially the following files bear more than a passing resemblance to Leon's code:
frontend.{ASTExtractors, CodeExtraction, DaisyExtraction, ExtractionPhase,
SaveImports, ScalaCompiler, SimpleReporter}
lang.{DefOps, Definitions, Extractors, Identifiers, PrettyPrinter, TreeOps, Trees, Types}
utils.{Context,DaisyFatalError, DaisyOption, DaisyPhase, DebugSection, Position, Reporter,
Settings, Timer}
......@@ -14,6 +14,12 @@ object CodeGenerationPhase extends DaisyPhase {
ctx.reporter.info("Hello, this is the code generation phase.")
val program = p.original
ctx.reporter.info("units: " + program.units)
ctx.reporter.info("modules: " + program.modules)
ctx.reporter.info(p.original)
......
......@@ -350,26 +350,6 @@ trait ASTExtractors {
object ExpressionExtractors {
import ExtractorHelpers._
/*object ExEpsilonExpression {
def unapply(tree: Apply) : Option[(Tree, Symbol, Tree)] = tree match {
case Apply(
TypeApply(ExSymbol("leon", "lang", "xlang", "epsilon"), typeTree :: Nil),
Function((vd @ ValDef(_, _, _, EmptyTree)) :: Nil, predicateBody) :: Nil) =>
Some((typeTree, vd.symbol, predicateBody))
case _ => None
}
}
object ExWaypointExpression {
def unapply(tree: Apply) : Option[(Tree, Tree, Tree)] = tree match {
case Apply(
TypeApply(ExSymbol("leon", "lang", "xlang", "waypoint"), typeTree :: Nil),
List(i, expr)) =>
Some((typeTree, i, expr))
case _ => None
}
}*/
object ExErrorExpression {
def unapply(tree: Apply) : Option[(String, Tree)] = tree match {
case a @ Apply(TypeApply(ExSymbol("leon", "lang", "error"), List(tpe)), List(lit : Literal)) =>
......@@ -399,16 +379,6 @@ trait ASTExtractors {
}
}
object ExWithOracleExpression {
def unapply(tree: Apply) : Option[(List[(Tree, Symbol)], Tree)] = tree match {
case a @ Apply(
TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "withOracle"), types),
Function(vds, body) :: Nil) =>
Some(((types zip vds.map(_.symbol)).toList, body))
case _ => None
}
}
object ExArrayUpdated {
def unapply(tree: Apply): Option[(Tree,Tree,Tree)] = tree match {
case Apply(
......@@ -577,6 +547,13 @@ trait ASTExtractors {
}
}
object ExFloat64Literal {
def unapply(tree: Literal): Option[Double] = tree match {
case Literal(c @ Constant(i)) if c.tpe == DoubleClass.tpe => Some(c.doubleValue)
case _ => None
}
}
object ExUnitLiteral {
def unapply(tree: Literal): Boolean = tree match {
case Literal(c @ Constant(_)) if c.tpe == UnitClass.tpe => true
......@@ -661,6 +638,44 @@ trait ASTExtractors {
}
}
object ExImplicitInt2Real {
def unapply(tree: Apply): Option[Int] = tree match {
case Apply(select, List(Literal(c @ Constant(i)))) if (select.toString == "leon.Real.int2real") =>
Some(c.intValue)
case _ => None
}
}
object ExImplicitDouble2Real {
def unapply(tree: Apply): Option[Double] = tree match {
case Apply(select, List(Literal(c @ Constant(i)))) if (select.toString == "leon.Real.double2real") =>
Some(c.doubleValue)
case _ => None
}
}
object ExSqrt {
def unapply(tree: Apply): Option[Tree] = tree match {
case Apply(select, List(arg)) if (select.toString == "leon.Real.sqrt") => Some(arg)
case _ => None
}
}
object ExUMinusReal {
def unapply(tree: Apply): Option[Tree] = tree match {
case Apply(Select(t, n), List()) if (n == nme.UNARY_-) => Some(t)
case _ => None
}
}
object ExPlusMinus {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
case Apply(Select(lhs, n), List(rhs)) if (n.toString == "$plus$div$minus") => Some((lhs,rhs))
//case Apply(Select(lhs, n), List(rhs)) if (n.toString == "$u00B1") => Some((lhs,rhs))
case _ => None
}
}
object ExPatternMatching {
def unapply(tree: Match): Option[(Tree,List[CaseDef])] =
if(tree != null) Some((tree.selector, tree.cases)) else None
......@@ -819,50 +834,11 @@ trait ASTExtractors {
}
}
}
object ExFloat64Literal {
def unapply(tree: Literal): Option[Double] = tree match {
case Literal(c @ Constant(i)) if c.tpe == DoubleClass.tpe => Some(c.doubleValue)
case _ => None
}
}
object ExImplicitInt2Real {
def unapply(tree: Apply): Option[Int] = tree match {
case Apply(select, List(Literal(c @ Constant(i)))) if (select.toString == "leon.Real.int2real") =>
Some(c.intValue)
case _ => None
}
}
object ExImplicitDouble2Real {
def unapply(tree: Apply): Option[Double] = tree match {
case Apply(select, List(Literal(c @ Constant(i)))) if (select.toString == "leon.Real.double2real") =>
Some(c.doubleValue)
case _ => None
}
}
object ExSqrt {
def unapply(tree: Apply): Option[Tree] = tree match {
case Apply(select, List(arg)) if (select.toString == "leon.Real.sqrt") => Some(arg)
case _ => None
}
}
object ExUMinusReal {
def unapply(tree: Apply): Option[Tree] = tree match {
case Apply(Select(t, n), List()) if (n == nme.UNARY_-) => Some(t)
case _ => None
}
}
object ExPlusMinus {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
case Apply(Select(lhs, n), List(rhs)) if (n.toString == "$plus$div$minus") => Some((lhs,rhs))
//case Apply(Select(lhs, n), List(rhs)) if (n.toString == "$u00B1") => Some((lhs,rhs))
case _ => None
}
}
}
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -6,9 +6,6 @@ package frontend
import scala.tools.nsc._
import scala.tools.nsc.plugins._
//import purescala.Definitions.Program
//mport purescala.Definitions.{ModuleDef => LeonModuleDef, _}
trait DaisyExtraction extends SubComponent with CodeExtraction {
import global._
......@@ -25,7 +22,7 @@ trait DaisyExtraction extends SubComponent with CodeExtraction {
}
def compiledUnits = {
new Extraction(units).extractUnits
extractUnits(units)
}
def newPhase(prev: scala.tools.nsc.Phase): StdPhase = new Phase(prev)
......
......@@ -6,10 +6,6 @@ package frontend
import scala.tools.nsc._
import scala.tools.nsc.plugins._
//import purescala.Definitions.Program
//import purescala.Definitions.{ModuleDef => LeonModuleDef, _}
//import utils.{Position => LeonPosition, RangePosition => LeonRangePosition, OffsetPosition => LeonOffsetPosition}
trait SaveImports extends SubComponent {
import global._
import global.definitions._
......@@ -21,21 +17,20 @@ trait SaveImports extends SubComponent {
var imports : Map[RefTree,List[Import]] = Map()
/*def scalaPosToLeonPos(p: global.Position): LeonPosition = {
def scalaPosToLeonPos(p: global.Position): daisy.utils.Position = {
if (p == NoPosition) {
leon.utils.NoPosition
daisy.utils.NoPosition
} else if (p.isRange) {
val start = p.focusStart
val end = p.focusEnd
LeonRangePosition(start.line, start.column, start.point,
daisy.utils.RangePosition(start.line, start.column, start.point,
end.line, end.column, end.point,
p.source.file.file)
} else {
LeonOffsetPosition(p.line, p.column, p.point,
daisy.utils.OffsetPosition(p.line, p.column, p.point,
p.source.file.file)
}
}*/
}
def newPhase(prev: scala.tools.nsc.Phase): StdPhase = new Phase(prev)
......@@ -53,7 +48,7 @@ trait SaveImports extends SubComponent {
tree.foreach {
case imp : Import =>
ctx.reporter.warning(
//scalaPosToLeonPos(imp.pos),
scalaPosToLeonPos(imp.pos),
"Imports will not be preserved in the AST unless they are at top-level"
)
case _ =>
......
......@@ -32,17 +32,11 @@ class ScalaCompiler(settings : NSCSettings, ctx: Context) extends Global(setting
superAccessors -> "add super accessors in traits and nested classes",
extensionMethods -> "add extension methods for inline classes",
pickler -> "serialize symbol tables",
saveImports -> "save imports to pass to leonExtraction",
saveImports -> "save imports to pass to daisyExtraction",
refChecks -> "reference/override checking, translate nested objects",
daisyExtraction -> "extracts leon trees out of scala trees"
)
phs foreach { phasesSet += _._1 }
}
class Run extends super.Run {
override def progress(current: Int, total: Int) {
//ctx.reporter.onCompilerProgress(current, total)
// ?? this methods is empty in Leon ?!
}
}
}
......@@ -5,6 +5,7 @@ package lang
import Identifiers._
import Definitions._
import Trees.{Require, Ensuring, NoTree, Expr}
object DefOps {
......@@ -187,5 +188,47 @@ object DefOps {
rec(df).reverse
}
def unitsInPackage(p: Program, pack : PackageRef) = p.units filter { _.pack == pack }
def withPrecondition(expr: Expr, pred: Option[Expr]): Expr = (pred, expr) match {
case (Some(newPre), Require(pre, b)) => Require(newPre, b)
case (Some(newPre), Ensuring(Require(pre, b), i, p)) => Ensuring(Require(newPre, b), i, p)
case (Some(newPre), Ensuring(b, i, p)) => Ensuring(Require(newPre, b), i, p)
case (Some(newPre), b) => Require(newPre, b)
case (None, Require(pre, b)) => b
case (None, Ensuring(Require(pre, b), i, p)) => Ensuring(b, i, p)
case (None, Ensuring(b, i, p)) => Ensuring(b, i, p)
case (None, b) => b
}
def withPostcondition(expr: Expr, oie: Option[(Identifier, Expr)]) = (oie, expr) match {
case (Some((nid, npost)), Ensuring(b, id, post)) => Ensuring(b, nid, npost)
case (Some((nid, npost)), b) => Ensuring(b, nid, npost)
case (None, Ensuring(b, i, p)) => b
case (None, b) => b
}
def withBody(expr: Expr, body: Option[Expr]) = expr match {
case Require(pre, _) => Require(pre, body.getOrElse(NoTree(expr.getType)))
case Ensuring(Require(pre, _), i, post) => Ensuring(Require(pre, body.getOrElse(NoTree(expr.getType))), i, post)
case Ensuring(_, i, post) => Ensuring(body.getOrElse(NoTree(expr.getType)), i, post)
case _ => body.getOrElse(NoTree(expr.getType))
}
def withoutSpec(expr: Expr) = expr match {
case Require(pre, b) => Option(b).filterNot(_.isInstanceOf[NoTree])
case Ensuring(Require(pre, b), i, post) => Option(b).filterNot(_.isInstanceOf[NoTree])
case Ensuring(b, i, post) => Option(b).filterNot(_.isInstanceOf[NoTree])
case b => Option(b).filterNot(_.isInstanceOf[NoTree])
}
def preconditionOf(expr: Expr) = expr match {
case Require(pre, _) => Some(pre)
case Ensuring(Require(pre, _), _, _) => Some(pre)
case b => None
}
def postconditionOf(expr: Expr) = expr match {
case Ensuring(_, i, post) => Some((i, post))
case _ => None
}
}
\ No newline at end of file
This diff is collapsed.
......@@ -59,7 +59,7 @@ object Identifiers {
def toVariable : Variable = Variable(this)
//def freshen: Identifier = FreshIdentifier(name, alwaysShowUniqueID).copiedFrom(this)
def freshen: Identifier = FreshIdentifier(name, alwaysShowUniqueID).copiedFrom(this)
var owner : Option[Definition] = None
......
......@@ -24,17 +24,10 @@ object Trees {
}
override def toString: String = PrettyPrinter(this)
// TODO: how is this different to toString
/*def asString(implicit ctx: LeonContext): String = {
ScalaPrinter(this, ctx)
}*/
}
/* EXPRESSIONS */
abstract class Expr extends Tree with Typed with Serializable
// TODO: do we need this? Can this happen with our subset?
case class NoTree(tpe: TypeTree) extends Expr with Terminal with FixedType {
val fixedType = tpe
}
......@@ -43,9 +36,10 @@ object Trees {
self: Expr =>
}
/* This describes computational errors (unmatched case, taking min of an
/** This describes computational errors (unmatched case, taking min of an
* empty set, division by zero, etc.). It should always be typed according to
* the expected type. */
* the expected type.
*/
case class Error(description: String) extends Expr with Terminal
case class Require(pred: Expr, body: Expr) extends Expr with FixedType {
......@@ -71,17 +65,6 @@ object Trees {
}
}
// Provide an oracle (synthesizable, all-seeing choose)
case class WithOracle(oracles: List[Identifier], body: Expr) extends Expr with FixedType with UnaryExtractable {
assert(!oracles.isEmpty)
val fixedType = body.getType
def extract = {
Some((body, (e: Expr) => WithOracle(oracles, e).setPos(this)))
}
}
case class Hole(fixedType: TypeTree, alts: Seq[Expr]) extends Expr with FixedType with NAryExtractable {
def extract = {
......@@ -559,8 +542,6 @@ object Trees {
val tpe = if (elements.isEmpty) None else leastUpperBound(elements.toSeq.map(_.getType))
tpe.foreach(t => setType(SetType(t)))
}
// TODO : Figure out what evaluation order is, for this.
// Perhaps then rewrite as "contains".
case class ElementOfSet(element: Expr, set: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
......@@ -705,7 +686,7 @@ object Trees {
}
//same as let, buf for mutable variable declaration
//same as let, but for mutable variable declaration
case class LetVar(binder: Identifier, value: Expr, body: Expr) extends Expr with BinaryExtractable {
val et = body.getType
if(et != Untyped)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment