Build Haskell backend as a submodule, hook into Maven (runtimeverific…

…ation#228)

* .gitmodule, haskell-backend/.../native/haskell-backend: add haskell-backend submodule

* haskell-backend/pom.xml: build haskell backend with mvn compile

* pom.xml: exclude haskell backend from checkstyle target

* haskell-backend/pom.xml, k-distribution/.../assembly/bin.xml: gather kore binaries for distribution

* README: instructions for installing Haskell Stack

* haskell-backend/pom.xml: remove unneeded project build type

* k-distribution/.../Makefile: parameterize tests in KOMPILE_BACKEND

* k-distribution/.../regression-new/imp-haskell: run IMP tests with Haskell backend

* haskell-backend/pom.xml: allow skipping Haskell backend with -Dhaskell.backend.skip

* kernel/.../GeneratedTopFormat: fix copyright

.gitmodules

@@ -1,3 +1,8 @@
 [submodule "llvm-backend/src/main/native/llvm-backend"]
 	path = llvm-backend/src/main/native/llvm-backend
 	url = https://github.com/kframework/llvm-backend
+	ignore = untracked
+[submodule "haskell-backend/src/main/native/haskell-backend"]
+	path = haskell-backend/src/main/native/haskell-backend
+	url = https://github.com/kframework/kore
+	ignore = untracked

README.md

@@ -14,7 +14,6 @@ source $HOME/.cargo/env
 rustup toolchain install 1.28.0
 rustup default 1.28.0
 curl -sSL https://get.haskellstack.org/ | sh
-
 ```
 
 If you install this list of dependencies, continue directly to the Install section.
@@ -62,9 +61,9 @@ rustup default 1.28.0
 
 ## Haskell Stack
 
-To install, go to https://docs.haskellstack.org/en/stable/README/ and follow the instructions.
+To install, go to <https://docs.haskellstack.org/en/stable/README/> and follow the instructions.
+You may need to do `stack upgrade` to ensure the latest version of Haskell Stack.
 
-
 ## Miscellaneous
 
 Also required:

haskell-backend/pom.xml

@@ -34,6 +34,33 @@
         <artifactId>maven-surefire-plugin</artifactId>
         <version>2.17</version>
       </plugin>
+      <plugin>
+        <artifactId>maven-antrun-plugin</artifactId>
+        <version>1.7</version>
+        <executions>
+          <execution>
+            <id>build-haskell</id>
+            <phase>compile</phase>
+            <configuration>
+              <skip>${haskell.backend.skip}</skip>
+              <target>
+                <exec executable="stack" dir="${project.basedir}/src/main/native/haskell-backend" failonerror="true">
+                  <arg value="build" />
+                </exec>
+                <mkdir dir="${project.build.directory}/stack-install" />
+                <exec executable="stack" dir="${project.basedir}/src/main/native/haskell-backend" failonerror="true">
+                  <arg value="install" />
+                  <arg value="--local-bin-path" />
+                  <arg value="${project.build.directory}/stack-install" />
+                </exec>
+              </target>
+            </configuration>
+            <goals>
+              <goal>run</goal>
+            </goals>
+          </execution>
+        </executions>
+      </plugin>
     </plugins>
   </build>
 </project>

k-distribution/include/ktest-keq.mak

@@ -2,6 +2,7 @@
 MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
 # path to the kompile binary of this distribuition
 KOMPILE=$(abspath $(MAKEFILE_PATH)/../bin/kompile)
+KOMPILE_BACKEND=java
 # ditto for keq
 KEQ=$(abspath $(MAKEFILE_PATH)/../bin/keq)
 
@@ -16,11 +17,11 @@ all: kompile keq
 kompile: $(DEF1)/$(DEF1)-kompiled/timestamp $(DEF2)/$(DEF2)-kompiled/timestamp $(DEF0)/$(DEF0)-kompiled/timestamp
 
 $(DEF0)/$(DEF0)-kompiled/timestamp: $(DEF0).k
-	$(KOMPILE) $< -d $(DEF0) --backend java
+	$(KOMPILE) $< -d $(DEF0) --backend $(KOMPILE_BACKEND)
 $(DEF1)/$(DEF1)-kompiled/timestamp: $(DEF1).k
-	$(KOMPILE) $< -d $(DEF1) --backend java
+	$(KOMPILE) $< -d $(DEF1) --backend $(KOMPILE_BACKEND)
 $(DEF2)/$(DEF2)-kompiled/timestamp: $(DEF2).k
-	$(KOMPILE) $< -d $(DEF2) --backend java
+	$(KOMPILE) $< -d $(DEF2) --backend $(KOMPILE_BACKEND)
 
 keq: $(SPEC1) $(SPEC2) kompile
 	$(KEQ) -d $(DEF0) -d1 $(DEF1) -d2 $(DEF2) -s1 $(SPEC1) -s2 $(SPEC2) -sm1 $(MODULE1) -sm2 $(MODULE2) --smt_prelude $(BASIC_SMT)

k-distribution/include/ktest.mak

@@ -17,6 +17,8 @@ RESULTDIR?=$(TESTDIR)
 # all tests in test directory with matching file extension
 TESTS?=$(wildcard $(TESTDIR)/*.$(EXT))
 PROOF_TESTS?=$(wildcard $(TESTDIR)/*-spec.k)
+# default KOMPILE_BACKEND
+KOMPILE_BACKEND?=ocaml
 
 CHECK=| diff -
 
@@ -29,7 +31,7 @@ all: kompile krun proofs
 kompile: $(DEFDIR)/$(DEF)-kompiled/timestamp
 
 $(DEFDIR)/%-kompiled/timestamp: %.k
-	$(KOMPILE) $(KOMPILE_FLAGS) $(DEBUG) $< -d $(DEFDIR)
+	$(KOMPILE) $(KOMPILE_FLAGS) --backend $(KOMPILE_BACKEND) $(DEBUG) $< -d $(DEFDIR)
 krun: $(TESTS)
 
 proofs: $(PROOF_TESTS)

k-distribution/src/main/assembly/bin.xml

@@ -72,5 +72,11 @@
       <directory>${project.basedir}/../llvm-backend/target/build/install/include</directory>
       <outputDirectory>/include</outputDirectory>
     </fileSet>
+    <fileSet>
+      <directory>${project.basedir}/../haskell-backend/target/stack-install</directory>
+      <outputDirectory>/bin</outputDirectory>
+      <fileMode>775</fileMode>
+      <directoryMode>775</directoryMode>
+    </fileSet>
   </fileSets>
 </assembly>

k-distribution/tests/builtins/collections/Makefile

@@ -1,6 +1,6 @@
 DEF=collections-test
 EXT=col
 TESTDIR=.
-KOMPILE_FLAGS=--backend java
+KOMPILE_BACKEND?=java
 
 include ../../../include/ktest.mak

k-distribution/tests/regression-new/Makefile

@@ -1,3 +1,3 @@
-SUBDIRS=issue-2273 concrete-function cell_map string_escape imp-kore poly-sort bit-range bit-range-ocaml cell-sort fresh1 fresh2 proj-attribute matching-attribute smt-prelude-attribute is-variable no-dup-rules
+SUBDIRS=issue-2273 concrete-function cell_map string_escape imp-kore poly-sort bit-range bit-range-ocaml cell-sort fresh1 fresh2 proj-attribute matching-attribute smt-prelude-attribute is-variable no-dup-rules imp-haskell
 
 include ../../include/ktest-group.mak

k-distribution/tests/regression-new/bit-range/Makefile

@@ -1,6 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--backend java
+KOMPILE_BACKEND?=java
 
 include ../../../include/ktest.mak

k-distribution/tests/regression-new/bytes/Makefile

@@ -1,6 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--backend java
+KOMPILE_BACKEND?=java
 
 include ../../../include/ktest.mak

k-distribution/tests/regression-new/cell-sort/Makefile

@@ -1,6 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--backend java
+KOMPILE_BACKEND?=java
 
 include ../../../include/ktest.mak

k-distribution/tests/regression-new/cell_map/Makefile

@@ -1,6 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--backend java
+KOMPILE_BACKEND?=java
 
 include ../../../include/ktest.mak

k-distribution/tests/regression-new/concrete-function/Makefile

@@ -1,6 +1,6 @@
 DEF=a
 EXT=a
-KOMPILE_FLAGS=--backend java
+KOMPILE_BACKEND=java
 TESTDIR=.
 
 include ../../../include/ktest.mak

k-distribution/tests/regression-new/float-id/Makefile

@@ -1,6 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--backend java
+KOMPILE_BACKEND?=java
 
 include ../../../include/ktest.mak

k-distribution/tests/regression-new/fresh1/Makefile

@@ -1,6 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--backend kore
+KOMPILE_BACKEND?=kore
 
 include ../../../include/ktest.mak

k-distribution/tests/regression-new/fresh2/Makefile

@@ -1,6 +1,6 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--backend kore
+KOMPILE_BACKEND?=kore
 
 include ../../../include/ktest.mak

k-distribution/tests/regression-new/imp-haskell/Makefile

@@ -0,0 +1,7 @@
+DEF=imp
+EXT=imp
+TESTDIR=.
+KOMPILE_BACKEND=haskell
+export KOMPILE_BACKEND
+
+include ../../../include/ktest.mak

k-distribution/tests/regression-new/imp-haskell/collatz.imp

@@ -0,0 +1,19 @@
+// This program tests the Collatz conjecture for all numbers up to m
+// and accumulates the total number of steps in s.
+
+int m, n, q, r, s;
+m = 10;
+while (!(m<=2)) {
+  n = m;
+  m = m + -1;
+  while (!(n<=1)) {
+    s = s+1;
+    q = n/2;
+    r = q+q+1;
+    if (r<=n) {
+      n = n+n+n+1;         // n becomes 3*n+1 if odd
+    } else {n=q;}          //        or   n/2 if even
+  }
+}
+
+// s should be 66 when m is 10

k-distribution/tests/regression-new/imp-haskell/collatz.imp.out

@@ -0,0 +1,12 @@
+<T>
+  <k>
+    .
+  </k>
+  <state>
+    m |-> 2
+    n |-> 1
+    q |-> 1
+    r |-> 3
+    s |-> 66
+  </state>
+</T>

k-distribution/tests/regression-new/imp-haskell/imp.k

@@ -0,0 +1,66 @@
+// Copyright (c) 2014-2019 K Team. All Rights Reserved.
+
+module IMP-SYNTAX
+  imports DOMAINS-SYNTAX
+
+  syntax AExp  ::= Int | Id
+                 | "-" Int                    [format(%1%2)]
+                 | AExp "/" AExp              [left, strict, color(pink)]
+                 > AExp "+" AExp              [left, strict, color(pink)]
+                 | "(" AExp ")"               [bracket]
+  syntax BExp  ::= Bool
+                 | AExp "<=" AExp             [seqstrict, latex({#1}\leq{#2}), color(pink)]
+                 | "!" BExp                   [strict, color(pink)]
+                 > BExp "&&" BExp             [left, strict(1), color(pink)]
+                 | "(" BExp ")"               [bracket]
+  syntax Block ::= "{" "}"
+                 | "{" Stmt "}"               [format(%1%i%n%2%d%n%3)]
+  syntax Stmt  ::= Block
+                 | Id "=" AExp ";"            [strict(2), color(pink), format(%1 %2 %3%4)]
+                 | "if" "(" BExp ")"
+                   Block "else" Block         [strict(1), colors(yellow, white, white, yellow), format(%1 %2%3%4 %5 %6 %7)]
+                 | "while" "(" BExp ")" Block [colors(yellow,white,white), format(%1 %2%3%4 %5)]
+                 > Stmt Stmt                  [left, format(%1%n%2)]
+
+  syntax Pgm ::= "int" Ids ";" Stmt           [format(%1 %2%3%n%4), colors(yellow,pink)]
+  syntax Ids ::= List{Id,","} [format(%1%2 %3)]
+endmodule
+
+module IMP
+  imports IMP-SYNTAX
+  imports DOMAINS
+
+  syntax KResult ::= Int | Bool
+
+  configuration <T color="yellow">
+                  <k color="green"> $PGM:Pgm </k>
+                  <state color="red"> .Map </state>
+                </T>
+
+  rule <k> X:Id => I ...</k> <state>... X |-> I ...</state>
+
+  rule I1 / I2 => I1 /Int I2  requires I2 =/=Int 0
+  rule I1 + I2 => I1 +Int I2
+  rule - I1 => 0 -Int I1
+
+  rule I1 <= I2 => I1 <=Int I2
+  rule ! T => notBool T
+  rule true && B => B
+  rule false && _ => false
+
+  rule {} => .   [structural]
+  rule {S} => S  [structural]
+
+  rule <k> X = I:Int; => . ...</k> <state>... X |-> (_ => I) ...</state>
+
+  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+
+  rule if (true)  S else _ => S
+  rule if (false) _ else S => S
+
+  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+
+  rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
+    requires notBool (X in keys(Rho))
+  rule int .Ids; S => S  [structural]
+endmodule

k-distribution/tests/regression-new/imp-haskell/primes.imp

@@ -0,0 +1,26 @@
+// This program counts in s all the prime numbers up to m.
+
+int i, m, n, q, r, s, t, x, y, z;
+m = 10;  n = 2;
+while (n <= m) {
+  // checking primality of n and writing t to 1 or 0
+  i = 2;  q = n/i;  t = 1;
+  while (i<=q && 1<=t) {
+    x = i;
+    y = q;
+    // fast multiplication (base 2) algorithm
+    z = 0;
+    while (!(x <= 0)) {
+      q = x/2;
+      r = q+q+1;
+      if (r <= x) { z = z+y; } else {}
+      x = q;
+      y = y+y;
+    } // end fast multiplication
+    if (n <= z) { t = 0; } else { i = i+1;  q = n/i; }
+  } // end checking primality
+  if (1 <= t) { s = s+1; } else {}
+  n = n+1;
+}
+
+// s should be 4 when m = 10.

k-distribution/tests/regression-new/imp-haskell/primes.imp.out

@@ -0,0 +1,17 @@
+<T>
+  <k>
+    .
+  </k>
+  <state>
+    i |-> 2
+    m |-> 10
+    n |-> 11
+    q |-> 0
+    r |-> 1
+    s |-> 4
+    t |-> 0
+    x |-> 0
+    y |-> 20
+    z |-> 10
+  </state>
+</T>

k-distribution/tests/regression-new/imp-haskell/sum.imp

@@ -0,0 +1,12 @@
+// This program calculates in sum
+// the sum of numbers from 1 to n.
+
+int n, sum;
+n = 100;
+sum = 0;
+while (!(n <= 0)) {
+  sum = sum + n;
+  n = n + -1;
+}
+
+// sum should be 5050 when n is 100

k-distribution/tests/regression-new/imp-haskell/sum.imp.out

@@ -0,0 +1,9 @@
+<T>
+  <k>
+    .
+  </k>
+  <state>
+    n |-> 0
+    sum |-> 5050
+  </state>
+</T>

k-distribution/tests/regression-new/imp-kore/Makefile

@@ -1,6 +1,6 @@
 DEF=imp
 EXT=imp
 TESTDIR=.
-KOMPILE_FLAGS=--backend kore
+KOMPILE_BACKEND?=kore
 
 include ../../../include/ktest.mak

k-distribution/tests/regression-new/is-variable/Makefile

@@ -1,6 +1,7 @@
 DEF=a
 EXT=a
-KOMPILE_FLAGS=--backend java --syntax-module A
+KOMPILE_FLAGS=--syntax-module A
+KOMPILE_BACKEND?=java
 
 TESTDIR=.
 

k-distribution/tests/regression-new/issue-101/Makefile

@@ -1,7 +1,7 @@
 DEF=test
 EXT=test
 TESTDIR=.
-KOMPILE_FLAGS=--backend java
+KOMPILE_BACKEND?=java
 KRUN_FLAGS=-cSTRATEGY='^ F2B'
 
 include ../../../include/ktest.mak