Commit 113ddf9e authored by Christian Müller's avatar Christian Müller

log messages better

parent 8f5e5d7d
......@@ -101,14 +101,12 @@ object Main extends App with LazyLogging {
if (checkinvariants) {
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val (t,safe) = time {
val (t,(safe, msg)) = time {
InvariantChecker.checkStubborn(spec.w, inv)
}
val noninter = s"Noninterference Invariant (took $t ms):\n$msg"
val string = "Workflow " + (if(safe)"proven SAFE" else "possibly UNSAFE") + s" after $t ms for invariant:\n${inv.pretty}"
write(s"$FOLDER/${name}.inv", string)
write(s"$FOLDER/${name}.inv", noninter)
}
}
......
......@@ -17,10 +17,10 @@ object Preconditions extends LazyLogging {
val updates = b.steps.map(s => {
s.fun -> (s.tuple, {
val frees = s.guard.freeVars() -- s.tuple.toSet
val list = List(s.guard) ++ choice.toList
val guard = And.make(list)
s match {
case Add(_, _, _) => {
Or(Fun(s.fun, s.tuple), Exists(frees.toList, guard)).simplify()
......@@ -37,14 +37,39 @@ object Preconditions extends LazyLogging {
case Fun(name, ind, params) if b.steps.exists(s => s.fun == name) => {
val up = updates(name)
val renamed = up._2.parallelRename(up._1, params)
// Annotate the precondition with the index
if (ind.isDefined) {
FormulaFunctions.annotate(renamed, ind.get)
FormulaFunctions.annotate(renamed, ind.get)
} else {
renamed
}
}
}
}
def weakestPreconditionWithInformedness(f: Formula, b: SimpleBlock) = {
val wp = weakestPrecondition(f, b)
val PRED = "__inf__"
val agent = "_i_"
if (b.may) {
val updates = b.steps.map(s => {
val frees = s.guard.freeVars() -- Set(s.tuple.head)
s match {
case Add(_, _, _) => {
Or(Fun(s.fun, s.tuple), Exists(frees.toList, guard)).simplify()
}
case Remove(_, _, _) => {
And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(guard))).simplify()
}
}
})
}
}
}
\ No newline at end of file
......@@ -48,6 +48,9 @@ object InvariantChecker extends LazyLogging {
// Build graph
val graph = Encoding.toGraph(w)
val msg = new StringBuilder()
msg ++= s"Trying to prove safe with invariant:\n${inv.pretty()}"
// Check all edges
val list = for (e <- graph.edges) yield {
......@@ -67,6 +70,7 @@ object InvariantChecker extends LazyLogging {
val res = checkOnZ3(tocheck)
if (res != Status.UNSATISFIABLE) {
msg ++= s"Possibly unsafe: Block\n${e.label}\nmay not uphold invariant."
logger.info(s"Could not prove invariant $inv")
logger.info(s"Z3 status $res")
logger.info(s"Block ${e.label} may not uphold it")
......@@ -76,9 +80,10 @@ object InvariantChecker extends LazyLogging {
val safe = list.reduceLeft(_ && _)
if (safe) {
msg ++= s"Proven safe."
logger.info(s"Workflow $w\n proven safe for invariant:\n${inv.pretty()}")
}
safe
(safe, msg)
}
def genEq(f:Fun, p:List[Var]) = {
......
......@@ -15,57 +15,57 @@ import de.tum.workflows.toz3.InvariantChecker
class InvariantTest extends FlatSpec {
"InvariantChecker" should "prove simple things safe" in {
val wf = ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get.w
val inv = Forall(List("a","b"), Eq(Fun("R", Some("t1"), List("a","b")), Fun("R", Some("t2"), List("a","b"))))
val safe = InvariantChecker.checkStubborn(wf, inv)
safe should be (true)
val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
val (safe, msg) = InvariantChecker.checkStubborn(wf, inv)
safe should be(true)
}
it should "prove fail to prove unsafe workflows safe" in {
val wf = ExampleWorkflows.parseExample("tests/simpleChoice").get.w
val inv = Forall(List("a","b"), Eq(Fun("R", Some("t1"), List("a","b")), Fun("R", Some("t2"), List("a","b"))))
val safe = InvariantChecker.checkStubborn(wf, inv)
safe should be (false)
val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
val (safe, msg) = InvariantChecker.checkStubborn(wf, inv)
safe should be(false)
}
it should "prove the paper example" in {
val wf = ExampleWorkflows.parseExample("omitting/conference").get.w
val x = Var("x", "A")
val p = Var("p","P")
val r = Var("r","R")
val inv = Forall(List(x,p,r), Implies(Fun("Conf", List(x,p)), Neg(Fun("Read", List(x,p,r)))))
val safe = InvariantChecker.checkStubborn(wf, inv)
safe should be (true)
val p = Var("p", "P")
val r = Var("r", "R")
val inv = Forall(List(x, p, r), Implies(Fun("Conf", List(x, p)), Neg(Fun("Read", List(x, p, r)))))
val (safe, msg) = InvariantChecker.checkStubborn(wf, inv)
safe should be(true)
}
it should "prove noninter invariants" in {
val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val safe = InvariantChecker.checkStubborn(spec.w, inv)
val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
safe should be (false)
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val (safe, msg) = InvariantChecker.checkStubborn(spec.w, inv)
safe should be(false)
}
it should "prove the paper example as noninter invariant"in {
val spec = ExampleWorkflows.parseExample("omitting/conference").get
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val safe = InvariantChecker.checkStubborn(spec.w, inv)
safe should be (true)
it should "prove the paper example as noninter invariant" in {
val spec = ExampleWorkflows.parseExample("omitting/conference").get
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val (safe, msg) = InvariantChecker.checkStubborn(spec.w, inv)
safe should be(true)
}
}
\ 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