Skip to content
Snippets Groups Projects
Commit 2bac2209 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Web interface moved to epfl-lara/leon-web

parent a7497d3e
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 1259 deletions
web/.gitignore deleted 100644 → 0
+ 0
− 15
View file @ a7497d3e
conf/local.conf
logs
project/project
project/target
target
tmp
.history
dist
/.idea
/*.iml
/out
/.idea_modules
/.classpath
/.project
/RUNNING_PID
web/README deleted 100644 → 0
+ 0
− 21
View file @ a7497d3e
HOWTO RUN LEON ONLINE
*********************
$ cd path/to/leon-2.0
$ sbt package script
$ cd web
$ source ../setupenv
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
!!! Make sure SCALA_HOME is SET! !!!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
** On laraserver **
$ export LD_LIBRARY_PATH=/localhome/leonweb/git/z3/build/
$ play "start -Dapp.prefix=/leon"
** Locally **
$ play run
web/app/controllers/Application.scala deleted 100644 → 0
+ 0
− 36
View file @ a7497d3e
package leon.web
package controllers
import play.api._
import play.api.mvc._
import play.api.libs.json._
import play.api.libs.json.Json._
import play.api.libs.json.Writes._
import examples._
import models.LeonConsole
object Application extends Controller {
val examples = VerificationExamples.allExamples ++ SynthesisExamples.allExamples
def index(powermode : Boolean) = Action { implicit request =>
val prefix = Play.current.configuration.getString("app.prefix").getOrElse("")
Ok(views.html.index(examples, VerificationExamples.default, prefix, powermode))
}
def getExample(id: Int) = Action {
examples.lift.apply(id) match {
case Some(ex) =>
Ok(toJson(Map("status" -> "success", "code" -> ex.code)))
case None =>
Ok(toJson(Map("status" -> "error", "errormsg" -> "Unknown example")))
}
}
def openConsole() = WebSocket.async[JsValue] { request =>
LeonConsole.open
}
}
web/app/examples/Example.scala deleted 100644 → 0
+ 0
− 3
View file @ a7497d3e
package examples
case class Example(title: String, kind: String, code: String)
web/app/examples/SynthesisExamples.scala deleted 100644 → 0
+ 0
− 87
View file @ a7497d3e
package examples
object SynthesisExamples {
var allExamples = List[Example]()
def newExample(title: String, code: String) {
allExamples = allExamples ::: Example(title, "synthesis", code) :: Nil
}
newExample("ADT Induction", """
import scala.collection.immutable.Set
import leon.Annotations._
import leon.Utils._
object SortedList {
sealed abstract class List
case class Cons(head: Int, tail: List) extends List
case class Nil() extends List
// proved with unrolling=0
def size(l: List) : Int = (l match {
case Nil() => 0
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
//def sizeSynth(l: List): Int = choose{ (i: Int) => i >= 0 && sizeSynth(Cons(0, l)) == i + 1}
def content(l: List): Set[Int] = l match {
case Nil() => Set.empty[Int]
case Cons(i, t) => Set(i) ++ content(t)
}
//def artifialSubcase(v : Int) = choose {
// (out : List) =>
// content(out) == (content(Nil()) -- Set(v))
//}
def deleteSynth(in: List, v: Int) = choose {
(out: List) =>
// This spec is too weak. Maybe use later as bad example?
//!(content(out) contains v) && size(out)+1 >= size(in)
(content(out) == (content(in) -- Set(v)))
}
def concatSynth(in1: List, in2: List) = choose {
(out : List) =>
content(out) == content(in1) ++ content(in2)
}
def isSorted(l: List): Boolean = l match {
case Nil() => true
case Cons(x, Nil()) => true
case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
}
}""".trim)
newExample("Binary Tree", """
import scala.collection.immutable.Set
import leon.Annotations._
import leon.Utils._
object BinaryTree {
sealed abstract class Tree
case class Node(left : Tree, value : Int, right : Tree) extends Tree
case class Leaf() extends Tree
def content(t : Tree): Set[Int] = t match {
case Leaf() => Set.empty[Int]
case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
}
def delete(in : Tree, v : Int) = choose { (out : Tree) =>
content(out) == (content(in) -- Set(v))
}
}
""".trim)
newExample("Seconds to Time", """
import leon.Utils._
object Sec2Time {
def s2t(total: Int) : (Int, Int, Int) = choose((h: Int, m: Int, s: Int) => 3600*h + 60*m + s == total && h >= 0 && m >= 0 && m < 60 && s >= 0 && s < 60)
}
""".trim)
}
web/app/examples/VerificationExamples.scala deleted 100644 → 0
+ 0
− 707
View file @ a7497d3e
This diff is collapsed.
web/app/models/LeonConsole.scala deleted 100644 → 0
+ 0
− 195
View file @ a7497d3e
package leon.web
package models
import akka.actor._
import akka.util.duration._
import play.api._
import play.api.libs.json._
import play.api.libs.iteratee._
import play.api.libs.concurrent._
import play.api.libs.json.Json._
import play.api.libs.json.Writes._
import akka.util.Timeout
import akka.pattern.ask
import play.api.Play.current
import leon.{LeonContext, Settings, Reporter}
import leon.plugin.{TemporaryInputPhase, ExtractionPhase}
import leon.synthesis.SynthesisPhase
import leon.verification.AnalysisPhase
object LeonConsole {
def open: Promise[(Iteratee[JsValue,_],Enumerator[JsValue])] = {
import ConsoleProtocol._
val session = Akka.system.actorOf(Props[ConsoleSession])
implicit val timeout = Timeout(1.seconds)
(session ? Init).asPromise.map {
case InitSuccess(enumerator) =>
// Create an Iteratee to consume the feed
val iteratee = Iteratee.foreach[JsValue] { event =>
(event \ "action").as[String] match {
case "start" =>
session ! Start((event \ "mode").as[String], (event \ "code").as[String])
case "startpower" =>
session ! StartPower((event \ "flags").asOpt[String].getOrElse(""), (event \ "code").as[String])
case "stop" =>
session ! Stop
case _ =>
}
}.mapDone { _ =>
session ! Quit
}
(iteratee,enumerator)
case InitFailure(error: String) =>
// Connection error
// A finished Iteratee sending EOF
val iteratee = Done[JsValue,Unit]((),Input.EOF)
// Send an error and close the socket
val enumerator = Enumerator[JsValue](toJson(
Map("kind" -> "error", "message" -> error)
)).andThen(Enumerator.enumInput(Input.EOF))
(iteratee,enumerator)
}
}
}
class ConsoleSession extends Actor {
import ConsoleProtocol._
var isStarted = false
var channel: PushEnumerator[JsValue] = _
var reporter: WSReporter = _
def log(msg: String) = {
channel.push(toJson(Map("kind" -> "log", "message" -> msg)))
}
def error(msg: String) = {
channel.push(toJson(Map("kind" -> "error", "message" -> msg)))
}
def event(kind: String) = {
channel.push(toJson(Map("kind" -> "event", "event" -> kind)))
}
def receive = {
case Init =>
channel = Enumerator.imperative[JsValue]()
reporter = WSReporter(channel)
sender ! InitSuccess(channel)
case Start(mode, code) =>
log("Welcome to LeonOnline!")
log("Processing request...")
val classPath = Play.current.configuration.getString("app.classpath").map(_.split(":").toList).getOrElse(Settings.defaultClassPath())
mode match {
case "verification" =>
event("started")
isStarted = true
var ctx = leon.Main.processOptions(reporter, "--timeout=2" :: Nil)
ctx = ctx.copy(settings = ctx.settings.copy(classPath = classPath))
val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen AnalysisPhase
val analysisResults = pipeline.run(ctx)((code, Nil))
log(analysisResults.summaryString)
event("stopped")
case "synthesis" =>
event("started")
isStarted = true
var ctx = leon.Main.processOptions(reporter, "--synthesis" :: "--parallel" :: "--timeout=10" :: Nil)
ctx = ctx.copy(settings = ctx.settings.copy(classPath = classPath))
val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen SynthesisPhase
pipeline.run(ctx)((code, Nil))
event("stopped")
case _ =>
error("Invalid request mode: "+mode)
}
case StartPower(flags, code) =>
val classPath = Play.current.configuration.getString("app.classpath").map(_.split(":").toList).getOrElse(Settings.defaultClassPath())
event("started")
isStarted = true
log("""> ____ __ __ _ _
> __ | _ \ _____ _____ _ __ | \/ | ___ __| | ___ | | __
> __ | |_) / _ \ \ /\ / / _ \ '__| | |\/| |/ _ \ / _` |/ _ \ | | __
> __ | __/ (_) \ V V / __/ | | | | | (_) | (_| | __/ |_| __
> |_| \___/ \_/\_/ \___|_| |_| |_|\___/ \__,_|\___| (_)""".stripMargin('>'))
var ctx = leon.Main.processOptions(reporter, flags.split(" ").filterNot(_.isEmpty).toList)
ctx = ctx.copy(settings = ctx.settings.copy(classPath = classPath))
val pipeline = TemporaryInputPhase andThen leon.Main.computePipeline(ctx.settings)
pipeline.run(ctx)((code, Nil)) match {
case report: leon.verification.VerificationReport => log(report.summaryString)
case report: leon.termination.TerminationReport => log(report.summaryString)
case _ =>
}
event("stopped")
case Stop =>
isStarted = false
event("stopped")
case Quit =>
}
}
object ConsoleProtocol {
case object Init
case class InitSuccess(enum: Enumerator[JsValue])
case class InitFailure(error: String)
case class Start(mode: String, code: String)
case class StartPower(flags : String, code : String)
case object Stop
case object Quit
}
case class WSReporter(channel: PushEnumerator[JsValue]) extends Reporter {
def infoFunction(msg: Any) : Unit = {
channel.push(toJson(Map("kind" -> "log", "message" -> (msg.toString))))
}
def warningFunction(msg: Any) : Unit = {
channel.push(toJson(Map("kind" -> "log", "message" -> ("Warning: "+msg.toString))))
}
def errorFunction(msg: Any) : Unit = {
channel.push(toJson(Map("kind" -> "log", "message" -> ("Error: "+msg.toString))))
}
def fatalErrorFunction(msg: Any) : Nothing = {
sys.error("FATAL: "+msg)
}
}
web/app/views/index.scala.html deleted 100644 → 0
+ 0
− 83
View file @ a7497d3e
@(exs: List[examples.Example], default: examples.Example, prefix: String, powermode : Boolean)(implicit request: RequestHeader)
@main("Leon Online", prefix) {
<div id="allcontent">
<div id="title" class="contentbox"></div>
<div id="contact">
<p>
<i>Leon</i> is developed by the <a alt="LARA Group EPFL" href="http://lara.epfl.ch">LARA</a> group at <a href="http://www.epfl.ch">EPFL</a>.
</p>
</div>
<div id="leonmain" class="contentbox">
<form id="leoninput" method="POST" action="">
<div id="codecolumn">
<div id="codebox">@default.code</div>
<div id="subcodebox">
@if(powermode) {
<input type="text" id="powerflags" value="--timeout=2" placeholder="add any flags here">
}
<input type="submit" id="askbutton" value="Run Leon !">
</div>
<div><textarea id="consolebox"></textarea></div>
</div>
<div id="selectcolumn">
<input type="hidden" id="leon-mode" value="verification">
<h3>Load an Example:</h3>
<div>We provide you with a list of code-examples, select one from the list below to load it:</div>
<select id="example-loader-verification" name="codeexample" onchange="loadExample('verification', '@prefix');">
<option value="">-- Load Example --</option>
@exs.zipWithIndex.collect{ case (ex, i) if ex.kind == "verification" =>
<option value="@i">@ex.title</option>
}
</select>
</div>
</form>
<script>
$(document).ready(function() {
var WS = window['MozWebSocket'] ? MozWebSocket : WebSocket
var leonSocket = new WS("@leon.web.controllers.routes.Application.openConsole().webSocketURL()")
var receiveEvent = function(event) {
var data = JSON.parse(event.data)
if (data.kind == "error") {
alert(data.message);
} else if (data.kind == "log") {
var txt = $("#consolebox")
txt.val(txt.val()+"\n"+data.message);
txt.scrollTop(txt[0].scrollHeight - txt.height())
} else if (data.kind == "event") {
if (data.event == "started") {
$("#askbutton").val("... processing ...")
} else if (data.event == "stopped") {
$("#askbutton").val("Ask Leon!")
}
}
}
leonSocket.onmessage = receiveEvent;
var leonStatus = "stopped";
$("#leoninput").submit(function () {
$("#consolebox").val("");
@if(!powermode) {
var msg = JSON.stringify(
{action: "start", mode: $("#leon-mode").val(), code: editor.getValue()}
);
} else {
var msg = JSON.stringify(
{action: "startpower", flags: $("#powerflags").val(), code: editor.getValue()}
);
}
leonSocket.send(msg);
return false;
});
});
</script>
</div>
</div>
}
web/app/views/main.scala.html deleted 100644 → 0
+ 0
− 18
View file @ a7497d3e
@(title: String, prefix: String)(content: Html)
<!DOCTYPE html>
<html>
<head>
<title>@title</title>
<link href="@prefix@routes.Assets.at("images/lambda-ico.png")" type="image/png" rel="icon">
<link rel="stylesheet" media="screen" href="@prefix@routes.Assets.at("stylesheets/leon.css")">
<script src="@prefix@routes.Assets.at("javascripts/jquery-1.8.3.min.js")" type="text/javascript"></script>
<script src="http://d1n0x3qji82z53.cloudfront.net/src-min-noconflict/ace.js" type="text/javascript" charset="utf-8"></script>
<script src="@prefix@routes.Assets.at("javascripts/leon.js")" type="text/javascript"></script>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
@content
</body>
</html>
web/conf/application.conf deleted 100644 → 0
+ 0
− 52
View file @ a7497d3e
# This is the main configuration file for the application.
# ~~~~~
# Secret key
# ~~~~~
# The secret key is used to secure cryptographics functions.
# If you deploy your application to several instances be sure to use the same key!
application.secret="_JKq[m=o8OG;]F8xD:bGMs^/?KXXb2Huq^KLM=obhIQvsPIwPNJq@sgLWTRCLr4]"
# The application languages
# ~~~~~
application.langs="en"
# Global object class
# ~~~~~
# Define the Global object class for this application.
# Default to Global in the root package.
# global=Global
# Database configuration
# ~~~~~
# You can declare as many datasources as you want.
# By convention, the default datasource is named `default`
#
# db.default.driver=org.h2.Driver
# db.default.url="jdbc:h2:mem:play"
# db.default.user=sa
# db.default.password=
# Evolutions
# ~~~~~
# You can disable evolutions if needed
# evolutionplugin=disabled
# Logger
# ~~~~~
# You can also configure logback (http://logback.qos.ch/), by providing a logger.xml file in the conf directory .
# Root logger:
logger.root=ERROR
# Logger used by the framework:
logger.play=INFO
# Logger provided to your application:
logger.application=DEBUG
# This specifies the prefix under which the web page lies, used almost exclusively for the laraserver setup
app.prefix=""
# Specifies the classpath used by the Scala compiler within Leon
# app.classpath="../library/target/scala-2.9.2/"
web/conf/routes deleted 100644 → 0
+ 0
− 12
View file @ a7497d3e
# Routes
# This file defines all application routes (Higher priority routes first)
# ~~~~
# Home page
GET / leon.web.controllers.Application.index(powermode : Boolean ?= false)
GET /ajax/getExample/:id leon.web.controllers.Application.getExample(id: Int)
GET /openConsole leon.web.controllers.Application.openConsole
# Map static resources from the /public folder to the /assets URL path
GET /assets/*file controllers.Assets.at(path="/public", file)
web/lib/cafebabe_2.9.2-1.2.jar deleted 120000 → 0
+ 0
− 1
View file @ a7497d3e
../../unmanaged/64/cafebabe_2.9.2-1.2.jar
\ No newline at end of file
web/lib/leon_2.9.2-2.0.jar deleted 120000 → 0
+ 0
− 1
View file @ a7497d3e
../../target/scala-2.9.2/leon_2.9.2-2.0.jar
\ No newline at end of file
web/lib/scalaz3.jar deleted 120000 → 0
+ 0
− 1
View file @ a7497d3e
../../unmanaged/64/scalaz3.jar
\ No newline at end of file
web/project/Build.scala deleted 100644 → 0
+ 0
− 18
View file @ a7497d3e
import sbt._
import Keys._
import PlayProject._
object ApplicationBuild extends Build {
val appName = "leononline"
val appVersion = "1.0-SNAPSHOT"
val appDependencies = Seq(
"org.scala-lang" % "scala-compiler" % "2.9.1"
)
val main = PlayProject(appName, appVersion, appDependencies, mainLang = SCALA).settings(
// Add your own project settings here
)
}
web/project/build.properties deleted 100644 → 0
+ 0
− 1
View file @ a7497d3e
sbt.version=0.11.3
\ No newline at end of file
web/project/plugins.sbt deleted 100644 → 0
+ 0
− 8
View file @ a7497d3e
// Comment to get more information during initialization
logLevel := Level.Warn
// The Typesafe repository
resolvers += "Typesafe repository" at "http://repo.typesafe.com/typesafe/releases/"
// Use the Play sbt plugin for Play projects
addSbtPlugin("play" % "sbt-plugin" % "2.0.4")
\ No newline at end of file
web/public/images/lambda-ico.png deleted 100644 → 0
+ 0
− 0
View file @ a7497d3e
web/public/images/lambda-ico.png

587 B

web/public/images/leonlogo.png deleted 100644 → 0
+ 0
− 0
View file @ a7497d3e
web/public/images/leonlogo.png

5.18 KiB

web/public/images/lionbkg.png deleted 100644 → 0
+ 0
− 0
View file @ a7497d3e
web/public/images/lionbkg.png

113 KiB

0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment