From ec36bd6c7f5c5c39b2ad483a757668554b90b6d9 Mon Sep 17 00:00:00 2001 From: Alex Rosengarten Date: Fri, 30 Apr 2021 16:09:10 -0700 Subject: [PATCH 1/5] Updated VerifyPolicy - Added flag to turn on debug mode. - made CLI more conventional - documented tool - added a few more log stmts --- java/arcs/core/analysis/InformationFlow.kt | 8 ++++++++ java/arcs/tools/README.md | 12 ++++++++++++ java/arcs/tools/VerifyPolicy.kt | 17 +++++++++++++---- 3 files changed, 33 insertions(+), 4 deletions(-) diff --git a/java/arcs/core/analysis/InformationFlow.kt b/java/arcs/core/analysis/InformationFlow.kt index 57b4c6b6d50..a2fb6c13c0d 100644 --- a/java/arcs/core/analysis/InformationFlow.kt +++ b/java/arcs/core/analysis/InformationFlow.kt @@ -693,8 +693,14 @@ private fun Predicate.labels(): List = when (this) { /** Returns true if the [check] is satisfied by the labels computed for [particle]. */ fun InformationFlow.AnalysisResult.verify(particle: Recipe.Particle, check: Check): Boolean { + val log = TaggedLog { "AnalysisResult.verify" } + + log.debug { "checking $check in $particle"} + val result = fixpoint.getValue(particle) + log.debug { "result: $result" } + // Unreachable particle => check is trivially satisfied. if (result.isBottom) return true @@ -703,6 +709,8 @@ fun InformationFlow.AnalysisResult.verify(particle: Recipe.Particle, check: Chec val accessPathLabels = result.getLabels(check.accessPath) + log.debug { "accessPathLabels: $accessPathLabels" } + // Unreachable => check is trivially satisfied. if (accessPathLabels.isBottom) return true // All possible values => check is unsatisfied. diff --git a/java/arcs/tools/README.md b/java/arcs/tools/README.md index 5f2d507fc1a..d462b71af4d 100644 --- a/java/arcs/tools/README.md +++ b/java/arcs/tools/README.md @@ -46,3 +46,15 @@ into textprotos. ``` $ bazel run --run_under="cd $PWD && " //java/arcs/tools:inspect_manifest -- ./ok_check_multiple_or_tags.binarypb ./ok_check_multiple_or_tags.textproto ``` + +## verify_policy + +Verifies that all recipes in an Arcs manifest file comply with their policies. + +``` +# bazel run //java/arcs/tools:verify_policy -- /absolute/path/to/binary_manifest.binarypb +``` + +Options: +- `-d, --debug`: Turn on debug tracing +- `--help`: Display usage info diff --git a/java/arcs/tools/VerifyPolicy.kt b/java/arcs/tools/VerifyPolicy.kt index 8f00c9dc7c2..d42fcdb0f97 100644 --- a/java/arcs/tools/VerifyPolicy.kt +++ b/java/arcs/tools/VerifyPolicy.kt @@ -4,21 +4,30 @@ import arcs.core.analysis.PolicyVerifier import arcs.core.data.proto.ManifestProto import arcs.core.data.proto.decodeRecipes import arcs.core.policy.proto.decode +import arcs.core.util.Log import com.github.ajalt.clikt.core.CliktCommand import com.github.ajalt.clikt.core.CliktError +import com.github.ajalt.clikt.parameters.arguments.argument +import com.github.ajalt.clikt.parameters.options.flag import com.github.ajalt.clikt.parameters.options.option -import com.github.ajalt.clikt.parameters.options.required import com.github.ajalt.clikt.parameters.types.file class VerifyPolicy : CliktCommand( name = "verify_policy", - help = "Verifies that all recipes in an Arcs manifest file comply with their policies." + help = "Verifies that all recipes in an Arcs manifest file comply with their policies.", + printHelpOnEmptyArgs = true ) { - val manifest by option( + val manifest by argument( help = "Arcs manifest to check, encoded as a binary proto file (.binarypb)" - ).file().required() + ).file() + + val debug by option("-d", "--debug", help = "Turn on debug tracing") + .flag(default = false) override fun run() { + if (debug) { + Log.level = Log.Level.Debug + } val manifestProto = ManifestProto.parseFrom(manifest.readBytes()) val recipes = manifestProto.decodeRecipes() From f078068c42f9f6f6d7265329a9b8452ebebd8a25 Mon Sep 17 00:00:00 2001 From: Alex Rosengarten Date: Fri, 30 Apr 2021 16:12:34 -0700 Subject: [PATCH 2/5] Less verbose log statement. --- java/arcs/core/analysis/InformationFlow.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/java/arcs/core/analysis/InformationFlow.kt b/java/arcs/core/analysis/InformationFlow.kt index a2fb6c13c0d..e69140c810a 100644 --- a/java/arcs/core/analysis/InformationFlow.kt +++ b/java/arcs/core/analysis/InformationFlow.kt @@ -695,7 +695,7 @@ private fun Predicate.labels(): List = when (this) { fun InformationFlow.AnalysisResult.verify(particle: Recipe.Particle, check: Check): Boolean { val log = TaggedLog { "AnalysisResult.verify" } - log.debug { "checking $check in $particle"} + log.debug { "checking $check in ${particle.spec.name}"} val result = fixpoint.getValue(particle) From 2c08bad211060ba318dc3ff256a96e409f30c88e Mon Sep 17 00:00:00 2001 From: Alex Rosengarten Date: Fri, 30 Apr 2021 16:14:01 -0700 Subject: [PATCH 3/5] Nit --- java/arcs/core/analysis/InformationFlow.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/java/arcs/core/analysis/InformationFlow.kt b/java/arcs/core/analysis/InformationFlow.kt index e69140c810a..b7e4cf0bc8c 100644 --- a/java/arcs/core/analysis/InformationFlow.kt +++ b/java/arcs/core/analysis/InformationFlow.kt @@ -695,7 +695,7 @@ private fun Predicate.labels(): List = when (this) { fun InformationFlow.AnalysisResult.verify(particle: Recipe.Particle, check: Check): Boolean { val log = TaggedLog { "AnalysisResult.verify" } - log.debug { "checking $check in ${particle.spec.name}"} + log.debug { "checking $check in ${particle.spec.name}" } val result = fixpoint.getValue(particle) From d7852ac118e6b827fc4bb2383dfae08438993557 Mon Sep 17 00:00:00 2001 From: Alex Rosengarten Date: Fri, 30 Apr 2021 16:47:34 -0700 Subject: [PATCH 4/5] Reverted changes to InformationFlow.kt. --- java/arcs/core/analysis/InformationFlow.kt | 8 -------- 1 file changed, 8 deletions(-) diff --git a/java/arcs/core/analysis/InformationFlow.kt b/java/arcs/core/analysis/InformationFlow.kt index b7e4cf0bc8c..57b4c6b6d50 100644 --- a/java/arcs/core/analysis/InformationFlow.kt +++ b/java/arcs/core/analysis/InformationFlow.kt @@ -693,14 +693,8 @@ private fun Predicate.labels(): List = when (this) { /** Returns true if the [check] is satisfied by the labels computed for [particle]. */ fun InformationFlow.AnalysisResult.verify(particle: Recipe.Particle, check: Check): Boolean { - val log = TaggedLog { "AnalysisResult.verify" } - - log.debug { "checking $check in ${particle.spec.name}" } - val result = fixpoint.getValue(particle) - log.debug { "result: $result" } - // Unreachable particle => check is trivially satisfied. if (result.isBottom) return true @@ -709,8 +703,6 @@ fun InformationFlow.AnalysisResult.verify(particle: Recipe.Particle, check: Chec val accessPathLabels = result.getLabels(check.accessPath) - log.debug { "accessPathLabels: $accessPathLabels" } - // Unreachable => check is trivially satisfied. if (accessPathLabels.isBottom) return true // All possible values => check is unsatisfied. From 802861e59b2581f990382e488a2d65644dda6981 Mon Sep 17 00:00:00 2001 From: Alex Rosengarten Date: Wed, 5 May 2021 16:11:45 -0700 Subject: [PATCH 5/5] Updated OSS tooling to support new CLI. --- third_party/java/arcs/build_defs/internal/tools.oss.bzl | 1 - 1 file changed, 1 deletion(-) diff --git a/third_party/java/arcs/build_defs/internal/tools.oss.bzl b/third_party/java/arcs/build_defs/internal/tools.oss.bzl index e25e545f639..1d9e8567312 100644 --- a/third_party/java/arcs/build_defs/internal/tools.oss.bzl +++ b/third_party/java/arcs/build_defs/internal/tools.oss.bzl @@ -74,7 +74,6 @@ def arcs_tool_verify_policy(name, manifest_proto): name = name, test_binary = "//java/arcs/tools:verify_policy", test_args = [ - "--manifest", "$(rootpath %s)" % manifest_proto, ], data = [