From 928536c94bef29b7eb9cdec975be531f5f0278cc Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Fri, 18 Jan 2013 17:04:38 +0100
Subject: [PATCH] Introduce a "PowerMode" for the web interface.
Add ?powermode=1 to the URL to access PowerMode. For now, all you can do
is set the flags manually. This allows you to run the synthesis or
termination phases from the web, for instance. Remember, with great
power comes great responsibility!
---
web/README | 2 +-
web/app/controllers/Application.scala | 4 ++--
web/app/models/LeonConsole.scala | 31 ++++++++++++++++++++++++++-
web/app/views/index.scala.html | 27 +++++++++++++++++------
web/conf/routes | 2 +-
web/public/stylesheets/leon.css | 12 ++++++++++-
6 files changed, 65 insertions(+), 13 deletions(-)
diff --git a/web/README b/web/README
index 66789901e..89a67e71b 100644
--- a/web/README
+++ b/web/README
@@ -14,7 +14,7 @@ $ source ../setupenv
** On laraserver **
$ export LD_LIBRARY_PATH=/localhome/leonweb/git/z3/build/
- $ play "run -Dapp.prefix=/leon"
+ $ play "start -Dapp.prefix=/leon"
** Locally **
diff --git a/web/app/controllers/Application.scala b/web/app/controllers/Application.scala
index 94a48eba4..ad0dff194 100644
--- a/web/app/controllers/Application.scala
+++ b/web/app/controllers/Application.scala
@@ -14,10 +14,10 @@ object Application extends Controller {
val examples = VerificationExamples.allExamples ++ SynthesisExamples.allExamples
- def index = Action { implicit request =>
+ def index(powermode : Boolean) = Action { implicit request =>
val prefix = Play.current.configuration.getString("app.prefix").getOrElse("")
- Ok(views.html.index(examples, VerificationExamples.default, prefix))
+ Ok(views.html.index(examples, VerificationExamples.default, prefix, powermode))
}
def getExample(id: Int) = Action {
diff --git a/web/app/models/LeonConsole.scala b/web/app/models/LeonConsole.scala
index 32ba4207e..ad3112e7a 100644
--- a/web/app/models/LeonConsole.scala
+++ b/web/app/models/LeonConsole.scala
@@ -35,6 +35,8 @@ object LeonConsole {
(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 _ =>
@@ -102,7 +104,9 @@ class ConsoleSession extends Actor {
val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen AnalysisPhase
- pipeline.run(ctx)((code, Nil))
+ val analysisResults = pipeline.run(ctx)((code, Nil))
+
+ log(analysisResults.summaryString)
event("stopped")
@@ -123,6 +127,30 @@ class ConsoleSession extends Actor {
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
@@ -140,6 +168,7 @@ object ConsoleProtocol {
case class Start(mode: String, code: String)
+ case class StartPower(flags : String, code : String)
case object Stop
diff --git a/web/app/views/index.scala.html b/web/app/views/index.scala.html
index 39c8d5f6a..3bc1aa931 100644
--- a/web/app/views/index.scala.html
+++ b/web/app/views/index.scala.html
@@ -1,4 +1,4 @@
-@(exs: List[examples.Example], default: examples.Example, prefix: String)(implicit request: RequestHeader)
+@(exs: List[examples.Example], default: examples.Example, prefix: String, powermode : Boolean)(implicit request: RequestHeader)
@main("Leon Online", prefix) {
<div id="allcontent">
@@ -12,8 +12,13 @@
<div id="leonmain" class="contentbox">
<form id="leoninput" method="POST" action="">
<div id="codecolumn">
- <div id="codebox">@default.code</div>
- <input type="submit" id="askbutton" value="Ask Leon !">
+ <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">
@@ -51,16 +56,24 @@
}
}
- leonSocket.onmessage = receiveEvent
+ leonSocket.onmessage = receiveEvent;
- var leonStatus = "stopped"
+ 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)
+ leonSocket.send(msg);
return false;
});
});
diff --git a/web/conf/routes b/web/conf/routes
index 38891796c..586dc60cb 100644
--- a/web/conf/routes
+++ b/web/conf/routes
@@ -3,7 +3,7 @@
# ~~~~
# Home page
-GET / leon.web.controllers.Application.index
+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
diff --git a/web/public/stylesheets/leon.css b/web/public/stylesheets/leon.css
index c2c8f7f19..6496e35af 100644
--- a/web/public/stylesheets/leon.css
+++ b/web/public/stylesheets/leon.css
@@ -130,8 +130,18 @@ li {
margin-bottom: 5px;
}
+#subcodebox {
+ margin: 460px 0px 0px 0px;
+}
+
+#powerflags {
+ margin: 0px 0px 5px 0px;
+ border: 1px solid #666666;
+ width: 700px;
+}
+
#askbutton {
- margin: 460px 0px 5px 0px;
+ margin: 0px 0px 5px 0px;
background-color: transparent;
border: 1px solid #666666;
width: 700px;
--
GitLab