Constant folding of Int, Float, String, and Bool

k-distribution/include/kframework/builtin/domains.md

@@ -1119,8 +1119,8 @@ module INT
   syntax Int ::= freshInt(Int)    [freshGenerator, function, functional]
   rule freshInt(I:Int) => I
 
-  syntax Int ::= randInt(Int) [function, hook(INT.rand)]
-  syntax K ::= srandInt(Int) [function, hook(INT.srand)]
+  syntax Int ::= randInt(Int) [function, hook(INT.rand), impure]
+  syntax K ::= srandInt(Int) [function, hook(INT.srand), impure]
 endmodule
 ```
 

k-distribution/tests/regression-new/checks/invalidConstantExp.k

@@ -0,0 +1,6 @@
+module INVALIDCONSTANTEXP
+  imports INT
+
+  rule 0 => 1 /Int 0
+
+endmodule

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)

k-distribution/tests/regression-new/constant-folding/1.test

@@ -0,0 +1 @@
+3

k-distribution/tests/regression-new/constant-folding/1.test.out

@@ -0,0 +1,3 @@
+<k>
+  .
+</k>

k-distribution/tests/regression-new/constant-folding/2.test

@@ -0,0 +1 @@
+11

k-distribution/tests/regression-new/constant-folding/2.test.out

@@ -0,0 +1,3 @@
+<k>
+  .
+</k>

k-distribution/tests/regression-new/constant-folding/3.test

@@ -0,0 +1 @@
+5

k-distribution/tests/regression-new/constant-folding/3.test.out

@@ -0,0 +1,3 @@
+<k>
+  5 ~> .
+</k>

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

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

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<Definition, Definition> 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<Definition, Definition> 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<Definition, Definition> genCoverage = d -> DefinitionTransformer.fromRuleBodyTransformerWithRule((r, body) -> cov.gen(r, body, d.mainModule()), "generate coverage instrumentation").apply(d);
@@ -160,6 +162,7 @@ public Function<Definition, Definition> steps() {
                 .andThen(subsortKItem)
                 .andThen(generateSortPredicateSyntax)
                 .andThen(generateSortProjections)
+                .andThen(constantFolding)
                 .andThen(expandMacros)
                 .andThen(guardOrs)
                 .andThen(AddImplicitComputationCell::transformDefinition)