From 9bae13f5ac8bd65c415fc3a73b24e0ba615fcbba Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 10 Dec 2024 11:22:19 +0100 Subject: [PATCH] cleaning up towards PR --- .../uka/ilkd/key/ldt/FinalHeapResolution.java | 82 +++++++++ .../uka/ilkd/key/ldt/FinalHeapResolver.java | 163 ------------------ .../proof/init/FinalFieldCodeValidator.java | 137 +++++++++++---- .../proof/init/FinalFieldsPOExtension.java | 4 +- .../key/speclang/jml/JMLSpecExtractor.java | 4 +- .../translation/SLAttributeResolver.java | 4 +- .../init/FinalFieldCodeValidatorTest.java | 4 +- .../init/final/shouldfail/FinalProblem1.java | 17 -- 8 files changed, 195 insertions(+), 220 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolver.java delete mode 100644 key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalProblem1.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java new file mode 100644 index 00000000000..31c9e321cce --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java @@ -0,0 +1,82 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.ldt; + +import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.settings.ProofSettings; +import org.jspecify.annotations.NonNull; + + +/** + * A little helper class to resolve the settings for treatment of final fields. + * + * During the generation of {@link de.uka.ilkd.key.proof.init.ProofOblInput}s, we need to know + * which final-treatment is activated. Also during translation from JML to JavaDL this is needed. + * Unfortunately, the settings are not directly available everywhere, so there is a mechanism to + * remember the setting while it is available in a thread-local variable. This class provides a + * simple interface to access this boolean variable. + * + * The alternative would be to make the settings available at more spots ... + * + * @author Mattias Ulbrich + */ +public class FinalHeapResolution { + + private static final ThreadLocal finalEnabledVariable = new ThreadLocal<>(); + private static final String SETTING = "finalFields"; + private static final String IMMUTABLE_OPTION = SETTING + ":immutable"; + + /** + * Returns whether final fields are treated different from normal fields as immutable data. + * + * If initConfig does not have settings yet, the default settings are used. + * + * @param initConfig the configuration to read the settings from + * @return true if final fields are treated as immutable + */ + public static boolean isFinalEnabled(@NonNull InitConfig initConfig) { + ProofSettings settings = initConfig.getSettings(); + if (settings == null) { + settings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS); + } + return isFinalEnabled(settings); + } + + /** + * Returns whether final fields are treated different from normal fields as immutable data. + * + * @param settings the settings to read the settings from + * @return true if final fields are treated as immutable + */ + public static boolean isFinalEnabled(@NonNull ProofSettings settings) { + return settings.getChoiceSettings().getDefaultChoices().get(SETTING) + .equals(IMMUTABLE_OPTION); + } + + /** + * Remembers the final fields are treated different from normal fields as immutable data + * in a thread-local variable that can be recalled later using {@link #recallIsFinalEnabled()}. + * + * @param initConfig the configuration to read the settings from + */ + public static void rememberIfFinalEnabled(InitConfig initConfig) { + finalEnabledVariable.set(isFinalEnabled(initConfig)); + } + + /** + * Recall a previously stored status regarding the treatment of final fields. + * See {@link #rememberIfFinalEnabled(InitConfig)}. + * + * @return true if final fields are treated as immutable (as recorded earlier) + * @throws IllegalStateException if the variable has not been set before + */ + + public static boolean recallIsFinalEnabled() { + Boolean bool = finalEnabledVariable.get(); + if (bool == null) { + throw new IllegalStateException("Unset final enabled variable"); + } + return bool.booleanValue(); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolver.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolver.java deleted file mode 100644 index 270b3b995d3..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolver.java +++ /dev/null @@ -1,163 +0,0 @@ -/* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.ldt; - -import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.proof.init.InitConfig; -import de.uka.ilkd.key.settings.ProofSettings; - - -public class FinalHeapResolver { - - private static final ThreadLocal finalEnabledVariable = new ThreadLocal<>(); - private static String OPTION = "finalFields"; - - public static boolean isFinalEnabled(InitConfig initConfig) { - ProofSettings settings = initConfig.getSettings(); - if (settings == null) { - settings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS); - } - return isFinalEnabled(settings); - } - - public static boolean isFinalEnabled(ProofSettings settings) { - return settings.getChoiceSettings().getDefaultChoices().get(OPTION) - .equals(OPTION + ":immutable"); - } - - public static boolean recallIsFinalEnabled() { - Boolean bool = finalEnabledVariable.get(); - if (bool == null) { - throw new IllegalStateException("Unset final enabled variable"); - } - return bool.booleanValue(); - } - - public static void rememberIfFinalEnabled(InitConfig initConfig) { - finalEnabledVariable.set(isFinalEnabled(initConfig)); - } - - - -// // see WellDefinednessCheck.isOn() -// public static boolean isFinalEnabled() { -// final String setting = -// ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices().get(OPTION); -// if(setting == null) { -// throw new RuntimeException("The setting for the wdProofs-option is not set."); -// } else if (setting.equals(OPTION + ":immutable")) { -// return true; -// } else if (setting.equals(OPTION + ":other")) { -// return false; -// } else { -// throw new RuntimeException( -// "The setting for the wdProofs-option is not valid: " + setting); -// } -// return bool.booleanValue(); -// } -// -// // see above ... I doubt that this works ... -// public static boolean isFinalEnabled(Services services) { -// final String setting = -// services.getProof().getSettings().getChoiceSettings().getDefaultChoices().get(OPTION); -// if(setting == null) { -// throw new RuntimeException("The setting for the wdProofs-option is not set."); -// } else if (setting.equals(OPTION + ":immutable")) { -// return true; -// } else if (setting.equals(OPTION + ":other")) { -// return false; -// } else { -// throw new RuntimeException( -// "The setting for the wdProofs-option is not valid: " + setting); -// } -// } - - // private final Services services; - // - // public FinalHeapResolver(Services services) { - // this.services = services; - // } - - // public T resolve(T contract) { - // return (T) contract.map(this::resolve, services); - // } - // - // private Term resolve(Term term) { - // if (term == null) { - // // for non-existing clauses in maps. - // return null; - // } - // - // if(services.getTypeConverter().getHeapLDT().isSelectOp(term.op())) { - // return resolveSelect(term); - // } - // - // return resolveDefault(term); - // } - // - // private Term resolveDefault(Term term) { - // Term[] newsubs = null; - // ImmutableArray subs = term.subs(); - // for (int i = 0; i < subs.size(); i++) { - // Term in = subs.get(i); - // Term out = resolve(in); - // if (in != out) { - // if (newsubs == null) { - // newsubs = subs.toArray(new Term[subs.size()]); - // } - // newsubs[i] = out; - // } - // } - // - // if (newsubs == null) { - // return term; - // } else { - // return services.getTermFactory().createTerm(term.op(), newsubs, - // term.boundVars(), term.javaBlock(), term.getLabels()); - // } - // } - // - // private Term resolveSelect(Term term) { - // Term obj = term.sub(1); - // Term field = term.sub(2); - // ProgramVariable pv = getFieldSymbol(field); - // if (pv != null && pv.isFinal()) { - // return services.getTermBuilder().finalDot(pv.sort(), - // resolve(obj), field); - // } - // return resolveDefault(term); - // } - // - // private ProgramVariable getFieldSymbol(Term fieldTerm) { - // Operator op = fieldTerm.op(); - // if (op instanceof Function) { - // final String name = op.name().toString(); - // - // // check for normal attribute - // int endOfClassName = name.indexOf("::$"); - // - // int startAttributeName = endOfClassName + 3; - // - // - // if (endOfClassName < 0) { - // // not a normal attribute, maybe an implicit attribute like ? - // endOfClassName = name.indexOf("::<"); - // startAttributeName = endOfClassName + 2; - // } - // - // if (endOfClassName < 0) { - // return null; - // } - // - // final String className = name.substring(0, endOfClassName); - // final String attributeName = name.substring(startAttributeName); - // - // final ProgramVariable attribute = - // services.getJavaInfo().getAttribute(attributeName, className); - // - // return attribute; - // } - // return null; - // } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java index 2961573c233..80e4570c58d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java @@ -16,37 +16,70 @@ import java.util.Set; /** - * Validates the code of a constructor to ensure that final fields are not read before they are initialized. + * Validates a constructor to ensure that the executed code does not read final fields before they + * have been initialized. This is implemented by a rather straightforward static analysis of the + * code. + *

+ * Currently, the rather rules to be obeyed here are rather strict, but safe: + *

    + *
  • Called methods must not receive 'this' as an explicit parameter.
    • + *
  • 'this' must not be assigned to any field or variable.
    • + *
  • 'final' fields must not be read.
    • + *
  • Methods called on 'this' must be effectively final (not overridable).
    • + *
  • The body of methods called on 'this' must not read any final fields as well. + * (This applies transitively.)
    • + *
+ *

+ * There is some potential for relaxations should the above rules turn out to be too strict + * in practice: + *

    + *
  • Final fields may be read after their initialization (locally and also in called methods). + * This requires a lot more bookkeeping, though.
    • + *
  • Effective 'final'-ness can be relaxed: If every constructor of every subclass is subject + * to this treatment, violations would still be observable by expanding methods, and any + * illegal reads would be revealed. That would require 'super(...)' calls to be expanded + * for analysis.
    • + *
+ *

+ * There are no restrictions for secondary constructors (referring to another constructor + * via 'this(...)'). + *

* - * Currently rather strict: - * - Called methods must not receive 'this' as an explicit parameter - * - 'this' must not be assigned to any field or variable - * - final fields must not be read. - * - Methods called on 'this' must be effectively final (not overridable) - * - Methods called on 'this' must not read any final fields as well. - * - * Potential for relaxaions: - * - Final fields may be read after initialization (locally and in called methods) - * This requires a lot more bookkeeping, though. - * - Effective finalness can be relaxed: If every constructor is subject to this treatment, - * corresponding expansion of the methods would reveal any illegal reads. ... if the super(...) - * calls are expanded for analysis. - * - * If this is a secondary constructor (referring to another constructor via this()), there are no restrictions. + * @author Mattias Ulbrich + * @since 2024-12-10 */ + class FinalFieldCodeValidator { private final InitConfig initConfig; + private final KeYJavaType enclosingClass; + + /** + * Methods that have already been validated so far. + */ private final Set validatedMethods = new IdentityHashSet<>(); + + /** + * Stack of methods currently being validated. Needed to resolve method references. + */ private final Deque methodStack = new ArrayDeque<>(); - private KeYJavaType enclosingClass; - public FinalFieldCodeValidator(InitConfig initConfig) { + private FinalFieldCodeValidator(InitConfig initConfig, KeYJavaType containerType) { this.initConfig = initConfig; + this.enclosingClass = containerType; } + /** + * Validates the given constructor. + * + * The method does not do anything if the constructor is not problematic. + * If the code is deemed problematic a {@link FinalViolationException} is thrown. + * + * @param constructor the constructor to validate + * @param initConfig the init config to be used during validation + * @throws FinalViolationException if the code is considered problematic wrt. final fields + */ public static void validateFinalFields(ProgramMethod constructor, InitConfig initConfig) { - var validator = new FinalFieldCodeValidator(initConfig); - validator.enclosingClass = constructor.getContainerType(); + var validator = new FinalFieldCodeValidator(initConfig, constructor.getContainerType()); if(isSecondaryConstructor(constructor)) { // secondary constructors are fine! return; @@ -54,6 +87,9 @@ public static void validateFinalFields(ProgramMethod constructor, InitConfig ini validator.validate(constructor); } + /* + * Secondary constructors have a 'this(...)' (ThisConstructorReference) as their first statement. + */ private static boolean isSecondaryConstructor(IProgramMethod constructor) { StatementBlock body = constructor.getBody(); if(body == null) { @@ -68,6 +104,10 @@ private static boolean isSecondaryConstructor(IProgramMethod constructor) { return firstStatement instanceof ThisConstructorReference; } + /* + * Recursively validate code and all called methods. + * + */ private void validate(IProgramMethod method) { if(validatedMethods.contains(method)) { return; @@ -87,6 +127,10 @@ private void validate(IProgramMethod method) { validatedMethods.add(method); } + /* + * Recursively validate code and all called methods. Makes case distinctions for different + * program elements. + */ private void validateProgramElement(SyntaxElement element) { if(element instanceof MethodReference methodReference) { validateMethodReference(methodReference); @@ -96,15 +140,26 @@ private void validateProgramElement(SyntaxElement element) { validateFieldReference(fieldReference); } else if(element instanceof Assignment assignment) { validateAssignment(assignment); + } else { + validateChildren(element); } // Case: "string" + this .... not allowed! // Case: Model method calls are as problematic as the rest ... + } + + /* + * Recursively validate all children of the given element. + */ + private void validateChildren(SyntaxElement element) { for(int i = 0; i < element.getChildCount(); i++) { validateProgramElement(element.getChild(i)); } } + /* + * Constructor calls must not leak 'this' to the called constructor. + */ private void validateConstructorReference(ConstructorReference methodReference) { // TODO We have to make sure that on non-static subclass is instantiated here var hasThisArgument = methodReference.getArguments().stream().anyMatch(ThisReference.class::isInstance); @@ -112,8 +167,14 @@ private void validateConstructorReference(ConstructorReference methodReference) if(hasThisArgument) { throw new FinalViolationException("Method call " + methodReference + " leaks 'this' to called method.", methodReference); } + + validateChildren(methodReference); } + /* + * Method calls must not leak 'this' to the called method (other than as receiver) + * Method calls on 'this' must be effectively final and are recursively validated. + */ private void validateMethodReference(MethodReference methodReference) { ReferencePrefix referencePrefix = methodReference.getReferencePrefix(); var calledOnThis = referencePrefix == null || referencePrefix instanceof ThisReference; @@ -128,7 +189,7 @@ private void validateMethodReference(MethodReference methodReference) { if(method.isStatic() || method.isConstructor()) { // local static methods are acutally fine ... // constructor calls are also fine - // TODO (well ... what about inner classes?) + // TODO (well ... what about inner classes? Aren't they evil?) return; } if(!method.isFinal() && !method.isPrivate() && !((ClassType)enclosingClass.getJavaType()).isFinal()) { @@ -136,35 +197,49 @@ private void validateMethodReference(MethodReference methodReference) { } validate(method); } + + validateChildren(methodReference); } private IProgramMethod findMethod(MethodReference methodReference) { - // return the program method for the method reference - // YOu can use enclosingClass to get the class in which the method is defined - // The method is guaranteed to be defined in the enclosing class not in a superclass. - // One can also peek the method stack if needed ... ExecutionContext ec = new ExecutionContext(new TypeRef(enclosingClass), methodStack.peek(), methodReference.getReferencePrefix()); - return methodReference.method(initConfig.getServices(), methodReference.determineStaticPrefixType(initConfig.getServices(), ec), ec); + return methodReference.method(initConfig.getServices(), methodReference.determineStaticPrefixType(initConfig.getServices(), ec), ec); } + /* + * Validate assignments. 'this' must not be assigned to any field or variable. + * References to final fields are ok on the left hand side. + */ private void validateAssignment(Assignment assignment) { + SyntaxElement assignee = assignment.getChild(0); SyntaxElement value = assignment.getChild(1); if (value instanceof ThisReference) { throw new FinalViolationException("'this' is leaked to a field or variable.", assignment); } + if (assignee instanceof FieldReference fr) { + // it is ok to assign to this.finalfield! + validateProgramElement(fr.getReferencePrefix()); + } else { + validateProgramElement(assignee); + } + validateProgramElement(value); } + /* + * Validate field references. Final fields must not be read. (Exception see assignment.) + */ private void validateFieldReference(FieldReference fieldReference) { ReferencePrefix prefix = fieldReference.getReferencePrefix(); ProgramVariable field = fieldReference.getProgramVariable(); if(field.isFinal() && prefix instanceof ThisReference) { throw new FinalViolationException("Final field " + field + " is read.", fieldReference); } + validateChildren(fieldReference); } static class FinalViolationException extends RuntimeException { - private final Position position; + private final PositionInfo position; public FinalViolationException(String message) { this(message, null); @@ -173,16 +248,14 @@ public FinalViolationException(String message) { public FinalViolationException(String message, SyntaxElement syntaxElement) { super(message); if (syntaxElement instanceof SourceElement sourceElement) { - this.position = sourceElement.getStartPosition(); + this.position = sourceElement.getPositionInfo(); } else { this.position = null; } } - public Position getPosition() { + public PositionInfo getPositionInfo() { return position; } } -} - - +} \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldsPOExtension.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldsPOExtension.java index 4054aed70f5..5694dbe358c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldsPOExtension.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldsPOExtension.java @@ -6,7 +6,7 @@ import java.util.List; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.ldt.FinalHeapResolver; +import de.uka.ilkd.key.ldt.FinalHeapResolution; import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.Choice; import de.uka.ilkd.key.logic.Term; @@ -35,7 +35,7 @@ public boolean isPOSupported(ProofOblInput po) { public Term modifyPostTerm(AbstractOperationPO abstractPO, InitConfig proofConfig, Services services, ProgramVariable selfVar, Term postTerm) { - if(!FinalHeapResolver.isFinalEnabled(proofConfig)) { + if(!FinalHeapResolution.isFinalEnabled(proofConfig)) { return postTerm; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java index 44ea359a7f1..fc08e35f07a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java @@ -19,7 +19,7 @@ import de.uka.ilkd.key.java.statement.LabeledStatement; import de.uka.ilkd.key.java.statement.LoopStatement; import de.uka.ilkd.key.java.statement.MergePointStatement; -import de.uka.ilkd.key.ldt.FinalHeapResolver; +import de.uka.ilkd.key.ldt.FinalHeapResolution; import de.uka.ilkd.key.logic.label.ParameterlessTermLabel; import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.op.IProgramMethod; @@ -75,7 +75,7 @@ public final class JMLSpecExtractor implements SpecExtractor { // ------------------------------------------------------------------------- public JMLSpecExtractor(InitConfig initConfig) { - FinalHeapResolver.rememberIfFinalEnabled(initConfig); + FinalHeapResolution.rememberIfFinalEnabled(initConfig); this.services = initConfig.getServices(); this.jsf = new JMLSpecFactory(services); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLAttributeResolver.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLAttributeResolver.java index 4631fe92e4b..f0596c50c77 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLAttributeResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLAttributeResolver.java @@ -10,7 +10,7 @@ import de.uka.ilkd.key.java.declaration.MemberDeclaration; import de.uka.ilkd.key.java.declaration.TypeDeclaration; import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder; -import de.uka.ilkd.key.ldt.FinalHeapResolver; +import de.uka.ilkd.key.ldt.FinalHeapResolution; import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.*; @@ -137,7 +137,7 @@ protected SLExpression doResolving(SLExpression receiver, String name, SLParamet attributeTerm = services.getTermBuilder().staticDot(attribute.sort(), fieldSymbol); } else if (attribute.isFinal() && - FinalHeapResolver.recallIsFinalEnabled()) { + FinalHeapResolution.recallIsFinalEnabled()) { attributeTerm = services.getTermBuilder().finalDot(attribute.sort(), recTerm, fieldSymbol); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidatorTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidatorTest.java index 83dcf87b94a..0520b16ec84 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidatorTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidatorTest.java @@ -25,7 +25,7 @@ public Stream testCodeValidatorParse() throws ProblemLoaderExceptio return testContracts(false, "final/shouldparse"); } - //@TestFactory + @TestFactory public Stream testCodeValidatorFail() throws ProblemLoaderException { return testContracts(true, "final/shouldfail"); } @@ -66,7 +66,7 @@ private void testConstructor(Contract c, KeYEnvironment env) throws ProofInpu ContractPO po = c.createProofObl(env.getInitConfig()); env.createProof(po); } catch(FinalFieldCodeValidator.FinalViolationException fex) { - System.err.println("Position: " + fex.getPosition()); + System.err.println("Position: " + fex.getPositionInfo()); fex.printStackTrace(); throw fex; } diff --git a/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalProblem1.java b/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalProblem1.java deleted file mode 100644 index 8829d75a723..00000000000 --- a/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalProblem1.java +++ /dev/null @@ -1,17 +0,0 @@ -class FinalReadBeforeWriteIndirect { - final int finalField; - - //@ ensures b; - FinalReadBeforeWriteIndirect(boolean b) { - int before = getFinalField(); - finalField = 42; - int after = getFinalField(); - } - - /*@ normal_behaviour - @ ensures \result == finalField; - @*/ - private int getFinalField() { - return finalField; - } -}