-
Notifications
You must be signed in to change notification settings - Fork 4
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
7 changed files
with
156 additions
and
134 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
4 changes: 2 additions & 2 deletions
4
compiler/src/main/kotlin/io/github/aplcornell/viaduct/precircuitanalysis/ProtocolAnalysis.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
137 changes: 114 additions & 23 deletions
137
compiler/src/main/kotlin/io/github/aplcornell/viaduct/reordering/DependencyGraph.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,44 +1,135 @@ | ||
| package io.github.aplcornell.viaduct.reordering | ||
|
|
||
| import io.github.aplcornell.viaduct.attributes.attribute | ||
| import io.github.aplcornell.viaduct.precircuitanalysis.NameAnalysis | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.ArrayTypeNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.BlockNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.BreakNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.CommandLetNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.ComputeLetNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.LetNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.Node | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.DeclassificationNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.DowngradeNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.EndorsementNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.ExpressionNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.FunctionDeclarationNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.IfNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.InputNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.LiteralNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.LookupNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.LoopNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.OperatorApplicationNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.OutputNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.ProgramNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.ReduceNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.ReferenceNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.ReturnNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.StatementNode | ||
| import io.github.aplcornell.viaduct.syntax.precircuit.VariableReferenceNode | ||
|
|
||
| val Node.uses: List<VariableReferenceNode> by attribute { TODO() } | ||
|
|
||
| class DependencyGraph(program: ProgramNode) { | ||
| private val nameAnalysis: NameAnalysis = NameAnalysis.get(program) | ||
| private val nodeToDependencies = mutableMapOf<StatementNode, MutableList<StatementNode>>() | ||
| private val nodeToDependents = mutableMapOf<StatementNode, MutableList<StatementNode>>() | ||
|
|
||
| init { | ||
| program.declarations.filterIsInstance<FunctionDeclarationNode>().forEach { buildDependencyGraph(it.body) } | ||
| println("HERE IS THE DEP MAP AFTER INIT") | ||
| nodeToDependencies.forEach { (k, _) -> println(k.toDocument().print()) } | ||
| } | ||
|
|
||
| private fun uses(node: StatementNode): List<VariableReferenceNode> = when (node) { | ||
| is ComputeLetNode -> uses(node.type) + uses(node.value) | ||
| is CommandLetNode -> when (val command = node.command) { | ||
| is InputNode -> uses(command.type) | ||
| is OutputNode -> uses(command.type) + listOf(command.message) | ||
| is DowngradeNode -> uses(command.expression) | ||
| } | ||
| is ReturnNode -> node.values.flatMap { uses(it) } | ||
| is BreakNode -> listOf() | ||
| is IfNode -> uses(node.guard) + node.thenBranch.flatMap { uses(it) } + node.elseBranch.flatMap { uses(it) } | ||
| is LoopNode -> node.body.flatMap { uses(it) } | ||
| } | ||
|
|
||
| private fun uses(node: ExpressionNode): List<VariableReferenceNode> = when (node) { | ||
| is LiteralNode -> listOf() | ||
| is ReferenceNode -> listOf(node) | ||
| is LookupNode -> listOf(node) + node.indices.flatMap { uses(it) } | ||
| is OperatorApplicationNode -> node.arguments.flatMap { uses(it) } | ||
| is ReduceNode -> uses(node.defaultValue) + uses(node.body) | ||
| } | ||
|
|
||
| private fun uses(node: ArrayTypeNode): List<VariableReferenceNode> = node.shape.flatMap { uses(it) } | ||
|
|
||
| private fun addDependencies(node: StatementNode, dependencies: List<StatementNode>) { | ||
| nodeToDependencies.getOrPut(node) { mutableListOf() } | ||
| nodeToDependents.getOrPut(node) { mutableListOf() } | ||
| dependencies.forEach { | ||
| nodeToDependencies[node]!!.add(it) | ||
| nodeToDependents.getOrPut(it) { mutableListOf() }.add(node) | ||
| } | ||
| } | ||
|
|
||
| fun dependents(statement: StatementNode) = nodeToDependents[statement]!! | ||
| fun dependencies(statement: StatementNode): List<StatementNode> { | ||
| println("getting dependencies of " + statement.toDocument().print()) | ||
| return nodeToDependencies[statement]!! //?: listOf() | ||
| } | ||
|
|
||
| fun BlockNode<StatementNode>.buildDependencyGraph(block: BlockNode<StatementNode>): Map<StatementNode, List<StatementNode>> { | ||
| val dependencyGraph = block.statements.associateWith { listOf<StatementNode>() }.toMutableMap() | ||
| private fun dataDependencies(stmt: StatementNode): List<StatementNode> { | ||
| return uses(stmt).map { nameAnalysis.declaration(it) }.mapNotNull { | ||
| // TODO Extremely hacky. A better way is to have two Contexts in NameAnalysis; | ||
| // one for contextAfter (let nodes only) and one for contextChildren (other variable declaration types) | ||
| when (it) { | ||
| is StatementNode -> it | ||
| else -> null | ||
| } | ||
| } | ||
| } | ||
|
|
||
| /** Fills in [nodeToDependencies] for [this]. Reordering will only occur within blocks. */ | ||
| // TODO Kind of weird: Data dependency edges extend outside of blocks but we only include security dependencies | ||
| // which are within the same block due to our assumption that we'll only reorder within blocks | ||
| private fun buildDependencyGraph(block: BlockNode<StatementNode>) { | ||
| val prevInputs: List<StatementNode> = listOf() | ||
| val prevOutputs: List<StatementNode> = listOf() | ||
| val prevDeclassifies: List<StatementNode> = listOf() | ||
| val prevEndorses: List<StatementNode> = listOf() | ||
| block.forEach { stmt -> | ||
| println("ADDing data dependencies for " + stmt.toDocument().print()) | ||
| addDependencies(stmt, dataDependencies(stmt)) | ||
| println("HERE IS THE DEP MAP AFTER ADDING") | ||
| nodeToDependencies.forEach { (k, _) -> println(k.toDocument().print()) } | ||
|
|
||
| this.forEach { stmt -> | ||
| when (stmt) { | ||
| is ComputeLetNode -> { | ||
| val dataDeps = stmt.uses.map { nameAnalysis.declaration(it) } | ||
| addDependencies(stmt, listOf()) | ||
| } // Only data dependencies matter | ||
| is CommandLetNode -> { | ||
| when (stmt.command) { | ||
| is InputNode, is OutputNode -> | ||
| // Shouldn't change interface to the user | ||
| addDependencies(stmt, prevInputs + prevOutputs) | ||
|
|
||
| is DeclassificationNode -> addDependencies(stmt, prevEndorses) | ||
| is EndorsementNode -> { | ||
| addDependencies(stmt, listOf()) | ||
| } // TODO No need to depend on declassifies? Does it break robust declassification | ||
| } | ||
| } | ||
| is ReturnNode -> // Cannot reorder with any side effects | ||
| addDependencies(stmt, prevInputs + prevOutputs + prevDeclassifies + prevEndorses) | ||
| is BreakNode -> | ||
| // Cannot reorder with any side effects | ||
| addDependencies(stmt, prevInputs + prevOutputs + prevDeclassifies + prevEndorses) | ||
| is IfNode -> { // TODO: the if's dependencies should be the union of its childrens | ||
| addDependencies(stmt, listOf()) | ||
| buildDependencyGraph(stmt.thenBranch) | ||
| buildDependencyGraph(stmt.elseBranch) | ||
| } | ||
| is LoopNode -> { | ||
| addDependencies(stmt, listOf()) | ||
| buildDependencyGraph(stmt.body) | ||
| } | ||
| is LetNode -> TODO() | ||
| is ReturnNode -> TODO() | ||
| } | ||
|
|
||
| } | ||
| /* | ||
| for each statement in block | ||
| data dependencies = declarations(stmt) | ||
| if stmt is output, iodependencies = all previous inputs (this can be relaxed but let's do something easy for now) | ||
| if stmt is declassify, securitydependencies = all previous endorses | ||
| if stmt is endorse, securitydependencies = all previous declassifies | ||
| if bob happy reveal data | ||
| endorse bob input | ||
| cannot move endorse before the if?? | ||
| */ | ||
| return dependencyGraph | ||
| } | ||
| } |
Oops, something went wrong.