Merge pull request #1403 from dwightguth/default

make PatternMatchRewriter the default Former-commit-id: 16bc03b2eead6d90603937195f52cf9b8f5ab683 [formerly fc7e3bd7a08e809ee5ca38103346896157863619] Former-commit-id: a7dd2482590f745327f5f478b7bd819fd8ea938c
runtimeverification · Mar 17, 2015 · 911ed5e · 911ed5e
2 parents 290d997 + a327be8
commit 911ed5e
Show file tree

Hide file tree

Showing 17 changed files with 274 additions and 48 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -28,6 +28,10 @@
   the class by dependency injection (i.e. via a 0-args or `@Inject`-annotated
   constructor)
 
+## Java Backend ##
+
+- Removed `--pattern-matching` flag and made this behavior the default. Added
+  `--symbolic-execution` flag, preserving old behavior.
 
 # K Framework 3.5 (released 2014-12-19) #
 

diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaExecutionOptions.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaExecutionOptions.java
@@ -14,9 +14,9 @@ public final class JavaExecutionOptions {
         + "execution in the java backend if function definitions are not deterministic.")
     public boolean deterministicFunctions = false;
 
-    @Parameter(names="--pattern-matching", description="Use pattern-matching rather than "
-        + "unification to drive rewriting in the Java backend.")
-    public boolean patternMatching = false;
+    @Parameter(names="--symbolic-execution", description="Use unification rather than "
+        + "pattern matching to drive rewriting in the Java backend.")
+    public boolean symbolicExecution = false;
 
     @Parameter(names="--rule-index", converter=RuleIndexConveter.class, description="Choose a technique for indexing the rules. <rule-index> is one of [table]. (Default: table). This only has effect with '--backend java'.")
     public IndexingAlgorithm ruleIndex = IndexingAlgorithm.RULE_TABLE;

diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaSymbolicExecutor.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaSymbolicExecutor.java
@@ -141,7 +141,7 @@ private RewriteRelation conventionalRewriteRun(ConstrainedTerm constrainedTerm,
     private RewriteRelation javaRewriteEngineRun(org.kframework.kil.Term cfg, int bound, boolean computeGraph) {
         Term term = getJavaKilTerm(cfg);
         TermContext termContext = getTermContext(term);
-        if (javaOptions.patternMatching) {
+        if (!javaOptions.symbolicExecution) {
             return patternMatcherRewriteRun(term, termContext, bound, computeGraph);
         }
         ConstrainedTerm constrainedTerm = new ConstrainedTerm(term, ConjunctiveFormula.of(termContext));
@@ -192,7 +192,7 @@ public SearchResults search(
         Term targetTerm = null;
         TermContext termContext = TermContext.of(globalContext);
         KRunGraph executionGraph = null;
-        if (javaOptions.patternMatching) {
+        if (!javaOptions.symbolicExecution) {
             if (computeGraph) {
                 KExceptionManager.criticalError("Compute Graph with Pattern Matching Not Implemented Yet");
             }

diff --git a/k-distribution/samples/agent/tests/config.xml b/k-distribution/samples/agent/tests/config.xml
@@ -10,20 +10,24 @@
       >
     <kompile-option name="--backend" value="java" />
     <all-programs>
+      <krun-option name="--symbolic-execution" />
       <krun-option name="--output" value="none" />
       <krun-option name="--color" value="off" />
     </all-programs>
     <program name="p17.agent">
+      <krun-option name="--symbolic-execution" />
       <krun-option name="--search" />
       <krun-option name="--bound" value="5" />
       <krun-option name="--pattern" value="&lt;out&gt; ListItem(#buffer(S:String)) &lt;/out&gt;" />
     </program>
     <program name="p22.agent">
+      <krun-option name="--symbolic-execution" />
       <krun-option name="--output" value="pretty" />
       <krun-option name="--search" />
       <krun-option name="--pattern" value="&lt;out&gt; ListItem(#buffer(S:String)) &lt;/out&gt;" />
     </program>
     <program name="p23.agent">
+      <krun-option name="--symbolic-execution" />
       <krun-option name="--output" value="pretty" />
       <krun-option name="--search" />
       <krun-option name="--pattern" value="&lt;out&gt; ListItem(#buffer(S:String)) &lt;/out&gt;" />

diff --git a/k-distribution/samples/kernelc/tests/config.xml b/k-distribution/samples/kernelc/tests/config.xml
@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<!-- Copyright (c) 2014 K Team. All Rights Reserved. -->
+<!-- Copyright (c) 2014-2015 K Team. All Rights Reserved. -->
 
 <tests>
     <test
@@ -10,11 +10,9 @@
             >
         <kompile-option name="--backend" value="java" />
         <all-programs>
-            <krun-option name="--pattern-matching" />
             <krun-option name="--output" value="none" />
         </all-programs>
         <program name="undefined.c">
-          <krun-option name="--pattern-matching" />
           <krun-option name="--output" value="pretty" />
         </program>
     </test>

diff --git a/k-distribution/tests/regression/java-rewrite-engine/config.xml b/k-distribution/tests/regression/java-rewrite-engine/config.xml
@@ -92,6 +92,7 @@
       >
     <kompile-option name="--backend" value="java" />
     <all-programs>
+      <krun-option name="--symbolic-execution" />
       <krun-option name="--smt" value="none" />
       <krun-option name="--output" value="pretty" />
     </all-programs>