diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index f267314a448..8584edb2dd8 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1119,8 +1119,8 @@ module INT syntax Int ::= freshInt(Int) [freshGenerator, function, functional] rule freshInt(I:Int) => I - syntax Int ::= randInt(Int) [function, hook(INT.rand)] - syntax K ::= srandInt(Int) [function, hook(INT.srand)] + syntax Int ::= randInt(Int) [function, hook(INT.rand), impure] + syntax K ::= srandInt(Int) [function, hook(INT.srand), impure] endmodule ``` diff --git a/k-distribution/tests/regression-new/checks/invalidConstantExp.k b/k-distribution/tests/regression-new/checks/invalidConstantExp.k new file mode 100644 index 00000000000..61f82c1db44 --- /dev/null +++ b/k-distribution/tests/regression-new/checks/invalidConstantExp.k @@ -0,0 +1,6 @@ +module INVALIDCONSTANTEXP + imports INT + + rule 0 => 1 /Int 0 + +endmodule diff --git a/k-distribution/tests/regression-new/checks/invalidConstantExp.k.out b/k-distribution/tests/regression-new/checks/invalidConstantExp.k.out new file mode 100644 index 00000000000..879f66bd996 --- /dev/null +++ b/k-distribution/tests/regression-new/checks/invalidConstantExp.k.out @@ -0,0 +1,6 @@ +[Error] Compiler: Division by zero. + while executing phase "constant expression folding" on sentence at + Source(invalidConstantExp.k) + Location(4,8,4,21) + Source(invalidConstantExp.k) + Location(4,13,4,21) diff --git a/k-distribution/tests/regression-new/constant-folding/1.test b/k-distribution/tests/regression-new/constant-folding/1.test new file mode 100644 index 00000000000..00750edc07d --- /dev/null +++ b/k-distribution/tests/regression-new/constant-folding/1.test @@ -0,0 +1 @@ +3 diff --git a/k-distribution/tests/regression-new/constant-folding/1.test.out b/k-distribution/tests/regression-new/constant-folding/1.test.out new file mode 100644 index 00000000000..19e2468eaf1 --- /dev/null +++ b/k-distribution/tests/regression-new/constant-folding/1.test.out @@ -0,0 +1,3 @@ + + . + diff --git a/k-distribution/tests/regression-new/constant-folding/2.test b/k-distribution/tests/regression-new/constant-folding/2.test new file mode 100644 index 00000000000..b4de3947675 --- /dev/null +++ b/k-distribution/tests/regression-new/constant-folding/2.test @@ -0,0 +1 @@ +11 diff --git a/k-distribution/tests/regression-new/constant-folding/2.test.out b/k-distribution/tests/regression-new/constant-folding/2.test.out new file mode 100644 index 00000000000..19e2468eaf1 --- /dev/null +++ b/k-distribution/tests/regression-new/constant-folding/2.test.out @@ -0,0 +1,3 @@ + + . + diff --git a/k-distribution/tests/regression-new/constant-folding/3.test b/k-distribution/tests/regression-new/constant-folding/3.test new file mode 100644 index 00000000000..7ed6ff82de6 --- /dev/null +++ b/k-distribution/tests/regression-new/constant-folding/3.test @@ -0,0 +1 @@ +5 diff --git a/k-distribution/tests/regression-new/constant-folding/3.test.out b/k-distribution/tests/regression-new/constant-folding/3.test.out new file mode 100644 index 00000000000..a4072584b3e --- /dev/null +++ b/k-distribution/tests/regression-new/constant-folding/3.test.out @@ -0,0 +1,3 @@ + + 5 ~> . + diff --git a/k-distribution/tests/regression-new/constant-folding/Makefile b/k-distribution/tests/regression-new/constant-folding/Makefile new file mode 100644 index 00000000000..d48aaade4fd --- /dev/null +++ b/k-distribution/tests/regression-new/constant-folding/Makefile @@ -0,0 +1,7 @@ +DEF=test +EXT=test +TESTDIR=. +KOMPILE_BACKEND=llvm +KOMPILE_FLAGS=--syntax-module TEST + +include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/constant-folding/test.k b/k-distribution/tests/regression-new/constant-folding/test.k new file mode 100644 index 00000000000..e7bce3a5c30 --- /dev/null +++ b/k-distribution/tests/regression-new/constant-folding/test.k @@ -0,0 +1,15 @@ +module TEST + imports INT + imports STRING + imports ID + + syntax Int ::= "foo" | "bar" + + syntax Id ::= "main" [token] + + rule foo => 1 +Int 2 [macro] + rule foo => .K + + rule bar => 1 +Int 2 *Int lengthString(Id2String(main) +String substrString("foo", 0, 1)) [macro] + rule bar => .K +endmodule diff --git a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java index c3280e352ea..2b21927f9b5 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java +++ b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java @@ -11,6 +11,7 @@ import org.kframework.compile.Backend; import org.kframework.compile.ConcretizeCells; import org.kframework.compile.ConfigurationInfoFromModule; +import org.kframework.compile.ConstantFolding; import org.kframework.compile.ExpandMacros; import org.kframework.compile.GenerateCoverage; import org.kframework.compile.GeneratedTopFormat; @@ -141,6 +142,7 @@ public Function steps() { ResolveFunctionWithConfig transformer = new ResolveFunctionWithConfig(d, true); return DefinitionTransformer.fromSentenceTransformer((m, s) -> new ExpandMacros(transformer, m, files, kem, kompileOptions, false, excludedModuleTags().contains(Att.CONCRETE())).expand(s), "expand macros").apply(d); }; + DefinitionTransformer constantFolding = DefinitionTransformer.fromSentenceTransformer(new ConstantFolding()::fold, "constant expression folding"); Function1 resolveFreshConstants = d -> DefinitionTransformer.from(m -> GeneratedTopFormat.resolve(new ResolveFreshConstants(d, true).resolve(m)), "resolving !Var variables").apply(d); GenerateCoverage cov = new GenerateCoverage(kompileOptions.coverage, files); Function1 genCoverage = d -> DefinitionTransformer.fromRuleBodyTransformerWithRule((r, body) -> cov.gen(r, body, d.mainModule()), "generate coverage instrumentation").apply(d); @@ -160,6 +162,7 @@ public Function steps() { .andThen(subsortKItem) .andThen(generateSortPredicateSyntax) .andThen(generateSortProjections) + .andThen(constantFolding) .andThen(expandMacros) .andThen(guardOrs) .andThen(AddImplicitComputationCell::transformDefinition) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java new file mode 100644 index 00000000000..5fb88fbd94f --- /dev/null +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -0,0 +1,723 @@ +// Copyright (c) 2021 K Team. All Rights Reserved. +package org.kframework.compile; + +import org.apache.commons.lang3.StringUtils; +import org.kframework.attributes.Att; +import org.kframework.builtin.Hooks; +import org.kframework.definition.Module; +import org.kframework.definition.Rule; +import org.kframework.definition.Sentence; +import org.kframework.kore.K; +import org.kframework.kore.KApply; +import org.kframework.kore.KToken; +import org.kframework.kore.Sort; +import org.kframework.kore.TransformK; +import org.kframework.utils.errorsystem.KEMException; +import org.kframework.utils.StringUtil; +import org.kframework.mpfr.BigFloat; +import org.kframework.mpfr.BinaryMathContext; + +import java.lang.reflect.InvocationTargetException; +import java.lang.reflect.Method; +import java.math.BigInteger; +import java.math.RoundingMode; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + +import static org.kframework.Collections.*; +import static org.kframework.kore.KORE.*; +import static org.kframework.definition.Constructors.*; + +public class ConstantFolding { + + private static final List hookNamespaces = Arrays.asList(Hooks.BOOL, Hooks.FLOAT, Hooks.INT, Hooks.STRING); + + private K loc; + + void setLoc(K loc) { + this.loc = loc; + } + + public Sentence fold(Module module, Sentence sentence) { + if (sentence instanceof Rule) { + Rule r = (Rule)sentence; + return Rule(fold(module, r.body(), true), fold(module, r.requires(), false), fold(module, r.ensures(), false), r.att()); + } + return sentence; + } + + public K fold(Module module, K body, boolean isBody) { + return new RewriteAwareTransformer(isBody) { + @Override + public K apply(KApply k) { + if (isLHS() || !isRHS()) { + return super.apply(k); + } + Att att = module.attributesFor().get(k.klabel()).getOrElse(() -> Att()); + if (att.contains(Att.HOOK()) && !att.contains(Att.IMPURE())) { + String hook = att.get(Att.HOOK()); + if (hookNamespaces.stream().anyMatch(ns -> hook.startsWith(ns + "."))) { + List args = new ArrayList<>(); + for (K arg : k.items()) { + K expanded = apply(arg); + if (!(expanded instanceof KToken)) { + return super.apply(k); + } + args.add(expanded); + } + try { + loc = k; + return doFolding(hook, args, module.productionsFor().apply(k.klabel().head()).head().substitute(k.klabel().params()).sort(), module); + } catch (NoSuchMethodException e) { + throw KEMException.internalError("Missing constant-folding implementation for hook " + hook, e); + } + } + } + return super.apply(k); + } + }.apply(body); + } + + private Class classOf(String hook) { + switch(hook) { + case "BOOL.Bool": + return boolean.class; + case "FLOAT.Float": + return FloatBuiltin.class; + case "INT.Int": + return BigInteger.class; + case "STRING.String": + return String.class; + default: + return String.class; + } + } + + private Object unwrap(String token, String hook) { + switch(hook) { + case "BOOL.Bool": + return Boolean.valueOf(token); + case "FLOAT.Float": + return FloatBuiltin.of(token); + case "INT.Int": + return new BigInteger(token); + case "STRING.String": + return StringUtil.unquoteKString(token); + default: + return token; + } + } + + private K wrap(Object result, Sort sort) { + if (result instanceof Boolean) { + return KToken(result.toString(), sort); + } else if (result instanceof FloatBuiltin) { + return KToken(((FloatBuiltin)result).value(), sort); + } else if (result instanceof BigInteger) { + return KToken(result.toString(), sort); + } else if (result instanceof String) { + return KToken(StringUtil.enquoteKString((String)result), sort); + } else { + return KToken(result.toString(), sort); + } + } + + private K doFolding(String hook, List args, Sort resultSort, Module module) throws NoSuchMethodException { + String renamedHook = hook.replace('.', '_'); + List> paramTypes = new ArrayList<>(); + List unwrappedArgs = new ArrayList<>(); + for (K arg : args) { + KToken tok = (KToken)arg; + Sort sort = tok.sort(); + String argHook = module.sortAttributesFor().apply(sort.head()).getOptional(Att.HOOK()).orElse(""); + paramTypes.add(classOf(argHook)); + unwrappedArgs.add(unwrap(tok.s(), argHook)); + } + try { + Method m = ConstantFolding.class.getDeclaredMethod(renamedHook, paramTypes.toArray(new Class[args.size()])); + Object result = m.invoke(this, unwrappedArgs.toArray(new Object[args.size()])); + return wrap(result, resultSort); + } catch (IllegalAccessException e) { + throw KEMException.internalError("Error invoking constant folding function", e); + } catch (InvocationTargetException e) { + if (e.getCause() instanceof KEMException) { + throw (KEMException)e.getCause(); + } else { + throw KEMException.internalError("Error invoking constant folding function", e); + } + } + } + + boolean BOOL_not(boolean a) { + return ! a; + } + + boolean BOOL_and(boolean a, boolean b) { + return a && b; + } + + boolean BOOL_andThen(boolean a, boolean b) { + return a && b; + } + + boolean BOOL_xor(boolean a, boolean b) { + return (a && !b) || (b && !a); + } + + boolean BOOL_or(boolean a, boolean b) { + return a || b; + } + + boolean BOOL_orElse(boolean a, boolean b) { + return a || b; + } + + boolean BOOL_implies(boolean a, boolean b) { + return ! a || b; + } + + boolean BOOL_eq(boolean a, boolean b) { + return a == b; + } + + boolean BOOL_ne(boolean a, boolean b) { + return a != b; + } + + String STRING_concat(String a, String b) { + return a + b; + } + + BigInteger STRING_length(String a) { + return BigInteger.valueOf(a.codePointCount(0, a.length())); + } + + String STRING_chr(BigInteger a) { + // unicode code points range from 0x0 to 0x10ffff + if (a.compareTo(BigInteger.ZERO) < 0 || a.compareTo(BigInteger.valueOf(0x10ffff)) > 0) { + throw KEMException.compilerError("Argument to hook STRING.chr out of range. Expected a number between 0 and 1114111.", loc); + } + int[] codePoint = new int[] { a.intValue() }; + return new String(codePoint, 0, 1); + } + + BigInteger STRING_ord(String a) { + if (a.codePointCount(0, a.length()) != 1) { + throw KEMException.compilerError("Argument to hook STRING.ord out of range. Expected a single character."); + } + return BigInteger.valueOf(a.codePointAt(0)); + } + + private void throwIfNotInt(BigInteger i, String hook) { + if (i.compareTo(BigInteger.valueOf(Integer.MIN_VALUE)) < 0 || i.compareTo(BigInteger.valueOf(Integer.MAX_VALUE)) > 0) { + throw KEMException.compilerError("Argument to hook " + hook + " out of range. Expected a 32-bit signed integer.", loc); + } + } + + private void throwIfNotUnsignedInt(BigInteger i, String hook) { + if (i.compareTo(BigInteger.ZERO) < 0 || i.compareTo(BigInteger.valueOf(Integer.MAX_VALUE)) > 0) { + throw KEMException.compilerError("Argument to hook " + hook + " out of range. Expected a 32-bit unsigned integer.", loc); + } + } + + String STRING_substr(String s, BigInteger start, BigInteger end) { + throwIfNotUnsignedInt(start, "STRING.substr"); + throwIfNotUnsignedInt(end, "STRING.substr"); + try { + return s.substring(s.offsetByCodePoints(0, start.intValue()), s.offsetByCodePoints(0, end.intValue())); + } catch (IndexOutOfBoundsException e) { + throw KEMException.compilerError("Argument to hook STRING.substr out of range. Expected two indices >= 0 and <= the length of the string.", e, loc); + } + } + + BigInteger STRING_find(String haystack, String needle, BigInteger idx) { + throwIfNotUnsignedInt(idx, "STRING.find"); + try { + int offset = haystack.offsetByCodePoints(0, idx.intValue()); + int foundOffset = haystack.indexOf(needle, offset); + return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + } catch(IndexOutOfBoundsException e) { + throw KEMException.compilerError("Argument to hook STRING.find out of range. Expected an index >= 0 and <= the length of the string to search.", e, loc); + } + } + + BigInteger STRING_rfind(String haystack, String needle, BigInteger idx) { + throwIfNotUnsignedInt(idx, "STRING.rfind"); + try { + int offset = haystack.offsetByCodePoints(0, idx.intValue()); + int foundOffset = haystack.lastIndexOf(needle, offset); + return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + } catch(IndexOutOfBoundsException e) { + throw KEMException.compilerError("Argument to hook STRING.rfind out of range. Expected an index >= 0 and <= the length of the string to search.", e, loc); + } + } + + BigInteger STRING_findChar(String haystack, String needles, BigInteger idx) { + throwIfNotUnsignedInt(idx, "STRING.findChar"); + try { + int offset = haystack.offsetByCodePoints(0, idx.intValue()); + int foundOffset = StringUtil.indexOfAny(haystack, needles, offset); + return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + } catch(IndexOutOfBoundsException e) { + throw KEMException.compilerError("Argument to hook STRING.findChar out of range. Expected an index >= 0 and <= the length of the string to search.", e, loc); + } + } + + BigInteger STRING_rfindChar(String haystack, String needles, BigInteger idx) { + throwIfNotUnsignedInt(idx, "STRING.rfindChar"); + try { + int offset = haystack.offsetByCodePoints(0, idx.intValue()); + int foundOffset = StringUtil.lastIndexOfAny(haystack, needles, offset); + return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + } catch(IndexOutOfBoundsException e) { + throw KEMException.compilerError("Argument to hook STRING.rfindChar out of range. Expected an index >= 0 and <= the length of the string to search.", e, loc); + } + } + + String STRING_float2string(FloatBuiltin f) { + return f.value(); + } + + String STRING_floatFormat(FloatBuiltin f, String format) { + return FloatBuiltin.printKFloat(f.bigFloatValue(), () -> f.bigFloatValue().toString(format)); + } + + FloatBuiltin STRING_string2float(String s) { + try { + return FloatBuiltin.of(s); + } catch (NumberFormatException e) { + throw KEMException.compilerError("Argument to hook STRING.string2float invalid. Expected a valid floating point nuwber.", e, loc); + } + } + + BigInteger STRING_string2int(String s) { + try { + return new BigInteger(s, 10); + } catch (NumberFormatException e) { + throw KEMException.compilerError("Argument to hook STRING.string2int invalid. Expected a valid integer.", e, loc); + } + } + + String STRING_int2string(BigInteger i) { + return i.toString(); + } + + BigInteger STRING_string2base(String s, BigInteger base) { + if (base.compareTo(BigInteger.valueOf(2)) < 0 || base.compareTo(BigInteger.valueOf(36)) > 0) { + throw KEMException.compilerError("Argument to hook STRING.string2base out of range. Expected a number between 2 and 36.", loc); + } + try { + return new BigInteger(s, base.intValue()); + } catch (NumberFormatException e) { + throw KEMException.compilerError("Argument to hook STRING.string2base invalid. Expected a valid integer in base " + base.intValue() + ".", e, loc); + } + } + + String STRING_base2string(BigInteger i, BigInteger base) { + if (base.compareTo(BigInteger.valueOf(2)) < 0 || base.compareTo(BigInteger.valueOf(36)) > 0) { + throw KEMException.compilerError("Argument to hook STRING.string2base out of range. Expected a number between 2 and 36.", loc); + } + return i.toString(base.intValue()); + } + + String STRING_replaceAll(String haystack, String needle, String replacement) { + return StringUtils.replace(haystack, needle, replacement); + } + + String STRING_replace(String haystack, String needle, String replacement, BigInteger times) { + throwIfNotUnsignedInt(times, "STRING.replace"); + return StringUtils.replace(haystack, needle, replacement, times.intValue()); + } + + String STRING_replaceFirst(String haystack, String needle, String replacement) { + return StringUtils.replaceOnce(haystack, needle, replacement); + } + + BigInteger STRING_countAllOccurrences(String haystack, String needle) { + return BigInteger.valueOf(StringUtils.countMatches(haystack, needle)); + } + + boolean STRING_eq(String a, String b) { + return a.equals(b); + } + + boolean STRING_ne(String a, String b) { + return !a.equals(b); + } + + boolean STRING_lt(String a, String b) { + return a.compareTo(b) < 0; + } + + boolean STRING_gt(String a, String b) { + return a.compareTo(b) > 0; + } + + boolean STRING_le(String a, String b) { + return a.compareTo(b) <= 0; + } + + boolean STRING_ge(String a, String b) { + return a.compareTo(b) >= 0; + } + + String STRING_token2string(String token) { + return token; + } + + String STRING_string2token(String str) { + return str; + } + + BigInteger INT_not(BigInteger a) { + return a.not(); + } + + BigInteger INT_pow(BigInteger a, BigInteger b) { + throwIfNotUnsignedInt(b, "INT.pow"); + return a.pow(b.intValue()); + } + + BigInteger INT_powmod(BigInteger a, BigInteger b, BigInteger c) { + try { + return a.modPow(b, c); + } catch(ArithmeticException e) { + throw KEMException.compilerError("Argument to hook INT.powmod is invalid. Modulus must be positive and negative exponents are only allowed when value and modulus are relatively prime.", e, loc); + } + } + + BigInteger INT_mul(BigInteger a, BigInteger b) { + return a.multiply(b); + } + + BigInteger INT_tdiv(BigInteger a, BigInteger b) { + if (b.compareTo(BigInteger.ZERO) == 0) { + throw KEMException.compilerError("Division by zero.", loc); + } + return a.divide(b); + } + + BigInteger INT_tmod(BigInteger a, BigInteger b) { + if (b.compareTo(BigInteger.ZERO) == 0) { + throw KEMException.compilerError("Modulus by zero.", loc); + } + return a.remainder(b); + } + + BigInteger INT_ediv(BigInteger a, BigInteger b) { + if (b.compareTo(BigInteger.ZERO) == 0) { + throw KEMException.compilerError("Division by zero.", loc); + } + return a.subtract(INT_emod(a, b)).divide(b); + } + + BigInteger INT_emod(BigInteger a, BigInteger b) { + if (b.compareTo(BigInteger.ZERO) == 0) { + throw KEMException.compilerError("Division by zero.", loc); + } + BigInteger rem = a.remainder(b); + if (rem.compareTo(BigInteger.ZERO) < 0) { + return rem.add(b.abs()); + } + return rem; + } + + BigInteger INT_add(BigInteger a, BigInteger b) { + return a.add(b); + } + + BigInteger INT_sub(BigInteger a, BigInteger b) { + return a.subtract(b); + } + + BigInteger INT_shr(BigInteger a, BigInteger b) { + throwIfNotUnsignedInt(b, "INT.shr"); + return a.shiftRight(b.intValue()); + } + + BigInteger INT_shl(BigInteger a, BigInteger b) { + throwIfNotUnsignedInt(b, "INT.shl"); + return a.shiftLeft(b.intValue()); + } + + BigInteger INT_and(BigInteger a, BigInteger b) { + return a.and(b); + } + + BigInteger INT_xor(BigInteger a, BigInteger b) { + return a.xor(b); + } + + BigInteger INT_or(BigInteger a, BigInteger b) { + return a.or(b); + } + + BigInteger INT_min(BigInteger a, BigInteger b) { + return a.min(b); + } + + BigInteger INT_max(BigInteger a, BigInteger b) { + return a.max(b); + } + + BigInteger INT_abs(BigInteger a) { + return a.abs(); + } + + BigInteger INT_log2(BigInteger a) { + if (a.compareTo(BigInteger.ZERO) <= 0) { + throw KEMException.compilerError("Argument to hook INT.log2 out of range. Expected a positive integer.", loc); + } + int log2 = 0; + while (a.compareTo(BigInteger.ONE) > 0) { + a = a.shiftRight(1); + log2++; + } + return BigInteger.valueOf(log2); + } + + BigInteger INT_bitRange(BigInteger i, BigInteger index, BigInteger length) { + throwIfNotUnsignedInt(index, "INT.bitRange"); + throwIfNotUnsignedInt(length, "INT.bitRange"); + return i.and(BigInteger.ONE.shiftLeft(length.intValue()).subtract(BigInteger.ONE).shiftLeft(index.intValue())).shiftRight(index.intValue()); + } + + BigInteger INT_signExtendBitRange(BigInteger i, BigInteger index, BigInteger length) { + throwIfNotUnsignedInt(index, "INT.signExtendBitRange"); + throwIfNotUnsignedInt(length, "INT.signExtendBitRange"); + if (length.intValue() == 0) { + return BigInteger.ZERO; + } + if (i.testBit(index.intValue() + length.intValue() - 1)) { + BigInteger max = BigInteger.ONE.shiftLeft(length.intValue() - 1); + BigInteger tmp = INT_bitRange(i, index, length); + tmp = tmp.add(max); + tmp = INT_bitRange(tmp, BigInteger.ZERO, length); + tmp = tmp.subtract(max); + return tmp; + } else { + return INT_bitRange(i, index, length); + } + } + + boolean INT_lt(BigInteger a, BigInteger b) { + return a.compareTo(b) < 0; + } + + boolean INT_gt(BigInteger a, BigInteger b) { + return a.compareTo(b) > 0; + } + + boolean INT_le(BigInteger a, BigInteger b) { + return a.compareTo(b) <= 0; + } + + boolean INT_ge(BigInteger a, BigInteger b) { + return a.compareTo(b) >= 0; + } + + boolean INT_eq(BigInteger a, BigInteger b) { + return a.equals(b); + } + + boolean INT_ne(BigInteger a, BigInteger b) { + return !a.equals(b); + } + + BigInteger FLOAT_precision(FloatBuiltin f) { + return BigInteger.valueOf(f.precision()); + } + + BigInteger FLOAT_exponentBits(FloatBuiltin f) { + return BigInteger.valueOf(f.exponent()); + } + + BigInteger FLOAT_exponent(FloatBuiltin f) { + BinaryMathContext mc = f.getMathContext(); + return BigInteger.valueOf(f.bigFloatValue().exponent(mc.minExponent, mc.maxExponent)); + } + + boolean FLOAT_sign(FloatBuiltin f) { + return f.bigFloatValue().sign(); + } + + boolean FLOAT_isNaN(FloatBuiltin f) { + return f.bigFloatValue().isNaN(); + } + + FloatBuiltin FLOAT_neg(FloatBuiltin f) { + return FloatBuiltin.of(f.bigFloatValue().negate(f.getMathContext()), f.exponent()); + } + + private void throwIfNotMatched(FloatBuiltin a, FloatBuiltin b, String hook) { + if (!a.getMathContext().equals(b.getMathContext())) { + throw KEMException.compilerError("Arguments to hook " + hook + " do not match in exponent bits and precision.", loc); + } + } + + FloatBuiltin FLOAT_pow(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.pow"); + return FloatBuiltin.of(a.bigFloatValue().pow(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_mul(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.mul"); + return FloatBuiltin.of(a.bigFloatValue().multiply(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_div(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.div"); + return FloatBuiltin.of(a.bigFloatValue().divide(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_rem(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.rem"); + return FloatBuiltin.of(a.bigFloatValue().remainder(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_add(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.add"); + return FloatBuiltin.of(a.bigFloatValue().add(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_sub(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.sub"); + return FloatBuiltin.of(a.bigFloatValue().subtract(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_root(FloatBuiltin a, BigInteger b) { + throwIfNotInt(b, "FLOAT.root"); + return FloatBuiltin.of(a.bigFloatValue().root(b.intValue(), a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_abs(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().abs(a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_round(FloatBuiltin a, BigInteger prec, BigInteger exp) { + throwIfNotUnsignedInt(prec, "FLOAT.round"); + throwIfNotUnsignedInt(exp, "FLOAT.round"); + if (prec.intValue() < 2 || exp.intValue() < 2) { + throw KEMException.compilerError("Arguments to hook FLOAT.round are too small. Precision and exponent bits must both be at least 2.", loc); + } + return FloatBuiltin.of(a.bigFloatValue().round(new BinaryMathContext(prec.intValue(), exp.intValue())), exp.intValue()); + } + + FloatBuiltin FLOAT_floor(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().rint(a.getMathContext().withRoundingMode(RoundingMode.FLOOR)), a.exponent()); + } + + FloatBuiltin FLOAT_ceil(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().rint(a.getMathContext().withRoundingMode(RoundingMode.CEILING)), a.exponent()); + } + + FloatBuiltin FLOAT_exp(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().exp(a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_log(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().log(a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_sin(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().sin(a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_cos(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().cos(a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_tan(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().tan(a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_asin(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().asin(a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_acos(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().acos(a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_atan(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().atan(a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_atan2(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.atan2"); + return FloatBuiltin.of(BigFloat.atan2(a.bigFloatValue(), b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_max(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.max"); + return FloatBuiltin.of(BigFloat.max(a.bigFloatValue(), b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_min(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.min"); + return FloatBuiltin.of(BigFloat.min(a.bigFloatValue(), b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + FloatBuiltin FLOAT_maxValue(BigInteger prec, BigInteger exp) { + throwIfNotUnsignedInt(prec, "FLOAT.maxValue"); + throwIfNotUnsignedInt(exp, "FLOAT.maxValue"); + if (prec.intValue() < 2 || exp.intValue() < 2) { + throw KEMException.compilerError("Arguments to hook FLOAT.maxValue are too small. Precision and exponent bits must both be at least 2.", loc); + } + BinaryMathContext mc = new BinaryMathContext(prec.intValue(), exp.intValue()); + return FloatBuiltin.of(BigFloat.maxValue(mc.precision, mc.maxExponent), exp.intValue()); + } + + FloatBuiltin FLOAT_minValue(BigInteger prec, BigInteger exp) { + throwIfNotUnsignedInt(prec, "FLOAT.minValue"); + throwIfNotUnsignedInt(exp, "FLOAT.minValue"); + if (prec.intValue() < 2 || exp.intValue() < 2) { + throw KEMException.compilerError("Arguments to hook FLOAT.minValue are too small. Precision and exponent bits must both be at least 2.", loc); + } + BinaryMathContext mc = new BinaryMathContext(prec.intValue(), exp.intValue()); + return FloatBuiltin.of(BigFloat.minValue(mc.precision, mc.minExponent), exp.intValue()); + } + + boolean FLOAT_lt(FloatBuiltin a, FloatBuiltin b) { + return a.bigFloatValue().lessThan(b.bigFloatValue()); + } + + boolean FLOAT_le(FloatBuiltin a, FloatBuiltin b) { + return a.bigFloatValue().lessThanOrEqualTo(b.bigFloatValue()); + } + + boolean FLOAT_gt(FloatBuiltin a, FloatBuiltin b) { + return a.bigFloatValue().greaterThan(b.bigFloatValue()); + } + + boolean FLOAT_ge(FloatBuiltin a, FloatBuiltin b) { + return a.bigFloatValue().greaterThanOrEqualTo(b.bigFloatValue()); + } + + boolean FLOAT_eq(FloatBuiltin a, FloatBuiltin b) { + return a.bigFloatValue().equalTo(b.bigFloatValue()); + } + + boolean FLOAT_ne(FloatBuiltin a, FloatBuiltin b) { + return !a.bigFloatValue().equalTo(b.bigFloatValue()); + } + + FloatBuiltin FLOAT_int2float(BigInteger a, BigInteger prec, BigInteger exp) { + throwIfNotUnsignedInt(prec, "FLOAT.int2float"); + throwIfNotUnsignedInt(exp, "FLOAT.int2float"); + if (prec.intValue() < 2 || exp.intValue() < 2) { + throw KEMException.compilerError("Arguments to hook FLOAT.int2float are too small. Precision and exponent bits must both be at least 2.", loc); + } + BinaryMathContext mc = new BinaryMathContext(prec.intValue(), exp.intValue()); + return FloatBuiltin.of(new BigFloat(a, mc), exp.intValue()); + } + + BigInteger FLOAT_float2int(FloatBuiltin a) { + try { + return a.bigFloatValue().rint(a.getMathContext()).toBigIntegerExact(); + } catch (ArithmeticException e) { + throw KEMException.compilerError("Argument to hook FLOAT.float2int cannot be rounded to an integer.", e, loc); + } + } +} diff --git a/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java b/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java index be6a9d7d370..93f19726338 100644 --- a/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java +++ b/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java @@ -112,6 +112,14 @@ public BigFloat bigFloatValue() { return value; } + public float floatValue() { + return value.floatValue(); + } + + public double doubleValue() { + return value.doubleValue(); + } + /** * Returns a {@link BinaryMathContext} representing the context to perform arithmetic under. */ @@ -119,6 +127,10 @@ public int exponent() { return exponent; } + public BinaryMathContext getMathContext() { + return new BinaryMathContext(precision(), exponent()); + } + public int precision() { return value.precision(); } @@ -157,4 +169,32 @@ public static String printKFloat(BigFloat value, Supplier toString) { public static String printKFloatSuffix(BigFloat value, int exponent) { return "p" + value.precision() + "x" + exponent; } + + @Override + public int hashCode() { + return value.hashCode() * 31 + exponent; + } + + @Override + public boolean equals(Object object) { + if (object == null) { + return false; + } + if (!object.getClass().equals(FloatBuiltin.class)) { + return false; + } + FloatBuiltin other = (FloatBuiltin)object; + if (!value.equals(other.value)) { + return false; + } + if (exponent != other.exponent) { + return false; + } + return true; + } + + @Override + public String toString() { + return value(); + } } diff --git a/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java b/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java new file mode 100644 index 00000000000..3ec8b7f33b7 --- /dev/null +++ b/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java @@ -0,0 +1,1042 @@ +// Copyright (c) 21 K Team. All Rights Reserved. +package org.kframework.compile; + +import org.junit.Before; +import org.junit.Test; +import org.kframework.mpfr.BigFloat; +import org.kframework.mpfr.BinaryMathContext; +import org.kframework.utils.errorsystem.KEMException; + +import java.math.BigInteger; +import java.util.function.BiFunction; +import java.util.function.Function; + +import static org.junit.Assert.*; +import static org.kframework.kore.KORE.*; + +public class ConstantFoldingTest { + + private ConstantFolding cf; + + @Before + public void setUp() { + cf = new ConstantFolding(); + cf.setLoc(KSequence()); + } + + @Test + public void testNot() { + assertEquals(true, cf.BOOL_not(false)); + assertEquals(false, cf.BOOL_not(true)); + } + + public void assertBinBoolOp(boolean a, boolean b, boolean c, boolean d, BiFunction f) { + assertEquals(a, f.apply(false, false)); + assertEquals(b, f.apply(false, true)); + assertEquals(c, f.apply(true, false)); + assertEquals(d, f.apply(true, true)); + } + + @Test + public void testAnd() { + assertBinBoolOp(false, false, false, true, cf::BOOL_and); + } + + @Test + public void testAndThen() { + assertBinBoolOp(false, false, false, true, cf::BOOL_andThen); + } + + @Test + public void testXor() { + assertBinBoolOp(false, true, true, false, cf::BOOL_xor); + } + + @Test + public void testOr() { + assertBinBoolOp(false, true, true, true, cf::BOOL_or); + } + + @Test + public void testOrElse() { + assertBinBoolOp(false, true, true, true, cf::BOOL_or); + } + + @Test + public void testImplies() { + assertBinBoolOp(true, true, false, true, cf::BOOL_implies); + } + + @Test + public void testBoolEq() { + assertBinBoolOp(true, false, false, true, cf::BOOL_eq); + } + + @Test + public void testBoolNe() { + assertBinBoolOp(false, true, true, false, cf::BOOL_ne); + } + + @Test + public void testConcat() { + assertEquals("", cf.STRING_concat("", "")); + assertEquals("foo", cf.STRING_concat("foo", "")); + assertEquals("foo", cf.STRING_concat("", "foo")); + assertEquals("foo", cf.STRING_concat("f", "oo")); + } + + @Test + public void testLength() { + assertEquals(BigInteger.valueOf(0), cf.STRING_length("")); + assertEquals(BigInteger.valueOf(3), cf.STRING_length("foo")); + assertEquals(BigInteger.valueOf(1), cf.STRING_length("\udbff\udfff")); + } + + @Test + public void testChr() { + assertEquals("\u0000", cf.STRING_chr(BigInteger.valueOf(0))); + assertEquals(" ", cf.STRING_chr(BigInteger.valueOf(32))); + assertEquals("a", cf.STRING_chr(BigInteger.valueOf(97))); + assertEquals("\u1234", cf.STRING_chr(BigInteger.valueOf(0x1234))); + assertEquals("\udbff\udfff", cf.STRING_chr(BigInteger.valueOf(0x10ffff))); + } + + @Test(expected=KEMException.class) + public void testChrError1() { + cf.STRING_chr(BigInteger.valueOf(-1)); + } + + @Test(expected=KEMException.class) + public void testChrError2() { + cf.STRING_chr(BigInteger.valueOf(0x110000)); + } + + @Test + public void testOrd() { + assertEquals(BigInteger.valueOf(0), cf.STRING_ord("\u0000")); + assertEquals(BigInteger.valueOf(32), cf.STRING_ord(" ")); + assertEquals(BigInteger.valueOf(97), cf.STRING_ord("a")); + assertEquals(BigInteger.valueOf(0x1234), cf.STRING_ord("\u1234")); + assertEquals(BigInteger.valueOf(0x10ffff), cf.STRING_ord("\udbff\udfff")); + } + + @Test(expected=KEMException.class) + public void testOrdError1() { + cf.STRING_ord(""); + } + + @Test(expected=KEMException.class) + public void testOrdError2() { + cf.STRING_ord("foo"); + } + + @Test + public void testSubstr() { + assertEquals("", cf.STRING_substr("foo", BigInteger.valueOf(0), BigInteger.valueOf(0))); + assertEquals("", cf.STRING_substr("foo", BigInteger.valueOf(1), BigInteger.valueOf(1))); + assertEquals("", cf.STRING_substr("foo", BigInteger.valueOf(2), BigInteger.valueOf(2))); + assertEquals("f", cf.STRING_substr("foo", BigInteger.valueOf(0), BigInteger.valueOf(1))); + assertEquals("fo", cf.STRING_substr("foo", BigInteger.valueOf(0), BigInteger.valueOf(2))); + assertEquals("foo", cf.STRING_substr("foo", BigInteger.valueOf(0), BigInteger.valueOf(3))); + assertEquals("oo", cf.STRING_substr("foo", BigInteger.valueOf(1), BigInteger.valueOf(3))); + assertEquals("o", cf.STRING_substr("foo", BigInteger.valueOf(2), BigInteger.valueOf(3))); + assertEquals("o", cf.STRING_substr("foo", BigInteger.valueOf(1), BigInteger.valueOf(2))); + } + + @Test(expected=KEMException.class) + public void testSubstrError1() { + cf.STRING_substr("foo", BigInteger.valueOf(1), BigInteger.valueOf(4)); + } + + @Test(expected=KEMException.class) + public void testSubstrError2() { + cf.STRING_substr("foo", BigInteger.valueOf(4), BigInteger.valueOf(5)); + } + + @Test(expected=KEMException.class) + public void testSubstrError3() { + cf.STRING_substr("foo", BigInteger.valueOf(3), BigInteger.valueOf(1)); + } + + @Test(expected=KEMException.class) + public void testSubstError4() { + cf.STRING_substr("foo", BigInteger.valueOf(-1), BigInteger.valueOf(1)); + } + + @Test + public void testFind() { + assertEquals(BigInteger.valueOf(0), cf.STRING_find("foo", "f", BigInteger.valueOf(0))); + assertEquals(BigInteger.valueOf(-1), cf.STRING_find("foo", "f", BigInteger.valueOf(1))); + assertEquals(BigInteger.valueOf(1), cf.STRING_find("foo", "o", BigInteger.valueOf(0))); + assertEquals(BigInteger.valueOf(1), cf.STRING_find("foo", "o", BigInteger.valueOf(1))); + assertEquals(BigInteger.valueOf(2), cf.STRING_find("foo", "o", BigInteger.valueOf(2))); + assertEquals(BigInteger.valueOf(1), cf.STRING_find("foo", "oo", BigInteger.valueOf(0))); + assertEquals(BigInteger.valueOf(-1), cf.STRING_find("foo", "oo", BigInteger.valueOf(2))); + } + + @Test(expected=KEMException.class) + public void testFindError1() { + cf.STRING_find("foo", "f", BigInteger.valueOf(-1)); + } + + @Test(expected=KEMException.class) + public void testFindError2() { + cf.STRING_find("foo", "f", BigInteger.valueOf(4)); + } + + @Test + public void testRFind() { + assertEquals(BigInteger.valueOf(0), cf.STRING_rfind("foo", "f", BigInteger.valueOf(0))); + assertEquals(BigInteger.valueOf(0), cf.STRING_rfind("foo", "f", BigInteger.valueOf(1))); + assertEquals(BigInteger.valueOf(-1), cf.STRING_rfind("foo", "o", BigInteger.valueOf(0))); + assertEquals(BigInteger.valueOf(1), cf.STRING_rfind("foo", "o", BigInteger.valueOf(1))); + assertEquals(BigInteger.valueOf(2), cf.STRING_rfind("foo", "o", BigInteger.valueOf(2))); + assertEquals(BigInteger.valueOf(-1), cf.STRING_rfind("foo", "oo", BigInteger.valueOf(0))); + assertEquals(BigInteger.valueOf(1), cf.STRING_rfind("foo", "oo", BigInteger.valueOf(2))); + } + + @Test(expected=KEMException.class) + public void testRFindError1() { + cf.STRING_rfind("foo", "f", BigInteger.valueOf(-1)); + } + + @Test(expected=KEMException.class) + public void testRFindError2() { + cf.STRING_rfind("foo", "f", BigInteger.valueOf(4)); + } + + @Test + public void testFindChar() { + assertEquals(BigInteger.valueOf(0), cf.STRING_findChar("sandwich", "sw", BigInteger.valueOf(0))); + assertEquals(BigInteger.valueOf(4), cf.STRING_findChar("sandwich", "sw", BigInteger.valueOf(1))); + assertEquals(BigInteger.valueOf(-1), cf.STRING_findChar("sandwich", "s", BigInteger.valueOf(1))); + } + + @Test(expected=KEMException.class) + public void testFindCharError1() { + cf.STRING_findChar("foo", "f", BigInteger.valueOf(-1)); + } + + @Test(expected=KEMException.class) + public void testFindCharError2() { + cf.STRING_findChar("foo", "f", BigInteger.valueOf(4)); + } + + @Test + public void testRFindChar() { + assertEquals(BigInteger.valueOf(0), cf.STRING_rfindChar("sandwich", "sw", BigInteger.valueOf(0))); + assertEquals(BigInteger.valueOf(0), cf.STRING_rfindChar("sandwich", "sw", BigInteger.valueOf(1))); + assertEquals(BigInteger.valueOf(4), cf.STRING_rfindChar("sandwich", "sw", BigInteger.valueOf(7))); + assertEquals(BigInteger.valueOf(-1), cf.STRING_rfindChar("sandwich", "w", BigInteger.valueOf(1))); + } + + @Test(expected=KEMException.class) + public void testRFindCharError1() { + cf.STRING_rfindChar("foo", "f", BigInteger.valueOf(-1)); + } + + @Test(expected=KEMException.class) + public void testRFindCharError2() { + cf.STRING_rfindChar("foo", "f", BigInteger.valueOf(4)); + } + + @Test + public void testFloat2String() { + assertEquals("Infinityp53x11", cf.STRING_float2string(FloatBuiltin.of(BigFloat.positiveInfinity(53), 11))); + assertEquals("NaNp53x11", cf.STRING_float2string(FloatBuiltin.of(BigFloat.NaN(53), 11))); + assertEquals("0e+00p53x11", cf.STRING_float2string(FloatBuiltin.of(BigFloat.zero(53), 11))); + assertEquals("-0e+00p53x11", cf.STRING_float2string(FloatBuiltin.of(BigFloat.negativeZero(53), 11))); + assertEquals("-Infinityp53x11", cf.STRING_float2string(FloatBuiltin.of(BigFloat.negativeInfinity(53), 11))); + assertEquals("1.0000000000000001e-01p53x11", cf.STRING_float2string(FloatBuiltin.of(new BigFloat(0.1, BinaryMathContext.BINARY64), 11))); + } + + @Test + public void testString2Float() { + assertEquals(FloatBuiltin.of(BigFloat.positiveInfinity(53), 11), cf.STRING_string2float("Infinity")); + assertEquals(FloatBuiltin.of(BigFloat.positiveInfinity(24), 8), cf.STRING_string2float("Infinityf")); + assertEquals(FloatBuiltin.of(BigFloat.positiveInfinity(10), 10), cf.STRING_string2float("Infinityp10x10")); + assertEquals(FloatBuiltin.of(BigFloat.NaN(53), 11), cf.STRING_string2float("NaN")); + assertEquals(FloatBuiltin.of(BigFloat.zero(53), 11), cf.STRING_string2float("0.0")); + assertEquals(FloatBuiltin.of(BigFloat.zero(53), 11), cf.STRING_string2float("0e+00")); + assertEquals(FloatBuiltin.of(BigFloat.zero(53), 11), cf.STRING_string2float("0e-00")); + assertEquals(FloatBuiltin.of(BigFloat.negativeZero(53), 11), cf.STRING_string2float("-0.0")); + assertEquals(FloatBuiltin.of(BigFloat.negativeInfinity(53), 11), cf.STRING_string2float("-Infinity")); + assertEquals(FloatBuiltin.of(new BigFloat(0.1, BinaryMathContext.BINARY64), 11), cf.STRING_string2float("0.1")); + assertEquals(FloatBuiltin.of(new BigFloat(0.1f, BinaryMathContext.BINARY32), 8), cf.STRING_string2float("0.1f")); + } + + @Test(expected=KEMException.class) + public void testString2FloatError() { + cf.STRING_string2float("0.0.0"); + } + + @Test + public void testInt2String() { + assertEquals("0", cf.STRING_int2string(BigInteger.valueOf(0))); + assertEquals("1", cf.STRING_int2string(BigInteger.valueOf(1))); + assertEquals("-1", cf.STRING_int2string(BigInteger.valueOf(-1))); + assertEquals("100000000000000000000", cf.STRING_int2string(new BigInteger("100000000000000000000"))); + } + + @Test + public void testString2Int() { + assertEquals(BigInteger.valueOf(0), cf.STRING_string2int("0")); + assertEquals(BigInteger.valueOf(1), cf.STRING_string2int("1")); + assertEquals(BigInteger.valueOf(1), cf.STRING_string2int("+1")); + assertEquals(BigInteger.valueOf(-1), cf.STRING_string2int("-1")); + assertEquals(new BigInteger("100000000000000000000"), cf.STRING_string2int("100000000000000000000")); + } + + @Test(expected=KEMException.class) + public void testString2IntError() { + cf.STRING_string2int("0.0"); + } + + @Test + public void testBase2String() { + assertEquals("1234", cf.STRING_base2string(BigInteger.valueOf(0x1234), BigInteger.valueOf(16))); + assertEquals("1234", cf.STRING_base2string(BigInteger.valueOf(01234), BigInteger.valueOf(8))); + assertEquals("1234", cf.STRING_base2string(BigInteger.valueOf(1234), BigInteger.valueOf(10))); + assertEquals("110", cf.STRING_base2string(BigInteger.valueOf(6), BigInteger.valueOf(2))); + assertEquals("-110", cf.STRING_base2string(BigInteger.valueOf(-6), BigInteger.valueOf(2))); + assertEquals("10", cf.STRING_base2string(BigInteger.valueOf(36), BigInteger.valueOf(36))); + } + + @Test(expected=KEMException.class) + public void testBase2StringError1() { + cf.STRING_base2string(BigInteger.valueOf(0), BigInteger.valueOf(1)); + } + + @Test(expected=KEMException.class) + public void testBase2StringError2() { + cf.STRING_base2string(BigInteger.valueOf(0), BigInteger.valueOf(37)); + } + + @Test + public void testString2Base() { + assertEquals(BigInteger.valueOf(0x1234), cf.STRING_string2base("1234", BigInteger.valueOf(16))); + assertEquals(BigInteger.valueOf(01234), cf.STRING_string2base("1234", BigInteger.valueOf(8))); + assertEquals(BigInteger.valueOf(1234), cf.STRING_string2base("1234", BigInteger.valueOf(10))); + assertEquals(BigInteger.valueOf(6), cf.STRING_string2base("110", BigInteger.valueOf(2))); + assertEquals(BigInteger.valueOf(6), cf.STRING_string2base("+110", BigInteger.valueOf(2))); + assertEquals(BigInteger.valueOf(-6), cf.STRING_string2base("-110", BigInteger.valueOf(2))); + assertEquals(BigInteger.valueOf(36), cf.STRING_string2base("10", BigInteger.valueOf(36))); + } + + @Test(expected=KEMException.class) + public void testString2BaseError1() { + cf.STRING_string2base("0", BigInteger.valueOf(1)); + } + + @Test(expected=KEMException.class) + public void testString2BaseError2() { + cf.STRING_string2base("0", BigInteger.valueOf(37)); + } + + @Test(expected=KEMException.class) + public void testString2BaseError3() { + cf.STRING_string2base("8", BigInteger.valueOf(8)); + } + + @Test(expected=KEMException.class) + public void testString2BaseError4() { + cf.STRING_string2base("g", BigInteger.valueOf(16)); + } + + @Test(expected=KEMException.class) + public void testString2BaseError5() { + cf.STRING_string2base("0.0", BigInteger.valueOf(2)); + } + + @Test + public void testReplaceAll() { + assertEquals("far", cf.STRING_replaceAll("foo", "oo", "ar")); + assertEquals("feeee", cf.STRING_replaceAll("foo", "o", "ee")); + assertEquals("foo", cf.STRING_replaceAll("foo", "bar", "baz")); + } + + @Test + public void testReplace() { + assertEquals("far", cf.STRING_replace("foo", "oo", "ar", BigInteger.valueOf(1))); + assertEquals("feeo", cf.STRING_replace("foo", "o", "ee", BigInteger.valueOf(1))); + assertEquals("feeeeo", cf.STRING_replace("fooo", "o", "ee", BigInteger.valueOf(2))); + assertEquals("foo", cf.STRING_replace("foo", "o", "ee", BigInteger.valueOf(0))); + assertEquals("foo", cf.STRING_replace("foo", "bar", "baz", BigInteger.valueOf(0))); + } + + @Test(expected=KEMException.class) + public void testReplaceError1() { + cf.STRING_replace("foo", "oo", "ar", BigInteger.valueOf(-1)); + } + + @Test(expected=KEMException.class) + public void testReplaceError2() { + cf.STRING_replace("foo", "oo", "ar", BigInteger.valueOf(Long.MAX_VALUE)); + } + + @Test + public void testReplaceFirst() { + assertEquals("far", cf.STRING_replaceFirst("foo", "oo", "ar")); + assertEquals("feeo", cf.STRING_replaceFirst("foo", "o", "ee")); + assertEquals("foo", cf.STRING_replaceFirst("foo", "bar", "baz")); + } + + @Test + public void testCountOccurrences() { + assertEquals(BigInteger.valueOf(1), cf.STRING_countAllOccurrences("foo", "oo")); + assertEquals(BigInteger.valueOf(2), cf.STRING_countAllOccurrences("foo", "o")); + assertEquals(BigInteger.valueOf(0), cf.STRING_countAllOccurrences("foo", "bar")); + } + + @Test + public void testStringEq() { + assertEquals(true, cf.STRING_eq("", "")); + assertEquals(false, cf.STRING_eq("", "foo")); + assertEquals(false, cf.STRING_eq("foo", "")); + assertEquals(true, cf.STRING_eq("foo", "foo")); + } + + @Test + public void testStringNe() { + assertEquals(false, cf.STRING_ne("", "")); + assertEquals(true, cf.STRING_ne("", "foo")); + assertEquals(true, cf.STRING_ne("foo", "")); + assertEquals(false, cf.STRING_ne("foo", "foo")); + } + + @Test + public void testStringLt() { + assertEquals(true, cf.STRING_lt("", "a")); + assertEquals(true, cf.STRING_lt("a", "b")); + assertEquals(true, cf.STRING_lt("a", "aa")); + assertEquals(true, cf.STRING_lt("aa", "b")); + assertEquals(false, cf.STRING_lt("", "")); + assertEquals(false, cf.STRING_lt("a", "")); + assertEquals(false, cf.STRING_lt("b", "a")); + assertEquals(false, cf.STRING_lt("aa", "a")); + assertEquals(false, cf.STRING_lt("b", "aa")); + } + + @Test + public void testStringLe() { + assertEquals(true, cf.STRING_le("", "a")); + assertEquals(true, cf.STRING_le("a", "b")); + assertEquals(true, cf.STRING_le("a", "aa")); + assertEquals(true, cf.STRING_le("aa", "b")); + assertEquals(true, cf.STRING_le("", "")); + assertEquals(false, cf.STRING_le("a", "")); + assertEquals(false, cf.STRING_le("b", "a")); + assertEquals(false, cf.STRING_le("aa", "a")); + assertEquals(false, cf.STRING_le("b", "aa")); + } + + @Test + public void testStringGt() { + assertEquals(false, cf.STRING_gt("", "a")); + assertEquals(false, cf.STRING_gt("a", "b")); + assertEquals(false, cf.STRING_gt("a", "aa")); + assertEquals(false, cf.STRING_gt("aa", "b")); + assertEquals(false, cf.STRING_gt("", "")); + assertEquals(true, cf.STRING_gt("a", "")); + assertEquals(true, cf.STRING_gt("b", "a")); + assertEquals(true, cf.STRING_gt("aa", "a")); + assertEquals(true, cf.STRING_gt("b", "aa")); + } + + @Test + public void testStringGe() { + assertEquals(false, cf.STRING_ge("", "a")); + assertEquals(false, cf.STRING_ge("a", "b")); + assertEquals(false, cf.STRING_ge("a", "aa")); + assertEquals(false, cf.STRING_ge("aa", "b")); + assertEquals(true, cf.STRING_ge("", "")); + assertEquals(true, cf.STRING_ge("a", "")); + assertEquals(true, cf.STRING_ge("b", "a")); + assertEquals(true, cf.STRING_ge("aa", "a")); + assertEquals(true, cf.STRING_ge("b", "aa")); + } + + @Test + public void testIntNot() { + assertEquals(BigInteger.valueOf(-19), cf.INT_not(BigInteger.valueOf(18))); + } + + @Test + public void testIntPow() { + assertEquals(BigInteger.valueOf(1), cf.INT_pow(BigInteger.valueOf(10), BigInteger.valueOf(0))); + assertEquals(BigInteger.valueOf(10), cf.INT_pow(BigInteger.valueOf(10), BigInteger.valueOf(1))); + assertEquals(BigInteger.valueOf(100), cf.INT_pow(BigInteger.valueOf(10), BigInteger.valueOf(2))); + } + + @Test(expected=KEMException.class) + public void testIntPowError() { + cf.INT_pow(BigInteger.valueOf(10), BigInteger.valueOf(-1)); + } + + @Test + public void testIntPowMod() { + assertEquals(BigInteger.valueOf(1), cf.INT_powmod(BigInteger.valueOf(10), BigInteger.valueOf(0), BigInteger.valueOf(7))); + assertEquals(BigInteger.valueOf(3), cf.INT_powmod(BigInteger.valueOf(10), BigInteger.valueOf(1), BigInteger.valueOf(7))); + assertEquals(BigInteger.valueOf(2), cf.INT_powmod(BigInteger.valueOf(10), BigInteger.valueOf(2), BigInteger.valueOf(7))); + assertEquals(BigInteger.valueOf(5), cf.INT_powmod(BigInteger.valueOf(10), BigInteger.valueOf(-1), BigInteger.valueOf(7))); + } + + @Test(expected=KEMException.class) + public void testIntPowModError1() { + cf.INT_powmod(BigInteger.valueOf(10), BigInteger.valueOf(1), BigInteger.valueOf(0)); + } + + @Test(expected=KEMException.class) + public void testIntPowModError2() { + cf.INT_powmod(BigInteger.valueOf(10), BigInteger.valueOf(1), BigInteger.valueOf(-1)); + } + + @Test(expected=KEMException.class) + public void testIntPowModError3() { + cf.INT_powmod(BigInteger.valueOf(10), BigInteger.valueOf(-1), BigInteger.valueOf(5)); + } + + @Test + public void testIntMul() { + assertEquals(BigInteger.valueOf(10), cf.INT_mul(BigInteger.valueOf(5), BigInteger.valueOf(2))); + } + + @Test + public void testIntTDiv() { + assertEquals(BigInteger.valueOf(2), cf.INT_tdiv(BigInteger.valueOf(10), BigInteger.valueOf(5))); + assertEquals(BigInteger.valueOf(2), cf.INT_tdiv(BigInteger.valueOf(7), BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(-2), cf.INT_tdiv(BigInteger.valueOf(7), BigInteger.valueOf(-3))); + assertEquals(BigInteger.valueOf(-2), cf.INT_tdiv(BigInteger.valueOf(-7), BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(2), cf.INT_tdiv(BigInteger.valueOf(-7), BigInteger.valueOf(-3))); + } + + @Test(expected=KEMException.class) + public void testIntTDivError() { + cf.INT_tdiv(BigInteger.valueOf(10), BigInteger.valueOf(0)); + } + + @Test + public void testIntTMod() { + assertEquals(BigInteger.valueOf(0), cf.INT_tmod(BigInteger.valueOf(10), BigInteger.valueOf(5))); + assertEquals(BigInteger.valueOf(1), cf.INT_tmod(BigInteger.valueOf(7), BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(-1), cf.INT_tmod(BigInteger.valueOf(-7), BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(1), cf.INT_tmod(BigInteger.valueOf(7), BigInteger.valueOf(-3))); + assertEquals(BigInteger.valueOf(-1), cf.INT_tmod(BigInteger.valueOf(-7), BigInteger.valueOf(-3))); + } + + @Test(expected=KEMException.class) + public void testIntTModError() { + cf.INT_tmod(BigInteger.valueOf(10), BigInteger.valueOf(0)); + } + + @Test + public void testIntEDiv() { + assertEquals(BigInteger.valueOf(2), cf.INT_ediv(BigInteger.valueOf(10), BigInteger.valueOf(5))); + assertEquals(BigInteger.valueOf(2), cf.INT_ediv(BigInteger.valueOf(7), BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(-2), cf.INT_ediv(BigInteger.valueOf(7), BigInteger.valueOf(-3))); + assertEquals(BigInteger.valueOf(-3), cf.INT_ediv(BigInteger.valueOf(-7), BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(3), cf.INT_ediv(BigInteger.valueOf(-7), BigInteger.valueOf(-3))); + } + + @Test(expected=KEMException.class) + public void testIntEDivError() { + cf.INT_ediv(BigInteger.valueOf(10), BigInteger.valueOf(0)); + } + + @Test + public void testIntEMod() { + assertEquals(BigInteger.valueOf(0), cf.INT_emod(BigInteger.valueOf(10), BigInteger.valueOf(5))); + assertEquals(BigInteger.valueOf(1), cf.INT_emod(BigInteger.valueOf(7), BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(2), cf.INT_emod(BigInteger.valueOf(-7), BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(1), cf.INT_emod(BigInteger.valueOf(7), BigInteger.valueOf(-3))); + assertEquals(BigInteger.valueOf(2), cf.INT_emod(BigInteger.valueOf(-7), BigInteger.valueOf(-3))); + } + + @Test(expected=KEMException.class) + public void testIntEModError() { + cf.INT_emod(BigInteger.valueOf(10), BigInteger.valueOf(0)); + } + + @Test + public void testIntAdd() { + assertEquals(BigInteger.valueOf(5), cf.INT_add(BigInteger.valueOf(2), BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(7), cf.INT_add(BigInteger.valueOf(10), BigInteger.valueOf(-3))); + } + + @Test + public void testIntSub() { + assertEquals(BigInteger.valueOf(5), cf.INT_sub(BigInteger.valueOf(2), BigInteger.valueOf(-3))); + assertEquals(BigInteger.valueOf(7), cf.INT_sub(BigInteger.valueOf(10), BigInteger.valueOf(3))); + } + + @Test + public void testShr() { + assertEquals(BigInteger.valueOf(8), cf.INT_shr(BigInteger.valueOf(32), BigInteger.valueOf(2))); + assertEquals(BigInteger.valueOf(8), cf.INT_shr(BigInteger.valueOf(8), BigInteger.valueOf(0))); + } + + @Test(expected=KEMException.class) + public void testShrError() { + cf.INT_shr(BigInteger.valueOf(8), BigInteger.valueOf(-2)); + } + + @Test + public void testShl() { + assertEquals(BigInteger.valueOf(32), cf.INT_shl(BigInteger.valueOf(8), BigInteger.valueOf(2))); + assertEquals(BigInteger.valueOf(8), cf.INT_shl(BigInteger.valueOf(8), BigInteger.valueOf(0))); + } + + @Test(expected=KEMException.class) + public void testShlError() { + cf.INT_shl(BigInteger.valueOf(32), BigInteger.valueOf(-2)); + } + + @Test + public void testIntAnd() { + assertEquals(BigInteger.valueOf(1), cf.INT_and(BigInteger.valueOf(9), BigInteger.valueOf(3))); + } + + @Test + public void testIntXor() { + assertEquals(BigInteger.valueOf(10), cf.INT_xor(BigInteger.valueOf(9), BigInteger.valueOf(3))); + } + + @Test + public void testIntOr() { + assertEquals(BigInteger.valueOf(11), cf.INT_or(BigInteger.valueOf(9), BigInteger.valueOf(3))); + } + + @Test + public void testIntMin() { + assertEquals(BigInteger.valueOf(1), cf.INT_min(BigInteger.valueOf(1), BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(1), cf.INT_min(BigInteger.valueOf(1), BigInteger.valueOf(1))); + assertEquals(BigInteger.valueOf(-1), cf.INT_min(BigInteger.valueOf(-1), BigInteger.valueOf(1))); + } + + @Test + public void testIntMax() { + assertEquals(BigInteger.valueOf(3), cf.INT_max(BigInteger.valueOf(1), BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(1), cf.INT_max(BigInteger.valueOf(1), BigInteger.valueOf(1))); + assertEquals(BigInteger.valueOf(1), cf.INT_max(BigInteger.valueOf(-1), BigInteger.valueOf(1))); + } + + @Test + public void testIntAbs() { + assertEquals(BigInteger.valueOf(3), cf.INT_abs(BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(3), cf.INT_abs(BigInteger.valueOf(-3))); + assertEquals(BigInteger.valueOf(0), cf.INT_abs(BigInteger.valueOf(0))); + } + + @Test + public void testIntLog2() { + assertEquals(BigInteger.valueOf(0), cf.INT_log2(BigInteger.valueOf(1))); + assertEquals(BigInteger.valueOf(1), cf.INT_log2(BigInteger.valueOf(2))); + assertEquals(BigInteger.valueOf(1), cf.INT_log2(BigInteger.valueOf(3))); + assertEquals(BigInteger.valueOf(2), cf.INT_log2(BigInteger.valueOf(4))); + assertEquals(BigInteger.valueOf(2), cf.INT_log2(BigInteger.valueOf(5))); + assertEquals(BigInteger.valueOf(2), cf.INT_log2(BigInteger.valueOf(7))); + assertEquals(BigInteger.valueOf(3), cf.INT_log2(BigInteger.valueOf(8))); + } + + @Test(expected=KEMException.class) + public void testIntLog2Error1() { + cf.INT_log2(BigInteger.valueOf(0)); + } + + @Test(expected=KEMException.class) + public void testIntLog2Error2() { + cf.INT_log2(BigInteger.valueOf(-1)); + } + + @Test + public void testBitRange() { + assertEquals(BigInteger.valueOf(127), cf.INT_bitRange(BigInteger.valueOf(127), BigInteger.valueOf(0), BigInteger.valueOf(8))); + assertEquals(BigInteger.valueOf(255), cf.INT_bitRange(BigInteger.valueOf(255), BigInteger.valueOf(0), BigInteger.valueOf(8))); + assertEquals(BigInteger.valueOf(64), cf.INT_bitRange(BigInteger.valueOf(128), BigInteger.valueOf(1), BigInteger.valueOf(7))); + assertEquals(BigInteger.valueOf(0), cf.INT_bitRange(BigInteger.valueOf(129), BigInteger.valueOf(1), BigInteger.valueOf(5))); + assertEquals(BigInteger.valueOf(0), cf.INT_bitRange(BigInteger.valueOf(128), BigInteger.valueOf(0), BigInteger.valueOf(0))); + assertEquals(BigInteger.valueOf(0), cf.INT_bitRange(new BigInteger("8040201008040201", 16), BigInteger.valueOf(256), BigInteger.valueOf(8))); + assertEquals(BigInteger.valueOf(12), cf.INT_bitRange(new BigInteger("-710567042938717889665411037832208781722350888143921263584927239275773573551204588944105336352942349727184887589413944684473529682801526123805453895275517072855048781056"), BigInteger.valueOf(32), BigInteger.valueOf(8))); + assertEquals(BigInteger.valueOf(56), cf.INT_bitRange(new BigInteger("697754608693466068295273213726275558775348389513141500672185545754018175722916164768735179047222610843044264325669307777729891642448846794142000"), BigInteger.valueOf(64), BigInteger.valueOf(8))); + } + + @Test(expected=KEMException.class) + public void testBitRangeError1() { + cf.INT_bitRange(BigInteger.valueOf(128), BigInteger.valueOf(0), BigInteger.valueOf(-1)); + } + + @Test(expected=KEMException.class) + public void testBitRangeError2() { + cf.INT_bitRange(BigInteger.valueOf(128), BigInteger.valueOf(-1), BigInteger.valueOf(8)); + } + + @Test + public void testSignExtendBitRange() { + assertEquals(BigInteger.valueOf(-1), cf.INT_signExtendBitRange(BigInteger.valueOf(255), BigInteger.valueOf(0), BigInteger.valueOf(8))); + assertEquals(BigInteger.valueOf(127), cf.INT_signExtendBitRange(BigInteger.valueOf(127), BigInteger.valueOf(0), BigInteger.valueOf(8))); + assertEquals(BigInteger.valueOf(-64), cf.INT_signExtendBitRange(BigInteger.valueOf(128), BigInteger.valueOf(1), BigInteger.valueOf(7))); + assertEquals(BigInteger.valueOf(0), cf.INT_signExtendBitRange(BigInteger.valueOf(129), BigInteger.valueOf(1), BigInteger.valueOf(5))); + assertEquals(BigInteger.valueOf(0), cf.INT_signExtendBitRange(BigInteger.valueOf(128), BigInteger.valueOf(0), BigInteger.valueOf(0))); + } + + @Test(expected=KEMException.class) + public void testSignExtendBitRangeError1() { + cf.INT_signExtendBitRange(BigInteger.valueOf(128), BigInteger.valueOf(0), BigInteger.valueOf(-1)); + } + + @Test(expected=KEMException.class) + public void testSignExtendBitRangeError2() { + cf.INT_signExtendBitRange(BigInteger.valueOf(128), BigInteger.valueOf(-1), BigInteger.valueOf(8)); + } + + @Test + public void testIntLt() { + assertEquals(true, cf.INT_lt(BigInteger.valueOf(-100), BigInteger.valueOf(-1))); + assertEquals(true, cf.INT_lt(BigInteger.valueOf(-1), BigInteger.valueOf(0))); + assertEquals(true, cf.INT_lt(BigInteger.valueOf(0), BigInteger.valueOf(1))); + assertEquals(true, cf.INT_lt(BigInteger.valueOf(1), BigInteger.valueOf(100))); + assertEquals(false, cf.INT_lt(BigInteger.valueOf(0), BigInteger.valueOf(0))); + assertEquals(false, cf.INT_lt(BigInteger.valueOf(-1), BigInteger.valueOf(-100))); + assertEquals(false, cf.INT_lt(BigInteger.valueOf(0), BigInteger.valueOf(-1))); + assertEquals(false, cf.INT_lt(BigInteger.valueOf(1), BigInteger.valueOf(0))); + assertEquals(false, cf.INT_lt(BigInteger.valueOf(100), BigInteger.valueOf(1))); + } + + @Test + public void testIntLe() { + assertEquals(true, cf.INT_le(BigInteger.valueOf(-100), BigInteger.valueOf(-1))); + assertEquals(true, cf.INT_le(BigInteger.valueOf(-1), BigInteger.valueOf(0))); + assertEquals(true, cf.INT_le(BigInteger.valueOf(0), BigInteger.valueOf(1))); + assertEquals(true, cf.INT_le(BigInteger.valueOf(1), BigInteger.valueOf(100))); + assertEquals(true, cf.INT_le(BigInteger.valueOf(0), BigInteger.valueOf(0))); + assertEquals(false, cf.INT_le(BigInteger.valueOf(-1), BigInteger.valueOf(-100))); + assertEquals(false, cf.INT_le(BigInteger.valueOf(0), BigInteger.valueOf(-1))); + assertEquals(false, cf.INT_le(BigInteger.valueOf(1), BigInteger.valueOf(0))); + assertEquals(false, cf.INT_le(BigInteger.valueOf(100), BigInteger.valueOf(1))); + } + + @Test + public void testIntGt() { + assertEquals(false, cf.INT_gt(BigInteger.valueOf(-100), BigInteger.valueOf(-1))); + assertEquals(false, cf.INT_gt(BigInteger.valueOf(-1), BigInteger.valueOf(0))); + assertEquals(false, cf.INT_gt(BigInteger.valueOf(0), BigInteger.valueOf(1))); + assertEquals(false, cf.INT_gt(BigInteger.valueOf(1), BigInteger.valueOf(100))); + assertEquals(false, cf.INT_gt(BigInteger.valueOf(0), BigInteger.valueOf(0))); + assertEquals(true, cf.INT_gt(BigInteger.valueOf(-1), BigInteger.valueOf(-100))); + assertEquals(true, cf.INT_gt(BigInteger.valueOf(0), BigInteger.valueOf(-1))); + assertEquals(true, cf.INT_gt(BigInteger.valueOf(1), BigInteger.valueOf(0))); + assertEquals(true, cf.INT_gt(BigInteger.valueOf(100), BigInteger.valueOf(1))); + } + + @Test + public void testIntGe() { + assertEquals(false, cf.INT_ge(BigInteger.valueOf(-100), BigInteger.valueOf(-1))); + assertEquals(false, cf.INT_ge(BigInteger.valueOf(-1), BigInteger.valueOf(0))); + assertEquals(false, cf.INT_ge(BigInteger.valueOf(0), BigInteger.valueOf(1))); + assertEquals(false, cf.INT_ge(BigInteger.valueOf(1), BigInteger.valueOf(100))); + assertEquals(true, cf.INT_ge(BigInteger.valueOf(0), BigInteger.valueOf(0))); + assertEquals(true, cf.INT_ge(BigInteger.valueOf(-1), BigInteger.valueOf(-100))); + assertEquals(true, cf.INT_ge(BigInteger.valueOf(0), BigInteger.valueOf(-1))); + assertEquals(true, cf.INT_ge(BigInteger.valueOf(1), BigInteger.valueOf(0))); + assertEquals(true, cf.INT_ge(BigInteger.valueOf(100), BigInteger.valueOf(1))); + } + + @Test + public void testIntEq() { + assertEquals(true, cf.INT_eq(BigInteger.valueOf(1), BigInteger.valueOf(1))); + assertEquals(false, cf.INT_eq(BigInteger.valueOf(1), BigInteger.valueOf(0))); + } + + @Test + public void testIntNe() { + assertEquals(false, cf.INT_ne(BigInteger.valueOf(1), BigInteger.valueOf(1))); + assertEquals(true, cf.INT_ne(BigInteger.valueOf(1), BigInteger.valueOf(0))); + } + + @Test + public void testPrecision() { + assertEquals(BigInteger.valueOf(2), cf.FLOAT_precision(FloatBuiltin.of(new BigFloat(1.0, new BinaryMathContext(2, 8)), 8))); + assertEquals(BigInteger.valueOf(24), cf.FLOAT_precision(FloatBuiltin.of(new BigFloat(1.0, BinaryMathContext.BINARY32), 8))); + } + + @Test + public void testExponentBits() { + assertEquals(BigInteger.valueOf(8), cf.FLOAT_exponentBits(FloatBuiltin.of(new BigFloat(1.0, new BinaryMathContext(2, 8)), 8))); + assertEquals(BigInteger.valueOf(11), cf.FLOAT_exponentBits(FloatBuiltin.of(new BigFloat(1.0, BinaryMathContext.BINARY64), 11))); + } + + @Test + public void testExponent() { + assertEquals(BigInteger.valueOf(-127), cf.FLOAT_exponent(FloatBuiltin.of(new BigFloat(0.0, BinaryMathContext.BINARY32), 8))); + assertEquals(BigInteger.valueOf(-127), cf.FLOAT_exponent(FloatBuiltin.of(new BigFloat(-0.0, BinaryMathContext.BINARY32), 8))); + assertEquals(BigInteger.valueOf(128), cf.FLOAT_exponent(FloatBuiltin.of(new BigFloat(1.0/0.0, BinaryMathContext.BINARY32), 8))); + assertEquals(BigInteger.valueOf(128), cf.FLOAT_exponent(FloatBuiltin.of(new BigFloat(0.0/0.0, BinaryMathContext.BINARY32), 8))); + assertEquals(BigInteger.valueOf(2), cf.FLOAT_exponent(FloatBuiltin.of(new BigFloat(4.0, BinaryMathContext.BINARY32), 8))); + assertEquals(BigInteger.valueOf(-127), cf.FLOAT_exponent(FloatBuiltin.of(BigFloat.minValue(24, BinaryMathContext.BINARY32.minExponent), 8))); + assertEquals(BigInteger.valueOf(-126), cf.FLOAT_exponent(FloatBuiltin.of(BigFloat.minNormal(24, BinaryMathContext.BINARY32.minExponent), 8))); + } + + private FloatBuiltin _float(float f) { + return FloatBuiltin.of(new BigFloat(f, BinaryMathContext.BINARY32), 8); + } + + private FloatBuiltin _double(double f) { + return FloatBuiltin.of(new BigFloat(f, BinaryMathContext.BINARY64), 11); + } + + @Test + public void testSign() { + assertEquals(false, cf.FLOAT_sign(_float(0.0f))); + assertEquals(true, cf.FLOAT_sign(_float(-0.0f))); + assertEquals(false, cf.FLOAT_sign(_float(1.0f/0.0f))); + assertEquals(true, cf.FLOAT_sign(_float(-1.0f/0.0f))); + assertEquals(false, cf.FLOAT_sign(_float(1.0f))); + assertEquals(true, cf.FLOAT_sign(_float(-1.0f))); + assertEquals(false, cf.FLOAT_sign(_float(3.0f))); + assertEquals(false, cf.FLOAT_sign(_float(0.5f))); + assertEquals(false, cf.FLOAT_sign(_float(0.0f/0.0f))); + } + + @Test + public void testIsNaN() { + assertEquals(false, cf.FLOAT_isNaN(_float(0.0f))); + assertEquals(false, cf.FLOAT_isNaN(_float(-0.0f))); + assertEquals(false, cf.FLOAT_isNaN(_float(1.0f/0.0f))); + assertEquals(true, cf.FLOAT_isNaN(_float(0.0f/0.0f))); + } + + @Test + public void testFloatNeg() { + testUnaryOp(cf::FLOAT_neg, a -> -a); + } + + private double[] refs = new double[] {0.0, -0.0, 1.0/0.0, -1.0/0.0, 1.0, -1.0, 3.0, 0.5, 0.0/0.0}; + + private void testUnaryOp(Function op, Function refOp) { + for (int i = 0; i < refs.length; i++) { + FloatBuiltin result = op.apply(_double(refs[i])); + double ref = refOp.apply(refs[i]); + assertEquals(ref, result.doubleValue(), Double.MIN_VALUE); + } + } + + private void testBinaryOp(String operator, BiFunction op, BiFunction refOp) { + for (int i = 0; i < refs.length; i++) { + for (int j = 0; j < refs.length; j++) { + FloatBuiltin result = op.apply(_double(refs[i]), _double(refs[j])); + double ref = refOp.apply(refs[i], refs[j]); + assertEquals("Operator " + operator + "(" + refs[i] + "," + refs[j] + ") failed", ref, result.doubleValue(), Double.MIN_VALUE); + } + } + } + + private double pow(double a, double b) { + if (a == 1.0) { + return 1.0; + } + if (a == -1.0 && Double.isInfinite(b)) { + return 1.0; + } + return Math.pow(a, b); + } + + @Test + public void testFloatPow() { + testBinaryOp("pow", cf::FLOAT_pow, this::pow); + } + + @Test + public void testFloatMul() { + testBinaryOp("*", cf::FLOAT_mul, (a, b) -> a*b); + } + + @Test + public void testFloatDiv() { + testBinaryOp("/", cf::FLOAT_div, (a, b) -> a/b); + } + + @Test + public void testFloatRem() { + testBinaryOp("%", cf::FLOAT_rem, (a, b) -> a%b); + } + + @Test + public void testFloatAdd() { + testBinaryOp("+", cf::FLOAT_add, (a, b) -> a+b); + } + + @Test + public void testFloatSub() { + testBinaryOp("-", cf::FLOAT_sub, (a, b) -> a-b); + } + + @Test + public void testRoot() { + testUnaryOp(f -> cf.FLOAT_root(f, BigInteger.valueOf(2)), Math::sqrt); + } + + @Test + public void testFloatAbs() { + testUnaryOp(cf::FLOAT_abs, Math::abs); + } + + @Test + public void testRound() { + assertEquals(12.0, cf.FLOAT_round(_double(10.5), BigInteger.valueOf(2), BigInteger.valueOf(8)).doubleValue(), Double.MIN_VALUE); + assertEquals(8.0, cf.FLOAT_round(_double(9.5), BigInteger.valueOf(2), BigInteger.valueOf(8)).doubleValue(), Double.MIN_VALUE); + assertEquals(10.5f, cf.FLOAT_round(_double(10.5), BigInteger.valueOf(24), BigInteger.valueOf(8)).floatValue(), Double.MIN_VALUE); + assertEquals(9.5f, cf.FLOAT_round(_double(9.5), BigInteger.valueOf(24), BigInteger.valueOf(8)).floatValue(), Double.MIN_VALUE); + } + + @Test + public void testFloor() { + assertEquals(10.0f, cf.FLOAT_floor(_float(10.5f)).floatValue(), Double.MIN_VALUE); + } + + @Test + public void testCeil() { + assertEquals(11.0f, cf.FLOAT_ceil(_float(10.5f)).floatValue(), Double.MIN_VALUE); + } + + @Test + public void testExp() { + testUnaryOp(cf::FLOAT_exp, Math::exp); + } + + @Test + public void testLog() { + testUnaryOp(cf::FLOAT_log, Math::log); + } + + @Test + public void testSin() { + testUnaryOp(cf::FLOAT_sin, Math::sin); + } + + @Test + public void testCos() { + testUnaryOp(cf::FLOAT_cos, Math::cos); + } + + @Test + public void testTan() { + testUnaryOp(cf::FLOAT_tan, Math::tan); + } + + @Test + public void testAsin() { + testUnaryOp(cf::FLOAT_asin, Math::asin); + } + + @Test + public void testAcos() { + testUnaryOp(cf::FLOAT_acos, Math::acos); + } + + @Test + public void testAtan() { + testUnaryOp(cf::FLOAT_atan, Math::atan); + } + + @Test + public void testAtan2() { + testBinaryOp("atan2", cf::FLOAT_atan2, Math::atan2); + } + + @Test + public void testMax() { + testBinaryOp("max", cf::FLOAT_max, this::max); + } + + @Test + public void testMin() { + testBinaryOp("min", cf::FLOAT_min, this::min); + } + + private double min(double a, double b) { + if (a != a) { + return b; + } + if (b != b) { + return a; + } + return Math.min(a, b); + } + + private double max(double a, double b) { + if (a != a) { + return b; + } + if (b != b) { + return a; + } + return Math.max(a, b); + } + + + @Test + public void testMaxValue() { + assertEquals(Float.MAX_VALUE, cf.FLOAT_maxValue(BigInteger.valueOf(24), BigInteger.valueOf(8)).floatValue(), Double.MIN_VALUE); + assertEquals(Double.MAX_VALUE, cf.FLOAT_maxValue(BigInteger.valueOf(53), BigInteger.valueOf(11)).doubleValue(), Double.MIN_VALUE); + } + + @Test + public void testMinValue() { + assertEquals(Float.MIN_VALUE, cf.FLOAT_minValue(BigInteger.valueOf(24), BigInteger.valueOf(8)).floatValue(), Double.MIN_VALUE); + assertEquals(Double.MIN_VALUE, cf.FLOAT_minValue(BigInteger.valueOf(53), BigInteger.valueOf(11)).doubleValue(), Double.MIN_VALUE); + } + + private void testComparisonOp(String operator, BiFunction op, BiFunction refOp) { + for (int i = 0; i < refs.length; i++) { + for (int j = 0; j < refs.length; j++) { + boolean result = op.apply(_double(refs[i]), _double(refs[j])); + boolean ref = refOp.apply(refs[i], refs[j]); + assertEquals("Operator " + operator + "(" + refs[i] + "," + refs[j] + ") failed", ref, result); + } + } + } + + @Test + public void testFloatLt() { + testComparisonOp("<", cf::FLOAT_lt, (a, b) -> a < b); + } + + @Test + public void testFloatGt() { + testComparisonOp(">", cf::FLOAT_gt, (a, b) -> a > b); + } + + @Test + public void testFloatLe() { + testComparisonOp("<=", cf::FLOAT_le, (a, b) -> a <= b); + } + + @Test + public void testFloatGe() { + testComparisonOp(">=", cf::FLOAT_ge, (a, b) -> a >= b); + } + + @Test + public void testFloatEq() { + testComparisonOp("==", cf::FLOAT_eq, (a, b) -> a.doubleValue() == b.doubleValue()); + } + + @Test + public void testFloatNe() { + testComparisonOp("!=", cf::FLOAT_ne, (a, b) -> a.doubleValue() != b.doubleValue()); + } + + @Test + public void testInt2Float() { + assertEquals(8.0, cf.FLOAT_int2float(BigInteger.valueOf(9), BigInteger.valueOf(2), BigInteger.valueOf(8)).doubleValue(), Double.MIN_VALUE); + assertEquals(12.0, cf.FLOAT_int2float(BigInteger.valueOf(11), BigInteger.valueOf(2), BigInteger.valueOf(8)).doubleValue(), Double.MIN_VALUE); + assertEquals(8.0, cf.FLOAT_int2float(BigInteger.valueOf(10), BigInteger.valueOf(2), BigInteger.valueOf(8)).doubleValue(), Double.MIN_VALUE); + assertEquals(10.0, cf.FLOAT_int2float(BigInteger.valueOf(10), BigInteger.valueOf(24), BigInteger.valueOf(8)).doubleValue(), Double.MIN_VALUE); + } + + @Test + public void testFloat2Int() { + assertEquals(BigInteger.valueOf(10), cf.FLOAT_float2int(_double(10.5))); + assertEquals(BigInteger.valueOf(10), cf.FLOAT_float2int(_double(9.5))); + } +} diff --git a/kore/src/main/java/org/kframework/utils/StringUtil.java b/kore/src/main/java/org/kframework/utils/StringUtil.java index d29cf393878..296da43644e 100644 --- a/kore/src/main/java/org/kframework/utils/StringUtil.java +++ b/kore/src/main/java/org/kframework/utils/StringUtil.java @@ -119,10 +119,11 @@ public static int lastIndexOfAny(String str, String search, int offset) { if (str.equals("") || search.equals("")) { return -1; } - for (int i = str.length(), strCodepoint; i > 0; i -= Character.charCount(strCodepoint)) { - strCodepoint = str.codePointBefore(i); - for (int j = search.length(), searchCodepoint; j > 0; j -= Character.charCount(searchCodepoint)) { - searchCodepoint = search.codePointBefore(j); + int start = str.offsetByCodePoints(0, offset); + for (int i = start, strCodepoint; i >= 0; i -= Character.charCount(strCodepoint)) { + strCodepoint = str.codePointAt(i); + for (int j = search.length() - 1, searchCodepoint; j >= 0; j -= Character.charCount(searchCodepoint)) { + searchCodepoint = search.codePointAt(j); if (strCodepoint == searchCodepoint) { return i; } @@ -135,7 +136,8 @@ public static int indexOfAny(String str, String search, int offset) { if (str.equals("") || search.equals("")) { return -1; } - for (int i = 0, strCodepoint; i < str.length(); i += Character.charCount(strCodepoint)) { + int start = str.offsetByCodePoints(0, offset); + for (int i = start, strCodepoint; i < str.length(); i += Character.charCount(strCodepoint)) { strCodepoint = str.codePointAt(i); for (int j = 0, searchCodepoint; j < search.length(); j += Character.charCount(searchCodepoint)) { searchCodepoint = search.codePointAt(j);