k/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java at master · https-github-com-goodman-ops/k · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
// Copyright (c) 2019 K Team. All Rights Reserved.
package org.kframework.compile;

import org.kframework.attributes.Att;
import org.kframework.builtin.KLabels;
import org.kframework.definition.Module;
import org.kframework.definition.Production;
import org.kframework.definition.Rule;
import org.kframework.kil.Attribute;
import org.kframework.kore.K;
import org.kframework.kore.KLabel;
import org.kframework.kore.KApply;
import org.kframework.kore.VisitK;

import edu.uci.ics.jung.graph.DirectedGraph;
import edu.uci.ics.jung.graph.DirectedSparseGraph;
import scala.Tuple2;

import java.util.Collection;
import java.util.Collections;
import java.util.HashSet;
import java.util.LinkedHashSet;
import java.util.LinkedList;
import java.util.Map;
import java.util.Queue;
import java.util.Set;

import static org.kframework.Collections.*;

public class ComputeTransitiveFunctionDependencies {
    public ComputeTransitiveFunctionDependencies(Module module) {
        dependencies = new DirectedSparseGraph<>();

        Set<KLabel> anywhereKLabels = new HashSet<>();
        stream(module.rules()).filter(r -> !ExpandMacros.isMacro(r)).forEach(r -> {
            K left = RewriteToTop.toLeft(r.body());
            if (left instanceof KApply) {
                KApply kapp = (KApply) left;
                if (r.att().contains(Attribute.ANYWHERE_KEY)) {
                    if (kapp.klabel().name().equals(KLabels.INJ)) {
                        K k = kapp.items().get(0);
                        if (k instanceof KApply) {
                            anywhereKLabels.add(((KApply)k).klabel());
                        }
                    } else {
                        anywhereKLabels.add(kapp.klabel());
                    }
                }
            }
        });

        class GetPredecessors extends VisitK {
            private final KLabel current;

            private GetPredecessors(KLabel current) {
                this.current = current;
            }

            @Override
            public void apply(KApply k) {
                if (k.klabel().name().equals(KLabels.INJ)) {
                    super.apply(k);
                    return;
                }
                if (module.attributesFor().getOrElse(k.klabel(), () -> Att.empty()).contains(Attribute.FUNCTION_KEY) || anywhereKLabels.contains(k.klabel())) {
                    dependencies.addEdge(new Object(), current, k.klabel());
                }
                super.apply(k);
            }
        }

        for (Tuple2<KLabel, scala.collection.Set<Rule>> entry : iterable(module.rulesFor())) {
            for (Rule rule : iterable(entry._2())) {
                if (module.attributesFor().getOrElse(entry._1(), () -> Att.empty()).contains(Attribute.FUNCTION_KEY)) {
                    GetPredecessors visitor = new GetPredecessors(entry._1());
                    visitor.apply(rule.body());
                    visitor.apply(rule.requires());
                }
            }
        }
    }

    private static <V> Set<V> ancestors(
            Collection<? extends V> startNodes, DirectedGraph<V, ?> graph)
    {
        Queue<V> queue = new LinkedList<V>();
        queue.addAll(startNodes);
        Set<V> visited = new LinkedHashSet<V>(startNodes);
        while(!queue.isEmpty())
        {
            V v = queue.poll();
            Collection<V> neighbors = graph.getPredecessors(v);
            for (V n : neighbors)
            {
                if (!visited.contains(n))
                {
                    queue.offer(n);
                    visited.add(n);
                }
            }
        }
        return visited;
    }

    public Set<KLabel> ancestors(KLabel label) {
        return ancestors(Collections.singleton(label), dependencies);
    }

    public Set<KLabel> ancestors(Set<KLabel> labels) {
        return ancestors(labels, dependencies);
    }

    private DirectedGraph<KLabel, Object> dependencies;
}