Base implementation of an SMTLib printer/solver

project/Build.scala

@@ -74,9 +74,12 @@ object Leon extends Build {
     id = "leon",
     base = file("."),
     settings = Project.defaultSettings ++ LeonProject.settings
-  ).dependsOn(Github.bonsai)
+  ).dependsOn(Github.bonsai, Github.scalaSmtLib)
 
   object Github {
     lazy val bonsai = RootProject(uri("git://github.com/colder/bonsai.git#8f485605785bda98ac61885b0c8036133783290a"))
+
+    private val scalaSmtLibVersion = "160a635e3677a185e2d5bd84669be98fcda8c574"
+    lazy val scalaSmtLib = RootProject(uri("git://github.com/regb/scala-smtlib.git#%s".format(scalaSmtLibVersion)))
   }
 }

src/main/scala/leon/Main.scala

@@ -276,6 +276,8 @@ object Main {
         ctx.timers.outputTable(debug)
       }
 
+      println("time: " + smtlib.SMTLIBSolver.time)
+
     } catch {
       case LeonFatalError(None) =>
         sys.exit(1)

src/main/scala/leon/smtlib/ExprToSExpr.scala

+package leon
+package smtlib
+
+import purescala._
+import Common._
+import Trees._
+import Extractors._
+import TreeOps._
+import TypeTrees._
+import Definitions._
+
+import _root_.smtlib.sexpr
+import sexpr.SExprs._
+import _root_.smtlib.Commands.{Identifier => SmtLibIdentifier, _}
+
+/** This pretty-printer prints an SMTLIB2 representation of the Purescala program */
+object ExprToSExpr {
+
+  //returns the set of free identifier
+  def apply(tree: Expr): (SExpr, Set[Identifier]) = {
+
+    var freeVars: Set[Identifier] = Set()
+    
+    def rec(t: Expr): SExpr = t match {
+      case Variable(id) => {
+        val sym = id2sym(id)
+        freeVars += id
+        sym
+      }
+      //case LetTuple(ids,d,e) => SList(List(
+      //  SSymbol("let"),
+      //  SList(List(ids))
+      case Let(b,d,e) => {
+        val id = id2sym(b)
+        val value = rec(d)
+        val newBody = rec(e)
+        freeVars -= b
+        
+        SList(
+          SSymbol("let"),
+          SList(
+            SList(id, value)
+          ),
+          newBody
+        )
+      }
+
+      case er@Error(_) => {
+        val id = FreshIdentifier("error_value").setType(er.getType)
+        val sym = id2sym(id)
+        freeVars += id
+        sym
+      }
+
+      case And(exprs) => SList(SSymbol("and") :: exprs.map(rec).toList)
+      case Or(exprs) => SList(SSymbol("or") :: exprs.map(rec).toList)
+      case Not(expr) => SList(SSymbol("not"), rec(expr))
+      case Equals(l,r) => SList(SSymbol("="), rec(l), rec(r))
+      case IntLiteral(v) => SInt(v)
+      case BooleanLiteral(v) => SSymbol(v.toString) //TODO: maybe need some builtin type here
+      case StringLiteral(s) => SString(s)
+
+      case Implies(l,r) => SList(SSymbol("=>"), rec(l), rec(r))
+      case Iff(l,r) => SList(SSymbol("="), rec(l), rec(r))
+
+      case Plus(l,r) => SList(SSymbol("+"), rec(l), rec(r))
+      case UMinus(expr) => SList(SSymbol("-"), rec(expr))
+      case Minus(l,r) => SList(SSymbol("-"), rec(l), rec(r))
+      case Times(l,r) => SList(SSymbol("*"), rec(l), rec(r))
+      case Division(l,r) => SList(SSymbol("div"), rec(l), rec(r))
+      case Modulo(l,r) => SList(SSymbol("mod"), rec(l), rec(r))
+      case LessThan(l,r) => SList(SSymbol("<"), rec(l), rec(r))
+      case LessEquals(l,r) => SList(SSymbol("<="), rec(l), rec(r))
+      case GreaterThan(l,r) => SList(SSymbol(">"), rec(l), rec(r))
+      case GreaterEquals(l,r) => SList(SSymbol(">="), rec(l), rec(r))
+
+      case IfExpr(c, t, e) => SList(SSymbol("ite"), rec(c), rec(t), rec(e))
+
+      case FunctionInvocation(fd, args) => SList(id2sym(fd.id) :: args.map(rec).toList)
+
+      //case ArrayFill(length, defaultValue) => SList(
+      //  SList(SSymbol("as"), SSymbol("const"), tpe2sort(tree.getType)),
+      //  rec(defaultValue)
+      //)
+      //case ArrayMake(defaultValue) => SList(
+      //  SList(SSymbol("as"), SSymbol("const"), tpe2sort(tree.getType)),
+      //  rec(defaultValue)
+      //)
+      //case ArraySelect(array, index) => SList(SSymbol("select"), rec(array), rec(index))
+      //case ArrayUpdated(array, index, newValue) => SList(SSymbol("store"), rec(array), rec(index), rec(newValue))
+
+      case CaseClass(ccd, args) if args.isEmpty => id2sym(ccd.id)
+      case CaseClass(ccd, args) => SList(id2sym(ccd.id) :: args.map(rec(_)).toList)
+      case CaseClassSelector(_, arg, field) => SList(id2sym(field), rec(arg))
+
+      case CaseClassInstanceOf(ccd, arg) => {
+        val name = id2sym(ccd.id)
+        val testerName = SSymbol("is-" + name.s)
+        SList(testerName, rec(arg))
+      }
+      case o => sys.error("TODO converting to smtlib: " + o)
+    }
+
+    val res = rec(tree)
+    (res, freeVars)
+  }
+}

src/main/scala/leon/smtlib/PrettyPrinter.scala

+//package leon
+//package smtlib
+//
+//import purescala._
+//import Common._
+//import Trees._
+//import Extractors._
+//import TreeOps._
+//import TypeTrees._
+//import Definitions._
+//
+//import _root_.smtlib.sexpr
+//import sexpr.SExprs._
+//import _root_.smtlib.Commands.{Identifier => SmtLibIdentifier, _}
+//
+//  // prec: there should be no lets and no pattern-matching in this expression
+//  def collectWithPathCondition(matcher: Expr=>Boolean, expression: Expr) : Set[(Seq[Expr],Expr)] = {
+//    var collected : Set[(Seq[Expr],Expr)] = Set.empty
+//
+//      def rec(expr: Expr, path: List[Expr]) : Unit = {
+//        if(matcher(expr)) {
+//          collected = collected + ((path.reverse, expr))
+//        }
+//
+//        expr match {
+//          case Let(i,e,b) => {
+//            rec(e, path)
+//              rec(b, Equals(Variable(i), e) :: path)
+//          }
+//          case IfExpr(cond, thn, els) => {
+//            rec(cond, path)
+//              rec(thn, cond :: path)
+//              rec(els, Not(cond) :: path)
+//          }
+//          case NAryOperator(args, _) => args.foreach(rec(_, path))
+//            case BinaryOperator(t1, t2, _) => rec(t1, path); rec(t2, path)
+//            case UnaryOperator(t, _) => rec(t, path)
+//          case t : Terminal => ;
+//          case _ => scala.sys.error("Unhandled tree in collectWithPathCondition : " + expr)
+//        }
+//      }
+//
+//    rec(expression, Nil)
+//      collected
+//  }
+//}

src/main/scala/leon/smtlib/SExprToExpr.scala

+package leon
+package smtlib
+
+import purescala._
+import Common._
+import Trees._
+import Extractors._
+import TreeOps._
+import TypeTrees._
+import Definitions._
+
+import _root_.smtlib.sexpr
+import sexpr.SExprs._
+import _root_.smtlib.Commands.{Identifier => SmtLibIdentifier, _}
+
+object SExprToExpr {
+
+  def apply(sexpr: SExpr, context: Map[String, Expr], constructors: Map[String, CaseClassDef]): Expr = sexpr match {
+    case SInt(n) => IntLiteral(n.toInt)
+    case SSymbol("TRUE") => BooleanLiteral(true)
+    case SSymbol("FALSE") => BooleanLiteral(false)
+    case SSymbol(s) => constructors.get(s) match {
+      case Some(app) => CaseClass(app, Seq())
+      case None => context(s)
+    }
+    case SList(SSymbol(app) :: args) if(constructors.isDefinedAt(app)) => 
+      CaseClass(constructors(app), args.map(apply(_, context, constructors)))
+
+    case SList(List(SSymbol("LET"), SList(defs), body)) => {
+      val leonDefs: Seq[(Identifier, Expr, String)] = defs.map {
+        case SList(List(SSymbol(sym), value)) => (FreshIdentifier(sym), apply(value, context, constructors), sym)
+      }
+      val recBody = apply(body, context ++ leonDefs.map(p => (p._3, p._1.toVariable)), constructors)
+      leonDefs.foldRight(recBody)((binding, b) => Let(binding._1, binding._2, b))
+    }
+    case SList(SSymbol(app) :: args) => {
+      val recArgs = args.map(arg => apply(arg, context, constructors))
+      app match {
+        case "-" => recArgs match {
+          case List(a) => UMinus(a)
+          case List(a, b) => Minus(a, b)
+        }
+      }
+    }
+    case o => sys.error("TODO converting from s-expr: " + o)
+  }
+
+}

src/main/scala/leon/smtlib/SMTLIBSolver.scala

+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+package smtlib
+
+import solvers.IncrementalSolver
+import utils.Interruptible
+import purescala._
+import Common._
+import Trees._
+import Extractors._
+import TreeOps._
+import TypeTrees._
+import Definitions._
+
+import _root_.smtlib.{PrettyPrinter => CommandPrinter, Commands, CommandResponses, sexpr, Interpreter => SMTLIBInterpreter}
+import Commands.{Identifier => SMTLIBIdentifier, _}
+import CommandResponses.{Error => ErrorResponse, _}
+import sexpr.SExprs._
+import _root_.smtlib.Commands.{Identifier => SmtLibIdentifier, _}
+
+
+class SMTLIBSolver(override val context: LeonContext, 
+                   val program: Program, 
+                   smtlibInterpreterFactory: () => SMTLIBInterpreter) 
+  extends IncrementalSolver with Interruptible {
+
+  override def interrupt: Unit = {}
+  override def recoverInterrupt(): Unit = {}
+
+
+  override def name: String = "smtlib-solver"
+  val out = new java.io.FileWriter("vcs/vc_" + SMTLIBSolver.counter)
+
+  //using a factory, so that creation and call to free are local to this class
+  private val smtlibInterpreter = smtlibInterpreterFactory()
+
+  private var errorConstants: Set[(SSymbol, SExpr)] = Set()
+
+  val defs: Seq[ClassTypeDef] = program.definedClasses
+
+  val partition: Seq[(AbstractClassDef, Seq[CaseClassDef])] = {
+    val parents: Seq[AbstractClassDef] = defs.filter(!_.hasParent).asInstanceOf[Seq[AbstractClassDef]]
+    parents.map(p => (p, defs.filter(c => c.parent match {
+      case Some(p2) => p == p2
+      case None => false
+    }).asInstanceOf[Seq[CaseClassDef]]))
+  }
+
+  val sorts: Seq[SExpr] = partition.map{ case (parent, children) => {
+    val name = id2sym(parent.id)
+    val constructors: List[SExpr] = children.map(child => {
+      val fields: List[SExpr] = child.fields.map{case VarDecl(id, tpe) => SList(id2sym(id), tpe2sort(tpe)) }.toList
+      if(fields.isEmpty) id2sym(child.id) else SList(id2sym(child.id) :: fields)
+    }).toList
+
+    SList(name :: constructors)
+  }}
+  val constructors: Map[String, CaseClassDef] = 
+    partition.unzip._2.flatMap(ccds => ccds.map(ccd => (ccd.id.uniqueName.toUpperCase, ccd))).toMap
+  val sortDecls = NonStandardCommand(SList(SSymbol("declare-datatypes"), SList(), SList(sorts.toList)))
+  val funDefDecls: Seq[Command] = program.definedFunctions.flatMap(fd2sexp)
+  val sortErrors: List[Command] = errorConstants.map(p => DeclareFun(p._1.s, Seq(), p._2)).toList
+
+  def declareConst(id: Identifier): Command = DeclareFun(id2sym(id).s, Seq(), tpe2sort(id.getType))
+
+    //SComment("! THEORY=1") +:
+    //SComment("Generated by Leon") +:
+  sendCommand(sortDecls)
+  sortErrors.foreach(sendCommand(_)) 
+  funDefDecls.foreach(sendCommand)
+
+      //convertedFunDefs.flatMap(_._1) ++
+      //convertedFunDefs.map(_._2) ++
+      //convertedFunDefs.flatMap(_._3) ++
+      //Seq(SList(SSymbol("check-sat")))
+
+  private var freeVars: Set[Identifier] = program.definedFunctions.flatMap(fd => fd.args.map(_.id)).toSet
+  override def assertCnstr(expression: Expr): Unit = {
+
+    val (sexpr, exprFreevars) = ExprToSExpr(expression)
+
+    val newFreeVars: Set[Identifier] = exprFreevars.diff(freeVars)
+    freeVars ++= newFreeVars
+    newFreeVars.foreach(id => sendCommand(declareConst(id)))
+
+    sendCommand(Assert(sexpr))
+  }
+
+  override def check: Option[Boolean] = sendCommand(CheckSat) match {
+    case CheckSatResponse(SatStatus) => Some(true)
+    case CheckSatResponse(UnsatStatus) => Some(false)
+    case CheckSatResponse(UnknownStatus) => None
+  }
+
+  override def getModel: Map[Identifier, Expr] = {
+    val ids: List[Identifier] = freeVars.toList
+    val sexprs: List[SSymbol] = ids.map(id => id2sym(id))
+    val cmd: Command = GetValue(sexprs.head, sexprs.tail)
+
+    val symToIds: Map[SExpr, Identifier] = sexprs.map(s => SSymbol(s.s.toUpperCase)).zip(ids).toMap
+    val GetValueResponse(valuationPairs) = sendCommand(cmd)
+    println("got valuation pairs: " + valuationPairs)
+    valuationPairs.map{ case (sym, value) => (symToIds(sym), SExprToExpr(value, Map(), constructors)) }.toMap
+  }
+
+  override def free() = {
+    sendCommand(Exit)
+    smtlibInterpreter.free()
+    out.close
+    SMTLIBSolver.counter += 1
+  }
+
+  override def push(): Unit = {
+    sendCommand(Push(1))
+  }
+  override def pop(lvl: Int = 1): Unit = {
+    sendCommand(Pop(1))
+  }
+
+  def sendCommand(cmd: Command): CommandResponse = {
+    val startTime = System.currentTimeMillis
+    CommandPrinter(cmd, out)
+    out.write("\n")
+    val response = smtlibInterpreter.eval(cmd)
+    assert(!response.isInstanceOf[Error])
+    SMTLIBSolver.time = SMTLIBSolver.time + (System.currentTimeMillis - startTime)
+    response
+  }
+
+  private def fd2sexp(funDef: FunDef): List[Command] = {
+    val name = id2sym(funDef.id)
+    val returnSort = tpe2sort(funDef.returnType)
+
+    val varDecls: List[(SSymbol, SExpr)] = funDef.args.map(vd => (id2sym(vd.id), tpe2sort(vd.tpe))).toList
+
+    val topLevelVarDecl: List[Command] = varDecls.map{ case (name, tpe) => DeclareFun(name.s, Seq(), tpe) }
+    val funDecl: Command = DeclareFun(name.s, varDecls.map(_._2), returnSort)
+
+    funDecl :: topLevelVarDecl
+  }
+}
+
+object SMTLIBSolver {
+  var counter = 0
+  var time: Long = 0
+}

src/main/scala/leon/smtlib/package.scala

+package leon
+
+import purescala._
+import Common._
+import Trees._
+import Extractors._
+import TreeOps._
+import TypeTrees._
+import Definitions._
+
+import _root_.smtlib.sexpr
+import sexpr.SExprs._
+import _root_.smtlib.Commands.{Identifier => SmtLibIdentifier, _}
+
+package object smtlib {
+
+  private[smtlib] def id2sym(id: Identifier): SSymbol = SSymbol(id.uniqueName)
+  //return a series of declarations, an expression that defines the function, 
+  //and the seq of asserts for pre/post-conditions
+
+
+  def tpe2sort[smtlib](tpe: TypeTree): SExpr = tpe match {
+    case Int32Type => SSymbol("Int")
+    case BooleanType => SSymbol("Bool")
+    case ArrayType(baseTpe) => SList(SSymbol("Array"), SSymbol("Int"), tpe2sort(baseTpe))
+    case AbstractClassType(abs) => id2sym(abs.id)
+    case _ => sys.error("TODO tpe2sort: " + tpe)
+  }
+
+}

src/main/scala/leon/solvers/combinators/UnrollingSolver.scala

@@ -118,6 +118,7 @@ class UnrollingSolver(val context: LeonContext, underlyings: SolverFactory[Incre
           theModel = Some(model)
       }
     }
+    solver.free
     result
 
   } getOrElse {

src/main/scala/leon/verification/AnalysisPhase.scala

@@ -151,7 +151,8 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
 
     val allSolvers = Map(
       "fairz3" -> SolverFactory(() => new FairZ3Solver(ctx, program) with TimeoutSolver),
-      "enum"   -> SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver)
+      "enum"   -> SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver),
+      "smt"    -> SolverFactory(() => new smtlib.SMTLIBSolver(ctx, program, new _root_.smtlib.interpreters.Z3Interpreter))
     )
 
     val reporter = ctx.reporter
@@ -184,7 +185,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
       SolverFactory( () => new PortfolioSolver(ctx, solversToUse.values.toSeq) with TimeoutSolver)
     }
 
-
     val mainSolver = timeout match {
       case Some(sec) =>
         new TimeoutSolverFactory(entrySolver, sec*1000L)