Skip to content
This repository has been archived by the owner on Mar 13, 2024. It is now read-only.

Commit

Permalink
Move components out of recipes
Browse files Browse the repository at this point in the history 
Change-Id: Icb4263392cc23c241c0e6410746e71ac72569052
  • Loading branch information
@Cypher1
Cypher1 committed Mar 3, 2022
1 parent c351e2a commit e873d90
Show file tree
Hide file tree
Showing 11 changed files with 155 additions and 282 deletions.
42 changes: 21 additions & 21 deletions ibis/demo.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,30 +21,30 @@
"metadata": {
"name": "demo"
},
"nodes": [
["p_a", "a", "write", "Int"],
["p_b", "b", "any", "Number"],
["p_c", "c", "write", "String"],
["p_de", "d", "read", "Serializable"],
["p_de", "e", "read", "ibis.UnionType(Number, String)"],
["p_f", "f", "write", "ibis.ProductType(name: String, age: Int)"],
["p_g", "g", "read", "name: *"],
["p_h", "h", "read", "ibis.ProductType(name: String, age: Int)"],
["p_i", "i", "read", "name: String"],
["p_j", "j", "read", "age: Int"]
],
"edges": [
["b", "e"]
],
"claims": [
["a", "private"]
],
"checks": [
["e", "public"]
],
"trusted_to_remove_tag": [
["b", "private"]
]
}
],
"nodes": [
["p_a", "a", "write", "Int"],
["p_b", "b", "any", "Number"],
["p_c", "c", "write", "String"],
["p_de", "d", "read", "Serializable"],
["p_de", "e", "read", "ibis.UnionType(Number, String)"],
["p_f", "f", "write", "ibis.ProductType(name: String, age: Int)"],
["p_g", "g", "read", "name: *"],
["p_h", "h", "read", "ibis.ProductType(name: String, age: Int)"],
["p_i", "i", "read", "name: String"],
["p_j", "j", "read", "age: Int"]
],
"claims": [
["a", "private"]
],
"checks": [
["e", "public"]
],
"trusted_to_remove_tag": [
["b", "private"]
]
}
23 changes: 12 additions & 11 deletions ibis/src/recipe_to_dot.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
// https://developers.google.com/open-source/licenses/bsd

use crate::dot::{DotGraph, ToDot};
use crate::recipes::{Check, Claim, HasTag, Ibis, Leak, Node, Recipe, TypeError};
use crate::recipes::{Check, Claim, HasTag, Ibis, Leak, Node, TrustedToRemoveTag, Recipe, TypeError};
use crate::Sol;
use std::collections::HashMap;

Expand All @@ -31,7 +31,7 @@ impl ToDot for Ibis {
let sol = &recipe.id.expect("Every recipe should have an id?");
let s_id = sol_id(sol);
#[allow(unused_mut)]
let mut sol_graph = recipe.to_dot_repr();
let mut sol_graph = (self, recipe).to_dot_repr();
#[cfg(feature = "ancestors")]
{
let s = Sol::from(recipe);
Expand Down Expand Up @@ -62,34 +62,35 @@ fn sol_id(sol: &Sol) -> String {
format!("sol_{}", &sol.id)
}

impl ToDot for Recipe {
impl ToDot for (&Ibis, &Recipe) {
fn to_dot_repr(&self) -> DotGraph {
let sol = &self.id.expect("Every recipe should have an id?");
let (ibis, recipe) = self;
let sol = &recipe.id.expect("Every recipe should have an id?");
let s_id = sol_id(sol);
let particle_id = |particle| format!("{}_p_{}", &s_id, particle);
let node_id = |node| format!("{}_h_{}", &s_id, node);
let mut sol_graph = DotGraph::default();
let mut particles = HashMap::new();
for Node(particle, node, cap, ty) in &self.nodes {
for Node(particle, node, cap, ty) in &ibis.nodes {
let mut extras: Vec<String> = vec![];
if let Some(feedback) = &self.feedback {
if let Some(feedback) = &recipe.feedback {
for HasTag(_hts, source, sink, tag) in &feedback.has_tags {
if sink == node && source != node {
extras.push(format!("'{}' from {}", tag, source));
}
}
}
for (trusted_n, tag) in &self.trusted_to_remove_tag {
for TrustedToRemoveTag(trusted_n, tag) in &ibis.trusted_to_remove_tag {
if trusted_n == node {
extras.push(format!("trusted to remove tag '{}'", tag));
}
}
for Claim(claim_node, tag) in &self.claims {
for Claim(claim_node, tag) in &ibis.claims {
if claim_node == node {
extras.push(format!("claims to be '{}'", tag));
}
}
for Check(check_node, tag) in &self.checks {
for Check(check_node, tag) in &ibis.checks {
if check_node == node {
extras.push(format!(
"<font color=\"blue\">checked to be '{}'</font>",
Expand All @@ -112,7 +113,7 @@ impl ToDot for Recipe {
);
}

if let Some(feedback) = &self.feedback {
if let Some(feedback) = &recipe.feedback {
for Leak(_leak_s, node, expected, source, tag) in &feedback.leaks {
sol_graph.add_edge(node_id(source), node_id(node), vec![format!("style=dotted color=red label=<<font color=\"red\">expected '{}', found contradiction '{}'</font>>", expected, tag)]);
}
Expand All @@ -122,7 +123,7 @@ impl ToDot for Recipe {
}
}

for (from_id, to_id) in &self.id.expect("WAT").edges() {
for (from_id, to_id) in &recipe.id.expect("WAT").edges() {
let from = format!("{}:s", node_id(from_id));
let to = format!("{}:n", node_id(to_id));
sol_graph.add_edge(from.clone(), to.clone(), vec![]);
Expand Down
94 changes: 31 additions & 63 deletions ibis/src/recipes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ ibis! {
Node(Ent, Ent, Ent, Ent); // particle-identifier, identifier, capability, type
Claim(Ent, Ent); // identifier, tag
Check(Ent, Ent); // identifier, tag
TrustedToRemoveTag(Ent, Ent); // node, tag

// Feedback
HasTag(Sol, Ent, Ent, Ent); // solution, source node, node with tag, tag
Expand All @@ -24,8 +25,7 @@ ibis! {
Subtype(from_type, to_type),
Node(to_particle, to, to_capability, to_type),
(from != to),
Solution(parent),
(!parent.has_edge(from, to));
Solution(parent);

Subtype(
x,
Expand Down Expand Up @@ -108,13 +108,13 @@ ibis! {
HasTag(s, source, curr, tag),
Node(_down_particle, down, _, _),
(s.has_edge(curr, down)),
(!s.is_trusted_to_remove_tag(down, tag));
!TrustedToRemoveTag(down, tag);

HasTag(s, source, down, tag) <- // Propagate tags 'across stream' (i.e. inside a particle)
HasTag(s, source, curr, tag),
Node(particle, curr, _, _),
Node(particle, down, _, _),
(!s.is_trusted_to_remove_tag(down, tag));
!TrustedToRemoveTag(down, tag);

Leak(s, n, t1, source, t2) <-
Check(n, t1),
Expand Down Expand Up @@ -186,6 +186,14 @@ pub struct Ibis {
pub config: Config,
#[serde(default = "starting_recipes", skip_serializing_if = "is_default")]
pub recipes: Vec<Recipe>,
#[serde(default, skip_serializing_if = "is_default")]
pub nodes: Vec<Node>,
#[serde(default, skip_serializing_if = "is_default")]
pub claims: Vec<Claim>,
#[serde(default, skip_serializing_if = "is_default")]
pub checks: Vec<Check>,
#[serde(default, skip_serializing_if = "is_default")]
pub trusted_to_remove_tag: Vec<TrustedToRemoveTag>,
}

#[derive(Default, Debug, Serialize, Deserialize, Eq, PartialEq)]
Expand All @@ -199,14 +207,6 @@ pub struct Recipe {
#[serde(skip_deserializing, flatten)]
pub feedback: Option<Feedback>,
#[serde(default, skip_serializing_if = "is_default")]
pub nodes: Vec<Node>,
#[serde(default, skip_serializing_if = "is_default")]
pub claims: Vec<Claim>,
#[serde(default, skip_serializing_if = "is_default")]
pub checks: Vec<Check>,
#[serde(default, skip_serializing_if = "is_default")]
pub trusted_to_remove_tag: Vec<(Ent, Ent)>,
#[serde(default, skip_serializing_if = "is_default")]
pub edges: Vec<(Ent, Ent)>,
#[cfg(feature = "ancestors")]
#[serde(default, skip_serializing_if = "is_default")]
Expand All @@ -222,27 +222,6 @@ impl Recipe {
id: Some(sol),
feedback: None,
metadata: serde_json::Value::Null,
nodes: solution
.nodes
.iter()
.map(|node| {
let particle = solution.node_to_particle.get(node).unwrap();
let ty = solution.node_types.get(node).unwrap();
let cap = solution.node_capabilities.get(node).unwrap();
Node(*particle, *node, *cap, *ty)
})
.collect(),
claims: solution
.claims
.iter()
.map(|(node, tag)| Claim(*node, *tag))
.collect(),
checks: solution
.checks
.iter()
.map(|(node, tag)| Check(*node, *tag))
.collect(),
trusted_to_remove_tag: solution.trusted_to_remove_tag.iter().cloned().collect(),
edges: solution.edges.iter().cloned().collect(),
}
}
Expand All @@ -266,19 +245,6 @@ impl From<&Recipe> for SolutionData {
fn from(recipe: &Recipe) -> Self {
Self {
edges: make(&recipe.edges, Clone::clone),
checks: make(&recipe.checks, |Check(node, tag)| (*node, *tag)),
claims: make(&recipe.claims, |Claim(node, tag)| (*node, *tag)),
node_to_particle: make(&recipe.nodes, |Node(particle, node, _cap, _ty)| {
(*node, *particle)
}),
node_types: make(&recipe.nodes, |Node(_particle, node, _cap, ty)| {
(*node, *ty)
}),
node_capabilities: make(&recipe.nodes, |Node(_particle, node, cap, _ty)| {
(*node, *cap)
}),
nodes: make(&recipe.nodes, |Node(_particle, node, _cap, _ty)| *node),
trusted_to_remove_tag: make(&recipe.trusted_to_remove_tag, Clone::clone),
}
}
}
Expand All @@ -290,15 +256,6 @@ impl From<Sol> for Recipe {
id: Some(sol),
feedback: None,
metadata: serde_json::Value::Null,
nodes: make(&solution.nodes, |node| {
let particle = solution.node_to_particle.get(node).unwrap();
let ty = solution.node_types.get(node).unwrap();
let cap = solution.node_capabilities.get(node).unwrap();
Node(*particle, *node, *cap, *ty)
}),
claims: make(&solution.claims, |(node, tag)| Claim(*node, *tag)),
checks: make(&solution.checks, |(node, tag)| Check(*node, *tag)),
trusted_to_remove_tag: make(&solution.trusted_to_remove_tag, Clone::clone),
edges: make(&solution.edges, Clone::clone),
#[cfg(feature = "ancestors")]
ancestors: sol.ancestors().iter().cloned().collect(),
Expand Down Expand Up @@ -331,7 +288,15 @@ impl Ibis {
capabilities,
},
mut recipes, // Mutation required to move rather than copy the data.
nodes,
claims,
checks,
trusted_to_remove_tag,
} = recipes;
self.nodes.extend(nodes);
self.claims.extend(claims);
self.checks.extend(checks);
self.trusted_to_remove_tag.extend(trusted_to_remove_tag);
self.config.types.extend(types);
self.config.subtypes.extend(subtypes);
self.config.less_private_than.extend(less_private_than);
Expand Down Expand Up @@ -360,21 +325,20 @@ impl Ibis {
SolutionInput(Sol::from(recipe))
}));

for recipe in self.recipes {
runtime.extend(recipe.checks.iter().map(|check| check.to_claim()));
runtime.extend(recipe.claims.iter().map(|claim| claim.to_claim()));
runtime.extend(recipe.nodes.iter().map(|node| node.to_claim()));
}
runtime.extend(self.checks.iter().map(|check| check.to_claim()));
runtime.extend(self.claims.iter().map(|claim| claim.to_claim()));
runtime.extend(self.nodes.iter().map(|node| node.to_claim()));

let (
solutions,
mut types,
mut less_private_than,
mut capabilities,
mut subtypes,
_nodes,
_claims,
_checks,
mut nodes,
mut claims,
mut checks,
mut trusted_to_remove_tag,
has_tags,
leaks,
type_errors,
Expand Down Expand Up @@ -444,6 +408,10 @@ impl Ibis {
less_private_than: less_private_than.drain().collect(),
capabilities: capabilities.drain().collect(),
},
checks: checks.drain().collect(),
claims: claims.drain().collect(),
nodes: nodes.drain().collect(),
trusted_to_remove_tag: trusted_to_remove_tag.drain().collect(),
recipes,
}
}
Expand Down
26 changes: 3 additions & 23 deletions ibis/src/solution_data.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,20 +5,12 @@
// https://developers.google.com/open-source/licenses/bsd

use crate::ent::*;
use std::collections::{BTreeMap, BTreeSet};
use std::collections::BTreeSet;

#[derive(Clone, PartialEq, Eq, Ord, PartialOrd, Hash, Default)]
pub struct SolutionData {
pub edges: BTreeSet<(Ent, Ent)>, // from, to

// Starting data
pub nodes: BTreeSet<Ent>,
pub node_types: BTreeMap<Ent, Ent>, // node, type
pub node_capabilities: BTreeMap<Ent, Ent>, // node, capability
pub node_to_particle: BTreeMap<Ent, Ent>, // node, particle
pub claims: BTreeSet<(Ent, Ent)>, // node, tag
pub checks: BTreeSet<(Ent, Ent)>, // node, tag
pub trusted_to_remove_tag: BTreeSet<(Ent, Ent)>, // node, tag
// TODO: Instances of: pub particle_instance: BTreeSet<(Ent, Ent)>, // from, to
}

impl SolutionData {
Expand All @@ -31,16 +23,4 @@ impl SolutionData {
n.edges.insert((from, to));
n
}

pub fn add_node(&self, particle: Ent, node: Ent, ty: Ent) -> SolutionData {
let mut n = SolutionData { ..self.clone() };
n.nodes.insert(node);
n.node_to_particle.insert(node, particle);
n.node_types.insert(node, ty);
n
}

pub fn is_trusted_to_remove_tag(&self, node: Ent, tag: Ent) -> bool {
self.trusted_to_remove_tag.contains(&(node, tag))
}
}
}
4 changes: 0 additions & 4 deletions ibis/src/solution_id.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,10 +131,6 @@ impl Sol {
self.solution().has_edge(from, to)
}

pub fn is_trusted_to_remove_tag(&self, node: Ent, tag: Ent) -> bool {
self.solution().is_trusted_to_remove_tag(node, tag)
}

#[cfg(feature = "ancestors")]
fn ancestor_string(&self) -> String {
let ancestors: Vec<String> = self
Expand Down
Loading

0 comments on commit e873d90

Please sign in to comment.