Merge master into fix-22-aklenikreview

smart-contract/hyperledger-fabric/v2/java/Dockerfile

@@ -6,6 +6,7 @@ COPY buildSrc/ buildSrc/
 COPY build.gradle.kts ./ 
 COPY gradle.properties ./
 COPY specs/ ./specs/
+COPY libs/ ./libs/
 
 RUN gradle --no-daemon shadowJar
 

smart-contract/hyperledger-fabric/v2/java/README.md

@@ -15,6 +15,16 @@ However, note that normally, you do not need to locally build the chaincode.
 The [test network](../../../../test-network/README.adoc) will build generate this JAR as part of a [dockerized](https://www.docker.com/) build process.
 Build directly only if you know what you are doing.
 
+## Development
+
+You most likely do not want to build with OpenJML for local development, eg in your IDE.
+To disable OpenJML, simply set the `withoutOpenJML` Gradle property to `true`.
+For example, in `gradle.properties`:
+
+```properties
+withoutOpenJML = "true"
+```
+
 
 ## License
 

smart-contract/hyperledger-fabric/v2/java/build.gradle.kts

@@ -1,9 +1,8 @@
 /* Originally based on https://github.com/mingyang91/openjml-template */
 
-import com.diffplug.gradle.spotless.SpotlessExtension
 import com.github.jengelman.gradle.plugins.shadow.tasks.ShadowJar
 import hu.bme.mit.ftsrg.openjmlhelper.*
-import java.io.File
+import org.gradle.api.tasks.testing.logging.TestLogEvent
 
 val openJMLDir = layout.projectDirectory.dir(".openjml")
 val openJMLJavaHomeDir = openJMLDir.dir("jdk")
@@ -12,13 +11,18 @@ val downloadDir = layout.buildDirectory.dir("tmp/download")
 val jmlavac = openJMLJavaHomeDir.file("bin/jmlavac")
 val jmlava = openJMLJavaHomeDir.file("bin/jmlava")
 
+val withoutOpenJML: String? by project
+val noOpenJML: Boolean = withoutOpenJML != null && withoutOpenJML.toBoolean()
+
 plugins {
   application
   id("com.github.johnrengelman.shadow") version "7.1.2"
   id("com.diffplug.spotless") version "6.19.0"
 }
 
-group = "hu.bme.mit.ftsrg.tpcc"
+// java { toolchain { languageVersion.set(JavaLanguageVersion.of(17) } }
+
+group = "hu.bme.mit.ftsrg.chaincode.tpcc"
 
 version = "0.1.0"
 
@@ -28,7 +32,9 @@ repositories {
 }
 
 dependencies {
-  implementation("ch.qos.logback:logback-classic:1.4.8")
+  implementation("ch.qos.logback:logback-core:1.5.6")
+  implementation("ch.qos.logback:logback-classic:1.5.6")
+  implementation("org.slf4j:slf4j-api:2.0.13")
   implementation("com.google.code.gson:gson:2.10.1")
   implementation("com.jcabi:jcabi-aspects:0.25.1")
   implementation("org.aspectj:aspectjrt:1.9.19")
@@ -37,6 +43,7 @@ dependencies {
   implementation("org.hyperledger.fabric:fabric-protos:0.3.0")
   implementation("org.json:json:20230227")
   implementation("org.projectlombok:lombok:1.18.28")
+  implementation(files("libs/hypernate-0.1.0.jar"))
   // Included also as implementation dependency so shadow will package it
   implementation(files("$openJMLDir/jmlruntime.jar"))
 
@@ -49,73 +56,83 @@ dependencies {
 application { mainClass.set("org.hyperledger.fabric.contract.ContractRouter") }
 
 tasks.named<ShadowJar>("shadowJar") {
-  if (System.getenv("NO_JML") == "") dependsOn(tasks.named("initOpenJML"))
-
   archiveBaseName.set("chaincode")
   archiveClassifier.set("")
   archiveVersion.set("")
 }
 
-tasks.named<Test>("test") { useJUnitPlatform() }
+tasks.register("initOpenJML") {
+  val openJMLVersion: String by project
 
-tasks.test {
-  java {
-    executable = "$openJMLDir/bin/jmlava"
-    jvmArgs = listOf("-Dorg.jmlspecs.openjml.rac=exception")
-  }
+  val zipFile: File = downloadDir.get().file("openjml.zip").asFile
+  downloadOpenJML(openJMLVersion, zipFile, logger)
+  extractOpenJML(zipFile, openJMLDir, logger)
+
+  // `jmlavac' is what we call `javac' that is actually
+  // OpenJML's javac; likewise, `jmlava' is a wrapper for `java' with
+  // OpenJML already in the classpath
+  generateJmlavac(jmlavac.asFile, openJMLJavaHomeDir, logger)
+  replaceJavac(openJMLJavaHomeDir, jmlavac.asFile, logger)
+  generateJmlava(jmlava.asFile, openJMLJavaHomeDir, logger)
+  replaceJava(openJMLJavaHomeDir, jmlava.asFile, logger)
+  logger.lifecycle("✅ OpenJML successfully initialized in $openJMLDir")
 }
 
-// java {
-//   sourceCompatibility = JavaVersion.VERSION_17
-//   targetCompatibility = JavaVersion.VERSION_17
-// }
+if (!noOpenJML) {
+  tasks.named<ShadowJar>("shadowJar") { dependsOn(tasks.named("initOpenJML")) }
+
+  tasks.test {
+    java {
+      executable = "$openJMLDir/bin/jmlava"
+      jvmArgs = listOf("-Dorg.jmlspecs.openjml.rac=exception")
+    }
+  }
 
-tasks.withType<JavaCompile>().configureEach {
-  // Only when not compiling because of Spotless
-  if (!gradle.startParameter.taskNames.any { it.contains("spotlessApply") } &&
-      System.getenv("NO_JML") == "") {
+  tasks.withType<JavaCompile>().configureEach {
     dependsOn(tasks.named("initOpenJML"))
-    val mode =
-        when (System.getenv("JML_MODE")) {
-          "esc" -> "esc"
-          else -> "rac"
-        }
-    options.isFork = true
-    options.compilerArgs.addAll(
-        listOf(
-            "-jml", "-$mode", "-timeout", "30", "--nullable-by-default", "--specs-path", "specs/"))
-    options.forkOptions.javaHome = openJMLJavaHomeDir.asFile
+    // Only when not compiling because of Spotless
+    if (!gradle.startParameter.taskNames.any { it.contains("spotlessApply") }) {
+      val mode =
+          when (System.getenv("JML_MODE")) {
+            "esc" -> "esc"
+            else -> "rac"
+          }
+      options.isFork = true
+      options.compilerArgs.addAll(
+          listOf(
+              "-jml",
+              "-$mode",
+              "-timeout",
+              "30",
+              "--nullable-by-default",
+              "--specs-path",
+              "specs/"))
+      options.forkOptions.javaHome = openJMLJavaHomeDir.asFile
+    }
   }
 }
 
-configure<SpotlessExtension> {
+tasks.test {
+  useJUnitPlatform()
+  testLogging {
+    showExceptions = true
+    events = setOf(TestLogEvent.FAILED, TestLogEvent.PASSED, TestLogEvent.SKIPPED)
+  }
+}
+
+spotless {
   java {
     importOrder()
     removeUnusedImports()
     googleJavaFormat()
     formatAnnotations()
     toggleOffOn()
+    licenseHeader("/* SPDX-License-Identifier: Apache-2.0 */")
   }
   kotlin {
     target("src/*/kotlin/**/*.kt", "buildSrc/src/*/kotlin/**/*.kt")
     ktfmt()
+    licenseHeader("/* SPDX-License-Identifier: Apache-2.0 */")
   }
   kotlinGradle { ktfmt() }
 }
-
-tasks.register("initOpenJML") {
-  val openJMLVersion: String by project
-
-  val zipFile: File = downloadDir.get().file("openjml.zip").asFile
-  downloadOpenJML(openJMLVersion, zipFile, logger)
-  extractOpenJML(zipFile, openJMLDir, logger)
-
-  // `jmlavac' is what we call `javac' that is actually
-  // OpenJML's javac; likewise, `jmlava' is a wrapper for `java' with
-  // OpenJML already in the classpath
-  generateJmlavac(jmlavac.asFile, openJMLJavaHomeDir, logger)
-  replaceJavac(openJMLJavaHomeDir, jmlavac.asFile, logger)
-  generateJmlava(jmlava.asFile, openJMLJavaHomeDir, logger)
-  replaceJava(openJMLJavaHomeDir, jmlava.asFile, logger)
-  logger.lifecycle("✅ OpenJML successfully initialized in $openJMLDir")
-}

smart-contract/hyperledger-fabric/v2/java/buildSrc/src/main/kotlin/hu/bme/mit/ftsrg/openjmlhelper/OpenJMLHelper.kt

@@ -1,3 +1,4 @@
+/* SPDX-License-Identifier: Apache-2.0 */
 package hu.bme.mit.ftsrg.openjmlhelper
 
 import java.io.File

smart-contract/hyperledger-fabric/v2/java/gradle.properties

@@ -1 +1,2 @@
 openJMLVersion = 0.17.0-alpha-15
+withoutOpenJML = false

smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/TPCC.jml

@@ -2,8 +2,8 @@
 
 package hu.bme.mit.ftsrg.chaincode.tpcc;
 
-import hu.bme.mit.ftsrg.chaincode.dataaccess.exception.EntityExistsException;
-import hu.bme.mit.ftsrg.chaincode.dataaccess.exception.EntityNotFoundException;
+import hu.bme.mit.ftsrg.hypernate.entity.EntityExistsException;
+import hu.bme.mit.ftsrg.hypernate.entity.EntityNotFoundException;
 import hu.bme.mit.ftsrg.chaincode.tpcc.data.input.*;
 import hu.bme.mit.ftsrg.chaincode.tpcc.data.output.*;
 import hu.bme.mit.ftsrg.chaincode.tpcc.middleware.TPCCContext;
@@ -57,4 +57,9 @@ public final class TPCC implements ContractInterface {
     @*/
   private StockLevelOutput stockLevel(final TPCCContext ctx, final StockLevelInput input)
       throws EntityNotFoundException, NotFoundException;
+
+  /*@
+    @ requires c_id < 2;
+    @*/
+  public String OJMLTEST__getCustomer(final TPCCContext ctx, final int c_w_id, final int c_d_id, final int c_id);
 }

smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/Customer.jml

@@ -2,9 +2,9 @@
 
 package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
 
-import hu.bme.mit.ftsrg.chaincode.dataaccess.SerializableEntityBase;
+import hu.bme.mit.ftsrg.hypernate.entity.Entity;
 
-public class Customer extends SerializableEntityBase<Customer> {
+public class Customer implements Entity<Customer> {
 
   public /*@ pure @*/ int getC_id();
 

smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/District.jml

@@ -2,9 +2,9 @@
 
 package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
 
-import hu.bme.mit.ftsrg.chaincode.dataaccess.SerializableEntityBase;
+import hu.bme.mit.ftsrg.hypernate.entity.Entity;
 
-public final class District extends SerializableEntityBase<District> {
+public final class District implements Entity<District> {
 
   public /*@ pure @*/ int getD_id();
 

smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/History.jml

@@ -2,9 +2,9 @@
 
 package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
 
-import hu.bme.mit.ftsrg.chaincode.dataaccess.SerializableEntityBase;
+import hu.bme.mit.ftsrg.hypernate.entity.Entity;
 
-public final class History extends SerializableEntityBase<History> {
+public final class History implements Entity<History> {
 
   public /*@ pure @*/ int getH_c_id();
 

smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/Item.jml

@@ -2,9 +2,9 @@
 
 package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
 
-import hu.bme.mit.ftsrg.chaincode.dataaccess.SerializableEntityBase;
+import hu.bme.mit.ftsrg.hypernate.entity.Entity;
 
-public final class Item extends SerializableEntityBase<Item> {
+public final class Item implements Entity<Item> {
 
   public /*@ pure @*/ int getI_id();
 

smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/NewOrder.jml

@@ -2,9 +2,9 @@
 
 package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
 
-import hu.bme.mit.ftsrg.chaincode.dataaccess.SerializableEntityBase;
+import hu.bme.mit.ftsrg.hypernate.entity.Entity;
 
-public final class NewOrder extends SerializableEntityBase<NewOrder> {
+public final class NewOrder implements Entity<NewOrder> {
 
   public /*@ pure @*/ int getNo_o_id();
 

smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/Order.jml

@@ -2,9 +2,9 @@
 
 package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
 
-import hu.bme.mit.ftsrg.chaincode.dataaccess.SerializableEntityBase;
+import hu.bme.mit.ftsrg.hypernate.entity.Entity;
 
-public final class Order extends SerializableEntityBase<Order> {
+public final class Order implements Entity<Order> {
 
   public /*@ pure @*/ int getO_id();
 

smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/OrderLine.jml

@@ -2,9 +2,9 @@
 
 package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
 
-import hu.bme.mit.ftsrg.chaincode.dataaccess.SerializableEntityBase;
+import hu.bme.mit.ftsrg.hypernate.entity.Entity;
 
-public final class OrderLine extends SerializableEntityBase<OrderLine> {
+public final class OrderLine implements Entity<OrderLine> {
 
   public /*@ pure @*/ int getOl_o_id();
 

smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/Stock.jml

@@ -2,9 +2,9 @@
 
 package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
 
-import hu.bme.mit.ftsrg.chaincode.dataaccess.SerializableEntityBase;
+import hu.bme.mit.ftsrg.hypernate.entity.Entity;
 
-public final class Stock extends SerializableEntityBase<Stock> {
+public final class Stock implements Entity<Stock> {
 
   public /*@ pure @*/ int getS_i_id();
 

smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/data/entity/Warehouse.jml

@@ -2,9 +2,9 @@
 
 package hu.bme.mit.ftsrg.chaincode.tpcc.data.entity;
 
-import hu.bme.mit.ftsrg.chaincode.dataaccess.SerializableEntityBase;
+import hu.bme.mit.ftsrg.hypernate.entity.Entity;
 
-public class Warehouse extends SerializableEntityBase<Warehouse> {
+public class Warehouse implements Entity<Warehouse> {
 
   public /*@ pure @*/ int getW_id();
 

smart-contract/hyperledger-fabric/v2/java/src/main/java/hu/bme/mit/ftsrg/chaincode/MethodLogger.java

@@ -1,6 +1,7 @@
+/* SPDX-License-Identifier: Apache-2.0 */
 package hu.bme.mit.ftsrg.chaincode;
 
-import hu.bme.mit.ftsrg.chaincode.dataaccess.SerializableEntity;
+import hu.bme.mit.ftsrg.hypernate.entity.Entity;
 import java.util.ArrayList;
 import java.util.List;
 import org.hyperledger.fabric.contract.Context;
@@ -42,7 +43,7 @@ public String generateParamsString(final Context ctx, final int... params) {
     return "%s,%s".formatted(ctx.toString(), generateParamsString(params));
   }
 
-  public <Type extends SerializableEntity<Type>> String generateParamsString(
+  public <Type extends Entity<Type>> String generateParamsString(
       final Context ctx, final Type obj) {
     return "%s,%s".formatted(ctx.toString(), obj.toString());
   }