From a57fdc978378a6f3a983c860738fce5ee5d612b1 Mon Sep 17 00:00:00 2001 From: Aakash Date: Fri, 3 Mar 2023 16:05:26 -0800 Subject: [PATCH] throwing error if there's a cycle in bound graph | fixing issue with default policy assignment to val defs --- .../main/scala/com/facebook/flowframe/CheckLabels.scala | 5 +++-- .../src/main/scala/com/facebook/flowframe/Policies.scala | 5 +++-- .../src/main/scala/com/facebook/flowframe/Solvers.scala | 7 +++++-- 3 files changed, 11 insertions(+), 6 deletions(-) diff --git a/flowframe-plugin/src/main/scala/com/facebook/flowframe/CheckLabels.scala b/flowframe-plugin/src/main/scala/com/facebook/flowframe/CheckLabels.scala index 1c1e974..dccaccc 100644 --- a/flowframe-plugin/src/main/scala/com/facebook/flowframe/CheckLabels.scala +++ b/flowframe-plugin/src/main/scala/com/facebook/flowframe/CheckLabels.scala @@ -334,9 +334,10 @@ abstract class CheckLabels[T <: PolicyLang] extends PluginComponent with SparkSi if (!t.hasAttachment[PolicyStruct]) { // assume that the definition annotation overrides the type annotation // if neither exist, resort to a default policy (generate a solver variable) - val defAnnOpt = getPolicyStruct(t.symbol, withDefault=false) + val defAnn = getPolicyStruct(t.symbol, withDefault=false).getOrElse { defaultPolicyStruct(t.symbol) } val tptAnnOpt = getPolicyStruct(t.tpt.symbol, withDefault=false) - val pol = defAnnOpt.orElse(tptAnnOpt).getOrElse { defaultPolicyStruct(t.symbol) } + + val pol = if (tptAnnOpt.isDefined) defAnn.join(tptAnnOpt.get) else defAnn // val pol = defAnnOpt.getOrElse { defaultPolicyStruct(t.symbol) } t.symbol.updateAttachment[PolicyStruct](pol) diff --git a/flowframe-plugin/src/main/scala/com/facebook/flowframe/Policies.scala b/flowframe-plugin/src/main/scala/com/facebook/flowframe/Policies.scala index 5c5e2a2..d1cfa53 100644 --- a/flowframe-plugin/src/main/scala/com/facebook/flowframe/Policies.scala +++ b/flowframe-plugin/src/main/scala/com/facebook/flowframe/Policies.scala @@ -121,11 +121,12 @@ trait Policies[T <: PolicyLang] { override def subst(substMap: Map[AbstractPolicy, PolicyExpr], seen: Set[PolicyExpr] = Set.empty) (implicit lattice: SecLattice): PolicyExpr = { substMap.get(this) match { - // case Some(sub) if seen.contains(sub) => + case Some(sub) if seen.contains(sub) => // // if there is a cycle in the bound graph, then apply cycleOp to the cycle. Typically this is a meet or join // // 1) all policies in the cycle are equivalent, and 2) for GLB, this parameter flows to anything // // we can prove at least one of these policies flows to - // lattice.simplify(seen.foldLeft(sub)((acc, p) => cycleOp(lattice)(acc, p))) + throw new InternalError("Found cycle in bound graph " + seen.toString()) +// lattice.simplify(seen.foldLeft(sub)((acc, p) => cycleOp(lattice)(acc, p))) case Some(sub) => // only recurse if we haven't seen this bound before diff --git a/flowframe-plugin/src/main/scala/com/facebook/flowframe/Solvers.scala b/flowframe-plugin/src/main/scala/com/facebook/flowframe/Solvers.scala index 8ae2abd..6a07893 100644 --- a/flowframe-plugin/src/main/scala/com/facebook/flowframe/Solvers.scala +++ b/flowframe-plugin/src/main/scala/com/facebook/flowframe/Solvers.scala @@ -44,8 +44,11 @@ trait Solvers[T <: PolicyLang] extends Constraints[T] { } // TODO: isn't this a LUBSolver? - class GLBSolver(lattice: SecLattice) { - + class GLBSolver(val lattice: SecLattice) { +// val lattice = _lattice +// def lattice() = { +// +// } import Status._ /**