From b682644ea74a51fade538008aae5f20d8fa7b8b9 Mon Sep 17 00:00:00 2001 From: Fausto Spoto Date: Mon, 6 Jan 2025 15:33:29 +0100 Subject: [PATCH] Clean-up of the white-listing --- ...ChecksForWhiteListingProofObligations.java | 2 +- .../java/io/hotmoka/tests/HotmokaTest.java | 4 +- .../errors/LegalStaticInitialization1.java | 10 +---- ...supportedVerificationVersionException.java | 2 +- .../api/WhiteListingProofObligation.java | 2 +- .../MustBeSafeLibraryCollection.java | 39 ++++++++++++++++ .../whitelisting/MustBeSafeLibraryMap.java | 39 ++++++++++++++++ ...sticTerminatingEqualsAndHashCodeCheck.java | 8 ++-- ...asDeterministicTerminatingEqualsCheck.java | 7 ++- ...DeterministicTerminatingHashCodeCheck.java | 14 +++--- ...DeterministicTerminatingToStringCheck.java | 22 ++++----- .../internal/checks/MustBeFalseCheck.java | 2 +- .../MustBeSafeLibraryCollectionCheck.java | 45 +++++++++++++++++++ .../checks/MustBeSafeLibraryMapCheck.java | 44 ++++++++++++++++++ .../database/version0/java/lang/Object.java | 2 +- .../version0/java/util/ArrayList.java | 2 +- .../version0/java/util/Collection.java | 11 +++-- .../database/version0/java/util/HashMap.java | 2 +- .../database/version0/java/util/HashSet.java | 2 +- .../version0/java/util/LinkedList.java | 2 +- .../database/version0/java/util/List.java | 3 +- .../database/version0/java/util/Map.java | 7 +-- .../database/version0/java/util/Random.java | 3 ++ .../database/version0/java/util/Set.java | 7 +-- .../src/main/java/module-info.java | 2 +- 25 files changed, 219 insertions(+), 64 deletions(-) create mode 100644 io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/MustBeSafeLibraryCollection.java create mode 100644 io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/MustBeSafeLibraryMap.java create mode 100644 io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeSafeLibraryCollectionCheck.java create mode 100644 io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeSafeLibraryMapCheck.java diff --git a/io-hotmoka-instrumentation/src/main/java/io/hotmoka/instrumentation/internal/instrumentationsOfMethod/AddRuntimeChecksForWhiteListingProofObligations.java b/io-hotmoka-instrumentation/src/main/java/io/hotmoka/instrumentation/internal/instrumentationsOfMethod/AddRuntimeChecksForWhiteListingProofObligations.java index 9f55e684b..70072e640 100644 --- a/io-hotmoka-instrumentation/src/main/java/io/hotmoka/instrumentation/internal/instrumentationsOfMethod/AddRuntimeChecksForWhiteListingProofObligations.java +++ b/io-hotmoka-instrumentation/src/main/java/io/hotmoka/instrumentation/internal/instrumentationsOfMethod/AddRuntimeChecksForWhiteListingProofObligations.java @@ -392,7 +392,7 @@ private InvokeInstruction addWhiteListVerificationMethodForNonINVOKEDYNAMIC(Inst il.append(invoke); il.append(InstructionFactory.createReturn(verifierReturnType)); - Type[] argsAsArray = args.toArray(Type[]::new); + var argsAsArray = args.toArray(Type[]::new); var addedVerifier = new MethodGen(PRIVATE_SYNTHETIC_STATIC, verifierReturnType, argsAsArray, null, verifierName, className, il, cpg); addMethod(addedVerifier, false); diff --git a/io-hotmoka-tests/src/test/java/io/hotmoka/tests/HotmokaTest.java b/io-hotmoka-tests/src/test/java/io/hotmoka/tests/HotmokaTest.java index ea98c03e0..d6457e879 100644 --- a/io-hotmoka-tests/src/test/java/io/hotmoka/tests/HotmokaTest.java +++ b/io-hotmoka-tests/src/test/java/io/hotmoka/tests/HotmokaTest.java @@ -152,11 +152,11 @@ public void beforeAll(ExtensionContext context) throws Exception { privateKeyOfGamete = keys.getPrivate(); Node wrapped; - //node = wrapped = mkDiskNode(); + node = wrapped = mkDiskNode(); //node = wrapped = mkMokamintNodeConnectedToPeer(); //node = wrapped = mkMokamintNetwork(4); //node = wrapped = mkTendermintNode(); - node = mkRemoteNode(wrapped = mkDiskNode()); + //node = mkRemoteNode(wrapped = mkDiskNode()); //node = mkRemoteNode(wrapped = mkMokamintNetwork(1)); //node = mkRemoteNode(wrapped = mkTendermintNode()); //node = wrapped = mkRemoteNode("ec2-54-194-239-91.eu-west-1.compute.amazonaws.com:8080"); diff --git a/io-hotmoka-tests/src/test/java/io/hotmoka/tests/errors/LegalStaticInitialization1.java b/io-hotmoka-tests/src/test/java/io/hotmoka/tests/errors/LegalStaticInitialization1.java index 6c80e8fb4..cc6c1a709 100644 --- a/io-hotmoka-tests/src/test/java/io/hotmoka/tests/errors/LegalStaticInitialization1.java +++ b/io-hotmoka-tests/src/test/java/io/hotmoka/tests/errors/LegalStaticInitialization1.java @@ -16,20 +16,12 @@ package io.hotmoka.tests.errors; -import java.io.IOException; import java.math.BigInteger; -import java.security.InvalidKeyException; -import java.security.SignatureException; -import java.util.NoSuchElementException; -import java.util.concurrent.TimeoutException; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.DisplayName; import org.junit.jupiter.api.Test; -import io.hotmoka.node.api.NodeException; -import io.hotmoka.node.api.TransactionException; -import io.hotmoka.node.api.TransactionRejectedException; import io.hotmoka.tests.HotmokaTest; class LegalStaticInitialization1 extends HotmokaTest { @@ -40,7 +32,7 @@ void beforeEach() throws Exception { } @Test @DisplayName("install jar") - void installJar() throws TransactionException, IOException, TransactionRejectedException, InvalidKeyException, SignatureException, NoSuchElementException, NodeException, TimeoutException, InterruptedException { + void installJar() throws Exception { addJarStoreTransaction(privateKey(0), account(0), _500_000, BigInteger.ONE, takamakaCode(), bytesOf("legalstaticinitialization1.jar"), takamakaCode()); } } \ No newline at end of file diff --git a/io-hotmoka-whitelisting-api/src/main/java/io/hotmoka/whitelisting/api/UnsupportedVerificationVersionException.java b/io-hotmoka-whitelisting-api/src/main/java/io/hotmoka/whitelisting/api/UnsupportedVerificationVersionException.java index 7fc2a135c..880e6a8c0 100644 --- a/io-hotmoka-whitelisting-api/src/main/java/io/hotmoka/whitelisting/api/UnsupportedVerificationVersionException.java +++ b/io-hotmoka-whitelisting-api/src/main/java/io/hotmoka/whitelisting/api/UnsupportedVerificationVersionException.java @@ -19,8 +19,8 @@ /** * An exception thrown when the verification version of the node is not supported. */ +@SuppressWarnings("serial") public class UnsupportedVerificationVersionException extends Exception { - private static final long serialVersionUID = -1232455923178336022L; /** * The unsupported verification version. diff --git a/io-hotmoka-whitelisting-api/src/main/java/io/hotmoka/whitelisting/api/WhiteListingProofObligation.java b/io-hotmoka-whitelisting-api/src/main/java/io/hotmoka/whitelisting/api/WhiteListingProofObligation.java index 8d8afd82e..c8b20a39b 100644 --- a/io-hotmoka-whitelisting-api/src/main/java/io/hotmoka/whitelisting/api/WhiteListingProofObligation.java +++ b/io-hotmoka-whitelisting-api/src/main/java/io/hotmoka/whitelisting/api/WhiteListingProofObligation.java @@ -23,7 +23,7 @@ import java.lang.annotation.Target; /** - * States that an annotation is meant to decorate an argument of a method + * An annotation that is meant to decorate an argument of a method * or constructor of a white-listed method and specifies some property that * the argument must satisfy, for the method to be white-listed. */ diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/MustBeSafeLibraryCollection.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/MustBeSafeLibraryCollection.java new file mode 100644 index 000000000..0743ce949 --- /dev/null +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/MustBeSafeLibraryCollection.java @@ -0,0 +1,39 @@ +/* +Copyright 2021 Fausto Spoto + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +*/ + +package io.hotmoka.whitelisting; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Inherited; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +import io.hotmoka.whitelisting.api.WhiteListingProofObligation; +import io.hotmoka.whitelisting.internal.checks.MustBeSafeLibraryCollectionCheck; + +/** + * States that an object of a white-listed method must be a safe library collection, + * exactly, hence not a user-defined collection class. + */ +@Retention(RetentionPolicy.RUNTIME) +@Target(value={ ElementType.METHOD, ElementType.PARAMETER }) +@Inherited +@Documented +@WhiteListingProofObligation(check = MustBeSafeLibraryCollectionCheck.class) +public @interface MustBeSafeLibraryCollection { +} \ No newline at end of file diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/MustBeSafeLibraryMap.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/MustBeSafeLibraryMap.java new file mode 100644 index 000000000..ff3b12872 --- /dev/null +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/MustBeSafeLibraryMap.java @@ -0,0 +1,39 @@ +/* +Copyright 2021 Fausto Spoto + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +*/ + +package io.hotmoka.whitelisting; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Inherited; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +import io.hotmoka.whitelisting.api.WhiteListingProofObligation; +import io.hotmoka.whitelisting.internal.checks.MustBeSafeLibraryMapCheck; + +/** + * States that an object of a white-listed method must be a safe library map, + * exactly, hence not a user-defined map class. + */ +@Retention(RetentionPolicy.RUNTIME) +@Target(value={ ElementType.METHOD, ElementType.PARAMETER }) +@Inherited +@Documented +@WhiteListingProofObligation(check = MustBeSafeLibraryMapCheck.class) +public @interface MustBeSafeLibraryMap { +} \ No newline at end of file diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingEqualsAndHashCodeCheck.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingEqualsAndHashCodeCheck.java index c23096e3b..321f03700 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingEqualsAndHashCodeCheck.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingEqualsAndHashCodeCheck.java @@ -73,23 +73,23 @@ private static boolean hashCodelsIsDeterministicAndTerminating(Class clazz, W private static Optional getHashCodeFor(Class clazz) { return Stream.of(clazz.getMethods()) - .filter(method -> !Modifier.isAbstract(method.getModifiers()) + .filter(method -> "hashCode".equals(method.getName()) + && !Modifier.isAbstract(method.getModifiers()) && Modifier.isPublic(method.getModifiers()) && !Modifier.isStatic(method.getModifiers()) && method.getParameters().length == 0 - && "hashCode".equals(method.getName()) && method.getReturnType() == int.class) .findFirst(); } private static Optional getEqualsFor(Class clazz) { return Stream.of(clazz.getMethods()) - .filter(method -> !Modifier.isAbstract(method.getModifiers()) + .filter(method -> "equals".equals(method.getName()) + && !Modifier.isAbstract(method.getModifiers()) && Modifier.isPublic(method.getModifiers()) && !Modifier.isStatic(method.getModifiers()) && method.getParameters().length == 1 && method.getParameterTypes()[0] == Object.class - && "equals".equals(method.getName()) && method.getReturnType() == boolean.class) .findFirst(); } diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingEqualsCheck.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingEqualsCheck.java index 5dbc71cff..4f105cc30 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingEqualsCheck.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingEqualsCheck.java @@ -45,8 +45,7 @@ private static boolean equalsIsDeterministicAndTerminating(Class clazz, White } private static boolean isInWhiteListingDatabaseWithoutProofObligations(Method method, WhiteListingWizard wizard) { - Optional model = wizard.whiteListingModelOf(method); - return model.isPresent() && hasNoProofObligations(model.get()); + return wizard.whiteListingModelOf(method).map(HasDeterministicTerminatingEqualsCheck::hasNoProofObligations).orElse(false); } private static boolean hasNoProofObligations(Method model) { @@ -59,12 +58,12 @@ private static boolean hasNoProofObligations(Method model) { private static Optional getEqualsFor(Class clazz) { return Stream.of(clazz.getMethods()) - .filter(method -> !Modifier.isAbstract(method.getModifiers()) + .filter(method -> "equals".equals(method.getName()) + && !Modifier.isAbstract(method.getModifiers()) && Modifier.isPublic(method.getModifiers()) && !Modifier.isStatic(method.getModifiers()) && method.getParameters().length == 1 && method.getParameterTypes()[0] == Object.class - && "equals".equals(method.getName()) && method.getReturnType() == boolean.class) .findFirst(); } diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingHashCodeCheck.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingHashCodeCheck.java index 0a5c5b16d..cfac5591a 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingHashCodeCheck.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingHashCodeCheck.java @@ -33,17 +33,15 @@ public class HasDeterministicTerminatingHashCodeCheck implements WhiteListingPre @Override public boolean test(Object value, WhiteListingWizard wizard) { - return value == null || hashCodelsIsDeterministicAndTerminating(value.getClass(), wizard); + return value == null || hashCodeIsDeterministicAndTerminating(value.getClass(), wizard); } - private static boolean hashCodelsIsDeterministicAndTerminating(Class clazz, WhiteListingWizard wizard) { - Optional hashCode = getHashCodeFor(clazz); - return hashCode.isPresent() && isInWhiteListingDatabaseWithoutProofObligations(hashCode.get(), wizard); + private static boolean hashCodeIsDeterministicAndTerminating(Class clazz, WhiteListingWizard wizard) { + return getHashCodeFor(clazz).map(hashCode -> isInWhiteListingDatabaseWithoutProofObligations(hashCode, wizard)).orElse(false); } private static boolean isInWhiteListingDatabaseWithoutProofObligations(Method method, WhiteListingWizard wizard) { - Optional model = wizard.whiteListingModelOf(method); - return model.isPresent() && hasNoProofObligations(model.get()); + return wizard.whiteListingModelOf(method).map(HasDeterministicTerminatingHashCodeCheck::hasNoProofObligations).orElse(false); } private static boolean hasNoProofObligations(Method model) { @@ -56,11 +54,11 @@ private static boolean hasNoProofObligations(Method model) { private static Optional getHashCodeFor(Class clazz) { return Stream.of(clazz.getMethods()) - .filter(method -> !Modifier.isAbstract(method.getModifiers()) + .filter(method -> "hashCode".equals(method.getName()) + && !Modifier.isAbstract(method.getModifiers()) && Modifier.isPublic(method.getModifiers()) && !Modifier.isStatic(method.getModifiers()) && method.getParameters().length == 0 - && "hashCode".equals(method.getName()) && method.getReturnType() == int.class) .findFirst(); } diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingToStringCheck.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingToStringCheck.java index cf58d4bc3..3dba934f6 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingToStringCheck.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingToStringCheck.java @@ -33,10 +33,10 @@ public class HasDeterministicTerminatingToStringCheck implements WhiteListingPre @Override public boolean test(Object value, WhiteListingWizard wizard) { - return value == null || toStringlsIsDeterministicAndTerminating(value.getClass(), wizard); + return value == null || toStringIsDeterministicAndTerminating(value.getClass(), wizard); } - private static boolean toStringlsIsDeterministicAndTerminating(Class clazz, WhiteListingWizard wizard) { + private static boolean toStringIsDeterministicAndTerminating(Class clazz, WhiteListingWizard wizard) { Optional toString = getToStringFor(clazz); return toString.isPresent() && (isInWhiteListingDatabaseWithoutProofObligations(toString.get(), wizard) @@ -44,8 +44,7 @@ private static boolean toStringlsIsDeterministicAndTerminating(Class clazz, W } private static boolean isInWhiteListingDatabaseWithoutProofObligations(Method method, WhiteListingWizard wizard) { - Optional model = wizard.whiteListingModelOf(method); - return model.isPresent() && hasNoProofObligations(model.get()); + return wizard.whiteListingModelOf(method).map(HasDeterministicTerminatingToStringCheck::hasNoProofObligations).orElse(false); } private static boolean hasNoProofObligations(Method model) { @@ -58,33 +57,28 @@ private static boolean hasNoProofObligations(Method model) { private static Optional getToStringFor(Class clazz) { return Stream.of(clazz.getMethods()) - .filter(method -> !Modifier.isAbstract(method.getModifiers()) + .filter(method -> "toString".equals(method.getName()) + && !Modifier.isAbstract(method.getModifiers()) && Modifier.isPublic(method.getModifiers()) && !Modifier.isStatic(method.getModifiers()) && method.getParameters().length == 0 - && "toString".equals(method.getName()) && method.getReturnType() == String.class) .findFirst(); } private static Optional getHashCodeFor(Class clazz) { return Stream.of(clazz.getMethods()) - .filter(method -> !Modifier.isAbstract(method.getModifiers()) + .filter(method -> "hashCode".equals(method.getName()) + && !Modifier.isAbstract(method.getModifiers()) && Modifier.isPublic(method.getModifiers()) && !Modifier.isStatic(method.getModifiers()) && method.getParameters().length == 0 - && "hashCode".equals(method.getName()) && method.getReturnType() == int.class) .findFirst(); } private static boolean toStringIsInObjectAndHashCodeIsDeterministicAndTerminating(Method toString, Class clazz, WhiteListingWizard wizard) { - if (toString.getDeclaringClass() == Object.class) { - Optional hashCode = getHashCodeFor(clazz); - return hashCode.isPresent() && isInWhiteListingDatabaseWithoutProofObligations(hashCode.get(), wizard); - } - else - return false; + return toString.getDeclaringClass() == Object.class && getHashCodeFor(clazz).map(hashCode -> isInWhiteListingDatabaseWithoutProofObligations(hashCode, wizard)).orElse(false); } @Override diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeFalseCheck.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeFalseCheck.java index b1fb53fd6..f5ad10788 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeFalseCheck.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeFalseCheck.java @@ -26,7 +26,7 @@ public class MustBeFalseCheck implements WhiteListingPredicate { @Override public boolean test(Object value, WhiteListingWizard wizard) { - return value.equals(Boolean.FALSE); + return Boolean.FALSE.equals(value); } @Override diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeSafeLibraryCollectionCheck.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeSafeLibraryCollectionCheck.java new file mode 100644 index 000000000..97caee1cd --- /dev/null +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeSafeLibraryCollectionCheck.java @@ -0,0 +1,45 @@ +/* +Copyright 2023 Fausto Spoto + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +*/ + +package io.hotmoka.whitelisting.internal.checks; + +import java.util.ArrayList; +import java.util.HashSet; +import java.util.LinkedList; + +import io.hotmoka.whitelisting.api.WhiteListingPredicate; +import io.hotmoka.whitelisting.api.WhiteListingWizard; + +/** + * A check that the class of a value is exactly one of the allowed collection classes from the library + * (not a user subclass then). + */ +public class MustBeSafeLibraryCollectionCheck implements WhiteListingPredicate { + + @Override + public boolean test(Object value, WhiteListingWizard wizard) { + return value == null || isSafeLibraryCollection(value.getClass()); + } + + private static boolean isSafeLibraryCollection(Class clazz) { + return clazz == HashSet.class || clazz == LinkedList.class || clazz == ArrayList.class; + } + + @Override + public String messageIfFailed(String methodName) { + return "cannot prove that this object is a safe library collection"; + } +} \ No newline at end of file diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeSafeLibraryMapCheck.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeSafeLibraryMapCheck.java new file mode 100644 index 000000000..62494b689 --- /dev/null +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeSafeLibraryMapCheck.java @@ -0,0 +1,44 @@ +/* +Copyright 2023 Fausto Spoto + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +*/ + +package io.hotmoka.whitelisting.internal.checks; + +import java.util.HashMap; + +import io.hotmoka.whitelisting.api.WhiteListingPredicate; +import io.hotmoka.whitelisting.api.WhiteListingWizard; + +/** + * A check that the class of a value is exactly one of the allowed map classes from the library + * (not a user subclass then). + */ +public class MustBeSafeLibraryMapCheck implements WhiteListingPredicate { + + @Override + public boolean test(Object value, WhiteListingWizard wizard) { + return value == null || isSafeLibraryMap(value.getClass()); + } + + private static boolean isSafeLibraryMap(Class clazz) { + System.out.println(clazz.getName()); + return clazz == HashMap.class; + } + + @Override + public String messageIfFailed(String methodName) { + return "cannot prove that this object is a safe library map"; + } +} \ No newline at end of file diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/lang/Object.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/lang/Object.java index 81e959463..82b9d4c67 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/lang/Object.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/lang/Object.java @@ -23,7 +23,7 @@ public abstract class Object { public Object() {} public abstract java.lang.Object clone(); - //public abstract java.lang.Class getClass(); // this needs a special treatment in the code + //public abstract java.lang.Class getClass(); // this needs a special treatment in the code since it's final in Object public abstract @HasDeterministicTerminatingEquals boolean equals(java.lang.Object other); public abstract @HasDeterministicTerminatingToString java.lang.String toString(); public abstract @HasDeterministicTerminatingHashCode int hashCode(); diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/ArrayList.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/ArrayList.java index 901d814e2..3d1d6e139 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/ArrayList.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/ArrayList.java @@ -19,7 +19,7 @@ public abstract class ArrayList { public ArrayList() {} public ArrayList(int size) {} - public ArrayList(java.util.Collection c) {} + public ArrayList(/*@MustBeSafeLibraryCollection*/ java.util.Collection c) {} // TODO public abstract void trimToSize(); public abstract void ensureCapacity(int minCapacity); } \ No newline at end of file diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Collection.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Collection.java index 750d2b9d1..00754812c 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Collection.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Collection.java @@ -17,6 +17,7 @@ package io.hotmoka.whitelisting.internal.database.version0.java.util; import io.hotmoka.whitelisting.HasDeterministicTerminatingEqualsAndHashCode; +import io.hotmoka.whitelisting.MustBeSafeLibraryCollection; public interface Collection { int size(); @@ -27,11 +28,13 @@ public interface Collection { T[] toArray(java.util.function.IntFunction generator); boolean add(@HasDeterministicTerminatingEqualsAndHashCode E e); boolean remove(@HasDeterministicTerminatingEqualsAndHashCode java.lang.Object o); - boolean containsAll(java.util.Collection c); - boolean addAll(java.util.Collection c); - boolean removeAll(java.util.Collection c); boolean removeIf(java.util.function.Predicate filter); - boolean retainAll(java.util.Collection c); void clear(); java.util.stream.Stream stream(); + // we do not allow any collection as parameter, because we don't know + // if their elements have deterministic equals() and hashCode() + boolean containsAll(@MustBeSafeLibraryCollection java.util.Collection c); + boolean addAll(@MustBeSafeLibraryCollection java.util.Collection c); + boolean removeAll(@MustBeSafeLibraryCollection java.util.Collection c); + boolean retainAll(@MustBeSafeLibraryCollection java.util.Collection c); } \ No newline at end of file diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/HashMap.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/HashMap.java index 3e9c59c4d..2dcffe75b 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/HashMap.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/HashMap.java @@ -20,5 +20,5 @@ public abstract class HashMap { public HashMap(int initialCapacity, float loadFactor) {} public HashMap(int initialCapacity) {} public HashMap() {} - public HashMap(java.util.Map m) {} + public HashMap(/*@MustBeSafeLibraryMap */ java.util.Map m) {} // TODO } \ No newline at end of file diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/HashSet.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/HashSet.java index ddfa13737..7f2a6e62d 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/HashSet.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/HashSet.java @@ -18,7 +18,7 @@ public class HashSet { public HashSet() {} - public HashSet(java.util.Collection c) {} + public HashSet(/*@MustBeSafeLibraryCollection*/ java.util.Collection c) {} // TODO: the annotation generates wrong bytecode public HashSet(int initialCapacity, float loadFactor) {} public HashSet(int initialCapacity) {} } \ No newline at end of file diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/LinkedList.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/LinkedList.java index 6919c37d7..2552f5135 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/LinkedList.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/LinkedList.java @@ -20,7 +20,7 @@ public abstract class LinkedList { public LinkedList() {} - public LinkedList(java.util.Collection c) {} + public LinkedList(/*@MustBeSafeLibraryCollection*/ java.util.Collection c) {} public abstract E getFirst(); public abstract E getLast(); public abstract E removeFirst(); diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/List.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/List.java index 7f1b534d4..ff72be7a3 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/List.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/List.java @@ -17,6 +17,7 @@ package io.hotmoka.whitelisting.internal.database.version0.java.util; import io.hotmoka.whitelisting.HasDeterministicTerminatingEqualsAndHashCode; +import io.hotmoka.whitelisting.MustBeSafeLibraryCollection; public interface List { E get(int index); @@ -43,5 +44,5 @@ public interface List { static java.util.List of(@HasDeterministicTerminatingEqualsAndHashCode E e1, @HasDeterministicTerminatingEqualsAndHashCode E e2, @HasDeterministicTerminatingEqualsAndHashCode E e3, @HasDeterministicTerminatingEqualsAndHashCode E e4, @HasDeterministicTerminatingEqualsAndHashCode E e5, @HasDeterministicTerminatingEqualsAndHashCode E e6, @HasDeterministicTerminatingEqualsAndHashCode E e7, @HasDeterministicTerminatingEqualsAndHashCode E e8) { return null; } static java.util.List of(@HasDeterministicTerminatingEqualsAndHashCode E e1, @HasDeterministicTerminatingEqualsAndHashCode E e2, @HasDeterministicTerminatingEqualsAndHashCode E e3, @HasDeterministicTerminatingEqualsAndHashCode E e4, @HasDeterministicTerminatingEqualsAndHashCode E e5, @HasDeterministicTerminatingEqualsAndHashCode E e6, @HasDeterministicTerminatingEqualsAndHashCode E e7, @HasDeterministicTerminatingEqualsAndHashCode E e8, @HasDeterministicTerminatingEqualsAndHashCode E e9) { return null; } static java.util.List of(@HasDeterministicTerminatingEqualsAndHashCode E e1, @HasDeterministicTerminatingEqualsAndHashCode E e2, @HasDeterministicTerminatingEqualsAndHashCode E e3, @HasDeterministicTerminatingEqualsAndHashCode E e4, @HasDeterministicTerminatingEqualsAndHashCode E e5, @HasDeterministicTerminatingEqualsAndHashCode E e6, @HasDeterministicTerminatingEqualsAndHashCode E e7, @HasDeterministicTerminatingEqualsAndHashCode E e8, @HasDeterministicTerminatingEqualsAndHashCode E e9, @HasDeterministicTerminatingEqualsAndHashCode E e10) { return null; } - static java.util.List copyOf(java.util.Collection coll) { return null; } + static java.util.List copyOf(@MustBeSafeLibraryCollection java.util.Collection coll) { return null; } } \ No newline at end of file diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Map.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Map.java index 4485a035a..80e6f6bad 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Map.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Map.java @@ -17,17 +17,18 @@ package io.hotmoka.whitelisting.internal.database.version0.java.util; import io.hotmoka.whitelisting.HasDeterministicTerminatingEqualsAndHashCode; +import io.hotmoka.whitelisting.MustBeSafeLibraryMap; public interface Map { int size(); boolean isEmpty(); V put(@HasDeterministicTerminatingEqualsAndHashCode K key, V value); - java.util.Set keySet(); + @MustBeSafeLibraryMap java.util.Set keySet(); boolean containsKey(@HasDeterministicTerminatingEqualsAndHashCode java.lang.Object key); boolean containsValue(java.lang.Object value); V get(@HasDeterministicTerminatingEqualsAndHashCode java.lang.Object key); V remove(@HasDeterministicTerminatingEqualsAndHashCode java.lang.Object key); - void putAll(java.util.Map m); + void putAll(@MustBeSafeLibraryMap java.util.Map m); void clear(); V getOrDefault(@HasDeterministicTerminatingEqualsAndHashCode java.lang.Object key, V defaultValue); void forEach(java.util.function.BiConsumer action); @@ -53,5 +54,5 @@ public interface Map { static java.util.Map of(@HasDeterministicTerminatingEqualsAndHashCode K k1, V v1, @HasDeterministicTerminatingEqualsAndHashCode K k2, V v2, @HasDeterministicTerminatingEqualsAndHashCode K k3, V v3, @HasDeterministicTerminatingEqualsAndHashCode K k4, V v4, @HasDeterministicTerminatingEqualsAndHashCode K k5, V v5, @HasDeterministicTerminatingEqualsAndHashCode K k6, V v6, @HasDeterministicTerminatingEqualsAndHashCode K k7, V v7, @HasDeterministicTerminatingEqualsAndHashCode K k8, V v8, @HasDeterministicTerminatingEqualsAndHashCode K k9, V v9, @HasDeterministicTerminatingEqualsAndHashCode K k10, V v10) { return null; } static java.util.Map ofEntries(java.util.Map.Entry[] entries) { return null; } static java.util.Map.Entry entry(@HasDeterministicTerminatingEqualsAndHashCode K k, V v) { return null; } - static java.util.Map copyOf(java.util.Map map) { return null; } + static java.util.Map copyOf(@MustBeSafeLibraryMap java.util.Map map) { return null; } } \ No newline at end of file diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Random.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Random.java index 6a1e210c2..f0abda0c1 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Random.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Random.java @@ -16,6 +16,9 @@ package io.hotmoka.whitelisting.internal.database.version0.java.util; +/** + * White-listed only if created with seed. + */ public abstract class Random { public Random(long seed) {} diff --git a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Set.java b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Set.java index 96ba48fc4..d76a15318 100644 --- a/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Set.java +++ b/io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/util/Set.java @@ -17,12 +17,9 @@ package io.hotmoka.whitelisting.internal.database.version0.java.util; import io.hotmoka.whitelisting.HasDeterministicTerminatingEqualsAndHashCode; +import io.hotmoka.whitelisting.MustBeSafeLibraryCollection; public interface Set { - boolean containsAll(java.util.Collection c); - boolean addAll(java.util.Collection c); - boolean retainAll(java.util.Collection c); - boolean removeAll(java.util.Collection c); static java.util.Set of() { return null; } static java.util.Set of(@HasDeterministicTerminatingEqualsAndHashCode E e1) { return null; } static java.util.Set of(@HasDeterministicTerminatingEqualsAndHashCode E e1, @HasDeterministicTerminatingEqualsAndHashCode E e2) { return null; } @@ -34,5 +31,5 @@ public interface Set { static java.util.Set of(@HasDeterministicTerminatingEqualsAndHashCode E e1, @HasDeterministicTerminatingEqualsAndHashCode E e2, @HasDeterministicTerminatingEqualsAndHashCode E e3, @HasDeterministicTerminatingEqualsAndHashCode E e4, @HasDeterministicTerminatingEqualsAndHashCode E e5, @HasDeterministicTerminatingEqualsAndHashCode E e6, @HasDeterministicTerminatingEqualsAndHashCode E e7, @HasDeterministicTerminatingEqualsAndHashCode E e8) { return null; } static java.util.Set of(@HasDeterministicTerminatingEqualsAndHashCode E e1, @HasDeterministicTerminatingEqualsAndHashCode E e2, @HasDeterministicTerminatingEqualsAndHashCode E e3, @HasDeterministicTerminatingEqualsAndHashCode E e4, @HasDeterministicTerminatingEqualsAndHashCode E e5, @HasDeterministicTerminatingEqualsAndHashCode E e6, @HasDeterministicTerminatingEqualsAndHashCode E e7, @HasDeterministicTerminatingEqualsAndHashCode E e8, @HasDeterministicTerminatingEqualsAndHashCode E e9) { return null; } static java.util.Set of(@HasDeterministicTerminatingEqualsAndHashCode E e1, @HasDeterministicTerminatingEqualsAndHashCode E e2, @HasDeterministicTerminatingEqualsAndHashCode E e3, @HasDeterministicTerminatingEqualsAndHashCode E e4, @HasDeterministicTerminatingEqualsAndHashCode E e5, @HasDeterministicTerminatingEqualsAndHashCode E e6, @HasDeterministicTerminatingEqualsAndHashCode E e7, @HasDeterministicTerminatingEqualsAndHashCode E e8, @HasDeterministicTerminatingEqualsAndHashCode E e9, @HasDeterministicTerminatingEqualsAndHashCode E e10) { return null; } - static java.util.Set copyOf(java.util.Collection coll) { return null; } + static java.util.Set copyOf(@MustBeSafeLibraryCollection java.util.Collection coll) { return null; } } \ No newline at end of file diff --git a/io-hotmoka-whitelisting/src/main/java/module-info.java b/io-hotmoka-whitelisting/src/main/java/module-info.java index 7b02c5bd2..fdfd2eaba 100644 --- a/io-hotmoka-whitelisting/src/main/java/module-info.java +++ b/io-hotmoka-whitelisting/src/main/java/module-info.java @@ -20,7 +20,7 @@ */ module io.hotmoka.whitelisting { exports io.hotmoka.whitelisting; - opens io.hotmoka.whitelisting.internal.checks; // they are accessed by reflection + opens io.hotmoka.whitelisting.internal.checks; // its needs to be accessed by reflection requires transitive io.hotmoka.whitelisting.api; requires java.logging;