Skip to content

Commit b14bece

Browse files
author
Dwight Guth
committed
more optimizations
Former-commit-id: 79048b5606d7f6bd66e2b34f896472040def0cfa [formerly b3f7557be9213cd2ea14e579e22a6c66210dedc5] Former-commit-id: c0f229b9eb25aff06651214cdeeaa4a1f2a8d3b9
1 parent e40e4b8 commit b14bece

11 files changed

Lines changed: 86 additions & 18 deletions

File tree

‎java-backend/src/main/java/org/kframework/backend/java/kil/KCollection.java‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -194,4 +194,9 @@ public Stream<K> stream() {
194194
public int size() {
195195
return items().size();
196196
}
197+
198+
@Override
199+
public Iterable<? extends K> asIterable() {
200+
return this;
201+
}
197202
}

‎java-backend/src/main/java/org/kframework/backend/java/kil/KItemRepresentation.java‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,10 @@ default Stream<K> stream() {
2424

2525
default List<K> items() { throw new AssertionError("Unimplemented"); }
2626

27+
default int size() { throw new AssertionError("Unimplemented"); }
28+
29+
default Iterable<K> asIterable() { throw new AssertionError("Unimplemented"); }
30+
2731
@Override
2832
default org.kframework.kore.KLabel klabel() {
2933
if (kLabel() instanceof KLabelInjection) {

‎kernel/src/main/java/org/kframework/krun/KRunFrontEnd.java‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,12 @@ public static List<Module> getModules(List<Module> definitionSpecificModules) {
8888
public int run() {
8989
scope.enter(kompiledDir.get());
9090
try {
91+
for (int i = 0; i < krunOptions.experimental.profile - 1; i++) {
92+
new KRun(kem, files, tty.stdin).run(compiledDef.get(),
93+
krunOptions,
94+
initializeRewriter.get(),
95+
executionMode.get());
96+
}
9197
return new KRun(kem, files, tty.stdin).run(compiledDef.get(),
9298
krunOptions,
9399
initializeRewriter.get(),

‎kernel/src/main/java/org/kframework/krun/KRunOptions.java‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -311,5 +311,8 @@ public boolean ltlmc() {
311311
@Parameter(names="--native-library-path", description="Directories to search for native libraries in for linking. Useful in defining rewriter plugins.",
312312
listConverter=StringListConverter.class)
313313
public List<String> nativeLibraryPath = Collections.emptyList();
314+
315+
@Parameter(names="--profile", description="Run krun multiple times to gather better performance metrics.")
316+
public int profile = 1;
314317
}
315318
}

‎kernel/src/main/java/org/kframework/parser/binary/BinaryParser.java‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@
44
import org.kframework.kore.K;
55
import org.kframework.kore.KLabel;
66
import org.kframework.utils.errorsystem.KEMException;
7+
import scala.collection.immutable.List$;
8+
import scala.collection.immutable.Nil$;
79

810
import java.io.ByteArrayInputStream;
911
import java.io.DataInputStream;
@@ -41,7 +43,7 @@ private K read400() throws IOException {
4143
int type = 0;
4244
while(type != END) {
4345
type = data.readByte();
44-
List<K> items;
46+
scala.collection.immutable.List<K> items;
4547
int arity;
4648
switch (type) {
4749
case KTOKEN:
@@ -50,17 +52,17 @@ private K read400() throws IOException {
5052
case KAPPLY:
5153
KLabel lbl = readKLabel();
5254
arity = data.readInt();
53-
items = new LinkedList<>();
55+
items = List$.MODULE$.<K>empty();
5456
for (int i = 0; i < arity; i++) {
55-
items.add(0, stack.pop());
57+
items = items.$colon$colon(stack.pop());
5658
}
5759
stack.push(KApply(lbl, KList(items)));
5860
break;
5961
case KSEQUENCE:
6062
arity = data.readInt();
61-
items = new LinkedList<>();
63+
items = List$.MODULE$.<K>empty();
6264
for (int i = 0; i < arity; i++) {
63-
items.add(0, stack.pop());
65+
items = items.$colon$colon(stack.pop());
6466
}
6567
stack.push(KSequence(items));
6668
break;

‎kernel/src/main/java/org/kframework/unparser/ToBinary.java‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -69,22 +69,22 @@ void apply(K k) throws IOException {
6969
} else if (k instanceof KApply) {
7070
KApply app = (KApply) k;
7171

72-
for (K item : app.items()) {
72+
for (K item : app.asIterable()) {
7373
apply(item);
7474
}
7575
data.writeByte(BinaryParser.KAPPLY);
7676
writeString(app.klabel().name());
7777
data.writeBoolean(app.klabel() instanceof KVariable);
78-
data.writeInt(app.items().size());
78+
data.writeInt(app.size());
7979

8080
} else if (k instanceof KSequence) {
8181
KSequence seq = (KSequence) k;
8282

83-
for (K item : seq.items()) {
83+
for (K item : seq.asIterable()) {
8484
apply(item);
85-
}
85+
}
8686
data.writeByte(BinaryParser.KSEQUENCE);
87-
data.writeInt(seq.items().size());
87+
data.writeInt(seq.size());
8888

8989
} else if (k instanceof KVariable) {
9090
KVariable var = (KVariable) k;

‎kore/src/main/java/org/kframework/kore/ListIterable.java‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
package org.kframework.kore;
2+
3+
import scala.collection.immutable.List;
4+
5+
import java.io.Serializable;
6+
import java.util.Iterator;
7+
8+
/**
9+
* Created by dwightguth on 11/19/15.
10+
*/
11+
public class ListIterable<T> implements Iterable<T>, Serializable {
12+
private List<T> list;
13+
14+
public ListIterable(List<T> l) {
15+
this.list = l;
16+
}
17+
18+
@Override
19+
public Iterator<T> iterator() {
20+
return new Iterator<T>() {
21+
22+
@Override
23+
public boolean hasNext() {
24+
return !list.isEmpty();
25+
}
26+
27+
@Override
28+
public T next() {
29+
T head = list.head();
30+
list = (scala.collection.immutable.List<T>) list.tail();
31+
return head;
32+
}
33+
};
34+
}
35+
}

‎kore/src/main/scala/org/kframework/kore/ADT.scala‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,10 +23,14 @@ object ADT {
2323

2424
case class KApply[KK <: K](klabel: kore.KLabel, klist: kore.KList, att: Att = Att()) extends kore.KApply {
2525
def items = klist.items
26+
def size = klist.size
27+
def asIterable = klist.asIterable
2628
}
2729

2830
class KSequence private(val elements: List[K], val att: Att = Att()) extends kore.KSequence {
2931
val items: java.util.List[K] = elements.asJava
32+
val size: Int = elements.size
33+
val asIterable: java.lang.Iterable[K] = new ListIterable(elements)
3034
val kApply: kore.KApply = items.asScala reduceRightOption { (a, b) => KLabel(KLabels.KSEQ)(a, b) } getOrElse { KLabel(KLabels.DOTK)() } match {
3135
case k: kore.KApply => k
3236
case x => KLabel(KLabels.KSEQ)(x, KLabel(KLabels.DOTK)())
@@ -62,6 +66,8 @@ object ADT {
6266
elements foreach { e => assert(e.isInstanceOf[K]) }
6367
def items: java.util.List[K] = elements.asJava
6468
def iterator: Iterator[K] = elements.iterator
69+
val size = elements.size
70+
val asIterable = new ListIterable(elements)
6571
}
6672

6773
case class KRewrite(left: kore.K, right: kore.K, att: Att = Att()) extends kore.KRewrite

‎kore/src/main/scala/org/kframework/kore/KORE.scala‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -21,21 +21,23 @@ object KORE extends Constructors[K] with ScalaSugared[K] {
2121

2222
val constructor = this
2323

24+
lazy val emptyAtt = Attributes()
25+
2426
def Attributes(ks: Set[K]) = attributes.Att(ks.toSeq: _*)
2527
@annotation.varargs def Attributes(ks: K*) = attributes.Att(ks: _*)
2628

2729
def Location(startLine: Int, startColumn: Int, endLine: Int, endColumn: Int) = attributes.Location(startLine,
2830
startColumn, endLine, endColumn)
2931

30-
def KApply(klabel: KLabel, klist: KList): KApply = KApply(klabel, klist, Attributes())
32+
def KApply(klabel: KLabel, klist: KList): KApply = KApply(klabel, klist, emptyAtt)
3133

32-
def KToken(string: String, sort: Sort): KToken = KToken(string, sort, Attributes())
34+
def KToken(string: String, sort: Sort): KToken = KToken(string, sort, emptyAtt)
3335

34-
def KSequence(ks: java.util.List[K]): KSequence = KSequence(ks, Att())
36+
def KSequence(ks: java.util.List[K]): KSequence = KSequence(ks, emptyAtt)
3537

36-
def KRewrite(left: K, right: K): KRewrite = KRewrite(left, right, Attributes())
38+
def KRewrite(left: K, right: K): KRewrite = KRewrite(left, right, emptyAtt)
3739

38-
def InjectedKLabel(label: KLabel): InjectedKLabel = InjectedKLabel(label, Att())
40+
def InjectedKLabel(label: KLabel): InjectedKLabel = InjectedKLabel(label, emptyAtt)
3941

4042
// def toKList: Collector[K, KList] =
4143
// Collector(() => new CombinerFromBuilder(KList.newBuilder()))
@@ -60,6 +62,8 @@ object KORE extends Constructors[K] with ScalaSugared[K] {
6062

6163
override def KList[KK <: K](items: java.util.List[KK]): KList = ADT.KList(items.asScala.toList)
6264

65+
def KList[KK <: K](items: List[KK]): KList = ADT.KList(items)
66+
6367
override def InjectedKLabel(klabel: KLabel, att: Att): InjectedKLabel = ADT.InjectedKLabel(klabel, att)
6468

6569
def toKList: Collector[K, KList] =
@@ -76,5 +80,5 @@ object KORE extends Constructors[K] with ScalaSugared[K] {
7680

7781
def self = this
7882

79-
@annotation.varargs override def KApply(klabel: KLabel, items: K*): KApply = KApply(klabel, KList(items.asJava), Att())
83+
@annotation.varargs override def KApply(klabel: KLabel, items: K*): KApply = KApply(klabel, KList(items.asJava), emptyAtt)
8084
}

‎kore/src/main/scala/org/kframework/kore/interface.scala‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,8 @@ trait Sort {
5252

5353
trait KCollection {
5454
def items: java.util.List[K]
55+
def size: Int
56+
def asIterable: java.lang.Iterable[_ <: K]
5557
def stream: java.util.stream.Stream[K] = items.stream()
5658

5759
override def equals(that: Any): Boolean =
@@ -65,7 +67,6 @@ trait KCollection {
6567
}
6668

6769
trait KList extends KCollection {
68-
def size: Int = items.size
6970
}
7071

7172
trait KApply extends KItem with KCollection {

0 commit comments

Comments
 (0)