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

update transformations

parent 5e41de33
...@@ -209,7 +209,7 @@ object Encoding extends LazyLogging { ...@@ -209,7 +209,7 @@ object Encoding extends LazyLogging {
val MAXINVLENGTH = 800 val MAXINVLENGTH = 800
def toDot(g: WorkflowGraph, elaboration:Option[(InvProperties, Spec)] = None)(labels:Map[Int, String], edges:Set[g.EdgeT]) = { def toDot(g: WorkflowGraph, elaboration:Option[(InvProperties, NISpec)] = None)(labels:Map[Int, String], edges:Set[g.EdgeT]) = {
val root = DotRootGraph( val root = DotRootGraph(
directed = true, directed = true,
id = Some("Invariant Labelling")) id = Some("Invariant Labelling"))
......
...@@ -25,7 +25,7 @@ object ExampleWorkflows extends LazyLogging { ...@@ -25,7 +25,7 @@ object ExampleWorkflows extends LazyLogging {
(sublists toMap) ++ here (sublists toMap) ++ here
} }
def parseExample(s:String):Option[Spec] = { def parseExample(s:String):Option[NISpec] = {
if (!examples.contains(s)) { if (!examples.contains(s)) {
logger.error(s"$s not contained in list of examples") logger.error(s"$s not contained in list of examples")
None None
...@@ -47,7 +47,7 @@ object ExampleWorkflows extends LazyLogging { ...@@ -47,7 +47,7 @@ object ExampleWorkflows extends LazyLogging {
} }
} }
def parsedExamples(prefix:String, folder:File):Map[String, Spec] = { def parsedExamples(prefix:String, folder:File):Map[String, NISpec] = {
val map = for ((name, f) <- examples) yield { val map = for ((name, f) <- examples) yield {
val s = Source.fromFile(f).mkString val s = Source.fromFile(f).mkString
val spec = WorkflowParser.parseSpec(s) val spec = WorkflowParser.parseSpec(s)
......
...@@ -5,7 +5,7 @@ import scala.io.Source ...@@ -5,7 +5,7 @@ import scala.io.Source
import com.typesafe.scalalogging.LazyLogging import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._ import de.tum.workflows.Utils._
import de.tum.workflows.blocks.Spec import de.tum.workflows.blocks.NISpec
import de.tum.workflows.toz3.InvariantChecker import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator import de.tum.workflows.toz3.InvariantGenerator
import de.tum.workflows.toz3.InvProperties import de.tum.workflows.toz3.InvProperties
...@@ -55,7 +55,7 @@ object InvariantCLI extends App with LazyLogging { ...@@ -55,7 +55,7 @@ object InvariantCLI extends App with LazyLogging {
spec.map(generate(new File(file).getName.stripSuffix(".spec"), _, properties)) spec.map(generate(new File(file).getName.stripSuffix(".spec"), _, properties))
} }
def generate(name: String, spec: Spec, properties: InvProperties) { def generate(name: String, spec: NISpec, properties: InvProperties) {
logger.info(s"Encoding Spec:\n$spec") logger.info(s"Encoding Spec:\n$spec")
def invariant = InvariantGenerator.invariantNoninterSingleBS(spec) def invariant = InvariantGenerator.invariantNoninterSingleBS(spec)
......
...@@ -11,7 +11,7 @@ import de.tum.workflows.foltl.Properties ...@@ -11,7 +11,7 @@ import de.tum.workflows.foltl.Properties
import java.io.PrintWriter import java.io.PrintWriter
import java.io.File import java.io.File
import de.tum.workflows.blocks.Workflow import de.tum.workflows.blocks.Workflow
import de.tum.workflows.blocks.Spec import de.tum.workflows.blocks.NISpec
import de.tum.workflows.foltl.FormulaFunctions import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator import de.tum.workflows.toz3.InvariantGenerator
...@@ -38,7 +38,7 @@ object InvariantInspector extends App with LazyLogging { ...@@ -38,7 +38,7 @@ object InvariantInspector extends App with LazyLogging {
val (t, (res, dot)) = time { val (t, (res, dot)) = time {
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true) // InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
val props = InvProperties(stubborn = false, eliminateAux = true) val props = InvProperties(stubborn = false, eliminateA = true)
val (result, graph, afterlabels, proven, dot, time) = val (result, graph, afterlabels, proven, dot, time) =
InvariantChecker.checkInvariantFPLabelling(spec, invariant(spec), props) InvariantChecker.checkInvariantFPLabelling(spec, invariant(spec), props)
......
...@@ -8,14 +8,14 @@ import de.tum.workflows.Utils._ ...@@ -8,14 +8,14 @@ import de.tum.workflows.Utils._
import java.io.PrintWriter import java.io.PrintWriter
import java.io.File import java.io.File
import de.tum.workflows.blocks.Workflow import de.tum.workflows.blocks.Workflow
import de.tum.workflows.blocks.Spec import de.tum.workflows.blocks.NISpec
import de.tum.workflows.foltl.FormulaFunctions import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator import de.tum.workflows.toz3.InvariantGenerator
object MainInvariants extends App with LazyLogging { object MainInvariants extends App with LazyLogging {
def generate(name: String, spec: Spec) { def generate(name: String, spec: NISpec) {
logger.info(s"Encoding Spec:\n$spec") logger.info(s"Encoding Spec:\n$spec")
def invariant = def invariant =
......
...@@ -4,7 +4,7 @@ import com.typesafe.scalalogging.LazyLogging ...@@ -4,7 +4,7 @@ import com.typesafe.scalalogging.LazyLogging
import com.microsoft.z3.Status import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._ import de.tum.workflows.Utils._
import de.tum.workflows.blocks.{SimpleBlock, Spec} import de.tum.workflows.blocks.{SimpleBlock, NISpec}
import de.tum.workflows.foltl.FOLTL._ import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FOTransformers import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.synth.Model import de.tum.workflows.synth.Model
...@@ -16,7 +16,7 @@ import Implicits._ ...@@ -16,7 +16,7 @@ import Implicits._
object MainInvariantsInference extends App with LazyLogging { object MainInvariantsInference extends App with LazyLogging {
def generate(name: String, spec: Spec, tar:Int) { def generate(name: String, spec: NISpec, tar:Int) {
logger.info(s"Encoding Spec:\n$spec") logger.info(s"Encoding Spec:\n$spec")
def invariant = def invariant =
...@@ -30,7 +30,7 @@ object MainInvariantsInference extends App with LazyLogging { ...@@ -30,7 +30,7 @@ object MainInvariantsInference extends App with LazyLogging {
val props = InvProperties( val props = InvProperties(
stubborn = true, stubborn = true,
eliminateAux = true, eliminateA = true,
eliminateB = true eliminateB = true
) )
......
...@@ -3,7 +3,7 @@ package de.tum.workflows ...@@ -3,7 +3,7 @@ package de.tum.workflows
import com.microsoft.z3.Status import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._ import de.tum.workflows.Utils._
import de.tum.workflows.blocks.{SimpleBlock, Spec} import de.tum.workflows.blocks.{SimpleBlock, NISpec}
import de.tum.workflows.foltl.FOLTL._ import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FOTransformers import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.synth.Model import de.tum.workflows.synth.Model
...@@ -15,7 +15,7 @@ import Implicits._ ...@@ -15,7 +15,7 @@ import Implicits._
object MainInvariantsInterpolation extends App with LazyLogging { object MainInvariantsInterpolation extends App with LazyLogging {
def generate(name: String, spec: Spec, tar:Int) { def generate(name: String, spec: NISpec, tar:Int) {
logger.info(s"Encoding Spec:\n$spec") logger.info(s"Encoding Spec:\n$spec")
def invariant = def invariant =
...@@ -24,7 +24,7 @@ object MainInvariantsInterpolation extends App with LazyLogging { ...@@ -24,7 +24,7 @@ object MainInvariantsInterpolation extends App with LazyLogging {
// InvariantChecker.invariantNoninterStubborn _ // InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _ // InvariantChecker.invariantAllEqual _
val props = InvProperties(stubborn = false, eliminateAux = true) val props = InvProperties(stubborn = false, eliminateA = true)
val inv = invariant(spec) val inv = invariant(spec)
val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props) val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
......
...@@ -5,7 +5,7 @@ import com.typesafe.scalalogging.LazyLogging ...@@ -5,7 +5,7 @@ import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.FOTransformers import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.Utils._ import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Properties import de.tum.workflows.foltl.Properties
import de.tum.workflows.blocks.Spec import de.tum.workflows.blocks.NISpec
import de.tum.workflows.foltl.FormulaFunctions import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.foltl.FOTransformers import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.owltransformer.OwlTransformer import de.tum.workflows.owltransformer.OwlTransformer
...@@ -15,7 +15,7 @@ import owl.ltl.rewriter.SimplifierFactory ...@@ -15,7 +15,7 @@ import owl.ltl.rewriter.SimplifierFactory
object MainLTL extends App with LazyLogging { object MainLTL extends App with LazyLogging {
def writeExample(name: String, spec: Spec, prop: Formula) { def writeExample(name: String, spec: NISpec, prop: Formula) {
val MAX_AGENTS = 8 val MAX_AGENTS = 8
...@@ -69,7 +69,7 @@ object MainLTL extends App with LazyLogging { ...@@ -69,7 +69,7 @@ object MainLTL extends App with LazyLogging {
write(name, s"$name.metrics", metrics.mkString("", "\n", "\n")) write(name, s"$name.metrics", metrics.mkString("", "\n", "\n"))
} }
def generate(name: String, spec: Spec, onlystubborn:Boolean) { def generate(name: String, spec: NISpec, onlystubborn:Boolean) {
logger.info(s"Encoding Spec:\n$spec") logger.info(s"Encoding Spec:\n$spec")
val t1 = "pi1" val t1 = "pi1"
val t2 = "pi2" val t2 = "pi2"
......
...@@ -9,11 +9,35 @@ import de.tum.workflows.toz3.{InvProperties, Z3BSFO} ...@@ -9,11 +9,35 @@ import de.tum.workflows.toz3.{InvProperties, Z3BSFO}
object Preconditions extends LazyLogging { object Preconditions extends LazyLogging {
private def elaborateSteps(b: SimpleBlock, s: Spec): List[SimpleBlock] = { private def elaborateSteps(b: SimpleBlock, spec: NISpec, properties: InvProperties): List[SimpleBlock] = {
val guardfix = if (!b.isoracly && b.pred.isDefined) {
// is "normal" may block
val choice = Fun(b.pred.get, b.agents)
for (s <- b.steps) yield {
val first = s.tuple.head
val inner = if (first.typ == spec.target.params.head.typ) {
val inf = Fun(INFNAME, List(b.agents.head))
if (properties.stubborn) {
choice.in(T1)
} else {
Or(And(Neg(inf.in(T1)), choice.in(T1)), And(inf.in(T1), choice))
}
} else {
choice
}
val newguard = And(s.guard, inner)
s.updateGuard(newguard)
}
} else {
b.steps
}
val newsteps = for ( val newsteps = for (
stmt <- b.steps stmt <- b.steps
if s.causals.map(_.typ).contains(stmt.tuple.head.typ) || if spec.causals.map(_.typ).contains(stmt.tuple.head.typ) ||
stmt.tuple.head.typ == s.target.params.head.typ) yield { stmt.tuple.head.typ == spec.target.params.head.typ) yield {
val fun = Fun(stmt.fun, stmt.tuple) val fun = Fun(stmt.fun, stmt.tuple)
// TODO // TODO
val guard = Neg(Equiv(fun.in(T1), fun.in(T2))) val guard = Neg(Equiv(fun.in(T1), fun.in(T2)))
...@@ -23,25 +47,40 @@ object Preconditions extends LazyLogging { ...@@ -23,25 +47,40 @@ object Preconditions extends LazyLogging {
} }
// For oracly blocks, remove O from guard and add to ForallMay choice predicate // For oracly blocks, remove O from guard and add to ForallMay choice predicate
private def elaborateOraclyBlock(b: SimpleBlock, s: Spec) = { private def elaborateOraclyBlock(b: SimpleBlock, spec: NISpec) = {
if (b.isoracly) { if (b.isoracly) {
val stmt = b.steps.head // can only be one val stmt = b.steps.head // can only be one
def fixguard(f: Formula) = {
f.everywhere {
case f: Fun if f.isOracle() => True
}
}
def findOracle(f: Formula) = { def findOracle(f: Formula) = {
f.collect { f.collect {
case f: Fun if (f.isOracle()) => List(f.name) case f: Fun if (f.isOracle()) => List(f.name)
} }
} }
val name = findOracle(stmt.guard).head val oracles = findOracle(stmt.guard)
val name = oracles.head
if (oracles.size != 1) {
logger.error(s"Found oracly block $b with more than one oracle")
}
val choice = Fun(name, b.agents)
def fixguard(f: Formula, choice:Fun) = {
val nooracles = f.everywhere {
case f: Fun if f.isOracle() => True
}
val decl = spec.declass.getOrElse(b.pred.get, (List(), False))._2
// FIXME: substitutions?
// FIXME: decl in T2?
And(nooracles, Or(And(decl.in(T1), choice.in(T1)), And(Neg(decl.in(T1)), choice)))
}
val newstmt = stmt match { val newstmt = stmt match {
case Add(guard, fun, tuple) => Add(fixguard(guard).simplify, fun, tuple) case Add(guard, fun, tuple) => Add(fixguard(guard, choice).simplify, fun, tuple)
case Remove(guard, fun, tuple) => Remove(fixguard(guard).simplify, fun, tuple) case Remove(guard, fun, tuple) => Remove(fixguard(guard, choice).simplify, fun, tuple)
} }
ForallMayBlock(b.agents, name, List(newstmt)) ForallMayBlock(b.agents, name, List(newstmt))
} else b } else b
...@@ -66,58 +105,27 @@ object Preconditions extends LazyLogging { ...@@ -66,58 +105,27 @@ object Preconditions extends LazyLogging {
}) })
} }
// TODO: make this a transformation instead of a logics block def getUpdate(s:Statement, choice:Option[Fun], spec:NISpec, properties:InvProperties) = {
def getUpdate(s:Statement, b:SimpleBlock, choice:Option[Fun], spec:Spec, properties:InvProperties) = {
// val list = List(s.guard) ++ choice.toList
// val guard = And.make(list)
val first = s.tuple.head
// Trace related substitution for informedness
val con = if (b.isoracly) {
val decl = spec.declass.getOrElse(b.pred.get, (List(), False))._2
// FIXME: substitutions?
// FIXME: decl in T2?
Or(And(decl.in(T1), choice.get.in(T1)), And(Neg(decl.in(T1)), choice.get))
} else if (choice.isDefined) {
// is "normal" may block
val inner = if (first.typ == spec.target.params.head.typ) {
val inf = Fun(INFNAME, List(b.agents.head))
if (properties.stubborn) {
choice.get.in(T1)
} else {
Or(And(Neg(inf.in(T1)), choice.get.in(T1)), And(inf.in(T1), choice.get))
}
} else {
choice.get
}
inner
} else {
True
}
val guard = And(s.guard, con).simplify
// val guard = True
val frees = guard.freeVars -- s.tuple.toSet -- spec.constants val frees = s.guard.freeVars -- s.tuple.toSet -- spec.constants
val form = s match { val form = s match {
case Add(_, _, _) => { case Add(_, _, _) => {
Or(Fun(s.fun, s.tuple), Exists(frees.toList, guard)).simplify Or(Fun(s.fun, s.tuple), Exists(frees.toList, s.guard)).simplify
} }
case Remove(_, _, _) => { case Remove(_, _, _) => {
And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(guard))).simplify And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(s.guard))).simplify
} }
} }
form form
} }
def elaborate(block: SimpleBlock, spec:Spec, properties:InvProperties) = { def elaborate(block: SimpleBlock, spec:NISpec, properties:InvProperties) = {
val stepOne = if (!properties.stubborn) elaborateSteps(block, spec) else List(block) val stepOne = if (!properties.stubborn) elaborateSteps(block, spec, properties) else List(block)
stepOne map { b => elaborateOraclyBlock(b, spec) } stepOne map { b => elaborateOraclyBlock(b, spec) }
} }
def weakestPrecondition(post: Formula, outerb: SimpleBlock, spec: Spec, properties: InvProperties) = { def weakestPrecondition(post: Formula, outerb: SimpleBlock, spec: NISpec, properties: InvProperties) = {
// TODO: Make 2-trace elaboration optional // TODO: Make 2-trace elaboration optional
...@@ -130,13 +138,11 @@ object Preconditions extends LazyLogging { ...@@ -130,13 +138,11 @@ object Preconditions extends LazyLogging {
precond precond
} }
private def weakestPreconditionSingle(f: Formula, b: SimpleBlock, spec: Spec, properties: InvProperties) = { private def weakestPreconditionSingle(f: Formula, b: SimpleBlock, spec: NISpec, properties: InvProperties) = {
val choice = b.pred.map(n => Fun(n, b.agents))
val updates = for (s <- b.steps) yield { val updates = for (s <- b.steps) yield {
s.fun -> (s.tuple, { s.fun -> (s.tuple, {
getUpdate(s, b, choice, spec, properties) getUpdate(s, b, spec, properties)
}) })
} }
...@@ -154,7 +160,7 @@ object Preconditions extends LazyLogging { ...@@ -154,7 +160,7 @@ object Preconditions extends LazyLogging {
removed removed
} }
def abstractedPrecondition(f: Formula, b: SimpleBlock, spec: Spec, properties: InvProperties, untouched: Set[String]) = { def abstractedPrecondition(f: Formula, b: SimpleBlock, spec: NISpec, properties: InvProperties, untouched: Set[String]) = {
val precond = weakestPrecondition(f, b, spec, properties) val precond = weakestPrecondition(f, b, spec, properties)
// Assume untoucheds empty // Assume untoucheds empty
...@@ -171,7 +177,6 @@ object Preconditions extends LazyLogging { ...@@ -171,7 +177,6 @@ object Preconditions extends LazyLogging {
z3simpednewinv z3simpednewinv
} }
// Abstract away inner existentials // Abstract away inner existentials
val universalinv = if (removedannotations.toNegNf.hasSubFormula { val universalinv = if (removedannotations.toNegNf.hasSubFormula {
case e:Exists => true case e:Exists => true
...@@ -182,15 +187,15 @@ object Preconditions extends LazyLogging { ...@@ -182,15 +187,15 @@ object Preconditions extends LazyLogging {
} }
// Eliminate Choices // Eliminate Choices
val auxless = if (b.pred.isDefined && properties.eliminateAux) { val auxless = if (b.pred.isDefined && properties.eliminateA) {
FOTransformers.eliminateAuxiliaryPredicate(universalinv, b.pred.get) FOTransformers.eliminateAuxiliaryPredicate(universalinv, b.pred.get)
} else { } else {
universalinv universalinv
} }
// Eliminate Oracles // Eliminate Oracles
val oless = if (properties.eliminateAux) { val oless = if (properties.eliminateA) {
val oracles = spec.w.sig.oracles.map(_.name) val oracles = spec.w.sig.as.map(_.name)
oracles.foldRight(auxless)((b, inv) => FOTransformers.eliminateAuxiliaryPredicate(inv, b)) oracles.foldRight(auxless)((b, inv) => FOTransformers.eliminateAuxiliaryPredicate(inv, b))
} else { } else {
auxless auxless
......
...@@ -68,7 +68,7 @@ object Utils extends LazyLogging { ...@@ -68,7 +68,7 @@ object Utils extends LazyLogging {
logger.info(s"Written $file") logger.info(s"Written $file")
} }
def check(name:String, desc:String, inv:Formula, spec:Spec, properties:InvProperties) = { def check(name:String, desc:String, inv:Formula, spec:NISpec, properties:InvProperties) = {
val model = if (properties.stubborn) "stubborn" else "causal" val model = if (properties.stubborn) "stubborn" else "causal"
val basename = name.split("/").last val basename = name.split("/").last
......
...@@ -186,7 +186,7 @@ object WorkflowParser extends RegexParsers with PackratParsers with LazyLogging ...@@ -186,7 +186,7 @@ object WorkflowParser extends RegexParsers with PackratParsers with LazyLogging
(("Declassify" ~> DECLASS)?) ~ (("Declassify" ~> DECLASS)?) ~
("Target" ~> FUN) ~ ("Target" ~> FUN) ~
(("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ { (("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ {
case _ ~ w ~ decl ~ tar ~ causals => Spec(w, toMap(decl.toList), tar, causals.getOrElse(List())) case _ ~ w ~ decl ~ tar ~ causals => NISpec(w, toMap(decl.toList), tar, causals.getOrElse(List()))
} }
def toMap(list:List[(Fun, Formula)]):Map[String, (List[Var], Formula)] = { def toMap(list:List[(Fun, Formula)]):Map[String, (List[Var], Formula)] = {
......
...@@ -5,14 +5,14 @@ import com.typesafe.scalalogging.LazyLogging ...@@ -5,14 +5,14 @@ import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils import de.tum.workflows.Utils
import de.tum.workflows.foltl.Properties import de.tum.workflows.foltl.Properties
case class Signature(oracles: Set[Fun], bs: Set[Fun], preds: Set[Fun]) case class Signature(as: Set[Fun], constas: Set[Fun], bs: Set[Fun], preds: Set[Fun])
object Signature { object Signature {
val EMPTY = Signature(Set(), Set(), Set()) val EMPTY = Signature(Set(), Set(), Set(), Set())
} }
case class Workflow(sig: Signature, steps: List[Block]) { case class Workflow(sig: Signature, steps: List[Block]) {
override def toString() = steps.mkString("\n") override def toString() = steps.mkString("\n")
def isomitting = { lazy val isomitting = {
steps.exists(_.isomitting) steps.exists(_.isomitting)
} }
} }
...@@ -20,11 +20,24 @@ object Workflow { ...@@ -20,11 +20,24 @@ object Workflow {
val EMPTY = Workflow(Signature.EMPTY, List()) val EMPTY = Workflow(Signature.EMPTY, List())
} }
case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target: Fun, causals:List[Var]) extends LazyLogging { trait Spec {
def w: Workflow
}
case class InvSpec(w: Workflow, always: Formula, invariant: Formula) extends Spec {
override def toString = { override def toString = {
s"Spec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target" s"Spec\nWorkflow:\n$w\nAlways:$always\nInvariant:$invariant"
} }
def toNISpec() = {
NISpec(w, Map(), Fun("NOTHING", List()), List())
}
}
case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], target: Fun, causals:List[Var]) extends Spec with LazyLogging {
override def toString = {
s"NISpec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
}
lazy val constants:Set[Var] = { lazy val constants:Set[Var] = {
// Treat free variables in the declassification as constants // Treat free variables in the declassification as constants
...@@ -33,33 +46,39 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target: ...@@ -33,33 +46,39 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
}.toSet }.toSet
// TODO: How to check for more constants? // TODO: How to check for more constants?
} }
def checkSanity() = { def checkSanity() = {
var sane = true var sane = true
// TODO: check all types // TODO: check all types
// TODO: check target types // TODO: check target types
// TODO: check declass arities and types (o should be an Oracle relation etc) // TODO: check declass arities and types (o should be an Oracle relation etc)
val ta = target.params.head val ta = target.params.head
// check declass bindings // check declass bindings
for ((o, (f, t)) <- declass if !t.freeVars.forall(v => f.contains(v) || (v == ta))) { for ((o, (f, t)) <- declass if !t.freeVars.forall(v => f.contains(v) || (v == ta))) {
logger.error(s"Not all variables of the declassification condition for $o bound by the oracle") logger.error(s"Not all variables of the declassification condition for $o bound by the oracle")
sane = false sane = false
} }
def saneoraclestmt(stmt:Statement, frees:List[Var]) = { def saneoraclestmt(stmt:Statement, frees:List[Var]) = {
// Oracle only positive // Oracle only positive
val f = stmt.guard.toNegNf val f = stmt.guard.toNegNf
val noneg = !f.hasSubFormula { val noneg = !f.hasSubFormula {
case Neg(f:Fun) if f.isOracle() => true case Neg(f:Fun) if f.isOracle() => true
} }
if (!noneg) {
logger.error(s"Found negated oracle in guard for statement $stmt")
}
val allvars = !(f hasSubFormula { val allvars = !(f hasSubFormula {
case f:Fun if f.isOracle && f.params != frees => true case f:Fun if f.isOracle && f.params != frees => true
}) })
if (!allvars) {
logger.error(s"Found oracle with wrong parameters in statement $stmt")
}
noneg && allvars noneg && allvars
} }
// check same relation only updated once per block // check same relation only updated once per block
def isSane(steps:List[Block]):Boolean = { def isSane(steps:List[Block]):Boolean = {
val sanes = steps map { val sanes = steps map {
...@@ -73,8 +92,8 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target: ...@@ -73,8 +92,8 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
val saneoracly = if (b.isoracly) { val saneoracly = if (b.isoracly) {
b.pred.isEmpty && b.steps.size == 1 && saneoraclestmt(b.steps.head, b.agents) b.pred.isEmpty && b.steps.size == 1 && saneoraclestmt(b.steps.head, b.agents)
} else true } else true
// if (!saneoracly) { logger.warn(s"Oracles used wrongly in $b") } if (!saneoracly) { logger.warn(s"Oracles used wrongly in $b") }
pred.isEmpty // && saneoracly TODO: enable this later? pred.isEmpty && saneoracly
} }
case Loop(steps) => isSane(steps) case Loop(steps) => isSane(steps)
case NondetChoice(left, right) => isSane(left) && isSane(right) case NondetChoice(left, right) => isSane(left) && isSane(right)
...@@ -85,8 +104,8 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target: ...@@ -85,8 +104,8 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
sane sane
} }
} }