From 48aea6058fb81cda905e3e723f16e0f33bf43da7 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 22 Mar 2021 11:48:32 -0500 Subject: [PATCH 01/27] initial constant folding of string, int, boolean --- .../kframework/backend/kore/KoreBackend.java | 3 + .../kframework/compile/ConstantFolding.java | 511 ++++++++++++++++++ 2 files changed, 514 insertions(+) create mode 100644 kernel/src/main/java/org/kframework/compile/ConstantFolding.java 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..16abff0133f --- /dev/null +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -0,0 +1,511 @@ +// 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 java.lang.reflect.InvocationTargetException; +import java.lang.reflect.Method; +import java.math.BigInteger; +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 final List hookNamespaces = Arrays.asList(Hooks.BOOL, Hooks.FLOAT, Hooks.INT, Hooks.MINT, Hooks.STRING); + + private K 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); + } + if (module.attributesFor().get(k.klabel()).getOrElse(() -> Att()).contains(Att.HOOK())) { + String hook = module.attributesFor().apply(k.klabel()).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 static class MIntBuiltin { + public BigInteger i; + public long precision; + + public MIntBuiltin(BigInteger i, long precision) { + this.i = i; + this.precision = precision; + } + } + + 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 "MINT.MInt": + return MIntBuiltin.class; + case "STRING.String": + return String.class; + default: + throw KEMException.internalError("Invalid constant-folding sort"); + } + } + + 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 "MINT.MInt": + int idx = token.indexOf('p'); + if (idx == -1) idx = token.indexOf('P'); + return new MIntBuiltin(new BigInteger(token.substring(0, idx)), Long.valueOf(token.substring(idx+1))); + case "STRING.String": + return StringUtil.unquoteKString(token); + default: + throw KEMException.internalError("Invalid constant-folding sort"); + } + } + + 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 MIntBuiltin) { + return KToken(result.toString(), sort); + } else if (result instanceof String) { + return KToken(StringUtil.enquoteKString((String)result), sort); + } else { + throw KEMException.internalError("Invalid constant-folding 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()).get(Att.HOOK()); + 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); + } + } + } + + private boolean BOOL_not(boolean a) { + return ! a; + } + + private boolean BOOL_and(boolean a, boolean b) { + return a && b; + } + + private boolean BOOL_andThen(boolean a, boolean b) { + return a && b; + } + + private boolean BOOL_xor(boolean a, boolean b) { + return (a && !b) || (b && !a); + } + + private boolean BOOL_or(boolean a, boolean b) { + return a || b; + } + + private boolean BOOL_orElse(boolean a, boolean b) { + return a || b; + } + + private boolean BOOL_implies(boolean a, boolean b) { + return ! a || b; + } + + private boolean BOOL_eq(boolean a, boolean b) { + return a == b; + } + + private boolean BOOL_ne(boolean a, boolean b) { + return a != b; + } + + private String STRING_concat(String a, String b) { + return a + b; + } + + private BigInteger STRING_length(String a) { + return BigInteger.valueOf(a.length()); + } + + private String STRING_chr(BigInteger a) { + 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); + } + + private 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); + } + } + + private String STRING_substr(String s, BigInteger start, BigInteger end) { + throwIfNotInt(start, "STRING.substr"); + throwIfNotInt(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); + } + } + + private BigInteger STRING_find(String haystack, String needle, BigInteger idx) { + throwIfNotInt(idx, "STRING.find"); + int offset = haystack.offsetByCodePoints(0, idx.intValue()); + int foundOffset = haystack.indexOf(needle, offset); + return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + } + + private BigInteger STRING_rfind(String haystack, String needle, BigInteger idx) { + throwIfNotInt(idx, "STRING.rfind"); + int offset = haystack.offsetByCodePoints(0, idx.intValue()); + int foundOffset = haystack.lastIndexOf(needle, offset); + return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + } + + private BigInteger STRING_findChar(String haystack, String needles, BigInteger idx) { + throwIfNotInt(idx, "STRING.findChar"); + int offset = haystack.offsetByCodePoints(0, idx.intValue()); + int foundOffset = StringUtil.indexOfAny(haystack, needles, offset); + return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + } + + private BigInteger STRING_rfindChar(String haystack, String needles, BigInteger idx) { + throwIfNotInt(idx, "STRING.findChar"); + int offset = haystack.offsetByCodePoints(0, idx.intValue()); + int foundOffset = StringUtil.lastIndexOfAny(haystack, needles, offset); + return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + } + + private String STRING_float2string(FloatBuiltin f) { + return FloatBuiltin.printKFloat(f.bigFloatValue(), f.bigFloatValue()::toString); + } + + private String STRING_floatFormat(FloatBuiltin f, String format) { + return FloatBuiltin.printKFloat(f.bigFloatValue(), () -> f.bigFloatValue().toString(format)); + } + + private 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); + } + } + + private 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); + } + } + + private String STRING_int2string(BigInteger i) { + return i.toString(); + } + + private 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); + } + } + + private 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()); + } + + private String STRING_replaceAll(String haystack, String needle, String replacement) { + return StringUtils.replace(haystack, needle, replacement); + } + + private String STRING_replace(String haystack, String needle, String replacement, BigInteger times) { + throwIfNotInt(times, "STRING.replace"); + return StringUtils.replace(haystack, needle, replacement, times.intValue()); + } + + private String STRING_replaceFirst(String haystack, String needle, String replacement) { + return StringUtils.replaceOnce(haystack, needle, replacement); + } + + private BigInteger STRING_countAllOccurrences(String haystack, String needle) { + return BigInteger.valueOf(StringUtils.countMatches(haystack, needle)); + } + + private boolean STRING_eq(String a, String b) { + return a.equals(b); + } + + private boolean STRING_ne(String a, String b) { + return !a.equals(b); + } + + private boolean STRING_lt(String a, String b) { + return a.compareTo(b) < 0; + } + + private boolean STRING_gt(String a, String b) { + return a.compareTo(b) > 0; + } + + private boolean STRING_le(String a, String b) { + return a.compareTo(b) <= 0; + } + + private boolean STRING_ge(String a, String b) { + return a.compareTo(b) >= 0; + } + + private BigInteger INT_not(BigInteger a) { + return a.not(); + } + + private BigInteger INT_pow(BigInteger a, BigInteger b) { + throwIfNotUnsignedInt(b, "INT.pow"); + return a.pow(b.intValue()); + } + + private 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); + } + } + + private BigInteger INT_mul(BigInteger a, BigInteger b) { + return a.multiply(b); + } + + private BigInteger INT_tdiv(BigInteger a, BigInteger b) { + if (b.compareTo(BigInteger.ZERO) == 0) { + throw KEMException.compilerError("Division by zero.", loc); + } + return a.divide(b); + } + + private BigInteger INT_tmod(BigInteger a, BigInteger b) { + if (b.compareTo(BigInteger.ZERO) == 0) { + throw KEMException.compilerError("Modulus by zero.", loc); + } + return a.remainder(b); + } + + private BigInteger INT_ediv(BigInteger a, BigInteger b) { + return a.subtract(a.mod(b)).divide(b); + } + + private BigInteger INT_emod(BigInteger a, BigInteger b) { + return a.mod(b); + } + + private BigInteger INT_add(BigInteger a, BigInteger b) { + return a.add(b); + } + + private BigInteger INT_sub(BigInteger a, BigInteger b) { + return a.subtract(b); + } + + private BigInteger INT_shr(BigInteger a, BigInteger b) { + throwIfNotUnsignedInt(b, "INT.shr"); + return a.shiftRight(b.intValue()); + } + + private BigInteger INT_shl(BigInteger a, BigInteger b) { + throwIfNotUnsignedInt(b, "INT.shl"); + return a.shiftLeft(b.intValue()); + } + + private BigInteger INT_and(BigInteger a, BigInteger b) { + return a.and(b); + } + + private BigInteger INT_xor(BigInteger a, BigInteger b) { + return a.xor(b); + } + + private BigInteger INT_or(BigInteger a, BigInteger b) { + return a.or(b); + } + + private BigInteger INT_min(BigInteger a, BigInteger b) { + return a.min(b); + } + + private BigInteger INT_max(BigInteger a, BigInteger b) { + return a.max(b); + } + + private BigInteger INT_abs(BigInteger a) { + return a.abs(); + } + + private 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); + } + + private BigInteger INT_bitRange(BigInteger i, BigInteger index, BigInteger length) { + throwIfNotUnsignedInt(index, "INT.bitRange"); + throwIfNotUnsignedInt(length, "INT.bitRange"); + byte[] twosComplement = i.toByteArray(); + BigInteger positive = new BigInteger(1, twosComplement); + for (int j = 0; j < index.intValue(); j++) { + i = i.clearBit(j); + } + for (int j = index.intValue() + length.intValue(); j < twosComplement.length * 8; j++) { + i = i.clearBit(j); + } + return i; + } + + private 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); + } + } + + private boolean INT_lt(BigInteger a, BigInteger b) { + return a.compareTo(b) < 0; + } + + private boolean INT_gt(BigInteger a, BigInteger b) { + return a.compareTo(b) > 0; + } + + private boolean INT_le(BigInteger a, BigInteger b) { + return a.compareTo(b) <= 0; + } + + private boolean INT_ge(BigInteger a, BigInteger b) { + return a.compareTo(b) >= 0; + } + + private boolean INT_eq(BigInteger a, BigInteger b) { + return a.equals(b); + } + + private boolean INT_ne(BigInteger a, BigInteger b) { + return !a.equals(b); + } + +} From b94ae11a2620ab4c90b8e99ddc0ca522dc1647a4 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 2 Apr 2021 15:36:37 -0500 Subject: [PATCH 02/27] make rand and srand impure --- k-distribution/include/kframework/builtin/domains.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index ac33e50f6ab..9f7ad4c69f6 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1112,8 +1112,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 ``` From 18217af0733c51cedb04f2f4db976d10a0922737 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 2 Apr 2021 15:37:09 -0500 Subject: [PATCH 03/27] remove MINT from constant folding --- .../kframework/compile/ConstantFolding.java | 20 +------------------ 1 file changed, 1 insertion(+), 19 deletions(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 16abff0133f..ffd21fe9a3c 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -28,7 +28,7 @@ public class ConstantFolding { - private final List hookNamespaces = Arrays.asList(Hooks.BOOL, Hooks.FLOAT, Hooks.INT, Hooks.MINT, Hooks.STRING); + private final List hookNamespaces = Arrays.asList(Hooks.BOOL, Hooks.FLOAT, Hooks.INT, Hooks.STRING); private K loc; @@ -71,16 +71,6 @@ public K apply(KApply k) { }.apply(body); } - private static class MIntBuiltin { - public BigInteger i; - public long precision; - - public MIntBuiltin(BigInteger i, long precision) { - this.i = i; - this.precision = precision; - } - } - private Class classOf(String hook) { switch(hook) { case "BOOL.Bool": @@ -89,8 +79,6 @@ private Class classOf(String hook) { return FloatBuiltin.class; case "INT.Int": return BigInteger.class; - case "MINT.MInt": - return MIntBuiltin.class; case "STRING.String": return String.class; default: @@ -106,10 +94,6 @@ private Object unwrap(String token, String hook) { return FloatBuiltin.of(token); case "INT.Int": return new BigInteger(token); - case "MINT.MInt": - int idx = token.indexOf('p'); - if (idx == -1) idx = token.indexOf('P'); - return new MIntBuiltin(new BigInteger(token.substring(0, idx)), Long.valueOf(token.substring(idx+1))); case "STRING.String": return StringUtil.unquoteKString(token); default: @@ -124,8 +108,6 @@ private K wrap(Object result, Sort sort) { return KToken(((FloatBuiltin)result).value(), sort); } else if (result instanceof BigInteger) { return KToken(result.toString(), sort); - } else if (result instanceof MIntBuiltin) { - return KToken(result.toString(), sort); } else if (result instanceof String) { return KToken(StringUtil.enquoteKString((String)result), sort); } else { From 0bee2687d7ee4889305778435505b05f40609f7f Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 2 Apr 2021 15:37:21 -0500 Subject: [PATCH 04/27] don't fold impure functions --- .../main/java/org/kframework/compile/ConstantFolding.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index ffd21fe9a3c..1205c024026 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -47,8 +47,9 @@ public K apply(KApply k) { if (isLHS() || !isRHS()) { return super.apply(k); } - if (module.attributesFor().get(k.klabel()).getOrElse(() -> Att()).contains(Att.HOOK())) { - String hook = module.attributesFor().apply(k.klabel()).get(Att.HOOK()); + 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()) { From 0407ca5f01aaae875d3c8be03d5807fa5ad1bc79 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 2 Apr 2021 15:37:34 -0500 Subject: [PATCH 05/27] constant folding of tokens --- .../org/kframework/compile/ConstantFolding.java | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 1205c024026..9114257ddb3 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -83,7 +83,7 @@ private Class classOf(String hook) { case "STRING.String": return String.class; default: - throw KEMException.internalError("Invalid constant-folding sort"); + return String.class; } } @@ -98,7 +98,7 @@ private Object unwrap(String token, String hook) { case "STRING.String": return StringUtil.unquoteKString(token); default: - throw KEMException.internalError("Invalid constant-folding sort"); + return token; } } @@ -112,7 +112,7 @@ private K wrap(Object result, Sort sort) { } else if (result instanceof String) { return KToken(StringUtil.enquoteKString((String)result), sort); } else { - throw KEMException.internalError("Invalid constant-folding sort"); + return KToken(result.toString(), sort); } } @@ -123,7 +123,7 @@ private K doFolding(String hook, List args, Sort resultSort, Module module) t for (K arg : args) { KToken tok = (KToken)arg; Sort sort = tok.sort(); - String argHook = module.sortAttributesFor().apply(sort.head()).get(Att.HOOK()); + String argHook = module.sortAttributesFor().apply(sort.head()).getOptional(Att.HOOK()).orElse(""); paramTypes.add(classOf(argHook)); unwrappedArgs.add(unwrap(tok.s(), argHook)); } @@ -338,6 +338,14 @@ private boolean STRING_ge(String a, String b) { return a.compareTo(b) >= 0; } + private String STRING_token2string(String token) { + return token; + } + + private String STRING_string2token(String str) { + return str; + } + private BigInteger INT_not(BigInteger a) { return a.not(); } From 63917306db5b73dc6e3a47c8cc8bc2f856c1cbf6 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 2 Apr 2021 15:40:11 -0500 Subject: [PATCH 06/27] add helper function to FloatBuiltin --- kernel/src/main/java/org/kframework/compile/FloatBuiltin.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java b/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java index be6a9d7d370..c68e95f2bb7 100644 --- a/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java +++ b/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java @@ -119,6 +119,10 @@ public int exponent() { return exponent; } + public BinaryMathContext getMathContext() { + return new BinaryMathContext(precision(), exponent()); + } + public int precision() { return value.precision(); } From c70bacfb70cfb96130157931f57ce815d88c0833 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 2 Apr 2021 15:40:18 -0500 Subject: [PATCH 07/27] float hooks --- .../kframework/compile/ConstantFolding.java | 198 ++++++++++++++++++ 1 file changed, 198 insertions(+) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 9114257ddb3..a6a8e3f85c9 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -14,10 +14,13 @@ 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; @@ -499,4 +502,199 @@ private boolean INT_ne(BigInteger a, BigInteger b) { return !a.equals(b); } + private BigInteger FLOAT_precision(FloatBuiltin f) { + return BigInteger.valueOf(f.precision()); + } + + private BigInteger FLOAT_exponentBits(FloatBuiltin f) { + return BigInteger.valueOf(f.exponent()); + } + + private BigInteger FLOAT_exponent(FloatBuiltin f) { + BinaryMathContext mc = f.getMathContext(); + return BigInteger.valueOf(f.bigFloatValue().exponent(mc.minExponent, mc.maxExponent)); + } + + private boolean FLOAT_sign(FloatBuiltin f) { + return f.bigFloatValue().sign(); + } + + private boolean FLOAT_isNaN(FloatBuiltin f) { + return f.bigFloatValue().isNaN(); + } + + private 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); + } + } + + private FloatBuiltin FLOAT_pow(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.pow"); + return FloatBuiltin.of(a.bigFloatValue().pow(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_mul(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.mul"); + return FloatBuiltin.of(a.bigFloatValue().multiply(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_div(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.div"); + return FloatBuiltin.of(a.bigFloatValue().divide(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_rem(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.rem"); + return FloatBuiltin.of(a.bigFloatValue().remainder(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_add(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.add"); + return FloatBuiltin.of(a.bigFloatValue().add(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_sub(FloatBuiltin a, FloatBuiltin b) { + throwIfNotMatched(a, b, "FLOAT.sub"); + return FloatBuiltin.of(a.bigFloatValue().subtract(b.bigFloatValue(), a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_root(FloatBuiltin a, BigInteger b) { + throwIfNotInt(b, "FLOAT.root"); + return FloatBuiltin.of(a.bigFloatValue().root(b.intValue(), a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_abs(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().abs(a.getMathContext()), a.exponent()); + } + + private 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()); + } + + private FloatBuiltin FLOAT_floor(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().rint(a.getMathContext().withRoundingMode(RoundingMode.FLOOR)), a.exponent()); + } + + private FloatBuiltin FLOAT_ceil(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().rint(a.getMathContext().withRoundingMode(RoundingMode.CEILING)), a.exponent()); + } + + private FloatBuiltin FLOAT_exp(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().exp(a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_log(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().log(a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_sin(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().sin(a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_cos(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().cos(a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_tan(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().tan(a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_asin(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().asin(a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_acos(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().acos(a.getMathContext()), a.exponent()); + } + + private FloatBuiltin FLOAT_atan(FloatBuiltin a) { + return FloatBuiltin.of(a.bigFloatValue().atan(a.getMathContext()), a.exponent()); + } + + private 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()); + } + + private 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()); + } + + private 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()); + } + + private 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()); + } + + private 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()); + } + + private boolean FLOAT_lt(FloatBuiltin a, FloatBuiltin b) { + return a.bigFloatValue().lessThan(b.bigFloatValue()); + } + + private boolean FLOAT_le(FloatBuiltin a, FloatBuiltin b) { + return a.bigFloatValue().lessThanOrEqualTo(b.bigFloatValue()); + } + + private boolean FLOAT_gt(FloatBuiltin a, FloatBuiltin b) { + return a.bigFloatValue().greaterThan(b.bigFloatValue()); + } + + private boolean FLOAT_ge(FloatBuiltin a, FloatBuiltin b) { + return a.bigFloatValue().greaterThanOrEqualTo(b.bigFloatValue()); + } + + private boolean FLOAT_eq(FloatBuiltin a, FloatBuiltin b) { + return a.bigFloatValue().equalTo(b.bigFloatValue()); + } + + private boolean FLOAT_ne(FloatBuiltin a, FloatBuiltin b) { + return !a.bigFloatValue().equalTo(b.bigFloatValue()); + } + + private 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()); + } + + private BigInteger FLOAT_float2int(FloatBuiltin a) { + try { + return a.bigFloatValue().rint(a.getMathContext().withRoundingMode(RoundingMode.DOWN)).toBigIntegerExact(); + } catch (ArithmeticException e) { + throw KEMException.compilerError("Argument to hook FLOAT.float2int cannot be rounded to an integer.", e, loc); + } + } } From 55a57c6a357c4ea8b3ddeb8715f8ed113a232f12 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 2 Apr 2021 15:48:38 -0500 Subject: [PATCH 08/27] fix whitespace --- .../src/main/java/org/kframework/compile/ConstantFolding.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index a6a8e3f85c9..0b211d3b157 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -261,7 +261,7 @@ private String STRING_float2string(FloatBuiltin f) { private String STRING_floatFormat(FloatBuiltin f, String format) { return FloatBuiltin.printKFloat(f.bigFloatValue(), () -> f.bigFloatValue().toString(format)); } - + private FloatBuiltin STRING_string2float(String s) { try { return FloatBuiltin.of(s); @@ -292,7 +292,7 @@ private BigInteger STRING_string2base(String s, BigInteger base) { throw KEMException.compilerError("Argument to hook STRING.string2base invalid. Expected a valid integer in base " + base.intValue() + ".", e, loc); } } - + private 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); From 57abe2ee777b00e2e2c682e11e64fe989c653263 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 7 Apr 2021 14:08:23 -0500 Subject: [PATCH 09/27] make field static --- .../src/main/java/org/kframework/compile/ConstantFolding.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 0b211d3b157..cd000956998 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -31,7 +31,7 @@ public class ConstantFolding { - private final List hookNamespaces = Arrays.asList(Hooks.BOOL, Hooks.FLOAT, Hooks.INT, Hooks.STRING); + private static final List hookNamespaces = Arrays.asList(Hooks.BOOL, Hooks.FLOAT, Hooks.INT, Hooks.STRING); private K loc; From a4c198fd0493a394cc8ea10bcc1b5e7d42f10b99 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 7 Apr 2021 14:08:36 -0500 Subject: [PATCH 10/27] make hooks package-private --- .../kframework/compile/ConstantFolding.java | 204 +++++++++--------- 1 file changed, 102 insertions(+), 102 deletions(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index cd000956998..71fc6119314 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -145,51 +145,51 @@ private K doFolding(String hook, List args, Sort resultSort, Module module) t } } - private boolean BOOL_not(boolean a) { + boolean BOOL_not(boolean a) { return ! a; } - private boolean BOOL_and(boolean a, boolean b) { + boolean BOOL_and(boolean a, boolean b) { return a && b; } - private boolean BOOL_andThen(boolean a, boolean b) { + boolean BOOL_andThen(boolean a, boolean b) { return a && b; } - private boolean BOOL_xor(boolean a, boolean b) { + boolean BOOL_xor(boolean a, boolean b) { return (a && !b) || (b && !a); } - private boolean BOOL_or(boolean a, boolean b) { + boolean BOOL_or(boolean a, boolean b) { return a || b; } - private boolean BOOL_orElse(boolean a, boolean b) { + boolean BOOL_orElse(boolean a, boolean b) { return a || b; } - private boolean BOOL_implies(boolean a, boolean b) { + boolean BOOL_implies(boolean a, boolean b) { return ! a || b; } - private boolean BOOL_eq(boolean a, boolean b) { + boolean BOOL_eq(boolean a, boolean b) { return a == b; } - private boolean BOOL_ne(boolean a, boolean b) { + boolean BOOL_ne(boolean a, boolean b) { return a != b; } - private String STRING_concat(String a, String b) { + String STRING_concat(String a, String b) { return a + b; } - private BigInteger STRING_length(String a) { + BigInteger STRING_length(String a) { return BigInteger.valueOf(a.length()); } - private String STRING_chr(BigInteger a) { + String STRING_chr(BigInteger a) { 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); } @@ -197,7 +197,7 @@ private String STRING_chr(BigInteger a) { return new String(codePoint, 0, 1); } - private BigInteger STRING_ord(String a) { + 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."); } @@ -216,7 +216,7 @@ private void throwIfNotUnsignedInt(BigInteger i, String hook) { } } - private String STRING_substr(String s, BigInteger start, BigInteger end) { + String STRING_substr(String s, BigInteger start, BigInteger end) { throwIfNotInt(start, "STRING.substr"); throwIfNotInt(end, "STRING.substr"); try { @@ -226,43 +226,43 @@ private String STRING_substr(String s, BigInteger start, BigInteger end) { } } - private BigInteger STRING_find(String haystack, String needle, BigInteger idx) { + BigInteger STRING_find(String haystack, String needle, BigInteger idx) { throwIfNotInt(idx, "STRING.find"); int offset = haystack.offsetByCodePoints(0, idx.intValue()); int foundOffset = haystack.indexOf(needle, offset); return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); } - private BigInteger STRING_rfind(String haystack, String needle, BigInteger idx) { + BigInteger STRING_rfind(String haystack, String needle, BigInteger idx) { throwIfNotInt(idx, "STRING.rfind"); int offset = haystack.offsetByCodePoints(0, idx.intValue()); int foundOffset = haystack.lastIndexOf(needle, offset); return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); } - private BigInteger STRING_findChar(String haystack, String needles, BigInteger idx) { + BigInteger STRING_findChar(String haystack, String needles, BigInteger idx) { throwIfNotInt(idx, "STRING.findChar"); int offset = haystack.offsetByCodePoints(0, idx.intValue()); int foundOffset = StringUtil.indexOfAny(haystack, needles, offset); return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); } - private BigInteger STRING_rfindChar(String haystack, String needles, BigInteger idx) { + BigInteger STRING_rfindChar(String haystack, String needles, BigInteger idx) { throwIfNotInt(idx, "STRING.findChar"); int offset = haystack.offsetByCodePoints(0, idx.intValue()); int foundOffset = StringUtil.lastIndexOfAny(haystack, needles, offset); return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); } - private String STRING_float2string(FloatBuiltin f) { + String STRING_float2string(FloatBuiltin f) { return FloatBuiltin.printKFloat(f.bigFloatValue(), f.bigFloatValue()::toString); } - private String STRING_floatFormat(FloatBuiltin f, String format) { + String STRING_floatFormat(FloatBuiltin f, String format) { return FloatBuiltin.printKFloat(f.bigFloatValue(), () -> f.bigFloatValue().toString(format)); } - private FloatBuiltin STRING_string2float(String s) { + FloatBuiltin STRING_string2float(String s) { try { return FloatBuiltin.of(s); } catch (NumberFormatException e) { @@ -270,7 +270,7 @@ private FloatBuiltin STRING_string2float(String s) { } } - private BigInteger STRING_string2int(String s) { + BigInteger STRING_string2int(String s) { try { return new BigInteger(s, 10); } catch (NumberFormatException e) { @@ -278,11 +278,11 @@ private BigInteger STRING_string2int(String s) { } } - private String STRING_int2string(BigInteger i) { + String STRING_int2string(BigInteger i) { return i.toString(); } - private BigInteger STRING_string2base(String s, BigInteger base) { + 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); } @@ -293,72 +293,72 @@ private BigInteger STRING_string2base(String s, BigInteger base) { } } - private String STRING_base2string(BigInteger i, BigInteger base) { + 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()); } - private String STRING_replaceAll(String haystack, String needle, String replacement) { + String STRING_replaceAll(String haystack, String needle, String replacement) { return StringUtils.replace(haystack, needle, replacement); } - private String STRING_replace(String haystack, String needle, String replacement, BigInteger times) { + String STRING_replace(String haystack, String needle, String replacement, BigInteger times) { throwIfNotInt(times, "STRING.replace"); return StringUtils.replace(haystack, needle, replacement, times.intValue()); } - private String STRING_replaceFirst(String haystack, String needle, String replacement) { + String STRING_replaceFirst(String haystack, String needle, String replacement) { return StringUtils.replaceOnce(haystack, needle, replacement); } - private BigInteger STRING_countAllOccurrences(String haystack, String needle) { + BigInteger STRING_countAllOccurrences(String haystack, String needle) { return BigInteger.valueOf(StringUtils.countMatches(haystack, needle)); } - private boolean STRING_eq(String a, String b) { + boolean STRING_eq(String a, String b) { return a.equals(b); } - private boolean STRING_ne(String a, String b) { + boolean STRING_ne(String a, String b) { return !a.equals(b); } - private boolean STRING_lt(String a, String b) { + boolean STRING_lt(String a, String b) { return a.compareTo(b) < 0; } - private boolean STRING_gt(String a, String b) { + boolean STRING_gt(String a, String b) { return a.compareTo(b) > 0; } - private boolean STRING_le(String a, String b) { + boolean STRING_le(String a, String b) { return a.compareTo(b) <= 0; } - private boolean STRING_ge(String a, String b) { + boolean STRING_ge(String a, String b) { return a.compareTo(b) >= 0; } - private String STRING_token2string(String token) { + String STRING_token2string(String token) { return token; } - private String STRING_string2token(String str) { + String STRING_string2token(String str) { return str; } - private BigInteger INT_not(BigInteger a) { + BigInteger INT_not(BigInteger a) { return a.not(); } - private BigInteger INT_pow(BigInteger a, BigInteger b) { + BigInteger INT_pow(BigInteger a, BigInteger b) { throwIfNotUnsignedInt(b, "INT.pow"); return a.pow(b.intValue()); } - private BigInteger INT_powmod(BigInteger a, BigInteger b, BigInteger c) { + BigInteger INT_powmod(BigInteger a, BigInteger b, BigInteger c) { try { return a.modPow(b, c); } catch(ArithmeticException e) { @@ -366,75 +366,75 @@ private BigInteger INT_powmod(BigInteger a, BigInteger b, BigInteger c) { } } - private BigInteger INT_mul(BigInteger a, BigInteger b) { + BigInteger INT_mul(BigInteger a, BigInteger b) { return a.multiply(b); } - private BigInteger INT_tdiv(BigInteger a, BigInteger 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); } - private BigInteger INT_tmod(BigInteger a, BigInteger 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); } - private BigInteger INT_ediv(BigInteger a, BigInteger b) { + BigInteger INT_ediv(BigInteger a, BigInteger b) { return a.subtract(a.mod(b)).divide(b); } - private BigInteger INT_emod(BigInteger a, BigInteger b) { + BigInteger INT_emod(BigInteger a, BigInteger b) { return a.mod(b); } - private BigInteger INT_add(BigInteger a, BigInteger b) { + BigInteger INT_add(BigInteger a, BigInteger b) { return a.add(b); } - private BigInteger INT_sub(BigInteger a, BigInteger b) { + BigInteger INT_sub(BigInteger a, BigInteger b) { return a.subtract(b); } - private BigInteger INT_shr(BigInteger a, BigInteger b) { + BigInteger INT_shr(BigInteger a, BigInteger b) { throwIfNotUnsignedInt(b, "INT.shr"); return a.shiftRight(b.intValue()); } - private BigInteger INT_shl(BigInteger a, BigInteger b) { + BigInteger INT_shl(BigInteger a, BigInteger b) { throwIfNotUnsignedInt(b, "INT.shl"); return a.shiftLeft(b.intValue()); } - private BigInteger INT_and(BigInteger a, BigInteger b) { + BigInteger INT_and(BigInteger a, BigInteger b) { return a.and(b); } - private BigInteger INT_xor(BigInteger a, BigInteger b) { + BigInteger INT_xor(BigInteger a, BigInteger b) { return a.xor(b); } - private BigInteger INT_or(BigInteger a, BigInteger b) { + BigInteger INT_or(BigInteger a, BigInteger b) { return a.or(b); } - private BigInteger INT_min(BigInteger a, BigInteger b) { + BigInteger INT_min(BigInteger a, BigInteger b) { return a.min(b); } - private BigInteger INT_max(BigInteger a, BigInteger b) { + BigInteger INT_max(BigInteger a, BigInteger b) { return a.max(b); } - private BigInteger INT_abs(BigInteger a) { + BigInteger INT_abs(BigInteger a) { return a.abs(); } - private BigInteger INT_log2(BigInteger a) { + 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); } @@ -446,7 +446,7 @@ private BigInteger INT_log2(BigInteger a) { return BigInteger.valueOf(log2); } - private BigInteger INT_bitRange(BigInteger i, BigInteger index, BigInteger length) { + BigInteger INT_bitRange(BigInteger i, BigInteger index, BigInteger length) { throwIfNotUnsignedInt(index, "INT.bitRange"); throwIfNotUnsignedInt(length, "INT.bitRange"); byte[] twosComplement = i.toByteArray(); @@ -460,7 +460,7 @@ private BigInteger INT_bitRange(BigInteger i, BigInteger index, BigInteger lengt return i; } - private BigInteger INT_signExtendBitRange(BigInteger i, BigInteger index, BigInteger length) { + BigInteger INT_signExtendBitRange(BigInteger i, BigInteger index, BigInteger length) { throwIfNotUnsignedInt(index, "INT.signExtendBitRange"); throwIfNotUnsignedInt(length, "INT.signExtendBitRange"); if (length.intValue() == 0) { @@ -478,52 +478,52 @@ private BigInteger INT_signExtendBitRange(BigInteger i, BigInteger index, BigInt } } - private boolean INT_lt(BigInteger a, BigInteger b) { + boolean INT_lt(BigInteger a, BigInteger b) { return a.compareTo(b) < 0; } - private boolean INT_gt(BigInteger a, BigInteger b) { + boolean INT_gt(BigInteger a, BigInteger b) { return a.compareTo(b) > 0; } - private boolean INT_le(BigInteger a, BigInteger b) { + boolean INT_le(BigInteger a, BigInteger b) { return a.compareTo(b) <= 0; } - private boolean INT_ge(BigInteger a, BigInteger b) { + boolean INT_ge(BigInteger a, BigInteger b) { return a.compareTo(b) >= 0; } - private boolean INT_eq(BigInteger a, BigInteger b) { + boolean INT_eq(BigInteger a, BigInteger b) { return a.equals(b); } - private boolean INT_ne(BigInteger a, BigInteger b) { + boolean INT_ne(BigInteger a, BigInteger b) { return !a.equals(b); } - private BigInteger FLOAT_precision(FloatBuiltin f) { + BigInteger FLOAT_precision(FloatBuiltin f) { return BigInteger.valueOf(f.precision()); } - private BigInteger FLOAT_exponentBits(FloatBuiltin f) { + BigInteger FLOAT_exponentBits(FloatBuiltin f) { return BigInteger.valueOf(f.exponent()); } - private BigInteger FLOAT_exponent(FloatBuiltin f) { + BigInteger FLOAT_exponent(FloatBuiltin f) { BinaryMathContext mc = f.getMathContext(); return BigInteger.valueOf(f.bigFloatValue().exponent(mc.minExponent, mc.maxExponent)); } - private boolean FLOAT_sign(FloatBuiltin f) { + boolean FLOAT_sign(FloatBuiltin f) { return f.bigFloatValue().sign(); } - private boolean FLOAT_isNaN(FloatBuiltin f) { + boolean FLOAT_isNaN(FloatBuiltin f) { return f.bigFloatValue().isNaN(); } - private FloatBuiltin FLOAT_neg(FloatBuiltin f) { + FloatBuiltin FLOAT_neg(FloatBuiltin f) { return FloatBuiltin.of(f.bigFloatValue().negate(f.getMathContext()), f.exponent()); } @@ -533,46 +533,46 @@ private void throwIfNotMatched(FloatBuiltin a, FloatBuiltin b, String hook) { } } - private FloatBuiltin FLOAT_pow(FloatBuiltin a, FloatBuiltin b) { + FloatBuiltin FLOAT_pow(FloatBuiltin a, FloatBuiltin b) { throwIfNotMatched(a, b, "FLOAT.pow"); return FloatBuiltin.of(a.bigFloatValue().pow(b.bigFloatValue(), a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_mul(FloatBuiltin a, FloatBuiltin b) { + FloatBuiltin FLOAT_mul(FloatBuiltin a, FloatBuiltin b) { throwIfNotMatched(a, b, "FLOAT.mul"); return FloatBuiltin.of(a.bigFloatValue().multiply(b.bigFloatValue(), a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_div(FloatBuiltin a, FloatBuiltin b) { + FloatBuiltin FLOAT_div(FloatBuiltin a, FloatBuiltin b) { throwIfNotMatched(a, b, "FLOAT.div"); return FloatBuiltin.of(a.bigFloatValue().divide(b.bigFloatValue(), a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_rem(FloatBuiltin a, FloatBuiltin b) { + FloatBuiltin FLOAT_rem(FloatBuiltin a, FloatBuiltin b) { throwIfNotMatched(a, b, "FLOAT.rem"); return FloatBuiltin.of(a.bigFloatValue().remainder(b.bigFloatValue(), a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_add(FloatBuiltin a, FloatBuiltin b) { + FloatBuiltin FLOAT_add(FloatBuiltin a, FloatBuiltin b) { throwIfNotMatched(a, b, "FLOAT.add"); return FloatBuiltin.of(a.bigFloatValue().add(b.bigFloatValue(), a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_sub(FloatBuiltin a, FloatBuiltin b) { + FloatBuiltin FLOAT_sub(FloatBuiltin a, FloatBuiltin b) { throwIfNotMatched(a, b, "FLOAT.sub"); return FloatBuiltin.of(a.bigFloatValue().subtract(b.bigFloatValue(), a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_root(FloatBuiltin a, BigInteger b) { + FloatBuiltin FLOAT_root(FloatBuiltin a, BigInteger b) { throwIfNotInt(b, "FLOAT.root"); return FloatBuiltin.of(a.bigFloatValue().root(b.intValue(), a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_abs(FloatBuiltin a) { + FloatBuiltin FLOAT_abs(FloatBuiltin a) { return FloatBuiltin.of(a.bigFloatValue().abs(a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_round(FloatBuiltin a, BigInteger prec, BigInteger exp) { + FloatBuiltin FLOAT_round(FloatBuiltin a, BigInteger prec, BigInteger exp) { throwIfNotUnsignedInt(prec, "FLOAT.round"); throwIfNotUnsignedInt(exp, "FLOAT.round"); if (prec.intValue() < 2 || exp.intValue() < 2) { @@ -581,62 +581,62 @@ private FloatBuiltin FLOAT_round(FloatBuiltin a, BigInteger prec, BigInteger exp return FloatBuiltin.of(a.bigFloatValue().round(new BinaryMathContext(prec.intValue(), exp.intValue())), exp.intValue()); } - private FloatBuiltin FLOAT_floor(FloatBuiltin a) { + FloatBuiltin FLOAT_floor(FloatBuiltin a) { return FloatBuiltin.of(a.bigFloatValue().rint(a.getMathContext().withRoundingMode(RoundingMode.FLOOR)), a.exponent()); } - private FloatBuiltin FLOAT_ceil(FloatBuiltin a) { + FloatBuiltin FLOAT_ceil(FloatBuiltin a) { return FloatBuiltin.of(a.bigFloatValue().rint(a.getMathContext().withRoundingMode(RoundingMode.CEILING)), a.exponent()); } - private FloatBuiltin FLOAT_exp(FloatBuiltin a) { + FloatBuiltin FLOAT_exp(FloatBuiltin a) { return FloatBuiltin.of(a.bigFloatValue().exp(a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_log(FloatBuiltin a) { + FloatBuiltin FLOAT_log(FloatBuiltin a) { return FloatBuiltin.of(a.bigFloatValue().log(a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_sin(FloatBuiltin a) { + FloatBuiltin FLOAT_sin(FloatBuiltin a) { return FloatBuiltin.of(a.bigFloatValue().sin(a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_cos(FloatBuiltin a) { + FloatBuiltin FLOAT_cos(FloatBuiltin a) { return FloatBuiltin.of(a.bigFloatValue().cos(a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_tan(FloatBuiltin a) { + FloatBuiltin FLOAT_tan(FloatBuiltin a) { return FloatBuiltin.of(a.bigFloatValue().tan(a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_asin(FloatBuiltin a) { + FloatBuiltin FLOAT_asin(FloatBuiltin a) { return FloatBuiltin.of(a.bigFloatValue().asin(a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_acos(FloatBuiltin a) { + FloatBuiltin FLOAT_acos(FloatBuiltin a) { return FloatBuiltin.of(a.bigFloatValue().acos(a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_atan(FloatBuiltin a) { + FloatBuiltin FLOAT_atan(FloatBuiltin a) { return FloatBuiltin.of(a.bigFloatValue().atan(a.getMathContext()), a.exponent()); } - private FloatBuiltin FLOAT_atan2(FloatBuiltin a, FloatBuiltin b) { + 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()); } - private FloatBuiltin FLOAT_max(FloatBuiltin a, FloatBuiltin b) { + 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()); } - private FloatBuiltin FLOAT_min(FloatBuiltin a, FloatBuiltin b) { + 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()); } - private FloatBuiltin FLOAT_maxValue(BigInteger prec, BigInteger exp) { + FloatBuiltin FLOAT_maxValue(BigInteger prec, BigInteger exp) { throwIfNotUnsignedInt(prec, "FLOAT.maxValue"); throwIfNotUnsignedInt(exp, "FLOAT.maxValue"); if (prec.intValue() < 2 || exp.intValue() < 2) { @@ -646,7 +646,7 @@ private FloatBuiltin FLOAT_maxValue(BigInteger prec, BigInteger exp) { return FloatBuiltin.of(BigFloat.maxValue(mc.precision, mc.maxExponent), exp.intValue()); } - private FloatBuiltin FLOAT_minValue(BigInteger prec, BigInteger exp) { + FloatBuiltin FLOAT_minValue(BigInteger prec, BigInteger exp) { throwIfNotUnsignedInt(prec, "FLOAT.minValue"); throwIfNotUnsignedInt(exp, "FLOAT.minValue"); if (prec.intValue() < 2 || exp.intValue() < 2) { @@ -656,31 +656,31 @@ private FloatBuiltin FLOAT_minValue(BigInteger prec, BigInteger exp) { return FloatBuiltin.of(BigFloat.minValue(mc.precision, mc.minExponent), exp.intValue()); } - private boolean FLOAT_lt(FloatBuiltin a, FloatBuiltin b) { + boolean FLOAT_lt(FloatBuiltin a, FloatBuiltin b) { return a.bigFloatValue().lessThan(b.bigFloatValue()); } - private boolean FLOAT_le(FloatBuiltin a, FloatBuiltin b) { + boolean FLOAT_le(FloatBuiltin a, FloatBuiltin b) { return a.bigFloatValue().lessThanOrEqualTo(b.bigFloatValue()); } - private boolean FLOAT_gt(FloatBuiltin a, FloatBuiltin b) { + boolean FLOAT_gt(FloatBuiltin a, FloatBuiltin b) { return a.bigFloatValue().greaterThan(b.bigFloatValue()); } - private boolean FLOAT_ge(FloatBuiltin a, FloatBuiltin b) { + boolean FLOAT_ge(FloatBuiltin a, FloatBuiltin b) { return a.bigFloatValue().greaterThanOrEqualTo(b.bigFloatValue()); } - private boolean FLOAT_eq(FloatBuiltin a, FloatBuiltin b) { + boolean FLOAT_eq(FloatBuiltin a, FloatBuiltin b) { return a.bigFloatValue().equalTo(b.bigFloatValue()); } - private boolean FLOAT_ne(FloatBuiltin a, FloatBuiltin b) { + boolean FLOAT_ne(FloatBuiltin a, FloatBuiltin b) { return !a.bigFloatValue().equalTo(b.bigFloatValue()); } - private FloatBuiltin FLOAT_int2float(BigInteger a, BigInteger prec, BigInteger exp) { + FloatBuiltin FLOAT_int2float(BigInteger a, BigInteger prec, BigInteger exp) { throwIfNotUnsignedInt(prec, "FLOAT.int2float"); throwIfNotUnsignedInt(exp, "FLOAT.int2float"); if (prec.intValue() < 2 || exp.intValue() < 2) { @@ -690,7 +690,7 @@ private FloatBuiltin FLOAT_int2float(BigInteger a, BigInteger prec, BigInteger e return FloatBuiltin.of(new BigFloat(a, mc), exp.intValue()); } - private BigInteger FLOAT_float2int(FloatBuiltin a) { + BigInteger FLOAT_float2int(FloatBuiltin a) { try { return a.bigFloatValue().rint(a.getMathContext().withRoundingMode(RoundingMode.DOWN)).toBigIntegerExact(); } catch (ArithmeticException e) { From ce43411ebab6c2f4a4e9cb57a054bfc6ec52253a Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 15:49:03 -0500 Subject: [PATCH 11/27] add unit tests for STRING, BOOL, INT --- .../compile/ConstantFoldingTest.java | 754 ++++++++++++++++++ 1 file changed, 754 insertions(+) create mode 100644 kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java 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..2634b83d167 --- /dev/null +++ b/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java @@ -0,0 +1,754 @@ +// 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 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))); + } +} From 8aec44c04ab146d2b4bd7fca13534ccc65378b2c Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 15:49:15 -0500 Subject: [PATCH 12/27] add setLoc function --- .../src/main/java/org/kframework/compile/ConstantFolding.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 71fc6119314..890f69f0901 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -35,6 +35,10 @@ public class ConstantFolding { 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; From 8fae2ca450af39c0603a1628de33e2b00f9a50cc Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 15:49:22 -0500 Subject: [PATCH 13/27] fix STRING.length --- .../src/main/java/org/kframework/compile/ConstantFolding.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 890f69f0901..899b802806d 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -190,7 +190,7 @@ String STRING_concat(String a, String b) { } BigInteger STRING_length(String a) { - return BigInteger.valueOf(a.length()); + return BigInteger.valueOf(a.codePointCount(0, a.length())); } String STRING_chr(BigInteger a) { From 59700316144ece1db1eb32f15fcbbea74e42c217 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 15:49:30 -0500 Subject: [PATCH 14/27] fix STRING.ord --- .../src/main/java/org/kframework/compile/ConstantFolding.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 899b802806d..43142b9fc3e 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -202,7 +202,7 @@ String STRING_chr(BigInteger a) { } BigInteger STRING_ord(String a) { - if (a.codePointCount(0, a.length()) > 1) { + 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)); From a0a8235f7f691f52dab6330f299318e8e8141019 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 15:49:58 -0500 Subject: [PATCH 15/27] some fixes where nonnegative integers are expected --- .../main/java/org/kframework/compile/ConstantFolding.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 43142b9fc3e..9d83f43af6f 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -221,8 +221,8 @@ private void throwIfNotUnsignedInt(BigInteger i, String hook) { } String STRING_substr(String s, BigInteger start, BigInteger end) { - throwIfNotInt(start, "STRING.substr"); - throwIfNotInt(end, "STRING.substr"); + 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) { @@ -309,7 +309,7 @@ String STRING_replaceAll(String haystack, String needle, String replacement) { } String STRING_replace(String haystack, String needle, String replacement, BigInteger times) { - throwIfNotInt(times, "STRING.replace"); + throwIfNotUnsignedInt(times, "STRING.replace"); return StringUtils.replace(haystack, needle, replacement, times.intValue()); } From 7f42e6ae84d00cfe6550b959e9d05af632f22f22 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 15:50:13 -0500 Subject: [PATCH 16/27] fix find, rfind, findChar, rfindChar --- .../kframework/compile/ConstantFolding.java | 48 ++++++++++++------- 1 file changed, 32 insertions(+), 16 deletions(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 9d83f43af6f..7ee16fc3f81 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -231,31 +231,47 @@ String STRING_substr(String s, BigInteger start, BigInteger end) { } BigInteger STRING_find(String haystack, String needle, BigInteger idx) { - throwIfNotInt(idx, "STRING.find"); - int offset = haystack.offsetByCodePoints(0, idx.intValue()); - int foundOffset = haystack.indexOf(needle, offset); - return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + 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) { - throwIfNotInt(idx, "STRING.rfind"); - int offset = haystack.offsetByCodePoints(0, idx.intValue()); - int foundOffset = haystack.lastIndexOf(needle, offset); - return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + 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) { - throwIfNotInt(idx, "STRING.findChar"); - int offset = haystack.offsetByCodePoints(0, idx.intValue()); - int foundOffset = StringUtil.indexOfAny(haystack, needles, offset); - return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + 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) { - throwIfNotInt(idx, "STRING.findChar"); - int offset = haystack.offsetByCodePoints(0, idx.intValue()); - int foundOffset = StringUtil.lastIndexOfAny(haystack, needles, offset); - return BigInteger.valueOf((foundOffset == -1 ? -1 : haystack.codePointCount(0, foundOffset))); + 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) { From d5aee49916b12493695479401e77eab277eb9cc4 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 15:50:23 -0500 Subject: [PATCH 17/27] fix float2string --- .../src/main/java/org/kframework/compile/ConstantFolding.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 7ee16fc3f81..26fc3b91319 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -275,7 +275,7 @@ BigInteger STRING_rfindChar(String haystack, String needles, BigInteger idx) { } String STRING_float2string(FloatBuiltin f) { - return FloatBuiltin.printKFloat(f.bigFloatValue(), f.bigFloatValue()::toString); + return f.value(); } String STRING_floatFormat(FloatBuiltin f, String format) { From 8d5b5f02932611a7fbe461d8f590373b6864fcac Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 15:50:30 -0500 Subject: [PATCH 18/27] fix ediv and emod --- .../org/kframework/compile/ConstantFolding.java | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 26fc3b91319..1dcdf9e4850 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -405,11 +405,21 @@ BigInteger INT_tmod(BigInteger a, BigInteger b) { } BigInteger INT_ediv(BigInteger a, BigInteger b) { - return a.subtract(a.mod(b)).divide(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) { - return a.mod(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) { From 8e26e0023addd516d93ce85fafb7d5941735277c Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 15:50:37 -0500 Subject: [PATCH 19/27] fix bitRange --- .../java/org/kframework/compile/ConstantFolding.java | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 1dcdf9e4850..15de611002b 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -479,15 +479,7 @@ BigInteger INT_log2(BigInteger a) { BigInteger INT_bitRange(BigInteger i, BigInteger index, BigInteger length) { throwIfNotUnsignedInt(index, "INT.bitRange"); throwIfNotUnsignedInt(length, "INT.bitRange"); - byte[] twosComplement = i.toByteArray(); - BigInteger positive = new BigInteger(1, twosComplement); - for (int j = 0; j < index.intValue(); j++) { - i = i.clearBit(j); - } - for (int j = index.intValue() + length.intValue(); j < twosComplement.length * 8; j++) { - i = i.clearBit(j); - } - return i; + 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) { From 67a0d93c18f64c0c69d37189af434b7850d51753 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 15:50:43 -0500 Subject: [PATCH 20/27] add hashCode and equals for FloatBuiltin --- .../org/kframework/compile/FloatBuiltin.java | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java b/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java index c68e95f2bb7..578d4770639 100644 --- a/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java +++ b/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java @@ -161,4 +161,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(); + } } From 0cdb84df921934864826646b635f14936cd1e986 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 15:51:00 -0500 Subject: [PATCH 21/27] fix bugs in indexOfAny and lastIndexOfAny --- .../main/java/org/kframework/utils/StringUtil.java | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) 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); From a37cd0a14f535675d807d65b2d878b02f46c5a58 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 8 Apr 2021 16:05:08 -0500 Subject: [PATCH 22/27] fix whitespace --- .../test/java/org/kframework/compile/ConstantFoldingTest.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java b/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java index 2634b83d167..343cc5af75d 100644 --- a/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java +++ b/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java @@ -283,7 +283,7 @@ public void testString2Int() { 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")); + assertEquals(new BigInteger("100000000000000000000"), cf.STRING_string2int("100000000000000000000")); } @Test(expected=KEMException.class) @@ -645,7 +645,7 @@ public void testIntLog2Error1() { @Test(expected=KEMException.class) public void testIntLog2Error2() { cf.INT_log2(BigInteger.valueOf(-1)); - } + } @Test public void testBitRange() { From 5778ad0bd397a7a0a423b152d23aec108f373a7f Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 9 Apr 2021 16:42:03 -0500 Subject: [PATCH 23/27] fix float2int --- .../src/main/java/org/kframework/compile/ConstantFolding.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 15de611002b..60983823e8f 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -714,7 +714,7 @@ FloatBuiltin FLOAT_int2float(BigInteger a, BigInteger prec, BigInteger exp) { BigInteger FLOAT_float2int(FloatBuiltin a) { try { - return a.bigFloatValue().rint(a.getMathContext().withRoundingMode(RoundingMode.DOWN)).toBigIntegerExact(); + 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); } From 8531e8c66483798a4ea9cd62ccb4a658737a430a Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 9 Apr 2021 16:42:13 -0500 Subject: [PATCH 24/27] add some useful functions to FloatBuiltin --- .../main/java/org/kframework/compile/FloatBuiltin.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java b/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java index 578d4770639..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. */ From b906b4bdff834b6380d687add7bd4dae0c280f17 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 9 Apr 2021 16:42:26 -0500 Subject: [PATCH 25/27] add tests for FLOAT hooks --- .../compile/ConstantFoldingTest.java | 288 ++++++++++++++++++ 1 file changed, 288 insertions(+) diff --git a/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java b/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java index 343cc5af75d..3ec8b7f33b7 100644 --- a/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java +++ b/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java @@ -9,6 +9,7 @@ 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.*; @@ -751,4 +752,291 @@ 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))); + } } From 26e5fb7def19beafdd5338fc4d1ff6bdb1637462 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 14 Apr 2021 14:19:36 -0500 Subject: [PATCH 26/27] add comment --- kernel/src/main/java/org/kframework/compile/ConstantFolding.java | 1 + 1 file changed, 1 insertion(+) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 60983823e8f..5fb88fbd94f 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -194,6 +194,7 @@ BigInteger STRING_length(String a) { } 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); } From 2c871aaf1fed5e3505846fc03a79fd2c31af0441 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 14 Apr 2021 14:25:40 -0500 Subject: [PATCH 27/27] add integration tests --- .../regression-new/checks/invalidConstantExp.k | 6 ++++++ .../checks/invalidConstantExp.k.out | 6 ++++++ .../tests/regression-new/constant-folding/1.test | 1 + .../regression-new/constant-folding/1.test.out | 3 +++ .../tests/regression-new/constant-folding/2.test | 1 + .../regression-new/constant-folding/2.test.out | 3 +++ .../tests/regression-new/constant-folding/3.test | 1 + .../regression-new/constant-folding/3.test.out | 3 +++ .../regression-new/constant-folding/Makefile | 7 +++++++ .../tests/regression-new/constant-folding/test.k | 15 +++++++++++++++ 10 files changed, 46 insertions(+) create mode 100644 k-distribution/tests/regression-new/checks/invalidConstantExp.k create mode 100644 k-distribution/tests/regression-new/checks/invalidConstantExp.k.out create mode 100644 k-distribution/tests/regression-new/constant-folding/1.test create mode 100644 k-distribution/tests/regression-new/constant-folding/1.test.out create mode 100644 k-distribution/tests/regression-new/constant-folding/2.test create mode 100644 k-distribution/tests/regression-new/constant-folding/2.test.out create mode 100644 k-distribution/tests/regression-new/constant-folding/3.test create mode 100644 k-distribution/tests/regression-new/constant-folding/3.test.out create mode 100644 k-distribution/tests/regression-new/constant-folding/Makefile create mode 100644 k-distribution/tests/regression-new/constant-folding/test.k 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