Skip to content

Commit 98015a2

Browse files
author
Dwight Guth
committed
fix concatenation of terms together
Former-commit-id: 8a5ac36e45bb7d351451b5a9527c20164212af46 [formerly db1e0df46b03a7ae9bd904643df49ab1e5c5fbaf] Former-commit-id: 5443f0ca4a69bd75d0e7b08517e149d147b39f07
1 parent f854edd commit 98015a2

7 files changed

Lines changed: 45 additions & 17 deletions

File tree

‎k-distribution/include/ocaml/lexer.mll‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ let parse_k_binary_string (s: char Stream.t) (interns: string list ref) : string
5454
interns := !interns @ [str];
5555
str
5656
else
57-
List.nth !interns (idx_in_interns - 1)
57+
List.nth !interns ((List.length !interns) - idx_in_interns)
5858

5959
let rec parse_k_binary_term (s: char Stream.t) (stack: k Stack.t) (interns: string list ref) : k =
6060
match Char.code (Stream.next s) with

‎k-distribution/include/ocaml/prelude.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -67,15 +67,15 @@ let print_k_binary (c: k) : string = let buf = Buffer.create 16 in
6767
Buffer.add_char buf (Char.chr three);
6868
Buffer.add_char buf (Char.chr four) in
6969
let print_string (s: string) : unit =
70-
let idx = try Hashtbl.find intern s with Not_found -> 0 in
71-
print_int idx;
72-
if idx = 0 then
70+
let idx = try Hashtbl.find intern s with Not_found -> Hashtbl.length intern in
71+
print_int (Hashtbl.length intern - idx);
72+
if idx = Hashtbl.length intern then
7373
(print_int (String.length s);
7474
for i = 0 to (String.length s) - 1 do
7575
Buffer.add_char buf '\x00';
7676
Buffer.add_char buf (String.get s i)
7777
done;
78-
let new_idx = (Hashtbl.length intern) + 1 in
78+
let new_idx = (Hashtbl.length intern) in
7979
assert (not (Hashtbl.mem intern s));
8080
Hashtbl.add intern s new_idx)
8181
else () in

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

Lines changed: 16 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -8,28 +8,32 @@
88
import org.kframework.definition.Module;
99
import org.kframework.definition.Rule;
1010
import org.kframework.kompile.CompiledDefinition;
11-
import org.kframework.kore.VisitK;
1211
import org.kframework.kore.K;
1312
import org.kframework.kore.KApply;
1413
import org.kframework.kore.KToken;
1514
import org.kframework.kore.KVariable;
1615
import org.kframework.kore.Sort;
16+
import org.kframework.kore.VisitK;
1717
import org.kframework.krun.modes.ExecutionMode;
1818
import org.kframework.main.Main;
1919
import org.kframework.parser.ProductionReference;
20+
import org.kframework.parser.binary.BinaryParser;
21+
import org.kframework.parser.kore.KoreParser;
2022
import org.kframework.rewriter.Rewriter;
2123
import org.kframework.unparser.AddBrackets;
2224
import org.kframework.unparser.KOREToTreeNodes;
2325
import org.kframework.unparser.OutputModes;
26+
import org.kframework.unparser.ToBinary;
27+
import org.kframework.unparser.ToKast;
2428
import org.kframework.utils.errorsystem.KEMException;
2529
import org.kframework.utils.errorsystem.KException;
2630
import org.kframework.utils.errorsystem.KExceptionManager;
2731
import org.kframework.utils.errorsystem.ParseFailedException;
2832
import org.kframework.utils.file.FileUtil;
29-
import org.kframework.parser.kore.KoreParser;
3033
import scala.Tuple2;
3134

3235
import java.io.BufferedReader;
36+
import java.io.ByteArrayOutputStream;
3337
import java.io.IOException;
3438
import java.io.InputStreamReader;
3539
import java.util.ArrayList;
@@ -112,9 +116,10 @@ private void printSearchResult(SearchResult result, KRunOptions options, Compile
112116
int i = 1;
113117
List<String> results = new ArrayList<>();
114118
for (Map<? extends KVariable, ? extends K> substitution : searchResult) {
115-
StringBuilder sb = new StringBuilder();
116-
prettyPrintSubstitution(substitution, result.getParsedRule(), compiledDef, options.output, sb::append);
117-
results.add(sb.toString());
119+
ByteArrayOutputStream sb = new ByteArrayOutputStream();
120+
prettyPrintSubstitution(substitution, result.getParsedRule(), compiledDef, options.output, v -> sb.write(v, 0, v.length));
121+
//Note that this is actually unsafe, but we are here assuming that --search is not used with --output binary
122+
results.add(new String(sb.toByteArray()));
118123
}
119124
Collections.sort(results);
120125
StringBuilder sb = new StringBuilder();
@@ -163,7 +168,11 @@ public void outputFile(String output, KRunOptions options) {
163168
}
164169
public void outputFile(byte[] output, KRunOptions options) {
165170
if (options.outputFile == null) {
166-
System.out.print(output);
171+
try {
172+
System.out.write(output);
173+
} catch (IOException e) {
174+
throw KEMException.internalError(e.getMessage(), e);
175+
}
167176
} else {
168177
files.saveToWorkingDirectory(options.outputFile, output);
169178
}
@@ -251,7 +260,7 @@ public void apply(KVariable k) {
251260
prettyPrint(compiledDefinition, outputModes, print, value);
252261
return;
253262
}
254-
prettyPrint(compiledDefinition, outputModes, print, variable);
263+
print.accept(variable.toString().getBytes());
255264
print.accept(" -->\n".getBytes());
256265
prettyPrint(compiledDefinition, outputModes, print, value);
257266
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ private String readString() throws IOException {
105105
interns.add(s);
106106
return s;
107107
} else {
108-
return interns.get(idx - 1);
108+
return interns.get(interns.size() - idx);
109109
}
110110
}
111111

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -110,12 +110,12 @@ void apply(K k) throws IOException {
110110
}
111111

112112
private void writeString(String s) throws IOException {
113-
int idx = interns.getOrDefault(s, 0);
114-
data.writeInt(idx);
115-
if (idx == 0) {
113+
int idx = interns.getOrDefault(s, interns.size());
114+
data.writeInt(interns.size() - idx);
115+
if (idx == interns.size()) {
116116
data.writeInt(s.length());
117117
data.writeChars(s);
118-
interns.put(s, interns.size() + 1);
118+
interns.put(s, interns.size());
119119
}
120120
}
121121
}

‎kernel/src/test/java/org/kframework/unparser/BinaryKASTTest.java‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,24 @@ public void testWriteThenRead() throws Exception {
3838
assertEquals(term, result2);
3939
}
4040

41+
42+
@Test
43+
public void testConcatenate() throws Exception {
44+
File tmp = File.createTempFile("tmp", null);
45+
BinaryLoader loader = new BinaryLoader(new KExceptionManager(new GlobalOptions()));
46+
loader.saveOrDie(tmp, term);
47+
K result = loader.loadOrDie(K.class, tmp);
48+
assertEquals(term, result);
49+
byte[] str = ToBinary.apply(term);
50+
byte[] krewrite = new byte[str.length * 2 - 8];
51+
System.arraycopy(str, 0, krewrite, 0, str.length - 1);
52+
System.arraycopy(str, 8, krewrite, str.length - 1, str.length - 9);
53+
krewrite[krewrite.length - 2] = BinaryParser.KREWRITE;
54+
krewrite[krewrite.length - 1] = BinaryParser.END;
55+
K result2 = BinaryParser.parse(krewrite);
56+
assertEquals(KRewrite(term, term), result2);
57+
}
58+
4159
@Test @Ignore
4260
public void testLarger() throws Exception {
4361
BinaryLoader loader = new BinaryLoader(new KExceptionManager(new GlobalOptions()));

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
// Copyright (c) 2015 K Team. All Rights Reserved.
12
package org.kframework.kore;
23

34
import scala.collection.immutable.List;

0 commit comments

Comments
 (0)