Commit 2aa2d6c3 authored by Christian Müller's avatar Christian Müller

fix parser to only accept valid signatures

parent 8136e377
......@@ -2,7 +2,9 @@ name := "LoopingWorkflows"
version := "0.1"
scalaVersion := "2.11.8"
scalaVersion := "2.12.1"
EclipseKeys.withBundledScalaContainers := false
libraryDependencies ++= Seq(
"com.typesafe.scala-logging" %% "scala-logging" % "3.5.0",
......@@ -10,6 +12,6 @@ libraryDependencies ++= Seq(
"org.scalactic" %% "scalactic" % "3.0.1",
"org.scalatest" %% "scalatest" % "3.0.1" % "test",
"org.scala-graph" %% "graph-core" % "1.11.4",
"org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.4"
"org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.5"
)
addSbtPlugin("com.artima.supersafe" % "sbtplugin" % "1.1.0")
addSbtPlugin("com.artima.supersafe" % "sbtplugin" % "1.1.2")
......@@ -13,16 +13,27 @@ object ExampleWorkflows extends LazyLogging {
val FOLDER = new File("examples")
val ENDING = ".spec"
val examples = (for (f <- FOLDER.listFiles() if f.isFile() && f.getName.endsWith(ENDING)) yield {
val s = Source.fromFile(f).mkString
val spec = WorkflowParser.parseSpec(s)
def readExamples() = {
val examples = (for (f <- FOLDER.listFiles() if f.isFile() && f.getName.endsWith(ENDING)) yield {
val s = Source.fromFile(f).mkString
val spec = WorkflowParser.parseSpec(s)
// drop file ending
val name = f.getName.replace(ENDING, "")
if (!spec.successful) {
logger.error(s"Parsing of $f unsuccessful: $spec")
name -> None
} else {
name -> Some(spec.get)
}
}) toMap
if (!spec.successful) {
logger.error(s"Parsing of $f unsuccessful: $spec")
// filter out all empty specs
for ((k, v) <- examples if (v.isDefined)) yield {
(k, v.get)
}
// drop file ending
val name = f.getName.replace(ENDING, "")
name -> spec.get
}) toMap
}
val examples = readExamples()
}
......@@ -66,9 +66,7 @@ object Main extends App with LazyLogging {
writeExample(s"results/${name}_causal", cprop)
}
for (k <- ExampleWorkflows.examples.keys) {
generateExample(k)
for ((k, value) <- ExampleWorkflows.examples) {
generateExample(k)
}
}
\ No newline at end of file
......@@ -4,8 +4,9 @@ import scala.util.parsing.combinator._
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.blocks.Workflow._
import com.typesafe.scalalogging.LazyLogging
object WorkflowParser extends RegexParsers {
object WorkflowParser extends RegexParsers with LazyLogging {
def addChoicePredicates(blocks: List[Block]) = {
var num = -1;
......@@ -21,12 +22,13 @@ object WorkflowParser extends RegexParsers {
}
}
def buildSig(list: List[Block]) = {
def allpredicates(list: List[Block]) = {
def predicatesStmt(s: Statement):Set[Fun] = {
// collect from guard
val inguard = s.guard.collect({
case f:Fun => List(f)
})
// changing function
val ch = Fun(s.fun, s.tuple)
inguard :+ ch toSet
}
......@@ -38,21 +40,46 @@ object WorkflowParser extends RegexParsers {
}
}
val preds = list flatMap predicates
list flatMap predicates
}
def checkSig(list: List[Block]) = {
val preds = allpredicates(list)
// Filter to just the first
val filtered = preds groupBy (_.name) map (_._2.head)
val grouped = preds groupBy (_.name)
val (oracles, rels) = filtered.partition(_.name.startsWith("O"))
// Check arities
val checks = for ((k, list) <- grouped) yield {
val sizes = list map (_.params.size)
// all equal
(k, sizes.distinct.size == 1)
}
for ((k, valid) <- checks) {
if (!valid) {
logger.error(s"Predicate $k appears with conflicting arities")
}
}
// all valid?
checks.forall(x => x._2)
}
def buildSig(list: List[Block]) = {
val preds = allpredicates(list)
// Filter to just the first
val filtered = preds groupBy (_.name) map (_._2.head)
val (oracles, rels) = filtered.partition(_.name.startsWith("O"))
Signature(oracles toSet, rels toSet)
}
def VAR = "[a-zA-Z][a-zA-Z0-9]*".r ^^ { str => Var(str) }
def tt = "True" ^^ { _ => True }
def ff = "False" ^^ { _ => False }
def tt = "True" ^^^ True
def ff = "False" ^^^ False
def AND = repsep(SIMPLETERM, "∧") ^^ { case ts => And.make(ts) }
def OR = repsep(SIMPLETERM, "∨") ^^ { case ts => Or.make(ts) }
def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) }
......@@ -73,10 +100,12 @@ object WorkflowParser extends RegexParsers {
def LOOP = "loop" ~> "{" ~> ((MAYBLOCK | BLOCK)+) <~ "}" ^^ { case bs => Loop(bs) }
def WORKFLOW = rep(BLOCK | MAYBLOCK | LOOP) ^^ { case blocks => {
val choiceblocks = addChoicePredicates(blocks)
Workflow(buildSig(choiceblocks), choiceblocks)
}}
def WORKFLOW = rep(BLOCK | MAYBLOCK | LOOP) ^? {
case blocks if checkSig(blocks) => {
val choiceblocks = addChoicePredicates(blocks)
Workflow(buildSig(choiceblocks), choiceblocks)
}
}
def SPEC = "Workflow" ~> WORKFLOW ~ (("Declassify" ~> TERM)?) ~ ("Target" ~> FUN) ^^ { case w ~ decl ~ tar => Spec(w, decl.getOrElse(True), tar) }
......
......@@ -3,12 +3,21 @@ package de.tum.workflows.blocks
import de.tum.workflows.foltl.FOLTL._
case class Signature(oracles: Set[Fun], preds: Set[Fun])
object Signature {
val EMPTY = Signature(Set(), Set())
}
case class Workflow(sig: Signature, steps: List[Block]) {
override def toString() = steps.mkString("\n")
}
object Workflow {
val EMPTY = Workflow(Signature.EMPTY, List())
}
case class Spec(w: Workflow, declass: Term, target: Fun)
object Spec {
val EMPTY = Spec(Workflow.EMPTY, True, Fun("NOTHING", List()))
}
abstract sealed class Block
......
......@@ -52,6 +52,7 @@ object FOLTL {
case class Fun(name: String, ind: Option[String], params: List[Var]) extends Term {
override def toString() = name + Utils.mkString(ind, "(", "", ")") + params.mkString("(", ",", ")")
def updatedParams(index: Int, p:Var) = Fun(name, ind, params.updated(index, p))
def updatedParams(list: List[Var]) = Fun(name, ind, list)
}
trait Quantifier extends Term {
......
......@@ -26,9 +26,12 @@ object Causal {
Forall(c.params.drop(1), Eq(newc.in(t1), newc.in(t2)))
}
val vexist = outputs flatMap (_.params) toList
val max = outputs.map(_.params.length).max
val vexist = (for (num <- 1 until max) yield { Var(s"causalce$num") }) toList
val agents = agent :: vexist
val violations = for (o <- outputs toList) yield {
val newo = o.updatedParams(0, agent)
val newo = o.updatedParams(agents.take(o.params.length))
Neg(Eq(newo.in(t1), newo.in(t2)))
}
......
......@@ -81,7 +81,7 @@ class EncodingTest extends FlatSpec {
val choices = Set(Fun("choice0", List("x", "y")))
val Rab = Fun("R", List("a", "b"))
val s = Spec(Workflow(Signature(Set(), Set()), List()), True, Rab)
val s = Spec(Workflow.EMPTY, True, Rab)
val nonint = Noninterference(choices, s, "t1", "t2")
......@@ -101,7 +101,7 @@ class EncodingTest extends FlatSpec {
choices should be (Set(Fun("choice0", List("x", "s"))))
val ce = Fun("R", List("ax", "as"))
val s = Spec(Workflow(Signature(Set(), Set()), List()), True, ce)
val s = Spec(Workflow.EMPTY, True, ce)
val noninter = Noninterference(choices, s, t1, t2)
noninter should be (
......
......@@ -135,6 +135,16 @@ class ParserTest extends FlatSpec {
testResult(s, w)
}
it should "fail on conflicting arities" in {
val s = """
forallmay x,s
O(x) -> R += (x,s)
forall x,y,s
O(s) -> R += (x,y,s)
"""
WorkflowParser.parseWorkflow(s).successful should be (false)
}
"Spec Parser" should "parse simpleNochoice" in {
val s = """
......@@ -185,5 +195,4 @@ class ParserTest extends FlatSpec {
testSpecResult(s, w, Fun("O", List("x")), t)
}
}
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment