From 80e29d032c6c6f3dc92bd4289be85753e03168f8 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 21 Apr 2022 12:44:01 -0700 Subject: [PATCH] [chore] remove mirai dataflow analysis to try to cut down on deps (#62) --- Cargo.lock | 12 - Cargo.toml | 1 - language/tools/README.md | 3 +- .../tools/mirai-dataflow-analysis/.gitignore | 2 - .../tools/mirai-dataflow-analysis/Cargo.toml | 18 - .../tools/mirai-dataflow-analysis/README.md | 229 ---------- .../mirai-dataflow-analysis/analyses/ddlog.dl | 396 ------------------ .../analyses/souffle.dl | 231 ---------- .../config/BoundsChecker_config.json | 25 -- .../config/CompiledModule_type_relations.json | 314 -------------- .../config/DuplicationChecker_config.json | 25 -- .../examples/BoundsChecker.md | 135 ------ .../examples/DuplicationChecker.md | 110 ----- .../examples/examples.md | 62 --- .../mirai-dataflow-analysis/rust-toolchain | 1 - .../src/configuration.rs | 141 ------- .../mirai-dataflow-analysis/src/datalog.rs | 121 ------ .../src/ddlog_output.rs | 131 ------ .../tools/mirai-dataflow-analysis/src/lib.rs | 2 - .../tools/mirai-dataflow-analysis/src/main.rs | 322 -------------- .../src/souffle_output.rs | 98 ----- .../tools/mirai-dataflow-analysis/src/util.rs | 24 -- .../tests/datalog_tests.rs | 122 ------ .../tests/ddlog_tests/AllDataflowVia.dat | 18 - .../tests/ddlog_tests/AllDataflowVia_loop.dat | 34 -- .../tests/ddlog_tests/AllTypedDataflowVia.dat | 33 -- .../ddlog_tests/AllTypedDataflowVia_loop.dat | 43 -- .../tests/ddlog_tests/Caller.dat | 12 - .../tests/ddlog_tests/CallerNT.dat | 11 - .../tests/ddlog_tests/Caller_loop.dat | 18 - .../tests/ddlog_tests/CheckedAtTypeBy.dat | 26 -- .../ddlog_tests/CheckedAtTypeBy_loop.dat | 29 -- .../tests/ddlog_tests/CheckedBy.dat | 20 - .../tests/ddlog_tests/CheckedBy_loop.dat | 22 - .../tests/ddlog_tests/Dataflow.dat | 32 -- .../tests/ddlog_tests/DataflowNotVia.dat | 32 -- .../tests/ddlog_tests/DataflowNotVia_loop.dat | 27 -- .../tests/ddlog_tests/DataflowVia.dat | 24 -- .../ddlog_tests/DataflowVia_mix_loop.dat | 28 -- .../tests/ddlog_tests/Dataflow_call_loop.dat | 32 -- .../tests/ddlog_tests/Dataflow_dom_loop.dat | 44 -- .../tests/ddlog_tests/Dataflow_mix_loop.dat | 45 -- .../tests/ddlog_tests/Dominates.dat | 16 - .../tests/ddlog_tests/DominatesNT.dat | 14 - .../tests/ddlog_tests/Dominates_loop.dat | 23 - .../tests/ddlog_tests/MemberTrans.dat | 17 - .../ddlog_tests/NeverCheckedAtTypeBy.dat | 39 -- .../ddlog_tests/NeverCheckedAtTypeBy_loop.dat | 38 -- .../tests/ddlog_tests/NeverCheckedBy.dat | 23 - .../tests/ddlog_tests/NeverCheckedBy_loop.dat | 22 - .../tests/ddlog_tests/NoDataflowVia.dat | 48 --- .../tests/ddlog_tests/NoDataflowVia_loop.dat | 32 -- .../tests/ddlog_tests/NoTypedDataflowVia.dat | 88 ---- .../ddlog_tests/NoTypedDataflowVia_loop.dat | 88 ---- .../tests/ddlog_tests/NotCheckedAtTypeBy.dat | 41 -- .../ddlog_tests/NotCheckedAtTypeBy_loop.dat | 40 -- .../tests/ddlog_tests/NotCheckedBy.dat | 24 -- .../tests/ddlog_tests/NotCheckedBy_loop.dat | 21 - .../tests/ddlog_tests/NotEqual.dat | 11 - .../tests/ddlog_tests/TypeEquality.dat | 18 - .../tests/ddlog_tests/TypedCaller.dat | 21 - .../tests/ddlog_tests/TypedCallerNT.dat | 20 - .../tests/ddlog_tests/TypedCaller_loop.dat | 22 - .../tests/ddlog_tests/TypedDataflow.dat | 71 ---- .../tests/ddlog_tests/TypedDataflowNotVia.dat | 27 -- .../ddlog_tests/TypedDataflowNotVia_loop.dat | 19 - .../tests/ddlog_tests/TypedDataflowVia.dat | 42 -- .../ddlog_tests/TypedDataflowVia_loop.dat | 35 -- .../tests/ddlog_tests/TypedDominates.dat | 28 -- .../tests/ddlog_tests/TypedDominatesNT.dat | 27 -- .../tests/ddlog_tests/TypedDominates_loop.dat | 28 -- .../tests/ddlog_tests/ValidNode.dat | 12 - .../tests/ddlog_tests/ValidType.dat | 14 - x.toml | 3 +- 74 files changed, 2 insertions(+), 4025 deletions(-) delete mode 100644 language/tools/mirai-dataflow-analysis/.gitignore delete mode 100644 language/tools/mirai-dataflow-analysis/Cargo.toml delete mode 100644 language/tools/mirai-dataflow-analysis/README.md delete mode 100644 language/tools/mirai-dataflow-analysis/analyses/ddlog.dl delete mode 100644 language/tools/mirai-dataflow-analysis/analyses/souffle.dl delete mode 100644 language/tools/mirai-dataflow-analysis/config/BoundsChecker_config.json delete mode 100644 language/tools/mirai-dataflow-analysis/config/CompiledModule_type_relations.json delete mode 100644 language/tools/mirai-dataflow-analysis/config/DuplicationChecker_config.json delete mode 100644 language/tools/mirai-dataflow-analysis/examples/BoundsChecker.md delete mode 100644 language/tools/mirai-dataflow-analysis/examples/DuplicationChecker.md delete mode 100644 language/tools/mirai-dataflow-analysis/examples/examples.md delete mode 100644 language/tools/mirai-dataflow-analysis/rust-toolchain delete mode 100644 language/tools/mirai-dataflow-analysis/src/configuration.rs delete mode 100644 language/tools/mirai-dataflow-analysis/src/datalog.rs delete mode 100644 language/tools/mirai-dataflow-analysis/src/ddlog_output.rs delete mode 100644 language/tools/mirai-dataflow-analysis/src/lib.rs delete mode 100644 language/tools/mirai-dataflow-analysis/src/main.rs delete mode 100644 language/tools/mirai-dataflow-analysis/src/souffle_output.rs delete mode 100644 language/tools/mirai-dataflow-analysis/src/util.rs delete mode 100644 language/tools/mirai-dataflow-analysis/tests/datalog_tests.rs delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllDataflowVia.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllDataflowVia_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllTypedDataflowVia.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllTypedDataflowVia_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Caller.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CallerNT.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Caller_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedAtTypeBy.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedAtTypeBy_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedBy.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedBy_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowNotVia.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowNotVia_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowVia.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowVia_mix_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_call_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_dom_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_mix_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dominates.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DominatesNT.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dominates_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/MemberTrans.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedAtTypeBy.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedAtTypeBy_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedBy.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedBy_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoDataflowVia.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoDataflowVia_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoTypedDataflowVia.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoTypedDataflowVia_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedAtTypeBy.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedAtTypeBy_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedBy.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedBy_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotEqual.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypeEquality.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCaller.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCallerNT.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCaller_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflow.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowNotVia.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowNotVia_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowVia.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowVia_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominates.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominatesNT.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominates_loop.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/ValidNode.dat delete mode 100644 language/tools/mirai-dataflow-analysis/tests/ddlog_tests/ValidType.dat diff --git a/Cargo.lock b/Cargo.lock index 5f6111c227..2a11b898e0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1837,18 +1837,6 @@ version = "1.12.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c9be0862c1b3f26a88803c4a49de6889c10e608b3ee9344e6ef5b45fb37ad3d1" -[[package]] -name = "mirai-dataflow-analysis" -version = "0.1.0" -dependencies = [ - "clap 3.1.8", - "csv", - "mirai-annotations", - "regex", - "serde 1.0.130", - "serde_json", -] - [[package]] name = "module-generation" version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml index 8bcb961621..c4c491eef0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -52,7 +52,6 @@ members = [ "language/testing-infra/module-generation", "language/testing-infra/test-generation", "language/testing-infra/transactional-test-runner", - "language/tools/mirai-dataflow-analysis", "language/tools/move-bytecode-utils", "language/tools/move-bytecode-viewer", "language/tools/move-cli", diff --git a/language/tools/README.md b/language/tools/README.md index ca7f1267b7..17f3f01a96 100644 --- a/language/tools/README.md +++ b/language/tools/README.md @@ -47,7 +47,6 @@ The `move-resource-viewer`, and `read-write-set` similarly are library crates that are used by and exposed by the Move CLI, but not through the `package` subcommand. -The `mirai-dataflow-analysis` and `move-bytecode-utils` crates are separate -crates that are either experimental in nature, or libraries holding general +The `move-bytecode-utils` crates holds general utilities for working with Move bytecode, e.g., computing the dependency order for modules. diff --git a/language/tools/mirai-dataflow-analysis/.gitignore b/language/tools/mirai-dataflow-analysis/.gitignore deleted file mode 100644 index f4d9deb80d..0000000000 --- a/language/tools/mirai-dataflow-analysis/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -**/*_ddlog/ -output diff --git a/language/tools/mirai-dataflow-analysis/Cargo.toml b/language/tools/mirai-dataflow-analysis/Cargo.toml deleted file mode 100644 index ba73e9e7a3..0000000000 --- a/language/tools/mirai-dataflow-analysis/Cargo.toml +++ /dev/null @@ -1,18 +0,0 @@ -[package] -name = "mirai-dataflow-analysis" -version = "0.1.0" -authors = ["Diem Association "] -description = "MIRAI Dataflow analysis tool" -repository = "https://github.com/diem/diem" -homepage = "https://diem.com" -license = "Apache-2.0" -publish = false -edition = "2018" - -[dependencies] -csv = "1.1" -mirai-annotations = "1.12" -regex = "1.4.3" -serde = {version="1.0", features=["derive"]} -serde_json = "1.0" -clap = { version = "3.1.8", features = ["derive"] } diff --git a/language/tools/mirai-dataflow-analysis/README.md b/language/tools/mirai-dataflow-analysis/README.md deleted file mode 100644 index 23695b224a..0000000000 --- a/language/tools/mirai-dataflow-analysis/README.md +++ /dev/null @@ -1,229 +0,0 @@ -# MIRAI Dataflow Analyzer - -This tool (`mirai-dataflow`) provides an end-to-end method for running a dataflow analysis over a Rust crate. -Internally, this tool uses [MIRAI](https://github.com/facebookexperimental/MIRAI) to generate a call graph of a Rust crate, as well as a Datalog -representation of that call graph. Then, a dataflow analysis is run over the call graph using either -[Differential Datalog](https://github.com/vmware/differential-datalog) or [Soufflé](https://souffle-lang.github.io/) and decoded results are presented. - -## Examples -Please see the included [examples](examples/examples.md) for notes on analysis construction, execution, and results. - -## Installation - -This tool depends on the presence of MIRAI, correctly installed on your system, as well as -either an installation of either Differential Datalog or Soufflé Datalog. Thus, to get a complete -setup, please follow the steps below: - -1. Install MIRAI by following the instructions in its [readme](https://github.com/facebookexperimental/MIRAI#readme). -2. Install Soufflé and / or Differential Datalog. -3. Set the nightly version of Rust for this crate using `rustup override set nightly-YYYY-MM-DD`. - - See [rust-toolchain](./rust_toolchain)) to determine the current compatible version, which in turn - must match the version [currently in use by MIRAI](https://github.com/facebookexperimental/MIRAI/blob/main/rust-toolchain). - -Please note that the MIRAI's [is_excluded](https://github.com/facebookexperimental/MIRAI/blob/49c8add3706d49f82d96f3ace2c01c738ea04dc2/checker/src/callbacks.rs#L145) function may have to be modified _before_ installing MIRAI to not exclude certain crates. - -### Differential-Datalog-specific step - -If Differential Datalog is being used, please additionally use Differential Datalog to build `analyses/ddlog.dl`. -``` -$ cd analyses/ -$ ddlog -i ddlog.dl -$ cd ddlog_ddlog && cargo build --release -``` -This will create a Rust crate (`analyses/ddlog_ddlog`) that includes a CLI that the `mirai-dataflow` -interfaces with to perform its analysis. - -## Configuration - -`mirai-dataflow` is configured via a combination of CLI arguments and a configuration file. - -### CLI - -`mirai-dataflow` exposes the following CLI (viewable via the `--help` flag): -``` -Rust dataflow analyzer built on MIRAI. - -USAGE: - mirai-dataflow-analysis [FLAGS] [OPTIONS] - -FLAGS: - --call-graph-only Only produce a call graph (no analysis) - -h, --help Prints help information - -n, --no-rebuild Do not rebuild the crate before analysis - -r, --reanalyze Rerun the Datalog analysis without running MIRAI - -V, --version Prints version information - -OPTIONS: - -d, --datalog-backend Datalog backend to use (DifferentialDatalog | Souffle) - -t, --type-relations-path Path to input type relations - -ARGS: - Path to the crate to analyze - Path to configuration file -``` - -The `crate-path` is the path to the crate you want to analyze. The `config-path` is a path to -a configuration file (explained below). Finally, the `type-relations-path` is a path to a set of -input type relations (see the call graph generator's -[documentation](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/CallGraph.md#type-relations) -for details). - -### Config File - -One of the required CLI arguments is a path to a configuration file. This configuration file tells -`mirai-dataflow` how the generated call graph should be preprocessed before analysis. - -The configuration file is a JSON file following this schema: -``` -{ - "reductions": List[Reduction], - "included_crates": List[String], - "node_types": { - "entry": List[String], - "checker: List[String], - "safe": List[String], - "exit": List[String] - } -} -``` -where a Reduction is one of: -``` -{"Slice": String} -"Fold" -"Clean" -"Deduplicate" -``` - -Please see the call graph generator's -[documentation](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/CallGraph.md) -for more details on the "reductions" and "included_crates" fields. - -#### Node Type Specifications - -The `node_type` configuration is of particular importance as it is used to inform the analysis -of entry points, exit points, checkers, and endpoints that can be safely ignored. -Please see below for an explanation of each of these types: - -1. Entry: This is a list of names of function that are considered entry points of the crate. -2. Checker: Names of functions that are considered checking functions of the crate. -3. Safe: Names of functions that are not checking functions, but are "safe" if they are endpoints -where an unchecked dataflow ends. This field is typically used to exclude function endpoints that -are false positives for an analysis. -4. Exit: Names of functions that are considered the exit points of the crate. - -These node types are converted into datalog input relations that are provided to the analysis -as well as the call graph input relations. -For Soufflé, a file name `NodeType.facts` is generated with relations of the form: -1. Entry: `{node_id},0` -2. Checker: `{node_id},1` -3. Safe: `{node_id},1` -4. Exit: `{node_id},2` - -For Differential Datalog, input relations are added directly to the call graph input relations file: -1. Entry: `NodeType({node_id},Entry)` -2. Checker: `NodeType({node_id},Checker)` -3. Safe: `NodeType({node_id},Checker)` -4. Exit: `NodeType({node_id},Exit)` - -Note that both Checker and Safe are assigned to Checker. This is a valid optimization as semantically -they are the same in the default analysis, but if an analysis assigns a different meaning to them -this can be modified. - -#### Example Configuration - -Below is an example of a valid configuration file: -``` -{ - "reductions": [ - {"Slice": "verify_impl"}, - "Fold", - "Clean" - ], - "included_crates": ["check_bounds"], - "node_types": { - "entry": [ - "verify_impl" - ], - "checker": [ - "check_bounds_impl", - "check_code_unit_bounds_impl", - "check_type_parameter" - ], - "exit": [ - "verify_impl_exit" - ] - } -} -``` - -## Usage - -Having configured `mirai-dataflow` as explained above, the analysis can then be run: -``` -$ cargo run -- ../../move-binary-format config/call_graph_config.json --type-relations-path=config/type_relations.json -``` - -`mirai-dataflow` will then execute MIRAI on the crate and then execute the Datalog analysis: -``` -... -Running MIRAI... -Done -Running analysis... -Done -Processing output... -Done -``` - -Finally, a folder called `output` should be created which will contain all of the analysis -artifacts from this run. Most importantly, it will contain a file `decoded.json` that has -the decoded Datalog output relation results. - -For example, if the output relations are `CheckedType(t)` (indicating that a type was checked -as expected) and `NotCheckedType(t)` (indicating that a type that was supposed to be checked -was not), you may see results like this in `decoded.json`: -``` -[ - { - "name": "CheckedType", - "operands": [ - { - "name": "t", - "index": 34, - "string": "file_format::IdentifierIndex", - "op_type": "Type" - } - ] - }, - ... - { - "name": "NotCheckedType", - "operands": [ - { - "name": "t", - "index": 16, - "string": "usize", - "op_type": "Type" - } - ] - } -] -``` - -In this case, an analyst may focus on the occurrences of `NotCheckedType` as they represent -potential issues in the analyzed crate. If the Soufflé Datalog backend is used, further triage -may be done via the Soufflé explain command, which produces a proof tree for an output fact. - -``` -$ cd output -$ souffle -t explain ../analyses/souffle.dl -Explain is invoked. -Enter command > explain NotCheckedType(16) -EdgeType(40, 16) --------------(R1) - ValidType(16) !CheckedType(16) --------------------------------(R1) - NotCheckedType(16) -``` - -Also useful is Soufflé's `explainnegation` command which can be used to interactively explore -why a particular fact _does not_ exist. diff --git a/language/tools/mirai-dataflow-analysis/analyses/ddlog.dl b/language/tools/mirai-dataflow-analysis/analyses/ddlog.dl deleted file mode 100644 index 4e1906eda5..0000000000 --- a/language/tools/mirai-dataflow-analysis/analyses/ddlog.dl +++ /dev/null @@ -1,396 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// SPDX-License-Identifier: Apache-2.0 -// ================================================ - -// Types -// Unique edge identifier -typedef EdgeID = u32 -// Unique node identifier -typedef NodeID = u32 -// Unique Rust type identifier -typedef TypeID = u32 -// The (annotated) kind of a node -typedef Nkind = Entry | Exit | Checker - - -// A node may be marked as an entry, an exit, or a checker -input relation NodeType(id: NodeID, nkind: Nkind) - - -// An edge connects two nodes and has a Rust type (rtype) -input relation Edge(id: EdgeID, node1: NodeID, node2: NodeID) -input relation EdgeType(id: EdgeID, rtype: TypeID) - - -// In the control flow graph, node1 dominates node2 -input relation Dom(node1: NodeID, node2: NodeID) - - -// Encodes that the type rtype2 is a member of type rtype1 -input relation Member(rtype1: TypeID, rtype2: TypeID) - - -// Encodes that rtype1 is equivalent to rtype1 -// (for the purpose of this analysis) -input relation EqType(rtype1: TypeID, rtype2: TypeID) - - -// A valid node is connected to the graph -output relation ValidNode(node: NodeID) -ValidNode(node) :- Edge(_, node, _). -ValidNode(node) :- Edge(_, _, node). - - -// Not the same node -// Node identifiers do not match -output relation NotEqual(node1: NodeID, node2: NodeID) -NotEqual(node1, node2) :- ValidNode(node1), ValidNode(node2), (node1 != node2). -NotEqual(node2, node1) :- NotEqual(node1, node2). - - -// Caller (non-transitive) -output relation CallerNT(node1: NodeID, node2: NodeID) -CallerNT(node1, node2) :- Edge(_, node1, node2). - - -// Caller -// node1 (transitively) calls node2 -output relation Caller(node1: NodeID, node2: NodeID) -Caller(node1, node2) :- CallerNT(node1, node2). -Caller(node1, node3) :- CallerNT(node1, node2), Caller(node2, node3), NotEqual(node1, node3). - - -// Dominates (non-transitive) -output relation DominatesNT(node1: NodeID, node2: NodeID) -DominatesNT(node1, node2) :- Dom(node1, node2). - - -// Transitive dominance -// Either there is an explicit (possibly transitive) dominance relationship -// Or the node has a caller with an explicit dominance relationship. -output relation Dominates(node1: NodeID, node2: NodeID) -Dominates(node1, node2) :- DominatesNT(node1, node2). -Dominates(node1, node3) :- DominatesNT(node1, node2), Dominates(node2, node3), NotEqual(node1, node3). -Dominates(node1, node2) :- Caller(parent, node1), NotEqual(node1, node2), Dominates(parent, node2). - - -// Dataflow model (non-transitive) -// Data flows from node1 to node2: -// a. if node1 directly calls node2 -// b. if node1 directly dominates node2 -output relation DataflowNT(node1: NodeID, node2: NodeID) -DataflowNT(node1, node2) :- CallerNT(node1, node2). -DataflowNT(node1, node2) :- DominatesNT(node1, node2). - - -// Dataflow model -// Data flows from node1 to node2: -// a. if node1 (transitively) calls node2 -// b. if node1 (transitively) dominates node2 -// c. if there transitively is a dataflow -output relation Dataflow(node1: NodeID, node2: NodeID) -Dataflow(node1, node2) :- Caller(node1, node2). -Dataflow(node1, node2) :- Dominates(node1, node2). -Dataflow(node1, node3) :- Dataflow(node1, node2), Dataflow(node2, node3). - - -// Dataflow via -// There exists a dataflow from node1 to node3 that passes through node2. -// This does not imply that every dataflow from node1 to node3 flows via node2. -output relation DataflowVia(node1: NodeID, node2: NodeID, node3: NodeID) -DataflowVia(node1, node2, node3) :- Dataflow(node1, node2), NotEqual(node1, node2), - Dataflow(node2, node3), NotEqual(node2, node3). - - -// Dataflow not via -// There exists a dataflow from node1 to node3 that does not pass through node2. -// -// a. There is a non-transitive dataflow from node1 to node3 (no intermediate nodes). -// b. There is a dataflow from node1 to node3 that passes through some node4 != node2. -// Since there is no dataflow from node2 to node4, node2 cannot be in that same flow. -// -// This is not guaranteed if an over-approximation of the call graph is used. -output relation DataflowNotVia(node1: NodeID, node2: NodeID, node3: NodeID) -DataflowNotVia(node1, node2, node3) :- NotEqual(node1, node2), NotEqual(node2, node3), - DataflowNT(node1, node3). -DataflowNotVia(node1, node2, node3) :- NotEqual(node1, node2), NotEqual(node2, node3), - DataflowVia(node1, node4, node3), NotEqual(node2, node4), - not Dataflow(node2, node4). - - -// No dataflow via -// There is no dataflow path from node1 to node3 that passes through node2. -// This is guaranteed to be true if an over-approximation of the call graph is used. -output relation NoDataflowVia(node1: NodeID, node2: NodeID, node3: NodeID) -NoDataflowVia(node1, node2, node3) :- NotEqual(node1, node2), NotEqual(node2, node3), - not DataflowVia(node1, node2, node3). - - -// All dataflow via -// Every path from node1 to node3 passes through node2. -// -// This occurs in two cases: -// a. If node2 dominates node3 then this holds for all dataflows from node1 to node2. -// b. If there is no dataflow from node1 to node3 that does not pass through node2. -// -// This is guaranteed to be true if an over-approximation of the call graph is used. -output relation AllDataflowVia(node1: NodeID, node2: NodeID, node3: NodeID) -AllDataflowVia(node1, node2, node3) :- Dataflow(node1, node2), Dom(node2, node3). -AllDataflowVia(node1, node2, node3) :- DataflowVia(node1, node2, node3), not DataflowNotVia(node1, node2, node3). -AllDataflowVia(node1, node2, node4) :- AllDataflowVia(node1, node2, node3), NotEqual(node1, node2), - AllDataflowVia(node2, node3, node4), NotEqual(node2, node4). -AllDataflowVia(node1, node3, node4) :- AllDataflowVia(node1, node2, node3), NotEqual(node1, node3), - AllDataflowVia(node2, node3, node4), NotEqual(node3, node4). - - -// Not checked by -// A node is not checked by a checker -// a. If the node has no outgoing dataflow -// b. If the node only has dataflow to a single node that is not the checker. -// c. If there exists some exit node2 such that the dataflow from node1 to node2 -// does not pass through the checker. -// This is not guaranteed if an over-approximation of the call graph is used. -output relation NotCheckedBy(node: NodeID, checker: NodeID) -NotCheckedBy(node1, checker) :- NodeType(checker, Checker), ValidNode(node1), not Dataflow(node1, _). -NotCheckedBy(node1, checker) :- NodeType(checker, Checker), DataflowNT(node1, node2), - NotEqual(node2, checker), not Dataflow(node2, _). -NotCheckedBy(node1, checker) :- NodeType(checker, Checker), NodeType(node2, Exit), - Dataflow(node1, node2), DataflowNotVia(node1, checker, node2). - - -// Checked by -// A node is checked by a checker -// a. If every dataflow from the node to an exit passes through the checker. -// b. If every dataflow from the node terminates in the checker. -// This checking is guaranteed if an over-approximation of the call graph is used. -output relation CheckedBy(node: NodeID, checker: NodeID) -CheckedBy(node, checker) :- NodeType(checker, Checker), NotEqual(node, checker), - DataflowNT(node, checker), not NotCheckedBy(node, checker). -CheckedBy(node, checker) :- NodeType(checker, Checker), NotEqual(node, checker), NodeType(node2, Exit), - AllDataflowVia(node, checker, node2), not NotCheckedBy(node, checker). -CheckedBy(node, checker2) :- CheckedBy(node, checker), CheckedBy(checker, checker2). - - -// Never checked by -// No dataflow from the node passes through the checker. -output relation NeverCheckedBy(node: NodeID, checker: NodeID) -NeverCheckedBy(node, checker) :- ValidNode(node), NodeType(checker, Checker), not Dataflow(node, checker). - - -// Valid type -// A valid type is associated with some edge in the graph. -// or is associated with some input type relation. -output relation ValidType(rtype: TypeID) -ValidType(rtype) :- EdgeType(_, rtype). -ValidType(t) :- EdgeType(_, t). -ValidType(t) :- Member(t, _). -ValidType(t) :- Member(_, t). -ValidType(t) :- EqType(t, _). -ValidType(t) :- EqType(_, t). - - -// Type equality -// Encodes that rtype1 and rtype2 either -// a. Known to be equal -// b. Nominally equal -output relation TypeEquality(rtype1: TypeID, rtype2: TypeID) -TypeEquality(rtype1, rtype2) :- ValidType(rtype1), ValidType(rtype2), rtype1 == rtype2. -TypeEquality(rtype1, rtype2) :- EqType(rtype1, rtype2). -TypeEquality(rtype1, rtype2) :- EqType(rtype2, rtype1). - - -// Transitive type member (includes type equality) -// Encodes that rtype2 is a (transitive) member of rtype1 if -// a. rtype1 == rtype2 -// b. rtype2 is (transitively) a member of rtype1 -// c. rtype1 and rtype2 are equal to some other rtypes that -// are in a membership relationship -output relation MemberTrans(rtype1: TypeID, rtype2: TypeID) -MemberTrans(rtype1, rtype2) :- TypeEquality(rtype1, rtype2). -MemberTrans(rtype1, rtype2) :- Member(rtype1, rtype2). -MemberTrans(rtype1, rtype3) :- Member(rtype1, rtype2), MemberTrans(rtype2, rtype3). -MemberTrans(rtype1a, rtype2a) :- TypeEquality(rtype1a, rtype1b), - TypeEquality(rtype2a, rtype2b), - MemberTrans(rtype1b, rtype2b). - - -// Typed caller (non-transitive) -// node1 is a caller of node2 at type t if there is an edge from node1 -// to node2 that is of type t' where t' == t or t is a member of t'. -output relation TypedCallerNT(node1: NodeID, node2: NodeID, t: TypeID) -TypedCallerNT(node1, node2, t2) :- Edge(id, node1, node2), EdgeType(id, t), MemberTrans(t, t2). - - -// Typed caller -// A caller, node1, can be typed at t if -// a. node1 calls node2 with an argument of type t -// b. node1 calls a sequence of nodes with arguments whose types are members -// of t up to the call to node2 -// c. t is a subtype of t2 and node1 calls node2 with t2 -output relation TypedCaller(node1: NodeID, node2: NodeID, t: NodeID) -TypedCaller(node1, node2, t) :- TypedCallerNT(node1, node2, t). -TypedCaller(node1, node3, t) :- TypedCallerNT(node1, node2, t), TypedCaller(node2, node3, t). -TypedCaller(node1, node2, t) :- MemberTrans(t2, t), TypedCaller(node1, node2, t2). - - -// Dominates with typing (non-transitive) -// node1 dominates node2 at type t if: -// node1 dominates node2 -// and -// node1 can be typed at t2, -// node2 can be typed at t3, -// and t is a member of both t2 and t3. -// Note that node1 and node2 must share some parent node. -output relation TypedDominatesNT(node1: NodeID, node2: NodeID, t: TypeID) -TypedDominatesNT(node1, node2, t) :- Dom(node1, node2), Edge(id1, parent, node1), Edge(id2, parent, node2), - EdgeType(id1, t2), EdgeType(id2, t3), MemberTrans(t2, t), MemberTrans(t3, t). - - -// Transitive dominance with typing -// Given node1, node2, and type t, either -// a. node1 non-transitively dominates node2 at type t -// b. node2 is a callee of some node that is dominated by node1 at type t. -// (This case is a heuristic that should be obviated with precise dominance information.) -// c. t is a subtype of t2 and node1 dominates node2 for t2 -output relation TypedDominates(node1: NodeID, node2: NodeID, t: TypeID) -TypedDominates(node1, node2, t) :- TypedDominatesNT(node1, node2, t). -TypedDominates(node1, node3, t) :- TypedDominatesNT(node1, node2, t), TypedDominates(node2, node3, t). -TypedDominates(node1, node2, t) :- TypedCaller(parent, node1, t), TypedDominates(parent, node2, t). -TypedDominates(node1, node2, t) :- Member(t2, t), TypedDominates(node1, node2, t2). - - -// Typed dataflow model (non-transitive) -// Data flows from node1 to node2: -// a. if node1 directly calls node2 at type t -// b. if node1 directly dominates node2 at type t -output relation TypedDataflowNT(node1: NodeID, node2: NodeID, t: TypeID) -TypedDataflowNT(node1, node2, t) :- TypedCallerNT(node1, node2, t). -TypedDataflowNT(node1, node2, t) :- TypedDominatesNT(node1, node2, t). - - -// Typed dataflow model -// Data of type t flows from node1 to node2 -// a. if node1 transitively calls node2 at type t -// b. if node1 transitively dominates node2 at type t -// c. if there transitively is a dataflow at type t -// d. if there is a dataflow of type t2 and t is a member of t2 -output relation TypedDataflow(node1: NodeID, node2: NodeID, t: TypeID) -TypedDataflow(node1, node2, t) :- TypedCaller(node1, node2, t). -TypedDataflow(node1, node2, t) :- TypedDominates(node1, node2, t). -TypedDataflow(node1, node3, t) :- TypedDataflow(node1, node2, t), TypedDataflow(node2, node3, t). -TypedDataflow(node1, node2, t) :- MemberTrans(t2, t), TypedDataflow(node1, node2, t2). - - -// Typed dataflow via -// There exists a dataflow from node1 to node3 that passes through node2 -// that can be typed at t. -output relation TypedDataflowVia(node1: NodeID, node2: NodeID, node3: NodeID, t: TypeID) -TypedDataflowVia(node1, node2, node3, t) :- TypedDataflow(node1, node2, t), NotEqual(node1, node2), - TypedDataflow(node2, node3, t), NotEqual(node2, node3). - - -// Safe dataflow -// A dataflow from node1 to node2 (a checker) is considered safe if -// a. node1 is a checker -// b. node1 has a dataflow to node2 -// c. node2 dominates node1 for t -output relation SafeDataflow(node1: NodeID, node2: NodeID, t: TypeID) -SafeDataflow(node1, node2, t) :- ValidNode(node2), ValidType(t), NodeType(node1, Checker). -SafeDataflow(node1, node2, t) :- TypedDataflow(node1, node2, t). -SafeDataflow(node1, node2, t) :- TypedDominates(node2, node1, t). - - -// Terminal node -// A node is a terminal node if it does not have any outgoing edges. -output relation TerminalNode(node: NodeID) -TerminalNode(node) :- ValidNode(node), not Edge(_, node, _). - - -// Typed dataflow not via -// There exists a dataflow of type t from node1 to node3 that does not pass through node2. -// -// a. There is a terminal non-transitive dataflow of type t from node1 to node3, and node3 is not -// dominated by node2 for t. -// b. There is a dataflow of type t from node1 to node3 that passes through some node4 != node2. -// Since there is no dataflow of type t from node2 to node4, node2 cannot be in that same flow. -// -// This is not guaranteed if an over-approximation of the call graph is used. -output relation TypedDataflowNotVia(node1: NodeID, node2: NodeID, node3: NodeID, t: TypeID) -TypedDataflowNotVia(node1, node2, node3, t) :- NotEqual(node1, node2), NotEqual(node2, node3), TerminalNode(node3), - TypedDataflowNT(node1, node3, t), not TypedDominates(node2, node3, t). -TypedDataflowNotVia(node1, node2, node3, t) :- NotEqual(node1, node2), NotEqual(node2, node3), - TypedDataflowVia(node1, node4, node3, t), NotEqual(node2, node4), - not SafeDataflow(node4, node2, t). - - -// No typed dataflow via -// There is no dataflow path of type t from node1 to node3 that passes through node2. -// This relation is expensive for bottom-up evaluation. -output relation NoTypedDataflowVia(node1: NodeID, node2: NodeID, node3: NodeID, t: TypeID) -NoTypedDataflowVia(node1, node2, node3, t) :- NotEqual(node1, node2), NotEqual(node2, node3), ValidType(t), - not TypedDataflowVia(node1, node2, node3, t). - - -// All typed dataflow via -// Every path from node1 to node3 of type t passes through node2 -// This occurs in two cases: -// a. If node2 dominates node3 at type t then this holds for all dataflows from node1 to node2. -// b. If there is no dataflow from node1 to node3 of type t that does not pass through node2. -output relation AllTypedDataflowVia(node1: NodeID, node2: NodeID, node3: NodeID, t: TypeID) -AllTypedDataflowVia(node1, node2, node3, t) :- TypedDataflow(node1, node2, t), TypedDominates(node2, node3, t). -AllTypedDataflowVia(node1, node2, node3, t) :- TypedDataflowVia(node1, node2, node3, t), not TypedDataflowNotVia(node1, node2, node3, t). -AllTypedDataflowVia(node1, node2, node4, t) :- AllTypedDataflowVia(node1, node2, node3, t), NotEqual(node1, node2), - AllTypedDataflowVia(node2, node3, node4, t), NotEqual(node2, node4). -AllTypedDataflowVia(node1, node3, node4, t) :- AllTypedDataflowVia(node1, node2, node3, t), NotEqual(node1, node3), - AllTypedDataflowVia(node2, node3, node4, t), NotEqual(node3, node4). - - -// Not checked at type by -// A node is not checked by a checker at type t -// a. If the node has no outgoing dataflow of type t -// b. If the node only has dataflow of type t to a single node that is not the checker. -// c. If there exists some exit node2 such that the dataflow from node1 to node2 of type t -// does not pass through the checker. -output relation NotCheckedAtTypeBy(node: NodeID, checker: NodeID, t: TypeID) -NotCheckedAtTypeBy(node1, checker, t) :- NodeType(checker, Checker), ValidNode(node1), ValidType(t), - not TypedDataflow(node1, _, t). -NotCheckedAtTypeBy(node1, checker, t) :- NodeType(checker, Checker), TypedDataflowNT(node1, node2, t), - NotEqual(node2, checker), not TypedDataflow(node2, _, t). -NotCheckedAtTypeBy(node1, checker, t) :- NodeType(checker, Checker), NodeType(node2, Exit), - TypedDataflow(node1, node2, t), TypedDataflowNotVia(node1, checker, node2, t). - - -// Checked by at type -// A node is checked by a checker at type t -// a. If every dataflow of type t from the node to an exit passes through the checker. -// b. If every dataflow of type t from the node terminates in the checker. -// c. If the node is checked by the checker at type t2, which t is a member of. -output relation CheckedAtTypeBy(node: NodeID, checker: NodeID, t: TypeID) -CheckedAtTypeBy(node, checker, t) :- NodeType(checker, Checker), NotEqual(node, checker), - TypedDataflowNT(node, checker, t), not NotCheckedAtTypeBy(node, checker, t). -CheckedAtTypeBy(node, checker, t) :- NodeType(checker, Checker), NotEqual(node, checker), NodeType(exit, Exit), - AllTypedDataflowVia(node, checker, exit, t), not NotCheckedAtTypeBy(node, checker, t). -CheckedAtTypeBy(node, checker2, t) :- CheckedAtTypeBy(node, checker, t), CheckedAtTypeBy(checker, checker2, t). -CheckedAtTypeBy(node, checker, t) :- CheckedAtTypeBy(node, checker, t2), Member(t2, t). - - -// Never checked at type by -// No dataflow of type t from the node passes through the checker. -output relation NeverCheckedAtTypeBy(node: NodeID, checker: NodeID, t: TypeID) -NeverCheckedAtTypeBy(node, checker, t) :- ValidNode(node), NodeType(checker, Checker), ValidType(t), - not TypedDataflow(node, checker, t). - - -// Checked type -// All dataflow of type t pass through a checker -// There does not exist a dataflow of type t that does not pass through a checker -output relation CheckedType(t: TypeID) -CheckedType(t) :- ValidType(t), NodeType(checker, Checker), NodeType(exit, Exit), - TypedDataflowVia(entry, checker, exit, t), - not TypedDataflowNotVia(_, checker, exit, t). - - -// Not checked type -// There exists a dataflow of type t that does not pass through a checker -output relation NotCheckedType(t: TypeID) -NotCheckedType(t) :- ValidType(t), not CheckedType(t). diff --git a/language/tools/mirai-dataflow-analysis/analyses/souffle.dl b/language/tools/mirai-dataflow-analysis/analyses/souffle.dl deleted file mode 100644 index 4b6fc3b758..0000000000 --- a/language/tools/mirai-dataflow-analysis/analyses/souffle.dl +++ /dev/null @@ -1,231 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// SPDX-License-Identifier: Apache-2.0 -// ================================================ - - -// Types -// Unique edge identifier -.type EdgeID = number -// Unique node identifier -.type NodeID = number -// Unique Rust type identifier -.type TypeID = number -// The (annotated) kind of a node -// 0 -> entry -// 1 -> checker -// 2 -> exit -.type Nkind = number - - -// A node may be marked as an entry, an exit, or a checker -.decl NodeType(id: NodeID, nkind: Nkind) -.input NodeType(IO=file, delimiter=",") - - -// An edge connects two nodes and has a Rust type (rtype) -.decl Edge(id: EdgeID, node1: NodeID, node2: NodeID) -.input Edge(IO=file, delimiter=",") - -.decl EdgeType(id: EdgeID, rtype: TypeID) -.input EdgeType(IO=file, delimiter=",") - - -// In the control flow graph, node1 dominates node2 -.decl Dom(node1: NodeID, node2: NodeID) -.input Dom(IO=file, delimiter=",") - - -// Encodes that the type rtype2 is a member of type rtype1 -.decl Member(rtype1: TypeID, rtype2: TypeID) -.input Member(IO=file, delimiter=",") - - -// Encodes that rtype1 is equivalent to rtype1 -// (for the purpose of this analysis) -.decl EqType(rtype1: TypeID, rtype2: TypeID) -.input EqType(IO=file, delimiter=",") - - -// A valid node is connected to the graph -.decl ValidNode(node: NodeID) -ValidNode(node) :- Edge(_, node, _). -ValidNode(node) :- Edge(_, _, node). - - -// Not the same node -// Node identifiers do not match -.decl NotEqual(node1: NodeID, node2: NodeID) -NotEqual(node1, node2) :- ValidNode(node1), ValidNode(node2), (node1 != node2). -NotEqual(node2, node1) :- NotEqual(node1, node2). - - -// Valid type -// A valid type is associated with some edge in the graph -// or is associated with some input type relation. -.decl ValidType(t: TypeID) -ValidType(t) :- EdgeType(_, t). -ValidType(t) :- Member(t, _). -ValidType(t) :- Member(_, t). -ValidType(t) :- EqType(t, _). -ValidType(t) :- EqType(_, t). - - -// Type equality -// Encodes that rtype1 and rtype2 either -// a. Known to be equal -// b. Nominally equal -.decl TypeEquality(rtype1: TypeID, rtype2: TypeID) -TypeEquality(rtype1, rtype2) :- ValidType(rtype1), ValidType(rtype2), rtype1 = rtype2. -TypeEquality(rtype1, rtype2) :- EqType(rtype1, rtype2). -TypeEquality(rtype1, rtype2) :- EqType(rtype2, rtype1). - - -// Transitive type member (includes type equality) -// Encodes that rtype2 is a (transitive) member of rtype1 if -// a. rtype1 == rtype2 -// b. rtype2 is (transitively) a member of rtype1 -// c. rtype1 and rtype2 are equal to some other rtypes that -// are in a membership relationship -.decl MemberTrans(rtype1: TypeID, rtype2: TypeID) -MemberTrans(rtype1, rtype2) :- TypeEquality(rtype1, rtype2). -MemberTrans(rtype1, rtype2) :- Member(rtype1, rtype2). -MemberTrans(rtype1, rtype3) :- Member(rtype1, rtype2), MemberTrans(rtype2, rtype3). -MemberTrans(rtype1a, rtype2a) :- TypeEquality(rtype1a, rtype1b), - TypeEquality(rtype2a, rtype2b), - MemberTrans(rtype1b, rtype2b). - -// Typed caller (non-transitive) -// node1 is a caller of node2 at type t if there is an edge from node1 -// to node2 that is of type t' where t' == t or t is a member of t'. -.decl TypedCallerNT(node1: NodeID, node2: NodeID, t: TypeID) -TypedCallerNT(node1, node2, t2) :- Edge(id, node1, node2), EdgeType(id, t), MemberTrans(t, t2). - - -// Typed caller -// A caller, node1, can be typed at t if -// a. node1 calls node2 with an argument of type t -// b. node1 calls a sequence of nodes with arguments whose types are members -// of t up to the call to node2 -// c. t is a subtype of t2 and node1 calls node2 with t2 -.decl TypedCaller(node1: NodeID, node2: NodeID, t: NodeID) -TypedCaller(node1, node2, t) :- TypedCallerNT(node1, node2, t). -TypedCaller(node1, node3, t) :- TypedCallerNT(node1, node2, t), TypedCaller(node2, node3, t). -TypedCaller(node1, node2, t) :- MemberTrans(t2, t), TypedCaller(node1, node2, t2). - - -// Dominates with typing (non-transitive) -// node1 dominates node2 at type t if: -// node1 dominates node2 -// and -// node1 can be typed at t2, -// node2 can be typed at t3, -// and t is a member of both t2 and t3. -// Note that node1 and node2 must share some parent node. -.decl TypedDominatesNT(node1: NodeID, node2: NodeID, t: TypeID) -TypedDominatesNT(node1, node2, t) :- Dom(node1, node2), Edge(id1, parent, node1), Edge(id2, parent, node2), - EdgeType(id1, t2), EdgeType(id2, t3), MemberTrans(t2, t), MemberTrans(t3, t). - - -// Transitive dominance with typing -// Given node1, node2, and type t, either -// a. node1 non-transitively dominates node2 at type t -// b. node2 is a callee of some node that is dominated by node1 at type t. -// (This case is a heuristic that should be obviated with precise dominance information.) -// c. t is a subtype of t2 and node1 dominates node2 for t2 -.decl TypedDominates(node1: NodeID, node2: NodeID, t: TypeID) -TypedDominates(node1, node2, t) :- TypedDominatesNT(node1, node2, t). -TypedDominates(node1, node3, t) :- TypedDominatesNT(node1, node2, t), TypedDominates(node2, node3, t). -TypedDominates(node1, node2, t) :- TypedCaller(parent, node1, t), TypedDominates(parent, node2, t). -TypedDominates(node1, node2, t) :- Member(t2, t), TypedDominates(node1, node2, t2). - - -// Typed dataflow model (non-transitive) -// Data flows from node1 to node2: -// a. if node1 directly calls node2 at type t -// b. if node1 directly dominates node2 at type t -.decl TypedDataflowNT(node1: NodeID, node2: NodeID, t: TypeID) -TypedDataflowNT(node1, node2, t) :- TypedCallerNT(node1, node2, t). -TypedDataflowNT(node1, node2, t) :- TypedDominatesNT(node1, node2, t). - - -// Typed dataflow model -// Data of type t flows from node1 to node2 -// a. if node1 transitively calls node2 at type t -// b. if node1 transitively dominates node2 at type t -// c. if there transitively is a dataflow at type t -// d. if there is a dataflow of type t2 and t is a member of t2 -.decl TypedDataflow(node1: NodeID, node2: NodeID, t: TypeID) -TypedDataflow(node1, node2, t) :- TypedCaller(node1, node2, t). -TypedDataflow(node1, node2, t) :- TypedDominates(node1, node2, t). -TypedDataflow(node1, node3, t) :- TypedDataflow(node1, node2, t), TypedDataflow(node2, node3, t). -TypedDataflow(node1, node2, t) :- MemberTrans(t2, t), TypedDataflow(node1, node2, t2). - - -// Typed dataflow via -// There exists a dataflow from node1 to node3 that passes through node2 -// that can be typed at t. -.decl TypedDataflowVia(node1: NodeID, node2: NodeID, node3: NodeID, t: TypeID) -TypedDataflowVia(node1, node2, node3, t) :- TypedDataflow(node1, node2, t), NotEqual(node1, node2), - TypedDataflow(node2, node3, t), NotEqual(node2, node3). - - -// Safe dataflow -// A dataflow from node1 to node2 (a checker) is considered safe if -// a. node1 is a checker -// b. node1 has a dataflow to node2 -// c. node2 dominates node1 for t -.decl SafeDataflow(node1: NodeID, node2: NodeID, t: TypeID) -SafeDataflow(node1, node2, t) :- ValidNode(node2), ValidType(t), NodeType(node1, 1). -SafeDataflow(node1, node2, t) :- TypedDataflow(node1, node2, t). -SafeDataflow(node1, node2, t) :- TypedDominates(node2, node1, t). - - -// Terminal node -// A node is a terminal node if it does not have any outgoing edges. -.decl TerminalNode(node: NodeID) -TerminalNode(node) :- ValidNode(node), !Edge(_, node, _). - - -// Typed dataflow not via -// There exists a dataflow of type t from node1 to node3 that does not pass through node2. -// -// a. There is a terminal non-transitive dataflow of type t from node1 to node3, and node3 is not -// dominated by node2 for t. -// b. There is a dataflow of type t from node1 to node3 that passes through some node4 != node2. -// Since there is no dataflow of type t from node2 to node4, node2 cannot be in that same flow. -// -// This is not guaranteed if an over-approximation of the call graph is used. -.decl TypedDataflowNotVia(node1: NodeID, node2: NodeID, node3: NodeID, t: TypeID) -TypedDataflowNotVia(node1, node2, node3, t) :- NotEqual(node1, node2), NotEqual(node2, node3), TerminalNode(node3), - TypedDataflowNT(node1, node3, t), !TypedDominates(node2, node3, t). -TypedDataflowNotVia(node1, node2, node3, t) :- NotEqual(node1, node2), NotEqual(node2, node3), - TypedDataflowVia(node1, node4, node3, t), NotEqual(node2, node4), - !SafeDataflow(node4, node2, t). - - -// Checked type -// All dataflow of type t pass through a checker -// There does not exist a dataflow of type t that does not pass through a checker -.decl CheckedType(t: TypeID) -CheckedType(t) :- ValidType(t), NodeType(entry, 0), NodeType(checker, 1), NodeType(exit, 2), - TypedDataflowVia(entry, checker, exit, t), - !TypedDataflowNotVia(entry, checker, exit, t). - - -// Not checked type -// There exists a dataflow of type t that does not pass through a checker -.decl NotCheckedType(t: TypeID) -NotCheckedType(t) :- ValidType(t), !CheckedType(t). - - -// Not checked type at -// There exists a dataflow of type t that does not pass through a checker, -// instead reaching some terminal node -.decl NotCheckedTypeAt(t: TypeID, node: NodeID) -NotCheckedTypeAt(t, node) :- ValidType(t), NodeType(entry, 0), NodeType(exit, 2), - !NodeType(node, 1), !Edge(_, node, _), - TypedDataflowVia(entry, node, exit, t). - - -.output CheckedType(io=file, headers=true, delimiter=",") -.output NotCheckedTypeAt(io=file, headers=true, delimiter=",") diff --git a/language/tools/mirai-dataflow-analysis/config/BoundsChecker_config.json b/language/tools/mirai-dataflow-analysis/config/BoundsChecker_config.json deleted file mode 100644 index 4a2cb98cb6..0000000000 --- a/language/tools/mirai-dataflow-analysis/config/BoundsChecker_config.json +++ /dev/null @@ -1,25 +0,0 @@ -{ - "reductions": [ - {"Slice": "verify_impl"}, - "Fold", - "Clean" - ], - "included_crates": ["check_bounds"], - "node_types": { - "entry": [ - "verify_impl" - ], - "checker": [ - "check_bounds_impl", - "check_code_unit_bounds_impl", - "check_type_parameter" - ], - "safe": [ - "get_locals", - "offset_out_of_bounds" - ], - "exit": [ - "verify_impl_exit" - ] - } -} diff --git a/language/tools/mirai-dataflow-analysis/config/CompiledModule_type_relations.json b/language/tools/mirai-dataflow-analysis/config/CompiledModule_type_relations.json deleted file mode 100644 index f737d8189e..0000000000 --- a/language/tools/mirai-dataflow-analysis/config/CompiledModule_type_relations.json +++ /dev/null @@ -1,314 +0,0 @@ -{ - "relations": [ - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::Signature]" - }, - { - "kind": "Member", - "type1": "file_format::Signature", - "type2": "file_format::SignatureToken" - }, - { - "kind": "Member", - "type1": "file_format::SignatureToken", - "type2": "file_format::StructHandleIndex" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::Constant]" - }, - { - "kind": "Member", - "type1": "file_format::Constant", - "type2": "file_format::SignatureToken" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::ModuleHandle]" - }, - { - "kind": "Member", - "type1": "file_format::ModuleHandle", - "type2": "file_format::AddressIdentifierIndex" - }, - { - "kind": "Member", - "type1": "file_format::ModuleHandle", - "type2": "file_format::IdentifierIndex" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "ModuleHandleIndex" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::StructHandle]" - }, - { - "kind": "Member", - "type1": "file_format::StructHandle", - "type2": "file_format::AddressIdentifierIndex" - }, - { - "kind": "Member", - "type1": "file_format::StructHandle", - "type2": "file_format::IdentifierIndex" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::FunctionHandle]" - }, - { - "kind": "Member", - "type1": "file_format::FunctionHandle", - "type2": "file_format::ModuleHandleIndex" - }, - { - "kind": "Member", - "type1": "file_format::FunctionHandle", - "type2": "file_format::IdentifierIndex" - }, - { - "kind": "Member", - "type1": "file_format::FunctionHandle", - "type2": "file_format::SignatureIndex" - }, - { - "kind": "Member", - "type1": "file_format::FunctionHandle", - "type2": "[file_format::AbilitySet]" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::FieldHandle]" - }, - { - "kind": "Member", - "type1": "file_format::FieldHandle", - "type2": "file_format::StructDefinitionIndex" - }, - { - "kind": "Member", - "type1": "file_format::StructDefinition", - "type2": "file_format::StructFieldInformation" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::StructDefInstantiation]" - }, - { - "kind": "Member", - "type1": "file_format::StructDefInstantiation", - "type2": "file_format::StructDefinitionIndex" - }, - { - "kind": "Member", - "type1": "file_format::StructDefInstantiation", - "type2": "file_format::SignatureIndex" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::FunctionInstantiation]" - }, - { - "kind": "Member", - "type1": "file_format::FunctionInstantiation", - "type2": "file_format::FunctionHandleIndex" - }, - { - "kind": "Member", - "type1": "file_format::FunctionInstantiation", - "type2": "file_format::SignatureIndex" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::FieldInstantiation]" - }, - { - "kind": "Member", - "type1": "file_format::FieldInstantiation", - "type2": "file_format::FieldHandleIndex" - }, - { - "kind": "Member", - "type1": "file_format::FieldInstantiation", - "type2": "file_format::SignatureIndex" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::StructDefinition]" - }, - { - "kind": "Member", - "type1": "file_format::StructDefinition", - "type2": "file_format::StructHandleIndex" - }, - { - "kind": "Member", - "type1": "file_format::StructDefinition", - "type2": "file_format::StructFieldInformation" - }, - { - "kind": "Member", - "type1": "file_format::StructFieldInformation", - "type2": "[file_format::FieldDefinition]" - }, - { - "kind": "Member", - "type1": "file_format::FieldDefinition", - "type2": "file_format::IdentifierIndex" - }, - { - "kind": "Member", - "type1": "file_format::FieldDefinition", - "type2": "file_format::TypeSignature" - }, - { - "kind": "Member", - "type1": "file_format::TypeSignature", - "type2": "file_format::SignatureToken" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::FunctionDefinition]" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "file_format::FunctionDefinition" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::FunctionDefinitionIndex]" - }, - { - "kind": "Member", - "type1": "file_format::FunctionDefinition", - "type2": "file_format::FunctionHandleIndex" - }, - { - "kind": "Member", - "type1": "file_format::FunctionDefinition", - "type2": "file_format::SignatureIndex" - }, - { - "kind": "Member", - "type1": "file_format::FunctionDefinition", - "type2": "[file_format::StructDefinitionIndex]" - }, - { - "kind": "Member", - "type1": "file_format::FunctionDefinition", - "type2": "[file_format::CodeUnit]" - }, - { - "kind": "Member", - "type1": "file_format::FunctionDefinition", - "type2": "file_format::CodeUnit" - }, - { - "kind": "Member", - "type1": "file_format::CodeUnit", - "type2": "file_format::ConstantPoolIndex" - }, - { - "kind": "Member", - "type1": "file_format::CodeUnit", - "type2": "file_format::StructDefInstantiationIndex" - }, - { - "kind": "Member", - "type1": "file_format::CodeUnit", - "type2": "file_format::FieldInstantiationIndex" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "file_format::FunctionInstantiationIndex" - }, - { - "kind": "Eq", - "type1": "move_binary_format::CompiledModule", - "type2": "check_bounds::BoundsChecker" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[move_core_types::identifier::Identifier]" - }, - { - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[move_core_types::account_address::AccountAddress]" - }, - { - "kind": "Eq", - "type1": "move_binary_format::file_format::Constant", - "type2": "file_format::Constant" - }, - { - "kind": "Eq", - "type1": "move_binary_format::file_format::Signature", - "type2": "file_format::Signature" - }, - { - "kind": "Eq", - "type1": "move_binary_format::file_format::ModuleHandle", - "type2": "file_format::ModuleHandle" - }, - { - "kind": "Eq", - "type1": "move_binary_format::file_format::FunctionHandle", - "type2": "file_format::FunctionHandle" - }, - { - "kind": "Eq", - "type1": "move_binary_format::file_format::FunctionInstantiation", - "type2": "file_format::FunctionInstantiation" - }, - { - "kind": "Eq", - "type1": "move_binary_format::file_format::FieldHandle", - "type2": "file_format::FieldHandle" - }, - { - "kind": "Eq", - "type1": "move_binary_format::file_format::FieldInstantiation", - "type2": "file_format::FieldInstantiation" - }, - { - "kind": "Eq", - "type1": "move_binary_format::file_format::FunctionDefinition", - "type2": "file_format::FunctionDefinition" - }, - { - "kind": "Eq", - "type1": "move_binary_format::file_format::StructHandle", - "type2": "file_format::StructHandle" - }, - { - "kind": "Eq", - "type1": "move_binary_format::file_format::StructDefinition", - "type2": "file_format::StructDefinition" - }, - { - "kind": "Eq", - "type1": "move_binary_format::CompiledModule", - "type2": "check_duplication::DuplicationChecker" - } - ] -} diff --git a/language/tools/mirai-dataflow-analysis/config/DuplicationChecker_config.json b/language/tools/mirai-dataflow-analysis/config/DuplicationChecker_config.json deleted file mode 100644 index 44740790f4..0000000000 --- a/language/tools/mirai-dataflow-analysis/config/DuplicationChecker_config.json +++ /dev/null @@ -1,25 +0,0 @@ -{ - "reductions": [ - {"Slice": "move_bytecode_verifier::check_duplication::{impl#0}::verify_module"}, - "Fold", - "Clean" - ], - "included_crates": ["check_duplication"], - "node_types": { - "entry": ["verify_module"], - "checker": ["first_duplicate_element"], - "safe": [ - "check_struct_handles::{closure#0}", - "check_function_handles::{closure#0}", - "check_function_defintions::{closure#0}", - "check_function_defintions::{closure#1}", - "check_function_defintions::{closure#2}", - "check_struct_definitions::{closure#0}", - "check_struct_definitions::{closure#1}", - "check_struct_definitions::{closure#2}", - "check_struct_definitions::{closure#3}", - "verify_script::{closure#0}" - ], - "exit": ["verify_module_impl_exit"] - } -} diff --git a/language/tools/mirai-dataflow-analysis/examples/BoundsChecker.md b/language/tools/mirai-dataflow-analysis/examples/BoundsChecker.md deleted file mode 100644 index dd9bf77aa6..0000000000 --- a/language/tools/mirai-dataflow-analysis/examples/BoundsChecker.md +++ /dev/null @@ -1,135 +0,0 @@ -# Bounds Checker Analysis - -## Property - -All module indexes fall within bounds of a corresponding pool. - -## Background - -The `CompiledModuleMut` has a set of pools, e.g. `module.field_handles` which contain structs that individually need to be checked. These structs are identified via indexes into their respective pools. - -## Analysis goal - -Check that every dataflow of `Index` type passes through one of the these three checking functions: - -1. `check_bounds_impl` -2. `check_code_unit_bounds_impl` -3. `check_type_parameter` - -Data types to Check: Data of `Index` type: -``` -ModuleHandleIndex, -StructHandleIndex, -FunctionHandleIndex, -FieldHandleIndex, -StructDefInstantiationIndex, -FunctionInstantiationIndex, -FieldInstantiationIndex, -IdentifierIndex, -AddressIdentifierIndex, -ConstantPoolIndex, -SignatureIndex, -StructDefinitionIndex, -FunctionDefinitionIndex -``` - -## Analysis definition - -1. Entry: `verify_impl` - - Justification: Both public entry points of the bounds checker, `verify_script` and `verify_module` subsequently call `verify_impl`. -2. Checkers: - 1. `check_bounds_impl` - 2. `check_code_unit_bounds_impl` - 3. `check_type_parameter` -3. Exit: Dummy function called at the end of `verify_impl`: - ```Rust - fn verify_impl_exit(&self) -> PartialVMResult<()> { - Ok(()) - } - ``` - - Justification: For the BoundsChecker, the entry point is the same as the exit (`verify_impl`), thus we need to distinguish the end of the function via a call to this dummy function. -4. Safe functions: - ``` - get_locals, - offset_out_of_bounds - ``` - - Justification: These functions are false positives of the analysis if not explicitly marked as safe. They are safe because they are utility functions that have dataflow within the context of the BoundsChecker. - -## Type relations - -The analysis uses input type relations that describe the structure of a compiled module with regards to the data-types-to-check, e.g., `ConstantPoolIndex, IdentifierIndex`, etc. For example, we provide a relation showing that the `CompiledModule` has a collection of `ModuleHandle`s that each have `IdentifierIndex`s: -``` -{ - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::ModuleHandle]" -}, -{ - "kind": "Member", - "type1": "file_format::ModuleHandle", - "type2": "file_format::IdentifierIndex" -}, -``` - -## Verification conditions for checkers - -1. For `check_bounds_impl(pool: &[T], idx: I)` - - Invariant: `idx >= pool.len() ==> Err` -2. For `check_code_unit_bounds_impl(pool: &[T], idx: I)` - - Invariant: `idx >= pool.len() ==> Err` -5. For `check_type_parameter(ty: &SignatureToken, type_param_count: usize)` - - Invariant: `exists ty == TypeParameter(idx) in ty . idx >= type_param_count ==> Err` - -## Required code modifications - -1. Add the exit dummy function. -2. Separate `verify_impl` loops into individual functions. This is already done as of Diem commit `5122a1d9994350d0c2de7acfe4b44c59e157d2fa`. Example: - - Before: - ```Rust - fn verify_impl(...) { - ... - for signature in self.view.signatures() { - self.check_signature(signature)? - } - ... - } - ``` - - After - ```Rust - fn verify_impl(...) { - ... - self.check_signatures(signature)?; - ... - } - - fn check_signatures(&self) -> PartialVMResult<()> { - for signature in self.view.signatures() { - self.check_signature(signature)? - } - Ok(()) - } - ``` - - - Justification: False positive occurs if this is not done ( - `NotCheckedType` with zero loop iterations): - - We cannot establish a dominance relationship between one of the functions in loops (e.g., `self.check_signature` and the exit. This is because the loop may execute zero times, in which case `self.check_signature` will not be called. - - Technically a true positive in the sense that there is a path to the exit where the dataflow is not checked, but actually a false positive because the loop only does not execute if there are no members of that dataflow to check in the first place. - -## Results - -All `Index` types are checked: -``` -ModuleHandleIndex, -StructHandleIndex, -FunctionHandleIndex, -FieldHandleIndex, -StructDefInstantiationIndex, -FunctionInstantiationIndex, -FieldInstantiationIndex, -IdentifierIndex, -AddressIdentifierIndex, -ConstantPoolIndex, -SignatureIndex, -StructDefinitionIndex, -FunctionDefinitionIndex -``` diff --git a/language/tools/mirai-dataflow-analysis/examples/DuplicationChecker.md b/language/tools/mirai-dataflow-analysis/examples/DuplicationChecker.md deleted file mode 100644 index cb09e7f5ac..0000000000 --- a/language/tools/mirai-dataflow-analysis/examples/DuplicationChecker.md +++ /dev/null @@ -1,110 +0,0 @@ -# Duplication Checker Analysis - -## Property - -No duplication of entries in any pool of a `CompiledModule` or `CompiledScript`. - -## Background - -The `CompiledModule` (and `CompiledScript`) have a set of pools, e.g. `module.field_handles` which contain structs. These pools need to be checked for duplicated elements. - -## Analysis goal - -Check that every dataflow of Pool type passes through the checking function: `first_duplicate_element`. Data types to Check: All of the module or script pools: -``` -module_handles: Vec -struct_handles: Vec -function_handles: Vec -field_handles: Vec -friend_decls: Vec -struct_def_instantiations: Vec -function_instantiations: Vec -field_instantiations: Vec -signatures: Vec -identifiers: Vec -address_identifiers: Vec -constant_pool: Vec -struct_defs: Vec -function_defs: Vec -``` -- Note that the `module_handles` and `friend_decls` share the same type so it is not possible to distinguish them in this analysis. - -## Analysis definition - -1. Entry points: - 1. `verify_module` - 2. `verify_script` -2. Checker: `first_duplicate_element` -3. Exit: Dummy function called at the end of `verify_module` and `verify_script`: - 1. `verify_module_impl_exit` - ```Rust - fn verify_module_impl_exit(_module: &'a CompiledModule) -> PartialVMResult<()> { - Ok(()) - } - ``` - 2. `verify_script_impl_exit` - ```Rust - fn verify_script_impl_exit(_module: &'a CompiledScript) -> PartialVMResult<()> { - Ok(()) - } - ``` - - Justification: For the DuplicationChecker, the entry points are the same as the exits, thus we need to distinguish the end of the function via a call to this dummy function. -4. Safe functions: - ``` - check_struct_handles::{closure#0} - check_function_handles::{closure#0} - check_function_defintions::{closure#0} - check_function_defintions::{closure#1} - check_function_defintions::{closure#2} - check_struct_definitions::{closure#0} - check_struct_definitions::{closure#1} - check_struct_definitions::{closure#2} - check_struct_definitions::{closure#3} - verify_script::{closure#0} - ``` - - Justification: As used in the DuplicationChecker, the above closures lead to two false positives for the analysis (causing both the `struct_defs` and `function_defs` to be identified as `NotCheckedType`). However, these checkers have no unsafe dataflows outside of the DuplicationChecker; they primarily show up in function application on iterators. - -## Type relations - -The analysis uses input type relations that describe the structure of a compiled module with regards to the data-types-to-check, e.g., `Vec, Vec` etc. For example, we provide a relation showing that the `CompiledModule` has a collection of signatures: -``` -{ - "kind": "Member", - "type1": "move_binary_format::CompiledModule", - "type2": "[file_format::Signature]" -} -``` - -## Verification conditions for checkers - -1. For `first_duplicate_element(iter) -> res: Option`: - ``` - res is None => - forall idx1 in iter . - forall idx2 in iter . - idx1 != idx2 => iter[idx1] != iter[idx2] - ``` - -## Required code modifications - -1. Add the dummy exit functions. - -## Results - -All pools are checked: -``` -module_handles: Vec -struct_handles: Vec -function_handles: Vec -field_handles: Vec -friend_decls: Vec -struct_def_instantiations: Vec -function_instantiations: Vec -field_instantiations: Vec -signatures: Vec -identifiers: Vec -address_identifiers: Vec -constant_pool: Vec -struct_defs: Vec -function_defs: Vec -``` diff --git a/language/tools/mirai-dataflow-analysis/examples/examples.md b/language/tools/mirai-dataflow-analysis/examples/examples.md deleted file mode 100644 index 09dbb6d676..0000000000 --- a/language/tools/mirai-dataflow-analysis/examples/examples.md +++ /dev/null @@ -1,62 +0,0 @@ -# Overview - -We present two example analyses using `mirai-dataflow`: -1. An analysis on the move-binary-format crate's [BoundsChecker](./BoundsChecker.md). -2. An analysis on the bytecode-verifier crate's [DuplicationChecker](./DuplicationChecker.md). - -## Environment - -All analysis results were captured using the following software versions: -- The Diem commit that this file was published with (after `92a19a426bae04199f2ca0845dfb19fdee4740a6`). -- The commit of MIRAI in use is `49c8add3706d49f82d96f3ace2c01c738ea04dc2`. -- The version of Soufflé in use is `2.1-123-g1f664173b`. -- The version of Differential Datalog in use is `v0.42.0 (f2824fec7b86c84486ec34b8880bd590678c0765)`. - -Please note that MIRAI's [is_excluded](https://github.com/facebookexperimental/MIRAI/blob/49c8add3706d49f82d96f3ace2c01c738ea04dc2/checker/src/callbacks.rs#L145) function will have to be modified _before_ installing MIRAI to not exclude the `move-binary-format` and `bytecode-verifier` crates: -1. For `move-binary-format` comment out [this line](https://github.com/facebookexperimental/MIRAI/blob/49c8add3706d49f82d96f3ace2c01c738ea04dc2/checker/src/callbacks.rs#L215). -2. For the `bytecode-verifier` comment out [this line](https://github.com/facebookexperimental/MIRAI/blob/49c8add3706d49f82d96f3ace2c01c738ea04dc2/checker/src/callbacks.rs#L149). - -## Example Structure - -The example analyses have the following structure: -1. Property -2. Background -3. Analysis goal -4. Analysis definition -5. Type relations -6. Verification conditions for checkers -7. Required code modifications -8. Results - -The **Property** section describes the property we want the analysis to check for. - -The **Background** section explains relevant background for the property. - -The **Analysis goal** section translates the property into a checked / unchecked dataflow problem statement, and states the data types that should be checked. - -The **Analysis definition** section identifies the entry point(s), checking function(s), and exit point(s). These correspond exactly to the `"node_type"` configuration of the analysis. - -The **Type relations** section describes the necessary input type relations needed to describe the data types that will be checked. - -The **Verification conditions for checkers** section states invariants that the checking function(s) must uphold in order for the analysis to imply satisfaction of the property. - -The **Required code modifications** section describes modifications that have (or had) to be performed to get the analysis to function correctly. - -Finally, the **Results** section describes the results of the analysis; e.g., which of the data-types-to-check are identified as being checked. - -## Running an example analysis - -The results presented in one of the analysis documents can be replicated by following these steps: -1. Ensure that installed versions of software match those listed under the "Environment" heading of _this_ document. -2. Ensure that a configuration file is present for the analysis and matches what is listed in the "Analysis definition" section of that analysis document. For the above examples, three configuration files should be present in the `config` folder: - ``` - BoundsChecker_config.json - DuplicationChecker_config.json - CompiledModule_type_relations.json - ``` -3. Make code modifications as described in the "Required code modifications" section of the analysis document. -4. Run the analysis using the provided configuration. For example, to run the BoundsChecker analysis: - ``` - cargo run -- ../../move-binary-format config/BoundsChecker_config.json --type-relations-path config/CompiledModule_type_relations.json - ``` -5. Review the results in `output/decoded.json` to ensure that they match those presented in the analysis document. diff --git a/language/tools/mirai-dataflow-analysis/rust-toolchain b/language/tools/mirai-dataflow-analysis/rust-toolchain deleted file mode 100644 index a03d26c046..0000000000 --- a/language/tools/mirai-dataflow-analysis/rust-toolchain +++ /dev/null @@ -1 +0,0 @@ -nightly-2021-09-17 diff --git a/language/tools/mirai-dataflow-analysis/src/configuration.rs b/language/tools/mirai-dataflow-analysis/src/configuration.rs deleted file mode 100644 index 6f365b0072..0000000000 --- a/language/tools/mirai-dataflow-analysis/src/configuration.rs +++ /dev/null @@ -1,141 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// SPDX-License-Identifier: Apache-2.0 - -use std::{ - fs, - path::{Path, PathBuf}, -}; - -use serde::{Deserialize, Serialize}; - -use crate::{datalog::DatalogBackend, util::make_absolute}; - -/// Specifies reduction operations that may be performed -/// on a call graph. Supported operations are: -#[derive(Debug, Clone, Serialize, Deserialize)] -pub enum CallGraphReduction { - /// Only include nodes reachable from the given node. - /// See `CallGraph::filter_reachable`. - Slice(Box), - /// Remove nodes in the graph that belong to crates other than - /// `CallGraphConfig.included_crates`. The outgoing edges of these - /// removed node are connected to the node's parents. - /// See `CallGraph::fold_excluded`. - Fold, - /// Remove duplicated edges (only considers edge endpoints). - /// See `CallGraph::deduplicate_edges`. - Deduplicate, - /// Remove nodes that have no incoming or outgoing edges. - /// See `CallGraph::filter_no_edges`. - Clean, -} - -/// Configuration options for Datalog output -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct DatalogConfig { - /// Specifies location for graph to be output as Datalog input relations. - pub ddlog_output_path: PathBuf, - /// Specifies location for mapping from type identifiers to type strings. - pub type_map_output_path: PathBuf, - /// Optionally specifies the location for manually defined type relations - /// to be imported. - pub type_relations_path: Option, - /// Datalog output backend to use. - /// Currently, Differential Datalog and Soufflé are supported. - pub datalog_backend: DatalogBackend, - /// Analysis raw output path - pub analysis_raw_output_path: PathBuf, - /// Analysis decoded output path - pub analysis_decoded_output_path: PathBuf, -} - -/// Configuration for node type input relations -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct NodeTypeConfig { - pub entry: Vec>, - pub checker: Vec>, - pub safe: Vec>, - pub exit: Vec>, -} - -/// Configuration options for call graph generation. -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct CallGraphConfig { - /// Optionally specifies location for graph to be output in dot format - /// (for Graphviz). - pub dot_output_path: Option, - /// A list of call graph reductions to apply sequentially - /// to the call graph. - pub reductions: Vec, - /// A list of crates to include in the call graph. - /// Nodes belonging to crates not in this list will be removed. - pub included_crates: Vec>, - /// Datalog output configuration - pub datalog_config: Option, - /// Node type annotations - pub node_types: NodeTypeConfig, -} - -/// Generate a complete CallGraphConfig from a combination of the partial config -/// file and command line options -pub fn generate_config( - config_path: &Path, - call_graph_only: bool, - datalog_backend: Option, - relations_path: Option, -) -> Result<(CallGraphConfig, PathBuf), String> { - let output_path = Path::new("./output"); - if !output_path.exists() { - fs::create_dir(output_path) - .map_err(|msg| format!("Failed to create output directory: {}", msg))?; - } - let mut config: CallGraphConfig = fs::read_to_string(config_path) - .map_err(|msg| format!("Failed to read config file: {}", msg)) - .and_then(|config_str| { - serde_json::from_str::(&config_str) - .map_err(|msg| format!("Failed to parse config: {}", msg)) - })?; - let dot_output_path = make_absolute(&output_path.join("graph.dot")) - .map_err(|msg| format!("Failed to construct dot_output_path: {}", msg))?; - config.dot_output_path = Some(dot_output_path); - if !call_graph_only { - let datalog_backend = match datalog_backend { - Some(backend) => backend, - None => DatalogBackend::Souffle, - }; - let ddlog_output_path = make_absolute(&match datalog_backend { - DatalogBackend::DifferentialDatalog => output_path.join("graph.dat"), - DatalogBackend::Souffle => output_path.to_path_buf(), - }) - .map_err(|msg| format!("Failed to construct ddlog_output_path: {}", msg))?; - let type_map_output_path = make_absolute(&output_path.join("graph_types.json")) - .map_err(|msg| format!("Failed to construct type_map_output_path: {}", msg))?; - let type_relations_path = match relations_path { - Some(path) => { - let canonical_path = make_absolute(&path) - .map_err(|msg| format!("Failed to construct type_relations_path: {}", msg))?; - Some(canonical_path) - } - None => None, - }; - let analysis_raw_output_path = match datalog_backend { - DatalogBackend::DifferentialDatalog => output_path.join("analysis.out"), - DatalogBackend::Souffle => output_path.to_path_buf(), - }; - let analysis_decoded_output_path = output_path.join("decoded.json"); - config.datalog_config = Some(DatalogConfig { - ddlog_output_path, - type_map_output_path, - type_relations_path, - datalog_backend, - analysis_raw_output_path, - analysis_decoded_output_path, - }); - } - let new_config_path = output_path.join("config.json"); - let config_str = serde_json::to_string(&config) - .map_err(|msg| format!("Failed to serialize config: {}", msg))?; - fs::write(new_config_path.clone(), config_str) - .map_err(|msg| format!("Failed to write config: {}", msg))?; - Ok((config, new_config_path)) -} diff --git a/language/tools/mirai-dataflow-analysis/src/datalog.rs b/language/tools/mirai-dataflow-analysis/src/datalog.rs deleted file mode 100644 index ff79b694a4..0000000000 --- a/language/tools/mirai-dataflow-analysis/src/datalog.rs +++ /dev/null @@ -1,121 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// SPDX-License-Identifier: Apache-2.0 - -use std::str::FromStr; - -use serde::{Deserialize, Serialize}; - -use crate::util::{NodeMap, TypeMap}; - -/// Annotations for NodeType input relations -#[derive(Debug, Clone)] -pub enum NodeType { - Entry(u32), - Checker(u32), - Safe(u32), - Exit(u32), -} - -pub type DatalogRelations = Vec; - -/// A Datalog relation operand is an index of a -/// call graph node or a call graph edge type -#[derive(Debug, Serialize)] -pub enum DatalogRelationOperandType { - Node, - Type, -} - -/// A Datalog relation operand has a name, -/// index, type, and string representation -#[derive(Debug, Serialize)] -pub struct DatalogRelationOperand { - name: String, - index: u32, - string: Option, - op_type: DatalogRelationOperandType, -} - -impl DatalogRelationOperand { - pub fn new( - name: String, - index: u32, - string: Option, - op_type: DatalogRelationOperandType, - ) -> DatalogRelationOperand { - DatalogRelationOperand { - name, - index, - string, - op_type, - } - } -} - -/// A Datalog relation has a name and a list -/// of operands -#[derive(Debug, Serialize)] -pub struct DatalogRelation { - name: String, - operands: Vec, -} - -impl DatalogRelation { - pub fn new(name: String, operands: Vec) -> DatalogRelation { - DatalogRelation { name, operands } - } -} - -/// The supported Datalog backend are -/// Differential Datalog and Soufflé -#[derive(Debug, Clone, Serialize, Deserialize)] -pub enum DatalogBackend { - DifferentialDatalog, - Souffle, -} - -impl FromStr for DatalogBackend { - type Err = String; - fn from_str(s: &str) -> Result { - match s { - "DifferentialDatalog" => Ok(DatalogBackend::DifferentialDatalog), - "Souffle" => Ok(DatalogBackend::Souffle), - _ => Err(format!("Failed to read Datalog backend: {}", s)), - } - } -} - -/// Determine the operand type of a Datalog relation from its name -pub fn determine_op_type(op_name: &str) -> Result { - if op_name.contains("node") || op_name.contains("checker") { - Ok(DatalogRelationOperandType::Node) - } else if op_name == "t" { - Ok(DatalogRelationOperandType::Type) - } else { - Err(format!( - "Failed to determine operand type for node: {}", - op_name - )) - } -} - -/// Use the node and type mappings to decode indexes in relation -/// operands to strings -pub fn decode_analysis_output( - relations: &mut DatalogRelations, - type_map: &TypeMap, - node_map: &NodeMap, -) { - for relation in relations.iter_mut() { - for operand in relation.operands.iter_mut() { - match operand.op_type { - DatalogRelationOperandType::Node => { - operand.string = node_map.get(&operand.index).map(|s| s.to_owned()); - } - DatalogRelationOperandType::Type => { - operand.string = type_map.get(&operand.index).map(|s| s.to_owned()); - } - } - } - } -} diff --git a/language/tools/mirai-dataflow-analysis/src/ddlog_output.rs b/language/tools/mirai-dataflow-analysis/src/ddlog_output.rs deleted file mode 100644 index 780751fa08..0000000000 --- a/language/tools/mirai-dataflow-analysis/src/ddlog_output.rs +++ /dev/null @@ -1,131 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// SPDX-License-Identifier: Apache-2.0 - -use regex::Regex; -use std::{ - fs, - io::Write, - path::Path, - process::{Command, Stdio}, -}; - -use crate::{ - datalog::{ - determine_op_type, DatalogRelation, DatalogRelationOperand, DatalogRelations, NodeType, - }, - util::get_child_output, -}; - -// This path is automatically generated as part of setting up the -// Differential Datalog analysis -const DDLOG_CLI_PATH: &str = "analyses/ddlog_ddlog/target/release/ddlog_cli"; - -// Run the Differential Datalog analysis on the test file and -// capture output -pub fn run_ddlog_analysis( - ddlog_output_path: &Path, - analysis_output_path: &Path, -) -> Result<(), String> { - let file_data = fs::read_to_string(ddlog_output_path) - .map_err(|msg| format!("Failed to read dat file: {}", msg))?; - let mut child = Command::new(DDLOG_CLI_PATH) - .stdin(Stdio::piped()) - .stdout(Stdio::piped()) - .spawn() - .map_err(|msg| format!("Failed to run analysis: {}", msg))?; - child - .stdin - .take() - .unwrap() - .write(file_data.as_bytes()) - .map_err(|msg| format!("Failed to run analysis: {}", msg))?; - let analysis_output = child - .wait_with_output() - .map(|output| get_child_output(&output)) - .map_err(|msg| format!("Failed to run analysis: {}", msg))?; - fs::write(analysis_output_path, analysis_output) - .map(|_| ()) - .map_err(|msg| format!("Failed to record analysis results: {}", msg)) -} - -/// Parse a Differential Datalog Datalog output relation into the -/// format of a DatalogRelation -fn parse_ddlog_relation(line: &str) -> Result { - let relation_name = (match Regex::new(r#"([A-Z])\w+"#).unwrap().captures(line) { - Some(captures) => Ok(captures[0].to_owned()), - None => Err("Failed to find relation name"), - })?; - let operand_string = (match Regex::new(r#"\{(.*)\}"#).unwrap().captures(line) { - Some(captures) => Ok(captures[1].to_owned()), - None => Err("Failed to find relation operands"), - })?; - let mut operands = Vec::::new(); - let operand_strs = operand_string.split(',').collect::>(); - for operand_str in operand_strs.iter() { - if let Some(captures) = Regex::new(r#"\.(\w+) = (\d+)"#) - .unwrap() - .captures(operand_str) - { - assert!(captures.len() == 3); - let op_name = captures[1].to_owned(); - let op_type = determine_op_type(&op_name)?; - operands.push(DatalogRelationOperand::new( - op_name, - captures[2].to_owned().parse::().unwrap(), - None, - op_type, - )); - } - } - Ok(DatalogRelation::new(relation_name, operands)) -} - -/// Parse all of the Differential datalog analysis output relations -pub fn parse_ddlog_output(analysis_output_path: &Path) -> Result { - fs::read_to_string(analysis_output_path) - .map_err(|msg| format!("Failed to read analysis output: {}", msg)) - .and_then(|out| { - let lines = out.split('\n').collect::>(); - let mut relations = Vec::::new(); - for line in lines.iter().filter(|line| line.contains('{')) { - match parse_ddlog_relation(line) { - Ok(relation) => { - relations.push(relation); - } - Err(msg) => { - return Err(format!( - "Failed to parse ddlog relation: {}\nbecause: {}", - line, msg - )); - } - } - } - Ok(relations) - }) -} - -/// Output node type annotations as datalog input relations -pub fn write_ddlog_node_types( - node_types: &[NodeType], - ddlog_relations_path: &Path, -) -> Result<(), String> { - let mut out_strs = Vec::::new(); - for node_type in node_types.iter() { - out_strs.push(match node_type { - NodeType::Entry(id) => format!("insert NodeType({},Entry)", id), - NodeType::Checker(id) => format!("insert NodeType({},Checker)", id), - NodeType::Safe(id) => format!("insert NodeType({},Checker)", id), - NodeType::Exit(id) => format!("insert NodeType({},Exit)", id), - }); - } - let mut out_str = out_strs.join(";\n"); - out_str.push_str(";\ncommit;\ndump CheckedType;\ndump NotCheckedType;"); - let ddlog_relations_str = fs::read_to_string(ddlog_relations_path) - .map_err(|msg| format!("Failed to read ddlog relations: {}", msg))?; - fs::write( - ddlog_relations_path, - ddlog_relations_str.replace("commit;", &out_str), - ) - .map(|_| ()) - .map_err(|msg| format!("Failed to write node type relations: {}", msg)) -} diff --git a/language/tools/mirai-dataflow-analysis/src/lib.rs b/language/tools/mirai-dataflow-analysis/src/lib.rs deleted file mode 100644 index 1cc54db129..0000000000 --- a/language/tools/mirai-dataflow-analysis/src/lib.rs +++ /dev/null @@ -1,2 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// SPDX-License-Identifier: Apache-2.0 diff --git a/language/tools/mirai-dataflow-analysis/src/main.rs b/language/tools/mirai-dataflow-analysis/src/main.rs deleted file mode 100644 index 85a67d334f..0000000000 --- a/language/tools/mirai-dataflow-analysis/src/main.rs +++ /dev/null @@ -1,322 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// SPDX-License-Identifier: Apache-2.0 - -use clap::Parser; -use mirai_annotations::unrecoverable; -use regex::Regex; -use std::{ - collections::HashMap, - fs, - path::{Path, PathBuf}, - process::Command, -}; - -mod configuration; -mod datalog; -mod ddlog_output; -mod souffle_output; -mod util; - -use configuration::{generate_config, NodeTypeConfig}; -use datalog::{decode_analysis_output, DatalogBackend, DatalogRelations, NodeType}; -use ddlog_output::{parse_ddlog_output, run_ddlog_analysis, write_ddlog_node_types}; -use souffle_output::{parse_souffle_output, run_souffle_analysis, write_souffle_node_types}; -use util::{get_child_output, NodeMap, TypeMap}; - -// Path to the current Rust nightly toolchain version -// that MIRAI is using -const RUST_TOOLCHAIN_PATH: &str = "./rust-toolchain"; - -// Run the Datalog analysis on the test file and -// capture output -fn run_mirai(config_path: &Path, crate_path: &Path, no_rebuild: bool) -> Result<(), String> { - if !no_rebuild { - // rustup override set toolchain - println!( - "Setting nightly toolchain version for {}", - crate_path.display() - ); - let nightly_str = fs::read_to_string(Path::new(RUST_TOOLCHAIN_PATH)) - .map_err(|msg| format!("Failed to toolchain nightly version: {}", msg)) - .map(|nightly_str| nightly_str.replace('\n', ""))?; - let out2 = Command::new("rustup") - .current_dir(&crate_path) - .arg("override") - .arg("set") - .arg(nightly_str) - .output() - .map_err(|msg| format!("Failed to set nightly: {}", msg))?; - println!("Result: {}", get_child_output(&out2)); - // 'RUSTFLAGS="-Z always_encode_mir" cargo build' - println!("Executing MIR cargo build on {}", crate_path.display()); - let out4 = Command::new("cargo") - .current_dir(&crate_path) - .env("RUSTFLAGS", "-Z always_encode_mir") - .arg("build") - .output() - .map_err(|msg| format!("Failed to build crate with MIR: {}", msg))?; - println!("Result: {}", get_child_output(&out4)); - } - // touch src/lib.rs - println!("Executing touch src/lib.rs {}", crate_path.display()); - let out5 = Command::new("touch") - .current_dir(&crate_path) - .arg("src/lib.rs") - .output() - .map_err(|msg| format!("Failed to execute touch: {}", msg))?; - println!("Result: {}", get_child_output(&out5)); - /* - RUSTFLAGS="-Z always_encode_mir" - RUSTC_WRAPPER=mirai - MIRAI_FLAGS="--call_graph_config=$CGG_PATH" - MIRAI_LOG=info - cargo build - */ - println!("Executing MIRAI on {}", crate_path.display()); - let out6 = Command::new("cargo") - .current_dir(&crate_path) - .env("RUSTFLAGS", "-Z always_encode_mir") - .env("RUSTC_WRAPPER", "mirai") - .env( - "MIRAI_FLAGS", - format!("--call_graph_config={}", config_path.to_str().unwrap()), - ) - .env("MIRAI_LOG", "info") - .arg("build") - .output() - .map(|output| get_child_output(&output)) - .map_err(|msg| format!("Failed to execute MIRAI: {}", msg))?; - println!("Result: {}", out6); - Ok(()) -} - -/// Read in a mapping from type indexes to type strings -fn parse_type_map(type_map_path: &Path) -> Result { - fs::read_to_string(type_map_path) - .map_err(|msg| format!("Failed to parse type map: {}", msg)) - .and_then(|out| { - serde_json::from_str::>(&out) - .map_err(|msg| format!("Failed to parse type map: {}", msg)) - }) -} - -/// Generate a mapping from node indexes to node names -fn parse_dot_graph(graph_path: &Path) -> Result { - fs::read_to_string(graph_path) - .map_err(|msg| format!("Failed to parse graph: {}", msg)) - .map(|out| { - let mut node_map = HashMap::::new(); - let lines = out.split('\n').collect::>(); - for line in lines.iter() { - if line.contains("label = ") { - if let Some(captures) = - Regex::new(r#"(\d+) \[.*"(.+)\\"#).unwrap().captures(line) - { - assert!(captures.len() == 3); - let node_id = captures[1].to_owned().parse::().unwrap(); - let node_name = captures[2].to_owned(); - assert_eq!(node_map.insert(node_id, node_name), None); - } - } - } - node_map - }) -} - -/// Process raw analysis output and write it to a file -fn process_datalog_output( - relations: &mut DatalogRelations, - node_map: &NodeMap, - type_map_path: &Path, - decoded_path: &Path, -) -> Result<(), String> { - let type_map = parse_type_map(type_map_path)?; - decode_analysis_output(relations, &type_map, node_map); - let relations_output = serde_json::to_string(&relations) - .map_err(|msg| format!("Failed to serialize relations: {}", msg))?; - fs::write(decoded_path, relations_output) - .map(|_| ()) - .map_err(|msg| format!("Failed to write relations to file: {}", msg)) -} - -/// Parse a node name to retrieve its suffix -fn parse_node_name(name: &str) -> String { - let name1 = name.replace("\"", ""); - let name_parts = name1.split("::").collect::>(); - let len = name_parts.len(); - assert!(len >= 2); - if name_parts[len - 1].contains("closure") { - format!("{}::{}", name_parts[len - 2], name_parts[len - 1]) - } else { - name_parts[len - 1].to_owned() - } -} - -/// Find the node id for a given node name -fn get_id_for_node(node_map: &NodeMap, name: &str) -> Result { - for (id, node_name) in node_map.iter() { - if parse_node_name(node_name) == name { - return Ok(*id); - } - } - Err(format!("Failed to find node {} in node map", &name)) -} - -/// Derive node type annotations from the node type configuration -pub fn parse_node_types( - node_map: &NodeMap, - raw_node_types: &NodeTypeConfig, -) -> Result, String> { - let mut node_types = Vec::::new(); - for node_name in raw_node_types.entry.iter() { - let node_id = get_id_for_node(node_map, node_name.as_ref())?; - node_types.push(NodeType::Entry(node_id)); - } - for node_name in raw_node_types.checker.iter() { - let node_id = get_id_for_node(node_map, node_name.as_ref())?; - node_types.push(NodeType::Checker(node_id)); - } - for node_name in raw_node_types.safe.iter() { - let node_id = get_id_for_node(node_map, node_name.as_ref())?; - node_types.push(NodeType::Safe(node_id)); - } - for node_name in raw_node_types.exit.iter() { - let node_id = get_id_for_node(node_map, node_name.as_ref())?; - node_types.push(NodeType::Exit(node_id)); - } - Ok(node_types) -} - -#[derive(Debug, Parser)] -#[clap( - name = "mirai-dataflow", - about = "Rust dataflow analyzer built on MIRAI." -)] -struct Opt { - /// Path to the crate to analyze - #[clap(parse(from_os_str))] - crate_path: PathBuf, - - /// Path to configuration file - #[clap(parse(from_os_str))] - config_path: PathBuf, - - /// Only produce a call graph (no analysis) - #[clap(long)] - call_graph_only: bool, - - /// Datalog backend to use (DifferentialDatalog | Souffle) - #[clap(short, long)] - datalog_backend: Option, - - /// Path to input type relations - #[clap(short, long, parse(from_os_str))] - type_relations_path: Option, - - /// Do not rebuild the crate before analysis - #[clap(short, long)] - no_rebuild: bool, - - /// Rerun the Datalog analysis without running MIRAI - #[clap(short, long)] - reanalyze: bool, -} - -fn main() { - // Process command line arguments - let opt = Opt::parse(); - // Canonicalize the crate path - let crate_path = match fs::canonicalize(opt.crate_path) { - Ok(crate_path) => crate_path, - Err(msg) => unrecoverable!("Failed to find crate to analyze: {}", msg), - }; - // Generate the call graph config - let (config, new_config_path) = match generate_config( - &opt.config_path, - opt.call_graph_only, - opt.datalog_backend, - opt.type_relations_path, - ) { - Ok(config) => config, - Err(msg) => unrecoverable!("Failed to generate analysis configuration: {}", msg), - }; - // Run MIRAI over the crate, producing call graph output - let config_path = match fs::canonicalize(new_config_path) { - Ok(crate_path) => crate_path, - Err(msg) => unrecoverable!("Failed to find call graph config: {}", msg), - }; - if !opt.reanalyze { - println!("Running MIRAI..."); - match run_mirai(&config_path, &crate_path, opt.no_rebuild) { - Ok(_) => {} - Err(msg) => unrecoverable!("{}", msg), - } - println!("Done"); - } - // If configured, analyze the call graph output with our - // Datalog analysis - if let Some(datalog_config) = config.datalog_config { - println!("Running Datalog analysis..."); - // Generate Datalog input relations for node types - assert!(config.dot_output_path.is_some()); - let node_map = match parse_dot_graph(&config.dot_output_path.unwrap()) { - Ok(node_map) => node_map, - Err(msg) => unrecoverable!("{}", msg), - }; - let node_types = match parse_node_types(&node_map, &config.node_types) { - Ok(node_types) => node_types, - Err(msg) => unrecoverable!("{}", msg), - }; - let node_type_result = match datalog_config.datalog_backend { - DatalogBackend::DifferentialDatalog => { - write_ddlog_node_types(&node_types, &datalog_config.ddlog_output_path) - } - DatalogBackend::Souffle => { - write_souffle_node_types(&node_types, &datalog_config.analysis_raw_output_path) - } - }; - match node_type_result { - Ok(_) => {} - Err(msg) => unrecoverable!("{}", msg), - } - let analysis_result = match datalog_config.datalog_backend { - DatalogBackend::DifferentialDatalog => run_ddlog_analysis( - &datalog_config.ddlog_output_path, - &datalog_config.analysis_raw_output_path, - ), - DatalogBackend::Souffle => { - run_souffle_analysis(&datalog_config.analysis_raw_output_path) - } - }; - match analysis_result { - Ok(_) => {} - Err(msg) => unrecoverable!("{}", msg), - } - println!("Done"); - // Process the raw analysis output into a decoded form - println!("Processing output..."); - let relations_result = match datalog_config.datalog_backend { - DatalogBackend::DifferentialDatalog => { - parse_ddlog_output(&datalog_config.analysis_raw_output_path) - } - DatalogBackend::Souffle => { - parse_souffle_output(&datalog_config.analysis_raw_output_path) - } - }; - let mut relations = match relations_result { - Ok(relations) => relations, - Err(msg) => unrecoverable!("{}", msg), - }; - let process_result = process_datalog_output( - &mut relations, - &node_map, - &datalog_config.type_map_output_path, - &datalog_config.analysis_decoded_output_path, - ); - match process_result { - Ok(_) => {} - Err(msg) => unrecoverable!("{}", msg), - } - println!("Done"); - } -} diff --git a/language/tools/mirai-dataflow-analysis/src/souffle_output.rs b/language/tools/mirai-dataflow-analysis/src/souffle_output.rs deleted file mode 100644 index ee86927248..0000000000 --- a/language/tools/mirai-dataflow-analysis/src/souffle_output.rs +++ /dev/null @@ -1,98 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// SPDX-License-Identifier: Apache-2.0 - -use std::{ - fs, - path::{Path, PathBuf}, - process::Command, -}; - -use crate::{ - datalog::{ - determine_op_type, DatalogRelation, DatalogRelationOperand, DatalogRelations, NodeType, - }, - util::make_absolute, -}; - -// Path to the Soufflé analysis file -const SOUFFLE_ANALYSIS_PATH: &str = "analyses/souffle.dl"; - -// Run the Soufflé Datalog analysis on the test file -pub fn run_souffle_analysis(analysis_output_path: &Path) -> Result<(), String> { - let souffle_dl_path = make_absolute(Path::new(SOUFFLE_ANALYSIS_PATH))?; - Command::new("souffle") - .current_dir(analysis_output_path) - .arg(souffle_dl_path.as_os_str()) - .output() - .map(|_| ()) - .map_err(|msg| format!("Failed to run analysis: {}", msg)) -} - -/// Parse a Soufflé Datalog Datalog output relation into the -/// format of a DatalogRelation -fn parse_souffle_relations(output_csv: &Path) -> Result { - assert!(output_csv.file_stem().is_some()); - let relation_name = output_csv.file_stem().unwrap(); - let csv_str = fs::read_to_string(output_csv) - .map_err(|msg| format!("Failed to read output CSV: {}", msg))?; - let mut rdr = csv::Reader::from_reader(csv_str.as_bytes()); - let headers: csv::StringRecord; - { - headers = rdr.headers().unwrap().to_owned(); - } - let mut relations = DatalogRelations::new(); - for result in rdr.records() { - let record = result.unwrap(); - let mut operands = Vec::::new(); - for (i, field) in record.iter().enumerate() { - let op_name = headers.get(i).unwrap().to_owned(); - let op_type = determine_op_type(&op_name)?; - let operand = - DatalogRelationOperand::new(op_name, field.parse::().unwrap(), None, op_type); - operands.push(operand); - } - let relation = DatalogRelation::new(relation_name.to_str().unwrap().to_owned(), operands); - relations.push(relation); - } - Ok(relations) -} - -/// Parse all of the Soufflé datalog analysis output relations -pub fn parse_souffle_output(output_path: &Path) -> Result { - let mut output_relation_paths: Vec = Vec::new(); - assert!(output_path.is_dir()); - for file in output_path.read_dir().unwrap() { - let _ = file.map(|file_elem| { - let path = file_elem.path(); - if let Some(extension) = path.extension() { - if extension == "csv" { - output_relation_paths.push(path); - } - } - }); - } - let mut relations = DatalogRelations::new(); - for path in output_relation_paths { - let relations_subset = parse_souffle_relations(&path).map_err(|msg| msg)?; - relations.extend(relations_subset); - } - Ok(relations) -} - -/// Output node type annotations as datalog input relations -pub fn write_souffle_node_types(node_types: &[NodeType], output_path: &Path) -> Result<(), String> { - let mut out_strs = Vec::::new(); - for node_type in node_types.iter() { - out_strs.push(match node_type { - NodeType::Entry(id) => format!("{},0", id), - NodeType::Checker(id) => format!("{},1", id), - NodeType::Safe(id) => format!("{},1", id), - NodeType::Exit(id) => format!("{},2", id), - }); - } - out_strs.sort_unstable(); - let out_str = out_strs.join("\n"); - fs::write(output_path.join("NodeType.facts"), out_str) - .map(|_| ()) - .map_err(|msg| format!("Failed to write node types: {}", msg)) -} diff --git a/language/tools/mirai-dataflow-analysis/src/util.rs b/language/tools/mirai-dataflow-analysis/src/util.rs deleted file mode 100644 index 5978ea2425..0000000000 --- a/language/tools/mirai-dataflow-analysis/src/util.rs +++ /dev/null @@ -1,24 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// SPDX-License-Identifier: Apache-2.0 - -use std::{ - collections::HashMap, - path::{Path, PathBuf}, - process::Output, -}; - -pub type TypeMap = HashMap; -pub type NodeMap = HashMap; - -/// Combine stdout and stderr of a child process -pub fn get_child_output(out: &Output) -> String { - (String::from_utf8_lossy(&out.stdout) + String::from_utf8_lossy(&out.stderr)).to_string() -} - -/// Create an absolute path from a path that is relative to the current directory -pub fn make_absolute(relative_path: &Path) -> Result { - let mut absolute_path = - std::env::current_dir().map_err(|msg| format!("Failed to get current path: {}", msg))?; - absolute_path.push(relative_path); - Ok(absolute_path) -} diff --git a/language/tools/mirai-dataflow-analysis/tests/datalog_tests.rs b/language/tools/mirai-dataflow-analysis/tests/datalog_tests.rs deleted file mode 100644 index 3e554e1b5e..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/datalog_tests.rs +++ /dev/null @@ -1,122 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// SPDX-License-Identifier: Apache-2.0 - -use regex::Regex; -use std::{ - collections::HashMap, - fs, - fs::read_to_string, - io::Write, - iter::FromIterator, - path::{Path, PathBuf}, - process::{Command, Stdio}, - str::FromStr, -}; - -// Gather test files from the test directory -fn gather_tests(directory_path: PathBuf) -> Vec { - let mut test_files = Vec::new(); - let error_msg = format!("Failed to read test directory {:?}", directory_path); - for entry in fs::read_dir(directory_path).unwrap_or_else(|_| panic!("{}", error_msg)) { - let entry = entry.unwrap(); - if !entry.file_type().unwrap().is_file() { - continue; - }; - let file_path = entry.path(); - test_files.push(file_path.into_os_string().into_string().unwrap()); - } - test_files -} - -// Parse expected or actual output into a map -// from trimmed non-empty lines to counts. -fn build_output_counter(output: &str) -> HashMap<&str, u32> { - let items: Vec<&str> = Vec::from_iter( - output - .split('\n') - .collect::>() - .iter() - .filter(|x| !x.is_empty()) - .map(|x| x.trim()), - ); - let mut counter = HashMap::<&str, u32>::new(); - for item in items.iter() { - *counter.entry(item).or_insert(0) += 1; - } - counter -} - -// Two outputs are considered equivalent if they -// have the same lines (and counts of each line), -// order-independent. -fn compare_lines(actual: &str, expected: &str) -> bool { - let actual_counter = build_output_counter(actual); - let expected_counter = build_output_counter(expected); - actual_counter == expected_counter -} - -// Run the Datalog analysis on the test file and -// capture output -fn run_analysis(file_name: &str) -> Result { - let file_data = read_to_string(file_name).expect("Test case should be readable"); - let mut child = Command::new("analyses/ddlog_ddlog/target/release/ddlog_cli") - .stdin(Stdio::piped()) - .stdout(Stdio::piped()) - .spawn() - .expect("Failed to execute process"); - child - .stdin - .take() - .unwrap() - .write_all(file_data.as_bytes()) - .unwrap(); - match child.wait_with_output() { - Ok(output) => Ok((String::from_utf8_lossy(&output.stdout) - + String::from_utf8_lossy(&output.stderr)) - .to_string()), - Err(_) => Err(()), - } -} - -// Check the call graph output files against -// the expected output from the test case file. -fn execute_test(file_name: &str) -> usize { - let test_case_data = - fs::read_to_string(Path::new(&file_name)).expect("Failed to read test case"); - // Check that the expected and actual output files match - let mut expected = String::new(); - let expected_regex = Regex::new(r"(# expect) (.*)").unwrap(); - for capture in expected_regex.captures_iter(&test_case_data) { - if let Some(c) = capture.get(2) { - expected.push_str(c.as_str()); - expected.push('\n') - } - } - let actual = run_analysis(file_name); - if let Ok(actual) = actual { - if compare_lines(&expected, &actual) { - 0 - } else { - println!("{} failed", file_name); - println!("Expected:\n{}", expected); - println!("Actual:\n{}", actual); - 1 - } - } else { - println!("{} failed", file_name); - 1 - } -} - -// Run the tests in the ddlog_tests directory -// This test is ignored by default because it requires manual setup -// of Differential Datalog -#[test] -#[ignore] -fn run_tests() { - let test_path = PathBuf::from_str("./tests/ddlog_tests/").unwrap(); - println!("{:?}", std::fs::canonicalize(&test_path)); - let files = gather_tests(test_path); - let result = files.iter().fold(0, |acc, file| acc + execute_test(file)); - assert_eq!(result, 0); -} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllDataflowVia.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllDataflowVia.dat deleted file mode 100644 index 7132c5fe1e..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllDataflowVia.dat +++ /dev/null @@ -1,18 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(4,1,4); -insert Edge(5,1,5); -insert Edge(6,1,6); - -insert Dom(2,4); -insert Dom(5,6); - -commit; - -dump AllDataflowVia; - -# expect AllDataflowVia{.node1 = 1, .node2 = 2, .node3 = 3} -# expect AllDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4} -# expect AllDataflowVia{.node1 = 1, .node2 = 5, .node3 = 6} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllDataflowVia_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllDataflowVia_loop.dat deleted file mode 100644 index a2a396cb17..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllDataflowVia_loop.dat +++ /dev/null @@ -1,34 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); -insert Edge(4,3,1); - -commit; - -dump AllDataflowVia; - -# expect AllDataflowVia{.node1 = 1, .node2 = 2, .node3 = 1} -# expect AllDataflowVia{.node1 = 1, .node2 = 2, .node3 = 3} -# expect AllDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4} - -# expect AllDataflowVia{.node1 = 1, .node2 = 3, .node3 = 1} -# expect AllDataflowVia{.node1 = 1, .node2 = 3, .node3 = 2} -# expect AllDataflowVia{.node1 = 1, .node2 = 3, .node3 = 4} - -# expect AllDataflowVia{.node1 = 2, .node2 = 1, .node3 = 2} -# expect AllDataflowVia{.node1 = 2, .node2 = 1, .node3 = 3} -# expect AllDataflowVia{.node1 = 2, .node2 = 1, .node3 = 4} - -# expect AllDataflowVia{.node1 = 2, .node2 = 3, .node3 = 1} -# expect AllDataflowVia{.node1 = 2, .node2 = 3, .node3 = 2} -# expect AllDataflowVia{.node1 = 2, .node2 = 3, .node3 = 4} - -# expect AllDataflowVia{.node1 = 3, .node2 = 1, .node3 = 2} -# expect AllDataflowVia{.node1 = 3, .node2 = 1, .node3 = 3} -# expect AllDataflowVia{.node1 = 3, .node2 = 1, .node3 = 4} - -# expect AllDataflowVia{.node1 = 3, .node2 = 2, .node3 = 1} -# expect AllDataflowVia{.node1 = 3, .node2 = 2, .node3 = 3} -# expect AllDataflowVia{.node1 = 3, .node2 = 2, .node3 = 4} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllTypedDataflowVia.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllTypedDataflowVia.dat deleted file mode 100644 index a08397ebbd..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllTypedDataflowVia.dat +++ /dev/null @@ -1,33 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); -insert Edge(4,1,5); -insert Edge(5,1,6); - -insert Dom(2,4); -insert Dom(5,6); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,1); -insert EdgeType(4,1); -insert EdgeType(5,1); - -insert Member(1,2); - -commit; - -dump AllTypedDataflowVia; - -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 3, .t = 2} - -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4, .t = 1} -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4, .t = 2} -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 4, .t = 2} - -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 5, .node3 = 6, .t = 1} -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 5, .node3 = 6, .t = 2} - -# expect AllTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 4, .t = 2} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllTypedDataflowVia_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllTypedDataflowVia_loop.dat deleted file mode 100644 index 933a5eed7c..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/AllTypedDataflowVia_loop.dat +++ /dev/null @@ -1,43 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); -insert Edge(4,3,1); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,1); -insert EdgeType(4,1); - -insert Member(1,2); - -commit; - -dump AllTypedDataflowVia; - -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 1, .t = 2} -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 3, .t = 2} -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4, .t = 2} - -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 1, .t = 2} -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 2, .t = 2} -# expect AllTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 4, .t = 2} - -# expect AllTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 2, .t = 2} -# expect AllTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 3, .t = 2} -# expect AllTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 4, .t = 2} - -# expect AllTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 1, .t = 2} -# expect AllTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 2, .t = 2} -# expect AllTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 4, .t = 2} - -# expect AllTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 2, .t = 1} -# expect AllTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 2, .t = 2} -# expect AllTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 3, .t = 2} -# expect AllTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 4, .t = 1} -# expect AllTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 4, .t = 2} - -# expect AllTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 1, .t = 2} -# expect AllTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 3, .t = 2} -# expect AllTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 4, .t = 2} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Caller.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Caller.dat deleted file mode 100644 index 3be4c8df66..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Caller.dat +++ /dev/null @@ -1,12 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); - -commit; - -dump Caller; - -# expect Caller{.node1 = 1, .node2 = 2} -# expect Caller{.node1 = 2, .node2 = 3} -# expect Caller{.node1 = 1, .node2 = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CallerNT.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CallerNT.dat deleted file mode 100644 index 81609c01c7..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CallerNT.dat +++ /dev/null @@ -1,11 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); - -commit; - -dump CallerNT; - -# expect CallerNT{.node1 = 1, .node2 = 2} -# expect CallerNT{.node1 = 2, .node2 = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Caller_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Caller_loop.dat deleted file mode 100644 index bf199ea548..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Caller_loop.dat +++ /dev/null @@ -1,18 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,1); - -commit; - -dump Caller; - -# expect Caller{.node1 = 1, .node2 = 2} -# expect Caller{.node1 = 1, .node2 = 3} - -# expect Caller{.node1 = 2, .node2 = 1} -# expect Caller{.node1 = 2, .node2 = 3} - -# expect Caller{.node1 = 3, .node2 = 1} -# expect Caller{.node1 = 3, .node2 = 2} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedAtTypeBy.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedAtTypeBy.dat deleted file mode 100644 index 85c764c0fe..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedAtTypeBy.dat +++ /dev/null @@ -1,26 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(4,Exit); -insert NodeType(5,Exit); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,1); - -insert Member(1,2); -insert Member(2,3); - -commit; - -dump CheckedAtTypeBy; - -# expect CheckedAtTypeBy{.node = 2, .checker = 3, .t = 2} -# expect CheckedAtTypeBy{.node = 2, .checker = 3, .t = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedAtTypeBy_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedAtTypeBy_loop.dat deleted file mode 100644 index 164efa499c..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedAtTypeBy_loop.dat +++ /dev/null @@ -1,29 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,4,1); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(4,Exit); -insert NodeType(5,Exit); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,1); -insert EdgeType(5,1); - -insert Member(1,2); -insert Member(2,3); - -commit; - -dump CheckedAtTypeBy; - -# expect CheckedAtTypeBy{.node = 2, .checker = 3, .t = 2} -# expect CheckedAtTypeBy{.node = 2, .checker = 3, .t = 3} -# expect CheckedAtTypeBy{.node = 4, .checker = 3, .t = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedBy.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedBy.dat deleted file mode 100644 index 6e10cc0998..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedBy.dat +++ /dev/null @@ -1,20 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,1,6); - -insert Dom(5,6); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(4,Exit); -insert NodeType(6,Exit); - -commit; - -dump CheckedBy; - -# expect CheckedBy{.node = 2, .checker = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedBy_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedBy_loop.dat deleted file mode 100644 index 3ae7d84470..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/CheckedBy_loop.dat +++ /dev/null @@ -1,22 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,1,6); -insert Edge(6,4,1); - -insert Dom(5,6); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(4,Exit); -insert NodeType(6,Exit); - -commit; - -dump CheckedBy; - -# expect CheckedBy{.node = 2, .checker = 3} -# expect CheckedBy{.node = 4, .checker = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow.dat deleted file mode 100644 index f29f5d6ca2..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow.dat +++ /dev/null @@ -1,32 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(4,1,4); -insert Edge(5,1,5); -insert Edge(6,1,6); -insert Edge(7,4,7); - -insert Dom(2,4); -insert Dom(5,6); - -commit; - -dump Dataflow; - -# expect Dataflow{.node1 = 1, .node2 = 2} -# expect Dataflow{.node1 = 1, .node2 = 3} -# expect Dataflow{.node1 = 1, .node2 = 4} -# expect Dataflow{.node1 = 1, .node2 = 5} -# expect Dataflow{.node1 = 1, .node2 = 6} -# expect Dataflow{.node1 = 1, .node2 = 7} - -# expect Dataflow{.node1 = 2, .node2 = 3} -# expect Dataflow{.node1 = 2, .node2 = 4} -# expect Dataflow{.node1 = 2, .node2 = 7} - -# expect Dataflow{.node1 = 3, .node2 = 4} -# expect Dataflow{.node1 = 3, .node2 = 7} - -# expect Dataflow{.node1 = 5, .node2 = 6} -# expect Dataflow{.node1 = 4, .node2 = 7} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowNotVia.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowNotVia.dat deleted file mode 100644 index 5ff776a5be..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowNotVia.dat +++ /dev/null @@ -1,32 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); -insert Edge(4,1,5); - -insert Dom(4,5); - -commit; - -dump DataflowNotVia; - -# expect DataflowNotVia{.node1 = 1, .node2 = 2, .node3 = 4} -# expect DataflowNotVia{.node1 = 1, .node2 = 2, .node3 = 5} -# expect DataflowNotVia{.node1 = 1, .node2 = 3, .node3 = 2} -# expect DataflowNotVia{.node1 = 1, .node2 = 3, .node3 = 4} -# expect DataflowNotVia{.node1 = 1, .node2 = 3, .node3 = 5} -# expect DataflowNotVia{.node1 = 1, .node2 = 4, .node3 = 2} -# expect DataflowNotVia{.node1 = 1, .node2 = 4, .node3 = 3} -# expect DataflowNotVia{.node1 = 1, .node2 = 4, .node3 = 5} -# expect DataflowNotVia{.node1 = 1, .node2 = 5, .node3 = 2} -# expect DataflowNotVia{.node1 = 1, .node2 = 5, .node3 = 3} -# expect DataflowNotVia{.node1 = 1, .node2 = 5, .node3 = 4} - -# expect DataflowNotVia{.node1 = 2, .node2 = 1, .node3 = 3} -# expect DataflowNotVia{.node1 = 2, .node2 = 4, .node3 = 3} -# expect DataflowNotVia{.node1 = 2, .node2 = 5, .node3 = 3} - -# expect DataflowNotVia{.node1 = 4, .node2 = 1, .node3 = 5} -# expect DataflowNotVia{.node1 = 4, .node2 = 2, .node3 = 5} -# expect DataflowNotVia{.node1 = 4, .node2 = 3, .node3 = 5} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowNotVia_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowNotVia_loop.dat deleted file mode 100644 index 2cf4167c12..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowNotVia_loop.dat +++ /dev/null @@ -1,27 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); -insert Edge(4,3,1); - -commit; - -dump DataflowNotVia; - -# expect DataflowNotVia{.node1 = 1, .node2 = 2, .node3 = 4} -# expect DataflowNotVia{.node1 = 1, .node2 = 3, .node3 = 2} -# expect DataflowNotVia{.node1 = 1, .node2 = 3, .node3 = 4} -# expect DataflowNotVia{.node1 = 1, .node2 = 4, .node3 = 1} -# expect DataflowNotVia{.node1 = 1, .node2 = 4, .node3 = 2} -# expect DataflowNotVia{.node1 = 1, .node2 = 4, .node3 = 3} - -# expect DataflowNotVia{.node1 = 2, .node2 = 1, .node3 = 3} -# expect DataflowNotVia{.node1 = 2, .node2 = 4, .node3 = 1} -# expect DataflowNotVia{.node1 = 2, .node2 = 4, .node3 = 2} -# expect DataflowNotVia{.node1 = 2, .node2 = 4, .node3 = 3} - -# expect DataflowNotVia{.node1 = 3, .node2 = 2, .node3 = 1} -# expect DataflowNotVia{.node1 = 3, .node2 = 4, .node3 = 1} -# expect DataflowNotVia{.node1 = 3, .node2 = 4, .node3 = 2} -# expect DataflowNotVia{.node1 = 3, .node2 = 4, .node3 = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowVia.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowVia.dat deleted file mode 100644 index 8bf2a586b9..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowVia.dat +++ /dev/null @@ -1,24 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(4,1,4); -insert Edge(5,1,5); -insert Edge(6,1,6); - -insert Dom(2,4); -insert Dom(5,6); - -commit; - -dump DataflowVia; - - -# expect DataflowVia{.node1 = 1, .node2 = 2, .node3 = 3} -# expect DataflowVia{.node1 = 1, .node2 = 2, .node3 = 4} - -# expect DataflowVia{.node1 = 1, .node2 = 3, .node3 = 4} - -# expect DataflowVia{.node1 = 1, .node2 = 5, .node3 = 6} - -# expect DataflowVia{.node1 = 2, .node2 = 3, .node3 = 4} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowVia_mix_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowVia_mix_loop.dat deleted file mode 100644 index 9969d6fb91..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DataflowVia_mix_loop.dat +++ /dev/null @@ -1,28 +0,0 @@ -# Dataflow loop formed by a mix of caller edges and dominance. - -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(5,3,1); - -insert Dom(2,3); - -commit; - -dump DataflowVia; - -# expect DataflowVia{.node1 = 1, .node2 = 2, .node3 = 1} -# expect DataflowVia{.node1 = 1, .node2 = 2, .node3 = 3} -# expect DataflowVia{.node1 = 1, .node2 = 3, .node3 = 1} -# expect DataflowVia{.node1 = 1, .node2 = 3, .node3 = 2} - -# expect DataflowVia{.node1 = 2, .node2 = 1, .node3 = 2} -# expect DataflowVia{.node1 = 2, .node2 = 1, .node3 = 3} -# expect DataflowVia{.node1 = 2, .node2 = 3, .node3 = 1} -# expect DataflowVia{.node1 = 2, .node2 = 3, .node3 = 2} - -# expect DataflowVia{.node1 = 3, .node2 = 1, .node3 = 2} -# expect DataflowVia{.node1 = 3, .node2 = 1, .node3 = 3} -# expect DataflowVia{.node1 = 3, .node2 = 2, .node3 = 1} -# expect DataflowVia{.node1 = 3, .node2 = 2, .node3 = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_call_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_call_loop.dat deleted file mode 100644 index 560093e82b..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_call_loop.dat +++ /dev/null @@ -1,32 +0,0 @@ -# Dataflow with a call loop - -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,4,1); - -commit; - -dump Dataflow; - -# expect Dataflow{.node1 = 1, .node2 = 1} -# expect Dataflow{.node1 = 1, .node2 = 2} -# expect Dataflow{.node1 = 1, .node2 = 3} -# expect Dataflow{.node1 = 1, .node2 = 4} - -# expect Dataflow{.node1 = 2, .node2 = 1} -# expect Dataflow{.node1 = 2, .node2 = 2} -# expect Dataflow{.node1 = 2, .node2 = 3} -# expect Dataflow{.node1 = 2, .node2 = 4} - -# expect Dataflow{.node1 = 3, .node2 = 1} -# expect Dataflow{.node1 = 3, .node2 = 2} -# expect Dataflow{.node1 = 3, .node2 = 3} -# expect Dataflow{.node1 = 3, .node2 = 4} - -# expect Dataflow{.node1 = 4, .node2 = 1} -# expect Dataflow{.node1 = 4, .node2 = 2} -# expect Dataflow{.node1 = 4, .node2 = 3} -# expect Dataflow{.node1 = 4, .node2 = 4} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_dom_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_dom_loop.dat deleted file mode 100644 index 2fb7e8181b..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_dom_loop.dat +++ /dev/null @@ -1,44 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,5,1); - -insert Dom(2,5); -insert Dom(5,1); - -commit; - -dump Dataflow; - -# expect Dataflow{.node1 = 1, .node2 = 1} -# expect Dataflow{.node1 = 1, .node2 = 2} -# expect Dataflow{.node1 = 1, .node2 = 3} -# expect Dataflow{.node1 = 1, .node2 = 4} -# expect Dataflow{.node1 = 1, .node2 = 5} - -# expect Dataflow{.node1 = 2, .node2 = 1} -# expect Dataflow{.node1 = 2, .node2 = 2} -# expect Dataflow{.node1 = 2, .node2 = 3} -# expect Dataflow{.node1 = 2, .node2 = 4} -# expect Dataflow{.node1 = 2, .node2 = 5} - -# expect Dataflow{.node1 = 3, .node2 = 1} -# expect Dataflow{.node1 = 3, .node2 = 2} -# expect Dataflow{.node1 = 3, .node2 = 3} -# expect Dataflow{.node1 = 3, .node2 = 4} -# expect Dataflow{.node1 = 3, .node2 = 5} - -# expect Dataflow{.node1 = 4, .node2 = 1} -# expect Dataflow{.node1 = 4, .node2 = 2} -# expect Dataflow{.node1 = 4, .node2 = 3} -# expect Dataflow{.node1 = 4, .node2 = 4} -# expect Dataflow{.node1 = 4, .node2 = 5} - -# expect Dataflow{.node1 = 5, .node2 = 1} -# expect Dataflow{.node1 = 5, .node2 = 2} -# expect Dataflow{.node1 = 5, .node2 = 3} -# expect Dataflow{.node1 = 5, .node2 = 4} -# expect Dataflow{.node1 = 5, .node2 = 5} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_mix_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_mix_loop.dat deleted file mode 100644 index 8f1f27d592..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dataflow_mix_loop.dat +++ /dev/null @@ -1,45 +0,0 @@ -# Dataflow loop formed by a mix of caller edges and dominance. - -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,5,1); - -insert Dom(2,5); - -commit; - -dump Dataflow; - -# expect Dataflow{.node1 = 1, .node2 = 1} -# expect Dataflow{.node1 = 1, .node2 = 2} -# expect Dataflow{.node1 = 1, .node2 = 3} -# expect Dataflow{.node1 = 1, .node2 = 4} -# expect Dataflow{.node1 = 1, .node2 = 5} - -# expect Dataflow{.node1 = 2, .node2 = 1} -# expect Dataflow{.node1 = 2, .node2 = 2} -# expect Dataflow{.node1 = 2, .node2 = 3} -# expect Dataflow{.node1 = 2, .node2 = 4} -# expect Dataflow{.node1 = 2, .node2 = 5} - -# expect Dataflow{.node1 = 3, .node2 = 1} -# expect Dataflow{.node1 = 3, .node2 = 2} -# expect Dataflow{.node1 = 3, .node2 = 3} -# expect Dataflow{.node1 = 3, .node2 = 4} -# expect Dataflow{.node1 = 3, .node2 = 5} - -# expect Dataflow{.node1 = 4, .node2 = 1} -# expect Dataflow{.node1 = 4, .node2 = 2} -# expect Dataflow{.node1 = 4, .node2 = 3} -# expect Dataflow{.node1 = 4, .node2 = 4} -# expect Dataflow{.node1 = 4, .node2 = 5} - -# expect Dataflow{.node1 = 5, .node2 = 1} -# expect Dataflow{.node1 = 5, .node2 = 2} -# expect Dataflow{.node1 = 5, .node2 = 3} -# expect Dataflow{.node1 = 5, .node2 = 4} -# expect Dataflow{.node1 = 5, .node2 = 5} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dominates.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dominates.dat deleted file mode 100644 index 90474ba686..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dominates.dat +++ /dev/null @@ -1,16 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); - -insert Dom(2,5); - -commit; - -dump Dominates; - -# expect Dominates{.node1 = 2, .node2 = 5} -# expect Dominates{.node1 = 3, .node2 = 5} -# expect Dominates{.node1 = 4, .node2 = 5} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DominatesNT.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DominatesNT.dat deleted file mode 100644 index e99f59a832..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/DominatesNT.dat +++ /dev/null @@ -1,14 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); - -insert Dom(2,5); - -commit; - -dump DominatesNT; - -# expect DominatesNT{.node1 = 2, .node2 = 5} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dominates_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dominates_loop.dat deleted file mode 100644 index 54cce88472..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/Dominates_loop.dat +++ /dev/null @@ -1,23 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,5,1); - -insert Dom(2,5); -insert Dom(5,1); - -commit; - -dump Dominates; - -# expect Dominates{.node1 = 2, .node2 = 5} -# expect Dominates{.node1 = 3, .node2 = 5} -# expect Dominates{.node1 = 4, .node2 = 5} - -# expect Dominates{.node1 = 5, .node2 = 1} -# expect Dominates{.node1 = 2, .node2 = 1} -# expect Dominates{.node1 = 3, .node2 = 1} -# expect Dominates{.node1 = 4, .node2 = 1} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/MemberTrans.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/MemberTrans.dat deleted file mode 100644 index 1fb24658e7..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/MemberTrans.dat +++ /dev/null @@ -1,17 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); - -insert EdgeType(1,1); -insert EdgeType(2,2); - -insert Member(1,2); - -commit; - -dump MemberTrans; - -# expect MemberTrans{.rtype1 = 1, .rtype2 = 1} -# expect MemberTrans{.rtype1 = 1, .rtype2 = 2} -# expect MemberTrans{.rtype1 = 2, .rtype2 = 2} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedAtTypeBy.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedAtTypeBy.dat deleted file mode 100644 index e946d36bb0..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedAtTypeBy.dat +++ /dev/null @@ -1,39 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(4,Exit); -insert NodeType(5,Exit); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,1); - -insert Member(1,2); -insert Member(2,3); - -commit; - -dump NeverCheckedAtTypeBy; - -# expect NeverCheckedAtTypeBy{.node = 1, .checker = 3, .t = 1} - -# expect NeverCheckedAtTypeBy{.node = 2, .checker = 3, .t = 1} - -# expect NeverCheckedAtTypeBy{.node = 3, .checker = 3, .t = 1} -# expect NeverCheckedAtTypeBy{.node = 3, .checker = 3, .t = 2} -# expect NeverCheckedAtTypeBy{.node = 3, .checker = 3, .t = 3} - -# expect NeverCheckedAtTypeBy{.node = 4, .checker = 3, .t = 1} -# expect NeverCheckedAtTypeBy{.node = 4, .checker = 3, .t = 2} -# expect NeverCheckedAtTypeBy{.node = 4, .checker = 3, .t = 3} - -# expect NeverCheckedAtTypeBy{.node = 5, .checker = 3, .t = 1} -# expect NeverCheckedAtTypeBy{.node = 5, .checker = 3, .t = 2} -# expect NeverCheckedAtTypeBy{.node = 5, .checker = 3, .t = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedAtTypeBy_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedAtTypeBy_loop.dat deleted file mode 100644 index c1c7339e30..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedAtTypeBy_loop.dat +++ /dev/null @@ -1,38 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,4,1); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(4,Exit); -insert NodeType(5,Exit); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,1); -insert EdgeType(5,1); - -insert Member(1,2); -insert Member(2,3); - -commit; - -dump NeverCheckedAtTypeBy; - -# expect NeverCheckedAtTypeBy{.node = 1, .checker = 3, .t = 1} - -# expect NeverCheckedAtTypeBy{.node = 2, .checker = 3, .t = 1} - -# expect NeverCheckedAtTypeBy{.node = 3, .checker = 3, .t = 1} -# expect NeverCheckedAtTypeBy{.node = 3, .checker = 3, .t = 2} - -# expect NeverCheckedAtTypeBy{.node = 4, .checker = 3, .t = 1} - -# expect NeverCheckedAtTypeBy{.node = 5, .checker = 3, .t = 1} -# expect NeverCheckedAtTypeBy{.node = 5, .checker = 3, .t = 2} -# expect NeverCheckedAtTypeBy{.node = 5, .checker = 3, .t = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedBy.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedBy.dat deleted file mode 100644 index 2471100b0c..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedBy.dat +++ /dev/null @@ -1,23 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,1,6); - -insert Dom(5,6); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(3,Exit); -insert NodeType(6,Exit); - -commit; - -dump NeverCheckedBy; - -# expect NeverCheckedBy{.node = 3, .checker = 3} -# expect NeverCheckedBy{.node = 4, .checker = 3} -# expect NeverCheckedBy{.node = 5, .checker = 3} -# expect NeverCheckedBy{.node = 6, .checker = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedBy_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedBy_loop.dat deleted file mode 100644 index 392e2110f0..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NeverCheckedBy_loop.dat +++ /dev/null @@ -1,22 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,1,6); -insert Edge(6,4,1); - -insert Dom(5,6); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(3,Exit); -insert NodeType(6,Exit); - -commit; - -dump NeverCheckedBy; - -# expect NeverCheckedBy{.node = 5, .checker = 3} -# expect NeverCheckedBy{.node = 6, .checker = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoDataflowVia.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoDataflowVia.dat deleted file mode 100644 index a1ec432e43..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoDataflowVia.dat +++ /dev/null @@ -1,48 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); - -commit; - -dump NoDataflowVia; - -# expect NoDataflowVia{.node1 = 1, .node2 = 2, .node3 = 1} -# expect NoDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4} -# expect NoDataflowVia{.node1 = 1, .node2 = 3, .node3 = 1} -# expect NoDataflowVia{.node1 = 1, .node2 = 3, .node3 = 2} -# expect NoDataflowVia{.node1 = 1, .node2 = 3, .node3 = 4} -# expect NoDataflowVia{.node1 = 1, .node2 = 4, .node3 = 1} -# expect NoDataflowVia{.node1 = 1, .node2 = 4, .node3 = 2} -# expect NoDataflowVia{.node1 = 1, .node2 = 4, .node3 = 3} - -# expect NoDataflowVia{.node1 = 2, .node2 = 1, .node3 = 2} -# expect NoDataflowVia{.node1 = 2, .node2 = 1, .node3 = 3} -# expect NoDataflowVia{.node1 = 2, .node2 = 1, .node3 = 4} -# expect NoDataflowVia{.node1 = 2, .node2 = 3, .node3 = 1} -# expect NoDataflowVia{.node1 = 2, .node2 = 3, .node3 = 2} -# expect NoDataflowVia{.node1 = 2, .node2 = 3, .node3 = 4} -# expect NoDataflowVia{.node1 = 2, .node2 = 4, .node3 = 1} -# expect NoDataflowVia{.node1 = 2, .node2 = 4, .node3 = 2} -# expect NoDataflowVia{.node1 = 2, .node2 = 4, .node3 = 3} - -# expect NoDataflowVia{.node1 = 3, .node2 = 1, .node3 = 2} -# expect NoDataflowVia{.node1 = 3, .node2 = 1, .node3 = 3} -# expect NoDataflowVia{.node1 = 3, .node2 = 1, .node3 = 4} -# expect NoDataflowVia{.node1 = 3, .node2 = 2, .node3 = 1} -# expect NoDataflowVia{.node1 = 3, .node2 = 2, .node3 = 3} -# expect NoDataflowVia{.node1 = 3, .node2 = 2, .node3 = 4} -# expect NoDataflowVia{.node1 = 3, .node2 = 4, .node3 = 1} -# expect NoDataflowVia{.node1 = 3, .node2 = 4, .node3 = 2} -# expect NoDataflowVia{.node1 = 3, .node2 = 4, .node3 = 3} - -# expect NoDataflowVia{.node1 = 4, .node2 = 1, .node3 = 2} -# expect NoDataflowVia{.node1 = 4, .node2 = 1, .node3 = 3} -# expect NoDataflowVia{.node1 = 4, .node2 = 1, .node3 = 4} -# expect NoDataflowVia{.node1 = 4, .node2 = 2, .node3 = 1} -# expect NoDataflowVia{.node1 = 4, .node2 = 2, .node3 = 3} -# expect NoDataflowVia{.node1 = 4, .node2 = 2, .node3 = 4} -# expect NoDataflowVia{.node1 = 4, .node2 = 3, .node3 = 1} -# expect NoDataflowVia{.node1 = 4, .node2 = 3, .node3 = 2} -# expect NoDataflowVia{.node1 = 4, .node2 = 3, .node3 = 4} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoDataflowVia_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoDataflowVia_loop.dat deleted file mode 100644 index db4d3a9371..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoDataflowVia_loop.dat +++ /dev/null @@ -1,32 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); -insert Edge(4,3,1); - -commit; - -dump NoDataflowVia; - -# expect NoDataflowVia{.node1 = 1, .node2 = 4, .node3 = 1} -# expect NoDataflowVia{.node1 = 1, .node2 = 4, .node3 = 2} -# expect NoDataflowVia{.node1 = 1, .node2 = 4, .node3 = 3} - -# expect NoDataflowVia{.node1 = 2, .node2 = 4, .node3 = 1} -# expect NoDataflowVia{.node1 = 2, .node2 = 4, .node3 = 2} -# expect NoDataflowVia{.node1 = 2, .node2 = 4, .node3 = 3} - -# expect NoDataflowVia{.node1 = 3, .node2 = 4, .node3 = 1} -# expect NoDataflowVia{.node1 = 3, .node2 = 4, .node3 = 2} -# expect NoDataflowVia{.node1 = 3, .node2 = 4, .node3 = 3} - -# expect NoDataflowVia{.node1 = 4, .node2 = 1, .node3 = 2} -# expect NoDataflowVia{.node1 = 4, .node2 = 1, .node3 = 3} -# expect NoDataflowVia{.node1 = 4, .node2 = 1, .node3 = 4} -# expect NoDataflowVia{.node1 = 4, .node2 = 2, .node3 = 1} -# expect NoDataflowVia{.node1 = 4, .node2 = 2, .node3 = 3} -# expect NoDataflowVia{.node1 = 4, .node2 = 2, .node3 = 4} -# expect NoDataflowVia{.node1 = 4, .node2 = 3, .node3 = 1} -# expect NoDataflowVia{.node1 = 4, .node2 = 3, .node3 = 2} -# expect NoDataflowVia{.node1 = 4, .node2 = 3, .node3 = 4} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoTypedDataflowVia.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoTypedDataflowVia.dat deleted file mode 100644 index 24b8dd5ab0..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoTypedDataflowVia.dat +++ /dev/null @@ -1,88 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); - -insert EdgeType(1,1); -insert EdgeType(2,1); -insert EdgeType(3,2); - -commit; - -dump NoTypedDataflowVia; - -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 3, .t = 2} - -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 3, .t = 2} - -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 3, .t = 2} - -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 4, .t = 2} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoTypedDataflowVia_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoTypedDataflowVia_loop.dat deleted file mode 100644 index 24b8dd5ab0..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NoTypedDataflowVia_loop.dat +++ /dev/null @@ -1,88 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); - -insert EdgeType(1,1); -insert EdgeType(2,1); -insert EdgeType(3,2); - -commit; - -dump NoTypedDataflowVia; - -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 1, .node2 = 4, .node3 = 3, .t = 2} - -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 2, .node2 = 4, .node3 = 3, .t = 2} - -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 3, .node2 = 4, .node3 = 3, .t = 2} - -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 1, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 3, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 3, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 2, .node3 = 4, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 1, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 1, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 2, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 2, .t = 2} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 4, .t = 1} -# expect NoTypedDataflowVia{.node1 = 4, .node2 = 3, .node3 = 4, .t = 2} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedAtTypeBy.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedAtTypeBy.dat deleted file mode 100644 index 551d6a24b4..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedAtTypeBy.dat +++ /dev/null @@ -1,41 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(4,Exit); -insert NodeType(5,Exit); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,1); - -insert Member(1,2); -insert Member(2,3); - -commit; - -dump NotCheckedAtTypeBy; - -# expect NotCheckedAtTypeBy{.node = 1, .checker = 3, .t = 1} -# expect NotCheckedAtTypeBy{.node = 1, .checker = 3, .t = 2} -# expect NotCheckedAtTypeBy{.node = 1, .checker = 3, .t = 3} - -# expect NotCheckedAtTypeBy{.node = 2, .checker = 3, .t = 1} - -# expect NotCheckedAtTypeBy{.node = 3, .checker = 3, .t = 1} -# expect NotCheckedAtTypeBy{.node = 3, .checker = 3, .t = 2} -# expect NotCheckedAtTypeBy{.node = 3, .checker = 3, .t = 3} - -# expect NotCheckedAtTypeBy{.node = 4, .checker = 3, .t = 1} -# expect NotCheckedAtTypeBy{.node = 4, .checker = 3, .t = 2} -# expect NotCheckedAtTypeBy{.node = 4, .checker = 3, .t = 3} - -# expect NotCheckedAtTypeBy{.node = 5, .checker = 3, .t = 1} -# expect NotCheckedAtTypeBy{.node = 5, .checker = 3, .t = 2} -# expect NotCheckedAtTypeBy{.node = 5, .checker = 3, .t = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedAtTypeBy_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedAtTypeBy_loop.dat deleted file mode 100644 index 2f90e7538a..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedAtTypeBy_loop.dat +++ /dev/null @@ -1,40 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,4,1); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(4,Exit); -insert NodeType(5,Exit); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,1); -insert EdgeType(5,1); - -insert Member(1,2); -insert Member(2,3); - -commit; - -dump NotCheckedAtTypeBy; - -# expect NotCheckedAtTypeBy{.node = 1, .checker = 3, .t = 1} -# expect NotCheckedAtTypeBy{.node = 1, .checker = 3, .t = 2} -# expect NotCheckedAtTypeBy{.node = 1, .checker = 3, .t = 3} - -# expect NotCheckedAtTypeBy{.node = 2, .checker = 3, .t = 1} - -# expect NotCheckedAtTypeBy{.node = 3, .checker = 3, .t = 1} -# expect NotCheckedAtTypeBy{.node = 3, .checker = 3, .t = 2} - -# expect NotCheckedAtTypeBy{.node = 4, .checker = 3, .t = 1} - -# expect NotCheckedAtTypeBy{.node = 5, .checker = 3, .t = 1} -# expect NotCheckedAtTypeBy{.node = 5, .checker = 3, .t = 2} -# expect NotCheckedAtTypeBy{.node = 5, .checker = 3, .t = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedBy.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedBy.dat deleted file mode 100644 index 35e28d4e4f..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedBy.dat +++ /dev/null @@ -1,24 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,1,6); - -insert Dom(5,6); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(3,Exit); -insert NodeType(6,Exit); - -commit; - -dump NotCheckedBy; - -# expect NotCheckedBy{.node = 1, .checker = 3} -# expect NotCheckedBy{.node = 3, .checker = 3} -# expect NotCheckedBy{.node = 4, .checker = 3} -# expect NotCheckedBy{.node = 5, .checker = 3} -# expect NotCheckedBy{.node = 6, .checker = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedBy_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedBy_loop.dat deleted file mode 100644 index 82386a40a2..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotCheckedBy_loop.dat +++ /dev/null @@ -1,21 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,5); -insert Edge(4,1,6); -insert Edge(5,3,1); - -insert Dom(5,6); - -insert NodeType(1,Entry); -insert NodeType(3,Checker); -insert NodeType(6,Exit); - -commit; - -dump NotCheckedBy; - -# expect NotCheckedBy{.node = 1, .checker = 3} -# expect NotCheckedBy{.node = 5, .checker = 3} -# expect NotCheckedBy{.node = 6, .checker = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotEqual.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotEqual.dat deleted file mode 100644 index bf2ee7a7ee..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/NotEqual.dat +++ /dev/null @@ -1,11 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,1); - -commit; - -dump NotEqual; - -# expect NotEqual{.node1 = 1, .node2 = 2} -# expect NotEqual{.node1 = 2, .node2 = 1} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypeEquality.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypeEquality.dat deleted file mode 100644 index 647813f36c..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypeEquality.dat +++ /dev/null @@ -1,18 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); - -insert EdgeType(1,1); -insert EdgeType(2,2); - -insert EqType(1,2); - -commit; - -dump TypeEquality; - -# expect TypeEquality{.rtype1 = 1, .rtype2 = 1} -# expect TypeEquality{.rtype1 = 1, .rtype2 = 2} -# expect TypeEquality{.rtype1 = 2, .rtype2 = 1} -# expect TypeEquality{.rtype1 = 2, .rtype2 = 2} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCaller.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCaller.dat deleted file mode 100644 index 0f952e3d47..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCaller.dat +++ /dev/null @@ -1,21 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); - -insert Member(1,2); - -commit; - -dump TypedCaller; - -# expect TypedCaller{.node1 = 1, .node2 = 2, .t = 1} -# expect TypedCaller{.node1 = 1, .node2 = 2, .t = 2} -# expect TypedCaller{.node1 = 1, .node2 = 3, .t = 2} -# expect TypedCaller{.node1 = 2, .node2 = 3, .t = 2} -# expect TypedCaller{.node1 = 3, .node2 = 4, .t = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCallerNT.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCallerNT.dat deleted file mode 100644 index 7e0e78423a..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCallerNT.dat +++ /dev/null @@ -1,20 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); - -insert Member(1,2); - -commit; - -dump TypedCallerNT; - -# expect TypedCallerNT{.node1 = 1, .node2 = 2, .t = 1} -# expect TypedCallerNT{.node1 = 1, .node2 = 2, .t = 2} -# expect TypedCallerNT{.node1 = 2, .node2 = 3, .t = 2} -# expect TypedCallerNT{.node1 = 3, .node2 = 4, .t = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCaller_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCaller_loop.dat deleted file mode 100644 index a03b9390e0..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedCaller_loop.dat +++ /dev/null @@ -1,22 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,4,1); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); - -insert Member(1,2); - -commit; - -dump TypedCaller; - -# expect TypedCaller{.node1 = 1, .node2 = 2, .t = 1} -# expect TypedCaller{.node1 = 1, .node2 = 2, .t = 2} -# expect TypedCaller{.node1 = 1, .node2 = 3, .t = 2} -# expect TypedCaller{.node1 = 2, .node2 = 3, .t = 2} -# expect TypedCaller{.node1 = 3, .node2 = 4, .t = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflow.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflow.dat deleted file mode 100644 index 030fc561f3..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflow.dat +++ /dev/null @@ -1,71 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); -insert Edge(4,1,5); -insert Edge(5,1,6); -insert Edge(7,4,7); - -insert Dom(2,4); -insert Dom(5,6); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,1); -insert EdgeType(5,1); -insert EdgeType(7,4); - -insert Member(1,2); -insert Member(2,3); -insert Member(3,4); - -commit; - -dump TypedDataflow; - -# expect TypedDataflow{.node1 = 1, .node2 = 2, .t = 1} -# expect TypedDataflow{.node1 = 1, .node2 = 2, .t = 2} -# expect TypedDataflow{.node1 = 1, .node2 = 2, .t = 3} -# expect TypedDataflow{.node1 = 1, .node2 = 2, .t = 4} - -# expect TypedDataflow{.node1 = 1, .node2 = 3, .t = 2} -# expect TypedDataflow{.node1 = 1, .node2 = 3, .t = 3} -# expect TypedDataflow{.node1 = 1, .node2 = 3, .t = 4} - -# expect TypedDataflow{.node1 = 1, .node2 = 4, .t = 3} -# expect TypedDataflow{.node1 = 1, .node2 = 4, .t = 4} - -# expect TypedDataflow{.node1 = 1, .node2 = 5, .t = 1} -# expect TypedDataflow{.node1 = 1, .node2 = 5, .t = 2} -# expect TypedDataflow{.node1 = 1, .node2 = 5, .t = 3} -# expect TypedDataflow{.node1 = 1, .node2 = 5, .t = 4} - -# expect TypedDataflow{.node1 = 1, .node2 = 6, .t = 1} -# expect TypedDataflow{.node1 = 1, .node2 = 6, .t = 2} -# expect TypedDataflow{.node1 = 1, .node2 = 6, .t = 3} -# expect TypedDataflow{.node1 = 1, .node2 = 6, .t = 4} - -# expect TypedDataflow{.node1 = 1, .node2 = 7, .t = 4} - -# expect TypedDataflow{.node1 = 2, .node2 = 3, .t = 2} -# expect TypedDataflow{.node1 = 2, .node2 = 3, .t = 3} -# expect TypedDataflow{.node1 = 2, .node2 = 3, .t = 4} - -# expect TypedDataflow{.node1 = 2, .node2 = 4, .t = 3} -# expect TypedDataflow{.node1 = 2, .node2 = 4, .t = 4} - -# expect TypedDataflow{.node1 = 2, .node2 = 7, .t = 4} - -# expect TypedDataflow{.node1 = 3, .node2 = 4, .t = 3} -# expect TypedDataflow{.node1 = 3, .node2 = 4, .t = 4} - -# expect TypedDataflow{.node1 = 3, .node2 = 7, .t = 4} - -# expect TypedDataflow{.node1 = 4, .node2 = 7, .t = 4} - -# expect TypedDataflow{.node1 = 5, .node2 = 6, .t = 1} -# expect TypedDataflow{.node1 = 5, .node2 = 6, .t = 2} -# expect TypedDataflow{.node1 = 5, .node2 = 6, .t = 3} -# expect TypedDataflow{.node1 = 5, .node2 = 6, .t = 4} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowNotVia.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowNotVia.dat deleted file mode 100644 index 0fd85adb49..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowNotVia.dat +++ /dev/null @@ -1,27 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); -insert Edge(4,1,5); - -insert Dom(4,5); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,1); - -commit; - -dump TypedDataflowNotVia; - -# expect TypedDataflowNotVia{.node1 = 1, .node2 = 2, .node3 = 4, .t = 3} -# expect TypedDataflowNotVia{.node1 = 1, .node2 = 2, .node3 = 5, .t = 1} -# expect TypedDataflowNotVia{.node1 = 1, .node2 = 3, .node3 = 4, .t = 3} -# expect TypedDataflowNotVia{.node1 = 1, .node2 = 3, .node3 = 5, .t = 1} -# expect TypedDataflowNotVia{.node1 = 1, .node2 = 4, .node3 = 5, .t = 1} -# expect TypedDataflowNotVia{.node1 = 1, .node2 = 5, .node3 = 4, .t = 3} -# expect TypedDataflowNotVia{.node1 = 2, .node2 = 1, .node3 = 3, .t = 2} -# expect TypedDataflowNotVia{.node1 = 2, .node2 = 4, .node3 = 3, .t = 2} -# expect TypedDataflowNotVia{.node1 = 2, .node2 = 5, .node3 = 3, .t = 2} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowNotVia_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowNotVia_loop.dat deleted file mode 100644 index a75e0fc4a0..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowNotVia_loop.dat +++ /dev/null @@ -1,19 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); -insert Edge(4,3,1); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,1); - -commit; - -dump TypedDataflowNotVia; - -# expect TypedDataflowNotVia{.node1 = 1, .node2 = 2, .node3 = 4, .t = 3} -# expect TypedDataflowNotVia{.node1 = 1, .node2 = 3, .node3 = 4, .t = 3} -# expect TypedDataflowNotVia{.node1 = 3, .node2 = 4, .node3 = 2, .t = 1} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowVia.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowVia.dat deleted file mode 100644 index e9b2d4a8aa..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowVia.dat +++ /dev/null @@ -1,42 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,1,4); -insert Edge(4,1,5); -insert Edge(5,1,6); - -insert Dom(2,4); -insert Dom(5,6); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,1); -insert EdgeType(5,1); - -insert Member(1,2); -insert Member(2,3); -insert Member(3,4); - -commit; - -dump TypedDataflowVia; - -# expect TypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 3, .t = 2} -# expect TypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 3, .t = 3} -# expect TypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 3, .t = 4} - -# expect TypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4, .t = 3} -# expect TypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 4, .t = 4} - -# expect TypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 4, .t = 3} -# expect TypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 4, .t = 4} - -# expect TypedDataflowVia{.node1 = 1, .node2 = 5, .node3 = 6, .t = 1} -# expect TypedDataflowVia{.node1 = 1, .node2 = 5, .node3 = 6, .t = 2} -# expect TypedDataflowVia{.node1 = 1, .node2 = 5, .node3 = 6, .t = 3} -# expect TypedDataflowVia{.node1 = 1, .node2 = 5, .node3 = 6, .t = 4} - -# expect TypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 4, .t = 3} -# expect TypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 4, .t = 4} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowVia_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowVia_loop.dat deleted file mode 100644 index ce8c739e03..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDataflowVia_loop.dat +++ /dev/null @@ -1,35 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,1); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); - -insert Member(1,2); -insert Member(2,3); - -commit; - -dump TypedDataflowVia; - -# expect TypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 1, .t = 3} -# expect TypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 3, .t = 2} -# expect TypedDataflowVia{.node1 = 1, .node2 = 2, .node3 = 3, .t = 3} - -# expect TypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 1, .t = 3} -# expect TypedDataflowVia{.node1 = 1, .node2 = 3, .node3 = 2, .t = 3} - -# expect TypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 2, .t = 3} -# expect TypedDataflowVia{.node1 = 2, .node2 = 1, .node3 = 3, .t = 3} - -# expect TypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 1, .t = 3} -# expect TypedDataflowVia{.node1 = 2, .node2 = 3, .node3 = 2, .t = 3} - -# expect TypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 2, .t = 3} -# expect TypedDataflowVia{.node1 = 3, .node2 = 1, .node3 = 3, .t = 3} - -# expect TypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 1, .t = 3} -# expect TypedDataflowVia{.node1 = 3, .node2 = 2, .node3 = 3, .t = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominates.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominates.dat deleted file mode 100644 index dc77f5d9c9..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominates.dat +++ /dev/null @@ -1,28 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,1,6); - -insert Dom(2,5); -insert Dom(5,6); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,4); -insert EdgeType(5,4); - -insert Member(1,2); -insert Member(2,3); -insert Member(1,4); - -commit; - -dump TypedDominates; - -# expect TypedDominates{.node1 = 2, .node2 = 5, .t = 4} -# expect TypedDominates{.node1 = 2, .node2 = 6, .t = 4} -# expect TypedDominates{.node1 = 5, .node2 = 6, .t = 4} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominatesNT.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominatesNT.dat deleted file mode 100644 index c0a93e46fd..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominatesNT.dat +++ /dev/null @@ -1,27 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,1,6); - -insert Dom(2,5); -insert Dom(5,6); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,4); -insert EdgeType(5,4); - -insert Member(1,2); -insert Member(2,3); -insert Member(1,4); - -commit; - -dump TypedDominatesNT; - -# expect TypedDominatesNT{.node1 = 2, .node2 = 5, .t = 4} -# expect TypedDominatesNT{.node1 = 5, .node2 = 6, .t = 4} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominates_loop.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominates_loop.dat deleted file mode 100644 index dc77f5d9c9..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/TypedDominates_loop.dat +++ /dev/null @@ -1,28 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); -insert Edge(3,3,4); -insert Edge(4,1,5); -insert Edge(5,1,6); - -insert Dom(2,5); -insert Dom(5,6); - -insert EdgeType(1,1); -insert EdgeType(2,2); -insert EdgeType(3,3); -insert EdgeType(4,4); -insert EdgeType(5,4); - -insert Member(1,2); -insert Member(2,3); -insert Member(1,4); - -commit; - -dump TypedDominates; - -# expect TypedDominates{.node1 = 2, .node2 = 5, .t = 4} -# expect TypedDominates{.node1 = 2, .node2 = 6, .t = 4} -# expect TypedDominates{.node1 = 5, .node2 = 6, .t = 4} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/ValidNode.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/ValidNode.dat deleted file mode 100644 index 1b0fe1e238..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/ValidNode.dat +++ /dev/null @@ -1,12 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); - -commit; - -dump ValidNode; - -# expect ValidNode{.node = 1} -# expect ValidNode{.node = 2} -# expect ValidNode{.node = 3} diff --git a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/ValidType.dat b/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/ValidType.dat deleted file mode 100644 index 4007957c17..0000000000 --- a/language/tools/mirai-dataflow-analysis/tests/ddlog_tests/ValidType.dat +++ /dev/null @@ -1,14 +0,0 @@ -start; - -insert Edge(1,1,2); -insert Edge(2,2,3); - -insert EdgeType(1,1); -insert EdgeType(2,2); - -commit; - -dump ValidType; - -# expect ValidType{.rtype = 1} -# expect ValidType{.rtype = 2} diff --git a/x.toml b/x.toml index 6af5a7ab7f..da2e76c5e8 100644 --- a/x.toml +++ b/x.toml @@ -108,7 +108,7 @@ features = ["failpoints", "fuzzing"] # # *** IMPORTANT *** # -# Published developer tools (e.g. Move compiler) ARE part of the production Diem codebase. +# Published developer tools (e.g. Move compiler) ARE part of the production Move codebase. # They should be listed in the root Cargo.toml's default-members, not here! # # Before adding a new crate to this list, ensure that it is *actually* test-only. If not, add it @@ -124,7 +124,6 @@ members = [ "bytecode-verifier-transactional-tests", "invalid-mutations", "language-benchmarks", - "mirai-dataflow-analysis", "module-generation", # TODO: remove this here once the crate is used in code. There is currently not other way to do this. # The code style direction to mark this crate as pulished doesn't work, because nothing in the repo