diff --git a/src/main/java/leon/codegen/runtime/CaseClass.java b/src/main/java/leon/codegen/runtime/CaseClass.java
index ea27c7853b4fb0f9a2eae287d186a00f73353e42..bbbdb92f8a41797e455477c5974424f1d2c15718 100644
--- a/src/main/java/leon/codegen/runtime/CaseClass.java
+++ b/src/main/java/leon/codegen/runtime/CaseClass.java
@@ -1,5 +1,7 @@
package leon.codegen.runtime;
public interface CaseClass {
- public abstract Object[] productElements();
+ public abstract Object[] productElements();
+
+ public abstract String productName();
}
diff --git a/src/main/java/leon/codegen/runtime/Map.java b/src/main/java/leon/codegen/runtime/Map.java
index b82ba05c9090677d713d0af74b9b8e937ae66c78..0bdb221c1939dd3ba995e05ec437d24c3f4a2fc6 100644
--- a/src/main/java/leon/codegen/runtime/Map.java
+++ b/src/main/java/leon/codegen/runtime/Map.java
@@ -1,10 +1,11 @@
package leon.codegen.runtime;
import java.util.Arrays;
+import java.util.Iterator;
import java.util.TreeMap;
/** If someone wants to make it an efficient implementation of immutable
- * sets, go ahead. */
+ * maps, go ahead. */
public final class Map {
private final TreeMap<Object,Object> _underlying;
@@ -16,22 +17,25 @@ public final class Map {
_underlying = new TreeMap<Object,Object>();
}
- // For Maps, it's simpler to build them by starting with empty and putting
- // the elements in.
+ private Map(TreeMap<Object,Object> u) {
+ _underlying = u;
+ }
+
+ // Uses mutation! Useful at building time.
public void add(Object key, Object value) {
_underlying.put(key, value);
}
- private Map(TreeMap<Object,Object> u) {
- _underlying = u;
+ public Iterator<java.util.Map.Entry<Object,Object>> getElements() {
+ return _underlying.entrySet().iterator();
}
public boolean isDefinedAt(Object element) {
- return underlying().containsKey(element);
+ return _underlying.containsKey(element);
}
public Object get(Object k) throws LeonCodeGenRuntimeException {
- Object result = underlying().get(k);
+ Object result = _underlying.get(k);
if(result == null) {
throw new LeonCodeGenRuntimeException("Get of undefined key.");
}
@@ -39,12 +43,52 @@ public final class Map {
}
public int size() {
- return underlying().size();
+ return _underlying.size();
}
public Map union(Map s) {
- TreeMap<Object,Object> n = new TreeMap<Object,Object>(underlying());
+ TreeMap<Object,Object> n = new TreeMap<Object,Object>(_underlying);
n.putAll(s.underlying());
return new Map(n);
}
+
+ @Override
+ public boolean equals(Object that) {
+ if(that == this) return true;
+ if(!(that instanceof Map)) return false;
+
+ Map other = (Map)that;
+
+ if(this.size() != other.size()) return false;
+
+ for(java.util.Map.Entry<Object,Object> entry : _underlying.entrySet()) {
+ Object there = other.underlying().get(entry.getKey());
+ if(there == null || !entry.getValue().equals(there)) return false;
+ }
+
+ return true;
+ }
+
+ @Override
+ public String toString() {
+ StringBuilder sb = new StringBuilder();
+ sb.append("Map(");
+ boolean first = true;
+ for(java.util.Map.Entry<Object,Object> entry : _underlying.entrySet()) {
+ if(!first) {
+ sb.append(", ");
+ first = false;
+ }
+ sb.append(entry.getKey().toString());
+ sb.append(" -> ");
+ sb.append(entry.getValue().toString());
+ }
+ sb.append(")");
+ return sb.toString();
+ }
+
+ @Override
+ public int hashCode() {
+ return _underlying.hashCode();
+ }
}
diff --git a/src/main/java/leon/codegen/runtime/Set.java b/src/main/java/leon/codegen/runtime/Set.java
index f882fdf3b377b29a8106d00b657a6778eb3590e6..b38ba90706efbebe08d93e3ea9bc20590718a57a 100644
--- a/src/main/java/leon/codegen/runtime/Set.java
+++ b/src/main/java/leon/codegen/runtime/Set.java
@@ -21,7 +21,7 @@ public final class Set {
_underlying = new TreeSet<Object>(Arrays.asList(elements));
}
- // Uses mutation!
+ // Uses mutation! Useful at building time.
public void add(Object e) {
_underlying.add(e);
}
@@ -52,7 +52,7 @@ public final class Set {
}
public Set union(Set s) {
- TreeSet<Object> n = new TreeSet<Object>(underlying());
+ TreeSet<Object> n = new TreeSet<Object>(_underlying);
n.addAll(s.underlying());
return new Set(n);
}
@@ -79,7 +79,32 @@ public final class Set {
public boolean equals(Object that) {
if(that == this) return true;
if(!(that instanceof Set)) return false;
+
Set other = (Set)that;
- return this.subsetOf(other) && other.subsetOf(this);
+
+ if(this.size() != other.size()) return false;
+
+ return this.subsetOf(other);
+ }
+
+ @Override
+ public String toString() {
+ StringBuilder sb = new StringBuilder();
+ sb.append("Set(");
+ boolean first = true;
+ for(Object o : _underlying) {
+ if(!first) {
+ sb.append(", ");
+ first = false;
+ }
+ sb.append(o.toString());
+ }
+ sb.append(")");
+ return sb.toString();
+ }
+
+ @Override
+ public int hashCode() {
+ return _underlying.hashCode();
}
}
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 1ad3cb99bd85505b0f85319e8f93af8d0e15527c..40cd6c23fbeb39130cad5a7bf829c8931fa3f30e 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -6,7 +6,10 @@ sealed abstract class LeonOption {
}
/** Boolean (on/off) options. Present means "on". */
-case class LeonFlagOption(name: String) extends LeonOption
+case class LeonFlagOption(name: String) extends LeonOption {
+ override def toString() : String = "--" + name
+}
+
/** Options of the form --option=value. */
case class LeonValueOption(name: String, value: String) extends LeonOption {
def splitList : Seq[String] = value.split(':').map(_.trim).filter(!_.isEmpty)
@@ -18,6 +21,8 @@ case class LeonValueOption(name: String, value: String) extends LeonOption {
ctx.reporter.error("Option --%s takes an integer as value.".format(name))
None
}
+
+ override def toString() : String = "--%s=%s".format(name, value)
}
sealed abstract class LeonOptionDef {
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 6ccb05f24ec05abb2517a6c4cc824ece3ca97559..03f4222cd0f8cba5937d93d616e171aaf2cb58ac 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -14,12 +14,14 @@ import cafebabe.Defaults.constructorName
import cafebabe.Flags._
object CodeGeneration {
- private val BoxedIntClass = "java/lang/Integer"
+ private val BoxedIntClass = "java/lang/Integer"
private val BoxedBoolClass = "java/lang/Boolean"
private val TupleClass = "leon/codegen/runtime/Tuple"
private val SetClass = "leon/codegen/runtime/Set"
+ private val MapClass = "leon/codegen/runtime/Map"
private val CaseClassClass = "leon/codegen/runtime/CaseClass"
+ private val ErrorClass = "leon/codegen/runtime/LeonCodeGenRuntimeException"
def defToJVMName(p : Program, d : Definition) : String = "Leon$CodeGen$" + d.id.uniqueName
@@ -28,6 +30,8 @@ object CodeGeneration {
case BooleanType => "Z"
+ case UnitType => "Z"
+
case c : ClassType =>
env.classDefToClass(c.classDef).map(n => "L" + n + ";").getOrElse("Unsupported class " + c.id)
@@ -37,6 +41,9 @@ object CodeGeneration {
case _ : SetType =>
"L" + SetClass + ";"
+ case _ : MapType =>
+ "L" + MapClass + ";"
+
case _ => throw CompilationException("Unsupported type : " + tpe)
}
@@ -50,10 +57,10 @@ object CodeGeneration {
mkExpr(exprToCompile, ch)(env.withVars(newMapping))
funDef.returnType match {
- case Int32Type | BooleanType =>
+ case Int32Type | BooleanType | UnitType =>
ch << IRETURN
- case _ : ClassType | _ : TupleType | _ : SetType =>
+ case _ : ClassType | _ : TupleType | _ : SetType | _ : MapType =>
ch << ARETURN
case other =>
@@ -68,7 +75,7 @@ object CodeGeneration {
case Variable(id) =>
val slot = slotFor(id)
val instr = id.getType match {
- case Int32Type | BooleanType => ILoad(slot)
+ case Int32Type | BooleanType | UnitType => ILoad(slot)
case _ => ALoad(slot)
}
ch << instr
@@ -77,7 +84,7 @@ object CodeGeneration {
mkExpr(d, ch)
val slot = ch.getFreshVar
val instr = i.getType match {
- case Int32Type | BooleanType => IStore(slot)
+ case Int32Type | BooleanType | UnitType => IStore(slot)
case _ => AStore(slot)
}
ch << instr
@@ -93,7 +100,7 @@ object CodeGeneration {
ch << InvokeVirtual(TupleClass, "get", "(I)Ljava/lang/Object;")
mkUnbox(i.getType, ch)
val instr = i.getType match {
- case Int32Type | BooleanType => IStore(s)
+ case Int32Type | BooleanType | UnitType => IStore(s)
case _ => AStore(s)
}
ch << instr
@@ -107,11 +114,15 @@ object CodeGeneration {
case BooleanLiteral(v) =>
ch << Ldc(if(v) 1 else 0)
+ case UnitLiteral =>
+ ch << Ldc(1)
+
+ // Case classes
case CaseClass(ccd, as) =>
val ccName = env.classDefToClass(ccd).getOrElse {
throw CompilationException("Unknown class : " + ccd.id)
}
- // It's a little ugly that we do it each time. Could be in env.
+ // TODO FIXME It's a little ugly that we do it each time. Could be in env.
val consSig = "(" + ccd.fields.map(f => typeToJVM(f.tpe)).mkString("") + ")V"
ch << New(ccName) << DUP
for(a <- as) {
@@ -134,6 +145,7 @@ object CodeGeneration {
ch << CheckCast(ccName)
ch << GetField(ccName, sid.name, typeToJVM(sid.getType))
+ // Tuples (note that instanceOf checks are in mkBranch)
case Tuple(es) =>
ch << New(TupleClass) << DUP
ch << Ldc(es.size)
@@ -153,6 +165,7 @@ object CodeGeneration {
ch << InvokeVirtual(TupleClass, "get", "(I)Ljava/lang/Object;")
mkUnbox(bs(i - 1), ch)
+ // Sets
case FiniteSet(es) =>
ch << DefaultNew(SetClass)
for(e <- es) {
@@ -190,6 +203,34 @@ object CodeGeneration {
mkExpr(s2, ch)
ch << InvokeVirtual(SetClass, "minus", "(L%s;)L%s;".format(SetClass,SetClass))
+ // Maps
+ case FiniteMap(ss) =>
+ ch << DefaultNew(MapClass)
+ for((f,t) <- ss) {
+ ch << DUP
+ mkBoxedExpr(f, ch)
+ mkBoxedExpr(t, ch)
+ ch << InvokeVirtual(MapClass, "add", "(Ljava/lang/Object;Ljava/lang/Object;)V")
+ }
+
+ case MapGet(m, k) =>
+ val MapType(_, tt) = m.getType
+ mkExpr(m, ch)
+ mkBoxedExpr(k, ch)
+ ch << InvokeVirtual(MapClass, "get", "(Ljava/lang/Object;)Ljava/lang/Object;")
+ mkUnbox(tt, ch)
+
+ case MapIsDefinedAt(m, k) =>
+ mkExpr(m, ch)
+ mkBoxedExpr(k, ch)
+ ch << InvokeVirtual(MapClass, "isDefinedAt", "(Ljava/lang/Object;)Z")
+
+ case MapUnion(m1, m2) =>
+ mkExpr(m1, ch)
+ mkExpr(m2, ch)
+ ch << InvokeVirtual(MapClass, "union", "(L%s;)L%s;".format(MapClass,MapClass))
+
+ // Branching
case IfExpr(c, t, e) =>
val tl = ch.getFreshLabel("then")
val el = ch.getFreshLabel("else")
@@ -210,6 +251,7 @@ object CodeGeneration {
}
ch << InvokeStatic(cn, mn, ms)
+ // Arithmetic
case Plus(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
@@ -225,13 +267,31 @@ object CodeGeneration {
mkExpr(r, ch)
ch << IMUL
+ case Division(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << IDIV
+
+ case Modulo(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << IREM
+
case UMinus(e) =>
mkExpr(e, ch)
ch << INEG
+ // Misc and boolean tests
+ case Error(desc) =>
+ ch << New(ErrorClass) << DUP
+ ch << Ldc(desc)
+ ch << InvokeSpecial(ErrorClass, constructorName, "(Ljava/lang/String;)V")
+ ch << ATHROW
+
// WARNING !!! See remark at the end of mkBranch ! The two functions are
// mutually recursive and will loop if none supports some Boolean construct !
case b if b.getType == BooleanType =>
+ // println("Don't know how to mkExpr for " + b)
val fl = ch.getFreshLabel("boolfalse")
val al = ch.getFreshLabel("boolafter")
ch << Ldc(1)
@@ -250,7 +310,7 @@ object CodeGeneration {
mkExpr(e, ch)
ch << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")
- case BooleanType =>
+ case BooleanType | UnitType =>
ch << New(BoxedBoolClass) << DUP
mkExpr(e, ch)
ch << InvokeSpecial(BoxedBoolClass, constructorName, "(Z)V")
@@ -267,7 +327,7 @@ object CodeGeneration {
case Int32Type =>
ch << New(BoxedIntClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")
- case BooleanType =>
+ case BooleanType | UnitType =>
ch << New(BoxedBoolClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedBoolClass, constructorName, "(Z)V")
case _ =>
@@ -280,7 +340,7 @@ object CodeGeneration {
case Int32Type =>
ch << CheckCast(BoxedIntClass) << InvokeVirtual(BoxedIntClass, "intValue", "()I")
- case BooleanType =>
+ case BooleanType | UnitType =>
ch << CheckCast(BoxedBoolClass) << InvokeVirtual(BoxedBoolClass, "booleanValue", "()Z")
case ct : ClassType =>
@@ -289,6 +349,15 @@ object CodeGeneration {
}
ch << CheckCast(cn)
+ case tt : TupleType =>
+ ch << CheckCast(TupleClass)
+
+ case st : SetType =>
+ ch << CheckCast(SetClass)
+
+ case mt : MapType =>
+ ch << CheckCast(MapClass)
+
case _ =>
throw new CompilationException("Unsupported type in unboxing : " + tpe)
}
@@ -314,6 +383,9 @@ object CodeGeneration {
ch << Label(fl)
mkBranch(Or(es.tail), then, elze, ch)
+ case Implies(l, r) =>
+ mkBranch(Or(Not(l), r), then, elze, ch)
+
case Not(c) =>
mkBranch(c, elze, then, ch)
@@ -324,10 +396,17 @@ object CodeGeneration {
mkExpr(l, ch)
mkExpr(r, ch)
l.getType match {
- case Int32Type | BooleanType => ch << If_ICmpEq(then) << Goto(elze)
- case _ => ch << If_ACmpEq(then) << Goto(elze)
+ case Int32Type | BooleanType | UnitType =>
+ ch << If_ICmpEq(then) << Goto(elze)
+
+ case _ =>
+ ch << InvokeVirtual("java/lang/Object", "equals", "(Ljava/lang/Object;)Z")
+ ch << IfEq(elze) << Goto(then)
}
+ case Iff(l,r) =>
+ mkBranch(Equals(l, r), then, elze, ch)
+
case LessThan(l,r) =>
mkExpr(l, ch)
mkExpr(r, ch)
@@ -351,6 +430,7 @@ object CodeGeneration {
// WARNING !!! mkBranch delegates to mkExpr, and mkExpr delegates to mkBranch !
// That means, between the two of them, they'd better know what to generate !
case other =>
+ // println("Don't know how to mkBranch for " + other)
mkExpr(other, ch)
ch << IfEq(elze) << Goto(then)
}
@@ -424,6 +504,20 @@ object CodeGeneration {
cch.freeze
}
+ locally {
+ val pnm = cf.addMethod("Ljava/lang/String;", "productName")
+ pnm.setFlags((
+ METHOD_ACC_PUBLIC |
+ METHOD_ACC_FINAL
+ ).asInstanceOf[U2])
+
+ val pnch = pnm.codeHandler
+
+ pnch << Ldc(cName) << ARETURN
+
+ pnch.freeze
+ }
+
locally {
val pem = cf.addMethod("[Ljava/lang/Object;", "productElements")
pem.setFlags((
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 1a56b8cfa3921576e57c7a2a5667e335937bc783..4cad603f7f6a5b44fd28e3721c89461fa869f6d5 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -14,29 +14,47 @@ import cafebabe.Flags._
import scala.collection.JavaConverters._
+import java.lang.reflect.Constructor
+
import CodeGeneration._
class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFile], implicit val env: CompilationEnvironment) {
- val jvmClassToDef = classes.map{ case (d, cf) => cf.className -> d }.toMap
+ private val jvmClassToDef = classes.map {
+ case (d, cf) => cf.className -> d
+ }.toMap
+
+ protected[codegen] val loader = {
+ val l = new CafebabeClassLoader
+ classes.values.foreach(l.register(_))
+ l
+ }
- val loader = new CafebabeClassLoader
- classes.values.foreach(loader.register(_))
+ private val caseClassConstructors : Map[CaseClassDef,Constructor[_]] = {
+ (classes collect {
+ case (ccd : CaseClassDef, cf) =>
+ val klass = loader.loadClass(cf.className)
+ // This is a hack: we pick the constructor with the most arguments.
+ val conss = klass.getConstructors().sortBy(_.getParameterTypes().length)
+ assert(!conss.isEmpty)
+ (ccd -> conss.last)
+ }).toMap
+ }
- def writeClassFiles() {
+ private def writeClassFiles() {
for ((d, cl) <- classes) {
cl.writeToFile(cl.className + ".class")
}
}
private var _nextExprId = 0
- def nextExprId = {
+ private def nextExprId = {
_nextExprId += 1
_nextExprId
}
// Currently, this method is only used to prepare arguments to reflective calls.
- // This means it is safe to return AnyRef (and never native values), because
+ // This means it is safe to return AnyRef (as opposed to primitive types), because
// reflection needs this anyway.
private[codegen] def valueToJVM(e: Expr): AnyRef = e match {
case IntLiteral(v) =>
@@ -45,6 +63,10 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
case BooleanLiteral(v) =>
new java.lang.Boolean(v)
+ case CaseClass(ccd, args) =>
+ val cons = caseClassConstructors(ccd)
+ cons.newInstance(args.map(valueToJVM).toArray : _*).asInstanceOf[AnyRef]
+
// just slightly overkill...
case _ =>
compileExpression(e, Seq()).evalToJVM(Seq())
@@ -76,8 +98,16 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
case set : runtime.Set =>
FiniteSet(set.getElements().asScala.map(jvmToValue).toSeq)
+ case map : runtime.Map =>
+ val pairs = map.getElements().asScala.map { entry =>
+ val k = jvmToValue(entry.getKey())
+ val v = jvmToValue(entry.getValue())
+ (k, v)
+ }
+ FiniteMap(pairs.toSeq)
+
case _ =>
- throw CompilationException("MEH Unsupported return value : " + e.getClass)
+ throw CompilationException("Unsupported return value : " + e.getClass)
}
def compileExpression(e: Expr, args: Seq[Identifier]): CompiledExpression = {
@@ -129,8 +159,10 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
loader.register(cf)
- new CompiledExpression(this, cf, args)
+ new CompiledExpression(this, cf, e, args)
}
+
+ // writeClassFiles
}
object CompilationUnit {
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index 0c10fe02a43b555463beeebc1169ce2c0111d0c1..0ae8f949f253ba305db59543004f29c2d05116a3 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -12,23 +12,28 @@ import cafebabe.ByteCodes._
import cafebabe.ClassFileTypes._
import cafebabe.Flags._
-class CompiledExpression(unit: CompilationUnit, cf: ClassFile, argsDecl: Seq[Identifier]) {
+import java.lang.reflect.InvocationTargetException
- def evalToJVM(args: Seq[Expr]): AnyRef = {
- val cl = unit.loader.loadClass(cf.className)
- val meth = cl.getMethods()(0)
+class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr, argsDecl: Seq[Identifier]) {
+ private lazy val cl = unit.loader.loadClass(cf.className)
+ private lazy val meth = cl.getMethods()(0)
+ protected[codegen] def evalToJVM(args: Seq[Expr]): AnyRef = {
assert(args.size == argsDecl.size)
if (args.isEmpty) {
meth.invoke(null)
} else {
- meth.invoke(null, args.map(unit.valueToJVM).toArray)
+ meth.invoke(null, args.map(unit.valueToJVM).toArray : _*)
}
}
- def eval(args: Seq[Expr]): Expr = {
- unit.jvmToValue(evalToJVM(args))
+ // This may throw an exception. We unwrap it if needed.
+ def eval(args: Seq[Expr]) : Expr = {
+ try {
+ unit.jvmToValue(evalToJVM(args))
+ } catch {
+ case ite : InvocationTargetException => throw ite.getCause()
+ }
}
-
}
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9b9702f31621c41d8f233c68690cc99d1ebe1356
--- /dev/null
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -0,0 +1,51 @@
+package leon
+package evaluators
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.TreeOps._
+import purescala.Trees._
+import purescala.TypeTrees._
+
+import codegen.CompilationUnit
+
+class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Evaluator(ctx, unit.program) {
+ val name = "codegen-eval"
+ val description = "Evaluator for PureScala expressions based on compilation to JVM"
+
+ /** Another constructor to make it look more like other `Evaluator`s. */
+ def this(ctx : LeonContext, prog : Program) {
+ this(ctx, CompilationUnit.compileProgram(prog).get) // this .get is dubious...
+ }
+
+
+ def eval(expression : Expr, mapping : Map[Identifier,Expr]) : EvaluationResult = {
+ // ctx.reporter.warning("Using `eval` in CodeGenEvaluator is discouraged. Use `compile` whenever applicable.")
+
+ val toPairs = mapping.toSeq
+ compile(expression, toPairs.map(_._1)).map(e => e(toPairs.map(_._2))).getOrElse(EvaluationError("Couldn't compile expression."))
+ }
+
+ override def compile(expression : Expr, argorder : Seq[Identifier]) : Option[Seq[Expr]=>EvaluationResult] = {
+ import leon.codegen.runtime.LeonCodeGenRuntimeException
+
+ val ce = unit.compileExpression(expression, argorder)
+
+ Some((args : Seq[Expr]) => {
+ try {
+ EvaluationSuccessful(ce.eval(args))
+ } catch {
+ case e : ArithmeticException =>
+ EvaluationFailure(e.getMessage)
+
+ case e : LeonCodeGenRuntimeException =>
+ EvaluationFailure(e.getMessage)
+
+ // Required, because the class may be loaded from a different classloader,
+ // and the check above would fail.
+ case t : Throwable if t.getClass.toString.endsWith("LeonCodeGenRuntimeException") =>
+ EvaluationFailure(t.getMessage)
+ }
+ })
+ }
+}
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
similarity index 63%
rename from src/main/scala/leon/Evaluator.scala
rename to src/main/scala/leon/evaluators/DefaultEvaluator.scala
index 24d0fd06e3b63a17ba67c3647bfecb4f443c1954..a6998f10b2ee4807844be3c40b5487b925e1b045 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -1,46 +1,29 @@
package leon
+package evaluators
import purescala.Common._
-import purescala.Trees._
-import xlang.Trees._
+import purescala.Definitions._
import purescala.TreeOps._
+import purescala.Trees._
import purescala.TypeTrees._
-object Evaluator {
-// Expr should be some ground term. We have call-by-value semantics.
- type EvaluationContext = Map[Identifier,Expr]
-
- sealed abstract class EvaluationResult {
- val finalResult: Option[Expr]
- }
- case class OK(result: Expr) extends EvaluationResult {
- val finalResult = Some(result)
- }
- case class RuntimeError(msg: String) extends EvaluationResult {
- val finalResult = None
- }
- case class TypeError(expression: Expr, expected: TypeTree) extends EvaluationResult {
- lazy val msg = "When typing:\n" + expression + "\nexpected: " + expected + ", found: " + expression.getType
- val finalResult = None
- }
- case class InfiniteComputation() extends EvaluationResult {
- val finalResult = None
- }
- case class ImpossibleComputation() extends EvaluationResult {
- val finalResult = None
- }
-
+import xlang.Trees._
- def eval(context: EvaluationContext, expression: Expr, evaluator: Option[(EvaluationContext)=>Boolean], maxSteps: Int=500000) : EvaluationResult = {
- case class RuntimeErrorEx(msg: String) extends Exception
- case class InfiniteComputationEx() extends Exception
- case class TypeErrorEx(typeError: TypeError) extends Exception
- case class ImpossibleComputationEx() extends Exception
+class DefaultEvaluator(ctx : LeonContext, prog : Program) extends Evaluator(ctx, prog) {
+ val name = "evaluator"
+ val description = "Recursive interpreter for PureScala expressions"
+ private def typeErrorMsg(tree : Expr, expected : TypeTree) : String = "Type error : expected %s, found %s.".format(expected, tree)
+ private case class EvalError(msg : String) extends Exception
+ private case class RuntimeError(msg : String) extends Exception
+
+ private val maxSteps = 50000
+
+ def eval(expression: Expr, mapping : Map[Identifier,Expr]) : EvaluationResult = {
var left: Int = maxSteps
- def rec(ctx: EvaluationContext, expr: Expr) : Expr = if(left <= 0) {
- throw InfiniteComputationEx()
+ def rec(ctx: Map[Identifier,Expr], expr: Expr) : Expr = if(left <= 0) {
+ throw RuntimeError("Diverging computation.")
} else {
// println("Step on : " + expr)
// println(ctx)
@@ -50,12 +33,12 @@ object Evaluator {
if(ctx.isDefinedAt(id)) {
val res = ctx(id)
if(!isGround(res)) {
- throw RuntimeErrorEx("Substitution for identifier " + id.name + " is not ground.")
+ throw EvalError("Substitution for identifier " + id.name + " is not ground.")
} else {
res
}
} else {
- throw RuntimeErrorEx("No value for identifier " + id.name + " in context.")
+ throw EvalError("No value for identifier " + id.name + " in mapping.")
}
}
case Tuple(ts) => {
@@ -70,35 +53,35 @@ object Evaluator {
val first = rec(ctx, e)
rec(ctx + ((i -> first)), b)
}
- case Error(desc) => throw RuntimeErrorEx("Error reached in evaluation: " + desc)
+ case Error(desc) => throw RuntimeError("Error reached in evaluation: " + desc)
case IfExpr(cond, then, elze) => {
val first = rec(ctx, cond)
first match {
case BooleanLiteral(true) => rec(ctx, then)
case BooleanLiteral(false) => rec(ctx, elze)
- case _ => throw TypeErrorEx(TypeError(first, BooleanType))
+ case _ => throw EvalError(typeErrorMsg(first, BooleanType))
}
}
case Waypoint(_, arg) => rec(ctx, arg)
case FunctionInvocation(fd, args) => {
val evArgs = args.map(a => rec(ctx, a))
- // build a context for the function...
+ // build a mapping for the function...
val frame = Map[Identifier,Expr]((fd.args.map(_.id) zip evArgs) : _*)
if(fd.hasPrecondition) {
rec(frame, matchToIfThenElse(fd.precondition.get)) match {
case BooleanLiteral(true) => ;
case BooleanLiteral(false) => {
- throw RuntimeErrorEx("Precondition violation for " + fd.id.name + " reached in evaluation.: " + fd.precondition.get)
+ throw RuntimeError("Precondition violation for " + fd.id.name + " reached in evaluation.: " + fd.precondition.get)
}
- case other => throw TypeErrorEx(TypeError(other, BooleanType))
+ case other => throw RuntimeError(typeErrorMsg(other, BooleanType))
}
}
- if(!fd.hasBody && !context.isDefinedAt(fd.id)) {
- throw RuntimeErrorEx("Evaluation of function with unknown implementation.")
+ if(!fd.hasBody && !mapping.isDefinedAt(fd.id)) {
+ throw EvalError("Evaluation of function with unknown implementation.")
}
- val body = fd.body.getOrElse(context(fd.id))
+ val body = fd.body.getOrElse(mapping(fd.id))
val callResult = rec(frame, matchToIfThenElse(body))
if(fd.hasPostcondition) {
@@ -106,9 +89,8 @@ object Evaluator {
val postBody = replace(Map(ResultVariable() -> Variable(freshResID)), matchToIfThenElse(fd.postcondition.get))
rec(frame + ((freshResID -> callResult)), postBody) match {
case BooleanLiteral(true) => ;
- case BooleanLiteral(false) if !fd.hasImplementation => throw ImpossibleComputationEx()
- case BooleanLiteral(false) => throw RuntimeErrorEx("Postcondition violation for " + fd.id.name + " reached in evaluation.")
- case other => throw TypeErrorEx(TypeError(other, BooleanType))
+ case BooleanLiteral(false) => throw RuntimeError("Postcondition violation for " + fd.id.name + " reached in evaluation.")
+ case other => throw EvalError(typeErrorMsg(other, BooleanType))
}
}
@@ -119,7 +101,7 @@ object Evaluator {
rec(ctx, args.head) match {
case BooleanLiteral(false) => BooleanLiteral(false)
case BooleanLiteral(true) => rec(ctx, And(args.tail))
- case other => throw TypeErrorEx(TypeError(other, BooleanType))
+ case other => throw EvalError(typeErrorMsg(other, BooleanType))
}
}
case Or(args) if args.isEmpty => BooleanLiteral(false)
@@ -127,20 +109,20 @@ object Evaluator {
rec(ctx, args.head) match {
case BooleanLiteral(true) => BooleanLiteral(true)
case BooleanLiteral(false) => rec(ctx, Or(args.tail))
- case other => throw TypeErrorEx(TypeError(other, BooleanType))
+ case other => throw EvalError(typeErrorMsg(other, BooleanType))
}
}
case Not(arg) => rec(ctx, arg) match {
case BooleanLiteral(v) => BooleanLiteral(!v)
- case other => throw TypeErrorEx(TypeError(other, BooleanType))
+ case other => throw EvalError(typeErrorMsg(other, BooleanType))
}
case Implies(l,r) => (rec(ctx,l), rec(ctx,r)) match {
case (BooleanLiteral(b1),BooleanLiteral(b2)) => BooleanLiteral(!b1 || b2)
- case (le,re) => throw TypeErrorEx(TypeError(le, BooleanType))
+ case (le,re) => throw EvalError(typeErrorMsg(le, BooleanType))
}
case Iff(le,re) => (rec(ctx,le),rec(ctx,re)) match {
case (BooleanLiteral(b1),BooleanLiteral(b2)) => BooleanLiteral(b1 == b2)
- case _ => throw TypeErrorEx(TypeError(le, BooleanType))
+ case _ => throw EvalError(typeErrorMsg(le, BooleanType))
}
case Equals(le,re) => {
val lv = rec(ctx,le)
@@ -164,53 +146,55 @@ object Evaluator {
val le = rec(ctx, expr)
le match {
case CaseClass(cd2, args) if cd == cd2 => args(cd.selectorID2Index(sel))
- case _ => throw TypeErrorEx(TypeError(le, CaseClassType(cd)))
+ case _ => throw EvalError(typeErrorMsg(le, CaseClassType(cd)))
}
}
case Plus(l,r) => (rec(ctx,l), rec(ctx,r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 + i2)
- case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case Minus(l,r) => (rec(ctx,l), rec(ctx,r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 - i2)
- case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case UMinus(e) => rec(ctx,e) match {
case IntLiteral(i) => IntLiteral(-i)
- case re => throw TypeErrorEx(TypeError(re, Int32Type))
+ case re => throw EvalError(typeErrorMsg(re, Int32Type))
}
case Times(l,r) => (rec(ctx,l), rec(ctx,r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 * i2)
- case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case Division(l,r) => (rec(ctx,l), rec(ctx,r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 / i2)
- case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
+ case (IntLiteral(i1), IntLiteral(i2)) =>
+ if(i2 != 0) IntLiteral(i1 / i2) else throw RuntimeError("Division by 0.")
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case Modulo(l,r) => (rec(ctx,l), rec(ctx,r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 % i2)
- case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
+ case (IntLiteral(i1), IntLiteral(i2)) =>
+ if(i2 != 0) IntLiteral(i1 % i2) else throw RuntimeError("Modulo by 0.")
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case LessThan(l,r) => (rec(ctx,l), rec(ctx,r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 < i2)
- case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case GreaterThan(l,r) => (rec(ctx,l), rec(ctx,r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 > i2)
- case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case LessEquals(l,r) => (rec(ctx,l), rec(ctx,r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 <= i2)
- case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case GreaterEquals(l,r) => (rec(ctx,l), rec(ctx,r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 >= i2)
- case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case SetUnion(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
case (f@FiniteSet(els1),FiniteSet(els2)) => FiniteSet((els1 ++ els2).distinct).setType(f.getType)
- case (le,re) => throw TypeErrorEx(TypeError(le, s1.getType))
+ case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
case SetIntersection(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
case (f@FiniteSet(els1),FiniteSet(els2)) => {
@@ -218,7 +202,7 @@ object Evaluator {
val baseType = f.getType.asInstanceOf[SetType].base
FiniteSet(newElems).setType(f.getType)
}
- case (le,re) => throw TypeErrorEx(TypeError(le, s1.getType))
+ case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
case SetDifference(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
case (f@FiniteSet(els1),FiniteSet(els2)) => {
@@ -226,17 +210,17 @@ object Evaluator {
val baseType = f.getType.asInstanceOf[SetType].base
FiniteSet(newElems).setType(f.getType)
}
- case (le,re) => throw TypeErrorEx(TypeError(le, s1.getType))
+ case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
case ElementOfSet(el,s) => (rec(ctx,el), rec(ctx,s)) match {
case (e, f @ FiniteSet(els)) => BooleanLiteral(els.contains(e))
- case (l,r) => throw TypeErrorEx(TypeError(r, SetType(l.getType)))
+ case (l,r) => throw EvalError(typeErrorMsg(r, SetType(l.getType)))
}
case SetCardinality(s) => {
val sr = rec(ctx, s)
sr match {
case FiniteSet(els) => IntLiteral(els.size)
- case _ => throw TypeErrorEx(TypeError(sr, SetType(AnyType)))
+ case _ => throw EvalError(typeErrorMsg(sr, SetType(AnyType)))
}
}
@@ -279,9 +263,9 @@ object Evaluator {
case g @ MapGet(m,k) => (rec(ctx,m), rec(ctx,k)) match {
case (FiniteMap(ss), e) => ss.find(_._1 == e) match {
case Some((_, v0)) => v0
- case None => throw RuntimeErrorEx("key not found: " + e)
+ case None => throw RuntimeError("Key not found: " + e)
}
- case (l,r) => throw TypeErrorEx(TypeError(l, MapType(r.getType, g.getType)))
+ case (l,r) => throw EvalError(typeErrorMsg(l, MapType(r.getType, g.getType)))
}
case u @ MapUnion(m1,m2) => (rec(ctx,m1), rec(ctx,m2)) match {
case (f1@FiniteMap(ss1), FiniteMap(ss2)) => {
@@ -289,11 +273,11 @@ object Evaluator {
val newSs = filtered1 ++ ss2
FiniteMap(newSs).setType(f1.getType)
}
- case (l, r) => throw TypeErrorEx(TypeError(l, m1.getType))
+ case (l, r) => throw EvalError(typeErrorMsg(l, m1.getType))
}
case i @ MapIsDefinedAt(m,k) => (rec(ctx,m), rec(ctx,k)) match {
case (FiniteMap(ss), e) => BooleanLiteral(ss.exists(_._1 == e))
- case (l, r) => throw TypeErrorEx(TypeError(l, m.getType))
+ case (l, r) => throw EvalError(typeErrorMsg(l, m.getType))
}
case Distinct(args) => {
val newArgs = args.map(rec(ctx, _))
@@ -301,33 +285,22 @@ object Evaluator {
}
case other => {
- Settings.reporter.error("Error: don't know how to handle " + other + " in Evaluator.")
- throw RuntimeErrorEx("unhandled case in Evaluator")
+ context.reporter.error("Error: don't know how to handle " + other + " in Evaluator.")
+ throw EvalError("Unhandled case in Evaluator : " + other)
}
}
}
- evaluator match {
- case Some(evalFun) =>
- try {
- OK(BooleanLiteral(evalFun(context)))
- } catch {
- case e: Exception => RuntimeError(e.getMessage)
- }
- case None =>
- try {
- OK(rec(context, expression))
- } catch {
- case RuntimeErrorEx(msg) => RuntimeError(msg)
- case InfiniteComputationEx() => InfiniteComputation()
- case TypeErrorEx(te) => te
- case ImpossibleComputationEx() => ImpossibleComputation()
- }
+ try {
+ EvaluationSuccessful(rec(mapping, expression))
+ } catch {
+ case EvalError(msg) => EvaluationError(msg)
+ case RuntimeError(msg) => EvaluationFailure(msg)
}
}
// quick and dirty.. don't overuse.
- def isGround(expr: Expr) : Boolean = {
+ private def isGround(expr: Expr) : Boolean = {
variablesOf(expr) == Set.empty
}
}
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7beda070f28ce84795afb44691e2e124f08906f8
--- /dev/null
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -0,0 +1,40 @@
+package leon
+package evaluators
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+
+abstract class Evaluator(val context : LeonContext, val program : Program) extends LeonComponent {
+
+ /** Evaluates an expression, using `mapping` as a valuation function for the free variables. */
+ def eval(expr : Expr, mapping : Map[Identifier,Expr]) : EvaluationResult
+
+ /** Evaluates a ground expression. */
+ final def eval(expr : Expr) : EvaluationResult = eval(expr, Map.empty)
+
+ /** Compiles an expression into a function, where the arguments are the free variables in the expression.
+ * `argorder` specifies in which order the arguments should be passed.
+ * The default implementation uses the evaluation function each time, but evaluators are free
+ * to (and encouraged to) apply any specialization. */
+ def compile(expr : Expr, argorder : Seq[Identifier]) : Option[Seq[Expr]=>EvaluationResult] = Some(
+ (args : Seq[Expr]) => if(args.size != argorder.size) {
+ EvaluationError("Wrong number of arguments for evaluation.")
+ } else {
+ val mapping = argorder.zip(args).toMap
+ eval(expr, mapping)
+ }
+ )
+}
+
+/** Possible results of expression evaluation. */
+sealed abstract class EvaluationResult(val result : Option[Expr])
+
+/** Represents an evaluation that successfully derived the result `value`. */
+case class EvaluationSuccessful(value : Expr) extends EvaluationResult(Some(value))
+
+/** Represents an evaluation that led to an error (in the program). */
+case class EvaluationFailure(message : String) extends EvaluationResult(None)
+
+/** Represents an evaluation that failed (in the evaluator). */
+case class EvaluationError(message : String) extends EvaluationResult(None)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index e212c1baae702f0eb6fe4b63ecbe119ecad3f0d2..6eee2247c7792a4653fe5fdbb541bb5fc4f023b2 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -68,6 +68,17 @@ object Definitions {
}
}
+ object Program {
+ lazy val empty : Program = Program(
+ FreshIdentifier("empty"),
+ ObjectDef(
+ FreshIdentifier("empty"),
+ Seq.empty,
+ Seq.empty
+ )
+ )
+ }
+
/** Objects work as containers for class definitions, functions (def's) and
* val's. */
case class ObjectDef(id: Identifier, defs : Seq[Definition], invariants: Seq[Expr]) extends Definition {
diff --git a/src/main/scala/leon/solvers/ParallelSolver.scala b/src/main/scala/leon/solvers/ParallelSolver.scala
index b6e66ff07f6dcad7618d18847a2fee61cbf31f21..e2a334df1360b121369eec6b7db7f59b0e3fd925 100644
--- a/src/main/scala/leon/solvers/ParallelSolver.scala
+++ b/src/main/scala/leon/solvers/ParallelSolver.scala
@@ -6,8 +6,6 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-import Evaluator._
-
import scala.actors.Actor
import scala.actors.DaemonActor
import scala.actors.Actor._
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index 3c72656350b097c795c97d3d1a95af6d608a354a..c793d37f853829a684b86197955a5bc53f68e0c1 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -7,7 +7,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.TypeTrees._
-import Evaluator._
+import evaluators._
import scala.util.Random
@@ -16,6 +16,11 @@ class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extend
require(nbTrial.forall(i => i >= 0))
private val reporter = context.reporter
+ private var evaluator : Evaluator = null
+
+ override def setProgram(program : Program) : Unit = {
+ evaluator = new DefaultEvaluator(context, program)
+ }
val name = "QC"
val description = "Solver applying random testing (QuickCheck-like)"
@@ -110,29 +115,26 @@ class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extend
val var2val: Map[Identifier, Expr] = Map(vars.map(v => (v, randomValue(v.getType, bound))).toList: _*)
//reporter.info("Trying with: " + var2val)
- val evalResult = eval(var2val, expression, None)
+ val evalResult = evaluator.eval(expression, var2val)
evalResult match {
- case OK(BooleanLiteral(true)) => {
+ case EvaluationSuccessful(BooleanLiteral(true)) => {
//continue trying
}
- case OK(BooleanLiteral(false)) => {
+
+ case EvaluationSuccessful(BooleanLiteral(false)) => {
reporter.info("Found counter example to formula: " + var2val)
result = Some(false)
stop = true
}
- /* in any of the following case, simply continue with another assignement */
- case InfiniteComputation() => {
- //reporter.info("Model seems to lead to divergent computation.")
- }
- case RuntimeError(msg) => {
- //reporter.info("Model leads to runtime error: " + msg)
- }
- case t @ TypeError(_,_) => {
- //reporter.info("Type error in model evaluation.\n" + t.msg)
- }
- case _ => {
- //reporter.info(" -> candidate model discarded.")
+
+ case EvaluationFailure(_) => {
+ reporter.info("Input leads to runtime error: " + var2val)
+ result = Some(false)
+ stop = true
}
+
+ // otherwise, simply continue with another assignement
+ case EvaluationError(_) => ;
}
iteration += 1
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 676f77e6189bbb968194c03c79d68e009af0333a..49a7c539966b49bb8b499ed2218eb9143f96012f 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -12,6 +12,8 @@ import purescala.Extractors._
import purescala.TreeOps._
import purescala.TypeTrees._
+import evaluators._
+
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
@@ -27,24 +29,42 @@ class FairZ3Solver(context : LeonContext)
val description = "Fair Z3 Solver"
override val definedOptions : Set[LeonOptionDef] = Set(
- LeonFlagOptionDef("checkmodels", "--checkmodels", "Double-check counter-examples"),
- LeonFlagOptionDef("feelinglucky", "--feelinglucky", "Use evaluator to find counter-examples early")
+ LeonFlagOptionDef("checkmodels", "--checkmodels", "Double-check counter-examples with evaluator"),
+ LeonFlagOptionDef("feelinglucky", "--feelinglucky", "Use evaluator to find counter-examples early"),
+ LeonFlagOptionDef("codegen", "--codegen", "Use compiled evaluator instead of interpreter")
)
- val (feelingLucky, checkModels) = locally {
- var lucky = false
- var check = false
+ // What wouldn't we do to avoid defining vars?
+ val (feelingLucky, checkModels, useCodeGen) = locally {
+ var lucky = false
+ var check = false
+ var codegen = false
for(opt <- context.options) opt match {
- case LeonFlagOption("checkmodels") => check = true
- case LeonFlagOption("feelinglucky") => lucky = true
+ case LeonFlagOption("checkmodels") => check = true
+ case LeonFlagOption("feelinglucky") => lucky = true
+ case LeonFlagOption("codegen") => codegen = true
case _ =>
}
- (lucky,check)
+ (lucky,check,codegen)
}
- // this is fixed
+ private var evaluator : Evaluator = null
+
+ override def setProgram(prog : Program) {
+ super.setProgram(prog)
+
+ evaluator = if(useCodeGen) {
+ // TODO If somehow we could not recompile each time we create a solver,
+ // that would be good?
+ new CodeGenEvaluator(context, prog)
+ } else {
+ new DefaultEvaluator(context, prog)
+ }
+ }
+
+ // This is fixed.
protected[leon] val z3cfg = new Z3Config(
"MODEL" -> true,
"MBQI" -> false,
@@ -67,7 +87,7 @@ class FairZ3Solver(context : LeonContext)
private var reverseFunctionMap: Map[Z3FuncDecl, FunDef] = Map.empty
private var axiomatizedFunctions : Set[FunDef] = Set.empty
- def prepareFunctions: Unit = {
+ protected[leon] def prepareFunctions: Unit = {
functionMap = Map.empty
reverseFunctionMap = Map.empty
for (funDef <- program.definedFunctions) {
@@ -105,9 +125,7 @@ class FairZ3Solver(context : LeonContext)
(solver.checkAssumptions(assumptions), solver.getModel, solver.getUnsatCore)
}
- private def validateAndDeleteModel(model: Z3Model, formula: Expr, variables: Set[Identifier], evaluator: Option[(Map[Identifier,Expr])=>Boolean] = None) : (Boolean, Map[Identifier,Expr]) = {
- import Evaluator._
-
+ private def validateModel(model: Z3Model, formula: Expr, variables: Set[Identifier]) : (Boolean, Map[Identifier,Expr]) = {
if(!forceStop) {
val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
@@ -137,31 +155,26 @@ class FairZ3Solver(context : LeonContext)
val asMap = modelToMap(model, variables) ++ functionsAsMap ++ constantFunctionsAsMap
lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
- val evalResult = eval(asMap, formula, evaluator)
+ val evalResult = evaluator.eval(formula, asMap)
evalResult match {
- case OK(BooleanLiteral(true)) => {
+ case EvaluationSuccessful(BooleanLiteral(true)) =>
reporter.info("- Model validated:")
reporter.info(modelAsString)
(true, asMap)
- }
- case RuntimeError(msg) => {
- reporter.info("- Invalid model")
- //reporter.error(modelAsString)
- (false, asMap)
- }
- case OK(BooleanLiteral(false)) => {
+
+ case EvaluationSuccessful(BooleanLiteral(false)) =>
reporter.info("- Invalid model.")
(false, asMap)
- }
- case ImpossibleComputation() => {
- reporter.info("- Invalid Model: the model could not be verified because of insufficient information.")
+
+ case EvaluationFailure(msg) =>
+ reporter.info("- Model leads to runtime error.")
(false, asMap)
- }
- case other => {
- reporter.error("Something went wrong. While evaluating the model, we got this: " + other)
+
+ case EvaluationError(msg) =>
+ reporter.error("Something went wrong. While evaluating the model, we got this : " + msg)
(false, asMap)
- }
+
}
} else {
(false, Map.empty)
@@ -233,8 +246,10 @@ class FairZ3Solver(context : LeonContext)
}
def getNewSolver = new solvers.IncrementalSolver {
+ private val evaluator = enclosing.evaluator
private val feelingLucky = enclosing.feelingLucky
private val checkModels = enclosing.checkModels
+ private val useCodeGen = enclosing.useCodeGen
initZ3
@@ -246,15 +261,16 @@ class FairZ3Solver(context : LeonContext)
}
}
+ private var varsInVC = Set[Identifier]()
+
private var frameGuards = List[Z3AST](z3.mkFreshConst("frame", z3.mkBoolSort))
private var frameExpressions = List[List[Expr]](Nil)
- private var varsInVC = Set[Identifier]()
def entireFormula = And(frameExpressions.flatten)
def push() {
- frameGuards = z3.mkFreshConst("frame", z3.mkBoolSort) :: frameGuards
- frameExpressions = Nil :: frameExpressions
+ frameGuards = z3.mkFreshConst("frame", z3.mkBoolSort) :: frameGuards
+ frameExpressions = Nil :: frameExpressions
}
def halt() {
@@ -262,12 +278,15 @@ class FairZ3Solver(context : LeonContext)
}
def pop(lvl: Int = 1) {
+ // TODO FIXME : this is wrong if lvl != 1.
+ // We could fix it, or change the interface to remove the optional arg.
+
// We make sure we discard the expressions guarded by this frame
solver.assertCnstr(z3.mkNot(frameGuards.head))
// Pop the frames
- frameGuards = frameGuards.tail
- frameExpressions = frameExpressions.tail
+ frameGuards = frameGuards.tail
+ frameExpressions = frameExpressions.tail
}
def check: Option[Boolean] = {
@@ -364,7 +383,7 @@ class FairZ3Solver(context : LeonContext)
val z3model = solver.getModel
if (this.checkModels) {
- val (isValid, model) = validateAndDeleteModel(z3model, entireFormula, varsInVC)
+ val (isValid, model) = validateModel(z3model, entireFormula, varsInVC)
if (isValid) {
foundAnswer(Some(true), model)
@@ -417,7 +436,7 @@ class FairZ3Solver(context : LeonContext)
if (this.feelingLucky && !forceStop) {
// we might have been lucky :D
luckyTime.start
- val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, entireFormula, varsInVC)
+ val (wereWeLucky, cleanModel) = validateModel(solver.getModel, entireFormula, varsInVC)
luckyTime.stop
if(wereWeLucky) {
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index 9debb3a8d340dcc8b9ba594cd242b8c434d122fc..1465ea919f33ec86e31693c37f54de84b99b8cb8 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -1,13 +1,18 @@
-package leon.synthesis
+package leon
+package synthesis
-import leon.purescala.Trees._
-import leon.purescala.TreeNormalizations.linearArithmeticForm
-import leon.purescala.TypeTrees._
-import leon.purescala.Common._
-import leon.Evaluator
-import leon.synthesis.Algebra._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TreeNormalizations.linearArithmeticForm
+import purescala.TypeTrees._
+import purescala.Common._
+
+import synthesis.Algebra._
object LinearEquations {
+ // This is a hack, but the use of an evaluator in this file is itself beyond that.
+ import evaluators._
+ private lazy val evaluator = new DefaultEvaluator(LeonContext(), Program.empty)
//eliminate one variable from normalizedEquation t + a1*x1 + ... + an*xn = 0
//return a mapping for each of the n variables in (pre, map, freshVars)
@@ -70,7 +75,8 @@ object LinearEquations {
val (_, sols) = particularSolution(as, IntLiteral(coef(j)*K(j)(j)) :: coef.drop(j+1).map(IntLiteral(_)).toList)
var i = 0
while(i < sols.size) {
- K(i+j+1)(j) = Evaluator.eval(Map(), sols(i), None).asInstanceOf[Evaluator.OK].result.asInstanceOf[IntLiteral].value
+ // seriously ???
+ K(i+j+1)(j) = evaluator.eval(sols(i)).asInstanceOf[EvaluationSuccessful].value.asInstanceOf[IntLiteral].value
i += 1
}
}
diff --git a/src/test/resources/regression/codegen/Prog001.scala b/src/test/resources/regression/codegen/Prog001.scala
deleted file mode 100644
index 91f9a253f37cdf7a3119d9b68caa8c12457d3b7a..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/codegen/Prog001.scala
+++ /dev/null
@@ -1,18 +0,0 @@
-object Prog001 {
- def fortyTwo() = 42
-
- def plus(x : Int, y : Int) = x + y
-
- def double(x : Int) : Int = {
- val a = x
- a + a
- }
-
- def implies(a : Boolean, b : Boolean) : Boolean = !a || b
-
- def abs(x : Int) : Int = {
- if(x < 0) -x else x
- }
-
- def factorial(i : Int) : Int = if(i <= 1) 1 else (i * factorial(i - 1))
-}
diff --git a/src/test/resources/regression/codegen/Prog002.scala b/src/test/resources/regression/codegen/Prog002.scala
deleted file mode 100644
index 1da0f03c0fa99187cbd693867f04eb72ef8ac9f8..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/codegen/Prog002.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-object Prog002 {
- sealed abstract class List
- case class Nil() extends List
- case class Cons(head : Int, tail : List) extends List
-
- def isNil(l : List) : Boolean = {
- l == Nil()
- }
-
- def size(l : List) : Int = l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }
-}
diff --git a/src/test/resources/regression/codegen/Prog003.scala b/src/test/resources/regression/codegen/Prog003.scala
deleted file mode 100644
index 82958305781e8e1efad738720f0cf5f30ff0e6b0..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/codegen/Prog003.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-object Prog003 {
- // Some tests for tuples
- def wrap(x : Int, b : Boolean) : (Int,Boolean) = (x,b)
-
- def fst(t : (Int,Boolean)) : Int = t._1
-
- def snd(t : (Int,Boolean)) : Boolean = t._2
-
- def swap(t : (Int,Boolean)) : (Boolean,Int) = {
- val (i,b) = t
-
- (b,i)
- }
-}
diff --git a/src/test/resources/regression/codegen/Prog004.scala b/src/test/resources/regression/codegen/Prog004.scala
deleted file mode 100644
index cf5ece1a1a0e9d85ace9fbefdf4f70c43ffe7a15..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/codegen/Prog004.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-object Prog004 {
- def set1() : Set[Int] = {
- Set(6, 7)
- }
-
- def set2() : Set[Int] = {
- set1() ++ Set(4)
- }
-
- def set3() : Set[Int] = {
- set2() ** set1()
- }
-
- def set4() : Set[Int] = {
- set2() -- set1()
- }
-}
diff --git a/src/test/resources/regression/codegen/README b/src/test/resources/regression/codegen/README
deleted file mode 100644
index 2edec540798afef79cf99eae4253420d89fbc890..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/codegen/README
+++ /dev/null
@@ -1,2 +0,0 @@
-This directory contains PureScala programs for which compilation (codegen)
-should always succeed entirely.
diff --git a/src/test/scala/leon/test/codegen/CodeGenEvaluation.scala b/src/test/scala/leon/test/codegen/CodeGenEvaluation.scala
deleted file mode 100644
index 13d4a49484de741320c90acb8539010adf381cad..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/test/codegen/CodeGenEvaluation.scala
+++ /dev/null
@@ -1,191 +0,0 @@
-package leon.test
-package codegen
-
-import leon._
-import leon.plugin.{TemporaryInputPhase, ExtractionPhase}
-import leon.codegen.CompilationUnit
-import leon.purescala.Definitions._
-import leon.purescala.TypeTrees.TypeErrorException
-
-import org.scalatest.FunSuite
-
-import TestUtils._
-
-class CodeGenEvaluation extends FunSuite {
- private var counter : Int = 0
- private def nextInt() : Int = {
- counter += 1
- counter
- }
-
- object CodeTestPhase extends LeonPhase[Program,Option[CompilationUnit]] {
- val name = "CodeGen"
- val description = "Compiles a Leon program into Java methods"
-
- def run(ctx : LeonContext)(p : Program) : Option[CompilationUnit] = {
- CompilationUnit.compileProgram(p)
- }
- }
-
- private case class Output(result : Option[CompilationUnit], reporter : Reporter)
-
- private def mkPipeline : Pipeline[List[String], Option[CompilationUnit]] =
- ExtractionPhase andThen CodeTestPhase
-
- private def forProgram(name: String)(content: String)(block: Output => Unit) = {
- test("PureScala program %3d: [%s]".format(nextInt(), name)) {
-
- val ctx = LeonContext(
- settings = Settings(
- synthesis = false,
- xlang = false,
- verify = false
- ),
- files = List(),
- reporter = new SilentReporter
- )
-
- val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen CodeTestPhase
-
- val result = pipeline.run(ctx)((content, Nil))
-
- block(Output(result, ctx.reporter))
- }
- }
-
- import purescala.Trees._
-
- def javaEval(unit: CompilationUnit)(ex: Expr): Expr = {
- val cp = unit.compileExpression(ex, Seq())
- cp.eval(Seq())
- }
-
- def getFunction(unit: CompilationUnit, name: String): FunDef = {
- unit.program.definedFunctions.find(_.id.toString == name) match {
- case Some(fd) =>
- fd
- case _ =>
- throw new AssertionError("Could not find any function named '"+name+"'")
- }
- }
-
- def getCaseClass(unit: CompilationUnit, name: String): CaseClassDef = {
- unit.program.mainObject.caseClassDef(name)
- }
-
- forProgram("Simple Evaluation")(
- """
-object Prog001 {
- def fortyTwo() = 42
-
- def plus(x : Int, y : Int) = x + y
-
- def double(x : Int) : Int = {
- val a = x
- a + a
- }
-
- def implies(a : Boolean, b : Boolean) : Boolean = !a || b
-
- def abs(x : Int) : Int = {
- if(x < 0) -x else x
- }
-
- def factorial(i : Int) : Int = if(i <= 1) 1 else (i * factorial(i - 1))
-}
- """
- ){ out =>
- assert(out.result.isDefined === true)
- val unit = out.result.get
-
- val fact = getFunction(unit, "factorial")
-
- val expr1 = Plus(IntLiteral(5), IntLiteral(42))
- assert(javaEval(unit)(expr1) === IntLiteral(47))
-
-
- val expr2 = Plus(FunctionInvocation(fact, Seq(IntLiteral(5))), IntLiteral(42))
- assert(javaEval(unit)(expr2) === IntLiteral(162))
-
- //Type error
- intercept[TypeErrorException] {
- val expr3 = FunctionInvocation(fact, Seq(BooleanLiteral(false)))
- assert(javaEval(unit)(expr3) != IntLiteral(1), "This should be a type error")
- }
- }
-
- forProgram("Case Classes Evaluation")(
- """
-object Prog002 {
- sealed abstract class List
- case class Nil() extends List
- case class Cons(head : Int, tail : List) extends List
-
- def isNil(l : List) : Boolean = {
- l == Nil()
- }
-
- def size(l : List) : Int = l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }
-
- def conscons(l: List): List = Cons(0, Cons(1, l))
-}
- """
- ){ out =>
- assert(out.result.isDefined === true)
- val unit = out.result.get
-
- val ccNil = getCaseClass(unit, "Nil")
- val ccCons = getCaseClass(unit, "Cons")
- val cons = getFunction(unit, "conscons")
-
- val expr1 = FunctionInvocation(cons, Seq(CaseClass(ccNil, Seq())))
- assert(javaEval(unit)(expr1) === CaseClass(ccCons, Seq(IntLiteral(0), CaseClass(ccCons, Seq(IntLiteral(1), CaseClass(ccNil, Seq()))))))
- }
-
- forProgram("Set Evaluation")(
- """
-object Sets {
- def s0() : Set[Int] = Set()
- def s1() : Set[Int] = Set(1, 2, 3)
- def s2() : Set[Int] = Set(2, 4, 6)
- def s3() : Set[Int] = s1() ++ s2()
- def s4() : Set[Int] = s2() ++ s1()
- def s5() : Set[Int] = s1() ** s2()
- def s6() : Set[Int] = s2() ** s1()
- def s7() : Set[Int] = s1() -- s2()
- def s8() : Set[Int] = s2() -- s1()
-}
- """
- ){ out =>
- assert(out.result.isDefined === true)
- val unit = out.result.get
-
- def asIntSet(e : Expr) : Option[Set[Int]] = e match {
- case FiniteSet(es) =>
- val ois = es.map(_ match {
- case IntLiteral(v) => Some(v)
- case _ => None
- })
- if(ois.forall(_.isDefined))
- Some(ois.map(_.get).toSet)
- else
- None
- case _ => None
- }
-
- def eval(f : String) : Option[Set[Int]] = asIntSet(javaEval(unit)(FunctionInvocation(getFunction(unit, f), Seq())))
-
- assert(eval("s0") === Some(Set.empty[Int]))
- assert(eval("s1") === Some(Set(1, 2, 3)))
- assert(eval("s2") === Some(Set(2, 4, 6)))
- assert(eval("s3") === Some(Set(1, 2, 3, 4, 6)))
- assert(eval("s4") === Some(Set(2, 4, 6, 1, 3)))
- assert(eval("s5") === Some(Set(2)))
- assert(eval("s6") === Some(Set(2)))
- assert(eval("s7") === Some(Set(1, 3)))
- assert(eval("s8") === Some(Set(4, 6)))
- }
-}
diff --git a/src/test/scala/leon/test/codegen/CodeGenRegression.scala b/src/test/scala/leon/test/codegen/CodeGenRegression.scala
deleted file mode 100644
index 75b58e9339a236cd4d1c8d0e3d8731456e2ec511..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/test/codegen/CodeGenRegression.scala
+++ /dev/null
@@ -1,71 +0,0 @@
-package leon.test
-package codegen
-
-import leon._
-import leon.plugin.ExtractionPhase
-import leon.codegen.CodeGenPhase
-import leon.codegen.CompilationResult
-
-import org.scalatest.FunSuite
-
-import java.io.File
-
-import TestUtils._
-
-class CodeGenRegression extends FunSuite {
- private var counter : Int = 0
- private def nextInt() : Int = {
- counter += 1
- counter
- }
-
- private case class Output(result : CompilationResult, reporter : Reporter)
-
- private def mkPipeline : Pipeline[List[String],CompilationResult] =
- ExtractionPhase andThen CodeGenPhase
-
- private def mkTest(file : File)(block: Output=>Unit) = {
- val fullName = file.getPath()
- val start = fullName.indexOf("regression")
- val displayName = if(start != -1) {
- fullName.substring(start, fullName.length)
- } else {
- fullName
- }
-
- test("%3d: %s".format(nextInt(), displayName)) {
- assert(file.exists && file.isFile && file.canRead,
- "Benchmark [%s] is not a readable file".format(displayName))
- val ctx = LeonContext(
- settings = Settings(
- synthesis = false,
- xlang = false,
- verify = false
- ),
- files = List(file),
- reporter = new SilentReporter
- )
-
- val pipeline = mkPipeline
-
- val result = pipeline.run(ctx)(file.getPath :: Nil)
-
- block(Output(result, ctx.reporter))
- }
- }
-
- private def forEachFileIn(cat : String)(block : Output=>Unit) {
- val fs = filesInResourceDir(cat, _.endsWith(".scala"))
-
- for(f <- fs) {
- mkTest(f)(block)
- }
- }
-
- forEachFileIn("regression/codegen/") { output =>
- val Output(result, reporter) = output
- assert(result.successful, "Compilation should be successful.")
- assert(reporter.errorCount === 0)
- assert(reporter.warningCount === 0)
- }
-}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1d2d690bc4b3a423778f503a3aaf9fd9e4c2905b
--- /dev/null
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -0,0 +1,347 @@
+package leon.test
+package evaluators
+
+import leon._
+
+import leon.evaluators._
+
+import leon.plugin.{TemporaryInputPhase, ExtractionPhase}
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
+
+import org.scalatest.FunSuite
+
+class EvaluatorsTests extends FunSuite {
+ private implicit lazy val leonContext = LeonContext(
+ settings = Settings(
+ synthesis = false,
+ xlang = false,
+ verify = false
+ ),
+ files = List(),
+ reporter = new SilentReporter
+ )
+
+ private val evaluatorConstructors : List[(LeonContext,Program)=>Evaluator] = List(
+ new DefaultEvaluator(_,_),
+ new CodeGenEvaluator(_,_)
+ )
+
+ private def prepareEvaluators(implicit ctx : LeonContext, prog : Program) : List[Evaluator] = evaluatorConstructors.map(c => c(leonContext, prog))
+
+ private def parseString(str : String) : Program = {
+ val pipeline = TemporaryInputPhase andThen ExtractionPhase
+
+ val errorsBefore = leonContext.reporter.errorCount
+ val warningsBefore = leonContext.reporter.warningCount
+
+ val program = pipeline.run(leonContext)((str, Nil))
+
+ assert(leonContext.reporter.errorCount === errorsBefore)
+ assert(leonContext.reporter.warningCount === warningsBefore)
+
+ program
+ }
+
+ private def mkCall(name : String, args : Expr*)(implicit p : Program) = {
+ val fDef = p.definedFunctions.find(_.id.name == name) getOrElse {
+ throw new AssertionError("No function named '%s' defined in program.".format(name))
+ }
+
+ FunctionInvocation(fDef, args.toSeq)
+ }
+
+ private def mkCaseClass(name : String, args : Expr*)(implicit p : Program) = {
+ val ccDef = p.mainObject.caseClassDef(name)
+ CaseClass(ccDef, args.toSeq)
+ }
+
+ private def checkCompSuccess(evaluator : Evaluator, in : Expr) : Expr = {
+ evaluator.eval(in) match {
+ case EvaluationFailure(msg) =>
+ throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have succeeded, but it failed (%s).".format(in, evaluator.name, msg))
+
+ case EvaluationError(msg) =>
+ throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have succeeded, but the evaluator had an internal error (%s).".format(in, evaluator.name, msg))
+
+ case EvaluationSuccessful(result) =>
+ result
+ }
+ }
+
+ private def checkComp(evaluator : Evaluator, in : Expr, out : Expr) {
+ val result = checkCompSuccess(evaluator, in)
+ if(result != out)
+ throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced '%s' but produced '%s' instead.".format(in, evaluator.name, out, result))
+ }
+
+ private def checkSetComp(evaluator : Evaluator, in : Expr, out : Set[Int]) {
+ val result = checkCompSuccess(evaluator, in)
+
+ def asIntSet(e : Expr) : Option[Set[Int]] = e match {
+ case FiniteSet(es) =>
+ val ois = es.map(_ match {
+ case IntLiteral(v) => Some(v)
+ case _ => None
+ })
+ if(ois.forall(_.isDefined))
+ Some(ois.map(_.get).toSet)
+ else
+ None
+ case _ => None
+ }
+
+ asIntSet(result) match {
+ case Some(s) if s == out =>
+ ;
+
+ case _ =>
+ throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced a set '%s', but it produced '%s' instead.".format(in, evaluator.name, out, result))
+ }
+ }
+
+ private def checkMapComp(evaluator : Evaluator, in : Expr, out : Map[Int,Int]) {
+ val result = checkCompSuccess(evaluator, in)
+
+ def asIntMap(e : Expr) : Option[Map[Int,Int]] = e match {
+ case FiniteMap(ss) =>
+ val oips : Seq[Option[(Int,Int)]] = ss.map(_ match {
+ case (IntLiteral(f),IntLiteral(t)) => Some(f -> t)
+ case _ => None
+ })
+ if(oips.forall(_.isDefined))
+ Some(oips.map(_.get).toMap)
+ else
+ None
+ case _ => None
+ }
+
+ asIntMap(result) match {
+ case Some(s) if s == out =>
+ ;
+
+ case _ =>
+ throw new AssertionError("Evaluation of '%s' with evaluator '%s' should produced a map '%s', but it produced '%s' instead.".format(in, evaluator.name, out, result))
+ }
+ }
+
+ private def checkError(evaluator : Evaluator, in : Expr) {
+ evaluator.eval(in) match {
+ case EvaluationError(msg) =>
+ throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have failed, but it produced an internal error (%s).".format(in, evaluator.name, msg))
+
+ case EvaluationSuccessful(result) =>
+ throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have failed, but it produced the result '%s' instead.".format(in, evaluator.name, result))
+
+ case EvaluationFailure(_) =>
+ // that's the desired outcome
+ }
+ }
+
+ private def T = BooleanLiteral(true)
+ private def F = BooleanLiteral(false)
+ private def IL(i : Int) = IntLiteral(i)
+
+ test("Arithmetic") {
+ val p = """|object Program {
+ | def plus(x : Int, y : Int) : Int = x + y
+ | def max(x : Int, y : Int) : Int = if(x >= y) x else y
+ | def square(i : Int) : Int = { val j = i; j * i }
+ | def abs(i : Int) : Int = if(i < 0) -i else i
+ | def intSqrt(n : Int) : Int = intSqrt0(abs(n), 0)
+ | def intSqrt0(n : Int, c : Int) : Int = {
+ | val s = square(c+1)
+ | if(s > n) c else intSqrt0(n, c+1)
+ | }
+ | def div(x : Int, y : Int) : Int = (x / y)
+ | def mod(x : Int, y : Int) : Int = (x % y)
+ |}
+ |""".stripMargin
+
+ implicit val prog = parseString(p)
+
+ val evaluators = prepareEvaluators
+
+ for(e <- evaluators) {
+ // Some simple math.
+ checkComp(e, mkCall("plus", IL(60), UMinus(IL(18))), IL(42))
+ checkComp(e, mkCall("max", IL(4), IL(42)), IL(42))
+ checkComp(e, mkCall("max", IL(42), UMinus(IL(42))), IL(42))
+ checkComp(e, mkCall("intSqrt", UMinus(IL(1800))), IL(42))
+ checkComp(e, mkCall("div", IL(7), IL(5)), IL(1))
+ checkComp(e, mkCall("div", IL(7), IL(-5)), IL(-1))
+ checkComp(e, mkCall("div", IL(-7), IL(5)), IL(-1))
+ checkComp(e, mkCall("div", IL(-7), IL(-5)), IL(1))
+ checkComp(e, mkCall("mod", IL(7), IL(5)), IL(2))
+ checkComp(e, mkCall("mod", IL(7), IL(-5)), IL(2))
+ checkComp(e, mkCall("mod", IL(-7), IL(5)), IL(-2))
+ checkComp(e, mkCall("mod", IL(-7), IL(-5)), IL(-2))
+
+ // Things that should crash.
+ checkError(e, mkCall("div", IL(42), IL(0)))
+ checkError(e, mkCall("mod", IL(42), IL(0)))
+ }
+ }
+
+ test("Booleans") {
+ val p = """|object Program {
+ |def and1(x : Boolean, y : Boolean) : Boolean = x && y
+ |def or1(x : Boolean, y : Boolean) : Boolean = x || y
+ |def and2(x : Boolean, y : Boolean) : Boolean = !(!x || !y)
+ |def or2(x : Boolean, y : Boolean) : Boolean = !(!x && !y)
+ |def safe(n : Int) : Boolean = (n != 0 && (1/n == n))
+ |}""".stripMargin
+
+ implicit val prog = parseString(p)
+
+ val evaluators = prepareEvaluators
+
+ for(e <- evaluators) {
+ checkComp(e, mkCall("and1", F, F), F)
+ checkComp(e, mkCall("and1", F, T), F)
+ checkComp(e, mkCall("and1", T, F), F)
+ checkComp(e, mkCall("and1", T, T), T)
+ checkComp(e, mkCall("and2", F, F), F)
+ checkComp(e, mkCall("and2", F, T), F)
+ checkComp(e, mkCall("and2", T, F), F)
+ checkComp(e, mkCall("and2", T, T), T)
+ checkComp(e, mkCall("or1", F, F), F)
+ checkComp(e, mkCall("or1", F, T), T)
+ checkComp(e, mkCall("or1", T, F), T)
+ checkComp(e, mkCall("or1", T, T), T)
+ checkComp(e, mkCall("or2", F, F), F)
+ checkComp(e, mkCall("or2", F, T), T)
+ checkComp(e, mkCall("or2", T, F), T)
+ checkComp(e, mkCall("or2", T, T), T)
+
+ checkComp(e, mkCall("safe", IL(1)), T)
+ checkComp(e, mkCall("safe", IL(2)), F)
+
+ // This one needs short-circuit.
+ checkComp(e, mkCall("safe", IL(0)), F)
+ }
+ }
+
+ test("Case classes") {
+ val p = """|object Program {
+ | sealed abstract class List
+ | case class Nil() extends List
+ | case class Cons(head : Int, tail : List) extends List
+ |
+ | def size(l : List) : Int = l match {
+ | case Nil() => 0
+ | case Cons(_, xs) => 1 + size(xs)
+ | }
+ |
+ | def compare(l1 : List, l2 : List) : Boolean = (l1 == l2)
+ |
+ | def head(l : List) : Int = l match {
+ | case Cons(h, _) => h
+ | }
+ |}""".stripMargin
+
+ implicit val prog = parseString(p)
+
+ val evaluators = prepareEvaluators
+
+ val nil = mkCaseClass("Nil")
+ val cons12a = mkCaseClass("Cons", IL(1), mkCaseClass("Cons", IL(2), mkCaseClass("Nil")))
+ val cons12b = mkCaseClass("Cons", IL(1), mkCaseClass("Cons", IL(2), mkCaseClass("Nil")))
+
+ for(e <- evaluators) {
+ checkComp(e, mkCall("size", nil), IL(0))
+ checkComp(e, mkCall("size", cons12a), IL(2))
+ checkComp(e, mkCall("compare", nil, cons12a), F)
+ checkComp(e, mkCall("compare", cons12a, cons12b), T)
+ checkComp(e, mkCall("head", cons12a), IL(1))
+
+ // Match error
+ checkError(e, mkCall("head", nil))
+ }
+ }
+
+ test("Sets") {
+ val p = """|object Program {
+ | sealed abstract class List
+ | case class Nil() extends List
+ | case class Cons(head : Int, tail : List) extends List
+ |
+ | def content(l : List) : Set[Int] = l match {
+ | case Nil() => Set.empty[Int]
+ | case Cons(x, xs) => Set(x) ++ content(xs)
+ | }
+ |
+ | def finite() : Set[Int] = Set(1, 2, 3)
+ | def build(x : Int, y : Int, z : Int) : Set[Int] = Set(x, y, z)
+ | def union(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 ++ s2
+ | def inter(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 ** s2
+ | def diff(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 -- s2
+ |}""".stripMargin
+
+ implicit val prog = parseString(p)
+
+ val evaluators = prepareEvaluators
+
+ val nil = mkCaseClass("Nil")
+ val cons12 = mkCaseClass("Cons", IL(1), mkCaseClass("Cons", IL(2), mkCaseClass("Nil")))
+
+ val semp = FiniteSet(Seq.empty).setType(SetType(Int32Type))
+ val s123 = FiniteSet(Seq(IL(1), IL(2), IL(3))).setType(SetType(Int32Type))
+ val s246 = FiniteSet(Seq(IL(2), IL(4), IL(6))).setType(SetType(Int32Type))
+
+ for(e <- evaluators) {
+ checkSetComp(e, mkCall("finite"), Set(1, 2, 3))
+ checkSetComp(e, mkCall("content", nil), Set.empty)
+ checkSetComp(e, mkCall("content", cons12), Set(1,2))
+ checkSetComp(e, mkCall("build", IL(1), IL(2), IL(3)), Set(1,2,3))
+ checkSetComp(e, mkCall("build", IL(1), IL(2), IL(2)), Set(1,2))
+ checkSetComp(e, mkCall("union", s123, s246), Set(1,2,3,4,6))
+ checkSetComp(e, mkCall("union", s246, s123), Set(1,2,3,4,6))
+ checkComp(e, Equals(mkCall("union", s123, s246), mkCall("union", s246, s123)), T)
+ checkSetComp(e, mkCall("inter", s123, s246), Set(2))
+ checkSetComp(e, mkCall("inter", s246, s123), Set(2))
+ checkComp(e, Equals(mkCall("inter", s123, s246), mkCall("inter", s246, s123)), T)
+ checkSetComp(e, mkCall("diff", s123, s246), Set(1,3))
+ checkSetComp(e, mkCall("diff", s246, s123), Set(4,6))
+ checkComp(e, Equals(mkCall("diff", s123, s246), mkCall("diff", s246, s123)), F)
+ }
+ }
+
+ test("Maps") {
+ val p = """|object Program {
+ |sealed abstract class PList
+ |case class PNil() extends PList
+ |case class PCons(headfst : Int, headsnd : Int, tail : PList) extends PList
+ |
+ |def toMap(pl : PList) : Map[Int,Int] = pl match {
+ | case PNil() => Map.empty[Int,Int]
+ | case PCons(f,s,xs) => toMap(xs).updated(f, s)
+ |}
+ |
+ |def finite0() : Map[Int,Int] = Map()
+ |def finite1() : Map[Int,Int] = Map(1 -> 2)
+ |def finite2() : Map[Int,Int] = Map(2 -> 3, 1 -> 2)
+ |def finite3() : Map[Int,Int] = finite1().updated(2, 3)
+ |}""".stripMargin
+
+ implicit val prog = parseString(p)
+
+ val evaluators = prepareEvaluators
+
+ val cons1223 = mkCaseClass("PCons", IL(1), IL(2), mkCaseClass("PCons", IL(2), IL(3), mkCaseClass("PNil")))
+
+ for(e <- evaluators) {
+ checkMapComp(e, mkCall("finite0"), Map.empty)
+ checkMapComp(e, mkCall("finite1"), Map(1 -> 2))
+ checkMapComp(e, mkCall("finite2"), Map(1 -> 2, 2 -> 3))
+ checkComp(e, Equals(mkCall("finite1"), mkCall("finite2")), F)
+ checkComp(e, Equals(mkCall("finite2"), mkCall("finite3")), T)
+ checkMapComp(e, mkCall("toMap", cons1223), Map(1 -> 2, 2 -> 3))
+ checkComp(e, MapIsDefinedAt(mkCall("finite2"), IL(2)), T)
+ checkComp(e, MapIsDefinedAt(mkCall("finite2"), IL(3)), F)
+ }
+ }
+}
diff --git a/src/test/scala/leon/test/purescala/LikelyEq.scala b/src/test/scala/leon/test/purescala/LikelyEq.scala
index 5de9e10ea9024d270e53b89e71129c9b9c8ea1a7..f1a6e971b5e2958bd742e76f23c5e1420ace3b59 100644
--- a/src/test/scala/leon/test/purescala/LikelyEq.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEq.scala
@@ -1,17 +1,20 @@
package leon.test.purescala
-import leon.Evaluator._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps.replace
+import leon._
+import leon.evaluators._
import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.TreeOps.replace
+import leon.purescala.Trees._
/*
- * Determine if two expressions over arithmetic variables are likely to be the same
+ * Determine if two expressions over arithmetic variables are likely to be equal.
*
* This is a probabilistic based approach, it does not rely on any external solver and can
* only prove the non equality of two expressions.
*/
object LikelyEq {
+ private lazy val evaluator : Evaluator = new DefaultEvaluator(LeonContext(reporter = new SilentReporter), Program.empty)
private val min = -5
private val max = 5
@@ -29,9 +32,9 @@ object LikelyEq {
compare: (Expr, Expr) => Boolean = (e1, e2) => e1 == e2,
defaultMap: Map[Identifier, Expr] = Map()): Boolean = {
if(vs.isEmpty) {
- val ndm = defaultMap.map{ case (id, expr) => (id, eval(Map(), expr, None).asInstanceOf[OK].result) } //TODO: not quite sure why I need to do this...
- (eval(ndm, e1, None), eval(defaultMap, e2, None)) match {
- case (OK(v1), OK(v2)) => compare(v1, v2)
+ val ndm = defaultMap.map { case (id, expr) => (id, evaluator.eval(expr).asInstanceOf[EvaluationSuccessful].value) } //TODO: not quite sure why I need to do this...
+ (evaluator.eval(e1, ndm), evaluator.eval(e2, defaultMap)) match {
+ case (EvaluationSuccessful(v1), EvaluationSuccessful(v2)) => compare(v1, v2)
case (err1, err2) => sys.error("evaluation could not complete, got: (" + err1 + ", " + err2 + ")")
}
} else {
@@ -46,14 +49,14 @@ object LikelyEq {
val ne1 = replace(m, e1)
val ne2 = replace(m, e2)
val npre = replace(m, pre)
- val ndm = defaultMap.map{ case (id, expr) => (id, eval(m.map{case (Variable(id), t) => (id, t)}, expr, None).asInstanceOf[OK].result) }
- eval(ndm, npre, None) match {
- case OK(BooleanLiteral(false)) =>
- case OK(BooleanLiteral(true)) =>
- val ev1 = eval(ndm, ne1, None)
- val ev2 = eval(ndm, ne2, None)
+ val ndm = defaultMap.map{ case (id, expr) => (id, evaluator.eval(expr, m.map{case (Variable(id), t) => (id, t)}).asInstanceOf[EvaluationSuccessful].value) }
+ evaluator.eval(npre, ndm) match {
+ case EvaluationSuccessful(BooleanLiteral(false)) =>
+ case EvaluationSuccessful(BooleanLiteral(true)) =>
+ val ev1 = evaluator.eval(ne1, ndm)
+ val ev2 = evaluator.eval(ne2, ndm)
(ev1, ev2) match {
- case (OK(v1), OK(v2)) => if(!compare(v1, v2)) isEq = false
+ case (EvaluationSuccessful(v1), EvaluationSuccessful(v2)) => if(!compare(v1, v2)) isEq = false
case (err1, err2) => sys.error("evaluation could not complete, got: (" + err1 + ", " + err2 + ")")
}
case err => sys.error("evaluation of precondition could not complete, got: " + err)
diff --git a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
index dcc0788b0f7125a0125319beff58969774ff03f1..4ba6a5845a67e0fbb602b47970f2feb95d80c405 100644
--- a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
@@ -2,13 +2,11 @@ package leon.test.purescala
import org.scalatest.FunSuite
-import leon.Evaluator
-import leon.purescala.Trees._
import leon.purescala.Common._
+import leon.purescala.Trees._
class LikelyEqSuite extends FunSuite {
-
def i(x: Int) = IntLiteral(x)
val xId = FreshIdentifier("x")
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index a7ca3dac335c46e7b694c3f76f08ffe983f22ce1..b19018e59191c6bb65facd15f51f5d05ae500c9f 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -14,15 +14,10 @@ import org.scalatest.FunSuite
class TreeOpsTests extends FunSuite {
private val silentContext = LeonContext(reporter = new SilentReporter)
- private val emptyProgram = Program(
- FreshIdentifier("Empty"),
- ObjectDef(FreshIdentifier("Empty"), Seq.empty, Seq.empty)
- )
-
test("Path-aware simplifications") {
import leon.solvers.z3.UninterpretedZ3Solver
val solver = new UninterpretedZ3Solver(silentContext)
- solver.setProgram(emptyProgram)
+ solver.setProgram(Program.empty)
// TODO actually testing something here would be better, sorry
// PS
diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
index 0372f4706915855f6639e8da7d926f5dcd6a739e..e94e071bc3b95953947d3af5bf86f781e4b90e15 100644
--- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
@@ -26,14 +26,9 @@ class TimeoutSolverTests extends FunSuite {
}
}
- private val emptyProgram = Program(
- FreshIdentifier("empty"),
- ObjectDef(FreshIdentifier("empty"), Seq.empty, Seq.empty)
- )
-
private def getTOSolver : Solver = {
val s = new TimeoutSolver(new IdioticSolver(LeonContext()), 1)
- s.setProgram(emptyProgram)
+ s.setProgram(Program.empty)
s
}
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index 1f49ae517ab0961489a803fe98f69d2aabbd83ab..95d8706beed1c963776c102ab1a6e3349cae1fb2 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -2,7 +2,6 @@ package leon.test.synthesis
import org.scalatest.FunSuite
-import leon.Evaluator
import leon.purescala.Trees._
import leon.purescala.TypeTrees._
import leon.purescala.TreeOps._
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 77a64fef4dcbfe904c7e480bac5f61daf0384130..74ce1ddc96488bd5a401602de0d788546feac4f5 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -21,7 +21,7 @@ class PureScalaVerificationRegression extends FunSuite {
private def mkPipeline : Pipeline[List[String],VerificationReport] =
leon.plugin.ExtractionPhase andThen leon.verification.AnalysisPhase
- private def mkTest(file : File, forError: Boolean = false)(block: Output=>Unit) = {
+ private def mkTest(file : File, leonOptions : Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
val fullName = file.getPath()
val start = fullName.indexOf("regression")
@@ -31,7 +31,7 @@ class PureScalaVerificationRegression extends FunSuite {
fullName
}
- test("%3d: %s".format(nextInt(), displayName)) {
+ test("%3d: %s %s".format(nextInt(), displayName, leonOptions.mkString(" "))) {
assert(file.exists && file.isFile && file.canRead,
"Benchmark %s is not a readable file".format(displayName))
@@ -41,7 +41,7 @@ class PureScalaVerificationRegression extends FunSuite {
xlang = false,
verify = true
),
- options = List(LeonFlagOption("feelinglucky")),
+ options = leonOptions.toList,
files = List(file),
reporter = new SilentReporter
)
@@ -67,7 +67,8 @@ class PureScalaVerificationRegression extends FunSuite {
_.endsWith(".scala"))
for(f <- fs) {
- mkTest(f, forError)(block)
+ mkTest(f, List(LeonFlagOption("feelinglucky")), forError)(block)
+ mkTest(f, List(LeonFlagOption("codegen"), LeonFlagOption("feelinglucky")), forError)(block)
}
}
diff --git a/unmanaged/common/cafebabe_2.9.2-1.2.jar b/unmanaged/common/cafebabe_2.9.2-1.2.jar
index 47ba4d4848e69cb70792570da656c576701949b6..bd36c4eee8b7548a6bb0e4fba9003597fc5bf2f6 100644
Binary files a/unmanaged/common/cafebabe_2.9.2-1.2.jar and b/unmanaged/common/cafebabe_2.9.2-1.2.jar differ