Fix regression in java backend (runtimeverification#102)

dwightguth · web-flow · commit 605c1e56f831 · 2018-06-21T12:11:58.000-05:00
* roll back using klabel key for map

* add test for regression
diff --git a/java-backend/src/main/java/org/kframework/backend/java/compile/KOREtoBackendKIL.java b/java-backend/src/main/java/org/kframework/backend/java/compile/KOREtoBackendKIL.java
@@ -152,7 +152,7 @@ public Term KApply1(org.kframework.kore.KLabel klabel, org.kframework.kore.KList
     private Optional<KLabel> getAssocKLabelForUnit(KLabel klabel) {
         return definition.kLabelAttributes().entrySet().stream()
                 .filter(e -> effectivelyAssocAttributes(e.getValue()) && e.getValue().get(Att.unit()).equals(klabel.name()))
-                .map(e -> e.getKey())
+                .map(e -> KORE.KLabel(e.getKey()))
                 .findAny();
     }
 
diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/Definition.java b/java-backend/src/main/java/org/kframework/backend/java/kil/Definition.java
@@ -53,15 +53,15 @@ private static class DefinitionData implements Serializable {
         public final Subsorts subsorts;
         public Map<String, DataStructureSort> dataStructureSorts;
         public final SetMultimap<String, SortSignature> signatures;
-        public final ImmutableMap<org.kframework.kore.KLabel, Att> kLabelAttributes;
+        public final ImmutableMap<String, Att> kLabelAttributes;
         public final Map<Sort, org.kframework.kore.KLabel> freshFunctionNames;
         public final Map<Sort, Sort> smtSortFlattening;
 
         private DefinitionData(
                 Subsorts subsorts,
                 Map<String, DataStructureSort> dataStructureSorts,
                 SetMultimap<String, SortSignature> signatures,
-                ImmutableMap<org.kframework.kore.KLabel, Att> kLabelAttributes,
+                ImmutableMap<String, Att> kLabelAttributes,
                 Map<Sort, org.kframework.kore.KLabel> freshFunctionNames,
                 Map<Sort, Sort> smtSortFlattening) {
             this.subsorts = subsorts;
@@ -119,9 +119,9 @@ public Definition(org.kframework.definition.Module module, KExceptionManager kem
             });
         });
 
-        ImmutableMap.Builder<org.kframework.kore.KLabel, Att> attributesBuilder = ImmutableMap.builder();
+        ImmutableMap.Builder<String, Att> attributesBuilder = ImmutableMap.builder();
         JavaConversions.mapAsJavaMap(module.attributesFor()).entrySet().stream().forEach(e -> {
-            attributesBuilder.put(e.getKey(), e.getValue());
+            attributesBuilder.put(e.getKey().name(), e.getValue());
         });
 
         definitionData = new DefinitionData(
@@ -346,12 +346,12 @@ public Set<SortSignature> signaturesOf(String label) {
         return definitionData.signatures.get(label);
     }
 
-    public Map<org.kframework.kore.KLabel, Att> kLabelAttributes() {
+    public Map<String, Att> kLabelAttributes() {
         return definitionData.kLabelAttributes;
     }
 
     public Att kLabelAttributesOf(org.kframework.kore.KLabel label) {
-        return Optional.ofNullable(definitionData.kLabelAttributes.get(label)).orElse(Att.empty());
+        return Optional.ofNullable(definitionData.kLabelAttributes.get(label.name())).orElse(Att.empty());
     }
 
     public DataStructureSort dataStructureSortOf(Sort sort) {
diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/BuiltinFunction.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/BuiltinFunction.java
@@ -9,6 +9,7 @@
 import org.kframework.backend.java.util.ImpureFunctionException;
 import org.kframework.kil.Attribute;
 import org.kframework.kore.KLabel;
+import org.kframework.kore.KORE;
 import org.kframework.utils.errorsystem.KEMException;
 import org.kframework.utils.errorsystem.KExceptionManager;
 
@@ -53,7 +54,7 @@ public BuiltinFunction(Definition definition, Map<String, MethodHandle> hookProv
         } catch (NoSuchMethodException | IllegalAccessException e) {
             throw KEMException.internalError("Failed to load partial evaluation hook implementation", e);
         }
-        for (Map.Entry<KLabel, Att> entry : definition.kLabelAttributes().entrySet()) {
+        for (Map.Entry<String, Att> entry : definition.kLabelAttributes().entrySet()) {
             String hookAttribute = entry.getValue().getOptional(Attribute.HOOK_KEY).orElse(null);
             if (hookAttribute != null) {
                 /*
@@ -72,7 +73,7 @@ public BuiltinFunction(Definition definition, Map<String, MethodHandle> hookProv
                     continue;
                 }
 
-                table.put(KLabelConstant.of(entry.getKey(), definition), hookProvider.get(hookAttribute));
+                table.put(KLabelConstant.of(KORE.KLabel(entry.getKey()), definition), hookProvider.get(hookAttribute));
             }
         }
     }
diff --git a/k-distribution/tests/regression-new/issue-101/1.test b/k-distribution/tests/regression-new/issue-101/1.test
@@ -0,0 +1 @@
+symbolicFoo
diff --git a/k-distribution/tests/regression-new/issue-101/1.test.out b/k-distribution/tests/regression-new/issue-101/1.test.out
@@ -0,0 +1,8 @@
+<TEST>
+  <s>
+    false
+  </s>
+  <k>
+    V0
+  </k>
+</TEST>
diff --git a/k-distribution/tests/regression-new/issue-101/Makefile b/k-distribution/tests/regression-new/issue-101/Makefile
@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_FLAGS=--backend java
+KRUN_FLAGS=-cSTRATEGY='^ F2B'
+
+include ../../../include/ktest.mak
diff --git a/k-distribution/tests/regression-new/issue-101/test.k b/k-distribution/tests/regression-new/issue-101/test.k
@@ -0,0 +1,20 @@
+// Copyright (c) 2018 K Team. All Rights Reserved.
+module TEST
+    imports DOMAINS
+    imports STRATEGY
+    imports BASIC-STRATEGY
+
+    configuration
+      <TEST>
+        <s/>
+        <k> $PGM:Foo </k>
+      </TEST>
+
+    syntax Foo ::= "symbolicFoo" [function]
+                 | "foo" | "bar"
+
+    rule <s> ~ S => . ... </s>
+    rule symbolicFoo => ?X:Foo
+    rule <k> foo => bar ... </k> [tag(F2B)]
+    rule <k> bar => foo ... </k> [tag(B2F)]
+endmodule

Original file line number	Diff line number	Diff line change
`@@ -152,7 +152,7 @@ public Term KApply1(org.kframework.kore.KLabel klabel, org.kframework.kore.KList`
`152`	`152`	`private Optional<KLabel> getAssocKLabelForUnit(KLabel klabel) {`
`153`	`153`	`return definition.kLabelAttributes().entrySet().stream()`
`154`	`154`	`.filter(e -> effectivelyAssocAttributes(e.getValue()) && e.getValue().get(Att.unit()).equals(klabel.name()))`
`155`		`- .map(e -> e.getKey())`
	`155`	`+ .map(e -> KORE.KLabel(e.getKey()))`
`156`	`156`	`.findAny();`
`157`	`157`	`}`
`158`	`158`
Original file line number	Diff line number	Diff line change
`@@ -9,6 +9,7 @@`
`9`	`9`	`import org.kframework.backend.java.util.ImpureFunctionException;`
`10`	`10`	`import org.kframework.kil.Attribute;`
`11`	`11`	`import org.kframework.kore.KLabel;`
	`12`	`+import org.kframework.kore.KORE;`
`12`	`13`	`import org.kframework.utils.errorsystem.KEMException;`
`13`	`14`	`import org.kframework.utils.errorsystem.KExceptionManager;`
`14`	`15`
`@@ -53,7 +54,7 @@ public BuiltinFunction(Definition definition, Map<String, MethodHandle> hookProv`
`53`	`54`	`} catch (NoSuchMethodException \| IllegalAccessException e) {`
`54`	`55`	`throw KEMException.internalError("Failed to load partial evaluation hook implementation", e);`
`55`	`56`	`}`
`56`		`- for (Map.Entry<KLabel, Att> entry : definition.kLabelAttributes().entrySet()) {`
	`57`	`+ for (Map.Entry<String, Att> entry : definition.kLabelAttributes().entrySet()) {`
`57`	`58`	`String hookAttribute = entry.getValue().getOptional(Attribute.HOOK_KEY).orElse(null);`
`58`	`59`	`if (hookAttribute != null) {`
`59`	`60`	`/*`
`@@ -72,7 +73,7 @@ public BuiltinFunction(Definition definition, Map<String, MethodHandle> hookProv`
`72`	`73`	`continue;`
`73`	`74`	`}`
`74`	`75`
`75`		`- table.put(KLabelConstant.of(entry.getKey(), definition), hookProvider.get(hookAttribute));`
	`76`	`+ table.put(KLabelConstant.of(KORE.KLabel(entry.getKey()), definition), hookProvider.get(hookAttribute));`
`76`	`77`	`}`
`77`	`78`	`}`
`78`	`79`	`}`
-Original file line number
+Diff line change
@@ @@ -0,0 +1,8 @@ @@
 +<TEST>
 +  <s>
 +    false
 +  </s>
 +  <k>
 +    V0
 +  </k>
 +</TEST>