Cell initializers as total functions (#4311)

fixes: #4301 Some cell initializers don't take any configuration variables as parameters and hence are constant functions. These can be marked as total functions for the provers. --------- Co-authored-by: Bruce Collie <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · May 10, 2024 · 75493bd · 75493bd
1 parent 3a49a8c
commit 75493bd
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git a/k-frontend/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java b/k-frontend/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java
@@ -458,7 +458,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
               KLabel(initLabel),
               initSort,
               Seq(Terminal(initLabel)),
-              Att.empty().add(Att.INITIALIZER()).add(Att.FUNCTION()));
+              Att.empty().add(Att.INITIALIZER()).add(Att.FUNCTION()).add(Att.TOTAL()));
       initializerRule =
           Rule(
               KRewrite(

diff --git a/k-frontend/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java b/k-frontend/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java
@@ -99,6 +99,7 @@ public void testSingleTop() {
         GenerateSentencesFromConfigDecl.gen(kem, configuration, BooleanUtils.FALSE, Att.empty(), m);
     Att initializerAtts = Att.empty().add(Att.INITIALIZER());
     Att productionAtts = initializerAtts.add(Att.FUNCTION());
+    Att totalProductionAtts = productionAtts.add(Att.TOTAL());
     Set<Sentence> reference =
         Set(
             Production(
@@ -209,7 +210,7 @@ public void testSingleTop() {
                 KLabel("initOptCell"),
                 Sort("OptCell"),
                 Seq(Terminal("initOptCell")),
-                productionAtts),
+                totalProductionAtts),
             Rule(
                 KRewrite(
                     KApply(KLabel("initThreadsCell"), KVariable("Init")),

diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py
@@ -53,12 +53,12 @@ def test_proof_trace(self, hints: bytes) -> None:
         # check that the first event is the rewrite a() => b()
         assert pt.trace[0].is_step_event()
         assert isinstance(pt.trace[0].step_event, prooftrace.LLVMRewriteEvent)
-        assert pt.trace[0].step_event.rule_ordinal == 96
+        assert pt.trace[0].step_event.rule_ordinal == 97
 
         # check that the second event is the rewrite b() => c()
         assert pt.trace[1].is_step_event()
         assert isinstance(pt.trace[1].step_event, prooftrace.LLVMRewriteEvent)
-        assert pt.trace[1].step_event.rule_ordinal == 97
+        assert pt.trace[1].step_event.rule_ordinal == 98
 
         # check that the third event is a configuration
         assert pt.trace[2].is_kore_pattern()