diff --git a/src/funcheck/AnalysisComponent.scala b/src/funcheck/AnalysisComponent.scala
index b92db66087b36850d46f0751b88f07e781d40657..3670c40d39ae1e67f5a85da061de7142d97097b0 100644
--- a/src/funcheck/AnalysisComponent.scala
+++ b/src/funcheck/AnalysisComponent.scala
@@ -37,8 +37,8 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
// That filter just helps getting meaningful errors before the attempt to
// extract the code, but it's really optional.
- (new ForeachTreeTraverser(firstFilter(unit))).traverse(unit.body)
- stopIfErrors
+ // (new ForeachTreeTraverser(firstFilter(unit))).traverse(unit.body)
+ // stopIfErrors
val prog: purescala.Definitions.Program = extractCode(unit)
println("Extracted program for " + unit + ": ")
@@ -58,24 +58,24 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
}
/** Weeds out some programs containing unsupported features. */
- def firstFilter(unit: CompilationUnit)(tree: Tree): Unit = {
- def unsup(s: String): String = "FunCheck: Unsupported construct: " + s
+ // def firstFilter(unit: CompilationUnit)(tree: Tree): Unit = {
+ // def unsup(s: String): String = "FunCheck: Unsupported construct: " + s
- tree match {
- case ValDef(mods, name, tpt, rhs) if mods.isVariable =>
- unit.error(tree.pos, unsup("mutable variable/field."))
- case LabelDef(name, params, rhs) => unit.error(tree.pos, unsup("loop."))
- case Assign(lhs, rhs) => unit.error(tree.pos, unsup("assignment to mutable variable/field."))
- case Return(expr) => unit.error(tree.pos, unsup("return statement."))
- case Try(block, catches, finalizer) => unit.error(tree.pos, unsup("try block."))
- case SingletonTypeTree(ref) => unit.error(tree.pos, unsup("singleton type."))
- case SelectFromTypeTree(qualifier, selector) => unit.error(tree.pos, unsup("path-dependent type."))
- case CompoundTypeTree(templ: Template) => unit.error(tree.pos, unsup("compound/refinement type."))
- case TypeBoundsTree(lo, hi) => unit.error(tree.pos, unsup("type bounds."))
- case ExistentialTypeTree(tpt, whereClauses) => unit.error(tree.pos, unsup("existential type."))
- case _ => ;
- }
- }
+ // tree match {
+ // case ValDef(mods, name, tpt, rhs) if mods.isVariable =>
+ // unit.error(tree.pos, unsup("mutable variable/field."))
+ // case LabelDef(name, params, rhs) => unit.error(tree.pos, unsup("loop."))
+ // case Assign(lhs, rhs) => unit.error(tree.pos, unsup("assignment to mutable variable/field."))
+ // case Return(expr) => unit.error(tree.pos, unsup("return statement."))
+ // case Try(block, catches, finalizer) => unit.error(tree.pos, unsup("try block."))
+ // case SingletonTypeTree(ref) => unit.error(tree.pos, unsup("singleton type."))
+ // case SelectFromTypeTree(qualifier, selector) => unit.error(tree.pos, unsup("path-dependent type."))
+ // case CompoundTypeTree(templ: Template) => unit.error(tree.pos, unsup("compound/refinement type."))
+ // case TypeBoundsTree(lo, hi) => unit.error(tree.pos, unsup("type bounds."))
+ // case ExistentialTypeTree(tpt, whereClauses) => unit.error(tree.pos, unsup("existential type."))
+ // case _ => ;
+ // }
+ // }
}
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index b9b50f6cc27735646bf0a4a2b2ed5b4854c45aad..29a23510173f017df5d81ae4bb388bf4618f1a87 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -12,6 +12,7 @@ trait CodeExtraction extends Extractors {
self: AnalysisComponent =>
import global._
+ import global.definitions._
import StructuralExtractors._
import ExpressionExtractors._
@@ -23,12 +24,10 @@ trait CodeExtraction extends Extractors {
def s2ps(tree: Tree): Expr = toPureScala(unit)(tree) match {
case Some(ex) => ex
- case None => stopIfErrors; throw new Error("unreachable?")
+ case None => stopIfErrors; scala.Predef.error("unreachable error.")
}
- /** Populates the symbolDefMap with object and class symbols, and returns
- * the symbol corresponding to the expected single top-level object. */
- def extractClassSymbols: ObjectDef = {
+ def extractTopLevelDef: ObjectDef = {
val top = unit.body match {
case p @ PackageDef(name, lst) if lst.size == 0 => {
unit.error(p.pos, "No top-level definition found.")
@@ -43,7 +42,7 @@ trait CodeExtraction extends Extractors {
case PackageDef(name, lst) => {
assert(lst.size == 1)
lst(0) match {
- case ExObjectDef(n, templ) => Some(extractObjectSym(n.toString, templ))
+ case ExObjectDef(n, templ) => Some(extractObjectDef(n.toString, templ))
case other @ _ => unit.error(other.pos, "Expected: top-level single object.")
None
}
@@ -54,38 +53,40 @@ trait CodeExtraction extends Extractors {
top.get
}
- def extractObjectSym(name: Identifier, tmpl: Template): ObjectDef = {
+ def extractObjectDef(name: Identifier, tmpl: Template): ObjectDef = {
// we assume that the template actually corresponds to an object
// definition. Typically it should have been obtained from the proper
// extractor (ExObjectDef)
var classDefs: List[ClassTypeDef] = Nil
- var objectDefs: List[purescala.Symbols.ObjectSymbol] = Nil
+ var objectDefs: List[ObjectDef] = Nil
+ var funDefs: List[FunDef] = Nil
- tmpl.body.foreach(tree => tree match {
- case ExObjectDef(o2, t2) => { objectSyms = extractObjectSym(o2, t2) :: objectSyms }
+ tmpl.body.foreach(tree => {
+ println("[[[ " + tree + "]]]\n");
+ tree match {
+ case ExObjectDef(o2, t2) => { objectDefs = extractObjectDef(o2, t2) :: objectDefs }
case ExAbstractClass(o2) => ;
+ case ExConstructorDef() => ;
+ case ExMainFunctionDef() => ;
+ case ExFunctionDef(n,p,t,b) => { funDefs = extractFunDef(n,p,t,b) :: funDefs }
case _ => ;
- })
+ }})
// val theSym = new purescala.Symbols.ObjectSymbol(name, classSyms.reverse, objectSyms.reverse)
// we register the tree associated to the symbol to be able to fill in
// the rest later
// symbolDefMap(theSym) = tmpl
- theSym
+ val theDef = new ObjectDef(name, objectDefs.reverse ::: classDefs.reverse ::: funDefs.reverse, Nil)
+ theDef
}
- // Step-by-step:
- // 1) extract class and object symbols recursively (objects can have
- // objects as members)
- // 2) set parents for classes
- // 3) extract function and val symbols (can now have a type, since we
- // have full class hierarchy)
- // 4) extract val and function bodies (can do it, since we have all
- // definitions, hence we can resolve all symbols)
+ def extractFunDef(name: Identifier, params: Seq[ValDef], tpt: Tree, body: Tree) = {
+ FunDef(name, scalaType2PureScala(unit, false)(tpt), Nil, null, None, None)
+ }
- // This extracts the class and object symbols recursively.
- val topLevelObjSym: purescala.Symbols.ObjectSymbol = extractClassSymbols
+ // THE EXTRACTION CODE STARTS HERE
+ val topLevelObjDef: ObjectDef = extractTopLevelDef
stopIfErrors
@@ -95,9 +96,11 @@ trait CodeExtraction extends Extractors {
}
println("Top level sym:")
- println(topLevelObjSym)
+ println(topLevelObjDef)
+
- Program(programName, ObjectDef("Object", Nil, Nil))
+ //Program(programName, ObjectDef("Object", Nil, Nil))
+ Program(programName, topLevelObjDef)
}
/** An exception thrown when non-purescala compatible code is encountered. */
@@ -130,6 +133,19 @@ trait CodeExtraction extends Extractors {
}
}
+ private def scalaType2PureScala(unit: CompilationUnit, silent: Boolean)(tree: Tree): funcheck.purescala.TypeTrees.TypeTree = {
+ tree match {
+ case tt: TypeTree if tt.tpe == IntClass.tpe => Int32Type
+
+ case _ => {
+ if(!silent) {
+ unit.error(tree.pos, "Could not extract type as PureScala.")
+ }
+ throw ImpureCodeEncounteredException(tree)
+ }
+ }
+ }
+
// def findContracts(tree: Tree): Unit = tree match {
// case DefDef(/*mods*/ _, name, /*tparams*/ _, /*vparamss*/ _, /*tpt*/ _, body) => {
// var realBody = body
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index 88f9ef0482ebbec66c12210f5568953b273c1c35..9ce171cdb6bfe46f1ca04111bb44327d7a34ff04 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -78,6 +78,23 @@ trait Extractors {
}
+ object ExConstructorDef {
+ def unapply(dd: DefDef): Boolean = dd match {
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if(name.toString == "<init>" && tparams.isEmpty && vparamss.size == 1 && vparamss(0).size == 0) => true
+ case _ => false
+ }
+ }
+
+ object ExMainFunctionDef {
+ def unapply(dd: DefDef): Boolean = dd match {
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if(name.toString == "main" && tparams.isEmpty && vparamss.size == 1 && vparamss(0).size == 1) => {
+ println("Looks like main " + vparamss(0)(0).symbol.tpe);
+ true
+ }
+ case _ => false
+ }
+ }
+
object ExFunctionDef {
/** Matches a function with a single list of arguments, no type
* parameters and regardless of its visibility. */
diff --git a/src/funcheck/purescala/Definitions.scala b/src/funcheck/purescala/Definitions.scala
index fcc92c6d0effc0ff13246984ab971e6dbe525cd5..ae1ea60395b5e2c0a944ee25a9d5cb76dfaf56cd 100644
--- a/src/funcheck/purescala/Definitions.scala
+++ b/src/funcheck/purescala/Definitions.scala
@@ -100,8 +100,8 @@ object Definitions {
}
/** Functions (= 'methods' of objects) */
- case class FunDef(id: Identifier, args: VarDecls, body: Expr, precondition: Option[Expr], postcondition: Option[Expr]) extends Definition {
- lazy val argTypes : Seq[TypeTree] = args.map(_.tpe)
- lazy val returnType : TypeTree = body.getType
+ case class FunDef(id: Identifier, returnType: TypeTree, args: VarDecls, body: Expr, precondition: Option[Expr], postcondition: Option[Expr]) extends Definition {
+ //lazy val argTypes : Seq[TypeTree] = args.map(_.tpe)
+ //lazy val returnType : TypeTree = body.getType
}
}
diff --git a/src/funcheck/purescala/PrettyPrinter.scala b/src/funcheck/purescala/PrettyPrinter.scala
index 855da6bd15a93208657f2f399b397621d6b3b8ab..bf1f9f3036d450517292efba75ad3b527612c455 100644
--- a/src/funcheck/purescala/PrettyPrinter.scala
+++ b/src/funcheck/purescala/PrettyPrinter.scala
@@ -87,6 +87,7 @@ object PrettyPrinter {
// TYPE TREES
// all type trees are printed in-line
private def pp(tpe: TypeTree, sb: StringBuffer): StringBuffer = tpe match {
+ case Int32Type => sb.append("Int")
case _ => sb.append("Type?")
}
@@ -121,6 +122,29 @@ object PrettyPrinter {
ind(nsb); nsb.append("}\n")
}
+ case FunDef(id, rt, args, body, pre, post) => {
+ var nsb = sb
+ ind(nsb)
+ nsb.append("def ")
+ nsb.append(id)
+ nsb.append("(")
+
+ args.foreach(a => {
+ nsb.append("ARG ")
+ })
+
+ nsb.append(") : ")
+ nsb = pp(rt, nsb)
+ nsb.append(" = {\n")
+
+ ind(nsb)
+ nsb = pp(body, nsb)
+ nsb.append("\n")
+
+ ind(nsb)
+ nsb.append("}\n")
+ }
+
case _ => sb.append("Defn?")
}
}
diff --git a/src/funcheck/util/FreshNameCreator.scala b/src/funcheck/util/FreshNameCreator.scala
index b5115b77b0c8c0fbf64339c3e6e2fe0371e6171b..3e51a5e4206c392a8bc92818f51f8df277dabcae 100644
--- a/src/funcheck/util/FreshNameCreator.scala
+++ b/src/funcheck/util/FreshNameCreator.scala
@@ -1,6 +1,5 @@
package funcheck.util
-
trait FreshNameCreator {
var fresh: scala.tools.nsc.util.FreshNameCreator
}