Verification (runtimeverification#683)

daejunpark · dwightguth · commit 9c115caf104a · 2018-02-07T16:41:23.000-06:00
* correct in_keys 92606afa52040f93691a55d93ef1402bc4b2795c

* for better debugging: add original name when renaming variable

* add hook KREFLECTION.isConcrete

* Cache function/anywhere symbol evaluation

* fix top constraint

* context.setTopConstraint after constraint.orientSubstitution in buildResult

* add #isConcrete to domains.k

* add isConcrete hook to prelude.ml, simply returning true

* fix hook_isConcrete in prelude.ml

* DefinitionParsing.java: fix auto-generated $SYNTAX module loading

* fix compile error in prelude.ml
diff --git a/java-backend/src/main/java/org/kframework/backend/java/builtins/BuiltinMapOperations.java b/java-backend/src/main/java/org/kframework/backend/java/builtins/BuiltinMapOperations.java
@@ -174,7 +174,17 @@ public static BuiltinSet keys(BuiltinMap map, TermContext context) {
     }
 
     public static BoolToken in_keys(Term key, BuiltinMap map, TermContext context) {
-        return BoolToken.of(map.getEntries().containsKey(key));
+        boolean in = map.getEntries().containsKey(key);
+        BoolToken r = BoolToken.of(in);
+        if (in) {
+            return r;
+        } else if (key.isGround() && map.isConcreteCollection() && map.hasOnlyGroundKeys()) {
+            return r;
+        } else if (map.isEmpty()) {
+            return r;
+        } else {
+            return null;
+        }
     }
 
     public static Term values(BuiltinMap map, TermContext context) {
diff --git a/java-backend/src/main/java/org/kframework/backend/java/builtins/MetaK.java b/java-backend/src/main/java/org/kframework/backend/java/builtins/MetaK.java
@@ -202,4 +202,8 @@ public static Term configuration(TermContext context) {
         //return KLabelInjection.injectionOf(context.getTopTerm(), context.global());
         return context.getTopTerm();
     }
+
+    public static BoolToken isConcrete(Term term, TermContext context) {
+        return BoolToken.of(term.isConcrete());
+    }
 }
diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/ConstrainedTerm.java b/java-backend/src/main/java/org/kframework/backend/java/kil/ConstrainedTerm.java
@@ -163,6 +163,7 @@ public ConjunctiveFormula matchImplies(ConstrainedTerm constrainedTerm, boolean
             return null;
         }
 
+        context.setTopConstraint(null);
         return data.constraint.addAndSimplify(constraint, context);
     }
 
@@ -221,7 +222,10 @@ public static List<Triple<ConjunctiveFormula, Boolean, Map<scala.collection.immu
             Pair<Map<scala.collection.immutable.List<Pair<Integer, Integer>>, Term>, ConjunctiveFormula> pair = ConstrainedTerm.splitRewrites(candidate);
             ConjunctiveFormula candidateConstraint = pair.getRight();
 
+            context.setTopConstraint(null);
             ConjunctiveFormula solution = candidateConstraint.addAndSimplify(subjectConstraint, context);
+            context.setTopConstraint(subjectConstraint);
+
             if (solution.isFalse()) {
                 continue;
             }
@@ -248,10 +252,12 @@ public static List<Triple<ConjunctiveFormula, Boolean, Map<scala.collection.immu
             if (candidate.substitution().keySet().equals(variables)
                     && !candidate.isSubstitution()
                     && subjectConstraint.implies(ConjunctiveFormula.of(context.global()).addAll(candidateConstraint.equalities()), Sets.newHashSet())) {
+                context.setTopConstraint(null);
                 solutions.add(Triple.of(
                         subjectConstraint.addAndSimplify(candidateConstraint.substitution(), context),
                         true,
                         pair.getLeft()));
+                context.setTopConstraint(subjectConstraint);
             } else {
                 solutions.add(Triple.of(solution, isMatching, pair.getLeft()));
             }
diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/JavaSymbolicObject.java b/java-backend/src/main/java/org/kframework/backend/java/kil/JavaSymbolicObject.java
@@ -2,10 +2,12 @@
 
 package org.kframework.backend.java.kil;
 
+import com.google.common.collect.Sets;
 import org.kframework.attributes.Att;
 import org.kframework.attributes.Location;
 import org.kframework.attributes.Source;
 import org.kframework.backend.java.symbolic.BinderSubstitutionTransformer;
+import org.kframework.backend.java.symbolic.ConjunctiveFormula;
 import org.kframework.backend.java.symbolic.IncrementalCollector;
 import org.kframework.backend.java.symbolic.LocalVisitor;
 import org.kframework.backend.java.symbolic.SubstitutionTransformer;
@@ -46,6 +48,7 @@ public abstract class JavaSymbolicObject<T extends JavaSymbolicObject<T>>
     volatile transient PSet<Variable> variableSet = null;
     volatile transient Boolean isGround = null;
     volatile transient Boolean isNormal = null;
+    volatile transient Set<ConjunctiveFormula> isEvaluated = Sets.newHashSet();
     volatile transient Set<Term> userVariableSet = null;
 
     private Att att;
@@ -102,8 +105,8 @@ public T renameVariables() {
     /**
      * Returns true if a call to {@link org.kframework.backend.java.kil.Term#substituteAndEvaluate(java.util.Map, TermContext)} may simplify this term.
      */
-    public boolean canSubstituteAndEvaluate(Map<Variable, ? extends Term> substitution) {
-        return (!substitution.isEmpty() && !isGround()) || !isNormal();
+    public boolean canSubstituteAndEvaluate(Map<Variable, ? extends Term> substitution, ConjunctiveFormula constraint) {
+        return !Sets.intersection(substitution.keySet(), variableSet()).isEmpty() || !isEvaluated(constraint);
     }
 
     /**
@@ -146,6 +149,19 @@ public boolean isNormal() {
         return isNormal;
     }
 
+    public boolean isConcrete() {
+        return isGround() && isNormal();
+    }
+
+     /**
+     * Returns true if the function and anywhere symbols in this
+     * {@code JavaSymbolicObject} have been evaluated under the given
+     * {@code ConjunctiveFormula}, false otherwise.
+     */
+    public boolean isEvaluated(ConjunctiveFormula constraint) {
+        return isEvaluated.contains(constraint);
+    }
+
     /**
      * Returns a {@code Set} view of the user variables (ie terms of sort Variable) in this
      * {@code JavaSymbolicObject}.
diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/KItem.java b/java-backend/src/main/java/org/kframework/backend/java/kil/KItem.java
@@ -271,11 +271,15 @@ public boolean isEvaluable() {
     }
 
     public Term evaluateFunction(TermContext context) {
-        return global.kItemOps.evaluateFunction(this, context);
+        Term result = global.kItemOps.evaluateFunction(this, context);
+        result.isEvaluated.add(context.getTopConstraint());
+        return result;
     }
 
     public Term resolveFunctionAndAnywhere(TermContext context) {
-        return global.kItemOps.resolveFunctionAndAnywhere(this, context);
+        Term result = global.kItemOps.resolveFunctionAndAnywhere(this, context);
+        result.isEvaluated.add(context.getTopConstraint());
+        return result;
     }
 
     @Override
diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/Term.java b/java-backend/src/main/java/org/kframework/backend/java/kil/Term.java
@@ -77,7 +77,7 @@ public Term evaluate(TermContext context) {
      * {@code evaluate} method instead.
      */
     public Term substituteAndEvaluate(Map<Variable, ? extends Term> substitution, TermContext context) {
-        return canSubstituteAndEvaluate(substitution) ?
+        return canSubstituteAndEvaluate(substitution, context.getTopConstraint()) ?
                (Term) this.accept(new SubstituteAndEvaluateTransformer(substitution, context)) :
                this;
     }
diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/Variable.java b/java-backend/src/main/java/org/kframework/backend/java/kil/Variable.java
@@ -62,6 +62,7 @@ public static Variable getAnonVariable(Sort sort) {
     }
 
     /* TODO(AndreiS): cache the variables */
+    private String originalName = "";
     private final String name;
     private final Sort sort;
     private final boolean anonymous;
@@ -109,6 +110,7 @@ public Variable(MetaVariable metaVariable) {
     public Variable getFreshCopy() {
         Variable var = Variable.getAnonVariable(sort);
         var.copyAttributesFrom(this);
+        var.originalName = this.name;
         return var;
     }
 
@@ -172,7 +174,7 @@ protected final int computeHash() {
 
     @Override
     public String toString() {
-        return name + ":" + sort;
+        return originalName + name + ":" + sort;
     }
 
     @Override
diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/SubstituteAndEvaluateTransformer.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/SubstituteAndEvaluateTransformer.java
@@ -37,7 +37,7 @@ public SubstituteAndEvaluateTransformer(Map<Variable, ? extends Term> substituti
     }
 
     protected boolean proceed(JavaSymbolicObject object) {
-        return object.canSubstituteAndEvaluate(substitution);
+        return object.canSubstituteAndEvaluate(substitution, context.getTopConstraint());
     }
 
     @Override
diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java
@@ -186,6 +186,8 @@ public List<ConstrainedTerm> fastComputeRewriteStep(ConstrainedTerm subject, boo
                 theNew = theNew.substituteAndEvaluate(substitution, subject.termContext());
             }
 
+            subject.termContext().setTopConstraint(null);
+
             theNew = restoreConfigurationIfNecessary(subject, rule, theNew);
 
             /* eliminate bindings of the substituted variables */
@@ -369,10 +371,11 @@ public static ConstrainedTerm buildResult(
 
 
         /* apply the constraints substitution on the rule RHS */
-        context.setTopConstraint(constraint);
         Set<Variable> substitutedVars = Sets.union(rule.freshConstants(), rule.matchingVariables());
         constraint = constraint.orientSubstitution(substitutedVars);
+        context.setTopConstraint(constraint);
         Term term = rule.rightHandSide().substituteAndEvaluate(constraint.substitution(), context);
+        context.setTopConstraint(null);
 
         /* eliminate bindings of the substituted variables */
         constraint = constraint.removeBindings(substitutedVars);
diff --git a/java-backend/src/main/resources/org/kframework/backend/java/symbolic/hooks.properties b/java-backend/src/main/resources/org/kframework/backend/java/symbolic/hooks.properties
@@ -172,6 +172,7 @@ UNIFICATION.freezeVariables : org.kframework.backend.java.builtins.MetaK.freezeV
 UNIFICATION.unifiable : org.kframework.backend.java.builtins.MetaK.unifiable
 KREFLECTION.getKLabel : org.kframework.backend.java.builtins.MetaK.getKLabel
 KREFLECTION.configuration : org.kframework.backend.java.builtins.MetaK.configuration
+KREFLECTION.isConcrete : org.kframework.backend.java.builtins.MetaK.isConcrete
 
 # unification hooks
 # TODO: unimplemented
diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k
@@ -620,6 +620,7 @@ module K-REFLECTION
   syntax String ::= #sort(K) [function, hook(KREFLECTION.sort)]
   syntax KItem ::= #fresh(String)   [function, hook(KREFLECTION.fresh), impure]
   syntax KItem ::= getKLabel(K)  [function, hook(KREFLECTION.getKLabel)]
+  syntax Bool ::= #isConcrete(K) [function, hook(KREFLECTION.isConcrete)]
 
   syntax String ::= #getenv(String) [function, impure, hook(KREFLECTION.getenv)]
 
diff --git a/k-distribution/include/ocaml/prelude.ml b/k-distribution/include/ocaml/prelude.ml
@@ -536,6 +536,7 @@ struct
   let hook_fresh c _ _ config ff = match c with
       [String sort] -> let res = ff sort config !freshCounter in freshCounter := Z.add !freshCounter Z.one; res
     | _ -> raise Not_implemented
+  let hook_isConcrete _ _ _ _ _ = [Bool true]
   let hook_getenv c _ _ _ _ = match c with
       [String key] -> [String (Sys.getenv key)]
     | _ -> raise Not_implemented
diff --git a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java
@@ -99,6 +99,8 @@ public Module parseModule(CompiledDefinition definition, File definitionFile, bo
                 autoImportDomains,
                 new HashSet<>());
 
+        modules = modules.stream().filter(m -> !m.name().endsWith("$SYNTAX")).collect(Collectors.toSet());
+
         if (modules.size() != 1) {
             throw KEMException.compilerError("Expected to find a file with 1 module: found " + modules.size() + " instead.");
         }

Original file line number	Diff line number	Diff line change
`@@ -202,4 +202,8 @@ public static Term configuration(TermContext context) {`
`202`	`202`	`//return KLabelInjection.injectionOf(context.getTopTerm(), context.global());`
`203`	`203`	`return context.getTopTerm();`
`204`	`204`	`}`
	`205`	`+`
	`206`	`+ public static BoolToken isConcrete(Term term, TermContext context) {`
	`207`	`+ return BoolToken.of(term.isConcrete());`
	`208`	`+ }`
`205`	`209`	`}`
Original file line number	Diff line number	Diff line change
`@@ -271,11 +271,15 @@ public boolean isEvaluable() {`
`271`	`271`	`}`
`272`	`272`
`273`	`273`	`public Term evaluateFunction(TermContext context) {`
`274`		`- return global.kItemOps.evaluateFunction(this, context);`
	`274`	`+ Term result = global.kItemOps.evaluateFunction(this, context);`
	`275`	`+ result.isEvaluated.add(context.getTopConstraint());`
	`276`	`+ return result;`
`275`	`277`	`}`
`276`	`278`
`277`	`279`	`public Term resolveFunctionAndAnywhere(TermContext context) {`
`278`		`- return global.kItemOps.resolveFunctionAndAnywhere(this, context);`
	`280`	`+ Term result = global.kItemOps.resolveFunctionAndAnywhere(this, context);`
	`281`	`+ result.isEvaluated.add(context.getTopConstraint());`
	`282`	`+ return result;`
`279`	`283`	`}`
`280`	`284`
`281`	`285`	`@Override`
Original file line number	Diff line number	Diff line change
`@@ -77,7 +77,7 @@ public Term evaluate(TermContext context) {`
`77`	`77`	`* {@code evaluate} method instead.`
`78`	`78`	`*/`
`79`	`79`	`public Term substituteAndEvaluate(Map<Variable, ? extends Term> substitution, TermContext context) {`
`80`		`- return canSubstituteAndEvaluate(substitution) ?`
	`80`	`+ return canSubstituteAndEvaluate(substitution, context.getTopConstraint()) ?`
`81`	`81`	`(Term) this.accept(new SubstituteAndEvaluateTransformer(substitution, context)) :`
`82`	`82`	`this;`
`83`	`83`	`}`
Original file line number	Diff line number	Diff line change
`@@ -62,6 +62,7 @@ public static Variable getAnonVariable(Sort sort) {`
`62`	`62`	`}`
`63`	`63`
`64`	`64`	`/* TODO(AndreiS): cache the variables */`
	`65`	`+ private String originalName = "";`
`65`	`66`	`private final String name;`
`66`	`67`	`private final Sort sort;`
`67`	`68`	`private final boolean anonymous;`
`@@ -109,6 +110,7 @@ public Variable(MetaVariable metaVariable) {`
`109`	`110`	`public Variable getFreshCopy() {`
`110`	`111`	`Variable var = Variable.getAnonVariable(sort);`
`111`	`112`	`var.copyAttributesFrom(this);`
	`113`	`+ var.originalName = this.name;`
`112`	`114`	`return var;`
`113`	`115`	`}`
`114`	`116`
`@@ -172,7 +174,7 @@ protected final int computeHash() {`
`172`	`174`
`173`	`175`	`@Override`
`174`	`176`	`public String toString() {`
`175`		`- return name + ":" + sort;`
	`177`	`+ return originalName + name + ":" + sort;`
`176`	`178`	`}`
`177`	`179`
`178`	`180`	`@Override`
Original file line number	Diff line number	Diff line change
`@@ -37,7 +37,7 @@ public SubstituteAndEvaluateTransformer(Map<Variable, ? extends Term> substituti`
`37`	`37`	`}`
`38`	`38`
`39`	`39`	`protected boolean proceed(JavaSymbolicObject object) {`
`40`		`- return object.canSubstituteAndEvaluate(substitution);`
	`40`	`+ return object.canSubstituteAndEvaluate(substitution, context.getTopConstraint());`
`41`	`41`	`}`
`42`	`42`
`43`	`43`	`@Override`