Add limited loop to Condition simplifier (#2915)

* Add limited loop in Condition simplifier

* Format with fourmolu

* Remove undefined from SubstitutionSimplifier

* Format with fourmolu

* Add warning for unsimplified Condition

* Format with fourmolu

* Remove commented out traces

* Materialize Nix expressions

* Add integration test

* Review: use foldM instead of explicit loop

Co-authored-by: David Cox <[email protected]>

* Format with fourmolu

Co-authored-by: github-actions <[email protected]>
Co-authored-by: David Cox <[email protected]>

Author: 3 people

kore/kore.cabal

@@ -358,7 +358,7 @@ library
     Kore.Log.WarnStuckClaimState
     Kore.Log.WarnSymbolSMTRepresentation
     Kore.Log.WarnTrivialClaim
-    Kore.Log.WarnUnsimplifiedPredicate
+    Kore.Log.WarnUnsimplified
     Kore.ModelChecker.Bounded
     Kore.ModelChecker.Simplification
     Kore.ModelChecker.Step

kore/src/Kore/Log/Registry.hs

@@ -139,7 +139,8 @@ import Kore.Log.WarnSymbolSMTRepresentation (
 import Kore.Log.WarnTrivialClaim (
     WarnTrivialClaim,
  )
-import Kore.Log.WarnUnsimplifiedPredicate (
+import Kore.Log.WarnUnsimplified (
+    WarnUnsimplifiedCondition,
     WarnUnsimplifiedPredicate,
  )
 import Log (
@@ -220,6 +221,7 @@ entryHelpDocsErr, entryHelpDocsNoErr :: [Pretty.Doc ()]
             , mk $ Proxy @DebugBeginClaim
             , mk $ Proxy @DebugProven
             , mk $ Proxy @WarnUnsimplifiedPredicate
+            , mk $ Proxy @WarnUnsimplifiedCondition
             ]
         ,
             [ mk $ Proxy @ErrorBottomTotalFunction

kore/src/Kore/Log/WarnUnsimplifiedPredicate.hs renamed to kore/src/Kore/Log/WarnUnsimplified.hs

@@ -2,11 +2,20 @@
 Copyright   : (c) Runtime Verification, 2021
 License     : BSD-3-Clause
 -}
-module Kore.Log.WarnUnsimplifiedPredicate (
+module Kore.Log.WarnUnsimplified (
     WarnUnsimplifiedPredicate (..),
     warnUnsimplifiedPredicate,
+    WarnUnsimplifiedCondition (..),
+    warnUnsimplifiedCondition,
 ) where
 
+import Kore.Internal.Condition (
+    Condition,
+ )
+import Kore.Internal.Conditional (
+    Conditional,
+ )
+import qualified Kore.Internal.Conditional as Conditional
 import Kore.Internal.MultiAnd (
     MultiAnd,
  )
@@ -31,6 +40,13 @@ data WarnUnsimplifiedPredicate = WarnUnsimplifiedPredicate
     }
     deriving stock (Show)
 
+data WarnUnsimplifiedCondition = WarnUnsimplifiedCondition
+    { limit :: !Int
+    , original :: !(Condition RewritingVariableName)
+    , output :: !(Condition RewritingVariableName)
+    }
+    deriving stock (Show)
+
 instance Pretty WarnUnsimplifiedPredicate where
     pretty WarnUnsimplifiedPredicate{original, output, limit} =
         Pretty.vsep
@@ -49,11 +65,34 @@ instance Pretty WarnUnsimplifiedPredicate where
             , (Pretty.indent 4) (Pretty.pretty output)
             ]
 
+instance Pretty WarnUnsimplifiedCondition where
+    pretty WarnUnsimplifiedCondition{original, output, limit} =
+        Pretty.vsep
+            [ Pretty.hsep
+                [ "Condition not simplified after"
+                , Pretty.pretty limit
+                , "rounds."
+                ]
+            , "Original condition:"
+            , (Pretty.indent 4) (Pretty.pretty original)
+            , Pretty.hsep
+                [ "Output after"
+                , Pretty.pretty limit
+                , "rounds:"
+                ]
+            , (Pretty.indent 4) (Pretty.pretty output)
+            ]
+
 instance Entry WarnUnsimplifiedPredicate where
     entrySeverity _ = Warning
     oneLineDoc WarnUnsimplifiedPredicate{limit} = Pretty.pretty limit
     helpDoc _ = "warn when a predicate is not simplified"
 
+instance Entry WarnUnsimplifiedCondition where
+    entrySeverity _ = Warning
+    oneLineDoc WarnUnsimplifiedCondition{limit} = Pretty.pretty limit
+    helpDoc _ = "warn when a condition is not simplified"
+
 warnUnsimplifiedPredicate ::
     MonadLog log =>
     Int ->
@@ -62,3 +101,15 @@ warnUnsimplifiedPredicate ::
     log ()
 warnUnsimplifiedPredicate limit original output =
     logEntry WarnUnsimplifiedPredicate{limit, original, output}
+
+warnUnsimplifiedCondition ::
+    MonadLog log =>
+    Int ->
+    Conditional RewritingVariableName any ->
+    Conditional RewritingVariableName any ->
+    log ()
+warnUnsimplifiedCondition
+    limit
+    (Conditional.withoutTerm -> original)
+    (Conditional.withoutTerm -> output) =
+        logEntry WarnUnsimplifiedCondition{limit, original, output}

kore/src/Kore/Simplify/Condition.hs

@@ -41,6 +41,9 @@ import Kore.Internal.Substitution (
     Assignment,
  )
 import qualified Kore.Internal.Substitution as Substitution
+import Kore.Log.WarnUnsimplified (
+    warnUnsimplifiedCondition,
+ )
 import Kore.Rewrite.RewritingVariable (
     RewritingVariableName,
  )
@@ -78,9 +81,24 @@ simplify ::
     SideCondition RewritingVariableName ->
     Conditional RewritingVariableName any ->
     LogicT simplifier (Conditional RewritingVariableName any)
-simplify SubstitutionSimplifier{simplifySubstitution} sideCondition =
-    normalize >=> worker
+simplify SubstitutionSimplifier{simplifySubstitution} sideCondition original = do
+    normOriginal <- normalize original
+    (isFullySimplified, result) <- foldM simplifyingCondition (False, normOriginal) [1 .. limit]
+    unless isFullySimplified $ warnUnsimplifiedCondition limit original result
+    return result
   where
+    limit :: Int
+    limit = 4
+
+    simplifyingCondition ::
+        (Bool, Conditional RewritingVariableName any) ->
+        Int ->
+        LogicT simplifier (Bool, Conditional RewritingVariableName any)
+    simplifyingCondition result@(True, _) _ = return result
+    simplifyingCondition (_, input) _ = do
+        output <- worker input
+        return (fullySimplified output, extract output)
+
     worker Conditional{term, predicate, substitution} = do
         let substitution' = Substitution.toMap substitution
             predicate' = substitute substitution' predicate
@@ -100,9 +118,7 @@ simplify SubstitutionSimplifier{simplifySubstitution} sideCondition =
                     (field @"predicate")
                     simplifyConjunctions
                     normalized{term}
-        if fullySimplified simplifiedPattern
-            then return (extract simplifiedPattern)
-            else worker (extract simplifiedPattern)
+        return simplifiedPattern
 
     simplifyPredicate predicate =
         Predicate.simplify sideCondition predicate & lift

kore/src/Kore/Simplify/Pattern.hs

@@ -129,7 +129,8 @@ makeEvaluate sideCondition =
 
     worker pattern' =
         OrPattern.observeAllT $ do
-            withSimplifiedCondition <- simplifyCondition sideCondition pattern'
+            withSimplifiedCondition <-
+                simplifyCondition sideCondition pattern'
             let (term, simplifiedCondition) =
                     Conditional.splitTerm withSimplifiedCondition
                 term' = substitute (toMap $ substitution simplifiedCondition) term

kore/src/Kore/Simplify/Predicate.hs

@@ -53,7 +53,7 @@ import Kore.Internal.TermLike (
     termLikeSort,
  )
 import qualified Kore.Internal.TermLike as TermLike
-import Kore.Log.WarnUnsimplifiedPredicate (
+import Kore.Log.WarnUnsimplified (
     warnUnsimplifiedPredicate,
  )
 import Kore.Rewrite.RewritingVariable (

nix/kore.nix.d/kore.nix

@@ -279,7 +279,7 @@
           "Kore/Log/WarnStuckClaimState"
           "Kore/Log/WarnSymbolSMTRepresentation"
           "Kore/Log/WarnTrivialClaim"
-          "Kore/Log/WarnUnsimplifiedPredicate"
+          "Kore/Log/WarnUnsimplified"
           "Kore/ModelChecker/Bounded"
           "Kore/ModelChecker/Simplification"
           "Kore/ModelChecker/Step"

test/kprove-hangs/Makefile

@@ -0,0 +1,2 @@
+DEF = test
+include $(CURDIR)/../include.mk

test/kprove-hangs/test-spec.k

@@ -0,0 +1,11 @@
+module VERIFICATION
+    imports TEST
+
+endmodule
+
+module TEST-SPEC
+    imports VERIFICATION
+
+    claim <k> (a ~> _ => .) ... </k>
+
+endmodule

test/kprove-hangs/test-spec.k.out.golden

@@ -0,0 +1,11 @@
+  #Ceil ( _0 ~> _DotVar1 ~> . )
+#And
+  #Not ( {
+    _DotVar1
+  #Equals
+    a ~> _0 ~> _DotVar1 ~> .
+  } )
+#And
+  <k>
+    a ~> _0 ~> _DotVar1 ~> .
+  </k>